llvm-{syntax,cli}: Register more overrides for libc and LLVM functions (

#1236)

This will allow us to more easily test the behavior of these
overrides, without involving the translation code.

crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs

@@ -30,12 +30,12 @@ import Lang.Crucible.LLVM.DataLayout (EndianForm(LittleEndian), defaultDataLayou
 import Lang.Crucible.LLVM.Extension (LLVM, ArchRepr(X86Repr))
 import Lang.Crucible.LLVM.MemModel (HasPtrWidth)
 import qualified Lang.Crucible.LLVM.MemModel as Mem
-import Lang.Crucible.LLVM.Intrinsics (alloc_and_register_override)
-import Lang.Crucible.LLVM.Intrinsics.Libc (llvmMallocOverride)
+import Lang.Crucible.LLVM.Intrinsics (defaultIntrinsicsOptions)
 import Lang.Crucible.LLVM.Translation (LLVMContext(..))
 import Lang.Crucible.LLVM.TypeContext (mkTypeContext)
 
 import Lang.Crucible.LLVM.Syntax (llvmParserHooks)
+import Lang.Crucible.LLVM.Syntax.Overrides (registerLLVMOverrides)
 import Lang.Crucible.LLVM.Syntax.TypeAlias (typeAliasParserHooks, x86_64LinuxTypes)
 
 -- | Small helper for providing LLVM language-specific hooks, e.g., for use with
@@ -74,7 +74,9 @@ withLlvmHooks k = do
                     }
               let ?lc = tyCtx
               let ?memOpts = Mem.defaultMemOptions
-              alloc_and_register_override bak llvmCtx llvmMallocOverride []
+              let ?intrinsicsOpts = defaultIntrinsicsOptions
+              _ <- registerLLVMOverrides bak llvmCtx
+              return ()
           , setupOverridesHook = setupOverrides
           }
   let ext _ = let ?recordLLVMAnnotation = \_ _ _ -> pure ()

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

@@ -0,0 +1,11 @@
+(defun @main () Unit
+  (start start:
+    (let g (resolve-global "memset"))
+    (let h (load-handle (Ptr 64) ((Ptr 64) (Ptr 32) (Ptr 64)) g))
+
+    (let p (alloca none (bv 64 8)))
+    (let c (ptr 32 0 (bv 32 0)))
+    (let sz (ptr 64 0 (bv 64 4)))
+    (let _ (funcall h p c sz))
+
+    (return ())))

crucible-llvm-cli/test-data/memset.out.good

@@ -0,0 +1,4 @@
+==== Begin Simulation ====
+
+==== Finish Simulation ====
+==== No proof obligations ====

crucible-llvm-syntax/crucible-llvm-syntax.cabal

@@ -108,6 +108,7 @@ library
 
   exposed-modules:
     Lang.Crucible.LLVM.Syntax
+    Lang.Crucible.LLVM.Syntax.Overrides
     Lang.Crucible.LLVM.Syntax.TypeAlias
 
 test-suite crucible-llvm-syntax-tests

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

@@ -0,0 +1,52 @@
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE ImplicitParams #-}
+
+module Lang.Crucible.LLVM.Syntax.Overrides
+  ( registerLLVMOverrides
+  ) where
+
+import Control.Monad.IO.Class (liftIO)
+import Data.Foldable qualified as F
+import Data.List qualified as List
+
+import Text.LLVM.AST qualified as L
+
+import Lang.Crucible.Backend qualified as C
+import Lang.Crucible.Simulator qualified as C
+
+import Lang.Crucible.LLVM.Functions qualified as CLLVM
+import Lang.Crucible.LLVM.Intrinsics.Libc qualified as Libc
+import Lang.Crucible.LLVM.Intrinsics.LLVM qualified as LLVM
+import Lang.Crucible.LLVM.Intrinsics qualified as CLLVM
+import Lang.Crucible.LLVM.MemModel qualified as CLLVM
+import Lang.Crucible.LLVM.Translation qualified as CLLVM
+import Lang.Crucible.LLVM.TypeContext qualified as CLLVM
+
+-- | Register overrides for libc functions and LLVM intrinsics
+registerLLVMOverrides ::
+  ( C.IsSymBackend sym bak
+  , CLLVM.HasLLVMAnn sym
+  , CLLVM.HasPtrWidth wptr
+  , ?lc :: CLLVM.TypeContext
+  , ?intrinsicsOpts :: CLLVM.IntrinsicsOptions
+  , ?memOpts :: CLLVM.MemOptions
+  ) =>
+  bak ->
+  CLLVM.LLVMContext arch ->
+  C.OverrideSim p sym ext rtp a r [CLLVM.SomeLLVMOverride p sym ext]
+registerLLVMOverrides bak llvmCtx = do
+  let ovs =  List.concat [Libc.libc_overrides, LLVM.basic_llvm_overrides]
+  let decls =
+        List.map (\(CLLVM.SomeLLVMOverride ov) -> CLLVM.llvmOverride_declare ov) (F.toList ovs)
+
+  let mvar = CLLVM.llvmMemVar llvmCtx
+  F.forM_ decls $ \decl -> do
+    let L.Symbol name = L.decName decl
+    let aliases = []
+    -- See the module comment on "Lang.Crucible.LLVM.Functions" for why this
+    -- part is necessary.
+    C.modifyGlobal mvar $ \mem ->
+      liftIO (CLLVM.registerFunPtr bak mem name (L.decName decl) aliases)
+
+  let tmpls = map (\(CLLVM.SomeLLVMOverride ov) -> CLLVM.basic_llvm_override ov) ovs
+  CLLVM.register_llvm_overrides_ llvmCtx tmpls decls