PRE-REQS
--------
Ubuntu 14.04+ (e.g. in a VM)


Install KLEE Docker Image
-------------------------
1) Install Docker
	$ sudo apt-get remove docker docker-engine docker.io
	$ sudo apt-get update
	$ sudo apt-get install apt-transport-https ca-certificates curl software-properties-common
	$ curl -fsSL https://download.docker.com/linux/ubuntu/gpg | sudo apt-key add -
	(optional) $ sudo apt-key fingerprint 0EBFCD88
	$ sudo add-apt-repository \
		"deb [arch=amd64] https://download.docker.com/linux/ubuntu \
		$(lsb_release -cs) \
		stable"
	$ sudo apt-get update
	$ sudo apt-get install docker-ce
2) Get the KLEE Docker image
	$ sudo docker pull klee/klee
3) Create and enter a KLEE Docker container
	$ sudo docker run -ti --name=my_first_klee_container --ulimit='stack=-1:-1' klee/klee
4) You are now klee@<docker container id>
	Do "stuff"
	$ pwd
	$ echo "int main(int argn, char** argv) { return 0; }" > test.c
	$ clang -emit-llvm -g -c test.c -o test.bc
	$ klee --libc=uclibc --posix-runtime test.bc
	$ ls
	$ exit
5) You are now back to being yourself
6) Restart the container
	$ sudo docker start -ai my_first_klee_container
7) Do "stuff" and then exit the container
8) When you want to delete the container
	$ sudo docker rm my_first_klee_container


First Tutorial
--------------
0) KLEE tutorials: https://klee.github.io/tutorials/
1) Open "First tutorial: Testing a small function" (https://klee.github.io/tutorials/testing-function/)
2) Create and enter a KLEE Docker container, e.g.
	$ sudo docker run -ti --name=klee_tutorials --ulimit='stack=-1:-1' klee/klee
3) (optional) If you don't like Vim, install nano
    $ sudo apt update
    $ sudo apt upgrade
	$ sudo apt install nano spell
	[sudo] password for klee: klee
4) Choices...
	A) $ cd klee_src/examples/get_sign/get_sign.c
	B) $ cp klee_src/examples/get_sign/get_sign.c . 
	C) $ nano get_sign.c
5) Either way, be in the same directory as get_sign.c now and READ THE CODE
	$ cat get_sign.c
6) Think: What test cases would you write to check get_sign's correctness?
	Hint: you should have 3
	$ clang -I ~/klee_src/include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c
8) Run KLEE
	$ klee get_sign.bc
9) Examine the test cases generated by KLEE
	$ ktest-tool klee-last/test000001.ktest
	$ ktest-tool klee-last/test000002.ktest
	$ ktest-tool klee-last/test000003.ktest
10) Think: What is the expected output for each test case?
11) Replay the test cases
	$ export LD_LIBRARY_PATH=~/klee_build/lib/:$LD_LIBRARY_PATH
	$ clang -I ~/klee_src/include -L ~/klee_build/lib/ get_sign.c -lkleeRuntest
	$ KTEST_FILE=klee-last/test000001.ktest ./a.out
	$ echo $?
	$ KTEST_FILE=klee-last/test000002.ktest ./a.out
	$ echo $?
	$ KTEST_FILE=klee-last/test000003.ktest ./a.out
	$ echo $?
12) Think: Are the outputs (return values) as expected?
13) Exit container, or don't, up to you
	$ exit


Second Tutorial
---------------
1) Open "Second tutorial: Testing a simple regular expression library" (https://klee.github.io/tutorials/testing-regex/)
2) Create a new container or use the same one from the first tutorial.  I'll use the same one.
	$ sudo docker start -ai klee_tutorials
3) Choices...
	A) $ cd klee_src/examples/regexp/Regexp.c
	B) $ cp klee_src/examples/regexp/Regexp.c . 
	C) $ nano Regexp.c
4) Either way, be in the same directory as Regexp.c now and read the code
	$ cat Regexp.c
5) Think: What test cases would you write to check Regexp's correctness?
	Estimate: how many do you expect there should be?
