Comments (14)
Unfortunately, there is no current workaround, but I'm planning to work on one in the coming days.
For a bit of context: although supported by Z3, CVC4 and CVC5, bv2nat
is not part of the official standard defined by the smtlib. More specifically, the theory for BV internally defines bv2nat
but only so that it can be used in its semantic specification.
Until now, dolmen
has strived to implement the standard, at least as a first goal, so that it could be used to check conformity against that standard. However, it appears that it's not sufficient anymore, so I'm planning to add a notion of typing extensions: these extensions would be enabled by cli flags and effectively add new functions to the typing builtins (similar to how the parsing extensions work, see #190 ).
from dolmen.
Understood. I'm trying to get a non-trivial program verification benchmark into the SMTComp suite. The code is cryptographic, so it has modular arithmetic and BV stuff all over the place...
from dolmen.
I should have an experimental version of dolmen
that can accept bv2nat
by the end of the week.
from dolmen.
Just to make sure, what would be the expected signature of the bv2nat
function ?
from dolmen.
Not sure.... how is it declared in Z3, CVC4 and CVC5?
from dolmen.
As far as I could tell when implementing these functions for Alt-Ergo, they use a family of function symbols of the form (bv2nat (_ BitVec n) Int)
for all n > 0
, and indexed function symbols ((_ int2bv n) Int (_ BitVec n))
for n > 0
.
(I believe Z3 also supports nat2bv
but CVC5 only supports int2bv
because the developers didn't like nat2bv
allowing negative arguments)
from dolmen.
In the cvc5 AletheLF proof signatures bv2nat
and int2nat
have the following signatures. This is roughly SMT-LIB 3 syntax.
(declare-const int2bv (->
(! Int :var w)
Int (BitVec w))
)
(declare-const bv2nat (->
(! Int :var m :implicit)
(BitVec m) Int)
)
from dolmen.
#208 adds a way for dolmen
to accept the bv2nat
and int2bv
functions.
from dolmen.
Is this merged now?
from dolmen.
Apologies for the delay, yes it has been merged.
from dolmen.
Solved by #208
One can now use the --ext=bvconv
option of the dolmen binary to allow bv2nat
and int2bv
.
from dolmen.
OK... now need to update the GitHub action associated with the smtcomp benchmark_submission repo so it will run the new binary with that option. Any idea how to do that?
from dolmen.
I had a look at the smt-comp repo, and its github actions will need a bit more code than currently to use the dev version of dolmen (since there is no release including PR#208 yet). You basically need two changes:
- First, the github action downloads the release binary for version 0.9, see these lines. Instead, you'll need to build the latest dev version of dolmen (or wait until I make a new release including the bvconv extension). To do that, build steps along these lines should be work (though I have not tested these):
# Setup ocaml/opam
- name: Setup ocaml/opam
uses: avsm/setup-ocaml@v2
with:
ocaml-compiler: ocaml-base-compiler.4.14.0
# Run opam udpate to get an up-to-date repo
- name: Update opam repo
run: opam update
# Install dev version of dolmen
- name: Install dolmen
run: opam pin --dev-repo dolmen dolmen_type dolmen_loop dolmen_model dolmen_bin
# Copy the dolmen binary
- name: Copy the dolmen binary
run: cp `opam exec -- which dolmen` ./dolmen-linux-amd64
Alternatively, I could try and see how to setup a github actions file that would build and upload a nightly release of dolmen (that wya, only the download url for the dolmen binary would need to change), but last time I looked, it was quite a bit of work.
- Second, you'll need to add the adequate extension on this line. Just adding
--ext=bvconv
should be enough.
from dolmen.
I think it's best for us to wait for the next formal binary release. Many thanks for all your efforts.
from dolmen.
Related Issues (20)
- Spec errors on the difference logic benchmarks of the SMT-LIB HOT 2
- Reject names starting with `@` and `.` outside of models
- Handling of `set-option :global-declarations`
- Handling of named terms HOT 2
- Check sat assuming HOT 2
- DIMACS variables do not appear as decls HOT 1
- Uncaught exception on buggy file
- 4.08 support broken (`List.concat_map`) HOT 10
- Quoted identifiers can be keywords HOT 12
- Warning regarding the `dolmen_type` file HOT 2
- Support non-incremental parsing from stdin HOT 1
- Handling abstract values in `(get-value)` statements HOT 8
- Supporting evaluation for custom functions HOT 5
- Support `bv2nat` as a "relaxed mode" HOT 2
- Attributes in nested quantifiers HOT 2
- RDL check is a bit too lenient HOT 1
- Can we get a formal 1.0 release please HOT 4
- Confusing error message with pattern matching on polymorphic type in ae's native language
- Support for `get-assignment` HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from dolmen.