-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.SymIO.Types
-- Description      : Crucible type definitions related to VFS
-- Copyright        : (c) Galois, Inc 2020
-- License          : BSD3
-- Maintainer       : Daniel Matichuk <dmatichuk@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}
module Lang.Crucible.SymIO.Types
  ( symIOIntrinsicTypes
  , FilePointer(..)
  , FilePointerType
  , pattern FilePointerRepr
  , FileHandle
  , FileHandleType
  , pattern FileHandleRepr
  , FileIdent
  , FileIdentType
  , FileSystem(..)
  , muxFileSystem
  , FileSystemType
  , FileSystemIndex
  , pattern FileSystemRepr
  , File(..)
  , pattern FileRepr
  , FileType
  , muxFile
  , DataChunk
  , SizedDataChunk
  , SizedDataChunkType
  )
where

import           Data.Typeable
import           GHC.TypeNats

import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.Context
import           Data.Parameterized.Classes
import           Data.Parameterized.NatRepr

import           Lang.Crucible.Backend
import           Lang.Crucible.Simulator.RegValue
import           Lang.Crucible.Types
import           Lang.Crucible.Simulator.Intrinsics

import           What4.Interface
import qualified What4.CachedArray as CA

-- | The intrinsic types used in the symbolic filesystem
symIOIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym
symIOIntrinsicTypes = id
  . MapF.insert (knownSymbol :: SymbolRepr "VFS_filesystem") IntrinsicMuxFn
  . MapF.insert (knownSymbol :: SymbolRepr "VFS_file") IntrinsicMuxFn
  . MapF.insert (knownSymbol :: SymbolRepr "VFS_filepointer") IntrinsicMuxFn
  $ MapF.empty

-- | An identifier for a file, which must be resolved into a 'File' to access
-- the underlying filesystem.
--
-- This is a file path
type FileIdent sym = RegValue sym FileIdentType

-- | The crucible-level type of 'FileIdent'
type FileIdentType = StringType Char8

-- | The crucible-level type of 'FileSystem'
type FileSystemType w = IntrinsicType "VFS_filesystem" (EmptyCtx ::> BVType w)

-- | Defines the current state of a symbolic filesystem.
data FileSystem sym w =
  FileSystem
    {
      fsPtrSize :: NatRepr w
    , fsFileNames :: RegValue sym (StringMapType (FileType w))
    -- ^ map from concrete file identifiers to files
    , fsFileSizes :: CA.CachedArray sym (EmptyCtx ::> BaseIntegerType) (BaseBVType w)
    -- ^ a symbolic map from files to their size
    , fsSymData :: CA.CachedArray sym (EmptyCtx ::> BaseBVType w ::> BaseIntegerType) (BaseBVType 8)
    -- ^ array representing symbolic file contents
    , fsConstraints :: forall a. ((IsSymInterface sym, 1 <= w) => a) -> a
    }

-- | A base index into the filesystem, consistent of a file identifier and an offset into that file.
type FileSystemIndex sym w = Assignment (SymExpr sym) (EmptyCtx ::> BaseBVType w ::> BaseIntegerType)

muxFileSystem ::
  IsSymInterface sym =>
  sym ->
  Pred sym ->
  FileSystem sym w ->
  FileSystem sym w ->
  IO (FileSystem sym w)
muxFileSystem sym p fsT fsF = do
  symData <- CA.muxArrays sym p (fsSymData fsT) (fsSymData fsF)
  symFiles <- muxStringMap sym (muxFile sym) p (fsFileNames fsT) (fsFileNames fsF)
  symFileSizes <- CA.muxArrays sym p (fsFileSizes fsT) (fsFileSizes fsF)
  return $ fsT { fsSymData  = symData, fsFileNames = symFiles, fsFileSizes = symFileSizes }

instance (IsSymInterface sym) => IntrinsicClass sym "VFS_filesystem" where
  type Intrinsic sym "VFS_filesystem" (EmptyCtx ::> BVType w) = FileSystem sym w

  muxIntrinsic sym _iTypes _nm (Empty :> (BVRepr _w)) = muxFileSystem sym
  muxIntrinsic _ _ nm ctx = \_ _ _ -> typeError nm ctx

pattern FileSystemRepr :: () => (1 <= w, ty ~ FileSystemType w) => NatRepr w -> TypeRepr ty
pattern FileSystemRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "VFS_filesystem") -> Just Refl)
                                           (Empty :> BVRepr w)
  where
    FileSystemRepr w = IntrinsicRepr knownSymbol (Empty :> BVRepr w)

