Temporary

cli/cli.hs

@@ -77,7 +77,7 @@ data Command w
 
   -- symbolic execution opts
       , root          :: w ::: Maybe String       <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a Foundry or DappTools project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType  <?> "Is this a CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
       , initialStorage :: w ::: Maybe (InitialStorage) <?> "Starting state for storage: Empty, Abstract (default Abstract)"
       , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"
       , arg           :: w ::: [String]           <?> "Values to encode"
@@ -147,11 +147,11 @@ data Command w
       , rpc         :: w ::: Maybe URL         <?> "Fetch state from a remote node"
       , block       :: w ::: Maybe W256        <?> "Block state is be fetched from"
       , root        :: w ::: Maybe String      <?> "Path to  project root directory (default: . )"
-      , projectType :: w ::: Maybe ProjectType <?> "Is this a Foundry or DappTools project (default: Foundry)"
+      , projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
       }
-  | Test -- Run DSTest unit tests
+  | Test -- Run Foundry unit tests
       { root        :: w ::: Maybe String               <?> "Path to  project root directory (default: . )"
-      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a Foundry or DappTools project (default: Foundry)"
+      , projectType   :: w ::: Maybe ProjectType        <?> "Is this a CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
       , rpc           :: w ::: Maybe URL                <?> "Fetch state from a remote node"
       , number        :: w ::: Maybe W256               <?> "Block: number"
       , verbose       :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"

doc/src/exec.md

@@ -39,12 +39,10 @@ Available options:
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
   --project-type PROJECTTYPE
-                           Is this a Foundry or DappTools project (default:
-                           Foundry)
 ```
 
 Minimum required flags: either you must provide `--code` or you must both pass
-`--rpc` and `--address`. 
+`--rpc` and `--address`.
 
 If the execution returns an output, it will be written
 to stdout. Exit code indicates whether the execution was successful or

doc/src/symbolic.md

@@ -42,8 +42,6 @@ Available options:
   --block W256             Block state is be fetched from
   --root STRING            Path to project root directory (default: . )
   --project-type PROJECTTYPE
-                           Is this a Foundry or DappTools project (default:
-                           Foundry)
   --initial-storage INITIALSTORAGE
                            Starting state for storage: Empty, Abstract (default
                            Abstract)

doc/src/test.md

@@ -14,8 +14,6 @@ Available options:
   -h,--help                Show this help text
   --root STRING            Path to project root directory (default: . )
   --project-type PROJECTTYPE
-                           Is this a Foundry or DappTools project (default:
-                           Foundry)
   --rpc TEXT               Fetch state from a remote node
   --number W256            Block: number
   --verbose INT            Append call trace: {1} failures {2} all

src/EVM.hs

@@ -1904,48 +1904,59 @@ cheatActions = Map.fromList
   , $(envReadMultipleCheat "envBytes32(string,string)" $ AbiBytesType 32) stringToBytes32
   , $(envReadMultipleCheat "envString(string,string)" AbiStringType) stringToByteString
   , $(envReadMultipleCheat "envBytes(bytes,bytes)" AbiBytesDynamicType) stringHexToByteString
-  , action "asserTrue(bool)" $ \sig input ->
+  , action "assertTrue(bool)" $ \sig input ->
       case decodeBuf [AbiBoolType] input of
         CAbi [AbiBool True] -> doStop
         CAbi [AbiBool False] -> frameRevert "assertion failed"
-        _ -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed") sig
-  , action "asserFalse(bool)" $ \sig input ->
+        SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
+          Lit 1 -> frameRevert "assertion failed"
+          Lit 0 -> doStop
+          ew -> branch (Expr.iszero ew) $ \case
+            True -> frameRevert "assertion failed"
+            False -> doStop
+        k -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed: " <> show k) sig
+  , action "assertFalse(bool)" $ \sig input ->
       case decodeBuf [AbiBoolType] input of
         CAbi [AbiBool False] -> doStop
         CAbi [AbiBool True] -> frameRevert "assertion failed"
-        _ -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed") sig
+        SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
+          Lit 0 -> frameRevert "assertion failed"
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False -> frameRevert "assertion failed"
+            True -> doStop
+        k -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed: " <> show k) sig
   , action "assertEq(bool,bool)"       $ assertEq AbiBoolType
   , action "assertEq(uint256,uint256)" $ assertEq (AbiUIntType 256)
   , action "assertEq(int256,int256)"   $ assertEq (AbiIntType 256)
   , action "assertEq(address,address)" $ assertEq AbiAddressType
   , action "assertEq(bytes32,bytes32)" $ assertEq (AbiBytesType 32)
   , action "assertEq(string,string)"   $ assertEq AbiStringType
+  , action "assertEq(bytes,bytes)"     $ assertEq AbiBytesDynamicType
   --
-  , action "assertNotEq(bytes,bytes)"     $ assertNotEq (AbiBytesDynamicType)
   , action "assertNotEq(bool,bool)"       $ assertNotEq AbiBoolType
   , action "assertNotEq(uint256,uint256)" $ assertNotEq (AbiUIntType 256)
   , action "assertNotEq(int256,int256)"   $ assertNotEq (AbiIntType 256)
   , action "assertNotEq(address,address)" $ assertNotEq AbiAddressType
   , action "assertNotEq(bytes32,bytes32)" $ assertNotEq (AbiBytesType 32)
   , action "assertNotEq(string,string)"   $ assertNotEq AbiStringType
-  , action "assertNotEq(bytes,bytes)"     $ assertNotEq (AbiBytesDynamicType)
+  , action "assertNotEq(bytes,bytes)"     $ assertNotEq AbiBytesDynamicType
   --
-  , action "assertNotEqMsg(bytes,bytes)"     $ assertNotEqMsg (AbiBytesDynamicType)
   , action "assertNotEqMsg(bool,bool)"       $ assertNotEqMsg AbiBoolType
   , action "assertNotEqMsg(uint256,uint256)" $ assertNotEqMsg (AbiUIntType 256)
   , action "assertNotEqMsg(int256,int256)"   $ assertNotEqMsg (AbiIntType 256)
   , action "assertNotEqMsg(address,address)" $ assertNotEqMsg AbiAddressType
   , action "assertNotEqMsg(bytes32,bytes32)" $ assertNotEqMsg (AbiBytesType 32)
   , action "assertNotEqMsg(string,string)"   $ assertNotEqMsg AbiStringType
-  , action "assertNotEqMsg(bytes,bytes)"     $ assertNotEqMsg (AbiBytesDynamicType)
+  , action "assertNotEqMsg(bytes,bytes)"     $ assertNotEqMsg AbiBytesDynamicType
   --
   , action "assertEq(bool,bool,string)"       $ assertEqMsg AbiBoolType
   , action "assertEq(uint256,uint256,string)" $ assertEqMsg (AbiUIntType 256)
   , action "assertEq(int256,int256,string)"   $ assertEqMsg (AbiIntType 256)
   , action "assertEq(address,address,string)" $ assertEqMsg AbiAddressType
   , action "assertEq(bytes32,bytes32,string)" $ assertEqMsg (AbiBytesType 32)
   , action "assertEq(string,string,string)"   $ assertEqMsg AbiStringType
-  , action "assertEq(bytes,bytes,string)"     $ assertEqMsg (AbiBytesDynamicType)
+  , action "assertEq(bytes,bytes,string)"     $ assertEqMsg AbiBytesDynamicType
   --
   , action "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)
   , action "assertLt(int256,int256)"   $ assertLt (AbiIntType 256)
@@ -1994,10 +2005,10 @@ cheatActions = Map.fromList
     stringToByteString = Right . Char8.pack
     stringHexToByteString :: String -> Either ByteString ByteString
     stringHexToByteString s = either (const $ Left "invalid bytes value") Right $ BS16.decodeBase16Untyped . Char8.pack . strip0x $ s
-    paramDecodeErr abitype name = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
-      ")  parameter decoding failed"
-    paramDecodeMsgErr abitype name = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
-      ",string)  parameter decoding failed"
+    paramDecodeErr abitype name abivals = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
+      ")  parameter decoding failed. Error: " <> show abivals
+    paramDecodeMsgErr abitype name abivals = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
+      ",string)  parameter decoding failed. Error: " <> show abivals
     revertErr a b comp = frameRevert $ "assertion failed: " <>
       BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
     revertMsgErr a b str comp = frameRevert $ "assertion failed: "
@@ -2006,42 +2017,92 @@ cheatActions = Map.fromList
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a == b -> doStop
         CAbi [a, b] -> revertErr a b "!="
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertEq") sig)
-    assertEqMsg abitype sig input =
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.eq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "!="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 "!="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertEq" abivals) sig)
+    --  TODO broken: EWords + AbiString don't mix
+    assertEqMsg abitype sig input = do
       case decodeBuf [abitype, abitype, AbiStringType] input of
         CAbi [a, b, _] | a == b -> doStop
         CAbi [a, b, AbiString str] -> revertMsgErr a b str "!="
-        _ -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertEq") sig)
+        MixAbi ([ew1, ew2], AbiString str) -> case (Expr.simplify (Expr.eq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "!="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertMsgErr ew1 ew2 str "!="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertEq" abivals) sig)
+    --  TODO broken: EWords + AbiString don't mix
     assertNotEq abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a /= b -> doStop
-        CAbi [a, b] -> revertErr a b "=="
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertNotEq") sig)
+        CAbi [a, b] -> revertErr a b "!="
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.iszero $ Expr.eq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "!="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 "!="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertNotEq" abivals) sig)
     assertNotEqMsg abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b, _] | a /= b -> doStop
-        CAbi [a, b, AbiString str] -> revertMsgErr a b str "=="
-        _ -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertNotEq") sig)
-    assertLt abitype sig input =
+        CAbi [a, b, AbiString str] -> revertMsgErr a b str "!="
+        MixAbi ([ew1, ew2], AbiString str) -> case (Expr.simplify (Expr.iszero $ Expr.eq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "!="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertMsgErr ew1 ew2 str "!="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeMsgErr abitype "assertEq" abivals) sig)
+    assertLt abitype sig input = do
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a < b -> doStop
         CAbi [a, b] -> revertErr a b ">="
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertLt") sig)
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.lt ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 ">="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 ">="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLt" abivals) sig)
     assertGt abitype sig input =
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a > b -> doStop
         CAbi [a, b] -> revertErr a b "<="
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertGt") sig)
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.gt ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "<="
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 "<="
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGt" abivals) sig)
     assertLe abitype sig input =
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a <= b -> doStop
-        CAbi [a, b] -> revertErr a b "<"
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertLe") sig)
+        CAbi [a, b] -> revertErr a b ">"
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.leq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 ">"
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 ">"
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLe" abivals) sig)
     assertGe abitype sig input =
       case decodeBuf [abitype, abitype] input of
         CAbi [a, b] | a >= b -> doStop
-        CAbi [a, b] -> revertErr a b ">"
-        _ -> vmError (BadCheatCode (paramDecodeErr abitype "assertGe") sig)
+        CAbi [a, b] -> revertErr a b "<"
+        SAbi [ew1, ew2] -> case (Expr.simplify (Expr.geq ew1 ew2)) of
+          Lit 0 -> revertErr ew1 ew2 "<"
+          Lit 1 -> doStop
+          ew -> branch (ew) $ \case
+            False ->revertErr ew1 ew2 "<"
+            True -> doStop
+        abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGe" abivals) sig)
 
 
 -- * General call implementation ("delegateCall")

src/EVM/ABI.hs

@@ -58,7 +58,7 @@ module EVM.ABI
   , showAlter
   ) where
 
-import EVM.Expr (readWord, isLitWord)
+import EVM.Expr (readWord, readByte, readBytes, isLitWord)
 import EVM.Types
 
 import Control.Applicative ((<|>))
@@ -71,7 +71,7 @@ import Data.ByteString qualified as BS
 import Data.ByteString.Base16 qualified as BS16
 import Data.ByteString.Char8 qualified as Char8
 import Data.ByteString.Lazy qualified as BSLazy
-import Data.Char (isHexDigit)
+import Data.Char (isHexDigit, chr)
 import Data.Data (Data)
 import Data.DoubleWord (Word256, Int256, signedWord)
 import Data.Functor (($>))
@@ -82,7 +82,7 @@ import Data.Text qualified as Text
 import Data.Text.Encoding (encodeUtf8)
 import Data.Vector (Vector, toList)
 import Data.Vector qualified as Vector
-import Data.Word (Word32)
+import Data.Word (Word32, Word8)
 import GHC.Generics (Generic)
 import Test.QuickCheck hiding ((.&.), label)
 import Numeric (showHex)
@@ -498,35 +498,65 @@ bytesP = do
     Right d -> pure $ ByteStringS d
     Left _ -> pfail
 
-data AbiVals = NoVals | CAbi [AbiValue] | SAbi [Expr EWord]
+data AbiVals = NoVals | CAbi [AbiValue] | SAbi [Expr EWord] | MixAbi ([Expr EWord], AbiValue)
   deriving (Show)
 
 decodeBuf :: [AbiType] -> Expr Buf -> AbiVals
 decodeBuf tps (ConcreteBuf b) =
   case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict b) of
     Right ("", _, args) -> CAbi (toList args)
     _ -> NoVals
-decodeBuf tps buf =
-  if any isDynamic tps then NoVals
-  else
-    let
-      vs = decodeStaticArgs 0 (length tps) buf
-      asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs)
-    in if not (all isLitWord vs)
-       then SAbi vs
-       else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of
-         Right ("", _, args) -> CAbi (toList args)
-         _ -> NoVals
-
+decodeBuf tpsOrig bufOrig = go tpsOrig bufOrig 0 NoVals
   where
     isDynamic t = abiKind t == Dynamic
+    go :: [AbiType] -> Expr Buf -> Int -> AbiVals -> AbiVals
+    go [] _ _ ret = ret
+    go [AbiStringType] buf off (SAbi acc) = MixAbi (acc, decodeStringArg off buf)
+    go (x:_) _ _ _ | isDynamic x = internalError "Dynamic type must be last in the list"
+    go (_:tps) buf off (SAbi acc) =
+      let
+        v = readWord (Lit (unsafeInto off)) buf
+      in if not (isLitWord v) then go tps buf (off+32) (SAbi (acc++[v]))
+         else internalError "can't mix Symbolic and Concrete"
+    go (t:tps) buf off (CAbi acc) =
+      let v = readWord (Lit (unsafeInto off)) buf
+          asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord [v])
+      in case runGetOrFail (getAbiSeq 1 [t]) (BSLazy.fromStrict asBS) of
+        Right ("", _, args) -> go tps buf (off+32) $ CAbi (acc++(toList args))
+        _ -> NoVals
+    go _ _ _ _ = internalError "decodeBuf: expected concrete buffer"
+-- decodeBuf tps buf =
+--   let
+--     vs = decodeStaticArgs 0 (length tps) buf
+--     asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord vs)
+--   in if not (all isLitWord vs)
+--      then SAbi vs
+--      else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of
+--        Right ("", _, args) -> CAbi (toList args)
+--        _ -> NoVals
+-- decodeBuf _ _ = internalError "decodeBuf: expected concrete buffer"
 
 decodeStaticArgs :: Int -> Int -> Expr Buf -> [Expr EWord]
 decodeStaticArgs offset numArgs b =
   [readWord (Lit . unsafeInto $ i) b | i <- [offset,(offset+32) .. (offset + (numArgs-1)*32)]]
 
--- QuickCheck instances
+decodeStringArg :: Int -> Expr Buf -> AbiValue
+decodeStringArg offs (ConcreteBuf b) =
+  let len = forceLit $ readBytes 4 (Lit . unsafeInto $ offs) (ConcreteBuf b)
+      str = [readByte (Lit . unsafeInto $ (offs + 4 + (unsafeInto i))) (ConcreteBuf b) | i <- [0..len]]
+      bs = (map toLitByte str)
+  in AbiString $ BS.pack bs
+  where
+    toLitByte :: Expr Byte -> Word8
+    toLitByte (LitByte w) = w
+    toLitByte _ = internalError "String part of calldata should be concrete"
+    forceLit :: Expr EWord -> W256
+    forceLit (Lit w) = w
+    forceLit _ = internalError "String part of calldata should be concrete"
+decodeStringArg _ _  = internalError "decodeStringArg: expected concrete buffer"
 
+-- QuickCheck instances
+--
 genAbiValue :: AbiType -> Gen AbiValue
 genAbiValue = \case
    AbiUIntType n -> AbiUInt n <$> genUInt n

src/EVM/Solidity.hs

@@ -185,7 +185,7 @@ instance Monoid BuildOutput where
   mempty = BuildOutput mempty mempty
 
 -- | The various project types understood by hevm
-data ProjectType = DappTools | CombinedJSON | Foundry | FoundryStdLib
+data ProjectType = CombinedJSON | Foundry | FoundryStdLib
   deriving (Eq, Show, Read, ParseField)
 
 data SourceCache = SourceCache
@@ -285,13 +285,6 @@ makeSrcMaps = (\case (_, Fe, _) -> Nothing; x -> Just (done x))
 
 -- | Reads all solc output json files found under the provided filepath and returns them merged into a BuildOutput
 readBuildOutput :: App m => FilePath -> ProjectType -> m (Either String BuildOutput)
-readBuildOutput root DappTools = do
-  let outDir = root </> "out"
-  jsons <- liftIO $ findJsonFiles outDir
-  case jsons of
-    [x] -> readSolc DappTools root (outDir </> x)
-    [] -> pure . Left $ "no json files found in: " <> outDir
-    _ -> pure . Left $ "multiple json files found in: " <> outDir
 readBuildOutput root CombinedJSON = do
   let outDir = root </> "out"
   jsons <- liftIO $ findJsonFiles outDir
@@ -413,7 +406,6 @@ force :: String -> Maybe a -> a
 force s = fromMaybe (internalError s)
 
 readJSON :: ProjectType -> Text -> Text -> Maybe (Contracts, Asts, Sources)
-readJSON DappTools _ json = readStdJSON json
 readJSON CombinedJSON _ json = readCombinedJSON json
 readJSON _ contractName json = readFoundryJSON contractName json