crucible-llvm: Remove LLVM AST type from load handle operation

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 was only ever used in
diagnostics anyway.

crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs

@@ -36,8 +36,6 @@ module Lang.Crucible.LLVM.Errors.MemoryError
 import           Prelude hiding (pred)
 
 import           Data.Text (Text)
-import qualified Text.LLVM.PP as L
-import qualified Text.LLVM.AST as L
 import           Type.Reflection (SomeTypeRep(SomeTypeRep))
 import           Prettyprinter
 
@@ -58,7 +56,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 String) (LLVMPtr sym w) (Mem sym)
   | forall wlen. (1 <= wlen) => MemInvalidateOp
        Text (Maybe String) (LLVMPtr sym w) (SymBV sym wlen) (Mem sym)
 
@@ -69,7 +67,7 @@ memOpMem =
     MemStoreOp _ _ _ mem -> mem
     MemStoreBytesOp _ _ _ mem -> mem
     MemCopyOp _ _ _ mem -> mem
-    MemLoadHandleOp _ _ _ mem -> mem
+    MemLoadHandleOp _ _ mem -> mem
     MemInvalidateOp _ _ _ _ mem -> mem
 
 data MemoryError sym where
@@ -156,8 +154,8 @@ ppMemoryOp (MemCopyOp (gsym_dest, dest) (gsym_src, src) len mem) =
        , indent 2 (ppMem mem)
        ]
 
-ppMemoryOp (MemLoadHandleOp sig gsym ptr mem) =
-  vsep [ "Attempting to load callable function with type:" <+> viaShow (L.ppType sig)
+ppMemoryOp (MemLoadHandleOp gsym ptr mem) =
+  vsep [ "Attempting to load callable function:"
        , indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
        , "In memory state:"
        , indent 2 (ppMem mem)
@@ -241,8 +239,8 @@ concMemoryOp sym conc (MemStoreBytesOp gsym ptr len mem) =
     concPtr sym conc ptr <*>
     traverse (concBV sym conc) len <*>
     concMem sym conc mem
-concMemoryOp sym conc (MemLoadHandleOp tp gsym ptr mem) =
-  MemLoadHandleOp tp gsym <$> concPtr sym conc ptr <*> concMem sym conc mem
+concMemoryOp sym conc (MemLoadHandleOp gsym ptr mem) =
+  MemLoadHandleOp gsym <$> concPtr sym conc ptr <*> concMem sym conc mem
 concMemoryOp sym conc (MemCopyOp (gsym_dest, dest) (gsym_src, src) len mem) =
   do dest' <- concPtr sym conc dest
      src'  <- concPtr sym conc src

crucible-llvm/src/Lang/Crucible/LLVM/Extension/Syntax.hs

@@ -171,7 +171,6 @@ 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 -} ->
      !(f (LLVMPointerType wptr)) {- Pointer to load from -} ->
      !(CtxRepr args)             {- Expected argument types of the function -} ->
      !(TypeRepr ret)             {- Expected return type of the function -} ->
@@ -351,7 +350,7 @@ instance TypeApp LLVMStmt where
     LLVM_Load _ _ tp _ _  -> tp
     LLVM_Store{} -> knownRepr
     LLVM_MemClear{} -> knownRepr
-    LLVM_LoadHandle _ _ _ args ret -> FunctionHandleRepr args ret
+    LLVM_LoadHandle _ _ args ret -> FunctionHandleRepr args ret
     LLVM_ResolveGlobal w _ _ -> LLVMPointerRepr w
     LLVM_PtrEq{} -> knownRepr
     LLVM_PtrLe{} -> knownRepr
@@ -373,8 +372,8 @@ instance PrettyApp LLVMStmt where
        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_LoadHandle mvar ptr _args _ret ->
+       pretty "loadFunctionHandle" <+> ppGlobalVar mvar <+> pp ptr
     LLVM_ResolveGlobal _ mvar gs ->
        pretty "resolveGlobal" <+> ppGlobalVar mvar <+> viaShow (globalSymbolName gs)
     LLVM_PtrEq mvar x y ->

crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -432,11 +432,11 @@ evalStmt bak = eval
         mem' <- liftIO $ doStore bak mem ptr tpr valType alignment val
         setMem mvar mem'
 
-  eval (LLVM_LoadHandle mvar ltp (regValue -> ptr) args ret) =
+  eval (LLVM_LoadHandle mvar (regValue -> ptr) args ret) =
      do mem <- getMem mvar
         let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr
         mhandle <- liftIO $ doLookupHandle sym mem ptr
-        let mop = MemLoadHandleOp ltp gsym ptr (memImplHeap mem)
+        let mop = MemLoadHandleOp gsym ptr (memImplHeap mem)
         let expectedTp = FunctionHandleRepr args ret
         case mhandle of
            Left lookupErr -> lift $

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs

@@ -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 ptr argTypes retTy)
           ret <- call v args''
           assign_f (BaseExpr retTy ret)
         _ -> fail $ unwords ["unsupported function value", show fn]