Patchwork [Ada] Crash on quantified expressions containing 'Old in postconditions

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 31, 2011, 8:54 a.m.
Message ID <20110831085445.GA1121@adacore.com>
Download mbox | patch
Permalink /patch/112469/
State New
Headers show

Comments

Arnaud Charlet - Aug. 31, 2011, 8:54 a.m.
The attribute reference 'Old  ppears within a postcondition, but refers to
an entity in the enclosing subprogram. If the prefix is a component of a formal
its expansion might generate actual subtypes that may be referenced in an inner
context, and which must be elaborated within the subprogram itself. As a result
we create a declaration for the prefix, insert it in the enclosing subprogram
itself and expand it at once. This is properly an expansion activity but it has
to be performed now to prevent out-of-order issues in the back-end.

the following commands

   gnatmake -q -gnat12 -gnata my_test
   my_test

must yield:

Max =  9
Min =  0
Average =  4
Find 0 in T1  4
Find 9 in T2  4

---
with Simple_Unc_Arrays; use Simple_Unc_Arrays;
with Ada.Text_IO; use Ada.Text_IO;

procedure My_Test is

   T1 : Table := (10, (5, 1, 3, 0, 9, 8, 2, 7, 4, 6));
   T2 : Table := (10, (4, 8, 6, 9, 0, 1, 7, 2, 5, 3));

   T3 : Table (10);

