{- |

This module defines a relational abstract domain for tracking
registers and stack addresses.  The model records when one of these
values is known to be equal to the current pointer stack frame.  This
domain also tracks equalities between nodes so that analysis
algorithms built on top of this are modulo known equivalences
between registers and stack locations.

The theory is defined over bitvector with a predefined
"address width" @addrWidth@ for the number of bits in the
address space

> p := t = u
>   |  t = stack_frame + c
>   |  t = uext u w    (1 <= width u && width u < w)
>
> t := r (@r@ is a register)
>   |  *(stack_frame + c)

@c@ is a signed @addrWidth@-bit bitvector.  @stack_frame@ denotes
a @addrWidth@-bit bitvector for the stack frame.  @w@ is a width
parameter.

Given a set of axioms using the constraint @P@ we have the following
proof rules:

> A,p |= p                                                       (assumption)
> A   |= t = t                                                   (reflexivity)
> A   |= t = u => A |= u = t                                     (symmetry)
> A   |= t = u && A |= u = v => A |= t = v                       (transitivity)
> A   |= t = uext u w && A |= u = uext v w' => A |= t = uext v w (double uext)
> A   |= t = uext u w && A |= u = v => A |= t = uext v w         (uext congruence)

-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.AbsDomain.StackAnalysis
  ( -- * Block level datatypes
    -- ** BlockStartStackConstraints
    BlockStartStackConstraints
  , StackEqConstraint(..)
  , ppBlockStartStackConstraints
  , fnEntryBlockStartStackConstraints
  , ppStackEqConstraint
  , blockStartLocExpr
  , blockStartLocStackOffset
  , StackOffConstraint(..)
  , blockStartLocRepAndCns
  , BoundLoc(..)
  , joinBlockStartStackConstraints
  , JoinClassMap
  , JoinClassPair(..)
    -- ** BlockIntraStackConstraints
  , BlockIntraStackConstraints
  , mkBlockIntraStackConstraints
  , biscInitConstraints
  , intraStackValueExpr
  , StackExpr(..)
  , intraStackRhsExpr
  , intraStackSetAssignId
  , discardMemInfo
  , writeStackOff
    -- ** Block terminator updates
  , postJumpStackConstraints
  , Data.Macaw.AbsDomain.CallParams.CallParams
  , postCallStackConstraints
    -- * LocMap
  , LocMap(..)
  , locMapEmpty
  , locMapNull
  , locMapToList
  , locLookup
  , nonOverlapLocInsert
  , locOverwriteWith
  , ppLocMap
  , foldLocMap
    -- * MemMap
  , MemMap
  , emptyMemMap
  , memMapLookup
  , memMapLookup'
  , MemMapLookup(..)
  , memMapOverwrite
  , memMapMapWithKey
  , memMapTraverseWithKey_
  , memMapTraverseMaybeWithKey
  , memMapDropAbove
  , memMapDropBelow
    -- * NextStateMonad
  , NextStateMonad
  , runNextStateMonad
  , getNextStateRepresentatives
    -- * Miscelaneous
  , MemVal(..)
  ) where

import           Control.Monad (unless)
import           Control.Monad.State (MonadState(..), State, evalState, gets)
import           Data.Kind
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Parameterized.Classes
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Pair
import           Data.Parameterized.TraversableF
import           Data.Parameterized.TraversableFC
import           Data.Proxy
import           Data.STRef
import           GHC.Natural
import           Prettyprinter
import           Text.Printf

import           Data.Macaw.AbsDomain.CallParams
import           Data.Macaw.CFG.App
import           Data.Macaw.CFG.Core
import           Data.Macaw.Memory
import qualified Data.Macaw.Types as M
import           Data.Macaw.Types hiding (Type)
import           Data.Macaw.Utils.Changed

addrTypeRepr :: MemWidth w => TypeRepr (BVType w)
addrTypeRepr :: forall (w :: Natural). MemWidth w => TypeRepr (BVType w)
addrTypeRepr = NatRepr w -> TypeRepr ('BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr w
forall (w :: Natural). MemWidth w => NatRepr w
memWidthNatRepr

ppAddend :: MemInt w -> Doc ann
ppAddend :: forall (w :: Natural) ann. MemInt w -> Doc ann
ppAddend MemInt w
o | MemInt w -> Int64
forall (w :: Natural). MemInt w -> Int64
memIntValue MemInt w
o Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
< Int64
0 =
               Doc ann
"-" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Integer -> Integer
forall a. Num a => a -> a
negate (Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger (MemInt w -> Int64
forall (w :: Natural). MemInt w -> Int64
memIntValue MemInt w
o)))
           | Bool
otherwise = Doc ann
"+" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> MemInt w -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MemInt w -> Doc ann
pretty MemInt w
o

ppStackOff :: MemInt w -> MemRepr tp -> Doc ann
ppStackOff :: forall (w :: Natural) (tp :: Type) ann.
MemInt w -> MemRepr tp -> Doc ann
ppStackOff MemInt w
o MemRepr tp
repr =
  Doc ann
"*(stack_frame" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> MemInt w -> Doc ann
forall (w :: Natural) ann. MemInt w -> Doc ann
ppAddend MemInt w
o Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
", " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> MemRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MemRepr tp -> Doc ann
pretty MemRepr tp
repr Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
")"

------------------------------------------------------------------------
-- JoinClassPair

data JoinClassPair (key :: k -> Type)  (tp :: k) = JoinClassPair !(key tp) !(key tp)

instance TestEquality k => TestEquality (JoinClassPair k) where
  testEquality :: forall (a :: k) (b :: k).
JoinClassPair k a -> JoinClassPair k b -> Maybe (a :~: b)
testEquality (JoinClassPair k a
x1 k a
x2) (JoinClassPair k b
y1 k b
y2) = do
    a :~: b
Refl <- k a -> k b -> Maybe (a :~: b)
forall (a :: k) (b :: k). k a -> k b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality k a
x1 k b
y1
    k a -> k b -> Maybe (a :~: b)
forall (a :: k) (b :: k). k a -> k b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality k a
x2 k b
y2

instance OrdF k => OrdF (JoinClassPair k) where
  compareF :: forall (x :: k) (y :: k).
JoinClassPair k x -> JoinClassPair k y -> OrderingF x y
compareF (JoinClassPair k x
x1 k x
x2) (JoinClassPair k y
y1 k y
y2) =
    OrderingF x y -> ((x ~ y) => OrderingF x y) -> OrderingF x y
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (k x -> k y -> OrderingF x y
forall (x :: k) (y :: k). k x -> k y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF k x
x1 k y
y1) (k x -> k y -> OrderingF x y
forall (x :: k) (y :: k). k x -> k y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF k x
x2 k y
y2)

------------------------------------------------------------------------
-- MemVal

-- | A value with a particular type along with a MemRepr indicating
-- how the type is encoded in memory.
data MemVal (p :: M.Type -> Type) =
  forall (tp :: M.Type) . MemVal !(MemRepr tp) !(p tp)

instance FunctorF MemVal where
  fmapF :: forall (f :: Type -> Type) (g :: Type -> Type).
(forall (x :: Type). f x -> g x) -> MemVal f -> MemVal g
fmapF forall (x :: Type). f x -> g x
f (MemVal MemRepr tp
r f tp
x) = MemRepr tp -> g tp -> MemVal g
forall (p :: Type -> Type) (tp :: Type).
MemRepr tp -> p tp -> MemVal p
MemVal MemRepr tp
r (f tp -> g tp
forall (x :: Type). f x -> g x
f f tp
x)

------------------------------------------------------------------------
-- BoundLoc

-- | A location within a function tracked by our bounds analysis
-- algorithms.
--
-- Locations for these purposes are registers, stack offsets, and
-- global memory offsets.
data BoundLoc (r :: M.Type -> Type) (tp :: M.Type) where
  -- | @RegLoc r@ denotes the register @r@.
  RegLoc :: !(r tp) -> BoundLoc r tp
  -- | @StackkOffLoc o repr@ denotes the bytes from address range
  -- @[initSP + o .. initSP + o + memReprBytes repr)@.
  --
  -- @initSP@ denotes the stack offset at the start of function
  -- execution.
  --
  -- We should note that this makes no claim that those addresses
  -- are valid.
  StackOffLoc :: !(MemInt (RegAddrWidth r))
              -> !(MemRepr tp)
              -> BoundLoc r tp

instance TestEquality r => TestEquality (BoundLoc r) where
  testEquality :: forall (a :: Type) (b :: Type).
BoundLoc r a -> BoundLoc r b -> Maybe (a :~: b)
testEquality (RegLoc r a
x) (RegLoc r b
y) = r a -> r b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type). r a -> r b -> Maybe (a :~: b)
testEquality r a
x r b
y
  testEquality (StackOffLoc MemInt (RegAddrWidth r)
xi MemRepr a
xr) (StackOffLoc MemInt (RegAddrWidth r)
yi MemRepr b
yr) | MemInt (RegAddrWidth r)
xi MemInt (RegAddrWidth r) -> MemInt (RegAddrWidth r) -> Bool
forall a. Eq a => a -> a -> Bool
== MemInt (RegAddrWidth r)
yi =
    MemRepr a -> MemRepr b -> Maybe (a :~: b)
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 a
xr MemRepr b
yr
  testEquality BoundLoc r a
_ BoundLoc r b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance HasRepr r TypeRepr => HasRepr (BoundLoc r) TypeRepr where
  typeRepr :: forall (tp :: Type). BoundLoc r tp -> TypeRepr tp
typeRepr (RegLoc r tp
r) = r tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). r tp -> TypeRepr tp
typeRepr r tp
r
  typeRepr (StackOffLoc MemInt (RegAddrWidth r)
_ MemRepr tp
r) = MemRepr tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). MemRepr tp -> TypeRepr tp
typeRepr MemRepr tp
r

instance OrdF r => OrdF (BoundLoc r) where
  compareF :: forall (x :: Type) (y :: Type).
BoundLoc r x -> BoundLoc r y -> OrderingF x y
compareF (RegLoc r x
x) (RegLoc r y
y) = r x -> r y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type). r x -> r y -> OrderingF x y
compareF r x
x r y
y
  compareF (RegLoc r x
_) BoundLoc r y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF BoundLoc r x
_ (RegLoc r y
_) = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (StackOffLoc MemInt (RegAddrWidth r)
xi MemRepr x
xr) (StackOffLoc MemInt (RegAddrWidth r)
yi MemRepr y
yr) =
    case MemInt (RegAddrWidth r) -> MemInt (RegAddrWidth r) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare MemInt (RegAddrWidth r)
xi MemInt (RegAddrWidth r)
yi of
      Ordering
LT -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
      Ordering
GT -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
      Ordering
EQ -> MemRepr x -> MemRepr y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
MemRepr x -> MemRepr y -> OrderingF x y
compareF MemRepr x
xr MemRepr y
yr

instance ShowF r => Pretty (BoundLoc r tp) where
  pretty :: forall ann. BoundLoc r tp -> Doc ann
pretty (RegLoc r tp
r) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (r tp -> String
forall k (f :: k -> Type) (tp :: k). ShowF f => f tp -> String
forall (tp :: Type). r tp -> String
showF r tp
r)
  pretty (StackOffLoc MemInt (RegAddrWidth r)
i MemRepr tp
tp) = MemInt (RegAddrWidth r) -> MemRepr tp -> Doc ann
forall (w :: Natural) (tp :: Type) ann.
MemInt w -> MemRepr tp -> Doc ann
ppStackOff MemInt (RegAddrWidth r)
i MemRepr tp
tp

instance ShowF r => PrettyF (BoundLoc r) where
  prettyF :: forall (tp :: Type) ann. BoundLoc r tp -> Doc ann
prettyF = BoundLoc r tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BoundLoc r tp -> Doc ann
pretty

instance ShowF r => Show (BoundLoc r tp) where
  show :: BoundLoc r tp -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (BoundLoc r tp -> Doc Any) -> BoundLoc r tp -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BoundLoc r tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. BoundLoc r tp -> Doc ann
pretty

instance ShowF r => ShowF (BoundLoc r)

instance TestEquality r => Eq (BoundLoc r tp) where
  BoundLoc r tp
x == :: BoundLoc r tp -> BoundLoc r tp -> Bool
== BoundLoc r tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (BoundLoc r tp -> BoundLoc r 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).
BoundLoc r a -> BoundLoc r b -> Maybe (a :~: b)
testEquality BoundLoc r tp
x BoundLoc r tp
y)

------------------------------------------------------------------------
-- MemMap

-- | This is a data structure for representing values written to
-- concrete offsets in memory.
--
-- The offset type is a parameter so that we can use signed or
-- unsigned offsets.
newtype MemMap o (v :: M.Type -> Type) = SM (Map o (MemVal v))

instance FunctorF (MemMap o) where
  fmapF :: forall (f :: Type -> Type) (g :: Type -> Type).
(forall (x :: Type). f x -> g x) -> MemMap o f -> MemMap o g
fmapF forall (x :: Type). f x -> g x
f (SM Map o (MemVal f)
m) = Map o (MemVal g) -> MemMap o g
forall o (v :: Type -> Type). Map o (MemVal v) -> MemMap o v
SM ((MemVal f -> MemVal g) -> Map o (MemVal f) -> Map o (MemVal g)
forall a b. (a -> b) -> Map o a -> Map o b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall (x :: Type). f x -> g x) -> MemVal f -> MemVal g
forall {k} (m :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorF m =>
(forall (x :: k). f x -> g x) -> m f -> m g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall (x :: Type). f x -> g x) -> MemVal f -> MemVal g
fmapF f x -> g x
forall (x :: Type). f x -> g x
f) Map o (MemVal f)
m)

-- | Empty stack map
emptyMemMap :: MemMap o v
emptyMemMap :: forall o (v :: Type -> Type). MemMap o v
emptyMemMap = Map o (MemVal v) -> MemMap o v
forall o (v :: Type -> Type). Map o (MemVal v) -> MemMap o v
SM Map o (MemVal v)
forall k a. Map k a
Map.empty

memMapNull :: MemMap o v -> Bool
memMapNull :: forall o (v :: Type -> Type). MemMap o v -> Bool
memMapNull (SM Map o (MemVal v)
m) = Map o (MemVal v) -> Bool
forall k a. Map k a -> Bool
Map.null Map o (MemVal v)
m

-- | Result returned by @memMapLookup@.
data MemMapLookup o p tp where
  -- | We found a value at the exact offset and repr
  MMLResult :: !(p tp) -> MemMapLookup o p tp
  -- | We found a value that had an overlapping offset and repr.
  MMLOverlap  :: !o
              -> !(MemRepr utp)
              -> !(p utp)
              -> MemMapLookup o p tp
  -- | We found neither an exact match nor an overlapping write.
  MMLNone :: MemMapLookup o p tp

class Ord o => MemIndex o where
  -- | @endOffset o w@ returns @Just (o + w)@ if it can be computed
  -- without overflowing.
  endOffset :: o -> Natural -> Maybe o

  -- | @memOverlap b r i@ returns @True@ if @i \in [b..b+sizeof r)@.
  memOverlap :: o -> MemRepr tp -> o -> Bool

instance MemWidth w => MemIndex (MemInt w) where
  endOffset :: MemInt w -> Natural -> Maybe (MemInt w)
endOffset MemInt w
off Natural
sz | MemInt w -> Integer
forall a. Integral a => a -> Integer
toInteger MemInt w
endI Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
end = MemInt w -> Maybe (MemInt w)
forall a. a -> Maybe a
Just MemInt w
endI
                   | Bool
otherwise = Maybe (MemInt w)
forall a. Maybe a
Nothing
    where end :: Integer
end = MemInt w -> Integer
forall a. Integral a => a -> Integer
toInteger MemInt w
off Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
sz
          endI :: MemInt w
endI = Integer -> MemInt w
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
end
  memOverlap :: forall (tp :: Type). MemInt w -> MemRepr tp -> MemInt w -> Bool
memOverlap MemInt w
b MemRepr tp
r MemInt w
i
    = MemInt w
b MemInt w -> MemInt w -> Bool
forall a. Ord a => a -> a -> Bool
<= MemInt w
i
    Bool -> Bool -> Bool
&& Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger (MemInt w -> Int64
forall (w :: Natural). MemInt w -> Int64
memIntValue MemInt w
i)
       Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<  Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger (MemInt w -> Int64
forall (w :: Natural). MemInt w -> Int64
memIntValue MemInt w
b) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (MemRepr tp -> Natural
forall (tp :: Type). MemRepr tp -> Natural
memReprBytes MemRepr tp
r)

-- | Lookup value (if any) at given offset and representation.
--
-- This generalized @memMapLookup@ below to not require exact matches, but
-- just some overlap.
memMapLookup' :: MemIndex o
              => o
              -> MemRepr tp
              -> MemMap o v
              -> Maybe (o, MemVal v)
memMapLookup' :: forall o (tp :: Type) (v :: Type -> Type).
MemIndex o =>
o -> MemRepr tp -> MemMap o v -> Maybe (o, MemVal v)
memMapLookup' o
off MemRepr tp
repr (SM Map o (MemVal v)
m) =  do
  case o -> Natural -> Maybe o
forall o. MemIndex o => o -> Natural -> Maybe o
endOffset o
off (MemRepr tp -> Natural
forall (tp :: Type). MemRepr tp -> Natural
memReprBytes MemRepr tp
repr) of
    Maybe o
Nothing -> Maybe (o, MemVal v)
forall a. Maybe a
Nothing
    Just o
end ->
      case o -> Map o (MemVal v) -> Maybe (o, MemVal v)
forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupLT o
end Map o (MemVal v)
m of
        Just p :: (o, MemVal v)
p@(o
oldOff, MemVal MemRepr tp
oldRepr v tp
_)
          | o -> MemRepr tp -> o -> Bool
forall o (tp :: Type). MemIndex o => o -> MemRepr tp -> o -> Bool
forall (tp :: Type). o -> MemRepr tp -> o -> Bool
memOverlap o
oldOff MemRepr tp
oldRepr o
off -> (o, MemVal v) -> Maybe (o, MemVal v)
forall a. a -> Maybe a
Just (o, MemVal v)
p
        Maybe (o, MemVal v)
_ -> Maybe (o, MemVal v)
forall a. Maybe a
Nothing

-- | Lookup value (if any) at given offset and representation.
memMapLookup :: MemIndex o
             => o
             -> MemRepr tp
             -> MemMap o p
             -> MemMapLookup o p tp
memMapLookup :: forall o (tp :: Type) (p :: Type -> Type).
MemIndex o =>
o -> MemRepr tp -> MemMap o p -> MemMapLookup o p tp
memMapLookup o
off MemRepr tp
repr (SM Map o (MemVal p)
m) =  do
  case o -> Natural -> Maybe o
forall o. MemIndex o => o -> Natural -> Maybe o
endOffset o
off (MemRepr tp -> Natural
forall (tp :: Type). MemRepr tp -> Natural
memReprBytes MemRepr tp
repr) of
    Maybe o
Nothing -> MemMapLookup o p tp
forall o (p :: Type -> Type) (tp :: Type). MemMapLookup o p tp
MMLNone
    Just o
end ->
      case o -> Map o (MemVal p) -> Maybe (o, MemVal p)
forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupLT o
end Map o (MemVal p)
m of
        Maybe (o, MemVal p)
Nothing -> MemMapLookup o p tp
forall o (p :: Type -> Type) (tp :: Type). MemMapLookup o p tp
MMLNone
        Just (o
oldOff, MemVal MemRepr tp
oldRepr p tp
val)
          -- If match exact
          | o
oldOff o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== o
off
          , 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
oldRepr MemRepr tp
repr ->
          p tp -> MemMapLookup o p tp
forall (p :: Type -> Type) (tp :: Type) o.
p tp -> MemMapLookup o p tp
MMLResult p tp
p tp
val
          -- If previous write ends after this write starts
          | o -> MemRepr tp -> o -> Bool
