hevm: wip multiple contracts

src/CLI.hs

@@ -19,6 +19,7 @@ import System.IO (hPutStrLn, stderr, stdout)
 import Data.Text (unpack)
 import Data.List
 import qualified Data.Map as Map
+import Data.Map (Map)
 import Data.Maybe
 import qualified Data.Text as Text
 import qualified Data.Text.IO as TIO
@@ -190,28 +191,33 @@ coq' f = do
 
 
 hevm :: FilePath -> Text -> Maybe FilePath -> Maybe ByteString -> Maybe ByteString -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
-hevm actspec cid sol' code' initcode' solver' timeout debug' = do
+hevm actspec _ sol' code' initcode' solver' timeout debug' = do
   specContents <- readFile actspec
-  (initcode'', bytecode) <- getBytecode
   let act = validation (\_ -> error "Too bad") id (enrich <$> compile specContents)
-  let opts = if debug' then debugVeriOpts else defaultVeriOpts
+  cmap <- createContractMap act
 
-  Solvers.withSolvers solver' 1 (naturalFromInteger <$> timeout) $ \solvers -> do
-    -- Constructor check
-    checkConstructors solvers opts initcode'' bytecode act (unpack cid)
-    -- Behavours check
-    checkBehaviours solvers opts bytecode act (unpack cid)
-    -- ABI exhaustiveness sheck
-    checkAbi solvers opts act bytecode
+  let opts = if debug' then debugVeriOpts else defaultVeriOpts
 
+  Solvers.withSolvers solver' 1 (naturalFromInteger <$> timeout) $ \solvers ->
+    checkContracts solvers opts cmap
   where
