From c6cc2a99fed50b96182a98b6dee998391c2ad8cc Mon Sep 17 00:00:00 2001 From: zoep Date: Mon, 10 Feb 2025 14:51:39 +0200 Subject: [PATCH 1/5] Rebase and fix conflicts --- src/EVM/Solidity.hs | 1 + src/EVM/SymExec.hs | 7 ++++--- test/test.hs | 34 +++++++++++++++++++++++++++------- 3 files changed, 32 insertions(+), 10 deletions(-) diff --git a/src/EVM/Solidity.hs b/src/EVM/Solidity.hs index 0128c5fd3..b2d98684c 100644 --- a/src/EVM/Solidity.hs +++ b/src/EVM/Solidity.hs @@ -394,6 +394,7 @@ solcRuntime contract src = do Just (Contracts sol, _, _) -> pure $ Map.lookup ("hevm.sol:" <> contract) sol <&> (.runtimeCode) Nothing -> internalError $ "unable to parse solidity output:\n" <> (T.unpack json) + functionAbi :: Text -> IO Method functionAbi f = do json <- solc Solidity ("contract ABI { function " <> f <> " public {}}") diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 10fe1d037..aa2471b27 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -687,8 +687,9 @@ equivalenceCheck -> ByteString -> VeriOpts -> (Expr Buf, [Prop]) + -> Bool -> m ([EquivResult], [Expr End]) -equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do +equivalenceCheck solvers bytecodeA bytecodeB opts calldata create = do conf <- readConfig case bytecodeA == bytecodeB of True -> liftIO $ do @@ -706,7 +707,7 @@ equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do getBranches :: ByteString -> m [Expr End] getBranches bs = do let bytecode = if BS.null bs then BS.pack [0] else bs - prestate <- liftIO $ stToIO $ abstractVM calldata bytecode Nothing False + prestate <- liftIO $ stToIO $ abstractVM calldata bytecode Nothing create expr <- interpret (Fetch.oracle solvers Nothing) opts.maxIter opts.askSmtIters opts.loopHeuristic prestate runExpr let simpl = if opts.simp then (Expr.simplify expr) else expr pure $ flattenExpr simpl @@ -844,7 +845,7 @@ equivalenceCheck' solvers branchesA branchesB = do -- TODO: is this sound? do we need a more sophisticated nonce representation? noncesDiffer = PBool (ac.nonce /= bc.nonce) storesDiffer = case (ac.storage, bc.storage) of - (ConcreteStore as, ConcreteStore bs) -> PBool $ as /= bs + (ConcreteStore as, ConcreteStore bs) | not (as == Map.empty || bs == Map.empty) -> PBool $ as /= bs (as, bs) -> if as == bs then PBool False else as ./= bs in balsDiffer .|| storesDiffer .|| noncesDiffer diff --git a/test/test.hs b/test/test.hs index 82da7c908..57628ef7f 100644 --- a/test/test.hs +++ b/test/test.hs @@ -3747,9 +3747,29 @@ tests = testGroup "hevm" } |] withSolvers Z3 3 1 Nothing $ \s -> do - (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) + (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False assertBoolM "Must have a difference" (any isCex res) , + test "implicit-constructor" $ do + Just initA <- solidity "C" + [i| + contract C { + uint x; + } + |] + Just initB <- solidity "C" + [i| + contract C { + uint x; + constructor() { + x = 0; + } + } + |] + withSolvers Z3 3 1 Nothing $ \s -> do + a <- equivalenceCheck s initA initB defaultVeriOpts (mkCalldata Nothing []) True + assertEqualM "Must have no difference" [Qed ()] a + , test "eq-sol-exp-qed" $ do Just aPrgm <- solcRuntime "C" [i| @@ -3772,7 +3792,7 @@ tests = testGroup "hevm" } |] withSolvers Z3 3 1 Nothing $ \s -> do - (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) + (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False assertEqualM "Must have no difference" [Qed ()] res , test "eq-balance-differs" $ do @@ -3803,7 +3823,7 @@ tests = testGroup "hevm" } |] withSolvers Z3 3 1 Nothing $ \s -> do - (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) + (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False assertBoolM "Must differ" (all isCex res) , -- TODO: this fails because we don't check equivalence of deployed contracts @@ -3864,7 +3884,7 @@ tests = testGroup "hevm" } |] withSolvers Z3 3 1 Nothing $ \s -> do - (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) + (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False assertBoolM "Must differ" (all isCex res) , test "eq-unknown-addr" $ do @@ -3888,7 +3908,7 @@ tests = testGroup "hevm" |] withSolvers Z3 3 1 Nothing $ \s -> do let cd = mkCalldata (Just (Sig "a(address,address)" [AbiAddressType, AbiAddressType])) [] - (res,_) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts cd + (res,_) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts cd False assertEqualM "Must be different" (any isCex res) True , test "eq-sol-exp-cex" $ do @@ -3913,7 +3933,7 @@ tests = testGroup "hevm" } |] withSolvers Bitwuzla 3 1 Nothing $ \s -> do - (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) + (res, _) <- equivalenceCheck s aPrgm bPrgm defaultVeriOpts (mkCalldata Nothing []) False assertEqualM "Must be different" (any isCex res) True , test "eq-all-yul-optimization-tests" $ do let opts = defaultVeriOpts{ maxIter = Just 5, askSmtIters = 20, loopHeuristic = Naive } @@ -4126,7 +4146,7 @@ tests = testGroup "hevm" Just bPrgm <- liftIO $ yul "" $ T.pack $ unlines filteredBSym procs <- liftIO $ getNumProcessors withSolvers CVC5 (unsafeInto procs) 1 (Just 100) $ \s -> do - (res, _) <- equivalenceCheck s aPrgm bPrgm opts (mkCalldata Nothing []) + (res, _) <- equivalenceCheck s aPrgm bPrgm opts (mkCalldata Nothing []) False end <- liftIO $ getCurrentTime case any isCex res of False -> liftIO $ do From 272354a3e4e3fa3478a881bf69cc91c274afd821 Mon Sep 17 00:00:00 2001 From: zoep Date: Mon, 10 Feb 2025 14:56:44 +0200 Subject: [PATCH 2/5] Rebase and fix conflicts --- test/test.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/test.hs b/test/test.hs index 57628ef7f..e4a0b2048 100644 --- a/test/test.hs +++ b/test/test.hs @@ -3767,8 +3767,8 @@ tests = testGroup "hevm" } |] withSolvers Z3 3 1 Nothing $ \s -> do - a <- equivalenceCheck s initA initB defaultVeriOpts (mkCalldata Nothing []) True - assertEqualM "Must have no difference" [Qed ()] a + (res, _) <- equivalenceCheck s initA initB defaultVeriOpts (mkCalldata Nothing []) True + assertEqualM "Must have no difference" [Qed ()] res , test "eq-sol-exp-qed" $ do Just aPrgm <- solcRuntime "C" From 283b3836b70210bf1825c50de366ff5b67ce446c Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 7 Feb 2025 19:49:33 +0100 Subject: [PATCH 3/5] Adding a simplification to remove an issue --- src/EVM/Expr.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index b38bfa4e7..9ea87e046 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -243,6 +243,9 @@ readByte i@(Lit x) (WriteWord (Lit idx) val src) (Lit _) -> indexWord (Lit $ x - idx) val _ -> IndexWord (Lit $ x - idx) val else readByte i src +-- reading a byte that is lower than the dstOffset of a CopySlice, so it's just reading from src +readByte i@(Lit x) (CopySlice _ (Lit dstOffset) _ _ dst) | dstOffset > x = + readByte i dst readByte i@(Lit x) (CopySlice (Lit srcOffset) (Lit dstOffset) (Lit size) src dst) = if x - dstOffset < size then readByte (Lit $ x - (dstOffset - srcOffset)) src From 630b347901a3abc805d2b723998c67dcc876cd75 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Fri, 7 Feb 2025 19:50:48 +0100 Subject: [PATCH 4/5] Fixing comment --- src/EVM/Expr.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 9ea87e046..7ca6067fd 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -243,7 +243,7 @@ readByte i@(Lit x) (WriteWord (Lit idx) val src) (Lit _) -> indexWord (Lit $ x - idx) val _ -> IndexWord (Lit $ x - idx) val else readByte i src --- reading a byte that is lower than the dstOffset of a CopySlice, so it's just reading from src +-- reading a byte that is lower than the dstOffset of a CopySlice, so it's just reading from dst readByte i@(Lit x) (CopySlice _ (Lit dstOffset) _ _ dst) | dstOffset > x = readByte i dst readByte i@(Lit x) (CopySlice (Lit srcOffset) (Lit dstOffset) (Lit size) src dst) From c751204d1d16496dcc964b2304dd9f0acb9abd0a Mon Sep 17 00:00:00 2001 From: zoep Date: Mon, 10 Feb 2025 14:25:14 +0200 Subject: [PATCH 5/5] Update changelog --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index bb13db829..84679276c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -19,6 +19,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Multiple solutions are allowed for a single symbolic expression - Aliasing works much better for symbolic and concrete addresses - Constant propagation for symbolic values +- Add deployment code flag to the `equivalenceCheck` function +- New simplification rule for reading a byte that is lower than destination offset in `copySlice` ## Fixed - We now try to simplify expressions fully before trying to cast them to a concrete value @@ -30,6 +32,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Better exponential simplification - Dumping of END states (.prop) files is now default for `--debug` - When cheatcode is missing, we produce a partial execution warning +- The equivalence checker now is able to prove that an empty store is equivalent to a store with all slots initialized to 0. + ## Changed - Warnings now lead printing FAIL. This way, users don't accidentally think that