diff --git a/.devcontainer/postCreate.sh b/.devcontainer/postCreate.sh index 85a31ea86..0e4252fc2 100644 --- a/.devcontainer/postCreate.sh +++ b/.devcontainer/postCreate.sh @@ -14,4 +14,4 @@ curl -L https://foundry.paradigm.xyz | bash echo 'source .venv/bin/activate' >> ~/.bashrc # just a test -# pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-v -st --storage-layout solidity --solver-timeout-assertion 0" +# pytest -v -k "not long and not ffi" --ignore=tests/lib --dolmos-options="-v -st --storage-layout solidity --solver-timeout-assertion 0" diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 000000000..8d8067ed1 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,3 @@ +# the file cheatcode tests (tests/regression/test/File.t.sol) hash these fixtures byte for byte: +# never convert their line endings (core.autocrlf is on by default on the Windows runners) +tests/regression/test/data/** -text diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md index 58b11868d..8343d9a2d 100644 --- a/.github/ISSUE_TEMPLATE/bug_report.md +++ b/.github/ISSUE_TEMPLATE/bug_report.md @@ -16,7 +16,7 @@ Please provide a reproducible example. **Environment:** - OS: [e.g., Linux / Windows / macOS] - Python version: [e.g., `python --version`] - - Halmos and other dependency versions: [e.g., `pip list`] + - dolmos and other dependency versions: [e.g., `pip list`] **Additional context** Add any other context about the problem here. diff --git a/.github/workflows/copilot-setup-steps.yml b/.github/workflows/copilot-setup-steps.yml index ad7e4d580..2d77655aa 100644 --- a/.github/workflows/copilot-setup-steps.yml +++ b/.github/workflows/copilot-setup-steps.yml @@ -15,10 +15,10 @@ jobs: steps: - name: Checkout code - uses: actions/checkout@v4 + uses: actions/checkout@v6 - name: Set up Python - uses: actions/setup-python@v4 + uses: actions/setup-python@v6 with: # let's use the oldest version of python that is supported by the project python-version: "3.11" @@ -27,9 +27,9 @@ jobs: uses: foundry-rs/foundry-toolchain@v1 - name: Install uv - uses: astral-sh/setup-uv@v4 + uses: astral-sh/setup-uv@v7 with: version: "0.5.21" - - name: Install halmos and its dependencies + - name: Install dolmos and its dependencies run: uv sync --extra dev diff --git a/.github/workflows/pre-commit.yml b/.github/workflows/pre-commit.yml index 027d087d4..1cb0eec15 100644 --- a/.github/workflows/pre-commit.yml +++ b/.github/workflows/pre-commit.yml @@ -6,6 +6,15 @@ jobs: pre-commit: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 - - uses: actions/setup-python@v5 - - uses: pre-commit/action@v3.0.1 + - uses: actions/checkout@v6 + - uses: actions/setup-python@v6 + with: + python-version: "3.12" + # pre-commit/action@v3.0.1 still uses actions/cache@v4 (node20) internally: + # run pre-commit directly, with a node24 cache + - uses: actions/cache@v5 + with: + path: ~/.cache/pre-commit + key: pre-commit-${{ hashFiles('.pre-commit-config.yaml') }} + - run: pip install pre-commit + - run: pre-commit run --show-diff-on-failure --color=always --all-files diff --git a/.github/workflows/publish-halmos-builder-package.yml b/.github/workflows/publish-dolmos-builder-package.yml similarity index 83% rename from .github/workflows/publish-halmos-builder-package.yml rename to .github/workflows/publish-dolmos-builder-package.yml index 60a6a494c..000d2b18c 100644 --- a/.github/workflows/publish-halmos-builder-package.yml +++ b/.github/workflows/publish-dolmos-builder-package.yml @@ -1,8 +1,8 @@ # based on https://docs.github.com/en/packages/managing-github-packages-using-github-actions-workflows/publishing-and-installing-a-package-with-github-actions#upgrading-a-workflow-that-accesses-a-registry-using-a-personal-access-token -name: Push halmos-builder package +name: Push dolmos-builder package on: - # only trigger manually, this is independent from halmos releases + # only trigger manually, this is independent from dolmos releases workflow_dispatch: workflow_run: workflows: ["Push solvers package"] @@ -10,11 +10,11 @@ on: - completed push: paths: - - packages/halmos-builder/**/* - - .github/workflows/publish-halmos-builder-package.yml + - packages/dolmos-builder/**/* + - .github/workflows/publish-dolmos-builder-package.yml env: - IMAGE_NAME: halmos-builder + IMAGE_NAME: dolmos-builder jobs: # This pushes the image to GitHub Packages. @@ -28,18 +28,18 @@ jobs: steps: - name: Login to GitHub Container Registry - uses: docker/login-action@v3 + uses: docker/login-action@v4 with: registry: ghcr.io username: ${{ github.actor }} password: ${{ secrets.GITHUB_TOKEN }} - - uses: actions/checkout@v4 + - uses: actions/checkout@v6 with: submodules: false - name: Build image - run: docker build . --file packages/halmos-builder/Dockerfile --tag $IMAGE_NAME --label "runnumber=${GITHUB_RUN_ID}" + run: docker build . --file packages/dolmos-builder/Dockerfile --tag $IMAGE_NAME --label "runnumber=${GITHUB_RUN_ID}" - name: Push image run: | diff --git a/.github/workflows/publish-halmos-package.yml b/.github/workflows/publish-dolmos-package.yml similarity index 58% rename from .github/workflows/publish-halmos-package.yml rename to .github/workflows/publish-dolmos-package.yml index abbef3993..6e2525a6b 100644 --- a/.github/workflows/publish-halmos-package.yml +++ b/.github/workflows/publish-dolmos-package.yml @@ -1,22 +1,22 @@ # based on https://docs.github.com/en/packages/managing-github-packages-using-github-actions-workflows/publishing-and-installing-a-package-with-github-actions#upgrading-a-workflow-that-accesses-a-registry-using-a-personal-access-token -name: Push halmos package +name: Push dolmos package on: workflow_dispatch: workflow_run: - workflows: ["Push halmos-builder package"] + workflows: ["Push dolmos-builder package"] types: - completed push: paths: - - packages/halmos/**/* - - .github/workflows/publish-halmos-package.yml + - packages/dolmos/**/* + - .github/workflows/publish-dolmos-package.yml tags: # push when we release a new tagged version - 'v*' env: - IMAGE_NAME: halmos + IMAGE_NAME: dolmos jobs: # This pushes the image to GitHub Packages. @@ -30,22 +30,22 @@ jobs: steps: - name: Login to GitHub Container Registry - uses: docker/login-action@v3 + uses: docker/login-action@v4 with: registry: ghcr.io username: ${{ github.actor }} password: ${{ secrets.GITHUB_TOKEN }} - - uses: actions/checkout@v4 + - uses: actions/checkout@v6 with: # we may need tests/lib for the workflows using this image submodules: recursive - name: Build image - run: docker build . --file packages/halmos/Dockerfile --tag $IMAGE_NAME --label "runnumber=${GITHUB_RUN_ID}" + run: docker build . --file packages/dolmos/Dockerfile --tag $IMAGE_NAME --label "runnumber=${GITHUB_RUN_ID}" - - name: Print halmos version - run: docker run $IMAGE_NAME halmos --version + - name: Print dolmos version + run: docker run $IMAGE_NAME dolmos --version - name: Push image run: | @@ -54,15 +54,17 @@ jobs: # This changes all uppercase characters to lowercase. IMAGE_ID=$(echo $IMAGE_ID | tr '[A-Z]' '[a-z]') - # This strips the git ref prefix from the version. - VERSION=$(echo "${{ github.ref }}" | sed -e 's,.*/\(.*\),\1,') + if [[ "${{ github.ref }}" == refs/tags/v* ]]; then + # release: X.Y.Z, X.Y and latest + VERSION="${GITHUB_REF_NAME#v}" + TAGS="$VERSION ${VERSION%.*} latest" + else + # anything else (main, builder rebuilds): a moving `main` tag + TAGS="main" + fi - # This strips the "v" prefix from the tag name. - [[ "${{ github.ref }}" == "refs/tags/"* ]] && VERSION=$(echo $VERSION | sed -e 's/^v//') - - # This uses the Docker `latest` tag convention. - [ "$VERSION" == "main" ] && VERSION=latest - echo IMAGE_ID=$IMAGE_ID - echo VERSION=$VERSION - docker tag $IMAGE_NAME $IMAGE_ID:$VERSION - docker push $IMAGE_ID:$VERSION + for TAG in $TAGS; do + echo "pushing $IMAGE_ID:$TAG" + docker tag $IMAGE_NAME $IMAGE_ID:$TAG + docker push $IMAGE_ID:$TAG + done diff --git a/.github/workflows/publish-pypi.yml b/.github/workflows/publish-pypi.yml index 0984e529e..cdc8591b7 100644 --- a/.github/workflows/publish-pypi.yml +++ b/.github/workflows/publish-pypi.yml @@ -1,22 +1,87 @@ name: Publish to PyPI + +# Triggered by publishing a GitHub Release whose tag is vX.Y.Z. +# The package version comes from that tag (setuptools-scm). + on: release: types: [published] + # manual dry run: builds and checks the distributions, publishes nothing + workflow_dispatch: + jobs: + build: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v6 + with: + # setuptools-scm needs the tags and the history + fetch-depth: 0 + + - uses: actions/setup-python@v6 + with: + python-version: "3.12" + + - name: Build + run: | + python -m pip install --upgrade build twine + python -m build + twine check --strict dist/* + + - name: Check that the version matches the tag + if: github.event_name == 'release' + run: | + expected="${GITHUB_REF_NAME#v}" + wheel=$(ls dist/*.whl) + case "$wheel" in + dist/dolmos-${expected}-*) echo "version $expected OK" ;; + *) echo "::error::wheel $wheel does not match tag $GITHUB_REF_NAME"; exit 1 ;; + esac + + - name: Smoke test the wheel + run: | + python -m venv /tmp/smoke + /tmp/smoke/bin/pip install dist/*.whl + /tmp/smoke/bin/dolmos --version + /tmp/smoke/bin/python -Ic 'import dolmos' + + - uses: actions/upload-artifact@v6 + with: + name: dist + path: dist/ + pypi: + needs: build + if: github.event_name == 'release' runs-on: ubuntu-latest - environment: release + environment: + name: release + url: https://pypi.org/project/dolmos/ permissions: - # IMPORTANT: this permission is mandatory for Trusted Publishing + # mandatory for Trusted Publishing # https://docs.pypi.org/trusted-publishers/using-a-publisher/ id-token: write steps: - - name: Checkout - uses: actions/checkout@v4 + - uses: actions/download-artifact@v7 with: - fetch-depth: 0 - - name: Build - run: python3 -m pip install --upgrade build && python3 -m build + name: dist + path: dist/ - name: Publish uses: pypa/gh-action-pypi-publish@release/v1 + github-release-assets: + needs: build + if: github.event_name == 'release' + runs-on: ubuntu-latest + permissions: + contents: write + steps: + - uses: actions/download-artifact@v7 + with: + name: dist + path: dist/ + - name: Attach the distributions to the GitHub Release + env: + GH_TOKEN: ${{ github.token }} + run: gh release upload "$GITHUB_REF_NAME" dist/* --repo "$GITHUB_REPOSITORY" --clobber diff --git a/.github/workflows/publish-solvers-package.yml b/.github/workflows/publish-solvers-package.yml index b1274e148..07860dcf1 100644 --- a/.github/workflows/publish-solvers-package.yml +++ b/.github/workflows/publish-solvers-package.yml @@ -2,7 +2,7 @@ name: Push solvers package on: - # only trigger manually, this is independent from halmos releases + # only trigger manually, this is independent from dolmos releases workflow_dispatch: push: paths: @@ -21,13 +21,13 @@ jobs: steps: - name: Login to GitHub Container Registry - uses: docker/login-action@v3 + uses: docker/login-action@v4 with: registry: ghcr.io username: ${{ github.actor }} password: ${{ secrets.GITHUB_TOKEN }} - - uses: actions/checkout@v4 + - uses: actions/checkout@v6 with: submodules: false diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index e0c9776ba..7582bea28 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -5,8 +5,8 @@ on: branches: [main, chore-workflows] workflow_dispatch: inputs: - halmos-options: - description: "additional halmos options" + dolmos-options: + description: "additional dolmos options" required: false type: string default: "" @@ -28,8 +28,10 @@ jobs: - repo: "morpho-org/morpho-blue" dir: "morpho-blue" cmd: "--solver-threads 3" - branch: "" - profile: "test" + # morpho-blue removed its halmos tests in January 2026 (d788823); + # pin the last commit that still has test/halmos/HalmosTest.sol + branch: "e773d85cd24d5162c836ec01ebcfa1d84550b668" + profile: "" - repo: "a16z/cicada" dir: "cicada" cmd: "--contract LibUint1024Test --function testProve --loop 256 --solver-threads 3" @@ -77,43 +79,51 @@ jobs: profile: "" steps: - - name: Checkout halmos - uses: actions/checkout@v4 + - name: Checkout dolmos + uses: actions/checkout@v6 with: # we won't be needing tests/lib for this workflow submodules: false - name: Build image - run: docker build -t halmos-image . --file packages/halmos/Dockerfile + run: docker build -t dolmos-image . --file packages/dolmos/Dockerfile - name: Run foundryup run: | - # run foundryup in halmos-image, save the result as a new image - docker run --name halmos-image-foundryup halmos-image foundryup + # run foundryup in dolmos-image, save the result as a new image + docker run --name dolmos-image-foundryup dolmos-image foundryup - # commit the result back to halmos-image - docker commit halmos-image-foundryup halmos-image + # commit the result back to dolmos-image + docker commit dolmos-image-foundryup dolmos-image # for snekmate - name: Install Vyper if: ${{ matrix.project.dir == 'snekmate' }} run: | - docker run --name halmos-image-vyper halmos-image uv pip install git+https://github.com/vyperlang/vyper@master - docker commit halmos-image-vyper halmos-image + docker run --name dolmos-image-vyper dolmos-image uv pip install git+https://github.com/vyperlang/vyper@master + docker commit dolmos-image-vyper dolmos-image # for sys-asm-halmos - name: Install Geas + if: ${{ matrix.project.dir == 'sys-asm-halmos' }} run: | - docker run --name tmp-halmos-image halmos-image bash -c "\ + # proxy.golang.org occasionally resets HTTP/2 streams mid-download: + # force HTTP/1.1, fall back to direct git fetch on any proxy error, retry + docker run --name tmp-dolmos-image dolmos-image bash -c "\ + set -e; \ apt-get update && \ - apt-get install -y golang-go && \ + apt-get install -y --no-install-recommends golang-go ca-certificates git && \ go version && \ - env 'GOBIN=/halmos/bin' go install github.com/fjl/geas/cmd/geas@latest && \ + export GOBIN=/dolmos/bin GOPROXY='https://proxy.golang.org|direct' GODEBUG=http2client=0; \ + for i in 1 2 3; do \ + go install github.com/fjl/geas/cmd/geas@v0.3.3 && break; \ + [ \$i -lt 3 ] || exit 1; echo \"retry \$i...\"; sleep 10; \ + done; \ geas -h" - docker commit tmp-halmos-image halmos-image + docker commit tmp-dolmos-image dolmos-image - name: Checkout external repo - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: repository: ${{ matrix.project.repo }} path: ${{ matrix.project.dir }} @@ -121,13 +131,13 @@ jobs: submodules: recursive - name: Print forge version - run: docker run halmos-image forge --version + run: docker run dolmos-image forge --version - - name: Print halmos version - run: docker run halmos-image halmos --version + - name: Print dolmos version + run: docker run dolmos-image dolmos --version - name: Test external repo - run: docker run -e FOUNDRY_PROFILE -v .:/workspace halmos-image halmos ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }} + run: docker run -e FOUNDRY_PROFILE -v .:/workspace dolmos-image dolmos ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 ${{ matrix.cache-solver }} ${{ inputs.dolmos-options }} working-directory: ${{ matrix.project.dir }} env: FOUNDRY_PROFILE: ${{ matrix.project.profile }} diff --git a/.github/workflows/test-ffi.yml b/.github/workflows/test-ffi.yml index 6026e5f65..a68f67821 100644 --- a/.github/workflows/test-ffi.yml +++ b/.github/workflows/test-ffi.yml @@ -18,16 +18,16 @@ jobs: - testname: "tests/ffi" steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v6 with: submodules: recursive - name: Build image run: | - docker build -t halmos-image . --file packages/halmos/Dockerfile + docker build -t dolmos-image . --file packages/dolmos/Dockerfile - - name: Print halmos version - run: docker run halmos-image halmos --version + - name: Print dolmos version + run: docker run dolmos-image dolmos --version - name: Run pytest - run: docker run -v .:/workspace halmos-image pytest -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="--ffi -v -st" + run: docker run -v .:/workspace dolmos-image pytest -v tests/test_dolmos.py -k ${{ matrix.testname }} --dolmos-options="--ffi -v -st" diff --git a/.github/workflows/test-long.yml b/.github/workflows/test-long.yml index 03b99c34b..6cdfed382 100644 --- a/.github/workflows/test-long.yml +++ b/.github/workflows/test-long.yml @@ -5,8 +5,8 @@ on: branches: [main, chore-workflows] workflow_dispatch: inputs: - halmos-options: - description: "additional halmos options" + dolmos-options: + description: "additional dolmos options" required: false type: string default: "" @@ -28,17 +28,17 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: submodules: recursive - name: Build image run: | - docker build -t halmos-image . --file packages/halmos/Dockerfile + docker build -t dolmos-image . --file packages/dolmos/Dockerfile - - name: Print halmos version - run: docker run halmos-image halmos --version + - name: Print dolmos version + run: docker run dolmos-image dolmos --version - name: Run pytest run: | - docker run -v .:/workspace halmos-image pytest -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options='-st --solver-threads 3 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}' -s --log-cli-level= + docker run -v .:/workspace dolmos-image pytest -x -v tests/test_dolmos.py -k ${{ matrix.testname }} --dolmos-options='-st --solver-threads 3 ${{ matrix.cache-solver }} ${{ inputs.dolmos-options }}' -s --log-cli-level= diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 1145e13b1..2aa24b650 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -7,8 +7,8 @@ on: branches: [main] workflow_dispatch: inputs: - halmos-options: - description: "additional halmos options" + dolmos-options: + description: "additional dolmos options" required: false type: string default: "" @@ -22,7 +22,7 @@ jobs: test: runs-on: ${{ matrix.os }} env: - HALMOS_ALLOW_DOWNLOAD: 1 + DOLMOS_ALLOW_DOWNLOAD: 1 strategy: fail-fast: false @@ -34,7 +34,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: # note: it is faster to let foundry do a sparse checkout of the missing libraries rather than having the action do a git checkout of the submodules submodules: false @@ -46,7 +46,7 @@ jobs: run: forge --version - name: Install uv - uses: astral-sh/setup-uv@v4 + uses: astral-sh/setup-uv@v7 with: # Install a specific version of uv. version: "0.5.21" @@ -54,20 +54,25 @@ jobs: - name: Set up python ${{ matrix.python-version }} run: uv python install ${{ matrix.python-version }} - - name: Install halmos and its dependencies + - name: Install dolmos and its dependencies run: | uv sync --extra dev - - name: Write halmos.toml + - name: Write dolmos.toml shell: bash run: | - uv run python -m halmos.config \ + uv run python -m dolmos.config \ --storage-layout ${{ matrix.storage-layout }} \ ${{ matrix.cache-solver }} \ - | tee tests/regression/halmos.toml + | tee tests/regression/dolmos.toml - name: Run pytest shell: bash run: | - uv run pytest -v -k "not long and not ffi" --ignore=tests/lib \ - --halmos-options="-st --disable-gc --solver-threads 1 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }} + # failed tests are reported as annotations on the run page (readable without + # signing in, pytest-github-actions-annotate-failures in the dev extras), and + # summarized at the end of the log (-rfE). + # no `uv run --with`: it runs pytest in an overlay environment, where dolmos + # does not find z3.exe (installed in .venv\bin, not on PATH, on Windows) + uv run pytest -v -rfE -k "not long and not ffi" --ignore=tests/lib \ + --dolmos-options="-st --disable-gc --solver-threads 1 ${{ inputs.dolmos-options }}" ${{ inputs.pytest-options }} diff --git a/BUILDING.md b/BUILDING.md new file mode 100644 index 000000000..0021730f0 --- /dev/null +++ b/BUILDING.md @@ -0,0 +1 @@ +pip install -e ".[dev]" diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 000000000..51e3200bc --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,115 @@ +# Changelog + +All notable changes to dolmos are documented here. The format follows +[Keep a Changelog](https://keepachangelog.com/en/1.1.0/) and versions follow +[Semantic Versioning](https://semver.org/). Dolmos is derived from halmos; see +[NOTICE](NOTICE) for the upstream commit it is based on. + +## [Unreleased] + +## [0.2.0] - 2026-10-16 + +### Added + +- file cheatcodes `vm.readFile`, `vm.readFileBinary`, `vm.parseBytes` and + `vm.projectRoot`, e.g. to deploy Huff bytecode read from a file; reads honor + `fs_permissions` from `foundry.toml` with foundry's semantics, and + `vm.parseBytes` accepts exactly what foundry accepts (halmos#213) +- `vm.expectRevert` (all overloads, including the reverter address and `count` + variants), `vm.expectPartialRevert`, `vm.expectEmit` and + `vm.expectEmitAnonymous` (including the emitter address and `count` variants), + with foundry's semantics; symbolic revert data and event fields are matched + symbolically and a counterexample is reported when an expectation can be + violated (halmos#409) +- multiple setup states: when `setUp()` has several feasible successful paths, + each test and each invariant test sequence is run from every one of them, + instead of failing with "Multiple paths were found in setUp()" (halmos#186) +- experimental: `--dump-lassos DIR` exports each loop that reaches the unrolling + bound as a lasso program, and `--pasttel BINARY` analyses it with PaSTTeL + (termination proof with a ranking function, or non-termination). Lassos use + a small-constants encoding by default, because PaSTTeL computes with doubles + and is unsound on 2^256 constants; `--lasso-exact-constants` gives the exact + encoding. See docs/loop-termination.md +- `SELFDESTRUCT` opcode, with the EIP-6780 (Cancun) semantics: the balance is sent to + the beneficiary and the frame halts; the account (code, storage, balance, nonce) is + deleted at the end of the transaction only if it was created in that transaction; + forbidden in static contexts (halmos#411) +- EVM version setting, `--evm-version VERSION` (also usable in `dolmos.toml` and + `@custom:dolmos` annotations): opcodes introduced after the selected fork are invalid, + and `SELFDESTRUCT` deletes the account unconditionally before Cancun. Defaults to the + `evmVersion` the test contract was compiled for (foundry's `evm_version`), or to the + latest supported fork, `osaka` (halmos#128) +- `--pretty-counterexamples` (`-pcex`) prints counterexamples that can be acted upon; see + docs/pretty-counterexamples.md: + - test arguments decoded with the ABI of the test, with the lengths of dynamic values + applied and values rendered by type (decimal, checksummed addresses, strings) + - `bytes` holding calldata decoded with the ABIs of the compiled contracts, and calls + made with calldata built by `svm.createCalldata` listed (halmos#369) + - `bytes4` values rendered as selectors, `0x00000000` as the empty selector of plain + ether transfers (halmos#419) + - invariant call sequences with concrete senders, values, arguments and timestamps + - a forge test replaying each counterexample + - duplicate counterexamples hidden, and counted (halmos#398) + - potentially invalid counterexamples relying on the approximation of `EXP` checked + against the real exponentiation: they are confirmed, replaced by a valid one, or + proven spurious; otherwise the reason is printed (halmos#280) + +### Fixed + +- `--early-exit` no longer reports the queries cancelled after the first counterexample as + solver errors (`executor has been shutdown`), nor saves them as failed queries + (halmos#398) +- SHA256, RIPEMD160 and MODEXP precompiles with symbolic input no longer crash + with a z3 sort mismatch (input sizes were given in bytes instead of bits). + Concrete inputs are now evaluated exactly; MODEXP follows EIP-198 (zero-padded + input, output on `len(M)` bytes) and EIP-7823 (lengths above 1024 bytes make + the call fail), and its symbolic model guarantees `result < M` (halmos#402) +- storage slots written as precomputed keccak256 literals (e.g. constant-folded by the + via-IR optimizer in a constructor) and read through SHA3 at runtime now hit the same + storage cell, instead of reading zero and reporting a false counterexample; applies to + both storage layouts (halmos#579) +- counterexamples relying on keccak256 values that differ from the real hash function + (keccak256 is uninterpreted, so the solver could pick e.g. `x = 0` and assume that its + hash is the key of a storage entry) are no longer reported as valid. The real hashes of + the preimages chosen by the model are added to the query, which is solved again, up to + `--keccak-refinement-rounds` times (default 3, 0 disables the check); a counterexample + that still disagrees is reported as potentially invalid (halmos#562) +- on Windows, `--solver-command` with a path such as `C:\solvers\z3.exe` is no + longer mangled (backslashes were parsed as shell escapes); quotes still group words +- on Windows, `vm.readFile` no longer falls back to foundry's default `fs_permissions` + when `forge config` writes non-ascii output, and `fs_permissions` paths are matched + case-insensitively, as by foundry + +## [0.1.0] - 2026-09-22 + +First release of dolmos. + +### Added + +- CREATE address derivation from `keccak256(rlp([sender, nonce]))` and account + nonces (EIP-161), so that CREATE3-style address prediction matches execution +- nonce cheatcodes: `vm.getNonce`, `vm.setNonce`, `vm.setNonceUnsafe`, + `vm.resetNonce` +- opcodes `CLZ` (EIP-7939), `BLOBHASH` and `BLOBBASEFEE` (EIP-4844) +- experimental Vyper support: Vyper test contracts, Solidity tests targeting + Vyper contracts, `@custom:dolmos` annotations in docstrings, + `--invalid-as-failure` +- `dolmos.toml` configuration file and `@custom:dolmos` annotations + (`halmos.toml`, `@custom:halmos` and `HALMOS_ALLOW_DOWNLOAD` remain accepted) +- PyPI package and Docker image `ghcr.io/dowsers/dolmos` + +### Changed + +- command, Python package and symbolic variable prefix renamed from `halmos` to + `dolmos`; downloaded solvers are cached in `~/.dolmos/solvers` + +### Fixed + +- Vyper artifact lookup in the forge cache on Windows +- builds with forge ≥ 1.8: `dynamic_test_linking` is disabled when dolmos runs + `forge build`, since it rewrites `new C()` into unsupported `vm.deployCode` + calls + +[Unreleased]: https://github.com/Dowsers/dolmos/compare/v0.2.0...HEAD +[0.2.0]: https://github.com/Dowsers/dolmos/compare/v0.1.0...v0.2.0 +[0.1.0]: https://github.com/Dowsers/dolmos/releases/tag/v0.1.0 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 4c385ca98..b8bf7e56b 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,10 +1,7 @@ -# Contributing to Halmos +# Contributing to dolmos -We greatly appreciate your feedback, suggestions, and contributions to make Halmos a better tool for everyone! - -Join the [Halmos Telegram Group][chat] for any inquiries or further discussions. - -[chat]: +Bug reports, suggestions and pull requests are welcome on +[GitHub](https://github.com/Dowsers/dolmos/issues). ## Development Setup @@ -12,13 +9,13 @@ Clone or fork the repository: ```sh # if you want to submit a pull request, fork the repository: -gh repo fork a16z/halmos +gh repo fork Dowsers/dolmos # Or, if you just want to develop locally, clone it: -git clone git@github.com:a16z/halmos.git +git clone git@github.com:Dowsers/dolmos.git # navigate to the project directory -cd halmos +cd dolmos ``` **Recommended**: set up the development environment using [uv](https://docs.astral.sh/uv/): @@ -39,8 +36,8 @@ uv sync --extra dev uv run pre-commit install uv run pre-commit run --all-files -# make changes to halmos, then run it with: -uv run halmos +# make changes to dolmos, then run it with: +uv run dolmos # run the tests with: uv run pytest @@ -65,7 +62,7 @@ Alternatively, you can manage the python version and the virtual environment man # create and activate a virtual environment with a suitable python version python3.12 -m venv .venv && source .venv/bin/activate -# install halmos and its runtime dependencies in editable mode +# install dolmos and its runtime dependencies in editable mode python -m pip install -e ".[dev]" # install and run the pre-commit hooks @@ -94,4 +91,4 @@ By contributing, you agree that your contributions will be licensed under its [A ## Disclaimer -_These smart contracts and code are being provided as is. No guarantee, representation or warranty is being made, express or implied, as to the safety or correctness of the user interface or the smart contracts and code. They have not been audited and as such there can be no assurance they will work as intended, and users may experience delays, failures, errors, omissions or loss of transmitted information. THE SMART CONTRACTS AND CODE CONTAINED HEREIN ARE FURNISHED AS IS, WHERE IS, WITH ALL FAULTS AND WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING ANY WARRANTY OF MERCHANTABILITY, NON-INFRINGEMENT OR FITNESS FOR ANY PARTICULAR PURPOSE. Further, use of any of these smart contracts and code may be restricted or prohibited under applicable law, including securities laws, and it is therefore strongly advised for you to contact a reputable attorney in any jurisdiction where these smart contracts and code may be accessible for any questions or concerns with respect thereto. Further, no information provided in this repo should be construed as investment advice or legal advice for any particular facts or circumstances, and is not meant to replace competent counsel. a16z is not liable for any use of the foregoing, and users should proceed with caution and use at their own risk. See a16z.com/disclosures for more info._ +See the disclaimer in the [README](README.md#disclaimer). diff --git a/MANIFEST.in b/MANIFEST.in new file mode 100644 index 000000000..3d8cb64a3 --- /dev/null +++ b/MANIFEST.in @@ -0,0 +1,6 @@ +# setuptools-scm puts every git-tracked file in the sdist, submodules included. +# Keep the sdist to what is needed to build and test dolmos itself. +prune tests/lib +prune benchmarks +prune .github +prune .devcontainer diff --git a/NOTICE b/NOTICE new file mode 100644 index 000000000..e0bfcf3bc --- /dev/null +++ b/NOTICE @@ -0,0 +1,45 @@ +dolmos +Copyright (C) 2026 Dowsers SAS + +This program is free software: you can redistribute it and/or modify it under +the terms of the GNU Affero General Public License as published by the Free +Software Foundation, version 3. See LICENSE. + + +ORIGIN +====== + +dolmos is a modified version of halmos (https://github.com/a16z/halmos), +a symbolic testing tool for EVM smart contracts developed by a16z crypto and its +contributors (maintainers at the time of the fork: Daejun Park, karmacoma), +distributed under the GNU Affero General Public License v3. + +dolmos is based on halmos as of upstream commit "fix: shorten bytecode output in +unknown deployed bytecode warning (#573)" (2025-08-06). Dowsers SAS has modified +it since 2026-05-15; the modifications include CREATE address derivation and +account nonces, nonce cheatcodes, the CLZ, BLOBHASH and BLOBBASEFEE opcodes, +Vyper support, and the renaming of the command, the Python package and the +Docker images to dolmos. The git history records every change. + +dolmos is maintained by Dowsers SAS and is not affiliated with or endorsed by +a16z crypto or the halmos maintainers. + + +COMPATIBILITY WITH HALMOS +========================= + +For compatibility with existing test suites, dolmos still accepts the +`@custom:halmos` natspec tag, the `halmos.toml` configuration file name and the +HALMOS_ALLOW_DOWNLOAD environment variable, and it supports the cheatcodes of +the halmos-cheatcodes Solidity library (https://github.com/a16z/halmos-cheatcodes), +which is a separate project used by the test suite as a git submodule. + + +DISCLAIMER OF THE ORIGINAL WORK +=============================== + +The following disclaimer accompanies halmos and applies to the original work: + +_These smart contracts and code are being provided as is. No guarantee, representation or warranty is being made, express or implied, as to the safety or correctness of the user interface or the smart contracts and code. They have not been audited and as such there can be no assurance they will work as intended, and users may experience delays, failures, errors, omissions or loss of transmitted information. THE SMART CONTRACTS AND CODE CONTAINED HEREIN ARE FURNISHED AS IS, WHERE IS, WITH ALL FAULTS AND WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING ANY WARRANTY OF MERCHANTABILITY, NON-INFRINGEMENT OR FITNESS FOR ANY PARTICULAR PURPOSE. Further, use of any of these smart contracts and code may be restricted or prohibited under applicable law, including securities laws, and it is therefore strongly advised for you to contact a reputable attorney in any jurisdiction where these smart contracts and code may be accessible for any questions or concerns with respect thereto. Further, no information provided in this repo should be construed as investment advice or legal advice for any particular facts or circumstances, and is not meant to replace competent counsel. a16z is not liable for any use of the foregoing, and users should proceed with caution and use at their own risk. See a16z.com/disclosures for more info._ + +The same absence of warranty applies to the modifications made by Dowsers SAS. diff --git a/README.md b/README.md index e06d88444..a188784a4 100644 --- a/README.md +++ b/README.md @@ -1,102 +1,207 @@ -# Halmos +# Dolmos + +[![License](https://img.shields.io/github/license/Dowsers/dolmos)](https://github.com/Dowsers/dolmos/blob/main/LICENSE) +[![Python Version from PEP 621 TOML](https://img.shields.io/python/required-version-toml?tomlFilePath=https%3A%2F%2Fraw.githubusercontent.com%2FDowsers%2Fdolmos%2Frefs%2Fheads%2Fmain%2Fpyproject.toml)](pyproject.toml) + +Dolmos is a _symbolic testing_ tool for EVM smart contracts, driven by +Foundry-style tests, maintained by [Dowsers](https://github.com/Dowsers) for its +audit and formal verification work. Tests look like fuzz tests, but inputs are +symbolic: a passing test holds for every input, and a failing one comes with a +counterexample. + +Start with the [getting started guide](https://github.com/Dowsers/dolmos/blob/main/docs/getting-started.md) and the +[examples](https://github.com/Dowsers/dolmos/blob/main/examples/README.md). +Loops that reach the unrolling bound can be exported for termination analysis with +PaSTTeL (experimental): see [docs/loop-termination.md](https://github.com/Dowsers/dolmos/blob/main/docs/loop-termination.md). + +## Features + +On top of symbolic execution of Solidity (and Vyper) tests with `check_*` and +`invariant_*` functions, dolmos provides the following. + +**CREATE address derivation and account nonces.** Accounts carry nonces (1 for a +newly created account per EIP-161, incremented by CREATE and CREATE2 even when +the creation fails), and CREATE addresses are derived from +`keccak256(rlp([sender, nonce]))`, mapped to a magic address as for CREATE2. A +contract that predicts its own deployment address, as every CREATE3 library +does, therefore agrees with the executor. + +**Nonce cheatcodes.** `vm.getNonce`, `vm.setNonce`, `vm.setNonceUnsafe` and +`vm.resetNonce`, with foundry's semantics: `setNonce` only raises a nonce, +`resetNonce` gives 0 to EOAs and 1 to accounts with code. + +**File cheatcodes.** `vm.readFile`, `vm.readFileBinary`, `vm.parseBytes` and +`vm.projectRoot`, so a test can deploy bytecode compiled outside solc (Huff, for +instance) from a file. Reads are subject to `fs_permissions` in `foundry.toml`, +resolved with `forge config` and applied as foundry does (paths normalized +against the project root, most specific permission wins, denied by default), so +a test that reads a file passes or fails the same way under `forge test`. + +**Fusaka / Cancun opcodes.** `CLZ` (EIP-7939), with a concrete fast path and a +logarithmic symbolic encoding, plus `BLOBHASH` and `BLOBBASEFEE` (EIP-4844). + +**Vyper.** Test contracts can be written in Vyper, and Solidity tests can target +Vyper contracts. forge's Vyper artifacts have no AST, no metadata and an empty +`methodIdentifiers`; dolmos reads `.vy`/`.vyi` artifacts, computes the selectors +from the ABI, takes the source path and compiler version from forge's cache, and +makes Vyper contracts visible to Solidity tests (deployed code, ABI for +invariant targets and traces, including contracts with immutables). +`vm.getCode` accepts `Foo.vy`, `src/Foo.vy` and `Foo.vy:Foo`. + +A Vyper test looks like a Solidity one: `setUp()` and `check_*`/`invariant_*` +functions, with cheatcodes called through an interface at +`0x7109709ECfa91a80626fF3989D68f67F5b1DD12D`. Use `assert ..., UNREACHABLE` for +properties: it compiles to the INVALID opcode, which the `--invalid-as-failure` +option reports as a failure, even when it is hit in a nested call and bubbles up +as an empty revert. A plain `assert` is an empty revert, indistinguishable from +a `require`, so the path is silently discarded. The `vm.assert*` cheatcodes work +as well. `@custom:dolmos` annotations go in the module and function docstrings. + +When the build contains Vyper contracts, `--storage-layout generic` (Vyper +computes `HashMap` slots as `keccak256(slot . key)`) and `--invalid-as-failure` +become the defaults; a value set in `dolmos.toml`, an annotation or on the +command line still wins. Coverage reports do not include Vyper code, since forge +emits no source maps for it. See `tests/vyper` for examples. + +## Compatibility with halmos + +Dolmos is derived from halmos (see [NOTICE](https://github.com/Dowsers/dolmos/blob/main/NOTICE)) and accepts the names used +by test suites written for it, so they should run without changes: + +| halmos | dolmos | | +|---|---|---| +| `@custom:halmos` | `@custom:dolmos` | both accepted, in contracts and functions | +| `halmos.toml` | `dolmos.toml` | `dolmos.toml` is read first | +| `HALMOS_ALLOW_DOWNLOAD` | `DOLMOS_ALLOW_DOWNLOAD` | both honored | +| `halmos-cheatcodes` | unchanged | the `svm.*` cheatcodes of this library are supported | + +Some things do change: the command and the Python package are named `dolmos` +(`import dolmos`), symbolic variables in counterexamples are prefixed with +`dolmos_`, and solvers downloaded on demand are cached in `~/.dolmos/solvers`. -[![PyPI - Version](https://img.shields.io/pypi/v/halmos)](https://pypi.org/project/halmos) -[![Python Version from PEP 621 TOML](https://img.shields.io/python/required-version-toml?tomlFilePath=https%3A%2F%2Fraw.githubusercontent.com%2Fa16z%2Fhalmos%2Frefs%2Fheads%2Fmain%2Fpyproject.toml)](https://github.com/a16z/halmos) -[![License](https://img.shields.io/github/license/a16z/halmos)](https://github.com/a16z/halmos/blob/main/LICENSE) -[![chat](https://img.shields.io/badge/chat-telegram-blue)](https://t.me/+4UhzHduai3MzZmUx) - -[**Install**](https://github.com/a16z/halmos?tab=readme-ov-file#installation) -| [**Getting Started**](https://github.com/a16z/halmos/blob/main/docs/getting-started.md) -| [**Examples**](https://github.com/a16z/halmos/blob/main/examples/README.md) -| [**FAQ**](https://github.com/a16z/halmos/wiki/FAQ) -| [**Chat**][chat] -| [**awesome-halmos**](https://github.com/redtrama/awesome-halmos) - -Halmos is a _symbolic testing_ tool for EVM smart contracts. A Solidity/Foundry frontend is currently offered by default, with plans to provide support for other languages, such as Vyper and Huff, in the future. - -You can read more in our post: "_[Symbolic testing with Halmos: Leveraging existing tests for formal verification][post]_." +## Installation -Join the [Halmos Telegram Group][chat] for any inquiries or further discussions. +Requires Python ≥ 3.11 and [Foundry](https://getfoundry.sh). -[post]: https://a16zcrypto.com/symbolic-testing-with-halmos-leveraging-existing-tests-for-formal-verification/ -[chat]: https://t.me/+4UhzHduai3MzZmUx +With [uv](https://docs.astral.sh/uv/) (recommended, installs `dolmos` as an +isolated command-line tool): -## Installation +```sh +uv tool install dolmos +dolmos --version +``` -### ⭐ Using `uv` (recommended for most users) +With pipx or pip: ```sh -# install uv if you don't have it already -curl -LsSf https://astral.sh/uv/install.sh | sh +pipx install dolmos +# or, in a virtual environment +pip install dolmos +``` -# install the latest version of halmos for the current user and add it to PATH -uv tool install --python 3.12 halmos +Upgrade with `uv tool upgrade dolmos` (or `pipx upgrade dolmos`, +`pip install -U dolmos`). -# or, install the development version from the repository -# uv tool install --python 3.12 git+https://github.com/a16z/halmos +### Docker -# after installing, you can update halmos to the latest version with: -uv tool upgrade halmos -``` +Each release is published as a Docker image that bundles dolmos, Foundry and the +SMT solvers (yices, z3, cvc5, bitwuzla, stp): -### Using `docker` +```sh +docker run --rm -v "$PWD":/workspace ghcr.io/dowsers/dolmos:latest dolmos +# or a fixed version +docker run --rm -v "$PWD":/workspace ghcr.io/dowsers/dolmos:0.1.0 dolmos +``` -You can download a pre-built Docker image that contains python, halmos, its dependencies, foundry, solvers, etc.: +### From source ```sh -docker pull ghcr.io/a16z/halmos:latest +git clone https://github.com/Dowsers/dolmos.git +cd dolmos +uv sync --extra dev # or: python -m venv .venv && pip install -e ".[dev]" +uv run dolmos --version ``` -### Using `pip` (for advanced users) +See [CONTRIBUTING.md](https://github.com/Dowsers/dolmos/blob/main/CONTRIBUTING.md) +for the development setup. -Note: this is not recommended because of the extra work required to manage the python version and the virtual environment. But if you know what you are doing, and need the extra control, you can do it like this: +## Usage ```sh -# make sure you have a suitable python version installed, e.g.: -python3.12 --version +cd /path/to/foundry/project +forge build +dolmos +``` -# create and activate a virtual environment with an explicit python version -python3.12 -m venv .venv && source .venv/bin/activate +```sh +dolmos --help +dolmos -test # alias for --match-test +dolmos --match-contract +``` -# install the latest version of halmos -pip install halmos +Options can be set per project in `dolmos.toml` at the project root: -# or, install the development version from the repository -pip install git+https://github.com/a16z/halmos +```toml +[global] +solver-timeout-assertion = 10000 ``` -## Usage +`python -m dolmos.config` prints every option with its default value, in that +format. Warnings link to their explanation in [docs/warnings.md](https://github.com/Dowsers/dolmos/blob/main/docs/warnings.md). + +## Tests ```sh -cd /path/to/src -halmos +pytest # unit tests and integration tests +pytest tests/test_dolmos.py -k "not long" ``` -For more details: +The regression suite lives in `tests/regression` and runs with both forge (real +EVM) and dolmos (symbolic): ```sh -halmos --help +cd tests/regression +forge build +dolmos ``` -Alternatively, you can run the latest halmos Docker image available at [ghcr.io/a16z/halmos](https://ghcr.io/a16z/halmos): +A few notes on the toolchain: -```sh -cd /path/to/src +- The suite sets `evm_version = 'osaka'` because of the CLZ tests, and + `test/OpCodesCLZ.sol` needs a solc recent enough to accept `clz()` in assembly + (0.8.31 or later); an older compiler fails with `Function "clz" not found`. +- `test/Invalid.t.sol` requires solc `^0.5.2`; if that version is unavailable, + `forge build` stops there. +- `test/Arith.t.sol` uses the `bitwuzla-abs` solver; set + `DOLMOS_ALLOW_DOWNLOAD=1` to let dolmos download it. +- The Vyper tests live in `tests/vyper` and need the `vyper` compiler in `PATH` + (`pip install vyper`); pytest skips them otherwise. -# mount '.' under /workspace in the container -docker run -v .:/workspace ghcr.io/a16z/halmos:latest -``` +## Contributing -## Getting Started +See [CONTRIBUTING.md](https://github.com/Dowsers/dolmos/blob/main/CONTRIBUTING.md). -Refer to the [getting started guide](docs/getting-started.md) and the [examples](examples/README.md) directory. +## Roadmap -## Contributing / Developing +- MODEXP precompile (EIP-198): concrete evaluation and a typed uninterpreted + function instead of the current opaque one +- performance: skip the Z3 `substitute()` traversal when no free variable + matches, bound the concurrency of solver subprocesses, memoize invariant + target resolution +- support multiple `setUp()` states -Refer to the [contributing guidelines](CONTRIBUTING.md), and explore the list of issues labeled ["good first issue" or "help wanted."][issues] +## License -[issues]: https://github.com/a16z/halmos/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22%2C%22help+wanted%22 +AGPL-3.0, see [LICENSE](https://github.com/Dowsers/dolmos/blob/main/LICENSE). Dolmos is a modified version of another +AGPL-3.0 program; [NOTICE](https://github.com/Dowsers/dolmos/blob/main/NOTICE) gives its origin and the notices that come +with it. ## Disclaimer -_These smart contracts and code are being provided as is. No guarantee, representation or warranty is being made, express or implied, as to the safety or correctness of the user interface or the smart contracts and code. They have not been audited and as such there can be no assurance they will work as intended, and users may experience delays, failures, errors, omissions or loss of transmitted information. THE SMART CONTRACTS AND CODE CONTAINED HEREIN ARE FURNISHED AS IS, WHERE IS, WITH ALL FAULTS AND WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING ANY WARRANTY OF MERCHANTABILITY, NON-INFRINGEMENT OR FITNESS FOR ANY PARTICULAR PURPOSE. Further, use of any of these smart contracts and code may be restricted or prohibited under applicable law, including securities laws, and it is therefore strongly advised for you to contact a reputable attorney in any jurisdiction where these smart contracts and code may be accessible for any questions or concerns with respect thereto. Further, no information provided in this repo should be construed as investment advice or legal advice for any particular facts or circumstances, and is not meant to replace competent counsel. a16z is not liable for any use of the foregoing, and users should proceed with caution and use at their own risk. See a16z.com/disclosures for more info._ +_This software and the smart contracts in this repository are provided as is, +without warranty of any kind, express or implied, including any warranty of +merchantability, non-infringement or fitness for a particular purpose. They have +not been audited. Passing symbolic tests is not a proof that a contract is free +of bugs. Nothing in this repository is investment or legal advice. See +[NOTICE](https://github.com/Dowsers/dolmos/blob/main/NOTICE) for the disclaimers attached to the original work this code is +derived from._ diff --git a/RELEASING.md b/RELEASING.md new file mode 100644 index 000000000..f8b6215e5 --- /dev/null +++ b/RELEASING.md @@ -0,0 +1,60 @@ +# Releasing dolmos + +A release is a git tag `vX.Y.Z` plus a GitHub Release. The package version is +derived from the tag by setuptools-scm: there is no version number to edit in +the code. + +## One-time setup + +1. **PyPI Trusted Publisher.** On https://pypi.org/manage/account/publishing/, + add a *pending publisher* (the `dolmos` project does not exist yet): + owner `Dowsers`, repository `dolmos`, workflow `publish-pypi.yml`, + environment `release`. After the first upload, the pending publisher becomes + a regular one. Do the same on https://test.pypi.org if you want dry runs. +2. **GitHub environment.** In the repository settings, create the `release` + environment and add required reviewers, so that a PyPI upload always needs + an explicit approval. +3. **Docker images.** Run, in this order and once, the workflows + `Push solvers package`, `Push dolmos-builder package` and + `Push dolmos package` (each triggers the next one). Then, in the + organization's *Packages* page, set `solvers`, `dolmos-builder` and `dolmos` + to **public** and link them to this repository. The CI jobs that run inside + these images (`test-long`, `test-ffi`, `test-external`) need them. +4. **Tag protection.** Add a ruleset that restricts who can create `v*` tags. + +## Release checklist + +1. All workflows are green on `main` (`Test`, `Test long`, `Test external`, + `pre-commit`). +2. Move the entries of `## [Unreleased]` in `CHANGELOG.md` under a new + `## [X.Y.Z] - YYYY-MM-DD` heading, update the links at the bottom, commit. +3. Optional dry run: run `Publish to PyPI` by hand (*workflow_dispatch*); it + builds, checks and smoke-tests the distributions without publishing. +4. Tag and push: + + ```sh + git tag -a vX.Y.Z -m "dolmos X.Y.Z" + git push origin vX.Y.Z + ``` + + The tag push triggers `Push dolmos package`, which publishes + `ghcr.io/dowsers/dolmos:X.Y.Z`, `:X.Y` and `:latest`. +5. Create the GitHub Release from the tag, with the changelog section as notes: + + ```sh + gh release create vX.Y.Z --title "dolmos X.Y.Z" --notes-file <(sed -n '/## \[X.Y.Z\]/,/## \[/p' CHANGELOG.md | sed '$d') + ``` + + Publishing it triggers `Publish to PyPI` (after the `release` environment + approval), which uploads to PyPI and attaches the wheel and sdist to the + release. +6. Check: `uv tool install dolmos==X.Y.Z && dolmos --version`, and + `docker run --rm ghcr.io/dowsers/dolmos:X.Y.Z dolmos --version`. + +A version published on PyPI can never be re-uploaded. If a release is broken, +yank it on PyPI and release `X.Y.(Z+1)`. + +## Version numbers + +- `0.x`: the CLI and the configuration may still change between minor versions. +- Patch releases (`0.1.1`) only contain fixes. diff --git a/benchmarks/baolean.sh b/benchmarks/baolean.sh index 73f2229df..2c37b2629 100755 --- a/benchmarks/baolean.sh +++ b/benchmarks/baolean.sh @@ -13,6 +13,6 @@ fi for test_name in "PostExampleTest" "PostExampleTwoTest" "PostExampleTwoLiveTest" "FooTest" "MiniVatTest"; do echo echo -e "▀▄▀▄▀▄ 🎀 Running ${GREEN}${test_name}${NC} 🎀 ▄▀▄▀▄▀" - time halmos --root symexec-bench/SymTest --contract ${test_name} "--function" test + time dolmos --root symexec-bench/SymTest --contract ${test_name} "--function" test done diff --git a/docs/getting-started.md b/docs/getting-started.md index bfac18cc0..3ae44f352 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -1,4 +1,4 @@ -# How to write symbolic tests with Halmos +# How to write symbolic tests with dolmos Symbolic tests look similar to fuzz tests, but there are certain differences that need to be understood. This guide will walk you through the process of writing symbolic tests, highlighting the differences compared to fuzz tests. It is intended for those who are already familiar with [Dapptools]-/[Foundry]-style fuzz tests. If you haven't experienced fuzz tests before, please refer to the [Foundry document][Foundry Fuzz Testing] to grasp the basic concepts. @@ -6,21 +6,17 @@ Symbolic tests look similar to fuzz tests, but there are certain differences tha [Foundry]: [Foundry Fuzz Testing]: -## 0. Install Halmos +## 0. Install dolmos -If you haven't installed Halmos yet, please refer to the [installation guide](../README.md#installation) or quickly install it with: - -```sh -uv tool install halmos -``` +If you haven't installed dolmos yet, follow the [installation guide](../README.md#installation). ## 1. Write setUp() Similar to foundry tests, you can provide the `setUp()` function that will be executed before each test. In the setup function, you can create an instance of the target contracts, and initialize their state. These initialized contracts will then be accessible for every test. -Furthermore, you are also allowed to call the constructor with symbolic arguments, initializing the contract state to be symbolic. You can create those symbols using [Halmos cheatcodes]. +Furthermore, you are also allowed to call the constructor with symbolic arguments, initializing the contract state to be symbolic. You can create those symbols using the cheatcodes of the [halmos-cheatcodes] library, which dolmos supports. -[Halmos cheatcodes]: +[halmos-cheatcodes]: For example, consider a basic ERC20 token contract as shown below: ```solidity @@ -53,12 +49,14 @@ By using the symbolic initial supply, you can check if the given tests pass for **Tips:** -- The Halmos cheatcodes can be installed like any other Solidity dependencies: +- The cheatcodes library can be installed like any other Solidity dependency: ``` forge install a16z/halmos-cheatcodes ``` -- The current list of available Halmos cheatcodes can be found [here][halmos-cheatcodes-list]. +- The current list of available cheatcodes can be found [here][halmos-cheatcodes-list]. + +- `setUp()` may branch on symbolic values (or revert on some of them): every feasible successful path becomes a separate setup state, and each test (and each invariant test sequence) is run from each of them. Counterexamples include the symbolic values that select the setup state. Run with `-v` to display the number of setup states. [halmos-cheatcodes-list]: @@ -128,7 +126,7 @@ for (uint160 sender = 0; sender < type(uint160).max; sender++) { **Tips:** -- Instead of declaring symbolic input parameters, you can dynamically create symbols inside the test using the Halmos cheatcodes. For instance, our running example can be rewritten as follows: +- Instead of declaring symbolic input parameters, you can dynamically create symbols inside the test using the symbolic cheatcodes. For instance, our running example can be rewritten as follows: ```solidity function check_transfer() { address sender = svm.createAddress("sender"); @@ -138,7 +136,7 @@ for (uint160 sender = 0; sender < type(uint160).max; sender++) { } ``` -- Halmos requires dynamically-sized arrays (including `bytes` and `string`) to be given with a fixed size. Thus they cannot be declared as input parameters, but need to be programmatically constructed. For example, a byte array can be generated using the `svm.createBytes()` cheatcode as follows: +- Dolmos requires dynamically-sized arrays (including `bytes` and `string`) to be given with a fixed size. Thus they cannot be declared as input parameters, but need to be programmatically constructed. For example, a byte array can be generated using the `svm.createBytes()` cheatcode as follows: ```solidity bytes memory data = svm.createBytes(96, 'data'); ``` @@ -200,6 +198,15 @@ token.transfer(receiver, amount); } ``` +- Foundry's `vm.expectRevert()` (all variants, including `expectPartialRevert`, the reverter address and the `count` overloads) and `vm.expectEmit()` (including `expectEmitAnonymous`, the emitter address and the `count` overloads) are supported, with the same semantics as in foundry. With symbolic inputs, dolmos reports a counterexample whenever the expectation can be violated: + ```solidity + vm.assume(amount > balanceOfSender); + vm.expectRevert(abi.encodeWithSelector(Token.InsufficientBalance.selector, sender)); + vm.prank(sender); + token.transfer(receiver, amount); + ``` + Note that like foundry, logs emitted by reverted subcalls are taken into account by `expectEmit`. + ### 2.4 Check output states After calling the target contracts, you can write assertions against the output state of the contracts. @@ -210,15 +217,17 @@ assert(token.balanceOf(sender) == balanceOfSender - amount); assert(token.balanceOf(receiver) == balanceOfReceiver + amount); ``` -If there are any inputs that violate these assertions, Halmos will reports those inputs, referred to as counterexamples. +If there are any inputs that violate these assertions, dolmos will report those inputs, referred to as counterexamples. -For our example, Halmos will identify an input combination where the sender address is identical to the receiver address. This is because self-transfers do not alter the balance, leading to scenarios where the above assertions are not satisfied. +For our example, dolmos will identify an input combination where the sender address is identical to the receiver address. This is because self-transfers do not alter the balance, leading to scenarios where the above assertions are not satisfied. **Tips:** -- Halmos focuses solely on assertion violations (i.e., revert with `Panic(1)`), disregarding other revert cases. This means that Halmos doesn't report any inputs that lead to other types of revert. For instance, in our example, any inputs that trigger an overflow in `balanceOfReceiver + amount`, or inputs causing the external contract call to fail will be ignored. To avoid disregarding such inputs, you can utilize an `unchecked` block or a low-level call. +- Run with `--pretty-counterexamples` (`-pcex`) to get counterexamples decoded with the ABI (arguments, calldata, selectors, invariant call sequences), without duplicates, and with a forge test that replays each of them. See [pretty counterexamples](pretty-counterexamples.md). + +- Dolmos focuses solely on assertion violations (i.e., revert with `Panic(1)`), disregarding other revert cases. This means that dolmos doesn't report any inputs that lead to other types of revert. For instance, in our example, any inputs that trigger an overflow in `balanceOfReceiver + amount`, or inputs causing the external contract call to fail will be ignored. To avoid disregarding such inputs, you can utilize an `unchecked` block or a low-level call. -- If you're using an older compiler version (`< 0.8.0`) that uses the `INVALID` opcode for assertion violation, rather than the `Panic(1)` error code, then Halmos will _not_ report any counterexamples. In that case, you will need to use a custom assertion that reverts with `Panic(1)` upon failure, as shown below: +- If you're using an older compiler version (`< 0.8.0`) that uses the `INVALID` opcode for assertion violation, rather than the `Panic(1)` error code, then dolmos will _not_ report any counterexamples by default. In that case, run with `--invalid-as-failure` (the default when the build contains Vyper contracts), or use a custom assertion that reverts with `Panic(1)` upon failure, as shown below: ```solidity function myAssert(bool cond) internal pure { if (!cond) { @@ -245,7 +254,3 @@ However, since symbolic tests are performed symbolically, certain behavioral dif - The `vm.assume()` cheatcode performs better than `bound()`. For further insights, refer to [examples of symbolic tests](../examples/README.md). - -Join the [Halmos Telegram Group] for any inquiries or further discussions. - -[Halmos Telegram Group]: diff --git a/docs/loop-termination.md b/docs/loop-termination.md new file mode 100644 index 000000000..0668a1e3f --- /dev/null +++ b/docs/loop-termination.md @@ -0,0 +1,217 @@ +# Loop termination analysis with PaSTTeL (experimental) + +dolmos explores loops by unrolling them up to a bound (`--loop`, 2 by default). When a +path would need more iterations, it is dropped and the test reports +`bounds: [...]`: the exploration is incomplete, and nothing is known about the loop +itself. + +With `--dump-lassos`, every loop that reaches the unrolling bound is exported as a +*lasso program*, which [PaSTTeL](https://github.com/Dowsers/PaSTTeL) can analyse to +prove termination (with a ranking function) or non-termination. + +- [Usage](#usage) +- [Reading the results](#reading-the-results) +- [How a loop becomes a lasso](#how-a-loop-becomes-a-lasso) +- [From bitvectors to integers](#from-bitvectors-to-integers) +- [The small-constants encoding (PaSTTeL workaround)](#the-small-constants-encoding-pasttel-workaround) +- [Limitations](#limitations) + +## Usage + +```bash +# export the lassos only +dolmos --dump-lassos lassos/ + +# export and analyse them +dolmos --dump-lassos lassos/ --pasttel /path/to/pasttel [--pasttel-timeout 30] +``` + +| Option | Description | +|---|---| +| `--dump-lassos DIR` | export each loop that reaches the unrolling bound to `DIR` | +| `--pasttel BINARY` | run PaSTTeL on each exported lasso and report the verdict | +| `--pasttel-timeout SECONDS` | time limit per PaSTTeL run (default: 30) | +| `--lasso-exact-constants` | exact wrap-around encoding with 2^256 constants, for tools with exact arithmetic (not PaSTTeL, see below) | + +The option has no effect on the test results: the extraction runs on a separate +solver, and a failed extraction is reported without affecting the test. + +For each loop, three files are written: + +- `__.json`: the lasso, in PaSTTeL's JSON trace format +- `__.meta.json`: which stack slots the program variables + `v0, v1, ...` stand for, the number of body paths, the encoding, and warnings +- `__.pasttel.txt`: PaSTTeL's output (with `--pasttel`) + +and a line is printed after the test result: + +``` +[PASS] check_count_down(uint256) (paths: 5, time: 0.15s, bounds: []) + loop 2129:473 (false branch): TERMINATING [RankingBased(AffineTemplate): v0] -> lassos/check_count_down_2129_473_f.json +``` + +## Reading the results + +- **TERMINATING**, with a ranking function: the loop terminates. This result is + reliable: the lasso over-approximates the behaviours of the loop, and a proof for + more behaviours is a proof for the actual ones. +- **NON-TERMINATING**: PaSTTeL found an infinite execution *of the lasso*. If the lasso + is exact (`"exact": true` in the metadata), the witness is an infinite execution of + the loop. Otherwise the verdict is printed as *unconfirmed*: the witness may rely on + behaviours that the over-approximation introduced. +- **UNKNOWN / TIMEOUT**: no conclusion. +- **Warnings**: + - `storage written in the loop body`: only stack variables are tracked (see + [Limitations](#limitations)). If the loop condition depends on a storage slot + written in the body, the result is not reliable, including a TERMINATING verdict. + - `body path not explored`, `too many body paths`, `step budget exhausted`: the + extraction is incomplete; the result is only indicative. + +## How a loop becomes a lasso + +A lasso is a *stem* (how the execution reaches the loop) followed by a *loop* +transition that repeats forever. dolmos builds both from the symbolic execution: + +1. **Loop variables.** At each visit of a symbolic `JUMPI`, the stack is recorded. + When the unrolling bound is reached, the stack slots that differ from the previous + visit are the loop variables. +2. **Cut point.** The lasso is cut right after the `JUMPI`, on the branch that + stays in the loop. The bound is often reached on a `JUMPI` inside an internal + function that solc generates (e.g. checked arithmetic): any point of the cycle is + a valid cut point, but it must be identified precisely. Like the unrolling + counters, dolmos uses the program counter and the jump destinations on the stack, + plus the stack height to tell apart the call sites of the same internal function. +3. **Generalized iteration.** The loop body is executed once more from a state where + the loop variables are fresh symbols, until the execution is back at the cut + point in the same frame. Each path that comes back *and takes the loop branch + again* is a disjunct of the loop transition. This execution runs on a separate + solver, with its own step budget. +4. **Stem.** The path condition up to the cut point, sliced to the conditions that + relate to the initial values of the loop variables. + +Subterms that don't depend on the loop variables (inputs, values read before the +loop) become constant program variables, shared by the stem and the loop: without +them, `for (i = 0; i < n; i++)` could not be proven, as `n` would change at every +iteration. + +## From bitvectors to integers + +EVM words are 256-bit bitvectors; PaSTTeL works on integers. Every w-bit value +becomes an integer `x` with `0 <= x`, and: + +| Bitvector | Integer encoding | +|---|---| +| `bvadd`, `bvsub`, `bvneg`, `bvmul`/`bvshl` by a constant | exact, with the wrap-around made explicit (see below) | +| `bvudiv`, `bvurem`, `bvlshr` by a constant, `extract`, `concat`, `zero_extend` | exact, with a quotient `q` such that `c*q <= a <= c*q + c - 1` | +| unsigned comparisons, boolean connectives | exact | +| `ite` | a fresh variable and a disjunction (PaSTTeL doesn't parse arithmetic `ite`) | +| anything else (keccak, storage and memory reads, bitwise operations, nonlinear arithmetic...) | a fresh variable: over-approximation | + +## The small-constants encoding (PaSTTeL workaround) + +### The problem + +The natural encoding of a wrap-around is `r = e - 2^256 * k`. It needs 2^256 +constants, and PaSTTeL cannot represent them: it parses and stores numbers as C++ +`double` (`std::stod` in its SMT parser, `double` coefficients in `AffineTerm`), +which are exact for integers up to 2^53 only. 2^256 and 2^256 - 1 become the same +number, and the analysis becomes unsound. In our experiments, PaSTTeL reported a +simple countdown loop as non-terminating, with a witness that is impossible even over +the rationals; it also produced ranking functions with coefficients equal to +`DBL_MAX`, and, worse, a termination proof for a loop that does not terminate (see +[Results](#results)). + +(A second, independent issue: ranking function synthesis works over the rationals. +With a free integer `k`, a fractional `k` allows any result, so the encoding +`r = e - 2^256 * k` loses all precision even with exact arithmetic. The exact +encoding therefore uses one disjunct per possible value of `k`.) + +The proper fix is exact rational arithmetic in PaSTTeL. Until then, dolmos produces +lassos without large constants: this is the default encoding. + +### The encoding + +No literal in the lasso exceeds 2^52 (this is checked before writing the file). + +1. **Wrap-arounds are proven absent when possible.** For each addition, subtraction + or multiplication by a constant, dolmos asks z3, with the bitvector semantics, + whether the operation can wrap around on the path. If it cannot, the result is + the plain integer expression (`x + 1`, `x - 1`), which is exact. + - With checked arithmetic (Solidity >= 0.8), the overflow checks are on the path, + so the proof usually succeeds. + - `x - 1` is compiled as `x + (2^256 - 1)`: an addition of a constant `C >= + 2^255` is handled as a subtraction of `2^256 - C`, with the borrow condition + `x >= 1`. +2. **The prover knows how the iteration was entered.** An increment `i + 1` only + wraps around if `i = 2^256 - 1`, which is excluded by the loop condition `i < n` + checked *before* the iteration, i.e. at the end of the previous one. The prover is + given this fact, as a disjunction over the body paths with renamed variables. It + is valid because the unrolling bound was reached (so there was a previous + iteration), and only used when the body paths are complete. +3. **Facts about the inputs are used.** The path conditions of the stem are about + input symbols, which never change: they hold at every iteration. For instance, + `vm.assume(n < 1000)` lets the prover show that `i += 3` doesn't wrap while + `i < n`. +4. **Otherwise, a sound over-approximation without large constants:** + - addition, multiplication (the result can only wrap downwards): `0 <= r <= e` + - subtraction (the result can only wrap upwards): + `(e >= 0 and r = e) or e < 0`, where `r` is unconstrained in the second case + - truncation (`extract`, masks): same as addition + - division or remainder by a large constant: `0 <= q <= a` +5. **Large literals become constant program variables** (`c0, c1, ...`), constrained + by their order (`0 <= c0 < c1 < ...`): comparisons such as `x < 2^200` keep their + structure. +6. **Upper bounds `x < 2^256` are dropped** (only `0 <= x` is kept): an + over-approximation. +7. **Signed comparisons** are exact when both operands are provably below 2^255 + (then they are unsigned comparisons); otherwise they are over-approximated. + +The metadata records the encoding and whether the lasso is exact +(`"exact": false` as soon as one over-approximation was used). + +### Results + +On a set of test loops (countdown, count-up, `unchecked` step of 3, loops leaving +through a wrap-around): + +| Loop | exact encoding (`--lasso-exact-constants`) | small-constants encoding (default) | +|---|---|---| +| `while (x > 0) x -= 1;` | TERMINATING, coefficients ~2^251 (unreliable) | TERMINATING, rank `v0` | +| `for (i = 0; i < n; i++) s += 1;` | TERMINATING, huge coefficients (unreliable) | TERMINATING, rank `5·k0 + v0 − 3·v1 − 3` | +| `while (i < n) unchecked { i += 3; }` (`n < 1000`) | TERMINATING, huge coefficients (unreliable) | TERMINATING, rank `8·k0 − 2·v0 − 27` | +| `while (x != 0) { unchecked { x -= 2; } if (x > 1000) break; }` | TERMINATING, rank `10·v0 − 1` | TERMINATING, rank `10·v0 + 19` | +| `while (x != 0) unchecked { x -= 2; }` (non-terminating for odd `x`) | **TERMINATING (wrong)** | NON-TERMINATING, unconfirmed (correct) | + +The fourth loop terminates: for odd `x`, `x - 2` eventually wraps around to +`2^256 - 1 > 1000`. An earlier version of the extraction, with the exact encoding, +reported it and the countdown loop as non-terminating. + +On the regression suite, the 20 loops reaching the bound are all extracted; the +test results are unchanged. + +### Exact encoding + +`--lasso-exact-constants` produces the exact encoding (2^256 constants, one +disjunct per wrap-around case). It is meant for termination tools with exact +arithmetic; with the current PaSTTeL, its results are unreliable. + +## Limitations + +- **Only stack variables are tracked.** Storage and memory are not generalized: + values read from them are either constants (if they don't depend on the loop + variables) or fresh values. Loops whose body writes to storage are flagged. + Loops that index memory with the loop counter (`arr[i]` on a memory array) often + cannot be extracted, as dolmos doesn't support symbolic memory offsets. +- **Non-termination is not confirmed.** A NON-TERMINATING verdict on an + over-approximated lasso would need to be replayed with the bitvector semantics; + this is not implemented yet. +- **Loops whose condition becomes constant are not exported.** dolmos only applies + the unrolling bound to loops whose condition is symbolic. A loop that makes no + progress, like `while (x > y) {}`, has a condition that becomes known after the + first iteration: dolmos keeps unrolling it forever, and the bound, hence the export, + is never reached. This is an existing dolmos limitation. +- **One cut point per loop and branch** is exported per test; the lasso describes + the loop from that point, with the paths found from the state where the bound was + reached. +- The ranking function proves termination, but it is not used yet to raise the + unrolling bound of the loop. diff --git a/docs/pretty-counterexamples.md b/docs/pretty-counterexamples.md new file mode 100644 index 000000000..cbda2ef4d --- /dev/null +++ b/docs/pretty-counterexamples.md @@ -0,0 +1,140 @@ +# Pretty counterexamples + +By default, a counterexample is printed as the raw solver model: one line per symbol, with +the full hexadecimal value of every word. A `bytes` argument of length 65 is printed as the +1024 bytes of its largest length candidate, a `bytes4` selector as `0x00`, and the same +values are repeated for every failing path. + +`--pretty-counterexamples` (short: `-pcex`) prints counterexamples that can be acted upon: + +``` +dolmos -pcex +``` + +It can also be set in `dolmos.toml` (`pretty-counterexamples = true`), or for a contract or +a function with `/// @custom:dolmos --pretty-counterexamples`. The verdicts of the tests +and the JSON output are the same as without the option, except for counterexamples that +are proven spurious (see [Potentially invalid counterexamples](#potentially-invalid-counterexamples)). + +## What it changes + +- **Arguments decoded with the ABI of the test.** The lengths of dynamic arrays, `bytes` and + `string` are applied, and values are printed by type: decimal integers (with a readable + form such as `1e18`, `2**255` or `type(uint256).max` when there is one), checksummed + addresses (with the contract deployed there and the state variable of the test holding + it), quoted strings, `true`/`false`. Structs and arrays are flattened to one line per + value (`p.a = 7`, `calls[1] = …`). +- **Calldata decoded** (halmos#369). `bytes` values whose first 4 bytes are the selector of a + function of a compiled contract are decoded with its ABI, e.g. + `Token.transfer(to: 0x…, amount: 2) + 956 trailing zero bytes`. Calls made by the test + with calldata built from other symbols (e.g. by `svm.createCalldata`) are listed under + `Calls made with symbolic calldata`. +- **Selectors** (halmos#419). `bytes4` values are printed with the function they select, and + `0x00000000` as the empty selector of plain ether transfers (`receive()` or + `fallback()`), unless some contract has a function with that selector. +- **Invariant call sequences with concrete values**: target, decoded arguments, `msg.sender`, + `msg.value`, `tx.origin` and `block.timestamp` of each call. The symbolic trace is still + printed with `-vv`. +- **A forge test replaying the counterexample**, to paste into the test contract. It fails + if the counterexample is real. +- **Duplicates hidden** (halmos#398). A counterexample with the same values as one already + printed for the test is counted but not printed; the number of hidden duplicates is + printed after the result of the test. `--early-exit` stops at the first valid + counterexample. +- **Potentially invalid counterexamples are checked**, and the reason is printed when they + remain potentially invalid (halmos#280), see below. + +## Example + +From `tests/regression/test/PrettyCex.t.sol`: + +```solidity +function check_pcex_calldata(bytes calldata data) external { + (bool ok,) = address(token).call(data); + assert(!ok || token.balanceOf(address(this)) == 1000); +} +``` + +Without the option, the counterexample is the 2048 hex digits of `data` (its largest length +candidate) and the length symbol. With it: + +``` +Counterexample: check_pcex_calldata(bytes) + data = PcexToken.transfer(to: 0x0000000000000000000000000000000000000000, amount: 512) + 956 trailing zero bytes + 0xa9059cbb000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002 + 957 zero bytes (1024 bytes) +Reproduce: add to PrettyCexTest (test/PrettyCex.t.sol), then `forge test --mt test_pcex_check_pcex_calldata_1 -vvvv` (the test fails if the counterexample is real) + function test_pcex_check_pcex_calldata_1() public { + this.check_pcex_calldata(abi.encodePacked(hex"a9059cbb000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002", new bytes(957))); + } +``` + +For an invariant test, the call sequence is printed with concrete values: + +``` +Counterexample: invariant_pcex_balance() + Sequence: + [1] PcexToken(token).transfer(to: 0xFFA9385be102ac3EAc297483Dd6233d62b3e1496, amount: 492) + msg.sender: 0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496 (PrettyCexTest), tx.origin: 0x0000000000000000000000000000000000000000 + then invariant_pcex_balance() at block.timestamp: 9223372036854775808 +Reproduce: add to PrettyCexTest (test/PrettyCex.t.sol), then `forge test --mt test_pcex_invariant_pcex_balance_1 -vvvv` (the test fails if the counterexample is real) + function test_pcex_invariant_pcex_balance_1() public { + vm.prank(0x7FA9385bE102ac3EAc297483Dd6233D62b3e1496, address(0)); + token.transfer(0xFFA9385be102ac3EAc297483Dd6233d62b3e1496, 492); + vm.warp(9223372036854775808); + this.invariant_pcex_balance(); + } +``` + +## Reproduction tests + +The generated function calls the test function through `this`, with the values of the +counterexample. When the arguments cannot be written as Solidity literals (a value that is +not a valid ABI encoding of its type, e.g. a `uint8` above 255, or an overloaded test +function), it replays the exact calldata with a low-level call instead. + +Invariant sequences are replayed with `vm.prank`, `vm.deal` and `vm.warp`. A target is +called through the state variable of the test that holds it (`vault.deposit(…)`), so that +the call goes to the instance deployed by forge. Dolmos deploys contracts at its own +addresses (`0xaaaa…`, `0xcccc…`), so a target that is not held by a state variable of the +test is called at the dolmos address, with a note to replace it. + +Values that the test creates itself with `svm.create*` cheatcodes (and the calldata it +builds with `svm.createCalldata`) cannot be injected: they are listed as comments at the +top of the function, to replace the cheatcodes with. + +## Potentially invalid counterexamples + +Dolmos approximates some operations with uninterpreted functions, so a model may rely on +values that the real operation never produces. Such counterexamples are reported as +*potentially invalid*. Without the option, the reason is not given (halmos#280). + +With the option, the operands and the result of every exponentiation that dolmos +approximates (`x ** y` with a symbolic exponent, or with a symbolic base and a constant +exponent above `--smt-exp-by-const`) are compared with the real `**`: + +- if they agree, the counterexample is valid; +- otherwise the query is solved again with facts that hold for the real `**`: constant + exponents are expanded by square and multiply, constant bases are tabulated (exactly for + an even base), and the real value is added at the operands chosen by the model. Every + real counterexample is kept, so `unsat` proves that there is none, and the test passes. + This is repeated up to 3 times, plus `--keccak-refinement-rounds` times for the keccak + values checked in the same loop. + +For example, `assert(x ** 3 != 27)` gives a potentially invalid counterexample `x = 8` +without the option, and the valid counterexample `x = 3` with it. When the model still +disagrees, the reason is printed: + +```solidity +function check_pow(uint256 x, uint256 y) external pure { + vm.assume(x % 2 == 0 && y > 0); + assert(x ** y != 3); +} +``` + +``` +Counterexample (potentially invalid): check_pow(uint256,uint256) + reason: EXP is approximated: x ** y (symbolic base and exponent): the model takes 10 ** 16 = 3 instead of 10000000000000000 (constrain the operands with vm.assume (e.g. exponent < 256) or make the base or the exponent constant) + x = 10 + y = 16 +(see https://github.com/Dowsers/dolmos/blob/main/docs/warnings.md#counterexample-invalid) +``` diff --git a/docs/warnings.md b/docs/warnings.md new file mode 100644 index 000000000..1617beda5 --- /dev/null +++ b/docs/warnings.md @@ -0,0 +1,64 @@ +# Warnings + +Each warning printed by dolmos ends with a link to its section below. + +## parsing-error + +A build artifact in the forge output directory could not be parsed and was +skipped, so the contracts it defines are neither tested nor available to +`vm.getCode`/`deployCode`. Rebuild with `forge build --force`; if the artifact +comes from an unusual compiler setup, run with `--debug` to see the full error. + +## internal-error + +Symbolic execution hit a case dolmos does not handle, or a cheatcode was used +in a way it does not support (for instance `vm.ffi` without `--ffi`). The +affected path is dropped, so the result of the test may be incomplete. Run with +`--debug` for details, and report it if the input looks legitimate. + +## library-placeholder + +The bytecode still contains unlinked library placeholders (`__$...$__`). Only +libraries compiled in the same build can be linked; deploy or link external +libraries explicitly in `setUp()`. + +## counterexample-invalid + +The solver produced a model for a failing path, but replaying it did not +reproduce the failure. This usually comes from approximations in the symbolic +model (hash functions, unbounded arrays, precompiles). The test is still +reported as failing; inspect the counterexample before trusting it. + +With `--pretty-counterexamples`, counterexamples relying on the approximation of +exponentiation are checked against the real `**` (and replaced by a valid +counterexample, or proven spurious, when possible), and the reason is printed when +they remain potentially invalid, e.g. a symbolic base and exponent, or keccak256 +values that differ from the real hash function. See +[pretty counterexamples](pretty-counterexamples.md#potentially-invalid-counterexamples). + +## counterexample-unknown + +The solver could not decide whether a failing path is feasible within +`--solver-timeout-assertion`. The test is reported as a timeout rather than a +pass. Increase the timeout, try another `--solver`, or reduce the input space +with `vm.assume` and smaller `--array-lengths`. + +## unsupported-opcode + +An opcode dolmos does not implement was executed; the path is dropped. + +## revert-all + +Every path of the test reverted, so nothing was actually checked. Typical +causes: `vm.assume` conditions that can never hold, a `setUp()` state that makes +the target always revert, or input bounds that are too tight. + +## loop-bound + +Some paths were cut at the loop unrolling bound (`--loop`), so they have not +been fully explored and bugs beyond that bound can be missed. Raise `--loop` +(globally or with a `@custom:dolmos --loop N` annotation) if the loops in +question are bounded by a small constant. + +To find out whether these loops terminate, export them with `--dump-lassos` and +analyse them with PaSTTeL: see [loop-termination.md](loop-termination.md). diff --git a/examples/README.md b/examples/README.md index 885695939..7187f7171 100644 --- a/examples/README.md +++ b/examples/README.md @@ -1,4 +1,4 @@ -# Halmos Examples +# Dolmos Examples #### Usage Examples @@ -8,7 +8,12 @@ - Includes identifying the DEI token bug exploited in the [Deus DAO hack](https://rekt.news/deus-dao-r3kt/). - [ERC721](tokens/ERC721/test/): verifies OpenZeppelin, Solady, and Solmate ERC721 tokens. -#### Halmos Tests in External Projects +#### Symbolic Tests in External Projects + +These suites were written for halmos; thanks to dolmos' compatibility with +`@custom:halmos` annotations and `halmos.toml` they should run with dolmos as +they are. + - [Morpho Blue] ([HalmosTest]): verifies the Morpho Blue protocol. - [Farcaster] ([IdRegistrySymTest], [KeyRegistrySymTest]): verifies state machine invariants in Farcaster's onchain registry contracts. @@ -36,4 +41,10 @@ ## Disclaimer -_These smart contracts and code are being provided as is. No guarantee, representation or warranty is being made, express or implied, as to the safety or correctness of the user interface or the smart contracts and code. They have not been audited and as such there can be no assurance they will work as intended, and users may experience delays, failures, errors, omissions or loss of transmitted information. THE SMART CONTRACTS AND CODE CONTAINED HEREIN ARE FURNISHED AS IS, WHERE IS, WITH ALL FAULTS AND WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING ANY WARRANTY OF MERCHANTABILITY, NON-INFRINGEMENT OR FITNESS FOR ANY PARTICULAR PURPOSE. Further, use of any of these smart contracts and code may be restricted or prohibited under applicable law, including securities laws, and it is therefore strongly advised for you to contact a reputable attorney in any jurisdiction where these smart contracts and code may be accessible for any questions or concerns with respect thereto. Further, no information provided in this repo should be construed as investment advice or legal advice for any particular facts or circumstances, and is not meant to replace competent counsel. a16z is not liable for any use of the foregoing, and users should proceed with caution and use at their own risk. See a16z.com/disclosures for more info._ +_This software and the smart contracts in this repository are provided as is, +without warranty of any kind, express or implied, including any warranty of +merchantability, non-infringement or fitness for a particular purpose. They have +not been audited. Passing symbolic tests is not a proof that a contract is free +of bugs. Nothing in this repository is investment or legal advice. See +[NOTICE](../NOTICE) for the disclaimers attached to the original work this code is +derived from._ diff --git a/examples/invariants/README.md b/examples/invariants/README.md index 21f0a1a70..823bc9ca7 100644 --- a/examples/invariants/README.md +++ b/examples/invariants/README.md @@ -1,6 +1,6 @@ -# Halmos Invariant Testing Examples +# Dolmos Invariant Testing Examples -This directory contains examples demonstrating various approaches to invariant testing with halmos. +This directory contains examples demonstrating various approaches to invariant testing with dolmos. ## Examples @@ -8,13 +8,13 @@ This directory contains examples demonstrating various approaches to invariant t - **ERC721 Test** ([`ERC721.t.sol`](test/ERC721.t.sol)): Simple ERC721 invariant testing without handlers. Demonstrates how straightforward invariant testing can be when state tracking isn't needed. -- **MiniVat Test** ([`MiniVat.t.sol`](test/MiniVat.t.sol)): Halmos version of [Antonio's MiniVat test](https://github.com/aviggiano/property-based-testing-benchmark/blob/main/projects/dai-certora/test/TargetFunctions.sol). Unlike other fuzzers, no bounds are needed, so no handlers are required. Simply deploy the contract and write the invariant. +- **MiniVat Test** ([`MiniVat.t.sol`](test/MiniVat.t.sol)): dolmos version of [Antonio's MiniVat test](https://github.com/aviggiano/property-based-testing-benchmark/blob/main/projects/dai-certora/test/TargetFunctions.sol). Unlike other fuzzers, no bounds are needed, so no handlers are required. Simply deploy the contract and write the invariant. - **Vat Test** ([`Vat.t.sol`](test/Vat.t.sol)): Tests the full Vat contract using the same invariant as MiniVat. It is more comprehensive and takes longer to run. -- **SimpleState Test** ([`SimpleState.t.sol`](test/SimpleState.t.sol)): Example from the [ItyFuzz paper](https://arxiv.org/pdf/2306.17135) that's hard to detect with simple random testing. Halmos uses exhaustive search and considers only unique state-generating call sequences for efficient space exploration. +- **SimpleState Test** ([`SimpleState.t.sol`](test/SimpleState.t.sol)): Example from the [ItyFuzz paper](https://arxiv.org/pdf/2306.17135) that's hard to detect with simple random testing. Dolmos uses exhaustive search and considers only unique state-generating call sequences for efficient space exploration. -- **Reentrancy Test** ([`Reentrancy.t.sol`](test/Reentrancy.t.sol)): Shows how to detect reentrancy exploits using halmos invariant testing. Demonstrates attacker contract implementation using [halmos cheatcodes](https://github.com/a16z/halmos-cheatcodes). +- **Reentrancy Test** ([`Reentrancy.t.sol`](test/Reentrancy.t.sol)): Shows how to detect reentrancy exploits using dolmos invariant testing. Demonstrates attacker contract implementation using the [halmos-cheatcodes](https://github.com/a16z/halmos-cheatcodes) library. ## Running Tests @@ -22,11 +22,11 @@ This directory contains examples demonstrating various approaches to invariant t cd examples/invariants # Run all invariant tests -halmos +dolmos # Run specific test -halmos --contract ERC20Test +dolmos --contract ERC20Test # Run specific invariant -halmos --function invariant_sumOfBalancesEqualsTotalSupply +dolmos --function invariant_sumOfBalancesEqualsTotalSupply ``` diff --git a/examples/invariants/test/ERC20.t.sol b/examples/invariants/test/ERC20.t.sol index 577c320ba..1ed5e43f9 100644 --- a/examples/invariants/test/ERC20.t.sol +++ b/examples/invariants/test/ERC20.t.sol @@ -6,7 +6,7 @@ pragma solidity >=0.8.0 <0.9.0; import {ERC20} from "../src/ERC20.sol"; import {Test} from "forge-std/Test.sol"; -/// @custom:halmos --solver bitwuzla-abs --loop 3 --solver-timeout-assertion 0 +/// @custom:dolmos --solver bitwuzla-abs --loop 3 --solver-timeout-assertion 0 contract ERC20Test is Test { // token address ERC20 internal token; diff --git a/examples/invariants/test/ERC721.t.sol b/examples/invariants/test/ERC721.t.sol index e892be540..55835a4b5 100644 --- a/examples/invariants/test/ERC721.t.sol +++ b/examples/invariants/test/ERC721.t.sol @@ -4,7 +4,7 @@ pragma solidity >=0.8.0 <0.9.0; import {ERC721} from "../src/ERC721.sol"; import {Test} from "forge-std/Test.sol"; -/// @custom:halmos --solver bitwuzla-abs --solver-timeout-assertion 0 +/// @custom:dolmos --solver bitwuzla-abs --solver-timeout-assertion 0 contract ERC721Test is Test { // ERC721 token address ERC721 internal token; diff --git a/examples/invariants/test/MiniVat.t.sol b/examples/invariants/test/MiniVat.t.sol index 86aca9231..431d92645 100644 --- a/examples/invariants/test/MiniVat.t.sol +++ b/examples/invariants/test/MiniVat.t.sol @@ -7,7 +7,7 @@ import "forge-std/Test.sol"; import {MiniVat} from "../src/MiniVat.sol"; -/// @custom:halmos --early-exit +/// @custom:dolmos --early-exit contract MiniVatTest is Test { MiniVat public minivat; diff --git a/examples/invariants/test/Reentrancy.t.sol b/examples/invariants/test/Reentrancy.t.sol index 171bc281d..adf819f0c 100644 --- a/examples/invariants/test/Reentrancy.t.sol +++ b/examples/invariants/test/Reentrancy.t.sol @@ -68,7 +68,7 @@ contract Attacker is SymTest, Test { } } -/// @custom:halmos --early-exit +/// @custom:dolmos --early-exit contract ReentrancyTest is Test, ERC1155Holder { ERC1155Mock token; BuggyVault vault; diff --git a/examples/invariants/test/SimpleState.t.sol b/examples/invariants/test/SimpleState.t.sol index bb96d8430..47eabb208 100644 --- a/examples/invariants/test/SimpleState.t.sol +++ b/examples/invariants/test/SimpleState.t.sol @@ -30,7 +30,7 @@ contract SimpleStateTest is Test { target = new SimpleState(); } - /// @custom:halmos --invariant-depth 10 + /// @custom:dolmos --invariant-depth 10 function invariant_buggy() public view { assertFalse(target.buggy()); } diff --git a/examples/invariants/test/Vat.t.sol b/examples/invariants/test/Vat.t.sol index a9ae8aaff..530dd81b0 100644 --- a/examples/invariants/test/Vat.t.sol +++ b/examples/invariants/test/Vat.t.sol @@ -5,7 +5,7 @@ import "forge-std/Test.sol"; import {Vat} from "../src/Vat.sol"; -/// @custom:halmos --early-exit +/// @custom:dolmos --early-exit contract VatTest is Test { Vat public vat; bytes32 ilk; diff --git a/examples/simple/README.md b/examples/simple/README.md index 0ed140b14..10ce25b74 100644 --- a/examples/simple/README.md +++ b/examples/simple/README.md @@ -29,13 +29,19 @@ $ forge test Once it passes, you can also perform **symbolic testing** to verify the same properties for **all possible inputs** (up to a specified limit): ``` -$ halmos --function test +$ dolmos --function test [FAIL] testTotalPriceBuggy(uint96,uint32) (paths: 6, time: 0.10s, bounds: []) Counterexample: [p_price_uint96 = 39614081294025656978550816768, p_quantity_uint32 = 1073741824] ``` -_(In this specific example, Halmos discovered an input that violated the assertion, which was missed by the fuzzer!)_ +_(In this specific example, Dolmos discovered an input that violated the assertion, which was missed by the fuzzer!)_ ## Disclaimer -_These smart contracts and code are being provided as is. No guarantee, representation or warranty is being made, express or implied, as to the safety or correctness of the user interface or the smart contracts and code. They have not been audited and as such there can be no assurance they will work as intended, and users may experience delays, failures, errors, omissions or loss of transmitted information. THE SMART CONTRACTS AND CODE CONTAINED HEREIN ARE FURNISHED AS IS, WHERE IS, WITH ALL FAULTS AND WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING ANY WARRANTY OF MERCHANTABILITY, NON-INFRINGEMENT OR FITNESS FOR ANY PARTICULAR PURPOSE. Further, use of any of these smart contracts and code may be restricted or prohibited under applicable law, including securities laws, and it is therefore strongly advised for you to contact a reputable attorney in any jurisdiction where these smart contracts and code may be accessible for any questions or concerns with respect thereto. Further, no information provided in this repo should be construed as investment advice or legal advice for any particular facts or circumstances, and is not meant to replace competent counsel. a16z is not liable for any use of the foregoing, and users should proceed with caution and use at their own risk. See a16z.com/disclosures for more info._ +_This software and the smart contracts in this repository are provided as is, +without warranty of any kind, express or implied, including any warranty of +merchantability, non-infringement or fitness for a particular purpose. They have +not been audited. Passing symbolic tests is not a proof that a contract is free +of bugs. Nothing in this repository is investment or legal advice. See +[NOTICE](../../NOTICE) for the disclaimers attached to the original work this code is +derived from._ diff --git a/examples/simple/foundry.toml b/examples/simple/foundry.toml index f9e9259ff..40162b395 100644 --- a/examples/simple/foundry.toml +++ b/examples/simple/foundry.toml @@ -6,5 +6,5 @@ libs = ["../../tests/lib", 'lib'] evm_version = 'cancun' force = false -# compile options used by halmos (to prevent unnecessary recompilation when running forge test and halmos together) +# compile options used by dolmos (to prevent unnecessary recompilation when running forge test and dolmos together) extra_output = ["storageLayout", "metadata"] diff --git a/examples/simple/test/BadElections.t.sol b/examples/simple/test/BadElections.t.sol index 4bf89d969..24897f9cc 100644 --- a/examples/simple/test/BadElections.t.sol +++ b/examples/simple/test/BadElections.t.sol @@ -18,12 +18,12 @@ contract BadElectionsTest is SymTest, Test { /// /// Running 1 tests for test/BadElections.t.sol:BadElectionsTest /// Counterexample: - /// halmos_fakeSig_bytes_01 = 0x00000000000000000000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffff5d576e7357a4501ddfe92f46681b20a100 (65 bytes) + /// dolmos_fakeSig_bytes_01 = 0x00000000000000000000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffff5d576e7357a4501ddfe92f46681b20a100 (65 bytes) /// p_proposalId_uint256 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0) /// [FAIL] check_canNotVoteTwice(uint256) (paths: 7, time: 0.63s, bounds: []) /// /// the counterexample values are not meaningful, but examining the trace shows - /// that halmos found a signature s.t. the voter can vote twice on the same proposal, + /// that dolmos found a signature s.t. the voter can vote twice on the same proposal, /// and the final vote count is 2 function check_canNotVoteTwice(uint256 proposalId) public { // setup diff --git a/examples/simple/test/IsPowerOfTwo.t.sol b/examples/simple/test/IsPowerOfTwo.t.sol index 17e2ec573..b28820abc 100644 --- a/examples/simple/test/IsPowerOfTwo.t.sol +++ b/examples/simple/test/IsPowerOfTwo.t.sol @@ -3,7 +3,7 @@ pragma solidity >=0.8.0 <0.9.0; import "../src/IsPowerOfTwo.sol"; -/// @custom:halmos --solver-timeout-assertion 0 +/// @custom:dolmos --solver-timeout-assertion 0 contract IsPowerOfTwoTest { IsPowerOfTwo target; @@ -17,7 +17,7 @@ contract IsPowerOfTwoTest { assert(result1 == result2); } - /// @custom:halmos --loop 256 + /// @custom:dolmos --loop 256 function check_isPowerOfTwo(uint256 x) public view { bool result1 = target.isPowerOfTwo(x); bool result2 = false; @@ -30,7 +30,7 @@ contract IsPowerOfTwoTest { assert(result1 == result2); } - /// @custom:halmos --loop 256 + /// @custom:dolmos --loop 256 function check_eq_isPowerOfTwo_isPowerOfTwoIter(uint x) public view { bool result1 = target.isPowerOfTwo(x); bool result2 = target.isPowerOfTwoIter(x); diff --git a/examples/simple/test/TotalPrice.t.sol b/examples/simple/test/TotalPrice.t.sol index e1a6ed835..265b70637 100644 --- a/examples/simple/test/TotalPrice.t.sol +++ b/examples/simple/test/TotalPrice.t.sol @@ -3,7 +3,7 @@ pragma solidity >=0.8.0 <0.9.0; import "../src/TotalPrice.sol"; -/// @custom:halmos --solver-timeout-assertion 0 +/// @custom:dolmos --solver-timeout-assertion 0 contract TotalPriceTest { TotalPrice target; diff --git a/examples/simple/test/Vault.t.sol b/examples/simple/test/Vault.t.sol index d354ff10b..583b57941 100644 --- a/examples/simple/test/Vault.t.sol +++ b/examples/simple/test/Vault.t.sol @@ -15,7 +15,7 @@ contract VaultMock is Vault { } } -/// @custom:halmos --solver-timeout-assertion 0 +/// @custom:dolmos --solver-timeout-assertion 0 contract VaultTest is SymTest { VaultMock vault; @@ -27,7 +27,7 @@ contract VaultTest is SymTest { } /// need to set a timeout for this test, the solver can run for hours - /// @custom:halmos --solver-timeout-assertion 10000 + /// @custom:dolmos --solver-timeout-assertion 10000 function check_deposit(uint assets) public { uint A1 = vault.totalAssets(); uint S1 = vault.totalShares(); diff --git a/examples/tokens/ERC20/remappings.txt b/examples/tokens/ERC20/remappings.txt index acf3e02df..95f579e0b 100644 --- a/examples/tokens/ERC20/remappings.txt +++ b/examples/tokens/ERC20/remappings.txt @@ -1,2 +1,3 @@ openzeppelin/=../../../tests/lib/openzeppelin-contracts/contracts/ ds-test/=../../../tests/lib/forge-std/lib/ds-test/src/ +solady/=../../../tests/lib/solady/src/ diff --git a/examples/tokens/ERC20/test/BackdoorERC20.t.sol b/examples/tokens/ERC20/test/BackdoorERC20.t.sol index 439514862..b7a79867b 100644 --- a/examples/tokens/ERC20/test/BackdoorERC20.t.sol +++ b/examples/tokens/ERC20/test/BackdoorERC20.t.sol @@ -10,10 +10,10 @@ import {IERC20} from "forge-std/interfaces/IERC20.sol"; // empty interface interface IEmpty { } -/// @custom:halmos --solver-timeout-assertion 0 +/// @custom:dolmos --solver-timeout-assertion 0 contract BackdoorERC20Test is ERC20Test { - /// @custom:halmos --solver-timeout-branching 1000 + /// @custom:dolmos --solver-timeout-branching 1000 function setUp() public override { address deployer = address(0x1000); diff --git a/examples/tokens/ERC20/test/CurveTokenV3.t.sol b/examples/tokens/ERC20/test/CurveTokenV3.t.sol index c68645c39..037cb9d31 100644 --- a/examples/tokens/ERC20/test/CurveTokenV3.t.sol +++ b/examples/tokens/ERC20/test/CurveTokenV3.t.sol @@ -28,12 +28,12 @@ interface CurveTokenV3 { contract EmptyContract { } -/// @custom:halmos --storage-layout=generic --solver-timeout-assertion 0 +/// @custom:dolmos --storage-layout=generic --solver-timeout-assertion 0 contract CurveTokenV3Test is ERC20Test { CurveTokenV3 token_; address minter; - /// @custom:halmos --solver-timeout-branching 1000 + /// @custom:dolmos --solver-timeout-branching 1000 function setUp() public override { token = address(new EmptyContract()); // Source of Deployed Bytecode: https://etherscan.io/address/0x06325440D014e39736583c165C2963BA99fAf14E#code diff --git a/examples/tokens/ERC20/test/DEIStablecoin.t.sol b/examples/tokens/ERC20/test/DEIStablecoin.t.sol index 942f9ed0e..be29f5a0c 100644 --- a/examples/tokens/ERC20/test/DEIStablecoin.t.sol +++ b/examples/tokens/ERC20/test/DEIStablecoin.t.sol @@ -19,12 +19,12 @@ contract SymAccount is SymTest { } /// @notice This example shows how to find the DEI token bug exploited by the Deus DAO hack: https://rekt.news/deus-dao-r3kt/ -/// @custom:halmos --solver-timeout-assertion 0 +/// @custom:dolmos --solver-timeout-assertion 0 contract DEIStablecoinTest is ERC20Test { DEIStablecoin token_; address lossless; - /// @custom:halmos --solver-timeout-branching 1000 + /// @custom:dolmos --solver-timeout-branching 1000 function setUp() public override { token = address(new EmptyContract()); // Source of Deployed Bytecode: https://etherscan.io/address/0x63c28e2ff796e1480eb9ac8c3c55dcb9ae7b3df6#code diff --git a/examples/tokens/ERC20/test/OpenZeppelinERC20.t.sol b/examples/tokens/ERC20/test/OpenZeppelinERC20.t.sol index d21913e7b..dbdd4e771 100644 --- a/examples/tokens/ERC20/test/OpenZeppelinERC20.t.sol +++ b/examples/tokens/ERC20/test/OpenZeppelinERC20.t.sol @@ -5,10 +5,10 @@ import {ERC20Test} from "./ERC20Test.sol"; import {OpenZeppelinERC20} from "../src/OpenZeppelinERC20.sol"; -/// @custom:halmos --solver-timeout-assertion 0 +/// @custom:dolmos --solver-timeout-assertion 0 contract OpenZeppelinERC20Test is ERC20Test { - /// @custom:halmos --solver-timeout-branching 1000 + /// @custom:dolmos --solver-timeout-branching 1000 function setUp() public override { address deployer = address(0x1000); diff --git a/examples/tokens/ERC20/test/SoladyERC20.t.sol b/examples/tokens/ERC20/test/SoladyERC20.t.sol index 2c45da8c7..57d87064a 100644 --- a/examples/tokens/ERC20/test/SoladyERC20.t.sol +++ b/examples/tokens/ERC20/test/SoladyERC20.t.sol @@ -5,10 +5,10 @@ import {ERC20Test} from "./ERC20Test.sol"; import {SoladyERC20} from "../src/SoladyERC20.sol"; -/// @custom:halmos --storage-layout=generic --solver-timeout-assertion 0 +/// @custom:dolmos --storage-layout=generic --solver-timeout-assertion 0 contract SoladyERC20Test is ERC20Test { - /// @custom:halmos --solver-timeout-branching 1000 + /// @custom:dolmos --solver-timeout-branching 1000 function setUp() public override { address deployer = address(0x1000); diff --git a/examples/tokens/ERC20/test/SolmateERC20.t.sol b/examples/tokens/ERC20/test/SolmateERC20.t.sol index 6e64252ec..89d453c5c 100644 --- a/examples/tokens/ERC20/test/SolmateERC20.t.sol +++ b/examples/tokens/ERC20/test/SolmateERC20.t.sol @@ -5,10 +5,10 @@ import {ERC20Test} from "./ERC20Test.sol"; import {SolmateERC20} from "../src/SolmateERC20.sol"; -/// @custom:halmos --solver-timeout-assertion 0 +/// @custom:dolmos --solver-timeout-assertion 0 contract SolmateERC20Test is ERC20Test { - /// @custom:halmos --solver-timeout-branching 1000 + /// @custom:dolmos --solver-timeout-branching 1000 function setUp() public override { address deployer = address(0x1000); diff --git a/examples/tokens/ERC721/remappings.txt b/examples/tokens/ERC721/remappings.txt index acf3e02df..95f579e0b 100644 --- a/examples/tokens/ERC721/remappings.txt +++ b/examples/tokens/ERC721/remappings.txt @@ -1,2 +1,3 @@ openzeppelin/=../../../tests/lib/openzeppelin-contracts/contracts/ ds-test/=../../../tests/lib/forge-std/lib/ds-test/src/ +solady/=../../../tests/lib/solady/src/ diff --git a/examples/tokens/ERC721/test/OpenZeppelinERC721.t.sol b/examples/tokens/ERC721/test/OpenZeppelinERC721.t.sol index 868a274d4..26b9ed744 100644 --- a/examples/tokens/ERC721/test/OpenZeppelinERC721.t.sol +++ b/examples/tokens/ERC721/test/OpenZeppelinERC721.t.sol @@ -5,10 +5,10 @@ import {ERC721Test} from "./ERC721Test.sol"; import {OpenZeppelinERC721} from "../src/OpenZeppelinERC721.sol"; -/// @custom:halmos --solver-timeout-assertion 0 +/// @custom:dolmos --solver-timeout-assertion 0 contract OpenZeppelinERC721Test is ERC721Test { - /// @custom:halmos --solver-timeout-branching 1000 + /// @custom:dolmos --solver-timeout-branching 1000 function setUp() public override { deployer = address(0x1000); diff --git a/examples/tokens/ERC721/test/SoladyERC721.t.sol b/examples/tokens/ERC721/test/SoladyERC721.t.sol index c3241a5e1..72f62e26f 100644 --- a/examples/tokens/ERC721/test/SoladyERC721.t.sol +++ b/examples/tokens/ERC721/test/SoladyERC721.t.sol @@ -5,10 +5,10 @@ import {ERC721Test} from "./ERC721Test.sol"; import {SoladyERC721} from "../src/SoladyERC721.sol"; -/// @custom:halmos --storage-layout=generic --solver-timeout-assertion 0 +/// @custom:dolmos --storage-layout=generic --solver-timeout-assertion 0 contract SoladyERC721Test is ERC721Test { - /// @custom:halmos --solver-timeout-branching 1000 + /// @custom:dolmos --solver-timeout-branching 1000 function setUp() public override { deployer = address(0x1000); diff --git a/examples/tokens/ERC721/test/SolmateERC721.t.sol b/examples/tokens/ERC721/test/SolmateERC721.t.sol index 1ca6eb4f2..8e3f256e8 100644 --- a/examples/tokens/ERC721/test/SolmateERC721.t.sol +++ b/examples/tokens/ERC721/test/SolmateERC721.t.sol @@ -5,10 +5,10 @@ import {ERC721Test} from "./ERC721Test.sol"; import {SolmateERC721} from "../src/SolmateERC721.sol"; -/// @custom:halmos --solver-timeout-assertion 0 +/// @custom:dolmos --solver-timeout-assertion 0 contract SolmateERC721Test is ERC721Test { - /// @custom:halmos --solver-timeout-branching 1000 + /// @custom:dolmos --solver-timeout-branching 1000 function setUp() public override { deployer = address(0x1000); diff --git a/packages/halmos-builder/Dockerfile b/packages/dolmos-builder/Dockerfile similarity index 71% rename from packages/halmos-builder/Dockerfile rename to packages/dolmos-builder/Dockerfile index b62594684..3e957761a 100644 --- a/packages/halmos-builder/Dockerfile +++ b/packages/dolmos-builder/Dockerfile @@ -1,4 +1,4 @@ -FROM ghcr.io/a16z/solvers:latest +FROM ghcr.io/dowsers/solvers:latest RUN apt-get update && apt-get install --no-install-recommends -y \ git \ @@ -18,12 +18,14 @@ RUN mkdir -p /root/.foundry/bin /root/.foundry/share/man/man1 # Add foundry binaries to PATH ENV PATH="/root/.foundry/bin:${PATH}" -# Download and run foundryup +# Download foundryup and install a pinned foundry version, so that the images (and +# the CI jobs that use them) do not change behaviour when foundry releases +ARG FOUNDRY_VERSION=v1.8.3 RUN curl -sSf -L https://raw.githubusercontent.com/foundry-rs/foundry/master/foundryup/foundryup \ -o /root/.foundry/bin/foundryup && \ chmod +x /root/.foundry/bin/foundryup && \ - foundryup + foundryup --install ${FOUNDRY_VERSION} # Set a nicer prompt -ENV IMAGE_NAME=halmos-builder +ENV IMAGE_NAME=dolmos-builder RUN echo 'PS1="($IMAGE_NAME) \[\033[1;32m\]\u@\h \[\033[1;35m\]\w \$\[\033[0m\] "' >> /root/.bashrc diff --git a/packages/halmos/Dockerfile b/packages/dolmos/Dockerfile similarity index 62% rename from packages/halmos/Dockerfile rename to packages/dolmos/Dockerfile index 1a26a55d3..f92e76488 100644 --- a/packages/halmos/Dockerfile +++ b/packages/dolmos/Dockerfile @@ -1,36 +1,36 @@ -FROM ghcr.io/a16z/halmos-builder:latest +FROM ghcr.io/dowsers/dolmos-builder:latest # inspired by https://hynek.me/articles/docker-uv/ # - enable the virtual environment -# - install halmos and its dependencies in UV_PROJECT_ENVIRONMENT +# - install dolmos and its dependencies in UV_PROJECT_ENVIRONMENT # - enable bytecode compilation for faster startup -# - disable downloading any additional packages +# - use the python of the builder image (ubuntu 24.04 ships 3.12), never download one # - use copy mode for linking instead of symlinking (because we mount to /src temporarily) -ENV PATH="/halmos/bin:$PATH" \ - VIRTUAL_ENV='/halmos' \ - UV_PROJECT_ENVIRONMENT='/halmos' \ +ENV PATH="/dolmos/bin:$PATH" \ + VIRTUAL_ENV='/dolmos' \ + UV_PROJECT_ENVIRONMENT='/dolmos' \ UV_COMPILE_BYTECODE=1 \ - UV_PYTHON=python3.13 \ + UV_PYTHON=python3.12 \ UV_PYTHON_DOWNLOADS=never \ UV_LINK_MODE=copy -# Install halmos, assuming it is checked out in the current host directory +# Install dolmos, assuming it is checked out in the current host directory # we don't specify --frozen or --locked because we don't check in uv.lock RUN --mount=type=bind,source=../..,target=/src,readonly=false \ cd /src && \ uv sync --extra dev --no-editable # Set a nicer prompt -ENV IMAGE_NAME=halmos +ENV IMAGE_NAME=dolmos RUN echo 'PS1="($IMAGE_NAME) \[\033[1;32m\]\u@\h \[\033[1;35m\]\w \$\[\033[0m\] "' >> /root/.bashrc -# optional: print python version, site packages, and check that halmos can be imported +# optional: print python version, site packages, and check that dolmos can be imported RUN </dev/null | grep "not found" && \ + bitwuzla --version && z3 --version + # Install uv COPY --from=ghcr.io/astral-sh/uv:latest /uv /uvx /bin/ diff --git a/packages/solvers/README.md b/packages/solvers/README.md index c5d961ac3..609d29d85 100644 --- a/packages/solvers/README.md +++ b/packages/solvers/README.md @@ -6,10 +6,10 @@ A minimalist Docker image containing high-performance SMT solvers. ```sh # Step 1: Pull the image -docker pull ghcr.io/a16z/solvers:latest +docker pull ghcr.io/dowsers/solvers:latest # Step 2: Tag the image with a shorter name -docker tag ghcr.io/a16z/solvers:latest solvers +docker tag ghcr.io/dowsers/solvers:latest solvers # Step 3: Run the container using the shorter name, for solver in bitwuzla boolector cvc5 stp yices z3 ; do \ @@ -48,12 +48,12 @@ z3: 4.13.3 Everyone is welcome to contribute new solvers or new versions to the image via pull requests. If a solver is competitive at [SMT-COMP](https://smt-comp.github.io), it would be great to have it included in the image. -When possible, we prefer release binaries from an official source like the Github releases for the project to minimize the time it takes to build the image. If you're unsure about a particular solver or how to integrate it, consider reaching out on the [Halmos Dev Chat](https://t.me/+4UhzHduai3MzZmUx). +When possible, we prefer release binaries from an official source like the Github releases for the project to minimize the time it takes to build the image. Before opening the pull request, please test your changes by verifying: * that you can build the image locally -* that you can correctly invoke the solver as described in the [Quick Start](https://github.com/a16z/halmos/tree/main/packages/solvers#quick-start) section +* that you can correctly invoke the solver as described in the [Quick Start](#quick-start) section * update this README with the name, version and source of the solver Thank you in advance! diff --git a/pyproject.toml b/pyproject.toml index 69cb98a46..bfd9ebefc 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,24 +1,35 @@ [build-system] -requires = ["setuptools>=61.0", "setuptools_scm[toml]>=6.2"] +requires = ["setuptools>=77.0", "setuptools_scm[toml]>=8.0"] build-backend = "setuptools.build_meta" [tool.setuptools_scm] +# the version comes from the git tag (vX.Y.Z); a missing tag gives 0.1.devN [project] -name = "halmos" +name = "dolmos" description = "A symbolic testing tool for EVM smart contracts" readme = "README.md" +license = "AGPL-3.0-only" +license-files = ["LICENSE", "NOTICE"] +keywords = ["ethereum", "evm", "solidity", "vyper", "symbolic-execution", "formal-verification", "foundry"] +# dolmos is derived from other authors' work, see NOTICE authors = [ - { name="a16z crypto" }, + { name="Dowsers SAS" }, ] maintainers = [ - { name="Daejun Park" }, - { name="karmacoma " }, + { name="Dowsers SAS" }, ] classifiers = [ - "Programming Language :: Python :: 3", - "License :: OSI Approved :: GNU Affero General Public License v3", + "Development Status :: 4 - Beta", + "Environment :: Console", + "Intended Audience :: Developers", "Operating System :: OS Independent", + "Programming Language :: Python :: 3", + "Programming Language :: Python :: 3.11", + "Programming Language :: Python :: 3.12", + "Programming Language :: Python :: 3.13", + "Topic :: Security", + "Topic :: Software Development :: Testing", ] requires-python = ">=3.11" dependencies = [ @@ -36,10 +47,13 @@ dependencies = [ dynamic = ["version"] [project.scripts] -halmos = "halmos.__main__:main" +dolmos = "dolmos.__main__:main" [project.urls] -"Homepage" = "https://github.com/a16z/halmos" +"Homepage" = "https://github.com/Dowsers/dolmos" +"Documentation" = "https://github.com/Dowsers/dolmos/blob/main/docs/getting-started.md" +"Issues" = "https://github.com/Dowsers/dolmos/issues" +"Changelog" = "https://github.com/Dowsers/dolmos/blob/main/CHANGELOG.md" # development dependencies, can be installed with # uv sync --extra dev @@ -50,6 +64,7 @@ halmos = "halmos.__main__:main" dev = [ "pre-commit>=4.0.1", "pytest>=8.3.4", + "pytest-github-actions-annotate-failures>=0.3.0", "ruff>=0.8.1", ] diff --git a/specification.md b/specification.md new file mode 100644 index 000000000..d6463d515 --- /dev/null +++ b/specification.md @@ -0,0 +1,36 @@ + + +# Modeling choices # + +## CLZ operator ## + + +## Self Destruct ## + +## Keccak256 256 operator ## + +Simplified explanation + +Dolmos models keccak256 using a family of uninterpreted functions, f_sha3_N, with one function for each input size. Instead of encoding the whole hash algorithm bit by bit—which would make SMT solving impractical—Dolmos only adds a few basic properties to these functions. + +When the input is concrete, Dolmos computes the real keccak256 value and stores the input/output pair for that execution path. This makes it possible to recover the preimage of a concrete storage slot and decode it into its structure, such as the base slot, mapping keys, and offsets. When the input is symbolic, the hash remains uninterpreted and is constrained only by a small set of axioms. An inverse function guarantees injectivity, so two different inputs cannot have the same hash. Hash values are also assumed to be non-zero and smaller than 2^256 − 2^64, preventing a struct or array offset from overflowing when added to a hashed storage slot. + +These assumptions are sound in practice, but they are deliberately incomplete: they do not formally connect the symbolic function to the real keccak256. As a result, the solver can invent a hash value. For example, it may choose an input whose symbolic hash matches a storage key written in setUp(), producing a counterexample that cannot actually be reproduced (halmos#562). + +Dolmos handles this lazily through counterexample-guided refinement. When the solver finds a satisfiable model, Dolmos reads the concrete preimages chosen by the model, computes their real keccak256 values, adds facts such as f_sha3_N(v) = keccak256(v), and runs the solver again. Because these facts are true for the real hash function, a real counterexample is never removed. Therefore, an unsat result proves that no counterexample exists under the stated assumptions. If the model remains inconsistent after a bounded number of refinement rounds, or if refinement cannot determine whether it is valid, Dolmos still reports it but marks it as potentially invalid instead of silently discarding it. + +Two additional design choices complete this approach. First, the optimizer may fold a keccak256 computation into a precomputed constant. If the resulting storage location is later decoded structurally, the value stored at the raw location is moved to the corresponding structured location (halmos#579). Second, the alternative generic storage layout can decode hashed storage keys purely structurally. This implicitly assumes that a hash cannot be equal to an unrelated constant. + +Example: halmos#562 + +The issue halmos#562, reproduced in KeccakRefinement.t.sol, shows why this refinement mechanism is necessary. In setUp(), the contract executes balances[key] = 50, where key is a concrete value. The test then checks that balances[uint256(keccak256(abi.encodePacked(amt)))] != 50 for every symbolic amt. + +When balances[key] is written, its storage location is keccak256(key . 0). Because the input is concrete, Dolmos computes the real hash and records it. It can therefore decode the storage location as (slot 0, key) rather than treating it as an arbitrary 256-bit value. + +During the test, however, keccak256(amt) is symbolic. Dolmos represents it as h = f_sha3_256(amt), so the read becomes a lookup at (slot 0, h). The read returns 50 if h = key. The current axioms do not prevent this: injectivity only says that two different inputs cannot have the same hash. The solver can therefore invent a model such as amt = 0 together with f_sha3_256(0) = key. It reports sat, but this is a false counterexample because the real keccak256(0) is not equal to key. + +Refinement then starts. Dolmos takes the model's preimage, 0, computes the real value of keccak256(0), and adds the constraint f_sha3_256(0) = keccak256(0). The previous model is now impossible. The solver may then try another value, for example amt = 1, with another invented hash. Dolmos adds the corresponding real hash and repeats the process. After the configured three refinement rounds (--keccak-refinement-rounds), the counterexample is reported as potentially invalid, rather than being presented as a valid exploit. + +The same mechanism behaves differently when a real preimage exists. In check_keccak_known_preimage, the test searches for an amt such that keccak256(amt) == keccak256(42). The solver proposes amt = 42, and the refinement step confirms that this matches the real hash. The counterexample is therefore validated immediately. + +The example also shows the effect of the two other modeling choices. With the generic storage layout, h is structurally understood as the hash of amt. It therefore cannot simply be treated as the unrelated constant key, so the problematic path can be eliminated before SMT solving. This is why the test uses the Solidity storage layout. Finally, if key were a compile-time constant, the optimizer could fold keccak256(key . 0) into a PUSH32 constant (halmos#579). The value would initially be stored under the raw location and then moved to the structured location when that location is later decoded. This is why the test keeps key in a state variable. diff --git a/src/halmos/__init__.py b/src/dolmos/__init__.py similarity index 100% rename from src/halmos/__init__.py rename to src/dolmos/__init__.py diff --git a/src/halmos/__main__.py b/src/dolmos/__main__.py similarity index 79% rename from src/halmos/__main__.py rename to src/dolmos/__main__.py index d768243d2..ddd410d17 100644 --- a/src/halmos/__main__.py +++ b/src/dolmos/__main__.py @@ -39,36 +39,50 @@ unsat, ) -import halmos.traces -from halmos.build import ( +import dolmos.traces +from dolmos.build import ( build_output_iterator, + get_source_path, + has_vyper_contracts, import_libs, parse_build_out, parse_devdoc, parse_natspec, ) -from halmos.bytevec import ByteVec -from halmos.calldata import FunctionInfo, get_abi, mk_calldata -from halmos.cheatcodes import snapshot_state -from halmos.config import Config as HalmosConfig -from halmos.config import ( +from dolmos.bytevec import ByteVec +from dolmos.calldata import FunctionInfo, get_abi, mk_calldata +from dolmos.cheatcodes import snapshot_state +from dolmos.config import Config as DolmosConfig +from dolmos.config import ( ConfigSource, arg_parser, default_config, + program_name, resolve_config_files, toml_parser, ) -from halmos.constants import ( +from dolmos.constants import ( VERBOSITY_TRACE_CONSTRUCTOR, VERBOSITY_TRACE_COUNTEREXAMPLE, VERBOSITY_TRACE_PATHS, VERBOSITY_TRACE_SETUP, ) -from halmos.contract import CoverageReporter -from halmos.env import init_env -from halmos.exceptions import FailCheatcode, HalmosException -from halmos.flamegraphs import CallSequenceFlamegraph, call_flamegraph, exec_flamegraph -from halmos.logs import ( +from dolmos.contract import CoverageReporter +from dolmos.env import init_env +from dolmos.evm_version import ( + EVM_VERSIONS, + LATEST_EVM_VERSION, + evm_version_from_metadata, + normalize_evm_version, +) +from dolmos.exceptions import ( + DolmosException, + FailCheatcode, + InvalidOpcode, + Revert, +) +from dolmos.flamegraphs import CallSequenceFlamegraph, call_flamegraph, exec_flamegraph +from dolmos.logs import ( COUNTEREXAMPLE_INVALID, INTERNAL_ERROR, LOOP_BOUND, @@ -80,9 +94,16 @@ warn, warn_code, ) -from halmos.mapper import BuildOut, DeployAddressMapper -from halmos.processes import ExecutorRegistry, ShutdownError -from halmos.sevm import ( +from dolmos.mapper import BuildOut, DeployAddressMapper +from dolmos.pcex import ( + CexLayout, + RenderedCex, + collect_layout, + render_counterexample, + repro_function, +) +from dolmos.processes import ExecutorRegistry, ShutdownError +from dolmos.sevm import ( EMPTY_BALANCE, FOUNDRY_CALLER, FOUNDRY_ORIGIN, @@ -102,24 +123,26 @@ jumpid_str, mnemonic, ) -from halmos.solve import ( +from dolmos.solve import ( ContractContext, FunctionContext, InvariantTestingContext, PathContext, SolverOutput, dirname, + mk_exp_apps, + mk_sha3_args, solve_end_to_end, solve_low_level, ) -from halmos.traces import ( +from dolmos.traces import ( render_trace, rendered_address, rendered_call_sequence, rendered_trace, ) -from halmos.ui import suspend_status, ui -from halmos.utils import ( +from dolmos.ui import suspend_status, ui +from dolmos.utils import ( EVM, Address, BitVecSort256, @@ -184,7 +207,7 @@ class Exitcode(Enum): COUNTEREXAMPLE = Exitcode.COUNTEREXAMPLE.value -def with_devdoc(args: HalmosConfig, fn_sig: str, contract_json: dict) -> HalmosConfig: +def with_devdoc(args: DolmosConfig, fn_sig: str, contract_json: dict) -> DolmosConfig: devdoc = parse_devdoc(fn_sig, contract_json) if not devdoc: return args @@ -194,9 +217,38 @@ def with_devdoc(args: HalmosConfig, fn_sig: str, contract_json: dict) -> HalmosC return args.with_overrides(source, **vars(overrides)) +def with_evm_version(args: DolmosConfig, contract_json: dict) -> DolmosConfig: + """ + Resolves the EVM version (a16z/halmos#128): the --evm-version option if given, + otherwise the evmVersion the contract was compiled for, otherwise the latest fork. + """ + if args.evm_version: + if normalize_evm_version(args.evm_version) is None: + error( + f"unsupported EVM version: {args.evm_version} " + f"(supported: {', '.join(EVM_VERSIONS)})" + ) + sys.exit(2) + return args + + compiled_for = evm_version_from_metadata(contract_json) + if compiled_for is None: + return args + + version = normalize_evm_version(compiled_for) + if version is None: + warn( + f"unsupported evmVersion {compiled_for} in the build output, " + f"using {LATEST_EVM_VERSION} (see --evm-version)" + ) + return args + + return args.with_overrides(ConfigSource.default, evm_version=version) + + def with_natspec( - args: HalmosConfig, contract_name: str, contract_natspec: str -) -> HalmosConfig: + args: DolmosConfig, contract_name: str, contract_natspec: str +) -> DolmosConfig: if not contract_natspec: return args @@ -209,7 +261,41 @@ def with_natspec( return args.with_overrides(source, **vars(overrides)) -def load_config(_args) -> HalmosConfig: +def with_vyper_defaults(args: DolmosConfig) -> DolmosConfig: + """ + Adjust the defaults for projects that contain vyper contracts: + - the solidity storage layout model does not apply to vyper (e.g. HashMap slots + are computed as keccak256(slot . key) instead of keccak256(key . slot)) + - vyper uses the INVALID opcode for `assert ..., UNREACHABLE`, its equivalent of + solidity's `assert` (Panic(0x01)) + + Values set in a config file, an annotation or on the command line take precedence. + """ + vyper_defaults = {"storage_layout": "generic", "invalid_as_failure": True} + + overrides = { + name: value + for name, value in vyper_defaults.items() + if args.value_with_source(name)[1] <= ConfigSource.default + } + + if not overrides: + return args + + print( + "Vyper contracts found, using " + + ", ".join( + f"--{name.replace('_', '-')}" + ("" if value is True else f" {value}") + for name, value in overrides.items() + ) + + " by default" + ) + + # same precedence as the global defaults, so any explicit setting still wins + return args.with_overrides(ConfigSource.default, **overrides) + + +def load_config(_args) -> DolmosConfig: config = default_config() # parse CLI args first, so that can get `--help` out of the way and resolve `--debug` @@ -252,7 +338,7 @@ def mk_addr(name: str) -> Address: return BitVec(name, 160) -def mk_solver(args: HalmosConfig, logic="QF_AUFBV", ctx=None) -> Solver: +def mk_solver(args: DolmosConfig, logic="QF_AUFBV", ctx=None) -> Solver: # in the config, we have a float in seconds # z3 expects an int in milliseconds timeout_ms = int(args.solver_timeout_branching * 1000) @@ -293,6 +379,9 @@ def deploy_test(ctx: FunctionContext, sevm: SEVM) -> Exec: # foundry default balance for the test contract ex.balance_update(this, con(0xFFFFFFFFFFFFFFFFFFFFFFFF)) + # the test contract is a deployed contract, so its nonce starts at 1 (EIP-161) + ex.set_nonce(this, 1) + # deploy libraries and resolve library placeholders in hexcode contract_ctx = ctx.contract_ctx (creation_hexcode, _) = ex.resolve_libs( @@ -308,7 +397,7 @@ def deploy_test(ctx: FunctionContext, sevm: SEVM) -> Exec: # sanity check if len(exs) != 1: - raise HalmosException(f"constructor: # of paths: {len(exs)}") + raise DolmosException(f"constructor: # of paths: {len(exs)}") [ex] = exs @@ -322,7 +411,7 @@ def deploy_test(ctx: FunctionContext, sevm: SEVM) -> Exec: output = ex.context.output returndata = output.data if output.error is not None or not returndata: - raise HalmosException(f"constructor failed: {output.error=} {returndata=}") + raise DolmosException(f"constructor failed: {output.error=} {returndata=}") deployed_bytecode = Contract(returndata) ex.try_resolve_contract_info(deployed_bytecode, args.coverage_output) @@ -335,7 +424,13 @@ def deploy_test(ctx: FunctionContext, sevm: SEVM) -> Exec: return ex -def setup(ctx: FunctionContext) -> Exec: +def setup(ctx: FunctionContext) -> list[Exec]: + """ + Deploys the test contract and runs its setUp function. + + Returns every feasible successful setup path: when setUp branches (e.g. on + symbolic values), each test is run from each of the resulting states. + """ setup_timer = NamedTimer("setup") setup_timer.create_subtimer("decode") @@ -349,7 +444,7 @@ def setup(ctx: FunctionContext) -> Exec: if not setup_sig: if args.statistics: print(setup_timer.report()) - return setup_ex + return [setup_ex] # TODO: dyn_params may need to be passed to mk_calldata in run() calldata, dyn_params = mk_calldata(ctx.contract_ctx.abi, setup_info, args) @@ -404,6 +499,7 @@ def setup(ctx: FunctionContext) -> Exec: case [(ex, _)]: setup_exs.append(ex) case _: + # keep every path that is not provably infeasible for path_id, (ex, query) in enumerate(setup_exs_no_error): path_ctx = PathContext( args=args, @@ -414,20 +510,24 @@ def setup(ctx: FunctionContext) -> Exec: solver_output = solve_low_level(path_ctx) if solver_output.result != unsat: setup_exs.append(ex) - if len(setup_exs) > 1: - break - match len(setup_exs): - case 0: - raise HalmosException(f"No successful path found in {setup_sig}") - case n if n > 1: - debug("\n".join(map(str, setup_exs))) - raise HalmosException(f"Multiple paths were found in {setup_sig}") + if not setup_exs: + raise DolmosException(f"No successful path found in {setup_sig}") - [setup_ex] = setup_exs + if len(setup_exs) > 1: + msg = ( + f"{setup_sig}: {len(setup_exs)} setup states found; " + "each test will be run from each of them" + ) + if args.verbose >= 1: + print(msg) + else: + debug(msg) if args.print_setup_states: - print(setup_ex) + for path_id, ex in enumerate(setup_exs): + print(f"# setup state {path_id}") + print(ex) if sevm.logs.bounded_loops: warn_code( @@ -439,7 +539,7 @@ def setup(ctx: FunctionContext) -> Exec: if args.statistics: print(setup_timer.report()) - return setup_ex + return setup_exs def is_global_fail_set(context: CallContext) -> bool: @@ -447,6 +547,30 @@ def is_global_fail_set(context: CallContext) -> bool: return hevm_fail or any(is_global_fail_set(x) for x in context.subcalls()) +def is_invalid_opcode_found(context: CallContext) -> bool: + """ + Check if the call failed because of an INVALID opcode (0xFE), e.g. vyper's + `assert ..., UNREACHABLE`. + + The INVALID opcode may have been hit in a nested call: the callers then see a + failed call with no returndata and typically bubble it up as an empty revert + (vyper `extcall`/`staticcall`, solidity high-level calls), so we follow the chain + of empty reverts down the last subcall. + """ + output = context.output + if isinstance(output.error, InvalidOpcode): + return True + + if not isinstance(output.error, Revert): + return False + + if output.data is not None and len(output.data) != 0: + return False + + last_subcall = context.last_subcall() + return last_subcall is not None and is_invalid_opcode_found(last_subcall) + + def get_state_id(ex: Exec) -> bytes: """ Computes the state snapshot hash, incorporating constraints on state variables. @@ -458,7 +582,7 @@ def get_state_id(ex: Exec) -> bytes: def run_target_function( - args: HalmosConfig, + args: DolmosConfig, ex: Exec, addr: Address, abi: dict, @@ -546,12 +670,12 @@ def run_target_contract( try: # create a symbolic tx.origin tx_origin = mk_addr( - f"halmos_tx_origin_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}" + f"dolmos_tx_origin_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}" ) # create a symbolic msg.sender msg_sender = mk_addr( - f"halmos_msg_sender_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}" + f"dolmos_msg_sender_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}" ) # restrict msg.sender to the specified target senders. @@ -569,7 +693,7 @@ def run_target_contract( # create a symbolic msg.value msg_value = BitVec( - f"halmos_msg_value_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}", + f"dolmos_msg_value_{id_str(addr)}_{uid()}_{ex.new_symbol_id():>02}", BitVecSort256, ) @@ -668,7 +792,7 @@ def _compute_frontier(ctx: ContractContext, depth: int) -> Iterator[Exec]: if flamegraph_enabled: call_flamegraph.add_with_sequence(post_ex.call_sequence, subcall) - # ignore and report if halmos-errored + # ignore and report if dolmos-errored if subcall.is_stuck(): error( f"{depth=}: addr={hexify(addr)}: {subcall.get_stuck_reason()}" @@ -679,7 +803,16 @@ def _compute_frontier(ctx: ContractContext, depth: int) -> Iterator[Exec]: if subcall.output.error: # ignore normal reverts panic_found = post_ex.is_panic_of(panic_error_codes) - if not panic_found and not is_global_fail_set(subcall): + invalid_found = ( + not panic_found + and args.invalid_as_failure + and is_invalid_opcode_found(subcall) + ) + if ( + not panic_found + and not invalid_found + and not is_global_fail_set(subcall) + ): continue fun_info = subcall.message.fun_info @@ -696,6 +829,7 @@ def _compute_frontier(ctx: ContractContext, depth: int) -> Iterator[Exec]: ex=post_ex, panic_found=panic_found, description=msg, + invalid_found=invalid_found, ) except ShutdownError: if args.debug: @@ -718,7 +852,7 @@ def _compute_frontier(ctx: ContractContext, depth: int) -> Iterator[Exec]: visited.add(post_id) # update timestamp - timestamp_name = f"halmos_block_timestamp_depth{depth}_{uid()}" + timestamp_name = f"dolmos_block_timestamp_depth{depth}_{uid()}" post_ex.block.timestamp = ZeroExt(192, BitVec(timestamp_name, 64)) post_ex.path.append(post_ex.block.timestamp >= pre_ex.block.timestamp) @@ -804,6 +938,7 @@ def handle_assertion_violation( ex: Exec, panic_found: bool, description: str = None, + invalid_found: bool = False, ) -> None: """ Handles a potential assertion violation by solving it in a separate process. @@ -816,6 +951,7 @@ def handle_assertion_violation( ex: The execution state containing the potential violation panic_found: Whether it's a panic error or a legacy hevm.fail flag description: Optional description of the violation + invalid_found: Whether an INVALID opcode was hit (see --invalid-as-failure) Raises: ShutdownError: If the executor has been shutdown during the solving process @@ -830,6 +966,8 @@ def handle_assertion_violation( if panic_found: panic_code = unbox_int(output.data[4:36].unwrap()) print(f"Panic(0x{panic_code:02x}) {error_output}") + elif invalid_found: + print(f"INVALID opcode (0xFE) {error_output}") else: # fail_found print(f"(fail flag set) {error_output}") @@ -851,6 +989,17 @@ def handle_assertion_violation( query: SMTQuery = ex.path.to_smt2(args) + # with --pretty-counterexamples, collect what is needed to render the counterexample + # (on this thread, as it reads z3 objects), and the EXP applications to be checked + layout, exp_apps = None, None + if args.pretty_counterexamples: + try: + layout = collect_layout(ctx, ex, self.is_invariant, self.is_probe) + except Exception as e: + debug(f"could not collect the counterexample layout: {e!r}") + if "f_evm_exp_256" in query.smtlib: + exp_apps = mk_exp_apps(ex.path.conditions) + # beware: because this object crosses thread boundaries, we must be careful to # avoid any reference to z3 objects path_ctx = PathContext( @@ -858,6 +1007,8 @@ def handle_assertion_violation( path_id=path_id, query=query, solving_ctx=ctx.solving_ctx, + sha3_args=mk_sha3_args(ex.sha3s) if args.keccak_refinement_rounds else (), + exp_apps=exp_apps, ) # ShutdownError may be raised here and will be handled by the caller @@ -868,33 +1019,46 @@ def handle_assertion_violation( ex=ex, path_ctx=path_ctx, description=description, + layout=layout, ) ) self.submitted_futures.append(solve_future) - def _get_solver_output(self, future: Future, path_ctx: PathContext) -> SolverOutput: + def _get_solver_output( + self, future: Future, path_ctx: PathContext + ) -> SolverOutput | None: + """ + Returns the output of the solver, or None if solving was cancelled because the + executor has been shut down (e.g. by --early-exit once a counterexample is found). + """ path_id, query_file = path_ctx.path_id, str(path_ctx.dump_file) if self.ctx.solving_ctx.executor.is_shutdown(): # if the thread pool is in the process of shutting down, # we want to stop processing remaining models/timeouts/errors, etc. - e = "executor has been shutdown" - return SolverOutput.from_error(e, path_id=path_id, query_file=query_file) + return None if e := future.exception(): - if not is_benign_solving_error(e): - error(f"encountered exception during assertion solving: {e!r}") + if is_benign_solving_error(e): + return None + error(f"encountered exception during assertion solving: {e!r}") return SolverOutput.from_error(e, path_id=path_id, query_file=query_file) try: return future.result() except Exception as e: - if not is_benign_solving_error(e): - error(f"encountered exception during assertion solving: {e!r}") + if is_benign_solving_error(e): + return None + error(f"encountered exception during assertion solving: {e!r}") return SolverOutput.from_error(e, path_id=path_id, query_file=query_file) def _solve_end_to_end_callback( - self, future: Future, ex: Exec, path_ctx: PathContext, description: str + self, + future: Future, + ex: Exec, + path_ctx: PathContext, + description: str, + layout: CexLayout | None = None, ) -> None: """ Callback function for handling solver results. @@ -903,6 +1067,7 @@ def _solve_end_to_end_callback( future: The Future object containing the solver result ex: The execution state description: Optional description of counterexample + layout: what is needed to render the counterexample (--pretty-counterexamples) """ # beware: this function may be called from threads other than the main thread, # so we must be careful to avoid referencing any z3 objects / contexts @@ -910,7 +1075,11 @@ def _solve_end_to_end_callback( ctx = self.ctx args = ctx.args - solver_output: SolverOutput = self._get_solver_output(future, path_ctx) + solver_output: SolverOutput | None = self._get_solver_output(future, path_ctx) + if solver_output is None: + # cancelled, e.g. by --early-exit: neither an error nor a result + return + ctx.solver_outputs.append(solver_output) result, model = solver_output.result, solver_output.model path_id = solver_output.path_id @@ -934,6 +1103,10 @@ def _solve_end_to_end_callback( if model is None: return + if args.pretty_counterexamples: + self._report_pretty_counterexample(ex, solver_output, description, layout) + return + # mark this probe as reported to avoid duplicate reporting # note: message.fun_info is used instead of ctx.info because the function context for probes is dummy. if self.is_probe: @@ -972,6 +1145,113 @@ def _solve_end_to_end_callback( if sequence := ctx.call_sequences[path_id]: print(f"Sequence:\n{sequence}") + def _report_pretty_counterexample( + self, + ex: Exec, + solver_output: SolverOutput, + description: str | None, + layout: CexLayout | None, + ) -> None: + """Reports a counterexample with --pretty-counterexamples (see dolmos.pcex)""" + # beware: called from the solver threads, see _solve_end_to_end_callback() + ctx = self.ctx + args = ctx.args + model, path_id = solver_output.model, solver_output.path_id + + rendered = None + if layout is not None: + try: + rendered = render_counterexample(layout, model.model) + except Exception as e: + debug(f"could not render the counterexample: {e!r}") + if args.debug: + traceback.print_exc() + + fun_sig = (layout.fun_sig if layout else ctx.info.sig) or "" + if rendered is not None: + body = rendered.body + else: + body = str(model).lstrip("\n").split("\n") + + pcex = ctx.pcex + with pcex.lock: + if model.is_valid: + ctx.valid_counterexamples.append(model) + else: + ctx.invalid_counterexamples.append(model) + + # mark this probe as reported to avoid duplicate reporting + if self.is_probe: + ctx.contract_ctx.probes_reported.add(ex.context.message.fun_info) + + # counterexamples with the same values as one already shown are only counted + if pcex.admit("\n".join(body), model.is_valid): + self._print_pretty_counterexample( + solver_output, description, layout, rendered, body, fun_sig + ) + + if model.is_valid: + # add the stacks from the temporary flamegraph to the global one + if self.flamegraph_enabled and self.is_invariant: + call_flamegraph.stacks.extend( + self.potential_flamegraphs[path_id].stacks + ) + + # we have a valid counterexample, so we are eligible for early exit + if args.early_exit: + debug(f"Shutting down {ctx.info.name}'s solver executor") + ctx.solving_ctx.executor.shutdown(wait=False) + + def _print_pretty_counterexample( + self, + solver_output: SolverOutput, + description: str | None, + layout: CexLayout | None, + rendered: RenderedCex | None, + body: list[str], + fun_sig: str, + ) -> None: + """Prints a counterexample shown by _report_pretty_counterexample()""" + ctx = self.ctx + args = ctx.args + model, path_id = solver_output.model, solver_output.path_id + + lines = [] + if description: + lines.append(description) + + if args.verbose >= VERBOSITY_TRACE_COUNTEREXAMPLE: + pid_str = f" #{path_id}" if args.verbose >= VERBOSITY_TRACE_PATHS else "" + lines.append(f"Trace{pid_str}:") + lines.append(ctx.traces[path_id].rstrip("\n")) + + if model.is_valid: + lines.append(color_error(f"Counterexample: {fun_sig}")) + else: + reason = ( + solver_output.invalid_reason + or "relies on an approximation of the EVM semantics" + ) + lines.append(color_warn(f"Counterexample (potentially invalid): {fun_sig}")) + lines.append(color_warn(f" reason: {reason}")) + + lines.extend(body) + + # the symbolic call sequence of invariant testing, replaced by the concrete one + sequence = ctx.call_sequences.get(path_id) + if sequence and ( + rendered is None or args.verbose >= VERBOSITY_TRACE_COUNTEREXAMPLE + ): + lines.append(f"Sequence (symbolic):\n{sequence.rstrip()}") + + if rendered is not None and rendered.repro and model.is_valid: + lines.extend(repro_function(layout, rendered, ctx.pcex.shown)) + + if not model.is_valid: + lines.append(f"(see {COUNTEREXAMPLE_INVALID.url()})") + + print("\n".join(lines)) + def _save_failed_query( self, path_id: int, solver_output: SolverOutput, failure_type: str ) -> None: @@ -1011,7 +1291,7 @@ def run_test(ctx: FunctionContext) -> TestResult: is_invariant = funname.startswith("invariant_") # set the config for every trace rendered in this test - halmos.traces.config_context.set(args) + dolmos.traces.config_context.set(args) # # prepare calldata @@ -1087,8 +1367,13 @@ def run_test(ctx: FunctionContext) -> TestResult: output = ex.context.output error_output = output.error panic_found = ex.is_panic_of(args.panic_error_codes) + invalid_found = ( + not panic_found + and args.invalid_as_failure + and is_invalid_opcode_found(ex.context) + ) - if panic_found or is_global_fail_set(ex.context): + if panic_found or invalid_found or is_global_fail_set(ex.context): potential += 1 try: @@ -1096,6 +1381,7 @@ def run_test(ctx: FunctionContext) -> TestResult: path_id=path_id, ex=ex, panic_found=panic_found, + invalid_found=invalid_found, ) except ShutdownError: if args.debug: @@ -1205,6 +1491,12 @@ def run_test(ctx: FunctionContext) -> TestResult: f"bounds: [{', '.join([str(x) for x in dyn_params])}])" ) + if args.pretty_counterexamples and (hidden := ctx.pcex.hidden): + print( + f" {hidden} duplicate counterexample{'s' if hidden > 1 else ''} not shown " + "(same values as a counterexample above)" + ) + if exitcode in (Exitcode.TIMEOUT.value, Exitcode.EXCEPTION.value): # print query directory information failure_type = "timeout" if exitcode == Exitcode.TIMEOUT.value else "error" @@ -1225,6 +1517,9 @@ def run_test(ctx: FunctionContext) -> TestResult: ) debug("\n".join(jumpid_str(x) for x in logs.bounded_loops)) + for lasso_result in logs.lassos: + print(f" {lasso_result.summary()}") + # return test result num_cexes = len(ctx.valid_counterexamples) + len(ctx.invalid_counterexamples) if args.minimal_json_output: @@ -1315,7 +1610,7 @@ def execute_simple_getter( # sanity check if len(exs) != 1: - raise HalmosException(f"{fun_info.sig}: # of paths: {len(exs)}") + raise DolmosException(f"{fun_info.sig}: # of paths: {len(exs)}") [ex] = exs @@ -1323,7 +1618,7 @@ def execute_simple_getter( returndata = output.data if output.error is not None or not returndata: - raise HalmosException(f"{fun_info.sig}: {output.error=} {returndata=}") + raise DolmosException(f"{fun_info.sig}: {output.error=} {returndata=}") return returndata @@ -1487,7 +1782,7 @@ def resolve_target_contracts(ctx: InvariantTestingContext, ex: Exec) -> set[Addr ) if not resolved_target_contracts: - raise HalmosException("No target contracts available.") + raise DolmosException("No target contracts available.") return resolved_target_contracts @@ -1523,7 +1818,7 @@ def resolve_target_selectors( debug(f"Skipping {fun_sig} ({state_mutability})") continue - # https://github.com/a16z/halmos/issues/514 + # see upstream halmos issue #514 # exclude special functions like test_, check_, setUp(), etc. if is_test_contract and ( fun_sig.startswith("test_") @@ -1560,9 +1855,10 @@ def run_contract(ctx: ContractContext) -> list[TestResult]: contract_ctx=ctx, ) - halmos.traces.config_context.set(setup_config) - setup_ex = setup(setup_ctx) - setup_ex.path_slice() + dolmos.traces.config_context.set(setup_config) + setup_exs = setup(setup_ctx) + for setup_ex in setup_exs: + setup_ex.path_slice() except Exception as err: error(f"{setup_info.sig} failed: {type(err).__name__}: {err}") if args.debug: @@ -1573,11 +1869,15 @@ def run_contract(ctx: ContractContext) -> list[TestResult]: return [] - # initialize the frontier and visited states using the initial setup state - ctx.frontier_states[0] = [setup_ex] - ctx.visited.add(get_state_id(setup_ex)) + # initialize the frontier and visited states using the initial setup states. + # every test (and every invariant test sequence) starts from each of them. + ctx.frontier_states[0] = setup_exs + for setup_ex in setup_exs: + ctx.visited.add(get_state_id(setup_ex)) - test_results = run_tests(ctx, setup_ex, ctx.funsigs) + # the invariant testing context (target contracts, senders, selectors) + # is read from the first setup state + test_results = run_tests(ctx, setup_exs[0], ctx.funsigs) # reset any remaining solver states from the default context reset(setup_solver) @@ -1588,7 +1888,7 @@ def run_contract(ctx: ContractContext) -> list[TestResult]: def print_invariant_targets(ctx: ContractContext, ex: Exec): try: target_contracts = resolve_target_contracts(ctx.inv_ctx, ex) - except HalmosException: + except DolmosException: # no target contracts found, let the downstream tests fail target_contracts = [] @@ -1729,7 +2029,7 @@ def _main(_args=None) -> MainResult: args = load_config(_args) if args.version: - print(f"halmos {metadata.version('halmos')}") + print(f"{program_name()} {metadata.version('dolmos')}") return MainResult(0) init_env(args.root) @@ -1742,7 +2042,7 @@ def _main(_args=None) -> MainResult: logger_unique.setLevel(logging.DEBUG) if args.trace_memory: - import halmos.memtrace as memtrace + import dolmos.memtrace as memtrace memtrace.MemTracer.get().start() @@ -1781,7 +2081,14 @@ def _main(_args=None) -> MainResult: # run forge without capturing stdout/stderr debug(f"Running {' '.join(build_cmd)}") - build_exitcode = subprocess.run(build_cmd).returncode + # recent forge versions enable `dynamic_test_linking` by default, which rewrites + # `new C(...)` in test files into `vm.deployCode(...)` calls. dolmos needs the + # original creation bytecode, so we turn it off (env var: ignored by older forge, + # and still overridable by the user). + build_env = os.environ.copy() + build_env.setdefault("FOUNDRY_DYNAMIC_TEST_LINKING", "false") + + build_exitcode = subprocess.run(build_cmd, env=build_env).returncode if build_exitcode: error(f"Build failed: {build_cmd}") @@ -1798,6 +2105,10 @@ def _main(_args=None) -> MainResult: traceback.print_exc() return MainResult(1) + # vyper support: switch some defaults, unless explicitly configured + if has_vyper_contracts(build_out): + args = with_vyper_defaults(args) + timer.create_subtimer("tests") total_passed = 0 @@ -1862,14 +2173,15 @@ def on_signal(signum, frame): linkReferences = contract_json["bytecode"]["linkReferences"] libs = import_libs(build_out_map, creation_hexcode, linkReferences) - contract_path = f"{contract_json['ast']['absolutePath']}:{contract_name}" + contract_path = f"{get_source_path(contract_json, filename)}:{contract_name}" print(f"\nRunning {num_found} tests for {contract_path}") # Set the test contract address in DeployAddressMapper DeployAddressMapper().add_deployed_contract(hexify(FOUNDRY_TEST), contract_name) - # support for `/// @custom:halmos` annotations + # support for `/// @custom:dolmos` annotations contract_args = with_natspec(args, contract_name, natspec) + contract_args = with_evm_version(contract_args, contract_json) contract_ctx = ContractContext( args=contract_args, name=contract_name, @@ -1942,12 +2254,12 @@ def on_signal(signum, frame): return on_exit(exitcode) -# entrypoint for the `halmos` script +# entrypoint for the `dolmos` script def main() -> int: exitcode = _main().exitcode return exitcode -# entrypoint for `python -m halmos` +# entrypoint for `python -m dolmos` if __name__ == "__main__": sys.exit(main()) diff --git a/src/halmos/assertions.py b/src/dolmos/assertions.py similarity index 98% rename from src/halmos/assertions.py rename to src/dolmos/assertions.py index de9e432ed..b4a225563 100644 --- a/src/halmos/assertions.py +++ b/src/dolmos/assertions.py @@ -13,8 +13,8 @@ is_bv, ) -from halmos.exceptions import HalmosException -from halmos.utils import ( +from dolmos.exceptions import DolmosException +from dolmos.utils import ( bytes_to_bv_value, extract_bytes, extract_bytes32_array_argument, @@ -178,7 +178,7 @@ def mk_assert_handler(signature): operator = match.group(1) params = match.group(2).split(",") else: - raise HalmosException(f"not supported signatures: {signature}") + raise DolmosException(f"not supported signatures: {signature}") # operator type: # - binary: compare two arguments diff --git a/src/halmos/bitvec.py b/src/dolmos/bitvec.py similarity index 65% rename from src/halmos/bitvec.py rename to src/dolmos/bitvec.py index e1d6ac3b7..cff22de4f 100644 --- a/src/halmos/bitvec.py +++ b/src/dolmos/bitvec.py @@ -34,10 +34,10 @@ simplify, ) -from halmos.exceptions import NotConcreteError +from dolmos.exceptions import NotConcreteError -BV: TypeAlias = "HalmosBitVec" -AnyValue: TypeAlias = "int | bytes | BitVecRef | BV | HalmosBool | str" +BV: TypeAlias = "DolmosBitVec" +AnyValue: TypeAlias = "int | bytes | BitVecRef | BV | DolmosBool | str" BVValue: TypeAlias = int | BitVecRef | BoolRef MaybeSize: TypeAlias = int | None AnyBool: TypeAlias = bool | BoolRef @@ -62,11 +62,11 @@ def as_int(value: AnyValue) -> tuple[BVValue, MaybeSize]: return int.from_bytes(value, "big"), len(value) * 8 elif is_bv_value(value): return value.as_long(), value.size() - elif isinstance(value, HalmosBitVec): + elif isinstance(value, DolmosBitVec): return value.unwrap(), value.size elif isinstance(value, BitVecRef): return value, value.size() - elif isinstance(value, HalmosBool): + elif isinstance(value, DolmosBool): return value.unwrap(), 1 elif isinstance(value, BoolRef): return value, 1 @@ -74,23 +74,23 @@ def as_int(value: AnyValue) -> tuple[BVValue, MaybeSize]: raise TypeError(f"Cannot convert {type(value)} to int") -class HalmosBool: +class DolmosBool: """ Immutable wrapper for concrete or symbolic boolean values. Can be constructed with: - - HalmosBool(42 % 2 == 0) # bool - - HalmosBool(BitVec(x, 8) != 0) # BoolRef - - HalmosBool(HalmosBitVec(x, 8)) # HalmosBitVec, same as above + - DolmosBool(42 % 2 == 0) # bool + - DolmosBool(BitVec(x, 8) != 0) # BoolRef + - DolmosBool(DolmosBitVec(x, 8)) # DolmosBitVec, same as above - Conversion to and from HalmosBitVec: - - HalmosBitVec(halmos_bool) (same as halmos_bool.as_bv()) - - HalmosBool(halmos_bitvec) (same as halmos_bitvec.is_non_zero()) + Conversion to and from DolmosBitVec: + - DolmosBitVec(dolmos_bool) (same as dolmos_bool.as_bv()) + - DolmosBool(dolmos_bitvec) (same as dolmos_bitvec.is_non_zero()) Wrapping/unwrapping: - - halmos_bool.as_z3() always converts to a z3 BoolRef - - bool(halmos_bool) converts to a concrete bool, raises if symbolic - - halmos_bool.value/unwrap() returns the underlying bool or z3 BoolRef + - dolmos_bool.as_z3() always converts to a z3 BoolRef + - bool(dolmos_bool) converts to a concrete bool, raises if symbolic + - dolmos_bool.value/unwrap() returns the underlying bool or z3 BoolRef """ __slots__ = ("con_val", "sym_val") @@ -103,10 +103,10 @@ def __new__(cls, value, *, do_simplify: bool = True): if type_value is bool: return TRUE if value else FALSE - if type_value is HalmosBool: + if type_value is DolmosBool: return value - if type_value is HalmosBitVec: + if type_value is DolmosBitVec: return value.is_non_zero() if type_value is BoolRef: @@ -137,14 +137,14 @@ def __init__(self, value: AnyBool | str, *, do_simplify: bool = True): self.sym_val = Bool(value) self.con_val = None - case HalmosBool(): + case DolmosBool(): return - case HalmosBitVec(): + case DolmosBitVec(): return case _: - raise TypeError(f"Cannot create HalmosBool from {type(value)}") + raise TypeError(f"Cannot create DolmosBool from {type(value)}") assert self.con_val is None or self.sym_val is None assert self.con_val is not None or self.sym_val is not None @@ -209,7 +209,7 @@ def __eq__(self, other: Any) -> bool: note: this is not the same as z3's comparison, which returns a constraint """ - if not isinstance(other, HalmosBool): + if not isinstance(other, DolmosBool): return False match (self.con_val, other.con_val): @@ -232,28 +232,28 @@ def __hash__(self) -> int: return hash((self.con_val, self.sym_val)) - def is_zero(self) -> "HalmosBool": + def is_zero(self) -> "DolmosBool": if self is TRUE: return FALSE if self is FALSE: return TRUE - return HalmosBool(Not(self.sym_val)) + return DolmosBool(Not(self.sym_val)) - def is_non_zero(self) -> "HalmosBool": + def is_non_zero(self) -> "DolmosBool": return self - def eq(self, other: "HalmosBool") -> "HalmosBool": - return HalmosBool(self.value == other.value) + def eq(self, other: "DolmosBool") -> "DolmosBool": + return DolmosBool(self.value == other.value) - def neg(self) -> "HalmosBool": + def neg(self) -> "DolmosBool": return self.is_zero() - def bitwise_not(self) -> "HalmosBool": + def bitwise_not(self) -> "DolmosBool": return self.is_zero() - def bitwise_and(self, other: "HalmosBool") -> "HalmosBool": + def bitwise_and(self, other: "DolmosBool") -> "DolmosBool": if self is TRUE: return other @@ -266,9 +266,9 @@ def bitwise_and(self, other: "HalmosBool") -> "HalmosBool": if other is FALSE: return other - return HalmosBool(And(self.as_z3(), other.as_z3())) + return DolmosBool(And(self.as_z3(), other.as_z3())) - def bitwise_or(self, other: "HalmosBool") -> "HalmosBool": + def bitwise_or(self, other: "DolmosBool") -> "DolmosBool": if self is TRUE: return self @@ -281,9 +281,9 @@ def bitwise_or(self, other: "HalmosBool") -> "HalmosBool": if other is FALSE: return self - return HalmosBool(Or(self.as_z3(), other.as_z3())) + return DolmosBool(Or(self.as_z3(), other.as_z3())) - def bitwise_xor(self, other: "HalmosBool") -> "HalmosBool": + def bitwise_xor(self, other: "DolmosBool") -> "DolmosBool": if self is TRUE: return other.bitwise_not() @@ -296,47 +296,47 @@ def bitwise_xor(self, other: "HalmosBool") -> "HalmosBool": if other is FALSE: return self - return HalmosBool(Xor(self.as_z3(), other.as_z3())) + return DolmosBool(Xor(self.as_z3(), other.as_z3())) def as_bv(self, size: int = 1) -> BV: if self is TRUE: - return ONE if size == 256 else HalmosBitVec(1, size=size) + return ONE if size == 256 else DolmosBitVec(1, size=size) if self is FALSE: - return ZERO if size == 256 else HalmosBitVec(0, size=size) + return ZERO if size == 256 else DolmosBitVec(0, size=size) expr = If(self.sym_val, BitVecVal(1, size), BitVecVal(0, size)) - return HalmosBitVec(expr, size=size) + return DolmosBitVec(expr, size=size) -class HalmosBitVec: +class DolmosBitVec: """ Immutable wrapper for concrete or symbolic bitvectors. Can be constructed with: - - HalmosBitVec(42) # int, size is default (256) - - HalmosBitVec(-1, size=8) # int, 2's complement - - HalmosBitVec(bytes.fromhex("12345678")) # bytes, size is inherited - - HalmosBitVec(BitVecVal(42, 8)) # BitVecVal, size is inherited - - HalmosBitVec(BitVec(x, 8)) # BitVecRef, size is inherited - - HalmosBitVec(halmos_bool) # HalmosBool, size 1 - - HalmosBitVec("x") # named symbol, size is default (256) - - Conversion to and from HalmosBool: - - HalmosBitVec(halmos_bool) (same as halmos_bool.as_bv()) - - HalmosBool(halmos_bitvec) (same as halmos_bitvec.is_non_zero()) + - DolmosBitVec(42) # int, size is default (256) + - DolmosBitVec(-1, size=8) # int, 2's complement + - DolmosBitVec(bytes.fromhex("12345678")) # bytes, size is inherited + - DolmosBitVec(BitVecVal(42, 8)) # BitVecVal, size is inherited + - DolmosBitVec(BitVec(x, 8)) # BitVecRef, size is inherited + - DolmosBitVec(dolmos_bool) # DolmosBool, size 1 + - DolmosBitVec("x") # named symbol, size is default (256) + + Conversion to and from DolmosBool: + - DolmosBitVec(dolmos_bool) (same as dolmos_bool.as_bv()) + - DolmosBool(dolmos_bitvec) (same as dolmos_bitvec.is_non_zero()) Wrapping/unwrapping: - - halmos_bitvec.as_z3() always converts to a z3 BitVecRef - - int(halmos_bitvec) converts to a concrete int, raises if symbolic - - halmos_bitvec.value/unwrap() returns the underlying int or z3 BitVecRef + - dolmos_bitvec.as_z3() always converts to a z3 BitVecRef + - int(dolmos_bitvec) converts to a concrete int, raises if symbolic + - dolmos_bitvec.value/unwrap() returns the underlying int or z3 BitVecRef """ __slots__ = ("_value", "_symbolic", "_size") def __new__(cls, value, size=None, do_simplify=True): - # fast path for existing HalmosBitVec of same size - if isinstance(value, HalmosBitVec): + # fast path for existing DolmosBitVec of same size + if isinstance(value, DolmosBitVec): size = size or value._size if size == value._size: return value @@ -348,7 +348,7 @@ def __init__( self, value: AnyValue, *, size: MaybeSize = None, do_simplify: bool = True ): """ - Create a new HalmosBitVec from an integer, bytes, or a z3 BitVecRef. + Create a new DolmosBitVec from an integer, bytes, or a z3 BitVecRef. If the value is too large for the bit size, it will be truncated. @@ -357,16 +357,16 @@ def __init__( type_value = type(value) - if type_value is HalmosBitVec: - # avoid reinitializing HalmosBitVec because of __new__ shortcut if same size + if type_value is DolmosBitVec: + # avoid reinitializing DolmosBitVec because of __new__ shortcut if same size if size == value.size: return - # otherwise, create a new HalmosBitVec with the new size + # otherwise, create a new DolmosBitVec with the new size value = value.unwrap() - # unwrap HalmosBool - elif type_value is HalmosBool: + # unwrap DolmosBool + elif type_value is DolmosBool: value = value.unwrap() # convenience, wrap a string as a named symbol @@ -404,7 +404,7 @@ def __init__( self._value = simplified else: - raise TypeError(f"Cannot create HalmosBitVec from {type(value)}") + raise TypeError(f"Cannot create DolmosBitVec from {type(value)}") def __deepcopy__(self, memo): # yay immutability @@ -441,7 +441,7 @@ def __eq__(self, other: Any) -> bool: note: this is not the same as z3's comparison, which returns a constraint """ - if not isinstance(other, HalmosBitVec): + if not isinstance(other, DolmosBitVec): return False if self._size != other.size: @@ -476,13 +476,13 @@ def __repr__(self) -> str: def __str__(self) -> str: return str(self._value) - def is_zero(self) -> HalmosBool: + def is_zero(self) -> DolmosBool: # works for both symbolic and concrete - return HalmosBool(self._value == 0) + return DolmosBool(self._value == 0) - def is_non_zero(self) -> HalmosBool: + def is_non_zero(self) -> DolmosBool: # works for both symbolic and concrete - return HalmosBool(self._value != 0) + return DolmosBool(self._value != 0) # # operations @@ -492,24 +492,24 @@ def add(self, other: BV) -> BV: size = self._size assert size == other._size - return HalmosBitVec(self._value + other._value, size=size) + return DolmosBitVec(self._value + other._value, size=size) - def sub(self, other: BV) -> "HalmosBitVec": + def sub(self, other: BV) -> "DolmosBitVec": size = self._size assert size == other._size - return HalmosBitVec(self._value - other._value, size=size) + return DolmosBitVec(self._value - other._value, size=size) def mul( self, other: BV, *, abstraction: FuncDeclRef | None = None - ) -> "HalmosBitVec": + ) -> "DolmosBitVec": size = self._size assert size == other.size lhs, rhs = self.value, other.value match (self.is_concrete, other.is_concrete): case (True, True): - return HalmosBitVec(lhs * rhs, size=size) + return DolmosBitVec(lhs * rhs, size=size) case (True, False): if lhs == 0: @@ -519,9 +519,9 @@ def mul( return other if is_power_of_two(lhs): - return other.lshl(HalmosBitVec(lhs.bit_length() - 1, size=size)) + return other.lshl(DolmosBitVec(lhs.bit_length() - 1, size=size)) - return HalmosBitVec(lhs * rhs, size=size) + return DolmosBitVec(lhs * rhs, size=size) case (False, True): if rhs == 0: @@ -531,20 +531,20 @@ def mul( return self if is_power_of_two(rhs): - return self.lshl(HalmosBitVec(rhs.bit_length() - 1, size=size)) + return self.lshl(DolmosBitVec(rhs.bit_length() - 1, size=size)) # simplify(x * 123) -> 123 * x - return HalmosBitVec(rhs * lhs, size=size) + return DolmosBitVec(rhs * lhs, size=size) return ( - HalmosBitVec(lhs * rhs, size=size) + DolmosBitVec(lhs * rhs, size=size) if abstraction is None - else HalmosBitVec(abstraction(lhs, rhs), size=size) + else DolmosBitVec(abstraction(lhs, rhs), size=size) ) def div( self, other: BV, *, abstraction: FuncDeclRef | None = None - ) -> "HalmosBitVec": + ) -> "DolmosBitVec": # TODO: div_xy_y size = self._size @@ -564,20 +564,20 @@ def div( # fully concrete case if self.is_concrete: - return HalmosBitVec(lhs // rhs, size=size) + return DolmosBitVec(lhs // rhs, size=size) if is_power_of_two(rhs): - return self.lshr(HalmosBitVec(rhs.bit_length() - 1, size=size)) + return self.lshr(DolmosBitVec(rhs.bit_length() - 1, size=size)) # symbolic case if abstraction is None: - return HalmosBitVec(UDiv(lhs, rhs), size=size) + return DolmosBitVec(UDiv(lhs, rhs), size=size) - return HalmosBitVec(abstraction(lhs, rhs), size=size) + return DolmosBitVec(abstraction(lhs, rhs), size=size) def sdiv( self, other: BV, *, abstraction: FuncDeclRef | None = None - ) -> "HalmosBitVec": + ) -> "DolmosBitVec": # TODO: sdiv_xy_y size = self._size assert size == other.size @@ -593,20 +593,20 @@ def sdiv( if self.is_concrete: # rely on z3 to handle the signed division - return HalmosBitVec( + return DolmosBitVec( BitVecVal(lhs, size) / BitVecVal(rhs, size), size=size, do_simplify=True, ) if abstraction is None: - return HalmosBitVec(other / self, size=size) + return DolmosBitVec(other / self, size=size) - return HalmosBitVec(abstraction(lhs, rhs), size=size) + return DolmosBitVec(abstraction(lhs, rhs), size=size) def mod( - self, other: "HalmosBitVec", *, abstraction: FuncDeclRef | None = None - ) -> "HalmosBitVec": + self, other: "DolmosBitVec", *, abstraction: FuncDeclRef | None = None + ) -> "DolmosBitVec": size = self._size assert size == other.size @@ -619,27 +619,27 @@ def mod( # mod by one is zero if rhs == 1: - return HalmosBitVec(0, size=size) + return DolmosBitVec(0, size=size) # fully concrete case if self.is_concrete: - return HalmosBitVec(lhs % rhs, size=size) + return DolmosBitVec(lhs % rhs, size=size) # mod by a power of two only keeps the low bits if is_power_of_two(rhs): # option 1: use z3 bitwise and # 10000 loops, best of 5: 148.215 usec per loop - # return HalmosBitVec(lhs & (rhs - 1), size=size) + # return DolmosBitVec(lhs & (rhs - 1), size=size) # option 2: truncate and extend # 10000 loops, best of 5: 146.525 usec per loop - # truncated = HalmosBitVec(lhs, size=rhs.bit_length() - 1) - # return HalmosBitVec(truncated, size=size) + # truncated = DolmosBitVec(lhs, size=rhs.bit_length() - 1) + # return DolmosBitVec(truncated, size=size) # option 3: truncate and extend, skip simplify # 10000 loops, best of 5: 130.028 usec per loop - # truncated = HalmosBitVec(lhs, size=rhs.bit_length() - 1, do_simplify=False) - # return HalmosBitVec(truncated, size=size) + # truncated = DolmosBitVec(lhs, size=rhs.bit_length() - 1, do_simplify=False) + # return DolmosBitVec(truncated, size=size) # option 4: explicit ZeroExt and Extract # on this path, we know that rhs > 1, so bitsize > 1 @@ -647,17 +647,17 @@ def mod( bitsize = rhs.bit_length() - 1 truncated = Extract(bitsize - 1, 0, lhs) extended = ZeroExt(size - bitsize, truncated) - return HalmosBitVec(extended, size=size) + return DolmosBitVec(extended, size=size) # symbolic case if abstraction is None: - return HalmosBitVec(URem(lhs, rhs), size=size) + return DolmosBitVec(URem(lhs, rhs), size=size) - return HalmosBitVec(abstraction(lhs, rhs), size=size) + return DolmosBitVec(abstraction(lhs, rhs), size=size) def smod( - self, other: "HalmosBitVec", *, abstraction: FuncDeclRef | None = None - ) -> "HalmosBitVec": + self, other: "DolmosBitVec", *, abstraction: FuncDeclRef | None = None + ) -> "DolmosBitVec": size = self._size assert size == other.size @@ -669,14 +669,14 @@ def smod( # mod by one is zero if rhs == 1: - return HalmosBitVec(0, size=size) + return DolmosBitVec(0, size=size) # TODO: implement concrete signed remainder # (tricky because it truncates towards zero) if self.is_concrete: # rely on z3 to handle the signed division - return HalmosBitVec( + return DolmosBitVec( SRem(BitVecVal(lhs, size), BitVecVal(rhs, size)), size=size, do_simplify=True, @@ -684,18 +684,18 @@ def smod( # lhs and rhs are symbolic if abstraction is None: - return HalmosBitVec(SRem(lhs, rhs), size=size) + return DolmosBitVec(SRem(lhs, rhs), size=size) - return HalmosBitVec(abstraction(lhs, rhs), size=size) + return DolmosBitVec(abstraction(lhs, rhs), size=size) def exp( self, - other: "HalmosBitVec", + other: "DolmosBitVec", *, exp_abstraction: FuncDeclRef | None = None, mul_abstraction: FuncDeclRef | None = None, smt_exp_by_const: int = 0, - ) -> "HalmosBitVec": + ) -> "DolmosBitVec": size = self._size assert size == other.size @@ -703,13 +703,13 @@ def exp( if other.is_concrete: if rhs == 0: - return HalmosBitVec(1, size=size) + return DolmosBitVec(1, size=size) if rhs == 1: return self if self.is_concrete: - return HalmosBitVec(lhs**rhs, size=size) + return DolmosBitVec(lhs**rhs, size=size) if rhs <= smt_exp_by_const: exp = self @@ -720,55 +720,55 @@ def exp( if exp_abstraction is None: raise NotImplementedError("missing SMT abstraction for exponentiation") - return HalmosBitVec(exp_abstraction(lhs, rhs), size=size) + return DolmosBitVec(exp_abstraction(lhs, rhs), size=size) def addmod( self, - other: "HalmosBitVec", - modulus: "HalmosBitVec", + other: "DolmosBitVec", + modulus: "DolmosBitVec", *, abstraction: FuncDeclRef | None = None, - ) -> "HalmosBitVec": + ) -> "DolmosBitVec": size = self._size assert size == other.size assert size == modulus.size if self.is_concrete and other.is_concrete and modulus.is_concrete: - return HalmosBitVec((self.value + other.value) % modulus.value, size=size) + return DolmosBitVec((self.value + other.value) % modulus.value, size=size) # to avoid add overflow; and to be a multiple of 8-bit newsize = size + 8 - r1 = HalmosBitVec(self, size=newsize).add(HalmosBitVec(other, size=newsize)) - r2 = r1.mod(HalmosBitVec(modulus, size=newsize), abstraction=abstraction) + r1 = DolmosBitVec(self, size=newsize).add(DolmosBitVec(other, size=newsize)) + r2 = r1.mod(DolmosBitVec(modulus, size=newsize), abstraction=abstraction) if r1.size != newsize: raise ValueError(r1) if r2.size != newsize: raise ValueError(r2) - return HalmosBitVec(r2, size=size) + return DolmosBitVec(r2, size=size) def mulmod( self, - other: "HalmosBitVec", - modulus: "HalmosBitVec", + other: "DolmosBitVec", + modulus: "DolmosBitVec", *, mul_abstraction: FuncDeclRef | None = None, mod_abstraction: FuncDeclRef | None = None, - ) -> "HalmosBitVec": + ) -> "DolmosBitVec": size = self._size assert size == other.size assert size == modulus.size if self.is_concrete and other.is_concrete and modulus.is_concrete: - return HalmosBitVec((self.value * other.value) % modulus.value, size=size) + return DolmosBitVec((self.value * other.value) % modulus.value, size=size) # to avoid mul overflow newsize = size * 2 - self_ext = HalmosBitVec(self, size=newsize) - other_ext = HalmosBitVec(other, size=newsize) - mod_ext = HalmosBitVec(modulus, size=newsize) + self_ext = DolmosBitVec(self, size=newsize) + other_ext = DolmosBitVec(other, size=newsize) + mod_ext = DolmosBitVec(modulus, size=newsize) r1 = self_ext.mul(other_ext, abstraction=mul_abstraction) r2 = r1.mod(mod_ext, abstraction=mod_abstraction) @@ -779,9 +779,9 @@ def mulmod( if r2.size != newsize: raise ValueError(r2) - return HalmosBitVec(r2, size=size) + return DolmosBitVec(r2, size=size) - def signextend(self, size: int) -> "HalmosBitVec": + def signextend(self, size: int) -> "DolmosBitVec": # TODO: handle other sizes assert self.size == 256 @@ -791,11 +791,11 @@ def signextend(self, size: int) -> "HalmosBitVec": # TODO: handle concrete case natively bl = (size + 1) * 8 - return HalmosBitVec( + return DolmosBitVec( SignExt(256 - bl, Extract(bl - 1, 0, self.as_z3())), size=256 ) - def lshl(self, shift: BV) -> "HalmosBitVec": + def lshl(self, shift: BV) -> "DolmosBitVec": """ Logical left shift """ @@ -808,11 +808,11 @@ def lshl(self, shift: BV) -> "HalmosBitVec": return self if shift_amount >= size: - return HalmosBitVec(0, size=size) + return DolmosBitVec(0, size=size) - return HalmosBitVec(self._value << shift_amount, size=size) + return DolmosBitVec(self._value << shift_amount, size=size) - def lshr(self, shift: BV) -> "HalmosBitVec": + def lshr(self, shift: BV) -> "DolmosBitVec": """ Logical right shift """ @@ -825,14 +825,14 @@ def lshr(self, shift: BV) -> "HalmosBitVec": return self if self.is_concrete: - return HalmosBitVec(self.value >> shift_amount, size=size) + return DolmosBitVec(self.value >> shift_amount, size=size) if shift_amount >= size: - return HalmosBitVec(0, size=size) + return DolmosBitVec(0, size=size) - return HalmosBitVec(LShR(self.as_z3(), shift.as_z3()), size=size) + return DolmosBitVec(LShR(self.as_z3(), shift.as_z3()), size=size) - def ashr(self, shift: BV) -> "HalmosBitVec": + def ashr(self, shift: BV) -> "DolmosBitVec": """ Arithmetic right shift """ @@ -841,81 +841,126 @@ def ashr(self, shift: BV) -> "HalmosBitVec": if shift.is_concrete and shift.value == 0: return self - return HalmosBitVec(self.as_z3() >> shift.value, size=self.size) + return DolmosBitVec(self.as_z3() >> shift.value, size=self.size) + + def clz(self) -> "DolmosBitVec": + """ + Count Leading Zeros — EVM opcode CLZ (0x1E, EIP-7939 / Fusaka). + + Stack semantics: [x] -> [clz(x)] + clz(0) == size (256 for a standard EVM word) + clz(1) == 255 + clz(2^255) == 0 + + Concrete: O(1) via int.bit_length(). + Symbolic: binary-search tree of 8 nested If() nodes (one per + bit-doubling level: 128/64/32/16/8/4/2/1), O(log n) Z3 terms. + + Algorithm: at each level `shift`, inspect the top `shift` bits of cur. + - If zero: add `shift` to acc, slide window left to expose next band. + - If nonzero: isolate this band for the next level. + """ + size = self._size # 256 in standard EVM context + + # --- concrete fast path --- + if self.is_concrete: + v = self._value + return DolmosBitVec(size if v == 0 else size - v.bit_length(), size=size) + + # --- symbolic path: binary search over bit-levels --- + x = self.as_z3() + zero = BitVecVal(0, size) + + acc = zero + cur = x + + for shift in (128, 64, 32, 16, 8, 4, 2, 1): + top_bits = LShR(cur, BitVecVal(size - shift, size)) + top_zero = top_bits == zero + acc = If(top_zero, acc + BitVecVal(shift, size), acc) + cur = If( + top_zero, + cur << BitVecVal(shift, size), # expose next band at MSB + top_bits << BitVecVal(size - shift, size), # keep current band aligned + ) + + # x == 0 -> every bit is a leading zero, result is `size`. + result = If(x == zero, BitVecVal(size, size), acc) + return DolmosBitVec(result, size=size) def bitwise_not(self) -> BV: if self.is_concrete: - return HalmosBitVec(~self._value & ((1 << self._size) - 1), size=self._size) + return DolmosBitVec(~self._value & ((1 << self._size) - 1), size=self._size) - return HalmosBitVec(~self.as_z3(), size=self.size) + return DolmosBitVec(~self.as_z3(), size=self.size) def bitwise_and(self, other: BV) -> BV: assert self._size == other._size - return HalmosBitVec(self._value & other._value, size=self._size) + return DolmosBitVec(self._value & other._value, size=self._size) def bitwise_or(self, other: BV) -> BV: assert self._size == other._size - return HalmosBitVec(self._value | other._value, size=self._size) + return DolmosBitVec(self._value | other._value, size=self._size) def bitwise_xor(self, other: BV) -> BV: assert self._size == other._size - return HalmosBitVec(self._value ^ other._value, size=self._size) + return DolmosBitVec(self._value ^ other._value, size=self._size) - def ult(self, other: BV) -> HalmosBool: + def ult(self, other: BV) -> DolmosBool: assert self._size == other._size if self.is_concrete and other.is_concrete: - return HalmosBool(self.value < other.value) + return DolmosBool(self.value < other.value) - return HalmosBool(ULT(self.as_z3(), other.as_z3())) + return DolmosBool(ULT(self.as_z3(), other.as_z3())) - def ugt(self, other: BV) -> HalmosBool: + def ugt(self, other: BV) -> DolmosBool: assert self._size == other._size if not self._symbolic and not other._symbolic: return TRUE if self.value > other.value else FALSE - return HalmosBool(UGT(self.as_z3(), other.as_z3())) + return DolmosBool(UGT(self.as_z3(), other.as_z3())) - def slt(self, other: BV) -> HalmosBool: + def slt(self, other: BV) -> DolmosBool: assert self._size == other._size if self.is_concrete and other.is_concrete: left = to_signed(self._value, self._size) right = to_signed(other._value, other._size) - return HalmosBool(left < right) + return DolmosBool(left < right) - return HalmosBool(self.as_z3() < other.as_z3()) + return DolmosBool(self.as_z3() < other.as_z3()) - def sgt(self, other: BV) -> HalmosBool: + def sgt(self, other: BV) -> DolmosBool: assert self._size == other._size if self.is_concrete and other.is_concrete: left = to_signed(self._value, self._size) right = to_signed(other._value, other._size) - return HalmosBool(left > right) + return DolmosBool(left > right) - return HalmosBool(self.as_z3() > other.as_z3()) + return DolmosBool(self.as_z3() > other.as_z3()) - def ule(self, other: BV) -> HalmosBool: + def ule(self, other: BV) -> DolmosBool: assert self._size == other._size if self.is_concrete and other.is_concrete: - return HalmosBool(self.value <= other.value) + return DolmosBool(self.value <= other.value) - return HalmosBool(ULE(self.as_z3(), other.as_z3())) + return DolmosBool(ULE(self.as_z3(), other.as_z3())) - def uge(self, other: BV) -> HalmosBool: + def uge(self, other: BV) -> DolmosBool: assert self._size == other._size if self.is_concrete and other.is_concrete: - return HalmosBool(self.value >= other.value) + return DolmosBool(self.value >= other.value) - return HalmosBool(UGE(self.as_z3(), other.as_z3())) + return DolmosBool(UGE(self.as_z3(), other.as_z3())) - def eq(self, other: BV) -> HalmosBool: + def eq(self, other: BV) -> DolmosBool: assert self._size == other._size - return HalmosBool(self._value == other._value) + return DolmosBool(self._value == other._value) def byte(self, idx: int, *, output_size: int = 8) -> BV: """ @@ -937,28 +982,28 @@ def byte(self, idx: int, *, output_size: int = 8) -> BV: assert idx >= 0 if idx >= byte_length: - return HalmosBitVec(0, size=output_size) + return DolmosBitVec(0, size=output_size) if self.is_concrete: b = self._value.to_bytes(length=byte_length, byteorder="big") - return HalmosBitVec(b[idx], size=output_size) + return DolmosBitVec(b[idx], size=output_size) # symbolic case lo = (byte_length - 1 - idx) * 8 hi = lo + 7 - return HalmosBitVec( + return DolmosBitVec( Extract(hi, lo, self._value), size=output_size, ) # initialize global constants -TRUE = object.__new__(HalmosBool) -FALSE = object.__new__(HalmosBool) +TRUE = object.__new__(DolmosBool) +FALSE = object.__new__(DolmosBool) TRUE.con_val = True TRUE.sym_val = None FALSE.con_val = False FALSE.sym_val = None -ZERO = HalmosBitVec(0, size=256) -ONE = HalmosBitVec(1, size=256) +ZERO = DolmosBitVec(0, size=256) +ONE = DolmosBitVec(1, size=256) diff --git a/src/dolmos/build.py b/src/dolmos/build.py new file mode 100644 index 000000000..7426990bf --- /dev/null +++ b/src/dolmos/build.py @@ -0,0 +1,474 @@ +# SPDX-License-Identifier: AGPL-3.0 + +import json +import os +import posixpath +import re +import traceback + +from eth_hash.auto import keccak + +from dolmos.calldata import str_abi +from dolmos.config import Config as DolmosConfig +from dolmos.logs import PARSING_ERROR, debug, warn_code +from dolmos.mapper import Mapper, SourceFileMap +from dolmos.ui import ui + +SOLIDITY_EXTENSIONS = (".sol",) +VYPER_EXTENSIONS = (".vy", ".vyi") + +# build output groups are keyed by compiler version; vyper groups get this prefix +# so that they never collide with solc versions (e.g. vyper 0.4.3 vs solc 0.4.3) +VYPER_VERSION_PREFIX = "vyper:" + +FORGE_CACHE_FILE = os.path.join("cache", "solidity-files-cache.json") + + +def is_vyper_file(filename: str) -> bool: + return filename.endswith(VYPER_EXTENSIONS) + + +def is_vyper_group(compiler_version: str) -> bool: + return compiler_version.startswith(VYPER_VERSION_PREFIX) + + +def is_vyper_contract(contract_json: dict) -> bool: + return contract_json.get("language") == "vyper" + + +def get_source_path(contract_json: dict, default: str | None = None) -> str | None: + """ + Return the source path of a build artifact (e.g. `test/Foo.t.sol`). + + solc artifacts carry it in their AST; vyper artifacts get it from the forge + cache during normalization (see `normalize_vyper_artifact`). + """ + if path := contract_json.get("sourcePath"): + return path + try: + return contract_json["ast"]["absolutePath"] + except (KeyError, TypeError): + return default + + +def _artifact_key(path: str) -> str: + """Normalize an artifact path to a platform-independent key (`/` separators).""" + return posixpath.normpath(path.replace("\\", "/")) + + +def load_forge_cache(root: str, out_path: str) -> dict: + """ + Return a mapping from artifact path (relative to the build output directory, + e.g. `Counter.vy/Counter.json`) to a (source path, compiler version) pair. + + Vyper artifacts emitted by forge only contain the abi and the bytecode, so the + forge cache is the only place where the source path and compiler version live. + Best effort: returns an empty mapping if the cache is missing or unreadable. + """ + cache_path = os.path.join(root, FORGE_CACHE_FILE) + result = {} + + try: + with open(cache_path, encoding="utf8") as f: + cache = json.load(f) + except (OSError, ValueError) as err: + debug(f"could not read forge cache {cache_path}: {err}") + return result + + for source_path, entry in cache.get("files", {}).items(): + for versions in entry.get("artifacts", {}).values(): + for version, profiles in versions.items(): + for artifact in profiles.values(): + artifact_path = artifact.get("path") + if not artifact_path: + continue + # paths are relative to the out dir; tolerate an `out/` prefix + artifact_path = _artifact_key(artifact_path) + out_prefix = os.path.basename(os.path.normpath(out_path)) + "/" + if artifact_path.startswith(out_prefix): + artifact_path = artifact_path[len(out_prefix) :] + result[artifact_path] = (source_path, version) + + return result + + +_DOCSTRING = r'(?:"""(?P.*?)"""|\'\'\'(?P.*?)\'\'\')' + +# module docstring: the first string literal of the file, possibly after comments +# such as `# pragma version ...` +_VYPER_MODULE_DOCSTRING = re.compile(r"\A(?:\s*#[^\n]*\n|\s+)*" + _DOCSTRING, re.DOTALL) + +# function docstring: first string literal right after the (possibly multiline) signature +_VYPER_FUNCTION_DOCSTRING = re.compile( + r"^[ \t]*def[ \t]+(?P\w+)[ \t]*\((?:[^()]|\([^()]*\))*\)" + r"(?:[ \t]*->[^:\n]+)?[ \t]*:[ \t]*(?:#[^\n]*)?\n\s*" + _DOCSTRING, + re.DOTALL | re.MULTILINE, +) + + +def _docstring_text(match: re.Match) -> str: + return match.group("doc") if match.group("doc") is not None else match.group("doc2") + + +def parse_vyper_docstrings(source: str) -> tuple[str | None, dict[str, str]]: + """ + Extract the module docstring and the per-function docstrings of a vyper source. + + Returns (module docstring or None, function name -> docstring). + """ + module_doc = None + if match := _VYPER_MODULE_DOCSTRING.match(source): + module_doc = _docstring_text(match) + + function_docs = {} + for match in _VYPER_FUNCTION_DOCSTRING.finditer(source): + function_docs.setdefault(match.group("name"), _docstring_text(match)) + + return module_doc, function_docs + + +def normalize_vyper_artifact( + json_out: dict, dirname: str, root: str, cache_entry +) -> tuple[str, str, dict | None]: + """ + Bring a forge vyper artifact into the shape that dolmos expects from solc artifacts. + + forge only emits `abi`, `bytecode`, `deployedBytecode`, an empty `methodIdentifiers` + and an `id` for vyper, so we fill in: + - `methodIdentifiers`, computed from the abi + - `bytecode.linkReferences` (vyper has no libraries) + - `metadata.compiler.version` and `metadata.output.devdoc` (for `@custom:dolmos`) + - `sourcePath` and `language` + + Returns (contract type, compiler version group key, natspec). + """ + source_path, version = cache_entry if cache_entry else (dirname, "unknown") + + json_out["language"] = "vyper" + json_out["sourcePath"] = source_path + + if not json_out.get("methodIdentifiers"): + json_out["methodIdentifiers"] = { + (sig := str_abi(item)): keccak(sig.encode()).hex()[:8] + for item in json_out.get("abi", []) + if item.get("type") == "function" + } + + for key in ("bytecode", "deployedBytecode"): + entry = json_out.get(key) + if isinstance(entry, str): + entry = {"object": entry} + entry = entry or {"object": "0x"} + entry.setdefault("object", "0x") + entry.setdefault("linkReferences", {}) + json_out[key] = entry + + # vyper modules are always contracts, .vyi files are always interfaces + contract_type = "interface" if dirname.endswith(".vyi") else "contract" + + # `@custom:dolmos` annotations live in docstrings; forge does not give us the + # devdoc for vyper, so read them straight from the source + natspec = None + devdoc_methods = {} + try: + with open(os.path.join(root, source_path), encoding="utf8") as f: + module_doc, function_docs = parse_vyper_docstrings(f.read()) + + if module_doc: + natspec = {"text": module_doc} + + for funsig in json_out["methodIdentifiers"]: + doc = function_docs.get(funsig.split("(")[0]) + if doc and (options := parse_natspec({"text": doc})): + devdoc_methods[funsig] = {"custom:dolmos": options} + except OSError as err: + debug(f"could not read vyper source {source_path}: {err}") + + metadata = json_out.setdefault("metadata", {}) + metadata.setdefault("compiler", {}).setdefault("version", version) + metadata.setdefault("output", {}).setdefault("devdoc", {}).setdefault( + "methods", {} + ).update(devdoc_methods) + + return contract_type, VYPER_VERSION_PREFIX + version, natspec + + +def get_contract_type( + ast_nodes: list, contract_name: str +) -> tuple[str | None, str | None]: + for node in ast_nodes: + if node["nodeType"] == "ContractDefinition" and node["name"] == contract_name: + abstract = "abstract " if node.get("abstract") else "" + contract_type = abstract + node["contractKind"] + natspec = node.get("documentation") + return contract_type, natspec + + return None, None + + +def parse_build_out(args: DolmosConfig) -> dict: + result = {} # compiler version -> source filename -> contract name -> (json, type) + + coverage_output = args.coverage_output + root = args.root + + if coverage_output: + SourceFileMap().set_root(root) + + out_path = os.path.join(root, args.forge_build_out) + if not os.path.exists(out_path): + raise FileNotFoundError( + f"The build output directory `{out_path}` does not exist" + ) + + ui.update_status(f"Parsing {out_path}") + + # only needed for vyper artifacts, loaded lazily + forge_cache = None + + for sol_dirname in os.listdir(out_path): # for each source filename + if not sol_dirname.endswith(SOLIDITY_EXTENSIONS + VYPER_EXTENSIONS): + continue + + sol_path = os.path.join(out_path, sol_dirname) + if not os.path.isdir(sol_path): + continue + + for json_filename in os.listdir(sol_path): # for each contract name + try: + if not json_filename.endswith(".json"): + continue + if json_filename.startswith("."): + continue + + json_path = os.path.join(sol_path, json_filename) + with open(json_path, encoding="utf8") as f: + json_out = json.load(f) + + # cut off compiler version number as well + contract_name = json_filename.split(".")[0] + + if is_vyper_file(sol_dirname): + if forge_cache is None: + forge_cache = load_forge_cache(root, out_path) + + cache_entry = forge_cache.get( + _artifact_key(f"{sol_dirname}/{json_filename}") + ) + contract_type, compiler_version, natspec = normalize_vyper_artifact( + json_out, sol_dirname, root, cache_entry + ) + + # note: coverage is not supported for vyper (no source maps), + # and vyper file ids would clash with solc ones + add_to_build_out( + result, + compiler_version, + sol_dirname, + contract_name, + (json_out, contract_type, natspec), + ) + parse_symbols( + args, result[compiler_version][sol_dirname], contract_name + ) + continue + + ast = json_out["ast"] + + if coverage_output: + # record the mapping between file id and file path + SourceFileMap().add_mapping(json_out["id"], ast["absolutePath"]) + + ast_nodes = ast["nodes"] + contract_type, natspec = get_contract_type(ast_nodes, contract_name) + + # can happen to solidity files for multiple reasons: + # - import only (like console2.log) + # - defines only structs or enums + # - defines only free functions + # - ... + if contract_type is None: + debug(f"Skipped {json_filename}, no contract definition found") + continue + + compiler_version = json_out["metadata"]["compiler"]["version"] + add_to_build_out( + result, + compiler_version, + sol_dirname, + contract_name, + (json_out, contract_type, natspec), + ) + parse_symbols( + args, result[compiler_version][sol_dirname], contract_name + ) + + except Exception as err: + warn_code( + PARSING_ERROR, + f"Skipped {json_filename} due to parsing failure: {type(err).__name__}: {err}", + ) + if args.debug: + traceback.print_exc() + continue + + ui.stop_status() + return result + + +def add_to_build_out( + result: dict, compiler_version: str, filename: str, contract_name: str, entry +) -> None: + contract_map = result.setdefault(compiler_version, {}).setdefault(filename, {}) + + if contract_name in contract_map: + raise ValueError( + "duplicate contract names in the same file", + contract_name, + filename, + ) + + contract_map[contract_name] = entry + + +def parse_symbols(args: DolmosConfig, contract_map: dict, contract_name: str) -> None: + try: + json_out = contract_map[contract_name][0] + + # workaround: solx does not emit bytecode at all for library contracts + # default to an empty object to emulate solc behavior + bytecode = json_out.get("bytecode", {"object": "0x"})["object"] + contract_mapping_info = Mapper().get_or_create(contract_name) + contract_mapping_info.bytecode = bytecode + + # vyper artifacts have no (solc-style) ast + if "ast" in json_out: + Mapper().parse_ast(json_out["ast"]) + + except Exception: + debug(f"error parsing symbols for contract {contract_name}") + debug(traceback.format_exc()) + + # we parse symbols as best effort, don't propagate exceptions + pass + + +# natspec tags carrying command line options; @custom:halmos is still accepted so +# that test suites written for halmos keep working unchanged +NATSPEC_TAGS = ("dolmos", "halmos") + + +def parse_devdoc(funsig: str, contract_json: dict) -> str | None: + try: + method_doc = contract_json["metadata"]["output"]["devdoc"]["methods"][funsig] + except KeyError: + return None + + values = [ + method_doc[f"custom:{tag}"] + for tag in NATSPEC_TAGS + if f"custom:{tag}" in method_doc + ] + return " ".join(values) if values else None + + +def parse_natspec(natspec: dict) -> str: + # This parsing scheme is designed to handle: + # + # - multiline tags: + # /// @custom:dolmos --x + # /// --y + # + # - multiple tags: + # /// @custom:dolmos --x + # /// @custom:dolmos --y + # + # - tags that start in the middle of line: + # /// blah blah @custom:dolmos --x + # /// --y + # + # In all the above examples, this scheme returns "--x (whitespaces) --y" + # (@custom:halmos is accepted as well, see NATSPEC_TAGS) + tags = {f"@custom:{tag}" for tag in NATSPEC_TAGS} + is_options_tag = False + result = "" + for item in re.split(r"(@\S+)", natspec.get("text", "")): + if item in tags: + is_options_tag = True + elif re.match(r"^@\S", item): + is_options_tag = False + elif is_options_tag: + result += item + return result.strip() + + +def import_libs(build_out_map: dict, hexcode: str, linkReferences: dict) -> dict: + libs = {} + + for filepath in linkReferences: + file_name = filepath.split("/")[-1] + + for lib_name in linkReferences[filepath]: + (lib_json, _, _) = build_out_map[file_name][lib_name] + lib_hexcode = lib_json["deployedBytecode"]["object"] + + # in bytes, multiply indices by 2 and offset 0x + placeholder_index = linkReferences[filepath][lib_name][0]["start"] * 2 + 2 + placeholder = hexcode[placeholder_index : placeholder_index + 40] + + libs[f"{filepath}:{lib_name}"] = { + "placeholder": placeholder, + "hexcode": lib_hexcode, + } + + return libs + + +def has_vyper_contracts(build_out: dict) -> bool: + return any(is_vyper_group(version) for version in build_out) + + +def build_out_view(build_out: dict, compiler_version: str) -> dict: + """ + Return the build output map visible to test contracts of the given group. + + Test contracts normally only see contracts compiled with the same compiler version + (e.g. for library linking and bytecode lookups). Cross-language setups are common + though (solidity tests for vyper contracts, and vice versa), so: + - solidity groups also see every vyper contract + - vyper groups see every vyper contract, and the solidity contracts if there is + a single solc version (otherwise the lookup would be ambiguous) + + Solidity and vyper filenames can't collide since they have different extensions. + """ + own = build_out[compiler_version] + vyper_groups = [v for v in build_out if is_vyper_group(v)] + solc_groups = [v for v in build_out if not is_vyper_group(v)] + + if is_vyper_group(compiler_version): + shared = [v for v in vyper_groups if v != compiler_version] + if len(solc_groups) == 1: + shared += solc_groups + else: + shared = vyper_groups + + if not shared: + return own + + view = dict(own) + for version in sorted(shared): + for filename, contracts in build_out[version].items(): + view.setdefault(filename, contracts) + return view + + +def build_output_iterator(build_out: dict): + for compiler_version in sorted(build_out): + build_out_map = build_out[compiler_version] + + # computed once per group, so that the BuildOut singleton can cache it + view = build_out_view(build_out, compiler_version) + + for filename in sorted(build_out_map): + for contract_name in sorted(build_out_map[filename]): + yield (view, filename, contract_name) diff --git a/src/halmos/bytevec.py b/src/dolmos/bytevec.py similarity index 99% rename from src/halmos/bytevec.py rename to src/dolmos/bytevec.py index a84d069ae..258de25ff 100644 --- a/src/halmos/bytevec.py +++ b/src/dolmos/bytevec.py @@ -7,9 +7,9 @@ from sortedcontainers import SortedDict from z3 import BitVecRef, If, eq, is_bool, is_bv, is_bv_value, simplify, substitute -from halmos.bitvec import HalmosBitVec as BV -from halmos.logs import warn -from halmos.utils import ( +from dolmos.bitvec import DolmosBitVec as BV +from dolmos.logs import warn +from dolmos.utils import ( Byte, Word, bv_value_to_bytes, diff --git a/src/halmos/calldata.py b/src/dolmos/calldata.py similarity index 97% rename from src/halmos/calldata.py rename to src/dolmos/calldata.py index 8d35cd4cc..08f37fb48 100644 --- a/src/halmos/calldata.py +++ b/src/dolmos/calldata.py @@ -10,10 +10,10 @@ BitVecRef, ) -from halmos.bytevec import ByteVec -from halmos.config import Config as HalmosConfig -from halmos.logs import debug_once -from halmos.utils import con, uid +from dolmos.bytevec import ByteVec +from dolmos.config import Config as DolmosConfig +from dolmos.logs import debug_once +from dolmos.utils import con, uid @dataclass(frozen=True) @@ -108,7 +108,7 @@ class Calldata: # For dynamic parameters not explicitly listed in --array-lengths, default sizes are used: # - For dynamic arrays: the size ranges from 0 to the value of --loop (inclusive). # - For bytes or strings: the size candidates are given by --default-bytes-lengths. - args: HalmosConfig + args: DolmosConfig # `dyn_params` will be updated to include the fully resolved size information for all dynamic parameters. dyn_params: list[DynamicParam] @@ -119,7 +119,7 @@ class Calldata: def __init__( self, - args: HalmosConfig, + args: DolmosConfig, new_symbol_id: Callable | None, ) -> None: self.args = args @@ -329,7 +329,7 @@ def get_abi(contract_json: dict) -> dict: def mk_calldata( abi: dict, fun_info: FunctionInfo, - args: HalmosConfig, + args: DolmosConfig, new_symbol_id: Callable = None, ) -> tuple[ByteVec, list[DynamicParam]]: return Calldata(args, new_symbol_id).create(abi, fun_info) diff --git a/src/halmos/cheatcodes.py b/src/dolmos/cheatcodes.py similarity index 86% rename from src/halmos/cheatcodes.py rename to src/dolmos/cheatcodes.py index 73452180e..eb0f0b316 100644 --- a/src/halmos/cheatcodes.py +++ b/src/dolmos/cheatcodes.py @@ -1,6 +1,7 @@ # SPDX-License-Identifier: AGPL-3.0 import json +import os import re from contextlib import suppress from dataclasses import dataclass @@ -25,27 +26,34 @@ unsat, ) -from halmos import env -from halmos.assertions import assert_cheatcode_handler -from halmos.bitvec import HalmosBitVec as BV -from halmos.bitvec import HalmosBool as Bool -from halmos.bytevec import ByteVec -from halmos.calldata import ( +from dolmos import env +from dolmos.assertions import assert_cheatcode_handler +from dolmos.bitvec import DolmosBitVec as BV +from dolmos.bitvec import DolmosBool as Bool +from dolmos.bytevec import ByteVec +from dolmos.calldata import ( FunctionInfo, get_abi, mk_calldata, ) -from halmos.constants import MAX_MEMORY_SIZE -from halmos.exceptions import ( +from dolmos.constants import MAX_MEMORY_SIZE +from dolmos.exceptions import ( + DolmosException, FailCheatcode, - HalmosException, InfeasiblePath, NotConcreteError, OutOfGasError, ) -from halmos.logs import debug -from halmos.mapper import BuildOut -from halmos.utils import ( +from dolmos.expectations import ( + EMIT_SIGNATURES, + REVERT_SIGNATURES, + parse_expect_emit, + parse_expect_revert, +) +from dolmos.fs import parse_hex_bytes, read_file +from dolmos.logs import debug +from dolmos.mapper import BuildOut +from dolmos.utils import ( Address, BitVecSort8, BitVecSort160, @@ -194,7 +202,7 @@ def lookup(self, to: BV) -> PrankResult: """ assert_address(to) - if self and to not in [halmos_cheat_code.address, hevm_cheat_code.address]: + if self and to not in [svm_cheat_code.address, hevm_cheat_code.address]: result = self.active if not self.keep: self.stopPrank() @@ -231,7 +239,7 @@ def symbolic_storage(ex, arg, sevm, stack): if account_alias is None: error_msg = f"enableSymbolicStorage() or setArbitraryStorage() is not allowed for a nonexistent account: {hexify(account)}" - raise HalmosException(error_msg) + raise DolmosException(error_msg) ex.storage[account_alias].symbolic = True @@ -246,7 +254,7 @@ def snapshot_storage(ex, arg, sevm, stack): if account_alias is None: error_msg = f"snapshotStorage() is not allowed for a nonexistent account: {hexify(account)}" - raise HalmosException(error_msg) + raise DolmosException(error_msg) zero_pad = b"\x00" * 16 return ByteVec(zero_pad + ex.storage[account_alias].digest()) @@ -299,10 +307,10 @@ def _get_contract_name(ex, arg) -> tuple[str | None, str | None]: ) if not (code := ex.code.get(addr)): - raise HalmosException(f"createCalldata: not contract account: {hexify(addr)}") + raise DolmosException(f"createCalldata: not contract account: {hexify(addr)}") if not (contract_name := code.contract_name): - raise HalmosException( + raise DolmosException( f"createCalldata: couldn't find the contract name for: {hexify(addr)}" ) @@ -436,14 +444,14 @@ def create_generic(ex, bits: int, var_name: str, type_name: str) -> BitVecRef | if not bits: return ByteVec() - label = f"halmos_{var_name}_{type_name}_{uid()}_{ex.new_symbol_id():>02}" + label = f"dolmos_{var_name}_{type_name}_{uid()}_{ex.new_symbol_id():>02}" return BitVec(label, BitVecSorts[bits]) def create_uint(ex, arg, name: str | None = None, **kwargs): bits = int_of(arg.get_word(4), "symbolic bit size for svm.createUint()") if bits > 256: - raise HalmosException(f"bitsize larger than 256: {bits}") + raise DolmosException(f"bitsize larger than 256: {bits}") name = name or name_of(extract_string_argument(arg, 1)) return ByteVec(uint256(create_generic(ex, bits, name, f"uint{bits}"))) @@ -457,7 +465,7 @@ def create_uint256(ex, arg, name: str | None = None, **kwargs): def create_int(ex, arg, name: str | None = None, **kwargs): bits = int_of(extract_word(arg, 4), "symbolic bit size for svm.createUint()") if bits > 256: - raise HalmosException(f"bitsize larger than 256: {bits}") + raise DolmosException(f"bitsize larger than 256: {bits}") name = name or name_of(extract_string_argument(arg, 1)) return ByteVec(int256(create_generic(ex, bits, name, f"int{bits}"))) @@ -521,7 +529,7 @@ def create_uint256_min_max(ex, arg, name: str | None = None, **kwargs): symbolic_value = create_generic(ex, 256, name, "uint256") if min_value > max_value: - raise HalmosException(f"expected min={min_value} <= max={max_value}") + raise DolmosException(f"expected min={min_value} <= max={max_value}") # Add constraints for the symbolic value to be within the specified range min_condition = simplify(UGE(symbolic_value, min_value)) @@ -595,6 +603,44 @@ def env_int(arg, **kwargs): return ByteVec(int_val) +def concrete_string_argument(arg, arg_idx: int, cheatcode: str) -> str: + value = extract_string_argument(arg, arg_idx) + if not isinstance(value, str): + raise NotConcreteError(f"{cheatcode}: expected a concrete string, got {value}") + return value + + +def read_file_cheatcode(sevm, arg) -> ByteVec: + """vm.readFile(string path) returns (string)""" + path = concrete_string_argument(arg, 0, "vm.readFile") + data = read_file(sevm.options.root, path, "vm.readFile") + try: + # like foundry, reject files that are not valid utf-8 text + data.decode("utf-8") + except UnicodeDecodeError as e: + msg = f"vm.readFile: {path} is not valid UTF-8 (use vm.readFileBinary): {e}" + raise DolmosException(msg) from e + return encode_tuple_bytes(data) + + +def read_file_binary_cheatcode(sevm, arg) -> ByteVec: + """vm.readFileBinary(string path) returns (bytes)""" + path = concrete_string_argument(arg, 0, "vm.readFileBinary") + return encode_tuple_bytes(read_file(sevm.options.root, path, "vm.readFileBinary")) + + +def parse_bytes_cheatcode(arg) -> ByteVec: + """vm.parseBytes(string) returns (bytes)""" + value = concrete_string_argument(arg, 0, "vm.parseBytes") + return encode_tuple_bytes(parse_hex_bytes(value, "vm.parseBytes")) + + +def project_root_cheatcode(sevm) -> ByteVec: + """vm.projectRoot() returns (string)""" + root = os.path.abspath(sevm.options.root) + return encode_tuple_bytes(root.encode("utf-8")) + + def abi_encode_array_words(values: list[Bool | Address | Word]) -> ByteVec: result = ByteVec() @@ -875,7 +921,7 @@ def apply_vmaddr(ex, private_key: Word): return addr -class halmos_cheat_code: +class svm_cheat_code: # address constant SVM_ADDRESS = # address(bytes20(uint160(uint256(keccak256('svm cheat code'))))); address = BV(0xF3993A62377BCD56AE39D773740A5390411E8BC9, size=160) @@ -905,13 +951,13 @@ class halmos_cheat_code: @staticmethod def handle(sevm, ex, arg: ByteVec, stack) -> list[BitVecRef]: - funsig = int_of(extract_funsig(arg), "symbolic halmos cheatcode") - if handler := halmos_cheat_code.handlers.get(funsig): + funsig = int_of(extract_funsig(arg), "symbolic svm cheatcode") + if handler := svm_cheat_code.handlers.get(funsig): result = handler(ex, arg, sevm=sevm, stack=stack) return result if isinstance(result, list) else [result] - error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" - raise HalmosException(error_msg) + error_msg = f"Unknown svm cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" + raise DolmosException(error_msg) class hevm_cheat_code: @@ -958,6 +1004,21 @@ class hevm_cheat_code: # bytes4(keccak256("deal(address,uint256)")) deal_sig: int = 0xC88A5E6D + # bytes4(keccak256("getNonce(address)")) + get_nonce_sig: int = 0x2D0335AB + + # bytes4(keccak256("getNonce((address,uint256,uint256,uint256))")) + get_nonce_wallet_sig: int = 0xA5748AAD + + # bytes4(keccak256("setNonce(address,uint64)")) + set_nonce_sig: int = 0xF8E18B57 + + # bytes4(keccak256("setNonceUnsafe(address,uint64)")) + set_nonce_unsafe_sig: int = 0x9B67B21C + + # bytes4(keccak256("resetNonce(address)")) + reset_nonce_sig: int = 0x1C72346D + # bytes4(keccak256("store(address,bytes32,bytes32)")) store_sig: int = 0x70CA10BB @@ -1099,6 +1160,18 @@ class hevm_cheat_code: # bytes4(keccak256("envExists(string)")) env_exists_sig: int = 0xCE8365F9 + # bytes4(keccak256("readFile(string)")) + read_file_sig: int = 0x60F9BB11 + + # bytes4(keccak256("readFileBinary(string)")) + read_file_binary_sig: int = 0x16ED7BC4 + + # bytes4(keccak256("parseBytes(string)")) + parse_bytes_sig: int = 0x8F5D232D + + # bytes4(keccak256("projectRoot()")) + project_root_sig: int = 0xD930A0E6 + @staticmethod def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: funsig: int = int_of(arg[:4].unwrap(), "symbolic hevm cheatcode") @@ -1134,9 +1207,17 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: path_len = arg.get_word(36) path = arg[68 : 68 + path_len].unwrap().decode("utf-8") + out_dir = sevm.options.forge_build_out if ":" in path: + # `File.sol:Name`, `path/to/File.vy:Name` [filename, contract_name] = path.split(":") - path = "out/" + filename + "/" + contract_name + ".json" + filename = os.path.basename(filename) + path = f"{out_dir}/{filename}/{contract_name}.json" + elif path.endswith((".sol", ".vy")): + # `File.sol`, `path/to/File.vy`: the contract named after the file + filename = os.path.basename(path) + contract_name = filename.rsplit(".", 1)[0] + path = f"{out_dir}/{filename}/{contract_name}.json" target = sevm.options.root.rstrip("/") path = target + "/" + path @@ -1156,7 +1237,7 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: sender = uint160(arg.get_word(4)).as_z3() result = ex.context.prank.prank(sender) if not result: - raise HalmosException( + raise DolmosException( "can not call vm.prank(address) with an active prank" ) return ret @@ -1167,7 +1248,7 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: origin = uint160(arg.get_word(36)).as_z3() result = ex.context.prank.prank(sender, origin) if not result: - raise HalmosException( + raise DolmosException( "can not call vm.prank(address, address) with an active prank" ) return ret @@ -1177,7 +1258,7 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: address = uint160(arg.get_word(4)).as_z3() result = ex.context.prank.startPrank(address) if not result: - raise HalmosException( + raise DolmosException( "can not call vm.startPrank(address) with an active prank" ) return ret @@ -1188,7 +1269,7 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: origin = uint160(arg.get_word(36)).as_z3() result = ex.context.prank.startPrank(sender, origin) if not result: - raise HalmosException( + raise DolmosException( "can not call vm.startPrank(address, address) with an active prank" ) return ret @@ -1205,6 +1286,63 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: ex.balance_update(who, amount) return ret + # vm.getNonce(address) / vm.getNonce(Wallet) + elif funsig in ( + hevm_cheat_code.get_nonce_sig, + hevm_cheat_code.get_nonce_wallet_sig, + ): + # Wallet is a static struct, its first field is the address + who = uint160(arg.get_word(4)).as_z3() + return ByteVec(con(ex.nonce_of(who))) + + # vm.setNonce(address,uint64) / vm.setNonceUnsafe(address,uint64) + elif funsig in ( + hevm_cheat_code.set_nonce_sig, + hevm_cheat_code.set_nonce_unsafe_sig, + ): + unsafe = funsig == hevm_cheat_code.set_nonce_unsafe_sig + name = "setNonceUnsafe" if unsafe else "setNonce" + + who = uint160(arg.get_word(4)) + if not who.is_concrete: + error_msg = f"vm.{name}(address who, uint64 nonce) must have concrete argument `who` but received {who}" + raise DolmosException(error_msg) + + nonce = int_of(arg.get_word(36), f"symbolic nonce in vm.{name}()") + if not (0 <= nonce < 2**64): + raise DolmosException( + f"vm.{name}(): nonce out of uint64 range: {nonce}" + ) + + who = who.as_z3() + current = ex.nonce_of(who) + + # vm.setNonce() can only increase the nonce, as in foundry + if not unsafe and nonce < current: + error_msg = ( + f"vm.setNonce(): the new nonce ({nonce}) must be greater than or equal to " + f"the current nonce ({current}) of {hexify(who)}; " + f"use vm.setNonceUnsafe() to decrease it" + ) + raise DolmosException(error_msg) + + ex.set_nonce(who, nonce) + return ret + + # vm.resetNonce(address) + elif funsig == hevm_cheat_code.reset_nonce_sig: + who = uint160(arg.get_word(4)) + if not who.is_concrete: + error_msg = f"vm.resetNonce(address who) must have concrete argument `who` but received {who}" + raise DolmosException(error_msg) + + who = who.as_z3() + + # 0 for EOAs, 1 for contract accounts + code = ex.code.get(who) + ex.set_nonce(who, 1 if code is not None and len(code) > 0 else 0) + return ret + # vm.store(address,bytes32,bytes32) elif funsig == hevm_cheat_code.store_sig: if arg == hevm_cheat_code.fail_payload: @@ -1221,7 +1359,7 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: if store_account_alias is None: error_msg = f"vm.store() is not allowed for a nonexistent account: {hexify(store_account)}" - raise HalmosException(error_msg) + raise DolmosException(error_msg) store_slot = uint256(arg.get_word(36)) store_value = uint256(arg.get_word(68)) @@ -1281,7 +1419,7 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: if not who.is_concrete: error_msg = f"vm.etch(address who, bytes code) must have concrete argument `who` but received {who}" - raise HalmosException(error_msg) + raise DolmosException(error_msg) # code must be concrete code_offset = int_of(arg.get_word(36), "symbolic code offset") @@ -1307,7 +1445,7 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: elif funsig == hevm_cheat_code.ffi_sig: if not sevm.options.ffi: error_msg = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it" - raise HalmosException(error_msg) + raise DolmosException(error_msg) cmd = extract_string_array_argument(arg, 0) @@ -1538,11 +1676,37 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: elif funsig == hevm_cheat_code.env_exists_sig: return env_exists(arg) + # vm.readFile(string) returns (string) + elif funsig == hevm_cheat_code.read_file_sig: + return read_file_cheatcode(sevm, arg) + + # vm.readFileBinary(string) returns (bytes) + elif funsig == hevm_cheat_code.read_file_binary_sig: + return read_file_binary_cheatcode(sevm, arg) + + # vm.parseBytes(string) returns (bytes) + elif funsig == hevm_cheat_code.parse_bytes_sig: + return parse_bytes_cheatcode(arg) + + # vm.projectRoot() returns (string) + elif funsig == hevm_cheat_code.project_root_sig: + return project_root_cheatcode(sevm) + + # vm.expectRevert(...) / vm.expectPartialRevert(...) + elif funsig in REVERT_SIGNATURES: + ex.context.expectations.expect_revert(parse_expect_revert(funsig, arg)) + return ret + + # vm.expectEmit(...) / vm.expectEmitAnonymous(...) + elif funsig in EMIT_SIGNATURES: + ex.context.expectations.expect_emit(parse_expect_emit(funsig, arg)) + return ret + elif funsig in dict_of_unsupported_cheatcodes: msg = f"Unsupported cheat code: {dict_of_unsupported_cheatcodes[funsig]}" - raise HalmosException(msg) + raise DolmosException(msg) else: # TODO: support other cheat codes msg = f"Unsupported cheat code: calldata = {hexify(arg)}" - raise HalmosException(msg) + raise DolmosException(msg) diff --git a/src/halmos/config.py b/src/dolmos/config.py similarity index 86% rename from src/halmos/config.py rename to src/dolmos/config.py index ff9cde8ff..b2e3b9e73 100644 --- a/src/halmos/config.py +++ b/src/dolmos/config.py @@ -15,9 +15,9 @@ import toml -from halmos.logs import warn -from halmos.solvers import SOLVERS, get_solver_command -from halmos.utils import parse_time +from dolmos.logs import warn +from dolmos.solvers import SOLVERS, get_solver_command +from dolmos.utils import parse_time # common strings internal = "internal" @@ -45,13 +45,13 @@ class ConfigSource(IntEnum): # default value, lowest precedence default = 1 - # e.g. halmos.toml + # e.g. dolmos.toml config_file = 2 - # contract-level annotation (e.g. @custom:halmos --some-option) + # contract-level annotation (e.g. @custom:dolmos --some-option) contract_annotation = 3 - # function-level annotation (e.g. @custom:halmos --some-option) + # function-level annotation (e.g. @custom:dolmos --some-option) function_annotation = 4 # from command line, highest precedence @@ -69,6 +69,7 @@ def arg( countable: bool = False, global_default_str: str | None = None, action: Callable = None, + extra_names: list[str] | None = None, ): return dataclass_field( default=None, @@ -79,6 +80,7 @@ def arg( "group": group, "choices": choices, "short": short, + "extra_names": extra_names or [], "countable": countable, "global_default_str": global_default_str, "action": action, @@ -86,6 +88,21 @@ def arg( ) +def split_command(command: str, windows: bool = os.name == "nt") -> list[str]: + """ + Split a command line into its arguments, like a POSIX shell. + + On Windows, backslashes are path separators rather than escape characters + (`C:\\solvers\\yices-smt2.exe` must stay intact); quotes still group words. + """ + if not windows: + return shlex.split(command) + lexer = shlex.shlex(command, posix=True) + lexer.whitespace_split = True + lexer.escape = "" + return list(lexer) + + def ensure_non_empty(values: list | set | dict) -> list: if not values: raise ValueError("required a non-empty list") @@ -211,7 +228,7 @@ def unparse(values: dict[str, list[int]]) -> str: # TODO: add kw_only=True when we support Python>=3.10 @dataclass(frozen=True) class Config: - """Configuration object for halmos. + """Configuration object for dolmos. Don't instantiate this directly, since all fields have default value None. Instead, use: @@ -259,8 +276,8 @@ class Config: config: str = arg( help="path to the config file", metavar="FILE", - global_default=lambda: os.path.join(os.getcwd(), "halmos.toml"), - global_default_str="ROOT/halmos.toml", + global_default=lambda: os.path.join(os.getcwd(), "dolmos.toml"), + global_default_str="ROOT/dolmos.toml", ) contract: str = arg( @@ -287,6 +304,7 @@ class Config: global_default="", metavar="FUNCTION_NAME_REGEX", short="mt", + extra_names=["-test"], ) panic_error_codes: str = arg( @@ -296,6 +314,11 @@ class Config: action=ParseErrorCodes, ) + invalid_as_failure: bool = arg( + help="treat the INVALID opcode (0xFE) as a test failure, like a Panic(0x01) revert. This is how Vyper compiles `assert ..., UNREACHABLE` (and how solc < 0.8 compiles `assert`). Enabled by default when the build output contains Vyper contracts.", + global_default=False, + ) + invariant_depth: int = arg( help="set depth for invariant testing (length of the stateful sequence of calls)", global_default=2, @@ -308,6 +331,29 @@ class Config: metavar="MAX_BOUND", ) + dump_lassos: str = arg( + help="when the loop unrolling bound is reached, export the loop as a lasso program (PaSTTeL JSON format) in the given directory", + global_default=None, + metavar="LASSO_DIR", + ) + + pasttel: str = arg( + help="path to the PaSTTeL binary: run the termination analysis on each exported lasso (requires --dump-lassos)", + global_default=None, + metavar="PASTTEL_BINARY", + ) + + lasso_exact_constants: bool = arg( + help="encode wrap-arounds exactly in exported lassos, with 2^256 constants (for termination tools with exact arithmetic; PaSTTeL needs the default small-constants encoding)", + global_default=False, + ) + + pasttel_timeout: int = arg( + help="time limit in seconds for each PaSTTeL run", + global_default=30, + metavar="SECONDS", + ) + width: int = arg( help="set the max number of paths; 0 means unlimited", global_default=0, @@ -342,11 +388,19 @@ class Config: ) storage_layout: str = arg( - help="Select one of the available storage layout models. The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul.", + help="Select one of the available storage layout models. The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul. Defaults to generic when the build output contains Vyper contracts.", global_default="solidity", choices=["solidity", "generic"], ) + evm_version: str = arg( + help="EVM version (hard fork) to execute against, e.g. shanghai, cancun, prague, osaka; " + "determines the available opcodes and the semantics of SELFDESTRUCT. " + "Defaults to the evmVersion the test contract was compiled for, or the latest supported fork", + global_default="", + metavar="VERSION", + ) + ffi: bool = arg( help="allow the usage of FFI to call external functions", global_default=False, @@ -471,6 +525,18 @@ class Config: group=debugging, ) + pretty_counterexamples: bool = arg( + help=( + "print exploitable counterexamples: arguments decoded with the ABI, calldata and " + "selectors decoded, concrete call sequences, a forge test replaying each " + "counterexample, duplicates hidden, and potentially invalid counterexamples " + "checked against the real EXP semantics, with the reason when they remain invalid" + ), + global_default=False, + group=debugging, + short="pcex", + ) + dump_smt_queries: bool = arg( help="dump SMT queries for assertion violations", global_default=False, @@ -583,6 +649,15 @@ class Config: group=solver_group, ) + keccak_refinement_rounds: int = arg( + help="when a counterexample relies on keccak values inconsistent with the real hash function, " + "add the real hash values to the query and solve again, at most this many times; " + "a counterexample that is still inconsistent is reported as potentially invalid (0 disables the check)", + global_default=3, + metavar="N", + group=solver_group, + ) + ### Experimental options symbolic_jump: bool = arg( @@ -744,7 +819,7 @@ def resolved_solver_command(self) -> list[str]: f"--solver-command will be used and --solver will be ignored", allow_duplicate=False, ) - return shlex.split(solver_command) + return split_command(solver_command) # if no `--solver-command` is provided, or `--solver` has higher precedence, # we need to resolve `--solver ` to an actual command @@ -775,12 +850,15 @@ def resolve_config_files(args: list[str], include_missing: bool = False) -> list if args.config: return [args.config] - # we expect to find halmos.toml in the project root directory - default_config_path = os.path.join(args.root, "halmos.toml") - if not include_missing and not os.path.exists(default_config_path): - return [] + # we expect to find dolmos.toml (or halmos.toml) in the project root directory + candidates = [ + os.path.join(args.root, name) for name in ("dolmos.toml", "halmos.toml") + ] + for path in candidates: + if os.path.exists(path): + return [path] - return [default_config_path] + return candidates[:1] if include_missing else [] class TomlParser: @@ -849,8 +927,9 @@ def _create_default_config() -> "Config": def _create_arg_parser() -> argparse.ArgumentParser: parser = argparse.ArgumentParser( - prog="halmos", - epilog="For more information, see https://github.com/a16z/halmos", + # use the name the command was invoked with + prog=program_name(), + epilog="For more information, see https://github.com/Dowsers/dolmos", ) groups = { @@ -870,6 +949,8 @@ def _create_arg_parser() -> argparse.ArgumentParser: if short_name: names.append(f"-{short_name}") + names.extend(field_info.metadata.get("extra_names", [])) + arg_help = field_info.metadata.get("help", "") metavar = field_info.metadata.get("metavar", None) group_name = field_info.metadata.get("group", None) @@ -913,6 +994,12 @@ def default_config() -> "Config": return _default_config +def program_name() -> str: + """The name the command was invoked with (`dolmos` for `python -m dolmos`).""" + name = os.path.basename(sys.argv[0]) + return "dolmos" if not name or name.endswith(".py") else name + + def arg_parser() -> argparse.ArgumentParser: return _arg_parser @@ -928,7 +1015,7 @@ def toml_parser(): # can generate a sample config file using: -# python -m halmos.config ARGS > halmos.toml +# python -m dolmos.config ARGS > dolmos.toml def main(): def _to_toml_str(value: Any, type) -> str: assert value is not None @@ -943,16 +1030,7 @@ def _to_toml_str(value: Any, type) -> str: source=ConfigSource.command_line, **vars(args) ) - # devs can have a little easter egg - lines = [ - "# ___ ___ ___ ___ ___ ___", - "# /\\__\\ /\\ \\ /\\__\\ /\\__\\ /\\ \\ /\\ \\", - "# /:/__/_ /::\\ \\ /:/ / /::L_L_ /::\\ \\ /::\\ \\", - "# /::\\/\\__\\ /::\\:\\__\\ /:/__/ /:/L:\\__\\ /:/\\:\\__\\ /\\:\\:\\__\\", - "# \\/\\::/ / \\/\\::/ / \\:\\ \\ \\/_/:/ / \\:\\/:/ / \\:\\:\\/__/", - "# /:/ / /:/ / \\:\\__\\ /:/ / \\::/ / \\::/ /", - "# \\/__/ \\/__/ \\/__/ \\/__/ \\/__/ \\/__/", - ] + lines = ["# dolmos configuration, generated by `python -m dolmos.config`"] lines.append("\n[global]") current_group_name = None diff --git a/src/halmos/console.py b/src/dolmos/console.py similarity index 97% rename from src/halmos/console.py rename to src/dolmos/console.py index 9a219172d..56a2269f7 100644 --- a/src/halmos/console.py +++ b/src/dolmos/console.py @@ -2,12 +2,12 @@ from z3 import BitVec -from halmos.bitvec import HalmosBitVec as BV -from halmos.logs import ( +from dolmos.bitvec import DolmosBitVec as BV +from dolmos.logs import ( info, warn, ) -from halmos.utils import ( +from dolmos.utils import ( extract_bytes, extract_bytes_argument, extract_funsig, diff --git a/src/halmos/constants.py b/src/dolmos/constants.py similarity index 83% rename from src/halmos/constants.py rename to src/dolmos/constants.py index 7511cad33..ae5296f50 100644 --- a/src/halmos/constants.py +++ b/src/dolmos/constants.py @@ -8,5 +8,5 @@ MAX_MEMORY_SIZE = 2**20 # to be compatible with startHoax(address), -# see https://github.com/a16z/halmos/issues/338 +# see upstream halmos issue #338 MAX_ETH = 1 << 128 diff --git a/src/halmos/contract.py b/src/dolmos/contract.py similarity index 97% rename from src/halmos/contract.py rename to src/dolmos/contract.py index 560c22ee2..20d798e3e 100644 --- a/src/halmos/contract.py +++ b/src/dolmos/contract.py @@ -4,19 +4,19 @@ from dataclasses import dataclass from typing import ClassVar -from halmos.bitvec import HalmosBitVec as BV -from halmos.bytevec import ByteVec, ConcreteChunk -from halmos.constants import MAX_MEMORY_SIZE -from halmos.exceptions import ( +from dolmos.bitvec import DolmosBitVec as BV +from dolmos.bytevec import ByteVec, ConcreteChunk +from dolmos.constants import MAX_MEMORY_SIZE +from dolmos.exceptions import ( NotConcreteError, OutOfGasError, ) -from halmos.logs import ( +from dolmos.logs import ( LIBRARY_PLACEHOLDER, warn_code, ) -from halmos.mapper import SingletonMeta, SourceFileMap -from halmos.utils import ( +from dolmos.mapper import SingletonMeta, SourceFileMap +from dolmos.utils import ( Address, Byte, con_addr, @@ -54,6 +54,7 @@ OP_SHL = 0x1B OP_SHR = 0x1C OP_SAR = 0x1D +OP_CLZ = 0x1E OP_SHA3 = 0x20 OP_ADDRESS = 0x30 OP_BALANCE = 0x31 @@ -80,6 +81,8 @@ OP_CHAINID = 0x46 OP_SELFBALANCE = 0x47 OP_BASEFEE = 0x48 +OP_BLOBHASH = 0x49 +OP_BLOBBASEFEE = 0x4A OP_POP = 0x50 OP_MLOAD = 0x51 OP_MSTORE = 0x52 diff --git a/src/halmos/env.py b/src/dolmos/env.py similarity index 98% rename from src/halmos/env.py rename to src/dolmos/env.py index bcd4386b5..14dad12de 100644 --- a/src/halmos/env.py +++ b/src/dolmos/env.py @@ -6,8 +6,8 @@ from dotenv import find_dotenv, load_dotenv -from halmos.logs import debug -from halmos.utils import Address, uint160 +from dolmos.logs import debug +from dolmos.utils import Address, uint160 def init_env(path: str | None = None): diff --git a/src/dolmos/evm_version.py b/src/dolmos/evm_version.py new file mode 100644 index 000000000..88b585b96 --- /dev/null +++ b/src/dolmos/evm_version.py @@ -0,0 +1,124 @@ +# SPDX-License-Identifier: AGPL-3.0 + +""" +EVM version (hard fork) setting (a16z/halmos#128). + +The version determines which opcodes are available: executing an opcode introduced +by a later fork halts the current frame with an invalid-opcode error, as on a node +running that fork. It also selects the semantics of SELFDESTRUCT (EIP-6780, Cancun). + +When no version is given, the `evmVersion` the test contract was compiled for is +used (from the compiler metadata), falling back to the latest supported fork. +""" + +from dolmos.contract import ( + OP_BASEFEE, + OP_BLOBBASEFEE, + OP_BLOBHASH, + OP_CHAINID, + OP_CLZ, + OP_CREATE2, + OP_DELEGATECALL, + OP_EXTCODEHASH, + OP_MCOPY, + OP_PUSH0, + OP_RETURNDATACOPY, + OP_RETURNDATASIZE, + OP_REVERT, + OP_SAR, + OP_SELFBALANCE, + OP_SHL, + OP_SHR, + OP_STATICCALL, + OP_TLOAD, + OP_TSTORE, +) + +# supported forks, in chronological order (solc/foundry names) +EVM_VERSIONS = ( + "homestead", + "tangerineWhistle", + "spuriousDragon", + "byzantium", + "constantinople", + "petersburg", + "istanbul", + "berlin", + "london", + "paris", + "shanghai", + "cancun", + "prague", + "osaka", +) + +LATEST_EVM_VERSION = EVM_VERSIONS[-1] + +# alternative names accepted on input +EVM_VERSION_ALIASES = { + "merge": "paris", + "frontier": "homestead", # frontier-only semantics are not modeled +} + +# fork that introduced each opcode, for opcodes not available since homestead +OPCODE_INTRODUCED_IN = { + OP_DELEGATECALL: "homestead", + OP_REVERT: "byzantium", + OP_RETURNDATASIZE: "byzantium", + OP_RETURNDATACOPY: "byzantium", + OP_STATICCALL: "byzantium", + OP_SHL: "constantinople", + OP_SHR: "constantinople", + OP_SAR: "constantinople", + OP_CREATE2: "constantinople", + OP_EXTCODEHASH: "constantinople", + OP_CHAINID: "istanbul", + OP_SELFBALANCE: "istanbul", + OP_BASEFEE: "london", + OP_PUSH0: "shanghai", + OP_TLOAD: "cancun", + OP_TSTORE: "cancun", + OP_MCOPY: "cancun", + OP_BLOBHASH: "cancun", + OP_BLOBBASEFEE: "cancun", + OP_CLZ: "osaka", +} + + +def normalize_evm_version(name: str) -> str | None: + """Returns the canonical fork name, or None if the name is not supported""" + name = EVM_VERSION_ALIASES.get(name, name) + for version in EVM_VERSIONS: + if version.lower() == name.lower(): + return version + return None + + +def fork_index(version: str) -> int: + return EVM_VERSIONS.index(version) + + +def is_at_least(version: str, fork: str) -> bool: + return fork_index(version) >= fork_index(fork) + + +def unavailable_opcodes(version: str) -> frozenset[int]: + """Opcodes introduced after the given fork""" + index = fork_index(version) + return frozenset( + opcode + for opcode, fork in OPCODE_INTRODUCED_IN.items() + if fork_index(fork) > index + ) + + +def evm_version_from_metadata(contract_json: dict) -> str | None: + """Returns the evmVersion found in the compiler metadata of a build artifact""" + metadata = contract_json.get("metadata") + if not isinstance(metadata, dict): + return None + settings = metadata.get("settings") + if not isinstance(settings, dict): + return None + version = settings.get("evmVersion") + return version if isinstance(version, str) else None diff --git a/src/halmos/exceptions.py b/src/dolmos/exceptions.py similarity index 97% rename from src/halmos/exceptions.py rename to src/dolmos/exceptions.py index 300d77f65..74b64e573 100644 --- a/src/halmos/exceptions.py +++ b/src/dolmos/exceptions.py @@ -20,7 +20,7 @@ class PathEndingException(Exception): pass -class HalmosException(PathEndingException): +class DolmosException(PathEndingException): """ Base class for unexpected internal errors happening during a test run. Inherits from RunEndingException because it should stop further path exploration. @@ -29,7 +29,7 @@ class HalmosException(PathEndingException): pass -class NotConcreteError(HalmosException): +class NotConcreteError(DolmosException): pass diff --git a/src/dolmos/expectations.py b/src/dolmos/expectations.py new file mode 100644 index 000000000..c4a719c7e --- /dev/null +++ b/src/dolmos/expectations.py @@ -0,0 +1,461 @@ +# SPDX-License-Identifier: AGPL-3.0 + +""" +Support for the `vm.expectRevert*` / `vm.expectPartialRevert*` and +`vm.expectEmit*` / `vm.expectEmitAnonymous*` cheatcodes (halmos issue #409). + +The semantics follow foundry: + +- an expectation is set by a cheatcode call and applies to the *next call* (or + contract creation) made by the same frame; calls to cheatcode addresses and to + the console are ignored. +- expectRevert: the next call must revert, with a matching reason and reverter if + given. When the expectation is met the call is reported as successful to the + caller, with dummy return data (like foundry). `count = n` requires the next n + calls to revert, `count = 0` requires the next call not to revert. +- expectEmit: the next event emitted by the frame itself is recorded as the + expected event. The next call must then emit events matching the expected ones + (in order, anywhere in its call tree). With a `count`, the expected event must + be emitted exactly `count` times. +- an expectation that is still pending when the frame returns successfully makes + the test fail. + +Because data may be symbolic, matching produces an SMT condition: the caller +forks a failing path when the condition can be false. +""" + +from collections.abc import Iterator +from dataclasses import dataclass, field + +from z3 import ( + And, + BitVecRef, + BoolRef, + BoolVal, + Concat, + Extract, + If, + Or, + Sum, + is_bv, + simplify, +) + +from dolmos.bitvec import DolmosBitVec as BV +from dolmos.bytevec import ByteVec +from dolmos.exceptions import DolmosException +from dolmos.utils import ( + bytes_to_bv_value, + con, + extract_bytes_argument, + int_of, + uint160, +) + +# foundry reports a successful call with 8192 zero bytes when a revert was expected +DUMMY_CALL_OUTPUT = ByteVec(bytes(8192)) + +# bytes4(keccak256("Error(string)")) +ERROR_STRING_SELECTOR = bytes.fromhex("08c379a0") + +UnwrappedBytes = bytes | BitVecRef + + +# +# expectation records +# + + +@dataclass +class ExpectedRevert: + reason: UnwrappedBytes | None = None # None: any revert data + partial: bool = False # only compare the first 4 bytes + reverter: BitVecRef | None = None # None: any reverter + count: int = 1 # 0: the next call must not revert + + def __str__(self) -> str: + parts = [] + if self.reason is not None: + parts.append(f"reason={_hex(self.reason)}") + if self.reverter is not None: + parts.append(f"reverter={self.reverter}") + if self.count != 1: + parts.append(f"count={self.count}") + name = "expectPartialRevert" if self.partial else "expectRevert" + return f"{name}({', '.join(parts)})" + + +@dataclass +class ExpectedEmit: + # checks for topic0 (anonymous events only), topic1, topic2, topic3, data + checks: tuple[bool, bool, bool, bool, bool] + anonymous: bool = False + emitter: BitVecRef | None = None + count: int | None = None # None: plain (ordered) expectation + log: object | None = None # the expected EventLog, once emitted + + def __str__(self) -> str: + name = "expectEmitAnonymous" if self.anonymous else "expectEmit" + emitter = f", emitter={self.emitter}" if self.emitter is not None else "" + count = f", count={self.count}" if self.count is not None else "" + return f"{name}(checks={self.checks}{emitter}{count})" + + +@dataclass +class Expectations: + """ + Pending expectations of a call frame. Stored in its CallContext. + """ + + revert: ExpectedRevert | None = None + emits: list[ExpectedEmit] = field(default_factory=list) + + def __bool__(self) -> bool: + return self.revert is not None or bool(self.emits) + + def expect_revert(self, expected: ExpectedRevert) -> None: + if self.revert is not None: + raise DolmosException( + "expectRevert: an expected revert is already pending; " + "call another function before expecting a second revert" + ) + self.revert = expected + + def expect_emit(self, expected: ExpectedEmit) -> None: + self.emits.append(expected) + + def capture_log(self, log) -> None: + """Records `log` as the expected event of the first unfilled expectEmit.""" + for spec in self.emits: + if spec.log is None: + spec.log = log + return + + def take(self) -> "Expectations | None": + """ + Returns the expectations that apply to the next call, and clears them. + """ + if not self: + return None + + taken = Expectations(revert=self.revert, emits=self.emits) + self.revert = None + self.emits = [] + return taken + + def describe(self) -> str: + items = ([str(self.revert)] if self.revert else []) + [ + str(e) for e in self.emits + ] + return ", ".join(items) + + +# +# cheatcode argument decoding +# + + +def _word(arg: ByteVec, idx: int): + return arg.get_word(4 + 32 * idx) + + +def _bool(arg: ByteVec, idx: int, name: str) -> bool: + return int_of(_word(arg, idx), f"symbolic {name} argument") != 0 + + +def _address(arg: ByteVec, idx: int) -> BitVecRef: + return uint160(_word(arg, idx)).as_z3() + + +def _uint64(arg: ByteVec, idx: int, name: str) -> int: + return int_of(_word(arg, idx), f"symbolic {name} count") & (2**64 - 1) + + +def _bytes4(arg: ByteVec, idx: int) -> UnwrappedBytes: + start = 4 + 32 * idx + return arg.slice(start, start + 4).unwrap() + + +# expectRevert variants: signature -> argument layout +REVERT_SIGNATURES: dict[int, tuple[str, tuple[str, ...]]] = { + 0xF4844814: ("expectRevert()", ()), + 0xC31EB0E0: ("expectRevert(bytes4)", ("bytes4",)), + 0xF28DCEB3: ("expectRevert(bytes)", ("bytes",)), + 0xD814F38A: ("expectRevert(address)", ("address",)), + 0x260BC5DE: ("expectRevert(bytes4,address)", ("bytes4", "address")), + 0x61EBCF12: ("expectRevert(bytes,address)", ("bytes", "address")), + 0x4EE38244: ("expectRevert(uint64)", ("count",)), + 0xE45CA72D: ("expectRevert(bytes4,uint64)", ("bytes4", "count")), + 0x4994C273: ("expectRevert(bytes,uint64)", ("bytes", "count")), + 0x1FF5F952: ("expectRevert(address,uint64)", ("address", "count")), + 0xB0762D73: ( + "expectRevert(bytes4,address,uint64)", + ("bytes4", "address", "count"), + ), + 0xD345FB1F: ( + "expectRevert(bytes,address,uint64)", + ("bytes", "address", "count"), + ), + 0x11FB5B9C: ("expectPartialRevert(bytes4)", ("bytes4",)), + 0x51AA008A: ("expectPartialRevert(bytes4,address)", ("bytes4", "address")), +} + +# expectEmit variants: signature -> (anonymous, argument layout) +EMIT_SIGNATURES: dict[int, tuple[str, bool, tuple[str, ...]]] = { + 0x440ED10D: ("expectEmit()", False, ()), + 0x86B9620D: ("expectEmit(address)", False, ("address",)), + 0x491CC7C2: ("expectEmit(bool,bool,bool,bool)", False, ("bool",) * 4), + 0x81BAD6F3: ( + "expectEmit(bool,bool,bool,bool,address)", + False, + ("bool",) * 4 + ("address",), + ), + 0x4C74A335: ("expectEmit(uint64)", False, ("count",)), + 0xB43AECE3: ("expectEmit(address,uint64)", False, ("address", "count")), + 0x5E1D1C33: ( + "expectEmit(bool,bool,bool,bool,uint64)", + False, + ("bool",) * 4 + ("count",), + ), + 0xC339D02C: ( + "expectEmit(bool,bool,bool,bool,address,uint64)", + False, + ("bool",) * 4 + ("address", "count"), + ), + 0x2E5F270C: ("expectEmitAnonymous()", True, ()), + 0x6FC68705: ("expectEmitAnonymous(address)", True, ("address",)), + 0xC948DB5E: ( + "expectEmitAnonymous(bool,bool,bool,bool,bool)", + True, + ("bool",) * 5, + ), + 0x71C95899: ( + "expectEmitAnonymous(bool,bool,bool,bool,bool,address)", + True, + ("bool",) * 5 + ("address",), + ), +} + + +def parse_expect_revert(funsig: int, arg: ByteVec) -> ExpectedRevert: + name, layout = REVERT_SIGNATURES[funsig] + expected = ExpectedRevert(partial=name.startswith("expectPartialRevert")) + + for idx, kind in enumerate(layout): + match kind: + case "bytes4": + expected.reason = _bytes4(arg, idx) + case "bytes": + expected.reason = extract_bytes_argument(arg, idx) + case "address": + expected.reverter = _address(arg, idx) + case "count": + expected.count = _uint64(arg, idx, name) + + return expected + + +def parse_expect_emit(funsig: int, arg: ByteVec) -> ExpectedEmit: + name, anonymous, layout = EMIT_SIGNATURES[funsig] + + bools = [_bool(arg, i, name) for i, k in enumerate(layout) if k == "bool"] + if not bools: + bools = [True] * (5 if anonymous else 4) + + # normalize to (topic0, topic1, topic2, topic3, data); + # topic0 (the event selector) is always checked for non-anonymous events + checks = tuple(bools) if anonymous else (True, *bools) + + expected = ExpectedEmit(checks=checks, anonymous=anonymous) + for idx, kind in enumerate(layout): + match kind: + case "address": + expected.emitter = _address(arg, idx) + case "count": + expected.count = _uint64(arg, idx, name) + + return expected + + +# +# symbolic matching +# + + +def _unwrap(x) -> UnwrappedBytes: + if isinstance(x, ByteVec): + return x.unwrap() + return x + + +def _len(x: UnwrappedBytes) -> int: + return x.size() // 8 if is_bv(x) else len(x) + + +def _slice(x: UnwrappedBytes, start: int, stop: int) -> UnwrappedBytes: + """Byte slice [start:stop), zero-padded if out of bounds.""" + n = _len(x) + if stop <= start: + return b"" + if not is_bv(x): + return (x + bytes(max(0, stop - n)))[start:stop] + if start >= n: + return bytes(stop - start) + hi = (n - start) * 8 - 1 + lo = max(0, (n - stop) * 8) + part = Extract(hi, lo, x) + pad = stop - min(stop, n) + return simplify(Concat(part, con(0, pad * 8))) if pad else simplify(part) + + +def _to_bv(x: UnwrappedBytes) -> BitVecRef: + return x if is_bv(x) else bytes_to_bv_value(x) + + +def eq_bytes(a, b) -> BoolRef: + a, b = _unwrap(a), _unwrap(b) + if _len(a) != _len(b): + return BoolVal(False) + if _len(a) == 0: + return BoolVal(True) + if not is_bv(a) and not is_bv(b): + return BoolVal(a == b) + return _to_bv(a) == _to_bv(b) + + +def as_z3_word(x): + if isinstance(x, BV): + return x.as_z3() + if isinstance(x, int): + return con(x) + return x + + +def revert_reason_matches(expected: ExpectedRevert, data: ByteVec) -> BoolRef: + """ + Whether revert `data` matches the expected reason: + - the raw revert data equals the reason, or + - the data is `Error(string)` and its payload equals the reason, or + - for partial matches, the first 4 bytes are equal. + """ + if expected.reason is None: + return BoolVal(True) + + reason = expected.reason + raw = _unwrap(data) + reason_len, data_len = _len(reason), _len(raw) + + conds = [eq_bytes(raw, reason)] + + if expected.partial and reason_len >= 4 and data_len >= 4: + conds.append(eq_bytes(_slice(raw, 0, 4), _slice(reason, 0, 4))) + + # Error(string) unwrapping: selector | offset (0x20) | length | payload + payload_end = 68 + reason_len + if data_len >= payload_end: + conds.append( + And( + eq_bytes(_slice(raw, 0, 4), ERROR_STRING_SELECTOR), + eq_bytes(_slice(raw, 4, 36), (32).to_bytes(32, "big")), + eq_bytes(_slice(raw, 36, 68), reason_len.to_bytes(32, "big")), + eq_bytes(_slice(raw, 68, payload_end), reason), + ) + ) + + return simplify(Or(*conds)) + + +def find_reverter(subcall) -> BitVecRef: + """ + The address that originally reverted: follow the chain of reverted subcalls + that bubbled up the same revert data. + """ + ctx = subcall + while True: + child = ctx.last_subcall() + if ( + child is None + or child.output.error is None + or child.output.data is None + or child.output.data != ctx.output.data + ): + return ctx.message.target + ctx = child + + +def iter_logs(ctx) -> Iterator: + """All the logs emitted in a call tree, in execution order.""" + for item in ctx.trace: + if hasattr(item, "topics"): + yield item + elif hasattr(item, "trace"): + yield from iter_logs(item) + + +def log_matches(spec: ExpectedEmit, log) -> BoolRef: + expected = spec.log + conds = [] + + if spec.emitter is not None: + conds.append(as_z3_word(log.address) == as_z3_word(spec.emitter)) + + if len(log.topics) != len(expected.topics): + return BoolVal(False) + + for i, (actual, wanted) in enumerate(zip(log.topics, expected.topics, strict=True)): + if spec.checks[i]: + conds.append(as_z3_word(actual) == as_z3_word(wanted)) + + if spec.checks[4]: + conds.append(eq_bytes(log.data or b"", expected.data or b"")) + + return simplify(And(*conds)) if conds else BoolVal(True) + + +def emits_match(specs: list[ExpectedEmit], subcall) -> tuple[BoolRef, str | None]: + """ + Returns (condition, error). A non-None error means the expectation can't be met. + """ + unfilled = [s for s in specs if s.log is None] + if unfilled: + return BoolVal(False), ( + f"{unfilled[0]}: no event was emitted between the cheatcode and the next call" + ) + + logs = list(iter_logs(subcall)) + conds = [] + + # counted expectations are checked independently + for spec in (s for s in specs if s.count is not None): + hits = [If(log_matches(spec, log), con(1), con(0)) for log in logs] + total = simplify(Sum(hits)) if hits else con(0) + conds.append(total == con(spec.count)) + + # plain expectations must appear as an ordered subsequence of the logs + ordered = [s for s in specs if s.count is None] + memo: dict[tuple[int, int], BoolRef] = {} + + def matches_from(i: int, j: int) -> BoolRef: + if i == len(ordered): + return BoolVal(True) + if len(ordered) - i > len(logs) - j: + return BoolVal(False) + if (i, j) not in memo: + memo[i, j] = simplify( + Or( + And(log_matches(ordered[i], logs[j]), matches_from(i + 1, j + 1)), + matches_from(i, j + 1), + ) + ) + return memo[i, j] + + if ordered: + conds.append(matches_from(0, 0)) + + return simplify(And(*conds)) if conds else BoolVal(True), None + + +def _hex(x: UnwrappedBytes) -> str: + if is_bv(x): + return str(x) + return "0x" + x.hex() diff --git a/src/halmos/flamegraphs.py b/src/dolmos/flamegraphs.py similarity index 97% rename from src/halmos/flamegraphs.py rename to src/dolmos/flamegraphs.py index 4502ea51a..3bd923f42 100644 --- a/src/halmos/flamegraphs.py +++ b/src/dolmos/flamegraphs.py @@ -7,10 +7,10 @@ import traceback from dataclasses import dataclass, field -from halmos.logs import debug, warn -from halmos.sevm import CallContext, CallSequence, Message -from halmos.traces import rendered_address -from halmos.utils import hexify +from dolmos.logs import debug, warn +from dolmos.sevm import CallContext, CallSequence, Message +from dolmos.traces import rendered_address +from dolmos.utils import hexify AUTO_REFRESH_INTERVAL_SECONDS = 0.250 diff --git a/src/dolmos/fs.py b/src/dolmos/fs.py new file mode 100644 index 000000000..0380c3bb0 --- /dev/null +++ b/src/dolmos/fs.py @@ -0,0 +1,172 @@ +# SPDX-License-Identifier: AGPL-3.0 + +""" +Filesystem access for the file cheatcodes (vm.readFile, vm.readFileBinary, ...). + +Access is governed by the project's `fs_permissions`, with the same semantics as +Foundry, so that a test reading a file behaves identically under `forge test` and +under dolmos: + +- permissions are read from the resolved forge configuration (`forge config --json`), + so profiles and environment overrides are honored; +- paths, both requested and permitted, are resolved against the project root and + normalized lexically (`a/../b` becomes `b`; symlinks are not followed); +- the most specific permission (longest matching path) wins, so a nested + `{ access = "none", path = "./data/private" }` overrides a broader read grant; +- without any matching permission, access is denied. +""" + +import json +import os +import re +import subprocess +from dataclasses import dataclass +from functools import cache + +from dolmos.exceptions import DolmosException +from dolmos.logs import debug, warn + +# foundry's default when fs_permissions is not configured +DEFAULT_FS_PERMISSIONS: tuple[dict, ...] = ({"access": "read", "path": "out"},) + +# `forge config --json` serializes "read-write" as true and "none" as false +_ACCESS_ALIASES = { + True: "read-write", + False: "none", + "true": "read-write", + "false": "none", +} + +_READABLE = frozenset({"read", "read-write"}) + + +@dataclass(frozen=True) +class FsPermission: + access: str # "none" | "read" | "write" | "read-write" + path: str # absolute and normalized + + @property + def can_read(self) -> bool: + return self.access in _READABLE + + +def resolve_path(root: str, path: str) -> str: + """Absolute, lexically normalized path; relative paths are taken from root.""" + return os.path.normpath(os.path.join(os.path.abspath(root), path)) + + +def parse_fs_permissions(root: str, raw: list | tuple) -> tuple[FsPermission, ...]: + permissions = [] + for entry in raw: + access = entry["access"] + access = _ACCESS_ALIASES.get(access, access) + if isinstance(access, str): + access = access.lower() + permissions.append(FsPermission(access, resolve_path(root, entry["path"]))) + return tuple(permissions) + + +@cache +def load_fs_permissions(root: str) -> tuple[FsPermission, ...]: + """Resolved fs_permissions of the forge project at root (cached per root).""" + + cmd = ["forge", "config", "--json", "--root", root] + try: + # forge writes utf-8 (warnings may contain non-ascii): do not decode with the + # locale encoding, which is not utf-8 on Windows + result = subprocess.run( + cmd, + capture_output=True, + encoding="utf-8", + errors="replace", + check=True, + ) + raw = json.loads(result.stdout).get("fs_permissions") or [] + except (OSError, subprocess.CalledProcessError, ValueError) as e: + warn( + f"could not resolve fs_permissions with `{' '.join(cmd)}` ({e}); " + "falling back to foundry's default (read access to `out` only)" + ) + raw = DEFAULT_FS_PERMISSIONS + + permissions = parse_fs_permissions(root, raw) + debug(f"fs_permissions for {root}: {permissions}") + return permissions + + +def find_permission( + permissions: tuple[FsPermission, ...], abs_path: str +) -> FsPermission | None: + """The most specific permission covering abs_path, if any.""" + + # paths are case-insensitive on Windows (normcase is the identity elsewhere) + target = os.path.normcase(abs_path) + best = None + for permission in permissions: + base = os.path.normcase(permission.path) + covered = target == base or target.startswith(base.rstrip(os.sep) + os.sep) + if covered and (best is None or len(permission.path) > len(best.path)): + best = permission + return best + + +def ensure_readable( + root: str, + path: str, + cheatcode: str, + permissions: tuple[FsPermission, ...] | None = None, +) -> str: + """ + Returns the absolute path to read, or raises if fs_permissions deny reading it. + """ + + if permissions is None: + permissions = load_fs_permissions(root) + + abs_path = resolve_path(root, path) + permission = find_permission(permissions, abs_path) + if permission is None or not permission.can_read: + shown = os.path.relpath(abs_path, os.path.abspath(root)) + if shown.startswith(os.pardir): + shown = abs_path + raise DolmosException( + f"{cheatcode}: the path {shown} is not allowed to be accessed for read " + "operations (see fs_permissions in foundry.toml)" + ) + + return abs_path + + +def read_file(root: str, path: str, cheatcode: str) -> bytes: + """Raw content of the file at path, subject to fs_permissions.""" + + abs_path = ensure_readable(root, path, cheatcode) + try: + with open(abs_path, "rb") as f: + return f.read() + except OSError as e: + raise DolmosException(f"{cheatcode}: failed to read {abs_path}: {e}") from e + + +_HEX_DIGITS = re.compile(r"[0-9a-fA-F]*") + + +def parse_hex_bytes(value: str, cheatcode: str = "vm.parseBytes") -> bytes: + """ + Parses a hex string the way Foundry's vm.parseBytes does: an optional + lowercase `0x` prefix followed by an even number of hex digits. Whitespace + is rejected, and the empty string is only accepted as `0x`. + """ + + digits = value[2:] if value.startswith("0x") else value + + if not value: + reason = 'missing hex prefix ("0x") for hex string' + elif not _HEX_DIGITS.fullmatch(digits): + reason = "invalid hex character" + elif len(digits) % 2: + reason = "odd number of digits" + else: + return bytes.fromhex(digits) + + raise DolmosException(f'{cheatcode}: failed parsing "{value}" as bytes: {reason}') diff --git a/src/halmos/hashes.py b/src/dolmos/hashes.py similarity index 100% rename from src/halmos/hashes.py rename to src/dolmos/hashes.py diff --git a/src/dolmos/lasso.py b/src/dolmos/lasso.py new file mode 100644 index 000000000..7ca56fc16 --- /dev/null +++ b/src/dolmos/lasso.py @@ -0,0 +1,886 @@ +# SPDX-License-Identifier: AGPL-3.0 + +""" +Export of bounded loops as lasso programs, for termination analysis with PaSTTeL. + +When the loop unrolling bound (--loop) is reached on a symbolic JUMPI, dolmos can +export the loop as a *lasso*: a stem (how the execution reaches the loop) and a +loop transition (one iteration of the body), in PaSTTeL's JSON format +(https://github.com/Dowsers/PaSTTeL). + +Extraction (see SEVM.extract_lasso) +- the loop variables are the stack slots that change between two visits +- the lasso is cut right after the JUMPI, on the branch that stays in the loop +- the body is re-executed once from a generalized state (fresh loop variables), + on a separate solver; each path that comes back and takes the loop branch + again is a disjunct of the loop transition + +Translation (Translator): bitvectors become non-negative integers. Exact where +possible, over-approximated otherwise (fresh variables), so that termination +proofs stay valid. + +By default, lassos use the *small-constants encoding*: no literal exceeds 2^52, +because PaSTTeL computes with doubles and is unsound on 2^256 constants. +Wrap-arounds are proven absent with z3 (bitvector semantics) when possible, and +over-approximated without large constants otherwise. + +See docs/loop-termination.md for details, soundness and limitations. +""" + +import json +import os +import re +import subprocess +from dataclasses import dataclass, field + +from z3 import ( + UGE, + ULT, + Z3_OP_AND, + Z3_OP_BADD, + Z3_OP_BAND, + Z3_OP_BLSHR, + Z3_OP_BMUL, + Z3_OP_BNEG, + Z3_OP_BNUM, + Z3_OP_BSHL, + Z3_OP_BSUB, + Z3_OP_BUDIV, + Z3_OP_BUDIV_I, + Z3_OP_BUREM, + Z3_OP_BUREM_I, + Z3_OP_CONCAT, + Z3_OP_DISTINCT, + Z3_OP_EQ, + Z3_OP_EXTRACT, + Z3_OP_FALSE, + Z3_OP_IFF, + Z3_OP_IMPLIES, + Z3_OP_ITE, + Z3_OP_NOT, + Z3_OP_OR, + Z3_OP_SGEQ, + Z3_OP_SGT, + Z3_OP_SLEQ, + Z3_OP_SLT, + Z3_OP_TRUE, + Z3_OP_UGEQ, + Z3_OP_UGT, + Z3_OP_ULEQ, + Z3_OP_ULT, + Z3_OP_UNINTERPRETED, + Z3_OP_XOR, + Z3_OP_ZERO_EXT, + And, + BitVec, + BitVecRef, + BitVecVal, + BoolRef, + ExprRef, + LShR, + Not, + Or, + Solver, + Sum, + ZeroExt, + is_bool, + is_bv, + is_bv_value, + is_false, + is_true, + simplify, + substitute, + unsat, +) +from z3.z3util import get_vars + +# upper bound on the paths of the generalized iteration +MAX_BODY_PATHS = 32 + +# upper bound on the number of instructions executed by the generalized iteration +MAX_BODY_STEPS = 200_000 + +LOOP_VAR_PREFIX = "lasso_v" + +# wrap-arounds with at most this many cases are encoded as disjunctions +MAX_WRAP_CASES = 4 + +# PaSTTeL stores numbers as doubles: integers are exact up to 2^53 +MAX_SMALL_CONSTANT = 2**52 + + +# +# snapshots and results +# + + +@dataclass(frozen=True) +class LoopSnapshot: + stack: tuple # stack below the JUMPI operands + cond: BoolRef # branching condition + + +@dataclass +class LassoResult: + test: str + jumpid: str + direction: bool + path: str | None = None # dumped JSON file + error: str | None = None # extraction failure + warnings: list[str] = field(default_factory=list) + verdict: str | None = None # PaSTTeL verdict + proof: str | None = None + approximate: bool = False # the lasso over-approximates the loop + + def summary(self) -> str: + where = f"loop {self.jumpid} ({'true' if self.direction else 'false'} branch)" + if self.error: + return f"{where}: lasso not extracted: {self.error}" + text = f"{where}: {self.verdict or 'lasso dumped'}" + if self.verdict == "NON-TERMINATING" and (self.approximate or self.warnings): + # only termination proofs survive over-approximation + text += " (unconfirmed: the lasso over-approximates the loop)" + if self.proof: + text += f" [{self.proof}]" + if self.warnings: + text += f" (warning: {'; '.join(self.warnings)})" + if self.path: + text += f" -> {self.path}" + return text + + +class LassoError(Exception): + pass + + +# +# BV -> Int translation +# + + +def is_loop_var(e: ExprRef) -> bool: + return ( + e.num_args() == 0 + and e.decl().kind() == Z3_OP_UNINTERPRETED + and e.decl().name().startswith(LOOP_VAR_PREFIX) + ) + + +def depends_on_loop_vars(e: ExprRef) -> bool: + return any(is_loop_var(v) for v in get_vars(e)) + + +class WrapProver: + """ + Proves, with the bitvector semantics, that an operation cannot wrap around + under the conditions of a path. Used by the small-constants encoding. + + The conditions of a generalized iteration mention the input symbols (via the + stem) and the fresh loop variables (via the body). Input symbols never + change, so facts about them hold at every iteration: using them is sound. + """ + + def __init__(self, conditions: list[BoolRef], timeout_ms: int): + self.solver = Solver() + self.solver.set(timeout=timeout_ms) + self.solver.add(*conditions) + self.memo: dict[int, bool] = {} + + def valid(self, cond: BoolRef) -> bool: + cond = simplify(cond) + if is_true(cond): + return True + if is_false(cond): + return False + key = cond.get_id() + if key not in self.memo: + self.solver.push() + self.solver.add(Not(cond)) + self.memo[key] = self.solver.check() == unsat + self.solver.pop() + return self.memo[key] + + +class Registry: + """State shared by all the translation contexts of one lasso.""" + + def __init__(self): + self.aux_counter = 0 + # loop-invariant opaque terms -> (program variable name, width, term) + self.invariants: dict[int, tuple[str, int, ExprRef]] = {} + # large literals (small-constants encoding) -> program variable name + self.big_constants: dict[int, str] = {} + # set when the translation over-approximates the bitvector semantics + self.approximate = False + + def fresh(self, prefix: str) -> str: + self.aux_counter += 1 + return f"{prefix}{self.aux_counter}" + + def invariant(self, e: ExprRef) -> str: + key = e.get_id() + if key not in self.invariants: + width = e.size() if is_bv(e) else 1 + self.invariants[key] = (f"k{len(self.invariants)}", width, e) + return self.invariants[key][0] + + def big_constant(self, value: int) -> str: + if value not in self.big_constants: + self.big_constants[value] = f"c{len(self.big_constants)}" + return self.big_constants[value] + + +class Translator: + """ + Translates bitvector formulas to linear integer SMT-LIB terms. + + One translator per transition disjunct: auxiliary variables and their + constraints are local to it. + + Two encodings: + - exact (prover is None): wrap-arounds are encoded exactly, with 2^w + constants. Suitable for tools with exact arithmetic. + - small constants (with a prover): no literal exceeds MAX_SMALL_CONSTANT, + because PaSTTeL represents numbers as doubles (exact up to 2^53 only). + See docs/loop-termination.md. + """ + + def __init__( + self, + registry: Registry, + names: dict[str, str], + stem: bool, + prover: WrapProver | None = None, + ): + self.reg = registry + self.names = names # loop variable name -> SSA name + self.stem = stem + self.prover = prover + self.aux: list[str] = [] + self.constraints: list[str] = [] + self.memo: dict[int, str] = {} + + @property + def small(self) -> bool: + return self.prover is not None + + # helpers + + def _aux(self, width: int | None) -> str: + name = self.reg.fresh("aux") + self.aux.append(name) + if width is not None: + self.constraints.append(f"(<= 0 {name})") + upper = 2**width + if not self.small or upper <= MAX_SMALL_CONSTANT: + self.constraints.append(f"(< {name} {upper})") + return name + + def _num(self, value: int) -> str: + """A literal; large ones become constant program variables if needed.""" + if self.small and value > MAX_SMALL_CONSTANT: + self.reg.approximate = True + name = self.reg.big_constant(value) + return f"{name}_s" if self.stem else name + return str(value) + + def _wrap( + self, + expr: str, + width: int, + k_min: int, + k_max: int | None, + no_wrap: BoolRef | None = None, + ) -> str: + """ + expr mod 2^width, where expr - r = 2^width * k with k in [k_min, k_max]. + + `no_wrap` is the bitvector condition under which k = 0. + """ + m = 2**width + + if self.small: + # k = 0 proven: the result is the integer expression itself + if no_wrap is not None and self.prover.valid(no_wrap): + return expr + self.reg.approximate = True + r = self._aux(width) + if k_min >= 0: + # only positive wrap-arounds: r = expr - 2^w * k <= expr + self.constraints.append(f"(<= {r} {expr})") + elif k_max is not None and k_max <= 0: + # only borrows: no wrap iff expr >= 0 (no large constant needed) + self.constraints.append( + f"(or (and (<= 0 {expr}) (= {r} {expr})) (< {expr} 0))" + ) + return r + + r = self._aux(width) + if k_max is not None and k_max - k_min < MAX_WRAP_CASES: + cases = [] + for k in range(k_min, k_max + 1): + lo, hi = m * k, m * (k + 1) + shifted = expr if k == 0 else f"(- {expr} {lo})" + cases.append( + f"(and (<= {lo} {expr}) (< {expr} {hi}) (= {r} {shifted}))" + ) + self.constraints.append( + cases[0] if len(cases) == 1 else f"(or {' '.join(cases)})" + ) + else: + k = self._aux(None) + self.constraints.append(f"(= {r} (- {expr} (* {m} {k})))") + return r + + def _ite(self, cond: str, a: str, b: str, width: int | None) -> str: + """Arithmetic if-then-else, which PaSTTeL doesn't parse: a fresh t with + (cond and t = a) or (not cond and t = b).""" + t = self._aux(width) + self.constraints.append( + f"(or (and {cond} (= {t} {a})) (and (not {cond}) (= {t} {b})))" + ) + return t + + def _div_const(self, a: str, c: int) -> str: + """a div c for a constant c > 0: c*q <= a <= c*q + c - 1.""" + if c == 1: + return a + q = self._aux(None) + if self.small and c > MAX_SMALL_CONSTANT: + self.reg.approximate = True + # only keep 0 <= q <= a + self.constraints.append(f"(<= 0 {q})") + self.constraints.append(f"(<= {q} {a})") + return q + self.constraints.append(f"(<= (* {c} {q}) {a})") + self.constraints.append(f"(<= {a} (+ (* {c} {q}) {c - 1}))") + return q + + def _rem_const(self, a: str, c: int) -> str: + if self.small and c > MAX_SMALL_CONSTANT: + self.reg.approximate = True + r = self._aux(None) + self.constraints.append(f"(<= 0 {r})") + self.constraints.append(f"(<= {r} {a})") + return r + return f"(- {a} (* {c} {self._div_const(a, c)}))" + + def _truncate(self, a_term: str, a: BitVecRef, width: int) -> str: + """a (of a wider sort) mod 2^width.""" + upper = 2**width + no_wrap = ULT(a, BitVecVal(upper, a.size())) if upper < 2 ** a.size() else None + k_max = 2 ** (a.size() - width) - 1 + return self._wrap(a_term, width, 0, k_max, no_wrap) + + def _opaque(self, e: ExprRef) -> str: + """Opaque term: shared constant if loop-invariant, fresh value otherwise.""" + # a free input symbol is represented exactly by a variable; a compound + # term (keccak, storage read, bitwise operation...) is not + if e.num_args() > 0: + self.reg.approximate = True + width = e.size() if is_bv(e) else 1 + if not self.stem and not depends_on_loop_vars(e): + return self.reg.invariant(e) + if self.stem and e.get_id() in self.reg.invariants: + return self.reg.invariants[e.get_id()][0] + "_s" + return self._aux(width) + + @staticmethod + def _const(e: ExprRef) -> int | None: + return e.as_long() if is_bv_value(e) else None + + # entry points + + def bv(self, e: BitVecRef) -> str: + key = e.get_id() + if key not in self.memo: + self.memo[key] = self._bv(e) + return self.memo[key] + + def bool(self, e: BoolRef) -> str: + key = e.get_id() + if key not in self.memo: + self.memo[key] = self._bool(e) + return self.memo[key] + + def any(self, e: ExprRef) -> str: + """Int term for a bitvector, 0/1 for a boolean.""" + if is_bool(e): + return self._ite(self.bool(e), "1", "0", 1) + return self.bv(e) + + # bitvectors + + def _bv(self, e: BitVecRef) -> str: + w = e.size() + kind = e.decl().kind() + args = e.children() + + if kind == Z3_OP_BNUM: + return self._num(e.as_long()) + + if e.num_args() == 0 and kind == Z3_OP_UNINTERPRETED: + name = e.decl().name() + if name in self.names: + return self.names[name] + return self._opaque(e) + + if kind == Z3_OP_BADD: + # x + C with C >= 2^(w-1) is x - (2^w - C), e.g. solc's x - 1 + consts = [c for a in args if (c := self._const(a)) is not None] + neg = sum(2**w - c for c in consts if c >= 2 ** (w - 1)) + if neg and 0 < neg < 2**w and len(consts) < len(args): + rest = [a for a in args if not (self._const(a) or 0) >= 2 ** (w - 1)] + rest_expr = rest[0] if len(rest) == 1 else Sum(rest) + d = BitVecVal(neg, w) + return self._wrap( + f"(- {self.bv(rest_expr)} {self._num(neg)})", + w, + -1, + 0, + UGE(rest_expr, d), + ) + terms = " ".join(self.bv(a) for a in args) + wide = w + len(args).bit_length() + total = Sum([ZeroExt(wide - w, a) for a in args]) + no_wrap = ULT(total, BitVecVal(2**w, wide)) + return self._wrap(f"(+ {terms})", w, 0, len(args) - 1, no_wrap) + + if kind == Z3_OP_BSUB: + a, b = args + return self._wrap(f"(- {self.bv(a)} {self.bv(b)})", w, -1, 0, UGE(a, b)) + + if kind == Z3_OP_BNEG: + return self._wrap(f"(- 0 {self.bv(args[0])})", w, -1, 0, args[0] == 0) + + if kind == Z3_OP_BMUL: + consts = [c for a in args if (c := self._const(a)) is not None] + others = [a for a in args if self._const(a) is None] + if len(others) <= 1: + coef = 1 + for c in consts: + coef *= c + coef %= 2**w + if not others: + return self._num(coef) + return self._scale(others[0], coef, w) + return self._opaque(e) + + if kind == Z3_OP_BSHL and (s := self._const(args[1])) is not None: + if s >= w: + return "0" + return self._scale(args[0], 2**s, w) + + if kind == Z3_OP_BLSHR and (s := self._const(args[1])) is not None: + if s >= w: + return "0" + return self._div_const(self.bv(args[0]), 2**s) + + if kind in (Z3_OP_BUDIV, Z3_OP_BUDIV_I) and (c := self._const(args[1])): + return self._div_const(self.bv(args[0]), c) + + if kind in (Z3_OP_BUREM, Z3_OP_BUREM_I) and (c := self._const(args[1])): + return self._rem_const(self.bv(args[0]), c) + + if kind == Z3_OP_BAND: + # masking with 2^n - 1 is a truncation + consts = [c for a in args if (c := self._const(a)) is not None] + others = [a for a in args if self._const(a) is None] + if len(consts) == 1 and len(others) == 1: + mask = consts[0] + if mask & (mask + 1) == 0: + n = mask.bit_length() + if n >= w: + return self.bv(others[0]) + return self._truncate(self.bv(others[0]), others[0], n) + return self._opaque(e) + + if kind == Z3_OP_EXTRACT: + hi, lo = e.params() + a = args[0] + if lo == 0 and hi + 1 >= a.size(): + return self.bv(a) + if lo == 0: + return self._truncate(self.bv(a), a, hi + 1) + shifted = self._div_const(self.bv(a), 2**lo) + if hi + 1 >= a.size(): + return shifted + # (a >> lo) mod 2^(hi - lo + 1) + return self._truncate(shifted, LShR(a, lo), hi - lo + 1) + + if kind == Z3_OP_CONCAT: + acc = None + for a in args: + term = self.bv(a) + if acc is None: + acc = term + elif self.small and 2 ** a.size() > MAX_SMALL_CONSTANT: + # the high part is scaled by a large constant + zeros = all(self._const(x) == 0 for x in args[:-1]) + acc = term if zeros else self._opaque(e) + if not zeros: + return acc + else: + acc = f"(+ (* {2 ** a.size()} {acc}) {term})" + return acc + + if kind == Z3_OP_ZERO_EXT: + return self.bv(args[0]) + + if kind == Z3_OP_ITE: + return self._ite(self.bool(args[0]), self.bv(args[1]), self.bv(args[2]), w) + + # dolmos abstractions of nonlinear arithmetic: exact when the divisor is constant + if kind == Z3_OP_UNINTERPRETED and len(args) == 2: + name = e.decl().name() + c = self._const(args[1]) + if name.startswith("f_evm_bvudiv") and c: + return self._div_const(self.bv(args[0]), c) + if name.startswith("f_evm_bvurem") and c: + return self._rem_const(self.bv(args[0]), c) + if name.startswith("f_evm_bvmul"): + c0, c1 = self._const(args[0]), self._const(args[1]) + if c0 is not None or c1 is not None: + coef, other = (c0, args[1]) if c0 is not None else (c1, args[0]) + return self._scale(other, coef, w) + + return self._opaque(e) + + def _scale(self, x: BitVecRef, coef: int, w: int) -> str: + """(coef * x) mod 2^w for a constant coef.""" + if coef == 0: + return "0" + if coef == 1: + return self.bv(x) + if self.small and coef > MAX_SMALL_CONSTANT: + self.reg.approximate = True + r = self._aux(w) + return r + wide = w + coef.bit_length() + no_wrap = ULT(ZeroExt(wide - w, x) * coef, BitVecVal(2**w, wide)) + return self._wrap(f"(* {coef} {self.bv(x)})", w, 0, max(coef - 1, 0), no_wrap) + + # booleans + + def _signed(self, e: BitVecRef) -> str: + w = e.size() + a = self.bv(e) + return self._ite(f"(>= {a} {2 ** (w - 1)})", f"(- {a} {2**w})", a, None) + + def _signed_cmp(self, op: str, a: BitVecRef, b: BitVecRef) -> str: + if self.small: + # without large constants: exact only when both operands are + # provably non-negative, in which case it is the unsigned comparison + w = a.size() + half = BitVecVal(2 ** (w - 1), w) + if self.prover.valid(And(ULT(a, half), ULT(b, half))): + return f"({op} {self.bv(a)} {self.bv(b)})" + self.reg.approximate = True + aux = self._aux(1) + return f"(= {aux} 1)" + return f"({op} {self._signed(a)} {self._signed(b)})" + + def _bool(self, e: BoolRef) -> str: + kind = e.decl().kind() + args = e.children() + + if kind == Z3_OP_TRUE: + return "true" + if kind == Z3_OP_FALSE: + return "false" + if kind == Z3_OP_NOT: + return f"(not {self.bool(args[0])})" + if kind == Z3_OP_AND: + return f"(and {' '.join(self.bool(a) for a in args)})" + if kind == Z3_OP_OR: + return f"(or {' '.join(self.bool(a) for a in args)})" + if kind == Z3_OP_IMPLIES: + return f"(or (not {self.bool(args[0])}) {self.bool(args[1])})" + if kind in (Z3_OP_IFF, Z3_OP_EQ) and is_bool(args[0]): + a, b = self.bool(args[0]), self.bool(args[1]) + return f"(or (and {a} {b}) (and (not {a}) (not {b})))" + if kind == Z3_OP_XOR: + a, b = self.bool(args[0]), self.bool(args[1]) + return f"(or (and {a} (not {b})) (and (not {a}) {b}))" + if kind == Z3_OP_ITE: + c, a, b = (self.bool(x) for x in args) + return f"(or (and {c} {a}) (and (not {c}) {b}))" + + if kind == Z3_OP_EQ: + return f"(= {self.bv(args[0])} {self.bv(args[1])})" + if kind == Z3_OP_DISTINCT and len(args) == 2: + return f"(not (= {self.bv(args[0])} {self.bv(args[1])}))" + + unsigned = {Z3_OP_ULT: "<", Z3_OP_ULEQ: "<=", Z3_OP_UGT: ">", Z3_OP_UGEQ: ">="} + if kind in unsigned: + return f"({unsigned[kind]} {self.bv(args[0])} {self.bv(args[1])})" + + signed = {Z3_OP_SLT: "<", Z3_OP_SLEQ: "<=", Z3_OP_SGT: ">", Z3_OP_SGEQ: ">="} + if kind in signed: + return self._signed_cmp(signed[kind], args[0], args[1]) + + # opaque boolean: encoded as an Int in {0, 1} + self.reg.approximate = True + b = self._aux(1) + return f"(= {b} 1)" + + def conj(self, parts: list[str]) -> str: + parts = [p for p in parts + self.constraints if p != "true"] + if not parts: + return "true" + if len(parts) == 1: + return parts[0] + return f"(and {' '.join(parts)})" + + +# +# lasso construction +# + + +def slice_conditions(conditions: list[BoolRef], seeds: list[ExprRef]) -> list[BoolRef]: + """Keeps the conditions transitively sharing variables with the seeds.""" + cond_vars = [{v.get_id() for v in get_vars(c)} for c in conditions] + wanted = {v.get_id() for s in seeds for v in get_vars(s)} + kept: set[int] = set() + changed = True + while changed: + changed = False + for i, vs in enumerate(cond_vars): + if i not in kept and vs & wanted: + kept.add(i) + wanted |= vs + changed = True + return [c for i, c in enumerate(conditions) if i in kept] + + +@dataclass +class BodyPath: + conditions: list[BoolRef] # conditions added during the iteration + outputs: list[ExprRef] # new values of the loop variables (in order) + context: list[BoolRef] = field(default_factory=list) # all path conditions + + +_LARGE_LITERAL_RE = re.compile(r"(? None: + for m in _LARGE_LITERAL_RE.finditer(formula): + if int(m.group(0)) > MAX_SMALL_CONSTANT: + raise LassoError(f"internal error: large literal {m.group(0)} in the lasso") + + +def build_lasso( + loop_vars: list[str], + widths: list[int], + initial_values: list[ExprRef], + stem_conditions: list[BoolRef], + guard: BoolRef | None, + bodies: list[BodyPath], + exact_constants: bool = False, + stem_context: list[BoolRef] | None = None, + prover_timeout_ms: int = 1000, + complete: bool = False, +) -> dict: + """ + loop_vars[i]: name of the i-th fresh loop variable (lasso_v...); + the branching condition is the last loop variable (0/1 or raw word), and + `guard` (over the loop variables) must hold to stay in the loop. + """ + small = not exact_constants + reg = Registry() + prog = [f"v{i}" for i in range(len(loop_vars))] + in_names = {lv: f"{p}_i" for lv, p in zip(loop_vars, prog, strict=True)} + + def upper(name: str, w: int) -> list[str]: + if small and 2**w > MAX_SMALL_CONSTANT: + return [] + return [f"(< {name} {2**w})"] + + # facts for the wrap-around prover: the current iteration was entered by + # taking the loop branch at the end of a previous iteration (there is one, + # since the unrolling bound was reached). Only valid if the body paths are + # complete, as the previous iteration may have followed any of them. + previous: list[BoolRef] = [] + if small and complete and bodies: + cur = [BitVec(name, 256) for name in loop_vars] + prev = [BitVec(f"{name}_prev", 256) for name in loop_vars] + pairs = list(zip(cur, prev, strict=True)) + previous.append( + Or( + *[ + And( + *[substitute(c, *pairs) for c in b.conditions], + *[ + v == substitute(out, *pairs) + for v, out in zip(cur, b.outputs, strict=True) + ], + ) + for b in bodies + ] + ) + ) + + # loop transition: one disjunct per body path + disjuncts = [] + loop_aux: list[str] = [] + for body in bodies: + prover = ( + WrapProver([*body.context, *previous], prover_timeout_ms) if small else None + ) + tr = Translator(reg, in_names, stem=False, prover=prover) + parts = [tr.bool(guard)] if guard is not None else [] + parts += [tr.bool(c) for c in body.conditions] + for p, out in zip(prog, body.outputs, strict=True): + parts.append(f"(= {p}_o {tr.any(out)})") + disjuncts.append(tr.conj(parts)) + loop_aux += tr.aux + + ranges = [] + for p, w in zip(prog, widths, strict=True): + for suffix in ("_i", "_o"): + ranges += [f"(<= 0 {p}{suffix})", *upper(f"{p}{suffix}", w)] + for name, w, _ in reg.invariants.values(): + ranges += [f"(<= 0 {name})", *upper(name, w)] + + body_formula = ( + disjuncts[0] if len(disjuncts) == 1 else f"(or {' '.join(disjuncts)})" + ) + loop_formula = f"(and {' '.join(ranges)} {body_formula})" + + invariant_names = [name for name, _, _ in reg.invariants.values()] + + # stem: initial values of the loop variables and of the loop invariants + prover = ( + WrapProver(stem_context or stem_conditions, prover_timeout_ms) + if small + else None + ) + tr = Translator(reg, {}, stem=True, prover=prover) + parts = [tr.bool(c) for c in stem_conditions] + for p, init in zip(prog, initial_values, strict=True): + parts.append(f"(= {p}_s {tr.any(init)})") + for name, _, term in list(reg.invariants.values()): + parts.append(f"(= {name}_s {tr.any(term)})") + stem_ranges = [] + for p, w in zip(prog, widths, strict=True): + stem_ranges += [f"(<= 0 {p}_s)", *upper(f"{p}_s", w)] + for name, w, _ in reg.invariants.values(): + stem_ranges += [f"(<= 0 {name}_s)", *upper(f"{name}_s", w)] + stem_formula = tr.conj(stem_ranges + parts) + + # large literals are constant program variables, identical in the stem and + # the loop; their only known facts are positivity and their relative order + big_names = [reg.big_constants[v] for v in sorted(reg.big_constants)] + order = [f"(<= 0 {big_names[0]})"] if big_names else [] + order += [f"(< {a} {b})" for a, b in zip(big_names, big_names[1:], strict=False)] + if order: + loop_formula = f"(and {' '.join(order)} {loop_formula})" + stem_order = [re.sub(r"\b(c\d+)\b", r"\1_s", o) for o in order] + stem_formula = f"(and {' '.join(stem_order)} {stem_formula})" + + if small: + check_small_constants(loop_formula) + check_small_constants(stem_formula) + + all_vars = prog + invariant_names + big_names + constants = invariant_names + big_names + return reg.approximate, { + "program_vars": all_vars, + "var_types": {v: "Int" for v in all_vars}, + "stem": [ + { + "source": "entry", + "target": "head", + "formula": stem_formula, + "in_vars": {v: f"{v}_e" for v in all_vars}, + "out_vars": {v: f"{v}_s" for v in all_vars}, + "aux_vars": tr.aux, + "assigned_vars": all_vars, + } + ], + "loop": [ + { + "source": "head", + "target": "head", + "formula": loop_formula, + "in_vars": {**{p: f"{p}_i" for p in prog}, **{k: k for k in constants}}, + "out_vars": { + **{p: f"{p}_o" for p in prog}, + **{k: k for k in constants}, + }, + "aux_vars": loop_aux, + "assigned_vars": prog, + } + ], + } + + +def fresh_loop_var(index: int, uid: int) -> BitVecRef: + return BitVec(f"{LOOP_VAR_PREFIX}{uid}_{index}", 256) + + +def as_z3(x) -> ExprRef: + return x.as_z3() if hasattr(x, "as_z3") else x + + +def same_term(a, b) -> bool: + if a is b: + return True + za, zb = as_z3(a), as_z3(b) + if is_bool(za) != is_bool(zb): + return False + return za.eq(zb) + + +def branch_taken(cond: ExprRef, direction: bool) -> BoolRef: + """The condition for a JUMPI on `cond` to take the `direction` branch.""" + if is_bool(cond): + return cond if direction else simplify(Not(cond)) + return cond != 0 if direction else cond == 0 + + +# +# PaSTTeL +# + +_VERDICT_RE = re.compile(r"OVERALL RESULT:\s*(\S+)") +_PROOF_RE = re.compile( + r"^(\S+\([^)]*\)|\S+)\s+(TERMINATING|NON-TERMINATING)\s+[\d.]+\s+(.*)$", re.M +) + + +def run_pasttel(binary: str, lasso_path: str, timeout: int) -> tuple[str, str | None]: + try: + proc = subprocess.run( + [binary, "-a", "both", "-t", str(timeout), lasso_path], + capture_output=True, + text=True, + timeout=timeout + 10, + ) + except subprocess.TimeoutExpired: + return "TIMEOUT", None + except OSError as err: + return f"ERROR ({err})", None + + output = proc.stdout + proc.stderr + with open(lasso_path.removesuffix(".json") + ".pasttel.txt", "w") as f: + f.write(output) + + verdict = m.group(1) if (m := _VERDICT_RE.search(output)) else "UNKNOWN" + proof = None + for m in _PROOF_RE.finditer(output): + if m.group(2) == verdict: + proof = f"{m.group(1)}: {m.group(3).strip()}" + break + return verdict, proof + + +def write_lasso(out_dir: str, name: str, lasso: dict, meta: dict) -> str: + os.makedirs(out_dir, exist_ok=True) + path = os.path.join(out_dir, f"{name}.json") + with open(path, "w") as f: + json.dump(lasso, f, indent=2) + with open(os.path.join(out_dir, f"{name}.meta.json"), "w") as f: + json.dump(meta, f, indent=2, default=str) + return path diff --git a/src/halmos/logs.py b/src/dolmos/logs.py similarity index 91% rename from src/halmos/logs.py rename to src/dolmos/logs.py index f44a2b18a..05d7814c5 100644 --- a/src/halmos/logs.py +++ b/src/dolmos/logs.py @@ -14,7 +14,7 @@ handlers=[RichHandler(level=logging.NOTSET, show_time=False, show_path=False)], ) -logger = logging.getLogger("halmos") +logger = logging.getLogger("dolmos") # @@ -33,7 +33,7 @@ def filter(self, record): return True -logger_unique = logging.getLogger("halmos.unique") +logger_unique = logging.getLogger("dolmos.unique") logger_unique.addFilter(UniqueLoggingFilter()) @@ -65,7 +65,7 @@ def debug_once(text: str) -> None: # Warnings with error code # -WARNINGS_BASE_URL = "https://github.com/a16z/halmos/wiki/warnings" +WARNINGS_BASE_URL = "https://github.com/Dowsers/dolmos/blob/main/docs/warnings.md" @dataclass diff --git a/src/halmos/mapper.py b/src/dolmos/mapper.py similarity index 94% rename from src/halmos/mapper.py rename to src/dolmos/mapper.py index f534e0c66..5425efc3b 100644 --- a/src/halmos/mapper.py +++ b/src/dolmos/mapper.py @@ -6,8 +6,8 @@ from dataclasses import dataclass, field from typing import Any, ForwardRef, Optional -from halmos.exceptions import HalmosException -from halmos.logs import debug +from dolmos.exceptions import DolmosException +from dolmos.logs import debug SELECTOR_FIELDS = { "VariableDeclaration": "functionSelector", @@ -204,6 +204,7 @@ def __init__(self): self._build_out_map: dict = None self._build_out_map_reverse: dict = None self._build_out_map_code: dict = None + self._vyper_code: list = None def set_build_out(self, build_out_map: dict): if self._build_out_map is build_out_map: @@ -212,6 +213,7 @@ def set_build_out(self, build_out_map: dict): self._build_out_map = build_out_map self._build_out_map_reverse = None self._build_out_map_code = None + self._vyper_code = None def create_build_out_map_reverse(self): # create reverse mapping @@ -276,6 +278,10 @@ def create_build_out_map_code(self): """ self._build_out_map_code = defaultdict(list) + # vyper appends immutables to the runtime code at deployment time, so the + # deployed code is longer than the compile-time runtime code (matched by prefix) + self._vyper_code = [] + empty = {"object": "0x"} for filename, file_map in self._build_out_map.items(): for contract_name, (contract_map, _, _) in file_map.items(): @@ -292,6 +298,9 @@ def create_build_out_map_code(self): code_data = (hexcode, placeholders, contract_name, filename, source_map) self._build_out_map_code[size].append(code_data) + if contract_map.get("language") == "vyper": + self._vyper_code.append(code_data) + def get_by_code( self, bytecode: ForwardRef("ByteVec") ) -> tuple[str | None, str | None, str | None]: @@ -323,13 +332,20 @@ def eq_bytes(bytecode: ForwardRef("ByteVec"), hexcode: str): if eq_except_placeholders(hexcode, placeholders): return (contract_name, filename, source_map) + # vyper contracts with immutables: compile-time runtime code + immutables section + for code_data in self._vyper_code: + hexcode, _, contract_name, filename, source_map = code_data + size = len(hexcode) // 2 + if size < len(bytecode) and eq_bytes(bytecode[:size], hexcode): + return (contract_name, filename, source_map) + return (None, None, None) def get_by_name(self, contract_name: str, filename: str = None) -> dict: """ Return the build output json for the given contract name. - Raise a HalmosException if the contract is not found, or cannot be uniquely determined. + Raise a DolmosException if the contract is not found, or cannot be uniquely determined. The optional filename argument is required, if the contract name appears in multiple files. """ @@ -339,11 +355,11 @@ def get_by_name(self, contract_name: str, filename: str = None) -> dict: mapping = self._build_out_map_reverse[contract_name] if not mapping: - raise HalmosException(f"{contract_name} is not found") + raise DolmosException(f"{contract_name} is not found") if filename is None: if len(mapping) > 1: - raise HalmosException( + raise DolmosException( f"{contract_name} exists in multiple files: {list(mapping.keys())}" ) [filename] = mapping.keys() @@ -351,7 +367,7 @@ def get_by_name(self, contract_name: str, filename: str = None) -> dict: result = mapping.get(filename) if not result: - raise HalmosException(f"{contract_name} is not found in {filename}") + raise DolmosException(f"{contract_name} is not found in {filename}") return result @@ -497,7 +513,7 @@ def main(): import json import sys - from halmos.utils import cyan + from dolmos.utils import cyan def read_json_file(file_path: str) -> dict: with open(file_path) as f: diff --git a/src/halmos/memtrace.py b/src/dolmos/memtrace.py similarity index 99% rename from src/halmos/memtrace.py rename to src/dolmos/memtrace.py index e82db5a93..737bf2ca6 100644 --- a/src/halmos/memtrace.py +++ b/src/dolmos/memtrace.py @@ -8,7 +8,7 @@ from rich.console import Console -from halmos.logs import debug +from dolmos.logs import debug console = Console() diff --git a/src/dolmos/pcex.py b/src/dolmos/pcex.py new file mode 100644 index 000000000..6745d5aa4 --- /dev/null +++ b/src/dolmos/pcex.py @@ -0,0 +1,1791 @@ +# SPDX-License-Identifier: AGPL-3.0 + +""" +Pretty counterexamples, enabled with --pretty-counterexamples (-pcex). + +The raw output of a counterexample is the solver model: one line per symbol, with the full +hex value of every word, e.g. 1024 bytes for a `bytes` argument whose length is 65. This module +turns the model into something that can be acted upon: + +- the arguments of the test are decoded with its ABI: the lengths of dynamic arguments are + applied, and values are rendered by type (decimal amounts, checksummed addresses, strings); +- `bytes` values that hold calldata are decoded with the ABIs of the compiled contracts, + e.g. `Token.transfer(to: 0x…, amount: 2)` (halmos#369); +- `bytes4` values are rendered as function selectors, including the empty selector 0x00000000 + of plain ether transfers (halmos#419); +- invariant call sequences are rendered with their concrete senders, values and arguments; +- a forge test that replays the counterexample is generated; +- duplicate counterexamples are hidden (halmos#398). + +Potentially invalid counterexamples are checked against the real EXP by the solver loop of +solve.py (see refine_exp, halmos#280). + +Threading: rendering runs in the callbacks of the solver threads, so nothing here may touch +z3 objects, except the collect_* functions, which run on the main thread when a potential +assertion violation is found, and return plain Python data. +""" + +import json +import re +import threading +from collections.abc import Iterable +from dataclasses import dataclass, field + +from eth_hash.auto import keccak + +# a raw model variable has .value (int) and .size_bits (int); see solve.ModelVariable +Model = dict + +WORD_BITS = 256 +WORD_MODULUS = 2**256 + +# selector of plain ether transfers and of calls with empty calldata +EMPTY_SELECTOR = b"\x00\x00\x00\x00" + +# limits, to keep the output readable +MAX_INLINE_ITEMS = 8 +MAX_HEX_BYTES = 160 +MAX_DECODE_DEPTH = 2 +MAX_ARRAY_LENGTH = 4096 + + +# +# symbol names +# + +# p____, created for ABI encoded arguments (see calldata.py); +# p__length__ for the length of a dynamic array, bytes or string +p_symbol_pattern = re.compile( + r"^p_(?P.*)_(?P[a-z]+[0-9]*)_(?P[0-9a-f]{7})_(?P\d+)$" +) + +# dolmos_