Merge pull request #5 from Veridise/main

sync changes from veridise
2026-05-11 03:00:06 -04:00 · 2022-09-08 17:29:34 -07:00
parent bd348e6414 be7e84d933
commit 19650d7459
3 changed files with 94 additions and 99 deletions
--- a/7
+++ b/7
@@ -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" ]
+WORKDIR /Picus/
+CMD [ "/bin/bash" ]
--- 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" ]
+CMD [ "/bin/bash" ]
--- a/resources/docker_entrypoint.sh
+++ b/resources/docker_entrypoint.sh
@@ -0,0 +1,45 @@
+#!/usr/bin/env bash
+
+# Script used for invoking Picus from Docker.
+# Instructions: set the following environment variables before calling this
+# script, then run this script with no arguments.
+
+# 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 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 $(find "$CIRCOM_OUT_DIR" -type f -name '*.r1cs'); do
+    echo "--------------------------------------------------------"
+    echo "Running picus on: $f"
+    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