{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Macaw.CFG.AssignRhs
  ( AssignRhs(..)
    -- * MemRepr
  , MemRepr(..)
  , memReprBytes
    -- * Architecture type families
  , RegAddrWidth
  , ArchReg
  , ArchFn
  , ArchStmt
  , ArchTermStmt
    -- * Synonyms
  , RegAddrWord
  , ArchAddrWidth
  , ArchAddrWord
  , ArchMemAddr
  ) where

import qualified Data.Kind as Kind
import           Data.Macaw.CFG.App
import           Data.Macaw.Memory (Endianness(..), MemWord, MemAddr)
import           Data.Macaw.Types
import           Data.Parameterized.Classes
import           Data.Parameterized.NatRepr
import           Data.Parameterized.TraversableFC (FoldableFC(..))
import           Data.Proxy
import           Numeric.Natural
import           Prettyprinter

-- | Width of register used to store addresses.
type family RegAddrWidth (r :: Type -> Kind.Type) :: Nat

-- | A word for the given architecture register type.
type RegAddrWord r = MemWord (RegAddrWidth r)

-- | Type family for defining what a "register" is for this architecture.
--
-- Registers include things like the general purpose registers, any flag
-- registers that can be read and written without side effects,
type family ArchReg (arch :: Kind.Type) = (reg :: Type -> Kind.Type) | reg -> arch
  -- Note the injectivity constraint. This makes GHC quit bothering us
  -- about ambigous types for functions taking ArchRegs as arguments.

-- | A type family for architecture specific functions.
--
-- The functions associated with architecture-function depend on the
-- contents of memory and implicit components of the processor state,
-- but they should not affect any of the architecture
-- registers in @ArchReg arch@.
--
-- Architecture specific functions are required to implement
-- `FoldableFC`, and the evaluation of an architecture specific
-- function may only depend on the value stored in a general purpose
-- register if it is given through the @fn@ parameter and provided
-- when folding over values.  This is required for accurate def-use
-- analysis of general purpose registers.
type family ArchFn (arch :: Kind.Type) = (fn :: (Type -> Kind.Type) -> Type -> Kind.Type) | fn -> arch

-- | A type family for defining architecture-specific statements.
--
-- The second parameter is used to denote the underlying values in the
-- statements so that we can use ArchStmts with multiple CFGs.
type family ArchStmt (arch :: Kind.Type) = (stmt :: (Type -> Kind.Type) -> Kind.Type) | stmt -> arch

-- | A type family for defining architecture-specific statements that
-- may have instruction-specific effects on control-flow and register state.
--
-- An architecture-specific terminal statement may have side effects and change register
-- values, it may or may not return to the current function.
--
-- Note that the meaning of the type parameter is identical to that of 'ArchStmt'
type family ArchTermStmt (arch :: Kind.Type) :: (Type -> Kind.Type) -> Kind.Type
   -- NOTE: Not injective because PPC32 and PPC64 use the same type.

-- | Number of bits in addreses for architecture.
type ArchAddrWidth arch = RegAddrWidth (ArchReg arch)

-- | A word for the given architecture bitwidth.
type ArchAddrWord arch = RegAddrWord (ArchReg arch)

-- | An address for a given architecture.
type ArchMemAddr arch = MemAddr (ArchAddrWidth arch)

------------------------------------------------------------------------
-- MemRepr

-- | The provides information sufficient to read supported types of values from
-- memory such as the number of bytes and endianness.
data MemRepr (tp :: Type) where
  -- | Denotes a bitvector with the given number of bytes and endianness.
  BVMemRepr :: (1 <= w) => !(NatRepr w) -> !Endianness -> MemRepr (BVType (8*w))
  -- | A floating point value (stored in given endianness.
  FloatMemRepr :: !(FloatInfoRepr f) -> !Endianness -> MemRepr (FloatType f)
  -- | A vector of values with zero entry first.
  --
  -- The first value is stored at the address, the second is stored at
  -- address + sizeof eltType, etc.
  PackedVecMemRepr :: !(NatRepr n) -> !(MemRepr tp) -> MemRepr (VecType n tp)

ppEndianness :: Endianness -> Doc ann
ppEndianness :: forall ann. Endianness -> Doc ann
ppEndianness Endianness
LittleEndian = Doc ann
"le"
ppEndianness Endianness
BigEndian    = Doc ann
"be"

instance Pretty (MemRepr tp) where
  pretty :: forall ann. MemRepr tp -> Doc ann
pretty (BVMemRepr NatRepr w
w Endianness
end) = Doc ann
"bv" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Endianness -> Doc ann
forall ann. Endianness -> Doc ann
ppEndianness Endianness
end Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> NatRepr w -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr w
w
  pretty (FloatMemRepr FloatInfoRepr f
f Endianness
end) = FloatInfoRepr f -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FloatInfoRepr f -> Doc ann
pretty FloatInfoRepr f
f Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Endianness -> Doc ann
forall ann. Endianness -> Doc ann
ppEndianness Endianness
end
  pretty (PackedVecMemRepr NatRepr n
w MemRepr tp
r) = Doc ann
"v" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> NatRepr n -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr n
w Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> MemRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. MemRepr tp -> Doc ann
pretty MemRepr tp
r

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

-- | Return the number of bytes this uses in memory.
memReprBytes :: MemRepr tp -> Natural
memReprBytes :: forall (tp :: Type). MemRepr tp -> Natural
memReprBytes (BVMemRepr NatRepr w
x Endianness
_) = NatRepr w -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
x
memReprBytes (FloatMemRepr FloatInfoRepr f
f Endianness
_) = NatRepr (FloatInfoBytes f) -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue (FloatInfoRepr f -> NatRepr (FloatInfoBytes f)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi)
floatInfoBytes FloatInfoRepr f
f)
memReprBytes (PackedVecMemRepr NatRepr n
w MemRepr tp
r) = NatRepr n -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr n
w Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* MemRepr tp -> Natural
forall (tp :: Type). MemRepr tp -> Natural
memReprBytes MemRepr tp
r

instance TestEquality MemRepr where
  testEquality :: forall (a :: Type) (b :: Type).
MemRepr a -> MemRepr b -> Maybe (a :~: b)
testEquality (BVMemRepr NatRepr w
xw Endianness
xe) (BVMemRepr NatRepr w
yw Endianness
ye) = do
    w :~: w
Refl <- NatRepr w -> NatRepr w -> Maybe (w :~: w)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
xw NatRepr w
yw
    if Endianness
xe Endianness -> Endianness -> Bool
forall a. Eq a => a -> a -> Bool
== Endianness
ye 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 (FloatMemRepr FloatInfoRepr f
xf Endianness
xe) (FloatMemRepr FloatInfoRepr f
yf Endianness
ye) = do
    f :~: f
Refl <- FloatInfoRepr f -> FloatInfoRepr f -> Maybe (f :~: f)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: FloatInfo) (b :: FloatInfo).
FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b)
testEquality FloatInfoRepr f
xf FloatInfoRepr f
yf
    if Endianness
