From fb69239a00b85f787c649b0454f0e93cc03132f8 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 12 Sep 2017 11:52:00 +0200 Subject: [PATCH] [multiple changes] 2017-09-12 Bob Duff * sem_ch6.adb (Analyze_Expression_Function): Initialize Def_Id to Empty. 2017-09-12 Georges-Axel Jaloyan * debug.adb: Reserving flag -gnatdF for safe pointer checking. * gnat1drv.adb (gnat1drv): Adding the call to the analysis on dF flag. * sem_spark.adb, sem_spark.ads: Implementation of the analysis, in preparation for the evolution of the SPARK language that includes a pointer analysis for checking non-aliasing of access types. The Check_Safe_Pointers function is the entry point, and will traverse the AST and raise compile-time errors everytime it detects non-begign aliasing. Detailed comments are present in the sem_spark.ads file. * sem_util.adb, sem_util.ads (First_Global, Next_Global): New functions to iterate over the list of globals of a subprogram. * libgnat/system.ads: Add restriction No_Finalization. * gcc-interface/Make-lang.in: Add new file sem_spark.adb and dependency on g-dynhta.adb. From-SVN: r252000 --- gcc/ada/ChangeLog | 23 + gcc/ada/debug.adb | 7 +- gcc/ada/gcc-interface/Make-lang.in | 2 + gcc/ada/gnat1drv.adb | 16 +- gcc/ada/libgnat/system.ads | 6 + gcc/ada/sem_ch6.adb | 2 +- gcc/ada/sem_spark.adb | 6188 ++++++++++++++++++++++++++++ gcc/ada/sem_spark.ads | 143 + gcc/ada/sem_util.adb | 139 + gcc/ada/sem_util.ads | 21 + 10 files changed, 6541 insertions(+), 6 deletions(-) create mode 100644 gcc/ada/sem_spark.adb create mode 100644 gcc/ada/sem_spark.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 4882093bf32..988f2ef55dc 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,26 @@ +2017-09-12 Bob Duff + + * sem_ch6.adb (Analyze_Expression_Function): Initialize Def_Id to + Empty. + +2017-09-12 Georges-Axel Jaloyan + + * debug.adb: Reserving flag -gnatdF for safe pointer checking. + * gnat1drv.adb (gnat1drv): Adding the call to the analysis on + dF flag. + * sem_spark.adb, sem_spark.ads: Implementation of the analysis, + in preparation for the evolution of the SPARK language that + includes a pointer analysis for checking non-aliasing of access + types. The Check_Safe_Pointers function is the entry point, and + will traverse the AST and raise compile-time errors everytime + it detects non-begign aliasing. Detailed comments are present + in the sem_spark.ads file. + * sem_util.adb, sem_util.ads (First_Global, Next_Global): New + functions to iterate over the list of globals of a subprogram. + * libgnat/system.ads: Add restriction No_Finalization. + * gcc-interface/Make-lang.in: Add new file sem_spark.adb and + dependency on g-dynhta.adb. + 2017-09-12 Bob Duff * sem_ch6.adb (Analyze_Expression_Function): Call diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index c45a1883ce2..77afd4b8c98 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -69,7 +69,7 @@ package body Debug is -- dC Output debugging information on check suppression -- dD Delete elaboration checks in inner level routines -- dE Apply elaboration checks to predefined units - -- dF + -- dF Perform the new SPARK checking rules for pointer aliasing -- dG Generate all warnings including those normally suppressed -- dH Hold (kill) call to gigi -- dI Inhibit internal name numbering in gnatG listing @@ -383,6 +383,11 @@ package body Debug is -- dE Apply compile time elaboration checking for with relations between -- predefined units. Normally no checks are made. + -- dF Perform the new SPARK checking rules for pointer aliasing. This is + -- only activated in GNATprove mode and on SPARK code. These rules are + -- not yet part of the official SPARK language, but are expected to be + -- included in a future version of SPARK. + -- dG Generate all warnings. Normally Errout suppresses warnings on -- units that are not part of the main extended source, and also -- suppresses warnings on instantiations in the main extended diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index 65826952d31..bbced4943aa 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -312,6 +312,7 @@ GNAT_ADA_OBJS = \ ada/freeze.o \ ada/frontend.o \ ada/libgnat/g-byorma.o \ + ada/libgnat/g-dynhta.o \ ada/libgnat/g-hesora.o \ ada/libgnat/g-htable.o \ ada/libgnat/g-spchge.o \ @@ -443,6 +444,7 @@ GNAT_ADA_OBJS = \ ada/sem_res.o \ ada/sem_scil.o \ ada/sem_smem.o \ + ada/sem_spark.o \ ada/sem_type.o \ ada/sem_util.o \ ada/sem_warn.o \ diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 3a0ceca3da5..197c6053d78 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -61,6 +61,7 @@ with Sem_Ch12; with Sem_Ch13; with Sem_Elim; with Sem_Eval; +with Sem_SPARK; use Sem_SPARK; with Sem_Type; with Set_Targ; with Sinfo; use Sinfo; @@ -1449,12 +1450,19 @@ begin Prepcomp.Add_Dependencies; - -- In gnatprove mode we're writing the ALI much earlier than usual - -- as flow analysis needs the file present in order to append its - -- own globals to it. - if GNATprove_Mode then + -- Perform the new SPARK checking rules for pointer aliasing. This is + -- only activated in GNATprove mode and on SPARK code. + + if Debug_Flag_FF then + Check_Safe_Pointers (Main_Unit_Node); + end if; + + -- In GNATprove mode we're writing the ALI much earlier than usual + -- as flow analysis needs the file present in order to append its + -- own globals to it. + -- Note: In GNATprove mode, an "object" file is always generated as -- the result of calling gnat1 or gnat2why, although this is not the -- same as the object file produced for compilation. diff --git a/gcc/ada/libgnat/system.ads b/gcc/ada/libgnat/system.ads index c35ee7cab27..c1a4a579ab7 100644 --- a/gcc/ada/libgnat/system.ads +++ b/gcc/ada/libgnat/system.ads @@ -44,6 +44,12 @@ pragma Restrictions (No_Implicit_Dynamic_Code); -- which prevent execution of code on the stack, e.g. in windows environments -- with DEP (Data Execution Protection) enabled. +pragma Restrictions (No_Finalization); +-- Use restriction No_Finalization to avoid pulling finalization (not allowed +-- in GNAT) inside sem_spark.adb, when defining type Perm_Tree_Access as an +-- access type on incomplete type Perm_Tree_Wrapper (which is required for +-- defining a recursive type). + package System is pragma Pure; -- Note that we take advantage of the implementation permission to make diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index b4232a5cfcd..ffcc357bfed 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -466,7 +466,7 @@ package body Sem_Ch6 is Orig_N : Node_Id; Ret : Node_Id; - Def_Id : Entity_Id; + Def_Id : Entity_Id := Empty; Prev : Entity_Id; -- If the expression is a completion, Prev is the entity whose -- declaration is completed. Def_Id is needed to analyze the spec. diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb new file mode 100644 index 00000000000..8c81d2e760f --- /dev/null +++ b/gcc/ada/sem_spark.adb @@ -0,0 +1,6188 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S E M _ S P A R K -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2017, 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. See the GNU General Public License -- +-- for more details. You should have received a copy of the GNU General -- +-- Public License distributed with GNAT; see file COPYING3. If not, go to -- +-- http://www.gnu.org/licenses for a complete copy of the license. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +with Atree; use Atree; +with Einfo; use Einfo; +with Errout; use Errout; +with Namet; use Namet; +with Nlists; use Nlists; +with Opt; use Opt; +with Osint; use Osint; +with Sem_Prag; use Sem_Prag; +with Sem_Util; use Sem_Util; +with Sem_Aux; use Sem_Aux; +with Sinfo; use Sinfo; +with Snames; use Snames; +with Treepr; use Treepr; + +with Ada.Unchecked_Deallocation; +with GNAT.Dynamic_HTables; use GNAT.Dynamic_HTables; + +package body Sem_SPARK is + + ------------------------------------------------- + -- Handling of Permissions Associated to Paths -- + ------------------------------------------------- + + package Permissions is + Elaboration_Context_Max : constant := 1009; + -- The hash range + + type Elaboration_Context_Index is range 0 .. Elaboration_Context_Max - 1; + + function Elaboration_Context_Hash + (Key : Entity_Id) return Elaboration_Context_Index; + -- Function to hash any node of the AST + + type Perm_Kind is (No_Access, Read_Only, Read_Write, Write_Only); + -- Permission type associated with paths + + subtype Read_Perm is Perm_Kind range Read_Only .. Read_Write; + subtype Write_Perm is Perm_Kind range Read_Write .. Write_Only; + + type Perm_Tree_Wrapper; + + type Perm_Tree_Access is access Perm_Tree_Wrapper; + -- A tree of permissions is defined, where the root is a whole object + -- and tree branches follow access paths in memory. As Perm_Tree is a + -- discriminated record, a wrapper type is used for the access type + -- designating a subtree, to make it unconstrained so that it can be + -- updated. + + -- Nodes in the permission tree are of different kinds + + type Path_Kind is + (Entire_Object, -- Scalar object, or folded object of any type + Reference, -- Unfolded object of access type + Array_Component, -- Unfolded object of array type + Record_Component -- Unfolded object of record type + ); + + package Perm_Tree_Maps is new Simple_HTable + (Header_Num => Elaboration_Context_Index, + Key => Node_Id, + Element => Perm_Tree_Access, + No_Element => null, + Hash => Elaboration_Context_Hash, + Equal => "="); + -- The instantation of a hash table, with keys being nodes and values + -- being pointers to trees. This is used to reference easily all + -- extensions of a Record_Component node (that can have name x, y, ...). + + -- The definition of permission trees. This is a tree, which has a + -- permission at each node, and depending on the type of the node, + -- can have zero, one, or more children pointed to by an access to tree. + type Perm_Tree (Kind : Path_Kind := Entire_Object) is record + Permission : Perm_Kind; + -- Permission at this level in the path + + Is_Node_Deep : Boolean; + -- Whether this node is of a deep type, to be used when moving the + -- path. + + case Kind is + + -- An entire object is either a leaf (an object which cannot be + -- extended further in a path) or a subtree in folded form (which + -- could later be unfolded further in another kind of node). The + -- field Children_Permission specifies a permission for every + -- extension of that node if that permission is different from + -- the node's permission. + + when Entire_Object => + Children_Permission : Perm_Kind; + + -- Unfolded path of access type. The permission of the object + -- pointed to is given in Get_All. + + when Reference => + Get_All : Perm_Tree_Access; + + -- Unfolded path of array type. The permission of the elements is + -- given in Get_Elem. + + when Array_Component => + Get_Elem : Perm_Tree_Access; + + -- Unfolded path of record type. The permission of the regular + -- components is given in Component. The permission of unknown + -- components (for objects of tagged type) is given in + -- Other_Components. + + when Record_Component => + Component : Perm_Tree_Maps.Instance; + Other_Components : Perm_Tree_Access; + end case; + end record; + + type Perm_Tree_Wrapper is record + Tree : Perm_Tree; + end record; + -- We use this wrapper in order to have unconstrained discriminants + + type Perm_Env is new Perm_Tree_Maps.Instance; + -- The definition of a permission environment for the analysis. This + -- is just a hash table of permission trees, each of them rooted with + -- an Identifier/Expanded_Name. + + type Perm_Env_Access is access Perm_Env; + -- Access to permission environments + + package Env_Maps is new Simple_HTable + (Header_Num => Elaboration_Context_Index, + Key => Entity_Id, + Element => Perm_Env_Access, + No_Element => null, + Hash => Elaboration_Context_Hash, + Equal => "="); + -- The instantiation of a hash table whose elements are permission + -- environments. This hash table is used to save the environments at + -- the entry of each loop, with the key being the loop label. + + type Env_Backups is new Env_Maps.Instance; + -- The type defining the hash table saving the environments at the entry + -- of each loop. + + package Boolean_Variables_Maps is new Simple_HTable + (Header_Num => Elaboration_Context_Index, + Key => Entity_Id, + Element => Boolean, + No_Element => False, + Hash => Elaboration_Context_Hash, + Equal => "="); + -- These maps allow tracking the variables that have been declared but + -- never used anywhere in the source code. Especially, we do not raise + -- an error if the variable stays write-only and is declared at package + -- level, because there is no risk that the variable has been moved, + -- because it has never been used. + + type Initialization_Map is new Boolean_Variables_Maps.Instance; + + -------------------- + -- Simple Getters -- + -------------------- + + -- Simple getters to avoid having .all.Tree.Field everywhere. Of course, + -- that's only for the top access, as otherwise this reverses the order + -- in accesses visually. + + function Children_Permission (T : Perm_Tree_Access) return Perm_Kind; + function Component (T : Perm_Tree_Access) return Perm_Tree_Maps.Instance; + function Get_All (T : Perm_Tree_Access) return Perm_Tree_Access; + function Get_Elem (T : Perm_Tree_Access) return Perm_Tree_Access; + function Is_Node_Deep (T : Perm_Tree_Access) return Boolean; + function Kind (T : Perm_Tree_Access) return Path_Kind; + function Other_Components (T : Perm_Tree_Access) return Perm_Tree_Access; + function Permission (T : Perm_Tree_Access) return Perm_Kind; + + ----------------------- + -- Memory Management -- + ----------------------- + + procedure Copy_Env + (From : Perm_Env; + To : in out Perm_Env); + -- Procedure to copy a permission environment + + procedure Copy_Init_Map + (From : Initialization_Map; + To : in out Initialization_Map); + -- Procedure to copy an initialization map + + procedure Copy_Tree + (From : Perm_Tree_Access; + To : Perm_Tree_Access); + -- Procedure to copy a permission tree + + procedure Free_Env + (PE : in out Perm_Env); + -- Procedure to free a permission environment + + procedure Free_Perm_Tree + (PT : in out Perm_Tree_Access); + -- Procedure to free a permission tree + + -------------------- + -- Error Messages -- + -------------------- + + procedure Perm_Mismatch + (Exp_Perm, Act_Perm : Perm_Kind; + N : Node_Id); + -- Issues a continuation error message about a mismatch between a + -- desired permission Exp_Perm and a permission obtained Act_Perm. N + -- is the node on which the error is reported. + + end Permissions; + + package body Permissions is + + ------------------------- + -- Children_Permission -- + ------------------------- + + function Children_Permission + (T : Perm_Tree_Access) + return Perm_Kind + is + begin + return T.all.Tree.Children_Permission; + end Children_Permission; + + --------------- + -- Component -- + --------------- + + function Component + (T : Perm_Tree_Access) + return Perm_Tree_Maps.Instance + is + begin + return T.all.Tree.Component; + end Component; + + -------------- + -- Copy_Env -- + -------------- + + procedure Copy_Env + (From : Perm_Env; + To : in out Perm_Env) + is + Comp_From : Perm_Tree_Access; + Key_From : Perm_Tree_Maps.Key_Option; + Son : Perm_Tree_Access; + + begin + Reset (To); + Key_From := Get_First_Key (From); + while Key_From.Present loop + Comp_From := Get (From, Key_From.K); + pragma Assert (Comp_From /= null); + + Son := new Perm_Tree_Wrapper; + Copy_Tree (Comp_From, Son); + + Set (To, Key_From.K, Son); + Key_From := Get_Next_Key (From); + end loop; + end Copy_Env; + + ------------------- + -- Copy_Init_Map -- + ------------------- + + procedure Copy_Init_Map + (From : Initialization_Map; + To : in out Initialization_Map) + is + Comp_From : Boolean; + Key_From : Boolean_Variables_Maps.Key_Option; + + begin + Reset (To); + Key_From := Get_First_Key (From); + while Key_From.Present loop + Comp_From := Get (From, Key_From.K); + Set (To, Key_From.K, Comp_From); + Key_From := Get_Next_Key (From); + end loop; + end Copy_Init_Map; + + --------------- + -- Copy_Tree -- + --------------- + + procedure Copy_Tree + (From : Perm_Tree_Access; + To : Perm_Tree_Access) + is + begin + To.all := From.all; + + case Kind (From) is + when Entire_Object => + null; + + when Reference => + To.all.Tree.Get_All := new Perm_Tree_Wrapper; + + Copy_Tree (Get_All (From), Get_All (To)); + + when Array_Component => + To.all.Tree.Get_Elem := new Perm_Tree_Wrapper; + + Copy_Tree (Get_Elem (From), Get_Elem (To)); + + when Record_Component => + declare + Comp_From : Perm_Tree_Access; + Key_From : Perm_Tree_Maps.Key_Option; + Son : Perm_Tree_Access; + Hash_Table : Perm_Tree_Maps.Instance; + begin + -- We put a new hash table, so that it gets dealiased from the + -- Component (From) hash table. + To.all.Tree.Component := Hash_Table; + + To.all.Tree.Other_Components := + new Perm_Tree_Wrapper'(Other_Components (From).all); + + Copy_Tree (Other_Components (From), Other_Components (To)); + + Key_From := Perm_Tree_Maps.Get_First_Key + (Component (From)); + while Key_From.Present loop + Comp_From := Perm_Tree_Maps.Get + (Component (From), Key_From.K); + + pragma Assert (Comp_From /= null); + Son := new Perm_Tree_Wrapper; + + Copy_Tree (Comp_From, Son); + + Perm_Tree_Maps.Set + (To.all.Tree.Component, Key_From.K, Son); + + Key_From := Perm_Tree_Maps.Get_Next_Key + (Component (From)); + end loop; + end; + end case; + end Copy_Tree; + + ------------------------------ + -- Elaboration_Context_Hash -- + ------------------------------ + + function Elaboration_Context_Hash + (Key : Entity_Id) return Elaboration_Context_Index + is + begin + return Elaboration_Context_Index (Key mod Elaboration_Context_Max); + end Elaboration_Context_Hash; + + -------------- + -- Free_Env -- + -------------- + + procedure Free_Env (PE : in out Perm_Env) is + CompO : Perm_Tree_Access; + begin + CompO := Get_First (PE); + while CompO /= null loop + Free_Perm_Tree (CompO); + CompO := Get_Next (PE); + end loop; + end Free_Env; + + -------------------- + -- Free_Perm_Tree -- + -------------------- + + procedure Free_Perm_Tree + (PT : in out Perm_Tree_Access) + is + procedure Free_Perm_Tree_Dealloc is + new Ada.Unchecked_Deallocation + (Perm_Tree_Wrapper, Perm_Tree_Access); + -- The deallocator for permission_trees + + begin + case Kind (PT) is + when Entire_Object => + Free_Perm_Tree_Dealloc (PT); + + when Reference => + Free_Perm_Tree (PT.all.Tree.Get_All); + Free_Perm_Tree_Dealloc (PT); + + when Array_Component => + Free_Perm_Tree (PT.all.Tree.Get_Elem); + + when Record_Component => + declare + Comp : Perm_Tree_Access; + + begin + Free_Perm_Tree (PT.all.Tree.Other_Components); + Comp := Perm_Tree_Maps.Get_First (Component (PT)); + while Comp /= null loop + -- Free every Component subtree + + Free_Perm_Tree (Comp); + Comp := Perm_Tree_Maps.Get_Next (Component (PT)); + end loop; + end; + Free_Perm_Tree_Dealloc (PT); + end case; + end Free_Perm_Tree; + + ------------- + -- Get_All -- + ------------- + + function Get_All + (T : Perm_Tree_Access) + return Perm_Tree_Access + is + begin + return T.all.Tree.Get_All; + end Get_All; + + -------------- + -- Get_Elem -- + -------------- + + function Get_Elem + (T : Perm_Tree_Access) + return Perm_Tree_Access + is + begin + return T.all.Tree.Get_Elem; + end Get_Elem; + + ------------------ + -- Is_Node_Deep -- + ------------------ + + function Is_Node_Deep + (T : Perm_Tree_Access) + return Boolean + is + begin + return T.all.Tree.Is_Node_Deep; + end Is_Node_Deep; + + ---------- + -- Kind -- + ---------- + + function Kind + (T : Perm_Tree_Access) + return Path_Kind + is + begin + return T.all.Tree.Kind; + end Kind; + + ---------------------- + -- Other_Components -- + ---------------------- + + function Other_Components + (T : Perm_Tree_Access) + return Perm_Tree_Access + is + begin + return T.all.Tree.Other_Components; + end Other_Components; + + ---------------- + -- Permission -- + ---------------- + + function Permission + (T : Perm_Tree_Access) + return Perm_Kind + is + begin + return T.all.Tree.Permission; + end Permission; + + ------------------- + -- Perm_Mismatch -- + ------------------- + + procedure Perm_Mismatch + (Exp_Perm, Act_Perm : Perm_Kind; + N : Node_Id) + is + begin + Error_Msg_N ("\expected at least `" + & Perm_Kind'Image (Exp_Perm) & "`, got `" + & Perm_Kind'Image (Act_Perm) & "`", N); + end Perm_Mismatch; + + end Permissions; + + use Permissions; + + -------------------------------------- + -- Analysis modes for AST traversal -- + -------------------------------------- + + -- The different modes for analysis. This allows to checking whether a path + -- found in the code should be moved, borrowed, or observed. + + type Checking_Mode is + + (Read, + -- Default mode. Checks that paths have Read_Perm permission. + + Move, + -- Regular moving semantics (not under 'Access). Checks that paths have + -- Read_Write permission. After moving a path, its permission is set to + -- Write_Only and the permission of its extensions is set to No_Access. + + Assign, + -- Used for the target of an assignment, or an actual parameter with + -- mode OUT. Checks that paths have Write_Perm permission. After + -- assigning to a path, its permission is set to Read_Write. + + Super_Move, + -- Enhanced moving semantics (under 'Access). Checks that paths have + -- Read_Write permission. After moving a path, its permission is set + -- to No_Access, as well as the permission of its extensions and the + -- permission of its prefixes up to the first Reference node. + + Borrow_Out, + -- Used for actual OUT parameters. Checks that paths have Write_Perm + -- permission. After checking a path, its permission is set to Read_Only + -- when of a by-copy type, to No_Access otherwise. After the call, its + -- permission is set to Read_Write. + + Observe + -- Used for actual IN parameters of a scalar type. Checks that paths + -- have Read_Perm permission. After checking a path, its permission + -- is set to Read_Only. + -- + -- Also used for formal IN parameters + ); + + type Result_Kind is (Folded, Unfolded, Function_Call); + -- The type declaration to discriminate in the Perm_Or_Tree type + + -- The result type of the function Get_Perm_Or_Tree. This returns either a + -- tree when it found the appropriate tree, or a permission when the search + -- finds a leaf and the subtree we are looking for is folded. In the last + -- case, we return instead the Children_Permission field of the leaf. + + type Perm_Or_Tree (R : Result_Kind) is record + case R is + when Folded => Found_Permission : Perm_Kind; + when Unfolded => Tree_Access : Perm_Tree_Access; + when Function_Call => null; + end case; + end record; + + ----------------------- + -- Local subprograms -- + ----------------------- + + function "<=" (P1, P2 : Perm_Kind) return Boolean; + function ">=" (P1, P2 : Perm_Kind) return Boolean; + function Glb (P1, P2 : Perm_Kind) return Perm_Kind; + function Lub (P1, P2 : Perm_Kind) return Perm_Kind; + + -- Checking proceduress for safe pointer usage. These procedures traverse + -- the AST, check nodes for correct permissions according to SPARK RM + -- 6.4.2, and update permissions depending on the node kind. + + procedure Check_Call_Statement (Call : Node_Id); + + procedure Check_Callable_Body (Body_N : Node_Id); + -- We are not in End_Of_Callee mode, hence we will save the environment + -- and start from a new one. We will add in the environment all formal + -- parameters as well as global used during the subprogram, with the + -- appropriate permissions (write-only for out, read-only for observed, + -- read-write for others). + -- + -- After that we analyze the body of the function, and finaly, we check + -- that each borrowed parameter and global has read-write permission. We + -- then clean up the environment and put back the saved environment. + + procedure Check_Declaration (Decl : Node_Id); + + procedure Check_Expression (Expr : Node_Id); + + procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode); + -- This procedure takes a global pragma and checks depending on mode: + -- Mode Read: every in global is readable + -- Mode Observe: same as Check_Param_Observes but on globals + -- Mode Borrow_Out: Check_Param_Outs for globals + -- Mode Move: Check_Param for globals with mode Read + -- Mode Assign: Check_Param for globals with mode Assign + + procedure Check_List (L : List_Id); + -- Calls Check_Node on each element of the list + + procedure Check_Loop_Statement (Loop_N : Node_Id); + + procedure Check_Node (N : Node_Id); + -- Main traversal procedure to check safe pointer usage. This procedure is + -- mutually recursive with the specialized procedures that follow. + + procedure Check_Package_Body (Pack : Node_Id); + + procedure Check_Param (Formal : Entity_Id; Actual : Node_Id); + -- This procedure takes a formal and an actual parameter and calls the + -- analyze node if the parameter is borrowed with mode in out, with the + -- appropriate Checking_Mode (Move). + + procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id); + -- This procedure takes a formal and an actual parameter and calls + -- the analyze node if the parameter is observed, with the appropriate + -- Checking_Mode. + + procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id); + -- This procedure takes a formal and an actual parameter and calls the + -- analyze node if the parameter is of mode out, with the appropriate + -- Checking_Mode. + + procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id); + -- This procedure takes a formal and an actual parameter and checks the + -- readability of every in-mode parameter. This includes observed in, and + -- also borrowed in, that are then checked afterwards. + + procedure Check_Statement (Stmt : Node_Id); + + function Get_Perm (N : Node_Id) return Perm_Kind; + -- The function that takes a name as input and returns a permission + -- associated to it. + + function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree; + -- This function gets a Node_Id and looks recursively to find the + -- appropriate subtree for that Node_Id. If the tree is folded on + -- that node, then it returns the permission given at the right level. + + function Get_Perm_Tree (N : Node_Id) return Perm_Tree_Access; + -- This function gets a Node_Id and looks recursively to find the + -- appropriate subtree for that Node_Id. If the tree is folded, then + -- it unrolls the tree up to the appropriate level. + + function Has_Alias + (N : Node_Id) + return Boolean; + -- Function that returns whether the path given as parameter contains an + -- extension that is declared as aliased. + + function Has_Array_Component (N : Node_Id) return Boolean; + -- This function gets a Node_Id and looks recursively to find if the given + -- path has any array component. + + function Has_Function_Component (N : Node_Id) return Boolean; + -- This function gets a Node_Id and looks recursively to find if the given + -- path has any function component. + + procedure Hp (P : Perm_Env); + -- A procedure that outputs the hash table. This function is used only in + -- the debugger to look into a hash table. + pragma Unreferenced (Hp); + + procedure Illegal_Global_Usage (N : Node_Or_Entity_Id); + pragma No_Return (Illegal_Global_Usage); + -- A procedure that is called when deep globals or aliased globals are used + -- without any global aspect. + + function Is_Borrowed_In (E : Entity_Id) return Boolean; + -- Function that tells if the given entity is a borrowed in a formal + -- parameter, that is, if it is an access-to-variable type. + + function Is_Deep (E : Entity_Id) return Boolean; + -- A function that can tell if a type is deep or not. Returns true if the + -- type passed as argument is deep. + + function Is_Shallow (E : Entity_Id) return Boolean; + -- A function that can tell if a type is shallow or not. Returns true if + -- the type passed as argument is shallow. + + function Loop_Of_Exit (N : Node_Id) return Entity_Id; + -- A function that takes an exit statement node and returns the entity of + -- the loop that this statement is exiting from. + + procedure Merge_Envs (Target : in out Perm_Env; Source : in out Perm_Env); + -- Merge Target and Source into Target, and then deallocate the Source + + procedure Perm_Error + (N : Node_Id; + Perm : Perm_Kind; + Found_Perm : Perm_Kind); + -- A procedure that is called when the permissions found contradict the + -- rules established by the RM. This function is called with the node, its + -- entity and the permission that was expected, and adds an error message + -- with the appropriate values. + + procedure Perm_Error_Subprogram_End + (E : Entity_Id; + Subp : Entity_Id; + Perm : Perm_Kind; + Found_Perm : Perm_Kind); + -- A procedure that is called when the permissions found contradict the + -- rules established by the RM at the end of subprograms. This function + -- is called with the node, its entity, the node of the returning function + -- and the permission that was expected, and adds an error message with the + -- appropriate values. + + procedure Process_Path (N : Node_Id); + + procedure Return_Declarations (L : List_Id); + -- Check correct permissions on every declared object at the end of a + -- callee. Used at the end of the body of a callable entity. Checks that + -- paths of all borrowed formal parameters and global have Read_Write + -- permission. + + procedure Return_Globals (Subp : Entity_Id); + -- Takes a subprogram as input, and checks that all borrowed global items + -- of the subprogram indeed have RW permission at the end of the subprogram + -- execution. + + procedure Return_Parameter_Or_Global + (Id : Entity_Id; + Mode : Formal_Kind; + Subp : Entity_Id); + -- Auxiliary procedure to Return_Parameters and Return_Globals + + procedure Return_Parameters (Subp : Entity_Id); + -- Takes a subprogram as input, and checks that all borrowed parameters of + -- the subprogram indeed have RW permission at the end of the subprogram + -- execution. + + procedure Set_Perm_Extensions (T : Perm_Tree_Access; P : Perm_Kind); + -- This procedure takes an access to a permission tree and modifies the + -- tree so that any strict extensions of the given tree become of the + -- access specified by parameter P. + + procedure Set_Perm_Extensions_Move (T : Perm_Tree_Access; E : Entity_Id); + -- Set permissions to + -- No for any extension with more .all + -- W for any deep extension with same number of .all + -- RW for any shallow extension with same number of .all + + function Set_Perm_Prefixes_Assign (N : Node_Id) return Perm_Tree_Access; + -- This function takes a name as an input and sets in the permission + -- tree the given permission to the given name. The general rule here is + -- that everybody updates the permission of the subtree it is returning. + -- The permission of the assigned path has been set to RW by the caller. + -- + -- Case where we have to normalize a tree after the correct permissions + -- have been assigned already. We look for the right subtree at the given + -- path, actualize its permissions, and then call the normalization on its + -- parent. + -- + -- Example: We assign x.y and x.z then during Set_Perm_Prefixes_Move will + -- change the permission of x to RW because all of its components have + -- permission have permission RW. + + function Set_Perm_Prefixes_Borrow_Out (N : Node_Id) return Perm_Tree_Access; + -- This function modifies the permissions of a given node_id in the + -- permission environment as well as in all the prefixes of the path, + -- given that the path is borrowed with mode out. + + function Set_Perm_Prefixes_Move + (N : Node_Id; Mode : Checking_Mode) + return Perm_Tree_Access; + pragma Precondition (Mode = Move or Mode = Super_Move); + -- Given a node and a mode (that can be either Move or Super_Move), this + -- function modifies the permissions of a given node_id in the permission + -- environment as well as all the prefixes of the path, given that the path + -- is moved with or without 'Access. The general rule here is everybody + -- updates the permission of the subtree they are returning. + -- + -- This case describes a move either under 'Access or without 'Access. + + function Set_Perm_Prefixes_Observe (N : Node_Id) return Perm_Tree_Access; + -- This function modifies the permissions of a given node_id in the + -- permission environment as well as all the prefixes of the path, + -- given that the path is observed. + + procedure Setup_Globals (Subp : Entity_Id); + -- Takes a subprogram as input, and sets up the environment by adding + -- global items with appropriate permissions. + + procedure Setup_Parameter_Or_Global + (Id : Entity_Id; + Mode : Formal_Kind); + -- Auxiliary procedure to Setup_Parameters and Setup_Globals + + procedure Setup_Parameters (Subp : Entity_Id); + -- Takes a subprogram as input, and sets up the environment by adding + -- formal parameters with appropriate permissions. + + ---------------------- + -- Global Variables -- + ---------------------- + + Current_Perm_Env : Perm_Env; + -- The permission environment that is used for the analysis. This + -- environment can be saved, modified, reinitialized, but should be the + -- only one valid from which to extract the permissions of the paths in + -- scope. The analysis ensures at each point that this variables contains + -- a valid permission environment with all bindings in scope. + + Current_Checking_Mode : Checking_Mode := Read; + -- The current analysis mode. This global variable indicates at each point + -- of the analysis whether the node being analyzed is moved, borrowed, + -- assigned, read, ... The full list of possible values can be found in + -- the declaration of type Checking_Mode. + + Current_Loops_Envs : Env_Backups; + -- This variable contains saves of permission environments at each loop the + -- analysis entered. Each saved environment can be reached with the label + -- of the loop. + + Current_Loops_Accumulators : Env_Backups; + -- This variable contains the environments used as accumulators for loops, + -- that consist of the merge of all environments at each exit point of + -- the loop (which can also be the entry point of the loop in the case of + -- non-infinite loops), each of them reachable from the label of the loop. + -- We require that the environment stored in the accumulator be less + -- restrictive than the saved environment at the beginning of the loop, and + -- the permission environment after the loop is equal to the accumulator. + + Current_Initialization_Map : Initialization_Map; + -- This variable contains a map that binds each variable of the analyzed + -- source code to a boolean that becomes true whenever the variable is used + -- after declaration. Hence we can exclude from analysis variables that + -- are just declared and never accessed, typically at package declaration. + + ---------- + -- "<=" -- + ---------- + + function "<=" (P1, P2 : Perm_Kind) return Boolean + is + begin + return P2 >= P1; + end "<="; + + ---------- + -- ">=" -- + ---------- + + function ">=" (P1, P2 : Perm_Kind) return Boolean + is + begin + case P2 is + when No_Access => return True; + when Read_Only => return P1 in Read_Perm; + when Write_Only => return P1 in Write_Perm; + when Read_Write => return P1 = Read_Write; + end case; + end ">="; + + -------------------------- + -- Check_Call_Statement -- + -------------------------- + + procedure Check_Call_Statement (Call : Node_Id) is + Saved_Env : Perm_Env; + + procedure Iterate_Call is new + Iterate_Call_Parameters (Check_Param); + procedure Iterate_Call_Observes is new + Iterate_Call_Parameters (Check_Param_Observes); + procedure Iterate_Call_Outs is new + Iterate_Call_Parameters (Check_Param_Outs); + procedure Iterate_Call_Read is new + Iterate_Call_Parameters (Check_Param_Read); + + begin + -- Save environment, so that the modifications done by analyzing the + -- parameters are not kept at the end of the call. + Copy_Env (Current_Perm_Env, + Saved_Env); + + -- We first check the Read access on every in parameter + + Current_Checking_Mode := Read; + Iterate_Call_Read (Call); + Check_Globals (Get_Pragma + (Get_Called_Entity (Call), Pragma_Global), Read); + + -- We first observe, then borrow with mode out, and then with other + -- modes. This ensures that we do not have to check for by-copy types + -- specially, because we read them before borrowing them. + + Iterate_Call_Observes (Call); + Check_Globals (Get_Pragma + (Get_Called_Entity (Call), Pragma_Global), + Observe); + + Iterate_Call_Outs (Call); + Check_Globals (Get_Pragma + (Get_Called_Entity (Call), Pragma_Global), + Borrow_Out); + + Iterate_Call (Call); + Check_Globals (Get_Pragma + (Get_Called_Entity (Call), Pragma_Global), Move); + + -- Restore environment, because after borrowing/observing actual + -- parameters, they get their permission reverted to the ones before + -- the call. + + Free_Env (Current_Perm_Env); + + Copy_Env (Saved_Env, + Current_Perm_Env); + + Free_Env (Saved_Env); + + -- We assign the out parameters (necessarily borrowed per RM) + Current_Checking_Mode := Assign; + Iterate_Call (Call); + Check_Globals (Get_Pragma + (Get_Called_Entity (Call), Pragma_Global), + Assign); + + end Check_Call_Statement; + + ------------------------- + -- Check_Callable_Body -- + ------------------------- + + procedure Check_Callable_Body (Body_N : Node_Id) is + + Mode_Before : constant Checking_Mode := Current_Checking_Mode; + + Saved_Env : Perm_Env; + Saved_Init_Map : Initialization_Map; + + New_Env : Perm_Env; + + Body_Id : constant Entity_Id := Defining_Entity (Body_N); + Spec_Id : constant Entity_Id := Unique_Entity (Body_Id); + + begin + -- Check if SPARK pragma is not set to Off + + if Present (SPARK_Pragma (Defining_Entity (Body_N))) then + if Get_SPARK_Mode_From_Annotation + (SPARK_Pragma (Defining_Entity (Body_N, False))) /= Opt.On + then + return; + end if; + else + return; + end if; + + -- Save environment and put a new one in place + + Copy_Env (Current_Perm_Env, Saved_Env); + + -- Save initialization map + + Copy_Init_Map (Current_Initialization_Map, Saved_Init_Map); + + Current_Checking_Mode := Read; + Current_Perm_Env := New_Env; + + -- Add formals and globals to the environment with adequate permissions + + if Is_Subprogram_Or_Entry (Spec_Id) then + Setup_Parameters (Spec_Id); + Setup_Globals (Spec_Id); + end if; + + -- Analyze the body of the function + + Check_List (Declarations (Body_N)); + Check_Node (Handled_Statement_Sequence (Body_N)); + + -- Check the read-write permissions of borrowed parameters/globals + + if Ekind_In (Spec_Id, E_Procedure, E_Entry) + and then not No_Return (Spec_Id) + then + Return_Parameters (Spec_Id); + Return_Globals (Spec_Id); + end if; + + -- Free the environments + + Free_Env (Current_Perm_Env); + + Copy_Env (Saved_Env, + Current_Perm_Env); + + Free_Env (Saved_Env); + + -- Restore initialization map + + Copy_Init_Map (Saved_Init_Map, Current_Initialization_Map); + + Reset (Saved_Init_Map); + + -- The assignment of all out parameters will be done by caller + + Current_Checking_Mode := Mode_Before; + end Check_Callable_Body; + + ----------------------- + -- Check_Declaration -- + ----------------------- + + procedure Check_Declaration (Decl : Node_Id) is + begin + case N_Declaration'(Nkind (Decl)) is + when N_Full_Type_Declaration => + -- Nothing to do here ??? NOT TRUE IF CONSTRAINT ON TYPE + null; + + when N_Object_Declaration => + -- First move the right-hand side + Current_Checking_Mode := Move; + Check_Node (Expression (Decl)); + + declare + Elem : Perm_Tree_Access; + + begin + Elem := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => + Is_Deep (Etype (Defining_Identifier (Decl))), + Permission => Read_Write, + Children_Permission => Read_Write)); + + -- If unitialized declaration, then set to Write_Only. If a + -- pointer declaration, it has a null default initialization. + if Nkind (Expression (Decl)) = N_Empty + and then not Has_Full_Default_Initialization + (Etype (Defining_Identifier (Decl))) + and then not Is_Access_Type + (Etype (Defining_Identifier (Decl))) + then + Elem.all.Tree.Permission := Write_Only; + Elem.all.Tree.Children_Permission := Write_Only; + end if; + + -- Create new tree for defining identifier + + Set (Current_Perm_Env, + Unique_Entity (Defining_Identifier (Decl)), + Elem); + + pragma Assert (Get_First (Current_Perm_Env) + /= null); + + end; + + when N_Subtype_Declaration => + Check_Node (Subtype_Indication (Decl)); + + when N_Iterator_Specification => + pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl)))); + null; + + when N_Loop_Parameter_Specification => + pragma Assert (Is_Shallow (Etype (Defining_Identifier (Decl)))); + null; + + -- Checking should not be called directly on these nodes + + when N_Component_Declaration + | N_Function_Specification + | N_Entry_Declaration + | N_Procedure_Specification + => + raise Program_Error; + + -- Ignored constructs for pointer checking + + when N_Formal_Object_Declaration + | N_Formal_Type_Declaration + | N_Incomplete_Type_Declaration + | N_Private_Extension_Declaration + | N_Private_Type_Declaration + | N_Protected_Type_Declaration + => + null; + + -- The following nodes are rewritten by semantic analysis + + when N_Expression_Function => + raise Program_Error; + end case; + end Check_Declaration; + + ---------------------- + -- Check_Expression -- + ---------------------- + + procedure Check_Expression (Expr : Node_Id) is + Mode_Before : constant Checking_Mode := Current_Checking_Mode; + begin + case N_Subexpr'(Nkind (Expr)) is + when N_Procedure_Call_Statement => + Check_Call_Statement (Expr); + + when N_Identifier + | N_Expanded_Name + => + -- Check if identifier is pointing to nothing (On/Off/...) + if not Present (Entity (Expr)) then + return; + end if; + + -- Do not analyze things that are not of object Kind + if Ekind (Entity (Expr)) not in Object_Kind then + return; + end if; + + -- Consider as ident + Process_Path (Expr); + + -- Switch to read mode and then check the readability of each operand + + when N_Binary_Op => + + Current_Checking_Mode := Read; + Check_Node (Left_Opnd (Expr)); + Check_Node (Right_Opnd (Expr)); + + -- Switch to read mode and then check the readability of each operand + + when N_Op_Abs + | N_Op_Minus + | N_Op_Not + | N_Op_Plus + => + pragma Assert (Is_Shallow (Etype (Expr))); + Current_Checking_Mode := Read; + Check_Node (Right_Opnd (Expr)); + + -- Forbid all deep expressions for Attribute ??? + + when N_Attribute_Reference => + case Attribute_Name (Expr) is + when Name_Access => + case Current_Checking_Mode is + when Read => + Check_Node (Prefix (Expr)); + + when Move => + Current_Checking_Mode := Super_Move; + Check_Node (Prefix (Expr)); + + -- Only assign names, not expressions + + when Assign => + raise Program_Error; + + -- Prefix in Super_Move should be a name, error here + + when Super_Move => + raise Program_Error; + + -- Could only borrow names of mode out, not n'Access + + when Borrow_Out => + raise Program_Error; + + when Observe => + Check_Node (Prefix (Expr)); + end case; + + when Name_Last + | Name_First + => + Current_Checking_Mode := Read; + Check_Node (Prefix (Expr)); + + when Name_Min => + Current_Checking_Mode := Read; + Check_Node (Prefix (Expr)); + + when Name_Image => + Check_Node (Prefix (Expr)); + + when Name_SPARK_Mode => + null; + + when Name_Value => + Current_Checking_Mode := Read; + Check_Node (Prefix (Expr)); + + when Name_Update => + Check_List (Expressions (Expr)); + Check_Node (Prefix (Expr)); + + when Name_Pred + | Name_Succ + => + Check_List (Expressions (Expr)); + Check_Node (Prefix (Expr)); + + when Name_Length => + Current_Checking_Mode := Read; + Check_Node (Prefix (Expr)); + + -- Any Attribute referring to the underlying memory is ignored + -- in the analysis. This means that taking the address of a + -- variable makes a silent alias that is not rejected by the + -- analysis. + + when Name_Address + | Name_Alignment + | Name_Component_Size + | Name_First_Bit + | Name_Last_Bit + | Name_Size + | Name_Position + => + null; + + -- Attributes referring to types (get values from types), hence + -- no need to check either for borrows or any loans. + + when Name_Base + | Name_Val + => + null; + + -- Other attributes that fall out of the scope of the analysis + + when others => + null; + end case; + + when N_In => + Current_Checking_Mode := Read; + Check_Node (Left_Opnd (Expr)); + Check_Node (Right_Opnd (Expr)); + + when N_Not_In => + Current_Checking_Mode := Read; + Check_Node (Left_Opnd (Expr)); + Check_Node (Right_Opnd (Expr)); + + -- Switch to read mode and then check the readability of each operand + + when N_And_Then + | N_Or_Else + => + pragma Assert (Is_Shallow (Etype (Expr))); + Current_Checking_Mode := Read; + Check_Node (Left_Opnd (Expr)); + Check_Node (Right_Opnd (Expr)); + + -- Check the arguments of the call + + when N_Function_Call => + Current_Checking_Mode := Read; + Check_List (Parameter_Associations (Expr)); + + when N_Explicit_Dereference => + Process_Path (Expr); + + -- Copy environment, run on each branch, and then merge + + when N_If_Expression => + declare + Saved_Env : Perm_Env; + + -- Accumulator for the different branches + + New_Env : Perm_Env; + + Elmt : Node_Id := First (Expressions (Expr)); + + begin + Current_Checking_Mode := Read; + + Check_Node (Elmt); + + Current_Checking_Mode := Mode_Before; + + -- Save environment + + Copy_Env (Current_Perm_Env, + Saved_Env); + + -- Here we have the original env in saved, current with a fresh + -- copy, and new aliased. + + -- THEN PART + + Next (Elmt); + Check_Node (Elmt); + + -- Here the new_environment contains curr env after then block + + -- ELSE part + + -- Restore environment before if + Copy_Env (Current_Perm_Env, + New_Env); + + Free_Env (Current_Perm_Env); + + Copy_Env (Saved_Env, + Current_Perm_Env); + + -- Here new environment contains the environment after then and + -- current the fresh copy of old one. + + Next (Elmt); + Check_Node (Elmt); + + Merge_Envs (New_Env, + Current_Perm_Env); + + -- CLEANUP + + Copy_Env (New_Env, + Current_Perm_Env); + + Free_Env (New_Env); + Free_Env (Saved_Env); + end; + + when N_Indexed_Component => + Process_Path (Expr); + + -- Analyze the expression that is getting qualified + + when N_Qualified_Expression => + Check_Node (Expression (Expr)); + + when N_Quantified_Expression => + declare + Saved_Env : Perm_Env; + begin + Copy_Env (Current_Perm_Env, Saved_Env); + Current_Checking_Mode := Read; + Check_Node (Iterator_Specification (Expr)); + Check_Node (Loop_Parameter_Specification (Expr)); + + Check_Node (Condition (Expr)); + Free_Env (Current_Perm_Env); + Copy_Env (Saved_Env, Current_Perm_Env); + Free_Env (Saved_Env); + end; + + -- Analyze the list of associations in the aggregate + + when N_Aggregate => + Check_List (Expressions (Expr)); + Check_List (Component_Associations (Expr)); + + when N_Allocator => + Check_Node (Expression (Expr)); + + when N_Case_Expression => + declare + Saved_Env : Perm_Env; + + -- Accumulator for the different branches + + New_Env : Perm_Env; + + Elmt : Node_Id := First (Alternatives (Expr)); + + begin + Current_Checking_Mode := Read; + Check_Node (Expression (Expr)); + + Current_Checking_Mode := Mode_Before; + + -- Save environment + + Copy_Env (Current_Perm_Env, + Saved_Env); + + -- Here we have the original env in saved, current with a fresh + -- copy, and new aliased. + + -- First alternative + + Check_Node (Elmt); + Next (Elmt); + + Copy_Env (Current_Perm_Env, + New_Env); + + Free_Env (Current_Perm_Env); + + -- Other alternatives + + while Present (Elmt) loop + -- Restore environment + + Copy_Env (Saved_Env, + Current_Perm_Env); + + Check_Node (Elmt); + + -- Merge Current_Perm_Env into New_Env + + Merge_Envs (New_Env, + Current_Perm_Env); + + Next (Elmt); + end loop; + + -- CLEANUP + Copy_Env (New_Env, + Current_Perm_Env); + + Free_Env (New_Env); + Free_Env (Saved_Env); + end; + + -- Analyze the list of associates in the aggregate as well as the + -- ancestor part. + + when N_Extension_Aggregate => + + Check_Node (Ancestor_Part (Expr)); + Check_List (Expressions (Expr)); + + when N_Range => + Check_Node (Low_Bound (Expr)); + Check_Node (High_Bound (Expr)); + + -- We arrived at a path. Process it. + + when N_Selected_Component => + Process_Path (Expr); + + when N_Slice => + Process_Path (Expr); + + when N_Type_Conversion => + Check_Node (Expression (Expr)); + + when N_Unchecked_Type_Conversion => + Check_Node (Expression (Expr)); + + -- Checking should not be called directly on these nodes + + when N_Target_Name => + raise Program_Error; + + -- Unsupported constructs in SPARK + + when N_Delta_Aggregate => + Error_Msg_N ("unsupported construct in SPARK", Expr); + + -- Ignored constructs for pointer checking + + when N_Character_Literal + | N_Null + | N_Numeric_Or_String_Literal + | N_Operator_Symbol + | N_Raise_Expression + | N_Raise_xxx_Error + => + null; + + -- The following nodes are never generated in GNATprove mode + + when N_Expression_With_Actions + | N_Reference + | N_Unchecked_Expression + => + raise Program_Error; + + end case; + end Check_Expression; + + ------------------- + -- Check_Globals -- + ------------------- + + procedure Check_Globals (N : Node_Id; Check_Mode : Checking_Mode) is + begin + if Nkind (N) = N_Empty then + return; + end if; + + declare + pragma Assert + (List_Length (Pragma_Argument_Associations (N)) = 1); + + PAA : constant Node_Id := + First (Pragma_Argument_Associations (N)); + pragma Assert (Nkind (PAA) = N_Pragma_Argument_Association); + + Row : Node_Id; + The_Mode : Name_Id; + RHS : Node_Id; + + procedure Process (Mode : Name_Id; + The_Global : Entity_Id); + + procedure Process (Mode : Name_Id; + The_Global : Node_Id) + is + Ident_Elt : constant Entity_Id := + Unique_Entity (Entity (The_Global)); + + Mode_Before : constant Checking_Mode := Current_Checking_Mode; + + begin + if Ekind (Ident_Elt) = E_Abstract_State then + return; + end if; + + case Check_Mode is + when Read => + case Mode is + when Name_Input + | Name_Proof_In + => + Check_Node (The_Global); + + when Name_Output + | Name_In_Out + => + null; + + when others => + raise Program_Error; + + end case; + + when Observe => + case Mode is + when Name_Input + | Name_Proof_In + => + if not Is_Borrowed_In (Ident_Elt) then + -- Observed in + + Current_Checking_Mode := Observe; + Check_Node (The_Global); + end if; + + when others => + null; + + end case; + + when Borrow_Out => + + case Mode is + when Name_Output => + -- Borrowed out + Current_Checking_Mode := Borrow_Out; + Check_Node (The_Global); + + when others => + null; + + end case; + + when Move => + case Mode is + when Name_Input + | Name_Proof_In + => + if Is_Borrowed_In (Ident_Elt) then + -- Borrowed in + + Current_Checking_Mode := Move; + else + -- Observed + + return; + end if; + + when Name_Output => + return; + + when Name_In_Out => + -- Borrowed in out + + Current_Checking_Mode := Move; + + when others => + raise Program_Error; + end case; + + Check_Node (The_Global); + when Assign => + case Mode is + when Name_Input + | Name_Proof_In + => + null; + + when Name_Output + | Name_In_Out + => + -- Borrowed out or in out + + Process_Path (The_Global); + + when others => + raise Program_Error; + end case; + + when others => + raise Program_Error; + end case; + + Current_Checking_Mode := Mode_Before; + end Process; + + begin + if Nkind (Expression (PAA)) = N_Null then + -- global => null + -- No globals, nothing to do + return; + + elsif Nkind_In (Expression (PAA), N_Identifier, N_Expanded_Name) then + -- global => foo + -- A single input + Process (Name_Input, Expression (PAA)); + + elsif Nkind (Expression (PAA)) = N_Aggregate + and then Expressions (Expression (PAA)) /= No_List + then + -- global => (foo, bar) + -- Inputs + RHS := First (Expressions (Expression (PAA))); + while Present (RHS) loop + case Nkind (RHS) is + when N_Identifier + | N_Expanded_Name + => + Process (Name_Input, RHS); + + when N_Numeric_Or_String_Literal => + Process (Name_Input, Original_Node (RHS)); + + when others => + raise Program_Error; + + end case; + RHS := Next (RHS); + end loop; + + elsif Nkind (Expression (PAA)) = N_Aggregate + and then Component_Associations (Expression (PAA)) /= No_List + then + -- global => (mode => foo, + -- mode => (bar, baz)) + -- A mixture of things + + declare + CA : constant List_Id := + Component_Associations (Expression (PAA)); + begin + Row := First (CA); + while Present (Row) loop + pragma Assert (List_Length (Choices (Row)) = 1); + The_Mode := Chars (First (Choices (Row))); + + RHS := Expression (Row); + case Nkind (RHS) is + when N_Aggregate => + RHS := First (Expressions (RHS)); + while Present (RHS) loop + case Nkind (RHS) is + when N_Numeric_Or_String_Literal => + Process (The_Mode, Original_Node (RHS)); + + when others => + Process (The_Mode, RHS); + + end case; + RHS := Next (RHS); + end loop; + + when N_Identifier + | N_Expanded_Name + => + Process (The_Mode, RHS); + + when N_Null => + null; + + when N_Numeric_Or_String_Literal => + Process (The_Mode, Original_Node (RHS)); + + when others => + raise Program_Error; + + end case; + + Row := Next (Row); + end loop; + end; + + else + raise Program_Error; + end if; + end; + end Check_Globals; + + ---------------- + -- Check_List -- + ---------------- + + procedure Check_List (L : List_Id) is + N : Node_Id; + begin + N := First (L); + while Present (N) loop + Check_Node (N); + Next (N); + end loop; + end Check_List; + + -------------------------- + -- Check_Loop_Statement -- + -------------------------- + + procedure Check_Loop_Statement (Loop_N : Node_Id) is + + -- Local Subprograms + + procedure Check_Is_Less_Restrictive_Env + (Exiting_Env : Perm_Env; + Entry_Env : Perm_Env); + -- This procedure checks that the Exiting_Env environment is less + -- restrictive than the Entry_Env environment. + + procedure Check_Is_Less_Restrictive_Tree + (New_Tree : Perm_Tree_Access; + Orig_Tree : Perm_Tree_Access; + E : Entity_Id); + -- Auxiliary procedure to check that the tree New_Tree is less + -- restrictive than the tree Orig_Tree for the entity E. + + procedure Perm_Error_Loop_Exit + (E : Entity_Id; + Loop_Id : Node_Id; + Perm : Perm_Kind; + Found_Perm : Perm_Kind); + -- A procedure that is called when the permissions found contradict + -- the rules established by the RM at the exit of loops. This function + -- is called with the entity, the node of the enclosing loop, the + -- permission that was expected and the permission found, and issues + -- an appropriate error message. + + ----------------------------------- + -- Check_Is_Less_Restrictive_Env -- + ----------------------------------- + + procedure Check_Is_Less_Restrictive_Env + (Exiting_Env : Perm_Env; + Entry_Env : Perm_Env) + is + Comp_Entry : Perm_Tree_Maps.Key_Option; + Iter_Entry, Iter_Exit : Perm_Tree_Access; + + begin + Comp_Entry := Get_First_Key (Entry_Env); + while Comp_Entry.Present loop + Iter_Entry := Get (Entry_Env, Comp_Entry.K); + pragma Assert (Iter_Entry /= null); + Iter_Exit := Get (Exiting_Env, Comp_Entry.K); + pragma Assert (Iter_Exit /= null); + Check_Is_Less_Restrictive_Tree + (New_Tree => Iter_Exit, + Orig_Tree => Iter_Entry, + E => Comp_Entry.K); + Comp_Entry := Get_Next_Key (Entry_Env); + end loop; + end Check_Is_Less_Restrictive_Env; + + ------------------------------------ + -- Check_Is_Less_Restrictive_Tree -- + ------------------------------------ + + procedure Check_Is_Less_Restrictive_Tree + (New_Tree : Perm_Tree_Access; + Orig_Tree : Perm_Tree_Access; + E : Entity_Id) + is + ----------------------- + -- Local Subprograms -- + ----------------------- + + procedure Check_Is_Less_Restrictive_Tree_Than + (Tree : Perm_Tree_Access; + Perm : Perm_Kind; + E : Entity_Id); + -- Auxiliary procedure to check that the tree N is less restrictive + -- than the given permission P. + + procedure Check_Is_More_Restrictive_Tree_Than + (Tree : Perm_Tree_Access; + Perm : Perm_Kind; + E : Entity_Id); + -- Auxiliary procedure to check that the tree N is more restrictive + -- than the given permission P. + + ----------------------------------------- + -- Check_Is_Less_Restrictive_Tree_Than -- + ----------------------------------------- + + procedure Check_Is_Less_Restrictive_Tree_Than + (Tree : Perm_Tree_Access; + Perm : Perm_Kind; + E : Entity_Id) + is + begin + if not (Permission (Tree) >= Perm) then + Perm_Error_Loop_Exit + (E, Loop_N, Permission (Tree), Perm); + end if; + + case Kind (Tree) is + when Entire_Object => + if not (Children_Permission (Tree) >= Perm) then + Perm_Error_Loop_Exit + (E, Loop_N, Children_Permission (Tree), Perm); + + end if; + + when Reference => + Check_Is_Less_Restrictive_Tree_Than + (Get_All (Tree), Perm, E); + + when Array_Component => + Check_Is_Less_Restrictive_Tree_Than + (Get_Elem (Tree), Perm, E); + + when Record_Component => + declare + Comp : Perm_Tree_Access; + begin + Comp := Perm_Tree_Maps.Get_First (Component (Tree)); + while Comp /= null loop + Check_Is_Less_Restrictive_Tree_Than (Comp, Perm, E); + Comp := + Perm_Tree_Maps.Get_Next (Component (Tree)); + end loop; + + Check_Is_Less_Restrictive_Tree_Than + (Other_Components (Tree), Perm, E); + end; + end case; + end Check_Is_Less_Restrictive_Tree_Than; + + ----------------------------------------- + -- Check_Is_More_Restrictive_Tree_Than -- + ----------------------------------------- + + procedure Check_Is_More_Restrictive_Tree_Than + (Tree : Perm_Tree_Access; + Perm : Perm_Kind; + E : Entity_Id) + is + begin + if not (Perm >= Permission (Tree)) then + Perm_Error_Loop_Exit + (E, Loop_N, Permission (Tree), Perm); + end if; + + case Kind (Tree) is + when Entire_Object => + if not (Perm >= Children_Permission (Tree)) then + Perm_Error_Loop_Exit + (E, Loop_N, Children_Permission (Tree), Perm); + end if; + + when Reference => + Check_Is_More_Restrictive_Tree_Than + (Get_All (Tree), Perm, E); + + when Array_Component => + Check_Is_More_Restrictive_Tree_Than + (Get_Elem (Tree), Perm, E); + + when Record_Component => + declare + Comp : Perm_Tree_Access; + begin + Comp := Perm_Tree_Maps.Get_First (Component (Tree)); + while Comp /= null loop + Check_Is_More_Restrictive_Tree_Than (Comp, Perm, E); + Comp := + Perm_Tree_Maps.Get_Next (Component (Tree)); + end loop; + + Check_Is_More_Restrictive_Tree_Than + (Other_Components (Tree), Perm, E); + end; + end case; + end Check_Is_More_Restrictive_Tree_Than; + + -- Start of processing for Check_Is_Less_Restrictive_Tree + + begin + if not (Permission (New_Tree) <= Permission (Orig_Tree)) then + Perm_Error_Loop_Exit + (E => E, + Loop_Id => Loop_N, + Perm => Permission (New_Tree), + Found_Perm => Permission (Orig_Tree)); + end if; + + case Kind (New_Tree) is + + -- Potentially folded tree. We check the other tree Orig_Tree to + -- check whether it is folded or not. If folded we just compare + -- their Permission and Children_Permission, if not, then we + -- look at the Children_Permission of the folded tree against + -- the unfolded tree Orig_Tree. + + when Entire_Object => + case Kind (Orig_Tree) is + when Entire_Object => + if not (Children_Permission (New_Tree) <= + Children_Permission (Orig_Tree)) + then + Perm_Error_Loop_Exit + (E, Loop_N, + Children_Permission (New_Tree), + Children_Permission (Orig_Tree)); + end if; + + when Reference => + Check_Is_More_Restrictive_Tree_Than + (Get_All (Orig_Tree), Children_Permission (New_Tree), E); + + when Array_Component => + Check_Is_More_Restrictive_Tree_Than + (Get_Elem (Orig_Tree), Children_Permission (New_Tree), E); + + when Record_Component => + declare + Comp : Perm_Tree_Access; + begin + Comp := Perm_Tree_Maps.Get_First + (Component (Orig_Tree)); + while Comp /= null loop + Check_Is_More_Restrictive_Tree_Than + (Comp, Children_Permission (New_Tree), E); + Comp := Perm_Tree_Maps.Get_Next + (Component (Orig_Tree)); + end loop; + + Check_Is_More_Restrictive_Tree_Than + (Other_Components (Orig_Tree), + Children_Permission (New_Tree), E); + end; + end case; + + when Reference => + case Kind (Orig_Tree) is + when Entire_Object => + Check_Is_Less_Restrictive_Tree_Than + (Get_All (New_Tree), Children_Permission (Orig_Tree), E); + + when Reference => + Check_Is_Less_Restrictive_Tree + (Get_All (New_Tree), Get_All (Orig_Tree), E); + + when others => + raise Program_Error; + end case; + + when Array_Component => + case Kind (Orig_Tree) is + when Entire_Object => + Check_Is_Less_Restrictive_Tree_Than + (Get_Elem (New_Tree), Children_Permission (Orig_Tree), E); + + when Array_Component => + Check_Is_Less_Restrictive_Tree + (Get_Elem (New_Tree), Get_Elem (Orig_Tree), E); + + when others => + raise Program_Error; + end case; + + when Record_Component => + declare + CompN : Perm_Tree_Access; + begin + CompN := + Perm_Tree_Maps.Get_First (Component (New_Tree)); + case Kind (Orig_Tree) is + when Entire_Object => + while CompN /= null loop + Check_Is_Less_Restrictive_Tree_Than + (CompN, Children_Permission (Orig_Tree), E); + + CompN := + Perm_Tree_Maps.Get_Next (Component (New_Tree)); + end loop; + + Check_Is_Less_Restrictive_Tree_Than + (Other_Components (New_Tree), + Children_Permission (Orig_Tree), + E); + + when Record_Component => + declare + + KeyO : Perm_Tree_Maps.Key_Option; + CompO : Perm_Tree_Access; + begin + KeyO := Perm_Tree_Maps.Get_First_Key + (Component (Orig_Tree)); + while KeyO.Present loop + pragma Assert (CompO /= null); + + Check_Is_Less_Restrictive_Tree (CompN, CompO, E); + + KeyO := Perm_Tree_Maps.Get_Next_Key + (Component (Orig_Tree)); + CompN := Perm_Tree_Maps.Get + (Component (New_Tree), KeyO.K); + CompO := Perm_Tree_Maps.Get + (Component (Orig_Tree), KeyO.K); + end loop; + + Check_Is_Less_Restrictive_Tree + (Other_Components (New_Tree), + Other_Components (Orig_Tree), + E); + end; + + when others => + raise Program_Error; + end case; + end; + end case; + end Check_Is_Less_Restrictive_Tree; + + -------------------------- + -- Perm_Error_Loop_Exit -- + -------------------------- + + procedure Perm_Error_Loop_Exit + (E : Entity_Id; + Loop_Id : Node_Id; + Perm : Perm_Kind; + Found_Perm : Perm_Kind) + is + begin + Error_Msg_Node_2 := Loop_Id; + Error_Msg_N ("insufficient permission for & when exiting loop &", E); + Perm_Mismatch (Exp_Perm => Perm, + Act_Perm => Found_Perm, + N => Loop_Id); + end Perm_Error_Loop_Exit; + + -- Local variables + + Loop_Name : constant Entity_Id := Entity (Identifier (Loop_N)); + Loop_Env : constant Perm_Env_Access := new Perm_Env; + + begin + -- Save environment prior to the loop + + Copy_Env (From => Current_Perm_Env, To => Loop_Env.all); + + -- Add saved environment to loop environment + + Set (Current_Loops_Envs, Loop_Name, Loop_Env); + + -- If the loop is not a plain-loop, then it may either never be entered, + -- or it may be exited after a number of iterations. Hence add the + -- current permission environment as the initial loop exit environment. + -- Otherwise, the loop exit environment remains empty until it is + -- populated by analyzing exit statements. + + if Present (Iteration_Scheme (Loop_N)) then + declare + Exit_Env : constant Perm_Env_Access := new Perm_Env; + begin + Copy_Env (From => Current_Perm_Env, To => Exit_Env.all); + Set (Current_Loops_Accumulators, Loop_Name, Exit_Env); + end; + end if; + + -- Analyze loop + + Check_Node (Iteration_Scheme (Loop_N)); + Check_List (Statements (Loop_N)); + + -- Check that environment gets less restrictive at end of loop + + Check_Is_Less_Restrictive_Env + (Exiting_Env => Current_Perm_Env, + Entry_Env => Loop_Env.all); + + -- Set environment to the one for exiting the loop + + declare + Exit_Env : constant Perm_Env_Access := + Get (Current_Loops_Accumulators, Loop_Name); + begin + Free_Env (Current_Perm_Env); + + -- In the normal case, Exit_Env is not null and we use it. In the + -- degraded case of a plain-loop without exit statements, Exit_Env is + -- null, and we use the initial permission environment at the start + -- of the loop to continue analysis. Any environment would be fine + -- here, since the code after the loop is dead code, but this way we + -- avoid spurious errors by having at least variables in scope inside + -- the environment. + + if Exit_Env /= null then + Copy_Env (From => Exit_Env.all, To => Current_Perm_Env); + else + Copy_Env (From => Loop_Env.all, To => Current_Perm_Env); + end if; + + Free_Env (Loop_Env.all); + Free_Env (Exit_Env.all); + end; + end Check_Loop_Statement; + + ---------------- + -- Check_Node -- + ---------------- + + procedure Check_Node (N : Node_Id) is + Mode_Before : constant Checking_Mode := Current_Checking_Mode; + begin + case Nkind (N) is + when N_Declaration => + Check_Declaration (N); + + when N_Subexpr => + Check_Expression (N); + + when N_Subtype_Indication => + Check_Node (Constraint (N)); + + when N_Body_Stub => + Check_Node (Get_Body_From_Stub (N)); + + when N_Statement_Other_Than_Procedure_Call => + Check_Statement (N); + + when N_Package_Body => + Check_Package_Body (N); + + when N_Subprogram_Body + | N_Entry_Body + | N_Task_Body + => + Check_Callable_Body (N); + + when N_Protected_Body => + Check_List (Declarations (N)); + + when N_Package_Declaration => + declare + Spec : constant Node_Id := Specification (N); + begin + Current_Checking_Mode := Read; + Check_List (Visible_Declarations (Spec)); + Check_List (Private_Declarations (Spec)); + + Return_Declarations (Visible_Declarations (Spec)); + Return_Declarations (Private_Declarations (Spec)); + end; + + when N_Iteration_Scheme => + Current_Checking_Mode := Read; + Check_Node (Condition (N)); + Check_Node (Iterator_Specification (N)); + Check_Node (Loop_Parameter_Specification (N)); + + when N_Case_Expression_Alternative => + Current_Checking_Mode := Read; + Check_List (Discrete_Choices (N)); + Current_Checking_Mode := Mode_Before; + Check_Node (Expression (N)); + + when N_Case_Statement_Alternative => + Current_Checking_Mode := Read; + Check_List (Discrete_Choices (N)); + Current_Checking_Mode := Mode_Before; + Check_List (Statements (N)); + + when N_Component_Association => + Check_Node (Expression (N)); + + when N_Handled_Sequence_Of_Statements => + Check_List (Statements (N)); + + when N_Parameter_Association => + Check_Node (Explicit_Actual_Parameter (N)); + + when N_Range_Constraint => + Check_Node (Range_Expression (N)); + + when N_Index_Or_Discriminant_Constraint => + Check_List (Constraints (N)); + + -- Checking should not be called directly on these nodes + + when N_Abortable_Part + | N_Accept_Alternative + | N_Access_Definition + | N_Access_Function_Definition + | N_Access_Procedure_Definition + | N_Access_To_Object_Definition + | N_Aspect_Specification + | N_Compilation_Unit + | N_Compilation_Unit_Aux + | N_Component_Clause + | N_Component_Definition + | N_Component_List + | N_Constrained_Array_Definition + | N_Contract + | N_Decimal_Fixed_Point_Definition + | N_Defining_Character_Literal + | N_Defining_Identifier + | N_Defining_Operator_Symbol + | N_Defining_Program_Unit_Name + | N_Delay_Alternative + | N_Derived_Type_Definition + | N_Designator + | N_Discriminant_Association + | N_Discriminant_Specification + | N_Elsif_Part + | N_Entry_Body_Formal_Part + | N_Enumeration_Type_Definition + | N_Entry_Call_Alternative + | N_Entry_Index_Specification + | N_Error + | N_Exception_Handler + | N_Floating_Point_Definition + | N_Formal_Decimal_Fixed_Point_Definition + | N_Formal_Derived_Type_Definition + | N_Formal_Discrete_Type_Definition + | N_Formal_Floating_Point_Definition + | N_Formal_Incomplete_Type_Definition + | N_Formal_Modular_Type_Definition + | N_Formal_Ordinary_Fixed_Point_Definition + | N_Formal_Private_Type_Definition + | N_Formal_Signed_Integer_Type_Definition + | N_Generic_Association + | N_Mod_Clause + | N_Modular_Type_Definition + | N_Ordinary_Fixed_Point_Definition + | N_Package_Specification + | N_Parameter_Specification + | N_Pragma_Argument_Association + | N_Protected_Definition + | N_Push_Pop_xxx_Label + | N_Real_Range_Specification + | N_Record_Definition + | N_SCIL_Dispatch_Table_Tag_Init + | N_SCIL_Dispatching_Call + | N_SCIL_Membership_Test + | N_Signed_Integer_Type_Definition + | N_Subunit + | N_Task_Definition + | N_Terminate_Alternative + | N_Triggering_Alternative + | N_Unconstrained_Array_Definition + | N_Unused_At_Start + | N_Unused_At_End + | N_Variant + | N_Variant_Part + => + raise Program_Error; + + -- Unsupported constructs in SPARK + + when N_Iterated_Component_Association => + Error_Msg_N ("unsupported construct in SPARK", N); + + -- Ignored constructs for pointer checking + + when N_Abstract_Subprogram_Declaration + | N_At_Clause + | N_Attribute_Definition_Clause + | N_Delta_Constraint + | N_Digits_Constraint + | N_Empty + | N_Enumeration_Representation_Clause + | N_Exception_Declaration + | N_Exception_Renaming_Declaration + | N_Formal_Package_Declaration + | N_Formal_Subprogram_Declaration + | N_Freeze_Entity + | N_Freeze_Generic_Entity + | N_Function_Instantiation + | N_Generic_Function_Renaming_Declaration + | N_Generic_Package_Declaration + | N_Generic_Package_Renaming_Declaration + | N_Generic_Procedure_Renaming_Declaration + | N_Generic_Subprogram_Declaration + | N_Implicit_Label_Declaration + | N_Itype_Reference + | N_Label + | N_Number_Declaration + | N_Object_Renaming_Declaration + | N_Others_Choice + | N_Package_Instantiation + | N_Package_Renaming_Declaration + | N_Pragma + | N_Procedure_Instantiation + | N_Record_Representation_Clause + | N_Subprogram_Declaration + | N_Subprogram_Renaming_Declaration + | N_Task_Type_Declaration + | N_Use_Package_Clause + | N_With_Clause + | N_Use_Type_Clause + | N_Validate_Unchecked_Conversion + => + null; + + -- The following nodes are rewritten by semantic analysis + + when N_Single_Protected_Declaration + | N_Single_Task_Declaration + => + raise Program_Error; + end case; + + Current_Checking_Mode := Mode_Before; + end Check_Node; + + ------------------------ + -- Check_Package_Body -- + ------------------------ + + procedure Check_Package_Body (Pack : Node_Id) is + Saved_Env : Perm_Env; + CorSp : Node_Id; + + begin + if Present (SPARK_Pragma (Defining_Entity (Pack, False))) then + if Get_SPARK_Mode_From_Annotation + (SPARK_Pragma (Defining_Entity (Pack))) /= Opt.On + then + return; + end if; + else + return; + end if; + + CorSp := Parent (Corresponding_Spec (Pack)); + while Nkind (CorSp) /= N_Package_Specification loop + CorSp := Parent (CorSp); + end loop; + + Check_List (Visible_Declarations (CorSp)); + + -- Save environment + + Copy_Env (Current_Perm_Env, + Saved_Env); + + Check_List (Private_Declarations (CorSp)); + + -- Set mode to Read, and then analyze declarations and statements + + Current_Checking_Mode := Read; + + Check_List (Declarations (Pack)); + Check_Node (Handled_Statement_Sequence (Pack)); + + -- Check RW for every stateful variable (i.e. in declarations) + + Return_Declarations (Private_Declarations (CorSp)); + Return_Declarations (Visible_Declarations (CorSp)); + Return_Declarations (Declarations (Pack)); + + -- Restore previous environment (i.e. delete every nonvisible + -- declaration) from environment. + + Free_Env (Current_Perm_Env); + Copy_Env (Saved_Env, + Current_Perm_Env); + end Check_Package_Body; + + ----------------- + -- Check_Param -- + ----------------- + + procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is + Mode : constant Entity_Kind := Ekind (Formal); + Mode_Before : constant Checking_Mode := Current_Checking_Mode; + + begin + case Current_Checking_Mode is + when Read => + case Formal_Kind'(Mode) is + when E_In_Parameter => + if Is_Borrowed_In (Formal) then + -- Borrowed in + + Current_Checking_Mode := Move; + else + -- Observed + + return; + end if; + + when E_Out_Parameter => + return; + + when E_In_Out_Parameter => + -- Borrowed in out + + Current_Checking_Mode := Move; + + end case; + + Check_Node (Actual); + + when Assign => + case Formal_Kind'(Mode) is + when E_In_Parameter => + null; + + when E_Out_Parameter + | E_In_Out_Parameter + => + -- Borrowed out or in out + + Process_Path (Actual); + + end case; + + when others => + raise Program_Error; + + end case; + Current_Checking_Mode := Mode_Before; + end Check_Param; + + -------------------------- + -- Check_Param_Observes -- + -------------------------- + + procedure Check_Param_Observes (Formal : Entity_Id; Actual : Node_Id) is + Mode : constant Entity_Kind := Ekind (Formal); + Mode_Before : constant Checking_Mode := Current_Checking_Mode; + + begin + case Mode is + when E_In_Parameter => + if not Is_Borrowed_In (Formal) then + -- Observed in + + Current_Checking_Mode := Observe; + Check_Node (Actual); + end if; + + when others => + null; + + end case; + + Current_Checking_Mode := Mode_Before; + end Check_Param_Observes; + + ---------------------- + -- Check_Param_Outs -- + ---------------------- + + procedure Check_Param_Outs (Formal : Entity_Id; Actual : Node_Id) is + Mode : constant Entity_Kind := Ekind (Formal); + Mode_Before : constant Checking_Mode := Current_Checking_Mode; + + begin + + case Mode is + when E_Out_Parameter => + -- Borrowed out + Current_Checking_Mode := Borrow_Out; + Check_Node (Actual); + + when others => + null; + + end case; + + Current_Checking_Mode := Mode_Before; + end Check_Param_Outs; + + ---------------------- + -- Check_Param_Read -- + ---------------------- + + procedure Check_Param_Read (Formal : Entity_Id; Actual : Node_Id) is + Mode : constant Entity_Kind := Ekind (Formal); + + begin + pragma Assert (Current_Checking_Mode = Read); + + case Formal_Kind'(Mode) is + when E_In_Parameter => + Check_Node (Actual); + + when E_Out_Parameter + | E_In_Out_Parameter + => + null; + + end case; + end Check_Param_Read; + + ------------------------- + -- Check_Safe_Pointers -- + ------------------------- + + procedure Check_Safe_Pointers (N : Node_Id) is + + -- Local subprograms + + procedure Check_List (L : List_Id); + -- Call the main analysis procedure on each element of the list + + procedure Initialize; + -- Initialize global variables before starting the analysis of a body + + ---------------- + -- Check_List -- + ---------------- + + procedure Check_List (L : List_Id) is + N : Node_Id; + begin + N := First (L); + while Present (N) loop + Check_Safe_Pointers (N); + Next (N); + end loop; + end Check_List; + + ---------------- + -- Initialize -- + ---------------- + + procedure Initialize is + begin + Reset (Current_Loops_Envs); + Reset (Current_Loops_Accumulators); + Reset (Current_Perm_Env); + Reset (Current_Initialization_Map); + end Initialize; + + -- Local variables + + Prag : Node_Id; + -- SPARK_Mode pragma in application + + -- Start of processing for Check_Safe_Pointers + + begin + Initialize; + + case Nkind (N) is + when N_Compilation_Unit => + Check_Safe_Pointers (Unit (N)); + + when N_Package_Body + | N_Package_Declaration + | N_Subprogram_Body + => + Prag := SPARK_Pragma (Defining_Entity (N)); + if Present (Prag) then + if Get_SPARK_Mode_From_Annotation (Prag) = Opt.Off then + return; + else + Check_Node (N); + end if; + + elsif Nkind (N) = N_Package_Body then + Check_List (Declarations (N)); + + elsif Nkind (N) = N_Package_Declaration then + Check_List (Private_Declarations (Specification (N))); + Check_List (Visible_Declarations (Specification (N))); + end if; + + when others => + null; + end case; + end Check_Safe_Pointers; + + --------------------- + -- Check_Statement -- + --------------------- + + procedure Check_Statement (Stmt : Node_Id) is + Mode_Before : constant Checking_Mode := Current_Checking_Mode; + begin + case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is + when N_Entry_Call_Statement => + Check_Call_Statement (Stmt); + + -- Move right-hand side first, and then assign left-hand side + + when N_Assignment_Statement => + if Is_Deep (Etype (Expression (Stmt))) then + Current_Checking_Mode := Move; + else + Current_Checking_Mode := Read; + end if; + + Check_Node (Expression (Stmt)); + Current_Checking_Mode := Assign; + Check_Node (Name (Stmt)); + + when N_Block_Statement => + declare + Saved_Env : Perm_Env; + + begin + -- Save environment + + Copy_Env (Current_Perm_Env, + Saved_Env); + + -- Analyze declarations and Handled_Statement_Sequences + + Current_Checking_Mode := Read; + Check_List (Declarations (Stmt)); + Check_Node (Handled_Statement_Sequence (Stmt)); + + -- Restore environment + + Free_Env (Current_Perm_Env); + Copy_Env (Saved_Env, + Current_Perm_Env); + end; + + when N_Case_Statement => + declare + Saved_Env : Perm_Env; + + -- Accumulator for the different branches + + New_Env : Perm_Env; + + Elmt : Node_Id := First (Alternatives (Stmt)); + + begin + Current_Checking_Mode := Read; + Check_Node (Expression (Stmt)); + Current_Checking_Mode := Mode_Before; + + -- Save environment + + Copy_Env (Current_Perm_Env, + Saved_Env); + + -- Here we have the original env in saved, current with a fresh + -- copy, and new aliased. + + -- First alternative + + Check_Node (Elmt); + Next (Elmt); + + Copy_Env (Current_Perm_Env, + New_Env); + Free_Env (Current_Perm_Env); + + -- Other alternatives + + while Present (Elmt) loop + -- Restore environment + + Copy_Env (Saved_Env, + Current_Perm_Env); + + Check_Node (Elmt); + + -- Merge Current_Perm_Env into New_Env + + Merge_Envs (New_Env, + Current_Perm_Env); + + Next (Elmt); + end loop; + + -- CLEANUP + Copy_Env (New_Env, + Current_Perm_Env); + + Free_Env (New_Env); + Free_Env (Saved_Env); + end; + + when N_Delay_Relative_Statement => + Check_Node (Expression (Stmt)); + + when N_Delay_Until_Statement => + Check_Node (Expression (Stmt)); + + when N_Loop_Statement => + Check_Loop_Statement (Stmt); + + -- If deep type expression, then move, else read + + when N_Simple_Return_Statement => + case Nkind (Expression (Stmt)) is + when N_Empty => + declare + -- ??? This does not take into account the fact that + -- a simple return inside an extended return statement + -- applies to the extended return statement. + Subp : constant Entity_Id := + Return_Applies_To (Return_Statement_Entity (Stmt)); + begin + Return_Parameters (Subp); + Return_Globals (Subp); + end; + + when others => + if Is_Deep (Etype (Expression (Stmt))) then + Current_Checking_Mode := Move; + elsif Is_Shallow (Etype (Expression (Stmt))) then + Current_Checking_Mode := Read; + else + raise Program_Error; + end if; + + Check_Node (Expression (Stmt)); + end case; + + when N_Extended_Return_Statement => + Check_List (Return_Object_Declarations (Stmt)); + Check_Node (Handled_Statement_Sequence (Stmt)); + + Return_Declarations (Return_Object_Declarations (Stmt)); + + declare + -- ??? This does not take into account the fact that a simple + -- return inside an extended return statement applies to the + -- extended return statement. + Subp : constant Entity_Id := + Return_Applies_To (Return_Statement_Entity (Stmt)); + begin + Return_Parameters (Subp); + Return_Globals (Subp); + end; + + -- Merge the current_Perm_Env with the accumulator for the given loop + + when N_Exit_Statement => + declare + Loop_Name : constant Entity_Id := Loop_Of_Exit (Stmt); + + Saved_Accumulator : constant Perm_Env_Access := + Get (Current_Loops_Accumulators, Loop_Name); + + Environment_Copy : constant Perm_Env_Access := + new Perm_Env; + begin + + Copy_Env (Current_Perm_Env, + Environment_Copy.all); + + if Saved_Accumulator = null then + Set (Current_Loops_Accumulators, + Loop_Name, Environment_Copy); + else + Merge_Envs (Saved_Accumulator.all, + Environment_Copy.all); + end if; + end; + + -- Copy environment, run on each branch, and then merge + + when N_If_Statement => + declare + Saved_Env : Perm_Env; + + -- Accumulator for the different branches + + New_Env : Perm_Env; + + begin + + Check_Node (Condition (Stmt)); + + -- Save environment + + Copy_Env (Current_Perm_Env, + Saved_Env); + + -- Here we have the original env in saved, current with a fresh + -- copy. + + -- THEN PART + + Check_List (Then_Statements (Stmt)); + + Copy_Env (Current_Perm_Env, + New_Env); + + Free_Env (Current_Perm_Env); + + -- Here the new_environment contains curr env after then block + + -- ELSIF part + declare + Elmt : Node_Id; + + begin + Elmt := First (Elsif_Parts (Stmt)); + while Present (Elmt) loop + -- Transfer into accumulator, and restore from save + + Copy_Env (Saved_Env, + Current_Perm_Env); + + Check_Node (Condition (Elmt)); + Check_List (Then_Statements (Stmt)); + + -- Merge Current_Perm_Env into New_Env + + Merge_Envs (New_Env, + Current_Perm_Env); + + Next (Elmt); + end loop; + end; + + -- ELSE part + + -- Restore environment before if + + Copy_Env (Saved_Env, + Current_Perm_Env); + + -- Here new environment contains the environment after then and + -- current the fresh copy of old one. + + Check_List (Else_Statements (Stmt)); + + Merge_Envs (New_Env, + Current_Perm_Env); + + -- CLEANUP + + Copy_Env (New_Env, + Current_Perm_Env); + + Free_Env (New_Env); + Free_Env (Saved_Env); + end; + + -- Unsupported constructs in SPARK + + when N_Abort_Statement + | N_Accept_Statement + | N_Asynchronous_Select + | N_Code_Statement + | N_Conditional_Entry_Call + | N_Goto_Statement + | N_Requeue_Statement + | N_Selective_Accept + | N_Timed_Entry_Call + => + Error_Msg_N ("unsupported construct in SPARK", Stmt); + + -- Ignored constructs for pointer checking + + when N_Null_Statement + | N_Raise_Statement + => + null; + + -- The following nodes are never generated in GNATprove mode + + when N_Compound_Statement + | N_Free_Statement + => + raise Program_Error; + end case; + end Check_Statement; + + -------------- + -- Get_Perm -- + -------------- + + function Get_Perm (N : Node_Id) return Perm_Kind is + Tree_Or_Perm : constant Perm_Or_Tree := Get_Perm_Or_Tree (N); + + begin + case Tree_Or_Perm.R is + when Folded => + return Tree_Or_Perm.Found_Permission; + + when Unfolded => + pragma Assert (Tree_Or_Perm.Tree_Access /= null); + return Permission (Tree_Or_Perm.Tree_Access); + + -- We encoutered a function call, hence the memory area is fresh, + -- which means that the association permission is RW. + + when Function_Call => + return Read_Write; + + end case; + end Get_Perm; + + ---------------------- + -- Get_Perm_Or_Tree -- + ---------------------- + + function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree is + begin + case Nkind (N) is + + -- Base identifier. Normally those are the roots of the trees stored + -- in the permission environment. + + when N_Defining_Identifier => + raise Program_Error; + + when N_Identifier + | N_Expanded_Name + => + declare + P : constant Entity_Id := Entity (N); + + C : constant Perm_Tree_Access := + Get (Current_Perm_Env, Unique_Entity (P)); + + begin + -- Setting the initialization map to True, so that this + -- variable cannot be ignored anymore when looking at end + -- of elaboration of package. + + Set (Current_Initialization_Map, Unique_Entity (P), True); + + if C = null then + -- No null possible here, there are no parents for the path. + -- This means we are using a global variable without adding + -- it in environment with a global aspect. + + Illegal_Global_Usage (N); + else + return (R => Unfolded, Tree_Access => C); + end if; + end; + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Get_Perm_Or_Tree (Expression (N)); + + -- Happening when we try to get the permission of a variable that + -- is a formal parameter. We get instead the defining identifier + -- associated with the parameter (which is the one that has been + -- stored for indexing). + + when N_Parameter_Specification => + return Get_Perm_Or_Tree (Defining_Identifier (N)); + + -- We get the permission tree of its prefix, and then get either the + -- subtree associated with that specific selection, or if we have a + -- leaf that folds its children, we take the children's permission + -- and return it using the discriminant Folded. + + when N_Selected_Component => + declare + C : constant Perm_Or_Tree := + Get_Perm_Or_Tree (Prefix (N)); + + begin + case C.R is + when Folded + | Function_Call + => + return C; + + when Unfolded => + pragma Assert (C.Tree_Access /= null); + + pragma Assert (Kind (C.Tree_Access) = Entire_Object + or else + Kind (C.Tree_Access) = Record_Component); + + if Kind (C.Tree_Access) = Record_Component then + declare + Selected_Component : constant Entity_Id := + Entity (Selector_Name (N)); + + Selected_C : constant Perm_Tree_Access := + Perm_Tree_Maps.Get + (Component (C.Tree_Access), Selected_Component); + + begin + if Selected_C = null then + return (R => Unfolded, + Tree_Access => + Other_Components (C.Tree_Access)); + else + return (R => Unfolded, + Tree_Access => Selected_C); + end if; + end; + elsif Kind (C.Tree_Access) = Entire_Object then + return (R => Folded, Found_Permission => + Children_Permission (C.Tree_Access)); + else + raise Program_Error; + end if; + end case; + end; + + -- We get the permission tree of its prefix, and then get either the + -- subtree associated with that specific selection, or if we have a + -- leaf that folds its children, we take the children's permission + -- and return it using the discriminant Folded. + + when N_Indexed_Component + | N_Slice + => + declare + C : constant Perm_Or_Tree := + Get_Perm_Or_Tree (Prefix (N)); + + begin + case C.R is + when Folded + | Function_Call + => + return C; + + when Unfolded => + pragma Assert (C.Tree_Access /= null); + + pragma Assert (Kind (C.Tree_Access) = Entire_Object + or else + Kind (C.Tree_Access) = Array_Component); + + if Kind (C.Tree_Access) = Array_Component then + pragma Assert (Get_Elem (C.Tree_Access) /= null); + + return (R => Unfolded, + Tree_Access => Get_Elem (C.Tree_Access)); + elsif Kind (C.Tree_Access) = Entire_Object then + return (R => Folded, Found_Permission => + Children_Permission (C.Tree_Access)); + else + raise Program_Error; + end if; + end case; + end; + + -- We get the permission tree of its prefix, and then get either the + -- subtree associated with that specific selection, or if we have a + -- leaf that folds its children, we take the children's permission + -- and return it using the discriminant Folded. + + when N_Explicit_Dereference => + declare + C : constant Perm_Or_Tree := + Get_Perm_Or_Tree (Prefix (N)); + + begin + case C.R is + when Folded + | Function_Call + => + return C; + + when Unfolded => + pragma Assert (C.Tree_Access /= null); + + pragma Assert (Kind (C.Tree_Access) = Entire_Object + or else + Kind (C.Tree_Access) = Reference); + + if Kind (C.Tree_Access) = Reference then + if Get_All (C.Tree_Access) = null then + -- Hash_Table_Error + raise Program_Error; + else + return + (R => Unfolded, + Tree_Access => Get_All (C.Tree_Access)); + end if; + elsif Kind (C.Tree_Access) = Entire_Object then + return (R => Folded, Found_Permission => + Children_Permission (C.Tree_Access)); + else + raise Program_Error; + end if; + end case; + end; + + -- The name contains a function call, hence the given path is always + -- new. We do not have to check for anything. + + when N_Function_Call => + return (R => Function_Call); + + when others => + raise Program_Error; + end case; + end Get_Perm_Or_Tree; + + ------------------- + -- Get_Perm_Tree -- + ------------------- + + function Get_Perm_Tree + (N : Node_Id) + return Perm_Tree_Access + is + begin + case Nkind (N) is + + -- Base identifier. Normally those are the roots of the trees stored + -- in the permission environment. + + when N_Defining_Identifier => + raise Program_Error; + + when N_Identifier + | N_Expanded_Name + => + declare + P : constant Node_Id := Entity (N); + + C : constant Perm_Tree_Access := + Get (Current_Perm_Env, Unique_Entity (P)); + + begin + -- Setting the initialization map to True, so that this + -- variable cannot be ignored anymore when looking at end + -- of elaboration of package. + + Set (Current_Initialization_Map, Unique_Entity (P), True); + + if C = null then + -- No null possible here, there are no parents for the path. + -- This means we are using a global variable without adding + -- it in environment with a global aspect. + + Illegal_Global_Usage (N); + else + return C; + end if; + end; + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Get_Perm_Tree (Expression (N)); + + when N_Parameter_Specification => + return Get_Perm_Tree (Defining_Identifier (N)); + + -- We get the permission tree of its prefix, and then get either the + -- subtree associated with that specific selection, or if we have a + -- leaf that folds its children, we unroll it in one step. + + when N_Selected_Component => + declare + C : constant Perm_Tree_Access := + Get_Perm_Tree (Prefix (N)); + + begin + if C = null then + -- If null then it means we went through a function call + + return null; + end if; + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Record_Component); + + if Kind (C) = Record_Component then + -- The tree is unfolded. We just return the subtree. + + declare + Selected_Component : constant Entity_Id := + Entity (Selector_Name (N)); + Selected_C : constant Perm_Tree_Access := + Perm_Tree_Maps.Get + (Component (C), Selected_Component); + + begin + if Selected_C = null then + return Other_Components (C); + end if; + + return Selected_C; + end; + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace the node with + -- Record_Component. + + Elem : Node_Id; + + -- Create the unrolled nodes + + Son : Perm_Tree_Access; + + Child_Perm : constant Perm_Kind := + Children_Permission (C); + + begin + + -- We change the current node from Entire_Object to + -- Record_Component with same permission and an empty + -- hash table as component list. + + C.all.Tree := + (Kind => Record_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Permission (C), + Component => Perm_Tree_Maps.Nil, + Other_Components => + new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + -- Is_Node_Deep is true, to be conservative + Is_Node_Deep => True, + Permission => Child_Perm, + Children_Permission => Child_Perm) + ) + ); + + -- We fill the hash table with all sons of the record, + -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant + (Etype (Prefix (N))); + + while Present (Elem) loop + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (Elem)), + Permission => Child_Perm, + Children_Permission => Child_Perm)); + + Perm_Tree_Maps.Set + (C.all.Tree.Component, Elem, Son); + + Next_Component_Or_Discriminant (Elem); + end loop; + + -- we return the tree to the sons, so that the recursion + -- can continue. + + declare + Selected_Component : constant Entity_Id := + Entity (Selector_Name (N)); + + Selected_C : constant Perm_Tree_Access := + Perm_Tree_Maps.Get + (Component (C), Selected_Component); + + begin + pragma Assert (Selected_C /= null); + + return Selected_C; + end; + + end; + else + raise Program_Error; + end if; + end; + + -- We set the permission tree of its prefix, and then we extract from + -- the returned pointer the subtree. If folded, we unroll the tree at + -- one step. + + when N_Indexed_Component + | N_Slice + => + declare + C : constant Perm_Tree_Access := + Get_Perm_Tree (Prefix (N)); + + begin + if C = null then + -- If null then we went through a function call + + return null; + end if; + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Array_Component); + + if Kind (C) = Array_Component then + -- The tree is unfolded. We just return the elem subtree + + pragma Assert (Get_Elem (C) = null); + + return Get_Elem (C); + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace node with Array_Component. + + Son : Perm_Tree_Access; + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Children_Permission (C), + Children_Permission => Children_Permission (C))); + + -- We change the current node from Entire_Object + -- to Array_Component with same permission and the + -- previously defined son. + + C.all.Tree := (Kind => Array_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Permission (C), + Get_Elem => Son); + + return Get_Elem (C); + end; + else + raise Program_Error; + end if; + end; + + -- We get the permission tree of its prefix, and then get either the + -- subtree associated with that specific selection, or if we have a + -- leaf that folds its children, we unroll the tree. + + when N_Explicit_Dereference => + declare + C : Perm_Tree_Access; + + begin + C := Get_Perm_Tree (Prefix (N)); + + if C = null then + -- If null, we went through a function call + + return null; + end if; + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Reference); + + if Kind (C) = Reference then + -- The tree is unfolded. We return the elem subtree + + if Get_All (C) = null then + -- Hash_Table_Error + raise Program_Error; + end if; + + return Get_All (C); + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace the node with Reference. + + Son : Perm_Tree_Access; + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (N)), + Permission => Children_Permission (C), + Children_Permission => Children_Permission (C))); + + -- We change the current node from Entire_Object to + -- Reference with same permission and the previous son. + + pragma Assert (Is_Node_Deep (C)); + + C.all.Tree := (Kind => Reference, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Permission (C), + Get_All => Son); + + return Get_All (C); + end; + else + raise Program_Error; + end if; + end; + + -- No permission tree for function calls + + when N_Function_Call => + return null; + + when others => + raise Program_Error; + end case; + end Get_Perm_Tree; + + --------- + -- Glb -- + --------- + + function Glb (P1, P2 : Perm_Kind) return Perm_Kind + is + begin + case P1 is + when No_Access => + return No_Access; + + when Read_Only => + case P2 is + when No_Access + | Write_Only + => + return No_Access; + + when Read_Perm => + return Read_Only; + end case; + + when Write_Only => + case P2 is + when No_Access + | Read_Only + => + return No_Access; + + when Write_Perm => + return Write_Only; + end case; + + when Read_Write => + return P2; + end case; + end Glb; + + --------------- + -- Has_Alias -- + --------------- + + function Has_Alias + (N : Node_Id) + return Boolean + is + function Has_Alias_Deep (Typ : Entity_Id) return Boolean; + function Has_Alias_Deep (Typ : Entity_Id) return Boolean + is + Comp : Node_Id; + begin + + if Is_Array_Type (Typ) + and then Has_Aliased_Components (Typ) + then + return True; + + -- Note: Has_Aliased_Components applies only to arrays + + elsif Is_Record_Type (Typ) then + -- It is possible to have an aliased discriminant, so they must be + -- checked along with normal components. + + Comp := First_Component_Or_Discriminant (Typ); + while Present (Comp) loop + if Is_Aliased (Comp) + or else Is_Aliased (Etype (Comp)) + then + return True; + end if; + + if Has_Alias_Deep (Etype (Comp)) then + return True; + end if; + + Next_Component_Or_Discriminant (Comp); + end loop; + return False; + else + return Is_Aliased (Typ); + end if; + end Has_Alias_Deep; + + begin + case Nkind (N) is + + when N_Identifier + | N_Expanded_Name + => + return Has_Alias_Deep (Etype (N)); + + when N_Defining_Identifier => + return Has_Alias_Deep (Etype (N)); + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Has_Alias (Expression (N)); + + when N_Parameter_Specification => + return Has_Alias (Defining_Identifier (N)); + + when N_Selected_Component => + case Nkind (Selector_Name (N)) is + when N_Identifier => + if Is_Aliased (Entity (Selector_Name (N))) then + return True; + end if; + + when others => null; + + end case; + + return Has_Alias (Prefix (N)); + + when N_Indexed_Component + | N_Slice + => + return Has_Alias (Prefix (N)); + + when N_Explicit_Dereference => + return True; + + when N_Function_Call => + return False; + + when N_Attribute_Reference => + if Is_Deep (Etype (Prefix (N))) then + raise Program_Error; + end if; + return False; + + when others => + return False; + end case; + end Has_Alias; + + ------------------------- + -- Has_Array_Component -- + ------------------------- + + function Has_Array_Component (N : Node_Id) return Boolean is + begin + case Nkind (N) is + -- Base identifier. There is no array component here. + + when N_Identifier + | N_Expanded_Name + | N_Defining_Identifier + => + return False; + + -- We check if the expression inside the conversion has an array + -- component. + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Has_Array_Component (Expression (N)); + + -- We check if the prefix has an array component + + when N_Selected_Component => + return Has_Array_Component (Prefix (N)); + + -- We found the array component, return True + + when N_Indexed_Component + | N_Slice + => + return True; + + -- We check if the prefix has an array component + + when N_Explicit_Dereference => + return Has_Array_Component (Prefix (N)); + + when N_Function_Call => + return False; + + when others => + raise Program_Error; + end case; + end Has_Array_Component; + + ---------------------------- + -- Has_Function_Component -- + ---------------------------- + + function Has_Function_Component (N : Node_Id) return Boolean is + begin + case Nkind (N) is + -- Base identifier. There is no function component here. + + when N_Identifier + | N_Expanded_Name + | N_Defining_Identifier + => + return False; + + -- We check if the expression inside the conversion has a function + -- component. + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Has_Function_Component (Expression (N)); + + -- We check if the prefix has a function component + + when N_Selected_Component => + return Has_Function_Component (Prefix (N)); + + -- We check if the prefix has a function component + + when N_Indexed_Component + | N_Slice + => + return Has_Function_Component (Prefix (N)); + + -- We check if the prefix has a function component + + when N_Explicit_Dereference => + return Has_Function_Component (Prefix (N)); + + -- We found the function component, return True + + when N_Function_Call => + return True; + + when others => + raise Program_Error; + + end case; + end Has_Function_Component; + + -------- + -- Hp -- + -------- + + procedure Hp (P : Perm_Env) is + Elem : Perm_Tree_Maps.Key_Option; + + begin + Elem := Get_First_Key (P); + while Elem.Present loop + Print_Node_Briefly (Elem.K); + Elem := Get_Next_Key (P); + end loop; + end Hp; + + -------------------------- + -- Illegal_Global_Usage -- + -------------------------- + + procedure Illegal_Global_Usage (N : Node_Or_Entity_Id) is + begin + Error_Msg_NE ("cannot use global variable & of deep type", N, N); + Error_Msg_N ("\without prior declaration in a Global aspect", N); + + Errout.Finalize (Last_Call => True); + Errout.Output_Messages; + Exit_Program (E_Errors); + end Illegal_Global_Usage; + + -------------------- + -- Is_Borrowed_In -- + -------------------- + + function Is_Borrowed_In (E : Entity_Id) return Boolean is + begin + return Is_Access_Type (Etype (E)) + and then not Is_Access_Constant (Etype (E)); + end Is_Borrowed_In; + + ------------- + -- Is_Deep -- + ------------- + + function Is_Deep (E : Entity_Id) return Boolean is + function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean; + + function Is_Private_Entity_Mode_Off (E : Entity_Id) return Boolean is + Decl : Node_Id; + Pack_Decl : Node_Id; + + begin + if Is_Itype (E) then + Decl := Associated_Node_For_Itype (E); + else + Decl := Parent (E); + end if; + + Pack_Decl := Parent (Parent (Decl)); + + if Nkind (Pack_Decl) /= N_Package_Declaration then + return False; + end if; + + return + Present (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) + and then Get_SPARK_Mode_From_Annotation + (SPARK_Aux_Pragma (Defining_Entity (Pack_Decl))) = Off; + end Is_Private_Entity_Mode_Off; + begin + pragma Assert (Is_Type (E)); + + case Ekind (E) is + when Scalar_Kind => + return False; + + when Access_Kind => + return True; + + -- Just check the depth of its component type + + when E_Array_Type + | E_Array_Subtype + => + return Is_Deep (Component_Type (E)); + + when E_String_Literal_Subtype => + return False; + + -- Per RM 8.11 for class-wide types + + when E_Class_Wide_Subtype + | E_Class_Wide_Type + => + return True; + + -- ??? What about hidden components + + when E_Record_Type + | E_Record_Subtype + => + declare + Elmt : Entity_Id; + + begin + Elmt := First_Component_Or_Discriminant (E); + while Present (Elmt) loop + if Is_Deep (Etype (Elmt)) then + return True; + else + Next_Component_Or_Discriminant (Elmt); + end if; + end loop; + + return False; + end; + + when Private_Kind => + if Is_Private_Entity_Mode_Off (E) then + return False; + else + if Present (Full_View (E)) then + return Is_Deep (Full_View (E)); + else + return True; + end if; + end if; + + when E_Incomplete_Type => + return True; + + when E_Incomplete_Subtype => + return True; + + -- No problem with synchronized types + + when E_Protected_Type + | E_Protected_Subtype + | E_Task_Subtype + | E_Task_Type + => + return False; + + when E_Exception_Type => + return False; + + when others => + raise Program_Error; + end case; + end Is_Deep; + + ---------------- + -- Is_Shallow -- + ---------------- + + function Is_Shallow (E : Entity_Id) return Boolean is + begin + pragma Assert (Is_Type (E)); + return not Is_Deep (E); + end Is_Shallow; + + ------------------ + -- Loop_Of_Exit -- + ------------------ + + function Loop_Of_Exit (N : Node_Id) return Entity_Id is + Nam : Node_Id := Name (N); + Stmt : Node_Id := N; + begin + if No (Nam) then + while Present (Stmt) loop + Stmt := Parent (Stmt); + if Nkind (Stmt) = N_Loop_Statement then + Nam := Identifier (Stmt); + exit; + end if; + end loop; + end if; + return Entity (Nam); + end Loop_Of_Exit; + --------- + -- Lub -- + --------- + + function Lub (P1, P2 : Perm_Kind) return Perm_Kind + is + begin + case P1 is + when No_Access => + return P2; + + when Read_Only => + case P2 is + when No_Access + | Read_Only + => + return Read_Only; + + when Write_Perm => + return Read_Write; + end case; + + when Write_Only => + case P2 is + when No_Access + | Write_Only + => + return Write_Only; + + when Read_Perm => + return Read_Write; + end case; + + when Read_Write => + return Read_Write; + end case; + end Lub; + + ---------------- + -- Merge_Envs -- + ---------------- + + procedure Merge_Envs + (Target : in out Perm_Env; + Source : in out Perm_Env) + is + procedure Merge_Trees + (Target : Perm_Tree_Access; + Source : Perm_Tree_Access); + + procedure Merge_Trees + (Target : Perm_Tree_Access; + Source : Perm_Tree_Access) + is + procedure Apply_Glb_Tree + (A : Perm_Tree_Access; + P : Perm_Kind); + + procedure Apply_Glb_Tree + (A : Perm_Tree_Access; + P : Perm_Kind) + is + begin + A.all.Tree.Permission := Glb (Permission (A), P); + + case Kind (A) is + when Entire_Object => + A.all.Tree.Children_Permission := + Glb (Children_Permission (A), P); + + when Reference => + Apply_Glb_Tree (Get_All (A), P); + + when Array_Component => + Apply_Glb_Tree (Get_Elem (A), P); + + when Record_Component => + declare + Comp : Perm_Tree_Access; + begin + Comp := Perm_Tree_Maps.Get_First (Component (A)); + while Comp /= null loop + Apply_Glb_Tree (Comp, P); + Comp := Perm_Tree_Maps.Get_Next (Component (A)); + end loop; + + Apply_Glb_Tree (Other_Components (A), P); + end; + end case; + end Apply_Glb_Tree; + + Perm : constant Perm_Kind := + Glb (Permission (Target), Permission (Source)); + + begin + pragma Assert (Is_Node_Deep (Target) = Is_Node_Deep (Source)); + Target.all.Tree.Permission := Perm; + + case Kind (Target) is + when Entire_Object => + declare + Child_Perm : constant Perm_Kind := + Children_Permission (Target); + + begin + case Kind (Source) is + when Entire_Object => + Target.all.Tree.Children_Permission := + Glb (Child_Perm, Children_Permission (Source)); + + when Reference => + Copy_Tree (Source, Target); + Target.all.Tree.Permission := Perm; + Apply_Glb_Tree (Get_All (Target), Child_Perm); + + when Array_Component => + Copy_Tree (Source, Target); + Target.all.Tree.Permission := Perm; + Apply_Glb_Tree (Get_Elem (Target), Child_Perm); + + when Record_Component => + Copy_Tree (Source, Target); + Target.all.Tree.Permission := Perm; + declare + Comp : Perm_Tree_Access; + + begin + Comp := + Perm_Tree_Maps.Get_First (Component (Target)); + while Comp /= null loop + -- Apply glb tree on every component subtree + + Apply_Glb_Tree (Comp, Child_Perm); + Comp := Perm_Tree_Maps.Get_Next + (Component (Target)); + end loop; + end; + Apply_Glb_Tree (Other_Components (Target), Child_Perm); + + end case; + end; + when Reference => + case Kind (Source) is + when Entire_Object => + Apply_Glb_Tree (Get_All (Target), + Children_Permission (Source)); + + when Reference => + Merge_Trees (Get_All (Target), Get_All (Source)); + + when others => + raise Program_Error; + + end case; + + when Array_Component => + case Kind (Source) is + when Entire_Object => + Apply_Glb_Tree (Get_Elem (Target), + Children_Permission (Source)); + + when Array_Component => + Merge_Trees (Get_Elem (Target), Get_Elem (Source)); + + when others => + raise Program_Error; + + end case; + + when Record_Component => + case Kind (Source) is + when Entire_Object => + declare + Child_Perm : constant Perm_Kind := + Children_Permission (Source); + + Comp : Perm_Tree_Access; + + begin + Comp := Perm_Tree_Maps.Get_First + (Component (Target)); + while Comp /= null loop + -- Apply glb tree on every component subtree + + Apply_Glb_Tree (Comp, Child_Perm); + Comp := + Perm_Tree_Maps.Get_Next (Component (Target)); + end loop; + Apply_Glb_Tree (Other_Components (Target), Child_Perm); + end; + + when Record_Component => + declare + Key_Source : Perm_Tree_Maps.Key_Option; + CompTarget : Perm_Tree_Access; + CompSource : Perm_Tree_Access; + + begin + Key_Source := Perm_Tree_Maps.Get_First_Key + (Component (Source)); + + while Key_Source.Present loop + CompSource := Perm_Tree_Maps.Get + (Component (Source), Key_Source.K); + CompTarget := Perm_Tree_Maps.Get + (Component (Target), Key_Source.K); + + pragma Assert (CompSource /= null); + Merge_Trees (CompTarget, CompSource); + + Key_Source := Perm_Tree_Maps.Get_Next_Key + (Component (Source)); + end loop; + + Merge_Trees (Other_Components (Target), + Other_Components (Source)); + end; + + when others => + raise Program_Error; + + end case; + end case; + end Merge_Trees; + + CompTarget : Perm_Tree_Access; + CompSource : Perm_Tree_Access; + KeyTarget : Perm_Tree_Maps.Key_Option; + + begin + KeyTarget := Get_First_Key (Target); + -- Iterate over every tree of the environment in the target, and merge + -- it with the source if there is such a similar one that exists. If + -- there is none, then skip. + while KeyTarget.Present loop + + CompSource := Get (Source, KeyTarget.K); + CompTarget := Get (Target, KeyTarget.K); + + pragma Assert (CompTarget /= null); + + if CompSource /= null then + Merge_Trees (CompTarget, CompSource); + Remove (Source, KeyTarget.K); + end if; + + KeyTarget := Get_Next_Key (Target); + end loop; + + -- Iterate over every tree of the environment of the source. And merge + -- again. If there is not any tree of the target then just copy the tree + -- from source to target. + declare + KeySource : Perm_Tree_Maps.Key_Option; + begin + KeySource := Get_First_Key (Source); + while KeySource.Present loop + + CompSource := Get (Source, KeySource.K); + CompTarget := Get (Target, KeySource.K); + + if CompTarget = null then + CompTarget := new Perm_Tree_Wrapper'(CompSource.all); + Copy_Tree (CompSource, CompTarget); + Set (Target, KeySource.K, CompTarget); + else + Merge_Trees (CompTarget, CompSource); + end if; + + KeySource := Get_Next_Key (Source); + end loop; + end; + + Free_Env (Source); + end Merge_Envs; + + ---------------- + -- Perm_Error -- + ---------------- + + procedure Perm_Error + (N : Node_Id; + Perm : Perm_Kind; + Found_Perm : Perm_Kind) + is + procedure Set_Root_Object + (Path : Node_Id; + Obj : out Entity_Id; + Deref : out Boolean); + -- Set the root object Obj, and whether the path contains a dereference, + -- from a path Path. + + --------------------- + -- Set_Root_Object -- + --------------------- + + procedure Set_Root_Object + (Path : Node_Id; + Obj : out Entity_Id; + Deref : out Boolean) + is + begin + case Nkind (Path) is + when N_Identifier + | N_Expanded_Name + => + Obj := Entity (Path); + Deref := False; + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + Set_Root_Object (Expression (Path), Obj, Deref); + + when N_Indexed_Component + | N_Selected_Component + | N_Slice + => + Set_Root_Object (Prefix (Path), Obj, Deref); + + when N_Explicit_Dereference => + Set_Root_Object (Prefix (Path), Obj, Deref); + Deref := True; + + when others => + raise Program_Error; + end case; + end Set_Root_Object; + + -- Local variables + + Root : Entity_Id; + Is_Deref : Boolean; + + -- Start of processing for Perm_Error + + begin + Set_Root_Object (N, Root, Is_Deref); + + if Is_Deref then + Error_Msg_NE + ("insufficient permission on dereference from &", N, Root); + else + Error_Msg_NE ("insufficient permission for &", N, Root); + end if; + + Perm_Mismatch (Perm, Found_Perm, N); + end Perm_Error; + + ------------------------------- + -- Perm_Error_Subprogram_End -- + ------------------------------- + + procedure Perm_Error_Subprogram_End + (E : Entity_Id; + Subp : Entity_Id; + Perm : Perm_Kind; + Found_Perm : Perm_Kind) + is + begin + Error_Msg_Node_2 := Subp; + Error_Msg_NE ("insufficient permission for & when returning from &", + Subp, E); + Perm_Mismatch (Perm, Found_Perm, Subp); + end Perm_Error_Subprogram_End; + + ------------------ + -- Process_Path -- + ------------------ + + procedure Process_Path (N : Node_Id) is + Root : constant Entity_Id := Get_Enclosing_Object (N); + begin + -- We ignore if yielding to synchronized + + if Present (Root) + and then Is_Synchronized_Object (Root) + then + return; + end if; + + -- We ignore shallow unaliased. They are checked in flow analysis, + -- allowing backward compatibility. + + if not Has_Alias (N) + and then Is_Shallow (Etype (N)) + then + return; + end if; + + declare + Perm_N : constant Perm_Kind := Get_Perm (N); + + begin + + case Current_Checking_Mode is + -- Check permission R, do nothing + + when Read => + if Perm_N not in Read_Perm then + Perm_Error (N, Read_Only, Perm_N); + end if; + + -- If shallow type no need for RW, only R + + when Move => + if Is_Shallow (Etype (N)) then + if Perm_N not in Read_Perm then + Perm_Error (N, Read_Only, Perm_N); + end if; + else + -- Check permission RW if deep + + if Perm_N /= Read_Write then + Perm_Error (N, Read_Write, Perm_N); + end if; + + declare + -- Set permission to W to the path and any of its prefix + + Tree : constant Perm_Tree_Access := + Set_Perm_Prefixes_Move (N, Move); + + begin + if Tree = null then + -- We went through a function call, no permission to + -- modify. + + return; + end if; + + -- Set permissions to + -- No for any extension with more .all + -- W for any deep extension with same number of .all + -- RW for any shallow extension with same number of .all + + Set_Perm_Extensions_Move (Tree, Etype (N)); + end; + end if; + + -- Check permission RW + + when Super_Move => + if Perm_N /= Read_Write then + Perm_Error (N, Read_Write, Perm_N); + end if; + + declare + -- Set permission to No to the path and any of its prefix up + -- to the first .all and then W. + + Tree : constant Perm_Tree_Access := + Set_Perm_Prefixes_Move (N, Super_Move); + + begin + if Tree = null then + -- We went through a function call, no permission to + -- modify. + + return; + end if; + + -- Set permissions to No on any strict extension of the path + + Set_Perm_Extensions (Tree, No_Access); + end; + + -- Check permission W + + when Assign => + if Perm_N not in Write_Perm then + Perm_Error (N, Write_Only, Perm_N); + end if; + + -- If the tree has an array component, then the permissions do + -- not get modified by the assignment. + + if Has_Array_Component (N) then + return; + end if; + + -- Same if has function component + + if Has_Function_Component (N) then + return; + end if; + + declare + -- Get the permission tree for the path + + Tree : constant Perm_Tree_Access := + Get_Perm_Tree (N); + + Dummy : Perm_Tree_Access; + + begin + if Tree = null then + -- We went through a function call, no permission to + -- modify. + + return; + end if; + + -- Set permission RW for it and all of its extensions + + Tree.all.Tree.Permission := Read_Write; + + Set_Perm_Extensions (Tree, Read_Write); + + -- Normalize the permission tree + + Dummy := Set_Perm_Prefixes_Assign (N); + end; + + -- Check permission W + + when Borrow_Out => + if Perm_N not in Write_Perm then + Perm_Error (N, Write_Only, Perm_N); + end if; + + declare + -- Set permission to No to the path and any of its prefixes + + Tree : constant Perm_Tree_Access := + Set_Perm_Prefixes_Borrow_Out (N); + + begin + if Tree = null then + -- We went through a function call, no permission to + -- modify. + + return; + end if; + + -- Set permissions to No on any strict extension of the path + + Set_Perm_Extensions (Tree, No_Access); + end; + + when Observe => + if Perm_N not in Read_Perm then + Perm_Error (N, Read_Only, Perm_N); + end if; + + if Is_By_Copy_Type (Etype (N)) then + return; + end if; + + declare + -- Set permission to No on the path and any of its prefixes + + Tree : constant Perm_Tree_Access := + Set_Perm_Prefixes_Observe (N); + + begin + if Tree = null then + -- We went through a function call, no permission to + -- modify. + + return; + end if; + + -- Set permissions to No on any strict extension of the path + + Set_Perm_Extensions (Tree, Read_Only); + end; + end case; + end; + end Process_Path; + + ------------------------- + -- Return_Declarations -- + ------------------------- + + procedure Return_Declarations (L : List_Id) is + + procedure Return_Declaration (Decl : Node_Id); + -- Check correct permissions for every declared object + + ------------------------ + -- Return_Declaration -- + ------------------------ + + procedure Return_Declaration (Decl : Node_Id) is + begin + if Nkind (Decl) = N_Object_Declaration then + -- Check RW for object declared, unless the object has never been + -- initialized. + + if Get (Current_Initialization_Map, + Unique_Entity (Defining_Identifier (Decl))) = False + then + return; + end if; + + -- We ignore shallow unaliased. They are checked in flow analysis, + -- allowing backward compatibility. + + if not Has_Alias (Defining_Identifier (Decl)) + and then Is_Shallow (Etype (Defining_Identifier (Decl))) + then + return; + end if; + + declare + Elem : constant Perm_Tree_Access := + Get (Current_Perm_Env, + Unique_Entity (Defining_Identifier (Decl))); + + begin + if Elem = null then + -- Here we are on a declaration. Hence it should have been + -- added in the environment when analyzing this node with + -- mode Read. Hence it is not possible to find a null + -- pointer here. + + -- Hash_Table_Error + raise Program_Error; + end if; + + if Permission (Elem) /= Read_Write then + Perm_Error (Decl, Read_Write, Permission (Elem)); + end if; + end; + end if; + end Return_Declaration; + + -- Local Variables + + N : Node_Id; + + -- Start of processing for Return_Declarations + + begin + N := First (L); + while Present (N) loop + Return_Declaration (N); + Next (N); + end loop; + end Return_Declarations; + + -------------------- + -- Return_Globals -- + -------------------- + + procedure Return_Globals (Subp : Entity_Id) is + + procedure Return_Globals_From_List + (First_Item : Node_Id; + Kind : Formal_Kind); + -- Return global items from the list starting at Item + + procedure Return_Globals_Of_Mode (Global_Mode : Name_Id); + -- Return global items for the mode Global_Mode + + ------------------------------ + -- Return_Globals_From_List -- + ------------------------------ + + procedure Return_Globals_From_List + (First_Item : Node_Id; + Kind : Formal_Kind) + is + Item : Node_Id := First_Item; + E : Entity_Id; + + begin + while Present (Item) loop + E := Entity (Item); + + -- Ignore abstract states, which play no role in pointer aliasing + + if Ekind (E) = E_Abstract_State then + null; + else + Return_Parameter_Or_Global (E, Kind, Subp); + end if; + Next_Global (Item); + end loop; + end Return_Globals_From_List; + + ---------------------------- + -- Return_Globals_Of_Mode -- + ---------------------------- + + procedure Return_Globals_Of_Mode (Global_Mode : Name_Id) is + Kind : Formal_Kind; + + begin + case Global_Mode is + when Name_Input | Name_Proof_In => + Kind := E_In_Parameter; + when Name_Output => + Kind := E_Out_Parameter; + when Name_In_Out => + Kind := E_In_Out_Parameter; + when others => + raise Program_Error; + end case; + + -- Return both global items from Global and Refined_Global pragmas + + Return_Globals_From_List (First_Global (Subp, Global_Mode), Kind); + Return_Globals_From_List + (First_Global (Subp, Global_Mode, Refined => True), Kind); + end Return_Globals_Of_Mode; + + -- Start of processing for Return_Globals + + begin + Return_Globals_Of_Mode (Name_Proof_In); + Return_Globals_Of_Mode (Name_Input); + Return_Globals_Of_Mode (Name_Output); + Return_Globals_Of_Mode (Name_In_Out); + end Return_Globals; + + -------------------------------- + -- Return_Parameter_Or_Global -- + -------------------------------- + + procedure Return_Parameter_Or_Global + (Id : Entity_Id; + Mode : Formal_Kind; + Subp : Entity_Id) + is + Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id); + pragma Assert (Elem /= null); + + begin + -- Shallow unaliased parameters and globals cannot introduce pointer + -- aliasing. + + if not Has_Alias (Id) and then Is_Shallow (Etype (Id)) then + null; + + -- Observed IN parameters and globals need not return a permission to + -- the caller. + + elsif Mode = E_In_Parameter and then not Is_Borrowed_In (Id) then + null; + + -- All other parameters and globals should return with mode RW to the + -- caller. + + else + if Permission (Elem) /= Read_Write then + Perm_Error_Subprogram_End + (E => Id, + Subp => Subp, + Perm => Read_Write, + Found_Perm => Permission (Elem)); + end if; + end if; + end Return_Parameter_Or_Global; + + ----------------------- + -- Return_Parameters -- + ----------------------- + + procedure Return_Parameters (Subp : Entity_Id) is + Formal : Entity_Id; + + begin + Formal := First_Formal (Subp); + while Present (Formal) loop + Return_Parameter_Or_Global (Formal, Ekind (Formal), Subp); + Next_Formal (Formal); + end loop; + end Return_Parameters; + + ------------------------- + -- Set_Perm_Extensions -- + ------------------------- + + procedure Set_Perm_Extensions + (T : Perm_Tree_Access; + P : Perm_Kind) + is + procedure Free_Perm_Tree_Children (T : Perm_Tree_Access); + + procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) + is + begin + case Kind (T) is + when Entire_Object => + null; + + when Reference => + Free_Perm_Tree (T.all.Tree.Get_All); + + when Array_Component => + Free_Perm_Tree (T.all.Tree.Get_Elem); + + -- Free every Component subtree + + when Record_Component => + declare + Comp : Perm_Tree_Access; + + begin + Comp := Perm_Tree_Maps.Get_First (Component (T)); + while Comp /= null loop + Free_Perm_Tree (Comp); + Comp := Perm_Tree_Maps.Get_Next (Component (T)); + end loop; + + Free_Perm_Tree (T.all.Tree.Other_Components); + end; + end case; + end Free_Perm_Tree_Children; + + Son : constant Perm_Tree := + Perm_Tree' + (Kind => Entire_Object, + Is_Node_Deep => Is_Node_Deep (T), + Permission => Permission (T), + Children_Permission => P); + + begin + Free_Perm_Tree_Children (T); + T.all.Tree := Son; + end Set_Perm_Extensions; + + ------------------------------ + -- Set_Perm_Extensions_Move -- + ------------------------------ + + procedure Set_Perm_Extensions_Move + (T : Perm_Tree_Access; + E : Entity_Id) + is + begin + if not Is_Node_Deep (T) then + -- We are a shallow extension with same number of .all + + Set_Perm_Extensions (T, Read_Write); + return; + end if; + + -- We are a deep extension here (or the moved deep path) + + T.all.Tree.Permission := Write_Only; + + case T.all.Tree.Kind is + -- Unroll the tree depending on the type + + when Entire_Object => + case Ekind (E) is + when Scalar_Kind + | E_String_Literal_Subtype + => + Set_Perm_Extensions (T, No_Access); + + -- No need to unroll here, directly put sons to No_Access + + when Access_Kind => + if Ekind (E) in Access_Subprogram_Kind then + null; + else + Set_Perm_Extensions (T, No_Access); + end if; + + -- No unrolling done, too complicated + + when E_Class_Wide_Subtype + | E_Class_Wide_Type + | E_Incomplete_Type + | E_Incomplete_Subtype + | E_Exception_Type + | E_Task_Type + | E_Task_Subtype + => + Set_Perm_Extensions (T, No_Access); + + -- Expand the tree. Replace the node with Array component. + + when E_Array_Type + | E_Array_Subtype => + declare + Son : Perm_Tree_Access; + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Node_Deep (T), + Permission => Read_Write, + Children_Permission => Read_Write)); + + Set_Perm_Extensions_Move (Son, Component_Type (E)); + + -- We change the current node from Entire_Object to + -- Reference with Write_Only and the previous son. + + pragma Assert (Is_Node_Deep (T)); + + T.all.Tree := (Kind => Array_Component, + Is_Node_Deep => Is_Node_Deep (T), + Permission => Write_Only, + Get_Elem => Son); + end; + + -- Unroll, and set permission extensions with component type + + when E_Record_Type + | E_Record_Subtype + | E_Record_Type_With_Private + | E_Record_Subtype_With_Private + | E_Protected_Type + | E_Protected_Subtype + => + declare + -- Expand the tree. Replace the node with + -- Record_Component. + + Elem : Node_Id; + + Son : Perm_Tree_Access; + + begin + -- We change the current node from Entire_Object to + -- Record_Component with same permission and an empty + -- hash table as component list. + + pragma Assert (Is_Node_Deep (T)); + + T.all.Tree := + (Kind => Record_Component, + Is_Node_Deep => Is_Node_Deep (T), + Permission => Write_Only, + Component => Perm_Tree_Maps.Nil, + Other_Components => + new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => True, + Permission => Read_Write, + Children_Permission => Read_Write) + ) + ); + + -- We fill the hash table with all sons of the record, + -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant (E); + while Present (Elem) loop + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (Elem)), + Permission => Read_Write, + Children_Permission => Read_Write)); + + Set_Perm_Extensions_Move (Son, Etype (Elem)); + + Perm_Tree_Maps.Set + (T.all.Tree.Component, Elem, Son); + + Next_Component_Or_Discriminant (Elem); + end loop; + end; + + when E_Private_Type + | E_Private_Subtype + | E_Limited_Private_Type + | E_Limited_Private_Subtype + => + Set_Perm_Extensions_Move (T, Underlying_Type (E)); + + when others => + raise Program_Error; + end case; + + when Reference => + -- Now the son does not have the same number of .all + Set_Perm_Extensions (T, No_Access); + + when Array_Component => + Set_Perm_Extensions_Move (Get_Elem (T), Component_Type (E)); + + when Record_Component => + declare + Comp : Perm_Tree_Access; + It : Node_Id; + + begin + It := First_Component_Or_Discriminant (E); + while It /= Empty loop + Comp := Perm_Tree_Maps.Get (Component (T), It); + pragma Assert (Comp /= null); + Set_Perm_Extensions_Move (Comp, It); + It := Next_Component_Or_Discriminant (E); + end loop; + + Set_Perm_Extensions (Other_Components (T), No_Access); + end; + end case; + end Set_Perm_Extensions_Move; + + ------------------------------ + -- Set_Perm_Prefixes_Assign -- + ------------------------------ + + function Set_Perm_Prefixes_Assign + (N : Node_Id) + return Perm_Tree_Access + is + C : constant Perm_Tree_Access := Get_Perm_Tree (N); + + begin + pragma Assert (Current_Checking_Mode = Assign); + + -- The function should not be called if has_function_component + + pragma Assert (C /= null); + + case Kind (C) is + when Entire_Object => + pragma Assert (Children_Permission (C) = Read_Write); + C.all.Tree.Permission := Read_Write; + + when Reference => + pragma Assert (Get_All (C) /= null); + + C.all.Tree.Permission := + Lub (Permission (C), Permission (Get_All (C))); + + when Array_Component => + pragma Assert (C.all.Tree.Get_Elem /= null); + + -- Given that it is not possible to know which element has been + -- assigned, then the permissions do not get changed in case of + -- Array_Component. + + null; + + when Record_Component => + declare + Perm : Perm_Kind := Read_Write; + + Comp : Perm_Tree_Access; + + begin + -- We take the Glb of all the descendants, and then update the + -- permission of the node with it. + Comp := Perm_Tree_Maps.Get_First (Component (C)); + while Comp /= null loop + Perm := Glb (Perm, Permission (Comp)); + Comp := Perm_Tree_Maps.Get_Next (Component (C)); + end loop; + + Perm := Glb (Perm, Permission (Other_Components (C))); + + C.all.Tree.Permission := Lub (Permission (C), Perm); + end; + end case; + + case Nkind (N) is + -- Base identifier. End recursion here. + + when N_Identifier + | N_Expanded_Name + | N_Defining_Identifier + => + return null; + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Set_Perm_Prefixes_Assign (Expression (N)); + + when N_Parameter_Specification => + raise Program_Error; + + -- Continue recursion on prefix + + when N_Selected_Component => + return Set_Perm_Prefixes_Assign (Prefix (N)); + + -- Continue recursion on prefix + + when N_Indexed_Component + | N_Slice + => + return Set_Perm_Prefixes_Assign (Prefix (N)); + + -- Continue recursion on prefix + + when N_Explicit_Dereference => + return Set_Perm_Prefixes_Assign (Prefix (N)); + + when N_Function_Call => + raise Program_Error; + + when others => + raise Program_Error; + + end case; + end Set_Perm_Prefixes_Assign; + + ---------------------------------- + -- Set_Perm_Prefixes_Borrow_Out -- + ---------------------------------- + + function Set_Perm_Prefixes_Borrow_Out + (N : Node_Id) + return Perm_Tree_Access + is + begin + pragma Assert (Current_Checking_Mode = Borrow_Out); + + case Nkind (N) is + -- Base identifier. Set permission to No. + + when N_Identifier + | N_Expanded_Name + => + declare + P : constant Node_Id := Entity (N); + + C : constant Perm_Tree_Access := + Get (Current_Perm_Env, Unique_Entity (P)); + + pragma Assert (C /= null); + + begin + -- Setting the initialization map to True, so that this + -- variable cannot be ignored anymore when looking at end + -- of elaboration of package. + + Set (Current_Initialization_Map, Unique_Entity (P), True); + + C.all.Tree.Permission := No_Access; + return C; + end; + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Set_Perm_Prefixes_Borrow_Out (Expression (N)); + + when N_Parameter_Specification + | N_Defining_Identifier + => + raise Program_Error; + + -- We set the permission tree of its prefix, and then we extract + -- our subtree from the returned pointer and assign an adequate + -- permission to it, if unfolded. If folded, we unroll the tree + -- in one step. + + when N_Selected_Component => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes_Borrow_Out (Prefix (N)); + + begin + if C = null then + -- We went through a function call, do nothing + + return null; + end if; + + -- The permission of the returned node should be No + + pragma Assert (Permission (C) = No_Access); + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Record_Component); + + if Kind (C) = Record_Component then + -- The tree is unfolded. We just modify the permission and + -- return the record subtree. + + declare + Selected_Component : constant Entity_Id := + Entity (Selector_Name (N)); + + Selected_C : Perm_Tree_Access := + Perm_Tree_Maps.Get + (Component (C), Selected_Component); + + begin + if Selected_C = null then + Selected_C := Other_Components (C); + end if; + + pragma Assert (Selected_C /= null); + + Selected_C.all.Tree.Permission := No_Access; + + return Selected_C; + end; + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace the node with + -- Record_Component. + + Elem : Node_Id; + + -- Create an empty hash table + + Hashtbl : Perm_Tree_Maps.Instance; + + -- We create the unrolled nodes, that will all have same + -- permission than parent. + + Son : Perm_Tree_Access; + + ChildrenPerm : constant Perm_Kind := + Children_Permission (C); + + begin + -- We change the current node from Entire_Object to + -- Record_Component with same permission and an empty + -- hash table as component list. + + C.all.Tree := + (Kind => Record_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Permission (C), + Component => Hashtbl, + Other_Components => + new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => True, + Permission => ChildrenPerm, + Children_Permission => ChildrenPerm) + )); + + -- We fill the hash table with all sons of the record, + -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant + (Etype (Prefix (N))); + + while Present (Elem) loop + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (Elem)), + Permission => ChildrenPerm, + Children_Permission => ChildrenPerm)); + + Perm_Tree_Maps.Set + (C.all.Tree.Component, Elem, Son); + + Next_Component_Or_Discriminant (Elem); + end loop; + + -- Now we set the right field to No_Access, and then we + -- return the tree to the sons, so that the recursion can + -- continue. + + declare + Selected_Component : constant Entity_Id := + Entity (Selector_Name (N)); + + Selected_C : Perm_Tree_Access := + Perm_Tree_Maps.Get + (Component (C), Selected_Component); + + begin + if Selected_C = null then + Selected_C := Other_Components (C); + end if; + + pragma Assert (Selected_C /= null); + + Selected_C.all.Tree.Permission := No_Access; + + return Selected_C; + end; + end; + else + raise Program_Error; + end if; + end; + + -- We set the permission tree of its prefix, and then we extract + -- from the returned pointer the subtree and assign an adequate + -- permission to it, if unfolded. If folded, we unroll the tree in + -- one step. + + when N_Indexed_Component + | N_Slice + => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes_Borrow_Out (Prefix (N)); + + begin + if C = null then + -- We went through a function call, do nothing + + return null; + end if; + + -- The permission of the returned node should be either W + -- (because the recursive call sets <= Write_Only) or No + -- (if another path has been moved with 'Access). + + pragma Assert (Permission (C) = No_Access); + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Array_Component); + + if Kind (C) = Array_Component then + -- The tree is unfolded. We just modify the permission and + -- return the elem subtree. + + pragma Assert (Get_Elem (C) /= null); + + C.all.Tree.Get_Elem.all.Tree.Permission := No_Access; + + return Get_Elem (C); + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace node with Array_Component. + + Son : Perm_Tree_Access; + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Node_Deep (C), + Permission => No_Access, + Children_Permission => Children_Permission (C))); + + -- We change the current node from Entire_Object + -- to Array_Component with same permission and the + -- previously defined son. + + C.all.Tree := (Kind => Array_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => No_Access, + Get_Elem => Son); + + return Get_Elem (C); + end; + else + raise Program_Error; + end if; + end; + + -- We set the permission tree of its prefix, and then we extract + -- from the returned pointer the subtree and assign an adequate + -- permission to it, if unfolded. If folded, we unroll the tree + -- at one step. + + when N_Explicit_Dereference => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes_Borrow_Out (Prefix (N)); + + begin + if C = null then + -- We went through a function call. Do nothing. + + return null; + end if; + + -- The permission of the returned node should be No + + pragma Assert (Permission (C) = No_Access); + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Reference); + + if Kind (C) = Reference then + -- The tree is unfolded. We just modify the permission and + -- return the elem subtree. + + pragma Assert (Get_All (C) /= null); + + C.all.Tree.Get_All.all.Tree.Permission := No_Access; + + return Get_All (C); + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace the node with Reference. + + Son : Perm_Tree_Access; + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (N)), + Permission => No_Access, + Children_Permission => Children_Permission (C))); + + -- We change the current node from Entire_Object to + -- Reference with No_Access and the previous son. + + pragma Assert (Is_Node_Deep (C)); + + C.all.Tree := (Kind => Reference, + Is_Node_Deep => Is_Node_Deep (C), + Permission => No_Access, + Get_All => Son); + + return Get_All (C); + end; + else + raise Program_Error; + end if; + end; + + when N_Function_Call => + return null; + + when others => + raise Program_Error; + end case; + end Set_Perm_Prefixes_Borrow_Out; + + ---------------------------- + -- Set_Perm_Prefixes_Move -- + ---------------------------- + + function Set_Perm_Prefixes_Move + (N : Node_Id; Mode : Checking_Mode) + return Perm_Tree_Access + is + begin + case Nkind (N) is + -- Base identifier. Set permission to W or No depending on Mode. + + when N_Identifier + | N_Expanded_Name + => + declare + P : constant Node_Id := Entity (N); + + C : constant Perm_Tree_Access := + Get (Current_Perm_Env, Unique_Entity (P)); + + begin + -- The base tree can be RW (first move from this base path) or + -- W (already some extensions values moved), or even No_Access + -- (extensions moved with 'Access). But it cannot be Read_Only + -- (we get an error). + + if Permission (C) = Read_Only then + raise Unrecoverable_Error; + end if; + + -- Setting the initialization map to True, so that this + -- variable cannot be ignored anymore when looking at end + -- of elaboration of package. + + Set (Current_Initialization_Map, Unique_Entity (P), True); + + if C = null then + -- No null possible here, there are no parents for the path. + -- This means we are using a global variable without adding + -- it in environment with a global aspect. + + Illegal_Global_Usage (N); + end if; + + if Mode = Super_Move then + C.all.Tree.Permission := No_Access; + else + C.all.Tree.Permission := Glb (Write_Only, Permission (C)); + end if; + + return C; + end; + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Set_Perm_Prefixes_Move (Expression (N), Mode); + + when N_Parameter_Specification + | N_Defining_Identifier + => + raise Program_Error; + + -- We set the permission tree of its prefix, and then we extract + -- from the returned pointer our subtree and assign an adequate + -- permission to it, if unfolded. If folded, we unroll the tree + -- at one step. + + when N_Selected_Component => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes_Move (Prefix (N), Mode); + + begin + if C = null then + -- We went through a function call, do nothing + + return null; + end if; + + -- The permission of the returned node should be either W + -- (because the recursive call sets <= Write_Only) or No + -- (if another path has been moved with 'Access). + + pragma Assert (Permission (C) = No_Access + or else Permission (C) = Write_Only); + + if Mode = Super_Move then + -- The permission of the returned node should be No (thanks + -- to the recursion). + + pragma Assert (Permission (C) = No_Access); + null; + end if; + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Record_Component); + + if Kind (C) = Record_Component then + -- The tree is unfolded. We just modify the permission and + -- return the record subtree. + + declare + Selected_Component : constant Entity_Id := + Entity (Selector_Name (N)); + + Selected_C : Perm_Tree_Access := + Perm_Tree_Maps.Get + (Component (C), Selected_Component); + + begin + if Selected_C = null then + -- If the hash table returns no element, then we fall + -- into the part of Other_Components. + pragma Assert (Is_Tagged_Type (Etype (Prefix (N)))); + + Selected_C := Other_Components (C); + end if; + + pragma Assert (Selected_C /= null); + + -- The Selected_C can have permissions: + -- RW : first move in this path + -- W : Already other moves in this path + -- No : Already other moves with 'Access + + pragma Assert (Permission (Selected_C) /= Read_Only); + if Mode = Super_Move then + Selected_C.all.Tree.Permission := No_Access; + else + Selected_C.all.Tree.Permission := + Glb (Write_Only, Permission (Selected_C)); + + end if; + + return Selected_C; + end; + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace the node with + -- Record_Component. + + Elem : Node_Id; + + -- Create an empty hash table + + Hashtbl : Perm_Tree_Maps.Instance; + + -- We are in Move or Super_Move mode, hence we can assume + -- that the Children_permission is RW, given that there + -- are no other paths that could have been moved. + + pragma Assert (Children_Permission (C) = Read_Write); + + -- We create the unrolled nodes, that will all have RW + -- permission given that we are in move mode. We will + -- then set the right node to W. + + Son : Perm_Tree_Access; + + begin + -- We change the current node from Entire_Object to + -- Record_Component with same permission and an empty + -- hash table as component list. + + C.all.Tree := + (Kind => Record_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Permission (C), + Component => Hashtbl, + Other_Components => + new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => True, + Permission => Read_Write, + Children_Permission => Read_Write) + )); + + -- We fill the hash table with all sons of the record, + -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant + (Etype (Prefix (N))); + + while Present (Elem) loop + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (Elem)), + Permission => Read_Write, + Children_Permission => Read_Write)); + + Perm_Tree_Maps.Set + (C.all.Tree.Component, Elem, Son); + + Next_Component_Or_Discriminant (Elem); + end loop; + + -- Now we set the right field to Write_Only or No_Access + -- depending on mode, and then we return the tree to the + -- sons, so that the recursion can continue. + + declare + Selected_Component : constant Entity_Id := + Entity (Selector_Name (N)); + + Selected_C : Perm_Tree_Access := + Perm_Tree_Maps.Get + (Component (C), Selected_Component); + + begin + if Selected_C = null then + Selected_C := Other_Components (C); + end if; + + pragma Assert (Selected_C /= null); + + -- Given that this is a newly created Select_C, we can + -- safely assume that its permission is Read_Write. + + pragma Assert (Permission (Selected_C) = + Read_Write); + + if Mode = Super_Move then + Selected_C.all.Tree.Permission := No_Access; + else + Selected_C.all.Tree.Permission := Write_Only; + end if; + + return Selected_C; + end; + end; + else + raise Program_Error; + end if; + end; + + -- We set the permission tree of its prefix, and then we extract + -- from the returned pointer the subtree and assign an adequate + -- permission to it, if unfolded. If folded, we unroll the tree + -- at one step. + + when N_Indexed_Component + | N_Slice + => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes_Move (Prefix (N), Mode); + + begin + if C = null then + -- We went through a function call, do nothing + + return null; + end if; + + -- The permission of the returned node should be either + -- W (because the recursive call sets <= Write_Only) + -- or No (if another path has been moved with 'Access) + + if Mode = Super_Move then + pragma Assert (Permission (C) = No_Access); + null; + else + pragma Assert (Permission (C) = Write_Only + or else Permission (C) = No_Access); + null; + end if; + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Array_Component); + + if Kind (C) = Array_Component then + -- The tree is unfolded. We just modify the permission and + -- return the elem subtree. + + if Get_Elem (C) = null then + -- Hash_Table_Error + raise Program_Error; + end if; + + -- The Get_Elem can have permissions : + -- RW : first move in this path + -- W : Already other moves in this path + -- No : Already other moves with 'Access + + pragma Assert (Permission (Get_Elem (C)) /= Read_Only); + + if Mode = Super_Move then + C.all.Tree.Get_Elem.all.Tree.Permission := No_Access; + else + C.all.Tree.Get_Elem.all.Tree.Permission := + Glb (Write_Only, Permission (Get_Elem (C))); + end if; + + return Get_Elem (C); + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace node with Array_Component. + + -- We are in move mode, hence we can assume that the + -- Children_permission is RW. + + pragma Assert (Children_Permission (C) = Read_Write); + + Son : Perm_Tree_Access; + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Read_Write, + Children_Permission => Read_Write)); + + if Mode = Super_Move then + Son.all.Tree.Permission := No_Access; + else + Son.all.Tree.Permission := Write_Only; + end if; + + -- We change the current node from Entire_Object + -- to Array_Component with same permission and the + -- previously defined son. + + C.all.Tree := (Kind => Array_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Permission (C), + Get_Elem => Son); + + return Get_Elem (C); + end; + else + raise Program_Error; + end if; + end; + + -- We set the permission tree of its prefix, and then we extract + -- from the returned pointer the subtree and assign an adequate + -- permission to it, if unfolded. If folded, we unroll the tree + -- at one step. + + when N_Explicit_Dereference => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes_Move (Prefix (N), Move); + + begin + if C = null then + -- We went through a function call: do nothing + + return null; + end if; + + -- The permission of the returned node should be only + -- W (because the recursive call sets <= Write_Only) + -- No is NOT POSSIBLE here + + pragma Assert (Permission (C) = Write_Only); + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Reference); + + if Kind (C) = Reference then + -- The tree is unfolded. We just modify the permission and + -- return the elem subtree. + + if Get_All (C) = null then + -- Hash_Table_Error + raise Program_Error; + end if; + + -- The Get_All can have permissions : + -- RW : first move in this path + -- W : Already other moves in this path + -- No : Already other moves with 'Access + + pragma Assert (Permission (Get_All (C)) /= Read_Only); + + if Mode = Super_Move then + C.all.Tree.Get_All.all.Tree.Permission := No_Access; + else + Get_All (C).all.Tree.Permission := + Glb (Write_Only, Permission (Get_All (C))); + end if; + return Get_All (C); + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace the node with Reference. + + -- We are in Move or Super_Move mode, hence we can assume + -- that the Children_permission is RW. + + pragma Assert (Children_Permission (C) = Read_Write); + + Son : Perm_Tree_Access; + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (N)), + Permission => Read_Write, + Children_Permission => Read_Write)); + + if Mode = Super_Move then + Son.all.Tree.Permission := No_Access; + else + Son.all.Tree.Permission := Write_Only; + end if; + + -- We change the current node from Entire_Object to + -- Reference with Write_Only and the previous son. + + pragma Assert (Is_Node_Deep (C)); + + C.all.Tree := (Kind => Reference, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Write_Only, + -- Write_only is equal to C.Permission + Get_All => Son); + + return Get_All (C); + end; + else + raise Program_Error; + end if; + end; + + when N_Function_Call => + return null; + + when others => + raise Program_Error; + end case; + + end Set_Perm_Prefixes_Move; + + ------------------------------- + -- Set_Perm_Prefixes_Observe -- + ------------------------------- + + function Set_Perm_Prefixes_Observe + (N : Node_Id) + return Perm_Tree_Access + is + begin + pragma Assert (Current_Checking_Mode = Observe); + + case Nkind (N) is + -- Base identifier. Set permission to R. + + when N_Identifier + | N_Expanded_Name + | N_Defining_Identifier + => + declare + P : Node_Id; + C : Perm_Tree_Access; + + begin + if Nkind (N) = N_Defining_Identifier then + P := N; + else + P := Entity (N); + end if; + + C := Get (Current_Perm_Env, Unique_Entity (P)); + -- Setting the initialization map to True, so that this + -- variable cannot be ignored anymore when looking at end + -- of elaboration of package. + + Set (Current_Initialization_Map, Unique_Entity (P), True); + + if C = null then + -- No null possible here, there are no parents for the path. + -- This means we are using a global variable without adding + -- it in environment with a global aspect. + + Illegal_Global_Usage (N); + end if; + + C.all.Tree.Permission := Glb (Read_Only, Permission (C)); + + return C; + end; + + when N_Type_Conversion + | N_Unchecked_Type_Conversion + | N_Qualified_Expression + => + return Set_Perm_Prefixes_Observe (Expression (N)); + + when N_Parameter_Specification => + raise Program_Error; + + -- We set the permission tree of its prefix, and then we extract + -- from the returned pointer our subtree and assign an adequate + -- permission to it, if unfolded. If folded, we unroll the tree + -- at one step. + + when N_Selected_Component => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes_Observe (Prefix (N)); + + begin + if C = null then + -- We went through a function call, do nothing + + return null; + end if; + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Record_Component); + + if Kind (C) = Record_Component then + -- The tree is unfolded. We just modify the permission and + -- return the record subtree. We put the permission to the + -- glb of read_only and its current permission, to consider + -- the case of observing x.y while x.z has been moved. Then + -- x should be No_Access. + + declare + Selected_Component : constant Entity_Id := + Entity (Selector_Name (N)); + + Selected_C : Perm_Tree_Access := + Perm_Tree_Maps.Get + (Component (C), Selected_Component); + + begin + if Selected_C = null then + Selected_C := Other_Components (C); + end if; + + pragma Assert (Selected_C /= null); + + Selected_C.all.Tree.Permission := + Glb (Read_Only, Permission (Selected_C)); + + return Selected_C; + end; + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace the node with + -- Record_Component. + + Elem : Node_Id; + + -- Create an empty hash table + + Hashtbl : Perm_Tree_Maps.Instance; + + -- We create the unrolled nodes, that will all have RW + -- permission given that we are in move mode. We will + -- then set the right node to W. + + Son : Perm_Tree_Access; + + Child_Perm : constant Perm_Kind := + Children_Permission (C); + + begin + -- We change the current node from Entire_Object to + -- Record_Component with same permission and an empty + -- hash table as component list. + + C.all.Tree := + (Kind => Record_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Permission (C), + Component => Hashtbl, + Other_Components => + new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => True, + Permission => Child_Perm, + Children_Permission => Child_Perm) + )); + + -- We fill the hash table with all sons of the record, + -- with basic Entire_Objects nodes. + Elem := First_Component_Or_Discriminant + (Etype (Prefix (N))); + + while Present (Elem) loop + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (Elem)), + Permission => Child_Perm, + Children_Permission => Child_Perm)); + + Perm_Tree_Maps.Set + (C.all.Tree.Component, Elem, Son); + + Next_Component_Or_Discriminant (Elem); + end loop; + + -- Now we set the right field to Read_Only. and then we + -- return the tree to the sons, so that the recursion can + -- continue. + + declare + Selected_Component : constant Entity_Id := + Entity (Selector_Name (N)); + + Selected_C : Perm_Tree_Access := + Perm_Tree_Maps.Get + (Component (C), Selected_Component); + + begin + if Selected_C = null then + Selected_C := Other_Components (C); + end if; + + pragma Assert (Selected_C /= null); + + Selected_C.all.Tree.Permission := + Glb (Read_Only, Child_Perm); + + return Selected_C; + end; + end; + else + raise Program_Error; + end if; + end; + + -- We set the permission tree of its prefix, and then we extract from + -- the returned pointer the subtree and assign an adequate permission + -- to it, if unfolded. If folded, we unroll the tree at one step. + + when N_Indexed_Component + | N_Slice + => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes_Observe (Prefix (N)); + + begin + if C = null then + -- We went through a function call, do nothing + + return null; + end if; + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Array_Component); + + if Kind (C) = Array_Component then + -- The tree is unfolded. We just modify the permission and + -- return the elem subtree. + + pragma Assert (Get_Elem (C) /= null); + + C.all.Tree.Get_Elem.all.Tree.Permission := + Glb (Read_Only, Permission (Get_Elem (C))); + + return Get_Elem (C); + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace node with Array_Component. + + Son : Perm_Tree_Access; + + Child_Perm : constant Perm_Kind := + Glb (Read_Only, Children_Permission (C)); + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Child_Perm, + Children_Permission => Child_Perm)); + + -- We change the current node from Entire_Object + -- to Array_Component with same permission and the + -- previously defined son. + + C.all.Tree := (Kind => Array_Component, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Child_Perm, + Get_Elem => Son); + + return Get_Elem (C); + end; + + else + raise Program_Error; + end if; + end; + + -- We set the permission tree of its prefix, and then we extract from + -- the returned pointer the subtree and assign an adequate permission + -- to it, if unfolded. If folded, we unroll the tree at one step. + + when N_Explicit_Dereference => + declare + C : constant Perm_Tree_Access := + Set_Perm_Prefixes_Observe (Prefix (N)); + + begin + if C = null then + -- We went through a function call, do nothing + + return null; + end if; + + pragma Assert (Kind (C) = Entire_Object + or else Kind (C) = Reference); + + if Kind (C) = Reference then + -- The tree is unfolded. We just modify the permission and + -- return the elem subtree. + + pragma Assert (Get_All (C) /= null); + + C.all.Tree.Get_All.all.Tree.Permission := + Glb (Read_Only, Permission (Get_All (C))); + + return Get_All (C); + elsif Kind (C) = Entire_Object then + declare + -- Expand the tree. Replace the node with Reference. + + Son : Perm_Tree_Access; + + Child_Perm : constant Perm_Kind := + Glb (Read_Only, Children_Permission (C)); + + begin + Son := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (N)), + Permission => Child_Perm, + Children_Permission => Child_Perm)); + + -- We change the current node from Entire_Object to + -- Reference with Write_Only and the previous son. + + pragma Assert (Is_Node_Deep (C)); + + C.all.Tree := (Kind => Reference, + Is_Node_Deep => Is_Node_Deep (C), + Permission => Child_Perm, + Get_All => Son); + + return Get_All (C); + end; + else + raise Program_Error; + end if; + end; + + when N_Function_Call => + return null; + + when others => + raise Program_Error; + + end case; + end Set_Perm_Prefixes_Observe; + + ------------------- + -- Setup_Globals -- + ------------------- + + procedure Setup_Globals (Subp : Entity_Id) is + + procedure Setup_Globals_From_List + (First_Item : Node_Id; + Kind : Formal_Kind); + -- Set up global items from the list starting at Item + + procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id); + -- Set up global items for the mode Global_Mode + + ----------------------------- + -- Setup_Globals_From_List -- + ----------------------------- + + procedure Setup_Globals_From_List + (First_Item : Node_Id; + Kind : Formal_Kind) + is + Item : Node_Id := First_Item; + E : Entity_Id; + + begin + while Present (Item) loop + E := Entity (Item); + + -- Ignore abstract states, which play no role in pointer aliasing + + if Ekind (E) = E_Abstract_State then + null; + else + Setup_Parameter_Or_Global (E, Kind); + end if; + Next_Global (Item); + end loop; + end Setup_Globals_From_List; + + --------------------------- + -- Setup_Globals_Of_Mode -- + --------------------------- + + procedure Setup_Globals_Of_Mode (Global_Mode : Name_Id) is + Kind : Formal_Kind; + + begin + case Global_Mode is + when Name_Input | Name_Proof_In => + Kind := E_In_Parameter; + when Name_Output => + Kind := E_Out_Parameter; + when Name_In_Out => + Kind := E_In_Out_Parameter; + when others => + raise Program_Error; + end case; + + -- Set up both global items from Global and Refined_Global pragmas + + Setup_Globals_From_List (First_Global (Subp, Global_Mode), Kind); + Setup_Globals_From_List + (First_Global (Subp, Global_Mode, Refined => True), Kind); + end Setup_Globals_Of_Mode; + + -- Start of processing for Setup_Globals + + begin + Setup_Globals_Of_Mode (Name_Proof_In); + Setup_Globals_Of_Mode (Name_Input); + Setup_Globals_Of_Mode (Name_Output); + Setup_Globals_Of_Mode (Name_In_Out); + end Setup_Globals; + + ------------------------------- + -- Setup_Parameter_Or_Global -- + ------------------------------- + + procedure Setup_Parameter_Or_Global + (Id : Entity_Id; + Mode : Formal_Kind) + is + Elem : Perm_Tree_Access; + + begin + Elem := new Perm_Tree_Wrapper' + (Tree => + (Kind => Entire_Object, + Is_Node_Deep => Is_Deep (Etype (Id)), + Permission => Read_Write, + Children_Permission => Read_Write)); + + case Mode is + when E_In_Parameter => + + -- Borrowed IN: RW for everybody + + if Is_Borrowed_In (Id) then + Elem.all.Tree.Permission := Read_Write; + Elem.all.Tree.Children_Permission := Read_Write; + + -- Observed IN: R for everybody + + else + Elem.all.Tree.Permission := Read_Only; + Elem.all.Tree.Children_Permission := Read_Only; + end if; + + -- OUT: borrow, but callee has W only + + when E_Out_Parameter => + Elem.all.Tree.Permission := Write_Only; + Elem.all.Tree.Children_Permission := Write_Only; + + -- IN OUT: borrow and callee has RW + + when E_In_Out_Parameter => + Elem.all.Tree.Permission := Read_Write; + Elem.all.Tree.Children_Permission := Read_Write; + end case; + + Set (Current_Perm_Env, Id, Elem); + end Setup_Parameter_Or_Global; + + ---------------------- + -- Setup_Parameters -- + ---------------------- + + procedure Setup_Parameters (Subp : Entity_Id) is + Formal : Entity_Id; + + begin + Formal := First_Formal (Subp); + while Present (Formal) loop + Setup_Parameter_Or_Global (Formal, Ekind (Formal)); + Next_Formal (Formal); + end loop; + end Setup_Parameters; + +end Sem_SPARK; diff --git a/gcc/ada/sem_spark.ads b/gcc/ada/sem_spark.ads new file mode 100644 index 00000000000..d7abd8ad74a --- /dev/null +++ b/gcc/ada/sem_spark.ads @@ -0,0 +1,143 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S E M _ S P A R K -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2017, 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. See the GNU General Public License -- +-- for more details. You should have received a copy of the GNU General -- +-- Public License distributed with GNAT; see file COPYING3. If not, go to -- +-- http://www.gnu.org/licenses for a complete copy of the license. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package implements an anti-aliasing analysis for access types. The +-- rules that are enforced are defined in the anti-aliasing section of the +-- SPARK RM 6.4.2 +-- +-- Analyze_SPARK is called by Gnat1drv, when GNATprove mode is activated. It +-- does an analysis of the source code, looking for code that is considered +-- as SPARK and launches another function called Analyze_Node that will do +-- the whole analysis. +-- +-- A path is an abstraction of a name, of which all indices, slices (for +-- indexed components) and function calls have been abstracted and all +-- dereferences are made explicit. A path is the atomic element viewed by the +-- analysis, with the notion of prefixes and extensions of different paths. +-- +-- The analysis explores the AST, and looks for different constructs +-- that may involve aliasing. These main constructs are assignments +-- (N_Assignment_Statement, N_Object_Declaration, ...), or calls +-- (N_Procedure_Call_Statement, N_Entry_Call_Statement, N_Function_Call). +-- The analysis checks the permissions of each construct and updates them +-- according to the SPARK RM. This can follow three main different types +-- of operations: move, borrow, and observe. + +---------------------------- +-- Deep and shallow types -- +---------------------------- + +-- The analysis focuses on objects that can cause problems in terms of pointer +-- aliasing. These objects have types that are called deep. Deep types are +-- defined as being either types with an access part or class-wide types +-- (which may have an access part in a derived type). Non-deep types are +-- called shallow. Some objects of shallow type may cause pointer aliasing +-- problems when they are explicitely marked as aliased (and then the aliasing +-- occurs when we take the Access to this object and store it in a pointer). + +---------- +-- Move -- +---------- + +-- Moves can happen at several points in the program: during assignment (and +-- any similar statement such as object declaration with initial value), or +-- during return statements. +-- +-- The underlying concept consists of transferring the ownership of any path +-- on the right-hand side to the left-hand side. There are some details that +-- should be taken into account so as not to transfer paths that appear only +-- as intermediate results of a more complex expression. + +-- More specifically, the SPARK RM defines moved expressions, and any moved +-- expression that points directly to a path is then checked and sees its +-- permissions updated accordingly. + +------------ +-- Borrow -- +------------ + +-- Borrows can happen in subprogram calls. They consist of a temporary +-- transfer of ownership from a caller to a callee. Expressions that can be +-- borrowed can be found in either procedure or entry actual parameters, and +-- consist of parameters of mode either "out" or "in out", or parameters of +-- mode "in" that are of type nonconstant access-to-variable. We consider +-- global variables as implicit parameters to subprograms, with their mode +-- given by the Global contract associated to the subprogram. Note that the +-- analysis looks for such a Global contract mentioning any global variable +-- of deep type accessed directly in the subprogram, and it raises an error if +-- there is no Global contract, or if the Global contract does not mention the +-- variable. +-- +-- A borrow of a parameter X is equivalent in terms of aliasing to moving +-- X'Access to the callee, and then assigning back X at the end of the call. +-- +-- Borrowed parameters should have read-write permission (or write-only for +-- "out" parameters), and should all have read-write permission at the end +-- of the call (this guarantee is ensured by the callee). + +------------- +-- Observe -- +------------- + +-- Observed parameters are all the other parameters that are not borrowed and +-- that may cause problems with aliasing. They are considered as being sent to +-- the callee with Read-Only permission, so that they can be aliased safely. +-- This is the only construct that allows aliasing that does not prevent +-- accessing the old path that is being aliased. However, this comes with +-- the restriction that those aliased path cannot be written in the callee. + +-------------------- +-- Implementation -- +-------------------- + +-- The implementation is based on trees that represent the possible paths +-- in the source code. Those trees can be unbounded in depth, hence they are +-- represented using lazy data structures, whose laziness is handled manually. +-- Each time an identifier is declared, its path is added to the permission +-- environment as a tree with only one node, the declared identifier. Each +-- time a path is checked or updated, we look in the tree at the adequate +-- node, unfolding the tree whenever needed. + +-- For this, each node has several variables that indicate whether it is +-- deep (Is_Node_Deep), what permission it has (Permission), and what is +-- the lowest permission of all its descendants (Children_Permission). After +-- unfolding the tree, we update the permissions of each node, deleting the +-- Children_Permission, and specifying new ones for the leaves of the unfolded +-- tree. + +-- After assigning a path, the descendants of the assigned path are dumped +-- (and hence the tree is folded back), given that all descendants directly +-- get read-write permission, which can be specified using the node's +-- Children_Permission field. + +with Types; use Types; + +package Sem_SPARK is + + procedure Check_Safe_Pointers (N : Node_Id); + -- The entry point of this package. It analyzes a node and reports errors + -- when there are violations of aliasing rules. + +end Sem_SPARK; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index bbf60a65bb0..6dc3591b973 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -8093,6 +8093,124 @@ package body Sem_Util is end if; end First_Actual; + ------------------ + -- First_Global -- + ------------------ + + function First_Global + (Subp : Entity_Id; + Global_Mode : Name_Id; + Refined : Boolean := False) return Node_Id + is + function First_From_Global_List + (List : Node_Id; + Global_Mode : Name_Id := Name_Input) return Entity_Id; + -- Get the first item with suitable mode from List + + ---------------------------- + -- First_From_Global_List -- + ---------------------------- + + function First_From_Global_List + (List : Node_Id; + Global_Mode : Name_Id := Name_Input) return Entity_Id + is + Assoc : Node_Id; + + begin + -- Empty list (no global items) + + if Nkind (List) = N_Null then + return Empty; + + -- Single global item declaration (only input items) + + elsif Nkind_In (List, N_Expanded_Name, + N_Identifier, + N_Selected_Component) + then + if Global_Mode = Name_Input then + return List; + else + return Empty; + end if; + + -- Simple global list (only input items) or moded global list + -- declaration. + + elsif Nkind (List) = N_Aggregate then + if Present (Expressions (List)) then + if Global_Mode = Name_Input then + return First (Expressions (List)); + else + return Empty; + end if; + + else + Assoc := First (Component_Associations (List)); + while Present (Assoc) loop + + -- When we find the desired mode in an association, call + -- recursively First_From_Global_List as if the mode was + -- Name_Input, in order to reuse the existing machinery + -- for the other cases. + + if Chars (First (Choices (Assoc))) = Global_Mode then + return First_From_Global_List (Expression (Assoc)); + end if; + + Next (Assoc); + end loop; + + return Empty; + end if; + + -- To accommodate partial decoration of disabled SPARK features, + -- this routine may be called with illegal input. If this is the + -- case, do not raise Program_Error. + + else + return Empty; + end if; + end First_From_Global_List; + + -- Local variables + + Global : Node_Id := Empty; + Body_Id : Entity_Id; + + begin + pragma Assert (Global_Mode = Name_Input + or else Global_Mode = Name_Output + or else Global_Mode = Name_In_Out + or else Global_Mode = Name_Proof_In); + + -- Retrieve the suitable pragma Global or Refined_Global. In the second + -- case, it can only be located on the body entity. + + if Refined then + Body_Id := Subprogram_Body_Entity (Subp); + if Present (Body_Id) then + Global := Get_Pragma (Body_Id, Pragma_Refined_Global); + end if; + else + Global := Get_Pragma (Subp, Pragma_Global); + end if; + + -- No corresponding global if pragma is not present + + if No (Global) then + return Empty; + + -- Otherwise retrieve the corresponding list of items depending on the + -- Global_Mode. + + else + return First_From_Global_List + (Expression (Get_Argument (Global, Subp)), Global_Mode); + end if; + end First_Global; + ------------- -- Fix_Msg -- ------------- @@ -18980,6 +19098,27 @@ package body Sem_Util is Actual_Id := Next_Actual (Actual_Id); end Next_Actual; + ----------------- + -- Next_Global -- + ----------------- + + function Next_Global (Node : Node_Id) return Node_Id is + begin + -- The global item may either be in a list, or by itself, in which case + -- there is no next global item with the same mode. + + if Is_List_Member (Node) then + return Next (Node); + else + return Empty; + end if; + end Next_Global; + + procedure Next_Global (Node : in out Node_Id) is + begin + Node := Next_Global (Node); + end Next_Global; + ---------------------------------- -- New_Requires_Transient_Scope -- ---------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 40325bf2a8c..5049ad6a7f8 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -885,6 +885,17 @@ package Sem_Util is -- Note that the value returned is always the expression (not the -- N_Parameter_Association nodes, even if named association is used). + function First_Global + (Subp : Entity_Id; + Global_Mode : Name_Id; + Refined : Boolean := False) return Node_Id; + -- Returns the first global item of mode Global_Mode (which can be + -- Name_Input, Name_Output, Name_In_Out or Name_Proof_In) associated to + -- subprogram Subp, or Empty otherwise. If Refined is True, the global item + -- is retrieved from the Refined_Global aspect/pragma associated to the + -- body of Subp if present. Next_Global can be used to get the next global + -- item with the same mode. + function Fix_Msg (Id : Entity_Id; Msg : String) return String; -- Replace all occurrences of a particular word in string Msg depending on -- the Ekind of Id as follows: @@ -2177,6 +2188,16 @@ package Sem_Util is -- Note that the result produced is always an expression, not a parameter -- association node, even if named notation was used. + procedure Next_Global (Node : in out Node_Id); + pragma Inline (Next_Actual); + -- Next_Global (N) is equivalent to N := Next_Global (N). Note that we + -- inline this procedural form, but not the functional form that follows. + + function Next_Global (Node : Node_Id) return Node_Id; + -- Node is a global item from a list, obtained through calling First_Global + -- and possibly Next_Global a number of times. Returns the next global item + -- with the same mode. + function No_Heap_Finalization (Typ : Entity_Id) return Boolean; -- Determine whether type Typ is subject to pragma No_Heap_Finalization -- 2.30.2