Merge branch 'main' into overapproximate-staticcall

.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'

CHANGELOG.md

@@ -9,6 +9,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - When a staticcall is made to a contract that does not exist, we overapproxiate
   and return symbolic values
 
+## Fixed
+- We now try to simplify expressions fully before trying to cast them to a concrete value
+  This should improve issues when "Unexpected Symbolic Arguments to Opcode" was
+  unnecessarily output
+
+
 ## [0.54.2] - 2024-12-12
 
 ## Fixed

cli/cli.hs

@@ -46,6 +46,7 @@ import EVM.Types hiding (word, Env, Symbolic)
 import EVM.Types qualified
 import EVM.UnitTest
 import EVM.Effects
+import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
 
 data AssertionType = DSTest | Forge
   deriving (Eq, Show, Read, ParseField)
@@ -489,7 +490,7 @@ vmFromCommand cmd = do
       putStrLn "Error, must provide at least (rpc + address) or code"
       exitFailure
 
-  let ts' = case maybeLitWord ts of
+  let ts' = case maybeLitWordSimp ts of
         Just t -> t
         Nothing -> internalError "unexpected symbolic timestamp when executing vm test"
 
@@ -511,7 +512,7 @@ vmFromCommand cmd = do
                     then InitCode bs mempty
                     else RuntimeCode (ConcreteRuntimeCode bs)
         address = if cmd.create
-                  then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddr origin) (W64 $ word64 (.nonce) 0))
+                  then addr (.address) (Concrete.createAddress (fromJust $ maybeLitAddrSimp origin) (W64 $ word64 (.nonce) 0))
                   else addr (.address) (LitAddr 0xacab)
 
         vm0 baseFee miner ts blockNum prevRan c = makeVm $ VMOpts

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

@@ -24,6 +24,7 @@ import EVM.Types qualified as Expr (Expr(Gas))
 import EVM.Sign qualified
 import EVM.Concrete qualified as Concrete
 import EVM.CheatsTH
+import EVM.Expr (maybeLitByteSimp, maybeLitWordSimp, maybeLitAddrSimp)
 
 import Control.Monad (unless, when)
 import Control.Monad.ST (ST)
@@ -282,7 +283,7 @@ getOpW8 state = case state.code of
       RuntimeCode (ConcreteRuntimeCode bs) -> BS.index bs state.pc
       RuntimeCode (SymbolicRuntimeCode ops) ->
         fromMaybe (internalError "could not analyze symbolic code") $
-          maybeLitByte $ ops V.! state.pc
+          maybeLitByteSimp $ ops V.! state.pc
 
 getOpName :: forall (t :: VMType) s . FrameState t s -> [Char]
 getOpName state = intToOpName $ fromEnum $ getOpW8 state
@@ -305,12 +306,9 @@ exec1 = do
     stk  = vm.state.stack
     self = vm.state.contract
     this = fromMaybe (internalError "state contract") (Map.lookup self vm.env.contracts)
-
     fees@FeeSchedule {..} = vm.block.schedule
-
     doStop = finishFrame (FrameReturned mempty)
-
-    litSelf = maybeLitAddr self
+    litSelf = maybeLitAddrSimp self
 
   if isJust litSelf && (fromJust litSelf) > 0x0 && (fromJust litSelf) <= 0xa then do
     -- call to precompile
@@ -750,7 +748,7 @@ exec1 = do
                         Lit v -> v
                         _ -> 0
                     storage_cost =
