OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Fix of some permission rules of pointers in SPARK

Browse Source 
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  <maalej@adacore.com>

gcc/ada/

	* sem_spark.adb: Fix of some permission rules of pointers in SPARK.

From-SVN: r260583
This commit is contained in:
Maroua Maalej 2018-05-23 10:22:41 +00:00 committed by Pierre-Marie de Rodat
parent a0fa549732
commit 6734617ced
2 changed files with 64 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
gcc/ada/ChangeLog
View File

@ -1,3 +1,7 @@
2018-05-23 Maroua Maalej <maalej@adacore.com>
* sem_spark.adb: Fix of some permission rules of pointers in SPARK.
2018-05-23 Ed Schonberg <schonberg@adacore.com>
* sem_ch5.adb (Preanalyze_Range): The pre-analysis of the domain of

95
gcc/ada/sem_spark.adb
View File

@ -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;