GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-28 01:35:33 +03:00
Code Issues Projects Releases Wiki Activity

Fix JumpBounds.

Browse Source
This commit is contained in:
Joe Hendrix 2017-01-31 13:47:26 -08:00
parent cc76e82455
commit 79a3390b09
No known key found for this signature in database
GPG Key ID: 00F67DE32381DB9F
3 changed files with 62 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Data/Macaw/AbsDomain/AbsState.hs
View File

@ -1208,7 +1208,7 @@ finalAbsBlockState c s =
transferReg r = transferValue c (s^.boundValue r)
in AbsBlockState { _absRegState = mkRegState transferReg
, _startAbsStack = c^.curAbsStack
, _initIndexBounds = nextBlockBounds s (c^.indexBounds)
, _initIndexBounds = nextBlockBounds (c^.indexBounds) s
}
------------------------------------------------------------------------

5
src/Data/Macaw/CFG.hs
View File

@ -65,6 +65,7 @@ module Data.Macaw.CFG
, traverseApp
-- * RegState
, RegState
, regStateMap
, boundValue
, cmpRegState
, curIP
@ -1006,6 +1007,10 @@ deriving instance FoldableF (RegState r)
instance TraversableF (RegState r) where
traverseF f (RegState m) = RegState <$> traverseF f m
-- | Return underlying map of register state.
regStateMap :: RegState r f -> MapF.MapF r f
regStateMap (RegState m) = m
-- | Traverse the register state with the name of each register and value.
traverseRegsWith :: Applicative m
=> (forall tp. r tp -> f tp -> m (g tp))

96
src/Data/Macaw/Discovery/JumpBounds.hs
View File

