{- |

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 #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.AbsDomain.JumpBounds
  ( -- * Initial jump bounds
    InitJumpBounds
  , initBndsMap
  , functionStartBounds
  , ppInitJumpBounds
  , joinInitialBounds
    -- * IntraJumpbounds
  , IntraJumpBounds
  , blockEndBounds
  , postCallBounds
  , postJumpBounds
  , BranchBounds(..)
  , postBranchBounds
  , unsignedUpperBound
  -- * Jump Targets
  , IntraJumpTarget
  ) where

import           Control.Monad (unless, when)
import           Data.Bits
import           Data.Foldable
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Monoid
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           Numeric.Natural
import           Prettyprinter

import           Data.Macaw.AbsDomain.AbsState ( AbsBlockState )
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           Data.Macaw.Utils.Changed

------------------------------------------------------------------------
-- RangePred

-- | A lower and or upper bound on a value when the value is interpreted
-- as an unsigned integer.
data RangePred u =
  -- | @RangePred w l h@ indicates a constraint on @w@ bits of the value
  -- are between @l@ and @h@ when the bitvector is treated as an
  -- unsigned integer.
  RangePred { forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth :: !(NatRepr u)
            , forall (u :: Nat). RangePred u -> Nat
rangeLowerBound :: !Natural
            , forall (u :: Nat). RangePred u -> Nat
rangeUpperBound :: !Natural
            }
  deriving (Int -> RangePred u -> ShowS
[RangePred u] -> ShowS
RangePred u -> String
(Int -> RangePred u -> ShowS)
-> (RangePred u -> String)
-> ([RangePred u] -> ShowS)
-> Show (RangePred u)
forall (u :: Nat). Int -> RangePred u -> ShowS
forall (u :: Nat). [RangePred u] -> ShowS
forall (u :: Nat). RangePred u -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (u :: Nat). Int -> RangePred u -> ShowS
showsPrec :: Int -> RangePred u -> ShowS
$cshow :: forall (u :: Nat). RangePred u -> String
show :: RangePred u -> String
$cshowList :: forall (u :: Nat). [RangePred u] -> ShowS
showList :: [RangePred u] -> ShowS
Show)

mkLowerBound :: NatRepr u -> Natural -> RangePred u
mkLowerBound :: forall (u :: Nat). NatRepr u -> Nat -> RangePred u
mkLowerBound NatRepr u
w Nat
l = NatRepr u -> Nat -> Nat -> RangePred u
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
RangePred NatRepr u
w Nat
l (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr u -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr u
w))

mkUpperBound :: NatRepr u -> Natural -> RangePred u
mkUpperBound :: forall (u :: Nat). NatRepr u -> Nat -> RangePred u
mkUpperBound NatRepr u
w Nat
u = NatRepr u -> Nat -> Nat -> RangePred u
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
RangePred NatRepr u
w Nat
0 Nat
u

mkRangeBound :: NatRepr u -> Natural -> Natural -> RangePred u
mkRangeBound :: forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
mkRangeBound NatRepr u
w Nat
l Nat
u = NatRepr u -> Nat -> Nat -> RangePred u
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
RangePred NatRepr u
w Nat
l Nat
u

-- | Return true if range does not include whole domain.
rangeNotTotal :: RangePred u -> Bool
rangeNotTotal :: forall (u :: Nat). RangePred u -> Bool
rangeNotTotal RangePred u
r = Nat
0 Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
l Bool -> Bool -> Bool
|| Nat
u Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr u -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr u
w)
  where w :: NatRepr u
w = RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
r
        l :: Nat
l = RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeLowerBound RangePred u
r
        u :: Nat
u = RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
r

instance Pretty (RangePred u) where
  pretty :: forall ann. RangePred u -> Doc ann
pretty (RangePred NatRepr u
w Nat
l Nat
h) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (NatRepr u -> Integer
forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr u
w), Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
l), Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
h)])

------------------------------------------------------------------------
-- 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 MaybeRangePred tp where
  -- | Predicate on bounds.
  SomeRangePred :: (u <= v)
                => !(RangePred u)
                -> MaybeRangePred (BVType v)
  -- | No constraints on value.
  NoRangePred :: MaybeRangePred tp

------------------------------------------------------------------------
-- InitJumpBounds

-- | Constraints on start of block
type BlockStartRangePred arch = LocMap (ArchReg arch) SubRange

-- | Bounds for a function as the start of a block.
data InitJumpBounds arch
   = InitJumpBounds { forall arch. InitJumpBounds arch -> BlockStartStackConstraints arch
initBndsMap    :: !(BlockStartStackConstraints arch)
                    , forall arch. InitJumpBounds arch -> BlockStartRangePred arch
initRngPredMap :: !(BlockStartRangePred arch)
                    , forall arch.
InitJumpBounds arch
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
initAddrPredMap :: !(Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange))
                    }

-- | Pretty print jump bounds.
ppInitJumpBounds :: forall arch ann . ShowF (ArchReg arch) => InitJumpBounds arch -> [Doc ann]
ppInitJumpBounds :: forall arch ann.
ShowF (ArchReg arch) =>
InitJumpBounds arch -> [Doc ann]
ppInitJumpBounds InitJumpBounds arch
cns
  =  BlockStartStackConstraints arch -> [Doc ann]
forall arch ann.
ShowF (ArchReg arch) =>
BlockStartStackConstraints arch -> [Doc ann]
ppBlockStartStackConstraints (InitJumpBounds arch -> BlockStartStackConstraints arch
forall arch. InitJumpBounds arch -> BlockStartStackConstraints arch
initBndsMap InitJumpBounds arch
cns)
  [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> (forall (tp :: Type). Doc ann -> SubRange tp -> Doc ann)
-> LocMap (ArchReg arch) SubRange -> [Doc ann]
forall (r :: Type -> Type) ann (p :: Type -> Type).
ShowF r =>
(forall (tp :: Type). Doc ann -> p tp -> Doc ann)
-> LocMap r p -> [Doc ann]
ppLocMap Doc ann -> SubRange tp -> Doc ann
forall ann (tp :: Type). Doc ann -> SubRange tp -> Doc ann
forall (tp :: Type). Doc ann -> SubRange tp -> Doc ann
ppSubRange (InitJumpBounds arch -> LocMap (ArchReg arch) SubRange
forall arch. InitJumpBounds arch -> BlockStartRangePred arch
initRngPredMap InitJumpBounds arch
cns)
  [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> [ Doc ann -> SubRange tp -> Doc ann
forall ann (tp :: Type). Doc ann -> SubRange tp -> Doc ann
ppSubRange (MemAddr (RegAddrWidth (ArchReg arch)) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MemAddr (RegAddrWidth (ArchReg arch)) -> Doc ann
pretty MemAddr (RegAddrWidth (ArchReg arch))
a) SubRange tp
r | (MemAddr (RegAddrWidth (ArchReg arch))
a,MemVal MemRepr tp
_repr SubRange tp
r) <- Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
-> [(MemAddr (RegAddrWidth (ArchReg arch)), MemVal SubRange)]
forall k a. Map k a -> [(k, a)]
Map.toList (InitJumpBounds arch
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
forall arch.
InitJumpBounds arch
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
initAddrPredMap InitJumpBounds arch
cns) ]

instance ShowF (ArchReg arch) => Pretty (InitJumpBounds arch) where
  pretty :: forall ann. InitJumpBounds arch -> Doc ann
pretty = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann)
-> (InitJumpBounds arch -> [Doc ann])
-> InitJumpBounds arch
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InitJumpBounds arch -> [Doc ann]
forall arch ann.
ShowF (ArchReg arch) =>
InitJumpBounds arch -> [Doc ann]
ppInitJumpBounds

instance ShowF (ArchReg arch) => Show (InitJumpBounds arch) where
  show :: InitJumpBounds arch -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (InitJumpBounds arch -> Doc Any)
-> InitJumpBounds arch
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InitJumpBounds arch -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. InitJumpBounds arch -> Doc ann
pretty

-- | Bounds at start of function.
functionStartBounds :: RegisterInfo (ArchReg arch) => InitJumpBounds arch
functionStartBounds :: forall arch. RegisterInfo (ArchReg arch) => InitJumpBounds arch
functionStartBounds =
  InitJumpBounds { initBndsMap :: BlockStartStackConstraints arch
initBndsMap = BlockStartStackConstraints arch
forall arch.
RegisterInfo (ArchReg arch) =>
BlockStartStackConstraints arch
fnEntryBlockStartStackConstraints
                 , initRngPredMap :: BlockStartRangePred arch
initRngPredMap = BlockStartRangePred arch
forall (r :: Type -> Type) (v :: Type -> Type). LocMap r v
locMapEmpty
                 , initAddrPredMap :: Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
initAddrPredMap = Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
forall k a. Map k a
Map.empty
                 }

-- | Return a jump bounds that implies both input bounds, or `Nothing`
-- if every fact in the old bounds is implied by the new bounds.
joinInitialBounds :: forall arch
                  .  ( MemWidth (ArchAddrWidth arch)
                     , OrdF (ArchReg arch)
                     , HasRepr (ArchReg arch) TypeRepr
                     )
                  => InitJumpBounds arch
                  -> InitJumpBounds arch
                  -> Maybe (InitJumpBounds arch)
joinInitialBounds :: forall arch.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 HasRepr (ArchReg arch) TypeRepr) =>
InitJumpBounds arch
-> InitJumpBounds arch -> Maybe (InitJumpBounds arch)
joinInitialBounds InitJumpBounds arch
old InitJumpBounds arch
new = (forall s. Changed s (InitJumpBounds arch))
-> Maybe (InitJumpBounds arch)
forall a. (forall s. Changed s a) -> Maybe a
runChanged ((forall s. Changed s (InitJumpBounds arch))
 -> Maybe (InitJumpBounds arch))
-> (forall s. Changed s (InitJumpBounds arch))
-> Maybe (InitJumpBounds arch)
forall a b. (a -> b) -> a -> b
$ do
  (BlockStartStackConstraints arch
finalStkCns, JoinClassMap (ArchReg arch)
_) <- BlockStartStackConstraints arch
-> BlockStartStackConstraints arch
-> Changed
     s (BlockStartStackConstraints arch, JoinClassMap (ArchReg arch))
forall arch s.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 HasRepr (ArchReg arch) TypeRepr) =>
BlockStartStackConstraints arch
-> BlockStartStackConstraints arch
-> Changed
     s (BlockStartStackConstraints arch, JoinClassMap (ArchReg arch))
joinBlockStartStackConstraints (InitJumpBounds arch -> BlockStartStackConstraints arch
forall arch. InitJumpBounds arch -> BlockStartStackConstraints arch
initBndsMap InitJumpBounds arch
old) (InitJumpBounds arch -> BlockStartStackConstraints arch
forall arch. InitJumpBounds arch -> BlockStartStackConstraints arch
initBndsMap InitJumpBounds arch
new)
  Bool -> Changed s () -> Changed s ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (LocMap (ArchReg arch) SubRange -> Bool
forall (r :: Type -> Type) (v :: Type -> Type). LocMap r v -> Bool
locMapNull (InitJumpBounds arch -> LocMap (ArchReg arch) SubRange
forall arch. InitJumpBounds arch -> BlockStartRangePred arch
initRngPredMap InitJumpBounds arch
old) Bool -> Bool -> Bool
&& Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange) -> Bool
forall k a. Map k a -> Bool
Map.null (InitJumpBounds arch
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
forall arch.
InitJumpBounds arch
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
initAddrPredMap InitJumpBounds arch
old)) (Changed s () -> Changed s ()) -> Changed s () -> Changed s ()
forall a b. (a -> b) -> a -> b
$ Bool -> Changed s ()
forall s. Bool -> Changed s ()
markChanged Bool
True
  InitJumpBounds arch -> Changed s (InitJumpBounds arch)
forall a. a -> Changed s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (InitJumpBounds arch -> Changed s (InitJumpBounds arch))
-> InitJumpBounds arch -> Changed s (InitJumpBounds arch)
forall a b. (a -> b) -> a -> b
$! InitJumpBounds { initBndsMap :: BlockStartStackConstraints arch
initBndsMap = BlockStartStackConstraints arch
finalStkCns
                         , initRngPredMap :: LocMap (ArchReg arch) SubRange
initRngPredMap = LocMap (ArchReg arch) SubRange
forall (r :: Type -> Type) (v :: Type -> Type). LocMap r v
locMapEmpty
                         , initAddrPredMap :: Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
initAddrPredMap = Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
forall k a. Map k a
Map.empty
                         }

------------------------------------------------------------------------
-- IntraJumpBounds

-- | This tracks bounds on a block during execution.
data IntraJumpBounds arch ids
   = IntraJumpBounds { forall arch ids. IntraJumpBounds arch ids -> InitJumpBounds arch
intraInitBounds :: !(InitJumpBounds arch)
                     , forall arch ids.
IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
intraStackConstraints :: !(BlockIntraStackConstraints arch ids)
                     , forall arch ids.
IntraJumpBounds arch ids -> MapF (AssignId ids) SubRange
intraReadPredMap :: !(MapF (AssignId ids) SubRange)
                       -- ^ Map from assignments (that are memory
                       -- reads) and any range predicate inferred on
                       -- that access.
                       --
                       -- Used so we can eagerly compute range predicate.
                     , forall arch ids. IntraJumpBounds arch ids -> Bool
intraMemCleared :: !Bool
                       -- ^ Flag to indicate if we had any memory
                       -- writes in block that could have altered
                       -- invariants on non-stack memory accesses.
                     }

