Merge pull request #591 from ethereum/maybe-smt

Either SMT so we can gracefully handle SMT generation issues such as CopySlice

CHANGELOG.md

@@ -36,6 +36,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   against incorrectly trivial UNSAT queries
 - Allow --num-solvers option for equivalence checking, use num cores by default
 - Preliminary support for multi-threaded Z3
+- Skip over SMT generation issues due to e.g. CopySlice with symbolic arguments, and return
+  partial results instead of erroring out
+- Fix interpreter's MCOPY handling so that it doesn't error out on symbolic arguments
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing

cli/cli.hs

@@ -260,8 +260,10 @@ equivalence cmd = do
     case any isCex res of
       False -> liftIO $ do
         putStrLn "No discrepancies found"
-        when (any isTimeout res) $ do
-          putStrLn "But timeout(s) occurred"
+        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
@@ -345,7 +347,7 @@ assert cmd = do
         showExtras solvers cmd calldata expr
       _ -> do
         let cexs = snd <$> mapMaybe getCex res
-            timeouts = mapMaybe getTimeout res
+            smtUnknowns = mapMaybe getUnknown res
             counterexamples
               | null cexs = []
               | otherwise =
@@ -354,15 +356,15 @@ assert cmd = do
                  , ""
                  ] <> fmap (formatCex (fst calldata) Nothing) cexs
             unknowns
-              | null timeouts = []
+              | null smtUnknowns = []
               | otherwise =
                  [ ""
                  , "Could not determine reachability of the following end state(s):"
                  , ""
-                 ] <> fmap (formatExpr) timeouts
+                 ] <> fmap (formatExpr) smtUnknowns
         liftIO $ T.putStrLn $ T.unlines (counterexamples <> unknowns)
         showExtras solvers cmd calldata expr
-        liftIO $ exitFailure
+        liftIO exitFailure
 
 showExtras :: App m => SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> m ()
 showExtras solvers cmd calldata expr = do

src/EVM.hs

@@ -656,16 +656,22 @@ exec1 = do
                   burn (g_verylow + (unsafeInto g_mcopy)) $
                     accessMemoryRange srcOff sz $ accessMemoryRange dstOff sz $ do
                       next
-                      m <- gets (.state.memory)
-                      case m of
-                        ConcreteMemory mem -> do
-                          buf <- freezeMemory mem
-                          copyBytesToMemory buf sz srcOff dstOff
-                        SymbolicMemory mem -> do
-                          assign (#state % #memory) (SymbolicMemory $ copySlice srcOff dstOff sz mem mem)
-                      assign (#state % #stack) xs
-                _ -> internalError "symbolic size in MCOPY"
+                      mcopy sz srcOff dstOff
+                _ -> do
+                  -- symbolic, ignore gas
+                  next
+                  mcopy sz srcOff dstOff
+              assign (#state % #stack) xs
             _ -> underrun
+            where
+            mcopy sz srcOff dstOff = do
+                  m <- gets (.state.memory)
+                  case m of
+                    ConcreteMemory mem -> do
+                      buf <- freezeMemory mem
+                      copyBytesToMemory buf sz srcOff dstOff
+                    SymbolicMemory mem -> do
+                      assign (#state % #memory) (SymbolicMemory $ copySlice srcOff dstOff sz mem mem)
 
         OpMstore ->
           case stk of

src/EVM/Fetch.hs

@@ -19,7 +19,6 @@ import Data.Text (Text, unpack, pack)
 import Data.Map.Strict qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.List (foldl')
-import Data.Text qualified as T
 import Data.Vector qualified as RegularVector
 import Network.Wreq
 import Network.Wreq.Session (Session)
@@ -200,7 +199,7 @@ oracle solvers info q = do
   case q of
     PleaseDoFFI vals envs continue -> case vals of
        cmd : args -> do
-          existingEnv <- liftIO $ getEnvironment
+          existingEnv <- liftIO getEnvironment
           let mergedEnv = Map.toList $ Map.union envs $ Map.fromList existingEnv
           let process = (proc cmd args :: CreateProcess) { env = Just mergedEnv }
           (_, stdout', _) <- liftIO $ readCreateProcessWithExitCode process ""
@@ -259,9 +258,7 @@ checkBranch solvers branchcondition pathconditions = do
         Unsat -> pure $ Case True
         -- Yes. Both branches possible
         Sat _ -> pure EVM.Types.Unknown
-        -- Explore both branches in case of timeout
-        EVM.Solvers.Unknown -> pure EVM.Types.Unknown
-        Error e -> internalError $ "SMT Solver pureed with an error: " <> T.unpack e
-    -- If the query times out, we simply explore both paths
-    EVM.Solvers.Unknown -> pure EVM.Types.Unknown
-    Error e -> internalError $ "SMT Solver pureed with an error: " <> T.unpack e
+    -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
+        _ -> pure EVM.Types.Unknown
+    -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
+    _ -> pure EVM.Types.Unknown