Copyright	(c) Galois Inc 2026
License	BSD3
Maintainer	Langston Barrett <langston@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.LLVM.Intrinsics.Cast

Contents

There
Back again
Lowering overrides

Description

In Crucible-LLVM, LLVM pointers and integers are translated to terms of type LLVMPointerType. When writing overrides, it can be convenient to take arguments or return values of BVType. This is done frequently in the built-in overrides in Lang.Crucible.LLVM.Intrinsics.Libc and Lang.Crucible.LLVM.Intrinsics.LLVM. This module contains helpers for "lowering" signatures using Crucible bitvectors to ones that use LLVM pointers.

Synopsis

type family CtxToLLVMType (t :: Ctx CrucibleType) :: Ctx CrucibleType where ...
type family ToLLVMType (t :: CrucibleType) :: CrucibleType where ...
ctxToLLVMType :: forall (ctx :: Ctx CrucibleType). Assignment TypeRepr ctx -> Assignment TypeRepr (CtxToLLVMType ctx)
toLLVMType :: forall (t :: CrucibleType). TypeRepr t -> TypeRepr (ToLLVMType t)
regValuesToLLVM :: forall sym (tys :: Ctx CrucibleType). IsSymInterface sym => sym -> Assignment TypeRepr tys -> Assignment (RegValue' sym) tys -> IO (Assignment (RegValue' sym) (CtxToLLVMType tys))
regValueToLLVM :: forall sym (ty :: CrucibleType). IsSymInterface sym => sym -> TypeRepr ty -> RegValue sym ty -> IO (RegValue sym (ToLLVMType ty))
regValuesFromLLVM :: forall sym bak (tys :: Ctx CrucibleType). IsSymBackend sym bak => bak -> FunctionName -> Assignment TypeRepr tys -> Assignment TypeRepr (CtxToLLVMType tys) -> Assignment (RegValue' sym) (CtxToLLVMType tys) -> IO (Assignment (RegValue' sym) tys)
regValueFromLLVM :: forall sym bak (ty :: CrucibleType). IsSymBackend sym bak => bak -> FunctionName -> TypeRepr ty -> TypeRepr (ToLLVMType ty) -> RegValue sym (ToLLVMType ty) -> IO (RegValue sym ty)
regEntriesFromLLVM :: forall sym bak (tys :: Ctx CrucibleType). IsSymBackend sym bak => bak -> FunctionName -> Assignment TypeRepr tys -> Assignment TypeRepr (CtxToLLVMType tys) -> Assignment (RegEntry sym) (CtxToLLVMType tys) -> IO (Assignment (RegEntry sym) tys)
regMapFromLLVM :: forall sym bak (tys :: Ctx CrucibleType). IsSymBackend sym bak => bak -> FunctionName -> Assignment TypeRepr tys -> Assignment TypeRepr (CtxToLLVMType tys) -> RegMap sym (CtxToLLVMType tys) -> IO (RegMap sym tys)
lowerLLVMOverride :: forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType). HasLLVMAnn sym => LLVMOverride p sym ext args ret -> LLVMOverride p sym ext (CtxToLLVMType args) (ToLLVMType ret)
lowerMakeOverride :: forall sym p ext (arch :: LLVMArch). HasLLVMAnn sym => MakeOverride p sym ext arch -> MakeOverride p sym ext arch
lowerOverrideTemplate :: forall sym p ext (arch :: LLVMArch). HasLLVMAnn sym => OverrideTemplate p sym ext arch -> OverrideTemplate p sym ext arch

There

type family CtxToLLVMType (t :: Ctx CrucibleType) :: Ctx CrucibleType where ... Source #

Convert bitvectors to LLVMPointers.

Equations

CtxToLLVMType (EmptyCtx :: Ctx CrucibleType) = EmptyCtx :: Ctx CrucibleType
CtxToLLVMType (ctx ::> tp) = CtxToLLVMType ctx ::> ToLLVMType tp

type family ToLLVMType (t :: CrucibleType) :: CrucibleType where ... Source #

Convert bitvectors to LLVMPointers.

Equations

