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?

Your program does not ensure that either I or J are within the range of index values for the instance A of P_Array. For instance, if the actual parameter passed to the formal prameter A is an array of 10 elements, range 0..9, and the parameters I and J are 11 and 23, the swap cannot be proven. Try adding the precondition that both I and J are within A'Range. — Jim Rogers, Nov 30 '20 at 22:59
I tried adding the precondition `Pre => I /= J and I in A'Range and J in A'Range` to `Swap_Indexes`, but GNATprove gave me the same error message about potential aliasing. Is that the correct way to assert that `I` and `J` are in the range of index values for `A`? — Daniel Ricketts, Nov 30 '20 at 23:11
It looks to me like the problem is with `Swap`. Because it's public, it might be called from outside the pkg, and there's no guarantee that it won't be called with the same variable for both parameters. What happens if you remove it from the spec? — Jeffrey R. Carter, Dec 01 '20 at 09:22
@JeffreyR.Carter That was my first thought as well and the warning on potential aliasing indeed disappears after removing `Swap` from the pkg 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 pkg spec that only calls the now local `Swap` in the pkg 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... — DeeDee, Dec 01 '20 at 18:43
@DeeDee It does seem weird to me that the visibility of `Swap` has an effect on the outcome of verification. After removing `Swap` from the pkg spec, if I change the implementation of `Swap_Indexes` to `Swap (A (I), A (I));` (both arguments to `Swap` are definitely the same), then GNATprove doesn't report any aliasing. — Daniel Ricketts, Dec 02 '20 at 01:18
@DanielRicketts Looking at the output of GNATprove (i.e. info on checks proved), it seems that removing `Swap` from the pkg spec causes the *GNAT compiler* (front-end) to inline `Swap` into `Swap_Indexes`. This effectively removes the call to `Swap` from `Swap_Indexes` and with it a reason to warn for potential effects due to aliasing. If the compiler would've decided to not inline `Swap`, then the warning for potential aliasing would likely have persisted. — DeeDee, Dec 02 '20 at 08:18
@DanielRicketts So at this point, the warning on aliasing can, for the specific example, be mitigated by removing `Swap` from the pkg spec. However, this doesn't answer the original question of why the precondition `I /= J` cannot prove the absence of aliasing. While I cannot say for sure, I *think* 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. — DeeDee, Dec 02 '20 at 08:49
@DeeDee Inlining of `Swap` makes sense and resolves my confusion there. Your suspicion about that limitation of the anti-aliasing analysis also makes sense. The reference manual [section on anti-aliasing](https://docs.adacore.com/spark2014-docs/html/lrm/subprograms.html#anti-aliasing) contains an example that proves absence of aliasing on statically known array indexes but not dynamic indexes. It makes me wonder whether the aliasing analysis uses preconditions at all. Do you want to make your comment an answer? — Daniel Ricketts, Dec 02 '20 at 16:42

DeeDee · Accepted Answer · 2020-12-02T18:48:29.317

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

Potential aliasing violation in swap array indexes SPARK-Ada

1 Answers1