Improve testing of code generator

Ref. eng/recordflux/RecordFlux#1496
AdaCore · Apr 12, 2024 · 21cd11a · 21cd11a
1 parent b650505
commit 21cd11a
Show file tree

Hide file tree

Showing 23 changed files with 2,971 additions and 9 deletions.
diff --git a/Makefile b/Makefile
@@ -332,7 +332,7 @@ test_property: $(RFLX)
 	$(PYTEST) tests/property
 
 test_tools: $(RFLX)
-	$(PYTEST) --cov=tools --cov-branch --cov-fail-under=43.6 --cov-report=term-missing:skip-covered tests/tools
+	$(PYTEST) --cov=tools --cov-branch --cov-fail-under=60.0 --cov-report=term-missing:skip-covered tests/tools
 
 test_ide: $(RFLX)
 	$(PYTEST) tests/ide

diff --git a/tests/compilation/generator_test.py b/tests/compilation/generator_test.py
@@ -0,0 +1,11 @@
+from pathlib import Path
+
+import pytest
+
+from tests.unit.generator.generator_test import GENERATOR_TEST_CASES, TC
+from tests.utils import assert_compilable_code
+
+
+@pytest.mark.parametrize("tc", GENERATOR_TEST_CASES)
+def test_compilability(tc: TC, tmp_path: Path) -> None:
+    assert_compilable_code(tc.model(), tc.integration(), tmp_path)
diff --git a/tests/data/generator/generated/boolean_variable/rflx-p-message.adb b/tests/data/generator/generated/boolean_variable/rflx-p-message.adb
@@ -0,0 +1,291 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         Generated by RecordFlux                          --
+--                                                                          --
+--                        Copyright (C) AdaCore GmbH                        --
+--                                                                          --
+--                   SPDX-License-Identifier: Apache-2.0                    --
+--                                                                          --
+------------------------------------------------------------------------------
+
+pragma Ada_2012;
+pragma Style_Checks ("N3aAbCdefhiIklnOprStux");
+pragma Warnings (Off, "redundant conversion");
+with RFLX.RFLX_Types.Operations;
+
+package body RFLX.P.Message with
+  SPARK_Mode
+is
+
+   pragma Unevaluated_Use_Of_Old (Allow);
+
+   procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; Written_Last : RFLX_Types.Bit_Length := 0) is
+   begin
+      Initialize (Ctx, Buffer, RFLX_Types.To_First_Bit_Index (Buffer'First), RFLX_Types.To_Last_Bit_Index (Buffer'Last), Written_Last);
+   end Initialize;
+
+   procedure Initialize (Ctx : out Context; Buffer : in out RFLX_Types.Bytes_Ptr; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length; Written_Last : RFLX_Types.Bit_Length := 0) is
+      Buffer_First : constant RFLX_Types.Index := Buffer'First;
+      Buffer_Last : constant RFLX_Types.Index := Buffer'Last;
+   begin
+      Ctx := (Buffer_First, Buffer_Last, First, Last, First - 1, (if Written_Last = 0 then First - 1 else Written_Last), Buffer, (F_A => (State => S_Invalid, others => <>), others => <>));
+      Buffer := null;
+   end Initialize;
+
+   procedure Reset (Ctx : in out Context) is
+   begin
+      Reset (Ctx, RFLX_Types.To_First_Bit_Index (Ctx.Buffer'First), RFLX_Types.To_Last_Bit_Index (Ctx.Buffer'Last));
+   end Reset;
+
+   procedure Reset (Ctx : in out Context; First : RFLX_Types.Bit_Index; Last : RFLX_Types.Bit_Length) is
+   begin
+      Ctx := (Ctx.Buffer_First, Ctx.Buffer_Last, First, Last, First - 1, First - 1, Ctx.Buffer, (F_A => (State => S_Invalid, others => <>), others => <>));
+   end Reset;
+
+   procedure Take_Buffer (Ctx : in out Context; Buffer : out RFLX_Types.Bytes_Ptr) is
+   begin
+      Buffer := Ctx.Buffer;
+      Ctx.Buffer := null;
+   end Take_Buffer;
+
+   procedure Copy (Ctx : Context; Buffer : out RFLX_Types.Bytes) is
+   begin
+      if Buffer'Length > 0 then
+         Buffer := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));
+      else
+         Buffer := Ctx.Buffer.all (1 .. 0);
+      end if;
+   end Copy;
+
+   procedure Generic_Read (Ctx : Context) is
+   begin
+      Read (Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last)));
+   end Generic_Read;
+
+   procedure Generic_Write (Ctx : in out Context; Offset : RFLX_Types.Length := 0) is
+      Length : RFLX_Types.Length;
+   begin
+      Reset (Ctx, RFLX_Types.To_First_Bit_Index (Ctx.Buffer_First), RFLX_Types.To_Last_Bit_Index (Ctx.Buffer_Last));
+      Write (Ctx.Buffer.all (Ctx.Buffer'First + RFLX_Types.Index (Offset + 1) - 1 .. Ctx.Buffer'Last), Length, Ctx.Buffer'Length, Offset);
+      pragma Assert (Length <= Ctx.Buffer.all'Length, "Length <= Buffer'Length is not ensured by postcondition of ""Write""");
+      Ctx.Written_Last := RFLX_Types.Bit_Index'Max (Ctx.Written_Last, RFLX_Types.To_Last_Bit_Index (RFLX_Types.Length (Ctx.Buffer_First) + Offset + Length - 1));
+   end Generic_Write;
+
+   procedure Data (Ctx : Context; Data : out RFLX_Types.Bytes) is
+   begin
+      Data := Ctx.Buffer.all (RFLX_Types.To_Index (Ctx.First) .. RFLX_Types.To_Index (Ctx.Verified_Last));
+   end Data;
+
+   function Invalid_Successor (Ctx : Context; Fld : Field) return Boolean is
+     ((case Fld is
+          when F_A =>
+             Invalid (Ctx.Cursors (F_B)),
+          when F_B =>
+             True));
+
+   function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is
+     (Ctx.Buffer /= null
+      and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) < RFLX_Types.Bit_Length'Last
+      and Ctx.First <= Field_First (Ctx, Fld)
+      and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) - 1 <= Ctx.Written_Last)
+    with
+     Pre =>
+       RFLX.P.Message.Has_Buffer (Ctx)
+       and RFLX.P.Message.Valid_Next (Ctx, Fld);
+
+   procedure Reset_Dependent_Fields (Ctx : in out Context; Fld : Field) with
+     Pre =>
+       RFLX.P.Message.Valid_Next (Ctx, Fld),
+     Post =>
+       Valid_Next (Ctx, Fld)
+       and Ctx.Buffer_First = Ctx.Buffer_First'Old
+       and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
+       and Ctx.First = Ctx.First'Old
+       and Ctx.Last = Ctx.Last'Old
+       and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old
+       and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old
+       and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Old
+       and (for all F in Field =>
+               (if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F) else Invalid (Ctx, F)))
+   is
+   begin
+      for Fld_Loop in reverse Fld .. Field'Last loop
+         pragma Loop_Invariant (Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Loop_Entry
+                                and Field_Size (Ctx, Fld) = Field_Size (Ctx, Fld)'Loop_Entry);
+         pragma Loop_Invariant ((for all F in Field =>
+                                    (if F <= Fld_Loop then Ctx.Cursors (F) = Ctx.Cursors'Loop_Entry (F) else Invalid (Ctx, F))));
+         Ctx.Cursors (Fld_Loop) := (State => S_Invalid, others => <>);
+      end loop;
+   end Reset_Dependent_Fields;
+
+   function Get (Ctx : Context; Fld : Field) return RFLX_Types.Base_Integer with
+     Pre =>
+       RFLX.P.Message.Has_Buffer (Ctx)
+       and then RFLX.P.Message.Valid_Next (Ctx, Fld)
+       and then RFLX.P.Message.Sufficient_Buffer_Length (Ctx, Fld)
+   is
+      First : constant RFLX_Types.Bit_Index := Field_First (Ctx, Fld);
+      Last : constant RFLX_Types.Bit_Index := Field_Last (Ctx, Fld);
+      Buffer_First : constant RFLX_Types.Index := RFLX_Types.To_Index (First);
+      Buffer_Last : constant RFLX_Types.Index := RFLX_Types.To_Index (Last);
+      Offset : constant RFLX_Types.Offset := RFLX_Types.Offset ((RFLX_Types.Byte'Size - Last mod RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size);
+      Size : constant Positive := (case Fld is
+          when F_A =>
+             1,
+          when F_B =>
+             7);
+      Byte_Order : constant RFLX_Types.Byte_Order := RFLX_Types.High_Order_First;
+   begin
+      return RFLX_Types.Operations.Extract (Ctx.Buffer.all, Buffer_First, Buffer_Last, Offset, Size, Byte_Order);
+   end Get;
+
+   procedure Verify (Ctx : in out Context; Fld : Field) is
+      Value : RFLX_Types.Base_Integer;
+   begin
+      if
+         Invalid (Ctx.Cursors (Fld))
+         and then Valid_Next (Ctx, Fld)
+      then
+         if Sufficient_Buffer_Length (Ctx, Fld) then
+            Value := Get (Ctx, Fld);
+            if
+               Valid_Value (Fld, Value)
+               and then Field_Condition (Ctx, Fld, Value)
+            then
+               pragma Assert ((if Fld = F_B then Field_Last (Ctx, Fld) mod RFLX_Types.Byte'Size = 0));
+               pragma Assert ((((Field_Last (Ctx, Fld) + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size = 0);
+               Ctx.Verified_Last := ((Field_Last (Ctx, Fld) + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size;
+               pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last);
+               Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value);
+            else
+               Ctx.Cursors (Fld) := (others => <>);
+            end if;
+         else
+            Ctx.Cursors (Fld) := (State => S_Incomplete, others => <>);
+         end if;
+      end if;
+   end Verify;
+
+   procedure Verify_Message (Ctx : in out Context) is
+   begin
+      for F in Field loop
+         pragma Loop_Invariant (Has_Buffer (Ctx)
+                                and Ctx.Buffer_First = Ctx.Buffer_First'Loop_Entry
+                                and Ctx.Buffer_Last = Ctx.Buffer_Last'Loop_Entry
+                                and Ctx.First = Ctx.First'Loop_Entry
+                                and Ctx.Last = Ctx.Last'Loop_Entry);
+         Verify (Ctx, F);
+      end loop;
+   end Verify_Message;
+
+   procedure Set (Ctx : in out Context; Fld : Field; Val : RFLX_Types.Base_Integer; Size : RFLX_Types.Bit_Length; State_Valid : Boolean; Buffer_First : out RFLX_Types.Index; Buffer_Last : out RFLX_Types.Index; Offset : out RFLX_Types.Offset) with
+     Pre =>
+       RFLX.P.Message.Has_Buffer (Ctx)
+       and then RFLX.P.Message.Valid_Next (Ctx, Fld)
+       and then RFLX.P.Message.Valid_Value (Fld, Val)
+       and then RFLX.P.Message.Valid_Size (Ctx, Fld, Size)
+       and then Size <= RFLX.P.Message.Available_Space (Ctx, Fld)
+       and then State_Valid,
+     Post =>
+       Valid_Next (Ctx, Fld)
+       and then Invalid_Successor (Ctx, Fld)
+       and then Buffer_First = RFLX_Types.To_Index (Field_First (Ctx, Fld))
+       and then Buffer_Last = RFLX_Types.To_Index (Field_First (Ctx, Fld) + Size - 1)
+       and then Offset = RFLX_Types.Offset ((RFLX_Types.Byte'Size - (Field_First (Ctx, Fld) + Size - 1) mod RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size)
+       and then Ctx.Buffer_First = Ctx.Buffer_First'Old
+       and then Ctx.Buffer_Last = Ctx.Buffer_Last'Old
+       and then Ctx.First = Ctx.First'Old
+       and then Ctx.Last = Ctx.Last'Old
+       and then Ctx.Buffer_First = Ctx.Buffer_First'Old
+       and then Ctx.Buffer_Last = Ctx.Buffer_Last'Old
+       and then Ctx.First = Ctx.First'Old
+       and then Ctx.Last = Ctx.Last'Old
+       and then Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old
+       and then Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old
+       and then Sufficient_Space (Ctx, Fld)
+       and then (if State_Valid and Size > 0 then Valid (Ctx, Fld) else Well_Formed (Ctx, Fld))
+       and then (Ctx.Cursors (Fld).Value = Val
+                 and then (if Fld in F_B and then Well_Formed_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, Fld)))
+       and then (for all F in Field =>
+                    (if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F)))
+   is
+      First : RFLX_Types.Bit_Index;
+      Last : RFLX_Types.Bit_Length;
+   begin
+      Reset_Dependent_Fields (Ctx, Fld);
+      First := Field_First (Ctx, Fld);
+      Last := Field_First (Ctx, Fld) + Size - 1;
+      Offset := RFLX_Types.Offset ((RFLX_Types.Byte'Size - Last mod RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size);
+      Buffer_First := RFLX_Types.To_Index (First);
+      Buffer_Last := RFLX_Types.To_Index (Last);
+      pragma Assert ((((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size) mod RFLX_Types.Byte'Size = 0);
+      pragma Warnings (Off, "attribute Update is an obsolescent feature");
+      Ctx := Ctx'Update (Verified_Last => ((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size, Written_Last => ((Last + RFLX_Types.Byte'Size - 1) / RFLX_Types.Byte'Size) * RFLX_Types.Byte'Size);
+      pragma Warnings (On, "attribute Update is an obsolescent feature");
+      if State_Valid then
+         Ctx.Cursors (Fld) := (State => S_Valid, First => First, Last => Last, Value => Val);
+      else
+         Ctx.Cursors (Fld) := (State => S_Well_Formed, First => First, Last => Last, Value => Val);
+      end if;
+      pragma Assert (Last = (Field_First (Ctx, Fld) + Size) - 1);
+   end Set;
+
+   procedure Set_Scalar (Ctx : in out Context; Fld : Field; Val : RFLX_Types.Base_Integer) with
+     Pre =>
+       not Ctx'Constrained
+       and then RFLX.P.Message.Has_Buffer (Ctx)
+       and then RFLX.P.Message.Valid_Next (Ctx, Fld)
+       and then Fld in F_A | F_B
+       and then RFLX.P.Message.Valid_Value (Fld, Val)
+       and then RFLX.P.Message.Valid_Size (Ctx, Fld, RFLX.P.Message.Field_Size (Ctx, Fld))
+       and then RFLX.P.Message.Available_Space (Ctx, Fld) >= RFLX.P.Message.Field_Size (Ctx, Fld)
+       and then RFLX.P.Message.Field_Size (Ctx, Fld) in 1 .. RFLX_Types.Base_Integer'Size
+       and then RFLX_Types.Fits_Into (Val, Natural (RFLX.P.Message.Field_Size (Ctx, Fld))),
+     Post =>
+       Has_Buffer (Ctx)
+       and Valid (Ctx, Fld)
+       and Invalid_Successor (Ctx, Fld)
+       and (Ctx.Cursors (Fld).Value = Val
+            and then (if Fld in F_B and then Well_Formed_Message (Ctx) then Message_Last (Ctx) = Field_Last (Ctx, Fld)))
+       and (for all F in Field =>
+               (if F < Fld then Ctx.Cursors (F) = Ctx.Cursors'Old (F)))
+       and Ctx.Buffer_First = Ctx.Buffer_First'Old
+       and Ctx.Buffer_Last = Ctx.Buffer_Last'Old
+       and Ctx.First = Ctx.First'Old
+       and Ctx.Last = Ctx.Last'Old
+       and Has_Buffer (Ctx) = Has_Buffer (Ctx)'Old
+       and Field_First (Ctx, Fld) = Field_First (Ctx, Fld)'Old
+   is
+      Buffer_First, Buffer_Last : RFLX_Types.Index;
+      Offset : RFLX_Types.Offset;
+      Size : constant RFLX_Types.Bit_Length := Field_Size (Ctx, Fld);
+   begin
+      Set (Ctx, Fld, Val, Size, True, Buffer_First, Buffer_Last, Offset);
+      RFLX_Types.Lemma_Size (Val, Positive (Size));
+      RFLX_Types.Operations.Insert (Val, Ctx.Buffer.all, Buffer_First, Buffer_Last, Offset, Positive (Size), RFLX_Types.High_Order_First);
+   end Set_Scalar;
+
+   procedure Set_A (Ctx : in out Context; Val : Boolean) is
+   begin
+      Set_Scalar (Ctx, F_A, To_Base_Integer (Val));
+   end Set_A;
+
+   procedure Set_B (Ctx : in out Context; Val : RFLX.P.T) is
+   begin
+      Set_Scalar (Ctx, F_B, RFLX.P.To_Base_Integer (Val));
+   end Set_B;
+
+   procedure To_Structure (Ctx : Context; Struct : out Structure) is
+   begin
+      Struct.A := Get_A (Ctx);
+      Struct.B := Get_B (Ctx);
+   end To_Structure;
+
+   procedure To_Context (Struct : Structure; Ctx : in out Context) is
+   begin
+      Reset (Ctx);
+      Set_A (Ctx, Struct.A);
+      Set_B (Ctx, Struct.B);
+   end To_Context;
+
+end RFLX.P.Message;