Made cap size optional.
authorMark Nevill <nevillm@ethz.ch>
Fri, 20 Jan 2012 08:17:24 +0000 (09:17 +0100)
committerMark Nevill <nevillm@ethz.ch>
Fri, 20 Jan 2012 08:17:24 +0000 (09:17 +0100)
capabilities/caps.hl
tools/hamlet/HamletAst.lhs
tools/hamlet/HamletBackend.lhs
tools/hamlet/Parser.hs

index 8672071..9bfb7a0 100644 (file)
@@ -28,12 +28,6 @@ define dispatcher_size 9;
 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.
 **/
@@ -118,10 +112,6 @@ cap Dispatcher from RAM {
     /**
       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;
@@ -130,15 +120,12 @@ cap Dispatcher from RAM {
       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 */
 
@@ -147,12 +134,10 @@ cap EndPoint from Dispatcher {
     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 };
@@ -161,6 +146,7 @@ cap EndPoint from Dispatcher {
     **/
 };
 
+/** Then, we go back to routine **/
 
 cap Frame from RAM from_self {
     /* Mappable memory frame */
index d240ca1..46740eb 100644 (file)
 >     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 ')'
 
index 2683b87..2ec16e1 100644 (file)
@@ -215,6 +215,7 @@ Generate code to calculate the "address" property of a cap.
 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
index f07f2a4..9b61d86 100644 (file)
@@ -121,7 +121,8 @@ capabilityDef name = 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
@@ -130,16 +131,18 @@ capabilityDef name = do
     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