import gov.nasa.jpf.JPF; //导入依赖的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.JPF; //导入依赖的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.JPF; //导入依赖的package包/类
@MJI
public static void log__Ljava_lang_String_2ILjava_lang_String_2_3Ljava_lang_Object_2__V (MJIEnv env, int clsObjRef,
    int loggerIdRef, int logLevel, int fmtRef, int argsRef){
  String loggerId = env.getStringObject(loggerIdRef);
  String fmt = env.getStringObject(fmtRef);
  JPFLogger logger = JPF.getLogger(loggerId);

  int[] argRefs = env.getReferenceArrayObject( argsRef);
  Object[] args = new Object[argRefs.length];
  for (int i=0; i<args.length; i++){
    ElementInfo eiArg = env.getElementInfo(argRefs[i]);
    if (eiArg.isStringObject()){
      args[i] = env.getStringObject(argRefs[i]);
    } else if (eiArg.isBoxObject()){
      args[i] = eiArg.asBoxObject(); 
    } else {
      args[i] = eiArg.toString();
    }
  }
  
  String msg = String.format(fmt, args);
  
  log( logger, logLevel, msg);
}
 

import gov.nasa.jpf.JPF; //导入依赖的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);
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
public PathOutputMonitor (Config config, JPF jpf) {
  vm = jpf.getVM();
  vm.storePathOutput();
  
  jpf.addPublisherExtension(ConsolePublisher.class, this);
  
  printOutput = config.getBoolean("pom.print_output", true);
  deferOutput = config.getBoolean("pom.defer_output", true);

  psClass = config.getClass("pom.output_spec.class", PathOutputSpec.class);

  if (psClass == null) {
    psClass = RegexOutputSpec.class;
  }
  
  anySpecs = loadSpecs(config, "pom.any");
  allSpecs = loadSpecs(config, "pom.all");
  noneSpecs = loadSpecs(config, "pom.none");
  
  violatedSpecs = new ArrayList<PathOutputSpec>();
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
public SimpleDot( Config config, JPF jpf){

    graphAttrs = config.getString("dot.graph_attr", GRAPH_ATTRS);
    genericNodeAttrs = config.getString("dot.node_attr", GENERIC_NODE_ATTRS);
    genericEdgeAttrs = config.getString("dot.edge_attr", GENERIC_EDGE_ATTRS);
    newEdgeAttrs = config.getString("dot.new_edge_attr", NEW_EDGE_ATTRS);
    visitedEdgeAttrs = config.getString("dot.visited_edge_attr", VISITED_EDGE_ATTRS);
    startNodeAttrs = config.getString("dot.start_node_attr", START_NODE_ATTRS);
    endNodeAttrs = config.getString("dot.end_node_attr", END_NODE_ATTRS);
    errorNodeAttrs = config.getString("dot.error_node_attr", ERROR_NODE_ATTRS);
    backtrackEdgeAttrs = config.getString("dot.bt_edge_attr", BACKTRACK_EDGE_ATTRS);
    restoreEdgeAttrs = config.getString("dot.restore_edge_attr", RESTORED_EDGE_ATTRS);

    printFile = config.getBoolean("dot.print_file", false);
    showTarget = config.getBoolean("dot.show_target", false);

    // app and filename are not known until the search is started
    
    jpf.addPublisherExtension(ConsolePublisher.class, this);
  }
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
public ChoiceTracker (Config config, JPF jpf) {
  this.config = config;
  vm = jpf.getVM();
  search = jpf.getSearch();
  
  String fname = config.getString("choice.trace");
  if (fname == null) {
    isReportExtension = true;
    jpf.addPublisherExtension(ConsolePublisher.class, this);
    // pw is going to be set later
  } else {
    try {
      pw = new PrintWriter(fname);
    } catch (FileNotFoundException fnfx) {
      System.err.println("cannot write choice trace to file: " + fname);
      pw = new PrintWriter(System.out);
    }
  }
  
  excludes = config.getStringArray("choice.exclude");
  cgClasses = config.getClasses("choice.class");

  format = config.getEnum("choice.format", Format.values(), Format.CG);
  showLocation = config.getBoolean("choice.show_location", true);
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
public ObjectTracker (Config conf, JPF jpf) {
  includeClasses = StringSetMatcher.getNonEmpty(conf.getStringArray("ot.include"));
  excludeClasses = StringSetMatcher.getNonEmpty(conf.getStringArray("ot.exclude", new String[] { "*" }));

  trackedRefs = new SortedArrayIntSet();
  
  int[] refs = conf.getIntArray("ot.refs");
  if (refs != null){
    for (int i=0; i<refs.length; i++){
      trackedRefs.add(refs[i]);
    }
  }
  
  logCalls = conf.getBoolean("ot.log_calls", true);
  logFieldAccess = conf.getBoolean("ot.log_fields", true);
  
  registerListener(jpf);
  jpf.addPublisherExtension(ConsolePublisher.class, this);
}
 

import gov.nasa.jpf.JPF; //导入依赖的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.JPF; //导入依赖的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.JPF; //导入依赖的package包/类
protected String getRevision() {
  try {
    InputStream is = JPF.class.getResourceAsStream(".version");
    if (is != null){
      int len = is.available();
      byte[] data = new byte[len];
      is.read(data);
      is.close();
      return new String(data).trim();
      
    } else {
      return null;
    }
    
  } catch (Throwable t){
    return null;
  }
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
protected String getRepositoryInfo() {
  try {
    InputStream is = JPF.class.getResourceAsStream("build.properties");
    if (is != null){
      Properties revInfo = new Properties();
      revInfo.load(is);

      StringBuffer sb = new StringBuffer();
      String date = revInfo.getProperty("date");
      String author = revInfo.getProperty("author");
      String rev = revInfo.getProperty("rev");
      String machine = revInfo.getProperty("hostname");
      String loc = revInfo.getProperty("location");
      String upstream = revInfo.getProperty("upstream");

      return String.format("%s %s %s %s %s", date,author,rev,machine,loc);
    }
  } catch (IOException iox) {
    return null;
  }

  return null;
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
/**
 * run JPF expecting no SuT property violations 
 */
protected JPF noPropertyViolation (StackTraceElement testMethod, String... args) {
  JPF jpf = null;

  report(args);

  try {
    jpf = createAndRunJPF( testMethod, args);
  } catch (Throwable t) {
    // we get as much as one little hickup and we declare it failed
    t.printStackTrace();
    fail("JPF internal exception executing: ", args, t.toString());
    return jpf;
  }

  List<Error> errors = jpf.getSearchErrors();
  if ((errors != null) && (errors.size() > 0)) {
    fail("JPF found unexpected errors: " + (errors.get(0)).getDescription());
  }

  return jpf;
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
/**
 * run JPF expecting it to throw an exception
 * NOTE - xClassName needs to be the concrete exception, not a super class
 * @param args JPF main() arguments
 */
protected JPF jpfException (StackTraceElement testMethod, Class<? extends Throwable> xCls, String... args) {
  JPF jpf = null;
  Throwable exception = null;

  report(args);

  try {
    jpf = createAndRunJPF( testMethod, args);
  } catch (JPF.ExitException xx) {
    exception = xx.getCause();
  } catch (Throwable x) {
    exception = x;
  }

  if (exception != null){
    if (!xCls.isAssignableFrom(exception.getClass())){
      fail("JPF produced wrong exception: " + exception + ", expected: " + xCls.getName());
    }
  } else {
    fail("JPF failed to produce exception, expected: " + xCls.getName());
  }

  return jpf;
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
/**
 * run JPF expecting a property violation of the SuT
 * @param args JPF main() arguments
 */
protected JPF propertyViolation (StackTraceElement testMethod, Class<? extends Property> propertyCls, String... args ){
  JPF jpf = null;

  report(args);

  try {
    jpf = createAndRunJPF( testMethod, args);
  } catch (Throwable t) {
    t.printStackTrace();
    fail("JPF internal exception executing: ", args, t.toString());
  }

  List<Error> errors = jpf.getSearchErrors();
  if (errors != null) {
    for (Error e : errors) {
      if (propertyCls == e.getProperty().getClass()) {
        return jpf; // success, we got the sucker
      }
    }
  }

  fail("JPF failed to detect error: " + propertyCls.getName());
  return jpf;
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
public String getJPFBanner () {
  StringBuilder sb = new StringBuilder();
  
  sb.append("JavaPathfinder core system v");
  sb.append(JPF.VERSION);
  
  String rev = getRevision();
  if (rev != null){
    sb.append(" (rev ");
    sb.append(rev);
    sb.append(')');
  }
  
  sb.append(" - (C) 2005-2014 United States Government. All rights reserved.");
  
  if (conf.getBoolean("report.show_repository", false)) {
    String repInfo =  getRepositoryInfo();
    if (repInfo != null) {
      sb.append( repInfo);
    }
  }
  
  return sb.toString();
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
private DataCollection performAnalysis(Config jpfConf) {
  boolean noSolver = jpfConf.getBoolean(NO_SOLVER_HEURISTIC_CONF, false);
  if (noSolver) {
    jpfConf.setProperty("symbolic.dp", "no_solver");
  }
  int maxInput = jpfConf.getInt(MAX_INPUT_CONF);
  jpfConf.setProperty("report.console.class", HeuristicResultsPublisher.class.getName());

  DataCollection dataCollection = new DataCollection();

  for (int inputSize = this.startAt; inputSize <= maxInput; inputSize += this.incr) {//TODO: should maxInput be included?
    logger.info("Exploring with heuristic input size " + inputSize + "...");
    jpfConf.setProperty("target.args", "" + inputSize);
    JPF jpf = new JPF(jpfConf);
    HeuristicListener heuristic = new HeuristicListener(jpfConf, jpf);
    jpf.addListener(heuristic); //weird instantiation...

    //explore guided by policy
    long start = System.currentTimeMillis();
    runJPF(jpf);
    long end = System.currentTimeMillis();

    logger.info("Heuristic exploration at input size " + inputSize + " done. Took " + ((end - start) / 1000) + "s");

    WorstCasePath wcPath = heuristic.getWcPath();

    if (wcPath == null) {
      logger.severe("No worst case path found for input size " + inputSize);
    } else {
      State wcState = wcPath.getWCState();
      dataCollection.addDatapoint(inputSize, wcState.getWC());
    }
  }
  return dataCollection;
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
private void runJPF(JPF jpf) {
  try {
    jpf.run();
  } catch (Exception e) {
    throw new WCAException("jpf-core threw exception", e);
  }
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
@Override
public void start(String[] args) {
  this.conf.setProperty("report.console.class", PolicyResultsPublisher.class.getName());
  for(int i = this.from; i <= this.to; i++) {
    this.conf.setProperty("target.args", ""+i);
    JPF jpf = new JPF(this.conf);
    jpf.addListener(new PolicyGeneratorListener(this.conf, jpf)); //weird instantiation...
    //get policy
    jpf.run();
  }
}
 

import gov.nasa.jpf.JPF; //导入依赖的package包/类
/**
 * Constructor. Initializes JDart from a JPF config only.
 *
 * @param conf the JPF config
 */
public JDart(Config conf) {
  //this(conf, true);
  // due to some bug the log manager has to be initialized first.
  LogManager.init(conf);
  this.config = conf;
  this.cc = new ConcolicConfig(conf);
  logger = JPF.getLogger("jdart");
}