Merge branch 'release/julien/ab-crown-docker' into 'master'

Adding alpha-beta-crown and fixing bugs in Docker

Closes #42

See merge request laiser/caisar!97

docker/Dockerfile.template

@@ -35,40 +35,26 @@ opam-2.1 update -y
 
 RUN sudo apt update  && \
     sudo apt install apt-utils wget && \
-    sudo apt install -yy git wget gfortran cmake protobuf-compiler libprotobuf-dev libboost-all-dev libopenblas-dev zip && \
+    sudo apt install -yy git wget gfortran cmake protobuf-compiler libprotobuf-dev libboost-all-dev libopenblas-dev zip python3.10-dev python3.10-venv && \
     sudo apt clean && \
     sudo rm -rf /var/lib/apt/lists/
 
 ENV PATH "/home/opam/.local/bin:$PATH"
 
-# Python Conda
-
-ENV SHACONDA "1564571a6a06a9999a75a6c65d63cb82911fc647e96ba5b729f904bf00c177d3"
-
-RUN wget https://repo.anaconda.com/miniconda/Miniconda3-py39_23.3.1-0-Linux-x86_64.sh -O ~/miniconda.sh
-
-RUN SHAFILE=$(sha256sum ~/miniconda.sh | awk '{print $1}') && if [ "$SHAFILE" != "$SHACONDA" ]; then echo "Mismatch between SHA256SUM of downloaded script and expected script, aborting installation."; echo "The expected SHA256SUM is $SHACONDA, but the SHA256SUM of downloaded script is $SHAFILE."; exit 1; fi
-
-RUN /bin/bash ~/miniconda.sh  -b && rm ~/miniconda.sh
-
-ENV PATH "/home/opam/miniconda3/bin:$PATH"
-
-RUN conda init bash && conda create -n python_caisar_env python=3.10.9
-
-SHELL ["conda", "run", "-n", "python_caisar_env", "/bin/bash", "-c"]
-
 # External provers
 
+RUN curl -sS https://bootstrap.pypa.io/get-pip.py | python3.10
+
 ## Pyrat
 
 RUN git clone https://git.frama-c.com/pub/pyrat.git && \
 git -C pyrat checkout 43c7389e5ce203b445ad3c7bfdcbf6bf408f3214
 
-RUN pip --default-timeout=1000 install -r pyrat/requirements.txt
+RUN /usr/bin/python3.10 -m pip --default-timeout=1000 install -r pyrat/requirements.txt
 
 ENV PATH "/home/opam/pyrat/:$PATH"
 
-RUN echo "#/usr/bin/sh\n exec /home/opam/miniconda3/envs/python_caisar_env/bin/python /home/opam/pyrat/pyrat.pyc \"\$@\"" > /home/opam/pyrat/pyrat
+RUN echo -e "#!/usr/bin/sh \n exec /usr/bin/python3.10 /home/opam/pyrat/pyrat.pyc \"\$@\"" > /home/opam/pyrat/pyrat
 RUN chmod u+x /home/opam/pyrat/pyrat
 
 RUN pyrat -h
@@ -90,7 +76,6 @@ cmake --build .
 
 ENV PATH "/home/opam/Marabou/build:$PATH"
 
-
 ## SAVer
 
 RUN git clone https://github.com/svm-abstract-verifier/saver.git && \
@@ -102,17 +87,34 @@ make install
 
 ENV PATH "/home/opam/saver/bin:$PATH"
 
-
 ## NNenum
 
 RUN git clone https://github.com/stanleybak/nnenum.git && \
 git -C nnenum checkout cf7c0e72c13543011a7ac3fbe0f5c59c3aafa77e
 
 RUN cd nnenum && \
-pip3 install -r requirements.txt
+/usr/bin/python3.10 -m pip install -r requirements.txt
 
 ENV PYTHONPATH "$PYTHONPATH:/home/opam/nnenum/src"
 
+## ABCrown
+
+RUN git clone https://github.com/Verified-Intelligence/alpha-beta-CROWN.git && \
+git -C alpha-beta-CROWN checkout 7b3d507caf40a5f42d99f6894373526c6fd615b7
+
+### From
+# https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/vnncomp_scripts/install_tool_general.sh,
+# and removing dependencies that are already in PyRAT
+# dependency set: pytorch, torchvision, torchaudio, tqdm,
+# pandas, protobuf, onnx, onnxruntime
+# DNNV and onnx2pytorch set on a specific commit
+# WARNING: Result in Pillow version and networkx version
+# different than what is expected by PyRAT and/or nnenum!
+
+RUN cd alpha-beta-CROWN && \
+/usr/bin/python3.10 -m pip install --no-input --no-cache-dir git+https://github.com/KaidiXu/onnx2pytorch.git@fe7281b9b6c8c28f61e72b8f3b0e3181067c7399 git+https://github.com/dlshriver/DNNV.git@6ab81fff8b83e5e7d5d964e409d092190368c8f1 pyyaml packaging appdirs sortedcontainers mkl==2019.0 pyyaml appdirs
+
+ENV PYTHONPATH "$PYTHONPATH:/home/opam/alpha-beta-CROWN/complete_verifier"
 
 # CAISAR
 

docker/Makefile

@@ -23,6 +23,7 @@
 .PHONY: pub push FORCE
 
 OCAML_VERSION?=4.13
+UBUNTU_VERSION?=22.04
 
 all: Dockerfile
 	@echo "You may want to consider adding ARGS=--no-cache to force"
@@ -33,8 +34,8 @@ push: all
 	@echo "You may need to execute 'docker login' beforehand."
 	docker push laiser/caisar:pub
 
-SHA_DOCKER=$(shell docker manifest inspect ocaml/opam:ubuntu-ocaml-$(OCAML_VERSION) | jq '.manifests| .[] | select(.platform.architecture == "amd64") | .digest' --raw-output)
-SHA_DOCKER:=$(or $(SHA_DOCKER),sha256:9d471148a7acdaba15caa139710f89ca8668a191c0052eb1c80cb9729e337c40)
+SHA_DOCKER=$(shell docker manifest inspect ocaml/opam:ubuntu-$(UBUNTU_VERSION)-ocaml-$(OCAML_VERSION) | jq '.manifests| .[] | select(.platform.architecture == "amd64") | .digest' --raw-output)
+SHA_DOCKER:=$(or $(SHA_DOCKER),sha256:e6529eedeeab653b03eae55b91a9491bc45be4717197d2f94a6615db939cfae6)
 
 CAISAR_COMMIT?=$(shell git rev-parse HEAD)