This reproducibility package is publicly available at github.com/UQ-PAC/basil-tv-artifact.
It has been tested on Fedora x86_64 using podman, on machine with a 13th Gen Intel(R) Core(TM) i7-12700.
The following instructions use podman, all commands should also be compatible with
the docker invocation in place of podman.
If your system only has docker, consider using alias podman=docker to allow
copy-pasting the commands below.
The host shell used throughout is bash.
At least 16 gb of ram is likely neccessary to run the artifact. The benchmarks have been tested with 24 gb and 32 gb.
podman image load -i basil-tv-artifact-image.tar.gz
The logs are stored in results-logs.
The table can be made using:
podman run ghcr.io/uq-pac/basil-tv-artifact:latest bash scripts/repro-from-logs.sh
+----+-------------------------------------------------+---------+-----------------+----------+------------------+-----------------+----------------+--------------+
| | prog | stmts | Delta stmt. % | guards | simp. guards % | result U,S,TO | procs U,S,TO | time (min) |
|----+-------------------------------------------------+---------+-----------------+----------+------------------+-----------------+----------------+--------------|
| 0 | out/basilbenchbase-catcatgtirb | 8104 | -28.4921 | 380 | 97.3684 | (216, 0, 0) | (34, 0, 0) | 50.7885 |
| 0 | out/basilbenchbase-datedategtirb | 14137 | -36.309 | 568 | 98.5915 | (300, 0, 0) | (51, 0, 0) | 111.172 |
| 0 | out/basilbenchbase-stringsstringsgtirb | 11563 | -28.0896 | 498 | 98.3936 | (308, 0, 0) | (51, 0, 0) | 57.699 |
| 0 | out/basilbenchcntlm-nodukcntlm-noduk_gtirb | 122563 | -56.2168 | 2414 | 100 | (952, 0, 0) | (124, 0, 0) | 396.249 |
| 0 | out/basilbenchcntlm-nodukcntlm-nodukgtirb | 97609 | -42.5524 | 2622 | 99.7712 | (928, 0, 0) | (110, 0, 0) | 756.456 |
| 0 | out/basilbenchgzipgzip_gtirb | 60031 | -60.1772 | 1436 | 99.8607 | (696, 0, 0) | (76, 0, 0) | 152.577 |
| 0 | out/basilbenchgzipgzipgtirb | 39929 | -33.6823 | 1656 | 99.0942 | (612, 0, 0) | (48, 0, 0) | 443.768 |
+----+-------------------------------------------------+---------+-----------------+----------+------------------+-----------------+----------------+--------------+
This simply calls the script plots/summary.py on each subdirectory of results-logs/out. These each contain
- A csv file containing the result of each smt solver run:
tv_veri_result.csv - The output of the basil decompiler with extra bookmarking log messages enabled:
output
Similar log files are produced in the ./out/ host directory by the following tasks, which mount this folder into the container.
export TASK=basilbench/conds/conds.gtirb ; time podman run -e JOBS="$JOBS" -e TIMEOUT="$TIMEOUT" -v ./out:/home/opam/out:Z,U,rw -it \
ghcr.io/uq-pac/basil-tv-artifact:latest bash scripts/run.sh $TASK
The jobs evironment variable corresponds to the number of concurrent TV queries to solve. It is generally recommended to limit jobs to 1 or 2, as each job already runs a portfolio of 3 solvers.
Timeout defaults to "1m" meaning 1m, this could be reduced to 10s to reduce total time.
-
Check that the results have appeard in the directory out/
-
It should output the following table:
+----+-------------------------------+---------+-----------------+----------+------------------+-----------------+----------------+--------------+ | | prog | stmts | Delta stmt. % | guards | simp. guards % | result U,S,TO | procs U,S,TO | time (min) | |----+-------------------------------+---------+-----------------+----------+------------------+-----------------+----------------+--------------| | 0 | out/basilbenchcondscondsgtirb | 46 | -71.7391 | 2 | 100 | (4, 0, 0) | (1, 0, 0) | 0.0837277 | +----+-------------------------------+---------+-----------------+----------+------------------+-----------------+----------------+--------------+
The out folder on the host should contain the following files:
out/basilbenchcondscondsgtirb/summary.csv--- row summary table corresponding to this benchmarkout/basilbenchcondscondsgtirb/tv_veri_result.csv--- result of every smt queryout/basilbenchcondscondsgtirb/*.smt2--- all the verification tasks emitted by the translation validator
An individual benchmark can be run by replacing the TASK variable in the above command with one of the below:
basilbench/9base-6/cat/cat.gtirb basilbench/9base-6/strings/strings.gtirb basilbench/9base-6/date/date.gtirb basilbench/gzip/gzip_O0.gtirb basilbench/gzip/gzip.gtirb basilbench/cntlm-noduk/cntlm-noduk.gtirb basilbench/cntlm-noduk/cntlm-noduk_O0.gtirb
E.g.,
export TASK=basilbench/9base-6/cat/cat.gtirb
time podman run -e JOBS="2" -e TIMEOUT="1m" -v ./out:/home/opam/out:Z,U,rw -it \
ghcr.io/uq-pac/basil-tv-artifact:latest bash scripts/run.sh $TASKOutputs the following in one around minute on a computer with a 12th Gen Intel(R) Core(TM) i7-12700:
+----+--------------------------------+---------+-----------------+----------+------------------+-----------------+----------------+--------------+
| | prog | stmts | Delta stmt. % | guards | simp. guards % | result U,S,TO | procs U,S,TO | time (min) |
|----+--------------------------------+---------+-----------------+----------+------------------+-----------------+----------------+--------------|
| 0 | out/basilbenchbase-catcatgtirb | 8104 | -28.4921 | 380 | 97.3684 | (216, 0, 0) | (34, 0, 0) | 76.063 |
+----+--------------------------------+---------+-----------------+----------+------------------+-----------------+----------------+--------------+
________________________________________________________
Executed in 56.34 secs fish external
usr time 0.35 secs 0.04 millis 0.35 secs
sys time 1.92 secs 1.02 millis 1.92 secs
They can also be run by calling the run script inside the container:
host $ podman run -v ./out:/home/opam/out:Z,U -it \
ghcr.io/uq-pac/basil-tv-artifact:latest bash
(env) opam@5f7e449e29df $ export TASK=basilbench/9base-6/cat/cat.gtirb
(env) opam@5f7e449e29df $ time bash scripts/run.sh $TASK
time podman run -e JOBS="$JOBS" -e TIMEOUT="$TIMEOUT" -v ./out:/home/opam/out:Z,U,rw -it ghcr.io/uq-pac/basil-tv-artifact:latest bash scripts/runnow.shThis can take a substantial amount of time (multiple hours)
Internally, what this script does is:
- Run basil on all the benchmark binaries (
$dirnamewill have a name of the formatout/<benchmark name>)
- Dump the final IL output in the file
$dirname-output.il - Dump all the SMT queries in
$dirname/*.smt2 - Dump intermediate IL files in
$dirname/*.il
- Run the post-processor and SMT solver on each
.smtfile and collect results in$dirname/tv_veri_results.csv. This takes a substantial amount of time.
By default the number of jobs used is set to the number of cores available (the result of nproc).
The timeout defaults to 60 minutes. These can be configured with the JOBS and TIMEOUT environment variables:
time podman run -e JOBS=2 -e TIMEOUT=10s -v ./out:/home/opam/out:Z,U,rw -it ghcr.io/uq-pac/basil-tv-artifact:latest bash scripts/runnow.shTIMEOUT is passed to the command timeout which supports the following
format:
DURATION is a floating point number with an optional suffix: 's' for seconds (the default), 'm' for minutes, 'h' for hours or 'd' for days. A duration of 0 disables the associated timeout.
Note that the solver already runs as portfolio so do not set JOBS higher than nproc / 3.
Be aware that a large number of jobs and longer timeouts can easily lead to memory exhaustion.
On an M4 Mac with
JOBS=4 TIMEOUT=5sthis task took around 25 minutes.
time podman run -e JOBS=1 -e TIMEOUT="1m" -v ./out:/home/opam/out:Z,U,rw -it ghcr.io/uq-pac/basil-tv-artifact:latest bash scripts/benchpress.sh
open comparison_plot_cactus.pdf
This can take a substantial amount of time (multiple hours), consider reducing the timeout to 10 seconds as several cases in the axiom benchmark do time-out.
Both of these emit output to the folder 'out'.
The container can be inspected interactively with the following command:
podman run -v ./out:/home/opam/out:Z,U -it \
ghcr.io/uq-pac/basil-tv-artifact:latest bashNow the script can be invoked manually on a specific file:
(env) opam@d5a03f21c22c:~$ bash scripts/run.sh basilbench/conds/conds.gtirb
The container can be inspected with the following:
time podman run -v ./out:/home/opam/out:Z,U -it ghcr.io/uq-pac/basil-tv-artifact:latest bash
Inside we have:
opam@79a5e5547cfe:~$ ls -1
BASIL # BASIL decompiler source code
basilbench # Benchmark binaries
scripts # Benchmark scripts
tblproc # Benchmark scripts
plots # Benchmark scripts
tv-sanity # Interactive TV effect solver processThe source code for the paper's main contribution is located under the
directory BASIL/src/main/scala/ir/transforms/validate. Notably
BASIL/src/main/scala/ir/transforms/validate/SimplifyPipeline.scala contains
the validated transform pipeline and invariant extraction code. Some
documentation of this can be found under BASIL/docs/src/development/tv.
The container has the followign files:
- BASIL : basil source code (includes translation validator at path
BASIL/src/main/scala/ir/transforms/validate/) - basilbench : pre-disassembled benchmark programs (the
.gtirbfiles) and their sources - scripts : experiment scripts
- out : the results of running the experiments, with a subfolder per benchmark, il file output, .smt TV proofs, and .csv result tables
- tv-sanity: post-processing of SMT file and run interactive queries to simplify traces, before final SMT solver run
To run the tool on a specific example from inside the container we can use the
run.sh script (from inside the container) and provide it a gtirb file.
This reproducibility package is publicly available at github.com/UQ-PAC/basil-tv-artifact.
The Containerfile builds an image containing the following dependencies:
- smt solvers cvc5 and z3
- java, scala toolchain bootstrapped by mill
- basil source code, copied from git submodules of translation validation branch github.com/uq-pac/basil
- pre-compiles and ddisasm lifted benchmark programs available at https://github.com/agle/basilbench
- ocaml, and smt and result processing scripts
The image can be built with:
git clone --recurse-submodules https://github.com/UQ-PAC/basil-tv-artifact.git
cd basil-tv-artifact
podman build . -t ghcr.io/uq-pac/basil-tv-artifact:latest
The above instructions can then be used to run benchmark tasks
The test that runs tv on a transform which randomly modifies the program is
enabled by running the script scripts/runbroken.sh
The script scripts/pc-tracking.sh greps for assertions which have been simplified to true
by the decompiler and prints counts.
Benchmark programs are located in ./basilbench, these are pre-compiled and
lifted. The compiler and disassembly toolchain is not included in the main
artifact.
To compile and lift new benchmarks from c source code, the script here can be used, this pulls a separate docker container which includes cross-compilers linux-elf aarch64 (basil's only supported input) and ddisasm.
You can start the container and leave it running, and use podman exec (rather than podman run),
so you can enter and detach without removing the continer,
for example if mounting ./out does not work
podman run -d --rm --name basil-tv-artifact ghcr.io/uq-pac/basil-tv-artifact:latest infinitymkdir out
podman run -it ghcr.io/uq-pac/basil-tv-artifact:latest /bin/bashIf the output is something along the lines of:
Error: creating container storage: the container name "basil-tv-artifact" is already in use by <sha>. You have to remove that container to be able to r
euse that name: that name is already in use, or use --replace to instruct Podman to do so.
The container is already running and nothing needs to be done.
(!) subsequent commands expect the container to have the name
basil-tv-artifact as set above
Assuming the container has been started as above, the following commands run the basil decompiler and translation validator on the trivial example in Figure 2.
time podman exec basil-tv-artifact bash scripts/run.sh basilbench/conds/conds.gtirb | tee -a preverify-output.log
podman cp basil-tv-artifact:/home/opam/out .Once the experiments are finished the container can be stopped and removed with
podman kill basil-tv-artifact
gtirb-pprinter basilbench/9base-6/cat/cat.gtirb > basilbench/9base-6/cat/cat.gtirb.asm gtirb-pprinter basilbench/9base-6/strings/strings.gtirb > basilbench/9base-6/strings/strings.gtirb.asm gtirb-pprinter basilbench/9base-6/date/date.gtirb > basilbench/9base-6/date/date.gtirb.asm gtirb-pprinter basilbench/gzip/gzip_O0.gtirb > basilbench/gzip/gzip_O0.gtirb.asm gtirb-pprinter basilbench/gzip/gzip.gtirb > basilbench/gzip/gzip.gtirb.asm gtirb-pprinter basilbench/cntlm-noduk/cntlm-noduk.gtirb > basilbench/cntlm-noduk/cntlm-noduk.gtirb.asm gtirb-pprinter basilbench/cntlm-noduk/cntlm-noduk_O0.gtirb > basilbench/cntlm-noduk/cntlm-noduk_O0.gtirb.asm