Z3str3RE - CAV 21 Artifact Evaluation VM - Ubuntu 20.04 LTS
| Main Authors: | Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh |
|---|---|
| Format: | Proceeding eJournal |
| Terbitan: |
, 2021
|
| Online Access: |
https://zenodo.org/record/4477692 |
Daftar Isi:
- This VM setup is heavily based on Sebastian Hjort Hyberts, Peter Gjøl Jensen and Thomas Neele:TACAS 21 Artifact Evaluation VM - Ubuntu 20.04 LTS. This file describes how to compile and install Z3str3RE and setup the benchmark infrastructure including the used benchmark sets to reproduce the results presented in the corresponding submission. We present a novel length-aware decision procedure for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. Motivated by program analysis, security, and verification applications, we implemented and evaluated this algorithm and related heuristics in the Z3 theorem prover. The artifact we present here is this implementation, which we call Z3str3RE. We showcase the power of our algorithm via an extensive empirical evaluation over a large and diverse benchmark of over 57000 regex-heavy instances, over 75% of which are derived from industrial applications, that include instances contributed by other solver developers. Our solver outperforms five other state-of-the-art string solvers, namely, CVC4, OSTRICH, Z3seq, Z3str3, and Z3-Trau, over this benchmark, in particular achieving a 2.4x speedup over CVC4, 4.4x speedup over Z3seq, 6.4x speedup over Z3-Trau, 9.1x speedup over Z3str3, and 13x speedup over OSTRICH. The implemented solver will be merged into the mainline Z3 solver (https://github.com/Z3Prover/z3) once the algorithm is published. Licences Our license file is called Licence.txt. Since we included all solvers to whom we compared our algorithm we included their licenses as well. They are located in the subfolder OTHER_SOLVER_LICENSES. Quick Start We provide a VirtualBox virtual machine running Ubuntu 20.04 LTS being based Sebastian Hjort Hyberts, Peter Gjøl Jensen and Thomas Neele:TACAS 21 Artifact Evaluation VM - Ubuntu 20.04 LTS. Whenever needed use username "re" and password "re". You can skip the "Install the prerequisites" section, since the virtual machine is already preconfigured. All instructions are starting within the home directory /home/re/reproduction/artifact. Compiling Z3str3RE We include a bash script named compileRegExSolver.sh which compiles the provided source code. To compile the solver you simply have to execute bash compileRegExSolver.sh Reproducing the results We provide two scripts to reproduce the presented results using the benchmark framework ZaligVinder. Repeating the run using all solvers on all presented benchmarks: bash runBenchmarks.sh Repeating the run including the heuristics analysis: bash runBenchmarksHeuristics.sh Within our empirical evaluation we use 57256 different instances. Running all these instances on a standard computer would take an extremely long time. Therefore, we added two additional runner scripts executing our experiments on a previously randomly selected set of benchmarks. To execute this "smaller" set, proceed as follows: Repeating the run using all solvers on a subset of the presented benchmarks (approximately 5 minutes): bash runBenchmarksSmall.sh Repeating the run including the heuristics analysis on a subset of the presented benchmarks (approximately 6 minutes): bash runBenchmarksHeuristicsSmall.sh After the ZaligVinder run has finished a webserver is started. You can review the results by guiding your browser to http://localhost:8081. Further post analysis steps Within the ZaligVinder folder ``zaligvinder`` we stored the database of our experimental evaluation. Inspecting the results within the web browser: Execute the following commands to review our results within ZaligVinder's web gui: cd zaligvinder python3 startwebserver.py cav21.db Afterwards navigate to http://localhost:8081 in your web browser. Generate an tables, plots and ASCII Doctor web page to review the results: Execute the following commands cd zaligvinder python3 tablegen.py which will open a terminal gui. Select cav21.db as database and a place to store the output file -- entering no output name stores the output data within the folder zaligvinder/external_data/<today's_date>. Afterwards you are able to select the benchmark sets of your choice being present within our run and the solvers. Note, Z3str3-base is the implementation of our regex solver. Z3str3RE-none, Z3str3RE-li, Z3str3RE-psh, Z3str3RE-ali, and Z3str3RE-asi represent solvers being part of our heuristics experiment. Next step is selecting whether you want to generate the cactus plots, tables or the ASCII Doctor page. Tables and Plots. Tables and plots need to be compiled by using ``latexmk``. Simply execute latexmk -pdf yourFileName to generate a PDF. Generating HTML for the ASCII doctor page. To view the ASCII Doctor page conveniently in your browser execute asciidoctor yourFileName which will create a <yourFileName>.html file. To open firefox execute firefox <yourFileName>.html. You can perform these post analysis steps on your own generated database too. To do so instead of using cav21.db within the terminal gui simply select your own generated database having a name similar to CAV21_results_1611768687.585239.db.