Merge pull request #700 from ethereum/martin-unify-two-types

Unifying result type

Author: msooseth

CHANGELOG.md

@@ -88,6 +88,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - block.number can now be symbolic. This only affects library use of hevm
 - Removed `--smtoutput` since it was never used
 - We now build with -DCMAKE_POLICY_VERSION_MINIMUM=3.5 libff, as cmake deprecated 3.5
+- CheckSatResult has now been unified with ProofResult via SMTResult
 
 ## [0.54.2] - 2024-12-12
 

cli/cli.hs

@@ -495,12 +495,12 @@ assert cFileOpts sOpts cExecOpts cOpts = do
     }
     (expr, res) <- verify solvers veriOpts preState (Just $ checkAssertions errCodes)
     case res of
-      [Qed _] -> do
+      [Qed] -> do
         liftIO $ putStrLn "\nQED: No reachable property violations discovered\n"
         showExtras solvers sOpts calldata expr
       _ -> do
         let cexs = snd <$> mapMaybe getCex res
-            smtUnknowns = mapMaybe getUnknown res
+            smtUnknowns = snd <$> mapMaybe getUnknown res
             counterexamples
               | null cexs = []
               | otherwise =
@@ -528,7 +528,7 @@ showExtras solvers sOpts calldata expr = do
   when sOpts.showReachableTree $ do
     reached <- reachable solvers expr
     liftIO $ do
-      putStrLn "=== Reachable Expression ===\n"
+      putStrLn "=== Potentially Reachable Expression ===\n"
       T.putStrLn (formatExpr . snd $ reached)
       putStrLn ""
   when sOpts.getModels $ do

src/EVM.hs

@@ -3009,7 +3009,7 @@ instance VMOps Symbolic where
         assign (#iterations % at loc) (Just (iteration + 1, stack))
         continue v
       -- Both paths are possible; we ask for more input
-      runBothPaths loc exploreDepth Unknown =
+      runBothPaths loc exploreDepth UnknownBranch =
         (runBoth depthLimit exploreDepth ) . PleaseRunBoth condSimp $ (runBothPaths loc exploreDepth) . Case
 
   -- numBytes allows us to specify how many bytes of the returned value is relevant

src/EVM/Fetch.hs

@@ -275,17 +275,17 @@ checkBranch solvers branchcondition pathconditions = do
   let props = [pathconditions .&& branchcondition]
   checkSatWithProps solvers props >>= \case
     -- the condition is unsatisfiable
-    (Unsat, _) -> -- if pathconditions are consistent then the condition must be false
+    (Qed, _) -> -- if pathconditions are consistent then the condition must be false
       pure $ Case False
     -- Sat means its possible for condition to hold
-    (Sat {}, _) -> do -- is its negation also possible?
+    (Cex {}, _) -> do -- is its negation also possible?
       let propsNeg = [pathconditions .&& (PNeg branchcondition)]
       checkSatWithProps solvers propsNeg >>= \case
         -- No. The condition must hold
-        (Unsat, _) -> pure $ Case True
+        (Qed, _) -> pure $ Case True
         -- Yes. Both branches possible
-        (Sat {}, _) -> pure EVM.Types.Unknown
+        (Cex {}, _) -> pure UnknownBranch
         -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
-        _ -> pure EVM.Types.Unknown
+        _ -> pure UnknownBranch
     -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
-    _ -> pure EVM.Types.Unknown
+    _ -> pure UnknownBranch

src/EVM/Fuzz.hs

@@ -15,7 +15,7 @@ import Data.Word (Word8)
 
 import EVM.Expr qualified as Expr
 import EVM.Expr (bytesToW256)
-import EVM.SMT qualified as SMT (BufModel(..), SMTCex(..))
+import EVM.Types qualified as SMT
 import EVM.Traversals
 import EVM.Types (Prop(..), W256, Expr(..), EType(..), internalError, keccak')
 

src/EVM/SMT.hs

@@ -77,56 +77,6 @@ instance Monoid CexVars where
       , txContext = mempty
       }
 
--- | A model for a buffer, either in it's compressed form (for storing parsed
--- models from a solver), or as a bytestring (for presentation to users)
-data BufModel
-  = Comp CompressedBuf
-  | Flat ByteString
-  deriving (Eq)
-instance Show BufModel where
-  show (Comp c) = "Comp " <> show c
-  show (Flat b) = "Flat 0x" <> bsToHex b
-
--- | This representation lets us store buffers of arbitrary length without
--- exhausting the available memory, it closely matches the format used by
--- smt-lib when returning models for arrays
-data CompressedBuf
-  = Base { byte :: Word8, length :: W256}
-  | Write { byte :: Word8, idx :: W256, next :: CompressedBuf }
-  deriving (Eq, Show)
-
-
--- | a final post shrinking cex, buffers here are all represented as concrete bytestrings
-data SMTCex = SMTCex
-  { vars :: Map (Expr EWord) W256
-  , addrs :: Map (Expr EAddr) Addr
-  , buffers :: Map (Expr Buf) BufModel
-  , store :: Map (Expr EAddr) (Map W256 W256)
-  , blockContext :: Map (Expr EWord) W256
-  , txContext :: Map (Expr EWord) W256
-  }
-  deriving (Eq, Show)
-
-instance Semigroup SMTCex where
-  a <> b = SMTCex
-    { vars = a.vars <> b.vars
-    , addrs = a.addrs <> b.addrs
-    , buffers = a.buffers <> b.buffers
-    , store = a.store <> b.store
-    , blockContext = a.blockContext <> b.blockContext
-    , txContext = a.txContext <> b.txContext
-    }
-
-instance Monoid SMTCex where
-  mempty = SMTCex
-    { vars = mempty
-    , addrs = mempty
-    , buffers = mempty
-    , store = mempty
-    , blockContext = mempty
-    , txContext = mempty
-    }
-
 flattenBufs :: SMTCex -> Maybe SMTCex
 flattenBufs cex = do
   bs <- mapM collapse cex.buffers

