Allow proving length properties in composite setters

ref #287
AdaCore · Jun 17, 2020 · 05c61a3 · 05c61a3
1 parent 818243b
commit 05c61a3
Show file tree

Hide file tree

Showing 16 changed files with 182 additions and 39 deletions.
diff --git a/README.md b/README.md
@@ -213,12 +213,17 @@ procedure Main is
    Context : RFLX.TLV.Message.Context;
    Data : RFLX.RFLX_Builtin_Types.Bytes (RFLX.RFLX_Builtin_Types.Index'First .. RFLX.RFLX_Builtin_Types.Index'First + 2**14);
 
-   procedure Write_Data (Buffer : out RFLX.RFLX_Builtin_Types.Bytes) is
+   function Data_Length (Length : RFLX.RFLX_Builtin_Types.Length) return Boolean is
+      (Length <= Data'Length);
+
+   procedure Write_Data (Buffer : out RFLX.RFLX_Builtin_Types.Bytes) with
+      Pre => Data_Length (Buffer'Length)
+   is
    begin
       Buffer := Data (Data'First .. Data'First + Buffer'Length - 1);
    end Write_Data;
 
-   procedure Set_Value is new RFLX.TLV.Message.Set_Value (Write_Data);
+   procedure Set_Value is new RFLX.TLV.Message.Set_Value (Write_Data, Data_Length);
 begin
    --  Generating message
    RFLX.TLV.Message.Initialize (Context, Buffer);

diff --git a/generated/rflx-arrays-generic_inner_message.ads b/generated/rflx-arrays-generic_inner_message.ads
@@ -216,14 +216,18 @@ is
 
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
+      with function Check_Length_Payload (Length : Types.Length) return Boolean;
    procedure Set_Payload (Ctx : in out Context) with
      Pre =>
        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_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0
+       and then Check_Length_Payload (Types.Length (Field_Length (Ctx, F_Payload) / 8)),
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
@@ -241,7 +245,9 @@ is
        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_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0,
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old

diff --git a/generated/rflx-ethernet-generic_frame.ads b/generated/rflx-ethernet-generic_frame.ads
@@ -415,14 +415,18 @@ is
 
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
+      with function Check_Length_Payload (Length : Types.Length) return Boolean;
    procedure Set_Payload (Ctx : in out Context) with
      Pre =>
        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), Field_Length (Ctx, F_Payload))
-       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0
+       and then Check_Length_Payload (Types.Length (Field_Length (Ctx, F_Payload) / 8)),
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
@@ -438,6 +442,7 @@ is
 
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
+      with function Check_Length_Payload (Length : Types.Length) return Boolean;
    procedure Set_Bounded_Payload (Ctx : in out Context; Length : Types.Bit_Length) with
      Pre =>
        not Ctx'Constrained
@@ -448,7 +453,10 @@ is
        and then Available_Space (Ctx, F_Payload) >= Length
        and then (Field_First (Ctx, F_Payload) + Length) <= Types.Bit_Index'Last / 2
        and then ((Valid (Ctx, F_Type_Length)
-                  and Get_Type_Length (Ctx) >= 1536)),
+                  and Get_Type_Length (Ctx) >= 1536))
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Length mod 8 = 0
+       and then Check_Length_Payload (Types.Length (Length / 8)),
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
@@ -469,7 +477,9 @@ is
        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), Field_Length (Ctx, F_Payload))
-       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0,
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
@@ -493,7 +503,9 @@ is
        and then Available_Space (Ctx, F_Payload) >= Length
        and then (Field_First (Ctx, F_Payload) + Length) <= Types.Bit_Index'Last / 2
        and then ((Valid (Ctx, F_Type_Length)
-                  and Get_Type_Length (Ctx) >= 1536)),
+                  and Get_Type_Length (Ctx) >= 1536))
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Length mod 8 = 0,
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old

diff --git a/generated/rflx-expression-generic_message.ads b/generated/rflx-expression-generic_message.ads
@@ -188,14 +188,18 @@ is
 
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
+      with function Check_Length_Payload (Length : Types.Length) return Boolean;
    procedure Set_Payload (Ctx : in out Context) with
      Pre =>
        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_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0
+       and then Check_Length_Payload (Types.Length (Field_Length (Ctx, F_Payload) / 8)),
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
@@ -212,7 +216,9 @@ is
        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_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0,
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old

