Results from the last SVComp shows that JR has raised null pointer exception when running on apachicli_eqchk. This resulted in us producing unknown result.

the stack trace is below

`region summary single path optimization applied.
UnrecognizedOptionException: Unrecognized option:
at Parser.processOption(Parser.java:455)
at Parser.parse(Parser.java:208)
at Parser.parse(Parser.java:109)
at CLI.execute(CLI.java:75)
at CLI.mainProcess(CLI.java:65)
at Main.runCLI(Main.java:8)
at Main.testFunction(Main.java:21)
at TestCLI.JRWrapper(TestCLI.java:30)
at TestCLI.testHarness(TestCLI.java:18)
at TestCLI.runTest(TestCLI.java:34)
at Main.main(Main.java:16)
stateAdvanced

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NullPointerException: Calling 'equals(Ljava/lang/Object;)Z' on null object
at TestCLI.testHarness(TestCLI.java:19)
at TestCLI.runTest(TestCLI.java:34)
at Main.main(Main.java:16)

====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
call stack:
at TestCLI.testHarness(TestCLI.java:19)
at TestCLI.runTest(TestCLI.java:34)
at Main.main(Main.java:16)

====================================================== VeritestingListener report:

/************************ Printing Exception Statistics *****************
Static Analysis exceptions count = 63
Instantiation Time exceptions count = 2255
Unknown phases exception count = 490
FindStructuredBlockEndNode: mal-formed region: (51, StaticAnalysisPhase)
cannot make ArrayRef for symbolic array reference: (1760, InstantiationPhase)
region contains condition that cannot be instantiated: (6, StaticAnalysisPhase)
createComplexIfCondition: unconditional branch (continue or break): (3, StaticAnalysisPhase)
trying to compose with two null statements: (490, Unknown phase)
out of bounds array access in ArrayExpressions: (490, InstantiationPhase)
region instantiation is not beneficial (2,2): (5, InstantiationPhase)
Untranslatable instruction in SSAToStatIVisitor: (3, StaticAnalysisPhase)

/************************ Printing Time Decomposition Statistics *****************
static analysis time = 1909 msec
Veritesting Dyn Time = 20516 msec
Veritesting fix-point Time = 0 msec

/************************ Printing Solver Statistics *****************
Total Solver Queries Count = 4209
Total Solver Time = 6767 msec
Total Solver Parse Time = 1054 msec
Region Summary Parse Time = 0 msec
Total Solver Clean up Time = 550 msec
PCSatSolverCount = 119
PCSatSolverTime = 2320 msec
Constant Propagation Time for PC sat. checks = 2
Array SPF Case count = 194
If-removed count = 200

/************************ Printing Region Statistics *****************
Number of Distinct Veritested Regions = 5
Number of Distinct Un-Veritested Symbolic Regions = 10
Number of Distinct Failed Regions for Field Reference = 0
Number of Distinct Failed Regions for SPFCases = 0
Number of Distinct Failed Regions for missing method summaries = 1
Number of Distinct Failed Regions for Other Reasons = 9
Number of High Order Regions Used = 0

/************************ Printing Instantiation Statistics *****************
Number of successful instantiations = 119
Total Number of unsuccessful instantiations = 496
Number of failed instantiations due to Field Reference = 0
Number of failed instantiations due to SPFCases = 0
Number of failed instantiations due to missing method summaries = 1
Number of failed instantiations due to Other Reasons = 495

Number of Veritested Regions Instances = 119
Printing keys of regions that were instantiated at least once
Options.shortOptsContain(C)Z#28
Options.shortOptsContain(C)Z#34
Options.shortOptsContain_get(C)Z#28
Options.shortOptsContain_get(C)Z#34
Parser.parse(LOptions;[[CLjava/util/Properties;Z)LCommandLine;#315
Finished printing keys of regions that were instantiated at least once

Metrics Vector:
22425,1909,20516,151,4209,6767,1054,550,5,10,0,0,0,1,9,0,15,119,496,0,0,0,1,495,42364,17334,6,10,2.215384615384615,63,2255,490

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NullPointerException: Calling 'equals(Lj..."

====================================================== statistics
elapsed time: 00:00:22
states: new=314,visited=0,backtracked=302,end=151
search: maxDepth=13,constraints=6
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=159
heap: new=69570,released=85542,maxLive=614,gcCycles=308
instructions: 3929002
max memory: 654MB
loaded code: classes=102,methods=2123

====================================================== search finished: 11/30/19 5:11 AM
UNKNOWN`

