{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Data.Macaw.AbsDomain.AbsState
  ( AbsBlockState
  , setAbsIP
  , absRegState
  , absStackHasReturnAddr
  , CallParams(..)
  , absEvalCall
  , AbsBlockStack
  , fnStartAbsBlockState
  , joinAbsBlockState
  , StackEntry(..)
  , ArchAbsValue
  , AbsValue(..)
  , bvadd
  , emptyAbsValue
  , concreteCodeAddr
  , joinAbsValue
  , ppAbsValue
  , absTrue
  , absFalse
  , subValue
  , concretize
  , asConcreteSingleton
  , meet
  , absValueSize
  , codePointerSet
  , AbsDomain(..)
  , AbsProcessorState
  , absMem
  , curAbsStack
  , absInitialRegs
  , initAbsProcessorState
  , absAssignments
  , assignLens
  , stridedInterval
  , finalAbsBlockState
  , addMemWrite
  , addCondMemWrite
  , transferValue
  , abstractULt
  , abstractULeq
  , isBottom
  , transferApp
    -- * Utilities
  , hasMaximum
  ) where

import           Control.Exception (assert)
import           Control.Lens
import           Control.Monad (guard)
import           Control.Monad.State.Strict (MonadState(..), State, modify, runState)
import           Data.Bits
import           Data.Foldable
import           Data.Int
import           Data.Map (Map)
import qualified Data.Map.Strict as Map
import           Data.Maybe
import           Data.Parameterized.Classes (EqF(..), ShowF(..))
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.NatRepr
import           Data.Set (Set)
import qualified Data.Set as Set
import           GHC.Stack
import           Numeric (showHex)
import           Prettyprinter

import           Data.Macaw.AbsDomain.CallParams
import qualified Data.Macaw.AbsDomain.StridedInterval as SI
import           Data.Macaw.CFG.App
import           Data.Macaw.CFG.Core
import           Data.Macaw.DebugLogging
import           Data.Macaw.Memory
import qualified Data.Macaw.Memory.Permissions as Perm
import           Data.Macaw.Types

------------------------------------------------------------------------
-- Utilities

-- | A helper for computing new signed offsets for values of type 'StackOffsetAbsVal'
--
-- This is a bit fiddly because 'StackOffsetAbsVal' has an 'Int64' as its second
-- value, so we need to be very careful when converting from bitvectors (encoded
-- as 'Integer') to 'Int64'.
addSignedOffset
  :: Int64   -- ^ The current offset of a 'StackOffsetAbsVal'
  -> Integer -- ^ The offset to add (to the current offset)
  -> Int64
addSignedOffset :: Int64 -> Integer -> Int64
addSignedOffset Int64
curOff Integer
i =
  Int64
curOff Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Integer -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i

-- | Add an offset represented as a bitvector to the current offset of a 'StackOffsetAbsVal'
--
-- Like 'addSignedOffset', this is tricky because the result is an 'Int64' while
-- bitvectors are represented as raw 'Integer'.
--
-- This handles the interpretation of the bitvector as an 'Int64'. It uses the
-- signed conversion function from the 'Data.Parameterized.NatRepr' module. This
-- takes the low @w@ bits of the Integer and represents it in twos-complement so
-- that the conversion to an 'Int64' properly sign extends.
addSignedOffsetBV
  :: (1 <= w)
  => NatRepr w
  -> Int64 -- ^ The current offset of a 'StackOffsetAbsVal'
  -> Integer -- ^ A *bitvector* of width @w@ represented as an 'Integer' to add to the current offset; it will be interpreted as signed
  -> Int64
addSignedOffsetBV :: forall (w :: Natural).
(1 <= w) =>
NatRepr w -> Int64 -> Integer -> Int64
addSignedOffsetBV NatRepr w
w Int64
curOff Integer
bv =
  Int64
curOff Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Integer -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatRepr w -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr w
w Integer
bv)

------------------------------------------------------------------------
-- AbsDomain

-- | This represents an lattice order.
--
-- Elements are comparable for equality, have a partial order, a top element,
-- and the ability to join to elements.
class Eq d => AbsDomain d where
  -- | The top element
  top :: d

  -- | A partial ordering over d.  forall x. x `leq` top
  leq :: d -> d -> Bool
  leq d
x d
y =
    case d -> d -> Maybe d
forall d. AbsDomain d => d -> d -> Maybe d
joinD d
y d
x of
      Maybe d
Nothing -> Bool
True
      Just d
_ -> Bool
False

  -- | Least upper bound (always defined, as we have top)
  lub :: d -> d -> d
  lub d
x d
y = case d -> d -> Maybe d
forall d. AbsDomain d => d -> d -> Maybe d
joinD d
x d
y of
              Maybe d
Nothing -> d
x
              Just d
r -> d
r

  -- | Join the old and new states and return the updated state iff
  -- the result is larger than the old state.
  joinD :: d -> d -> Maybe d
  joinD d
old d
new
    | d
new d -> d -> Bool
forall d. AbsDomain d => d -> d -> Bool
`leq` d
old = Maybe d
forall a. Maybe a
Nothing
    | Bool
otherwise     = d -> Maybe d
forall a. a -> Maybe a
Just (d -> Maybe d) -> d -> Maybe d
forall a b. (a -> b) -> a -> b
$ d -> d -> d
forall d. AbsDomain d => d -> d -> d
lub d
old d
new

  {-# MINIMAL (top, ((leq,lub) | joinD)) #-}

------------------------------------------------------------------------
-- AbsValue

-- | The abstract information that is associated with values of a given type.
--
-- The first parameter is the width of pointers on the value.  It is expected
-- to be at most 64 bits.
data AbsValue w (tp :: Type)
  = (tp ~ BoolType) => BoolConst !Bool
    -- ^ A Boolean constant
  | forall n . (tp ~ BVType n) => FinSet !(Set Integer)
    -- ^ Denotes that this value can take any one of the fixed set.
  | (tp ~ BVType w) => CodePointers !(Set (MemSegmentOff w)) !Bool
     -- ^ Represents that all values point to a bounded set of
     -- addresses in an executable segment or the constant zero.  The
     -- set contains the possible addresses, and the Boolean indicates
     -- whether this set contains the address 0.
  | (tp ~ BVType w) => StackOffsetAbsVal !(MemAddr w) !Int64
    -- ^ Offset of stack from the beginning of the block at the given address.
    --
    -- To avoid conflating offsets that are relative to the begining of different
    -- blocks, we include the address of the block as the first argument.
  | (tp ~ BVType w) => SomeStackOffset !(MemAddr w)
    -- ^ An offset to the stack at some offset.
    --
    -- Note. We do nothing to guarantee that this is a legal stack offset.
    --
    -- To avoid conflating offsets that are relative to the begining of different
    -- blocks, we include the address of the block as the first argument.
  | forall n . (tp ~ BVType n) => StridedInterval !(SI.StridedInterval n)
    -- ^ A strided interval
  | forall n n'
    . ((n + 1) <= n', tp ~ BVType n')
    => SubValue !(NatRepr n) !(AbsValue w (BVType n))
    -- ^ A sub-value about which we know something about the low order bits.
    --
    --e.g., when tp = BVType 16, and n = 8, and the abs value argument is @av@, we
    --know that the lower 8-bits of the value are in @av@, but the upper bits may
    -- be arbitrary.
  | TopV
    -- ^ Any value
  | (tp ~ BVType w) => ReturnAddr
    -- ^ Denotes a return address in the body of a function.

-- | Denotes that we do not know of any value that could be in set.
emptyAbsValue :: AbsValue w (BVType w)
emptyAbsValue :: forall (w :: Natural). AbsValue w (BVType w)
emptyAbsValue = Set (MemSegmentOff w) -> Bool -> AbsValue w (BVType w)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
Set (MemSegmentOff w) -> Bool -> AbsValue w tp
CodePointers Set (MemSegmentOff w)
forall a. Set a
Set.empty Bool
False

-- | Construct a abstract value for a pointer to a code address.
concreteCodeAddr :: MemSegmentOff w -> AbsValue w (BVType w)
concreteCodeAddr :: forall (w :: Natural). MemSegmentOff w -> AbsValue w (BVType w)
concreteCodeAddr MemSegmentOff w
addr = Set (MemSegmentOff w) -> Bool -> AbsValue w (BVType w)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
Set (MemSegmentOff w) -> Bool -> AbsValue w tp
CodePointers (MemSegmentOff w -> Set (MemSegmentOff w)
forall a. a -> Set a
Set.singleton MemSegmentOff w
addr) Bool
False

-- | Returns a finite set of values with some width.
data SomeFinSet tp where
  IsFin :: !(Set Integer) -> SomeFinSet (BVType n)
  NotFin :: SomeFinSet tp

-- | Given a segmented addr and flag indicating if zero is contained return the underlying
-- integer set and the set of addresses that had no base.
partitionAbsoluteAddrs :: MemWidth w
                        => Set (MemSegmentOff w)
                        -> Bool
                        -> (Set Integer, Set (MemSegmentOff w))
partitionAbsoluteAddrs :: forall (w :: Natural).
MemWidth w =>
Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
partitionAbsoluteAddrs Set (MemSegmentOff w)
addrSet Bool
b = ((Set Integer, Set (MemSegmentOff w))
 -> MemSegmentOff w -> (Set Integer, Set (MemSegmentOff w)))
-> (Set Integer, Set (MemSegmentOff w))
-> Set (MemSegmentOff w)
-> (Set Integer, Set (MemSegmentOff w))
forall b a. (b -> a -> b) -> b -> Set a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Set Integer, Set (MemSegmentOff w))
-> MemSegmentOff w -> (Set Integer, Set (MemSegmentOff w))
forall {w :: Natural}.
(Assert (OrdCond (CmpNat 1 w) 'True 'True 'False) (TypeError ...),
 MemWidth w) =>
(Set Integer, Set (MemSegmentOff w))
-> MemSegmentOff w -> (Set Integer, Set (MemSegmentOff w))
f (Set Integer
s0, Set (MemSegmentOff w)
forall a. Set a
Set.empty) Set (MemSegmentOff w)
addrSet
   where s0 :: Set Integer
s0 = if Bool
b then Integer -> Set Integer
forall a. a -> Set a
Set.singleton Integer
0 else Set Integer
forall a. Set a
Set.empty
         f :: (Set Integer, Set (MemSegmentOff w))
-> MemSegmentOff w -> (Set Integer, Set (MemSegmentOff w))
f (Set Integer
intSet,Set (MemSegmentOff w)
badSet) MemSegmentOff w
addr =
           case MemSegmentOff w -> Maybe (MemWord w)
forall (w :: Natural).
MemWidth w =>
MemSegmentOff w -> Maybe (MemWord w)
segoffAsAbsoluteAddr MemSegmentOff w
addr of
             Just MemWord w
addrVal -> Set Integer
-> (Set Integer, Set (MemSegmentOff w))
-> (Set Integer, Set (MemSegmentOff w))
forall a b. a -> b -> b
seq Set Integer
intSet' ((Set Integer, Set (MemSegmentOff w))
 -> (Set Integer, Set (MemSegmentOff w)))
-> (Set Integer, Set (MemSegmentOff w))
-> (Set Integer, Set (MemSegmentOff w))
forall a b. (a -> b) -> a -> b
$ (Set Integer
intSet', Set (MemSegmentOff w)
badSet)
               where intSet' :: Set Integer
intSet' = Integer -> Set Integer -> Set Integer
forall a. Ord a => a -> Set a -> Set a
Set.insert (MemWord w -> Integer
forall a. Integral a => a -> Integer
toInteger MemWord w
addrVal) Set Integer
intSet
             Maybe (MemWord w)
Nothing -> Set (MemSegmentOff w)
-> (Set Integer, Set (MemSegmentOff w))
-> (Set Integer, Set (MemSegmentOff w))
forall a b. a -> b -> b
seq Set (MemSegmentOff w)
badSet' ((Set Integer, Set (MemSegmentOff w))
 -> (Set Integer, Set (MemSegmentOff w)))
-> (Set Integer, Set (MemSegmentOff w))
-> (Set Integer, Set (MemSegmentOff w))
forall a b. (a -> b) -> a -> b
$ (Set Integer
intSet, Set (MemSegmentOff w)
badSet')
               where badSet' :: Set (MemSegmentOff w)
badSet' = MemSegmentOff w -> Set (MemSegmentOff w) -> Set (MemSegmentOff w)
forall a. Ord a => a -> Set a -> Set a
Set.insert MemSegmentOff w
addr Set (MemSegmentOff w)
badSet

asFinSet :: forall w tp
         .  MemWidth w
         => String
         -> AbsValue w tp
         -> SomeFinSet tp
asFinSet :: forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
_ (FinSet Set Integer
s) = Set Integer -> SomeFinSet (BVType n)
forall (n :: Natural). Set Integer -> SomeFinSet (BVType n)
IsFin Set Integer
s
asFinSet String
_ (CodePointers Set (MemSegmentOff w)
s Bool
False)
  | Set (MemSegmentOff w) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff w)
s = Set Integer -> SomeFinSet (BVType w)
forall (n :: Natural). Set Integer -> SomeFinSet (BVType n)
IsFin Set Integer
forall a. Set a
Set.empty
asFinSet String
_ (CodePointers Set (MemSegmentOff w)
s Bool
True)
  | Set (MemSegmentOff w) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff w)
s = Set Integer -> SomeFinSet (BVType w)
forall (n :: Natural). Set Integer -> SomeFinSet (BVType n)
IsFin (Integer -> Set Integer
forall a. a -> Set a
Set.singleton Integer
0)
asFinSet String
nm (CodePointers Set (MemSegmentOff w)
addrSet Bool
b) = [MemSegmentOff w] -> Set Integer -> SomeFinSet (BVType w)
go (Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
addrSet) (Set Integer -> SomeFinSet tp) -> Set Integer -> SomeFinSet tp
forall a b. (a -> b) -> a -> b
$! Set Integer
s0
  where s0 :: Set Integer
s0 = if Bool
b then Integer -> Set Integer
forall a. a -> Set a
Set.singleton Integer
0 else Set Integer
forall a. Set a
Set.empty
        go :: [MemSegmentOff w] -> Set Integer -> SomeFinSet (BVType w)
        go :: [MemSegmentOff w] -> Set Integer -> SomeFinSet (BVType w)
go [] Set Integer
s = DebugClass
-> String -> SomeFinSet (BVType w) -> SomeFinSet (BVType w)
forall a. (?loc::CallStack) => DebugClass -> String -> a -> a
debug DebugClass
DAbsInt (String
"dropping Codeptr " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm) (SomeFinSet (BVType w) -> SomeFinSet (BVType w))
-> SomeFinSet (BVType w) -> SomeFinSet (BVType w)
forall a b. (a -> b) -> a -> b
$ Set Integer -> SomeFinSet (BVType w)
forall (n :: Natural). Set Integer -> SomeFinSet (BVType n)
IsFin Set Integer
s
        go (MemSegmentOff w
seg_off: [MemSegmentOff w]
r) Set Integer
s =
          case MemSegmentOff w -> Maybe (MemWord w)
forall (w :: Natural).
MemWidth w =>
MemSegmentOff w -> Maybe (MemWord w)
segoffAsAbsoluteAddr MemSegmentOff w
seg_off of
            Just MemWord w
addr -> [MemSegmentOff w] -> Set Integer -> SomeFinSet (BVType w)
go [MemSegmentOff w]
r (Set Integer -> SomeFinSet (BVType w))
-> Set Integer -> SomeFinSet (BVType w)
forall a b. (a -> b) -> a -> b
$! Integer -> Set Integer -> Set Integer
forall a. Ord a => a -> Set a -> Set a
Set.insert (MemWord w -> Integer
forall a. Integral a => a -> Integer
toInteger MemWord w
addr) Set Integer
s
            Maybe (MemWord w)
Nothing -> SomeFinSet (BVType w)
forall (tp :: Type). SomeFinSet tp
NotFin
asFinSet String
_ AbsValue w tp
_ = SomeFinSet tp
forall (tp :: Type). SomeFinSet tp
NotFin

-- asFinSet64 :: String -> AbsValue (BVType 64) -> Maybe (Set Word64)
-- asFinSet64 _ (FinSet s) = Just $! (Set.mapMonotonic fromInteger s)
-- asFinSet64 nm (CodePointers s)
--   | isZeroPtr s = Just s
--   | otherwise = debug DAbsInt ("dropping Codeptr " ++ nm) $ Just s
-- asFinSet64 _ _ = Nothing

codePointerSet :: AbsValue w tp -> Set (MemSegmentOff w)
codePointerSet :: forall (w :: Natural) (tp :: Type).
AbsValue w tp -> Set (MemSegmentOff w)
codePointerSet (CodePointers Set (MemSegmentOff w)
s Bool
_) = Set (MemSegmentOff w)
s
codePointerSet AbsValue w tp
_ = Set (MemSegmentOff w)
forall a. Set a
Set.empty

-- | The maximum number of values we hold in a value set, after which we move to
-- intervals
maxSetSize :: Int
maxSetSize :: Int
maxSetSize = Int
5

-- Note that this is syntactic equality only.
instance Eq (AbsValue w tp) where
  FinSet Set Integer
x    == :: AbsValue w tp -> AbsValue w tp -> Bool
== FinSet Set Integer
y      = Set Integer
x Set Integer -> Set Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set Integer
y
  CodePointers Set (MemSegmentOff w)
x Bool
xb == CodePointers Set (MemSegmentOff w)
y Bool
yb = Set (MemSegmentOff w)
x Set (MemSegmentOff w) -> Set (MemSegmentOff w) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (MemSegmentOff w)
y Bool -> Bool -> Bool
&& Bool
xb Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
yb
  StackOffsetAbsVal MemAddr w
ax Int64
ox  == StackOffsetAbsVal MemAddr w
ay Int64
oy   = (MemAddr w
ax,Int64
ox) (MemAddr w, Int64) -> (MemAddr w, Int64) -> Bool
forall a. Eq a => a -> a -> Bool
== (MemAddr w
ay,Int64
oy)
  SomeStackOffset MemAddr w
ax == SomeStackOffset MemAddr w
ay = MemAddr w
ax MemAddr w -> MemAddr w -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr w
ay
  StridedInterval StridedInterval n
si1 == StridedInterval StridedInterval n
si2 = StridedInterval n
si1 StridedInterval n -> StridedInterval n -> Bool
forall a. Eq a => a -> a -> Bool
== StridedInterval n
StridedInterval n
si2
  SubValue NatRepr n
n AbsValue w (BVType n)
v == SubValue NatRepr n
n' AbsValue w (BVType n)
v'
    | Just n :~: n
Refl <- NatRepr n -> NatRepr n -> Maybe (n :~: n)
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 n
n NatRepr n
n' = AbsValue w (BVType n)
v AbsValue w (BVType n) -> AbsValue w (BVType n) -> Bool
forall a. Eq a => a -> a -> Bool
== AbsValue w (BVType n)
AbsValue w (BVType n)
v'
    | Bool
otherwise = Bool
False
  AbsValue w tp
TopV == AbsValue w tp
TopV = Bool
True
  AbsValue w tp
ReturnAddr == AbsValue w tp
ReturnAddr = Bool
True
  AbsValue w tp
_    == AbsValue w tp
_    = Bool
False

instance EqF (AbsValue w) where
  eqF :: forall (a :: Type). AbsValue w a -> AbsValue w a -> Bool
eqF = AbsValue w a -> AbsValue w a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

instance MemWidth w => Show (AbsValue w tp) where
  show :: AbsValue w tp -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (AbsValue w tp -> Doc Any) -> AbsValue w tp -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsValue w tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. AbsValue w tp -> Doc ann
pretty

ppSet :: [Doc ann] -> Doc ann
ppSet :: forall ann. [Doc ann] -> Doc ann
ppSet = Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep Doc ann
forall ann. Doc ann
lbrace Doc ann
forall ann. Doc ann
rbrace Doc ann
forall ann. Doc ann
comma

instance MemWidth w => Pretty (AbsValue w tp) where
  pretty :: forall ann. AbsValue w tp -> Doc ann
pretty (BoolConst Bool
b) = Bool -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Bool
b
  pretty (FinSet Set Integer
s) = Doc ann
"finset" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Set Integer -> Doc ann
forall w ann. (Integral w, Show w) => Set w -> Doc ann
ppIntegerSet Set Integer
s
  pretty (CodePointers Set (MemSegmentOff w)
s Bool
b) = Doc ann
"code" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
ppSet ([Doc ann]
s0 [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [Doc ann]
sd)
    where s0 :: [Doc ann]
s0 = if Bool
b then [Doc ann
"0"] else []
          sd :: [Doc ann]
sd = MemSegmentOff w -> Doc ann
forall a ann. Show a => a -> Doc ann
f (MemSegmentOff w -> Doc ann) -> [MemSegmentOff w] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
s
          f :: a -> Doc ann
f a
segAddr = a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow a
segAddr

  pretty (StridedInterval StridedInterval n
s) =
    Doc ann
"strided" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (StridedInterval n -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. StridedInterval n -> Doc ann
pretty StridedInterval n
s)
  pretty (SubValue NatRepr n
n AbsValue w (BVType n)
av) =
    Doc ann
"sub" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (NatRepr n -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr n
n) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
comma Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> AbsValue w (BVType n) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. AbsValue w (BVType n) -> Doc ann
pretty AbsValue w (BVType n)
av)
  pretty (StackOffsetAbsVal MemAddr w
a Int64
v')
    | Int64
v' Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int64
0   = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ String
"rsp_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ MemAddr w -> String
forall a. Show a => a -> String
show MemAddr w
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int64 -> String -> String
forall a. Integral a => a -> String -> String
showHex Int64
v' String
""
    | Bool
otherwise = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ String
"rsp_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ MemAddr w -> String
forall a. Show a => a -> String
show MemAddr w
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String -> String
forall a. Integral a => a -> String -> String
showHex (Integer -> Integer
forall a. Num a => a -> a
negate (Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger Int64
v')) String
""
  pretty (SomeStackOffset MemAddr w
a) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ String
"rsp_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ MemAddr w -> String
forall a. Show a => a -> String
show MemAddr w
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + ?"
  pretty AbsValue w tp
TopV = Doc ann
"top"
  pretty AbsValue w tp
ReturnAddr = Doc ann
"return_addr"

ppIntegerSet :: (Integral w, Show w) => Set w -> Doc ann
ppIntegerSet :: forall w ann. (Integral w, Show w) => Set w -> Doc ann
ppIntegerSet Set w
s = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
ppSet (w -> Doc ann
forall {a} {ann}. Integral a => a -> Doc ann
ppv (w -> Doc ann) -> [w] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Set w -> [w]
forall a. Set a -> [a]
Set.toList Set w
s)
  where ppv :: a -> Doc ann
ppv a
v' | a
v' a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (a -> String -> String
forall a. Integral a => a -> String -> String
showHex a
v' String
"")
               | Bool
otherwise = String -> Doc ann
forall a. HasCallStack => String -> a
error String
"ppIntegerSet given negative value"

-- | Returns a set of concrete integers that this value may be.
-- This function will neither return the complete set or an
-- known under-approximation.
concretize :: MemWidth w => AbsValue w tp -> Maybe (Set Integer)
concretize :: forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> Maybe (Set Integer)
concretize (FinSet Set Integer
s) = Set Integer -> Maybe (Set Integer)
forall a. a -> Maybe a
Just Set Integer
s
concretize (CodePointers Set (MemSegmentOff w)
s Bool
b) = Set Integer -> Maybe (Set Integer)
forall a. a -> Maybe a
Just (Set Integer -> Maybe (Set Integer))
-> Set Integer -> Maybe (Set Integer)
forall a b. (a -> b) -> a -> b
$ [Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList ([Integer] -> Set Integer) -> [Integer] -> Set Integer
forall a b. (a -> b) -> a -> b
$
  [ MemWord w -> Integer
forall a. Integral a => a -> Integer
toInteger MemWord w
addr
  | MemSegmentOff w
mseg <- Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
s
  , MemWord w
addr <- Maybe (MemWord w) -> [MemWord w]
forall a. Maybe a -> [a]
maybeToList (MemSegmentOff w -> Maybe (MemWord w)
forall (w :: Natural).
MemWidth w =>
MemSegmentOff w -> Maybe (MemWord w)
segoffAsAbsoluteAddr MemSegmentOff w
mseg)
  ]
  [Integer] -> [Integer] -> [Integer]
forall a. [a] -> [a] -> [a]
++ (if Bool
b then [Integer
0] else [])
concretize (SubValue NatRepr n
_ AbsValue w (BVType n)
_) = Maybe (Set Integer)
forall a. Maybe a
Nothing -- we know nothing about _all_ values
concretize (StridedInterval StridedInterval n
s) =
  DebugClass -> String -> Maybe (Set Integer) -> Maybe (Set Integer)
forall a. (?loc::CallStack) => DebugClass -> String -> a -> a
debug DebugClass
DAbsInt (String
"Concretizing " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (StridedInterval n -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. StridedInterval n -> Doc ann
pretty StridedInterval n
s)) (Maybe (Set Integer) -> Maybe (Set Integer))
-> Maybe (Set Integer) -> Maybe (Set Integer)
forall a b. (a -> b) -> a -> b
$
  Set Integer -> Maybe (Set Integer)
forall a. a -> Maybe a
Just ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList (StridedInterval n -> [Integer]
forall (w :: Natural). StridedInterval w -> [Integer]
SI.toList StridedInterval n
s))
concretize (BoolConst Bool
b) = Set Integer -> Maybe (Set Integer)
forall a. a -> Maybe a
Just (Integer -> Set Integer
forall a. a -> Set a
Set.singleton (if Bool
b then Integer
1 else Integer
0))
concretize StackOffsetAbsVal{} = Maybe (Set Integer)
forall a. Maybe a
Nothing
concretize SomeStackOffset{} = Maybe (Set Integer)
forall a. Maybe a
Nothing
concretize AbsValue w tp
TopV       = Maybe (Set Integer)
forall a. Maybe a
Nothing
concretize AbsValue w tp
ReturnAddr = Maybe (Set Integer)
forall a. Maybe a
Nothing

-- FIXME: make total, we would need to carry around tp
absValueSize :: AbsValue w tp -> Maybe Integer
absValueSize :: forall (w :: Natural) (tp :: Type). AbsValue w tp -> Maybe Integer
absValueSize (FinSet Set Integer
s) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Set Integer -> Int
forall a. Set a -> Int
Set.size Set Integer
s)
absValueSize (CodePointers Set (MemSegmentOff w)
s Bool
b) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Set (MemSegmentOff w) -> Int
forall a. Set a -> Int
Set.size Set (MemSegmentOff w)
s) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (if Bool
b then Integer
1 else Integer
0)
absValueSize (StridedInterval StridedInterval n
s) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ StridedInterval n -> Integer
forall (tp :: Natural). StridedInterval tp -> Integer
SI.size StridedInterval n
s
absValueSize (StackOffsetAbsVal MemAddr w
_ Int64
_) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
absValueSize SomeStackOffset{} = Maybe Integer
forall a. Maybe a
Nothing
absValueSize (BoolConst Bool
_)     = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
1
absValueSize SubValue{} = Maybe Integer
forall a. Maybe a
Nothing
absValueSize AbsValue w tp
TopV       = Maybe Integer
forall a. Maybe a
Nothing
absValueSize AbsValue w tp
ReturnAddr = Maybe Integer
forall a. Maybe a
Nothing

