Merge branch 'main' into better-debug

.github/scripts/install-libsecp256k1.sh

@@ -3,7 +3,7 @@ set -eux -o pipefail
 
 ## The following script builds and installs libsecp256k1 to ~/.local/lib
 
-INSTALL_VERSION=0.5.0
+INSTALL_VERSION=0.5.1
 
 if [[ "$(uname -s)" =~ ^MSYS_NT.* ]]; then
     echo "This script is only meant to run on Windows under MSYS2"

.github/workflows/bitwuzla-windows.yml

@@ -2,7 +2,7 @@ on:
   workflow_call:
 
 env:
-    BITWUZLA_VERSION: 0.5.0
+    BITWUZLA_VERSION: 0.6.1
 
 jobs:
   build:

.github/workflows/build.yml

@@ -109,7 +109,7 @@ jobs:
             openssl:p
             z3:p
             go:p
-      - uses: haskell-actions/[email protected].0
+      - uses: haskell-actions/[email protected].7
         id: setup
         with:
           ghc-version: '9.6.5'

doc/src/exec.md

@@ -1,6 +1,6 @@
 # `hevm exec`
 
-Run an EVM computation using specified parameters, using an interactive debugger when `--debug` flag is given.
+Run an EVM computation using specified parameters.
 
 ```
 Usage: hevm exec [--code TEXT] [--calldata TEXT] [--address ADDR]
@@ -38,7 +38,8 @@ Available options:
   --rpc TEXT               Fetch state from a remote node
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
-  --project-type PROJECTTYPE Foundry or CombinedJSON project
+  --project-type PROJ      Foundry or CombinedJSON project (default: Foundry)
+  --assertion-type ASSERT  Assertions as per Forge or DSTest (default: Forge)
 ```
 
 Minimum required flags: either you must provide `--code` or you must both pass

hevm.cabal

@@ -146,11 +146,11 @@ library
     containers                        >= 0.6.0 && < 0.7,
     transformers                      >= 0.5 && < 0.7,
     tree-view                         >= 0.5 && < 0.6,
-    aeson                             >= 2.0.0 && < 2.2,
-    bytestring                        >= 0.11.3.1 && < 0.12,
+    aeson                             >= 2.0.0 && < 2.3,
+    bytestring                        >= 0.11.3.1 && < 0.13,
     scientific                        >= 0.3.6 && < 0.4,
     binary                            >= 0.8.6 && < 0.9,
-    text                              >= 1.2.3 && < 2.1,
+    text                              >= 1.2.3 && < 2.2,
     unordered-containers              >= 0.2.10 && < 0.3,
     vector                            >= 0.12.1 && < 0.14,
     base16                            >= 1.0 && < 1.1,
@@ -231,12 +231,10 @@ common test-base
     base,
     containers,
     directory,
-    extra,
     bytestring,
     filemanip,
     filepath,
     hevm,
-    here,
     mtl,
     process,
     tasty,
@@ -284,6 +282,8 @@ test-suite test
     base16,
     binary,
     data-dword,
+    extra,
+    here,
     time,
     regex
 

src/EVM.hs

@@ -950,6 +950,8 @@ exec1 = do
                   case gasTryFrom xGas of
                     Left _ -> vmError IllegalOverflow
                     Right gas ->
+                      -- NOTE: we don't update overrideCaller in this case because
+                      -- forge-std doesn't. see: https://github.com/foundry-rs/foundry/pull/8863
                       delegateCall this gas xTo' self (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $
                         \_ -> touchAccount self
             _ -> underrun

src/EVM/Expr.hs

