Skip to content

Commit c34d4d6

Browse files
msoosethmsooseth
committed
Collect Keccak Preimages and use them during querying
1 parent f8484a4 commit c34d4d6

File tree

8 files changed

+97
-32
lines changed

8 files changed

+97
-32
lines changed

‎CHANGELOG.md‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,19 @@ All notable changes to this project will be documented in this file.
55
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
66
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
77

8-
## Unreleased
9-
10-
## Changed
11-
- Updated forge to 1.2.3 and forge-std to 60acb7aa (1.9.7+)
8+
## [Unreleased]
129

1310
## Fixed
1411
- We now extract more Keccak computations than before from the Props to assert
1512
more Keccak equalities.
1613
- Faster word256Bytes and word160Bytes functions to help concrete execution
1714
performance
1815

16+
## Changed
17+
- Updated forge to 1.2.3 and forge-std to 60acb7aa (1.9.7+)
18+
- We now gather Keccak axioms during `setUp()` and inject them into the SMT solver.
19+
This helps us finding more correct Keccak preimages
20+
1921
## [0.55.1] - 2025-07-22
2022

2123
## Added

‎hevm.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -313,6 +313,7 @@ test-suite ethereum-tests
313313
BlockchainTests.hs
314314

315315
test-suite cli-test
316+
import: test-common
316317
type:
317318
exitcode-stdio-1.0
318319
default-language: GHC2021

‎src/EVM.hs‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -166,6 +166,7 @@ makeVm o = do
166166
, osEnv = mempty
167167
, freshVar = 0
168168
, exploreDepth = 0
169+
, keccakPreImgs = fromList []
169170
}
170171
where
171172
env = Env
@@ -437,7 +438,11 @@ exec1 conf = do
437438
orig@(ConcreteBuf bs) ->
438439
whenSymbolicElse
439440
(pure $ Keccak orig)
440-
(pure $ Lit (keccak' bs))
441+
(do
442+
let kc = keccak' bs
443+
modifying #keccakPreImgs (insert (bs, kc))
444+
pure $ Lit kc
445+
)
441446
buf -> pure $ Keccak buf
442447
next
443448
assign' (#state % #stack) (hash : xs)

‎src/EVM/SymExec.hs‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -709,13 +709,13 @@ verifyInputs solvers opts fetcher preState maybepost = do
709709
putStrLn " Flattening expression"
710710
printPartialIssues flattened ("the call " <> call)
711711
putStrLn $ " Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
712-
712+
putStrLn $ " Keccak preimages in state: " <> (show $ length preState.keccakPreImgs)
713713
case maybepost of
714714
Nothing -> pure (expr, [(Qed, expr)], partials)
715715
Just post -> do
716716
let
717717
-- Filter out any leaves from `flattened` that can be statically shown to be safe
718-
tocheck = flip map flattened $ \leaf -> (toPropsFinal conf leaf preState.constraints post, leaf)
718+
tocheck = flip map flattened $ \leaf -> (toProps leaf preState post, leaf)
719719
withQueries = filter canBeSat tocheck
720720
when conf.debug $ liftIO $ putStrLn $ " Checking for reachability of " <> show (length withQueries)
721721
<> " potential property violation(s) in call " <> call
@@ -733,9 +733,9 @@ verifyInputs solvers opts fetcher preState maybepost = do
733733
getCallPrefix :: Expr Buf -> String
734734
getCallPrefix (WriteByte (Lit 0) (LitByte a) (WriteByte (Lit 1) (LitByte b) (WriteByte (Lit 2) (LitByte c) (WriteByte (Lit 3) (LitByte d) _)))) = mconcat $ map (printf "%02x") [a,b,c,d]
735735
getCallPrefix _ = "unknown"
736-
toProps leaf constr post = PNeg (post preState leaf) : constr <> extractProps leaf
737-
toPropsFinal conf leaf constr post = if conf.simp then Expr.simplifyProps $ toProps leaf constr post
738-
else toProps leaf constr post
736+
toProps leaf vm post = let keccakConstraints = map (\(bs, k)-> PEq (Keccak (ConcreteBuf bs)) (Lit k)) (Set.toList vm.keccakPreImgs)
737+
in PNeg (post preState leaf) : vm.constraints <> extractProps leaf <> keccakConstraints
738+
739739
canBeSat (a, _) = case a of
740740
[PBool False] -> False
741741
_ -> True

‎src/EVM/Types.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -696,7 +696,8 @@ data VM (t :: VMType) s = VM
696696
, freshVar :: Int
697697
-- ^ used to generate fresh symbolic variable names for overapproximations
698698
-- during symbolic execution. See e.g. OpStaticcall
699-
, exploreDepth :: Int
699+
, exploreDepth :: Int
700+
, keccakPreImgs :: Set (ByteString, W256)
700701
}
701702
deriving (Generic)
702703

‎test/clitest.hs‎

Lines changed: 53 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -11,24 +11,52 @@ break the hevm CLI interface.
1111
-}
1212

