Constructor calls in HEVM equivalence #162
Conversation
zoep
changed the title
zoep
changed the title
| @@ -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 | |||
There was a problem hiding this comment.
This test should pass once we merge #388 into hevm.
| @@ -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) | |||
There was a problem hiding this comment.
Contact option is removed from CLI. Now all contracts in the spec are checked.
| getBytecode :: IO (BS.ByteString, BS.ByteString) | ||
| getBytecode = | ||
|
|
||
| createContractMap :: [Contract] -> IO (Map Id (Contract, BS.ByteString, BS.ByteString)) |
There was a problem hiding this comment.
We create a map from contact ids to their (Act spec, initcode, bytecode) triples. This makes it easy to look up the spec and the byte code of a contract when we encounter a call to its constructor. To check equivalence between the spec and the bytecodes, we traverse the map.
| 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) |
There was a problem hiding this comment.
I'm not sure how we can support bytecode input when we have multiple contracts.
|
|
||
| updatesToExpr :: Layout -> Id -> [StorageUpdate] -> ContractMap -> ContractMap | ||
| updatesToExpr layout cid upds initmap = foldl (flip $ updateToExpr layout cid) initmap upds | ||
| updatesToExpr :: CodeMap -> Layout -> Id -> EVM.Expr EVM.EAddr -> [StorageUpdate] -> (ContractMap, [EVM.Prop]) -> (ContractMap, [EVM.Prop]) |
There was a problem hiding this comment.
The return type propagates the preconditions of constructor calls upwards after substitution. As we discussed this is probably not needed. I will think about this a bit more and probably will be removing this from the return type.
|
Subsumed by #167 |
This PR adds support for multiple contracts in Act spec (WIP). More precisely:
--contractoption, since all contracts in the spec are now checked by defaultTODO: