Merge pull request #447 from ethereum/limit-vmresult

Limit VMResult cases when concrete

cli/cli.hs

@@ -397,9 +397,6 @@ launchExec cmd = do
       Just (VMFailure err) -> liftIO $ do
         putStrLn $ "Error: " <> show err
         exitWith (ExitFailure 2)
-      Just (Unfinished p) -> liftIO $ do
-        putStrLn $ "Could not continue execution: " <> show p
-        exitWith (ExitFailure 2)
       Just (VMSuccess buf) -> liftIO $ do
         let msg = case buf of
               ConcreteBuf msg' -> msg'

src/EVM.hs

@@ -1251,32 +1251,11 @@ getCodeLocation vm = (vm.state.contract, vm.state.pc)
 query :: Query t s -> EVM t s ()
 query = assign #result . Just . HandleEffect . Query
 
-choose :: Choose t s -> EVM t s ()
+choose :: Choose s -> EVM Symbolic s ()
 choose = assign #result . Just . HandleEffect . Choose
 
-branch :: forall t s. Expr EWord -> (Bool -> EVM t s ()) -> EVM t s ()
-branch cond continue = do
-  loc <- codeloc
-  pathconds <- use #constraints
-  query $ PleaseAskSMT cond pathconds (choosePath loc)
-  where
-    condSimp = Expr.simplify cond
-    condSimpConc = Expr.concKeccakSimpExpr condSimp
-    choosePath :: CodeLocation -> BranchCondition -> EVM t s ()
-    choosePath loc (Case v) = do
-      assign #result Nothing
-      pushTo #constraints $ if v then Expr.simplifyProp (condSimpConc ./= Lit 0) else Expr.simplifyProp (condSimpConc .== Lit 0)
-      (iteration, _) <- use (#iterations % at loc % non (0,[]))
-      stack <- use (#state % #stack)
-      assign (#cache % #path % at (loc, iteration)) (Just v)
-      assign (#iterations % at loc) (Just (iteration + 1, stack))
-      continue v
-    -- Both paths are possible; we ask for more input
-    choosePath loc Unknown =
-      choose . PleaseChoosePath condSimp $ choosePath loc . Case
-
 -- | Construct RPC Query and halt execution until resolved
-fetchAccount :: Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
+fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
 fetchAccount addr continue =
   use (#env % #contracts % at addr) >>= \case
     Just c -> continue c
@@ -1300,7 +1279,7 @@ fetchAccount addr continue =
       GVar _ -> internalError "Unexpected GVar"
 
 accessStorage
-  :: Expr EAddr
+  :: VMOps t => Expr EAddr
   -> Expr EWord
   -> (Expr EWord -> EVM t s ())
   -> EVM t s ()
@@ -1448,42 +1427,42 @@ notStatic continue = do
     then vmError StateChangeWhileStatic
     else continue
 
-forceAddr :: Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()
+forceAddr :: VMOps t => Expr EWord -> String -> (Expr EAddr -> EVM t s ()) -> EVM t s ()
 forceAddr n msg continue = case wordToAddr n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])
   Just c -> continue c
 
-forceConcrete :: Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
+forceConcrete :: VMOps t => Expr EWord -> String -> (W256 -> EVM t s ()) -> EVM t s ()
 forceConcrete n msg continue = case maybeLitWord n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])
   Just c -> continue c
 
-forceConcreteAddr :: Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()
+forceConcreteAddr :: VMOps t => Expr EAddr -> String -> (Addr -> EVM t s ()) -> EVM t s ()
 forceConcreteAddr n msg continue = case maybeLitAddr n of
   Nothing -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n])
   Just c -> continue c
 
-forceConcreteAddr2 :: (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()
+forceConcreteAddr2 :: VMOps t => (Expr EAddr, Expr EAddr) -> String -> ((Addr, Addr) -> EVM t s ()) -> EVM t s ()
 forceConcreteAddr2 (n,m) msg continue = case (maybeLitAddr n, maybeLitAddr m) of
   (Just c, Just d) -> continue (c,d)
   _ -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])
 
