Optimize preconditions related to buffer index type

Ref. #548
AdaCore · Jan 14, 2021 · c040f95 · c040f95
1 parent 5846f47
commit c040f95
Show file tree

Hide file tree

Showing 31 changed files with 125 additions and 268 deletions.
diff --git a/rflx/generator/common.py b/rflx/generator/common.py
@@ -503,9 +503,7 @@ def public_context_predicate() -> ada.Expr:
             ada.Call(const.TYPES_BYTE_INDEX, [ada.Variable("Last")]), ada.Variable("Buffer_Last")
         ),
         ada.LessEqual(ada.Variable("First"), ada.Variable("Last")),
-        ada.LessEqual(
-            ada.Variable("Last"), ada.Div(ada.Last(const.TYPES_BIT_INDEX), ada.Number(2))
-        ),
+        ada.Less(ada.Variable("Last"), ada.Last(const.TYPES_BIT_INDEX)),
     )
 
 

diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -33,7 +33,6 @@
     DefaultInitialCondition,
     Depends,
     Discriminant,
-    Div,
     DynamicPredicate,
     EnumerationType,
     Equal,
@@ -55,6 +54,7 @@
     InstantiationUnit,
     Last,
     Length,
+    Less,
     LessEqual,
     Mod,
     ModularType,
@@ -663,10 +663,7 @@ def __create_initialize_procedure() -> UnitPart:
                                 Not(Constrained("Ctx")),
                                 NotEqual(Variable("Buffer"), NULL),
                                 Greater(Length("Buffer"), Number(0)),
-                                LessEqual(
-                                    Last("Buffer"),
-                                    Div(Last(const.TYPES_INDEX), Number(2)),
-                                ),
+                                Less(Last("Buffer"), Last(const.TYPES_INDEX)),
                             )
                         ),
                         Postcondition(
@@ -749,10 +746,7 @@ def __create_restricted_initialize_procedure(message: Message) -> UnitPart:
                                     Last("Buffer"),
                                 ),
                                 LessEqual(Variable("First"), Variable("Last")),
