Examples

Example 1

Consider the program test.c:

#include "clam/clam.h"

int main() {
  int k = nd_int();
  int n = nd_int();
  __CRAB_assume (k > 0);
  __CRAB_assume (n > 0);
  
  int x = k;
  int y = k;
  while (x < n) {
    x++;
    y++;
  }
  __CRAB_assert (x >= y);
  __CRAB_assert (x <= y);  
  return 0;
}

Clam provides a Python script called clam.py. Type the command:

clam.py --crab-check=assert test.c

Important: the first thing that clam.py does is to compile the C program into LLVM bitcode by using Clang. Since Clam is based on LLVM 10, the version of clang must be 10 as well.

The header file clam.h contains a list of external functions (without body) that have special meaning for Crab. For instance, __CRAB_assume, __CRAB_assert, etc.

When the above command succeeds, then the output should be something like this:

/** INVARIANTS: {} **/
  havoc(_3) /*   %_3 = call i32 %_2() #2*/;
  havoc(_5) /*   %_5 = call i32 %_4() #2*/;
  assume(-_3 <= -1);
  assume(-_5 <= -1);
  .01 = _3;
  .0 = _3;
/** INVARIANTS: ({}, {_3 -> [1, +oo], _5 -> [1, +oo], .01 -> [1, +oo], .0 -> [1, +oo], .01-_3<=0, .0-_3<=0, _3-.01<=0, .0-.01<=0, _3-.0<=0, .01-.0<=0}) **/
  goto _.01;
_.01:
/** INVARIANTS: ({}, {_3 -> [1, +oo], _5 -> [1, +oo], .01 -> [1, +oo], .0 -> [1, +oo], _3-.01<=0, .0-.01<=0, _3-.0<=0, .01-.0<=0}) **/
  goto __@bb_5,__@bb_6;
__@bb_5:
  assume(-_5+.01 <= -1);
  goto _12;
_12:
/** INVARIANTS: ({}, {_3 -> [1, +oo], _5 -> [2, +oo], .01 -> [1, +oo], .0 -> [1, +oo], .01-_5<=-1, _3-_5<=-1, .0-_5<=-1, _3-.01<=0, .0-.01<=0, _3-.0<=0, .01-.0<=0}) **/
  _13 = .01+1;
  _br2 = .0+1;
  .01 = _13;
  .0 = _br2;
/** INVARIANTS: ({}, {_3 -> [1, +oo], _5 -> [2, +oo], .0 -> [2, +oo], _13 -> [2, +oo], _br2 -> [2, +oo], .01 -> [2, +oo], .01-_5<=0, _3-_5<=-1, .0-_5<=0, _13-_5<=0, _br2-_5<=0, _br2-.0<=0, _3-.0<=-1, .01-.0<=0, _13-.0<=0, .01-_13<=0, _3-_13<=-1, .0-_13<=0, _br2-_13<=0, .0-_br2<=0, _3-_br2<=-1, .01-_br2<=0, _13-_br2<=0, _13-.01<=0, _3-.01<=-1, .0-.01<=0, _br2-.01<=0}) **/
  goto _.01;
__@bb_6:
  assume(_5-.01 <= 0);
  goto _15;
_15:
/** INVARIANTS: ({}, {_3 -> [1, +oo], _5 -> [1, +oo], .01 -> [1, +oo], .0 -> [1, +oo], _3-.01<=0, .0-.01<=0, _5-.01<=0, _3-.0<=0, .01-.0<=0, _5-.0<=0}) **/
  // loc(file=none line=-1 col=-1) id=1 Result:  OK
  assert(-.01+.0 <= 0)   /* loc(file=none line=-1 col=-1) id=1 */;
  // loc(file=none line=-1 col=-1) id=2 Result:  OK
  assert(.01-.0 <= 0)   /* loc(file=none line=-1 col=-1) id=2 */;
  @V_1 = 0;
/** INVARIANTS: ({}, {_3 -> [1, +oo], _5 -> [1, +oo], .01 -> [1, +oo], .0 -> [1, +oo], @V_1 -> [0, 0], _3-.01<=0, .0-.01<=0, _5-.01<=0, _3-.0<=0, .01-.0<=0, _5-.0<=0}) **/

It shows the Control-Flow Graph analyzed by Crab (called CrabIR) together with the invariants inferred for function main that hold at the entry and and the exit of each basic block.

Note that Clam does not provide a translation from the basic block identifiers and variable names to the original C program. The reason is that Clam does not analyze C but instead the corresponding LLVM bitcode generated after compiling the C program with Clang. To help users understanding the invariants Clam provides an option to visualize the CFG of the function described in terms of the LLVM bitcode:

clam.py test.c --llvm-dot-cfg

and you should see a screen with a similar CFG to this one:

Since we are interested at the relationships between x and y after the loop, the LLVM basic block of interest is _15 and the variables are .01 and .0, for x and y, respectively.

With this information, we can look back at the invariants inferred by our tool and see the linear constraints:

.0-.01<=0, ... , .01-.0<=0

Example 2

Consider the next program:

    #include "clam/clam.h"
    int a[10];
    int main (){
       int i;
       for (i=0;i<10;i++) {
         if (nd_int())
            a[i]=0;
         else 
            a[i]=5;
       }
       int res = a[i-1];
       return res;
    }

and type

clam.py test.c --crab-track=sing-mem --crab-opt=add-invariants --crab-opt-invariants-loc=all --crab-promote-assume -o test.crab.bc
llvm-dis test.crab.bc

The content of test.crab.bc should be similar to:

    define i32 @main() #0 {
    entry:
       br label %loop.header
    loop.header:   ; preds = %loop.body, %entry
       %i.0 = phi i32 [ 0, %entry ], [ %_br2, %loop.body ]
       %crab_2 = icmp ult i32 %i.0, 11
       call void @llvm.assume(i1 %crab_2) #2
       %_br1 = icmp slt i32 %i.0, 10
       br i1 %_br1, label %loop.body, label %loop.exit
    loop.body:   ; preds = %loop.header
       call void @llvm.assume(i1 %_br1) #2
       %crab_14 = icmp ult i32 %i.0, 10
       call void @llvm.assume(i1 %crab_14) #2
       %_5 = call i32 (...)* @__CRAB_nd() #2
       %_6 = icmp eq i32 %_5, 0
       %_7 = sext i32 %i.0 to i64
       %_. = getelementptr inbounds [10 x i32]* @a, i64 0, i64 %_7
       %. = select i1 %_6, i32 5, i32 0
       store i32 %., i32* %_., align 4
       %_br2 = add nsw i32 %i.0, 1
       br label %loop.header
    loop.exit:   ; preds = %loop.header
       %_11 = add nsw i32 %i.0, -1
       %_12 = sext i32 %_11 to i64
       %_13 = getelementptr inbounds [10 x i32]* @a, i64 0, i64 %_12
       %_ret = load i32* %_13, align 4
       %crab_23 = icmp ult i32 %_ret, 6
       call void @llvm.assume(i1 %crab_23) #2
       ret i32 %_ret
    }

The special thing about the above LLVM bitcode is the existence of @llvm.assume instructions (see here for its semantics). For instance, the instruction @llvm.assume(i1 %crab_2) indicates that %i.0 is between 0 and 10 at the loop header. Also, @llvm.assume(i1 %crab_23) indicates that the result of the load instruction at block loop.exit is between 0 and 5.