6) Compile get_sign.c to LLVM bitcode
	$ clang -I ~/klee_src/include/ -emit-llvm -c -g Regexp.c
7) Execute the code with KLEE
	$ klee --only-output-states-covering-new -max-time=60 Regexp.bc
8) Examine the test cases and additional information generated by KLEE
	$ for file in klee-last/*.ktest; do ktest-tool $file; echo; done
	$ cat klee-last/test000008.ptr.err # your test case number may be different
	$ cat klee-last/test000009.ptr.err # your test case number may be different
9) Think: trace the execution of one of the error test cases (8 and 9, for me)
	Do you see the out-of-bounds memory reference?
10) Fix the test harness to make re null-terminated: re[SIZE - 1] = '\0'
	$ cp Regexp.c Regexp2.c
	$ nano Regexp2.c
11) Re-run KLEE
	$ clang -I ~/klee_src/include/ -emit-llvm -c -g Regexp2.c
	$ klee --only-output-states-covering-new -max-time=60 Regexp2.bc
12) Fix the test harness to use klee_assume: klee_assume(re[SIZE - 1] == '\0');
	$ cp Regexp.c Regexp3.c
	$ nano Regexp3.c
13) Re-run KLEE
	$ clang -I ~/klee_src/include/ -emit-llvm -c -g Regexp3.c
	$ klee --only-output-states-covering-new -max-time=60 Regexp3.bc
14) Exit container, or don't, up to you
	$ exit


Third Tutorial
--------------
1) Open "Solving a maze with KLEE" (https://feliam.wordpress.com/2010/10/07/the-symbolic-maze/)
2) Create a new container or use the same one from the first tutorial.  I'll use the same one.
	$ sudo docker start -ai klee_tutorials
3) Choices...
	$ cd ~
	$ mkdir maze
	$ cd maze
	A) $ wget https://pastebin.com/raw/6wG5stht -O maze.c
	B) $ nano maze.c
4) Either way, be in ~/maze now and read the code
	$ nano maze.c # syntax highlighting makes it easier
	If you downloaded it, #include <unistd.h> and fix the spelling errors
5) Play the game yourself
	$ clang maze.c -o maze
	$ ./maze
	You have to specify the instructions all at once, then hit return to go
6) Add KLEE annotation to mark the input "program" as symbolic
	Change line 72:
		- read(0,program,ITERS);
		+ klee_make_symbolic(program,ITERS,"program");
	Add KLEE header: #include<klee/klee.h>
7) Compile code to LLVM bitcode
	$ clang -I ~/klee_src/include/ -emit-llvm -c -g maze.c
8) Run KLEE
	$ klee --only-output-states-covering-new maze.bc
9) Check out the test cases
	$ for file in klee-last/*.ktest; do ktest-tool $file; echo; done
10) Make it easier to find the interesting test cases
	Insert klee_assert(0); under printf ("You win!\n");
		This was on line 106 for me.
	Add #include<assert.h>
11) Recompile and run KLEE
	$ clang -I ~/klee_src/include/ -emit-llvm -c -g maze.c
	$ klee --only-output-states-covering-new maze.bc
12) Which test case is also an error?
	$ ls -1 klee-last | grep err
13) Examine that test case
	$ TEST="klee-last/$(ls -1 klee-last | grep err | cut -d . -f 1).ktest"
	$ ktest-tool $TEST
	Note the length of the solution.  Seems a bit short, right?
14) Run that test case
	(if you haven't done this yet) $ export LD_LIBRARY_PATH=~/klee_build/lib/:$LD_LIBRARY_PATH
	$ clang -I ~/klee_src/include -L ~/klee_build/lib/ maze.c -o maze -lkleeRuntest
	$ KTEST_FILE=$TEST ./maze
	That's SNEAKY!!!
15) Find all possible solutions
	$ klee --only-output-states-covering-new --emit-all-errors maze.bc
	$ for file in $(ls -1 klee-last | grep err | cut -d . -f 1); do ktest-tool klee-last/$file.ktest; echo; done
16) Think: which line in the code makes the "cheat" possible?