Hi Stefan,
for me the llvm code looks correct: There is an icmp instruction and
one way from entry over bb to bb3 and one way from entry over bb2 to bb3.
$ cat test.o.ll
...
define i32 @main(i32 %argc, i8** %argv) nounwind {
entry:
%argc_addr = alloca i32 ; <i32*> [#uses=1]
%argv_addr = alloca i8** ; <i8***> [#uses=1]
%retval = alloca i32 ; <i32*> [#uses=2]
%0 = alloca i32 ; <i32*> [#uses=3]
%c = alloca i32 ; <i32*> [#uses=2]
%"alloca point" = bitcast i32 0 to i32 ; <i32> [#uses=0]
call void @llvm.dbg.declare(metadata <badref>, metadata !0)
store i32 %argc, i32* %argc_addr
call void @llvm.dbg.declare(metadata <badref>, metadata !9)
store i8** %argv, i8*** %argv_addr
call void @llvm.dbg.declare(metadata <badref>, metadata !10)
%c1 = bitcast i32* %c to i8* ; <i8*> [#uses=1]
call void @klee_make_symbolic(i8* %c1, i32 4, i8* getelementptr
inbounds ([2 x i8]* @.str, i32 0, i32 0)) nounwind
%1 = load i32* %c, align 4 ; <i32> [#uses=1]
%2 = icmp sgt i32 %1, 10 ; <i1> [#uses=1]
br i1 %2, label %bb, label %bb2
bb: ; preds = %entry
store i32 1, i32* %0, align 4
br label %bb3
bb2: ; preds = %entry
store i32 0, i32* %0, align 4
br label %bb3
bb3: ; preds = %bb2, %bb
%3 = load i32* %0, align 4 ; <i32> [#uses=1]
store i32 %3, i32* %retval, align 4
br label %return
return: ; preds = %bb3
%retval4 = load i32* %retval ; <i32> [#uses=1]
ret i32 %retval4
}
...
Heinz
On 05/20/2010 08:55 PM, Stefan Bucur wrote:
> Heinz,
>
> Did you actually see the LLVM generated code? Perhaps a dead code
> elimination optimization removed the branch and you were left with a
> simple return statement. You should run llvm-dis on test.o, and check
> the test.o.ll generated file, and see if that branch actually got
> compiled in the code. If not, you should recompile the code with -O0
> and see what happens.
>
> Cheers,
> Stefan
>
> On Thu, May 20, 2010 at 8:18 PM, Heinz Riener<hriener at student.tugraz.at>
> wrote:
>>
>> I tried several different version of LLVM and klee but I always run into
>> this problem. It seems that the solver returns incorrect results but
>> all solver related unit tests pass. So, what's actually wrong? Have I
>> forgotten some settings in the configuration/building process?
>>
>> $ cat test.c
>> #include<klee/klee.h>
>> int main(int argc, char *argv[]) {
>> int c;
>> klee_make_symbolic(&c, sizeof c, "c");
>> if (c> 10)
>> return 1;
>> return 0;
>> }
>>
>> $ llvm-gcc -c -g -emit-llvm -I$KLEE_DIR/include test.c
>> $ klee -use-stp-query-pc-log test.o; cat klee-out-0/stp-queries.qlog
>>
>> KLEE: done: total instructions = 19
>> KLEE: done: completed paths = 1
>> KLEE: done: generated tests = 1
>>
>> # Query 0 -- Type: InitialValues, Instructions: 13
>> (query [] false)
>> # OK -- Elapsed: 0.000226092
>> # Solvable: true
>>
>> # Query 1 -- Type: InitialValues, Instructions: 13
>> array arr1[4] : w32 -> w8 = symbolic
>> (query [] (Eq false
>> (Slt 10
>> (ReadLSB w32 0 arr1))) []
>> [arr1])
>> # OK -- Elapsed: 0.00159706
>> # Solvable: false
>>
>> $ klee -debug-validate-solver test.o
>> KLEE: output directory = "klee-out-1"
>> klee: Solver.cpp:302: virtual bool
>> ValidatingSolver::computeValidity(const klee::Query&,
>> klee::Solver::Validity&): Assertion `0&& "invalid solver result
>> (computeValidity)"' failed.
>> 0 klee 0x08a468e8
>> zsh: abort klee -debug-validate-solver test.o
>>
>> Heinz
>>
>> On 05/19/2010 01:22 AM, Heinz Riener wrote:
>>> Dear all,
>>>
>>> I've updated (yesterday night) to the head SVN revisions of LLVM and
>>> Klee. Now, for every program Klee completes only one path. For instance,
>>> running Klee on the example of tutorial one, gives me the following output:
>>>
>>> $ llvm-gcc -c -g -emit-llvm islower.c
>>> $ klee islower.o
>>> KLEE: output directory = "klee-out-0"
>>>
>>> KLEE: done: total instructions = 27
>>> KLEE: done: completed paths = 1
>>> KLEE: done: generated tests = 1
>>>
>>> $ ktest-tool klee-last/test000001.ktest
>>> ktest file : 'klee-last/test000001.ktest'
>>> args : ['islower.o']
>>> num objects: 1
>>> object 0: name: 'input'
>>> object 0: size: 1
>>> object 0: data: '\x00'
>>>
>>> For all other programs, it's absolutely the same: the state set is
>>> always empty (except the initial state) and the data is always zero.
>>>
>>> I followed exactly the steps on the homepage[1] to build Klee with
>>> uclibc support. I'm currently at revision 103959 and created Release
>>> builds of LLVM and Klee. All unit tests pass but I see lots of fails in
>>> the check summary. (The whole output of make check is attached.)
>>>
>>> === Summary ===
>>>
>>> # of expected passes 62
>>> # of unexpected failures 43
>>> # of expected failures 2
>>>
>>> My previous versions of LLVM and Klee were several weeks old but worked
>>> fine.
>>>
>>> [1] http://klee.llvm.org/GetStarted.html
>>>
>>> Heinz
>>>
>>>
>>>
>>> _______________________________________________
>>> klee-dev mailing list
>>> klee-dev at keeda.stanford.edu
>>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at keeda.stanford.edu
>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>>