-- | Create index bounds from initial index bounds.
mkIntraJumpBounds :: forall arch ids
                  .  (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch))
                  => InitJumpBounds arch
                  -> IntraJumpBounds arch ids
mkIntraJumpBounds :: forall arch ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
InitJumpBounds arch -> IntraJumpBounds arch ids
mkIntraJumpBounds InitJumpBounds arch
bnds =
  IntraJumpBounds { intraInitBounds :: InitJumpBounds arch
intraInitBounds = InitJumpBounds arch
bnds
                  , intraStackConstraints :: BlockIntraStackConstraints arch ids
intraStackConstraints = BlockStartStackConstraints arch
-> BlockIntraStackConstraints arch ids
forall arch ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BlockIntraStackConstraints arch ids
mkBlockIntraStackConstraints (InitJumpBounds arch -> BlockStartStackConstraints arch
forall arch. InitJumpBounds arch -> BlockStartStackConstraints arch
initBndsMap InitJumpBounds arch
bnds)
                  , intraReadPredMap :: MapF (AssignId ids) SubRange
intraReadPredMap = MapF (AssignId ids) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
                  , intraMemCleared :: Bool
intraMemCleared = Bool
False
                  }

instance ShowF (ArchReg arch) => Pretty (IntraJumpBounds arch ids) where
  pretty :: forall ann. IntraJumpBounds arch ids -> Doc ann
pretty IntraJumpBounds arch ids
cns = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$
    BlockStartStackConstraints arch -> [Doc ann]
forall arch ann.
ShowF (ArchReg arch) =>
BlockStartStackConstraints arch -> [Doc ann]
ppBlockStartStackConstraints (BlockIntraStackConstraints arch ids
-> BlockStartStackConstraints arch
forall arch ids.
BlockIntraStackConstraints arch ids
-> BlockStartStackConstraints arch
biscInitConstraints (IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
forall arch ids.
IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
intraStackConstraints IntraJumpBounds arch ids
cns))

-- | Update the stack constraints in the bounds.
modifyIntraStackConstraints ::IntraJumpBounds arch ids
                           ->  (BlockIntraStackConstraints arch ids -> BlockIntraStackConstraints arch ids)
                           -> IntraJumpBounds arch ids
modifyIntraStackConstraints :: forall arch ids.
IntraJumpBounds arch ids
-> (BlockIntraStackConstraints arch ids
    -> BlockIntraStackConstraints arch ids)
-> IntraJumpBounds arch ids
modifyIntraStackConstraints IntraJumpBounds arch ids
bnds BlockIntraStackConstraints arch ids
-> BlockIntraStackConstraints arch ids
f = IntraJumpBounds arch ids
bnds { intraStackConstraints = f (intraStackConstraints bnds) }

discardMemBounds :: IntraJumpBounds arch ids -> IntraJumpBounds arch ids
discardMemBounds :: forall arch ids.
IntraJumpBounds arch ids -> IntraJumpBounds arch ids
discardMemBounds IntraJumpBounds arch ids
bnds =
  IntraJumpBounds arch ids
bnds { intraStackConstraints = discardMemInfo (intraStackConstraints bnds)
       , intraMemCleared = True
       }

------------------------------------------------------------------------
-- Execute a statement

-- | Function that determines whether it thinks an
-- architecture-specific function could modify stack.
--
-- Uses principal that architecture-specific functions can only depend
-- on value if they reference it in their foldable instance.
archFnCouldAffectStack :: forall f arch ids tp
                       .  (FoldableFC f, MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch))
                       => BlockIntraStackConstraints arch ids
                       -> f (Value arch ids) tp
                       -> Bool
archFnCouldAffectStack :: forall {l} (f :: (Type -> Type) -> l -> Type) arch ids (tp :: l).
(FoldableFC f, MemWidth (ArchAddrWidth arch),
 OrdF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> f (Value arch ids) tp -> Bool
archFnCouldAffectStack BlockIntraStackConstraints arch ids
cns = Any -> Bool
getAny (Any -> Bool)
-> (f (Value arch ids) tp -> Any) -> f (Value arch ids) tp -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: Type). Value arch ids x -> Any)
-> forall (x :: l). f (Value arch ids) x -> Any
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) m.
(FoldableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
forall (f :: Type -> Type) m.
Monoid m =>
(forall (x :: Type). f x -> m) -> forall (x :: l). f f x -> m
foldMapFC (Bool -> Any
Any (Bool -> Any)
-> (Value arch ids x -> Bool) -> Value arch ids x -> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value arch ids x -> Bool
forall (utp :: Type). Value arch ids utp -> Bool
refStack)
  where refStack :: Value arch ids utp -> Bool
        refStack :: forall (utp :: Type). Value arch ids utp -> Bool
refStack Value arch ids utp
v =
          case BlockIntraStackConstraints arch ids
-> Value arch ids utp -> StackExpr arch ids utp
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> Value arch ids tp -> StackExpr arch ids tp
intraStackValueExpr BlockIntraStackConstraints arch ids
cns Value arch ids utp
v of
            StackOffsetExpr MemInt (ArchAddrWidth arch)
_ -> Bool
True
            StackExpr arch ids utp
_ -> Bool
False

-- | Given a statement this modifies the bounds based on the statement.
execStatement :: ( MemWidth (ArchAddrWidth arch)
                 , OrdF (ArchReg arch)
                 , ShowF (ArchReg arch)
                 , FoldableFC (ArchFn arch)
                 )
              => IntraJumpBounds arch ids
              -> Stmt arch ids
              -> IntraJumpBounds arch ids
execStatement :: forall arch ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 ShowF (ArchReg arch), FoldableFC (ArchFn arch)) =>
IntraJumpBounds arch ids
-> Stmt arch ids -> IntraJumpBounds arch ids
execStatement IntraJumpBounds arch ids
bnds Stmt arch ids
stmt =
  case Stmt arch ids
stmt of
    AssignStmt (Assignment AssignId ids tp
aid AssignRhs arch (Value arch ids) tp
arhs) -> do
      let bnds1 :: IntraJumpBounds arch ids
bnds1 = case AssignRhs arch (Value arch ids) tp
arhs of
                    ReadMem Value arch ids (BVType (ArchAddrWidth arch))
addrVal MemRepr tp
readRepr
                      | Bool
False <- IntraJumpBounds arch ids -> Bool
forall arch ids. IntraJumpBounds arch ids -> Bool
intraMemCleared IntraJumpBounds arch ids
bnds
                      , Just MemAddr (ArchAddrWidth arch)
addr <- Value arch ids (BVType (ArchAddrWidth arch))
-> Maybe (MemAddr (ArchAddrWidth arch))
forall arch ids.
MemWidth (ArchAddrWidth arch) =>
BVValue arch ids (ArchAddrWidth arch) -> Maybe (ArchMemAddr arch)
valueAsMemAddr Value arch ids (BVType (ArchAddrWidth arch))
addrVal
                      , Just (MemVal MemRepr tp
bndRepr SubRange tp
bnd)  <- MemAddr (ArchAddrWidth arch)
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
-> Maybe (MemVal SubRange)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup MemAddr (ArchAddrWidth arch)
addr (InitJumpBounds arch
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
forall arch.
InitJumpBounds arch
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
initAddrPredMap (IntraJumpBounds arch ids -> InitJumpBounds arch
forall arch ids. IntraJumpBounds arch ids -> InitJumpBounds arch
intraInitBounds IntraJumpBounds arch ids
bnds))
                      , Just tp :~: tp
Refl <- MemRepr tp -> MemRepr tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
MemRepr a -> MemRepr b -> Maybe (a :~: b)
testEquality MemRepr tp
readRepr MemRepr tp
bndRepr ->
                        IntraJumpBounds arch ids
bnds { intraReadPredMap = MapF.insert aid bnd (intraReadPredMap bnds) }
                    -- Clear all knowledge about the stack on architecture-specific
                    -- functions that accept stack pointer as they may have side effects.
                    --
                    -- Note. This is very conservative, and we may need to improve
                    -- this.
                    EvalArchFn ArchFn arch (Value arch ids) tp
f TypeRepr tp
_ ->
                      if BlockIntraStackConstraints arch ids
-> ArchFn arch (Value arch ids) tp -> Bool
forall {l} (f :: (Type -> Type) -> l -> Type) arch ids (tp :: l).
(FoldableFC f, MemWidth (ArchAddrWidth arch),
 OrdF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> f (Value arch ids) tp -> Bool
archFnCouldAffectStack (IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
forall arch ids.
IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
intraStackConstraints IntraJumpBounds arch ids
bnds) ArchFn arch (Value arch ids) tp
f then
                        IntraJumpBounds arch ids -> IntraJumpBounds arch ids
forall arch ids.
IntraJumpBounds arch ids -> IntraJumpBounds arch ids
discardMemBounds IntraJumpBounds arch ids
bnds
                       else
                        IntraJumpBounds arch ids
bnds { intraMemCleared = True }
                    AssignRhs arch (Value arch ids) tp
_ -> IntraJumpBounds arch ids
bnds
      -- Associate the given expression with a bounds.
       in IntraJumpBounds arch ids
-> (BlockIntraStackConstraints arch ids
    -> BlockIntraStackConstraints arch ids)
-> IntraJumpBounds arch ids
forall arch ids.
IntraJumpBounds arch ids
-> (BlockIntraStackConstraints arch ids
    -> BlockIntraStackConstraints arch ids)
-> IntraJumpBounds arch ids
modifyIntraStackConstraints IntraJumpBounds arch ids
bnds1 ((BlockIntraStackConstraints arch ids
  -> BlockIntraStackConstraints arch ids)
 -> IntraJumpBounds arch ids)
-> (BlockIntraStackConstraints arch ids
    -> BlockIntraStackConstraints arch ids)
-> IntraJumpBounds arch ids
forall a b. (a -> b) -> a -> b
$ \BlockIntraStackConstraints arch ids
cns ->
                    AssignId ids tp
-> StackExpr arch ids tp
-> BlockIntraStackConstraints arch ids
-> BlockIntraStackConstraints arch ids
forall ids (tp :: Type) arch.
AssignId ids tp
-> StackExpr arch ids tp
-> BlockIntraStackConstraints arch ids
-> BlockIntraStackConstraints arch ids
intraStackSetAssignId AssignId ids tp
aid (BlockIntraStackConstraints arch ids
-> AssignId ids tp
-> AssignRhs arch (Value arch ids) tp
-> StackExpr arch ids tp
forall arch ids (tp :: Type).
(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
intraStackRhsExpr BlockIntraStackConstraints arch ids
cns AssignId ids tp
aid AssignRhs arch (Value arch ids) tp
arhs) BlockIntraStackConstraints arch ids
cns
    WriteMem Value arch ids (BVType (ArchAddrWidth arch))
addr MemRepr tp
repr Value arch ids tp
val ->
      case BlockIntraStackConstraints arch ids
-> Value arch ids (BVType (ArchAddrWidth arch))
-> StackExpr arch ids (BVType (ArchAddrWidth arch))
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> Value arch ids tp -> StackExpr arch ids tp
intraStackValueExpr (IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
forall arch ids.
IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
intraStackConstraints IntraJumpBounds arch ids
bnds) Value arch ids (BVType (ArchAddrWidth arch))
addr of
        StackOffsetExpr MemInt (ArchAddrWidth arch)
addrOff ->
          IntraJumpBounds arch ids
-> (BlockIntraStackConstraints arch ids
    -> BlockIntraStackConstraints arch ids)
-> IntraJumpBounds arch ids
forall arch ids.
IntraJumpBounds arch ids
-> (BlockIntraStackConstraints arch ids
    -> BlockIntraStackConstraints arch ids)
-> IntraJumpBounds arch ids
modifyIntraStackConstraints IntraJumpBounds arch ids
bnds ((BlockIntraStackConstraints arch ids
  -> BlockIntraStackConstraints arch ids)
 -> IntraJumpBounds arch ids)
-> (BlockIntraStackConstraints arch ids
    -> BlockIntraStackConstraints arch ids)
-> IntraJumpBounds arch ids
forall a b. (a -> b) -> a -> b
$ \BlockIntraStackConstraints arch ids
cns ->
            BlockIntraStackConstraints arch ids
-> MemInt (ArchAddrWidth arch)
-> MemRepr tp
-> Value arch ids tp
-> BlockIntraStackConstraints arch ids
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> MemInt (ArchAddrWidth arch)
-> MemRepr tp
-> Value arch ids tp
-> BlockIntraStackConstraints arch ids
writeStackOff BlockIntraStackConstraints arch ids
cns MemInt (ArchAddrWidth arch)
addrOff MemRepr tp
repr Value arch ids tp
val
        -- If we write to something other than stack, then clear all
        -- stack references.
        --
        -- This is probably not a good idea in general, but seems fine
        -- for stack detection.
        StackExpr arch ids (BVType (ArchAddrWidth arch))
_ -> IntraJumpBounds arch ids -> IntraJumpBounds arch ids
forall arch ids.
IntraJumpBounds arch ids -> IntraJumpBounds arch ids
discardMemBounds IntraJumpBounds arch ids
bnds
    CondWriteMem{} -> IntraJumpBounds arch ids -> IntraJumpBounds arch ids
forall arch ids.
IntraJumpBounds arch ids -> IntraJumpBounds arch ids
discardMemBounds IntraJumpBounds arch ids
bnds
    InstructionStart{} -> IntraJumpBounds arch ids
bnds
    Comment{} -> IntraJumpBounds arch ids
bnds
    ExecArchStmt{} -> IntraJumpBounds arch ids -> IntraJumpBounds arch ids
forall arch ids.
IntraJumpBounds arch ids -> IntraJumpBounds arch ids
discardMemBounds IntraJumpBounds arch ids
bnds
    ArchState{} -> IntraJumpBounds arch ids
bnds

-- | Create bounds for end of block.
blockEndBounds :: ( MemWidth (ArchAddrWidth arch)
                  , OrdF (ArchReg arch)
                  , ShowF (ArchReg arch)
                  , FoldableFC (ArchFn arch)
                  )
               => InitJumpBounds arch
               -> [Stmt arch ids] -- ^
               -> IntraJumpBounds arch ids
blockEndBounds :: forall arch ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 ShowF (ArchReg arch), FoldableFC (ArchFn arch)) =>
InitJumpBounds arch -> [Stmt arch ids] -> IntraJumpBounds arch ids
blockEndBounds InitJumpBounds arch
blockBnds [Stmt arch ids]
stmts =
   (IntraJumpBounds arch ids
 -> Stmt arch ids -> IntraJumpBounds arch ids)
-> IntraJumpBounds arch ids
-> [Stmt arch ids]
-> IntraJumpBounds arch ids
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' IntraJumpBounds arch ids
-> Stmt arch ids -> IntraJumpBounds arch ids
forall arch ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 ShowF (ArchReg arch), FoldableFC (ArchFn arch)) =>
IntraJumpBounds arch ids
-> Stmt arch ids -> IntraJumpBounds arch ids
execStatement (InitJumpBounds arch -> IntraJumpBounds arch ids
forall arch ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
InitJumpBounds arch -> IntraJumpBounds arch ids
mkIntraJumpBounds InitJumpBounds arch
blockBnds) [Stmt arch ids]
stmts

