{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Translation.Types
-- Description      : Translation of LLVM AST into Crucible control-flow graph
-- Copyright        : (c) Galois, Inc 2014-2015
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
--
-- This module defines the translation from LLVM types to Crucible types.
--
-- The translation of the LLVM types themselves is not so difficult;
-- however, navigating the fact that Crucible expressions are strongly
-- typed at the Haskell level, whereas the LLVM types are not makes for
-- some slightly strange programming idioms.  In particular, all the
-- functions that do the type translation are written in a polymorphic
-- continuation-passing style.
----------------------------------------------------------------------

module Lang.Crucible.LLVM.Translation.Types
( VarArgs
, varArgsRepr
, llvmTypesAsCtx
, llvmTypeAsRepr
, llvmRetTypeAsRepr
, llvmDeclToFunHandleRepr
, llvmDeclToFunHandleRepr'
, LLVMPointerType
, pattern PtrWidth
, pattern LLVMPointerRepr
, declareFromDefine
, allModuleDeclares
, liftMemType
, liftRetType
, liftDeclare
) where

import qualified Control.Monad.Fail as Fail
import           Data.Foldable
import           Data.String

import qualified Text.LLVM.AST as L
import           Prettyprinter

import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Some


import           Lang.Crucible.Panic(panic)
import           Lang.Crucible.Types

import           Lang.Crucible.LLVM.MemModel.Pointer
import           Lang.Crucible.LLVM.MemType
import           Lang.Crucible.LLVM.MalformedLLVMModule
import qualified Lang.Crucible.LLVM.PrettyPrint as LPP
import           Lang.Crucible.LLVM.TypeContext as TyCtx



type VarArgs   = VectorType AnyType

varArgsRepr :: TypeRepr VarArgs
varArgsRepr = VectorRepr AnyRepr

------------------------------------------------------------------------
-- LLVM AST utilities

declareFromDefine :: L.Define -> L.Declare
declareFromDefine d =
  L.Declare { L.decLinkage = L.defLinkage d
            , L.decVisibility = L.defVisibility d
            , L.decRetType = L.defRetType d
            , L.decName = L.defName d
            , L.decArgs = L.typedType <$> L.defArgs d
            , L.decVarArgs = L.defVarArgs d
            , L.decAttrs   = L.defAttrs d
            , L.decComdat  = mempty
            }

-- | Return all declarations derived from both external symbols and
-- internal definitions.
allModuleDeclares :: L.Module -> [L.Declare]
allModuleDeclares m = L.modDeclares m ++ def_decls
  where def_decls = declareFromDefine <$> L.modDefines m

-----------------------------------------------------------------------------------------
-- Type translations

-- | Translate a list of LLVM expressions into a crucible type context,
--   which is passed into the given continuation.
llvmTypesAsCtx :: forall a wptr
                . HasPtrWidth wptr
               => [MemType]
               -> (forall ctx. CtxRepr ctx -> a)
               -> a
llvmTypesAsCtx xs f = go (concatMap (toList . llvmTypeToRepr) xs) Ctx.empty
 where go :: forall ctx. [Some TypeRepr] -> CtxRepr ctx -> a
       go []       ctx      = f ctx
       go (Some tp:tps) ctx = go tps (ctx Ctx.:> tp)

-- | Translate an LLVM type into a crucible type, which is passed into
--   the given continuation
llvmTypeAsRepr :: forall a wptr
                . HasPtrWidth wptr
               => MemType
               -> (forall tp. TypeRepr tp -> a)
               -> a
llvmTypeAsRepr xs f = go (llvmTypeToRepr xs)
 where go :: Maybe (Some TypeRepr) -> a
       go Nothing         = f UnitRepr
       go (Just (Some x)) = f x

-- | Translate an LLVM return type into a crucible type, which is passed into
--   the given continuation
llvmRetTypeAsRepr :: forall a wptr
                   . HasPtrWidth wptr
                  => Maybe MemType
                  -> (forall tp. TypeRepr tp -> a)
                  -> a
llvmRetTypeAsRepr Nothing   f = f UnitRepr
llvmRetTypeAsRepr (Just tp) f = llvmTypeAsRepr tp f

-- | Actually perform the type translation
llvmTypeToRepr :: HasPtrWidth wptr => MemType -> Maybe (Some TypeRepr)
llvmTypeToRepr (ArrayType _ tp)  = Just $ llvmTypeAsRepr tp (\t -> Some (VectorRepr t))
llvmTypeToRepr (VecType _ tp)    = Just $ llvmTypeAsRepr tp (\t-> Some (VectorRepr t))
llvmTypeToRepr (StructType si)   = Just $ llvmTypesAsCtx tps (\ts -> Some (StructRepr ts))
  where tps = map fiType $ toList $ siFields si
llvmTypeToRepr (PtrType _)  = Just $ Some (LLVMPointerRepr PtrWidth)
llvmTypeToRepr PtrOpaqueType = Just $ Some (LLVMPointerRepr PtrWidth)
llvmTypeToRepr FloatType    = Just $ Some (FloatRepr SingleFloatRepr)
llvmTypeToRepr DoubleType   = Just $ Some (FloatRepr DoubleFloatRepr)
llvmTypeToRepr X86_FP80Type = Just $ Some (FloatRepr X86_80FloatRepr)
llvmTypeToRepr MetadataType = Nothing
llvmTypeToRepr (IntType n) =
   case mkNatRepr n of
     Some w | Just LeqProof <- isPosNat w -> Just $ Some (LLVMPointerRepr w)
     _ -> panic "Translation.Types.llvmTypeToRepr"
              [" *** invalid integer width " ++ show n]

-- | Compute the function Crucible function signature
--   that corresponds to the given LLVM function declaration.
llvmDeclToFunHandleRepr
   :: HasPtrWidth wptr
   => FunDecl
   -> (forall args ret. CtxRepr args -> TypeRepr ret -> a)
   -> a
llvmDeclToFunHandleRepr decl k =
  llvmTypesAsCtx (fdArgTypes decl) $ \args ->
    llvmRetTypeAsRepr (fdRetType decl) $ \ret ->
      if fdVarArgs decl then
        k (args Ctx.:> varArgsRepr) ret
      else
        k args ret


llvmDeclToFunHandleRepr' ::
   (?lc :: TypeContext, HasPtrWidth wptr, Fail.MonadFail m) =>
   L.Declare ->
   (forall args ret. CtxRepr args -> TypeRepr ret -> m a) ->
   m a
llvmDeclToFunHandleRepr' decl k =
  case liftDeclare decl of
    Left msg ->
      malformedLLVMModule
        ( "Invalid declaration for:" <+> fromString (show (L.decName decl)) )
        [ fromString (show (LPP.ppDeclare decl))
        , fromString msg
        ]

    Right fd -> llvmDeclToFunHandleRepr fd k