* [Ada] Fix of some permission rules of pointers in SPARK
@ 2018-05-23 10:32 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2018-05-23 10:32 UTC (permalink / raw)
To: gcc-patches; +Cc: Maroua Maalej
[-- Attachment #1: Type: text/plain, Size: 855 bytes --]
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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-05-23 Maroua Maalej <maalej@adacore.com>
gcc/ada/
* sem_spark.adb: Fix of some permission rules of pointers in SPARK.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 11104 bytes --]
--- gcc/ada/sem_spark.adb
+++ 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;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2018-05-23 10:32 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-05-23 10:32 [Ada] Fix of some permission rules of pointers in SPARK Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).