* Bound functions near loops now partially work.

  Syntax:
  {@ bnd : N } while N > 0 do N := N - 1;

  Problems are still: 
  - more than one loop per function or procedure
  - loops not in a function or procedure
(Jochem Berndsen)

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

compiler/nflw.pas

@@ -70,7 +70,8 @@ interface
        end;
 
        twhilerepeatnode = class(tloopnode)
-          invariant : tnode; { the loop invariant (an expression) }
+          invariant : tnode; { the loop invariant (an expression or NIL) }
+          bound : tnode; { the loop bound function (an expression or NIL) }
           constructor create(l,r:Tnode;tab,cn:boolean);virtual;
           destructor destroy;override;
           function det_resulttype:tnode;override;
@@ -78,6 +79,9 @@ interface
           { Set the invariant and insert an assertion inline node
           before the first statement } 
           procedure setinvariant(inv : tnode);
+          { Set the bound function and insert checks at the beginning and
+          at the end of the loop }
+          procedure setbound(bnd : tnode);
 {$ifdef state_tracking}
           function track_state_pass(exec_known:boolean):boolean;override;
 {$endif}
@@ -358,11 +362,13 @@ implementation
           if cn then
               include(loopflags,lnf_checknegate);
           invariant:=nil;
+          bound:=nil;
       end;
 
     destructor twhilerepeatnode.destroy;
       begin
         invariant.free;
+        bound.free;
         inherited destroy;
       end;
 
@@ -378,6 +384,7 @@ implementation
             Message1(type_e_boolean_expr_expected, invariant.resulttype.def.typename);
             invariant.destroy;
             invariant:=nil;
