Potential aliasing violation in swap array indexes SPARK-Ada

Question

The Introduction to Spark course contains an example (#5) where GNATprove fails to prove that no aliasing occurs in a procedure that swaps two elements of an array:

package P
  with SPARK_Mode => On
is
   type P_Array is array (Natural range <>) of Positive;

   procedure Swap_Indexes (A : in out P_Array; I, J : Natural);
   procedure Swap (X, Y : in out Positive);
end P;

package body P
  with SPARK_Mode => On
is
   procedure Swap (X, Y : in out Positive) is
      Tmp : constant Positive := X;
   begin
      X := Y;
      Y := Tmp;
   end Swap;

   procedure Swap_Indexes (A : in out P_Array; I, J : Natural) is
   begin
      Swap (A (I), A (J));
   end Swap_Indexes;

end P;

GNATprove says p.adb:13:13: medium: formal parameters "X" and "Y" might be aliased (SPARK RM 6.4.2). This seems like a valid bug because the indexes passed to Swap_Indexes might be equal. However, after adding the precondition Pre => I /= J to Swap_Indexes, GNATprove still fails to prove a lack of aliasing. Why is that precondition insufficient?

Answer 1

As stated in the comments, the warning for potential aliasing can be mitigated by removing the Swap subprogram from the package spec. However, the precondition I /= J on Swap_Indexes can then also be omitted without the outcome to change. Moreover, adding again a new Swap2 (A, B : in out Positive) subprogram to the package spec that only calls the now local Swap in the package body will not cause the warning on potential aliasing to re-appear. This suggests that the problem is really the call to Swap, not it's visibility.

Looking at the output of GNATprove (i.e. info on checks proved), it seems that removing Swap from the package spec causes the GNAT compiler (frontend) to inline Swap into Swap_Indexes. Inlining effectively removes the call to Swap from Swap_Indexes and with it a reason to warn for potential effects due to aliasing.

NOTE: This can actually be verified by passing the debug option -gnatd.j to the compiler (see here) and passing the option --no-inlining to GNATprove as shown in the example below.

So while the warning on aliasing can, for the specific example, be mitigated by removing Swap from the package spec, the solution doesn't answer the original question of why the precondition I /= J cannot prove the absence of aliasing. And while I cannot say for sure, I suspect that this is just a current limitation of GNATprove's ability to prove the absence of aliasing for non-static actual parameters. Thereby noting that while the absence of aliasing effects is obvious given the precondition in the example, proving this in the general might quickly become (very) hard.

p.ads

package P with SPARK_Mode is

   type P_Array is array (Natural range <>) of Positive;

   procedure Swap_Indexes (A : in out P_Array; I, J : Natural)
     with Pre => I in A'Range and J in A'Range;
   
   procedure Swap2 (A, B : in out Positive)
     with Global => null;
   
end P;

p.adb

package body P with SPARK_Mode is
   
   procedure Swap (X, Y : in out Positive) is
      Tmp : constant Positive := X;
   begin
      X := Y;
      Y := Tmp;
   end Swap_Local;
   
   procedure Swap_Indexes (A : in out P_Array; I, J : Natural) is
   begin
      Swap (A (I), A (J));
   end Swap_Indexes;
   
   procedure Swap2 (A, B : in out Positive) is
   begin
      Swap (A, B);
   end Swap2;

end P;

output (GNATprove)

$ gnatprove -Pdefault.gpr -j0 --level=1 --report=all -cargs -gnatd.j
Phase 1 of 2: generation of Global contracts ...
List of calls inlined by the frontend
  1:p.adb:12:7:
  2:p.adb:17:7:
Phase 2 of 2: flow analysis and proof ...
List of calls inlined by the frontend
  1:p.adb:12:7:
  2:p.adb:17:7:
p.adb:4:34: info: index check proved, in call inlined at p.adb:12
p.adb:6:07: info: index check proved, in call inlined at p.adb:12
p.adb:6:12: info: index check proved, in call inlined at p.adb:12
p.adb:7:07: info: index check proved, in call inlined at p.adb:12
p.ads:9:11: info: data dependencies proved
Summary logged in [...]/gnatprove.out

Requesting GNATprove not to inline (--no-inlining) makes the warning to re-appear, even if the precondition I /= J is added to Swap_Indexes.

output (GNATprove)

$ gnatprove --no-inlining -Pdefault.gpr -j0 --level=1 --report=all -cargs -gnatd.j
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
p.adb:12:13: medium: formal parameters "X" and "Y" might be aliased (SPARK RM 6.4.2)
p.adb:12:16: info: index check proved
p.adb:12:23: info: index check proved
p.ads:9:11: info: data dependencies proved
Summary logged in [...]/gnatprove.out