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
>
