From 94396a27bcfbdcb156586688de9a5a2e1bee2d4a Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 2 Nov 2021 15:43:42 +0100 Subject: [Ada] Create explicit ghost mirror unit for big integers gcc/ada/ * Makefile.rtl: Add unit. * libgnat/a-nbnbin__ghost.adb: Move... * libgnat/a-nbnbig.adb: ... here. Mark ghost as ignored. * libgnat/a-nbnbin__ghost.ads: Move... * libgnat/a-nbnbig.ads: ... here. Add comment for purpose of this unit. Mark ghost as ignored. * libgnat/s-widthu.adb: Use new unit. * sem_aux.adb (First_Subtype): Adapt to the case of a ghost type whose freeze node is rewritten to a null statement. --- gcc/ada/Makefile.rtl | 1 + gcc/ada/libgnat/a-nbnbig.adb | 81 ++++++++++++++ gcc/ada/libgnat/a-nbnbig.ads | 216 ++++++++++++++++++++++++++++++++++++ gcc/ada/libgnat/a-nbnbin__ghost.adb | 76 ------------- gcc/ada/libgnat/a-nbnbin__ghost.ads | 202 --------------------------------- gcc/ada/libgnat/s-widthu.adb | 4 +- gcc/ada/sem_aux.adb | 10 +- 7 files changed, 309 insertions(+), 281 deletions(-) create mode 100644 gcc/ada/libgnat/a-nbnbig.adb create mode 100644 gcc/ada/libgnat/a-nbnbig.ads delete mode 100644 gcc/ada/libgnat/a-nbnbin__ghost.adb delete mode 100644 gcc/ada/libgnat/a-nbnbin__ghost.ads (limited to 'gcc') diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl index fb3f6f6..282b25c 100644 --- a/gcc/ada/Makefile.rtl +++ b/gcc/ada/Makefile.rtl @@ -211,6 +211,7 @@ GNATRTL_NONTASKING_OBJS= \ a-lllwti$(objext) \ a-lllzti$(objext) \ a-locale$(objext) \ + a-nbnbig$(objext) \ a-nbnbin$(objext) \ a-nbnbre$(objext) \ a-ncelfu$(objext) \ diff --git a/gcc/ada/libgnat/a-nbnbig.adb b/gcc/ada/libgnat/a-nbnbig.adb new file mode 100644 index 0000000..d04d2a4 --- /dev/null +++ b/gcc/ada/libgnat/a-nbnbig.adb @@ -0,0 +1,81 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT RUN-TIME COMPONENTS -- +-- -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2021, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This body is provided as a work-around for a GNAT compiler bug, as GNAT +-- currently does not compile instantiations of the spec with imported ghost +-- generics for packages Signed_Conversions and Unsigned_Conversions. + +-- Ghost code in this unit is meant for analysis only, not for run-time +-- checking. This is enforced by setting the assertion policy to Ignore. + +pragma Assertion_Policy (Ghost => Ignore); + +package body Ada.Numerics.Big_Numbers.Big_Integers_Ghost with + SPARK_Mode => Off +is + + package body Signed_Conversions with + SPARK_Mode => Off + is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer is + begin + raise Program_Error; + return (null record); + end To_Big_Integer; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int is + begin + raise Program_Error; + return 0; + end From_Big_Integer; + + end Signed_Conversions; + + package body Unsigned_Conversions with + SPARK_Mode => Off + is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer is + begin + raise Program_Error; + return (null record); + end To_Big_Integer; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int is + begin + raise Program_Error; + return 0; + end From_Big_Integer; + + end Unsigned_Conversions; + +end Ada.Numerics.Big_Numbers.Big_Integers_Ghost; diff --git a/gcc/ada/libgnat/a-nbnbig.ads b/gcc/ada/libgnat/a-nbnbig.ads new file mode 100644 index 0000000..237bca1 --- /dev/null +++ b/gcc/ada/libgnat/a-nbnbig.ads @@ -0,0 +1,216 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT RUN-TIME COMPONENTS -- +-- -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST -- +-- -- +-- S p e c -- +-- -- +-- This specification is derived from the Ada Reference Manual for use with -- +-- GNAT. In accordance with the copyright of that document, you can freely -- +-- copy and modify this specification, provided that if you redistribute a -- +-- modified version, any changes that you have made are clearly indicated. -- +-- -- +------------------------------------------------------------------------------ + +-- This unit is provided as a replacement for the standard unit +-- Ada.Numerics.Big_Numbers.Big_Integers when only proof with SPARK is +-- intended. It cannot be used for execution, as all subprograms are marked +-- imported with no definition. + +-- Contrary to Ada.Numerics.Big_Numbers.Big_Integers, this unit does not +-- depend on System or Ada.Finalization, which makes it more convenient for +-- use in run-time units. + +-- Ghost code in this unit is meant for analysis only, not for run-time +-- checking. This is enforced by setting the assertion policy to Ignore. + +pragma Assertion_Policy (Ghost => Ignore); + +package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with + SPARK_Mode, + Ghost, + Preelaborate +is + type Big_Integer is private + with Integer_Literal => From_Universal_Image; + + function Is_Valid (Arg : Big_Integer) return Boolean + with + Import, + Global => null; + + subtype Valid_Big_Integer is Big_Integer + with Dynamic_Predicate => Is_Valid (Valid_Big_Integer), + Predicate_Failure => raise Program_Error; + + function "=" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function "<" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function "<=" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function ">" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function ">=" (L, R : Valid_Big_Integer) return Boolean with + Import, + Global => null; + + function To_Big_Integer (Arg : Integer) return Valid_Big_Integer + with + Import, + Global => null; + + subtype Big_Positive is Big_Integer + with Dynamic_Predicate => + (if Is_Valid (Big_Positive) + then Big_Positive > To_Big_Integer (0)), + Predicate_Failure => (raise Constraint_Error); + + subtype Big_Natural is Big_Integer + with Dynamic_Predicate => + (if Is_Valid (Big_Natural) + then Big_Natural >= To_Big_Integer (0)), + Predicate_Failure => (raise Constraint_Error); + + function In_Range + (Arg : Valid_Big_Integer; Low, High : Big_Integer) return Boolean + is (Low <= Arg and Arg <= High) + with + Import, + Global => null; + + function To_Integer (Arg : Valid_Big_Integer) return Integer + with + Import, + Pre => In_Range (Arg, + Low => To_Big_Integer (Integer'First), + High => To_Big_Integer (Integer'Last)) + or else (raise Constraint_Error), + Global => null; + + generic + type Int is range <>; + package Signed_Conversions is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer + with + Global => null; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int + with + Pre => In_Range (Arg, + Low => To_Big_Integer (Int'First), + High => To_Big_Integer (Int'Last)) + or else (raise Constraint_Error), + Global => null; + end Signed_Conversions; + + generic + type Int is mod <>; + package Unsigned_Conversions is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer + with + Global => null; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int + with + Pre => In_Range (Arg, + Low => To_Big_Integer (Int'First), + High => To_Big_Integer (Int'Last)) + or else (raise Constraint_Error), + Global => null; + + end Unsigned_Conversions; + + function From_String (Arg : String) return Valid_Big_Integer + with + Import, + Global => null; + + function From_Universal_Image (Arg : String) return Valid_Big_Integer + renames From_String; + + function "+" (L : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "-" (L : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer + with + Import, + Global => null; + + function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer + with + Import, + Global => null; + + function Greatest_Common_Divisor + (L, R : Valid_Big_Integer) return Big_Positive + with + Import, + Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0)) + or else (raise Constraint_Error), + Global => null; + +private + pragma SPARK_Mode (Off); + + type Big_Integer is null record; + +end Ada.Numerics.Big_Numbers.Big_Integers_Ghost; diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.adb b/gcc/ada/libgnat/a-nbnbin__ghost.adb deleted file mode 100644 index 7d22086..0000000 --- a/gcc/ada/libgnat/a-nbnbin__ghost.adb +++ /dev/null @@ -1,76 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT RUN-TIME COMPONENTS -- --- -- --- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- --- -- --- B o d y -- --- -- --- Copyright (C) 2021, Free Software Foundation, Inc. -- --- -- --- GNAT is free software; you can redistribute it and/or modify it under -- --- terms of the GNU General Public License as published by the Free Soft- -- --- ware Foundation; either version 3, or (at your option) any later ver- -- --- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- --- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- --- or FITNESS FOR A PARTICULAR PURPOSE. -- --- -- --- As a special exception under Section 7 of GPL version 3, you are granted -- --- additional permissions described in the GCC Runtime Library Exception, -- --- version 3.1, as published by the Free Software Foundation. -- --- -- --- You should have received a copy of the GNU General Public License and -- --- a copy of the GCC Runtime Library Exception along with this program; -- --- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- --- . -- --- -- --- GNAT was originally developed by the GNAT team at New York University. -- --- Extensive contributions were provided by Ada Core Technologies Inc. -- --- -- ------------------------------------------------------------------------------- - --- This body is provided as a work-around for a GNAT compiler bug, as GNAT --- currently does not compile instantiations of the spec with imported ghost --- generics for packages Signed_Conversions and Unsigned_Conversions. - -package body Ada.Numerics.Big_Numbers.Big_Integers with - SPARK_Mode => Off -is - - package body Signed_Conversions with - SPARK_Mode => Off - is - - function To_Big_Integer (Arg : Int) return Valid_Big_Integer is - begin - raise Program_Error; - return (null record); - end To_Big_Integer; - - function From_Big_Integer (Arg : Valid_Big_Integer) return Int is - begin - raise Program_Error; - return 0; - end From_Big_Integer; - - end Signed_Conversions; - - package body Unsigned_Conversions with - SPARK_Mode => Off - is - - function To_Big_Integer (Arg : Int) return Valid_Big_Integer is - begin - raise Program_Error; - return (null record); - end To_Big_Integer; - - function From_Big_Integer (Arg : Valid_Big_Integer) return Int is - begin - raise Program_Error; - return 0; - end From_Big_Integer; - - end Unsigned_Conversions; - -end Ada.Numerics.Big_Numbers.Big_Integers; diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.ads b/gcc/ada/libgnat/a-nbnbin__ghost.ads deleted file mode 100644 index 3663dd7..0000000 --- a/gcc/ada/libgnat/a-nbnbin__ghost.ads +++ /dev/null @@ -1,202 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT RUN-TIME COMPONENTS -- --- -- --- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- --- -- --- S p e c -- --- -- --- This specification is derived from the Ada Reference Manual for use with -- --- GNAT. In accordance with the copyright of that document, you can freely -- --- copy and modify this specification, provided that if you redistribute a -- --- modified version, any changes that you have made are clearly indicated. -- --- -- ------------------------------------------------------------------------------- - -package Ada.Numerics.Big_Numbers.Big_Integers with - SPARK_Mode, - Ghost, - Preelaborate -is - type Big_Integer is private - with Integer_Literal => From_Universal_Image; - - function Is_Valid (Arg : Big_Integer) return Boolean - with - Import, - Global => null; - - subtype Valid_Big_Integer is Big_Integer - with Dynamic_Predicate => Is_Valid (Valid_Big_Integer), - Predicate_Failure => raise Program_Error; - - function "=" (L, R : Valid_Big_Integer) return Boolean with - Import, - Global => null; - - function "<" (L, R : Valid_Big_Integer) return Boolean with - Import, - Global => null; - - function "<=" (L, R : Valid_Big_Integer) return Boolean with - Import, - Global => null; - - function ">" (L, R : Valid_Big_Integer) return Boolean with - Import, - Global => null; - - function ">=" (L, R : Valid_Big_Integer) return Boolean with - Import, - Global => null; - - function To_Big_Integer (Arg : Integer) return Valid_Big_Integer - with - Import, - Global => null; - - subtype Big_Positive is Big_Integer - with Dynamic_Predicate => - (if Is_Valid (Big_Positive) - then Big_Positive > To_Big_Integer (0)), - Predicate_Failure => (raise Constraint_Error); - - subtype Big_Natural is Big_Integer - with Dynamic_Predicate => - (if Is_Valid (Big_Natural) - then Big_Natural >= To_Big_Integer (0)), - Predicate_Failure => (raise Constraint_Error); - - function In_Range - (Arg : Valid_Big_Integer; Low, High : Big_Integer) return Boolean - is (Low <= Arg and Arg <= High) - with - Import, - Global => null; - - function To_Integer (Arg : Valid_Big_Integer) return Integer - with - Import, - Pre => In_Range (Arg, - Low => To_Big_Integer (Integer'First), - High => To_Big_Integer (Integer'Last)) - or else (raise Constraint_Error), - Global => null; - - generic - type Int is range <>; - package Signed_Conversions is - - function To_Big_Integer (Arg : Int) return Valid_Big_Integer - with - Global => null; - - function From_Big_Integer (Arg : Valid_Big_Integer) return Int - with - Pre => In_Range (Arg, - Low => To_Big_Integer (Int'First), - High => To_Big_Integer (Int'Last)) - or else (raise Constraint_Error), - Global => null; - end Signed_Conversions; - - generic - type Int is mod <>; - package Unsigned_Conversions is - - function To_Big_Integer (Arg : Int) return Valid_Big_Integer - with - Global => null; - - function From_Big_Integer (Arg : Valid_Big_Integer) return Int - with - Pre => In_Range (Arg, - Low => To_Big_Integer (Int'First), - High => To_Big_Integer (Int'Last)) - or else (raise Constraint_Error), - Global => null; - - end Unsigned_Conversions; - - function From_String (Arg : String) return Valid_Big_Integer - with - Import, - Global => null; - - function From_Universal_Image (Arg : String) return Valid_Big_Integer - renames From_String; - - function "+" (L : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "-" (L : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer - with - Import, - Global => null; - - function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function Greatest_Common_Divisor - (L, R : Valid_Big_Integer) return Big_Positive - with - Import, - Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0)) - or else (raise Constraint_Error), - Global => null; - -private - pragma SPARK_Mode (Off); - - type Big_Integer is null record; - -end Ada.Numerics.Big_Numbers.Big_Integers; diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb index fce8c7a..79a0074 100644 --- a/gcc/ada/libgnat/s-widthu.adb +++ b/gcc/ada/libgnat/s-widthu.adb @@ -29,8 +29,8 @@ -- -- ------------------------------------------------------------------------------ -with Ada.Numerics.Big_Numbers.Big_Integers; -use Ada.Numerics.Big_Numbers.Big_Integers; +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; function System.Width_U (Lo, Hi : Uns) return Natural is diff --git a/gcc/ada/sem_aux.adb b/gcc/ada/sem_aux.adb index dcced7e..e1bcf53 100644 --- a/gcc/ada/sem_aux.adb +++ b/gcc/ada/sem_aux.adb @@ -336,10 +336,18 @@ package body Sem_Aux is function First_Subtype (Typ : Entity_Id) return Entity_Id is B : constant Entity_Id := Base_Type (Typ); - F : constant Node_Id := Freeze_Node (B); + F : Node_Id := Freeze_Node (B); Ent : Entity_Id; begin + -- The freeze node of a ghost type might have been rewritten in a null + -- statement by the time gigi calls First_Subtype on the corresponding + -- type. + + if Nkind (F) = N_Null_Statement then + F := Original_Node (F); + end if; + -- If the base type has no freeze node, it is a type in Standard, and -- always acts as its own first subtype, except where it is one of the -- predefined integer types. If the type is formal, it is also a first -- cgit v1.1