* [COMMITTED] ada: Fix proof of runtime unit System.Value*
@ 2023-05-15 9:42 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2023-05-15 9:42 UTC (permalink / raw)
To: gcc-patches; +Cc: Claire Dross
From: Claire Dross <dross@adacore.com>
Use cut operations to restore the proof of System.Value*.
gcc/ada/
* libgnat/s-valueu.adb: Use cut operations inside assertion to
restore proofs
* gcc-interface/Make-lang.in (GNAT_ADA_OBJS): Add s-spark and
s-spcuop dependencies.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/gcc-interface/Make-lang.in | 2 +
gcc/ada/libgnat/s-valueu.adb | 92 ++++++++++++++++++++----------
2 files changed, 64 insertions(+), 30 deletions(-)
diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in
index 9507f2f0920..7b826f2366f 100644
--- a/gcc/ada/gcc-interface/Make-lang.in
+++ b/gcc/ada/gcc-interface/Make-lang.in
@@ -536,6 +536,8 @@ GNAT_ADA_OBJS+= \
ada/libgnat/s-secsta.o \
ada/libgnat/s-soflin.o \
ada/libgnat/s-soliin.o \
+ ada/libgnat/s-spark.o \
+ ada/libgnat/s-spcuop.o \
ada/libgnat/s-stache.o \
ada/libgnat/s-stalib.o \
ada/libgnat/s-stoele.o \
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
index c6e26b0ee1f..bc6ed1ca669 100644
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -29,6 +29,8 @@
-- --
------------------------------------------------------------------------------
+with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations;
+
package body System.Value_U is
-- Ghost code, loop invariants and assertions in this unit are meant for
@@ -174,6 +176,7 @@ package body System.Value_U is
P := Ptr.all;
Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init);
Uval := Character'Pos (Str (P)) - Character'Pos ('0');
+ pragma Assert (Str (P) in '0' .. '9');
P := P + 1;
-- Scan out digits of what is either the number or the base.
@@ -215,19 +218,24 @@ package body System.Value_U is
-- Accumulate result, checking for overflow
else
+ pragma Assert
+ (By
+ (Str (P) in '0' .. '9',
+ By
+ (Character'Pos (Str (P)) >= Character'Pos ('0'),
+ Uns '(Character'Pos (Str (P))) >=
+ Character'Pos ('0'))));
Spec.Lemma_Scan_Based_Number_Ghost_Step
(Str, P, Last_Num_Init, Acc => Uval);
Spec.Lemma_Scan_Based_Number_Ghost_Overflow
(Str, P, Last_Num_Init, Acc => Uval);
if Uval <= Umax then
- pragma Assert
- (Spec.Hexa_To_Unsigned_Ghost (Str (P)) = Digit);
Uval := 10 * Uval + Digit;
pragma Assert
(if not Overflow
then Init_Val = Spec.Scan_Based_Number_Ghost
- (Str, P + 1, Last_Num_Init, Acc => Uval));
+ (Str, P + 1, Last_Num_Init, Acc => Uval));
elsif Uval > Umax10 then
Overflow := True;
@@ -241,7 +249,8 @@ package body System.Value_U is
pragma Assert
(if not Overflow
then Init_Val = Spec.Scan_Based_Number_Ghost
- (Str, P + 1, Last_Num_Init, Acc => Uval));
+ (Str, P + 1, Last_Num_Init, Acc => Uval));
+
end if;
P := P + 1;
@@ -252,7 +261,9 @@ package body System.Value_U is
end;
pragma Assert_And_Cut
- (P = Last_Num_Init + 1
+ (By
+ (P = Last_Num_Init + 1,
+ P > Max or else Str (P) not in '_' | '0' .. '9')
and then Overflow = Init_Val.Overflow
and then (if not Overflow then Init_Val.Value = Uval));
@@ -313,13 +324,24 @@ package body System.Value_U is
-- already stored in Ptr.all.
else
+ pragma Assert
+ (By
+ (Spec.Only_Hexa_Ghost (Str, P, Last_Num_Based),
+ P > Last_Num_Init + 1
+ and Spec.Only_Hexa_Ghost
+ (Str, Last_Num_Init + 2, Last_Num_Based)));
Spec.Lemma_Scan_Based_Number_Ghost_Base
(Str, P, Last_Num_Based, Base, Uval);
Uval := Base;
Base := 10;
pragma Assert (Ptr.all = Last_Num_Init + 1);
pragma Assert
- (if Starts_As_Based then P = Last_Num_Based + 1);
+ (if Starts_As_Based
+ then By
+ (P = Last_Num_Based + 1,
+ P <= Last_Num_Based + 1
+ and Str (P) not in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_'));
pragma Assert (not Is_Based);
pragma Assert (if not Overflow then Uval = Init_Val.Value);
exit;
@@ -394,11 +416,15 @@ package body System.Value_U is
Ptr.all := P + 1;
pragma Assert (P = Last_Num_Based + 1);
pragma Assert (Ptr.all = Last_Num_Based + 2);
- pragma Assert (Starts_As_Based);
- pragma Assert (Last_Num_Based < Max);
- pragma Assert (Str (Last_Num_Based + 1) = Base_Char);
- pragma Assert (Base_Char = Str (Last_Num_Init + 1));
- pragma Assert (Is_Based);
+ pragma Assert
+ (By
+ (Is_Based,
+ So
+ (Starts_As_Based,
+ So
+ (Last_Num_Based < Max,
+ Str (Last_Num_Based + 1) = Base_Char
+ and Base_Char = Str (Last_Num_Init + 1)))));
Spec.Lemma_Scan_Based_Number_Ghost_Base
(Str, P, Last_Num_Based, Base, Uval);
exit;
@@ -414,41 +440,40 @@ package body System.Value_U is
(if not Overflow
then Based_Val = Spec.Scan_Based_Number_Ghost
(Str, P, Last_Num_Based, Base, Uval));
- pragma Assert (Str (P) /= '_');
- pragma Assert (Str (P) /= Base_Char);
+ pragma Assert (Str (P) not in '_' | Base_Char);
end if;
Lemma_Digit_Not_Last (Str, P, Last_Num_Init + 2, Max);
- pragma Assert (Str (P) /= '_');
- pragma Assert (Str (P) /= Base_Char);
+ pragma Assert (Str (P) not in '_' | Base_Char);
end loop;
end;
pragma Assert
(if Starts_As_Based then P = Last_Num_Based + 1
else P = Last_Num_Init + 2);
pragma Assert
- (Last_Num_Init < Max - 1
- and then Str (Last_Num_Init + 1) in '#' | ':');
- pragma Assert
- (Overflow =
- (Init_Val.Overflow
- or else Init_Val.Value not in 2 .. 16
- or else (Starts_As_Based and then Based_Val.Overflow)));
- pragma Assert
- (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max));
+ (By
+ (Overflow /= Spec.Scan_Split_No_Overflow_Ghost
+ (Str, Ptr_Old, Max),
+ So
+ (Last_Num_Init < Max - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':',
+ Overflow =
+ (Init_Val.Overflow
+ or else Init_Val.Value not in 2 .. 16
+ or else (Starts_As_Based and Based_Val.Overflow)))));
end if;
pragma Assert_And_Cut
(Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max)
- and then
- (if not Overflow then
- (if Is_Based then Uval = Based_Val.Value
- else Uval = Init_Val.Value))
and then Ptr.all = First_Exp
and then Base in 2 .. 16
and then
(if not Overflow then
- (if Is_Based then Base = Init_Val.Value else Base = 10)));
+ (if Is_Based then Base = Init_Val.Value else Base = 10))
+ and then
+ (if not Overflow then
+ (if Is_Based then Uval = Based_Val.Value
+ else Uval = Init_Val.Value)));
-- Come here with scanned unsigned value in Uval. The only remaining
-- required step is to deal with exponent if one is present.
@@ -456,7 +481,14 @@ package body System.Value_U is
Scan_Exponent (Str, Ptr, Max, Expon);
pragma Assert
- (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max));
+ (By
+ (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max),
+ (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max))
+ then Ptr.all = First_Exp
+ elsif Str (First_Exp + 1) in '-' | '+' then
+ Ptr.all = Last_Number_Ghost (Str (First_Exp + 2 .. Max)) + 1
+ else Ptr.all =
+ Last_Number_Ghost (Str (First_Exp + 1 .. Max)) + 1)));
pragma Assert
(if not Overflow
then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) =
--
2.40.0
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-05-15 9:42 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-05-15 9:42 [COMMITTED] ada: Fix proof of runtime unit System.Value* Marc Poulhiès
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).