Allow z3-solver<=4.13.0.0, streamline Dockerfile (#1867)

.github/workflows/container.yml

@@ -0,0 +1,31 @@
+on:
+  pull_request:
+    paths:
+      - .github/workflows/container.yml
+      - Dockerfile
+      - docker_build_and_deploy.sh
+      - requirements.txt
+      - setup.py
+
+name: container
+
+concurrency:
+  # Concurrency group that uses the workflow name and PR number if available
+  # or commit SHA as a fallback. If a new build is triggered under that
+  # concurrency group while a previous build is running it will be canceled.
+  # Repeated pushes to a PR will cancel all previous builds, while multiple
+  # merges to a branch will not cancel.
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.sha }}
+  cancel-in-progress: true
+
+jobs:
+  test:
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+    steps:
+      - uses: actions/checkout@v4
+      - name: build and test
+        run: |
+          # when no DOCKERHUB_USERNAME is set, this only builds the
+          # container and runs the myth-smoke-test
+          ./docker_build_and_deploy.sh mythril/myth-dev

.pre-commit-config.yaml

@@ -19,6 +19,19 @@ repos:
     hooks:
     -   id: ruff
         args: [--fix, --show-fixes]
+-   repo: https://github.com/scop/pre-commit-shfmt
+    rev: v3.8.0-1
+    hooks:
+    -   id: shfmt
+        args: [--write, --indent, '4']
+-   repo: https://github.com/shellcheck-py/shellcheck-py
+    rev: v0.10.0.1
+    hooks:
+    -   id: shellcheck
+-   repo: https://github.com/hadolint/hadolint
+    rev: v2.12.0
+    hooks:
+    -   id: hadolint-docker
 -   repo: https://github.com/macisamuele/language-formatters-pre-commit-hooks
     rev: v2.14.0
     hooks:

Dockerfile

@@ -3,7 +3,7 @@ ARG PYTHON_VERSION=3.10
 ARG INSTALLED_SOLC_VERSIONS
 
 
-FROM python:${PYTHON_VERSION:?} AS python-wheel
+FROM python:${PYTHON_VERSION} AS python-wheel
 WORKDIR /wheels
 
 
@@ -13,75 +13,36 @@ FROM python-wheel AS python-wheel-with-cargo
 # https://github.com/rust-lang/cargo/issues/10781#issuecomment-1163819998
 ENV CARGO_UNSTABLE_SPARSE_REGISTRY=true
 
+SHELL ["/bin/bash", "-euo", "pipefail", "-c"]
 RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
 ENV PATH=/root/.cargo/bin:$PATH
 
 
-# z3-solver needs to build from src on arm, and it takes a long time, so
-# building it in a separate stage helps parallelise the build and helps it stay
-# in the build cache.
-FROM python-wheel AS python-wheel-z3-solver
-RUN pip install auditwheel
-RUN --mount=source=requirements.txt,target=/run/requirements.txt \
-  pip wheel "$(grep z3-solver /run/requirements.txt)"
-# The wheel z3-solver builds does not install in arm64 because it generates
-# incorrect platform compatibility metadata for arm64 builds. (It uses the
-# platform manylinux1_aarch64 but manylinux1 is only defined for x86 systems,
-# not arm: https://peps.python.org/pep-0600/#legacy-manylinux-tags). To work
-# around this, we use pypa's auditwheel tool to infer and apply a compatible
-# platform tag.
-RUN ( auditwheel addtag ./z3_solver-* \
-      # replace incorrect wheel with the re-tagged one
-      && rm ./z3_solver-* && mv wheelhouse/z3_solver-* . ) \
-    # addtag exits with status 1 if no tags need adding, which is fine
-    || true
-
-
-FROM python-wheel-with-cargo AS python-wheel-blake2b
-# blake2b-py doesn't publish ARM builds, and also don't publish source packages
-# on PyPI (other than the old 0.1.3 version) so we need to build from a git
-# tag. They do publish binaries for linux amd64, but their binaries only support
-# certain platform versions and the amd64 python image isn't supported, so we
-# have to build from src for that as well.
-
-# Try to get a binary build or a source release on PyPI first, then fall back
-# to building from the git repo.
-RUN pip wheel 'blake2b-py>=0.2.0,<1' \
-  || pip wheel git+https://github.com/ethereum/[email protected]
-
-
-FROM python-wheel AS mythril-wheels
-# cython is needed to build some wheels, such as cytoolz
-RUN pip install cython
+FROM python-wheel-with-cargo AS mythril-wheels
 RUN --mount=source=requirements.txt,target=/run/requirements.txt \
-  # ignore blake2b and z3-solver as we've already built them
-  grep -v -e blake2b -e z3-solver /run/requirements.txt > /tmp/requirements-remaining.txt
-RUN pip wheel -r /tmp/requirements-remaining.txt
+  pip wheel -r /run/requirements.txt
 
 COPY . /mythril
 RUN pip wheel --no-deps /mythril
 
-COPY --from=python-wheel-blake2b /wheels/blake2b* /wheels
-COPY --from=python-wheel-z3-solver /wheels/z3_solver* /wheels
-
 
 # Solidity Compiler Version Manager. This provides cross-platform solc builds.
 # It's used by foundry to provide solc. https://github.com/roynalnaruto/svm-rs
 FROM python-wheel-with-cargo AS solidity-compiler-version-manager
 RUN cargo install svm-rs
 # put the binaries somewhere obvious for later stages to use
-RUN mkdir -p /svm-rs/bin && cd ~/.cargo/bin/ && cp svm solc /svm-rs/bin/
+RUN mkdir -p /svm-rs/bin && cp ~/.cargo/bin/svm ~/.cargo/bin/solc /svm-rs/bin/
 
 
-FROM python:${PYTHON_VERSION:?}-slim AS myth
+FROM python:${PYTHON_VERSION}-slim AS myth
 ARG PYTHON_VERSION
 # Space-separated version string without leading 'v' (e.g. "0.4.21 0.4.22")
 ARG INSTALLED_SOLC_VERSIONS
 
 COPY --from=solidity-compiler-version-manager /svm-rs/bin/* /usr/local/bin/
 
 RUN --mount=from=mythril-wheels,source=/wheels,target=/wheels \
-  export PYTHONDONTWRITEBYTECODE=1 && pip install /wheels/*.whl
+  export PYTHONDONTWRITEBYTECODE=1 && pip install --no-cache-dir /wheels/*.whl
 
 RUN adduser --disabled-password mythril
 USER mythril
@@ -142,5 +103,5 @@ RUN --mount=source=./solidity_examples,target=/solidity_examples \
   /smoke-test.sh 2>&1 | tee smoke-test.log
 
 
-FROM scratch as myth-smoke-test
+FROM scratch AS myth-smoke-test
 COPY --from=myth-smoke-test-execution /smoke-test/* /

all_tests.sh

@@ -1,4 +1,6 @@
-#!/bin/sh
+#!/bin/bash
+
+set -euo pipefail
 
 echo -n "Checking Python version... "
 python -c 'import sys
@@ -7,7 +9,6 @@ assert sys.version_info[0:2] >= (3,5), \
 """Please make sure you are using Python 3.5 or later.
 You ran with {}""".format(sys.version)' || exit $?
 
-
 rm -rf ./tests/testdata/outputs_current/
 mkdir -p ./tests/testdata/outputs_current/
 rm -rf ./tests/testdata/outputs_current_laser_result/

docker/docker-entrypoint.sh

@@ -13,7 +13,7 @@ sync-svm-solc-versions-with-solcx
 # By default we run myth with options from arguments we received. But if the
 # first argument is a valid program, we execute that instead so that people can
 # run other commands without overriding the entrypoint (e.g. bash).
-if command -v "${1:-}" > /dev/null; then
+if command -v "${1:-}" >/dev/null; then
     exec -- "$@"
 fi
 exec -- myth "$@"

docker_build_and_deploy.sh

@@ -4,17 +4,15 @@ set -eo pipefail
 
 NAME=$1
 
-if [[ ! $NAME =~ ^mythril/myth(-dev)?$ ]];
-then
-  echo "Error: unknown image name: $NAME" >&2
-  exit 1
+if [[ ! $NAME =~ ^mythril/myth(-dev)?$ ]]; then
+    echo "Error: unknown image name: $NAME" >&2
+    exit 1
 fi
 
-if [ ! -z $CIRCLE_TAG ];
-then
-  GIT_VERSION=${CIRCLE_TAG#?}
+if [ -n "$CIRCLE_TAG" ]; then
+    GIT_VERSION=${CIRCLE_TAG#?}
 else
-  GIT_VERSION=${CIRCLE_SHA1}
+    GIT_VERSION=${CIRCLE_SHA1}
 fi
 
 export DOCKER_BUILDKIT=1
@@ -24,7 +22,12 @@ docker buildx create --use
 # so the next build should be almost instant.)
 docker buildx bake myth-smoke-test
 
-echo "$DOCKERHUB_PASSWORD" | docker login -u $DOCKERHUB_USERNAME --password-stdin
+if [ -z "$DOCKERHUB_USERNAME" ]; then
+    echo "Finishing without pushing to dockerhub"
+    exit 0
+fi
+
+echo "$DOCKERHUB_PASSWORD" | docker login -u "$DOCKERHUB_USERNAME" --password-stdin
 
 # strip mythril/ from NAME, e.g. myth or myth-dev
 BAKE_TARGET="${NAME#mythril/}"

requirements.txt

@@ -1,4 +1,4 @@
-blake2b-py
+blake2b-py>=0.2.0,<1
 coloredlogs>=10.0
 coincurve>=13.0.0
 cytoolz>=0.12.0
@@ -22,6 +22,6 @@ pyparsing<3,>=2.0.2
 requests
 rlp<4,>=3
 semantic_version
-z3-solver<=4.12.5.0,>=4.8.8.0
+z3-solver<=4.13.0.0,>=4.8.8.0
 matplotlib
 certifi>=2020.06.20