- keystone (optional)
pip install keystone-engine
- Clang (optional)
Our assembler version can use clang. We have tested our implementation with version llvm 15. Other versions are untested; you can try to use them, but YMMV.
- gcc-aarch64-linux-gnu
sudo apt install binutils-aarch64-linux-gnu
sudo apt install gcc-aarch64-linux-gnu
- ply
Ply is our specification parser.
pip install ply
- Bitwuzla
Our smt solver now default to bitwuzla. We have tested our implementation with version 0.6.0. Other versions are untested; you can try to use them, but YMMV.
To build Bitwuzla, run
$ https://github.com/bitwuzla/bitwuzla.git
$ cd bitwuzla
$ pip install meson
$ python configure.py --shared
$ cd build
$ sudo ninja install
$ sudo ldconfig
Note: Remember to record the output path of bitwuzla/c/bitwuzla.h and libbitwuzla.so when running sudo ninja install and add it to enviroment variable BITWUZLA_INCLUDE_DIRS and BITWUZLA_LIBRARIES for triton to build with bitwuzla. For instance,
export BITWUZLA_INCLUDE_DIRS="/usr/local/include"
export BITWUZLA_LIBRARIES="/usr/local/lib64/libbitwuzla.so"
- Triton
Triton relies on the following dependencies:
* libcapstone >= 5.0.1 https://github.com/capstone-engine/capstone
* libboost (optional) >= 1.68
* libpython (optional) >= 3.6
* libz3 >= 4.8.12 https://github.com/Z3Prover/z3
* libbitwuzla >= 0.4.x https://github.com/bitwuzla/bitwuzla
* llvm >= 15
For ubuntu 22.04, run
$ git clone https://github.com/GreenieQwQ/EA_Trition.git
$ cd Triton
$ mkdir build ; cd build
$ cmake ..
$ make -j3
$ sudo make install
Note: maybe simply run python setup.py build and copy the built python stubs to your python enviroment root also do the job (reference EA_Trition/fastbuild.sh).
Note2: note that the capstone version is 5.0.1. And maybe you should run
$ ln -s /usr/lib/libcapstone.so.5 /usr/lib/x86_64-linux-gnu/libcapstone.so
to manually link capstone with the runtime library.
Other platform are untested; you can try to use them, but YMMV.
First, change the current directory to the root of the EA project. Then run
$ ./run.sh -f1 <ASM_FILE1> -f2 <ASM_FILE2>
For example, try
$ ./run.sh -f1 data/inEqTests/p7.s -f2 data/inEqTests/p7_add1.s
or
$ ./run.sh -f1 data/memoryTests/sumArray.s -f2 data/memoryTests/sumArray_inEq.s
with memory involved.
First, change the current directory to the root of the EA project. Then run
$ ./run_tc_gen.sh -f <ASM_FILE> -cp <CEX_FILE>
For example, try
$ ./run_tc_gen.sh -f data/eqTests/csel_b.s -cp cex.json -n 3
or
$ ./run_tc_gen.sh -f data/memoryTests/sumArray.s -cp cex.json -n 1
with memory involved.
The run.sh simply expands to
export PYTHONPATH="src/preProcess":$PYTHONPATH
export PYTHONPATH="src/symbolic_engine":$PYTHONPATH
export PYTHONPATH="src/specification":$PYTHONPATH
python src/main.py $@which means that you can simply set the enviroment variable PYTHONPATH with the absolute path of src/preProcess, src/symbolic_engine and src/specification, then you can run main.py everywhere.
With argument -sp <spec file>, we can run EA under certain precondition specified in spec file. For example, run
$ ./run.sh -sa -f1 data/stackTests/ex1.s -f2 data/stackTests/ex1_ineq.s -sp data/stackTests/spec/nocross.spec
The constraint in nocross.spec expands to
(x0 <= -2 && x0 >= -0xfffffff) || (x0 >= 0 && x0 <= 0xfffffff)
#NOTE: currently spec can only constraint whole x0, e.g., w0 <= 0xffff is equal to x0 <= 0xffff
#NOTE2: use '#' to comment
x0 == x0
#NOTE3: we conjuct lines, i,e., the whole spec acts as "((x0 <= -2 && x0 >= -0xfffffff) || (x0 >= 0 && x0 <= 0xfffffff)) && (x0 == x0)"
The codes are inequal when w0 < -2 and w0 > 0, but remains equal for the rest of the input. For example, you can run
$ ./run.sh -sa -f1 data/stackTests/ex1.s -f2 data/stackTests/ex1_ineq.s
to get a fair counterexample. Under the precondition specified in nocross.spec (which is w0 <= -2 && w0 >= 0), the two codes are equal.
usage: main.py [-h] [--bound BOUND] --file1 FILE1 --file2 FILE2 [--solver {z3,bitwuzla}] [--smtTimeout SMTTIMEOUT]
[--directByte] [--stackArray] [--perByte] [--quiet] [--cexPath CEXPATH] [--specPath SPECPATH]
[--retReg RETREG] [--pathProjection] [--trivialCache] [--redundantCache] [--unsatCoreCache]
Asm equivalence checker.
options:
-h, --help show this help message and exit
--bound BOUND, -b BOUND
Equivalence checking bound (default: 4)
--file1 FILE1, -f1 FILE1
The first asm file
--file2 FILE2, -f2 FILE2
The second asm file
--solver {z3,bitwuzla}, -s {z3,bitwuzla}
The smt solver (z3/bitwuzla). Default bitwuzla.
--smtTimeout SMTTIMEOUT, -st SMTTIMEOUT
SMT timeout in milliseconds (default: 0 -- no timeout)
--directByte, -db Prompt that the asm files are in byte form instead of strings. (default off)
--stackArray, -sa Use independent array to model stack. (default off)
--perByte, -pb Check equivalence per byte instead of whole array. (default off)
--quiet, -q Disable verbose logging mode. (default off)
--cexPath CEXPATH, -cp CEXPATH
The path for counterexample file (json format)
--specPath SPECPATH, -sp SPECPATH
The path for specification file
--retReg RETREG, -rr RETREG
The name of return register (default x0, example: -rr x1).
--pathProjection, -pp,
Enable path projection. (default off)
--trivialCache, -tc,
Enable caching when solving constraints. (default off)
--redundantCache, -rc,
Enable caching for path conditions. (default off)
--unsatCoreCache, -uc,
Enable caching for unsat cores. (default off)
For AArch64 semantics, reference this doc.