feat: Dockerfile for bv-evaluation scripts

.gitignore

@@ -38,3 +38,4 @@ test-semantics/*.llvm
 *.olean
 lakefile.olean
 .lake/
+docker-results

SSA/Projects/InstCombine/HackersDelight/ch2_1DeMorgan.lean

@@ -14,39 +14,39 @@ variable {x y z : BitVec WIDTH}
 
 theorem not_and_eq_not_or_not :
     ~~~ (x &&& y) = ~~~ x ||| ~~~ y := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_or_eq_not_and_not :
     ~~~ (x ||| y) = ~~~ x &&& ~~~ y := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_add_one_eq_not_sub_one :
     ~~~ (x + 1) = ~~~ x - 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_sub_one_eq_not_add_one :
     ~~~ (x - 1) = ~~~ x + 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_neg_eq_sub_one :
     ~~~ (- x) = x - 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_xor_eq_not_xor :
     ~~~ (x ^^^ y) = ~~~ x ^^^ y := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem q_not_xor :
     ~~~ (x ^^^ y) = ~~~ x ^^^ y := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_add_eq_not_sub :
     ~~~ (x + y) = ~~~ x - y := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_sub_eq_not_add :
     ~~~ (x - y) = ~~~ x + y := by
-  all_goals sorry
+  all_goals bv_compare'
 
 end DeMorgansLawsExtended
 

SSA/Projects/InstCombine/HackersDelight/ch2_2AdditionAndLogicalOps.lean

@@ -12,91 +12,91 @@ variable {x y z : BitVec WIDTH}
 
 theorem neg_eq_not_add_one :
     -x = ~~~ x + 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem neg_eq_neg_not_one :
     -x = ~~~ (x - 1) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_eq_neg_sub_one :
     ~~~ x = - x - 1:= by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem neg_not_eq_add_one :
     - ~~~ x = x + 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_neg_eq_sub_one :
     ~~~ (-x) = x - 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem add_eq_sub_not_sub_one :
     x + y = x - ~~~ y - 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem add_eq_xor_add_mul_and :
     x + y = (x ^^^ y) + 2 * (x &&& y) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem add_eq_or_add_and :
     x + y = (x ||| y) + (x &&& y) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem add_eq_mul_or_neg_xor :
     x + y = 2 * (x ||| y) - (x ^^^ y) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem sub_eq_add_not_add_one :
     x - y = x + ~~~ y + 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem sub_eq_xor_sub_mul_not_and :
     x - y = (x ^^^ y) - 2 * (~~~ x &&& y) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem sub_eq_and_not_sub_not_and :
     x - y = (x &&& ~~~ y) - (~~~ x &&& y) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem sub_eq_mul_and_not_sub_xor :
     x - y = 2 * (x &&& ~~~ y) - (x ^^^ y) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem xor_eq_or_sub_and :
     x ^^^ y = (x ||| y) - (x &&& y) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem and_not_eq_or_sub:
     x &&& ~~~ y = (x ||| y) - y := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem and_not_eq_sub_add :
     x &&& ~~~ y = x - (x &&& y) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_sub_eq_sub_sub_one :
     ~~~ (x - y) = y - x - 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_sub_eq_not_add :
     ~~~ (x - y) = ~~~x + y := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_xor_eq_and_sub_or_sub_one :
     ~~~ (x ^^^ y) = (x &&& y) - (x ||| y) - 1 := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem not_xor_eq_and_add_not_or :
     ~~~ (x ^^^ y) = (x &&& y) + ~~~ (x ||| y) := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem or_eq_and_not_add :
     x ||| y = (x &&& ~~~ y) + y := by
-  all_goals sorry
+  all_goals bv_compare'
 
 theorem and_eq_not_or_sub_not :
     x &&& y = (~~~ x ||| y) - ~~~ x := by
-  all_goals sorry
+  all_goals bv_compare'
 
 end AdditionCombinedWithLogicalOperations
 

artifact-evaluation/Dockerfile

@@ -6,27 +6,54 @@ WORKDIR /code
 RUN apt-get update -y \
     && DEBIAN_FRONTEND="noninteractive" apt-get install --yes \
         tzdata \
+	pip \
+	python3-venv \
         build-essential \
         cmake \
         git \
-        ripgrep \
-        vim \
-        neovim \
-        emacs \
         ninja-build \
-        gdb curl wget
+        gdb curl wget \
+        # dependencies for experiment scripts
+        python3-matplotlib python3-pandas python3-num2words \
+        # bitwuzla dependencies
+        meson libgmp-dev libcadical-dev libsymfpu-dev pkg-config
 
 # Install Lean
 RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > /code/elan.sh \
     && sh /code/elan.sh -y # elan
 ENV PATH /root/.elan/bin:$PATH
 ENV LIBRARY_PATH /root/.elan/lib:$LIBRARY_PATH
 
-# Download & build lean-mlir
-RUN curl -L https://github.com/opencompl/ssa/archive/refs/tags/v0.1.3.tar.gz > /code/ssa.tar.gz # SSA tar file
-RUN tar xf ssa.tar.gz && ls /code/ && mv ssa-0.1.3 ssa # untar
-WORKDIR /code/ssa
-RUN lake -R exe cache get
-RUN lake build SSA mlirnatural
+# Install Bitwuzla
+RUN git clone https://github.com/bitwuzla/bitwuzla
+WORKDIR /code/bitwuzla
+RUN ./configure.py && cd build && ninja install
 
-USER root
+# Install Lean-MLIR 
+RUN git clone https://github.com/opencompl/lean-mlir
+WORKDIR /code/lean-mlir
+
+# Install plotting script dependencies
+
+# WORKDIR /code/lean-mlir/bv-evaluation/
+# RUN bash -c "\
+# 	python3 -m venv venv \
+# 	&& source venv/bin/activate \
+# 	&& python3 -m pip install -r /code/lean-mlir/bv-evaluation/requirements.txt "
+
+# First, get cached dependencies
+WORKDIR /code/lean-mlir
+COPY . .
+
+# COPY lean-toolchain lakefile.toml lake-manifest.json ./
+# RUN lake exe cache get!
+
+# Then, copy & build lean-mlir
+RUN lake exe cache get
+RUN lake build
+
+# Set the evaluation script directory as working dir
+WORKDIR /code/lean-mlir/bv-evaluation/
+RUN python3 compare-leansat-vs-bitwuzla-hdel.py
+
+USER root

artifact-evaluation/README.md

@@ -7,5 +7,10 @@ $ docker login
 $ make docker-build-and-push
 ```
 
-#### Steps to use docker image
+#### Build docker image and extract results
 
+from folder lean-mlir: 
+- docker build -f artifact-evaluation/Dockerfile -t lean-image .
+- docker create --name temp-container lean-image
+- docker cp temp-container:/code/lean-mlir/bv-evaluation/raw-data ./docker-results
+- docker rm temp-container

artifact-evaluation/artifact.tex

@@ -116,10 +116,15 @@ \subsubsection{Software dependencies}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{Experiment workflow}
 
-Access the docker image \texttt{opencompl-ssa} from
-\url{https://zenodo.org/records/11519739}.
+Access the docker image \texttt{lean-mlir} from
+\textcolor{red}{Zenodo link}.
 
 \begin{minted}[fontsize=\scriptsize]{text}
+  from folder lean-mlir: 
+- docker build -f artifact-evaluation/Dockerfile -t lean-image .
+- docker create --name temp-container lean-image
+- docker cp temp-container:/code/lean-mlir/bv-evaluation/raw-data ./docker-results
+- docker rm temp-container
 $ docker load -i opencompl-ssa.tar
 $ docker run -it siddudruid/opencompl-ssa
 # | This clears the build cache,

bv-evaluation/Makefile

@@ -0,0 +1,17 @@
+
+DOCKER=podman
+DOCKER_IMAGE_TAG=opencompl/lean-mlir-bv-evaluate
+
+docker-image:
+	${DOCKER} build -f Dockerfile ../ -t "${DOCKER_IMAGE_TAG}"
+
+.PHONY: 
+
+*.py:   .PHONY  
+	./run-script.sh python3 $@
+
+clean:
+	docker rmi ${DOCKER_IMAGE_TAG}
+
+all: 
+	./run-script.sh ./run-tests.sh

bv-evaluation/collect-data-alive.py

@@ -4,7 +4,7 @@
 import os 
 import re
 
-paper_directory = 'for-paper/'
+paper_directory = ''
 benchmark_dir = "../SSA/Projects/InstCombine/"
 res_dir = "results/AliveSymbolic/"
 raw_data_dir = paper_directory + 'raw-data/AliveSymbolic/'
@@ -19,6 +19,16 @@
 "#fb9a99",
 "#e31a1c"]
 
+def clear_folder():
+    for file in os.listdir(RESULTS_DIR):
+        file_path = os.path.join(RESULTS_DIR, file)
+        try:
+            if os.path.isfile(file_path) or os.path.islink(file_path):
+                os.unlink(file_path)
+            elif os.path.isdir(file_path):
+                shutil.rmtree(file_path)
+        except Exception as e:
+            print('Failed to delete %s. Reason: %s' % (file_path, e))
 
 
 def parse_tacbenches(file_name, raw):

bv-evaluation/collect-data-hdel-symbolic.py

@@ -4,7 +4,7 @@
 import os 
 import re
 
-paper_directory = 'for-paper/'
+paper_directory = ''
 benchmark_dir = "../SSA/Projects/InstCombine/HackersDelight/"
 res_dir = "results/HackersDelightSymbolic/"
 raw_data_dir = paper_directory + 'raw-data/HackersDelightSymbolic/'

bv-evaluation/collect-data-hdel.py

@@ -3,7 +3,7 @@
 import pandas as pd
 import os 
 
-paper_directory = 'for-paper/'
+paper_directory = ''
 benchmark_dir = "../SSA/Projects/InstCombine/HackersDelight/"
 res_dir = "results/HackersDelight/"
 raw_data_dir = paper_directory + 'raw-data/HackersDelight/'
@@ -80,7 +80,9 @@
             while l:
                 if "Bitwuzla " in l: 
                     cegb = False
-                    if "counter" in l : 
+                    if "failed" in l : 
+                        print(l)
+                    elif "counter" in l : 
                         cegb = True
                         tot = float(l.split("after ")[1].split("ms")[0])
                         if r == 0:

bv-evaluation/collect-data-llvm-symbolic.py

@@ -4,7 +4,7 @@
 import os 
 import re
 
-paper_directory = 'for-paper/'
+paper_directory = ''
 benchmark_dir = "../SSA/Projects/InstCombine/tests/proofs/"
 res_dir = "results/InstCombineSymbolic/"
 raw_data_dir = paper_directory + 'raw-data/InstCombineSymbolic/'

bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py

@@ -74,4 +74,4 @@ def process(jobs: int):
 parser = argparse.ArgumentParser(prog='compare-leansat-vs-bitwuzla-llvm')
 parser.add_argument('-j', '--jobs', type=int, default=1)
 args = parser.parse_args()
-process(args.jobs)
+process(args.jobs)