From 461972db0e5588d3596cef56cfdec8c386bfde45 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 21 Oct 2024 17:25:36 +0200
Subject: [PATCH] Better printing of issues

---
 cli/cli.hs          |  4 +++-
 src/EVM/SymExec.hs  | 12 +++++++++++-
 src/EVM/UnitTest.hs | 15 ++++-----------
 3 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/cli/cli.hs b/cli/cli.hs
index 80206d318..149e2d0a5 100644
--- a/cli/cli.hs
+++ b/cli/cli.hs
@@ -261,7 +261,9 @@ equivalence cmd = do
       False -> liftIO $ do
         putStrLn "No discrepancies found"
         when (any isUnknown res || any isError res) $ do
-          putStrLn $ "But " <> (show $ length $ filter isUnknown res) <> " timeout(s) and/or " <> (show $ length $ filter isError res) <> " error(s)/incomplete execution(s) occurred"
+          putStrLn "But the following issues occurred:"
+          forM_ (groupIssues (filter isError res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+          forM_ (groupIssues (filter isUnknown res)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
           exitFailure
       True -> liftIO $ do
         let cexs = mapMaybe getCex res
diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs
index 59679daba..72ba513e8 100644
--- a/src/EVM/SymExec.hs
+++ b/src/EVM/SymExec.hs
@@ -15,7 +15,7 @@ import Data.ByteString (ByteString)
 import Data.ByteString qualified as BS
 import Data.Containers.ListUtils (nubOrd)
 import Data.DoubleWord (Word256)
-import Data.List (foldl', sortBy)
+import Data.List (foldl', sortBy, sort, group)
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
@@ -77,6 +77,16 @@ isQed :: ProofResult a b c d -> Bool
 isQed (Qed _) = True
 isQed _ = False
 
+groupIssues :: [ProofResult a b c String] -> [(Integer, String)]
+groupIssues results = map (\g -> (into (length g), head g)) grouped
+  where
+    getErr :: ProofResult a b c String -> String
+    getErr (EVM.SymExec.Error k) = k
+    getErr (EVM.SymExec.Unknown _) = "SMT result timeout/unknown"
+    getErr _ = internalError "shouldn't happen"
+    sorted = sort $ map getErr results
+    grouped = group sorted
+
 data VeriOpts = VeriOpts
   { simp :: Bool
   , maxIter :: Maybe Integer
diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs
index 5152865d5..b0379a262 100644
--- a/src/EVM/UnitTest.hs
+++ b/src/EVM/UnitTest.hs
@@ -15,7 +15,7 @@ import EVM.FeeSchedule (feeSchedule)
 import EVM.Fetch qualified as Fetch
 import EVM.Format
 import EVM.Solidity
-import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isError, VerifyResult, ProofResult (..))
+import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isUnknown, isError, groupIssues)
 import EVM.Types
 import EVM.Transaction (initTx)
 import EVM.Stepper (Stepper)
@@ -27,7 +27,6 @@ import Control.Monad.State.Strict (execState, get, put, liftIO)
 import Optics.Core
 import Optics.State
 import Optics.State.Operators
-import Data.List (sort, group)
 import Data.Binary.Get (runGet)
 import Data.ByteString (ByteString)
 import Data.ByteString.Lazy qualified as BSLazy
@@ -225,9 +224,10 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     -- check postconditions against vm
     (e, results) <- verify solvers (makeVeriOpts opts) (symbolify vm') (Just postcondition)
     let allReverts = not . (any Expr.isSuccess) . flattenExpr $ e
-    when (any isError results) $ liftIO $ do
+    when (any isUnknown results || any isError results) $ liftIO $ do
       putStrLn $ "      \x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the test " <> Text.unpack testName <> " due to: ";
-      forM_ (countOccurrences (filter isError results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+      forM_ (groupIssues (filter isError results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+      forM_ (groupIssues (filter isUnknown results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
 
     -- display results
     if all isQed results
@@ -245,13 +245,6 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
       liftIO $ putStr $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n" <> Text.unpack y
       pure False
     where
-      countOccurrences :: [VerifyResult] -> [(Integer, String)]
-      countOccurrences results = map (\g -> (into (length g), head g)) grouped
-        where
-          getProofErr (EVM.SymExec.Error k) = k
-          getProofErr _ = internalError "shouldn't happen"
-          sorted = sort $ map getProofErr results
-          grouped = group sorted
 
 allBranchRev :: Text
 allBranchRev = intercalate "\n"