Merge branch 'main' into per-mapping-smt-array

ethereum · Jan 16, 2024 · a07ebff · a07ebff
2 parents 9376006 + 7a828a5
commit a07ebff
Show file tree

Hide file tree

Showing 25 changed files with 815 additions and 666 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -12,6 +12,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## Added
 - Optimized smt queries that significantly improve performance when dealing with solidity mappings and arrays
+- Support for using Bitwuzla as a solver
 - Symbolic tests now support statically sized arrays as parameters
 - `hevm test` now has a `num-solvers` parameter that controls how many solver instances to spawn
 - New solc-specific simplification rules that should make the final Props a lot more readable

diff --git a/cli/cli.hs b/cli/cli.hs
@@ -41,7 +41,8 @@ import EVM.Solvers
 import EVM.Stepper qualified
 import EVM.SymExec
 import EVM.Transaction qualified
-import EVM.Types hiding (word, Env)
+import EVM.Types hiding (word, Env, Symbolic)
+import EVM.Types qualified
 import EVM.UnitTest
 import EVM.Effects
 
@@ -84,7 +85,7 @@ data Command w
       , showReachableTree :: w ::: Bool           <?> "Print only reachable branches explored in tree view"
       , smttimeout    :: w ::: Maybe Natural      <?> "Timeout given to SMT solver in seconds (default: 300)"
       , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"
-      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc5"
+      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"
       , debug         :: w ::: Bool               <?> "Debug printing of internal behaviour"
       , trace         :: w ::: Bool               <?> "Dump trace"
@@ -104,7 +105,7 @@ data Command w
       , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"
       , smttimeout    :: w ::: Maybe Natural    <?> "Timeout given to SMT solver in seconds (default: 300)"
       , maxIterations :: w ::: Maybe Integer    <?> "Number of times we may revisit a particular branching point"
-      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc5"
+      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
       , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"
       , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"
       , debug         :: w ::: Bool             <?> "Debug printing of internal behaviour"
@@ -150,7 +151,7 @@ data Command w
       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"
       , coverage      :: w ::: Bool                     <?> "Coverage analysis"
       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
-      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc5"
+      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default), cvc5, or bitwuzla"
       , numSolvers    :: w ::: Maybe Natural            <?> "Number of solver instances to use (default: number of cpu cores)"
       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"
       , debug         :: w ::: Bool                     <?> "Debug printing of internal behaviour"
@@ -265,6 +266,7 @@ getSolver cmd = case cmd.solver of
                   Just s -> case T.unpack s of
                               "z3" -> pure Z3
                               "cvc5" -> pure CVC5
+                              "bitwuzla" -> pure Bitwuzla
                               input -> do
                                 putStrLn $ "unrecognised solver: " <> input
                                 exitFailure
@@ -407,7 +409,7 @@ launchExec cmd = do
         internalError "no EVM result"
 
 -- | Creates a (concrete) VM from command line options
-vmFromCommand :: Command Options.Unwrapped -> IO (VM RealWorld)
+vmFromCommand :: Command Options.Unwrapped -> IO (VM Concrete RealWorld)
 vmFromCommand cmd = do
   (miner,ts,baseFee,blockNum,prevRan) <- case cmd.rpc of
     Nothing -> pure (LitAddr 0,Lit 0,0,0,0)
@@ -492,14 +494,13 @@ vmFromCommand cmd = do
           , baseState      = EmptyBase
           , txAccessList   = mempty -- TODO: support me soon
           , allowFFI       = False
-          , symbolic       = False
           }
         word f def = fromMaybe def (f cmd)
         word64 f def = fromMaybe def (f cmd)
         addr f def = maybe def LitAddr (f cmd)
         bytes f def = maybe def decipher (f cmd)
 
-symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM RealWorld)
+symvmFromCommand :: Command Options.Unwrapped -> (Expr Buf, [Prop]) -> IO (VM EVM.Types.Symbolic RealWorld)
 symvmFromCommand cmd calldata = do
   (miner,blockNum,baseFee,prevRan) <- case cmd.rpc of
     Nothing -> pure (SymAddr "miner",0,0,0)
@@ -557,7 +558,7 @@ symvmFromCommand cmd calldata = do
       , address        = address
       , caller         = caller
       , origin         = origin
-      , gas            = word64 (.gas) 0xffffffffffffffff
+      , gas            = ()
       , gaslimit       = word64 (.gaslimit) 0xffffffffffffffff
       , baseFee        = baseFee
       , priorityFee    = word (.priorityFee) 0