1313
import Test.Hspec
14-
import System.Process (readProcess, readProcessWithExitCode)
15-
import System.FilePath ((</>))
14+
import System.Process (readProcessWithExitCode)
1615
import System.Exit (ExitCode(..))
1716
import Data.List.Split (splitOn)
1817
import Data.Text qualified as T
1918
import Data.String.Here
19+
import System.IO.Temp
2020

2121
import EVM.Solidity
22+
import EVM.Types qualified as Types
2223
import EVM.Effects
23-
import EVM.Types
24-
24+
import EVM.Test.Utils
25+
26+
testEnv :: Env
27+
testEnv = Env { config = defaultConfig {
28+
dumpQueries = False
29+
, dumpExprs = False
30+
, dumpEndStates = False
31+
, debug = False
32+
, dumpTrace = False
33+
, decomposeStorage = True
34+
, verb = 1
35+
} }
36+
37+
runOneKeccakTest :: FilePath -> IO ()
38+
runOneKeccakTest testFile = do
39+
withSystemTempDirectory "dapp-test" $ \root -> do
40+
let projectType = Foundry
41+
ret <- runEnv testEnv $ compile projectType root testFile
42+
case ret of
43+
Left e -> do
44+
putStrLn e
45+
Types.internalError $ "Error compiling test file " <> show testFile <> " in directory "
46+
<> show root <> " using project type " <> show projectType
47+
Right _ -> do
48+
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "test"
49+
, "--root", root, "--debug", "--num-cex-fuzz", "0", "--smtdebug"] ""
50+
stderr `shouldNotContain` "CallStack"
51+
stdout `shouldContain` "0x0000000000000000000000000000000000001234"
52+
exitCode `shouldBe` (ExitFailure 1)
2553

2654
main :: IO ()
2755
main = do
2856
hspec $
2957
describe "CLI" $ do
3058
it "hevm help works" $ do
31-
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "--help"] ""
59+
(_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "--help"] ""
3260
stdout `shouldContain` "Usage: hevm"
3361
stdout `shouldContain` "test"
3462
stdout `shouldContain` "equivalence"
@@ -46,18 +74,18 @@ main = do
4674
}
4775
}
4876
|])
49-
let symbHex = bsToHex symbBin
50-
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", symbHex] ""
77+
let symbHex = Types.bsToHex symbBin
78+
(exitCode, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", symbHex] ""
5179
stdout `shouldContain` "Discovered the following"
5280
exitCode `shouldBe` ExitFailure 1
5381

54-
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", symbHex, "--sig", "nonexistent()"] ""
55-
stdout `shouldContain` "QED"
56-
exitCode `shouldBe` ExitSuccess
82+
(exitCode2, stdout2, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", symbHex, "--sig", "nonexistent()"] ""
83+
stdout2 `shouldContain` "QED"
84+
exitCode2 `shouldBe` ExitSuccess
5785

5886
it "hevm equivalence tutorial works -- FAIL" $ do
5987
let torun = splitOn " " "equivalence --code-a 60003560000260005260016000f3 --code-b 7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff60005260016000f3"
60-
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--" ] ++ torun) ""
88+
(exitCode, stdout, _) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--" ] ++ torun) ""
6189
stdout `shouldContain` "Not equivalent"
6290
stdout `shouldContain` "FAIL"
6391
exitCode `shouldBe` ExitFailure 1
@@ -72,7 +100,7 @@ main = do
72100
}
73101
}
74102
|])
75-
let aHex = bsToHex a
103+
let aHex = Types.bsToHex a
76104
Just b <- runApp $ solcRuntime (T.pack "MyContract") (T.pack [i|
77105
contract MyContract {
78106
mapping (address => uint) balances;
@@ -84,15 +112,15 @@ main = do
84112
}
85113
}
86114
|])
87-
let bHex = bsToHex b
88-
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--", "equivalence" , "--code-a", aHex, "--code-b", bHex ]) ""
115+
let bHex = Types.bsToHex b
116+
(exitCode, stdout, _) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--", "equivalence" , "--code-a", aHex, "--code-b", bHex ]) ""
89117
stdout `shouldContain` "No discrepancies found"
90118
stdout `shouldContain` "PASS"
91119
exitCode `shouldBe` ExitSuccess
92120

93121
it "hevm concrete tutorial works" $ do
94122
let torun = splitOn " " "exec --code 0x647175696e6550383480393834f3 --gas 0xff"
95-
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--" ] ++ torun) ""
123+
(exitCode, stdout, _) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--" ] ++ torun) ""
96124
stdout `shouldContain` "Return: 0x64"
97125
exitCode `shouldBe` ExitSuccess
98126

