Merge pull request #645 from ethereum/better-results-printing

Better results printing, WARNING-s make the check FAIL now.

Author: msooseth

CHANGELOG.md

@@ -31,6 +31,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Dumping of END states (.prop) files is now default for `--debug`
 - When cheatcode is missing, we produce a partial execution warning
 
+## Changed
+- Warnings now lead printing FAIL. This way, users don't accidentally think that
+  their contract is correct when there were cases/branches that hevm could not
+  fully explore. Printing of issues is also now much more organized
+
 ## [0.54.2] - 2024-12-12
 
 ## Fixed

cli/cli.hs

@@ -243,7 +243,7 @@ main = withUtf8 $ do
             -- TODO: which functions here actually require a BuildOutput, and which can take it as a Maybe?
             testOpts <- liftIO $ unitTestOptions cmd solvers (Just out)
             res <- unitTest testOpts out.contracts
-            liftIO $ unless res exitFailure
+            liftIO $ unless (uncurry (&&) res) exitFailure
 
 equivalence :: App m => Command Options.Unwrapped -> m ()
 equivalence cmd = do
@@ -269,15 +269,16 @@ equivalence cmd = do
     cores <- liftIO $ unsafeInto <$> getNumProcessors
     let solverCount = fromMaybe cores cmd.numSolvers
     withSolvers solver solverCount (fromMaybe 1 cmd.solverThreads) cmd.smttimeout $ \s -> do
-      res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata
+      (res, e) <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata
+      liftIO $ case (any isCex res, any Expr.isPartial e || any isUnknown res) of
+        (False, False) -> putStrLn "   \x1b[32m[PASS]\x1b[0m Contracts behave equivalently"
+        (True, _)      -> putStrLn "   \x1b[31m[FAIL]\x1b[0m Contracts do not behave equivalently"
+        (_, True)      -> putStrLn "   \x1b[31m[FAIL]\x1b[0m Contracts may not behave equivalently"
+      liftIO $ printWarnings e res "the contracts under test"
       case any isCex res of
         False -> liftIO $ do
+          when (any isUnknown res || any isError res || any isPartial e) exitFailure
           putStrLn "No discrepancies found"
-          when (any isUnknown res || any isError res) $ do
-            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
           T.putStrLn . T.unlines $

src/EVM/Format.hs

@@ -4,6 +4,7 @@ module EVM.Format
   ( formatExpr
   , formatSomeExpr
   , formatPartial
+  , formatPartialShort
   , formatProp
   , contractNamePart
   , contractPathPart
@@ -483,6 +484,13 @@ formatPartial = \case
     , "function selector: " <> T.pack (show selector)
     ]
 
+formatPartialShort :: PartialExec -> Text
+formatPartialShort = \case
+  UnexpectedSymbolicArg _ opcode _ _ -> "Unexpected symbolic arguments to opcode: " <> T.pack opcode
+  MaxIterationsReached {}            -> "Max iterations reached"
+  JumpIntoSymbolicCode {}            -> "Encountered a jump into a potentially symbolic code region while executing initcode"
+  CheatCodeMissing _ selector        -> "Cheat code not recognized: " <> T.pack (show selector)
+
 formatSomeExpr :: SomeExpr -> Text
 formatSomeExpr (SomeExpr e) = formatExpr $ Expr.simplify e
 

src/EVM/SymExec.hs

@@ -37,7 +37,7 @@ import EVM.ABI
 import EVM.Effects
 import EVM.Expr qualified as Expr
 import EVM.FeeSchedule (feeSchedule)
-import EVM.Format (formatExpr, formatPartial, showVal, bsToHex, indent, formatBinary)
+import EVM.Format (formatExpr, formatPartial, formatPartialShort, showVal, bsToHex, indent, formatBinary)
 import EVM.SMT (SMTCex(..), SMT2(..), assertProps)
 import EVM.SMT qualified as SMT
 import EVM.Solvers
@@ -89,6 +89,15 @@ groupIssues results = map (\g -> (into (length g), NE.head g)) grouped
     sorted = sort $ map getErr results
     grouped = NE.group sorted
 
