Improve provability

Ref. #736
AdaCore · Jan 3, 2022 · 0e17ad2 · 0e17ad2
1 parent 4326eb3
commit 0e17ad2
Show file tree

Hide file tree

Showing 68 changed files with 607 additions and 70 deletions.
diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -403,7 +403,7 @@ def __create_message(self, message: Message) -> None:
         unit += self.__create_field_condition_function(message)
         unit += self.__create_field_size_function(message, scalar_fields, composite_fields)
         unit += self.__create_field_first_function(message)
-        unit += self.__create_field_last_function()
+        unit += self.__create_field_last_function(scalar_fields, composite_fields)
         unit += self.__create_predecessor_function()
         unit += self.__create_successor_function(message)
         unit += self.__create_valid_predecessor_function(message, composite_fields)
@@ -1891,7 +1891,9 @@ def substituted(
         )
 
     @staticmethod
-    def __create_field_last_function() -> UnitPart:
+    def __create_field_last_function(
+        scalar_fields: ty.Mapping[Field, Type], composite_fields: ty.Sequence[Field]
+    ) -> UnitPart:
         specification = FunctionSpecification(
             "Field_Last",
             const.TYPES_BIT_INDEX,
@@ -1911,7 +1913,38 @@ def __create_field_last_function() -> UnitPart:
                                     Call("Field_Size", [Variable("Ctx"), Variable("Fld")]),
                                 ),
                             )
-                        )
+                        ),
+                        *(
+                            [
+                                Postcondition(
+                                    Case(
+                                        Variable("Fld"),
+                                        [
+                                            *[
+                                                (
+                                                    Variable(f.affixed_name),
+                                                    Equal(
+                                                        Mod(
+                                                            Result("Field_Last"),
+                                                            Size(const.TYPES_BYTE),
+                                                        ),
+                                                        Number(0),
+                                                    ),
+                                                )
+                                                for f in composite_fields
+                                            ],
+                                            *(
+                                                [(Variable("others"), TRUE)]
+                                                if scalar_fields
+                                                else []
+                                            ),
+                                        ],
+                                    )
+                                )
+                            ]
+                            if composite_fields
+                            else []
+                        ),
                     ],
                 )
             ],

diff --git a/rflx/generator/parser.py b/rflx/generator/parser.py
@@ -34,6 +34,7 @@
     Mod,
     Mul,
     NamedAggregate,
+    NullStatement,
     Number,
     ObjectDeclaration,
     Old,
@@ -310,7 +311,32 @@ def create_verify_procedure(
                 [
                     (
                         Call("Composite_Field", [Variable("Fld")]),
-                        [set_context_cursor_composite_field("Fld")],
+                        # Componolit/RecordFlux#664
+                        # The provability of the context predicate is increased by duplicating
+                        # the statement inside a case statement. Not required for versions newer
+                        # than SPARK Community 2021.
+                        [
+                            CaseStatement(
+                                Variable("Fld"),
+                                [
+                                    *[
+                                        (
+                                            Variable(f.affixed_name),
+                                            [set_context_cursor_composite_field(f.affixed_name)],
+                                        )
+                                        for f in composite_fields
+                                    ],
+                                    *(
+                                        [(Variable("others"), [NullStatement()])]
+                                        if scalar_fields
+                                        else []
+                                    ),
+                                ],
+                                case_grouping=False,
+                            )
+                        ]
+                        if len(composite_fields) > 1
+                        else [set_context_cursor_composite_field("Fld")],
                     )
                 ],
                 [set_context_cursor_scalar()],

diff --git a/tests/integration/messages/generated/rflx-universal-message.adb b/tests/integration/messages/generated/rflx-universal-message.adb
@@ -292,7 +292,18 @@ is
                end case;
                pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last);
                if Composite_Field (Fld) then
-                  Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
+                  case Fld is
+                     when F_Data =>
+                        Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor);
+                     when F_Option_Types =>
+                        Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor);
+                     when F_Options =>
+                        Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor);
+                     when F_Values =>
+                        Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor);
+                     when others =>
+                        null;
+                  end case;
                else
                   Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
                end if;

diff --git a/tests/integration/messages/generated/rflx-universal-message.ads b/tests/integration/messages/generated/rflx-universal-message.ads
@@ -269,7 +269,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data | F_Option_Types | F_Options | F_Values =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

diff --git a/tests/integration/messages/generated/rflx-universal-option.ads b/tests/integration/messages/generated/rflx-universal-option.ads
@@ -264,7 +264,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

diff --git a/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb b/tests/integration/messages_with_implict_size/generated/rflx-universal-message.adb
@@ -292,7 +292,18 @@ is
                end case;
                pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last);
                if Composite_Field (Fld) then
