* tobjectdef has now an attribute "invariant", with the class invariants.

* tsubscriptnode can now have a NIL left. If so, it is filled with the current
  "self" pointer later on. For example:
  type o = class
    procedure foo;
    x : Integer;
    {...}
    {@ inv I0 = x > 0 }
  end;
  While parsing, "x" is not "bound" to an object, but when checking the class
  invariants in methods, an object is created and x is an attribute of an 
  actual object.
* Specvars are now implemented. The following:
    function sqr(const x : integer): integer;
    {@ specvar oldx = x;
       post = x * x = oldx
    }
    begin result:=x*x end;
    is a correct specification.
  Specvars are implemented as local variables, but it is an error (the compiler
  will fail to compile it) to use a specification variable outside the annotation.
* In class declarations, formal annotation of the form
   {@ inv IDENTIFIER = BOOLEAN_EXPRESSION } is allowed.
  The expression will be checked in run-time (if asserts are on),
  as the precondition and postcondition of each (public, non-static!!) method.
  Exceptions: not before the constructor, and after the destructor.
  I assume the pre-check will be left out later (assuming that the "outside world"
  cannot invalidate the invariant, this is correct).
* Arbitrarily typed definitions are now supported, and "propositions" are boolean
  definitions.
* Some syntax changes in the procedure/function-header part:
  specvar ID [:TYPE] = EXPR {, ID [:TYPE] = EXPR}*
  pre = EXPR
  post = EXPR
  def ID [:TYPE] = EXPR {, ID [:TYPE] = EXPR}*
 
(Jochem Berndsen <[email protected]>)

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

compiler/nmem.pas

@@ -578,9 +578,13 @@ implementation
     function tsubscriptnode.det_resulttype:tnode;
       begin
         result:=nil;
-        resulttypepass(left);
-        { tp procvar support }
-        maybe_call_procvar(left,true);
+        if assigned(left) then
+          begin
+            resulttypepass(left);
+            { tp procvar support }
+            maybe_call_procvar(left,true);
+          end;
+
         resulttype:=vs.vartype;
       end;
 

compiler/nobj.pas

@@ -30,7 +30,8 @@ interface
        cutils,cclasses,
        globtype,
        symdef,symsym,
-       aasmbase,aasmtai
+       aasmbase,aasmtai,
+       node
        ;
 
     type
@@ -104,6 +105,8 @@ interface
         procedure gintfdoonintf(intf: tobjectdef; intfindex: longint);
         procedure gintfwalkdowninterface(intf: tobjectdef; intfindex: longint);
       public
+        invariant : tnode;
+
         constructor create(c:tobjectdef);
         destructor destroy;override;
         { generates the message tables for a class }
@@ -144,6 +147,7 @@ implementation
       begin
         inherited Create;
         _Class:=c;
+        invariant:=nil;
       end;
 
 

compiler/pdecformal.pas

@@ -28,7 +28,13 @@ interface
     uses
       symsym, symdef;
 
+    { Read the formal declaration in procedure/function/method "headers"
+    and in the main program }
     procedure read_formal_decs;
+    
+    { Read the formal declaration in class declarations }
+    procedure read_formal_decs_in_class;
+
 
 implementation
   
@@ -58,7 +64,7 @@ implementation
        ;
 
 
-    procedure read_proposition; forward;
+    procedure read_definition; forward;
     procedure read_specvar; forward;
     procedure read_precondition; forward;
     procedure read_postcondition; forward;
@@ -86,7 +92,7 @@ implementation
             if upcase(pattern)='DEF' then
               begin
                 consume(_ID);
-                read_proposition;
+                read_definition;
               end
             else if upcase(pattern)='SPECVAR' then
               begin
@@ -129,72 +135,103 @@ implementation
       
       end; { procedure read_formal_decs }
     
-    procedure read_proposition;
+    procedure read_definition;
       var
-        prop_name : string;
-        expr : tnode;
-        vs : tabstractvarsym;
+        def_name : string;
+        def_type : ttype;
+        def_expr : tnode;
+        def : tabstractvarsym;
+        type_given : boolean;
+        prev_ignore_equal : boolean;
       begin