xe Endianness -> Endianness -> Bool
forall a. Eq a => a -> a -> Bool
== Endianness
ye 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 (PackedVecMemRepr NatRepr n
xn MemRepr tp
xe) (PackedVecMemRepr NatRepr n
yn MemRepr tp
ye) = 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
xn NatRepr n
yn
    tp :~: tp
Refl <- MemRepr tp -> MemRepr tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
MemRepr a -> MemRepr b -> Maybe (a :~: b)
testEquality MemRepr tp
xe MemRepr tp
ye
    (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality MemRepr a
_ MemRepr b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance Eq (MemRepr tp) where
  MemRepr tp
a == :: MemRepr tp -> MemRepr tp -> Bool
== MemRepr tp
b = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (MemRepr tp -> MemRepr tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Type) (b :: Type).
MemRepr a -> MemRepr b -> Maybe (a :~: b)
testEquality MemRepr tp
a MemRepr tp
b)

instance Hashable (MemRepr tp) where
  hashWithSalt :: Int -> MemRepr tp -> Int
hashWithSalt Int
s MemRepr tp
mr =
    case MemRepr tp
mr of
      BVMemRepr NatRepr w
w Endianness
e        -> Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0::Int) Int -> NatRepr w -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` NatRepr w
w Int -> Endianness -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Endianness
e
      FloatMemRepr FloatInfoRepr f
r Endianness
e     -> Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1::Int) Int -> FloatInfoRepr f -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` FloatInfoRepr f
r Int -> Endianness -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Endianness
e
      PackedVecMemRepr NatRepr n
n MemRepr tp
e -> Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2::Int) Int -> NatRepr n -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` NatRepr n
n Int -> MemRepr tp -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` MemRepr tp
e

instance HashableF MemRepr where
  hashWithSaltF :: forall (tp :: Type). Int -> MemRepr tp -> Int
hashWithSaltF = Int -> MemRepr tp -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt

instance OrdF MemRepr where
  compareF :: forall (x :: Type) (y :: Type).
