Unexpected Output!

[General Email]

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

[Daniel Liew]

Hi,

You should check what happens if you use -emit-all-errors command line flags.

It's possible that an optimisation moved the klee_assume() call
outside of the if/else branch so that there is **only** one call to
the klee_assume() function in the LLVM bitcode. If that is the case
then KLEE will ignore any errors at the location if it is visited
again. The -emit-all-errors flag will cause KLEE to report all errors
even if KLEE has visited that Instruction in the LLVM bitcode before.

To see what LLVM Bitcode is interpreting take a look at
klee-last/assembly.ll file produced by KLEE.

There is probably more to this issue because I didn't expect KLEE to
generate a test case for paths with invalid constraints.

Thanks,
Dan

Post by General Email
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
}
}
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
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

[Cristian Cadar]

From what I can tell, there's nothing to prevent y+7 from overflowing
and become negative.

Cristian

Post by General Email
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
}
}
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
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[General Email]

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-/***@public.gmane.org> 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-/***@public.gmane.org> 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