vaibhavbsharma / jpf-symbc-veritesting Goto Github PK

In the below test case, cfg changes significantly once we add assert and support "new" object instruction.

public int assertRegions(boolean x, boolean y) {
int a = 0;
int b = a;
if (x) {
a = a+3;
} else {
a = a+2;
}
assert(x? a == 3 : a==2);
return a;
}

I am trying to run tcas.jpf and I got an assertion error on line 262 in the MyIVisitor.
instruction.getNumberOfUses() is actually equal to 0 not 1.
the instruction is " 5 = getstatic < Application, Ltcas, Alt_Layer_Value, <Primordial,I> >"
output and stack here

/Library/Java/JavaVirtualMachines/jdk1.8.0_131.jdk/Contents/Home/bin/java -Djava.library.path=/Users/sohanabel/git/veritesting/jpf-symbc-veritesting/lib -Xmx1024m -ea -Dfile.encoding=UTF-8 -jar /Users/sohanabel/git/veritesting/jpf-core-veritesting/build/RunJPF.jar /Users/sohanabel/git/veritesting/benchmarks/tcas/src/tcas.jpf
symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
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
JavaPathfinder core system v8.0 - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
tcas.main()

====================================================== search started: 1/9/18 3:20 PM
could not resolve < Application, Ltcas, main([LString;)V >
Starting analysis for initialize(tcas.initialize()V)
Starting doAnalysis
Starting analysis for ALIM(tcas.ALIM()I)
Starting doAnalysis
java.lang.AssertionError
at gov.nasa.jpf.symbc.veritesting.MyIVisitor.visitGet(MyIVisitor.java:262)
at com.ibm.wala.ssa.SSAGetInstruction.visit(SSAGetInstruction.java:56)
at gov.nasa.jpf.symbc.veritesting.VeritestingMain.doAnalysis(VeritestingMain.java:268)
at gov.nasa.jpf.symbc.veritesting.VeritestingMain.startAnalysis(VeritestingMain.java:128)
at gov.nasa.jpf.symbc.veritesting.VeritestingMain.analyzeForVeritesting(VeritestingMain.java:92)
at gov.nasa.jpf.symbc.VeritestingListener.executeInstruction(VeritestingListener.java:115)
at gov.nasa.jpf.vm.VM.notifyExecuteInstruction(VM.java:793)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1904)
at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
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.JPF.start(JPF.java:189)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:498)
at gov.nasa.jpf.tool.Run.call(Run.java:80)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during executeInstruction() notification
at gov.nasa.jpf.vm.VM.notifyExecuteInstruction(VM.java:800)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1904)
at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
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.JPF.start(JPF.java:189)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:498)
at gov.nasa.jpf.tool.Run.call(Run.java:80)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
Caused by: java.lang.AssertionError
at gov.nasa.jpf.symbc.veritesting.MyIVisitor.visitGet(MyIVisitor.java:262)
at com.ibm.wala.ssa.SSAGetInstruction.visit(SSAGetInstruction.java:56)
at gov.nasa.jpf.symbc.veritesting.VeritestingMain.doAnalysis(VeritestingMain.java:268)
at gov.nasa.jpf.symbc.veritesting.VeritestingMain.startAnalysis(VeritestingMain.java:128)
at gov.nasa.jpf.symbc.veritesting.VeritestingMain.analyzeForVeritesting(VeritestingMain.java:92)
at gov.nasa.jpf.symbc.VeritestingListener.executeInstruction(VeritestingListener.java:115)
at gov.nasa.jpf.vm.VM.notifyExecuteInstruction(VM.java:793)
... 14 more
SSAGetInstruction = 5 = getstatic < Application, Ltcas, Alt_Layer_Value, <Primordial,I> >
[SEVERE] JPF exception, terminating: exception during executeInstruction() notification

Process finished with exit code 0

