MESA Mathematical Execution for Safety Assurance of Numerical Applications

Downloads

How to build MESA (Augmented Weak Distance)

MESA infers program reachability by (1) extracting feasible control‑flow paths from LLVM IR and (2) minimizing an augmented weak‑distance objective over those paths. This page shows how to build and run MESA using Docker (recommended) and how to run it natively for development.

Download MESA

Download code from here.

Download sources from here.

The Docker workflow builds a ready‑to‑use environment with LLVM 14, glog, and Python dependencies.

Option A — Docker (recommended)

  1. Build the image (from the repository root):

    ./mydocker.sh build .             # uses the Dockerfile in the repo (clang/LLVM 14)

  2. Start a container with the repo mounted:

    ./mydocker.sh run .               # drops you in /mnt inside the container

  3. Inside the container you can now run the quickstart below.

Option B — Native (developers)

Install prerequisites (Debian/Ubuntu example):

sudo apt-get update
sudo apt-get install -y clang-14 llvm-14 llvm-14-tools opt \
    python3 python3-venv python3-dev python3-pip \
    libgoogle-glog-dev libgtest-dev cmake graphviz jq
pip3 install numpy==2.0.1 scipy==1.13.1
# Build and install GoogleTest static libs (system packages sometimes omit them)
cd /usr/src/gtest && sudo cmake . && sudo make && sudo mv lib/libgtest*.a /usr/local/lib

How to use

These are quickstart instructions using an example benchmark and the provided build scripts.

Quickstart (single benchmark)

  1. Provide a benchmark config (example under test_data/):

    # choose one config, e.g., test_data/21_*/config.json
CONFIG=test_data/21_foo/config.json

  2. Build the analysis artifact euler.so for this config:

    make clean_euler                       # ensure a fresh build
make configfile="$CONFIG" euler.so

  3. Generate path specifications:

    make PATHS.txt
# Creates PATHS.txt based on LLVM passes (label_basic_blocks, find_paths)

  4. Run the minimization driver:

    python3 src/min.py

What you get

  • euler.so — the analysis shared library implementing the augmented objective and instrumentation hooks.
  • PATHS.txt — the set of boolean branch decisions for each discovered path.
  • Console logs with per‑path minimization results and an overall reachability verdict (REACHABLE if any path minimizes to 0).

  • Intermediate IR artifacts helpful for debugging:

    • foo.ll (IR from the input C), label.ll (labeled blocks), foo_embed.ll (with __pen_* calls), foo_x.o, etc.

Batch run (multiple benchmarks)

Use the provided helper to iterate over many config.json files:

./run_newton.sh

The script times three phases for each config: (1) build euler.so, (2) compute PATHS.txt, and (3) run src/min.py. It prints per‑step and total CPU time.

Alternate quickstart on a supplied IR

If you want to exercise the call_to_block → label_basic_blocks → find_paths pipeline directly on a sample .ll file:

./quick_run.sh

This runs the three passes and ensures the outputs are created in test_data/challenge11/.

Configuration

MESA reads parameters from config.json to control path search and entry/target selection. Typical keys include:

  • entry_func_name — entry function of the analysis (e.g., foo).
  • target_func_name — reachability target (e.g., __logic_error_marker).
  • max_number_paths, max_path_depth, max_call_stack_size — BFS bounds for path search.
  • foo, foox, foo_inc — input sources for the benchmark (see the Makefile rules foo.c, foo_x.c, and foo.ll).
  • euler_lib_flags — extra linker flags when producing euler.so.

You can switch benchmarks by passing configfile=<path> to make, which copies it to ./config.json and records the source path.

Developer notes

Build system

  • LLVM passes live under src/ and compile to loadable .so files: label_basic_blocks.so, find_paths.so, get_types.so, embed.so, call_to_block.so.
  • make euler.so links src/pen.o, foo_embed.ll, and foo_x.o into the runtime library used by min.py.
  • make PATHS.txt runs opt with the analysis passes to materialize the boolean path file consumed by the minimizer.

Running the Python minimizer

  • src/min.py uses ctypes to load euler.so and Scipy’s basinhopping to minimize the objective over each path.

  • By default it expects ./euler.so and ./PATHS.txt. You can point to alternates:

    python3 src/min.py --euler ./euler.so --paths ./PATHS.txt --dimension 1

Troubleshooting

“cannot open shared object file” when loading euler.so

  • Make sure the .so matches your CPU architecture: file ./euler.so should say x86-64 if you’re on x86‑64.

  • If you previously built for a different arch, clean and rebuild:

    make clean_euler && make clean
make configfile="$CONFIG" euler.so

Linker says Relocations in generic ELF (EM: 183) or file in wrong format

  • Stale ARM64 objects are being linked on x86‑64. Remove intermediates and rebuild as above.

ldd ./euler.so shows missing deps

  • Install the required libs (inside Docker they’re preinstalled):

    sudo apt-get install -y libstdc++6 libgoogle-glog0v5 libgflags2.2

  • If you use custom prefixes, update the runtime path:

    export LD_LIBRARY_PATH=/usr/local/lib:/usr/lib:$LD_LIBRARY_PATH
sudo ldconfig

Pass pipeline didn’t create PATHS.txt

  • Re‑run labeling and find‑paths on a fresh IR:

    rm -f foo.ll foo_embed.ll label.ll PATHS.txt
make PATHS.txt

  • Check config.json for entry_func_name / target_func_name correctness.

Verbose C++ logging

  • min.py initializes glog at WARNING level. For deeper debugging, change the level or call init_glog differently in src/min.py.

Reference: key files & scripts

  • Makefile — targets for building passes, euler.so, and PATHS.txt; helpers clean_euler, test, etc.
  • Dockerfile — LLVM 14 base image with glog, googletest, numpy/scipy pinned.
  • mydocker.sh — build and run helpers for Docker.
  • quick_run.sh — one‑shot pipeline on a sample .ll.
  • run_newton.sh — batch runner over multiple test_data/*/config.json.
  • src/min.py — optimization driver calling euler() per path.

(Optional) Build without Docker — concise recipe

# Prereqs
sudo apt-get update && sudo apt-get install -y \
  clang-14 llvm-14 llvm-14-tools opt libgoogle-glog-dev libgtest-dev cmake \
  python3 python3-dev python3-pip graphviz jq && \
  pip3 install numpy==2.0.1 scipy==1.13.1 && \
  (cd /usr/src/gtest && sudo cmake . && sudo make && sudo mv lib/libgtest*.a /usr/local/lib)

# Build and run a benchmark
make clean_euler && make clean
make configfile=test_data/21_foo/config.json euler.so
make PATHS.txt
python3 src/min.py

Last updated: 2025‑10‑13.