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

make JumpBounds abstract interpretation more precise

Browse Source
This commit is contained in:
Daniel Wagner 2018-05-25 10:54:19 -04:00
parent d0566fe03b
commit 917f921301
1 changed files with 14 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
base/src/Data/Macaw/AbsDomain/JumpBounds.hs
View File

@ -18,6 +18,7 @@ module Data.Macaw.AbsDomain.JumpBounds
import Control.Lens import Control.Lens
import Control.Monad.State import Control.Monad.State
import Data.Bits
import Data.Functor import Data.Functor
import Data.Parameterized.Classes import Data.Parameterized.Classes
import Data.Parameterized.Map (MapF) import Data.Parameterized.Map (MapF)
@ -165,12 +166,17 @@ assertPred (AssignedValue a) isTrue bnds =
EvalApp (BVUnsignedLe x (BVValue _ c)) | isTrue -> addUpperBound x c bnds EvalApp (BVUnsignedLe x (BVValue _ c)) | isTrue -> addUpperBound x c bnds
-- Given not (c <= y), assert y <= (c-1) -- Given not (c <= y), assert y <= (c-1)
EvalApp (BVUnsignedLe (BVValue _ c) y) | not isTrue -> addUpperBound y (c-1) bnds EvalApp (BVUnsignedLe (BVValue _ c) y) | not isTrue -> addUpperBound y (c-1) bnds
-- Given x && y, assert x, then assert y
EvalApp (AndApp l r) | isTrue -> (assertPred l isTrue >=> assertPred r isTrue) bnds
-- Given not (x || y), assert not x, then assert not y
EvalApp (OrApp l r) | not isTrue -> (assertPred l isTrue >=> assertPred r isTrue) bnds
_ -> Right bnds _ -> Right bnds
assertPred _ _ bnds = Right bnds assertPred _ _ bnds = Right bnds
-- | Lookup an upper bound or return analysis for why it is not defined. -- | Lookup an upper bound or return analysis for why it is not defined.
unsignedUpperBound :: ( MapF.OrdF (ArchReg arch) unsignedUpperBound :: ( MapF.OrdF (ArchReg arch)
, MapF.ShowF (ArchReg arch) , MapF.ShowF (ArchReg arch)
, RegisterInfo (ArchReg arch)
) )
=> IndexBounds (ArchReg arch) ids => IndexBounds (ArchReg arch) ids
-> Value arch ids tp -> Value arch ids tp
@ -194,6 +200,13 @@ unsignedUpperBound bnds v =
Right (IntegerUpperBound (min xb yb)) Right (IntegerUpperBound (min xb yb))
(Right xb, Left{}) -> Right xb (Right xb, Left{}) -> Right xb
(Left{}, yb) -> yb (Left{}, yb) -> yb
EvalApp (SExt x w) -> do
IntegerUpperBound r <- unsignedUpperBound bnds x
-- sign-extend r
pure . IntegerUpperBound
$ if r < 2^(natValue w-1)
then r
else maxUnsigned (typeWidth v) .&. r
EvalApp (UExt x _) -> do EvalApp (UExt x _) -> do
IntegerUpperBound r <- unsignedUpperBound bnds x IntegerUpperBound r <- unsignedUpperBound bnds x
pure (IntegerUpperBound r) pure (IntegerUpperBound r)
@ -214,6 +227,7 @@ eitherToMaybe Left{} = Nothing
nextBlockBounds :: forall arch ids nextBlockBounds :: forall arch ids
. ( MapF.OrdF (ArchReg arch) . ( MapF.OrdF (ArchReg arch)
, MapF.ShowF (ArchReg arch) , MapF.ShowF (ArchReg arch)
, RegisterInfo (ArchReg arch)
) )
=> IndexBounds (ArchReg arch) ids => IndexBounds (ArchReg arch) ids
-- ^ Index bounds at end of this state. -- ^ Index bounds at end of this state.