diff --git a/examples/a.out b/examples/a.out index 81e51b36cd97f40e411fa57ab58a740248bba2d7..d17f0345c7afb7865dc5550d6d6c6a1db5cd5fa0 100755 Binary files a/examples/a.out and b/examples/a.out differ diff --git a/examples/get_sign.bc b/examples/get_sign.bc index 9b6d64807d3f7ca6e46b8102c0a0b438e2bc07a6..6b58850ce5098dcc54947def8b066de78515a9fe 100644 Binary files a/examples/get_sign.bc and b/examples/get_sign.bc differ diff --git a/examples/get_sign.c b/examples/get_sign.c index a10b519e23e4a2c7607b196cdb941fad8d159960..d536444459366ce4133f3bdd7dfc535f0de82796 100644 --- a/examples/get_sign.c +++ b/examples/get_sign.c @@ -177,13 +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) +// No +// echo $? gives 255 // // Why not? Confer to shell error codes: // // [your answer here] -// ??? TODO +// In bash exit code 255 means "Exit status out of range" and it says "exit takes only integer args in the range 0 - 255". The result should have been -1 but it is out of range for bash, so that is why I didn't get the expected result. // // D) Debugging // diff --git a/examples/klee-last b/examples/klee-last index c01e6451b12d8641916ad2be4999212cfbc63164..fd456c4124a0757962daf61e81e5803b001b06b3 120000 --- a/examples/klee-last +++ b/examples/klee-last @@ -1 +1 @@ -/home/niklas/Desktop/D7020E/klee_tutorial/examples/klee-out-0 \ No newline at end of file +/home/niklas/Desktop/D7020E/klee_tutorial/examples/klee-out-1 \ No newline at end of file diff --git a/examples/klee-out-1/assembly.ll b/examples/klee-out-1/assembly.ll new file mode 100644 index 0000000000000000000000000000000000000000..a9095db605ff4849d1b6eb0febc171c7c98c42f0 --- /dev/null +++ b/examples/klee-out-1/assembly.ll @@ -0,0 +1,60 @@ +; ModuleID = 'get_sign.bc' +source_filename = "get_sign.c" +target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-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) #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" "frame-pointer"="all" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "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" "frame-pointer"="all" "less-precise-fpmad"="false" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="true" "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 = !{!"Ubuntu clang version 11.0.0-2"} diff --git a/examples/klee-out-1/info b/examples/klee-out-1/info new file mode 100644 index 0000000000000000000000000000000000000000..1f816e9983e9c47330ac1e581bf52a55ce118e23 --- /dev/null +++ b/examples/klee-out-1/info @@ -0,0 +1,22 @@ +klee get_sign.bc +PID: 232064 +Using monotonic steady clock with 1/1000000000s resolution +Started: 2020-12-15 16:48:54 +BEGIN searcher description +<InterleavedSearcher> containing 2 searchers: +RandomPathSearcher +WeightedRandomSearcher::CoveringNew +</InterleavedSearcher> +END searcher description +Finished: 2020-12-15 16:48:54 +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 diff --git a/examples/klee-out-1/messages.txt b/examples/klee-out-1/messages.txt new file mode 100644 index 0000000000000000000000000000000000000000..d49ad73298ce077c15ada9b7d55fa15a59692adf --- /dev/null +++ b/examples/klee-out-1/messages.txt @@ -0,0 +1 @@ +KLEE: Using Z3 solver backend diff --git a/examples/klee-out-1/run.istats b/examples/klee-out-1/run.istats new file mode 100644 index 0000000000000000000000000000000000000000..963132326101b0ae1b71342ef1ec1ab6c72c90e1 --- /dev/null +++ b/examples/klee-out-1/run.istats @@ -0,0 +1,52 @@ +version: 1 +creator: klee +pid: 232064 +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 32370 +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 13814 +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 46184 +48 0 1 0 0 0 3 0 0 0 0 0 0 0 0 diff --git a/examples/klee-out-1/run.stats b/examples/klee-out-1/run.stats new file mode 100644 index 0000000000000000000000000000000000000000..160d68a57724c30a1c336cc780df730dca12c7bf Binary files /dev/null and b/examples/klee-out-1/run.stats differ diff --git a/examples/klee-out-1/test000001.ktest b/examples/klee-out-1/test000001.ktest new file mode 100644 index 0000000000000000000000000000000000000000..25f74a85d90a98ba12009cab156dd058ea9079b6 Binary files /dev/null and b/examples/klee-out-1/test000001.ktest differ diff --git a/examples/klee-out-1/test000002.ktest b/examples/klee-out-1/test000002.ktest new file mode 100644 index 0000000000000000000000000000000000000000..052994a96ef7578d3e66bc8ba1bd04b3fb521309 Binary files /dev/null and b/examples/klee-out-1/test000002.ktest differ diff --git a/examples/klee-out-1/test000003.ktest b/examples/klee-out-1/test000003.ktest new file mode 100644 index 0000000000000000000000000000000000000000..181f91f22038d0ca19e866aad982d22d6ba68a44 Binary files /dev/null and b/examples/klee-out-1/test000003.ktest differ diff --git a/examples/klee-out-1/warnings.txt b/examples/klee-out-1/warnings.txt new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391