-- | The crucible type of file handles.
type FileHandleType w = ReferenceType (MaybeType (FilePointerType w))

-- |  A file handle is a mutable file pointer that increments every time it is read.
type FileHandle sym w = RegValue sym (FileHandleType w)

-- | A 'File' represents a file in the filesystem independent
-- of any open handles to it
--
-- The 'NatRepr' records the size of file pointers (in bits)
--
-- The 'SymInteger' is an index into the underlying array of arrays that represents file contents
data File sym w = File (NatRepr w) (SymInteger sym)

pattern FileRepr :: () => (1 <= w, ty ~ FileType w) => NatRepr w -> TypeRepr ty
pattern FileRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "VFS_file") -> Just Refl)
                                           (Empty :> BVRepr w)
  where
    FileRepr w = IntrinsicRepr knownSymbol (Empty :> BVRepr w)

-- | The crucible-level type of 'File'
type FileType w = IntrinsicType "VFS_file" (EmptyCtx ::> BVType w)

instance (IsSymInterface sym) => IntrinsicClass sym "VFS_file" where
  type Intrinsic sym "VFS_file" (EmptyCtx ::> BVType w) = File sym w

  muxIntrinsic sym _iTypes _nm (Empty :> BVRepr _w) = muxFile sym
  muxIntrinsic _ _ nm ctx = typeError nm ctx

muxFile ::
  IsSymInterface sym =>
  sym ->
  Pred sym ->
  File sym w ->
  File sym w ->
  IO (File sym w)
muxFile sym p (File w f1) (File _w f2) = File w <$> baseTypeIte sym p f1 f2

-- | A file pointer represents an index into a particular file.
--
-- The 'File' is similar to an inode, and uniquely identifies a file (as an
-- index into the array of all files).  The 'SymBV' is the offset into the file
-- that the file pointer is currently at (i.e., where the next read or write
-- will be from).
data FilePointer sym w =
  FilePointer (File sym w) (SymBV sym w) 

-- | The crucible type of 'FilePointer'
type FilePointerType w = IntrinsicType "VFS_filepointer" (EmptyCtx ::> BVType w)

instance (IsSymInterface sym) => IntrinsicClass sym "VFS_filepointer" where
  type Intrinsic sym "VFS_filepointer" (EmptyCtx ::> BVType w) = FilePointer sym w

  muxIntrinsic sym _iTypes _nm (Empty :> (BVRepr _w)) = muxFilePointer sym
  muxIntrinsic _ _ nm ctx = typeError nm ctx

-- | Mux on 'FilePointer'
muxFilePointer ::
  (1 <= w) =>
  IsSymInterface sym =>
  sym ->
  Pred sym ->
  FilePointer sym w ->
  FilePointer sym w ->
  IO (FilePointer sym w)
muxFilePointer sym p (FilePointer f1 off1) (FilePointer f2 off2) =
  do b   <- muxFile sym p f1 f2
     off <- bvIte sym p off1 off2
     return $ FilePointer b off


type DataChunk sym w = CA.ArrayChunk sym (BaseBVType w) (BaseBVType 8)

type SizedDataChunkType w = SymbolicStructType (EmptyCtx ::> BaseArrayType (EmptyCtx ::> BaseBVType w) (BaseBVType 8) ::> BaseBVType w)
type SizedDataChunk sym w = SymStruct sym (EmptyCtx ::> BaseArrayType (EmptyCtx ::> BaseBVType w) (BaseBVType 8) ::> BaseBVType w)

-- | A file handle is a reference to an optional file pointer
--
-- If the file pointer is not present, the file handle is closed. Otherwise, the
-- file pointer is the current pointer into the file (i.e., that will be read
-- from or written to next).
--
-- Note that this is just the repr and the real file handle value is symbolic
-- and stored in a Crucible reference.
pattern FileHandleRepr :: () => (1 <= w, ty ~ FileHandleType w) => NatRepr w -> TypeRepr ty
pattern FileHandleRepr w = ReferenceRepr (MaybeRepr (FilePointerRepr w))

pattern FilePointerRepr :: () => (1 <= w, ty ~ FilePointerType w) => NatRepr w -> TypeRepr ty
pattern FilePointerRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "VFS_filepointer") -> Just Refl)
                                           (Empty :> BVRepr w)
  where
    FilePointerRepr w = IntrinsicRepr knownSymbol (Empty :> BVRepr w)