-- | Returns single value, if the abstract value can only take on one value.
asConcreteSingleton :: MemWidth w => AbsValue w tp -> Maybe Integer
asConcreteSingleton :: forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> Maybe Integer
asConcreteSingleton AbsValue w tp
v = do
  Integer
sz <- AbsValue w tp -> Maybe Integer
forall (w :: Natural) (tp :: Type). AbsValue w tp -> Maybe Integer
absValueSize AbsValue w tp
v
  Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Integer
sz Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1)
  [Integer
i] <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList (Set Integer -> [Integer])
-> Maybe (Set Integer) -> Maybe [Integer]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsValue w tp -> Maybe (Set Integer)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> Maybe (Set Integer)
concretize AbsValue w tp
v
  Integer -> Maybe Integer
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
i

-- -----------------------------------------------------------------------------
-- Smart constructors

-- | Smart constructor for strided intervals which takes care of top
stridedInterval :: SI.StridedInterval n -> AbsValue w (BVType n)
stridedInterval :: forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval StridedInterval n
si
  | StridedInterval n -> Bool
forall (w :: Natural). StridedInterval w -> Bool
SI.isTop StridedInterval n
si = AbsValue w (BVType n)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
  | Bool
otherwise   = StridedInterval n -> AbsValue w (BVType n)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
StridedInterval n -> AbsValue w tp
StridedInterval StridedInterval n
si

-- | Smart constructor for sub-values.  This ensures that the
-- subvalues are sorted on size.
subValue :: ((n + 1) <= n')
         => NatRepr n
         -> AbsValue w (BVType n)
         -> AbsValue w (BVType n')
subValue :: forall (n :: Natural) (n' :: Natural) (w :: Natural).
((n + 1) <= n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
subValue NatRepr n
n AbsValue w (BVType n)
v
  | AbsValue w (BVType n)
TopV <- AbsValue w (BVType n)
v = AbsValue w (BVType n')
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
  | Bool
otherwise = NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
forall (w :: Natural) (tp :: Type) (n :: Natural) (n' :: Natural).
((n + 1) <= n', tp ~ BVType n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w tp
SubValue NatRepr n
n AbsValue w (BVType n)
v

isEmpty :: AbsValue w tp -> Bool
isEmpty :: forall (w :: Natural) (tp :: Type). AbsValue w tp -> Bool
isEmpty (CodePointers Set (MemSegmentOff w)
s Bool
b) = Set (MemSegmentOff w) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff w)
s Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
b
isEmpty (FinSet Set Integer
s) = Set Integer -> Bool
forall a. Set a -> Bool
Set.null Set Integer
s
isEmpty AbsValue w tp
_ = Bool
False

-------------------------------------------------------------------------------
-- Joining abstract values

instance MemWidth w => AbsDomain (AbsValue w tp) where
  top :: AbsValue w tp
top = AbsValue w tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
  joinD :: AbsValue w tp -> AbsValue w tp -> Maybe (AbsValue w tp)
joinD = AbsValue w tp -> AbsValue w tp -> Maybe (AbsValue w tp)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> Maybe (AbsValue w tp)
joinAbsValue

-- | Join the old and new states and return the updated state iff
-- the result is larger than the old state.
-- This also returns any addresses that are discarded during joining.
joinAbsValue :: MemWidth w
             => AbsValue w tp
             -> AbsValue w tp
             -> Maybe (AbsValue w tp)
joinAbsValue :: forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> Maybe (AbsValue w tp)
joinAbsValue AbsValue w tp
x AbsValue w tp
y
    | Set (MemSegmentOff w) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff w)
s = Maybe (AbsValue w tp)
r
    | Bool
otherwise = DebugClass
-> String -> Maybe (AbsValue w tp) -> Maybe (AbsValue w tp)
forall a. (?loc::CallStack) => DebugClass -> String -> a -> a
debug DebugClass
DAbsInt (String
"dropping " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show Doc Any
dropped String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ AbsValue w tp -> String
forall a. Show a => a -> String
show AbsValue w tp
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ AbsValue w tp -> String
forall a. Show a => a -> String
show AbsValue w tp
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n") Maybe (AbsValue w tp)
r
  where (Maybe (AbsValue w tp)
r,Set (MemSegmentOff w)
s) = State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
-> Set (MemSegmentOff w)
-> (Maybe (AbsValue w tp), Set (MemSegmentOff w))
forall s a. State s a -> s -> (a, s)
runState (AbsValue w tp
-> AbsValue w tp
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp
-> AbsValue w tp
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
joinAbsValue' AbsValue w tp
x AbsValue w tp
y) Set (MemSegmentOff w)
forall a. Set a
Set.empty
        dropped :: Doc Any
dropped = [Doc Any] -> Doc Any
forall ann. [Doc ann] -> Doc ann
ppSet (MemSegmentOff w -> Doc Any
forall a ann. Show a => a -> Doc ann
viaShow (MemSegmentOff w -> Doc Any) -> [MemSegmentOff w] -> [Doc Any]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
s)

addWords :: Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords :: forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords Set (MemSegmentOff w)
s = (Set (MemSegmentOff w) -> Set (MemSegmentOff w))
-> StateT (Set (MemSegmentOff w)) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((Set (MemSegmentOff w) -> Set (MemSegmentOff w))
 -> StateT (Set (MemSegmentOff w)) Identity ())
-> (Set (MemSegmentOff w) -> Set (MemSegmentOff w))
-> StateT (Set (MemSegmentOff w)) Identity ()
forall a b. (a -> b) -> a -> b
$ Set (MemSegmentOff w)
-> Set (MemSegmentOff w) -> Set (MemSegmentOff w)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (MemSegmentOff w)
s

-- | Join the old and new states and return the updated state iff
-- the result is larger than the old state.
-- This also returns any addresses that are discarded during joining.
joinAbsValue' :: MemWidth w
              => AbsValue w tp
              -> AbsValue w tp
              -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
joinAbsValue' :: forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp
-> AbsValue w tp
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
joinAbsValue' AbsValue w tp
TopV AbsValue w tp
x = do
  Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords (AbsValue w tp -> Set (MemSegmentOff w)
forall (w :: Natural) (tp :: Type).
AbsValue w tp -> Set (MemSegmentOff w)
codePointerSet AbsValue w tp
x)
  Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$! Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
joinAbsValue' AbsValue w tp
x AbsValue w tp
y | AbsValue w tp -> Bool
forall (w :: Natural) (tp :: Type). AbsValue w tp -> Bool
isEmpty AbsValue w tp
y = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
                  | AbsValue w tp -> Bool
forall (w :: Natural) (tp :: Type). AbsValue w tp -> Bool
isEmpty AbsValue w tp
x = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ (AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just (AbsValue w tp -> Maybe (AbsValue w tp))
-> AbsValue w tp -> Maybe (AbsValue w tp)
forall a b. (a -> b) -> a -> b
$! AbsValue w tp
y)
joinAbsValue' (CodePointers Set (MemSegmentOff w)
old Bool
old_b) (CodePointers Set (MemSegmentOff w)
new Bool
new_b)
    | Set (MemSegmentOff w)
new Set (MemSegmentOff w) -> Set (MemSegmentOff w) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set (MemSegmentOff w)
old Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
new_b Bool -> Bool -> Bool
|| Bool
old_b) = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
    | Bool
otherwise = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ (AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just (AbsValue w tp -> Maybe (AbsValue w tp))
-> AbsValue w tp -> Maybe (AbsValue w tp)
forall a b. (a -> b) -> a -> b
$! Set (MemSegmentOff w) -> Bool -> AbsValue w tp
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
Set (MemSegmentOff w) -> Bool -> AbsValue w tp
CodePointers Set (MemSegmentOff w)
r (Bool
old_b Bool -> Bool -> Bool
|| Bool
new_b))
  where r :: Set (MemSegmentOff w)
r = Set (MemSegmentOff w)
-> Set (MemSegmentOff w) -> Set (MemSegmentOff w)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (MemSegmentOff w)
old Set (MemSegmentOff w)
new
joinAbsValue' (FinSet Set Integer
old) (CodePointers Set (MemSegmentOff w)
new_set Bool
new_zero)
    | Set Integer
wordSet Set Integer -> Set Integer -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set Integer
old = do
      Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords Set (MemSegmentOff w)
new_set
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
    | Set Integer -> Int
forall a. Set a -> Int
Set.size Set Integer
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxSetSize = do
      Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords Set (MemSegmentOff w)
new_set
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just AbsValue w tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
    | Bool
otherwise = do
      Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords Set (MemSegmentOff w)
new_set
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just (Set Integer -> AbsValue w tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet Set Integer
r)

  where (Set Integer
wordSet,Set (MemSegmentOff w)
_) = Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
forall (w :: Natural).
MemWidth w =>
Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
partitionAbsoluteAddrs Set (MemSegmentOff w)
new_set Bool
new_zero
        r :: Set Integer
r = Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Integer
old Set Integer
wordSet

joinAbsValue' (CodePointers Set (MemSegmentOff w)
old Bool
old_zero) (FinSet Set Integer
new)
    | Set Integer -> Int
forall a. Set a -> Int
Set.size Set Integer
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxSetSize = do
      Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords Set (MemSegmentOff w)
old
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just AbsValue w tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
    | Bool
otherwise = do
      Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords Set (MemSegmentOff w)
old
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just (Set Integer -> AbsValue w tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet Set Integer
r)
  where (Set Integer
wordSet,Set (MemSegmentOff w)
_) = Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
forall (w :: Natural).
MemWidth w =>
Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
partitionAbsoluteAddrs Set (MemSegmentOff w)
old Bool
old_zero
        r :: Set Integer
r = Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Integer
wordSet Set Integer
new
joinAbsValue' (FinSet Set Integer
old) (FinSet Set Integer
new)
    | Set Integer
new Set Integer -> Set Integer -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set Integer
old = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
    | Set Integer -> Int
forall a. Set a -> Int
Set.size Set Integer
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxSetSize = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just AbsValue w tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
    | Bool
otherwise = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just (Set Integer -> AbsValue w tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet Set Integer
r)
  where r :: Set Integer
r = Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Integer
old Set Integer
new
joinAbsValue' (StackOffsetAbsVal MemAddr w
a_old Int64
old) (StackOffsetAbsVal MemAddr w
b_old Int64
new)
    | MemAddr w
a_old MemAddr w -> MemAddr w -> Bool
forall a. Eq a => a -> a -> Bool
/= MemAddr w
b_old = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just AbsValue w tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV)
    | Int64
old Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Int64
new = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just (MemAddr w -> AbsValue w tp
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
a_old))
    | Bool
otherwise = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
-- Intervals
joinAbsValue' AbsValue w tp
v AbsValue w tp
v'
    | StridedInterval StridedInterval n
si_old <- AbsValue w tp
v, StridedInterval StridedInterval n
si_new <- AbsValue w tp
v'
    , StridedInterval n
si_new StridedInterval n -> StridedInterval n -> Bool
forall (w :: Natural).
StridedInterval w -> StridedInterval w -> Bool
`SI.isSubsetOf` StridedInterval n
StridedInterval n
si_old =
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
    | StridedInterval StridedInterval n
si_old <- AbsValue w tp
v, StridedInterval StridedInterval n
si_new <- AbsValue w tp
v' =
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
forall {n :: Natural} {w :: Natural}.
StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
go StridedInterval n
si_old StridedInterval n
StridedInterval n
si_new
    | StridedInterval StridedInterval n
si <- AbsValue w tp
v,  FinSet Set Integer
s <- AbsValue w tp
v' =
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
forall {n :: Natural} {w :: Natural}.
StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
go StridedInterval n
si (NatRepr n -> Set Integer -> StridedInterval n
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable (StridedInterval n -> NatRepr n
forall (w :: Natural). StridedInterval w -> NatRepr w
SI.typ StridedInterval n
si) Set Integer
s)
    | StridedInterval StridedInterval n
si <- AbsValue w tp
v,  CodePointers Set (MemSegmentOff w)
s Bool
b <- AbsValue w tp
v' = do
      Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords Set (MemSegmentOff w)
s
      let (Set Integer
wordSet, Set (MemSegmentOff w)
_) = Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
forall (w :: Natural).
MemWidth w =>
Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
partitionAbsoluteAddrs Set (MemSegmentOff w)
s Bool
b
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
forall {n :: Natural} {w :: Natural}.
StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
go StridedInterval n
si (NatRepr n -> Set Integer -> StridedInterval n
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable (StridedInterval n -> NatRepr n
forall (w :: Natural). StridedInterval w -> NatRepr w
SI.typ StridedInterval n
si) Set Integer
wordSet)
    | FinSet Set Integer
s <- AbsValue w tp
v, StridedInterval StridedInterval n
si <- AbsValue w tp
v' =
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
forall {n :: Natural} {w :: Natural}.
StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
go StridedInterval n
si (NatRepr n -> Set Integer -> StridedInterval n
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable (StridedInterval n -> NatRepr n
forall (w :: Natural). StridedInterval w -> NatRepr w
SI.typ StridedInterval n
si) Set Integer
s)
    | StridedInterval StridedInterval n
si <- AbsValue w tp
v', CodePointers Set (MemSegmentOff w)
s Bool
b <- AbsValue w tp
v = do
      Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords Set (MemSegmentOff w)
s
      let (Set Integer
wordSet, Set (MemSegmentOff w)
_) = Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
forall (w :: Natural).
MemWidth w =>
Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
partitionAbsoluteAddrs Set (MemSegmentOff w)
s Bool
b
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
forall {n :: Natural} {w :: Natural}.
StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
go StridedInterval n
si (NatRepr n -> Set Integer -> StridedInterval n
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable (StridedInterval n -> NatRepr n
forall (w :: Natural). StridedInterval w -> NatRepr w
SI.typ StridedInterval n
si) Set Integer
wordSet)
  where go :: StridedInterval n
-> StridedInterval n -> Maybe (AbsValue w (BVType n))
go StridedInterval n
si1 StridedInterval n
si2
           | StridedInterval n -> Integer
forall (tp :: Natural). StridedInterval tp -> Integer
SI.range StridedInterval n
si Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
10 = AbsValue w (BVType n) -> Maybe (AbsValue w (BVType n))
forall a. a -> Maybe a
Just AbsValue w (BVType n)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV -- Give up on stride
           | Bool
otherwise = AbsValue w (BVType n) -> Maybe (AbsValue w (BVType n))
forall a. a -> Maybe a
Just (AbsValue w (BVType n) -> Maybe (AbsValue w (BVType n)))
-> AbsValue w (BVType n) -> Maybe (AbsValue w (BVType n))
forall a b. (a -> b) -> a -> b
$ StridedInterval n -> AbsValue w (BVType n)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval StridedInterval n
si
          where si :: StridedInterval n
si = StridedInterval n -> StridedInterval n -> StridedInterval n
forall (w :: Natural).
StridedInterval w -> StridedInterval w -> StridedInterval w
SI.lub StridedInterval n
si1 StridedInterval n
si2

-- Sub values
joinAbsValue' (SubValue NatRepr n
n AbsValue w (BVType n)
av) (SubValue NatRepr n
n' AbsValue w (BVType n)
av') =
  case NatRepr n -> NatRepr n -> NatCases n n
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr n
n NatRepr n
n' of
    NatCaseLT LeqProof (n + 1) n
LeqProof -> (AbsValue w (BVType n) -> AbsValue w tp)
-> Maybe (AbsValue w (BVType n)) -> Maybe (AbsValue w tp)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
forall (n :: Natural) (n' :: Natural) (w :: Natural).
((n + 1) <= n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
subValue NatRepr n
n) (Maybe (AbsValue w (BVType n)) -> Maybe (AbsValue w tp))
-> StateT
     (Set (MemSegmentOff w)) Identity (Maybe (AbsValue w (BVType n)))
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsValue w (BVType n)
-> AbsValue w (BVType n)
-> StateT
     (Set (MemSegmentOff w)) Identity (Maybe (AbsValue w (BVType n)))
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp
-> AbsValue w tp
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
joinAbsValue' AbsValue w (BVType n)
av (AbsValue w (BVType n) -> NatRepr n -> AbsValue w (BVType n)
forall (w :: Natural) (v :: Natural) (u :: Natural).
(MemWidth w, (v + 1) <= u) =>
AbsValue w (BVType u) -> NatRepr v -> AbsValue w (BVType v)
trunc AbsValue w (BVType n)
av' NatRepr n
n)
    NatCases n n
NatCaseEQ          -> (AbsValue w (BVType n) -> AbsValue w tp)
-> Maybe (AbsValue w (BVType n)) -> Maybe (AbsValue w tp)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
forall (n :: Natural) (n' :: Natural) (w :: Natural).
((n + 1) <= n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
subValue NatRepr n
n) (Maybe (AbsValue w (BVType n)) -> Maybe (AbsValue w tp))
-> StateT
     (Set (MemSegmentOff w)) Identity (Maybe (AbsValue w (BVType n)))
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsValue w (BVType n)
-> AbsValue w (BVType n)
-> StateT
     (Set (MemSegmentOff w)) Identity (Maybe (AbsValue w (BVType n)))
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp
-> AbsValue w tp
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
joinAbsValue' AbsValue w (BVType n)
av AbsValue w (BVType n)
AbsValue w (BVType n)
av'
    NatCaseGT LeqProof (n + 1) n
LeqProof -> do
      let new_av :: AbsValue w (BVType n)
new_av = AbsValue w (BVType n) -> NatRepr n -> AbsValue w (BVType n)
forall (w :: Natural) (v :: Natural) (u :: Natural).
(MemWidth w, (v + 1) <= u) =>
AbsValue w (BVType u) -> NatRepr v -> AbsValue w (BVType v)
trunc AbsValue w (BVType n)
av NatRepr n
n'
      Maybe (AbsValue w (BVType n))
mv <- AbsValue w (BVType n)
-> AbsValue w (BVType n)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w (BVType n)))
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp
-> AbsValue w tp
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
joinAbsValue' AbsValue w (BVType n)
new_av AbsValue w (BVType n)
av'
      Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just (AbsValue w tp -> Maybe (AbsValue w tp))
-> AbsValue w tp -> Maybe (AbsValue w tp)
forall a b. (a -> b) -> a -> b
$! NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
forall (n :: Natural) (n' :: Natural) (w :: Natural).
((n + 1) <= n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
subValue NatRepr n
n' (AbsValue w (BVType n)
-> Maybe (AbsValue w (BVType n)) -> AbsValue w (BVType n)
forall a. a -> Maybe a -> a
fromMaybe AbsValue w (BVType n)
new_av Maybe (AbsValue w (BVType n))
mv)
-- Join addresses
joinAbsValue' (SomeStackOffset MemAddr w
ax) (StackOffsetAbsVal MemAddr w
ay Int64
_) | MemAddr w
ax MemAddr w -> MemAddr w -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr w
ay = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
joinAbsValue' (StackOffsetAbsVal MemAddr w
ax Int64
_) (SomeStackOffset MemAddr w
ay)
  | MemAddr w
ax MemAddr w -> MemAddr w -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr w
ay = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just (MemAddr w -> AbsValue w tp
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax)
joinAbsValue' (SomeStackOffset MemAddr w
ax) (SomeStackOffset MemAddr w
ay) | MemAddr w
ax MemAddr w -> MemAddr w -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr w
ay = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$ Maybe (AbsValue w tp)
forall a. Maybe a
Nothing


joinAbsValue' AbsValue w tp
ReturnAddr AbsValue w tp
ReturnAddr = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
joinAbsValue' (BoolConst Bool
b1) (BoolConst Bool
b2)
  | Bool
b1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b2  = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (AbsValue w tp)
forall a. Maybe a
Nothing
  | Bool
otherwise = Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$! AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just AbsValue w tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV

joinAbsValue' AbsValue w tp
x AbsValue w tp
y = do
  Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords (AbsValue w tp -> Set (MemSegmentOff w)
forall (w :: Natural) (tp :: Type).
AbsValue w tp -> Set (MemSegmentOff w)
codePointerSet AbsValue w tp
x)
  Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
forall (w :: Natural).
Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
addWords (AbsValue w tp -> Set (MemSegmentOff w)
forall (w :: Natural) (tp :: Type).
AbsValue w tp -> Set (MemSegmentOff w)
codePointerSet AbsValue w tp
y)
  Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a. a -> StateT (Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (AbsValue w tp)
 -> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp)))
-> Maybe (AbsValue w tp)
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall a b. (a -> b) -> a -> b
$! AbsValue w tp -> Maybe (AbsValue w tp)
forall a. a -> Maybe a
Just AbsValue w tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV

-------------------------------------------------------------------------------
-- Abstract value operations

-- | Return true if the integer value may be an a member of
mayBeMember :: Integer -> AbsValue w (BVType n) -> Bool
mayBeMember :: forall (w :: Natural) (n :: Natural).
Integer -> AbsValue w (BVType n) -> Bool
mayBeMember Integer
_ AbsValue w (BVType n)
TopV = Bool
True
mayBeMember Integer
n (FinSet Set Integer
s) = Integer -> Set Integer -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Integer
n Set Integer
s
mayBeMember Integer
0 (CodePointers Set (MemSegmentOff w)
_ Bool
b) = Bool
b
mayBeMember Integer
n (StridedInterval StridedInterval n
si) = Integer -> StridedInterval n -> Bool
forall (w :: Natural). Integer -> StridedInterval w -> Bool
SI.member Integer
n StridedInterval n
si
mayBeMember Integer
n (SubValue NatRepr n
n' AbsValue w (BVType n)
v) = Integer -> AbsValue w (BVType n) -> Bool
forall (w :: Natural) (n :: Natural).
Integer -> AbsValue w (BVType n) -> Bool
mayBeMember (Integer
n Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. NatRepr n -> Integer
forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr n
n') AbsValue w (BVType n)
v
mayBeMember Integer
_n AbsValue w (BVType n)
_v = Bool
True

-- | Returns true if this value represents the empty set.
isBottom :: AbsValue w tp -> Bool
isBottom :: forall (w :: Natural) (tp :: Type). AbsValue w tp -> Bool
isBottom BoolConst{}      = Bool
False
isBottom (FinSet Set Integer
v)       = Set Integer -> Bool
forall a. Set a -> Bool
Set.null Set Integer
v
isBottom (CodePointers Set (MemSegmentOff w)
v Bool
b) = Set (MemSegmentOff w) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff w)
v Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
b
isBottom (StackOffsetAbsVal MemAddr w
_ Int64
_) = Bool
False
isBottom (SomeStackOffset MemAddr w
_) = Bool
False
isBottom (StridedInterval StridedInterval n
v) = StridedInterval n -> Integer
forall (tp :: Natural). StridedInterval tp -> Integer
SI.size StridedInterval n
v Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
isBottom (SubValue NatRepr n
_ AbsValue w (BVType n)
v) = AbsValue w (BVType n) -> Bool
forall (w :: Natural) (tp :: Type). AbsValue w tp -> Bool
isBottom AbsValue w (BVType n)
v
isBottom AbsValue w tp
TopV = Bool
False
isBottom AbsValue w tp
ReturnAddr = Bool
False

-------------------------------------------------------------------------------
-- Intersection abstract values

-- meet is probably the wrong word here --- we are really refining the
-- abstract value based upon some new information.  Thus, we want to
-- return an overapproximation rather than an underapproximation of
-- the value.
-- Currently the only case we care about is where v' is an interval

-- @meet x y@ returns an over-approximation of the values in @x@ and @y@.
meet :: MemWidth w
     => AbsValue w tp
     -> AbsValue w tp
     -> AbsValue w tp
meet :: forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet AbsValue w tp
x AbsValue w tp
y
  | AbsValue w tp -> Bool
forall (w :: Natural) (tp :: Type). AbsValue w tp -> Bool
isBottom AbsValue w tp
m
  , Bool -> Bool
not (AbsValue w tp -> Bool
forall (w :: Natural) (tp :: Type). AbsValue w tp -> Bool
isBottom AbsValue w tp
x)
  , Bool -> Bool
not (AbsValue w tp -> Bool
forall (w :: Natural) (tp :: Type). AbsValue w tp -> Bool
isBottom AbsValue w tp
y) =
      DebugClass -> String -> AbsValue w tp -> AbsValue w tp
forall a. (?loc::CallStack) => DebugClass -> String -> a -> a
debug DebugClass
DAbsInt (String
"Got empty: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (AbsValue w tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. AbsValue w tp -> Doc ann
pretty AbsValue w tp
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (AbsValue w tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. AbsValue w tp -> Doc ann
pretty AbsValue w tp
y)) (AbsValue w tp -> AbsValue w tp) -> AbsValue w tp -> AbsValue w tp
forall a b. (a -> b) -> a -> b
$ AbsValue w tp
m
  | Bool
otherwise = AbsValue w tp
m
  where m :: AbsValue w tp
m = AbsValue w tp -> AbsValue w tp -> AbsValue w tp
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet' AbsValue w tp
x AbsValue w tp
y

meet' :: MemWidth w => AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet' :: forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet' AbsValue w tp
TopV AbsValue w tp
x = AbsValue w tp
x
meet' AbsValue w tp
x AbsValue w tp
TopV = AbsValue w tp
x
-- FIXME: reuse an old value if possible?
meet' (CodePointers Set (MemSegmentOff w)
old Bool
old_zero) (CodePointers Set (MemSegmentOff w)
new Bool
new_zero) =
  Set (MemSegmentOff w) -> Bool -> AbsValue w tp
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
Set (MemSegmentOff w) -> Bool -> AbsValue w tp
CodePointers (Set (MemSegmentOff w)
-> Set (MemSegmentOff w) -> Set (MemSegmentOff w)
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set (MemSegmentOff w)
old Set (MemSegmentOff w)
new) (Bool
old_zero Bool -> Bool -> Bool
&& Bool
new_zero)
--TODO: Fix below
meet' (String -> AbsValue w tp -> SomeFinSet tp
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"meet" -> IsFin Set Integer
old) (String -> AbsValue w tp -> SomeFinSet tp
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"meet" -> IsFin Set Integer
new) =
  Set Integer -> AbsValue w tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Set Integer -> AbsValue w tp) -> Set Integer -> AbsValue w tp
forall a b. (a -> b) -> a -> b
$ Set Integer -> Set Integer -> Set Integer
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Integer
old Set Integer
new
meet' (StackOffsetAbsVal MemAddr w
ax Int64
old) (StackOffsetAbsVal MemAddr w
ay Int64
new)
  | MemAddr w
ax MemAddr w -> MemAddr w -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr w
ay, Int64
old Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== Int64
new = MemAddr w -> Int64 -> AbsValue w tp
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> Int64 -> AbsValue w tp
StackOffsetAbsVal MemAddr w
ax Int64
old
  | Bool
otherwise = Set Integer -> AbsValue w tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet Set Integer
forall a. Set a
Set.empty

-- Intervals
meet' AbsValue w tp
v AbsValue w tp
v'
  | StridedInterval StridedInterval n
si_old <- AbsValue w tp
v, StridedInterval StridedInterval n
si_new <- AbsValue w tp
v'
    = StridedInterval n -> AbsValue w (BVType n)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval n -> AbsValue w (BVType n))
-> StridedInterval n -> AbsValue w (BVType n)
forall a b. (a -> b) -> a -> b
$ StridedInterval n
si_old StridedInterval n -> StridedInterval n -> StridedInterval n
forall (w :: Natural).
StridedInterval w -> StridedInterval w -> StridedInterval w
`SI.glb` StridedInterval n
StridedInterval n
si_new
  | StridedInterval StridedInterval n
si <- AbsValue w tp
v,  IsFin Set Integer
s <- String -> AbsValue w tp -> SomeFinSet tp
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"meet" AbsValue w tp
v'
    = Set Integer -> AbsValue w tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Set Integer -> AbsValue w tp) -> Set Integer -> AbsValue w tp
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> StridedInterval n -> Bool
forall (w :: Natural). Integer -> StridedInterval w -> Bool
`SI.member` StridedInterval n
si) Set Integer
s
  | StridedInterval StridedInterval n
si <- AbsValue w tp
v', IsFin Set Integer
s <- String -> AbsValue w tp -> SomeFinSet tp
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"meet" AbsValue w tp
v
    = Set Integer -> AbsValue w tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Set Integer -> AbsValue w tp) -> Set Integer -> AbsValue w tp
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Integer -> StridedInterval n -> Bool
forall (w :: Natural). Integer -> StridedInterval w -> Bool
`SI.member` StridedInterval n
si) Set Integer
s

-- These cases are currently sub-optimal: really we want to remove all
-- those from the larger set which don't have a prefix in the smaller
-- set.
meet' AbsValue w tp
v AbsValue w tp
v'
  | SubValue NatRepr n
n AbsValue w (BVType n)
av <- AbsValue w tp
v, SubValue NatRepr n
n' AbsValue w (BVType n)
av' <- AbsValue w tp
v' =
      case NatRepr n -> NatRepr n -> NatCases n n
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr n
n NatRepr n
n' of
        NatCaseLT LeqProof (n + 1) n
LeqProof -> NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
forall (n :: Natural) (n' :: Natural) (w :: Natural).
((n + 1) <= n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
subValue NatRepr n
n AbsValue w (BVType n)
av -- FIXME
        NatCases n n
NatCaseEQ          -> NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
forall (n :: Natural) (n' :: Natural) (w :: Natural).
((n + 1) <= n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
subValue NatRepr n
n (AbsValue w (BVType n)
-> AbsValue w (BVType n) -> AbsValue w (BVType n)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet AbsValue w (BVType n)
av AbsValue w (BVType n)
AbsValue w (BVType n)
av')
        NatCaseGT LeqProof (n + 1) n
LeqProof -> NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
forall (n :: Natural) (n' :: Natural) (w :: Natural).
((n + 1) <= n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType n')
subValue NatRepr n
n' AbsValue w (BVType n)
av' -- FIXME
  | SubValue NatRepr n
n AbsValue w (BVType n)
av <- AbsValue w tp
v, IsFin Set Integer
s <- String -> AbsValue w tp -> SomeFinSet tp
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"meet" AbsValue w tp
v' =
      Set Integer -> AbsValue w tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Set Integer -> AbsValue w tp) -> Set Integer -> AbsValue w tp
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Integer
x -> (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. NatRepr n -> Integer
forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer -> AbsValue w (BVType n) -> Bool
forall (w :: Natural) (n :: Natural).
Integer -> AbsValue w (BVType n) -> Bool
`mayBeMember` AbsValue w (BVType n)
av) Set Integer
s
  | SubValue NatRepr n
n AbsValue w (BVType n)
av <- AbsValue w tp
v', IsFin Set Integer
s <- String -> AbsValue w tp -> SomeFinSet tp
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"meet" AbsValue w tp
v =
      Set Integer -> AbsValue w tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Set Integer -> AbsValue w tp) -> Set Integer -> AbsValue w tp
forall a b. (a -> b) -> a -> b
$ (Integer -> Bool) -> Set Integer -> Set Integer
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Integer
x -> (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. NatRepr n -> Integer
forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr n
n) Integer -> AbsValue w (BVType n) -> Bool
forall (w :: Natural) (n :: Natural).
Integer -> AbsValue w (BVType n) -> Bool
`mayBeMember` AbsValue w (BVType n)
av) Set Integer
s
  | SubValue NatRepr n
_ AbsValue w (BVType n)
_ <- AbsValue w tp
v, StridedInterval StridedInterval n
_ <- AbsValue w tp
v' = AbsValue w tp
v' -- FIXME: ?
  | StridedInterval StridedInterval n
_ <- AbsValue w tp
v, SubValue NatRepr n
_ AbsValue w (BVType n)
_ <- AbsValue w tp
v' = AbsValue w tp
v -- FIXME: ?

-- Join addresses
meet' (SomeStackOffset MemAddr w
ax) s :: AbsValue w tp
s@(StackOffsetAbsVal MemAddr w
ay Int64
_) = Bool -> AbsValue w tp -> AbsValue w tp
forall a. HasCallStack => Bool -> a -> a
assert (MemAddr w
ax MemAddr w -> MemAddr w -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr w
ay) AbsValue w tp
s
meet' s :: AbsValue w tp
s@(StackOffsetAbsVal MemAddr w
ax Int64
_) (SomeStackOffset MemAddr w
ay) | MemAddr w
ax MemAddr w -> MemAddr w -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr w
ay = AbsValue w tp
s
meet' (SomeStackOffset MemAddr w
ax) (SomeStackOffset MemAddr w
ay) = Bool -> AbsValue w tp -> AbsValue w tp
forall a. HasCallStack => Bool -> a -> a
assert (MemAddr w
ax MemAddr w -> MemAddr w -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr w
ay) (AbsValue w tp -> AbsValue w tp) -> AbsValue w tp -> AbsValue w tp
forall a b. (a -> b) -> a -> b
$ MemAddr w -> AbsValue w tp
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
meet' AbsValue w tp
x AbsValue w tp
_ = AbsValue w tp
x -- Arbitrarily pick one.
-- meet x y = error $ "meet: impossible" ++ show (x,y)

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

-- | @trunc s w@ returns an abstract value @t@ such that foreach @v@ in
-- @s@, @trunc v w@ is in @t@.
trunc :: (MemWidth w, v+1 <= u)
      => AbsValue w (BVType u)
      -> NatRepr v
      -> AbsValue w (BVType v)
trunc :: forall (w :: Natural) (v :: Natural) (u :: Natural).
(MemWidth w, (v + 1) <= u) =>
AbsValue w (BVType u) -> NatRepr v -> AbsValue w (BVType v)
trunc (FinSet Set Integer
s) NatRepr v
w       = Set Integer -> AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ((Integer -> Integer) -> Set Integer -> Set Integer
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (NatRepr v -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr v
w) Set Integer
s)
trunc (CodePointers Set (MemSegmentOff w)
_ Bool
_) NatRepr v
_ = AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
trunc (StridedInterval StridedInterval n
s) NatRepr v
w = StridedInterval v -> AbsValue w (BVType v)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval n -> NatRepr v -> StridedInterval v
forall (u :: Natural) (v :: Natural).
StridedInterval u -> NatRepr v -> StridedInterval v
SI.trunc StridedInterval n
s NatRepr v
w)
trunc (SubValue NatRepr n
n AbsValue w (BVType n)
av) NatRepr v
w =
  case NatRepr n -> NatRepr v -> NatCases n v
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatCases m n
testNatCases NatRepr n
n NatRepr v
w of
   NatCaseLT LeqProof (n + 1) v
LeqProof -> NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type) (n :: Natural) (n' :: Natural).
((n + 1) <= n', tp ~ BVType n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w tp
SubValue NatRepr n
n AbsValue w (BVType n)
av
   NatCases n v
NatCaseEQ          -> AbsValue w (BVType v)
AbsValue w (BVType n)
av
   NatCaseGT LeqProof (v + 1) n
LeqProof -> AbsValue w (BVType n) -> NatRepr v -> AbsValue w (BVType v)
forall (w :: Natural) (v :: Natural) (u :: Natural).
(MemWidth w, (v + 1) <= u) =>
AbsValue w (BVType u) -> NatRepr v -> AbsValue w (BVType v)
trunc AbsValue w (BVType n)
av NatRepr v
w
trunc (StackOffsetAbsVal MemAddr w
_ Int64
_)   NatRepr v
_ = AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
trunc (SomeStackOffset MemAddr w
_) NatRepr v
_ = AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
trunc AbsValue w (BVType u)
ReturnAddr NatRepr v
_ = AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
trunc AbsValue w (BVType u)
TopV NatRepr v
_ = AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV

uext :: forall u v w
     .  (u+1 <= v, MemWidth w)
     => AbsValue w (BVType u) -> NatRepr v -> AbsValue w (BVType v)
uext :: forall (u :: Natural) (v :: Natural) (w :: Natural).
((u + 1) <= v, MemWidth w) =>
AbsValue w (BVType u) -> NatRepr v -> AbsValue w (BVType v)
uext (FinSet Set Integer
s) NatRepr v
_ = Set Integer -> AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet Set Integer
s
uext (CodePointers Set (MemSegmentOff w)
s Bool
b) NatRepr v
_ = Set Integer -> AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet Set Integer
wordSet
  where (Set Integer
wordSet, Set (MemSegmentOff w)
_) = Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
forall (w :: Natural).
MemWidth w =>
Set (MemSegmentOff w)
-> Bool -> (Set Integer, Set (MemSegmentOff w))
partitionAbsoluteAddrs Set (MemSegmentOff w)
s Bool
b
uext (StridedInterval StridedInterval n
si) NatRepr v
w =
  StridedInterval v -> AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
StridedInterval n -> AbsValue w tp
StridedInterval (StridedInterval v -> AbsValue w (BVType v))
-> StridedInterval v -> AbsValue w (BVType v)
forall a b. (a -> b) -> a -> b
$ StridedInterval n
si { SI.typ = w }
uext (SubValue (NatRepr n
n :: NatRepr n) AbsValue w (BVType n)
av) NatRepr v
_ =
  -- u + 1 <= v, n + 1 <= u, need n + 1 <= v
  -- proof: n + 1 <= u + 1 by addIsLeq
  --        u + 1 <= v     by assumption
  --        n + 1 <= v     by transitivity
  case LeqProof (n + 1) v
proof of
    LeqProof (n + 1) v
LeqProof -> NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type) (n :: Natural) (n' :: Natural).
((n + 1) <= n', tp ~ BVType n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w tp
SubValue NatRepr n
n AbsValue w (BVType n)
av
  where
    proof :: LeqProof (n + 1) v
    proof :: LeqProof (n + 1) v
proof = LeqProof (n + 1) (u + 1)
-> LeqProof (u + 1) v -> LeqProof (n + 1) v
forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (LeqProof (n + 1) u -> NatRepr 1 -> LeqProof (n + 1) (u + 1)
forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (LeqProof (n + 1) u
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof (n+1) u) NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat) (LeqProof (u + 1) v
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof (u + 1) v)
uext (StackOffsetAbsVal MemAddr w
_ Int64
_) NatRepr v
_ = AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
uext (SomeStackOffset MemAddr w
_) NatRepr v
_ = AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
uext AbsValue w (BVType u)
ReturnAddr NatRepr v
_ = AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
uext AbsValue w (BVType u)
TopV NatRepr v
_ = AbsValue w (BVType v)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV

asBoolConst :: AbsValue w BoolType -> Maybe Bool
asBoolConst :: forall (w :: Natural). AbsValue w BoolType -> Maybe Bool
asBoolConst (BoolConst Bool
b) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b
asBoolConst AbsValue w BoolType
TopV = Maybe Bool
forall a. Maybe a
Nothing

-- | Add an integer to the abstract value.
--
-- This is not exported and is only used to increment or decrement the stack
-- pointer by a known (by the architecture backend) signed integer after a call
-- returns. The integer is *not* a bitvector.
--
-- The 'Integer' needs to be in range of an 'Int64', but isn't changed to that
-- type currently to avoid some other code churn. In practice, this 'Integer' is
-- 0, 4, or 8.
bvinc :: forall w u
      .  NatRepr u
      -> AbsValue w (BVType u)
      -> Integer
      -- ^ An integer value to add to the previous argument.
      -> AbsValue w (BVType u)
bvinc :: forall (w :: Natural) (u :: Natural).
NatRepr u
-> AbsValue w (BVType u) -> Integer -> AbsValue w (BVType u)
bvinc NatRepr u
w (FinSet Set Integer
s) Integer
o =
  Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Set Integer -> AbsValue w (BVType u))
-> Set Integer -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer) -> Set Integer -> Set Integer
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (NatRepr u -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
o)) Set Integer
s
bvinc NatRepr u
_ (CodePointers Set (MemSegmentOff w)
_  Bool
_) Integer
_ =
  AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
bvinc NatRepr u
_w (StackOffsetAbsVal MemAddr w
a Int64
s) Integer
o =
  Bool -> AbsValue w (BVType u) -> AbsValue w (BVType u)
forall a. HasCallStack => Bool -> a -> a
assert (Integer
o Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger (Int64
forall a. Bounded a => a
maxBound :: Int64)) (AbsValue w (BVType u) -> AbsValue w (BVType u))
-> AbsValue w (BVType u) -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$
    MemAddr w -> Int64 -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> Int64 -> AbsValue w tp
StackOffsetAbsVal MemAddr w
a (Int64 -> Integer -> Int64
addSignedOffset Int64
s Integer
o)
bvinc NatRepr u
_ (SomeStackOffset MemAddr w
a) Integer
_ =
  MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
a
-- Strided intervals
bvinc NatRepr u
w (StridedInterval StridedInterval n
si) Integer
o =
  StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> StridedInterval u -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ NatRepr u
-> StridedInterval u -> StridedInterval u -> StridedInterval u
forall (u :: Natural).
NatRepr u
-> StridedInterval u -> StridedInterval u -> StridedInterval u
SI.bvadd NatRepr u
w StridedInterval u
StridedInterval n
si (NatRepr u -> Integer -> StridedInterval u
forall (w :: Natural). NatRepr w -> Integer -> StridedInterval w
SI.singleton NatRepr u
w Integer
o)
bvinc NatRepr u
_ (SubValue NatRepr n
w' AbsValue w (BVType n)
v) Integer
o =
  case NatRepr n
-> AbsValue w (BVType n) -> Integer -> AbsValue w (BVType n)
forall (w :: Natural) (u :: Natural).
NatRepr u
-> AbsValue w (BVType u) -> Integer -> AbsValue w (BVType u)
bvinc NatRepr n
w' AbsValue w (BVType n)
v Integer
o of
    AbsValue w (BVType n)
TopV -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
    AbsValue w (BVType n)
v' -> NatRepr n -> AbsValue w (BVType n) -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural) (n' :: Natural).
((n + 1) <= n', tp ~ BVType n') =>
NatRepr n -> AbsValue w (BVType n) -> AbsValue w tp
SubValue NatRepr n
w' AbsValue w (BVType n)
v'
bvinc NatRepr u
_ AbsValue w (BVType u)
TopV Integer
_ = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
bvinc NatRepr u
_ AbsValue w (BVType u)
ReturnAddr Integer
_ = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV

bvadc :: forall w u
      .  MemWidth w
      => NatRepr u
      -> AbsValue w (BVType u)
      -> AbsValue w (BVType u)
      -> AbsValue w BoolType
      -> AbsValue w (BVType u)
-- Stacks
bvadc :: forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w BoolType
-> AbsValue w (BVType u)
bvadc NatRepr u
w (StackOffsetAbsVal MemAddr w
a Int64
j) (FinSet Set Integer
t) AbsValue w BoolType
c
  | [Integer
o0] <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t
  , BoolConst Bool
b <- AbsValue w BoolType
c
  , Integer
o <- if Bool
b then Integer
o0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 else Integer
o0 =
    MemAddr w -> Int64 -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> Int64 -> AbsValue w tp
StackOffsetAbsVal MemAddr w
a (NatRepr u -> Int64 -> Integer -> Int64
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> Int64 -> Integer -> Int64
addSignedOffsetBV NatRepr u
w Int64
j Integer
o)
bvadc NatRepr u
w (FinSet Set Integer
t) (StackOffsetAbsVal MemAddr w
a Int64
j) AbsValue w BoolType
c
  | [Integer
o0] <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t
  , BoolConst Bool
b <- AbsValue w BoolType
c
  , Integer
o <- if Bool
b then Integer
o0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 else Integer
o0 =
    MemAddr w -> Int64 -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> Int64 -> AbsValue w tp
StackOffsetAbsVal MemAddr w
a (NatRepr u -> Int64 -> Integer -> Int64
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> Int64 -> Integer -> Int64
addSignedOffsetBV NatRepr u
w Int64
j Integer
o)
-- Two finite sets
bvadc NatRepr u
w (FinSet Set Integer
l) (FinSet Set Integer
r) (BoolConst Bool
b)
  | [Integer]
ls <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
l
  , [Integer]
rs <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
r
  = case [Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [NatRepr u -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
lvalInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
rvalInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+if Bool
b then Integer
1 else Integer
0 | Integer
lval <- [Integer]
ls, Integer
rval <- [Integer]
rs] of
      Set Integer
s | Set Integer -> Int
forall a. Set a -> Int
Set.size Set Integer
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
maxSetSize -> Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet Set Integer
s
      Set Integer
_ -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
-- Strided intervals
bvadc NatRepr u
w AbsValue w (BVType u)
v AbsValue w (BVType u)
v' AbsValue w BoolType
c
  | StridedInterval StridedInterval n
si1 <- AbsValue w (BVType u)
v, StridedInterval StridedInterval n
si2 <- AbsValue w (BVType u)
v' = StridedInterval u -> StridedInterval u -> AbsValue w (BVType u)
go StridedInterval u
StridedInterval n
si1 StridedInterval u
StridedInterval n
si2
  | StridedInterval StridedInterval n
si <- AbsValue w (BVType u)
v,  IsFin Set Integer
s <- String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvadc" AbsValue w (BVType u)
v' = StridedInterval u -> StridedInterval u -> AbsValue w (BVType u)
go StridedInterval u
StridedInterval n
si (NatRepr u -> Set Integer -> StridedInterval u
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable NatRepr u
w Set Integer
s)
  | StridedInterval StridedInterval n
si <- AbsValue w (BVType u)
v', IsFin Set Integer
s <- String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvadc" AbsValue w (BVType u)
v  = StridedInterval u -> StridedInterval u -> AbsValue w (BVType u)
go StridedInterval u
StridedInterval n
si (NatRepr u -> Set Integer -> StridedInterval u
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable NatRepr u
w Set Integer
s)
  where
    go :: SI.StridedInterval u -> SI.StridedInterval u -> AbsValue w (BVType u)
    go :: StridedInterval u -> StridedInterval u -> AbsValue w (BVType u)
go StridedInterval u
si1 StridedInterval u
si2 = StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> StridedInterval u -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ NatRepr u
-> StridedInterval u
-> StridedInterval u
-> Maybe Bool
-> StridedInterval u
forall (u :: Natural).
NatRepr u
-> StridedInterval u
-> StridedInterval u
-> Maybe Bool
-> StridedInterval u
SI.bvadc NatRepr u
w StridedInterval u
si1 StridedInterval u
si2 (AbsValue w BoolType -> Maybe Bool
forall (w :: Natural). AbsValue w BoolType -> Maybe Bool
asBoolConst AbsValue w BoolType
c)

-- the rest
bvadc NatRepr u
_ (StackOffsetAbsVal MemAddr w
ax Int64
_)   AbsValue w (BVType u)
_ AbsValue w BoolType
_ = MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvadc NatRepr u
_ AbsValue w (BVType u)
_   (StackOffsetAbsVal MemAddr w
ax Int64
_) AbsValue w BoolType
_ = MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvadc NatRepr u
_ (SomeStackOffset MemAddr w
ax) AbsValue w (BVType u)
_ AbsValue w BoolType
_ = MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvadc NatRepr u
_ AbsValue w (BVType u)
_ (SomeStackOffset MemAddr w
ax) AbsValue w BoolType
_ = MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvadc NatRepr u
_ AbsValue w (BVType u)
_ AbsValue w (BVType u)
_ AbsValue w BoolType
_ = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV

bvadd :: forall w u
      .  MemWidth w
      => NatRepr u
      -> AbsValue w (BVType u)
      -> AbsValue w (BVType u)
      -> AbsValue w (BVType u)
bvadd :: forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bvadd NatRepr u
w AbsValue w (BVType u)
x AbsValue w (BVType u)
y = NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w BoolType
-> AbsValue w (BVType u)
forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w BoolType
-> AbsValue w (BVType u)
bvadc NatRepr u
w AbsValue w (BVType u)
x AbsValue w (BVType u)
y (Bool -> AbsValue w BoolType
forall (w :: Natural) (tp :: Type).
(tp ~ BoolType) =>
Bool -> AbsValue w tp
BoolConst Bool
False)

setL :: Ord a
     => ([a] -> AbsValue w (BVType n))
     -> (Set a -> AbsValue w (BVType n))
     -> [a]
     -> AbsValue w (BVType n)
setL :: forall a (w :: Natural) (n :: Natural).
Ord a =>
([a] -> AbsValue w (BVType n))
-> (Set a -> AbsValue w (BVType n)) -> [a] -> AbsValue w (BVType n)
setL [a] -> AbsValue w (BVType n)
def Set a -> AbsValue w (BVType n)
c [a]
l | [a] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [a]
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxSetSize = [a] -> AbsValue w (BVType n)
def [a]
l
             | Bool
otherwise = Set a -> AbsValue w (BVType n)
c ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a]
l)

-- | Subtracting
bvsbb :: forall w u
      .  MemWidth w
      => Memory w
         -- ^ Memory used for checking code pointers.
      -> NatRepr u
      -> AbsValue w (BVType u)
      -> AbsValue w (BVType u)
      -> AbsValue w BoolType
      -> AbsValue w (BVType u)
bvsbb :: forall (w :: Natural) (u :: Natural).
MemWidth w =>
Memory w
-> NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w BoolType
-> AbsValue w (BVType u)
bvsbb Memory w
mem NatRepr u
w (CodePointers Set (MemSegmentOff w)
s Bool
b) (FinSet Set Integer
t) (BoolConst Bool
False)
      -- If we just have zero.
    | Set (MemSegmentOff w) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff w)
s Bool -> Bool -> Bool
&& Bool
b = Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ((Integer -> Integer) -> Set Integer -> Set Integer
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (NatRepr u -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
negate) Set Integer
t)
    | (Maybe (MemSegmentOff w) -> Bool)
-> [Maybe (MemSegmentOff w)] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all Maybe (MemSegmentOff w) -> Bool
forall a. Maybe a -> Bool
isJust [Maybe (MemSegmentOff w)]
vals Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
b Bool -> Bool -> Bool
|| Integer -> Set Integer
forall a. a -> Set a
Set.singleton Integer
0 Set Integer -> Set Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set Integer
t) =
      Set (MemSegmentOff w) -> Bool -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
Set (MemSegmentOff w) -> Bool -> AbsValue w tp
CodePointers ([MemSegmentOff w] -> Set (MemSegmentOff w)
forall a. Ord a => [a] -> Set a
Set.fromList ([Maybe (MemSegmentOff w)] -> [MemSegmentOff w]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (MemSegmentOff w)]
vals)) Bool
b
  where -- This list contains an entry for each pair of elements in s and t
        -- containing the address obtained by subtractin the offset in t
        -- from the address in s or `Nothing` if the result is not a valid
        -- segment offset.
        vals :: [Maybe (MemSegmentOff w)]
        vals :: [Maybe (MemSegmentOff w)]
vals = do
          MemSegmentOff w
x <- Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
s
          Integer
y <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t
          let z :: MemAddr w
z = MemSegmentOff w -> MemAddr w
forall (w :: Natural). MemSegmentOff w -> MemAddr w
segoffAddr MemSegmentOff w
x MemAddr w -> (MemAddr w -> MemAddr w) -> MemAddr w
forall a b. a -> (a -> b) -> b
& Integer -> MemAddr w -> MemAddr w
forall (w :: Natural).
MemWidth w =>
Integer -> MemAddr w -> MemAddr w
incAddr (Integer -> Integer
forall a. Num a => a -> a
negate Integer
y)
          case Memory w -> MemAddr w -> Maybe (MemSegmentOff w)
forall (w :: Natural).
Memory w -> MemAddr w -> Maybe (MemSegmentOff w)
asSegmentOff Memory w
mem MemAddr w
z of
            Just MemSegmentOff w
z_mseg | MemSegment w -> Flags
forall (w :: Natural). MemSegment w -> Flags
segmentFlags (MemSegmentOff w -> MemSegment w
forall (w :: Natural). MemSegmentOff w -> MemSegment w
segoffSegment MemSegmentOff w
z_mseg) Flags -> Flags -> Bool
`Perm.hasPerm` Flags
Perm.execute ->
              Maybe (MemSegmentOff w) -> [Maybe (MemSegmentOff w)]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MemSegmentOff w -> Maybe (MemSegmentOff w)
forall a. a -> Maybe a
Just MemSegmentOff w
z_mseg)
            Maybe (MemSegmentOff w)
_ ->
              Maybe (MemSegmentOff w) -> [Maybe (MemSegmentOff w)]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (MemSegmentOff w)
forall a. Maybe a
Nothing
bvsbb Memory w
_ NatRepr u
_ xv :: AbsValue w (BVType u)
xv@(CodePointers Set (MemSegmentOff w)
xs Bool
xb) (CodePointers Set (MemSegmentOff w)
ys Bool
yb) (BoolConst Bool
False)
      -- If we just have zero.
    | Set (MemSegmentOff w) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff w)
ys Bool -> Bool -> Bool
&& Bool
yb = AbsValue w (BVType u)
xv
      --
    | (Maybe Integer -> Bool) -> [Maybe Integer] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all Maybe Integer -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Integer]
vals Bool -> Bool -> Bool
&& Bool
xb Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
yb =
        if Bool
xb then
          Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Integer -> Set Integer -> Set Integer
forall a. Ord a => a -> Set a -> Set a
Set.insert Integer
0 ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList ([Maybe Integer] -> [Integer]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Integer]
vals)))
         else
          Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList ([Maybe Integer] -> [Integer]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Integer]
vals))
  where vals :: [Maybe Integer]
        vals :: [Maybe Integer]
vals = do
          MemSegmentOff w
x <- Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
xs
          MemSegmentOff w
y <- Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
ys
          Maybe Integer -> [Maybe Integer]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MemSegmentOff w -> MemAddr w
forall (w :: Natural). MemSegmentOff w -> MemAddr w
segoffAddr MemSegmentOff w
x MemAddr w -> MemAddr w -> Maybe Integer
forall (w :: Natural).
MemWidth w =>
MemAddr w -> MemAddr w -> Maybe Integer
`diffAddr` MemSegmentOff w -> MemAddr w
forall (w :: Natural). MemSegmentOff w -> MemAddr w
segoffAddr MemSegmentOff w
y)
bvsbb Memory w
_ NatRepr u
w (FinSet Set Integer
s) (String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvsub3" -> IsFin Set Integer
t) (BoolConst Bool
b) =
  ([Integer] -> AbsValue w (BVType u))
-> (Set Integer -> AbsValue w (BVType u))
-> [Integer]
-> AbsValue w (BVType u)
forall a (w :: Natural) (n :: Natural).
Ord a =>
([a] -> AbsValue w (BVType n))
-> (Set a -> AbsValue w (BVType n)) -> [a] -> AbsValue w (BVType n)
setL (StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> ([Integer] -> StridedInterval u)
-> [Integer]
-> AbsValue w (BVType u)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr u -> [Integer] -> StridedInterval u
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable NatRepr u
w) Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ([Integer] -> AbsValue w (BVType u))
-> [Integer] -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ do
  Integer
x <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
s
  Integer
y <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t
  Integer -> [Integer]
forall a. a -> [a]
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> [Integer]) -> Integer -> [Integer]
forall a b. (a -> b) -> a -> b
$ NatRepr u -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (if Bool
b then Integer
1 else Integer
0)
bvsbb Memory w
_ NatRepr u
w (StackOffsetAbsVal MemAddr w
ax Int64
x) (String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvsub6" -> IsFin Set Integer
t) (BoolConst Bool
False) =
  case Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t of
    [] -> Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet Set Integer
forall a. Set a
Set.empty
    [Integer
y] -> MemAddr w -> Int64 -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> Int64 -> AbsValue w tp
StackOffsetAbsVal MemAddr w
ax (NatRepr u -> Int64 -> Integer -> Int64
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> Int64 -> Integer -> Int64
addSignedOffsetBV NatRepr u
w Int64
x (Integer -> Integer
forall a. Num a => a -> a
negate (NatRepr u -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr u
w Integer
y)))
    [Integer]
_ -> MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvsbb Memory w
_ NatRepr u
_ (StackOffsetAbsVal MemAddr w
ax Int64
_) AbsValue w (BVType u)
_ AbsValue w BoolType
_ = MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvsbb Memory w
_ NatRepr u
_ AbsValue w (BVType u)
_ (StackOffsetAbsVal MemAddr w
_ Int64
_) AbsValue w BoolType
_ = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
bvsbb Memory w
_ NatRepr u
_ (SomeStackOffset MemAddr w
ax) AbsValue w (BVType u)
_ AbsValue w BoolType
_ = MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvsbb Memory w
_ NatRepr u
_ AbsValue w (BVType u)
_ (SomeStackOffset MemAddr w
_) AbsValue w BoolType
_ = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
bvsbb Memory w
_ NatRepr u
_ AbsValue w (BVType u)
_ AbsValue w (BVType u)
_ AbsValue w BoolType
_b = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV

-- | Subtracting
bvsub :: forall w u
      .  MemWidth w
      => Memory w
         -- ^ Memory used for checking code pointers.
      -> NatRepr u
      -> AbsValue w (BVType u)
      -> AbsValue w (BVType u)
      -> AbsValue w (BVType u)
bvsub :: forall (w :: Natural) (u :: Natural).
MemWidth w =>
Memory w
-> NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bvsub Memory w
mem NatRepr u
w (CodePointers Set (MemSegmentOff w)
s Bool
b) (FinSet Set Integer
t)
      -- If we just have zero.
    | Set (MemSegmentOff w) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff w)
s Bool -> Bool -> Bool
&& Bool
b = Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ((Integer -> Integer) -> Set Integer -> Set Integer
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (NatRepr u -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
negate) Set Integer
t)
    | (Maybe (MemSegmentOff w) -> Bool)
-> [Maybe (MemSegmentOff w)] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all Maybe (MemSegmentOff w) -> Bool
forall a. Maybe a -> Bool
isJust [Maybe (MemSegmentOff w)]
vals Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
b Bool -> Bool -> Bool
|| Integer -> Set Integer
forall a. a -> Set a
Set.singleton Integer
0 Set Integer -> Set Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set Integer
t) =
      Set (MemSegmentOff w) -> Bool -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
Set (MemSegmentOff w) -> Bool -> AbsValue w tp
CodePointers ([MemSegmentOff w] -> Set (MemSegmentOff w)
forall a. Ord a => [a] -> Set a
Set.fromList ([Maybe (MemSegmentOff w)] -> [MemSegmentOff w]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (MemSegmentOff w)]
vals)) Bool
b
    | Bool
otherwise = String -> AbsValue w (BVType u)
forall a. HasCallStack => String -> a
error String
"Losing code pointers due to bvsub."
  where vals :: [Maybe (MemSegmentOff w)]
        vals :: [Maybe (MemSegmentOff w)]
vals = do
          MemSegmentOff w
x <- Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
s
          Integer
y <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t
          let z :: MemAddr w
z = MemSegmentOff w -> MemAddr w
forall (w :: Natural). MemSegmentOff w -> MemAddr w
segoffAddr MemSegmentOff w
x MemAddr w -> (MemAddr w -> MemAddr w) -> MemAddr w
forall a b. a -> (a -> b) -> b
& Integer -> MemAddr w -> MemAddr w
forall (w :: Natural).
MemWidth w =>
Integer -> MemAddr w -> MemAddr w
incAddr (Integer -> Integer
forall a. Num a => a -> a
negate Integer
y)
          case Memory w -> MemAddr w -> Maybe (MemSegmentOff w)
forall (w :: Natural).
Memory w -> MemAddr w -> Maybe (MemSegmentOff w)
asSegmentOff Memory w
mem MemAddr w
z of
            Just MemSegmentOff w
z_mseg | MemSegment w -> Flags
forall (w :: Natural). MemSegment w -> Flags
segmentFlags (MemSegmentOff w -> MemSegment w
forall (w :: Natural). MemSegmentOff w -> MemSegment w
segoffSegment MemSegmentOff w
z_mseg) Flags -> Flags -> Bool
`Perm.hasPerm` Flags
Perm.execute ->
              Maybe (MemSegmentOff w) -> [Maybe (MemSegmentOff w)]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MemSegmentOff w -> Maybe (MemSegmentOff w)
forall a. a -> Maybe a
Just MemSegmentOff w
z_mseg)
            Maybe (MemSegmentOff w)
_ ->
              Maybe (MemSegmentOff w) -> [Maybe (MemSegmentOff w)]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (MemSegmentOff w)
forall a. Maybe a
Nothing
bvsub Memory w
_ NatRepr u
_ xv :: AbsValue w (BVType u)
xv@(CodePointers Set (MemSegmentOff w)
xs Bool
xb) (CodePointers Set (MemSegmentOff w)
ys Bool
yb)
      -- If we just have zero.
    | Set (MemSegmentOff w) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff w)
ys Bool -> Bool -> Bool
&& Bool
yb = AbsValue w (BVType u)
xv
      --
    | (Maybe Integer -> Bool) -> [Maybe Integer] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all Maybe Integer -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Integer]
vals Bool -> Bool -> Bool
&& Bool
xb Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
yb =
        if Bool
xb then
          Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Integer -> Set Integer -> Set Integer
forall a. Ord a => a -> Set a -> Set a
Set.insert Integer
0 ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList ([Maybe Integer] -> [Integer]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Integer]
vals)))
         else
          Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ([Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList ([Maybe Integer] -> [Integer]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Integer]
vals))
    | Bool
otherwise = String -> AbsValue w (BVType u)
forall a. HasCallStack => String -> a
error String
"Losing code pointers due to bvsub."
  where vals :: [Maybe Integer]
        vals :: [Maybe Integer]
vals = do
          MemSegmentOff w
x <- Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
xs
          MemSegmentOff w
y <- Set (MemSegmentOff w) -> [MemSegmentOff w]
forall a. Set a -> [a]
Set.toList Set (MemSegmentOff w)
ys
          Maybe Integer -> [Maybe Integer]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (MemSegmentOff w -> MemAddr w
forall (w :: Natural). MemSegmentOff w -> MemAddr w
segoffAddr MemSegmentOff w
x MemAddr w -> MemAddr w -> Maybe Integer
forall (w :: Natural).
MemWidth w =>
MemAddr w -> MemAddr w -> Maybe Integer
`diffAddr` MemSegmentOff w -> MemAddr w
forall (w :: Natural). MemSegmentOff w -> MemAddr w
segoffAddr MemSegmentOff w
y)
bvsub Memory w
_ NatRepr u
w (FinSet Set Integer
s) (String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvsub3" -> IsFin Set Integer
t) =
  ([Integer] -> AbsValue w (BVType u))
-> (Set Integer -> AbsValue w (BVType u))
-> [Integer]
-> AbsValue w (BVType u)
forall a (w :: Natural) (n :: Natural).
Ord a =>
([a] -> AbsValue w (BVType n))
-> (Set a -> AbsValue w (BVType n)) -> [a] -> AbsValue w (BVType n)
setL (StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> ([Integer] -> StridedInterval u)
-> [Integer]
-> AbsValue w (BVType u)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr u -> [Integer] -> StridedInterval u
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable NatRepr u
w) Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ([Integer] -> AbsValue w (BVType u))
-> [Integer] -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ do
  Integer
x <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
s
  Integer
y <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t
  Integer -> [Integer]
forall a. a -> [a]
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr u -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y))
bvsub Memory w
_ NatRepr u
w AbsValue w (BVType u)
v AbsValue w (BVType u)
v'
  | StridedInterval StridedInterval n
si1 <- AbsValue w (BVType u)
v, StridedInterval StridedInterval n
si2 <- AbsValue w (BVType u)
v' = StridedInterval n -> StridedInterval n -> AbsValue w (BVType u)
forall {p} {p} {w :: Natural} {tp :: Type}. p -> p -> AbsValue w tp
go StridedInterval n
si1 StridedInterval n
si2
  | StridedInterval StridedInterval n
si <- AbsValue w (BVType u)
v,  IsFin Set Integer
s <- String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvsub4" AbsValue w (BVType u)
v' = StridedInterval n -> StridedInterval u -> AbsValue w (BVType u)
forall {p} {p} {w :: Natural} {tp :: Type}. p -> p -> AbsValue w tp
go StridedInterval n
si (NatRepr u -> Set Integer -> StridedInterval u
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable NatRepr u
w Set Integer
s)
  | StridedInterval StridedInterval n
si <- AbsValue w (BVType u)
v', IsFin Set Integer
s <- String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvsub5" AbsValue w (BVType u)
v  = StridedInterval n -> StridedInterval u -> AbsValue w (BVType u)
forall {p} {p} {w :: Natural} {tp :: Type}. p -> p -> AbsValue w tp
go StridedInterval n
si (NatRepr u -> Set Integer -> StridedInterval u
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable NatRepr u
w Set Integer
s)
  where
    go :: p -> p -> AbsValue w tp
go p
_si1 p
_si2 = AbsValue w tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV -- FIXME
bvsub Memory w
_ NatRepr u
w (StackOffsetAbsVal MemAddr w
ax Int64
x) (String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvsub6" -> IsFin Set Integer
t) =
  case Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t of
    [] -> Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet Set Integer
forall a. Set a
Set.empty
    [Integer
y] -> MemAddr w -> Int64 -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> Int64 -> AbsValue w tp
StackOffsetAbsVal MemAddr w
ax (NatRepr u -> Int64 -> Integer -> Int64
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> Int64 -> Integer -> Int64
addSignedOffsetBV NatRepr u
w Int64
x (Integer -> Integer
forall a. Num a => a -> a
negate (NatRepr u -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr u
w Integer
y)))
    [Integer]
_ -> MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvsub Memory w
_ NatRepr u
_ (StackOffsetAbsVal MemAddr w
ax Int64
_) AbsValue w (BVType u)
_ = MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvsub Memory w
_ NatRepr u
_ AbsValue w (BVType u)
_ (StackOffsetAbsVal MemAddr w
_ Int64
_) = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
bvsub Memory w
_ NatRepr u
_ (SomeStackOffset MemAddr w
ax) AbsValue w (BVType u)
_ = MemAddr w -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> AbsValue w tp
SomeStackOffset MemAddr w
ax
bvsub Memory w
_ NatRepr u
_ AbsValue w (BVType u)
_ (SomeStackOffset MemAddr w
_) = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
bvsub Memory w
_ NatRepr u
_ AbsValue w (BVType u)
_ AbsValue w (BVType u)
_ = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV -- Keep the pattern checker happy

bvmul :: forall w u
      .  MemWidth w
      => NatRepr u
      -> AbsValue w (BVType u)
      -> AbsValue w (BVType u)
      -> AbsValue w (BVType u)
bvmul :: forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bvmul NatRepr u
w (String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvmul" -> IsFin Set Integer
s) (String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvmul" -> IsFin Set Integer
t) =
  ([Integer] -> AbsValue w (BVType u))
-> (Set Integer -> AbsValue w (BVType u))
-> [Integer]
-> AbsValue w (BVType u)
forall a (w :: Natural) (n :: Natural).
Ord a =>
([a] -> AbsValue w (BVType n))
-> (Set a -> AbsValue w (BVType n)) -> [a] -> AbsValue w (BVType n)
setL (StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> ([Integer] -> StridedInterval u)
-> [Integer]
-> AbsValue w (BVType u)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NatRepr u -> [Integer] -> StridedInterval u
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable NatRepr u
w) Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ([Integer] -> AbsValue w (BVType u))
-> [Integer] -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ do
  Integer
x <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
s
  Integer
y <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t
  Integer -> [Integer]
forall a. a -> [a]
forall (m :: Type -> Type) a. Monad m => a -> m a
return (NatRepr u -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr u
w (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y))
bvmul NatRepr u
w AbsValue w (BVType u)
v AbsValue w (BVType u)
v'
  | StridedInterval StridedInterval n
si1 <- AbsValue w (BVType u)
v, StridedInterval StridedInterval n
si2 <- AbsValue w (BVType u)
v' = StridedInterval u -> StridedInterval u -> AbsValue w (BVType u)
go StridedInterval u
StridedInterval n
si1 StridedInterval u
StridedInterval n
si2
  | StridedInterval StridedInterval n
si <- AbsValue w (BVType u)
v,  IsFin Set Integer
s <- String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvmul" AbsValue w (BVType u)
v' = StridedInterval u -> StridedInterval u -> AbsValue w (BVType u)
go StridedInterval u
StridedInterval n
si (NatRepr u -> Set Integer -> StridedInterval u
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable NatRepr u
w Set Integer
s)
  | StridedInterval StridedInterval n
si <- AbsValue w (BVType u)
v', IsFin Set Integer
s <- String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bvmul" AbsValue w (BVType u)
v  = StridedInterval u -> StridedInterval u -> AbsValue w (BVType u)
go StridedInterval u
StridedInterval n
si (NatRepr u -> Set Integer -> StridedInterval u
forall (t :: Type -> Type) (n :: Natural).
Foldable t =>
NatRepr n -> t Integer -> StridedInterval n
SI.fromFoldable NatRepr u
w Set Integer
s)
  where
    go :: SI.StridedInterval u -> SI.StridedInterval u -> AbsValue w (BVType u)
    go :: StridedInterval u -> StridedInterval u -> AbsValue w (BVType u)
go StridedInterval u
si1 StridedInterval u
si2 = StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> StridedInterval u -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ NatRepr u
-> StridedInterval u -> StridedInterval u -> StridedInterval u
forall (u :: Natural).
NatRepr u
-> StridedInterval u -> StridedInterval u -> StridedInterval u
SI.bvmul NatRepr u
w StridedInterval u
si1 StridedInterval u
si2

-- bvmul w (SubValue _n _av c) v' = bvmul w c v'
-- bvmul w v (SubValue _n _av c)  = bvmul w v c

bvmul NatRepr u
_ AbsValue w (BVType u)
_ AbsValue w (BVType u)
_ = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV

-- FIXME: generalise
bitop :: MemWidth w
      => (Integer -> Integer -> Integer)
      -> NatRepr u
      -> AbsValue w (BVType u)
      -> AbsValue w  (BVType u)
      -> AbsValue w (BVType u)
bitop :: forall (w :: Natural) (u :: Natural).
MemWidth w =>
(Integer -> Integer -> Integer)
-> NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bitop Integer -> Integer -> Integer
doOp NatRepr u
w (StackOffsetAbsVal MemAddr w
a Int64
j) (FinSet Set Integer
t)
  | [Integer
o] <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t
  = MemAddr w -> Int64 -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> Int64 -> AbsValue w tp
