Include Kissat in the Kani bundle #2087
Conversation
zhassan-aws
force-pushed
the
integrate-kissat
branch
from
0e06a39 to
d135ff7
Compare
|
do we need to include this in the dependencies also? |
Good point. Added. |
|
Can we also check the expected version as part of the regression script? For the follow up PR, can you also please add a test that uses kissat as part of the bundle tests. |
|
The follow-up PR is #2088. I'll make sure to add a bundle test to it. |
Added a check.
I added a test to this PR since #2088 needs some work. The test is invoked using |
celinval
left a comment
celinval
left a comment
There was a problem hiding this comment.
I suggested a few little improvements to make our lives easier, but not a big deal if you don't do that as part of this PR. But something for us to keep in mind. Thanks!
scripts/kani-regression.sh
Outdated
| # To enable "unsound_experimental features, run as follows: | ||
| # `KANI_ENABLE_UNSOUND_EXPERIMENTS=1 scripts/kani-regression.sh` | ||
|
|
||
| # Check if kissat has the minimum required version |
There was a problem hiding this comment.
can you move this to its own check_kissat_version? Or even augment the CBMC to include the kissat version.
There was a problem hiding this comment.
I moved it to a separate script. Didn't feel it should be part of the CBMC one. Perhaps as a cleanup, we can create a single script, e.g. check_dep_versions that calls the other scripts.
| ./scripts/setup/ubuntu/install_deps.sh | ||
| ./scripts/setup/ubuntu/install_cbmc.sh | ||
| ./scripts/setup/ubuntu/install_viewer.sh | ||
| ./scripts/setup/install_kissat.sh |
There was a problem hiding this comment.
Can we make the install_deps.sh to invoke all the other installation scripts? We can keep the other scripts since they are handy to update versions, but this list is starting to grow too much.
There was a problem hiding this comment.
I'll do this in a follow-up PR.
| fi | ||
|
|
||
|
|
||
| # Kissat release |
There was a problem hiding this comment.
Can we check if the version is already installed first?
There was a problem hiding this comment.
Good idea. Done.
| @@ -156,6 +156,7 @@ jobs: | |||
| docker run -w /tmp/kani/tests/cargo-kani/simple-lib $tag cargo kani | |||
There was a problem hiding this comment.
These should also be a separate script.
There was a problem hiding this comment.
I'll do this one as well in a follow-up PR.
3 participants
Description of changes:
Install Kissat as part of the Kani setup, and include it in the Kani release bundle.
This is required by a PR that adds a
kani::solverattribute (whic will follow shortly).Keeping this as a draft until we integrate a CBMC version that fixes #1962.
Resolved issues:
Towards #1656
Related RFC:
Optional #ISSUE-NUMBER.
Call-outs:
Testing:
How is this change tested? A test is included in a PR that will follow shortly.
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.