CBMC-REPAIR

A property-driven tool for suggesting fence insertion using CBMC.

Download

• The tool can be downloaded from here.
• The benchmarks used can be downloaded from here.

Instructions

Installing

1. cbmc-repair requires the source of MiniSAT-2.2.0. Install these solvers in appropriate directories.
2. Download cbmc-repair.tgz in a directory.
3. Provide paths to directories where MiniSAT2 is installed in variable MINISAT2 in the file src/config.inc
4. Follow compilation instructions given in file COMPILING.

Running

• The general format is as follows cbmc --repair value [options] filename.c
• --repair is mandatory with valid values being tso:sc or pso:sc. Thus a command would look like cbmc --repair tso:sc filename.c
• By default, ROBMC algorithm with early termination is used. (ROBMC-ET)
• To use ROBMC algorithm without early termination add --no-early-termination (ROBMC)
• To use a remmex like approach use --no-reorder-optimization. (FI)
• To use a dfence style approach use --trace-enum. (TE)
• At most one of --trace-enum, --no-reorder-optimization and --no-early-termination should be used.
• With the default option or with --no-early-termination one can use --minbound NUM to specify the initial bound for ROBMC.

Loop related options

• For bounded loops (e.g. for(i=0;i<10;i++) CBMC automatically figures out the unrolling depth for the loops.
• For other loops the unrolling depth has to be given externally.
• --unwind NUM unrolls all the loops to the depth given by NUM.
• For unbounded loops, you also MUST provide --no-unwinding-assertions.
• To specify bounds for each loop individually, use --unwindset loop1:depth1,loop2:depth2
• To get the loop identifiers that needs to be used as loop1, loop2 in --unwindset run cbmc --show-loops filename.c. The identifiers will be of the form c::methodname.0

Running Benchmarks

• Script RUNSCRIPT.sh is provided in param-benchmarks/classic to run all the experiments.
• modify EXEC variable in the script to point to the cbmc executable in src/cbmc folder.
• You can use bash benchmark-gen.sh NUM to generate a C file of benchmark with parametric fragment added NUM times.
• Refer to instructions above to run the tool on this C file.
• The script runs the tool on all the benchmark on all 4 algorithms for parameter n from 2 to 40 and parameter K1 from 2 to 40. Adjust these parameter bounds using variables paramsize and k1size variables. Depending upon the bounds given, running all the experiments may take several days.

CONTACT US

Saurabh Joshi and Daniel Kroening Email : firstname.lastname@cs.ox.ac.uk