| -- | |
| -- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) | |
| -- | |
| -- SPDX-License-Identifier: BSD-2-Clause | |
| -- | |
| module CapDL.PrintIsabelle where | |
| import CapDL.Model | |
| import CapDL.State (koType, lookupSizeMap, objSizeBits) | |
| import CapDL.PrintUtils (printAsid) | |
| import Prelude () | |
| import Prelude.Compat | |
| import Text.PrettyPrint | |
| import Numeric (showHex) | |
| import Data.List.Compat | |
| import Data.Ord (comparing) | |
| import Control.Monad (unless) | |
| import Control.Monad.State.Strict (StateT (..)) | |
| import qualified Data.Map as Map | |
| import qualified Data.Set as Set | |
| import Data.Maybe | |
| import Data.Bits | |
| import System.FilePath.Posix | |
| import Text.Regex (mkRegex, matchRegex) | |
| -- This lifts `mapAccumL` over a monad | |
| mapAccumM :: (Monad m, Traversable t) => | |
| (a -> b -> m (a, c)) -> a -> t b -> m (a, t c) | |
| mapAccumM f z xs = swap <$> runStateT (traverse (StateT . f') xs) z | |
| where swap (a, b) = (b, a) | |
| f' x z = swap <$> f z x | |
| lookupElem :: (Eq a) => a -> Map.Map k a -> Maybe k | |
| lookupElem x m = | |
| case find ((==) x . snd) (Map.toList m) of | |
| Just (k, _) -> Just k | |
| Nothing -> Nothing | |
| mapElem :: (Eq a) => a -> Map.Map k a -> Bool | |
| mapElem x m = case lookupElem x m of | |
| Just _ -> True | |
| Nothing -> False | |
| indent = 2 | |
| num n = int (fromIntegral n) | |
| hex :: Word -> String | |
| hex x = "0x" ++ showHex x "" | |
| equiv = text "\\<equiv>" | |
| lambda = text "\\<lambda>" | |
| isaComment x = "\\<comment> \\<open>" ++ x ++ "\\<close>" | |
| {- This mangles hierarchical names into valid Isabelle identifiers: | |
| - we replace '.' by '\'' and check that the result would be valid. -} | |
| mangle :: String -> String | |
| mangle = fixDots . checkValid | |
| where -- Technically, we could support more names, but we don't | |
| -- expect the camkes toolchain to generate them. | |
| nameRE = mkRegex "^[a-zA-Z]([a-zA-Z0-9_.]*[a-zA-Z0-9])?$" | |
| checkValid s = case matchRegex nameRE s of | |
| Just _ -> s | |
| _ -> error $ "can't mangle object name to Isabelle: " ++ show s | |
| fixDots = map (\c -> if c == '.' then '\'' else c) | |
| showID :: ObjID -> String | |
| showID (name, Nothing) = mangle name | |
| showID (name, Just num) = mangle $ name ++ "_" ++ show num | |
| capsName id = showID id ++ "_caps" | |
| constdefs :: String -> String -> Doc | |
| constdefs name typ = | |
| text ("definition " ++ name ++ " :: ") <> doubleQuotes (text typ) <+> | |
| text "where" | |
| {- Prove a set of lemmas. The given proof script is assumed to | |
| - discharge all the proof goals. -} | |
| lemmas :: String -> [String] -> [String] -> Doc | |
| lemmas name statements proof = | |
| text ("lemma " ++ name ++ ": ") $+$ | |
| nest 2 (vcat (map (doubleQuotes . text) statements)) $+$ | |
| nest 2 (vcat (map text proof)) | |
| -- Prove a single lemma. | |
| lemma :: String -> String -> [String] -> Doc | |
| lemma name statement proof = | |
| lemmas name [statement] proof | |
| record :: Doc -> Doc | |
| record p = text "\\<lparr>" <+> p <+> text "\\<rparr>" | |
| printSet :: [Doc] -> Doc | |
| printSet ls = braces $ hsep $ punctuate comma ls | |
| filterEmpty :: [Doc] -> [Doc] | |
| filterEmpty = filter (not . isEmpty) | |
| -- Untypeds are not kernel objects in the Isabelle models. | |
| notUntyped :: KernelObject a -> Bool | |
| notUntyped Untyped{} = False | |
| notUntyped _ = True | |
| {- HACK: fake location for IRQ nodes. | |
| - IRQ CNodes are model-level objects, so we need to invent a physical | |
| - presence for them even if the capDL input doesn't mention them. | |
| - Suitably aligned for 1024 irqs. DSpec probably doesn't care, though. -} | |
| irq_node_paddr__hack :: Word | |
| irq_node_paddr__hack = 0x10000 | |
| {- | |
| - Helper that recovers memory layout from a single untypedCover. | |
| -} | |
| -- Check that we allocate objects consistently with their paddrs. | |
| checkEqPaddr :: KernelObject a -> Word -> Bool | |
| checkEqPaddr obj p = maybe True (p ==) (objPaddr obj) | |
| untypedCoverToPaddrs :: | |
| ObjectSizeMap -> ObjMap Word -> ObjID -> KernelObject Word -> [ObjID] | |
| -> Either (String, [ObjID]) (Map.Map ObjID Word) | |
| untypedCoverToPaddrs sizeMap objs | |
| utID (Untyped { maybePaddr = Just utPaddr, maybeSizeBits = Just utSizeBits }) | |
| cover = | |
| do | |
| let getObject id = | |
| case Map.lookup id objs of | |
| Just o -> return o | |
| _ -> Left ("Object in untyped but not in objects list", [id, utID]) | |
| utSize = 2^utSizeBits | |
| utEnd = utPaddr + utSize | |
| alloc1 addr objID = | |
| do obj <- getObject objID | |
| let objSize = 2^objSizeBits sizeMap obj | |
| unless (checkEqPaddr obj addr) $ | |
| Left ("Object addr doesn't match untyped's current addr (" ++ | |
| hex addr ++ ")", [utID, objID]) | |
| let addr' = addr + objSize | |
| unless (addr `mod` objSize == 0) $ | |
| Left ("Can't place obj at unaligned addr (addr=" ++ | |
| hex addr ++ ", obj size=" ++ | |
| hex objSize ++ ")", [utID, objID]) | |
| unless (addr' <= utEnd) $ | |
| Left ("Can't place obj at addr outside untyped (addr=" ++ | |
| hex addr ++ ", ut end=" ++ hex utEnd ++ ", obj size=" ++ | |
| hex objSize ++ ")", [utID, objID]) | |
| return (addr', (objID, addr)) | |
| Map.fromList . snd <$> mapAccumM alloc1 utPaddr cover | |
| -- unused, or child untyped; no-op | |
| untypedCoverToPaddrs _ _ _ Untyped{} [] = return Map.empty | |
| untypedCoverToPaddrs _ _ utID Untyped{} (:){} = | |
| Left ("Untyped has children but is missing paddr or size", [utID]) | |
| untypedCoverToPaddrs _ _ koID _ _ = | |
| error $ "internal error in untypedCoverToPaddrs: not an untyped: " ++ show koID | |
| {- | |
| - Determine the memory address (i.e. cdl_object_id) for each object. | |
| - This only works for capDL specs that have been pre-allocated, i.e., | |
| - every object belongs to an untypedCover that has a physical address. | |
| -} | |
| getPhysAddrs :: ObjectSizeMap -> ObjMap Word -> CoverMap | |
| -> Either (String, [ObjID]) (Map.Map ObjID Word) | |
| getPhysAddrs objSizeMap objs untypedCovers = | |
| Map.unions <$> | |
| sequence [ | |
| Map.insert utID utPaddr <$> -- add untyped's own addr | |
| untypedCoverToPaddrs objSizeMap objs utID ut cover | |
| | (utID, cover) <- Map.toList untypedCovers, | |
| let ut@Untyped{ maybePaddr = Just utPaddr } = objs Map.! utID ] | |
| {- | |
| - Look up object locations that have been computed by getPhysAddrs. | |
| - Also invent locations for IRQ nodes. | |
| -} | |
| getAddr :: ObjectSizeMap -> Map.Map ObjID Word -> IRQMap -> ObjID -> Word | |
| getAddr objSizeMap objAddrs irqNode id | |
| | Just irq <- lookupElem id irqNode = irq_node_paddr__hack + irq * slotSize | |
| | Just addr <- Map.lookup id objAddrs = addr | |
| | otherwise = error $ "getID: no address for object: " ++ showID id | |
| where slotSize = 2^lookupSizeMap CNode_T objSizeMap | |
| getID :: ObjectSizeMap -> Map.Map ObjID Word -> IRQMap -> ObjID -> Doc | |
| getID objSizeMap objAddrs irqNode id = text $ hex $ getAddr objSizeMap objAddrs irqNode id | |
| printID :: ObjID -> Doc | |
| printID id = text (showID id ++ "_id") | |
| printRight :: Rights -> Doc | |
| printRight = text . show | |
| printRightsList :: [Rights] -> [Doc] | |
| printRightsList [] = [empty] | |
| printRightsList xs = map printRight xs | |
| printRights :: CapRights -> Doc | |
| printRights r = | |
| printSet $ printRightsList $ Set.toList r | |
| printFrameSize :: ObjID -> ObjMap Word -> Doc | |
| printFrameSize id ms = | |
| let Just (Frame sz _ _) = Map.lookup id ms | |
| in num sz | |
| printCoverSet :: ObjMap Word -> Maybe [ObjID] -> Doc | |
| printCoverSet _ Nothing = printSet [] | |
| printCoverSet ms (Just objs) = printSet $ map printID objs' | |
| where objs' = filter (\id -> isJust $ Map.lookup id ms) objs | |
| printMaybeAsid :: Maybe Asid -> Doc | |
| printMaybeAsid Nothing = text "None" | |
| printMaybeAsid (Just asid) = parens $ text "Some" <+> printAsid asid | |
| printReal :: Bool -> Doc | |
| printReal True = text "Real" | |
| printReal False = text "Fake" | |
| printCNodeSize :: ObjMap Word -> ObjID -> Doc | |
| printCNodeSize ms id = | |
| let (CNode _ sz _) = fromJust $ Map.lookup id ms | |
| in num sz | |
| -- FIXME: missing capDL attribute | |
| untypedIsDev :: KernelObject Word -> Bool | |
| untypedIsDev Untyped{} = False -- lies | |
| untypedIsDev obj = error $ "untypedIsDev: got " ++ show (koType obj) | |
| -- The bool represents whether the cap is a real cap; | |
| -- i.e. if it is not in a PT or PD | |
| printCap :: ObjMap Word -> IRQMap -> CoverMap -> Bool -> Cap -> Doc | |
| printCap _ _ _ _ NullCap = text "NullCap" | |
| printCap ms _ _ _ (UntypedCap id) = | |
| text "UntypedCap" <+> text (show $ untypedIsDev (ms Map.! id)) <+> | |
| parens (text "ptr_range" <+> printID id <+> num utSize) <+> | |
| printSet [] -- TODO: check implied free range (or assert ut is empty) | |
| where Just Untyped{ maybeSizeBits = Just utSize } = | |
| Map.lookup id ms | |
| printCap _ _ _ _ (EndpointCap id badge rights) = text "EndpointCap" <+> | |
| printID id <+> num badge <+> printRights rights | |
| printCap _ _ _ _ (NotificationCap id badge rights) = text "NotificationCap" <+> | |
| printID id <+> num badge <+> printRights rights | |
| printCap _ _ _ _ (ReplyCap id) = text "ReplyCap" <+> printID id | |
| printCap _ _ _ _ (MasterReplyCap id) = | |
| text "MasterReplyCap" <+> printID id | |
| printCap ms _ _ _ (CNodeCap id guard gsize) = | |
| text "CNodeCap" <+> printID id <+> num guard <+> num gsize <+> | |
| printCNodeSize ms id | |
| printCap _ _ _ _ (TCBCap id) = text "TcbCap" <+> printID id | |
| printCap _ _ _ _ IRQControlCap = text "IrqControlCap" | |
| printCap _ irqNode _ _ (IRQHandlerCap id) = | |
| text "IrqHandlerCap" <+> num (fromJust (lookupElem id irqNode)) | |
| printCap _ _ _ _ DomainCap = text "DomainCap" | |
| printCap ms _ _ real (FrameCap id rights asid cached _) = text "FrameCap" <+> | |
| -- is_device flag, assumed always false. FIXME: add to model? | |
| text "False" <+> | |
| printID id <+> printRights rights <+> printFrameSize id ms <+> | |
| printReal real <+> printMaybeAsid asid <+> | |
| text (if cached then "" else isaComment "uncached") | |
| printCap _ _ _ real (PTCap id asid) = | |
| text "PageTableCap" <+> printID id <+> printReal real <+> | |
| printMaybeAsid asid | |
| printCap _ _ _ real (PDCap id asid) = | |
| text "PageDirectoryCap" <+> printID id <+> printReal real <+> | |
| printMaybeAsid asid | |
| printCap _ _ _ _ ASIDControlCap = text "AsidControlCap" | |
| printCap ms _ _ _ (ASIDPoolCap id) = | |
| text "AsidPoolCap" <+> printID id <+> asidHigh | |
| -- In capDL, asid_high is a property of the asid_pool (as it should be), | |
| -- but in DSpec it is a property of ASIDPoolCaps. We do the translation here. | |
| where asidHigh = | |
| case Map.lookup id ms of | |
| Just (ASIDPool _ (Just asidHigh)) -> text (hex asidHigh) | |
| _ -> text "undefined" | |
| printCap _ _ _ _ cap = text $ "undefined " ++ isaComment ("unsupported cap: " ++ show cap) | |
| printCapMapping :: ObjMap Word -> IRQMap -> CoverMap -> Bool -> (Word, Cap) -> Doc | |
| printCapMapping ms irqNode covers real (slot, cap) = | |
| num slot <+> text "\\<mapsto>" | |
| <+> text "Types_D." <> printCap ms irqNode covers real cap | |
| printCapMap :: ObjMap Word -> IRQMap -> CoverMap -> Bool -> CapMap Word -> Doc | |
| printCapMap ms irqNode covers real slots = | |
| case map (printCapMapping ms irqNode covers real) (Map.toList slots) of | |
| [] -> text "Map.empty" | |
| xs -> brackets $ vcat $ punctuate comma xs | |
| printCaps' :: ObjMap Word -> ObjID -> IRQMap -> CoverMap -> Bool -> CapMap Word -> Doc | |
| printCaps' ms id irqNode covers real slots = constdefs name "cdl_cap_map" $+$ | |
| doubleQuotes (text name <+> equiv <+> printCapMap ms irqNode covers real slots) | |
| where name = capsName id | |
| printCaps :: ObjMap Word -> ObjID -> IRQMap -> CoverMap -> KernelObject Word -> Doc | |
| printCaps ms id irqNode covers (PT slots) = | |
| printCaps' ms id irqNode covers False slots $+$ text "" | |
| printCaps ms id irqNode covers (PD slots) = | |
| printCaps' ms id irqNode covers False slots $+$ text "" | |
| printCaps ms id irqNode covers (ASIDPool slots _) = | |
| printCaps' ms id irqNode covers False slots $+$ text "" | |
| printCaps ms id irqNode covers obj | |
| | hasSlots obj = printCaps' ms id irqNode covers True (slots obj) $+$ text "" | |
| | otherwise = empty | |
| getAddress' :: ObjMap Word -> [Cap] -> Word -> Cap -> (Word, Cap) -> Maybe Word | |
| getAddress' ms seen current_word goal_cap (slot, cap) = | |
| getAddress ms seen (current_word + slot) goal_cap cap | |
| getAddress :: ObjMap Word -> [Cap] -> Word -> Cap -> Cap -> Maybe Word | |
| getAddress ms seen current_word goal_cap cap@(CNodeCap objID guard gsz) | |
| | cap `elem` seen = Nothing | |
| | otherwise = | |
| let (CNode slots sz _) = fromJust $ Map.lookup objID ms | |
| radix_sz = fromIntegral sz | |
| level_sz = fromIntegral $ gsz + sz | |
| new_word = shift current_word level_sz + shift guard radix_sz | |
| in case lookupElem goal_cap slots of | |
| Just slot -> Just (new_word + slot) | |
| Nothing -> listToMaybe $ mapMaybe | |
| (getAddress' ms (cap:seen) new_word goal_cap) | |
| (Map.toList slots) | |
| getAddress _ _ _ _ _ = Nothing | |
| hasFaultEndpoint :: Maybe Word -> String | |
| hasFaultEndpoint fault = | |
| case fault of | |
| Just _ -> "True" | |
| Nothing -> "False" | |
| printObjID :: ObjectSizeMap -> Map.Map ObjID Word -> IRQMap -> (ObjID, KernelObject Word) -> Doc | |
| printObjID objSizeMap objAddrs irqNode (id, _) = | |
| constdefs name "cdl_object_id" $+$ | |
| doubleQuotes (printID id <+> equiv <+> obj_id) | |
| $+$ text "" | |
| where name = showID id ++ "_id" | |
| obj_id = getID objSizeMap objAddrs irqNode id | |
| printObjIDs :: ObjectSizeMap -> Map.Map ObjID Word -> ObjMap Word -> IRQMap -> Doc | |
| printObjIDs objSizeMap objAddrs ms irqs = | |
| vcat (map (printObjID objSizeMap objAddrs irqs) (Map.toList ms)) | |
| $+$ text "" | |
| printObj' :: ObjMap Word -> ObjID -> KernelObject Word -> Doc | |
| printObj' _ _ Endpoint = text "Endpoint" | |
| printObj' _ _ Notification = text "Notification" | |
| printObj' _ id (TCB _ fault _ dom _) = text "Tcb" <+> | |
| record (fsep $ punctuate comma $ map text | |
| ["cdl_tcb_caps = " ++ capsName id, | |
| "cdl_tcb_fault_endpoint = " ++ maybe "0" show fault, | |
| "cdl_tcb_intent = undefined", | |
| "cdl_tcb_has_fault = " ++ hasFaultEndpoint fault, | |
| "cdl_tcb_domain = " ++ show dom]) | |
| printObj' _ id (CNode _ bits _) = text "CNode" <+> | |
| record (fsep $ punctuate comma $ map text | |
| ["cdl_cnode_caps = " ++ capsName id, | |
| "cdl_cnode_size_bits = " ++ show bits]) | |
| printObj' _ id (ASIDPool _ _) = text "AsidPool" <+> | |
| record (fsep $ punctuate comma $ map text | |
| ["cdl_asid_pool_caps = " ++ capsName id]) | |
| printObj' _ id (PT _) = text "PageTable" <+> | |
| record (fsep $ punctuate comma $ map text | |
| ["cdl_page_table_caps = " ++ capsName id]) | |
| printObj' _ id (PD _) = text "PageDirectory" <+> | |
| record (fsep $ punctuate comma $ map text | |
| ["cdl_page_directory_caps = " ++ capsName id]) | |
| printObj' _ _ (Frame vmSzBits _ _) = text "Frame" <+> | |
| record (fsep $ punctuate comma $ map text | |
| ["cdl_frame_size_bits = " ++ show vmSzBits]) | |
| printObj' _ _ obj = text $ "undefined " ++ isaComment ("unsupported obj: " ++ show obj) | |
| printLemmaObjectSlots :: ObjID -> Doc | |
| printLemmaObjectSlots id = | |
| lemma (objName++"_object_slots") | |
| ("object_slots "++objName++" = "++slots) | |
| ["by (simp add: "++objName++"_def object_slots_def)"] | |
| where objName = showID id | |
| slots = capsName id | |
| printObj :: ObjMap Word -> IRQMap -> CoverMap -> (ObjID, KernelObject Word) -> Doc | |
| printObj ms irqNode covers (id, obj) = printCaps ms id irqNode covers obj $+$ | |
| constdefs name "cdl_object" $+$ | |
| doubleQuotes (text name <+> equiv <+> text "Types_D." <> printObj' ms id obj) | |
| $+$ text "" $+$ | |
| (if hasSlots obj then printLemmaObjectSlots id $+$ text "" else text "") | |
| where name = showID id | |
| printObjs :: ObjMap Word -> IRQMap -> CoverMap -> [(ObjID, KernelObject Word)] -> Doc | |
| printObjs ms irqNode covers isaCdlObjects = | |
| vcat (map (printObj ms irqNode covers) isaCdlObjects) | |
| printObjMapping :: (ObjID, KernelObject Word) -> Doc | |
| printObjMapping (id, _) = printID id <+> text ("\\<mapsto> " ++ showID id) | |
| printObjMap :: ObjMap Word -> [(ObjID, KernelObject Word)] -> Doc | |
| printObjMap _ isaCdlObjects = | |
| case map printObjMapping isaCdlObjects of | |
| [] -> text "Map.empty" | |
| xs -> brackets $ fsep $ punctuate comma xs | |
| -- Map of all objects. We use the FastMap builder for scalability. | |
| printObjects :: [(ObjID, KernelObject Word)] -> Doc | |
| printObjects isaCdlObjects = | |
| text "local_setup {*" $+$ | |
| text "FastMap.define_map (FastMap.name_opts_default \"objects\")" $+$ | |
| nest 2 ( | |
| nest 2 (brackets (vcat $ punctuate comma $ map binding isaCdlObjects)) $+$ | |
| text "@{term \"id :: cdl_object_id \\<Rightarrow> cdl_object_id\"}" $+$ | |
| text "@{thms ids}" $+$ | |
| text "false" | |
| ) $+$ | |
| text "*}" | |
| where binding (id, _) = text $ "(@{term \"" ++ showID id ++ "_id\"}, " ++ | |
| "@{term \"" ++ showID id ++ "\"})" | |
| printIrqMapping :: (Word, Doc) -> Doc | |
| printIrqMapping (irqID, id) = | |
| text (hex irqID) <+> text ":=" <+> id | |
| {- The capDL formal model doesn't use a partial mapping for | |
| - irqs, which is nonsensical: no platform has all possible | |
| - "cdl_irq" values. This is a bug to be fixed. | |
| - For now, we just use "undefined" as the default mapping, and | |
| - add IRQs from our input model on top of that. | |
| -} | |
| -- Map each known IRQ to its IRQ node address. | |
| printIRQsMap :: ObjMap Word -> IRQMap -> Doc | |
| printIRQsMap _ irqNode = | |
| let irqs = Map.map printID irqNode | |
| irqMap = parens $ fsep $ punctuate comma $ map printIrqMapping $ | |
| Map.toList irqs | |
| baseIrqs = text "undefined" | |
| allIrqs | Map.null irqs = baseIrqs -- irqMap would be "()" | |
| | otherwise = baseIrqs <+> irqMap | |
| in allIrqs | |
| printIRQs :: ObjMap Word -> IRQMap -> Doc | |
| printIRQs ms irqNode = | |
| constdefs "irqs" "cdl_irq \\<Rightarrow> cdl_object_id" $+$ | |
| doubleQuotes (text "irqs" <+> equiv <+> printIRQsMap ms irqNode) | |
| makeASIDTable :: ObjMap Word -> CapMap Word | |
| makeASIDTable ms = foldl' addToASIDTable Map.empty (Map.toList ms) | |
| where addToASIDTable asidTable (objID, ASIDPool _ (Just asidHigh)) = | |
| Map.insert asidHigh (ASIDPoolCap objID) asidTable | |
| addToASIDTable asidTable _ = asidTable | |
| printASIDTable :: ObjMap Word -> IRQMap -> CoverMap -> Doc | |
| printASIDTable ms irqs covers = | |
| constdefs "asid_table" "cdl_cap_map" $+$ | |
| doubleQuotes (text "asid_table" <+> equiv <+> | |
| printCapMap ms irqs covers False (makeASIDTable ms)) | |
| printCapRef :: CapRef -> Doc | |
| printCapRef (obj, slot) = parens $ printID obj <> comma <+> num slot | |
| printCDTMapping :: (CapRef, CapRef) -> Doc | |
| printCDTMapping (parent, child) = | |
| printCapRef parent <+> text "\\<mapsto>" <+> printCapRef child | |
| printCDTMap :: CDT -> Doc | |
| printCDTMap cdt = | |
| case map printCDTMapping (Map.toList cdt) of | |
| [] -> text "Map.empty" | |
| xs -> brackets $ fsep $ punctuate comma xs | |
| printCDT :: CDT -> Doc | |
| printCDT cdt = constdefs "cdt" "cdl_cdt" $+$ | |
| doubleQuotes (text "cdt" <+> equiv <+> printCDTMap cdt) | |
| printCDLState :: Arch -> Doc | |
| printCDLState arch = | |
| record $ fsep $ punctuate comma $ map text ["cdl_arch = " ++ show arch, | |
| "cdl_objects = objects", "cdl_cdt = cdt", | |
| "cdl_current_thread = undefined", "cdl_irq_node = irqs", | |
| "cdl_asid_table = asid_table", "cdl_current_domain = undefined"] | |
| printSimps :: ObjMap Word -> [(ObjID, KernelObject Word)] -> Doc | |
| printSimps ms isaCdlObjects = | |
| text "lemmas ids = " $+$ vcat (map objIDDef $ Map.toList ms) $+$ text "" $+$ | |
| text "lemmas cap_defs = " $+$ vcat (map capsDef objsWithCaps) $+$ text "" $+$ | |
| text "lemmas obj_defs = " $+$ vcat (map objDef isaCdlObjects) $+$ text "" | |
| where objIDDef (id, _) = printID id <> text "_def" | |
| capsDef (id, _) = text (capsName id) <> text "_def" | |
| objDef (id, _) = text (showID id) <> text "_def" | |
| objsWithCaps = filter (\(_, obj) -> hasSlots obj) isaCdlObjects | |
| printState :: Arch -> Doc | |
| printState arch = constdefs "state" "cdl_state" $+$ | |
| doubleQuotes (text "state" <+> equiv <+> printCDLState arch) | |
| printFileName :: String -> Doc | |
| printFileName file = text $ dropExtension $ takeFileName file | |
| printHeader :: String -> Doc | |
| printHeader name = | |
| text "theory" <+> doubleQuotes (printFileName name) $+$ text "imports" $+$ | |
| nest 2 (text "\"DSpec.Types_D\"" $+$ | |
| text "\"Lib.FastMap\"" $+$ | |
| text ("\"DPolicy.Dpolicy\" " ++ isaComment "@{const ptr_range}")) $+$ | |
| text "begin" | |
| printFooter :: Doc | |
| printFooter = text "end" | |
| printIsabelle :: String -> ObjectSizeMap -> Model Word -> Doc | |
| printIsabelle name objSizeMap (Model (arch@ARM11) ms irqNode cdt untypedCovers) = | |
| printHeader name $+$ text "" $+$ | |
| printObjIDs objSizeMap objAddrs ms irqNode $+$ | |
| printObjs ms irqNode untypedCovers isaCdlObjects $+$ | |
| text "" $+$ | |
| printSimps ms isaCdlObjects $+$ text "" $+$ | |
| printObjects isaCdlObjects $+$ text "" $+$ | |
| printIRQs ms irqNode $+$ text "" $+$ | |
| printASIDTable ms irqNode untypedCovers $+$ text "" $+$ | |
| printCDT cdt $+$ text "" $+$ | |
| printState arch $+$ text "" $+$ | |
| printFooter | |
| where objAddrs = case getPhysAddrs objSizeMap ms untypedCovers of | |
| Left (msg, ids) -> | |
| error $ "Failed to allocate objects from untypeds: " ++ | |
| msg ++ " (" ++ intercalate ", " (map show ids) ++ ")" | |
| Right x -> x | |
| getAddr' = getAddr objSizeMap objAddrs irqNode | |
| -- Isabelle capDL objects. These are sorted by id because the | |
| -- FastMap builder expects a sorted list as input. | |
| isaCdlObjects = sortBy (comparing $ getAddr' . fst) $ | |
| filter (notUntyped . snd) $ | |
| Map.toList ms | |
| printIsabelle _ _ _ = | |
| error "Currently only the ARM11 architecture is supported when parsing to Isabelle" |