+groupPartials :: [Expr End] -> [(Integer, String)]
+groupPartials e = map (\g -> (into (length g), NE.head g)) grouped
+  where
+    getErr :: Expr End -> String
+    getErr (Partial _ _ reason) = T.unpack $ formatPartialShort reason
+    getErr _ = internalError "shouldn't happen"
+    sorted = sort $ map getErr (filter isPartial e)
+    grouped = NE.group sorted
+
 data VeriOpts = VeriOpts
   { simp :: Bool
   , maxIter :: Maybe Integer
@@ -575,6 +584,13 @@ isPartial :: Expr a -> Bool
 isPartial (Partial _ _ _) = True
 isPartial _ = False
 
+printPartialIssues :: [Expr End] -> String -> IO ()
+printPartialIssues flattened call =
+  when (any isPartial flattened) $ do
+    T.putStrLn $ indent 3 "\x1b[33m[WARNING]\x1b[0m: hevm was only able to partially explore "
+                <> T.pack call <> " due to the following issue(s):"
+    T.putStr . T.unlines . fmap (indent 5 . ("- " <>)) . fmap formatPartial . getPartials $ flattened
+
 getPartials :: [Expr End] -> [PartialExec]
 getPartials = mapMaybe go
   where
@@ -603,14 +619,10 @@ verify solvers opts preState maybepost = do
     when conf.debug $ putStrLn "   Simplifying expression"
     let expr = if opts.simp then (Expr.simplify exprInter) else exprInter
     when conf.dumpExprs $ T.writeFile "simplified.expr" (formatExpr expr)
-
-    when conf.debug $ putStrLn $ "   Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
-
     let flattened = flattenExpr expr
-    when (any isPartial flattened) $ do
-      T.putStrLn $ indent 3 "\x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the call "
-                  <> T.pack call <> " due to the following issue(s):"
-      T.putStr . T.unlines . fmap (indent 5 . ("- " <>)) . fmap formatPartial . getPartials $ flattened
+    when conf.debug $ do
+      printPartialIssues flattened ("the call " <> call)
+      putStrLn $ "   Exploration finished, " <> show (Expr.numBranches expr) <> " branch(es) to check in call " <> call
 
     case maybepost of
       Nothing -> pure (expr, [Qed ()])
@@ -675,19 +687,20 @@ equivalenceCheck
   -> ByteString
   -> VeriOpts
   -> (Expr Buf, [Prop])
-  -> m [EquivResult]
+  -> m ([EquivResult], [Expr End])
 equivalenceCheck solvers bytecodeA bytecodeB opts calldata = do
   conf <- readConfig
   case bytecodeA == bytecodeB of
     True -> liftIO $ do
       putStrLn "bytecodeA and bytecodeB are identical"
-      pure [Qed ()]
+      pure ([Qed ()], mempty)
     False -> do
-      branchesA <- getBranches bytecodeA
-      branchesB <- getBranches bytecodeB
       when conf.debug $ liftIO $ do
         putStrLn "bytecodeA and bytecodeB are different, checking for equivalence"
-      equivalenceCheck' solvers branchesA branchesB
+      branchesA <- getBranches bytecodeA
+      branchesB <- getBranches bytecodeB
+      res <- equivalenceCheck' solvers branchesA branchesB
+      pure (res, branchesA <> branchesB)
   where
     -- decompiles the given bytecode into a list of branches
     getBranches :: ByteString -> m [Expr End]
@@ -703,14 +716,14 @@ equivalenceCheck'
   :: forall m . App m
   => SolverGroup -> [Expr End] -> [Expr End] -> m [EquivResult]
 equivalenceCheck' solvers branchesA branchesB = do
-      when (any isPartial branchesA || any isPartial branchesB) $ liftIO $ do
-        putStrLn "\x1b[33mWARNING\x1b[0m: hevm was only able to partially explore the given contract due to the following issue(s):"
-        T.putStr . T.unlines . fmap (indent 2 . ("- " <>)) . fmap formatPartial . nubOrd $ ((getPartials branchesA) <> (getPartials branchesB))
+      conf <- readConfig
+      when conf.debug $ do
+        liftIO $ printPartialIssues branchesA "codeA"
+        liftIO $ printPartialIssues branchesB "codeB"
 
       let allPairs = [(a,b) | a <- branchesA, b <- branchesB]
       liftIO $ putStrLn $ "Found " <> show (length allPairs) <> " total pairs of endstates"
 
-      conf <- readConfig
       when conf.dumpEndStates $ liftIO $
         putStrLn $ "endstates in bytecodeA: " <> show (length branchesA)
                    <> "\nendstates in bytecodeB: " <> show (length branchesB)
@@ -726,9 +739,10 @@ equivalenceCheck' solvers branchesA branchesB = do
 
       let useful = foldr (\(_, b) n -> if b then n+1 else n) (0::Integer) results
       liftIO $ putStrLn $ "Reuse of previous queries was Useful in " <> (show useful) <> " cases"
+
       case all (isQed . fst) results of
         True -> pure [Qed ()]
-        False -> pure $ filter (/= Qed ()) . fmap fst $ results
+        False -> pure $ filter (not . isQed) . fmap fst $ results
   where
     -- we order the sets by size because this gives us more cache hits when
     -- running our queries later on (since we rely on a subset check)

src/EVM/UnitTest.hs

@@ -14,7 +14,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, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isUnknown, isError, groupIssues)
+import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isCex, extractCex, prettyCalldata, panicMsg, VeriOpts(..), flattenExpr, isUnknown, isError, groupIssues, groupPartials, ProofResult(..))
 import EVM.Types
 import EVM.Transaction (initTx)
 import EVM.Stepper (Stepper)
