feat[test]: add hevm harness for venom passes

.github/workflows/test.yml

@@ -60,6 +60,45 @@ jobs:
       - name: Run docs
         run: sphinx-build -E -b html docs dist/docs -n -q --color
 
+  # Symbolic tests
+  symbolic-tests:
+    runs-on: "ubuntu-latest"
+    name: symbolic-tests
+
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Set up Python 3.11
+      uses: actions/setup-python@v5
+      with:
+        python-version: "3.11"
+        cache: "pip"
+
+    - name: Install dependencies
+      run: pip install .[test]
+
+    - name: Install hevm
+      run: |
+        # hevm dependency
+        sudo apt-get install z3
+
+        wget --no-verbose -O hevm https://github.com/ethereum/hevm/releases/download/release/0.54.2/hevm-x86_64-linux
+        chmod +x hevm
+        mkdir -p "$HOME/.local/bin/"
+        mv hevm "$HOME/.local/bin/"
+        echo "$HOME/.local/bin/" >> $GITHUB_PATH
+
+        hevm version
+
+    - name: Run tests
+      run: >
+        pytest
+        -m "hevm"
+        --hevm
+        --cov-config=setup.cfg
+        --cov=vyper
+        tests/
+
   # "Regular"/core tests.
   tests:
     runs-on: ${{ matrix.os || 'ubuntu' }}-latest
@@ -166,7 +205,7 @@ jobs:
     # summary result from test matrix.
     # see https://github.community/t/status-check-for-a-matrix-jobs/127354/7
     runs-on: ubuntu-latest
-    needs: [tests]
+    needs: [tests, symbolic-tests]
     steps:
       - name: Check tests tests all succeeded
         if: ${{ needs.tests.result != 'success' }}

README.md

@@ -53,6 +53,10 @@ make dev-init
 ./quicktest.sh -m "not fuzzing"
 ```
 
+## Testing (with hevm)
+
+Install hevm by downloading it from the releases page (https://github.com/ethereum/hevm/releases/latest) and making sure it is in your PATH. hevm tests can be enabled with `--hevm` flag, and hevm tests can be selected with the `-m hevm` marker. For instance, `./quicktest.sh -m "hevm" --hevm`.
+
 ## Developing (working on the compiler)
 
 A useful script to have in your PATH is something like the following:
@@ -67,7 +71,9 @@ To run a python performance profile (to find compiler perf hotspots):
 PYTHONPATH=. python -m cProfile -s tottime vyper/cli/vyper_compile.py "$@"
 ```
 
