[DRAFT - do not review] Soft errors

CHANGELOG.md

@@ -30,6 +30,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

@@ -239,7 +239,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
@@ -265,15 +265,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
@@ -118,61 +127,70 @@ bool :: Expr EWord -> Prop
 bool e = POr (PEq (Lit 1) e) (PEq (Lit 0) e)
 
 -- | Abstract calldata argument generation
-symAbiArg :: Text -> AbiType -> CalldataFragment
+symAbiArg :: Text -> AbiType -> Err CalldataFragment
 symAbiArg name = \case
   AbiUIntType n ->
     if n `mod` 8 == 0 && n <= 256
-    then St [Expr.inRange n v] v
-    else internalError "bad type"
+    then pure $ St [Expr.inRange n v] v
+    else Left "bad type"
   AbiIntType n ->
     if n `mod` 8 == 0 && n <= 256
     -- TODO: is this correct?
-    then St [Expr.inRange n v] v
-    else internalError "bad type"
-  AbiBoolType -> St [bool v] v
-  AbiAddressType -> St [] (WAddr (SymAddr name))
+    then pure $ St [Expr.inRange n v] v
+    else Left "bad type"
+  AbiBoolType -> pure $ St [bool v] v
+  AbiAddressType -> pure $ St [] (WAddr (SymAddr name))
   AbiBytesType n ->
     if n > 0 && n <= 32
-    then St [Expr.inRange (n * 8) v] v
-    else internalError "bad type"
-  AbiArrayType sz tps -> do
-    Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg (name <> "-a-" <> i) tp) $ (V.replicate sz tps)
-  AbiTupleType tps ->
-    Comp . V.toList . V.imap (\(T.pack . show -> i) tp -> symAbiArg (name <> "-t-" <> i) tp) $ tps
-  t -> internalError $ "TODO: symbolic abi encoding for " <> show t
+    then pure $ St [Expr.inRange (n * 8) v] v
+    else Left "bad type"
+  AbiArrayType sz tps -> pure . Comp =<< mapM (fun "a") (zip [0..] (replicate sz tps))
+  AbiTupleType tps    -> pure . Comp =<< mapM (fun "a") (zip [0..] (V.toList tps))
+  t -> Left $ "TODO: symbolic abi encoding for " <> show t
   where
     v = Var name
+    fun :: Text -> (Int, AbiType) -> Err CalldataFragment
+    fun n (i, tp) = symAbiArg (name <> "-" <> n <> "-" <> (T.pack . show $ i)) tp
 
 data CalldataFragment
   = St [Prop] (Expr EWord)
   | Dy [Prop] (Expr EWord) (Expr Buf)
   | Comp [CalldataFragment]
   deriving (Show, Eq)
 
+zipWith3M :: Monad m => (a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d]
+zipWith3M _ [] _ _ = pure []
+zipWith3M _ _ [] _ = pure []
+zipWith3M _ _ _ [] = pure []
+zipWith3M f (x:xs) (y:ys) (z:zs) = do
+    result <- f x y z
+    rest <- zipWith3M f xs ys zs
+    pure (result : rest)
+
 -- | Generates calldata matching given type signature, optionally specialized
 -- with concrete arguments.
 -- Any argument given as "<symbolic>" or omitted at the tail of the list are
 -- kept symbolic.
-symCalldata :: Text -> [AbiType] -> [String] -> Expr Buf -> (Expr Buf, [Prop])
-symCalldata sig typesignature concreteArgs base =
+symCalldata :: Text -> [AbiType] -> [String] -> Expr Buf -> Err (Expr Buf, [Prop])
+symCalldata sig typesignature concreteArgs base = do
   let
     args = concreteArgs <> replicate (length typesignature - length concreteArgs) "<symbolic>"
-    mkArg :: AbiType -> String -> Int -> CalldataFragment
+    mkArg :: AbiType -> String -> Int -> Err CalldataFragment
     mkArg typ "<symbolic>" n = symAbiArg (T.pack $ "arg" <> show n) typ
     mkArg typ arg _ =
       case makeAbiValue typ arg of
-        AbiUInt _ w -> St [] . Lit . into $ w
-        AbiInt _ w -> St [] . Lit . unsafeInto $ w
-        AbiAddress w -> St [] . Lit . into $ w
-        AbiBool w -> St [] . Lit $ if w then 1 else 0
-        _ -> internalError "TODO"
-    calldatas = zipWith3 mkArg typesignature args [1..]
-    (cdBuf, props) = combineFragments calldatas base
-    withSelector = writeSelector cdBuf sig
-    sizeConstraints
-      = (Expr.bufLength withSelector .>= cdLen calldatas)
-      .&& (Expr.bufLength withSelector .< (Lit (2 ^ (64 :: Integer))))
-  in (withSelector, sizeConstraints : props)
+        AbiUInt _ w  -> pure $ St [] . Lit . into $ w
+        AbiInt _ w   -> pure $ St [] . Lit . unsafeInto $ w
+        AbiAddress w -> pure $ St [] . Lit . into $ w
+        AbiBool w    -> pure $ St [] . Lit $ if w then 1 else 0
+        _ -> Left "Can't handle this symbolic type"
+  calldatas <- zipWith3M mkArg typesignature args [1..]
+  let (cdBuf, props) = combineFragments calldatas base
+      withSelector = writeSelector cdBuf sig
+      sizeConstraints
+        = (Expr.bufLength withSelector .>= cdLen calldatas)
+        .&& (Expr.bufLength withSelector .< (Lit (2 ^ (64 :: Integer))))
+  pure (withSelector, sizeConstraints : props)
 
 cdLen :: [CalldataFragment] -> Expr EWord
 cdLen = go (Lit 4)
@@ -466,6 +484,10 @@ allPanicCodes = [0x00, 0x01, 0x11, 0x12, 0x21, 0x22, 0x31, 0x32, 0x41, 0x51]
 panicMsg :: Word256 -> ByteString
 panicMsg err = selector "Panic(uint256)" <> encodeAbiValue (AbiUInt 256 err)
 
+getRight :: Err b -> b
+getRight (Right y) = y
+getRight (Left err)  = internalError err
+
 -- | Builds a buffer representing calldata from the provided method description
 -- and concrete arguments
 mkCalldata :: Maybe Sig -> [String] -> (Expr Buf, [Prop])
@@ -477,8 +499,7 @@ mkCalldata Nothing _ =
   -- TODO: can we encode calldata as an array with a smaller length?
   , [Expr.bufLength (AbstractBuf "txdata") .< (Lit (2 ^ (64 :: Integer)))]
   )
-mkCalldata (Just (Sig name types)) args =
-  symCalldata name types args (AbstractBuf "txdata")
+mkCalldata (Just (Sig name types)) args = getRight $ symCalldata name types args (AbstractBuf "txdata")
 
 verifyContract
   :: App m
@@ -575,6 +596,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 +631,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 +699,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 +728,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 +751,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)