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

Lang.Crucible.LLVM.Intrinsics.Cast

Description

The built-in overrides in Lang.Crucible.LLVM.Intrinsics.Libc and Lang.Crucible.LLVM.Intrinsics.LLVM frequently take arguments of type BVType, but at runtime everything is represented as an LLVMPtr. This module contains helpers for "casting" between pointers and bitvectors.

Synopsis

data ValCastError
printValCastError :: ValCastError -> [String]
data ArgCast p sym ext (args :: Ctx CrucibleType) (args' :: Ctx CrucibleType)
data ValCast p sym ext (tp :: CrucibleType) (tp' :: CrucibleType)
castLLVMArgs :: forall p sym ext bak (args :: Ctx CrucibleType) (args' :: Ctx CrucibleType). IsSymBackend sym bak => FunctionName -> bak -> CtxRepr args' -> CtxRepr args -> Either ValCastError (ArgCast p sym ext args args')
castLLVMRet :: forall sym bak (ret :: CrucibleType) (ret' :: CrucibleType) p ext. IsSymBackend sym bak => FunctionName -> bak -> TypeRepr ret -> TypeRepr ret' -> Either ValCastError (ValCast p sym ext ret ret')

Documentation

Turn a ValCastError into a human-readable message (lines).

A function to (infallibly) cast between Assignments of RegEntrys.

A function to (infallibly) cast a value of types tp to tp'.

Arguments

:: forall p sym ext bak (args :: Ctx CrucibleType) (args' :: Ctx CrucibleType). IsSymBackend sym bak
=> FunctionName	Only used in error messages
-> bak
-> CtxRepr args'
-> CtxRepr args
-> Either ValCastError (ArgCast p sym ext args args')

Attempt to construct a function to cast between Assignments of RegEntrys.

Arguments

:: forall sym bak (ret :: CrucibleType) (ret' :: CrucibleType) p ext. IsSymBackend sym bak
=> FunctionName	Only used in error messages
-> bak
-> TypeRepr ret
-> TypeRepr ret'
-> Either ValCastError (ValCast p sym ext ret ret')

Attempt to construct a function to cast values of type ret to type ret'.