Refactoring issues

[vaibhavbsharma]

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 HigherOrder3 equivalence-check fails #26.
   2. Support "reference" as a type in fields and arrays instead of trying to use them as "int" type in Ranger IR
2. Upgrade baseline SPF with the latest code in the upstream SPF github repository.
   • assigned to Vaibhav
3. Have new set of modes that are configurable to any sort of combination rather than the current fixed increments of path-merging features.
4. Support real numbers variables in veritesting.
5. Document all the configuration options we are using
6. Document all the equivalence-checks that we are using
7. Compare our results with JBMC on WBS and TCAS.
8. 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.
9. 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.
10. Test case generation for veritesting.
11. Look into testing Java Ranger with SV-COMP Java benchmarks
    • Send Willem an email asking for SV-COMP benchmarks driver files (Vaibhav)
12. Email Corina giving her an update on the tool and asking for more interesting benchmarks.
    • This will be done after we have upgraded baseline SPF to its latest code
    • 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.
13. Instantiate method summaries when they are beneficial in reducing the number of execution paths even if they are outside a multi-path region.
14. Skip side-effect-free functions like System.out.println. Maybe even identify such functions dynamically in the future.
15. Re-run the benchmarks with the exclusions file
    • Assigned to Vaibhav
16. Do returns inside method summary after it is inlined inside a multi-path region cause the region instantiation to be aborted?
    • Assigned to Soha
17. Use the solver interface of Green to see how much of a performance improvement we get with SPF and with Java Ranger.
18. Look into use of path subsumption as done by Tian et al. (paper here).
19. 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.

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 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 d74e360