{-# 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 { SymbolicFileContents -> Word64
symbolicContentSize :: Word64
                   }
  deriving (Int -> SymbolicFileContents -> ShowS
[SymbolicFileContents] -> ShowS
SymbolicFileContents -> String
(Int -> SymbolicFileContents -> ShowS)
-> (SymbolicFileContents -> String)
-> ([SymbolicFileContents] -> ShowS)
-> Show SymbolicFileContents
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SymbolicFileContents -> ShowS
showsPrec :: Int -> SymbolicFileContents -> ShowS
$cshow :: SymbolicFileContents -> String
show :: SymbolicFileContents -> String
$cshowList :: [SymbolicFileContents] -> ShowS
showList :: [SymbolicFileContents] -> ShowS
Show, (forall x. SymbolicFileContents -> Rep SymbolicFileContents x)
-> (forall x. Rep SymbolicFileContents x -> SymbolicFileContents)
-> Generic SymbolicFileContents
forall x. Rep SymbolicFileContents x -> SymbolicFileContents
forall x. SymbolicFileContents -> Rep SymbolicFileContents x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymbolicFileContents -> Rep SymbolicFileContents x
from :: forall x. SymbolicFileContents -> Rep SymbolicFileContents x
$cto :: forall x. Rep SymbolicFileContents x -> SymbolicFileContents
to :: forall x. Rep SymbolicFileContents x -> SymbolicFileContents
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 { SymbolicManifest -> [(String, SymbolicFileContents)]
symbolicFiles :: [(FilePath, SymbolicFileContents)]
                   , SymbolicManifest -> Bool
useStdout :: Bool
                   , SymbolicManifest -> Bool
useStderr :: Bool
                   }
  deriving (Int -> SymbolicManifest -> ShowS
[SymbolicManifest] -> ShowS
SymbolicManifest -> String
(Int -> SymbolicManifest -> ShowS)
-> (SymbolicManifest -> String)
-> ([SymbolicManifest] -> ShowS)
-> Show SymbolicManifest
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SymbolicManifest -> ShowS
showsPrec :: Int -> SymbolicManifest -> ShowS
$cshow :: SymbolicManifest -> String
show :: SymbolicManifest -> String
$cshowList :: [SymbolicManifest] -> ShowS
showList :: [SymbolicManifest] -> ShowS
Show, (forall x. SymbolicManifest -> Rep SymbolicManifest x)
-> (forall x. Rep SymbolicManifest x -> SymbolicManifest)
-> Generic SymbolicManifest
forall x. Rep SymbolicManifest x -> SymbolicManifest
forall x. SymbolicManifest -> Rep SymbolicManifest x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymbolicManifest -> Rep SymbolicManifest x
from :: forall x. SymbolicManifest -> Rep SymbolicManifest x
$cto :: forall x. Rep SymbolicManifest x -> SymbolicManifest
to :: forall x. Rep SymbolicManifest x -> SymbolicManifest
Generic)

instance JSON.FromJSON SymbolicManifest

-- | A file path that is absolute within the symbolic filesystem we are building
newtype AbsolutePath = AbsolutePath FilePath
  deriving (AbsolutePath -> AbsolutePath -> Bool
(AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool) -> Eq AbsolutePath
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbsolutePath -> AbsolutePath -> Bool
== :: AbsolutePath -> AbsolutePath -> Bool
$c/= :: AbsolutePath -> AbsolutePath -> Bool
/= :: AbsolutePath -> AbsolutePath -> Bool
Eq, Eq AbsolutePath
Eq AbsolutePath =>
(AbsolutePath -> AbsolutePath -> Ordering)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> AbsolutePath)
-> (AbsolutePath -> AbsolutePath -> AbsolutePath)
-> Ord AbsolutePath
AbsolutePath -> AbsolutePath -> Bool
AbsolutePath -> AbsolutePath -> Ordering
AbsolutePath -> AbsolutePath -> AbsolutePath
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: AbsolutePath -> AbsolutePath -> Ordering
compare :: AbsolutePath -> AbsolutePath -> Ordering
$c< :: AbsolutePath -> AbsolutePath -> Bool
< :: AbsolutePath -> AbsolutePath -> Bool
$c<= :: AbsolutePath -> AbsolutePath -> Bool
<= :: AbsolutePath -> AbsolutePath -> Bool
$c> :: AbsolutePath -> AbsolutePath -> Bool
> :: AbsolutePath -> AbsolutePath -> Bool
$c>= :: AbsolutePath -> AbsolutePath -> Bool
>= :: AbsolutePath -> AbsolutePath -> Bool
$cmax :: AbsolutePath -> AbsolutePath -> AbsolutePath
max :: AbsolutePath -> AbsolutePath -> AbsolutePath
$cmin :: AbsolutePath -> AbsolutePath -> AbsolutePath
min :: AbsolutePath -> AbsolutePath -> AbsolutePath
Ord, Int -> AbsolutePath -> ShowS
[AbsolutePath] -> ShowS
AbsolutePath -> String
(Int -> AbsolutePath -> ShowS)
-> (AbsolutePath -> String)
-> ([AbsolutePath] -> ShowS)
-> Show AbsolutePath
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbsolutePath -> ShowS
showsPrec :: Int -> AbsolutePath -> ShowS
$cshow :: AbsolutePath -> String
show :: AbsolutePath -> String
$cshowList :: [AbsolutePath] -> ShowS
showList :: [AbsolutePath] -> ShowS
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 :: String -> String -> AbsolutePath
toInternalAbsolutePath String
pfx String
x = String -> AbsolutePath
AbsolutePath (String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
x (String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix String
pfx String
x))

createSymbolicFile
  :: (LCB.IsSymInterface sym)
  => sym
  -> (FilePath, SymbolicFileContents)
  -> IO (SymIO.FDTarget SymIO.In, [WI.SymBV sym 8])
createSymbolicFile :: forall sym.
IsSymInterface sym =>
sym
-> (String, SymbolicFileContents)
-> IO (FDTarget In, [SymBV sym 8])
createSymbolicFile sym
sym (String
internalAbsPath, SymbolicFileContents
symContent) =
  case SymbolicFileContents
symContent of
    SymbolicContents { symbolicContentSize :: SymbolicFileContents -> Word64
symbolicContentSize = Word64
numBytes } -> do
      [SymBV sym 8]
bytes <- [Word64] -> (Word64 -> IO (SymBV sym 8)) -> IO [SymBV sym 8]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
T.forM [Word64
0.. Word64
numBytes Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1] ((Word64 -> IO (SymBV sym 8)) -> IO [SymBV sym 8])
-> (Word64 -> IO (SymBV sym 8)) -> IO [SymBV sym 8]
forall a b. (a -> b) -> a -> b
$ \Word64
byteNum -> do
        let symName :: SolverSymbol
symName = String -> SolverSymbol
WI.safeSymbol (String
internalAbsPath String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. Show a => a -> String
show Word64
byteNum)
        sym
-> SolverSymbol -> BaseTypeRepr ('BaseBVType 8) -> IO (SymBV sym 8)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
forall (tp :: BaseType).
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
WI.freshConstant sym
sym SolverSymbol
symName (NatRepr 8 -> BaseTypeRepr ('BaseBVType 8)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
WT.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
PN.knownNat @8))
      (FDTarget In, [SymBV sym 8]) -> IO (FDTarget In, [SymBV sym 8])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> FDTarget In
SymIO.FileTarget String
internalAbsPath, [SymBV sym 8]
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 :: forall sym.
IsSymInterface sym =>
sym -> String -> IO (InitialFileSystemContents sym)
loadInitialFiles sym
sym String
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 :: String
concreteFilesRoot = String
fsRoot String -> ShowS
</> String
"root"
  let isRegular :: FindClause Bool
isRegular = FindClause FileType
SFF.fileType FindClause FileType -> FileType -> FindClause Bool
forall a. Eq a => FindClause a -> a -> FindClause Bool
SFF.==? FileType
SFF.RegularFile
  [String]
concreteFilePaths <- FindClause Bool -> FindClause Bool -> String -> IO [String]
SFF.find FindClause Bool
SFF.always FindClause Bool
isRegular String
concreteFilesRoot

  -- Check if standard input has been specified as a concrete file
  let stdinPath :: String
stdinPath = String
fsRoot String -> ShowS
</> Text -> String
T.unpack (FDTarget In -> Text
forall (k :: TargetDirection). FDTarget k -> Text
SymIO.fdTargetToText FDTarget In
SymIO.StdinTarget)
  Bool
hasStdin <- String -> IO Bool
SD.doesFileExist String
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 :: [(String, AbsolutePath)]
relativePaths = [ (String
p, String -> String -> AbsolutePath
toInternalAbsolutePath String
concreteFilesRoot String
p)
                      | String
p <- [String]
concreteFilePaths
                      ]
  [(AbsolutePath, ByteString)]
concFiles <- ((String, AbsolutePath) -> IO (AbsolutePath, ByteString))
-> [(String, AbsolutePath)] -> IO [(AbsolutePath, ByteString)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(String
p, AbsolutePath
name) -> (AbsolutePath
name,) (ByteString -> (AbsolutePath, ByteString))
-> IO ByteString -> IO (AbsolutePath, ByteString)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO ByteString
BS.readFile String
p) [(String, AbsolutePath)]
relativePaths
  let concMap0 :: Map (FDTarget In) ByteString
concMap0 = [(FDTarget In, ByteString)] -> Map (FDTarget In) ByteString
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (String -> FDTarget In
SymIO.FileTarget String
p, ByteString
bytes) | (AbsolutePath String
p, ByteString
bytes) <- [(AbsolutePath, ByteString)]
concFiles ]
  Map (FDTarget In) ByteString
concMap1 <-
    if | Bool
hasStdin -> do
           ByteString
stdinBytes <- String -> IO ByteString
BS.readFile String
stdinPath
           Map (FDTarget In) ByteString -> IO (Map (FDTarget In) ByteString)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FDTarget In
-> ByteString
-> Map (FDTarget In) ByteString
-> Map (FDTarget In) ByteString
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FDTarget In
SymIO.StdinTarget ByteString
stdinBytes Map (FDTarget In) ByteString
concMap0)
       | Bool