The contents of the tcas.jpf file is
target=tcas
classpath=/Users/sohanabel/git/veritesting/benchmarks/tcas/bin
sourcepath=/Users/sohanabel/git/veritesting/benchmarks/tcas/src
symbolic.method = tcas.mainProcess(sym#sym#sym#sym#sym#sym#sym#sym#sym#sym#sym#sym)
symbolic.minint=-100
symbolic.maxint=100
vm.storage.class=nil
listener = .symbc.VeritestingListener
symbolic.dp=z3bitvector
#listener = .listener.ChoiceTracker

For this test case a region is created when it should not.

public int createObjectComplexRegionTC7(boolean x, boolean y) {
int a = 0;
if (new TempClass3(true).valid) {
a = 1;
if (x) {
a = 3;
} else {
a = 2;
}
}
return a;
}

Same for this test case as well:

public int branchOnConcrete(boolean x, boolean y) {
int a = 0;
if (new TempClass3(true).valid) {
a = 3;
} else {
a = 2;
}
return a;
}

line number 134 in VeritestingListener returns null symbolic variable. The actual exception is thrown at the assert statement in line 78 in PCParser.java.

WBS.jpf file is configured as
target=WBS
classpath=${jpf-symbc}/build/examples
sourcepath=${jpf-symbc}/src/examples
symbolic.method = WBS.launch(sym#sym#sym#sym#sym#sym#con#con#con)
symbolic.minint=-100
symbolic.maxint=100
vm.storage.class=nil
listener = .symbc.VeritestingListener
symbolic.dp=z3bitvector
#listener = .listener.ChoiceTracker

Output and trace is

/Library/Java/JavaVirtualMachines/jdk1.8.0_131.jdk/Contents/Home/bin/java -Djava.library.path=/Users/sohanabel/git/veritesting/jpf-symbc-veritesting/lib -Xmx1024m -ea -Dfile.encoding=UTF-8 -jar /Users/sohanabel/git/veritesting/jpf-core-veritesting/build/RunJPF.jar /Users/sohanabel/git/veritesting/jpf-symbc-veritesting/src/examples/WBS.jpf
symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
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
JavaPathfinder core system v8.0 - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
WBS.main()

====================================================== search started: 1/9/18 2:36 PM
could not resolve < Application, LWBS, main([LString;)V >
Starting analysis for update(WBS.update(IZZ)V)
Starting doAnalysis
SSAGotoInstruction = goto (from iindex= 13 to iindex = 15)
SSAPhiInstruction = 11 = phi 10,9

SSAConditionalBranchInstruction = conditional branch(ne, to iindex=28) 2,10

SSAConditionalBranchInstruction = conditional branch(eq, to iindex=57) 11,9

SSAConditionalBranchInstruction = conditional branch(ne, to iindex=73) 11,9

SSAConditionalBranchInstruction = conditional branch(eq, to iindex=84) 4,9

SSAGotoInstruction = goto (from iindex= 94 to iindex = 97)
SSAPhiInstruction = 20 = phi 9,19

SSAGotoInstruction = goto (from iindex= 102 to iindex = 105)
SSAPhiInstruction = 21 = phi 9,19

SSAConditionalBranchInstruction = conditional branch(lt, to iindex=117) 21,10

SSAConditionalBranchInstruction = conditional branch(ne, to iindex=133) 18,10

SSABinaryOpInstruction = 28 = binaryop(add) 16 , 15
SSAGotoInstruction = goto (from iindex= 164 to iindex = 169)
SSAPhiInstruction = 29 = phi 9,28

SSAPutInstruction = putfield 1.< Application, LWBS, Sys_Mode, <Primordial,I> > = 9
SSAPutInstruction = putfield 1.< Application, LWBS, Sys_Mode, <Primordial,I> > = 10
SSAGotoInstruction = goto (from iindex= 175 to iindex = 179)
SSAConditionalBranchInstruction = conditional branch(eq, to iindex=185) 17,9

SSAConditionalBranchInstruction = conditional branch(lt, to iindex=194) 29,9

SSAGotoInstruction = goto (from iindex= 228 to iindex = 231)
SSAPhiInstruction = 31 = phi 20,9

SSAConditionalBranchInstruction = conditional branch(ne, to iindex=247) 30,10

SSAConditionalBranchInstruction = conditional branch(ne, to iindex=293) 15,10

Starting analysis for launch(WBS.launch(IZZIZZIZZ)V)
Starting doAnalysis
Number of veritesting regions = 6
veritesting analysis took 413 milliseconds
[SEVERE] JPF exception, terminating: exception during executeInstruction() notification
java.lang.AssertionError
at gov.nasa.jpf.symbc.numeric.PCParser.getExpression(PCParser.java:78)
at gov.nasa.jpf.symbc.numeric.PCParser.createDPNonLinearIntegerConstraint(PCParser.java:934)
at gov.nasa.jpf.symbc.numeric.PCParser.addConstraint(PCParser.java:1087)
at gov.nasa.jpf.symbc.numeric.PCParser.parse(PCParser.java:1054)
at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.isSatisfiable(SymbolicConstraintsGeneral.java:135)
at gov.nasa.jpf.symbc.numeric.PathCondition.simplifyOld(PathCondition.java:475)
at gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:352)
at gov.nasa.jpf.symbc.VeritestingListener.executeInstruction(VeritestingListener.java:137)
at gov.nasa.jpf.vm.VM.notifyExecuteInstruction(VM.java:793)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1904)
at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
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.JPF.start(JPF.java:189)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:498)
at gov.nasa.jpf.tool.Run.call(Run.java:80)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during executeInstruction() notification
at gov.nasa.jpf.vm.VM.notifyExecuteInstruction(VM.java:800)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1904)
at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
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.JPF.start(JPF.java:189)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:498)
at gov.nasa.jpf.tool.Run.call(Run.java:80)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
Caused by: java.lang.AssertionError
at gov.nasa.jpf.symbc.numeric.PCParser.getExpression(PCParser.java:78)
at gov.nasa.jpf.symbc.numeric.PCParser.createDPNonLinearIntegerConstraint(PCParser.java:934)
at gov.nasa.jpf.symbc.numeric.PCParser.addConstraint(PCParser.java:1087)
at gov.nasa.jpf.symbc.numeric.PCParser.parse(PCParser.java:1054)
at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.isSatisfiable(SymbolicConstraintsGeneral.java:135)
at gov.nasa.jpf.symbc.numeric.PathCondition.simplifyOld(PathCondition.java:475)
at gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:352)
at gov.nasa.jpf.symbc.VeritestingListener.executeInstruction(VeritestingListener.java:137)
at gov.nasa.jpf.vm.VM.notifyExecuteInstruction(VM.java:793)
... 14 more

Process finished with exit code 0