Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas

<p><strong>Fuzzing SMT solvers with Diversified Sub-formulas</strong></p> <p>Table of Contents</p> <ul> <li>Background</li> <li>Install</li> <li>Usage</li> <li>Bugs</li> </ul> <p>&nbsp;</p> <p><strong>Background</strong></p> <p><strong>Octopus&nbsp;</strong>is the tool for detecting soundness bugs in SMT solvers.&nbsp;<br> We have submitted 10 valid bug reports for Z3 so far. 7 bugs are confirmed/fixed by developers among these reports.</p> <p>&nbsp;</p> <p><strong>Install</strong></p> <p>Octopus itself has few dependencies.&nbsp;It uses Python3 and Python-virtualenv.</p> <p>You can install Python-virtualenv&nbsp;using &nbsp;<code>pip install virtualenv</code></p> <p>Then install Octopus.</p> <p><code>virtualenv --python=/usr/bin/python3.6 virenv</code></p> <p><code>source virenv/bin/activate</code></p> <p><code>cd octopus</code></p> <p><code>python3 setup.py install</code>&nbsp;</p> <p>&nbsp;</p> <p><strong>Usage</strong></p> <p>You can download SMT instances in SMT COMP 2021 as benchmarks.</p> <p><a href="https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=1">2021-05-26 - StarExec</a></p> <p>Then&nbsp;install&nbsp;and build&nbsp;the SMT solver you want to test.</p> <p>For example:</p> <p><code>git clone https://github.com/Z3Prover/z3.git</code></p> <p><code>python scripts/mk_make.py </code></p> <p><code>cd build; make</code></p> <p>Then Octopus can be used to validate it, for example:</p> <p><code>octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA</code></p> <p>To run Octopus in multiple cores:</p> <p><code>octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA --cores=20</code></p> <p>&nbsp;</p> <p><strong>Bugs</strong></p> <p>Octopus has detected many new refutational soundness bugs in Z3.</p> <p>Here is a list of issues we reported.</p> <p><a href="https://github.com/Z3Prover/z3/issues/5373">https://github.com/Z3Prover/z3/issues/5373</a>&nbsp;[confirmed]<br> <a href="https://github.com/Z3Prover/z3/issues/5443">https://github.com/Z3Prover/z3/issues/5443</a>&nbsp;[reported]<br> <a href="https://github.com/Z3Prover/z3/issues/5447">https://github.com/Z3Prover/z3/issues/5447</a>&nbsp;[fixed]<br> <a href="https://github.com/Z3Prover/z3/issues/5456">https://github.com/Z3Prover/z3/issues/5456</a>&nbsp;[fixed]<br> <a href="https://github.com/Z3Prover/z3/issues/5457">https://github.com/Z3Prover/z3/issues/5457</a>&nbsp;[fixed]&nbsp;<br> <a href="https://github.com/Z3Prover/z3/issues/5460">https://github.com/Z3Prover/z3/issues/5460</a>&nbsp;[fixed]<br> <a href="https://github.com/Z3Prover/z3/issues/5468">https://github.com/Z3Prover/z3/issues/5468</a>&nbsp;[fixed]&nbsp;<br> <a href="https://github.com/Z3Prover/z3/issues/5488">https://github.com/Z3Prover/z3/issues/5488</a>&nbsp;[fixed]<br> <a href="https://github.com/Z3Prover/z3/issues/5502">https://github.com/Z3Prover/z3/issues/5502</a>&nbsp;[duplicate]<br> <a href="https://github.com/Z3Prover/z3/issues/5508">https://github.com/Z3Prover/z3/issues/5508</a>&nbsp;[reported]<br> <a href="https://github.com/Z3Prover/z3/issues/5423">https://github.com/Z3Prover/z3/issues/5423</a>&nbsp;[invalid]&nbsp;</p>