search

vaibhavbsharma / java-ranger

Java Ranger is a path-merging extension of Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
13 stars 5 forks source link

Java Ranger To-Do Notes #2

Open vaibhavbsharma opened 3 years ago

vaibhavbsharma commented 3 years ago

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
sohah commented 3 years ago

Adding some more enhancements for JR during the Amazon meeting.