llvm: Remove the LLVM declaration from `LLVMOverride`

[langston-barrett]

The LLVMOverride type has a L.Declare:

https://github.com/GaloisInc/crucible/blob/0834003f70242a65e6850a5e54c8d882c3106b6c/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs#L78-L82

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

https://github.com/GaloisInc/crucible/blob/0834003f70242a65e6850a5e54c8d882c3106b6c/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs#L255-L276

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.

:+1: