Add code from report #16
Conversation
..._half-rand-iter_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.execution_time.png
Outdated
Show resolved
Hide resolved
evaluation/scripts/profile-all.sh
Outdated
| # Set the path to silicon.sh | ||
| SILICON_PATH= | ||
| # Set the path to the Z3 binary | ||
| # Tested Versions: 4.8.7 (newer versions may not work; produce errors and different output) | ||
| Z3_PATH= | ||
| # Set the path to the Gobra jar | ||
| GOBRA_PATH= |
There was a problem hiding this comment.
Instead of leaving this blank for whoever imports the script, I think it would be better to expect these variables to be set when the script starts (we should still document what we expect these variables to contain). In the beginning, we can check that they are set and throw an error otherwise.
This has a few advantages:
- it fails clearly if people forget to set-up the script
- you will not have to change a file that is tracked under git to configure the script (unlike the current solution that will cause a bogus change to be always reported in
git status)
There was a problem hiding this comment.
Those are good points, thanks for the feedback. I addressed it.
In case it doesn't take too long, would you be willing to run the script and see whether it appears to work (i.e. doesn't crash somehow, and produces csvs/plots)? I am currently having some issues with my machine.
There was a problem hiding this comment.
I tried to run the script and I noticed a few things:
- instead of defining
Z3_PATH, we can just reuse the variableZ3_EXEwhich is needed for silicon and carbon anyway - on Mac, by default, there is no executable called
python, but there is one calledpython3. Maybe usingpython3would be more generally supported - After running it on my machine with all occurrences of
pythonreplaced bypython3, I get the output as shown in output.txt- maybe we should put in the readme the commands that we need to install the necessary dependencies
There was a problem hiding this comment.
instead of defining Z3_PATH, we can just reuse the variable Z3_EXE which is needed for silicon and carbon anyway
The script requires old versions of Z3, so I think it would be better if these are different variables.
on Mac, by default, there is no executable called python, but there is one called python3. Maybe using python3 would be more generally supported
On GNU Guix it is the same, but I wasn't sure whether it is a quirk of it. I will change it.
After running it on my machine with all occurrences of python replaced by python3, I get the output as shown in output.txt
I came across this problem myself too sometimes. Usually it is fixed by pulling and building Silicon again. I will add a note to the README.
maybe we should put in the readme the commands that we need to install the necessary dependencies
I think it is a good idea to put the dependencies also into the README. Since installing packages differs from distribution to distribution (pip, for example, refuses to install packages on some Linux distributions, as it doesn't want to mess with the system packages), I will add a generic note.
There was a problem hiding this comment.
The script requires old versions of Z3, so I think it would be better if these are different variables.
I'm not sure if that is true. In principle, the script should use the version of z3 that is used by the tools for the results to be meaningful. Also, we can always change the value of Z3_EXE for the current shell.
There was a problem hiding this comment.
I agree that that's the way it should be; however, the issue is described here viperproject/silicon#786.
For the script to be able to use newer versions of Z3, the following things probably need to be done:
- fix
Invalid quantifier instances line from prover: - find documentation for the columns (since their amount has changed)
- adapt
profile.pybased on the documentation for the columns
In my opinion, a failure with regards to Z3's path is better than some failure in profile.py due to the unexpected format, since in the former case I believe it is more likely for a user to learn about the version issue. However, it is no problem for me to change it, so I leave that decision up to you.
There was a problem hiding this comment.
Ok, Sounds good. I will merge this PR. can you please add this explanation on what to change to the README or to some issue on the issue tracker or some page on the wiki? It would be good to be able to find this easily later.
Adds the code written for the report of the practical work: