{-|
Defines data types needed to represent values, assignments, and statements from Machine code.

This is a low-level CFG representation where the entire program is a
single CFG.
-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Data.Macaw.CFG.Core
  ( -- * Stmt level declarations
    Stmt(..)
  , Assignment(..)
  , AssignId(..)
    -- * Value
  , Value(..)
  , CValue(..)
  , pattern BoolValue
  , pattern BVValue
  , pattern RelocatableValue
  , pattern SymbolValue
  , BVValue
  , valueAsApp
  , valueAsArchFn
  , valueAsRhs
  , valueAsMemAddr
  , valueAsSegmentOff
  , valueAsStaticMultiplication
  , StackOffsetView(..)
  , appAsStackOffset
  , asBaseOffset
  , asInt64Constant
  , IPAlignment(..)
  , mkLit
  , bvValue
  , ppValueAssignments
  , ppValueAssignmentList
  -- * RegState
  , RegState
  , regStateMap
  , getBoundValue
  , boundValue
  , cmpRegState
  , curIP
  , mkRegState
  , mkRegStateM
  , mapRegsWith
  , traverseRegsWith
  , traverseRegsWith_
  , zipWithRegState
  , ppRegMap
  -- * Pretty printing
  , ppAssignId
  , ppValue
  , ppStmt
  , PrettyF(..)
  , ArchConstraints
  , PrettyRegValue(..)
  , IsArchFn(..)
  , IsArchStmt(..)
  , IsArchTermStmt(..)
  , collectValueRep
  , ppValueAssignments'
  , DocF
    -- * Utilities
  , addrWidthTypeRepr
    -- * RegisterInfo
  , RegisterInfo(..)
  , asStackAddrOffset
    -- * References
  , refsInValue
    -- ** Synonyms
  , ArchAddrValue
  , ArchSegmentOff
  , ArchBlockPrecond
  , Data.Parameterized.TraversableFC.FoldableFC(..)
  , module Data.Macaw.CFG.AssignRhs
  , module Data.Macaw.Utils.Pretty
  ) where

import           Control.Lens
import           Control.Monad (when)
import           Control.Monad.State.Strict (MonadState(..), State, gets, modify, runState)
import           Data.Bits
import           Data.Int (Int64)
import qualified Data.Kind as Kind
import           Data.Maybe (isNothing, catMaybes)
import           Data.Parameterized.Classes
import           Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableF
import           Data.Parameterized.TraversableFC (FoldableFC(..))
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Text (Text)
import           Numeric (showHex)
import           Numeric.Natural (Natural)
import           Prettyprinter as PP

import           Data.Macaw.CFG.App
import           Data.Macaw.CFG.AssignRhs
import           Data.Macaw.Memory
import           Data.Macaw.Types
import           Data.Macaw.Utils.Pretty

-- | This family maps architecture parameters to information needed to
-- successfully translate machine code into Macaw CFGs.
--
-- This is currently used for registers values that are required to be
-- known constants at translation time.  For example, on X86_64, due to
-- aliasing between the FPU and MMX registers, we require that the
-- floating point stack value is known at translation time so that
-- we do not need to check which register is modified when pushing or
-- poping from the x86 stack.
--
-- If no preconditions are needed, this can just be set to the unit type.
type family ArchBlockPrecond (arch :: Kind.Type) :: Kind.Type

-- | A pair containing a segment and valid offset within the segment.
type ArchSegmentOff arch = MemSegmentOff (ArchAddrWidth arch)

-- Note:
-- The declarations in this file follow a top-down order, so the top-level
-- definitions should be first.

type Prec = Int

colonPrec :: Prec
colonPrec :: Prec
colonPrec = Prec
7

plusPrec :: Prec
plusPrec :: Prec
plusPrec = Prec
6

-- | Class for pretty printing with a precedence field.
class PrettyPrec v where
  prettyPrec :: Int -> v -> Doc ann

-- | Pretty print over all instances of a type.
class PrettyF (f :: k -> Kind.Type) where
  prettyF :: f tp -> Doc ann

-- | Pretty print a document with parens if condition is true
parenIf :: Bool -> Doc ann -> Doc ann
parenIf :: forall ann. Bool -> Doc ann -> Doc ann
parenIf Bool
True Doc ann
d = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens Doc ann
d
parenIf Bool
False Doc ann
d = Doc ann
d

bracketsep :: [Doc ann] -> Doc ann
bracketsep :: forall ann. [Doc ann] -> Doc ann
bracketsep [] = Doc ann
"{}"
bracketsep (Doc ann
h:[Doc ann]
l) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$
  [Doc ann
forall ann. Doc ann
lbrace Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
h]
  [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ (Doc ann -> Doc ann) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Doc ann
forall ann. Doc ann
comma Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) [Doc ann]
l
  [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [Doc ann
forall ann. Doc ann
rbrace]

-- | A type repr for the address width
addrWidthTypeRepr :: AddrWidthRepr w -> TypeRepr (BVType w)
addrWidthTypeRepr :: forall (w :: Natural). AddrWidthRepr w -> TypeRepr (BVType w)
addrWidthTypeRepr AddrWidthRepr w
Addr32 = NatRepr w -> TypeRepr ('BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr w
forall (n :: Natural). KnownNat n => NatRepr n
knownNat
addrWidthTypeRepr AddrWidthRepr w
Addr64 = NatRepr w -> TypeRepr ('BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr w
forall (n :: Natural). KnownNat n => NatRepr n
knownNat

------------------------------------------------------------------------
-- AssignId

-- | An 'AssignId' is a unique identifier used to identify assignment
-- statements, in a manner similar to SSA (single static assignment)
-- form. 'AssignId's are typed, and also include a type variable @ids@
-- that intuitively denotes the set of identifiers from which they are
-- drawn.
newtype AssignId (ids :: Kind.Type) (tp :: Type) = AssignId (Nonce ids tp)

ppAssignId :: AssignId ids tp -> Doc ann
ppAssignId :: forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId (AssignId Nonce ids tp
w) = Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'r' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nonce ids tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue Nonce ids tp
w)

instance Eq (AssignId ids tp) where
  AssignId Nonce ids tp
id1 == :: AssignId ids tp -> AssignId ids tp -> Bool
== AssignId Nonce ids tp
id2 = Nonce ids tp
id1 Nonce ids tp -> Nonce ids tp -> Bool
forall a. Eq a => a -> a -> Bool
== Nonce ids tp
id2

instance TestEquality (AssignId ids) where
  testEquality :: forall (a :: Type) (b :: Type).
AssignId ids a -> AssignId ids b -> Maybe (a :~: b)
testEquality (AssignId Nonce ids a
id1) (AssignId Nonce ids b
id2) = Nonce ids a -> Nonce ids b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
Nonce ids a -> Nonce ids b -> Maybe (a :~: b)
testEquality Nonce ids a
id1 Nonce ids b
id2

instance Ord (AssignId ids tp) where
  compare :: AssignId ids tp -> AssignId ids tp -> Ordering
compare (AssignId Nonce ids tp
x) (AssignId Nonce ids tp
y) = Nonce ids tp -> Nonce ids tp -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Nonce ids tp
x Nonce ids tp
y

instance OrdF (AssignId ids) where
  compareF :: forall (x :: Type) (y :: Type).
AssignId ids x -> AssignId ids y -> OrderingF x y
compareF (AssignId Nonce ids x
id1) (AssignId Nonce ids y
id2) = Nonce ids x -> Nonce ids y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
Nonce ids x -> Nonce ids y -> OrderingF x y
compareF Nonce ids x
id1 Nonce ids y
id2

instance Show (AssignId ids tp) where
  show :: AssignId ids tp -> String
show (AssignId Nonce ids tp
n) = Word64 -> String
forall a. Show a => a -> String
show (Nonce ids tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue Nonce ids tp
n)

instance ShowF (AssignId ids) where
  showF :: forall (tp :: Type). AssignId ids tp -> String
showF = AssignId ids tp -> String
forall a. Show a => a -> String
show

------------------------------------------------------------------------
-- CValue

-- | A constant whose value does not change during execution.
data CValue arch tp where
  -- | A constant bitvector
  --
  -- The integer should be between 0 and 2^n-1.
  BVCValue :: (1 <= n) => !(NatRepr n) -> !Integer -> CValue arch (BVType n)
  -- | A constant Boolean
  BoolCValue :: !Bool -> CValue arch BoolType
  -- | A memory address
  RelocatableCValue :: !(AddrWidthRepr (ArchAddrWidth arch))
                    -> !(MemAddr (ArchAddrWidth arch))
                    -> CValue arch (BVType (ArchAddrWidth arch))
  -- | This denotes the address of a symbol identifier in the binary.
  --
  -- This appears when dealing with relocations.
  SymbolCValue :: !(AddrWidthRepr (ArchAddrWidth arch))
               -> !SymbolIdentifier
               -> CValue arch (BVType (ArchAddrWidth arch))

instance TestEquality (CValue arch) where
  testEquality :: forall (a :: Type) (b :: Type).
CValue arch a -> CValue arch b -> Maybe (a :~: b)
testEquality (BVCValue NatRepr n
xw Integer
xi) (BVCValue NatRepr n
yw Integer
yi) = do
    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
xw NatRepr n
yw
    if Integer
xi Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
yi then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  testEquality (BoolCValue Bool
x) (BoolCValue Bool
y) = do
    if Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
y then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  testEquality (RelocatableCValue AddrWidthRepr (ArchAddrWidth arch)
_ MemAddr (ArchAddrWidth arch)
x) (RelocatableCValue AddrWidthRepr (ArchAddrWidth arch)
_ MemAddr (ArchAddrWidth arch)
y) = do
    if MemAddr (ArchAddrWidth arch)
x MemAddr (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Bool
forall a. Eq a => a -> a -> Bool
== MemAddr (ArchAddrWidth arch)
y then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  testEquality (SymbolCValue AddrWidthRepr (ArchAddrWidth arch)
_ SymbolIdentifier
x) (SymbolCValue AddrWidthRepr (ArchAddrWidth arch)
_ SymbolIdentifier
y) = do
    if SymbolIdentifier
x SymbolIdentifier -> SymbolIdentifier -> Bool
forall a. Eq a => a -> a -> Bool
== SymbolIdentifier
y then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing
  testEquality CValue arch a
_ CValue arch b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance Eq (CValue arch tp) where
  CValue arch tp
a == :: CValue arch tp -> CValue arch tp -> Bool
== CValue arch tp
b = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (CValue arch tp -> CValue arch 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).
CValue arch a -> CValue arch b -> Maybe (a :~: b)
testEquality CValue arch tp
a CValue arch tp
b)

instance OrdF (CValue arch) where
  compareF :: forall (x :: Type) (y :: Type).
CValue arch x -> CValue arch y -> OrderingF x y
compareF (BoolCValue Bool
x) (BoolCValue Bool
y) = Ordering -> OrderingF x x
forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Bool
x Bool
y)
  compareF BoolCValue{} CValue arch y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF CValue arch x
_ BoolCValue{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (BVCValue NatRepr n
wx Integer
vx) (BVCValue NatRepr n
wy Integer
vy) =
    case NatRepr n -> NatRepr n -> OrderingF n n
forall (x :: Natural) (y :: Natural).
NatRepr x -> NatRepr y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF NatRepr n
wx NatRepr n
wy of
      OrderingF n n
LTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
      OrderingF n n
EQF -> Ordering -> OrderingF x x
forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
vx Integer
vy)
      OrderingF n n
GTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
  compareF BVCValue{} CValue arch y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF CValue arch x
_ BVCValue{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (RelocatableCValue AddrWidthRepr (ArchAddrWidth arch)
_ MemAddr (ArchAddrWidth arch)
x) (RelocatableCValue AddrWidthRepr (ArchAddrWidth arch)
_ MemAddr (ArchAddrWidth arch)
y) =
    Ordering -> OrderingF x x
forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (MemAddr (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare MemAddr (ArchAddrWidth arch)
x MemAddr (ArchAddrWidth arch)
y)
  compareF RelocatableCValue{} CValue arch y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF CValue arch x
_ RelocatableCValue{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (SymbolCValue AddrWidthRepr (ArchAddrWidth arch)
_ SymbolIdentifier
x) (SymbolCValue AddrWidthRepr (ArchAddrWidth arch)
_ SymbolIdentifier
y) =
    Ordering -> OrderingF x x
forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (SymbolIdentifier -> SymbolIdentifier -> Ordering
forall a. Ord a => a -> a -> Ordering
compare SymbolIdentifier
x SymbolIdentifier
y)

instance HasRepr (CValue arch) TypeRepr where
  typeRepr :: forall (tp :: Type). CValue arch tp -> TypeRepr tp
typeRepr (BoolCValue Bool
_) = TypeRepr tp
TypeRepr BoolType
BoolTypeRepr
  typeRepr (BVCValue NatRepr n
w Integer
_) = NatRepr n -> TypeRepr ('BVType n)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr n
w
  typeRepr (RelocatableCValue AddrWidthRepr (ArchAddrWidth arch)
w MemAddr (ArchAddrWidth arch)
_) = AddrWidthRepr (ArchAddrWidth arch)
-> TypeRepr ('BVType (ArchAddrWidth arch))
forall (w :: Natural). AddrWidthRepr w -> TypeRepr (BVType w)
addrWidthTypeRepr AddrWidthRepr (ArchAddrWidth arch)
w
  typeRepr (SymbolCValue AddrWidthRepr (ArchAddrWidth arch)
w SymbolIdentifier
_)      = AddrWidthRepr (ArchAddrWidth arch)
-> TypeRepr ('BVType (ArchAddrWidth arch))
forall (w :: Natural). AddrWidthRepr w -> TypeRepr (BVType w)
addrWidthTypeRepr AddrWidthRepr (ArchAddrWidth arch)
w

instance Hashable (CValue arch tp) where
  hashWithSalt :: Prec -> CValue arch tp -> Prec
hashWithSalt Prec
s CValue arch tp
cv =
    case CValue arch tp
cv of
      BVCValue NatRepr n
w Integer
i          -> Prec
s Prec -> Prec -> Prec
forall a. Hashable a => Prec -> a -> Prec
`hashWithSalt` (Prec
0::Int) Prec -> NatRepr n -> Prec
forall a. Hashable a => Prec -> a -> Prec
`hashWithSalt` NatRepr n
w Prec -> Integer -> Prec
forall a. Hashable a => Prec -> a -> Prec
`hashWithSalt` Integer
i
      BoolCValue Bool
b          -> Prec
s Prec -> Prec -> Prec
forall a. Hashable a => Prec -> a -> Prec
`hashWithSalt` (Prec
1::Int) Prec -> Bool -> Prec
forall a. Hashable a => Prec -> a -> Prec
`hashWithSalt` Bool
b
      RelocatableCValue AddrWidthRepr (ArchAddrWidth arch)
_ MemAddr (ArchAddrWidth arch)
a -> Prec
s Prec -> Prec -> Prec
forall a. Hashable a => Prec -> a -> Prec
`hashWithSalt` (Prec
2::Int) Prec -> MemAddr (ArchAddrWidth arch) -> Prec
forall a. Hashable a => Prec -> a -> Prec
`hashWithSalt` MemAddr (ArchAddrWidth arch)
a
      SymbolCValue AddrWidthRepr (ArchAddrWidth arch)
_ SymbolIdentifier
sym    -> Prec
s Prec -> Prec -> Prec
forall a. Hashable a => Prec -> a -> Prec
`hashWithSalt` (Prec
3::Int) Prec -> SymbolIdentifier -> Prec
forall a. Hashable a => Prec -> a -> Prec
`hashWithSalt` SymbolIdentifier
sym

instance HashableF (CValue arch) where
  hashWithSaltF :: forall (tp :: Type). Prec -> CValue arch tp -> Prec
hashWithSaltF = Prec -> CValue arch tp -> Prec
forall a. Hashable a => Prec -> a -> Prec
hashWithSalt

ppLit :: NatRepr n -> Integer -> Doc ann
ppLit :: forall (n :: Natural) ann. NatRepr n -> Integer -> Doc ann
ppLit NatRepr n
w Integer
i
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> ShowS
forall a. Integral a => a -> ShowS
showHex Integer
i String
"") 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
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (NatRepr n -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr n
w)
  | Bool
otherwise = String -> Doc ann
forall a. HasCallStack => String -> a
error String
"ppLit given negative value"

ppCValue :: Prec -> CValue arch tp -> Doc ann
ppCValue :: forall arch (tp :: Type) ann. Prec -> CValue arch tp -> Doc ann
ppCValue Prec
_ (BoolCValue Bool
b) = if Bool
b then Doc ann
"true" else Doc ann
"false"
ppCValue Prec
p (BVCValue NatRepr n
w Integer
i)
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parenIf (Prec
p Prec -> Prec -> Bool
forall a. Ord a => a -> a -> Bool
> Prec
colonPrec) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ NatRepr n -> Integer -> Doc ann
forall (n :: Natural) ann. NatRepr n -> Integer -> Doc ann
ppLit NatRepr n
w Integer
i
  | Bool
otherwise =
    -- TODO: We may want to report an error here.
    Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parenIf (Prec
p Prec -> Prec -> Bool
forall a. Ord a => a -> a -> Bool
> Prec
colonPrec) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
    Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
i 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
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (NatRepr n -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr n
w)
ppCValue Prec
p (RelocatableCValue AddrWidthRepr (ArchAddrWidth arch)
_ MemAddr (ArchAddrWidth arch)
a) = Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parenIf (Prec
p Prec -> Prec -> Bool
forall a. Ord a => a -> a -> Bool
> Prec
plusPrec) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ MemAddr (ArchAddrWidth arch) -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow MemAddr (ArchAddrWidth arch)
a
ppCValue Prec
_ (SymbolCValue AddrWidthRepr (ArchAddrWidth arch)
_ SymbolIdentifier
a) = SymbolIdentifier -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow SymbolIdentifier
a

instance PrettyPrec (CValue arch tp) where
  prettyPrec :: forall ann. Prec -> CValue arch tp -> Doc ann
prettyPrec = Prec -> CValue arch tp -> Doc ann
forall arch (tp :: Type) ann. Prec -> CValue arch tp -> Doc ann
ppCValue

instance Pretty (CValue arch tp) where
  pretty :: forall ann. CValue arch tp -> Doc ann
pretty = Prec -> CValue arch tp -> Doc ann
forall arch (tp :: Type) ann. Prec -> CValue arch tp -> Doc ann
ppCValue Prec
0

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

------------------------------------------------------------------------
-- Value and Assignment

-- | A value at runtime
--
-- Values are only well-defined in the context of a particular block,
-- and are immutable within that context (i.e. their value would not
-- change from a memory write).
data Value arch ids tp where
  -- | A constant value
  CValue :: !(CValue arch tp) -> Value arch ids tp
  -- | Value from an assignment statement.
  AssignedValue :: !(Assignment arch ids tp)
                -> Value arch ids tp
  -- | Represents the value assigned to the register when the block started.
  Initial :: !(ArchReg arch tp)
          -> Value arch ids tp

-- | A constant bitvector
--
-- The integer should be between 0 and 2^n-1.
pattern BVValue :: ()
                => forall n . (tp ~ (BVType n), 1 <= n)
                => NatRepr n
                -> Integer
                -> Value arch ids tp
pattern $mBVValue :: forall {r} {tp :: Type} {arch} {ids}.
Value arch ids tp
-> (forall {n :: Natural}.
    (tp ~ BVType n, 1 <= n) =>
    NatRepr n -> Integer -> r)
-> ((# #) -> r)
-> r
$bBVValue :: forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue w i = CValue (BVCValue w i)

-- | A constant Boolean
pattern BoolValue :: () => (tp ~ BoolType) => Bool -> Value arch ids tp
pattern $mBoolValue :: forall {r} {tp :: Type} {arch} {ids}.
Value arch ids tp
-> ((tp ~ BoolType) => Bool -> r) -> ((# #) -> r) -> r
$bBoolValue :: forall (tp :: Type) arch ids.
(tp ~ BoolType) =>
Bool -> Value arch ids tp
BoolValue b = CValue (BoolCValue b)

-- | A memory address
pattern RelocatableValue :: ()
                         => tp ~ BVType (ArchAddrWidth arch)
                         => AddrWidthRepr (ArchAddrWidth arch)
                         -> MemAddr (ArchAddrWidth arch)
                         -> Value arch ids tp
pattern $mRelocatableValue :: forall {r} {tp :: Type} {arch} {ids}.
Value arch ids tp
-> ((tp ~ BVType (ArchAddrWidth arch)) =>
    AddrWidthRepr (ArchAddrWidth arch)
    -> MemAddr (ArchAddrWidth arch) -> r)
-> ((# #) -> r)
-> r
$bRelocatableValue :: forall (tp :: Type) arch ids.
(tp ~ BVType (ArchAddrWidth arch)) =>
AddrWidthRepr (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Value arch ids tp
RelocatableValue w a = CValue (RelocatableCValue w a)

-- | This denotes the address of a symbol identifier in the binary.
--
-- This appears when dealing with relocations.
pattern SymbolValue :: ()
                    => tp ~ BVType (ArchAddrWidth arch)
                    => AddrWidthRepr (ArchAddrWidth arch)
                    -> SymbolIdentifier
                    -> Value arch ids tp
pattern $mSymbolValue :: forall {r} {tp :: Type} {arch} {ids}.
Value arch ids tp
-> ((tp ~ BVType (ArchAddrWidth arch)) =>
    AddrWidthRepr (ArchAddrWidth arch) -> SymbolIdentifier -> r)
-> ((# #) -> r)
-> r
$bSymbolValue :: forall (tp :: Type) arch ids.
(tp ~ BVType (ArchAddrWidth arch)) =>
AddrWidthRepr (ArchAddrWidth arch)
-> SymbolIdentifier -> Value arch ids tp
SymbolValue w s = CValue (SymbolCValue w s)

{-# COMPLETE BVValue, BoolValue, RelocatableValue, SymbolValue, AssignedValue, Initial #-}

-- | An assignment consists of a unique location identifier and a right-
-- hand side that returns a value.
data Assignment arch ids tp =
  Assignment { forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId :: !(AssignId ids tp)
             , forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignRhs arch (Value arch ids) tp
assignRhs :: !(AssignRhs arch (Value arch ids) tp)
             }

-- | A  value with a bitvector type.
type BVValue arch ids w = Value arch ids (BVType w)

-- | A address value for a specific architecture
type ArchAddrValue arch ids = BVValue arch ids (ArchAddrWidth arch)

------------------------------------------------------------------------
-- Type operations on assignment Value

instance HasRepr (ArchReg arch) TypeRepr
      => HasRepr (Value arch ids) TypeRepr where

  typeRepr :: forall (tp :: Type). Value arch ids tp -> TypeRepr tp
typeRepr (CValue CValue arch tp
c) = CValue arch tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). CValue arch tp -> TypeRepr tp
typeRepr CValue arch tp
c
  typeRepr (AssignedValue Assignment arch ids tp
a) = AssignRhs arch (Value arch ids) tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type).
AssignRhs arch (Value arch ids) tp -> TypeRepr tp
typeRepr (Assignment arch ids tp -> AssignRhs arch (Value arch ids) tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignRhs arch (Value arch ids) tp
assignRhs Assignment arch ids tp
a)
  typeRepr (Initial ArchReg arch tp
r) = ArchReg arch tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). ArchReg arch tp -> TypeRepr tp
typeRepr ArchReg arch tp
r

------------------------------------------------------------------------
-- Value equality

instance OrdF (ArchReg arch)
      => OrdF (Value arch ids) where

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

  compareF (AssignedValue Assignment arch ids x
x) (AssignedValue Assignment arch ids y
y) =
    AssignId ids x -> AssignId ids y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
AssignId ids x -> AssignId ids y -> OrderingF x y
compareF (Assignment arch ids x -> AssignId ids x
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId Assignment arch ids x
x) (Assignment arch ids y -> AssignId ids y
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId Assignment arch ids y
y)
  compareF AssignedValue{} Value arch ids y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF Value arch ids x
_ AssignedValue{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareF (Initial ArchReg arch x
r) (Initial ArchReg arch y
r') =
    case ArchReg arch x -> ArchReg arch y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
ArchReg arch x -> ArchReg arch y -> OrderingF x y
compareF ArchReg arch x
r ArchReg arch y
r' of
      OrderingF x y
LTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
      OrderingF x y
EQF -> OrderingF x x
OrderingF x y
forall {k} (x :: k). OrderingF x x
EQF
      OrderingF x y
GTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF

instance OrdF (ArchReg arch)
      => TestEquality (Value arch ids) where
  testEquality :: forall (a :: Type) (b :: Type).
Value arch ids a -> Value arch ids b -> Maybe (a :~: b)
testEquality Value arch ids a
x Value arch ids b
y = OrderingF a b -> Maybe (a :~: b)
forall {k} (x :: k) (y :: k). OrderingF x y -> Maybe (x :~: y)
orderingF_refl (Value arch ids a -> Value arch ids b -> OrderingF a b
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Type) (y :: Type).
Value arch ids x -> Value arch ids y -> OrderingF x y
compareF Value arch ids a
x Value arch ids b
y)

instance OrdF (ArchReg arch)
      => Eq  (Value arch ids tp) where
  Value arch ids tp
x == :: Value arch ids tp -> Value arch ids tp -> Bool
== Value arch ids tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (Value arch ids tp -> Value arch ids tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
Value arch ids a -> Value arch ids b -> Maybe (a :~: b)
testEquality Value arch ids tp
x Value arch ids tp
y)

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

instance OrdF (ArchReg arch)
      => EqF (Value arch ids) where
  eqF :: forall (a :: Type). Value arch ids a -> Value arch ids a -> Bool
eqF = Value arch ids a -> Value arch ids a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

------------------------------------------------------------------------
-- Value operations

mkLit :: (1 <= n) => NatRepr n -> Integer -> Value arch ids (BVType n)
mkLit :: forall (n :: Natural) arch ids.
(1 <= n) =>
NatRepr n -> Integer -> Value arch ids (BVType n)
mkLit NatRepr n
n Integer
v = NatRepr n -> Integer -> Value arch ids (BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
n (Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)
  where mask :: Integer
mask = NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
maxUnsigned NatRepr n
n

bvValue :: (KnownNat n, 1 <= n) => Integer -> Value arch ids (BVType n)
bvValue :: forall (n :: Natural) arch ids.
(KnownNat n, 1 <= n) =>
Integer -> Value arch ids (BVType n)
bvValue Integer
i = NatRepr n -> Integer -> Value arch ids (BVType n)
forall (n :: Natural) arch ids.
(1 <= n) =>
NatRepr n -> Integer -> Value arch ids (BVType n)
mkLit NatRepr n
forall (n :: Natural). KnownNat n => NatRepr n
knownNat Integer
i

-- | Return the right-hand side if this is an assignment.
valueAsRhs :: Value arch ids tp -> Maybe (AssignRhs arch (Value arch ids) tp)
valueAsRhs :: forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (AssignRhs arch (Value arch ids) tp)
valueAsRhs (AssignedValue (Assignment AssignId ids tp
_ AssignRhs arch (Value arch ids) tp
v)) = AssignRhs arch (Value arch ids) tp
-> Maybe (AssignRhs arch (Value arch ids) tp)
forall a. a -> Maybe a
Just AssignRhs arch (Value arch ids) tp
v
valueAsRhs Value arch ids tp
_ = Maybe (AssignRhs arch (Value arch ids) tp)
forall a. Maybe a
Nothing

-- | Return the value evaluated if this is from an `App`.
valueAsApp :: Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp :: forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp (AssignedValue (Assignment AssignId ids tp
_ (EvalApp App (Value arch ids) tp
a))) = App (Value arch ids) tp -> Maybe (App (Value arch ids) tp)
forall a. a -> Maybe a
Just App (Value arch ids) tp
a
valueAsApp Value arch ids tp
_ = Maybe (App (Value arch ids) tp)
forall a. Maybe a
Nothing

-- | Return the architecture-specific function associated with a value.
valueAsArchFn :: Value arch ids tp -> Maybe (ArchFn arch (Value arch ids) tp)
valueAsArchFn :: forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (ArchFn arch (Value arch ids) tp)
valueAsArchFn (AssignedValue (Assignment AssignId ids tp
_ (EvalArchFn ArchFn arch (Value arch ids) tp
a TypeRepr tp
_))) = ArchFn arch (Value arch ids) tp
-> Maybe (ArchFn arch (Value arch ids) tp)
forall a. a -> Maybe a
Just ArchFn arch (Value arch ids) tp
a
valueAsArchFn Value arch ids tp
_ = Maybe (ArchFn arch (Value arch ids) tp)
forall a. Maybe a
Nothing

-- | This returns a segmented address if the value can be interpreted as a literal memory
-- address, and returns nothing otherwise.
valueAsMemAddr :: MemWidth (ArchAddrWidth arch)
               => BVValue arch ids (ArchAddrWidth arch)
               -> Maybe (ArchMemAddr arch)
valueAsMemAddr :: forall arch ids.
MemWidth (ArchAddrWidth arch) =>
BVValue arch ids (ArchAddrWidth arch) -> Maybe (ArchMemAddr arch)
valueAsMemAddr (BVValue NatRepr n
_ Integer
val)      = ArchMemAddr arch -> Maybe (ArchMemAddr arch)
forall a. a -> Maybe a
Just (ArchMemAddr arch -> Maybe (ArchMemAddr arch))
-> ArchMemAddr arch -> Maybe (ArchMemAddr arch)
forall a b. (a -> b) -> a -> b
$ MemWord n -> MemAddr n
forall (w :: Natural). MemWord w -> MemAddr w
absoluteAddr (Integer -> MemWord n
forall a. Num a => Integer -> a
fromInteger Integer
val)
valueAsMemAddr (RelocatableValue AddrWidthRepr (ArchAddrWidth arch)
_ ArchMemAddr arch
i) = ArchMemAddr arch -> Maybe (ArchMemAddr arch)
forall a. a -> Maybe a
Just ArchMemAddr arch
i
valueAsMemAddr BVValue arch ids (ArchAddrWidth arch)
_ = Maybe (ArchMemAddr arch)
forall a. Maybe a
Nothing

valueAsStaticMultiplication
  :: BVValue arch ids w
  -> Maybe (Natural, BVValue arch ids w)
valueAsStaticMultiplication :: forall arch ids (w :: Natural).
BVValue arch ids w -> Maybe (Natural, BVValue arch ids w)
valueAsStaticMultiplication BVValue arch ids w
v
  | Just (BVMul NatRepr n
_ (BVValue NatRepr n
_ Integer
mul) Value arch ids ('BVType n)
v') <- BVValue arch ids w -> Maybe (App (Value arch ids) (BVType w))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp BVValue arch ids w
v = (Natural, BVValue arch ids w)
-> Maybe (Natural, BVValue arch ids w)
forall a. a -> Maybe a
Just (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
mul, BVValue arch ids w
Value arch ids ('BVType n)
v')
  | Just (BVMul NatRepr n
_ Value arch ids ('BVType n)
v' (BVValue NatRepr n
_ Integer
mul)) <- BVValue arch ids w -> Maybe (App (Value arch ids) (BVType w))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp BVValue arch ids w
v = (Natural, BVValue arch ids w)
-> Maybe (Natural, BVValue arch ids w)
forall a. a -> Maybe a
Just (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
mul, BVValue arch ids w
Value arch ids ('BVType n)
v')
  | Just (BVShl NatRepr n
_ Value arch ids ('BVType n)
v' (BVValue NatRepr n
_ Integer
sh))  <- BVValue arch ids w -> Maybe (App (Value arch ids) (BVType w))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp BVValue arch ids w
v = (Natural, BVValue arch ids w)
-> Maybe (Natural, BVValue arch ids w)
forall a. a -> Maybe a
Just (Natural
2Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
sh, BVValue arch ids w
Value arch ids ('BVType n)
v')
  -- the PowerPC way to shift left is a bit obtuse...
  | Just (BVAnd NatRepr n
w Value arch ids ('BVType n)
v' (BVValue NatRepr n
_ Integer
c)) <- BVValue arch ids w -> Maybe (App (Value arch ids) (BVType w))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp BVValue arch ids w
v
  , Just (BVOr NatRepr n
_ Value arch ids ('BVType n)
l Value arch ids ('BVType n)
r) <- Value arch ids ('BVType n)
-> Maybe (App (Value arch ids) ('BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp Value arch ids ('BVType n)
v'
  , Just (BVShl NatRepr n
_ Value arch ids ('BVType n)
l' (BVValue NatRepr n
_ Integer
shl)) <- Value arch ids ('BVType n)
-> Maybe (App (Value arch ids) ('BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp Value arch ids ('BVType n)
l
  , Just (BVShr NatRepr n
_ Value arch ids ('BVType n)
_ (BVValue NatRepr n
_ Integer
shr)) <- Value arch ids ('BVType n)
-> Maybe (App (Value arch ids) ('BVType n))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp Value arch ids ('BVType n)
r
  , Integer
c Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Integer
forall a. Bits a => a -> a
complement (Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
shlInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Prec -> Integer
forall a. Bits a => Prec -> a
bit (Integer -> Prec
forall a. Num a => Integer -> a
fromInteger (NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w))
  , Integer
shr Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= NatRepr n -> Integer
forall (w :: Natural). NatRepr w -> Integer
intValue NatRepr n
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
shl
  = (Natural, BVValue arch ids w)
-> Maybe (Natural, BVValue arch ids w)
forall a. a -> Maybe a
Just (Natural
2Natural -> Integer -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
shl, BVValue arch ids w
Value arch ids ('BVType n)
l')
  | Bool
otherwise = Maybe (Natural, BVValue arch ids w)
forall a. Maybe a
Nothing

-- | Returns a segment offset associated with the value if one can be defined.
valueAsSegmentOff :: Memory (ArchAddrWidth arch)
                  -> BVValue arch ids (ArchAddrWidth arch)
                  -> Maybe (ArchSegmentOff arch)
valueAsSegmentOff :: forall arch ids.
Memory (ArchAddrWidth arch)
-> BVValue arch ids (ArchAddrWidth arch)
-> Maybe (ArchSegmentOff arch)
valueAsSegmentOff Memory (ArchAddrWidth arch)
mem BVValue arch ids (ArchAddrWidth arch)
v = do
  MemAddr (ArchAddrWidth arch)
a <- AddrWidthRepr (ArchAddrWidth arch)
-> (MemWidth (ArchAddrWidth arch) =>
    Maybe (MemAddr (ArchAddrWidth arch)))
-> Maybe (MemAddr (ArchAddrWidth arch))
forall (w :: Natural) a. AddrWidthRepr w -> (MemWidth w => a) -> a
addrWidthClass (Memory (ArchAddrWidth arch) -> AddrWidthRepr (ArchAddrWidth arch)
forall (w :: Natural). Memory w -> AddrWidthRepr w
memAddrWidth Memory (ArchAddrWidth arch)
mem) (BVValue arch ids (ArchAddrWidth arch)
-> Maybe (MemAddr (ArchAddrWidth arch))
forall arch ids.
MemWidth (ArchAddrWidth arch) =>
BVValue arch ids (ArchAddrWidth arch) -> Maybe (ArchMemAddr arch)
valueAsMemAddr BVValue arch ids (ArchAddrWidth arch)
v)
  Memory (ArchAddrWidth arch)
-> MemAddr (ArchAddrWidth arch) -> Maybe (ArchSegmentOff arch)
forall (w :: Natural).
Memory w -> MemAddr w -> Maybe (MemSegmentOff w)
asSegmentOff Memory (ArchAddrWidth arch)
mem MemAddr (ArchAddrWidth arch)
a

asInt64Constant :: Value arch ids (BVType 64) -> Maybe Int64
asInt64Constant :: forall arch ids. Value arch ids (BVType 64) -> Maybe Int64
asInt64Constant (BVValue NatRepr n
_ Integer
o) = Int64 -> Maybe Int64
forall a. a -> Maybe a
Just (Integer -> Int64
forall a. Num a => Integer -> a
fromInteger Integer
o)
asInt64Constant Value arch ids (BVType 64)
_ = Maybe Int64
forall a. Maybe a
Nothing

asBaseOffset :: Value arch ids (BVType w) -> (Value arch ids (BVType w), Integer)
asBaseOffset :: forall arch ids (w :: Natural).
Value arch ids (BVType w) -> (Value arch ids (BVType w), Integer)
asBaseOffset Value arch ids (BVType w)
x
  | Just (BVAdd NatRepr n
_ Value arch ids ('BVType n)
x_base (BVValue NatRepr n
_  Integer
x_off)) <- Value arch ids (BVType w)
-> Maybe (App (Value arch ids) (BVType w))
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp Value arch ids (BVType w)
x = (Value arch ids (BVType w)
Value arch ids ('BVType n)
x_base, Integer
x_off)
  | Bool
otherwise = (Value arch ids (BVType w)
x,Integer
0)

-- | A stack offset that can also capture the width must match the pointer width.
data StackOffsetView arch tp where
  StackOffsetView :: !Integer -> StackOffsetView arch (BVType (ArchAddrWidth arch))

-- | This pattern matches on an app to see if it can be used to adjust a
-- stack offset.
appAsStackOffset :: forall arch ids tp
                 .  MemWidth (ArchAddrWidth arch)
                 => (Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer)
                 -- ^ Function for inferring if argument is a stack offset.
                 -> App (Value arch ids) tp
                 -> Maybe (StackOffsetView arch tp)
appAsStackOffset :: forall arch ids (tp :: Type).
MemWidth (ArchAddrWidth arch) =>
(Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer)
-> App (Value arch ids) tp -> Maybe (StackOffsetView arch tp)
appAsStackOffset Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer
stackFn App (Value arch ids) tp
app =
  case App (Value arch ids) tp
app of
    BVAdd NatRepr n
w (BVValue NatRepr n
_ Integer
i) Value arch ids ('BVType n)
y -> do
      n :~: ArchAddrWidth arch
Refl <- NatRepr n
-> NatRepr (ArchAddrWidth arch) -> Maybe (n :~: ArchAddrWidth arch)
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 (forall (w :: Natural). MemWidth w => NatRepr w
memWidthNatRepr @(ArchAddrWidth arch))
      (\Integer
j -> Integer -> StackOffsetView arch (BVType (ArchAddrWidth arch))
forall arch.
Integer -> StackOffsetView arch (BVType (ArchAddrWidth arch))
StackOffsetView (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
j)) (Integer -> StackOffsetView arch tp)
-> Maybe Integer -> Maybe (StackOffsetView arch tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer
stackFn Value arch ids ('BVType n)
Value arch ids (BVType (ArchAddrWidth arch))
y
    BVAdd NatRepr n
w Value arch ids ('BVType n)
x (BVValue NatRepr n
_ Integer
j) -> do
      n :~: ArchAddrWidth arch
Refl <- NatRepr n
-> NatRepr (ArchAddrWidth arch) -> Maybe (n :~: ArchAddrWidth arch)
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 (forall (w :: Natural). MemWidth w => NatRepr w
memWidthNatRepr @(ArchAddrWidth arch))
      (\Integer
i -> Integer -> StackOffsetView arch (BVType (ArchAddrWidth arch))
forall arch.
Integer -> StackOffsetView arch (BVType (ArchAddrWidth arch))
StackOffsetView (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
j)) (Integer -> StackOffsetView arch tp)
-> Maybe Integer -> Maybe (StackOffsetView arch tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer
stackFn Value arch ids ('BVType n)
Value arch ids (BVType (ArchAddrWidth arch))
x
    BVSub NatRepr n
w Value arch ids ('BVType n)
x (BVValue NatRepr n
_ Integer
j) -> do
      n :~: ArchAddrWidth arch
Refl <- NatRepr n
-> NatRepr (ArchAddrWidth arch) -> Maybe (n :~: ArchAddrWidth arch)
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 (forall (w :: Natural). MemWidth w => NatRepr w
memWidthNatRepr @(ArchAddrWidth arch))
      (\Integer
i -> Integer -> StackOffsetView arch (BVType (ArchAddrWidth arch))
forall arch.
Integer -> StackOffsetView arch (BVType (ArchAddrWidth arch))
StackOffsetView (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
j)) (Integer -> StackOffsetView arch tp)
-> Maybe Integer -> Maybe (StackOffsetView arch tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Value arch ids (BVType (ArchAddrWidth arch)) -> Maybe Integer
stackFn Value arch ids ('BVType n)
Value arch ids (BVType (ArchAddrWidth arch))
x
    App (Value arch ids) tp
_ ->
      Maybe (StackOffsetView arch tp)
forall a. Maybe a
Nothing

-- | During the jump-table detection phase of code discovery, we have the
-- following problem: we are given a value which represents the computation
-- done to create an address to jump to. We'd like to look at the shape of that
-- computation and check whether it "looks like a jump table" -- say, whether
-- it is the computation @array_base + pointer_size * i@ for some unknown index
-- @i@.
--
-- However, some architectures have special rules about what addresses are
-- valid jump targets, and so there is frequently a sort of "standard prelude"
-- which converts an arbitrary address into a valid jump target. For example,
-- on PowerPC, the instruction pointer is always a multiple of four, so any
-- computed jump strips off the bottom two bits. We'd like the jump-table
-- detection code to be able to ignore that standard prelude when looking for
-- jump-table-like computations (without having to know that the right thing to
-- look for is "ignore the bottom two bits").
--
-- The 'fromIPAligned' method below gives specific architectures a hook for
-- stripping away the prelude and leaving the underlying computed value (which
-- is potentially an invalid jump target!).
--
-- Of course, after stripping away the cleanup parts of the computation,
-- checking the unclean computation for specific patterns, and finding
-- particular concrete values that the unclean computation could evaluate to,
-- the discovery code then needs to be able to re-clean the concrete values.
-- The 'toIPAligned' method gives architectures a hook to do that direction of
-- translation.
class IPAlignment arch where
  -- | Take an aligned value and strip away the bits of the semantics that
  -- align it, leaving behind a (potentially unaligned) value. Return 'Nothing'
  -- if the input value does not appear to be a valid value for the instruction
  -- pointer.
  fromIPAligned :: ArchAddrValue arch ids -> Maybe (ArchAddrValue arch ids)

  -- | Take an unaligned memory address and clean it up so that it is a valid
  -- value for the instruction pointer.
  toIPAligned :: MemAddr (ArchAddrWidth arch) -> MemAddr (ArchAddrWidth arch)

------------------------------------------------------------------------
-- RegState

-- | This represents the state of the processor registers.
newtype RegState (r :: k -> Kind.Type) (f :: k -> Kind.Type) = RegState (MapF.MapF r f)

deriving instance (OrdF r, EqF f) => Eq (RegState r f)

deriving instance FunctorF  (RegState r)
deriving instance FoldableF (RegState r)

instance TraversableF (RegState r) where
  traverseF :: forall (m :: Type -> Type) (e :: k -> Type) (f :: k -> Type).
Applicative m =>
(forall (s :: k). e s -> m (f s))
-> RegState r e -> m (RegState r f)
traverseF forall (s :: k). e s -> m (f s)
f (RegState MapF r e
m) = MapF r f -> RegState r f
forall k (r :: k -> Type) (f :: k -> Type).
MapF r f -> RegState r f
RegState (MapF r f -> RegState r f) -> m (MapF r f) -> m (RegState r f)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (s :: k). e s -> m (f s)) -> MapF r e -> m (MapF r f)
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: k -> Type) (f :: k -> Type).
Applicative m =>
(forall (s :: k). e s -> m (f s)) -> MapF r e -> m (MapF r f)
traverseF e s -> m (f s)
forall (s :: k). e s -> m (f s)
f MapF r e
m

-- | Return underlying map of register state.
regStateMap :: RegState r f -> MapF.MapF r f
regStateMap :: forall {v} (r :: v -> Type) (f :: v -> Type).
RegState r f -> MapF r f
regStateMap (RegState MapF r f
m) = MapF r f
m

-- | Traverse the register state with the name of each register and value.
traverseRegsWith :: Applicative m
                 => (forall tp. r tp -> f tp -> m (g tp))
                 -> RegState r f
                 -> m (RegState r g)
traverseRegsWith :: forall {k} (m :: Type -> Type) (r :: k -> Type) (f :: k -> Type)
       (g :: k -> Type).
Applicative m =>
(forall (tp :: k). r tp -> f tp -> m (g tp))
-> RegState r f -> m (RegState r g)
traverseRegsWith forall (tp :: k). r tp -> f tp -> m (g tp)
f (RegState MapF r f
m) = MapF r g -> RegState r g
forall k (r :: k -> Type) (f :: k -> Type).
MapF r f -> RegState r f
RegState (MapF r g -> RegState r g) -> m (MapF r g) -> m (RegState r g)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: k). r tp -> f tp -> m (g tp))
-> MapF r f -> m (MapF r g)
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type)
       (g :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m (g tp))
-> MapF ktp f -> m (MapF ktp g)
MapF.traverseWithKey r tp -> f tp -> m (g tp)
forall (tp :: k). r tp -> f tp -> m (g tp)
f MapF r f
m

-- | Traverse the register state with the name of each register and value.
traverseRegsWith_ :: Applicative m
                  => (forall tp. r tp -> f tp -> m ())
                  -> RegState r f
                  -> m ()
traverseRegsWith_ :: forall {k} (m :: Type -> Type) (r :: k -> Type) (f :: k -> Type).
Applicative m =>
(forall (tp :: k). r tp -> f tp -> m ()) -> RegState r f -> m ()
traverseRegsWith_ forall (tp :: k). r tp -> f tp -> m ()
f (RegState MapF r f
m) = (forall (tp :: k). r tp -> f tp -> m ()) -> MapF r f -> m ()
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m ()) -> MapF ktp f -> m ()
MapF.traverseWithKey_ r tp -> f tp -> m ()
forall (tp :: k). r tp -> f tp -> m ()
f MapF r f
m

-- | Traverse the register state with the name of each register and value.
mapRegsWith :: (forall tp. r tp -> f tp -> g tp)
            -> RegState r f
            -> RegState r g
mapRegsWith :: forall {k} (r :: k -> Type) (f :: k -> Type) (g :: k -> Type).
(forall (tp :: k). r tp -> f tp -> g tp)
-> RegState r f -> RegState r g
mapRegsWith forall (tp :: k). r tp -> f tp -> g tp
f (RegState MapF r f
m) = MapF r g -> RegState r g
forall k (r :: k -> Type) (f :: k -> Type).
MapF r f -> RegState r f
RegState ((forall (tp :: k). r tp -> f tp -> g tp) -> MapF r f -> MapF r g
forall {v} (ktp :: v -> Type) (f :: v -> Type) (g :: v -> Type).
(forall (tp :: v). ktp tp -> f tp -> g tp)
-> MapF ktp f -> MapF ktp g
MapF.mapWithKey r tp -> f tp -> g tp
forall (tp :: k). r tp -> f tp -> g tp
f MapF r f
m)

{-# INLINE[1] boundValue #-} -- Make sure the RULE gets a chance to fire

-- | Get a register out of the state.
boundValue :: forall r f tp
           .  OrdF r
           => r tp
           -> Lens' (RegState r f) (f tp)
boundValue :: forall {k} (r :: k -> Type) (f :: k -> Type) (tp :: k).
OrdF r =>
r tp -> Lens' (RegState r f) (f tp)
boundValue r tp
r =
  -- TODO Ideally there would be a Lens-aware "alter"-type operation
  -- in Data.Parameterized.Map (see Data.Map source); such an
  -- operation would have SPECIALIZE pragmas that would make it good
  -- to use to implement this.  We're resorting to RULES here, without
  -- which boundValue was accounting for over 8% of runtime on
  -- Brittle.
  (RegState r f -> f tp)
-> (RegState r f -> f tp -> RegState r f)
-> Lens (RegState r f) (RegState r f) (f tp) (f tp)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (r tp -> RegState r f -> f tp
forall {k} (r :: k -> Type) (tp :: k) (f :: k -> Type).
OrdF r =>
r tp -> RegState r f -> f tp
getBoundValue r tp
r) (r tp -> RegState r f -> f tp -> RegState r f
forall {k} (r :: k -> Type) (tp :: k) (f :: k -> Type).
OrdF r =>
r tp -> RegState r f -> f tp -> RegState r f
setBoundValue r tp
r)

getBoundValue :: OrdF r => r tp -> RegState r f -> f tp
getBoundValue :: forall {k} (r :: k -> Type) (tp :: k) (f :: k -> Type).
OrdF r =>
r tp -> RegState r f -> f tp
getBoundValue r tp
r (RegState MapF r f
m) =
  case r tp -> MapF r f -> Maybe (f 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 f
m of
    Just f tp
v -> f tp
v
    Maybe (f tp)
Nothing -> String -> f tp
forall a. HasCallStack => String -> a
error String
"internal error in boundValue given unexpected reg"

-- Without this rule, boundValue gets left as a higher-order function,
-- making its uses VERY slow.
{-# RULES
      "boundValue/get" forall rs r. get (boundValue r) rs = getBoundValue r rs
  #-}
-- Note that this rule seems to cover (^.) as well as get, which is
-- fortunate since a parsing bug makes it impossible to mention (^.)
-- in a rule.

setBoundValue :: OrdF r => r tp -> RegState r f -> f tp -> RegState r f
setBoundValue :: forall {k} (r :: k -> Type) (tp :: k) (f :: k -> Type).
OrdF r =>
r tp -> RegState r f -> f tp -> RegState r f
setBoundValue r tp
r (RegState MapF r f
m) f tp
v = MapF r f -> RegState r f
forall k (r :: k -> Type) (f :: k -> Type).
MapF r f -> RegState r f
RegState (r tp -> f tp -> MapF r f -> MapF r f
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert r tp
r f tp
v MapF r f
m)

-- | Compares if two register states are equal.
cmpRegState :: OrdF r
            => (forall u. f u -> g u -> Bool)
               -- ^ Function for checking if two values are equal.
            -> RegState r f
            -> RegState r g
            -> Bool
cmpRegState :: forall {k} (r :: k -> Type) (f :: k -> Type) (g :: k -> Type).
OrdF r =>
(forall (u :: k). f u -> g u -> Bool)
-> RegState r f -> RegState r g -> Bool
cmpRegState forall (u :: k). f u -> g u -> Bool
p (RegState MapF r f
x) (RegState MapF r g
y) = [Pair r f] -> [Pair r g] -> Bool
go (MapF r f -> [Pair r f]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Pair k2 a]
MapF.toList MapF r f
x) (MapF r g -> [Pair r g]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Pair k2 a]
MapF.toList MapF r g
y)
  where go :: [Pair r f] -> [Pair r g] -> Bool
go [] [] = Bool
True
        go [] (Pair r g
_:[Pair r g]
_) = Bool
False
        go (Pair r f
_:[Pair r f]
_) [] = Bool
False
        go (MapF.Pair r tp
xk f tp
xv:[Pair r f]
xr) (MapF.Pair r tp
yk g tp
yv:[Pair r g]
yr) =
          case r tp -> r tp -> Maybe (tp :~: tp)
forall (a :: k) (b :: k). r a -> r b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality r tp
xk r tp
yk of
            Maybe (tp :~: tp)
Nothing -> Bool
False
            Just tp :~: tp
Refl -> f tp -> g tp -> Bool
forall (u :: k). f u -> g u -> Bool
p f tp
xv g tp
g tp
yv Bool -> Bool -> Bool
&& [Pair r f] -> [Pair r g] -> Bool
go [Pair r f]
xr [Pair r g]
yr

------------------------------------------------------------------------
-- RegisterInfo

-- | This class provides access to information about registers.
class ( OrdF r
      , ShowF r
      , MemWidth (RegAddrWidth r)
      , HasRepr r  TypeRepr
      ) => RegisterInfo r where

  -- | List of all arch registers.
  archRegs :: [Some r]

  -- | Set of all arch registers (expressed as a 'MapF.Map' of units).
  -- Preferable to 'archRegs' when building a map.
  archRegSet :: MapF.MapF r (Const ())
  archRegSet = [Pair r (Const ())] -> MapF r (Const ())
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
[Pair k a] -> MapF k a
MapF.fromList [ r x -> Const () x -> Pair r (Const ())
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
MapF.Pair r x
r (() -> Const () x
forall {k} a (b :: k). a -> Const a b
Const ()) | Some r x
r <- [Some r]
forall (r :: Type -> Type). RegisterInfo r => [Some r]
archRegs ]

  -- | The stack pointer register
  sp_reg :: r (BVType (RegAddrWidth r))

  -- | The instruction pointer register
  ip_reg :: r (BVType (RegAddrWidth r))

  -- | The register used to store system call numbers.
  syscall_num_reg :: r (BVType (RegAddrWidth r))

  -- | Registers used for passing system call arguments
  syscallArgumentRegs :: [r (BVType (RegAddrWidth r))]

--  The value of the current instruction pointer.
curIP :: RegisterInfo r
      => Lens' (RegState r f) (f (BVType (RegAddrWidth r)))
curIP :: forall (r :: Type -> Type) (f :: Type -> Type).
RegisterInfo r =>
Lens' (RegState r f) (f (BVType (RegAddrWidth r)))
curIP = r (BVType (RegAddrWidth r))
-> Lens' (RegState r f) (f (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

mkRegStateM :: (RegisterInfo r, Applicative m)
            => (forall tp . r tp -> m (f tp))
            -> m (RegState r f)
mkRegStateM :: 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 -> m (f tp)
f = MapF r f -> RegState r f
forall k (r :: k -> Type) (f :: k -> Type).
MapF r f -> RegState r f
RegState (MapF r f -> RegState r f) -> m (MapF r f) -> m (RegState r f)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: Type). r tp -> Const () tp -> m (f tp))
-> MapF r (Const ()) -> m (MapF r f)
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type)
       (g :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m (g tp))
-> MapF ktp f -> m (MapF ktp g)
MapF.traverseWithKey (\r tp
k Const () tp
_ -> r tp -> m (f tp)
forall (tp :: Type). r tp -> m (f tp)
f r tp
k) MapF r (Const ())
forall (r :: Type -> Type). RegisterInfo r => MapF r (Const ())
archRegSet

-- Create a pure register state
mkRegState :: RegisterInfo r
           => (forall tp . r tp -> f tp)
           -> RegState r f
mkRegState :: forall (r :: Type -> Type) (f :: Type -> Type).
RegisterInfo r =>
(forall (tp :: Type). r tp -> f tp) -> RegState r f
mkRegState forall (tp :: Type). r tp -> f tp
f = Identity (RegState r f) -> RegState r f
forall a. Identity a -> a
runIdentity ((forall (tp :: Type). r tp -> Identity (f tp))
-> Identity (RegState r f)
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 (f tp -> Identity (f tp)
forall a. a -> Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (f tp -> Identity (f tp))
-> (r tp -> f tp) -> r tp -> Identity (f tp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r tp -> f tp
forall (tp :: Type). r tp -> f tp
f))

zipWithRegState :: RegisterInfo r
                => (forall u. f u -> g u -> h u)
                -> RegState r f
                -> RegState r g
                -> RegState r h
zipWithRegState :: forall (r :: Type -> Type) (f :: Type -> Type) (g :: Type -> Type)
       (h :: Type -> Type).
RegisterInfo r =>
(forall (u :: Type). f u -> g u -> h u)
-> RegState r f -> RegState r g -> RegState r h
zipWithRegState forall (u :: Type). f u -> g u -> h u
f RegState r f
x RegState r g
y = (forall (tp :: Type). r tp -> h tp) -> RegState r h
forall (r :: Type -> Type) (f :: Type -> Type).
RegisterInfo r =>
(forall (tp :: Type). r tp -> f tp) -> RegState r f
mkRegState (\r tp
r -> f tp -> g tp -> h tp
forall (u :: Type). f u -> g u -> h u
f (RegState r f
x RegState r f -> Getting (f tp) (RegState r f) (f tp) -> f tp
forall s a. s -> Getting a s a -> a
^. r tp -> Lens' (RegState r f) (f 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) (RegState r g
y RegState r g -> Getting (g tp) (RegState r g) (g tp) -> g tp
forall s a. s -> Getting a s a -> a
^. r tp -> Lens' (RegState r g) (g 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))

-- | Returns a offset if the value is an offset of the stack.
asStackAddrOffset :: RegisterInfo (ArchReg arch)
                  => Value arch ids tp
                  -> Maybe (BVValue arch ids (ArchAddrWidth arch))
asStackAddrOffset :: forall arch ids (tp :: Type).
RegisterInfo (ArchReg arch) =>
Value arch ids tp -> Maybe (BVValue arch ids (ArchAddrWidth arch))
asStackAddrOffset Value arch ids tp
addr
  | Just (BVAdd NatRepr n
_ (Initial ArchReg arch ('BVType n)
base) Value arch ids ('BVType n)
offset) <- Value arch ids tp -> Maybe (App (Value arch ids) tp)
forall arch ids (tp :: Type).
Value arch ids tp -> Maybe (App (Value arch ids) tp)
valueAsApp Value arch ids tp
addr
  , Just 'BVType n :~: BVType (RegAddrWidth (ArchReg arch))
Refl <- ArchReg arch ('BVType n)
-> ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
-> Maybe ('BVType n :~: 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 ('BVType n)
base ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
sp_reg = do
    Value arch ids ('BVType n) -> Maybe (Value arch ids ('BVType n))
forall a. a -> Maybe a
Just Value arch ids ('BVType n)
offset
  | Initial ArchReg arch tp
base <- Value arch ids tp
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
base ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
forall (r :: Type -> Type).
RegisterInfo r =>
r (BVType (RegAddrWidth r))
sp_reg =
      case ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
-> TypeRepr (BVType (RegAddrWidth (ArchReg arch)))
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). ArchReg arch tp -> TypeRepr tp
typeRepr ArchReg arch tp
ArchReg arch (BVType (RegAddrWidth (ArchReg arch)))
base of
        BVTypeRepr NatRepr n
w -> Value arch ids ('BVType n) -> Maybe (Value arch ids ('BVType n))
forall a. a -> Maybe a
Just (NatRepr n -> Integer -> Value arch ids ('BVType n)
forall (tp :: Type) arch ids (n :: Natural).
(tp ~ BVType n, 1 <= n) =>
NatRepr n -> Integer -> Value arch ids tp
BVValue NatRepr n
w Integer
0)
  | Bool
otherwise =
    Maybe (BVValue arch ids (RegAddrWidth (ArchReg arch)))
forall a. Maybe a
Nothing

------------------------------------------------------------------------
-- Pretty print Assign, AssignRhs, Value operations

-- | Pretty print a value.
ppValue :: ShowF (ArchReg arch) => Prec -> Value arch ids tp -> Doc ann
ppValue :: forall arch ids (tp :: Type) ann.
ShowF (ArchReg arch) =>
Prec -> Value arch ids tp -> Doc ann
ppValue Prec
p (CValue CValue arch tp
c) = Prec -> CValue arch tp -> Doc ann
forall arch (tp :: Type) ann. Prec -> CValue arch tp -> Doc ann
ppCValue Prec
p CValue arch tp
c
ppValue Prec
_ (AssignedValue Assignment arch ids tp
a) = AssignId ids tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId (Assignment arch ids tp -> AssignId ids tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId Assignment arch ids tp
a)
ppValue Prec
_ (Initial ArchReg arch tp
r)       = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (ArchReg arch tp -> String
forall k (f :: k -> Type) (tp :: k). ShowF f => f tp -> String
forall (tp :: Type). ArchReg arch tp -> String
showF ArchReg arch tp
r) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
"_0"

instance ShowF (ArchReg arch) => PrettyPrec (Value arch ids tp) where
  prettyPrec :: forall ann. Prec -> Value arch ids tp -> Doc ann
prettyPrec = Prec -> Value arch ids tp -> Doc ann
forall arch ids (tp :: Type) ann.
ShowF (ArchReg arch) =>
Prec -> Value arch ids tp -> Doc ann
ppValue

instance ShowF (ArchReg arch) => Pretty (Value arch ids tp) where
  pretty :: forall ann. Value arch ids tp -> Doc ann
pretty = Prec -> Value arch ids tp -> Doc ann
forall arch ids (tp :: Type) ann.
ShowF (ArchReg arch) =>
Prec -> Value arch ids tp -> Doc ann
ppValue Prec
0

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

-- | Typeclass for architecture-specific functions
class IsArchFn (f :: (Type -> Kind.Type) -> Type -> Kind.Type)  where
  -- | A function for pretty printing an archFn of a given type.
  ppArchFn :: Applicative m
           => (forall u . v u -> m (Doc ann))
              -- ^ Function for pretty printing vlaue.
           -> f v tp
           -> m (Doc ann)

-- | Typeclass for architecture-specific statements
class IsArchStmt (f :: (Type -> Kind.Type) -> Kind.Type)  where
  -- | A function for pretty printing an architecture statement of a given type.
  ppArchStmt :: (forall u . v u -> Doc ann)
                -- ^ Function for pretty printing value.
             -> f v
             -> Doc ann

class IsArchTermStmt (f :: (Type -> Kind.Type) -> Kind.Type) where
  ppArchTermStmt :: (forall u . v u -> Doc ann)
                 -- ^ Function to pretty print contained values
                 -> f v
                 -> Doc ann

-- | Constructs expected by architectures type classes.
type ArchConstraints arch
   = ( RegisterInfo (ArchReg arch)
     , FoldableFC (ArchFn arch)
     , IsArchFn   (ArchFn arch)
     , IsArchStmt (ArchStmt arch)
     , FoldableF  (ArchStmt arch)
     , IsArchTermStmt (ArchTermStmt arch)
     , IPAlignment arch
     )

-- | Pretty print an assignment right-hand side using operations parameterized
-- over an application to allow side effects.
ppAssignRhs :: (Applicative m, ArchConstraints arch)
            => (forall u . f u -> m (Doc ann))
               -- ^ Function for pretty printing value.
            -> AssignRhs arch f tp
            -> m (Doc ann)
ppAssignRhs :: forall (m :: Type -> Type) arch (f :: Type -> Type) ann
       (tp :: Type).
(Applicative m, ArchConstraints arch) =>
(forall (u :: Type). f u -> m (Doc ann))
-> AssignRhs arch f tp -> m (Doc ann)
ppAssignRhs forall (u :: Type). f u -> m (Doc ann)
pp (EvalApp App f tp
a) = (forall (u :: Type). f u -> m (Doc ann)) -> App f tp -> m (Doc ann)
forall (m :: Type -> Type) (f :: Type -> Type) (tp :: Type) ann.
Applicative m =>
(forall (u :: Type). f u -> m (Doc ann)) -> App f tp -> m (Doc ann)
ppAppA f u -> m (Doc ann)
forall (u :: Type). f u -> m (Doc ann)
pp App f tp
a
ppAssignRhs forall (u :: Type). f u -> m (Doc ann)
_  (SetUndefined TypeRepr tp
tp) = Doc ann -> m (Doc ann)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> m (Doc ann)) -> Doc ann -> m (Doc ann)
forall a b. (a -> b) -> a -> b
$ Doc ann
"undef ::" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (TypeRepr tp -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow TypeRepr tp
tp)
ppAssignRhs forall (u :: Type). f u -> m (Doc ann)
pp (ReadMem f (BVType (ArchAddrWidth arch))
a MemRepr tp
repr) =
  (\Doc ann
d -> Doc ann
"read_mem" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
d Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
PP.parens (MemRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MemRepr tp -> Doc ann
pretty MemRepr tp
repr)) (Doc ann -> Doc ann) -> m (Doc ann) -> m (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (BVType (ArchAddrWidth arch)) -> m (Doc ann)
forall (u :: Type). f u -> m (Doc ann)
pp f (BVType (ArchAddrWidth arch))
a
ppAssignRhs forall (u :: Type). f u -> m (Doc ann)
pp (CondReadMem MemRepr tp
repr f BoolType
c f (BVType (ArchAddrWidth arch))
a f tp
d) = Doc ann -> Doc ann -> Doc ann -> Doc ann
f (Doc ann -> Doc ann -> Doc ann -> Doc ann)
-> m (Doc ann) -> m (Doc ann -> Doc ann -> Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f BoolType -> m (Doc ann)
forall (u :: Type). f u -> m (Doc ann)
pp f BoolType
c m (Doc ann -> Doc ann -> Doc ann)
-> m (Doc ann) -> m (Doc ann -> Doc ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> f (BVType (ArchAddrWidth arch)) -> m (Doc ann)
forall (u :: Type). f u -> m (Doc ann)
pp f (BVType (ArchAddrWidth arch))
a m (Doc ann -> Doc ann) -> m (Doc ann) -> m (Doc ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> f tp -> m (Doc ann)
forall (u :: Type). f u -> m (Doc ann)
pp f tp
d
  where f :: Doc ann -> Doc ann -> Doc ann -> Doc ann
f Doc ann
cd Doc ann
ad Doc ann
dd = Doc ann
"cond_read_mem" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
PP.parens (MemRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MemRepr tp -> Doc ann
pretty MemRepr tp
repr) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
cd Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
ad Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
dd
ppAssignRhs forall (u :: Type). f u -> m (Doc ann)
pp (EvalArchFn ArchFn arch f tp
f TypeRepr tp
_) = (forall (u :: Type). f u -> m (Doc ann))
-> ArchFn arch f tp -> m (Doc ann)
forall (m :: Type -> Type) (v :: Type -> Type) ann (tp :: Type).
Applicative m =>
(forall (u :: Type). v u -> m (Doc ann))
-> ArchFn arch v tp -> m (Doc ann)
forall (f :: (Type -> Type) -> Type -> Type) (m :: Type -> Type)
       (v :: Type -> Type) ann (tp :: Type).
(IsArchFn f, Applicative m) =>
(forall (u :: Type). v u -> m (Doc ann)) -> f v tp -> m (Doc ann)
ppArchFn f u -> m (Doc ann)
forall (u :: Type). f u -> m (Doc ann)
pp ArchFn arch f tp
f

instance ArchConstraints arch => Pretty (AssignRhs arch (Value arch ids) tp) where
  pretty :: forall ann. AssignRhs arch (Value arch ids) tp -> Doc ann
pretty = Identity (Doc ann) -> Doc ann
forall a. Identity a -> a
runIdentity (Identity (Doc ann) -> Doc ann)
-> (AssignRhs arch (Value arch ids) tp -> Identity (Doc ann))
-> AssignRhs arch (Value arch ids) tp
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (u :: Type). Value arch ids u -> Identity (Doc ann))
-> AssignRhs arch (Value arch ids) tp -> Identity (Doc ann)
forall (m :: Type -> Type) arch (f :: Type -> Type) ann
       (tp :: Type).
(Applicative m, ArchConstraints arch) =>
(forall (u :: Type). f u -> m (Doc ann))
-> AssignRhs arch f tp -> m (Doc ann)
ppAssignRhs (Doc ann -> Identity (Doc ann)
forall a. a -> Identity a
Identity (Doc ann -> Identity (Doc ann))
-> (Value arch ids u -> Doc ann)
-> Value arch ids u
-> Identity (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prec -> Value arch ids u -> Doc ann
forall arch ids (tp :: Type) ann.
ShowF (ArchReg arch) =>
Prec -> Value arch ids tp -> Doc ann
ppValue Prec
10)

instance ArchConstraints arch => Pretty (Assignment arch ids tp) where
  pretty :: forall ann. Assignment arch ids tp -> Doc ann
pretty (Assignment AssignId ids tp
lhs AssignRhs arch (Value arch ids) tp
rhs) = AssignId ids tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId ids tp
lhs 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
<+> AssignRhs arch (Value arch ids) tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. AssignRhs arch (Value arch ids) tp -> Doc ann
pretty AssignRhs arch (Value arch ids) tp
rhs

------------------------------------------------------------------------
-- Pretty print a value assignment

-- | Helper type to wrap up a 'Doc' with a dummy type argument; used to put
-- 'Doc's into heterogenous maps in the below
newtype DocF ann (a :: Type) = DocF (Doc ann)

-- | This pretty prints a value's representation while saving the pretty
-- printed repreentation of subvalues in a map.
collectValueRep :: forall arch ids tp ann
                .  ArchConstraints arch
                => Prec -- ^ Outer precedence
                -> Value arch ids tp
                -> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
collectValueRep :: forall arch ids (tp :: Type) ann.
ArchConstraints arch =>
Prec
-> Value arch ids tp
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
collectValueRep Prec
_ (AssignedValue Assignment arch ids tp
a) = do
  let lhs :: AssignId ids tp
lhs = Assignment arch ids tp -> AssignId ids tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignId ids tp
assignId Assignment arch ids tp
a
  Maybe (DocF ann tp)
mr <- (MapF (AssignId ids) (DocF ann) -> Maybe (DocF ann tp))
-> StateT
     (MapF (AssignId ids) (DocF ann)) Identity (Maybe (DocF ann tp))
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
gets ((MapF (AssignId ids) (DocF ann) -> Maybe (DocF ann tp))
 -> StateT
      (MapF (AssignId ids) (DocF ann)) Identity (Maybe (DocF ann tp)))
-> (MapF (AssignId ids) (DocF ann) -> Maybe (DocF ann tp))
-> StateT
     (MapF (AssignId ids) (DocF ann)) Identity (Maybe (DocF ann tp))
forall a b. (a -> b) -> a -> b
$ AssignId ids tp
-> MapF (AssignId ids) (DocF ann) -> Maybe (DocF ann 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
lhs
  Bool
-> StateT (MapF (AssignId ids) (DocF ann)) Identity ()
-> StateT (MapF (AssignId ids) (DocF ann)) Identity ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Maybe (DocF ann tp) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (DocF ann tp)
mr) (StateT (MapF (AssignId ids) (DocF ann)) Identity ()
 -> StateT (MapF (AssignId ids) (DocF ann)) Identity ())
-> StateT (MapF (AssignId ids) (DocF ann)) Identity ()
-> StateT (MapF (AssignId ids) (DocF ann)) Identity ()
forall a b. (a -> b) -> a -> b
$ do
    let ppVal :: forall u . Value arch ids u ->
                 State (MapF (AssignId ids) (DocF ann)) (Doc ann)
        ppVal :: forall (u :: Type).
Value arch ids u
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
ppVal = Prec
-> Value arch ids u
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall arch ids (tp :: Type) ann.
ArchConstraints arch =>
Prec
-> Value arch ids tp
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
collectValueRep Prec
10
    Doc ann
rhs <- (forall (u :: Type).
 Value arch ids u
 -> State (MapF (AssignId ids) (DocF ann)) (Doc ann))
-> AssignRhs arch (Value arch ids) tp
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall (m :: Type -> Type) arch (f :: Type -> Type) ann
       (tp :: Type).
(Applicative m, ArchConstraints arch) =>
(forall (u :: Type). f u -> m (Doc ann))
-> AssignRhs arch f tp -> m (Doc ann)
ppAssignRhs Value arch ids u
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall (u :: Type).
Value arch ids u
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
ppVal (Assignment arch ids tp -> AssignRhs arch (Value arch ids) tp
forall arch ids (tp :: Type).
Assignment arch ids tp -> AssignRhs arch (Value arch ids) tp
assignRhs Assignment arch ids tp
a)
    let d :: Doc ann
d = AssignId ids tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId ids tp
lhs 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
<+> Doc ann
rhs
    (MapF (AssignId ids) (DocF ann) -> MapF (AssignId ids) (DocF ann))
-> StateT (MapF (AssignId ids) (DocF ann)) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((MapF (AssignId ids) (DocF ann) -> MapF (AssignId ids) (DocF ann))
 -> StateT (MapF (AssignId ids) (DocF ann)) Identity ())
-> (MapF (AssignId ids) (DocF ann)
    -> MapF (AssignId ids) (DocF ann))
-> StateT (MapF (AssignId ids) (DocF ann)) Identity ()
forall a b. (a -> b) -> a -> b
$ AssignId ids tp
-> DocF ann tp
-> MapF (AssignId ids) (DocF ann)
-> MapF (AssignId ids) (DocF ann)
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
lhs (Doc ann -> DocF ann tp
forall ann (a :: Type). Doc ann -> DocF ann a
DocF Doc ann
d)
    () -> StateT (MapF (AssignId ids) (DocF ann)) Identity ()
forall a. a -> StateT (MapF (AssignId ids) (DocF ann)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
  Doc ann -> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall a. a -> StateT (MapF (AssignId ids) (DocF ann)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Doc ann -> State (MapF (AssignId ids) (DocF ann)) (Doc ann))
-> Doc ann -> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall a b. (a -> b) -> a -> b
$! AssignId ids tp -> Doc ann
forall ids (tp :: Type) ann. AssignId ids tp -> Doc ann
ppAssignId AssignId ids tp
lhs
collectValueRep Prec
p Value arch ids tp
v = Doc ann -> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall a. a -> StateT (MapF (AssignId ids) (DocF ann)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Doc ann -> State (MapF (AssignId ids) (DocF ann)) (Doc ann))
-> Doc ann -> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall a b. (a -> b) -> a -> b
$ Prec -> Value arch ids tp -> Doc ann
forall arch ids (tp :: Type) ann.
ShowF (ArchReg arch) =>
Prec -> Value arch ids tp -> Doc ann
ppValue Prec
p Value arch ids tp
v

-- | This pretty prints all the history used to create a value.
ppValueAssignments' :: State (MapF (AssignId ids) (DocF ann)) (Doc ann) -> Doc ann
ppValueAssignments' :: forall ids ann.
State (MapF (AssignId ids) (DocF ann)) (Doc ann) -> Doc ann
ppValueAssignments' State (MapF (AssignId ids) (DocF ann)) (Doc ann)
m =
  case MapF (AssignId ids) (DocF ann) -> [Some (DocF ann)]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Some a]
MapF.elems MapF (AssignId ids) (DocF ann)
bindings of
    [] -> Doc ann
rhs
    (Some (DocF Doc ann
h):[Some (DocF ann)]
r) ->
      let first :: Doc ann
first               = Doc ann
"let" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
h
          f :: Some (DocF ann) -> Doc ann
f (Some (DocF Doc ann
b))   = Doc ann
"    " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
b
       in [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (Doc ann
firstDoc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
:(Some (DocF ann) -> Doc ann) -> [Some (DocF ann)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Some (DocF ann) -> Doc ann
forall {ann}. Some (DocF ann) -> Doc ann
f [Some (DocF ann)]
r)
               , Doc ann
" in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
rhs ]
  where (Doc ann
rhs, MapF (AssignId ids) (DocF ann)
bindings) = State (MapF (AssignId ids) (DocF ann)) (Doc ann)
-> MapF (AssignId ids) (DocF ann)
-> (Doc ann, MapF (AssignId ids) (DocF ann))
forall s a. State s a -> s -> (a, s)
runState State (MapF (AssignId ids) (DocF ann)) (Doc ann)
m MapF (AssignId ids) (DocF ann)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty

-- | This pretty prints all the history used to create a value.
ppValueAssignments :: ArchConstraints arch => Value arch ids tp -> Doc ann
ppValueAssignments :: forall arch ids (tp :: Type) ann.
ArchConstraints arch =>
Value arch ids tp -> Doc ann
ppValueAssignments Value arch ids tp
v = State (MapF (AssignId ids) (DocF ann)) (Doc ann) -> Doc ann
forall ids ann.
State (MapF (AssignId ids) (DocF ann)) (Doc ann) -> Doc ann
ppValueAssignments' (Prec
-> Value arch ids tp
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall arch ids (tp :: Type) ann.
ArchConstraints arch =>
Prec
-> Value arch ids tp
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
collectValueRep Prec
0 Value arch ids tp
v)

ppValueAssignmentList :: ArchConstraints arch => [Value arch ids tp] -> Doc ann
ppValueAssignmentList :: forall arch ids (tp :: Type) ann.
ArchConstraints arch =>
[Value arch ids tp] -> Doc ann
ppValueAssignmentList [Value arch ids tp]
vals =
  State (MapF (AssignId ids) (DocF ann)) (Doc ann) -> Doc ann
forall ids ann.
State (MapF (AssignId ids) (DocF ann)) (Doc ann) -> Doc ann
ppValueAssignments' (State (MapF (AssignId ids) (DocF ann)) (Doc ann) -> Doc ann)
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann) -> Doc ann
forall a b. (a -> b) -> a -> b
$ do
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Doc ann -> Doc ann)
-> ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hcat ([Doc ann] -> Doc ann)
-> ([Doc ann] -> [Doc ann]) -> [Doc ann] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma
      ([Doc ann] -> Doc ann)
-> StateT (MapF (AssignId ids) (DocF ann)) Identity [Doc ann]
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value arch ids tp
 -> State (MapF (AssignId ids) (DocF ann)) (Doc ann))
-> [Value arch ids tp]
-> StateT (MapF (AssignId ids) (DocF ann)) Identity [Doc ann]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Prec
-> Value arch ids tp
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
forall arch ids (tp :: Type) ann.
ArchConstraints arch =>
Prec
-> Value arch ids tp
-> State (MapF (AssignId ids) (DocF ann)) (Doc ann)
collectValueRep Prec
0) [Value arch ids tp]
vals

------------------------------------------------------------------------
-- Pretty printing RegState

-- | This class provides a way of optionally pretty printing the contents
-- of a register or omitting them.
class PrettyRegValue r (f :: Type -> Kind.Type) where
  -- | ppValueEq should return a doc if the contents of the given register
  -- should be printed, and Nothing if the contents should be ignored.
  ppValueEq :: r tp -> f tp -> Maybe (Doc ann)

ppRegMap :: forall r v ann . PrettyRegValue r v => MapF.MapF r v -> Doc ann
ppRegMap :: forall (r :: Type -> Type) (v :: Type -> Type) ann.
PrettyRegValue r v =>
MapF r v -> Doc ann
ppRegMap MapF r v
m = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
bracketsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Maybe (Doc ann)] -> [Doc ann]
forall a. [Maybe a] -> [a]
catMaybes (Pair r v -> Maybe (Doc ann)
f (Pair r v -> Maybe (Doc ann)) -> [Pair r v] -> [Maybe (Doc ann)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> MapF r v -> [Pair r v]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Pair k2 a]
MapF.toList MapF r v
m)
  where f :: MapF.Pair r v -> Maybe (Doc ann)
        f :: Pair r v -> Maybe (Doc ann)
f (MapF.Pair r tp
r v tp
v) = r tp -> v tp -> Maybe (Doc ann)
forall (tp :: Type) ann. r tp -> v tp -> Maybe (Doc ann)
forall (r :: Type -> Type) (f :: Type -> Type) (tp :: Type) ann.
PrettyRegValue r f =>
r tp -> f tp -> Maybe (Doc ann)
ppValueEq r tp
r v tp
v


instance ( PrettyRegValue r f)
      => Pretty (RegState r f) where
  pretty :: forall ann. RegState r f -> Doc ann
pretty (RegState MapF r f
m) = MapF r f -> Doc ann
forall (r :: Type -> Type) (v :: Type -> Type) ann.
PrettyRegValue r v =>
MapF r v -> Doc ann
ppRegMap MapF r f
m

instance ( PrettyRegValue r f
         )
      => Show (RegState r f) where
  show :: RegState r f -> String
show RegState r f
s = Doc Any -> String
forall a. Show a => a -> String
show (RegState r f -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. RegState r f -> Doc ann
pretty RegState r f
s)

instance ( RegisterInfo r
         , r ~ ArchReg arch
         )
      => PrettyRegValue r (Value arch ids) where
  ppValueEq :: forall (tp :: Type) ann.
r tp -> Value arch ids tp -> Maybe (Doc ann)
ppValueEq r tp
r (Initial ArchReg arch tp
r')
    | Just tp :~: tp
_ <- r tp -> r tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type). r a -> r b -> Maybe (a :~: b)
testEquality r tp
r r tp
ArchReg arch tp
r' = Maybe (Doc ann)
forall a. Maybe a
Nothing
  ppValueEq r tp
r Value arch ids tp
v
    | Bool
otherwise   = Doc ann -> Maybe (Doc ann)
forall a. a -> Maybe a
Just (Doc ann -> Maybe (Doc ann)) -> Doc ann -> Maybe (Doc ann)
forall a b. (a -> b) -> a -> b
$ 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
<+> Value arch ids tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Value arch ids tp -> Doc ann
pretty Value arch ids tp
v

------------------------------------------------------------------------
-- Stmt

-- | A statement in our control flow graph language.
data Stmt arch ids
   = forall tp . AssignStmt !(Assignment arch ids tp)
   | forall tp . WriteMem !(ArchAddrValue arch ids) !(MemRepr tp) !(Value arch ids tp)
     -- ^ This denotes a write to memory, and consists of an address
     -- to write to, a `MemRepr` defining how the value should be
     -- stored in memory, and the value to be written.
  | forall tp .
    CondWriteMem !(Value arch ids BoolType)
                 !(ArchAddrValue arch ids)
                 !(MemRepr tp)
                 !(Value arch ids tp)
     -- ^ This denotes a write to memory that only executes if the
     -- condition is true.
   | InstructionStart !(ArchAddrWord arch) !Text
     -- ^ The start of an instruction
     --
     -- The information includes the offset relative to the start of
     -- the block and the disassembler output if available (or empty
     -- string if unavailable)
   | Comment !Text
     -- ^ A user-level comment
   | ExecArchStmt !(ArchStmt arch (Value arch ids))
     -- ^ Execute an architecture specific statement
   | ArchState !(ArchMemAddr arch) !(MapF.MapF (ArchReg arch) (Value arch ids))
     -- ^ Address of an instruction and the *machine* registers that
     -- it updates (with their associated macaw values after the
     -- execution of the instruction).

ppStmt :: ArchConstraints arch
       => (ArchAddrWord arch -> Doc ann)
          -- ^ Function for pretty printing an instruction address offset
       -> Stmt arch ids
       -> Doc ann
ppStmt :: forall arch ann ids.
ArchConstraints arch =>
(ArchAddrWord arch -> Doc ann) -> Stmt arch ids -> Doc ann
ppStmt ArchAddrWord arch -> Doc ann
ppOff Stmt arch ids
stmt =
  case Stmt arch ids
stmt of
    AssignStmt Assignment arch ids tp
a -> Assignment arch ids tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Assignment arch ids tp -> Doc ann
pretty Assignment arch ids tp
a
    WriteMem     BVValue arch ids (RegAddrWidth (ArchReg arch))
a MemRepr tp
_ Value arch ids tp
rhs ->
      Doc ann
"write_mem" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Prec -> BVValue arch ids (RegAddrWidth (ArchReg arch)) -> Doc ann
forall ann.
Prec -> BVValue arch ids (RegAddrWidth (ArchReg arch)) -> Doc ann
forall v ann. PrettyPrec v => Prec -> v -> Doc ann
prettyPrec Prec
11 BVValue arch ids (RegAddrWidth (ArchReg arch))
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Prec -> Value arch ids tp -> Doc ann
forall arch ids (tp :: Type) ann.
ShowF (ArchReg arch) =>
Prec -> Value arch ids tp -> Doc ann
ppValue Prec
0 Value arch ids tp
rhs
    CondWriteMem Value arch ids BoolType
c BVValue arch ids (RegAddrWidth (ArchReg arch))
a MemRepr tp
_ Value arch ids tp
rhs ->
      Doc ann
"cond_write_mem" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Prec -> Value arch ids BoolType -> Doc ann
forall ann. Prec -> Value arch ids BoolType -> Doc ann
forall v ann. PrettyPrec v => Prec -> v -> Doc ann
prettyPrec Prec
11 Value arch ids BoolType
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Prec -> BVValue arch ids (RegAddrWidth (ArchReg arch)) -> Doc ann
forall ann.
Prec -> BVValue arch ids (RegAddrWidth (ArchReg arch)) -> Doc ann
forall v ann. PrettyPrec v => Prec -> v -> Doc ann
prettyPrec Prec
11 BVValue arch ids (RegAddrWidth (ArchReg arch))
a
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Prec -> Value arch ids tp -> Doc ann
forall arch ids (tp :: Type) ann.
ShowF (ArchReg arch) =>
Prec -> Value arch ids tp -> Doc ann
ppValue Prec
0 Value arch ids tp
rhs
    InstructionStart ArchAddrWord arch
off Text
mnem -> Doc ann
"#" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ArchAddrWord arch -> Doc ann
ppOff ArchAddrWord arch
off Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Text -> Doc ann
pretty Text
mnem
    Comment Text
s -> Doc ann
"# " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Text -> Doc ann
pretty Text
s
    ExecArchStmt ArchStmt arch (Value arch ids)
s -> (forall (u :: Type). Value arch ids u -> Doc ann)
-> ArchStmt arch (Value arch ids) -> Doc ann
forall (v :: Type -> Type) ann.
(forall (u :: Type). v u -> Doc ann) -> ArchStmt arch v -> Doc ann
forall (f :: (Type -> Type) -> Type) (v :: Type -> Type) ann.
IsArchStmt f =>
(forall (u :: Type). v u -> Doc ann) -> f v -> Doc ann
ppArchStmt (Prec -> Value arch ids u -> Doc ann
forall arch ids (tp :: Type) ann.
ShowF (ArchReg arch) =>
Prec -> Value arch ids tp -> Doc ann
ppValue Prec
10) ArchStmt arch (Value arch ids)
s
    ArchState ArchMemAddr arch
a MapF (ArchReg arch) (Value arch ids)
m ->
        Prec -> Doc ann -> Doc ann
forall ann. Prec -> Doc ann -> Doc ann
hang (String -> Prec
forall a. [a] -> Prec
forall (t :: Type -> Type) a. Foldable t => t a -> Prec
length (Doc ann -> String
forall a. Show a => a -> String
show Doc ann
prefix)) (Doc ann
prefix Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
PP.encloseSep Doc ann
forall ann. Doc ann
PP.lbrace Doc ann
forall ann. Doc ann
PP.rbrace Doc ann
forall ann. Doc ann
PP.semi ((forall (s :: Type).
 ArchReg arch s -> Value arch ids s -> [Doc ann] -> [Doc ann])
-> [Doc ann] -> MapF (ArchReg arch) (Value arch ids) -> [Doc ann]
forall {v} (k :: v -> Type) (a :: v -> Type) b.
(forall (s :: v). k s -> a s -> b -> b) -> b -> MapF k a -> b
MapF.foldrWithKey ArchReg arch s -> Value arch ids s -> [Doc ann] -> [Doc ann]
forall {k} {f :: k -> Type} {arch} {tp :: k} {ids} {tp :: Type}
       {ann}.
(ShowF f, ShowF (ArchReg arch)) =>
f tp -> Value arch ids tp -> [Doc ann] -> [Doc ann]
forall (s :: Type).
ArchReg arch s -> Value arch ids s -> [Doc ann] -> [Doc ann]
ppUpdate [] MapF (ArchReg arch) (Value arch ids)
m))
      where
      ppAddr :: MemAddr w -> Doc ann
ppAddr MemAddr w
addr =
        case MemAddr w -> Maybe (MemWord w)
forall (w :: Natural). MemWidth w => MemAddr w -> Maybe (MemWord w)
asAbsoluteAddr MemAddr w
addr of
          Just MemWord w
absAddr -> MemWord w -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow MemWord w
absAddr
          Maybe (MemWord w)
Nothing -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
PP.braces (Prec -> Doc ann
forall ann. Prec -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (MemAddr w -> Prec
forall (w :: Natural). MemAddr w -> Prec
addrBase MemAddr w
addr)) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
"+" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> MemWord w -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (MemAddr w -> MemWord w
forall (w :: Natural). MemAddr w -> MemWord w
addrOffset MemAddr w
addr)
      prefix :: Doc ann
prefix = Doc ann
"#" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ArchMemAddr arch -> Doc ann
forall {w :: Natural} {ann}.
(Assert (OrdCond (CmpNat 1 w) 'True 'True 'False) (TypeError ...),
 MemWidth w) =>
MemAddr w -> Doc ann
ppAddr ArchMemAddr arch
a Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
": "
      ppUpdate :: f tp -> Value arch ids tp -> [Doc ann] -> [Doc ann]
ppUpdate f tp
key Value arch ids tp
val [Doc ann]
acc = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (f tp -> String
forall (tp :: k). f tp -> String
forall k (f :: k -> Type) (tp :: k). ShowF f => f tp -> String
showF f tp
key) 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
<+> Prec -> Value arch ids tp -> Doc ann
forall arch ids (tp :: Type) ann.
ShowF (ArchReg arch) =>
Prec -> Value arch ids tp -> Doc ann
ppValue Prec
0 Value arch ids tp
val Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [Doc ann]
acc

instance ArchConstraints arch => Show (Stmt arch ids) where
  show :: Stmt arch ids -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (Stmt arch ids -> Doc Any) -> Stmt arch ids -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MemWord (RegAddrWidth (ArchReg arch)) -> Doc Any)
-> Stmt arch ids -> Doc Any
forall arch ann ids.
ArchConstraints arch =>
(ArchAddrWord arch -> Doc ann) -> Stmt arch ids -> Doc ann
ppStmt MemWord (RegAddrWidth (ArchReg arch)) -> Doc Any
forall a ann. Show a => a -> Doc ann
viaShow

------------------------------------------------------------------------
-- References

refsInValue :: Value arch ids tp -> Set (Some (AssignId ids))
refsInValue :: forall arch ids (tp :: Type).
Value arch ids tp -> Set (Some (AssignId ids))
refsInValue (AssignedValue (Assignment AssignId ids tp
v AssignRhs arch (Value arch ids) tp
_)) = Some (AssignId ids) -> Set (Some (AssignId ids))
forall a. a -> Set a
Set.singleton (AssignId ids tp -> Some (AssignId ids)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some AssignId ids tp
v)
refsInValue Value arch ids tp
_                                = Set (Some (AssignId ids))
forall a. Set a
Set.empty