------------------------------------------------------------------------
-- Operations

-- | Bounds for a function as the start of a block.
data ExprRangePredInfo arch ids =
  ExprRangePredInfo { forall arch ids.
ExprRangePredInfo arch ids -> BlockStartStackConstraints arch
erpiBndsMap    :: !(BlockStartStackConstraints arch)
                    , forall arch ids.
ExprRangePredInfo arch ids -> BlockStartRangePred arch
erpiRngPredMap :: !(BlockStartRangePred arch)
                    , forall arch ids.
ExprRangePredInfo arch ids -> MapF (AssignId ids) SubRange
erpiReadPredMap ::  !(MapF (AssignId ids) SubRange)
                    , forall arch ids.
ExprRangePredInfo arch ids -> BranchConstraints arch ids
erpiBranchConstraints :: !(BranchConstraints arch ids)
                    }

-- | This returns the current predicate on the bound expression.
exprRangePred :: ( MemWidth (ArchAddrWidth arch)
                 , HasRepr (ArchReg arch) TypeRepr
                 , OrdF (ArchReg arch)
                 , ShowF (ArchReg arch)
                 )
              => ExprRangePredInfo arch ids
              -> StackExpr arch ids tp
              -> MaybeRangePred tp
exprRangePred :: forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
ExprRangePredInfo arch ids
-> StackExpr arch ids tp -> MaybeRangePred tp
exprRangePred ExprRangePredInfo arch ids
info StackExpr arch ids tp
e = do
  let brCns :: BranchConstraints arch ids
brCns = ExprRangePredInfo arch ids -> BranchConstraints arch ids
forall arch ids.
ExprRangePredInfo arch ids -> BranchConstraints arch ids
erpiBranchConstraints ExprRangePredInfo arch ids
info
  case StackExpr arch ids tp
e of
    ClassRepExpr BoundLoc (ArchReg arch) tp
loc ->
      case BoundLoc (ArchReg arch) tp
