forked from Z3Prover/z3
-
Notifications
You must be signed in to change notification settings - Fork 5
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #101 from VeriFIT/readme-update
Readme update
- Loading branch information
Showing
2 changed files
with
56 additions
and
54 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,44 @@ | ||
## Building and running on Starexec VM | ||
|
||
1. The VM: | ||
``` | ||
VM: https://www.starexec.org/vmimage/ | ||
user: root | ||
passwd: St@rexec | ||
``` | ||
2. Install newer CMake: | ||
```shell | ||
git clone 'https://gitlab.kitware.com/cmake/cmake.git' | ||
cd cmake | ||
./configure | ||
gmake | ||
make install | ||
``` | ||
3. Install Mata | ||
```shell | ||
git clone 'https://github.com/VeriFIT/mata.git' | ||
cd mata | ||
vim CMakeLists.txt | ||
# ... comment out the following two lines: | ||
# include(CodeCoverage) | ||
# setup_target_for_coverage(${PROJECT_NAME}_coverage tests coverage) | ||
CC=/opt/rh/devtoolset-8/root/usr/bin/gcc CXX=/opt/rh/devtoolset-8/root/usr/bin/g++ make release | ||
make install | ||
``` | ||
4. Compile Noodler: | ||
|
||
```shell | ||
git clone 'https://github.com/VeriFIT/z3-noodler.git' | ||
mkdir z3-noodler/build | ||
cd z3-noodler/build | ||
vim ../src/test/CMakeLists.txt | ||
# ... comment out the following line: | ||
# add_subdirectory(noodler) | ||
CC=/opt/rh/devtoolset-8/root/usr/bin/gcc CXX=/opt/rh/devtoolset-8/root/usr/bin/g++ cmake -DCMAKE_BUILD_TYPE=Release .. | ||
make | ||
``` | ||
|
||
5. Now you should be able to run Z3-Noodler by typing | ||
```shell | ||
/root/z3-noodler/build/z3 smt.string_solver="noodler" <path/to/instance.smt2> | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,10 +2,8 @@ | |
|
||
Z3-Noodler is an SMT solver for string constraints such as those that occur in symbolic execution and analysis of programs, | ||
reasoning about configuration files of cloud services and smart contracts, etc. | ||
Z3-Noodler is based on the SMT solver [Z3](https://github.com/Z3Prover/z3), in which it replaces the solver for the theory of strings. | ||
The core of the string solver relies on the equation stabilization algorithm from the paper | ||
|
||
> F. Blahoudek, Y. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál, and J. Síč. [Word Equations in Synergy with Regular Constraints](https://link.springer.com/chapter/10.1007/978-3-031-27481-7_23). In *Proc. of FM’23*, Lübeck, Germany, volume 14000 of LNCS, pages 403–423, 2023. Springer-Verlag. | ||
Z3-Noodler is based on the SMT solver [Z3 v4.12.2](https://github.com/Z3Prover/z3/releases/tag/z3-4.12.2), in which it replaces the solver for the theory of strings. | ||
The core of the string solver implements several decision procedures, but mainly it relies on the equation stabilization algorithm (see [Publications](#publications)). | ||
|
||
Z3-Noodler utilizes the automata library [Mata](https://github.com/VeriFIT/mata/) for efficient representation of automata and their processing. | ||
|
||
|
@@ -60,64 +58,23 @@ cd build/ | |
``` | ||
## Limitations | ||
The following functions/predicates of the SMTLIB theory `Strings` are not supported at the moment. | ||
The following functions/predicates of the [SMTLIB Strings theory](https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml) are not supported at the moment. | ||
``` | ||
str.< | ||
str.<= | ||
str.replace_all | ||
str.replace_re | ||
str.replace_re_all | ||
str.is_digit | ||
str.to_code | ||
str.from_code | ||
str.to_int | ||
str.from_int | ||
``` | ||
We provide a full support for `str.contains`, but a limited support for its negated version. | ||
## Building and running on Starexec VM | ||
1. The VM: | ||
``` | ||
VM: https://www.starexec.org/vmimage/ | ||
user: root | ||
passwd: St@rexec | ||
``` | ||
2. Install newer CMake: | ||
```shell | ||
git clone 'https://gitlab.kitware.com/cmake/cmake.git' | ||
cd cmake | ||
./configure | ||
gmake | ||
make install | ||
``` | ||
3. Install Mata | ||
```shell | ||
git clone 'https://github.com/VeriFIT/mata.git' | ||
cd mata | ||
vim CMakeLists.txt | ||
# ... comment out the following two lines: | ||
# include(CodeCoverage) | ||
# setup_target_for_coverage(${PROJECT_NAME}_coverage tests coverage) | ||
CC=/opt/rh/devtoolset-8/root/usr/bin/gcc CXX=/opt/rh/devtoolset-8/root/usr/bin/g++ make release | ||
make install | ||
``` | ||
4. Compile Noodler: | ||
```shell | ||
git clone 'https://github.com/VeriFIT/z3-noodler.git' | ||
mkdir z3-noodler/build | ||
cd z3-noodler/build | ||
vim ../src/test/CMakeLists.txt | ||
# ... comment out the following line: | ||
# add_subdirectory(noodler) | ||
CC=/opt/rh/devtoolset-8/root/usr/bin/gcc CXX=/opt/rh/devtoolset-8/root/usr/bin/g++ cmake -DCMAKE_BUILD_TYPE=Release .. | ||
make | ||
``` | ||
## Publications | ||
- Y. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál, and J. Síč. Solving String Constraints with Lengths by Stabilization. In *Proc. of OOPSLA'23*, Cascais, Portugal. 2023. ACM. | ||
- F. Blahoudek, Y. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál, and J. Síč. [Word Equations in Synergy with Regular Constraints](https://link.springer.com/chapter/10.1007/978-3-031-27481-7_23). In *Proc. of FM’23*, Lübeck, Germany, volume 14000 of LNCS, pages 403–423, 2023. Springer-Verlag. | ||
|
||
5. Now you should be able to run Z3-Noodler by typing | ||
```shell | ||
/root/z3-noodler/build/z3 smt.string_solver="noodler" <path/to/instance.smt2> | ||
``` | ||
|
||
## Z3-Noodler source files | ||
|
||
|
@@ -126,12 +83,13 @@ The string solver of Z3-Noodler is implemented in [src/smt/theory_str_noodler](s | |
Tests for Z3-Noodler are located in [src/test/noodler](src/test/noodler). | ||
|
||
## Authors | ||
- :envelope: [Vojtěch Havlena](mailto:[email protected]?subject=[GitHub]%20Z3-Noodler), | ||
- :envelope: [Juraj Síč](mailto:[email protected]?subject=[GitHub]%20Z3-Noodler), | ||
- [Yu-Fang Chen](mailto:[email protected]?subject=[GitHub]%20Z3-Noodler), | ||
- [David Chocholatý](mailto:[email protected]?subject=[GitHub]%20Z3-Noodler), | ||
- [Vojtěch Havlena](mailto:[email protected]?subject=[GitHub]%20Z3-Noodler), | ||
- [Lukáš Holík](mailto:[email protected]?subject=[GitHub]%20Z3-Noodler), | ||
- [Ondřej Lengál](mailto:[email protected]?subject=[GitHub]%20Z3-Noodler), | ||
- [Juraj Síč](mailto:[email protected]?subject=[GitHub]%20Z3-Noodler). | ||
- [Ondřej Lengál](mailto:[email protected]?subject=[GitHub]%20Z3-Noodler). | ||
|
||
|
||
## Original Z3 README | ||
|
||
|