-        { parse P : expression }
+        { parse A[,A]*, where A::= P [: TYPE ] = EXPRESSION }
         repeat
-          prop_name:=pattern;
+          def_name:=pattern;
           consume(_ID);
-          consume(_COLON);
-          expr:=comp_expr_in_formal_context(true);
-          do_resulttypepass(expr);
-          if not is_boolean(expr.resulttype.def) then
+          
+          if try_to_consume(_COLON) then
             begin
-              Message1(type_e_boolean_expr_expected, expr.resulttype.def.typename);
-              exit;
-            end;
-          if not(symtablestack.symtabletype in [localsymtable,globalsymtable]) then
+              prev_ignore_equal:=ignore_equal;
+              ignore_equal:=true;{ Signals to read_type to ignore the = token }
+              read_type(def_type, '', false);
+              ignore_equal:=prev_ignore_equal;
+              type_given:=true;
+            end
+          else
+            type_given:=false;
+
+          consume(_EQUAL);
+
+          def_expr:=comp_expr_in_formal_context(true);
+          do_resulttypepass(def_expr);
+
+          if type_given then
+            { Match the given type and the type of the expression }
+            inserttypeconv(def_expr, def_type)
+          else
+            { Use the computed type of the expression }
+            def_type:=def_expr.resulttype;
+
+          if not(symtablestack.symtabletype in [localsymtable,globalsymtable,staticsymtable]) then
             begin
               { TODO : more descriptive error message }
               raise EInvalidAnnotation.Create('Proposition definition outside local '+
               'or global declaration context');
             end;
-          vs:=tspecvarsym.create(prop_name, expr.resulttype { Boolean }, expr);
-          symtablestack.insert(vs);
+          def:=tdefinitionsym.create(def_name, def_type, def_expr);
+          symtablestack.insert(def);
         until not try_to_consume(_COMMA);
       end;
 
     procedure read_specvar;
       var
+        sv : tspecvarsym;
         sv_name : string;
         sv_type : ttype;
         sv_expr : tnode;
-        sv      : tabstractvarsym;
         type_given : boolean;
         prev_ignore_equal : boolean;
       begin
+        { parse A[,A]* where A::= ID[:TYPE] = EXPRESSION }
         repeat
-          { parse P [: type] = expression }
           sv_name:=pattern;
           consume(_ID);
-          { Is a type given ? }
+
           if try_to_consume(_COLON) then
             begin
+              type_given:=true;
               prev_ignore_equal:=ignore_equal;
-              ignore_equal:=true; { Signals to read_type to ignore the = token }
+              ignore_equal:=true; { Signals to read_type that the = token
+                should be ignored }
               read_type(sv_type, '', false);
               ignore_equal:=prev_ignore_equal;
-              type_given:=true;
             end
           else
             type_given:=false;
-            
+
           consume(_EQUAL);
-          { Parse the expression }
-          sv_expr:=comp_expr(true);
+
+          sv_expr:=comp_expr_in_formal_context(true);
           do_resulttypepass(sv_expr);
+
           if type_given then
             { Match the given type and the type of the expression }
             inserttypeconv(sv_expr, sv_type)
           else
-            { Set the type to the type of the expression } 
+            { Use the computed type of the expression }
             sv_type:=sv_expr.resulttype;
+
+          if not(symtablestack.symtabletype in [localsymtable,globalsymtable,staticsymtable]) then
+            raise EInvalidAnnotation.Create('Specvars can only be defined in local or global contexts');
+
           sv:=tspecvarsym.create(sv_name, sv_type, sv_expr);
           symtablestack.insert(sv);
+
+          if (not assigned(current_procinfo)) or (not assigned(current_procinfo.procdef)) then
+            raise EInvalidAnnotation.Create('Specvars cannot be defined here');
+
+          current_procinfo.procdef.specvars.Add(sv);
+
         until not try_to_consume(_COMMA);
       end;
 
