{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.LLVM.Extension.Syntax where
import Data.Kind
import Data.List.NonEmpty (NonEmpty)
import GHC.TypeLits
import Data.Text (Text)
import qualified Text.LLVM.AST as L
import Prettyprinter
import Data.Functor.Classes (Eq1(..), Ord1(..))
import Data.Parameterized.Classes
import Data.Parameterized.ClassesC (TestEqualityC(..), OrdC(..))
import qualified Data.Parameterized.TH.GADT as U
import Data.Parameterized.TraversableF
import Data.Parameterized.TraversableFC
import Lang.Crucible.CFG.Common
import Lang.Crucible.CFG.Extension
import Lang.Crucible.Types
import Lang.Crucible.LLVM.Arch.X86 as X86
import Lang.Crucible.LLVM.Bytes
import Lang.Crucible.LLVM.DataLayout
import Lang.Crucible.LLVM.Errors.UndefinedBehavior( UndefinedBehavior )
import Lang.Crucible.LLVM.MemModel.Pointer
import Lang.Crucible.LLVM.MemModel.Type
import Lang.Crucible.LLVM.Types
data LLVMSideCondition (f :: CrucibleType -> Type) =
LLVMSideCondition (f BoolType) (UndefinedBehavior f)
instance TestEqualityC LLVMSideCondition where
testEqualityC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y))
-> LLVMSideCondition f -> LLVMSideCondition f -> Bool
testEqualityC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
sub (LLVMSideCondition f BoolType
px UndefinedBehavior f
dx) (LLVMSideCondition f BoolType
py UndefinedBehavior f
dy) =
Maybe (BoolType :~: BoolType) -> Bool
forall a. Maybe a -> Bool
isJust (f BoolType -> f BoolType -> Maybe (BoolType :~: BoolType)
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
sub f BoolType
px f BoolType
py) Bool -> Bool -> Bool
&& (forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y))
-> UndefinedBehavior f -> UndefinedBehavior f -> Bool
forall k (t :: (k -> Type) -> Type) (f :: k -> Type).
TestEqualityC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> t f -> t f -> Bool
forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y))
-> UndefinedBehavior f -> UndefinedBehavior f -> Bool
testEqualityC f x -> f y -> Maybe (x :~: y)
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
sub UndefinedBehavior f
dx UndefinedBehavior f
dy
instance OrdC LLVMSideCondition where
compareC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y)
-> LLVMSideCondition f -> LLVMSideCondition g -> Ordering
compareC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y
sub (LLVMSideCondition f BoolType
px UndefinedBehavior f
dx) (LLVMSideCondition g BoolType
py UndefinedBehavior g
dy) =
OrderingF BoolType BoolType -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (f BoolType -> g BoolType -> OrderingF BoolType BoolType
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y
sub f BoolType
px g BoolType
py) Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> (forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y)
-> UndefinedBehavior f -> UndefinedBehavior g -> Ordering
forall k (t :: (k -> Type) -> Type) (f :: k -> Type)
(g :: k -> Type).
OrdC t =>
(forall (x :: k) (y :: k). f x -> g y -> OrderingF x y)
-> t f -> t g -> Ordering
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y)
-> UndefinedBehavior f -> UndefinedBehavior g -> Ordering
compareC f x -> g y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y
sub UndefinedBehavior f
dx UndefinedBehavior g
dy
instance FunctorF LLVMSideCondition where
fmapF :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> LLVMSideCondition f -> LLVMSideCondition g
fmapF = (forall (s :: CrucibleType). f s -> g s)
-> LLVMSideCondition f -> LLVMSideCondition g
forall {k} (t :: (k -> Type) -> Type) (e :: k -> Type)
(f :: k -> Type).
TraversableF t =>
(forall (s :: k). e s -> f s) -> t e -> t f
fmapFDefault
instance FoldableF LLVMSideCondition where
foldMapF :: forall m (e :: CrucibleType -> Type).
Monoid m =>
(forall (s :: CrucibleType). e s -> m) -> LLVMSideCondition e -> m
foldMapF = (forall (s :: CrucibleType). e s -> m) -> LLVMSideCondition e -> m
forall {k} (t :: (k -> Type) -> Type) m (e :: k -> Type).
(TraversableF t, Monoid m) =>
(forall (s :: k). e s -> m) -> t e -> m
foldMapFDefault
instance TraversableF LLVMSideCondition where
traverseF :: forall (m :: Type -> Type) (e :: CrucibleType -> Type)
(f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> LLVMSideCondition e -> m (LLVMSideCondition f)
traverseF forall (s :: CrucibleType). e s -> m (f s)
f (LLVMSideCondition e BoolType
p UndefinedBehavior e
desc) =
f BoolType -> UndefinedBehavior f -> LLVMSideCondition f
forall (f :: CrucibleType -> Type).
f BoolType -> UndefinedBehavior f -> LLVMSideCondition f
LLVMSideCondition (f BoolType -> UndefinedBehavior f -> LLVMSideCondition f)
-> m (f BoolType) -> m (UndefinedBehavior f -> LLVMSideCondition f)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e BoolType -> m (f BoolType)
forall (s :: CrucibleType). e s -> m (f s)
f e BoolType
p m (UndefinedBehavior f -> LLVMSideCondition f)
-> m (UndefinedBehavior f) -> m (LLVMSideCondition f)
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
<*> (forall (s :: CrucibleType). e s -> m (f s))
-> UndefinedBehavior e -> m (UndefinedBehavior 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 :: CrucibleType -> Type)
(f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> UndefinedBehavior e -> m (UndefinedBehavior f)
traverseF e s -> m (f s)
forall (s :: CrucibleType). e s -> m (f s)
f UndefinedBehavior e
desc
data LLVMExtensionExpr :: (CrucibleType -> Type) -> (CrucibleType -> Type) where
X86Expr ::
!(X86.ExtX86 f t) ->
LLVMExtensionExpr f t
LLVM_SideConditions ::
!(GlobalVar Mem) ->
!(TypeRepr tp) ->
!(NonEmpty (LLVMSideCondition f)) ->
!(f tp) ->
LLVMExtensionExpr f tp
LLVM_PointerExpr ::
(1 <= w) => !(NatRepr w) -> !(f NatType) -> !(f (BVType w)) ->
LLVMExtensionExpr f (LLVMPointerType w)
LLVM_PointerBlock ::
(1 <= w) => !(NatRepr w) -> !(f (LLVMPointerType w)) ->
LLVMExtensionExpr f NatType
LLVM_PointerOffset ::
(1 <= w) => !(NatRepr w) -> !(f (LLVMPointerType w)) ->
LLVMExtensionExpr f (BVType w)
LLVM_PointerIte ::
(1 <= w) => !(NatRepr w) ->
!(f BoolType) -> !(f (LLVMPointerType w)) -> !(f (LLVMPointerType w)) ->
LLVMExtensionExpr f (LLVMPointerType w)
data LLVMStmt (f :: CrucibleType -> Type) :: CrucibleType -> Type where
LLVM_PushFrame ::
!Text ->
!(GlobalVar Mem) ->
LLVMStmt f UnitType
LLVM_PopFrame ::
!(GlobalVar Mem) ->
LLVMStmt f UnitType
LLVM_Alloca ::
HasPtrWidth wptr =>
!(NatRepr wptr) ->
!(GlobalVar Mem) ->
!(f (BVType wptr)) ->
!Alignment ->
!String ->
LLVMStmt f (LLVMPointerType wptr)
LLVM_Load ::
HasPtrWidth wptr =>
!(GlobalVar Mem) ->
!(f (LLVMPointerType wptr)) ->
!(TypeRepr tp) ->
!StorageType ->
!Alignment ->
LLVMStmt f tp
LLVM_Store ::
HasPtrWidth wptr =>
!(GlobalVar Mem) ->
!(f (LLVMPointerType wptr)) ->
!(TypeRepr tp) ->
!StorageType ->
!Alignment ->
!(f tp) ->
LLVMStmt f UnitType
LLVM_MemClear ::
HasPtrWidth wptr =>
!(GlobalVar Mem) ->
!(f (LLVMPointerType wptr)) ->
!Bytes ->
LLVMStmt f UnitType
LLVM_LoadHandle ::
HasPtrWidth wptr =>
!(GlobalVar Mem) ->
!(Maybe L.Type) ->
!(f (LLVMPointerType wptr)) ->
!(CtxRepr args) ->
!(TypeRepr ret) ->
LLVMStmt f (FunctionHandleType args ret)
LLVM_ResolveGlobal ::
HasPtrWidth wptr =>
!(NatRepr wptr) ->
!(GlobalVar Mem) ->
GlobalSymbol ->
LLVMStmt f (LLVMPointerType wptr)
LLVM_PtrEq ::
HasPtrWidth wptr =>
!(GlobalVar Mem) ->
!(f (LLVMPointerType wptr)) ->
!(f (LLVMPointerType wptr)) ->
LLVMStmt f BoolType
LLVM_PtrLe ::
HasPtrWidth wptr =>
!(GlobalVar Mem) ->
!(f (LLVMPointerType wptr)) ->
!(f (LLVMPointerType wptr)) ->
LLVMStmt f BoolType
LLVM_PtrAddOffset ::
HasPtrWidth wptr =>
!(NatRepr wptr) ->
!(GlobalVar Mem) ->
!(f (LLVMPointerType wptr)) ->
!(f (BVType wptr)) ->
LLVMStmt f (LLVMPointerType wptr)
LLVM_PtrSubtract ::
HasPtrWidth wptr =>
!(NatRepr wptr) ->
!(GlobalVar Mem) ->
!(f (LLVMPointerType wptr)) ->
!(f (LLVMPointerType wptr)) ->
LLVMStmt f (BVType wptr)
LLVM_Debug ::
!(LLVM_Dbg f c) ->
LLVMStmt f UnitType
data LLVM_Dbg f c where
LLVM_Dbg_Addr ::
HasPtrWidth wptr =>
!(f (LLVMPointerType wptr)) ->
L.DILocalVariable ->
L.DIExpression ->
LLVM_Dbg f (LLVMPointerType wptr)
LLVM_Dbg_Declare ::
HasPtrWidth wptr =>
!(f (LLVMPointerType wptr)) ->
L.DILocalVariable ->
L.DIExpression ->
LLVM_Dbg f (LLVMPointerType wptr)
LLVM_Dbg_Value ::
!(TypeRepr c) ->
!(f c) ->
L.DILocalVariable ->
L.DIExpression ->
LLVM_Dbg f c
$(return [])
instance TypeApp LLVMExtensionExpr where
appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType).
LLVMExtensionExpr f x -> TypeRepr x
appType LLVMExtensionExpr f x
e =
case LLVMExtensionExpr f x
e of
X86Expr ExtX86 f x
ex -> ExtX86 f x -> TypeRepr x
forall (f :: CrucibleType -> Type) (x :: CrucibleType).
ExtX86 f x -> TypeRepr x
forall (app :: (CrucibleType -> Type) -> CrucibleType -> Type)
(f :: CrucibleType -> Type) (x :: CrucibleType).
TypeApp app =>
app f x -> TypeRepr x
appType ExtX86 f x
ex
LLVM_SideConditions GlobalVar Mem
_ TypeRepr x
tpr NonEmpty (LLVMSideCondition f)
_ f x
_ -> TypeRepr x
tpr
LLVM_PointerExpr NatRepr w
w f NatType
_ f (BVType w)
_ -> NatRepr w -> TypeRepr x
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr w
w
LLVM_PointerBlock NatRepr w
_ f (LLVMPointerType w)
_ -> TypeRepr x
TypeRepr NatType
NatRepr
LLVM_PointerOffset NatRepr w
w f (LLVMPointerType w)
_ -> NatRepr w -> TypeRepr ('BaseToType (BaseBVType w))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w
LLVM_PointerIte NatRepr w
w f BoolType
_ f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
_ f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
_ -> NatRepr w -> TypeRepr x
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr w
w
instance PrettyApp LLVMExtensionExpr where
ppApp :: forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). LLVMExtensionExpr f x -> Doc ann
ppApp forall (x :: CrucibleType). f x -> Doc ann
pp LLVMExtensionExpr f x
e =
case LLVMExtensionExpr f x
e of
X86Expr ExtX86 f x
ex -> (forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). ExtX86 f x -> Doc ann
forall k (app :: (k -> Type) -> k -> Type) (f :: k -> Type) ann.
PrettyApp app =>
(forall (x :: k). f x -> Doc ann)
-> forall (x :: k). app f x -> Doc ann
forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). ExtX86 f x -> Doc ann
ppApp f x -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp ExtX86 f x
ex
LLVM_SideConditions GlobalVar Mem
_ TypeRepr x
_ NonEmpty (LLVMSideCondition f)
_conds f x
ex ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"sideConditions" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f x -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f x
ex
LLVM_PointerExpr NatRepr w
_ f NatType
blk f (BVType w)
off ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"pointerExpr" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f NatType -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f NatType
blk Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (BVType w) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (BVType w)
off
LLVM_PointerBlock NatRepr w
_ f (LLVMPointerType w)
ptr ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"pointerBlock" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType w) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType w)
ptr
LLVM_PointerOffset NatRepr w
_ f (LLVMPointerType w)
ptr ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"pointerOffset" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType w) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType w)
ptr
LLVM_PointerIte NatRepr w
_ f BoolType
cond f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
x f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
y ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"pointerIte" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f BoolType -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f BoolType
cond Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
-> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
-> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w))
y
instance TestEqualityFC LLVMExtensionExpr where
testEqualityFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y))
-> forall (x :: CrucibleType) (y :: CrucibleType).
LLVMExtensionExpr f x -> LLVMExtensionExpr f y -> Maybe (x :~: y)
testEqualityFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
testSubterm =
$(U.structuralTypeEquality [t|LLVMExtensionExpr|]
[ (U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
, (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
, (U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
, (U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|testEquality|])
, (U.ConType [t|X86.ExtX86|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|testEqualityFC testSubterm|])
, (U.ConType [t|NonEmpty|] `U.TypeApp` (U.ConType [t|LLVMSideCondition|] `U.TypeApp` U.AnyType)
, [| \x y -> if liftEq (testEqualityC testSubterm) x y then Just Refl else Nothing |]
)
])
instance OrdFC LLVMExtensionExpr where
compareFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y)
-> forall (x :: CrucibleType) (y :: CrucibleType).
LLVMExtensionExpr f x -> LLVMExtensionExpr f y -> OrderingF x y
compareFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
testSubterm =
$(U.structuralTypeOrd [t|LLVMExtensionExpr|]
[ (U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
, (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
, (U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
, (U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|compareF|])
, (U.ConType [t|X86.ExtX86|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|compareFC testSubterm|])
, (U.ConType [t|NonEmpty|] `U.TypeApp` (U.ConType [t|LLVMSideCondition|] `U.TypeApp` U.AnyType)
, [| \x y -> fromOrdering (liftCompare (compareC testSubterm) x y) |]
)
])
instance FunctorFC LLVMExtensionExpr where
fmapFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType).
LLVMExtensionExpr f x -> LLVMExtensionExpr g x
fmapFC = (forall (x :: CrucibleType). f x -> g x)
-> LLVMExtensionExpr f x -> LLVMExtensionExpr g x
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType).
LLVMExtensionExpr f x -> LLVMExtensionExpr g x
forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
TraversableFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType).
LLVMExtensionExpr f x -> LLVMExtensionExpr g x
fmapFCDefault
instance FoldableFC LLVMExtensionExpr where
foldMapFC :: forall (f :: CrucibleType -> Type) m.
Monoid m =>
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). LLVMExtensionExpr f x -> m
foldMapFC = (forall (x :: CrucibleType). f x -> m)
-> LLVMExtensionExpr f x -> m
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). LLVMExtensionExpr f x -> m
forall {k} {l} (t :: (k -> Type) -> l -> Type) m (f :: k -> Type).
(TraversableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
foldMapFCDefault
traverseConds ::
Applicative m =>
(forall s. f s -> m (g s)) ->
NonEmpty (LLVMSideCondition f) ->
m (NonEmpty (LLVMSideCondition g))
traverseConds :: forall (m :: Type -> Type) (f :: CrucibleType -> Type)
(g :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). f s -> m (g s))
-> NonEmpty (LLVMSideCondition f)
-> m (NonEmpty (LLVMSideCondition g))
traverseConds forall (s :: CrucibleType). f s -> m (g s)
f = (LLVMSideCondition f -> m (LLVMSideCondition g))
-> NonEmpty (LLVMSideCondition f)
-> m (NonEmpty (LLVMSideCondition g))
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) -> NonEmpty a -> f (NonEmpty b)
traverse ((forall (s :: CrucibleType). f s -> m (g s))
-> LLVMSideCondition f -> m (LLVMSideCondition g)
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 :: CrucibleType -> Type)
(f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> LLVMSideCondition e -> m (LLVMSideCondition f)
traverseF f s -> m (g s)
forall (s :: CrucibleType). f s -> m (g s)
f)
instance TraversableFC LLVMExtensionExpr where
traverseFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType).
LLVMExtensionExpr f x -> m (LLVMExtensionExpr g x)
traverseFC = $(U.structuralTraversal [t|LLVMExtensionExpr|]
[(U.ConType [t|X86.ExtX86|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType, [|traverseFC|])
,(U.ConType [t|NonEmpty|] `U.TypeApp` (U.ConType [t|LLVMSideCondition|] `U.TypeApp` U.AnyType)
, [| traverseConds |]
)
])
instance TypeApp LLVMStmt where
appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType).
LLVMStmt f x -> TypeRepr x
appType = \case
LLVM_PushFrame{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
LLVM_PopFrame{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
LLVM_Alloca NatRepr wptr
w GlobalVar Mem
_ f (BVType wptr)
_ Alignment
_ String
_ -> NatRepr wptr -> TypeRepr x
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr wptr
w
LLVM_Load GlobalVar Mem
_ f (LLVMPointerType wptr)
_ TypeRepr x
tp StorageType
_ Alignment
_ -> TypeRepr x
tp
LLVM_Store{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
LLVM_MemClear{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
LLVM_LoadHandle GlobalVar Mem
_ Maybe Type
_ f (LLVMPointerType wptr)
_ CtxRepr args
args TypeRepr ret
ret -> CtxRepr args
-> TypeRepr ret -> TypeRepr ('FunctionHandleType args ret)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr ctx
-> TypeRepr ret -> TypeRepr ('FunctionHandleType ctx ret)
FunctionHandleRepr CtxRepr args
args TypeRepr ret
ret
LLVM_ResolveGlobal NatRepr wptr
w GlobalVar Mem
_ GlobalSymbol
_ -> NatRepr wptr -> TypeRepr x
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr wptr
w
LLVM_PtrEq{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
LLVM_PtrLe{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
LLVM_PtrAddOffset NatRepr wptr
w GlobalVar Mem
_ f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
_ f (BVType wptr)
_ -> NatRepr wptr -> TypeRepr x
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr wptr
w
LLVM_PtrSubtract NatRepr wptr
w GlobalVar Mem
_ f (LLVMPointerType wptr)
_ f (LLVMPointerType wptr)
_ -> NatRepr wptr -> TypeRepr ('BaseToType (BaseBVType wptr))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr wptr
w
LLVM_Debug{} -> TypeRepr x
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
instance PrettyApp LLVMStmt where
ppApp :: forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). LLVMStmt f x -> Doc ann
ppApp forall (x :: CrucibleType). f x -> Doc ann
pp = \case
LLVM_PushFrame Text
nm GlobalVar Mem
mvar ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"pushFrame" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
nm Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar
LLVM_PopFrame GlobalVar Mem
mvar ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"popFrame" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar
LLVM_Alloca NatRepr wptr
_ GlobalVar Mem
mvar f (BVType wptr)
sz Alignment
a String
loc ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"alloca" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (BVType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (BVType wptr)
sz Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Alignment -> Doc ann
forall ann. Alignment -> Doc ann
ppAlignment Alignment
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
loc
LLVM_Load GlobalVar Mem
mvar f (LLVMPointerType wptr)
ptr TypeRepr x
_tpr StorageType
tp Alignment
a ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"load" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
ptr Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StorageType -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow StorageType
tp Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Alignment -> Doc ann
forall ann. Alignment -> Doc ann
ppAlignment Alignment
a
LLVM_Store GlobalVar Mem
mvar f (LLVMPointerType wptr)
ptr TypeRepr tp
_tpr StorageType
tp Alignment
a f tp
v ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"store" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
ptr Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StorageType -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow StorageType
tp Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Alignment -> Doc ann
forall ann. Alignment -> Doc ann
ppAlignment Alignment
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f tp -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f tp
v
LLVM_MemClear GlobalVar Mem
mvar f (LLVMPointerType wptr)
ptr Bytes
len ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"memClear" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
ptr Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bytes -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Bytes
len
LLVM_LoadHandle GlobalVar Mem
mvar Maybe Type
ltp f (LLVMPointerType wptr)
ptr CtxRepr args
_args TypeRepr ret
_ret ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"loadFunctionHandle" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
ptr Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"as" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Maybe Type -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Maybe Type
ltp
LLVM_ResolveGlobal NatRepr wptr
_ GlobalVar Mem
mvar GlobalSymbol
gs ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"resolveGlobal" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (GlobalSymbol -> String
globalSymbolName GlobalSymbol
gs)
LLVM_PtrEq GlobalVar Mem
mvar f (LLVMPointerType wptr)
x f (LLVMPointerType wptr)
y ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"ptrEq" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
y
LLVM_PtrLe GlobalVar Mem
mvar f (LLVMPointerType wptr)
x f (LLVMPointerType wptr)
y ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"ptrLe" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
y
LLVM_PtrAddOffset NatRepr wptr
_ GlobalVar Mem
mvar f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
x f (BVType wptr)
y ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"ptrAddOffset" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
-> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (BVType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (BVType wptr)
y
LLVM_PtrSubtract NatRepr wptr
_ GlobalVar Mem
mvar f (LLVMPointerType wptr)
x f (LLVMPointerType wptr)
y ->
String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"ptrSubtract" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar Mem -> Doc ann
forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar GlobalVar Mem
mvar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f (LLVMPointerType wptr) -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f (LLVMPointerType wptr)
y
LLVM_Debug LLVM_Dbg f c
dbg -> (forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). LLVM_Dbg f x -> Doc ann
forall k (app :: (k -> Type) -> k -> Type) (f :: k -> Type) ann.
PrettyApp app =>
(forall (x :: k). f x -> Doc ann)
-> forall (x :: k). app f x -> Doc ann
forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). LLVM_Dbg f x -> Doc ann
ppApp f x -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp LLVM_Dbg f c
dbg
instance PrettyApp LLVM_Dbg where
ppApp :: forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). LLVM_Dbg f x -> Doc ann
ppApp forall (x :: CrucibleType). f x -> Doc ann
pp = \case
LLVM_Dbg_Addr f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
x DILocalVariable
_ DIExpression
_ -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"dbg.addr" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
-> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
x
LLVM_Dbg_Declare f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
x DILocalVariable
_ DIExpression
_ -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"dbg.declare" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
-> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f ('IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType wptr))
x
LLVM_Dbg_Value TypeRepr x
_ f x
x DILocalVariable
_ DIExpression
_ -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"dbg.value" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> f x -> Doc ann
forall (x :: CrucibleType). f x -> Doc ann
pp f x
x
ppGlobalVar :: GlobalVar Mem -> Doc ann
ppGlobalVar :: forall ann. GlobalVar Mem -> Doc ann
ppGlobalVar = GlobalVar Mem -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow
ppAlignment :: Alignment -> Doc ann
ppAlignment :: forall ann. Alignment -> Doc ann
ppAlignment = Alignment -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow
instance TestEqualityFC LLVM_Dbg where
testEqualityFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y))
-> forall (x :: CrucibleType) (y :: CrucibleType).
LLVM_Dbg f x -> LLVM_Dbg f y -> Maybe (x :~: y)
testEqualityFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
testSubterm = $(U.structuralTypeEquality [t|LLVM_Dbg|]
[(U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
])
instance OrdFC LLVM_Dbg where
compareFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y)
-> forall (x :: CrucibleType) (y :: CrucibleType).
LLVM_Dbg f x -> LLVM_Dbg f y -> OrderingF x y
compareFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
compareSubterm = $(U.structuralTypeOrd [t|LLVM_Dbg|]
[(U.DataArg 0 `U.TypeApp` U.AnyType, [|compareSubterm|])
,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
])
instance FoldableFC LLVM_Dbg where
foldMapFC :: forall (f :: CrucibleType -> Type) m.
Monoid m =>
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). LLVM_Dbg f x -> m
foldMapFC = (forall (x :: CrucibleType). f x -> m) -> LLVM_Dbg f x -> m
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). LLVM_Dbg f x -> m
forall {k} {l} (t :: (k -> Type) -> l -> Type) m (f :: k -> Type).
(TraversableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
foldMapFCDefault
instance FunctorFC LLVM_Dbg where
fmapFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). LLVM_Dbg f x -> LLVM_Dbg g x
fmapFC = (forall (x :: CrucibleType). f x -> g x)
-> LLVM_Dbg f x -> LLVM_Dbg g x
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). LLVM_Dbg f x -> LLVM_Dbg g x
forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
TraversableFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). LLVM_Dbg f x -> LLVM_Dbg g x
fmapFCDefault
instance TraversableFC LLVM_Dbg where
traverseFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). LLVM_Dbg f x -> m (LLVM_Dbg g x)
traverseFC = $(U.structuralTraversal [t|LLVM_Dbg|] [])
instance TestEqualityFC LLVMStmt where
testEqualityFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y))
-> forall (x :: CrucibleType) (y :: CrucibleType).
LLVMStmt f x -> LLVMStmt f y -> Maybe (x :~: y)
testEqualityFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
testSubterm =
$(U.structuralTypeEquality [t|LLVMStmt|]
[(U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
,(U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
,(U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|testEquality|])
,(U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
,(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|testEqualityFC testSubterm|])
])
instance OrdFC LLVMStmt where
compareFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y)
-> forall (x :: CrucibleType) (y :: CrucibleType).
LLVMStmt f x -> LLVMStmt f y -> OrderingF x y
compareFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
compareSubterm =
$(U.structuralTypeOrd [t|LLVMStmt|]
[(U.DataArg 0 `U.TypeApp` U.AnyType, [|compareSubterm|])
,(U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
,(U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|compareF|])
,(U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType, [|compareF|])
,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
,(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|compareFC compareSubterm|])
])
instance FunctorFC LLVMStmt where
fmapFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). LLVMStmt f x -> LLVMStmt g x
fmapFC = (forall (x :: CrucibleType). f x -> g x)
-> LLVMStmt f x -> LLVMStmt g x
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). LLVMStmt f x -> LLVMStmt g x
forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
TraversableFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). LLVMStmt f x -> LLVMStmt g x
fmapFCDefault
instance FoldableFC LLVMStmt where
foldMapFC :: forall (f :: CrucibleType -> Type) m.
Monoid m =>
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). LLVMStmt f x -> m
foldMapFC = (forall (x :: CrucibleType). f x -> m) -> LLVMStmt f x -> m
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). LLVMStmt f x -> m
forall {k} {l} (t :: (k -> Type) -> l -> Type) m (f :: k -> Type).
(TraversableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
foldMapFCDefault
instance TraversableFC LLVMStmt where
traverseFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
(m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). LLVMStmt f x -> m (LLVMStmt g x)
traverseFC =
$(U.structuralTraversal [t|LLVMStmt|]
[(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|traverseFC|])
])