From 7e0f6fb87d0117a26530c6c00af78384c772cb39 Mon Sep 17 00:00:00 2001
From: Roland Heusser <skofgar@gmail.com>
Date: Tue, 28 Jul 2020 09:44:42 -0700
Subject: [PATCH] adding Dockerfile to build from local source and extend
 README

---
 docker/Dockerfile-solcverify-local.src | 53 +++++++++++++++++++++++
 docker/README.md                       | 58 +++++++++++++++++++++++++-
 2 files changed, 110 insertions(+), 1 deletion(-)
 create mode 100644 docker/Dockerfile-solcverify-local.src

diff --git a/docker/Dockerfile-solcverify-local.src b/docker/Dockerfile-solcverify-local.src
new file mode 100644
index 000000000000..be3605db7028
--- /dev/null
+++ b/docker/Dockerfile-solcverify-local.src
@@ -0,0 +1,53 @@
+FROM ubuntu:focal
+
+# Generic packages
+RUN apt update && DEBIAN_FRONTEND="noninteractive" apt install -y \
+  cmake \
+  curl \
+  git \
+  libboost-filesystem-dev \
+  libboost-program-options-dev \
+  libboost-system-dev \
+  libboost-test-dev \
+  python3-pip \
+  software-properties-common \
+  unzip \
+  wget
+
+# Python dependencies
+RUN pip3 install psutil
+
+# CVC4
+RUN curl --silent "https://api.github.com/repos/CVC4/CVC4/releases/latest" | grep browser_download_url | grep -E 'linux' | cut -d '"' -f 4 | wget -qi - -O /usr/local/bin/cvc4 \
+  && chmod a+x /usr/local/bin/cvc4
+
+# Z3
+RUN curl --silent "https://api.github.com/repos/Z3Prover/z3/releases/latest" | grep browser_download_url | grep -E 'ubuntu' | cut -d '"' -f 4 | wget -qi - -O z3.zip \
+  && unzip -p z3.zip '*bin/z3' > /usr/local/bin/z3 \
+  && chmod a+x /usr/local/bin/z3
+
+# Get .NET
+RUN wget https://packages.microsoft.com/config/ubuntu/20.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb \
+  && dpkg -i packages-microsoft-prod.deb \
+  && apt update \
+  && apt install -y apt-transport-https \
+  && apt update \
+  && apt install -y dotnet-sdk-3.1
+
+# Get boogie
+RUN dotnet tool install --global boogie
+ENV PATH="${PATH}:/root/.dotnet/tools"
+
+# Copy solidity sourcecode, instead of cloning it
+RUN mkdir solidity
+COPY . solidity
+
+RUN cd solidity \
+        && mkdir -p build \
+        && cd build \
+        && cmake -DUSE_Z3=Off -DUSE_CVC4=Off .. \
+        && make \
+        && make install
+
+# Set entrypoint
+ENTRYPOINT ["solc-verify.py"]
diff --git a/docker/README.md b/docker/README.md
index 86207983084b..52f5ed95f8c9 100644
--- a/docker/README.md
+++ b/docker/README.md
@@ -2,14 +2,70 @@
 
 This Dockerfile allows to quickly try solc-verify using [Docker](https://docs.docker.com/).
 
-The Dockerfile can be built with the following command:
+The Dockerfile can be built with one of the following commands:
+
+## Build from Open Source
+
+The following Dockerfile will clone the latest solitidy version from GitHub. This is useful if you only have the solc-verify Dockerfile, but not the sourcecode itself.
+
 ```
 docker build -t solc-verify -f Dockerfile-solcverify.src .
 ```
 
+## Build locally
+
+Building locally is useful, if you are working on a local copy of solc-verify or in a CI pipeline.
+
+```
+# go back to solidity root folder
+cd ..
+
+# build docker image
+docker build -t solc-verify -f docker/Dockerfile-solcverify-local.src .
+```
+
+# Verify Contracts
+
+## Use `runsv.sh` script
+
 The included `runsv.sh` script can be used run the containerized solc-verify on programs residing on the host:
 ```
 ./runsv.sh Contract.sol [FLAGS]
 ```
 
+> Example: `./runsv.sh ../test/solc-verify/examples/Annotations.sol`
+
+## Directly use docker commands to verify contracts
+
+### Validate sample contract
+
+Verify that the docker image is functioning correctly by validating one of the built in contracts. The following command instantiates the SOLC-Verify image, verifies a contract and then shuts down again:
+
+```bash
+PATH_TO_SAMPLE_CONTRACT=/solidity/test/solc-verify/examples/Annotations.sol
+docker run --rm solc-verify:latest $PATH_TO_SAMPLE_CONTRACT
+```
+
+The command should return following messages:
+
+```
+C::add: OK
+C::[implicit_constructor]: OK
+C::[receive_ether_selfdestruct]: OK
+Use --show-warnings to see 1 warning.
+No errors found.
+```
+
+### Validate your contracts
+
+To validate your own contracts place them in a directory that can be mounted into a running container of SOLC-Verify. All you need is the absolute path to the location, where the contracts are located. The following command will mount the contracts located in `$PATH_TO_CONTRACTS` into a running docker container of SOLC-verify and will then validate the contract with the name `$CONTRACT_NAME`.
+
+
+```bash
+PATH_TO_CONTRACTS= # path where the contracts are located on the machine running the docker image
+CONTRACT_NAME= # name of the contract to be validated
+
+docker run --rm -v $PATH_TO_CONTRACTS:/contracts solc-verify:latest /contracts/$CONTRACT_NAME
+```
+
 For more information on running solc-verify and examples, see [SOLC-VERIFY-README.md](../SOLC-VERIFY-README.md).