HEVM: WIP pass contract map to behaviours

src/HEVM.hs

@@ -12,7 +12,8 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE TypeApplications #-}
-
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE NoFieldSelectors #-}
 
 module HEVM where
 
@@ -32,22 +33,21 @@ import Control.Monad
 import Data.DoubleWord
 import Data.Maybe
 import System.Exit ( exitFailure )
-import Control.Monad.ST (stToIO)
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
 
 import Syntax.Annotated
 import Syntax.Untyped (makeIface)
 import Syntax
 import HEVM_utils
 
-import qualified EVM.Types as EVM hiding (Contract(..))
+import qualified EVM.Types as EVM
+import qualified EVM as EVM
 import EVM.Expr hiding (op2, inRange)
 import EVM.SymExec hiding (EquivResult, isPartial)
 import qualified EVM.SymExec as SymExec (EquivResult)
 import EVM.SMT (SMTCex(..), assertProps, formatSMT2)
 import EVM.Solvers
 import qualified EVM.Format as Format
-import qualified EVM.Fetch as Fetch
 
 import Debug.Trace
 
@@ -81,9 +81,9 @@ slotMap store =
 
 -- * Act translation
 
-translateActBehvs :: CodeMap -> Store -> [Behaviour] -> BS.ByteString -> [(Id, [EVM.Expr EVM.End], Calldata)]
-translateActBehvs codemap store behvs bytecode =
-  translateBehvs codemap (slotMap store) bytecode behvs
+translateActBehvs :: CodeMap -> Store -> [Behaviour] -> BS.ByteString -> ContractMap -> [(Id, [EVM.Expr EVM.End], Calldata)]
+translateActBehvs codemap store behvs bytecode cmap =
+  translateBehvs codemap (slotMap store) bytecode cmap behvs
 
 translateActConstr :: CodeMap -> Store -> Contract -> BS.ByteString -> ([EVM.Expr EVM.End], Calldata)
 translateActConstr codemap store (Contract ctor _) bytecode = translateConstructor codemap (slotMap store) ctor bytecode
@@ -112,10 +112,10 @@ translateConstructor codemap layout (Constructor cid iface preconds _ _ upds _)
                  Nothing -> error "Internal error: init contract not found"
 
 
-translateBehvs :: CodeMap -> Layout -> BS.ByteString -> [Behaviour] -> [(Id, [EVM.Expr EVM.End], Calldata)]
-translateBehvs codemap layout bytecode behvs =
+translateBehvs :: CodeMap -> Layout -> BS.ByteString -> ContractMap -> [Behaviour] -> [(Id, [EVM.Expr EVM.End], Calldata)]
+translateBehvs codemap layout bytecode cmap behvs =
   let groups = (groupBy sameIface behvs) :: [[Behaviour]] in
-  fmap (\behvs' -> (behvName behvs', fmap (translateBehv codemap layout bytecode) behvs', behvCalldata behvs')) groups
+  fmap (\behvs' -> (behvName behvs', fmap (translateBehv codemap layout bytecode cmap) behvs', behvCalldata behvs')) groups
   where
 
     behvCalldata (Behaviour _ _ iface _ _ _ _ _:_) = makeCalldata iface
@@ -128,23 +128,16 @@ translateBehvs codemap layout bytecode behvs =
     behvName (Behaviour _ _ (Interface name _) _ _ _ _ _:_) = name
     behvName [] = error "Internal error: behaviour groups cannot be empty"
 
-translateBehv :: CodeMap -> Layout -> BS.ByteString -> Behaviour -> EVM.Expr EVM.End
-translateBehv codemap layout bytecode (Behaviour _ cid _ preconds caseconds _ upds ret) =
-  EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr codemap layout cid upds bytecode)
+translateBehv :: CodeMap -> Layout -> BS.ByteString -> ContractMap -> Behaviour -> EVM.Expr EVM.End
+translateBehv codemap layout bytecode cmap (Behaviour _ cid _ preconds caseconds _ upds ret) =
+  EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr codemap layout cid bytecode cmap upds)
 
-rewritesToExpr :: CodeMap -> Layout -> Id -> [Rewrite] -> BS.ByteString -> ContractMap
-rewritesToExpr codemap layout cid rewrites bytecode = foldl (flip $ rewriteToExpr codemap layout cid initAddr) initmap rewrites
-  where
-    initcontract = EVM.C { EVM.code  = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode)
-                         , EVM.storage = EVM.AbstractStore initAddr
-                         , EVM.balance = EVM.Balance (EVM.SymAddr "entrypoint")
-                         , EVM.nonce = Just 0
-                         }
-    initmap = M.fromList [(initAddr, initcontract)]
+rewritesToExpr :: CodeMap -> Layout -> Id -> BS.ByteString -> ContractMap -> [Rewrite] -> ContractMap
+rewritesToExpr codemap layout cid bytecode cmap rewrites = foldl (rewriteToExpr codemap layout cid initAddr) cmap rewrites
 
