Skip to content

Commit

Permalink
Implement check that all symbolic addesses are unique, until we do in…
Browse files Browse the repository at this point in the history
…ternal renaming
  • Loading branch information
zoep committed Nov 4, 2024
1 parent f464723 commit 1141ca5
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 3 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ hevm_buggy=tests/hevm/pass/transfer/transfer.act
hevm_pass=$(filter-out $(hevm_buggy), $(wildcard tests/hevm/pass/*/*.act))
# supposed to fail
hevm_fail=$(wildcard tests/hevm/fail/*/*.act)
# slow tests
# slow passing tests
hevm_slow=tests/hevm/pass/amm/amm.act tests/hevm/pass/amm-2/amm-2.act
# supposed to pass, run fust
hevm_fast=$(filter-out $(hevm_slow), $(hevm_pass))
Expand Down
2 changes: 1 addition & 1 deletion src/Act/Decompile.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@

{-|
Module : Decompile
Description : Decompile EVM bytecode into Act378
Description : Decompile EVM bytecode into Act
This module decompiles EVM bytecode into an Act spec. It operates as follows
Expand Down
12 changes: 11 additions & 1 deletion src/Act/HEVM.hs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ module Act.HEVM where
import Prelude hiding (GT, LT)

import qualified Data.Map as M
import qualified Data.Set as S
import Data.List
import Data.Containers.ListUtils (nubOrd)
import qualified Data.Text as T
Expand Down Expand Up @@ -658,8 +659,9 @@ getInitContractState solvers iface pointers preconds cmap = do
(cmaps, checks) <- unzip <$> mapM getContractState (fmap nub casts')

let finalmap = M.unions (cmap:cmaps)

check <- checkAliasing finalmap cmaps
pure (finalmap, check <* sequenceA_ checks)
pure (finalmap, check <* sequenceA_ checks <* checkUniqueAddr (cmap:cmaps))

where

Expand Down Expand Up @@ -710,7 +712,15 @@ getInitContractState solvers iface pointers preconds cmap = do

msg = "\x1b[1mThe following addresses cannot be proved distinct:\x1b[m"

-- currently we check that all symbolic addresses are globaly unique, and fail otherwise
-- (this is required for aliasing check to be sound when merging graphs
-- In the future, we should implement an internal renaming of variables to ensure global
-- uniqueness of symbolic a)ddresses.

checkUniqueAddr :: [ContractMap] -> Error String ()
checkUniqueAddr cmaps =
let pairs = comb cmaps in
assert (nowhere, "Names of symbolic adresses must be unique") (foldl (\b (c1, c2) -> S.disjoint (M.keysSet c1) (M.keysSet c2) && b) True pairs)

checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Contract -> ActT m (Error String ContractMap)
checkConstructors solvers initcode runtimecode (Contract ctor@(Constructor _ iface pointers preconds _ _ _) _) = do
Expand Down

0 comments on commit 1141ca5

Please sign in to comment.