diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b99ca1a5b4e..cd5cd128cf5 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,7 @@ +2018-05-23 Maroua Maalej + + * sem_spark.adb: Fix of some permission rules of pointers in SPARK. + 2018-05-23 Ed Schonberg * sem_ch5.adb (Preanalyze_Range): The pre-analysis of the domain of diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index c44fbc61c4f..ac04bc93a6c 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -554,9 +554,10 @@ package body Sem_SPARK is Super_Move, -- Enhanced moving semantics (under 'Access). Checks that paths have - -- Read_Write permission. After moving a path, its permission is set - -- to No_Access, as well as the permission of its extensions and the - -- permission of its prefixes up to the first Reference node. + -- Read_Write permission (shallow types may have only Write permission). + -- After moving a path, its permission is set to No_Access, as well as + -- the permission of its extensions and the permission of its prefixes + -- up to the first Reference node. Borrow_Out, -- Used for actual OUT parameters. Checks that paths have Write_Perm @@ -750,9 +751,10 @@ package body Sem_SPARK is -- execution. procedure Return_Parameter_Or_Global - (Id : Entity_Id; - Mode : Formal_Kind; - Subp : Entity_Id); + (Id : Entity_Id; + Mode : Formal_Kind; + Subp : Entity_Id; + Global_Var : Boolean); -- Auxiliary procedure to Return_Parameters and Return_Globals procedure Return_Parameters (Subp : Entity_Id); @@ -813,8 +815,9 @@ package body Sem_SPARK is -- global items with appropriate permissions. procedure Setup_Parameter_Or_Global - (Id : Entity_Id; - Mode : Formal_Kind); + (Id : Entity_Id; + Mode : Formal_Kind; + Global_Var : Boolean); -- Auxiliary procedure to Setup_Parameters and Setup_Globals procedure Setup_Parameters (Subp : Entity_Id); @@ -1049,23 +1052,27 @@ package body Sem_SPARK is declare Elem : Perm_Tree_Access; - + Deep : constant Boolean := + Is_Deep (Etype (Defining_Identifier (Decl))); begin Elem := new Perm_Tree_Wrapper' (Tree => (Kind => Entire_Object, - Is_Node_Deep => - Is_Deep (Etype (Defining_Identifier (Decl))), + Is_Node_Deep => Deep, Permission => Read_Write, Children_Permission => Read_Write)); -- If unitialized declaration, then set to Write_Only. If a -- pointer declaration, it has a null default initialization. - if Nkind (Expression (Decl)) = N_Empty + if No (Expression (Decl)) and then not Has_Full_Default_Initialization (Etype (Defining_Identifier (Decl))) and then not Is_Access_Type (Etype (Defining_Identifier (Decl))) + -- Objects of shallow types are considered as always + -- initialized, leaving the checking of initialization to + -- flow analysis. + and then Deep then Elem.all.Tree.Permission := Write_Only; Elem.all.Tree.Children_Permission := Write_Only; @@ -1209,6 +1216,9 @@ package body Sem_SPARK is Check_Node (Prefix (Expr)); when Name_Image => + Check_List (Expressions (Expr)); + + when Name_Img => Check_Node (Prefix (Expr)); when Name_SPARK_Mode => @@ -2350,7 +2360,7 @@ package body Sem_SPARK is | N_Use_Type_Clause | N_Validate_Unchecked_Conversion | N_Variable_Reference_Marker - => + => null; -- The following nodes are rewritten by semantic analysis @@ -3528,10 +3538,10 @@ package body Sem_SPARK is when N_Identifier | N_Expanded_Name => - return Has_Alias_Deep (Etype (N)); + return Is_Aliased (Entity (N)) or else Has_Alias_Deep (Etype (N)); when N_Defining_Identifier => - return Has_Alias_Deep (Etype (N)); + return Is_Aliased (N) or else Has_Alias_Deep (Etype (N)); when N_Type_Conversion | N_Unchecked_Type_Conversion @@ -4231,6 +4241,7 @@ package body Sem_SPARK is procedure Process_Path (N : Node_Id) is Root : constant Entity_Id := Get_Enclosing_Object (N); begin + -- We ignore if yielding to synchronized if Present (Root) @@ -4242,7 +4253,8 @@ package body Sem_SPARK is -- We ignore shallow unaliased. They are checked in flow analysis, -- allowing backward compatibility. - if not Has_Alias (N) + if Current_Checking_Mode /= Super_Move + and then not Has_Alias (N) and then Is_Shallow (Etype (N)) then return; @@ -4259,6 +4271,7 @@ package body Sem_SPARK is when Read => if Perm_N not in Read_Perm then Perm_Error (N, Read_Only, Perm_N); + return; end if; -- If shallow type no need for RW, only R @@ -4267,12 +4280,14 @@ package body Sem_SPARK is if Is_Shallow (Etype (N)) then if Perm_N not in Read_Perm then Perm_Error (N, Read_Only, Perm_N); + return; end if; else -- Check permission RW if deep if Perm_N /= Read_Write then Perm_Error (N, Read_Write, Perm_N); + return; end if; declare @@ -4303,6 +4318,7 @@ package body Sem_SPARK is when Super_Move => if Perm_N /= Read_Write then Perm_Error (N, Read_Write, Perm_N); + return; end if; declare @@ -4330,6 +4346,7 @@ package body Sem_SPARK is when Assign => if Perm_N not in Write_Perm then Perm_Error (N, Write_Only, Perm_N); + return; end if; -- If the tree has an array component, then the permissions do @@ -4341,7 +4358,7 @@ package body Sem_SPARK is -- Same if has function component - if Has_Function_Component (N) then + if Has_Function_Component (N) then -- Dead code? return; end if; @@ -4534,7 +4551,7 @@ package body Sem_SPARK is if Ekind (E) = E_Abstract_State then null; else - Return_Parameter_Or_Global (E, Kind, Subp); + Return_Parameter_Or_Global (E, Kind, Subp, Global_Var => True); end if; Next_Global (Item); end loop; @@ -4580,9 +4597,10 @@ package body Sem_SPARK is -------------------------------- procedure Return_Parameter_Or_Global - (Id : Entity_Id; - Mode : Formal_Kind; - Subp : Entity_Id) + (Id : Entity_Id; + Mode : Formal_Kind; + Subp : Entity_Id; + Global_Var : Boolean) is Elem : constant Perm_Tree_Access := Get (Current_Perm_Env, Id); pragma Assert (Elem /= null); @@ -4591,13 +4609,18 @@ package body Sem_SPARK is -- Shallow unaliased parameters and globals cannot introduce pointer -- aliasing. - if not Has_Alias (Id) and then Is_Shallow (Etype (Id)) then + if not Has_Alias (Id) + and then Is_Shallow (Etype (Id)) + then null; -- Observed IN parameters and globals need not return a permission to -- the caller. - elsif Mode = E_In_Parameter and then not Is_Borrowed_In (Id) then + elsif Mode = E_In_Parameter + and then (not Is_Borrowed_In (Id) + or else Global_Var) + then null; -- All other parameters and globals should return with mode RW to the @@ -4624,7 +4647,7 @@ package body Sem_SPARK is begin Formal := First_Formal (Subp); while Present (Formal) loop - Return_Parameter_Or_Global (Formal, Ekind (Formal), Subp); + Return_Parameter_Or_Global (Formal, Ekind (Formal), Subp, False); Next_Formal (Formal); end loop; end Return_Parameters; @@ -4877,6 +4900,7 @@ package body Sem_SPARK is case Kind (C) is when Entire_Object => pragma Assert (Children_Permission (C) = Read_Write); + -- Maroua: Children could have read_only perm. Why Read_Write? C.all.Tree.Permission := Read_Write; when Reference => @@ -4888,9 +4912,9 @@ package body Sem_SPARK is when Array_Component => pragma Assert (C.all.Tree.Get_Elem /= null); - -- Given that it is not possible to know which element has been - -- assigned, then the permissions do not get changed in case of - -- Array_Component. + -- Given that it is not possible to know which element has been + -- assigned, then the permissions do not get changed in case of + -- Array_Component. null; @@ -4901,8 +4925,8 @@ package body Sem_SPARK is Comp : Perm_Tree_Access; begin - -- We take the Glb of all the descendants, and then update the - -- permission of the node with it. + -- 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)); @@ -6081,7 +6105,7 @@ package body Sem_SPARK is if Ekind (E) = E_Abstract_State then null; else - Setup_Parameter_Or_Global (E, Kind); + Setup_Parameter_Or_Global (E, Kind, Global_Var => True); end if; Next_Global (Item); end loop; @@ -6127,8 +6151,9 @@ package body Sem_SPARK is ------------------------------- procedure Setup_Parameter_Or_Global - (Id : Entity_Id; - Mode : Formal_Kind) + (Id : Entity_Id; + Mode : Formal_Kind; + Global_Var : Boolean) is Elem : Perm_Tree_Access; @@ -6145,7 +6170,7 @@ package body Sem_SPARK is -- Borrowed IN: RW for everybody - if Is_Borrowed_In (Id) then + if Is_Borrowed_In (Id) and not Global_Var then Elem.all.Tree.Permission := Read_Write; Elem.all.Tree.Children_Permission := Read_Write; @@ -6182,9 +6207,9 @@ package body Sem_SPARK is begin Formal := First_Formal (Subp); while Present (Formal) loop - Setup_Parameter_Or_Global (Formal, Ekind (Formal)); + Setup_Parameter_Or_Global + (Formal, Ekind (Formal), Global_Var => False); Next_Formal (Formal); end loop; end Setup_Parameters; - end Sem_SPARK;