@@ -352,7 +352,7 @@ copySlice s@(Lit srcOffset) d@(Lit dstOffset) sz@(Lit size) src ds@(ConcreteBuf
     hd = padRight (unsafeInto dstOffset) $ BS.take (unsafeInto dstOffset) dst
     sl = [readByte (Lit i) src | i <- [srcOffset .. srcOffset + (size - 1)]]
     tl = BS.drop (unsafeInto dstOffset + unsafeInto size) dst
-    in if Prelude.and . (fmap isLitByte) $ sl
+    in if all isLitByte sl
        then ConcreteBuf $ hd <> (BS.pack . (mapMaybe maybeLitByteSimp) $ sl) <> tl
        else CopySlice s d sz src ds
   | otherwise = CopySlice s d sz src ds
@@ -530,7 +530,7 @@ toList buf = case bufLength buf of
   _ -> Nothing
 
 fromList :: V.Vector (Expr Byte) -> Expr Buf
-fromList bs = case Prelude.and (fmap isLitByte bs) of
+fromList bs = case all isLitByte bs of
   True -> ConcreteBuf . BS.pack . V.toList . V.mapMaybe maybeLitByteSimp $ bs
   -- we want to minimize the size of the resulting expression, so we do two passes:
   --   1. write all concrete bytes to some base buffer
@@ -1482,7 +1482,7 @@ padBytesLeft n bs
 
 joinBytes :: [Expr Byte] -> Expr EWord
 joinBytes bs
-  | Prelude.and . (fmap isLitByte) $ bs = Lit . bytesToW256 . (mapMaybe maybeLitByteSimp) $ bs
+  | all isLitByte bs = Lit . bytesToW256 . (mapMaybe maybeLitByteSimp) $ bs
   | otherwise = let
       bytes = padBytesLeft 32 bs
     in JoinBytes
@@ -1512,7 +1512,7 @@ numBranches (ITE _ t f) = numBranches t + numBranches f
 numBranches _ = 1
 
 allLit :: [Expr Byte] -> Bool
-allLit = Data.List.and . fmap (isLitByte)
+allLit = all isLitByte
 
 -- | True if the given expression contains any node that satisfies the
 -- input predicate

src/EVM/Format.hs

@@ -38,7 +38,7 @@ import EVM (traceForest, traceForest', traceContext, cheatCode)
 import EVM.ABI (getAbiSeq, parseTypeName, AbiValue(..), AbiType(..), SolError(..), Indexed(..), Event(..))
 import EVM.Dapp (DappContext(..), DappInfo(..), findSrc, showTraceLocation)
 import EVM.Expr qualified as Expr
-import EVM.Solidity (SolcContract(..), Method(..), contractName, abiMap)
+import EVM.Solidity (SolcContract(..), Method(..))
 import EVM.Types
 import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
 
@@ -57,7 +57,7 @@ import Data.DoubleWord (signedWord)
 import Data.Foldable (toList)
 import Data.List (isPrefixOf, sort)
 import Data.Map qualified as Map
-import Data.Maybe (catMaybes, fromMaybe)
+import Data.Maybe (catMaybes, fromMaybe, listToMaybe)
 import Data.Text (Text, pack, unpack, intercalate, dropEnd, splitOn)
 import Data.Text qualified as T
 import Data.Text.Encoding qualified as T
@@ -122,14 +122,21 @@ textValues ts (ConcreteBuf bs) =
     Left (_, _, _)   -> [formatBinary bs]
 textValues ts _ = fmap (const "<symbolic>") ts
 
+textValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text
+textValue ts (ConcreteBuf bs) =
+  case runGetOrFail (getAbiSeq 1 [ts]) (fromStrict bs) of
+    Right (_, _, xs) -> fromMaybe (internalError "impossible empty list") $ listToMaybe $ textAbiValues xs
+    Left (_, _, _)   -> formatBinary bs
+textValue _ _ = "<symbolic>"
+
 parenthesise :: [Text] -> Text
 parenthesise ts = "(" <> intercalate ", " ts <> ")"
 
 showValues :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
 showValues ts b = parenthesise $ textValues ts b
 
 showValue :: (?context :: DappContext) => AbiType -> Expr Buf -> Text
-showValue t b = head $ textValues [t] b
+showValue t b = textValue t b
 
 showCall :: (?context :: DappContext) => [AbiType] -> Expr Buf -> Text
 showCall ts (ConcreteBuf bs) = showValues ts $ ConcreteBuf (BS.drop 4 bs)
@@ -276,7 +283,7 @@ showTrace trace =
             showTopic :: AbiType -> Expr EWord -> Text
             showTopic abiType topic =
               case maybeLitWordSimp (Expr.concKeccakSimpExpr topic) of
-                Just w -> head $ textValues [abiType] (ConcreteBuf (word256Bytes w))
+                Just w -> textValue abiType (ConcreteBuf (word256Bytes w))
                 _ -> "<symbolic>"
 
           withName :: Text -> Text -> Text

src/EVM/SMT.hs

@@ -16,8 +16,9 @@ import Data.List qualified as List
 import Data.List.NonEmpty (NonEmpty((:|)))
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.String.Here
-import Data.Maybe (fromJust, fromMaybe, isJust)
+import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)
 import Data.Either.Extra (fromRight')
+import Data.Foldable (fold)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
 import Data.Set (Set)
@@ -164,7 +165,7 @@ declareIntermediates bufs stores = do
       sorted = List.sortBy compareFst $ Map.toList $ encSs <> encBs
   decls <- mapM snd sorted
   let smt2 = (SMT2 [fromText "; intermediate buffers & stores"] mempty mempty):decls
-  pure $ foldr (<>) mempty smt2
+  pure $ fold smt2
   where
     compareFst (l, _) (r, _) = compare l r
     encodeBuf n expr = do
@@ -929,9 +930,11 @@ expandExp base expnt
 -- | Concatenates a list of bytes into a larger bitvector
 concatBytes :: [Expr Byte] -> Err Builder
 concatBytes bytes = do
-  let bytesRev = reverse bytes
-  a2 <- exprToSMT (head bytesRev)
-  foldM wrap a2 $ tail bytesRev
+  case List.uncons $ reverse bytes of
+    Nothing -> Left "unexpected empty bytes"
+    Just (h, t) -> do
+      a2 <- exprToSMT h
+      foldM wrap a2 t
   where
     wrap :: Builder -> Expr a -> Err Builder
     wrap inner byte = do
@@ -990,9 +993,14 @@ parseInteger = parseSC
 parseW8 :: SpecConstant -> Word8
 parseW8 = parseSC
 
+readOrError :: (Num a, Eq a) => ReadS a -> TS.Text -> a
+readOrError reader val = fst . headErr . reader . T.unpack . T.fromStrict $ val
+  where
+    headErr x = fromMaybe (internalError "error reading empty result") $ listToMaybe x
+
 parseSC :: (Num a, Eq a) => SpecConstant -> a
-parseSC (SCHexadecimal a) = fst . head . Numeric.readHex . T.unpack . T.fromStrict $ a
-parseSC (SCBinary a) = fst . head . Numeric.readBin . T.unpack . T.fromStrict $ a
+parseSC (SCHexadecimal a) = readOrError Numeric.readHex a
+parseSC (SCBinary a) = readOrError Numeric.readBin a
 parseSC sc = internalError $ "cannot parse: " <> show sc
 
 parseErr :: (Show a) => a -> b

src/EVM/SymExec.hs

@@ -15,8 +15,9 @@ import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.Containers.ListUtils (nubOrd)
 import Data.DoubleWord (Word256)
-import Data.List (foldl', sortBy, sort, group)
-import Data.Maybe (fromMaybe, mapMaybe)
+import Data.List (foldl', sortBy, sort)
+import Data.List.NonEmpty qualified as NE
+import Data.Maybe (fromMaybe, mapMaybe, listToMaybe)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
 import Data.Map.Merge.Strict qualified as Map
@@ -79,14 +80,14 @@ isQed (Qed _) = True
 isQed _ = False
 
 groupIssues :: [ProofResult a b c String] -> [(Integer, String)]
-groupIssues results = map (\g -> (into (length g), head g)) grouped
+groupIssues results = map (\g -> (into (length g), NE.head g)) grouped
   where
     getErr :: ProofResult a b c String -> String
     getErr (EVM.SymExec.Error k) = k
     getErr (EVM.SymExec.Unknown _) = "SMT result timeout/unknown"
     getErr _ = internalError "shouldn't happen"
     sorted = sort $ map getErr results
-    grouped = group sorted
+    grouped = NE.group sorted
 
 data VeriOpts = VeriOpts
   { simp :: Bool
@@ -953,7 +954,7 @@ formatCex cd sig m@(SMTCex _ addrs _ store blockContext txContext) = T.unlines $
     prettyBuf b = internalError $ "Unexpected symbolic buffer:\n" <> T.unpack (formatExpr b)
 
 prettyCalldata :: SMTCex -> Expr Buf -> Text -> [AbiType] -> Text
-prettyCalldata cex buf sig types = head (T.splitOn "(" sig) <> "(" <> body <> ")"
+prettyCalldata cex buf sig types = headErr errSig (T.splitOn "(" sig) <> "(" <> body <> ")"
   where
     argdata = Expr.drop 4 . Expr.simplify . defaultSymbolicValues $ subModel cex buf
     body = case decodeBuf types argdata of
@@ -962,7 +963,9 @@ prettyCalldata cex buf sig types = head (T.splitOn "(" sig) <> "(" <> body <> ")
           ConcreteBuf c -> T.pack (bsToHex c)
           _ -> err
       SAbi _ -> err
+    headErr e l = fromMaybe e $ listToMaybe l 
     err = internalError $ "unable to produce a concrete model for calldata: " <> show buf
+    errSig = internalError $ "unable to split sig: " <> show sig
 
 -- | If the expression contains any symbolic values, default them to some
 -- concrete value The intuition here is that if we still have symbolic values

src/EVM/UnitTest.hs

@@ -375,10 +375,11 @@ formatTestLog events (LogEntry _ args (topic:_)) =
         _ -> Nothing
 
         where
+          headErr l = fromMaybe (internalError "shouldn't happen") $ listToMaybe l
           argTypes = [argType | (_, argType, NotIndexed) <- argInfos]
           unquote = Text.dropAround (\c -> c == '"' || c == '«' || c == '»')
           log_unnamed =
-            Just $ showValue (head argTypes) args
+            Just $ showValue (headErr argTypes) args
           log_named =
             let (key, val) = case take 2 (textValues argTypes args) of
                   [k, v] -> (k, v)