[Boogie Backend] Add SMT bit-vector builtin operations #2901
Conversation
zhassan-aws
changed the title
Yes, this is something I'm annoyed about. I currently manually run tests locally before opening a PR to make sure nothing broke. to To have proper tests, we'd need to install the Boogie verifier in our CI and update the Kani driver to call it. This will require a bit of work though. In the meantime, we can add tests that check that the generated Boogie file is what we expect it to be (or at least contains some of the lines we're expecting). Such tests may be fragile though due to changes in MIR. |
zhassan-aws
force-pushed
the
features/boogie
branch
from
d518ae1
to
215b31b
Compare
zhassan-aws
force-pushed
the
smt-builtins
branch
2 times, most recently
from
d89fa80
to
1996ac7
Compare
zhassan-aws
force-pushed
the
features/boogie
branch
2 times, most recently
from
aea0126
to
44ff9da
Compare
I think the second option might be helpful while you are still working from a branch. I'm assuming you don't merge with main very often, do you? |
zhassan-aws
force-pushed
the
smt-builtins
branch
from
1996ac7
to
52c1c99
Compare
Sounds good. If you don't mind, I'll add those tests in a follow-up PR.
No, this is kept separate from |
Created #2914. |
zhassan-aws
merged commit e907a73
into
model-checking:features/boogie
Define SMT bit-vector builtin operations (e.g. `bvult`, `bvadd`, `bvand`, etc.) as functions in the preamble and codegen MIR binary operations as calls to those functions. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Define SMT bit-vector builtin operations (e.g. `bvult`, `bvadd`, `bvand`, etc.) as functions in the preamble and codegen MIR binary operations as calls to those functions. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Define SMT bit-vector builtin operations (e.g. `bvult`, `bvadd`, `bvand`, etc.) as functions in the preamble and codegen MIR binary operations as calls to those functions. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Define SMT bit-vector builtin operations (e.g. `bvult`, `bvadd`, `bvand`, etc.) as functions in the preamble and codegen MIR binary operations as calls to those functions. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Define SMT bit-vector builtin operations (e.g.
bvult,bvadd,bvand, etc.) as functions in the preamble and codegen MIR binary operations as calls to those functions.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.