[gcc r12-6447] [Ada] Proof of System.Vectors.Boolean_Operations

[gcc r12-6447] [Ada] Proof of System.Vectors.Boolean_Operations

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:e5be83512a66369ae77c9652d3a3073a14ff466a

commit r12-6447-ge5be83512a66369ae77c9652d3a3073a14ff466a
Author: Yannick Moy <moy@adacore.com>
Date:   Thu Dec 16 16:42:36 2021 +0100

    [Ada] Proof of System.Vectors.Boolean_Operations
    
    gcc/ada/
    
            * libgnat/s-veboop.adb: Add ghost code for proof.
            * libgnat/s-veboop.ads: Add specification.

Diff:
---
 gcc/ada/libgnat/s-veboop.adb | 106 ++++++++++++++++++++++++++++++++++++++++-
 gcc/ada/libgnat/s-veboop.ads | 111 +++++++++++++++++++++++++++++++++++++++----
 2 files changed, 207 insertions(+), 10 deletions(-)

diff --git a/gcc/ada/libgnat/s-veboop.adb b/gcc/ada/libgnat/s-veboop.adb
index c56895ff2e3..7bb0b5eebdd 100644
--- a/gcc/ada/libgnat/s-veboop.adb
+++ b/gcc/ada/libgnat/s-veboop.adb
@@ -29,7 +29,17 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package body System.Vectors.Boolean_Operations is
+--  Ghost code, loop invariants and assertions in this unit are meant for
+--  analysis only, not for run-time checking, as it would be too costly
+--  otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
+package body System.Vectors.Boolean_Operations
+  with SPARK_Mode
+is
 
    SU : constant := Storage_Unit;
    --  Convenient short hand, used throughout
@@ -76,7 +86,26 @@ package body System.Vectors.Boolean_Operations is
    -----------
 
    function "not" (Item : Vectors.Vector) return Vectors.Vector is
+
+      procedure Prove_Not (Result : Vectors.Vector)
+      with
+        Ghost,
+        Pre  => Valid (Item)
+          and then Result = (Item xor True_Val),
+        Post => Valid (Result)
+          and then (for all J in 1 .. Vector_Boolean_Size =>
+                      Model (Result) (J) = not Model (Item) (J));
+
+      procedure Prove_Not (Result : Vectors.Vector) is
+      begin
+         for J in 1 .. Vector_Boolean_Size loop
+            pragma Assert
+              (Element (Result, J) = 1 - Element (Item, J));
+         end loop;
+      end Prove_Not;
+
    begin
+      Prove_Not (Item xor True_Val);
       return Item xor True_Val;
    end "not";
 
@@ -90,7 +119,32 @@ package body System.Vectors.Boolean_Operations is
    end Nand;
 
    function Nand (Left, Right : Vectors.Vector) return Vectors.Vector is
+
+      procedure Prove_And (Result : Vectors.Vector)
+      with
+        Ghost,
+        Pre  => Valid (Left)
+          and then Valid (Right)
+          and then Result = (Left and Right),
+          Post => Valid (Result)
+            and then (for all J in 1 .. Vector_Boolean_Size =>
+                        Model (Result) (J) =
+                          (Model (Left) (J) and Model (Right) (J)));
+
+      procedure Prove_And (Result : Vectors.Vector) is
+      begin
+         for J in 1 .. Vector_Boolean_Size loop
+            pragma Assert
+              (Element (Result, J) =
+                 (if Element (Left, J) = 1
+                    and Element (Right, J) = 1
+                  then 1
+                  else 0));
+         end loop;
+      end Prove_And;
+
    begin
+      Prove_And (Left and Right);
       return not (Left and Right);
    end Nand;
 
@@ -104,7 +158,32 @@ package body System.Vectors.Boolean_Operations is
    end Nor;
 
    function Nor (Left, Right : Vectors.Vector) return Vectors.Vector is