-rewriteToExpr :: CodeMap -> Layout -> Id -> EVM.Expr EVM.EAddr -> Rewrite -> ContractMap -> ContractMap
-rewriteToExpr _ _ _ _ (Constant _) cmap = cmap
-rewriteToExpr codemap layout cid caddr (Rewrite upd) cmap = fst $ updateToExpr codemap layout cid caddr upd (cmap, [])
+rewriteToExpr :: CodeMap -> Layout -> Id -> EVM.Expr EVM.EAddr -> ContractMap -> Rewrite -> ContractMap
+rewriteToExpr _ _ _ _ cmap (Constant _) = cmap
+rewriteToExpr codemap layout cid caddr cmap (Rewrite upd) = fst $ updateToExpr codemap layout cid caddr upd (cmap, [])
 
 updatesToExpr :: CodeMap -> Layout -> Id -> EVM.Expr EVM.EAddr -> [StorageUpdate] -> (ContractMap, [EVM.Prop]) -> (ContractMap, [EVM.Prop])
 updatesToExpr codemap layout cid caddr upds initmap = foldl (flip $ updateToExpr codemap layout cid caddr) initmap upds
@@ -468,7 +461,7 @@ checkEquiv solvers opts l1 l2 =
     toEquivRes (Timeout b) = Timeout b
 
 
-checkConstructors :: SolverGroup -> VeriOpts -> ByteString -> ByteString -> Store -> Contract -> CodeMap -> IO ()
+checkConstructors :: SolverGroup -> VeriOpts -> ByteString -> ByteString -> Store -> Contract -> CodeMap -> IO ContractMap
 checkConstructors solvers opts initcode runtimecode store contract codemap = do
   let (actbehvs, calldata) = translateActConstr codemap store contract runtimecode
   solbehvs <- removeFails <$> getInitcodeBranches solvers initcode calldata
@@ -479,15 +472,20 @@ checkConstructors solvers opts initcode runtimecode store contract codemap = do
   checkResult =<< checkEquiv solvers opts solbehvs actbehvs
   putStrLn "\x1b[1mChecking if constructor input spaces are the same.\x1b[m"
   checkResult =<< checkInputSpaces solvers opts solbehvs actbehvs
+  pure $ getContractMap actbehvs
   where
     removeFails branches = filter isSuccess $ branches
 
+getContractMap :: [EVM.Expr EVM.End] -> ContractMap
+getContractMap [EVM.Success _ _ _ m] = m
+getContractMap _ = error "Internal error: unexpected shape of Act translation"
 
