diff options
author | TUeSET <TUeSET@3ad0048d-3df7-0310-abae-a5850022a9f2> | 2006-10-24 19:22:34 +0000 |
---|---|---|
committer | TUeSET <TUeSET@3ad0048d-3df7-0310-abae-a5850022a9f2> | 2006-10-24 19:22:34 +0000 |
commit | e941e7801ccc80578b0975e20f7a057652bf78ab (patch) | |
tree | 2fddda988d9fd2895824c5bbf3752ec16efb82bd | |
parent | 3dff3d5197f4505af758c26bb2213d670da98a07 (diff) | |
download | fpc-tue.tar.gz |
* Bound functions near loops now partially work.tue
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: http://svn.freepascal.org/svn/fpc/branches/tue@5020 3ad0048d-3df7-0310-abae-a5850022a9f2
-rw-r--r-- | compiler/nflw.pas | 85 | ||||
-rw-r--r-- | compiler/pdecformal.pas | 3 | ||||
-rw-r--r-- | compiler/pstatmnt.pas | 39 |
3 files changed, 118 insertions, 9 deletions
diff --git a/compiler/nflw.pas b/compiler/nflw.pas index a0950c29a4..bd889b6ff7 100644 --- a/compiler/nflw.pas +++ b/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 diff --git a/compiler/pdecformal.pas b/compiler/pdecformal.pas index db1f253fa8..b1dfc61dd7 100644 --- a/compiler/pdecformal.pas +++ b/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 } diff --git a/compiler/pstatmnt.pas b/compiler/pstatmnt.pas index 2ab55c1255..9de0ec0f9a 100644 --- a/compiler/pstatmnt.pas +++ b/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); |