Comments (11)
I've pushed a first attempt at this. I did not go through the Java front-end though, but by using some sort uninterpreted functions in the C front-end. This was because I wasn't able to get the Java part working (after discussing also with @martin-cs). I'm attaching a simple example of how the thing works so far. You can run it (from my fork) like this:
$ ./cbmc/cbmc --smt2 --outfile /tmp/out.smt2 --cvc4 /path/to/test.c
Then you can run cvc4 on the output, and it gives the expected result (unsat):
$ ./cvc4 /tmp/out.smt2
A lot needs to be done of course, and I've only tested a subset of the functions mentioned in cprover-string-hack.h
. However, I hope this is enough for you to tell me if I'm going in the right direction.
from cbmc.
from cbmc.
I've continued along the lines discussed with martin. I've added support for
an alternative string backend, using arrays with length and quantified
axioms. This is enabled if you use --z3
. I've also updated the example and
put it in the repo (under regressions/strings
).
Note I'm now working on a smt-strings
branch instead of master
As usual, everything is very unstable and likely to crash in many different
ways... there's one example that works though :-)
from cbmc.
I pushed a couple more tests for strings. They are still tiny, but already
enough to show that current solvers aren't very good at handling this kind of
problems. Running regressions/strings/test3/test.c
with the Z3 backend
results in an unkonwn
answer, whereas CVC4 just seems to take forever.
from cbmc.
I also tried Z3 with built-in string support (i.e. running it on the .smt2 file generated with --cvc4 --smt2 --outfile
), but it is as slow as CVC4
from cbmc.
Indeed, as discussed the INT<->BV conversion that is needed for integrating
with CBMC is a major source of difficulty for the solvers. I just committed
two versions of a hand-written SMT2 encoding of test3, one using Ints
directly, and one going through and Int<->BV conversion layer. The former is
solved almost immediately by CVC4, whereas the latter takes forever. I tried
also some other variants of Int<->BV conversion, but with no luck.
Suggestions welcome. In particular, is there a way to use unbounded integers
in CBMC? An alternative could be to check with the CVC4 people how feasible it
is to hack the string theory solver to work on BV directly (if possible by
perserving soundness...)
from cbmc.
quick update. I'm now experimenting with the PASS quantifier instantiation
strategy for solving string constraints as quantified arrays with length. I've
built a simple prototype to start playing with the technique. You can find it
at: https://github.com/agriggio/diffblue-experiments
(see the comment at the beginning of pass.py for instructions)
from cbmc.
Extending Z3str2 with bit-vector constraints:
https://uwspace.uwaterloo.ca/handle/10012/10022
There is a paper at the upcoming SMT'16 about this. Unfortunately, I haven't been able to find the solver and/or the benchmarks online. I'm reading the thesis now
from cbmc.
I have made some progress with my PASS-like prototype (at
https://github.com/agriggio/diffblue-experiments). Now the solver can also say
"sat" in some cases, and not just "unsat". Thanks also to a bug fix in the
encoding, now all the small examples in the regression/strings
directory of
(my fork of) cbmc can be solved. This is remarkable because neither Z3 nor
CVC4 can solve all these problems, despite their (apparent?) simplicity.
from cbmc.
Added a bunch of small benchmarks from Z3str2-bv, whose source code in now on bitbucket:
https://bitbucket.org/sanues/z3-str2-bv
Unfortunately, the solver seems to crash quite often for me
from cbmc.
Closing this as now a sub-goal of #6134.
from cbmc.
Related Issues (20)
- Incorrect location coverage results in the presence of assumptions HOT 7
- DFCC loop contracts crashes with VS HOT 2
- Finite loop run can't be terminated? HOT 4
- An assertion about complex numbers. HOT 1
- Pointer to enum gives the failure result. HOT 1
- Unexpected result for struct member with bit fields.
- CBMC gives unexpected result in equivalent transformation.
- Whether cbmc supports built-in functions? HOT 1
- CBMC deals with mmap and munmap in pointer check.
- abs() >=0 assertion failed HOT 5
- The transformation between pointer and array of type char16_t & char32_t.
- The size of the first dimension is omitted when the array is defined. HOT 2
- C code has extern keyword in pointer check. HOT 4
- issues with auto-objects
- [Safety feature] Error when enforcing contracts twice
- [Question] Could not find goto-cc in the windows MSI HOT 2
- [Question] Minimum requirements for running CBMC in windows HOT 4
- [RFC] Build system support in CBMC version 6 HOT 3
- Invariant violation when dumping C code with anonymous structs or unions HOT 3
- Compilation error on ARM64 Linux HOT 1
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 cbmc.