src/EVM/Solvers.hs

@@ -77,25 +77,9 @@ data MultiData = MultiData
 
 data SingleData = SingleData
   { smt2 :: SMT2
-  , resultChan :: Chan CheckSatResult
+  , resultChan :: Chan SMTResult
   }
 
--- | The result of a call to (check-sat)
-data CheckSatResult
-  = Sat SMTCex
-  | Unsat
-  | Unknown String
-  | Error String
-  deriving (Show, Eq)
-
-isSat :: CheckSatResult -> Bool
-isSat (Sat _) = True
-isSat _ = False
-
-isUnsat :: CheckSatResult -> Bool
-isUnsat Unsat = True
-isUnsat _ = False
-
 checkMulti :: SolverGroup -> Err SMT2 -> MultiSol -> IO (Maybe [W256])
 checkMulti (SolverGroup taskQueue) smt2 multiSol = do
   if isLeft smt2 then pure Nothing
@@ -107,20 +91,20 @@ checkMulti (SolverGroup taskQueue) smt2 multiSol = do
     -- collect result
     readChan resChan
 
-checkSatWithProps :: App m => SolverGroup -> [Prop] -> m (CheckSatResult, Err SMT2)
+checkSatWithProps :: App m => SolverGroup -> [Prop] -> m (SMTResult, Err SMT2)
 checkSatWithProps (SolverGroup taskQueue) props = do
   conf <- readConfig
   let psSimp = simplifyProps props
-  if psSimp == [PBool False] then pure (Unsat, Right mempty)
+  if psSimp == [PBool False] then pure (Qed, Right mempty)
   else do
     let smt2 = assertProps conf psSimp
     if isLeft smt2 then
-      let err = getError smt2 in pure (EVM.Solvers.Unknown err, Left err)
+      let err = getError smt2 in pure (Error err, Left err)
     else do
       res <- liftIO $ checkSat (SolverGroup taskQueue) smt2
       pure (res, Right (getNonError smt2))
 
-checkSat :: SolverGroup -> Err SMT2 -> IO CheckSatResult
+checkSat :: SolverGroup -> Err SMT2 -> IO SMTResult
 checkSat (SolverGroup taskQueue) smt2 = do
   if isLeft smt2 then pure $ Error $ getError smt2
   else do
@@ -227,7 +211,7 @@ getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCo
           when conf.debug $ putStrLn $ "Unable to write SMT to solver: " <> (T.unpack err)
           writeChan r Nothing
 
-getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> (Chan CheckSatResult) -> SolverInstance -> Chan SolverInstance -> Int -> m ()
+getOneSol :: (MonadIO m, ReadConfig m) => SMT2 -> (Chan SMTResult) -> SolverInstance -> Chan SolverInstance -> Int -> m ()
 getOneSol smt2@(SMT2 cmds cexvars ps) r inst availableInstances fileCounter = do
   conf <- readConfig
   let fuzzResult = tryCexFuzz ps conf.numCexFuzz
@@ -236,7 +220,7 @@ getOneSol smt2@(SMT2 cmds cexvars ps) r inst availableInstances fileCounter = do
     if (isJust fuzzResult)
       then do
         when (conf.debug) $ putStrLn $ "   Cex found via fuzzing:" <> (show fuzzResult)
-        writeChan r (Sat $ fromJust fuzzResult)
+        writeChan r (Cex $ fromJust fuzzResult)
       else if Prelude.not conf.onlyCexFuzz then do
         -- reset solver and send all lines of provided script
         out <- sendScript inst ("(reset)" : cmds)
@@ -248,10 +232,10 @@ getOneSol smt2@(SMT2 cmds cexvars ps) r inst availableInstances fileCounter = do
             sat <- sendLine inst "(check-sat)"
             res <- do
                 case sat of
-                  "unsat" -> pure Unsat
-                  "timeout" -> pure $ EVM.Solvers.Unknown "Result timeout by SMT solver"
-                  "unknown" -> pure $ EVM.Solvers.Unknown "Result unknown by SMT solver"
-                  "sat" -> Sat <$> getModel inst cexvars
+                  "unsat" -> pure Qed
+                  "timeout" -> pure $ Unknown "Result timeout by SMT solver"
+                  "unknown" -> pure $ Unknown "Result unknown by SMT solver"
+                  "sat" -> Cex <$> getModel inst cexvars
                   _ -> pure . Error $ "Unable to parse SMT solver output: " <> T.unpack sat
             writeChan r res
       else do