StackOffsetAbsVal MemAddr w
a (Int64 -> AbsValue w (BVType u)) -> Int64 -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ Integer -> Int64
forall a. Num a => Integer -> a
fromInteger (Integer -> Int64) -> Integer -> Int64
forall a b. (a -> b) -> a -> b
$ NatRepr u -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr u
w (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b c. (a -> b -> c) -> b -> a -> c
flip Integer -> Integer -> Integer
doOp Integer
o (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger Int64
j
bitop Integer -> Integer -> Integer
doOp NatRepr u
w (FinSet Set Integer
t) (StackOffsetAbsVal MemAddr w
a Int64
j)
  | [Integer
o] <- Set Integer -> [Integer]
forall a. Set a -> [a]
Set.toList Set Integer
t
  = MemAddr w -> Int64 -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> Int64 -> AbsValue w tp
StackOffsetAbsVal MemAddr w
a (Int64 -> AbsValue w (BVType u)) -> Int64 -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ Integer -> Int64
forall a. Num a => Integer -> a
fromInteger (Integer -> Int64) -> Integer -> Int64
forall a b. (a -> b) -> a -> b
$ NatRepr u -> Integer -> Integer
forall (w :: Natural). (1 <= w) => NatRepr w -> Integer -> Integer
toSigned NatRepr u
w (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
doOp Integer
o (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Int64 -> Integer
forall a. Integral a => a -> Integer
toInteger Int64
j
bitop Integer -> Integer -> Integer
doOp NatRepr u
_w (String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bitop" -> IsFin Set Integer
s) (AbsValue w (BVType u) -> Maybe Integer
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> Maybe Integer
asConcreteSingleton -> Just Integer
v)
  = Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ((Integer -> Integer) -> Set Integer -> Set Integer
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b c. (a -> b -> c) -> b -> a -> c
flip Integer -> Integer -> Integer
doOp Integer
v) Set Integer
s)
bitop Integer -> Integer -> Integer
doOp NatRepr u
_w (AbsValue w (BVType u) -> Maybe Integer
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> Maybe Integer
asConcreteSingleton -> Just Integer
v) (String -> AbsValue w (BVType u) -> SomeFinSet (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
String -> AbsValue w tp -> SomeFinSet tp
asFinSet String
"bitop" -> IsFin Set Integer
s)
  = Set Integer -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet ((Integer -> Integer) -> Set Integer -> Set Integer
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Integer -> Integer -> Integer
doOp Integer
v) Set Integer
s)
bitop Integer -> Integer -> Integer
_ NatRepr u
_ AbsValue w (BVType u)
_ AbsValue w (BVType u)
_ = AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV

ppAbsValue :: MemWidth w => AbsValue w tp -> Maybe (Doc ann)
ppAbsValue :: forall (w :: Natural) (tp :: Type) ann.
MemWidth w =>
AbsValue w tp -> Maybe (Doc ann)
ppAbsValue AbsValue w tp
TopV = Maybe (Doc ann)
forall a. Maybe a
Nothing
ppAbsValue AbsValue w tp
v = Doc ann -> Maybe (Doc ann)
forall a. a -> Maybe a
Just (AbsValue w tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. AbsValue w tp -> Doc ann
pretty AbsValue w tp
v)

-- | Print a list of Docs vertically separated.
instance (MemWidth w, ShowF r) => PrettyRegValue r (AbsValue w) where
  ppValueEq :: forall (tp :: Type) ann. r tp -> AbsValue w tp -> Maybe (Doc ann)
ppValueEq r tp
_ AbsValue w tp
TopV = Maybe (Doc ann)
forall a. Maybe a
Nothing
  ppValueEq r tp
r AbsValue w tp
v = Doc ann -> Maybe (Doc ann)
forall a. a -> Maybe a
Just (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) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> AbsValue w tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. AbsValue w tp -> Doc ann
pretty AbsValue w tp
v)


absTrue :: AbsValue w BoolType
absTrue :: forall (w :: Natural). AbsValue w BoolType
absTrue = Bool -> AbsValue w BoolType
forall (w :: Natural) (tp :: Type).
(tp ~ BoolType) =>
Bool -> AbsValue w tp
BoolConst Bool
True

absFalse :: AbsValue w BoolType
absFalse :: forall (w :: Natural). AbsValue w BoolType
absFalse = Bool -> AbsValue w BoolType
forall (w :: Natural) (tp :: Type).
(tp ~ BoolType) =>
Bool -> AbsValue w tp
BoolConst Bool
False

-- | This returns the smallest abstract value that contains the
-- given unsigned integer.
abstractSingleton :: MemWidth w
                  => Memory w
                     -- ^ Width of code pointer
                  -> NatRepr n
                  -> Integer
                  -> AbsValue w (BVType n)
abstractSingleton :: forall (w :: Natural) (n :: Natural).
MemWidth w =>
Memory w -> NatRepr n -> Integer -> AbsValue w (BVType n)
abstractSingleton Memory w
mem NatRepr n
w Integer
i
  | Just n :~: w
Refl <- NatRepr n -> NatRepr w -> Maybe (n :~: 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 n
w (Memory w -> NatRepr w
forall (w :: Natural). Memory w -> NatRepr w
memWidth Memory w
mem)
  , Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr n -> Integer
forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr n
w
  , Just MemSegmentOff w
sa <- Memory w -> MemWord w -> Maybe (MemSegmentOff w)
forall (w :: Natural).
Memory w -> MemWord w -> Maybe (MemSegmentOff w)
resolveAbsoluteAddr Memory w
mem (Integer -> MemWord w
forall a. Num a => Integer -> a
fromInteger Integer
i)
  , MemSegment w -> Flags
forall (w :: Natural). MemSegment w -> Flags
segmentFlags (MemSegmentOff w -> MemSegment w
forall (w :: Natural). MemSegmentOff w -> MemSegment w
segoffSegment MemSegmentOff w
sa) Flags -> Flags -> Bool
`Perm.hasPerm` Flags
Perm.execute =
    MemSegmentOff w -> AbsValue w (BVType w)
forall (w :: Natural). MemSegmentOff w -> AbsValue w (BVType w)
concreteCodeAddr MemSegmentOff w
sa
  | Bool
otherwise =
      Set Integer -> AbsValue w (BVType n)
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Integer -> Set Integer
forall a. a -> Set a
Set.singleton (NatRepr n -> Integer -> Integer
forall (w :: Natural). NatRepr w -> Integer -> Integer
toUnsigned NatRepr n
w Integer
i))

-- | Create a concrete stack offset.
concreteStackOffset :: MemAddr w -> Integer -> AbsValue w (BVType w)
concreteStackOffset :: forall (w :: Natural).
MemAddr w -> Integer -> AbsValue w (BVType w)
concreteStackOffset MemAddr w
a Integer
o = MemAddr w -> Int64 -> AbsValue w (BVType w)
forall (w :: Natural) (tp :: Type).
(tp ~ BVType w) =>
MemAddr w -> Int64 -> AbsValue w tp
StackOffsetAbsVal MemAddr w
a (Integer -> Int64
forall a. Num a => Integer -> a
fromInteger Integer
o)

------------------------------------------------------------------------
-- Restrictions

hasMaximum :: NatRepr w -> AbsValue p (BVType w) -> Maybe Integer
hasMaximum :: forall (w :: Natural) (p :: Natural).
NatRepr w -> AbsValue p (BVType w) -> Maybe Integer
hasMaximum NatRepr w
n AbsValue p (BVType w)
v =
  case AbsValue p (BVType w)
v of
    FinSet Set Integer
s | Set Integer -> Bool
forall a. Set a -> Bool
Set.null Set Integer
s -> Maybe Integer
forall a. Maybe a
Nothing
             | Bool
otherwise  -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$! Set Integer -> Integer
forall a. Set a -> a
Set.findMax Set Integer
s
    CodePointers Set (MemSegmentOff p)
s Bool
b | Set (MemSegmentOff p) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff p)
s -> if Bool
b then Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0 else Maybe Integer
forall a. Maybe a
Nothing
                     | Bool
otherwise  -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Integer
forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr w
n
    StridedInterval StridedInterval n
si -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (StridedInterval n -> Integer
forall (tp :: Natural). StridedInterval tp -> Integer
SI.intervalEnd StridedInterval n
si)
    AbsValue p (BVType w)
TopV               -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ NatRepr w -> Integer
forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr w
n
    AbsValue p (BVType w)
_                  -> Maybe Integer
forall a. Maybe a
Nothing


hasMinimum :: NatRepr w -> AbsValue p (BVType w) -> Maybe Integer
hasMinimum :: forall (w :: Natural) (p :: Natural).
NatRepr w -> AbsValue p (BVType w) -> Maybe Integer
hasMinimum NatRepr w
_tp AbsValue p (BVType w)
v =
  case AbsValue p (BVType w)
v of
   FinSet Set Integer
s       | Set Integer -> Bool
forall a. Set a -> Bool
Set.null Set Integer
s -> Maybe Integer
forall a. Maybe a
Nothing
                  | Bool
otherwise  -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$! Set Integer -> Integer
forall a. Set a -> a
Set.findMin Set Integer
s
   CodePointers Set (MemSegmentOff p)
s Bool
b | Set (MemSegmentOff p) -> Bool
forall a. Set a -> Bool
Set.null Set (MemSegmentOff p)
s -> if Bool
b then Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0 else Maybe Integer
forall a. Maybe a
Nothing
   StridedInterval StridedInterval n
si -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$! StridedInterval n -> Integer
forall (tp :: Natural). StridedInterval tp -> Integer
SI.base StridedInterval n
si
   AbsValue p (BVType w)
_                  -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0

-- | @abstractULt x y@ refines x and y with the knowledge that @x < y@
-- is unsigned.
-- For example, given {2, 3} and {2, 3, 4}, we know (only) that
-- {2, 3} and {3, 4} because we may pick any element from either set.

abstractULt :: MemWidth w
            => NatRepr u
            -> AbsValue w (BVType u)
            -> AbsValue w (BVType u)
            -> (AbsValue w (BVType u), AbsValue w (BVType u))
abstractULt :: forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> (AbsValue w (BVType u), AbsValue w (BVType u))
abstractULt NatRepr u
_n AbsValue w (BVType u)
TopV AbsValue w (BVType u)
TopV = (AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV, AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV)
abstractULt NatRepr u
n AbsValue w (BVType u)
x AbsValue w (BVType u)
y
  | Just Integer
u_y <- NatRepr u -> AbsValue w (BVType u) -> Maybe Integer
forall (w :: Natural) (p :: Natural).
NatRepr w -> AbsValue p (BVType w) -> Maybe Integer
hasMaximum NatRepr u
n AbsValue w (BVType u)
y
  , Just Integer
l_x <- NatRepr u -> AbsValue w (BVType u) -> Maybe Integer
forall (w :: Natural) (p :: Natural).
NatRepr w -> AbsValue p (BVType w) -> Maybe Integer
hasMinimum NatRepr u
n AbsValue w (BVType u)
x =
    -- debug DAbsInt' ("abstractLt " ++ show (pretty x) ++ " " ++ show (pretty y) ++ " -> ")
    ( AbsValue w (BVType u)
-> AbsValue w (BVType u) -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet AbsValue w (BVType u)
x (StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> StridedInterval u -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ NatRepr u
-> Bool -> Integer -> Integer -> Integer -> StridedInterval u
forall (w :: Natural).
NatRepr w
-> Bool -> Integer -> Integer -> Integer -> StridedInterval w
SI.mkStridedInterval NatRepr u
n Bool
False Integer
0 (Integer
u_y Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer
1)
    , AbsValue w (BVType u)
-> AbsValue w (BVType u) -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet AbsValue w (BVType u)
y (StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> StridedInterval u -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ NatRepr u
-> Bool -> Integer -> Integer -> Integer -> StridedInterval u
forall (w :: Natural).
NatRepr w
-> Bool -> Integer -> Integer -> Integer -> StridedInterval w
SI.mkStridedInterval NatRepr u
n Bool
False (Integer
l_x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (NatRepr u -> Integer
forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr u
n) Integer
1))

abstractULt NatRepr u
_tp AbsValue w (BVType u)
x AbsValue w (BVType u)
y = (AbsValue w (BVType u)
x, AbsValue w (BVType u)
y)

-- | @abstractULeq u v@ returns a pair @(u',v')@ where for each @x@ in
-- @u@, and @y@ in @v@, such that @x <= y@, we have that @x \in u'@ and
-- @y@ in v'.
abstractULeq :: MemWidth w
             => NatRepr u
             -> AbsValue w (BVType u)
             -> AbsValue w (BVType u)
             -> (AbsValue w (BVType u), AbsValue w (BVType u))
abstractULeq :: forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> (AbsValue w (BVType u), AbsValue w (BVType u))
abstractULeq NatRepr u
_n AbsValue w (BVType u)
TopV AbsValue w (BVType u)
TopV = (AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV, AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV)
abstractULeq NatRepr u
n AbsValue w (BVType u)
x AbsValue w (BVType u)
y
  | Just Integer
u_y <- NatRepr u -> AbsValue w (BVType u) -> Maybe Integer
forall (w :: Natural) (p :: Natural).
NatRepr w -> AbsValue p (BVType w) -> Maybe Integer
hasMaximum NatRepr u
n AbsValue w (BVType u)
y
  , Just Integer
l_x <- NatRepr u -> AbsValue w (BVType u) -> Maybe Integer
forall (w :: Natural) (p :: Natural).
NatRepr w -> AbsValue p (BVType w) -> Maybe Integer
hasMinimum NatRepr u
n AbsValue w (BVType u)
x =
    ( AbsValue w (BVType u)
-> AbsValue w (BVType u) -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet AbsValue w (BVType u)
x (StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> StridedInterval u -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ NatRepr u
-> Bool -> Integer -> Integer -> Integer -> StridedInterval u
forall (w :: Natural).
NatRepr w
-> Bool -> Integer -> Integer -> Integer -> StridedInterval w
SI.mkStridedInterval NatRepr u
n Bool
False Integer
0   Integer
u_y Integer
1)
    , AbsValue w (BVType u)
-> AbsValue w (BVType u) -> AbsValue w (BVType u)
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp -> AbsValue w tp -> AbsValue w tp
meet AbsValue w (BVType u)
y (StridedInterval u -> AbsValue w (BVType u)
forall (n :: Natural) (w :: Natural).
StridedInterval n -> AbsValue w (BVType n)
stridedInterval (StridedInterval u -> AbsValue w (BVType u))
-> StridedInterval u -> AbsValue w (BVType u)
forall a b. (a -> b) -> a -> b
$ NatRepr u
-> Bool -> Integer -> Integer -> Integer -> StridedInterval u
forall (w :: Natural).
NatRepr w
-> Bool -> Integer -> Integer -> Integer -> StridedInterval w
SI.mkStridedInterval NatRepr u
n Bool
False Integer
l_x (NatRepr u -> Integer
forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr u
n) Integer
1))

abstractULeq NatRepr u
_tp AbsValue w (BVType u)
x AbsValue w (BVType u)
y = (AbsValue w (BVType u)
x, AbsValue w (BVType u)
y)

------------------------------------------------------------------------
-- AbsBlockStack

data StackEntry w
   = forall tp . StackEntry !(MemRepr tp) !(AbsValue w tp)

instance Eq (StackEntry w) where
  StackEntry MemRepr tp
x_tp AbsValue w tp
x_v == :: StackEntry w -> StackEntry w -> Bool
== StackEntry MemRepr tp
y_tp AbsValue w tp
y_v
    | 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
x_tp MemRepr tp
y_tp = AbsValue w tp
x_v AbsValue w tp -> AbsValue w tp -> Bool
forall a. Eq a => a -> a -> Bool
== AbsValue w tp
AbsValue w tp
y_v
    | Bool
otherwise = Bool
False

deriving instance MemWidth w => Show (StackEntry w)

-- | The AbsBlockStack describes offsets of the stack.
-- Values that are not in the map may denote any values.
--
-- The stack grows down, so negative keys are in the stack frame.
type AbsBlockStack w = Map Int64 (StackEntry w)

-- absStackLeq :: AbsBlockStack -> AbsBlockStack -> Bool
-- absStackLeq x y = all entryLeq (Map.toList y)
--   where entryLeq (o, StackEntry y_tp y_v) =
--           case Map.lookup o x of
--             Just (StackEntry x_tp x_v) | Just Refl <- testEquality x_tp y_tp ->
--               isNothing (joinAbsValue y_v x_v)
--             _ -> False

-- | @absStackJoinD y x@ returns the stack containing the union @z@ of the
-- values in @y@ and @x@.  It sets the first state parameter to true if @z@
-- is different from @y@ and adds and escaped code pointers to the second
-- parameter.
absStackJoinD :: MemWidth w
              => AbsBlockStack w
              -> AbsBlockStack w
              -> State (Bool,Set (MemSegmentOff w)) (AbsBlockStack w)
absStackJoinD :: forall (w :: Natural).
MemWidth w =>
AbsBlockStack w
-> AbsBlockStack w
-> State (Bool, Set (MemSegmentOff w)) (AbsBlockStack w)
absStackJoinD AbsBlockStack w
y AbsBlockStack w
x = do
  -- This attempts to merge information from the new state into the old state.
  let entryLeq :: (Int64, StackEntry w)
-> StateT
     (Bool, Set (MemSegmentOff w))
     Identity
     (Maybe (Int64, StackEntry w))
entryLeq (Int64
o, StackEntry MemRepr tp
y_tp AbsValue w tp
y_v) =
        case Int64 -> AbsBlockStack w -> Maybe (StackEntry w)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int64
o AbsBlockStack w
x of
          -- The new state contains a valuewith the same type.
          Just (StackEntry MemRepr tp
x_tp AbsValue w tp
x_v) | 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
x_tp MemRepr tp
y_tp -> do
            Set (MemSegmentOff w)
s <- Getting
  (Set (MemSegmentOff w))
  (Bool, Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
-> StateT
     (Bool, Set (MemSegmentOff w)) Identity (Set (MemSegmentOff w))
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (Set (MemSegmentOff w))
  (Bool, Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (Bool, Set (MemSegmentOff w))
  (Bool, Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
_2
            -- Attempt to merge values
            case State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
-> Set (MemSegmentOff w)
-> (Maybe (AbsValue w tp), Set (MemSegmentOff w))
forall s a. State s a -> s -> (a, s)
runState (AbsValue w tp
-> AbsValue w tp
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp
-> AbsValue w tp
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
joinAbsValue' AbsValue w tp
y_v AbsValue w tp
AbsValue w tp
x_v) Set (MemSegmentOff w)
s of
              -- If merging returns the value y_v, then keep it.
              (Maybe (AbsValue w tp)
Nothing,  Set (MemSegmentOff w)
s') -> do
                (Set (MemSegmentOff w) -> Identity (Set (MemSegmentOff w)))
-> (Bool, Set (MemSegmentOff w))
-> Identity (Bool, Set (MemSegmentOff w))
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (Bool, Set (MemSegmentOff w))
  (Bool, Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
_2 ((Set (MemSegmentOff w) -> Identity (Set (MemSegmentOff w)))
 -> (Bool, Set (MemSegmentOff w))
 -> Identity (Bool, Set (MemSegmentOff w)))
-> Set (MemSegmentOff w)
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set (MemSegmentOff w)
s'
                Maybe (Int64, StackEntry w)
-> StateT
     (Bool, Set (MemSegmentOff w))
     Identity
     (Maybe (Int64, StackEntry w))
forall a. a -> StateT (Bool, Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (Int64, StackEntry w)
 -> StateT
      (Bool, Set (MemSegmentOff w))
      Identity
      (Maybe (Int64, StackEntry w)))
-> Maybe (Int64, StackEntry w)
-> StateT
     (Bool, Set (MemSegmentOff w))
     Identity
     (Maybe (Int64, StackEntry w))
forall a b. (a -> b) -> a -> b
$ (Int64, StackEntry w) -> Maybe (Int64, StackEntry w)
forall a. a -> Maybe a
Just (Int64
o, MemRepr tp -> AbsValue w tp -> StackEntry w
forall (w :: Natural) (tp :: Type).
MemRepr tp -> AbsValue w tp -> StackEntry w
StackEntry MemRepr tp
y_tp AbsValue w tp
y_v)
              -- Otherwise merging returned a new value.
              (Just AbsValue w tp
z_v, Set (MemSegmentOff w)
s') -> do
                case AbsValue w tp
y_v of
                  AbsValue w tp
ReturnAddr -> DebugClass
-> String
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall a. (?loc::CallStack) => DebugClass -> String -> a -> a
debug DebugClass
DAbsInt (String
"absStackJoinD dropping return value:\n"
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Old state: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (AbsBlockStack w -> Doc Any
forall (w :: Natural) ann. MemWidth w => AbsBlockStack w -> Doc ann
ppAbsStack AbsBlockStack w
y)
                                    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"New state: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (AbsBlockStack w -> Doc Any
forall (w :: Natural) ann. MemWidth w => AbsBlockStack w -> Doc ann
ppAbsStack AbsBlockStack w
x)) (StateT (Bool, Set (MemSegmentOff w)) Identity ()
 -> StateT (Bool, Set (MemSegmentOff w)) Identity ())
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall a b. (a -> b) -> a -> b
$
                    () -> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall a. a -> StateT (Bool, Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
                  AbsValue w tp
_ -> () -> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall a. a -> StateT (Bool, Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
                (Bool -> Identity Bool)
-> (Bool, Set (MemSegmentOff w))
-> Identity (Bool, Set (MemSegmentOff w))
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Bool, Set (MemSegmentOff w))
  (Bool, Set (MemSegmentOff w))
  Bool
  Bool
_1 ((Bool -> Identity Bool)
 -> (Bool, Set (MemSegmentOff w))
 -> Identity (Bool, Set (MemSegmentOff w)))
-> Bool -> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Bool
True
                (Set (MemSegmentOff w) -> Identity (Set (MemSegmentOff w)))
-> (Bool, Set (MemSegmentOff w))
-> Identity (Bool, Set (MemSegmentOff w))
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (Bool, Set (MemSegmentOff w))
  (Bool, Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
_2 ((Set (MemSegmentOff w) -> Identity (Set (MemSegmentOff w)))
 -> (Bool, Set (MemSegmentOff w))
 -> Identity (Bool, Set (MemSegmentOff w)))
-> Set (MemSegmentOff w)
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set (MemSegmentOff w)
s'
                Maybe (Int64, StackEntry w)
-> StateT
     (Bool, Set (MemSegmentOff w))
     Identity
     (Maybe (Int64, StackEntry w))
forall a. a -> StateT (Bool, Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (Int64, StackEntry w)
 -> StateT
      (Bool, Set (MemSegmentOff w))
      Identity
      (Maybe (Int64, StackEntry w)))
-> Maybe (Int64, StackEntry w)
-> StateT
     (Bool, Set (MemSegmentOff w))
     Identity
     (Maybe (Int64, StackEntry w))
forall a b. (a -> b) -> a -> b
$ (Int64, StackEntry w) -> Maybe (Int64, StackEntry w)
forall a. a -> Maybe a
Just (Int64
o, MemRepr tp -> AbsValue w tp -> StackEntry w
forall (w :: Natural) (tp :: Type).
MemRepr tp -> AbsValue w tp -> StackEntry w
StackEntry MemRepr tp
y_tp AbsValue w tp
z_v)
          Maybe (StackEntry w)
_ -> do
            case AbsValue w tp
y_v of
              AbsValue w tp
ReturnAddr ->
                DebugClass
-> String
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall a. (?loc::CallStack) => DebugClass -> String -> a -> a
debug DebugClass
DAbsInt (String
"absStackJoinD dropping return value:"
                               String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nOld state: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (AbsBlockStack w -> Doc Any
forall (w :: Natural) ann. MemWidth w => AbsBlockStack w -> Doc ann
ppAbsStack AbsBlockStack w
y)
                               String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nNew state: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (AbsBlockStack w -> Doc Any
forall (w :: Natural) ann. MemWidth w => AbsBlockStack w -> Doc ann
ppAbsStack AbsBlockStack w
x)) (StateT (Bool, Set (MemSegmentOff w)) Identity ()
 -> StateT (Bool, Set (MemSegmentOff w)) Identity ())
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall a b. (a -> b) -> a -> b
$
                () -> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall a. a -> StateT (Bool, Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
              AbsValue w tp
_ -> () -> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall a. a -> StateT (Bool, Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
            (Bool -> Identity Bool)
-> (Bool, Set (MemSegmentOff w))
-> Identity (Bool, Set (MemSegmentOff w))
forall s t a b. Field1 s t a b => Lens s t a b
Lens
  (Bool, Set (MemSegmentOff w))
  (Bool, Set (MemSegmentOff w))
  Bool
  Bool
_1 ((Bool -> Identity Bool)
 -> (Bool, Set (MemSegmentOff w))
 -> Identity (Bool, Set (MemSegmentOff w)))
-> Bool -> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Bool
True
            (Set (MemSegmentOff w) -> Identity (Set (MemSegmentOff w)))
-> (Bool, Set (MemSegmentOff w))
-> Identity (Bool, Set (MemSegmentOff w))
forall s t a b. Field2 s t a b => Lens s t a b
Lens
  (Bool, Set (MemSegmentOff w))
  (Bool, Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
  (Set (MemSegmentOff w))
_2 ((Set (MemSegmentOff w) -> Identity (Set (MemSegmentOff w)))
 -> (Bool, Set (MemSegmentOff w))
 -> Identity (Bool, Set (MemSegmentOff w)))
-> (Set (MemSegmentOff w) -> Set (MemSegmentOff w))
-> StateT (Bool, Set (MemSegmentOff w)) Identity ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Set (MemSegmentOff w)
-> Set (MemSegmentOff w) -> Set (MemSegmentOff w)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (AbsValue w tp -> Set (MemSegmentOff w)
forall (w :: Natural) (tp :: Type).
AbsValue w tp -> Set (MemSegmentOff w)
codePointerSet AbsValue w tp
y_v)
            Maybe (Int64, StackEntry w)
-> StateT
     (Bool, Set (MemSegmentOff w))
     Identity
     (Maybe (Int64, StackEntry w))
forall a. a -> StateT (Bool, Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (Int64, StackEntry w)
forall a. Maybe a
Nothing
  [Maybe (Int64, StackEntry w)]
z <- ((Int64, StackEntry w)
 -> StateT
      (Bool, Set (MemSegmentOff w))
      Identity
      (Maybe (Int64, StackEntry w)))
-> [(Int64, StackEntry w)]
-> StateT
     (Bool, Set (MemSegmentOff w))
     Identity
     [Maybe (Int64, StackEntry w)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (Int64, StackEntry w)
-> StateT
     (Bool, Set (MemSegmentOff w))
     Identity
     (Maybe (Int64, StackEntry w))
entryLeq (AbsBlockStack w -> [(Int64, StackEntry w)]
forall k a. Map k a -> [(k, a)]
Map.toList AbsBlockStack w
y)
  AbsBlockStack w
-> State (Bool, Set (MemSegmentOff w)) (AbsBlockStack w)
forall a. a -> StateT (Bool, Set (MemSegmentOff w)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (AbsBlockStack w
 -> State (Bool, Set (MemSegmentOff w)) (AbsBlockStack w))
-> AbsBlockStack w
-> State (Bool, Set (MemSegmentOff w)) (AbsBlockStack w)
forall a b. (a -> b) -> a -> b
$! [(Int64, StackEntry w)] -> AbsBlockStack w
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([Maybe (Int64, StackEntry w)] -> [(Int64, StackEntry w)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Int64, StackEntry w)]
z)

showSignedHex :: Integer -> ShowS
showSignedHex :: Integer -> String -> String
showSignedHex Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = String -> String -> String
showString String
"-0x" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String -> String
forall a. Integral a => a -> String -> String
showHex (Integer -> Integer
forall a. Num a => a -> a
negate Integer
x)
                | Bool
otherwise = String -> String -> String
showString String
"0x" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String -> String
forall a. Integral a => a -> String -> String
showHex Integer
x

ppAbsStack :: MemWidth w => AbsBlockStack w -> Doc ann
ppAbsStack :: forall (w :: Natural) ann. MemWidth w => AbsBlockStack w -> Doc ann
ppAbsStack AbsBlockStack w
m = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ((Int64, StackEntry w) -> Doc ann
forall {w :: Natural} {a} {ann}.
(Assert (OrdCond (CmpNat 1 w) 'True 'True 'False) (TypeError ...),
 Integral a, MemWidth w) =>
(a, StackEntry w) -> Doc ann
pp ((Int64, StackEntry w) -> Doc ann)
-> [(Int64, StackEntry w)] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsBlockStack w -> [(Int64, StackEntry w)]
forall k a. Map k a -> [(k, a)]
Map.toDescList AbsBlockStack w
m)
  where pp :: (a, StackEntry w) -> Doc ann
pp (a
o,StackEntry MemRepr tp
_ AbsValue w tp
v) = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Integer -> String -> String
showSignedHex (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
o) String
" :=") Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> AbsValue w tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. AbsValue w tp -> Doc ann
pretty AbsValue w tp
v

------------------------------------------------------------------------
-- AbsBlockState

-- | Processor/memory state after at beginning of a block.
data AbsBlockState r
   = AbsBlockState { forall (r :: Type -> Type).
AbsBlockState r -> RegState r (AbsValue (RegAddrWidth r))
_absRegState :: !(RegState r (AbsValue (RegAddrWidth r)))
                   , forall (r :: Type -> Type).
AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
startAbsStack :: !(AbsBlockStack (RegAddrWidth r))
                   }

absRegState :: Lens' (AbsBlockState r)
                           (RegState r (AbsValue (RegAddrWidth r)))
absRegState :: forall (r :: Type -> Type) (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsBlockState r -> f (AbsBlockState r)
absRegState = (AbsBlockState r -> RegState r (AbsValue (RegAddrWidth r)))
-> (AbsBlockState r
    -> RegState r (AbsValue (RegAddrWidth r)) -> AbsBlockState r)
-> Lens
     (AbsBlockState r)
     (AbsBlockState r)
     (RegState r (AbsValue (RegAddrWidth r)))
     (RegState r (AbsValue (RegAddrWidth r)))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens AbsBlockState r -> RegState r (AbsValue (RegAddrWidth r))
forall (r :: Type -> Type).
AbsBlockState r -> RegState r (AbsValue (RegAddrWidth r))
_absRegState (\AbsBlockState r
s RegState r (AbsValue (RegAddrWidth r))
v -> AbsBlockState r
s { _absRegState = v })

-- | This constructs the abstract state for the start of the function.
--
-- It populates the register state with abstract values from the provided map,
-- along with defaults for the instruction pointer and stack pointer.  The
-- provided list provides abstract values to be placed on the stack.
--
-- NOTE: It does not place the return address as where that is stored is
-- architecture-specific.
fnStartAbsBlockState :: forall r
                     .  RegisterInfo r
                     => MemSegmentOff (RegAddrWidth r)
                        -- ^ Start address of the block
                     -> MapF r (AbsValue (RegAddrWidth r))
                        -- ^ Values to explicitly assign to registers (overriding default IP and SP values)
                     -> [(Int64, StackEntry (RegAddrWidth r))]
                        -- ^ Stack entries to populate the abstract stack with (format: (offset, abstract stack entry))
                     -> AbsBlockState r
fnStartAbsBlockState :: forall (r :: Type -> Type).
RegisterInfo r =>
MemSegmentOff (RegAddrWidth r)
-> MapF r (AbsValue (RegAddrWidth r))
-> [(Int64, StackEntry (RegAddrWidth r))]
-> AbsBlockState r
fnStartAbsBlockState MemSegmentOff (RegAddrWidth r)
addr MapF r (AbsValue (RegAddrWidth r))
m [(Int64, StackEntry (RegAddrWidth r))]
entries =
  let regFn :: r tp -> AbsValue (RegAddrWidth r) tp
      regFn :: forall (tp :: Type). r tp -> AbsValue (RegAddrWidth r) tp
regFn r tp
r
        | Just AbsValue (RegAddrWidth r) tp
v <- r tp
-> MapF r (AbsValue (RegAddrWidth r))
-> Maybe (AbsValue (RegAddrWidth r) 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 MapF r (AbsValue (RegAddrWidth r))
m = AbsValue (RegAddrWidth r) tp
v
        | Just BVType (RegAddrWidth r) :~: tp
Refl <- r (BVType (RegAddrWidth r))
-> r tp -> Maybe (BVType (RegAddrWidth r) :~: tp)
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 (BVType (RegAddrWidth r))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
ip_reg r tp
r = MemSegmentOff (RegAddrWidth r)
-> AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
forall (w :: Natural). MemSegmentOff w -> AbsValue w (BVType w)
concreteCodeAddr MemSegmentOff (RegAddrWidth r)
addr
        | Just BVType (RegAddrWidth r) :~: tp
Refl <- r (BVType (RegAddrWidth r))
-> r tp -> Maybe (BVType (RegAddrWidth r) :~: tp)
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 (BVType (RegAddrWidth r))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
sp_reg r tp
r = MemAddr (RegAddrWidth r)
-> Integer -> AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
forall (w :: Natural).
MemAddr w -> Integer -> AbsValue w (BVType w)
concreteStackOffset (MemSegmentOff (RegAddrWidth r) -> MemAddr (RegAddrWidth r)
forall (w :: Natural). MemSegmentOff w -> MemAddr w
segoffAddr MemSegmentOff (RegAddrWidth r)
addr) Integer
0
        | Bool
otherwise = AbsValue (RegAddrWidth r) tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
   in AbsBlockState { _absRegState :: RegState r (AbsValue (RegAddrWidth r))
_absRegState    = (forall (tp :: Type). r tp -> AbsValue (RegAddrWidth r) tp)
-> RegState r (AbsValue (RegAddrWidth r))
forall (r :: Type -> Type) (f :: Type -> Type).
RegisterInfo r =>
(forall (tp :: Type). r tp -> f tp) -> RegState r f
mkRegState r tp -> AbsValue (RegAddrWidth r) tp
forall (tp :: Type). r tp -> AbsValue (RegAddrWidth r) tp
regFn
                    , startAbsStack :: AbsBlockStack (RegAddrWidth r)
startAbsStack  = [(Int64, StackEntry (RegAddrWidth r))]
-> AbsBlockStack (RegAddrWidth r)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int64, StackEntry (RegAddrWidth r))]
entries
                    }

joinAbsBlockState :: RegisterInfo r
                  => AbsBlockState r
                  -> AbsBlockState r
                  -> Maybe (AbsBlockState r)
joinAbsBlockState :: forall (r :: Type -> Type).
RegisterInfo r =>
AbsBlockState r -> AbsBlockState r -> Maybe (AbsBlockState r)
joinAbsBlockState AbsBlockState r
x AbsBlockState r
y
    | Bool
regs_changed = AbsBlockState r -> Maybe (AbsBlockState r)
forall a. a -> Maybe a
Just (AbsBlockState r -> Maybe (AbsBlockState r))
-> AbsBlockState r -> Maybe (AbsBlockState r)
forall a b. (a -> b) -> a -> b
$! AbsBlockState r
z
    | Bool
otherwise = Maybe (AbsBlockState r)
forall a. Maybe a
Nothing
  where xs :: RegState r (AbsValue (RegAddrWidth r))
xs = AbsBlockState r
xAbsBlockState r
-> Getting
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsBlockState r)
     (RegState r (AbsValue (RegAddrWidth r)))
-> RegState r (AbsValue (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.Getting
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsBlockState r)
  (RegState r (AbsValue (RegAddrWidth r)))
forall (r :: Type -> Type) (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsBlockState r -> f (AbsBlockState r)
absRegState
        ys :: RegState r (AbsValue (RegAddrWidth r))
ys = AbsBlockState r
yAbsBlockState r
-> Getting
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsBlockState r)
     (RegState r (AbsValue (RegAddrWidth r)))
-> RegState r (AbsValue (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.Getting
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsBlockState r)
  (RegState r (AbsValue (RegAddrWidth r)))
forall (r :: Type -> Type) (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsBlockState r -> f (AbsBlockState r)
absRegState

        x_stk :: AbsBlockStack (RegAddrWidth r)
x_stk = AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
forall (r :: Type -> Type).
AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
startAbsStack AbsBlockState r
x
        y_stk :: AbsBlockStack (RegAddrWidth r)
y_stk = AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
forall (r :: Type -> Type).
AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
startAbsStack AbsBlockState r
y

        (AbsBlockState r
z,(Bool
regs_changed,Set (MemSegmentOff (RegAddrWidth r))
_dropped)) = (State
   (Bool, Set (MemSegmentOff (RegAddrWidth r))) (AbsBlockState r)
 -> (Bool, Set (MemSegmentOff (RegAddrWidth r)))
 -> (AbsBlockState r, (Bool, Set (MemSegmentOff (RegAddrWidth r)))))
-> (Bool, Set (MemSegmentOff (RegAddrWidth r)))
-> State
     (Bool, Set (MemSegmentOff (RegAddrWidth r))) (AbsBlockState r)
-> (AbsBlockState r, (Bool, Set (MemSegmentOff (RegAddrWidth r))))
forall a b c. (a -> b -> c) -> b -> a -> c
flip State
  (Bool, Set (MemSegmentOff (RegAddrWidth r))) (AbsBlockState r)
-> (Bool, Set (MemSegmentOff (RegAddrWidth r)))
-> (AbsBlockState r, (Bool, Set (MemSegmentOff (RegAddrWidth r))))
forall s a. State s a -> s -> (a, s)
runState (Bool
False, Set (MemSegmentOff (RegAddrWidth r))
forall a. Set a
Set.empty) (State
   (Bool, Set (MemSegmentOff (RegAddrWidth r))) (AbsBlockState r)
 -> (AbsBlockState r, (Bool, Set (MemSegmentOff (RegAddrWidth r)))))
-> State
     (Bool, Set (MemSegmentOff (RegAddrWidth r))) (AbsBlockState r)
-> (AbsBlockState r, (Bool, Set (MemSegmentOff (RegAddrWidth r))))
forall a b. (a -> b) -> a -> b
$ do
            RegState r (AbsValue (RegAddrWidth r))
z_regs <- (forall (tp :: Type).
 r tp
 -> StateT
      (Bool, Set (MemSegmentOff (RegAddrWidth r)))
      Identity
      (AbsValue (RegAddrWidth r) tp))
-> StateT
     (Bool, Set (MemSegmentOff (RegAddrWidth r)))
     Identity
     (RegState r (AbsValue (RegAddrWidth r)))
forall (r :: Type -> Type) (m :: Type -> Type) (f :: Type -> Type).
(RegisterInfo r, Applicative m) =>
(forall (tp :: Type). r tp -> m (f tp)) -> m (RegState r f)
mkRegStateM ((forall (tp :: Type).
  r tp
  -> StateT
       (Bool, Set (MemSegmentOff (RegAddrWidth r)))
       Identity
       (AbsValue (RegAddrWidth r) tp))
 -> StateT
      (Bool, Set (MemSegmentOff (RegAddrWidth r)))
      Identity
      (RegState r (AbsValue (RegAddrWidth r))))
-> (forall (tp :: Type).
    r tp
    -> StateT
         (Bool, Set (MemSegmentOff (RegAddrWidth r)))
         Identity
         (AbsValue (RegAddrWidth r) tp))
-> StateT
     (Bool, Set (MemSegmentOff (RegAddrWidth r)))
     Identity
     (RegState r (AbsValue (RegAddrWidth r)))
forall a b. (a -> b) -> a -> b
$ \r tp
r -> do
              let xr :: AbsValue (RegAddrWidth r) tp
xr = RegState r (AbsValue (RegAddrWidth r))
xsRegState r (AbsValue (RegAddrWidth r))
-> Getting
     (AbsValue (RegAddrWidth r) tp)
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsValue (RegAddrWidth r) tp)
-> AbsValue (RegAddrWidth r) tp
forall s a. s -> Getting a s a -> a
^.r tp
-> Lens'
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsValue (RegAddrWidth r) tp)
forall {k} (r :: k -> Type) (f :: k -> Type) (tp :: k).
OrdF r =>
r tp -> Lens' (RegState r f) (f tp)
boundValue r tp
r
              (Bool
c,Set (MemSegmentOff (RegAddrWidth r))
s) <- StateT
  (Bool, Set (MemSegmentOff (RegAddrWidth r)))
  Identity
  (Bool, Set (MemSegmentOff (RegAddrWidth r)))
forall s (m :: Type -> Type). MonadState s m => m s
get
              case State
  (Set (MemSegmentOff (RegAddrWidth r)))
  (Maybe (AbsValue (RegAddrWidth r) tp))
-> Set (MemSegmentOff (RegAddrWidth r))
-> (Maybe (AbsValue (RegAddrWidth r) tp),
    Set (MemSegmentOff (RegAddrWidth r)))
forall s a. State s a -> s -> (a, s)
runState (AbsValue (RegAddrWidth r) tp
-> AbsValue (RegAddrWidth r) tp
-> State
     (Set (MemSegmentOff (RegAddrWidth r)))
     (Maybe (AbsValue (RegAddrWidth r) tp))
forall (w :: Natural) (tp :: Type).
MemWidth w =>
AbsValue w tp
-> AbsValue w tp
-> State (Set (MemSegmentOff w)) (Maybe (AbsValue w tp))
joinAbsValue' AbsValue (RegAddrWidth r) tp
xr (RegState r (AbsValue (RegAddrWidth r))
ysRegState r (AbsValue (RegAddrWidth r))
-> Getting
     (AbsValue (RegAddrWidth r) tp)
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsValue (RegAddrWidth r) tp)
-> AbsValue (RegAddrWidth r) tp
forall s a. s -> Getting a s a -> a
^.r tp
-> Lens'
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsValue (RegAddrWidth r) tp)
forall {k} (r :: k -> Type) (f :: k -> Type) (tp :: k).
OrdF r =>
r tp -> Lens' (RegState r f) (f tp)
boundValue r tp
r)) Set (MemSegmentOff (RegAddrWidth r))
s of
                (Maybe (AbsValue (RegAddrWidth r) tp)
Nothing,Set (MemSegmentOff (RegAddrWidth r))
s') -> do
                  Set (MemSegmentOff (RegAddrWidth r))
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
forall a b. a -> b -> b
seq Set (MemSegmentOff (RegAddrWidth r))
s' (StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
 -> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ())
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
forall a b. (a -> b) -> a -> b
$ (Bool, Set (MemSegmentOff (RegAddrWidth r)))
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put ((Bool, Set (MemSegmentOff (RegAddrWidth r)))
 -> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ())
-> (Bool, Set (MemSegmentOff (RegAddrWidth r)))
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
forall a b. (a -> b) -> a -> b
$ (Bool
c,Set (MemSegmentOff (RegAddrWidth r))
s')
                  AbsValue (RegAddrWidth r) tp
-> StateT
     (Bool, Set (MemSegmentOff (RegAddrWidth r)))
     Identity
     (AbsValue (RegAddrWidth r) tp)
forall a.
a -> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (AbsValue (RegAddrWidth r) tp
 -> StateT
      (Bool, Set (MemSegmentOff (RegAddrWidth r)))
      Identity
      (AbsValue (RegAddrWidth r) tp))
-> AbsValue (RegAddrWidth r) tp
-> StateT
     (Bool, Set (MemSegmentOff (RegAddrWidth r)))
     Identity
     (AbsValue (RegAddrWidth r) tp)
forall a b. (a -> b) -> a -> b
$! AbsValue (RegAddrWidth r) tp
xr
                (Just AbsValue (RegAddrWidth r) tp
zr,Set (MemSegmentOff (RegAddrWidth r))
s') -> do
                  Set (MemSegmentOff (RegAddrWidth r))
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
forall a b. a -> b -> b
seq Set (MemSegmentOff (RegAddrWidth r))
s' (StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
 -> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ())
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
forall a b. (a -> b) -> a -> b
$ (Bool, Set (MemSegmentOff (RegAddrWidth r)))
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put ((Bool, Set (MemSegmentOff (RegAddrWidth r)))
 -> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ())
-> (Bool, Set (MemSegmentOff (RegAddrWidth r)))
-> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity ()
forall a b. (a -> b) -> a -> b
$ (Bool
True,Set (MemSegmentOff (RegAddrWidth r))
s')
                  AbsValue (RegAddrWidth r) tp
-> StateT
     (Bool, Set (MemSegmentOff (RegAddrWidth r)))
     Identity
     (AbsValue (RegAddrWidth r) tp)
forall a.
a -> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (AbsValue (RegAddrWidth r) tp
 -> StateT
      (Bool, Set (MemSegmentOff (RegAddrWidth r)))
      Identity
      (AbsValue (RegAddrWidth r) tp))
-> AbsValue (RegAddrWidth r) tp
-> StateT
     (Bool, Set (MemSegmentOff (RegAddrWidth r)))
     Identity
     (AbsValue (RegAddrWidth r) tp)
forall a b. (a -> b) -> a -> b
$! AbsValue (RegAddrWidth r) tp
zr
            AbsBlockStack (RegAddrWidth r)
z_stk <- AbsBlockStack (RegAddrWidth r)
-> AbsBlockStack (RegAddrWidth r)
-> State
     (Bool, Set (MemSegmentOff (RegAddrWidth r)))
     (AbsBlockStack (RegAddrWidth r))
forall (w :: Natural).
MemWidth w =>
AbsBlockStack w
-> AbsBlockStack w
-> State (Bool, Set (MemSegmentOff w)) (AbsBlockStack w)
absStackJoinD AbsBlockStack (RegAddrWidth r)
x_stk AbsBlockStack (RegAddrWidth r)
y_stk
            AbsBlockState r
-> State
     (Bool, Set (MemSegmentOff (RegAddrWidth r))) (AbsBlockState r)
forall a.
a -> StateT (Bool, Set (MemSegmentOff (RegAddrWidth r))) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (AbsBlockState r
 -> State
      (Bool, Set (MemSegmentOff (RegAddrWidth r))) (AbsBlockState r))
-> AbsBlockState r
-> State
     (Bool, Set (MemSegmentOff (RegAddrWidth r))) (AbsBlockState r)
forall a b. (a -> b) -> a -> b
$ AbsBlockState { _absRegState :: RegState r (AbsValue (RegAddrWidth r))
_absRegState     = RegState r (AbsValue (RegAddrWidth r))
z_regs
                                   , startAbsStack :: AbsBlockStack (RegAddrWidth r)
startAbsStack   = AbsBlockStack (RegAddrWidth r)
z_stk
                                   }

instance ( ShowF r
         , MemWidth (RegAddrWidth r)
         ) => Pretty (AbsBlockState r) where
  pretty :: forall ann. AbsBlockState r -> Doc ann
pretty AbsBlockState r
s =
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
    [ Doc ann
"registers:"
    , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (RegState r (AbsValue (RegAddrWidth r)) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. RegState r (AbsValue (RegAddrWidth r)) -> Doc ann
pretty (AbsBlockState r
sAbsBlockState r
-> Getting
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsBlockState r)
     (RegState r (AbsValue (RegAddrWidth r)))
-> RegState r (AbsValue (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.Getting
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsBlockState r)
  (RegState r (AbsValue (RegAddrWidth r)))
forall (r :: Type -> Type) (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsBlockState r -> f (AbsBlockState r)
absRegState))
    , Doc ann
stack_d
    ]
    where stack :: AbsBlockStack (RegAddrWidth r)
stack = AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
forall (r :: Type -> Type).
AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
startAbsStack AbsBlockState r
s
          stack_d :: Doc ann
stack_d | AbsBlockStack (RegAddrWidth r) -> Bool
forall k a. Map k a -> Bool
Map.null AbsBlockStack (RegAddrWidth r)
stack = Doc ann
forall ann. Doc ann
emptyDoc
                  | Bool
otherwise =
                      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
                      [ Doc ann
"stack:"
                      , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (AbsBlockStack (RegAddrWidth r) -> Doc ann
forall (w :: Natural) ann. MemWidth w => AbsBlockStack w -> Doc ann
ppAbsStack AbsBlockStack (RegAddrWidth r)
stack)
                      ]

instance (ShowF r, MemWidth (RegAddrWidth r)) => Show (AbsBlockState r) where
  show :: AbsBlockState r -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (AbsBlockState r -> Doc Any) -> AbsBlockState r -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsBlockState r -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. AbsBlockState r -> Doc ann
pretty

-- | Update the block state to point to a specific IP address.
setAbsIP :: RegisterInfo r
         => MemSegmentOff (RegAddrWidth r)
            -- ^ The address to set.
         -> AbsBlockState r
         -> AbsBlockState r
setAbsIP :: forall (r :: Type -> Type).
RegisterInfo r =>
MemSegmentOff (RegAddrWidth r)
-> AbsBlockState r -> AbsBlockState r
setAbsIP MemSegmentOff (RegAddrWidth r)
a AbsBlockState r
b
    -- Check to avoid reassigning next IP if it is not needed.
  | CodePointers Set (MemSegmentOff (RegAddrWidth r))
s Bool
False <- AbsBlockState r
bAbsBlockState r
-> Getting
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsBlockState r)
     (RegState r (AbsValue (RegAddrWidth r)))
-> RegState r (AbsValue (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.Getting
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsBlockState r)
  (RegState r (AbsValue (RegAddrWidth r)))
forall (r :: Type -> Type) (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsBlockState r -> f (AbsBlockState r)
absRegStateRegState r (AbsValue (RegAddrWidth r))
-> Getting
     (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)))
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)))
-> AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.r (BVType (RegAddrWidth r))
-> Lens'
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)))
forall {k} (r :: k -> Type) (f :: k -> Type) (tp :: k).
OrdF r =>
r tp -> Lens' (RegState r f) (f tp)
boundValue r (BVType (RegAddrWidth r))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
ip_reg
  , Set (MemSegmentOff (RegAddrWidth r)) -> Int
forall a. Set a -> Int
Set.size Set (MemSegmentOff (RegAddrWidth r))
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
  , MemSegmentOff (RegAddrWidth r)
-> Set (MemSegmentOff (RegAddrWidth r)) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member MemSegmentOff (RegAddrWidth r)
a Set (MemSegmentOff (RegAddrWidth r))
s =
    AbsBlockState r
b
  | Bool
otherwise =
    AbsBlockState r
b AbsBlockState r
-> (AbsBlockState r -> AbsBlockState r) -> AbsBlockState r
forall a b. a -> (a -> b) -> b
& (RegState r (AbsValue (RegAddrWidth r))
 -> Identity (RegState r (AbsValue (RegAddrWidth r))))
-> AbsBlockState r -> Identity (AbsBlockState r)
forall (r :: Type -> Type) (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsBlockState r -> f (AbsBlockState r)
absRegState ((RegState r (AbsValue (RegAddrWidth r))
  -> Identity (RegState r (AbsValue (RegAddrWidth r))))
 -> AbsBlockState r -> Identity (AbsBlockState r))
-> ((AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
     -> Identity (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))))
    -> RegState r (AbsValue (RegAddrWidth r))
    -> Identity (RegState r (AbsValue (RegAddrWidth r))))
-> (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
    -> Identity (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))))
-> AbsBlockState r
-> Identity (AbsBlockState r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
 -> Identity (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))))
-> RegState r (AbsValue (RegAddrWidth r))
-> Identity (RegState r (AbsValue (RegAddrWidth r)))
Lens'
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)))
forall (r :: Type -> Type) (f :: Type -> Type).
RegisterInfo r =>
Lens' (RegState r f) (f (BVType (RegAddrWidth r)))
curIP ((AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
  -> Identity (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))))
 -> AbsBlockState r -> Identity (AbsBlockState r))
-> AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
-> AbsBlockState r
-> AbsBlockState r
forall s t a b. ASetter s t a b -> b -> s -> t
.~ MemSegmentOff (RegAddrWidth r)
-> AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
forall (w :: Natural). MemSegmentOff w -> AbsValue w (BVType w)
concreteCodeAddr MemSegmentOff (RegAddrWidth r)
a

------------------------------------------------------------------------
-- AbsProcessorState

-- | The type of abstract values associated with a given architecture.
--
-- This is only a function of the address width.
type ArchAbsValue arch = AbsValue (ArchAddrWidth arch)

-- | This stores the abstract state of the system which may be within
-- a block.
data AbsProcessorState r ids
   = AbsProcessorState { forall (r :: Type -> Type) ids.
AbsProcessorState r ids -> Memory (RegAddrWidth r)
absMem       :: !(Memory (RegAddrWidth r))
                         -- ^ Recognizer for code addresses.
                       , forall (r :: Type -> Type) ids.
AbsProcessorState r ids -> RegState r (AbsValue (RegAddrWidth r))
_absInitialRegs
                         :: !(RegState r (AbsValue (RegAddrWidth r)))
                         -- ^ Default values of registers
                       , forall (r :: Type -> Type) ids.
AbsProcessorState r ids
-> MapF (AssignId ids) (AbsValue (RegAddrWidth r))
_absAssignments :: !(MapF (AssignId ids) (AbsValue (RegAddrWidth r)))
                         -- ^ The assignments that have been seen, and the
                         -- symbolic values associated with them
                       , forall (r :: Type -> Type) ids.
AbsProcessorState r ids -> AbsBlockStack (RegAddrWidth r)
_curAbsStack    :: !(AbsBlockStack (RegAddrWidth r))
                         -- ^ The current symbolic state of the stack
                       }

absInitialRegs :: Lens' (AbsProcessorState r ids)
                              (RegState r (AbsValue (RegAddrWidth r)))
absInitialRegs :: forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
absInitialRegs = (AbsProcessorState r ids -> RegState r (AbsValue (RegAddrWidth r)))
-> (AbsProcessorState r ids
    -> RegState r (AbsValue (RegAddrWidth r))
    -> AbsProcessorState r ids)
-> Lens
     (AbsProcessorState r ids)
     (AbsProcessorState r ids)
     (RegState r (AbsValue (RegAddrWidth r)))
     (RegState r (AbsValue (RegAddrWidth r)))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens AbsProcessorState r ids -> RegState r (AbsValue (RegAddrWidth r))
forall (r :: Type -> Type) ids.
AbsProcessorState r ids -> RegState r (AbsValue (RegAddrWidth r))
_absInitialRegs (\AbsProcessorState r ids
s RegState r (AbsValue (RegAddrWidth r))
v -> AbsProcessorState r ids
s { _absInitialRegs = v })

absAssignments :: Lens' (AbsProcessorState r ids)
                              (MapF (AssignId ids) (AbsValue (RegAddrWidth r)))
absAssignments :: forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(MapF (AssignId ids) (AbsValue (RegAddrWidth r))
 -> f (MapF (AssignId ids) (AbsValue (RegAddrWidth r))))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
absAssignments = (AbsProcessorState r ids
 -> MapF (AssignId ids) (AbsValue (RegAddrWidth r)))
-> (AbsProcessorState r ids
    -> MapF (AssignId ids) (AbsValue (RegAddrWidth r))
    -> AbsProcessorState r ids)
-> Lens
     (AbsProcessorState r ids)
     (AbsProcessorState r ids)
     (MapF (AssignId ids) (AbsValue (RegAddrWidth r)))
     (MapF (AssignId ids) (AbsValue (RegAddrWidth r)))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens AbsProcessorState r ids
-> MapF (AssignId ids) (AbsValue (RegAddrWidth r))
forall (r :: Type -> Type) ids.
AbsProcessorState r ids
-> MapF (AssignId ids) (AbsValue (RegAddrWidth r))
_absAssignments (\AbsProcessorState r ids
s MapF (AssignId ids) (AbsValue (RegAddrWidth r))
v -> AbsProcessorState r ids
s { _absAssignments = v })

curAbsStack :: Lens' (AbsProcessorState r ids) (AbsBlockStack (RegAddrWidth r))
curAbsStack :: forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack = (AbsProcessorState r ids -> AbsBlockStack (RegAddrWidth r))
-> (AbsProcessorState r ids
    -> AbsBlockStack (RegAddrWidth r) -> AbsProcessorState r ids)
-> Lens
     (AbsProcessorState r ids)
     (AbsProcessorState r ids)
     (AbsBlockStack (RegAddrWidth r))
     (AbsBlockStack (RegAddrWidth r))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens AbsProcessorState r ids -> AbsBlockStack (RegAddrWidth r)
forall (r :: Type -> Type) ids.
AbsProcessorState r ids -> AbsBlockStack (RegAddrWidth r)
_curAbsStack (\AbsProcessorState r ids
s AbsBlockStack (RegAddrWidth r)
v -> AbsProcessorState r ids
s { _curAbsStack = v })

instance (ShowF r, MemWidth (RegAddrWidth r))
      => Pretty (AbsProcessorState r ids) where
  pretty :: forall ann. AbsProcessorState r ids -> Doc ann
pretty AbsProcessorState r ids
s =
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
    [ Doc ann
"registers:"
    , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (RegState r (AbsValue (RegAddrWidth r)) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. RegState r (AbsValue (RegAddrWidth r)) -> Doc ann
pretty (AbsProcessorState r ids
sAbsProcessorState r ids
-> Getting
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsProcessorState r ids)
     (RegState r (AbsValue (RegAddrWidth r)))
-> RegState r (AbsValue (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.Getting
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsProcessorState r ids)
  (RegState r (AbsValue (RegAddrWidth r)))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
absInitialRegs))
    , Doc ann
stack_d
    ]
    where stack :: Map Int64 (StackEntry (RegAddrWidth r))
stack = AbsProcessorState r ids
sAbsProcessorState r ids
-> Getting
     (Map Int64 (StackEntry (RegAddrWidth r)))
     (AbsProcessorState r ids)
     (Map Int64 (StackEntry (RegAddrWidth r)))
