From 19f30d5700375608c4897bfed7eb799c1837a2d0 Mon Sep 17 00:00:00 2001 From: Jack Ek <2727556+kjekac@users.noreply.github.com> Date: Thu, 26 Aug 2021 18:55:18 +0200 Subject: [PATCH 1/8] add summary to output in HEVM mode --- src/Main.hs | 35 +++++++++++++++++++++++------------ src/act.cabal | 2 +- 2 files changed, 24 insertions(+), 13 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index f0dedfd5..7818cbeb 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -17,6 +17,7 @@ import System.IO (hPutStrLn, stderr, stdout) import Data.SBV hiding (preprocess, sym, prove) import Data.Text (pack, unpack) import Data.List +import Data.Either (lefts) import Data.Maybe import Data.Tree import qualified EVM.Solidity as Solidity @@ -217,18 +218,28 @@ hevm spec' soljson' solver' smttimeout' smtdebug' = do passes <- forM specs $ \behv -> do res <- runSMTWithTimeOut solver' smttimeout' smtdebug' $ proveBehaviour sources behv case res of - Qed posts -> do - putStrLn $ "Successfully proved " <> (_name behv) <> "(" <> show (_mode behv) <> ")" - <> ", " <> show (length $ last $ levels posts) <> " cases." - return True - Cex _ -> do - putStrLn $ "Failed to prove " <> (_name behv) <> "(" <> show (_mode behv) <> ")" - return False - Timeout _ -> do - putStrLn $ "Solver timeout when attempting to prove " <> (_name behv) <> "(" <> show (_mode behv) <> ")" - return False - unless (and passes) exitFailure - + Qed posts -> let msg = "Successfully proved " <> showBehv behv <> ", " + <> show (length $ last $ levels posts) <> " cases." + in putStrLn msg >> return (Right msg) + Cex _ -> let msg = "Failed to prove " <> showBehv behv + in putStrLn msg >> return (Left msg) + Timeout _ -> let msg = "Solver timeout when attempting to prove " <> showBehv behv + in putStrLn msg >> return (Left msg) + let fails = lefts passes + + putStrLn "\n==== RESULT ====" + putStrLn . unlines $ + if null fails + then [ "Success!" + , "" + , soljson' <> " fully satisfies " <> spec' <> "." ] + else [ "Failure!" + , "" + , unwords [show . length $ fails, "out", "of", show . length $ passes, "claims", "unproven:"] + , unlines fails ] + unless (null fails) exitFailure + where + showBehv behv = _name behv <> "(" <> show (_mode behv) <> ")" ------------------- -- *** Util *** --- diff --git a/src/act.cabal b/src/act.cabal index 55f2df2a..4bd327f7 100644 --- a/src/act.cabal +++ b/src/act.cabal @@ -14,7 +14,7 @@ common deps build-depends: base >= 4.9 && < 5, aeson >= 1.0, containers >= 0.5, - hevm >= 0.47.1, + hevm >= 0.47.1 && < 0.48, lens >= 4.17.1, text >= 1.2, array >= 0.5.3.0, From 00f67b3af837c07dbe80e9518f26e58666faa82d Mon Sep 17 00:00:00 2001 From: Jack Ek <2727556+kjekac@users.noreply.github.com> Date: Thu, 26 Aug 2021 19:36:01 +0200 Subject: [PATCH 2/8] adjust output formatting --- src/Main.hs | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index 7818cbeb..6e18a2be 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -225,19 +225,21 @@ hevm spec' soljson' solver' smttimeout' smtdebug' = do in putStrLn msg >> return (Left msg) Timeout _ -> let msg = "Solver timeout when attempting to prove " <> showBehv behv in putStrLn msg >> return (Left msg) - let fails = lefts passes + let failures = lefts passes putStrLn "\n==== RESULT ====" putStrLn . unlines $ - if null fails + if null failures then [ "Success!" , "" - , soljson' <> " fully satisfies " <> spec' <> "." ] + , soljson' <> " fully satisfies " <> spec' <> "." + ] else [ "Failure!" + , unwords [show . length $ failures, "out of", show . length $ passes, "claims unproven:"] , "" - , unwords [show . length $ fails, "out", "of", show . length $ passes, "claims", "unproven:"] - , unlines fails ] - unless (null fails) exitFailure + , unlines $ zipWith (\i msg -> show i <> "\t" <> msg) [1..] failures + ] + unless (null failures) exitFailure where showBehv behv = _name behv <> "(" <> show (_mode behv) <> ")" From 03cefeee60f7d5dfa4f9faed98524da3c3655e85 Mon Sep 17 00:00:00 2001 From: Jack Ek <2727556+kjekac@users.noreply.github.com> Date: Thu, 26 Aug 2021 20:51:05 +0200 Subject: [PATCH 3/8] fix CI errors --- src/Main.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Main.hs b/src/Main.hs index 6e18a2be..d6be70f2 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -237,7 +237,7 @@ hevm spec' soljson' solver' smttimeout' smtdebug' = do else [ "Failure!" , unwords [show . length $ failures, "out of", show . length $ passes, "claims unproven:"] , "" - , unlines $ zipWith (\i msg -> show i <> "\t" <> msg) [1..] failures + , unlines $ zipWith (\i msg -> show (i::Int) <> "\t" <> msg) [1..] failures ] unless (null failures) exitFailure where From 94f3b4a986fe28490c500395825315486eeb36ca Mon Sep 17 00:00:00 2001 From: Jack Ek <2727556+kjekac@users.noreply.github.com> Date: Fri, 27 Aug 2021 08:57:47 +0200 Subject: [PATCH 4/8] simplify output and code --- src/Main.hs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index d6be70f2..790667ec 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -227,18 +227,17 @@ hevm spec' soljson' solver' smttimeout' smtdebug' = do in putStrLn msg >> return (Left msg) let failures = lefts passes - putStrLn "\n==== RESULT ====" putStrLn . unlines $ if null failures - then [ "Success!" + then [ "==== SUCCESS ====" , "" , soljson' <> " fully satisfies " <> spec' <> "." ] - else [ "Failure!" - , unwords [show . length $ failures, "out of", show . length $ passes, "claims unproven:"] + else [ "==== FAILURE ====" , "" - , unlines $ zipWith (\i msg -> show (i::Int) <> "\t" <> msg) [1..] failures + , show (length failures) <> " out of " <> show (length passes) <> " claims unproven:" ] + <> zipWith (\i msg -> show (i::Int) <> "\t" <> msg) [1..] failures unless (null failures) exitFailure where showBehv behv = _name behv <> "(" <> show (_mode behv) <> ")" From 9d8b71b994d297ba2a7fc0bb1a07848c1e83f394 Mon Sep 17 00:00:00 2001 From: Jack Ek <2727556+kjekac@users.noreply.github.com> Date: Fri, 27 Aug 2021 09:00:47 +0200 Subject: [PATCH 5/8] tweak output --- src/Main.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index 790667ec..562f5c09 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -230,12 +230,11 @@ hevm spec' soljson' solver' smttimeout' smtdebug' = do putStrLn . unlines $ if null failures then [ "==== SUCCESS ====" - , "" , soljson' <> " fully satisfies " <> spec' <> "." ] else [ "==== FAILURE ====" - , "" , show (length failures) <> " out of " <> show (length passes) <> " claims unproven:" + , "" ] <> zipWith (\i msg -> show (i::Int) <> "\t" <> msg) [1..] failures unless (null failures) exitFailure From 27e024ab9010e5b2fc1aaca34e3a191e54afb3c4 Mon Sep 17 00:00:00 2001 From: Jack Ek <2727556+kjekac@users.noreply.github.com> Date: Fri, 27 Aug 2021 09:29:24 +0200 Subject: [PATCH 6/8] strip paths from filenames --- src/Main.hs | 3 ++- src/act.cabal | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index 562f5c09..fdfee452 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -25,6 +25,7 @@ import qualified Data.Text as Text import qualified Data.Text.IO as TIO import qualified Data.Map.Strict as Map import System.Environment (setEnv) +import System.FilePath.Posix (takeFileName) import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) import qualified Data.ByteString.Lazy.Char8 as B @@ -230,7 +231,7 @@ hevm spec' soljson' solver' smttimeout' smtdebug' = do putStrLn . unlines $ if null failures then [ "==== SUCCESS ====" - , soljson' <> " fully satisfies " <> spec' <> "." + , takeFileName soljson' <> " fully satisfies " <> takeFileName spec' <> "." ] else [ "==== FAILURE ====" , show (length failures) <> " out of " <> show (length passes) <> " claims unproven:" diff --git a/src/act.cabal b/src/act.cabal index 4bd327f7..753ed670 100644 --- a/src/act.cabal +++ b/src/act.cabal @@ -26,7 +26,8 @@ common deps utf8-string >= 1.0.1.1, process >= 1.6.5.0, ansi-wl-pprint >= 0.6.9, - regex-tdfa + regex-tdfa, + filepath other-modules: Lex ErrM Parse K HEVM Coq Syntax Syntax.Untyped Syntax.Typed Syntax.Annotated Syntax.Timing Syntax.TimeAgnostic Type Print Enrich SMT if flag(ci) From 36836ded865c18d517dc280c9cc8599c73fc96aa Mon Sep 17 00:00:00 2001 From: Jack Ek <2727556+kjekac@users.noreply.github.com> Date: Fri, 27 Aug 2021 14:48:54 +0200 Subject: [PATCH 7/8] Apply suggestions from code review Co-authored-by: David Terry <6689924+d-xo@users.noreply.github.com> --- src/Main.hs | 2 +- src/act.cabal | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index fdfee452..8c3b201e 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -231,7 +231,7 @@ hevm spec' soljson' solver' smttimeout' smtdebug' = do putStrLn . unlines $ if null failures then [ "==== SUCCESS ====" - , takeFileName soljson' <> " fully satisfies " <> takeFileName spec' <> "." + "All behaviours implemented as specified ∎." ] else [ "==== FAILURE ====" , show (length failures) <> " out of " <> show (length passes) <> " claims unproven:" diff --git a/src/act.cabal b/src/act.cabal index 753ed670..9bbbc47c 100644 --- a/src/act.cabal +++ b/src/act.cabal @@ -14,7 +14,7 @@ common deps build-depends: base >= 4.9 && < 5, aeson >= 1.0, containers >= 0.5, - hevm >= 0.47.1 && < 0.48, + hevm >= 0.47.1 && < 0.48, -- Ugly upper bound to force usage of version from nix-shell. lens >= 4.17.1, text >= 1.2, array >= 0.5.3.0, From 30cf040c63249c511a7e4b52b72fd001d77db869 Mon Sep 17 00:00:00 2001 From: Jack Ek <2727556+kjekac@users.noreply.github.com> Date: Fri, 27 Aug 2021 15:13:39 +0200 Subject: [PATCH 8/8] fix build errors --- src/Main.hs | 3 +-- src/act.cabal | 9 ++++++--- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index 8c3b201e..fab00eff 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -25,7 +25,6 @@ import qualified Data.Text as Text import qualified Data.Text.IO as TIO import qualified Data.Map.Strict as Map import System.Environment (setEnv) -import System.FilePath.Posix (takeFileName) import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) import qualified Data.ByteString.Lazy.Char8 as B @@ -231,7 +230,7 @@ hevm spec' soljson' solver' smttimeout' smtdebug' = do putStrLn . unlines $ if null failures then [ "==== SUCCESS ====" - "All behaviours implemented as specified ∎." + , "All behaviours implemented as specified ∎." ] else [ "==== FAILURE ====" , show (length failures) <> " out of " <> show (length passes) <> " claims unproven:" diff --git a/src/act.cabal b/src/act.cabal index 9bbbc47c..9fe498b9 100644 --- a/src/act.cabal +++ b/src/act.cabal @@ -14,7 +14,11 @@ common deps build-depends: base >= 4.9 && < 5, aeson >= 1.0, containers >= 0.5, - hevm >= 0.47.1 && < 0.48, -- Ugly upper bound to force usage of version from nix-shell. + hevm >= 0.47.1 && < 0.48, + -- hevm version has an ugly upper bound to + -- force usage of version from nix-shell, + -- which avoids weird missing deps when + -- pulling it from hackage. lens >= 4.17.1, text >= 1.2, array >= 0.5.3.0, @@ -26,8 +30,7 @@ common deps utf8-string >= 1.0.1.1, process >= 1.6.5.0, ansi-wl-pprint >= 0.6.9, - regex-tdfa, - filepath + regex-tdfa other-modules: Lex ErrM Parse K HEVM Coq Syntax Syntax.Untyped Syntax.Typed Syntax.Annotated Syntax.Timing Syntax.TimeAgnostic Type Print Enrich SMT if flag(ci)