BinarySearchTree example for input size 100 crashes?

[charitha22]

Hi,

My name is Charitha Saumya. I am PhD student in Computer engineering department at Purdue university.

I've been trying out your spf-wca tool.

When I try to run the tool for BinarySearchTree example for input size 100, It gives me the following error.

[INFO] Exploring with heuristic input size 100...
symbolic.min_int=-100
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=100
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=4.9E-324
symbolic.max_double=1.7976931348623157E308
Exception in thread "main" wcanalysis.WCAException: jpf-core threw exception
at wcanalysis.WorstCaseAnalyzer.runJPF(WorstCaseAnalyzer.java:273)
at wcanalysis.WorstCaseAnalyzer.performAnalysis(WorstCaseAnalyzer.java:252)
at wcanalysis.WorstCaseAnalyzer.start(WorstCaseAnalyzer.java:144)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:108)
Caused by: gov.nasa.jpf.JPFListenerException: exception during searchFinished() notification
at gov.nasa.jpf.search.Search.notifySearchFinished(Search.java:572)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:110)
at gov.nasa.jpf.JPF.run(JPF.java:613)
at wcanalysis.WorstCaseAnalyzer.runJPF(WorstCaseAnalyzer.java:271)
... 3 more
Caused by: java.lang.StackOverflowError
at java.lang.StringBuilder.append(StringBuilder.java:136)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:194)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:196)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:196)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:196)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:196)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:196)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:196)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:196)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:196)
at gov.nasa.jpf.symbc.numeric.Constraint.prefix_notation(Constraint.java:196)

I wanted to run the tool for specific input size in phase 2. So edited the .jpf file as follows. (used the "startat" config)

@using spf-wca

shell=wcanalysis.WorstCaseAnalyzer

symbolic.min_int=-100
symbolic.max_int=100
symbolic.dp=z3

target=wise.BinaryTreeSearch

symbolic.wc.policy.history.size=0

symbolic.worstcase.policy.inputsize=3
symbolic.worstcase.input.max=100

symbolic.worstcase.startat=100
symbolic.worstcase.verbose=true
symbolic.worstcase.outputpath=${spf-wca}/binary_tree_search_results

symbolic.method=benchmarks.BinaryTreeSearch$BinaryTree.search(con);benchmarks.BinaryTreeSearch$BinaryTree.insert(con)
symbolic.heuristic.measuredmethods=benchmarks.BinaryTreeSearch$BinaryTree.search(con)

Tool runs perfectly fine for scales 10,20,40,50 .. but for 100 it crashes. Can you suggest a fix for this.

Thanks,

Charitha