Merge pull request #50 from ethereum/fix-cvc5-good

Author: d-xo

README.md

@@ -104,7 +104,7 @@ Available options:
                            60000)
   --max-iterations INTEGER Number of times we may revisit a particular branching
                            point
-  --solver TEXT            Used SMT solver: z3 (default) or cvc4
+  --solver TEXT            Used SMT solver: z3 (default) or cvc5
   --smtdebug               Print smt queries sent to the solver
   --assertions [WORD256]   Comma seperated list of solc panic codes to check for
                            (default: everything except arithmetic overflow)

flake.nix

@@ -25,7 +25,7 @@
             inherit secp256k1;
           })
           [
-            (haskell.lib.compose.addTestToolDepends [ solc z3 cvc4 ])
+            (haskell.lib.compose.addTestToolDepends [ solc z3 cvc5 ])
             (haskell.lib.compose.appendConfigureFlags (
               [ "--ghc-option=-O2" ]
               ++ lib.optionals stdenv.isLinux [
@@ -75,7 +75,7 @@
             packages = _: [ hevm ];
             buildInputs = [
               z3
-              cvc4
+              cvc5
               solc
               haskellPackages.cabal-install
               haskellPackages.haskell-language-server

nix/hevm-tests/default.nix

@@ -11,9 +11,9 @@ let
 in
   pkgs.recurseIntoAttrs {
     yulEquivalence-z3 = runWithSolver ./yul-equivalence.nix "z3";
-    yulEquivalence-cvc4 = runWithSolver ./yul-equivalence.nix "cvc4";
+    yulEquivalence-cvc5 = runWithSolver ./yul-equivalence.nix "cvc5";
 
     # z3 takes 3hrs to run these tests on a fast machine, and even then ~180 timeout
     #smtChecker-z3 = runWithSolver ./smt-checker.nix "z3";
-    smtChecker-cvc4 = runWithSolver ./smt-checker.nix "cvc4";
+    smtChecker-cvc5 = runWithSolver ./smt-checker.nix "cvc5";
   }

src/hevm/hevm-cli/hevm-cli.hs

@@ -121,7 +121,7 @@ data Command w
       , showTree      :: w ::: Bool               <?> "Print branches explored in tree view"
       , smttimeout    :: w ::: Maybe Integer      <?> "Timeout given to SMT solver in milliseconds (default: 60000)"
       , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"
-      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc4"
+      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc5"
       , smtdebug      :: w ::: Bool               <?> "Print smt queries sent to the solver"
       , assertions    :: w ::: Maybe [Word256]    <?> "Comma seperated list of solc panic codes to check for (default: everything except arithmetic overflow)"
       , askSmtIterations :: w ::: Maybe Integer   <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"
@@ -132,7 +132,7 @@ data Command w
       , sig           :: w ::: Maybe Text       <?> "Signature of types to decode / encode"
       , smttimeout    :: w ::: Maybe Integer    <?> "Timeout given to SMT solver in milliseconds (default: 60000)"
       , maxIterations :: w ::: Maybe Integer    <?> "Number of times we may revisit a particular branching point"
-      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc4"
+      , solver        :: w ::: Maybe Text       <?> "Used SMT solver: z3 (default) or cvc5"
       , smtoutput     :: w ::: Bool             <?> "Print verbose smt output"
       , smtdebug      :: w ::: Bool             <?> "Print smt queries sent to the solver"
       , askSmtIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 5)"
@@ -182,7 +182,7 @@ data Command w
       , cache         :: w ::: Maybe String             <?> "Path to rpc cache repository"
       , match         :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"
       , covMatch      :: w ::: Maybe String             <?> "Coverage filter - only print coverage for files matching regex"
-      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc4"
+      , solver        :: w ::: Maybe Text               <?> "Used SMT solver: z3 (default) or cvc5"
       , smtdebug      :: w ::: Bool                     <?> "Print smt queries sent to the solver"
       , ffi           :: w ::: Bool                     <?> "Allow the usage of the hevm.ffi() cheatcode (WARNING: this allows test authors to execute arbitrary code on your machine)"
       , smttimeout    :: w ::: Maybe Integer            <?> "Timeout given to SMT solver in milliseconds (default: 60000)"
@@ -439,7 +439,7 @@ getSrcInfo cmd =
 
 -- Although it is tempting to fully abstract calldata and give any hints about
 -- the nature of the signature doing so results in significant time spent in
--- consulting z3 about rather trivial matters. But with cvc4 it is quite
+-- consulting z3 about rather trivial matters. But with cvc5 it is quite
 -- pleasant!
 
 -- If function signatures are known, they should always be given for best results.

src/hevm/src/EVM/SMT.hs

@@ -242,11 +242,9 @@ prelude = SMT2 . fmap (T.drop 2) . T.lines $ [i|
   (declare-const abstractStore Storage)
   (define-const emptyStore Storage ((as const Storage) ((as const (Array (_ BitVec 256) (_ BitVec 256))) #x0000000000000000000000000000000000000000000000000000000000000000)))
 
-  (define-fun sstore ((addr Word) (key Word) (val Word) (storage Storage)) Storage (
-      store storage addr (store (select storage addr) key val)))
+  (define-fun sstore ((addr Word) (key Word) (val Word) (storage Storage)) Storage (store storage addr (store (select storage addr) key val)))
 
-  (define-fun sload ((addr Word) (key Word) (storage Storage)) Word (
-      select (select storage addr) key))
+  (define-fun sload ((addr Word) (key Word) (storage Storage)) Word (select (select storage addr) key))
   |]
 
 declareBufs :: [Text] -> SMT2
@@ -704,8 +702,7 @@ solverArgs = \case
     [ "-in" ]
   CVC5 ->
     [ "--lang=smt"
-    , "--interactive"
-    , "--no-interactive-prompt"
+    , "--no-interactive"
     , "--produce-models"
     ]
   Custom _ -> []