Issue 713: Derive buffer sizes for some constructs

rflx/generator/allocator.py

@@ -42,7 +42,7 @@
 )
 from rflx.error import Location
 from rflx.integration import Integration
-from rflx.model import Session, declaration as decl, statement as stmt
+from rflx.model import Session, State, declaration as decl, statement as stmt
 
 from . import const
 
@@ -268,6 +268,18 @@ def _allocate_global_slots(self) -> List[SlotInfo]:
                 slots.append(SlotInfo(self.get_size(d.identifier), [d.location]))
         return slots
 
+    @staticmethod
+    def _scope(state: State, var_id: rid.ID) -> Optional[rid.ID]:
+        """
+        Return the scope of the variable var_id.
+
+        Return the ID of the state if var_id was defined in that state, otherwise
+        return None to indicate that var_id is a global variable of the session.
+        """
+        if var_id in state.declarations.keys():
+            return state.identifier.name
+        return None
+
     def _allocate_local_slots(self) -> List[SlotInfo]:
         """
         Allocate slots for state variables and state actions.
@@ -304,11 +316,17 @@ class AllocationRequirement:
                     and isinstance(a.expression.sequence, (expr.Selected, expr.Variable))
                 ):
                     state_requirements.append(
-                        AllocationRequirement(a.location, self._integration.defaultsize)
+                        AllocationRequirement(
+                            a.location,
+                            self.get_size(a.identifier, self._scope(s, a.identifier)),
+                        )
                     )
                 if isinstance(a, stmt.Assignment) and isinstance(a.expression, expr.Head):
                     state_requirements.append(
-                        AllocationRequirement(a.location, self._integration.defaultsize)
+                        AllocationRequirement(
+                            a.location,
+                            self.get_size(a.identifier, self._scope(s, a.identifier)),
+                        )
                     )
 
             alloc_requirements_per_state.append(state_requirements)

tests/integration/session_comprehension_on_sequence/generated/rflx-test-session.adb

@@ -211,7 +211,7 @@ is
          return;
       end if;
       if
-         Universal.Option_Types.Size (Option_Types_Ctx) <= 32768
+         Universal.Option_Types.Size (Option_Types_Ctx) <= 64768
          and then Universal.Option_Types.Size (Option_Types_Ctx) mod RFLX_Types.Byte'Size = 0
       then
          if RFLX_Types.To_First_Bit_Index (Message_Ctx.Buffer_Last) - RFLX_Types.To_First_Bit_Index (Message_Ctx.Buffer_First) + 1 >= RFLX_Types.Bit_Length (Universal.Option_Types.Size (Option_Types_Ctx) + 24) then

tests/integration/session_comprehension_on_sequence/generated/rflx-test-session_allocator.adb

@@ -9,9 +9,9 @@ is
 
    Slot_2 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
 
-   Slot_3 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
+   Slot_3 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 8095 => RFLX_Types.Byte'First);
 
-   Slot_4 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
+   Slot_4 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 8095 => RFLX_Types.Byte'First);
 
    procedure Initialize with
      SPARK_Mode =>

tests/integration/session_comprehension_on_sequence/generated/rflx-test-session_allocator.ads

@@ -18,13 +18,19 @@ is
        or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First
                 and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095);
 
+   subtype Slot_Ptr_Type_8096 is RFLX_Types.Bytes_Ptr with
+     Dynamic_Predicate =>
+       Slot_Ptr_Type_8096 = null
+       or else (Slot_Ptr_Type_8096'First = RFLX_Types.Index'First
+                and then Slot_Ptr_Type_8096'Last = RFLX_Types.Index'First + 8095);
+
    Slot_Ptr_1 : Slot_Ptr_Type_4096;
 
    Slot_Ptr_2 : Slot_Ptr_Type_4096;
 
-   Slot_Ptr_3 : Slot_Ptr_Type_4096;
+   Slot_Ptr_3 : Slot_Ptr_Type_8096;
 
-   Slot_Ptr_4 : Slot_Ptr_Type_4096;
+   Slot_Ptr_4 : Slot_Ptr_Type_8096;
 
    function Initialized return Boolean is
      (Slot_Ptr_1 /= null

tests/integration/session_comprehension_on_sequence/test.rfi

@@ -0,0 +1,7 @@
+Session:
+  Session:
+    Buffer_Size:
+      Default: 4096
+      Local:
+        Process:
+          Option_Types: 8096

tests/integration/session_sequence_append_head/generated/rflx-test-session.ads

@@ -107,7 +107,7 @@ private
       and then Tags_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095
       and then TLV.Message.Has_Buffer (Message_Ctx)
       and then Message_Ctx.Buffer_First = RFLX_Types.Index'First
-      and then Message_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095
+      and then Message_Ctx.Buffer_Last = RFLX_Types.Index'First + 8095
       and then Test.Session_Allocator.Global_Allocated);
 
    function Active return Boolean is

tests/integration/session_sequence_append_head/generated/rflx-test-session_allocator.adb

@@ -9,9 +9,9 @@ is
 
    Slot_2 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
 
-   Slot_3 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
+   Slot_3 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 8095 => RFLX_Types.Byte'First);
 
-   Slot_4 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
+   Slot_4 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 8095 => RFLX_Types.Byte'First);
 
    Slot_5 : aliased RFLX_Types.Bytes := (RFLX_Types.Index'First .. RFLX_Types.Index'First + 4095 => RFLX_Types.Byte'First);
 

tests/integration/session_sequence_append_head/generated/rflx-test-session_allocator.ads

@@ -18,13 +18,19 @@ is
        or else (Slot_Ptr_Type_4096'First = RFLX_Types.Index'First
                 and then Slot_Ptr_Type_4096'Last = RFLX_Types.Index'First + 4095);
 
+   subtype Slot_Ptr_Type_8096 is RFLX_Types.Bytes_Ptr with
+     Dynamic_Predicate =>
+       Slot_Ptr_Type_8096 = null
+       or else (Slot_Ptr_Type_8096'First = RFLX_Types.Index'First
+                and then Slot_Ptr_Type_8096'Last = RFLX_Types.Index'First + 8095);
+
    Slot_Ptr_1 : Slot_Ptr_Type_4096;
 
    Slot_Ptr_2 : Slot_Ptr_Type_4096;
 
-   Slot_Ptr_3 : Slot_Ptr_Type_4096;
+   Slot_Ptr_3 : Slot_Ptr_Type_8096;
 
-   Slot_Ptr_4 : Slot_Ptr_Type_4096;
+   Slot_Ptr_4 : Slot_Ptr_Type_8096;
 
    Slot_Ptr_5 : Slot_Ptr_Type_4096;
 

tests/integration/session_sequence_append_head/test.rfi

@@ -0,0 +1,6 @@
+Session:
+  Session:
+    Buffer_Size:
+      Default: 4096
+      Global:
+        Message: 8096