From: Yannick Moy Date: Wed, 8 Dec 2021 14:09:25 +0000 (-0500) Subject: [Ada] Proof of System.Generic_Array_Operations at silver level X-Git-Tag: upstream/12.2.0~2382 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=42dd6f60d8fefe1b026989d78eabf0108c528e4b;p=platform%2Fupstream%2Fgcc.git [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 --git a/gcc/ada/libgnat/a-ngcoar.adb b/gcc/ada/libgnat/a-ngcoar.adb index ed9be6a..953cb09 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 5095db8..c34cdd6 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 92af09d..e86d982 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 340cf96..a3c0239 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;