[crab-llvm] Invariants aren't inserted into LLVM bitcode

crabllvm_log.txt

$ crabllvm.py ex.c --crab-dom=zones --crab-track=arr --crab-add-invariants=all -o test.crab.bc
CRAB WARNING: unsigned inequality -_7 <=_u -1338 skipped by split_dbm domain
CRAB WARNING: unsigned inequality _7 <=_u 1337 skipped by split_dbm domain

@V_23:int declare main(:int,:ptr)
_3:
/**
  INVARIANTS: ({}, {})
**/
  _4 = &() + 4;
  _5 = &(_4) + 0;
  _6 = *(_5);
  _7 = array_load(@V_6,_6,sz=4);
  _9 = _7*3;
  _10 = _9&32;
  _11 = _7*7;
  _12 = _11+-91;
 _13 = ite(-_7 <=_u -1338,_12,_10);
/**
  INVARIANTS: ({}, {_12-_11<=-91, _11-_12<=91})
**/
  goto __@bb_1,__@bb_2;
__@bb_1:
  assume(_7 = 1433958485);
  goto _15;
_15:
/**
  INVARIANTS: ({}, {_7 -> [1433958485, 1433958485], _12-_11<=-91, _11-_12<=91})
**/
  _puts1 = &(str.1) + 0;
  havoc(puts1);
/**
  INVARIANTS: ({}, {_7 -> [1433958485, 1433958485], _12-_11<=-91, _11-_12<=91})
**/
  goto _19;
_19:
/**
  INVARIANTS: ({}, {_12-_11<=-91, _11-_12<=91})
**/
  _20 = &(.str.2) + 0;
  havoc(_ret);
  @V_23 = 0;
  return @V_23;
/**
  INVARIANTS: ({}, {@V_23 -> [0, 0], _12-_11<=-91, _11-_12<=91})
**/

__@bb_2:
  assume(_7 != 1433958485);
  goto _17;
_17:
/**
  INVARIANTS: ({}, {_12-_11<=-91, _11-_12<=91})
**/
  _puts = &(str) + 0;
  havoc(puts);
/**
  INVARIANTS: ({}, {_12-_11<=-91, _11-_12<=91})
**/
  goto _19;
CRAB WARNING: unsigned inequality -_7 <=_u -1338 skipped by split_dbm domain
CRAB WARNING: unsigned inequality _7 <=_u 1337 skipped by split_dbm domain
----------------------------------------------------------------------
BRUNCH_STAT Clang 0.02
BRUNCH_STAT CrabLlvm 0.01
BRUNCH_STAT CrabLlvmPP 0.01
----------------------------------------------------------------------

ex.c

#include <stdio.h>

unsigned a;
unsigned x;

int main(int argc, char const* argv[])
{
    a = *(unsigned *) argv[1];
    unsigned b = a;

    unsigned c = 1;
    if (a > 1337) {
        x = a - 13;
        c = 7;
    } else {
        x = 32;
        x ^= a * 3;
    }
    x *= c;

    if (b == 0x55787855)
        printf("SUCCESS\n");
    else
        printf("FAILURE\n");
    printf("0x%x", x);
    return 0;
}

new_main.crab.ll

define i32 @main(i32, i8**) local_unnamed_addr #0 {
_3:
  %_4 = getelementptr inbounds i8*, i8** %1, i32 1
  %_5 = bitcast i8** %_4 to i32**
  %_6 = load i32*, i32** %_5, align 4
  %_7 = load i32, i32* %_6, align 4
  %_8 = icmp ugt i32 %_7, 1337
  %_9 = mul i32 %_7, 3
  %_10 = xor i32 %_9, 32
  %_11 = mul i32 %_7, 7
  %_12 = add i32 %_11, -91
  %_13 = select i1 %_8, i32 %_12, i32 %_10
  %_br = icmp eq i32 %_7, 1433958485
  br i1 %_br, label %_15, label %_17

_15:                                              ; preds = %_3
  %crab_ = sub i32 0, %_7
  %crab_1 = icmp slt i32 %crab_, -1433958484
  call void @verifier.assume(i1 %crab_1) #2
  %puts1 = call i32 @puts(i8* getelementptr inbounds ([8 x i8], [8 x i8]* @str.1, i32 0, i32 0))
  br label %_19

_17:                                              ; preds = %_3
  %puts = call i32 @puts(i8* getelementptr inbounds ([8 x i8], [8 x i8]* @str, i32 0, i32 0))
  br label %_19

_19:                                              ; preds = %_17, %_15
  %_ret = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.str.2, i32 0, i32 0), i32 %_13) #2
  ret i32 0
}

old_main.crab.ll

define i32 @main(i32, i8**) local_unnamed_addr #0 {
_3:
  %_4 = getelementptr inbounds i8*, i8** %1, i32 1
  %_5 = bitcast i8** %_4 to i32**
  %_6 = load i32*, i32** %_5, align 4
  %_7 = load i32, i32* %_6, align 4
  %_8 = icmp ugt i32 %_7, 1337
  %_9 = mul i32 %_7, 3
  %_10 = xor i32 %_9, 32
  %_11 = mul i32 %_7, 7
  %_12 = add i32 %_11, -91
  %_13 = select i1 %_8, i32 %_12, i32 %_10
  %_br = icmp eq i32 %_7, 1433958485
  br i1 %_br, label %_15, label %_17

_15:                                              ; preds = %_3
  %crab_6 = zext i32 %_11 to i64
  %crab_8 = zext i32 %_12 to i64
  %crab_9 = sub nsw i64 %crab_8, %crab_6
  %crab_10 = icmp slt i64 %crab_9, -90
  call void @verifier.assume(i1 %crab_10) #2
  %crab_11 = zext i32 %_11 to i64
  %crab_13 = zext i32 %_12 to i64
  %crab_14 = sub nsw i64 %crab_11, %crab_13
  %crab_15 = icmp slt i64 %crab_14, 92
  call void @verifier.assume(i1 %crab_15) #2
  %puts1 = call i32 @puts(i8* getelementptr inbounds ([8 x i8], [8 x i8]* @str.1, i32 0, i32 0))
  br label %_19

_17:                                              ; preds = %_3
  %crab_16 = zext i32 %_11 to i64
  %crab_18 = zext i32 %_12 to i64
  %crab_19 = sub nsw i64 %crab_18, %crab_16
  %crab_20 = icmp slt i64 %crab_19, -90
  call void @verifier.assume(i1 %crab_20) #2
  %crab_21 = zext i32 %_11 to i64
  %crab_23 = zext i32 %_12 to i64
  %crab_24 = sub nsw i64 %crab_21, %crab_23
  %crab_25 = icmp slt i64 %crab_24, 92
  call void @verifier.assume(i1 %crab_25) #2
  %puts = call i32 @puts(i8* getelementptr inbounds ([8 x i8], [8 x i8]* @str, i32 0, i32 0))
  br label %_19

_19:                                              ; preds = %_17, %_15
  %_ret = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.str.2, i32 0, i32 0), i32 %_13) #2
  ret i32 0
}