+            exit;
           end;
         s:=cstringconstnode.createstr('Invariant failed', st_default);
         ass:=geninlinenode(in_assert_x_y, false, 
@@ -387,6 +394,82 @@ implementation
         right:=cstatementnode.create(ass, right);
       end;
 
+    procedure twhilerepeatnode.setbound(bnd: tnode);
+       
+      var
+        lvar : tabstractnormalvarsym;
+        assgn : tnode;
+        assert1, expr1, assert2, expr2 : tnode;
+        s : tnode;
+        last : tnode;
+
+      begin
+        bound:=bnd.getcopy;
+        resulttypepass(bound);
+        if not is_integer(bound.resulttype.def) then
+          begin
+            Message1(type_e_integer_expr_expected, bound.resulttype.def.typename);
+            bound.destroy;
+            bound:=nil;
+            exit;
+          end;
+
+        case symtablestack.symtabletype of
+        localsymtable :
+          lvar:=tlocalvarsym.create('$bound',vs_value,bound.resulttype,[]);
+        staticsymtable,
+        globalsymtable :
+          lvar:=tglobalvarsym.create('$bound',vs_value,bound.resulttype,[]);
+        else
+          internalerror(2006102401);
+        end;
+        symtablestack.insert(lvar);
+
+        { Create assertion that this is a positive integer }
+        s:=cstringconstnode.createstr('Bound function is not positive', st_default);
+        expr1:=caddnode.create(gtn,
+          cloadnode.create(lvar, symtablestack),
+          cordconstnode.create(0, s32inttype, false)
+        ); 
+        assert1:=cstatementnode.create(geninlinenode(
+          in_assert_x_y,
+          false,
+          ccallparanode.create(expr1,
+            ccallparanode.create(s, nil)
+          )
+        ), right); 
+
+        { Create assignment to bound variable }
+        assgn:=cstatementnode.create(
+          cassignmentnode.create(
+            cloadnode.create(lvar, symtablestack),
+            bound.getcopy
+          ),
+          assert1
+        );
+        { Add assignment and assertion at beginning of repetition body }
+        right:=assgn;
+
+        { Create assertion that bound function is lower }
+        s:=cstringconstnode.createstr('Bound function did not decrease', st_default);
+        expr2:=caddnode.create(gtn,
+          cloadnode.create(lvar, symtablestack),
+          bound.getcopy
+        );
+        assert2:=cstatementnode.create(geninlinenode(
+          in_assert_x_y,
+          false,
+          ccallparanode.create(expr2,
+            ccallparanode.create(s, nil)
+          )
+        ), nil);
+
+        last:=right;
+        while assigned(tbinarynode(last).right) do
+          last:=tbinarynode(last).right;
+        
+        tbinarynode(last).right:=assert2;
+      end;
 
     function twhilerepeatnode.det_resulttype:tnode;
       var

compiler/pdecformal.pas

@@ -287,8 +287,7 @@ implementation
         rst : tnode;
       begin
         consume(_EQUAL);
-        { Proposition variables are not allowed here }
-        expr:=comp_expr(true);
+        expr:=comp_expr_in_formal_context(true);
         { Convert this to "Result = expr" } 
         if not assigned(current_procinfo.procdef.funcretsym) then
           raise EInvalidAnnotation.Create('{@ ret : expr } in a non-returning something'); { TODO }

compiler/pstatmnt.pas

@@ -1071,7 +1071,7 @@ implementation
          pure_statement:=code;
       end;
 
-    function formal_annotation(var loop_invariant : tnode) : tnode;
+    function formal_annotation(var loop_invariant : tnode; var bound_function : tnode) : tnode;
     var
       expr : tnode;
       s : tnode;
@@ -1099,6 +1099,22 @@ implementation
             formal_annotation:=cnothingnode.create;
             consume(_CLOSE_FORMAL);
           end
+        else if (token=_ID) and (upcase(pattern)='BND') then
+          begin
+            consume(_ID);
+            consume(_COLON);
+            expr:=comp_expr_in_formal_context(true);
+            if assigned(bound_function) then
+              begin
+                { A bound function was already specified,
+                this is an error }
+                { TODO }
+              end
+            else
+              bound_function:=expr;
+            formal_annotation:=cnothingnode.create;
+            consume(_CLOSE_FORMAL);
+          end
         else
           begin
             expr:=comp_expr_in_formal_context(true);
@@ -1116,6 +1132,7 @@ implementation
       first : tnode;
       tochange : ^tnode;
       invariant : tnode;
+      bound : tnode;
 
         procedure parse_formal_annotation_star;
         begin
@@ -1123,7 +1140,7 @@ implementation
            begin
              if not(cs_do_assertion in aktlocalswitches) then
               Message(parser_w_formal_annotation_not_compiled);
-             ass:=formal_annotation(invariant);
+             ass:=formal_annotation(invariant, bound);
              tochange^:=cstatementnode.create(ass, nil);
              tochange:=@(tstatementnode(tochange^).right);
            end;
@@ -1134,11 +1151,12 @@ implementation
 
     begin
       invariant:=nil;
+      bound:=nil;
       first:=nil;
       tochange:=@first;
       parse_formal_annotation_star;
 
-      if assigned(invariant) then
+      if assigned(invariant) or assigned(bound) then
         begin
           { ASSUMPTION :
             repeat_statement and while_statement return a
@@ -1152,10 +1170,18 @@ implementation
           else
             begin
               Message(parser_w_invariant_not_before_loop);
-              invariant.destroy;
+              invariant.free;
               invariant:=nil;
+              bound.free;
+              bound:=nil;
             end; { else }
           end; { case }
+          { Warning: order is important, first bound, then invariant }
+          if assigned(bound) then
+            begin
+              { Set the bound function }
+              twhilerepeatnode(tstatementnode(tochange^).left).setbound(bound);
+            end;
           if assigned(invariant) then
             begin
               { Set the invariant (include a check in each iteration of the loop) }
@@ -1168,10 +1194,11 @@ implementation
                 in_assert_x_y, false, ccallparanode.create(invariant.getcopy,
                   ccallparanode.create(fail_string, nil))), nil);
 
-              tochange:=@(tstatementnode(tochange^).right);
             end;
+          if assigned(invariant) or assigned(bound) then
+            tochange:=@(tstatementnode(tochange^).right);
         end
-      else { not assigned(invariant) }
+      else { not assigned(invariant) and not assigned(bound) }
         begin
           tochange^:=cstatementnode.create(pure_statement, nil);
           tochange:=@(tstatementnode(tochange^).right);