-forceConcrete2 :: (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()
+forceConcrete2 :: VMOps t => (Expr EWord, Expr EWord) -> String -> ((W256, W256) -> EVM t s ()) -> EVM t s ()
 forceConcrete2 (n,m) msg continue = case (maybeLitWord n, maybeLitWord m) of
   (Just c, Just d) -> continue (c, d)
   _ -> do
     vm <- get
     partial $ UnexpectedSymbolicArg vm.state.pc msg (wrap [n, m])
 
-forceConcreteBuf :: Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s ()
+forceConcreteBuf :: VMOps t => Expr Buf -> String -> (ByteString -> EVM t s ()) -> EVM t s ()
 forceConcreteBuf (ConcreteBuf b) _ continue = continue b
 forceConcreteBuf b msg _ = do
     vm <- get
@@ -1910,9 +1889,6 @@ resetState = do
 vmError :: VMOps t => EvmError -> EVM t s ()
 vmError e = finishFrame (FrameErrored e)
 
-partial :: PartialExec -> EVM t s ()
-partial e = assign #result (Just (Unfinished e))
-
 wrap :: Typeable a => [Expr a] -> [SomeExpr]
 wrap = fmap SomeExpr
 
@@ -2287,7 +2263,7 @@ checkJump x xs = noJumpIntoInitData x $ do
     False -> vmError BadJumpDestination
 
 -- fails with partial if we're trying to jump into the symbolic region of an `InitCode`
-noJumpIntoInitData :: Int -> EVM t s () -> EVM t s ()
+noJumpIntoInitData :: VMOps t => Int -> EVM t s () -> EVM t s ()
 noJumpIntoInitData idx cont = do
   vm <- get
   case vm.state.code of
@@ -2595,6 +2571,27 @@ instance VMOps Symbolic where
   toGas _ = ()
   whenSymbolicElse a _ = a
 
+  partial e = assign #result (Just (Unfinished e))
+  branch cond continue = do
+    loc <- codeloc
+    pathconds <- use #constraints
+    query $ PleaseAskSMT cond pathconds (choosePath loc)
+    where
+      condSimp = Expr.simplify cond
+      condSimpConc = Expr.concKeccakSimpExpr condSimp
+      choosePath loc (Case v) = do
+        assign #result Nothing
+        pushTo #constraints $ if v then Expr.simplifyProp (condSimpConc ./= Lit 0)
+                                   else Expr.simplifyProp (condSimpConc .== Lit 0)
+        (iteration, _) <- use (#iterations % at loc % non (0,[]))
+        stack <- use (#state % #stack)
+        assign (#cache % #path % at (loc, iteration)) (Just v)
+        assign (#iterations % at loc) (Just (iteration + 1, stack))
+        continue v
+      -- Both paths are possible; we ask for more input
+      choosePath loc Unknown =
+        choose . PleaseChoosePath condSimp $ choosePath loc . Case
+
 instance VMOps Concrete where
   burn' n continue = do
     available <- use (#state % #gas)
@@ -2724,6 +2721,10 @@ instance VMOps Concrete where
 
   whenSymbolicElse _ a = a
 
+  partial _ = internalError "won't happen during concrete exec"
+
+  branch (forceLit -> cond) continue = continue (cond > 0)
+
 -- Create symbolic VM from concrete VM
 symbolify :: VM Concrete s -> VM Symbolic s
 symbolify vm =
@@ -2745,7 +2746,6 @@ symbolifyResult result =
     HandleEffect _ -> internalError "shouldn't happen"
     VMFailure e -> VMFailure e
     VMSuccess b -> VMSuccess b
-    Unfinished p -> Unfinished p
 
 forceLit :: Expr EWord -> W256
 forceLit (Lit w) = w

src/EVM/Stepper.hs

@@ -34,7 +34,6 @@ import EVM.Types
 import Control.Monad.ST (stToIO, RealWorld)
 import Control.Monad.IO.Class
 import EVM.Effects
-import EVM.Expr (concKeccakSimpExpr)
 
 -- | The instruction type of the operational monad
 data Action t s a where
@@ -46,7 +45,7 @@ data Action t s a where
   Wait :: Query t s -> Action t s ()
 
   -- | Multiple things can happen
-  Ask :: Choose t s -> Action t s ()
+  Ask :: Choose s -> Action Symbolic s ()
 
   -- | Embed a VM state transformation
   EVM  :: EVM t s a -> Action t s a
@@ -68,7 +67,7 @@ run = exec >> evm get
 wait :: Query t s -> Stepper t s ()
 wait = singleton . Wait
 
-ask :: Choose t s -> Stepper t s ()
+ask :: Choose s -> Stepper Symbolic s ()
 ask = singleton . Ask
 
 evm :: EVM t s a -> Stepper t s a
@@ -78,19 +77,15 @@ evmIO :: IO a -> Stepper t s a
 evmIO = singleton . IOAct
 
 -- | Run the VM until final result, resolving all queries
-execFully :: Stepper t s (Either EvmError (Expr Buf))
+execFully :: Stepper Concrete s (Either EvmError (Expr Buf))
 execFully =
   exec >>= \case
     HandleEffect (Query q) ->
       wait q >> execFully
-    HandleEffect (Choose q) ->
-      ask q >> execFully
     VMFailure x ->
       pure (Left x)
     VMSuccess x ->
       pure (Right x)
-    Unfinished x
-      -> internalError $ "partial execution encountered during concrete execution: " <> show x
 
 -- | Run the VM until its final state
 runFully :: Stepper t s (VM t s)
@@ -123,19 +118,12 @@ interpret fetcher vm = eval . view
         Exec -> do
           (r, vm') <- liftIO $ stToIO $ runStateT EVM.Exec.exec vm
           interpret fetcher vm' (k r)
-        Wait (PleaseAskSMT expr _ continue) -> case (concKeccakSimpExpr expr) of
-          Lit c -> do
-            (r, vm') <- liftIO $ stToIO $ runStateT (continue (Case (c > 0))) vm
-            interpret fetcher vm' (k r)
-          _ ->  internalError $ "cannot handle symbolic branch conditions in this interpreter: " <> show expr
         Wait q -> do
           m <- fetcher q
           vm' <- liftIO $ stToIO $ execStateT m vm
           interpret fetcher vm' (k ())
-        Ask _ ->
-          internalError "cannot make choices with this interpreter"
         IOAct m -> do
-          r <- liftIO $ m
+          r <- liftIO m
           interpret fetcher vm (k r)
         EVM m -> do
           (r, vm') <- liftIO $ stToIO $ runStateT m vm

src/EVM/Types.hs

@@ -546,21 +546,21 @@ data PartialExec
   deriving (Show, Eq, Ord)
 
 -- | Effect types used by the vm implementation for side effects & control flow
-data Effect t s
-  = Query (Query t s)
-  | Choose (Choose t s)
+data Effect t s where
+  Query :: Query t s -> Effect t s
+  Choose :: Choose s -> Effect Symbolic s
 deriving instance Show (Effect t s)
 
 -- | Queries halt execution until resolved through RPC calls or SMT queries
 data Query t s where
   PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s
   PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s
-  PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM t s ()) -> Query t s
+  PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s
   PleaseDoFFI         :: [String] -> (ByteString -> EVM t s ()) -> Query t s
 
 -- | Execution could proceed down one of two branches
-data Choose t s where
-  PleaseChoosePath    :: Expr EWord -> (Bool -> EVM t s ()) -> Choose t s
+data Choose s where
+  PleaseChoosePath    :: Expr EWord -> (Bool -> EVM Symbolic s ()) -> Choose s
 
 -- | The possible return values of a SMT query
 data BranchCondition = Case Bool | Unknown
@@ -581,17 +581,17 @@ instance Show (Query t s) where
     PleaseDoFFI cmd _ ->
       (("<EVM.Query: do ffi: " ++ (show cmd)) ++)
 
-instance Show (Choose t s) where
+instance Show (Choose s) where
   showsPrec _ = \case
     PleaseChoosePath _ _ ->
       (("<EVM.Choice: waiting for user to select path (0,1)") ++)
 
 -- | The possible result states of a VM
-data VMResult t s
-  = VMFailure EvmError      -- ^ An operation failed
-  | VMSuccess (Expr Buf)    -- ^ Reached STOP, RETURN, or end-of-code
-  | HandleEffect (Effect t s) -- ^ An effect must be handled for execution to continue
-  | Unfinished PartialExec  -- ^ Execution could not continue further
+data VMResult (t :: VMType) s where
+  Unfinished :: PartialExec -> VMResult Symbolic s -- ^ Execution could not continue further
+  VMFailure :: EvmError -> VMResult t s            -- ^ An operation failed
+  VMSuccess :: (Expr Buf) -> VMResult t s          -- ^ Reached STOP, RETURN, or end-of-code
+  HandleEffect :: (Effect t s) -> VMResult t s     -- ^ An effect must be handled for execution to continue
 
 deriving instance Show (VMResult t s)
 
@@ -796,6 +796,9 @@ class VMOps (t :: VMType) where
 
   whenSymbolicElse :: EVM t s a -> EVM t s a -> EVM t s a
 
+  partial :: PartialExec -> EVM t s ()
+  branch :: Expr EWord -> (Bool -> EVM t s ()) -> EVM t s ()
+
 -- Bytecode Representations ------------------------------------------------------------------------
 
 

src/EVM/UnitTest.hs

@@ -110,7 +110,7 @@ unitTest opts (Contracts cs) = do
 
 -- | Assuming a constructor is loaded, this stepper will run the constructor
 -- to create the test contract, give it an initial balance, and run `setUp()'.
-initializeUnitTest :: VMOps t => UnitTestOptions s -> SolcContract -> Stepper t s ()
+initializeUnitTest :: UnitTestOptions s -> SolcContract -> Stepper Concrete s ()
 initializeUnitTest opts theContract = do
 
   let addr = opts.testParams.address

test/EVM/Test/Tracing.hs

@@ -576,17 +576,12 @@ interpretWithTrace fetcher =
       case action of
         Stepper.Exec ->
           execWithTrace >>= interpretWithTrace fetcher . k
-        Stepper.Wait q -> case q of
-          PleaseAskSMT (Lit x) _ continue ->
-            interpretWithTrace fetcher (Stepper.evm (continue (Case (x > 0))) >>= k)
-          _ -> do
-            m <- State.lift $ fetcher q
-            vm <- use _1
-            vm' <- liftIO $ stToIO $ State.execStateT m vm
-            assign _1 vm'
-            interpretWithTrace fetcher (k ())
-        Stepper.Ask _ ->
-          internalError "cannot make choice in this interpreter"
+        Stepper.Wait q -> do
+          m <- State.lift $ fetcher q
+          vm <- use _1
+          vm' <- liftIO $ stToIO $ State.execStateT m vm
+          assign _1 vm'
+          interpretWithTrace fetcher (k ())
         Stepper.IOAct q ->
           liftIO q >>= interpretWithTrace fetcher . k
         Stepper.EVM m -> do

test/test.hs

@@ -3544,7 +3544,7 @@ runSimpleVM x ins = do
          vm' = set (#state % #calldata) calldata vm
      res <- Stepper.interpret (Fetch.zero 0 Nothing) vm' Stepper.execFully
      case res of
-       (Right (ConcreteBuf bs)) -> pure $ Just bs
+       Right (ConcreteBuf bs) -> pure $ Just bs
        s -> internalError $ show s
 
 -- | Takes a creation code and returns a vm with the result of executing the creation code
@@ -3553,18 +3553,19 @@ loadVM x = do
   vm <- liftIO $ stToIO $ vmForEthrunCreation x
   vm1 <- Stepper.interpret (Fetch.zero 0 Nothing) vm Stepper.runFully
   case vm1.result of
-     Just (VMSuccess (ConcreteBuf targetCode)) -> do
-       let target = vm1.state.contract
-       vm2 <- Stepper.interpret (Fetch.zero 0 Nothing) vm1 (prepVm target targetCode >> Stepper.run)
-       writeTrace vm2
-       pure $ Just vm2
-     _ -> pure Nothing
+    Just (VMSuccess (ConcreteBuf targetCode)) -> do
+      let target = vm1.state.contract
+      vm2 <- Stepper.interpret (Fetch.zero 0 Nothing) vm1 (prepVm target targetCode)
+      writeTrace vm2
+      pure $ Just vm2
+    _ -> pure Nothing
   where
     prepVm target targetCode = Stepper.evm $ do
       replaceCodeOfSelf (RuntimeCode $ ConcreteRuntimeCode targetCode)
       resetState
       assign (#state % #gas) 0xffffffffffffffff -- kludge
       execState (loadContract target) <$> get >>= put
+      get
 
 hex :: ByteString -> ByteString
 hex s =