@@ -574,7 +575,6 @@ symvmFromCommand cmd calldata = do
       , baseState      = maybe AbstractBase parseInitialStorage (cmd.initialStorage)
       , txAccessList   = mempty
       , allowFFI       = False
-      , symbolic       = True
       }
     word f def = fromMaybe def (f cmd)
     word64 f def = fromMaybe def (f cmd)

diff --git a/doc/src/equivalence.md b/doc/src/equivalence.md
@@ -18,7 +18,7 @@ Available options:
   --smttimeout NATURAL     Timeout given to SMT solver in seconds (default: 300)
   --max-iterations INTEGER Number of times we may revisit a particular branching
                            point
-  --solver TEXT            Used SMT solver: z3 (default) or cvc5
+  --solver TEXT            Used SMT solver: z3 (default), cvc5, or bitwuzla
   --smtoutput              Print verbose smt output
   --smtdebug               Print smt queries sent to the solver
   --ask-smt-iterations INTEGER

diff --git a/doc/src/symbolic.md b/doc/src/symbolic.md
@@ -55,7 +55,7 @@ Available options:
   --smttimeout NATURAL     Timeout given to SMT solver in seconds (default: 300)
   --max-iterations INTEGER Number of times we may revisit a particular branching
                            point
-  --solver TEXT            Used SMT solver: z3 (default) or cvc5
+  --solver TEXT            Used SMT solver: z3 (default), cvc5, or bitwuzla
   --smtdebug               Print smt queries sent to the solver
   --assertions [WORD256]   Comma separated list of solc panic codes to check for
                            (default: user defined assertion violations only)

diff --git a/doc/src/test.md b/doc/src/test.md
@@ -1,4 +1,4 @@
-# `hevm dapp-test`
+# `hevm test`
 
 ```
 Usage: hevm test [--root STRING] [--project-type PROJECTTYPE] [--rpc TEXT]
@@ -18,7 +18,8 @@ Available options:
   --verbose INT            Append call trace: {1} failures {2} all
   --coverage               Coverage analysis
   --match STRING           Test case filter - only run methods matching regex
-  --solver TEXT            Used SMT solver: z3 (default) or cvc5
+  --solver TEXT            Used SMT solver: z3 (default), cvc5, or bitwuzla
+
   --num-solvers NATURAL    Number of solver instances to use (default: number of cpu cores)
   --smtdebug               Print smt queries sent to the solver
   --ffi                    Allow the usage of the hevm.ffi() cheatcode (WARNING:

diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -5,6 +5,7 @@
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
     foundry.url = "github:shazow/foundry.nix/monthly";
+    bitwuzla-pkgs.url = "github:d-xo/nixpkgs/6e7c9e4267f3c2df116bf76d8e31c2602e2d543d";
     flake-compat = {
       url = "github:edolstra/flake-compat";
       flake = false;
@@ -27,16 +28,18 @@
     };
   };
 
-  outputs = { self, nixpkgs, flake-utils, solidity, forge-std, ethereum-tests, foundry, cabal-head, ... }:
+  outputs = { self, nixpkgs, flake-utils, solidity, forge-std, ethereum-tests, foundry, cabal-head, bitwuzla-pkgs, ... }:
     flake-utils.lib.eachDefaultSystem (system:
       let
         pkgs = (import nixpkgs { inherit system; config = { allowBroken = true; }; });
+        bitwuzla = (import bitwuzla-pkgs { inherit system; }).bitwuzla;
         testDeps = with pkgs; [
           go-ethereum
           solc
           z3
           cvc5
           git
+          bitwuzla
         ] ++ lib.optional (!(pkgs.stdenv.isDarwin && pkgs.stdenv.isAarch64)) [
           foundry.defaultPackage.${system}
         ];
@@ -126,7 +129,7 @@
           buildInputs = [ makeWrapper ];
           postBuild = ''
             wrapProgram $out/bin/hevm \
-              --prefix PATH : "${lib.makeBinPath ([ bash coreutils git solc z3 cvc5 ])}"
+              --prefix PATH : "${lib.makeBinPath ([ bash coreutils git solc z3 cvc5 bitwuzla ])}"
           '';
         };
 

diff --git a/hevm.cabal b/hevm.cabal
@@ -59,6 +59,8 @@ common shared
     -Wno-orphans
     -Wno-ambiguous-fields
     -optc-Wno-ignored-attributes
+    -fspecialize-aggressively
+    -fexpose-all-unfoldings
   default-language: GHC2021
   default-extensions:
     DuplicateRecordFields