[klee-dev] confuse how klee collect symbolic constraints

[Andrew Santosa]

Dear Qingkun,
I believe the following is close to your original source:
#include <klee/klee.h>
#include <assert.h>

int get_sign(int x) {

  if (x == 0) {
    return 0;
  }

  if (x < 0) {
    return -1;
  }

  return 1;
}


int main() {
  int a;
  klee_make_symbolic((char *) &a, sizeof(int), "a");
  return get_sign(a);
} 

On your questions:1. Yes, they should be the same address, from how KLEE handles a bitcast in Executor::executeInstruction:
  case Instruction::BitCast: {
    ref<Expr> result = eval(ki, 0, state).value;
    bindLocal(ki, state, result);
  }
   The first statement evaluates the 0-th argument and immediately assigns it to "result", which is then bound as the value of the instruction in the second line.2. The constraints that KLEE construct are in terms of the initial values of the symbolic variables. So, instead of using the temp variables %2, %3, %4 like what you mentioned, for your example KLEE build the constraints using only a as the symbolic variable, which symbolically represent the value of a at the callsite of klee_make_symbolic() in main(). This is because any variable whose value depend on some symbolic variables can always be represented using a function on those symbolic variables. In your example, the temp values can be represented using an identity function on a. Simply put, KLEE tracks the assignments and knows that those temp variables are a. At the first branching point in get_sign(), since it knows that %3 at Line 13 is a, KLEE figures out that the constraint to be added for each of the branches are:  (Eq 0 (ReadLSB w32 0 a)) and (Eq false (Eq 0 (ReadLSB w32 0 a))). Note that you can get KLEE to display ref<Expr> objects using dump() method: the first constraint is, in the more common syntax, a == 0 and the second one is a != 0.

I'm not an authority on KLEE, but I hope this helps.
Best,Andrew
 

    On Saturday, 25 June 2016, 12:15, meng qingkun <mengqingkun1988 at outlook.com> wrote:
 

  <!--#yiv3197942777 P {margin-top:0;margin-bottom:0;}-->Dear all klee developers
I recently debug klee source Dozens of times but I have problems to understand how klee collect and spread symbolic constraints. Take the get_sign.c as example which located at $kleedir/examples/get_sign. I have compile get_sign.c file to get_sign.bc and take it as one of the arguments. I use eclipse as klee debug IDE and the debug arguments are "--libc=uclibc /home/mqk/software/klee_se/klee/examples/get_sign/get_sign.bc". The LLVM IR version of main function is pasted below:
 8 define i32 @get_sign(i32 %x) #0 { 9  %1 = alloca i32, align 410 %2 = alloca i32, align 4 11 store i32 %x, i32* %2, align 4 12 call void @llvm.dbg.declare(metadata !{i32* %2}, metadata !15), !dbg !16 13 %3 = load i32* %2, align 4, !dbg !17 14 %4 = icmp eq i32 %3, 0, !dbg !17 15 br i1 %4, label %5, label %6, !dbg !17 16 17 ; <label>:5                                       ; preds = %0 18 store i32 0, i32* %1, !dbg !19 19 br label %11, !dbg !19 20 21 ; <label>:6                                       ; preds = %0 22 %7 = load i32* %2, align 4, !dbg !20 23 %8 = icmp slt i32 %7, 0, !dbg !20 24 br i1 %8, label %9, label %10, !dbg !2025 26 ; <label>:9                                       ; preds = %627 store i32 -1, i32* %1, !dbg !2228  br label %11, !dbg !222930 ; <label>:10                                      ; preds = %631  store i32 1, i32* %1, !dbg !2332  br label %11, !dbg !233334 ; <label>:11                                      ; preds = %10, %9, %535  %12 = load i32* %1, !dbg !2436  ret i32 %12, !dbg !2437 }3839 ; Function Attrs: nounwind readnone40 declare void @llvm.dbg.declare(metadata, metadata) #141 42 ; Function Attrs: nounwind uwtable43 define i32 @main() #0 {44 %1 = alloca i32, align 445 %a = alloca i32, align 4
46 store i32 0, i32* %147 call void @llvm.dbg.declare(metadata !{i32* %a}, metadata !25), !dbg !2648 %2 = bitcast i32* %a to i8*, !dbg !2749 call void @klee_make_symbolic(i8* %2, i64 4, i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0)), !dbg !2750 %3 = load i32* %a, align 4, !dbg !2851 %4 = call i32 @get_sign(i32 %3), !dbg !2852 ret i32 %4, !dbg !2853 }
Problems: 1. When klee execute the instruction of line 49, it shows that the value of first argument (represented as an Expr object) of klee_make_symbolic is an address. As far as I know the first argument is passed from line 45, does the variable %a and the first argument( both are represented by Expr objects) are share the same address? 2. How klee to construct and spread symbolic constraints though several temp variables? Take the branch at line 15 for example, in order to arrive line 18, variable %a( transmitted to temp variable %2 at line 48) firstly passes to variable %2(from function get_sign( i32 %x)) at line 11, then passes to variable %3 at line 13, then adds symbolic constraint through a equal expression at line 14, at last determine whether there should be a fork. Does klee construct a constraint like (%2( from main at line 48)==%2( from get_sign at line 10))&&==(%2( from get_sign at line 10)==%3( at line 13))&&(%4==0)?
I am a newby of klee so I could misunderstand some code. If someone can kindly give me some suggestions, detail explanation will be thankful. Thanks for the attention. 
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


  
-------------- next part --------------
HTML attachment scrubbed and removed