GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-01 00:22:24 +03:00
Code Issues Projects Releases Wiki Activity

AbsState: Add missing casses to concretize and absValueSize

Browse Source
This commit is contained in:
Jason Dagit 2017-07-12 16:34:11 -07:00
parent 0e66a3dfea
commit 66b41f1d56
1 changed files with 11 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -286,7 +286,11 @@ concretize (SubValue _ _) = Nothing -- we know nothing about _all_ values
concretize (StridedInterval s) = concretize (StridedInterval s) =
debug DAbsInt ("Concretizing " ++ show (pretty s)) $ debug DAbsInt ("Concretizing " ++ show (pretty s)) $
Just (Set.fromList (SI.toList s)) Just (Set.fromList (SI.toList s))
concretize _ = Nothing concretize (BoolConst b) = Just (Set.singleton (if b then 1 else 0))
concretize SomeStackOffset{} = Nothing
concretize TopV = Nothing
concretize ReturnAddr = Nothing
concretize StackOffset{} = Nothing
-- FIXME: make total, we would need to carry around tp -- FIXME: make total, we would need to carry around tp
absValueSize :: AbsValue w tp -> Maybe Integer absValueSize :: AbsValue w tp -> Maybe Integer
@ -294,9 +298,13 @@ absValueSize (FinSet s) = Just $ fromIntegral (Set.size s)
absValueSize (CodePointers s b) = Just $ fromIntegral (Set.size s) + (if b then 1 else 0) absValueSize (CodePointers s b) = Just $ fromIntegral (Set.size s) + (if b then 1 else 0)
absValueSize (StridedInterval s) = Just $ SI.size s absValueSize (StridedInterval s) = Just $ SI.size s
absValueSize (StackOffset _ s) = Just $ fromIntegral (Set.size s) absValueSize (StackOffset _ s) = Just $ fromIntegral (Set.size s)
absValueSize _ = Nothing absValueSize (BoolConst _) = Just 1
absValueSize SomeStackOffset{} = Nothing
absValueSize SubValue{} = Nothing
absValueSize TopV = Nothing
absValueSize ReturnAddr = Nothing
-- | Return single value is the abstract value can only take on one value. -- | Returns single value, if the abstract value can only take on one value.
asConcreteSingleton :: MemWidth w => AbsValue w tp -> Maybe Integer asConcreteSingleton :: MemWidth w => AbsValue w tp -> Maybe Integer
asConcreteSingleton v = do asConcreteSingleton v = do
sz <- absValueSize v sz <- absValueSize v