{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
-- | This module defines a default loader for initial symbolic filesystem contents
--
-- It uses a simple convention to convert on-disk files and metadata into a
-- 'SymIO.InitialFileSystemContents'. This is not the only way to construct
-- initial filesystem contents, but it is a good default if a tool does not have
-- more specific needs.
--
-- The caller provides a single input: a path to a directory.  The directory
-- contains two things:
--
-- 1. A subdirectory named @root@ that contains the concrete files in the symbolic filesystem (i.e., the directory mapped to @/@)
-- 2. (Optional) A file named @symbolic-manifest.json@, which describes symbolic files and overlays
--
-- The symbolic manifest specifies the contents of symbolic files, including
-- constraints on symbolic values.  Furthermore, it enables users to specify
-- that concrete files in the provided filesystem have symbolic values overlaid
-- over the concrete values. If an overlay is specified in the symbolic
-- manifest, the referenced concrete file /must/ exist.
--
-- Note: future versions of this interface could support symbolic filesystems
-- stored in zip or tar files.
module Lang.Crucible.SymIO.Loader (
    loadInitialFiles
  , FileSystemLoadError(..)
  ) where

import qualified Control.Exception as X
import qualified Data.Aeson as JSON
import qualified Data.ByteString as BS
import qualified Data.Foldable as F
import qualified Data.List as List
import qualified Data.Map.Strict as Map
import           Data.Maybe ( fromMaybe )
import qualified Data.Parameterized.NatRepr as PN
import qualified Data.Text as T
import qualified Data.Traversable as T
import           Data.Word ( Word64 )
import           GHC.Generics ( Generic )
import qualified System.Directory as SD
import           System.FilePath ( (</>) )
import qualified System.FilePath.Find as SFF
import qualified What4.BaseTypes as WT
import qualified What4.Interface as WI

import qualified Lang.Crucible.Backend as LCB
import qualified Lang.Crucible.SymIO as SymIO

data FileSystemLoadError = ErrorDecodingJSON String
                         | forall k . FileSpecifiedAsSymbolicAndConcrete (SymIO.FDTarget k)

deriving instance Show FileSystemLoadError

instance X.Exception FileSystemLoadError

-- | The specification for the symbolic contents of a file in the symbolic
-- filesystem
--
-- There will be multiple specifications including:
--
--   * Complete symbolic file specifications (including concrete regions)
--   * Symbolic overlays on otherwise concrete files
data SymbolicFileContents =
  SymbolicContents { symbolicContentSize :: Word64
                   }
  deriving (Show, Generic)

instance JSON.FromJSON SymbolicFileContents

-- | A description of the contents of a symbolic filesystem
--
-- This includes high-level metadata and the specifications for symbolic files.
--
-- Note that the file paths are /absolute/ paths within the symbolic filesystem
data SymbolicManifest =
  SymbolicManifest { symbolicFiles :: [(FilePath, SymbolicFileContents)]
                   , useStdout :: Bool
                   , useStderr :: Bool
                   }
  deriving (Show, Generic)

instance JSON.FromJSON SymbolicManifest

-- | A file path that is absolute within the symbolic filesystem we are building
newtype AbsolutePath = AbsolutePath FilePath
  deriving (Eq, Ord, Show)

-- | Create an absolute path *within the symbolic filesystem* based on the root
-- FS path and the absolute path to a file in the real filesystem
--
-- This effectively strips the real root FS off of the absolute file path,
-- creating an absolute path within the symbolic FS.
toInternalAbsolutePath
  :: FilePath
  -- ^ The path to the root filesystem in the real (non-symbolic) filesystem
  -> FilePath
  -- ^ The absolute path to the file in the real (non-symbolic) filesystem
  -> AbsolutePath
toInternalAbsolutePath pfx x = AbsolutePath (fromMaybe x (List.stripPrefix pfx x))

createSymbolicFile
  :: (LCB.IsSymInterface sym)
  => sym
  -> (FilePath, SymbolicFileContents)
  -> IO (SymIO.FDTarget SymIO.In, [WI.SymBV sym 8])
createSymbolicFile sym (internalAbsPath, symContent) =
  case symContent of
    SymbolicContents { symbolicContentSize = numBytes } -> do
      bytes <- T.forM [0.. numBytes - 1] $ \byteNum -> do
        let symName = WI.safeSymbol (internalAbsPath ++ "_" ++ show byteNum)
        WI.freshConstant sym symName (WT.BaseBVRepr (PN.knownNat @8))
      return (SymIO.FileTarget internalAbsPath, bytes)

-- | Load the symbolic filesystem at the given file path
--
-- Note that this will throw an exception if:
--
--   * The symbolic manifest declares an overlay for a file that does not exist in the concrete portion of the filesystem
loadInitialFiles
  :: (LCB.IsSymInterface sym)
  => sym
  -> FilePath
  -> IO (SymIO.InitialFileSystemContents sym)
loadInitialFiles sym fsRoot = do
  -- FIXME: Use the lower-level fold primitive that enables exception handling;
  -- this version just spews errors to stderr, which is inappropriate.
  let concreteFilesRoot = fsRoot </> "root"
  let isRegular = SFF.fileType SFF.==? SFF.RegularFile
  concreteFilePaths <- SFF.find SFF.always isRegular concreteFilesRoot

  -- Check if standard input has been specified as a concrete file
  let stdinPath = fsRoot </> T.unpack (SymIO.fdTargetToText SymIO.StdinTarget)
  hasStdin <- SD.doesFileExist stdinPath

  -- Note that all of these paths are absolute *if* @fsRoot@ was absolute.
  -- Also, if it has leading .. components, they will be included.  We need to
  -- normalize these paths so that they have @fsRoot@ stripped off (and thus are
  -- absolute in the symbolic filesystem)
  let relativePaths = [ (p, toInternalAbsolutePath concreteFilesRoot p)
                      | p <- concreteFilePaths
                      ]
  concFiles <- mapM (\(p, name) -> (name,) <$> BS.readFile p) relativePaths
  let concMap0 = Map.fromList [ (SymIO.FileTarget p, bytes) | (AbsolutePath p, bytes) <- concFiles ]
  concMap1 <-
    if | hasStdin -> do
           stdinBytes <- BS.readFile stdinPath
           return (Map.insert SymIO.StdinTarget stdinBytes concMap0)
       | otherwise -> return concMap0

  let manifestFilePath = fsRoot </> "system-manifest.json"
  hasManifest <- SD.doesFileExist manifestFilePath
  case hasManifest of
    False ->
      return SymIO.InitialFileSystemContents { SymIO.concreteFiles = concMap1
                                             , SymIO.symbolicFiles = Map.empty
                                             , SymIO.useStdout = False
                                             , SymIO.useStderr = False
                                             }
    True -> do
      manifestBytes <- BS.readFile manifestFilePath
      case JSON.eitherDecodeStrict manifestBytes of
        Left msg -> X.throwIO (ErrorDecodingJSON msg)
        Right symManifest -> do
          symFiles <- mapM (createSymbolicFile sym) (symbolicFiles symManifest)
          F.forM_ symFiles $ \(fdTarget, _) -> do
            case Map.lookup fdTarget concMap1 of
              Nothing -> return ()
              Just _ -> X.throwIO (FileSpecifiedAsSymbolicAndConcrete fdTarget)
          return SymIO.InitialFileSystemContents { SymIO.concreteFiles = concMap1
                                                 , SymIO.symbolicFiles = Map.fromList symFiles
                                                 , SymIO.useStdout = useStdout symManifest
                                                 , SymIO.useStderr = useStderr symManifest
                                                 }