1%include polycode.fmt 2 3%if false 4 Error: DSL for error definition 5 6 Copyright (c) 2009 ETH Zurich. 7 All rights reserved. 8 9 This file is distributed under the terms in the attached LICENSE file. 10 If you do not find this file, copies can be found by writing to: 11 ETH Zurich D-INFK, Haldeneggsteig 4, CH-8092 Zurich. Attn: Systems Group. 12%endif 13 14%if false 15 16> {-# OPTIONS_GHC -XBangPatterns #-} 17 18%endif 19 20%if false 21 22> module HamletBackend where 23 24> import Data.Maybe 25> import Data.List 26> import Data.Char 27> import qualified Data.Map as Map 28 29> import Debug.Trace 30 31> import Semantics 32> import Constructs 33> import PureExpressions 34> import Expressions 35 36> import Constructs.Conditionals 37> import Constructs.References 38> import Constructs.Functions 39> import Constructs.Enumerations 40> import Constructs.Structures 41> import Constructs.Unions 42 43> import Libc.Assert 44 45> import Libbarrelfish.HasDescendants 46> import Libbarrelfish.MemToPhys 47> import qualified Libbarrelfish.GetAddress as H (get_address) 48 49> import HamletAst 50 51%endif 52 53 54> strict x = x 55 56 57> boolT :: TypeExpr 58> boolT = typedef uint64T "bool" 59> 60> false :: PureExpr 61> false = uint64 $ 0 62> 63> true :: PureExpr 64> true = uint64 $ 1 65 66> objtypeT :: TypeExpr 67> objtypeT = typedef uint64T "enum objtype" 68 69> ctePtrT :: TypeExpr 70> ctePtrT = typedef uint64T "struct cte *" 71 72> lvaddrT :: TypeExpr 73> lvaddrT = typedef uint64T "lvaddr_t" 74 75> genpaddrT :: TypeExpr 76> genpaddrT = typedef uint64T "genpaddr_t" 77 78> gensizeT :: TypeExpr 79> gensizeT = typedef uint64T "gensize_t" 80 81> getCap cap_pp = (readRef cap_pp >>= readRef) 82 83> lower = map toLower 84 85\section{|Objtype| Enumeration} 86 87> ofObjTypeEnum :: CapName -> PureExpr 88> ofObjTypeEnum (CapName x) = CLRef Global uint64T (Provided ("ObjType_" ++ x)) 89 90 91> mkObjTypeEnum :: [Capability] -> Enumeration 92> mkObjTypeEnum caps = enums `seq` objTypeNum `seq` 93> objTypeNum : enums 94> where (n,enums) = foldl' mkEnumField (0,[]) caps 95> mkEnumField (!i,!acc) !cap = i' `seq` 96> (i',acc' ) 97> where CapName capName = name cap 98> strName = "ObjType_" ++ capName 99> acc' = strName `seq` (strName, i) : acc 100> i' = i + 1 101> objTypeNum = ("ObjType_Num",n) 102 103> mkObjDefineList :: [Define] -> [(String, Int)] 104> mkObjDefineList defs = map (\(s, i) -> (map toUpper s, i)) $ mkDefineList defs 105 106\section{Capabality Structure} 107 108> capRightsT :: TypeExpr 109> capRightsT = typedef uint8T "CapRights" 110 111 112> capNameOf :: Capability -> String 113> capNameOf cap = capName 114> where CapName capName = name cap 115 116> mkCapsStruct :: Capabilities -> TFieldList 117> mkCapsStruct caps = strict 118> [("u", capUnionT), 119> ("type", objtypeT), 120> ("rights", capRightsT)] 121> where capUnionT = unionST "capability_u" ((map (\cap -> (lower $ capNameOf cap, mkCapStructT cap)) 122> (capabilities caps)) ) 123> -- XXX: Why do I need to define types here when they are already 124> -- defined somewhere else? Also as hamlet doesn't handle uintptr_t, 125> -- lvaddr is defined as uint64 although that is not always the case. 126> -- Using a type not defined here will generate "type"* 127> -- which is obviously broken. -Akhi 128> mkCapStructT cap = structST (capNameOf cap) (map mkCapField (fields cap)) 129> mkCapField (CapField typ (NameField name)) = (name, toFofType typ) 130> toFofType UInt8 = uint8T 131> toFofType UInt16 = uint16T 132> toFofType UInt32 = uint32T 133> toFofType UInt64 = uint64T 134> toFofType Int = int32T 135> toFofType GenPAddr = typedef uint64T "genpaddr_t" 136> toFofType GenSize = typedef uint64T "gensize_t" 137> toFofType LPAddr = typedef uint64T "lpaddr_t" 138> toFofType GenVAddr = typedef uint64T "genvaddr_t" 139> toFofType LVAddr = typedef uint64T "lvaddr_t" 140> toFofType CAddr = typedef uint32T "capaddr_t" 141> toFofType (Pointer s) = typedef uint64T (s ++ "*") 142> toFofType CapRights = capRightsT 143> toFofType CoreId = typedef uint8T "coreid_t" 144> toFofType PasId = typedef uint32T "pasid_t" 145 146> capsStructT :: Capabilities -> TypeExpr 147> capsStructT cap = structST "capability" (mkCapsStruct cap) 148 149\section{Get address and size} 150 151\subsection{Convert common expressions} 152 153Generate an expression for the size of a value expressed in "bits" 154i.e. {\tt (((gensize\_t)1) << bits)} 155 156> mkSize :: PureExpr -> PureExpr 157> mkSize bits = (cast gensizeT (uint64 1)) .<<. bits 158 159> readCapAttr :: PureExpr -> String -> FoFCode PureExpr 160> readCapAttr cap attr = getCap cap >>= (\c -> readStruct c attr) 161 162Try and look up a name in a definitions and failing that generated code to look 163it up in the fields of a cap. 164 165> lookupName :: [(String, Int)] -> PureExpr -> String -> String -> FoFCode PureExpr 166> lookupName defs cap capType name = 167> case (name `lookup` defs) of 168> Nothing -> do 169> capU <- readCapAttr cap "u" 170> capCStruct <- readUnion capU $ lower $ capType 171> readStruct capCStruct name 172> Just val -> return $ uint64 $ toInteger val 173 174Generate code to calculate the result of an expression. 175 176> exprCode :: [(String, Int)] -> PureExpr -> String -> Expr -> FoFCode PureExpr 177> exprCode defs cap capType (NameExpr n) = lookupName defs cap capType n 178> exprCode defs cap capType (AddExpr left right) = 179> do 180> lval <- lookupName defs cap capType left 181> rval <- lookupName defs cap capType right 182> return (lval .+. rval) 183 184Generate code to calculate the "address" property of a cap. 185 186> addressExprCode :: [(String, Int)] -> PureExpr -> String -> AddressExpr -> FoFCode PureExpr 187> addressExprCode defs cap capType (MemToPhysOp expr) = 188> do 189> lval <- exprCode defs cap capType expr 190> mem_to_phys $ cast lvaddrT lval 191> addressExprCode defs cap capType (GetAddrOp expr) = 192> do 193> lval <- exprCode defs cap capType expr 194> H.get_address $ lval 195> addressExprCode defs cap capType (AddressExpr expr) = 196> exprCode defs cap capType expr 197 198Generate code to calculate the "size" property of a cap. 199 200> sizeExprCode :: [(String, Int)] -> PureExpr -> String -> SizeExpr -> FoFCode PureExpr 201> sizeExprCode defs cap capType (ZeroSize) = return $ uint64 0 202> sizeExprCode defs cap capType (SizeExpr expr) = exprCode defs cap capType expr 203> sizeExprCode defs cap capType (SizeBitsExpr expr) = 204> do 205> bitsExpr <- exprCode defs cap capType expr 206> return $ mkSize $ bitsExpr 207 208\subsection{get\_address} 209 210> get_address :: Capabilities -> FoFCode PureExpr 211> get_address caps = 212> def [] "get_address" 213> (mkGetPropSwitch caps mkGetAddr) 214> genpaddrT 215> [(ptrT $ ptrT $ capsStructT caps, Just "cap")] 216> where 217> nullptr = cast genpaddrT $ uint64 0 218> mkGetAddr :: [(String, Int)] -> Capability -> PureExpr -> FoFCode PureExpr 219> mkGetAddr defines capType cap = 220> case rangeExpr capType of 221> Just expr -> mkGetAddrExpr defines capType cap $ fst expr 222> Nothing -> returnc nullptr 223> mkGetAddrExpr defines capType cap expr = 224> do 225> res <- addressExprCode defines cap capName expr 226> returnc res 227> where 228> capName = case name capType of (CapName s) -> s 229 230\subsection{get\_size} 231 232> get_size :: Capabilities -> FoFCode PureExpr 233> get_size caps = 234> def [] "get_size" 235> (mkGetPropSwitch caps mkGetSize) 236> gensizeT 237> [(ptrT $ ptrT $ capsStructT caps, Just "cap")] 238> where 239> mkGetSize :: [(String, Int)] -> Capability -> PureExpr -> FoFCode PureExpr 240> mkGetSize defines capType cap = 241> case rangeExpr capType of 242> Just expr -> mkGetSizeExpr defines capType cap $ snd expr 243> Nothing -> returnc $ cast gensizeT $ uint64 0 244> mkGetSizeExpr defines capType cap expr = 245> do 246> res <- sizeExprCode defines cap capName expr 247> returnc res 248> where 249> capName = case name capType of (CapName s) -> s 250 251\subsection{Generate switch on enum objtype} 252 253\verb|mkGetPropSwitch| generates a switch statement that switches on the 254objtype of the cap argument and uses mkGetProp to generate code for the 255different cases. 256 257> mkGetPropSwitch :: Capabilities 258> -> ([(String, Int)] -> Capability -> PureExpr -> FoFCode PureExpr) 259> -> ([PureExpr] -> FoFCode PureExpr) 260> mkGetPropSwitch caps mkGetProp = get_prop_int 261> where 262> get_prop_int :: [PureExpr] -> FoFCode PureExpr 263> get_prop_int (cap : []) = 264> do 265> let cases = map (mkGetPropCase cap) (capabilities caps) 266> capTypeInt <- readCapAttr cap "type" 267> switch capTypeInt cases ((assert false) >> (returnc $ uint64 0)) 268> mkGetPropCase cap capType = 269> ((ofObjTypeEnum $ name capType), mkGetProp defineList capType cap) 270> defineList = mkDefineList $ defines caps 271 272\section{Compare} 273 274$get\_type\_root$ gets a number indicating which tree root of the type forest a 275given type belongs to. 276 277> get_type_root :: Capabilities -> FoFCode PureExpr 278> get_type_root caps = 279> def [] "get_type_root" 280> get_type_root_int 281> uint8T 282> [(objtypeT, Just "type")] 283> where 284> get_type_root_int [typ] = 285> -- big switch over all types, each just returns the result 286> switch typ cases (assert false >> returnc false) 287> cases = map (mkCase . name) $ capTypes 288> mkCase capName = (ofObjTypeEnum capName, mkGetRoot capName) 289> -- case body just returns the calculated number 290> mkGetRoot capName = returnc $ uint8 $ fromIntegral $ fromJust $ elemIndex (typeRoot capName) rootTypeNames 291> capTypes = capabilities caps 292> -- cap name -> cap lookup list 293> capTypesLookup = map (\c -> (name c, c)) capTypes 294> -- list of names of root types. the index in this list is the final 295> -- root index 296> rootTypeNames = map name $ filter (isNothing . from) capTypes 297> typeRoot capName = 298> -- recursively walk up retype relations 299> case from $ fromJust $ lookup capName capTypesLookup of 300> Just n -> typeRoot n 301> Nothing -> capName 302 303$compare\_caps$ returns -1, 0 or 1 indicating the ordering of the given caps. 304 305\texttt{compare\_caps(left, right) $op$ 0} implies \texttt{left $op$ right}, where op is a numerical comparison. 306 307> compare_caps :: Capabilities -> 308> PureExpr -> 309> PureExpr -> 310> PureExpr -> 311> FoFCode PureExpr 312> compare_caps caps get_type_root get_address get_size = 313> def [] "compare_caps" 314> (compare_caps_int caps get_type_root get_address get_size) 315> int8T 316> [(ptrT $ ptrT $ capsStructT caps, Just "left"), 317> (ptrT $ ptrT $ capsStructT caps, Just "right"), 318> (boolT, Just "tiebreak")] 319 320> compare_caps_int :: Capabilities -> 321> PureExpr -> 322> PureExpr -> 323> PureExpr -> 324> [PureExpr] -> 325> FoFCode PureExpr 326> compare_caps_int caps get_type_root get_address get_size 327> [left_cap_pp, right_cap_pp, tiebreak] = 328> do 329> leftCap <- getCap left_cap_pp 330> rightCap <- getCap right_cap_pp 331> leftType <- readStruct leftCap "type" 332> rightType <- readStruct rightCap "type" 333> -- perform a bunch of global tests 334> sequence $ map (doCmp left_cap_pp leftCap leftType 335> right_cap_pp rightCap rightType) tests 336> -- at this point we know the caps are the same type 337> -- also, they are at the same address and have the same size 338> -- if the cap type has additional "eq" attributes, we now compare those 339> let haveEqCaps = filter (not . null . eqFields) $ capabilities caps 340> mkCase capType = ((ofObjTypeEnum $ name capType), 341> (mkEqCmp leftCap rightCap capType)) 342> eqCases = map mkCase haveEqCaps 343> switch leftType eqCases (return false) 344> -- finally, if the tie break param is true we compare the pointers 345> ifc (return tiebreak) (mkCmp left_cap_pp right_cap_pp (.<.)) (return false) 346> returnc $ int8 0 347> where 348> 349> -- type-independent tests 350> -- Note the reversed ordering on the capability size: Ordering 351> -- capabilities by descending size makes parents that have the same 352> -- starting address as their children appear before those children in 353> -- the order. 354> tests = [(getRoot, (.<.)), 355> (getAddr, (.<.)), 356> (getSize, (.>.)), 357> (getType, (.<.))] 358> getRoot cpp c ct = call get_type_root [ct] 359> getAddr cpp c ct = call get_address [cpp] 360> getSize cpp c ct = call get_size [cpp] 361> getType cpp c ct = return ct 362> 363> -- comparison code generators 364> mkCmp left right op = 365> ifc (return (left .!=. right)) 366> (returnc $ test (left `op` right) (int8 (-1)) (int8 1)) 367> (return false) 368> doCmp lcpp lc lct rcpp rc rct (f, op) = 369> do 370> l <- f lcpp lc lct 371> r <- f rcpp rc rct 372> mkCmp l r op 373> mkEqCmp leftCap rightCap capType = 374> do 375> let eqs = map (\(NameField n) -> n) $ eqFields capType 376> leftCapU <- readStruct leftCap "u" 377> rightCapU <- readStruct rightCap "u" 378> let capName = case name capType of CapName n -> n 379> leftCapS <- readUnion leftCapU $ lower capName 380> rightCapS <- readUnion rightCapU $ lower capName 381> sequence $ map (doFieldCmp leftCapS rightCapS) eqs 382> return false 383> doFieldCmp lc rc n = 384> do 385> l <- readStruct lc n 386> r <- readStruct rc n 387> mkCmp l r (.<.) 388 389\section{Is well founded} 390 391\subsection{Compute Well-found-ness Relation} 392 393{\tt is\_well\_founded} checks if {\tt src\_type} can be retyped to {\tt 394dest\_type}. 395 396> is_well_founded :: [Capability] -> 397> FoFCode PureExpr 398> is_well_founded caps = 399> def [] "is_well_founded" 400> (is_well_founded_int caps) 401> boolT 402> [(objtypeT, Just "src_type"), 403> (objtypeT, Just "dest_type")] 404 405> is_well_founded_int caps (src_type : dest_type : []) = 406> do 407> switch dest_type cases (returnc false) 408> where 409> cases = map mkCase $ filter (\c -> (isJust $ from c) || (fromSelf c)) caps 410> mkCase capType = ((ofObjTypeEnum $ name capType), (checkIsParent src_type capType)) 411> checkIsParent parent capType = returnc ((checkIsFrom parent capType) .|. (checkIsFromSelf parent capType)) 412> checkIsFrom parent capType = 413> case from capType of 414> Just capName -> (parent .==. (ofObjTypeEnum capName)) 415> Nothing -> false 416> checkIsFromSelf parent capType = 417> if fromSelf capType 418> then (parent .==. (ofObjTypeEnum $ name capType)) 419> else false 420 421> is_equal_types :: FoFCode PureExpr 422> is_equal_types = 423> def [] "is_equal_type" 424> is_equal_int 425> boolT 426> [(objtypeT, Just "left_type"), 427> (objtypeT, Just "right_type")] 428> where is_equal_int (src_type : dest_type : []) = 429> do returnc (src_type .==. dest_type) 430 431\section{Is revoked first} 432 433This function queries if the given capability can be retyped in its current 434state. 435 436\subsection{Compute Revocation Paths} 437 438\verb|revokePaths| indicates for all capability types if the type 439can be retyped multiple times. 440 441> revokePaths :: [Capability] -> 442> [(PureExpr, Maybe Bool)] 443> revokePaths caps = map revokePath caps 444> where revokePath cap = strict ( ofObjTypeEnum $ name cap, multiRet cap) 445> multiRet cap = if null (getChildren cap caps) then Nothing else Just $ multiRetype cap 446> -- this returns a list of children in the type order for the capability `cap'. 447> getChildren cap capabilities = 448> [ c | c <- capabilities, isChild c cap ] ++ 449> (if fromSelf cap then [cap] else []) 450> isChild c p = if isJust (from c) then name p == (fromJust $ from c) else False 451 452\subsection{Generate Code} 453 454> is_revoked_first :: [Capability] -> 455> FoFCode PureExpr 456> is_revoked_first caps = 457> def [] 458> "is_revoked_first" 459> (is_revoked_first_int caps) 460> boolT 461> [(ctePtrT, Just "src_cte"), 462> (objtypeT, Just "src_type")] 463 464> is_revoked_first_int :: [Capability] -> 465> [PureExpr] -> 466> FoFCode PureExpr 467> is_revoked_first_int caps (src_cte : src_type : []) = 468> do 469> let cases = map (mkRevokeCase src_cte) revokeP 470> switch src_type 471> cases 472> (do 473> returnc false) 474> -- revokeP contains all cap types that can be retyped 475> where revokeP = [(st, fromJust rp) | (st, rp) <- revokePaths caps, isJust rp] 476> mkRevokeCase cte (rType, mult) = (rType, caseCode cte mult) 477> -- return true if type of cte is multi-retypable or cte has no descendants, 478> -- else false 479> caseCode cte mult = do if mult then returnc true 480> else do b <- has_descendants cte 481> ifc (return b) 482> (returnc false) 483> (returnc true) 484 485\section{Is copy} 486 487Check whether two capabilities represent the same object. This is different 488from \texttt{compare\_caps(left, right, false) == 0} in that it respects 489general equality specifiers like \texttt{is\_always\_copy} and 490\texttt{is\_never\_copy}. 491 492> is_copy :: Capabilities -> 493> PureExpr -> 494> FoFCode PureExpr 495> is_copy caps compare_caps = 496> def [] 497> "is_copy" 498> (is_copy_int caps compare_caps) 499> boolT 500> [(ptrT $ ptrT thisCapsStructT, Just "left"), 501> (ptrT $ ptrT thisCapsStructT, Just "right")] 502> where thisCapsStructT = capsStructT caps 503 504> is_copy_int :: Capabilities -> 505> PureExpr -> 506> [PureExpr] -> 507> FoFCode PureExpr 508> is_copy_int caps compare_caps (leftPP : rightPP : []) = 509> do 510> -- compare types 511> leftCap <- getCap leftPP 512> rightCap <- getCap rightPP 513> leftType <- readStruct leftCap "type" 514> rightType <- readStruct rightCap "type" 515> ifc (return (leftType .!=. rightType)) 516> (returnc false) (return false) 517> -- we now have equal types, check general equality for the type 518> switch leftType generalEqCases (return false) 519> -- don't have general equality, call compare_caps with tiebreak = false 520> res <- call compare_caps [leftPP, rightPP, false] 521> returnc (res .==. (int8 0)) 522> where 523> -- in general equality switch, only handle cases with such an equality 524> generalEqCases = map mkGeqCase $ 525> filter (isJust . generalEquality) $ 526> capabilities caps 527> -- case body: just return the value of the equality 528> mkGeqCase capType = ((ofObjTypeEnum $ name capType), 529> (returnc $ fofBool $ fromJust $ generalEquality capType)) 530> fofBool b = if b then true else false 531 532\section{Is Ancestor} 533 534{\tt is\_ancestor} checks if one cap is an immediate ancestor of another (note: 535if ancestor and child are of the same type, a non-immediate ancestor will also 536count). 537 538> is_ancestor :: Capabilities -> 539> PureExpr -> 540> PureExpr -> 541> PureExpr -> 542> FoFCode PureExpr 543> is_ancestor caps is_well_founded get_address get_size = 544> def [] 545> "is_ancestor" 546> (is_ancestor_int caps is_well_founded get_address get_size) 547> boolT 548> [(ptrT $ ptrT thisCapsStructT, Just "child"), 549> (ptrT $ ptrT thisCapsStructT, Just "parent")] 550> where thisCapsStructT = capsStructT caps 551 552> is_ancestor_int :: Capabilities -> 553> PureExpr -> 554> PureExpr -> 555> PureExpr -> 556> [PureExpr] -> 557> FoFCode PureExpr 558> is_ancestor_int caps is_well_founded get_address get_size (childPP : parentPP : []) = 559> do 560> child <- getCap childPP 561> parent <- getCap parentPP 562> childType <- readStruct child "type" 563> parentType <- readStruct parent "type" 564> 565> -- fail if relationship is not "well founded" 566> wellFounded <- call is_well_founded [parentType, childType] 567> ifc (return $ neg $ wellFounded) 568> (returnc false) (return void) 569> 570> -- compute begin and end of parent and child 571> parentAddr <- call get_address [parentPP] 572> childAddr <- call get_address [childPP] 573> parentSize <- call get_size [parentPP] 574> childSize <- call get_size [childPP] 575> parentEnd <- return $ parentAddr .+. parentSize 576> childEnd <- return $ childAddr .+. childSize 577> 578> -- check that the child is inside the parent 579> ifc (return (childType .==. parentType)) 580> -- for self-retypes the ancestor must be strictly greater than the child 581> (checkStrictInside parentAddr parentEnd childAddr childEnd) 582> (checkInside parentAddr parentEnd childAddr childEnd) 583> 584> where 585> checkStrictInside parentAddr parentEnd childAddr childEnd = 586> do returnc (((parentAddr .<. childAddr) .&. (parentEnd .>=. childEnd)) 587> .|. ((parentAddr .<=. childAddr) .&. (parentEnd .>. childEnd))) 588> checkInside parentAddr parentEnd childAddr childEnd = 589> do returnc ((parentAddr .<=. childAddr) .&. (parentEnd .>=. childEnd)) 590> 591 592\section{Back-end} 593 594> backend :: Capabilities -> FoFCode PureExpr 595> backend caps = 596> do dummy <- newEnum "__attribute__((__packed__)) objtype" enums "ObjType_Num" 597> dummy <- newEnum "objdefines" defs "ObjDefines_Num" 598> getAddress <- get_address caps 599> getSize <- get_size caps 600> getTypeRoot <- get_type_root caps 601> compareCaps <- compare_caps caps getTypeRoot getAddress getSize 602> isWellFounded <- is_well_founded capList 603> isEqualTypes <- is_equal_types 604> isRevokedFirst <- is_revoked_first capList 605> isCopy <- is_copy caps compareCaps 606> isAncestor <- is_ancestor caps isWellFounded getAddress getSize 607> return void 608> where capList = capabilities caps 609> enums = mkObjTypeEnum capList 610> defs = mkObjDefineList $ defines caps 611 612> userbackend :: Capabilities -> FoFCode PureExpr 613> userbackend caps = 614> do dummy <- newEnum "objtype" enums "ObjType_Num" 615> getAddress <- get_address caps 616> getSize <- get_size caps 617> getTypeRoot <- get_type_root caps 618> compareCaps <- compare_caps caps getTypeRoot getAddress getSize 619> isWellFounded <- is_well_founded capList 620> isEqualTypes <- is_equal_types 621> isCopy <- is_copy caps compareCaps 622> isAncestor <- is_ancestor caps isWellFounded getAddress getSize 623> return void 624> where capList = capabilities caps 625> enums = mkObjTypeEnum capList 626