This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Aspect Depends


This patch provides the initial implementation of aspect Depends. This
construct is intended for formal verification proofs.

The syntax of the aspect is as follows:

   DEPENDENCY_RELATION ::= null
                         | DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}
   DEPENDENCY_CLAUSE   ::= OUTPUT_LIST =>[+] INPUT_LIST
   OUTPUT_LIST         ::= null
                         | OUTPUT
                         | (OUTPUT {, OUTPUT})
   INPUT_LIST          ::= null
                         | INPUT
                         | (INPUT {, INPUT})
   OUTPUT              ::= NAME | FUNCTION_RESULT
   INPUT               ::= NAME

where FUNCTION_RESULT is a function Result attribute_reference

The semantics of the aspect are as follows:

Every input and output of a dependency_relation of a Depends aspect of a
subprogram denotes a state abstraction, an entire variable or a formal
parameter of the subprogram.

An input must have a mode of in or in out and an output must have an mode of in
out or out. [Note: As a consequence an entity which is both an input and an
output shall have a mode of in out.]

For the purposes of determining the legality of a Result attribute_reference, a
dependency_relation is considered to be a postcondition of the function to
which the enclosing aspect_specification applies.

There can be at most one output_list which is a null symbol and if it exists it
must be the output_list of the last dependency_clause in the
dependency_relation. An input which is in an input_list of a null output_list
may not appear in another input_list of the same dependency_relation.

The entity denoted by an output in an output_list shall not be denoted by any
other output in that output_list or any other output_list.

The entity denoted by an input in an input_list shall not be denoted by any
other input in that input_list.

Every output of the subprogram shall appear in exactly one output_list. Every
input of the subprogram shall appear in at least one input_list.

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

--  types.ads

package Types is
   type Rec is record
      Comp : Natural;
   end record;
   type Arr is array (1 .. 5) of Rec;
   function Get_Comp (Obj : Rec) return Natural;
end Types;

--  types.adb

package body Types is
   function Get_Comp (Obj : Rec) return Natural is
   begin
      return Obj.Comp;
   end Get_Comp;
end Types;

--  semantics.ads

with Types; use Types;

package Semantics with
   Abstract_State => State
