Fix fatal error caused by variable in case expression

Ref. eng/recordflux/RecordFlux#1800

CHANGELOG.md

@@ -12,6 +12,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Rejection of invalid parameter types and return types in function declarations (eng/recordflux/RecordFlux#977)
 - Consequential errors caused by undefined variables in binary expressions (eng/recordflux/RecordFlux#1672)
 - Rejection of variable declarations with type `Opaque` (eng/recordflux/RecordFlux#633)
+- Fatal error caused by variable in case expression (eng/recordflux/RecordFlux#1800)
 
 ## [0.24.0] - 2024-09-12
 

rflx/ir.py

@@ -2276,6 +2276,31 @@ def _(
             expression.origin,
         )
 
+    elif isinstance(expression, CaseExpr):
+        assert isinstance(target_type, ty.Integer)
+
+        choices = []
+
+        for k, v in expression.choices:
+            assert isinstance(v, IntExpr)
+            choices.append(
+                (
+                    k,
+                    (
+                        v
+                        if target_type.is_compatible_strong(v.type_)
+                        else IntConversion(target_type, v, v.origin)
+                    ),
+                ),
+            )
+
+        result = expression.__class__(
+            expression.expression,
+            choices,
+            target_type,
+            origin=expression.origin,
+        )
+
     else:
         assert False
 

tests/feature/fsm_case_expression_numeric/generated/rflx-test-s-fsm.adb

@@ -38,7 +38,7 @@ is
         Ghost;
    begin
       pragma Assert (Start_Invariant);
-      -- tests/feature/fsm_case_expression_numeric/test.rflx:19:10
+      -- tests/feature/fsm_case_expression_numeric/test.rflx:21:10
       Test.Message.Verify_Message (Ctx.P.Message_Ctx);
       if Test.Message.Well_Formed_Message (Ctx.P.Message_Ctx) then
          Ctx.P.Next_State := S_Prepare;
@@ -55,6 +55,7 @@ is
        Initialized (Ctx)
    is
       Value : Test.Tiny_Int;
+      T : Test.Int;
       T_0 : Test.Tiny_Int;
       function Prepare_Invariant return Boolean is
         (Ctx.P.Slots.Slot_Ptr_1 = null)
@@ -64,7 +65,9 @@ is
         Ghost;
    begin
       pragma Assert (Prepare_Invariant);
-      -- tests/feature/fsm_case_expression_numeric/test.rflx:31:25
+      -- tests/feature/fsm_case_expression_numeric/test.rflx:34:10
+      T := 1;
+      -- tests/feature/fsm_case_expression_numeric/test.rflx:35:25
       pragma Warnings (Off, "condition can only be False if invalid values present");
       pragma Warnings (Off, "condition is always False");
       pragma Warnings (Off, "this code can never be executed and has been deleted");
@@ -80,17 +83,17 @@ is
       pragma Warnings (On, "this code can never be executed and has been deleted");
       pragma Warnings (On, "condition is always False");
       pragma Warnings (On, "condition can only be False if invalid values present");
-      -- tests/feature/fsm_case_expression_numeric/test.rflx:31:25
+      -- tests/feature/fsm_case_expression_numeric/test.rflx:35:25
       T_0 := Test.Message.Get_Value (Ctx.P.Message_Ctx);
-      -- tests/feature/fsm_case_expression_numeric/test.rflx:31:10
+      -- tests/feature/fsm_case_expression_numeric/test.rflx:35:10
       Value := (case T_0 is
           when 1 | 2 =>
              4,
           when 3 =>
-             1,
+             Test.Tiny_Int (T),
           when 4 =>
              2);
-      -- tests/feature/fsm_case_expression_numeric/test.rflx:36:10
+      -- tests/feature/fsm_case_expression_numeric/test.rflx:40:10
       Test.Message.Reset (Ctx.P.Message_Ctx);
       if not Test.Message.Sufficient_Space (Ctx.P.Message_Ctx, Test.Message.F_Value) then
          Ctx.P.Next_State := S_Final;
@@ -122,7 +125,7 @@ is
         Ghost;
    begin
       pragma Assert (Reply_Invariant);
-      -- tests/feature/fsm_case_expression_numeric/test.rflx:45:10
+      -- tests/feature/fsm_case_expression_numeric/test.rflx:49:10
       Ctx.P.Next_State := S_Final;
       pragma Assert (Reply_Invariant);
    end Reply;

tests/feature/fsm_case_expression_numeric/generated/rflx-test.ads

@@ -36,4 +36,20 @@ is
      Pre =>
        Valid_Tiny_Int (Val);
 
+   type Int is range 0 .. 2**16 - 1 with
+     Size =>
+       16;
+
+   function Valid_Int (Val : RFLX.RFLX_Types.Base_Integer) return Boolean is
+     (Val <= 65535);
+
+   function To_Base_Integer (Val : RFLX.Test.Int) return RFLX.RFLX_Types.Base_Integer is
+     (RFLX.RFLX_Types.Base_Integer (Val));
+
+   function To_Actual (Val : RFLX.RFLX_Types.Base_Integer) return RFLX.Test.Int is
+     (RFLX.Test.Int (Val))
+    with
+     Pre =>
+       Valid_Int (Val);
+
 end RFLX.Test;

tests/feature/fsm_case_expression_numeric/test.rflx

@@ -9,6 +9,8 @@ package Test is
          Value : Tiny_Int;
       end message;
 
+   type Int is range 0 .. 2 ** 16 - 1 with Size => 16;
+
    generic
       Channel : Channel with Readable, Writable;
    machine S is
@@ -27,10 +29,12 @@ package Test is
 
       state Prepare is
          Value : Tiny_Int;
+         T : Int;
       begin
+         T := 1;
          Value := (case Message.Value is
                       when 1 | 2 => 4,
-                      when 3     => 1,
+                      when 3     => T,
                       when 4     => 2);
 
          Message := Message'(Value => Value);