forall o (tp :: Type). MemIndex o => o -> MemRepr tp -> o -> Bool
forall (tp :: Type). o -> MemRepr tp -> o -> Bool
memOverlap o
oldOff MemRepr tp
oldRepr o
off ->
            o -> MemRepr tp -> p tp -> MemMapLookup o p tp
forall o (u :: Type) (p :: Type -> Type) (tp :: Type).
o -> MemRepr u -> p u -> MemMapLookup o p tp
MMLOverlap o
oldOff MemRepr tp
oldRepr p tp
val
          | Bool
otherwise ->
            MemMapLookup o p tp
forall o (p :: Type -> Type) (tp :: Type). MemMapLookup o p tp
MMLNone

-- | This assigns a region of bytes to a particular value in the stack.
--
-- It overwrites any values that overlap with the location.
memMapOverwrite :: forall o p tp
                .  (Ord o, Num o)
                => o -- ^ Offset in the stack to write to
                -> MemRepr tp -- ^ Type of value to write
                -> p tp  -- ^ Value to write
                -> MemMap o p
                -> MemMap o p
memMapOverwrite :: forall o (p :: Type -> Type) (tp :: Type).
(Ord o, Num o) =>
o -> MemRepr tp -> p tp -> MemMap o p -> MemMap o p
memMapOverwrite o
off MemRepr tp
repr p tp
v (SM Map o (MemVal p)
m) =
   let e :: o
e = o
off o -> o -> o
forall a. Num a => a -> a -> a
+ Natural -> o
forall a b. (Integral a, Num b) => a -> b
fromIntegral (MemRepr tp -> Natural
forall (tp :: Type). MemRepr tp -> Natural
memReprBytes MemRepr tp
repr) o -> o -> o
forall a. Num a => a -> a -> a
- o
1
       (Map o (MemVal p)
lm, Map o (MemVal p)
_) = o -> Map o (MemVal p) -> (Map o (MemVal p), Map o (MemVal p))
forall k a. Ord k => k -> Map k a -> (Map k a, Map k a)
Map.split o
off Map o (MemVal p)
m
       hm :: Map o (MemVal p)
hm | o
off o -> o -> Bool
forall a. Ord a => a -> a -> Bool
<= o
e = (Map o (MemVal p), Map o (MemVal p)) -> Map o (MemVal p)
forall a b. (a, b) -> b
snd (o -> Map o (MemVal p) -> (Map o (MemVal p), Map o (MemVal p))
forall k a. Ord k => k -> Map k a -> (Map k a, Map k a)
Map.split o
e Map o (MemVal p)
m)
          | Bool
otherwise = Map o (MemVal p)
forall k a. Map k a
Map.empty
    in Map o (MemVal p) -> MemMap o p
forall o (v :: Type -> Type). Map o (MemVal v) -> MemMap o v
SM (Map o (MemVal p) -> MemMap o p) -> Map o (MemVal p) -> MemMap o p
forall a b. (a -> b) -> a -> b
$ o -> MemVal p -> Map o (MemVal p) -> Map o (MemVal p)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert o
off (MemRepr tp -> p tp -> MemVal p
forall (p :: Type -> Type) (tp :: Type).
MemRepr tp -> p tp -> MemVal p
MemVal MemRepr tp
repr p tp
v) Map o (MemVal p)
lm Map o (MemVal p) -> Map o (MemVal p) -> Map o (MemVal p)
forall a. Semigroup a => a -> a -> a
<> Map o (MemVal p)
hm

-- | This sets the value at an offset without checking to clear any
-- previous writes to values.
unsafeMemMapInsert :: Ord o => o -> MemRepr tp -> p tp -> MemMap o p -> MemMap o p
unsafeMemMapInsert :: forall o (tp :: Type) (p :: Type -> Type).
Ord o =>
o -> MemRepr tp -> p tp -> MemMap o p -> MemMap o p
unsafeMemMapInsert o
o MemRepr tp
repr p tp
v (SM Map o (MemVal p)
m) = Map o (MemVal p) -> MemMap o p
forall o (v :: Type -> Type). Map o (MemVal v) -> MemMap o v
SM (o -> MemVal p -> Map o (MemVal p) -> Map o (MemVal p)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert o
o (MemRepr tp -> p tp -> MemVal p
forall (p :: Type -> Type) (tp :: Type).
MemRepr tp -> p tp -> MemVal p
MemVal MemRepr tp
repr p tp
v) Map o (MemVal p)
m)

memMapFoldlWithKey :: (forall tp . r -> o -> MemRepr tp -> v tp -> r)
                   -> r
                   -> MemMap o v
                   -> r
memMapFoldlWithKey :: forall r o (v :: Type -> Type).
(forall (tp :: Type). r -> o -> MemRepr tp -> v tp -> r)
-> r -> MemMap o v -> r
memMapFoldlWithKey forall (tp :: Type). r -> o -> MemRepr tp -> v tp -> r
f r
z (SM Map o (MemVal v)
m) =
  (r -> o -> MemVal v -> r) -> r -> Map o (MemVal v) -> r
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey (\r
r o
k (MemVal MemRepr tp
repr v tp
v) -> r -> o -> MemRepr tp -> v tp -> r
forall (tp :: Type). r -> o -> MemRepr tp -> v tp -> r
f r
r o
k MemRepr tp
repr v tp
v) r
z Map o (MemVal v)
m

memMapFoldrWithKey :: (forall tp . o -> MemRepr tp -> v tp -> r -> r)
                   -> r
                   -> MemMap o v
                   -> r
memMapFoldrWithKey :: forall o (v :: Type -> Type) r.
(forall (tp :: Type). o -> MemRepr tp -> v tp -> r -> r)
-> r -> MemMap o v -> r
memMapFoldrWithKey forall (tp :: Type). o -> MemRepr tp -> v tp -> r -> r
f r
z (SM Map o (MemVal v)
m) =
  (o -> MemVal v -> r -> r) -> r -> Map o (MemVal v) -> r
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\o
k (MemVal MemRepr tp
repr v tp
v) r
r -> o -> MemRepr tp -> v tp -> r -> r
forall (tp :: Type). o -> MemRepr tp -> v tp -> r -> r
f o
k MemRepr tp
repr v tp
v r
r) r
z Map o (MemVal v)
m

memMapTraverseWithKey_ :: Applicative m
                       => (forall tp . o -> MemRepr tp -> v tp -> m ())
                       -> MemMap o v
                       -> m ()
memMapTraverseWithKey_ :: forall (m :: Type -> Type) o (v :: Type -> Type).
Applicative m =>
(forall (tp :: Type). o -> MemRepr tp -> v tp -> m ())
-> MemMap o v -> m ()
memMapTraverseWithKey_ forall (tp :: Type). o -> MemRepr tp -> v tp -> m ()
f (SM Map o (MemVal v)
m) =
  (o -> MemVal v -> m () -> m ()) -> m () -> Map o (MemVal v) -> m ()
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\o
k (MemVal MemRepr tp
repr v tp
v) m ()
r -> o -> MemRepr tp -> v tp -> m ()
forall (tp :: Type). o -> MemRepr tp -> v tp -> m ()
f o
k MemRepr tp
repr v tp
v m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> m ()
r) (() -> m ()
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()) Map o (MemVal v)
m

memMapMapWithKey :: (forall tp . o -> MemRepr tp -> a tp -> b tp)
                 -> MemMap o a
                 -> MemMap o b
memMapMapWithKey :: forall o (a :: Type -> Type) (b :: Type -> Type).
(forall (tp :: Type). o -> MemRepr tp -> a tp -> b tp)
-> MemMap o a -> MemMap o b
memMapMapWithKey forall (tp :: Type). o -> MemRepr tp -> a tp -> b tp
f (SM Map o (MemVal a)
m) =
  Map o (MemVal b) -> MemMap o b
forall o (v :: Type -> Type). Map o (MemVal v) -> MemMap o v
SM ((o -> MemVal a -> MemVal b) -> Map o (MemVal a) -> Map o (MemVal b)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\o
o (MemVal MemRepr tp
repr a tp
v) -> MemRepr tp -> b tp -> MemVal b
forall (p :: Type -> Type) (tp :: Type).
MemRepr tp -> p tp -> MemVal p
MemVal MemRepr tp
repr (o -> MemRepr tp -> a tp -> b tp
forall (tp :: Type). o -> MemRepr tp -> a tp -> b tp
f o
o MemRepr tp
repr a tp
v)) Map o (MemVal a)
m)

memMapTraverseMaybeWithKey
  :: Applicative m
  => (forall tp . o -> MemRepr tp -> a tp -> m (Maybe (b tp)))
  -- ^ Traversal function
  -> MemMap o a
  -> m (MemMap o b)
memMapTraverseMaybeWithKey :: forall (m :: Type -> Type) o (a :: Type -> Type)
       (b :: Type -> Type).
Applicative m =>
(forall (tp :: Type). o -> MemRepr tp -> a tp -> m (Maybe (b tp)))
-> MemMap o a -> m (MemMap o b)
memMapTraverseMaybeWithKey forall (tp :: Type). o -> MemRepr tp -> a tp -> m (Maybe (b tp))
f (SM Map o (MemVal a)
m) =
  Map o (MemVal b) -> MemMap o b
