From 6ab16bfb0ff3569f370b6e383a206e26abefb168 Mon Sep 17 00:00:00 2001 From: zhuyt Date: Mon, 14 Oct 2024 12:54:19 +0800 Subject: [PATCH] update README --- README.md | 86 ++++++++++++++++++++++++++++++++++++------------ scripts/build.sh | 14 +++++--- x.py | 19 +++++------ 3 files changed, 83 insertions(+), 36 deletions(-) diff --git a/README.md b/README.md index 59b1dbc1..e3224feb 100644 --- a/README.md +++ b/README.md @@ -1,39 +1,57 @@ -## SELO +# SELO SELO is a bounded model checking framework for checking memory safety properties in heap-manipulating C programs. It inherits the architecture of [ESBMC](https://github.com/esbmc/esbmc) and components needed for BMC upon Seperation Logic with Heap Variables(SLHV) are added into the framework. -SELO encodes verification conditions(VCs) in SLHV and such VC will be fed to [Z3-SLHV](https://anonymous.4open.science/r/Z3-SLHV) to solve. +SELO encodes verification conditions(VCs) in SLHV and such VC will be fed to [Z3-SLHV](https://anonymous.4open.science/r/Z3-SLHV). -#### Configuring CMake for SELO +## Building SELO shares the same building method with ESBMC, one can refer to ESBMC for detailed information. For convenience, we give some scripts and commands to compile the target. -### Prerequisite + +### Using script(recommended) + +We provide a script `./scripts/build.sh` to automatically configure LLVM and Z3_SLHV and compile SELO. +```sh +./scripts/build.sh +``` +More detail can be found by `-h` arguement. + +*Notice: the script must be executed in root of SELO.* + +### Manually building + +#### Prerequisite Linux: ``` sudo apt-get update && sudo apt-get install build-essential git gperf libgmp-dev cmake bison curl flex g++-multilib linux-libc-dev libboost-all-dev libtinfo-dev ninja-build python3-setuptools unzip wget python3-pip openjdk-8-jre ``` -CMake > 3.22 +CMake >= 3.22 + +#### Alternative 1: Building with shared library -### Alternative 1: Building with shared library **Preparing distributed Clang (recommended for a shared build)** + For shared builds, it is recommended to use the system's LLVM/Clang, which on Ubuntu can be obtained by: ``` apt-get install libclang-cpp11-dev && ESBMC_CLANG="-DLLVM_DIR=/usr/lib/llvm-11/lib/cmake/llvm -DClang_DIR=/usr/lib/cmake/clang-11" && ESBMC_STATIC=OFF ``` -#### Setting up solvers -referring to [Z3-SLHV](https://anonymous.4open.science/r/Z3-SLHV) -#### Configuring CMake for SELO -Before running the following commands, make sure ```your_z3_lib_path``` and ```your_release_path``` are configured in the script file ```mk_make.py```. -``` -mkdir build -python3 mk_make.py --shared +**Preparing distributed Z3-SLHV (recommended for a shared build):** +Referring to [Z3-SLHV](https://anonymous.4open.science/r/Z3-SLHV) + +**Configuring CMake** +```sh +mkdir build && cd build +cmake .. -GNinja -DClang_DIR=/usr/lib/cmake/clang-11 \ + -DLLVM_DIR=/usr/lib/llvm-11/lib/cmake/llvm \ + -DENABLE_Z3_SLHV=On \ + -DZ3_DIR=/z3_slhv_lib ``` -### Alternative 2: Building with static library +#### Alternative 2: Building with static library **Preparing external standard Clang (recommended for a static build)** @@ -44,15 +62,41 @@ tar xfJ clang+llvm-11.0.0-x86_64-linux-gnu-ubuntu-20.04.tar.xz && ESBMC_CLANG=$(echo -D{LLVM,Clang}_DIR=$PWD/clang+llvm-11.0.0-x86_64-linux-gnu-ubuntu-20.04) && ESBMC_STATIC=ON ``` -#### Setting up solvers -referring to [Z3-SLHV](https://anonymous.4open.science/r/Z3-SLHV) +**Preparing distributed Z3-SLHV (recommended for a static build):** +Referring to [Z3-SLHV](https://anonymous.4open.science/r/Z3-SLHV) + +**Configuring CMake** +```sh +mkdir build && cd build +cmake .. -GNinja -DClang_DIR= + -DLLVM_DIR= \ + -DBUILD_STATIC=ON \ + -DENABLE_Z3_SLHV=On \ + -DZ3_DIR=/z3_slhv_lib +``` +Note that all `path_to_*` must be configured correctlly. More details can be found in ESBMC. #### Compile SELO -Before running the following commands, make sure ```your_z3_lib_path``` and ```your_release_path``` are configured in the script file ```mk_make.py```. + +```sh +cd build && cmake --build . ``` -mkdir build -python3 mk_make.py --static +If compiler can not find `z3++.h`, appending arg ` + -DCMAKE_CXX_FLAGS="-I/z3_slhv_lib/include"` solves the issue. + +## Running SELO + +To run SELO, the following arguments must be included. +```sh +--no-library --force-malloc-success --result-only --multi-property --z3-slhv +``` +`--z3-slhv` is a must to enable SELO using SLHV for encoding and using Z3-SLHV for backend solver. + +We also provide a simple script `x.py`. We can easily to run SELO on a single file. For example, we run SELO on "case_1.c" in our benchmark bu the follwing command. +```sh +./x.py --run ./benchmark/tests/case_1.c ``` +Mor details can be found by `./x.py --help` -### Build SELO -TDB: add complation scripts +### TODO +Adjust the script later. \ No newline at end of file diff --git a/scripts/build.sh b/scripts/build.sh index ead9b088..7dfbaeb0 100755 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -34,15 +34,18 @@ ubuntu_setup () { mkdir deps fi cd deps + DEPS_ROOT=$PWD + if [ -z "$STATIC" ]; then - STATIC=static + STATIC=ON + echo "Static building" else - STATIC=shared + echo "Shared building" fi - echo "Configuring Clang-$CLANG_VERSION: $STATIC" - if [ $STATIC = shared ]; then + echo "Configuring Clang-$CLANG_VERSION" + if [ $STATIC = OFF ]; then PKGS="$PKGS \ llvm-$CLANG_VERSION-dev \ libclang-$CLANG_VERSION-dev \ @@ -62,7 +65,7 @@ ubuntu_setup () { fi - echo "Configuring Z3_SLHV: $STATIC" + echo "Configuring Z3_SLHV" if [ ! -d "Z3-SLHV" ]; then git clone https://github.com/SpencerL-Y/Z3-SLHV.git fi @@ -71,6 +74,7 @@ ubuntu_setup () { rm -r build && python3 mk_${STATIC}_cmake.py cd build && ninja install fi + cd $DEPS_ROOT/Z3-SLHV BASE_ARGS="$BASE_ARGS -DBUILD_STATIC=$STATIC" SOLVER_FLAGS="$SOLVER_FLAGS \ -DZ3_DIR=$PWD/z3_slhv_lib \ diff --git a/x.py b/x.py index c6071f53..c515967a 100755 --- a/x.py +++ b/x.py @@ -26,7 +26,6 @@ def help(): os.system(f"{selo} -h") cmds = { - "--init" : ('', "Init output directory"), "--compile" : ('',"Compile esbmc"), "--run" : ("file extra_args","Only test a single file 'file'"), "--experiment": ("path extra_args", "Run on a benchmark 'path'"), @@ -329,17 +328,17 @@ def run_expriment_on(benchmark_root, extra_args): if __name__ == '__main__': + if not os.path.exists(output_root): + os.mkdir(output_root) + if not os.path.exists(log_root): + os.mkdir(log_root) + if not os.path.exists(vcc_log): + os.mkdir(vcc_root) + if "--esbmc" in sys.argv: csv_file = os.path.join(output_root, "results_esbmc.csv") - - if sys.argv[1] == "--init": - if not os.path.exists(output_root): - os.mkdir(output_root) - if not os.path.exists(log_root): - os.mkdir(log_root) - if not os.path.exists(vcc_log): - os.mkdir(vcc_root) - elif sys.argv[1] == "--compile": + + if sys.argv[1] == "--compile": compile() elif sys.argv[1] == "--run": run_on(sys.argv[2], sys.argv[3:])