message: add more info to Readme
diff: Alive2
  ======
  -WIP; do not use!
  +Alive2 consists of several libraries and tools for analysis and verification
  +of LLVM code and transformations.
  +Alive2 includes the following libraries:
  +* Alive2 IR
  +* Symbolic executor
  +* LLVM -> Alive2 IR converter
  +* Refinement check (aka optimization verifier)
  +* SMT abstraction layer
  +
  +Included tools:
  +* Alive drop-in replacement
  +* Translation validation plugin for LLVM's `opt`
  +
  Prerequisites
  -------------
  -
  -* Z3 4.8.3
  +To build Alive2 you need recent versions of:
  +* cmake
  +* gcc/clang
  * re2c
  +* Z3
  +* LLVM (optional)
  +
  Building
  --------
  @@ -15,38 +31,38 @@ Building
  ```
  mkdir build
  cd build
  -cmake ..
  -make
  +cmake -GNinja -DCMAKE_BUILD_TYPE=Release ..
  +ninja
  ```
  If CMake cannot find the Z3 include directory (or finds the wrong one) pass
  the ``-DZ3_INCLUDE_DIR=/path/to/z3/include`` argument to CMake
  +
  Building and Running Translation Validation
  --------
  -Build an LLVM after configuring it using the ``-DLLVM_ENABLE_RTTI=ON
  --DLLVM_ENABLE_EH=ON`` options to CMake
  -
  -Copy ``alive2/scripts/opt-alive.sh`` somewhere and edit it to point to
  -the proper locations, keeping in mind that lit strips environment
  -variables other than $HOME
  -
  +Alive2's `opt` translation validation requires a build of LLVM with RTTI and
  +exceptions turned on.
  +LLVM can be built in the following way:
  ```
  +cd llvm
  mkdir build
  -cd build
  -cmake .. -GNinja -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=Release
  -ninja
  +cmake -GNinja -DLLVM_ENABLE_RTTI=ON -DLLVM_ENABLE_EH=ON -DCMAKE_BUILD_TYPE=Release -DLLVM_TARGETS_TO_BUILD=X86 -DLLVM_ENABLE_ASSERTIONS=ON -DLLVM_ENABLE_PROJECTS="llvm;clang" ../llvm
  +```
  +
  +Alive2 should then be configured as follows:
  +```
  +cmake -GNinja -DLLVM_DIR=~/llvm/build/lib/cmake/llvm -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=Release ..
  ```
  -Translation validation of a single test case:
  +Translation validation of a single test case:
  ```
  -${TEST_LLVM_BUILD}/bin/llvm-lit -vv -Dopt="/path/to/opt-alive.sh" ${TEST_LLVM_SRC}/test/Transforms/InstCombine/canonicalize-constant-low-bit-mask-and-icmp-sge-to-icmp-sle.ll
  +~/llvm/build/bin/llvm-lit -vv -Dopt=/home/user/alive2/scripts/opt-alive.sh ~/llvm/llvm/test/Transforms/InstCombine/canonicalize-constant-low-bit-mask-and-icmp-sge-to-icmp-sle.ll
  ```
  The output should be:
  -
  ```
  -- Testing: 1 tests, 1 threads --
  PASS: LLVM :: Transforms/InstCombine/canonicalize-constant-low-bit-mask-and-icmp-sge-to-icmp-sle.ll (1 of 1)
  @@ -57,5 +73,5 @@ Testing Time: 0.11s
  Translation validation of the LLVM unit tests:
  ```
  -${TEST_LLVM_BUILD}/bin/llvm-lit -s -Dopt="/path/to/opt-alive.sh" ${TEST_LLVM_SRC}/test/Transforms
  +~/llvm/build/bin/llvm-lit -vv -Dopt=/home/user/alive2/scripts/opt-alive.sh ~/llvm/llvm/test/Transforms
  ```
  