Fix fatal error for list comprehensions without condition or True c…

…ondition Ref. #1302, eng/recordflux/RecordFlux#1786
AdaCore · Sep 11, 2024 · bab3228 · bab3228
1 parent 351c6d1
commit bab3228
Show file tree

Hide file tree

Showing 8 changed files with 364 additions and 158 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -35,6 +35,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Copying of sequence fields for external IO buffers (eng/recordflux/RecordFlux#1704)
 - Syntax highlighting for identifiers with numbers or keywords (AdaCore/RecordFlux#1301, eng/recordflux/RecordFlux#1776)
 - Fatal errors caused by missing locations after proof timeouts (eng/recordflux/RecordFlux#1782)
+- Fatal errors when generating code for list comprehensions without condition or `True` condition (AdaCore/RecordFlux#1302, eng/recordflux/RecordFlux#1786)
 
 ## [0.23.0] - 2024-08-23
 

diff --git a/rflx/expr_conv.py b/rflx/expr_conv.py
@@ -344,9 +344,9 @@ def _(expression: expr.Literal, _variable_id: Generator[ID, None, None]) -> ir.C
 
     if expression.type_ == rty.BOOLEAN:
         if expression.identifier == ID("True"):
-            return ir.ComplexExpr([], ir.BoolVal(value=True, origin=expression))
+            return ir.ComplexBoolExpr([], ir.BoolVal(value=True, origin=expression))
         assert expression.identifier == ID("False")
-        return ir.ComplexExpr([], ir.BoolVal(value=False, origin=expression))
+        return ir.ComplexBoolExpr([], ir.BoolVal(value=False, origin=expression))
 
     return ir.ComplexExpr([], ir.EnumLit(expression.name, expression.type_, origin=expression))
 
@@ -807,9 +807,9 @@ def _(
 def _(expression: expr.Comprehension, variable_id: Generator[ID, None, None]) -> ir.ComplexExpr:
     sequence = to_ir(expression.sequence, variable_id)
     selector = to_ir(expression.selector, variable_id)
-    condition = to_ir(expression.condition, variable_id)
+    condition = to_ir(expression.condition.simplified(), variable_id)
     assert isinstance(sequence.expr, (ir.Var, ir.FieldAccess))
-    assert isinstance(condition, ir.ComplexBoolExpr), condition
+    assert isinstance(condition, ir.ComplexBoolExpr)
     return ir.ComplexExpr(
         sequence.stmts,
         ir.Comprehension(

diff --git a/rflx/generator/state_machine.py b/rflx/generator/state_machine.py
@@ -5945,6 +5945,30 @@ def _comprehension(  # noqa: PLR0913
                 ),
             ]
 
+        handle_element = (
+            self._comprehension_append_element(
+                target_identifier,
+                target_type,
+                selector_stmts,
+                selector,
+                update_context,
+                local_exception_handler,
+                is_global,
+                state,
+            )
+            if isinstance(target_type, rty.Sequence)
+            else self._comprehension_assign_element(
+                target_identifier,
+                target_type,
+                selector_stmts,
+                selector,
+                update_context,
+                local_exception_handler,
+                is_global,
+                state,
+            )
+        )
+
         return While(
             Call(
                 sequence_type * "Has_Element",
@@ -6000,35 +6024,16 @@ def _comprehension(  # noqa: PLR0913
                                 is_global,
                             )
                         ],
-                        IfStatement(
-                            [
-                                (
-                                    self._to_ada_expr(condition, is_global),
-                                    (
-                                        self._comprehension_append_element(
-                                            target_identifier,
-                                            target_type,
-                                            selector_stmts,
-                                            selector,
-                                            update_context,
-                                            local_exception_handler,
-                                            is_global,
-                                            state,
-                                        )
-                                        if isinstance(target_type, rty.Sequence)
-                                        else self._comprehension_assign_element(
-                                            target_identifier,
-                                            target_type,
-                                            selector_stmts,
-                                            selector,
-                                            update_context,
-                                            local_exception_handler,
-                                            is_global,
-                                            state,
-                                        )
-                                    ),
+                        *(
+                            handle_element
+                            if condition == ir.BoolVal(value=True)
+                            else [
+                                IfStatement(
+                                    [
+                                        (self._to_ada_expr(condition, is_global), handle_element),
+                                    ],
                                 ),
-                            ],
+                            ]
                         ),
                         *update_context,
                     ],