module LLVM.Analysis.NullPointers (
HasNullSummary(..),
NullPointersSummary,
nullPointersAnalysis,
nullPointersAt,
notNullPointersAt,
branchNullInfo,
NullInfoError(..)
) where
import Control.Failure
import Data.Functor.Identity
import Data.Maybe ( fromMaybe )
import Data.Monoid
import Data.HashSet ( HashSet )
import qualified Data.HashSet as HS
import Data.Typeable ( Typeable )
import LLVM.Analysis
import LLVM.Analysis.CFG
import LLVM.Analysis.Dataflow
class HasNullSummary a where
getNullSummary :: a -> NullPointersSummary
instance HasNullSummary NullPointersSummary where
getNullSummary = id
data NULLState = Top
| NS (HashSet Value) (HashSet Value)
deriving (Eq, Show)
newtype NullPointersSummary =
NPS (DataflowResult Identity NULLState)
deriving (Eq, Show)
nullPointersAnalysis :: (HasCFG cfg) => cfg -> NullPointersSummary
nullPointersAnalysis cfgLike =
NPS $ runIdentity $ dataflow cfgLike analysis f0
where
f0 = NS mempty mempty
analysis = fwdDataflowEdgeAnalysis Top meet transfer edgeTransfer
nullPointersAt :: NullPointersSummary -> Instruction -> [Value]
nullPointersAt (NPS summ) i =
case runIdentity $ dataflowResultAt summ i of
Top -> []
NS mustNull _ -> HS.toList mustNull
notNullPointersAt :: NullPointersSummary -> Instruction -> [Value]
notNullPointersAt (NPS summ) i =
case runIdentity $ dataflowResultAt summ i of
Top -> []
NS _ notNull -> HS.toList notNull
meet :: NULLState -> NULLState -> NULLState
meet Top other = other
meet other Top = other
meet (NS must1 not1) (NS must2 not2) =
NS (must1 `HS.intersection` must2) (not1 `HS.intersection` not2)
transfer :: (Monad m) => NULLState -> Instruction -> m NULLState
transfer s _ = return s
edgeTransfer :: (Monad m ) => NULLState -> Instruction -> m [(BasicBlock, NULLState)]
edgeTransfer s i = return $ fromMaybe [] $ do
(nullBlock, nullVal, notNullBlock) <- branchNullInfo i
return [(nullBlock, addNull nullVal s),
(notNullBlock, addNotNull nullVal s)
]
isNullPtr :: Value -> Bool
isNullPtr (valueContent -> ConstantC ConstantPointerNull {}) = True
isNullPtr _ = False
data NullInfoError = NotABranchInst Instruction
| NotANullTest Instruction
deriving (Typeable, Show)
branchNullInfo :: (Failure NullInfoError m)
=> Instruction
-> m (BasicBlock, Value, BasicBlock)
branchNullInfo i@BranchInst { branchTrueTarget = tt
, branchFalseTarget = ft
, branchCondition = (valueContent -> InstructionC ci@ICmpInst { cmpPredicate = ICmpEq })
}
| isNullPtr (cmpV1 ci) = return (tt, cmpV2 ci, ft)
| isNullPtr (cmpV2 ci) = return (tt, cmpV1 ci, ft)
| otherwise = failure (NotANullTest i)
branchNullInfo i@BranchInst { branchTrueTarget = tt
, branchFalseTarget = ft
, branchCondition = (valueContent -> InstructionC ci@ICmpInst { cmpPredicate = ICmpNe })
}
| isNullPtr (cmpV1 ci) = return (ft, cmpV2 ci, tt)
| isNullPtr (cmpV2 ci) = return (ft, cmpV1 ci, tt)
| otherwise = failure (NotANullTest i)
branchNullInfo i = failure (NotABranchInst i)
addNull :: Value -> NULLState -> NULLState
addNull v s =
case s of
Top -> NS (HS.singleton v) mempty
NS must notNull -> NS (HS.insert v must) notNull
addNotNull :: Value -> NULLState -> NULLState
addNotNull v s =
case s of
Top -> NS mempty (HS.singleton v)
NS must notNull -> NS must (HS.insert v notNull)