#[dyn_alloc] attribute.

Introduce the `#[dyn_alloc]` attribute that applies to extern types
only. It tells the compiler that the type allocates its storage dynamically
on the heap.  Rust knows the size of the stack-allocated portion of such
types statically and allows using them as part of recursive typedefs.

This is a step towards supporting generic container types.  Currently
the compiler has built-in support for Vec, Set, Map, TinySet types.
Adding new container types, e.g., the immutable containers that will
be introduced shortly, requires changes to the compiler.  There are two
reasons for this.  First, the compiler needs to know how to iterate over
instances of these types in for-loops.  Second, it must be aware that
these types allocate their storage dynamically and can therefore be
safely used to construct recursive typedefs.

This commit takes care of the latter: instead of maintaining a list of
known dynamically allocated types in the compiler, we allow the
programmer to label types as dynamically allocated using the new
attribute.

Author: ryzhyk

doc/tutorial/tutorial.md

@@ -3011,6 +3011,18 @@ to optimize data structures layout:
 extern type IObj<'A>
 ```
 
+### `#[dyn_alloc]`
+
+This attribute is applicable to `extern type` declarations.  It tells the
+compiler that the type allocates its storage dynamically on the heap.  Rust
+knows the size of the stack-allocated portion of such types statically and
+allows using them as part of recursive typedefs.
+
+```
+#[dyn_alloc]
+extern type Set<'A>
+```
+
 ### `#[custom_serde]`
 
 Tells DDlog not to generate `Serialize` and `Deserialize` implementations for a type.

lib/ddlog_std.dl

@@ -558,6 +558,7 @@ function max(g: Group<'K, 'V>): 'V {
 /*
  * Vec
  */
+#[dyn_alloc]
 extern type Vec<'A>
 
 extern function vec_empty(): Vec<'A>
