diff --git a/README-Starexec.md b/README-Starexec.md new file mode 100644 index 00000000000..f38fce8aae8 --- /dev/null +++ b/README-Starexec.md @@ -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" +``` diff --git a/README.md b/README.md index c397fa6f8e6..55ec054cac5 100644 --- a/README.md +++ b/README.md @@ -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" -``` ## 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:ihavlena@fit.vut.cz?subject=[GitHub]%20Z3-Noodler), +- :envelope: [Juraj Síč](mailto:sicjuraj@fit.vut.cz?subject=[GitHub]%20Z3-Noodler), - [Yu-Fang Chen](mailto:yfc@iis.sinica.edu.tw?subject=[GitHub]%20Z3-Noodler), - [David Chocholatý](mailto:xchoch08@stud.fit.vutbr.cz?subject=[GitHub]%20Z3-Noodler), -- [Vojtěch Havlena](mailto:ihavlena@fit.vut.cz?subject=[GitHub]%20Z3-Noodler), - [Lukáš Holík](mailto:holik@fit.vut.cz?subject=[GitHub]%20Z3-Noodler), -- [Ondřej Lengál](mailto:lengal@fit.vut.cz?subject=[GitHub]%20Z3-Noodler), -- [Juraj Síč](mailto:sicjuraj@fit.vut.cz?subject=[GitHub]%20Z3-Noodler). +- [Ondřej Lengál](mailto:lengal@fit.vut.cz?subject=[GitHub]%20Z3-Noodler). + ## Original Z3 README