define vnode_size 12; /* BASE_PAGE_BITS */
/**
- XXX: this is for the Dispatcher/Endpoint hack (see corresponding cap
- definitions) and should be removed as soon as that is resolved -MN
-**/
-define zero 0;
-
-/**
The capabilities of the whole system are listed thereafter.
The minimal definition consists of a name and an empty body.
**/
/**
The Dispatcher is a special case that can be retyped several
times to an end-point
-
- The comparison function for a singleton ptr, the formula is
- simply:
- "parent->ptr == child->ptr"
**/
/** Note: This must be the first statement */
can_retype_multiple;
We allow the use of unknow structures. However, equality will
be defined by address, not by structure.
**/
-
"struct dcb" dcb; /* Pointer to kernel DCB */
address { mem_to_phys(dcb) };
size_bits { dispatcher_size };
};
-/** Then, we go back to routine **/
-
cap EndPoint from Dispatcher {
/* IDC endpoint */
uint32 epbuflen; /* Length of endpoint buffer in words */
address { mem_to_phys(listener) };
- /* XXX: see note before dispatcher -MN */
- size { zero };
- /**
- preferable definitions for address and size, should be used as soon as
- the whole multi retype hack stuff is fixed:
+ /** XXX
+ Preferable definitions for address and size would be as below. These
+ should be used as soon as the whole multi retype hack stuff is fixed:
address { mem_to_phys(listener + epoffset) };
size { epbuflen };
**/
};
+/** Then, we go back to routine **/
cap Frame from RAM from_self {
/* Mappable memory frame */
> pretty (AddressExpr e) = pretty e
> pretty (MemToPhysOp e) = text "mem_to_phys(" <> pretty e <> text ")"
-> data SizeExpr = SizeExpr Expr | SizeBitsExpr Expr
+> data SizeExpr = ZeroSize | SizeExpr Expr | SizeBitsExpr Expr
> deriving Show
> instance Pretty SizeExpr where
+> pretty (ZeroSize) = text "0"
> pretty (SizeExpr e) = pretty e
> pretty (SizeBitsExpr e) = text "2^(" <> pretty e <> char ')'
Generate code to calculate the "size" property of a cap.
> sizeExprCode :: [(String, Int)] -> PureExpr -> String -> SizeExpr -> FoFCode PureExpr
+> sizeExprCode defs cap capType (ZeroSize) = return $ uint64 0
> sizeExprCode defs cap capType (SizeExpr expr) = exprCode defs cap capType expr
> sizeExprCode defs cap capType (SizeBitsExpr expr) =
> do
(fields, addresses, sizes, eqExprs) <- return $ unzipDefs annotatedFields
-- lengths to check
- (numAddrs, numSizes) <- return (length addresses, length sizes)
+ let numAddrs = length addresses
+ numSizes = length sizes
-- check that there are either 0 or 1 of both address and size definitions
if numAddrs > 1
if numSizes > 1
then unexpected ("multiple size definitions for cap " ++ name)
else return ()
- if numAddrs > 0 && numSizes < 1
- then unexpected ("have address definition but no size definition for cap " ++ name)
- else return ()
if numAddrs < 1 && numSizes > 0
then unexpected ("have size definition but no address definition for cap " ++ name)
else return ()
- -- merged address and size expressions if present
- return $ let rangeExpr = if null addresses then Nothing else Just (head addresses, head sizes)
- in (fields, rangeExpr, eqExprs, multi)
+ -- merge address and size expressions if present
+ let rangeExpr = if null addresses
+ then Nothing
+ else Just $
+ if null sizes
+ then (head addresses, ZeroSize)
+ else (head addresses, head sizes)
+ return (fields, rangeExpr, eqExprs, multi)
where
-- un-maybe lists from capfields parsing