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

gcc/ada/

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

From-SVN: r260583

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b99ca1a5b4e9432198f4221abef65c097afdcc64..cd5cd128cf5310941e841de2bd16078fbe910e9e 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -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

diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index c44fbc61c4f83e18acb8de3c83a315df688596cf..ac04bc93a6c25f20213a00d4aa7c4b55070c5aca 100644 (file)
--- 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;