Usage

Video Demo

LLBMC: The Low-Level Bounded Model Checker

Example 1: Detecting Memory Access Violations

Consider, as a first example, the following C program:

 1 /* Example 1 (ex1.c) */
 2 
 3 int a[3];
 4 
 5 void foo(int m)
 6 {
 7   int i;
 8 
 9   for (i = 0; i < m; i++)
10     a[i] = i;  // memory access violation, if m > 3
11 }

In line 10 of this program (ex1.c), a memory access error occurs if m > 3. To run LLBMC on this example, we first have to compile it to LLVM IR (intermediate representation, bitcode) using LLVM's clang compiler: 

clang -c -g -emit-llvm ex1.c -o ex1.bc
clang produces the bitcode file 'ex1.bc', which we can then pass to LLBMC: 
llbmc ex1.bc
LLBMC reports—among others—that the default loop iteration bound (zero in this case) has not been sufficient for the check
(often LLBMC can determine a suitable loop bound automatically, though):

Show/Hide Complete Output 
Running LLBMC with automatically determined function call depth and
at most 0 iterations for loops with non-derivable trip count.

Loop iteration bound is not sufficient. The program analysis is thus not complete.

Increase the limit using "--max-loop-iterations=<uint>" or switch off
loop unroll checks with the option "--no-max-loop-iterations-checks".

We thus tell LLBMC, as suggested, to use a larger loop iteration bound using the option --max-loop-iterations=<uint>.
A bound of 4 is sufficient: 

  llbmc ex1.bc --max-loop-iterations=4
LLBMC then correctly detects a write access error in line 10 of the program:

Show/Hide 
Error detected.

Assertion failed: Memory write access error in the store instruction
  store i32 %i.0.3, i32* %arrayidx.3

Source file: ex1.c
Line / column number: 10:5

For detailed information about when the error occurs, we run LLBMC with the additional option --counterexample. It then produces an error trace (on the level of LLVM's intermediate representation), which shows exactly how the program gets to the error location. In this case, we can see that the error occurs, e.g., when i=3 and m=6.

Show/Hide 
Counter-example:
================

@a = common global [3 x i32] zeroinitializer ; @ 0x1ffffff4

define void @foo(i32 %m) {
  ; i32 %m = 6
  ...
  %i.0.3 = phi i32 [ %inc.3, %for.inc.3 ], [ %inc.2, %for.inc.2 ]  ; 3
  %arrayidx.3 = getelementptr inbounds [3 x i32]* @a, i32 0, i32 %i.0.3  ; 0x20000000
  store i32 %i.0.3, i32* %arrayidx.3  ; INVALID MEMORY ACCESS
  ...
This concludes our first example.

Example 2: Functional Equivalence

In our second example, we want to check whether two functions exhibit equivalent behavior. Both functions are intended to compute the population count of a 32-bit integer (i.e. the number of 1-bits in its binary representation). We therefore set up a test function (called __llbmc_main in our example), which calls both functions with an uninitalized input variable x, and then compares their results using __llbmc_assert. This has the effect, that LLBMC searches through all possible values of x for a value on which the assertion fails. (Instead of using an undetermined parameter for function __llbmc_main, we could also have set variable x to an undefined—and thus non-deterministically chosen—value explicitly using LLBMC's function __llbmc_nondef_uint32_t.) 

 1 /* Example 2 (ex2.c) */
 2 
 3 #include <stdint.h>
 4 #include "llbmc.h"
 5 
 6 uint32_t optimized_popcount(uint32_t x)
 7 {
 8     x = x - ((x >> 1 ) & 0x55555555);
 9     x = (x & 0x33333333) + ((x >> 2) & 0x33333333);
10     x = (x + (x >> 4)) & 0x0F0F0F0F;
11     x += (x >> 8);
12     x += (x >> 16);
13     return x & 0x0000003F;
14 }
15 
16 uint32_t reference_popcount(uint32_t x)
17 {
18     int i, s = 0;
19     for(i = 0; i < 32; ++i)
20         if(x & (1 << i))
21             s++;
22     return s;
23 }
24 
25 void __llbmc_main(uint32_t x)
26 {
27     uint32_t opt = optimized_popcount(x);
28     uint32_t ref = reference_popcount(x);
29 
30     __llbmc_assert(opt == ref); // equivalence check
31 }

When we compile the program with clang and run LLBMC on its bitcode file, using the commands 

clang -c -g -I. -emit-llvm ex2.c -o ex2.bc
llbmc ex2.bc
(-I. is needed for the include file llbmc.h) we obtain this output from LLBMC, which shows that the assertion holds and the functions are indeed equivalent:

Show/Hide 
Running LLBMC with automatically determined function call depth and
at most 0 iterations for loops with non-derivable trip count.

No error detected.