Support for multiple contracts in equivalence check

Makefile

@@ -53,7 +53,7 @@ hevm_fail=$(wildcard tests/hevm/fail/*/*.act)
 failing_typing=tests/frontend/pass/array/array.act tests/frontend/pass/dss/vat.act tests/frontend/pass/creation/createMultiple.act tests/frontend/pass/staticstore/staticstore.act
 
 
-coq-examples = tests/coq/transitions tests/coq/safemath tests/coq/exponent tests/coq/token tests/coq/ERC20 tests/coq/multi
+coq-examples = tests/coq/transitions tests/coq/safemath tests/coq/exponent tests/coq/token tests/coq/ERC20 tests/coq/multi tests/coq/multi
 
 .PHONY: test-coq $(coq-examples)
 test-coq: compiler $(coq-examples)
@@ -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

flake.nix

@@ -5,7 +5,7 @@
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:nixos/nixpkgs";
     hevmUpstream = {
-      url = "github:ethereum/hevm";
+      url = "github:ethereum/hevm/f96f0993b73c2937db48bb38e29634d922c40af1";
       inputs.nixpkgs.follows = "nixpkgs";
     };
   };

src/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
@@ -77,7 +78,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)"
@@ -109,9 +109,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'
 
 
 ---------------------------------
@@ -207,29 +207,32 @@ 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 = if debug' then debugVeriOpts else defaultVeriOpts
 
+    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