diff --git a/generated/rflx-ipv4-generic_option.ads b/generated/rflx-ipv4-generic_option.ads
@@ -338,14 +338,18 @@ is
 
    generic
       with procedure Process_Option_Data (Option_Data : out Types.Bytes);
+      with function Check_Length_Option_Data (Length : Types.Length) return Boolean;
    procedure Set_Option_Data (Ctx : in out Context) with
      Pre =>
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
        and then Valid_Next (Ctx, F_Option_Data)
        and then Field_Last (Ctx, F_Option_Data) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Option_Data))
-       and then Available_Space (Ctx, F_Option_Data) >= Field_Length (Ctx, F_Option_Data),
+       and then Available_Space (Ctx, F_Option_Data) >= Field_Length (Ctx, F_Option_Data)
+       and then Field_First (Ctx, F_Option_Data) mod 8 = 1
+       and then Field_Length (Ctx, F_Option_Data) mod 8 = 0
+       and then Check_Length_Option_Data (Types.Length (Field_Length (Ctx, F_Option_Data) / 8)),
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
@@ -366,7 +370,9 @@ is
        and then Valid_Next (Ctx, F_Option_Data)
        and then Field_Last (Ctx, F_Option_Data) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Option_Data))
-       and then Available_Space (Ctx, F_Option_Data) >= Field_Length (Ctx, F_Option_Data),
+       and then Available_Space (Ctx, F_Option_Data) >= Field_Length (Ctx, F_Option_Data)
+       and then Field_First (Ctx, F_Option_Data) mod 8 = 1
+       and then Field_Length (Ctx, F_Option_Data) mod 8 = 0,
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old

diff --git a/generated/rflx-ipv4-generic_packet.ads b/generated/rflx-ipv4-generic_packet.ads
@@ -964,14 +964,18 @@ is
 
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
+      with function Check_Length_Payload (Length : Types.Length) return Boolean;
    procedure Set_Payload (Ctx : in out Context) with
      Pre =>
        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_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0
+       and then Check_Length_Payload (Types.Length (Field_Length (Ctx, F_Payload) / 8)),
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
@@ -1003,7 +1007,9 @@ is
        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_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0,
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old

diff --git a/generated/rflx-tlv-generic_message.ads b/generated/rflx-tlv-generic_message.ads
@@ -250,14 +250,18 @@ is
 
    generic
       with procedure Process_Value (Value : out Types.Bytes);
+      with function Check_Length_Value (Length : Types.Length) return Boolean;
    procedure Set_Value (Ctx : in out Context) with
      Pre =>
        not Ctx'Constrained
        and then Has_Buffer (Ctx)
        and then Valid_Next (Ctx, F_Value)
        and then Field_Last (Ctx, F_Value) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Value))
-       and then Available_Space (Ctx, F_Value) >= Field_Length (Ctx, F_Value),
+       and then Available_Space (Ctx, F_Value) >= Field_Length (Ctx, F_Value)
+       and then Field_First (Ctx, F_Value) mod 8 = 1
+       and then Field_Length (Ctx, F_Value) mod 8 = 0
+       and then Check_Length_Value (Types.Length (Field_Length (Ctx, F_Value) / 8)),
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
@@ -276,7 +280,9 @@ is
        and then Valid_Next (Ctx, F_Value)
        and then Field_Last (Ctx, F_Value) <= Types.Bit_Index'Last / 2
        and then Field_Condition (Ctx, (Fld => F_Value))
-       and then Available_Space (Ctx, F_Value) >= Field_Length (Ctx, F_Value),
+       and then Available_Space (Ctx, F_Value) >= Field_Length (Ctx, F_Value)
+       and then Field_First (Ctx, F_Value) mod 8 = 1
+       and then Field_Length (Ctx, F_Value) mod 8 = 0,
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old

diff --git a/generated/rflx-udp-generic_datagram.ads b/generated/rflx-udp-generic_datagram.ads
@@ -318,14 +318,18 @@ is
 
    generic
       with procedure Process_Payload (Payload : out Types.Bytes);
+      with function Check_Length_Payload (Length : Types.Length) return Boolean;
    procedure Set_Payload (Ctx : in out Context) with
      Pre =>
        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_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0
+       and then Check_Length_Payload (Types.Length (Field_Length (Ctx, F_Payload) / 8)),
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old
@@ -346,7 +350,9 @@ is
        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_Length (Ctx, F_Payload),
