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.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
