+ pdecformal.pas - Parsing of declarations in formal annotation.

  For now, only propositions will be accepted, but pre-/postconditions and
  specification variables are planned.
* pexpr.pas now has support for (declared!) propositions in expressions (only
  within formal annotation)
* There is a new metatype, TPropositionSym.
* tscannerfile has a new attribute, "in_formal_annotation", and the scanner
  uses {$FORMAL+} and {$FORMAL-} to activate/deactivate parsing of formal annotation.
(Jochem Berndsen <[email protected]>)

git-svn-id: branches/tue@4841 -

.gitattributes

@@ -273,6 +273,7 @@ compiler/parser.pas svneol=native#text/plain
 compiler/pass_1.pas svneol=native#text/plain
 compiler/pass_2.pas svneol=native#text/plain
 compiler/pbase.pas svneol=native#text/plain
+compiler/pdecformal.pas svneol=native#text/plain
 compiler/pdecl.pas svneol=native#text/plain
 compiler/pdecobj.pas svneol=native#text/plain
 compiler/pdecsub.pas svneol=native#text/plain

compiler/msg/errore.msg

@@ -326,7 +326,7 @@ scan_n_app_type_not_support=02073_N_APPTYPE is not supported by the target OS
 #
 # Parser
 #
-# 03219 is the last used one
+# 03220 is the last used one
 #
 % \section{Parser messages}
 % This section lists all parser messages. The parser takes care of the
@@ -1054,6 +1054,8 @@ parser_w_overridden_methods_not_same_ret=03218_W_Overridden methods must have a
 parser_w_formal_annotation_not_compiled=03219_W_Formal annotation will not be compiled into an assert statement (use -Sa)
 % Formal annotation was encountered, but run-time assertion checking is not
 % switched on; only the syntax of the formal annotation will be checked.
+parser_e_invalid_formal_annotation=03220_E_Invalid formal annotation
+% A syntax error was encountered in formal annotation.
 % \end{description}
 #
 # Type Checking

compiler/msgidx.inc

@@ -291,6 +291,7 @@ const
   parser_e_dispinterface_needs_a_guid=03217;
   parser_w_overridden_methods_not_same_ret=03218;
   parser_w_formal_annotation_not_compiled=03219;
+  parser_e_invalid_formal_annotation=03220;
   type_e_mismatch=04000;
   type_e_incompatible_types=04001;
   type_e_not_equal_types=04002;

compiler/pdecformal.pas