@@ -113,7 +113,8 @@ makeVeriOpts opts =
                    }
 
 -- | Top level CLI endpoint for hevm test
-unitTest :: App m => UnitTestOptions RealWorld -> Contracts -> m Bool
+-- | Returns tuple of (No Cex, No warnings)
+unitTest :: App m => UnitTestOptions RealWorld -> Contracts -> m (Bool, Bool)
 unitTest opts (Contracts cs) = do
   let unitTestContrs = findUnitTests opts.match $ Map.elems cs
   conf <- readConfig
@@ -122,7 +123,9 @@ unitTest opts (Contracts cs) = do
     let x = map (\(a,b) -> "  --> " <> a <> "  ---  functions: " <> (Text.pack $ show b)) unitTestContrs
     putStrLn $ unlines $ map Text.unpack x
   results <- concatMapM (runUnitTestContract opts cs) unitTestContrs
-  pure $ and results
+  when conf.debug $ liftIO $ putStrLn $ "unitTest individual results: " <> show results
+  let (firsts, seconds) = unzip results
+  pure (and firsts, and seconds)
 
 -- | Assuming a constructor is loaded, this stepper will run the constructor
 -- to create the test contract, give it an initial balance, and run `setUp()'.
@@ -155,24 +158,20 @@ initializeUnitTest opts theContract = do
     Left e -> pushTrace (ErrorTrace e)
     _ -> popTrace
 
+-- Returns tuple of (No Cex, No warnings)
 runUnitTestContract
   :: App m
   => UnitTestOptions RealWorld
   -> Map Text SolcContract
   -> (Text, [Sig])
-  -> m [Bool]
+  -> m [(Bool, Bool)]
 runUnitTestContract
   opts@(UnitTestOptions {..}) contractMap (name, testSigs) = do
-
-  -- Print a header
   liftIO $ putStrLn $ "Checking " ++ show (length testSigs) ++ " function(s) in contract " ++ unpack name
 
   -- Look for the wanted contract by name from the Solidity info
   case Map.lookup name contractMap of
-    Nothing ->
-      -- Fail if there's no such contract
-      internalError $ "Contract " ++ unpack name ++ " not found"
-
+    Nothing -> internalError $ "Contract " ++ unpack name ++ " not found"
     Just theContract -> do
       -- Construct the initial VM and begin the contract's constructor
       vm0 :: VM Concrete RealWorld <- liftIO $ stToIO $ initialUnitTestVm opts theContract
@@ -184,15 +183,16 @@ runUnitTestContract
       writeTraceDapp dapp vm1
       case vm1.result of
         Just (VMFailure _) -> liftIO $ do
-          Text.putStrLn "\x1b[31m[BAIL]\x1b[0m setUp() "
-          tick $ failOutput vm1 opts "setUp()"
-          pure [False]
+          Text.putStrLn "   \x1b[31m[BAIL]\x1b[0m setUp() "
+          tick $ indentLines 3 $ failOutput vm1 opts "setUp()"
+          pure [(True, False)]
         Just (VMSuccess _) -> do
           forM testSigs $ \s -> symRun opts vm1 s
         _ -> internalError "setUp() did not end with a result"
 
--- | Define the thread spawner for symbolic tests
-symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m Bool
+-- Define the thread spawner for symbolic tests
+-- Returns tuple of (No Cex, No warnings)
+symRun :: App m => UnitTestOptions RealWorld -> VM Concrete RealWorld -> Sig -> m (Bool, Bool)
 symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     let callSig = testName <> "(" <> (Text.intercalate "," (map abiTypeSolidity types)) <> ")"
     liftIO $ putStrLn $ "\x1b[96m[RUNNING]\x1b[0m " <> Text.unpack callSig
@@ -227,42 +227,47 @@ symRun opts@UnitTestOptions{..} vm (Sig testName types) = do
     writeTraceDapp dapp vm'
 
     -- check postconditions against vm
-    (e, results) <- verify solvers (makeVeriOpts opts) (symbolify vm') (Just postcondition)
-    let allReverts = not . (any Expr.isSuccess) . flattenExpr $ e
-
+    (end, results) <- verify solvers (makeVeriOpts opts) (symbolify vm') (Just postcondition)
+    let ends = flattenExpr end
     conf <- readConfig
-    when conf.debug $ liftIO $ forM_ (filter Expr.isFailure (flattenExpr e)) $ \case
+    when conf.debug $ liftIO $ forM_ (filter Expr.isFailure ends) $ \case
       (Failure _ _ a) ->  putStrLn $ "   -> debug of func: " <> Text.unpack testName <> " Failure at the end of expr: " <> show a;
       _ -> internalError "cannot be, filtered for failure"
-    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_ (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
-    then if allReverts && (not shouldFail)
-         then do
-           liftIO $ putStr $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n" <> Text.unpack allBranchRev
-           pure False
-         else do
-           liftIO $ putStr $ "   \x1b[32m[PASS]\x1b[0m " <> Text.unpack testName <> "\n"
-           pure True
-    else do
-      -- not all is Qed
-      let x = mapMaybe extractCex results
-      let y = symFailure opts testName (fst cd) types x
-      liftIO $ putStr $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n" <> Text.unpack y
-      pure False
-
-allBranchRev :: Text
-allBranchRev = intercalate "\n"
-  [ Text.concat $ indentLines 3 <$>
-      [ "Reason:"
-      , "  No reachable assertion violations, but all branches reverted"
-      , "  Prefix this testname with `proveFail` if this is expected"
-      ]
-  ]
+    let t = "the test " <> Text.unpack testName
+    let warnings = any Expr.isPartial ends || any isUnknown results || any isError results
+    let allReverts = not . (any Expr.isSuccess) $ ends
+    let unexpectedAllRevert = allReverts && not shouldFail
+    when conf.debug $ liftIO $ putStrLn $ "symRun -- (cex,warnings,unexpectedAllRevert): " <> show (any isCex results, warnings, unexpectedAllRevert)
+    liftIO $ case (any isCex results, warnings, unexpectedAllRevert) of
+      (False, False, False) -> do
+        -- happy case
+        putStr $ "   \x1b[32m[PASS]\x1b[0m " <> Text.unpack testName <> "\n"
+      (True, _, _) -> do
+        -- there are counterexamples (and maybe other things, but Cex is most important)
+        let x = mapMaybe extractCex results
+            y = symFailure opts testName (fst cd) types x
+        putStr $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n" <> Text.unpack y
+      (_, True, _) -> do
+        -- There are errors/unknowns/partials, we fail them
+        putStr $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n"
+      (_, _, True) -> do
+        -- No cexes/errors/unknowns/partials, but all branches reverted
+        putStr $ "   \x1b[31m[FAIL]\x1b[0m " <> Text.unpack testName <> "\n"
+          <> "   No reachable assertion violations, but all branches reverted\n"
+    liftIO $ printWarnings ends results t
+    pure (not (any isCex results), not (warnings || unexpectedAllRevert))
+
+printWarnings :: [Expr 'End] -> [ProofResult a b c String] -> String -> IO ()
+printWarnings e results testName = do
+  when (any isUnknown results || any isError results || any Expr.isPartial e) $ do
+    putStrLn $ "   \x1b[33m[WARNING]\x1b[0m hevm was only able to partially explore " <> testName <> " due to: ";
+    forM_ (groupIssues (filter isError results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+    forM_ (groupIssues (filter isUnknown results)) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+    forM_ (groupPartials e) $ \(num, str) -> putStrLn $ "      " <> show num <> "x -> " <> str
+  putStrLn ""
+
 symFailure :: UnitTestOptions RealWorld -> Text -> Expr Buf -> [AbiType] -> [(Expr End, SMTCex)] -> Text
 symFailure UnitTestOptions {..} testName cd types failures' =
   mconcat
@@ -278,9 +283,9 @@ symFailure UnitTestOptions {..} testName cd types failures' =
           in Text.pack $ prettyvmresult res
       mkMsg (leaf, cex) = intercalate "\n" $
         ["Counterexample:"
-        ,"  result:   " <> showRes leaf
         ,"  calldata: " <> let ?context = dappContext (traceContext leaf)
                            in prettyCalldata cex cd testName types
+        ,"  result:   " <> showRes leaf
         ] <> verbText leaf
       verbText leaf = case verbose of
             Just _ -> [Text.unlines [ indentLines 2 (showTraceTree' dapp leaf)]]
@@ -323,7 +328,6 @@ failOutput vm UnitTestOptions { .. } testName =
       Just _ -> indentLines 2 (showTraceTree dapp vm)
       _ -> ""
   , indentLines 2 (formatTestLogs dapp.eventMap vm.logs)
-  , "\n"
   ]
 
 formatTestLogs :: (?context :: DappContext) => Map W256 Event -> [Expr Log] -> Text

test/EVM/Test/Utils.hs

@@ -24,9 +24,10 @@ import Data.Maybe (fromMaybe)
 import EVM.Types (internalError)
 import System.Environment (lookupEnv)
 
+-- Returns tuple of (No cex, No warnings)
 runSolidityTestCustom
   :: (MonadMask m, App m)
-  => FilePath -> Text -> Maybe Natural -> Maybe Integer -> Bool -> RpcInfo -> ProjectType -> m Bool
+  => FilePath -> Text -> Maybe Natural -> Maybe Integer -> Bool -> RpcInfo -> ProjectType -> m (Bool, Bool)
 runSolidityTestCustom testFile match timeout maxIter ffiAllowed rpcinfo projectType = do
   withSystemTempDirectory "dapp-test" $ \root -> do
     (compile projectType root testFile) >>= \case
@@ -39,9 +40,10 @@ runSolidityTestCustom testFile match timeout maxIter ffiAllowed rpcinfo projectT
           opts <- liftIO $ testOpts solvers root (Just bo) match maxIter ffiAllowed rpcinfo
           unitTest opts contracts
 
+-- Returns tuple of (No cex, No warnings)
 runSolidityTest
   :: (MonadMask m, App m)
-  => FilePath -> Text -> m Bool
+  => FilePath -> Text -> m (Bool, Bool)
 runSolidityTest testFile match = runSolidityTestCustom testFile match Nothing Nothing True Nothing Foundry
 
 testOpts :: SolverGroup -> FilePath -> Maybe BuildOutput -> Text -> Maybe Integer -> Bool -> RpcInfo -> IO (UnitTestOptions RealWorld)

test/rpc.hs

@@ -72,7 +72,7 @@ tests = testGroup "rpc"
     [ test "dapp-test" $ do
         let testFile = "test/contracts/pass/rpc.sol"
         res <- runSolidityTestCustom testFile ".*" Nothing Nothing False testRpcInfo Foundry
-        liftIO $ assertEqual "test result" True res
+        liftIO $ assertEqual "test result" (True, True) res
 
     -- concretely exec "transfer" on WETH9 using remote rpc
     -- https://etherscan.io/token/0xc02aaa39b223fe8d0a0e5c4f27ead9083c756cc2#code