From 6734617cedcadfddfc33378ce824b4620381d91c Mon Sep 17 00:00:00 2001 From: Maroua Maalej Date: Wed, 23 May 2018 10:22:41 +0000 Subject: [PATCH] [Ada] Fix of some permission rules of pointers in SPARK This commit fixes bugs in the code that implements the rules for safe pointers in SPARK. This only affects SPARK tools, not compilation. * Global variables should be handled differently compared to parameters. The whole tree of an in global variable has the permission Read-Only. In contrast, an in parameter has the permission Read-Only for the first level and Read-Write permission for suffixes. * The suffix X of Integer'image(X) was not analyzed correctly. * The instruction X'img was not dealt with. * Shallow aliased types which are not initialized are now allowed and analyzed. Dealing with function inlining is not handled correctly yet. 2018-05-23 Maroua Maalej gcc/ada/ * sem_spark.adb: Fix of some permission rules of pointers in SPARK. From-SVN: r260583 --- gcc/ada/ChangeLog | 4 +++ gcc/ada/sem_spark.adb | 95 ++++++++++++++++++++++++++++++++------------------- 2 files changed, 64 insertions(+), 35 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b99ca1a..cd5cd12 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 c44fbc6..ac04bc9 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; -- 2.7.4