Unsound handling of access type arguments

[tobycmurray]

In GNAT Community Edition 2019, the SPARK Prover appears to be missing certain alias checks needed to prevent unsoundness when handling certain uses of access types. The following is a minimal example that demonstrates the issue.

The following program main.adb, when run, violates the assert, which is proved by the SPARK Prover

with Ada.Text_IO;

procedure Main with SPARK_Mode is
   type Int_Ptr is access Integer;

   procedure Zero_First_Arg(X : access Integer; Y : access Integer)
     with Pre => (X /= null and Y /= null),
          Post => (Y.all = Y.all'Old and X.all = 0) is
   begin
      X.all := 0;
      Ada.Text_IO.New_Line; -- silence spurious warning about Zero_First_Arg having no effect
   end Zero_First_Arg;
   
   X : Int_Ptr := new Integer'(1);
begin
   Zero_First_Arg(X,X);
   pragma Assert (X.all /= 0);
   if (X.all = 0) then
      Ada.Text_IO.Put_Line("It's 0!");
   end if;
   
end Main;

The project file default.gpr is trivial:

project Default is
    for Source_Dirs use (".");
    for Object_Dir use "obj";
    for Main use ("main.adb");
end Default;

To reproduce, on the command line: (noting that I have anonymised some of the output)

$ gnatprove -Pdefault.gpr --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:8:19: info: postcondition proved
main.adb:8:22: info: pointer dereference check proved
main.adb:8:30: info: pointer dereference check proved
main.adb:8:44: info: pointer dereference check proved
main.adb:10:09: info: pointer dereference check proved
main.adb:16:04: info: precondition proved
main.adb:17:19: info: assertion proved
main.adb:17:21: info: pointer dereference check proved
main.adb:18:10: info: pointer dereference check proved
Summary logged in $PWD/obj/gnatprove/gnatprove.out

$ gnatmake main
gcc -c main.adb
gnatbind -x main.ali
gnatlink main.ali
$ ./main

It's 0!

The version of gnatprove I am running is simply the Mac OS 64-bit binary package:

$ gnatprove --version
2019 (20190517)
Why3 for gnatprove version 1.2.0+git
/Users/tobym/opt/GNAT/2019/libexec/spark/bin/alt-ergo: Alt-Ergo version 2.3.0
/Users/tobym/opt/GNAT/2019/libexec/spark/bin/cvc4: This is CVC4 version 1.7.1-prerelease
/Users/tobiasm1/opt/GNAT/2019/libexec/spark/bin/z3: Z3 version 4.8.0 - 64 bit

[ptroja]

Hi @tobycmurray, thanks for a detailed report. I confirm this is a bug and it is still present in the current development version of GNATprove. We will look into it.

[tobycmurray]

No worries. I’d be curious to know: does the SPARK RM forbid this case? Is this just a missing check in the tools, or a deeper issue?

[ptroja]

This is just a missing check in the tool, not a deeper issue. The wrongly implemented rule is SPARK RM 6.4.2(2):

A formal parameter is said to be immutable in the following cases:

• it is of mode in and not of an access type.

http://docs.adacore.com/spark2014-docs/html/lrm/subprograms.html#anti-aliasing

[tobycmurray]

OK here is another issue, demonstrated by the attached (which I admit is not quite as minimal as I'd hoped to get it but I've run out of time... sorry).
bug.zip

The problem here appears to be the Get_Name procedure of the Person package: that procedure should be generating a permission error, I believe.

The inconsistency in Main is of course that we know the two pointers P.Name and S2 alias (indeed we can prove it), but then we use the Zero_First_Arg procedure which purportedly only modifies the memory pointed to by one of them. Inconsistency then ensues, IIUC.

[ptroja]

What I get on this code is:

person.ads:16:19: prefix of "Old" attribute which is not a function call is not allowed in SPARK (SPARK RM 3.10(13))
person.ads:16:19: violation of aspect SPARK_Mode at line 1

Then, when I remove problematic Post contracts with 'Old I get:

warning: no bodies have been analyzed by GNATprove
enable analysis of a non-generic body using SPARK_Mode

Finally, after adding SPARK_Mode to person.adb body, I get:

person.ads:15:14: insufficient permission for "P" when returning from "Get_Name"
person.ads:15:14: object was moved at person.adb:12

This I guess is what you expected, right?

A small procedural tip: I suggest you to report issues by email to report@adacore.com, where they will be immediately seen by all SPARK & GNAT engineers. Also, this will allow us to better track progress on fixing the problem, if necessary.

[tobycmurray]

Ah, my apologies. I see the issue was that I didn't have SPARK_Mode in the package body. Thanks :)

I did not get the warning about violating SPARK RM 3.10(13)). But possibly this is because I am running the 2019 release?

Anyway, sorry for the noise and thanks for looking at it. I'll remember the tip about the reporting by email for future.

[ptroja]

No worries, you are welcome :)

If you are specifically interested in playing with access types, then I strongly recommend you to focus on Community Edition 2020, as have fixed a lot of bugs and holes in this area since Community Edition 2019.

PS If you are experimenting with SPARK for anything more than toy example, and if this is related to your academic activities, then I encourage you to have look at https://www.adacore.com/academia

[ptroja]

This issue has been fixed in the development version of GNATprove, which now emits a message (in the extended output format, which was recently implemented):

main.adb:16:19: high: formal parameters "X" and "Y" are aliased (SPARK RM 6.4.2)
   16 |   Zero_First_Arg(X,X);
      |                  ^ here

I am closing the issue. Thanks again for reporting it!