otherwise -> Map (FDTarget In) ByteString -> IO (Map (FDTarget In) ByteString)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Map (FDTarget In) ByteString
concMap0

  let manifestFilePath :: String
manifestFilePath = String
fsRoot String -> ShowS
</> String
"system-manifest.json"
  Bool
hasManifest <- String -> IO Bool
SD.doesFileExist String
manifestFilePath
  case Bool
hasManifest of
    Bool
False ->
      InitialFileSystemContents sym -> IO (InitialFileSystemContents sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SymIO.InitialFileSystemContents { concreteFiles :: Map (FDTarget In) ByteString
SymIO.concreteFiles = Map (FDTarget In) ByteString
concMap1
                                             , symbolicFiles :: Map (FDTarget In) [SymBV sym 8]
SymIO.symbolicFiles = Map (FDTarget In) [SymBV sym 8]
forall k a. Map k a
Map.empty
                                             , useStdout :: Bool
SymIO.useStdout = Bool
False
                                             , useStderr :: Bool
SymIO.useStderr = Bool
False
                                             }
    Bool
True -> do
      ByteString
manifestBytes <- String -> IO ByteString
BS.readFile String
manifestFilePath
      case ByteString -> Either String SymbolicManifest
forall a. FromJSON a => ByteString -> Either String a
JSON.eitherDecodeStrict ByteString
manifestBytes of
        Left String
msg -> FileSystemLoadError -> IO (InitialFileSystemContents sym)
forall e a. Exception e => e -> IO a
X.throwIO (String -> FileSystemLoadError
ErrorDecodingJSON String
msg)
        Right SymbolicManifest
symManifest -> do
          [(FDTarget In, [SymBV sym 8])]
symFiles <- ((String, SymbolicFileContents) -> IO (FDTarget In, [SymBV sym 8]))
-> [(String, SymbolicFileContents)]
-> IO [(FDTarget In, [SymBV sym 8])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (sym
-> (String, SymbolicFileContents)
-> IO (FDTarget In, [SymBV sym 8])
forall sym.
IsSymInterface sym =>
sym
-> (String, SymbolicFileContents)
-> IO (FDTarget In, [SymBV sym 8])
createSymbolicFile sym
sym) (SymbolicManifest -> [(String, SymbolicFileContents)]
symbolicFiles SymbolicManifest
symManifest)
          [(FDTarget In, [SymBV sym 8])]
-> ((FDTarget In, [SymBV sym 8]) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
F.forM_ [(FDTarget In, [SymBV sym 8])]
symFiles (((FDTarget In, [SymBV sym 8]) -> IO ()) -> IO ())
-> ((FDTarget In, [SymBV sym 8]) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(FDTarget In
fdTarget, [SymBV sym 8]
_) -> do
            case FDTarget In -> Map (FDTarget In) ByteString -> Maybe ByteString
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FDTarget In
fdTarget Map (FDTarget In) ByteString
concMap1 of
              Maybe ByteString
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just ByteString
_ -> FileSystemLoadError -> IO ()
forall e a. Exception e => e -> IO a
X.throwIO (FDTarget In -> FileSystemLoadError
forall (k :: TargetDirection). FDTarget k -> FileSystemLoadError
FileSpecifiedAsSymbolicAndConcrete FDTarget In
fdTarget)
          InitialFileSystemContents sym -> IO (InitialFileSystemContents sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SymIO.InitialFileSystemContents { concreteFiles :: Map (FDTarget In) ByteString
SymIO.concreteFiles = Map (FDTarget In) ByteString
concMap1
                                                 , symbolicFiles :: Map (FDTarget In) [SymBV sym 8]
SymIO.symbolicFiles = [(FDTarget In, [SymBV sym 8])] -> Map (FDTarget In) [SymBV sym 8]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(FDTarget In, [SymBV sym 8])]
symFiles
                                                 , useStdout :: Bool
SymIO.useStdout = SymbolicManifest -> Bool
useStdout SymbolicManifest
symManifest
                                                 , useStderr :: Bool
SymIO.useStderr = SymbolicManifest -> Bool
useStderr SymbolicManifest
symManifest
                                                 }