diff --git a/flake.lock b/flake.lock index 49fe93ed..20a0b889 100644 --- a/flake.lock +++ b/flake.lock @@ -1,65 +1,32 @@ { "nodes": { - "cabal-3-12": { - "flake": false, - "locked": { - "lastModified": 1719273538, - "narHash": "sha256-/TECd3cdqGDdlEur88H0KbV7jcE/czc0jecj9921T5c=", - "owner": "haskell", - "repo": "cabal", - "rev": "260ecdc3d848782d4df49e629cb0a5dc9e96ca9e", - "type": "github" - }, - "original": { - "owner": "haskell", - "ref": "Cabal-v3.12.1.0", - "repo": "cabal", - "type": "github" - } - }, "ethereum-tests": { "flake": false, "locked": { - "lastModified": 1682506704, - "narHash": "sha256-PyFZhdUQRUbmohoMS+w41rmSFfKeTO2RqHLetWlU4Jw=", + "lastModified": 1698656397, + "narHash": "sha256-1zhBaJ3X5kQ94qv9Yz12/3d83w3jNP6OtzjH+ykK8sg=", "owner": "ethereum", "repo": "tests", - "rev": "b25623d4d7df10e38498cace7adc7eb413c4b20d", + "rev": "428f218d7d6f4a52544e12684afbfe6e2882ffbf", "type": "github" }, "original": { "owner": "ethereum", - "ref": "v12.2", + "ref": "v13", "repo": "tests", "type": "github" } }, - "flake-compat": { - "flake": false, - "locked": { - "lastModified": 1696426674, - "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", - "type": "github" - }, - "original": { - "owner": "edolstra", - "repo": "flake-compat", - "type": "github" - } - }, "flake-utils": { "inputs": { "systems": "systems" }, "locked": { - "lastModified": 1710146030, - "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "lastModified": 1726560853, + "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a", "type": "github" }, "original": { @@ -141,25 +108,23 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1719997877, - "narHash": "sha256-/Edw+w0PiGgxwnCeJycM0VgH4HtlCi91v1d8xbi+REE=", + "lastModified": 1724145005, + "narHash": "sha256-fTvalF9fSKWJj/HJWtHQ8DrMR1nBH1NV1w/x+O4M/Zw=", "owner": "shazow", "repo": "foundry.nix", - "rev": "02febba4f1cf0606d790acdb24adcf7a64afb4e1", + "rev": "47f8ae49275eeff9bf0526d45e3c1f76723bb5d3", "type": "github" }, "original": { "owner": "shazow", "repo": "foundry.nix", - "rev": "6089aad0ef615ac8c7b0c948d6052fa848c99523", + "rev": "47f8ae49275eeff9bf0526d45e3c1f76723bb5d3", "type": "github" } }, - "hevmUpstream": { + "hevm": { "inputs": { - "cabal-3-12": "cabal-3-12", "ethereum-tests": "ethereum-tests", - "flake-compat": "flake-compat", "flake-utils": "flake-utils_2", "forge-std": "forge-std", "foundry": "foundry", @@ -170,17 +135,17 @@ "solidity": "solidity" }, "locked": { - "lastModified": 1724425154, - "narHash": "sha256-qW2ulOxIWE6EzYoQp0tJhVxav4CyrEBx//qDxxi6bao=", + "lastModified": 1729608902, + "narHash": "sha256-6uTYwVYGGyVUdIcejP5shHdIzF/jp4XPz3kpDKN8FJ4=", "owner": "ethereum", "repo": "hevm", - "rev": "6f87c03094b6c67a678d15e9b6e6bcf49bdb2186", + "rev": "56d106e529162eda66253d4203dd4a39429317de", "type": "github" }, "original": { "owner": "ethereum", + "ref": "dynamic-flake-output", "repo": "hevm", - "rev": "6f87c03094b6c67a678d15e9b6e6bcf49bdb2186", "type": "github" } }, @@ -200,11 +165,11 @@ }, "nixpkgs_2": { "locked": { - "lastModified": 1724015816, - "narHash": "sha256-hVESnM7Eiz93+4DeiE0a1TwMeaeph1ytRJ5QtqxYRWg=", + "lastModified": 1726481836, + "narHash": "sha256-MWTBH4dd5zIz2iatDb8IkqSjIeFum9jAqkFxgHLdzO4=", "owner": "nixos", "repo": "nixpkgs", - "rev": "9aa35efbea27d320d0cdc5f922f0890812affb60", + "rev": "20f9370d5f588fb8c72e844c54511cab054b5f40", "type": "github" }, "original": { @@ -217,7 +182,7 @@ "root": { "inputs": { "flake-utils": "flake-utils", - "hevmUpstream": "hevmUpstream", + "hevm": "hevm", "nixpkgs": "nixpkgs_2" } }, @@ -237,17 +202,17 @@ "inputs": { "flake-utils": "flake-utils_4", "nixpkgs": [ - "hevmUpstream", + "hevm", "nixpkgs" ], "solc-macos-amd64-list-json": "solc-macos-amd64-list-json" }, "locked": { - "lastModified": 1717442267, - "narHash": "sha256-6TnQvA6Q/xC3r1M+wGC5gnDc/5XfOPjC8X6LlGDWDNc=", + "lastModified": 1724145339, + "narHash": "sha256-z8pLkpdsAA0At1ofQd6KNmrxpBuUT9OKTlCDqJDW1GI=", "owner": "hellwolf", "repo": "solc.nix", - "rev": "2ac2862f224aa0d67cbc6b3246392489f8a50596", + "rev": "9630767051bfefd552c6858c5df141368338b077", "type": "github" }, "original": { @@ -259,17 +224,17 @@ "solidity": { "flake": false, "locked": { - "lastModified": 1670421565, - "narHash": "sha256-VCZDKQHnMsXu+ucsT5BLPYQoZ2FYjpyGbDVoDYjr1W8=", + "lastModified": 1716280767, + "narHash": "sha256-cvRFeJkiaYPA+SoboEZhvH5sHDmmcMNR62OoKuEOWRg=", "owner": "ethereum", "repo": "solidity", - "rev": "1c8745c54a239d20b6fb0f79a8bd2628d779b27e", + "rev": "8a97fa7a1db1ec509221ead6fea6802c684ee887", "type": "github" }, "original": { "owner": "ethereum", "repo": "solidity", - "rev": "1c8745c54a239d20b6fb0f79a8bd2628d779b27e", + "rev": "8a97fa7a1db1ec509221ead6fea6802c684ee887", "type": "github" } }, @@ -321,4 +286,4 @@ }, "root": "root", "version": 7 -} +} \ No newline at end of file diff --git a/flake.nix b/flake.nix index 898ea814..6adc8f7d 100644 --- a/flake.nix +++ b/flake.nix @@ -4,23 +4,23 @@ inputs = { flake-utils.url = "github:numtide/flake-utils"; nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; - hevmUpstream = { - url = "github:ethereum/hevm/6f87c03094b6c67a678d15e9b6e6bcf49bdb2186"; + hevm = { + url = "github:ethereum/hevm/dynamic-flake-output"; inputs.nixpkgs.follows = "nixpkgs"; }; }; - outputs = { self, nixpkgs, flake-utils, hevmUpstream, ... }: + outputs = { nixpkgs, flake-utils, hevm, ... }: flake-utils.lib.eachDefaultSystem (system: let pkgs = nixpkgs.legacyPackages.${system}; gitignore = pkgs.nix-gitignore.gitignoreSourcePure [ ./.gitignore ]; - myHaskellPackages = pkgs.haskellPackages.override { - overrides = self: super: rec { - hevm = hevmUpstream.packages.${system}.noTests; + hspkgs = pkgs.haskellPackages.override { + overrides = self: super: { + hevm = hevm.packages.${system}.unwrapped; }; }; - act = (myHaskellPackages.callCabal2nixWithOptions "act" (gitignore ./.) "-fci" {}) + act = (hspkgs.callCabal2nixWithOptions "act" (gitignore ./.) "-fci" {}) .overrideAttrs (attrs : { buildInputs = attrs.buildInputs ++ [ pkgs.z3 pkgs.cvc5 pkgs.solc ]; }); @@ -31,13 +31,13 @@ apps.act = flake-utils.lib.mkApp { drv = packages.act; }; apps.default = apps.act; - devShell = with pkgs; - let libraryPath = "${lib.makeLibraryPath [ libff secp256k1 gmp ]}"; - in myHaskellPackages.shellFor { + devShell = let + libraryPath = "${pkgs.lib.makeLibraryPath (with pkgs; [ libff secp256k1 gmp ])}"; + in hspkgs.shellFor { packages = _: [ act ]; - buildInputs = with pkgs.haskellPackages; [ - cabal-install - haskell-language-server + buildInputs = [ + hspkgs.cabal-install + hspkgs.haskell-language-server pkgs.jq pkgs.z3 pkgs.cvc5 @@ -54,7 +54,7 @@ export PATH=$(pwd)/bin:$PATH export DYLD_LIBRARY_PATH="${libraryPath}" ''; - }; - } + }; + } ); } \ No newline at end of file diff --git a/funding.json b/funding.json new file mode 100644 index 00000000..9b8c389d --- /dev/null +++ b/funding.json @@ -0,0 +1,5 @@ +{ + "opRetro": { + "projectId": "0x2704cd27b8c60b098d4fe8c5c0fbae2f8f5fe9067c687c501a4c6dc6e9887876" + } +} diff --git a/src/Act/CLI.hs b/src/Act/CLI.hs index a5eefab0..965adec3 100644 --- a/src/Act/CLI.hs +++ b/src/Act/CLI.hs @@ -221,7 +221,7 @@ coq' f solver' smttimeout' debug' = do decompile' :: FilePath -> Text -> Solvers.Solver -> Maybe Integer -> Bool -> IO () decompile' solFile' cid solver' timeout debug' = do let config = if debug' then debugActConfig else defaultActConfig - cores <- liftM fromIntegral getNumProcessors + cores <- fmap fromIntegral getNumProcessors json <- solc Solidity =<< TIO.readFile solFile' let (Contracts contracts, _, _) = fromJust $ readStdJSON json case Map.lookup ("hevm.sol:" <> cid) contracts of @@ -229,7 +229,7 @@ decompile' solFile' cid solver' timeout debug' = do putStrLn "compilation failed" exitFailure Just c -> do - res <- runEnv (Env config) $ Solvers.withSolvers solver' cores (naturalFromInteger <$> timeout) $ \solvers -> decompile c solvers + res <- runEnv (Env config) $ Solvers.withSolvers solver' cores 1 (naturalFromInteger <$> timeout) $ \solvers -> decompile c solvers case res of Left e -> do TIO.putStrLn e @@ -245,7 +245,7 @@ hevm actspec sol' code' initcode' solver' timeout debug' = do specContents <- readFile actspec proceed specContents (enrich <$> compile specContents) $ \ (Act store contracts) -> do cmap <- createContractMap contracts - res <- runEnv (Env config) $ Solvers.withSolvers solver' cores (naturalFromInteger <$> timeout) $ \solvers -> + res <- runEnv (Env config) $ Solvers.withSolvers solver' cores 1 (naturalFromInteger <$> timeout) $ \solvers -> checkContracts solvers store cmap case res of Success _ -> pure () diff --git a/src/Act/Decompile.hs b/src/Act/Decompile.hs index 4c30d2d4..42b662d5 100644 --- a/src/Act/Decompile.hs +++ b/src/Act/Decompile.hs @@ -149,7 +149,7 @@ summarize solvers contract = do makeIntSafe :: forall m a. App m => SolverGroup -> EVM.Expr a -> m (EVM.Expr a) makeIntSafe solvers expr = evalStateT (mapExprM go expr) mempty where - -- Walks the expression bottom up and checks (using an smt solver) if overflow is possible for any + -- Walks the expression bottom up and checks (using an smt solver) if overflow is possible for any -- arithmetic operations it encounters. Results from child nodes are stored and reused as we move up the tree go :: forall b. EVM.Expr b -> StateT (Map (EVM.Expr EVM.EWord) EVM.Prop) m (EVM.Expr b) go = \case @@ -225,11 +225,11 @@ mkConstructor cs where addDefaults :: Map (Integer, Integer) (Text, SlotType) -> DistinctStore -> DistinctStore - addDefaults layout (DistinctStore storage) = + addDefaults layout (DistinctStore storage) = DistinctStore $ Map.foldr (\(name, typ) s -> case Map.lookup name storage of Just _ -> s Nothing -> Map.insert name (LitInt nowhere 0, typ) s) storage layout - + -- | Build behaviour specs from the summarized bytecode mkBehvs :: EVMContract -> Either Text [Behaviour] mkBehvs c = concatMapM (\(i, bs) -> mapM (mkbehv i) (Set.toList bs)) (Map.toList c.runtime) @@ -309,7 +309,7 @@ decomposeStorage layout = go mempty checkedInsert :: (Map Text (Exp AInteger, SlotType)) -> (EVM.W256, EVM.Expr EVM.EWord) -> Either Text (Map Text (Exp AInteger, SlotType)) checkedInsert curr (key, val) = case Map.lookup (toInteger key, 0) layout of - Just (name, typ) -> + Just (name, typ) -> case Map.lookup name curr of -- if a key was already written to higher in the write chain, ignore this write Just _ -> pure curr @@ -328,6 +328,9 @@ simplify e = if (mapTerm go e == e) go (Neg _ (Neg _ p)) = p go (Eq _ SInteger (ITE _ a (LitInt _ 1) (LitInt _ 0)) (LitInt _ 1)) = go a go (Eq _ SInteger (ITE _ a (LitInt _ 1) (LitInt _ 0)) (LitInt _ 0)) = go (Neg nowhere (go a)) + go (Eq _ SInteger (LitInt _ 1) (ITE _ a (LitInt _ 1) (LitInt _ 0))) = go a + go (Eq _ SInteger (LitInt _ 0) (ITE _ a (LitInt _ 1) (LitInt _ 0))) = go (Neg nowhere (go a)) + -- TODO perhaps normalize before simplification to make rewrites less verbose and more robust -- this is the condition we get for a non overflowing uint multiplication -- ~ ((x != 0) & ~ (in_range 256 x)) diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs index f6320384..9efa5dc6 100644 --- a/src/Act/HEVM.hs +++ b/src/Act/HEVM.hs @@ -73,7 +73,7 @@ type ContractMap = M.Map (EVM.Expr EVM.EAddr) (EVM.Expr EVM.EContract, Id) -- when we encounter a constructor call. type CodeMap = M.Map Id (Contract, BS.ByteString, BS.ByteString) -type EquivResult = ProofResult () (T.Text, SMTCex) () +type EquivResult = ProofResult () (T.Text, SMTCex) T.Text T.Text initAddr :: EVM.Expr EVM.EAddr initAddr = EVM.SymAddr "entrypoint" @@ -155,11 +155,11 @@ translateConstructor bytecode (Constructor cid iface _ preconds _ _ upds) cmap = calldata = makeCtrCalldata iface initcontract = EVM.C { EVM.code = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode) , EVM.storage = EVM.ConcreteStore mempty + , EVM.tStorage = EVM.ConcreteStore mempty , EVM.balance = EVM.Lit 0 , EVM.nonce = Just 1 } - symAddrCnstr :: Int -> Int -> [EVM.Prop] symAddrCnstr start end = fmap (\i -> EVM.PNeg (EVM.PEq (EVM.WAddr (EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show i))) (EVM.Lit 0))) [start..end] @@ -228,12 +228,12 @@ applyUpdate readMap writeMap (Update typ (Item _ _ ref) e) = do -- isContract _ = False updateStorage :: (EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage) -> EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract - updateStorage updfun (EVM.C code storage bal nonce) = EVM.C code (updfun storage) bal nonce + updateStorage updfun (EVM.C code storage tstorage bal nonce) = EVM.C code (updfun storage) tstorage bal nonce updateStorage _ (EVM.GVar _) = error "Internal error: contract cannot be a global variable" updateNonce :: EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract - updateNonce (EVM.C code storage bal (Just n)) = EVM.C code storage bal (Just (n + 1)) - updateNonce c@(EVM.C _ _ _ Nothing) = c + updateNonce (EVM.C code storage tstorage bal (Just n)) = EVM.C code storage tstorage bal (Just (n + 1)) + updateNonce c@(EVM.C _ _ _ _ Nothing) = c updateNonce (EVM.GVar _) = error "Internal error: contract cannot be a global variable" createContract :: Monad m => ContractMap -> ContractMap -> EVM.Expr EVM.EAddr -> Exp AInteger -> ActT m ContractMap @@ -243,6 +243,7 @@ createContract readMap writeMap freshAddr (Create _ cid args) = do Just (Contract (Constructor _ iface _ _ _ _ upds) _, _, bytecode) -> do let contract = EVM.C { EVM.code = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode) , EVM.storage = EVM.ConcreteStore mempty + , EVM.tStorage = EVM.ConcreteStore mempty , EVM.balance = EVM.Lit 0 , EVM.nonce = Just 1 } @@ -567,7 +568,7 @@ toExpr cmap = liftM stripMods . go caddr' <- baseAddr cmap ref let (contract, _) = fromMaybe (error "Internal error: contract not found") $ M.lookup caddr' cmap let storage = case contract of - EVM.C _ s _ _ -> s + EVM.C _ s _ _ _ -> s EVM.GVar _ -> error "Internal error: contract cannot be a global variable" pure $ EVM.SLoad slot storage @@ -647,7 +648,8 @@ checkEquiv solvers l1 l2 = do toEquivRes :: SymExec.EquivResult -> EquivResult toEquivRes (Cex cex) = Cex ("\x1b[1mThe following input results in different behaviours\x1b[m", cex) toEquivRes (Qed a) = Qed a - toEquivRes (Timeout b) = Timeout b + toEquivRes (SymExec.Unknown ()) = SymExec.Unknown "" + toEquivRes (SymExec.Error b) = SymExec.Error (T.pack b) -- | Create the initial contract state before analysing a contract @@ -761,9 +763,10 @@ translateCmap :: ContractMap -> [(EVM.Expr EVM.EAddr, EVM.Contract)] translateCmap cmap = (\(addr, (c, _)) -> (addr, toContract c)) <$> M.toList cmap where toContract :: EVM.Expr EVM.EContract -> EVM.Contract - toContract (EVM.C code storage balance nonce) = EVM.Contract + toContract (EVM.C code storage tstorage balance nonce) = EVM.Contract { EVM.code = code , EVM.storage = storage + , EVM.tStorage = tstorage , EVM.origStorage = storage , EVM.balance = balance , EVM.nonce = nonce @@ -991,18 +994,18 @@ assertSelector txdata sig = toVRes :: T.Text -> CheckSatResult -> EquivResult toVRes msg res = case res of Sat cex -> Cex (msg, cex) - EVM.Solvers.Unknown -> Timeout () + EVM.Solvers.Unknown e -> SymExec.Unknown (T.pack e) Unsat -> Qed () - Error e -> error $ "Internal Error: solver responded with error: " <> show e + EVM.Solvers.Error e -> SymExec.Error (T.pack e) checkResult :: App m => Calldata -> Maybe Sig -> [EquivResult] -> m (Error String ()) checkResult calldata sig res = case any isCex res of False -> - case any isTimeout res of + case any isUnknown res || any isError res of True -> do - showMsg "\x1b[41mNo discrepancies found but timeout(s) occurred. \x1b[m" + showMsg "\x1b[41mNo discrepancies found but timeouts or solver errors were encountered. \x1b[m" pure $ Failure $ NE.singleton (nowhere, "Failure: Cannot prove equivalence.") False -> do showMsg "\x1b[42mNo discrepancies found.\x1b[m " diff --git a/src/Act/HEVM_utils.hs b/src/Act/HEVM_utils.hs index 412dd204..0862df30 100644 --- a/src/Act/HEVM_utils.hs +++ b/src/Act/HEVM_utils.hs @@ -188,4 +188,5 @@ loadSymVM (entryaddr, entrycontract) othercontracts callvalue cd create fresh = , txAccessList = mempty , allowFFI = False , freshAddresses = fresh + , beaconRoot = 0 }) diff --git a/src/Act/Print.hs b/src/Act/Print.hs index 49c7d9ea..6ad684e5 100644 --- a/src/Act/Print.hs +++ b/src/Act/Print.hs @@ -251,6 +251,10 @@ prettyInvPred = prettyExp . untime . fst Var p _ at vt a -> Var p Neither at vt (untimeVarRef a) +-- | Doc type for terminal output +type DocAnsi = Doc Term.AnsiStyle + + -- | Doc type for terminal output type DocAnsi = Doc Term.AnsiStyle diff --git a/src/Test/Decompile.hs b/src/Test/Decompile.hs index 53a0e73d..668cc74f 100644 --- a/src/Test/Decompile.hs +++ b/src/Test/Decompile.hs @@ -109,7 +109,7 @@ checkDecompilation contract src = do json <- solc Solidity src let (Contracts sol, _, _) = fromJust $ readStdJSON json let c = fromJust $ Map.lookup ("hevm.sol:" <> contract) sol - runEnv (Env defaultActConfig) (Solvers.withSolvers CVC5 1 (Just 100000000) (decompile c)) >>= \case + runEnv (Env defaultActConfig) (Solvers.withSolvers CVC5 1 1 (Just 100000000) (decompile c)) >>= \case Left es -> do T.putStrLn es assertBool "decompilation should succeed" False diff --git a/src/Test/Main.hs b/src/Test/Main.hs index 91f1b1b2..d43bf539 100644 --- a/src/Test/Main.hs +++ b/src/Test/Main.hs @@ -11,7 +11,6 @@ import Test.Tasty.QuickCheck (Gen, arbitrary, testProperty, Property, (===), cou import Test.QuickCheck.Instances.ByteString() import Test.QuickCheck.GenT import Test.QuickCheck.Monadic -import Text.PrettyPrint.ANSI.Leijen (pretty) import Control.Monad import Control.Monad.Trans @@ -90,7 +89,7 @@ typeCheckSMT solver = do solverInstance <- spawnSolver smtconf all isNothing <$> mapM (askSMT solverInstance) queries - askSMT solverInstance query = sendLines solverInstance ("(reset)" : (lines . show . pretty . getSMT $ query)) + askSMT solverInstance query = sendLines solverInstance ("(reset)" : (lines . show . getSMT $ query)) -- *** QuickCheck Generators *** --