-                                LessEqual(
-                                    Variable("Last"),
-                                    Div(Last(const.TYPES_BIT_INDEX), Number(2)),
-                                ),
+                                Less(Variable("Last"), Last(const.TYPES_BIT_INDEX)),
                             )
                         ),
                         Postcondition(
@@ -1138,8 +1132,12 @@ def __create_field_last_function() -> UnitPart:
                     specification,
                     [
                         Precondition(
-                            And(
+                            AndThen(
                                 Call("Valid_Next", [Variable("Ctx"), Variable("Fld")]),
+                                GreaterEqual(
+                                    Call("Available_Space", [Variable("Ctx"), Variable("Fld")]),
+                                    Call("Field_Size", [Variable("Ctx"), Variable("Fld")]),
+                                ),
                             )
                         )
                     ],
@@ -1646,35 +1644,23 @@ def __create_sufficient_buffer_length_function() -> UnitPart:
                     ),
                     And(
                         NotEqual(Variable("Ctx.Buffer"), Variable("null")),
-                        LessEqual(
-                            Variable("Ctx.First"),
-                            Div(Last(const.TYPES_BIT_INDEX), Number(2)),
-                        ),
-                        LessEqual(
-                            Call("Field_First", [Variable("Ctx"), Variable("Fld")]),
-                            Div(Last(const.TYPES_BIT_INDEX), Number(2)),
-                        ),
                         GreaterEqual(
                             Call("Field_Size", [Variable("Ctx"), Variable("Fld")]), Number(0)
                         ),
-                        LessEqual(
-                            Call("Field_Size", [Variable("Ctx"), Variable("Fld")]),
-                            Div(Last(const.TYPES_BIT_LENGTH), Number(2)),
-                        ),
-                        LessEqual(
+                        Less(
                             Add(
                                 Call("Field_First", [Variable("Ctx"), Variable("Fld")]),
                                 Call("Field_Size", [Variable("Ctx"), Variable("Fld")]),
                             ),
-                            Div(Last(const.TYPES_BIT_LENGTH), Number(2)),
+                            Last(const.TYPES_BIT_LENGTH),
                         ),
                         LessEqual(
                             Variable("Ctx.First"),
                             Call("Field_First", [Variable("Ctx"), Variable("Fld")]),
                         ),
                         GreaterEqual(
-                            Variable("Ctx.Last"),
-                            Call("Field_Last", [Variable("Ctx"), Variable("Fld")]),
+                            Call("Available_Space", [Variable("Ctx"), Variable("Fld")]),
+                            Call("Field_Size", [Variable("Ctx"), Variable("Fld")]),
                         ),
                     ),
                     [
@@ -1815,13 +1801,6 @@ def specification(field: Field) -> ProcedureSpecification:
                                     ),
                                     Number(1),
                                 ),
-                                LessEqual(
-                                    Call(
-                                        "Field_Last",
-                                        [Variable("Ctx"), Variable(f.affixed_name)],
-                                    ),
-                                    Div(Last(const.TYPES_BIT_INDEX), Number(2)),
-                                ),
                                 Call(
                                     "Field_Condition",
                                     [

diff --git a/rflx/generator/serializer.py b/rflx/generator/serializer.py
@@ -28,7 +28,6 @@
     In,
     Indexed,
     InOutParameter,
-    Last,
     LessEqual,
     Mod,
     NamedAggregate,
@@ -682,10 +681,6 @@ def setter_preconditions(field: Field) -> Sequence[Expr]:
             Not(Constrained("Ctx")),
             Call("Has_Buffer", [Variable("Ctx")]),
             Call("Valid_Next", [Variable("Ctx"), Variable(field.affixed_name)]),
-            LessEqual(
-                Call("Field_Last", [Variable("Ctx"), Variable(field.affixed_name)]),
-                Div(Last(const.TYPES_BIT_INDEX), Number(2)),
-            ),
         ]
 
     @staticmethod

diff --git a/rflx/templates/rflx_message_sequence.ads b/rflx/templates/rflx_message_sequence.ads
@@ -26,14 +26,14 @@ is
        and Types.Byte_Index (Last) <= Buffer_Last
        and First mod Types.Byte'Size = 1
        and First <= Last
-       and Last <= Types.Bit_Index'Last / 2;
+       and Last <= Types.Bit_Index'Last - 1;
 
    procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr) with
      Pre =>
        (not Ctx'Constrained
         and then Buffer /= null
         and then Buffer'Length > 0
-        and then Buffer'Last <= Types.Index'Last / 2),
+        and then Buffer'Last < Types.Index'Last),
      Post =>
        (Has_Buffer (Ctx)
         and Valid (Ctx)
@@ -56,7 +56,7 @@ is
         and then Types.Byte_Index (Last) <= Buffer'Last
         and then First mod Types.Byte'Size = 1
         and then First <= Last
-        and then Last <= Types.Bit_Index'Last / 2),
+        and then Last <= Types.Bit_Index'Last - 1),
      Post =>
        (Buffer = null
         and Has_Buffer (Ctx)
@@ -185,7 +185,7 @@ private
         and Types.Byte_Index (Last) <= Buffer_Last
         and First mod Types.Byte'Size = 1
         and First <= Last
-        and Last <= (Types.Bit_Index'Last / 2)
+        and Last <= Types.Bit_Index'Last - 1
         and Sequence_Last >= First - 1
         and Sequence_Last <= Last);
 

diff --git a/rflx/templates/rflx_scalar_sequence.ads b/rflx/templates/rflx_scalar_sequence.ads
@@ -22,14 +22,14 @@ is
        and Types.Byte_Index (Last) <= Buffer_Last
        and First mod Types.Byte'Size = 1
        and First <= Last
-       and Last <= Types.Bit_Index'Last / 2;
+       and Last <= Types.Bit_Index'Last - 1;
 
    procedure Initialize (Ctx : out Context; Buffer : in out Types.Bytes_Ptr) with
      Pre =>
        (not Ctx'Constrained
         and then Buffer /= null
         and then Buffer'Length > 0
-        and then Buffer'Last <= Types.Index'Last / 2),
+        and then Buffer'Last < Types.Index'Last),
      Post =>
        (Has_Buffer (Ctx)
         and Valid (Ctx)
@@ -52,7 +52,7 @@ is
         and then Types.Byte_Index (Last) <= Buffer'Last
         and then First mod Types.Byte'Size = 1
         and then First <= Last
-        and then Last <= Types.Bit_Index'Last / 2),
+        and then Last <= Types.Bit_Index'Last - 1),
      Post =>
        (Buffer = null
         and Has_Buffer (Ctx)
@@ -169,7 +169,7 @@ private
         and Types.Byte_Index (Last) <= Buffer_Last
         and First mod Types.Byte'Size = 1
         and First <= Last
-        and Last <= (Types.Bit_Index'Last / 2)
+        and Last <= Types.Bit_Index'Last - 1
         and Sequence_Last >= First - 1
         and Sequence_Last <= Last);
 

diff --git a/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.adb b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.adb
@@ -140,13 +140,10 @@ is
 
    function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is
      (Ctx.Buffer /= null
-      and Ctx.First <= Types.Bit_Index'Last / 2
-      and Field_First (Ctx, Fld) <= Types.Bit_Index'Last / 2
       and Field_Size (Ctx, Fld) >= 0
-      and Field_Size (Ctx, Fld) <= Types.Bit_Length'Last / 2
-      and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) <= Types.Bit_Length'Last / 2
+      and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) < Types.Bit_Length'Last
       and Ctx.First <= Field_First (Ctx, Fld)
-      and Ctx.Last >= Field_Last (Ctx, Fld))
+      and Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld))
     with
      Pre =>
        Has_Buffer (Ctx)

