From ed722edd2f4accad60744b95426dba3fc9ca084c Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 2 Dec 2021 10:55:04 +0100 Subject: [PATCH] [Ada] Proof of runtime units for binary modular exponentiation gcc/ada/ * libgnat/s-explllu.ads: Mark in SPARK. * libgnat/s-expllu.ads: Mark in SPARK. * libgnat/s-exponu.adb: Add loop invariants and needed assertions. * libgnat/s-exponu.ads: Add functional contract. * libgnat/s-expuns.ads: Mark in SPARK. --- gcc/ada/libgnat/s-explllu.ads | 15 ++++++++++++++- gcc/ada/libgnat/s-expllu.ads | 15 ++++++++++++++- gcc/ada/libgnat/s-exponu.adb | 23 ++++++++++++++++++++++- gcc/ada/libgnat/s-exponu.ads | 16 +++++++++++++++- gcc/ada/libgnat/s-expuns.ads | 15 ++++++++++++++- 5 files changed, 79 insertions(+), 5 deletions(-) diff --git a/gcc/ada/libgnat/s-explllu.ads b/gcc/ada/libgnat/s-explllu.ads index 5a54ada..eb883a4 100644 --- a/gcc/ada/libgnat/s-explllu.ads +++ b/gcc/ada/libgnat/s-explllu.ads @@ -34,10 +34,23 @@ -- The result is always full width, the caller must do a masking operation if -- the modulus is less than 2 ** Long_Long_Long_Unsigned'Size. +-- 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); + with System.Exponu; with System.Unsigned_Types; -package System.Exp_LLLU is +package System.Exp_LLLU + with SPARK_Mode +is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; diff --git a/gcc/ada/libgnat/s-expllu.ads b/gcc/ada/libgnat/s-expllu.ads index 9f7b404..e028f67 100644 --- a/gcc/ada/libgnat/s-expllu.ads +++ b/gcc/ada/libgnat/s-expllu.ads @@ -34,10 +34,23 @@ -- The result is always full width, the caller must do a masking operation if -- the modulus is less than 2 ** Long_Long_Unsigned'Size. +-- 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); + with System.Exponu; with System.Unsigned_Types; -package System.Exp_LLU is +package System.Exp_LLU + with SPARK_Mode +is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; diff --git a/gcc/ada/libgnat/s-exponu.adb b/gcc/ada/libgnat/s-exponu.adb index 9525638..06ed509 100644 --- a/gcc/ada/libgnat/s-exponu.adb +++ b/gcc/ada/libgnat/s-exponu.adb @@ -29,7 +29,19 @@ -- -- ------------------------------------------------------------------------------ -function System.Exponu (Left : Int; Right : Natural) return Int is +function System.Exponu (Left : Int; Right : Natural) return Int + with SPARK_Mode +is + -- 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); -- Note that negative exponents get a constraint error because the -- subtype of the Right argument (the exponent) is Natural. @@ -49,7 +61,16 @@ begin if Exp /= 0 then loop + pragma Loop_Invariant (Exp > 0); + pragma Loop_Invariant (Result * Factor ** Exp = Left ** Right); + pragma Loop_Variant (Decreases => Exp); + if Exp rem 2 /= 0 then + pragma Assert + (Result * (Factor * Factor ** (Exp - 1)) = Left ** Right); + pragma Assert + ((Result * Factor) * Factor ** (Exp - 1) = Left ** Right); + Result := Result * Factor; end if; diff --git a/gcc/ada/libgnat/s-exponu.ads b/gcc/ada/libgnat/s-exponu.ads index 7faa122..b18a3a4 100644 --- a/gcc/ada/libgnat/s-exponu.ads +++ b/gcc/ada/libgnat/s-exponu.ads @@ -31,8 +31,22 @@ -- Modular integer exponentiation +-- 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); + generic type Int is mod <>; -function System.Exponu (Left : Int; Right : Natural) return Int; +function System.Exponu (Left : Int; Right : Natural) return Int +with + SPARK_Mode, + Post => System.Exponu'Result = Left ** Right; diff --git a/gcc/ada/libgnat/s-expuns.ads b/gcc/ada/libgnat/s-expuns.ads index b49e7c0..751f3fa 100644 --- a/gcc/ada/libgnat/s-expuns.ads +++ b/gcc/ada/libgnat/s-expuns.ads @@ -34,10 +34,23 @@ -- The result is always full width, the caller must do a masking operation if -- the modulus is less than 2 ** Unsigned'Size. +-- 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); + with System.Exponu; with System.Unsigned_Types; -package System.Exp_Uns is +package System.Exp_Uns + with SPARK_Mode +is subtype Unsigned is Unsigned_Types.Unsigned; -- 2.7.4