Fix code generation for trivial sessions

- Fix noncompilable code for session without allocation points - Fix noncompilable code for session without IO states Fixes #883 Fixes #884
AdaCore · Dec 21, 2021 · ec852ad · ec852ad
1 parent e795b6d
commit ec852ad
Show file tree

Hide file tree

Showing 3 changed files with 47 additions and 19 deletions.
diff --git a/rflx/generator/allocator.py b/rflx/generator/allocator.py
@@ -5,6 +5,7 @@
 from rflx import expression as expr, identifier as rid, typing_ as rty
 from rflx.ada import (
     ID,
+    TRUE,
     Add,
     And,
     AndThen,
@@ -20,6 +21,7 @@
     Last,
     NamedAggregate,
     NotEqual,
+    NullStatement,
     Number,
     ObjectDeclaration,
     OrElse,
@@ -128,8 +130,9 @@ def _ptr_type(size: int) -> ID:
         return ID(f"Slot_Ptr_Type_{size}")
 
     def _create(self, slots: List[NumberedSlotInfo]) -> None:
-        self._unit_part += self._create_ptr_subtypes(slots)
-        self._unit_part += self._create_slots(slots)
+        if slots:
+            self._unit_part += self._create_ptr_subtypes(slots)
+            self._unit_part += self._create_slots(slots)
         self._unit_part += self._create_init_pred(slots)
         self._unit_part += self._create_init_proc(slots)
         self._unit_part += self._create_global_allocated_pred(slots)
@@ -206,7 +209,9 @@ def _create_init_pred(self, slots: List[NumberedSlotInfo]) -> UnitPart:
                             )
                             for slot in slots
                         ]
-                    ),
+                    )
+                    if slots
+                    else TRUE,
                 )
             ]
         )
@@ -233,19 +238,25 @@ def _create_global_allocated_pred(self, slots: List[NumberedSlotInfo]) -> UnitPa
                             for slot in slots
                             if not slot.global_
                         ],
-                    ),
+                    )
+                    if slots
+                    else TRUE,
                 )
             ]
         )
 
     def _create_init_proc(self, slots: List[NumberedSlotInfo]) -> UnitPart:
-        assignments = [
-            Assignment(
-                self._slot_name(slot.slot_id),
-                UnrestrictedAccess(Variable(ID(f"Slot_{slot.slot_id}"))),
-            )
-            for slot in slots
-        ]
+        assignments: List[Statement] = (
+            [
+                Assignment(
+                    self._slot_name(slot.slot_id),
+                    UnrestrictedAccess(Variable(ID(f"Slot_{slot.slot_id}"))),
+                )
+                for slot in slots
+            ]
+            if slots
+            else [NullStatement()]
+        )
         proc = ProcedureSpecification(ID("Initialize"))
         return UnitPart(
             [SubprogramDeclaration(proc, [Postcondition(Call("Initialized"))])],

diff --git a/rflx/generator/session.py b/rflx/generator/session.py
@@ -530,13 +530,19 @@ def _create_declarations(
                     for t in self._session_context.used_types
                     if not model.is_builtin_type(t) and not model.is_internal_type(t)
                 ],
-                EnumerationType(
-                    "Channel",
-                    {
-                        ID(f"C_{parameter.identifier}"): None
-                        for parameter in session.parameters.values()
-                        if isinstance(parameter, decl.ChannelDeclaration)
-                    },
+                *(
+                    [
+                        EnumerationType(
+                            "Channel",
+                            {
+                                ID(f"C_{parameter.identifier}"): None
+                                for parameter in session.parameters.values()
+                                if isinstance(parameter, decl.ChannelDeclaration)
+                            },
+                        )
+                    ]
+                    if session.parameters.values()
+                    else []
                 ),
                 EnumerationType("State", {ID(f"S_{s.identifier}"): None for s in session.states}),
             ],
@@ -906,7 +912,9 @@ def _create_run_procedure(session: model.Session) -> UnitPart:
                     In(
                         Variable("P_Next_State"),
                         ChoiceList(*[Variable(f"S_{state.identifier}") for state in io_states]),
-                    ),
+                    )
+                    if io_states
+                    else FALSE,
                 ),
                 SubprogramBody(
                     specification,

diff --git a/tests/unit/generator_test.py b/tests/unit/generator_test.py
@@ -2654,3 +2654,12 @@ def test_provability(test_case: str, tmp_path: Path) -> None:
         main=main,
         units=spark_units,
     )
+
+
+def test_simple_model(tmp_path: Path) -> None:
+    state = State("St", transitions=[])
+    session = Session(
+        "P::S", initial="St", final="St", states=[state], declarations=[], parameters=[], types=[]
+    )
+    model = Model(types=[], sessions=[session])
+    assert_compilable_code(model, Integration(), tmp_path)