[klee-dev] confuse how klee collect symbolic constraints

[meng qingkun]

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 4
10 %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 !20
25
26 ; <label>:9                                       ; preds = %6
27 store i32 -1, i32* %1, !dbg !22
28  br label %11, !dbg !22
29
30 ; <label>:10                                      ; preds = %6
31  store i32 1, i32* %1, !dbg !23
32  br label %11, !dbg !23
33
34 ; <label>:11                                      ; preds = %10, %9, %5
35  %12 = load i32* %1, !dbg !24
36  ret i32 %12, !dbg !24
37 }
38
39 ; Function Attrs: nounwind readnone
40 declare void @llvm.dbg.declare(metadata, metadata) #1
41
42 ; Function Attrs: nounwind uwtable

43 define i32 @main() #0 {
44 %1 = alloca i32, align 4
45 %a = alloca i32, align 4
46 store i32 0, i32* %1
47 call void @llvm.dbg.declare(metadata !{i32* %a}, metadata !25), !dbg !26
48 %2 = bitcast i32* %a to i8*, !dbg !27
49 call void @klee_make_symbolic(i8* %2, i64 4, i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0)), !dbg !27
50 %3 = load i32* %a, align 4, !dbg !28
51 %4 = call i32 @get_sign(i32 %3), !dbg !28
52 ret i32 %4, !dbg !28
53 }


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.
-------------- next part --------------
HTML attachment scrubbed and removed