@@ -667,6 +668,7 @@ function update_nth(v: mut Vec<'X>, idx: usize, value: 'X): bool {
  * Map
  */
 
+#[dyn_alloc]
 extern type Map<'K,'V>
 
 extern function map_empty(): Map<'K, 'V>
@@ -713,6 +715,7 @@ function keys(m: Map<'K, 'V>): Vec<'K> {
  * Set
  */
 
+#[dyn_alloc]
 extern type Set<'A>
 
 extern function set_singleton(x: 'X): Set<'X>

lib/tinyset.dl

@@ -4,6 +4,7 @@
  * `Set64`, which is a set of values that fit in 64 bits and can be cloned by
  * copying (e.g., 8, 16, 32, or 64-bit integers). */
 
+#[dyn_alloc]
 extern type Set64<'X>
 
 extern function size(s: Set64<'X>): bit<64>

src/Language/DifferentialDatalog/Attribute.hs

@@ -1,5 +1,5 @@
 {-
-Copyright (c) 2020 VMware, Inc.
+Copyright (c) 2021 VMware, Inc.
 SPDX-License-Identifier: MIT
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
@@ -53,6 +53,7 @@ typedefValidateAttrs d tdef@TypeDef{..} = do
     _ <- tdefCheckCustomSerdeAttr d tdef
     _ <- tdefCheckCustomFromRecord d tdef
     _ <- tdefCheckSharedRefAttr d tdef
+    _ <- tdefCheckDynAllocAttr d tdef
     _ <- tdefCheckAliasAttr d tdef
     _ <- checkRustAttrs d tdefAttrs
     maybe (return ()) (typeValidateAttrs d) tdefType
@@ -84,6 +85,9 @@ typedefValidateAttr d TypeDef{..} attr = do
                 $ "'sharef_ref' attribute is only applicable to extern types."
             check d (length tdefArgs == 1) (pos attr)
                 $ "Types annotated with 'shared_ref' must have exactly one type argument, e.g., \"Ref<'T>\"."
+         "dyn_alloc" -> do
+            check d (isNothing tdefType) (pos attr)
+                $ "'dyn_alloc' attribute is only applicable to extern types."
          "alias" -> do
              case tdefType of
                   Just TUser{} -> err d (pos attr) "The 'alias' attribute does not apply to struct types."
@@ -203,6 +207,22 @@ tdefGetSharedRefAttr d tdef =
          Left e  -> error e
          Right b -> b
 
+{- 'dyn_alloc' attribute: Tells DDlog that the type is a shared reference in
+ - the style of `Ref` and `Intern`. -}
+tdefCheckDynAllocAttr :: (MonadError String me) => DatalogProgram -> TypeDef -> me Bool
+tdefCheckDynAllocAttr d TypeDef{..} =
+    case find ((== "dyn_alloc") . name) tdefAttrs of
+         Nothing   -> return False
+         Just attr -> do check d (attrVal attr == eTrue) (pos attr)
+                               "The value of 'dyn_alloc' attribute must be 'true' or empty"
+                         return True
+
+tdefGetDynAllocAttr :: DatalogProgram -> TypeDef -> Bool
+tdefGetDynAllocAttr d tdef =
+    case tdefCheckDynAllocAttr d tdef of
+         Left e  -> error e
+         Right b -> b
+
 {- 'alias' attribute: Tells DDlog not to generate Rust declaration for the type
  - and instead replace all occurrences of the type with its definition. -}
 tdefCheckAliasAttr :: (MonadError String me) => DatalogProgram -> TypeDef -> me Bool

src/Language/DifferentialDatalog/Type.hs

@@ -1,5 +1,5 @@
 {-
-Copyright (c) 2018-2020 VMware, Inc.
+Copyright (c) 2018-2021 VMware, Inc.
 SPDX-License-Identifier: MIT
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
@@ -48,7 +48,7 @@ module Language.DifferentialDatalog.Type(
     typDeref',
     typDeref'',
     isBool, isBit, isSigned, isBigInt, isInteger, isFP, isString, isStruct, isTuple, isGroup, isDouble, isFloat,
-    isMap, isTinySet, isSharedRef,
+    isMap, isTinySet, isSharedRef, isDynAlloced,
     isOption, isResult,
     checkTypesMatch,
     typesMatch,
@@ -105,10 +105,6 @@ sET_TYPES = [mOD_STD ++ "::Set", mOD_STD ++ "::Vec", tINYSET_TYPE]
 tINYSET_TYPE :: String
 tINYSET_TYPE = "tinyset::Set64"
 
--- Dynamically allocated types.
-dYNAMIC_TYPES :: [String]
-dYNAMIC_TYPES = mAP_TYPE : sET_TYPES
-
 gROUP_TYPE :: String
 gROUP_TYPE = mOD_STD ++ "::Group"
 
@@ -475,6 +471,12 @@ isSharedRef d a =
          TOpaque _ t _ -> tdefGetSharedRefAttr d $ getType d t
          _             -> False
 
+isDynAlloced :: (WithType a) => DatalogProgram -> a -> Bool
+isDynAlloced d a =
+    case typ' d a of
+         TOpaque _ t _ -> tdefGetDynAllocAttr d $ getType d t
+         _             -> False
+
 isOption :: (WithType a) => DatalogProgram -> a -> Bool
 isOption d a = case typ'' d a of
                     TUser _ t _ | t == oPTION_TYPE -> True
@@ -546,9 +548,9 @@ typeStaticMemberTypes' :: DatalogProgram -> Type -> [String]
 typeStaticMemberTypes' d TStruct{..}   = concatMap (typeStaticMemberTypes d . typ)
                                                    $ concatMap consArgs typeCons
 typeStaticMemberTypes' d TTuple{..}    = concatMap (typeStaticMemberTypes d . typ) typeTupArgs
-typeStaticMemberTypes' d t@TUser{..}   | elem typeName dYNAMIC_TYPES || isSharedRef d t = []
+typeStaticMemberTypes' d t@TUser{..}   | isDynAlloced d t || isSharedRef d t = []
                                        | otherwise = typeName : concatMap (typeStaticMemberTypes d) typeArgs
-typeStaticMemberTypes' d t@TOpaque{..} | elem typeName dYNAMIC_TYPES || isSharedRef d t = []
+typeStaticMemberTypes' d t@TOpaque{..} | isDynAlloced d t || isSharedRef d t = []
                                        | otherwise = concatMap (typeStaticMemberTypes d) typeArgs
 typeStaticMemberTypes' _ _             = []