@@ -203,7 +240,7 @@ implementation
       var
         expr : tnode;
       begin
-        consume(_COLON);
+        consume(_EQUAL);
         expr:=comp_expr_in_formal_context(true);
         { Check here the result type of the expression.
         This will be checked later on as well (after conversion to "assert"),
@@ -225,7 +262,7 @@ implementation
       var
         expr : tnode;
       begin
-        consume(_COLON);
+        consume(_EQUAL);
         expr:=comp_expr_in_formal_context(true);
         { Check here the result type of the expression.
         This will be checked later on as well (after conversion to "assert"),
@@ -249,7 +286,7 @@ implementation
         evald : tnode;
         rst : tnode;
       begin
-        consume(_COLON);
+        consume(_EQUAL);
         { Proposition variables are not allowed here }
         expr:=comp_expr(true);
         { Convert this to "Result = expr" } 
@@ -264,6 +301,53 @@ implementation
         current_procinfo.procdef.postcondition:=evald;  
       end;
 
+
+    procedure read_formal_decs_in_class;
+
+      var
+        inv_name : string;
+        inv_expr : tnode;
+
+      begin
+        if not (try_to_consume(_CLOSE_FORMAL)) then
+          begin
+            try
+              if (upcase(pattern)<>'INV') then
+                raise EInvalidAnnotation.Create('inv expected');
+              consume(_ID);
+
+              inv_name:=pattern;
+              consume(_ID);
+
+              consume(_EQUAL);
+
+              inv_expr:=comp_expr_in_formal_context_class_header(true);
+
+              do_resulttypepass(inv_expr);
+              if not is_boolean(inv_expr.resulttype.def) then
+                raise EInvalidAnnotation.Create('boolean expression expected');
+
+              if assigned(aktobjectdef.invariant) then
+                aktobjectdef.invariant:=caddnode.create(andn,
+                  aktobjectdef.invariant,
+                  inv_expr)
+              else
+                aktobjectdef.invariant:=inv_expr;
+
+
+              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; { on EInvalidAnnotation }
+            end; { try..except }
+          end; { if not try_to_consume(_CLOSE_FORMAL) }
+      end;
 end.
 
 

compiler/pdecobj.pas

@@ -39,7 +39,7 @@ implementation
       symconst,symbase,symsym,
       node,nld,nmem,ncon,ncnv,ncal,
       scanner,
-      pbase,pexpr,pdecsub,pdecvar,ptype
+      pbase,pexpr,pdecsub,pdecvar,ptype,pdecformal
       ;
 
     const
@@ -476,6 +476,7 @@ implementation
       var
         pd : tprocdef;
         dummysymoptions : tsymoptions;
+
       begin
          old_object_option:=current_object_option;
 
@@ -654,6 +655,11 @@ implementation
 
                     parse_only:=oldparse_only;
                   end;
+                _OPEN_FORMAL :
+                  begin
+                    consume(_OPEN_FORMAL);
+                    read_formal_decs_in_class;
+                  end;
                 _CONSTRUCTOR :
                   begin
                     if (sp_published in current_object_option) and

compiler/pexpr.pas

@@ -35,9 +35,18 @@ interface
 
     { reads an expression without assignements and .. }
     function comp_expr(accept_equal : boolean):tnode;
+
     { reads an expression without assignments and .., but with
-    proposition syms, ... }
+    definition syms, specvars }
     function comp_expr_in_formal_context(accept_equal : boolean):tnode;
+    
+    { reads an expression without assignments and .., but with
+    definition syms and specvars.
+    Furthermore, for fields of classes/records a csubscriptnode is created,
+    but the "left" pointer of this node is set to NIL }
+    function comp_expr_in_formal_context_class_header(
+      accept_equal : boolean): tnode;
+
 
     { reads a single factor }
     function factor(getaddr : boolean) : tnode;
@@ -80,7 +89,12 @@ implementation
        ;
 
     var
+      { Initially false, is set to true iff the expression is 
+      in a formal context (i.e. within _OPEN_FORMAL and _CLOSE_FORMAL) }
       in_formal_context : boolean;
+      { Initially false, is set to true iff in_formal_context and
+      we are in a class header (thus in_class_header implies in_formal_context) }
+      in_class_header : boolean;
 
     { sub_expr(opmultiply) is need to get -1 ** 4 to be
       read as - (1**4) and not (-1)**4 PM }
@@ -1281,7 +1295,7 @@ implementation
                       p1:=cloadnode.create(srsym,srsymtable);
                   end;
 
-                specvarsym:
+                definitionsym:
                   begin
                     if not in_formal_context then
                       begin
@@ -1289,49 +1303,61 @@ implementation
                         Message(parser_e_illegal_expression);
                       end
                     else
-                      p1:=tspecvarsym(srsym).expr.getcopy
+                      p1:=tdefinitionsym(srsym).expr.getcopy
                   end;
 
+
                 globalvarsym,
                 localvarsym,
                 paravarsym,
                 fieldvarsym :
                   begin
-                    if (sp_static in srsym.symoptions) then
-                     begin
-                       static_name:=lower(srsym.owner.name^)+'_'+srsym.name;
-                       searchsym(static_name,srsym,srsymtable);
-		       if assigned(srsym) then
-                         check_hints(srsym,srsym.symoptions);
-                     end
+                    if (srsym is tspecvarsym) and not in_formal_context then
+                      begin
+                        p1:=cerrornode.create;
+                        Message(parser_e_illegal_expression);
+                      end
                     else
-                     begin
-                       { are we in a class method, we check here the
-                         srsymtable, because a field in another object
-                         also has objectsymtable. And withsymtable is
-                         not possible for self in class methods (PFV) }
-                       if (srsymtable.symtabletype=objectsymtable) and
-                          assigned(current_procinfo) and
-                          (po_classmethod in current_procinfo.procdef.procoptions) then
-                         Message(parser_e_only_class_methods);
-                     end;
+                      begin
+                        if (sp_static in srsym.symoptions) then
+                         begin
+                           static_name:=lower(srsym.owner.name^)+'_'+srsym.name;
+                           searchsym(static_name,srsym,srsymtable);
+                		       if assigned(srsym) then
+                             check_hints(srsym,srsym.symoptions);
+                         end
+                        else
+                         begin
+                         { are we in a class method, we check here the
+                           srsymtable, because a field in another object
+                           also has objectsymtable. And withsymtable is
+                           not possible for self in class methods (PFV) }
+                           if (srsymtable.symtabletype=objectsymtable) and
+                              assigned(current_procinfo) and
+                              (po_classmethod in current_procinfo.procdef.procoptions) then
+                             Message(parser_e_only_class_methods);
+                         end;
 
-                    case srsymtable.symtabletype of
-                      objectsymtable :
-                        begin
-                          p1:=csubscriptnode.create(srsym,load_self_node);
-                          node_tree_set_filepos(p1,aktfilepos);
-                        end;
-                      withsymtable :
-                        begin
-                          p1:=csubscriptnode.create(srsym,tnode(twithsymtable(srsymtable).withrefnode).getcopy);
-                          node_tree_set_filepos(p1,aktfilepos);
+                        case srsymtable.symtabletype of
+                          objectsymtable :
+                            begin
+                              if in_class_header then
+                                p1:=csubscriptnode.create(srsym,nil)
+                              else
+                                p1:=csubscriptnode.create(srsym,load_self_node);
+                              node_tree_set_filepos(p1,aktfilepos);
+                            end;
+                          withsymtable :
+                            begin
+                              p1:=csubscriptnode.create(srsym,tnode(twithsymtable(srsymtable).withrefnode).getcopy);
+                              node_tree_set_filepos(p1,aktfilepos);
+                            end;
+                          else
+                            p1:=cloadnode.create(srsym,srsymtable);
                         end;
-                      else
-                        p1:=cloadnode.create(srsym,srsymtable);
-                    end;
+                      end;
                   end;
-
+    
                 typedconstsym :
                   begin
                     p1:=cloadnode.create(srsym,srsymtable);
@@ -2612,6 +2638,18 @@ implementation
         comp_expr_in_formal_context:=comp_expr(accept_equal);
         in_formal_context:=prev;
       end;
+    
+    function comp_expr_in_formal_context_class_header(accept_equal : boolean)
+      : tnode;
+
+      var
+        prev : boolean;
+      begin
+        prev:=in_class_header;
+        in_class_header:=true;
+        result:=comp_expr_in_formal_context(accept_equal);
+        in_class_header:=prev;
+      end;
 
     function comp_expr(accept_equal : boolean):tnode;
       var
@@ -2741,5 +2779,6 @@ implementation
 
 initialization
     in_formal_context:=false;
+    in_class_header:=false;
 
 end.

compiler/psub.pas

@@ -251,6 +251,27 @@ implementation
       end;
 
 
+    { While parsing the class invariants, there are probably
+    csubscriptnodes created (if one or more invariants referred to fields)
+    but these have NIL as "left" since there is no "self" pointer in the
+    class declaration. We fill them in in this procedure }
+    procedure fill_in_self_pointers(var node: tnode);
+      begin
+        { Caution: the order is important,
+        since a tsubscriptnode inherits from tunarynode,
+        and a tbinarynode inherits from tunarynode as well. }
+        if node is tsubscriptnode then
+          tsubscriptnode(node).left:=load_self_node 
+        else if node is tbinarynode then
+          begin
+            fill_in_self_pointers(tbinarynode(node).left);
+            fill_in_self_pointers(tbinarynode(node).right);
+          end
+        else if node is tunarynode then
+          fill_in_self_pointers(tunarynode(node).left);
+      end;
+
+
     function generate_bodyentry_block:tnode;
       var
         srsym        : tsym;
@@ -258,9 +279,48 @@ implementation
         newstatement : tstatementnode;
         htype        : ttype;
         failstring   : tnode;
+        i            : Integer;
+        specvar      : tspecvarsym;
+        invariant    : tnode;
       begin
         result:=internalstatements(newstatement);
 
+        { Initialize specification variables }
+        for i := 0 to current_procinfo.procdef.specvars.Count - 1 do
+          begin
+            specvar := tspecvarsym(current_procinfo.procdef.specvars[i]);
+            addstatement(newstatement,
+              cassignmentnode.create(
+                cloadnode.create(specvar, current_procinfo.procdef.localst),
+                specvar.expr.getcopy
+              )
+            );
+          end;
+
+        { Create assertion for class invariant,
+        is this necessary? --TODO
+        } 
+        if assigned(current_procinfo.procdef._class) and
+          assigned(current_procinfo.procdef._class.invariant) then
+          begin
+            if (sp_public in current_procinfo.procdef.symoptions) and
+              not(sp_static in current_procinfo.procdef.symoptions) and
+              not(potype_constructor=current_procinfo.procdef.proctypeoption)
+              then
+              begin
+                invariant:=current_procinfo.procdef._class.invariant.getcopy;
+                fill_in_self_pointers(invariant);
+                failstring:=cstringconstnode.createstr('Class invariant failed', st_default);
+                addstatement(newstatement,
+                  geninlinenode(in_assert_x_y,false,ccallparanode.create(
+                    invariant,
+                    ccallparanode.create(failstring,nil)))
+                ); 
+             end;
+          end; { if in class and class invariant set }
+
+
+        { Create assertion for precondition }
         if assigned(current_procinfo.procdef.precondition) then
           begin
             failstring:=cstringconstnode.createstr('Precondition failed', st_default);
@@ -369,9 +429,31 @@ implementation
         para : tcallparanode;
         newstatement : tstatementnode;
         failstring : tnode;
+        invariant : tnode;
       begin
         result:=internalstatements(newstatement);
 
+        { Create assertion for class invariant } 
+        if assigned(current_procinfo.procdef._class) and
+          assigned(current_procinfo.procdef._class.invariant) then
+          begin
+            if (sp_public in current_procinfo.procdef.symoptions) and
+              not(sp_static in current_procinfo.procdef.symoptions) and
+              not(potype_destructor=current_procinfo.procdef.proctypeoption)
+              then
+              begin
+                invariant:=current_procinfo.procdef._class.invariant.getcopy;
+                fill_in_self_pointers(invariant);
+                failstring:=cstringconstnode.createstr('Class invariant failed', st_default);
+                addstatement(newstatement,
+                  geninlinenode(in_assert_x_y,false,ccallparanode.create(
+                    invariant,
+                    ccallparanode.create(failstring,nil)))
+                ); 
+             end;
+          end; { if in class and class invariant set }
+
+        { Create assertion for postcondition }
         if assigned(current_procinfo.procdef.postcondition) then
           begin
             failstring:=cstringconstnode.createstr('Postcondition failed', st_default);

compiler/symconst.pas

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

compiler/symdef.pas

@@ -282,6 +282,10 @@ interface
           objname,
           objrealname   : pstring;
           objectoptions : tobjectoptions;
+
+          { invariant of this class (conjunction of its invariants),
+          or NIL if there are none }
+          invariant : tnode;
           { to be able to have a variable vmt position }
           { and no vmt field for objects without virtuals }
           vmt_offset : longint;
@@ -590,9 +594,11 @@ interface
           interfacedef : boolean;
           { true if the procedure has a forward declaration }
           hasforward : boolean;
-          { pointer to the pre-/postcondition nodes }
+          { pointers to precondition/postcondition }
           precondition : tnode;
           postcondition : tnode;
+          { specification variables list }
+          specvars : tlist;
           { import info }
           import_dll,
           import_name : pstring;
@@ -3890,6 +3896,7 @@ implementation
          localst := nil;
          precondition:=nil;
          postcondition:=nil;
+         specvars:=tlist.create;
          defref:=nil;
          lastwritten:=nil;
          refcount:=0;
@@ -5098,6 +5105,7 @@ implementation
         objecttype:=ot;
         deftype:=objectdef;
         objectoptions:=[];
+        invariant:=nil;
         childof:=nil;
         symtable:=tobjectsymtable.create(n,aktpackrecords);
         { create space for vmt !! }
@@ -5195,6 +5203,7 @@ implementation
            implementedinterfaces.free;
          if assigned(iidguid) then
            dispose(iidguid);
+         invariant.free;
          inherited destroy;
       end;
 

compiler/symsym.pas

@@ -208,9 +208,16 @@ interface
 {$endif GDB}
       end;
 
-      tspecvarsym = class(tabstractnormalvarsym)
+      tdefinitionsym = class(tabstractnormalvarsym)
           expr : tnode;
           constructor create(const n : string; const tt : ttype; aexpr : tnode);
+          destructor destroy;
+      end;
+
+      tspecvarsym = class(tlocalvarsym)
+          expr : tnode;
+          constructor create(const n : string; const tt : ttype; aexpr : tnode);
+          destructor destroy;
       end;
       
       tparavarsym = class(tabstractnormalvarsym)
@@ -1732,14 +1739,36 @@ implementation
 {$endif GDB}
 
 {****************************************************************************
-                               TPROPOSITIONSYM
+                               TDEFINITIONSYM
+****************************************************************************}
+
+    constructor tdefinitionsym.create(const n : string; const tt: ttype; aexpr : tnode);
+      begin
+        inherited create(n, vs_value, tt, []);
+        expr:=aexpr;
+        typ:=definitionsym;
+      end;
+
+    destructor tdefinitionsym.destroy;
+      begin
+        expr.free;
+        inherited destroy;
+      end;
+
+{****************************************************************************
+                               TSPECVARSYM
 ****************************************************************************}
 
     constructor tspecvarsym.create(const n : string; const tt: ttype; aexpr : tnode);
       begin
         inherited create(n, vs_value, tt, []);
         expr:=aexpr;
-        typ:=specvarsym;
+      end;
+
+    destructor tspecvarsym.destroy;
+      begin
+        expr.free;
+        inherited destroy;
       end;