-> MapF (BoundLoc (ArchReg arch)) SubRange -> Maybe (SubRange tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup BoundLoc (ArchReg arch) tp
loc (BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
forall arch ids.
BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints BranchConstraints arch ids
brCns) of
        Just (SubRange RangePred u
r) -> RangePred u -> MaybeRangePred ('BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred RangePred u
r
        Maybe (SubRange tp)
Nothing ->
          case BoundLoc (ArchReg arch) tp
-> LocMap (ArchReg arch) SubRange -> Maybe (SubRange tp)
forall (r :: Type -> Type) (tp :: Type) (v :: Type -> Type).
(MemWidth (RegAddrWidth r), OrdF r) =>
BoundLoc r tp -> LocMap r v -> Maybe (v tp)
locLookup BoundLoc (ArchReg arch) tp
loc (ExprRangePredInfo arch ids -> LocMap (ArchReg arch) SubRange
forall arch ids.
ExprRangePredInfo arch ids -> BlockStartRangePred arch
erpiRngPredMap ExprRangePredInfo arch ids
info) of
            Maybe (SubRange tp)
Nothing ->  MaybeRangePred tp
forall (tp :: Type). MaybeRangePred tp
NoRangePred
            Just (SubRange RangePred u
r) -> RangePred u -> MaybeRangePred ('BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred RangePred u
r
    UninterpAssignExpr AssignId ids tp
aid AssignRhs arch (Value arch ids) tp
_
      -- Lookup range predicate in newly asserted conditions
      | Just (SubRange RangePred u
r) <-  AssignId ids tp
-> MapF (AssignId ids) SubRange -> Maybe (SubRange tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup AssignId ids tp
aid (BranchConstraints arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
BranchConstraints arch ids -> MapF (AssignId ids) SubRange
newUninterpAssignConstraints BranchConstraints arch ids
brCns)
      , RangePred u -> Bool
forall (u :: Nat). RangePred u -> Bool
rangeNotTotal RangePred u
r ->
        RangePred u -> MaybeRangePred ('BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred RangePred u
r
      -- Otherwise lookup range predicate for memory reads from block start
      | Just (SubRange RangePred u
r) <- AssignId ids tp
-> MapF (AssignId ids) SubRange -> Maybe (SubRange tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup AssignId ids tp
aid (ExprRangePredInfo arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
ExprRangePredInfo arch ids -> MapF (AssignId ids) SubRange
erpiReadPredMap ExprRangePredInfo arch ids
info)
      , RangePred u -> Bool
forall (u :: Nat). RangePred u -> Bool
rangeNotTotal RangePred u
r -> do
          RangePred u -> MaybeRangePred ('BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred RangePred u
r
      | Bool
otherwise ->
        MaybeRangePred tp
forall (tp :: Type). MaybeRangePred tp
NoRangePred
    StackOffsetExpr MemInt (ArchAddrWidth arch)
_ -> MaybeRangePred tp
forall (tp :: Type). MaybeRangePred tp
NoRangePred
    CExpr (BVCValue NatRepr n
w Integer
i) -> RangePred n -> MaybeRangePred ('BVType n)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred (NatRepr n -> Nat -> Nat -> RangePred n
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
mkRangeBound NatRepr n
w (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger Integer
i) (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger Integer
i))
    CExpr CValue arch tp
_ -> MaybeRangePred tp
forall (tp :: Type). MaybeRangePred tp
NoRangePred
    AppExpr AssignId ids tp
n App (StackExpr arch ids) tp
_app
      -- If a bound has been deliberately asserted to this assignment
      -- then use that.
      | Just (SubRange RangePred u
r) <- AssignId ids tp
-> MapF (AssignId ids) SubRange -> Maybe (SubRange tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup AssignId ids tp
n (BranchConstraints arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
BranchConstraints arch ids -> MapF (AssignId ids) SubRange
newUninterpAssignConstraints BranchConstraints arch ids
brCns)
      , RangePred u -> Bool
forall (u :: Nat). RangePred u -> Bool
rangeNotTotal RangePred u
r ->
          RangePred u -> MaybeRangePred ('BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred RangePred u
r
    -- Otherwise see what we can infer.
    UExtExpr StackExpr arch ids (BVType u)
x NatRepr w
w ->
      case ExprRangePredInfo arch ids
-> StackExpr arch ids (BVType u) -> MaybeRangePred (BVType u)
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
ExprRangePredInfo arch ids
-> StackExpr arch ids tp -> MaybeRangePred tp
exprRangePred ExprRangePredInfo arch ids
info StackExpr arch ids (BVType u)
x of
        MaybeRangePred (BVType u)
NoRangePred -> RangePred w -> MaybeRangePred ('BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred (NatRepr w -> Nat -> Nat -> RangePred w
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
mkRangeBound NatRepr w
w Nat
0 (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w)))
        SomeRangePred RangePred u
r ->
          -- 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
          if NatRepr u -> NatRepr u -> Bool
forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> Bool
leqF (StackExpr arch ids (BVType u) -> NatRepr u
forall (f :: Type -> Type) (w :: Nat).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth StackExpr arch ids (BVType u)
x) (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
r) then
            RangePred w -> MaybeRangePred ('BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred (NatRepr w -> Nat -> Nat -> RangePred w
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
mkRangeBound NatRepr w
w (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeLowerBound RangePred u
r) (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
r))
           else
            -- Dynamic check on range width that should never fail.
            case NatRepr u -> NatRepr w -> Maybe (LeqProof u w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
r) NatRepr w
w of
              Just LeqProof u w
LeqProof -> RangePred u -> MaybeRangePred ('BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred RangePred u
r
              Maybe (LeqProof u w)
Nothing -> String -> MaybeRangePred tp
forall a. HasCallStack => String -> a
error String
"exprRangePred given malformed app."
    AppExpr AssignId ids tp
_n App (StackExpr arch ids) tp
app ->
      case App (StackExpr arch ids) tp
app of
        UExt StackExpr arch ids (BVType m)
x NatRepr n
w
          | SomeRangePred RangePred u
r <- ExprRangePredInfo arch ids
-> StackExpr arch ids (BVType m) -> MaybeRangePred (BVType m)
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
ExprRangePredInfo arch ids
-> StackExpr arch ids tp -> MaybeRangePred tp
exprRangePred ExprRangePredInfo arch ids
info StackExpr arch ids (BVType m)
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 NatRepr u -> NatRepr m -> Maybe (u :~: m)
forall (a :: Nat) (b :: Nat).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
r) (StackExpr arch ids (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Nat).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth StackExpr arch ids (BVType m)
x) of
                Just u :~: m
Refl ->
                  RangePred n -> MaybeRangePred ('BVType n)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred (NatRepr n -> Nat -> Nat -> RangePred n
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
mkRangeBound NatRepr n
w (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeLowerBound RangePred u
r) (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
r))
                Maybe (u :~: m)
Nothing ->
                  -- Dynamic check on range width that should never fail.
                  case NatRepr u -> NatRepr n -> Maybe (LeqProof u n)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
r) NatRepr n
w of
                    Just LeqProof u n
LeqProof -> RangePred u -> MaybeRangePred ('BVType n)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred RangePred u
r
                    Maybe (LeqProof u n)
Nothing -> String -> MaybeRangePred tp
forall a. HasCallStack => String -> a
error String
"exprRangePred given malformed app."
        BVAdd NatRepr n
_ StackExpr arch ids ('BVType n)
x (CExpr (BVCValue NatRepr n
_ Integer
c))
          | SomeRangePred RangePred u
r <- ExprRangePredInfo arch ids
-> StackExpr arch ids ('BVType n) -> MaybeRangePred ('BVType n)
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
ExprRangePredInfo arch ids
-> StackExpr arch ids tp -> MaybeRangePred tp
exprRangePred ExprRangePredInfo arch ids
info StackExpr arch ids ('BVType n)
x
          , NatRepr u
w <- RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
r
          , Nat
lr <- RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeLowerBound RangePred u
r Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr u -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w Integer
c)
          , Nat
ur <- RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
r Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr u -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w Integer
c)
          , Nat
lr Nat -> Int -> Nat
forall a. Bits a => a -> Int -> a
`shiftR` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatRepr u -> Nat
forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr u
w) Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
ur Nat -> Int -> Nat
forall a. Bits a => a -> Int -> a
`shiftR` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatRepr u -> Nat
forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr u
w)
          , Nat
lr' <- Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr u -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w (Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
lr))
          , Nat
ur' <- Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr u -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w (Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
ur)) ->
            RangePred u -> MaybeRangePred ('BVType n)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred (NatRepr u -> Nat -> Nat -> RangePred u
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
RangePred NatRepr u
w Nat
lr' Nat
ur')
        Trunc StackExpr arch ids (BVType m)
x NatRepr n
w
          | SomeRangePred RangePred u
r <- ExprRangePredInfo arch ids
-> StackExpr arch ids (BVType m) -> MaybeRangePred (BVType m)
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
ExprRangePredInfo arch ids
-> StackExpr arch ids tp -> MaybeRangePred tp
exprRangePred ExprRangePredInfo arch ids
info StackExpr arch ids (BVType m)
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.
          -> case NatRepr u -> NatRepr n -> Maybe (LeqProof u n)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
r) NatRepr n
w of
              Just LeqProof u n
LeqProof -> RangePred u -> MaybeRangePred ('BVType n)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred RangePred u
r

              -- Otherwise, we need to rewrite the constraints to be on w bits.
              -- We can do that by clamping the lower/upper bounds if they're
              -- outside of the range [0, 2^w-1].
              Maybe (LeqProof u n)
Nothing ->
                let
                  truncUnsigned :: Natural -> Natural
                  truncUnsigned :: Nat -> Nat
truncUnsigned = Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (Integer -> Nat) -> (Nat -> Integer) -> Nat -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
unsignedClamp NatRepr n
w (Integer -> Integer) -> (Nat -> Integer) -> Nat -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a. Integral a => a -> Integer
toInteger

                  lowerBound :: Nat
lowerBound = Nat -> Nat
truncUnsigned (Nat -> Nat) -> Nat -> Nat
forall a b. (a -> b) -> a -> b
$ RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeLowerBound RangePred u
r
                  upperBound :: Nat
upperBound = Nat -> Nat
truncUnsigned (Nat -> Nat) -> Nat -> Nat
forall a b. (a -> b) -> a -> b
$ RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
r
                in
                  RangePred n -> MaybeRangePred ('BVType n)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> MaybeRangePred (BVType w)
SomeRangePred (NatRepr n -> Nat -> Nat -> RangePred n
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
mkRangeBound NatRepr n
w Nat
lowerBound Nat
upperBound)
        App (StackExpr arch ids) tp
_ -> MaybeRangePred tp
forall (tp :: Type). MaybeRangePred tp
NoRangePred

-- | This returns a natural number with a computed upper bound for the
-- value or `Nothing` if no explicit bound was inferred.
unsignedUpperBound :: ( MapF.OrdF (ArchReg arch)
                      , MapF.ShowF (ArchReg arch)
                      , RegisterInfo (ArchReg arch)
                      )
                   => IntraJumpBounds arch ids
                   -> Value arch ids tp
                   -> Maybe Natural
unsignedUpperBound :: forall arch ids (tp :: Type).
(OrdF (ArchReg arch), ShowF (ArchReg arch),
 RegisterInfo (ArchReg arch)) =>
IntraJumpBounds arch ids -> Value arch ids tp -> Maybe Nat
unsignedUpperBound IntraJumpBounds arch ids
bnds Value arch ids tp
v = do
  let ibnds :: InitJumpBounds arch
ibnds = IntraJumpBounds arch ids -> InitJumpBounds arch
forall arch ids. IntraJumpBounds arch ids -> InitJumpBounds arch
intraInitBounds IntraJumpBounds arch ids
bnds
  let stkCns :: BlockIntraStackConstraints arch ids
stkCns = IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
forall arch ids.
IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
intraStackConstraints IntraJumpBounds arch ids
bnds
  let valExpr :: StackExpr arch ids tp
valExpr = BlockIntraStackConstraints arch ids
-> Value arch ids tp -> StackExpr arch ids tp
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> Value arch ids tp -> StackExpr arch ids tp
intraStackValueExpr BlockIntraStackConstraints arch ids
stkCns Value arch ids tp
v
  let info :: ExprRangePredInfo arch ids
info =   ExprRangePredInfo { erpiBndsMap :: BlockStartStackConstraints arch
erpiBndsMap      =  BlockIntraStackConstraints arch ids
-> BlockStartStackConstraints arch
forall arch ids.
BlockIntraStackConstraints arch ids
-> BlockStartStackConstraints arch
biscInitConstraints BlockIntraStackConstraints arch ids
stkCns
                                 , erpiRngPredMap :: BlockStartRangePred arch
erpiRngPredMap   = InitJumpBounds arch -> BlockStartRangePred arch
forall arch. InitJumpBounds arch -> BlockStartRangePred arch
initRngPredMap InitJumpBounds arch
ibnds
                                 , erpiReadPredMap :: MapF (AssignId ids) SubRange
erpiReadPredMap  = IntraJumpBounds arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
IntraJumpBounds arch ids -> MapF (AssignId ids) SubRange
intraReadPredMap IntraJumpBounds arch ids
bnds
                                 , erpiBranchConstraints :: BranchConstraints arch ids
erpiBranchConstraints = BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints
                                 }
  case ExprRangePredInfo arch ids
-> StackExpr arch ids tp -> MaybeRangePred tp
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
ExprRangePredInfo arch ids
-> StackExpr arch ids tp -> MaybeRangePred tp
exprRangePred ExprRangePredInfo arch ids
info StackExpr arch ids tp
valExpr of
    SomeRangePred RangePred u
r -> do
      u :~: v
Refl <- NatRepr u -> NatRepr v -> Maybe (u :~: v)
forall (a :: Nat) (b :: Nat).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
r) (Value arch ids ('BVType v) -> NatRepr v
forall (f :: Type -> Type) (w :: Nat).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth Value arch ids tp
Value arch ids ('BVType v)
v)
      Nat -> Maybe Nat
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
r)
    MaybeRangePred tp
NoRangePred -> Maybe Nat
forall a. Maybe a
Nothing

------------------------------------------------------------------------
-- SubRange

-- | This indicates a range predicate on a selected number of bits.
data SubRange tp where
  SubRange :: (u <= w) => !(RangePred u) -> SubRange (BVType w)

instance Pretty (SubRange tp) where
  pretty :: forall ann. SubRange tp -> Doc ann
pretty (SubRange RangePred u
p) = RangePred u -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. RangePred u -> Doc ann
pretty RangePred u
p

ppSubRange :: Doc ann -> SubRange tp -> Doc ann
ppSubRange :: forall ann (tp :: Type). Doc ann -> SubRange tp -> Doc ann
ppSubRange Doc ann
d (SubRange RangePred u
r) = Doc ann
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> RangePred u -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. RangePred u -> Doc ann
pretty RangePred u
r

-- | Take the union of two subranges, and return `Nothing` if this is
-- a maximum range bound.
disjoinRangePred :: RangePred u -> RangePred u -> Maybe (RangePred u)
disjoinRangePred :: forall (u :: Nat).
RangePred u -> RangePred u -> Maybe (RangePred u)
disjoinRangePred RangePred u
x RangePred u
y
    | Nat
l Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
0 Bool -> Bool -> Bool
|| Nat
h Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr u -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr u
w) = RangePred u -> Maybe (RangePred u)
forall a. a -> Maybe a
Just (NatRepr u -> Nat -> Nat -> RangePred u
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
mkRangeBound NatRepr u
w Nat
l Nat
h)
    | Bool
otherwise = Maybe (RangePred u)
forall a. Maybe a
Nothing
  where w :: NatRepr u
w = RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
x
        l :: Nat
l = Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
min (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeLowerBound RangePred u
x) (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeLowerBound RangePred u
y)
        h :: Nat
h = Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
x) (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
y)

-- | Take the union of two subranges.
--
-- Return `Nothing` if range is not value.
disjoinSubRange :: SubRange tp -> SubRange tp -> Maybe (SubRange tp)
disjoinSubRange :: forall (tp :: Type).
SubRange tp -> SubRange tp -> Maybe (SubRange tp)
disjoinSubRange (SubRange RangePred u
x) (SubRange RangePred u
y)
  | Just u :~: u
Refl <- NatRepr u -> NatRepr u -> Maybe (u :~: u)
forall (a :: Nat) (b :: Nat).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
x) (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
y) =
      RangePred u -> SubRange tp
RangePred u -> SubRange ('BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> SubRange (BVType w)
SubRange (RangePred u -> SubRange tp)
-> Maybe (RangePred u) -> Maybe (SubRange tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RangePred u -> RangePred u -> Maybe (RangePred u)
forall (u :: Nat).
RangePred u -> RangePred u -> Maybe (RangePred u)
disjoinRangePred RangePred u
x RangePred u
RangePred u
y
  | Bool
otherwise =
      Maybe (SubRange tp)
forall a. Maybe a
Nothing

------------------------------------------------------------------------
-- BranchConstraints

-- | Constraints on variable ranges inferred from a branch.
--
-- Branches predicates are analyzed to infer the constraints in
-- indices used in jump tables only, and this analysis is based on
-- that.
data BranchConstraints arch ids = BranchConstraints
  { forall arch ids.
BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints :: !(MapF (BoundLoc (ArchReg arch)) SubRange)
    -- ^ Maps locations to constraints on the initial values of
    -- the variable that are inferred from asserted branches.
  , forall arch ids.
BranchConstraints arch ids -> MapF (AssignId ids) SubRange
newUninterpAssignConstraints :: !(MapF (AssignId ids) SubRange)
    -- ^ Maps assignments to inferred subrange constraints on
    -- assignments.
  , forall arch ids.
BranchConstraints arch ids
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints :: !(Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange))
    -- ^ Maps addresses to an inferred subrange constraints on the
    -- value stored at that address.
  }

instance ShowF (ArchReg arch) => Pretty (BranchConstraints arch ids) where
  pretty :: forall ann. BranchConstraints arch ids -> Doc ann
pretty BranchConstraints arch ids
x =
    let cl :: [Pair (BoundLoc (ArchReg arch)) SubRange]
cl = MapF (BoundLoc (ArchReg arch)) SubRange
-> [Pair (BoundLoc (ArchReg arch)) SubRange]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Pair k2 a]
MapF.toList (BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
forall arch ids.
BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints BranchConstraints arch ids
x)
        al :: [Pair (AssignId ids) SubRange]
al = MapF (AssignId ids) SubRange -> [Pair (AssignId ids) SubRange]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Pair k2 a]
MapF.toList (BranchConstraints arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
BranchConstraints arch ids -> MapF (AssignId ids) SubRange
newUninterpAssignConstraints BranchConstraints arch ids
x)
        ppLoc :: Pair (BoundLoc (ArchReg arch)) SubRange -> Doc ann
        ppLoc :: forall ann. Pair (BoundLoc (ArchReg arch)) SubRange -> Doc ann
ppLoc (Pair BoundLoc (ArchReg arch) tp
l SubRange tp
r) = BoundLoc (ArchReg arch) tp -> Doc ann
forall k (f :: k -> Type) (tp :: k) ann.
PrettyF f =>
f tp -> Doc ann
forall (tp :: Type) ann. BoundLoc (ArchReg arch) tp -> Doc ann
prettyF BoundLoc (ArchReg arch) tp
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SubRange tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. SubRange tp -> Doc ann
pretty SubRange tp
r
        ppAssign :: Pair (AssignId ids) SubRange -> Doc ann
        ppAssign :: forall ann. Pair (AssignId ids) SubRange -> Doc ann
