Alt-Ergo-Fuzz: A fuzzer for the Alt-Ergo SMT solver.

• CVC5.
• AFL.
• Alt-Ergo's compilation requirements + the crowbar OCaml library.

(P.S: The following commands assume that you're placed at the root of the repo)

make
./aef/init.sh #to generate necessary folders/files for the fuzzer

To run the fuzzer:

./aef/fuzz.sh

Optional command line arguments:

  -tf, --to-files
    Doesn't open a terminal but redirects the output to a file in
    "./fuzz_output/fop{num}.txt".
  -pm NBCORES, --parallel-mode=NBCORES
    Runs the fuzzer in the parallel mode using NBCORES cores (if they are
    availabe).
  -t TIMEOUT, --timeout=TIMEOUT
    Sets the timeout of every run to TIMEOUT (in milliseconds).
  -m MEMLIMIT, --memory=MEMLIMIT
    Sets the memory consumption limit of every run to MEMLIMIT (in
    megabytes).

When a crash happens : (aka: total crashes > 0)

For each crash a file is created under: ./aef/store/{foldername}/

Containing information about what caused the crash in a marshalled file.

{foldername} is the name of the subfolder under which the crash file is stored, and it represents the type of error that caused the crash, it can be one of the following: [internalcrash|outofmemory|stackoverflow|timeout|other].

It can be done by running:

./_build/default/aef/main.exe [-r|--rerun] [-i|--input] {ipf}

Which reruns the solvers on the list of SMT statements that caused the crash.

If the option [-v|--verbose] is provided, then it will print the original answers and the exception that was raised during the crash, as well as the new answers.

The list of SMT statements that caused some crash can be translated to the SMT-LIB2 standard or Alt-Ergo's native langauge and printed into a file by running:

./_build/default/aef/main.exe [-t|--translate] [alt-ergo|smt-lib2] [-i|--input] {ipf} [-o|--output] {opf[.ae|.smt2]}