-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Extension.Syntax
-- Description      : LLVM interface for Crucible
-- Copyright        : (c) Galois, Inc 2015-2016
-- License          : BSD3
-- Maintainer       : rdockins@galois.com
-- Stability        : provisional
--
-- Syntax extension definitions for LLVM
------------------------------------------------------------------------

{-# 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) {- Memory global variable -} ->
    !(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)


-- | Extension statements for LLVM.  These statements represent the operations
--   necessary to interact with the LLVM memory model.
data LLVMStmt (f :: CrucibleType -> Type) :: CrucibleType -> Type where

  -- | Indicate the beginning of a new stack frame upon entry to a function.
  LLVM_PushFrame ::
     !Text ->
     !(GlobalVar Mem) {- Memory global variable -} ->
     LLVMStmt f UnitType

  -- | Indicate the end of the current stack frame upon exit from a function.
  LLVM_PopFrame ::
     !(GlobalVar Mem) {- Memory global variable -} ->
     LLVMStmt f UnitType

  -- | Allocate a new memory object in the current stack frame.  This memory
  --   will be automatically deallocated when the corresponding PopFrame
  --   statement is executed.
  LLVM_Alloca ::
     HasPtrWidth wptr =>
     !(NatRepr wptr)       {- Pointer width -} ->
     !(GlobalVar Mem)      {- Memory global variable -} ->
     !(f (BVType wptr))    {- Number of bytes to allocate -} ->
     !Alignment            {- Minimum alignment of this allocation -} ->
     !String               {- Location string to identify this allocation for debugging purposes -} ->
     LLVMStmt f (LLVMPointerType wptr)

  -- | Load a value from the memory.  The load is defined only if
  --   the given pointer is a live pointer; if the bytes in the memory
  --   at that location can be read and reconstructed into a value of the
  --   desired type; and if the given pointer is actually aligned according
  --   to the given alignment value.
  LLVM_Load ::
     HasPtrWidth wptr =>
     !(GlobalVar Mem)            {- Memory global variable -} ->
     !(f (LLVMPointerType wptr)) {- Pointer to load from -} ->
     !(TypeRepr tp)              {- Expected crucible type of the result -} ->
     !StorageType                {- Storage type -} ->
     !Alignment                  {- Assumed alignment of the pointer -} ->
     LLVMStmt f tp

  -- | Store a value in to the memory.  The store is defined only if the given
  --   pointer is a live pointer; if the given value fits into the memory object
  --   at the location pointed to; and the given pointer is aligned according
  --   to the given alignment value.
  LLVM_Store ::
     HasPtrWidth wptr =>
     !(GlobalVar Mem)            {- Memory global variable -} ->
     !(f (LLVMPointerType wptr)) {- Pointer to store at -} ->
     !(TypeRepr tp)              {- Crucible type of the value being stored -} ->
     !StorageType                {- Storage type of the value -} ->
     !Alignment                  {- Assumed alignment of the pointer -} ->
     !(f tp)                     {- Value to store -} ->
     LLVMStmt f UnitType

  -- | Clear a region of memory by setting all the bytes in it to the zero byte.
  --   This is primarily used for initializing the value of global variables,
  --   but can also result from zero initializers.
  LLVM_MemClear ::
     HasPtrWidth wptr =>
     !(GlobalVar Mem)            {- Memory global variable -} ->
     !(f (LLVMPointerType wptr)) {- Pointer to store at -} ->
     !Bytes                      {- Number of bytes to clear -} ->
     LLVMStmt f UnitType

  -- | Load the Crucible function handle that corresponds to a function pointer value.
  --   This load is defined only if the given pointer was previously allocated as
  --   a function pointer value and associated with a Crucible function handle of
  --   the expected type.
  LLVM_LoadHandle ::
     HasPtrWidth wptr =>
     !(GlobalVar Mem)            {- Memory global variable -} ->
     !(Maybe L.Type)             {- expected LLVM type of the function (used only for pretty-printing) -} ->
     !(f (LLVMPointerType wptr)) {- Pointer to load from -} ->
     !(CtxRepr args)             {- Expected argument types of the function -} ->
     !(TypeRepr ret)             {- Expected return type of the function -} ->
     LLVMStmt f (FunctionHandleType args ret)

  -- | Resolve the given global symbol name to a pointer value.
  LLVM_ResolveGlobal ::
     HasPtrWidth wptr =>
     !(NatRepr wptr)      {- Pointer width -} ->
     !(GlobalVar Mem)     {- Memory global variable -} ->
     GlobalSymbol         {- The symbol to resolve -} ->
     LLVMStmt f (LLVMPointerType wptr)

  -- | Test two pointer values for equality.
  --   Note! This operation is defined only
  --   in case both pointers are live or null.
  LLVM_PtrEq ::
     HasPtrWidth wptr =>
     !(GlobalVar Mem)            {- Pointer width -} ->
     !(f (LLVMPointerType wptr)) {- First pointer to compare -} ->
     !(f (LLVMPointerType wptr)) {- First pointer to compare -} ->
     LLVMStmt f BoolType

  -- | Test two pointer values for ordering.
  --   Note! This operation is only defined if
  --   both pointers are live pointers into the
  --   same memory object.
  LLVM_PtrLe ::
     HasPtrWidth wptr =>
     !(GlobalVar Mem)            {- Pointer width -} ->
     !(f (LLVMPointerType wptr)) {- First pointer to compare -} ->
     !(f (LLVMPointerType wptr)) {- First pointer to compare -} ->
     LLVMStmt f BoolType

  -- | Add an offset value to a pointer.
  --   Note! This operation is only defined if both
  --   the input pointer is a live pointer, and
  --   the resulting computed pointer remains in the bounds
  --   of its associated memory object (or one past the end).
  LLVM_PtrAddOffset ::
     HasPtrWidth wptr =>
     !(NatRepr wptr)             {- Pointer width -} ->
     !(GlobalVar Mem)            {- Memory global variable -} ->
     !(f (LLVMPointerType wptr)) {- Pointer value -} ->
     !(f (BVType wptr))          {- Offset value -} ->
     LLVMStmt f (LLVMPointerType wptr)

  -- | Compute the offset between two pointer values.
  --   Note! This operation is only defined if both pointers
  --   are live pointers into the same memory object.
  LLVM_PtrSubtract ::
     HasPtrWidth wptr =>
     !(NatRepr wptr)             {- Pointer width -} ->
     !(GlobalVar Mem)            {- Memory global value -} ->
     !(f (LLVMPointerType wptr)) {- First pointer -} ->
     !(f (LLVMPointerType wptr)) {- Second pointer -} ->
     LLVMStmt f (BVType wptr)

  -- | Debug information
  LLVM_Debug ::
    !(LLVM_Dbg f c)              {- Debug variant -} ->
    LLVMStmt f UnitType

-- | Debug statement variants - these have no semantic meaning
data LLVM_Dbg f c where
  -- | Annotates a value pointed to by a pointer with local-variable debug information
  --
  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-addr>
  LLVM_Dbg_Addr ::
    HasPtrWidth wptr =>
    !(f (LLVMPointerType wptr))  {- Pointer to local variable -} ->
    L.DILocalVariable            {- Local variable information -} ->
    L.DIExpression               {- Complex expression -} ->
    LLVM_Dbg f (LLVMPointerType wptr)

  -- | Annotates a value pointed to by a pointer with local-variable debug information
  --
  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-declare>
  LLVM_Dbg_Declare ::
    HasPtrWidth wptr =>
    !(f (LLVMPointerType wptr))  {- Pointer to local variable -} ->
    L.DILocalVariable            {- Local variable information -} ->
    L.DIExpression               {- Complex expression -} ->
    LLVM_Dbg f (LLVMPointerType wptr)

  -- | Annotates a value with local-variable debug information
  --
  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-value>
  LLVM_Dbg_Value ::
    !(TypeRepr c)                {- Type of local variable -} ->
    !(f c)                       {- Value of local variable -} ->
    L.DILocalVariable            {- Local variable information -} ->
    L.DIExpression               {- Complex expression -} ->
    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 -- TODO? Print the conditions?
      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

-- TODO: move to a Pretty instance
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

-- TODO: move to a Pretty instance
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|])
      ])