Merge pull request crytic#1421 from crytic/test-improvements

Test improvements

Author: elopez

.github/scripts/install-bitwuzla.sh

@@ -0,0 +1,23 @@
+#!/bin/bash
+set -eux -o pipefail
+
+VERSION=0.8.2
+
+mkdir -p "$HOME/.local/bin/"
+
+if [ "$HOST_OS" = "Linux" ]; then
+  if [ $(uname -m) = "aarch64" ]; then
+    curl -fsSL -o bitwuzla.zip https://github.com/bitwuzla/bitwuzla/releases/download/0.8.2/Bitwuzla-Linux-arm64-static.zip
+  elif [ $(uname -m) = "x86_64" ]; then
+    curl -fsSL -o bitwuzla.zip https://github.com/bitwuzla/bitwuzla/releases/download/0.8.2/Bitwuzla-Linux-x86_64-static.zip
+  fi
+  unzip bitwuzla.zip
+  cp Bitwuzla*/bin/bitwuzla "$HOME/.local/bin/"
+fi
+if [ "$HOST_OS" = "Windows" ]; then
+  curl -fsSL "https://github.com/bitwuzla/bitwuzla/releases/download/$VERSION/Bitwuzla-Win64-x86_64-static.zip" -o bitwuzla.zip
+  unzip bitwuzla.zip
+  cp Bitwuzla*/bin/bitwuzla.exe "$HOME/.local/bin/"
+fi
+
+rm -rf bitwuzla.zip Bitwuzla*/

.github/scripts/install-z3.sh

@@ -2,8 +2,14 @@
 set -eux -o pipefail
 
 if [ "$HOST_OS" = "Linux" ]; then
-  sudo apt-get update
-  sudo apt-get install -y z3
+  if [ $(uname -m) = "aarch64" ]; then
+    curl -fsSL -o z3.zip https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-arm64-glibc-2.34.zip
+  elif [ $(uname -m) = "x86_64" ]; then
+    curl -fsSL -o z3.zip https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-x64-glibc-2.39.zip
+  fi
+  unzip z3.zip
+  cp -a z3-*/bin/z3 "$HOME/.local/bin/"
+  rm -rf z3-*/ z3.zip
 fi
 if [ "$HOST_OS" = "Windows" ]; then
   choco install z3

.github/workflows/ci.yml

@@ -220,7 +220,8 @@ jobs:
           - ubuntu-latest
           - windows-latest
         solc: ${{
-            (github.event_name == 'push' && github.ref == 'refs/heads/master') &&
+            ((github.event_name == 'push' && github.ref == 'refs/heads/master') ||
+             (github.event_name == 'pull_request' && contains(github.event.pull_request.labels.*.name, 'ci-all-solc'))) &&
             fromJSON('["0.4.25", "0.5.7", "0.6.12", "0.7.5", "0.8.10", "0.8.25"]') ||
             fromJSON('["0.8.10", "0.8.25"]')
           }}
@@ -243,6 +244,7 @@ jobs:
           .github/scripts/install-solc.sh
           .github/scripts/install-crytic-compile.sh
           .github/scripts/install-z3.sh
+          .github/scripts/install-bitwuzla.sh
         env:
           HOST_OS: ${{ runner.os }}
           SOLC_VER: ${{ matrix.solc }}
@@ -254,6 +256,8 @@ jobs:
 
       - name: Test
         run: |
+          export PATH="$PATH:$HOME/.local/bin"
           solc-select use ${{ matrix.solc }}
           chmod +x echidna-testsuite*
           ./echidna-testsuite*
+        shell: bash

src/test/Tests/Symbolic.hs

@@ -5,18 +5,21 @@ import Common (testContract', solcV, solved, verified)
 import Echidna.Types.Worker (WorkerType(..))
 
 symbolicTests :: TestTree
-symbolicTests = testGroup "Symbolic tests"
-  [ testContract' "symbolic/verify.sol" Nothing (Just (>= solcV (0,6,9))) (Just "symbolic/verify.yaml") True SymbolicWorker
+symbolicTests = testGroup "Symbolic tests" $
+  map (\conf ->
+    testContract' "symbolic/verify.sol" Nothing (Just (>= solcV (0,6,9))) (Just conf) True SymbolicWorker
       [ ("simple passed", solved "simple")
       , ("array passed", solved "array")
       , ("negative passed", solved "negative")
       , ("close passed", solved "close")
       , ("far not verified", verified "far")
       , ("correct not verified", verified "correct")
-    ]
+      ]
+  ) ["symbolic/verify.yaml", "symbolic/verify.bitwuzla.yaml"]
+  ++ ([
     -- This test is commented out because it requires a specific setup where both the FuzzWorker and SymbolicWorker are used.
     -- If you run the symbolic worker alone, it will hang indefinitely.
     --, testContract' "symbolic/explore.sol" Nothing Nothing (Just "symbolic/explore.yaml") True SymbolicWorker
     --  [ ("f passed", solved "f")
     --]
-  ]
+  ] :: [TestTree])

tests/solidity/cheat/ffi.sol

@@ -11,10 +11,10 @@ contract TestFFI {
 
   function foo(int x) external {
     string[] memory inputs = new string[](3);
-    inputs[0] = "python3";
+    inputs[0] = "sh";
     inputs[1] = "-c";
     // ABI encoded "gm", as a string
-    inputs[2] = "print('0x00000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000002676d000000000000000000000000000000000000000000000000000000000000', end='')";
+    inputs[2] = "printf '%s' '0x00000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000002676d000000000000000000000000000000000000000000000000000000000000'";
 
     bytes memory res = Hevm(HEVM_ADDRESS).ffi(inputs);
 

tests/solidity/symbolic/verify.bitwuzla.yaml

@@ -0,0 +1,5 @@
+testMode: assertion
+symExec: true
+symExecSMTSolver: bitwuzla
+workers: 0
+seqLen: 1