Support for multiple contracts in equivalence check (#167)

* HEVM: start from concrete store for constructors

* wip

* wip

* wip

* Compiling

* most examples are working

* hevm: port to sym addresses

* fix initcode argumentsin hevm

* ast: add ABI type tag to vars

* hevm: remove warnings

* CLI: cleanup

* HEVM: cleanup

* test: fix compilation errors

* hevm: wip multiple contracts

* hevm: wip multiple contracts

* hevm: pass contract map around

* hevm: WIP create new contracts

* hevm: WIP create new contracts

* hevm: handle nonces for new contracts

* hevm: WIP multiple contracts

* WIP: substitutions

* HEVM: argument substitutions

* HEVM: propagate constraints

* HEVM: constructors with multiple contracts

* HEVM: fix contract address

* HEVM: remove warnings

* tests: add multiple contracts tests

* hevm: fix bug in fresh address

* HEVM: wip

* Makefile: remove multiple contracts

* Makefile: remove multiple contracts

* hevm: nits

* hevm: nits

* tests: fix test

* hevm: add blockhash

* hevm: fix compilation error

* CLI: remove contract option

* HEVM: remove condition propagation and add printing

* HEVM: add comment

* tests: nits

* hevm: cleanup

* makefile: remove --contract

* makefile: add back tests

* makefile: remove test

* tests: regenerate tests output

* hevm: remove unused constructor id

* HEVM: small cleanup

* HEVM: split utils files

* HEVM: split utils files

* flake: update hevm

* HEVM: WIP pass contract map to behaviours

* HEVM: pass contract map to behaviours

* HEVM: behavior equivalence

* HEVM: remove some traces

* tests: updates multi tests

* flake: use hevm commit

* hevm: fix storage access of other contracts

* hevm: port everything to state monad

* hevm: wip in compiling

* hevm: refector compiles

* hevm: fix bugs

* hevm: fix fresh counter bug

* test: multi test

* hevm: remove warnings

* tests: add failing tests

* hevm: cleanup

* makefile: add back test

* bump hevm

* Update Makefile

Co-authored-by: dxo  <[email protected]>

* Update src/HEVM.hs

Co-authored-by: dxo  <[email protected]>

* hevm: nits from PR

* wip updating hevm

* HEVM updates

* add file

* hevm: fix warnings

---------

Co-authored-by: dxo <[email protected]>

Makefile

@@ -104,11 +104,11 @@ tests/%.postcondition.fail:
 
 tests/hevm/pass/%.act.hevm.pass:
 	$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/pass/$*.sol))
-	./bin/act hevm --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol --contract $(CONTRACT)
+	./bin/act hevm --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol
 
 tests/hevm/fail/%.act.hevm.fail:
 	$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/fail/$*.sol))
-	./bin/act hevm --spec tests/hevm/fail/$*.act --sol tests/hevm/fail/$*.sol --contract $(CONTRACT) && exit 1 || echo 0
+	./bin/act hevm --spec tests/hevm/fail/$*.act --sol tests/hevm/fail/$*.sol && exit 1 || echo 0
 
 test-ci: test-parse test-type test-invariant test-postcondition test-coq test-hevm
 test: test-ci test-cabal

act.cabal

@@ -64,6 +64,7 @@ library
     Act.Enrich
     Act.Dev
     Act.HEVM
+    Act.HEVM_utils
     Act.Consistency
 
 executable act

src/Act/CLI.hs

@@ -19,6 +19,7 @@ import System.IO (hPutStrLn, stderr)
 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
@@ -43,12 +44,14 @@ import Act.SMT as SMT
 import Act.Type
 import Act.Coq hiding (indent)
 import Act.HEVM
+import Act.HEVM_utils
 import Act.Consistency
 import Act.Print
 
 import EVM.SymExec
 import qualified EVM.Solvers as Solvers
 import EVM.Solidity
+import EVM.Effects
 
 --command line options
 data Command w
@@ -78,7 +81,6 @@ data Command w
                     , sol        :: w ::: Maybe String         <?> "Path to .sol"
                     , code       :: w ::: Maybe ByteString     <?> "Runtime code"
                     , initcode   :: w ::: Maybe ByteString     <?> "Initial code"
-                    , contract   :: w ::: String               <?> "Contract name"
                     , solver     :: w ::: Maybe Text           <?> "SMT solver: cvc5 (default) or z3"
                     , smttimeout :: w ::: Maybe Integer        <?> "Timeout given to SMT solver in milliseconds (default: 20000)"
                     , debug      :: w ::: Bool                 <?> "Print verbose SMT output (default: False)"
@@ -110,9 +112,9 @@ main = do
       Coq f solver' smttimeout' debug' -> do
         solver'' <- parseSolver solver'
         coq' f solver'' smttimeout' debug'
-      HEVM spec' sol' code' initcode' contract' solver' smttimeout' debug' -> do
+      HEVM spec' sol' code' initcode' solver' smttimeout' debug' -> do
         solver'' <- parseSolver solver'
-        hevm spec' (Text.pack contract') sol' code' initcode' solver'' smttimeout' debug'
+        hevm spec' sol' code' initcode' solver'' smttimeout' debug'
 
 
 ---------------------------------
@@ -208,29 +210,33 @@ coq' f solver' smttimeout' debug' = do
     TIO.putStr $ coq claims
 
 
-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
-  let opts = if debug' then debugVeriOpts else defaultVeriOpts
-  (initcode'', bytecode) <- getBytecode
+hevm :: FilePath -> Maybe FilePath -> Maybe ByteString -> Maybe ByteString -> Solvers.Solver -> Maybe Integer -> Bool -> IO ()
+hevm actspec sol' code' initcode' solver' timeout debug' = do
   specContents <- readFile actspec
-  proceed specContents (enrich <$> compile specContents) $ \act -> do
-    checkCases act solver' timeout debug'
-    Solvers.withSolvers solver' 1 (naturalFromInteger <$> timeout) $ \solvers -> do
-      -- Constructor check
-      checkConstructors solvers opts initcode'' bytecode act
-      -- Behavours check
-      checkBehaviours solvers opts bytecode act
-      -- ABI exhaustiveness sheck
-      checkAbi solvers opts act bytecode
+  proceed specContents (enrich <$> compile specContents) $ \ (Act store contracts) -> do
+    cmap <- createContractMap contracts
+    let opts = defaultVeriOpts -- TODO maybe remove
 
+    let config = if debug' then defaultActConfig else debugActConfig
+    runEnv (Env config) $ Solvers.withSolvers solver' 1 (naturalFromInteger <$> timeout) $ \solvers ->
+      checkContracts solvers opts store cmap
   where
-    getBytecode :: IO (BS.ByteString, BS.ByteString)
-    getBytecode =
+
+    createContractMap :: [Contract] -> IO (Map Id (Contract, BS.ByteString, BS.ByteString))
+    createContractMap contracts = do
+      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" <> line) >> exitFailure
         (Nothing, _, Nothing) -> render (text "No initial code is given" <> line) >> exitFailure
         (Just _, Just _, _) -> render (text "Both Solidity file and runtime code are given. Please specify only one." <> line) >> exitFailure