+       and then Available_Space (Ctx, F_Payload) >= Field_Length (Ctx, F_Payload)
+       and then Field_First (Ctx, F_Payload) mod 8 = 1
+       and then Field_Length (Ctx, F_Payload) mod 8 = 0,
      Post =>
        Has_Buffer (Ctx)
        and Ctx.Buffer_First = Ctx.Buffer_First'Old

diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -40,6 +40,7 @@
     Indexed,
     Last,
     LessEqual,
+    Mod,
     NamedAggregate,
     Not,
     Number,
@@ -396,7 +397,14 @@ def formal_parameters(field: Field) -> Sequence[FormalSubprogramDeclaration]:
                     ProcedureSpecification(
                         f"Process_{field.name}", [OutParameter([field.name], const.TYPES_BYTES)],
                     )
-                )
+                ),
+                FormalSubprogramDeclaration(
+                    FunctionSpecification(
+                        f"Check_Length_{field.name}",
+                        "Boolean",
+                        [Parameter(["Length"], const.TYPES_LENGTH)],
+                    )
+                ),
             ]
 
         return UnitPart(
@@ -408,6 +416,23 @@ def formal_parameters(field: Field) -> Sequence[FormalSubprogramDeclaration]:
                             AndThen(
                                 *self.setter_preconditions(f),
                                 *self.unbounded_composite_setter_preconditions(message, f),
+                                Call(
+                                    f"Check_Length_{f.name}",
+                                    [
+                                        Call(
+                                            const.TYPES_LENGTH,
+                                            [
+                                                Div(
+                                                    Call(
+                                                        "Field_Length",
+                                                        [Variable("Ctx"), Variable(f.affixed_name)],
+                                                    ),
+                                                    Number(8),
+                                                ),
+                                            ],
+                                        ),
+                                    ],
+                                ),
                             )
                         ),
                         Postcondition(And(*self.composite_setter_postconditions(message, f),)),
@@ -425,6 +450,15 @@ def formal_parameters(field: Field) -> Sequence[FormalSubprogramDeclaration]:
                             AndThen(
                                 *self.setter_preconditions(f),
                                 *self.bounded_composite_setter_preconditions(message, f),
+                                Call(
+                                    f"Check_Length_{f.name}",
+                                    [
+                                        Call(
+                                            const.TYPES_LENGTH,
+                                            [Div(Variable("Length"), Number(8))],
+                                        )
+                                    ],
+                                ),
                             )
                         ),
                         Postcondition(And(*self.composite_setter_postconditions(message, f),)),
@@ -647,6 +681,19 @@ def unbounded_composite_setter_preconditions(message: Message, field: Field) ->
                 ),
             ),
             common.sufficient_space_for_field_condition(Variable(field.affixed_name)),
+            Equal(
+                Mod(
+                    Call("Field_First", [Variable("Ctx"), Variable(field.affixed_name)]), Number(8)
+                ),
+                Number(1),
+            ),
+            Equal(
+                Mod(
+                    Call("Field_Length", [Variable("Ctx"), Variable(field.affixed_name)]),
+                    Number(8),
+                ),
+                Number(0),
+            ),
         ]
 
     @staticmethod
@@ -688,6 +735,13 @@ def bounded_composite_setter_preconditions(message: Message, field: Field) -> Se
                     if Last("Message") in l.length
                 ]
             ),
+            Equal(
+                Mod(
+                    Call("Field_First", [Variable("Ctx"), Variable(field.affixed_name)]), Number(8)
+                ),
+                Number(1),
+            ),
+            Equal(Mod(Variable("Length"), Number(8)), Number(0),),
         ]
 
 

diff --git a/test.gpr b/test.gpr
@@ -44,9 +44,9 @@ project Test is
             for Proof_Switches ("rflx-custom_types_tests.adb") use ("--steps=2000");
             for Proof_Switches ("rflx-derivation-tests.adb") use ("--steps=4000");
             for Proof_Switches ("rflx-ethernet-tests.adb") use ("--steps=2000");
-            for Proof_Switches ("rflx-in_ethernet-tests.adb") use ("--steps=64000");
-            for Proof_Switches ("rflx-in_ipv4-tests.adb") use ("--steps=98000");
-            for Proof_Switches ("rflx-ipv4-tests.adb") use ("--steps=48000");
+            for Proof_Switches ("rflx-in_ethernet-tests.adb") use ("--steps=100000");
+            for Proof_Switches ("rflx-in_ipv4-tests.adb") use ("--steps=126000");
+            for Proof_Switches ("rflx-ipv4-tests.adb") use ("--steps=66000");
       end case;
    end Prove;