diff --git a/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.ads b/tests/spark/generated/rflx-arrays-generic_array_size_defined_by_message_size.ads
@@ -35,7 +35,7 @@ is
        Types.Byte_Index (First) >= Buffer_First
        and Types.Byte_Index (Last) <= Buffer_Last
        and First <= Last
-       and Last <= Types.Bit_Index'Last / 2;
+       and Last < Types.Bit_Index'Last;
 
    type Field_Dependent_Value (Fld : Virtual_Field := F_Initial) is
       record
@@ -52,7 +52,7 @@ is
        not Ctx'Constrained
        and then Buffer /= null
        and then Buffer'Length > 0
-       and then Buffer'Last <= Types.Index'Last / 2,
+       and then Buffer'Last < Types.Index'Last,
      Post =>
        Has_Buffer (Ctx)
        and Buffer = null
@@ -73,7 +73,7 @@ is
        and then Types.Byte_Index (First) >= Buffer'First
        and then Types.Byte_Index (Last) <= Buffer'Last
        and then First <= Last
-       and then Last <= Types.Bit_Index'Last / 2,
+       and then Last < Types.Bit_Index'Last,
      Post =>
        Buffer = null
        and Has_Buffer (Ctx)
@@ -129,7 +129,8 @@ is
 
    function Field_Last (Ctx : Context; Fld : Field) return Types.Bit_Index with
      Pre =>
-       Valid_Next (Ctx, Fld);
+       Valid_Next (Ctx, Fld)
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 
@@ -204,7 +205,6 @@ is
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
        and then Valid_Next (Ctx, F_Header)
-       and then Field_Last (Ctx, F_Header) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (F_Header, To_Base (Val)))
        and then True
        and then Available_Space (Ctx, F_Header) >= Field_Size (Ctx, F_Header),
@@ -228,7 +228,6 @@ is
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
        and then Valid_Next (Ctx, F_Vector)
-       and then Field_Last (Ctx, F_Vector) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Vector))
        and then Available_Space (Ctx, F_Vector) >= Field_Size (Ctx, F_Vector)
        and then Field_First (Ctx, F_Vector) mod Types.Byte'Size = 1
@@ -251,7 +250,6 @@ is
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
        and then Valid_Next (Ctx, F_Vector)
-       and then Field_Last (Ctx, F_Vector) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Vector))
        and then Available_Space (Ctx, F_Vector) >= Field_Size (Ctx, F_Vector)
        and then Field_First (Ctx, F_Vector) mod Types.Byte'Size = 1
@@ -283,7 +281,6 @@ is
        and then Valid_Next (Ctx, F_Vector)
        and then Field_Size (Ctx, F_Vector) > 0
        and then Field_First (Ctx, F_Vector) mod Types.Byte'Size = 1
-       and then Field_Last (Ctx, F_Vector) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Vector))
        and then Available_Space (Ctx, F_Vector) >= Field_Size (Ctx, F_Vector),
      Post =>
