Resolving indirect calls about clam

[caballa]

I've realized that the option --devirt-functions was not using LLVM DSA to resolve indirect calls. It did that in the past but it was changed some time ago. Instead, it was using types to resolve calls. I also realized there were some bugs.
I've committed some changes and changed the option --devirt-functions. Please read the message of the commit 4c1edd2

Coming back to your example. I modified it a bit so that x is not dead, otherwise LLVM might be too smart:

extern void __CRAB_assert(int);

int a (void);
int b (void);

int main(int argc, char** argv) {
  int (*p) (void);
  if (argc == 1)
      p = a;
  else
      p = b;
  int x = p();
  __CRAB_assert(x>=5);
  return 0;
}

int a() {return 10;}
int b() {return 5;}

You can analyze this program using the command

crabllvm.py -O0 --devirt-functions=types --crab-inter --crab-check=assert  ../test.c 

You can add the option -oll=test.ll to see the LLVM bitcode that it's actually analyzed. If you open test.ll you will see how indirect calls are translated to a bunch of direct calls.

The crab-llvm output should be something like this:

@V_5:int declare main(argc:int)
_1:
/**
  INVARIANTS: ({}, {})
**/
  _3 = call seahorn.bounce();
  _4 = (-_3 <= -5);
  assert (_4);
  @V_5 = 0;
  return @V_5;
/**
  INVARIANTS: ({_4 -> true}, {@V_5 -> [0, 0], _3 -> [5, 10]})
**/


@V_7:int declare a()
_ret:
/**
  INVARIANTS: ({}, {})
**/
  @V_7 = 10;
  return @V_7;
/**
  INVARIANTS: ({}, {@V_7 -> [10, 10]})
**/


@V_8:int declare b()
_ret:
/**
  INVARIANTS: ({}, {})
**/
  @V_8 = 5;
  return @V_8;
/**
  INVARIANTS: ({}, {@V_8 -> [5, 5]})
**/


UnifiedRetVal:int declare seahorn.bounce()
entry:
/**
  INVARIANTS: ({}, {})
**/
  havoc(sc1);
/**
  INVARIANTS: ({}, {})
**/
  goto __@bb_1,__@bb_2;
__@bb_1:
  goto b;
b:
/**
  INVARIANTS: ({}, {})
**/
  _1 = call b();
  UnifiedRetVal = _1;
/**
  INVARIANTS: ({}, {UnifiedRetVal -> [5, 5], _1 -> [5, 5]})
**/
  goto UnifiedReturnBlock;
UnifiedReturnBlock:
/**
  INVARIANTS: ({}, {UnifiedRetVal -> [5, 10]})
**/
  return UnifiedRetVal;
/**
  INVARIANTS: ({}, {UnifiedRetVal -> [5, 10]})
**/

__@bb_2:
  goto a;
a:
/**
  INVARIANTS: ({}, {})
**/
  _0 = call a();
  UnifiedRetVal = _0;
/**
  INVARIANTS: ({}, {UnifiedRetVal -> [10, 10], _0 -> [10, 10]})
**/
  goto UnifiedReturnBlock;

************** ANALYSIS RESULTS ****************
1  Number of total safe checks
0  Number of total error checks
0  Number of total warning checks
************** ANALYSIS RESULTS END*************

The output consists of the CFGs for each function analyzed by Crab and the invariants inferred by Crab that hold at the entry and at the exit of each block. There is a function here called seahorn.bounce that it was not in the original program. That function is how the option --devirt-functions=types translates an indirect call to multiple direct calls.

In this case, using the option --devirt-functions=dsa wouldn't make a difference. Let us try now to analyze this slightly different program:

extern void __CRAB_assert(int);

int a (void);
int b (void);
int c (void);
int d (void);

int main(int argc, char** argv) {
  int (*p) (void);
  int (*q) (void);  
  
  if (argc == 1) {
      p = a;
      q = c;
  } else {
      p = b;
      q = d;
  }

  int x = p();
  int y = q();

  __CRAB_assert(x>= 5);
  __CRAB_assert(y>= 15);    
  return 0;
}

int a() {return 10;}
int b() {return 5;}
int c() {return 15;}
int d() {return 20;}

With the command crabllvm.py -O0 --devirt-functions=types --crab-inter --crab-check=assert test.c the output would be:

....
************** ANALYSIS RESULTS ****************
1  Number of total safe checks
0  Number of total error checks
1  Number of total warning checks
************** ANALYSIS RESULTS END*************

But, if you try the command:

crabllvm.py -O0 --devirt-functions=dsa --crab-inter --crab-check=assert test.c

The output is

....
************** ANALYSIS RESULTS ****************
2  Number of total safe checks
0  Number of total error checks
0  Number of total warning checks
************** ANALYSIS RESULTS END*************

Again, use the option -oll=test.ll to see the generated LLVM bitcode and convince yourself how indirect calls are handled by types and dsa.

[tregua87]

Hi @caballa !
Thank you very much for your support.
I guess this tool is exactly what I am looking for :)