forall o (v :: Type -> Type). Map o (MemVal v) -> MemMap o v
SM (Map o (MemVal b) -> MemMap o b)
-> m (Map o (MemVal b)) -> m (MemMap o b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (o -> MemVal a -> m (Maybe (MemVal b)))
-> Map o (MemVal a) -> m (Map o (MemVal b))
forall (f :: Type -> Type) k a b.
Applicative f =>
(k -> a -> f (Maybe b)) -> Map k a -> f (Map k b)
Map.traverseMaybeWithKey
       (\o
o (MemVal MemRepr tp
repr a tp
v) -> (b tp -> MemVal b) -> Maybe (b tp) -> Maybe (MemVal b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (MemRepr tp -> b tp -> MemVal b
forall (p :: Type -> Type) (tp :: Type).
MemRepr tp -> p tp -> MemVal p
MemVal MemRepr tp
repr) (Maybe (b tp) -> Maybe (MemVal b))
-> m (Maybe (b tp)) -> m (Maybe (MemVal b))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> o -> MemRepr tp -> a tp -> m (Maybe (b tp))
forall (tp :: Type). o -> MemRepr tp -> a tp -> m (Maybe (b tp))
f o
o MemRepr tp
repr a tp
v) Map o (MemVal a)
m

-- @memMapDropAbove bnd m@ includes only entries in @m@ whose bytes
-- do not go above @bnd@.
memMapDropAbove :: Integral o => Integer -> MemMap o p -> MemMap o p
memMapDropAbove :: forall o (p :: Type -> Type).
Integral o =>
Integer -> MemMap o p -> MemMap o p
memMapDropAbove Integer
bnd (SM Map o (MemVal p)
m) = Map o (MemVal p) -> MemMap o p
forall o (v :: Type -> Type). Map o (MemVal v) -> MemMap o v
SM ((o -> MemVal p -> Bool) -> Map o (MemVal p) -> Map o (MemVal p)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey o -> MemVal p -> Bool
p Map o (MemVal p)
m)
  where p :: o -> MemVal p -> Bool
p o
o (MemVal MemRepr tp
r p tp
_) = o -> Integer
forall a. Integral a => a -> Integer
toInteger o
o  Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (MemRepr tp -> Natural
forall (tp :: Type). MemRepr tp -> Natural
memReprBytes MemRepr tp
r) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
bnd

-- @memMapDropBelow bnd m@ includes only entries in @m@ whose bytes
-- do not go below @bnd@.
memMapDropBelow :: Integral o => Integer -> MemMap o p -> MemMap o p
memMapDropBelow :: forall o (p :: Type -> Type).
Integral o =>
Integer -> MemMap o p -> MemMap o p
memMapDropBelow Integer
bnd (SM Map o (MemVal p)
m) = Map o (MemVal p) -> MemMap o p
forall o (v :: Type -> Type). Map o (MemVal v) -> MemMap o v
SM ((o -> MemVal p -> Bool) -> Map o (MemVal p) -> Map o (MemVal p)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey o -> MemVal p -> Bool
p Map o (MemVal p)
m)
  where p :: o -> MemVal p -> Bool
p o
o MemVal p
_ = o -> Integer
forall a. Integral a => a -> Integer
toInteger o
o Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
bnd

------------------------------------------------------------------------
-- LocMap

-- | A map from `BoundLoc` locations to values.
data LocMap (r :: M.Type -> Type) (v :: M.Type -> Type)
  = LocMap { forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MapF r v
locMapRegs :: !(MapF r v)
           , forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
locMapStack :: !(MemMap (MemInt (RegAddrWidth r)) v)
           }

-- | Return true if map is null.
locMapNull :: LocMap r v -> Bool
locMapNull :: forall (r :: Type -> Type) (v :: Type -> Type). LocMap r v -> Bool
locMapNull LocMap r v
m
  = MapF r v -> Bool
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a -> Bool
MapF.null (LocMap r v -> MapF r v
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MapF r v
locMapRegs LocMap r v
m)
  Bool -> Bool -> Bool
&& MemMap (MemInt (RegAddrWidth r)) v -> Bool
forall o (v :: Type -> Type). MemMap o v -> Bool
memMapNull (LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
locMapStack LocMap r v
m)

-- | An empty location map.
locMapEmpty :: LocMap r v
locMapEmpty :: forall (r :: Type -> Type) (v :: Type -> Type). LocMap r v
locMapEmpty = LocMap { locMapRegs :: MapF r v
locMapRegs  = MapF r v
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
                     , locMapStack :: MemMap (MemInt (RegAddrWidth r)) v
locMapStack = MemMap (MemInt (RegAddrWidth r)) v
forall o (v :: Type -> Type). MemMap o v
emptyMemMap
                     }

-- | Construct a list out of a location map.
locMapToList :: forall r v . LocMap r v -> [Pair (BoundLoc r) v]
locMapToList :: forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> [Pair (BoundLoc r) v]
locMapToList LocMap r v
m0 =
  let prependRegPair :: r tp -> b tp -> [Pair (BoundLoc r) b] -> [Pair (BoundLoc r) b]
prependRegPair r tp
r b tp
v [Pair (BoundLoc r) b]
z = BoundLoc r tp -> b tp -> Pair (BoundLoc r) b
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (r tp -> BoundLoc r tp
forall (r :: Type -> Type) (tp :: Type). r tp -> BoundLoc r tp
RegLoc r tp
r) b tp
v Pair (BoundLoc r) b
-> [Pair (BoundLoc r) b] -> [Pair (BoundLoc r) b]
forall a. a -> [a] -> [a]
: [Pair (BoundLoc r) b]
z
      prependStackPair :: MemInt (RegAddrWidth r)
-> MemRepr tp
-> b tp
-> [Pair (BoundLoc r) b]
-> [Pair (BoundLoc r) b]
prependStackPair MemInt (RegAddrWidth r)
i MemRepr tp
repr b tp
v [Pair (BoundLoc r) b]
z = BoundLoc r tp -> b tp -> Pair (BoundLoc r) b
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (MemInt (RegAddrWidth r) -> MemRepr tp -> BoundLoc r tp
forall (r :: Type -> Type) (tp :: Type).
MemInt (RegAddrWidth r) -> MemRepr tp -> BoundLoc r tp
StackOffLoc MemInt (RegAddrWidth r)
i MemRepr tp
repr) b tp
v Pair (BoundLoc r) b
-> [Pair (BoundLoc r) b] -> [Pair (BoundLoc r) b]
forall a. a -> [a] -> [a]
: [Pair (BoundLoc r) b]
z
   in ([Pair (BoundLoc r) v] -> MapF r v -> [Pair (BoundLoc r) v])
-> MapF r v -> [Pair (BoundLoc r) v] -> [Pair (BoundLoc r) v]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((forall (s :: Type).
 r s -> v s -> [Pair (BoundLoc r) v] -> [Pair (BoundLoc r) v])
-> [Pair (BoundLoc r) v] -> MapF r v -> [Pair (BoundLoc r) v]
forall {v} (k :: v -> Type) (a :: v -> Type) b.
(forall (s :: v). k s -> a s -> b -> b) -> b -> MapF k a -> b
MapF.foldrWithKey r s -> v s -> [Pair (BoundLoc r) v] -> [Pair (BoundLoc r) v]
forall (s :: Type).
r s -> v s -> [Pair (BoundLoc r) v] -> [Pair (BoundLoc r) v]
forall {r :: Type -> Type} {tp :: Type} {b :: Type -> Type}.
r tp -> b tp -> [Pair (BoundLoc r) b] -> [Pair (BoundLoc r) b]
prependRegPair) (LocMap r v -> MapF r v
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MapF r v
locMapRegs LocMap r v
m0) ([Pair (BoundLoc r) v] -> [Pair (BoundLoc r) v])
-> [Pair (BoundLoc r) v] -> [Pair (BoundLoc r) v]
forall a b. (a -> b) -> a -> b
$
      ([Pair (BoundLoc r) v]
 -> MemMap (MemInt (RegAddrWidth r)) v -> [Pair (BoundLoc r) v])
-> MemMap (MemInt (RegAddrWidth r)) v
-> [Pair (BoundLoc r) v]
-> [Pair (BoundLoc r) v]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((forall (tp :: Type).
 MemInt (RegAddrWidth r)
 -> MemRepr tp
 -> v tp
 -> [Pair (BoundLoc r) v]
 -> [Pair (BoundLoc r) v])
-> [Pair (BoundLoc r) v]
-> MemMap (MemInt (RegAddrWidth r)) v
-> [Pair (BoundLoc r) v]
forall o (v :: Type -> Type) r.
(forall (tp :: Type). o -> MemRepr tp -> v tp -> r -> r)
-> r -> MemMap o v -> r
memMapFoldrWithKey MemInt (RegAddrWidth r)
-> MemRepr tp
-> v tp
-> [Pair (BoundLoc r) v]
-> [Pair (BoundLoc r) v]
forall (tp :: Type).
MemInt (RegAddrWidth r)
-> MemRepr tp
-> v tp
-> [Pair (BoundLoc r) v]
-> [Pair (BoundLoc r) v]
forall {r :: Type -> Type} {tp :: Type} {b :: Type -> Type}.
MemInt (RegAddrWidth r)
-> MemRepr tp
-> b tp
-> [Pair (BoundLoc r) b]
-> [Pair (BoundLoc r) b]
prependStackPair) (LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
locMapStack LocMap r v
m0) ([Pair (BoundLoc r) v] -> [Pair (BoundLoc r) v])
-> [Pair (BoundLoc r) v] -> [Pair (BoundLoc r) v]
forall a b. (a -> b) -> a -> b
$
      []

-- | Fold over values in a location map.
foldLocMap :: forall a r v
           .  (forall tp . a -> BoundLoc r tp -> v tp -> a)
           -> a
           -> LocMap r v
           -> a
foldLocMap :: forall a (r :: Type -> Type) (v :: Type -> Type).
(forall (tp :: Type). a -> BoundLoc r tp -> v tp -> a)
-> a -> LocMap r v -> a
foldLocMap forall (tp :: Type). a -> BoundLoc r tp -> v tp -> a
f a
a0 LocMap r v
m0 =
  (a -> MemMap (MemInt (RegAddrWidth r)) v -> a)
-> MemMap (MemInt (RegAddrWidth r)) v -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((forall (tp :: Type).
 a -> MemInt (RegAddrWidth r) -> MemRepr tp -> v tp -> a)
-> a -> MemMap (MemInt (RegAddrWidth r)) v -> a
forall r o (v :: Type -> Type).
(forall (tp :: Type). r -> o -> MemRepr tp -> v tp -> r)
-> r -> MemMap o v -> r
memMapFoldlWithKey (\a
a MemInt (RegAddrWidth r)
o MemRepr tp
r v tp
v -> a -> BoundLoc r tp -> v tp -> a
forall (tp :: Type). a -> BoundLoc r tp -> v tp -> a
f a
a (MemInt (RegAddrWidth r) -> MemRepr tp -> BoundLoc r tp
forall (r :: Type -> Type) (tp :: Type).
MemInt (RegAddrWidth r) -> MemRepr tp -> BoundLoc r tp
StackOffLoc MemInt (RegAddrWidth r)
o MemRepr tp
r) v tp
v)) (LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
locMapStack LocMap r v
m0) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$
  (a -> MapF r v -> a) -> MapF r v -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((forall (s :: Type). a -> r s -> v s -> a) -> a -> MapF r v -> a
forall {v} b (k :: v -> Type) (a :: v -> Type).
(forall (s :: v). b -> k s -> a s -> b) -> b -> MapF k a -> b
MapF.foldlWithKey (\a
a r s
r v s
v -> a -> BoundLoc r s -> v s -> a
forall (tp :: Type). a -> BoundLoc r tp -> v tp -> a
f a
a (r s -> BoundLoc r s
forall (r :: Type -> Type) (tp :: Type). r tp -> BoundLoc r tp
RegLoc r s
r) v s
v)) (LocMap r v -> MapF r v
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MapF r v
locMapRegs LocMap r v
m0) a
a0

locMapTraverseWithKey_ :: forall m r p
                       .  Applicative m
                       => (forall tp . BoundLoc r tp -> p tp -> m ())
                       -> LocMap r p
                       -> m ()
locMapTraverseWithKey_ :: forall (m :: Type -> Type) (r :: Type -> Type) (p :: Type -> Type).
Applicative m =>
(forall (tp :: Type). BoundLoc r tp -> p tp -> m ())
-> LocMap r p -> m ()
locMapTraverseWithKey_ forall (tp :: Type). BoundLoc r tp -> p tp -> m ()
f LocMap r p
m0 = do
  let regFn :: r utp -> p utp -> m ()
      regFn :: forall (utp :: Type). r utp -> p utp -> m ()
regFn r utp
r p utp
v = BoundLoc r utp -> p utp -> m ()
forall (tp :: Type). BoundLoc r tp -> p tp -> m ()
f (r utp -> BoundLoc r utp
forall (r :: Type -> Type) (tp :: Type). r tp -> BoundLoc r tp
RegLoc r utp
r) p utp
v
      stackFn :: MemInt (RegAddrWidth r) -> MemRepr utp -> p utp -> m ()
      stackFn :: forall (utp :: Type).
MemInt (RegAddrWidth r) -> MemRepr utp -> p utp -> m ()
stackFn MemInt (RegAddrWidth r)
o MemRepr utp
r p utp
c = BoundLoc r utp -> p utp -> m ()
forall (tp :: Type). BoundLoc r tp -> p tp -> m ()
f (MemInt (RegAddrWidth r) -> MemRepr utp -> BoundLoc r utp
forall (r :: Type -> Type) (tp :: Type).
MemInt (RegAddrWidth r) -> MemRepr tp -> BoundLoc r tp
StackOffLoc MemInt (RegAddrWidth r)
o MemRepr utp
r) p utp
c
  (forall (utp :: Type). r utp -> p utp -> m ()) -> MapF r p -> m ()
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m ()) -> MapF ktp f -> m ()
MapF.traverseWithKey_ r tp -> p tp -> m ()
forall (utp :: Type). r utp -> p utp -> m ()
regFn (LocMap r p -> MapF r p
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MapF r v
locMapRegs LocMap r p
m0)
   m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> (forall (utp :: Type).
 MemInt (RegAddrWidth r) -> MemRepr utp -> p utp -> m ())
-> MemMap (MemInt (RegAddrWidth r)) p -> m ()
forall (m :: Type -> Type) o (v :: Type -> Type).
Applicative m =>
(forall (tp :: Type). o -> MemRepr tp -> v tp -> m ())
-> MemMap o v -> m ()
memMapTraverseWithKey_ MemInt (RegAddrWidth r) -> MemRepr tp -> p tp -> m ()
forall (utp :: Type).
MemInt (RegAddrWidth r) -> MemRepr utp -> p utp -> m ()
stackFn (LocMap r p -> MemMap (MemInt (RegAddrWidth r)) p
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
locMapStack LocMap r p
m0)

-- | Pretty print a location map.
ppLocMap :: ShowF r => (forall tp . Doc ann -> p tp -> Doc ann) -> LocMap r p -> [Doc ann]
ppLocMap :: 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 forall (tp :: Type). Doc ann -> p tp -> Doc ann
f LocMap r p
m =
  let ppPair :: Pair (BoundLoc r) p -> Doc ann
ppPair (Pair BoundLoc r tp
l p tp
v) = Doc ann -> p tp -> Doc ann
forall (tp :: Type). Doc ann -> p tp -> Doc ann
f (BoundLoc r tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BoundLoc r tp -> Doc ann
pretty BoundLoc r tp
l) p tp
v
   in Pair (BoundLoc r) p -> Doc ann
ppPair (Pair (BoundLoc r) p -> Doc ann)
-> [Pair (BoundLoc r) p] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> LocMap r p -> [Pair (BoundLoc r) p]
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> [Pair (BoundLoc r) v]
locMapToList LocMap r p
m

-- | Return value associated with location or nothing if it is not
-- defined.
locLookup :: (MemWidth (RegAddrWidth r), OrdF r)
          => BoundLoc r tp
          -> LocMap r v
          -> Maybe (v tp)
locLookup :: forall (r :: Type -> Type) (tp :: Type) (v :: Type -> Type).
(MemWidth (RegAddrWidth r), OrdF r) =>
BoundLoc r tp -> LocMap r v -> Maybe (v tp)
locLookup (RegLoc r tp
r) LocMap r v
m = r tp -> MapF r v -> Maybe (v tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup r tp
r (LocMap r v -> MapF r v
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MapF r v
locMapRegs LocMap r v
m)
locLookup (StackOffLoc MemInt (RegAddrWidth r)
o MemRepr tp
repr) LocMap r v
m =
  case MemInt (RegAddrWidth r)
-> MemRepr tp
-> MemMap (MemInt (RegAddrWidth r)) v
-> MemMapLookup (MemInt (RegAddrWidth r)) v tp
forall o (tp :: Type) (p :: Type -> Type).
MemIndex o =>
o -> MemRepr tp -> MemMap o p -> MemMapLookup o p tp
memMapLookup MemInt (RegAddrWidth r)
o MemRepr tp
repr (LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
locMapStack LocMap r v
m) of
    MMLResult v tp
r -> v tp -> Maybe (v tp)
forall a. a -> Maybe a
Just v tp
r
    MMLOverlap MemInt (RegAddrWidth r)
_ MemRepr utp
_ v utp
_ -> Maybe (v tp)
forall a. Maybe a
Nothing
    MemMapLookup (MemInt (RegAddrWidth r)) v tp
MMLNone -> Maybe (v tp)
forall a. Maybe a
Nothing

-- | This associates the location with a value in the map, replacing any existing binding.
--
-- It is prefixed with "nonOverlap" because it doesn't guarantee that stack
-- values are non-overlapping -- the user should ensure this before calling this.
nonOverlapLocInsert :: OrdF r => BoundLoc r tp -> v tp -> LocMap r v -> LocMap r v
nonOverlapLocInsert :: forall (r :: Type -> Type) (tp :: Type) (v :: Type -> Type).
OrdF r =>
BoundLoc r tp -> v tp -> LocMap r v -> LocMap r v
nonOverlapLocInsert (RegLoc r tp
r) v tp
v LocMap r v
m =
  LocMap r v
m { locMapRegs = MapF.insert r v (locMapRegs m) }
nonOverlapLocInsert (StackOffLoc MemInt (RegAddrWidth r)
off MemRepr tp
repr) v tp
v LocMap r v
m =
  LocMap r v
m { locMapStack = unsafeMemMapInsert off repr v (locMapStack m) }

locOverwriteWith :: (OrdF r, MemWidth (RegAddrWidth r))
                 => (v tp -> v tp -> v tp) -- ^ Update takes new and  old.
                 -> BoundLoc r tp
                 -> v tp
                 -> LocMap r v
                 -> LocMap r v
locOverwriteWith :: forall (r :: Type -> Type) (v :: Type -> Type) (tp :: Type).
(OrdF r, MemWidth (RegAddrWidth r)) =>
(v tp -> v tp -> v tp)
-> BoundLoc r tp -> v tp -> LocMap r v -> LocMap r v
locOverwriteWith v tp -> v tp -> v tp
upd (RegLoc r tp
r) v tp
v LocMap r v
m =
  LocMap r v
m { locMapRegs = MapF.insertWith upd r v (locMapRegs m) }
locOverwriteWith v tp -> v tp -> v tp
upd (StackOffLoc MemInt (RegAddrWidth r)
o MemRepr tp
repr) v tp
v LocMap r v
m =
  let nv :: v tp
nv = case MemInt (RegAddrWidth r)
-> MemRepr tp
-> MemMap (MemInt (RegAddrWidth r)) v
-> MemMapLookup (MemInt (RegAddrWidth r)) v tp
forall o (tp :: Type) (p :: Type -> Type).
MemIndex o =>
o -> MemRepr tp -> MemMap o p -> MemMapLookup o p tp
memMapLookup MemInt (RegAddrWidth r)
o MemRepr tp
repr (LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
locMapStack LocMap r v
m) of
             MemMapLookup (MemInt (RegAddrWidth r)) v tp
MMLNone -> v tp
v
             MMLOverlap MemInt (RegAddrWidth r)
_ MemRepr utp
_ v utp
_ -> v tp
v
             MMLResult v tp
oldv -> v tp -> v tp -> v tp
upd v tp
v v tp
oldv
   in LocMap r v
m { locMapStack = memMapOverwrite o repr nv (locMapStack m) }

------------------------------------------------------------------------
-- StackEqConstraint

-- | A constraint on the value stored in a location (i.e., register or
-- stack offset) at the start of block executino.
data StackEqConstraint r tp where
  -- | This indicates the value is equal to the frame pointer plus the
  -- given offset.
  --
  -- As stacks grow down on many architectures, the offset will
  -- typically be negative.
  IsStackOff :: !(MemInt (RegAddrWidth r)) -> StackEqConstraint r (BVType (RegAddrWidth r))
  -- | Indicates the value is equal to the value stored at the
  -- location.
  EqualLoc   :: !(BoundLoc r tp) -> StackEqConstraint r tp
  -- | Indicates the value is the unsigned extension of the value
  -- at another location.
  IsUExt :: (1 <= u, u+1 <= w)
         => !(BoundLoc r (BVType u))
         -> !(NatRepr w)
         -> StackEqConstraint r (BVType w)


ppStackEqConstraint :: ShowF r => Doc ann -> StackEqConstraint r tp -> Doc ann
ppStackEqConstraint :: forall (r :: Type -> Type) ann (tp :: Type).
ShowF r =>
Doc ann -> StackEqConstraint r tp -> Doc ann
ppStackEqConstraint Doc ann
d (IsStackOff MemInt (RegAddrWidth r)
i) =
  Doc ann
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"= stack_frame" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> MemInt (RegAddrWidth r) -> Doc ann
forall (w :: Natural) ann. MemInt w -> Doc ann
ppAddend MemInt (RegAddrWidth r)
i
ppStackEqConstraint Doc ann
d (EqualLoc   BoundLoc r tp
l) = Doc ann
d Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" = " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> BoundLoc r tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BoundLoc r tp -> Doc ann
pretty BoundLoc r tp
l
ppStackEqConstraint Doc ann
d (IsUExt BoundLoc r (BVType u)
l NatRepr w
w) = Doc ann
d Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" = (uext " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> BoundLoc r (BVType u) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BoundLoc r (BVType u) -> Doc ann
pretty BoundLoc r (BVType u)
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> NatRepr w -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr w
w Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
")"

------------------------------------------------------------------------
-- BlockStartStackConstraints

-- | Constraints on start of block.
--
-- This datatype maintains equality constraints between locations and
-- stack offsets.  It is used in jump bounds and other analysis
-- libraries where we want to know when two registers or stack
-- locations are equal.
newtype BlockStartStackConstraints arch =
  BSSC { forall arch.
BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
unBSSC :: LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch)) }

-- | Pretty print the lines in stack constraints.
ppBlockStartStackConstraints :: ShowF (ArchReg arch)
                             => BlockStartStackConstraints arch
                             -> [Doc ann]
ppBlockStartStackConstraints :: forall arch ann.
ShowF (ArchReg arch) =>
BlockStartStackConstraints arch -> [Doc ann]
ppBlockStartStackConstraints = (forall (tp :: Type).
 Doc ann -> StackEqConstraint (ArchReg arch) tp -> Doc ann)
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> [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 -> StackEqConstraint (ArchReg arch) tp -> Doc ann
forall (tp :: Type).
Doc ann -> StackEqConstraint (ArchReg arch) tp -> Doc ann
forall (r :: Type -> Type) ann (tp :: Type).
ShowF r =>
Doc ann -> StackEqConstraint r tp -> Doc ann
ppStackEqConstraint (LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
 -> [Doc ann])
-> (BlockStartStackConstraints arch
    -> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch)))
-> BlockStartStackConstraints arch
-> [Doc ann]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
forall arch.
BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
unBSSC

fnEntryBlockStartStackConstraints :: RegisterInfo (ArchReg arch)
                                  => BlockStartStackConstraints arch
fnEntryBlockStartStackConstraints :: forall arch.
RegisterInfo (ArchReg arch) =>
BlockStartStackConstraints arch
fnEntryBlockStartStackConstraints =
  BSSC { unBSSC :: LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
unBSSC =
           LocMap { locMapRegs :: MapF (ArchReg arch) (StackEqConstraint (ArchReg arch))
locMapRegs = ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
-> StackEqConstraint
     (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))
-> MapF (ArchReg arch) (StackEqConstraint (ArchReg arch))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
k tp -> a tp -> MapF k a
MapF.singleton ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
sp_reg (MemInt (RegAddrWidth (ArchReg arch))
-> StackEqConstraint
     (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
MemInt (RegAddrWidth r)
-> StackEqConstraint r (BVType (RegAddrWidth r))
IsStackOff MemInt (RegAddrWidth (ArchReg arch))
0)
                  , locMapStack :: MemMap
  (MemInt (RegAddrWidth (ArchReg arch)))
  (StackEqConstraint (ArchReg arch))
locMapStack = MemMap
  (MemInt (RegAddrWidth (ArchReg arch)))
  (StackEqConstraint (ArchReg arch))
forall o (v :: Type -> Type). MemMap o v
emptyMemMap
                  }
       }

-- | @blockStartLocStackOffset c l@ determines if @l@ has the form @stack_frame + o@
-- using the constraints @c@ for some stack offset @o@.
--
-- If it does, then this returns @Just o@.  Otherwise it returns @Nothing@.
blockStartLocStackOffset :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch))
                         => BlockStartStackConstraints arch
                         -> BoundLoc (ArchReg arch) tp
                         -> Maybe (MemInt (ArchAddrWidth arch))
blockStartLocStackOffset :: forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> Maybe (MemInt (ArchAddrWidth arch))
blockStartLocStackOffset BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) tp
loc =
  case BoundLoc (ArchReg arch) tp
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> Maybe (StackEqConstraint (ArchReg arch) 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 (BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
forall arch.
BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
unBSSC BlockStartStackConstraints arch
cns) of
    Maybe (StackEqConstraint (ArchReg arch) tp)
Nothing -> Maybe (MemInt (ArchAddrWidth arch))
forall a. Maybe a
Nothing
    Just (IsStackOff MemInt (ArchAddrWidth arch)
o) -> MemInt (ArchAddrWidth arch) -> Maybe (MemInt (ArchAddrWidth arch))
forall a. a -> Maybe a
Just MemInt (ArchAddrWidth arch)
o
    Just (EqualLoc BoundLoc (ArchReg arch) tp
loc') -> BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> Maybe (MemInt (ArchAddrWidth arch))
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> Maybe (MemInt (ArchAddrWidth arch))
blockStartLocStackOffset BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) tp
loc'
    -- Unsigned extensions cannot be stack offsets.
    Just (IsUExt BoundLoc (ArchReg arch) (BVType u)
_ NatRepr w
_) -> Maybe (MemInt (ArchAddrWidth arch))
forall a. Maybe a
Nothing

-- | Constraint on a class representative
data StackOffConstraint r tp where
  StackOffCns :: !(MemInt (RegAddrWidth r)) -> StackOffConstraint r (BVType (RegAddrWidth r))
  UExtCns :: (1 <= u, u+1 <= w)
          => !(BoundLoc r (BVType u))
          -> !(NatRepr w)
          -> StackOffConstraint r (BVType w)

instance TestEquality r => Eq (StackOffConstraint r tp) where
  StackOffCns MemInt (RegAddrWidth r)
i == :: StackOffConstraint r tp -> StackOffConstraint r tp -> Bool
== StackOffCns MemInt (RegAddrWidth r)
j = MemInt (RegAddrWidth r)
i MemInt (RegAddrWidth r) -> MemInt (RegAddrWidth r) -> Bool
forall a. Eq a => a -> a -> Bool
== MemInt (RegAddrWidth r)
j
  UExtCns BoundLoc r (BVType u)
xl NatRepr w
_ == UExtCns BoundLoc r (BVType u)
yl NatRepr w
_ =
    case BoundLoc r (BVType u)
-> BoundLoc r (BVType u) -> Maybe (BVType u :~: BVType u)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
BoundLoc r a -> BoundLoc r b -> Maybe (a :~: b)
testEquality BoundLoc r (BVType u)
xl BoundLoc r (BVType u)
yl of
      Just BVType u :~: BVType u
Refl -> Bool
True
      Maybe (BVType u :~: BVType u)
Nothing  -> Bool
False
  StackOffConstraint r tp
_ == StackOffConstraint r tp
_ = Bool
False

-- | @boundsLocRep cns loc@ returns the representative location for
-- @loc@.
--
-- This representative location has the property that a location must
-- have the same value as its representative location, and if two
-- locations have provably equal values in @cns@, then they must
-- have the same representative.
blockStartLocRepAndCns :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch))
                       => BlockStartStackConstraints arch
                       -> BoundLoc (ArchReg arch) tp
                       -> ( BoundLoc (ArchReg arch) tp
                          , Maybe (StackOffConstraint (ArchReg arch) tp)
                          )