@@ -403,7 +400,7 @@ private
       and then (Types.Byte_Index (First) >= Buffer_First
                 and Types.Byte_Index (Last) <= Buffer_Last
                 and First <= Last
-                and Last <= Types.Bit_Index'Last / 2)
+                and Last < Types.Bit_Index'Last)
       and then First <= Message_Last
       and then Message_Last <= Last
       and then (for all F in Field'First .. Field'Last =>

diff --git a/tests/spark/generated/rflx-arrays-generic_inner_message.adb b/tests/spark/generated/rflx-arrays-generic_inner_message.adb
@@ -140,13 +140,10 @@ is
 
    function Sufficient_Buffer_Length (Ctx : Context; Fld : Field) return Boolean is
      (Ctx.Buffer /= null
-      and Ctx.First <= Types.Bit_Index'Last / 2
-      and Field_First (Ctx, Fld) <= Types.Bit_Index'Last / 2
       and Field_Size (Ctx, Fld) >= 0
-      and Field_Size (Ctx, Fld) <= Types.Bit_Length'Last / 2
-      and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) <= Types.Bit_Length'Last / 2
+      and Field_First (Ctx, Fld) + Field_Size (Ctx, Fld) < Types.Bit_Length'Last
       and Ctx.First <= Field_First (Ctx, Fld)
-      and Ctx.Last >= Field_Last (Ctx, Fld))
+      and Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld))
     with
      Pre =>
        Has_Buffer (Ctx)

diff --git a/tests/spark/generated/rflx-arrays-generic_inner_message.ads b/tests/spark/generated/rflx-arrays-generic_inner_message.ads
@@ -33,7 +33,7 @@ is
        Types.Byte_Index (First) >= Buffer_First
        and Types.Byte_Index (Last) <= Buffer_Last
        and First <= Last
-       and Last <= Types.Bit_Index'Last / 2;
+       and Last < Types.Bit_Index'Last;
 
    type Field_Dependent_Value (Fld : Virtual_Field := F_Initial) is
       record
@@ -50,7 +50,7 @@ is
        not Ctx'Constrained
        and then Buffer /= null
        and then Buffer'Length > 0
-       and then Buffer'Last <= Types.Index'Last / 2,
+       and then Buffer'Last < Types.Index'Last,
      Post =>
        Has_Buffer (Ctx)
        and Buffer = null
@@ -71,7 +71,7 @@ is
        and then Types.Byte_Index (First) >= Buffer'First
        and then Types.Byte_Index (Last) <= Buffer'Last
        and then First <= Last
-       and then Last <= Types.Bit_Index'Last / 2,
+       and then Last < Types.Bit_Index'Last,
      Post =>
        Buffer = null
        and Has_Buffer (Ctx)
@@ -127,7 +127,8 @@ is
 
    function Field_Last (Ctx : Context; Fld : Field) return Types.Bit_Index with
      Pre =>
-       Valid_Next (Ctx, Fld);
+       Valid_Next (Ctx, Fld)
+       and then Available_Space (Ctx, Fld) >= Field_Size (Ctx, Fld);
 
    function Predecessor (Ctx : Context; Fld : Virtual_Field) return Virtual_Field;
 
@@ -202,7 +203,6 @@ is
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
        and then Valid_Next (Ctx, F_Length)
-       and then Field_Last (Ctx, F_Length) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (F_Length, To_Base (Val)))
        and then Valid (To_Base (Val))
        and then Available_Space (Ctx, F_Length) >= Field_Size (Ctx, F_Length),
@@ -226,7 +226,6 @@ is
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
        and then Valid_Next (Ctx, F_Payload)
-       and then Field_Last (Ctx, F_Payload) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Payload))
        and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload)
        and then Field_First (Ctx, F_Payload) mod Types.Byte'Size = 1
@@ -252,7 +251,6 @@ is
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
        and then Valid_Next (Ctx, F_Payload)
-       and then Field_Last (Ctx, F_Payload) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Payload))
        and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload)
        and then Field_First (Ctx, F_Payload) mod Types.Byte'Size = 1
@@ -275,7 +273,6 @@ is
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
        and then Valid_Next (Ctx, F_Payload)
-       and then Field_Last (Ctx, F_Payload) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Payload))
        and then Available_Space (Ctx, F_Payload) >= Field_Size (Ctx, F_Payload)
        and then Field_First (Ctx, F_Payload) mod Types.Byte'Size = 1
@@ -356,7 +353,7 @@ private
       and then (Types.Byte_Index (First) >= Buffer_First
                 and Types.Byte_Index (Last) <= Buffer_Last
                 and First <= Last
-                and Last <= Types.Bit_Index'Last / 2)
+                and Last < Types.Bit_Index'Last)
       and then First <= Message_Last
       and then Message_Last <= Last
       and then (for all F in Field'First .. Field'Last =>