[Ada] Contract_Cases on entries

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements apect/pragma Contract_Cases on enties.

------------
-- Source --
------------

--  tracker.ads

package Tracker is
   type Check_Kind is
     (Pre,
      Refined_Post,
      Post,
      Conseq_1,
      Conseq_2);

   type Tested_Array is array (Check_Kind) of Boolean;
   --  A value of "True" indicates that a check has been tested

   function Greater_Than
     (Kind : Check_Kind;
      Val  : Natural;
      Exp  : Natural) return Boolean;
   --  Determine whether value Val is greater than expected value Exp. The
   --  routine also updates the history for check of kind Kind. Duplicate
   --  attempts to modify the history are flagged as errors.

   procedure Reset;
   --  Reset the history

   procedure Verify (Exp : Tested_Array);
   --  Verify whether expected tests Exp were indeed checked. Emit an error if
   --  this is not the case.
end Tracker;

--  tacker.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Tracker is
   History : array (Check_Kind) of Boolean := (others => False);
   --  The history of performed checked. A value of "True" indicates that a
   --  check was performed.

   ------------------
   -- Greater_Than --
   ------------------

   function Greater_Than
     (Kind : Check_Kind;
      Val  : Natural;
      Exp  : Natural) return Boolean
   is
   begin
      if History (Kind) then
         Put_Line ("  ERROR: " & Kind'Img & " tested multiple times");
      else
         History (Kind) := True;
      end if;

      return Val > Exp;
   end Greater_Than;

   -----------
   -- Reset --
   -----------

   procedure Reset is
   begin
      History := (others => False);
   end Reset;

   ------------
   -- Verify --
   ------------

   procedure Verify (Exp : Tested_Array) is
   begin
      for Index in Check_Kind'Range loop
         if Exp (Index) and not History (Index) then
            Put_Line ("  ERROR: " & Index'Img & " was not tested");
         elsif not Exp (Index) and History (Index) then
            Put_Line ("  ERROR: " & Index'Img & " was tested");
         end if;
      end loop;
   end Verify;
end Tracker;

--  sync_contracts.ads

with Tracker; use Tracker;

package Sync_Contracts
  with SPARK_Mode,
       Abstract_State => State
is
   protected type Prot_Typ is
      entry Prot_Entry (Input : Natural; Output : out Natural)
        with Global  => (Input => State),
             Depends => ((Prot_Typ, Output) => (State, Prot_Typ, Input)),
             Pre  => Greater_Than (Pre,  Input,  1),
             Post => Greater_Than (Post, Output, 4),
             Contract_Cases =>
               (Input < 5 => True,
                Input = 5 => Greater_Than (Conseq_1, Output, 6),
                Input = 6 => Greater_Than (Conseq_2, Output, 7),
                Input > 6 => False);

      procedure Prot_Proc (Input : Natural; Output : out Natural)
        with Pre  => Greater_Than (Pre , Input,  1),
             Post => Greater_Than (Post, Output, 4),
             Contract_Cases =>
               (Input < 5 => True,
                Input = 5 => Greater_Than (Conseq_1, Output, 6),
                Input = 6 => Greater_Than (Conseq_2, Output, 7),
                Input > 6 => False);

      function Prot_Func (Input : Natural) return Natural
        with Pre  => Greater_Than (Pre , Input, 1),
             Post => Greater_Than (Post, Prot_Func'Result, 4),
             Contract_Cases =>
               (Input < 5 => True,
                Input = 5 => Greater_Than (Conseq_1, Prot_Func'Result, 6),
                Input = 6 => Greater_Than (Conseq_2, Prot_Func'Result, 7),
                Input > 6 => False);
   end Prot_Typ;

   task type Tsk_Typ is
      entry Tsk_Entry (Input : Natural; Output : out Natural)
        with Pre  => Greater_Than (Pre , Input,  1),
             Post => Greater_Than (Post, Output, 4),
             Contract_Cases =>
               (Input < 5 => True,
                Input = 5 => Greater_Than (Conseq_1, Output, 6),
                Input = 6 => Greater_Than (Conseq_2, Output, 7),
                Input > 6 => False);
   end Tsk_Typ;
end Sync_Contracts;

--  sync_contracts.adb

package body Sync_Contracts
  with SPARK_Mode,
       Refined_State => (State => Var)
is
   Var : Integer := 1;

   protected body Prot_Typ is
      entry Prot_Entry (Input : Natural; Output : out Natural)
        with Refined_Global  => (Input => Var),
             Refined_Depends => ((Prot_Typ, Output) => (Var, Prot_Typ, Input)),
             Refined_Post => Greater_Than (Refined_Post, Output, 3)
        when True
      is
      begin
         Output := Input + 1;
      end Prot_Entry;

      procedure Prot_Proc (Input : Natural; Output : out Natural)
        with Refined_Post => Greater_Than (Refined_Post, Output, 3)
      is
      begin
         Output := Input + 1;
      end Prot_Proc;

      function Prot_Func (Input : Natural) return Natural
        with Refined_Post => Greater_Than (Refined_Post, Prot_Func'Result, 3)
      is
      begin
         return Input + 1;
      end Prot_Func;
   end Prot_Typ;

   task body Tsk_Typ is
   begin
      select
         accept Tsk_Entry (Input : Natural; Output : out Natural) do
            Output := Input + 1;
         end Tsk_Entry;
      or
         terminate;
      end select;
   end Tsk_Typ;
end Sync_Contracts;

--  main.adb

with Ada.Assertions; use Ada.Assertions;
with Ada.Text_IO;    use Ada.Text_IO;
with Sync_Contracts; use Sync_Contracts;
with Tracker;        use Tracker;

procedure Main is
   Result : Natural;

begin
   --  NOTES:
   --  1) Refined_Post does not work on entry bodies due to an implementation
   --     limitation.
   --  2) The consequences of Contract_Cases are mutually exclusive, only one
   --     should fail at any one time.

   declare
      P : Prot_Typ;
   begin
      --  Protected preconditions

      Put_Line ("Test 1");
      Reset;
      begin
         P.Prot_Entry (1, Result);
         Put_Line ("ERROR: Test 1: did not fail");
      exception
         when Assertion_Error => Verify ((True, False, False, False, False));
         when others => Put_Line ("ERROR: Test 1: unexpected error");
      end;

      Put_Line ("Test 2");
      Reset;
      begin
         P.Prot_Proc (1, Result);
         Put_Line ("ERROR: Test 2: did not fail");
      exception
         when Assertion_Error => Verify ((True, False, False, False, False));
         when others => Put_Line ("ERROR: Test 2: unexpected error");
      end;

      Put_Line ("Test 3");
      Reset;
      begin
         Result := P.Prot_Func (1);
         Put_Line ("ERROR: Test 3: did not fail");
      exception
         when Assertion_Error => Verify ((True, False, False, False, False));
         when others => Put_Line ("ERROR: Test 3: unexpected error");
      end;

      --  Protected refined postconditions

      Put_Line ("Test 4");
      Reset;
      begin
         P.Prot_Entry (2, Result);
         Put_Line ("ERROR: Test 4: did not fail");
      exception
         when Assertion_Error => Verify ((True, False, True, False, False));
         when others => Put_Line ("ERROR: Test 4: unexpected error");
      end;

      Put_Line ("Test 5");
      Reset;
      begin
         P.Prot_Proc (2, Result);
         Put_Line ("ERROR: Test 5: did not fail");
      exception
         when Assertion_Error => Verify ((True, True, False, False, False));
         when others => Put_Line ("ERROR: Test 5: unexpected error");
      end;

      Put_Line ("Test 6");
      Reset;
      begin
         Result := P.Prot_Func (2);
         Put_Line ("ERROR: Test 6: did not fail");
      exception
         when Assertion_Error => Verify ((True, True, False, False, False));
         when others => Put_Line ("ERROR: Test 6: unexpected error");
      end;

      --  Protected postconditions

      Put_Line ("Test 7");
      Reset;
      begin
         P.Prot_Entry (3, Result);
         Put_Line ("ERROR: Test 7: did not fail");
      exception
         when Assertion_Error => Verify ((True, False, True, False, False));
         when others => Put_Line ("ERROR: Test 7: unexpected error");
      end;

      Put_Line ("Test 8");
      Reset;
      begin
         P.Prot_Proc (3, Result);
         Put_Line ("ERROR: Test 8: did not fail");
      exception
         when Assertion_Error => Verify ((True, True, True, False, False));
         when others => Put_Line ("ERROR: Test 8: unexpected error");
      end;

      Put_Line ("Test 9");
      Reset;
      begin
         Result := P.Prot_Func (3);
         Put_Line ("ERROR: Test 9: did not fail");
      exception
         when Assertion_Error => Verify ((True, True, True, False, False));
         when others => Put_Line ("ERROR: Test 9: unexpected error");
      end;

      --  Protected contract cases

      Put_Line ("Test 10");
      Reset;
      begin
         P.Prot_Entry (5, Result);
         Put_Line ("ERROR: Test 10: did not fail");
      exception
         when Assertion_Error => Verify ((True, False, True, True, False));
         when others => Put_Line ("ERROR: Test 10: unexpected error");
      end;

      Put_Line ("Test 11");
      Reset;
      begin
         P.Prot_Entry (6, Result);
         Put_Line ("ERROR: Test 11: did not fail");
      exception
         when Assertion_Error => Verify ((True, False, True, False, True));
         when others => Put_Line ("ERROR: Test 11: unexpected error");
      end;

      Put_Line ("Test 12");
      Reset;
      begin
         P.Prot_Proc (5, Result);
         Put_Line ("ERROR: Test 12: did not fail");
      exception
         when Assertion_Error => Verify ((True, True, True, True, False));
         when others => Put_Line ("ERROR: Test 12: unexpected error");
      end;

      --  NOTE: 

      Put_Line ("Test 13");
      Reset;
      begin
         P.Prot_Proc (6, Result);
         Put_Line ("ERROR: Test 13: did not fail");
      exception
         when Assertion_Error => Verify ((True, True, True, False, True));
         when others => Put_Line ("ERROR: Test 13: unexpected error");
      end;

      Put_Line ("Test 14");
      Reset;
      begin
         Result := P.Prot_Func (5);
         Put_Line ("ERROR: Test 14: did not fail");
      exception
         when Assertion_Error => Verify ((True, True, True, True, False));
         when others => Put_Line ("ERROR: Test 14: unexpected error");
      end;

      Put_Line ("Test 15");
      Reset;
      begin
         Result := P.Prot_Func (6);
         Put_Line ("ERROR: Test 15: did not fail");
      exception
         when Assertion_Error => Verify ((True, True, True, False, True));
         when others => Put_Line ("ERROR: Test 15: unexpected error");
      end;
   end;

   --  Task entry precondition

   Put_Line ("Test 16");
   Reset;
   declare
      T : Tsk_Typ;
   begin
      T.Tsk_Entry (1, Result);
      Put_Line ("ERROR: Test 16: did not fail");
   exception
      when Assertion_Error => Verify ((True, False, False, False, False));
      when others => Put_Line ("ERROR: Test 16: unexpected error");
   end;

   --  Task entry postcondition

   Put_Line ("Test 17");
   Reset;
   declare
      T : Tsk_Typ;
   begin
      T.Tsk_Entry (3, Result);
      Put_Line ("ERROR: Test 17: did not fail");
   exception
      when Assertion_Error => Verify ((True, False, True, False, False));
      when others => Put_Line ("ERROR: Test 17: unexpected error");
   end;

   --  Task contract cases

   Put_Line ("Test 18");
   Reset;
   declare
      T : Tsk_Typ;
   begin
      T.Tsk_Entry (5, Result);
      Put_Line ("ERROR: Test 18: did not fail");
   exception
      when Assertion_Error => Verify ((True, False, True, True, False));
      when others => Put_Line ("ERROR: Test 18: unexpected error");
   end;

   Put_Line ("Test 19");
   Reset;
   declare
      T : Tsk_Typ;
   begin
      T.Tsk_Entry (6, Result);
      Put_Line ("ERROR: Test 19: did not fail");
   exception
      when Assertion_Error => Verify ((True, False, True, False, True));
      when others => Put_Line ("ERROR: Test 19: unexpected error");
   end;
end Main;

----------------------------
-- Compilation and output --
----------------------------

$ gnatmake -q -gnata main.adb
$ ./main
Test 1
Test 2
Test 3
Test 4
Test 5
Test 6
Test 7
Test 8
Test 9
Test 10
Test 11
Test 12
Test 13
Test 14
Test 15
Test 16
Test 17
Test 18
Test 19

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

2015-11-12  Hristian Kirtchev  <kirtchev@adacore.com>

	* contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract):
	Remove the guard concerning entry bodies as it is spurious.
	(Analyze_Entry_Or_Subprogram_Contract): Skip the analysis of
	Contract_Cases when not annotating the tree.
	* einfo.adb Node25 is now used as Contract_Wrapper.
	(Contract_Wrapper): New routine.
	(PPC_Wrapper): Removed.
	(Set_Contract_Wrapper): New routine.
	(Set_PPC_Wrapper): Removed.
	(Write_Field25_Name): Add output for Contract_Wrapper. Remove
	output for PPC_Wrapper.
	* einfo.ads New attribute Contract_Wrapper along with usage
	in entities. Remove attribute PPC_Wrapper along with usage in nodes.
	(Contract_Wrapper): New routine along with pragma Inline.
	(PPC_Wrapper): Removed along with pragma Inline.
	(Set_Contract_Wrapper): New routine along with pragma Inline.
	(Set_PPC_Wrapper): Removed along with pragma Inline.
	* exp_ch9.adb (Build_Contract_Wrapper): New routine.
	(Build_PPC_Wrapper): Removed.
	(Build_Protected_Entry): Code cleanup.
	(Expand_Entry_Declaration): Create a contract wrapper
	which now verifies Contract_Cases along with pre/postconditions.
	(Expand_N_Task_Type_Declaration): There is no need to check
	whether an entry has pre/postconditions as this is now done
	in Build_Contract_Wrapper.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Pragma
	Refined_Post is now properly inserted in entry bodies.
	(Insert_Pragma): Add circuitry to insert in an entry body. Redo
	the instance "header" circuitry. Remove the now obsolete special
	case of inserting pre- conditions.
	* sem_prag.adb (Analyze_Pragma): Pragma Contract_Cases now
	applies to entries.
	* sem_res.adb (Resolve_Entry_Call): Update the calls to
	PPC_Wrapper.

Attachment: difs
Description: Text document