Skip to content

Commit

Permalink
Moving to forge-std
Browse files Browse the repository at this point in the history
  • Loading branch information
msooseth committed Oct 31, 2024
1 parent 92a7048 commit 0905738
Show file tree
Hide file tree
Showing 12 changed files with 63 additions and 133 deletions.
6 changes: 3 additions & 3 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 CombinedJSON | Foundry | FoundryStdLib 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 CombinedJSON | Foundry | FoundryStdLib project (default: Foundry)"
, projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON or Foundry project (default: Foundry)"
}
| Test -- Run Foundry unit tests
{ root :: w ::: Maybe String <?> "Path to project root directory (default: . )"
, projectType :: w ::: Maybe ProjectType <?> "Is this a CombinedJSON | Foundry | FoundryStdLib 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
2 changes: 1 addition & 1 deletion doc/src/exec.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,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
--project-type PROJECTTYPE Foundry or CombinedJSON project
```

Minimum required flags: either you must provide `--code` or you must both pass
Expand Down
2 changes: 1 addition & 1 deletion doc/src/symbolic.md
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +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
--project-type PROJECTTYPE Foundry or CombinedJSON project
--initial-storage INITIALSTORAGE
Starting state for storage: Empty, Abstract (default
Abstract)
Expand Down
2 changes: 1 addition & 1 deletion doc/src/test.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +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
--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
64 changes: 8 additions & 56 deletions src/EVM.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1911,7 +1911,7 @@ cheatActions = Map.fromList
SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
Lit 1 -> frameRevert "assertion failed"
Lit 0 -> doStop
ew -> branch (Expr.iszero ew) $ \case
ew -> branch ew $ \case
True -> frameRevert "assertion failed"
False -> doStop
k -> vmError $ BadCheatCode ("assertTrue(bool) parameter decoding failed: " <> show k) sig
Expand All @@ -1922,7 +1922,7 @@ cheatActions = Map.fromList
SAbi [eword] -> case (Expr.simplify (Expr.iszero eword)) of
Lit 0 -> frameRevert "assertion failed"
Lit 1 -> doStop
ew -> branch (ew) $ \case
ew -> branch ew $ \case
False -> frameRevert "assertion failed"
True -> doStop
k -> vmError $ BadCheatCode ("assertFalse(bool) parameter decoding failed: " <> show k) sig
Expand All @@ -1931,32 +1931,12 @@ cheatActions = Map.fromList
, 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(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 "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 "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 "assertLt(uint256,uint256)" $ assertLt (AbiUIntType 256)
, action "assertLt(int256,int256)" $ assertLt (AbiIntType 256)
Expand Down Expand Up @@ -2007,66 +1987,38 @@ cheatActions = Map.fromList
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
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: "
<> str <> ": " <> BS8.pack (show a) <> " " <> comp <> " " <> BS8.pack (show b)
assertEq 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 0 -> revertErr ew1 ew2 "!="
Lit 1 -> doStop
ew -> branch (ew) $ \case
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 "!="
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 "!="
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
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 "!="
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 ">="
SAbi [ew1, ew2] -> case (Expr.simplify (Expr.lt ew1 ew2)) of
Lit 0 -> revertErr ew1 ew2 ">="
Lit 1 -> doStop
ew -> branch (ew) $ \case
ew -> branch ew $ \case
False ->revertErr ew1 ew2 ">="
True -> doStop
abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLt" abivals) sig)
Expand All @@ -2077,7 +2029,7 @@ cheatActions = Map.fromList
SAbi [ew1, ew2] -> case (Expr.simplify (Expr.gt ew1 ew2)) of
Lit 0 -> revertErr ew1 ew2 "<="
Lit 1 -> doStop
ew -> branch (ew) $ \case
ew -> branch ew $ \case
False ->revertErr ew1 ew2 "<="
True -> doStop
abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGt" abivals) sig)
Expand All @@ -2088,7 +2040,7 @@ cheatActions = Map.fromList
SAbi [ew1, ew2] -> case (Expr.simplify (Expr.leq ew1 ew2)) of
Lit 0 -> revertErr ew1 ew2 ">"
Lit 1 -> doStop
ew -> branch (ew) $ \case
ew -> branch ew $ \case
False ->revertErr ew1 ew2 ">"
True -> doStop
abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertLe" abivals) sig)
Expand All @@ -2099,7 +2051,7 @@ cheatActions = Map.fromList
SAbi [ew1, ew2] -> case (Expr.simplify (Expr.geq ew1 ew2)) of
Lit 0 -> revertErr ew1 ew2 "<"
Lit 1 -> doStop
ew -> branch (ew) $ \case
ew -> branch ew $ \case
False ->revertErr ew1 ew2 "<"
True -> doStop
abivals -> vmError (BadCheatCode (paramDecodeErr abitype "assertGe" abivals) sig)
Expand Down
77 changes: 26 additions & 51 deletions src/EVM/ABI.hs
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ module EVM.ABI
, showAlter
) where

import EVM.Expr (readWord, readByte, readBytes, isLitWord)
import EVM.Expr (readWord, isLitWord)
import EVM.Types

import Control.Applicative ((<|>))
Expand All @@ -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, chr)
import Data.Char (isHexDigit)
import Data.Data (Data)
import Data.DoubleWord (Word256, Int256, signedWord)
import Data.Functor (($>))
Expand All @@ -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, Word8)
import Data.Word (Word32)
import GHC.Generics (Generic)
import Test.QuickCheck hiding ((.&.), label)
import Numeric (showHex)
Expand Down Expand Up @@ -328,22 +328,19 @@ abiTailSize x =
_ -> internalError "impossible"

abiHeadSize :: AbiValue -> Int
abiHeadSize x = abiSizeType (abiValueType x)

abiSizeType :: AbiType -> Int
abiSizeType x =
case abiKind x of
abiHeadSize x =
case abiKind (abiValueType x) of
Dynamic -> 32
Static ->
case x of
AbiUIntType _ -> 32
AbiIntType _ -> 32
AbiBytesType n -> roundTo32Bytes n
AbiAddressType -> 32
AbiBoolType -> 32
AbiTupleType n -> sum (abiSizeType <$> n)
AbiArrayType n t -> n*(abiSizeType t)
AbiFunctionType -> 32
AbiUInt _ _ -> 32
AbiInt _ _ -> 32
AbiBytes n _ -> roundTo32Bytes n
AbiAddress _ -> 32
AbiBool _ -> 32
AbiTuple v -> sum (abiHeadSize <$> v)
AbiArray _ _ xs -> sum (abiHeadSize <$> xs)
AbiFunction _ -> 32
_ -> internalError "impossible"

putAbiSeq :: Vector AbiValue -> Put
Expand Down Expand Up @@ -501,56 +498,34 @@ bytesP = do
Right d -> pure $ ByteStringS d
Left _ -> pfail

data AbiVals = NoVals | CAbi [AbiValue] | SAbi [Expr EWord] | MixAbi ([Expr EWord], AbiValue)
data AbiVals = NoVals | CAbi [AbiValue] | SAbi [Expr EWord]
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 tpsOrig bufOrig = go tpsOrig bufOrig 0 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
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 [_] _ _ (SAbi _) = internalError "Currently we can only decode string as last dynamic type"
go (x:_) _ _ _ | isDynamic x = internalError "Dynamic type must be last in the list"
go (t:ts) buf off (SAbi acc) =
let len = abiSizeType t
v = readBytes len (Lit (unsafeInto off)) buf
in go ts buf (off+len) (SAbi (acc++[v]))
go (t:ts) buf off (CAbi acc) | (not . isDynamic) t =
let len = abiSizeType t
v = readBytes len (Lit (unsafeInto off)) buf
asBS = mconcat $ fmap word256Bytes (mapMaybe maybeLitWord [v])
in case runGetOrFail (getAbiSeq 1 [t]) (BSLazy.fromStrict asBS) of
Right ("", _, args) -> go ts buf (off+len) $ CAbi (acc++(toList args))
_ -> NoVals
go _ _ _ _ = 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)]]

decodeStringArg :: Int -> Expr Buf -> AbiValue
decodeStringArg offs (ConcreteBuf b) =
let len = forceLit $ readBytes 32 (Lit . unsafeInto $ offs) (ConcreteBuf b)
str = [readByte (Lit . unsafeInto $ (offs + 32 + (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
Expand Down
2 changes: 1 addition & 1 deletion 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 = CombinedJSON | Foundry | FoundryStdLib
data ProjectType = CombinedJSON | Foundry
deriving (Eq, Show, Read, ParseField)

data SourceCache = SourceCache
Expand Down
8 changes: 4 additions & 4 deletions src/EVM/UnitTest.hs
Original file line number Diff line number Diff line change
Expand Up @@ -204,13 +204,13 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
Nothing -> And (readStorage' (Lit 0) (testContract store).storage) (Lit 2) .== Lit 2
postcondition = curry $ case shouldFail of
True -> \(_, post) -> case post of
Success _ _ _ store -> failed store
_ -> PBool True
Success _ _ _ store -> failed store
_ -> PBool True
False -> \(_, post) -> case post of
Success _ _ _ store -> PNeg (failed store)
Failure _ _ (Revert msg) -> case msg of
ConcreteBuf b -> do
if (BS.isPrefixOf (BS.pack "assert failed") b) || b == panicMsg 0x01 then PBool False
ConcreteBuf b ->
if (BS.isPrefixOf (selector "Error(string)") b) || b == panicMsg 0x01 then PBool False
else PBool True
b -> b ./= ConcreteBuf (panicMsg 0x01)
Failure _ _ _ -> PBool True
Expand Down
2 changes: 1 addition & 1 deletion test/EVM/Test/Utils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ callProcessCwd cmd args cwd = do

compile :: App m => ProjectType -> FilePath -> FilePath -> m (Either String BuildOutput)
compile CombinedJSON _root _src = internalError "unsupported compile type: CombinedJSON"
compile foundryType root src = do
compile Foundry root src = do
liftIO $ createDirectory (root </> "src")
liftIO $ writeFile (root </> "src" </> "unit-tests.t.sol") =<< readFile =<< Paths.getDataFileName src
liftIO $ initLib (root </> "lib" </> "tokens") ("test" </> "contracts" </> "lib" </> "erc20.sol") "erc20.sol"
Expand Down
2 changes: 2 additions & 0 deletions test/contracts/pass/cheatCodes.sol
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,8 @@ contract Empty {}

contract CheatCodes is Test {
address store = address(new HasStorage());
address constant HEVM_ADDRESS =
address(bytes20(uint160(uint256(keccak256('hevm cheat code')))));
Hevm hevm = Hevm(HEVM_ADDRESS);

function prove_warp_concrete() public {
Expand Down
Loading

0 comments on commit 0905738

Please sign in to comment.