Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[DRAFT] Cheatcodes as per new std-forge library #567

Draft
wants to merge 8 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- More complete and precise array/mapping slot rewrite, along with a copySlice improvement
- Use a let expression in copySlice to decrease expression size
- The `--debug` flag now dumps the internal expressions as well
- hevm now uses the std-forge library's way of detecting failures, i.e. through
reverting with a specific error code

## Added
- More POr and PAnd rules
Expand Down
8 changes: 4 additions & 4 deletions cli/cli.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 or Foundry 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"
Expand Down Expand Up @@ -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 or Foundry 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 or Foundry 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"
Expand Down
6 changes: 2 additions & 4 deletions doc/src/exec.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,13 +38,11 @@ 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
Is this a Foundry or DappTools project (default:
Foundry)
--project-type PROJECTTYPE Foundry or CombinedJSON project
```

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
Expand Down
4 changes: 1 addition & 3 deletions doc/src/symbolic.md
Original file line number Diff line number Diff line change
Expand Up @@ -41,9 +41,7 @@ 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
Is this a Foundry or DappTools project (default:
Foundry)
--project-type PROJECTTYPE Foundry or CombinedJSON project
--initial-storage INITIALSTORAGE
Starting state for storage: Empty, Abstract (default
Abstract)
Expand Down
4 changes: 1 addition & 3 deletions doc/src/test.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,7 @@ Usage: hevm test [--root STRING] [--project-type PROJECTTYPE] [--rpc TEXT]
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)
--project-type PROJECTTYPE Foundry or CombinedJSON project
--rpc TEXT Fetch state from a remote node
--number W256 Block: number
--verbose INT Append call trace: {1} failures {2} all
Expand Down
5 changes: 0 additions & 5 deletions funding.json

This file was deleted.

146 changes: 131 additions & 15 deletions src/EVM.hs
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ import Data.Bits (FiniteBits, countLeadingZeros, finiteBitSize)
import Data.ByteArray qualified as BA
import Data.ByteString (ByteString)
import Data.ByteString qualified as BS
import Data.ByteString.Char8 qualified as BS8
import Data.ByteString.Base16 qualified as BS16
import Data.ByteString.Lazy (fromStrict)
import Data.ByteString.Lazy qualified as LS
Expand Down Expand Up @@ -1695,7 +1696,7 @@ cheat gas (inOffset, inSize) (outOffset, outSize) xs = do
Nothing -> partial $ UnexpectedSymbolicArg vm.state.pc (getOpName vm.state) "symbolic cheatcode selector" (wrap [abi])
Just (unsafeInto -> abi') ->
case Map.lookup abi' cheatActions of
Nothing -> vmError (BadCheatCode "cannot understand cheatcode, maybe cheatcode not supported?" abi')
Nothing -> vmError (BadCheatCode "Cannot understand cheatcode. " abi')
Just action -> action input

type CheatAction t s = Expr Buf -> EVM t s ()
Expand Down Expand Up @@ -1903,6 +1904,50 @@ cheatActions = Map.fromList
, $(envReadMultipleCheat "envBytes32(string,string)" $ AbiBytesType 32) stringToBytes32
, $(envReadMultipleCheat "envString(string,string)" AbiStringType) stringToByteString
, $(envReadMultipleCheat "envBytes(bytes,bytes)" AbiBytesDynamicType) stringHexToByteString
, action "assertTrue(bool)" $ \sig input ->
case decodeBuf [AbiBoolType] input of
CAbi [AbiBool True] -> doStop
CAbi [AbiBool False] -> frameRevert "assertion failed"
SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
Lit 1 -> frameRevert "assertion failed"
Lit 0 -> doStop
ew -> branch 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"
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 "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 "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)
, action "assertLt(int256,int256)" $ assertLt (AbiIntType 256)
, action "assertLe(uint256,uint256)" $ assertLe (AbiUIntType 256)
, action "assertLe(int256,int256)" $ assertLe (AbiIntType 256)
, action "assertGt(uint256,uint256)" $ assertGt (AbiUIntType 256)
, action "assertGt(int256,int256)" $ assertGt (AbiIntType 256)
, action "assertGe(uint256,uint256)" $ assertGe (AbiUIntType 256)
, action "assertGe(int256,int256)" $ assertGe (AbiIntType 256)
]
where
action s f = (abiKeccak s, f (abiKeccak s))
Expand Down Expand Up @@ -1942,6 +1987,77 @@ 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 abivals = name <> "(" <> (show abitype) <> "," <> (show abitype) <>
") parameter decoding failed. Error: " <> show abivals
revertErr a b comp = frameRevert $ "assertion failed: " <>
BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
assertEq abitype sig input = do
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not super bothered by the duplication but if you wanted to cut some lines you could probably merge the implementations into one function that is parametrised on the comparison function and string used in the revert error?

case decodeBuf [abitype, abitype] input of
CAbi [a, b] | a == b -> doStop
CAbi [a, b] -> revertErr a b "!="
SAbi [ew1, ew2] -> case (Expr.simplify (Expr.eq ew1 ew2)) of
Lit 0 -> revertErr ew1 ew2 "!="
Lit _ -> doStop
ew -> branch ew $ \case
False ->revertErr ew1 ew2 "!="
True -> doStop
abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertEq" abivals) sig)
assertNotEq abitype sig input = do
case decodeBuf [abitype, abitype] input of
CAbi [a, b] | a /= b -> doStop
CAbi [a, b] -> revertErr a b "=="
SAbi [ew1, ew2] -> case (Expr.simplify (Expr.eq ew1 ew2)) of
Lit 1 -> revertErr ew1 ew2 "=="
Lit _ -> doStop
ew -> branch ew $ \case
True ->revertErr ew1 ew2 "=="
False -> doStop
abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertNotEq" 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 ">="
SAbi [ew1, ew2] -> case (Expr.simplify (Expr.lt ew1 ew2)) of
Lit 0 -> revertErr ew1 ew2 ">="
Lit _ -> 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 "<="
SAbi [ew1, ew2] -> case (Expr.simplify (Expr.gt ew1 ew2)) of
Lit 0 -> revertErr ew1 ew2 "<="
Lit _ -> 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 ">"
SAbi [ew1, ew2] -> case (Expr.simplify (Expr.leq ew1 ew2)) of
Lit 0 -> revertErr ew1 ew2 ">"
Lit _ -> 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 "<"
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")
-- note that the continuation is ignored in the precompile case
Expand Down Expand Up @@ -2212,14 +2328,10 @@ finishFrame how = do
nextFrame : remainingFrames -> do

-- Insert a debug trace.
insertTrace $
case how of
FrameErrored e ->
ErrorTrace e
FrameReverted e ->
ErrorTrace (Revert e)
FrameReturned output ->
ReturnTrace output nextFrame.context
insertTrace $ case how of
FrameReturned output -> ReturnTrace output nextFrame.context
FrameReverted e -> ErrorTrace (Revert e)
FrameErrored e -> ErrorTrace e
-- Pop to the previous level of the debug trace stack.
popTrace

Expand Down Expand Up @@ -2267,11 +2379,13 @@ finishFrame how = do
push 0

-- Case 3: Error during a call?
FrameErrored _ -> do
FrameErrored e -> do
revertContracts
revertSubstate
assign (#state % #returndata) mempty
push 0
if (isInterpretFailure e) then finishFrame (FrameErrored e)
else do
assign (#state % #returndata) mempty
push 0
-- Or were we creating?
CreationContext _ _ reversion subState' -> do
creator <- use (#state % #contract)
Expand Down Expand Up @@ -2314,11 +2428,13 @@ finishFrame how = do
push 0

-- Case 6: Error during a creation?
FrameErrored _ -> do
FrameErrored e -> do
revertContracts
revertSubstate
assign (#state % #returndata) mempty
push 0
if (isInterpretFailure e) then finishFrame (FrameErrored e)
else do
assign (#state % #returndata) mempty
push 0


-- * Memory helpers
Expand Down
1 change: 0 additions & 1 deletion src/EVM/ABI.hs
Original file line number Diff line number Diff line change
Expand Up @@ -517,7 +517,6 @@ decodeBuf tps buf =
else case runGetOrFail (getAbiSeq (length tps) tps) (BSLazy.fromStrict asBS) of
Right ("", _, args) -> CAbi (toList args)
_ -> NoVals

where
isDynamic t = abiKind t == Dynamic

Expand Down
10 changes: 1 addition & 9 deletions src/EVM/Solidity.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
deriving (Eq, Show, Read, ParseField)

data SourceCache = SourceCache
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down
40 changes: 40 additions & 0 deletions src/EVM/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -550,6 +550,46 @@ data EvmError
| NonexistentFork Int
deriving (Show, Eq, Ord)

isInterpretFailure :: EvmError -> Bool
isInterpretFailure = \case
(BadCheatCode {}) -> True
(NonexistentFork {}) -> True
PrecompileFailure -> True
StateChangeWhileStatic -> True
UnrecognizedOpcode _ -> True
_ -> False

isInterpretFailEnd :: Expr a -> Bool
isInterpretFailEnd = \case
(Failure _ _ k) -> isInterpretFailure k
_ -> False

evmErrToString :: EvmError -> String
evmErrToString = \case
-- NOTE: error text made to closely match go-ethereum's errors.go file
OutOfGas {} -> "Out of gas"
-- TODO "contract creation code storage out of gas" not handled
CallDepthLimitReached -> "Max call depth exceeded"
BalanceTooLow {} -> "Insufficient balance for transfer"
-- TODO "contract address collision" not handled
Revert {} -> "Execution reverted"
-- TODO "max initcode size exceeded" not handled
MaxCodeSizeExceeded {} -> "Max code size exceeded"
BadJumpDestination -> "Invalid jump destination"
StateChangeWhileStatic -> "Attempting to modify state while in static context"
ReturnDataOutOfBounds -> "Return data out of bounds"
IllegalOverflow -> "Gas uint64 overflow"
UnrecognizedOpcode op -> "Invalid opcode: 0x" <> showHex op ""
NonceOverflow -> "Nonce uint64 overflow"
StackUnderrun -> "Stack underflow"
StackLimitExceeded -> "Stack limit reached"
InvalidMemoryAccess -> "Write protection"
(BadCheatCode err fun) -> err <> " Cheatcode function selector: " <> show fun
NonexistentFork fork -> "Nonexistent fork: " <> show fork
PrecompileFailure -> "Precompile failure"
err -> "hevm error: " <> show err


-- | Sometimes we can only partially execute a given program
data PartialExec
= UnexpectedSymbolicArg { pc :: Int, opcode :: String, msg :: String, args :: [SomeExpr] }
Expand Down
Loading
Loading