Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas

Fuzzing SMT solvers with Diversified Sub-formulas

Table of Contents

Background

Install

Usage

Bugs

Background

Octopus is the tool for detecting soundness bugs in SMT solvers. 
We have submitted 10 valid bug reports for Z3 so far. 7 bugs are confirmed/fixed by developers among these reports.

Install

Octopus itself has few dependencies. It uses Python3 and Python-virtualenv.

You can install Python-virtualenv using  pip install virtualenv

Then install Octopus.

virtualenv --python=/usr/bin/python3.6 virenv

source virenv/bin/activate

cd octopus

python3 setup.py install 

Usage

You can download SMT instances in SMT COMP 2021 as benchmarks.

2021-05-26 - StarExec

Then install and build the SMT solver you want to test.

For example:

git clone https://github.com/Z3Prover/z3.git

python scripts/mk_make.py

cd build; make

Then Octopus can be used to validate it, for example:

octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA

To run Octopus in multiple cores:

octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA --cores=20

Bugs

Octopus has detected many new refutational soundness bugs in Z3.

Here is a list of issues we reported.

https://github.com/Z3Prover/z3/issues/5373 [confirmed]
https://github.com/Z3Prover/z3/issues/5443 [reported]
https://github.com/Z3Prover/z3/issues/5447 [fixed]
https://github.com/Z3Prover/z3/issues/5456 [fixed]
https://github.com/Z3Prover/z3/issues/5457 [fixed] 
https://github.com/Z3Prover/z3/issues/5460 [fixed]
https://github.com/Z3Prover/z3/issues/5468 [fixed] 
https://github.com/Z3Prover/z3/issues/5488 [fixed]
https://github.com/Z3Prover/z3/issues/5502 [duplicate]
https://github.com/Z3Prover/z3/issues/5508 [reported]
https://github.com/Z3Prover/z3/issues/5423 [invalid]