------------------------------------------------------------------------ -- | -- Module : Lang.Crucible.Analysis.ForwardDataflow -- Description : Forward dataflow analysis framework based on Kildall's algorithm -- Copyright : (c) Galois, Inc 2015 -- License : BSD3 -- Maintainer : Rob Dockins -- Stability : provisional -- -- This module defines a generic framework for forward dataflow analysis, -- with some additional control-flow data on the side. -- -- We calculate a fixpoint of a given analysis via the straightforward -- method of iterating the transfer function until no more updates occur. -- -- Our current method for doing this is quite naive, and more efficient -- methods exist. ------------------------------------------------------------------------ {-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeSynonymInstances #-} module Lang.Crucible.Analysis.ForwardDataflow {-# DEPRECATED "Lang.Crucible.Analysis.Fixpoint is a better implementation of these ideas" #-} where import Control.Lens import Control.Monad.State.Strict import Data.Kind import Data.Parameterized.Context ( Assignment ) import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.TraversableFC import Data.Set (Set) import qualified Data.Set as Set import Prelude hiding (foldr) import Prettyprinter import Lang.Crucible.Types import Lang.Crucible.CFG.Core import Lang.Crucible.CFG.Expr import qualified Debug.Trace as Debug ----------------------- data SymDom = Dead | Symbolic | Concrete deriving (Eq, Ord, Show) symbolicResults :: IsSyntaxExtension ext => CFG ext blocks init ret -- -> Assignment (Ignore SymDom) init -> String -- -> (Assignment (KildallPair (Assignment (Ignore SymDom)) SymDom) blocks, Ignore SymDom ret, SymDom) symbolicResults cfg = show $ kildall_forward symbolicAnalysis cfg (begin, Concrete) where sz = Ctx.size (blockInputs (getBlock (cfgEntryBlockID cfg) (cfgBlockMap cfg))) begin = Ctx.generate sz (\_ -> Ignore Symbolic) symlub :: SymDom -> SymDom -> SymDom symlub Dead x = x symlub x Dead = x symlub Symbolic _ = Symbolic symlub _ Symbolic = Symbolic symlub Concrete Concrete = Concrete sym_reg_transfer :: Reg ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom sym_reg_transfer reg asgn = ignoreOut $ asgn Ctx.! (regIndex reg) sym_expr_transfer :: IsSyntaxExtension ext => Expr ext ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom sym_expr_transfer (App a) asgn = foldApp (\r z -> symlub z $ sym_reg_transfer r asgn) Dead a -- FIXME this whole shabang is bogus, and should be replace by something that works... -- we assume every function other than "matlabFunctionHandle" returns a symbolic -- output, but does not have control flow that depends on symbolic data... sym_call_transfer :: CtxRepr args -> TypeRepr ret -> Reg ctx (FunctionHandleType args ret) -> Ignore SymDom (FunctionHandleType args ret) -> Assignment a args -> Ignore SymDom ret sym_call_transfer _ _ ex _ _ = Debug.trace (show $ pretty ex) $ Ignore Symbolic symbolicAnalysis :: IsSyntaxExtension ext => KildallForward ext blocks (Ignore SymDom) SymDom symbolicAnalysis = KildallForward { kfwd_lub = \(Ignore x) (Ignore y) -> Ignore (symlub x y) , kfwd_bot = Ignore Dead , kfwd_club = symlub , kfwd_cbot = Dead , kfwd_same = \(Ignore x) (Ignore y) -> x == y , kfwd_csame = \x y -> x == y , kfwd_br = \_ (Ignore x) y -> let z = symlub x y in (z, z) , kfwd_maybe = \_ _ (Ignore x) y -> let z = symlub x y in (z, Ignore x, z) , kfwd_reg = \_ ex asgn -> Ignore $ sym_reg_transfer ex asgn , kfwd_expr = \_ ex asgn -> Ignore $ sym_expr_transfer ex asgn , kfwd_call = sym_call_transfer , kfwd_rdglobal = \_ -> Ignore Symbolic -- FIXME, here we make the totally pessimistic assumption -- that every global variable read is symbolic , kfwd_onentry = \_ x -> x } ------------------- data KildallPair (a::k -> Type) (c :: Type) (tp::k) = KP (a tp) c instance (ShowF a, Show c) => Show (KildallPair a c tp) where show (KP x y) = "(" ++ showF x ++ ", " ++ show y ++ ")" instance (ShowF a, Show c) => ShowF (KildallPair a c) newtype Ignore a (b::k) = Ignore { ignoreOut :: a } deriving (Eq, Ord) instance Show a => Show (Ignore a tp) where show (Ignore x) = show x instance Show a => ShowF (Ignore a) data KildallForward ext blocks (a :: CrucibleType -> Type) c = KildallForward { kfwd_lub :: forall tp. a tp -> a tp -> a tp , kfwd_bot :: forall tp. a tp , kfwd_club :: c -> c -> c , kfwd_cbot :: c , kfwd_same :: forall tp. a tp -> a tp -> Bool , kfwd_csame :: c -> c -> Bool , kfwd_br :: forall ctx. Reg ctx BoolType -> a BoolType -> c -> (c, c) , kfwd_maybe :: forall ctx tp. TypeRepr tp -> Reg ctx (MaybeType tp) -> a (MaybeType tp) -> c -> (c, a tp, c) , kfwd_reg :: !(forall ctx tp. TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp) , kfwd_expr :: !(forall ctx tp. TypeRepr tp -> Expr ext ctx tp -> Assignment a ctx -> a tp) , kfwd_call :: forall ctx args ret. CtxRepr args -> TypeRepr ret -> Reg ctx (FunctionHandleType args ret) -> a (FunctionHandleType args ret) -> Assignment a args -> a ret , kfwd_rdglobal :: forall tp. GlobalVar tp -> a tp , kfwd_onentry :: forall ctx. BlockID blocks ctx -> (Assignment a ctx, c) -> (Assignment a ctx, c) } kildall_transfer :: forall ext a c blocks ret ctx . KildallForward ext blocks a c -> TypeRepr ret -> Block ext blocks ret ctx -> (Assignment a ctx, c) -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks))) kildall_transfer analysis retRepr blk = transfer_seq (_blockStmts blk) where transfer_seq :: forall ctx' . StmtSeq ext blocks ret ctx' -> (Assignment a ctx', c) -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks))) transfer_seq (ConsStmt _loc stmt ss) x = transfer_seq ss (transfer_stmt stmt x) transfer_seq (TermStmt _loc term) x = transfer_term term x transfer_stmt :: forall ctx1 ctx2. Stmt ext ctx1 ctx2 -> (Assignment a ctx1, c) -> (Assignment a ctx2, c) transfer_stmt (SetReg tp ex) (asgn, c) = (Ctx.extend asgn (kfwd_expr analysis tp ex asgn), c) transfer_stmt (CallHandle rettp ex argstp actuals) (asgn, c) = let xs = Ctx.zipWith (\tp act -> kfwd_reg analysis tp act asgn) argstp actuals ex_sh = kfwd_reg analysis (FunctionHandleRepr argstp rettp) ex asgn a' = kfwd_call analysis argstp rettp ex ex_sh xs in (Ctx.extend asgn a', c) transfer_stmt (Print _) asgn = asgn transfer_stmt (ReadGlobal gv) (asgn, c) = (Ctx.extend asgn (kfwd_rdglobal analysis gv), c) transfer_stmt FreshConstant{} _ = error "forward dataflow: fresh constant!" transfer_stmt FreshFloat{} _ = error "forward dataflow: fresh float!" transfer_stmt FreshNat{} _ = error "forward dataflow: fresh nat!" transfer_stmt ExtendAssign{} _ = error "extension statement!" transfer_stmt NewRefCell{} _ = error "forward dataflow: reference cell!" transfer_stmt NewEmptyRefCell{} _ = error "forward dataflow: reference cell!" transfer_stmt ReadRefCell{} _ = error "forward dataflow: reference cell!" transfer_stmt WriteRefCell{} _ = error "forward dataflow: reference cell!" transfer_stmt DropRefCell{} _ = error "forward dataflow: reference cell!" transfer_stmt (WriteGlobal _ _) asgnc = asgnc -- FIXME? need to check something here, perhaps? transfer_stmt (Assert _ _) asgnc = asgnc -- FIXME? is it useful to remember assertions some way? transfer_stmt (Assume _ _) asgnc = asgnc -- FIXME? is it useful to remember assertions some way? transfer_term :: forall ctx' . TermStmt blocks ret ctx' -> (Assignment a ctx', c) -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks))) transfer_term (ErrorStmt _) _ = return Set.empty transfer_term (Jump tgt) x = transfer_jump tgt x transfer_term (Br ex tgt1 tgt2) (asgn,c) = do let a = kfwd_reg analysis knownRepr ex asgn let (c1,c2) = kfwd_br analysis ex a c s1 <- transfer_jump tgt1 (asgn,c1) s2 <- transfer_jump tgt2 (asgn,c2) return (Set.union s1 s2) transfer_term (Return ex) (asgn, c) = do let a = kfwd_reg analysis retRepr ex asgn modify (\ (x,r,rc) -> (x, kfwd_lub analysis r a, kfwd_club analysis rc c)) return Set.empty transfer_term (TailCall fn callargs actuals) (asgn, c) = do let xs = Ctx.zipWith (\tp act -> kfwd_reg analysis tp act asgn) callargs actuals let fn_sh = kfwd_reg analysis (FunctionHandleRepr callargs retRepr) fn asgn let a' = kfwd_call analysis callargs retRepr fn fn_sh xs modify (\ (x,r,rc) -> (x, kfwd_lub analysis r a', kfwd_club analysis rc c)) return Set.empty transfer_term (MaybeBranch tp ex swtgt jmptgt) (asgn, c) = do let a = kfwd_reg analysis (MaybeRepr tp) ex asgn let (c1, a1, c2) = kfwd_maybe analysis tp ex a c s1 <- transfer_switch swtgt a1 (asgn, c1) s2 <- transfer_jump jmptgt (asgn, c2) return (Set.union s1 s2) transfer_term (VariantElim _ctx _ex _switch) (_asgn, _c) = do error "FIXME: transfer_term for VariantElim not implemented" transfer_switch :: forall ctx' tp . SwitchTarget blocks ctx' tp -> a tp -> (Assignment a ctx', c) -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks))) transfer_switch (SwitchTarget tgt argstp actuals) a1 (asgn, c) = do let xs = Ctx.zipWith (\tp act -> kfwd_reg analysis tp act asgn) argstp actuals let xs' = Ctx.extend xs a1 transfer_target tgt (xs', c) transfer_jump :: forall ctx' . JumpTarget blocks ctx' -> (Assignment a ctx', c) -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks))) transfer_jump (JumpTarget tgt argstp actuals) (asgn, c) = do let xs = Ctx.zipWith (\tp act -> kfwd_reg analysis tp act asgn) argstp actuals transfer_target tgt (xs, c) transfer_target :: forall ctx' . BlockID blocks ctx' -> (Assignment a ctx', c) -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks))) transfer_target tgt@(BlockID idx) (asgn, c) = do (x,r,rc) <- get let KP old oldc = x Ctx.! idx let new = Ctx.zipWith (\a b -> kfwd_lub analysis a b) old asgn let zipsame = Ctx.zipWith (\a b -> Ignore $ kfwd_same analysis a b) old new let samex = foldlFC (\a (Ignore b) -> a && b) True zipsame let newc = kfwd_club analysis c oldc let same = samex && kfwd_csame analysis oldc newc if same then return Set.empty else do put (x & ixF idx .~ KP new newc, r, rc) return (Set.singleton (Some tgt)) kildall_forward :: forall ext a c blocks ret init . KildallForward ext blocks a c -> CFG ext blocks init ret -> (Assignment a init, c) -> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) kildall_forward analysis cfg (asgn0,c0) = let initblk@(BlockID idx) = cfgEntryBlockID cfg freshAsgn :: Ctx.Index blocks ctx -> Assignment a ctx freshAsgn i = fmapFC (\_ -> kfwd_bot analysis) (blockInputs (getBlock (BlockID i) (cfgBlockMap cfg))) in execState (loop (Set.singleton (Some initblk))) ( Ctx.generate (Ctx.size (cfgBlockMap cfg)) $ \i -> case testEquality i idx of Just Refl -> KP asgn0 c0 Nothing -> KP (freshAsgn i) (kfwd_cbot analysis) , kfwd_bot analysis , kfwd_cbot analysis ) where visit :: Block ext blocks ret ctx -> (Assignment a ctx, c) -> Set (Some (BlockID blocks)) -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) () visit blk start worklist = do s <- kildall_transfer analysis (cfgReturnType cfg) blk start loop (Set.union s worklist) loop worklist = case Set.minView worklist of Nothing -> return () Just (Some tgt@(BlockID idx), worklist') -> do (x,_,_) <- get let (KP a c) = x Ctx.! idx (a',c') = kfwd_onentry analysis tgt (a,c) visit (getBlock tgt (cfgBlockMap cfg)) (a',c') worklist'