Thanks Stefan but your code doesn't work either.
$ klee test.o
KLEE: output directory = "klee-out-0"
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
WARNING: Linking two modules of different data layouts!
WARNING: Linking two modules of different target triples!
KLEE: done: total instructions = 27
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
The metadata is debug related. In the last days I built several LLVM
versions with different flags. The <badref>s might be an issue from
there. However, if we compare the LLVM code compiled without the '-g'
flag set, the sources should look similar (except that you use a 64bit
machine and mine is 32bit). (I've attached my version without metadata.)
What about the STP queries?
# Query 0 -- Type: InitialValues, Instructions: 13
(query [] false)
# OK -- Elapsed: 0.000226092
# Solvable: true
Is a "false" query really solvable?
# 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
Shouldn't this query (c > 10) be solvable?
I don't understand where the problem comes from. I had klee already
running on my system and it worked fine. The only serious change in my
system (that I'm aware of) is a distribution related update to GCC 4.5.0.
Heinz
On 05/20/2010 09:33 PM, Stefan Bucur wrote:
> Your code seems to have some problems, although I don't know how they
> affect the Klee operation. I compiled your code with my LLVM 2.6
> installation, and it resulted:
>
> define i32 @main(i32 %argc, i8** %argv) nounwind {
> entry:
> %argc_addr = alloca i32 ;<i32*> [#uses=2]
> %argv_addr = alloca i8** ;<i8***> [#uses=2]
> %retval = alloca i32 ;<i32*> [#uses=2]
> %c = alloca i32 ;<i32*> [#uses=3]
> %0 = alloca i32 ;<i32*> [#uses=3]
> %"alloca point" = bitcast i32 0 to i32 ;<i32> [#uses=0]
> call void @llvm.dbg.func.start({ }* bitcast
> (%llvm.dbg.subprogram.type* @llvm.dbg.subprogram to { }*))
> %1 = bitcast i32* %argc_addr to { }* ;<{ }*> [#uses=1]
> call void @llvm.dbg.declare({ }* %1, { }* bitcast
> (%llvm.dbg.variable.type* @llvm.dbg.variable to { }*))
> store i32 %argc, i32* %argc_addr
> %2 = bitcast i8*** %argv_addr to { }* ;<{ }*> [#uses=1]
> call void @llvm.dbg.declare({ }* %2, { }* bitcast
> (%llvm.dbg.variable.type* @llvm.dbg.variable10 to { }*))
> store i8** %argv, i8*** %argv_addr
> %3 = bitcast i32* %c to { }* ;<{ }*> [#uses=1]
> call void @llvm.dbg.declare({ }* %3, { }* bitcast
> (%llvm.dbg.variable.type* @llvm.dbg.variable12 to { }*))
> call void @llvm.dbg.stoppoint(i32 4, i32 0, { }* bitcast
> (%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
> %c1 = bitcast i32* %c to i8* ;<i8*> [#uses=1]
> call void @klee_make_symbolic(i8* %c1, i64 4, i8* getelementptr
> inbounds ([2 x i8]* @.str13, i64 0, i64 0)) nounwind
> call void @llvm.dbg.stoppoint(i32 5, i32 0, { }* bitcast
> (%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
> %4 = load i32* %c, align 4 ;<i32> [#uses=1]
> %5 = icmp sgt i32 %4, 10 ;<i1> [#uses=1]
> br i1 %5, label %bb, label %bb2
> ; No predecessors!
> call void @llvm.dbg.stoppoint(i32 5, i32 0, { }* bitcast
> (%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
> br label %bb
>
> bb: ; preds = %6, %entry
> call void @llvm.dbg.stoppoint(i32 6, i32 0, { }* bitcast
> (%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
> store i32 1, i32* %0, align 4
> br label %bb3
> ; No predecessors!
> call void @llvm.dbg.stoppoint(i32 6, i32 0, { }* bitcast
> (%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
> br label %bb2
>
> bb2: ; preds = %7, %entry
> call void @llvm.dbg.stoppoint(i32 7, i32 0, { }* bitcast
> (%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
> store i32 0, i32* %0, align 4
> br label %bb3
>
> bb3: ; preds = %bb2, %bb
> call void @llvm.dbg.stoppoint(i32 7, i32 0, { }* bitcast
> (%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
> %8 = load i32* %0, align 4 ;<i32> [#uses=1]
> store i32 %8, i32* %retval, align 4
> br label %return
>
> return: ; preds = %bb3
> %retval4 = load i32* %retval ;<i32> [#uses=1]
> call void @llvm.dbg.stoppoint(i32 7, i32 0, { }* bitcast
> (%llvm.dbg.compile_unit.type* @llvm.dbg.compile_unit to { }*))
> call void @llvm.dbg.region.end({ }* bitcast
> (%llvm.dbg.subprogram.type* @llvm.dbg.subprogram to { }*))
> ret i32 %retval4
> }
>
> You can see that the llvm.dbg.* calls do not have the "metadata
> <badref>", but some valid parameters instead.
>
> In any case, I attached in this message the test.o file that works for
> me (it generates 2 paths with Klee). You should try it out and see if
> it works with your Klee setup, as well. If it does, then there is a
> problem with the way you set up LLVM on your machine.
>
> Stefan
>
> On Thu, May 20, 2010 at 9:17 PM, Heinz Riener<hriener at student.tugraz.at>
> wrote:
>> 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
>>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.o
Type: application/x-object
Size: 712 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100520/7c281ab3/attachment-0001.bin
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: test.o.ll
Url:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100520/7c281ab3/attachment-0001.cc