-To get a call graph from a python profile, https://stackoverflow.com/a/23164271/ is helpful.
+To get a call graph from a python profile, pip install `gprof2dot` and `xdot`, and run it like `gprof2dot -f pstats stats | xdot -`. (See https://stackoverflow.com/a/23164271/).
+
+The utility timer functions `timeit`, `profileit` and `cumtimeit` are available in `vyper/utils.py`.
 
 
 # Contributing

setup.cfg

@@ -26,14 +26,15 @@ line_length = 100
 [tool:pytest]
 addopts = -n auto
 	--dist worksteal
+	--strict-markers
 python_files = test_*.py
 testpaths = tests
 xfail_strict = true
 markers =
 	fuzzing: Run Hypothesis fuzz test suite (deselect with '-m "not fuzzing"')
 	requires_evm_version(version): Mark tests that require at least a specific EVM version and would throw `EvmVersionException` otherwise
 	venom_xfail: mark a test case as a regression (expected to fail) under the venom pipeline
-
+	hevm: run tests marked for symbolic execution
 
 [coverage:run]
 branch = True

tests/conftest.py

@@ -7,6 +7,7 @@
 from eth_keys.datatypes import PrivateKey
 from hexbytes import HexBytes
 
+import tests.hevm
 import vyper.evm.opcodes as evm_opcodes
 from tests.evm_backends.base_env import BaseEnv, ExecutionReverted
 from tests.evm_backends.pyevm_env import PyEvmEnv
@@ -40,6 +41,7 @@ def pytest_addoption(parser):
     parser.addoption("--enable-compiler-debug-mode", action="store_true")
     parser.addoption("--experimental-codegen", action="store_true")
     parser.addoption("--tracing", action="store_true")
+    parser.addoption("--hevm", action="store_true")
 
     parser.addoption(
         "--evm-version",
@@ -114,6 +116,13 @@ def evm_version(pytestconfig):
     return pytestconfig.getoption("evm_version")
 
 
+@pytest.fixture(scope="session", autouse=True)
+def set_hevm(pytestconfig):
+    flag_value = pytestconfig.getoption("hevm")
+    assert isinstance(flag_value, bool)
+    tests.hevm.HAS_HEVM = flag_value
+
+
 @pytest.fixture(scope="session")
 def evm_backend(pytestconfig):
     backend_str = pytestconfig.getoption("evm_backend")

tests/hevm.py

@@ -0,0 +1,80 @@
+import subprocess
+
+from tests.venom_utils import parse_from_basic_block
+from vyper.ir.compile_ir import assembly_to_evm
+from vyper.venom import StoreExpansionPass, VenomCompiler
+from vyper.venom.analysis import IRAnalysesCache
+from vyper.venom.basicblock import IRInstruction, IRLiteral
+
+HAS_HEVM: bool = False
+
+
+def _prep_hevm_venom(venom_source_code):
+    ctx = parse_from_basic_block(venom_source_code)
+
+    num_calldataloads = 0
+    for fn in ctx.functions.values():
+        for bb in fn.get_basic_blocks():
+            for inst in bb.instructions:
+                # transform `param` instructions into "symbolic" values for
+                # hevm via calldataload
+                if inst.opcode == "param":
+                    # hevm limit: 256 bytes of symbolic calldata
+                    assert num_calldataloads < 8
+
+                    inst.opcode = "calldataload"
+                    inst.operands = [IRLiteral(num_calldataloads * 32)]
+                    num_calldataloads += 1
+
+            term = bb.instructions[-1]
+            # test convention, terminate by `return`ing the variables
+            # you want to check
+            assert term.opcode == "return"
+            num_return_values = 0
+            for op in term.operands:
+                ptr = IRLiteral(num_return_values * 32)
+                new_inst = IRInstruction("mstore", [op, ptr])
+                bb.insert_instruction(new_inst, index=-1)
+                num_return_values += 1
+
+            # return 0, 32 * num_variables
+            term.operands = [IRLiteral(num_return_values * 32), IRLiteral(0)]
+
+        ac = IRAnalysesCache(fn)
+        # requirement for venom_to_assembly
+        StoreExpansionPass(ac, fn).run_pass()
+
+    compiler = VenomCompiler([ctx])
+    return assembly_to_evm(compiler.generate_evm(no_optimize=True))[0].hex()
+
+
+def hevm_check_venom(pre, post, verbose=False):
+    global HAS_HEVM
+
+    if not HAS_HEVM:
+        return
+
+    # perform hevm equivalence check
+    if verbose:
+        print("HEVM COMPARE.")
+        print("BEFORE:", pre)
+        print("OPTIMIZED:", post)
+    bytecode1 = _prep_hevm_venom(pre)
+    bytecode2 = _prep_hevm_venom(post)
+
+    hevm_check_bytecode(bytecode1, bytecode2, verbose=verbose)
+
+
+def hevm_check_bytecode(bytecode1, bytecode2, verbose=False):
+    # debug:
+    if verbose:
+        print("RUN HEVM:")
+        print(bytecode1)
+        print(bytecode2)
+
+    subp_args = ["hevm", "equivalence", "--code-a", bytecode1, "--code-b", bytecode2]
+
+    if verbose:
+        subprocess.check_call(subp_args)
+    else:
+        subprocess.check_output(subp_args)

tests/unit/compiler/venom/test_algebraic_binopt.py

@@ -1,5 +1,6 @@
 import pytest
 
+from tests.hevm import hevm_check_venom
 from tests.venom_utils import assert_ctx_eq, parse_from_basic_block
 from vyper.venom.analysis import IRAnalysesCache
 from vyper.venom.passes import AlgebraicOptimizationPass, StoreElimination
@@ -8,8 +9,10 @@
 Test abstract binop+unop optimizations in algebraic optimizations pass
 """
 
+pytestmark = pytest.mark.hevm
 
-def _sccp_algebraic_runner(pre, post):
+
+def _sccp_algebraic_runner(pre, post, hevm=True):
     ctx = parse_from_basic_block(pre)
 
     for fn in ctx.functions.values():
@@ -20,6 +23,10 @@ def _sccp_algebraic_runner(pre, post):
 
     assert_ctx_eq(ctx, parse_from_basic_block(post))
 
+    if not hevm:
+        return
+    hevm_check_venom(pre, post)
+
 
 def test_sccp_algebraic_opt_sub_xor():
     # x - x -> 0
@@ -87,7 +94,8 @@ def test_sccp_algebraic_opt_sub_xor_max():
         return %1, %2, %3
     """
 
-    _sccp_algebraic_runner(pre, post)
+    # hevm chokes on this example.
+    _sccp_algebraic_runner(pre, post, hevm=False)
 
 
 def test_sccp_algebraic_opt_shift():
@@ -222,7 +230,7 @@ def test_sccp_algebraic_opt_mul_div_to_shifts(n):
         return %1, %2, %3, %4, %5, %6
     """
 
-    _sccp_algebraic_runner(pre, post)
+    _sccp_algebraic_runner(pre, post, hevm=False)
 
 
 def test_sccp_algebraic_opt_exp():
@@ -244,7 +252,8 @@ def test_sccp_algebraic_opt_exp():
         return 1, 1, %3, %par
     """
 
-    _sccp_algebraic_runner(pre, post)
+    # can set hevm=True after https://github.com/ethereum/hevm/pull/638 is merged
+    _sccp_algebraic_runner(pre, post, hevm=False)
 
 
 def test_sccp_algebraic_opt_compare_self():

vyper/venom/passes/algebraic_optimization.py

@@ -393,7 +393,11 @@ def _optimize_comparator_instruction(self, inst, prefer_iszero):
 
         if lit_eq(operands[0], almost_never):
             # (lt x 1), (gt x (MAX_UINT256 - 1)), (slt x (MIN_INT256 + 1))
+
+            # correct optimization:
             self.updater._update(inst, "eq", [operands[1], IRLiteral(never)])
+            # canary:
+            # self.updater._update(inst, "eq", [operands[1], IRLiteral(lo)])
             return
 
         # rewrites. in positions where iszero is preferred, (gt x 5) => (ge x 6)