@@ -113,8 +141,8 @@ main = do
113141
}
114142
}
115143
|])
116-
let hexStr = bsToHex c
117-
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", hexStr] ""
144+
let hexStr = Types.bsToHex c
145+
(_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", hexStr] ""
118146
stdout `shouldContain` "Warning: fetching contract at address 0"
119147

120148
-- file "devcon_example.yul" from "eq-all-yul-optimization-tests" in test.hs
@@ -156,13 +184,17 @@ main = do
156184
} |]
157185
Just aPrgm <- yul (T.pack "") $ T.pack a
158186
Just bPrgm <- yul (T.pack "") $ T.pack b
159-
let hexStrA = bsToHex aPrgm
160-
hexStrB = bsToHex bPrgm
161-
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "equivalence", "--num-solvers", "1", "--debug", "--code-a", hexStrA, "--code-b", hexStrB] ""
187+
let hexStrA = Types.bsToHex aPrgm
188+
hexStrB = Types.bsToHex bPrgm
189+
(_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "equivalence", "--num-solvers", "1", "--debug", "--code-a", hexStrA, "--code-b", hexStrB] ""
162190
stdout `shouldContain` "Qed found via cache"
163191
it "crash-of-hevm" $ do
164192
let hexStrA = "608060405234801561001057600080fd5b506004361061002b5760003560e01c8063efa2978514610030575b600080fd5b61004361003e3660046102ad565b610045565b005b60006100508561007a565b9050600061005d866100a8565b905080821461006e5761006e61034c565b50505050505050505050565b600061008761032e6103aa565b8261009457610197610098565b61013e5b6100a291906103e2565b92915050565b60006100b561032e6103aa565b6100be906103aa565b6100c7906103aa565b82806100d1575060005b806100da575060005b61013157605a6100ea60006103aa565b6100f3906103aa565b6100ff6001605a610404565b61010b6001605a610404565b61011891166101976103e2565b6101229190610493565b61012c9190610493565b610149565b604061013f8161013e6103e2565b6101499190610493565b61015391906103e2565b61016061032e60006103e2565b83801561016b575060015b15801590610177575060015b80156101a05750831515801561018b575060015b15158015610197575060015b806101a0575060005b610251576101976101b3605a602d610493565b602d60006101c2600182610493565b6101cd906001610404565b6101d8906001610404565b6101e1906103aa565b6101ea906103aa565b6101f491906103e2565b6101ff90605a610404565b604e61020c8160016103e2565b6102169190610493565b61022490600116605a610404565b1661022e906103aa565b61023891906103e2565b6102429190610493565b61024c9190610493565b610283565b604561025f8161013e6103e2565b6102699190610493565b60456102778161013e6103e2565b6102819190610493565b165b61028d91906103e2565b1692915050565b80358015155b81146100a257600080fd5b80358061029a565b600080600080600080600080610100898b0312156102ca57600080fd5b6102d48a8a610294565b97506102e38a60208b01610294565b96506102f28a60408b016102a5565b95506103018a60608b016102a5565b94506103108a60808b01610294565b935061031f8a60a08b016102a5565b925061032e8a60c08b01610294565b915061033d8a60e08b016102a5565b90509295985092959890939650565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60007f800000000000000000000000000000000000000000000000000000000000000082036103db576103db61037b565b5060000390565b818103600083128015838313168383129190911617156100a2576100a261037b565b60008261043a577f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f800000000000000000000000000000000000000000000000000000000000000082147fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff8414161561048e5761048e61037b565b500590565b80820160008212801584831290811690159190911617156100a2576100a261037b56fea26469706673582212200a37769e5bf4b8b890caac8ab643126d55feb821a0201d2f674203f23fa666ad64736f6c634300081e0033"
165193

166-
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", hexStrA] ""
194+
(exitCode, _, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", hexStrA] ""
167195
stderr `shouldNotContain` "CallStack"
168196
exitCode `shouldBe` ExitSuccess
197+
198+
-- both should fail with address 0x1234 -- a SPECIFIC address, not a ranomly generated one
199+
it "keccak-assumptions-setup" $ runOneKeccakTest "test/contracts/fail/keccak-preimage-setup.sol"
200+
it "keccak-assumptions-constructor" $ runOneKeccakTest "test/contracts/fail/keccak-preimage-constructor.sol"

‎test/contracts/fail/keccak-preimage-constructor.sol‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// SPDX-License-Identifier: MIT
2+
import {Test} from "forge-std/Test.sol";
3+
4+
contract MyContractTest is Test {
5+
mapping (address => uint) balances;
6+
constructor() {
7+
balances[address(0x1234)] = 50;
8+
}
9+
function prove_bad_addr(address x) public view {
10+
assert(balances[x] != 50);
11+
}
12+
}

‎test/contracts/fail/keccak-preimage-setup.sol‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// SPDX-License-Identifier: MIT
2+
import {Test} from "forge-std/Test.sol";
3+
4+
contract MyContractTest is Test {
5+
mapping (address => uint) balances;
6+
function setUp() public {
7+
balances[address(0x1234)] = 50;
8+
}
9+
function prove_bad_addr(address x) public view {
10+
assert(balances[x] != 50);
11+
}
12+
}

0 commit comments

Comments
 (0)