Patchwork [Ada] Ada2012: detecting dangerous order dependences

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 25, 2010, 1:51 p.m.
Message ID <20101025135110.GA683@adacore.com>
Download mbox | patch
Permalink /patch/69098/
State New
Headers show

Comments

Arnaud Charlet - Oct. 25, 2010, 1:51 p.m.
This patch implements AI05-144-2: detecting order dependences among actuals
in calls that appear in the same construct. The potentially dangerous cases
described in the AI are flagged as warnings for now, not as errors. The
detection of overlapping actuals in a simple call remains under control of
the debugging switch -gnatw.i, to minimize disruption to legacy code.
This AI complements AI05-143, on in-out parameters for functions, because it
is in the presence of such functions that dangerous order dependences arise.

Below is an example of the warnings generated by

     gcc -c -gnat12 -gnatw.i order.adb

---
Compiling: order.adb (source file time stamp: 2010-10-07 20:43:39)

     1. procedure Order is
     2.    function Change (X, Y : in out Integer) return integer;
     3.
     4.    function Change (X, Y : in out Integer) return integer is
     5.    begin
     6.       X := X * 2;
     7.       Y := Y * 4;
     8.       return X + Y;
     9.    end;
    10.
    11.    One : Integer := 10;
    12.    Two : Integer := 25;
    13.    Res : Integer;
    14.    Uno : Integer renames One;
    15.
    16.    Table : array (1..3) of integer := (10, 20, 30);
    17.    T1 : Integer renames Table (1);
    18.
    19.    procedure ND (X, Y : integer) is
    20.    begin
    21.       null;
    22.    end;
    23.
    24.    Var : Natural := 2;
    25. begin
    26.     Two := Change (One, Two);
    27.     Two := Change (One, One);
                           |
        >>> warning: writable actual overlaps with actual for "Y"

    28.     Two := Change (X => One, Y => Two);
    29.     Res := Change (One, Two) + Change (One, Two);
                           1    2
        >>> warning: result may differ if evaluated  after other actual in expression
        >>> warning: result may differ if evaluated  after other actual in expression

    30.     Two := Change (One, Order.Two);
    31.     One := Change (Table (1), Table (2));
    32.     One := Change (Table (1), Table (1));
                           |
        >>> warning: writable actual overlaps with actual for "Y"

    33.     ND (Change (One, Two), Change (Two, Res));
                             |
        >>> warning: result may differ if evaluated  after other actual in expression

    34.     Two := Change (Uno, One);
                           |
        >>> warning: writable actual overlaps with actual for "Y"

    35.     Res := Change (T1, Table (1));
                           |
        >>> warning: writable actual overlaps with actual for "Y"

    36.     if Change (T1, T1) > 10 then null; end if;
                       |
        >>> warning: writable actual overlaps with actual for "Y"

    37.
    38.    Table (Change (One, Two)) := Table (Change (One, Res));
                          |
        >>> warning: result may differ if evaluated  after other actual in expression

    39.    if Change (One, Two) + Change (Two, Res) > 10 then null; end if;
                           |
        >>> warning: result may differ if evaluated  after other actual in expression

    40.    if Change (One, Two) + Change (Two, Res) > 10
                           1                   2
        >>> warning: result may differ if evaluated  after other actual in expression
        >>> warning: result may differ if evaluated  after other actual in expression

    41.      or else Change (Res, Res) = -1  then null; end if;
                             |
        >>> warning: writable actual overlaps with actual for "Y"

    42. end;

 42 lines: No errors, 13 warnings

Tested on x86_64-pc-linux-gnu, committed on trunk

2010-10-25  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch5.adb (Analyze_Assignment_Statement): Check dangerous order
	dependence.
	* sem_ch6.adb (Analyze_Procedure_Call_Statement): Ditto.
	* sem_res.adb (Analyze_Actuals): Add actual to list of actuals for
	current construct, for subsequent order dependence checking.
	(Resolve): Check order dependence on expressions that are not
	subexpressions.
	* sem_util.adb (Check_Order_Dependence): Code cleanup, to correspond
	to latest version of AI05-144-2.
	* sem_warn.adb (Warn_On_Overlapping_Actuals): Code cleanup.
Duncan Sands - Oct. 25, 2010, 3:48 p.m.
Hi Arnaud,

+                     Error_Msg_N (
+                       "result may differ if evaluated "
+                        & " after other actual in expression?", Act1);

did you really mean to have two spaces between "evaluated" and "after"?

Ciao,

Duncan.
Arnaud Charlet - Oct. 25, 2010, 3:52 p.m.
Duncan,

It's really hard to answer your emails, since you do not give enough
context, in particular I have to guess which file you are referring to.

> +                     Error_Msg_N (
> +                       "result may differ if evaluated "
> +                        & " after other actual in expression?", Act1);
> 
> did you really mean to have two spaces between "evaluated" and "after"?

