From 54310e656bfa3fc57a096ca99c4381b1db45a084 Mon Sep 17 00:00:00 2001 From: cyberthirst Date: Wed, 30 Oct 2024 10:35:00 +0100 Subject: [PATCH 1/5] add basic hevm runner script --- scripts/symbolic_tests.sh | 79 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100755 scripts/symbolic_tests.sh diff --git a/scripts/symbolic_tests.sh b/scripts/symbolic_tests.sh new file mode 100755 index 0000000000..54644278c9 --- /dev/null +++ b/scripts/symbolic_tests.sh @@ -0,0 +1,79 @@ +#!/usr/bin/env bash +set -euo pipefail + +# Default values +SOLVER="z3" +TIMEOUT=300 +NUM_CORES=$(nproc 2>/dev/null || sysctl -n hw.ncpu) +TARGET_DIR="examples" +SPECIFIC_CONTRACT="" + +# Parse arguments +while [[ $# -gt 0 ]]; do + case $1 in + --solver) + SOLVER="$2" + shift 2 + ;; + --timeout) + TIMEOUT="$2" + shift 2 + ;; + --cores) + NUM_CORES="$2" + shift 2 + ;; + --contract) + SPECIFIC_CONTRACT="$2" + shift 2 + ;; + *) + echo "Unknown option: $1" + exit 1 + ;; + esac +done + +# Function to run hevm equivalence check +check_equivalence() { + local contract=$1 + local base_name=$(basename "$contract") + + echo "Testing equivalence for $base_name..." + + hevm equivalence \ + --code-a "$(vyper -f bytecode_runtime --no-optimize "$contract")" \ + --code-b "$(vyper -f bytecode_runtime --experimental-codegen --no-optimize "examples/factory/Factory.vy")" \ + --solver "$SOLVER" \ + --smttimeout "$TIMEOUT" \ + --num-solvers "$NUM_CORES" +} + +# Main testing function +test_contract() { + local contract=$1 + local base_name=$(basename "$contract") + + echo "Processing $base_name..." + + if ! check_equivalence "$contract"; then + echo "❌ Equivalence check failed for $base_name" + return 1 + else + echo "✅ Equivalence check passed for $base_name" + fi +} + +# Main execution +if [ -n "$SPECIFIC_CONTRACT" ]; then + if [ ! -f "$SPECIFIC_CONTRACT" ]; then + echo "Contract file not found: $SPECIFIC_CONTRACT" + exit 1 + fi + test_contract "$SPECIFIC_CONTRACT" +else + # Find all Vyper contracts in examples directory + find "$TARGET_DIR" -name "*.vy" -type f | while read -r contract; do + test_contract "$contract" + done +fi From 299aa0f03b524bceda9995fe2675e35e453b80b5 Mon Sep 17 00:00:00 2001 From: cyberthirst Date: Wed, 30 Oct 2024 10:40:50 +0100 Subject: [PATCH 2/5] add exit value based on eq results --- scripts/symbolic_tests.sh | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/scripts/symbolic_tests.sh b/scripts/symbolic_tests.sh index 54644278c9..d307ae6bad 100755 --- a/scripts/symbolic_tests.sh +++ b/scripts/symbolic_tests.sh @@ -64,16 +64,21 @@ test_contract() { fi } +# Track if any test failed +any_failed=0 + # Main execution if [ -n "$SPECIFIC_CONTRACT" ]; then if [ ! -f "$SPECIFIC_CONTRACT" ]; then echo "Contract file not found: $SPECIFIC_CONTRACT" exit 1 fi - test_contract "$SPECIFIC_CONTRACT" + test_contract "$SPECIFIC_CONTRACT" || any_failed=1 else # Find all Vyper contracts in examples directory find "$TARGET_DIR" -name "*.vy" -type f | while read -r contract; do - test_contract "$contract" + test_contract "$contract" || any_failed=1 done fi + +exit $any_failed From 94ccb06ea2fa0b8ed8d3966bd43578e3bdb1cdcf Mon Sep 17 00:00:00 2001 From: cyberthirst Date: Wed, 30 Oct 2024 11:03:56 +0100 Subject: [PATCH 3/5] add debug mode --- scripts/symbolic_tests.sh | 40 ++++++++++++++++++++++++--------------- 1 file changed, 25 insertions(+), 15 deletions(-) diff --git a/scripts/symbolic_tests.sh b/scripts/symbolic_tests.sh index d307ae6bad..0aa801d848 100755 --- a/scripts/symbolic_tests.sh +++ b/scripts/symbolic_tests.sh @@ -4,9 +4,11 @@ set -euo pipefail # Default values SOLVER="z3" TIMEOUT=300 -NUM_CORES=$(nproc 2>/dev/null || sysctl -n hw.ncpu) +NUM_CORES=$(nproc 2>/dev/null || sysctl -n hw.ncpu 2>/dev/null || echo 1) TARGET_DIR="examples" SPECIFIC_CONTRACT="" +DEBUG=false + # Parse arguments while [[ $# -gt 0 ]]; do @@ -27,6 +29,10 @@ while [[ $# -gt 0 ]]; do SPECIFIC_CONTRACT="$2" shift 2 ;; + --debug) + DEBUG=true + shift + ;; *) echo "Unknown option: $1" exit 1 @@ -37,30 +43,34 @@ done # Function to run hevm equivalence check check_equivalence() { local contract=$1 - local base_name=$(basename "$contract") - - echo "Testing equivalence for $base_name..." + + echo "Testing equivalence for $contract..." + + local cmd="hevm equivalence \ + --code-a \"$(vyper -f bytecode_runtime --no-optimize $contract)\" \ + --code-b \"$(vyper -f bytecode_runtime --experimental-codegen --no-optimize $contract)\" \ + --solver \"$SOLVER\" \ + --smttimeout \"$TIMEOUT\" \ + --num-solvers \"$NUM_CORES\"" - hevm equivalence \ - --code-a "$(vyper -f bytecode_runtime --no-optimize "$contract")" \ - --code-b "$(vyper -f bytecode_runtime --experimental-codegen --no-optimize "examples/factory/Factory.vy")" \ - --solver "$SOLVER" \ - --smttimeout "$TIMEOUT" \ - --num-solvers "$NUM_CORES" + if [ "$DEBUG" = true ]; then + time eval "$cmd" + else + eval "$cmd" + fi } # Main testing function test_contract() { local contract=$1 - local base_name=$(basename "$contract") - - echo "Processing $base_name..." + + echo "Processing $contract..." if ! check_equivalence "$contract"; then - echo "❌ Equivalence check failed for $base_name" + echo "❌ Equivalence check failed for $contract" return 1 else - echo "✅ Equivalence check passed for $base_name" + echo "✅ Equivalence check passed for $contract" fi } From 59d70c290a8079b1da6ab9d0477c4eef0d84b37d Mon Sep 17 00:00:00 2001 From: cyberthirst Date: Wed, 30 Oct 2024 11:12:57 +0100 Subject: [PATCH 4/5] add support to exclude contracts --- scripts/symbolic_tests.sh | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/scripts/symbolic_tests.sh b/scripts/symbolic_tests.sh index 0aa801d848..ad656c9ded 100755 --- a/scripts/symbolic_tests.sh +++ b/scripts/symbolic_tests.sh @@ -9,6 +9,16 @@ TARGET_DIR="examples" SPECIFIC_CONTRACT="" DEBUG=false +# Contracts to exclude from testing +EXCLUDED_CONTRACTS=( + "examples/wallet/wallet.vy" # CopySlice with a symbolically sized region not currently implemented + "examples/voting/ballot.vy" # loooong + "examples/auctions/blind_auction.vy" # loooong + "examples/tokens/ERC4626.vy" # loong + "examples/tokens/ERC1155ownable.vy" #looong + "examples/tokens/ERC721.vy" # loongs + "examples/name_registry/name_registry.vy" # again copy slice? +) # Parse arguments while [[ $# -gt 0 ]]; do @@ -40,6 +50,17 @@ while [[ $# -gt 0 ]]; do esac done +# Function to check if contract should be excluded +is_excluded() { + local contract=$1 + for excluded in "${EXCLUDED_CONTRACTS[@]}"; do + if [ "$contract" = "$excluded" ]; then + return 0 + fi + done + return 1 +} + # Function to run hevm equivalence check check_equivalence() { local contract=$1 @@ -64,6 +85,11 @@ check_equivalence() { test_contract() { local contract=$1 + if is_excluded "$contract"; then + echo "Skipping excluded contract: $contract" + return 0 + fi + echo "Processing $contract..." if ! check_equivalence "$contract"; then From 39e80ba58a898b7f5645c442d9808078314b9e41 Mon Sep 17 00:00:00 2001 From: cyberthirst Date: Wed, 30 Oct 2024 11:59:22 +0100 Subject: [PATCH 5/5] print summary --- scripts/symbolic_tests.sh | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/scripts/symbolic_tests.sh b/scripts/symbolic_tests.sh index ad656c9ded..e6fb581f69 100755 --- a/scripts/symbolic_tests.sh +++ b/scripts/symbolic_tests.sh @@ -3,7 +3,7 @@ set -euo pipefail # Default values SOLVER="z3" -TIMEOUT=300 +TIMEOUT=600 # hevm default is 300 NUM_CORES=$(nproc 2>/dev/null || sysctl -n hw.ncpu 2>/dev/null || echo 1) TARGET_DIR="examples" SPECIFIC_CONTRACT="" @@ -12,12 +12,11 @@ DEBUG=false # Contracts to exclude from testing EXCLUDED_CONTRACTS=( "examples/wallet/wallet.vy" # CopySlice with a symbolically sized region not currently implemented - "examples/voting/ballot.vy" # loooong - "examples/auctions/blind_auction.vy" # loooong - "examples/tokens/ERC4626.vy" # loong - "examples/tokens/ERC1155ownable.vy" #looong - "examples/tokens/ERC721.vy" # loongs - "examples/name_registry/name_registry.vy" # again copy slice? + "examples/name_registry/name_registry.vy" # CopySlice with a symbolically sized region not currently implemented + "examples/auctions/blind_auction.vy" # 1x -> SMT result timeout/unknown for TIMEOUT=600 + "examples/tokens/ERC1155ownable.vy" # long time to finish + "examples/voting/ballot.vy" # long time to finish + "examples/tokens/ERC721.vy" # long time to finish ) # Parse arguments @@ -117,4 +116,10 @@ else done fi +if [ $any_failed -eq 0 ]; then + echo "✅ All tests passed" +else + echo "❌ Some tests failed" +fi + exit $any_failed