Diver-Artifact

Diver is a black-box fuzzer for SMT Solvers. This repository contains the artifact for reproducing the experiments in our paper accepted to ICSE 2023:

• Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations

Table of Contents

• Operating System and Hardware Requirements
• Artifact Structure
• Setup
  • Basic Testing
• Comparison with Existing Tools (Section IV-B)
• Utility of Diver's Techniques (Section IV-C)
• Instructions for Extending or Reusing Diver
• Tool Maintenance

1. Operating System and Hardware Requirements

Please see REQUIREMENTS.md for requirements for OS and Hardware environments.

2. Artifact Structure

• Diver: contains the implementation of Diver (the same with the one in the docker image that will be installed via Setup).
• Section_IV: contains benchmark formulas used in our experiments.
• scripts: contains scripts to run experiments and check corresponding results.
• tests: contains seed files that will be used for the basic testing.

3. Setup

Please see INSTALL.md for the installation. We provide a dockerized environment for reproducing the experimental results in our paper.

Basic Testing

To check whether the installlation was successful or not, run the following commands:

$ docker run -ti --rm -v `pwd`/test_output:/Diver/output jongwook123/diver:icse2023-artifact timeout 20 python3 __main__.py -i tests/seed1.smt2 -l QF_SLIA -s cvc -b /solvers/cvc5-1.0.1/build/bin/cvc5

If the installation and the testing were successful, you will obtain the log file test_output/test_output.log that looks similar to the below one:

[2023-01-21 10:52:56,059] Start!!!!
[2023-01-21 10:52:57,019] #Mutant 1 #Gen 2.0 Res sat ST 0.0 UT 0.0 TT 0.6809334754943848 GT 0.0009491443634033203 JT 0.1392803192138672
[2023-01-21 10:52:57,134] #Mutant 2 #Gen 3.0 Res sat ST 0.0 UT 0.0 TT 0.7067527770996094 GT 0.002476215362548828 JT 0.22508883476257324
[2023-01-21 10:52:57,425] #Mutant 3 #Gen 7.0 Res sat ST 0.0 UT 0.0 TT 0.7337627410888672 GT 0.004488706588745117 JT 0.4859590530395508
...

4. Comparison with Existing Tools (Section IV-B)

Please see Exp_SectionIV-B.md.

5. Utility of Diver's Techniques (Section IV-C)

Please see Exp_SectionIV-C.md.

6. Instructions for Reusing Diver

Please see USAGE.md to run Diver on new other formulas.

7. Tool Maintenance

Diver will be maintained in a seperate repository: https://github.com/kupl/Diver