-                  Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
+                  case Fld is
+                     when F_Data =>
+                        Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor);
+                     when F_Option_Types =>
+                        Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor);
+                     when F_Options =>
+                        Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor);
+                     when F_Values =>
+                        Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor);
+                     when others =>
+                        null;
+                  end case;
                else
                   Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
                end if;

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
@@ -269,7 +269,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data | F_Option_Types | F_Options | F_Values =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

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
@@ -264,7 +264,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

diff --git a/tests/integration/parameterized_messages/generated/rflx-test-message.ads b/tests/integration/parameterized_messages/generated/rflx-test-message.ads
@@ -271,7 +271,11 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data | F_Extension =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.adb b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.adb
@@ -292,7 +292,18 @@ is
                end case;
                pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last);
                if Composite_Field (Fld) then
-                  Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
+                  case Fld is
+                     when F_Data =>
+                        Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor);
+                     when F_Option_Types =>
+                        Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor);
+                     when F_Options =>
+                        Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor);
+                     when F_Values =>
+                        Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor);
+                     when others =>
+                        null;
+                  end case;
                else
                   Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
                end if;

diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads b/tests/integration/session_append_unconstrained/generated/rflx-universal-message.ads
@@ -269,7 +269,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data | F_Option_Types | F_Options | F_Values =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

diff --git a/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads b/tests/integration/session_append_unconstrained/generated/rflx-universal-option.ads
@@ -264,7 +264,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

diff --git a/tests/integration/session_binding/generated/rflx-universal-message.adb b/tests/integration/session_binding/generated/rflx-universal-message.adb
@@ -292,7 +292,18 @@ is
                end case;
                pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last);
                if Composite_Field (Fld) then
-                  Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
+                  case Fld is
+                     when F_Data =>
+                        Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor);
+                     when F_Option_Types =>
+                        Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor);
+                     when F_Options =>
+                        Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor);
+                     when F_Values =>
+                        Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor);
+                     when others =>
+                        null;
+                  end case;
                else
                   Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
                end if;

diff --git a/tests/integration/session_binding/generated/rflx-universal-message.ads b/tests/integration/session_binding/generated/rflx-universal-message.ads
@@ -269,7 +269,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data | F_Option_Types | F_Options | F_Values =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

diff --git a/tests/integration/session_binding/generated/rflx-universal-option.ads b/tests/integration/session_binding/generated/rflx-universal-option.ads
@@ -264,7 +264,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.adb b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.adb
@@ -292,7 +292,18 @@ is
                end case;
                pragma Assert (Field_Last (Ctx, Fld) <= Ctx.Verified_Last);
                if Composite_Field (Fld) then
-                  Ctx.Cursors (Fld) := (State => S_Structural_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
+                  case Fld is
+                     when F_Data =>
+                        Ctx.Cursors (F_Data) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Data), Last => Field_Last (Ctx, F_Data), Value => Value, Predecessor => Ctx.Cursors (F_Data).Predecessor);
+                     when F_Option_Types =>
+                        Ctx.Cursors (F_Option_Types) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Option_Types), Last => Field_Last (Ctx, F_Option_Types), Value => Value, Predecessor => Ctx.Cursors (F_Option_Types).Predecessor);
+                     when F_Options =>
+                        Ctx.Cursors (F_Options) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Options), Last => Field_Last (Ctx, F_Options), Value => Value, Predecessor => Ctx.Cursors (F_Options).Predecessor);
+                     when F_Values =>
+                        Ctx.Cursors (F_Values) := (State => S_Structural_Valid, First => Field_First (Ctx, F_Values), Last => Field_Last (Ctx, F_Values), Value => Value, Predecessor => Ctx.Cursors (F_Values).Predecessor);
+                     when others =>
+                        null;
+                  end case;
                else
                   Ctx.Cursors (Fld) := (State => S_Valid, First => Field_First (Ctx, Fld), Last => Field_Last (Ctx, Fld), Value => Value, Predecessor => Ctx.Cursors (Fld).Predecessor);
                end if;

diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads b/tests/integration/session_channel_multiplexing/generated/rflx-universal-message.ads
@@ -269,7 +269,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data | F_Option_Types | F_Options | F_Values =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 

diff --git a/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads b/tests/integration/session_channel_multiplexing/generated/rflx-universal-option.ads
@@ -264,7 +264,13 @@ is
    function Field_Last (Ctx : Context; Fld : Field) return RFLX_Types.Bit_Index with
      Pre =>
        Valid_Next (Ctx, Fld)
-       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld),
+     Post =>
+       (case Fld is
+           when F_Data =>
+              Field_Last'Result mod RFLX_Types.Byte'Size = 0,
+           when others =>
+              True);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;