Prevent changes to usable range of buffer

- Consider size restrictions of refined fields - Allow setting array fields with size defined by message size Ref. #356, #486
AdaCore · Nov 16, 2020 · 1b34aa7 · 1b34aa7
1 parent 5208aca
commit 1b34aa7
Show file tree

Hide file tree

Showing 44 changed files with 1,656 additions and 1,409 deletions.
diff --git a/examples/apps/ping/Makefile b/examples/apps/ping/Makefile
@@ -9,5 +9,9 @@ test_spark:
 	gprbuild -Pping
 	sudo -n timeout 3 obj/ping 127.0.0.1 || test $$? -eq 124
 
+prove:
+	rflx generate -d generated specs/ipv4.rflx
+	gnatprove -Pping
+
 clean:
 	rm -rf generated/* obj python
diff --git a/examples/apps/ping/ping.gpr b/examples/apps/ping/ping.gpr
@@ -42,17 +42,17 @@ project Ping is
       );
 
       for Proof_Switches ("basalt-strings_generic.adb") use ("--prover=CVC4", "--steps=1735");
-      for Proof_Switches ("icmpv4.adb") use ("--prover=Z3,CVC4", "--steps=202506");
-      for Proof_Switches ("rflx-icmp-message.ads") use ("--prover=CVC4", "--steps=31799");
+      for Proof_Switches ("icmpv4.adb") use ("--prover=Z3,CVC4", "--steps=211172");
+      for Proof_Switches ("rflx-icmp-message.ads") use ("--prover=CVC4", "--steps=25545");
       for Proof_Switches ("rflx-icmp.ads") use ("--prover=CVC4", "--steps=1");
-      for Proof_Switches ("rflx-ipv4-contains.ads") use ("--prover=CVC4,Z3", "--steps=65010");
-      for Proof_Switches ("rflx-ipv4-options.ads") use ("--prover=CVC4", "--steps=450");
-      for Proof_Switches ("rflx-ipv4-packet.ads") use ("--prover=Z3,CVC4", "--steps=138127");
+      for Proof_Switches ("rflx-ipv4-contains.ads") use ("--prover=CVC4,Z3", "--steps=64299");
+      for Proof_Switches ("rflx-ipv4-options.ads") use ("--prover=CVC4", "--steps=451");
+      for Proof_Switches ("rflx-ipv4-packet.ads") use ("--prover=CVC4,Z3", "--steps=19485");
       for Proof_Switches ("rflx-ipv4.ads") use ("--prover=CVC4", "--steps=1");
-      for Proof_Switches ("rflx-ipv4_option-option.ads") use ("--prover=CVC4", "--steps=1920");
+      for Proof_Switches ("rflx-ipv4_option-option.ads") use ("--prover=CVC4", "--steps=2879");
       for Proof_Switches ("rflx-ipv4_option.ads") use ("--prover=CVC4", "--steps=1");
       for Proof_Switches ("rflx-rflx_arithmetic.adb") use ("--prover=CVC4", "--steps=70979");
-      for Proof_Switches ("rflx-rflx_types.ads") use ("--prover=altergo,Z3,CVC4", "--steps=239854");
+      for Proof_Switches ("rflx-rflx_types.ads") use ("--prover=Z3,altergo,CVC4", "--steps=239854");
    end Prove;
 
 end Ping;
diff --git a/examples/apps/ping/src/icmpv4.adb b/examples/apps/ping/src/icmpv4.adb
@@ -57,6 +57,7 @@ is
       Success     : Boolean;
       Ignore_Last : RFLX.RFLX_Builtin_Types.Index;
       Buffer      : RFLX.RFLX_Builtin_Types.Bytes_Ptr := new RFLX.RFLX_Builtin_Types.Bytes'(1 .. 1024 => 0);
+      Last        : RFLX.RFLX_Builtin_Types.Index;
    begin
       Socket.Setup;
       if
@@ -79,8 +80,8 @@ is
          pragma Loop_Invariant (Buffer /= null);
          pragma Loop_Invariant (Buffer'First = 1);
          pragma Loop_Invariant (Buffer'Length = 1024);
-         ICMPv4.Generate (Buffer, Address);
-         Socket.Send (Buffer.all (Buffer'First .. Buffer'First + 35), Address, Success);
+         ICMPv4.Generate (Buffer, Address, Last);
+         Socket.Send (Buffer.all (Buffer'First .. Last), Address, Success);
          if not Success then
             Ada.Text_IO.Put_Line ("Failed to send packet");
             Free_Bytes_Ptr (Buffer);
@@ -168,12 +169,14 @@ is
    --------------
 
    procedure Generate (Buf  : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr;
-                       Addr :        RFLX.IPv4.Address) is
+                       Addr :        RFLX.IPv4.Address;
+                       Last :    out RFLX.RFLX_Builtin_Types.Index)
+   is
       use type RFLX.ICMP.Sequence_Number;
       use type RFLX.RFLX_Builtin_Types.Bit_Length;
       IP_Context   : RFLX.IPv4.Packet.Context;
       ICMP_Context : RFLX.ICMP.Message.Context;
-      Data         : constant RFLX.RFLX_Builtin_Types.Bytes (1 .. 8) := (others => 65);
+      Data         : constant RFLX.RFLX_Builtin_Types.Bytes (1 .. 56) := (others => 65);
       function Valid_Length (L : RFLX.RFLX_Builtin_Types.Length) return Boolean is
          (L = Data'Length);
       procedure Process_Data (Buffer : out RFLX.RFLX_Builtin_Types.Bytes) with
@@ -183,15 +186,15 @@ is
       begin
          Buffer := Data;
       end Process_Data;
-      procedure Set_Data is new RFLX.ICMP.Message.Set_Bounded_Data (Process_Data, Valid_Length);
+      procedure Set_Data is new RFLX.ICMP.Message.Set_Data (Process_Data, Valid_Length);
    begin
       pragma Warnings (Off, "unused assignment to ""*_Context""");
       RFLX.IPv4.Packet.Initialize (IP_Context, Buf);
       RFLX.IPv4.Packet.Set_Version (IP_Context, 4);
       RFLX.IPv4.Packet.Set_IHL (IP_Context, 5);
       RFLX.IPv4.Packet.Set_DSCP (IP_Context, 0);
       RFLX.IPv4.Packet.Set_ECN (IP_Context, 0);
-      RFLX.IPv4.Packet.Set_Total_Length (IP_Context, 24);
+      RFLX.IPv4.Packet.Set_Total_Length (IP_Context, 84);
       RFLX.IPv4.Packet.Set_Identification (IP_Context, 1);
       RFLX.IPv4.Packet.Set_Flag_R (IP_Context, False);
       RFLX.IPv4.Packet.Set_Flag_DF (IP_Context, False);
@@ -214,12 +217,13 @@ is
                                              0, 0, Sequence, Data));
          RFLX.ICMP.Message.Set_Identifier (ICMP_Context, 0);
          RFLX.ICMP.Message.Set_Sequence_Number (ICMP_Context, Sequence);
-         Set_Data (ICMP_Context, 64);
+         Set_Data (ICMP_Context);
          RFLX.ICMP.Message.Take_Buffer (ICMP_Context, Buf);
          Sequence := Sequence + 1;
       else
          RFLX.IPv4.Packet.Take_Buffer (IP_Context, Buf);
       end if;
+      Last := RFLX.RFLX_Types.Byte_Index (RFLX.IPv4.Packet.Message_Last (IP_Context));
       pragma Warnings (On, "unused assignment to ""*_Context""");
    end Generate;
 

diff --git a/examples/apps/ping/src/icmpv4.ads b/examples/apps/ping/src/icmpv4.ads
@@ -27,14 +27,16 @@ is
                  Input  => Ada.Real_Time.Clock_Time);
 
    procedure Generate (Buf  : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr;
-                       Addr :        RFLX.IPv4.Address) with
+                       Addr :        RFLX.IPv4.Address;
+                       Last :    out RFLX.RFLX_Builtin_Types.Index) with
       Pre    => Buf /= null
                 and then Buf'Length = 1024
                 and then Buf'First = 1,
       Post   => Buf /= null
                 and then Buf'Length = Buf'Length'Old
-                and then Buf'First = Buf'First'Old,
-      Global => (In_Out => Ping_State);
+                and then Buf'First = Buf'First'Old
+                and then Last <= Buf'Last,
+     Global => (In_Out => Ping_State);
 
    procedure Print (Buf : in out RFLX.RFLX_Builtin_Types.Bytes_Ptr) with
       Pre    => Buf /= null

diff --git a/rflx/generator/common.py b/rflx/generator/common.py
@@ -459,6 +459,8 @@ def invalid_successors_invariant() -> ada.Expr:
             ]
         ),
         public_context_predicate(),
+        ada.LessEqual(ada.Variable("First"), ada.Variable("Message_Last")),
+        ada.LessEqual(ada.Variable("Message_Last"), ada.Variable("Last")),
         ada.ForAllIn(
             "F",
             ada.ValueRange(ada.First("Field"), ada.Last("Field")),
@@ -480,7 +482,7 @@ def invalid_successors_invariant() -> ada.Expr:
                                 ada.Selected(
                                     ada.Indexed(ada.Variable("Cursors"), ada.Variable("F")), "Last"
                                 ),
-                                ada.Variable("Last"),
+                                ada.Variable("Message_Last"),
                             ),
                             ada.LessEqual(
                                 ada.Selected(
@@ -576,17 +578,7 @@ def initialize_field_statements(
             "Reset_Dependent_Fields",
             [ada.Variable("Ctx"), ada.Variable(field.affixed_name)],
         ),
-        ada.Assignment(
-            "Ctx",
-            ada.Aggregate(
-                ada.Variable("Ctx.Buffer_First"),
-                ada.Variable("Ctx.Buffer_Last"),
-                ada.Variable("Ctx.First"),
-                ada.Variable("Last"),
-                ada.Variable("Ctx.Buffer"),
-                ada.Variable("Ctx.Cursors"),
-            ),
-        ),
+        ada.Assignment("Ctx.Message_Last", ada.Variable("Last")),
         # WORKAROUND:
         # Limitation of GNAT Community 2019 / SPARK Pro 20.0
         # Provability of predicate is increased by adding part of

diff --git a/rflx/generator/const.py b/rflx/generator/const.py
@@ -1,4 +1,4 @@
-import rflx.ada as ada
+from rflx import ada
 from rflx.common import file_name
 
 REFINEMENT_PACKAGE = ada.ID("Contains")
@@ -48,3 +48,13 @@
 TYPES_OFFSET = TYPES * "Offset"
 TYPES_UNREACHABLE_BIT_LENGTH = TYPES * "Unreachable_Bit_Length"
 TYPES_U64 = TYPES * "U64"
+
+CONTEXT_INVARIANT = [
+    ada.Equal(e, ada.Old(e))
+    for e in (
+        ada.Variable("Ctx.Buffer_First"),
+        ada.Variable("Ctx.Buffer_Last"),
+        ada.Variable("Ctx.First"),
+        ada.Variable("Ctx.Last"),
+    )
+]