llvm: Remove the LLVM declaration from LLVMOverride

[langston-barrett]

The LLVMOverride type has a L.Declare:

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

Lines 78 to 82 in 0834003

	-- | This type represents an implementation of an LLVM intrinsic function in
	-- Crucible.
	data LLVMOverride p sym args ret =
	LLVMOverride
	{ llvmOverride_declare :: L.Declare -- ^ An LLVM name and signature for this intrinsic

This is used to check that an override's "provided" declaration matches the declaration found in the LLVM module under the same name:

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

Lines 255 to 276 in 0834003

	-- | Check that the requested declaration matches the provided declaration. In
	-- this context, \"matching\" means that both declarations have identical names,
	-- as well as equal argument and result types. When checking types for equality,
	-- we consider opaque pointer types to be equal to non-opaque pointer types so
	-- that we do not have to define quite so many overrides with different
	-- combinations of pointer types.
	isMatchingDeclaration ::
	L.Declare {- ^ Requested declaration -} ->
	L.Declare {- ^ Provided declaration for intrinsic -} ->
	Bool
	isMatchingDeclaration requested provided = and
	[ L.decName requested == L.decName provided
	, matchingArgList (L.decArgs requested) (L.decArgs provided)
	, L.decRetType requested `L.eqTypeModuloOpaquePtrs` L.decRetType provided
	-- TODO? do we need to pay attention to various attributes?
	]
	where
	matchingArgList [] [] = True
	matchingArgList [] _ = L.decVarArgs requested
	matchingArgList _ [] = L.decVarArgs provided
	matchingArgList (x:xs) (y:ys) = x `L.eqTypeModuloOpaquePtrs` y && matchingArgList xs ys

Note, however that the equality check happens modulo opaque pointers, meaning that T* and ptr are treated as equal for all T. As LLVM has completed the migration to pointer types, none of the more-specific (non-opaque) in our overrides' L.Declares add any additional type-safety beyond just using ptr. We can remove the L.Declare from LLVMOverride and instead create a function TypeRepr t -> L.Type that maps LLVMPointerType sym w to LLVM's ptr. This would obviate our LLVM quasiquoters, and allow us to specify the types of each override just once (as Crucbile-LLVM types).

[langston-barrett]

Here's a first cut of functions to create an LLVM declaration from a Crucible-LLVM type signature:

llvmType :: HasPtrWidth wptr => TypeRepr t -> Maybe L.Type
llvmType =
  \case
    AnyRepr {} -> Nothing
    BoolRepr -> Just (L.PrimType (L.Integer 1))
    CharRepr {} -> Nothing
    BVRepr w -> intType w
    ComplexRealRepr {} -> Nothing
    FloatRepr {} -> Nothing  -- TODO?
    FunctionHandleRepr {} -> Nothing
    IEEEFloatRepr {} -> Nothing  -- TODO?
    IntegerRepr {} -> Nothing
    MaybeRepr {} -> Nothing
    NatRepr {} -> Nothing
    RealValRepr {} -> Nothing
    RecursiveRepr {} -> Nothing
    ReferenceRepr {} -> Nothing
    SequenceRepr {} -> Nothing
    StringRepr {} -> Nothing
    StringMapRepr {} -> Nothing
    StructRepr {} -> Nothing
    SymbolicArrayRepr {} -> Nothing
    SymbolicStructRepr {} -> Nothing
    UnitRepr -> Just (L.PrimType L.Void)
    VariantRepr {} -> Nothing
    VectorRepr {} -> Nothing
    WordMapRepr {} -> Nothing

    LLVMPointerRepr w ->
      case testEquality w ?ptrWidth of
        Just Refl -> Just L.PtrOpaque
        Nothing -> intType w
    IntrinsicRepr {} -> Nothing
  where
    intType :: NatRepr n -> Maybe L.Type
    intType w = 
      let natVal = natValue w
      in if natVal > fromIntegral (maxBound :: Word32)
         then Nothing
         else Just (L.PrimType (L.Integer (fromIntegral natVal)))

llvmOverrideDeclare ::
  HasPtrWidth w => 
  LLVMOverride p sym args ret ->
  Either (Some TypeRepr) L.Declare
llvmOverrideDeclare ov = do
  let getType :: forall t. TypeRepr t -> Either (Some TypeRepr) L.Type
      getType t =
        case llvmType t of
          Nothing -> Left (Some t)
          Just llTy -> Right llTy
  (Some args, isVarArgs) <-
    case Ctx.viewAssign (llvmOverride_args ov) of
      Ctx.AssignEmpty ->
        pure (Some (llvmOverride_args ov), False)
      Ctx.AssignExtend rest lastTy | Just Refl <- testEquality varArgsRepr lastTy ->
        pure (Some rest, True)
      _ ->
        pure (Some (llvmOverride_args ov), False)
  llvmArgs <- sequence (toListFC getType args)
  llvmRet <- getType (llvmOverride_ret ov)
  pure $
    L.Declare
    { L.decArgs = llvmArgs
    , L.decAttrs = []
    , L.decComdat = Nothing
    , L.decLinkage = Nothing
    , L.decName = llvmOverride_name ov
    , L.decRetType = llvmRet
    , L.decVarArgs = isVarArgs
    , L.decVisibility = Nothing
    }

llvmOverride_declare :: HasPtrWidth wptr => LLVMOverride p sym args ret -> L.Declare
llvmOverride_declare ov =
  case llvmOverrideDeclare ov of
    Right decl -> decl
    Left (Some tpr) -> 
      panic "Intrinsics.llvmOverride_declare"
        [ "Couldn't convert Crucible-LLVM type to LLVM type"
        , show tpr
        ]
{-# DEPRECATED llvmOverride_declare "Use llvmOverrideDeclare instead" #-}

[RyanGlScott]

Is isMatchingDeclaration the only place where we make use of llvmOverride_declare? If so, I'd be more enthusiastic about simply removing the field altogether and instead checking if two overrides have the same type by directly comparing the argument and result types as Crucible TypeReprs. This would avoid the need to reconstruct LLVM Types from Crucible TypeReprs, which is tricky. (For instance, I'm not entirely convinced that we'd always want to map LLVMPointerRepr to PtrOpaque—don't we use LLVMPointerReprs for both bitvectors and pointers?)

[langston-barrett]

Is isMatchingDeclaration the only place where we make use of llvmOverride_declare?

Looks like it, though that search doesn't capture pattern matches that don't use the record selector names.

If so, I'd be more enthusiastic about simply removing the field altogether and instead checking if two overrides have the same type by directly comparing the argument and result types as Crucible TypeReprs.

👍