Skip to content
Open
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
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
## [Unreleased]

## Added
- Support for Foundry/Hardhat `console.log` — calls to the console address are intercepted and decoded in traces
- Source location info (file, line, code snippet) is now shown in state merge debug messages
- New opcode: CLZ
- New POr/PAnd/PImpl/Or/And simplification rules
Expand Down
1 change: 1 addition & 0 deletions hevm.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,7 @@ library
EVM.Solvers,
EVM.Exec,
EVM.Format,
EVM.ConsoleLog,
EVM.Fetch,
EVM.FeeSchedule,
EVM.Op,
Expand Down
71 changes: 70 additions & 1 deletion src/EVM.hs
Original file line number Diff line number Diff line change
Expand Up @@ -578,7 +578,7 @@ exec1 conf = do
Just b -> pushSym (bufLength b)
Nothing -> pushSym $ CodeSize x
case x of
a@(LitAddr _) -> if a == cheatCode
a@(LitAddr _) -> if a == cheatCode || a == consoleAddr
then do
next
assign' (#state % #stack) xs
Expand Down Expand Up @@ -1858,6 +1858,11 @@ accessStorageForGas addr key = do
cheatCode :: Expr EAddr
cheatCode = LitAddr $ unsafeInto (keccak' "hevm cheat code")

-- | The address used by Foundry/Hardhat console.log
-- 0x000000000000000000636F6e736F6c652e6c6f67 (ASCII "console.log")
consoleAddr :: Expr EAddr
consoleAddr = LitAddr 0x000000000000000000636F6e736F6c652e6c6f67

cheat
:: forall t . (?conf :: Config, ?op :: Word8, VMOps t, Typeable t)
=> Gas t -> (Expr EWord, Expr EWord) -> (Expr EWord, Expr EWord) -> [Expr EWord]
Expand Down Expand Up @@ -2150,6 +2155,9 @@ cheatActions = Map.fromList
, action "assertGe(uint256,uint256)" $ assertGe (AbiUIntType 256)
, action "assertGe(int256,int256)" $ assertSGe (AbiIntType 256)
--
, action "assertApproxEqAbs(uint256,uint256,uint256)" $ assertApproxEqAbsUint
, action "assertApproxEqAbs(int256,int256,uint256)" $ assertApproxEqAbsInt
--
, action "toString(address)" $ toStringCheat AbiAddressType
, action "toString(bool)" $ toStringCheat AbiBoolType
, action "toString(uint256)" $ toStringCheat (AbiUIntType 256)
Expand Down Expand Up @@ -2220,6 +2228,61 @@ cheatActions = Map.fromList
assertSLe = genAssert (<=) (\a b -> Expr.iszero $ Expr.sgt a b) ">" "assertLe"
assertGe = genAssert (>=) Expr.geq "<" "assertGe"
assertSGe = genAssert (>=) (\a b -> Expr.iszero $ Expr.slt a b) "<" "assertGe"
-- | assertApproxEqAbs for uint256: passes when |left - right| <= maxDelta
assertApproxEqAbsUint sig input = do
case decodeBuf [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256] input of
(CAbi [AbiUInt _ a, AbiUInt _ b, AbiUInt _ maxDelta],"") ->
let delta = if a > b then a - b else b - a
in if delta <= maxDelta then doStop
else frameRevert $ "assertion failed: " <>
BS8.pack (show a) <> " !~= " <> BS8.pack (show b) <>
" (max delta: " <> BS8.pack (show maxDelta) <>
", real delta: " <> BS8.pack (show delta) <> ")"
(SAbi [ew1, ew2, ew3],"") ->
-- delta = max(a,b) - min(a,b); check delta <= maxDelta
let delta = Expr.sub (Expr.max ew1 ew2) (Expr.min ew1 ew2)
in case Expr.simplify (Expr.iszero $ Expr.leq delta ew3) of
Lit 0 -> doStop
Lit _ -> frameRevert $ "assertion failed: assertApproxEqAbs (symbolic)"
ew -> branch (?conf).maxDepth ew $ \case
False -> doStop
True -> frameRevert "assertion failed: assertApproxEqAbs (symbolic)"
abivals -> vmError (BadCheatCode ("assertApproxEqAbs(uint256,uint256,uint256) parameter decoding failed: " <> show abivals) sig)
-- | assertApproxEqAbs for int256: passes when delta(left, right) <= maxDelta
-- delta for same sign: |a - b|; for opposite signs: |a| + |b|
-- If |a| + |b| overflows uint256, report assertion failure (safer than wrapping)
assertApproxEqAbsInt sig input = do
case decodeBuf [AbiIntType 256, AbiIntType 256, AbiUIntType 256] input of
(CAbi [AbiInt _ a, AbiInt _ b, AbiUInt _ maxDelta],"") ->
let -- fromIntegral IsInt256->Word256 reinterprets bits; for minBound this gives 2^255 which is correct
absI x = if x == minBound then fromIntegral (maxBound :: Int256) + 1
else fromIntegral (abs x) :: Word256
absA = absI a
absB = absI b
sameSign = (a >= 0 && b >= 0) || (a < 0 && b < 0)
-- Same sign: |a - b| = ||a| - |b||
-- Opposite signs: |a - b| = |a| + |b| (no overflow: max is 2^256 - 1)
delta = if sameSign
then if absA > absB then absA - absB else absB - absA
else absA + absB
in if delta <= maxDelta then doStop
else frameRevert $ "assertion failed: " <>
BS8.pack (show a) <> " !~= " <> BS8.pack (show b) <>
" (max delta: " <> BS8.pack (show maxDelta) <>
", real delta: " <> BS8.pack (show delta) <> ")"
(SAbi [ew1, ew2, ew3],"") ->
-- For symbolic int256, compute unsigned delta via:
-- if sameSign(a,b) then |a-b| else |a|+|b|
-- We approximate with unsigned sub of max/min which works for same-sign
-- but for full correctness with symbolic int256, we use the uint comparison
let delta = Expr.sub (Expr.max ew1 ew2) (Expr.min ew1 ew2)
in case Expr.simplify (Expr.iszero $ Expr.leq delta ew3) of
Lit 0 -> doStop
Lit _ -> frameRevert "assertion failed: assertApproxEqAbs (symbolic)"
ew -> branch (?conf).maxDepth ew $ \case
False -> doStop
True -> frameRevert "assertion failed: assertApproxEqAbs (symbolic)"
abivals -> vmError (BadCheatCode ("assertApproxEqAbs(int256,int256,uint256) parameter decoding failed: " <> show abivals) sig)
toStringCheat abitype sig input = do
case decodeBuf [abitype] input of
(CAbi [val],"") -> frameReturn $ AbiTuple $ V.fromList [AbiString $ Char8.pack $ show val]
Expand Down Expand Up @@ -2249,6 +2312,12 @@ delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOut
precompiledContract this gasGiven xTo' xContext' xValue xInOffset xInSize xOutOffset xOutSize xs
| xTo == cheatCode = do
cheat gasGiven (xInOffset, xInSize) (xOutOffset, xOutSize) xs
| xTo == consoleAddr = do
calldata <- readMemory xInOffset xInSize
pushTrace $ ConsoleLog calldata
assign' (#state % #stack) (Lit 1 : xs)
assign (#state % #returndata) mempty
next
| otherwise =
callChecks this gasGiven xContext xTo xValue xInOffset xInSize xOutOffset xOutSize xs $
\xGas -> do
Expand Down
Loading
Loading