This was a typo, fixed.

Arno

Patch

Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb	(revision 165916)
+++ sem_ch5.adb	(working copy)
@@ -662,6 +662,7 @@  package body Sem_Ch5 is
       --  checks have been applied.
 
       Note_Possible_Modification (Lhs, Sure => True);
+      Check_Order_Dependence;
 
       --  ??? a real accessibility check is needed when ???
 
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 165916)
+++ sem_util.adb	(working copy)
@@ -101,12 +101,12 @@  package body Sem_Util is
    --  whether the corresponding formal is OUT or IN OUT. Each top-level call
    --  (procedure call, condition, assignment) examines all the actuals for a
    --  possible order dependence. The table is reset after each such check.
+   --  The actuals to be checked in a call to Check_Order_Dependence are at
+   --  positions 1 .. Last.
 
    type Actual_Name is record
       Act         : Node_Id;
       Is_Writable : Boolean;
-      --  Comments needed???
-
    end record;
 
    package Actuals_In_Call is new Table.Table (
@@ -1222,9 +1222,17 @@  package body Sem_Util is
       Act2 : Node_Id;
 
    begin
-      --  This could use comments ???
+      if Ada_Version < Ada_2012 then
+         return;
+      end if;
 
-      for J in 0 .. Actuals_In_Call.Last loop
+      --  Ada2012 AI04-0144-2 : dangerous order dependence.
+      --  Actuals in nested calls within a construct have been collected.
+      --  If one of them is writeable and overlaps with another one, evaluation
+      --  of the enclosing construct is non-deterministic.
+      --  This is illegal in Ada2012, but is treated as a warning for now.
+
+      for J in 1 .. Actuals_In_Call.Last loop
          if Actuals_In_Call.Table (J).Is_Writable then
             Act1 := Actuals_In_Call.Table (J).Act;
 
@@ -1232,7 +1240,7 @@  package body Sem_Util is
                Act1 := Prefix (Act1);
             end if;
 
-            for K in 0 .. Actuals_In_Call.Last loop
+            for K in 1 .. Actuals_In_Call.Last loop
                if K /= J then
                   Act2 := Actuals_In_Call.Table (K).Act;
 
@@ -1248,15 +1256,19 @@  package body Sem_Util is
                      null;
 
                   elsif Denotes_Same_Object (Act1, Act2)
-                    and then False
+                    and then Parent (Act1) /= Parent (Act2)
                   then
-                     Error_Msg_N ("?,mighty suspicious!!!", Act1);
+                     Error_Msg_N (
+                       "result may differ if evaluated "
+                        & " after other actual in expression?", Act1);
                   end if;
                end if;
             end loop;
          end if;
       end loop;
 
+      --  Remove checked actuals from table.
+
       Actuals_In_Call.Set_Last (0);
    end Check_Order_Dependence;
 
@@ -2350,49 +2362,105 @@  package body Sem_Util is
    -------------------------
 
    function Denotes_Same_Object (A1, A2 : Node_Id) return Boolean is
+      Obj1 : Node_Id := A1;
+      Obj2 : Node_Id := A2;
+
+      procedure Check_Renaming (Obj : in out Node_Id);
+      --  If an object is a renaming, examine renamed object. If is is a
+      --  dereference of a variable, or an indexed expression with non-
+      --  constant indices, no overlap check can be reported.
+
+      procedure Check_Renaming (Obj : in out Node_Id) is
+      begin
+         if Is_Entity_Name (Obj)
+           and then Present (Renamed_Entity (Entity (Obj)))
+         then
+            Obj := Renamed_Entity (Entity (Obj));
+            if Nkind (Obj) = N_Explicit_Dereference
+              and then Is_Variable (Prefix (Obj))
+            then
+               Obj := Empty;
+
+            elsif Nkind (Obj) = N_Indexed_Component then
+               declare
+                  Indx : Node_Id;
+
+               begin
+                  Indx := First (Expressions (Obj));
+                  while Present (Indx) loop
+                     if not Is_OK_Static_Expression (Indx) then
+                        Obj := Empty;
+                        exit;
+                     end if;
+
+                     Next_Index (Indx);
+                  end loop;
+               end;
+            end if;
+         end if;
+      end Check_Renaming;
+
    begin
+      Check_Renaming (Obj1);
+      Check_Renaming (Obj2);
+
+      if No (Obj1)
+        or else No (Obj2)
+      then
+         return False;
+      end if;
+
       --  If we have entity names, then must be same entity
 
-      if Is_Entity_Name (A1) then
-         if Is_Entity_Name (A2) then
-            return Entity (A1) = Entity (A2);
+      if Is_Entity_Name (Obj1) then
+         if Is_Entity_Name (Obj2) then
+            return Entity (Obj1) = Entity (Obj2);
          else
             return False;
          end if;
 
       --  No match if not same node kind
 
-      elsif Nkind (A1) /= Nkind (A2) then
+      elsif Nkind (Obj1) /= Nkind (Obj2) then
          return False;
 
       --  For selected components, must have same prefix and selector
 
-      elsif Nkind (A1) = N_Selected_Component then
-         return Denotes_Same_Object (Prefix (A1), Prefix (A2))
+      elsif Nkind (Obj1) = N_Selected_Component then
+         return Denotes_Same_Object (Prefix (Obj1), Prefix (Obj2))
            and then
-         Entity (Selector_Name (A1)) = Entity (Selector_Name (A2));
+         Entity (Selector_Name (Obj1)) = Entity (Selector_Name (Obj2));
 
       --  For explicit dereferences, prefixes must be same
 
-      elsif Nkind (A1) = N_Explicit_Dereference then
-         return Denotes_Same_Object (Prefix (A1), Prefix (A2));
+      elsif Nkind (Obj1) = N_Explicit_Dereference then
+         return Denotes_Same_Object (Prefix (Obj1), Prefix (Obj2));
 
       --  For indexed components, prefixes and all subscripts must be the same
 
-      elsif Nkind (A1) = N_Indexed_Component then
-         if Denotes_Same_Object (Prefix (A1), Prefix (A2)) then
+      elsif Nkind (Obj1) = N_Indexed_Component then
+         if Denotes_Same_Object (Prefix (Obj1), Prefix (Obj2)) then
             declare
                Indx1 : Node_Id;
                Indx2 : Node_Id;
 
             begin
-               Indx1 := First (Expressions (A1));
-               Indx2 := First (Expressions (A2));
+               Indx1 := First (Expressions (Obj1));
+               Indx2 := First (Expressions (Obj2));
                while Present (Indx1) loop
 
-                  --  Shouldn't we be checking that values are the same???
+                  --  Indices must denote the same static value or the same
+                  --  object.
+
+                  if Is_OK_Static_Expression (Indx1) then
+                     if not Is_OK_Static_Expression (Indx2) then
+                        return False;
 
-                  if not Denotes_Same_Object (Indx1, Indx2) then
+                     elsif Expr_Value (Indx1) /= Expr_Value (Indx2) then
+                        return False;
+                     end if;
+
+                  elsif not Denotes_Same_Object (Indx1, Indx2) then
                      return False;
                   end if;
 
@@ -2408,21 +2476,19 @@  package body Sem_Util is
 
       --  For slices, prefixes must match and bounds must match
 
-      elsif Nkind (A1) = N_Slice
-        and then Denotes_Same_Object (Prefix (A1), Prefix (A2))
+      elsif Nkind (Obj1) = N_Slice
+        and then Denotes_Same_Object (Prefix (Obj1), Prefix (Obj2))
       then
          declare
             Lo1, Lo2, Hi1, Hi2 : Node_Id;
 
          begin
-            Get_Index_Bounds (Etype (A1), Lo1, Hi1);
-            Get_Index_Bounds (Etype (A2), Lo2, Hi2);
+            Get_Index_Bounds (Etype (Obj1), Lo1, Hi1);
+            Get_Index_Bounds (Etype (Obj2), Lo2, Hi2);
 
             --  Check whether bounds are statically identical. There is no
             --  attempt to detect partial overlap of slices.
 
-            --  What about an array and a slice of an array???
-
             return Denotes_Same_Object (Lo1, Lo2)
               and then Denotes_Same_Object (Hi1, Hi2);
          end;
@@ -2430,8 +2496,8 @@  package body Sem_Util is
          --  Literals will appear as indexes. Isn't this where we should check
          --  Known_At_Compile_Time at least if we are generating warnings ???
 
-      elsif Nkind (A1) = N_Integer_Literal then
-         return Intval (A1) = Intval (A2);
+      elsif Nkind (Obj1) = N_Integer_Literal then
+         return Intval (Obj1) = Intval (Obj2);
 
       else
          return False;
@@ -10696,7 +10762,10 @@  package body Sem_Util is
 
    procedure Save_Actual (N : Node_Id;  Writable : Boolean := False) is
    begin
-      if Is_Entity_Name (N)
+      if Ada_Version < Ada_2012 then
+         return;
+
+      elsif Is_Entity_Name (N)
         or else
           Nkind_In (N, N_Indexed_Component, N_Selected_Component, N_Slice)
         or else
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 165916)
+++ sem_res.adb	(working copy)
@@ -2744,6 +2744,18 @@  package body Sem_Res is
             return;
          end if;
 
