diff --git a/base/macaw-base.cabal b/base/macaw-base.cabal index 94cf069d..596b7e33 100644 --- a/base/macaw-base.cabal +++ b/base/macaw-base.cabal @@ -52,6 +52,7 @@ library Data.Macaw.AbsDomain.CallParams Data.Macaw.AbsDomain.JumpBounds Data.Macaw.AbsDomain.Refine + Data.Macaw.AbsDomain.StackAnalysis Data.Macaw.AbsDomain.StridedInterval Data.Macaw.Analysis.FunctionArgs Data.Macaw.Analysis.RegisterUse @@ -76,6 +77,7 @@ library Data.Macaw.Memory.Symbols Data.Macaw.SCFG Data.Macaw.Types + Data.Macaw.Utils.Changed Data.Macaw.Utils.Pretty ghc-options: -Wall -Wcompat diff --git a/base/src/Data/Macaw/AbsDomain/JumpBounds.hs b/base/src/Data/Macaw/AbsDomain/JumpBounds.hs index acdc6ae9..24b65a3c 100644 --- a/base/src/Data/Macaw/AbsDomain/JumpBounds.hs +++ b/base/src/Data/Macaw/AbsDomain/JumpBounds.hs @@ -1,15 +1,10 @@ {- | -This module defines a relational abstract domain for tracking relationships -between values in registers and on stack slots. It also maintains abstractions -of upper bounds for those values. - -The overall problem being solved with this abstract domain is tracking upper -bounds on values, but under the observation that sometimes compilers generate -code that performs bounds checks on values that have been copied to the stack, -but then later uses the value from the stack rather than the register that was -checked. Thus, we need a relational domain to track the equality between the -two values in order to learn the bounds on the copy on the stack. +This module defines a relational abstract domain for tracking bounds +checks emitted by the compiler on registers and stack location. This is +built on top of an underlying stack pointer tracking domain so that we +can include checks on stack locations and maintain constraints between +known equivalent values. -} {-# LANGUAGE DataKinds #-} @@ -24,105 +19,38 @@ two values in order to learn the bounds on the copy on the stack. module Data.Macaw.AbsDomain.JumpBounds ( -- * Initial jump bounds InitJumpBounds + , initBndsMap , functionStartBounds - , joinInitialBounds , ppInitJumpBounds - , boundsLocationInfo - , boundsLocationRep + , joinInitialBounds -- * IntraJumpbounds , IntraJumpBounds , mkIntraJumpBounds , execStatement , postCallBounds - , nextBlockBounds + , postJumpBounds , postBranchBounds , unsignedUpperBound - , stackOffset - -- * Low-level details - , ClassPred(..) - -- ** Locations and location maps - , BoundLoc(..) - , LocMap - , locMapEmpty - , locLookup - , locMapRegs - , locMapStack - , nonOverlapLocInsert - , locOverwriteWith - -- * Stack map - , StackMap - , emptyStackMap - , stackMapReplace - , stackMapOverwrite - , StackMapLookup(..) - , stackMapLookup - , ppStackMap ) where import Control.Monad.Reader -import Control.Monad.ST -import Control.Monad.State import Data.Bits -import Data.Functor -import Data.Kind -import Data.Map.Strict (Map) -import qualified Data.Map.Strict as Map -import Data.Maybe +import Data.Foldable import Data.Parameterized.Classes import Data.Parameterized.Map (MapF) import qualified Data.Parameterized.Map as MapF import Data.Parameterized.NatRepr import Data.Parameterized.Pair -import Data.Parameterized.TraversableF -import Data.Parameterized.TraversableFC -import Data.STRef -import GHC.Stack import Numeric.Natural import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) import Data.Macaw.AbsDomain.CallParams +import Data.Macaw.AbsDomain.StackAnalysis import Data.Macaw.CFG.App import Data.Macaw.CFG.Core import Data.Macaw.Memory import Data.Macaw.Types hiding (Type) -import qualified Data.Macaw.Types as M - -addrTypeRepr :: MemWidth w => TypeRepr (BVType w) -addrTypeRepr = BVTypeRepr memWidthNatRepr - ------------------------------------------------------------------------- --- Changed - --- | A monad that can be used to record when a value is changed. -type Changed s = ReaderT (STRef s Bool) (ST s) - --- | Record the value has changed if the Boolean is true. -markChanged :: Bool -> Changed s () -markChanged False = pure () -markChanged True = do - r <- ask - lift $ writeSTRef r True - -runChanged :: forall a . (forall s . Changed s a) -> Maybe a -runChanged action = runST $ do - r <- newSTRef False - a <- runReaderT action r - b <- readSTRef r - pure $! if b then Just a else Nothing - ------------------------------------------------------------------------- --- KeyPair - -data KeyPair (key :: k -> Type) (tp :: k) = KeyPair !(key tp) !(key tp) - -instance TestEquality k => TestEquality (KeyPair k) where - testEquality (KeyPair x1 x2) (KeyPair y1 y2) = do - Refl <- testEquality x1 y1 - testEquality x2 y2 - -instance OrdF k => OrdF (KeyPair k) where - compareF (KeyPair x1 x2) (KeyPair y1 y2) = - joinOrderingF (compareF x1 y1) (compareF x2 y2) +import Data.Macaw.Utils.Changed ------------------------------------------------------------------------ -- RangePred @@ -148,374 +76,55 @@ mkRangeBound :: NatRepr u -> Natural -> Natural -> RangePred u mkRangeBound w l u = RangePred w l u instance Pretty (RangePred u) where - pretty (RangePred w l h) = parens (hsep [pretty (intValue w), pretty (toInteger l), pretty (toInteger h)]) + pretty (RangePred w l h) = + parens (hsep [pretty (intValue w), pretty (toInteger l), pretty (toInteger h)]) ------------------------------------------------------------------------ --- ClassPred +-- MaybeRangePred -- | This describes a constraint associated with an equivalence class -- of registers in @InitJumpBounds@. -- -- The first parameter is the number of bits in the -data ClassPred (w :: Nat) tp where +data JustRangePred tp where -- | Predicate on bounds. - BoundedBV :: (u <= v) - => !(RangePred u) - -> ClassPred w (BVType v) + JustRangePred :: (u <= v) + => !(RangePred u) + -> JustRangePred (BVType v) - -- | Value is a offset of the stack pointer at the given offset argument. - IsStackOffset :: {-# UNPACK #-} !(MemInt w) - -> ClassPred w (BVType w) +ppJustRangePred :: Doc -> JustRangePred tp -> Doc +ppJustRangePred d (JustRangePred r) = d <+> text "in" <+> pretty r + +-- | This describes a constraint associated with an equivalence class +-- of registers in @InitJumpBounds@. +-- +-- The first parameter is the number of bits in the +data MaybeRangePred tp where + -- | Predicate on bounds. + SomeRangePred :: (u <= v) + => !(RangePred u) + -> MaybeRangePred (BVType v) -- | No constraints on value. - TopPred :: ClassPred w tp - -ppAddend :: MemInt w -> Doc -ppAddend o | memIntValue o < 0 = - text "-" <+> pretty (negate (toInteger (memIntValue o))) - | otherwise = text "+" <+> pretty o - --- | Pretty print the class predicate -ppClassPred :: Doc -> ClassPred w tp -> Doc -ppClassPred d (BoundedBV p) = - d <+> text "in" <+> pretty p -ppClassPred d (IsStackOffset i) = - d <+> text "= stack_frame" <+> ppAddend i -ppClassPred _d TopPred = - text "" - --- | Take the union of the old and new constraint, and record if the --- old constraint was weakened by the new constraint. -joinClassPred :: ClassPred w tp - -> ClassPred w tp - -> Changed s (ClassPred w tp) -joinClassPred old new = - case (old,new) of - (BoundedBV ob, BoundedBV nb) - | Just Refl <- testEquality (rangeWidth ob) (rangeWidth nb) - , Just r <- disjoinRangePred ob nb -> - let oldTighter = rangeLowerBound ob > rangeLowerBound ob - || rangeUpperBound ob < rangeUpperBound ob - in markChanged oldTighter $> BoundedBV r - (IsStackOffset i, IsStackOffset j) - | i == j -> pure $! old - (TopPred,_) -> pure TopPred - (_,_) -> markChanged True $> TopPred - ------------------------------------------------------------------------- --- BoundLoc - --- | Either a register or stack offset. --- --- These locations are tracked by our bounds analysis algorithm. -data BoundLoc (r :: M.Type -> Type) (tp :: M.Type) where - -- | @RegLoc r@ denotes the register @r@. - RegLoc :: !(r tp) -> BoundLoc r tp - -- | @StackkOffLoc o repr@ denotes the bytes from address range - -- @[initSP + o .. initSP + o + memReprBytes repr)@. - -- - -- We should note that this makes no claim that those addresses - -- are valid. - StackOffLoc :: !(MemInt (RegAddrWidth r)) - -> !(MemRepr tp) - -> BoundLoc r tp - -instance TestEquality r => TestEquality (BoundLoc r) where - testEquality (RegLoc x) (RegLoc y) = testEquality x y - testEquality (StackOffLoc xi xr) (StackOffLoc yi yr) | xi == yi = - testEquality xr yr - testEquality _ _ = Nothing - -instance HasRepr r TypeRepr => HasRepr (BoundLoc r) TypeRepr where - typeRepr (RegLoc r) = typeRepr r - typeRepr (StackOffLoc _ r) = typeRepr r - -instance OrdF r => OrdF (BoundLoc r) where - compareF (RegLoc x) (RegLoc y) = compareF x y - compareF (RegLoc _) _ = LTF - compareF _ (RegLoc _) = GTF - - compareF (StackOffLoc xi xr) (StackOffLoc yi yr) = - case compare xi yi of - LT -> LTF - GT -> GTF - EQ -> compareF xr yr - -instance ShowF r => Pretty (BoundLoc r tp) where - pretty (RegLoc r) = text (showF r) - pretty (StackOffLoc i tp) = - text "*(stack_frame " <+> ppAddend i <> text ") :" <> pretty tp - -instance ShowF r => PrettyF (BoundLoc r) where - prettyF = pretty - ------------------------------------------------------------------------- --- LocConstraint - --- | A constraint on a @BoundLoc -data LocConstraint r tp where - -- | An equivalence class representative with the given number of - -- elements. - -- - -- In our map the number of equivalence class members should always - -- be positive. - ValueRep :: !(ClassPred (RegAddrWidth r) tp) - -> LocConstraint r tp - EqualValue :: !(BoundLoc r tp) - -> LocConstraint r tp - -unconstrained :: LocConstraint r tp -unconstrained = ValueRep TopPred - -ppLocConstraint :: ShowF r => Doc -> LocConstraint r tp -> Doc -ppLocConstraint d (ValueRep p) = ppClassPred d p -ppLocConstraint d (EqualValue v) = d <+> text "=" <+> pretty v - ------------------------------------------------------------------------- --- MemVal - --- | A value with a particular type along with a MemRepr indicating --- how the type is encoded in memory. -data MemVal (p :: M.Type -> Type) = - forall (tp :: M.Type) . MemVal !(MemRepr tp) !(p tp) - -instance FunctorF MemVal where - fmapF f (MemVal r x) = MemVal r (f x) - -ppStackOff :: MemInt w -> MemRepr tp -> Doc -ppStackOff o repr = - text "*(stack_frame" <+> ppAddend o <> text "," <+> pretty repr <> text ")" - ------------------------------------------------------------------------- --- StackMap - --- | This is a data structure for representing values written to --- concrete stack offsets. -newtype StackMap w (v :: M.Type -> Type) = SM (Map (MemInt w) (MemVal v)) - -instance FunctorF (StackMap w) where - fmapF f (SM m) = SM (fmap (fmapF f) m) - --- | Empty stack map -emptyStackMap :: StackMap w p -emptyStackMap = SM Map.empty - --- | Pretty print a stack map given a term -ppStackMap :: (forall tp . Doc -> v tp -> Doc) -> StackMap w v -> Doc -ppStackMap f (SM m) - | Map.null m = text "empty-stack-map" - | otherwise = - vcat $ - [ f (ppStackOff o repr) v - | (o,MemVal repr v) <- Map.toList m - ] - -instance PrettyF v => Pretty (StackMap w v) where - pretty = ppStackMap (\nm d -> nm <+> text ":=" <+> prettyF d) - --- | Result returned by @stackMapLookup@. -data StackMapLookup w p tp where - -- 1| We found a value at the exact offset and repr - SMLResult :: !(p tp) -> StackMapLookup w p tp - -- | We found a value that had an overlapping offset and repr. - SMLOverlap :: !(MemInt w) - -> !(MemRepr utp) - -> !(p utp) - -> StackMapLookup w p tp - -- | We found neither an exact match nor an overlapping write. - SMLNone :: StackMapLookup w p tp - --- | Lookup value (if any) at given offset and representation. -stackMapLookup :: MemWidth w - => MemInt w - -> MemRepr tp - -> StackMap w p - -> StackMapLookup w p tp -stackMapLookup off repr (SM m) = do - let end = off + fromIntegral (memReprBytes repr) - if end < off then - error $ "stackMapLookup given bad offset." - else - case Map.lookupLT end m of - Just (oldOff, MemVal oldRepr val) - -- If match exact - | oldOff == off - , Just Refl <- testEquality oldRepr repr -> - SMLResult val - -- If previous write ends after this write starts - | oldOff + fromIntegral (memReprBytes oldRepr) > off -> - SMLOverlap oldOff oldRepr val - | otherwise -> - SMLNone - Nothing -> SMLNone - -clearPreWrites :: Ord i => i -> i -> Map i v -> Map i v -clearPreWrites l h m = - case Map.lookupLT h m of - Just (o,_v) | o >= l -> clearPreWrites l h (Map.delete o m) - _ -> m - -clearPostWrites :: Ord i => i -> i -> Map i v -> Map i v -clearPostWrites l h m = - case Map.lookupGE l m of - Just (o,_v) | o < h -> clearPostWrites l h (Map.delete o m) - _ -> m - --- | This updates the stack map with a write if this write is either --- unreserved or completely replaces an existing write. -stackMapReplace :: forall w p tp - . (MemWidth w, HasCallStack) - => MemInt w - -> MemRepr tp - -> p tp - -> StackMap w p - -> Either (MemInt w, Pair MemRepr p) (StackMap w p) -stackMapReplace off repr val (SM m) = do - let end = off + fromIntegral (memReprBytes repr) - -- If overflow occured in address then raise error. - when (end < off) $ error "Invalid stack offset" - - case Map.lookupLE end m of - Nothing -> pure () - Just (oldOff, MemVal oldRepr oldVal) - -- Previous write ends before this write. - | oldOff + fromIntegral (memReprBytes oldRepr) <= off -> - pure () - -- This write replaces a previous write - | oldOff == off, memReprBytes oldRepr == memReprBytes repr -> - pure () - -- This write overlaps without completely replacing - | otherwise -> - Left (oldOff, Pair oldRepr oldVal) - -- Update map - pure $! SM (Map.insert off (MemVal repr val) m) - --- | This assigns a region of bytes to a particular value in the stack. --- --- It overwrites any values that overlap with the location. -stackMapOverwrite :: forall w p tp - . MemWidth w - => MemInt w -- ^ Offset in the stack to write to - -> MemRepr tp -- ^ Type of value to write - -> p tp -- ^ Value to write - -> StackMap w p - -> StackMap w p -stackMapOverwrite off repr v (SM m) = - let e = off + fromIntegral (memReprBytes repr) - in SM $ Map.insert off (MemVal repr v) - $ clearPreWrites off e - $ clearPostWrites off e m - --- | This sets the value at an offset without checking to clear any --- previous writes to values. -unsafeStackMapInsert :: MemInt w -> MemRepr tp -> p tp -> StackMap w p -> StackMap w p -unsafeStackMapInsert o repr v (SM m) = SM (Map.insert o (MemVal repr v) m) - -stackMapFoldrWithKey :: (forall tp . MemInt w -> MemRepr tp -> v tp -> r -> r) - -> r - -> StackMap w v - -> r -stackMapFoldrWithKey f z (SM m) = - Map.foldrWithKey (\k (MemVal repr v) r -> f k repr v r) z m - -stackMapTraverseWithKey_ :: Applicative m - => (forall tp . MemInt w -> MemRepr tp -> v tp -> m ()) - -> StackMap w v - -> m () -stackMapTraverseWithKey_ f (SM m) = - Map.foldrWithKey (\k (MemVal repr v) r -> f k repr v *> r) (pure ()) m - -stackMapMapWithKey :: (forall tp . MemInt w -> MemRepr tp -> a tp -> b tp) - -> StackMap w a - -> StackMap w b -stackMapMapWithKey f (SM m) = - SM (Map.mapWithKey (\o (MemVal repr v) -> MemVal repr (f o repr v)) m) - -stackMapTraverseMaybeWithKey :: Applicative m - => (forall tp . MemInt w -> MemRepr tp -> a tp -> m (Maybe (b tp))) - -- ^ Traversal function - -> StackMap w a - -> m (StackMap w b) -stackMapTraverseMaybeWithKey f (SM m) = - SM <$> Map.traverseMaybeWithKey (\o (MemVal repr v) -> fmap (MemVal repr) <$> f o repr v) m - --- @stackMapDropAbove bnd m@ includes only entries in @m@ whose bytes do not go above @bnd@. -stackMapDropAbove :: MemWidth w => Integer -> StackMap w p -> StackMap w p -stackMapDropAbove bnd (SM m) = SM (Map.filterWithKey p m) - where p o (MemVal r _) = toInteger o + toInteger (memReprBytes r) <= bnd - --- @stackMapDropBelow bnd m@ includes only entries in @m@ whose bytes do not go below @bnd@. -stackMapDropBelow :: MemWidth w => Integer -> StackMap w p -> StackMap w p -stackMapDropBelow bnd (SM m) = SM (Map.filterWithKey p m) - where p o _ = toInteger o >= bnd - ------------------------------------------------------------------------- --- LocMap - --- | A map from register/concrete stack offsets to values -data LocMap (r :: M.Type -> Type) (v :: M.Type -> Type) - = LocMap { locMapRegs :: !(MapF r v) - , locMapStack :: !(StackMap (RegAddrWidth r) v) - } - --- | An empty location map. -locMapEmpty :: LocMap r v -locMapEmpty = LocMap { locMapRegs = MapF.empty, locMapStack = emptyStackMap } - --- | Return value associated with location or nothing if it is not --- defined. -locLookup :: (MemWidth (RegAddrWidth r), OrdF r) - => BoundLoc r tp - -> LocMap r v - -> Maybe (v tp) -locLookup (RegLoc r) m = MapF.lookup r (locMapRegs m) -locLookup (StackOffLoc o repr) m = - case stackMapLookup o repr (locMapStack m) of - SMLResult r -> Just r - SMLOverlap _ _ _ -> Nothing - SMLNone -> Nothing - --- | This associates the location with a value in the map, replacing any existing binding. --- --- It is prefixed with "nonOverlap" because it doesn't guarantee that stack --- values are non-overlapping -- the user should ensure this before calling this. -nonOverlapLocInsert :: OrdF r => BoundLoc r tp -> v tp -> LocMap r v -> LocMap r v -nonOverlapLocInsert (RegLoc r) v m = - m { locMapRegs = MapF.insert r v (locMapRegs m) } -nonOverlapLocInsert (StackOffLoc off repr) v m = - m { locMapStack = unsafeStackMapInsert off repr v (locMapStack m) } - -locOverwriteWith :: (OrdF r, MemWidth (RegAddrWidth r)) - => (v tp -> v tp -> v tp) -- ^ Update takes new and old. - -> BoundLoc r tp - -> v tp - -> LocMap r v - -> LocMap r v -locOverwriteWith upd (RegLoc r) v m = - m { locMapRegs = MapF.insertWith upd r v (locMapRegs m) } -locOverwriteWith upd (StackOffLoc o repr) v m = - let nv = case stackMapLookup o repr (locMapStack m) of - SMLNone -> v - SMLOverlap _ _ _ -> v - SMLResult oldv -> upd v oldv - in m { locMapStack = stackMapOverwrite o repr nv (locMapStack m) } + NoRangePred :: MaybeRangePred tp ------------------------------------------------------------------------ -- InitJumpBounds + +-- | Constraints on start of block +type BlockStartRangePred arch = LocMap (ArchReg arch) JustRangePred + -- | Bounds for a function as the start of a block. -newtype InitJumpBounds arch - = InitJumpBounds { initBndsMap :: LocMap (ArchReg arch) (LocConstraint (ArchReg arch)) +data InitJumpBounds arch + = InitJumpBounds { initBndsMap :: !(BlockStartStackConstraints arch) + , initRngPredMap :: !(BlockStartRangePred arch) } -- | Pretty print jump bounds. -ppInitJumpBounds :: forall arch - . ShowF (ArchReg arch) => InitJumpBounds arch -> [Doc] -ppInitJumpBounds (InitJumpBounds m) - = flip (MapF.foldrWithKey (\k v -> (ppLocConstraint (text (showF k)) v:))) - (locMapRegs m) - $ stackMapFoldrWithKey (\i repr v -> (ppLocConstraint (ppStackOff i repr) v:)) - [] - (locMapStack m) +ppInitJumpBounds :: forall arch . ShowF (ArchReg arch) => InitJumpBounds arch -> [Doc] +ppInitJumpBounds bnds + = ppBlockStartStackConstraints (initBndsMap bnds) + ++ ppLocMap ppJustRangePred (initRngPredMap bnds) instance ShowF (ArchReg arch) => Pretty (InitJumpBounds arch) where pretty = vcat . ppInitJumpBounds @@ -526,107 +135,9 @@ instance ShowF (ArchReg arch) => Show (InitJumpBounds arch) where -- | Bounds at start of function. functionStartBounds :: RegisterInfo (ArchReg arch) => InitJumpBounds arch functionStartBounds = - let m = LocMap { locMapRegs = MapF.singleton sp_reg (ValueRep (IsStackOffset 0)) - , locMapStack = emptyStackMap + InitJumpBounds { initBndsMap = fnEntryBlockStartStackConstraints + , initRngPredMap = locMapEmpty } - in InitJumpBounds m - --- | Return the representative and predicate associated with the location in the map. -locConstraint :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) - => InitJumpBounds arch - -> BoundLoc (ArchReg arch) tp - -> LocConstraint (ArchReg arch) tp -locConstraint (InitJumpBounds m) l = fromMaybe unconstrained (locLookup l m) - --- | @boundsLocationInfo bnds loc@ returns a triple containing the --- class representative, predicate, and class size associated the --- location. -boundsLocationInfo :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) - => InitJumpBounds arch - -> BoundLoc (ArchReg arch) tp - -> ( BoundLoc (ArchReg arch) tp - , ClassPred (ArchAddrWidth arch) tp - ) -boundsLocationInfo bnds l = - case locConstraint bnds l of - EqualValue loc -> boundsLocationInfo bnds loc - ValueRep p -> (l, p) - --- | @boundsLocRep bnds loc@ returns the representative location for --- @loc@. --- --- This representative location has the property that a location must --- have the same value as its representative location, and if two --- locations have provably equal values in the bounds, then they must --- have the same representative. -boundsLocationRep :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) - => InitJumpBounds arch - -> BoundLoc (ArchReg arch) tp - -> BoundLoc (ArchReg arch) tp -boundsLocationRep bnds l = - case boundsLocationInfo bnds l of - (r,_) -> r - --- | The the location to have the given constraint in the bounds, and --- return the new bounds. -setLocConstraint :: OrdF (ArchReg arch) - => BoundLoc (ArchReg arch) tp - -> LocConstraint (ArchReg arch) tp - -> InitJumpBounds arch - -> InitJumpBounds arch -setLocConstraint l c (InitJumpBounds m) = - InitJumpBounds (nonOverlapLocInsert l c m) - --- | Join locations -joinNewLoc :: forall s arch tp - . (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) - => InitJumpBounds arch - -> InitJumpBounds arch - -> STRef s (InitJumpBounds arch) - -- ^ The current index bounds. - -> STRef s (MapF (KeyPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))) - -- ^ The map from (oldClassRep, newClassRep) pairs to the - -- result class rep. - -> STRef s Int - -- ^ Stores the number of equivalence classes we have seen in - -- in the old class - -- Used so determining if any classes are changed. - -> BoundLoc (ArchReg arch) tp - -- ^ Location in join that we have not yet visited. - -> LocConstraint (ArchReg arch) tp - -- ^ Constraint on location in original list. - -> Changed s () -joinNewLoc old new bndsRef procRef cntr thisLoc oldCns = do - (oldRep, oldPred) <- lift $ - case oldCns of - ValueRep p -> do - -- Increment number of equivalence classes when we see an old - -- representative. - modifySTRef' cntr (+1) - -- Return this loc - pure (thisLoc, p) - EqualValue oldLoc -> - pure (boundsLocationInfo old oldLoc) - let (newRep, newPred) = boundsLocationInfo new thisLoc - m <- lift $ readSTRef procRef - -- See if we have already added a representative for this class. - let pair = KeyPair oldRep newRep - case MapF.lookup pair m of - Nothing -> do - p <- joinClassPred oldPred newPred - lift $ do - writeSTRef procRef $! MapF.insert pair thisLoc m - case p of - TopPred -> pure () - _ -> modifySTRef' bndsRef $ setLocConstraint thisLoc (ValueRep p) - Just resRep -> - -- Assert r is equal to resRep - lift $ modifySTRef' bndsRef $ - setLocConstraint thisLoc (EqualValue resRep) - --- | Bounds where there are no constraints. -emptyInitialBounds :: InitJumpBounds arch -emptyInitialBounds = InitJumpBounds locMapEmpty -- | Return a jump bounds that implies both input bounds, or `Nothing` -- if every fact inx the old bounds is implied by the new bounds. @@ -636,269 +147,58 @@ joinInitialBounds :: forall arch -> InitJumpBounds arch -> Maybe (InitJumpBounds arch) joinInitialBounds old new = runChanged $ do - -- Reference to new bounds. - bndsRef <- lift $ newSTRef emptyInitialBounds - -- This maps pairs containing the class representative in the old - -- and new maps to the associated class representative in the - -- combined bounds. - procRef <- lift $ newSTRef MapF.empty - cntr <- lift $ newSTRef 0 - -- - MapF.traverseWithKey_ - (\r -> joinNewLoc old new bndsRef procRef cntr (RegLoc r)) - (locMapRegs (initBndsMap old)) - stackMapTraverseWithKey_ - (\i r c -> joinNewLoc old new bndsRef procRef cntr (StackOffLoc i r) c) - (locMapStack (initBndsMap old)) - - -- Check number of equivalence classes in result and original - -- The count should not have decreased, but may increase if two elements - -- are no longer equal, and we need to check this. - origClassCount <- lift $ readSTRef cntr - resultClassCount <- lift $ MapF.size <$> readSTRef procRef - unless (origClassCount <= resultClassCount) $ do - error "Original class count should be bound by resultClassCount" - -- Record changed if any classes are different. - markChanged (origClassCount < resultClassCount) - - lift $ readSTRef bndsRef - ------------------------------------------------------------------------- --- BoundExpr - --- | This is an expression that represents the value of stack --- locations and assignments during steping through the block. --- --- The main diference between this and --- the `Value` type, index expressions do not depend on values read --- and written to memory during execution of the block, and are purely --- functions of the input --- --- This is different from `ClassPred` in that @ClassPred@ is a property --- assigned to equivalence classes -data BoundExpr arch ids tp where - -- | This refers to the contents of the location at the start - -- of block execution. - -- - -- The location should be a class representative in the initial bounds. - ClassRepExpr :: !(BoundLoc (ArchReg arch) tp) -> BoundExpr arch ids tp - -- | An assignment that is not interpreted, and just treated as a constant. - UninterpAssignExpr :: !(AssignId ids tp) - -> !(TypeRepr tp) - -> BoundExpr arch ids tp - -- | Denotes the value of the stack pointer at function start plus some constant. - StackOffsetExpr :: !(MemInt (ArchAddrWidth arch)) - -> BoundExpr arch ids (BVType (ArchAddrWidth arch)) - -- | Denotes a constant - CExpr :: !(CValue arch tp) -> BoundExpr arch ids tp - - -- | This is a pure function applied to other index expressions that - -- may be worth interpreting (but could be treated as an uninterp - -- assign expr also. - AppExpr :: !(AssignId ids tp) - -> !(App (BoundExpr arch ids) tp) - -> BoundExpr arch ids tp - -instance TestEquality (ArchReg arch) => TestEquality (BoundExpr arch ids) where - testEquality (ClassRepExpr x) (ClassRepExpr y) = - testEquality x y - testEquality (UninterpAssignExpr x _) (UninterpAssignExpr y _) = - testEquality x y - testEquality (StackOffsetExpr x) (StackOffsetExpr y) = - if x == y then - Just Refl - else - Nothing - testEquality (CExpr x) (CExpr y) = - testEquality x y - testEquality (AppExpr xn _xa) (AppExpr yn _ya) = - testEquality xn yn - testEquality _ _ = Nothing - -instance OrdF (ArchReg arch) => OrdF (BoundExpr arch ids) where - compareF (ClassRepExpr x) (ClassRepExpr y) = compareF x y - compareF ClassRepExpr{} _ = LTF - compareF _ ClassRepExpr{} = GTF - - compareF (UninterpAssignExpr x _) (UninterpAssignExpr y _) = compareF x y - compareF UninterpAssignExpr{} _ = LTF - compareF _ UninterpAssignExpr{} = GTF - - compareF (StackOffsetExpr x) (StackOffsetExpr y) = fromOrdering (compare x y) - compareF StackOffsetExpr{} _ = LTF - compareF _ StackOffsetExpr{} = GTF - - compareF (CExpr x) (CExpr y) = compareF x y - compareF CExpr{} _ = LTF - compareF _ CExpr{} = GTF - - compareF (AppExpr xn _xa) (AppExpr yn _ya) = compareF xn yn - -instance ( HasRepr (ArchReg arch) TypeRepr - , MemWidth (ArchAddrWidth arch) - ) => HasRepr (BoundExpr arch ids) TypeRepr where - typeRepr e = - case e of - ClassRepExpr x -> typeRepr x - UninterpAssignExpr _ tp -> tp - StackOffsetExpr _ -> addrTypeRepr - CExpr x -> typeRepr x - AppExpr _ a -> typeRepr a - -instance ShowF (ArchReg arch) => Pretty (BoundExpr arch id tp) where - pretty e = - case e of - ClassRepExpr l -> pretty l - UninterpAssignExpr n _ -> parens (text "uninterp" <+> ppAssignId n) - StackOffsetExpr o -> parens (text "+ stack_off" <+> pretty o) - CExpr v -> pretty v - AppExpr n _ -> parens (text "app" <+> ppAssignId n) - -instance ShowF (ArchReg arch) => PrettyF (BoundExpr arch id) where - prettyF = pretty + (finalStkCns, _) <- joinBlockStartStackConstraints (initBndsMap old) (initBndsMap new) + pure $! InitJumpBounds { initBndsMap = finalStkCns + , initRngPredMap = locMapEmpty + } ------------------------------------------------------------------------ -- IntraJumpBounds -- | Information about bounds for a particular value within a block. data IntraJumpBounds arch ids - = IntraJumpBounds { initBounds :: !(LocMap (ArchReg arch) (LocConstraint (ArchReg arch))) - -- ^ Bounds at execution start. - -- - -- This may have been refined by branch predicates. - , stackExprMap :: !(StackMap (ArchAddrWidth arch) (BoundExpr arch ids)) - -- ^ Maps stack offsets to the expression associated with them. - , assignExprMap :: !(MapF (AssignId ids) (BoundExpr arch ids)) - -- ^ Maps processed assignments to index expressions. - , memoTable :: !(MapF (App (BoundExpr arch ids)) (BoundExpr arch ids)) - -- ^ Table for ensuring each bound expression - -- has a single representative. + = IntraJumpBounds { intraStackConstraints :: !(BlockIntraStackConstraints arch ids) + , intraRangePredMap :: !(BlockStartRangePred arch) } --- | Return an expression equivalent to the location in the constraint --- map. --- --- This attempts to normalize the expression to get a representative. -locExpr :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) - => LocMap (ArchReg arch) (LocConstraint (ArchReg arch)) - -> BoundLoc (ArchReg arch) tp - -> BoundExpr arch ids tp -locExpr m loc = - case locLookup loc m of - Nothing -> ClassRepExpr loc - Just (EqualValue loc') -> locExpr m loc' - Just (ValueRep p) -> - case p of - IsStackOffset i -> StackOffsetExpr i - BoundedBV _ -> ClassRepExpr loc - TopPred -> ClassRepExpr loc -- | Create index bounds from initial index bounds. mkIntraJumpBounds :: forall arch ids . (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) => InitJumpBounds arch -> IntraJumpBounds arch ids -mkIntraJumpBounds (InitJumpBounds initBnds) = do - let -- Map stack offset and memory annotation pair to the - -- representative in the initial bounds. - stackExpr :: MemInt (ArchAddrWidth arch) - -> MemRepr tp - -> LocConstraint (ArchReg arch) tp - -> BoundExpr arch ids tp - stackExpr i tp _ = locExpr initBnds (StackOffLoc i tp) - in IntraJumpBounds { initBounds = initBnds - , stackExprMap = stackMapMapWithKey stackExpr (locMapStack initBnds) - , assignExprMap = MapF.empty - , memoTable = MapF.empty - } +mkIntraJumpBounds bnds = + IntraJumpBounds { intraStackConstraints = mkBlockIntraStackConstraints (initBndsMap bnds) + , intraRangePredMap = initRngPredMap bnds + } --- | Return the value of the index expression given the bounds. -valueExpr :: forall arch ids tp - . (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) - => IntraJumpBounds arch ids - -> Value arch ids tp - -> BoundExpr arch ids tp -valueExpr bnds val = - case val of - CValue c -> CExpr c - AssignedValue (Assignment aid _) -> - case MapF.lookup aid (assignExprMap bnds) of - Just e -> e - Nothing -> error $ "valueExpr internal: Expected value to be assigned." - Initial r -> locExpr (initBounds bnds) (RegLoc r) +initJumpBounds :: IntraJumpBounds arch ids -> InitJumpBounds arch +initJumpBounds bnds = + InitJumpBounds { initBndsMap = biscInitConstraints (intraStackConstraints bnds) + , initRngPredMap = intraRangePredMap bnds + } --- | Return stack offset if value is a stack offset. -stackOffset :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) - => IntraJumpBounds arch ids - -> Value arch ids (BVType (ArchAddrWidth arch)) - -> Maybe (MemInt (ArchAddrWidth arch)) -stackOffset bnds val = - case valueExpr bnds val of - StackOffsetExpr i -> Just i - _ -> Nothing +instance ShowF (ArchReg arch) => Pretty (IntraJumpBounds arch ids) where + pretty = pretty . initJumpBounds --- | Update the stack to point to the given expression. -writeStackOff :: forall arch ids tp - . (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) - => IntraJumpBounds arch ids - -> MemInt (ArchAddrWidth arch) - -> MemRepr tp - -> Value arch ids tp - -> IntraJumpBounds arch ids -writeStackOff bnds off repr v = - bnds { stackExprMap = stackMapOverwrite off repr (valueExpr bnds v) (stackExprMap bnds) } --- | Return an index expression associated with the @AssignRhs@. -rhsExpr :: forall arch ids tp - . ( MemWidth (ArchAddrWidth arch) - , OrdF (ArchReg arch) - , ShowF (ArchReg arch) - ) - => IntraJumpBounds arch ids - -> AssignId ids tp - -> AssignRhs arch (Value arch ids) tp - -> BoundExpr arch ids tp -rhsExpr bnds aid arhs = - case arhs of - EvalApp app -> do - let stackFn v = toInteger <$> stackOffset bnds v - case appAsStackOffset stackFn app of - Just (StackOffsetView o) -> do - StackOffsetExpr $ fromInteger o - _ -> do - let a = fmapFC (valueExpr bnds) app - case MapF.lookup a (memoTable bnds) of - Just r -> r - Nothing -> AppExpr aid a - ReadMem addr repr - | Just o <- stackOffset bnds addr - , SMLResult e <- stackMapLookup o repr (stackExprMap bnds) -> - e - _ -> UninterpAssignExpr aid (typeRepr arhs) +modifyIntraStackConstraints :: (BlockIntraStackConstraints arch ids -> BlockIntraStackConstraints arch ids) + -> IntraJumpBounds arch ids + -> IntraJumpBounds arch ids +modifyIntraStackConstraints f bnds = bnds { intraStackConstraints = f (intraStackConstraints bnds) } --- | Associate the given bound expression with the assignment. -bindAssignment :: IntraJumpBounds arch ids - -> AssignId ids tp - -> BoundExpr arch ids tp - -> IntraJumpBounds arch ids -bindAssignment bnds aid expr = - bnds { assignExprMap = MapF.insert aid expr (assignExprMap bnds) } - --- | Discard information about the stack in the bounds due to an --- operation that may affect the stack. -discardStackInfo :: IntraJumpBounds arch ids - -> IntraJumpBounds arch ids -discardStackInfo bnds = bnds { stackExprMap = emptyStackMap } +------------------------------------------------------------------------ +-- Execute a statement -- | Given a statement this modifies the bounds based on the statement. -execStatement :: ( MemWidth (ArchAddrWidth arch) - , OrdF (ArchReg arch) - , ShowF (ArchReg arch) - ) - => IntraJumpBounds arch ids - -> Stmt arch ids - -> IntraJumpBounds arch ids -execStatement bnds stmt = +stackExecStatement :: ( MemWidth (ArchAddrWidth arch) + , OrdF (ArchReg arch) + , ShowF (ArchReg arch) + ) + => BlockIntraStackConstraints arch ids + -> Stmt arch ids + -> BlockIntraStackConstraints arch ids +stackExecStatement bnds stmt = case stmt of AssignStmt (Assignment aid arhs) -> do -- Clear all knowledge about the stack on architecture-specific @@ -910,12 +210,13 @@ execStatement bnds stmt = EvalArchFn{} -> discardStackInfo bnds _ -> bnds -- Associate the given expression with a bounds. - seq bnds' $ bindAssignment bnds' aid (rhsExpr bnds' aid arhs) + seq bnds' $ bindAssignment aid (blockIntraRhsExpr bnds' aid arhs) bnds' WriteMem addr repr val -> - case stackOffset bnds addr of + case blockIntraValueStackOffset bnds addr of Just addrOff -> writeStackOff bnds addrOff repr val -- If we write to something other than stack, then clear all stack references. + -- Note. This seems like a bad idea. Nothing -> discardStackInfo bnds CondWriteMem{} -> @@ -929,41 +230,43 @@ execStatement bnds stmt = ArchState{} -> bnds -instance ShowF (ArchReg arch) => Pretty (IntraJumpBounds arch ids) where - pretty bnds = pretty (InitJumpBounds (initBounds bnds)) +-- | Update the bounds based on a statement. +execStatement :: ( MemWidth (ArchAddrWidth arch) + , OrdF (ArchReg arch) + , ShowF (ArchReg arch) + ) + => IntraJumpBounds arch ids + -> Stmt arch ids + -> IntraJumpBounds arch ids +execStatement bnds stmt = + modifyIntraStackConstraints (`stackExecStatement` stmt) bnds + ------------------------------------------------------------------------ -- Operations --- | Return predicate from constant. -cvaluePred :: CValue arch tp -> ClassPred (ArchAddrWidth arch) tp -cvaluePred v = - case v of - BoolCValue _ -> TopPred - BVCValue w i -> BoundedBV (mkRangeBound w (fromInteger i) (fromInteger i)) - RelocatableCValue{} -> TopPred - SymbolCValue{} -> TopPred - -- | This returns the current predicate on the bound expression. -exprPred :: ( MemWidth (ArchAddrWidth arch) - , HasRepr (ArchReg arch) TypeRepr - , OrdF (ArchReg arch) - , ShowF (ArchReg arch) - ) - => LocMap (ArchReg arch) (LocConstraint (ArchReg arch)) - -- ^ Constraints on stacks/registers - -> BranchConstraints (ArchReg arch) ids - -- ^ Bounds on assignments inferred from branch predicate. - -> BoundExpr arch ids tp - -> ClassPred (ArchAddrWidth arch) tp -exprPred lm brCns v = - case v of +exprRangePred :: ( MemWidth (ArchAddrWidth arch) + , HasRepr (ArchReg arch) TypeRepr + , OrdF (ArchReg arch) + , ShowF (ArchReg arch) + ) + => BlockStartStackConstraints arch + -> BlockStartRangePred arch + -- ^ Inferred range constraints + -> BranchConstraints (ArchReg arch) ids + -- ^ Bounds on assignments inferred from branch predicate. + -> StackExpr arch ids tp + -> MaybeRangePred tp +exprRangePred stkCns rpCns brCns e = + case e of ClassRepExpr loc -> case MapF.lookup loc (newClassRepConstraints brCns) of - Just (SubRange r) -> BoundedBV r + Just (SubRange r) -> SomeRangePred r Nothing -> - case boundsLocationInfo (InitJumpBounds lm) loc of - (_,p) -> p + case locLookup loc rpCns of + Nothing -> NoRangePred + Just (JustRangePred r) -> SomeRangePred r UninterpAssignExpr n _ -> do case MapF.lookup n (newUninterpAssignConstraints brCns) of Just (SubRange r) @@ -971,10 +274,11 @@ exprPred lm brCns v = , l <- rangeLowerBound r , u <- rangeUpperBound r , (0 < l) || (u < fromInteger (maxUnsigned w)) -> - BoundedBV r - _ -> TopPred - StackOffsetExpr x -> IsStackOffset x - CExpr c -> cvaluePred c + SomeRangePred r + _ -> NoRangePred + StackOffsetExpr _ -> NoRangePred + CExpr (BVCValue w i) -> SomeRangePred (mkRangeBound w (fromInteger i) (fromInteger i)) + CExpr _ -> NoRangePred AppExpr n _app -- If a bound has been deliberately asserted to this assignment -- then use that. @@ -983,79 +287,41 @@ exprPred lm brCns v = , l <- rangeLowerBound r , u <- rangeUpperBound r , (0 < l) || (u < fromInteger (maxUnsigned w)) -> - BoundedBV r + SomeRangePred r -- Otherwise see what we can infer. AppExpr _n app -> case app of UExt x w - | BoundedBV r <- exprPred lm brCns x -> + | SomeRangePred r <- exprRangePred stkCns rpCns brCns x -> -- If bound covers all the bits in x, then we can extend it to all -- the bits in result (since new bits are false) -- -- Otherwise, we only have the partial bound case testEquality (rangeWidth r) (typeWidth x) of Just Refl -> - BoundedBV (mkRangeBound w (rangeLowerBound r) (rangeUpperBound r)) + SomeRangePred (mkRangeBound w (rangeLowerBound r) (rangeUpperBound r)) Nothing -> -- Dynamic check on range width that should never fail. case testLeq (rangeWidth r) w of - Just LeqProof -> BoundedBV r - Nothing -> error "exprPred given malformed app." + Just LeqProof -> SomeRangePred r + Nothing -> error "exprRangePred given malformed app." BVAdd _ x (CExpr (BVCValue _ c)) - | BoundedBV r <- exprPred lm brCns x + | SomeRangePred r <- exprRangePred stkCns rpCns brCns x , w <- rangeWidth r , lr <- rangeLowerBound r + fromInteger (toUnsigned w c) , ur <- rangeUpperBound r + fromInteger (toUnsigned w c) , lr `shiftR` fromIntegral (natValue w) == ur `shiftR` fromIntegral (natValue w) , lr' <- fromInteger (toUnsigned w (toInteger lr)) , ur' <- fromInteger (toUnsigned w (toInteger ur)) -> - BoundedBV (RangePred w lr' ur') + SomeRangePred (RangePred w lr' ur') Trunc x w - | BoundedBV r <- exprPred lm brCns x + | SomeRangePred r <- exprRangePred stkCns rpCns brCns x -- Compare the range constraint with the output number of bits. -- If the bound on r covers at most the truncated number -- of bits, then we just pass it through. , Just LeqProof <- testLeq (rangeWidth r) w -> - BoundedBV r -{- - BVAnd _ x y -> - case (exprPred lm brCns x, exprPred lm brCns y) of - (BoundedBV (UBVUpperBound xw xb), BoundedBV (UBVUpperBound yw yb)) - | Just Refl <- testEquality xw yw -> - BoundedBV (UBVUpperBound xw (min xb yb)) - (TopPred, yb) -> yb - (xb, _) -> xb - SExt x w -> - case exprPred lm brCns x of - BoundedBV (UBVUpperBound u b) -> - case testLeq u w of - Just LeqProof -> BoundedBV (UBVUpperBound u b) - Nothing -> error "unsignedUpperBound given bad width" - _ -> TopPred --} - _ -> TopPred - --- | This attempts to resolve the predicate associated with a value. --- --- This does not make use of any branch constraints. -valuePred :: ( MapF.OrdF (ArchReg arch) - , MapF.ShowF (ArchReg arch) - , RegisterInfo (ArchReg arch) - ) - => IntraJumpBounds arch ids - -> Value arch ids tp - -> ClassPred (ArchAddrWidth arch) tp -valuePred bnds v = - case v of - CValue cv -> cvaluePred cv - AssignedValue a -> - case MapF.lookup (assignId a) (assignExprMap bnds) of - Just valExpr -> - exprPred (initBounds bnds) emptyBranchConstraints valExpr - Nothing -> TopPred - Initial r -> - case boundsLocationInfo (InitJumpBounds (initBounds bnds)) (RegLoc r) of - (_,p) -> p + SomeRangePred r + _ -> NoRangePred -- | This returns a natural number with a computed upper bound for the -- value or `Nothing` if no explicit bound was inferred. @@ -1066,12 +332,15 @@ unsignedUpperBound :: ( MapF.OrdF (ArchReg arch) => IntraJumpBounds arch ids -> Value arch ids tp -> Maybe Natural -unsignedUpperBound bnds v = - case valuePred bnds v of - BoundedBV r -> do +unsignedUpperBound bnds v = do + let stkCns = intraStackConstraints bnds + let ibnds = biscInitConstraints stkCns + let valExpr = blockIntraValueExpr stkCns v + case exprRangePred ibnds (intraRangePredMap bnds) emptyBranchConstraints valExpr of + SomeRangePred r -> do Refl <- testEquality (rangeWidth r) (typeWidth v) pure (rangeUpperBound r) - _ -> Nothing + NoRangePred -> Nothing ------------------------------------------------------------------------ -- SubRange @@ -1209,7 +478,7 @@ addRangePred :: ( MapF.OrdF (ArchReg arch) , u <= w , MemWidth (ArchAddrWidth arch) ) - => BoundExpr arch ids (BVType w) + => StackExpr arch ids (BVType w) -- ^ Value we are adding bounds for. -> RangePred u @@ -1297,16 +566,18 @@ assertPred :: ( OrdF (ArchReg arch) assertPred bnds (AssignedValue a) isTrue = case assignRhs a of EvalApp (Eq x (BVValue w c)) -> do - addRangePred (valueExpr bnds x) (mkRangeBound w (fromInteger c) (fromInteger c)) + addRangePred (blockIntraValueExpr (intraStackConstraints bnds) x) (mkRangeBound w (fromInteger c) (fromInteger c)) EvalApp (Eq (BVValue w c) x) -> do - addRangePred (valueExpr bnds x) (mkRangeBound w (fromInteger c) (fromInteger c)) + addRangePred (blockIntraValueExpr (intraStackConstraints bnds) x) (mkRangeBound w (fromInteger c) (fromInteger c)) -- Given x < c), assert x <= c-1 EvalApp (BVUnsignedLt x (BVValue _ c)) -> do if isTrue then do when (c == 0) $ Left "x < 0 must be false." - addRangePred (valueExpr bnds x) $! mkUpperBound (typeWidth x) (fromInteger (c-1)) + addRangePred (blockIntraValueExpr (intraStackConstraints bnds) x) $! + mkUpperBound (typeWidth x) (fromInteger (c-1)) else do - addRangePred (valueExpr bnds x) $! mkLowerBound (typeWidth x) (fromInteger c) + addRangePred (blockIntraValueExpr (intraStackConstraints bnds) x) $! + mkLowerBound (typeWidth x) (fromInteger c) -- Given not (c < y), assert y <= c EvalApp (BVUnsignedLt (BVValue w c) y) -> do p <- @@ -1315,7 +586,7 @@ assertPred bnds (AssignedValue a) isTrue = pure $! mkLowerBound w (fromInteger (c+1)) else do pure $! mkUpperBound w (fromInteger c) - addRangePred (valueExpr bnds y) p + addRangePred (blockIntraValueExpr (intraStackConstraints bnds) y) p -- Given x <= c, assert x <= c EvalApp (BVUnsignedLe x (BVValue w c)) -> do p <- @@ -1324,14 +595,16 @@ assertPred bnds (AssignedValue a) isTrue = else do when (c >= maxUnsigned w) $ Left "x <= max_unsigned must be true" pure $! mkLowerBound w (fromInteger (c+1)) - addRangePred (valueExpr bnds x) p + addRangePred (blockIntraValueExpr (intraStackConstraints bnds) x) p -- Given not (c <= y), assert y <= (c-1) EvalApp (BVUnsignedLe (BVValue _ c) y) | isTrue -> do - addRangePred (valueExpr bnds y) (mkLowerBound (typeWidth y) (fromInteger c)) + addRangePred (blockIntraValueExpr (intraStackConstraints bnds) y) (mkLowerBound (typeWidth y) (fromInteger c)) | otherwise -> do when (c == 0) $ Left "0 <= x cannot be false" - addRangePred (valueExpr bnds y) (mkUpperBound (typeWidth y) (fromInteger (c-1))) + addRangePred + (blockIntraValueExpr (intraStackConstraints bnds) y) + (mkUpperBound (typeWidth y) (fromInteger (c-1))) EvalApp (AndApp l r) -> if isTrue then conjoinBranchConstraints @@ -1359,75 +632,27 @@ assertPred bnds (AssignedValue a) isTrue = assertPred _ _ _ = Right emptyBranchConstraints --- | Maps bound expression that have been visited to their location. --- --- We memoize expressions seen so that we can infer when two locations --- must be equal. -type NextBlockState arch ids = MapF (BoundExpr arch ids) (BoundLoc (ArchReg arch) ) --- | Return the constraint associated with the given location and expression --- or nothing if the constraint is the top one and should be stored. -nextStateLocConstraint :: ( MemWidth (ArchAddrWidth arch) - , HasRepr (ArchReg arch) TypeRepr - , OrdF (ArchReg arch) - , ShowF (ArchReg arch) - ) - => LocMap (ArchReg arch) (LocConstraint (ArchReg arch)) - -- ^ Constraints on stacks/registers - -> BranchConstraints (ArchReg arch) ids - -- ^ Bounds on assignments inferred from branch - -- predicate. - -> BoundLoc (ArchReg arch) tp - -- ^ Location expression is stored at. - -> BoundExpr arch ids tp - -- ^ Expression to infer predicate or. - -> State (NextBlockState arch ids) - (Maybe (LocConstraint (ArchReg arch) tp)) -nextStateLocConstraint lm brCns loc e = do - m <- get - case MapF.lookup e m of - Just l -> do - pure $! Just $ EqualValue l - Nothing -> do - put $! MapF.insert e loc m - case exprPred lm brCns e of - TopPred -> pure Nothing - p -> pure $! (Just $! ValueRep p) - -nextRegConstraint :: ( MemWidth (ArchAddrWidth arch) - , HasRepr (ArchReg arch) TypeRepr - , OrdF (ArchReg arch) - , ShowF (ArchReg arch) - ) - => IntraJumpBounds arch ids - -- ^ Bounds at end of this state. - -> BranchConstraints (ArchReg arch) ids - -- ^ Constraints inferred from branch (or `emptyBranchConstraints) - -> ArchReg arch tp - -> Value arch ids tp - -> State (NextBlockState arch ids) - (Maybe (LocConstraint (ArchReg arch) tp)) -nextRegConstraint bnds brCns r v = - nextStateLocConstraint (initBounds bnds) brCns (RegLoc r) (valueExpr bnds v) - -nextStackConstraint :: ( MemWidth (ArchAddrWidth arch) - , HasRepr (ArchReg arch) TypeRepr - , OrdF (ArchReg arch) - , ShowF (ArchReg arch) - ) - => IntraJumpBounds arch ids - -- ^ Bounds at end of this state. - -> BranchConstraints (ArchReg arch) ids - -- ^ Constraints inferred from branch (or `emptyBranchConstraints) - -> MemInt (ArchAddrWidth arch) - -> MemRepr tp - -> BoundExpr arch ids tp - -> State (NextBlockState arch ids) (Maybe (LocConstraint (ArchReg arch) tp)) -nextStackConstraint bnds brCns i repr e = - nextStateLocConstraint (initBounds bnds) brCns (StackOffLoc i repr) e +updateRangePredMap :: ( MemWidth (ArchAddrWidth arch) + , HasRepr (ArchReg arch) TypeRepr + , OrdF (ArchReg arch) + , ShowF (ArchReg arch) + ) + => BlockStartStackConstraints arch + -- ^ Constraints on stacks/registers + -> BranchConstraints (ArchReg arch) ids + -- ^ Bounds on assignments inferred from branch + -- predicate. + -> LocMap (ArchReg arch) JustRangePred + -> Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids) + -> LocMap (ArchReg arch) JustRangePred +updateRangePredMap stkCns brCns m (Pair l e) = do + case exprRangePred stkCns locMapEmpty brCns e of + SomeRangePred r -> nonOverlapLocInsert l (JustRangePred r) m + NoRangePred -> m -- | Bounds for block after jump -nextBlockBounds' :: forall arch ids +nextBlockBounds :: forall arch ids . RegisterInfo (ArchReg arch) => IntraJumpBounds arch ids -- ^ Bounds at end of this state. @@ -1436,88 +661,48 @@ nextBlockBounds' :: forall arch ids -> RegState (ArchReg arch) (Value arch ids) -- ^ Register values at start of next state. -> InitJumpBounds arch -nextBlockBounds' bnds brCns regs = do - flip evalState MapF.empty $ do - rm <- MapF.traverseMaybeWithKey (nextRegConstraint bnds brCns) (regStateMap regs) - sm <- stackMapTraverseMaybeWithKey (nextStackConstraint bnds brCns) (stackExprMap bnds) - let m = LocMap { locMapRegs = rm, locMapStack = sm } - pure $! InitJumpBounds m +nextBlockBounds bnds brCns regs = runNextStateMonad $ do + stkCns <- postJumpStackConstraints (intraStackConstraints bnds) regs + reps <- getNextStateRepresentatives + let icns = biscInitConstraints (intraStackConstraints bnds) + let rngMap = foldl' (updateRangePredMap icns brCns) locMapEmpty reps + pure $! InitJumpBounds { initBndsMap = stkCns + , initRngPredMap = rngMap + } -- | Bounds for block after jump -nextBlockBounds :: forall arch ids +postJumpBounds :: forall arch ids . RegisterInfo (ArchReg arch) => IntraJumpBounds arch ids -- ^ Bounds at end of this state. -> RegState (ArchReg arch) (Value arch ids) -- ^ Register values at start of next state. -> InitJumpBounds arch -nextBlockBounds bnds regs = nextBlockBounds' bnds emptyBranchConstraints regs +postJumpBounds bnds regs = nextBlockBounds bnds emptyBranchConstraints regs -- | Get bounds for start of block after a branch (either the true or -- false branch) -postBranchBounds - :: RegisterInfo (ArchReg arch) - => IntraJumpBounds arch ids -- ^ Bounds just before jump - -> Value arch ids BoolType -- ^ Branch condition - -> Bool -- ^ Flag indicating if branch predicate is true or false. - -> RegState (ArchReg arch) (Value arch ids) - -- ^ Register values at start of next state. - -> Either String (InitJumpBounds arch) +postBranchBounds :: RegisterInfo (ArchReg arch) + => IntraJumpBounds arch ids -- ^ Bounds just before jump + -> Value arch ids BoolType -- ^ Branch condition + -> Bool -- ^ Flag indicating if branch predicate is true or false. + -> RegState (ArchReg arch) (Value arch ids) + -- ^ Register values at start of next state. + -> Either String (InitJumpBounds arch) postBranchBounds bnds c condIsTrue regs = do brCns <- assertPred bnds c condIsTrue - pure (nextBlockBounds' bnds brCns regs) + pure (nextBlockBounds bnds brCns regs) --- | Get the constraint associated with a register after a call. -postCallConstraint :: RegisterInfo (ArchReg arch) - => CallParams (ArchReg arch) - -- ^ Information about calling convention. - -> IntraJumpBounds arch ids - -- ^ Bounds at end of this state. - -> ArchReg arch tp - -- ^ Register to get - -> Value arch ids tp - -- ^ Value of register at time call occurs. - -> State (NextBlockState arch ids) (Maybe (LocConstraint (ArchReg arch) tp)) -postCallConstraint params bnds r v - | Just Refl <- testEquality r sp_reg - , IsStackOffset o <- - exprPred (initBounds bnds) emptyBranchConstraints (valueExpr bnds v) = do - let postCallPred = IsStackOffset (o+fromInteger (postCallStackDelta params)) - pure (Just (ValueRep postCallPred)) - | preserveReg params r = - nextStateLocConstraint (initBounds bnds) emptyBranchConstraints (RegLoc r) (valueExpr bnds v) - | otherwise = - pure Nothing -- | Return the index bounds after a function call. postCallBounds :: forall arch ids - . ( RegisterInfo (ArchReg arch) - ) + . RegisterInfo (ArchReg arch) => CallParams (ArchReg arch) -> IntraJumpBounds arch ids -> RegState (ArchReg arch) (Value arch ids) -> InitJumpBounds arch -postCallBounds params bnds regs = do - flip evalState MapF.empty $ do - rm <- MapF.traverseMaybeWithKey (postCallConstraint params bnds) (regStateMap regs) - let finalStack = stackExprMap bnds - let filteredStack = - case valuePred bnds (getBoundValue sp_reg regs) of - IsStackOffset spOff - | stackGrowsDown params -> - let newOff = toInteger spOff + postCallStackDelta params - -- Keep entries at offsets above return address. - in stackMapDropBelow newOff finalStack - | otherwise -> - let newOff = toInteger spOff + postCallStackDelta params - -- Keep entries whose high address is below new stack offset - in stackMapDropAbove newOff finalStack - _ -> emptyStackMap - let nextStackFn :: MemInt (ArchAddrWidth arch) - -> MemRepr tp - -> BoundExpr arch ids tp - -> State (NextBlockState arch ids) (Maybe (LocConstraint (ArchReg arch) tp)) - nextStackFn = nextStackConstraint bnds emptyBranchConstraints - sm <- stackMapTraverseMaybeWithKey nextStackFn filteredStack - let newMap = LocMap { locMapRegs = rm, locMapStack = sm } - pure $! InitJumpBounds newMap +postCallBounds params bnds regs = + let cns = postCallStackConstraints params (intraStackConstraints bnds) regs + in InitJumpBounds { initBndsMap = cns + , initRngPredMap = locMapEmpty + } diff --git a/base/src/Data/Macaw/AbsDomain/StackAnalysis.hs b/base/src/Data/Macaw/AbsDomain/StackAnalysis.hs new file mode 100644 index 00000000..950ea7ed --- /dev/null +++ b/base/src/Data/Macaw/AbsDomain/StackAnalysis.hs @@ -0,0 +1,885 @@ +{- | + +This module defines a relational abstract domain for tracking +registers and stack addresses. The model records when one of these +values is known to be equal to the current pointer stack frame. This +domain also tracks equalities between nodes so that analysis +algorithms built on top of this are modulo known equivalences +between registers and stack locations. + +-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE UndecidableInstances #-} +module Data.Macaw.AbsDomain.StackAnalysis + ( -- * Block level datatypes + -- ** BlockStartStackConstraints + BlockStartStackConstraints + , StackEqConstraint(..) + , ppBlockStartStackConstraints + , fnEntryBlockStartStackConstraints + , ppStackEqConstraint + , blockStartLocExpr + , blockStartLocStackOffset + , StackOffConstraint + , blockStartLocRepAndCns + , BoundLoc(..) + , joinBlockStartStackConstraints + , JoinClassMap + , JoinClassPair(..) + -- ** BlockIntraStackConstraints + , BlockIntraStackConstraints + , mkBlockIntraStackConstraints + , biscInitConstraints + , blockIntraValueExpr + , blockIntraValueStackOffset + , StackExpr(..) + , blockIntraRhsExpr + , bindAssignment + , discardStackInfo + , writeStackOff + -- ** Block terminator updates + , postJumpStackConstraints + , postCallStackConstraints + -- * LocMap + , LocMap(..) + , locMapEmpty + , locLookup + , nonOverlapLocInsert + , locOverwriteWith + , ppLocMap + -- * StackMap + , StackMap + , emptyStackMap + , stackMapLookup + , StackMapLookup(..) + , stackMapOverwrite + , stackMapMapWithKey + , stackMapTraverseMaybeWithKey + , stackMapDropAbove + , stackMapDropBelow + -- * NextStateMonad + , NextStateMonad + , runNextStateMonad + , getNextStateRepresentatives + -- * Miscelaneous + ) where + +import Control.Monad.Reader +import Control.Monad.State +import Data.Functor +import Data.Kind +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Parameterized.Classes +import Data.Parameterized.Map (MapF) +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.Pair +import Data.Parameterized.TraversableF +import Data.Parameterized.TraversableFC +import Data.STRef +import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) + +import Data.Macaw.AbsDomain.CallParams +import Data.Macaw.CFG.App +import Data.Macaw.CFG.Core +import Data.Macaw.Memory +import qualified Data.Macaw.Types as M +import Data.Macaw.Types hiding (Type) +import Data.Macaw.Utils.Changed + +addrTypeRepr :: MemWidth w => TypeRepr (BVType w) +addrTypeRepr = BVTypeRepr memWidthNatRepr + +ppAddend :: MemInt w -> Doc +ppAddend o | memIntValue o < 0 = + text "-" <+> pretty (negate (toInteger (memIntValue o))) + | otherwise = text "+" <+> pretty o + +ppStackOff :: MemInt w -> MemRepr tp -> Doc +ppStackOff o repr = + text "*(stack_frame" <+> ppAddend o <> text "," <+> pretty repr <> text ")" + +------------------------------------------------------------------------ +-- JoinClassPair + +data JoinClassPair (key :: k -> Type) (tp :: k) = JoinClassPair !(key tp) !(key tp) + +instance TestEquality k => TestEquality (JoinClassPair k) where + testEquality (JoinClassPair x1 x2) (JoinClassPair y1 y2) = do + Refl <- testEquality x1 y1 + testEquality x2 y2 + +instance OrdF k => OrdF (JoinClassPair k) where + compareF (JoinClassPair x1 x2) (JoinClassPair y1 y2) = + joinOrderingF (compareF x1 y1) (compareF x2 y2) + +------------------------------------------------------------------------ +-- MemVal + +-- | A value with a particular type along with a MemRepr indicating +-- how the type is encoded in memory. +data MemVal (p :: M.Type -> Type) = + forall (tp :: M.Type) . MemVal !(MemRepr tp) !(p tp) + +instance FunctorF MemVal where + fmapF f (MemVal r x) = MemVal r (f x) + +------------------------------------------------------------------------ +-- BoundLoc + +-- | Either a register or stack offset. +-- +-- These locations are tracked by our bounds analysis algorithm. +data BoundLoc (r :: M.Type -> Type) (tp :: M.Type) where + -- | @RegLoc r@ denotes the register @r@. + RegLoc :: !(r tp) -> BoundLoc r tp + -- | @StackkOffLoc o repr@ denotes the bytes from address range + -- @[initSP + o .. initSP + o + memReprBytes repr)@. + -- + -- We should note that this makes no claim that those addresses + -- are valid. + StackOffLoc :: !(MemInt (RegAddrWidth r)) + -> !(MemRepr tp) + -> BoundLoc r tp + +instance TestEquality r => TestEquality (BoundLoc r) where + testEquality (RegLoc x) (RegLoc y) = testEquality x y + testEquality (StackOffLoc xi xr) (StackOffLoc yi yr) | xi == yi = + testEquality xr yr + testEquality _ _ = Nothing + +instance HasRepr r TypeRepr => HasRepr (BoundLoc r) TypeRepr where + typeRepr (RegLoc r) = typeRepr r + typeRepr (StackOffLoc _ r) = typeRepr r + +instance OrdF r => OrdF (BoundLoc r) where + compareF (RegLoc x) (RegLoc y) = compareF x y + compareF (RegLoc _) _ = LTF + compareF _ (RegLoc _) = GTF + + compareF (StackOffLoc xi xr) (StackOffLoc yi yr) = + case compare xi yi of + LT -> LTF + GT -> GTF + EQ -> compareF xr yr + +instance ShowF r => Pretty (BoundLoc r tp) where + pretty (RegLoc r) = text (showF r) + pretty (StackOffLoc i tp) = + text "*(stack_frame " <+> ppAddend i <> text ") :" <> pretty tp + +instance ShowF r => PrettyF (BoundLoc r) where + prettyF = pretty + +------------------------------------------------------------------------ +-- StackMap + +-- | This is a data structure for representing values written to +-- concrete stack offsets. +newtype StackMap w (v :: M.Type -> Type) = SM (Map (MemInt w) (MemVal v)) + +instance FunctorF (StackMap w) where + fmapF f (SM m) = SM (fmap (fmapF f) m) + +-- | Empty stack map +emptyStackMap :: StackMap w p +emptyStackMap = SM Map.empty + +-- | Pretty print a stack map given a term +ppStackMap :: (forall tp . Doc -> v tp -> Doc) -> StackMap w v -> Doc +ppStackMap f (SM m) + | Map.null m = text "empty-stack-map" + | otherwise = + vcat $ + [ f (ppStackOff o repr) v + | (o,MemVal repr v) <- Map.toList m + ] + +instance PrettyF v => Pretty (StackMap w v) where + pretty = ppStackMap (\nm d -> nm <+> text ":=" <+> prettyF d) + +-- | Result returned by @stackMapLookup@. +data StackMapLookup w p tp where + -- 1| We found a value at the exact offset and repr + SMLResult :: !(p tp) -> StackMapLookup w p tp + -- | We found a value that had an overlapping offset and repr. + SMLOverlap :: !(MemInt w) + -> !(MemRepr utp) + -> !(p utp) + -> StackMapLookup w p tp + -- | We found neither an exact match nor an overlapping write. + SMLNone :: StackMapLookup w p tp + +-- | Lookup value (if any) at given offset and representation. +stackMapLookup :: MemWidth w + => MemInt w + -> MemRepr tp + -> StackMap w p + -> StackMapLookup w p tp +stackMapLookup off repr (SM m) = do + let end = off + fromIntegral (memReprBytes repr) + if end < off then + error $ "stackMapLookup given bad offset." + else + case Map.lookupLT end m of + Just (oldOff, MemVal oldRepr val) + -- If match exact + | oldOff == off + , Just Refl <- testEquality oldRepr repr -> + SMLResult val + -- If previous write ends after this write starts + | oldOff + fromIntegral (memReprBytes oldRepr) > off -> + SMLOverlap oldOff oldRepr val + | otherwise -> + SMLNone + Nothing -> SMLNone + +clearPreWrites :: Ord i => i -> i -> Map i v -> Map i v +clearPreWrites l h m = + case Map.lookupLT h m of + Just (o,_v) | o >= l -> clearPreWrites l h (Map.delete o m) + _ -> m + +clearPostWrites :: Ord i => i -> i -> Map i v -> Map i v +clearPostWrites l h m = + case Map.lookupGE l m of + Just (o,_v) | o < h -> clearPostWrites l h (Map.delete o m) + _ -> m + +-- | This assigns a region of bytes to a particular value in the stack. +-- +-- It overwrites any values that overlap with the location. +stackMapOverwrite :: forall w p tp + . MemWidth w + => MemInt w -- ^ Offset in the stack to write to + -> MemRepr tp -- ^ Type of value to write + -> p tp -- ^ Value to write + -> StackMap w p + -> StackMap w p +stackMapOverwrite off repr v (SM m) = + let e = off + fromIntegral (memReprBytes repr) + in SM $ Map.insert off (MemVal repr v) + $ clearPreWrites off e + $ clearPostWrites off e m + +-- | This sets the value at an offset without checking to clear any +-- previous writes to values. +unsafeStackMapInsert :: MemInt w -> MemRepr tp -> p tp -> StackMap w p -> StackMap w p +unsafeStackMapInsert o repr v (SM m) = SM (Map.insert o (MemVal repr v) m) + +stackMapFoldrWithKey :: (forall tp . MemInt w -> MemRepr tp -> v tp -> r -> r) + -> r + -> StackMap w v + -> r +stackMapFoldrWithKey f z (SM m) = + Map.foldrWithKey (\k (MemVal repr v) r -> f k repr v r) z m + +stackMapTraverseWithKey_ :: Applicative m + => (forall tp . MemInt w -> MemRepr tp -> v tp -> m ()) + -> StackMap w v + -> m () +stackMapTraverseWithKey_ f (SM m) = + Map.foldrWithKey (\k (MemVal repr v) r -> f k repr v *> r) (pure ()) m + +stackMapMapWithKey :: (forall tp . MemInt w -> MemRepr tp -> a tp -> b tp) + -> StackMap w a + -> StackMap w b +stackMapMapWithKey f (SM m) = + SM (Map.mapWithKey (\o (MemVal repr v) -> MemVal repr (f o repr v)) m) + +stackMapTraverseMaybeWithKey :: Applicative m + => (forall tp . MemInt w -> MemRepr tp -> a tp -> m (Maybe (b tp))) + -- ^ Traversal function + -> StackMap w a + -> m (StackMap w b) +stackMapTraverseMaybeWithKey f (SM m) = + SM <$> Map.traverseMaybeWithKey (\o (MemVal repr v) -> fmap (MemVal repr) <$> f o repr v) m + +-- @stackMapDropAbove bnd m@ includes only entries in @m@ whose bytes do not go above @bnd@. +stackMapDropAbove :: MemWidth w => Integer -> StackMap w p -> StackMap w p +stackMapDropAbove bnd (SM m) = SM (Map.filterWithKey p m) + where p o (MemVal r _) = toInteger o + toInteger (memReprBytes r) <= bnd + +-- @stackMapDropBelow bnd m@ includes only entries in @m@ whose bytes do not go below @bnd@. +stackMapDropBelow :: MemWidth w => Integer -> StackMap w p -> StackMap w p +stackMapDropBelow bnd (SM m) = SM (Map.filterWithKey p m) + where p o _ = toInteger o >= bnd + +------------------------------------------------------------------------ +-- LocMap + +-- | A map from register/concrete stack offsets to values +data LocMap (r :: M.Type -> Type) (v :: M.Type -> Type) + = LocMap { locMapRegs :: !(MapF r v) + , locMapStack :: !(StackMap (RegAddrWidth r) v) + } + +-- | An empty location map. +locMapEmpty :: LocMap r v +locMapEmpty = LocMap { locMapRegs = MapF.empty, locMapStack = emptyStackMap } + +-- | Pretty print a location map. +ppLocMap :: ShowF r => (forall tp . Doc -> p tp -> Doc) -> LocMap r p -> [Doc] +ppLocMap f m + = flip (MapF.foldrWithKey (\k v -> (f (text (showF k)) v:))) + (locMapRegs m) + $ stackMapFoldrWithKey (\i repr v -> (f (ppStackOff i repr) v:)) + [] + (locMapStack m) + +-- | Return value associated with location or nothing if it is not +-- defined. +locLookup :: (MemWidth (RegAddrWidth r), OrdF r) + => BoundLoc r tp + -> LocMap r v + -> Maybe (v tp) +locLookup (RegLoc r) m = MapF.lookup r (locMapRegs m) +locLookup (StackOffLoc o repr) m = + case stackMapLookup o repr (locMapStack m) of + SMLResult r -> Just r + SMLOverlap _ _ _ -> Nothing + SMLNone -> Nothing + +-- | This associates the location with a value in the map, replacing any existing binding. +-- +-- It is prefixed with "nonOverlap" because it doesn't guarantee that stack +-- values are non-overlapping -- the user should ensure this before calling this. +nonOverlapLocInsert :: OrdF r => BoundLoc r tp -> v tp -> LocMap r v -> LocMap r v +nonOverlapLocInsert (RegLoc r) v m = + m { locMapRegs = MapF.insert r v (locMapRegs m) } +nonOverlapLocInsert (StackOffLoc off repr) v m = + m { locMapStack = unsafeStackMapInsert off repr v (locMapStack m) } + +locOverwriteWith :: (OrdF r, MemWidth (RegAddrWidth r)) + => (v tp -> v tp -> v tp) -- ^ Update takes new and old. + -> BoundLoc r tp + -> v tp + -> LocMap r v + -> LocMap r v +locOverwriteWith upd (RegLoc r) v m = + m { locMapRegs = MapF.insertWith upd r v (locMapRegs m) } +locOverwriteWith upd (StackOffLoc o repr) v m = + let nv = case stackMapLookup o repr (locMapStack m) of + SMLNone -> v + SMLOverlap _ _ _ -> v + SMLResult oldv -> upd v oldv + in m { locMapStack = stackMapOverwrite o repr nv (locMapStack m) } + +------------------------------------------------------------------------ +-- StackEqConstraint + +-- | A constraint on a location for the stack analysis. +data StackEqConstraint r tp where + -- | An equivalence class representative with the given number of + -- elements. + -- + -- In our map the number of equivalence class members should always + -- be positive. + IsStackOff :: !(MemInt (RegAddrWidth r)) -> StackEqConstraint r (BVType (RegAddrWidth r)) + EqualLoc :: !(BoundLoc r tp) -> StackEqConstraint r tp + +ppStackEqConstraint :: ShowF r => Doc -> StackEqConstraint r tp -> Doc +ppStackEqConstraint d (IsStackOff i) = + d <+> text "= stack_frame" <+> ppAddend i +ppStackEqConstraint d (EqualLoc l) = d <+> text "=" <+> pretty l + +------------------------------------------------------------------------ +-- BlockStartStackConstraints + +-- | Constraints on start of block +newtype BlockStartStackConstraints arch = + BSSC { unBSSC :: LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch)) } + +-- | Pretty print the lines in stack constraints. +ppBlockStartStackConstraints :: ShowF (ArchReg arch) => BlockStartStackConstraints arch -> [Doc] +ppBlockStartStackConstraints = ppLocMap ppStackEqConstraint . unBSSC + +fnEntryBlockStartStackConstraints :: RegisterInfo (ArchReg arch) => BlockStartStackConstraints arch +fnEntryBlockStartStackConstraints = + BSSC LocMap { locMapRegs = MapF.singleton sp_reg (IsStackOff 0) + , locMapStack = emptyStackMap + } + +-- | @blockStartLocStackOffset c l@ returns an offset of the stack +-- pointer that the value stored in @l@ is inferred to be equivalent +-- to when the block starts execution. +blockStartLocStackOffset :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) + => BlockStartStackConstraints arch + -> BoundLoc (ArchReg arch) tp + -> Maybe (MemInt (ArchAddrWidth arch)) +blockStartLocStackOffset cns loc = + case locLookup loc (unBSSC cns) of + Nothing -> Nothing + Just (IsStackOff o) -> Just o + Just (EqualLoc loc') -> blockStartLocStackOffset cns loc' + +data StackOffConstraint w tp where + StackOffCns :: !(MemInt w) -> StackOffConstraint w (BVType w) + +-- | @boundsLocRep bnds loc@ returns the representative location for +-- @loc@. +-- +-- This representative location has the property that a location must +-- have the same value as its representative location, and if two +-- locations have provably equal values in the bounds, then they must +-- have the same representative. +blockStartLocRepAndCns :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) + => BlockStartStackConstraints arch + -> BoundLoc (ArchReg arch) tp + -> (BoundLoc (ArchReg arch) tp, Maybe (StackOffConstraint (ArchAddrWidth arch) tp)) +blockStartLocRepAndCns cns l = + case locLookup l (unBSSC cns) of + Just (EqualLoc loc) -> blockStartLocRepAndCns cns loc + Just (IsStackOff o) -> (l,Just (StackOffCns o)) + Nothing -> (l, Nothing) + +------------------------------------------------------------------------ +-- joinStackExpr + +type JoinClassMap r = MapF (JoinClassPair (BoundLoc r)) (BoundLoc r) + +joinStackEqConstraint :: Maybe (StackOffConstraint w tp) + -> Maybe (StackOffConstraint w tp) + -> Changed s (Maybe (StackOffConstraint w tp)) +joinStackEqConstraint Nothing _ = pure Nothing +joinStackEqConstraint p@(Just (StackOffCns i)) (Just (StackOffCns j)) | i == j = pure p +joinStackEqConstraint _ _ = markChanged True $> Nothing + +-- | Join locations +joinNewLoc :: forall s arch tp + . (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) + => BlockStartStackConstraints arch + -> BlockStartStackConstraints arch + -> STRef s (BlockStartStackConstraints arch) + -- ^ The current index bounds. + -> STRef s (JoinClassMap (ArchReg arch)) + -- ^ The map from (oldClassRep, newClassRep) pairs to the + -- result class rep. + -> STRef s Int + -- ^ Stores the number of equivalence classes we have seen in + -- in the old class + -- Used so determining if any classes are changed. + -> BoundLoc (ArchReg arch) tp + -- ^ Location in join that we have not yet visited. + -> StackEqConstraint (ArchReg arch) tp + -- ^ Constraint on location in original list. + -> Changed s () +joinNewLoc old new bndsRef procRef cntr thisLoc oldCns = do + (oldRep, oldPred) <- changedST $ + case oldCns of + EqualLoc oldLoc -> + pure (blockStartLocRepAndCns old oldLoc) + IsStackOff o -> do + -- Increment number of equivalence classes when we see an old + -- representative. + modifySTRef' cntr (+1) + -- Return this loc + pure (thisLoc, Just (StackOffCns o)) + let (newRep, newPred) = blockStartLocRepAndCns new thisLoc + m <- changedST $ readSTRef procRef + -- See if we have already added a representative for this class. + let pair = JoinClassPair oldRep newRep + case MapF.lookup pair m of + Nothing -> do + mp <- joinStackEqConstraint oldPred newPred + changedST $ do + writeSTRef procRef $! MapF.insert pair thisLoc m + case mp of + Nothing -> pure () + Just (StackOffCns o) -> + modifySTRef' bndsRef $ \cns -> BSSC (nonOverlapLocInsert thisLoc (IsStackOff o) (unBSSC cns)) + Just resRep -> + -- Assert r is equal to resRep + changedST $ + modifySTRef' bndsRef $ \cns -> BSSC (nonOverlapLocInsert thisLoc (EqualLoc resRep) (unBSSC cns)) + +-- | Return a jump bounds that implies both input bounds, or `Nothing` +-- if every fact inx the old bounds is implied by the new bounds. +joinBlockStartStackConstraints :: forall arch s + . (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) + => BlockStartStackConstraints arch + -> BlockStartStackConstraints arch + -> Changed s (BlockStartStackConstraints arch, JoinClassMap (ArchReg arch)) +joinBlockStartStackConstraints old new = do + -- Reference to new bounds. + bndsRef <- changedST $ newSTRef (BSSC locMapEmpty) + -- This maps pairs containing the class representative in the old + -- and new maps to the associated class representative in the + -- combined bounds. + procRef <- changedST $ newSTRef MapF.empty + cntr <- changedST $ newSTRef 0 + -- + MapF.traverseWithKey_ + (\r -> joinNewLoc old new bndsRef procRef cntr (RegLoc r)) + (locMapRegs (unBSSC old)) + stackMapTraverseWithKey_ + (\i r c -> joinNewLoc old new bndsRef procRef cntr (StackOffLoc i r) c) + (locMapStack (unBSSC old)) + + -- Check number of equivalence classes in result and original + -- The count should not have decreased, but may increase if two elements + -- are no longer equal, and we need to check this. + origClassCount <- changedST $ readSTRef cntr + resultClassCount <- changedST $ MapF.size <$> readSTRef procRef + unless (origClassCount <= resultClassCount) $ do + error "Original class count should be bound by resultClassCount" + -- Record changed if any classes are different. + markChanged (origClassCount < resultClassCount) + + changedST $ (,) <$> readSTRef bndsRef <*> readSTRef procRef + +------------------------------------------------------------------------ +-- StackExpr + +-- | This is an expression that represents the value of stack +-- locations and assignments during steping through the block. +-- +-- The main diference between this and +-- the `Value` type, index expressions do not depend on values read +-- and written to memory during execution of the block, and are purely +-- functions of the input +-- +-- This is different from `ClassPred` in that @ClassPred@ is a property +-- assigned to equivalence classes +data StackExpr arch ids tp where + -- | This refers to the value that a location had at the start of + -- block execution. + -- + -- The location should be a class representative in the initial bounds. + ClassRepExpr :: !(BoundLoc (ArchReg arch) tp) -> StackExpr arch ids tp + -- | An assignment that is not interpreted, and just treated as a constant. + UninterpAssignExpr :: !(AssignId ids tp) + -> !(TypeRepr tp) + -> StackExpr arch ids tp + -- | Denotes the value of the stack pointer at function start plus some constant. + StackOffsetExpr :: !(MemInt (ArchAddrWidth arch)) + -> StackExpr arch ids (BVType (ArchAddrWidth arch)) + -- | Denotes a constant + CExpr :: !(CValue arch tp) -> StackExpr arch ids tp + + -- | This is a pure function applied to other index expressions that + -- may be worth interpreting (but could be treated as an uninterp + -- assign expr also. + AppExpr :: !(AssignId ids tp) + -> !(App (StackExpr arch ids) tp) + -> StackExpr arch ids tp + +instance TestEquality (ArchReg arch) => TestEquality (StackExpr arch ids) where + testEquality (ClassRepExpr x) (ClassRepExpr y) = + testEquality x y + testEquality (UninterpAssignExpr x _) (UninterpAssignExpr y _) = + testEquality x y + testEquality (StackOffsetExpr x) (StackOffsetExpr y) = + if x == y then + Just Refl + else + Nothing + testEquality (CExpr x) (CExpr y) = + testEquality x y + testEquality (AppExpr xn _xa) (AppExpr yn _ya) = + testEquality xn yn + testEquality _ _ = Nothing + +instance OrdF (ArchReg arch) => OrdF (StackExpr arch ids) where + compareF (ClassRepExpr x) (ClassRepExpr y) = compareF x y + compareF ClassRepExpr{} _ = LTF + compareF _ ClassRepExpr{} = GTF + + compareF (UninterpAssignExpr x _) (UninterpAssignExpr y _) = compareF x y + compareF UninterpAssignExpr{} _ = LTF + compareF _ UninterpAssignExpr{} = GTF + + compareF (StackOffsetExpr x) (StackOffsetExpr y) = fromOrdering (compare x y) + compareF StackOffsetExpr{} _ = LTF + compareF _ StackOffsetExpr{} = GTF + + compareF (CExpr x) (CExpr y) = compareF x y + compareF CExpr{} _ = LTF + compareF _ CExpr{} = GTF + + compareF (AppExpr xn _xa) (AppExpr yn _ya) = compareF xn yn + +instance ( HasRepr (ArchReg arch) TypeRepr + , MemWidth (ArchAddrWidth arch) + ) => HasRepr (StackExpr arch ids) TypeRepr where + typeRepr e = + case e of + ClassRepExpr x -> typeRepr x + UninterpAssignExpr _ tp -> tp + StackOffsetExpr _ -> addrTypeRepr + CExpr x -> typeRepr x + AppExpr _ a -> typeRepr a + +instance ShowF (ArchReg arch) => Pretty (StackExpr arch id tp) where + pretty e = + case e of + ClassRepExpr l -> pretty l + UninterpAssignExpr n _ -> parens (text "uninterp" <+> ppAssignId n) + StackOffsetExpr o -> parens (text "+ stack_off" <+> pretty o) + CExpr v -> pretty v + AppExpr n _ -> parens (text "app" <+> ppAssignId n) + +instance ShowF (ArchReg arch) => PrettyF (StackExpr arch id) where + prettyF = pretty + +-- | Return an expression equivalent to the location in the constraint +-- map. +-- +-- This attempts to normalize the expression to get a representative. +blockStartLocExpr :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) + => BlockStartStackConstraints arch + -> BoundLoc (ArchReg arch) tp + -> StackExpr arch ids tp +blockStartLocExpr bnds loc = + case locLookup loc (unBSSC bnds) of + Nothing -> ClassRepExpr loc + Just (IsStackOff o) -> StackOffsetExpr o + Just (EqualLoc loc') -> blockStartLocExpr bnds loc' + +------------------------------------------------------------------------ +-- BlockIntraStackConstraints + +-- | Information about bounds for a particular value within a block. +data BlockIntraStackConstraints arch ids + = BISC { biscInitConstraints :: !(BlockStartStackConstraints arch) + -- ^ Bounds at execution start. + , stackExprMap :: !(StackMap (ArchAddrWidth arch) (StackExpr arch ids)) + -- ^ Maps stack offsets to the expression associated with them. + , assignExprMap :: !(MapF (AssignId ids) (StackExpr arch ids)) + -- ^ Maps processed assignments to index expressions. + , memoTable :: !(MapF (App (StackExpr arch ids)) (StackExpr arch ids)) + -- ^ Table for ensuring each bound expression has a single + -- representative. + } + +-- | Create index bounds from initial index bounds. +mkBlockIntraStackConstraints :: forall arch ids + . (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) + => BlockStartStackConstraints arch + -> BlockIntraStackConstraints arch ids +mkBlockIntraStackConstraints bnds = + let stackExpr :: MemInt (ArchAddrWidth arch) + -> MemRepr tp + -> StackEqConstraint (ArchReg arch) tp + -> StackExpr arch ids tp + stackExpr i tp _ = blockStartLocExpr bnds (StackOffLoc i tp) + in BISC { biscInitConstraints = bnds + , stackExprMap = stackMapMapWithKey stackExpr (locMapStack (unBSSC bnds)) + , assignExprMap = MapF.empty + , memoTable = MapF.empty + } + +-- | Return the value of the index expression given the bounds. +blockIntraValueExpr :: forall arch ids tp + . (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) + => BlockIntraStackConstraints arch ids + -> Value arch ids tp + -> StackExpr arch ids tp +blockIntraValueExpr bnds val = + case val of + CValue c -> CExpr c + AssignedValue (Assignment aid _) -> + case MapF.lookup aid (assignExprMap bnds) of + Just e -> e + Nothing -> error $ "blockIntraValueExpr internal: Expected value to be assigned." + Initial r -> blockStartLocExpr (biscInitConstraints bnds) (RegLoc r) + +-- | Return stack offset if value is a stack offset. +blockIntraValueStackOffset :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) + => BlockIntraStackConstraints arch ids + -> Value arch ids (BVType (ArchAddrWidth arch)) + -> Maybe (MemInt (ArchAddrWidth arch)) +blockIntraValueStackOffset bnds val = + case blockIntraValueExpr bnds val of + StackOffsetExpr i -> Just i + _ -> Nothing + +-- | Return an expression associated with the @AssignRhs@. +blockIntraRhsExpr :: forall arch ids tp + . ( MemWidth (ArchAddrWidth arch) + , OrdF (ArchReg arch) + , ShowF (ArchReg arch) + ) + => BlockIntraStackConstraints arch ids + -> AssignId ids tp + -> AssignRhs arch (Value arch ids) tp + -> StackExpr arch ids tp +blockIntraRhsExpr bnds aid arhs = + case arhs of + EvalApp app -> do + let stackFn v = toInteger <$> blockIntraValueStackOffset bnds v + case appAsStackOffset stackFn app of + Just (StackOffsetView o) -> do + StackOffsetExpr $ fromInteger o + _ -> + let a = fmapFC (blockIntraValueExpr bnds) app + in case MapF.lookup a (memoTable bnds) of + Just r -> r + Nothing -> AppExpr aid a + ReadMem addr repr + | Just o <- blockIntraValueStackOffset bnds addr + , SMLResult e <- stackMapLookup o repr (stackExprMap bnds) -> + e + _ -> UninterpAssignExpr aid (typeRepr arhs) + +-- | Associate the given bound expression with the assignment. +bindAssignment :: AssignId ids tp + -> StackExpr arch ids tp + -> BlockIntraStackConstraints arch ids + -> BlockIntraStackConstraints arch ids +bindAssignment aid expr bnds = + bnds { assignExprMap = MapF.insert aid expr (assignExprMap bnds) } + +-- | Discard information about the stack in the bounds due to an +-- operation that may affect the stack. +discardStackInfo :: BlockIntraStackConstraints arch ids + -> BlockIntraStackConstraints arch ids +discardStackInfo bnds = + bnds { stackExprMap = emptyStackMap } + +-- | Update the stack to point to the given expression. +writeStackOff :: forall arch ids tp + . (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) + => BlockIntraStackConstraints arch ids + -> MemInt (ArchAddrWidth arch) + -> MemRepr tp + -> Value arch ids tp + -> BlockIntraStackConstraints arch ids +writeStackOff bnds off repr v = + bnds { stackExprMap = stackMapOverwrite off repr (blockIntraValueExpr bnds v) (stackExprMap bnds) } + +------------------------------------------------------------------------ +-- NextStateMonad + +-- | Maps bound expression that have been visited to their location. +-- +-- We memoize expressions seen so that we can infer when two locations +-- must be equal. +data NextBlockState arch ids = + NBS { nbsExprMap :: !(MapF (StackExpr arch ids) (BoundLoc (ArchReg arch) )) + , nbsRepLocs :: ![Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)] + -- ^ List of location expression pairs + } + +-- Monad used for computing next states. +newtype NextStateMonad arch ids a = NSM (State (NextBlockState arch ids) a) + deriving (Functor, Applicative, Monad) + +runNextStateMonad :: NextStateMonad arch ids a -> a +runNextStateMonad (NSM m) = evalState m $! NBS { nbsExprMap = MapF.empty, nbsRepLocs = [] } + +-- | Return a list of locations and associated expressions that +-- represent equivalence classes in the next state. +-- +-- Note that each equivalence class has a unique stack expression, so +-- all the locations in an equivalence class should have the same +-- expression. +getNextStateRepresentatives :: NextStateMonad arch ids [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)] +getNextStateRepresentatives = NSM $ gets nbsRepLocs + +------------------------------------------------------------------------ +-- BlockIntraStackConstraints next state + +-- | Return the constraint associated with the given location and expression +-- or nothing if the constraint is the top one and should be stored. +nextStateStackEqConstraint :: ( MemWidth (ArchAddrWidth arch) + , HasRepr (ArchReg arch) TypeRepr + , OrdF (ArchReg arch) + , ShowF (ArchReg arch) + ) + => BoundLoc (ArchReg arch) tp + -- ^ Location expression is stored at. + -> StackExpr arch ids tp + -- ^ Expression to infer predicate or. + -> NextStateMonad arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)) +nextStateStackEqConstraint loc e = do + s <- NSM $ get + case MapF.lookup e (nbsExprMap s) of + Just l -> + pure $! Just $ EqualLoc l + Nothing -> do + NSM $ put $! NBS { nbsExprMap = MapF.insert e loc (nbsExprMap s) + , nbsRepLocs = Pair loc e : nbsRepLocs s + } + case e of + StackOffsetExpr o -> + pure $! (Just $! IsStackOff o) + _ -> + pure $! Nothing + +-- | Bounds for block after jump +postJumpStackConstraints :: forall arch ids + . RegisterInfo (ArchReg arch) + => BlockIntraStackConstraints arch ids + -- ^ Constraints at end of block. + -> RegState (ArchReg arch) (Value arch ids) + -- ^ Register values at start of next state. + -> NextStateMonad arch ids (BlockStartStackConstraints arch) +postJumpStackConstraints bnds regs = do + rm <- MapF.traverseMaybeWithKey + (\r v -> nextStateStackEqConstraint (RegLoc r) (blockIntraValueExpr bnds v)) + (regStateMap regs) + sm <- stackMapTraverseMaybeWithKey (\i repr e -> nextStateStackEqConstraint (StackOffLoc i repr) e) + (stackExprMap bnds) + pure $! BSSC (LocMap { locMapRegs = rm, locMapStack = sm }) + +-- | Get the constraint associated with a register after a call. +postCallConstraint :: RegisterInfo (ArchReg arch) + => CallParams (ArchReg arch) + -- ^ Information about calling convention. + -> BlockIntraStackConstraints arch ids + -- ^ Bounds at end of this state. + -> ArchReg arch tp + -- ^ Register to get + -> Value arch ids tp + -- ^ Value of register at time call occurs. + -> NextStateMonad arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)) +postCallConstraint params bnds r v + | Just Refl <- testEquality r sp_reg + , StackOffsetExpr o <- blockIntraValueExpr bnds v = do + pure $! (Just $! IsStackOff (o+fromInteger (postCallStackDelta params))) + | preserveReg params r = + nextStateStackEqConstraint (RegLoc r) (blockIntraValueExpr bnds v) + | otherwise = + pure Nothing + +-- | Return the index bounds after a function call. +postCallStackConstraints :: forall arch ids + . RegisterInfo (ArchReg arch) + => CallParams (ArchReg arch) + -> BlockIntraStackConstraints arch ids + -> RegState (ArchReg arch) (Value arch ids) + -> BlockStartStackConstraints arch +postCallStackConstraints params cns regs = + runNextStateMonad $ do + rm <- MapF.traverseMaybeWithKey (postCallConstraint params cns) (regStateMap regs) + + let finalStack = stackExprMap cns + let filteredStack = + case blockIntraValueExpr cns (getBoundValue sp_reg regs) of + StackOffsetExpr spOff + | stackGrowsDown params -> + let newOff = toInteger spOff + postCallStackDelta params + -- Keep entries at offsets above return address. + in stackMapDropBelow newOff finalStack + | otherwise -> + let newOff = toInteger spOff + postCallStackDelta params + -- Keep entries whose high address is below new stack offset + in stackMapDropAbove newOff finalStack + _ -> emptyStackMap + let nextStackFn :: MemInt (ArchAddrWidth arch) + -> MemRepr tp + -> StackExpr arch ids tp + -> NextStateMonad arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)) + nextStackFn i repr e = + nextStateStackEqConstraint (StackOffLoc i repr) e + + sm <- stackMapTraverseMaybeWithKey nextStackFn filteredStack + + pure $! BSSC (LocMap { locMapRegs = rm, locMapStack = sm }) diff --git a/base/src/Data/Macaw/Analysis/FunctionArgs.hs b/base/src/Data/Macaw/Analysis/FunctionArgs.hs index 1d05d53f..935d29d6 100644 --- a/base/src/Data/Macaw/Analysis/FunctionArgs.hs +++ b/base/src/Data/Macaw/Analysis/FunctionArgs.hs @@ -395,9 +395,9 @@ valueUses (AssignedValue (Assignment a rhs)) = do rhs' <- foldlMFC (\s v -> seq s $ Set.union s <$> valueUses v) Set.empty rhs seq rhs' $ modify' $ Map.insert (Some a) rhs' pure $ rhs' -valueUses (Initial r) = do +valueUses (Initial r) = pure $! Set.singleton (Some r) -valueUses _ = do +valueUses _ = pure $! Set.empty addValueUses :: (OrdF (ArchReg arch), FoldableFC (ArchFn arch)) @@ -434,7 +434,7 @@ recordBlockTransfer _addr regs regSet = do -> Some (ArchReg arch) -> State (AssignmentCache (ArchReg arch) ids) (FinalRegisterDemands (ArchReg arch)) - doReg m (Some r) = do + doReg m (Some r) = case testEquality r ip_reg of Just _ -> pure m Nothing -> do diff --git a/base/src/Data/Macaw/Analysis/RegisterUse.hs b/base/src/Data/Macaw/Analysis/RegisterUse.hs index e51dbf60..5328c014 100644 --- a/base/src/Data/Macaw/Analysis/RegisterUse.hs +++ b/base/src/Data/Macaw/Analysis/RegisterUse.hs @@ -38,7 +38,8 @@ import qualified Data.Set as Set import GHC.Stack import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) -import Data.Macaw.AbsDomain.JumpBounds +import Data.Macaw.AbsDomain.JumpBounds (initBndsMap) +import Data.Macaw.AbsDomain.StackAnalysis import Data.Macaw.CFG.DemandSet ( DemandContext , demandConstraints @@ -78,7 +79,7 @@ type AssignStackOffsetMap w ids = Map (Some (AssignId ids)) (MemInt w) valueStackOffset :: ( MemWidth (ArchAddrWidth arch) , OrdF (ArchReg arch) ) - => InitJumpBounds arch + => BlockStartStackConstraints arch -> AssignStackOffsetMap (ArchAddrWidth arch) ids -> Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe (MemInt (ArchAddrWidth arch)) @@ -87,9 +88,7 @@ valueStackOffset bnds amap v = CValue{} -> Nothing Initial r -> - case boundsLocationInfo bnds (RegLoc r) of - (_rep, IsStackOffset o) -> Just o - _ -> Nothing + blockStartLocStackOffset bnds (RegLoc r) AssignedValue (Assignment aid _) -> Map.lookup (Some aid) amap @@ -251,7 +250,7 @@ data RegisterUseContext arch ids -- particular locations after the block executes. data BlockUsageSummary (arch :: Type) ids = RUS { -- | Information about stack layout/jump bounds at start of block. - blockPrecond :: !(InitJumpBounds arch) + blockPrecond :: !(BlockStartStackConstraints arch) -- | Maps locations to the dependencies needed to compute values in that location. , _blockInitDeps :: !(BlockProvideDepMap (ArchReg arch) ids) -- | Dependencies needed to execute statements with side effects. @@ -266,9 +265,9 @@ data BlockUsageSummary (arch :: Type) ids = RUS type RegisterUseM arch ids a = ReaderT (RegisterUseContext arch ids) (StateT (BlockUsageSummary arch ids) (Except String)) a -initBlockUsageSummary :: InitJumpBounds arch -> BlockUsageSummary arch ids -initBlockUsageSummary bnds = - RUS { blockPrecond = bnds +initBlockUsageSummary :: BlockStartStackConstraints arch -> BlockUsageSummary arch ids +initBlockUsageSummary bCns = + RUS { blockPrecond = bCns , _blockInitDeps = emptyBlockProvideDepMap , _blockExecDemands = emptyDeps , _assignmentCache = Map.empty @@ -459,7 +458,7 @@ summarizeBlock :: forall arch ids -> ParsedBlock arch ids -> Except String (BlockUsageSummary arch ids) summarizeBlock ctx blk = do - let s0 = initBlockUsageSummary (blockJumpBounds blk) + let s0 = initBlockUsageSummary (initBndsMap (blockJumpBounds blk)) flip execStateT s0 $ flip runReaderT ctx $ do let addr = pblockAddr blk -- Add demanded values for terminal diff --git a/base/src/Data/Macaw/Discovery.hs b/base/src/Data/Macaw/Discovery.hs index e462db6b..3b637388 100644 --- a/base/src/Data/Macaw/Discovery.hs +++ b/base/src/Data/Macaw/Discovery.hs @@ -158,7 +158,7 @@ cameFromUnsoundReason found_map rsn = do -- | Add any values needed to compute term statement to demand set. addTermDemands :: TermStmt arch ids -> DemandComp arch ids () -addTermDemands t = do +addTermDemands t = case t of FetchAndExecute regs -> do traverseF_ addValueDemands regs @@ -1218,10 +1218,11 @@ directJumpClassifier = classifierName "Jump" $ do let abst = finalAbsBlockState (classifierAbsState bcc) (classifierFinalRegState bcc) let abst' = abst & setAbsIP tgt_mseg + let tgtBnds = Jmp.postJumpBounds (classifierJumpBounds bcc) (classifierFinalRegState bcc) pure $ ParsedContents { parsedNonterm = toList (classifierStmts bcc) , parsedTerm = ParsedJump (classifierFinalRegState bcc) tgt_mseg , writtenCodeAddrs = classifierWrittenAddrs bcc - , intraJumpTargets = [(tgt_mseg, abst', Jmp.nextBlockBounds (classifierJumpBounds bcc) (classifierFinalRegState bcc))] + , intraJumpTargets = [(tgt_mseg, abst', tgtBnds)] , newFunctionAddrs = [] } @@ -1240,7 +1241,7 @@ jumpTableClassifier = classifierName "Jump table" $ do let abst :: AbsBlockState (ArchReg arch) abst = finalAbsBlockState (classifierAbsState bcc) (classifierFinalRegState bcc) - let nextBnds = Jmp.nextBlockBounds (classifierJumpBounds bcc) (classifierFinalRegState bcc) + let nextBnds = Jmp.postJumpBounds (classifierJumpBounds bcc) (classifierFinalRegState bcc) let term = ParsedLookupTable (classifierFinalRegState bcc) jumpIndex entries pure $ seq abst $ ParsedContents { parsedNonterm = toList (classifierStmts bcc) diff --git a/base/src/Data/Macaw/Utils/Changed.hs b/base/src/Data/Macaw/Utils/Changed.hs new file mode 100644 index 00000000..dbfe24ee --- /dev/null +++ b/base/src/Data/Macaw/Utils/Changed.hs @@ -0,0 +1,47 @@ +{- | + +This module defines a monad `Changed` that is designed for supporting +functions which take a value of some type as an argument, and may +modify it's value. + +It is primarily used for abstract domains so that we know if we need +to re-explore a block when joining new edges into the state. +-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +module Data.Macaw.Utils.Changed + ( Changed + , runChanged + , markChanged + , changedST + ) where + +import Control.Monad.Reader +import Control.Monad.ST +import Data.STRef + +------------------------------------------------------------------------ +-- Changed + +-- | A monad that can be used to record when a value is changed. +newtype Changed s a = Changed { unChanged :: ReaderT (STRef s Bool) (ST s) a } + deriving (Functor, Applicative, Monad) + +-- | Run a `ST` computation. +changedST :: ST s a -> Changed s a +changedST m = Changed (lift m) + +-- | Record the value has changed if the Boolean is true. +markChanged :: Bool -> Changed s () +markChanged False = pure () +markChanged True = do + r <- Changed ask + changedST $ writeSTRef r True + +runChanged :: forall a . (forall s . Changed s a) -> Maybe a +runChanged action = runST $ do + r <- newSTRef False + a <- runReaderT (unChanged action) r + b <- readSTRef r + pure $! if b then Just a else Nothing