{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
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
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
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
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)
toInternalAbsolutePath
:: FilePath
-> FilePath
-> 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)
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
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
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
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
}