content: -----------------------------------------------------------------------
  -- |
  -- 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 sub (LLVMSideCondition px dx) (LLVMSideCondition py dy) =
      isJust (sub px py) && testEqualityC sub dx dy
  
  instance OrdC LLVMSideCondition where
    compareC sub (LLVMSideCondition px dx) (LLVMSideCondition py dy) =
      toOrdering (sub px py) <> compareC sub dx dy
  
  instance FunctorF LLVMSideCondition where
    fmapF = fmapFDefault
  
  instance FoldableF LLVMSideCondition where
    foldMapF = foldMapFDefault
  
  instance TraversableF LLVMSideCondition where
    traverseF f (LLVMSideCondition p desc) =
        LLVMSideCondition <$> f p <*> traverseF f 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 e =
      case e of
        X86Expr ex             -> appType ex
        LLVM_SideConditions _ tpr _ _ -> tpr
        LLVM_PointerExpr w _ _ -> LLVMPointerRepr w
        LLVM_PointerBlock _ _  -> NatRepr
        LLVM_PointerOffset w _ -> BVRepr w
        LLVM_PointerIte w _ _ _ -> LLVMPointerRepr w
  
  instance PrettyApp LLVMExtensionExpr where
    ppApp pp e =
      case e of
        X86Expr ex -> ppApp pp ex
        LLVM_SideConditions _ _ _conds ex ->
          pretty "sideConditions" <+> pp ex -- TODO? Print the conditions?
        LLVM_PointerExpr _ blk off ->
          pretty "pointerExpr" <+> pp blk <+> pp off
        LLVM_PointerBlock _ ptr ->
          pretty "pointerBlock" <+> pp ptr
        LLVM_PointerOffset _ ptr ->
          pretty "pointerOffset" <+> pp ptr
        LLVM_PointerIte _ cond x y ->
          pretty "pointerIte" <+> pp cond <+> pp x <+> pp y
  
  instance TestEqualityFC LLVMExtensionExpr where
    testEqualityFC 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 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 = fmapFCDefault
  
  instance FoldableFC LLVMExtensionExpr where
    foldMapFC = foldMapFCDefault
  
  
  traverseConds ::
    Applicative m =>
    (forall s. f s -> m (g s)) ->
    NonEmpty (LLVMSideCondition f) ->
    m (NonEmpty (LLVMSideCondition g))
  traverseConds f = traverse (traverseF f)
  
  
  instance TraversableFC LLVMExtensionExpr where
    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 = \case
      LLVM_PushFrame{} -> knownRepr
      LLVM_PopFrame{} -> knownRepr
      LLVM_Alloca w _ _ _ _ -> LLVMPointerRepr w
      LLVM_Load _ _ tp _ _  -> tp
      LLVM_Store{} -> knownRepr
      LLVM_MemClear{} -> knownRepr
      LLVM_LoadHandle _ _ _ args ret -> FunctionHandleRepr args ret
      LLVM_ResolveGlobal w _ _ -> LLVMPointerRepr w
      LLVM_PtrEq{} -> knownRepr
      LLVM_PtrLe{} -> knownRepr
      LLVM_PtrAddOffset w _ _ _ -> LLVMPointerRepr w
      LLVM_PtrSubtract w _ _ _ -> BVRepr w
      LLVM_Debug{} -> knownRepr
  
  instance PrettyApp LLVMStmt where
    ppApp pp = \case
      LLVM_PushFrame nm mvar ->
         pretty "pushFrame" <+> pretty nm <+> ppGlobalVar mvar
      LLVM_PopFrame mvar  ->
         pretty "popFrame" <+> ppGlobalVar mvar
      LLVM_Alloca _ mvar sz a loc ->
         pretty "alloca" <+> ppGlobalVar mvar <+> pp sz <+> ppAlignment a <+> pretty loc
      LLVM_Load mvar ptr _tpr tp a ->
         pretty "load" <+> ppGlobalVar mvar <+> pp ptr <+> viaShow tp <+> ppAlignment a
      LLVM_Store mvar ptr _tpr tp a v ->
         pretty "store" <+> ppGlobalVar mvar <+> pp ptr <+> viaShow tp <+> ppAlignment a <+> pp v
      LLVM_MemClear mvar ptr len ->
         pretty "memClear" <+> ppGlobalVar mvar <+> pp ptr <+> viaShow len
      LLVM_LoadHandle mvar ltp ptr _args _ret ->
         pretty "loadFunctionHandle" <+> ppGlobalVar mvar <+> pp ptr <+> pretty "as" <+> viaShow ltp
      LLVM_ResolveGlobal _ mvar gs ->
         pretty "resolveGlobal" <+> ppGlobalVar mvar <+> viaShow (globalSymbolName gs)
      LLVM_PtrEq mvar x y ->
         pretty "ptrEq" <+> ppGlobalVar mvar <+> pp x <+> pp y
      LLVM_PtrLe mvar x y ->
         pretty "ptrLe" <+> ppGlobalVar mvar <+> pp x <+> pp y
      LLVM_PtrAddOffset _ mvar x y ->
         pretty "ptrAddOffset" <+> ppGlobalVar mvar <+> pp x <+> pp y
      LLVM_PtrSubtract _ mvar x y ->
         pretty "ptrSubtract" <+> ppGlobalVar mvar <+> pp x <+> pp y
      LLVM_Debug dbg -> ppApp pp dbg
  
  instance PrettyApp LLVM_Dbg where
    ppApp pp = \case
      LLVM_Dbg_Addr    x _ _ -> pretty "dbg.addr"    <+> pp x
      LLVM_Dbg_Declare x _ _ -> pretty "dbg.declare" <+> pp x
      LLVM_Dbg_Value _ x _ _ -> pretty "dbg.value"   <+> pp x
  
  -- TODO: move to a Pretty instance
  ppGlobalVar :: GlobalVar Mem -> Doc ann
  ppGlobalVar = viaShow
  
  -- TODO: move to a Pretty instance
  ppAlignment :: Alignment -> Doc ann
  ppAlignment = viaShow
  
  instance TestEqualityFC LLVM_Dbg where
    testEqualityFC 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 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 = foldMapFCDefault
  instance FunctorFC LLVM_Dbg where
    fmapFC = fmapFCDefault
  
  instance TraversableFC LLVM_Dbg where
    traverseFC = $(U.structuralTraversal [t|LLVM_Dbg|] [])
  
  instance TestEqualityFC LLVMStmt where
    testEqualityFC 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 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 = fmapFCDefault
  
  instance FoldableFC LLVMStmt where
    foldMapFC = foldMapFCDefault
  
  instance TraversableFC LLVMStmt where
    traverseFC =
      $(U.structuralTraversal [t|LLVMStmt|]
        [(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|traverseFC|])
        ])
  