Something is going wrong with WBS in JR mode when running it with 3 steps. This is happening for both the guiding and the collect modes. Basically more test cases are generated than possible since they are more than the total number of obligations in WBS.

I am observing behavior difference when running z3inc and z3bitvectorinc on the following code:

public int testERInline(boolean a, int x) {
        int z = 0;
        if (a)
            z = testingER1(a, x);
        return z;
    }

    private int testingER1(boolean a, int x) {
        int z = 1;
        if (x > 2) {
            return z;
        }

        this.sideEffect = 5;

        z++;


        return z;
    }

Running the above with

listener =.symbc.BranchListener,gov.nasa.jpf.symbc.sequences.ThreadSymbolicSequenceListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener
coverageMode=3

with the z3incvector turned on, throws an exception due to the non-existence of an object in the solver query. The same behavior is not noticed when using z3inc. I need to understand the difference in behavior and tune TCG for the bitvector mode.

To do

1. Figure out the last place where SPF got stuck when trying to solve symbolic string constraints.
2. Submit another changes-to-SPF pull request to upstream SPF.
3. Improve documentation on installation instructions, why we're duplicating SPF inside this repository, how the TARGET_CLASSPATH_WALA needs to be set up
4. What types does Java Ranger support? What types does it not support? When does it incur loss of precision due to translation of a longer type (Long) in SPF into a shorter type (Integer) in Green?
5. Logging in JR sucks. Implement it so that it is easy to turn off all the logging statements.
6. Figure out a way to warn the user that they have run into silent concretization/loss of symbolic state.
7. Add debugging APIs so that users can view the symbolic expression at a certain program location.
8. tutorial walk through, ideally a sequence of videos that describe the setup and the different features provided by JR
9. have support for Lambda calculus.
10. string support.
11. Set up SPF tests as regression tests in JR
12. Have a pipeline that finds regressions with every JR master commit
13. Fix JR SV-COMP version so that the runner script does not communicate with JR via a log file.

Done

1. Allow symbolic regions to read a symbolic input from the stack

Current SVComp rules says

The verifier does not exceed an stdout/stderr limit of at most 2 MB.

With the growing output of JR which is irrelevant to the competition and users, we need to support a developer flag, that prints out the JR print statements and close it otherwise.

This is the issue reported by Georges regarding silent object concretization.

Here follows a reproducer for the bug about silent concretization when casting to Object. Here follows the code:

import gov.nasa.jpf.symbc.Debug;

import java.util.HashMap;
import java.util.Map;

public class Compare {
    protected Compare() {
        // prevents calls from subclass
        throw new UnsupportedOperationException();
    }
    private static Map<String, Object> map;
    public static void main(String[] args) {
        map = new HashMap<>();
        boolean mybool = Debug.makeSymbolicBoolean("randomvalue");
        map.put("abc", mybool);
        if ((boolean) map.get("abc")) {
            System.out.println("loose");
            assert (false);
        } else {
            System.out.println("win");
        }
        return;
    }
}
 

And I put the output of JR attached (as you see, it does not report any error, while it should as we can reach the assert (false) ) .

the log file is below

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
* running veritesting with SPFCases and Early Returns.
JavaPathfinder core system v8.0 (rev 0df77f0a2a8fa55d58a4ed89b70b61e39626866c) - (C) 2005-2014 United States Government. All rights reserved.


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

====================================================== search started: 10/2/20 11:24 PM
win

====================================================== VeritestingListener report:
Encountered Veritesting Regions in veriRegions (i.e., VeriTestingMain.veriRegions size) = 0

