1. Marius Lindauer
  2. SpyBug

Overview

HTTPS SSH

SpyBug

a tool to find bugs in algorithms wrt to their configuration spaces

License

It is distributed under the GNU Public License. See COPYING for details regarding the license.

Overview

SpyBug is a tool to find bugs in software (in particular in SAT solvers). It is written in Python and is based on interfaces of AClib (www.aclib.net) and the algorithm configurator SMAC. Please see SMAC Manual

Requirements

Installation

git clone https://mlindauer@bitbucket.org/mlindauer/spybug.git

Package Content

example/ - directory containing a small set of instances and Riss

scritps/ - directory containing some helper scripts

SpyBug/ - directory containing the python scripts

COPYING - license file

README.md - this file

SpyBug.py - main file to call SpyBug

Usage

See:

$ python SpyBug.py -h

Toy Test example

cd SpyBug/unit_tests/files
python ../../../SpyBug.py --scen bug.scenario

One of our unit tests provides a very simple toy example. The algorithm has four parameters and each has the domain {0,1}. (see bug.pcs) An artificial bug will triggered, if (p2==1 and p4==1) or (p3==1).

SpyBug will find these bugs very fast and will minimize the erroneous configurations to the minimal reasons (see above).

The output should look like this:

[INFO] Iteration: 1 (reported in an exponential schedule)
[INFO] Iteration: 2 (reported in an exponential schedule)
[INFO] Iteration: 4 (reported in an exponential schedule)
[INFO] We have probably found a bug in -p2 0 -p3 1 -p1 0 -p4 1 on blub2 in iteration 5
[INFO] Minimal bug config: -p3 1
[INFO] New forbidden clause: [['p3', '1']]
[INFO] We have probably found a bug in -p2 1 -p3 0 -p1 1 -p4 1 on blub2 in iteration 7
[INFO] Minimal bug config: -p4 1 -p2 1
[INFO] New forbidden clause: [['p4', '1'], ['p2', '1']]
...

Example with Riss

cd example/
python ../SpyBug.py --scenario scenario_riss.txt --n 100000 --time_limit 100000

We provide a real use-case scenario for Spybug as an example to find bugs in the SAT solver Riss (version 427). Please note that Riss has 214 parameters and more than 10^86 possible configurations in a discretized space. Therefore, SpyBug will need some time to find the bugs in Riss.

All necessary files related to Riss and the problem instances are specified in scenario.txt, i.e., the runtime cutoff, the instance file (listing all problem instances), the target algorithm call (wrapper by Python script) and the parameter configuration space file:

cutoff_time = 5
instance_file = instances.txt
algo = python -u Riss427/SATCSSCWrapper.py --mem-limit 3000 --script Riss427/rissWrapper.py --sat-checker ../scripts/SAT --sol-file .
paramfile = Riss427/riss427-CSSC.pcs

The actual call to SpyBug requires only this scenario file. To specify how long SpyBug will search for bugs can be specified by the following options:

  --n_runs N_RUNS       maximal number of algorithm runs (default: 1000)
  --time_limit TIME_LIMIT
                        wallclock time limit [sec] (default: 3600)

Example with Glucose

We also provide a second example scenario with the SAT solver Glucose. The call to this scenario is:

python ../SpyBug.py --scenario scenario_glucose.txt

However, this scenario is only for illustration. We are not aware of any bug in Glucose on the used instances.

How to apply SpyBug to your SAT solver?

To apply SpyBug to your own solver, you have to only provide these components:

  1. The binary of your solver
  2. A (Python) script that generates the call string of your solver (see, e.g., example/Riss427/rissWrapper.py and example/glucose/glucoseWrapper.py). We maintain a generic wrapper for this task here.
  3. A parameter configuration space (pcs) file that defines the parameter space of your solver (see SMAC Manual for the format)
  4. A set of test instances (in a file that lists an instances per line)

If you provide all these components, you simply have to adapt the scenario file (see, e.g., example/scenario_riss.txt or example/scenario_glucose.txt). For algo, you have to replace Riss427/rissWrapper.py by your Python script.

How to apply SpyBug to your solver/algoritm from any another domain?

You mainly have to follow the same steps as described for SAT solvers. However, you need furthermore to write a Python function that checks whether the output of your solver/algorithm. Your script has to exactly implement the following function as the script for SAT solver, i.e., scripts/SATCSSCWrapper.py:

  • get_command_line_args()
  • save_failed_cmd()
  • process_results()

Tips

To speedup the process of finding bugs, you can run multiple independent runs of SpyBug in parallel. To this end, we recommend to use different random seeds:

  --seed SEED           random seed (default: 12345)

To get a more verbose output of SpyBug (e.g., to see all target algorithm calls), please use the verbose option and set it to DEBUG:

  --verbose {INFO,DEBUG}
                        verbosity level (default: INFO)

CONTACT

Marius Lindauer
University of Freiburg
lindauer@cs.uni-freiburg.de

Norbert Manthey
University of Dresden
norbert.manthey@tu-dresden.de