From e5be83512a66369ae77c9652d3a3073a14ff466a Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 16 Dec 2021 16:42:36 +0100 Subject: [PATCH] [Ada] Proof of System.Vectors.Boolean_Operations gcc/ada/ * libgnat/s-veboop.adb: Add ghost code for proof. * libgnat/s-veboop.ads: Add specification. --- 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 c56895f..7bb0b5e 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 e0174ae..4614759 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); -- 2.7.4