/************************ Printing Exception Statistics *****************
Static Analysis exceptions count = 0
Instantiation Time exceptions count = 0
Unknown phases exception count = 0


/************************ Printing Time Decomposition Statistics *****************
static analysis time = 0 msec
Veritesting Dyn Time = 261 msec
Veritesting fix-point Time = 0 msec
GoTo rewrite instances = 0

/************************ Printing Solver Statistics *****************
Total Solver Queries Count = 0
Total Solver Time = 0 msec
Total Solver Parse Time = 0 msec
Region Summary Parse Time = 0 msec
Total Solver Clean up Time = 0 msec
PCSatSolverCount = 0
PCSatSolverTime = 0 msec
Constant Propagation Time for PC sat. checks = 0
Array SPF Case count = 0
If-removed count = 0

/************************ Printing Region Statistics *****************
Number of Distinct Veritested Regions = 0
Number of Distinct Un-Veritested Symbolic Regions = 0
Number of Distinct Failed Regions for Field Reference = 0
Number of Distinct Failed Regions for SPFCases = 0
Number of Distinct Failed Regions for missing method summaries = 0
Number of Distinct Failed Regions for Other Reasons = 0
Number of High Order Regions Used = 0

/************************ Printing Instantiation Statistics *****************
Number of successful instantiations = 0
Total Number of unsuccessful instantiations = 0
Number of failed instantiations due to Field Reference = 0
Number of failed instantiations due to SPFCases = 0
Number of failed instantiations due to missing method summaries = 0
Number of failed instantiations due to Other Reasons = 0


Number of Veritested Regions Instances = 0
Printing keys of regions that were instantiated at least once
Finished printing keys of regions that were instantiated at least once

Metrics Vector:
261,0,261,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,-1,-1,0.0,0,0,0

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=374,released=11,maxLive=0,gcCycles=1
instructions:       3368
max memory:         123MB
loaded code:        classes=63,methods=1336

====================================================== search finished: 10/2/20 11:24 PM

Problem with early returns

package veritesting.tcas;


public class tcas {
    public int OLEV = 600;
    public int MAXALTDIFF = 300;
    public int MINSEP = 600;
    public int NOZCROSS = 100;

    public int Cur_Vertical_Sep;
    public boolean High_Confidence;
    public boolean Two_of_Three_Reports_Valid;

    public int Own_Tracked_Alt;
    public int Own_Tracked_Alt_Rate;
    public int Other_Tracked_Alt;

    public int Alt_Layer_Value;

    int Positive_RA_Alt_Thresh_0;
    int Positive_RA_Alt_Thresh_1;
    int Positive_RA_Alt_Thresh_2;
    int Positive_RA_Alt_Thresh_3;

    public int Up_Separation;
    public int Down_Separation;

    public int Other_RAC;

    public int NO_INTENT = 0;
    public int DO_NOT_CLIMB = 1;
    public int DO_NOT_DESCEND = 2;

    public int Other_Capability;
    public int TCAS_TA = 1;
    public int OTHER = 2;

    public int Climb_Inhibit;

    public int UNRESOLVED = 0;
    public int UPWARD_RA = 1;
    public int DOWNWARD_RA = 2;

    private int result_alt_sep_test = -1;
    private int result_alim = -1;

    private int b2I(boolean b) {
        return b ? 1 : 0;
    }

    public void initialize() {
        Positive_RA_Alt_Thresh_0 = 400;
        Positive_RA_Alt_Thresh_1 = 500;
        Positive_RA_Alt_Thresh_2 = 640;
        Positive_RA_Alt_Thresh_3 = 740;
    }

    public int ALIM() {
        if (Alt_Layer_Value == 0) {
            return Positive_RA_Alt_Thresh_0;
        } else if (Alt_Layer_Value == 1) {
            return Positive_RA_Alt_Thresh_1;
        } else if (Alt_Layer_Value == 2) {
            return Positive_RA_Alt_Thresh_2;
        } else {
            return Positive_RA_Alt_Thresh_3;
        }
    }

    public int alt_sep_test() {
        int alt_sep = UNRESOLVED;
        if (High_Confidence) {
            alt_sep = ALIM();
        }
        return alt_sep;
    }

    public void mainProcess(int a1, int a2, int a7) {//,
        
        initialize();
        Cur_Vertical_Sep = a1;
        if (a2 == 0) {
            High_Confidence = false;
        } else {
            High_Confidence = true;
        }

        Alt_Layer_Value = a7;

        result_alt_sep_test = alt_sep_test();

    }

    public void sym1(int a1, int a2, int a7) {
        mainProcess(a1, a2, a7);
    }

    public static void main(String[] argv) {
        int maxSteps = Integer.parseInt(System.getenv("MAX_STEPS"));
        if (maxSteps-- > 0) (new tcas()).sym1(601, -1, 0);

    }

}

From WBS: problem with complex conditions

if ((AutoBrake &&
		         WBS_Node_WBS_BSCU_Command_Is_Normal_Relational_Operator)) {
		      WBS_Node_WBS_BSCU_Command_Switch = 1;
		   }  else {
		      WBS_Node_WBS_BSCU_Command_Switch = 0;
		   }

Hi,

It seems that JR (or SPF) fails on the following small piece of code:

import java.util.Map;
import java.util.TreeMap;
import gov.nasa.jpf.symbc.Debug;

public class Test {
    protected Test() {
        // prevents calls from subclass
        throw new UnsupportedOperationException();
    }

    public static void main(String[] args) {
        Map<String, Object> map1 = new TreeMap<>(String.CASE_INSENSITIVE_ORDER);
        map1.put("key", Debug.makeSymbolicBoolean("test1"));

        Map<String, Object> map2 = new TreeMap<>(String.CASE_INSENSITIVE_ORDER);
        map2.put("key", Debug.makeSymbolicBoolean("test2"));
        System.out.println(map2.get("key"));
    }
}

When trying to debug, I see that the fieldAttr of the value associated to the key is an ObjectList of Boolean, containing both symbolic booleans that I created (while it should be a sole Boolean).

This results in the following crash:

gov.nasa.jpf.util.ObjectList$Node cannot be cast to gov.nasa.jpf.symbc.numeric.Expression
java.lang.ClassCastException: gov.nasa.jpf.util.ObjectList$Node cannot be cast to gov.nasa.jpf.symbc.numeric.Expression
    at gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil.isSymCond(SpfUtil.java:83)
    at gov.nasa.jpf.symbc.VeritestingListener.executeInstruction(VeritestingListener.java:319)
    at gov.nasa.jpf.vm.VM.notifyExecuteInstruction(VM.java:793)                                      
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1904)

Given that symbolic values seem to work pretty well with everything else (except maps), I assume that there is a wrong interaction between both that makes everything crash. The same bug happens if I replace TreeMaps by HashMaps.

Regards,
Georges-Axel.

PS: this is the jpf file that I use:

classpath=/private/tmp/test/reproducer/build/test.jar
symbolic.debug=false
symbolic.lazy=false
veritestingMode = 5
performanceMode = true
search.multiple_errors=true
symbolic.dp=z3bitvectorinc
listener = .symbc.VeritestingListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener
symbolic.optimizechoices=false
jitAnalysis = true

Run only obligation transformation on regions that have uncovered obligations.

We have a problem in populating the side effects for fields, and I am assuming the same will happen for the arrays, when an early return happens on one path. In particular, running the following code with JR mode 3, raises an assert exception, while on plain SPF no assertions are violated.

class Something{

int sideEffect = 0;
private int testERInline(boolean a, int x) {
        int z = 0;
        if (a) z = testingER1(a, x);
        assert !(a && x > 2) || this.sideEffect == 0;
        return z;
    }

    private int testingER1(boolean a, int x) {
        int z = 1;
        if (x > 2) {
            z = x + 1;
            return z;
        }
        z++;
        this.sideEffect = 5;

        return z;
    }
}

The problem is with the sideEffect field update in testingER1 method. There the side effect should be guarded by the fact that the early return did not happen. Since the field transformation happens after the early return removal, it does not account for the fact that the side effect should be void in case of early returns happening.

I ran the above code with jpf configuration

veritestingMode=3
symbolic.dp=z3bitvectorinc
listener =.symbc.VeritestingListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener

or with the following listener

listener =.symbc.SymbolicListener,gov.nasa.jpf.symbc.numeric.solvers.IncrementalListener

1. Merge the varTypeTable and fieldRefTypeTable.
   1. Add information into each entry of the varTypeTable if a type was figured out statically or dynamically. See Issue sohah/VeritestingTransformations#26.
   2. Support "reference" as a type in fields and arrays instead of trying to use them as "int" type in Ranger IR
2. Have new set of modes that are configurable to any sort of combination rather than the current fixed increments of path-merging features.
3. Support real numbers variables in veritesting.
4. Document all the configuration options we are using
5. Document all the equivalence-checks that we are using
6. Compare our results with JBMC on all the benchmarks
   • Assigned to Vaibhav
7. Dont instantiate a region if the number of paths through the region is less than or equal to the number of Java Ranger choices through the region.
   • A simple version of this optimization that only looks at the conditions associated with Java Ranger choices has already been implemented. But a choice's condition can also be infeasible when evaluated in the context of the path condition. We need to figure out if there is a way to do this optimization without invoking the solver. One idea is to try Z3's simplification.
8. Implement heuristic to estimate the cost of instantiating the region and don't instantiate the region if the cost is too high. One such heuristic was implemented by Kuznetsov et al.(https://www.cs.rhul.ac.uk/home/kinder/papers/pldi12.pdf).
   • Vaiibhav to try a dumb algorithm first. This can potentially turn into an entire paper's worth of work.
9. Test case generation for veritesting.
10. Look into testing Java Ranger with SV-COMP Java benchmarks
    • Send Willem an email asking for SV-COMP benchmarks driver files (Vaibhav)
11. Follow-up with Corina on the merge of java-ranger with SPF.
    • Check if the performance flakiness still exists with baseline SPF with its latest code
    • Changing the memory allocation to 12.288 GB from 8.192GB for replace11 caused its total running time in mode1 to go from ~20 minutes to ~1 hour 11 minutes. This weirdness running time increase was observed twice. Changing the memory allocation back to 8.192 GB for replace11 caused its running time to come back to ~20 minutes.
12. Instantiate method summaries when they are beneficial in reducing the number of execution paths even if they are outside a multi-path region.
13. Skip side-effect-free functions like System.out.println. Maybe even identify such functions dynamically in the future.
14. Re-run the benchmarks with the exclusions file
    • Assigned to Vaibhav
15. Do returns inside method summary after it is inlined inside a multi-path region cause the region instantiation to be aborted?
    • Assigned to Soha
16. Use the solver interface of Green to see how much of a performance improvement we get with SPF and with Java Ranger.
17. Look into use of path subsumption as done by Tian et al. (paper here).
18. Finish off the bounded value concretization feature (that currently sits in symarrays/NEWARRAY.java) by adding a new choice generator class that allows an arbitrary set of values to be explored as feasible values for a symbolic variable.
19. Email JBMC authors if we're using their tool correctly.
    • assigned to Vaibhav
20. Use the Defects4J bug database for bug-finding with java ranger

Completed:

1. Add support for the checkCast instruction.
2. Get incremental solver mode working
3. Support stack input and outputs
4. Add fixed point computation during region instantiation
5. Get JIT static method analysis working.
6. Have a metrics of why we did not instantiate veritesting regions, and whether SPF's requirement for concrete references at the end of blocks is one of the main reasons.
   • Root causes of the field reference failures have been fixed (they were being incorrectly logged as field reference failures as of the FSE2019 submission) and all the "other failure reason" causes of region instantiation failures were found to be due to missing method summaries. Vaibhav has set the region metrics up to log field-related failures correctly and will be on the lookout for region instantiation failures.
7. Figure out what is going wrong with the static analysis of the motivating example in the paper.
   • Assigned to Vaibhav, fixed in commit sohah/VeritestingTransformations@ea2c1ed
8. Don't instantiate a region with single-path cases if the branching factor of the single-path cases is not strictly less than the number of execution paths through the region.
   • Is it possible to use Z3's simplifier to do this check? Vaibhav: Possibly, but we dont need something as sophisticated as Z3's simplifier to figure out how many feasible choices Java Ranger is creating. Update [04/29/2019) This heuristic is now implemented.
9. What is going wrong with jitAnalysis in MerArbiter?
   • Assigned to Soha - "Region MerArbiter.TopLevelArbiter$REGION_T$STATE_T$RegionR39$StateRunning35$RegionR38$StateUser244$RegionR37$Transition189.guard()Z#93 has no recovered static region", fixed in commit sohah/VeritestingTransformations@d74e360
10. Upgrade baseline SPF with the latest code in the upstream SPF github repository.
    • assigned to Vaibhav

The current implementation supports z3inc. To support z3bitvectorinc, some translation for the model output from the solver is needed.