public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r12-6315] [Ada] Proof of System.Generic_Array_Operations at silver level
@ 2022-01-06 17:14 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-01-06 17:14 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:42dd6f60d8fefe1b026989d78eabf0108c528e4b
commit r12-6315-g42dd6f60d8fefe1b026989d78eabf0108c528e4b
Author: Yannick Moy <moy@adacore.com>
Date: Wed Dec 8 09:09:25 2021 -0500
[Ada] Proof of System.Generic_Array_Operations at silver level
gcc/ada/
* libgnat/a-ngcoar.adb: Add pragma to ignore assertions in
instance.
* libgnat/a-ngrear.adb: Likewise.
* libgnat/s-gearop.adb: Prove implementation is free of runtime
errors.
* libgnat/s-gearop.ads: Add contracts to protect against runtime
errors in the generic part.
Diff:
---
gcc/ada/libgnat/a-ngcoar.adb | 11 ++
gcc/ada/libgnat/a-ngrear.adb | 11 ++
gcc/ada/libgnat/s-gearop.adb | 321 +++++++++++++++++++++++++++++++++++++++----
gcc/ada/libgnat/s-gearop.ads | 198 ++++++++++++++++++++++----
4 files changed, 490 insertions(+), 51 deletions(-)
diff --git a/gcc/ada/libgnat/a-ngcoar.adb b/gcc/ada/libgnat/a-ngcoar.adb
index ed9be6a5c5b..953cb0966d8 100644
--- a/gcc/ada/libgnat/a-ngcoar.adb
+++ b/gcc/ada/libgnat/a-ngcoar.adb
@@ -29,6 +29,17 @@
-- --
------------------------------------------------------------------------------
+-- Preconditions, postconditions, 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 (Pre => Ignore,
+ Post => Ignore,
+ Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
with System.Generic_Array_Operations; use System.Generic_Array_Operations;
package body Ada.Numerics.Generic_Complex_Arrays is
diff --git a/gcc/ada/libgnat/a-ngrear.adb b/gcc/ada/libgnat/a-ngrear.adb
index 5095db8ee65..c34cdd686c0 100644
--- a/gcc/ada/libgnat/a-ngrear.adb
+++ b/gcc/ada/libgnat/a-ngrear.adb
@@ -36,6 +36,17 @@
-- BLAS/LAPACK implementation. Finally, on some platforms there are more
-- floating point types than supported by BLAS/LAPACK.
+-- Preconditions, postconditions, 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 (Pre => Ignore,
+ Post => Ignore,
+ Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
with Ada.Containers.Generic_Anonymous_Array_Sort; use Ada.Containers;
with System; use System;
diff --git a/gcc/ada/libgnat/s-gearop.adb b/gcc/ada/libgnat/s-gearop.adb
index 92af09d09da..e86d982d551 100644
--- a/gcc/ada/libgnat/s-gearop.adb
+++ b/gcc/ada/libgnat/s-gearop.adb
@@ -29,18 +29,44 @@
-- --
------------------------------------------------------------------------------
+-- Preconditions, postconditions, 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 (Pre => Ignore,
+ Post => Ignore,
+ Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
with Ada.Numerics; use Ada.Numerics;
-package body System.Generic_Array_Operations is
+
+package body System.Generic_Array_Operations
+ with SPARK_Mode
+is
+ pragma Warnings
+ (Off, "aspect * not enforced on inlined subprogram",
+ Reason => "Contracts in this unit are never executed");
+
function Check_Unit_Last
(Index : Integer;
Order : Positive;
- First : Integer) return Integer;
+ First : Integer) return Integer
+ with
+ Pre => Index >= First
+ and then First <= Integer'Last - Order + 1
+ and then Index <= First + (Order - 1),
+ Post => Check_Unit_Last'Result = First + (Order - 1);
+
pragma Inline_Always (Check_Unit_Last);
-- Compute index of last element returned by Unit_Vector or Unit_Matrix.
-- A separate function is needed to allow raising Constraint_Error before
-- declaring the function result variable. The result variable needs to be
-- declared first, to allow front-end inlining.
+ pragma Warnings (On, "aspect * not enforced on inlined subprogram");
+
--------------
-- Diagonal --
--------------
@@ -48,9 +74,14 @@ package body System.Generic_Array_Operations is
function Diagonal (A : Matrix) return Vector is
N : constant Natural := Natural'Min (A'Length (1), A'Length (2));
begin
- return R : Vector (A'First (1) .. A'First (1) + N - 1) do
+ return R : Vector (A'First (1) .. A'First (1) + (N - 1))
+ with Relaxed_Initialization
+ do
for J in 0 .. N - 1 loop
R (R'First + J) := A (A'First (1) + J, A'First (2) + J);
+
+ pragma Loop_Invariant
+ (for all JJ in R'First .. R'First + J => R (JJ)'Initialized);
end loop;
end return;
end Diagonal;
@@ -103,7 +134,10 @@ package body System.Generic_Array_Operations is
(M : in out Matrix;
Target : Integer;
Source : Integer;
- Factor : Scalar);
+ Factor : Scalar)
+ with
+ Pre => Target in M'Range (1)
+ and then Source in M'Range (1);
-- Elementary row operation that subtracts Factor * M (Source, <>) from
-- M (Target, <>)
@@ -131,6 +165,9 @@ package body System.Generic_Array_Operations is
begin
Do_Rows : for Row in reverse M'Range (1) loop
+
+ pragma Loop_Invariant (Max_Col <= M'Last (2));
+
Find_Non_Zero : for Col in reverse M'First (2) .. Max_Col loop
if Is_Non_Zero (M (Row, Col)) then
@@ -144,12 +181,15 @@ package body System.Generic_Array_Operations is
-- equals Integer'First, which is true for aggregates
-- without explicit bounds..
- J : Integer := M'First (1);
+ J : Integer := M'First (1);
+ NZ : constant Scalar := M (Row, Col);
begin
while J < Row loop
- Sub_Row (N, J, Row, (M (J, Col) / M (Row, Col)));
- Sub_Row (M, J, Row, (M (J, Col) / M (Row, Col)));
+ pragma Loop_Invariant (J in M'Range (1));
+
+ Sub_Row (N, J, Row, (M (J, Col) / NZ));
+ Sub_Row (M, J, Row, (M (J, Col) / NZ));
J := J + 1;
end loop;
end;
@@ -189,19 +229,38 @@ package body System.Generic_Array_Operations is
(M : in out Matrix;
Target : Integer;
Source : Integer;
- Factor : Scalar);
+ Factor : Scalar)
+ with
+ Pre => Target in M'Range (1)
+ and then Source in M'Range (1);
-- Subtrace Factor * M (Source, <>) from M (Target, <>)
procedure Divide_Row
(M, N : in out Matrix;
Row : Integer;
- Scale : Scalar);
+ Scale : Scalar)
+ with
+ Pre => Row in M'Range (1)
+ and then M'First (1) = N'First (1)
+ and then M'Last (1) = N'Last (1)
+ and then Scale /= Zero;
-- Divide M (Row) and N (Row) by Scale, and update Det
procedure Switch_Row
(M, N : in out Matrix;
Row_1 : Integer;
- Row_2 : Integer);
+ Row_2 : Integer)
+ with
+ Pre => Row_1 in M'Range (1)
+ and then Row_2 in M'Range (1)
+ and then M'First (1) = N'First (1)
+ and then M'Last (1) = N'Last (1),
+ Post => (for all J in M'Range (2) =>
+ M (Row_1, J) = M'Old (Row_2, J)
+ and then M (Row_2, J) = M'Old (Row_1, J))
+ and then (for all J in N'Range (2) =>
+ N (Row_1, J) = N'Old (Row_2, J)
+ and then N (Row_2, J) = N'Old (Row_1, J));
-- Exchange M (Row_1) and N (Row_1) with M (Row_2) and N (Row_2),
-- negating Det in the process.
@@ -238,8 +297,7 @@ package body System.Generic_Array_Operations is
end loop;
for J in N'Range (2) loop
- N (Row - M'First (1) + N'First (1), J) :=
- N (Row - M'First (1) + N'First (1), J) / Scale;
+ N (Row, J) := N (Row, J) / Scale;
pragma Annotate
(CodePeer, False_Positive, "divide by zero", "Scale /= 0");
end loop;
@@ -254,7 +312,9 @@ package body System.Generic_Array_Operations is
Row_1 : Integer;
Row_2 : Integer)
is
- procedure Swap (X, Y : in out Scalar);
+ procedure Swap (X, Y : in out Scalar)
+ with
+ Post => X = Y'Old and then Y = X'Old;
-- Exchange the values of X and Y
----------
@@ -276,11 +336,28 @@ package body System.Generic_Array_Operations is
for J in M'Range (2) loop
Swap (M (Row_1, J), M (Row_2, J));
+ pragma Annotate
+ (GNATprove, False_Positive,
+ "formal parameters ""X"" and ""Y"" might be aliased",
+ "Row_1 /= Row_2");
+
+ pragma Loop_Invariant
+ (for all JJ in M'First (2) .. J =>
+ M (Row_1, JJ) = M'Loop_Entry (Row_2, JJ)
+ and then M (Row_2, JJ) = M'Loop_Entry (Row_1, JJ));
end loop;
for J in N'Range (2) loop
- Swap (N (Row_1 - M'First (1) + N'First (1), J),
- N (Row_2 - M'First (1) + N'First (1), J));
+ Swap (N (Row_1, J), N (Row_2, J));
+ pragma Annotate
+ (GNATprove, False_Positive,
+ "formal parameters ""X"" and ""Y"" might be aliased",
+ "Row_1 /= Row_2");
+
+ pragma Loop_Invariant
+ (for all JJ in N'First (2) .. J =>
+ N (Row_1, JJ) = N'Loop_Entry (Row_2, JJ)
+ and then N (Row_2, JJ) = N'Loop_Entry (Row_1, JJ));
end loop;
end if;
end Switch_Row;
@@ -295,6 +372,8 @@ package body System.Generic_Array_Operations is
Det := One;
for J in M'Range (2) loop
+ pragma Loop_Invariant (Row >= M'First (1));
+
declare
Max_Row : Integer := Row;
Max_Abs : Real'Base := 0.0;
@@ -303,6 +382,10 @@ package body System.Generic_Array_Operations is
-- Find best pivot in column J, starting in row Row
for K in Row .. M'Last (1) loop
+ pragma Loop_Invariant (Max_Row in M'Range (1));
+ pragma Loop_Invariant
+ (if Max_Abs /= 0.0 then Max_Abs = abs M (Max_Row, J));
+
declare
New_Abs : constant Real'Base := abs M (K, J);
begin
@@ -316,6 +399,8 @@ package body System.Generic_Array_Operations is
if Max_Abs > 0.0 then
Switch_Row (M, N, Row, Max_Row);
+ pragma Assert (Max_Abs = abs M (Row, J));
+
-- The temporaries below are necessary to force a copy of the
-- value and avoid improper aliasing.
@@ -325,7 +410,7 @@ package body System.Generic_Array_Operations is
Divide_Row (M, N, Row, Scale);
end;
- for U in Row + 1 .. M'Last (1) loop
+ for U in Row .. M'Last (1) when U /= Row loop
declare
Factor : constant Scalar := M (U, J);
begin
@@ -379,7 +464,11 @@ package body System.Generic_Array_Operations is
begin
for J in X'Range loop
+ pragma Loop_Invariant (Sum >= 0.0);
Sum := Sum + Result_Real'Base (abs X (J))**2;
+ pragma Annotate
+ (GNATprove, Intentional, "float overflow check might fail",
+ "Intermediate computation might overflow in L2_Norm");
end loop;
return Sqrt (Sum);
@@ -391,11 +480,25 @@ package body System.Generic_Array_Operations is
function Matrix_Elementwise_Operation (X : X_Matrix) return Result_Matrix is
begin
- return R : Result_Matrix (X'Range (1), X'Range (2)) do
+ return R : Result_Matrix (X'Range (1), X'Range (2))
+ with Relaxed_Initialization
+ do
for J in R'Range (1) loop
for K in R'Range (2) loop
R (J, K) := Operation (X (J, K));
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
end loop;
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'Range (2) => R (J, KK)'Initialized);
end loop;
end return;
end Matrix_Elementwise_Operation;
@@ -422,7 +525,9 @@ package body System.Generic_Array_Operations is
Right : Right_Matrix) return Result_Matrix
is
begin
- return R : Result_Matrix (Left'Range (1), Left'Range (2)) do
+ return R : Result_Matrix (Left'Range (1), Left'Range (2))
+ with Relaxed_Initialization
+ do
if Left'Length (1) /= Right'Length (1)
or else
Left'Length (2) /= Right'Length (2)
@@ -439,7 +544,19 @@ package body System.Generic_Array_Operations is
Right
(J - R'First (1) + Right'First (1),
K - R'First (2) + Right'First (2)));
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
end loop;
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'Range (2) => R (J, KK)'Initialized);
end loop;
end return;
end Matrix_Matrix_Elementwise_Operation;
@@ -454,7 +571,9 @@ package body System.Generic_Array_Operations is
Z : Z_Scalar) return Result_Matrix
is
begin
- return R : Result_Matrix (X'Range (1), X'Range (2)) do
+ return R : Result_Matrix (X'Range (1), X'Range (2))
+ with Relaxed_Initialization
+ do
if X'Length (1) /= Y'Length (1)
or else
X'Length (2) /= Y'Length (2)
@@ -471,7 +590,19 @@ package body System.Generic_Array_Operations is
Y (J - R'First (1) + Y'First (1),
K - R'First (2) + Y'First (2)),
Z);
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
end loop;
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'Range (2) => R (J, KK)'Initialized);
end loop;
end return;
end Matrix_Matrix_Scalar_Elementwise_Operation;
@@ -527,11 +658,25 @@ package body System.Generic_Array_Operations is
Right : Right_Scalar) return Result_Matrix
is
begin
- return R : Result_Matrix (Left'Range (1), Left'Range (2)) do
+ return R : Result_Matrix (Left'Range (1), Left'Range (2))
+ with Relaxed_Initialization
+ do
for J in R'Range (1) loop
for K in R'Range (2) loop
R (J, K) := Operation (Left (J, K), Right);
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
end loop;
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'Range (2) => R (J, KK)'Initialized);
end loop;
end return;
end Matrix_Scalar_Elementwise_Operation;
@@ -561,11 +706,25 @@ package body System.Generic_Array_Operations is
Right : Right_Matrix) return Result_Matrix
is
begin
- return R : Result_Matrix (Right'Range (1), Right'Range (2)) do
+ return R : Result_Matrix (Right'Range (1), Right'Range (2))
+ with Relaxed_Initialization
+ do
for J in R'Range (1) loop
for K in R'Range (2) loop
R (J, K) := Operation (Left, Right (J, K));
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
end loop;
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'Range (2) => R (J, KK)'Initialized);
end loop;
end return;
end Scalar_Matrix_Elementwise_Operation;
@@ -590,7 +749,9 @@ package body System.Generic_Array_Operations is
-- Sqrt --
----------
- function Sqrt (X : Real'Base) return Real'Base is
+ function Sqrt (X : Real'Base) return Real'Base
+ with SPARK_Mode => Off -- Not in SPARK due to use of Real'Exponent
+ is
Root, Next : Real'Base;
begin
@@ -651,7 +812,9 @@ package body System.Generic_Array_Operations is
Right : Right_Matrix) return Result_Matrix
is
begin
- return R : Result_Matrix (Left'Range (1), Right'Range (2)) do
+ return R : Result_Matrix (Left'Range (1), Right'Range (2))
+ with Relaxed_Initialization
+ do
if Left'Length (2) /= Right'Length (1) then
raise Constraint_Error with
"incompatible dimensions in matrix multiplication";
@@ -671,7 +834,19 @@ package body System.Generic_Array_Operations is
R (J, K) := S;
end;
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
end loop;
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'Range (2) => R (J, KK)'Initialized);
end loop;
end return;
end Matrix_Matrix_Product;
@@ -681,10 +856,21 @@ package body System.Generic_Array_Operations is
----------------------------
function Matrix_Vector_Solution (A : Matrix; X : Vector) return Vector is
+
+ procedure Ignore (M : Matrix)
+ with
+ Ghost,
+ Depends => (null => M);
+
+ procedure Ignore (M : Matrix) is null;
+ -- Ghost procedure to document that the value of argument M is ignored,
+ -- which prevents a warning being issued about the value not being used
+ -- in the rest of the code.
+
N : constant Natural := A'Length (1);
MA : Matrix := A;
- MX : Matrix (A'Range (1), 1 .. 1);
- R : Vector (A'Range (2));
+ MX : Matrix (A'Range (1), 1 .. 1) with Relaxed_Initialization;
+ R : Vector (A'Range (2)) with Relaxed_Initialization;
Det : Scalar;
begin
@@ -698,18 +884,29 @@ package body System.Generic_Array_Operations is
for J in 0 .. MX'Length (1) - 1 loop
MX (MX'First (1) + J, 1) := X (X'First + J);
+
+ pragma Loop_Invariant
+ (for all JJ in MX'First (1) .. MX'First (1) + J =>
+ MX (JJ, 1)'Initialized);
end loop;
Forward_Eliminate (MA, MX, Det);
if Det = Zero then
raise Constraint_Error with "matrix is singular";
+ pragma Annotate
+ (GNATprove, Intentional, "exception might be raised",
+ "An exception should be raised on a singular matrix");
end if;
Back_Substitute (MA, MX);
+ Ignore (MA);
for J in 0 .. R'Length - 1 loop
R (R'First + J) := MX (MX'First (1) + J, 1);
+
+ pragma Loop_Invariant
+ (for all JJ in R'First .. R'First + J => R (JJ)'Initialized);
end loop;
return R;
@@ -720,9 +917,20 @@ package body System.Generic_Array_Operations is
----------------------------
function Matrix_Matrix_Solution (A, X : Matrix) return Matrix is
+
+ procedure Ignore (M : Matrix)
+ with
+ Ghost,
+ Depends => (null => M);
+
+ procedure Ignore (M : Matrix) is null;
+ -- Ghost procedure to document that the value of argument M is ignored,
+ -- which prevents a warning being issued about the value not being used
+ -- in the rest of the code.
+
N : constant Natural := A'Length (1);
- MA : Matrix (A'Range (2), A'Range (2));
- MB : Matrix (A'Range (2), X'Range (2));
+ MA : Matrix (A'Range (2), A'Range (2)) with Relaxed_Initialization;
+ MB : Matrix (A'Range (2), X'Range (2)) with Relaxed_Initialization;
Det : Scalar;
begin
@@ -737,20 +945,53 @@ package body System.Generic_Array_Operations is
for J in 0 .. A'Length (1) - 1 loop
for K in MA'Range (2) loop
MA (MA'First (1) + J, K) := A (A'First (1) + J, K);
+
+ pragma Loop_Invariant
+ (for all JJ in MA'First (1) .. MA'First (1) + J
+ when JJ /= MA'First (1) + J
+ =>
+ (for all KK in MA'Range (2) =>
+ MA (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in MA'First (2) .. K =>
+ MA (MA'First (1) + J, KK)'Initialized);
end loop;
for K in MB'Range (2) loop
MB (MB'First (1) + J, K) := X (X'First (1) + J, K);
+
+ pragma Loop_Invariant
+ (for all JJ in MB'First (1) .. MB'First (1) + J
+ when JJ /= MB'First (1) + J
+ =>
+ (for all KK in MB'Range (2) =>
+ MB (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in MB'First (2) .. K =>
+ MB (MB'First (1) + J, KK)'Initialized);
end loop;
+
+ pragma Loop_Invariant
+ (for all JJ in MA'First (1) .. MA'First (1) + J =>
+ (for all KK in MA'Range (2) =>
+ MA (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all JJ in MB'First (1) .. MB'First (1) + J =>
+ (for all KK in MB'Range (2) =>
+ MB (JJ, KK)'Initialized));
end loop;
Forward_Eliminate (MA, MB, Det);
if Det = Zero then
raise Constraint_Error with "matrix is singular";
+ pragma Annotate
+ (GNATprove, Intentional, "exception might be raised",
+ "An exception should be raised on a singular matrix");
end if;
Back_Substitute (MA, MB);
+ Ignore (MA);
return MB;
end Matrix_Matrix_Solution;
@@ -795,11 +1036,25 @@ package body System.Generic_Array_Operations is
Right : Right_Vector) return Matrix
is
begin
- return R : Matrix (Left'Range, Right'Range) do
+ return R : Matrix (Left'Range, Right'Range)
+ with Relaxed_Initialization
+ do
for J in R'Range (1) loop
for K in R'Range (2) loop
R (J, K) := Left (J) * Right (K);
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
end loop;
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all KK in R'Range (2) => R (JJ, KK)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'Range (2) => R (J, KK)'Initialized);
end loop;
end return;
end Outer_Product;
@@ -828,7 +1083,17 @@ package body System.Generic_Array_Operations is
for K in R'Range (2) loop
R (J, K) := A (K - R'First (2) + A'First (1),
J - R'First (1) + A'First (2));
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J when JJ /= J =>
+ (for all K in R'Range (2) => R (JJ, K)'Initialized));
+ pragma Loop_Invariant
+ (for all KK in R'First (2) .. K => R (J, KK)'Initialized);
end loop;
+
+ pragma Loop_Invariant
+ (for all JJ in R'First (1) .. J =>
+ (for all K in R'Range (2) => R (JJ, K)'Initialized));
end loop;
end Transpose;
diff --git a/gcc/ada/libgnat/s-gearop.ads b/gcc/ada/libgnat/s-gearop.ads
index 340cf96f218..a3c0239fa07 100644
--- a/gcc/ada/libgnat/s-gearop.ads
+++ b/gcc/ada/libgnat/s-gearop.ads
@@ -29,8 +29,29 @@
-- --
------------------------------------------------------------------------------
-package System.Generic_Array_Operations is
-pragma Pure (Generic_Array_Operations);
+-- Proof of this unit is only done up to silver level, i.e. absence of runtime
+-- errors, and only regarding runtime checks that depend on the generic part,
+-- ignoring runtime checks related to formal generic subprogram parameters
+-- in instantiations. For example, contracts do not protect against scalar
+-- overflows in arithmetic operations passed on as formal generic subprogram
+-- parameters.
+
+-- 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.Generic_Array_Operations
+ with SPARK_Mode
+is
+
+ pragma Pure (Generic_Array_Operations);
---------------------
-- Back_Substitute --
@@ -43,7 +64,10 @@ pragma Pure (Generic_Array_Operations);
with function "*" (Left, Right : Scalar) return Scalar is <>;
with function "/" (Left, Right : Scalar) return Scalar is <>;
with function Is_Non_Zero (X : Scalar) return Boolean is <>;
- procedure Back_Substitute (M, N : in out Matrix);
+ procedure Back_Substitute (M, N : in out Matrix)
+ with
+ Pre => M'First (1) = N'First (1)
+ and then M'Last (1) = N'Last (1);
--------------
-- Diagonal --
@@ -53,7 +77,14 @@ pragma Pure (Generic_Array_Operations);
type Scalar is private;
type Vector is array (Integer range <>) of Scalar;
type Matrix is array (Integer range <>, Integer range <>) of Scalar;
- function Diagonal (A : Matrix) return Vector;
+ function Diagonal (A : Matrix) return Vector
+ with
+ Pre => A'First (1) < A'Last (1)
+ and then A'First (2) < A'Last (2)
+ and then (if A'First (1) <= 0 then
+ A'Last (1) < Integer'Last + A'First (1))
+ and then (if A'First (2) <= 0 then
+ A'Last (2) < Integer'Last + A'First (2));
-----------------------
-- Forward_Eliminate --
@@ -76,7 +107,10 @@ pragma Pure (Generic_Array_Operations);
procedure Forward_Eliminate
(M : in out Matrix;
N : in out Matrix;
- Det : out Scalar);
+ Det : out Scalar)
+ with
+ Pre => M'First (1) = N'First (1)
+ and then M'Last (1) = N'Last (1);
--------------------------
-- Square_Matrix_Length --
@@ -85,8 +119,14 @@ pragma Pure (Generic_Array_Operations);
generic
type Scalar is private;
type Matrix is array (Integer range <>, Integer range <>) of Scalar;
- function Square_Matrix_Length (A : Matrix) return Natural;
- -- If A is non-square, raise Constraint_Error, else return its dimension
+ function Square_Matrix_Length (A : Matrix) return Natural
+ with
+ Pre => (if A'First (1) <= 0 then
+ A'Last (1) < Integer'Last + A'First (1))
+ and then (if A'First (2) <= 0 then
+ A'Last (2) < Integer'Last + A'First (2))
+ and then A'Length (1) = A'Length (2);
+ -- If A is non-square, raise Constraint_Error, else return its dimension
----------------------------------
-- Vector_Elementwise_Operation --
@@ -129,7 +169,13 @@ pragma Pure (Generic_Array_Operations);
Right : Right_Scalar) return Result_Scalar;
function Vector_Vector_Elementwise_Operation
(Left : Left_Vector;
- Right : Right_Vector) return Result_Vector;
+ Right : Right_Vector) return Result_Vector
+ with
+ Pre => (if Left'First <= 0 then
+ Left'Last < Integer'Last + Left'First)
+ and then (if Right'First <= 0 then
+ Right'Last < Integer'Last + Right'First)
+ and then Left'Length = Right'Length;
------------------------------------------------
-- Vector_Vector_Scalar_Elementwise_Operation --
@@ -150,7 +196,11 @@ pragma Pure (Generic_Array_Operations);
function Vector_Vector_Scalar_Elementwise_Operation
(X : X_Vector;
Y : Y_Vector;
- Z : Z_Scalar) return Result_Vector;
+ Z : Z_Scalar) return Result_Vector
+ with
+ Pre => (if X'First <= 0 then X'Last < Integer'Last + X'First)
+ and then (if Y'First <= 0 then Y'Last < Integer'Last + Y'First)
+ and then X'Length = Y'Length;
-----------------------------------------
-- Matrix_Matrix_Elementwise_Operation --
@@ -171,7 +221,18 @@ pragma Pure (Generic_Array_Operations);
Right : Right_Scalar) return Result_Scalar;
function Matrix_Matrix_Elementwise_Operation
(Left : Left_Matrix;
- Right : Right_Matrix) return Result_Matrix;
+ Right : Right_Matrix) return Result_Matrix
+ with
+ Pre => (if Left'First (1) <= 0 then
+ Left'Last (1) < Integer'Last + Left'First (1))
+ and then (if Right'First (1) <= 0 then
+ Right'Last (1) < Integer'Last + Right'First (1))
+ and then Left'Length (1) = Right'Length (1)
+ and then (if Left'First (2) <= 0 then
+ Left'Last (2) < Integer'Last + Left'First (2))
+ and then (if Right'First (2) <= 0 then
+ Right'Last (2) < Integer'Last + Right'First (2))
+ and then Left'Length (2) = Right'Length (2);
------------------------------------------------
-- Matrix_Matrix_Scalar_Elementwise_Operation --
@@ -193,7 +254,18 @@ pragma Pure (Generic_Array_Operations);
function Matrix_Matrix_Scalar_Elementwise_Operation
(X : X_Matrix;
Y : Y_Matrix;
- Z : Z_Scalar) return Result_Matrix;
+ Z : Z_Scalar) return Result_Matrix
+ with
+ Pre => (if X'First (1) <= 0 then
+ X'Last (1) < Integer'Last + X'First (1))
+ and then (if Y'First (1) <= 0 then
+ Y'Last (1) < Integer'Last + Y'First (1))
+ and then X'Length (1) = Y'Length (1)
+ and then (if X'First (2) <= 0 then
+ X'Last (2) < Integer'Last + X'First (2))
+ and then (if Y'First (2) <= 0 then
+ Y'Last (2) < Integer'Last + Y'First (2))
+ and then X'Length (2) = Y'Length (2);
-----------------------------------------
-- Vector_Scalar_Elementwise_Operation --
@@ -286,7 +358,13 @@ pragma Pure (Generic_Array_Operations);
Right : Result_Scalar) return Result_Scalar is <>;
function Inner_Product
(Left : Left_Vector;
- Right : Right_Vector) return Result_Scalar;
+ Right : Right_Vector) return Result_Scalar
+ with
+ Pre => (if Left'First <= 0 then
+ Left'Last < Integer'Last + Left'First)
+ and then (if Right'First <= 0 then
+ Right'Last < Integer'Last + Right'First)
+ and then Left'Length = Right'Length;
-------------
-- L2_Norm --
@@ -340,7 +418,13 @@ pragma Pure (Generic_Array_Operations);
Right : Result_Scalar) return Result_Scalar is <>;
function Matrix_Vector_Product
(Left : Matrix;
- Right : Right_Vector) return Result_Vector;
+ Right : Right_Vector) return Result_Vector
+ with
+ Pre => (if Left'First (2) <= 0 then
+ Left'Last (2) < Integer'Last + Left'First (2))
+ and then (if Right'First <= 0 then
+ Right'Last < Integer'Last + Right'First)
+ and then Left'Length (2) = Right'Length;
---------------------------
-- Vector_Matrix_Product --
@@ -363,7 +447,13 @@ pragma Pure (Generic_Array_Operations);
Right : Result_Scalar) return Result_Scalar is <>;
function Vector_Matrix_Product
(Left : Left_Vector;
- Right : Matrix) return Result_Vector;
+ Right : Matrix) return Result_Vector
+ with
+ Pre => (if Left'First <= 0 then
+ Left'Last < Integer'Last + Left'First)
+ and then (if Right'First (1) <= 0 then
+ Right'Last (1) < Integer'Last + Right'First (1))
+ and then Left'Length = Right'Length (1);
---------------------------
-- Matrix_Matrix_Product --
@@ -388,7 +478,13 @@ pragma Pure (Generic_Array_Operations);
Right : Result_Scalar) return Result_Scalar is <>;
function Matrix_Matrix_Product
(Left : Left_Matrix;
- Right : Right_Matrix) return Result_Matrix;
+ Right : Right_Matrix) return Result_Matrix
+ with
+ Pre => (if Left'First (2) <= 0 then
+ Left'Last (2) < Integer'Last + Left'First (2))
+ and then (if Right'First (1) <= 0 then
+ Right'Last (1) < Integer'Last + Right'First (1))
+ and then Left'Length (2) = Right'Length (1);
----------------------------
-- Matrix_Vector_Solution --
@@ -404,7 +500,16 @@ pragma Pure (Generic_Array_Operations);
(M : in out Matrix;
N : in out Matrix;
Det : out Scalar) is <>;
- function Matrix_Vector_Solution (A : Matrix; X : Vector) return Vector;
+ function Matrix_Vector_Solution (A : Matrix; X : Vector) return Vector
+ with
+ Pre => (if A'First (1) <= 0 then
+ A'Last (1) < Integer'Last + A'First (1))
+ and then (if A'First (2) <= 0 then
+ A'Last (2) < Integer'Last + A'First (2))
+ and then A'Length (1) = A'Length (2)
+ and then (if X'First <= 0 then
+ X'Last < Integer'Last + X'First)
+ and then A'Length (1) = X'Length;
----------------------------
-- Matrix_Matrix_Solution --
@@ -419,7 +524,16 @@ pragma Pure (Generic_Array_Operations);
(M : in out Matrix;
N : in out Matrix;
Det : out Scalar) is <>;
- function Matrix_Matrix_Solution (A : Matrix; X : Matrix) return Matrix;
+ function Matrix_Matrix_Solution (A : Matrix; X : Matrix) return Matrix
+ with
+ Pre => (if A'First (1) <= 0 then
+ A'Last (1) < Integer'Last + A'First (1))
+ and then (if A'First (2) <= 0 then
+ A'Last (2) < Integer'Last + A'First (2))
+ and then A'Length (1) = A'Length (2)
+ and then (if X'First (1) <= 0 then
+ X'Last (1) < Integer'Last + X'First (1))
+ and then A'Length (1) = X'Length (1);
----------
-- Sqrt --
@@ -436,7 +550,10 @@ pragma Pure (Generic_Array_Operations);
generic
type Scalar is private;
type Matrix is array (Integer range <>, Integer range <>) of Scalar;
- procedure Swap_Column (A : in out Matrix; Left, Right : Integer);
+ procedure Swap_Column (A : in out Matrix; Left, Right : Integer)
+ with
+ Pre => Left in A'Range (2)
+ and then Right in A'Range (2);
---------------
-- Transpose --
@@ -445,7 +562,18 @@ pragma Pure (Generic_Array_Operations);
generic
type Scalar is private;
type Matrix is array (Integer range <>, Integer range <>) of Scalar;
- procedure Transpose (A : Matrix; R : out Matrix);
+ procedure Transpose (A : Matrix; R : out Matrix)
+ with
+ Relaxed_Initialization => R,
+ Pre => A'First (1) = R'First (2)
+ and then A'Last (1) = R'Last (2)
+ and then A'First (2) = R'First (1)
+ and then A'Last (2) = R'Last (1)
+ and then (if A'First (1) < 0 then
+ A'Last (1) <= Integer'Last + A'First (1))
+ and then (if A'First (2) < 0 then
+ A'Last (2) <= Integer'Last + A'First (2)),
+ Post => R'Initialized;
-------------------------------
-- Update_Vector_With_Vector --
@@ -457,7 +585,13 @@ pragma Pure (Generic_Array_Operations);
type X_Vector is array (Integer range <>) of X_Scalar;
type Y_Vector is array (Integer range <>) of Y_Scalar;
with procedure Update (X : in out X_Scalar; Y : Y_Scalar);
- procedure Update_Vector_With_Vector (X : in out X_Vector; Y : Y_Vector);
+ procedure Update_Vector_With_Vector (X : in out X_Vector; Y : Y_Vector)
+ with
+ Pre => (if X'First <= 0 then
+ X'Last < Integer'Last + X'First)
+ and then (if Y'First <= 0 then
+ Y'Last < Integer'Last + Y'First)
+ and then X'Length = Y'Length;
-------------------------------
-- Update_Matrix_With_Matrix --
@@ -469,7 +603,18 @@ pragma Pure (Generic_Array_Operations);
type X_Matrix is array (Integer range <>, Integer range <>) of X_Scalar;
type Y_Matrix is array (Integer range <>, Integer range <>) of Y_Scalar;
with procedure Update (X : in out X_Scalar; Y : Y_Scalar);
- procedure Update_Matrix_With_Matrix (X : in out X_Matrix; Y : Y_Matrix);
+ procedure Update_Matrix_With_Matrix (X : in out X_Matrix; Y : Y_Matrix)
+ with
+ Pre => (if X'First (1) <= 0 then
+ X'Last (1) < Integer'Last + X'First (1))
+ and then (if Y'First (1) <= 0 then
+ Y'Last (1) < Integer'Last + Y'First (1))
+ and then X'Length (1) = Y'Length (1)
+ and then (if X'First (2) <= 0 then
+ X'Last (2) < Integer'Last + X'First (2))
+ and then (if Y'First (2) <= 0 then
+ Y'Last (2) < Integer'Last + Y'First (2))
+ and then X'Length (2) = Y'Length (2);
-----------------
-- Unit_Matrix --
@@ -483,7 +628,10 @@ pragma Pure (Generic_Array_Operations);
function Unit_Matrix
(Order : Positive;
First_1 : Integer := 1;
- First_2 : Integer := 1) return Matrix;
+ First_2 : Integer := 1) return Matrix
+ with
+ Pre => First_1 <= Integer'Last - Order + 1
+ and then First_2 <= Integer'Last - Order + 1;
-----------------
-- Unit_Vector --
@@ -497,6 +645,10 @@ pragma Pure (Generic_Array_Operations);
function Unit_Vector
(Index : Integer;
Order : Positive;
- First : Integer := 1) return Vector;
+ First : Integer := 1) return Vector
+ with
+ Pre => Index >= First
+ and then First <= Integer'Last - Order + 1
+ and then Index <= First + (Order - 1);
end System.Generic_Array_Operations;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-01-06 17:14 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-01-06 17:14 [gcc r12-6315] [Ada] Proof of System.Generic_Array_Operations at silver level Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).