From 7125f427c9fe9c7211859630eb542002eddf2738 Mon Sep 17 00:00:00 2001 From: Bryan Tan Date: Sat, 3 Sep 2022 13:42:25 -0700 Subject: [PATCH 1/2] Simplify docker image build and add entrypoint script --- Dockerfile | 7 +- resources/Dockerfile@base | 141 +++++++++++---------------------- resources/docker_entrypoint.sh | 27 +++++++ 3 files changed, 76 insertions(+), 99 deletions(-) create mode 100644 resources/docker_entrypoint.sh diff --git a/Dockerfile b/Dockerfile index 449bdd1..807901a 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,6 +1,7 @@ -FROM chyanju/picus:base +FROM veridise/picus:base -# copy current version of Eurus +# copy current version of Picus COPY ./ /Picus/ -CMD [ "/bin/bash" ] \ No newline at end of file +WORKDIR /Picus/ +CMD [ "/bin/bash" ] diff --git a/resources/Dockerfile@base b/resources/Dockerfile@base index 92c5a87..a8d7f91 100644 --- a/resources/Dockerfile@base +++ b/resources/Dockerfile@base @@ -1,75 +1,36 @@ -FROM ubuntu:20.04 +FROM ubuntu:22.04 ENV LANG=C.UTF-8 LC_ALL=C.UTF-8 ENV PATH /opt/conda/bin:$PATH SHELL ["/bin/bash", "-c"] -# anaconda -# hadolint ignore=DL3008 +# Basic dependencies, antlr4, and C++ build tools +# libpoly: libgmp-dev +# racket: openssh-client RUN set -x && \ apt-get update --fix-missing && \ apt-get install -y --no-install-recommends \ bzip2 \ ca-certificates \ - git \ - libglib2.0-0 \ - libsm6 \ - libxcomposite1 \ - libxcursor1 \ - libxdamage1 \ - libxext6 \ - libxfixes3 \ - libxi6 \ - libxinerama1 \ - libxrandr2 \ - libxrender1 \ - mercurial \ openssh-client \ - procps \ - subversion \ + git \ wget \ - && apt-get clean \ - && rm -rf /var/lib/apt/lists/* && \ - UNAME_M="$(uname -m)" && \ - if [ "${UNAME_M}" = "x86_64" ]; then \ - ANACONDA_URL="https://repo.anaconda.com/archive/Anaconda3-2021.11-Linux-x86_64.sh"; \ - SHA256SUM="fedf9e340039557f7b5e8a8a86affa9d299f5e9820144bd7b92ae9f7ee08ac60"; \ - elif [ "${UNAME_M}" = "s390x" ]; then \ - ANACONDA_URL="https://repo.anaconda.com/archive/Anaconda3-2021.11-Linux-s390x.sh"; \ - SHA256SUM="1504e9259816c5804eff1304fe7e339517b9fc1a08bfd991bc525a7efb6568f1"; \ - elif [ "${UNAME_M}" = "aarch64" ]; then \ - ANACONDA_URL="https://repo.anaconda.com/archive/Anaconda3-2021.11-Linux-aarch64.sh"; \ - SHA256SUM="4daacb88fbd3a6c14e28cd3b37004ed4c2643e2b187302e927eb81a074e837bc"; \ - elif [ "${UNAME_M}" = "ppc64le" ]; then \ - ANACONDA_URL="https://repo.anaconda.com/archive/Anaconda3-2021.11-Linux-ppc64le.sh"; \ - SHA256SUM="7eb6a95925ee756240818599f8dcbba7a155adfb05ef6cd5336aa3c083de65f3"; \ - fi && \ - wget "${ANACONDA_URL}" -O anaconda.sh -q && \ - echo "${SHA256SUM} anaconda.sh" > shasum && \ - sha256sum --check --status shasum && \ - /bin/bash anaconda.sh -b -p /opt/conda && \ - rm anaconda.sh shasum && \ - ln -s /opt/conda/etc/profile.d/conda.sh /etc/profile.d/conda.sh && \ - echo ". /opt/conda/etc/profile.d/conda.sh" >> ~/.bashrc && \ - echo "conda activate base" >> ~/.bashrc && \ - find /opt/conda/ -follow -type f -name '*.a' -delete && \ - find /opt/conda/ -follow -type f -name '*.js.map' -delete && \ - /opt/conda/bin/conda clean -afy - -# Antlr -RUN apt-get update && \ - apt-get install -y build-essential && \ - apt-get install -y antlr4 && \ - apt-get install -y zip unzip + build-essential \ + zip unzip \ + python3-dev python3-pip \ + gcc make cmake ninja-build \ + antlr4 \ + libgmp-dev \ + software-properties-common gpg-agent # racket and rosette and other racket packages ARG DEBIAN_FRONTEND=noninteractive -RUN apt-get update && \ - apt-get install -y software-properties-common && \ - add-apt-repository -y ppa:plt/racket && \ +RUN add-apt-repository -y ppa:plt/racket && \ apt-get update && \ - apt-get install -y racket && \ - raco pkg install --auto rosette + apt-get install -y racket libssl-dev curl && \ + raco pkg install --auto rosette && \ + apt-get clean && \ + rm -rf /var/lib/apt/lists/* # build rust & circom 2.0.7 RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y && \ @@ -79,57 +40,45 @@ RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y && \ git checkout v2.0.7 && \ cargo build --release && \ cargo install --path circom && \ - cd .. + cd .. && rm -rf circom/ # install z3 RUN wget https://github.com/Z3Prover/z3/releases/download/z3-4.11.0/z3-4.11.0-x64-glibc-2.31.zip && \ unzip z3-4.11.0-x64-glibc-2.31.zip && \ - cp z3-4.11.0-x64-glibc-2.31/bin/z3 /bin/ - -# install CoCoALib -RUN apt-get update && \ - apt-get install -y libgmp-dev && \ - wget https://cocoa.dima.unige.it/cocoa/cocoalib/tgz/CoCoALib-0.99800.tgz && \ - tar -xvzf CoCoALib-0.99800.tgz && \ - cd CoCoALib-0.99800/ && \ - ./configure && \ - make && \ - cd .. - - -# re-compile CoCoALib with patch from cvc5-ff -RUN apt-get update && \ - apt-get install -y cmake && \ - git clone https://github.com/alex-ozdemir/CVC4.git && \ - cd ./CVC4/ && \ - git checkout ddcecc5 && \ - ./configure.sh --cocoa --auto-download && \ - cd .. && \ - cp ./CVC4/cmake/deps-utils/CoCoALib-0.99800-trace.patch ./ && \ - mv ./CoCoALib-0.99800 ./a && \ - patch -s -p0 < CoCoALib-0.99800-trace.patch && \ - mv ./a ./CoCoALib-0.99800 && \ - cd CoCoALib-0.99800/ && \ - ./configure && \ - make && \ - cd .. + cp z3-4.11.0-x64-glibc-2.31/bin/z3 /bin/ && \ + rm -r z3-4.11.0-x64-glibc-2.31/ # install libpoly -RUN apt-get update && \ - apt-get install gcc cmake make libgmp-dev && \ - git clone https://github.com/SRI-CSL/libpoly.git && \ +RUN git clone https://github.com/SRI-CSL/libpoly.git && \ cd ./libpoly/ && \ cd ./build/ && \ - cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/usr/local && \ + cmake .. -GNinja -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/usr/local && \ + cmake --build . && \ + cmake --install . && \ + cd ../../ && rm -r ./libpoly + +# fetch cvc5-ff +RUN pip install toml && \ + git clone https://github.com/alex-ozdemir/CVC4.git -b ff --single-branch && \ + cd ./CVC4 && \ + git checkout ddcecc5 + +# compile and install CoCoALib with patch from cvc5-ff +RUN wget https://cocoa.dima.unige.it/cocoa/cocoalib/tgz/CoCoALib-0.99800.tgz && \ + tar -xvzf CoCoALib-0.99800.tgz &&\ + patch -s -p1 -d ./CoCoALib-0.99800 < ./CVC4/cmake/deps-utils/CoCoALib-0.99800-trace.patch && \ + cd CoCoALib-0.99800/ && \ + ./configure && \ make && \ make install && \ - cd ../../ + cd .. && rm -r ./CoCoALib-0.99800 -# actually install cvc5-ff +# compile and install cvc5-ff RUN cd ./CVC4/ && \ - ./configure.sh --cocoa --auto-download && \ + ./configure.sh --cocoa --auto-download --ninja && \ cd ./build/ && \ - make -j4 install && \ - cd .. + cmake --build . && \ + cmake --install . && \ + cd ../.. && rm -r ./CVC4 -CMD [ "/bin/bash" ] \ No newline at end of file +CMD [ "/bin/bash" ] diff --git a/resources/docker_entrypoint.sh b/resources/docker_entrypoint.sh new file mode 100644 index 0000000..1cd4ce5 --- /dev/null +++ b/resources/docker_entrypoint.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash + +set -e + +CIRCOM_SRC_DIR=${CIRCOM_SRC_DIR:-/src_files} +CIRCOM_OUT_DIR=${CIRCOM_OUT_DIR:-/artifact_dir} + +mkdir -p "$CIRCOM_OUT_DIR" + +# Run circom compiler +echo "Running circom compiler..." +for f in "$CIRCOM_SRC_DIR"/*.circom; do + echo "Compile: $f" + circom -o "${CIRCOM_OUT_DIR}" "$f" --r1cs --sym --O0 +done +echo "Done compiling." +echo + +# Run uniqueness tests on r1cs files +echo "Running picus..." +for f in "$CIRCOM_OUT_DIR"/*.r1cs; do + echo "--------------------------------------------------------" + echo "Running picus on: $f" + racket test-pp-uniqueness.rkt --r1cs "$f" --solver cvc5 --weak + echo "--------------------------------------------------------" + echo +done From 32de137676579adbf21c71d328947f58bbce92f0 Mon Sep 17 00:00:00 2001 From: Bryan Tan Date: Tue, 6 Sep 2022 15:40:36 -0700 Subject: [PATCH 2/2] Add docker_entrypoint.sh variables to make running easier --- resources/docker_entrypoint.sh | 34 ++++++++++++++++++++++++++-------- 1 file changed, 26 insertions(+), 8 deletions(-) diff --git a/resources/docker_entrypoint.sh b/resources/docker_entrypoint.sh index 1cd4ce5..9e6c17f 100644 --- a/resources/docker_entrypoint.sh +++ b/resources/docker_entrypoint.sh @@ -1,27 +1,45 @@ #!/usr/bin/env bash -set -e +# Script used for invoking Picus from Docker. +# Instructions: set the following environment variables before calling this +# script, then run this script with no arguments. -CIRCOM_SRC_DIR=${CIRCOM_SRC_DIR:-/src_files} -CIRCOM_OUT_DIR=${CIRCOM_OUT_DIR:-/artifact_dir} +# The folder containing all source files, including libraries. +CIRCOM_SRC_DIR="${CIRCOM_SRC_DIR:-/src_files}" + +# A colon-separated list of folders/files in CIRCOM_SRC_DIR that Picus should +# be run on. +MAIN_FILES="${MAIN_FILES:-${CIRCOM_SRC_DIR}}" + +# The folder where the circom output and picus logs should be stored. +CIRCOM_OUT_DIR="${CIRCOM_OUT_DIR:-/artifact_dir}" + +set -e mkdir -p "$CIRCOM_OUT_DIR" # Run circom compiler echo "Running circom compiler..." -for f in "$CIRCOM_SRC_DIR"/*.circom; do - echo "Compile: $f" - circom -o "${CIRCOM_OUT_DIR}" "$f" --r1cs --sym --O0 +for main_loc in $(xargs -n1 -d: <<< "$MAIN_FILES"); do + for f in $(find "$main_loc" -type f -name '*.circom'); do + echo "Compile: $f" + out_dir=$(dirname $(realpath --relative-to="$CIRCOM_SRC_DIR" "$f")) + mkdir -p "${CIRCOM_OUT_DIR}"/"$out_dir" + circom -o "${CIRCOM_OUT_DIR}"/"$out_dir" "$f" --r1cs --sym --O0 + done done echo "Done compiling." echo # Run uniqueness tests on r1cs files echo "Running picus..." -for f in "$CIRCOM_OUT_DIR"/*.r1cs; do +for f in $(find "$CIRCOM_OUT_DIR" -type f -name '*.r1cs'); do echo "--------------------------------------------------------" echo "Running picus on: $f" - racket test-pp-uniqueness.rkt --r1cs "$f" --solver cvc5 --weak + fdir=$(dirname "$f") + logfile="$fdir"/"$(basename "$f")".picus.log + racket test-pp-uniqueness.rkt --r1cs "$f" --solver cvc5 --weak |& tee "$logfile" + echo "Log saved to $logfile" echo "--------------------------------------------------------" echo done