This proves the generic unit System.Expont instantiated for Integer,
Long_Long_Integer and Long_Long_Long_Integer. The proof is similar to
the one done for the same units with checks off. In this case too, the
generic function is changed into a generic package.
GNATprove is called with switch --level=2.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-expint.ads: Mark in SPARK. Adapt to change to
package.
* libgnat/s-explli.ads: Likewise.
* libgnat/s-expllli.ads: Likewise.
* libgnat/s-expont.adb: Add lemmas and ghost code.
* libgnat/s-expont.ads: Add functional contract.diff --git a/gcc/ada/libgnat/s-expint.ads b/gcc/ada/libgnat/s-expint.ads
--- a/gcc/ada/libgnat/s-expint.ads
+++ b/gcc/ada/libgnat/s-expint.ads
@@ -31,11 +31,26 @@
-- Integer exponentiation (checks on)
+-- 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.Expont;
-package System.Exp_Int is
+package System.Exp_Int
+ with SPARK_Mode
+is
+
+ package Expont_Integer is new Expont (Integer);
- function Exp_Integer is new Expont (Integer);
- pragma Pure_Function (Exp_Integer);
+ function Exp_Integer (Left : Integer; Right : Natural) return Integer
+ renames Expont_Integer.Expon;
end System.Exp_Int;
diff --git a/gcc/ada/libgnat/s-explli.ads b/gcc/ada/libgnat/s-explli.ads
--- a/gcc/ada/libgnat/s-explli.ads
+++ b/gcc/ada/libgnat/s-explli.ads
@@ -31,11 +31,27 @@
-- Long_Long_Integer exponentiation (checks on)
+-- 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.Expont;
-package System.Exp_LLI is
+package System.Exp_LLI
+ with SPARK_Mode
+is
+
+ package Expont_Integer is new Expont (Long_Long_Integer);
- function Exp_Long_Long_Integer is new Expont (Long_Long_Integer);
- pragma Pure_Function (Exp_Long_Long_Integer);
+ function Exp_Long_Long_Integer
+ (Left : Long_Long_Integer; Right : Natural) return Long_Long_Integer
+ renames Expont_Integer.Expon;
end System.Exp_LLI;
diff --git a/gcc/ada/libgnat/s-expllli.ads b/gcc/ada/libgnat/s-expllli.ads
--- a/gcc/ada/libgnat/s-expllli.ads
+++ b/gcc/ada/libgnat/s-expllli.ads
@@ -31,11 +31,28 @@
-- Long_Long_Long_Integer exponentiation (checks on)
+-- 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.Expont;
-package System.Exp_LLLI is
+package System.Exp_LLLI
+ with SPARK_Mode
+is
+
+ package Expont_Integer is new Expont (Long_Long_Long_Integer);
- function Exp_Long_Long_Long_Integer is new Expont (Long_Long_Long_Integer);
- pragma Pure_Function (Exp_Long_Long_Long_Integer);
+ function Exp_Long_Long_Long_Integer
+ (Left : Long_Long_Long_Integer; Right : Natural)
+ return Long_Long_Long_Integer
+ renames Expont_Integer.Expon;
end System.Exp_LLLI;
diff --git a/gcc/ada/libgnat/s-expont.adb b/gcc/ada/libgnat/s-expont.adb
--- a/gcc/ada/libgnat/s-expont.adb
+++ b/gcc/ada/libgnat/s-expont.adb
@@ -29,44 +29,198 @@
-- --
------------------------------------------------------------------------------
-function System.Expont (Left : Int; Right : Natural) return Int is
+package body System.Expont
+ with SPARK_Mode
+is
- -- Note that negative exponents get a constraint error because the
- -- subtype of the Right argument (the exponent) is Natural.
+ -- 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.
- Result : Int := 1;
- Factor : Int := Left;
- Exp : Natural := Right;
+ pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
-begin
- -- We use the standard logarithmic approach, Exp gets shifted right
- -- testing successive low order bits and Factor is the value of the
- -- base raised to the next power of 2.
+ -- Local lemmas
- -- Note: it is not worth special casing base values -1, 0, +1 since
- -- the expander does this when the base is a literal, and other cases
- -- will be extremely rare.
+ procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural)
+ with
+ Ghost,
+ Pre => A /= 0,
+ Post =>
+ (if Exp rem 2 = 0 then
+ A ** Exp = A ** (Exp / 2) * A ** (Exp / 2)
+ else
+ A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+
+ procedure Lemma_Exp_In_Range (A : Big_Integer; Exp : Positive)
+ with
+ Ghost,
+ Pre => In_Int_Range (A ** Exp * A ** Exp),
+ Post => In_Int_Range (A * A);
+
+ procedure Lemma_Exp_Not_Zero (A : Big_Integer; Exp : Natural)
+ with
+ Ghost,
+ Pre => A /= 0,
+ Post => A ** Exp /= 0;
+
+ procedure Lemma_Exp_Positive (A : Big_Integer; Exp : Natural)
+ with
+ Ghost,
+ Pre => A /= 0
+ and then Exp rem 2 = 0,
+ Post => A ** Exp > 0;
+
+ procedure Lemma_Mult_In_Range (X, Y, Z : Big_Integer)
+ with
+ Ghost,
+ Pre => Y /= 0
+ and then not (X = -Big (Int'First) and Y = -1)
+ and then X * Y = Z
+ and then In_Int_Range (Z),
+ Post => In_Int_Range (X);
+
+ -----------------------------
+ -- Local lemma null bodies --
+ -----------------------------
+
+ procedure Lemma_Exp_Not_Zero (A : Big_Integer; Exp : Natural) is null;
+ procedure Lemma_Mult_In_Range (X, Y, Z : Big_Integer) is null;
+
+ -----------
+ -- Expon --
+ -----------
+
+ function Expon (Left : Int; Right : Natural) return Int is
+
+ -- Note that negative exponents get a constraint error because the
+ -- subtype of the Right argument (the exponent) is Natural.
+
+ Result : Int := 1;
+ Factor : Int := Left;
+ Exp : Natural := Right;
+
+ Rest : Big_Integer with Ghost;
+ -- Ghost variable to hold Factor**Exp between Exp and Factor updates
+
+ begin
+ -- We use the standard logarithmic approach, Exp gets shifted right
+ -- testing successive low order bits and Factor is the value of the
+ -- base raised to the next power of 2.
+
+ -- Note: for compilation only, it is not worth special casing base
+ -- values -1, 0, +1 since the expander does this when the base is a
+ -- literal, and other cases will be extremely rare. But for proof,
+ -- special casing zero in both positions makes ghost code and lemmas
+ -- simpler, so we do it.
+
+ if Right = 0 then
+ return 1;
+ elsif Left = 0 then
+ return 0;
+ end if;
- if Exp /= 0 then
loop
+ pragma Loop_Invariant (Exp > 0);
+ pragma Loop_Invariant (Factor /= 0);
+ pragma Loop_Invariant
+ (Big (Result) * Big (Factor) ** Exp = Big (Left) ** Right);
+ pragma Loop_Variant (Decreases => Exp);
+ pragma Annotate
+ (CodePeer, False_Positive,
+ "validity check", "confusion on generated code");
+
if Exp rem 2 /= 0 then
declare
pragma Unsuppress (Overflow_Check);
begin
+ pragma Assert
+ (Big (Factor) ** Exp
+ = Big (Factor) * Big (Factor) ** (Exp - 1));
+ Lemma_Exp_Positive (Big (Factor), Exp - 1);
+ Lemma_Mult_In_Range (Big (Result) * Big (Factor),
+ Big (Factor) ** (Exp - 1),
+ Big (Left) ** Right);
+
Result := Result * Factor;
end;
end if;
+ Lemma_Exp_Expand (Big (Factor), Exp);
+
Exp := Exp / 2;
exit when Exp = 0;
+ Rest := Big (Factor) ** Exp;
+ pragma Assert
+ (Big (Result) * (Rest * Rest) = Big (Left) ** Right);
+
declare
pragma Unsuppress (Overflow_Check);
begin
+ Lemma_Mult_In_Range (Rest * Rest,
+ Big (Result),
+ Big (Left) ** Right);
+ Lemma_Exp_In_Range (Big (Factor), Exp);
+
Factor := Factor * Factor;
end;
+
+ pragma Assert (Big (Factor) ** Exp = Rest * Rest);
end loop;
- end if;
- return Result;
+ pragma Assert (Big (Result) = Big (Left) ** Right);
+
+ return Result;
+ end Expon;
+
+ ----------------------
+ -- Lemma_Exp_Expand --
+ ----------------------
+
+ procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
+ begin
+ if Exp rem 2 = 0 then
+ pragma Assert (Exp = Exp / 2 + Exp / 2);
+ else
+ pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
+ pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
+ pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
+ pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+ end if;
+ end Lemma_Exp_Expand;
+
+ ------------------------
+ -- Lemma_Exp_In_Range --
+ ------------------------
+
+ procedure Lemma_Exp_In_Range (A : Big_Integer; Exp : Positive) is
+ begin
+ if A /= 0 and Exp /= 1 then
+ pragma Assert (A ** Exp = A * A ** (Exp - 1));
+ Lemma_Mult_In_Range
+ (A * A, A ** (Exp - 1) * A ** (Exp - 1), A ** Exp * A ** Exp);
+ end if;
+ end Lemma_Exp_In_Range;
+
+ ------------------------
+ -- Lemma_Exp_Positive --
+ ------------------------
+
+ procedure Lemma_Exp_Positive (A : Big_Integer; Exp : Natural) is
+ begin
+ if Exp = 0 then
+ pragma Assert (A ** Exp = 1);
+ else
+ pragma Assert (Exp = 2 * (Exp / 2));
+ pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2));
+ pragma Assert (A ** Exp = (A ** (Exp / 2)) ** 2);
+ Lemma_Exp_Not_Zero (A, Exp / 2);
+ end if;
+ end Lemma_Exp_Positive;
+
end System.Expont;
diff --git a/gcc/ada/libgnat/s-expont.ads b/gcc/ada/libgnat/s-expont.ads
--- a/gcc/ada/libgnat/s-expont.ads
+++ b/gcc/ada/libgnat/s-expont.ads
@@ -31,8 +31,41 @@
-- Signed integer exponentiation (checks on)
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+
generic
type Int is range <>;
-function System.Expont (Left : Int; Right : Natural) return Int;
+package System.Expont
+ with Pure, SPARK_Mode
+is
+
+ -- 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 Signed_Conversion is new Signed_Conversions (Int => Int);
+
+ function Big (Arg : Int) return Big_Integer is
+ (Signed_Conversion.To_Big_Integer (Arg))
+ with Ghost;
+
+ function In_Int_Range (Arg : Big_Integer) return Boolean is
+ (In_Range (Arg, Big (Int'First), Big (Int'Last)))
+ with Ghost;
+
+ function Expon (Left : Int; Right : Natural) return Int
+ with
+ Pre => In_Int_Range (Big (Left) ** Right),
+ Post => Expon'Result = Left ** Right;
+
+end System.Expont;
