From 70dae09b2d8fd504cf14471378c474a1f4cfa6a1 Mon Sep 17 00:00:00 2001 From: TUeSET Date: Tue, 17 Oct 2006 23:33:24 +0000 Subject: * 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 ) git-svn-id: http://svn.freepascal.org/svn/fpc/branches/tue@4952 3ad0048d-3df7-0310-abae-a5850022a9f2 --- compiler/nmem.pas | 10 +++- compiler/nobj.pas | 6 +- compiler/pdecformal.pas | 144 ++++++++++++++++++++++++++++++++++++++---------- compiler/pdecobj.pas | 8 ++- compiler/pexpr.pas | 107 +++++++++++++++++++++++------------ compiler/psub.pas | 82 +++++++++++++++++++++++++++ compiler/symconst.pas | 4 +- compiler/symdef.pas | 11 +++- compiler/symsym.pas | 35 +++++++++++- 9 files changed, 332 insertions(+), 75 deletions(-) diff --git a/compiler/nmem.pas b/compiler/nmem.pas index 7ac031ee6d..ecb92e3f7c 100644 --- a/compiler/nmem.pas +++ b/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; diff --git a/compiler/nobj.pas b/compiler/nobj.pas index 7cc3832caf..a5af6188cf 100644 --- a/compiler/nobj.pas +++ b/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; diff --git a/compiler/pdecformal.pas b/compiler/pdecformal.pas index 68de825a7d..f8981de75b 100644 --- a/compiler/pdecformal.pas +++ b/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. diff --git a/compiler/pdecobj.pas b/compiler/pdecobj.pas index 1846261ef6..5f5572c5cb 100644 --- a/compiler/pdecobj.pas +++ b/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 diff --git a/compiler/pexpr.pas b/compiler/pexpr.pas index c74ca632e6..4ad39fb664 100644 --- a/compiler/pexpr.pas +++ b/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. diff --git a/compiler/psub.pas b/compiler/psub.pas index aa7723cc12..ac2ef86bad 100644 --- a/compiler/psub.pas +++ b/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); diff --git a/compiler/symconst.pas b/compiler/symconst.pas index dc924f4be7..efa04f48bb 100644 --- a/compiler/symconst.pas +++ b/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] = ( diff --git a/compiler/symdef.pas b/compiler/symdef.pas index f96fc846a9..aed56765f2 100644 --- a/compiler/symdef.pas +++ b/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; diff --git a/compiler/symsym.pas b/compiler/symsym.pas index 5b3dc4edc5..a9db5967b6 100644 --- a/compiler/symsym.pas +++ b/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; -- cgit v1.2.1