Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tweak ReadMe: Variablize uses of ~/llvm in the build instructions, #945

Merged
merged 15 commits into from
Oct 14, 2023
Merged

Tweak ReadMe: Variablize uses of ~/llvm in the build instructions, #945

Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
22b06d5
Add official links for the non-obvious (at least to me) Prerequisites.
FlashSheridan Oct 10, 2023
63bbcb1
Note that the example LLVM build instruction targets X86.
FlashSheridan Oct 10, 2023
6154100
Also link the obvious prerequisites
FlashSheridan Oct 10, 2023
8bd3c88
Variablize the uses of ~/llvm in the build instructions.
FlashSheridan Oct 10, 2023
f5a8445
Also variablize the directory above …/alive2/
FlashSheridan Oct 10, 2023
3116242
Relativize changing to your llvm directory,
FlashSheridan Oct 10, 2023
cb3d1c4
Also variablize the LLVM build directory (our build script puts it so…
FlashSheridan Oct 10, 2023
88d0510
Make explicit the directory for Building Translation Validation.
FlashSheridan Oct 10, 2023
b26fc3f
Use https://github.com/llvm/llvm-project for LLVM link, since
FlashSheridan Oct 10, 2023
2f674f3
Adjust LLVM2_HOME for default clone directory name.
FlashSheridan Oct 10, 2023
cf9e400
Actually build LLVM
FlashSheridan Oct 10, 2023
346b174
Note how to build with Clang. (gcc gave lots of warnings on
FlashSheridan Oct 10, 2023
0a0b6c6
Actually build Alive2
FlashSheridan Oct 10, 2023
080a1e5
Remove one more hard-coded “llvm”
FlashSheridan Oct 13, 2023
f0c74e3
Also give the syntax for the new pass manager, with an actual file,
FlashSheridan Oct 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 32 additions & 18 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,18 +31,23 @@ spurious counterexamples if run with such passes.
Prerequisites
-------------
To build Alive2 you need recent versions of:
* cmake
* gcc/clang
* re2c
* Z3
* LLVM (optional)
* hiredis (optional, needed for caching)
* [cmake](https://cmake.org)
* [gcc](https://gcc.gnu.org)/[clang](https://clang.llvm.org)
* [re2c](https://re2c.org/)
* [Z3](https://github.com/Z3Prover/z3)
* [LLVM](https://github.com/llvm/llvm-project) (optional)
* [hiredis](https://github.com/redis/hiredis) (optional, needed for caching)


Building
--------

```
export ALIVE2_HOME=$PWD
export LLVM2_HOME=$PWD/llvm-project
export LLVM2_BUILD=$LLVM2_HOME/build
git clone [email protected]:AliveToolkit/alive2.git
cd alive2
mkdir build
cd build
cmake -GNinja -DCMAKE_BUILD_TYPE=Release ..
Expand All @@ -58,26 +63,35 @@ Building and Running Translation Validation

Alive2's `opt` and `clang` translation validation requires a build of LLVM with
RTTI and exceptions turned on.
LLVM can be built in the following way:
LLVM can be built targeting X86 in the following way. (You may prefer to add `-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++` to the CMake step if your default compiler is `gcc`.)
```
cd llvm
cd $LLVM2_HOME
mkdir build
cd build
cmake -GNinja -DLLVM_ENABLE_RTTI=ON -DLLVM_ENABLE_EH=ON -DBUILD_SHARED_LIBS=ON -DCMAKE_BUILD_TYPE=Release -DLLVM_TARGETS_TO_BUILD=X86 -DLLVM_ENABLE_ASSERTIONS=ON -DLLVM_ENABLE_PROJECTS="llvm;clang" ../llvm
ninja
```

Alive2 should then be configured as follows:
Alive2 should then be configured and built as follows:
```
cmake -GNinja -DCMAKE_PREFIX_PATH=~/llvm/build -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=Release ..
cd $ALIVE2_HOME/alive2/build
cmake -GNinja -DCMAKE_PREFIX_PATH=$LLVM2_BUILD -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=Release ..
ninja
```

Translation validation of one or more LLVM passes transforming an IR file on Linux:
```
~/llvm/build/bin/opt -load $HOME/alive2/build/tv/tv.so -load-pass-plugin $HOME/alive2/build/tv/tv.so -tv -instcombine -tv -o /dev/null foo.ll
$LLVM2_BUILD/bin/opt -load $ALIVE2_HOME/alive2/build/tv/tv.so -load-pass-plugin $ALIVE2_HOME/alive2/build/tv/tv.so -tv -instcombine -tv -o /dev/null foo.ll
```
For the new pass manager:
```
$LLVM2_BUILD/bin/opt -load $ALIVE2_HOME/alive2/build/tv/tv.so -load-pass-plugin $ALIVE2_HOME/alive2/build/tv/tv.so -passes=tv -passes=instcombine -passes=tv -o /dev/null $LLVM2_HOME/llvm/test/Analysis/AssumptionCache/basic.ll
```


On a Mac:
```
~/llvm/build/bin/opt -load $HOME/alive2/build/tv/tv.dylib -load-pass-plugin $HOME/alive2/build/tv/tv.dylib -tv -instcombine -tv -o /dev/null foo.ll
$LLVM2_BUILD/bin/opt -load $ALIVE2_HOME/alive2/build/tv/tv.dylib -load-pass-plugin $ALIVE2_HOME/alive2/build/tv/tv.dylib -tv -instcombine -tv -o /dev/null foo.ll
```
You can run any pass or combination of passes, but on the command line
they must be placed in between the two invocations of the Alive2 `-tv`
Expand All @@ -86,7 +100,7 @@ pass.

Translation validation of a single LLVM unit test, using lit:
```
~/llvm/build/bin/llvm-lit -vv -Dopt=$HOME/alive2/build/opt-alive.sh ~/llvm/llvm/test/Transforms/InstCombine/canonicalize-constant-low-bit-mask-and-icmp-sge-to-icmp-sle.ll
$LLVM2_BUILD/bin/llvm-lit -vv -Dopt=$ALIVE2_HOME/alive2/build/opt-alive.sh $LLVM2_HOME/llvm/llvm/test/Transforms/InstCombine/canonicalize-constant-low-bit-mask-and-icmp-sge-to-icmp-sle.ll
```

The output should be:
Expand All @@ -101,7 +115,7 @@ To run translation validation on all the LLVM unit tests for IR-level
transformations:

```
~/llvm/build/bin/llvm-lit -vv -Dopt=$HOME/alive2/build/opt-alive.sh ~/llvm/llvm/test/Transforms
$LLVM2_BUILD/bin/llvm-lit -vv -Dopt=$ALIVE2_HOME/alive2/build/opt-alive.sh $LLVM2_HOME/llvm/llvm/test/Transforms
```

We run this command on the main LLVM branch each day, and keep track of the results
Expand All @@ -116,15 +130,15 @@ by LLVM. Invoke the plugin like this:

```
$ clang -O3 <src.c> -S -emit-llvm \
-fpass-plugin=$HOME/alive2/build/tv/tv.so \
-Xclang -load -Xclang $HOME/alive2/build/tv/tv.so
-fpass-plugin=$ALIVE2_HOME/alive2/build/tv/tv.so \
-Xclang -load -Xclang $ALIVE2_HOME/alive2/build/tv/tv.so
```

Or, more conveniently:

```
$ $HOME/alive2/build/alivecc -O3 -c <src.c>
$ $HOME/alive2/build/alive++ -O3 -c <src.cpp>
$ $ALIVE2_HOME/alive2/build/alivecc -O3 -c <src.c>
$ $ALIVE2_HOME/alive2/build/alive++ -O3 -c <src.cpp>
```

The Clang plugin can optionally use multiple cores. To enable parallel
Expand Down