+         --  AI05-144-2: Check dangerous order dependence within an expression
+         --  that is not a subexpression. Exclude RHS of an assignment, because
+         --  both sides may have side-effects and the check must be performed
+         --  over the statement.
+
+         if Nkind (Parent (N)) not in N_Subexpr
+           and then Nkind (Parent (N)) /= N_Assignment_Statement
+           and then Nkind (Parent (N)) /= N_Procedure_Call_Statement
+         then
+            Check_Order_Dependence;
+         end if;
+
          --  The expression is definitely NOT overloaded at this point, so
          --  we reset the Is_Overloaded flag to avoid any confusion when
          --  reanalyzing the node.
@@ -3529,12 +3541,10 @@  package body Sem_Res is
             A_Typ := Etype (A);
             F_Typ := Etype (F);
 
-            --  Save actual for subsequent check on order dependence,
-            --  and indicate whether actual is modifiable. For AI05-0144
+            --  Save actual for subsequent check on order dependence, and
+            --  indicate whether actual is modifiable. For AI05-0144-2.
 
-            --  Save_Actual (A,
-            --    Ekind (F) /= E_In_Parameter or else Is_Access_Type (F_Typ));
-            --  Why is this code commented out ???
+            Save_Actual (A, Ekind (F) /= E_In_Parameter);
 
             --  For mode IN, if actual is an entity, and the type of the formal
             --  has warnings suppressed, then we reset Never_Set_In_Source for