blockStartLocRepAndCns :: forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
blockStartLocRepAndCns BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) tp
l =
  case BoundLoc (ArchReg arch) tp
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> Maybe (StackEqConstraint (ArchReg arch) 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
l (BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
forall arch.
BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
unBSSC BlockStartStackConstraints arch
cns) of
    Just (EqualLoc BoundLoc (ArchReg arch) tp
loc) -> BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
blockStartLocRepAndCns BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) tp
loc
    Just (IsStackOff MemInt (ArchAddrWidth arch)
o) -> (BoundLoc (ArchReg arch) tp
l, StackOffConstraint (ArchReg arch) ('BVType (ArchAddrWidth arch))
-> Maybe
     (StackOffConstraint (ArchReg arch) ('BVType (ArchAddrWidth arch)))
forall a. a -> Maybe a
Just (MemInt (ArchAddrWidth arch)
-> StackOffConstraint (ArchReg arch) ('BVType (ArchAddrWidth arch))
forall (r :: Type -> Type).
MemInt (RegAddrWidth r)
-> StackOffConstraint r (BVType (RegAddrWidth r))
StackOffCns MemInt (ArchAddrWidth arch)
o))
    Just (IsUExt BoundLoc (ArchReg arch) (BVType u)
loc NatRepr w
w) -> (BoundLoc (ArchReg arch) tp
l, StackOffConstraint (ArchReg arch) ('BVType w)
-> Maybe (StackOffConstraint (ArchReg arch) ('BVType w))
forall a. a -> Maybe a
Just (BoundLoc (ArchReg arch) (BVType u)
-> NatRepr w -> StackOffConstraint (ArchReg arch) ('BVType w)
forall (u :: Natural) (w :: Natural) (r :: Type -> Type).
(1 <= u, (u + 1) <= w) =>
BoundLoc r (BVType u)
-> NatRepr w -> StackOffConstraint r (BVType w)
UExtCns BoundLoc (ArchReg arch) (BVType u)
loc NatRepr w
w))
    Maybe (StackEqConstraint (ArchReg arch) tp)
Nothing -> (BoundLoc (ArchReg arch) tp
l, Maybe (StackOffConstraint (ArchReg arch) tp)
forall a. Maybe a
Nothing)

------------------------------------------------------------------------
-- joinStackExpr

-- | Maps representatives from old and new join constraints to
-- representative in merged map.
type JoinClassMap r = MapF (JoinClassPair (BoundLoc r)) (BoundLoc r)

-- | Information needed to join classes.
data JoinContext s arch = JoinContext { forall s arch.
JoinContext s arch -> BlockStartStackConstraints arch
jctxOldCns :: !(BlockStartStackConstraints arch)
                                        -- ^ Old constraints being joined
                                      , forall s arch.
JoinContext s arch -> BlockStartStackConstraints arch
jctxNewCns :: !(BlockStartStackConstraints arch)
                                        -- ^ New constraints being joined.
                                      , forall s arch.
JoinContext s arch -> STRef s (BlockStartStackConstraints arch)
jctxNextCnsRef :: !(STRef s (BlockStartStackConstraints arch))
                                        -- ^ Reference maintaining current bounds.
                                      , forall s arch.
JoinContext s arch -> STRef s (JoinClassMap (ArchReg arch))
jctxClassMapRef :: !(STRef s (JoinClassMap (ArchReg arch)))
                                        -- ^ The map from (oldClassRep, newClassRep) pairs to the
                                        -- next class map.
                                      , forall s arch. JoinContext s arch -> STRef s Int
jctxClassCountRef :: !(STRef s Int)
                                        -- ^ Reference that stores numbers of classes seen in
                                        -- old reference so we can see if new number of classes
                                        -- is different.
                                      }

-- | @setNextConstraint ctx loc cns@ asserts that @loc@ satisfies the
-- constraint @cns@ in the next constraint ref of @ctx@.
setNextConstraint :: OrdF (ArchReg arch)
                  => JoinContext s arch
                  -> BoundLoc (ArchReg arch) tp
                  -> StackEqConstraint (ArchReg arch) tp
                  -> Changed s ()
setNextConstraint :: forall arch s (tp :: Type).
OrdF (ArchReg arch) =>
JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
setNextConstraint JoinContext s arch
ctx BoundLoc (ArchReg arch) tp
thisLoc StackEqConstraint (ArchReg arch) tp
eqCns =
  ST s () -> Changed s ()
forall s a. ST s a -> Changed s a
changedST (ST s () -> Changed s ()) -> ST s () -> Changed s ()
forall a b. (a -> b) -> a -> b
$  STRef s (BlockStartStackConstraints arch)
-> (BlockStartStackConstraints arch
    -> BlockStartStackConstraints arch)
-> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' (JoinContext s arch -> STRef s (BlockStartStackConstraints arch)
forall s arch.
JoinContext s arch -> STRef s (BlockStartStackConstraints arch)
jctxNextCnsRef JoinContext s arch
ctx) ((BlockStartStackConstraints arch
  -> BlockStartStackConstraints arch)
 -> ST s ())
-> (BlockStartStackConstraints arch
    -> BlockStartStackConstraints arch)
-> ST s ()
forall a b. (a -> b) -> a -> b
$ \BlockStartStackConstraints arch
cns ->
    LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> BlockStartStackConstraints arch
forall arch.
LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> BlockStartStackConstraints arch
BSSC (BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
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
thisLoc StackEqConstraint (ArchReg arch) tp
eqCns (BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
forall arch.
BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
unBSSC BlockStartStackConstraints arch
cns))

type LocConPair r tp = (BoundLoc r tp, Maybe (StackOffConstraint r tp))

-- | @locAreEqual cns x y@ return true if @cns |= x = y@.
locAreEqual :: ( MemWidth (ArchAddrWidth arch)
               , OrdF (ArchReg arch)
               )
            => BlockStartStackConstraints arch
            -> BoundLoc (ArchReg arch) tp
            -> BoundLoc (ArchReg arch) tp
            -> Bool
locAreEqual :: forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> BoundLoc (ArchReg arch) tp -> Bool
locAreEqual BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) tp
x BoundLoc (ArchReg arch) tp
y =
  let (BoundLoc (ArchReg arch) tp
xr, Maybe (StackOffConstraint (ArchReg arch) tp)
_) = BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
blockStartLocRepAndCns BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) tp
x
      (BoundLoc (ArchReg arch) tp
yr, Maybe (StackOffConstraint (ArchReg arch) tp)
_) = BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
blockStartLocRepAndCns BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) tp
y
   in BoundLoc (ArchReg arch) tp
xr BoundLoc (ArchReg arch) tp -> BoundLoc (ArchReg arch) tp -> Bool
forall a. Eq a => a -> a -> Bool
== BoundLoc (ArchReg arch) tp
yr

joinNextLoc :: forall s arch tp
           .  ( MemWidth (ArchAddrWidth arch)
              , OrdF (ArchReg arch)
              , HasRepr (ArchReg arch) TypeRepr
              )
           => JoinContext s arch
           -> BoundLoc (ArchReg arch) tp
              -- ^ Location to use for next representative if we need
              -- need to make old.
           -> LocConPair (ArchReg arch) tp
           -> Changed s (BoundLoc (ArchReg arch) tp)
joinNextLoc :: forall s arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 HasRepr (ArchReg arch) TypeRepr) =>
JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> LocConPair (ArchReg arch) tp
-> Changed s (BoundLoc (ArchReg arch) tp)
joinNextLoc JoinContext s arch
ctx BoundLoc (ArchReg arch) tp
thisLoc (BoundLoc (ArchReg arch) tp
oldRep, Maybe (StackOffConstraint (ArchReg arch) tp)
oldPred) = do
  -- Get representative in new lcoaton.
  let (BoundLoc (ArchReg arch) tp
newRep, Maybe (StackOffConstraint (ArchReg arch) tp)
newPred) = BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
blockStartLocRepAndCns (JoinContext s arch -> BlockStartStackConstraints arch
forall s arch.
JoinContext s arch -> BlockStartStackConstraints arch
jctxNewCns JoinContext s arch
ctx) BoundLoc (ArchReg arch) tp
thisLoc
  MapF
  (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
m <- ST
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
-> Changed
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall s a. ST s a -> Changed s a
changedST (ST
   s
   (MapF
      (JoinClassPair (BoundLoc (ArchReg arch)))
      (BoundLoc (ArchReg arch)))
 -> Changed
      s
      (MapF
         (JoinClassPair (BoundLoc (ArchReg arch)))
         (BoundLoc (ArchReg arch))))
-> ST
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
-> Changed
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall a b. (a -> b) -> a -> b
$ STRef
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
-> ST
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall s a. STRef s a -> ST s a
readSTRef (JoinContext s arch
-> STRef
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall s arch.
JoinContext s arch -> STRef s (JoinClassMap (ArchReg arch))
jctxClassMapRef JoinContext s arch
ctx)
  -- Make pair containing old and new rep so we can lookup if we
  -- already have visited this class.
  let pair :: JoinClassPair (BoundLoc (ArchReg arch)) tp
pair = BoundLoc (ArchReg arch) tp
-> BoundLoc (ArchReg arch) tp
-> JoinClassPair (BoundLoc (ArchReg arch)) tp
forall k (key :: k -> Type) (tp :: k).
key tp -> key tp -> JoinClassPair key tp
JoinClassPair BoundLoc (ArchReg arch) tp
oldRep BoundLoc (ArchReg arch) tp
newRep
  case JoinClassPair (BoundLoc (ArchReg arch)) tp
-> MapF
     (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
-> Maybe (BoundLoc (ArchReg arch) tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup JoinClassPair (BoundLoc (ArchReg arch)) tp
pair MapF
  (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
m of
    -- If we have visited then we just assert @thisLoc@ is equal to
    -- the previously added rep.
    Just BoundLoc (ArchReg arch) tp
resRep -> do
      -- Assert r is equal to resRep
      JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
forall arch s (tp :: Type).
OrdF (ArchReg arch) =>
JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
setNextConstraint JoinContext s arch
ctx BoundLoc (ArchReg arch) tp
thisLoc (BoundLoc (ArchReg arch) tp -> StackEqConstraint (ArchReg arch) tp
forall (r :: Type -> Type) (tp :: Type).
BoundLoc r tp -> StackEqConstraint r tp
EqualLoc BoundLoc (ArchReg arch) tp
resRep)
      BoundLoc (ArchReg arch) tp
-> Changed s (BoundLoc (ArchReg arch) tp)
forall a. a -> Changed s a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BoundLoc (ArchReg arch) tp
resRep
    -- If we have not visited these reps, then we need to join the
    -- constraint
    Maybe (BoundLoc (ArchReg arch) tp)
Nothing -> do
      ST s () -> Changed s ()
forall s a. ST s a -> Changed s a
changedST (ST s () -> Changed s ()) -> ST s () -> Changed s ()
forall a b. (a -> b) -> a -> b
$ STRef
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
-> MapF
     (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
-> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef (JoinContext s arch
-> STRef
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall s arch.
JoinContext s arch -> STRef s (JoinClassMap (ArchReg arch))
jctxClassMapRef JoinContext s arch
ctx) (MapF
   (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
 -> ST s ())
-> MapF
     (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
-> ST s ()
forall a b. (a -> b) -> a -> b
$! JoinClassPair (BoundLoc (ArchReg arch)) tp
-> BoundLoc (ArchReg arch) tp
-> MapF
     (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
-> MapF
     (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert JoinClassPair (BoundLoc (ArchReg arch)) tp
pair BoundLoc (ArchReg arch) tp
thisLoc MapF
  (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
m
      case (Maybe (StackOffConstraint (ArchReg arch) tp)
oldPred, Maybe (StackOffConstraint (ArchReg arch) tp)
newPred) of
        (Maybe (StackOffConstraint (ArchReg arch) tp)
Nothing, Maybe (StackOffConstraint (ArchReg arch) tp)
_) ->
          () -> Changed s ()
forall a. a -> Changed s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
        (Just (StackOffCns MemInt (ArchAddrWidth arch)
x), Just (StackOffCns MemInt (ArchAddrWidth arch)
y))
          | MemInt (ArchAddrWidth arch)
x MemInt (ArchAddrWidth arch) -> MemInt (ArchAddrWidth arch) -> Bool
forall a. Eq a => a -> a -> Bool
== MemInt (ArchAddrWidth arch)
y -> do
            JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
forall arch s (tp :: Type).
OrdF (ArchReg arch) =>
JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
setNextConstraint JoinContext s arch
ctx BoundLoc (ArchReg arch) tp
thisLoc (MemInt (ArchAddrWidth arch)
-> StackEqConstraint (ArchReg arch) ('BVType (ArchAddrWidth arch))
forall (r :: Type -> Type).
MemInt (RegAddrWidth r)
-> StackEqConstraint r (BVType (RegAddrWidth r))
IsStackOff MemInt (ArchAddrWidth arch)
x)
          -- In old, thisLoc == uext xl w
          -- In new, thisLoc == uext yl w
          -- We see if xl and yl have same rep in old loc.
          -- If so, then we
        (Just (UExtCns BoundLoc (ArchReg arch) (BVType u)
xl NatRepr w
w), Just (UExtCns BoundLoc (ArchReg arch) (BVType u)
yl NatRepr w
_))
          | Just u :~: u
Refl <- NatRepr u -> NatRepr u -> Maybe (u :~: u)
forall (a :: Natural) (b :: Natural).
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 (BoundLoc (ArchReg arch) (BVType u) -> NatRepr u
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth BoundLoc (ArchReg arch) (BVType u)
xl) (BoundLoc (ArchReg arch) (BVType u) -> NatRepr u
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth BoundLoc (ArchReg arch) (BVType u)
yl)
          , BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) (BVType u)
-> BoundLoc (ArchReg arch) (BVType u)
-> Bool
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> BoundLoc (ArchReg arch) tp -> Bool
locAreEqual (JoinContext s arch -> BlockStartStackConstraints arch
forall s arch.
JoinContext s arch -> BlockStartStackConstraints arch
jctxOldCns JoinContext s arch
ctx) BoundLoc (ArchReg arch) (BVType u)
xl BoundLoc (ArchReg arch) (BVType u)
BoundLoc (ArchReg arch) (BVType u)
yl
          , BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) (BVType u)
-> BoundLoc (ArchReg arch) (BVType u)
-> Bool
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> BoundLoc (ArchReg arch) tp -> Bool
locAreEqual (JoinContext s arch -> BlockStartStackConstraints arch
forall s arch.
JoinContext s arch -> BlockStartStackConstraints arch
jctxNewCns JoinContext s arch
ctx) BoundLoc (ArchReg arch) (BVType u)
xl BoundLoc (ArchReg arch) (BVType u)
BoundLoc (ArchReg arch) (BVType u)
yl -> do
            let xlRep :: (BoundLoc (ArchReg arch) (BVType u),
 Maybe (StackOffConstraint (ArchReg arch) (BVType u)))
xlRep = BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) (BVType u)
-> (BoundLoc (ArchReg arch) (BVType u),
    Maybe (StackOffConstraint (ArchReg arch) (BVType u)))
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
blockStartLocRepAndCns (JoinContext s arch -> BlockStartStackConstraints arch
forall s arch.
JoinContext s arch -> BlockStartStackConstraints arch
jctxOldCns JoinContext s arch
ctx) BoundLoc (ArchReg arch) (BVType u)
xl
            BoundLoc (ArchReg arch) (BVType u)
nextSubRep <- JoinContext s arch
-> BoundLoc (ArchReg arch) (BVType u)
-> (BoundLoc (ArchReg arch) (BVType u),
    Maybe (StackOffConstraint (ArchReg arch) (BVType u)))
-> Changed s (BoundLoc (ArchReg arch) (BVType u))
forall s arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 HasRepr (ArchReg arch) TypeRepr) =>
JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> LocConPair (ArchReg arch) tp
-> Changed s (BoundLoc (ArchReg arch) tp)
joinNextLoc JoinContext s arch
ctx BoundLoc (ArchReg arch) (BVType u)
xl (BoundLoc (ArchReg arch) (BVType u),
 Maybe (StackOffConstraint (ArchReg arch) (BVType u)))
xlRep
            JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
forall arch s (tp :: Type).
OrdF (ArchReg arch) =>
JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
setNextConstraint JoinContext s arch
ctx BoundLoc (ArchReg arch) tp
thisLoc (BoundLoc (ArchReg arch) (BVType u)
-> NatRepr w -> StackEqConstraint (ArchReg arch) ('BVType w)
forall (u :: Natural) (w :: Natural) (r :: Type -> Type).
(1 <= u, (u + 1) <= w) =>
BoundLoc r (BVType u)
-> NatRepr w -> StackEqConstraint r (BVType w)
IsUExt BoundLoc (ArchReg arch) (BVType u)
nextSubRep NatRepr w
w)
        (Just StackOffConstraint (ArchReg arch) tp
_, Maybe (StackOffConstraint (ArchReg arch) tp)
_) -> do
          Bool -> Changed s ()
forall s. Bool -> Changed s ()
markChanged Bool
True
      BoundLoc (ArchReg arch) tp
-> Changed s (BoundLoc (ArchReg arch) tp)
forall a. a -> Changed s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BoundLoc (ArchReg arch) tp
thisLoc

-- | @joinOldLoc ctx l eq@ visits a location in a old map and ensures
-- it is bound.
joinOldLoc :: forall s arch tp
           .  ( MemWidth (ArchAddrWidth arch)
              , OrdF (ArchReg arch)
              , HasRepr (ArchReg arch) TypeRepr
              )
           => JoinContext s arch
           -> BoundLoc (ArchReg arch) tp
              -- ^ Location that appears in old constraints.
           -> StackEqConstraint (ArchReg arch) tp
              -- ^ Constraint on location in original list.
           -> Changed s ()
joinOldLoc :: forall s arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 HasRepr (ArchReg arch) TypeRepr) =>
JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
joinOldLoc JoinContext s arch
ctx BoundLoc (ArchReg arch) tp
thisLoc StackEqConstraint (ArchReg arch) tp
oldCns = do
  (BoundLoc (ArchReg arch) tp,
 Maybe (StackOffConstraint (ArchReg arch) tp))
oldRepPredPair <- ST
  s
  (BoundLoc (ArchReg arch) tp,
   Maybe (StackOffConstraint (ArchReg arch) tp))
-> Changed
     s
     (BoundLoc (ArchReg arch) tp,
      Maybe (StackOffConstraint (ArchReg arch) tp))
forall s a. ST s a -> Changed s a
changedST (ST
   s
   (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
 -> Changed
      s
      (BoundLoc (ArchReg arch) tp,
       Maybe (StackOffConstraint (ArchReg arch) tp)))
-> ST
     s
     (BoundLoc (ArchReg arch) tp,
      Maybe (StackOffConstraint (ArchReg arch) tp))
-> Changed
     s
     (BoundLoc (ArchReg arch) tp,
      Maybe (StackOffConstraint (ArchReg arch) tp))
forall a b. (a -> b) -> a -> b
$
    case StackEqConstraint (ArchReg arch) tp
oldCns of
      EqualLoc BoundLoc (ArchReg arch) tp
oldLoc ->
        (BoundLoc (ArchReg arch) tp,
 Maybe (StackOffConstraint (ArchReg arch) tp))
-> ST
     s
     (BoundLoc (ArchReg arch) tp,
      Maybe (StackOffConstraint (ArchReg arch) tp))
forall a. a -> ST s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
blockStartLocRepAndCns (JoinContext s arch -> BlockStartStackConstraints arch
forall s arch.
JoinContext s arch -> BlockStartStackConstraints arch
jctxOldCns JoinContext s arch
ctx) BoundLoc (ArchReg arch) tp
oldLoc)
      IsStackOff MemInt (ArchAddrWidth arch)
o -> do
        -- Increment number of equivalence classes when we see an old
        -- representative.
        STRef s Int -> (Int -> Int) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' (JoinContext s arch -> STRef s Int
forall s arch. JoinContext s arch -> STRef s Int
jctxClassCountRef JoinContext s arch
ctx) (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
        -- Return this loc
        (BoundLoc (ArchReg arch) tp,
 Maybe (StackOffConstraint (ArchReg arch) tp))
-> ST
     s
     (BoundLoc (ArchReg arch) tp,
      Maybe (StackOffConstraint (ArchReg arch) tp))
forall a. a -> ST s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BoundLoc (ArchReg arch) tp
BoundLoc (ArchReg arch) ('BVType (ArchAddrWidth arch))
thisLoc, StackOffConstraint (ArchReg arch) ('BVType (ArchAddrWidth arch))
-> Maybe
     (StackOffConstraint (ArchReg arch) ('BVType (ArchAddrWidth arch)))
forall a. a -> Maybe a
Just (MemInt (ArchAddrWidth arch)
-> StackOffConstraint (ArchReg arch) ('BVType (ArchAddrWidth arch))
forall (r :: Type -> Type).
MemInt (RegAddrWidth r)
-> StackOffConstraint r (BVType (RegAddrWidth r))
StackOffCns MemInt (ArchAddrWidth arch)
o))
      IsUExt BoundLoc (ArchReg arch) (BVType u)
oldSubLoc NatRepr w
w -> do
        -- Increment number of equivalence classes when we see an old
        -- representative.
        STRef s Int -> (Int -> Int) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef' (JoinContext s arch -> STRef s Int
forall s arch. JoinContext s arch -> STRef s Int
jctxClassCountRef JoinContext s arch
ctx) (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
        let (BoundLoc (ArchReg arch) (BVType u)
subRep, Maybe (StackOffConstraint (ArchReg arch) (BVType u))
_) = BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) (BVType u)
-> (BoundLoc (ArchReg arch) (BVType u),
    Maybe (StackOffConstraint (ArchReg arch) (BVType u)))
forall arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
blockStartLocRepAndCns (JoinContext s arch -> BlockStartStackConstraints arch
forall s arch.
JoinContext s arch -> BlockStartStackConstraints arch
jctxOldCns JoinContext s arch
ctx) BoundLoc (ArchReg arch) (BVType u)
oldSubLoc
        (BoundLoc (ArchReg arch) tp,
 Maybe (StackOffConstraint (ArchReg arch) tp))
-> ST
     s
     (BoundLoc (ArchReg arch) tp,
      Maybe (StackOffConstraint (ArchReg arch) tp))
forall a. a -> ST s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BoundLoc (ArchReg arch) tp
BoundLoc (ArchReg arch) ('BVType w)
thisLoc, StackOffConstraint (ArchReg arch) ('BVType w)
-> Maybe (StackOffConstraint (ArchReg arch) ('BVType w))
forall a. a -> Maybe a
Just (BoundLoc (ArchReg arch) (BVType u)
-> NatRepr w -> StackOffConstraint (ArchReg arch) ('BVType w)
forall (u :: Natural) (w :: Natural) (r :: Type -> Type).
(1 <= u, (u + 1) <= w) =>
BoundLoc r (BVType u)
-> NatRepr w -> StackOffConstraint r (BVType w)
UExtCns BoundLoc (ArchReg arch) (BVType u)
subRep NatRepr w
w))
  BoundLoc (ArchReg arch) tp
_ <- JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> (BoundLoc (ArchReg arch) tp,
    Maybe (StackOffConstraint (ArchReg arch) tp))
-> Changed s (BoundLoc (ArchReg arch) tp)
forall s arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 HasRepr (ArchReg arch) TypeRepr) =>
JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> LocConPair (ArchReg arch) tp
-> Changed s (BoundLoc (ArchReg arch) tp)
joinNextLoc JoinContext s arch
ctx BoundLoc (ArchReg arch) tp
thisLoc (BoundLoc (ArchReg arch) tp,
 Maybe (StackOffConstraint (ArchReg arch) tp))
oldRepPredPair
  () -> Changed s ()
forall a. a -> Changed s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()

-- | Return a jump bounds that implies both input bounds, or `Nothing`
-- if every fact inx the old bounds is implied by the new bounds.
joinBlockStartStackConstraints
  :: forall arch s
  .  (MemWidth (ArchAddrWidth arch)
     , OrdF (ArchReg arch)
     , HasRepr (ArchReg arch) TypeRepr
     )
  => BlockStartStackConstraints arch
  -> BlockStartStackConstraints arch
  -> Changed s (BlockStartStackConstraints arch, JoinClassMap (ArchReg arch))
joinBlockStartStackConstraints :: 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 BlockStartStackConstraints arch
old BlockStartStackConstraints arch
new = do
  -- Reference to new bounds.
  STRef s (BlockStartStackConstraints arch)
cnsRef <- ST s (STRef s (BlockStartStackConstraints arch))
-> Changed s (STRef s (BlockStartStackConstraints arch))
forall s a. ST s a -> Changed s a
changedST (ST s (STRef s (BlockStartStackConstraints arch))
 -> Changed s (STRef s (BlockStartStackConstraints arch)))
-> ST s (STRef s (BlockStartStackConstraints arch))
-> Changed s (STRef s (BlockStartStackConstraints arch))
forall a b. (a -> b) -> a -> b
$ BlockStartStackConstraints arch
-> ST s (STRef s (BlockStartStackConstraints arch))
forall a s. a -> ST s (STRef s a)
newSTRef (LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> BlockStartStackConstraints arch
forall arch.
LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> BlockStartStackConstraints arch
BSSC LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
forall (r :: Type -> Type) (v :: Type -> Type). LocMap r v
locMapEmpty)
  -- This maps pairs containing the class representative in the old
  -- and new maps to the associated class representative in the
  -- combined bounds.
  STRef
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
procRef <- ST
  s
  (STRef
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch))))
-> Changed
     s
     (STRef
        s
        (MapF
           (JoinClassPair (BoundLoc (ArchReg arch)))
           (BoundLoc (ArchReg arch))))
forall s a. ST s a -> Changed s a
changedST (ST
   s
   (STRef
      s
      (MapF
         (JoinClassPair (BoundLoc (ArchReg arch)))
         (BoundLoc (ArchReg arch))))
 -> Changed
      s
      (STRef
         s
         (MapF
            (JoinClassPair (BoundLoc (ArchReg arch)))
            (BoundLoc (ArchReg arch)))))
-> ST
     s
     (STRef
        s
        (MapF
           (JoinClassPair (BoundLoc (ArchReg arch)))
           (BoundLoc (ArchReg arch))))
-> Changed
     s
     (STRef
        s
        (MapF
           (JoinClassPair (BoundLoc (ArchReg arch)))
           (BoundLoc (ArchReg arch))))
forall a b. (a -> b) -> a -> b
$ MapF
  (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
-> ST
     s
     (STRef
        s
        (MapF
           (JoinClassPair (BoundLoc (ArchReg arch)))
           (BoundLoc (ArchReg arch))))
forall a s. a -> ST s (STRef s a)
newSTRef MapF
  (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
  STRef s Int
cntr    <- ST s (STRef s Int) -> Changed s (STRef s Int)
forall s a. ST s a -> Changed s a
changedST (ST s (STRef s Int) -> Changed s (STRef s Int))
-> ST s (STRef s Int) -> Changed s (STRef s Int)
forall a b. (a -> b) -> a -> b
$ Int -> ST s (STRef s Int)
forall a s. a -> ST s (STRef s a)
newSTRef Int
0
  let ctx :: JoinContext s arch
ctx = JoinContext { jctxOldCns :: BlockStartStackConstraints arch
jctxOldCns = BlockStartStackConstraints arch
old
                        , jctxNewCns :: BlockStartStackConstraints arch
jctxNewCns = BlockStartStackConstraints arch
new
                        , jctxNextCnsRef :: STRef s (BlockStartStackConstraints arch)
jctxNextCnsRef = STRef s (BlockStartStackConstraints arch)
cnsRef
                        , jctxClassMapRef :: STRef
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
jctxClassMapRef = STRef
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
procRef
                        , jctxClassCountRef :: STRef s Int
jctxClassCountRef = STRef s Int
cntr
                        }
  (forall (tp :: Type).
 BoundLoc (ArchReg arch) tp
 -> StackEqConstraint (ArchReg arch) tp -> Changed s ())
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> Changed s ()
forall (m :: Type -> Type) (r :: Type -> Type) (p :: Type -> Type).
Applicative m =>
(forall (tp :: Type). BoundLoc r tp -> p tp -> m ())
-> LocMap r p -> m ()
locMapTraverseWithKey_ (JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
forall s arch (tp :: Type).
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch),
 HasRepr (ArchReg arch) TypeRepr) =>
JoinContext s arch
-> BoundLoc (ArchReg arch) tp
-> StackEqConstraint (ArchReg arch) tp
-> Changed s ()
joinOldLoc JoinContext s arch
ctx) (BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
forall arch.
BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
unBSSC BlockStartStackConstraints arch
old)
  -- Check number of equivalence classes in result and original
  -- The count should not have decreased, but may increase if two elements
  -- are no longer equal, and we need to check this.
  Int
origClassCount   <- ST s Int -> Changed s Int
forall s a. ST s a -> Changed s a
changedST (ST s Int -> Changed s Int) -> ST s Int -> Changed s Int
forall a b. (a -> b) -> a -> b
$ STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
cntr
  Int
resultClassCount <- ST s Int -> Changed s Int
forall s a. ST s a -> Changed s a
changedST (ST s Int -> Changed s Int) -> ST s Int -> Changed s Int
forall a b. (a -> b) -> a -> b
$ MapF
  (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
-> Int
forall t e. IsBinTree t e => t -> Int
MapF.size (MapF
   (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
 -> Int)
-> ST
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
-> ST s Int
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
-> ST
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall s a. STRef s a -> ST s a
readSTRef STRef
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
procRef
  Bool -> Changed s () -> Changed s ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless (Int
origClassCount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
resultClassCount) (Changed s () -> Changed s ()) -> Changed s () -> Changed s ()
forall a b. (a -> b) -> a -> b
$ do
    String -> Changed s ()
forall a. HasCallStack => String -> a
error String
"Original class count should be bound by resultClassCount"
  -- Record changed if any classes are different.
  Bool -> Changed s ()
forall s. Bool -> Changed s ()
markChanged (Int
origClassCount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
resultClassCount)
  ST
  s
  (BlockStartStackConstraints arch,
   MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
-> Changed
     s
     (BlockStartStackConstraints arch,
      MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall s a. ST s a -> Changed s a
changedST (ST
   s
   (BlockStartStackConstraints arch,
    MapF
      (JoinClassPair (BoundLoc (ArchReg arch)))
      (BoundLoc (ArchReg arch)))
 -> Changed
      s
      (BlockStartStackConstraints arch,
       MapF
         (JoinClassPair (BoundLoc (ArchReg arch)))
         (BoundLoc (ArchReg arch))))
-> ST
     s
     (BlockStartStackConstraints arch,
      MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
-> Changed
     s
     (BlockStartStackConstraints arch,
      MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall a b. (a -> b) -> a -> b
$ (,) (BlockStartStackConstraints arch
 -> MapF
      (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
 -> (BlockStartStackConstraints arch,
     MapF
       (JoinClassPair (BoundLoc (ArchReg arch)))
       (BoundLoc (ArchReg arch))))
-> ST s (BlockStartStackConstraints arch)
-> ST
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
      -> (BlockStartStackConstraints arch,
          MapF
            (JoinClassPair (BoundLoc (ArchReg arch)))
            (BoundLoc (ArchReg arch))))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef s (BlockStartStackConstraints arch)
-> ST s (BlockStartStackConstraints arch)
forall s a. STRef s a -> ST s a
readSTRef STRef s (BlockStartStackConstraints arch)
cnsRef ST
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch))) (BoundLoc (ArchReg arch))
   -> (BlockStartStackConstraints arch,
       MapF
         (JoinClassPair (BoundLoc (ArchReg arch)))
         (BoundLoc (ArchReg arch))))
-> ST
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
-> ST
     s
     (BlockStartStackConstraints arch,
      MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall a b. ST s (a -> b) -> ST s a -> ST s b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> STRef
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
-> ST
     s
     (MapF
        (JoinClassPair (BoundLoc (ArchReg arch)))
        (BoundLoc (ArchReg arch)))
forall s a. STRef s a -> ST s a
readSTRef STRef
  s
  (MapF
     (JoinClassPair (BoundLoc (ArchReg arch)))
     (BoundLoc (ArchReg arch)))
procRef

------------------------------------------------------------------------
-- StackExpr

-- | This is an expression that represents the value of stack
-- locations and assignments during steping through the block.
--
-- The main diference between this and
-- the `Value` type, index expressions do not depend on values read
-- and written to memory during execution of the block, and are purely
-- functions of the input
--
-- This is different from `ClassPred` in that @ClassPred@ is a property
-- assigned to equivalence classes
data StackExpr arch ids tp where
  -- | This refers to the value that a location had at the start of
  -- block execution.
  --
  -- The location should be a class representative in the initial bounds.
  ClassRepExpr :: !(BoundLoc (ArchReg arch) tp) -> StackExpr arch ids tp
  -- | An assignment that is not interpreted, and just treated as a constant.
  UninterpAssignExpr :: !(AssignId ids tp)
                     -> !(AssignRhs arch (Value arch ids) tp)
                     -> StackExpr arch ids tp
  -- | Denotes the value of the stack pointer at function start plus some constant.
  StackOffsetExpr :: !(MemInt (ArchAddrWidth arch))
                  -> StackExpr arch ids (BVType (ArchAddrWidth arch))
  -- | Denotes a constant
  CExpr :: !(CValue arch tp) -> StackExpr arch ids tp

  -- | This is a pure function applied to other index expressions that
  -- may be worth interpreting (but could be treated as an uninterp
  -- assign expr also.
  UExtExpr :: (1 <= u, u+1 <= w)
           => StackExpr arch ids (BVType u)
           -> NatRepr w
           -> StackExpr arch ids (BVType w)

  -- | This is a pure function applied to other index expressions that
  -- may be worth interpreting (but could be treated as an uninterp
  -- assign expr also.
  AppExpr :: !(AssignId ids tp)
          -> !(App (StackExpr arch ids) tp)
          -> StackExpr arch ids tp

instance ShowF (ArchReg arch) => Show (StackExpr arch ids tp) where
  show :: StackExpr arch ids tp -> String
show (ClassRepExpr BoundLoc (ArchReg arch) tp
l) = String
"(ClassRepExpr " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> BoundLoc (ArchReg arch) tp -> String
forall a. Show a => a -> String
show BoundLoc (ArchReg arch) tp
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (UninterpAssignExpr AssignId ids tp
a AssignRhs arch (Value arch ids) tp
_r) = String
"(UninterpAssignExpr " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> AssignId ids tp -> String
forall a. Show a => a -> String
show AssignId ids tp
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" _)"
  show (StackOffsetExpr MemInt (ArchAddrWidth arch)
o) = String
"(StackOffsetExpr " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> MemInt (ArchAddrWidth arch) -> String
forall a. Show a => a -> String
show MemInt (ArchAddrWidth arch)
o String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (CExpr CValue arch tp
c) = String
"(CExpr " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> CValue arch tp -> String
forall a. Show a => a -> String
show CValue arch tp
c String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (UExtExpr StackExpr arch ids (BVType u)
u NatRepr w
w) = String
"(UExtExpr " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> StackExpr arch ids (BVType u) -> String
forall a. Show a => a -> String
show StackExpr arch ids (BVType u)
u String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> NatRepr w -> String
forall a. Show a => a -> String
show NatRepr w
w String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  show (AppExpr AssignId ids tp
a App (StackExpr arch ids) tp
_r) = String
"(AppExpr " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> AssignId ids tp -> String
forall a. Show a => a -> String
show AssignId ids tp
a String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" _)"

instance TestEquality (ArchReg arch) => TestEquality (StackExpr arch ids) where
  testEquality :: forall (a :: Type) (b :: Type).
StackExpr arch ids a -> StackExpr arch ids b -> Maybe (a :~: b)
testEquality (ClassRepExpr BoundLoc (ArchReg arch) a
x) (ClassRepExpr BoundLoc (ArchReg arch) b
y) =
    BoundLoc (ArchReg arch) a
-> BoundLoc (ArchReg arch) b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
BoundLoc (ArchReg arch) a
-> BoundLoc (ArchReg arch) b -> Maybe (a :~: b)
testEquality BoundLoc (ArchReg arch) a
x BoundLoc (ArchReg arch) b
y
  testEquality (UninterpAssignExpr AssignId ids a
x AssignRhs arch (Value arch ids) a
_) (UninterpAssignExpr AssignId ids b
y AssignRhs arch (Value arch ids) b
_) =
    AssignId ids a -> AssignId ids b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
AssignId ids a -> AssignId ids b -> Maybe (a :~: b)
testEquality AssignId ids a
x AssignId ids b
y
  testEquality (StackOffsetExpr MemInt (ArchAddrWidth arch)
x) (StackOffsetExpr MemInt (ArchAddrWidth arch)
y) =
    if MemInt (ArchAddrWidth arch)
x MemInt (ArchAddrWidth arch) -> MemInt (ArchAddrWidth arch) -> Bool
forall a. Eq a => a -> a -> Bool
== MemInt (ArchAddrWidth arch)
y then
      (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
     else
      Maybe (a :~: b)
forall a. Maybe a
Nothing
  testEquality (CExpr CValue arch a
x) (CExpr CValue arch b
y) =
    CValue arch a -> CValue arch b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
CValue arch a -> CValue arch b -> Maybe (a :~: b)
testEquality CValue arch a
x CValue arch b
y
  testEquality (UExtExpr StackExpr arch ids (BVType u)
x NatRepr w
xw) (UExtExpr StackExpr arch ids (BVType u)
y NatRepr w
yw) = do
    w :~: w
Refl <- NatRepr w -> NatRepr w -> Maybe (w :~: w)
forall (a :: Natural) (b :: Natural).
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 NatRepr w
xw NatRepr w
yw
    BVType u :~: BVType u
Refl <- StackExpr arch ids (BVType u)
-> StackExpr arch ids (BVType u) -> Maybe (BVType u :~: BVType u)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
StackExpr arch ids a -> StackExpr arch ids b -> Maybe (a :~: b)
testEquality StackExpr arch ids (BVType u)
x StackExpr arch ids (BVType u)
y
    (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality (AppExpr AssignId ids a
xn App (StackExpr arch ids) a
_xa) (AppExpr AssignId ids b
yn App (StackExpr arch ids) b
_ya) =
    AssignId ids a -> AssignId ids b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
AssignId ids a -> AssignId ids b -> Maybe (a :~: b)
testEquality AssignId ids a
xn AssignId ids b
yn
  testEquality StackExpr arch ids a
_ StackExpr arch ids b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF (ArchReg arch) => OrdF (StackExpr arch ids) where
  compareF :: forall (x :: Type) (y :: Type).
StackExpr arch ids x -> StackExpr arch ids y -> OrderingF x y
compareF (ClassRepExpr BoundLoc (ArchReg arch) x
x) (ClassRepExpr BoundLoc (ArchReg arch) y
y) = BoundLoc (ArchReg arch) x
-> BoundLoc (ArchReg arch) y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
BoundLoc (ArchReg arch) x
-> BoundLoc (ArchReg arch) y -> OrderingF x y
compareF BoundLoc (ArchReg arch) x
x BoundLoc (ArchReg arch) y
y
  compareF ClassRepExpr{} StackExpr arch ids y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF StackExpr arch ids x
_ ClassRepExpr{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (UninterpAssignExpr AssignId ids x
x AssignRhs arch (Value arch ids) x
_) (UninterpAssignExpr AssignId ids y
y AssignRhs arch (Value arch ids) y
_) = AssignId ids x -> AssignId ids y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
AssignId ids x -> AssignId ids y -> OrderingF x y
compareF AssignId ids x
x AssignId ids y
y
  compareF UninterpAssignExpr{} StackExpr arch ids y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF StackExpr arch ids x
_ UninterpAssignExpr{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (StackOffsetExpr MemInt (ArchAddrWidth arch)
x) (StackOffsetExpr MemInt (ArchAddrWidth arch)
y) = Ordering -> OrderingF x x
forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (MemInt (ArchAddrWidth arch)
-> MemInt (ArchAddrWidth arch) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare MemInt (ArchAddrWidth arch)
x MemInt (ArchAddrWidth arch)
y)
  compareF StackOffsetExpr{} StackExpr arch ids y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF StackExpr arch ids x
_ StackOffsetExpr{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (CExpr CValue arch x
x) (CExpr CValue arch y
y) = CValue arch x -> CValue arch y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
CValue arch x -> CValue arch y -> OrderingF x y
compareF CValue arch x
x CValue arch y
y
  compareF CExpr{} StackExpr arch ids y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF StackExpr arch ids x
_ CExpr{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (UExtExpr StackExpr arch ids (BVType u)
x NatRepr w
xw) (UExtExpr StackExpr arch ids (BVType u)
y NatRepr w
yw) =
    OrderingF w w -> ((w ~ w) => OrderingF x y) -> OrderingF x y
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (NatRepr w -> NatRepr w -> OrderingF w w
forall (x :: Natural) (y :: Natural).
NatRepr x -> NatRepr y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF NatRepr w
xw NatRepr w
yw) (((w ~ w) => OrderingF x y) -> OrderingF x y)
-> ((w ~ w) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    OrderingF (BVType u) (BVType u)
-> ((BVType u ~ BVType u) => OrderingF x y) -> OrderingF x y
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (StackExpr arch ids (BVType u)
-> StackExpr arch ids (BVType u) -> OrderingF (BVType u) (BVType u)
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
StackExpr arch ids x -> StackExpr arch ids y -> OrderingF x y
compareF StackExpr arch ids (BVType u)
x StackExpr arch ids (BVType u)
y) (((BVType u ~ BVType u) => OrderingF x y) -> OrderingF x y)
-> ((BVType u ~ BVType u) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$ OrderingF x x
OrderingF x y
(BVType u ~ BVType u) => OrderingF x y
forall {k} (x :: k). OrderingF x x
EQF
  compareF UExtExpr{} StackExpr arch ids y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF StackExpr arch ids x
_ UExtExpr{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (AppExpr AssignId ids x
xn App (StackExpr arch ids) x
_xa) (AppExpr AssignId ids y
yn App (StackExpr arch ids) y
_ya) = AssignId ids x -> AssignId ids y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
AssignId ids x -> AssignId ids y -> OrderingF x y
compareF AssignId ids x
xn AssignId ids y
yn

instance TestEquality (ArchReg arch) => Eq (StackExpr arch ids tp) where
  StackExpr arch ids tp
x == :: StackExpr arch ids tp -> StackExpr arch ids tp -> Bool
== StackExpr arch ids tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (StackExpr arch ids tp -> StackExpr arch ids 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).
StackExpr arch ids a -> StackExpr arch ids b -> Maybe (a :~: b)
testEquality StackExpr arch ids tp
x StackExpr arch ids tp
y)

instance OrdF (ArchReg arch) => Ord (StackExpr arch ids tp) where
  compare :: StackExpr arch ids tp -> StackExpr arch ids tp -> Ordering
compare StackExpr arch ids tp
x StackExpr arch ids tp
y = OrderingF tp tp -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (StackExpr arch ids tp -> StackExpr arch ids tp -> OrderingF tp tp
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
StackExpr arch ids x -> StackExpr arch ids y -> OrderingF x y
compareF StackExpr arch ids tp
x StackExpr arch ids tp
y)

instance ( HasRepr (ArchReg arch) TypeRepr
         , MemWidth (ArchAddrWidth arch)
         ) => HasRepr (StackExpr arch ids) TypeRepr where
  typeRepr :: forall (tp :: Type). StackExpr arch ids tp -> TypeRepr tp
typeRepr StackExpr arch ids tp
e =
    case StackExpr arch ids tp
e of
      ClassRepExpr BoundLoc (ArchReg arch) tp
x    -> BoundLoc (ArchReg arch) tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). BoundLoc (ArchReg arch) tp -> TypeRepr tp
typeRepr BoundLoc (ArchReg arch) tp
x
      UninterpAssignExpr AssignId ids tp
_ AssignRhs arch (Value arch ids) tp
rhs   -> AssignRhs arch (Value arch ids) tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type).
AssignRhs arch (Value arch ids) tp -> TypeRepr tp
typeRepr AssignRhs arch (Value arch ids) tp
rhs
      StackOffsetExpr MemInt (ArchAddrWidth arch)
_ -> TypeRepr tp
TypeRepr ('BVType (ArchAddrWidth arch))
forall (w :: Natural). MemWidth w => TypeRepr (BVType w)
addrTypeRepr
      CExpr CValue arch tp
x           -> CValue arch tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). CValue arch tp -> TypeRepr tp
typeRepr CValue arch tp
x
      UExtExpr (StackExpr arch ids (BVType u)
_ :: StackExpr arch ids (BVType u)) (NatRepr w
w :: NatRepr w) ->
        case LeqProof 1 (u + 1) -> LeqProof (u + 1) w -> LeqProof 1 w
forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (LeqProof 1 u -> Proxy 1 -> LeqProof 1 (u + 1)
forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof @1 @u) (Proxy 1
forall {k} (t :: k). Proxy t
Proxy :: Proxy 1)) (forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof @(u+1) @w) of
          LeqProof 1 w
LeqProof -> NatRepr w -> TypeRepr ('BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr w
w
      AppExpr AssignId ids tp
_ App (StackExpr arch ids) tp
a       -> App (StackExpr arch ids) tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). App (StackExpr arch ids) tp -> TypeRepr tp
typeRepr App (StackExpr arch ids) tp
a

instance ShowF (ArchReg arch) => Pretty (StackExpr arch id tp) where
  pretty :: forall ann. StackExpr arch id tp -> Doc ann
pretty StackExpr arch id tp
e =
    case StackExpr arch id tp
e of
      ClassRepExpr BoundLoc (ArchReg arch) tp
l -> BoundLoc (ArchReg arch) tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BoundLoc (ArchReg arch) tp -> Doc ann
pretty BoundLoc (ArchReg arch) tp
l
      UninterpAssignExpr AssignId id tp
n AssignRhs arch (Value arch id) tp
_ -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"uninterp" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> AssignId id tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId id tp
n)
      StackOffsetExpr MemInt (ArchAddrWidth arch)
o
        | MemInt (ArchAddrWidth arch) -> Int64
forall (w :: Natural). MemInt w -> Int64
memIntValue MemInt (ArchAddrWidth arch)
o Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
> Int64
0 -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"+ stack_off" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> MemInt (ArchAddrWidth arch) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MemInt (ArchAddrWidth arch) -> Doc ann
pretty MemInt (ArchAddrWidth arch)
o)
        | MemInt (ArchAddrWidth arch) -> Int64
forall (w :: Natural). MemInt w -> Int64
memIntValue MemInt (ArchAddrWidth arch)
o Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
< Int64
0 -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"- stack_off" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Integer -> Integer
forall a. Num a => a -> a
negate (Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger (MemInt (ArchAddrWidth arch) -> Int64
forall (w :: Natural). MemInt w -> Int64
memIntValue MemInt (ArchAddrWidth arch)
o))))
        | Bool
otherwise -> Doc ann
"stack_off"
      CExpr CValue arch tp
v -> CValue arch tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. CValue arch tp -> Doc ann
pretty CValue arch tp
v
      UExtExpr StackExpr arch id (BVType u)
l NatRepr w
w -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"uext " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> StackExpr arch id (BVType u) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StackExpr arch id (BVType u) -> Doc ann
pretty StackExpr arch id (BVType u)
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> NatRepr w -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr w
w)
      AppExpr AssignId id tp
n App (StackExpr arch id) tp
_ -> AssignId id tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId id tp
n

instance ShowF (ArchReg arch) => PrettyF (StackExpr arch id) where
  prettyF :: forall (tp :: Type) ann. StackExpr arch id tp -> Doc ann
prettyF = StackExpr arch id tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StackExpr arch id tp -> Doc ann
pretty

-- | Return an expression equivalent to the location in the constraint
-- map.
--
-- This attempts to normalize the expression to get a representative.
blockStartLocExpr :: (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch))
                  => BlockStartStackConstraints arch
                  -> BoundLoc (ArchReg arch) tp
                  -> StackExpr arch ids tp
blockStartLocExpr :: forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
blockStartLocExpr BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) tp
loc =
  case BoundLoc (ArchReg arch) tp
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> Maybe (StackEqConstraint (ArchReg arch) 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 (BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
forall arch.
BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
unBSSC BlockStartStackConstraints arch
cns) of
    Maybe (StackEqConstraint (ArchReg arch) tp)
Nothing -> BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
forall arch (tp :: Type) ids.
BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
ClassRepExpr BoundLoc (ArchReg arch) tp
loc
    Just (IsStackOff MemInt (ArchAddrWidth arch)
o) -> MemInt (ArchAddrWidth arch)
-> StackExpr arch ids ('BVType (ArchAddrWidth arch))
forall arch ids.
MemInt (ArchAddrWidth arch)
-> StackExpr arch ids (BVType (ArchAddrWidth arch))
StackOffsetExpr MemInt (ArchAddrWidth arch)
o
    Just (EqualLoc BoundLoc (ArchReg arch) tp
loc') -> BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
blockStartLocExpr BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) tp
loc'
    Just (IsUExt BoundLoc (ArchReg arch) (BVType u)
loc' NatRepr w
w) -> StackExpr arch ids (BVType u)
-> NatRepr w -> StackExpr arch ids ('BVType w)
forall (u :: Natural) (w :: Natural) arch ids.
(1 <= u, (u + 1) <= w) =>
StackExpr arch ids (BVType u)
-> NatRepr w -> StackExpr arch ids (BVType w)
UExtExpr (BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) (BVType u)
-> StackExpr arch ids (BVType u)
forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
blockStartLocExpr BlockStartStackConstraints arch
cns BoundLoc (ArchReg arch) (BVType u)
loc') NatRepr w
w

------------------------------------------------------------------------
-- BlockIntraStackConstraints

-- | Information about bounds for a particular value within a block.
data BlockIntraStackConstraints arch ids
   = BISC { forall arch ids.
BlockIntraStackConstraints arch ids
-> BlockStartStackConstraints arch
biscInitConstraints :: !(BlockStartStackConstraints arch)
            -- ^ Bounds at execution start.
          , forall arch ids.
BlockIntraStackConstraints arch ids
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
stackExprMap :: !(MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids))
            -- ^ Maps stack offsets to the expression associated with them at the current
            -- location.
          , forall arch ids.
BlockIntraStackConstraints arch ids
-> MapF (AssignId ids) (StackExpr arch ids)
assignExprMap :: !(MapF (AssignId ids) (StackExpr arch ids))
            -- ^ Maps processed assignments to index expressions.
          }

instance ShowF (ArchReg arch) => Pretty (BlockIntraStackConstraints arch ids) where
  pretty :: forall ann. BlockIntraStackConstraints arch ids -> Doc ann
pretty BlockIntraStackConstraints arch ids
cns =
    let ppStk :: MemInt (ArchAddrWidth arch) -> MemRepr tp -> StackExpr arch ids tp -> Doc ann
        ppStk :: forall (tp :: Type) ann.
MemInt (ArchAddrWidth arch)
-> MemRepr tp -> StackExpr arch ids tp -> Doc ann
ppStk MemInt (ArchAddrWidth arch)
o MemRepr tp
r StackExpr arch ids tp
v = MemInt (ArchAddrWidth arch) -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow MemInt (ArchAddrWidth arch)
o Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
", " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> MemRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MemRepr tp -> Doc ann
pretty MemRepr tp
r Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" := " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> StackExpr arch ids tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StackExpr arch ids tp -> Doc ann
pretty StackExpr arch ids tp
v
        sm :: Doc ann
        sm :: forall ann. Doc ann
sm = (forall (tp :: Type).
 MemInt (ArchAddrWidth arch)
 -> MemRepr tp -> StackExpr arch ids tp -> Doc ann -> Doc ann)
-> Doc ann
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
-> Doc ann
forall o (v :: Type -> Type) r.
(forall (tp :: Type). o -> MemRepr tp -> v tp -> r -> r)
-> r -> MemMap o v -> r
memMapFoldrWithKey (\MemInt (ArchAddrWidth arch)
o MemRepr tp
r StackExpr arch ids tp
v Doc ann
d -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [MemInt (ArchAddrWidth arch)
-> MemRepr tp -> StackExpr arch ids tp -> Doc ann
forall (tp :: Type) ann.
MemInt (ArchAddrWidth arch)
-> MemRepr tp -> StackExpr arch ids tp -> Doc ann
ppStk MemInt (ArchAddrWidth arch)
o MemRepr tp
r StackExpr arch ids tp
v, Doc ann
d]) Doc ann
forall ann. Doc ann
emptyDoc (BlockIntraStackConstraints arch ids
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
forall arch ids.
BlockIntraStackConstraints arch ids
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
stackExprMap BlockIntraStackConstraints arch ids
cns)
        ppAssign :: AssignId ids tp -> StackExpr arch ids tp -> Doc ann -> Doc ann
        ppAssign :: forall (tp :: Type) ann.
AssignId ids tp -> StackExpr arch ids tp -> Doc ann -> Doc ann
ppAssign AssignId ids tp
a (AppExpr AssignId ids tp
u App (StackExpr arch ids) tp
app) Doc ann
d =
          case AssignId ids tp -> AssignId ids 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).
AssignId ids a -> AssignId ids b -> Maybe (a :~: b)
testEquality AssignId ids tp
a AssignId ids tp
u of
            Maybe (tp :~: tp)
Nothing -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [AssignId ids tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId ids tp
a Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" := " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> AssignId ids tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId ids tp
u, Doc ann
d]
            Just tp :~: tp
Refl -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [AssignId ids tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId ids tp
a Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" := " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> (forall (u :: Type). StackExpr arch ids u -> Doc ann)
-> App (StackExpr arch ids) tp -> Doc ann
forall (f :: Type -> Type) ann (tp :: Type).
(forall (u :: Type). f u -> Doc ann) -> App f tp -> Doc ann
ppApp StackExpr arch ids u -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StackExpr arch ids u -> Doc ann
forall (u :: Type). StackExpr arch ids u -> Doc ann
pretty App (StackExpr arch ids) tp
app, Doc ann
d]
        ppAssign AssignId ids tp
a StackExpr arch ids tp
e Doc ann
d = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [AssignId ids tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId ids tp
a Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" := " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> StackExpr arch ids tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StackExpr arch ids tp -> Doc ann
pretty StackExpr arch ids tp
e, Doc ann
d]
        am :: Doc ann
        am :: forall ann. Doc ann
am = (forall (s :: Type).
 AssignId ids s -> StackExpr arch ids s -> Doc ann -> Doc ann)
-> Doc ann -> MapF (AssignId ids) (StackExpr arch ids) -> Doc ann
forall {v} (k :: v -> Type) (a :: v -> Type) b.
(forall (s :: v). k s -> a s -> b -> b) -> b -> MapF k a -> b
MapF.foldrWithKey AssignId ids s -> StackExpr arch ids s -> Doc ann -> Doc ann
forall (s :: Type).
AssignId ids s -> StackExpr arch ids s -> Doc ann -> Doc ann
forall (tp :: Type) ann.
AssignId ids tp -> StackExpr arch ids tp -> Doc ann -> Doc ann
ppAssign Doc ann
forall ann. Doc ann
emptyDoc (BlockIntraStackConstraints arch ids
-> MapF (AssignId ids) (StackExpr arch ids)
forall arch ids.
BlockIntraStackConstraints arch ids
-> MapF (AssignId ids) (StackExpr arch ids)
assignExprMap BlockIntraStackConstraints arch ids
cns)
     in [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ Doc ann
"stackExprMap:"
             , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ann
forall ann. Doc ann
sm
             , Doc ann
"assignExprMap:"
             , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ann
forall ann. Doc ann
am
             ]


-- | Create index bounds from initial index bounds.
mkBlockIntraStackConstraints :: forall arch ids
                             .  (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch))
                             => BlockStartStackConstraints arch
                             -> BlockIntraStackConstraints arch ids
mkBlockIntraStackConstraints :: forall arch ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BlockIntraStackConstraints arch ids
mkBlockIntraStackConstraints BlockStartStackConstraints arch
cns =
  let stackExpr :: MemInt (ArchAddrWidth arch)
                -> MemRepr tp
                -> StackEqConstraint (ArchReg arch) tp
                -> StackExpr arch ids tp
      stackExpr :: forall (tp :: Type).
MemInt (ArchAddrWidth arch)
-> MemRepr tp
-> StackEqConstraint (ArchReg arch) tp
-> StackExpr arch ids tp
stackExpr MemInt (ArchAddrWidth arch)
i MemRepr tp
tp StackEqConstraint (ArchReg arch) tp
_ = BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
blockStartLocExpr BlockStartStackConstraints arch
cns (MemInt (ArchAddrWidth arch)
-> MemRepr tp -> BoundLoc (ArchReg arch) tp
forall (r :: Type -> Type) (tp :: Type).
MemInt (RegAddrWidth r) -> MemRepr tp -> BoundLoc r tp
StackOffLoc MemInt (ArchAddrWidth arch)
i MemRepr tp
tp)
   in BISC { biscInitConstraints :: BlockStartStackConstraints arch
biscInitConstraints = BlockStartStackConstraints arch
cns
           , stackExprMap :: MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
stackExprMap   = (forall (tp :: Type).
 MemInt (ArchAddrWidth arch)
 -> MemRepr tp
 -> StackEqConstraint (ArchReg arch) tp
 -> StackExpr arch ids tp)
-> MemMap
     (MemInt (ArchAddrWidth arch)) (StackEqConstraint (ArchReg arch))
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
forall o (a :: Type -> Type) (b :: Type -> Type).
(forall (tp :: Type). o -> MemRepr tp -> a tp -> b tp)
-> MemMap o a -> MemMap o b
memMapMapWithKey MemInt (ArchAddrWidth arch)
-> MemRepr tp
-> StackEqConstraint (ArchReg arch) tp
-> StackExpr arch ids tp
forall (tp :: Type).
MemInt (ArchAddrWidth arch)
-> MemRepr tp
-> StackEqConstraint (ArchReg arch) tp
-> StackExpr arch ids tp
stackExpr (LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> MemMap
     (MemInt (ArchAddrWidth arch)) (StackEqConstraint (ArchReg arch))
forall (r :: Type -> Type) (v :: Type -> Type).
LocMap r v -> MemMap (MemInt (RegAddrWidth r)) v
locMapStack (BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
forall arch.
BlockStartStackConstraints arch
-> LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
unBSSC BlockStartStackConstraints arch
cns))
           , assignExprMap :: MapF (AssignId ids) (StackExpr arch ids)
assignExprMap  = MapF (AssignId ids) (StackExpr arch ids)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
           }

-- | Return the value of the index expression given the bounds.
intraStackValueExpr :: forall arch ids tp
                    .  (MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch))
                    => BlockIntraStackConstraints arch ids
                    -> Value arch ids tp
                    -> StackExpr arch ids tp
intraStackValueExpr :: 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 tp
val =
  case Value arch ids tp
val of
    CValue CValue arch tp
c -> CValue arch tp -> StackExpr arch ids tp
forall arch (tp :: Type) ids.
CValue arch tp -> StackExpr arch ids tp
CExpr CValue arch tp
c
    AssignedValue (Assignment AssignId ids tp
aid AssignRhs arch (Value arch ids) tp
_) ->
      case AssignId ids tp
-> MapF (AssignId ids) (StackExpr arch ids)
-> Maybe (StackExpr arch ids 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 (BlockIntraStackConstraints arch ids
-> MapF (AssignId ids) (StackExpr arch ids)
forall arch ids.
BlockIntraStackConstraints arch ids
-> MapF (AssignId ids) (StackExpr arch ids)
assignExprMap BlockIntraStackConstraints arch ids
cns) of
        Just StackExpr arch ids tp
e -> StackExpr arch ids tp
e
        Maybe (StackExpr arch ids tp)
Nothing ->
          String -> StackExpr arch ids tp
forall a. HasCallStack => String -> a
error (String -> StackExpr arch ids tp)
-> String -> StackExpr arch ids tp
forall a b. (a -> b) -> a -> b
$ String -> ShowS
forall r. PrintfType r => String -> r
printf String
"Expected %s to be assigned." (Doc Any -> String
forall a. Show a => a -> String
show (AssignId ids tp -> Doc Any
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId ids tp
aid))
    Initial ArchReg arch tp
r -> BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), OrdF (ArchReg arch)) =>
BlockStartStackConstraints arch
-> BoundLoc (ArchReg arch) tp -> StackExpr arch ids tp
blockStartLocExpr (BlockIntraStackConstraints arch ids
-> BlockStartStackConstraints arch
forall arch ids.
BlockIntraStackConstraints arch ids
-> BlockStartStackConstraints arch
biscInitConstraints BlockIntraStackConstraints arch ids
cns) (ArchReg arch tp -> BoundLoc (ArchReg arch) tp
forall (r :: Type -> Type) (tp :: Type). r tp -> BoundLoc r tp
RegLoc ArchReg arch tp
r)

-- | Return an expression associated with the @AssignRhs@.
intraStackRhsExpr :: forall arch ids tp
                  .  ( MemWidth (ArchAddrWidth arch)
                     , OrdF (ArchReg arch)
                     , ShowF (ArchReg arch)
                     )
                  => BlockIntraStackConstraints arch ids
                  -> AssignId ids tp
                  -> AssignRhs arch (Value arch ids) tp
                  -> StackExpr arch ids tp
intraStackRhsExpr :: 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 =
  case AssignRhs arch (Value arch ids) tp
arhs of
    EvalApp (UExt Value arch ids (BVType m)
x NatRepr n
w) ->
      StackExpr arch ids (BVType m)
-> NatRepr n -> StackExpr arch ids ('BVType n)
forall (u :: Natural) (w :: Natural) arch ids.
(1 <= u, (u + 1) <= w) =>
StackExpr arch ids (BVType u)
-> NatRepr w -> StackExpr arch ids (BVType w)
UExtExpr (BlockIntraStackConstraints arch ids
-> Value arch ids (BVType m) -> StackExpr arch ids (BVType m)
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 m)
x) NatRepr n
w
    EvalApp App (Value arch ids) tp
app -> do
      let stackFn :: Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer
stackFn Value arch ids (BVType (ArchAddrWidth arch))
v =
            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 BlockIntraStackConstraints arch ids
cns Value arch ids (BVType (ArchAddrWidth arch))
v of
              StackOffsetExpr MemInt (ArchAddrWidth arch)
i -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (MemInt (ArchAddrWidth arch) -> Integer
forall a. Integral a => a -> Integer
toInteger MemInt (ArchAddrWidth arch)
i)
              StackExpr arch ids (BVType (ArchAddrWidth arch))
_ -> Maybe Integer
forall a. Maybe a
Nothing
      case (Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer)
-> App (Value arch ids) tp -> Maybe (StackOffsetView arch tp)
forall arch ids (tp :: Type).
MemWidth (ArchAddrWidth arch) =>
(Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer)
-> App (Value arch ids) tp -> Maybe (StackOffsetView arch tp)
appAsStackOffset Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer
stackFn App (Value arch ids) tp
app of
        Just (StackOffsetView Integer
o) -> do
          MemInt (ArchAddrWidth arch)
-> StackExpr arch ids (BVType (ArchAddrWidth arch))
forall arch ids.
MemInt (ArchAddrWidth arch)
-> StackExpr arch ids (BVType (ArchAddrWidth arch))
StackOffsetExpr (MemInt (ArchAddrWidth arch)
 -> StackExpr arch ids (BVType (ArchAddrWidth arch)))
-> MemInt (ArchAddrWidth arch)
-> StackExpr arch ids (BVType (ArchAddrWidth arch))
forall a b. (a -> b) -> a -> b
$ Integer -> MemInt (ArchAddrWidth arch)
forall a. Num a => Integer -> a
fromInteger Integer
o
        Maybe (StackOffsetView arch tp)
_ ->
          let a :: App (StackExpr arch ids) tp
a = (forall (x :: Type). Value arch ids x -> StackExpr arch ids x)
-> forall (x :: Type).
   App (Value arch ids) x -> App (StackExpr arch ids) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: Type -> Type) (g :: Type -> Type).
(forall (x :: Type). f x -> g x)
-> forall (x :: Type). App f x -> App g x
fmapFC (BlockIntraStackConstraints arch ids
-> Value arch ids x -> StackExpr arch ids x
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) App (Value arch ids) tp
app
           in AssignId ids tp
-> App (StackExpr arch ids) tp -> StackExpr arch ids tp
forall ids (tp :: Type) arch.
AssignId ids tp
-> App (StackExpr arch ids) tp -> StackExpr arch ids tp
AppExpr AssignId ids tp
aid App (StackExpr arch ids) tp
a
    ReadMem Value arch ids (BVType (ArchAddrWidth arch))
addr MemRepr tp
repr
      | StackOffsetExpr MemInt (ArchAddrWidth arch)
o <- 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 BlockIntraStackConstraints arch ids
cns Value arch ids (BVType (ArchAddrWidth arch))
addr
      , MMLResult StackExpr arch ids tp
e <- MemInt (ArchAddrWidth arch)
-> MemRepr tp
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
-> MemMapLookup
     (MemInt (ArchAddrWidth arch)) (StackExpr arch ids) tp
forall o (tp :: Type) (p :: Type -> Type).
MemIndex o =>
o -> MemRepr tp -> MemMap o p -> MemMapLookup o p tp
memMapLookup MemInt (ArchAddrWidth arch)
o MemRepr tp
repr (BlockIntraStackConstraints arch ids
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
forall arch ids.
BlockIntraStackConstraints arch ids
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
stackExprMap BlockIntraStackConstraints arch ids
cns) ->
        StackExpr arch ids tp
e
    AssignRhs arch (Value arch ids) tp
_ -> AssignId ids tp
-> AssignRhs arch (Value arch ids) tp -> StackExpr arch ids tp
forall ids (tp :: Type) arch.
AssignId ids tp
-> AssignRhs arch (Value arch ids) tp -> StackExpr arch ids tp
UninterpAssignExpr AssignId ids tp
aid AssignRhs arch (Value arch ids) tp
arhs

-- | Associate the given bound expression with the assignment.
intraStackSetAssignId :: AssignId ids tp
                      -> StackExpr arch ids tp
                      -> BlockIntraStackConstraints arch ids
                      -> BlockIntraStackConstraints arch ids
intraStackSetAssignId :: forall ids (tp :: Type) arch.
AssignId ids tp
-> StackExpr arch ids tp
-> BlockIntraStackConstraints arch ids
-> BlockIntraStackConstraints arch ids
intraStackSetAssignId AssignId ids tp
aid StackExpr arch ids tp
expr BlockIntraStackConstraints arch ids
cns =
  BlockIntraStackConstraints arch ids
cns { assignExprMap = MapF.insert aid expr (assignExprMap cns) }

-- | Discard information about memory due to an operation that may
-- affect arbitrary memory.
discardMemInfo :: BlockIntraStackConstraints arch ids
               -> BlockIntraStackConstraints arch ids
discardMemInfo :: forall arch ids.
BlockIntraStackConstraints arch ids
-> BlockIntraStackConstraints arch ids
discardMemInfo BlockIntraStackConstraints arch ids
cns =
  BlockIntraStackConstraints arch ids
cns { stackExprMap = emptyMemMap }

-- | Update the stack to point to the given expression.
writeStackOff :: forall arch ids tp
              .  (MemWidth (ArchAddrWidth arch), OrdF  (ArchReg arch))
              => BlockIntraStackConstraints arch ids
              -> MemInt (ArchAddrWidth arch)
              -> MemRepr tp
              -> Value arch ids tp
              -> BlockIntraStackConstraints arch ids
writeStackOff :: 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)
off MemRepr tp
repr Value arch ids tp
v =
  BlockIntraStackConstraints arch ids
cns { stackExprMap = memMapOverwrite off repr (intraStackValueExpr cns v) (stackExprMap cns) }

------------------------------------------------------------------------
-- NextStateMonad

-- | Maps bound expression that have been visited to their location.
--
-- We memoize expressions seen so that we can infer when two locations
-- must be equal.
data NextBlockState arch ids =
  NBS { forall arch ids.
NextBlockState arch ids
-> MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
nbsExprMap :: !(MapF (StackExpr arch ids) (BoundLoc (ArchReg arch) ))
      , forall arch ids.
NextBlockState arch ids
-> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
nbsRepLocs :: ![Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
        -- ^ List of location expression pairs
      }

-- Monad used for computing next states.
newtype NextStateMonad arch ids a = NSM (State (NextBlockState arch ids) a)
  deriving ((forall a b.
 (a -> b) -> NextStateMonad arch ids a -> NextStateMonad arch ids b)
-> (forall a b.
    a -> NextStateMonad arch ids b -> NextStateMonad arch ids a)
-> Functor (NextStateMonad arch ids)
forall a b.
a -> NextStateMonad arch ids b -> NextStateMonad arch ids a
forall a b.
(a -> b) -> NextStateMonad arch ids a -> NextStateMonad arch ids b
forall arch ids a b.
a -> NextStateMonad arch ids b -> NextStateMonad arch ids a
forall arch ids a b.
(a -> b) -> NextStateMonad arch ids a -> NextStateMonad arch ids b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall arch ids a b.
(a -> b) -> NextStateMonad arch ids a -> NextStateMonad arch ids b
fmap :: forall a b.
(a -> b) -> NextStateMonad arch ids a -> NextStateMonad arch ids b
$c<$ :: forall arch ids a b.
a -> NextStateMonad arch ids b -> NextStateMonad arch ids a
<$ :: forall a b.
a -> NextStateMonad arch ids b -> NextStateMonad arch ids a
Functor, Functor (NextStateMonad arch ids)
Functor (NextStateMonad arch ids) =>
(forall a. a -> NextStateMonad arch ids a)
-> (forall a b.
    NextStateMonad arch ids (a -> b)
    -> NextStateMonad arch ids a -> NextStateMonad arch ids b)
-> (forall a b c.
    (a -> b -> c)
    -> NextStateMonad arch ids a
    -> NextStateMonad arch ids b
    -> NextStateMonad arch ids c)
-> (forall a b.
    NextStateMonad arch ids a
    -> NextStateMonad arch ids b -> NextStateMonad arch ids b)
-> (forall a b.
    NextStateMonad arch ids a
    -> NextStateMonad arch ids b -> NextStateMonad arch ids a)
-> Applicative (NextStateMonad arch ids)
forall a. a -> NextStateMonad arch ids a
forall arch ids. Functor (NextStateMonad arch ids)
forall a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids a
forall a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids b
forall a b.
NextStateMonad arch ids (a -> b)
-> NextStateMonad arch ids a -> NextStateMonad arch ids b
forall arch ids a. a -> NextStateMonad arch ids a
forall a b c.
(a -> b -> c)
-> NextStateMonad arch ids a
-> NextStateMonad arch ids b
-> NextStateMonad arch ids c
forall arch ids a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids a
forall arch ids a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids b
forall arch ids a b.
NextStateMonad arch ids (a -> b)
-> NextStateMonad arch ids a -> NextStateMonad arch ids b
forall arch ids a b c.
(a -> b -> c)
-> NextStateMonad arch ids a
-> NextStateMonad arch ids b
-> NextStateMonad arch ids c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall arch ids a. a -> NextStateMonad arch ids a
pure :: forall a. a -> NextStateMonad arch ids a
$c<*> :: forall arch ids a b.
NextStateMonad arch ids (a -> b)
-> NextStateMonad arch ids a -> NextStateMonad arch ids b
<*> :: forall a b.
NextStateMonad arch ids (a -> b)
-> NextStateMonad arch ids a -> NextStateMonad arch ids b
$cliftA2 :: forall arch ids a b c.
(a -> b -> c)
-> NextStateMonad arch ids a
-> NextStateMonad arch ids b
-> NextStateMonad arch ids c
liftA2 :: forall a b c.
(a -> b -> c)
-> NextStateMonad arch ids a
-> NextStateMonad arch ids b
-> NextStateMonad arch ids c
$c*> :: forall arch ids a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids b
*> :: forall a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids b
$c<* :: forall arch ids a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids a
<* :: forall a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids a
Applicative, Applicative (NextStateMonad arch ids)
Applicative (NextStateMonad arch ids) =>
(forall a b.
 NextStateMonad arch ids a
 -> (a -> NextStateMonad arch ids b) -> NextStateMonad arch ids b)
-> (forall a b.
    NextStateMonad arch ids a
    -> NextStateMonad arch ids b -> NextStateMonad arch ids b)
-> (forall a. a -> NextStateMonad arch ids a)
-> Monad (NextStateMonad arch ids)
forall a. a -> NextStateMonad arch ids a
forall arch ids. Applicative (NextStateMonad arch ids)
forall a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids b
forall a b.
NextStateMonad arch ids a
-> (a -> NextStateMonad arch ids b) -> NextStateMonad arch ids b
forall arch ids a. a -> NextStateMonad arch ids a
forall arch ids a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids b
forall arch ids a b.
NextStateMonad arch ids a
-> (a -> NextStateMonad arch ids b) -> NextStateMonad arch ids b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall arch ids a b.
NextStateMonad arch ids a
-> (a -> NextStateMonad arch ids b) -> NextStateMonad arch ids b
>>= :: forall a b.
NextStateMonad arch ids a
-> (a -> NextStateMonad arch ids b) -> NextStateMonad arch ids b
$c>> :: forall arch ids a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids b
>> :: forall a b.
NextStateMonad arch ids a
-> NextStateMonad arch ids b -> NextStateMonad arch ids b
$creturn :: forall arch ids a. a -> NextStateMonad arch ids a
return :: forall a. a -> NextStateMonad arch ids a
Monad)

runNextStateMonad :: NextStateMonad arch ids a -> a
runNextStateMonad :: forall arch ids a. NextStateMonad arch ids a -> a
runNextStateMonad (NSM State (NextBlockState arch ids) a
m) = State (NextBlockState arch ids) a -> NextBlockState arch ids -> a
forall s a. State s a -> s -> a
evalState State (NextBlockState arch ids) a
m (NextBlockState arch ids -> a) -> NextBlockState arch ids -> a
forall a b. (a -> b) -> a -> b
$! NBS { nbsExprMap :: MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
nbsExprMap = MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty, nbsRepLocs :: [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
nbsRepLocs = [] }

-- | Return a list of locations and associated expressions that
-- represent equivalence classes in the next state.
--
-- Note that each equivalence class has a unique stack expression, so
-- all the locations in an equivalence class should have the same
-- expression.
getNextStateRepresentatives
  :: NextStateMonad arch ids [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
getNextStateRepresentatives :: forall arch ids.
NextStateMonad
  arch ids [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
getNextStateRepresentatives = State
  (NextBlockState arch ids)
  [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
-> NextStateMonad
     arch ids [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
forall arch ids a.
State (NextBlockState arch ids) a -> NextStateMonad arch ids a
NSM (State
   (NextBlockState arch ids)
   [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
 -> NextStateMonad
      arch ids [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
-> State
     (NextBlockState arch ids)
     [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
-> NextStateMonad
     arch ids [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
forall a b. (a -> b) -> a -> b
$ (NextBlockState arch ids
 -> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)])
-> State
     (NextBlockState arch ids)
     [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets NextBlockState arch ids
-> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
forall arch ids.
NextBlockState arch ids
-> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
nbsRepLocs

------------------------------------------------------------------------
-- BlockIntraStackConstraints next state

-- | Return the constraint associated with the given location and expression
-- or nothing if the constraint is the top one and should be stored.
nextStateStackEqConstraint
  :: ( MemWidth (ArchAddrWidth arch)
     , HasRepr (ArchReg arch) TypeRepr
     , OrdF (ArchReg arch)
     , ShowF (ArchReg arch)
     )
  => BoundLoc (ArchReg arch) tp
     -- ^ Location expression is stored at.
  -> StackExpr arch ids tp
     -- ^ Expression to infer predicate for.
  -> NextStateMonad arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
nextStateStackEqConstraint :: forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
nextStateStackEqConstraint BoundLoc (ArchReg arch) tp
loc StackExpr arch ids tp
e = do
  NextBlockState arch ids
s <- State (NextBlockState arch ids) (NextBlockState arch ids)
-> NextStateMonad arch ids (NextBlockState arch ids)
forall arch ids a.
State (NextBlockState arch ids) a -> NextStateMonad arch ids a
NSM (State (NextBlockState arch ids) (NextBlockState arch ids)
 -> NextStateMonad arch ids (NextBlockState arch ids))
-> State (NextBlockState arch ids) (NextBlockState arch ids)
-> NextStateMonad arch ids (NextBlockState arch ids)
forall a b. (a -> b) -> a -> b
$ State (NextBlockState arch ids) (NextBlockState arch ids)
forall s (m :: Type -> Type). MonadState s m => m s
get
  case StackExpr arch ids tp
-> MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
-> Maybe (BoundLoc (ArchReg arch) tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup StackExpr arch ids tp
e (NextBlockState arch ids
-> MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
forall arch ids.
NextBlockState arch ids
-> MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
nbsExprMap NextBlockState arch ids
s) of
    Just BoundLoc (ArchReg arch) tp
l ->
      Maybe (StackEqConstraint (ArchReg arch) tp)
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall a. a -> NextStateMonad arch ids a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe (StackEqConstraint (ArchReg arch) tp)
 -> NextStateMonad
      arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)))
-> Maybe (StackEqConstraint (ArchReg arch) tp)
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall a b. (a -> b) -> a -> b
$! StackEqConstraint (ArchReg arch) tp
-> Maybe (StackEqConstraint (ArchReg arch) tp)
forall a. a -> Maybe a
Just (StackEqConstraint (ArchReg arch) tp
 -> Maybe (StackEqConstraint (ArchReg arch) tp))
-> StackEqConstraint (ArchReg arch) tp
-> Maybe (StackEqConstraint (ArchReg arch) tp)
forall a b. (a -> b) -> a -> b
$ BoundLoc (ArchReg arch) tp -> StackEqConstraint (ArchReg arch) tp
forall (r :: Type -> Type) (tp :: Type).
BoundLoc r tp -> StackEqConstraint r tp
EqualLoc BoundLoc (ArchReg arch) tp
l
    Maybe (BoundLoc (ArchReg arch) tp)
Nothing -> do
      State (NextBlockState arch ids) () -> NextStateMonad arch ids ()
forall arch ids a.
State (NextBlockState arch ids) a -> NextStateMonad arch ids a
NSM (State (NextBlockState arch ids) () -> NextStateMonad arch ids ())
-> State (NextBlockState arch ids) () -> NextStateMonad arch ids ()
forall a b. (a -> b) -> a -> b
$ NextBlockState arch ids -> State (NextBlockState arch ids) ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put (NextBlockState arch ids -> State (NextBlockState arch ids) ())
-> NextBlockState arch ids -> State (NextBlockState arch ids) ()
forall a b. (a -> b) -> a -> b
$! NBS { nbsExprMap :: MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
nbsExprMap = StackExpr arch ids tp
-> BoundLoc (ArchReg arch) tp
-> MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
-> MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert StackExpr arch ids tp
e BoundLoc (ArchReg arch) tp
loc (NextBlockState arch ids
-> MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
forall arch ids.
NextBlockState arch ids
-> MapF (StackExpr arch ids) (BoundLoc (ArchReg arch))
nbsExprMap NextBlockState arch ids
s)
                       , nbsRepLocs :: [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
nbsRepLocs = BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair BoundLoc (ArchReg arch) tp
loc StackExpr arch ids tp
e Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)
-> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
-> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
forall a. a -> [a] -> [a]
: NextBlockState arch ids
-> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
forall arch ids.
NextBlockState arch ids
-> [Pair (BoundLoc (ArchReg arch)) (StackExpr arch ids)]
nbsRepLocs NextBlockState arch ids
s
                       }
      case StackExpr arch ids tp
e of
        StackOffsetExpr MemInt (ArchAddrWidth arch)
o ->
          Maybe (StackEqConstraint (ArchReg arch) tp)
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall a. a -> NextStateMonad arch ids a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe (StackEqConstraint (ArchReg arch) tp)
 -> NextStateMonad
      arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)))
-> Maybe (StackEqConstraint (ArchReg arch) tp)
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall a b. (a -> b) -> a -> b
$! (StackEqConstraint (ArchReg arch) tp
-> Maybe (StackEqConstraint (ArchReg arch) tp)
forall a. a -> Maybe a
Just (StackEqConstraint (ArchReg arch) tp
 -> Maybe (StackEqConstraint (ArchReg arch) tp))
-> StackEqConstraint (ArchReg arch) tp
-> Maybe (StackEqConstraint (ArchReg arch) tp)
forall a b. (a -> b) -> a -> b
$! MemInt (ArchAddrWidth arch)
-> StackEqConstraint (ArchReg arch) ('BVType (ArchAddrWidth arch))
forall (r :: Type -> Type).
MemInt (RegAddrWidth r)
-> StackEqConstraint r (BVType (RegAddrWidth r))
IsStackOff MemInt (ArchAddrWidth arch)
o)
        StackExpr arch ids tp
_ ->
          Maybe (StackEqConstraint (ArchReg arch) tp)
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall a. a -> NextStateMonad arch ids a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe (StackEqConstraint (ArchReg arch) tp)
 -> NextStateMonad
      arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)))
-> Maybe (StackEqConstraint (ArchReg arch) tp)
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall a b. (a -> b) -> a -> b
$! Maybe (StackEqConstraint (ArchReg arch) tp)
forall a. Maybe a
Nothing

-- | Bounds for block after jump
postJumpStackConstraints :: forall arch ids
                         .  RegisterInfo (ArchReg arch)
                         => BlockIntraStackConstraints arch ids
                         -- ^ Constraints at end of block.
                         -> RegState (ArchReg arch) (Value arch ids)
                         -- ^ Register values at start of next state.
                         --
                         -- Note. ip_reg is ignored, so it does not have to be up-to-date.
                         -> NextStateMonad arch ids (BlockStartStackConstraints arch)
postJumpStackConstraints :: 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 = do
  let postReg :: ArchReg arch tp
              -> Value arch ids tp
              -> NextStateMonad arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
      postReg :: forall (tp :: Type).
ArchReg arch tp
-> Value arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
postReg ArchReg arch tp
r Value arch ids tp
v =
        case ArchReg arch tp
-> ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
-> Maybe (tp :~: BVType (RegAddrWidth (ArchReg arch)))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
ArchReg arch a -> ArchReg arch b -> Maybe (a :~: b)
testEquality ArchReg arch tp
r ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
ip_reg of
          Just tp :~: BVType (RegAddrWidth (ArchReg arch))
Refl -> Maybe
  (StackEqConstraint
     (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))
-> NextStateMonad
     arch
     ids
     (Maybe
        (StackEqConstraint
           (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))))
forall a. a -> NextStateMonad arch ids a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe
  (StackEqConstraint
     (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))
forall a. Maybe a
Nothing
          Maybe (tp :~: BVType (RegAddrWidth (ArchReg arch)))
Nothing -> BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
nextStateStackEqConstraint (ArchReg arch tp -> BoundLoc (ArchReg arch) tp
forall (r :: Type -> Type) (tp :: Type). r tp -> BoundLoc r tp
RegLoc ArchReg arch tp
r) (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
cns Value arch ids tp
v)
  MapF (ArchReg arch) (StackEqConstraint (ArchReg arch))
rm <- (forall (tp :: Type).
 ArchReg arch tp
 -> Value arch ids tp
 -> NextStateMonad
      arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)))
-> MapF (ArchReg arch) (Value arch ids)
-> NextStateMonad
     arch ids (MapF (ArchReg arch) (StackEqConstraint (ArchReg arch)))
forall {v} (f :: Type -> Type) (k :: v -> Type) (a :: v -> Type)
       (b :: v -> Type).
Applicative f =>
(forall (tp :: v). k tp -> a tp -> f (Maybe (b tp)))
-> MapF k a -> f (MapF k b)
MapF.traverseMaybeWithKey ArchReg arch tp
-> Value arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall (tp :: Type).
ArchReg arch tp
-> Value arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
postReg (RegState (ArchReg arch) (Value arch ids)
-> MapF (ArchReg arch) (Value arch ids)
forall {v} (r :: v -> Type) (f :: v -> Type).
RegState r f -> MapF r f
regStateMap RegState (ArchReg arch) (Value arch ids)
regs)
  MemMap
  (MemInt (RegAddrWidth (ArchReg arch)))
  (StackEqConstraint (ArchReg arch))
sm <- (forall (tp :: Type).
 MemInt (RegAddrWidth (ArchReg arch))
 -> MemRepr tp
 -> StackExpr arch ids tp
 -> NextStateMonad
      arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)))
-> MemMap
     (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
-> NextStateMonad
     arch
     ids
     (MemMap
        (MemInt (RegAddrWidth (ArchReg arch)))
        (StackEqConstraint (ArchReg arch)))
forall (m :: Type -> Type) o (a :: Type -> Type)
       (b :: Type -> Type).
Applicative m =>
(forall (tp :: Type). o -> MemRepr tp -> a tp -> m (Maybe (b tp)))
-> MemMap o a -> m (MemMap o b)
memMapTraverseMaybeWithKey
          (\MemInt (RegAddrWidth (ArchReg arch))
i MemRepr tp
repr StackExpr arch ids tp
e -> BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
nextStateStackEqConstraint (MemInt (RegAddrWidth (ArchReg arch))
-> MemRepr tp -> BoundLoc (ArchReg arch) tp
forall (r :: Type -> Type) (tp :: Type).
MemInt (RegAddrWidth r) -> MemRepr tp -> BoundLoc r tp
StackOffLoc MemInt (RegAddrWidth (ArchReg arch))
i MemRepr tp
repr) StackExpr arch ids tp
e)
          (BlockIntraStackConstraints arch ids
-> MemMap
     (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
forall arch ids.
BlockIntraStackConstraints arch ids
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
stackExprMap BlockIntraStackConstraints arch ids
cns)
  BlockStartStackConstraints arch
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
forall a. a -> NextStateMonad arch ids a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BlockStartStackConstraints arch
 -> NextStateMonad arch ids (BlockStartStackConstraints arch))
-> BlockStartStackConstraints arch
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
forall a b. (a -> b) -> a -> b
$! LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> BlockStartStackConstraints arch
forall arch.
LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> BlockStartStackConstraints arch
BSSC (LocMap { locMapRegs :: MapF (ArchReg arch) (StackEqConstraint (ArchReg arch))
locMapRegs = MapF (ArchReg arch) (StackEqConstraint (ArchReg arch))
rm, locMapStack :: MemMap
  (MemInt (RegAddrWidth (ArchReg arch)))
  (StackEqConstraint (ArchReg arch))
locMapStack = MemMap
  (MemInt (RegAddrWidth (ArchReg arch)))
  (StackEqConstraint (ArchReg arch))
sm })

-- | Get the constraint associated with a register after a call.
postCallConstraint :: RegisterInfo (ArchReg arch)
                   => CallParams (ArchReg arch)
                      -- ^ Information about calling convention.
                   -> BlockIntraStackConstraints arch ids
                      -- ^ Bounds at end of this state.
                   -> ArchReg arch tp
                   -- ^ Register to get
                   -> Value arch ids tp
                   -- ^ Value of register at time call occurs.
                   -> NextStateMonad arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
postCallConstraint :: forall arch ids (tp :: Type).
RegisterInfo (ArchReg arch) =>
CallParams (ArchReg arch)
-> BlockIntraStackConstraints arch ids
-> ArchReg arch tp
-> Value arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
postCallConstraint CallParams (ArchReg arch)
params BlockIntraStackConstraints arch ids
cns ArchReg arch tp
r Value arch ids tp
v
  | Just tp :~: BVType (RegAddrWidth (ArchReg arch))
Refl <- ArchReg arch tp
-> ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
-> Maybe (tp :~: BVType (RegAddrWidth (ArchReg arch)))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
ArchReg arch a -> ArchReg arch b -> Maybe (a :~: b)
testEquality ArchReg arch tp
r ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
ip_reg =
      Maybe
  (StackEqConstraint
     (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))
-> NextStateMonad
     arch
     ids
     (Maybe
        (StackEqConstraint
           (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))))
forall a. a -> NextStateMonad arch ids a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe
  (StackEqConstraint
     (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))
forall a. Maybe a
Nothing
  | Just tp :~: BVType (RegAddrWidth (ArchReg arch))
Refl <- ArchReg arch tp
-> ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
-> Maybe (tp :~: BVType (RegAddrWidth (ArchReg arch)))
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
ArchReg arch a -> ArchReg arch b -> Maybe (a :~: b)
testEquality ArchReg arch tp
r ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
sp_reg
  , StackOffsetExpr MemInt (RegAddrWidth (ArchReg arch))
o <- 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
cns Value arch ids tp
v = do
      Maybe
  (StackEqConstraint
     (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))
-> NextStateMonad
     arch
     ids
     (Maybe
        (StackEqConstraint
           (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))))
forall a. a -> NextStateMonad arch ids a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Maybe
   (StackEqConstraint
      (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))
 -> NextStateMonad
      arch
      ids
      (Maybe
         (StackEqConstraint
            (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))))
-> Maybe
     (StackEqConstraint
        (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))
-> NextStateMonad
     arch
     ids
     (Maybe
        (StackEqConstraint
           (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))))
forall a b. (a -> b) -> a -> b
$! (StackEqConstraint
  (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))
-> Maybe
     (StackEqConstraint
        (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))
forall a. a -> Maybe a
Just (StackEqConstraint
   (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))
 -> Maybe
      (StackEqConstraint
         (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))))
-> StackEqConstraint
     (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))
-> Maybe
     (StackEqConstraint
        (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch))))
forall a b. (a -> b) -> a -> b
$! MemInt (RegAddrWidth (ArchReg arch))
-> StackEqConstraint
     (ArchReg arch) (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
MemInt (RegAddrWidth r)
-> StackEqConstraint r (BVType (RegAddrWidth r))
IsStackOff (MemInt (RegAddrWidth (ArchReg arch))
oMemInt (RegAddrWidth (ArchReg arch))
-> MemInt (RegAddrWidth (ArchReg arch))
-> MemInt (RegAddrWidth (ArchReg arch))
forall a. Num a => a -> a -> a
+Integer -> MemInt (RegAddrWidth (ArchReg arch))
forall a. Num a => Integer -> a
fromInteger (CallParams (ArchReg arch) -> Integer
forall (r :: Type -> Type). CallParams r -> Integer
postCallStackDelta CallParams (ArchReg arch)
params)))
  | CallParams (ArchReg arch)
-> forall (tp :: Type). ArchReg arch tp -> Bool
forall (r :: Type -> Type).
CallParams r -> forall (tp :: Type). r tp -> Bool
preserveReg CallParams (ArchReg arch)
params ArchReg arch tp
r =
      BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
nextStateStackEqConstraint (ArchReg arch tp -> BoundLoc (ArchReg arch) tp
forall (r :: Type -> Type) (tp :: Type). r tp -> BoundLoc r tp
RegLoc ArchReg arch tp
r) (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
cns Value arch ids tp
v)
  | Bool
otherwise =
      Maybe (StackEqConstraint (ArchReg arch) tp)
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall a. a -> NextStateMonad arch ids a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (StackEqConstraint (ArchReg arch) tp)
forall a. Maybe a
Nothing

-- | Return the index bounds after a function call.
postCallStackConstraints :: forall arch ids
                         .  RegisterInfo (ArchReg arch)
                         => CallParams (ArchReg arch)
                         -> BlockIntraStackConstraints arch ids
                         -> RegState (ArchReg arch) (Value arch ids)
                         -> NextStateMonad arch ids (BlockStartStackConstraints arch)
postCallStackConstraints :: 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 BlockIntraStackConstraints arch ids
cns RegState (ArchReg arch) (Value arch ids)
regs = do
  MapF (ArchReg arch) (StackEqConstraint (ArchReg arch))
rm <- (forall (tp :: Type).
 ArchReg arch tp
 -> Value arch ids tp
 -> NextStateMonad
      arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)))
