FV: Practical Exercise 4: Verifying C with CBMC

CBMC resources

• CBMC Homepage.
• CPROVER Manual. This is the main documentation page on CBMC and related tools.
• Conference paper introducing CBMC (2004) 
• Short tutorial on CBMC
• Preview of 32 page book chapter on CBMC (Feb 2023)

Lab instructions

1. Download the files cbmc-lab-1_0.zip and cbmc-lab-2.zip to some new directory in your DICE file-space, cd to that directory in a shell,  and unpack the zip files:

   unzip cbmc-lab-1_0.zip 
   unzip cbmc-lab-2.zip

   Two zip files are needed here because of an OpenCourse website file size restriction.  You should find now that your directory also contains the x86 Linux executable files cbmc, goto-instrument, and goto-cc, and the example C files

   file1.c           
   file2.c           
   binsearch.c           
   lock-example.c           
   lock-example-fixed.c          
   max3.c  
   mult.c

   If you are wanting to run the lab on Windows or macOS rather than in an x86 Linux environment, you will need to download and use the alternate appropriate executables from the CBMC Homepage. The instructions following assume you are working on Linux.

2. To run the cbmc executable from the directory you have unpacked the files to, type ./cbmc. E.g.

   ./cbmc file1.c --show-properties --bounds-check --pointer-check

   Type

   ./cbmc --help

   to see a full range of options accepted by CBMC. Below, the "./"prefix has been dropped from all the invocations of the CBMC executable files. Either add it back in each case, or put the executables in a directory that you add to your PATH.

3. Follow the CBMC short tutorial which makes use of the first 5 C files listed above. Here are a few further notes on some of this tutorial's sections:

   • Verifying Modules:

     Try changing the i < 10 to i <= 10 and observe the bounds check now fails.

   • Loop Unwinding:

     See how the unwinding assertion fails if the unwind number is reduced below 6. Note the "option --property" at the section end should be "option --trace".

   • Unbounded Loops:

     Use commands like

     cbmc lock-example.c --unwind 2

     Add the option --trace to generate a counter-example trace and note how the counter-example points to the problem with the code. Ignore the suggestion to use the option --unwinding-assertions; this is not appropriate here as it will always fail. See lock-example-fixed.c for a fixed version of the code.

4. Browse the description of CBMC's capabilities for generating tests for code coverage. Ignore the pid.c example discussed there and use the much simpler max3.c provided in the lab.zip file you downloaded. Use commands such as

   cbmc max3.c --function max3 --cover decision

   Try replacing decision with condition or mcdc. For each of these kinds of coverage, can CBMC achieve full coverage? If not, why not? Try adding the option --xml-ui to see fuller information on the inputs needed for each test case.

5. Here we explore CBMC's internals, using the multiplication example from class. First let's compile the C source mult.c to a goto binary mult.gb

   goto-cc mult.c -o mult.gb

   The goto binary represents programs using control flow graphs. To see the graphs for this example, generate a Graphviz dot file for the goto binary and generate a pdf of the graph from this.

   goto-instrument mult.gb mult.dot --dot   
   dot -Tpdf mult.dot -o mult.pdf

   View the pdf using some suitable pdf viewer. On DICE Linux:

   evince mult.pdf

   Transform the goto binary by unrolling the loop 2 times and inserting an assume statement.

   goto-instrument mult.gb mult-u2.gb --unwind 2

   Using the previously shown commands, you could generate a pdf of the new goto binary to see the unrolled loop. Alternatively you can translate the binary back into C code:

   goto-instrument mult-u2.gb --dump-c 

   For a compact presentation of the verification condition associated with the assert statement in the main function, do

   cbmc mult-u2.gb --show-vcc --slice-formula

   The verification condition is shown as a sequent, with assumption clauses numbered with negative numbers (like "{-14}" here) and conclusion clauses with positive numbers (here "{1}"). In general such sequents are read as claiming that the conjunction of the assumptions implies the disjunction of the conclusions (or just the conclusion if there is only one conclusion clause).

   In this VC sequent, you should see that the multiply function has been inlined and the SSA (single static assignment) tranformation has been applied. The --slice-formula option makes CBMC simplify the VC so the VC focuses on just what is relevant to the conclusion to be proved. Try leaving the option off to see its effect.

   To see an SMTLib version of the VC, execute

   cbmc mult-u2.gb --smt2 --outfile mult.smt2

   You could try running Z3 on this SMTLib formula, or, assuming Z3 is on your path (say from Practical Exercise 2),

   cbmc mult-u2.gb --z3

   ought to cause CBMC to call Z3 on the VC.