[klee-dev] Unexpected Output!
General Email
general_mail2011 at yahoo.com
Mon Jan 27 14:41:56 GMT 2014
Thanks Dan,
I ran klee with the emit-all-errors option and I still got the same output (two tests: one feasible and one unfeasible) and as I understand, the output should show two unfeasible paths!
Here is the assembly.ll file generated.
; ModuleID = 'question.o'
target datalayout = "e-p:32:32:32-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:32:64-f32:32:32-f64:32:64-v64:64:64-v128:128:128-a0:0:64-f80:32:32-n8:16:32"
target triple = "i386-pc-linux-gnu"
@.str = private constant [2 x i8] c"y\00", align 1 ; <[2 x i8]*> [#uses=1]
define i32 @main() nounwind {
entry:
%retval = alloca i32 ; <i32*> [#uses=1]
%attr1 = alloca i32 ; <i32*> [#uses=4]
%attr2 = alloca i32 ; <i32*> [#uses=3]
%y = alloca i32 ; <i32*> [#uses=3]
%"alloca point" = bitcast i32 0 to i32 ; <i32> [#uses=0]
store i32 100, i32* %attr1, align 4, !dbg !0
store i32 12, i32* %attr2, align 4, !dbg !0
%0 = call i32 (...)* @klee_make_symbolic(i32* %y, i32 4, i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0)) nounwind, !dbg !7 ; <i32> [#uses=0]
%1 = load i32* %y, align 4, !dbg !8 ; <i32> [#uses=1]
%2 = icmp sgt i32 %1, 0, !dbg !8 ; <i1> [#uses=1]
br i1 %2, label %bb, label %bb1, !dbg !8
bb: ; preds = %entry
%3 = load i32* %y, align 4, !dbg !9 ; <i32> [#uses=1]
%4 = add nsw i32 %3, 7, !dbg !9 ; <i32> [#uses=1]
store i32 %4, i32* %attr1, align 4, !dbg !9
store i32 500, i32* %attr2, align 4, !dbg !10
%5 = load i32* %attr1, align 4, !dbg !11 ; <i32> [#uses=1]
%6 = icmp slt i32 %5, 0, !dbg !11 ; <i1> [#uses=1]
%7 = zext i1 %6 to i32, !dbg !11 ; <i32> [#uses=1]
%8 = call i32 (...)* @klee_assume(i32 %7) nounwind, !dbg !11 ; <i32> [#uses=0]
br label %return, !dbg !11
bb1: ; preds = %entry
store i32 800, i32* %attr2, align 4, !dbg !12
%9 = load i32* %attr1, align 4, !dbg !13 ; <i32> [#uses=1]
%10 = icmp slt i32 %9, 0, !dbg !13 ; <i1> [#uses=1]
%11 = zext i1 %10 to i32, !dbg !13 ; <i32> [#uses=1]
%12 = call i32 (...)* @klee_assume(i32 %11) nounwind, !dbg !13 ; <i32> [#uses=0]
br label %return, !dbg !13
return: ; preds = %bb, %bb1
%retval3 = load i32* %retval, !dbg !14 ; <i32> [#uses=1]
ret i32 %retval3, !dbg !14
}
declare void @llvm.dbg.declare(metadata, metadata) nounwind readnone
declare i32 @klee_make_symbolic(...)
declare i32 @klee_assume(...)
!0 = metadata !{i32 3, i32 0, metadata !1, null}
!1 = metadata !{i32 458763, metadata !2, i32 2, i32 0} ; [ DW_TAG_lexical_block ]
!2 = metadata !{i32 458798, i32 0, metadata !3, metadata !"main", metadata !"main", metadata !"main", metadata !3, i32 2, metadata !4, i1 false, i1 true, i32 0, i32 0, null, i1 false} ; [ DW_TAG_subprogram ]
!3 = metadata !{i32 458769, i32 0, i32 1, metadata !"question.c", metadata !"/home/pgbovine/klee/examples/myKleeTryouts/", metadata !"4.2.1 (Based on Apple Inc. build 5658) (LLVM build 2.7)", i1 true, i1 false, metadata !"", i32 0} ; [ DW_TAG_compile_uni
!4 = metadata !{i32 458773, metadata !3, metadata !"", metadata !3, i32 0, i64 0, i64 0, i64 0, i32 0, null, metadata !5, i32 0, null} ; [ DW_TAG_subroutine_type ]
!5 = metadata !{metadata !6}
!6 = metadata !{i32 458788, metadata !3, metadata !"int", metadata !3, i32 0, i64 32, i64 32, i64 0, i32 0, i32 5} ; [ DW_TAG_base_type ]
!7 = metadata !{i32 5, i32 0, metadata !1, null}
!8 = metadata !{i32 7, i32 0, metadata !1, null}
!9 = metadata !{i32 9, i32 0, metadata !1, null}
!10 = metadata !{i32 10, i32 0, metadata !1, null}
!11 = metadata !{i32 11, i32 0, metadata !1, null}
!12 = metadata !{i32 15, i32 0, metadata !1, null}
!13 = metadata !{i32 16, i32 0, metadata !1, null}
!14 = metadata !{i32 19, i32 0, metadata !1, null}
Thanks
On Friday, January 24, 2014 11:43 AM, General Email <general_mail2011 at yahoo.com> wrote:
Thanks Dan,
I moved the klee_assume statement to the end of the conditional statement and ran klee with the emit-all-errors option and I got the same output!
The code:
int main()
{
int attr1=100, attr2=12;
int y;
klee_make_symbolic(&y, sizeof(int), "y");
if(y>0)
{
attr1=y+7;
attr2=500;
printf("attr2 = %d\n", attr2);
}
else
{
attr2=800;
printf("attr2 = %d\n", attr2);
}
klee_assume(attr1<0);
}
The output:
attr2 = 800
KLEE: ERROR: invalid klee_assume call (provably false)
attr2 = 500
KLEE: done: total instructions = 33
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
Any advise?
On Friday, January 24, 2014 11:12 AM, General Email <general_mail2011 at yahoo.com> wrote:
Hi,
Can anybody correct me if my notice is wrong?
I have the following code which should generate two symbolic execution paths; none of them can by satisfiable. However Klee doesn't show this!!!
int main()
{
int attr1=100, attr2=12;
int y;
klee_make_symbolic(&y, sizeof(int), "y");
if(y>0)
{
attr1=y+7;
attr2=500;
printf("attr2 = %d\n", attr2);
klee_assume(attr1<0); //by all means this cannot be satisfied
}
else
{
attr2=800;
printf("attr2 = %d\n", attr2);
klee_assume(attr1<0); ////by all means this also cannot be satisfied
}
}
Here is the output from Klee:
attr2 = 800
KLEE: ERROR: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
attr2 = 500
//My question why it doesn't give an error saying "invalid klee_assume call (provably false)" here also?
KLEE: done: total instructions = 32
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
Here are the values of y generated in each test:
ktest file : 'klee-last/test000001.ktest' //This represents the else branch (i.e., y<=0)
object 0: name: 'y'
object 0: size: 4
object 0: data: 0
ktest file : 'klee-last/test000002.ktest' //This represents the then branch (i.e., y>0)
object 0: name: 'y'
object 0: size: 4
object 0: data: 2147483642
Note: using klee_assert in place of klee_assume will give assertion fail in the two branches.
attr2 = 800
KLEE: ERROR: ASSERTION FAIL: attr1<0
KLEE: NOTE: now ignoring this error at this location
attr2 = 500
KLEE: ERROR: ASSERTION FAIL: attr1<0
Please advise?
Thanks
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list