Hi everyone
I want to extract the exact sequence of the program's instructions.But I have
a problem when I do this.
the source code like this:
int get_sign(/*int x*/) {
int x, ret;
klee_make_symbolic(&x, sizeof(x), "x");
if (x == 0)
ret = 0;
if (x < 0)
ret = x-1;
else
ret = x+1;
klee_assert(ret>=0);
return ret;
}
and I use llvm-dis command get the human-readable llvm-bitcode like this:
define i32 @get_sign() nounwind {
entry:
%retval = alloca i32
%0 = alloca i32
%x = alloca i32
%ret = alloca i32
%"alloca point" = bitcast i32 0 to i32
call void @llvm.dbg.declare(metadata !{i32* %x}, metadata !7), !dbg !9
call void @llvm.dbg.declare(metadata !{i32* %ret}, metadata !10), !dbg !9
%x1 = bitcast i32* %x to i8*, !dbg !11
call void @klee_make_symbolic(i8* %x1, i64 4, i8* getelementptr inbounds ([2
x i8]* @.str, i64 0, i64 0)) nounwind, !dbg !11
%1 = load i32* %x, align 4, !dbg !12
%2 = icmp eq i32 %1, 0, !dbg !12
br i1 %2, label %bb, label %bb2, !dbg !12
bb: ; preds = %entry
store i32 0, i32* %ret, align 4, !dbg !13
br label %bb2, !dbg !13
bb2: ; preds = %bb, %entry
%3 = load i32* %x, align 4, !dbg !14
%4 = icmp slt i32 %3, 0, !dbg !14
br i1 %4, label %bb3, label %bb4, !dbg !14
bb3: ; preds = %bb2
%5 = load i32* %x, align 4, !dbg !15
%6 = sub nsw i32 %5, 1, !dbg !15
store i32 %6, i32* %ret, align 4, !dbg !15
br label %bb5, !dbg !15
bb4: ; preds = %bb2
%7 = load i32* %x, align 4, !dbg !16
%8 = add nsw i32 %7, 1, !dbg !16
store i32 %8, i32* %ret, align 4, !dbg !16
br label %bb5, !dbg !16
bb5: ; preds = %bb4, %bb3
%9 = load i32* %ret, align 4, !dbg !17
%10 = icmp slt i32 %9, 0, !dbg !17
br i1 %10, label %bb6, label %bb7, !dbg !17
bb6: ; preds = %bb5
%11 = call i32 (...)* @__assert_fail(i8* getelementptr inbounds ([7 x i8]*
@.str1, i64 0, i64 0), i8* getelementptr inbounds ([11 x i8]* @.str2, i64 0,
i64 0), i32 17, i8* getelementptr inbounds ([9 x i8]*
@__PRETTY_FUNCTION__.1541, i64 0, i64 0)) nounwind, !dbg !17
br label %bb7, !dbg !17
bb7: ; preds = %bb6, %bb5
%12 = load i32* %ret, align 4, !dbg !18
store i32 %12, i32* %0, align 4, !dbg !18
%13 = load i32* %0, align 4, !dbg !18
store i32 %13, i32* %retval, align 4, !dbg !18
br label %return, !dbg !18
return: ; preds = %bb7
%retval8 = load i32* %retval, !dbg !18
ret i32 %retval8, !dbg !18
}
then I use some code to get the instructions' sequence,like this:
for (itKF = kmodule->functionMap.begin(); itKF != kmodule->functionMap.end();
++itKF) { //print the instructions' info in klee's way
KFunction *kf = itKF->second;
for (unsigned i=0; i<kf->numInstructions; ++i) {
KInstruction *ki = kf->instructions[i];
llvm::Instruction *inst = ki->inst;
const InstructionInfo *info = ki->info;
// if (std::find(fullTrace.begin(), fullTrace.end(), info->line) !=
fullTrace.end()) {
*msg << info->line << " " << info->assemblyLine << " " <<
inst->getOpcodeName() << "\n";
// }
}
}
llvm::Module *module = kmodule->module;
//print the instructions' info in llvm's way
for (llvm::Module::iterator itf = module->begin(); itf != module->end();
++itf) {
llvm::Function *f = itf;
for (llvm::Function::iterator itb = f->begin(); itb != f->end(); ++itb)
{
llvm::BasicBlock *bb = itb;
for (llvm::BasicBlock::iterator iti = bb->begin(); iti !=
bb->end(); ++iti) {
llvm::Instruction *i = iti;
*msg << i->getOpcodeName() << "\n";
}
*msg << "\n";
}
}
but I get the result like this:
I use the annotation to show my problems,so I do not know why this happen.Does
the code which I used to extract the instruction have something wrong or the
klee do some optimization to the llvm-bitcode? Can you help me? thank you very
much!
24 70 alloca
24 71 alloca
24 72 alloca
24 73 alloca
24 74 bitcast
24 75 bitcast
24 76 call
26 77 call
26 78 store
30 79 store
30 80 load
30 81 store
30 82 load
30 83 ret
9 13 alloca
9 14 alloca
9 15 alloca
9 16 alloca
9 17 bitcast
9 18 bitcast
9 19 call
10 20 load
10 21 icmp
10 22 br
11 25 store
11 26 br
13 29 load
13 30 icmp
14 31 load //the load instruction should be after the br instuction in
our soucrce llvm bit-code
13 32 br
14 35 sub
14 36 store
14 37 br
16 40 add //here lost the load instruction
16 41 store
16 42 br
17 45 load
17 46 icmp
17 47 br
17 50 call
17 51 unreachable
18 54 load
18 55 store
18 56 load
18 57 store
18 58 load
18 59 ret
alloca
alloca
alloca
alloca
bitcast
bitcast
call
load
icmp
br
store
br
load
icmp
load //the load instruction should be after the br instuction in our soucrce
llvm bit-code
br
sub //here lost the load instruction
store
br
add //here lost the load instruction
store
br
load
icmp
br
call
unreachable
load
store
load
store
load
ret
Yi Zhou
Institute Of Software
Chinese Academy of Sciences
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
