From 47404a27208601f867575a5ab1038900764eb46b Mon Sep 17 00:00:00 2001 From: Zoe Paraskevopoulou Date: Mon, 25 Sep 2023 15:39:09 +0300 Subject: [PATCH] Port to symbolic addresses (#160) * 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 * flake: use hevm main * HEVM: wip updating hevm * hevm: fix nonce * hevm: small nits --- flake.lock | 24 +++++- flake.nix | 2 +- src/Coq.hs | 8 +- src/Enrich.hs | 2 +- src/HEVM.hs | 146 +++++++++++++++++++++---------------- src/K.hs | 2 +- src/Print.hs | 7 +- src/SMT.hs | 2 +- src/Syntax/TimeAgnostic.hs | 12 +-- src/Type.hs | 10 +-- src/test/Test.hs | 6 +- 11 files changed, 127 insertions(+), 94 deletions(-) diff --git a/flake.lock b/flake.lock index 62e4a9f6..41838511 100644 --- a/flake.lock +++ b/flake.lock @@ -1,5 +1,21 @@ { "nodes": { + "cabal-head": { + "flake": false, + "locked": { + "lastModified": 1691811891, + "narHash": "sha256-e/dXo93pNSva1aKDpuO392Nig1M51Us96Qm0Peb/3bQ=", + "owner": "haskell", + "repo": "cabal", + "rev": "e77f13945d66fb829525c7249d97a6ad29fc701b", + "type": "github" + }, + "original": { + "owner": "haskell", + "repo": "cabal", + "type": "github" + } + }, "ethereum-tests": { "flake": false, "locked": { @@ -103,6 +119,7 @@ }, "hevmUpstream": { "inputs": { + "cabal-head": "cabal-head", "ethereum-tests": "ethereum-tests", "flake-compat": "flake-compat", "flake-utils": "flake-utils_2", @@ -113,17 +130,16 @@ "solidity": "solidity" }, "locked": { - "lastModified": 1689591967, - "narHash": "sha256-FJuWEGyWMNk05zQ7WtHNK53gPbERBPQwmVFdWLxQQCU=", + "lastModified": 1695059034, + "narHash": "sha256-LqQBLQ5Pl2xDUKqiiRF1iGRWFxTlgrf4SemusvxsnBM=", "owner": "ethereum", "repo": "hevm", - "rev": "308cf16788c29a3e98542d87125d3ffb237615e1", + "rev": "fb7c953cc108f7b2350d1e8ab7212dcf38f309f2", "type": "github" }, "original": { "owner": "ethereum", "repo": "hevm", - "rev": "308cf16788c29a3e98542d87125d3ffb237615e1", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 2be86ce3..b2964a6b 100644 --- a/flake.nix +++ b/flake.nix @@ -5,7 +5,7 @@ flake-utils.url = "github:numtide/flake-utils"; nixpkgs.url = "github:nixos/nixpkgs"; hevmUpstream = { - url = "github:ethereum/hevm/308cf16788c29a3e98542d87125d3ffb237615e1"; + url = "github:ethereum/hevm"; inputs.nixpkgs.follows = "nixpkgs"; }; }; diff --git a/src/Coq.hs b/src/Coq.hs index b5d966d4..95520a4e 100644 --- a/src/Coq.hs +++ b/src/Coq.hs @@ -281,7 +281,7 @@ coqexp :: Exp a -> T.Text -- booleans coqexp (LitBool _ True) = "true" coqexp (LitBool _ False) = "false" -coqexp (Var _ SBoolean name) = T.pack name +coqexp (Var _ SBoolean _ name) = T.pack name coqexp (And _ e1 e2) = parens $ "andb " <> coqexp e1 <> " " <> coqexp e2 coqexp (Or _ e1 e2) = parens $ "orb" <> coqexp e1 <> " " <> coqexp e2 coqexp (Impl _ e1 e2) = parens $ "implb" <> coqexp e1 <> " " <> coqexp e2 @@ -295,7 +295,7 @@ coqexp (GEQ _ e1 e2) = parens $ coqexp e2 <> " <=? " <> coqexp e1 -- integers coqexp (LitInt _ i) = T.pack $ show i -coqexp (Var _ SInteger name) = T.pack name +coqexp (Var _ SInteger _ name) = T.pack name coqexp (Add _ e1 e2) = parens $ coqexp e1 <> " + " <> coqexp e2 coqexp (Sub _ e1 e2) = parens $ coqexp e1 <> " - " <> coqexp e2 coqexp (Mul _ e1 e2) = parens $ coqexp e1 <> " * " <> coqexp e2 @@ -323,12 +323,12 @@ coqexp (ITE _ b e1 e2) = parens $ "if " -- as the corresponding Haskell constructor coqexp (IntEnv _ envVal) = parens $ T.pack (show envVal) <> " " <> envVar -- Contracts -coqexp (Var _ SContract name) = T.pack name +coqexp (Var _ SContract _ name) = T.pack name coqexp (Create _ cid args) = parens $ T.pack cid <> "." <> T.pack cid <> " " <> envVar <> " " <> coqargs args -- unsupported coqexp Cat {} = error "bytestrings not supported" coqexp Slice {} = error "bytestrings not supported" -coqexp (Var _ SByteStr _) = error "bytestrings not supported" +coqexp (Var _ SByteStr _ _) = error "bytestrings not supported" coqexp ByStr {} = error "bytestrings not supported" coqexp ByLit {} = error "bytestrings not supported" coqexp ByEnv {} = error "bytestrings not supported" diff --git a/src/Enrich.hs b/src/Enrich.hs index 48b6b4fa..09b9867a 100644 --- a/src/Enrich.hs +++ b/src/Enrich.hs @@ -88,5 +88,5 @@ mkStorageBounds refs = catMaybes $ mkBound <$> refs mkCallDataBounds :: [Decl] -> [Exp ABoolean] mkCallDataBounds = concatMap $ \(Decl typ name) -> case fromAbiType typ of - AInteger -> [bound typ (_Var name)] + AInteger -> [bound typ (_Var typ name)] _ -> [] diff --git a/src/HEVM.hs b/src/HEVM.hs index 09ea62f3..11ec795d 100644 --- a/src/HEVM.hs +++ b/src/HEVM.hs @@ -29,15 +29,15 @@ import Control.Monad import Data.DoubleWord import Data.Maybe import System.Exit ( exitFailure ) +import Control.Monad.ST (stToIO) import Syntax.Annotated import Syntax.Untyped (makeIface) import Syntax -import qualified EVM.Types as EVM -import EVM.Concrete (createAddress) +import qualified EVM.Types as EVM hiding (Contract(..)) import EVM.Expr hiding (op2, inRange) -import EVM.SymExec hiding (EquivResult) +import EVM.SymExec hiding (EquivResult, isPartial) import qualified EVM.SymExec as SymExec (EquivResult) import EVM.SMT (SMTCex(..), assertProps, formatSMT2) import EVM.Solvers @@ -50,20 +50,27 @@ type family ExprType a where ExprType 'AByteStr = EVM.Buf ExprType 'AContract = EVM.EWord -- address? -type Layout = M.Map Id (M.Map Id (EVM.Addr, Integer)) +type Layout = M.Map Id (M.Map Id (EVM.Expr EVM.EAddr, Integer)) -- TODO move this to HEVM type Calldata = (EVM.Expr EVM.Buf, [EVM.Prop]) +type ContractMap = M.Map (EVM.Expr EVM.EAddr) (EVM.Expr EVM.EContract) + type EquivResult = ProofResult () (T.Text, SMTCex) () +abstRefineDefault :: EVM.AbstRefineConfig +abstRefineDefault = EVM.AbstRefineConfig False False + ethrunAddress :: EVM.Addr ethrunAddress = EVM.Addr 0x00a329c0648769a73afac7f9381e08fb43dbea72 +initAddr :: EVM.Expr EVM.EAddr +initAddr = EVM.SymAddr "entrypoint" + slotMap :: Store -> Layout slotMap store = - let addr = createAddress ethrunAddress 1 in -- for now all contracts have the same address - M.map (M.map (\(_, slot) -> (addr, slot))) store + M.map (M.map (\(_, slot) -> (initAddr, slot))) store -- Create a calldata that matches the interface of a certain behaviour -- or constructor. Use an abstract txdata buffer as the base. @@ -71,7 +78,7 @@ makeCalldata :: Interface -> Calldata makeCalldata iface@(Interface _ decls) = let mkArg :: Decl -> CalldataFragment - mkArg (Decl typ x) = symAbiArg (T.pack x) typ + mkArg (Decl typ x) = symAbiArg (T.pack x) typ makeSig = T.pack $ makeIface iface calldatas = fmap mkArg decls (cdBuf, _) = combineFragments calldatas (EVM.ConcreteBuf "") @@ -85,7 +92,7 @@ makeCtrCalldata :: Interface -> Calldata makeCtrCalldata (Interface _ decls) = let mkArg :: Decl -> CalldataFragment - mkArg (Decl typ x) = symAbiArg (T.pack x) typ + mkArg (Decl typ x) = symAbiArg (T.pack x) typ calldatas = fmap mkArg decls -- We need to use a concrete buf as a base here because hevm bails when trying to execute with an abstract buf -- This is because hevm ends up trying to execute a codecopy with a symbolic size, which is unsupported atm @@ -107,10 +114,10 @@ combineFragments' fragments start base = go (EVM.Lit start) fragments (base, []) -- * Act translation -translateActBehvs :: Act -> [(Id, [EVM.Expr EVM.End], Calldata)] -translateActBehvs (Act store contracts) = +translateActBehvs :: Act -> BS.ByteString -> [(Id, [EVM.Expr EVM.End], Calldata)] +translateActBehvs (Act store contracts) bytecode = let slots = slotMap store in - concatMap (\(Contract _ behvs) -> translateBehvs slots behvs) contracts + concatMap (\(Contract _ behvs) -> translateBehvs slots bytecode behvs) contracts translateActConstr :: Act -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata) translateActConstr (Act store [Contract ctor _]) bytecode = translateConstructor (slotMap store) ctor bytecode @@ -118,14 +125,21 @@ translateActConstr (Act _ _) _ = error "TODO multiple contracts" translateConstructor :: Layout -> Constructor -> BS.ByteString -> (Id, [EVM.Expr EVM.End], Calldata) translateConstructor layout (Constructor cid iface preconds _ _ upds _) bytecode = - (cid, [EVM.Success (snd calldata <> (fmap (toProp layout) $ preconds)) mempty (EVM.ConcreteBuf bytecode) (updatesToExpr layout cid upds (EVM.ConcreteStore mempty))], - calldata) - where calldata = makeCtrCalldata iface - -translateBehvs :: Layout -> [Behaviour] -> [(Id, [EVM.Expr EVM.End], Calldata)] -translateBehvs layout behvs = + (cid, [EVM.Success (snd calldata <> (fmap (toProp layout) $ preconds)) mempty (EVM.ConcreteBuf bytecode) (updatesToExpr layout cid upds initmap)], + calldata) + where + calldata = makeCtrCalldata iface + initcontract = EVM.C { EVM.code = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode) + , EVM.storage = EVM.ConcreteStore mempty + , EVM.balance = EVM.Lit 0 + , EVM.nonce = Just 1 + } + initmap = M.fromList [(initAddr, initcontract)] + +translateBehvs :: Layout -> BS.ByteString -> [Behaviour] -> [(Id, [EVM.Expr EVM.End], Calldata)] +translateBehvs layout bytecode behvs = let groups = (groupBy sameIface behvs) :: [[Behaviour]] in - fmap (\behvs' -> (behvName behvs', fmap (translateBehv layout) behvs', behvCalldata behvs')) groups + fmap (\behvs' -> (behvName behvs', fmap (translateBehv layout bytecode) behvs', behvCalldata behvs')) groups where behvCalldata (Behaviour _ _ iface _ _ _ _ _:_) = makeCalldata iface @@ -138,31 +152,43 @@ translateBehvs layout behvs = behvName (Behaviour _ _ (Interface name _) _ _ _ _ _:_) = name behvName [] = error "Internal error: behaviour groups cannot be empty" -translateBehv :: Layout -> Behaviour -> EVM.Expr EVM.End -translateBehv layout (Behaviour _ cid _ preconds caseconds _ upds ret) = - EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr layout cid upds) - -rewritesToExpr :: Layout -> Id -> [Rewrite] -> EVM.Expr EVM.Storage -rewritesToExpr layout cid rewrites = foldl (flip $ rewriteToExpr layout cid) EVM.AbstractStore rewrites - -rewriteToExpr :: Layout -> Id -> Rewrite -> EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage -rewriteToExpr _ _ (Constant _) state = state -rewriteToExpr layout cid (Rewrite upd) state = updateToExpr layout cid upd state - -updatesToExpr :: Layout -> Id -> [StorageUpdate] -> EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage -updatesToExpr layout cid upds initstore = foldl (flip $ updateToExpr layout cid) initstore upds +translateBehv :: Layout -> BS.ByteString -> Behaviour -> EVM.Expr EVM.End +translateBehv layout bytecode (Behaviour _ cid _ preconds caseconds _ upds ret) = + EVM.Success (fmap (toProp layout) $ preconds <> caseconds) mempty (returnsToExpr layout ret) (rewritesToExpr layout cid upds bytecode) -updateToExpr :: Layout -> Id -> StorageUpdate -> EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage -updateToExpr layout cid (Update typ i@(Item _ _ ref) e) state = +rewritesToExpr :: Layout -> Id -> [Rewrite] -> BS.ByteString -> ContractMap +rewritesToExpr layout cid rewrites bytecode = foldl (flip $ rewriteToExpr layout cid) initmap rewrites + where + initcontract = EVM.C { EVM.code = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode) + , EVM.storage = EVM.AbstractStore initAddr + , EVM.balance = EVM.Balance (EVM.SymAddr "entrypoint") + , EVM.nonce = Just 0 + } + initmap = M.fromList [(initAddr, initcontract)] + +rewriteToExpr :: Layout -> Id -> Rewrite -> ContractMap -> ContractMap +rewriteToExpr _ _ (Constant _) cmap = cmap +rewriteToExpr layout cid (Rewrite upd) cmap = updateToExpr layout cid upd cmap + +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 = case typ of - SInteger -> EVM.SStore (EVM.Lit $ fromIntegral addr) offset e' state - SBoolean -> EVM.SStore (EVM.Lit $ fromIntegral addr) offset e' state + 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" where (addr, slot) = getSlot layout cid (idFromItem i) offset = offsetFromRef layout slot ref e' = toExpr layout e + contract = fromMaybe (error "Internal error: contract not found") $ M.lookup addr cmap + + updateStorage :: (EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage) -> EVM.Expr EVM.EContract -> EVM.Expr EVM.EContract + updateStorage upd c'@(EVM.C _ _ _ _) = c' { EVM.storage = upd c'.storage } + updateStorage _ (EVM.GVar _) = error "Internal error: contract cannot be a global variable" returnsToExpr :: Layout -> Maybe TypedExp -> EVM.Expr EVM.Buf returnsToExpr _ Nothing = EVM.ConcreteBuf "" @@ -193,7 +219,7 @@ expToBuf layout styp e = SByteStr -> toExpr layout e SContract -> error "Internal error: expecting primitive type" -getSlot :: Layout -> Id -> Id -> (EVM.Addr, Integer) +getSlot :: Layout -> Id -> Id -> (EVM.Expr EVM.EAddr, Integer) getSlot layout cid name = case M.lookup cid layout of Just m -> case M.lookup name m of @@ -201,7 +227,7 @@ getSlot layout cid name = Nothing -> error $ "Internal error: invalid variable name: " <> show name Nothing -> error "Internal error: invalid contract name" -refOffset :: Layout -> StorageRef -> (EVM.Addr, EVM.Expr EVM.EWord) +refOffset :: Layout -> StorageRef -> (EVM.Expr EVM.EAddr, EVM.Expr EVM.EWord) refOffset layout (SVar _ cid name) = let (addr, slot) = getSlot layout cid name in (addr, EVM.Lit $ fromIntegral slot) @@ -213,11 +239,11 @@ refOffset layout (SMapping _ ref ixs) = refOffset _ _ = error "TODO" ethEnvToWord :: EthEnv -> EVM.Expr EVM.EWord -ethEnvToWord Callvalue = EVM.CallValue 0 -ethEnvToWord Caller = EVM.Caller 0 +ethEnvToWord Callvalue = EVM.TxValue +ethEnvToWord Caller = EVM.WAddr $ EVM.SymAddr "caller" ethEnvToWord Origin = EVM.Origin ethEnvToWord Blocknumber = EVM.BlockNumber -ethEnvToWord Blockhash = error "TODO" -- EVM.BlockHash ?? +ethEnvToWord Blockhash = error "TODO" -- TODO argument of EVM.BlockHash ?? ethEnvToWord Chainid = EVM.ChainId ethEnvToWord Gaslimit = EVM.GasLimit ethEnvToWord Coinbase = EVM.Coinbase @@ -249,7 +275,7 @@ toProp layout = \case (NEq _ SBoolean e1 e2) -> EVM.PNeg $ op2 EVM.PEq e1 e2 (NEq _ _ _ _) -> error "unsupported" (ITE _ _ _ _) -> error "Internal error: expecting flat expression" - (Var _ _ _) -> error "TODO" -- (EVM.Var (T.pack x)) -- vars can only be words? TODO other types + (Var _ _ _ _) -> error "TODO" (TEntry _ _ _) -> error "TODO" -- EVM.SLoad addr idx (InRange _ t e) -> toProp layout (inRange t e) where @@ -310,17 +336,22 @@ toExpr layout = \case (ITE _ _ _ _) -> error "Internal error: expecting flat expression" - (Var _ SInteger x) -> (EVM.Var (T.pack x)) -- vars can only be words? TODO other types + (Var _ SInteger typ x) -> -- TODO other types + fromCalldataFramgment $ symAbiArg (T.pack x) typ (TEntry _ _ (Item SInteger _ ref)) -> let (addr, slot) = refOffset layout ref in - EVM.SLoad (litAddr addr) slot EVM.AbstractStore + EVM.SLoad slot (EVM.AbstractStore addr) e -> error $ "TODO: " <> show e where op2 :: forall b c. (EVM.Expr (ExprType c) -> EVM.Expr (ExprType c) -> b) -> Exp c -> Exp c -> b op2 op e1 e2 = op (toExpr layout e1) (toExpr layout e2) + fromCalldataFramgment :: CalldataFragment -> EVM.Expr EVM.EWord + fromCalldataFramgment (St _ word) = word + fromCalldataFramgment _ = error "Internal error: only static types are supported" + inRange :: AbiType -> Exp AInteger -> Exp ABoolean -- if the type has the type of machine word then check per operation inRange (AbiUIntType 256) e = checkOp e @@ -331,7 +362,7 @@ inRange t e = bound t e checkOp :: Exp AInteger -> Exp ABoolean checkOp (LitInt _ i) = LitBool nowhere $ i <= (fromIntegral (maxBound :: Word256)) -checkOp (Var _ _ _) = LitBool nowhere True +checkOp (Var _ _ _ _) = LitBool nowhere True checkOp (TEntry _ _ _) = LitBool nowhere True checkOp e@(Add _ e1 _) = LEQ nowhere e1 e -- check for addition overflow checkOp e@(Sub _ e1 _) = LEQ nowhere e e1 @@ -365,7 +396,7 @@ checkEquiv solvers opts l1 l2 = checkConstructors :: SolverGroup -> VeriOpts -> ByteString -> ByteString -> Act -> IO () checkConstructors solvers opts initcode runtimecode act = do let (_, actbehvs, calldata) = translateActConstr act runtimecode - let initVM = abstractVM calldata initcode Nothing (EVM.ConcreteStore mempty) True + 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 let solbehvs = removeFails $ flattenExpr simpl @@ -376,13 +407,10 @@ checkConstructors solvers opts initcode runtimecode act = do where removeFails branches = filter isSuccess $ branches - isSuccess (EVM.Success _ _ _ _) = True - isSuccess _ = False - checkBehaviours :: SolverGroup -> VeriOpts -> ByteString -> Act -> IO () checkBehaviours solvers opts bytecode act = do - let actbehvs = translateActBehvs act + let actbehvs = translateActBehvs act bytecode flip mapM_ actbehvs $ \(name,behvs,calldata) -> do solbehvs <- removeFails <$> getBranches solvers bytecode calldata putStrLn $ "\x1b[1mChecking behavior \x1b[4m" <> name <> "\x1b[m of Act\x1b[m" @@ -395,9 +423,6 @@ checkBehaviours solvers opts bytecode act = do where removeFails branches = filter isSuccess $ branches - isSuccess (EVM.Success _ _ _ _) = True - isSuccess _ = False - -- | Find the input space of an expr list inputSpace :: [EVM.Expr EVM.End] -> [EVM.Prop] inputSpace exprs = map aux exprs @@ -411,8 +436,8 @@ checkInputSpaces :: SolverGroup -> VeriOpts -> [EVM.Expr EVM.End] -> [EVM.Expr E checkInputSpaces solvers opts l1 l2 = do let p1 = inputSpace l1 let p2 = inputSpace l2 - let queries = fmap assertProps [ [ EVM.PNeg (EVM.por p1), EVM.por p2 ] - , [ EVM.por p1, EVM.PNeg (EVM.por p2) ] ] + let queries = fmap (assertProps abstRefineDefault) [ [ EVM.PNeg (EVM.por p1), EVM.por p2 ] + , [ EVM.por p1, EVM.PNeg (EVM.por p2) ] ] when opts.debug $ forM_ (zip [(1 :: Int)..] queries) $ \(idx, q) -> do TL.writeFile @@ -438,7 +463,7 @@ checkAbi solver opts act bytecode = do let txdata = EVM.AbstractBuf "txdata" let selectorProps = assertSelector txdata <$> nubOrd (actSigs act) evmBehvs <- getBranches solver bytecode (txdata, []) - let queries = fmap assertProps $ filter (/= []) $ fmap (checkBehv selectorProps) evmBehvs + let queries = fmap (assertProps abstRefineDefault) $ filter (/= []) $ fmap (checkBehv selectorProps) evmBehvs when opts.debug $ forM_ (zip [(1 :: Int)..] queries) $ \(idx, q) -> do TL.writeFile @@ -465,9 +490,8 @@ checkAbi solver opts act bytecode = do -- | 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 - let - bytecode = if BS.null bs then BS.pack [0] else bs - prestate = abstractVM calldata bytecode Nothing EVM.AbstractStore False + let bytecode = if BS.null bs then BS.pack [0] else bs + prestate <- stToIO $ abstractVM calldata bytecode Nothing False expr <- interpret (Fetch.oracle solvers Nothing) Nothing 1 StackBased prestate runExpr let simpl = if True then (simplify expr) else expr let nodes = flattenExpr simpl @@ -513,12 +537,6 @@ toVRes msg res = case res of Error e -> error $ "Internal Error: solver responded with error: " <> show e --- TODO this is also defined in hevm-cli -getCex :: ProofResult a b c -> Maybe b -getCex (Cex c) = Just c -getCex _ = Nothing - - checkResult :: [EquivResult] -> IO () checkResult res = case any isCex res of diff --git a/src/K.hs b/src/K.hs index 0b9bbad7..56a6c8d3 100644 --- a/src/K.hs +++ b/src/K.hs @@ -129,7 +129,7 @@ kExpr (Eq _ t a b) = kExpr (ByStr _ str) = show str kExpr (ByLit _ bs) = show bs kExpr (TEntry _ t item) = kStorageName t item -kExpr (Var _ _ a) = kVar a +kExpr (Var _ _ _ a) = kVar a kExpr v = error ("Internal error: TODO kExpr of " <> show v) --kExpr (Cat a b) = --kExpr (Slice a start end) = diff --git a/src/Print.hs b/src/Print.hs index 29acbe44..9b526967 100644 --- a/src/Print.hs +++ b/src/Print.hs @@ -90,7 +90,7 @@ prettyExp e = case e of --polymorphic ITE _ a b c -> "(if " <> prettyExp a <> " then " <> prettyExp b <> " else " <> prettyExp c <> ")" TEntry _ t a -> timeParens t $ prettyItem a - Var _ _ x -> x + Var _ _ _ x -> x where print2 sym a b = "(" <> prettyExp a <> " " <> sym <> " " <> prettyExp b <> ")" @@ -175,9 +175,8 @@ prettyInvPred = prettyExp . untime . fst ITE p x y z -> ITE p (untime x) (untime y) (untime z) Slice p a b c -> Slice p (untime a) (untime b) (untime c) TEntry p _ (Item t vt a) -> TEntry p Neither (Item t vt (untimeStorageRef a)) - Var p t a -> Var p t a - - + Var p t at a -> Var p t at a + -- | prints a Doc, with wider output than the built in `putDoc` render :: Doc -> IO () render doc = displayIO stdout (renderPretty 0.9 120 doc) diff --git a/src/SMT.hs b/src/SMT.hs index b36642e1..38ac6e45 100644 --- a/src/SMT.hs +++ b/src/SMT.hs @@ -619,7 +619,7 @@ expToSMT2 expr = case expr of Eq _ _ a b -> binop "=" a b NEq p s a b -> unop "not" (Eq p s a b) ITE _ a b c -> triop "ite" a b c - Var _ _ a -> nameFromVarId a + Var _ _ _ a -> nameFromVarId a TEntry _ w item -> entry item w where unop :: String -> Exp a -> Ctx SMT2 diff --git a/src/Syntax/TimeAgnostic.hs b/src/Syntax/TimeAgnostic.hs index 29f46a8e..0f974e7e 100644 --- a/src/Syntax/TimeAgnostic.hs +++ b/src/Syntax/TimeAgnostic.hs @@ -229,7 +229,7 @@ data Exp (a :: ActType) (t :: Timing) where Eq :: Pn -> SType a -> Exp a t -> Exp a t -> Exp ABoolean t NEq :: Pn -> SType a -> Exp a t -> Exp a t -> Exp ABoolean t ITE :: Pn -> Exp ABoolean t -> Exp a t -> Exp a t -> Exp a t - Var :: Pn -> SType a -> Id -> Exp a t + Var :: Pn -> SType a -> AbiType -> Id -> Exp a t TEntry :: Pn -> Time t -> TStorageItem a t -> Exp a t deriving instance Show (Exp a t) @@ -271,7 +271,7 @@ instance Eq (Exp a t) where ITE _ a b c == ITE _ d e f = a == d && b == e && c == f TEntry _ a t == TEntry _ b u = a == b && t == u - Var _ _ a == Var _ _ b = a == b + Var _ _ _ a == Var _ _ _ b = a == b Create _ a b == Create _ c d = a == c && b == d @@ -331,7 +331,7 @@ instance Timable (Exp a) where NEq p s x y -> NEq p s (go x) (go y) ITE p x y z -> ITE p (go x) (go y) (go z) TEntry p _ item -> TEntry p time (go item) - Var p t x -> Var p t x + Var p t a x -> Var p t a x where go :: Timable c => c Untimed -> c Timed go = setTime time @@ -486,7 +486,7 @@ instance ToJSON (Exp a t) where toJSON (ByEnv _ a) = String . pack $ show a toJSON (TEntry _ t a) = object [ fromString (show t) .= toJSON a ] - toJSON (Var _ _ a) = toJSON a + toJSON (Var _ _ _ a) = toJSON a toJSON (Create _ f xs) = object [ "symbol" .= pack "create" , "arity" .= Data.Aeson.Types.Number 2 , "args" .= Array (fromList [object [ "fun" .= String (pack f) ], toJSON xs]) ] @@ -559,5 +559,5 @@ uintmin _ = 0 uintmax :: Int -> Integer uintmax a = 2 ^ a - 1 -_Var :: SingI a => Id -> Exp a t -_Var = Var nowhere sing +_Var :: SingI a => AbiType -> Id -> Exp a t +_Var atyp = Var nowhere sing atyp diff --git a/src/Type.hs b/src/Type.hs index add6c454..8dcf4805 100644 --- a/src/Type.hs +++ b/src/Type.hs @@ -159,7 +159,7 @@ data Env = Env { contract :: Id -- ^ The name of the current contract. , store :: Map Id SlotType -- ^ This contract's storage entry names and their types. , theirs :: Store -- ^ Mapping from contract names to a map of their entry names and their types. - , calldata :: Map Id ActType -- ^ The calldata var names and their types. + , calldata :: Map Id AbiType -- ^ The calldata var names and their types. , constructors :: Map Id [AbiType] -- ^ Interfaces of contract contructors (we only allow constructor calls ATM) } @@ -195,7 +195,7 @@ mkEnv contract store constructors = Env addCalldata :: Env -> [Decl] -> Env addCalldata env decls = env{ calldata = abiVars } where - abiVars = Map.fromList $ map (\(Decl typ var) -> (var, fromAbiType typ)) decls + abiVars = Map.fromList $ map (\(Decl typ var) -> (var, typ)) decls @@ -389,7 +389,7 @@ checkIffs env = foldr check (pure []) genInRange :: AbiType -> Exp AInteger t -> [Exp ABoolean t] genInRange t e@(LitInt _ _) = [InRange nowhere t e] -genInRange t e@(Var _ _ _) = [InRange nowhere t e] +genInRange t e@(Var _ _ _ _) = [InRange nowhere t e] genInRange t e@(TEntry _ _ _) = [InRange nowhere t e] genInRange t e@(Add _ e1 e2) = [InRange nowhere t e] <> genInRange t e1 <> genInRange t e2 genInRange t e@(Sub _ e1 e2) = [InRange nowhere t e] <> genInRange t e1 <> genInRange t e2 @@ -501,7 +501,7 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of checkCalldataEntry Env{store,calldata} (U.EVar p name) = case (Map.lookup name store, Map.lookup name calldata) of (Nothing, Nothing) -> throw (p, "Unknown variable " <> name) (Just _, Just _) -> throw (p, "Ambiguous variable " <> name) - (Nothing, Just (FromAct varType)) -> Var p typ name <$ checkEq p typ varType + (Nothing, Just at@(FromAbi varType)) -> Var p typ at name <$ checkEq p typ varType (Just _, Nothing) -> error "Internal error: variable must be in calldata" checkCalldataEntry _ _ = error "Internal error: variable cannot be mapping or contract field" @@ -509,7 +509,7 @@ checkExpr env@Env{constructors} typ e = case (typ, e) of -- | Find the contract id of an expression with contract type contractId :: Exp AContract t -> Id contractId (ITE _ _ a _) = contractId a -contractId (Var _ _ _) = error "Internal error: calldata variables cannot have contract types" +contractId (Var _ _ _ _) = error "Internal error: calldata variables cannot have contract types" contractId (Create _ c _) = c contractId (TEntry _ _ (Item _ (ContractType c) _)) = c contractId (TEntry _ _ (Item _ _ _)) = error "Internal error: entry does not have contract type" diff --git a/src/test/Test.hs b/src/test/Test.hs index 27db442a..7c7b1e68 100644 --- a/src/test/Test.hs +++ b/src/test/Test.hs @@ -161,12 +161,12 @@ genTypedExp names n = oneof -- TODO: literals, cat slice, ITE, storage, ByStr genExpBytes :: Names -> Int -> ExpoGen (Exp AByteStr) -genExpBytes names _ = _Var <$> selectName AByteStr names +genExpBytes names _ = _Var (AbiBytesType 32) <$> selectName AByteStr names -- TODO: ITE, storage genExpBool :: Names -> Int -> ExpoGen (Exp ABoolean) genExpBool names 0 = oneof - [ _Var <$> selectName ABoolean names + [ _Var AbiBoolType <$> selectName ABoolean names , LitBool nowhere <$> liftGen arbitrary ] genExpBool names n = oneof @@ -192,7 +192,7 @@ genExpBool names n = oneof genExpInt :: Names -> Int -> ExpoGen (Exp AInteger) genExpInt names 0 = oneof [ LitInt nowhere <$> liftGen arbitrary - , _Var <$> selectName AInteger names + , _Var (AbiUIntType 256) <$> selectName AInteger names , return $ IntEnv nowhere Caller , return $ IntEnv nowhere Callvalue , return $ IntEnv nowhere Calldepth