-checkBehaviours :: SolverGroup -> VeriOpts -> ByteString -> Store -> Contract -> CodeMap -> IO ()
-checkBehaviours solvers opts bytecode store (Contract _ behvs) codemap = do
-  let actbehvs = translateActBehvs codemap store behvs bytecode
+checkBehaviours :: SolverGroup -> VeriOpts -> ByteString -> Store -> Contract -> CodeMap -> ContractMap -> IO ()
+checkBehaviours solvers opts bytecode store (Contract _ behvs) codemap cmap = do
+  let (actstorage, hevmstorage) = createStorage cmap
+  let actbehvs = translateActBehvs codemap store behvs bytecode actstorage
   flip mapM_ actbehvs $ \(name,behvs',calldata) -> do
-    solbehvs <- removeFails <$> getRuntimeBranches solvers bytecode calldata
+    solbehvs <- removeFails <$> getRuntimeBranches solvers hevmstorage calldata
 
     putStrLn $ "\x1b[1mChecking behavior \x1b[4m" <> name <> "\x1b[m of Act\x1b[m"
     traceShowM "Solidity behaviors"
@@ -501,6 +499,39 @@ checkBehaviours solvers opts bytecode store (Contract _ behvs) codemap = do
     where
       removeFails branches = filter isSuccess $ branches
 
+
+createStorage :: ContractMap -> (ContractMap, [(EVM.Expr EVM.EAddr, EVM.Contract)])
+createStorage cmap =
+  let cmap' = M.mapWithKey makeContract cmap in
+  let contracts = fmap (\(addr, c) -> (addr, toContract c)) $ M.toList cmap' in
+  (cmap', contracts)
+
+  where
+    traverseStorage :: EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage
+    traverseStorage (EVM.SStore offset (EVM.WAddr addr) storage) =
+      EVM.SStore offset (EVM.WAddr addr) (traverseStorage storage)
+    traverseStorage (EVM.SStore _ _ storage) = traverseStorage storage
+    traverseStorage _ = error "Internal error: unexpected storage shape"
+
+    makeContract :: EVM.Expr EVM.EAddr -> EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract
+    makeContract addr (EVM.C code storage _ _) = EVM.C code (traverseStorage storage) (EVM.Balance addr) (Just 0)
+    makeContract _ (EVM.GVar _) = error "Internal error: contract cannot be gvar"
+
+    toContract :: EVM.Expr EVM.EContract -> EVM.Contract
+    toContract (EVM.C code storage balance nonce) = EVM.Contract
+      { EVM.code        = code
+      , EVM.storage     = storage
+      , EVM.origStorage = storage
+      , EVM.balance     = balance
+      , EVM.nonce       = nonce
+      , EVM.codehash    = EVM.hashcode code
+      , EVM.opIxMap     = EVM.mkOpIxMap code
+      , EVM.codeOps     = EVM.mkCodeOps code
+      , EVM.external    = False
+      }
+    toContract (EVM.GVar _) = error "Internal error: contract cannot be gvar"
+
+
 -- | Find the input space of an expr list
 inputSpace :: [EVM.Expr EVM.End] -> [EVM.Prop]
 inputSpace exprs = map aux exprs
@@ -540,7 +571,7 @@ checkAbi solver opts contract bytecode = do
   putStrLn "\x1b[1mChecking if the ABI of the contract matches the specification\x1b[m"
   let txdata = EVM.AbstractBuf "txdata"
   let selectorProps = assertSelector txdata <$> nubOrd (actSigs contract)
-  evmBehvs <- getRuntimeBranches solver bytecode (txdata, [])
+  evmBehvs <- getRuntimeBranches solver [] (txdata, []) -- XXX TODO what to put here???
   let queries =  fmap (assertProps abstRefineDefault) $ filter (/= []) $ fmap (checkBehv selectorProps) evmBehvs
 
   when opts.debug $ forM_ (zip [(1 :: Int)..] queries) $ \(idx, q) -> do
@@ -568,9 +599,9 @@ checkContracts solvers opts store codemap =
   mapM_ (\(_, (contract, initcode, bytecode)) -> do
             putStrLn $ "\x1b[1mChecking contract \x1b[4m" <> nameOfContract contract <> "\x1b[m"
             -- Constructor check
-            checkConstructors solvers opts initcode bytecode store contract codemap
+            cmap <- checkConstructors solvers opts initcode bytecode store contract codemap
             -- Behavours check
-            checkBehaviours solvers opts bytecode store contract codemap
+            checkBehaviours solvers opts bytecode store contract codemap cmap
             -- ABI exhaustiveness sheck
             checkAbi solvers opts contract bytecode
         ) (M.toList codemap)

src/HEVM_utils.hs

@@ -19,22 +19,24 @@ module HEVM_utils where
 import Prelude hiding (GT, LT)
 
 import Data.Containers.ListUtils (nubOrd)
+import Data.List
 import qualified Data.Text as T
 import qualified Data.Text.IO as TIO
 import qualified Data.ByteString as BS
 import Control.Monad
-import Control.Monad.ST (stToIO)
+import Control.Monad.ST (stToIO, ST)
 
 import Syntax.Annotated
 import Syntax.Untyped (makeIface)
 
-import qualified EVM.Types as EVM hiding (Contract(..))
+import qualified EVM.Types as EVM
 import EVM.Expr hiding (op2, inRange)
-import EVM.SymExec hiding (EquivResult, isPartial)
+import EVM.SymExec hiding (EquivResult, isPartial, abstractVM, loadSymVM)
 import EVM.Solvers
 import qualified EVM.Format as Format
 import qualified EVM.Fetch as Fetch
-
+import qualified EVM as EVM
+import EVM.FeeSchedule (feeSchedule)
 
 -- TODO move this to HEVM
 type Calldata = (EVM.Expr EVM.Buf, [EVM.Prop])
@@ -79,10 +81,9 @@ combineFragments' fragments start base = go (EVM.Lit start) fragments (base, [])
         s -> error $ "unsupported cd fragment: " <> show s
 
 -- | decompiles the given EVM bytecode into a list of Expr branches
-getRuntimeBranches :: SolverGroup -> BS.ByteString -> Calldata -> IO [EVM.Expr EVM.End]
-getRuntimeBranches solvers bs calldata = do
-      let bytecode = if BS.null bs then BS.pack [0] else bs
-      prestate <- stToIO $ abstractVM calldata bytecode Nothing False
+getRuntimeBranches :: SolverGroup -> [(EVM.Expr EVM.EAddr, EVM.Contract)] -> Calldata -> IO [EVM.Expr EVM.End]
+getRuntimeBranches solvers contracts calldata = do
+      prestate <- stToIO $ abstractVM contracts calldata
       expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased prestate runExpr
       let simpl = if True then (simplify expr) else expr
       let nodes = flattenExpr simpl
@@ -98,17 +99,73 @@ getRuntimeBranches solvers bs calldata = do
 
 -- | decompiles the given EVM initcode into a list of Expr branches
 getInitcodeBranches :: SolverGroup -> BS.ByteString -> Calldata -> IO [EVM.Expr EVM.End]
-getInitcodeBranches solvers initcode calldata = do  
-  initVM <- stToIO $ abstractVM calldata initcode Nothing True
+getInitcodeBranches solvers initcode calldata = do
+  initVM <- stToIO $ abstractInitVM initcode calldata
   expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased initVM runExpr
   let simpl = if True then (simplify expr) else expr
   -- traceM (T.unpack $ Format.formatExpr simpl)
-  let nodes = flattenExpr simpl  
-      
+  let nodes = flattenExpr simpl
+
   when (any isPartial nodes) $ do
     putStrLn ""
     putStrLn "WARNING: hevm was only able to partially explore the given contract due to the following issues:"
     putStrLn ""
     TIO.putStrLn . T.unlines . fmap (Format.indent 2 . ("- " <>)) . fmap Format.formatPartial . nubOrd $ (getPartials nodes)
 
   pure nodes
+
+
+abstractInitVM :: ByteString -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> ST s (EVM.VM s)
+abstractInitVM contractCode cd = do
+  let value = EVM.TxValue
+  let code = EVM.InitCode contractCode (fst cd)
+  loadSymVM (EVM.SymAddr "entrypoint", EVM.initialContract code) [] value cd True
+
+abstractVM :: [(EVM.Expr EVM.EAddr, EVM.Contract)] -> (EVM.Expr EVM.Buf, [EVM.Prop]) -> ST s (EVM.VM s)
+abstractVM contracts cd = do
+  let value = EVM.TxValue
+  let (c, cs) = findInitContract
+  loadSymVM c cs value cd False
+
+  where
+    findInitContract :: ((EVM.Expr 'EVM.EAddr, EVM.Contract), [(EVM.Expr 'EVM.EAddr, EVM.Contract)])
+    findInitContract =
+      case partition (\(a, _) -> a == EVM.SymAddr "entrypoint") contracts of
+        ([c], cs) -> (c, cs)
+        _ -> error "Internal error: address entrypoint expected exactly once"
+
+
+loadSymVM
+  :: (EVM.Expr EVM.EAddr, EVM.Contract)
+  -> [(EVM.Expr EVM.EAddr, EVM.Contract)]
+  -> EVM.Expr EVM.EWord
+  -> (EVM.Expr EVM.Buf, [EVM.Prop])
+  -> Bool
+  -> ST s (EVM.VM s)
+loadSymVM (entryaddr, entrycontract) othercontracts callvalue cd create =
+  (EVM.makeVm $ EVM.VMOpts
+    { contract = entrycontract
+    , otherContracts = othercontracts
+    , calldata = cd
+    , value = callvalue
+    , baseState = EVM.AbstractBase
+    , address = entryaddr
+    , caller = EVM.SymAddr "caller"
+    , origin = EVM.SymAddr "origin"
+    , coinbase = EVM.SymAddr "coinbase"
+    , number = 0
+    , timestamp = EVM.Lit 0
+    , blockGaslimit = 0
+    , gasprice = 0
+    , prevRandao = 42069
+    , gas = 0xffffffffffffffff
+    , gaslimit = 0xffffffffffffffff
+    , baseFee = 0
+    , priorityFee = 0
+    , maxCodeSize = 0xffffffff
+    , schedule = feeSchedule
+    , chainId = 1
+    , create = create
+    , txAccessList = mempty
+    , allowFFI = False
+    })