llvm: Remove LLVM declares from LLVM overrides

crucible-llvm-cli/test-data/memset.cbl

@@ -1,9 +1,9 @@
-(declare @memset ((dst (Ptr 64)) (val (Bitvector 32)) (count (Ptr 64))) (Ptr 64))
+(declare @memset ((dst (Ptr 64)) (val (Bitvector 32)) (count (Bitvector 64))) (Ptr 64))
 
 (defun @main () Unit
   (start start:
     (let p (alloca none (bv 64 8)))
     (let c (bv 32 0))
-    (let sz (ptr 64 0 (bv 64 4)))
+    (let sz (bv 64 4))
     (let _ (funcall @memset p c sz))
     (return ())))

crucible-llvm-cli/test-data/ptr.cbl

@@ -25,8 +25,8 @@
     (let g (resolve-global "malloc"))
     (let gblk (ptr-block 64 g))
     (assert! (not (equal? gblk 0)) "malloc block number nonzero")
-    (let h (load-handle (Ptr 64) ((Ptr 64)) g))
-    (let m (funcall h p0))
+    (let h (load-handle (Ptr 64) ((Bitvector 64)) g))
+    (let m (funcall h off0))
     (let mblk (ptr-block 64 m))
     (assert! (not (equal? mblk 0)) "malloc'd block number nonzero")
 

crucible-llvm-cli/test-data/ub/025.out.good

@@ -9,6 +9,6 @@ Prove:
   Details:
     Expected function handle of type FunctionHandleRepr [] UnitRepr
     for call to function malloc
-    but found calling handle of type FunctionHandleRepr [IntrinsicRepr LLVM_pointer [BVRepr 64]] (IntrinsicRepr LLVM_pointer [BVRepr 64])
+    but found calling handle of type FunctionHandleRepr [BVRepr 64] (IntrinsicRepr LLVM_pointer [BVRepr 64])
   false
 COUNTEREXAMPLE

crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/Overrides.hs

@@ -77,18 +77,29 @@ registerLLVMOverrides bak llvmCtx fwdDecs = do
 
   -- Forward all of the `declare`d handles to the actual override
   F.forM_ ovs $ \(CLLVM.SomeLLVMOverride llOv) -> do
-    let L.Symbol nm = L.decName (CLLVM.llvmOverride_declare llOv)
+    let symb@(L.Symbol nm) = CLLVM.llvmOverride_name llOv
     let fnm = WFN.functionNameFromText (Text.pack nm)
     case Map.lookup fnm fwdDecs of
       Nothing -> pure ()
       Just (C.SomeHandle hdl) -> do
-        let llArgs = CLLVM.llvmOverride_args llOv
-        let llRet = CLLVM.llvmOverride_ret llOv
         let hdlArgs = C.handleArgTypes hdl
         let hdlRet = C.handleReturnType hdl
-        o <- CLLVM.build_llvm_override fnm llArgs llRet hdlArgs hdlRet
-               (\asgn -> CLLVM.llvmOverride_def llOv mvar asgn)
-        C.registerFnBinding (C.FnBinding hdl (C.UseOverride o))
+        let llArgs = CLLVM.llvmOverride_args llOv
+        let llRet = CLLVM.llvmOverride_ret llOv
+        case (C.testEquality llArgs hdlArgs, C.testEquality llRet hdlRet) of
+          (Just C.Refl, Just C.Refl) -> do
+            let typedOv = CLLVM.llvmOverrideToTypedOverride mvar llOv
+            let ov = C.runTypedOverride fnm typedOv
+            CLLVM.bindLLVMHandle mvar symb hdl (C.UseOverride ov)
+          _ -> do
+            fail $ unlines $
+              [ "Bad signature in `declare`"
+              , " *** `declare` args: " ++ show hdlArgs
+              , " *** override args:  " ++ show llArgs
+              , " *** `declare` ret:  " ++ show hdlRet
+              , " *** override ret:   " ++ show llRet
+              , ""
+              ]
 
   pure ovs