Swoosh Verification Project Setup Guide

Target OS: Ubuntu 22.04 / 24.04 (x86-64)
Purpose: Setup environment for LLVM 12, SMACK, Boogie, PyPy, and the Swoosh verification pipeline.

---

1. System & Dependencies

Update the system and install core build tools, Redis, and the .NET SDK (required for Boogie).

# Update System
sudo apt update && sudo apt upgrade -y

# Install Build Tools & Libraries
sudo apt install -y build-essential cmake libboost-all-dev

# Install Redis (Data Store)
sudo apt install -y redis-server
sudo systemctl enable --now redis-server

# Install .NET 8 SDK (Required for Boogie)
sudo apt install -y dotnet-sdk-8.0

---

2. Build LLVM 12 & Clang

This project requires a specific version of LLVM (v12). We must build it from source as it is no longer in standard repositories.

# 1. Prepare Directory
export LLVM_DIR=$HOME/llvm-dir
mkdir -p "$LLVM_DIR"/{src/build,src/tools/clang,src/projects/compiler-rt}

# 2. Download Sources
cd "$LLVM_DIR"
wget -q [https://github.com/llvm/llvm-project/releases/download/llvmorg-12.0.1/llvm-12.0.1.src.tar.xz](https://github.com/llvm/llvm-project/releases/download/llvmorg-12.0.1/llvm-12.0.1.src.tar.xz)
wget -q [https://github.com/llvm/llvm-project/releases/download/llvmorg-12.0.1/clang-12.0.1.src.tar.xz](https://github.com/llvm/llvm-project/releases/download/llvmorg-12.0.1/clang-12.0.1.src.tar.xz)
wget -q [https://github.com/llvm/llvm-project/releases/download/llvmorg-12.0.1/compiler-rt-12.0.1.src.tar.xz](https://github.com/llvm/llvm-project/releases/download/llvmorg-12.0.1/compiler-rt-12.0.1.src.tar.xz)

# 3. Extract
sudo tar -C src -xf llvm-12.0.1.src.tar.xz --strip-components=1
sudo tar -C src/tools/clang -xf clang-12.0.1.src.tar.xz --strip-components=1
sudo tar -C src/projects/compiler-rt -xf compiler-rt-12.0.1.src.tar.xz --strip-components=1

# 4. Build (Release mode for speed)
cd "$LLVM_DIR/build"
cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release ../src
make -j$(nproc)

# 5. Add to PATH (Add this to your ~/.bashrc as well)
export PATH=$LLVM_DIR/build/bin:$PATH

---

3. Install SMACK

Build SMACK using the LLVM 12 installation from step 2.

# Navigate to your project root or where you want to clone SMACK
cd ~/boogie-parser 
# git clone --recursive <your-repo-url> .  # If not already cloned

# Create Build Directory
mkdir -p smack/build && cd smack/build

# Configure & Build
cmake -G "Unix Makefiles" \
 -DCMAKE_C_COMPILER=clang \
 -DCMAKE_CXX_COMPILER=clang++ \
 -DCMAKE_BUILD_TYPE=Release ..

make -j$(nproc)

---

4. Python Environment Setup

We use PyPy 3.11 for heavy lifting (compiling/interpreting) and standard Python 3 for the driver.

4.1 Install PyPy 3.11

cd /tmp
wget -q [https://downloads.python.org/pypy/pypy3.11-v7.3.19-linux64.tar.bz2](https://downloads.python.org/pypy/pypy3.11-v7.3.19-linux64.tar.bz2)
sudo mkdir -p /opt/pypy-7.3.19
sudo tar -C /opt/pypy-7.3.19 --strip-components=1 -xjf pypy3.11-v7.3.19-linux64.tar.bz2

# Add to PATH (Add this to ~/.bashrc)
echo 'export PATH=/opt/pypy-7.3.19/bin:$PATH' >> ~/.bashrc
source ~/.bashrc

4.2 Install Python Packages

# 1. For PyPy (Compiler & Interpreter)
pypy -m ensurepip --upgrade
pypy -m pip install lark graphviz

# 2. For Standard Python (The Driver & Redis Client)
python3 -m pip install redis

---

5. Install Boogie (Verifier)

# Install Boogie as a global .NET tool
dotnet tool install --global boogie

# Add .NET tools to PATH (if not already present)
if ! grep -q 'DOTNET_TOOLS' ~/.bashrc; then
  printf '\n# DOTNET_TOOLS\nexport PATH="$PATH:$HOME/.dotnet/tools"\n' >> ~/.bashrc
  source ~/.bashrc
fi

---

6. The "Swoosh" Workflow

The pipeline consists of 4 distinct stages. Run these from your project root (~/boogie-parser).

Step 1: Generate (C -> Boogie)

Transpile C code into a Boogie program via SMACK (.bpl).

Step 2: Compile (Boogie -> IR)

Use pypy to compile the BPL file into internal packages.

# Usage: pypy -m tools.compile <file.bpl>
pypy -m tools.compile examples/build/aead.bpl

Step 3: Interpret (Concrete Traces)

Run the interpreter on the compiled package (_pkg folder) to generate execution traces.

# Usage: pypy interpreter.py <pkg_dir>
# Note: The tool automatically adds "_pkg" to the directory name created in Step 2
pypy interpreter.py test_packages/aead_pkg/

Step 4: Verify (The Driver)

Use the standard Python driver to verify the traces against the Redis configuration.

# Usage: python3 -m tools.driver <config.conf>
python3 -m tools.driver redis_conf/aead.conf

Optional: Analysis

Analyze the output logs from the driver.

python3 tools/analyze_driver_out.py driver.out

---

Quick Reference Table

Action	Environment	Command
Generate	bash/smack
Compile	pypy	pypy -m tools.compile ...
Interpret	pypy	pypy interpreter.py ...
Verify	python3	python3 -m tools.driver ...