Fix code generation for messages with single opaque field

Ref. #888
AdaCore · Mar 25, 2022 · 72f2de8 · 72f2de8
1 parent 3254011
commit 72f2de8
Show file tree

Hide file tree

Showing 77 changed files with 3,062 additions and 109 deletions.
diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -1884,7 +1884,7 @@ def __create_field_last_function(
     ) -> UnitPart:
         specification = FunctionSpecification(
             "Field_Last",
-            const.TYPES_BIT_INDEX,
+            const.TYPES_BIT_LENGTH,
             [Parameter(["Ctx"], "Context"), Parameter(["Fld"], "Field")],
         )
 

diff --git a/tests/integration/messages/generated/rflx-universal-message.ads b/tests/integration/messages/generated/rflx-universal-message.ads
@@ -296,7 +296,7 @@ is
 
    pragma Warnings (On, "postcondition does not mention function result");
 
-   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
+   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with
      Pre =>
        Valid_Next (Ctx, Fld)
        and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
@@ -1447,7 +1447,7 @@ private
    function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
      ((if Fld = F_Message_Type then Ctx.First else Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1));
 
-   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
+   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is
      (Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field is

diff --git a/tests/integration/messages/generated/rflx-universal-option.ads b/tests/integration/messages/generated/rflx-universal-option.ads
@@ -293,7 +293,7 @@ is
 
    pragma Warnings (On, "postcondition does not mention function result");
 
-   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
+   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with
      Pre =>
        Valid_Next (Ctx, Fld)
        and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
@@ -747,7 +747,7 @@ private
    function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
      ((if Fld = F_Option_Type then Ctx.First else Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1));
 
-   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
+   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is
      (Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field is

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.ads
@@ -296,7 +296,7 @@ is
 
    pragma Warnings (On, "postcondition does not mention function result");
 
-   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
+   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with
      Pre =>
        Valid_Next (Ctx, Fld)
        and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
@@ -1447,7 +1447,7 @@ private
    function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
      ((if Fld = F_Message_Type then Ctx.First else Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1));
 
-   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
+   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is
      (Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field is

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads b/tests/integration/messages_with_implict_size/generated/rflx-universal-option.ads
@@ -293,7 +293,7 @@ is
 
    pragma Warnings (On, "postcondition does not mention function result");
 
-   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
+   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length with
      Pre =>
        Valid_Next (Ctx, Fld)
        and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
@@ -747,7 +747,7 @@ private
    function Field_First (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
      ((if Fld = F_Option_Type then Ctx.First else Ctx.Cursors (Ctx.Cursors (Fld).Predecessor).Last + 1));
 
-   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index is
+   function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Length is
      (Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field is

diff --git a/tests/integration/messages_with_single_opaque_field/config.yml b/tests/integration/messages_with_single_opaque_field/config.yml
@@ -0,0 +1,13 @@
+input:
+  Channel:
+    - 1 2 3
+output:
+  - Channel
+sequence: |
+  Write Channel: 1 2 3
+  State: Start
+  State: Process
+  Read Channel: 1 2 3
+  State: Reply
+# ISSUE: Componolit/RecordFlux#691
+# prove:
diff --git a/tests/integration/messages_with_single_opaque_field/generated/rflx-rflx_arithmetic.adb b/tests/integration/messages_with_single_opaque_field/generated/rflx-rflx_arithmetic.adb
@@ -0,0 +1,65 @@
+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;
+
+end RFLX.RFLX_Arithmetic;
diff --git a/tests/integration/messages_with_single_opaque_field/generated/rflx-rflx_arithmetic.ads b/tests/integration/messages_with_single_opaque_field/generated/rflx-rflx_arithmetic.ads
@@ -0,0 +1,85 @@
+pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+
+package RFLX.RFLX_Arithmetic with
+  SPARK_Mode
+is
+
+   type U64 is mod 2**64 with
+     Annotate => (GNATprove, No_Wrap_Around);
+
+   --  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;
+
+   --  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;
+
+end RFLX.RFLX_Arithmetic;
diff --git a/...ation/messages_with_single_opaque_field/generated/rflx-rflx_builtin_types-conversions.ads b/...ation/messages_with_single_opaque_field/generated/rflx-rflx_builtin_types-conversions.ads
@@ -0,0 +1,37 @@
+pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
+
+with RFLX.RFLX_Arithmetic;
+
+package RFLX.RFLX_Builtin_Types.Conversions with
+  SPARK_Mode
+is
+
+   pragma Annotate (GNATprove, Terminating, 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);
+
+end RFLX.RFLX_Builtin_Types.Conversions;
diff --git a/tests/integration/messages_with_single_opaque_field/generated/rflx-rflx_builtin_types.ads b/tests/integration/messages_with_single_opaque_field/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;