-> Map Int64 (StackEntry (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.Getting
  (Map Int64 (StackEntry (RegAddrWidth r)))
  (AbsProcessorState r ids)
  (Map Int64 (StackEntry (RegAddrWidth r)))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack
          stack_d :: Doc ann
stack_d | Map Int64 (StackEntry (RegAddrWidth r)) -> Bool
forall k a. Map k a -> Bool
Map.null Map Int64 (StackEntry (RegAddrWidth r))
stack = Doc ann
forall ann. Doc ann
emptyDoc
                  | Bool
otherwise =
                    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
                    [ Doc ann
"stack:"
                    , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Map Int64 (StackEntry (RegAddrWidth r)) -> Doc ann
forall (w :: Natural) ann. MemWidth w => AbsBlockStack w -> Doc ann
ppAbsStack Map Int64 (StackEntry (RegAddrWidth r))
stack)
                    ]

instance (ShowF r, MemWidth (RegAddrWidth r))
      => Show (AbsProcessorState r ids) where
  show :: AbsProcessorState r ids -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (AbsProcessorState r ids -> Doc Any)
-> AbsProcessorState r ids
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsProcessorState r ids -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. AbsProcessorState r ids -> Doc ann
pretty

-- | Construct a abstate processor state for the start of block execution.
initAbsProcessorState :: Memory (RegAddrWidth r)
                         -- ^ Current state of memory in the processor.
                         --
                         -- Used for checking code segment status.
                      -> AbsBlockState r
                      -> AbsProcessorState r ids
initAbsProcessorState :: forall (r :: Type -> Type) ids.
Memory (RegAddrWidth r)
-> AbsBlockState r -> AbsProcessorState r ids
initAbsProcessorState Memory (RegAddrWidth r)
mem AbsBlockState r
s =
  AbsProcessorState { absMem :: Memory (RegAddrWidth r)
absMem = Memory (RegAddrWidth r)
mem
                    , _absInitialRegs :: RegState r (AbsValue (RegAddrWidth r))
_absInitialRegs = AbsBlockState r
sAbsBlockState r
-> Getting
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsBlockState r)
     (RegState r (AbsValue (RegAddrWidth r)))
-> RegState r (AbsValue (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.Getting
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsBlockState r)
  (RegState r (AbsValue (RegAddrWidth r)))
forall (r :: Type -> Type) (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsBlockState r -> f (AbsBlockState r)
absRegState
                    , _absAssignments :: MapF (AssignId ids) (AbsValue (RegAddrWidth r))
_absAssignments = MapF (AssignId ids) (AbsValue (RegAddrWidth r))
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty
                    , _curAbsStack :: AbsBlockStack (RegAddrWidth r)
_curAbsStack = AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
forall (r :: Type -> Type).
AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
startAbsStack AbsBlockState r
s
                    }

-- | A lens that allows one to lookup and update the value of an assignment in
-- map from assignments to abstract values.
assignLens :: AssignId ids tp
           -> Lens' (MapF (AssignId ids) (AbsValue w)) (AbsValue w tp)
assignLens :: forall ids (tp :: Type) (w :: Natural).
AssignId ids tp
-> Lens' (MapF (AssignId ids) (AbsValue w)) (AbsValue w tp)
assignLens AssignId ids tp
aid = (MapF (AssignId ids) (AbsValue w) -> AbsValue w tp)
-> (MapF (AssignId ids) (AbsValue w)
    -> AbsValue w tp -> MapF (AssignId ids) (AbsValue w))
-> Lens
     (MapF (AssignId ids) (AbsValue w))
     (MapF (AssignId ids) (AbsValue w))
     (AbsValue w tp)
     (AbsValue w tp)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (AbsValue w tp -> Maybe (AbsValue w tp) -> AbsValue w tp
forall a. a -> Maybe a -> a
fromMaybe AbsValue w tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV (Maybe (AbsValue w tp) -> AbsValue w tp)
-> (MapF (AssignId ids) (AbsValue w) -> Maybe (AbsValue w tp))
-> MapF (AssignId ids) (AbsValue w)
-> AbsValue w tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AssignId ids tp
-> MapF (AssignId ids) (AbsValue w) -> Maybe (AbsValue w 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)
                      (\MapF (AssignId ids) (AbsValue w)
s AbsValue w tp
v -> AssignId ids tp
-> AbsValue w tp
-> MapF (AssignId ids) (AbsValue w)
-> MapF (AssignId ids) (AbsValue w)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert AssignId ids tp
aid AbsValue w tp
v MapF (AssignId ids) (AbsValue w)
s)

deleteRange :: Int64 -> Int64 -> AbsBlockStack w -> AbsBlockStack w
deleteRange :: forall (w :: Natural).
Int64 -> Int64 -> AbsBlockStack w -> AbsBlockStack w
deleteRange Int64
l Int64
h AbsBlockStack w
m
  | Int64
h Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int64
l = AbsBlockStack w
m
  | Bool
otherwise =
    case Int64 -> AbsBlockStack w -> Maybe (Int64, StackEntry w)
forall k v. Ord k => k -> Map k v -> Maybe (k, v)
Map.lookupGE Int64
l AbsBlockStack w
m of
      Just (Int64
k,StackEntry w
v)
        | Int64
k Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
< Int64
h
        , StackEntry MemRepr tp
_ AbsValue w tp
ReturnAddr <- StackEntry w
v ->
          DebugClass -> String -> AbsBlockStack w -> AbsBlockStack w
forall a. (?loc::CallStack) => DebugClass -> String -> a -> a
debug DebugClass
DAbsInt (String
"Failing to delete return address at offset " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int64, Int64, Int64) -> String
forall a. Show a => a -> String
show (Int64
k,Int64
l,Int64
h))
                (Int64 -> Int64 -> AbsBlockStack w -> AbsBlockStack w
forall (w :: Natural).
Int64 -> Int64 -> AbsBlockStack w -> AbsBlockStack w
deleteRange (Int64
kInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1) Int64
h AbsBlockStack w
m)
        | Int64
k Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
< Int64
h ->
          Int64 -> Int64 -> AbsBlockStack w -> AbsBlockStack w
forall (w :: Natural).
Int64 -> Int64 -> AbsBlockStack w -> AbsBlockStack w
deleteRange (Int64
kInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1) Int64
h (Int64 -> AbsBlockStack w -> AbsBlockStack w
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Int64
k AbsBlockStack w
m)
      Maybe (Int64, StackEntry w)
_ -> AbsBlockStack w
m

-- | Prune stack based on write that may modify stack.
pruneStack :: AbsBlockStack w -> AbsBlockStack w
pruneStack :: forall (w :: Natural). AbsBlockStack w -> AbsBlockStack w
pruneStack = (StackEntry w -> Bool)
-> Map Int64 (StackEntry w) -> Map Int64 (StackEntry w)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter StackEntry w -> Bool
forall {w :: Natural}. StackEntry w -> Bool
f
  where f :: StackEntry w -> Bool
f (StackEntry MemRepr tp
_ AbsValue w tp
ReturnAddr) = Bool
True
        f StackEntry w
_ = Bool
False

------------------------------------------------------------------------
-- Transfer Value

-- | Compute abstract value from value and current registers.
transferValue :: forall a ids tp
              .  ( RegisterInfo (ArchReg a)
                 , HasCallStack
                 )
              => AbsProcessorState (ArchReg a) ids
              -> Value a ids tp
              -> ArchAbsValue a tp
transferValue :: forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg a) ids
c Value a ids tp
v = do
  case Value a ids tp
v of
    BoolValue Bool
b -> Bool -> AbsValue (RegAddrWidth (ArchReg a)) tp
forall (w :: Natural) (tp :: Type).
(tp ~ BoolType) =>
Bool -> AbsValue w tp
BoolConst Bool
b
    BVValue NatRepr n
w Integer
i
      | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= NatRepr n -> Integer
forall (n :: Natural). NatRepr n -> Integer
maxUnsigned NatRepr n
w -> Memory (RegAddrWidth (ArchReg a))
-> NatRepr n
-> Integer
-> AbsValue (RegAddrWidth (ArchReg a)) (BVType n)
forall (w :: Natural) (n :: Natural).
MemWidth w =>
Memory w -> NatRepr n -> Integer -> AbsValue w (BVType n)
abstractSingleton (AbsProcessorState (ArchReg a) ids
-> Memory (RegAddrWidth (ArchReg a))
forall (r :: Type -> Type) ids.
AbsProcessorState r ids -> Memory (RegAddrWidth r)
absMem AbsProcessorState (ArchReg a) ids
c) NatRepr n
w Integer
i
      | Bool
otherwise -> String -> AbsValue (RegAddrWidth (ArchReg a)) tp
forall a. HasCallStack => String -> a
error (String -> AbsValue (RegAddrWidth (ArchReg a)) tp)
-> String -> AbsValue (RegAddrWidth (ArchReg a)) tp
forall a b. (a -> b) -> a -> b
$ String
"transferValue given illegal value " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Value a ids tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Value a ids tp -> Doc ann
pretty Value a ids tp
v)
    -- TODO: Ensure a relocatable value is in code.
    RelocatableValue AddrWidthRepr (RegAddrWidth (ArchReg a))
_w MemAddr (RegAddrWidth (ArchReg a))
i
      | Just MemSegmentOff (RegAddrWidth (ArchReg a))
addr <- Memory (RegAddrWidth (ArchReg a))
-> MemAddr (RegAddrWidth (ArchReg a))
-> Maybe (MemSegmentOff (RegAddrWidth (ArchReg a)))
forall (w :: Natural).
Memory w -> MemAddr w -> Maybe (MemSegmentOff w)
asSegmentOff (AbsProcessorState (ArchReg a) ids
-> Memory (RegAddrWidth (ArchReg a))
forall (r :: Type -> Type) ids.
AbsProcessorState r ids -> Memory (RegAddrWidth r)
absMem AbsProcessorState (ArchReg a) ids
c) MemAddr (RegAddrWidth (ArchReg a))
i
      , MemSegment (RegAddrWidth (ArchReg a)) -> Flags
forall (w :: Natural). MemSegment w -> Flags
segmentFlags (MemSegmentOff (RegAddrWidth (ArchReg a))
-> MemSegment (RegAddrWidth (ArchReg a))
forall (w :: Natural). MemSegmentOff w -> MemSegment w
segoffSegment MemSegmentOff (RegAddrWidth (ArchReg a))
addr) Flags -> Flags -> Bool
`Perm.hasPerm` Flags
Perm.execute ->
        MemSegmentOff (RegAddrWidth (ArchReg a))
-> AbsValue
     (RegAddrWidth (ArchReg a)) (BVType (RegAddrWidth (ArchReg a)))
forall (w :: Natural). MemSegmentOff w -> AbsValue w (BVType w)
concreteCodeAddr MemSegmentOff (RegAddrWidth (ArchReg a))
addr
      | Just MemWord (RegAddrWidth (ArchReg a))
addr <- MemAddr (RegAddrWidth (ArchReg a))
-> Maybe (MemWord (RegAddrWidth (ArchReg a)))
forall (w :: Natural). MemWidth w => MemAddr w -> Maybe (MemWord w)
asAbsoluteAddr MemAddr (RegAddrWidth (ArchReg a))
i ->
          Set Integer -> AbsValue (RegAddrWidth (ArchReg a)) tp
forall (w :: Natural) (tp :: Type) (n :: Natural).
(tp ~ BVType n) =>
Set Integer -> AbsValue w tp
FinSet (Set Integer -> AbsValue (RegAddrWidth (ArchReg a)) tp)
-> Set Integer -> AbsValue (RegAddrWidth (ArchReg a)) tp
forall a b. (a -> b) -> a -> b
$ Integer -> Set Integer
forall a. a -> Set a
Set.singleton (Integer -> Set Integer) -> Integer -> Set Integer
forall a b. (a -> b) -> a -> b
$ MemWord (RegAddrWidth (ArchReg a)) -> Integer
forall a. Integral a => a -> Integer
toInteger MemWord (RegAddrWidth (ArchReg a))
addr
      | Bool
otherwise ->
        AbsValue (RegAddrWidth (ArchReg a)) tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
    SymbolValue{} -> AbsValue (RegAddrWidth (ArchReg a)) tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
    -- Invariant: v is in m
    AssignedValue Assignment a ids tp
a ->
      AbsValue (RegAddrWidth (ArchReg a)) tp
-> Maybe (AbsValue (RegAddrWidth (ArchReg a)) tp)
-> AbsValue (RegAddrWidth (ArchReg a)) tp
forall a. a -> Maybe a -> a
fromMaybe (String -> AbsValue (RegAddrWidth (ArchReg a)) tp
forall a. HasCallStack => String -> a
error (String -> AbsValue (RegAddrWidth (ArchReg a)) tp)
-> String -> AbsValue (RegAddrWidth (ArchReg a)) tp
forall a b. (a -> b) -> a -> b
$ String
"Missing assignment for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AssignId ids tp -> String
forall a. Show a => a -> String
show (Assignment a ids tp -> AssignId ids tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId Assignment a ids tp
a))
                (AssignId ids tp
-> MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a)))
-> Maybe (AbsValue (RegAddrWidth (ArchReg a)) tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup (Assignment a ids tp -> AssignId ids tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId Assignment a ids tp
a) (AbsProcessorState (ArchReg a) ids
cAbsProcessorState (ArchReg a) ids
-> Getting
     (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a))))
     (AbsProcessorState (ArchReg a) ids)
     (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a))))
-> MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a)))
forall s a. s -> Getting a s a -> a
^.Getting
  (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a))))
  (AbsProcessorState (ArchReg a) ids)
  (MapF (AssignId ids) (AbsValue (RegAddrWidth (ArchReg a))))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(MapF (AssignId ids) (AbsValue (RegAddrWidth r))
 -> f (MapF (AssignId ids) (AbsValue (RegAddrWidth r))))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
absAssignments))
    Initial ArchReg a tp
r -> AbsProcessorState (ArchReg a) ids
cAbsProcessorState (ArchReg a) ids
-> Getting
     (RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a))))
     (AbsProcessorState (ArchReg a) ids)
     (RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a))))
-> RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a)))
forall s a. s -> Getting a s a -> a
^.Getting
  (RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a))))
  (AbsProcessorState (ArchReg a) ids)
  (RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a))))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
absInitialRegs RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a)))
-> Getting
     (AbsValue (RegAddrWidth (ArchReg a)) tp)
     (RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a))))
     (AbsValue (RegAddrWidth (ArchReg a)) tp)
-> AbsValue (RegAddrWidth (ArchReg a)) tp
forall s a. s -> Getting a s a -> a
^. ArchReg a tp
-> Lens'
     (RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a))))
     (AbsValue (RegAddrWidth (ArchReg a)) tp)
forall {k} (r :: k -> Type) (f :: k -> Type) (tp :: k).
OrdF r =>
r tp -> Lens' (RegState r f) (f tp)
boundValue ArchReg a tp
r

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

-- | Update the processor state with a memory write.
addMemWrite :: ( RegisterInfo (ArchReg arch)
               , MemWidth (ArchAddrWidth arch)
               , HasCallStack
               )
            => AbsProcessorState (ArchReg arch) ids
            -- ^ Current processor state.
            -> Value arch ids (BVType (ArchAddrWidth arch))
            -- ^ Address that we are writing to.
            -> MemRepr tp
            -- ^ Information about how value should be represented in memory.
            -> Value arch ids tp
            -- ^ Value to write to memory
            -> AbsProcessorState (ArchReg arch) ids
addMemWrite :: forall arch ids (tp :: Type).
(RegisterInfo (ArchReg arch), MemWidth (ArchAddrWidth arch),
 HasCallStack) =>
AbsProcessorState (ArchReg arch) ids
-> Value arch ids (BVType (ArchAddrWidth arch))
-> MemRepr tp
-> Value arch ids tp
-> AbsProcessorState (ArchReg arch) ids
addMemWrite AbsProcessorState (ArchReg arch) ids
r Value arch ids (BVType (ArchAddrWidth arch))
a MemRepr tp
memRepr Value arch ids tp
v = do
  let v_abs :: ArchAbsValue arch tp
v_abs = AbsProcessorState (ArchReg arch) ids
-> Value arch ids tp -> ArchAbsValue arch tp
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg arch) ids
r Value arch ids tp
v
  case AbsProcessorState (ArchReg arch) ids
-> Value arch ids (BVType (ArchAddrWidth arch))
-> ArchAbsValue arch (BVType (ArchAddrWidth arch))
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg arch) ids
r Value arch ids (BVType (ArchAddrWidth arch))
a of
    -- (_,TopV) -> r
    -- We overwrite _some_ stack location.  An alternative would be to
    -- update everything with v.
    SomeStackOffset MemAddr (ArchAddrWidth arch)
_ -> do
      let cur_ip :: ArchAbsValue arch (BVType (ArchAddrWidth arch))
cur_ip = AbsProcessorState (ArchReg arch) ids
rAbsProcessorState (ArchReg arch) ids
-> Getting
     (RegState (ArchReg arch) (AbsValue (ArchAddrWidth arch)))
     (AbsProcessorState (ArchReg arch) ids)
     (RegState (ArchReg arch) (AbsValue (ArchAddrWidth arch)))
-> RegState (ArchReg arch) (AbsValue (ArchAddrWidth arch))
forall s a. s -> Getting a s a -> a
^.Getting
  (RegState (ArchReg arch) (AbsValue (ArchAddrWidth arch)))
  (AbsProcessorState (ArchReg arch) ids)
  (RegState (ArchReg arch) (AbsValue (ArchAddrWidth arch)))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
absInitialRegsRegState (ArchReg arch) (AbsValue (ArchAddrWidth arch))
-> Getting
     (ArchAbsValue arch (BVType (ArchAddrWidth arch)))
     (RegState (ArchReg arch) (AbsValue (ArchAddrWidth arch)))
     (ArchAbsValue arch (BVType (ArchAddrWidth arch)))
-> ArchAbsValue arch (BVType (ArchAddrWidth arch))
forall s a. s -> Getting a s a -> a
^.Getting
  (ArchAbsValue arch (BVType (ArchAddrWidth arch)))
  (RegState (ArchReg arch) (AbsValue (ArchAddrWidth arch)))
  (ArchAbsValue arch (BVType (ArchAddrWidth arch)))
Lens'
  (RegState (ArchReg arch) (AbsValue (ArchAddrWidth arch)))
  (ArchAbsValue arch (BVType (ArchAddrWidth arch)))
forall (r :: Type -> Type) (f :: Type -> Type).
RegisterInfo r =>
Lens' (RegState r f) (f (BVType (RegAddrWidth r)))
curIP
      DebugClass
-> String
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall a. (?loc::CallStack) => DebugClass -> String -> a -> a
debug DebugClass
DAbsInt (String
"addMemWrite: dropping stack at "
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (ArchAbsValue arch (BVType (ArchAddrWidth arch)) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann.
ArchAbsValue arch (BVType (ArchAddrWidth arch)) -> Doc ann
pretty ArchAbsValue arch (BVType (ArchAddrWidth arch))
cur_ip)
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" via " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Value arch ids (BVType (ArchAddrWidth arch)) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Value arch ids (BVType (ArchAddrWidth arch)) -> Doc ann
pretty Value arch ids (BVType (ArchAddrWidth arch))
a)
             String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" in SomeStackOffset case") (AbsProcessorState (ArchReg arch) ids
 -> AbsProcessorState (ArchReg arch) ids)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall a b. (a -> b) -> a -> b
$
        AbsProcessorState (ArchReg arch) ids
r AbsProcessorState (ArchReg arch) ids
-> (AbsProcessorState (ArchReg arch) ids
    -> AbsProcessorState (ArchReg arch) ids)
-> AbsProcessorState (ArchReg arch) ids
forall a b. a -> (a -> b) -> b
& (AbsBlockStack (ArchAddrWidth arch)
 -> Identity (AbsBlockStack (ArchAddrWidth arch)))
-> AbsProcessorState (ArchReg arch) ids
-> Identity (AbsProcessorState (ArchReg arch) ids)
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack ((AbsBlockStack (ArchAddrWidth arch)
  -> Identity (AbsBlockStack (ArchAddrWidth arch)))
 -> AbsProcessorState (ArchReg arch) ids
 -> Identity (AbsProcessorState (ArchReg arch) ids))
-> (AbsBlockStack (ArchAddrWidth arch)
    -> AbsBlockStack (ArchAddrWidth arch))
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ AbsBlockStack (ArchAddrWidth arch)
-> AbsBlockStack (ArchAddrWidth arch)
forall (w :: Natural). AbsBlockStack w -> AbsBlockStack w
pruneStack
    StackOffsetAbsVal MemAddr (ArchAddrWidth arch)
_ Int64
o ->
      let w :: Int64
          w :: Int64
w = Natural -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (MemRepr tp -> Natural
forall (tp :: Type). MemRepr tp -> Natural
memReprBytes MemRepr tp
memRepr)
          stk0 :: AbsBlockStack (ArchAddrWidth arch)
stk0 = AbsProcessorState (ArchReg arch) ids
rAbsProcessorState (ArchReg arch) ids
-> Getting
     (AbsBlockStack (ArchAddrWidth arch))
     (AbsProcessorState (ArchReg arch) ids)
     (AbsBlockStack (ArchAddrWidth arch))
-> AbsBlockStack (ArchAddrWidth arch)
forall s a. s -> Getting a s a -> a
^.Getting
  (AbsBlockStack (ArchAddrWidth arch))
  (AbsProcessorState (ArchReg arch) ids)
  (AbsBlockStack (ArchAddrWidth arch))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack
          -- Delete information about old assignment
          stk1 :: AbsBlockStack (ArchAddrWidth arch)
stk1 = Int64
-> Int64
-> AbsBlockStack (ArchAddrWidth arch)
-> AbsBlockStack (ArchAddrWidth arch)
forall (w :: Natural).
Int64 -> Int64 -> AbsBlockStack w -> AbsBlockStack w
deleteRange Int64
o (Int64
oInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
w) AbsBlockStack (ArchAddrWidth arch)
stk0
          -- Add information about new assignment
          stk2 :: AbsBlockStack (ArchAddrWidth arch)
stk2 | ArchAbsValue arch tp
v_abs ArchAbsValue arch tp -> ArchAbsValue arch tp -> Bool
forall a. Eq a => a -> a -> Bool
/= ArchAbsValue arch tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV = Int64
-> StackEntry (ArchAddrWidth arch)
-> AbsBlockStack (ArchAddrWidth arch)
-> AbsBlockStack (ArchAddrWidth arch)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int64
o (MemRepr tp
-> ArchAbsValue arch tp -> StackEntry (ArchAddrWidth arch)
forall (w :: Natural) (tp :: Type).
MemRepr tp -> AbsValue w tp -> StackEntry w
StackEntry MemRepr tp
memRepr ArchAbsValue arch tp
v_abs) AbsBlockStack (ArchAddrWidth arch)
stk1
               | Bool
otherwise = AbsBlockStack (ArchAddrWidth arch)
stk1
       in AbsProcessorState (ArchReg arch) ids
r AbsProcessorState (ArchReg arch) ids
-> (AbsProcessorState (ArchReg arch) ids
    -> AbsProcessorState (ArchReg arch) ids)
-> AbsProcessorState (ArchReg arch) ids
forall a b. a -> (a -> b) -> b
& (AbsBlockStack (ArchAddrWidth arch)
 -> Identity (AbsBlockStack (ArchAddrWidth arch)))
-> AbsProcessorState (ArchReg arch) ids
-> Identity (AbsProcessorState (ArchReg arch) ids)
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack ((AbsBlockStack (ArchAddrWidth arch)
  -> Identity (AbsBlockStack (ArchAddrWidth arch)))
 -> AbsProcessorState (ArchReg arch) ids
 -> Identity (AbsProcessorState (ArchReg arch) ids))
-> AbsBlockStack (ArchAddrWidth arch)
-> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids
forall s t a b. ASetter s t a b -> b -> s -> t
.~ AbsBlockStack (ArchAddrWidth arch)
stk2
    -- FIXME: nuke stack on an unknown address or Top?
    ArchAbsValue arch (BVType (ArchAddrWidth arch))
_ -> AbsProcessorState (ArchReg arch) ids
r


-- | Update the processor state with a potential memory write.
addCondMemWrite :: ( RegisterInfo r
                   , MemWidth (RegAddrWidth r)
                   , HasCallStack
                   , r ~ ArchReg arch
                   )
                => AbsProcessorState r ids
                -- ^ Current processor state.
                -> Value arch ids BoolType
                -- ^ Condition that holds if write is performed.
                -> Value arch ids (BVType (RegAddrWidth r))
                -- ^ Address that we are writing to.
                -> MemRepr tp
                -- ^ Information about how value should be represented in memory.
                -> Value arch ids tp
               -- ^ Value to write to memory
                -> AbsProcessorState r ids
addCondMemWrite :: forall (r :: Type -> Type) arch ids (tp :: Type).
(RegisterInfo r, MemWidth (RegAddrWidth r), HasCallStack,
 r ~ ArchReg arch) =>
AbsProcessorState r ids
-> Value arch ids BoolType
-> Value arch ids (BVType (RegAddrWidth r))
-> MemRepr tp
-> Value arch ids tp
-> AbsProcessorState r ids
addCondMemWrite AbsProcessorState r ids
r Value arch ids BoolType
_cond Value arch ids (BVType (RegAddrWidth r))
a MemRepr tp
memRepr Value arch ids tp
v = do
  case AbsProcessorState (ArchReg arch) ids
-> Value arch ids (BVType (RegAddrWidth r))
-> ArchAbsValue arch (BVType (RegAddrWidth r))
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState r ids
AbsProcessorState (ArchReg arch) ids
r Value arch ids (BVType (RegAddrWidth r))
a of
    -- (_,TopV) -> r
    -- We overwrite _some_ stack location.  An alternative would be to
    -- update everything with v.
    SomeStackOffset MemAddr (ArchAddrWidth arch)
_ -> do
      let cur_ip :: AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
cur_ip = AbsProcessorState r ids
rAbsProcessorState r ids
-> Getting
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsProcessorState r ids)
     (RegState r (AbsValue (RegAddrWidth r)))
-> RegState r (AbsValue (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.Getting
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsProcessorState r ids)
  (RegState r (AbsValue (RegAddrWidth r)))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(RegState r (AbsValue (RegAddrWidth r))
 -> f (RegState r (AbsValue (RegAddrWidth r))))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
absInitialRegsRegState r (AbsValue (RegAddrWidth r))
-> Getting
     (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)))
     (RegState r (AbsValue (RegAddrWidth r)))
     (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)))
-> AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
forall s a. s -> Getting a s a -> a
^.Getting
  (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)))
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)))
Lens'
  (RegState r (AbsValue (RegAddrWidth r)))
  (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)))
forall (r :: Type -> Type) (f :: Type -> Type).
RegisterInfo r =>
Lens' (RegState r f) (f (BVType (RegAddrWidth r)))
curIP
      DebugClass
