Create Err SMT

Adding some tests, better internal errors

Fixing

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

src/EVM.hs

@@ -663,8 +663,17 @@ exec1 = do
  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"
+ _ -> do
+ -- symbolic, ignore gas
+ 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
  _ -> underrun
 
  OpMstore ->

src/EVM/Fetch.hs

@@ -200,7 +200,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 ""
@@ -260,8 +260,8 @@ checkBranch solvers branchcondition pathconditions = do
  -- 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
+ EVM.Solvers.Unknown _ -> pure EVM.Types.Unknown
+ Error e -> internalError $ "SMT Solver returned with error: " <> T.unpack e
+ -- If the query times out, or can't be executed (e.g. symbolic copyslice) we simply explore both paths
+ EVM.Solvers.Unknown _ -> pure EVM.Types.Unknown
+ Error e -> internalError $ "SMT Solver returned with error: " <> T.unpack e