-                      case (maybeLitWord current, maybeLitWord new) of
+                      case (maybeLitWordSimp current, maybeLitWordSimp new) of
                         (Just current', Just new') ->
                            if (current' == new') then g_sload
                            else if (current' == original) && (original == 0) then g_sset
@@ -768,7 +766,7 @@ exec1 = do
                     assign (#state % #stack) xs
                     modifying (#env % #contracts % ix self % #storage) (writeStorage x new)
 
-                    case (maybeLitWord current, maybeLitWord new) of
+                    case (maybeLitWordSimp current, maybeLitWordSimp new) of
                        (Just current', Just new') ->
                           unless (current' == new') $
                             if current' == original then
@@ -923,7 +921,7 @@ exec1 = do
                 output <- readMemory xOffset xSize
                 let
                   codesize = fromMaybe (internalError "processing opcode RETURN. Cannot return dynamically sized abstract data")
-                               . maybeLitWord . bufLength $ output
+                               . maybeLitWordSimp . bufLength $ output
                   maxsize = vm.block.maxCodeSize
                   creation = case vm.frames of
                     [] -> vm.tx.isCreate
@@ -961,6 +959,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
@@ -1195,7 +1195,7 @@ precompiledContract this xGas precompileAddr recipient xValue inOffset inSize ou
       vm <- get
       case result' of
         Nothing -> case stk of
-          x:_ -> case maybeLitWord x of
+          x:_ -> case maybeLitWordSimp x of
             Just 0 ->
               pure ()
             Just 1 ->
@@ -1610,28 +1610,28 @@ forceAddr n msg continue = case wordToAddr n of
   Just c -> continue c
 
 forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
-forceConcrete n msg continue = case maybeLitWord n of
+forceConcrete n msg continue = case maybeLitWordSimp n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])
   Just c -> continue c
 
 forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()
-forceConcreteAddr n msg continue = case maybeLitAddr n of
+forceConcreteAddr n msg continue = case maybeLitAddrSimp n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n])
   Just c -> continue c
 
 forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()
-forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of
+forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddrSimp n, maybeLitAddrSimp m) of
   (Just c, Just d) -> continue (c,d)
   _ -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) msg (wrap [n, m])
 
 forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()
-forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of
+forceConcrete2 (n,m) msg continue = case (maybeLitWordSimp n, maybeLitWordSimp m) of
   (Just c, Just d) -> continue (c, d)
   _ -> do
     vm <- get
