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