begin
   Put_Line ("Max = " & Max (T1)'img);
   Put_Line ("Min = " & Min (T1)'img );
   Put_Line ("Average = " & Average (T1)'img);
   Put_Line ("Find 0 in T1 " & Search (T1, 0)'img);
   Put_Line ("Find 9 in T2 " & Search (T2, 9)'img);

   T3 := Add (T1, T2);
   pragma Assert (for all I in 1 .. T3.Last => T3.V (I) = 9);

   T3 := Bubble_Sort (T1);
   Quick_Sort (T1);
   
   pragma Assert (T1 = T3);
end;
---
package Simple_Unc_Arrays is

  -- This should be a generic parameter
   type Value is new Integer; -- should be range <>;

   -- This is declaring arrays with a fixed first bound of 1

   type Values is array (Positive range <>) of Value;

   type Table (Last : Natural) is record
      V : Values (1 .. Last);
   end record;

   ---------
   -- Add --
   ---------

   function Add (A, B : Table) return Table
   with Pre  => Same_Range (A, B),
        Post => Same_Range (Add'Result, A)
    and then (for all J in 1 .. A.Last =>
                 (Add'Result.V (J) = A.V (J) + B.V (J)));

   -------------
   -- Reverse --
   -------------

   Procedure Inverse (A : in out Table)
   with Post => (for all J in 1 .. A.Last => (A.V (J) = A.V'Old (A.Last - J + 1)));
   --  Reverses the content of A

   ---------
   -- Min --
   ---------

   function Min (A : Table) return Value
   with
     Pre  => not Empty (A),
     Post => (for all  J in 1 .. A.Last => Min'Result <= A.V (J))
     and then (for some J in 1 .. A.Last => Min'Result  = A.V (J));
   --  Returns the minimum value occurring in A

   ---------
   -- Max --
   ---------

   function Max (A : Table) return Value
   with
     Pre  => not Empty (A),
   Post =>    (for all  J in 1 .. A.Last => Max'Result >= A.V (J))
     and then (for some J in 1 .. A.Last => Max'Result  = A.V (J));
   --  Returns the maximun value occurring in A

   -------------
   -- Average --
   -------------

   function Average (A : Table) return Value
   with
     Pre  => not Empty (A),
     Post =>    Min (A) <= Average'Result
       and then Max (A) >= Average'Result;
   --  Returns the average value in A. Here, the given postcondition does not
   --  describe completely the value returned.

   ------------
   -- Search --
   ------------

   function Search (A : Table; V : Value) return Natural
   with Post => (Search'Result = 0 and then Not_In (A, V, 1 ,A.Last))
     or else (A.V (Search'Result) = V
              and then Not_In (A, V, 1, Search'Result-1));
   --  Returns the first index at which value V occurs in array A, or else 0

   -----------------
   -- Bubble_Sort --
   -----------------

   function Bubble_Sort (A: Table) return Table
   with Post => (for all J in 1 ..  A.Last - 1 =>
                 Bubble_Sort'Result.V (J) <= Bubble_Sort'Result.V (J+1))
     and then   (for all J in 1 .. A.Last =>
                 (for some K in 1 .. A.Last => A.V (J) = Bubble_Sort'Result.V (K)));
   --  Sorts an array in increasing order by using bubble sort

   ----------------
   -- Quick_Sort --
   ----------------

   Procedure Quick_Sort (A: in out Table);
   --  with Post => (for all J in 1 .. A.Last - 1 => A.V (J) <= A.V (J+1))
   --    and then   (for all J in 1 .. A.Last =>
   --                (for some K in 1 .. A.Last => A.V'Old (J) = A.V (K)));
   --  Sorts an array in increasing order by using quick sort

   -----------------
   -- utililities --
   -----------------

   function Empty (A : Table) return Boolean is (1 > A.Last);
   function Same_Range (A, B : Table) return Boolean is (A.Last = B.Last);
   function Not_In  (A   : Table;
                     V   : Value;
                     Low : Positive;
                     Up  : Natural)
     return Boolean is
       (Up > A.Last or else (for all J in Low .. Up => A.V (J) /= V));


   procedure Swap (V, W : in out Value)
   with Post => (V = W'Old and then W = V'Old);
   --  Swaps two values V and W

end Simple_Unc_Arrays;
---
package body Simple_Unc_Arrays is
  ---------
   -- Add --
   ---------

   function Add (A, B : Table) return Table is
   begin
      return C : Table (A.Last) do
         for I in 1 .. A.Last loop
            pragma Assert
              ((for all J in 1 .. I-1 => C.V (J) = A.V (J) + B.V (J))
              -- and then (for all K in I .. A.Last => C.V (K) = C.V'old (K)));
             );

            C.V (I) := A.V (I) + B.V (I);
         end loop;
      end return;
   end Add;

   -------------
   -- Reverse --
   -------------

  procedure Inverse (A : in out Table) is
      Low  : Positive := 1;
      High : Natural := A.Last;

   begin
      while Low < High loop
       pragma Assert
         (for all J in 1 .. Low - 1  => (A.V (J) = A.V'Old (A.Last - J + 1))
          and then (for all J in Low -1 .. A.Last => (A.V (J) = A.V'Old (J)))
         );

         Swap (A.V (Low), A.V (High));
         Low  := Low + 1;
         High := High - 1;
      end loop;
   end Inverse;

   ---------
   -- Min --
   ---------

   function Min (A : Table) return Value is
     Res : Value := A.V (1);
   begin
      for I in 2 .. A.Last loop
         pragma Assert (for all J in 1 .. I - 1 => Res <= A.V (J));

         if Res > A.V (I) then
            Res := A.V (I);
         end if;
      end loop;

      return Res;
   end Min;

  ---------
   -- Max --
   ---------

   function Max (A : Table) return Value is
   begin
     return Res : Value := A.V (1) do
       for I in 2 .. A.Last loop
          pragma Assert (for all J in 1 .. I - 1 => Res >= A.V (J));

         if Res < A.V (I) then
            Res := A.V (I);
         end if;
       end loop;
     end return;
   end Max;

   -------------
   -- Average --
   -------------

   function Average (A : Table) return Value is
      Sum     : Value := 0;

   begin
      for I in 1 .. A.Last loop
        Sum := Sum + A.V (I);
      end loop;

      return Sum / Value (A.Last);
   end Average;

   ------------
   -- Search --
   ------------

   function Search (A : Table; V : Value) return Natural is
      Pos : Natural := 0;
   begin
      for I in A.V'range loop
         pragma Assert (for all J in 1 .. I - 1 => A.V (J) /= V);
         if A.V (I) = V then
            Pos := I;
            exit;
         end if;
      end loop;

      return Pos;
   end Search;

   -----------------
   -- Bubble_Sort --
   -----------------

   function Bubble_Sort (A: Table) return Table is
      Bull : Boolean  := True;
      Res  : Table := A;
   begin
      while Bull loop
         Bull := False;
         for I in 1 .. Res.Last - 1 loop
            if Res.V (I + 1) < Res.V (I) then
               Swap (Res.V (I), Res.V (I+1));
               Bull := True;
            end if;
         end loop;
      end loop;
      return Res;
   end Bubble_Sort;

   ----------------
   -- Quick_Sort --
   ----------------

   procedure Quick_Sort (A : in out Table) is

      procedure Q_S (First, Last : Natural);
      -- for the recursive call

      procedure Q_S (First, Last : Natural) is
         Pivot_Index, Right, Left : Natural;
         Pivot_Value: Value;
      begin
         if First < Last then
            Pivot_Index := (First + Last + 1) / 2;
            Pivot_Value := A.V (Pivot_Index);
            Left  := First;
            Right := Last;
            loop
               while Left < Last and then A.V (Left) < Pivot_Value loop
                  Left := Left + 1;
               end loop;

               while Right > First and then A.V (Right) > Pivot_Value loop
                  Right := Right - 1;
               end loop;

               exit when Left >= Right;

               Swap (A.V (Left), A.V (Right));
            end loop;

            if Right > First then
               Q_S (First, Right - 1);
            end if;

            if Left < Last then
               Q_S (Left, Last);
            end if;
         end if;
     end Q_S;

   begin
      Q_S (1, A.Last);
   end Quick_Sort;

   procedure Swap (V, W : in out Value) is
      Tmp : Value;
   begin
      Tmp := V;
      V   := W;
      W   := Tmp;
   end Swap;

end Simple_Unc_Arrays;

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

2011-08-31  Ed Schonberg  <schonberg@adacore.com>

	* sem_attr.adb (Analyze_Attribute, case 'Old): If prefix may be a
	discriminated component of an actual, expand at once to prevent
	ouf-of-order references with generated subtypes.

Patch

Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 178358)
+++ sem_attr.adb	(working copy)
@@ -1939,7 +1939,7 @@ 
       --  Analyze prefix and exit if error in analysis. If the prefix is an
       --  incomplete type, use full view if available. Note that there are
       --  some attributes for which we do not analyze the prefix, since the
-      --  prefix is not a normal name.
+      --  prefix is not a normal name, or else needs special handling.
 
       if Aname /= Name_Elab_Body
            and then
@@ -1950,6 +1950,8 @@ 
          Aname /= Name_UET_Address
            and then
          Aname /= Name_Enabled
+           and then
+         Aname /= Name_Old
       then
          Analyze (P);
          P_Type := Etype (P);
@@ -3772,6 +3774,12 @@ 
          end if;
 
          Check_E0;
+
+         --  Prefix has not been analyzed yet, and its full analysis will take
+         --  place during expansion (see below).
+
+         Preanalyze_And_Resolve (P);
+         P_Type := Etype (P);
          Set_Etype (N, P_Type);
 
          if No (Current_Subprogram) then
@@ -3852,6 +3860,24 @@ 
             end if;
          end Check_Local;
 
+         --  The attribute ppears within a pre/postcondition, but refers to
+         --  an entity in the enclosing subprogram. If it is a component of a
+         --  formal its expansion might generate actual subtypes that may be
+         --  referenced in an inner context, and which must be elaborated
+         --  within the subprogram itself. As a result we create a declaration
+         --  for it and insert it at the start of the enclosing subprogram
+         --  This is properly an expansion activity but it has to be performed
+         --  now to prevent out-of-order issues.
+
+         if Nkind (P) = N_Selected_Component
+           and then Has_Discriminants (Etype (Prefix (P)))
+         then
+            P_Type := Base_Type (P_Type);
+            Set_Etype (N, P_Type);
+            Set_Etype (P, P_Type);
+            Expand (N);
+         end if;
+
       ------------
       -- Output --
       ------------