@@ -1683,7 +1683,7 @@ accessAccountForGas addr = do
 accessStorageForGas :: Expr EAddr -> Expr EWord -> EVM t s Bool
 accessStorageForGas addr key = do
   accessedStrkeys <- use (#tx % #subState % #accessedStorageKeys)
-  case maybeLitWord key of
+  case maybeLitWordSimp key of
     Just litword -> do
       let accessed = member (addr, litword) accessedStrkeys
       assign (#tx % #subState % #accessedStorageKeys) (insert (addr, litword) accessedStrkeys)
@@ -1708,7 +1708,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
   input <- readMemory (Expr.add inOffset (Lit 4)) (Expr.sub inSize (Lit 4))
   calldata <- readMemory inOffset inSize
   abi <- readBytes 4 (Lit 0) <$> readMemory inOffset (Lit 4)
-  let newContext = CallContext cheatCode cheatCode outOffset outSize (Lit 0) (maybeLitWord abi) calldata vm.env.contracts vm.tx.subState
+  let newContext = CallContext cheatCode cheatCode outOffset outSize (Lit 0) (maybeLitWordSimp abi) calldata vm.env.contracts vm.tx.subState
 
   pushTrace $ FrameTrace newContext
   next
@@ -1717,7 +1717,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
                     { state = vm1.state { stack = xs }
                     , context = newContext
                     }
-  case maybeLitWord abi of
+  case maybeLitWordSimp abi of
     Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi])
     Just (unsafeInto -> abi') ->
       case Map.lookup abi' cheatActions of
@@ -2073,7 +2073,7 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut
               _ -> do
                 burn' xGas $ do
                   calldata <- readMemory xInOffset xInSize
-                  abi <- maybeLitWord . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)
+                  abi <- maybeLitWordSimp . readBytes 4 (Lit 0) <$> readMemory xInOffset (Lit 4)
                   let newContext = CallContext
                                     { target    = xTo
                                     , context   = xContext
@@ -2670,7 +2670,7 @@ isValidJumpDest vm x = let
       UnknownCode _ -> internalError "Cannot analyze jumpdests for unknown code"
       InitCode ops _ -> BS.indexMaybe ops x
       RuntimeCode (ConcreteRuntimeCode ops) -> BS.indexMaybe ops x
-      RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByte
+      RuntimeCode (SymbolicRuntimeCode ops) -> ops V.!? x >>= maybeLitByteSimp
   in case op of
        Nothing -> False
        Just b -> 0x5b == b && OpJumpdest == snd (contract.codeOps V.! (contract.opIxMap SV.! x))
@@ -2709,7 +2709,7 @@ mkOpIxMap (RuntimeCode (SymbolicRuntimeCode ops))
       let (_, _, _, m) = foldl (go v) (0, 0, 0, pure ()) (stripBytecodeMetadataSym $ V.toList ops)
       in m >> pure v
       where
-        go v (0, !i, !j, !m) x = case maybeLitByte x of
+        go v (0, !i, !j, !m) x = case maybeLitByteSimp x of
           Just x' -> if x' >= 0x60 && x' <= 0x7f
             -- start of PUSH op --
                      then (x' - 0x60 + 1, i + 1, j,     m >> SV.write v i j)
@@ -2734,7 +2734,7 @@ vmOp vm =
         RuntimeCode (ConcreteRuntimeCode xs') ->
           (BS.index xs' i, fmap LitByte $ BS.unpack $ BS.drop i xs')
         RuntimeCode (SymbolicRuntimeCode xs') ->
-          ( fromMaybe (internalError "unexpected symbolic code") . maybeLitByte $ xs' V.! i , V.toList $ V.drop i xs')
+          ( fromMaybe (internalError "unexpected symbolic code") . maybeLitByteSimp $ xs' V.! i , V.toList $ V.drop i xs')
   in if (opslen code' < i)
      then Nothing
      else Just (readOp op pushdata)
@@ -2762,7 +2762,7 @@ mkCodeOps contractCode =
         Nothing ->
           mempty
         Just (x, xs') ->
-          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByte x
+          let x' = fromMaybe (internalError "unexpected symbolic code argument") $ maybeLitByteSimp x
               j = opSize x'
           in (i, readOp x' xs') Seq.<| go (i + j) (drop j xs)
 

src/EVM/ABI.hs

@@ -60,6 +60,7 @@ module EVM.ABI
 
 import EVM.Expr (readWord, isLitWord)
 import EVM.Types
+import EVM.Expr (maybeLitWordSimp)
 
 import Control.Applicative ((<|>))
 import Control.Monad (replicateM, replicateM_, forM_, void)
@@ -511,7 +512,7 @@ decodeBuf tps buf =
   else
     let
       vs = decodeStaticArgs 0 (length tps) buf
-      asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs)
+      asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWordSimp vs)
     in if not (all isLitWord vs)
        then SAbi vs
        else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of

src/EVM/Dapp.hs

@@ -4,6 +4,7 @@ import EVM.ABI
 import EVM.Concrete
 import EVM.Solidity
 import EVM.Types
+import EVM.Expr (maybeLitByteSimp, maybeLitWordSimp)
 
 import Control.Arrow ((>>>), second)
 import Data.Aeson (Value)
@@ -138,7 +139,7 @@ srcMap dapp contr opIndex = do
 
 findSrc :: Contract -> DappInfo -> Maybe SolcContract
 findSrc c dapp = do
-  hash <- maybeLitWord c.codehash
+  hash <- maybeLitWordSimp c.codehash
   case Map.lookup hash dapp.solcByHash of
     Just (_, v) -> Just v
     Nothing -> lookupCode c.code dapp
@@ -153,7 +154,7 @@ lookupCode (RuntimeCode (ConcreteRuntimeCode c)) a =
     Just x -> pure x
     Nothing -> snd <$> find (compareCode c . fst) a.solcByCode
 lookupCode (RuntimeCode (SymbolicRuntimeCode c)) a = let
-    code = BS.pack $ mapMaybe maybeLitByte $ V.toList c
+    code = BS.pack $ mapMaybe maybeLitByteSimp $ V.toList c
   in case snd <$> Map.lookup (keccak' (stripBytecodeMetadata code)) a.solcByHash of
     Just x -> pure x
     Nothing -> snd <$> find (compareCode code . fst) a.solcByCode