-> String -> AbsProcessorState r ids -> AbsProcessorState r ids
forall a. (?loc::CallStack) => DebugClass -> String -> a -> a
debug DebugClass
DAbsInt (String
"addMemWrite: dropping stack at "
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann.
AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r)) -> Doc ann
pretty AbsValue (RegAddrWidth r) (BVType (RegAddrWidth r))
cur_ip)
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" via " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Value arch ids (BVType (RegAddrWidth r)) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Value arch ids (BVType (RegAddrWidth r)) -> Doc ann
pretty Value arch ids (BVType (RegAddrWidth r))
a)
             String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" in SomeStackOffset case") (AbsProcessorState r ids -> AbsProcessorState r ids)
-> AbsProcessorState r ids -> AbsProcessorState r ids
forall a b. (a -> b) -> a -> b
$
        AbsProcessorState r ids
r AbsProcessorState r ids
-> (AbsProcessorState r ids -> AbsProcessorState r ids)
-> AbsProcessorState r ids
forall a b. a -> (a -> b) -> b
& (AbsBlockStack (RegAddrWidth r)
 -> Identity (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> Identity (AbsProcessorState r ids)
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack ((AbsBlockStack (RegAddrWidth r)
  -> Identity (AbsBlockStack (RegAddrWidth r)))
 -> AbsProcessorState r ids -> Identity (AbsProcessorState r ids))
-> (AbsBlockStack (RegAddrWidth r)
    -> AbsBlockStack (RegAddrWidth r))
-> AbsProcessorState r ids
-> AbsProcessorState r ids
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ AbsBlockStack (RegAddrWidth r) -> AbsBlockStack (RegAddrWidth r)
forall (w :: Natural). AbsBlockStack w -> AbsBlockStack w
pruneStack
    StackOffsetAbsVal MemAddr (ArchAddrWidth arch)
_ Int64
o ->
      let w :: Int64
          w :: Int64
w = Natural -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (MemRepr tp -> Natural
forall (tp :: Type). MemRepr tp -> Natural
memReprBytes MemRepr tp
memRepr)
          stk0 :: AbsBlockStack (RegAddrWidth r)
stk0 = AbsProcessorState r ids
rAbsProcessorState r ids
-> Getting
     (AbsBlockStack (RegAddrWidth r))
     (AbsProcessorState r ids)
     (AbsBlockStack (RegAddrWidth r))
-> AbsBlockStack (RegAddrWidth r)
forall s a. s -> Getting a s a -> a
^.Getting
  (AbsBlockStack (RegAddrWidth r))
  (AbsProcessorState r ids)
  (AbsBlockStack (RegAddrWidth r))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack
          -- Delete information about old assignment
          stk1 :: AbsBlockStack (RegAddrWidth r)
stk1 = Int64
-> Int64
-> AbsBlockStack (RegAddrWidth r)
-> AbsBlockStack (RegAddrWidth r)
forall (w :: Natural).
Int64 -> Int64 -> AbsBlockStack w -> AbsBlockStack w
deleteRange Int64
o (Int64
oInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
w) AbsBlockStack (RegAddrWidth r)
stk0
          -- Add information about new assignment
          stk2 :: AbsBlockStack (RegAddrWidth r)
stk2
            | -- Skip if new value is top
              ArchAbsValue arch tp
v_abs <- AbsProcessorState (ArchReg arch) ids
-> Value arch ids tp -> ArchAbsValue arch tp
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState r ids
AbsProcessorState (ArchReg arch) ids
r Value arch ids tp
v
            , AbsValue (RegAddrWidth r) tp
ArchAbsValue arch tp
v_abs AbsValue (RegAddrWidth r) tp
-> AbsValue (RegAddrWidth r) tp -> Bool
forall a. Eq a => a -> a -> Bool
/= AbsValue (RegAddrWidth r) tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
              -- Lookup existing value at tack
            , AbsValue (RegAddrWidth r) tp
oldAbs <-
                case Int64
-> AbsBlockStack (RegAddrWidth r)
-> Maybe (StackEntry (RegAddrWidth r))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int64
o AbsBlockStack (RegAddrWidth r)
stk0 of
                  Just (StackEntry MemRepr tp
oldMemRepr AbsValue (RegAddrWidth r) tp
old)
                    | 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
memRepr MemRepr tp
oldMemRepr -> AbsValue (RegAddrWidth r) tp
AbsValue (RegAddrWidth r) tp
old
                  Maybe (StackEntry (RegAddrWidth r))
_ -> AbsValue (RegAddrWidth r) tp
forall d. AbsDomain d => d
top
              -- Computed merged value
            , AbsValue (RegAddrWidth r) tp
mergedValue <- AbsValue (RegAddrWidth r) tp
-> AbsValue (RegAddrWidth r) tp -> AbsValue (RegAddrWidth r) tp
forall d. AbsDomain d => d -> d -> d
lub AbsValue (RegAddrWidth r) tp
ArchAbsValue arch tp
v_abs AbsValue (RegAddrWidth r) tp
oldAbs
              -- Insert only non-top values
            , AbsValue (RegAddrWidth r) tp
mergedValue AbsValue (RegAddrWidth r) tp
-> AbsValue (RegAddrWidth r) tp -> Bool
forall a. Eq a => a -> a -> Bool
/= AbsValue (RegAddrWidth r) tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV =
               Int64
-> StackEntry (RegAddrWidth r)
-> AbsBlockStack (RegAddrWidth r)
-> AbsBlockStack (RegAddrWidth r)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int64
o (MemRepr tp
-> AbsValue (RegAddrWidth r) tp -> StackEntry (RegAddrWidth r)
forall (w :: Natural) (tp :: Type).
MemRepr tp -> AbsValue w tp -> StackEntry w
StackEntry MemRepr tp
memRepr AbsValue (RegAddrWidth r) tp
mergedValue) AbsBlockStack (RegAddrWidth r)
stk1
            | Bool
otherwise = AbsBlockStack (RegAddrWidth r)
stk1
       in AbsProcessorState r ids
r AbsProcessorState r ids
-> (AbsProcessorState r ids -> AbsProcessorState r ids)
-> AbsProcessorState r ids
forall a b. a -> (a -> b) -> b
& (AbsBlockStack (RegAddrWidth r)
 -> Identity (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> Identity (AbsProcessorState r ids)
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack ((AbsBlockStack (RegAddrWidth r)
  -> Identity (AbsBlockStack (RegAddrWidth r)))
 -> AbsProcessorState r ids -> Identity (AbsProcessorState r ids))
-> AbsBlockStack (RegAddrWidth r)
-> AbsProcessorState r ids
-> AbsProcessorState r ids
forall s t a b. ASetter s t a b -> b -> s -> t
.~ AbsBlockStack (RegAddrWidth r)
stk2
    -- FIXME: nuke stack on an unknown address or Top?
    ArchAbsValue arch (BVType (RegAddrWidth r))
_ -> AbsProcessorState r ids
r

-- | Returns true if return address is known to sit on stack.
absStackHasReturnAddr :: AbsBlockState r -> Bool
absStackHasReturnAddr :: forall (r :: Type -> Type). AbsBlockState r -> Bool
absStackHasReturnAddr AbsBlockState r
s = Maybe (StackEntry (RegAddrWidth r)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (StackEntry (RegAddrWidth r)) -> Bool)
-> Maybe (StackEntry (RegAddrWidth r)) -> Bool
forall a b. (a -> b) -> a -> b
$ (StackEntry (RegAddrWidth r) -> Bool)
-> [StackEntry (RegAddrWidth r)]
-> Maybe (StackEntry (RegAddrWidth r))
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
find StackEntry (RegAddrWidth r) -> Bool
forall {w :: Natural}. StackEntry w -> Bool
isReturnAddr (Map Int64 (StackEntry (RegAddrWidth r))
-> [StackEntry (RegAddrWidth r)]
forall k a. Map k a -> [a]
Map.elems (AbsBlockState r -> Map Int64 (StackEntry (RegAddrWidth r))
forall (r :: Type -> Type).
AbsBlockState r -> AbsBlockStack (RegAddrWidth r)
startAbsStack AbsBlockState r
s))
  where isReturnAddr :: StackEntry w -> Bool
isReturnAddr (StackEntry MemRepr tp
_ AbsValue w tp
ReturnAddr) = Bool
True
        isReturnAddr StackEntry w
_ = Bool
False

-- | Return state for after value has run.
finalAbsBlockState :: forall a ids
                   .  ( RegisterInfo (ArchReg a))
                   => AbsProcessorState (ArchReg a) ids
                   -> RegState (ArchReg a) (Value a ids)
                      -- ^  Final values for abstract processor state
                   -> AbsBlockState (ArchReg a)
finalAbsBlockState :: forall a ids.
RegisterInfo (ArchReg a) =>
AbsProcessorState (ArchReg a) ids
-> RegState (ArchReg a) (Value a ids) -> AbsBlockState (ArchReg a)
finalAbsBlockState AbsProcessorState (ArchReg a) ids
c RegState (ArchReg a) (Value a ids)
regs =
  let transferReg :: ArchReg a tp -> ArchAbsValue a tp
      transferReg :: forall (tp :: Type). ArchReg a tp -> ArchAbsValue a tp
transferReg ArchReg a tp
r = AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> AbsValue (RegAddrWidth (ArchReg a)) tp
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg a) ids
c (RegState (ArchReg a) (Value a ids)
regsRegState (ArchReg a) (Value a ids)
-> Getting
     (Value a ids tp)
     (RegState (ArchReg a) (Value a ids))
     (Value a ids tp)
-> Value a ids tp
forall s a. s -> Getting a s a -> a
^.ArchReg a tp
-> Lens' (RegState (ArchReg a) (Value a ids)) (Value a ids tp)
forall {k} (r :: k -> Type) (f :: k -> Type) (tp :: k).
OrdF r =>
r tp -> Lens' (RegState r f) (f tp)
boundValue ArchReg a tp
r)
   in AbsBlockState { _absRegState :: RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a)))
_absRegState = (forall (tp :: Type). ArchReg a tp -> ArchAbsValue a tp)
-> RegState (ArchReg a) (AbsValue (RegAddrWidth (ArchReg a)))
forall (r :: Type -> Type) (f :: Type -> Type).
RegisterInfo r =>
(forall (tp :: Type). r tp -> f tp) -> RegState r f
mkRegState ArchReg a tp -> ArchAbsValue a tp
forall (tp :: Type). ArchReg a tp -> ArchAbsValue a tp
transferReg
                    , startAbsStack :: AbsBlockStack (RegAddrWidth (ArchReg a))
startAbsStack = AbsProcessorState (ArchReg a) ids
cAbsProcessorState (ArchReg a) ids
-> Getting
     (AbsBlockStack (RegAddrWidth (ArchReg a)))
     (AbsProcessorState (ArchReg a) ids)
     (AbsBlockStack (RegAddrWidth (ArchReg a)))
-> AbsBlockStack (RegAddrWidth (ArchReg a))
forall s a. s -> Getting a s a -> a
^.Getting
  (AbsBlockStack (RegAddrWidth (ArchReg a)))
  (AbsProcessorState (ArchReg a) ids)
  (AbsBlockStack (RegAddrWidth (ArchReg a)))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack
                    }

------------------------------------------------------------------------
-- Transfer functions

transferApp :: forall a ids tp
            .  ( RegisterInfo (ArchReg a)
               , HasCallStack
               )
            => AbsProcessorState (ArchReg a) ids
            -> App (Value a ids) tp
            -> ArchAbsValue a tp
transferApp :: forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> App (Value a ids) tp -> ArchAbsValue a tp
transferApp AbsProcessorState (ArchReg a) ids
r App (Value a ids) tp
a = do
  let t :: Value a ids utp -> ArchAbsValue a utp
      t :: forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t = AbsProcessorState (ArchReg a) ids
-> Value a ids utp -> AbsValue (RegAddrWidth (ArchReg a)) utp
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg a) ids
r
  case App (Value a ids) tp
a of
    Trunc Value a ids (BVType m)
v NatRepr n
w -> AbsValue (RegAddrWidth (ArchReg a)) (BVType m)
-> NatRepr n -> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (w :: Natural) (v :: Natural) (u :: Natural).
(MemWidth w, (v + 1) <= u) =>
AbsValue w (BVType u) -> NatRepr v -> AbsValue w (BVType v)
trunc (Value a ids (BVType m)
-> AbsValue (RegAddrWidth (ArchReg a)) (BVType m)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids (BVType m)
v) NatRepr n
w
    UExt  Value a ids (BVType m)
v NatRepr n
w -> AbsValue (RegAddrWidth (ArchReg a)) (BVType m)
-> NatRepr n -> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (u :: Natural) (v :: Natural) (w :: Natural).
((u + 1) <= v, MemWidth w) =>
AbsValue w (BVType u) -> NatRepr v -> AbsValue w (BVType v)
uext  (Value a ids (BVType m)
-> AbsValue (RegAddrWidth (ArchReg a)) (BVType m)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids (BVType m)
v) NatRepr n
w
    BVAdd NatRepr n
w Value a ids ('BVType n)
x Value a ids ('BVType n)
y -> NatRepr n
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bvadd NatRepr n
w (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
x) (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
y)
    BVAdc NatRepr n
w Value a ids ('BVType n)
x Value a ids ('BVType n)
y Value a ids BoolType
c -> NatRepr n
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) BoolType
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w BoolType
-> AbsValue w (BVType u)
bvadc NatRepr n
w (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
x) (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
y) (Value a ids BoolType
-> AbsValue (RegAddrWidth (ArchReg a)) BoolType
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids BoolType
c)
    BVSub NatRepr n
w Value a ids ('BVType n)
x Value a ids ('BVType n)
y -> Memory (RegAddrWidth (ArchReg a))
-> NatRepr n
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (w :: Natural) (u :: Natural).
MemWidth w =>
Memory w
-> NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bvsub (AbsProcessorState (ArchReg a) ids
-> Memory (RegAddrWidth (ArchReg a))
forall (r :: Type -> Type) ids.
AbsProcessorState r ids -> Memory (RegAddrWidth r)
absMem AbsProcessorState (ArchReg a) ids
r) NatRepr n
w (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
x) (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
y)
    BVSbb NatRepr n
w Value a ids ('BVType n)
x Value a ids ('BVType n)
y Value a ids BoolType
b -> Memory (RegAddrWidth (ArchReg a))
-> NatRepr n
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) BoolType
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (w :: Natural) (u :: Natural).
MemWidth w =>
Memory w
-> NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w BoolType
-> AbsValue w (BVType u)
bvsbb (AbsProcessorState (ArchReg a) ids
-> Memory (RegAddrWidth (ArchReg a))
forall (r :: Type -> Type) ids.
AbsProcessorState r ids -> Memory (RegAddrWidth r)
absMem AbsProcessorState (ArchReg a) ids
r) NatRepr n
w (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
x) (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
y) (Value a ids BoolType
-> AbsValue (RegAddrWidth (ArchReg a)) BoolType
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids BoolType
b)
    BVMul NatRepr n
w Value a ids ('BVType n)
x Value a ids ('BVType n)
y -> NatRepr n
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (w :: Natural) (u :: Natural).
MemWidth w =>
NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bvmul NatRepr n
w (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
x) (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
y)
    BVAnd NatRepr n
w Value a ids ('BVType n)
x Value a ids ('BVType n)
y -> (Integer -> Integer -> Integer)
-> NatRepr n
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (w :: Natural) (u :: Natural).
MemWidth w =>
(Integer -> Integer -> Integer)
-> NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bitop Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.&.) NatRepr n
w (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
x) (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
y)
    BVOr NatRepr n
w Value a ids ('BVType n)
x Value a ids ('BVType n)
y  -> (Integer -> Integer -> Integer)
-> NatRepr n
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (w :: Natural) (u :: Natural).
MemWidth w =>
(Integer -> Integer -> Integer)
-> NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bitop Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
(.|.) NatRepr n
w (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
x) (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
y)
    BVShl NatRepr n
w Value a ids ('BVType n)
v Value a ids ('BVType n)
s -> (Integer -> Integer -> Integer)
-> NatRepr n
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (w :: Natural) (u :: Natural).
MemWidth w =>
(Integer -> Integer -> Integer)
-> NatRepr u
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
-> AbsValue w (BVType u)
bitop (\Integer
x1 Integer
x2 -> Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
x1 (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
x2)) NatRepr n
w (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
v) (Value a ids ('BVType n)
-> AbsValue (RegAddrWidth (ArchReg a)) ('BVType n)
forall (utp :: Type). Value a ids utp -> ArchAbsValue a utp
t Value a ids ('BVType n)
s)
    App (Value a ids) tp
_ -> ArchAbsValue a tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV


-- | This updates the registers after a call has been performed.
absEvalCall :: forall arch ids
                 .  ( RegisterInfo (ArchReg arch)
                    )
                 => CallParams (ArchReg arch)
                    -- ^ Configuration
                 -> AbsProcessorState (ArchReg arch) ids
                    -- ^ State before call
                 -> RegState (ArchReg arch) (Value arch ids)
                 -> ArchSegmentOff arch
                    -- ^ Address we are jumping to
                 -> AbsBlockState (ArchReg arch)
absEvalCall :: forall arch ids.
RegisterInfo (ArchReg arch) =>
CallParams (ArchReg arch)
-> AbsProcessorState (ArchReg arch) ids
-> RegState (ArchReg arch) (Value arch ids)
-> ArchSegmentOff arch
-> AbsBlockState (ArchReg arch)
absEvalCall CallParams (ArchReg arch)
params AbsProcessorState (ArchReg arch) ids
ab0 RegState (ArchReg arch) (Value arch ids)
regs ArchSegmentOff arch
addr =
  let spAbstractVal :: ArchAbsValue arch (BVType (RegAddrWidth (ArchReg arch)))
spAbstractVal = AbsProcessorState (ArchReg arch) ids
-> Value arch ids (BVType (RegAddrWidth (ArchReg arch)))
-> ArchAbsValue arch (BVType (RegAddrWidth (ArchReg arch)))
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg arch) ids
ab0 (RegState (ArchReg arch) (Value arch ids)
regsRegState (ArchReg arch) (Value arch ids)
-> Getting
     (Value arch ids (BVType (RegAddrWidth (ArchReg arch))))
     (RegState (ArchReg arch) (Value arch ids))
     (Value arch ids (BVType (RegAddrWidth (ArchReg arch))))
-> Value arch ids (BVType (RegAddrWidth (ArchReg arch)))
forall s a. s -> Getting a s a -> a
^.ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
-> Lens'
     (RegState (ArchReg arch) (Value arch ids))
     (Value arch ids (BVType (RegAddrWidth (ArchReg arch))))
forall {k} (r :: k -> Type) (f :: k -> Type) (tp :: k).
OrdF r =>
r tp -> Lens' (RegState r f) (f tp)
boundValue ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
sp_reg)
      regFn :: ArchReg arch tp
            -> AbsValue (ArchAddrWidth arch) tp
      regFn :: forall (tp :: Type).
ArchReg arch tp -> AbsValue (RegAddrWidth (ArchReg arch)) tp
regFn ArchReg arch tp
r
        -- We set IPReg
        | 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 =
            ArchSegmentOff arch
-> ArchAbsValue arch (BVType (RegAddrWidth (ArchReg arch)))
forall (w :: Natural). MemSegmentOff w -> AbsValue w (BVType w)
concreteCodeAddr ArchSegmentOff arch
addr
        | 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 =
            NatRepr (RegAddrWidth (ArchReg arch))
-> ArchAbsValue arch (BVType (RegAddrWidth (ArchReg arch)))
-> Integer
-> ArchAbsValue arch (BVType (RegAddrWidth (ArchReg arch)))
forall (w :: Natural) (u :: Natural).
NatRepr u
-> AbsValue w (BVType u) -> Integer -> AbsValue w (BVType u)
bvinc (ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
-> NatRepr (RegAddrWidth (ArchReg arch))
forall (f :: Type -> Type) (w :: Natural).
HasRepr f TypeRepr =>
f (BVType w) -> NatRepr w
typeWidth ArchReg arch tp
ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
r) ArchAbsValue arch (BVType (RegAddrWidth (ArchReg arch)))
spAbstractVal (CallParams (ArchReg arch) -> Integer
forall (r :: Type -> Type). CallParams r -> Integer
postCallStackDelta CallParams (ArchReg arch)
params)
          -- Copy callee saved registers
        | 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 =
            AbsProcessorState (ArchReg arch) ids
-> Value arch ids tp -> AbsValue (RegAddrWidth (ArchReg arch)) tp
forall a ids (tp :: Type).
(RegisterInfo (ArchReg a), HasCallStack) =>
AbsProcessorState (ArchReg a) ids
-> Value a ids tp -> ArchAbsValue a tp
transferValue AbsProcessorState (ArchReg arch) ids
ab0 (RegState (ArchReg arch) (Value arch ids)
regsRegState (ArchReg arch) (Value arch ids)
-> Getting
     (Value arch ids tp)
     (RegState (ArchReg arch) (Value arch ids))
     (Value arch ids tp)
-> Value arch ids tp
forall s a. s -> Getting a s a -> a
^.ArchReg arch tp
-> Lens'
     (RegState (ArchReg arch) (Value arch ids)) (Value arch ids tp)
forall {k} (r :: k -> Type) (f :: k -> Type) (tp :: k).
OrdF r =>
r tp -> Lens' (RegState r f) (f tp)
boundValue ArchReg arch tp
r)
          -- We know nothing about other registers.
        | Bool
otherwise =
            AbsValue (RegAddrWidth (ArchReg arch)) tp
forall (w :: Natural) (tp :: Type). AbsValue w tp
TopV
   in AbsBlockState { _absRegState :: RegState (ArchReg arch) (AbsValue (RegAddrWidth (ArchReg arch)))
_absRegState = (forall (tp :: Type).
 ArchReg arch tp -> AbsValue (RegAddrWidth (ArchReg arch)) tp)
-> RegState (ArchReg arch) (AbsValue (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type) (f :: Type -> Type).
RegisterInfo r =>
(forall (tp :: Type). r tp -> f tp) -> RegState r f
mkRegState ArchReg arch tp -> AbsValue (RegAddrWidth (ArchReg arch)) tp
forall (tp :: Type).
ArchReg arch tp -> AbsValue (RegAddrWidth (ArchReg arch)) tp
regFn
                      -- Drop return address from stack.
                    , startAbsStack :: AbsBlockStack (RegAddrWidth (ArchReg arch))
startAbsStack =
                        case ArchAbsValue arch (BVType (RegAddrWidth (ArchReg arch)))
spAbstractVal of
                          StackOffsetAbsVal MemAddr (RegAddrWidth (ArchReg arch))
_ Int64
spOff
                            | CallParams (ArchReg arch) -> Bool
forall (r :: Type -> Type). CallParams r -> Bool
stackGrowsDown CallParams (ArchReg arch)
params ->
                                let newOff :: Int64
newOff = Int64
spOff Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Integer -> Int64
forall a. Num a => Integer -> a
fromInteger (CallParams (ArchReg arch) -> Integer
forall (r :: Type -> Type). CallParams r -> Integer
postCallStackDelta CallParams (ArchReg arch)
params)
                                    -- Keep entries whose low address is above new stack offset.
                                    p :: Int64 -> StackEntry (RegAddrWidth (ArchReg arch)) -> Bool
p Int64
o StackEntry (RegAddrWidth (ArchReg arch))
_v = Int64
o Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int64
newOff
                                    -- Keep entries at offsets above return address.
                                 in (Int64 -> StackEntry (RegAddrWidth (ArchReg arch)) -> Bool)
-> AbsBlockStack (RegAddrWidth (ArchReg arch))
-> AbsBlockStack (RegAddrWidth (ArchReg arch))
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey Int64 -> StackEntry (RegAddrWidth (ArchReg arch)) -> Bool
p (AbsProcessorState (ArchReg arch) ids
ab0AbsProcessorState (ArchReg arch) ids
-> Getting
     (AbsBlockStack (RegAddrWidth (ArchReg arch)))
     (AbsProcessorState (ArchReg arch) ids)
     (AbsBlockStack (RegAddrWidth (ArchReg arch)))
-> AbsBlockStack (RegAddrWidth (ArchReg arch))
forall s a. s -> Getting a s a -> a
^.Getting
  (AbsBlockStack (RegAddrWidth (ArchReg arch)))
  (AbsProcessorState (ArchReg arch) ids)
  (AbsBlockStack (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack)
                            | Bool
otherwise ->
                                let newOff :: Int64
newOff = Int64
spOff Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Integer -> Int64
forall a. Num a => Integer -> a
fromInteger (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
                                    p :: Int64 -> StackEntry (RegAddrWidth (ArchReg arch)) -> Bool
p Int64
o (StackEntry MemRepr tp
r AbsValue (RegAddrWidth (ArchReg arch)) tp
_) = Int64
o Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Natural -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (MemRepr tp -> Natural
forall (tp :: Type). MemRepr tp -> Natural
memReprBytes MemRepr tp
r) Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Int64
newOff
                                 in (Int64 -> StackEntry (RegAddrWidth (ArchReg arch)) -> Bool)
-> AbsBlockStack (RegAddrWidth (ArchReg arch))
-> AbsBlockStack (RegAddrWidth (ArchReg arch))
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey Int64 -> StackEntry (RegAddrWidth (ArchReg arch)) -> Bool
p (AbsProcessorState (ArchReg arch) ids
ab0AbsProcessorState (ArchReg arch) ids
-> Getting
     (AbsBlockStack (RegAddrWidth (ArchReg arch)))
     (AbsProcessorState (ArchReg arch) ids)
     (AbsBlockStack (RegAddrWidth (ArchReg arch)))
-> AbsBlockStack (RegAddrWidth (ArchReg arch))
forall s a. s -> Getting a s a -> a
^.Getting
  (AbsBlockStack (RegAddrWidth (ArchReg arch)))
  (AbsProcessorState (ArchReg arch) ids)
  (AbsBlockStack (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type) ids (f :: Type -> Type).
Functor f =>
(AbsBlockStack (RegAddrWidth r)
 -> f (AbsBlockStack (RegAddrWidth r)))
-> AbsProcessorState r ids -> f (AbsProcessorState r ids)
curAbsStack)
                          ArchAbsValue arch (BVType (RegAddrWidth (ArchReg arch)))
_ -> AbsBlockStack (RegAddrWidth (ArchReg arch))
forall k a. Map k a
Map.empty
                    }