-    getBytecode :: IO (BS.ByteString, BS.ByteString)
-    getBytecode =
+
+    createContractMap :: Act -> IO (Map Id (Contract, BS.ByteString, BS.ByteString))
+    createContractMap act = do
+      let (Act _ contracts) = act
+      foldM (\cmap spec'@(Contract cnstr _) -> do
+                let cid =  _cname cnstr
+                (initcode'', runtimecode') <- getBytecode cid -- TODO do not reread the file each time
+                pure $ Map.insert cid (spec', initcode'', runtimecode') cmap
+            ) mempty contracts
+
+    getBytecode :: Id -> IO (BS.ByteString, BS.ByteString)
+    getBytecode cid =
       case (sol', code', initcode') of
         (Just f, Nothing, Nothing) -> do
           solContents  <- TIO.readFile f
-          bytecodes cid solContents
-        (Nothing, Just c, Just i) -> pure (i, c)
+          bytecodes (Text.pack cid) solContents
+        (Nothing, Just _, Just _) -> render (text "Only Solidity file supported") >> exitFailure -- pure (i, c)
         (Nothing, Nothing, _) -> render (text "No runtime code is given") >> exitFailure
         (Nothing, _, Nothing) -> render (text "No initial code is given") >> exitFailure
         (Just _, Just _, _) -> render (text "Both Solidity file and runtime code are given. Please specify only one.") >> exitFailure

src/HEVM.hs

@@ -44,6 +44,7 @@ import EVM.Solvers
 import qualified EVM.Format as Format
 import qualified EVM.Fetch as Fetch
 
+import Debug.Trace
 
 type family ExprType a where
   ExprType 'AInteger  = EVM.EWord
@@ -115,16 +116,15 @@ combineFragments' fragments start base = go (EVM.Lit start) fragments (base, [])
 translateActBehvs :: Act -> BS.ByteString -> Id -> [(Id, [EVM.Expr EVM.End], Calldata)]
 translateActBehvs (Act store contracts) bytecode cid =
   let slots = slotMap store in
-  concatMap (\(Contract _ behvs) -> translateBehvs slots bytecode behvs) contracts
-
+  concatMap (\(Contract _ behvs) -> translateBehvs slots bytecode behvs) contracts'
   where
     contracts' = filter (\(Contract constructor _) -> _cname constructor == cid) contracts
 
 translateActConstr :: Act -> BS.ByteString -> Id -> (Id, [EVM.Expr EVM.End], Calldata)
 translateActConstr (Act store contracts) bytecode cid = translateConstructor (slotMap store) ctor bytecode
   where
     ctor = case find (\(Contract constructor _) -> _cname constructor == cid) contracts of
-             Just (Contract ctor _)  -> ctor
+             Just (Contract c _)  -> c
              Nothing -> error $ "Contract " <> cid <> " not found in Act spec"
 
 
@@ -179,12 +179,12 @@ updatesToExpr :: Layout -> Id -> [StorageUpdate] -> ContractMap -> ContractMap
 updatesToExpr layout cid upds initmap = foldl (flip $ updateToExpr layout cid) initmap upds
 
 updateToExpr :: Layout -> Id -> StorageUpdate -> ContractMap -> ContractMap
-updateToExpr layout cid (Update typ i@(Item _ _ ref) e) cmap =
+updateToExpr layout cid upd@(Update typ i@(Item _ _ ref) e) cmap =
   case typ of
     SInteger -> M.insert addr (updateStorage (EVM.SStore offset e') contract) cmap
     SBoolean -> M.insert addr (updateStorage (EVM.SStore offset e') contract) cmap
     SByteStr -> error "Bytestrings not supported"
-    SContract -> error "Contracts not supported"
+    SContract -> error $ "Contracts not supported. Expression: " <> show upd
   where
     (addr, slot) = getSlot layout cid (idFromItem i)
     offset = offsetFromRef layout slot ref
@@ -406,7 +406,9 @@ checkConstructors solvers opts initcode runtimecode act ctor = do
   initVM <- stToIO $ abstractVM calldata initcode Nothing True
   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 solbehvs = removeFails $ flattenExpr simpl
+  mapM_ (traceM . T.unpack . Format.formatExpr) actbehvs
   putStrLn "\x1b[1mChecking if constructor results are equivalent.\x1b[m"
   checkResult =<< checkEquiv solvers opts solbehvs actbehvs
   putStrLn "\x1b[1mChecking if constructor input spaces are the same.\x1b[m"
@@ -464,8 +466,8 @@ checkInputSpaces solvers opts l1 l2 = do
 
 -- | Checks whether all successful EVM behaviors are withing the
 -- interfaces specified by Act
-checkAbi :: SolverGroup -> VeriOpts -> Act -> BS.ByteString -> IO ()
-checkAbi solver opts act bytecode = do
+checkAbi :: SolverGroup -> VeriOpts -> Act -> BS.ByteString -> Id -> IO ()
+checkAbi solver opts act bytecode cid = 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 act)
@@ -481,9 +483,10 @@ checkAbi solver opts act bytecode = do
 
   where
     actSig (Behaviour _ _ iface _ _ _ _ _) = T.pack $ makeIface iface
-    actSigs (Act _ [(Contract _ behvs)]) = actSig <$> behvs
-    -- TODO multiple contracts
-    actSigs (Act _ _) = error "TODO multiple contracts"
+    actSigs (Act _ contracts) =
+      case find (\(Contract constructor _) -> _cname constructor == cid) contracts of
+        Just (Contract _ behvs)  -> actSig <$> behvs
+        Nothing -> error $ "Internal error: Contract " <> cid <> " not found in Act spec"
 
     checkBehv :: [EVM.Prop] -> EVM.Expr EVM.End -> [EVM.Prop]
     checkBehv assertions (EVM.Success cnstr _ _ _) = assertions <> cnstr
@@ -494,6 +497,18 @@ checkAbi solver opts act bytecode = do
 
     msg = "\x1b[1mThe following function selector results in behaviors not covered by the Act spec:\x1b[m"
 
+checkContracts :: SolverGroup -> VeriOpts -> M.Map Id (Contract, BS.ByteString, BS.ByteString) -> IO ()
+checkContracts solvers opts cmap = error "TODO"
+
+    -- -- Constructor check
+    -- checkConstructors solvers opts initcode bytecode act (unpack cid)
+    -- -- Behavours check
+    -- checkBehaviours solvers opts bytecode act (unpack cid)
+    -- -- ABI exhaustiveness sheck
+    -- checkAbi solvers opts act bytecode (unpack cid)
+
+
+
 -- | decompiles the given EVM bytecode into a list of Expr branches
 getBranches :: SolverGroup -> BS.ByteString -> Calldata -> IO [EVM.Expr EVM.End]
 getBranches solvers bs calldata = do