-> MapF (ArchReg arch) (Value arch ids)
-> NextStateMonad
     arch ids (MapF (ArchReg arch) (StackEqConstraint (ArchReg arch)))
forall {v} (f :: Type -> Type) (k :: v -> Type) (a :: v -> Type)
       (b :: v -> Type).
Applicative f =>
(forall (tp :: v). k tp -> a tp -> f (Maybe (b tp)))
-> MapF k a -> f (MapF k b)
MapF.traverseMaybeWithKey (CallParams (ArchReg arch)
-> BlockIntraStackConstraints arch ids
-> ArchReg arch tp
-> Value arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall arch ids (tp :: Type).
RegisterInfo (ArchReg arch) =>
CallParams (ArchReg arch)
-> BlockIntraStackConstraints arch ids
-> ArchReg arch tp
-> Value arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
postCallConstraint CallParams (ArchReg arch)
params BlockIntraStackConstraints arch ids
cns) (RegState (ArchReg arch) (Value arch ids)
-> MapF (ArchReg arch) (Value arch ids)
forall {v} (r :: v -> Type) (f :: v -> Type).
RegState r f -> MapF r f
regStateMap RegState (ArchReg arch) (Value arch ids)
regs)

  let finalStack :: MemMap (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
finalStack = BlockIntraStackConstraints arch ids
-> MemMap
     (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
forall arch ids.
BlockIntraStackConstraints arch ids
-> MemMap (MemInt (ArchAddrWidth arch)) (StackExpr arch ids)
stackExprMap BlockIntraStackConstraints arch ids
cns
  let filteredStack :: MemMap (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
filteredStack =
        case BlockIntraStackConstraints arch ids
-> Value arch ids (BVType (RegAddrWidth (ArchReg arch)))
-> StackExpr arch ids (BVType (RegAddrWidth (ArchReg arch)))
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 (ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
-> RegState (ArchReg arch) (Value arch ids)
-> Value arch ids (BVType (RegAddrWidth (ArchReg arch)))
forall {k} (r :: k -> Type) (tp :: k) (f :: k -> Type).
OrdF r =>
r tp -> RegState r f -> f tp
getBoundValue ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
sp_reg RegState (ArchReg arch) (Value arch ids)
regs) of
          StackOffsetExpr MemInt (RegAddrWidth (ArchReg arch))
spOff
            | CallParams (ArchReg arch) -> Bool
forall (r :: Type -> Type). CallParams r -> Bool
stackGrowsDown CallParams (ArchReg arch)
params ->
                let newOff :: Integer
newOff = MemInt (RegAddrWidth (ArchReg arch)) -> Integer
forall a. Integral a => a -> Integer
toInteger MemInt (RegAddrWidth (ArchReg arch))
spOff Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ CallParams (ArchReg arch) -> Integer
forall (r :: Type -> Type). CallParams r -> Integer
postCallStackDelta CallParams (ArchReg arch)
params
                    -- Keep entries at offsets above return address.
                 in Integer
-> MemMap
     (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
-> MemMap
     (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
forall o (p :: Type -> Type).
Integral o =>
Integer -> MemMap o p -> MemMap o p
memMapDropBelow Integer
newOff MemMap (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
finalStack
            | Bool
otherwise ->
                let newOff :: Integer
newOff = MemInt (RegAddrWidth (ArchReg arch)) -> Integer
forall a. Integral a => a -> Integer
toInteger MemInt (RegAddrWidth (ArchReg arch))
spOff Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ CallParams (ArchReg arch) -> Integer
forall (r :: Type -> Type). CallParams r -> Integer
postCallStackDelta CallParams (ArchReg arch)
params
                    -- Keep entries whose high address is below new stack offset
                 in Integer
-> MemMap
     (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
-> MemMap
     (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
forall o (p :: Type -> Type).
Integral o =>
Integer -> MemMap o p -> MemMap o p
memMapDropAbove Integer
newOff MemMap (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
finalStack
          StackExpr arch ids (BVType (RegAddrWidth (ArchReg arch)))
_ -> MemMap (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
forall o (v :: Type -> Type). MemMap o v
emptyMemMap
  let nextStackFn :: MemInt (ArchAddrWidth arch)
                  -> MemRepr tp
                  -> StackExpr arch ids tp
                  -> NextStateMonad arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
      nextStackFn :: forall (tp :: Type).
MemInt (RegAddrWidth (ArchReg arch))
-> MemRepr tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
nextStackFn MemInt (RegAddrWidth (ArchReg arch))
i MemRepr tp
repr StackExpr arch ids tp
e =
        BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall arch (tp :: Type) ids.
(MemWidth (ArchAddrWidth arch), HasRepr (ArchReg arch) TypeRepr,
 OrdF (ArchReg arch), ShowF (ArchReg arch)) =>
BoundLoc (ArchReg arch) tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
nextStateStackEqConstraint (MemInt (RegAddrWidth (ArchReg arch))
-> MemRepr tp -> BoundLoc (ArchReg arch) tp
forall (r :: Type -> Type) (tp :: Type).
MemInt (RegAddrWidth r) -> MemRepr tp -> BoundLoc r tp
StackOffLoc MemInt (RegAddrWidth (ArchReg arch))
i MemRepr tp
repr) StackExpr arch ids tp
e
  MemMap
  (MemInt (RegAddrWidth (ArchReg arch)))
  (StackEqConstraint (ArchReg arch))
sm <- (forall (tp :: Type).
 MemInt (RegAddrWidth (ArchReg arch))
 -> MemRepr tp
 -> StackExpr arch ids tp
 -> NextStateMonad
      arch ids (Maybe (StackEqConstraint (ArchReg arch) tp)))
-> MemMap
     (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
-> NextStateMonad
     arch
     ids
     (MemMap
        (MemInt (RegAddrWidth (ArchReg arch)))
        (StackEqConstraint (ArchReg arch)))
forall (m :: Type -> Type) o (a :: Type -> Type)
       (b :: Type -> Type).
Applicative m =>
(forall (tp :: Type). o -> MemRepr tp -> a tp -> m (Maybe (b tp)))
-> MemMap o a -> m (MemMap o b)
memMapTraverseMaybeWithKey MemInt (RegAddrWidth (ArchReg arch))
-> MemRepr tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
forall (tp :: Type).
MemInt (RegAddrWidth (ArchReg arch))
-> MemRepr tp
-> StackExpr arch ids tp
-> NextStateMonad
     arch ids (Maybe (StackEqConstraint (ArchReg arch) tp))
nextStackFn MemMap (MemInt (RegAddrWidth (ArchReg arch))) (StackExpr arch ids)
filteredStack
  BlockStartStackConstraints arch
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
forall a. a -> NextStateMonad arch ids a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BlockStartStackConstraints arch
 -> NextStateMonad arch ids (BlockStartStackConstraints arch))
-> BlockStartStackConstraints arch
-> NextStateMonad arch ids (BlockStartStackConstraints arch)
forall a b. (a -> b) -> a -> b
$! LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> BlockStartStackConstraints arch
forall arch.
LocMap (ArchReg arch) (StackEqConstraint (ArchReg arch))
-> BlockStartStackConstraints arch
BSSC (LocMap { locMapRegs :: MapF (ArchReg arch) (StackEqConstraint (ArchReg arch))
locMapRegs = MapF (ArchReg arch) (StackEqConstraint (ArchReg arch))
rm
                       , locMapStack :: MemMap
  (MemInt (RegAddrWidth (ArchReg arch)))
  (StackEqConstraint (ArchReg arch))
locMapStack = MemMap
  (MemInt (RegAddrWidth (ArchReg arch)))
  (StackEqConstraint (ArchReg arch))
sm
                       })