Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

crucible-llvm-cli: Support for overrides; loading and calling functions #1125

Merged
Prev Previous commit
Next Next commit
crucible-llvm: Make LLVM AST type in load handle operation optional
This is in advance of adding syntax for this operation to crucible-llvm-syntax,
which shouldn't need to use llvm-pretty's AST. This type is only ever used in
diagnostics anyway.
  • Loading branch information
langston-barrett committed Nov 14, 2023
commit 12bdab70f7687df23e17395dcfdb87f6885a610f
8 changes: 6 additions & 2 deletions crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ data MemoryOp sym w
(Maybe String, LLVMPtr sym w) -- src
(SymBV sym wlen) -- length
(Mem sym)
| MemLoadHandleOp L.Type (Maybe String) (LLVMPtr sym w) (Mem sym)
| MemLoadHandleOp (Maybe L.Type) (Maybe String) (LLVMPtr sym w) (Mem sym)
| forall wlen. (1 <= wlen) => MemInvalidateOp
Text (Maybe String) (LLVMPtr sym w) (SymBV sym wlen) (Mem sym)

Expand Down Expand Up @@ -157,7 +157,11 @@ ppMemoryOp (MemCopyOp (gsym_dest, dest) (gsym_src, src) len mem) =
]

ppMemoryOp (MemLoadHandleOp sig gsym ptr mem) =
vsep [ "Attempting to load callable function with type:" <+> viaShow (L.ppType sig)
vsep [ case sig of
Just s ->
hsep ["Attempting to load callable function with type:", viaShow (L.ppType s)]
Nothing ->
hsep ["Attempting to load callable function:"]
, indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
, "In memory state:"
, indent 2 (ppMem mem)
Expand Down
2 changes: 1 addition & 1 deletion crucible-llvm/src/Lang/Crucible/LLVM/Extension/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,7 @@ data LLVMStmt (f :: CrucibleType -> Type) :: CrucibleType -> Type where
LLVM_LoadHandle ::
HasPtrWidth wptr =>
!(GlobalVar Mem) {- Memory global variable -} ->
!L.Type {- expected LLVM type of the function -} ->
!(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 -} ->
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1877,7 +1877,7 @@ callOrdinaryFunction instr _tailCall fnTy@(L.FunTy lretTy _largTys _varargs) fn
case asScalar fn' of
Scalar _ PtrRepr ptr -> do
memVar <- getMemVar
v <- extensionStmt (LLVM_LoadHandle memVar fnTy ptr argTypes retTy)
v <- extensionStmt (LLVM_LoadHandle memVar (Just fnTy) ptr argTypes retTy)
ret <- call v args''
assign_f (BaseExpr retTy ret)
_ -> fail $ unwords ["unsupported function value", show fn]
Expand Down