ppAssign (Pair AssignId ids tp
l SubRange tp
r) = AssignId ids tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId ids tp
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SubRange tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. SubRange tp -> Doc ann
pretty SubRange tp
r
     in [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ((Pair (BoundLoc (ArchReg arch)) SubRange -> Doc ann)
-> [Pair (BoundLoc (ArchReg arch)) SubRange] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Pair (BoundLoc (ArchReg arch)) SubRange -> Doc ann
forall ann. Pair (BoundLoc (ArchReg arch)) SubRange -> Doc ann
ppLoc [Pair (BoundLoc (ArchReg arch)) SubRange]
cl [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ (Pair (AssignId ids) SubRange -> Doc ann)
-> [Pair (AssignId ids) SubRange] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Pair (AssignId ids) SubRange -> Doc ann
forall ann. Pair (AssignId ids) SubRange -> Doc ann
ppAssign [Pair (AssignId ids) SubRange]
al)

instance ShowF (ArchReg arch) => Show (BranchConstraints arch ids) where
  show :: BranchConstraints arch ids -> String
show BranchConstraints arch ids
x = Doc Any -> String
forall a. Show a => a -> String
show (BranchConstraints arch ids -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. BranchConstraints arch ids -> Doc ann
pretty BranchConstraints arch ids
x)

-- | Empty set of branch constraints.
emptyBranchConstraints :: BranchConstraints arch ids
emptyBranchConstraints :: forall arch ids. BranchConstraints arch ids
emptyBranchConstraints =
  BranchConstraints { newClassRepConstraints :: MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints = MapF (BoundLoc (ArchReg arch)) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
                    , newUninterpAssignConstraints :: MapF (AssignId ids) SubRange
newUninterpAssignConstraints = MapF (AssignId ids) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
                    , newAddrConstraints :: Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints = Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
forall k a. Map k a
Map.empty
                    }

branchLocRangePred :: (u <= w)
                   => BoundLoc (ArchReg arch) (BVType w)
                   -> RangePred u
                   -> BranchConstraints arch ids
branchLocRangePred :: forall (u :: Nat) (w :: Nat) arch ids.
(u <= w) =>
BoundLoc (ArchReg arch) (BVType w)
-> RangePred u -> BranchConstraints arch ids
branchLocRangePred BoundLoc (ArchReg arch) (BVType w)
l RangePred u
p =
  BranchConstraints { newClassRepConstraints :: MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints = BoundLoc (ArchReg arch) (BVType w)
-> SubRange (BVType w) -> MapF (BoundLoc (ArchReg arch)) SubRange
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
k tp -> a tp -> MapF k a
MapF.singleton BoundLoc (ArchReg arch) (BVType w)
l (RangePred u -> SubRange (BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> SubRange (BVType w)
SubRange RangePred u
p)
                    , newUninterpAssignConstraints :: MapF (AssignId ids) SubRange
newUninterpAssignConstraints = MapF (AssignId ids) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
                    , newAddrConstraints :: Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints = Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
forall k a. Map k a
Map.empty
                    }

branchAssignRangePred :: (u <= w)
                      => AssignId ids (BVType w)
                      -> RangePred u
                      -> BranchConstraints arch ids
branchAssignRangePred :: forall (u :: Nat) (w :: Nat) ids arch.
(u <= w) =>
AssignId ids (BVType w)
-> RangePred u -> BranchConstraints arch ids
branchAssignRangePred AssignId ids (BVType w)
a RangePred u
p =
  BranchConstraints { newClassRepConstraints :: MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints = MapF (BoundLoc (ArchReg arch)) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
                    , newUninterpAssignConstraints :: MapF (AssignId ids) SubRange
newUninterpAssignConstraints = AssignId ids (BVType w)
-> SubRange (BVType w) -> MapF (AssignId ids) SubRange
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
k tp -> a tp -> MapF k a
MapF.singleton AssignId ids (BVType w)
a (RangePred u -> SubRange (BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> SubRange (BVType w)
SubRange RangePred u
p)
                    , newAddrConstraints :: Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints = Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
forall k a. Map k a
Map.empty
                    }

-- | Create a predicate on a
branchReadMemRangePred :: (u <= w)
                       => AssignId ids (BVType w)
                       -> MemAddr (ArchAddrWidth arch)
                       -> MemRepr (BVType w)
                       -> RangePred u
                       -> BranchConstraints arch ids
branchReadMemRangePred :: forall (u :: Nat) (w :: Nat) ids arch.
(u <= w) =>
AssignId ids (BVType w)
-> MemAddr (ArchAddrWidth arch)
-> MemRepr (BVType w)
-> RangePred u
-> BranchConstraints arch ids
branchReadMemRangePred AssignId ids (BVType w)
aid MemAddr (ArchAddrWidth arch)
a MemRepr (BVType w)
r RangePred u
p =
  BranchConstraints { newClassRepConstraints :: MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints = MapF (BoundLoc (ArchReg arch)) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
                    , newUninterpAssignConstraints :: MapF (AssignId ids) SubRange
newUninterpAssignConstraints = AssignId ids (BVType w)
-> SubRange (BVType w) -> MapF (AssignId ids) SubRange
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
k tp -> a tp -> MapF k a
MapF.singleton AssignId ids (BVType w)
aid (RangePred u -> SubRange (BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> SubRange (BVType w)
SubRange RangePred u
p)
                    , newAddrConstraints :: Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints = MemAddr (ArchAddrWidth arch)
-> MemVal SubRange
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
forall k a. k -> a -> Map k a
Map.singleton MemAddr (ArchAddrWidth arch)
a (MemRepr (BVType w) -> SubRange (BVType w) -> MemVal SubRange
forall (p :: Type -> Type) (tp :: Type).
MemRepr tp -> p tp -> MemVal p
MemVal MemRepr (BVType w)
r (RangePred u -> SubRange (BVType w)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> SubRange (BVType w)
SubRange RangePred u
p))
                    }

-- | @conjoinBranchConstraints x y@ returns constraints inferred from
-- by @x@ and @y@.
conjoinBranchConstraints :: OrdF (ArchReg arch)
                         => BranchConstraints arch ids
                         -> BranchConstraints arch ids
                         -> BranchConstraints arch ids
conjoinBranchConstraints :: forall arch ids.
OrdF (ArchReg arch) =>
BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
conjoinBranchConstraints BranchConstraints arch ids
x BranchConstraints arch ids
y = do
  BranchConstraints { newClassRepConstraints :: MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints =
                        MapF (BoundLoc (ArchReg arch)) SubRange
-> MapF (BoundLoc (ArchReg arch)) SubRange
-> MapF (BoundLoc (ArchReg arch)) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
MapF k a -> MapF k a -> MapF k a
MapF.union (BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
forall arch ids.
BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints BranchConstraints arch ids
x) (BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
forall arch ids.
BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints BranchConstraints arch ids
y)
                    , newUninterpAssignConstraints :: MapF (AssignId ids) SubRange
newUninterpAssignConstraints =
                        MapF (AssignId ids) SubRange
-> MapF (AssignId ids) SubRange -> MapF (AssignId ids) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
MapF k a -> MapF k a -> MapF k a
MapF.union (BranchConstraints arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
BranchConstraints arch ids -> MapF (AssignId ids) SubRange
newUninterpAssignConstraints BranchConstraints arch ids
x) (BranchConstraints arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
BranchConstraints arch ids -> MapF (AssignId ids) SubRange
newUninterpAssignConstraints BranchConstraints arch ids
y)
                    , newAddrConstraints :: Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
newAddrConstraints = Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (BranchConstraints arch ids
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
forall arch ids.
BranchConstraints arch ids
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints BranchConstraints arch ids
x) (BranchConstraints arch ids
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
forall arch ids.
BranchConstraints arch ids
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints BranchConstraints arch ids
y)
                    }

mapIntersectWithKeyMaybe :: Ord k
                         => (k -> a -> b -> Maybe c)
                         -> Map k a
                         -> Map k b
                         -> Map k c
mapIntersectWithKeyMaybe :: forall k a b c.
Ord k =>
(k -> a -> b -> Maybe c) -> Map k a -> Map k b -> Map k c
mapIntersectWithKeyMaybe k -> a -> b -> Maybe c
f =
  (k -> a -> b -> Maybe c)
-> (Map k a -> Map k c)
-> (Map k b -> Map k c)
-> Map k a
-> Map k b
-> Map k c
forall k a b c.
Ord k =>
(k -> a -> b -> Maybe c)
-> (Map k a -> Map k c)
-> (Map k b -> Map k c)
-> Map k a
-> Map k b
-> Map k c
Map.mergeWithKey k -> a -> b -> Maybe c
f (Map k c -> Map k a -> Map k c
forall a b. a -> b -> a
const Map k c
forall k a. Map k a
Map.empty) (Map k c -> Map k b -> Map k c
forall a b. a -> b -> a
const Map k c
forall k a. Map k a
Map.empty)

-- | @disjoinBranchConstraints x y@ returns constraints inferred that
-- @x@ or @y@ is true.
disjoinBranchConstraints :: (OrdF (ArchReg arch), ShowF (ArchReg arch))
                         => BranchConstraints arch ids
                         -> BranchConstraints arch ids
                         -> BranchConstraints arch ids
disjoinBranchConstraints :: forall arch ids.
(OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
disjoinBranchConstraints BranchConstraints arch ids
x BranchConstraints arch ids
y =
  let joinMemVal :: k -> MemVal SubRange -> MemVal SubRange -> Maybe (MemVal SubRange)
      joinMemVal :: forall k.
k -> MemVal SubRange -> MemVal SubRange -> Maybe (MemVal SubRange)
joinMemVal k
_ (MemVal MemRepr tp
rx SubRange tp
sx) (MemVal MemRepr tp
ry SubRange tp
sy) = do
        tp :~: tp
Refl <- MemRepr tp -> MemRepr tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
MemRepr a -> MemRepr b -> Maybe (a :~: b)
testEquality MemRepr tp
rx MemRepr tp
ry
        MemRepr tp -> SubRange tp -> MemVal SubRange
forall (p :: Type -> Type) (tp :: Type).
MemRepr tp -> p tp -> MemVal p
MemVal MemRepr tp
rx (SubRange tp -> MemVal SubRange)
-> Maybe (SubRange tp) -> Maybe (MemVal SubRange)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SubRange tp -> SubRange tp -> Maybe (SubRange tp)
forall (tp :: Type).
SubRange tp -> SubRange tp -> Maybe (SubRange tp)
disjoinSubRange SubRange tp
sx SubRange tp
SubRange tp
sy
   in BranchConstraints
      { newClassRepConstraints :: MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints =
          (forall (tp :: Type).
 BoundLoc (ArchReg arch) tp
 -> SubRange tp -> SubRange tp -> Maybe (SubRange tp))
-> MapF (BoundLoc (ArchReg arch)) SubRange
-> MapF (BoundLoc (ArchReg arch)) SubRange
-> MapF (BoundLoc (ArchReg arch)) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type).
OrdF k =>
(forall (tp :: v). k tp -> a tp -> b tp -> Maybe (c tp))
-> MapF k a -> MapF k b -> MapF k c
MapF.intersectWithKeyMaybe
            (\BoundLoc (ArchReg arch) tp
_ -> SubRange tp -> SubRange tp -> Maybe (SubRange tp)
forall (tp :: Type).
SubRange tp -> SubRange tp -> Maybe (SubRange tp)
disjoinSubRange)
            (BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
forall arch ids.
BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints BranchConstraints arch ids
x)
            (BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
forall arch ids.
BranchConstraints arch ids
-> MapF (BoundLoc (ArchReg arch)) SubRange
newClassRepConstraints BranchConstraints arch ids
y)
      , newUninterpAssignConstraints :: MapF (AssignId ids) SubRange
newUninterpAssignConstraints =
          (forall (tp :: Type).
 AssignId ids tp
 -> SubRange tp -> SubRange tp -> Maybe (SubRange tp))
-> MapF (AssignId ids) SubRange
-> MapF (AssignId ids) SubRange
-> MapF (AssignId ids) SubRange
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type).
OrdF k =>
(forall (tp :: v). k tp -> a tp -> b tp -> Maybe (c tp))
-> MapF k a -> MapF k b -> MapF k c
MapF.intersectWithKeyMaybe
            (\AssignId ids tp
_ -> SubRange tp -> SubRange tp -> Maybe (SubRange tp)
forall (tp :: Type).
SubRange tp -> SubRange tp -> Maybe (SubRange tp)
disjoinSubRange)
            (BranchConstraints arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
BranchConstraints arch ids -> MapF (AssignId ids) SubRange
newUninterpAssignConstraints BranchConstraints arch ids
x)
            (BranchConstraints arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
BranchConstraints arch ids -> MapF (AssignId ids) SubRange
newUninterpAssignConstraints BranchConstraints arch ids
y)
      , newAddrConstraints :: Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
newAddrConstraints =
          (MemAddr (RegAddrWidth (ArchReg arch))
 -> MemVal SubRange -> MemVal SubRange -> Maybe (MemVal SubRange))
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
forall k a b c.
Ord k =>
(k -> a -> b -> Maybe c) -> Map k a -> Map k b -> Map k c
mapIntersectWithKeyMaybe MemAddr (RegAddrWidth (ArchReg arch))
-> MemVal SubRange -> MemVal SubRange -> Maybe (MemVal SubRange)
forall k.
k -> MemVal SubRange -> MemVal SubRange -> Maybe (MemVal SubRange)
joinMemVal (BranchConstraints arch ids
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
forall arch ids.
BranchConstraints arch ids
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints BranchConstraints arch ids
x) (BranchConstraints arch ids
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
forall arch ids.
BranchConstraints arch ids
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints BranchConstraints arch ids
y)
      }

------------------------------------------------------------------------
-- Bounds inference

-- | @addRangePred v p@ asserts that @(trunc v (rangeWidth p))@ is satisifies
-- bounds in @p@.
--
-- In several architectures, but particularly x86, we may have
-- constraints on just the bits in an expression, and so our bounds
-- tracking has special support for this.
--
-- This either returns the refined bounds, or `Left msg` where `msg`
-- is an explanation of what inconsistency was detected.  The upper
-- bounds must be non-negative.
addRangePred :: ( MapF.OrdF (ArchReg arch)
                , HasRepr (ArchReg arch) TypeRepr
                , u <= w
                , MemWidth (ArchAddrWidth arch)
                , ShowF (ArchReg arch)
                )
               => BlockIntraStackConstraints arch ids
               -> StackExpr arch ids (BVType w)
                 -- ^ Value we are adding bounds for.
               -> RangePred u
                  -- ^ Predicate on value to assert.
               -> Either String (BranchConstraints arch ids)
addRangePred :: forall arch (u :: Nat) (w :: Nat) ids.
(OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr, u <= w,
 MemWidth (ArchAddrWidth arch), ShowF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType w)
-> RangePred u
-> Either String (BranchConstraints arch ids)
addRangePred BlockIntraStackConstraints arch ids
_ StackExpr arch ids (BVType w)
v RangePred u
rng
    -- Do nothing if upper bounds equals or exceeds maximum unsigned
    -- value.
  | Nat
bnd <- RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
rng
  , Nat
bnd Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (StackExpr arch ids (BVType w) -> NatRepr w
forall (f :: Type -> Type) (w :: Nat).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth StackExpr arch ids (BVType w)
v)) =
      BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. b -> Either a b
Right BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints
addRangePred BlockIntraStackConstraints arch ids
_ StackExpr arch ids (BVType w)
v RangePred u
rng
    -- Do nothing if upper bounds equals or exceeds maximum unsigned
    -- value.
  | Nat
bnd <- RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
rng
  , Nat
bnd Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned (StackExpr arch ids (BVType w) -> NatRepr w
forall (f :: Type -> Type) (w :: Nat).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth StackExpr arch ids (BVType w)
v)) =
      BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. b -> Either a b
Right BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints
addRangePred BlockIntraStackConstraints arch ids
cns StackExpr arch ids (BVType w)
v RangePred u
p =
  case StackExpr arch ids (BVType w)
v of
    ClassRepExpr BoundLoc (ArchReg arch) (BVType w)
loc ->
      BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a. a -> Either String a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BranchConstraints arch ids
 -> Either String (BranchConstraints arch ids))
-> BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! BoundLoc (ArchReg arch) (BVType w)
-> RangePred u -> BranchConstraints arch ids
forall (u :: Nat) (w :: Nat) arch ids.
(u <= w) =>
BoundLoc (ArchReg arch) (BVType w)
-> RangePred u -> BranchConstraints arch ids
branchLocRangePred BoundLoc (ArchReg arch) (BVType w)
loc RangePred u
p
    UninterpAssignExpr AssignId ids (BVType w)
aid (ReadMem Value arch ids (BVType (ArchAddrWidth arch))
addrVal MemRepr (BVType w)
r) | Just ArchMemAddr arch
addr <- Value arch ids (BVType (ArchAddrWidth arch))
-> Maybe (ArchMemAddr arch)
forall arch ids.
MemWidth (ArchAddrWidth arch) =>
BVValue arch ids (ArchAddrWidth arch) -> Maybe (ArchMemAddr arch)
valueAsMemAddr Value arch ids (BVType (ArchAddrWidth arch))
addrVal ->
      BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a. a -> Either String a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BranchConstraints arch ids
 -> Either String (BranchConstraints arch ids))
-> BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! AssignId ids (BVType w)
-> ArchMemAddr arch
-> MemRepr (BVType w)
-> RangePred u
-> BranchConstraints arch ids
forall (u :: Nat) (w :: Nat) ids arch.
(u <= w) =>
AssignId ids (BVType w)
-> MemAddr (ArchAddrWidth arch)
-> MemRepr (BVType w)
-> RangePred u
-> BranchConstraints arch ids
branchReadMemRangePred AssignId ids (BVType w)
aid ArchMemAddr arch
addr MemRepr (BVType w)
r RangePred u
p
    UninterpAssignExpr AssignId ids (BVType w)
aid AssignRhs arch (Value arch ids) (BVType w)
_ ->
      BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a. a -> Either String a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BranchConstraints arch ids
 -> Either String (BranchConstraints arch ids))
-> BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! AssignId ids (BVType w)
-> RangePred u -> BranchConstraints arch ids
forall (u :: Nat) (w :: Nat) ids arch.
(u <= w) =>
AssignId ids (BVType w)
-> RangePred u -> BranchConstraints arch ids
branchAssignRangePred AssignId ids (BVType w)
aid RangePred u
p
    -- Drop constraints on the offset of a stack.
    -- This is unexpected.
    StackOffsetExpr MemInt (ArchAddrWidth arch)
_i ->
      BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a. a -> Either String a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BranchConstraints arch ids
 -> Either String (BranchConstraints arch ids))
-> BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints

    CExpr CValue arch (BVType w)
cv ->
      case CValue arch (BVType w)
cv of
        BVCValue NatRepr n
_ Integer
c -> do
          Bool -> Either String () -> Either String ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (NatRepr u -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
p) Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Nat -> Integer
forall a. Integral a => a -> Integer
toInteger (RangePred u -> Nat
forall (u :: Nat). RangePred u -> Nat
rangeUpperBound RangePred u
p)) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ do
            String -> Either String ()
forall a b. a -> Either a b
Left String
"Constant is greater than asserted bounds."
          BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a. a -> Either String a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BranchConstraints arch ids
 -> Either String (BranchConstraints arch ids))
-> BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints
        RelocatableCValue{} ->
          BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a. a -> Either String a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BranchConstraints arch ids
 -> Either String (BranchConstraints arch ids))
-> BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints
        SymbolCValue{} ->
          BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a. a -> Either String a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BranchConstraints arch ids
 -> Either String (BranchConstraints arch ids))
-> BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints
    UExtExpr StackExpr arch ids (BVType u)
x NatRepr w
_outWidth
      -- If this constraint affects fewer bits than the extension,
      -- then we just propagate the property to value
      -- pre-extension.
      | Just LeqProof u u
LeqProof <- NatRepr u -> NatRepr u -> Maybe (LeqProof u u)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
p) (StackExpr arch ids (BVType u) -> NatRepr u
forall (f :: Type -> Type) (w :: Nat).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth StackExpr arch ids (BVType u)
x) ->
          BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType u)
-> RangePred u
-> Either String (BranchConstraints arch ids)
forall arch (u :: Nat) (w :: Nat) ids.
(OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr, u <= w,
 MemWidth (ArchAddrWidth arch), ShowF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType w)
-> RangePred u
-> Either String (BranchConstraints arch ids)
addRangePred BlockIntraStackConstraints arch ids
cns StackExpr arch ids (BVType u)
x RangePred u
p
      -- Otherwise, we still can constrain our width.
      | Bool
otherwise -> do
          BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType u)
-> RangePred u
-> Either String (BranchConstraints arch ids)
forall arch (u :: Nat) (w :: Nat) ids.
(OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr, u <= w,
 MemWidth (ArchAddrWidth arch), ShowF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType w)
-> RangePred u
-> Either String (BranchConstraints arch ids)
addRangePred BlockIntraStackConstraints arch ids
cns StackExpr arch ids (BVType u)
x (RangePred u
p { rangeWidth = typeWidth x })
    AppExpr AssignId ids (BVType w)
n App (StackExpr arch ids) (BVType w)
a ->
      case App (StackExpr arch ids) (BVType w)
a of
        BVAdd NatRepr n
_ StackExpr arch ids ('BVType n)
x (CExpr (BVCValue NatRepr n
w Integer
c))
          | RangePred NatRepr u
_wp Nat
l Nat
u <- RangePred u
p
          , Integer
l' <- Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
c
          , Integer
u' <- Nat -> Integer
forall a. Integral a => a -> Integer
toInteger Nat
u Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
c
            -- Check overflow is consistent
          , Integer
l' Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatRepr n -> Nat
forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr n
w) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
u' Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatRepr n -> Nat
forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr n
w) -> do
              BlockIntraStackConstraints arch ids
