get_sign

README.md

+# Klee tutorial
+
+Installing and testing klee.
+
+## Dependencies
+
+Dependencies for building klee is discussed in [building klee](https://klee.github.io/build-llvm9/).
+
+Under the hood, klee uses a `sat` solver for First Order Logic (FOL). Klee can interface to [z3](https://en.wikipedia.org/wiki/Z3_Theorem_Prover) which is modern and efficient solver using Satisfiability Modulo Theories (SMT). In essence SMT is FOL + built in theories for reasoning on fixed-size bit-vectors, extensional arrays, datatypes, and uninterpreted functions, making it suitable for program analysis.
+
+So first install `z3` on your system (then klee will use that instead of the default solver).
+
+Under arch with `yay` installed simply:
+
+```shell
+> yay -S z3
+```
+
+
+## Install KLEE from source
+
+
+The instructions recommend LLVM 9, but the current master (2.2-pre) supports LLVM 11 (which is what you would have under arch as of 2020-12-07).
+
+Under arch you can simply
+
+```shell
+> git clone https://github.com/klee/klee.git
+> cd klee
+> mkdir build
+> cd build
+> cmake ..
+> make -j 8 (-j sets number of parallel builds, e.g., on a 8 threaded machine)
+> sudo make install
+```
+
+Verify that you have the tool installed.
+
+```shell
+> klee -version
+KLEE 2.2-pre (https://klee.github.io)
+  Build mode: RelWithDebInfo (Asserts: ON)
+  Build revision: 199bd43deffc614b2915f4de26475ca43d22e2ae
+
+LLVM (http://llvm.org/):
+  LLVM version 11.0.0
+  Optimized build.
+  Default target: x86_64-pc-linux-gnu
+  Host CPU: znver2
+```
+
+If your build fails at some point, consult the docs [building klee](https://klee.github.io/build-llvm9/).
+
+## Testing a small function
+
+See the `examples/get_sign` folder.

examples/get_sign.c

+/*
+ * First KLEE tutorial: testing a small function
+ * https://klee.github.io/tutorials/testing-function/
+ */
+
+#include <klee/klee.h>
+
+int get_sign(int x)
+{
+    if (x == 0)
+        return 0;
+
+    if (x < 0)
+        return -1;
+    else
+        return 1;
+}
+
+int main()
+{
+    int a;
+    klee_make_symbolic(&a, sizeof(a), "a");
+    return get_sign(a);
+}
+
+// A) Compiling into LLVM bitcode
+// > clang -emit-llvm -c get_sign.c
+//
+// [your answer here]
+//
+// B) Inspecting the output
+//
+// > ls klee-last/
+//
+// [your answer here]
+//
+// C) Inspecting the generated test cases
+//
+// > ktest-tool klee-last/test000001.ktest
+//
+// What path in the code does this test represent?
+//
+// [your answer here]
+//
+// > ktest-tool klee-last/test000002.ktest
+//
+// What path in the code does this test represent?
+//
+// [your answer here]
+// > ktest-tool klee-last/test000002.ktest
+//
+// What path in the code does this test represent?
+//
+// [your answer here]
+//
+// D) Replaying a test case
+//
+// Fist check that includes were installed:
+// > ls /usr/local/include
+// klee
+//
+// > ls /usr/local/lib
+// klee  libkleeRuntest.so  libkleeRuntest.so.1.0
+//
+// If those are ok, then you can compile for replay:
+//
+// > clang -I /usr/local/include/ -L /usr/local/lib get_sign.c -l kleeRuntest
+//
+// To replay the first test:
+// > KTEST_FILE=klee-last/test000001.ktest ./a.out
+// > echo $?
+//
+// $? is the return value (error code) as seen by the shell.
+//
+// Did the result correspond to the expected path for the test?
+//
+// [your answer here]
+//
+// > KTEST_FILE=klee-last/test000002.ktest ./a.out
+// > echo $?
+//
+// Did the result correspond to the expected path for the test?
+//
+// [your answer here]
+//
+// > KTEST_FILE=klee-last/test000003.ktest ./a.out
+// > echo $?
+//
+// Did the result correspond to the expected path for the test?
+//
+// [your answer here]
+//
+// Why not? Confir to shell error codes
+//
+// [your answer here]
+//
+// D) Debugging
+//
+// In the above example its kind of hard to see exactly
+// what happens. Using `gdb` you single step the program.
+//
+// First build it with debug symbols (`-g`).
+// > clang -g -I /usr/local/include/ -L /usr/local/lib get_sign.c -l kleeRuntest
+//
+// We need to add the libary path so it can be dynamically loaded:
+// Depending on shell this might look different:
+//
+// Under `bash` (and `bash` like shells)
+// > export LD_LIBRARY_PATH=/usr/local/lib:$LD_LIBRARY_PATH
+// Under `fish`
+// > set -x LD_LIBRARY_PATH /usr/local/lib/
+//
+// Then start `gdb`:
+// > KTEST_FILE=klee-last/test000001.ktest gdb ./a.out
+// (gdb) break get_sign
+//
+// (gdb) run
+//
+// Now we can inspect the `x` argument by:
+// (gdb) print x
+//
+// What value do you get, and why?
+//
+// [your answer here]
+//
+// Step the code
+// > (gdb) next
+//
+// What path did it take, and why?
+//
+// [your answer here]
+//
+// Now we can try with another test:
+//
+// (gdb) set environment KTEST_FILE=klee-last/test000002.ktest
+//
+// And (re-start) the debug session:
+// (gdb) run
+//
+// Step through the code.
+//
+// Which path did it take, and why?
+//
+// [your answer here]
+//
+// And finally:
+//
+// (gdb) set environment KTEST_FILE=klee-last/test000003.ktest
+//
+// Which path did it take, and why?
+//
+// [your answer here]
+//
+// E) Under the hood.
+//
+// Explain in your own words how
+// `klee_make_symbolic(&a, sizeof(a), "a");`
+// works when you run `klee` to generate test cases:
+//
+// [your answer here]
+// (hint, mark memory region as symbolic)
+//
+// Explain in your own words how
+// `klee_make_symbolic(&a, sizeof(a), "a");`
+// works when you replay test cases:
+//
+// [your answer here]
+// (hint, KTEST_FILE points to a concrete assignment
+// of the memory region)