| -- | |
| -- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) | |
| -- | |
| -- SPDX-License-Identifier: BSD-2-Clause | |
| -- | |
| module Main where | |
| import CapDL.Parser | |
| import CapDL.DumpParser | |
| import CapDL.PrintUtils | |
| import CapDL.ParserUtils (emptyMaps) | |
| import CapDL.Model | |
| import CapDL.MakeModel | |
| import CapDL.PrintModel | |
| import CapDL.State | |
| import CapDL.PrintDot | |
| import CapDL.PrintXml | |
| import CapDL.PrintIsabelle | |
| import CapDL.PrintC | |
| import CapDL.STCC | |
| import System.Environment | |
| import System.Exit (exitFailure) | |
| import System.FilePath | |
| import System.IO | |
| import System.Posix (rename, removeLink) | |
| import Text.ParserCombinators.Parsec | |
| import Control.Exception (bracketOnError) | |
| import Control.Monad | |
| import Control.Monad.Writer | |
| import Data.Maybe | |
| import System.Console.GetOpt | |
| import Data.String.Utils | |
| import qualified Data.Map as Map | |
| import qualified Data.Yaml as Yaml | |
| import qualified Text.PrettyPrint as PP | |
| data Options = Options { | |
| optOutputIsabelle :: Maybe String, | |
| optOutputXml :: Maybe String, | |
| optOutputDot :: Maybe String, | |
| optOutputCSpec :: Maybe String, | |
| optDynamicAllocCSpec :: Bool, | |
| optOutputText :: Maybe String, | |
| optOutputAnalysis :: Maybe String, | |
| optDumpAST :: Maybe String, | |
| optObjectSizeFile :: Maybe String | |
| } | |
| -- Default options. | |
| defaultOptions :: Options | |
| defaultOptions = Options { | |
| optOutputIsabelle = Nothing, | |
| optOutputXml = Nothing, | |
| optOutputDot = Nothing, | |
| optOutputCSpec = Nothing, | |
| optDynamicAllocCSpec = True, | |
| optOutputText = Nothing, | |
| optOutputAnalysis = Nothing, | |
| optDumpAST = Nothing, | |
| optObjectSizeFile = Nothing | |
| } | |
| -- | |
| -- Options our program supports. | |
| -- | |
| options = [ | |
| Option ['i'] ["isabelle"] | |
| (ReqArg (\arg -> \o -> o {optOutputIsabelle = Just arg }) "FILE") | |
| "output isabelle to FILE", | |
| Option ['d'] ["dot"] | |
| (ReqArg (\arg -> \o -> o {optOutputDot = Just arg }) "FILE") | |
| "output dot to FILE", | |
| Option ['c'] ["code"] | |
| (ReqArg (\arg -> \o -> o {optOutputCSpec = Just arg}) "FILE") | |
| "output C initialiser source to FILE", | |
| Option [] ["code-dynamic-alloc"] | |
| (NoArg (\o -> o {optDynamicAllocCSpec = True})) | |
| "assume dynamic allocation for C initialiser (default)", | |
| Option [] ["code-static-alloc"] | |
| (NoArg (\o -> o {optDynamicAllocCSpec = False})) | |
| "assume static allocation for C initialiser (must have untyped covers)", | |
| Option ['x'] ["xml"] | |
| (ReqArg (\arg -> \o -> o {optOutputXml = Just arg }) "FILE") | |
| "output XML to FILE", | |
| Option ['t'] ["text"] | |
| (ReqArg (\arg -> \o -> o {optOutputText = Just arg }) "FILE") | |
| "output text to FILE", | |
| Option ['a'] ["analysis"] | |
| (ReqArg (\arg o -> o {optOutputAnalysis = Just arg }) "FILE") | |
| "perform analysis and output cap leak and info flow .dot files and capDL text", | |
| Option [] ["dump-ast"] | |
| (ReqArg (\arg o -> o {optDumpAST = Just arg}) "FILE") | |
| "dump internal AST", | |
| Option [] ["object-sizes"] | |
| (ReqArg (\arg o -> o {optObjectSizeFile = Just arg}) "FILE") | |
| "YAML file containing kernel object sizes. Required for --code-dynamic-alloc and --isabelle" | |
| ] | |
| -- | |
| -- Usage information | |
| -- | |
| usageHeader = "usage: parse-capDL [options] <input file>" | |
| -- | |
| -- The result of "getOpt" returns a list of functions that transforms | |
| -- a "Options", returning a new "Options" object with the option applied. This | |
| -- fucnction applies all these generated option functions together. | |
| -- | |
| processOpts :: [Options -> Options] -> Options | |
| processOpts [] = defaultOptions | |
| processOpts (action:actions) = action (processOpts actions) | |
| genparseFromFile :: GenParser Char s a -> s -> String -> IO (Either ParseError a) | |
| genparseFromFile p st fname = do | |
| input <- readFile fname | |
| return $ runParser p st fname input | |
| isDump :: String -> IO Bool | |
| isDump fname = do | |
| input <- openFile fname ReadMode | |
| first <- hGetLine input | |
| hClose input | |
| if strip first == "-- Dump" | |
| then return True | |
| else return False | |
| genObjectSizeMap :: Map.Map String Word -> ObjectSizeMap | |
| genObjectSizeMap m = | |
| Map.fromList [ (koType, sz) | |
| | (n, sz) <- Map.toList m, Just koType <- [Map.lookup n names] ] | |
| where names = Map.fromList | |
| [ ("seL4_Slot", CNode_T) | |
| , ("seL4_TCBObject", TCB_T) | |
| , ("seL4_EndpointObject", Endpoint_T) | |
| , ("seL4_NotificationObject", Notification_T) | |
| , ("seL4_ASID_Pool", ASIDPool_T) | |
| , ("seL4_RTReplyObject", RTReply_T) | |
| , ("seL4_VCPU", VCPU_T) | |
| , ("seL4_PageTableObject", PT_T) | |
| , ("seL4_PageDirectoryObject", PD_T) | |
| , ("seL4_AARCH64_PGD", PGD_T) | |
| , ("seL4_AARCH64_PUD", PUD_T) | |
| , ("seL4_IOPageTableObject", IOPT_T) | |
| , ("seL4_X64_PDPT", PDPT_T) | |
| , ("seL4_X64_PML4", PML4_T) | |
| , ("seL4_SchedContextObject", SC_T) | |
| , ("seL4_IOPorts", IOPorts_T) | |
| , ("seL4_IODevice", IODevice_T) | |
| , ("seL4_ARMIODevice", ARMIODevice_T) | |
| , ("seL4_IRQ", IrqSlot_T) | |
| , ("seL4_IOAPICIRQ", IOAPICIrqSlot_T) | |
| , ("seL4_MSIIRQ", MSIIrqSlot_T) | |
| , ("seL4_ARMIRQ", ARMIrqSlot_T) | |
| , ("seL4_ARMSID", ARMSID_T) | |
| , ("seL4_ARMCB", ARMCB_T) | |
| ] | |
| -- Abort with an error message if 'isFullyAllocated' fails. | |
| assertIsFullyAllocated :: (PP.Doc -> PP.Doc) -> ObjectSizeMap -> ObjMap Word -> CoverMap -> IO () | |
| assertIsFullyAllocated wrapMessage sizeMap objs untypedCovers = | |
| case isFullyAllocated sizeMap objs untypedCovers of | |
| Right () -> return () | |
| Left (msg, badObjs) -> do | |
| hPutStrLn stderr . PP.render . wrapMessage $ | |
| PP.text (msg ++ ":") PP.$+$ | |
| -- TODO: maybe limit number of badObjs printed | |
| PP.nest 2 (PP.vcat $ PP.text . CapDL.PrintUtils.showID <$> badObjs) | |
| exitFailure | |
| main = do | |
| -- Parse command line arguments. | |
| args <- getArgs | |
| let (actions, nonOpts, msgs) = getOpt RequireOrder options args | |
| when (length msgs > 0) $ | |
| error (concat msgs ++ usageInfo usageHeader options) | |
| when (length nonOpts < 1) $ | |
| error ("input file not specified\n" ++ usageInfo usageHeader options) | |
| when (length nonOpts > 1) $ | |
| error ("unrecognised arguments: " ++ unwords nonOpts ++ "\n" ++ usageInfo usageHeader options) | |
| let opt = foldr ($) defaultOptions actions | |
| -- Print option names that satisfy a condition | |
| let gatherOptions = Data.String.Utils.join " and " . map snd . filter fst | |
| let whyNeedObjectSizes = gatherOptions | |
| [ (isJust (optOutputIsabelle opt), "--isabelle") | |
| , (isJust (optOutputCSpec opt) && optDynamicAllocCSpec opt, "--code-dynamic-alloc") ] | |
| when (not (null whyNeedObjectSizes) && isNothing (optObjectSizeFile opt)) $ | |
| error $ "--object-sizes file is required for " ++ whyNeedObjectSizes | |
| -- Parse the file. | |
| let inputFile = nonOpts !! 0 | |
| dump <- isDump inputFile | |
| res <- if dump | |
| then genparseFromFile capDLDumpModule emptyMaps inputFile | |
| else genparseFromFile capDLModule emptyMaps inputFile | |
| -- Parse object sizes file, if available. | |
| objSizeMap <- case optObjectSizeFile opt of | |
| Nothing -> return Map.empty | |
| Just f -> do yParse <- Yaml.decodeFileEither f | |
| case yParse of | |
| Left err -> error $ "failed to parse object sizes file " ++ show f ++ "\n" | |
| ++ show err | |
| Right m -> return $ genObjectSizeMap m | |
| -- Get the parse result (or show an error if it failed). | |
| res <- case res of | |
| Left e -> error (show e) | |
| Right t -> return t | |
| let ((m, i, c), mmLog) = runWriter (makeModel res) | |
| when (not (PP.isEmpty mmLog)) $ hPrint stderr mmLog | |
| -- `--isabelle` requires a statically allocated spec, so check this now. | |
| -- NB: we don't check this for `--code-static-alloc`, because we might not | |
| -- have objSizeMap for that mode. | |
| let whyNeedStaticAlloc = gatherOptions | |
| [ (isJust (optOutputIsabelle opt), "--isabelle") ] | |
| prefix = "A statically allocated spec is required for " ++ whyNeedStaticAlloc | |
| when (not (null whyNeedStaticAlloc)) $ | |
| assertIsFullyAllocated (PP.text prefix PP.$+$) objSizeMap (objects m) (untypedCovers m) | |
| let writeFile' "-" s = putStr s | |
| writeFile' f s = bracketOnError | |
| (do (tempF, handle) <- uncurry openTempFile (splitFileName f) | |
| hClose handle -- ignore for now | |
| return tempF) | |
| removeLink | |
| (\tempF -> do writeFile tempF s | |
| rename tempF f) | |
| let (valid, log) = runWriter (checkModel m) | |
| if valid | |
| then do | |
| -- Output model in any requested format. | |
| let optActions = [(optOutputIsabelle, \f -> writeFile' f $ show $ printIsabelle f objSizeMap m), | |
| (optOutputXml, \f -> writeFile' f $ show $ printXml inputFile m), | |
| (optOutputDot, \f -> writeFile' f $ show $ printDot inputFile m), | |
| (optOutputCSpec, \f -> let allocType | |
| | optDynamicAllocCSpec opt = DynamicAlloc objSizeMap | |
| | otherwise = StaticAlloc | |
| in writeFile' f $ show $ | |
| printC allocType m i c), | |
| (optOutputText, \f -> writeFile' f $ show $ pretty m), | |
| (optOutputAnalysis, \f -> do (leakDot, flowDot, newM) <- leakMatrix m | |
| writeFile (f ++ "-leak.dot") leakDot | |
| writeFile (f ++ "-flow.dot") flowDot | |
| writeFile (f ++ "-saturation.txt") $ show $ pretty newM), | |
| (optDumpAST, \f -> writeFile' f $ show m)] | |
| condDoOpt (projection, action) = maybe (return ()) action (projection opt) | |
| mapM_ condDoOpt optActions | |
| else do | |
| putStr $ show log | |
| error("Failed to check model") |