-> StackExpr arch ids ('BVType n)
-> RangePred n
-> Either String (BranchConstraints arch ids)
forall arch (u :: Nat) (w :: Nat) ids.
(OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr, u <= w,
 MemWidth (ArchAddrWidth arch), ShowF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType w)
-> RangePred u
-> Either String (BranchConstraints arch ids)
addRangePred BlockIntraStackConstraints arch ids
cns StackExpr arch ids ('BVType n)
x (NatRepr n -> Nat -> Nat -> RangePred n
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
RangePred NatRepr n
w (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
l'))
                                              (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
u')))

        -- Truncation passes through as we aonly affect low order bits.
        Trunc StackExpr arch ids (BVType m)
x NatRepr n
_w ->
          case NatRepr u -> NatRepr m -> Maybe (LeqProof u m)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (RangePred u -> NatRepr u
forall (u :: Nat). RangePred u -> NatRepr u
rangeWidth RangePred u
p) (StackExpr arch ids (BVType m) -> NatRepr m
forall (f :: Type -> Type) (w :: Nat).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth StackExpr arch ids (BVType m)
x) of
            Just LeqProof u m
LeqProof ->
              BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType m)
-> RangePred u
-> Either String (BranchConstraints arch ids)
forall arch (u :: Nat) (w :: Nat) ids.
(OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr, u <= w,
 MemWidth (ArchAddrWidth arch), ShowF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType w)
-> RangePred u
-> Either String (BranchConstraints arch ids)
addRangePred BlockIntraStackConstraints arch ids
cns StackExpr arch ids (BVType m)
x RangePred u
p
            Maybe (LeqProof u m)
Nothing -> String -> Either String (BranchConstraints arch ids)
forall a. HasCallStack => String -> a
error String
"Invariant broken"

        -- If none of the above cases apply, then we just assign the
        -- predicate to the nonce identifing the app.
        App (StackExpr arch ids) (BVType w)
_ ->
          BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. b -> Either a b
Right (BranchConstraints arch ids
 -> Either String (BranchConstraints arch ids))
-> BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$ AssignId ids (BVType w)
-> RangePred u -> BranchConstraints arch ids
forall (u :: Nat) (w :: Nat) ids arch.
(u <= w) =>
AssignId ids (BVType w)
-> RangePred u -> BranchConstraints arch ids
branchAssignRangePred AssignId ids (BVType w)
n RangePred u
p

-- | @addLowerBoundPred cns w l x@ adds a @l <= x@ constraint over the `w`-bit-truncated values.
-- Fails when the bound excludes all possible values (lower bound greater than the maximum `w`-bit
-- value).
-- Note: The arguments are ordered so that it reads more naturally, as the difference of type
-- between `l` and `x` prevents mistakes.
addLowerBoundPred ::
  RegisterInfo (ArchReg arch) =>
  BlockIntraStackConstraints arch ids -> NatRepr n -> Integer -> Value arch ids (BVType n) ->
  Either String (BranchConstraints arch ids)
addLowerBoundPred :: forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
addLowerBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Integer
l Value arch ids (BVType n)
x
  | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr n
w = String -> Either String (BranchConstraints arch ids)
forall a b. a -> Either a b
Left String
"Lower bound excludes all possible values"
  | Bool
otherwise = BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType n)
-> RangePred n
-> Either String (BranchConstraints arch ids)
forall arch (u :: Nat) (w :: Nat) ids.
(OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr, u <= w,
 MemWidth (ArchAddrWidth arch), ShowF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType w)
-> RangePred u
-> Either String (BranchConstraints arch ids)
addRangePred BlockIntraStackConstraints arch ids
cns (BlockIntraStackConstraints arch ids
-> Value arch ids (BVType n) -> StackExpr arch ids (BVType n)
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> Value arch ids tp -> StackExpr arch ids tp
intraStackValueExpr BlockIntraStackConstraints arch ids
cns Value arch ids (BVType n)
x) (RangePred n -> Either String (BranchConstraints arch ids))
-> RangePred n -> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! NatRepr n -> Nat -> RangePred n
forall (u :: Nat). NatRepr u -> Nat -> RangePred u
mkLowerBound NatRepr n
w (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger Integer
l)

-- | @addUpperBoundPred cns w x u@ adds a @x <= u@ constraint over the `w`-bit-truncated values.
-- Fails when the bound excludes all possible values (`u` < 0).
addUpperBoundPred ::
  RegisterInfo (ArchReg arch) =>
  BlockIntraStackConstraints arch ids -> NatRepr n -> Value arch ids (BVType n) -> Integer ->
  Either String (BranchConstraints arch ids)
addUpperBoundPred :: forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
addUpperBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids (BVType n)
x Integer
u
  | Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = String -> Either String (BranchConstraints arch ids)
forall a b. a -> Either a b
Left String
"Upper bound excludes all possible values"
  | Bool
otherwise = BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType n)
-> RangePred n
-> Either String (BranchConstraints arch ids)
forall arch (u :: Nat) (w :: Nat) ids.
(OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr, u <= w,
 MemWidth (ArchAddrWidth arch), ShowF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType w)
-> RangePred u
-> Either String (BranchConstraints arch ids)
addRangePred BlockIntraStackConstraints arch ids
cns (BlockIntraStackConstraints arch ids
-> Value arch ids (BVType n) -> StackExpr arch ids (BVType n)
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> Value arch ids tp -> StackExpr arch ids tp
intraStackValueExpr BlockIntraStackConstraints arch ids
cns Value arch ids (BVType n)
x) (RangePred n -> Either String (BranchConstraints arch ids))
-> RangePred n -> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! NatRepr n -> Nat -> RangePred n
forall (u :: Nat). NatRepr u -> Nat -> RangePred u
mkUpperBound NatRepr n
w (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger Integer
u)

clamp :: NatRepr w -> Integer -> Integer
clamp :: forall (w :: Nat). NatRepr w -> Integer -> Integer
clamp NatRepr w
w Integer
x
  | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Integer
0
  | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w = NatRepr w -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr w
w
  | Bool
otherwise = Integer
x

-- | @addWithinRangePred cns w l x u@ adds a @l <= x <= u@ constraint over the `w`-bit-truncated values.
-- Fails when the bound excludes all possible values.
-- Note: The arguments are ordered so that it reads more naturally.
addWithinRangePred ::
  RegisterInfo (ArchReg arch) =>
  BlockIntraStackConstraints arch ids -> NatRepr n -> Integer -> Value arch ids (BVType n) -> Integer ->
  Either String (BranchConstraints arch ids)
addWithinRangePred :: forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
addWithinRangePred BlockIntraStackConstraints arch ids
cns NatRepr n
w Integer
l Value arch ids (BVType n)
x Integer
u
  -- Note: we could avoid this duplication by instead producing a conjunction of `addLowerBoundPred`
  -- and `addUpperBoundPred`, but this produces a single range instead.
  | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr n
w = String -> Either String (BranchConstraints arch ids)
forall a b. a -> Either a b
Left String
"Lower bound excludes all possible values"
  | Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = String -> Either String (BranchConstraints arch ids)
forall a b. a -> Either a b
Left String
"Upper bound excludes all possible values"
  | NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
clamp NatRepr n
w Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< NatRepr n -> Integer -> Integer
forall (w :: Nat). NatRepr w -> Integer -> Integer
clamp NatRepr n
w Integer
l = String -> Either String (BranchConstraints arch ids)
forall a b. a -> Either a b
Left String
"Empty range excludes all possible values"
  | Bool
otherwise =
    BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType n)
-> RangePred n
-> Either String (BranchConstraints arch ids)
forall arch (u :: Nat) (w :: Nat) ids.
(OrdF (ArchReg arch), HasRepr (ArchReg arch) TypeRepr, u <= w,
 MemWidth (ArchAddrWidth arch), ShowF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> StackExpr arch ids (BVType w)
-> RangePred u
-> Either String (BranchConstraints arch ids)
addRangePred BlockIntraStackConstraints arch ids
cns (BlockIntraStackConstraints arch ids
-> Value arch ids (BVType n) -> StackExpr arch ids (BVType n)
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockIntraStackConstraints arch ids
-> Value arch ids tp -> StackExpr arch ids tp
intraStackValueExpr BlockIntraStackConstraints arch ids
cns Value arch ids (BVType n)
x) (RangePred n -> Either String (BranchConstraints arch ids))
-> RangePred n -> Either String (BranchConstraints arch ids)
forall a b. (a -> b) -> a -> b
$! NatRepr n -> Nat -> Nat -> RangePred n
forall (u :: Nat). NatRepr u -> Nat -> Nat -> RangePred u
mkRangeBound NatRepr n
w (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger Integer
l) (Integer -> Nat
forall a. Num a => Integer -> a
fromInteger Integer
u)

-- | @addExcludeRangePred cns w x l u@ adds a @(x < l) or (u < x)@ constraint over the
-- `w`-bit-truncated values.  Fails when the bound excludes all possible values.
addExcludeRangePred ::
  RegisterInfo (ArchReg arch) =>
  BlockIntraStackConstraints arch ids -> NatRepr n -> Value arch ids (BVType n) -> Integer -> Integer ->
  Either String (BranchConstraints arch ids)
addExcludeRangePred :: forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Integer
-> Either String (BranchConstraints arch ids)
addExcludeRangePred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids (BVType n)
x Integer
l Integer
u = do
  let lowerBoundTooLow :: Bool
lowerBoundTooLow = Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0              -- (l - 1) would be negative
  let upperBoundTooHigh :: Bool
upperBoundTooHigh = Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr n -> Integer
forall (w :: Nat). NatRepr w -> Integer
maxUnsigned NatRepr n
w -- (u + 1) would overflow
  if
    | Bool
lowerBoundTooLow Bool -> Bool -> Bool
&& Bool
upperBoundTooHigh -> String -> Either String (BranchConstraints arch ids)
forall a b. a -> Either a b
Left String
"Excluded range excludes all possible values"
    | Bool
lowerBoundTooLow -> BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
addLowerBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w (Integer
u Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Value arch ids (BVType n)
x
    | Bool
upperBoundTooHigh -> BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
addUpperBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids (BVType n)
x (Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
    | Bool
otherwise ->
      -- compiles it to @(x <= l - 1) or (u + 1 <= x)@
      BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
forall arch ids.
(OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
disjoinBranchConstraints
        (BranchConstraints arch ids
 -> BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either
     String (BranchConstraints arch ids -> BranchConstraints arch ids)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
addUpperBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids (BVType n)
x (Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
        Either
  String (BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
addLowerBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w (Integer
u Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Value arch ids (BVType n)
x

-- | @assertEqPred cns x w c isTrue@ asserts equality @x = BVValue c w@ is either true or false,
-- based on `isTrue`.
assertEqPred ::
  RegisterInfo (ArchReg arch) =>
  -- | Constraints that let us evaluate `x`
  BlockIntraStackConstraints arch ids ->
  -- | Bitwidth the comparison should apply to
  NatRepr w ->
  -- | Value to be constrained
  Value arch ids (BVType w) ->
  -- | Numeric constant x should be equal/different to
  Integer ->
  -- | `True` if we should assert equality, `False` if we should assert non-equality
  Bool ->
  Either String (BranchConstraints arch ids)
assertEqPred :: forall arch ids (w :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr w
-> Value arch ids (BVType w)
-> Integer
-> Bool
-> Either String (BranchConstraints arch ids)
assertEqPred BlockIntraStackConstraints arch ids
cns NatRepr w
w Value arch ids (BVType w)
x Integer
c Bool
isTrue
  | Bool
isTrue =
    -- x == c becomes c <= x <= c
    BlockIntraStackConstraints arch ids
-> NatRepr w
-> Integer
-> Value arch ids (BVType w)
-> Integer
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
addWithinRangePred BlockIntraStackConstraints arch ids
cns NatRepr w
w Integer
c Value arch ids (BVType w)
x Integer
c
  | Bool
otherwise =
    -- !(x == c) is handled via !(c <= x <= c) and becomes (x <= c - 1) or (c + 1 <= x)
    BlockIntraStackConstraints arch ids
-> NatRepr w
-> Value arch ids (BVType w)
-> Integer
-> Integer
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Integer
-> Either String (BranchConstraints arch ids)
addExcludeRangePred BlockIntraStackConstraints arch ids
cns NatRepr w
w Value arch ids (BVType w)
x Integer
c Integer
c

-- | Assert a predicate is true/false and update bounds.
--
-- If it returns a new upper bounds, then that may be used.
-- Otherwise, it detects an inconsistency and returns a message
-- explaing why.
assertPred :: RegisterInfo (ArchReg arch)
           => IntraJumpBounds arch ids
           -> Value arch ids BoolType -- ^ Value representing predicate
           -> Bool -- ^ Controls whether predicate is true or false
           -> Either String (BranchConstraints arch ids)
assertPred :: forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds (AssignedValue Assignment arch ids BoolType
a) Bool
isTrue = do
  let cns :: BlockIntraStackConstraints arch ids
cns = IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
forall arch ids.
IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
intraStackConstraints IntraJumpBounds arch ids
bnds
  case Assignment arch ids BoolType
-> AssignRhs arch (Value arch ids) BoolType
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignRhs arch (Value arch ids) tp
assignRhs Assignment arch ids BoolType
a of
    EvalApp (Eq Value arch ids tp1
x (BVValue NatRepr n
w Integer
c)) -> BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids (w :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr w
-> Value arch ids (BVType w)
-> Integer
-> Bool
-> Either String (BranchConstraints arch ids)
assertEqPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids tp1
Value arch ids (BVType n)
x Integer
c Bool
isTrue
    EvalApp (Eq (BVValue NatRepr n
w Integer
c) Value arch ids tp1
x) -> BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids (w :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr w
-> Value arch ids (BVType w)
-> Integer
-> Bool
-> Either String (BranchConstraints arch ids)
assertEqPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids tp1
Value arch ids (BVType n)
x Integer
c Bool
isTrue
    EvalApp (BVUnsignedLt Value arch ids (BVType n)
x (BVValue NatRepr n
w Integer
c))
      | Bool
isTrue ->
        -- x < c becomes x <= c - 1
        BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
addUpperBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids (BVType n)
Value arch ids (BVType n)
x (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
      | Bool
otherwise ->
        -- !(x < c) becomes c <= x
        BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
addLowerBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Integer
c Value arch ids (BVType n)
Value arch ids (BVType n)
x
    EvalApp (BVUnsignedLt (BVValue NatRepr n
w Integer
c) Value arch ids (BVType n)
y)
      | Bool
isTrue ->
        -- c < y becomes c + 1 <= y
        BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
addLowerBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Value arch ids (BVType n)
Value arch ids (BVType n)
y
      | Bool
otherwise ->
        -- !(c < y) becomes y <= c
        BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
addUpperBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids (BVType n)
Value arch ids (BVType n)
y Integer
c
    EvalApp (BVUnsignedLe Value arch ids (BVType n)
x (BVValue NatRepr n
w Integer
c))
      | Bool
isTrue ->
        -- x <= c
        BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
addUpperBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids (BVType n)
Value arch ids (BVType n)
x Integer
c
      | Bool
otherwise ->
        -- !(x <= c) becomes c + 1 <= x
        BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
addLowerBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Value arch ids (BVType n)
Value arch ids (BVType n)
x
    EvalApp (BVUnsignedLe (BVValue NatRepr n
w Integer
c) Value arch ids (BVType n)
y)
      | Bool
isTrue ->
        -- c <= y
        BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Integer
-> Value arch ids (BVType n)
-> Either String (BranchConstraints arch ids)
addLowerBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Integer
c Value arch ids (BVType n)
Value arch ids (BVType n)
y
      | Bool
otherwise ->
        -- !(c <= y) becomes y <= c - 1
        BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
forall arch ids (n :: Nat).
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> NatRepr n
-> Value arch ids (BVType n)
-> Integer
-> Either String (BranchConstraints arch ids)
addUpperBoundPred BlockIntraStackConstraints arch ids
cns NatRepr n
w Value arch ids (BVType n)
Value arch ids (BVType n)
y (Integer
c Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
    EvalApp (AndApp Value arch ids BoolType
l Value arch ids BoolType
r)
      | Bool
isTrue ->
        -- l && r
        BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
forall arch ids.
OrdF (ArchReg arch) =>
BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
conjoinBranchConstraints
          (BranchConstraints arch ids
 -> BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either
     String (BranchConstraints arch ids -> BranchConstraints arch ids)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds Value arch ids BoolType
l Bool
True
          Either
  String (BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds Value arch ids BoolType
r Bool
True
      | Bool
otherwise ->
        -- !(l && r) becomes !l || !r
        BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
forall arch ids.
(OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
disjoinBranchConstraints
          (BranchConstraints arch ids
 -> BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either
     String (BranchConstraints arch ids -> BranchConstraints arch ids)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds Value arch ids BoolType
l Bool
False
          Either
  String (BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds Value arch ids BoolType
r Bool
False
    EvalApp (OrApp  Value arch ids BoolType
l Value arch ids BoolType
r)
      | Bool
isTrue ->
        -- l || r
        BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
forall arch ids.
(OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
disjoinBranchConstraints
          (BranchConstraints arch ids
 -> BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either
     String (BranchConstraints arch ids -> BranchConstraints arch ids)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds Value arch ids BoolType
l Bool
True
          Either
  String (BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds Value arch ids BoolType
r Bool
True
      | Bool
otherwise ->
        -- !(l || r) becomes !l && !r
        BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
forall arch ids.
OrdF (ArchReg arch) =>
BranchConstraints arch ids
-> BranchConstraints arch ids -> BranchConstraints arch ids
conjoinBranchConstraints
          (BranchConstraints arch ids
 -> BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either
     String (BranchConstraints arch ids -> BranchConstraints arch ids)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds Value arch ids BoolType
l Bool
False
          Either
  String (BranchConstraints arch ids -> BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
-> Either String (BranchConstraints arch ids)
forall a b.
Either String (a -> b) -> Either String a -> Either String b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds Value arch ids BoolType
r Bool
False
    EvalApp (NotApp Value arch ids BoolType
p) -> IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
bnds Value arch ids BoolType
p (Bool -> Bool
not Bool
isTrue)
    AssignRhs arch (Value arch ids) BoolType
_ -> BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. b -> Either a b
Right BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints
assertPred IntraJumpBounds arch ids
_ Value arch ids BoolType
_ Bool
_ =
  BranchConstraints arch ids
-> Either String (BranchConstraints arch ids)
forall a b. b -> Either a b
Right BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints

updateRangePredMap :: ( MemWidth (ArchAddrWidth arch)
                      , HasRepr (ArchReg arch) TypeRepr
                      , OrdF (ArchReg arch)
                      , ShowF (ArchReg arch)
                      )
                   => ExprRangePredInfo arch ids
                   -- ^ Information for computing range predicates of stack expressions.
                   -> LocMap (ArchReg arch) SubRange
                   -> Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)
                   -> LocMap (ArchReg arch) SubRange
updateRangePredMap :: forall arch ids.
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
ExprRangePredInfo arch ids
-> LocMap (ArchReg arch) SubRange
-> Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)
-> LocMap (ArchReg arch) SubRange
updateRangePredMap ExprRangePredInfo arch ids
info LocMap (ArchReg arch) SubRange
m (Pair BoundLoc (ArchReg arch) tp
l StackExpr arch ids tp
e) =
  case ExprRangePredInfo arch ids
-> StackExpr arch ids tp -> MaybeRangePred tp
forall arch ids (tp :: Type).
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
ExprRangePredInfo arch ids
-> StackExpr arch ids tp -> MaybeRangePred tp
exprRangePred ExprRangePredInfo arch ids
info StackExpr arch ids tp
e of
    SomeRangePred RangePred u
r -> BoundLoc (ArchReg arch) tp
-> SubRange tp
-> LocMap (ArchReg arch) SubRange
-> LocMap (ArchReg arch) SubRange
forall (r :: Type -> Type) (tp :: Type) (v :: Type -> Type).
OrdF r =>
BoundLoc r tp -> v tp -> LocMap r v -> LocMap r v
nonOverlapLocInsert BoundLoc (ArchReg arch) tp
l (RangePred u -> SubRange ('BVType v)
forall (u :: Nat) (w :: Nat).
(u <= w) =>
RangePred u -> SubRange (BVType w)
SubRange RangePred u
r) LocMap (ArchReg arch) SubRange
m
    MaybeRangePred tp
NoRangePred -> LocMap (ArchReg arch) SubRange
m

nextStackConstraintsAndReps :: RegisterInfo (ArchReg arch)
                            => BlockIntraStackConstraints arch ids
                              -- ^ Bounds at end of this state.
                            -> RegState (ArchReg arch) (Value arch ids)
                            -- ^ Register values at start of next state.
                            -- Note. ip_reg is ignored
                            -> ( BlockStartStackConstraints arch
                               , [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
                               )
nextStackConstraintsAndReps :: forall arch ids.
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> (BlockStartStackConstraints arch,
    [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
nextStackConstraintsAndReps BlockIntraStackConstraints arch ids
cns RegState (ArchReg arch) (Value arch ids)
regs = NextStateMonad
  arch
  ids
  (BlockStartStackConstraints arch,
   [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
-> (BlockStartStackConstraints arch,
    [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
forall arch ids a. NextStateMonad arch ids a -> a
runNextStateMonad (NextStateMonad
   arch
   ids
   (BlockStartStackConstraints arch,
    [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
 -> (BlockStartStackConstraints arch,
     [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]))
-> NextStateMonad
     arch
     ids
     (BlockStartStackConstraints arch,
      [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
-> (BlockStartStackConstraints arch,
    [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
forall a b. (a -> b) -> a -> b
$
  (,) (BlockStartStackConstraints arch
 -> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
 -> (BlockStartStackConstraints arch,
     [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]))
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
-> NextStateMonad
     arch
     ids
     ([Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
      -> (BlockStartStackConstraints arch,
          [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> BlockIntraStackConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
forall arch ids.
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
postJumpStackConstraints BlockIntraStackConstraints arch ids
cns RegState (ArchReg arch) (Value arch ids)
regs
      NextStateMonad
  arch
  ids
  ([Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
   -> (BlockStartStackConstraints arch,
       [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]))
-> NextStateMonad
     arch ids [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
-> NextStateMonad
     arch
     ids
     (BlockStartStackConstraints arch,
      [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
forall a b.
NextStateMonad arch ids (a -> b)
-> NextStateMonad arch ids a -> NextStateMonad arch ids b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> NextStateMonad
  arch ids [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
forall arch ids.
NextStateMonad
  arch ids [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
getNextStateRepresentatives

-- | Bounds for block after jump
nextBlockBounds :: forall arch ids
                .  RegisterInfo (ArchReg arch)
                => IntraJumpBounds arch ids
                   -- ^ Bounds at end of this state.
                -> BranchConstraints arch ids
                   -- ^ Constraints inferred from branch (or `emptyBranchConstraints)
                -> RegState (ArchReg arch) (Value arch ids)
                   -- ^ Register values at start of next state.
                   --
                   -- Note. This ignores @ip_reg@.
                -> InitJumpBounds arch
nextBlockBounds :: forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
nextBlockBounds IntraJumpBounds arch ids
bnds BranchConstraints arch ids
brCns RegState (ArchReg arch) (Value arch ids)
regs =
  let cns :: BlockIntraStackConstraints arch ids
cns = IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
forall arch ids.
IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
intraStackConstraints IntraJumpBounds arch ids
bnds
      (BlockStartStackConstraints arch
stkCns, [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
reps) = BlockIntraStackConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> (BlockStartStackConstraints arch,
    [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
forall arch ids.
RegisterInfo (ArchReg arch) =>
BlockIntraStackConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> (BlockStartStackConstraints arch,
    [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
nextStackConstraintsAndReps BlockIntraStackConstraints arch ids
cns RegState (ArchReg arch) (Value arch ids)
regs
      info :: ExprRangePredInfo arch ids
info = ExprRangePredInfo { erpiBndsMap :: BlockStartStackConstraints arch
erpiBndsMap = BlockIntraStackConstraints arch ids
-> BlockStartStackConstraints arch
forall arch ids.
BlockIntraStackConstraints arch ids
-> BlockStartStackConstraints arch
biscInitConstraints BlockIntraStackConstraints arch ids
cns
                               , erpiRngPredMap :: BlockStartRangePred arch
erpiRngPredMap = BlockStartRangePred arch
forall (r :: Type -> Type) (v :: Type -> Type). LocMap r v
locMapEmpty
                               , erpiReadPredMap :: MapF (AssignId ids) SubRange
erpiReadPredMap = IntraJumpBounds arch ids -> MapF (AssignId ids) SubRange
forall arch ids.
IntraJumpBounds arch ids -> MapF (AssignId ids) SubRange
intraReadPredMap IntraJumpBounds arch ids
bnds
                               , erpiBranchConstraints :: BranchConstraints arch ids
erpiBranchConstraints = BranchConstraints arch ids
brCns
                               }
   in InitJumpBounds { initBndsMap :: BlockStartStackConstraints arch
initBndsMap     = BlockStartStackConstraints arch
stkCns
                     , initRngPredMap :: BlockStartRangePred arch
initRngPredMap  = (BlockStartRangePred arch
 -> Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)
 -> BlockStartRangePred arch)
-> BlockStartRangePred arch
-> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
-> BlockStartRangePred arch
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (ExprRangePredInfo arch ids
-> BlockStartRangePred arch
-> Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)
-> BlockStartRangePred arch
forall arch ids.
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
ExprRangePredInfo arch ids
-> LocMap (ArchReg arch) SubRange
-> Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)
-> LocMap (ArchReg arch) SubRange
updateRangePredMap ExprRangePredInfo arch ids
info) BlockStartRangePred arch
forall (r :: Type -> Type) (v :: Type -> Type). LocMap r v
locMapEmpty [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
reps
                     , initAddrPredMap :: Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
initAddrPredMap = BranchConstraints arch ids
-> Map (MemAddr (RegAddrWidth (ArchReg arch))) (MemVal SubRange)
forall arch ids.
BranchConstraints arch ids
-> Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
newAddrConstraints BranchConstraints arch ids
brCns
                     }

-- | Bounds for block after jump
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
postJumpBounds :: forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> RegState (ArchReg arch) (Value arch ids) -> InitJumpBounds arch
postJumpBounds IntraJumpBounds arch ids
cns RegState (ArchReg arch) (Value arch ids)
regs = IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
nextBlockBounds IntraJumpBounds arch ids
cns BranchConstraints arch ids
forall arch ids. BranchConstraints arch ids
emptyBranchConstraints RegState (ArchReg arch) (Value arch ids)
regs

data BranchBounds arch
   = InfeasibleBranch
   | TrueFeasibleBranch  !(InitJumpBounds arch)
   | FalseFeasibleBranch !(InitJumpBounds arch)
   | BothFeasibleBranch  !(InitJumpBounds arch) !(InitJumpBounds arch)

postBranchBounds :: RegisterInfo (ArchReg arch)
                 => IntraJumpBounds arch ids -- ^ Bounds just before jump
                 -> RegState (ArchReg arch) (Value arch ids)
                 -- ^ Register values at start of next state.
                 -> Value arch ids BoolType -- ^ Branch condition
                 -> BranchBounds arch
postBranchBounds :: forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> Value arch ids BoolType
-> BranchBounds arch
postBranchBounds IntraJumpBounds arch ids
cns RegState (ArchReg arch) (Value arch ids)
regs Value arch ids BoolType
c = do
  case (IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
cns Value arch ids BoolType
c Bool
True, IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> Value arch ids BoolType
-> Bool
-> Either String (BranchConstraints arch ids)
assertPred IntraJumpBounds arch ids
cns Value arch ids BoolType
c Bool
False) of
    (Right BranchConstraints arch ids
brCnsT, Right BranchConstraints arch ids
brCnsF) ->
      InitJumpBounds arch -> InitJumpBounds arch -> BranchBounds arch
forall arch.
InitJumpBounds arch -> InitJumpBounds arch -> BranchBounds arch
BothFeasibleBranch (IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
nextBlockBounds IntraJumpBounds arch ids
cns BranchConstraints arch ids
brCnsT RegState (ArchReg arch) (Value arch ids)
regs)
                         (IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
nextBlockBounds IntraJumpBounds arch ids
cns BranchConstraints arch ids
brCnsF RegState (ArchReg arch) (Value arch ids)
regs)
    (Right BranchConstraints arch ids
brCnsT, Left String
_) ->
      InitJumpBounds arch -> BranchBounds arch
forall arch. InitJumpBounds arch -> BranchBounds arch
TrueFeasibleBranch  (IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
nextBlockBounds IntraJumpBounds arch ids
cns BranchConstraints arch ids
brCnsT RegState (ArchReg arch) (Value arch ids)
regs)
    (Left String
_, Right BranchConstraints arch ids
brCnsF) ->
      InitJumpBounds arch -> BranchBounds arch
forall arch. InitJumpBounds arch -> BranchBounds arch
FalseFeasibleBranch (IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
forall arch ids.
RegisterInfo (ArchReg arch) =>
IntraJumpBounds arch ids
-> BranchConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
nextBlockBounds IntraJumpBounds arch ids
cns BranchConstraints arch ids
brCnsF RegState (ArchReg arch) (Value arch ids)
regs)
    (Left String
_, Left String
_) ->
      BranchBounds arch
forall arch. BranchBounds arch
InfeasibleBranch

-- | Return the index bounds after a function call.
postCallBounds :: forall arch ids
               .  RegisterInfo (ArchReg arch)
               => CallParams (ArchReg arch)
               -> IntraJumpBounds arch ids
               -> RegState (ArchReg arch) (Value arch ids)
               -> InitJumpBounds arch
postCallBounds :: forall arch ids.
RegisterInfo (ArchReg arch) =>
CallParams (ArchReg arch)
-> IntraJumpBounds arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> InitJumpBounds arch
postCallBounds CallParams (ArchReg arch)
params IntraJumpBounds arch ids
cns RegState (ArchReg arch) (Value arch ids)
regs =
  let cns' :: BlockStartStackConstraints arch
cns' = NextStateMonad arch ids (BlockStartStackConstraints arch)
-> BlockStartStackConstraints arch
forall arch ids a. NextStateMonad arch ids a -> a
runNextStateMonad (NextStateMonad arch ids (BlockStartStackConstraints arch)
 -> BlockStartStackConstraints arch)
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
-> BlockStartStackConstraints arch
forall a b. (a -> b) -> a -> b
$
              CallParams (ArchReg arch)
-> BlockIntraStackConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
forall arch ids.
RegisterInfo (ArchReg arch) =>
CallParams (ArchReg arch)
-> BlockIntraStackConstraints arch ids
-> RegState (ArchReg arch) (Value arch ids)
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
postCallStackConstraints CallParams (ArchReg arch)
params (IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
forall arch ids.
IntraJumpBounds arch ids -> BlockIntraStackConstraints arch ids
intraStackConstraints IntraJumpBounds arch ids
cns) RegState (ArchReg arch) (Value arch ids)
regs
   in InitJumpBounds { initBndsMap :: BlockStartStackConstraints arch
initBndsMap = BlockStartStackConstraints arch
cns'
                     , initRngPredMap :: BlockStartRangePred arch
initRngPredMap = BlockStartRangePred arch
forall (r :: Type -> Type) (v :: Type -> Type). LocMap r v
locMapEmpty
                     , initAddrPredMap :: Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
initAddrPredMap = Map (MemAddr (ArchAddrWidth arch)) (MemVal SubRange)
forall k a. Map k a
Map.empty
                     }

-- | This type is used to represent the location to return to *within a
-- function* after executing an architecture-specific terminator instruction.
--
--  * The 'MemSegmentOff' is the address to jump to next (within the function)
--  * The 'AbsBlockState' is the abstract state to use at the start of the block returned to (reflecting any changes made by the architecture-specific terminator)
--  * The 'Jmp.InitJumpBounds' is a collection of relations between values in registers and on the stack that should hold (see 'Jmp.postCallBounds' for to construct this in the common case)
--
-- Note: This is defined here (despite not being used here) to avoid import cycles elsewhere
type IntraJumpTarget arch =
  (ArchSegmentOff arch, AbsBlockState (ArchReg arch), InitJumpBounds arch)