Completed A-D

examples/get_sign.c

@@ -31,12 +31,20 @@ int main()
 // > klee get_sign.bc
 //
 // [your answer here]
+// KLEE: Using Z3 solver backend
+// 
+// KLEE: done: total instructions = 31
+// KLEE: done: completed paths = 3
+// KLEE: done: generated tests = 3
+// 
 //
 // B) Inspecting the output
 //
 // > ls klee-last/
 //
 // [your answer here]
+// assembly.ll  info  messages.txt  run.istats  run.stats
+// test000001.ktest  test000002.ktest  test000003.ktest  warnings.txt
 //
 // C) Inspecting the generated test cases
 //
@@ -45,17 +53,57 @@ int main()
 // What path in the code does this test represent?
 //
 // [your answer here]
+// ktest file : 'klee-last/test000001.ktest'
+// args       : ['get_sign.bc']
+// num objects: 1
+// object 0: name: 'a'
+// object 0: size: 4
+// object 0: data: b'\x00\x00\x00\x00'
+// object 0: hex : 0x00000000
+// object 0: int : 0
+// object 0: uint: 0
+// object 0: text: ....
+//
+// It represent the path where x = 0 and the return value is 0.
+// 
 //
 // > ktest-tool klee-last/test000002.ktest
 //
 // What path in the code does this test represent?
 //
 // [your answer here]
+// ktest file : 'klee-last/test000002.ktest'
+// args       : ['get_sign.bc']
+// num objects: 1
+// object 0: name: 'a'
+// object 0: size: 4
+// object 0: data: b'\x01\x01\x01\x01'
+// object 0: hex : 0x01010101
+// object 0: int : 16843009
+// object 0: uint: 16843009
+// object 0: text: ....
+//
+// It represent the path where x > 0 and the return value is 1.
+//
+//
 // > ktest-tool klee-last/test000003.ktest
 //
 // What path in the code does this test represent?
 //
 // [your answer here]
+// ktest file : 'klee-last/test000003.ktest'
+// args       : ['get_sign.bc']
+// num objects: 1
+// object 0: name: 'a'
+// object 0: size: 4
+// object 0: data: b'\x02\x01\x01\x80'
+// object 0: hex : 0x02010180
+// object 0: int : -2147417854
+// object 0: uint: 2147549442
+// object 0: text: ....
+//
+// It represent the path where x < 0 and the return value is -1.
+//
 //
 // D) Replaying a test case
 //
@@ -109,6 +157,8 @@ int main()
 // Did the result correspond to the expected path for the test?
 //
 // [your answer here]
+// yes
+// echo $?  gives  0
 //
 // > KTEST_FILE=klee-last/test000002.ktest ./a.out
 //
@@ -117,6 +167,8 @@ int main()
 // Did the result correspond to the expected path for the test?
 //
 // [your answer here]
+// Yes
+// echo $?  gives  1
 //
 // > KTEST_FILE=klee-last/test000003.ktest ./a.out
 //
@@ -125,10 +177,13 @@ int main()
 // Did the result correspond to the expected path for the test?
 //
 // [your answer here]
+// Yes
+// echo $?  gives 255 (which is equal to -1 of 8 signed bits)
 //
 // Why not? Confer to shell error codes:
 //
 // [your answer here]
+// ??? TODO
 //
 // D) Debugging
 //
@@ -153,6 +208,9 @@ int main()
 // What value do you get, and why?
 //
 // [your answer here]
+// (gdb) print x
+// $1 = 0
+// It has the value 0 and it got that because the constraint x == o is the fist split in the paths. 
 //
 // Step the code
 // > (gdb) next
@@ -160,6 +218,12 @@ int main()
 // What path did it take, and why?
 //
 // [your answer here]
+// Breakpoint 1, get_sign (x=0) at get_sign.c:10
+// 10	    if (x == 0)
+// (gdb) next
+// 11	        return 0;
+// It took the path where it returns 0.
+// It took that path because x = 0 thus x == 0.
 //
 // Now we can try with another test:
 //
@@ -173,6 +237,15 @@ int main()
 // Which path did it take, and why?
 //
 // [your answer here]
+// Breakpoint 1, get_sign (x=16843009) at get_sign.c:10
+// 10	    if (x == 0)
+// (gdb) next
+// 13	    if (x < 0)
+// (gdb) next
+// 16	        return 1;
+// It took the path where it returns 1.
+// It took that path because x = 16843009 thus x != 0 and x !< 0.
+//
 //
 // And finally:
 //
@@ -181,6 +254,14 @@ int main()
 // Which path did it take, and why?
 //
 // [your answer here]
+// Breakpoint 1, get_sign (x=-2147417854) at get_sign.c:10
+// 10	    if (x == 0)
+// (gdb) next
+// 13	    if (x < 0)
+// (gdb) next
+// 14	        return -1;
+// It took the path where it returns -1.
+// It took that path because x = -2147417854 thus x != 0 and x < 0.
 //
 // E) Under the hood.
 //