@@ -0,0 +1,169 @@
+{
+    Copyright (c) 1998-2002 by Eindhoven University of Technology
+
+    Parses formal annotation in declarations.
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program; if not, write to the Free Software
+    Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+
+ ****************************************************************************
+}
+unit pdecformal;
+
+{$i fpcdefs.inc}
+
+interface
+  
+    uses
+      symsym, symdef;
+
+    procedure read_formal_decs;
+
+implementation
+  
+    uses
+       { common }
+       cutils,cclasses,
+       { global }
+       globtype,globals,tokens,verbose,
+       systems,
+       { symtable }
+       symconst,symbase,symtype,symtable,defutil,defcmp,
+       fmodule,
+       { pass 1 }
+       node,pass_1,
+       nmat,nadd,ncal,nset,ncnv,ninl,ncon,nld,nflw,nmem,
+       { codegen }
+       ncgutil,
+       { parser }
+       scanner,
+       pbase,pexpr,ptype,ptconst,pdecsub,
+       { link }
+       import,
+       { exceptions }
+       sysutils
+       ;
+
+
+    procedure read_proposition; forward;
+    procedure read_specvar; forward;
+    procedure read_precondition; forward;
+    procedure read_postcondition; forward;
+
+    type
+      EInvalidAnnotation = class(Exception);
+
+    procedure read_formal_decs;
+    { Reads the formal declarations of specification variables ('specvar's),
+    propositions, pre- and postconditions into a symtablestack. }
+      begin
+        if (token=_CLOSE_FORMAL) then
+          begin
+            consume(_CLOSE_FORMAL);
+            exit;
+          end;
+
+        try
+          repeat
+            { expect "def", "specvar", "pre" or "post" }
+            if (token<>_ID) then
+              consume(_ID);
+
+            if upcase(pattern)='DEF' then
+              begin
+                consume(_ID);
+                read_proposition;
+              end
+            else if upcase(pattern)='SPECVAR' then
+              begin
+                consume(_ID);
+                read_specvar;
+              end
+            else if upcase(pattern)='PRE' then
+              begin
+                consume(_ID);
+                read_precondition;
+              end
+            else if upcase(pattern)='POST' then
+              begin
+                consume(_ID);
+                read_postcondition;
+              end
+            else
+              begin
+                raise EInvalidAnnotation.Create('specvar, pre, post or def expected');
+              end;
+
+          until not try_to_consume(_SEMICOLON);
+          consume(_CLOSE_FORMAL);
+
+        except
+          on e: EInvalidAnnotation do
+            begin
+              { Consume the whole annotation }
+              while token<>_CLOSE_FORMAL do
+                consume(token);
+              consume(_CLOSE_FORMAL);
+              Message1(parser_e_invalid_formal_annotation, e.message);
+            end;
+        end; { try..except }
+      
+      end; { procedure read_formal_decs }
+    
+    procedure read_proposition;
+      var
+        prop_name : string;
+        expr : tnode;
+        vs : tabstractvarsym;
+      begin
+        { parse P : expression }
+        prop_name := pattern;
+        consume(_ID);
+        consume(_COLON);
+        expr:=comp_expr(true);
+        do_resulttypepass(expr);
+        if not is_boolean(expr.resulttype.def) then
+          begin
+            Message1(type_e_boolean_expr_expected, expr.resulttype.def.typename);
+            exit;
+          end;
+        if not(symtablestack.symtabletype in [localsymtable,globalsymtable]) then
+          begin
+            { TODO : more descriptive error message }
+            raise EInvalidAnnotation.Create('Proposition definition outside local '+
+            'or global declaration context');
+          end;
+        vs:=tpropositionsym.create(prop_name, expr.resulttype, expr);
+        symtablestack.insert(vs);
+      end;
+
+    procedure read_specvar;
+      begin
+        raise EInvalidAnnotation.Create('Specification variables are not yet implemented');
+      end;
+
+    procedure read_precondition;
+      begin
+        raise EInvalidAnnotation.Create('Pre-/postconditions are not yet implemented');
+      end;
+
+    procedure read_postcondition;
+      begin
+        raise EInvalidAnnotation.Create('Pre-/postconditions are not yet implemented');
+      end;
+
+end.
+
+
+

compiler/pdecl.pas

@@ -42,6 +42,7 @@ interface
     procedure threadvar_dec;
     procedure property_dec;
     procedure resourcestring_dec;
+    procedure formal_dec;
 
 implementation
 
@@ -61,9 +62,10 @@ implementation
        ncgutil,
        { parser }
        scanner,
-       pbase,pexpr,ptype,ptconst,pdecsub,pdecvar,pdecobj,
+       pbase,pexpr,ptype,ptconst,pdecsub,pdecvar,pdecobj,pdecformal,
        { cpu-information }
-       cpuinfo
+       cpuinfo,
+       pass_1
        ;
 
 
@@ -583,6 +585,12 @@ implementation
         read_var_decs(false,false,false);
       end;
 
+    procedure formal_dec;
+      begin
+        consume(_OPEN_FORMAL);
+        read_formal_decs;
+      end;
+
 
     procedure property_dec;
       var

compiler/pexpr.pas

@@ -1273,6 +1273,17 @@ implementation
                       p1:=cloadnode.create(srsym,srsymtable);
                   end;
 
+                propositionsym:
+                  begin
+                    if (current_scanner.in_formal_annotation) then
+                      p1:=tpropositionsym(srsym).expr.getcopy
+                    else
+                      begin
+                        p1:=cerrornode.create;
+                        Message(parser_e_illegal_expression);
+                      end;
+                  end;
+
                 globalvarsym,
                 localvarsym,
                 paravarsym,

compiler/psub.pas

@@ -1401,6 +1401,8 @@ implementation
                 var_dec;
               _THREADVAR:
                 threadvar_dec;
+              _OPEN_FORMAL:
+                formal_dec;
               _CONSTRUCTOR,
               _DESTRUCTOR,
               _FUNCTION,

compiler/scanner.pas

