max_depth does not work?

[chenbihuan]

Hello,

I felt confused about the configuration option max_depth.

According to WiKi, the resulting constraints tree will in no case be deeper than max_depth. In the implementation, however, it seems max_depth is just ignored during the construction of constraints tree.

if(anaConf.maxDepthExceeded(current.depth)) {
      //System.err.println("DEPTH EXCEEDED");
      return BranchEffect.NORMAL; // just ignore it
 }

Alternatively, max_depth is used when finding the next valuation, i.e., skipping the node that is deeper than the max_depth.

if(anaConf.maxAltDepthExceeded(ad) || anaConf.maxDepthExceeded(currentTarget.depth)) {
      currentTarget.dontKnow();
      continue;
}

As a result, the construction of constraints tree can be get stuck for programs that have deep loops. For example, the iteration of a loop may depend on an input that could be 100,000,000.

for (int i = 0; i < n; i++) {
      ...
}

Am I understanding the implementation correctly? Any ideas of avoiding the "stuck" in such cases?

Thank you. Bihuan

[ksluckow]

Hi Bihuan,

The max_depth configuration will limit the depth of the constraints tree. If you look in the method that contains the condition you mention:

if(anaConf.maxDepthExceeded(current.depth)) {
  //System.err.println("DEPTH EXCEEDED");
  return BranchEffect.NORMAL; // just ignore it
}

DecisionData data;
try {
  if(!current.hasDecisionData())
    data = new DecisionData(current, insn, decisions, explore);
  else {
    data = current.decisionData();
    data.verifyDecision(insn, decisions);
  }

  current.setDecision(data);
}  catch(IllegalStateException e) {
//...
}

then it will simply return and not add a node to the constraints tree if max_depth is exceeded. If the max depth is not exceeded then a new DecisionData is constructed and added to the tree.

Regarding your second question: To cut off the exploration depth in cases like you mention (or simply for cases with while(true) {...}), we rely on the jpf-core config:

search.depth_limit

Hope it helps.

Kasper

[chenbihuan]

Hi Kasper,

Thank you for your reply.

Setting search.depth_limit does not work. It seems one path in the constraints tree is constructed within one invocation of vm.forward(), thus depth in the search class is not increased as more branches are explored.

As a result, for programs with deep loops, jdart could be stuck by keeping invoking the decision(...) method although it does not create any new DecisionData.

Any suggestions to avoid invoking that method when reaching the max_depth? Otherwise, it will be too slow (e.g., a path does not finish in 15 hours in one of my cases) to use concolic execution.

Thanks and Regards, Bihuan

[ksluckow]

Hi Bihuan,

Thanks for clarifying! It is true that jpf does not advance the state, because the constraints tree is a separate data structure that is maintained manually; not by JPF choice generators. I could explain more about why this is so, but let's stick to the topic :)

What you want to do is currently not possible, but I think it is not hard to add that feature -- we should do it.

Let me sketch the solution:

1. Create a JPF-listener (or possibly add to ConcolicListener) that listens on the executeInstruction event.
2. Obtain the current node in the constraints tree (class InternalConstraintsTree).
3. Test whether its depth is greater than the bound specified in the analysis config.
4. If it is, ignore the state (method VM.ignoreState())
5. Otherwise, continue

A crude implementation of the above (in ConcolicListener) could be the following:

@Override
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
  ConcolicMethodExplorer ca = ConcolicMethodExplorer.getCurrentAnalysis(ti);
  if(ca == null)
    return;
  InternalConstraintsTree tree = ca.getInternalConstraintsTree();
  if(anaConf.maxDepthExceeded(tree.current.getDepth())) {
    vm.ignoreState();
  }
}

I will think a bit about how it can be better integrated, but for now, I think the above works. You will have to obtain a reference to the AnalysisConfig (i.e. anaConf) and change the visibility of the current node in the constraints tree.

[chenbihuan]

Hi Kasper,

Thanks for the solution. I cannot try that now due to a strange problem.

JDart suddenly failed to work due to the following exception.

