From a9dc1a3509cbb2e530cc351cfbc622b4c94a4ce1 Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 1 Oct 2024 00:29:19 +0300 Subject: [PATCH] Refactor to use StateT and WIP in check aliasing --- src/Act/HEVM.hs | 262 +++++++++++++++++++++++++----------------------- 1 file changed, 138 insertions(+), 124 deletions(-) diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs index fef33bf9..e7116ffb 100644 --- a/src/Act/HEVM.hs +++ b/src/Act/HEVM.hs @@ -91,36 +91,36 @@ data ActEnv = ActEnv , caller :: Maybe (EVM.Expr EVM.EAddr) } -type ActM a = State ActEnv a +type ActT m a = StateT ActEnv m a -getCodemap :: ActM CodeMap +getCodemap :: Monad m => ActT m CodeMap getCodemap = do env <- get pure env.codemap -getFreshIncr :: ActM Int +getFreshIncr :: Monad m => ActT m Int getFreshIncr = do env <- get let fresh = env.fresh put (env { fresh = fresh + 1 }) pure (fresh + 1) -getFresh :: ActM Int +getFresh :: Monad m => ActT m Int getFresh = do env <- get pure env.fresh -getLayout :: ActM Layout +getLayout :: Monad m => ActT m Layout getLayout = do env <- get pure env.layout -getCaddr :: ActM (EVM.Expr EVM.EAddr) +getCaddr :: Monad m => ActT m (EVM.Expr EVM.EAddr) getCaddr = do env <- get pure env.caddr -localCaddr :: EVM.Expr EVM.EAddr -> ActM a -> ActM a +localCaddr :: Monad m => EVM.Expr EVM.EAddr -> ActT m a -> ActT m a localCaddr caddr m = do env <- get let caddr' = env.caddr @@ -131,7 +131,7 @@ localCaddr caddr m = do put (env' { caddr = caddr', caller = caller' }) pure res -getCaller :: ActM (EVM.Expr EVM.EAddr) +getCaller :: Monad m => ActT m (EVM.Expr EVM.EAddr) getCaller = do env <- get case env.caller of @@ -141,7 +141,7 @@ getCaller = do -- * Act translation -translateConstructor :: BS.ByteString -> Constructor -> ContractMap -> ActM ([EVM.Expr EVM.End], Calldata, Sig) +translateConstructor :: Monad m => BS.ByteString -> Constructor -> ContractMap -> ActT m ([EVM.Expr EVM.End], Calldata, Sig) translateConstructor bytecode (Constructor _ iface _ preconds _ _ upds) cmap = do let initmap = M.insert initAddr initcontract cmap preconds' <- mapM (toProp initmap) preconds @@ -160,7 +160,7 @@ translateConstructor bytecode (Constructor _ iface _ preconds _ _ upds) cmap = d symAddrCnstr :: Int -> Int -> [EVM.Prop] symAddrCnstr start end = fmap (\i -> EVM.PNeg (EVM.PEq (EVM.WAddr (EVM.SymAddr $ "freshSymAddr" <> (T.pack $ show i))) (EVM.Lit 0))) [start..end] -translateBehvs :: ContractMap -> [Behaviour] -> ActM [(Id, [EVM.Expr EVM.End], Calldata, Sig)] +translateBehvs :: Monad m => ContractMap -> [Behaviour] -> ActT m [(Id, [EVM.Expr EVM.End], Calldata, Sig)] translateBehvs cmap behvs = do let groups = (groupBy sameIface behvs) :: [[Behaviour]] mapM (\behvs' -> do @@ -185,7 +185,7 @@ ifaceToSig (Interface name args) = Sig (T.pack name) (fmap fromdecl args) where fromdecl (Decl t _) = t -translateBehv :: ContractMap -> Behaviour -> ActM (EVM.Expr EVM.End) +translateBehv :: Monad m => ContractMap -> Behaviour -> ActT m (EVM.Expr EVM.End) translateBehv cmap (Behaviour _ _ _ _ preconds caseconds _ upds ret) = do fresh <- getFresh preconds' <- mapM (toProp cmap) preconds @@ -196,10 +196,10 @@ translateBehv cmap (Behaviour _ _ _ _ preconds caseconds _ upds ret) = do pure $ EVM.Success (preconds' <> caseconds' <> symAddrCnstr (fresh+1) fresh') mempty ret' store -applyUpdates :: ContractMap -> ContractMap -> [StorageUpdate] -> ActM ContractMap +applyUpdates :: Monad m => ContractMap -> ContractMap -> [StorageUpdate] -> ActT m ContractMap applyUpdates readMap writeMap upds = foldM (applyUpdate readMap) writeMap upds -applyUpdate :: ContractMap -> ContractMap -> StorageUpdate -> ActM ContractMap +applyUpdate :: Monad m => ContractMap -> ContractMap -> StorageUpdate -> ActT m ContractMap applyUpdate readMap writeMap (Update typ (Item _ vtyp ref) e) = do caddr' <- baseAddr readMap ref offset <- refOffset readMap ref @@ -233,7 +233,7 @@ applyUpdate readMap writeMap (Update typ (Item _ vtyp ref) e) = do updateNonce c@(EVM.C _ _ _ Nothing) = c updateNonce (EVM.GVar _) = error "Internal error: contract cannot be a global variable" -createContract :: ContractMap -> ContractMap -> EVM.Expr EVM.EAddr -> Exp AInteger -> ActM ContractMap +createContract :: Monad m => ContractMap -> ContractMap -> EVM.Expr EVM.EAddr -> Exp AInteger -> ActT m ContractMap createContract readMap writeMap freshAddr (Create _ cid args) = do codemap <- getCodemap case M.lookup cid codemap of @@ -321,7 +321,7 @@ substExp subst expr = case expr of Create pn a b -> Create pn a (substArgs subst b) -returnsToExpr :: ContractMap -> Maybe TypedExp -> ActM (EVM.Expr EVM.Buf) +returnsToExpr :: Monad m => ContractMap -> Maybe TypedExp -> ActT m (EVM.Expr EVM.Buf) returnsToExpr _ Nothing = pure $ EVM.ConcreteBuf "" returnsToExpr cmap (Just r) = typedExpToBuf cmap r @@ -331,12 +331,12 @@ wordToBuf w = EVM.WriteWord (EVM.Lit 0) w (EVM.ConcreteBuf "") wordToProp :: EVM.Expr EVM.EWord -> EVM.Prop wordToProp w = EVM.PNeg (EVM.PEq w (EVM.Lit 0)) -typedExpToBuf :: ContractMap -> TypedExp -> ActM (EVM.Expr EVM.Buf) +typedExpToBuf :: Monad m => ContractMap -> TypedExp -> ActT m (EVM.Expr EVM.Buf) typedExpToBuf cmap expr = case expr of TExp styp e -> expToBuf cmap styp e -expToBuf :: forall a. ContractMap -> SType a -> Exp a -> ActM (EVM.Expr EVM.Buf) +expToBuf :: Monad m => forall a. ContractMap -> SType a -> Exp a -> ActT m (EVM.Expr EVM.Buf) expToBuf cmap styp e = do case styp of SInteger -> do @@ -355,7 +355,7 @@ getSlot layout cid name = Nothing -> error $ "Internal error: invalid variable name: " <> show name Nothing -> error "Internal error: invalid contract name" -refOffset :: ContractMap -> StorageRef -> ActM (EVM.Expr EVM.EWord) +refOffset :: Monad m => ContractMap -> StorageRef -> ActT m (EVM.Expr EVM.EWord) refOffset _ (SVar _ cid name) = do layout <- getLayout let slot = getSlot layout cid name @@ -370,13 +370,13 @@ refOffset _ (SField _ _ cid name) = do let slot = getSlot layout cid name pure $ EVM.Lit (fromIntegral slot) -baseAddr :: ContractMap -> StorageRef -> ActM (EVM.Expr EVM.EAddr) +baseAddr :: Monad m => ContractMap -> StorageRef -> ActT m (EVM.Expr EVM.EAddr) baseAddr _ (SVar _ _ _) = getCaddr baseAddr cmap (SField _ ref _ _) = refAddr cmap ref baseAddr cmap (SMapping _ ref _) = baseAddr cmap ref -- | find the contract that is stored in the given reference of contract type -refAddr :: ContractMap -> StorageRef -> ActM (EVM.Expr EVM.EAddr) +refAddr :: Monad m => ContractMap -> StorageRef -> ActT m (EVM.Expr EVM.EAddr) refAddr cmap (SVar _ c x) = do caddr <- getCaddr case M.lookup caddr cmap of @@ -401,7 +401,7 @@ refAddr cmap (SField _ ref c x) = do Nothing -> error "Internal error: contract not found" refAddr _ (SMapping _ _ _) = error "Internal error: mapping address not suppported" -ethEnvToWord :: EthEnv -> ActM (EVM.Expr EVM.EWord) +ethEnvToWord :: Monad m => EthEnv -> ActT m (EVM.Expr EVM.EWord) ethEnvToWord Callvalue = pure $ EVM.TxValue ethEnvToWord Caller = do c <- getCaller @@ -424,7 +424,7 @@ ethEnvToBuf :: EthEnv -> EVM.Expr EVM.Buf ethEnvToBuf _ = error "Internal error: there are no bytestring environment values" -toProp :: ContractMap -> Exp ABoolean -> ActM EVM.Prop +toProp :: Monad m => ContractMap -> Exp ABoolean -> ActT m EVM.Prop toProp cmap = \case (And _ e1 e2) -> pop2 EVM.PAnd e1 e2 (Or _ e1 e2) -> pop2 EVM.POr e1 e2 @@ -452,13 +452,13 @@ toProp cmap = \case (TEntry _ _ _) -> error "TODO" -- EVM.SLoad addr idx (InRange _ t e) -> toProp cmap (inRange t e) where - op2 :: forall a b. (EVM.Expr (ExprType b) -> EVM.Expr (ExprType b) -> a) -> Exp b -> Exp b -> ActM a + op2 :: Monad m => forall a b. (EVM.Expr (ExprType b) -> EVM.Expr (ExprType b) -> a) -> Exp b -> Exp b -> ActT m a op2 op e1 e2 = do e1' <- toExpr cmap e1 e2' <- toExpr cmap e2 pure $ op e1' e2' - pop2 :: forall a. (EVM.Prop -> EVM.Prop -> a) -> Exp ABoolean -> Exp ABoolean -> ActM a + pop2 :: Monad m => forall a. (EVM.Prop -> EVM.Prop -> a) -> Exp ABoolean -> Exp ABoolean -> ActT m a pop2 op e1 e2 = do e1' <- toProp cmap e1 e2' <- toProp cmap e2 @@ -475,7 +475,7 @@ stripMods = mapExpr go go (EVM.Mod a (EVM.Lit MAX_UINT)) = a go a = a -toExpr :: forall a. ContractMap -> Exp a -> ActM (EVM.Expr (ExprType a)) +toExpr :: Monad m => forall a. ContractMap -> Exp a -> ActT m (EVM.Expr (ExprType a)) toExpr cmap = liftM stripMods . go where go = \case @@ -546,7 +546,7 @@ toExpr cmap = liftM stripMods . go e -> error $ "TODO: " <> show e - op2 :: forall b c. (EVM.Expr (ExprType c) -> EVM.Expr (ExprType c) -> b) -> Exp c -> Exp c -> ActM b + op2 :: Monad m => forall b c. (EVM.Expr (ExprType c) -> EVM.Expr (ExprType c) -> b) -> Exp c -> Exp c -> ActT m b op2 op e1 e2 = do e1' <- toExpr cmap e1 e2' <- toExpr cmap e2 @@ -600,56 +600,103 @@ checkEquiv solvers l1 l2 = do toEquivRes (Timeout b) = Timeout b +-- | Merge two contract states +-- mergeContractState :: App m => SolverGroup -> Constructor -> [ContractMap] -> m (Error String ()) +-- mergeContractState solvers (Constructor _ _ _ _ _ _ _) cmaps = -getInitContractState :: Constructor -> Store -> CodeMap -> Int -> (ContractMap, Int) -getInitContractState (Constructor _ _ pointers _ _ _ _) store codemap fresh = - let casts = (\(PointsTo _ x c) -> (x, c)) <$> pointers in - let casts' = groupBy (\x y -> fst x == fst y) casts in - let (cmaps, fresh''') = foldl (\(maps, fresh') ptr -> - let (cmap, fresh'') = getContractState fresh' (nub ptr) in (cmap : maps, fresh'') - ) ([], fresh) casts' in - let actstorage = M.empty in -- mergeContractaps cmaps fresh ctor in - (actstorage, fresh''') +-- | Checks that all the given addresses are mutually distinct in the context of given interface and preconditions +checkAliasing :: App m => SolverGroup -> Interface -> [Exp ABoolean] -> [Exp AInteger] -> m (Error String ()) +checkAliasing solver iface@(Interface ifaceName decls) preconds addresses@(_:_) = do + let addressquery = [prelude <> SMT2 (fmap fromString $ lines . show . prettyAnsi $ mksmt) mempty mempty mempty] + res <- liftIO $ mapConcurrently (checkSat solver) addressquery + checkResult (makeCalldata iface) Nothing (fmap (toVRes msg) res) where + -- declare vars + args = SMT.declareArg ifaceName <$> decls + envs = SMT.declareEthEnv <$> concatMap ethEnvFromExp preconds + -- constraints + asserts = SMT.mkAssert ifaceName <$> ((existEqual (combine addresses [])):preconds) + mksmt = SMT.SMTExp + { SMT._storage = [] + , SMT._calldata = args + , SMT._environment = envs + , SMT._assertions = asserts + } + + combine :: [Exp AInteger] -> [[(Exp AInteger,Exp AInteger)]] -> [(Exp AInteger,Exp AInteger)] + combine [] acc = concat acc + combine (x:xs) acc = combine xs ([(x,y) | y <- xs]:acc) + + existEqual :: [(Exp AInteger,Exp AInteger)] -> Exp ABoolean + existEqual ls = foldl (\p (x,y) -> Or nowhere (Eq nowhere SInteger x y) p) (LitBool nowhere False) ls + + msg = "\x1b[1m Input addresses are not guaranteed to be unique!\x1b[m" + + prelude :: SMT2 + prelude = SMT2 src mempty mempty mempty + where + src = [ "; logic", + "(set-info :smt-lib-version 2.6)", + "(set-logic ALL)" ] +checkAliasing _ _ _ _ = pure $ Success () + + + +-- mergeContractaps cmaps fresh ctor + +-- -- | Create the initial contract state before analysing a contract +-- getInitContractState :: App m => Solvers -> Pointers -> ActT m (ContractMap, Int) +-- getInitContractState pointers = +-- let casts = (\(PointsTo _ x c) -> (x, c)) <$> pointers in +-- let casts' = groupBy (\x y -> fst x == fst y) casts in +-- let (cmaps, fresh''') = foldM l (\(maps, fresh') ptr -> do +-- (cmap, fresh'') <= getContractState fresh' (nub ptr) +-- pure (cmap : maps, fresh'') +-- ) ([], fresh) casts' in +-- let actstorage = flip addr pruneContractState $ M.empty in -- mergeContractaps cmaps fresh ctor in +-- pure (actstorage, fresh''') + +-- where - getContractState :: Int -> [(Id, Id)] -> (ContractMap, Int) - getContractState fresh [(x, cid)] = - let addr = EVM.SymAddr $ T.pack x in - case M.lookup cid codemap of - Just (Contract ctor@(Constructor _ _ _ _ _ _ upds) _, _, bytecode) -> - let (icmap, fresh') = getInitContractState ctor store codemap fresh in - let actenv = ActEnv codemap fresh' (slotMap store) addr Nothing in - - let contract = EVM.C { EVM.code = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode) - , EVM.storage = EVM.ConcreteStore mempty - , EVM.balance = EVM.Lit 0 - , EVM.nonce = Just 1 - } in - - let (cmap, actenv') = flip runState actenv $ applyUpdates (M.insert addr contract icmap) (M.insert addr contract icmap) upds in - let actstorage = abstractCmap cmap in - (actstorage, actenv'.fresh) - Nothing -> error $ "Internal error: Contract " <> cid <> " not found\n" <> show codemap - getContractState _ [] = error "Internal error: Cast cannot be empty" - getContractState _ _ = error "Error: Cannot have different casts to the same address" - - -checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Store -> Contract -> CodeMap -> m (Error String (ContractMap, ActEnv)) -checkConstructors solvers initcode runtimecode store (Contract ctor _) codemap = do +-- getContractState :: Int -> [(Id, Id)] -> m (Error String ((ContractMap, Int))) +-- getContractState [(x, cid)] = do +-- let addr = EVM.SymAddr $ T.pack x +-- case M.lookup cid codemap of +-- Just ((Contract Constructor _ ifface pointers preconds _ _ upds) _, _, bytecode) -> do +-- (icmap, fresh') <- getInitContractState pointers store codemap fresh +-- let actenv = ActEnv codemap fresh' (slotMap store) addr Nothing + +-- let contract = EVM.C { EVM.code = EVM.RuntimeCode (EVM.ConcreteRuntimeCode bytecode) +-- , EVM.storage = EVM.ConcreteStore mempty +-- , EVM.balance = EVM.Lit 0 +-- , EVM.nonce = Just 1 +-- } +-- let (cmap, actenv') = flip runState actenv $ applyUpdates (M.insert addr contract icmap) (M.insert addr contract icmap) upds +-- let actstorage = abstractCmap cmap -- TODO can prune happen at the top-level? +-- checkAliasing solvers iface preconds (\k -> EVar AInteger <$> pointers) fresh +-- pure (actstorage, actenv'.fresh) +-- Nothing -> error $ "Internal error: Contract " <> cid <> " not found\n" <> show codemap +-- getContractState _ [] = error "Internal error: Cast cannot be empty" +-- getContractState _ _ = error "Error: Cannot have different casts to the same address" + + +checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Contract -> ActT m (Error String ContractMap) +checkConstructors solvers initcode runtimecode (Contract ctor _) = do -- First find all casts from addresses and create a store where all asumed constracts are present -- currently ignoring any asts in behaviours, maybe prohibit them - let (actinitmap, fresh) = getInitContractState ctor store codemap 0 + let actinitmap = M.empty -- TODO getInitContractState ctor store codemap 0 let hevminitmap = translateCmap actinitmap -- Create the Act state - let actenv = ActEnv codemap fresh (slotMap store) (EVM.SymAddr "entrypoint") Nothing + -- let actenv = ActEnv codemap fresh (slotMap store) (EVM.SymAddr "entrypoint") Nothing -- = flip runState actenv $ -- Translate Act constructor to Expr - let ((actbehvs, calldata, sig), actenv') = flip runState actenv $ translateConstructor runtimecode ctor actinitmap + (actbehvs, calldata, sig) <- translateConstructor runtimecode ctor actinitmap -- check is any addresses casted to contracts can be aliased -- checkAliasingCtor solvers ctor (map fst casts) calldata -- Symbolically execute bytecode -- TODO check if contrainsts about preexistsing fresh symbolic addresses are necessary - solbehvs <- removeFails <$> getInitcodeBranches solvers initcode hevminitmap calldata (symAddrCnstr 1 fresh) fresh + fresh <- getFresh + solbehvs <- lift $ removeFails <$> getInitcodeBranches solvers initcode hevminitmap calldata (symAddrCnstr 1 fresh) fresh -- traceM "Solc behvs: " -- traceM $ showBehvs solbehvs @@ -657,11 +704,11 @@ checkConstructors solvers initcode runtimecode store (Contract ctor _) codemap = -- traceM $ showBehvs actbehvs -- Check equivalence - showMsg "\x1b[1mChecking if constructor results are equivalent.\x1b[m" - res1 <- checkResult calldata (Just sig) =<< checkEquiv solvers solbehvs actbehvs - showMsg "\x1b[1mChecking if constructor input spaces are the same.\x1b[m" - res2 <- checkResult calldata (Just sig) =<< checkInputSpaces solvers solbehvs actbehvs - pure $ res1 *> res2 *> Success (abstractCmap $ getContractMap actbehvs, actenv') + lift $ showMsg "\x1b[1mChecking if constructor results are equivalent.\x1b[m" + res1 <- lift $ checkResult calldata (Just sig) =<< checkEquiv solvers solbehvs actbehvs + lift $ showMsg "\x1b[1mChecking if constructor input spaces are the same.\x1b[m" + res2 <- lift $ checkResult calldata (Just sig) =<< checkInputSpaces solvers solbehvs actbehvs + pure $ res1 *> res2 *> Success (abstractCmap initAddr $ getContractMap actbehvs) where removeFails branches = filter isSuccess $ branches @@ -669,21 +716,22 @@ getContractMap :: [EVM.Expr EVM.End] -> ContractMap getContractMap [EVM.Success _ _ _ m] = m getContractMap _ = error "Internal error: unexpected shape of Act translation" -checkBehaviours :: forall m. App m => SolverGroup -> Contract -> ActEnv -> ContractMap -> m (Error String ()) -checkBehaviours solvers (Contract _ behvs) actenv actstorage = do +checkBehaviours :: forall m. App m => SolverGroup -> Contract -> ContractMap -> ActT m (Error String ()) +checkBehaviours solvers (Contract _ behvs) actstorage = do let hevmstorage = translateCmap actstorage - let actbehvs = fst $ flip runState actenv $ translateBehvs actstorage behvs + fresh <- getFresh + actbehvs <- translateBehvs actstorage behvs (liftM $ concatError def) $ flip mapM actbehvs $ \(name,behvs',calldata, sig) -> do - solbehvs <- removeFails <$> getRuntimeBranches solvers hevmstorage calldata actenv.fresh - showMsg $ "\x1b[1mChecking behavior \x1b[4m" <> name <> "\x1b[m of Act\x1b[m" + solbehvs <- lift $ removeFails <$> getRuntimeBranches solvers hevmstorage calldata fresh + lift $ showMsg $ "\x1b[1mChecking behavior \x1b[4m" <> name <> "\x1b[m of Act\x1b[m" -- check for potential alliasing in the initial state -- checkAliasingBehv solvers ctor (map fst casts) calldata -- equivalence check - showMsg $ "\x1b[1mChecking if behaviour is matched by EVM\x1b[m" - res1 <- checkResult calldata (Just sig) =<< checkEquiv solvers solbehvs behvs' + lift $ showMsg $ "\x1b[1mChecking if behaviour is matched by EVM\x1b[m" + res1 <- lift $ checkResult calldata (Just sig) =<< checkEquiv solvers solbehvs behvs' -- input space exhaustiveness check - showMsg $ "\x1b[1mChecking if the input spaces are the same\x1b[m" - res2 <- checkResult calldata (Just sig) =<< checkInputSpaces solvers solbehvs behvs' + lift $ showMsg $ "\x1b[1mChecking if the input spaces are the same\x1b[m" + res2 <- lift $ checkResult calldata (Just sig) =<< checkInputSpaces solvers solbehvs behvs' pure $ res1 *> res2 where @@ -710,9 +758,8 @@ translateCmap cmap = (\(addr, c) -> (addr, toContract c)) <$> M.toList cmap -abstractCmap :: ContractMap -> ContractMap -abstractCmap cmap = prune $ M.mapWithKey makeContract cmap - +abstractCmap :: EVM.Expr EVM.EAddr -> ContractMap -> ContractMap +abstractCmap this cmap = pruneContractState this $ M.mapWithKey makeContract cmap where traverseStorage :: EVM.Expr EVM.EAddr -> EVM.Expr EVM.Storage -> EVM.Expr EVM.Storage traverseStorage addr (EVM.SStore offset (EVM.WAddr symaddr) storage) = @@ -726,11 +773,13 @@ abstractCmap cmap = prune $ M.mapWithKey makeContract cmap makeContract addr (EVM.C code storage _ _) = EVM.C code (traverseStorage addr storage) (EVM.Balance addr) (Just 0) makeContract _ (EVM.GVar _) = error "Internal error: contract cannot be gvar" - -- Remove garbage addresses - prune cmap' = - let reach = reachable initAddr cmap' in - M.filterWithKey (\k _ -> elem k reach) cmap' +-- | Remove unreachable addresses from a contract map +pruneContractState :: EVM.Expr EVM.EAddr -> ContractMap -> ContractMap +pruneContractState entryaddr cmap = + let reach = reachable entryaddr cmap in + M.filterWithKey (\k _ -> elem k reach) cmap + where -- Find reachable addresses from given address reachable :: EVM.Expr EVM.EAddr -> ContractMap -> [EVM.Expr EVM.EAddr] reachable addr cmap' = nub $ go addr @@ -784,42 +833,6 @@ checkInputSpaces solvers l1 l2 = do False -> pure $ filter (/= Qed ()) results' --- Checks that all the casted addresses of a contract are mutually distinct -checkAliasingCtor :: App m => SolverGroup -> Constructor -> [Exp AInteger] -> Calldata -> m (Error String ()) -checkAliasingCtor solver constructor@(Constructor _ (Interface ifaceName decls) _ preconds _ _ _) addresses@(_:_) calldata = do - let addressquery = [prelude <> SMT2 (fmap fromString $ lines . show . prettyAnsi $ mksmt) mempty mempty mempty] - res <- liftIO $ mapConcurrently (checkSat solver) addressquery - checkResult calldata Nothing (fmap (toVRes msg) res) - where - -- declare vars - args = SMT.declareArg ifaceName <$> decls - envs = SMT.declareEthEnv <$> ethEnvFromConstructor constructor - -- constraints - asserts = SMT.mkAssert ifaceName <$> ((existEqual (combine addresses [])):preconds) - mksmt = SMT.SMTExp - { SMT._storage = [] - , SMT._calldata = args - , SMT._environment = envs - , SMT._assertions = asserts - } - - combine :: [Exp AInteger] -> [[(Exp AInteger,Exp AInteger)]] -> [(Exp AInteger,Exp AInteger)] - combine [] acc = concat acc - combine (x:xs) acc = combine xs ([(x,y) | y <- xs]:acc) - - existEqual :: [(Exp AInteger,Exp AInteger)] -> Exp ABoolean - existEqual ls = foldl (\p (x,y) -> Or nowhere (Eq nowhere SInteger x y) p) (LitBool nowhere False) ls - - msg = "\x1b[1m Input addresses are not guaranteed to be unique!\x1b[m" - - prelude :: SMT2 - prelude = SMT2 src mempty mempty mempty - where - src = [ "; logic", - "(set-info :smt-lib-version 2.6)", - "(set-logic ALL)" ] -checkAliasingCtor _ _ _ _ = pure $ Success () - -- -- Checks that all the casted addresses of a contract are mutually distinct -- checkAliasing :: App m => SolverGroup -> Constructor -> ContractMap -> Calldata -> m (Error String ()) -- checkAliasingBehv solver behv@(Behaviour _ _ (Interface ifaceName decls) preconds caseconds _ _ _) cmap calldata = do @@ -891,14 +904,15 @@ checkAbi solver contract cmap = do checkContracts :: forall m. App m => SolverGroup -> Store -> M.Map Id (Contract, BS.ByteString, BS.ByteString) -> m (Error String ()) checkContracts solvers store codemap = + let actenv = ActEnv codemap 0 (slotMap store) (EVM.SymAddr "entrypoint") Nothing in liftM (concatError def) $ flip mapM (M.toList codemap) (\(_, (contract, initcode, bytecode)) -> do showMsg $ "\x1b[1mChecking contract \x1b[4m" <> nameOfContract contract <> "\x1b[m" - res <- checkConstructors solvers initcode bytecode store contract codemap + (res, actenv') <- flip runStateT actenv $ checkConstructors solvers initcode bytecode contract case res of - Success (cmap, actenv) -> do - behs <- checkBehaviours solvers contract actenv cmap + Success cmap -> do + (behvs, _) <- flip runStateT actenv' $ checkBehaviours solvers contract cmap abi <- checkAbi solvers contract cmap - pure $ behs *> abi + pure $ behvs *> abi Failure e -> pure $ Failure e) where def = Success ()