ToLLVMType (BVType w) = LLVMPointerType w
ToLLVMType (VectorType tp) = VectorType (ToLLVMType tp)
ToLLVMType (StructType ctx) = StructType (CtxToLLVMType ctx)
ToLLVMType AnyType = AnyType
ToLLVMType UnitType = UnitType
ToLLVMType BoolType = BoolType
ToLLVMType NatType = NatType
ToLLVMType IntegerType = IntegerType
ToLLVMType RealValType = RealValType
ToLLVMType (FloatType flt) = FloatType flt
ToLLVMType (IEEEFloatType ps) = IEEEFloatType ps
ToLLVMType CharType = CharType
ToLLVMType (StringType si) = StringType si
ToLLVMType ComplexRealType = ComplexRealType
ToLLVMType (IntrinsicType nm ctx) = IntrinsicType nm ctx
ToLLVMType (FunctionHandleType ctx ret) = FunctionHandleType ctx ret
ToLLVMType (RecursiveType nm ctx) = RecursiveType nm ctx
ToLLVMType (MaybeType tp) = MaybeType tp
ToLLVMType (ReferenceType t) = ReferenceType t
ToLLVMType (SequenceType tp) = SequenceType tp
ToLLVMType (VariantType ctx) = VariantType ctx
ToLLVMType (WordMapType n tp) = WordMapType n tp
ToLLVMType (StringMapType tp) = StringMapType tp
ToLLVMType (SymbolicArrayType idx t) = SymbolicArrayType idx t
ToLLVMType (SymbolicStructType ctx) = SymbolicStructType ctx

ctxToLLVMType :: forall (ctx :: Ctx CrucibleType). Assignment TypeRepr ctx -> Assignment TypeRepr (CtxToLLVMType ctx) Source #

Value-level analogue of CtxToLLVMType

toLLVMType :: forall (t :: CrucibleType). TypeRepr t -> TypeRepr (ToLLVMType t) Source #

Value-level analogue of ToLLVMType

regValuesToLLVM :: forall sym (tys :: Ctx CrucibleType). IsSymInterface sym => sym -> Assignment TypeRepr tys -> Assignment (RegValue' sym) tys -> IO (Assignment (RegValue' sym) (CtxToLLVMType tys)) Source #

regValueToLLVM over an Assignment

regValueToLLVM :: forall sym (ty :: CrucibleType). IsSymInterface sym => sym -> TypeRepr ty -> RegValue sym ty -> IO (RegValue sym (ToLLVMType ty)) Source #

Convert a RegValue to its corresponding LLVM type (replacing bitvectors with LLVM pointers).

Back again

regValuesFromLLVM Source #

Arguments

:: forall sym bak (tys :: Ctx CrucibleType). IsSymBackend sym bak
=> bak
-> FunctionName	Only used in error messages
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegValue' sym) (CtxToLLVMType tys)
-> IO (Assignment (RegValue' sym) tys)

Map regValueFromLLVM over an Assignment.

regValueFromLLVM Source #

Arguments

:: forall sym bak (ty :: CrucibleType). IsSymBackend sym bak
=> bak
-> FunctionName	Only used in error messages
-> TypeRepr ty
-> TypeRepr (ToLLVMType ty)
-> RegValue sym (ToLLVMType ty)
-> IO (RegValue sym ty)

Convert a RegValue from its corresponding LLVM type (replacing LLVM pointers with bitvectors where needed).

regEntriesFromLLVM Source #

Arguments

:: forall sym bak (tys :: Ctx CrucibleType). IsSymBackend sym bak
=> bak
-> FunctionName	Only used in error messages
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> Assignment (RegEntry sym) (CtxToLLVMType tys)
-> IO (Assignment (RegEntry sym) tys)

Map regValueFromLLVM over an Assignment of RegEntrys.

regMapFromLLVM Source #

Arguments

:: forall sym bak (tys :: Ctx CrucibleType). IsSymBackend sym bak
=> bak
-> FunctionName	Only used in error messages
-> Assignment TypeRepr tys
-> Assignment TypeRepr (CtxToLLVMType tys)
-> RegMap sym (CtxToLLVMType tys)
-> IO (RegMap sym tys)

Map regValueFromLLVM over a RegMap.

Lowering overrides

lowerLLVMOverride :: forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType). HasLLVMAnn sym => LLVMOverride p sym ext args ret -> LLVMOverride p sym ext (CtxToLLVMType args) (ToLLVMType ret) Source #

Lower an override to use the Crucible-LLVM ABI.

lowerMakeOverride :: forall sym p ext (arch :: LLVMArch). HasLLVMAnn sym => MakeOverride p sym ext arch -> MakeOverride p sym ext arch Source #

Postcompose lowerLLVMOverride with a MakeOverride

lowerOverrideTemplate :: forall sym p ext (arch :: LLVMArch). HasLLVMAnn sym => OverrideTemplate p sym ext arch -> OverrideTemplate p sym ext arch Source #

Call lowerLLVMOverride on the override in a OverrideTemplate