llvm: Remove LLVM `declare`s from LLVM overrides #1705

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

Open

langston-barrett wants to merge 15 commits into master from rm-llvm-decl

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

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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

-Original file line number
+Diff line change
@@ Expand Up / @@ -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

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -1,7 +1,6 @@
  
    {-# LANGUAGE GADTs #-}

    {-# LANGUAGE ImportQualifiedPost #-}

    {-# LANGUAGE ImplicitParams #-}

    {-# LANGUAGE LambdaCase #-}

    {-# LANGUAGE RankNTypes #-}

    {-# LANGUAGE TypeOperators #-}

    @@ -11,15 +10,11 @@ module Lang.Crucible.LLVM.Syntax.Overrides
  
    import Control.Monad.IO.Class (liftIO)

    import Data.Foldable qualified as F

    import Data.List qualified as List

    import Data.Map (Map)

    import Data.Map qualified as Map

    import Data.Text qualified as Text

    import Data.Parameterized.Context qualified as Ctx

    import Data.Parameterized.NatRepr qualified as NatRepr

    import Data.Parameterized.Some qualified as Some

    import Data.Parameterized.TraversableFC qualified as TFC

    import Text.LLVM.AST qualified as L

    import Lang.Crucible.Backend qualified as C

    @@ -30,6 +25,7 @@ import Lang.Crucible.Types qualified as C
  
    import Lang.Crucible.LLVM.Extension qualified as CLLVM

    import Lang.Crucible.LLVM.Functions qualified as CLLVM

    import Lang.Crucible.LLVM.Intrinsics qualified as CLLVM

    import Lang.Crucible.LLVM.Intrinsics.Declare 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

    @@ -53,124 +49,44 @@ registerLLVMOverrides ::
  
      Map FunctionName C.SomeHandle ->

      C.OverrideSim p sym ext rtp a r [CLLVM.SomeLLVMOverride p sym ext]

    registerLLVMOverrides bak llvmCtx fwdDecs = do

      let mkHdlDecl (C.SomeHandle hdl) =

            mkDeclare

              (Text.unpack (WFN.functionName (C.handleName hdl)))

              (C.handleArgTypes hdl)

              (C.handleReturnType hdl)

      let mvar = CLLVM.llvmMemVar llvmCtx

      let mDecls = traverse mkHdlDecl (Map.elems fwdDecs)

      decls <-

        case mDecls of

          Left err -> fail (show err)

          Right ok -> pure ok

      let decls = List.map CLLVM.fromSomeHandle (Map.elems fwdDecs)

      F.forM_ decls $ \decl -> do

        let L.Symbol name = L.decName decl

      F.forM_ decls $ \(CLLVM.SomeDeclare decl) -> do

        let symb@(L.Symbol name) = CLLVM.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)

          liftIO (CLLVM.registerFunPtr bak mem name symb aliases)

      ovs <- CLLVM.register_llvm_overrides_ llvmCtx CLLVM.declare_overrides decls

      -- 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.llvmOvSymbol 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.llvmOvArgs llOv

            let llRet = CLLVM.llvmOvRet 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)

              _ ->

                fail $ unlines $

                  [ "Bad signature in `declare`"

                  , " *** name: " ++ nm

                  , " *** `declare` args: " ++ show hdlArgs

                  , " *** override args:  " ++ show llArgs

                  , " *** `declare` ret:  " ++ show hdlRet

                  , " *** override ret:   " ++ show llRet

                  , ""

                  ]

      pure ovs

    -- | Lift a Crucible type to an LLVM type.

    --

    -- This function has several missing cases that can be filled in as necessary.

    llvmType :: CLLVM.HasPtrWidth w => C.TypeRepr t -> Maybe L.Type

    llvmType =

      \case

        C.AnyRepr{} -> Nothing

        C.BoolRepr -> Just (L.PrimType (L.Integer 1))

        C.CharRepr{} -> Nothing

        C.BVRepr w -> Just (intType w)

        C.ComplexRealRepr{} -> Nothing

        C.FloatRepr C.HalfFloatRepr -> Just (L.PrimType (L.FloatType L.Half))

        C.FloatRepr C.SingleFloatRepr -> Just (L.PrimType (L.FloatType L.Float))

        C.FloatRepr C.DoubleFloatRepr -> Just (L.PrimType (L.FloatType L.Double))

        C.FloatRepr C.X86_80FloatRepr -> Just (L.PrimType (L.FloatType L.X86_fp80))

        C.FloatRepr C.DoubleDoubleFloatRepr -> Nothing

        C.FloatRepr C.QuadFloatRepr -> Nothing

        C.FunctionHandleRepr{} -> Nothing

        C.IEEEFloatRepr{} -> Nothing -- TODO?

        C.IntegerRepr{} -> Nothing

        C.MaybeRepr{} -> Nothing

        C.NatRepr{} -> Nothing

        C.RealValRepr{} -> Nothing

        C.RecursiveRepr{} -> Nothing

        C.ReferenceRepr{} -> Nothing

        C.SequenceRepr{} -> Nothing

        C.StringRepr{} -> Nothing

        C.StringMapRepr{} -> Nothing

        C.StructRepr fieldAssn -> do

          fieldTys <-

            traverse (Some.viewSome llvmType) $

              TFC.toListFC Some.Some fieldAssn

          Just $ L.Struct fieldTys

        C.SymbolicArrayRepr{} -> Nothing

        C.SymbolicStructRepr{} -> Nothing

        C.UnitRepr -> Just (L.PrimType L.Void)

        C.VariantRepr{} -> Nothing

        -- HACK: It's not clear how to support other vector sizes, because Crucible

        -- vectors don't have the length as part of the type. We arbitrarily choose

        -- 4 here so that we can write tests for vectorized intrinsics of width 4

        -- in crucible-llvm-cli.

        C.VectorRepr t -> L.Vector 4 <$> llvmType t

        C.WordMapRepr{} -> Nothing

        CLLVM.LLVMPointerRepr w ->

          case C.testEquality w ?ptrWidth of

            Just C.Refl -> Just L.PtrOpaque

            Nothing -> Just (intType w)

        C.IntrinsicRepr{} -> Nothing

     where

      intType :: NatRepr.NatRepr n -> L.Type

      intType w = L.PrimType (L.Integer (fromIntegral (NatRepr.natValue w)))

    -- | Create an LLVM declaration from Crucible types.

    --

    -- See https://github.com/GaloisInc/crucible/issues/1138 for progress on

    -- obviating this code.

    mkDeclare ::

      CLLVM.HasPtrWidth w =>

      String ->

      Ctx.Assignment C.TypeRepr args ->

      C.TypeRepr ret ->

      Either String L.Declare

    mkDeclare name args ret = do

      let getType :: forall t. C.TypeRepr t -> Either String L.Type

          getType t =

            case llvmType t of

              Nothing -> Left ("Can't make LLVM type from Crucible type " ++ show t)

              Just llTy -> Right llTy

      llvmArgs <- sequence (TFC.toListFC getType args)

      llvmRet <- getType ret

      pure $

        L.Declare

          { L.decArgs = llvmArgs

          , L.decAttrs = []

          , L.decComdat = Nothing

          , L.decLinkage = Nothing

          , L.decName = L.Symbol name

          , L.decRetType = llvmRet

          , L.decVarArgs = False

          , L.decVisibility = Nothing

          }

crucible-llvm/CHANGELOG.md

-Original file line number
+Diff line change
@@ Expand Up / @@ -34,6 +34,23 @@ @@
     * Remove the `Eq LLVMConst` instance. This instance was inherently unreliable
       because it cannot easily compute a simple `True`-or-`False` answer in the
       presence of `undef` or `poison` values.
+    * Remove `llvmOverride_declare :: Text.LLVM.AST.Declare` from `LLVMOverride`.
+      * Add `Lang.Crucible.LLVM.Intrinsics.Declare` module.
+      * Change functions in `Lang.Crucible.LLVM.Intrinsics` to work
+        with `Lang.Crucible.LLVM.Intrinsics.Declare.Declare`s. To
+        migrate, use `Lang.Crucible.LLVM.Intrinsics.Declare.fromLLVM`
+        to translate `Text.LLVM.AST.Declare`s into
+        `Lang.Crucible.LLVM.Intrinsics.Declare.Declare`s
+      * `do_register_llvm_override` no longer does any mapping nor adaptation of
+        types, use `Lang.Crucible.LLVM.Intrinsics.Cast.lowerLLVMOverride` for that.
+      * Replace `build_llvm_override` with
+        `Lang.Crucible.LLVM.Intrinsics.Cast.lowerLLVMOverride`.
+      * Overhaul the API of `Lang.Crucible.LLVM.Intrinsics.Cast`.
+      * Replace various fields of `LLVMOverride` with a `Declare`. To migrate:
+        * Replace `llvmOverride_name` with `llvmOvSymbol`
+        * Replace `llvmOverride_args` with `llvmOvArgs`
+        * Replace `llvmOverride_ret` with `llvmOvRet`
     # 0.8.0 -- 2025-11-09
@@ Expand Down @@

crucible-llvm/crucible-llvm.cabal

-Original file line number
+Diff line change
@@ Expand Up / @@ -166,6 +166,7 @@ library @@
         Lang.Crucible.LLVM.Internal
         Lang.Crucible.LLVM.Intrinsics
         Lang.Crucible.LLVM.Intrinsics.Cast
+        Lang.Crucible.LLVM.Intrinsics.Declare
         Lang.Crucible.LLVM.Intrinsics.Libc
         Lang.Crucible.LLVM.Intrinsics.LLVM
         Lang.Crucible.LLVM.MalformedLLVMModule
@@ Expand Down @@

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

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -53,6 +53,8 @@ import           Lang.Crucible.LLVM.Translation.Types
  
    import           Lang.Crucible.LLVM.TypeContext (TypeContext)

    import           Lang.Crucible.LLVM.Intrinsics.Common

    import qualified Lang.Crucible.LLVM.Intrinsics.Cast as Cast

    import qualified Lang.Crucible.LLVM.Intrinsics.Declare as Decl

    import qualified Lang.Crucible.LLVM.Intrinsics.LLVM as LLVM

    import qualified Lang.Crucible.LLVM.Intrinsics.Libc as Libc

    import qualified Lang.Crucible.LLVM.Intrinsics.Libcxx as Libcxx

    @@ -91,10 +93,11 @@ register_llvm_overrides llvmModule defineOvrs declareOvrs llvmctx =
  
    -- and the structure of C++ demangled names to extract more information.

    filterTemplates ::

      [OverrideTemplate p sym ext arch] ->

      L.Declare ->

      Decl.SomeDeclare ->

      [OverrideTemplate p sym ext arch]

    filterTemplates ts decl = filter (matches nm . overrideTemplateMatcher) ts

     where L.Symbol nm = L.decName decl

    filterTemplates ts (Decl.SomeDeclare decl) =

      filter (matches nm . overrideTemplateMatcher) ts

      where L.Symbol nm = Decl.decName decl

    -- | Match a set of 'OverrideTemplate's against a single 'L.Declare',

    -- registering all the overrides that apply and returning them as a list.

    @@ -104,16 +107,17 @@ match_llvm_overrides ::
  
      -- | Overrides to attempt to match against this declaration

      [OverrideTemplate p sym ext arch] ->

      -- | Declaration of the function that might get overridden

      L.Declare ->

      Decl.SomeDeclare ->

      OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]

    match_llvm_overrides llvmctx acts decl =

    match_llvm_overrides llvmctx acts someDecl =

      llvmPtrWidth llvmctx $ \wptr -> withPtrWidth wptr $ do

        let acts' = filterTemplates acts decl

        let L.Symbol nm = L.decName decl

        let acts' = filterTemplates acts someDecl

        Decl.SomeDeclare decl <- pure someDecl

        let L.Symbol nm = Decl.decName decl

        let declnm = either (const Nothing) Just $ ABI.demangleName nm

        mbOvs <-

          forM (map overrideTemplateAction acts') $ \(MakeOverride act) ->

            case act decl declnm llvmctx of

            case act someDecl declnm llvmctx of

              Nothing -> pure Nothing

              Just sov@(SomeLLVMOverride ov) -> do

                register_llvm_override ov decl llvmctx

    @@ -128,7 +132,7 @@ register_llvm_overrides_ ::
  
      -- | Overrides to attempt to match against these declarations

      [OverrideTemplate p sym ext arch] ->

      -- | Declarations of the functions that might get overridden

      [L.Declare] ->

      [Decl.SomeDeclare] ->

      OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]

    register_llvm_overrides_ llvmctx acts decls =

      concat <$> forM decls (\decl -> match_llvm_overrides llvmctx acts decl)

    @@ -146,10 +150,11 @@ register_llvm_define_overrides ::
  
      [OverrideTemplate p sym LLVM arch] ->

      LLVMContext arch ->

      OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]

    register_llvm_define_overrides llvmModule addlOvrs llvmctx =

      let ?lc = llvmctx^.llvmTypeCtx in

      register_llvm_overrides_ llvmctx (addlOvrs ++ define_overrides) $

         (allModuleDeclares llvmModule)

    register_llvm_define_overrides llvmModule addlOvrs llvmctx = do

      let ?lc = llvmctx^.llvmTypeCtx

      decls <- Decl.fromLLVMWithWarnings (allModuleDeclares llvmModule)

      let ovs = map Cast.lowerOverrideTemplate (addlOvrs ++ define_overrides)

      register_llvm_overrides_ llvmctx ovs decls

    -- | Match a set of 'OverrideTemplate's against all the @declare@s in a

    -- 'L.Module', registering all the overrides that apply and returning them as

    @@ -165,10 +170,11 @@ register_llvm_declare_overrides ::
  
      [OverrideTemplate p sym LLVM arch] ->

      LLVMContext arch ->

      OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]

    register_llvm_declare_overrides llvmModule addlOvrs llvmctx =

    register_llvm_declare_overrides llvmModule addlOvrs llvmctx = do

      let ?lc = llvmctx^.llvmTypeCtx

      in register_llvm_overrides_ llvmctx (addlOvrs ++ declare_overrides) $

           L.modDeclares llvmModule

      decls <- Decl.fromLLVMWithWarnings (L.modDeclares llvmModule)

      let ovs = map Cast.lowerOverrideTemplate (addlOvrs ++ declare_overrides)

      register_llvm_overrides_ llvmctx ovs decls

    -- | Register overrides for declared-but-not-defined functions

    declare_overrides ::

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

llvm: Remove LLVM `declare`s from LLVM overrides #1705

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

llvm: Remove LLVM declares from LLVM overrides #1705

Are you sure you want to change the base?

Uh oh!

llvm: Remove LLVM declares from LLVM overrides #1705

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

llvm: Remove LLVM `declare`s from LLVM overrides #1705

llvm: Remove LLVM `declare`s from LLVM overrides #1705