Adding witness generation to SymbolicListener GSoC 2024 project#104
Adding witness generation to SymbolicListener GSoC 2024 project#104kylekim72 wants to merge 31 commits intoSymbolicPathFinder:sv-compfrom
Conversation
A test PR for gradle-build branch. Please reject this.
sohah
left a comment
sohah
left a comment
There was a problem hiding this comment.
I looked at this pull requests, and it needs serious refactoring. Please check out the specific comments on the code, but here are some general comments:
- Make a witness package that has all the necessary code for generating the witness.
- Refactor your code so that we can see the GraphML as java objects, this means we want to see a GraphML class that contains Node, and Edge objects. Then you'll need to serialize these objects to string, then to the witness file.
- Clean up all commented statements
- Include comments for all the classes and methods you are using, follow the Java documentation guidelines for that
- Files that contain template should exist under the "src/main/resources" directory within the project
- You should aim that the SymbolicListener would have a minimal added/modified code. Mostly method invocation to the Witness generation package.
- The state variable 'interceptSymbolic' needs to be set and reset correctly, check out my detailed comment on your code.
| VM vm = search.getVM(); | ||
| // Path to the witness template | ||
| // Assume working directory is SPF | ||
| String inputFilePath = "./jpf-symbc/witness_template/witness_template_minimal.txt"; |
There was a problem hiding this comment.
This file needs to be under "src/main/resources" directory.
|
@sohah , I fixed my code based on your advice. Please take a look and give me some other feedbacks when you have a moment. Thank you! |
sohah
left a comment
sohah
left a comment
There was a problem hiding this comment.
I have went over the readme instructions, and cannot reproduce the same outputs you've indicated, please look at the specific comments that I have left you, and let me know when you've addressed them. Thank you.
README.md
Outdated
| echo "symbolic.dp=z3bitvector" >> $DIR/config.jpf | ||
| echo "symbolic.bvlength=64" >> $DIR/config.jpf | ||
| echo "search.depth_limit=200" >> $DIR/config.jpf | ||
| echo "symbolic.strings=true" >> $DIR/config.jpf |
There was a problem hiding this comment.
I think this configuration is wrong, you cannot have the string support enabled. This is going to give an error. Have you tried that? is this what you are using?
The readme should be very easy to follow and to reproduce the results that you have on your machine.
There was a problem hiding this comment.
Yes it works. I used this when I ran all the benchmarks. I think symbolic string support isn't implemented yet, so regardless of whether the symbolic string option is turned on or off, it will just run as if it's turned off. This is just my guess, so if you have any other thoughts, please let me know.
2 participants
Hi there,
Here is the list that shows the changes in SPF.
I wrote a code to generate violation witness at SymbolicListener.java. It starts writing witness with reading "witness_template_minimal.txt", thus I added witness_template directory at jpf-symbc.
We decided to use
Debug.makeSymbolicBoolean()instead ofVerifier.randomBool()to generate witness. Therefore, I changed Verifier.java.When you have a moment, please give me some comments to improve. Thank you!