MemRepr x -> MemRepr y -> OrderingF x y
compareF (BVMemRepr NatRepr w
xw Endianness
xe) (BVMemRepr NatRepr w
yw Endianness
ye) =
    OrderingF w w -> ((w ~ w) => OrderingF x y) -> OrderingF x y
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (NatRepr w -> NatRepr w -> OrderingF w w
forall (x :: Natural) (y :: Natural).
NatRepr x -> NatRepr y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF NatRepr w
xw NatRepr w
yw) (((w ~ w) => OrderingF x y) -> OrderingF x y)
-> ((w ~ w) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
     Ordering -> OrderingF x x
forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (Endianness -> Endianness -> Ordering
forall a. Ord a => a -> a -> Ordering
compare  Endianness
xe Endianness
ye)
  compareF BVMemRepr{} MemRepr y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF MemRepr x
_ BVMemRepr{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
  compareF (FloatMemRepr FloatInfoRepr f
xf Endianness
xe) (FloatMemRepr FloatInfoRepr f
yf Endianness
ye) =
    OrderingF f f -> ((f ~ f) => OrderingF x y) -> OrderingF x y
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (FloatInfoRepr f -> FloatInfoRepr f -> OrderingF f f
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: FloatInfo) (y :: FloatInfo).
FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y
compareF FloatInfoRepr f
xf FloatInfoRepr f
yf) (((f ~ f) => OrderingF x y) -> OrderingF x y)
-> ((f ~ f) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    Ordering -> OrderingF x x
forall {k} (x :: k). Ordering -> OrderingF x x
fromOrdering (Endianness -> Endianness -> Ordering
forall a. Ord a => a -> a -> Ordering
compare  Endianness
xe Endianness
ye)
  compareF FloatMemRepr{} MemRepr y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF MemRepr x
_ FloatMemRepr{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
  compareF (PackedVecMemRepr NatRepr n
xn MemRepr tp
xe) (PackedVecMemRepr NatRepr n
yn MemRepr tp
ye) =
    OrderingF n n -> ((n ~ n) => OrderingF x y) -> OrderingF x y
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (NatRepr 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
xn NatRepr n
yn) (((n ~ n) => OrderingF x y) -> OrderingF x y)
-> ((n ~ n) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    OrderingF tp tp -> ((tp ~ tp) => OrderingF x y) -> OrderingF x y
forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (MemRepr tp -> MemRepr 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).
MemRepr x -> MemRepr y -> OrderingF x y
compareF  MemRepr tp
xe MemRepr tp
ye) (((tp ~ tp) => OrderingF x y) -> OrderingF x y)
-> ((tp ~ tp) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    OrderingF x x
OrderingF x y
(tp ~ tp) => OrderingF x y
forall {k} (x :: k). OrderingF x x
EQF

instance HasRepr MemRepr TypeRepr where
  typeRepr :: forall (tp :: Type). MemRepr tp -> TypeRepr tp
typeRepr (BVMemRepr NatRepr w
w Endianness
_) =
    let r :: NatRepr (8 * w)
r = (NatRepr 8 -> NatRepr w -> NatRepr (8 * w)
forall (n :: Natural) (m :: Natural).
NatRepr n -> NatRepr m -> NatRepr (n * m)
natMultiply NatRepr 8
n8 NatRepr w
w)
     in case Proxy 8 -> NatRepr w -> LeqProof 1 (8 * w)
forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
       (y :: Natural).
(1 <= x, 1 <= y) =>
p x -> q y -> LeqProof 1 (x * y)
leqMulPos (Proxy 8
forall {k} (t :: k). Proxy t
Proxy :: Proxy 8) NatRepr w
w of
          LeqProof 1 (8 * w)
LeqProof -> NatRepr (8 * w) -> TypeRepr ('BVType (8 * w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BVType n)
BVTypeRepr NatRepr (8 * w)
r
  typeRepr (FloatMemRepr FloatInfoRepr f
f Endianness
_) = FloatInfoRepr f -> TypeRepr ('FloatType f)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> TypeRepr ('FloatType fi)
FloatTypeRepr FloatInfoRepr f
f
  typeRepr (PackedVecMemRepr NatRepr n
n MemRepr tp
e) = NatRepr n -> TypeRepr tp -> TypeRepr ('VecType n tp)
forall (n :: Natural) (tp1 :: Type).
NatRepr n -> TypeRepr tp1 -> TypeRepr ('VecType n tp1)
VecTypeRepr NatRepr n
n (MemRepr tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). MemRepr tp -> TypeRepr tp
typeRepr MemRepr tp
e)

------------------------------------------------------------------------
-- AssignRhs

-- | The right hand side of an assignment is an expression that
-- returns a value.
data AssignRhs (arch :: Kind.Type) (f :: Type -> Kind.Type) tp where
  -- | An expression that is computed from evaluating subexpressions.
  EvalApp :: !(App f tp)
          -> AssignRhs arch f tp

  -- | An expression with an undefined value.
  SetUndefined :: !(TypeRepr tp)
               -> AssignRhs arch f tp

  -- | Read memory at given location.
  ReadMem :: !(f (BVType (ArchAddrWidth arch)))
          -> !(MemRepr tp)
          -> AssignRhs arch f tp

  -- | @CondReadMem tp cond addr v@ reads from memory at the given address if the
  -- condition is true and returns the value if it false.
  CondReadMem :: !(MemRepr tp)
              -> !(f BoolType)
              -> !(f (BVType (ArchAddrWidth arch)))
              -> !(f tp)
              -> AssignRhs arch f tp

  -- Call an architecture specific function that returns some result.
  EvalArchFn :: !(ArchFn arch f tp)
             -> !(TypeRepr tp)
             -> AssignRhs arch f tp

instance HasRepr (AssignRhs arch f) TypeRepr where
  typeRepr :: forall (tp :: Type). AssignRhs arch f tp -> TypeRepr tp
typeRepr AssignRhs arch f tp
rhs =
    case AssignRhs arch f tp
rhs of
      EvalApp App f tp
a -> App f tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). App f tp -> TypeRepr tp
typeRepr App f tp
a
      SetUndefined TypeRepr tp
tp -> TypeRepr tp
tp
      ReadMem f (BVType (ArchAddrWidth arch))
_ MemRepr tp
tp -> MemRepr tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). MemRepr tp -> TypeRepr tp
typeRepr MemRepr tp
tp
      CondReadMem MemRepr tp
tp f BoolType
_ f (BVType (ArchAddrWidth arch))
_ f tp
_ -> MemRepr tp -> TypeRepr tp
forall k (f :: k -> Type) (v :: k -> Type) (tp :: k).
HasRepr f v =>
f tp -> v tp
forall (tp :: Type). MemRepr tp -> TypeRepr tp
typeRepr MemRepr tp
tp
      EvalArchFn ArchFn arch f tp
_ TypeRepr tp
rtp -> TypeRepr tp
rtp

instance FoldableFC (ArchFn arch) => FoldableFC (AssignRhs arch) where
  foldMapFC :: forall (f :: Type -> Type) m.
Monoid m =>
(forall (x :: Type). f x -> m)
-> forall (x :: Type). AssignRhs arch f x -> m
foldMapFC forall (x :: Type). f x -> m
go AssignRhs arch f x
v =
    case AssignRhs arch f x
v of
      EvalApp App f x
a -> (forall (x :: Type). f x -> m) -> forall (x :: Type). App f x -> m
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) m.
(FoldableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
forall (f :: Type -> Type) m.
Monoid m =>
(forall (x :: Type). f x -> m) -> forall (x :: Type). App f x -> m
foldMapFC f x -> m
forall (x :: Type). f x -> m
go App f x
a
      SetUndefined TypeRepr x
_w -> m
forall a. Monoid a => a
mempty
      ReadMem f (BVType (ArchAddrWidth arch))
addr MemRepr x
_ -> f (BVType (ArchAddrWidth arch)) -> m
forall (x :: Type). f x -> m
go f (BVType (ArchAddrWidth arch))
addr
      CondReadMem MemRepr x
_ f BoolType
c f (BVType (ArchAddrWidth arch))
a f x
d -> f BoolType -> m
forall (x :: Type). f x -> m
go f BoolType
c m -> m -> m
forall a. Semigroup a => a -> a -> a
<> f (BVType (ArchAddrWidth arch)) -> m
forall (x :: Type). f x -> m
go f (BVType (ArchAddrWidth arch))
a m -> m -> m
forall a. Semigroup a => a -> a -> a
<> f x -> m
forall (x :: Type). f x -> m
go f x
d
      EvalArchFn ArchFn arch f x
f TypeRepr x
_ -> (forall (x :: Type). f x -> m)
-> forall (x :: Type). ArchFn arch f x -> m
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) m.
(FoldableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
forall (f :: Type -> Type) m.
Monoid m =>
(forall (x :: Type). f x -> m)
-> forall (x :: Type). ArchFn arch f x -> m
foldMapFC f x -> m
forall (x :: Type). f x -> m
go ArchFn arch f x
f