From d8a1767c66fa01962b54903413d42573192c44df Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 20 Aug 2024 01:22:50 +0300 Subject: [PATCH 1/9] WIP in compiling Act --- act.cabal | 2 + flake.lock | 137 ++++++++++++++++++++++++++++++++--------------- flake.nix | 4 +- src/Act/Print.hs | 32 +++++++++-- src/Act/SMT.hs | 52 +++++++++--------- src/Act/Type.hs | 4 +- 6 files changed, 156 insertions(+), 75 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..12852f59 100644 --- a/flake.lock +++ b/flake.lock @@ -1,33 +1,18 @@ { "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": { + "cabal-3-12": { "flake": false, "locked": { - "lastModified": 1693777827, - "narHash": "sha256-zMwVwTztoQGrNIJSxSdVJjYN77rleRjpC+K5AoIl7po=", + "lastModified": 1719273538, + "narHash": "sha256-/TECd3cdqGDdlEur88H0KbV7jcE/czc0jecj9921T5c=", "owner": "haskell", "repo": "cabal", - "rev": "24a4603eebfcf7730f00bb69a02d1568990798d5", + "rev": "260ecdc3d848782d4df49e629cb0a5dc9e96ca9e", "type": "github" }, "original": { "owner": "haskell", + "ref": "Cabal-v3.12.1.0", "repo": "cabal", "type": "github" } @@ -52,11 +37,11 @@ "flake-compat": { "flake": false, "locked": { - "lastModified": 1673956053, - "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", "owner": "edolstra", "repo": "flake-compat", - "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", "type": "github" }, "original": { @@ -88,11 +73,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 +101,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,24 +141,23 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1691140388, - "narHash": "sha256-AH3fx2VFGPRSOjnuakab4T4AdUstwTnFTbnkoU4df8Q=", + "lastModified": 1719997877, + "narHash": "sha256-/Edw+w0PiGgxwnCeJycM0VgH4HtlCi91v1d8xbi+REE=", "owner": "shazow", "repo": "foundry.nix", - "rev": "6089aad0ef615ac8c7b0c948d6052fa848c99523", + "rev": "02febba4f1cf0606d790acdb24adcf7a64afb4e1", "type": "github" }, "original": { "owner": "shazow", - "ref": "monthly", "repo": "foundry.nix", + "rev": "6089aad0ef615ac8c7b0c948d6052fa848c99523", "type": "github" } }, "hevmUpstream": { "inputs": { - "bitwuzla-pkgs": "bitwuzla-pkgs", - "cabal-head": "cabal-head", + "cabal-3-12": "cabal-3-12", "ethereum-tests": "ethereum-tests", "flake-compat": "flake-compat", "flake-utils": "flake-utils_2", @@ -164,14 +166,15 @@ "nixpkgs": [ "nixpkgs" ], + "solc-pkgs": "solc-pkgs", "solidity": "solidity" }, "locked": { - "lastModified": 1712067908, - "narHash": "sha256-gh+dCwIbxAK7ICDFF5gdajgAlP2gnrT3yFnIx+qG6tY=", + "lastModified": 1723540200, + "narHash": "sha256-EO0oj4SHcab7NM3ry1muI38rM4gKdavQ2TNBQGZ9+S4=", "owner": "ethereum", "repo": "hevm", - "rev": "072864345e0dad26028184ecadd23f4f1ac8c89b", + "rev": "eee947de40c62ec7c57a8b7288d7844b82d2415a", "type": "github" }, "original": { @@ -196,17 +199,17 @@ }, "nixpkgs_2": { "locked": { - "lastModified": 1698165927, - "narHash": "sha256-XWfxt0Mi2h1EatZ9UKpbC0iXlS7+DupCs2dDl/yENO0=", + "lastModified": 1724015816, + "narHash": "sha256-hVESnM7Eiz93+4DeiE0a1TwMeaeph1ytRJ5QtqxYRWg=", "owner": "nixos", "repo": "nixpkgs", - "rev": "f85a3c6af20f02135814867870deb419329e8297", + "rev": "9aa35efbea27d320d0cdc5f922f0890812affb60", "type": "github" }, "original": { "owner": "nixos", + "ref": "nixpkgs-unstable", "repo": "nixpkgs", - "rev": "f85a3c6af20f02135814867870deb419329e8297", "type": "github" } }, @@ -217,6 +220,41 @@ "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": [ + "hevmUpstream", + "nixpkgs" + ], + "solc-macos-amd64-list-json": "solc-macos-amd64-list-json" + }, + "locked": { + "lastModified": 1717442267, + "narHash": "sha256-6TnQvA6Q/xC3r1M+wGC5gnDc/5XfOPjC8X6LlGDWDNc=", + "owner": "hellwolf", + "repo": "solc.nix", + "rev": "2ac2862f224aa0d67cbc6b3246392489f8a50596", + "type": "github" + }, + "original": { + "owner": "hellwolf", + "repo": "solc.nix", + "type": "github" + } + }, "solidity": { "flake": false, "locked": { @@ -263,6 +301,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..845b0c5a 100644 --- a/flake.nix +++ b/flake.nix @@ -3,7 +3,7 @@ inputs = { flake-utils.url = "github:numtide/flake-utils"; - nixpkgs.url = "github:nixos/nixpkgs/f85a3c6af20f02135814867870deb419329e8297"; + nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; hevmUpstream = { url = "github:ethereum/hevm"; inputs.nixpkgs.follows = "nixpkgs"; @@ -57,4 +57,4 @@ }; } ); -} +} \ No newline at end of file diff --git a/src/Act/Print.hs b/src/Act/Print.hs index e54fd681..15ff31a8 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 qualified Prettyprinter as PP +import Prettyprinter.Render.Text (renderIO) +import qualified Prettyprinter.Render.Terminal as RenderT + 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,27 @@ 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 + + + -- | prints a Doc, with wider output than the built in `putDoc` -render :: Doc -> IO () -render doc = displayIO stdout (renderPretty 0.9 120 doc) +render :: PP.Doc ann -> IO () +render doc = + let opts = PP.LayoutOptions { PP.layoutPageWidth = PP.AvailablePerLine 120 0.9 } in + renderIO stdout (PP.layoutSmart opts doc) + + +-- backwards compatibility with Text.PrettyPrint.ANSI.Leijen + +type Doc = PP.Doc RenderT.AnsiStyle + +underline :: Doc -> Doc +underline = PP.annotate RenderT.underlined + +bold :: Doc -> Doc +bold = PP.annotate RenderT.bold + +(<$$>) = \x y -> PP.vsep [x,y] + + + diff --git a/src/Act/SMT.hs b/src/Act/SMT.hs index 1d6bbd50..5af9263c 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) @@ -100,10 +101,10 @@ data SMTExp = SMTExp instance Pretty SMTExp where pretty 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 @@ -140,7 +141,7 @@ data Model = Model instance Pretty Model where pretty (Model prestate poststate (ifaceName, args) environment initargs) = - (underline . text $ "counterexample:") <$$> line + (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 @@ -730,20 +732,20 @@ 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 (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 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 (Inv _ (_, csmt) behvs) = pretty "; constructor" <$$> sep' <$$> line <> pretty 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 <> pretty smt + sep' = pretty "; -------------------------------" ifExists :: Foldable t => t a -> Doc -> Doc -ifExists a b = if null a then empty else b +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] From c8883cde827ff252e07ef0885670266fae759e31 Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 20 Aug 2024 22:04:43 +0300 Subject: [PATCH 2/9] Act compiling --- src/Act/CLI.hs | 22 +++++++++++----------- src/Act/Consistency.hs | 10 +++++----- src/Act/Print.hs | 41 +++++++++++++++++++++++++++-------------- src/Act/SMT.hs | 24 ++++++++++++------------ 4 files changed, 55 insertions(+), 42 deletions(-) diff --git a/src/Act/CLI.hs b/src/Act/CLI.hs index 56927743..11f1659b 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 diff --git a/src/Act/Consistency.hs b/src/Act/Consistency.hs index 5c588af8..c4e7b20b 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 @@ -83,7 +83,7 @@ mkCaseQuery props behvs@((Behaviour _ _ (Interface ifaceName decls) preconds _ _ , _minitargs = [] } mkCaseQuery _ [] = error "Internal error: behaviours cannot be empty" - + -- | Checks nonoverlapping and exhaustiveness of cases checkCases :: Act -> Solvers.Solver -> Maybe Integer -> Bool -> IO () checkCases (Act _ contracts) solver' smttimeout debug = do @@ -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/Print.hs b/src/Act/Print.hs index 15ff31a8..a5244205 100644 --- a/src/Act/Print.hs +++ b/src/Act/Print.hs @@ -6,9 +6,9 @@ module Act.Print where import Prelude hiding (GT, LT) import Data.ByteString.UTF8 (toString) -import qualified Prettyprinter as PP -import Prettyprinter.Render.Text (renderIO) -import qualified Prettyprinter.Render.Terminal as RenderT +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 @@ -231,25 +231,38 @@ prettyInvPred = prettyExp . untime . fst +-- backwards compatibility with Text.PrettyPrint.ANSI.Leijen +type DocAnsi = Doc Term.AnsiStyle -- | prints a Doc, with wider output than the built in `putDoc` -render :: PP.Doc ann -> IO () +render :: DocAnsi -> IO () render doc = - let opts = PP.LayoutOptions { PP.layoutPageWidth = PP.AvailablePerLine 120 0.9 } in - renderIO stdout (PP.layoutSmart opts doc) + let opts = LayoutOptions { layoutPageWidth = AvailablePerLine 120 0.9 } in + Term.renderIO stdout (layoutPretty opts doc) +underline :: DocAnsi -> DocAnsi +underline = annotate Term.underlined --- backwards compatibility with Text.PrettyPrint.ANSI.Leijen +red :: DocAnsi -> DocAnsi +red = annotate (Term.color Term.Red) + +yellow :: DocAnsi -> DocAnsi +yellow = annotate (Term.color Term.Yellow) -type Doc = PP.Doc RenderT.AnsiStyle +green :: DocAnsi -> DocAnsi +green = annotate (Term.color Term.Green) -underline :: Doc -> Doc -underline = PP.annotate RenderT.underlined +bold :: DocAnsi -> DocAnsi +bold = annotate Term.bold -bold :: Doc -> Doc -bold = PP.annotate RenderT.bold +(<$$>) :: Doc ann -> Doc ann -> Doc ann +(<$$>) = \x y -> vsep [x,y] -(<$$>) = \x y -> PP.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 5af9263c..85d51217 100644 --- a/src/Act/SMT.hs +++ b/src/Act/SMT.hs @@ -98,8 +98,8 @@ 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 = pretty ";STORAGE:" <$$> (vsep . (fmap pretty) . nubOrd . _storage $ e) <> line calldata = pretty ";CALLDATA:" <$$> (vsep . (fmap pretty) . nubOrd . _calldata $ e) <> line @@ -139,8 +139,8 @@ data Model = Model } deriving (Show) -instance Pretty Model where - pretty (Model prestate poststate (ifaceName, args) environment initargs) = +instance PrettyAnsi Model where + prettyAnsi (Model prestate poststate (ifaceName, args) environment initargs) = (underline . pretty $ "counterexample:") <$$> line <> (indent 2 ( calldata' @@ -335,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)" @@ -731,21 +731,21 @@ isFail _ = True isPass :: SMTResult -> Bool isPass = not . isFail -getBehvName :: Query -> Doc +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 :: 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) = pretty "; 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 <> pretty "; behaviour: " <> (pretty . _name $ b) <$$> sep' <$$> line <> pretty smt + formatBehv (b, smt) = line <> pretty "; behaviour: " <> (pretty . _name $ b) <$$> sep' <$$> line <> prettyAnsi smt sep' = pretty "; -------------------------------" -ifExists :: Foldable t => t a -> Doc -> Doc +ifExists :: Foldable t => t a -> DocAnsi -> DocAnsi ifExists a b = if null a then emptyDoc else b From ae2a518d0dc1372144e7867fc3ebd0f64f5577b7 Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 20 Aug 2024 22:09:59 +0300 Subject: [PATCH 3/9] Nits --- src/Act/Consistency.hs | 2 +- src/Act/Print.hs | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Act/Consistency.hs b/src/Act/Consistency.hs index c4e7b20b..a24f3028 100644 --- a/src/Act/Consistency.hs +++ b/src/Act/Consistency.hs @@ -83,7 +83,7 @@ mkCaseQuery props behvs@((Behaviour _ _ (Interface ifaceName decls) preconds _ _ , _minitargs = [] } mkCaseQuery _ [] = error "Internal error: behaviours cannot be empty" - + -- | Checks nonoverlapping and exhaustiveness of cases checkCases :: Act -> Solvers.Solver -> Maybe Integer -> Bool -> IO () checkCases (Act _ contracts) solver' smttimeout debug = do diff --git a/src/Act/Print.hs b/src/Act/Print.hs index a5244205..3968c3f5 100644 --- a/src/Act/Print.hs +++ b/src/Act/Print.hs @@ -230,8 +230,7 @@ prettyInvPred = prettyExp . untime . fst Var p t at a -> Var p t at a - --- backwards compatibility with Text.PrettyPrint.ANSI.Leijen +-- | Doc type for terminal output type DocAnsi = Doc Term.AnsiStyle -- | prints a Doc, with wider output than the built in `putDoc` From 02be389bc11d55783ae9c38ba8b92c98e0b8182b Mon Sep 17 00:00:00 2001 From: zoep Date: Mon, 2 Sep 2024 19:18:17 +0300 Subject: [PATCH 4/9] Fix compilation error --- src/Test/Main.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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 84be0ad7334f7ab341d492b0a449ae553bd7493e Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 17 Sep 2024 14:03:29 +0300 Subject: [PATCH 5/9] bump flake --- flake.lock | 66 ++++++++++++++++++++---------------------------------- 1 file changed, 24 insertions(+), 42 deletions(-) diff --git a/flake.lock b/flake.lock index 12852f59..35dbb893 100644 --- a/flake.lock +++ b/flake.lock @@ -1,35 +1,18 @@ { "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" } @@ -55,11 +38,11 @@ "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,23 +124,22 @@ "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": { "inputs": { - "cabal-3-12": "cabal-3-12", "ethereum-tests": "ethereum-tests", "flake-compat": "flake-compat", "flake-utils": "flake-utils_2", @@ -170,11 +152,11 @@ "solidity": "solidity" }, "locked": { - "lastModified": 1723540200, - "narHash": "sha256-EO0oj4SHcab7NM3ry1muI38rM4gKdavQ2TNBQGZ9+S4=", + "lastModified": 1726564969, + "narHash": "sha256-Wy/fEjh7Q8hnc+Cmckbqowz4qEvS6K5KDIApndxaskw=", "owner": "ethereum", "repo": "hevm", - "rev": "eee947de40c62ec7c57a8b7288d7844b82d2415a", + "rev": "b420af77c2d585ed72a15e398503c255f31590b9", "type": "github" }, "original": { @@ -199,11 +181,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": { @@ -242,11 +224,11 @@ "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": { @@ -258,17 +240,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" } }, From 20a65e70313dbf26986db8393c624f2fe0803695 Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 17 Sep 2024 16:26:24 +0300 Subject: [PATCH 6/9] hevm update --- src/Act/HEVM.hs | 19 +++++++++++-------- src/Act/HEVM_utils.hs | 2 ++ 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs index e2352959..3b4222e6 100644 --- a/src/Act/HEVM.hs +++ b/src/Act/HEVM.hs @@ -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 @@ -638,13 +640,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 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 }) From c1ed9c596081b67000d96a511f32f30762a984a0 Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 17 Sep 2024 16:29:45 +0300 Subject: [PATCH 7/9] nit --- src/Act/HEVM.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs index 3b4222e6..b8342efa 100644 --- a/src/Act/HEVM.hs +++ b/src/Act/HEVM.hs @@ -647,7 +647,7 @@ createStorage cmap = toContract (EVM.C code storage tstorage balance nonce) = EVM.Contract { EVM.code = code , EVM.storage = storage - , EVM.tStorage = tstorage + , EVM.tStorage = tstorage , EVM.origStorage = storage , EVM.balance = balance , EVM.nonce = nonce From 54af02490c151d142387878dc7a293583ed53238 Mon Sep 17 00:00:00 2001 From: zoep Date: Mon, 23 Sep 2024 17:27:40 +0300 Subject: [PATCH 8/9] Fix in decompiler simplification --- src/Act/Decompile.hs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) 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)) From dfa1cbd0c67f7da66544d7bef8ca3b6fd61dfeab Mon Sep 17 00:00:00 2001 From: dxo Date: Wed, 23 Oct 2024 14:24:32 +0200 Subject: [PATCH 9/9] flake: use dynamic hevm output --- flake.lock | 30 +++++++----------------------- flake.nix | 32 ++++++++++++++++---------------- src/Act/CLI.hs | 6 +++--- src/Act/HEVM.hs | 15 ++++++++------- src/Test/Decompile.hs | 2 +- 5 files changed, 35 insertions(+), 50 deletions(-) diff --git a/flake.lock b/flake.lock index 35dbb893..71a08634 100644 --- a/flake.lock +++ b/flake.lock @@ -17,22 +17,6 @@ "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" @@ -138,10 +122,9 @@ "type": "github" } }, - "hevmUpstream": { + "hevm": { "inputs": { "ethereum-tests": "ethereum-tests", - "flake-compat": "flake-compat", "flake-utils": "flake-utils_2", "forge-std": "forge-std", "foundry": "foundry", @@ -152,15 +135,16 @@ "solidity": "solidity" }, "locked": { - "lastModified": 1726564969, - "narHash": "sha256-Wy/fEjh7Q8hnc+Cmckbqowz4qEvS6K5KDIApndxaskw=", + "lastModified": 1729608902, + "narHash": "sha256-6uTYwVYGGyVUdIcejP5shHdIzF/jp4XPz3kpDKN8FJ4=", "owner": "ethereum", "repo": "hevm", - "rev": "b420af77c2d585ed72a15e398503c255f31590b9", + "rev": "56d106e529162eda66253d4203dd4a39429317de", "type": "github" }, "original": { "owner": "ethereum", + "ref": "dynamic-flake-output", "repo": "hevm", "type": "github" } @@ -198,7 +182,7 @@ "root": { "inputs": { "flake-utils": "flake-utils", - "hevmUpstream": "hevmUpstream", + "hevm": "hevm", "nixpkgs": "nixpkgs_2" } }, @@ -218,7 +202,7 @@ "inputs": { "flake-utils": "flake-utils_4", "nixpkgs": [ - "hevmUpstream", + "hevm", "nixpkgs" ], "solc-macos-amd64-list-json": "solc-macos-amd64-list-json" diff --git a/flake.nix b/flake.nix index 845b0c5a..c2159612 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"; + 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/src/Act/CLI.hs b/src/Act/CLI.hs index 11f1659b..b3a35149 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/HEVM.hs b/src/Act/HEVM.hs index b8342efa..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" @@ -586,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)) @@ -757,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/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