import gov.nasa.jpf.Config; //导入依赖的package包/类
@Override
public PredicateAbstraction create(Config config, String[]... args) {
    Predicates predicates = new Predicates();

    systemPredicates = createPredicates("predicates", systemPredicatesFilename); // Store a copy of the initial predicates
    predicates.contexts.addAll(createPredicates("predicates", systemPredicatesFilename).contexts);

    for (String[] arguments : args) {
        predicates.contexts.addAll(createPredicates(arguments).contexts);
    }

    if (config.getBoolean("panda.verbose")) {
        System.out.println(predicates.toString());
    }

    return new PredicateAbstraction(predicates);
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
public HeuristicListener(Config jpfConf, JPF jpf) {
  super(jpfConf, jpf);
  policiesEnabled = jpfConf.getBoolean(WorstCaseAnalyzer.ENABLE_POLICIES, WorstCaseAnalyzer.ENABLE_POLICIES_DEF);

  if (policiesEnabled) {
    PolicyManager policyManager = new PolicyManager(new File(getSerializedInputDir(jpfConf)));

    try {
      this.heuristicPolicy = policyManager.loadPolicy(measuredMethods, Policy.class);
    } catch (IOException | PolicyManagerException e) {
      logger.severe(e.getMessage());
      throw new RuntimeException(e);
    }
  }

  // Set termination strategy
  this.terminationStrategy = jpfConf.getInstance(TERMINATION_STRATEGY_CONF,
      TerminationStrategy.class, DEFAULT_TERMINATION_STRATEGY);
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
/** 
 * generates a jpf config corresponding to this configuration
 * 
 * @param conf
 * @return 
 */
public Config generateJPFConfig(Config conf) {
  Config newConf = new Config("");
  if(conf != null) {
    newConf.putAll(conf);
    newConf.setClassLoader(conf.getClassLoader());
  }
  else {
    newConf.initClassLoader(JPF.class.getClassLoader());
  }
  
  StringBuilder sb = new StringBuilder();
  boolean first = true;
  for(ConcolicMethodConfig mc : concolicMethods.values()) {
    generatePerturbConfig(mc, newConf);
    if(first)
      first = false;
    else
      sb.append(',');
    sb.append(mc.getId());
  }
  
  newConf.setProperty("perturb.params", sb.toString());
  
  return newConf;
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
/**
 * initialize object from config file
 * 
 * @param conf 
 */
private void initialize(Config conf) {
  // create a constraint solver
  ConstraintSolverFactory cFactory = new ConstraintSolverFactory(conf);
  this.solver = cFactory.createSolver(conf);
  
  // parse symbolic method info
  if(conf.hasValue(CONF_PREFIX + ".method")) {
    String id = conf.getString(CONF_PREFIX + ".method");
    ConcolicMethodConfig mc = ConcolicMethodConfig.read(id, CONF_PREFIX + ".method." + id, conf);
    registerConcolicMethod(mc);
  }
  
  // parse termination
  this.termination = parseTerminationStrategy(conf);
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
private static MethodSummary summarize(ConcolicMethodConfig mw, Config c) {
  c.setTarget("__jpf_jdart.summarizer.SummaryGenerator$Exec_" + mw.getId());
  c.setProperty("concolic.method", mw.getId());
  
  JDart jdart = new JDart(c, false);
  ConcolicExplorer cex = jdart.run();
  
  CompletedAnalysis ca = cex.getFirstCompletedAnalysis(mw.getId());
  ConstraintsTree ct = ca.getConstraintsTree();      
  MethodSummary summary = new MethodSummary(mw.getId(), ct, ca.getInitialValuation());

  c.remove("target");
  c.remove("concolic.method");
          
  return summary;
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
public File compile(Config config) throws IOException {
  JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
  StandardJavaFileManager fileManager = compiler.getStandardFileManager(null, null, null);
  fileManager.setLocation(StandardLocation.SOURCE_PATH, Collections.singleton(tmpSrcDir));
  
  File tmpClassDir = File.createTempFile("jpf-testing", "classes");
  tmpClassDir.delete();
  tmpClassDir.mkdir();
  fileManager.setLocation(StandardLocation.CLASS_OUTPUT, Collections.singleton(tmpClassDir));
  
  File[] cp = config.getPathArray("classpath");
  fileManager.setLocation(StandardLocation.CLASS_PATH, Arrays.asList(cp));
  
  CompilationTask task = compiler.getTask(null, fileManager, null, null, null, fileManager.getJavaFileObjectsFromFiles(sourceFiles));
  if(!task.call())
    throw new RuntimeException("Compilation failed");
  
  return tmpClassDir;
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
public JDartOracle(Config config, SymbolicMethodAlphabet inputs) {
  this.config = config;
  this.inputs = inputs;
  this.targetClasspath = this.config.getProperty("classpath");

  this.config.setTarget(JDartOracleTarget.class.getName());
  this.config.setProperty("concolic.method", "q__uery");
  this.config.setProperty("concolic.method.q__uery", CONCOLIC_METHOD);
  //this.config.setProperty(
  //"concolic.method.q__uery.config","all_fields_symbolic");
  this.config.setProperty("concolic.method.q__uery.config", "q__uery");
  this.config.setProperty("jdart.configs.q__uery.symbolic.include",
          ALPHABET_CLASS + ";" + ALPHABET_CLASS + ".*");
  this.config.setProperty(
          "jdart.configs.q__uery.symbolic.statics", ALPHABET_CLASS);
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
int getSysPropsFromFile (MJIEnv env){
  Config conf = env.getConfig();
  
  String cf = conf.getString("vm.sysprop.file", "system.properties");
  if (cf != null){
    try {
      Properties p = new Properties();
      FileInputStream fis = new FileInputStream(cf);
      p.load(fis);
      
      return getProperties(env, p);
      
    } catch (IOException iox){
      return MJIEnv.NULL;
    }
  }
  //.. not yet
  return MJIEnv.NULL;
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
protected GenericSharednessPolicy (Config config){
  neverBreakInMethods = MethodSpecMatcher.create( config.getStringArray("vm.shared.never_break_methods"));
  
  neverBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.never_break_types"));
  alwaysBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.always_break_types"));
  
  neverBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.never_break_fields"));
  alwaysBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.always_break_fields"));
  
  skipFinals = config.getBoolean("vm.shared.skip_finals", true);
  skipConstructedFinals = config.getBoolean("vm.shared.skip_constructed_finals", false);
  skipStaticFinals = config.getBoolean("vm.shared.skip_static_finals", true);
  skipInits = config.getBoolean("vm.shared.skip_inits", true);
  
  breakOnExposure = config.getBoolean("vm.shared.break_on_exposure", true);
  
  useSyncDetection = config.getBoolean("vm.shared.sync_detection", true);
  lockThreshold = config.getInt("vm.shared.lockthreshold", 5);  
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
public static boolean init (Config conf) {
  // this is an example of how to handle cross-initialization between
  // native peers - this might also get explicitly called by the java.lang.Class
  // peer, since it creates Constructor objects. Here we have to make sure
  // we only reset between JPF runs
  
  if (registry == null){
    registry = new MethodInfoRegistry();
    
    RunRegistry.getDefaultRegistry().addListener( new RunListener() {
      @Override
public void reset (RunRegistry reg){
        registry = null;
      }
    });
  }
  return true;
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
public BudgetChecker (Config conf, JPF jpf) {
  
  //--- get the configured budget limits (0 means not set)
  maxTime = conf.getDuration("budget.max_time", 0);
  maxHeap = conf.getMemorySize("budget.max_heap", 0);
  maxDepth = conf.getInt("budget.max_depth", 0);
  maxInsn = conf.getLong("budget.max_insn", 0);
  maxState = conf.getInt("budget.max_state", 0);
  maxNewStates = conf.getInt("budget.max_new_states", 0);
  
  tStart = System.currentTimeMillis();
  
  if (maxHeap > 0) {
    mxb = ManagementFactory.getMemoryMXBean();
    muStart = mxb.getHeapMemoryUsage();
    mStart = muStart.getUsed();
  }

  search = jpf.getSearch();
  vm = jpf.getVM();
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
@Override
public void init(Config config) {
  // these built-in come first
  appendStaticAmmendment(IgnoreConstants.instance);
  appendInstanceAmmendment(IgnoreReflectiveNames.instance);
  appendFieldAmmendment(IgnoreThreadNastiness.instance);
  appendFieldAmmendment(IgnoreUtilSilliness.instance);
  
  // ignores (e.g. NoMatch) from annotations
  IgnoresFromAnnotations ignores = new IgnoresFromAnnotations(config); 
  appendFieldAmmendment(ignores);
  appendFrameAmmendment(ignores);
  
  // configured via properties
  super.init(config);
  
  // includes (e.g. ForceMatch) from annotations
  IncludesFromAnnotations includes = new IncludesFromAnnotations(config); 
  appendFieldAmmendment(includes);
  //appendFrameAmmendment(includes);
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
protected void addToFieldWatchList (Config conf, String id){
  String keyPrefix = "perturb." + id;

  String fs = conf.getString(keyPrefix + ".field");
  if (fs != null) {
    FieldSpec fieldSpec = FieldSpec.createFieldSpec(fs);
    if (fieldSpec != null){
      Object[] args = {conf, keyPrefix};
      OperandPerturbator perturbator = conf.getInstance(keyPrefix + ".class", OperandPerturbator.class, argTypes, args);
      if (perturbator != null) {
        String loc = conf.getString(keyPrefix + ".location");
        FieldPerturbation p = new FieldPerturbation(fieldSpec, perturbator, loc);
        fieldWatchList.add(p);
      } else {
        log.warning("invalid perturbator spec for ", keyPrefix);
      }
    } else {
      log.warning("malformed field specification for ", keyPrefix);
    }

  } else {
    log.warning("missing field specification for ", keyPrefix);
  }
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
void initialize (VM vm){
  Config config = vm.getConfig();
  
  app = vm.getSUTName();
  app = app.replace("+", "__");
  app = app.replace('.', '_');

  String fname = config.getString("dot.file");
  if (fname == null){
    fname = app + ".dot";
  }

  try {
    file = new File(fname);
    FileWriter fw = new FileWriter(file);
    pw = new PrintWriter(fw);
  } catch (IOException iox){
    throw new JPFConfigException("unable to open SimpleDot output file: " + fname);
  }
  
  seenEdges = new HashSet<Long>();
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
@Override
public void propertyChanged(Config config, String key, String oldValue, String newValue) {
  // Different Config instance
  if (!config.equals(Search.this.config)) {
    return;
  }

  // Check if Search configuration changed
  if (key.startsWith("search.")){
    String k = key.substring(7);
    if ("match_depth".equals(k) ||
        "min_free".equals(k) ||
        "multiple_errors".equals(k)){
      initialize(config);
    }
  }
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
private void createVarChecks(Config conf){
  String[] checkIds = conf.getCompactTrimmedStringArray("range.vars");
  if (checkIds.length > 0){
    varChecks = new VarCheck[checkIds.length];

    for (int i = 0; i < checkIds.length; i++) {
      String id = checkIds[i];
      VarCheck check = null;
      String keyPrefix = "range." + id;
      String spec = conf.getString(keyPrefix + ".var");
      if (spec != null) {
        VarSpec vs = VarSpec.createVarSpec(spec);
        if (vs != null) {
          double min = conf.getDouble(keyPrefix + ".min", Double.MIN_VALUE);
          double max = conf.getDouble(keyPrefix + ".max", Double.MAX_VALUE);
          check = new VarCheck(vs, min, max);
        }
      }
      if (check == null) {
        throw new JPFConfigException("illegal variable range check specification for " + id);
      }
      varChecks[i] = check;
    }
  }
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
void addConfiguredPublishers (Config conf) {
  String[] def = { "console" };

  Class<?>[] argTypes = { Config.class, Reporter.class };
  Object[] args = { conf, this };

  for (String id : conf.getStringArray("report.publisher", def)){
    Publisher p = conf.getInstance("report." + id + ".class",
                                   Publisher.class, argTypes, args);
    if (p != null){
      publishers.add(p);
    } else {
      log.warning("could not instantiate publisher class: " + id);
    }
  }
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
public TraceStorer (Config config, JPF jpf){
  
  traceFileName = config.getString("trace.file", "trace");
  storeMultiple = config.getBoolean("trace.multiple", false);    
  storeDepth = config.getInt("trace.depth", Integer.MAX_VALUE);
  verbose = config.getBoolean("trace.verbose", false);
  
  terminateOnStore = config.getBoolean("trace.terminate", false);
  storeOnConstraintHit = config.getBoolean("trace.store_constraint", false);
  
  storeCalls = StringSetMatcher.getNonEmpty(config.getStringArray("trace.store_calls"));
  storeThreads = StringSetMatcher.getNonEmpty(config.getStringArray("trace.store_threads"));
  
  vm = jpf.getVM();
  search = jpf.getSearch();
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
protected void addToReturnWatchList (Config conf, String id){
  String keyPrefix = "perturb." + id;

  String ms = conf.getString(keyPrefix + ".method");
  if (ms != null) {
    MethodSpec mthSpec = MethodSpec.createMethodSpec(ms);
    if (mthSpec != null) {
      Object[] args = {conf, keyPrefix};
      OperandPerturbator perturbator = conf.getInstance(keyPrefix + ".class", OperandPerturbator.class, argTypes, args);
      if (perturbator != null) {
        String loc = conf.getString(keyPrefix + ".location");
        ReturnPerturbation p = new ReturnPerturbation(mthSpec, perturbator, loc);
        returnWatchList.add(p);
      } else {
        log.warning("invalid perturbator spec for ", keyPrefix);
      }

    } else {
      log.warning("malformed method specification for ", keyPrefix);
    }

  } else {
    log.warning("missing method specification for ", keyPrefix);
  }
}
 

import gov.nasa.jpf.Config; //导入依赖的package包/类
public CoverageAnalyzer(Config conf, JPF jpf) {
  includes = StringSetMatcher.getNonEmpty(conf.getStringArray("coverage.include"));
  excludes = StringSetMatcher.getNonEmpty(conf.getStringArray("coverage.exclude"));

  showMethods = conf.getBoolean("coverage.show_methods", false);
  showMethodBodies = conf.getBoolean("coverage.show_bodies", false);
  excludeHandlers = conf.getBoolean("coverage.exclude_handlers", false);
  showBranchCoverage = conf.getBoolean("coverage.show_branches", true);
  loadedOnly = conf.getBoolean("coverage.loaded_only", true);
  showRequirements = conf.getBoolean("coverage.show_requirements", false);

  if (!loadedOnly) {
    getCoverageCandidates(); // this might take a little while
  }

  jpf.addPublisherExtension(ConsolePublisher.class, this);
}