From: Yannick Moy Date: Thu, 19 Sep 2019 08:13:43 +0000 (+0000) Subject: [Ada] Move SPARK borrow-checker to gnat2why codebase X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f5766e3b541a9fb2d4365281f5c9da4f80e9622c;p=gcc.git [Ada] Move SPARK borrow-checker to gnat2why codebase Unit sem_spark was implementing the borrow-checker for the support of ownership pointers in SPARK. It has been moved to gnat2why codebase to facilitate its evolution and allow the more powerful flow analysis to provide its results for better analysis on pointers. 2019-09-19 Yannick Moy gcc/ada/ * gcc-interface/Make-lang.in: Remove references to sem_spark. * sem_spark.adb, sem_spark.ads: Remove unit. From-SVN: r275944 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 289213e914a..6fa4edf21ca 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-09-19 Yannick Moy + + * gcc-interface/Make-lang.in: Remove references to sem_spark. + * sem_spark.adb, sem_spark.ads: Remove unit. + 2019-09-19 Eric Botcazou * exp_attr.adb (Is_Inline_Floating_Point_Attribute): Treat diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index df5f0b3373b..276c41c2edf 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -450,7 +450,6 @@ 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/sem_spark.adb b/gcc/ada/sem_spark.adb deleted file mode 100644 index e4a8b3ecaaf..00000000000 --- a/gcc/ada/sem_spark.adb +++ /dev/null @@ -1,6179 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- S E M _ S P A R K -- --- -- --- B o d y -- --- -- --- Copyright (C) 2017-2019, 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 with 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; - -- The hash function - - -- Permission type associated with paths. These are related to but not - -- the same as the states associated with names used in SPARK RM 3.10: - -- Unrestricted, Observed, Borrowed, Moved. When ownership rules lead to - -- a state change for a name, this may correspond to multiple permission - -- changes for the paths corresponding to the name, its prefixes, and - -- its extensions. For example, when an object is assigned to, the - -- corresponding name gets into state Moved, while the path for the name - -- gets permission Write_Only as well as every prefix of the name, and - -- every suffix gets permission No_Access. - - type Perm_Kind_Option is - (None, - -- Special value used when no permission is passed around - - No_Access, - -- The path cannot be accessed for reading or writing. This is the - -- case for the path of a name in the Borrowed state. - - Read_Only, - -- The path can only be accessed for reading. This is the case for - -- the path of a name in the Observed state. - - Read_Write, - -- The path can be accessed for both reading and writing. This is the - -- case for the path of a name in the Unrestricted state. - - Write_Only - -- The path can only be accessed for writing. This is the case for - -- the path of a name in the Moved state. - ); - - subtype Perm_Kind is Perm_Kind_Option range No_Access .. Write_Only; - 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 => Entity_Id, - Element => Perm_Tree_Access, - No_Element => null, - Hash => Elaboration_Context_Hash, - Equal => "="); - -- The instantation of a hash table, with keys being entities and values - -- being pointers to permission trees. This is used to define global - -- environment permissions (entities in that case are stand-alone - -- objects or formal parameters), as well as the permissions for the - -- extensions of a Record_Component node (entities in that case are - -- record components). - - -- 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 reached through 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, i.e. an access type or a - -- composite type containing access type subcomponents. This - -- corresponds to both "observing" and "owning" types in SPARK RM - -- 3.10. To be used when moving the path. - - Explanation : Node_Id; - -- Node that can be used in an explanation for a permission mismatch - - 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 elements is - -- given in Get_Elem. - - when Array_Component => - Get_Elem : Perm_Tree_Access; - - -- Unfolded path of record type. The permission of the components - -- is given in Component. - - when Record_Component => - Component : Perm_Tree_Maps.Instance; - 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 from entities to permission trees. - - 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 Variable_Maps is new Simple_HTable - (Header_Num => Elaboration_Context_Index, - Key => Entity_Id, - Element => Node_Id, - No_Element => Empty, - Hash => Elaboration_Context_Hash, - Equal => "="); - - type Variable_Mapping is new Variable_Maps.Instance; - -- Mapping from variables to nodes denoting paths that are observed or - -- borrowed by the variable. - - -------------------- - -- 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 Explanation (T : Perm_Tree_Access) return Node_Id; - 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 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 Move_Env (From, To : in out Perm_Env); - -- Procedure to move a permission environment. It frees To, moves From - -- in To and sets From to Nil. - - procedure Move_Variable_Mapping (From, To : in out Variable_Mapping); - -- Move a variable mapping, freeing memory as needed and resetting the - -- source mapping. - - procedure Copy_Tree (From, 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_Tree (PT : in out Perm_Tree_Access); - -- Procedure to free a permission tree - - -------------------- - -- Error Messages -- - -------------------- - - procedure Perm_Mismatch - (N : Node_Id; - Exp_Perm : Perm_Kind; - Act_Perm : Perm_Kind; - Expl : Node_Id; - Forbidden_Perm : Boolean := False); - -- 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 - Free_Env (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_Tree -- - --------------- - - procedure Copy_Tree (From, To : Perm_Tree_Access) is - begin - -- Copy the direct components of the tree - - To.all := From.all; - - -- Now reallocate access components for a deep copy of the tree - - 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; - 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_Tree (CompO); - CompO := Get_Next (PE); - end loop; - - Reset (PE); - end Free_Env; - - --------------- - -- Free_Tree -- - --------------- - - procedure Free_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 => - null; - - when Reference => - Free_Tree (PT.all.Tree.Get_All); - - when Array_Component => - Free_Tree (PT.all.Tree.Get_Elem); - - when Record_Component => - declare - Comp : Perm_Tree_Access; - - begin - Comp := Perm_Tree_Maps.Get_First (Component (PT)); - while Comp /= null loop - - -- Free every Component subtree - - Free_Tree (Comp); - Comp := Perm_Tree_Maps.Get_Next (Component (PT)); - end loop; - end; - end case; - - Free_Perm_Tree_Dealloc (PT); - end Free_Tree; - - ----------------- - -- Explanation -- - ----------------- - - function Explanation (T : Perm_Tree_Access) return Node_Id is - begin - return T.all.Tree.Explanation; - end Explanation; - - ------------- - -- 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; - - -------------- - -- Move_Env -- - -------------- - - procedure Move_Env (From, To : in out Perm_Env) is - begin - Free_Env (To); - To := From; - From := Perm_Env (Perm_Tree_Maps.Nil); - end Move_Env; - - --------------------------- - -- Move_Variable_Mapping -- - --------------------------- - - procedure Move_Variable_Mapping (From, To : in out Variable_Mapping) is - begin - Reset (To); - To := From; - From := Variable_Mapping (Variable_Maps.Nil); - end Move_Variable_Mapping; - - ---------------- - -- Permission -- - ---------------- - - function Permission (T : Perm_Tree_Access) return Perm_Kind is - begin - return T.all.Tree.Permission; - end Permission; - - ------------------- - -- Perm_Mismatch -- - ------------------- - - procedure Perm_Mismatch - (N : Node_Id; - Exp_Perm : Perm_Kind; - Act_Perm : Perm_Kind; - Expl : Node_Id; - Forbidden_Perm : Boolean := False) - is - begin - Error_Msg_Sloc := Sloc (Expl); - - if Forbidden_Perm then - if Exp_Perm = No_Access then - Error_Msg_N ("\object was moved #", N); - else - raise Program_Error; - end if; - else - case Exp_Perm is - when Write_Perm => - if Act_Perm = Read_Only then - Error_Msg_N - ("\object was declared as not writeable #", N); - else - Error_Msg_N ("\object was moved #", N); - end if; - - when Read_Only => - Error_Msg_N ("\object was moved #", N); - - when No_Access => - raise Program_Error; - end case; - end if; - end Perm_Mismatch; - - end Permissions; - - use Permissions; - - -------------------------------------- - -- Analysis modes for AST traversal -- - -------------------------------------- - - -- The different modes for analysis. This allows checking whether a path - -- has the right permission, and also updating permissions when a path is - -- moved, borrowed, or observed. - - type Extended_Checking_Mode is - - (Read_Subexpr, - -- Special value used for assignment, to check that subexpressions of - -- the assigned path are readable. - - Read, - -- Default mode - - Move, - -- Move semantics. Checks that paths have Read_Write permission. After - -- moving a path, its permission and the permission of its prefixes are - -- set to Write_Only, while 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 and the permission of its - -- extensions are set to Read_Write. The permission of its prefixes may - -- be normalized from Write_Only to Read_Write depending on other - -- permissions in the tree (a prefix gets permission Read_Write when all - -- its extensions become Read_Write). - - Borrow, - -- Borrow semantics. Checks that paths have Read_Write permission. After - -- borrowing a path, its permission and the permission of its prefixes - -- and extensions are set to No_Access. - - Observe - -- Observe semantics. Checks that paths have Read_Perm permission. After - -- observing a path, its permission and the permission of its prefixes - -- and extensions are set to Read_Only. - ); - - subtype Checking_Mode is Extended_Checking_Mode range Read .. Observe; - - type Result_Kind is (Folded, Unfolded); - -- 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; - Explanation : Node_Id; - when Unfolded => - Tree_Access : Perm_Tree_Access; - end case; - end record; - - type Error_Status is (OK, Error); - - ----------------------- - -- 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; - - procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id); - -- Handle assignment as part of an assignment statement or an object - -- declaration. - - procedure Check_Call_Statement (Call : Node_Id); - - procedure Check_Callable_Body (Body_N : Node_Id); - -- Entry point for the analysis of a subprogram or entry body - - procedure Check_Declaration (Decl : Node_Id); - - procedure Check_Declaration_Legality - (Decl : Node_Id; - Force : Boolean; - Legal : in out Boolean); - -- Check the legality of declaration Decl regarding rules not related to - -- permissions. Update Legal to False if a rule is violated. Issue an - -- error message if Force is True and Emit_Messages returns True. - - procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode); - pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint, - N_Range_Constraint, - N_Subtype_Indication, - N_Digits_Constraint, - N_Delta_Constraint) - or else Nkind (Expr) in N_Subexpr); - - procedure Check_Globals (Subp : Entity_Id); - -- This procedure takes a subprogram called and checks the permission of - -- globals. - - -- Checking proceduress for safe pointer usage. These procedures traverse - -- the AST, check nodes for correct permissions according to SPARK RM 3.10, - -- and update permissions depending on the node kind. The main procedure - -- Check_Node is mutually recursive with the specialized procedures that - -- follow. - - procedure Check_List (L : List_Id); - -- Calls Check_Node on each element of the list - - procedure Check_Loop_Statement (Stmt : Node_Id); - - procedure Check_Node (N : Node_Id); - -- Main traversal procedure to check safe pointer usage - - procedure Check_Old_Loop_Entry (N : Node_Id); - -- Check SPARK RM 3.10(13) regarding 'Old and 'Loop_Entry - - procedure Check_Package_Body (Pack : Node_Id); - - procedure Check_Package_Spec (Pack : Node_Id); - - procedure Check_Parameter_Or_Global - (Expr : Node_Id; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean); - -- Check the permission of every actual parameter or global - - procedure Check_Pragma (Prag : Node_Id); - - procedure Check_Source_Of_Borrow_Or_Observe - (Expr : Node_Id; - Status : out Error_Status); - - procedure Check_Statement (Stmt : Node_Id); - - procedure Check_Type_Legality - (Typ : Entity_Id; - Force : Boolean; - Legal : in out Boolean); - -- Check that type Typ is either not deep, or that it is an observing or - -- owning type according to SPARK RM 3.10 - - function Get_Expl (N : Node_Or_Entity_Id) return Node_Id; - -- The function that takes a name as input and returns an explanation node - -- for the permission associated with it. - - function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id; - pragma Precondition (Is_Path_Expression (Expr)); - -- Return the expression being borrowed/observed when borrowing or - -- observing Expr. If Expr contains a call to traversal function, this is - -- the first actual of the first such call, otherwise it is Expr. - - function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind; - -- The function that takes a name as input and returns a permission - -- associated with it. - - function Get_Perm_Or_Tree (N : Node_Id) return Perm_Or_Tree; - pragma Precondition (Is_Path_Expression (N)); - -- This function gets a node and looks recursively to find the appropriate - -- subtree for that node. 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; - pragma Precondition (Is_Path_Expression (N)); - -- This function gets a node and looks recursively to find the appropriate - -- subtree for that node. If the tree is folded, then it unrolls the tree - -- up to the appropriate level. - - function Get_Root_Object - (Expr : Node_Id; - Through_Traversal : Boolean := True; - Is_Traversal : Boolean := False) return Entity_Id; - -- Return the root of the path expression Expr, or Empty for an allocator, - -- NULL, or a function call. Through_Traversal is True if it should follow - -- through calls to traversal functions. Is_Traversal is True if this - -- corresponds to a value returned from a traversal function, which should - -- allow if-expressions and case-expressions that refer to the same root, - -- even if the paths are not the same in all branches. - - generic - with procedure Handle_Parameter_Or_Global - (Expr : Node_Id; - Formal_Typ : Entity_Id; - Param_Mode : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean); - procedure Handle_Globals (Subp : Entity_Id); - -- Handling of globals is factored in a generic instantiated below - - function Has_Array_Component (Expr : Node_Id) return Boolean; - pragma Precondition (Is_Path_Expression (Expr)); - -- This function gets a node and looks recursively to determine whether the - -- given path has any array 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; E : 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_Path_Expression - (Expr : Node_Id; - Is_Traversal : Boolean := False) return Boolean; - -- Return whether Expr corresponds to a path. Is_Traversal is True if this - -- corresponds to a value returned from a traversal function, which should - -- allow if-expressions and case-expressions. - - function Is_Subpath_Expression - (Expr : Node_Id; - Is_Traversal : Boolean := False) return Boolean; - -- Return True if Expr can be part of a path expression. Is_Traversal is - -- True if this corresponds to a value returned from a traversal function, - -- which should allow if-expressions and case-expressions. - - function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean; - -- Determine if the candidate Prefix is indeed a prefix of Expr, or almost - -- a prefix, in the sense that they could still refer to overlapping memory - -- locations. - - function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean; - - 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_Env (Source : in out Perm_Env; Target : 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; - Expl : Node_Id; - Forbidden_Perm : Boolean := False); - -- A procedure that is called when the permissions found contradict the - -- rules established by the RM. This function is called with the node and - -- the permission that was expected, and issues 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; - Expl : Node_Id); - -- 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, the node of the returning function, and the - -- permission that was expected, and adds an error message with the - -- appropriate values. - - procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode); - pragma Precondition (Is_Path_Expression (Expr)); - -- Check correct permission for the path in the checking mode Mode, and - -- update permissions of the path and its prefixes/extensions. - - procedure Return_Globals (Subp : Entity_Id); - -- Takes a subprogram as input, and checks that all borrowed global items - -- of the subprogram indeed have Read_Write permission at the end of the - -- subprogram execution. - - procedure Return_Parameter_Or_Global - (Id : Entity_Id; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean); - -- Auxiliary procedure to Return_Parameters and Return_Globals - - procedure Return_Parameters (Subp : Entity_Id); - -- Takes a subprogram as input, and checks that all out parameters of the - -- subprogram indeed have Read_Write permission at the end of the - -- subprogram execution. - - procedure Set_Perm_Extensions - (T : Perm_Tree_Access; - P : Perm_Kind; - Expl : Node_Id); - -- 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; - Expl : Node_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 - (N : Node_Id; - Perm : Perm_Kind_Option; - Expl : Node_Id) return Perm_Tree_Access; - pragma Precondition (Is_Path_Expression (N)); - -- This function modifies the permissions of a given node in the permission - -- environment as well as all the prefixes of the path, to the new - -- permission Perm. The general rule here is that everybody updates the - -- permission of the subtree they are returning. - - procedure Set_Perm_Prefixes_Assign (N : Node_Id); - pragma Precondition (Is_Path_Expression (N)); - -- This procedure 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, and then Set_Perm_Prefixes_Assign will - -- change the permission of x to RW because all of its components have - -- permission RW. - - 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; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean; - Expl : Node_Id); - -- 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. - - procedure Setup_Protected_Components (Subp : Entity_Id); - -- Takes a protected operation as input, and sets up the environment by - -- adding protected components 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. - - Inside_Procedure_Call : Boolean := False; - -- Set while checking the actual parameters of a procedure or entry call - - Inside_Elaboration : Boolean := False; - -- Set during package spec/body elaboration, during which move and local - -- observe/borrow are not allowed. As a result, no other checking is needed - -- during elaboration. - - 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_Borrowers : Variable_Mapping; - -- Mapping from borrowers to the path borrowed - - Current_Observers : Variable_Mapping; - -- Mapping from observers to the path observed - - -------------------- - -- Handle_Globals -- - -------------------- - - -- Generic procedure is defined first so that instantiations can be defined - -- anywhere afterwards. - - procedure Handle_Globals (Subp : Entity_Id) is - - -- Local subprograms - - procedure Handle_Globals_From_List - (First_Item : Node_Id; - Kind : Formal_Kind); - -- Handle global items from the list starting at Item - - procedure Handle_Globals_Of_Mode (Global_Mode : Name_Id); - -- Handle global items for the mode Global_Mode - - ------------------------------ - -- Handle_Globals_From_List -- - ------------------------------ - - procedure Handle_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 - Handle_Parameter_Or_Global (Expr => Item, - Formal_Typ => Retysp (Etype (Item)), - Param_Mode => Kind, - Subp => Subp, - Global_Var => True); - end if; - - Next_Global (Item); - end loop; - end Handle_Globals_From_List; - - ---------------------------- - -- Handle_Globals_Of_Mode -- - ---------------------------- - - procedure Handle_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; - - -- Check both global items from Global and Refined_Global pragmas - - Handle_Globals_From_List (First_Global (Subp, Global_Mode), Kind); - Handle_Globals_From_List - (First_Global (Subp, Global_Mode, Refined => True), Kind); - end Handle_Globals_Of_Mode; - - -- Start of processing for Handle_Globals - - begin - Handle_Globals_Of_Mode (Name_Proof_In); - Handle_Globals_Of_Mode (Name_Input); - Handle_Globals_Of_Mode (Name_Output); - Handle_Globals_Of_Mode (Name_In_Out); - end Handle_Globals; - - ---------- - -- "<=" -- - ---------- - - 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_Assignment -- - ---------------------- - - procedure Check_Assignment (Target : Node_Or_Entity_Id; Expr : Node_Id) is - - -- Local subprograms - - procedure Handle_Borrow - (Var : Entity_Id; - Expr : Node_Id; - Is_Decl : Boolean); - -- Update map of current borrowers - - procedure Handle_Observe - (Var : Entity_Id; - Expr : Node_Id; - Is_Decl : Boolean); - -- Update map of current observers - - ------------------- - -- Handle_Borrow -- - ------------------- - - procedure Handle_Borrow - (Var : Entity_Id; - Expr : Node_Id; - Is_Decl : Boolean) - is - Borrowed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr); - - begin - -- SPARK RM 3.10(7): If the type of the target is an anonymous - -- access-to-variable type (an owning access type), the source shall - -- be an owning access object [..] whose root object is the target - -- object itself. - - -- ??? In fact we could be slightly more permissive in allowing even - -- a call to a traversal function of the right form. - - if not Is_Decl - and then (Is_Traversal_Function_Call (Expr) - or else Get_Root_Object (Borrowed) /= Var) - then - if Emit_Messages then - Error_Msg_NE - ("source of assignment must have & as root" & - " (SPARK RM 3.10(7)))", - Expr, Var); - end if; - return; - end if; - - Set (Current_Borrowers, Var, Borrowed); - end Handle_Borrow; - - -------------------- - -- Handle_Observe -- - -------------------- - - procedure Handle_Observe - (Var : Entity_Id; - Expr : Node_Id; - Is_Decl : Boolean) - is - Observed : constant Node_Id := Get_Observed_Or_Borrowed_Expr (Expr); - - begin - -- ??? We are currently using the same restriction for observers - -- as for borrowers. To be seen if the SPARK RM current rule really - -- allows more uses. - - if not Is_Decl - and then (Is_Traversal_Function_Call (Expr) - or else Get_Root_Object (Observed) /= Var) - then - if Emit_Messages then - Error_Msg_NE - ("source of assignment must have & as root" & - " (SPARK RM 3.10(7)))", - Expr, Var); - end if; - return; - end if; - - Set (Current_Observers, Var, Observed); - end Handle_Observe; - - -- Local variables - - Target_Typ : constant Node_Id := Etype (Target); - Is_Decl : constant Boolean := Nkind (Target) = N_Defining_Identifier; - Target_Root : Entity_Id; - Expr_Root : Entity_Id; - Perm : Perm_Kind; - Status : Error_Status; - Dummy : Boolean := True; - - -- Start of processing for Check_Assignment - - begin - Check_Type_Legality (Target_Typ, Force => True, Legal => Dummy); - - if Is_Anonymous_Access_Type (Target_Typ) then - Check_Source_Of_Borrow_Or_Observe (Expr, Status); - - if Status /= OK then - return; - end if; - - if Is_Decl then - Target_Root := Target; - else - Target_Root := Get_Root_Object (Target); - end if; - - Expr_Root := Get_Root_Object (Expr); - - -- SPARK RM 3.10(7): For an assignment statement where the target is - -- a stand-alone object of an anonymous access-to-object type. - - pragma Assert (Present (Target_Root)); - - -- If the type of the target is an anonymous access-to-constant type - -- (an observing access type), the source shall be an owning access - -- object denoted by a name that is not in the Moved state, and whose - -- root object is not in the Moved state and is not declared at a - -- statically deeper accessibility level than that of the target - -- object. - - if Is_Access_Constant (Target_Typ) then - Perm := Get_Perm (Expr); - - if Perm = No_Access then - Perm_Error (Expr, No_Access, No_Access, - Expl => Get_Expl (Expr), - Forbidden_Perm => True); - return; - end if; - - Perm := Get_Perm (Expr_Root); - - if Perm = No_Access then - Perm_Error (Expr, No_Access, No_Access, - Expl => Get_Expl (Expr_Root), - Forbidden_Perm => True); - return; - end if; - - -- ??? check accessibility level - - -- If the type of the target is an anonymous access-to-variable - -- type (an owning access type), the source shall be an owning - -- access object denoted by a name that is in the Unrestricted - -- state, and whose root object is the target object itself. - - Check_Expression (Expr, Observe); - Handle_Observe (Target_Root, Expr, Is_Decl); - - else - Perm := Get_Perm (Expr); - - if Perm /= Read_Write then - Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr)); - return; - end if; - - if not Is_Decl then - if not Is_Entity_Name (Target) then - if Emit_Messages then - Error_Msg_N - ("target of borrow must be stand-alone variable", - Target); - end if; - return; - - elsif Target_Root /= Expr_Root then - if Emit_Messages then - Error_Msg_NE - ("source of borrow must be variable &", - Expr, Target); - end if; - return; - end if; - end if; - - Check_Expression (Expr, Borrow); - Handle_Borrow (Target_Root, Expr, Is_Decl); - end if; - - elsif Is_Deep (Target_Typ) then - - if Is_Path_Expression (Expr) then - Check_Expression (Expr, Move); - - else - if Emit_Messages then - Error_Msg_N ("expression not allowed as source of move", Expr); - end if; - return; - end if; - - else - Check_Expression (Expr, Read); - end if; - end Check_Assignment; - - -------------------------- - -- Check_Call_Statement -- - -------------------------- - - procedure Check_Call_Statement (Call : Node_Id) is - - Subp : constant Entity_Id := Get_Called_Entity (Call); - - -- Local subprograms - - procedure Check_Param (Formal : Entity_Id; Actual : Node_Id); - -- Check the permission of every actual parameter - - procedure Update_Param (Formal : Entity_Id; Actual : Node_Id); - -- Update the permission of OUT actual parameters - - ----------------- - -- Check_Param -- - ----------------- - - procedure Check_Param (Formal : Entity_Id; Actual : Node_Id) is - begin - Check_Parameter_Or_Global - (Expr => Actual, - Typ => Retysp (Etype (Formal)), - Kind => Ekind (Formal), - Subp => Subp, - Global_Var => False); - end Check_Param; - - ------------------ - -- Update_Param -- - ------------------ - - procedure Update_Param (Formal : Entity_Id; Actual : Node_Id) is - Mode : constant Entity_Kind := Ekind (Formal); - - begin - case Formal_Kind'(Mode) is - when E_Out_Parameter => - Check_Expression (Actual, Assign); - - when others => - null; - end case; - end Update_Param; - - procedure Check_Params is new - Iterate_Call_Parameters (Check_Param); - - procedure Update_Params is new - Iterate_Call_Parameters (Update_Param); - - -- Start of processing for Check_Call_Statement - - begin - Inside_Procedure_Call := True; - Check_Params (Call); - if Ekind (Get_Called_Entity (Call)) = E_Subprogram_Type then - if Emit_Messages then - Error_Msg_N - ("call through access to subprogram is not allowed in SPARK", - Call); - end if; - else - Check_Globals (Get_Called_Entity (Call)); - end if; - - Inside_Procedure_Call := False; - Update_Params (Call); - end Check_Call_Statement; - - ------------------------- - -- Check_Callable_Body -- - ------------------------- - - procedure Check_Callable_Body (Body_N : Node_Id) is - Save_In_Elab : constant Boolean := Inside_Elaboration; - Body_Id : constant Entity_Id := Defining_Entity (Body_N); - Spec_Id : constant Entity_Id := Unique_Entity (Body_Id); - Prag : constant Node_Id := SPARK_Pragma (Body_Id); - - Saved_Env : Perm_Env; - Saved_Borrowers : Variable_Mapping; - Saved_Observers : Variable_Mapping; - - begin - -- Only SPARK bodies are analyzed - - if No (Prag) - or else Get_SPARK_Mode_From_Annotation (Prag) /= Opt.On - then - return; - end if; - - Inside_Elaboration := False; - - if Ekind (Spec_Id) = E_Function - and then Is_Anonymous_Access_Type (Etype (Spec_Id)) - and then not Is_Traversal_Function (Spec_Id) - then - if Emit_Messages then - Error_Msg_N ("anonymous access type for result only allowed for " - & "traversal functions", Spec_Id); - end if; - return; - end if; - - -- Save environment and put a new one in place - - Move_Env (Current_Perm_Env, Saved_Env); - Move_Variable_Mapping (Current_Borrowers, Saved_Borrowers); - Move_Variable_Mapping (Current_Observers, Saved_Observers); - - -- 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; - - -- For protected operations, add protected components to the environment - -- with adequate permissions. - - if Is_Protected_Operation (Spec_Id) then - Setup_Protected_Components (Spec_Id); - end if; - - -- Analyze the body of the subprogram - - 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; - - -- Restore the saved environment and free the current one - - Move_Env (Saved_Env, Current_Perm_Env); - Move_Variable_Mapping (Saved_Borrowers, Current_Borrowers); - Move_Variable_Mapping (Saved_Observers, Current_Observers); - - Inside_Elaboration := Save_In_Elab; - end Check_Callable_Body; - - ----------------------- - -- Check_Declaration -- - ----------------------- - - procedure Check_Declaration (Decl : Node_Id) is - Target : constant Entity_Id := Defining_Identifier (Decl); - Target_Typ : constant Node_Id := Etype (Target); - Expr : Node_Id; - Legal : Boolean := True; - - begin - -- Start with legality rules not related to permissions - - Check_Declaration_Legality (Decl, Force => True, Legal => Legal); - - -- Now check permission-related legality rules - - case N_Declaration'(Nkind (Decl)) is - when N_Full_Type_Declaration => - null; - - -- ??? What about component declarations with defaults. - - when N_Subtype_Declaration => - Check_Expression (Subtype_Indication (Decl), Read); - - when N_Object_Declaration => - Expr := Expression (Decl); - - if Legal and then Present (Expr) then - Check_Assignment (Target => Target, - Expr => Expr); - end if; - - -- Always add variable to the current permission environment, - -- even in the illegal case, as the rest of the analysis expects - -- to find it. - - if Is_Deep (Target_Typ) then - declare - Tree : constant Perm_Tree_Access := - new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => True, - Explanation => Decl, - Permission => Read_Write, - Children_Permission => Read_Write)); - begin - Set (Current_Perm_Env, Target, Tree); - end; - end if; - - when N_Iterator_Specification => - null; - - when N_Loop_Parameter_Specification => - null; - - -- Checking should not be called directly on these nodes - - when N_Function_Specification - | N_Entry_Declaration - | N_Procedure_Specification - | N_Component_Declaration - => - 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_Declaration_Legality -- - -------------------------------- - - procedure Check_Declaration_Legality - (Decl : Node_Id; - Force : Boolean; - Legal : in out Boolean) - is - function Original_Emit_Messages return Boolean renames Emit_Messages; - - function Emit_Messages return Boolean; - -- Local wrapper around generic formal parameter Emit_Messages, to - -- check the value of parameter Force before calling the original - -- Emit_Messages, and setting Legal to False. - - ------------------- - -- Emit_Messages -- - ------------------- - - function Emit_Messages return Boolean is - begin - Legal := False; - return Force and then Original_Emit_Messages; - end Emit_Messages; - - -- Local variables - - Target : constant Entity_Id := Defining_Identifier (Decl); - Target_Typ : constant Node_Id := Etype (Target); - Expr : Node_Id; - - -- Start of processing for Check_Declaration_Legality - - begin - case N_Declaration'(Nkind (Decl)) is - when N_Full_Type_Declaration => - Check_Type_Legality (Target, Force, Legal); - - when N_Subtype_Declaration => - null; - - when N_Object_Declaration => - Expr := Expression (Decl); - - Check_Type_Legality (Target_Typ, Force, Legal); - - -- A declaration of a stand-alone object of an anonymous access - -- type shall have an explicit initial value and shall occur - -- immediately within a subprogram body, an entry body, or a - -- block statement (SPARK RM 3.10(4)). - - if Is_Anonymous_Access_Type (Target_Typ) then - declare - Scop : constant Entity_Id := Scope (Target); - begin - if not Is_Local_Context (Scop) then - if Emit_Messages then - Error_Msg_N - ("object of anonymous access type must be declared " - & "immediately within a subprogram, entry or block " - & "(SPARK RM 3.10(4))", Decl); - end if; - end if; - end; - - if No (Expr) then - if Emit_Messages then - Error_Msg_N ("object of anonymous access type must be " - & "initialized (SPARK RM 3.10(4))", Decl); - end if; - end if; - end if; - - when N_Iterator_Specification => - null; - - when N_Loop_Parameter_Specification => - null; - - -- Checking should not be called directly on these nodes - - when N_Function_Specification - | N_Entry_Declaration - | N_Procedure_Specification - | N_Component_Declaration - => - 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_Legality; - - ---------------------- - -- Check_Expression -- - ---------------------- - - procedure Check_Expression - (Expr : Node_Id; - Mode : Extended_Checking_Mode) - is - -- Local subprograms - - function Is_Type_Name (Expr : Node_Id) return Boolean; - -- Detect when a path expression is in fact a type name - - procedure Move_Expression (Expr : Node_Id); - -- Some subexpressions are only analyzed in Move mode. This is a - -- specialized version of Check_Expression for that case. - - procedure Move_Expression_List (L : List_Id); - -- Call Move_Expression on every expression in the list L - - procedure Read_Expression (Expr : Node_Id); - -- Most subexpressions are only analyzed in Read mode. This is a - -- specialized version of Check_Expression for that case. - - procedure Read_Expression_List (L : List_Id); - -- Call Read_Expression on every expression in the list L - - procedure Read_Indexes (Expr : Node_Id); - -- When processing a path, the index expressions and function call - -- arguments occurring on the path should be analyzed in Read mode. - - ------------------ - -- Is_Type_Name -- - ------------------ - - function Is_Type_Name (Expr : Node_Id) return Boolean is - begin - return Nkind_In (Expr, N_Expanded_Name, N_Identifier) - and then Is_Type (Entity (Expr)); - end Is_Type_Name; - - --------------------- - -- Move_Expression -- - --------------------- - - -- Distinguish the case where the argument is a path expression that - -- needs explicit moving. - - procedure Move_Expression (Expr : Node_Id) is - begin - if Is_Path_Expression (Expr) then - Check_Expression (Expr, Move); - else - Read_Expression (Expr); - end if; - end Move_Expression; - - -------------------------- - -- Move_Expression_List -- - -------------------------- - - procedure Move_Expression_List (L : List_Id) is - N : Node_Id; - begin - N := First (L); - while Present (N) loop - Move_Expression (N); - Next (N); - end loop; - end Move_Expression_List; - - --------------------- - -- Read_Expression -- - --------------------- - - procedure Read_Expression (Expr : Node_Id) is - begin - Check_Expression (Expr, Read); - end Read_Expression; - - -------------------------- - -- Read_Expression_List -- - -------------------------- - - procedure Read_Expression_List (L : List_Id) is - N : Node_Id; - begin - N := First (L); - while Present (N) loop - Read_Expression (N); - Next (N); - end loop; - end Read_Expression_List; - - ------------------ - -- Read_Indexes -- - ------------------ - - procedure Read_Indexes (Expr : Node_Id) is - - -- Local subprograms - - function Is_Singleton_Choice (Choices : List_Id) return Boolean; - -- Return whether Choices is a singleton choice - - procedure Read_Param (Formal : Entity_Id; Actual : Node_Id); - -- Call Read_Expression on the actual - - ------------------------- - -- Is_Singleton_Choice -- - ------------------------- - - function Is_Singleton_Choice (Choices : List_Id) return Boolean is - Choice : constant Node_Id := First (Choices); - begin - return List_Length (Choices) = 1 - and then Nkind (Choice) /= N_Others_Choice - and then not Nkind_In (Choice, N_Subtype_Indication, N_Range) - and then not - (Nkind_In (Choice, N_Identifier, N_Expanded_Name) - and then Is_Type (Entity (Choice))); - end Is_Singleton_Choice; - - ---------------- - -- Read_Param -- - ---------------- - - procedure Read_Param (Formal : Entity_Id; Actual : Node_Id) is - pragma Unreferenced (Formal); - begin - Read_Expression (Actual); - end Read_Param; - - procedure Read_Params is new Iterate_Call_Parameters (Read_Param); - - -- Start of processing for Read_Indexes - - begin - if not Is_Subpath_Expression (Expr) then - if Emit_Messages then - Error_Msg_N - ("name expected here for move/borrow/observe", Expr); - end if; - return; - end if; - - case N_Subexpr'(Nkind (Expr)) is - when N_Identifier - | N_Expanded_Name - | N_Null - => - null; - - when N_Explicit_Dereference - | N_Selected_Component - => - Read_Indexes (Prefix (Expr)); - - when N_Indexed_Component => - Read_Indexes (Prefix (Expr)); - Read_Expression_List (Expressions (Expr)); - - when N_Slice => - Read_Indexes (Prefix (Expr)); - Read_Expression (Discrete_Range (Expr)); - - -- The argument of an allocator is moved as part of the implicit - -- assignment. - - when N_Allocator => - Move_Expression (Expression (Expr)); - - when N_Function_Call => - Read_Params (Expr); - if Ekind (Get_Called_Entity (Expr)) = E_Subprogram_Type then - if Emit_Messages then - Error_Msg_N - ("call through access to subprogram is not allowed in " - & "SPARK", Expr); - end if; - else - Check_Globals (Get_Called_Entity (Expr)); - end if; - - when N_Op_Concat => - Read_Expression (Left_Opnd (Expr)); - Read_Expression (Right_Opnd (Expr)); - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - Read_Indexes (Expression (Expr)); - - when N_Aggregate => - declare - Assocs : constant List_Id := Component_Associations (Expr); - CL : List_Id; - Assoc : Node_Id := Nlists.First (Assocs); - Choice : Node_Id; - - begin - -- The subexpressions of an aggregate are moved as part - -- of the implicit assignments. Handle the positional - -- components first. - - Move_Expression_List (Expressions (Expr)); - - -- Handle the named components next - - while Present (Assoc) loop - CL := Choices (Assoc); - - -- For an array aggregate, we should also check that the - -- expressions used in choices are readable. - - if Is_Array_Type (Etype (Expr)) then - Choice := Nlists.First (CL); - while Present (Choice) loop - if Nkind (Choice) /= N_Others_Choice then - Read_Expression (Choice); - end if; - Next (Choice); - end loop; - end if; - - -- There can be only one element for a value of deep type - -- in order to avoid aliasing. - - if not Box_Present (Assoc) - and then Is_Deep (Etype (Expression (Assoc))) - and then not Is_Singleton_Choice (CL) - and then Emit_Messages - then - Error_Msg_F - ("singleton choice required to prevent aliasing", - First (CL)); - end if; - - -- The subexpressions of an aggregate are moved as part - -- of the implicit assignments. - - if not Box_Present (Assoc) then - Move_Expression (Expression (Assoc)); - end if; - - Next (Assoc); - end loop; - end; - - when N_Extension_Aggregate => - declare - Exprs : constant List_Id := Expressions (Expr); - Assocs : constant List_Id := Component_Associations (Expr); - CL : List_Id; - Assoc : Node_Id := Nlists.First (Assocs); - - begin - Move_Expression (Ancestor_Part (Expr)); - - -- No positional components allowed at this stage - - if Present (Exprs) then - raise Program_Error; - end if; - - while Present (Assoc) loop - CL := Choices (Assoc); - - -- Only singleton components allowed at this stage - - if not Is_Singleton_Choice (CL) then - raise Program_Error; - end if; - - -- The subexpressions of an aggregate are moved as part - -- of the implicit assignments. - - if not Box_Present (Assoc) then - Move_Expression (Expression (Assoc)); - end if; - - Next (Assoc); - end loop; - end; - - when N_If_Expression => - declare - Cond : constant Node_Id := First (Expressions (Expr)); - Then_Part : constant Node_Id := Next (Cond); - Else_Part : constant Node_Id := Next (Then_Part); - begin - Read_Expression (Cond); - Read_Indexes (Then_Part); - Read_Indexes (Else_Part); - end; - - when N_Case_Expression => - declare - Cases : constant List_Id := Alternatives (Expr); - Cur_Case : Node_Id := First (Cases); - - begin - Read_Expression (Expression (Expr)); - - while Present (Cur_Case) loop - Read_Indexes (Expression (Cur_Case)); - Next (Cur_Case); - end loop; - end; - - when N_Attribute_Reference => - pragma Assert - (Get_Attribute_Id (Attribute_Name (Expr)) = - Attribute_Loop_Entry - or else - Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update - or else - Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Image); - - Read_Expression (Prefix (Expr)); - - if Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update - or else (Get_Attribute_Id (Attribute_Name (Expr)) = - Attribute_Image - and then Is_Type_Name (Prefix (Expr))) - then - Read_Expression_List (Expressions (Expr)); - end if; - - when others => - raise Program_Error; - end case; - end Read_Indexes; - - -- Start of processing for Check_Expression - - begin - if Is_Type_Name (Expr) then - return; - - elsif Is_Path_Expression (Expr) then - if Mode /= Assign then - Read_Indexes (Expr); - end if; - - if Mode /= Read_Subexpr then - Process_Path (Expr, Mode); - end if; - - return; - end if; - - -- Expressions that are not path expressions should only be analyzed in - -- Read mode. - - if Mode /= Read then - if Emit_Messages then - Error_Msg_N ("name expected here for move/borrow/observe", Expr); - end if; - return; - end if; - - -- Special handling for nodes that may contain evaluated expressions in - -- the form of constraints. - - case Nkind (Expr) is - when N_Index_Or_Discriminant_Constraint => - declare - Assn : Node_Id := First (Constraints (Expr)); - begin - while Present (Assn) loop - case Nkind (Assn) is - when N_Discriminant_Association => - Read_Expression (Expression (Assn)); - - when others => - Read_Expression (Assn); - end case; - - Next (Assn); - end loop; - end; - return; - - when N_Range_Constraint => - Read_Expression (Range_Expression (Expr)); - return; - - when N_Subtype_Indication => - if Present (Constraint (Expr)) then - Read_Expression (Constraint (Expr)); - end if; - return; - - when N_Digits_Constraint => - Read_Expression (Digits_Expression (Expr)); - if Present (Range_Constraint (Expr)) then - Read_Expression (Range_Constraint (Expr)); - end if; - return; - - when N_Delta_Constraint => - Read_Expression (Delta_Expression (Expr)); - if Present (Range_Constraint (Expr)) then - Read_Expression (Range_Constraint (Expr)); - end if; - return; - - when others => - null; - end case; - - -- At this point Expr can only be a subexpression - - case N_Subexpr'(Nkind (Expr)) is - - when N_Binary_Op - | N_Short_Circuit - => - Read_Expression (Left_Opnd (Expr)); - Read_Expression (Right_Opnd (Expr)); - - when N_Membership_Test => - Read_Expression (Left_Opnd (Expr)); - if Present (Right_Opnd (Expr)) then - Read_Expression (Right_Opnd (Expr)); - else - declare - Cases : constant List_Id := Alternatives (Expr); - Cur_Case : Node_Id := First (Cases); - - begin - while Present (Cur_Case) loop - Read_Expression (Cur_Case); - Next (Cur_Case); - end loop; - end; - end if; - - when N_Unary_Op => - Read_Expression (Right_Opnd (Expr)); - - when N_Attribute_Reference => - declare - Aname : constant Name_Id := Attribute_Name (Expr); - Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname); - Pref : constant Node_Id := Prefix (Expr); - Args : constant List_Id := Expressions (Expr); - - begin - case Attr_Id is - - -- The following attributes take either no arguments, or - -- arguments that do not refer to evaluated expressions - -- (like Length or Loop_Entry), hence only the prefix - -- needs to be read. - - when Attribute_Address - | Attribute_Alignment - | Attribute_Callable - | Attribute_Component_Size - | Attribute_Constrained - | Attribute_First - | Attribute_First_Bit - | Attribute_Last - | Attribute_Last_Bit - | Attribute_Length - | Attribute_Loop_Entry - | Attribute_Object_Size - | Attribute_Position - | Attribute_Size - | Attribute_Terminated - | Attribute_Valid - | Attribute_Value_Size - => - Read_Expression (Pref); - - -- The following attributes take a type name as prefix, - -- hence only the arguments need to be read. - - when Attribute_Ceiling - | Attribute_Floor - | Attribute_Max - | Attribute_Min - | Attribute_Mod - | Attribute_Pos - | Attribute_Pred - | Attribute_Remainder - | Attribute_Rounding - | Attribute_Succ - | Attribute_Truncation - | Attribute_Val - | Attribute_Value - => - Read_Expression_List (Args); - - -- Attributes Image and Img either take a type name as - -- prefix with an expression in argument, or the expression - -- directly as prefix. Adapt to each case. - - when Attribute_Image - | Attribute_Img - => - if No (Args) then - Read_Expression (Pref); - else - Read_Expression_List (Args); - end if; - - -- Attribute Update takes expressions as both prefix and - -- arguments, so both need to be read. - - when Attribute_Update => - Read_Expression (Pref); - Read_Expression_List (Args); - - -- Attribute Modulus does not reference the evaluated - -- expression, so it can be ignored for this analysis. - - when Attribute_Modulus => - null; - - -- The following attributes apply to types; there are no - -- expressions to read. - - when Attribute_Class - | Attribute_Storage_Size - => - null; - - -- Postconditions should not be analyzed - - when Attribute_Old - | Attribute_Result - => - raise Program_Error; - - when others => - null; - end case; - end; - - when N_Range => - Read_Expression (Low_Bound (Expr)); - Read_Expression (High_Bound (Expr)); - - when N_If_Expression => - Read_Expression_List (Expressions (Expr)); - - when N_Case_Expression => - declare - Cases : constant List_Id := Alternatives (Expr); - Cur_Case : Node_Id := First (Cases); - - begin - while Present (Cur_Case) loop - Read_Expression (Expression (Cur_Case)); - Next (Cur_Case); - end loop; - - Read_Expression (Expression (Expr)); - end; - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - Read_Expression (Expression (Expr)); - - when N_Quantified_Expression => - declare - For_In_Spec : constant Node_Id := - Loop_Parameter_Specification (Expr); - For_Of_Spec : constant Node_Id := - Iterator_Specification (Expr); - For_Of_Spec_Typ : Node_Id; - - begin - if Present (For_In_Spec) then - Read_Expression (Discrete_Subtype_Definition (For_In_Spec)); - else - Read_Expression (Name (For_Of_Spec)); - For_Of_Spec_Typ := Subtype_Indication (For_Of_Spec); - if Present (For_Of_Spec_Typ) then - Read_Expression (For_Of_Spec_Typ); - end if; - end if; - - Read_Expression (Condition (Expr)); - end; - - when N_Character_Literal - | N_Numeric_Or_String_Literal - | N_Operator_Symbol - | N_Raise_Expression - | N_Raise_xxx_Error - => - null; - - when N_Delta_Aggregate - | N_Target_Name - => - null; - - -- Procedure calls are handled in Check_Node - - when N_Procedure_Call_Statement => - raise Program_Error; - - -- Path expressions are handled before this point - - when N_Aggregate - | N_Allocator - | N_Expanded_Name - | N_Explicit_Dereference - | N_Extension_Aggregate - | N_Function_Call - | N_Identifier - | N_Indexed_Component - | N_Null - | N_Selected_Component - | N_Slice - => - raise Program_Error; - - -- 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_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 (Stmt : 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; - Expl : Node_Id); - -- 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, Stmt, Permission (Tree), Perm, Explanation (Tree)); - end if; - - case Kind (Tree) is - when Entire_Object => - if not (Children_Permission (Tree) >= Perm) then - Perm_Error_Loop_Exit - (E, Stmt, Children_Permission (Tree), Perm, - Explanation (Tree)); - - 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; - 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, Stmt, Permission (Tree), Perm, Explanation (Tree)); - end if; - - case Kind (Tree) is - when Entire_Object => - if not (Perm >= Children_Permission (Tree)) then - Perm_Error_Loop_Exit - (E, Stmt, Children_Permission (Tree), Perm, - Explanation (Tree)); - 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; - 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 => Stmt, - Perm => Permission (New_Tree), - Found_Perm => Permission (Orig_Tree), - Expl => Explanation (New_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, Stmt, - Children_Permission (New_Tree), - Children_Permission (Orig_Tree), - Explanation (New_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; - 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; - - 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 - CompN := Perm_Tree_Maps.Get - (Component (New_Tree), KeyO.K); - CompO := Perm_Tree_Maps.Get - (Component (Orig_Tree), KeyO.K); - pragma Assert (CompO /= null); - - Check_Is_Less_Restrictive_Tree (CompN, CompO, E); - - KeyO := Perm_Tree_Maps.Get_Next_Key - (Component (Orig_Tree)); - end loop; - 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; - Expl : Node_Id) - is - begin - if Emit_Messages then - 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, - Expl => Expl); - end if; - end Perm_Error_Loop_Exit; - - -- Local variables - - Loop_Name : constant Entity_Id := Entity (Identifier (Stmt)); - Loop_Env : constant Perm_Env_Access := new Perm_Env; - Scheme : constant Node_Id := Iteration_Scheme (Stmt); - - -- Start of processing for Check_Loop_Statement - - 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 (Stmt)) 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 - - if Present (Scheme) then - - -- Case of a WHILE loop - - if Present (Condition (Scheme)) then - Check_Expression (Condition (Scheme), Read); - - -- Case of a FOR loop - - else - declare - Param_Spec : constant Node_Id := - Loop_Parameter_Specification (Scheme); - Iter_Spec : constant Node_Id := Iterator_Specification (Scheme); - begin - if Present (Param_Spec) then - Check_Expression - (Discrete_Subtype_Definition (Param_Spec), Read); - else - Check_Expression (Name (Iter_Spec), Read); - if Present (Subtype_Indication (Iter_Spec)) then - Check_Expression (Subtype_Indication (Iter_Spec), Read); - end if; - end if; - end; - end if; - end if; - - Check_List (Statements (Stmt)); - - -- 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); - Free_Env (Loop_Env.all); - Free_Env (Exit_Env.all); - else - Copy_Env (From => Loop_Env.all, To => Current_Perm_Env); - Free_Env (Loop_Env.all); - end if; - end; - end Check_Loop_Statement; - - ---------------- - -- Check_Node -- - ---------------- - - procedure Check_Node (N : Node_Id) is - - procedure Check_Subprogram_Contract (N : Node_Id); - -- Check the postcondition-like contracts for use of 'Old - - ------------------------------- - -- Check_Subprogram_Contract -- - ------------------------------- - - procedure Check_Subprogram_Contract (N : Node_Id) is - begin - if Nkind (N) = N_Subprogram_Declaration - or else Acts_As_Spec (N) - then - declare - E : constant Entity_Id := Unique_Defining_Entity (N); - Post : constant Node_Id := - Get_Pragma (E, Pragma_Postcondition); - Cases : constant Node_Id := - Get_Pragma (E, Pragma_Contract_Cases); - begin - Check_Old_Loop_Entry (Post); - Check_Old_Loop_Entry (Cases); - end; - - elsif Nkind (N) = N_Subprogram_Body then - declare - E : constant Entity_Id := Defining_Entity (N); - Ref_Post : constant Node_Id := - Get_Pragma (E, Pragma_Refined_Post); - begin - Check_Old_Loop_Entry (Ref_Post); - end; - end if; - end Check_Subprogram_Contract; - - -- Start of processing for Check_Node - - begin - case Nkind (N) is - when N_Declaration => - Check_Declaration (N); - - when N_Body_Stub => - Check_Node (Get_Body_From_Stub (N)); - - when N_Statement_Other_Than_Procedure_Call => - Check_Statement (N); - - when N_Procedure_Call_Statement => - Check_Call_Statement (N); - - when N_Package_Body => - if not Is_Generic_Unit (Unique_Defining_Entity (N)) then - Check_Package_Body (N); - end if; - - when N_Subprogram_Body => - if not Is_Generic_Unit (Unique_Defining_Entity (N)) then - Check_Subprogram_Contract (N); - Check_Callable_Body (N); - end if; - - when N_Entry_Body - | N_Task_Body - => - Check_Callable_Body (N); - - when N_Protected_Body => - Check_List (Declarations (N)); - - when N_Package_Declaration => - Check_Package_Spec (N); - - when N_Handled_Sequence_Of_Statements => - Check_List (Statements (N)); - - when N_Pragma => - Check_Pragma (N); - - when N_Subprogram_Declaration => - Check_Subprogram_Contract (N); - - -- Attribute references in statement position are not supported in - -- SPARK and will be rejected by GNATprove. - - when N_Attribute_Reference => - null; - - -- Ignored constructs for pointer checking - - when N_Abstract_Subprogram_Declaration - | N_At_Clause - | N_Attribute_Definition_Clause - | N_Call_Marker - | 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_Procedure_Instantiation - | N_Raise_xxx_Error - | N_Record_Representation_Clause - | N_Subprogram_Renaming_Declaration - | N_Task_Type_Declaration - | N_Use_Package_Clause - | N_With_Clause - | N_Use_Type_Clause - | N_Validate_Unchecked_Conversion - | N_Variable_Reference_Marker - | N_Discriminant_Association - - -- ??? check whether we should do something special for - -- N_Discriminant_Association, or maybe raise Program_Error. - => - null; - - -- Checking should not be called directly on these nodes - - when others => - raise Program_Error; - end case; - end Check_Node; - - -------------------------- - -- Check_Old_Loop_Entry -- - -------------------------- - - procedure Check_Old_Loop_Entry (N : Node_Id) is - - function Check_Attribute (N : Node_Id) return Traverse_Result; - - --------------------- - -- Check_Attribute -- - --------------------- - - function Check_Attribute (N : Node_Id) return Traverse_Result is - Attr_Id : Attribute_Id; - Aname : Name_Id; - Pref : Node_Id; - - begin - if Nkind (N) = N_Attribute_Reference then - Attr_Id := Get_Attribute_Id (Attribute_Name (N)); - Aname := Attribute_Name (N); - - if Attr_Id = Attribute_Old - or else Attr_Id = Attribute_Loop_Entry - then - Pref := Prefix (N); - - if Is_Deep (Etype (Pref)) then - if Nkind (Pref) /= N_Function_Call then - if Emit_Messages then - Error_Msg_Name_1 := Aname; - Error_Msg_N - ("prefix of % attribute must be a function call " - & "(SPARK RM 3.10(13))", Pref); - end if; - - elsif Is_Traversal_Function_Call (Pref) then - if Emit_Messages then - Error_Msg_Name_1 := Aname; - Error_Msg_N - ("prefix of % attribute should not call a traversal " - & "function (SPARK RM 3.10(13))", Pref); - end if; - end if; - end if; - end if; - end if; - - return OK; - end Check_Attribute; - - procedure Check_All is new Traverse_Proc (Check_Attribute); - - -- Start of processing for Check_Old_Loop_Entry - - begin - Check_All (N); - end Check_Old_Loop_Entry; - - ------------------------ - -- Check_Package_Body -- - ------------------------ - - procedure Check_Package_Body (Pack : Node_Id) is - Save_In_Elab : constant Boolean := Inside_Elaboration; - Spec : constant Node_Id := - Package_Specification (Corresponding_Spec (Pack)); - Id : constant Entity_Id := Defining_Entity (Pack); - Prag : constant Node_Id := SPARK_Pragma (Id); - Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id); - Saved_Env : Perm_Env; - - begin - if Present (Prag) - and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On - then - Inside_Elaboration := True; - - -- Save environment and put a new one in place - - Move_Env (Current_Perm_Env, Saved_Env); - - -- Reanalyze package spec to have its variables in the environment - - Check_List (Visible_Declarations (Spec)); - Check_List (Private_Declarations (Spec)); - - -- Check declarations and statements in the special mode for - -- elaboration. - - Check_List (Declarations (Pack)); - - if Present (Aux_Prag) - and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On - then - Check_Node (Handled_Statement_Sequence (Pack)); - end if; - - -- Restore the saved environment and free the current one - - Move_Env (Saved_Env, Current_Perm_Env); - - Inside_Elaboration := Save_In_Elab; - end if; - end Check_Package_Body; - - ------------------------ - -- Check_Package_Spec -- - ------------------------ - - procedure Check_Package_Spec (Pack : Node_Id) is - Save_In_Elab : constant Boolean := Inside_Elaboration; - Spec : constant Node_Id := Specification (Pack); - Id : constant Entity_Id := Defining_Entity (Pack); - Prag : constant Node_Id := SPARK_Pragma (Id); - Aux_Prag : constant Node_Id := SPARK_Aux_Pragma (Id); - Saved_Env : Perm_Env; - - begin - if Present (Prag) - and then Get_SPARK_Mode_From_Annotation (Prag) = Opt.On - then - Inside_Elaboration := True; - - -- Save environment and put a new one in place - - Move_Env (Current_Perm_Env, Saved_Env); - - -- Check declarations in the special mode for elaboration - - Check_List (Visible_Declarations (Spec)); - - if Present (Aux_Prag) - and then Get_SPARK_Mode_From_Annotation (Aux_Prag) = Opt.On - then - Check_List (Private_Declarations (Spec)); - end if; - - -- Restore the saved environment and free the current one. As part of - -- the restoration, the environment of the package spec is merged in - -- the enclosing environment, which may be an enclosing - -- package/subprogram spec or body which has access to the variables - -- of the package spec. - - Merge_Env (Saved_Env, Current_Perm_Env); - - Inside_Elaboration := Save_In_Elab; - end if; - end Check_Package_Spec; - - ------------------------------- - -- Check_Parameter_Or_Global -- - ------------------------------- - - procedure Check_Parameter_Or_Global - (Expr : Node_Id; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean) - is - Mode : Checking_Mode; - Status : Error_Status; - - begin - if not Global_Var - and then Is_Anonymous_Access_Type (Typ) - then - Check_Source_Of_Borrow_Or_Observe (Expr, Status); - - if Status /= OK then - return; - end if; - end if; - - case Kind is - when E_In_Parameter => - - -- Inputs of functions have R permission only - - if Ekind (Subp) = E_Function then - Mode := Read; - - -- Input global variables have R permission only - - elsif Global_Var then - Mode := Read; - - -- Anonymous access to constant is an observe - - elsif Is_Anonymous_Access_Type (Typ) - and then Is_Access_Constant (Typ) - then - Mode := Observe; - - -- Other access types are a borrow - - elsif Is_Access_Type (Typ) then - Mode := Borrow; - - -- Deep types other than access types define an observe - - elsif Is_Deep (Typ) then - Mode := Observe; - - -- Otherwise the variable is read - - else - Mode := Read; - end if; - - when E_Out_Parameter => - Mode := Assign; - - when E_In_Out_Parameter => - Mode := Move; - end case; - - if Mode = Assign then - Check_Expression (Expr, Read_Subexpr); - end if; - - Check_Expression (Expr, Mode); - end Check_Parameter_Or_Global; - - procedure Check_Globals_Inst is - new Handle_Globals (Check_Parameter_Or_Global); - - procedure Check_Globals (Subp : Entity_Id) renames Check_Globals_Inst; - - ------------------ - -- Check_Pragma -- - ------------------ - - procedure Check_Pragma (Prag : Node_Id) is - Prag_Id : constant Pragma_Id := Get_Pragma_Id (Prag); - Arg1 : constant Node_Id := - First (Pragma_Argument_Associations (Prag)); - Arg2 : Node_Id := Empty; - - begin - if Present (Arg1) then - Arg2 := Next (Arg1); - end if; - - case Prag_Id is - when Pragma_Check => - declare - Expr : constant Node_Id := Expression (Arg2); - begin - Check_Expression (Expr, Read); - - -- Prefix of Loop_Entry should be checked inside any assertion - -- where it may appear. - - Check_Old_Loop_Entry (Expr); - end; - - -- Prefix of Loop_Entry should be checked inside a Loop_Variant - - when Pragma_Loop_Variant => - Check_Old_Loop_Entry (Prag); - - -- There is no need to check contracts, as these can only access - -- inputs and outputs of the subprogram. Inputs are checked - -- independently for R permission. Outputs are checked - -- independently to have RW permission on exit. - - -- Postconditions are checked for correct use of 'Old, but starting - -- from the corresponding declaration, in order to avoid dealing with - -- with contracts on generic subprograms which are not handled in - -- GNATprove. - - when Pragma_Precondition - | Pragma_Postcondition - | Pragma_Contract_Cases - | Pragma_Refined_Post - => - null; - - -- The same holds for the initial condition after package - -- elaboration, for the different reason that library-level - -- variables can only be left in RW state after elaboration. - - when Pragma_Initial_Condition => - null; - - -- These pragmas should have been rewritten and/or removed in - -- GNATprove mode. - - when Pragma_Assert - | Pragma_Assert_And_Cut - | Pragma_Assume - | Pragma_Compile_Time_Error - | Pragma_Compile_Time_Warning - | Pragma_Debug - | Pragma_Loop_Invariant - => - raise Program_Error; - - when others => - null; - end case; - end Check_Pragma; - - ------------------------- - -- 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); - end Initialize; - - -- 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_Declaration - | N_Subprogram_Body - => - declare - E : constant Entity_Id := Defining_Entity (N); - Prag : constant Node_Id := SPARK_Pragma (E); - -- SPARK_Mode pragma in application - - begin - if Ekind (Unique_Entity (E)) in Generic_Unit_Kind then - null; - - elsif Present (Prag) then - if Get_SPARK_Mode_From_Annotation (Prag) = Opt.On then - 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; - end; - - when others => - null; - end case; - end Check_Safe_Pointers; - - --------------------------------------- - -- Check_Source_Of_Borrow_Or_Observe -- - --------------------------------------- - - procedure Check_Source_Of_Borrow_Or_Observe - (Expr : Node_Id; - Status : out Error_Status) - is - Root : Entity_Id; - - begin - if Is_Path_Expression (Expr) then - Root := Get_Root_Object (Expr); - else - Root := Empty; - end if; - - Status := OK; - - -- SPARK RM 3.10(3): If the target of an assignment operation is an - -- object of an anonymous access-to-object type (including copy-in for - -- a parameter), then the source shall be a name denoting a part of a - -- stand-alone object, a part of a parameter, or a call to a traversal - -- function. - - if No (Root) then - if Emit_Messages then - if Nkind (Expr) = N_Function_Call then - Error_Msg_N - ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr); - Error_Msg_N - ("\function called must be a traversal function", Expr); - else - Error_Msg_N - ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr); - Error_Msg_N - ("\expression must be part of stand-alone object or " & - "parameter", - Expr); - end if; - end if; - - Status := Error; - end if; - end Check_Source_Of_Borrow_Or_Observe; - - --------------------- - -- Check_Statement -- - --------------------- - - procedure Check_Statement (Stmt : Node_Id) is - begin - case N_Statement_Other_Than_Procedure_Call'(Nkind (Stmt)) is - - -- An entry call is handled like other calls - - when N_Entry_Call_Statement => - Check_Call_Statement (Stmt); - - -- An assignment may correspond to a move, a borrow, or an observe - - when N_Assignment_Statement => - declare - Target : constant Node_Id := Name (Stmt); - - begin - -- Start with checking that the subexpressions of the target - -- path are readable, before possibly updating the permission - -- of these subexpressions in Check_Assignment. - - Check_Expression (Target, Read_Subexpr); - - Check_Assignment (Target => Target, - Expr => Expression (Stmt)); - - -- ??? We need a rule that forbids targets of assignment for - -- which the path is not known, for example when there is a - -- function call involved (which includes calls to traversal - -- functions). Otherwise there is no way to update the - -- corresponding path permission. - - if No (Get_Root_Object - (Target, Through_Traversal => False)) - then - if Emit_Messages then - Error_Msg_N ("illegal target for assignment", Target); - end if; - return; - end if; - - Check_Expression (Target, Assign); - end; - - when N_Block_Statement => - Check_List (Declarations (Stmt)); - Check_Node (Handled_Statement_Sequence (Stmt)); - - -- Remove local borrowers and observers - - declare - Decl : Node_Id := First (Declarations (Stmt)); - Var : Entity_Id; - begin - while Present (Decl) loop - if Nkind (Decl) = N_Object_Declaration then - Var := Defining_Identifier (Decl); - Remove (Current_Borrowers, Var); - Remove (Current_Observers, Var); - end if; - - Next (Decl); - end loop; - end; - - when N_Case_Statement => - declare - Alt : Node_Id; - Saved_Env : Perm_Env; - -- Copy of environment for analysis of the different cases - New_Env : Perm_Env; - -- Accumulator for the different cases - - begin - Check_Expression (Expression (Stmt), Read); - - -- Save environment - - Copy_Env (Current_Perm_Env, Saved_Env); - - -- First alternative - - Alt := First (Alternatives (Stmt)); - Check_List (Statements (Alt)); - Next (Alt); - - -- Cleanup - - Move_Env (Current_Perm_Env, New_Env); - - -- Other alternatives - - while Present (Alt) loop - - -- Restore environment - - Copy_Env (Saved_Env, Current_Perm_Env); - - -- Next alternative - - Check_List (Statements (Alt)); - Next (Alt); - - -- Merge Current_Perm_Env into New_Env - - Merge_Env (Source => Current_Perm_Env, Target => New_Env); - end loop; - - Move_Env (New_Env, Current_Perm_Env); - Free_Env (Saved_Env); - end; - - when N_Delay_Relative_Statement - | N_Delay_Until_Statement - => - Check_Expression (Expression (Stmt), Read); - - when N_Loop_Statement => - Check_Loop_Statement (Stmt); - - when N_Simple_Return_Statement => - declare - Subp : constant Entity_Id := - Return_Applies_To (Return_Statement_Entity (Stmt)); - Expr : constant Node_Id := Expression (Stmt); - begin - if Present (Expression (Stmt)) then - declare - Return_Typ : constant Entity_Id := - Etype (Expression (Stmt)); - - begin - -- SPARK RM 3.10(5): A return statement that applies - -- to a traversal function that has an anonymous - -- access-to-constant (respectively, access-to-variable) - -- result type, shall return either the literal null - -- or an access object denoted by a direct or indirect - -- observer (respectively, borrower) of the traversed - -- parameter. - - if Is_Anonymous_Access_Type (Return_Typ) then - pragma Assert (Is_Traversal_Function (Subp)); - - if Nkind (Expr) /= N_Null then - declare - Expr_Root : constant Entity_Id := - Get_Root_Object (Expr, Is_Traversal => True); - Param : constant Entity_Id := - First_Formal (Subp); - begin - if Param /= Expr_Root and then Emit_Messages then - Error_Msg_NE - ("returned value must be rooted in " - & "traversed parameter & " - & "(SPARK RM 3.10(5))", - Stmt, Param); - end if; - end; - end if; - - -- Move expression to caller - - elsif Is_Deep (Return_Typ) then - - if Is_Path_Expression (Expr) then - Check_Expression (Expr, Move); - - else - if Emit_Messages then - Error_Msg_N - ("expression not allowed as source of move", - Expr); - end if; - return; - end if; - - else - Check_Expression (Expr, Read); - end if; - - if Ekind_In (Subp, E_Procedure, E_Entry) - and then not No_Return (Subp) - then - Return_Parameters (Subp); - Return_Globals (Subp); - end if; - end; - end if; - end; - - when N_Extended_Return_Statement => - declare - Subp : constant Entity_Id := - Return_Applies_To (Return_Statement_Entity (Stmt)); - Decls : constant List_Id := Return_Object_Declarations (Stmt); - Decl : constant Node_Id := Last_Non_Pragma (Decls); - Obj : constant Entity_Id := Defining_Identifier (Decl); - Perm : Perm_Kind; - - begin - -- SPARK RM 3.10(5): return statement of traversal function - - if Is_Traversal_Function (Subp) and then Emit_Messages then - Error_Msg_N - ("extended return cannot apply to a traversal function", - Stmt); - end if; - - Check_List (Return_Object_Declarations (Stmt)); - Check_Node (Handled_Statement_Sequence (Stmt)); - - if Is_Deep (Etype (Obj)) then - Perm := Get_Perm (Obj); - - if Perm /= Read_Write then - Perm_Error (Decl, Read_Write, Perm, - Expl => Get_Expl (Obj)); - end if; - end if; - - if Ekind_In (Subp, E_Procedure, E_Entry) - and then not No_Return (Subp) - then - Return_Parameters (Subp); - Return_Globals (Subp); - end if; - end; - - -- On loop exit, merge the current permission environment 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_Env (Source => Environment_Copy.all, - Target => Saved_Accumulator.all); - -- ??? Either free Environment_Copy, or change the type - -- of loop accumulators to directly store permission - -- environments. - end if; - end; - - -- On branches, analyze each branch independently on a fresh copy of - -- the permission environment, then merge the resulting permission - -- environments. - - when N_If_Statement => - declare - Saved_Env : Perm_Env; - New_Env : Perm_Env; - -- Accumulator for the different branches - - begin - Check_Expression (Condition (Stmt), Read); - - -- Save environment - - Copy_Env (Current_Perm_Env, Saved_Env); - - -- THEN branch - - Check_List (Then_Statements (Stmt)); - Move_Env (Current_Perm_Env, New_Env); - - -- ELSIF branches - - declare - Branch : Node_Id; - begin - Branch := First (Elsif_Parts (Stmt)); - while Present (Branch) loop - - -- Restore current permission environment - - Copy_Env (Saved_Env, Current_Perm_Env); - Check_Expression (Condition (Branch), Read); - Check_List (Then_Statements (Branch)); - - -- Merge current permission environment - - Merge_Env (Source => Current_Perm_Env, Target => New_Env); - Next (Branch); - end loop; - end; - - -- ELSE branch - - -- Restore current permission environment - - Copy_Env (Saved_Env, Current_Perm_Env); - Check_List (Else_Statements (Stmt)); - - -- Merge current permission environment - - Merge_Env (Source => Current_Perm_Env, Target => New_Env); - - -- Cleanup - - Move_Env (New_Env, Current_Perm_Env); - Free_Env (Saved_Env); - end; - - -- We should ideally ignore the branch after raising an exception, - -- so that it is not taken into account in merges. For now, just - -- propagate the current environment. - - when N_Raise_Statement => - null; - - when N_Null_Statement => - null; - - -- 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 - => - 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; - - ------------------------- - -- Check_Type_Legality -- - ------------------------- - - procedure Check_Type_Legality - (Typ : Entity_Id; - Force : Boolean; - Legal : in out Boolean) - is - function Original_Emit_Messages return Boolean renames Emit_Messages; - - function Emit_Messages return Boolean; - -- Local wrapper around generic formal parameter Emit_Messages, to - -- check the value of parameter Force before calling the original - -- Emit_Messages, and setting Legal to False. - - ------------------- - -- Emit_Messages -- - ------------------- - - function Emit_Messages return Boolean is - begin - Legal := False; - return Force and then Original_Emit_Messages; - end Emit_Messages; - - -- Local variables - - Check_Typ : constant Entity_Id := Retysp (Typ); - - -- Start of processing for Check_Type_Legality - - begin - case Type_Kind'(Ekind (Check_Typ)) is - when Access_Kind => - case Access_Kind'(Ekind (Check_Typ)) is - when E_Access_Type - | E_Anonymous_Access_Type - => - null; - when E_Access_Subtype => - Check_Type_Legality (Base_Type (Check_Typ), Force, Legal); - when E_Access_Attribute_Type => - if Emit_Messages then - Error_Msg_N ("access attribute not allowed in SPARK", - Check_Typ); - end if; - when E_Allocator_Type => - if Emit_Messages then - Error_Msg_N ("missing type resolution", Check_Typ); - end if; - when E_General_Access_Type => - if Emit_Messages then - Error_Msg_NE - ("general access type & not allowed in SPARK", - Check_Typ, Check_Typ); - end if; - when Access_Subprogram_Kind => - if Emit_Messages then - Error_Msg_NE - ("access to subprogram type & not allowed in SPARK", - Check_Typ, Check_Typ); - end if; - end case; - - when E_Array_Type - | E_Array_Subtype - => - Check_Type_Legality (Component_Type (Check_Typ), Force, Legal); - - when Record_Kind => - if Is_Deep (Check_Typ) - and then (Is_Tagged_Type (Check_Typ) - or else Is_Class_Wide_Type (Check_Typ)) - then - if Emit_Messages then - Error_Msg_NE - ("tagged type & cannot be owning in SPARK", - Check_Typ, Check_Typ); - end if; - - else - declare - Comp : Entity_Id; - begin - Comp := First_Component_Or_Discriminant (Check_Typ); - while Present (Comp) loop - - -- Ignore components which are not visible in SPARK - - if Component_Is_Visible_In_SPARK (Comp) then - Check_Type_Legality (Etype (Comp), Force, Legal); - end if; - Next_Component_Or_Discriminant (Comp); - end loop; - end; - end if; - - when Scalar_Kind - | E_String_Literal_Subtype - | Protected_Kind - | Task_Kind - | Incomplete_Kind - | E_Exception_Type - | E_Subprogram_Type - => - null; - - -- Do not check type whose full view is not SPARK - - when E_Private_Type - | E_Private_Subtype - | E_Limited_Private_Type - | E_Limited_Private_Subtype - => - null; - end case; - end Check_Type_Legality; - - -------------- - -- Get_Expl -- - -------------- - - function Get_Expl (N : Node_Or_Entity_Id) return Node_Id is - begin - -- Special case for the object declared in an extended return statement - - if Nkind (N) = N_Defining_Identifier then - declare - C : constant Perm_Tree_Access := - Get (Current_Perm_Env, Unique_Entity (N)); - begin - pragma Assert (C /= null); - return Explanation (C); - end; - - -- The expression is a call to a traversal function - - elsif Is_Traversal_Function_Call (N) then - return N; - - -- The expression is directly rooted in an object - - elsif Present (Get_Root_Object (N, Through_Traversal => False)) then - declare - 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.Explanation; - - when Unfolded => - pragma Assert (Tree_Or_Perm.Tree_Access /= null); - return Explanation (Tree_Or_Perm.Tree_Access); - end case; - end; - - -- The expression is a function call, an allocation, or null - - else - return N; - end if; - end Get_Expl; - - ----------------------------------- - -- Get_Observed_Or_Borrowed_Expr -- - ----------------------------------- - - function Get_Observed_Or_Borrowed_Expr (Expr : Node_Id) return Node_Id is - - function Find_Func_Call (Expr : Node_Id) return Node_Id; - -- Search for function calls in the prefixes of Expr - - -------------------- - -- Find_Func_Call -- - -------------------- - - function Find_Func_Call (Expr : Node_Id) return Node_Id is - begin - case Nkind (Expr) is - when N_Expanded_Name - | N_Identifier - => - return Empty; - - when N_Explicit_Dereference - | N_Indexed_Component - | N_Selected_Component - | N_Slice - => - return Find_Func_Call (Prefix (Expr)); - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - return Find_Func_Call (Expression (Expr)); - - when N_Function_Call => - return Expr; - - when others => - raise Program_Error; - end case; - end Find_Func_Call; - - B_Expr : Node_Id := Expr; - - begin - -- Search for the first call to a traversal function in Expr. If there - -- is one, its first parameter is the borrowed expression. Otherwise, - -- it is Expr. - - loop - declare - Call : constant Node_Id := Find_Func_Call (B_Expr); - begin - exit when No (Call); - pragma Assert (Is_Traversal_Function_Call (Call)); - B_Expr := First_Actual (Call); - end; - end loop; - - return B_Expr; - end Get_Observed_Or_Borrowed_Expr; - - -------------- - -- Get_Perm -- - -------------- - - function Get_Perm (N : Node_Or_Entity_Id) return Perm_Kind is - begin - -- Special case for the object declared in an extended return statement - - if Nkind (N) = N_Defining_Identifier then - declare - C : constant Perm_Tree_Access := - Get (Current_Perm_Env, Unique_Entity (N)); - begin - pragma Assert (C /= null); - return Permission (C); - end; - - -- The expression is a call to a traversal function - - elsif Is_Traversal_Function_Call (N) then - declare - Callee : constant Entity_Id := Get_Called_Entity (N); - begin - if Is_Access_Constant (Etype (Callee)) then - return Read_Only; - else - return Read_Write; - end if; - end; - - -- The expression is directly rooted in an object - - elsif Present (Get_Root_Object (N, Through_Traversal => False)) then - declare - 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); - end case; - end; - - -- The expression is a function call, an allocation, or null - - else - return Read_Write; - end if; - 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 - - when N_Expanded_Name - | N_Identifier - => - declare - C : constant Perm_Tree_Access := - Get (Current_Perm_Env, Unique_Entity (Entity (N))); - begin - -- Except during elaboration, the root object should have been - -- declared and entered into the current permission - -- environment. - - if not Inside_Elaboration - and then C = null - then - Illegal_Global_Usage (N, N); - end if; - - return (R => Unfolded, Tree_Access => C); - end; - - -- For a nonterminal path, we get the permission tree of its - -- prefix, and then get the subtree associated with the extension, - -- if unfolded. If folded, we return the permission associated with - -- children. - - when N_Explicit_Dereference - | N_Indexed_Component - | N_Selected_Component - | N_Slice - => - declare - C : constant Perm_Or_Tree := Get_Perm_Or_Tree (Prefix (N)); - begin - case C.R is - - -- Some earlier prefix was already folded, return the - -- permission found. - - when Folded => - return C; - - when Unfolded => - case Kind (C.Tree_Access) is - - -- If the prefix tree is already folded, return the - -- children permission. - - when Entire_Object => - return (R => Folded, - Found_Permission => - Children_Permission (C.Tree_Access), - Explanation => - Explanation (C.Tree_Access)); - - when Reference => - pragma Assert (Nkind (N) = N_Explicit_Dereference); - return (R => Unfolded, - Tree_Access => Get_All (C.Tree_Access)); - - when Record_Component => - pragma Assert (Nkind (N) = N_Selected_Component); - declare - Comp : constant Entity_Id := - Original_Record_Component - (Entity (Selector_Name (N))); - D : constant Perm_Tree_Access := - Perm_Tree_Maps.Get - (Component (C.Tree_Access), Comp); - begin - pragma Assert (D /= null); - return (R => Unfolded, - Tree_Access => D); - end; - - when Array_Component => - pragma Assert (Nkind (N) = N_Indexed_Component - or else - Nkind (N) = N_Slice); - pragma Assert (Get_Elem (C.Tree_Access) /= null); - return (R => Unfolded, - Tree_Access => Get_Elem (C.Tree_Access)); - end case; - end case; - end; - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - return Get_Perm_Or_Tree (Expression (N)); - - 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 - return Set_Perm_Prefixes (N, None, Empty); - end Get_Perm_Tree; - - --------------------- - -- Get_Root_Object -- - --------------------- - - function Get_Root_Object - (Expr : Node_Id; - Through_Traversal : Boolean := True; - Is_Traversal : Boolean := False) return Entity_Id - is - function GRO (Expr : Node_Id) return Entity_Id; - -- Local wrapper on the actual function, to propagate the values of - -- optional parameters. - - --------- - -- GRO -- - --------- - - function GRO (Expr : Node_Id) return Entity_Id is - begin - return Get_Root_Object (Expr, Through_Traversal, Is_Traversal); - end GRO; - - Get_Root_Object : Boolean; - pragma Unmodified (Get_Root_Object); - -- Local variable to mask the name of function Get_Root_Object, to - -- prevent direct call. Instead GRO wrapper should be called. - - -- Start of processing for Get_Root_Object - - begin - if not Is_Subpath_Expression (Expr, Is_Traversal) then - if Emit_Messages then - Error_Msg_N ("name expected here for path", Expr); - end if; - return Empty; - end if; - - case Nkind (Expr) is - when N_Expanded_Name - | N_Identifier - => - return Entity (Expr); - - when N_Explicit_Dereference - | N_Indexed_Component - | N_Selected_Component - | N_Slice - => - return GRO (Prefix (Expr)); - - -- There is no root object for an (extension) aggregate, allocator, - -- concat, or NULL. - - when N_Aggregate - | N_Allocator - | N_Extension_Aggregate - | N_Null - | N_Op_Concat - => - return Empty; - - -- In the case of a call to a traversal function, the root object is - -- the root of the traversed parameter. Otherwise there is no root - -- object. - - when N_Function_Call => - if Through_Traversal - and then Is_Traversal_Function_Call (Expr) - then - return GRO (First_Actual (Expr)); - else - return Empty; - end if; - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - return GRO (Expression (Expr)); - - when N_Attribute_Reference => - pragma Assert - (Get_Attribute_Id (Attribute_Name (Expr)) = - Attribute_Loop_Entry - or else - Get_Attribute_Id (Attribute_Name (Expr)) = - Attribute_Update - or else Get_Attribute_Id (Attribute_Name (Expr)) = - Attribute_Image); - return Empty; - - when N_If_Expression => - if Is_Traversal then - declare - Cond : constant Node_Id := First (Expressions (Expr)); - Then_Part : constant Node_Id := Next (Cond); - Else_Part : constant Node_Id := Next (Then_Part); - Then_Root : constant Entity_Id := GRO (Then_Part); - Else_Root : constant Entity_Id := GRO (Else_Part); - begin - if Nkind (Then_Part) = N_Null then - return Else_Root; - elsif Nkind (Else_Part) = N_Null then - return Then_Part; - elsif Then_Root = Else_Root then - return Then_Root; - else - if Emit_Messages then - Error_Msg_N - ("same name expected here in each branch", Expr); - end if; - return Empty; - end if; - end; - else - if Emit_Messages then - Error_Msg_N ("name expected here for path", Expr); - end if; - return Empty; - end if; - - when N_Case_Expression => - if Is_Traversal then - declare - Cases : constant List_Id := Alternatives (Expr); - Cur_Case : Node_Id := First (Cases); - Cur_Root : Entity_Id; - Common_Root : Entity_Id := Empty; - - begin - while Present (Cur_Case) loop - Cur_Root := GRO (Expression (Cur_Case)); - - if Common_Root = Empty then - Common_Root := Cur_Root; - elsif Common_Root /= Cur_Root then - if Emit_Messages then - Error_Msg_N - ("same name expected here in each branch", Expr); - end if; - return Empty; - end if; - Next (Cur_Case); - end loop; - - return Common_Root; - end; - else - if Emit_Messages then - Error_Msg_N ("name expected here for path", Expr); - end if; - return Empty; - end if; - - when others => - raise Program_Error; - end case; - end Get_Root_Object; - - --------- - -- 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_Array_Component -- - ------------------------- - - function Has_Array_Component (Expr : Node_Id) return Boolean is - begin - case Nkind (Expr) is - when N_Expanded_Name - | N_Identifier - => - return False; - - when N_Explicit_Dereference - | N_Selected_Component - => - return Has_Array_Component (Prefix (Expr)); - - when N_Indexed_Component - | N_Slice - => - return True; - - when N_Allocator - | N_Null - | N_Function_Call - => - return False; - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - return Has_Array_Component (Expression (Expr)); - - when others => - raise Program_Error; - end case; - end Has_Array_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; E : Entity_Id) - is - begin - Error_Msg_NE ("cannot use global variable & of deep type", N, E); - 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_Deep -- - ------------- - - function Is_Deep (Typ : Entity_Id) return Boolean is - begin - case Type_Kind'(Ekind (Retysp (Typ))) is - when Access_Kind => - return True; - - when E_Array_Type - | E_Array_Subtype - => - return Is_Deep (Component_Type (Retysp (Typ))); - - when Record_Kind => - declare - Comp : Entity_Id; - begin - Comp := First_Component_Or_Discriminant (Retysp (Typ)); - while Present (Comp) loop - - -- Ignore components not visible in SPARK - - if Component_Is_Visible_In_SPARK (Comp) - and then Is_Deep (Etype (Comp)) - then - return True; - end if; - Next_Component_Or_Discriminant (Comp); - end loop; - end; - return False; - - when Scalar_Kind - | E_String_Literal_Subtype - | Protected_Kind - | Task_Kind - | Incomplete_Kind - | E_Exception_Type - | E_Subprogram_Type - => - return False; - - -- Ignore full view of types if it is not in SPARK - - when E_Private_Type - | E_Private_Subtype - | E_Limited_Private_Type - | E_Limited_Private_Subtype - => - return False; - end case; - end Is_Deep; - - -------------- - -- Is_Legal -- - -------------- - - function Is_Legal (N : Node_Id) return Boolean is - Legal : Boolean := True; - - begin - case Nkind (N) is - when N_Declaration => - Check_Declaration_Legality (N, Force => False, Legal => Legal); - when others => - null; - end case; - - return Legal; - end Is_Legal; - - ---------------------- - -- Is_Local_Context -- - ---------------------- - - function Is_Local_Context (Scop : Entity_Id) return Boolean is - begin - return Is_Subprogram_Or_Entry (Scop) - or else Ekind (Scop) = E_Block; - end Is_Local_Context; - - ------------------------ - -- Is_Path_Expression -- - ------------------------ - - function Is_Path_Expression - (Expr : Node_Id; - Is_Traversal : Boolean := False) return Boolean - is - function IPE (Expr : Node_Id) return Boolean; - -- Local wrapper on the actual function, to propagate the values of - -- optional parameter Is_Traversal. - - --------- - -- IPE -- - --------- - - function IPE (Expr : Node_Id) return Boolean is - begin - return Is_Path_Expression (Expr, Is_Traversal); - end IPE; - - Is_Path_Expression : Boolean; - pragma Unmodified (Is_Path_Expression); - -- Local variable to mask the name of function Is_Path_Expression, to - -- prevent direct call. Instead IPE wrapper should be called. - - -- Start of processing for Is_Path_Expression - - begin - case Nkind (Expr) is - when N_Expanded_Name - | N_Explicit_Dereference - | N_Identifier - | N_Indexed_Component - | N_Selected_Component - | N_Slice - => - return True; - - -- Special value NULL corresponds to an empty path - - when N_Null => - return True; - - -- Object returned by an (extension) aggregate, an allocator, or - -- a function call corresponds to a path. - - when N_Aggregate - | N_Allocator - | N_Extension_Aggregate - | N_Function_Call - => - return True; - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - return IPE (Expression (Expr)); - - -- When returning from a traversal function, consider an - -- if-expression as a possible path expression. - - when N_If_Expression => - if Is_Traversal then - declare - Cond : constant Node_Id := First (Expressions (Expr)); - Then_Part : constant Node_Id := Next (Cond); - Else_Part : constant Node_Id := Next (Then_Part); - begin - return IPE (Then_Part) - and then IPE (Else_Part); - end; - else - return False; - end if; - - -- When returning from a traversal function, consider - -- a case-expression as a possible path expression. - - when N_Case_Expression => - if Is_Traversal then - declare - Cases : constant List_Id := Alternatives (Expr); - Cur_Case : Node_Id := First (Cases); - - begin - while Present (Cur_Case) loop - if not IPE (Expression (Cur_Case)) then - return False; - end if; - Next (Cur_Case); - end loop; - - return True; - end; - else - return False; - end if; - - when others => - return False; - end case; - end Is_Path_Expression; - - ------------------------- - -- Is_Prefix_Or_Almost -- - ------------------------- - - function Is_Prefix_Or_Almost (Pref, Expr : Node_Id) return Boolean is - - type Expr_Array is array (Positive range <>) of Node_Id; - -- Sequence of expressions that make up a path - - function Get_Expr_Array (Expr : Node_Id) return Expr_Array; - pragma Precondition (Is_Path_Expression (Expr)); - -- Return the sequence of expressions that make up a path - - -------------------- - -- Get_Expr_Array -- - -------------------- - - function Get_Expr_Array (Expr : Node_Id) return Expr_Array is - begin - case Nkind (Expr) is - when N_Expanded_Name - | N_Identifier - => - return Expr_Array'(1 => Expr); - - when N_Explicit_Dereference - | N_Indexed_Component - | N_Selected_Component - | N_Slice - => - return Get_Expr_Array (Prefix (Expr)) & Expr; - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - return Get_Expr_Array (Expression (Expr)); - - when others => - raise Program_Error; - end case; - end Get_Expr_Array; - - -- Local variables - - Prefix_Path : constant Expr_Array := Get_Expr_Array (Pref); - Expr_Path : constant Expr_Array := Get_Expr_Array (Expr); - - Prefix_Root : constant Node_Id := Prefix_Path (1); - Expr_Root : constant Node_Id := Expr_Path (1); - - Common_Len : constant Positive := - Positive'Min (Prefix_Path'Length, Expr_Path'Length); - - -- Start of processing for Is_Prefix_Or_Almost - - begin - if Entity (Prefix_Root) /= Entity (Expr_Root) then - return False; - end if; - - for J in 2 .. Common_Len loop - declare - Prefix_Elt : constant Node_Id := Prefix_Path (J); - Expr_Elt : constant Node_Id := Expr_Path (J); - begin - case Nkind (Prefix_Elt) is - when N_Explicit_Dereference => - if Nkind (Expr_Elt) /= N_Explicit_Dereference then - return False; - end if; - - when N_Selected_Component => - if Nkind (Expr_Elt) /= N_Selected_Component - or else Original_Record_Component - (Entity (Selector_Name (Prefix_Elt))) - /= Original_Record_Component - (Entity (Selector_Name (Expr_Elt))) - then - return False; - end if; - - when N_Indexed_Component - | N_Slice - => - if not Nkind_In (Expr_Elt, N_Indexed_Component, N_Slice) then - return False; - end if; - - when others => - raise Program_Error; - end case; - end; - end loop; - - -- If the expression path is longer than the prefix one, then at this - -- point the prefix property holds. - - if Expr_Path'Length > Prefix_Path'Length then - return True; - - -- Otherwise check if none of the remaining path elements in the - -- candidate prefix involve a dereference. - - else - for J in Common_Len + 1 .. Prefix_Path'Length loop - if Nkind (Prefix_Path (J)) = N_Explicit_Dereference then - return False; - end if; - end loop; - - return True; - end if; - end Is_Prefix_Or_Almost; - - --------------------------- - -- Is_Subpath_Expression -- - --------------------------- - - function Is_Subpath_Expression - (Expr : Node_Id; - Is_Traversal : Boolean := False) return Boolean - is - begin - return Is_Path_Expression (Expr, Is_Traversal) - - or else (Nkind_In (Expr, N_Qualified_Expression, - N_Type_Conversion, - N_Unchecked_Type_Conversion) - and then Is_Subpath_Expression (Expression (Expr))) - - or else (Nkind (Expr) = N_Attribute_Reference - and then - (Get_Attribute_Id (Attribute_Name (Expr)) = - Attribute_Update - or else - Get_Attribute_Id (Attribute_Name (Expr)) = - Attribute_Loop_Entry - or else - Get_Attribute_Id (Attribute_Name (Expr)) = - Attribute_Image)) - - or else Nkind (Expr) = N_Op_Concat; - end Is_Subpath_Expression; - - --------------------------- - -- Is_Traversal_Function -- - --------------------------- - - function Is_Traversal_Function (E : Entity_Id) return Boolean is - begin - return Ekind (E) = E_Function - - -- A function is said to be a traversal function if the result type of - -- the function is an anonymous access-to-object type, - - and then Is_Anonymous_Access_Type (Etype (E)) - - -- the function has at least one formal parameter, - - and then Present (First_Formal (E)) - - -- and the function's first parameter is of an access type. - - and then Is_Access_Type (Retysp (Etype (First_Formal (E)))); - end Is_Traversal_Function; - - -------------------------------- - -- Is_Traversal_Function_Call -- - -------------------------------- - - function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean is - begin - return Nkind (Expr) = N_Function_Call - and then Present (Get_Called_Entity (Expr)) - and then Is_Traversal_Function (Get_Called_Entity (Expr)); - end Is_Traversal_Function_Call; - - ------------------ - -- 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_Env -- - --------------- - - procedure Merge_Env (Source : in out Perm_Env; Target : in out Perm_Env) is - - -- Local subprograms - - procedure Apply_Glb_Tree - (A : Perm_Tree_Access; - P : Perm_Kind); - - procedure Merge_Trees - (Target : Perm_Tree_Access; - Source : Perm_Tree_Access); - - -------------------- - -- Apply_Glb_Tree -- - -------------------- - - 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; - end; - end case; - end Apply_Glb_Tree; - - ----------------- - -- Merge_Trees -- - ----------------- - - procedure Merge_Trees - (Target : Perm_Tree_Access; - Source : Perm_Tree_Access) - is - 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; - 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; - 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; - end; - - when others => - raise Program_Error; - end case; - end case; - end Merge_Trees; - - -- Local variables - - CompTarget : Perm_Tree_Access; - CompSource : Perm_Tree_Access; - KeyTarget : Perm_Tree_Maps.Key_Option; - - -- Start of processing for Merge_Env - - 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_Env; - - ---------------- - -- Perm_Error -- - ---------------- - - procedure Perm_Error - (N : Node_Id; - Perm : Perm_Kind; - Found_Perm : Perm_Kind; - Expl : Node_Id; - Forbidden_Perm : Boolean := False) - 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 Emit_Messages then - 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 (N, Perm, Found_Perm, Expl, Forbidden_Perm); - end if; - 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; - Expl : Node_Id) - is - begin - if Emit_Messages then - Error_Msg_Node_2 := Subp; - Error_Msg_NE ("insufficient permission for & when returning from &", - Subp, E); - Perm_Mismatch (Subp, Perm, Found_Perm, Expl); - end if; - end Perm_Error_Subprogram_End; - - ------------------ - -- Process_Path -- - ------------------ - - procedure Process_Path (Expr : Node_Id; Mode : Checking_Mode) is - - procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id); - -- Check expression Expr originating in Root was not borrowed - - procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id); - -- Check expression Expr originating in Root was not observed - - ------------------------ - -- Check_Not_Borrowed -- - ------------------------ - - procedure Check_Not_Borrowed (Expr : Node_Id; Root : Entity_Id) is - begin - -- An expression without root object cannot be borrowed - - if No (Root) then - return; - end if; - - -- Otherwise, try to match the expression with one of the borrowed - -- expressions. - - declare - Key : Variable_Maps.Key_Option := - Get_First_Key (Current_Borrowers); - Var : Entity_Id; - Borrowed : Node_Id; - B_Pledge : Entity_Id := Empty; - - begin - -- Search for a call to a pledge function or a global pragma in - -- the parents of Expr. - - declare - Call : Node_Id := Expr; - begin - while Present (Call) - and then - (Nkind (Call) /= N_Function_Call - or else not Is_Pledge_Function (Get_Called_Entity (Call))) - loop - -- Do not check for borrowed objects in global contracts - -- ??? However we should keep these objects in the borrowed - -- state when verifying the subprogram so that we can make - -- sure that they are only read inside pledges. - -- ??? There is probably a better way to disable checking of - -- borrows inside global contracts. - - if Nkind (Call) = N_Pragma - and then Get_Pragma_Id (Pragma_Name (Call)) = Pragma_Global - then - return; - end if; - - Call := Parent (Call); - end loop; - - if Present (Call) - and then Nkind (First_Actual (Call)) in N_Has_Entity - then - B_Pledge := Entity (First_Actual (Call)); - end if; - end; - - while Key.Present loop - Var := Key.K; - Borrowed := Get (Current_Borrowers, Var); - - if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr) - and then Var /= B_Pledge - and then Emit_Messages - then - Error_Msg_Sloc := Sloc (Borrowed); - Error_Msg_N ("object was borrowed #", Expr); - end if; - - Key := Get_Next_Key (Current_Borrowers); - end loop; - end; - end Check_Not_Borrowed; - - ------------------------ - -- Check_Not_Observed -- - ------------------------ - - procedure Check_Not_Observed (Expr : Node_Id; Root : Entity_Id) is - begin - -- An expression without root object cannot be observed - - if No (Root) then - return; - end if; - - -- Otherwise, try to match the expression with one of the observed - -- expressions. - - declare - Key : Variable_Maps.Key_Option := - Get_First_Key (Current_Observers); - Var : Entity_Id; - Observed : Node_Id; - - begin - while Key.Present loop - Var := Key.K; - Observed := Get (Current_Observers, Var); - - if Is_Prefix_Or_Almost (Pref => Observed, Expr => Expr) - and then Emit_Messages - then - Error_Msg_Sloc := Sloc (Observed); - Error_Msg_N ("object was observed #", Expr); - end if; - - Key := Get_Next_Key (Current_Observers); - end loop; - end; - end Check_Not_Observed; - - -- Local variables - - Expr_Type : constant Entity_Id := Etype (Expr); - Root : Entity_Id := Get_Root_Object (Expr); - Perm : Perm_Kind_Option; - - -- Start of processing for Process_Path - - begin - -- Nothing to do if the root type is not deep, or the path is not rooted - -- in an object. - - if not Present (Root) - or else not Is_Object (Root) - or else not Is_Deep (Etype (Root)) - then - return; - end if; - - -- Identify the root type for the path - - Root := Unique_Entity (Root); - - -- Except during elaboration, the root object should have been declared - -- and entered into the current permission environment. - - if not Inside_Elaboration - and then Get (Current_Perm_Env, Root) = null - then - Illegal_Global_Usage (Expr, Root); - end if; - - -- During elaboration, only the validity of operations is checked, no - -- need to compute the permission of Expr. - - if Inside_Elaboration then - Perm := None; - else - Perm := Get_Perm (Expr); - end if; - - -- Check permissions - - case Mode is - - when Read => - - -- No checking needed during elaboration - - if Inside_Elaboration then - return; - end if; - - -- Check path is readable - - if Perm not in Read_Perm then - Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr)); - return; - end if; - - when Move => - - -- Forbidden on deep path during elaboration, otherwise no - -- checking needed. - - if Inside_Elaboration then - if Is_Deep (Expr_Type) - and then not Inside_Procedure_Call - and then Present (Get_Root_Object (Expr)) - and then Emit_Messages - then - Error_Msg_N ("illegal move during elaboration", Expr); - end if; - - return; - end if; - - -- For deep path, check RW permission, otherwise R permission - - if not Is_Deep (Expr_Type) then - if Perm not in Read_Perm then - Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr)); - end if; - return; - end if; - - -- SPARK RM 3.10(1): At the point of a move operation the state of - -- the source object (if any) shall be Unrestricted. - - if Perm /= Read_Write then - Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr)); - return; - end if; - - when Assign => - - -- No checking needed during elaboration - - if Inside_Elaboration then - return; - end if; - - -- For assignment, check W permission - - if Perm not in Write_Perm then - Perm_Error (Expr, Write_Only, Perm, Expl => Get_Expl (Expr)); - return; - end if; - - when Borrow => - - -- Forbidden during elaboration, an error is already issued in - -- Check_Declaration, just return. - - if Inside_Elaboration then - return; - end if; - - -- For borrowing, check RW permission - - if Perm /= Read_Write then - Perm_Error (Expr, Read_Write, Perm, Expl => Get_Expl (Expr)); - return; - end if; - - when Observe => - - -- Forbidden during elaboration, an error is already issued in - -- Check_Declaration, just return. - - if Inside_Elaboration then - return; - end if; - - -- For borrowing, check R permission - - if Perm not in Read_Perm then - Perm_Error (Expr, Read_Only, Perm, Expl => Get_Expl (Expr)); - return; - end if; - end case; - - -- Check path was not borrowed - - Check_Not_Borrowed (Expr, Root); - - -- For modes that require W permission, check path was not observed - - case Mode is - when Read | Observe => - null; - when Assign | Move | Borrow => - Check_Not_Observed (Expr, Root); - end case; - - -- Do not update permission environment when handling calls - - if Inside_Procedure_Call then - return; - end if; - - -- Update the permissions - - case Mode is - - when Read => - null; - - when Move => - - -- SPARK RM 3.10(1): After a move operation, the state of the - -- source object (if any) becomes Moved. - - if Present (Get_Root_Object (Expr)) then - declare - Tree : constant Perm_Tree_Access := - Set_Perm_Prefixes (Expr, Write_Only, Expl => Expr); - begin - pragma Assert (Tree /= null); - Set_Perm_Extensions_Move (Tree, Etype (Expr), Expl => Expr); - end; - end if; - - when Assign => - - -- If there is no root object, or the tree has an array component, - -- then the permissions do not get modified by the assignment. - - if No (Get_Root_Object (Expr)) - or else Has_Array_Component (Expr) - then - return; - end if; - - -- Set permission RW for the path and its extensions - - declare - Tree : constant Perm_Tree_Access := Get_Perm_Tree (Expr); - begin - Tree.all.Tree.Permission := Read_Write; - Set_Perm_Extensions (Tree, Read_Write, Expl => Expr); - - -- Normalize the permission tree - - Set_Perm_Prefixes_Assign (Expr); - end; - - -- Borrowing and observing of paths is handled by the variables - -- Current_Borrowers and Current_Observers. - - when Borrow | Observe => - null; - end case; - end Process_Path; - - -------------------- - -- Return_Globals -- - -------------------- - - procedure Return_Globals (Subp : Entity_Id) is - - procedure Return_Global - (Expr : Node_Id; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean); - -- Proxy procedure to return globals, to adjust for the type of first - -- parameter expected by Return_Parameter_Or_Global. - - ------------------- - -- Return_Global -- - ------------------- - - procedure Return_Global - (Expr : Node_Id; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean) - is - begin - Return_Parameter_Or_Global - (Id => Entity (Expr), - Typ => Typ, - Kind => Kind, - Subp => Subp, - Global_Var => Global_Var); - end Return_Global; - - procedure Return_Globals_Inst is new Handle_Globals (Return_Global); - - -- Start of processing for Return_Globals - - begin - Return_Globals_Inst (Subp); - end Return_Globals; - - -------------------------------- - -- Return_Parameter_Or_Global -- - -------------------------------- - - procedure Return_Parameter_Or_Global - (Id : Entity_Id; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean) - is - begin - -- Shallow parameters and globals need not be considered - - if not Is_Deep (Typ) then - return; - - elsif Kind = E_In_Parameter then - - -- Input global variables are observed only - - if Global_Var then - return; - - -- Anonymous access to constant is an observe - - elsif Is_Anonymous_Access_Type (Typ) - and then Is_Access_Constant (Typ) - then - return; - - -- Deep types other than access types define an observe - - elsif not Is_Access_Type (Typ) then - return; - end if; - end if; - - -- All other parameters and globals should return with mode RW to the - -- caller. - - declare - Tree : constant Perm_Tree_Access := Get (Current_Perm_Env, Id); - begin - if Permission (Tree) /= Read_Write then - Perm_Error_Subprogram_End - (E => Id, - Subp => Subp, - Perm => Read_Write, - Found_Perm => Permission (Tree), - Expl => Explanation (Tree)); - end if; - end; - 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 - (Id => Formal, - Typ => Retysp (Etype (Formal)), - Kind => Ekind (Formal), - Subp => Subp, - Global_Var => False); - Next_Formal (Formal); - end loop; - end Return_Parameters; - - ------------------------- - -- Set_Perm_Extensions -- - ------------------------- - - procedure Set_Perm_Extensions - (T : Perm_Tree_Access; - P : Perm_Kind; - Expl : Node_Id) is - - procedure Free_Perm_Tree_Children (T : Perm_Tree_Access); - -- Free the permission tree of children if any, prio to replacing T - - ----------------------------- - -- Free_Perm_Tree_Children -- - ----------------------------- - - procedure Free_Perm_Tree_Children (T : Perm_Tree_Access) is - begin - case Kind (T) is - when Entire_Object => - null; - - when Reference => - Free_Tree (T.all.Tree.Get_All); - - when Array_Component => - Free_Tree (T.all.Tree.Get_Elem); - - when Record_Component => - declare - Hashtbl : Perm_Tree_Maps.Instance := Component (T); - Comp : Perm_Tree_Access; - - begin - Comp := Perm_Tree_Maps.Get_First (Hashtbl); - while Comp /= null loop - Free_Tree (Comp); - Comp := Perm_Tree_Maps.Get_Next (Hashtbl); - end loop; - - Perm_Tree_Maps.Reset (Hashtbl); - end; - end case; - end Free_Perm_Tree_Children; - - -- Start of processing for Set_Perm_Extensions - - begin - Free_Perm_Tree_Children (T); - T.all.Tree := Perm_Tree'(Kind => Entire_Object, - Is_Node_Deep => Is_Node_Deep (T), - Explanation => Expl, - Permission => Permission (T), - Children_Permission => P); - end Set_Perm_Extensions; - - ------------------------------ - -- Set_Perm_Extensions_Move -- - ------------------------------ - - procedure Set_Perm_Extensions_Move - (T : Perm_Tree_Access; - E : Entity_Id; - Expl : Node_Id) - is - Check_Ty : constant Entity_Id := Retysp (E); - begin - -- Shallow extensions are set to RW - - if not Is_Node_Deep (T) then - Set_Perm_Extensions (T, Read_Write, Expl => Expl); - return; - end if; - - -- Deep extensions are set to W before .all and NO afterwards - - T.all.Tree.Permission := Write_Only; - - case T.all.Tree.Kind is - - -- For a folded tree of composite type, unfold the tree for better - -- precision. - - when Entire_Object => - case Ekind (Check_Ty) is - when E_Array_Type - | E_Array_Subtype - => - declare - C : constant Perm_Tree_Access := - new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Node_Deep (T), - Explanation => Expl, - Permission => Read_Write, - Children_Permission => Read_Write)); - begin - Set_Perm_Extensions_Move - (C, Component_Type (Check_Ty), Expl); - T.all.Tree := (Kind => Array_Component, - Is_Node_Deep => Is_Node_Deep (T), - Explanation => Expl, - Permission => Write_Only, - Get_Elem => C); - end; - - when Record_Kind => - declare - C : Perm_Tree_Access; - Comp : Entity_Id; - Hashtbl : Perm_Tree_Maps.Instance; - - begin - Comp := First_Component_Or_Discriminant (Check_Ty); - while Present (Comp) loop - - -- Unfold components which are visible in SPARK - - if Component_Is_Visible_In_SPARK (Comp) then - C := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Deep (Etype (Comp)), - Explanation => Expl, - Permission => Read_Write, - Children_Permission => Read_Write)); - Set_Perm_Extensions_Move (C, Etype (Comp), Expl); - - -- Hidden components are never deep - - else - C := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => False, - Explanation => Expl, - Permission => Read_Write, - Children_Permission => Read_Write)); - Set_Perm_Extensions (C, Read_Write, Expl => Expl); - end if; - - Perm_Tree_Maps.Set - (Hashtbl, Original_Record_Component (Comp), C); - Next_Component_Or_Discriminant (Comp); - end loop; - - T.all.Tree := - (Kind => Record_Component, - Is_Node_Deep => Is_Node_Deep (T), - Explanation => Expl, - Permission => Write_Only, - Component => Hashtbl); - end; - - -- Otherwise, extensions are set to NO - - when others => - Set_Perm_Extensions (T, No_Access, Expl); - end case; - - when Reference => - Set_Perm_Extensions (T, No_Access, Expl); - - when Array_Component => - Set_Perm_Extensions_Move - (Get_Elem (T), Component_Type (Check_Ty), Expl); - - when Record_Component => - declare - C : Perm_Tree_Access; - Comp : Entity_Id; - - begin - Comp := First_Component_Or_Discriminant (Check_Ty); - while Present (Comp) loop - C := Perm_Tree_Maps.Get - (Component (T), Original_Record_Component (Comp)); - pragma Assert (C /= null); - - -- Move visible components - - if Component_Is_Visible_In_SPARK (Comp) then - Set_Perm_Extensions_Move (C, Etype (Comp), Expl); - - -- Hidden components are never deep - - else - Set_Perm_Extensions (C, Read_Write, Expl => Expl); - end if; - - Next_Component_Or_Discriminant (Comp); - end loop; - end; - end case; - end Set_Perm_Extensions_Move; - - ----------------------- - -- Set_Perm_Prefixes -- - ----------------------- - - function Set_Perm_Prefixes - (N : Node_Id; - Perm : Perm_Kind_Option; - Expl : Node_Id) return Perm_Tree_Access - is - begin - case Nkind (N) is - when N_Expanded_Name - | N_Identifier - => - declare - E : constant Entity_Id := Unique_Entity (Entity (N)); - C : constant Perm_Tree_Access := Get (Current_Perm_Env, E); - pragma Assert (C /= null); - - begin - if Perm /= None then - C.all.Tree.Permission := Glb (Perm, Permission (C)); - end if; - - return C; - end; - - -- For a nonterminal path, 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 one level. - - when N_Explicit_Dereference => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes (Prefix (N), Perm, Expl); - pragma Assert (C /= null); - pragma Assert (Kind (C) = Entire_Object - or else Kind (C) = Reference); - begin - -- The tree is already unfolded. Replace the permission of the - -- dereference. - - if Kind (C) = Reference then - declare - D : constant Perm_Tree_Access := Get_All (C); - pragma Assert (D /= null); - - begin - if Perm /= None then - D.all.Tree.Permission := Glb (Perm, Permission (D)); - end if; - - return D; - end; - - -- The tree is folded. Expand it. - - else - declare - pragma Assert (Kind (C) = Entire_Object); - - Child_P : constant Perm_Kind := Children_Permission (C); - D : constant Perm_Tree_Access := - new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Deep (Etype (N)), - Explanation => Expl, - Permission => Child_P, - Children_Permission => Child_P)); - begin - if Perm /= None then - D.all.Tree.Permission := Perm; - end if; - - C.all.Tree := (Kind => Reference, - Is_Node_Deep => Is_Node_Deep (C), - Explanation => Expl, - Permission => Permission (C), - Get_All => D); - return D; - end; - end if; - end; - - when N_Selected_Component => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes (Prefix (N), Perm, Expl); - pragma Assert (C /= null); - pragma Assert (Kind (C) = Entire_Object - or else Kind (C) = Record_Component); - begin - -- The tree is already unfolded. Replace the permission of the - -- component. - - if Kind (C) = Record_Component then - declare - Comp : constant Entity_Id := - Original_Record_Component - (Entity (Selector_Name (N))); - D : constant Perm_Tree_Access := - Perm_Tree_Maps.Get (Component (C), Comp); - pragma Assert (D /= null); - - begin - if Perm /= None then - D.all.Tree.Permission := Glb (Perm, Permission (D)); - end if; - - return D; - end; - - -- The tree is folded. Expand it. - - else - declare - pragma Assert (Kind (C) = Entire_Object); - - D : Perm_Tree_Access; - D_This : Perm_Tree_Access; - Comp : Node_Id; - P : Perm_Kind; - Child_P : constant Perm_Kind := Children_Permission (C); - Hashtbl : Perm_Tree_Maps.Instance; - -- Create an empty hash table - - begin - Comp := - First_Component_Or_Discriminant - (Retysp (Etype (Prefix (N)))); - - while Present (Comp) loop - if Perm /= None - and then Original_Record_Component (Comp) = - Original_Record_Component - (Entity (Selector_Name (N))) - then - P := Perm; - else - P := Child_P; - end if; - - D := new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => - -- Hidden components are never deep - Component_Is_Visible_In_SPARK (Comp) - and then Is_Deep (Etype (Comp)), - Explanation => Expl, - Permission => P, - Children_Permission => Child_P)); - Perm_Tree_Maps.Set - (Hashtbl, Original_Record_Component (Comp), D); - - -- Store the tree to return for this component - - if Original_Record_Component (Comp) = - Original_Record_Component - (Entity (Selector_Name (N))) - then - D_This := D; - end if; - - Next_Component_Or_Discriminant (Comp); - end loop; - - C.all.Tree := (Kind => Record_Component, - Is_Node_Deep => Is_Node_Deep (C), - Explanation => Expl, - Permission => Permission (C), - Component => Hashtbl); - return D_This; - end; - end if; - end; - - when N_Indexed_Component - | N_Slice - => - declare - C : constant Perm_Tree_Access := - Set_Perm_Prefixes (Prefix (N), Perm, Expl); - pragma Assert (C /= null); - pragma Assert (Kind (C) = Entire_Object - or else Kind (C) = Array_Component); - begin - -- The tree is already unfolded. Replace the permission of the - -- component. - - if Kind (C) = Array_Component then - declare - D : constant Perm_Tree_Access := Get_Elem (C); - pragma Assert (D /= null); - - begin - if Perm /= None then - D.all.Tree.Permission := Glb (Perm, Permission (D)); - end if; - - return D; - end; - - -- The tree is folded. Expand it. - - else - declare - pragma Assert (Kind (C) = Entire_Object); - - Child_P : constant Perm_Kind := Children_Permission (C); - D : constant Perm_Tree_Access := - new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Node_Deep (C), - Explanation => Expl, - Permission => Child_P, - Children_Permission => Child_P)); - begin - if Perm /= None then - D.all.Tree.Permission := Perm; - end if; - - C.all.Tree := (Kind => Array_Component, - Is_Node_Deep => Is_Node_Deep (C), - Explanation => Expl, - Permission => Permission (C), - Get_Elem => D); - return D; - end; - end if; - end; - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - return Set_Perm_Prefixes (Expression (N), Perm, Expl); - - when others => - raise Program_Error; - end case; - end Set_Perm_Prefixes; - - ------------------------------ - -- Set_Perm_Prefixes_Assign -- - ------------------------------ - - procedure Set_Perm_Prefixes_Assign (N : Node_Id) is - C : constant Perm_Tree_Access := Get_Perm_Tree (N); - - begin - case Kind (C) is - when Entire_Object => - pragma Assert (Children_Permission (C) = Read_Write); - C.all.Tree.Permission := Read_Write; - - when Reference => - C.all.Tree.Permission := - Lub (Permission (C), Permission (Get_All (C))); - - when Array_Component => - null; - - when Record_Component => - declare - Comp : Perm_Tree_Access; - Perm : Perm_Kind := Read_Write; - - 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; - - C.all.Tree.Permission := Lub (Permission (C), Perm); - end; - end case; - - case Nkind (N) is - - -- Base identifier end recursion - - when N_Expanded_Name - | N_Identifier - => - null; - - when N_Explicit_Dereference - | N_Indexed_Component - | N_Selected_Component - | N_Slice - => - Set_Perm_Prefixes_Assign (Prefix (N)); - - when N_Qualified_Expression - | N_Type_Conversion - | N_Unchecked_Type_Conversion - => - Set_Perm_Prefixes_Assign (Expression (N)); - - when others => - raise Program_Error; - end case; - end Set_Perm_Prefixes_Assign; - - ------------------- - -- Setup_Globals -- - ------------------- - - procedure Setup_Globals (Subp : Entity_Id) is - - procedure Setup_Global - (Expr : Node_Id; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean); - -- Proxy procedure to set up globals, to adjust for the type of first - -- parameter expected by Setup_Parameter_Or_Global. - - ------------------ - -- Setup_Global -- - ------------------ - - procedure Setup_Global - (Expr : Node_Id; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean) - is - begin - Setup_Parameter_Or_Global - (Id => Entity (Expr), - Typ => Typ, - Kind => Kind, - Subp => Subp, - Global_Var => Global_Var, - Expl => Expr); - end Setup_Global; - - procedure Setup_Globals_Inst is new Handle_Globals (Setup_Global); - - -- Start of processing for Setup_Globals - - begin - Setup_Globals_Inst (Subp); - end Setup_Globals; - - ------------------------------- - -- Setup_Parameter_Or_Global -- - ------------------------------- - - procedure Setup_Parameter_Or_Global - (Id : Entity_Id; - Typ : Entity_Id; - Kind : Formal_Kind; - Subp : Entity_Id; - Global_Var : Boolean; - Expl : Node_Id) - is - Perm : Perm_Kind_Option; - - begin - case Kind is - when E_In_Parameter => - - -- Shallow parameters and globals need not be considered - - if not Is_Deep (Typ) then - Perm := None; - - -- Inputs of functions have R permission only - - elsif Ekind (Subp) = E_Function then - Perm := Read_Only; - - -- Input global variables have R permission only - - elsif Global_Var then - Perm := Read_Only; - - -- Anonymous access to constant is an observe - - elsif Is_Anonymous_Access_Type (Typ) - and then Is_Access_Constant (Typ) - then - Perm := Read_Only; - - -- Other access types are a borrow - - elsif Is_Access_Type (Typ) then - Perm := Read_Write; - - -- Deep types other than access types define an observe - - else - Perm := Read_Only; - end if; - - when E_Out_Parameter - | E_In_Out_Parameter - => - -- Shallow parameters and globals need not be considered - - if not Is_Deep (Typ) then - Perm := None; - - -- Functions cannot have outputs in SPARK - - elsif Ekind (Subp) = E_Function then - return; - - -- Deep types define a borrow or a move - - else - Perm := Read_Write; - end if; - end case; - - if Perm /= None then - declare - Tree : constant Perm_Tree_Access := - new Perm_Tree_Wrapper' - (Tree => - (Kind => Entire_Object, - Is_Node_Deep => Is_Deep (Etype (Id)), - Explanation => Expl, - Permission => Perm, - Children_Permission => Perm)); - begin - Set (Current_Perm_Env, Id, Tree); - end; - end if; - 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 - (Id => Formal, - Typ => Retysp (Etype (Formal)), - Kind => Ekind (Formal), - Subp => Subp, - Global_Var => False, - Expl => Formal); - Next_Formal (Formal); - end loop; - end Setup_Parameters; - - -------------------------------- - -- Setup_Protected_Components -- - -------------------------------- - - procedure Setup_Protected_Components (Subp : Entity_Id) is - Typ : constant Entity_Id := Scope (Subp); - Comp : Entity_Id; - Kind : Formal_Kind; - - begin - Comp := First_Component_Or_Discriminant (Typ); - - -- The protected object is an implicit input of protected functions, and - -- an implicit input-output of protected procedures and entries. - - if Ekind (Subp) = E_Function then - Kind := E_In_Parameter; - else - Kind := E_In_Out_Parameter; - end if; - - while Present (Comp) loop - Setup_Parameter_Or_Global - (Id => Comp, - Typ => Retysp (Etype (Comp)), - Kind => Kind, - Subp => Subp, - Global_Var => False, - Expl => Comp); - - Next_Component_Or_Discriminant (Comp); - end loop; - end Setup_Protected_Components; - -end Sem_SPARK; diff --git a/gcc/ada/sem_spark.ads b/gcc/ada/sem_spark.ads deleted file mode 100644 index ff9aa633ab0..00000000000 --- a/gcc/ada/sem_spark.ads +++ /dev/null @@ -1,177 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT COMPILER COMPONENTS -- --- -- --- S E M _ S P A R K -- --- -- --- S p e c -- --- -- --- Copyright (C) 2017-2019, 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 ownership analysis for access types. The rules --- that are enforced are defined in section 3.10 of the SPARK Reference --- Manual. --- --- Check_Safe_Pointers 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. - --- The implementation is done as a generic, so that GNATprove can instantiate --- it with suitable formal arguments that depend on the SPARK_Mode boundary --- as well as the two-phase architecture of GNATprove (which runs the GNAT --- front end twice, once for global generation and once for analysis). - -with Types; use Types; - -generic - with function Retysp (X : Entity_Id) return Entity_Id; - -- Return the representative type in SPARK for a type. - - with function Component_Is_Visible_In_SPARK (C : Entity_Id) return Boolean; - -- Return whether a component is visible in SPARK. No aliasing check is - -- performed for a component that is visible. - - with function Emit_Messages return Boolean; - -- Return True when error messages should be emitted. - - with function Is_Pledge_Function (E : Entity_Id) return Boolean; - -- Return True if E is annotated with a pledge annotation - -package Sem_SPARK is - - function Is_Legal (N : Node_Id) return Boolean; - -- Test the legality of a node wrt ownership-checking rules. This does not - -- check rules related to the validity of permissions associated with paths - -- from objects, so that it can be called from GNATprove on code of library - -- units analyzed in SPARK_Mode Auto. - - 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 ownership rules. - - function Is_Deep (Typ : Entity_Id) return Boolean; - -- Returns True if the type passed as argument is deep - - function Is_Traversal_Function (E : Entity_Id) return Boolean; - - function Is_Local_Context (Scop : Entity_Id) return Boolean; - -- Return if a given scope defines a local context where it is legal to - -- declare a variable of anonymous access type. - -end Sem_SPARK;