is
   Arr_Obj : Arr;
   Rec_Obj : Rec;

   --  Renaming chain of an object

   Ren_1 : Rec renames Rec_Obj;
   Ren_2 : Rec renames Ren_1;

   --  Renaming of a record component

   Ren_3 : Natural renames Rec_Obj.Comp;

   --  Renaming of an array element

   Ren_4 : Rec renames Arr_Obj (3);

   --  Renaming of a function call result

   Ren_5 : Natural renames Get_Comp (Rec_Obj);

   --  Legality rules
   --  1. Every input and output of a dependency_relation of a Depends aspect
   --  of a subprogram denotes a state abstraction, an entire variable or a
   --  formal parameter of the subprogram.

   procedure OK_1a (Formal : Natural; Result : out Natural)
      with Depends =>
        (Result =>
          (State,     --  abstract state
           Arr_Obj,   --  object
           Rec_Obj,   --  object
           Formal));  --  formal

   procedure OK_1b (Result : out Natural)
      with Depends => (Result => Ren_1);  --  renaming of object

   procedure OK_1c (Result : out Natural)
      with Depends => (Result => Ren_2);  --  renaming of renaming of object

   procedure Error_1 (Result : out Natural)
      with Depends =>
        (Result =>
          (Arr_Obj (3),         --  element
           Rec_Obj.Comp,        --  component
           Get_Comp (Rec_Obj),  --  function call
           Ren_3,               --  renaming of component
           Ren_4,               --  renaming of element
           Ren_5,               --  renaming of function call result
           1234));              --  junk

   --  Legality rules
   --  3. For the purposes of determining the legality of a Result
   --  attribute_reference, a dependency_relation is considered to
   --  be a postcondition of the function to which the enclosing
   --  aspect_specification applies.

   function OK_3 return Natural
      with Depends =>
        (OK_3'Result => Rec_Obj);  --  'Result is an output

   function Error_3a (Result : out Natural) return Natural
      with Depends =>
        (Result => Error_3a'Result);  --  'Result is an input

   function Error_3b (Formal : Natural) return Natural
      with Depends =>
        (Get_Comp (Rec_Obj)'Result => Formal);  --  'Result must apply to the
                                                --  enclosing function

   --  Legality rules
   --  4. There can be at most one output_list which is a null symbol and if it
   --  exists it must be the output_list of the last dependency_clause in the
   --  dependency_relation.

   procedure OK_4a (Formal : Natural; Result : out Natural)
      with Depends =>
        (Result => Formal,
         null   => Rec_Obj);  --  null is last output_list

   function Error_4a (Formal : Natural) return Natural
      with Depends =>
        (null            => Arr_Obj,  --  null is not the last output_list
         Error_4a'Result => Formal);

   --  Legality rules
   --  4. An input which is in an input_list of a null output_list may not
   --  appear in another input_list of the same dependency_relation.

   procedure OK_4b (Formal : Natural; Result : out Natural)
      with Depends =>
        (Result => Ren_1,
         null   => Formal);

   procedure Error_4b (Formal : Natural; Result : out Natural)
      with Depends =>
        (Result => Formal,
         null   => Formal);  --  Formal appears in both output_lists

   --  Legality rules
   --  5. The entity denoted by an output in an output_list shall not
   --  be denoted by any other output in that output_list or any other
   --  output_list.

   procedure OK_5a (Result_1 : out Natural; Result_2 : out Natural)
      with Depends =>
        ((Result_1, Result_2) => Ren_2);

   procedure OK_5b (Result_1 : out Natural; Result_2 : out Natural)
      with Depends =>
        (Result_1 => Arr_Obj,
         Result_2 => Rec_Obj);

   procedure Error_5 (Result_1 : out Natural; Result_2 : out Natural)
      with Depends =>
        ((Result_1, Result_2, Result_1) => Arr_Obj,  --  Result_1 appears twice
          Result_2 => Ren_1);  --  Result_2 is already in the first input_list

   --  Legality rules
   --  6. The entity denoted by an input in an input_list shall not be denoted
   --  by any other input in that input_list.

   function OK_6 (Result : out Natural) return Natural
      with Depends =>
        (Result      => (Rec_Obj, Arr_Obj),
         OK_6'Result =>  Rec_Obj);

   procedure Error_6 (Result : out Natural)
      with Depends =>
        (Result =>
          (Rec_Obj, Ren_1, Ren_2));  --  All inputs are the same object

   --  Extra checks

   procedure Error_E1
      (Formal   : Natural;
       Result_1 : out Natural;
       Result_2 : out Natural;
       Result_3 : out Natural)
   with Depends =>
      ((Result_1, (Result_2, Result_3)) => (Formal, (Arr_Obj, Rec_Obj)));
   --  Cannot have nested groupings such as (Result_2, Result_3)

end Semantics;

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

$ gcc -c -gnat12 -gnatd.V semantics.ads
semantics.ads:48:12: item must denote variale, state or formal parameter
semantics.ads:49:19: item must denote variale, state or formal parameter
semantics.ads:50:12: item must denote variale, state or formal parameter
semantics.ads:51:12: item must denote variale, state or formal parameter
semantics.ads:52:12: item must denote variale, state or formal parameter
semantics.ads:53:12: item must denote variale, state or formal parameter
semantics.ads:54:12: item must denote variale, state or formal parameter
semantics.ads:68:28: function result cannot act as input
semantics.ads:72:28: prefix of attribute "Result" must denote the enclosing
  function
semantics.ads:87:10: null output list must be the last clause in a dependency
  relation
semantics.ads:102:20: input of a null output list appears in multiple input
  lists
semantics.ads:120:31: duplicate use of item
semantics.ads:121:11: duplicate use of item
semantics.ads:135:21: duplicate use of item
semantics.ads:135:28: duplicate use of item
semantics.ads:145:19: nested grouping of items not allowed
semantics.ads:145:53: nested grouping of items not allowed

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

2013-04-11  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.ads, aspects.adb: Add Aspect_Depends to all the relevant
	tables.
	* elists.ads, elists.adb (Contains): New routine.
	* par-prag.adb: Pragma Depends does not need any special treatment
	by the parser.
	* sem_ch13.adb (Analyze_Aspect_Specifications):
	Transform aspect Depends into a corresponding pragma.
	(Check_Aspect_At_Freeze_Point): Aspect Depends does not need
	inspection at its freeze point.
	* sem_prag.adb (Analyze_Pragma): Perform analysis and
	normalization of pragma Depends. Remove the use of function
	Is_Duplicate_Item. Use End_Scope to uninstalle the formal
	parameters of a subprogram. Add a value for pragma Depends in
	table Sig_Flags.
	(Is_Duplicate_Item): Removed.
	* snames.ads-tmpl: Add predefined name for Depends as well as
	a pragma identifier.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]