Exception in thread "main" java.lang.NoSuchMethodError: org.opt4j.start.Opt4JTask.<init>(ZLcoral/solvers/Solver$Guard;)V
    at coral.solvers.search.opt4j.pso.PSOSolver.call(PSOSolver.java:89)
    at coral.solvers.search.opt4j.pso.PSOSolver.call(PSOSolver.java:243)
    at coral.solvers.Solver.call(Solver.java:241)
    at coral.solvers.Solver$1.call(Solver.java:100)
    at coral.solvers.Solver$1.call(Solver.java:1)
    at gov.nasa.jpf.constraints.solvers.coral.CoralSolver.solve(CoralSolver.java:153)
    at gov.nasa.jpf.constraints.solvers.coral.CoralSolverContext.solve(CoralSolverContext.java:66)
    at gov.nasa.jpf.jdart.constraints.InternalConstraintsTree.findNext(InternalConstraintsTree.java:478)
    at gov.nasa.jpf.jdart.ConcolicMethodExplorer.hasMoreChoices(ConcolicMethodExplorer.java:206)
    at gov.nasa.jpf.jdart.ConcolicExplorer.hasMoreChoices(ConcolicExplorer.java:206)
    at gov.nasa.jpf.jdart.JDartChoiceGenerator.hasMoreChoices(JDartChoiceGenerator.java:64)
    at gov.nasa.jpf.vm.SystemState.advanceCurCg(SystemState.java:883)
    at gov.nasa.jpf.vm.SystemState.initializeNextTransition(SystemState.java:745)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1709)
    at gov.nasa.jpf.search.Search.forward(Search.java:579)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.jdart.JDart.run(JDart.java:207)
    at gov.nasa.jpf.jdart.JDart.start(JDart.java:131)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:108)

The coral solver passed all the tests when doing maven install. But it just didn't work with JDart. It seems opt4j only has the method org.opt4j.start.Opt4JTask.(Z)V. Since I do not have the source code of coral, I do not know why it calls the not-found method. Any clues about this?

Thank you. Bihuan

[ksluckow]

I don't think I have seen that before. Can you provide an MWE?

[chenbihuan]

Hi Kasper,

I have tested your suggested solution, and it works. Thanks for your great help.

I have also fixed the NoSuchMethodError bug. It turned out that, both coral.jar and opt4j-2.2.jar are in the classpath and contain the class Opt4JTask, but their construction methods have different parameters. Actually, the Opt4JTask from coral.jar is the right class to be loaded; but instead, the Opt4JTask from opt4j-2.2.jar is accidentally loaded and thus a NoSuchMethodError is thrown. According to JVM's class loading mechanism, if two jars contain the same class, this class will be loaded from the jar that appears first in the classpath. This means, if coral.jar is loaded before opt4j-2.2.jar, everything works fine (as in my old computer); and if opt4j-2.2.jar is loaded before coral.jar, a NoSuchMethodError is thrown (as in my new computer).

After diving into the implementation details of jconstraints, I found that this bug results from the method addJARS(...) in the class ExtensionLoader. It uses File.listFiles to load the jars (including coral.jar and opt4j-2.2.jar) from the extensions folder. As indicated by javadoc, however, for File.listFiles, there is no guarantee that the name strings in the resulting array will appear in any specific order; they are not, in particular, guaranteed to appear in alphabetical order.

private static void addJARs(File directory, List<File> jarList) {
    ...
    Collections.addAll(jarList, directory.listFiles(JAR_FILTER));
}

To fix this bug, my simple solution is to sort the listed jars before adding to jarList to ensure that coral.jar is definitely loaded before opt4j-2.2.jar.

private static void addJARs(File directory, List<File> jarList) {
    ...
    File[] files = directory.listFiles(JAR_FILTER);
    java.util.Arrays.sort(files);
    Collections.addAll(jarList, files);
}

Best wishes, Bihuan

[ksluckow]

Hi Bihuan,

Great you got it working! I'll probably add the feature for limited path exploration this week.

Also great you got coral working! :) Now that you mention the problem, I think I had similar issues some time ago. While sorting the files in this particular case solves the problem, it doesn't solve the more general problem of classpath conflicts. One way of partly solving the problem could be to monitor the classes being loaded by jconstraints, and issue warnings if classpath conflicts arise. In that case, we could resort to a manual (or semi-automatic) classpath setup by, e.g., priority-assignment to the entries.

Cheers, Kasper