update README

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=<path_to_Z3-SLHV>/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=<path_to_cmake/clang-11>
+  -DLLVM_DIR=<path_to_llvm-11/lib/cmake/llvm> \
+  -DBUILD_STATIC=ON \
+  -DENABLE_Z3_SLHV=On \
+  -DZ3_DIR=<path_to_Z3-SLHV>/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<path_to_Z3-SLHV>/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.

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 \

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:])