@@ -89,6 +89,7 @@ interface
           ignoredirectives : tstringlist; { ignore directives, used to give warnings only once }
           preprocstack   : tpreprocstack;
           in_asm_string  : boolean;
+          in_formal_annotation : boolean;
 
           preproc_pattern : string;
           preproc_token   : ttoken;
@@ -1423,17 +1424,15 @@ In case not, the value returned can be arbitrary.
       end;
 
     procedure dir_formal;
-    (* Parse comments of the form {$FORMAL ON} and {$FORMAL OFF}
+    (* Parse comments of the form {$FORMAL+} and {$FORMAL-}
     *)
     var
       s : string;
     begin
-      current_scanner.skipspace;
       s:=current_scanner.readcomment;
-      s:=upcase(s);
-      if (s='ON') then 
+      if (s='+') then 
          include(aktlocalswitches,cs_formal_annotation)
-      else if (s='OFF') then
+      else if (s='-') then
          exclude(aktlocalswitches,cs_formal_annotation)
       else
          Message1(scan_w_illegal_switch,'$FORMAL '+s);
@@ -1689,6 +1688,7 @@ In case not, the value returned can be arbitrary.
         lastasmgetchar:=#0;
         ignoredirectives:=TStringList.Create;
         in_asm_string:=false;
+        in_formal_annotation:=false;
       end;
 
 
@@ -2745,6 +2745,7 @@ In case not, the value returned can be arbitrary.
               dec_comment_level;
               readchar;
               nexttoken:=_OPEN_FORMAL;
+              in_formal_annotation:=true;
               exit;
             end;
          end;
@@ -3001,6 +3002,7 @@ In case not, the value returned can be arbitrary.
                   begin
                     readchar;
                     token:=_CLOSE_FORMAL;
+                    in_formal_annotation:=false;
                     goto exit_label;
                   end
                  else

compiler/symconst.pas

@@ -365,7 +365,8 @@ type
   tsymtyp = (abstractsym,globalvarsym,localvarsym,paravarsym,fieldvarsym,
              typesym,procsym,unitsym,constsym,enumsym,typedconstsym,
              errorsym,syssym,labelsym,absolutevarsym,propertysym,
-             macrosym,rttisym);
+             macrosym,rttisym,
+             propositionsym);
 
   { State of the variable, if it's declared, assigned or used }
   tvarstate=(vs_none,
@@ -434,7 +435,7 @@ const
        'abstractsym','globalvar','localvar','paravar','fieldvar',
        'type','proc','unit','const','enum','typed const',
        'errorsym','system sym','label','absolutevar','property',
-       'macrosym','rttisym'
+       'macrosym','rttisym', 'proposition'
      );
 
      DefTypeName : array[tdeftype] of string[12] = (

compiler/symsym.pas

@@ -36,7 +36,8 @@ interface
        cclasses,symnot,
        { aasm }
        aasmbase,aasmtai,
-       cpuinfo,cpubase,cgbase,cgutils,parabase
+       cpuinfo,cpubase,cgbase,cgutils,parabase,
+       node
        ;
 
     type
@@ -207,6 +208,11 @@ interface
 {$endif GDB}
       end;
 
+      tpropositionsym = class(tabstractnormalvarsym)
+          expr : tnode;
+          constructor create(const n : string; const tt : ttype; aexpr : tnode);
+      end;
+
       tparavarsym = class(tabstractnormalvarsym)
           paraloc       : array[tcallercallee] of TCGPara;
           paranr        : word; { position of this parameter }
@@ -404,8 +410,6 @@ implementation
        systems,
        { symtable }
        defutil,symtable,
-       { tree }
-       node,
        { aasm }
 {$ifdef gdb}
        gdb,
@@ -1727,6 +1731,19 @@ implementation
     end;
 {$endif GDB}
 
+{****************************************************************************
+                               TPROPOSITIONSYM
+****************************************************************************}
+
+    constructor tpropositionsym.create(const n : string; const tt: ttype; aexpr : tnode);
+      begin
+        if not is_boolean(tt.def) then
+          internalerror(20061009);
+        inherited create(n, vs_value, tt, []);
+        expr:=aexpr;
+        typ:=propositionsym;
+      end;
+
 
 {****************************************************************************
                                TLOCALVARSYM