+
+      procedure Prove_Or (Result : Vectors.Vector)
+      with
+        Ghost,
+        Pre  => Valid (Left)
+          and then Valid (Right)
+          and then Result = (Left or Right),
+          Post => Valid (Result)
+            and then (for all J in 1 .. Vector_Boolean_Size =>
+                        Model (Result) (J) =
+                          (Model (Left) (J) or Model (Right) (J)));
+
+      procedure Prove_Or (Result : Vectors.Vector) is
+      begin
+         for J in 1 .. Vector_Boolean_Size loop
+            pragma Assert
+              (Element (Result, J) =
+                 (if Element (Left, J) = 1
+                    or Element (Right, J) = 1
+                  then 1
+                  else 0));
+         end loop;
+      end Prove_Or;
+
    begin
+      Prove_Or (Left or Right);
       return not (Left or Right);
    end Nor;
 
@@ -118,7 +197,32 @@ package body System.Vectors.Boolean_Operations is
    end Nxor;
 
    function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector is
+
+      procedure Prove_Xor (Result : Vectors.Vector)
+      with
+        Ghost,
+        Pre  => Valid (Left)
+          and then Valid (Right)
+          and then Result = (Left xor Right),
+          Post => Valid (Result)
+            and then (for all J in 1 .. Vector_Boolean_Size =>
+                        Model (Result) (J) =
+                          (Model (Left) (J) xor Model (Right) (J)));
+
+      procedure Prove_Xor (Result : Vectors.Vector) is
+      begin
+         for J in 1 .. Vector_Boolean_Size loop
+            pragma Assert
+              (Element (Result, J) =
+                 (if Element (Left, J) = 1
+                    xor Element (Right, J) = 1
+                  then 1
+                  else 0));
+         end loop;
+      end Prove_Xor;
+
    begin
+      Prove_Xor (Left xor Right);
       return not (Left xor Right);
    end Nxor;
 
diff --git a/gcc/ada/libgnat/s-veboop.ads b/gcc/ada/libgnat/s-veboop.ads
index e0174ae4672..461475947e5 100644
--- a/gcc/ada/libgnat/s-veboop.ads
+++ b/gcc/ada/libgnat/s-veboop.ads
@@ -31,15 +31,77 @@
 
 --  This package contains functions for runtime operations on boolean vectors
 
-package System.Vectors.Boolean_Operations is
-   pragma Pure;
+--  Preconditions in this unit are meant for analysis only, not for run-time
+--  checking, so that the expected exceptions are raised. This is enforced by
+--  setting the corresponding assertion policy to Ignore. Postconditions and
+--  contract cases should not be executed at runtime as well, in order not to
+--  slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
+package System.Vectors.Boolean_Operations
+  with Pure, SPARK_Mode
+is
+   pragma Warnings (Off, "aspect ""Pre"" not enforced on inlined subprogram",
+                    Reason => "Pre only used in proof");
+   pragma Warnings (Off, "aspect ""Post"" not enforced on inlined subprogram",
+                    Reason => "Post only used in proof");
+
+   --  Type Vectors.Vector represents an array of Boolean, each of which
+   --  takes 8 bits of the representation, with the 7 msb set to zero. Express
+   --  in contracts the constraint on valid vectors and the model that they
+   --  represent, and the relationship between input models and output model.
+
+   Vector_Boolean_Size : constant Positive :=
+     System.Word_Size / System.Storage_Unit
+   with Ghost;
+
+   type Vector_Element is mod 2 ** System.Storage_Unit with Ghost;
+
+   type Vector_Boolean_Array is array (1 .. Vector_Boolean_Size) of Boolean
+   with Ghost;
+
+   function Shift_Right (V : Vectors.Vector; N : Natural) return Vectors.Vector
+   with Ghost, Import, Convention => Intrinsic;
+
+   function Element (V : Vectors.Vector; N : Positive) return Vector_Element is
+     (Vector_Element (Shift_Right (V, (N - 1) * System.Storage_Unit)
+                        and (2 ** System.Storage_Unit - 1)))
+   with
+     Ghost,
+     Pre => N <= Vector_Boolean_Size;
+   --  Return the Nth element represented by the vector
+
+   function Valid (V : Vectors.Vector) return Boolean is
+     (for all J in 1 .. Vector_Boolean_Size =>
+        Element (V, J) in 0 .. 1)
+   with Ghost;
+   --  A valid vector is one for which all elements are 0 (representing False)
+   --  or 1 (representing True).
+
+   function Model (V : Vectors.Vector) return Vector_Boolean_Array
+   with
+     Ghost,
+     Pre => Valid (V);
+
+   function Model (V : Vectors.Vector) return Vector_Boolean_Array is
+     (for J in 1 .. Vector_Boolean_Size => Element (V, J) = 1);
+   --  The model of a valid vector is the corresponding array of Boolean values
 
    --  Although in general the boolean operations on arrays of booleans are
    --  identical to operations on arrays of unsigned words of the same size,
    --  for the "not" operator this is not the case as False is typically
    --  represented by 0 and true by 1.
 
