crucible-llvm-0.6: src/Lang/Crucible/LLVM/Extension/Syntax.hs
-----------------------------------------------------------------------
-- |
-- 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|])
])