Implement code generation for case expressions

Ref. #907

rflx/expression.py

@@ -2869,7 +2869,12 @@ def precedence(self) -> Precedence:
         raise NotImplementedError
 
     def ada_expr(self) -> ada.Expr:
-        raise NotImplementedError
+        choices = [
+            (Literal(choice).ada_expr(), expr.ada_expr())
+            for choices, expr in self.choices
+            for choice in choices
+        ]
+        return ada.CaseExpr(self.expr.ada_expr(), choices)
 
     @lru_cache(maxsize=None)
     def z3expr(self) -> z3.ExprRef:

rflx/generator/session.py

@@ -3874,7 +3874,7 @@ def _set_message_field(
                     exception_handler,
                 )
 
-        if isinstance(value, (expr.Number, expr.Aggregate)) or (
+        if isinstance(value, (expr.Number, expr.Aggregate, expr.Case)) or (
             isinstance(
                 value,
                 (expr.Variable, expr.Literal, expr.MathBinExpr, expr.MathAssExpr, expr.Size),

tests/integration/session_case_expression/config.yml

@@ -0,0 +1,12 @@
+input:
+  Channel:
+    - 3 0 0
+output:
+  - Channel
+sequence: |
+  Write Channel: 3 0 0
+  State: Start
+  State: Prepare
+  Read Channel: 2 0 1 16
+  State: Reply
+prove:

tests/integration/session_case_expression/generated/rflx-rflx_arithmetic.adb

@@ -0,0 +1,77 @@
+pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+
+package body RFLX.RFLX_Arithmetic with
+  SPARK_Mode
+is
+
+   function Shift_Left (Value : U64; Amount : Natural) return U64 with
+      Import,
+      Convention => Intrinsic,
+      Global => null;
+
+   function Shift_Right (Value : U64; Amount : Natural) return U64 with
+      Import,
+      Convention => Intrinsic,
+      Global => null;
+
+   function Shift_Add (V : U64;
+                       Data : U64;
+                       Amount : Natural;
+                       Bits : Natural) return U64
+   is
+      pragma Unreferenced (Bits);
+   begin
+      return Shift_Left (V, Amount) + Data;
+   end Shift_Add;
+
+   function Right_Shift (V : U64; Amount : Natural; Size : Natural) return U64
+   is
+      pragma Unreferenced (Size);
+   begin
+      return Shift_Right (V, Amount);
+   end Right_Shift;
+
+   function Left_Shift (V : U64; Amount : Natural; Size : Natural) return U64
+   is
+      pragma Unreferenced (Size);
+      Result : constant U64 := Shift_Left (V, Amount);
+   begin
+      return Result;
+   end Left_Shift;
+
+   function Mask_Lower (V : U64; Mask, Bits : Natural) return U64
+   is
+      Result : constant U64 := Shift_Left (Shift_Right (V, Mask), Mask);
+   begin
+      pragma Assert
+        (if Bits < U64'Size then Result <= 2 ** Bits - 2 ** Mask
+         elsif Mask < U64'Size then Result <= U64'Last - 2 ** Mask + 1);
+      return Result;
+   end Mask_Lower;
+
+   function Mask_Upper (V : U64; Mask : Natural) return U64
+   is
+   begin
+      return V and (2 ** Mask - 1);
+   end Mask_Upper;
+
+   function Add (A : U64; B : U64; Total_Bits, Lower_Bits : Natural) return U64
+   is
+      pragma Unreferenced (Total_Bits, Lower_Bits);
+   begin
+      return A + B;
+   end Add;
+
+   procedure Lemma_Size (Val : Base_Integer; Size : Positive) is
+   begin
+      if Size < Base_Integer'Size then
+         pragma Assert (Val < 2 ** Size);
+         pragma Assert (U64 (Val) < 2 ** Size);
+         pragma Assert (Fits_Into (U64 (Val), Size));
+      else
+         pragma Assert (Size = 63);
+         pragma Assert (Fits_Into (U64 (Val), Size));
+      end if;
+   end Lemma_Size;
+
+end RFLX.RFLX_Arithmetic;

tests/integration/session_case_expression/generated/rflx-rflx_arithmetic.ads

@@ -0,0 +1,96 @@
+pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+
+package RFLX.RFLX_Arithmetic with
+  SPARK_Mode
+is
+
+   type U64 is mod 2**64 with
+     Annotate => (GNATprove, No_Wrap_Around);
+
+   type Base_Integer is range 0 .. 2 ** 63 - 1;
+
+   --  Express that V contains at most Bits non-zero bits, in the least
+   --  significant part (the rest is zero).
+   pragma Warnings (Off, "postcondition does not mention function result");
+   function Fits_Into (V : U64; Bits : Natural) return Boolean
+   is (if Bits < U64'Size then V < 2 ** Bits)
+     with Post => True;
+
+   function Fits_Into (V : Base_Integer; Bits : Natural) return Boolean
+   is (if Bits < Base_Integer'Size then V < 2 ** Bits)
+     with Post => True;
+
+   --  Express that V contains (U64'Size - Bits) leading zero bits, then (Bits -
+   --  Lower) bits of data, then Lower bits of zeros.
+   --  |- (U64'Size - bits) -|- (Bits-Lower) -|- Lower -|
+   --  |000000000000000000000|xxxxxxxxxxxxxxxx|000000000|
+   function Fits_Into_Upper (V : U64; Bits, Lower : Natural) return Boolean
+   is (if Bits < U64'Size then V <= 2 ** Bits - 2 ** Lower
+       elsif Lower > 0 and then Lower < U64'Size then V <= U64'Last - 2 ** Lower + 1)
+     with Pre => Bits <= U64'Size and then Lower <= Bits,
+          Post => True;
+   pragma Warnings (On, "postcondition does not mention function result");
+
+   --  V is assumed to contain Bits bits of data. Add the Amount bits contained
+   --  in Data by shifting V to the left and adding Data. The result contains
+   --  (Bits + Amount) bits of data.
+   function Shift_Add (V : U64;
+                       Data : U64;
+                       Amount : Natural;
+                       Bits : Natural) return U64
+     with Pre  =>
+       Bits < U64'Size
+       and then Amount < U64'Size
+       and then Fits_Into (V, Bits)
+       and then U64'Size - Amount >= Bits
+       and then Fits_Into (Data, Amount),
+     Post => Fits_Into (Shift_Add'Result, Bits + Amount);
+
+   --  Wrapper of Shift_Right that expresses the operation in terms of
+   --  Fits_Into.
+   function Right_Shift (V : U64; Amount : Natural; Size : Natural) return U64 with
+     Pre =>
+       Size <= U64'Size
+       and then Fits_Into (V, Size)
+       and then Amount <= Size
+       and then Size - Amount < U64'Size,
+     Post => Fits_Into (Right_Shift'Result, Size - Amount);
+
+   --  Wrapper of Shift_Left that expresses the operation in terms of
+   --  Fits_Into/Fits_Into_Upper.
+   function Left_Shift (V : U64; Amount : Natural; Size : Natural) return U64 with
+     Pre =>
+       Size < U64'Size
+       and then Amount < U64'Size
+       and then Fits_Into (V, Size)
+       and then Size + Amount < U64'Size,
+       Post => Fits_Into_Upper (Left_Shift'Result, Size + Amount, Amount);
+
+   --  V is assumed to have Bits bits of data. Set the lower bits of V to zero.
+   function Mask_Lower (V : U64; Mask, Bits : Natural) return U64
+     with Pre => Bits <= U64'Size and then Fits_Into (V, Bits) and then Mask <= Bits and then Mask >= 1,
+          Post => Fits_Into_Upper (Mask_Lower'Result, Bits, Mask);
+
+   --  Set the upper bits of V to zero.
+   function Mask_Upper (V : U64; Mask : Natural) return U64
+     with Pre => Mask < U64'Size,
+          Post => Fits_Into (Mask_Upper'Result, Mask);
+
+   --  Add A and B in the special case where A only uses the upper bits and B
+   --  only the lower bits.
+   function Add (A : U64; B : U64; Total_Bits, Lower_Bits : Natural) return U64
+     with Pre =>
+       Total_Bits <= U64'Size
+       and then Lower_Bits <= Total_Bits
+       and then (if Total_Bits = U64'Size then Lower_Bits /= U64'Size)
+       and then Fits_Into_Upper (A, Total_Bits, Lower_Bits)
+       and then Fits_Into (B, Lower_Bits),
+     Post => Add'Result = A + B and Fits_Into (Add'Result, Total_Bits),
+     Global => null;
+
+   procedure Lemma_Size (Val : Base_Integer; Size : Positive)
+   with Ghost,
+      Pre => Size in 1 .. 63 and then Fits_Into (Val, Size),
+      Post => Fits_Into (U64 (Val), Size);
+
+end RFLX.RFLX_Arithmetic;

tests/integration/session_case_expression/generated/rflx-rflx_builtin_types-conversions.ads

@@ -0,0 +1,63 @@
+pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+
+with RFLX.RFLX_Arithmetic;
+
+package RFLX.RFLX_Builtin_Types.Conversions with
+  SPARK_Mode
+is
+
+   pragma Annotate (GNATprove, Always_Return, Conversions);
+
+   function Valid_Boolean (Val : RFLX.RFLX_Arithmetic.U64) return Boolean is
+     (case Val is
+         when 0 | 1 =>
+            True,
+         when others =>
+            False);
+
+   function To_U64 (Enum : Boolean) return RFLX.RFLX_Arithmetic.U64 is
+     (case Enum is
+         when False =>
+            0,
+         when True =>
+            1);
+
+   function To_Actual (Val : RFLX.RFLX_Arithmetic.U64) return Boolean is
+     (case Val is
+         when 0 =>
+            False,
+         when 1 =>
+            True,
+         when others =>
+            False)
+    with
+     Pre =>
+       Valid_Boolean (Val);
+
+   function Valid_Boolean (Val : RFLX.RFLX_Arithmetic.Base_Integer) return Boolean is
+     (case Val is
+         when 0 | 1 =>
+            True,
+         when others =>
+            False);
+
+   function To_Base_Integer (Enum : Boolean) return RFLX.RFLX_Arithmetic.Base_Integer is
+     (case Enum is
+         when False =>
+            0,
+         when True =>
+            1);
+
+   function To_Actual (Val : RFLX.RFLX_Arithmetic.Base_Integer) return Boolean is
+     (case Val is
+         when 0 =>
+            False,
+         when 1 =>
+            True,
+         when others =>
+            False)
+    with
+     Pre =>
+       Valid_Boolean (Val);
+
+end RFLX.RFLX_Builtin_Types.Conversions;

tests/integration/session_case_expression/generated/rflx-rflx_builtin_types.ads

@@ -0,0 +1,21 @@
+pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+
+package RFLX.RFLX_Builtin_Types with
+  SPARK_Mode
+is
+
+   type Length is new Natural;
+
+   type Index is new Length range 1 .. Length'Last;
+
+   type Byte is mod 2**8;
+
+   type Bytes is array (Index range <>) of Byte;
+
+   type Bytes_Ptr is access Bytes;
+
+   type Bit_Length is range 0 .. Length'Last * 8;
+
+   type Boolean_Base is mod 2;
+
+end RFLX.RFLX_Builtin_Types;