-   function "not" (Item : Vectors.Vector) return Vectors.Vector;
+   function "not" (Item : Vectors.Vector) return Vectors.Vector
+   with
+     Pre  => Valid (Item),
+     Post => Valid ("not"'Result)
+       and then (for all J in 1 .. Vector_Boolean_Size =>
+                   Model ("not"'Result) (J) = not Model (Item) (J));
 
    --  The three boolean operations "nand", "nor" and "nxor" are needed
    --  for cases where the compiler moves boolean array operations into
@@ -51,13 +113,44 @@ package System.Vectors.Boolean_Operations is
    --    (not X) xor (not Y)  =  X xor Y
    --    X       xor (not Y)  =  not (X xor Y)  =  Nxor (X, Y)
 
-   function Nand (Left, Right : Boolean) return Boolean;
-   function Nor  (Left, Right : Boolean) return Boolean;
-   function Nxor (Left, Right : Boolean) return Boolean;
+   function Nand (Left, Right : Boolean) return Boolean
+   with
+     Post => Nand'Result = not (Left and Right);
+
+   function Nor  (Left, Right : Boolean) return Boolean
+   with
+     Post => Nor'Result = not (Left or Right);
+
+   function Nxor (Left, Right : Boolean) return Boolean
+   with
+     Post => Nxor'Result = not (Left xor Right);
+
+   function Nand (Left, Right : Vectors.Vector) return Vectors.Vector
+   with
+     Pre  => Valid (Left)
+       and then Valid (Right),
+     Post => Valid (Nand'Result)
+       and then (for all J in 1 .. Vector_Boolean_Size =>
+                   Model (Nand'Result) (J) =
+                     Nand (Model (Left) (J), Model (Right) (J)));
+
+   function Nor (Left, Right : Vectors.Vector) return Vectors.Vector
+   with
+     Pre  => Valid (Left)
+       and then Valid (Right),
+     Post => Valid (Nor'Result)
+       and then (for all J in 1 .. Vector_Boolean_Size =>
+                   Model (Nor'Result) (J) =
+                     Nor (Model (Left) (J), Model (Right) (J)));
 
-   function Nand (Left, Right : Vectors.Vector) return Vectors.Vector;
-   function Nor (Left, Right : Vectors.Vector) return Vectors.Vector;
-   function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector;
+   function Nxor (Left, Right : Vectors.Vector) return Vectors.Vector
+   with
+     Pre  => Valid (Left)
+       and then Valid (Right),
+     Post => Valid (Nxor'Result)
+       and then (for all J in 1 .. Vector_Boolean_Size =>
+                   Model (Nxor'Result) (J) =
+                     Nxor (Model (Left) (J), Model (Right) (J)));
 
    pragma Inline_Always ("not");
    pragma Inline_Always (Nand);