@@ -8228,11 +8238,8 @@  package body Sem_Res is
       R     : constant Node_Id   := Right_Opnd (N);
 
    begin
-      --  Why are the calls to Check_Order_Dependence commented out ???
       Resolve (L, B_Typ);
-      --  Check_Order_Dependence;   --  For AI05-0144
       Resolve (R, B_Typ);
-      --  Check_Order_Dependence;   --  For AI05-0144
 
       --  Check for issuing warning for always False assert/check, this happens
       --  when assertions are turned off, in which case the pragma Assert/Check
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 165916)
+++ sem_ch6.adb	(working copy)
@@ -811,9 +811,8 @@  package body Sem_Ch6 is
          end if;
 
          --  Apply checks suggested by AI05-0144 (dangerous order dependence)
-         --  (Disabled for now)
 
-         --  Check_Order_Dependence;
+         Check_Order_Dependence;
       end if;
    end Analyze_Function_Return;
 
@@ -1116,9 +1115,9 @@  package body Sem_Ch6 is
             Analyze_Call (N);
             Resolve (N, Standard_Void_Type);
 
-            --  Apply checks suggested by AI05-0144 (Disabled for now)
+            --  Apply checks suggested by AI05-0144
 
-            --  Check_Order_Dependence;
+            Check_Order_Dependence;
 
          else
             Analyze (N);
Index: sem_warn.adb
===================================================================
--- sem_warn.adb	(revision 165916)
+++ sem_warn.adb	(working copy)
@@ -3708,7 +3708,7 @@  package body Sem_Warn is
       Form1 := First_Formal (Subp);
       Act1  := First_Actual (N);
       while Present (Form1) and then Present (Act1) loop
-         if Ekind (Form1) = E_In_Out_Parameter then
+         if Ekind (Form1) /= E_In_Parameter then
             Form2 := First_Formal (Subp);
             Act2  := First_Actual (N);
             while Present (Form2) and then Present (Act2) loop
@@ -3739,11 +3739,11 @@  package body Sem_Warn is
                   elsif Nkind (Act2) = N_Function_Call then
                      null;
 
-                  --  If either type is elementary the aliasing is harmless.
+                  --  If type is not by-copy we can assume that  the aliasing
+                  --  is intended.
 
-                  elsif Is_Elementary_Type (Underlying_Type (Etype (Form1)))
-                          or else
-                        Is_Elementary_Type (Underlying_Type (Etype (Form2)))
+                  elsif
+                    Is_By_Reference_Type (Underlying_Type (Etype (Form1)))
                   then
                      null;
 
@@ -3762,11 +3762,21 @@  package body Sem_Warn is
                            Next_Actual (Act);
                         end loop;
 
+                        if Is_Elementary_Type (Etype (Act1))
+                          and then Ekind (Form2) = E_In_Parameter
+                        then
+                           null;  --  no real aliasing.
+
+                        elsif Is_Elementary_Type (Etype (Act2))
+                          and then Ekind (Form2) = E_In_Parameter
+                        then
+                           null;  --  ditto
+
                         --  If the call was written in prefix notation, and
                         --  thus its prefix before rewriting was a selected
                         --  component, count only visible actuals in the call.
 
-                        if Is_Entity_Name (First_Actual (N))
+                        elsif Is_Entity_Name (First_Actual (N))
                           and then Nkind (Original_Node (N)) = Nkind (N)
                           and then Nkind (Name (Original_Node (N))) =
                                                          N_Selected_Component