Convert the README to Markdown

Author: Sebastian Poeplau

README renamed to README.md

@@ -1,7 +1,4 @@
-
-
-               SymCC: efficient compiler-based symbolic execution
-
+# SymCC: efficient compiler-based symbolic execution
 
 SymCC is a compiler wrapper which embeds symbolic execution into the program
 during compilation, and an associated run-time support library. In essence, the
@@ -12,32 +9,37 @@ run time.
 To build the pass and the support library, make sure that LLVM 8, 9 or 10 and Z3
 version 4.5 or later, as well as a C++ compiler with support for C++17 are
 installed. (Alternatively, see below for using the provided Dockerfile.) Make
-sure to pull the Qsym code:
+sure to pull the QSYM code:
 
+```
 $ git submodule init
 $ git submodule update
+```
 
-Note that it is not necessary or recommended to build the Qsym submodule - our
+Note that it is not necessary or recommended to build the QSYM submodule - our
 build system will automatically extract the right source files and include them
 in the build.
 
 Create a build directory somewhere, and execute the following commands inside
 it:
 
+```
 $ cmake -G Ninja -DQSYM_BACKEND=ON /path/to/compiler/sources
 $ ninja check
+```
 
 If LLVM is installed in a non-standard location, add the CMake parameter
-"-DLLVM_DIR=/path/to/llvm/cmake/module". Similarly, you can point to a
-non-standard Z3 installation with "-DZ3_DIR=/path/to/z3/cmake/module" (which
+`-DLLVM_DIR=/path/to/llvm/cmake/module`. Similarly, you can point to a
+non-standard Z3 installation with `-DZ3_DIR=/path/to/z3/cmake/module` (which
 requires Z3 to be built with CMake).
 
-The main build artifact from the user's point of view is symcc, a wrapper script
-around clang that sets the right options to load our pass and link against the
-run-time library. (See below for additional C++ support.)
+The main build artifact from the user's point of view is `symcc`, a wrapper
+script around clang that sets the right options to load our pass and link
+against the run-time library. (See below for additional C++ support.)
 
 To try the compiler, take some simple C code like the following:
 
+``` c
 #include <stdio.h>
 #include <stdint.h>
 #include <unistd.h>
@@ -60,21 +62,28 @@ int main(int argc, char* argv[]) {
     printf("%d\n", foo(x, 7));
     return 0;
 }
+```
 
-Save the code as "test.c". To compile it with symbolic execution built in, we
+Save the code as `test.c`. To compile it with symbolic execution built in, we
 call symcc as we would normally call clang:
 
+```
 $ ./symcc test.c -o test
+```
 
 Before starting the analysis, create a directory for the results and tell SymCC
 about it:
 
+```
 $ mkdir results
 $ export SYMCC_OUTPUT_DIR=`pwd`/results
+```
 
 Then run the program like any other binary, providing arbitrary input:
 
+```
 $ echo 'aaaa' | ./test
+```
 
 The program will execute the same computations as an uninstrumented version
 would, but additionally the injected code will track computations symbolically
@@ -83,71 +92,77 @@ program reads from standard input is treated as symbolic; alternatively, you can
 set the environment variable SYMCC_INPUT_FILE to the name of a file whose
 contents will be treated as symbolic when read.
 
-Note that due how the Qsym backend is implemented, all input has to be available
+Note that due how the QSYM backend is implemented, all input has to be available
 from the start. In particular, when providing symbolic data on standard input
 interactively, you need to terminate your input by pressing Ctrl+D before the
 program starts to execute.
 
 When execution is finished, the result directory will contain the new test cases
 generated during program execution. Try running the program again on one of
-those or combine it with a fuzzer to automate this process (see below).
+those or combine it with a fuzzer to automate this process (see
+docs/Fuzzing.txt).
 
 
-                                 Documentation
+## Documentation
 
-The directory "docs" contains documentation on several internal aspects of
+The directory [docs](docs) contains documentation on several internal aspects of
 SymCC, as well as building C++ code, compiling 32-bit binaries on a 64-bit host,
 and running SymCC with a fuzzer.
 
 
-                            Building a Docker image
+## Building a Docker image
 
 If you prefer a Docker container over building SymCC natively, just tell Docker
-to build the image after pulling the Qsym code as above. (Be warned though: the
+to build the image after pulling the QSYM code as above. (Be warned though: the
 Docker image enables optional C++ support and builds Z3 from source, so creating
 the image can take quite some time!)
 
+```
 $ git submodule init
 $ git submodule update
 $ docker build -t symcc .
 $ docker run -it --rm symcc
+```
 
 This will build a Docker image and run an ephemeral container to try out SymCC.
-Inside the container, "symcc" is available as a drop-in replacement for "clang",
-using the Qsym backend; similarly, "sym++" can be used instead of "clang++". Now
+Inside the container, `symcc` is available as a drop-in replacement for `clang`,
+using the QSYM backend; similarly, `sym++` can be used instead of `clang++`. Now
 try something like the following inside the container:
 
+```
 container$ cat sample.cpp
 (Note that "root" is the input we're looking for.)
 container$ sym++ -o sample sample.cpp
 container$ echo test | ./sample
 ...
 container$ cat /tmp/output/000008-optimistic
 root
+```
 
-The Docker image also has AFL and "symcc_fuzzing_helper" preinstalled, so you
-can use it to run SymCC with a fuzzer as described in "docs/Fuzzing.txt". (The
-AFL binaries are located in "/afl".)
+The Docker image also has AFL and `symcc_fuzzing_helper` preinstalled, so you
+can use it to run SymCC with a fuzzer as described in [the
+docs](docs/Fuzzing.txt). (The AFL binaries are located in `/afl`.)
 
 While the Docker image is very convenient for _using_ SymCC, I recommend a local
 build outside Docker for _development_. Docker will rebuild most of the image on
 every change to SymCC (which is, in principle the right thing to do), whereas in
-many cases it is sufficient to let Ninja figure out what to rebuild (and
-recompile libc++ only when necessary).
+many cases it is sufficient to let the build system figure out what to rebuild
+(and recompile, e.g., libc++ only when necessary).
 
 
-                                    Contact
+## Contact
 
 Feel free to use GitHub issues and pull requests for improvements, bug reports,
 etc. Alternatively, you can send an email to Sebastian Poeplau
 ([email protected]) and Aurélien Francillon
 ([email protected]).
 
 
-                                   Reference
+## Reference
 
 To cite SymCC in scientific work, please use the following BibTeX:
 
+``` bibtex
 @inproceedings {poeplau2020symcc,
   author =       {Sebastian Poeplau and Aurélien Francillon},
   title =        {Symbolic execution with {SymCC}: Don't execute, compile!},
@@ -158,9 +173,10 @@ To cite SymCC in scientific work, please use the following BibTeX:
   publisher =    {{USENIX} Association},
   month =        August,
 }
+```
 
 
-                                    License
+## License
 
 SymCC is free software: you can redistribute it and/or modify it under the terms
 of the GNU General Public License as published by the Free Software Foundation,
@@ -176,6 +192,7 @@ SymCC. If not, see <https://www.gnu.org/licenses/>.
 The following pieces of software have additional or alternate copyrights,
 licenses, and/or restrictions:
 
-Program             Directory
--------             ---------
-QSYM                runtime/qsym_backend/qsym
+| Program | Directory                   |
+| ---     | ---                         |
+| QSYM    | `runtime/qsym_backend/qsym` |
+