examples/klee-last

+/home/niklas/Desktop/D7020E/klee_tutorial/examples/klee-out-0
\ No newline at end of file

examples/klee-out-0/assembly.ll

+; ModuleID = 'get_sign.bc'
+source_filename = "get_sign.c"
+target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-pc-linux-gnu"
+
+@.str = private unnamed_addr constant [2 x i8] c"a\00", align 1
+
+; Function Attrs: noinline nounwind optnone uwtable
+define dso_local i32 @get_sign(i32) #0 {
+  %2 = alloca i32, align 4
+  %3 = alloca i32, align 4
+  store i32 %0, i32* %3, align 4
+  %4 = load i32, i32* %3, align 4
+  %5 = icmp eq i32 %4, 0
+  br i1 %5, label %6, label %7
+
+6:                                                ; preds = %1
+  store i32 0, i32* %2, align 4
+  br label %12
+
+7:                                                ; preds = %1
+  %8 = load i32, i32* %3, align 4
+  %9 = icmp slt i32 %8, 0
+  br i1 %9, label %10, label %11
+
+10:                                               ; preds = %7
+  store i32 -1, i32* %2, align 4
+  br label %12
+
+11:                                               ; preds = %7
+  store i32 1, i32* %2, align 4
+  br label %12
+
+12:                                               ; preds = %11, %10, %6
+  %13 = load i32, i32* %2, align 4
+  ret i32 %13
+}
+
+; Function Attrs: noinline nounwind optnone uwtable
+define dso_local i32 @main() #0 {
+  %1 = alloca i32, align 4
+  %2 = alloca i32, align 4
+  store i32 0, i32* %1, align 4
+  %3 = bitcast i32* %2 to i8*
+  call void @klee_make_symbolic(i8* %3, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i64 0, i64 0))
+  %4 = load i32, i32* %2, align 4
+  %5 = call i32 @get_sign(i32 %4)
+  ret i32 %5
+}
+
+declare dso_local void @klee_make_symbolic(i8*, i64, i8*) #1
+
+attributes #0 = { noinline nounwind optnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
+attributes #1 = { "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
+
+!llvm.module.flags = !{!0}
+!llvm.ident = !{!1}
+
+!0 = !{i32 1, !"wchar_size", i32 4}
+!1 = !{!"clang version 9.0.0-2 (tags/RELEASE_900/final)"}

examples/klee-out-0/info

+klee get_sign.bc
+PID: 31615
+Using monotonic steady clock with 1/1000000000s resolution
+Started: 2020-12-07 17:08:04
+BEGIN searcher description
+<InterleavedSearcher> containing 2 searchers:
+RandomPathSearcher
+WeightedRandomSearcher::CoveringNew
+</InterleavedSearcher>
+END searcher description
+Finished: 2020-12-07 17:08:04
+Elapsed: 00:00:00
+KLEE: done: explored paths = 3
+KLEE: done: avg. constructs per query = 11
+KLEE: done: total queries = 3
+KLEE: done: valid queries = 0
+KLEE: done: invalid queries = 3
+KLEE: done: query cex = 3
+
+KLEE: done: total instructions = 31
+KLEE: done: completed paths = 3
+KLEE: done: generated tests = 3

examples/klee-out-0/messages.txt

+KLEE: Using Z3 solver backend

examples/klee-out-0/run.istats

+version: 1
+creator: klee
+pid: 31615
+cmd: get_sign.bc
+
+
+positions: instr line
+event: Icov : CoveredInstructions
+event: Forks : Forks
+event: Ireal : InstructionRealTimes
+event: Itime : InstructionTimes
+event: I : Instructions
+event: UCdist : MinDistToUncovered
+event: Rtime : ResolveTime
+event: States : States
+event: Iuncov : UncoveredInstructions
+event: Q : Queries
+event: Qiv : QueriesInvalid
+event: Qv : QueriesValid
+event: Qtime : QueryTime
+events: Icov Forks Ireal Itime I UCdist Rtime States Iuncov Q Qiv Qv Qtime 
+ob=assembly.ll
+fn=get_sign
+10 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+11 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+12 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+13 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+14 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+15 0 1 1 0 0 1 0 0 0 0 2 2 0 40035 
+18 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+19 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+22 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+23 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+24 0 1 1 0 0 1 0 0 0 0 1 1 0 18179 
+27 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+28 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+31 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+32 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+35 0 1 0 0 0 3 0 0 0 0 0 0 0 0 
+36 0 1 0 0 0 3 0 0 0 0 0 0 0 0 
+fn=main
+41 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+42 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+43 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+44 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+45 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+46 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+47 0 1 0 0 0 1 0 0 0 0 0 0 0 0 
+cfn=get_sign
+calls=1 8 0
+47 0 17 2 0 0 21 0 0 0 0 3 3 0 58214 
+48 0 1 0 0 0 3 0 0 0 0 0 0 0 0