From 206a9b28290135ea7f3617d6c15f2c515bc1ff00 Mon Sep 17 00:00:00 2001 From: Zoe Paraskevopoulou Date: Mon, 26 Aug 2024 12:52:12 +0300 Subject: [PATCH 1/3] Create funding.json (#187) --- funding.json | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 funding.json 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" + } +} From 151d988c56378497fa993752b10521b609c647f0 Mon Sep 17 00:00:00 2001 From: Zoe Paraskevopoulou Date: Wed, 23 Oct 2024 17:30:30 +0300 Subject: [PATCH 2/3] Bump nixpkgs (#185) * WIP in compiling Act * Act compiling * Nits * Fix compilation error * bump flake * hevm update * nit * Fix in decompiler simplification * flake: use dynamic hevm output --------- Co-authored-by: dxo --- act.cabal | 2 + flake.lock | 181 +++++++++++++++++++++++------------------ flake.nix | 32 ++++---- src/Act/CLI.hs | 28 +++---- src/Act/Consistency.hs | 8 +- src/Act/Decompile.hs | 11 ++- src/Act/HEVM.hs | 34 ++++---- src/Act/HEVM_utils.hs | 2 + src/Act/Print.hs | 44 +++++++++- src/Act/SMT.hs | 72 ++++++++-------- src/Act/Type.hs | 4 +- src/Test/Decompile.hs | 2 +- src/Test/Main.hs | 3 +- 13 files changed, 245 insertions(+), 178 deletions(-) diff --git a/act.cabal b/act.cabal index 3e40ee57..ee8341bc 100644 --- a/act.cabal +++ b/act.cabal @@ -40,6 +40,8 @@ common common deriving-compat, async >= 2.2.4, data-dword >= 0.3.2.1, + prettyprinter, + prettyprinter-ansi-terminal, if flag(ci) ghc-options: -O2 -Wall -Werror -Wno-orphans -Wno-unticked-promoted-constructors else diff --git a/flake.lock b/flake.lock index a27e3f13..71a08634 100644 --- a/flake.lock +++ b/flake.lock @@ -1,80 +1,32 @@ { "nodes": { - "bitwuzla-pkgs": { - "locked": { - "lastModified": 1705518710, - "narHash": "sha256-4AV1Q3YEYakWcsu3nSX3U0hXZAcir0maGFrG5sEU/Kk=", - "owner": "d-xo", - "repo": "nixpkgs", - "rev": "94e802bce3a1bc05b3acfc5e876de15fd2ecb564", - "type": "github" - }, - "original": { - "owner": "d-xo", - "repo": "nixpkgs", - "rev": "94e802bce3a1bc05b3acfc5e876de15fd2ecb564", - "type": "github" - } - }, - "cabal-head": { - "flake": false, - "locked": { - "lastModified": 1693777827, - "narHash": "sha256-zMwVwTztoQGrNIJSxSdVJjYN77rleRjpC+K5AoIl7po=", - "owner": "haskell", - "repo": "cabal", - "rev": "24a4603eebfcf7730f00bb69a02d1568990798d5", - "type": "github" - }, - "original": { - "owner": "haskell", - "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": 1673956053, - "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", - "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": { @@ -88,11 +40,11 @@ "systems": "systems_2" }, "locked": { - "lastModified": 1692799911, - "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=", + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", "type": "github" }, "original": { @@ -116,14 +68,32 @@ "type": "github" } }, + "flake-utils_4": { + "inputs": { + "systems": "systems_3" + }, + "locked": { + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, "forge-std": { "flake": false, "locked": { - "lastModified": 1702656582, - "narHash": "sha256-qDC/3x/CfeghsqftBJme4IlNGDG7YgV9cx8I5tc30KA=", + "lastModified": 1715903882, + "narHash": "sha256-Uqr0ZwCnQL9ShWxIgG/ci/5ukGyuqt2n+C0GFKlJiho=", "owner": "foundry-rs", "repo": "forge-std", - "rev": "155d547c449afa8715f538d69454b83944117811", + "rev": "52715a217dc51d0de15877878ab8213f6cbbbab5", "type": "github" }, "original": { @@ -138,44 +108,43 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1691140388, - "narHash": "sha256-AH3fx2VFGPRSOjnuakab4T4AdUstwTnFTbnkoU4df8Q=", + "lastModified": 1724145005, + "narHash": "sha256-fTvalF9fSKWJj/HJWtHQ8DrMR1nBH1NV1w/x+O4M/Zw=", "owner": "shazow", "repo": "foundry.nix", - "rev": "6089aad0ef615ac8c7b0c948d6052fa848c99523", + "rev": "47f8ae49275eeff9bf0526d45e3c1f76723bb5d3", "type": "github" }, "original": { "owner": "shazow", - "ref": "monthly", "repo": "foundry.nix", + "rev": "47f8ae49275eeff9bf0526d45e3c1f76723bb5d3", "type": "github" } }, - "hevmUpstream": { + "hevm": { "inputs": { - "bitwuzla-pkgs": "bitwuzla-pkgs", - "cabal-head": "cabal-head", "ethereum-tests": "ethereum-tests", - "flake-compat": "flake-compat", "flake-utils": "flake-utils_2", "forge-std": "forge-std", "foundry": "foundry", "nixpkgs": [ "nixpkgs" ], + "solc-pkgs": "solc-pkgs", "solidity": "solidity" }, "locked": { - "lastModified": 1712067908, - "narHash": "sha256-gh+dCwIbxAK7ICDFF5gdajgAlP2gnrT3yFnIx+qG6tY=", + "lastModified": 1729608902, + "narHash": "sha256-6uTYwVYGGyVUdIcejP5shHdIzF/jp4XPz3kpDKN8FJ4=", "owner": "ethereum", "repo": "hevm", - "rev": "072864345e0dad26028184ecadd23f4f1ac8c89b", + "rev": "56d106e529162eda66253d4203dd4a39429317de", "type": "github" }, "original": { "owner": "ethereum", + "ref": "dynamic-flake-output", "repo": "hevm", "type": "github" } @@ -196,41 +165,76 @@ }, "nixpkgs_2": { "locked": { - "lastModified": 1698165927, - "narHash": "sha256-XWfxt0Mi2h1EatZ9UKpbC0iXlS7+DupCs2dDl/yENO0=", + "lastModified": 1726481836, + "narHash": "sha256-MWTBH4dd5zIz2iatDb8IkqSjIeFum9jAqkFxgHLdzO4=", "owner": "nixos", "repo": "nixpkgs", - "rev": "f85a3c6af20f02135814867870deb419329e8297", + "rev": "20f9370d5f588fb8c72e844c54511cab054b5f40", "type": "github" }, "original": { "owner": "nixos", + "ref": "nixpkgs-unstable", "repo": "nixpkgs", - "rev": "f85a3c6af20f02135814867870deb419329e8297", "type": "github" } }, "root": { "inputs": { "flake-utils": "flake-utils", - "hevmUpstream": "hevmUpstream", + "hevm": "hevm", "nixpkgs": "nixpkgs_2" } }, + "solc-macos-amd64-list-json": { + "flake": false, + "locked": { + "narHash": "sha256-Prwz95BgMHcWd72VwVbcH17LsV9f24K2QMcUiWUQZzI=", + "type": "file", + "url": "https://github.com/ethereum/solc-bin/raw/f743ca7/macosx-amd64/list.json" + }, + "original": { + "type": "file", + "url": "https://github.com/ethereum/solc-bin/raw/f743ca7/macosx-amd64/list.json" + } + }, + "solc-pkgs": { + "inputs": { + "flake-utils": "flake-utils_4", + "nixpkgs": [ + "hevm", + "nixpkgs" + ], + "solc-macos-amd64-list-json": "solc-macos-amd64-list-json" + }, + "locked": { + "lastModified": 1724145339, + "narHash": "sha256-z8pLkpdsAA0At1ofQd6KNmrxpBuUT9OKTlCDqJDW1GI=", + "owner": "hellwolf", + "repo": "solc.nix", + "rev": "9630767051bfefd552c6858c5df141368338b077", + "type": "github" + }, + "original": { + "owner": "hellwolf", + "repo": "solc.nix", + "type": "github" + } + }, "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" } }, @@ -263,6 +267,21 @@ "repo": "default", "type": "github" } + }, + "systems_3": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", diff --git a/flake.nix b/flake.nix index be1155de..c2159612 100644 --- a/flake.nix +++ b/flake.nix @@ -3,24 +3,24 @@ inputs = { flake-utils.url = "github:numtide/flake-utils"; - nixpkgs.url = "github:nixos/nixpkgs/f85a3c6af20f02135814867870deb419329e8297"; - hevmUpstream = { - url = "github:ethereum/hevm"; + nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; + 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}" ''; - }; - } + }; + } ); } diff --git a/src/Act/CLI.hs b/src/Act/CLI.hs index 56927743..b3a35149 100644 --- a/src/Act/CLI.hs +++ b/src/Act/CLI.hs @@ -23,7 +23,7 @@ import Data.Map (Map) import Data.Maybe import qualified Data.Text as Text import qualified Data.Text.IO as TIO -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) +import Prettyprinter hiding (annotate, line') import GHC.Conc import GHC.Natural import Options.Generic @@ -154,7 +154,7 @@ parseSolver s = case s of Just s' -> case Text.unpack s' of "z3" -> pure Solvers.Z3 "cvc5" -> pure Solvers.CVC5 - input -> render (text $ "unrecognised solver: " <> input) >> exitFailure + input -> render (text $ "unrecognised solver: " <> Text.pack input) >> exitFailure prove :: FilePath -> Solvers.Solver -> Maybe Integer -> Bool -> IO () prove file' solver' smttimeout' debug' = do @@ -167,27 +167,27 @@ prove file' solver' smttimeout' debug' = do catErrors results = [e | e@SMT.Error {} <- results] catUnknowns results = [u | u@SMT.Unknown {} <- results] - (<->) :: Doc -> [Doc] -> Doc + (<->) :: DocAnsi -> [DocAnsi] -> DocAnsi x <-> y = x <$$> line <> (indent 2 . vsep $ y) - failMsg :: [SMT.SMTResult] -> Doc + failMsg :: [SMT.SMTResult] -> DocAnsi failMsg results | not . null . catUnknowns $ results = text "could not be proven due to a" <+> (yellow . text $ "solver timeout") | not . null . catErrors $ results - = (red . text $ "failed") <+> "due to solver errors:" <-> ((fmap (text . show)) . catErrors $ results) + = (red . text $ "failed") <+> "due to solver errors:" <-> ((fmap viaShow) . catErrors $ results) | otherwise - = (red . text $ "violated") <> colon <-> (fmap pretty . catModels $ results) + = (red . text $ "violated") <> colon <-> (fmap prettyAnsi . catModels $ results) - passMsg :: Doc + passMsg :: DocAnsi passMsg = (green . text $ "holds") <+> (bold . text $ "∎") - accumulateResults :: (Bool, Doc) -> (Query, [SMT.SMTResult]) -> (Bool, Doc) + accumulateResults :: (Bool, DocAnsi) -> (Query, [SMT.SMTResult]) -> (Bool, DocAnsi) accumulateResults (status, report) (query, results) = (status && holds, report <$$> msg <$$> smt) where holds = all isPass results msg = identifier query <+> if holds then passMsg else failMsg results - smt = if debug' then line <> getSMT query else empty + smt = if debug' then line <> getSMT query else emptyDoc solverInstance <- spawnSolver config pcResults <- mapM (runQuery solverInstance) (mkPostconditionQueries claims) @@ -196,10 +196,10 @@ prove file' solver' smttimeout' debug' = do let invTitle = line <> (underline . bold . text $ "Invariants:") <> line - invOutput = foldl' accumulateResults (True, empty) invResults + invOutput = foldl' accumulateResults (True, emptyDoc) invResults pcTitle = line <> (underline . bold . text $ "Postconditions:") <> line - pcOutput = foldl' accumulateResults (True, empty) pcResults + pcOutput = foldl' accumulateResults (True, emptyDoc) pcResults render $ vsep [ ifExists invResults invTitle @@ -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/Consistency.hs b/src/Act/Consistency.hs index 5c588af8..a24f3028 100644 --- a/src/Act/Consistency.hs +++ b/src/Act/Consistency.hs @@ -14,7 +14,7 @@ module Act.Consistency ( import Prelude hiding (GT, LT) import Data.List -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) +import Prettyprinter import System.Exit (exitFailure) import Data.Maybe @@ -109,10 +109,10 @@ checkCases (Act _ contracts) solver' smttimeout debug = do checkRes :: String -> (Id, SMT.SMTResult) -> IO () checkRes check (name, res) = case res of - Sat model -> failMsg ("Cases are not " <> check <> " for behavior " <> name <> ".") (pretty model) + Sat model -> failMsg ("Cases are not " <> check <> " for behavior " <> name <> ".") (prettyAnsi model) Unsat -> pure () Unknown -> errorMsg $ "Solver timeour. Cannot prove that cases are " <> check <> " for behavior " <> name <> "." SMT.Error _ err -> errorMsg $ "Solver error: " <> err <> "\nCannot prove that cases are " <> check <> " for behavior " <> name <> "." - failMsg str model = render (red (text str) <> line <> model <> line) >> exitFailure - errorMsg str = render (text str <> line) >> exitFailure + failMsg str model = render (red (pretty str) <> line <> model <> line) >> exitFailure + errorMsg str = render (pretty str <> line) >> exitFailure diff --git a/src/Act/Decompile.hs b/src/Act/Decompile.hs index 1824a031..8452b1ea 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 @@ -224,11 +224,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) @@ -307,7 +307,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 @@ -326,6 +326,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 e2352959..5f289b3a 100644 --- a/src/Act/HEVM.hs +++ b/src/Act/HEVM.hs @@ -44,7 +44,7 @@ import EVM as EVM hiding (bytecode) import qualified EVM.Types as EVM hiding (FrameState(..)) import EVM.Expr hiding (op2, inRange) import EVM.SymExec hiding (EquivResult, isPartial) -import qualified EVM.SymExec as SymExec (EquivResult) +import qualified EVM.SymExec as SymExec (EquivResult, ProofResult(..)) import EVM.SMT (SMTCex(..), assertProps) import EVM.Solvers import EVM.Effects @@ -66,7 +66,7 @@ type ContractMap = M.Map (EVM.Expr EVM.EAddr) (EVM.Expr EVM.EContract) -- 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" @@ -146,6 +146,7 @@ translateConstructor bytecode (Constructor _ iface preconds _ _ upds) = do 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 } @@ -212,12 +213,12 @@ applyUpdate readMap writeMap (Update typ (Item _ _ ref) e) = do where 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 :: ContractMap -> ContractMap -> EVM.Expr EVM.EAddr -> Exp AContract -> ActM ContractMap @@ -227,6 +228,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 } @@ -369,7 +371,7 @@ refAddr :: ContractMap -> StorageRef -> ActM (EVM.Expr EVM.EAddr) refAddr cmap (SVar _ c x) = do caddr <- getCaddr case M.lookup caddr cmap of - Just (EVM.C _ storage _ _) -> do + Just (EVM.C _ storage _ _ _) -> do layout <- getLayout let slot = EVM.Lit $ fromIntegral $ getSlot layout c x case simplify (EVM.SLoad slot storage) of @@ -381,7 +383,7 @@ refAddr cmap (SField _ ref c x) = do layout <- getLayout caddr' <- refAddr cmap ref case M.lookup caddr' cmap of - Just (EVM.C _ storage _ _) -> do + Just (EVM.C _ storage _ _ _) -> do let slot = EVM.Lit $ fromIntegral $ getSlot layout c x case simplify (EVM.SLoad slot storage) of EVM.WAddr symaddr -> pure symaddr @@ -528,7 +530,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 @@ -584,7 +586,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) checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Store -> Contract -> CodeMap -> m (Error String (ContractMap, ActEnv)) @@ -638,13 +641,14 @@ createStorage cmap = traverseStorage _ _ = error "Internal error: unexpected storage shape" makeContract :: EVM.Expr EVM.EAddr -> EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract - makeContract addr (EVM.C code storage _ _) = EVM.C code (traverseStorage addr storage) (EVM.Balance addr) (Just 0) + makeContract addr (EVM.C code storage tstorage _ _) = EVM.C code (traverseStorage addr storage) tstorage (EVM.Balance addr) (Just 0) makeContract _ (EVM.GVar _) = error "Internal error: contract cannot be gvar" 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 @@ -754,18 +758,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 47f55bab..d6bb0d92 100644 --- a/src/Act/HEVM_utils.hs +++ b/src/Act/HEVM_utils.hs @@ -184,4 +184,6 @@ loadSymVM (entryaddr, entrycontract) othercontracts callvalue cd create = , create = create , txAccessList = mempty , allowFFI = False + , freshAddresses = 0 + , beaconRoot = 0 }) diff --git a/src/Act/Print.hs b/src/Act/Print.hs index e54fd681..3968c3f5 100644 --- a/src/Act/Print.hs +++ b/src/Act/Print.hs @@ -6,14 +6,17 @@ module Act.Print where import Prelude hiding (GT, LT) import Data.ByteString.UTF8 (toString) -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), brackets) +import Prettyprinter hiding (brackets) +import qualified Prettyprinter.Render.Terminal as Term +import qualified Data.Text as Text + import System.IO (stdout) import Data.Text qualified as T import EVM.ABI (abiTypeSolidity) import Data.List -import Act.Syntax.TimeAgnostic +import Act.Syntax.TimeAgnostic hiding (annotate) prettyAct :: Act t -> String prettyAct (Act _ contracts) @@ -226,6 +229,39 @@ prettyInvPred = prettyExp . untime . fst TEntry p _ (Item t vt a) -> TEntry p Neither (Item t vt (untimeStorageRef a)) Var p t at a -> Var p t at a + +-- | Doc type for terminal output +type DocAnsi = Doc Term.AnsiStyle + -- | prints a Doc, with wider output than the built in `putDoc` -render :: Doc -> IO () -render doc = displayIO stdout (renderPretty 0.9 120 doc) +render :: DocAnsi -> IO () +render doc = + let opts = LayoutOptions { layoutPageWidth = AvailablePerLine 120 0.9 } in + Term.renderIO stdout (layoutPretty opts doc) + +underline :: DocAnsi -> DocAnsi +underline = annotate Term.underlined + +red :: DocAnsi -> DocAnsi +red = annotate (Term.color Term.Red) + +yellow :: DocAnsi -> DocAnsi +yellow = annotate (Term.color Term.Yellow) + +green :: DocAnsi -> DocAnsi +green = annotate (Term.color Term.Green) + +bold :: DocAnsi -> DocAnsi +bold = annotate Term.bold + +(<$$>) :: Doc ann -> Doc ann -> Doc ann +(<$$>) = \x y -> vsep [x,y] + +string :: String -> DocAnsi +string = pretty + +text :: Text.Text -> DocAnsi +text = pretty + +class PrettyAnsi a where + prettyAnsi :: a -> DocAnsi diff --git a/src/Act/SMT.hs b/src/Act/SMT.hs index 1d6bbd50..85d51217 100644 --- a/src/Act/SMT.hs +++ b/src/Act/SMT.hs @@ -47,10 +47,11 @@ import Prelude hiding (GT, LT) import Data.Containers.ListUtils (nubOrd) import System.Process (createProcess, cleanupProcess, proc, ProcessHandle, std_in, std_out, std_err, StdStream(..)) import Text.Regex.TDFA hiding (empty) -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) +import Prettyprinter hiding (Doc) import Control.Applicative ((<|>)) import Control.Monad.Reader +import Control.Monad import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.List.NonEmpty as NonEmpty @@ -60,7 +61,7 @@ import GHC.IO.Handle (Handle, hGetLine, hPutStr, hFlush) import Data.ByteString.UTF8 (fromString) import Act.Syntax -import Act.Syntax.Annotated +import Act.Syntax.Annotated hiding (annotate) import Act.Print import Act.Type (defaultStore) @@ -97,13 +98,13 @@ data SMTExp = SMTExp } deriving (Show) -instance Pretty SMTExp where - pretty e = vsep [storage, calldata, environment, assertions] +instance PrettyAnsi SMTExp where + prettyAnsi e = vsep [storage, calldata, environment, assertions] where - storage = text ";STORAGE:" <$$> (vsep . (fmap text) . nubOrd . _storage $ e) <> line - calldata = text ";CALLDATA:" <$$> (vsep . (fmap text) . nubOrd . _calldata $ e) <> line - environment = text ";ENVIRONMENT" <$$> (vsep . (fmap text) . nubOrd . _environment $ e) <> line - assertions = text ";ASSERTIONS:" <$$> (vsep . (fmap text) . nubOrd . _assertions $ e) <> line + storage = pretty ";STORAGE:" <$$> (vsep . (fmap pretty) . nubOrd . _storage $ e) <> line + calldata = pretty ";CALLDATA:" <$$> (vsep . (fmap pretty) . nubOrd . _calldata $ e) <> line + environment = pretty ";ENVIRONMENT" <$$> (vsep . (fmap pretty) . nubOrd . _environment $ e) <> line + assertions = pretty ";ASSERTIONS:" <$$> (vsep . (fmap pretty) . nubOrd . _assertions $ e) <> line data Transition = Behv Behaviour @@ -138,9 +139,9 @@ data Model = Model } deriving (Show) -instance Pretty Model where - pretty (Model prestate poststate (ifaceName, args) environment initargs) = - (underline . text $ "counterexample:") <$$> line +instance PrettyAnsi Model where + prettyAnsi (Model prestate poststate (ifaceName, args) environment initargs) = + (underline . pretty $ "counterexample:") <$$> line <> (indent 2 ( calldata' <$$> ifExists environment (line <> environment' <> line) @@ -148,18 +149,19 @@ instance Pretty Model where <$$> ifExists initargs (line <> initargs') )) where - calldata' = text "calldata:" <$$> line <> (indent 2 $ formatSig ifaceName args) - environment' = text "environment:" <$$> line <> (indent 2 . vsep $ fmap formatEnvironment environment) - storage = text "storage:" <$$> (indent 2 . vsep $ [ifExists prestate (line <> prestate'), poststate']) - initargs' = text "constructor arguments:" <$$> line <> (indent 2 $ formatSig "constructor" initargs) + calldata' = pretty "calldata:" <$$> line <> (indent 2 $ formatSig ifaceName args) + environment' = pretty "environment:" <$$> line <> (indent 2 . vsep $ fmap formatEnvironment environment) + storage = pretty "storage:" <$$> (indent 2 . vsep $ [ifExists prestate (line <> prestate'), poststate']) + initargs' = pretty "constructor arguments:" <$$> line <> (indent 2 $ formatSig "constructor" initargs) - prestate' = text "prestate:" <$$> line <> (indent 2 . vsep $ fmap formatStorage prestate) <> line - poststate' = text "poststate:" <$$> line <> (indent 2 . vsep $ fmap formatStorage poststate) + prestate' = pretty "prestate:" <$$> line <> (indent 2 . vsep $ fmap formatStorage prestate) <> line + poststate' = pretty "poststate:" <$$> line <> (indent 2 . vsep $ fmap formatStorage poststate) + + formatSig iface cd = pretty iface <> (encloseSep lparen rparen (pretty ", ") $ fmap formatCalldata cd) + formatCalldata (Decl _ name, val) = pretty $ name <> " = " <> prettyTypedExp val + formatEnvironment (env, val) = pretty $ prettyEnv env <> " = " <> prettyTypedExp val + formatStorage (loc, val) = pretty $ prettyLocation loc <> " = " <> prettyTypedExp val - formatSig iface cd = text iface <> (encloseSep lparen rparen (text ", ") $ fmap formatCalldata cd) - formatCalldata (Decl _ name, val) = text $ name <> " = " <> prettyTypedExp val - formatEnvironment (env, val) = text $ prettyEnv env <> " = " <> prettyTypedExp val - formatStorage (loc, val) = text $ prettyLocation loc <> " = " <> prettyTypedExp val data SolverInstance = SolverInstance { _type :: Solver @@ -333,7 +335,7 @@ runQuery solver query@(Inv (Invariant _ _ _ predicate) (ctor, ctorSMT) behvs) = checkSat :: SolverInstance -> (SolverInstance -> IO Model) -> SMTExp -> IO SMTResult checkSat solver modelFn smt = do -- render (pretty smt) - err <- sendLines solver ("(reset)" : (lines . show . pretty $ smt)) + err <- sendLines solver ("(reset)" : (lines . show . prettyAnsi $ smt)) case err of Nothing -> do sat <- sendCommand solver "(check-sat)" @@ -729,21 +731,21 @@ isFail _ = True isPass :: SMTResult -> Bool isPass = not . isFail -getBehvName :: Query -> Doc -getBehvName (Postcondition (Ctor _) _ _) = (text "the") <+> (bold . text $ "constructor") -getBehvName (Postcondition (Behv behv) _ _) = (text "behaviour") <+> (bold . text $ _name behv) +getBehvName :: Query -> DocAnsi +getBehvName (Postcondition (Ctor _) _ _) = (pretty "the") <+> (bold . pretty $ "constructor") +getBehvName (Postcondition (Behv behv) _ _) = (pretty "behaviour") <+> (bold . pretty $ _name behv) getBehvName (Inv {}) = error "Internal Error: invariant queries do not have an associated behaviour" -identifier :: Query -> Doc -identifier q@(Inv (Invariant _ _ _ e) _ _) = (bold . text . prettyInvPred $ e) <+> text "of" <+> (bold . text . getQueryContract $ q) -identifier q@Postcondition {} = (bold . text . prettyExp . target $ q) <+> text "in" <+> getBehvName q <+> text "of" <+> (bold . text . getQueryContract $ q) +identifier :: Query -> DocAnsi +identifier q@(Inv (Invariant _ _ _ e) _ _) = (bold . pretty . prettyInvPred $ e) <+> pretty "of" <+> (bold . pretty . getQueryContract $ q) +identifier q@Postcondition {} = (bold . pretty . prettyExp . target $ q) <+> pretty "in" <+> getBehvName q <+> pretty "of" <+> (bold . pretty . getQueryContract $ q) -getSMT :: Query -> Doc -getSMT (Postcondition _ _ smt) = pretty smt -getSMT (Inv _ (_, csmt) behvs) = text "; constructor" <$$> sep' <$$> line <> pretty csmt <$$> vsep (fmap formatBehv behvs) +getSMT :: Query -> DocAnsi +getSMT (Postcondition _ _ smt) = prettyAnsi smt +getSMT (Inv _ (_, csmt) behvs) = pretty "; constructor" <$$> sep' <$$> line <> prettyAnsi csmt <$$> vsep (fmap formatBehv behvs) where - formatBehv (b, smt) = line <> text "; behaviour: " <> (text . _name $ b) <$$> sep' <$$> line <> pretty smt - sep' = text "; -------------------------------" + formatBehv (b, smt) = line <> pretty "; behaviour: " <> (pretty . _name $ b) <$$> sep' <$$> line <> prettyAnsi smt + sep' = pretty "; -------------------------------" -ifExists :: Foldable t => t a -> Doc -> Doc -ifExists a b = if null a then empty else b +ifExists :: Foldable t => t a -> DocAnsi -> DocAnsi +ifExists a b = if null a then emptyDoc else b diff --git a/src/Act/Type.hs b/src/Act/Type.hs index b910f8a1..46b6ae62 100644 --- a/src/Act/Type.hs +++ b/src/Act/Type.hs @@ -22,7 +22,7 @@ import qualified Data.Map.Strict as Map -- abandon in favor of [(a,b)]? import Data.Typeable hiding (typeRep) import Type.Reflection (typeRep) -import Control.Monad.Writer +import Control.Monad (when) import Data.List.Extra (snoc,unsnoc) import Data.Function (on) import Data.Foldable @@ -227,7 +227,7 @@ checkTransition env (U.Transition _ name contract iface@(Interface _ decls) iffs noIllegalWilds = case cases of U.Direct _ -> pure () U.Branches bs -> for_ (init bs) $ \c@(U.Case p _ _) -> - when (isWild c) (throw (p, "Wildcard pattern must be last case")) -- TODO test when wildcard isn't last + ((when (isWild c) ((throw (p, "Wildcard pattern must be last case")):: Err ())) :: Err ()) -- TODO test when wildcard isn't last -- translate wildcards into negation of other branches and translate a single case to a wildcard normalizedCases :: [U.Case] 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 *** -- From 530160debb2289c8bbc3a7bfc6e97feb1dd2cc50 Mon Sep 17 00:00:00 2001 From: Zoe Paraskevopoulou Date: Sun, 27 Oct 2024 10:25:55 +0200 Subject: [PATCH 3/3] Pass fresh address counter to `makeVM` (#186) * WIP in compiling Act * Act compiling * Nits * Thread fresh address to hevm * WIP fresh addresses * Fix fresh address bug * Add new tests * Fix merge error --- flake.lock | 2 +- flake.nix | 2 +- src/Act/HEVM.hs | 21 ++++++++---- src/Act/HEVM_utils.hs | 29 +++++++++-------- tests/hevm/pass/multi4/multi4.act | 53 +++++++++++++++++++++++++++++++ tests/hevm/pass/multi4/multi4.sol | 25 +++++++++++++++ 6 files changed, 109 insertions(+), 23 deletions(-) create mode 100644 tests/hevm/pass/multi4/multi4.act create mode 100644 tests/hevm/pass/multi4/multi4.sol diff --git a/flake.lock b/flake.lock index 71a08634..20a0b889 100644 --- a/flake.lock +++ b/flake.lock @@ -286,4 +286,4 @@ }, "root": "root", "version": 7 -} +} \ No newline at end of file diff --git a/flake.nix b/flake.nix index c2159612..6adc8f7d 100644 --- a/flake.nix +++ b/flake.nix @@ -57,4 +57,4 @@ }; } ); -} +} \ No newline at end of file diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs index 5f289b3a..9c4a9c64 100644 --- a/src/Act/HEVM.hs +++ b/src/Act/HEVM.hs @@ -141,7 +141,7 @@ translateConstructor bytecode (Constructor _ iface preconds _ _ upds) = do preconds' <- mapM (toProp initmap) preconds cmap <- applyUpdates initmap initmap upds fresh <- getFresh - pure $ ([EVM.Success (snd calldata <> preconds' <> symAddrCnstr fresh) mempty (EVM.ConcreteBuf bytecode) cmap], calldata, ifaceToSig iface) + pure $ ([EVM.Success (snd calldata <> preconds' <> symAddrCnstr 1 fresh) mempty (EVM.ConcreteBuf bytecode) cmap], calldata, ifaceToSig iface) where calldata = makeCtrCalldata iface initcontract = EVM.C { EVM.code = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode) @@ -152,8 +152,9 @@ translateConstructor bytecode (Constructor _ iface preconds _ _ upds) = do } initmap = M.fromList [(initAddr, initcontract)] - -- TODO remove when hevm PR is merged - symAddrCnstr n = fmap (\i -> EVM.PNeg (EVM.PEq (EVM.WAddr (EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show i))) (EVM.Lit 0))) [1..n] + +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] translateBehvs :: ContractMap -> [Behaviour] -> ActM [(Id, [EVM.Expr EVM.End], Calldata, Sig)] translateBehvs cmap behvs = do @@ -182,11 +183,13 @@ ifaceToSig (Interface name args) = Sig (T.pack name) (fmap fromdecl args) translateBehv :: ContractMap -> Behaviour -> ActM (EVM.Expr EVM.End) translateBehv cmap (Behaviour _ _ _ preconds caseconds _ upds ret) = do + fresh <- getFresh preconds' <- mapM (toProp cmap) preconds caseconds' <- mapM (toProp cmap) caseconds ret' <- returnsToExpr cmap ret store <- applyUpdates cmap cmap upds - pure $ EVM.Success (preconds' <> caseconds') mempty ret' store + fresh' <- getFresh + pure $ EVM.Success (preconds' <> caseconds' <> symAddrCnstr (fresh+1) fresh') mempty ret' store applyUpdates :: ContractMap -> ContractMap -> [StorageUpdate] -> ActM ContractMap @@ -594,7 +597,7 @@ checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Store - checkConstructors solvers initcode runtimecode store (Contract ctor _) codemap = do let actenv = ActEnv codemap 0 (slotMap store) (EVM.SymAddr "entrypoint") Nothing let ((actbehvs, calldata, sig), actenv') = flip runState actenv $ translateConstructor runtimecode ctor - solbehvs <- removeFails <$> getInitcodeBranches solvers initcode calldata + solbehvs <- removeFails <$> getInitcodeBranches solvers initcode calldata 0 showMsg "\x1b[1mChecking if constructor results are equivalent.\x1b[m" res1 <- checkResult calldata (Just sig) =<< checkEquiv solvers solbehvs actbehvs showMsg "\x1b[1mChecking if constructor input spaces are the same.\x1b[m" @@ -612,7 +615,7 @@ checkBehaviours solvers (Contract _ behvs) actenv cmap = do let (actstorage, hevmstorage) = createStorage cmap let actbehvs = fst $ flip runState actenv $ translateBehvs actstorage behvs (liftM $ concatError def) $ flip mapM actbehvs $ \(name,behvs',calldata, sig) -> do - solbehvs <- removeFails <$> getRuntimeBranches solvers hevmstorage calldata + solbehvs <- removeFails <$> getRuntimeBranches solvers hevmstorage calldata actenv.fresh showMsg $ "\x1b[1mChecking behavior \x1b[4m" <> name <> "\x1b[m of Act\x1b[m" -- equivalence check showMsg $ "\x1b[1mChecking if behaviour is matched by EVM\x1b[m" @@ -674,6 +677,7 @@ checkInputSpaces solvers l1 l2 = do let p1 = inputSpace l1 let p2 = inputSpace l2 conf <- readConfig + let queries = fmap (assertProps conf) [ [ EVM.PNeg (EVM.por p1), EVM.por p2 ] , [ EVM.por p1, EVM.PNeg (EVM.por p2) ] ] @@ -696,7 +700,7 @@ checkAbi solver contract cmap = do let (_, hevmstorage) = createStorage cmap let txdata = EVM.AbstractBuf "txdata" let selectorProps = assertSelector txdata <$> nubOrd (actSigs contract) - evmBehvs <- getRuntimeBranches solver hevmstorage (txdata, []) + evmBehvs <- getRuntimeBranches solver hevmstorage (txdata, []) 0 -- TODO what freshAddr goes here? conf <- readConfig let queries = fmap (assertProps conf) $ filter (/= []) $ fmap (checkBehv selectorProps) evmBehvs res <- liftIO $ mapConcurrently (checkSat solver) queries @@ -782,3 +786,6 @@ checkResult calldata sig res = -- | Pretty prints a list of hevm behaviours for debugging purposes showBehvs :: [EVM.Expr a] -> String showBehvs behvs = T.unpack $ T.unlines $ fmap Format.formatExpr behvs + +showProps :: [EVM.Prop] -> String +showProps props = T.unpack $ T.unlines $ fmap Format.formatProp props diff --git a/src/Act/HEVM_utils.hs b/src/Act/HEVM_utils.hs index d6bb0d92..0a3b629a 100644 --- a/src/Act/HEVM_utils.hs +++ b/src/Act/HEVM_utils.hs @@ -111,9 +111,9 @@ checkPartial nodes = else pure () -- | decompiles the given EVM bytecode into a list of Expr branches -getRuntimeBranches :: App m => SolverGroup -> [(EVM.Expr EVM.EAddr, EVM.Contract)] -> Calldata -> m [EVM.Expr EVM.End] -getRuntimeBranches solvers contracts calldata = do - prestate <- liftIO $ stToIO $ abstractVM contracts calldata +getRuntimeBranches :: App m => SolverGroup -> [(EVM.Expr EVM.EAddr, EVM.Contract)] -> Calldata -> Int -> m [EVM.Expr EVM.End] +getRuntimeBranches solvers contracts calldata fresh = do + prestate <- liftIO $ stToIO $ abstractVM contracts calldata fresh expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased prestate runExpr let simpl = simplify expr let nodes = flattenExpr simpl @@ -122,26 +122,26 @@ getRuntimeBranches solvers contracts calldata = do -- | decompiles the given EVM initcode into a list of Expr branches -getInitcodeBranches :: App m => SolverGroup -> BS.ByteString -> Calldata -> m [EVM.Expr EVM.End] -getInitcodeBranches solvers initcode calldata = do - initVM <- liftIO $ stToIO $ abstractInitVM initcode calldata +getInitcodeBranches :: App m => SolverGroup -> BS.ByteString -> Calldata -> Int -> m [EVM.Expr EVM.End] +getInitcodeBranches solvers initcode calldata fresh = do + initVM <- liftIO $ stToIO $ abstractInitVM initcode calldata fresh expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased initVM runExpr let simpl = if True then (simplify expr) else expr let nodes = flattenExpr simpl checkPartial nodes pure nodes -abstractInitVM :: BS.ByteString -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> ST s (EVM.VM EVM.Symbolic s) -abstractInitVM contractCode cd = do +abstractInitVM :: BS.ByteString -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> Int -> ST s (EVM.VM EVM.Symbolic s) +abstractInitVM contractCode cd fresh = do let value = EVM.TxValue let code = EVM.InitCode contractCode (fst cd) - loadSymVM (EVM.SymAddr "entrypoint", EVM.initialContract code) [] value cd True + loadSymVM (EVM.SymAddr "entrypoint", EVM.initialContract code) [] value cd True fresh -abstractVM :: [(EVM.Expr EVM.EAddr, EVM.Contract)] -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> ST s (EVM.VM EVM.Symbolic s) -abstractVM contracts cd = do +abstractVM :: [(EVM.Expr EVM.EAddr, EVM.Contract)] -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> Int -> ST s (EVM.VM EVM.Symbolic s) +abstractVM contracts cd fresh = do let value = EVM.TxValue let (c, cs) = findInitContract - loadSymVM c cs value cd False + loadSymVM c cs value cd False fresh where findInitContract :: ((EVM.Expr 'EVM.EAddr, EVM.Contract), [(EVM.Expr 'EVM.EAddr, EVM.Contract)]) @@ -157,8 +157,9 @@ loadSymVM -> EVM.Expr EVM.EWord -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> Bool + -> Int -> ST s (EVM.VM EVM.Symbolic s) -loadSymVM (entryaddr, entrycontract) othercontracts callvalue cd create = +loadSymVM (entryaddr, entrycontract) othercontracts callvalue cd create fresh = (EVM.makeVm $ EVM.VMOpts { contract = entrycontract , otherContracts = othercontracts @@ -184,6 +185,6 @@ loadSymVM (entryaddr, entrycontract) othercontracts callvalue cd create = , create = create , txAccessList = mempty , allowFFI = False - , freshAddresses = 0 + , freshAddresses = fresh , beaconRoot = 0 }) diff --git a/tests/hevm/pass/multi4/multi4.act b/tests/hevm/pass/multi4/multi4.act new file mode 100644 index 00000000..dcc495dd --- /dev/null +++ b/tests/hevm/pass/multi4/multi4.act @@ -0,0 +1,53 @@ +// contract A + +constructor of A +interface constructor(uint z) + +iff + CALLVALUE == 0 + inRange(uint256, z + 1) + +creates + uint x := z + 1 + + +behaviour x of A +interface x() + +iff + CALLVALUE == 0 + +returns + pre(x) + +behaviour add_x of A +interface add_x(uint y) + +iff + CALLVALUE == 0 + inRange(uint256, x + y) + +storage + + x => x + y + + +// contract B +constructor of B +interface constructor(uint i) +iff + CALLVALUE == 0 + inRange(uint256, i + 42) + +creates + uint z := i + 42 + A a := create A(i) + +behaviour foo of B +interface foo() + +iff + CALLVALUE == 0 + +storage + a => create A(42) diff --git a/tests/hevm/pass/multi4/multi4.sol b/tests/hevm/pass/multi4/multi4.sol new file mode 100644 index 00000000..1c206030 --- /dev/null +++ b/tests/hevm/pass/multi4/multi4.sol @@ -0,0 +1,25 @@ +contract A { + uint public x; + + constructor (uint z) { + x = z + 1; + } + + function add_x(uint y) public { + x = x + y; + } +} + +contract B { + uint z; + A a; + + constructor (uint i) { + z = i + 42; + a = new A(i); + } + + function foo() public { + a = new A(42); + } +}