@ -8,7 +8,7 @@ module Data.Macaw.Discovery.JumpBounds
, joinInitialBounds
, IndexBounds
, mkIndexBounds
, addUpperBounds
, addUpperBound
, lookupUpperBound
, nextBlockBounds
) where
@ -16,6 +16,7 @@ module Data.Macaw.Discovery.JumpBounds
import Control.Lens
import Control.Monad.State
import Data.Functor
import Data.Parameterized.Classes
import Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.NatRepr (maxUnsigned)
@ -24,28 +25,28 @@ import Data.Macaw.CFG
import Data.Macaw.Types
-- | An upper bound on a value.
data UpperBounds tp = forall w . (tp ~ BVType w) => IntegerUpperBound Integer
data UpperBound tp = forall w . (tp ~ BVType w) => IntegerUpperBound Integer
instance Eq (UpperBounds tp) where
instance Eq (UpperBound tp) where
IntegerUpperBound x == IntegerUpperBound y = x == y
instance MapF.EqF UpperBounds where
instance MapF.EqF UpperBound where
eqF = (==)
instance Ord (UpperBounds tp) where
instance Ord (UpperBound tp) where
compare (IntegerUpperBound x) (IntegerUpperBound y) = compare x y
-- | Bounds for a function as the start of a block.
data InitialIndexBounds r
= InitialIndexBounds { initialRegUpperBounds :: !(MapF r UpperBounds)
= InitialIndexBounds { initialRegUpperBound :: !(MapF r UpperBound)
}
instance MapF.TestEquality r => Eq (InitialIndexBounds r) where
x == y = initialRegUpperBounds x == initialRegUpperBounds y
x == y = initialRegUpperBound x == initialRegUpperBound y
-- | Create initial index bounds that can represent any system state.
arbitraryInitialBounds :: InitialIndexBounds reg
arbitraryInitialBounds = InitialIndexBounds { initialRegUpperBounds = MapF.empty }
arbitraryInitialBounds = InitialIndexBounds { initialRegUpperBound = MapF.empty }
type Changed = State Bool
@ -66,87 +67,102 @@ joinInitialBounds :: forall r
-> InitialIndexBounds r
-> Maybe (InitialIndexBounds r)
joinInitialBounds old new = runChanged $ do
let combineF :: r tp -> UpperBounds tp -> UpperBounds tp -> Changed (Maybe (UpperBounds tp))
let combineF :: r tp -> UpperBound tp -> UpperBound tp -> Changed (Maybe (UpperBound tp))
combineF _ (IntegerUpperBound x) (IntegerUpperBound y) =
markChanged (x < y) $> Just (IntegerUpperBound (max x y))
-- Mark upper bounds exclusively in old set.
-- If we have any only-old bounds add mark value as changed.
oldF :: MapF r UpperBounds -> Changed (MapF r UpperBounds)
oldF :: MapF r UpperBound -> Changed (MapF r UpperBound)
oldF m = markChanged (not (MapF.null m)) $> MapF.empty
-- How to upper bounds exclusively in new set.
-- Drop any only-new bounds.
newF :: MapF r UpperBounds -> Changed (MapF r UpperBounds)
newF :: MapF r UpperBound -> Changed (MapF r UpperBound)
newF _ = pure MapF.empty
z <- MapF.mergeWithKeyM combineF oldF newF (initialRegUpperBounds old) (initialRegUpperBounds new)
pure InitialIndexBounds { initialRegUpperBounds = z }
z <- MapF.mergeWithKeyM combineF oldF newF (initialRegUpperBound old) (initialRegUpperBound new)
pure InitialIndexBounds { initialRegUpperBound = z }
-- | Information about bounds for a particular value within a block.
data IndexBounds reg ids
= IndexBounds { _regBounds :: !(MapF reg UpperBounds)
, _assignUpperBounds :: !(MapF (AssignId ids) UpperBounds)
= IndexBounds { _regBounds :: !(MapF reg UpperBound)
, _assignUpperBound :: !(MapF (AssignId ids) UpperBound)
}
-- | Maps assignment ids to the associated upper bounds
regBounds :: Simple Lens (IndexBounds reg ids) (MapF reg UpperBounds)
regBounds :: Simple Lens (IndexBounds reg ids) (MapF reg UpperBound)
regBounds = lens _regBounds (\s v -> s { _regBounds = v })
-- | Maps assignment ids to the associated upper bounds
assignUpperBounds :: Simple Lens (IndexBounds reg ids) (MapF (AssignId ids) UpperBounds)
assignUpperBounds = lens _assignUpperBounds (\s v -> s { _assignUpperBounds = v })
assignUpperBound :: Simple Lens (IndexBounds reg ids) (MapF (AssignId ids) UpperBound)
assignUpperBound = lens _assignUpperBound (\s v -> s { _assignUpperBound = v })
-- | Create index bounds from initial index bounds.
mkIndexBounds :: InitialIndexBounds reg -> IndexBounds reg ids
mkIndexBounds i = IndexBounds { _regBounds = initialRegUpperBounds i
, _assignUpperBounds = MapF.empty
mkIndexBounds i = IndexBounds { _regBounds = initialRegUpperBound i
, _assignUpperBound = MapF.empty
}
addUpperBounds :: ( MapF.OrdF (ArchReg arch)
addUpperBound :: ( MapF.OrdF (ArchReg arch)
, HasRepr (ArchReg arch) TypeRepr
)
=> BVValue arch ids w
-> Integer -- ^ Upper bound as an unsigned number
-> IndexBounds (ArchReg arch) ids
-> Either String (IndexBounds (ArchReg arch) ids)
addUpperBounds v u bnds
addUpperBound v u bnds
-- Do nothing if upper bounds equals or exceeds function
| u >= maxUnsigned (valueWidth v) = Right bnds
| u < 0 = error "addUpperBounds given negative value."
| u < 0 = error "addUpperBound given negative value."
| otherwise =
case v of
BVValue _ c | c <= u -> Right bnds
| otherwise -> Left "Constant given upper bound that is statically less than given bounds"
RelocatableValue{} -> Left "Relocatable value does not have upper bounds."
AssignedValue a ->
Right $ bnds & assignUpperBounds %~ MapF.insertWith min (assignId a) (IntegerUpperBound u)
Right $ bnds & assignUpperBound %~ MapF.insertWith min (assignId a) (IntegerUpperBound u)
Initial r ->
Right $ bnds & regBounds %~ MapF.insertWith min r (IntegerUpperBound u)
-- | Lookup an upper bound or return analysis for why it is not defined.
lookupUpperBound :: ( MapF.OrdF (ArchReg arch)
, Show (ArchReg arch (BVType w))
, MapF.ShowF (ArchReg arch)
)
=> BVValue arch ids w
-> IndexBounds (ArchReg arch) ids
-> Either String Integer
lookupUpperBound v bnds =
=> IndexBounds (ArchReg arch) ids
-> Value arch ids tp
-> Either String (UpperBound tp)
lookupUpperBound bnds v =
case v of
BVValue _ i -> Right i
RelocatableValue{} -> Left "Relocatable values do not have bounds."
BVValue _ i -> Right (IntegerUpperBound i)
RelocatableValue{} ->
Left "Relocatable values do not have bounds."
AssignedValue a ->
case MapF.lookup (assignId a) (bnds^.assignUpperBounds) of
Just (IntegerUpperBound bnd) -> Right bnd
case MapF.lookup (assignId a) (bnds^.assignUpperBound) of
Just bnd -> Right bnd
Nothing -> Left $ "Could not find upper bounds for " ++ show (assignId a) ++ "."
Initial r ->
case MapF.lookup r (bnds^.regBounds) of
Just (IntegerUpperBound bnd) -> Right bnd
Nothing -> Left $ "Could not find upper bounds for " ++ show r ++ "."
Just bnd -> Right bnd
Nothing -> Left $ "Could not find upper bounds for " ++ showF r ++ "."
nextBlockBounds :: RegState r (Value arch ids)
-> IndexBounds (ArchReg arch) ids
eitherToMaybe :: Either a b -> Maybe b
eitherToMaybe (Right v) = Just v
eitherToMaybe Left{} = Nothing
nextBlockBounds :: forall arch ids
. ( MapF.OrdF (ArchReg arch)
, MapF.ShowF (ArchReg arch)
)
=> IndexBounds (ArchReg arch) ids
-- ^ Index bounds at end of this state.
-> RegState (ArchReg arch) (Value arch ids)
-- ^ Register values at start of next state.
-> InitialIndexBounds (ArchReg arch)
nextBlockBounds _regs _bnds =
let m = undefined
in InitialIndexBounds { initialRegUpperBounds = m
nextBlockBounds bnds regs =
let m = regStateMap regs
nextBounds = MapF.mapMaybe (eitherToMaybe . lookupUpperBound bnds) m
in InitialIndexBounds { initialRegUpperBound = nextBounds
}