Major refactoring of contract code. Modifications include:
- Better parsing support. Contract sections are no longer hard-coded. New
types of contracts can be added merely be adding an entry to a table.
- Fixed argument naming problems with inheritance. For example, if someone
specified a contract for a base class and a contract for a derived
class method, but they didn't use the same argument names in the
contracts.
- Fixed contracts for static member functions.
- Reduced the amount of generated code--especially for inheritance.
- Changed error messages to indicate inheritance hierarchy.
- Fixed problems with duplicate contract checking code being
emitted.
- Reorganized code that collects contracts and deals with inheritance
to be more generic---no hardcoded contract names or types.
- Reorganized process by which contracts is collected.
- Eliminated unimplemented features for release.
git-svn-id: https://swig.svn.sourceforge.net/svnroot/swig/trunk/SWIG@5320 626c5289-ae23-0410-ae9c-e8d60b6d4f22
This commit is contained in:
parent
c27b0572ec
commit
c0072eb5ed
1 changed files with 189 additions and 476 deletions
|
|
@ -4,7 +4,8 @@
|
||||||
* Support for Wrap by Contract in SWIG
|
* Support for Wrap by Contract in SWIG
|
||||||
*
|
*
|
||||||
* Author(s) : Songyan Feng (Tiger) (songyanf@cs.uchicago.edu)
|
* Author(s) : Songyan Feng (Tiger) (songyanf@cs.uchicago.edu)
|
||||||
*
|
* David Beazley (beazley@cs.uchicago.edu)
|
||||||
|
*
|
||||||
* Department of Computer Science
|
* Department of Computer Science
|
||||||
* University of Chicago
|
* University of Chicago
|
||||||
*
|
*
|
||||||
|
|
@ -16,6 +17,21 @@ char cvsroot_contract_cxx[] = "$Header$";
|
||||||
|
|
||||||
#include "swigmod.h"
|
#include "swigmod.h"
|
||||||
|
|
||||||
|
/* Contract structure. This holds rules about the different kinds of contract sections
|
||||||
|
and their combination rules */
|
||||||
|
|
||||||
|
struct contract {
|
||||||
|
const char *section;
|
||||||
|
const char *combiner;
|
||||||
|
};
|
||||||
|
/* Contract rules. This table defines what contract sections are recognized as well as
|
||||||
|
how contracts are to combined via inheritance */
|
||||||
|
|
||||||
|
static contract Rules[] = {
|
||||||
|
{"require:", "&&"},
|
||||||
|
{"ensure:", "||"},
|
||||||
|
{ NULL, NULL}
|
||||||
|
};
|
||||||
|
|
||||||
/************************************************************************
|
/************************************************************************
|
||||||
* class Contracts:
|
* class Contracts:
|
||||||
|
|
@ -25,25 +41,18 @@ char cvsroot_contract_cxx[] = "$Header$";
|
||||||
*************************************************************************/
|
*************************************************************************/
|
||||||
|
|
||||||
class Contracts : public Dispatcher {
|
class Contracts : public Dispatcher {
|
||||||
|
String *make_expression(String *s, Node *n);
|
||||||
|
void substitute_parms(String *s, ParmList *p, int method);
|
||||||
public:
|
public:
|
||||||
int ContractSplit(Node *n);
|
Hash *ContractSplit(Node *n);
|
||||||
int AssertModify(Node *n, int flag);
|
int emit_contract(Node *n, int method);
|
||||||
int InheritModify(Node *n);
|
|
||||||
int InheritAssertAppend(Node *n, Node *bases);
|
|
||||||
int AssertAddTag(Node *n);
|
|
||||||
int AssertAddErrorMsg(Node *n);
|
|
||||||
int AssertSetParms(Node *n);
|
|
||||||
|
|
||||||
int emit_contract(Node *n);
|
|
||||||
int cDeclaration(Node *n);
|
int cDeclaration(Node *n);
|
||||||
int constructorDeclaration(Node *n);
|
int constructorDeclaration(Node *n);
|
||||||
int destructorDeclaration(Node *n);
|
|
||||||
int externDeclaration(Node *n);
|
int externDeclaration(Node *n);
|
||||||
int extendDirective(Node *n);
|
int extendDirective(Node *n);
|
||||||
int importDirective(Node *n);
|
int importDirective(Node *n);
|
||||||
int includeDirective(Node *n);
|
int includeDirective(Node *n);
|
||||||
int classDeclaration(Node *n);
|
int classDeclaration(Node *n);
|
||||||
int classHandler(Node *n);
|
|
||||||
virtual int top(Node *n);
|
virtual int top(Node *n);
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
@ -51,18 +60,9 @@ extern void Swig_contracts(Node *n);
|
||||||
extern void Swig_contract_mode_set(int flag);
|
extern void Swig_contract_mode_set(int flag);
|
||||||
extern int Swig_contract_mode_get();
|
extern int Swig_contract_mode_get();
|
||||||
|
|
||||||
#define SWIG_PREASSERT "require:"
|
|
||||||
#define SWIG_POSTASSERT "ensure:"
|
|
||||||
#define SWIG_INVARIANT "invariant:"
|
|
||||||
#define SWIG_BEFORE "swig_before("
|
|
||||||
#define SWIG_AFTER "swig_after("
|
|
||||||
#define SWIG_CONTRACT_SET "SET"
|
|
||||||
|
|
||||||
static int Contract_Mode = 0; /* contract option */
|
static int Contract_Mode = 0; /* contract option */
|
||||||
|
|
||||||
static int InClass = 0; /* Parsing C++ or not */
|
static int InClass = 0; /* Parsing C++ or not */
|
||||||
static int InConstructor = 0;
|
static int InConstructor = 0;
|
||||||
static int InDestructor = 0;
|
|
||||||
static Node *CurrentClass = 0;
|
static Node *CurrentClass = 0;
|
||||||
|
|
||||||
/* Set the contract mode, default is 0 (not open) */
|
/* Set the contract mode, default is 0 (not open) */
|
||||||
|
|
@ -70,7 +70,6 @@ static Node *CurrentClass = 0;
|
||||||
void Swig_contract_mode_set(int flag) {
|
void Swig_contract_mode_set(int flag) {
|
||||||
Contract_Mode = flag;
|
Contract_Mode = flag;
|
||||||
}
|
}
|
||||||
|
|
||||||
/* Get the contract mode */
|
/* Get the contract mode */
|
||||||
int Swig_contract_mode_get() {
|
int Swig_contract_mode_get() {
|
||||||
return Contract_Mode;
|
return Contract_Mode;
|
||||||
|
|
@ -78,7 +77,6 @@ int Swig_contract_mode_get() {
|
||||||
|
|
||||||
/* Apply contracts */
|
/* Apply contracts */
|
||||||
void Swig_contracts(Node *n) {
|
void Swig_contracts(Node *n) {
|
||||||
// Printf(stdout,"Applying contracts (experimental version)\n");
|
|
||||||
|
|
||||||
Contracts *a = new Contracts;
|
Contracts *a = new Contracts;
|
||||||
a->top(n);
|
a->top(n);
|
||||||
|
|
@ -86,236 +84,125 @@ void Swig_contracts(Node *n) {
|
||||||
}
|
}
|
||||||
|
|
||||||
/* Split the whole contract into preassertion, postassertion and others */
|
/* Split the whole contract into preassertion, postassertion and others */
|
||||||
int Contracts::ContractSplit(Node *n) {
|
Hash *Contracts::ContractSplit(Node *n) {
|
||||||
|
|
||||||
String *contract = Getattr(n, "feature:contract");
|
String *contract = Getattr(n, "feature:contract");
|
||||||
|
Hash *result;
|
||||||
if (!contract)
|
if (!contract)
|
||||||
return SWIG_ERROR;
|
return NULL;
|
||||||
|
|
||||||
String *preassert = NewString(""); /* preassertion */
|
result = NewHash();
|
||||||
String *postassert = NewString("");
|
String *current_section = NewString("");
|
||||||
String *invariant = NewString("");
|
const char *current_section_name = Rules[0].section;
|
||||||
char *mark_pre = Strstr(contract, SWIG_PREASSERT); /* position of preassertion in whole contract */
|
List *l = SplitLines(contract);
|
||||||
char *mark_post = Strstr(contract, SWIG_POSTASSERT);
|
|
||||||
char *mark_invar = Strstr(contract, SWIG_INVARIANT);
|
Iterator i;
|
||||||
int len_pre = Len(SWIG_PREASSERT); /* length of preassertion */
|
for (i = First(l); i.item; i = Next(i)) {
|
||||||
int len_post = Len(SWIG_POSTASSERT);
|
int found = 0;
|
||||||
int len_invar = Len(SWIG_INVARIANT);
|
if (Strstr(i.item,"{")) continue;
|
||||||
|
if (Strstr(i.item,"}")) continue;
|
||||||
if (!mark_invar) { /* No invar- */
|
for (int j = 0; Rules[j].section; j++) {
|
||||||
if (!mark_post) { /* No post- */
|
if (Strstr(i.item,Rules[j].section)) {
|
||||||
if ( !mark_pre ) { /* No pre-, default is preassert */
|
if (Len(current_section)) {
|
||||||
preassert = contract;
|
Setattr(result,current_section_name,current_section);
|
||||||
} else { /* with pre- only */
|
current_section = Getattr(result,Rules[j].section);
|
||||||
mark_pre[len_pre-1]='{';
|
if (!current_section) current_section = NewString("");
|
||||||
mark_pre[len_pre]='\n';
|
}
|
||||||
preassert = mark_pre+len_pre-1; /* strcpy? */
|
current_section_name = Rules[j].section;
|
||||||
}
|
found = 1;
|
||||||
} else { /* with post- */
|
break;
|
||||||
if (!mark_pre) { /* with post- only, but maybe has preassert */
|
|
||||||
preassert = contract;
|
|
||||||
mark_post[0] = '}';
|
|
||||||
mark_post[1] = '\0';
|
|
||||||
mark_post[len_post-2] = '{';
|
|
||||||
mark_post[len_post-1] = '\n';
|
|
||||||
postassert = mark_post+len_post-2;
|
|
||||||
} else { /* with both pre- & post- marks */
|
|
||||||
mark_pre[len_pre-1]='{';
|
|
||||||
mark_pre[len_pre]='\n';
|
|
||||||
preassert = mark_pre+len_pre-1;
|
|
||||||
mark_post[0] = '}';
|
|
||||||
mark_post[1] = '\0';
|
|
||||||
mark_post[len_post-2] = '{';
|
|
||||||
mark_post[len_post-1] = '\n';
|
|
||||||
postassert = mark_post+len_post-2;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
} else { /* with invar-mark */
|
|
||||||
if (!mark_post) { /* No post- mark */
|
|
||||||
if ( !mark_pre ) { /* with invar- only, but maybe has pre- */
|
|
||||||
preassert = contract;
|
|
||||||
mark_invar[0] = '}';
|
|
||||||
mark_invar[1] = '\0';
|
|
||||||
mark_invar[len_invar-2] = '{';
|
|
||||||
mark_invar[len_invar-1] = '\n';
|
|
||||||
invariant = mark_invar+len_invar-2;
|
|
||||||
} else { /* with pre- & invar-, no postassert */
|
|
||||||
mark_pre[len_pre-1]='{';
|
|
||||||
mark_pre[len_pre]='\n';
|
|
||||||
preassert = mark_pre+len_pre-1;
|
|
||||||
mark_invar[0] = '}';
|
|
||||||
mark_invar[1] = '\0';
|
|
||||||
mark_invar[len_invar-2] = '{';
|
|
||||||
mark_invar[len_invar-1] = '\n';
|
|
||||||
invariant = mark_invar+len_invar-2;
|
|
||||||
}
|
|
||||||
} else { /* with invar- & post- */
|
|
||||||
if (!mark_pre) { /* with post- & invar- only, but maybe has preassert */
|
|
||||||
preassert = contract;
|
|
||||||
mark_post[0] = '}';
|
|
||||||
mark_post[1] = '\0';
|
|
||||||
mark_post[len_post-2] = '{';
|
|
||||||
mark_post[len_post-1] = '\n';
|
|
||||||
postassert = mark_post+len_post-2;
|
|
||||||
mark_invar[0] = '}';
|
|
||||||
mark_invar[1] = '\0';
|
|
||||||
mark_invar[len_invar-2] = '{';
|
|
||||||
mark_invar[len_invar-1] = '\n';
|
|
||||||
invariant = mark_invar+len_invar-2;
|
|
||||||
} else { /* with pre-, post- & invar- */
|
|
||||||
mark_pre[len_pre-1]='{';
|
|
||||||
mark_pre[len_pre]='\n';
|
|
||||||
preassert = mark_pre+len_pre-1;
|
|
||||||
mark_post[0] = '}';
|
|
||||||
mark_post[1] = '\0';
|
|
||||||
mark_post[len_post-2] = '{';
|
|
||||||
mark_post[len_post-1] = '\n';
|
|
||||||
postassert = mark_post+len_post-2;
|
|
||||||
mark_invar[0] = '}';
|
|
||||||
mark_invar[1] = '\0';
|
|
||||||
mark_invar[len_invar-2] = '{';
|
|
||||||
mark_invar[len_invar-1] = '\n';
|
|
||||||
invariant = mark_invar+len_invar-2;
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
if (!found) Append(current_section, i.item);
|
||||||
}
|
}
|
||||||
if (Len(preassert)) Setattr(n, "feature:preassert", preassert);
|
if (Len(current_section)) Setattr(result, current_section_name, current_section);
|
||||||
if (Len(postassert)) Setattr(n, "feature:postassert", postassert);
|
return result;
|
||||||
if (Len(invariant)) Setattr(n, "feature:invariant", invariant);
|
|
||||||
|
|
||||||
Delete(contract);
|
|
||||||
return SWIG_OK;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/* Modify the contract inheritance */
|
/* This function looks in base classes and collects contracts found */
|
||||||
int Contracts::InheritModify(Node *n) {
|
void inherit_contracts(Node *c, Node *n, Hash *contracts, Hash *messages) {
|
||||||
Node *parent, *bases;
|
|
||||||
String *str_assert_pre, *str_assert_post;
|
|
||||||
|
|
||||||
/* Set the preassert to the inherit_preassert as the basic inherit */
|
|
||||||
str_assert_pre = Getattr(n, "feature:preassert");
|
|
||||||
if (Len(str_assert_pre) != 0)
|
|
||||||
Setattr(n, "feature:inherit_preassert", str_assert_pre);
|
|
||||||
/* Set the postassert to the inherit_postassert as the basic inherit */
|
|
||||||
str_assert_post = Getattr(n, "feature:postassert");
|
|
||||||
if (Len(str_assert_post) != 0)
|
|
||||||
Setattr(n, "feature:inherit_postassert", str_assert_post);
|
|
||||||
|
|
||||||
parent = parentNode(n); /* class node of function node n */
|
|
||||||
if (!parent)
|
|
||||||
return SWIG_OK;
|
|
||||||
|
|
||||||
bases = Getattr(parent, "bases"); /* base class list of current class */
|
Node *b, *temp;
|
||||||
if (!bases)
|
String *name, *type, *local_decl, *base_decl;
|
||||||
return SWIG_OK;
|
List *bases;
|
||||||
|
int found = 0;
|
||||||
|
|
||||||
InheritAssertAppend(n, bases);
|
bases = Getattr(c,"bases");
|
||||||
return SWIG_OK;
|
if (!bases) return;
|
||||||
}
|
|
||||||
|
name = Getattr(n, "name");
|
||||||
int Contracts::InheritAssertAppend(Node *n, Node *bases) {
|
type = Getattr(n, "type");
|
||||||
/* check whether the method is inherited from the base */
|
|
||||||
/* if inherited, then AND the ancestor's preassertion to its own preassertion */
|
|
||||||
/* OR its own postassertion to the ancestor's postassertion */
|
|
||||||
String *str_assert_pre;
|
|
||||||
String *str_inherit_pre;
|
|
||||||
String *str_assert_post;
|
|
||||||
String *str_inherit_post;
|
|
||||||
|
|
||||||
Node *b, *temp_base;
|
|
||||||
String *local_name, *local_type, *local_decl, *base_decl;
|
|
||||||
|
|
||||||
int defined = 0;
|
|
||||||
|
|
||||||
if ( (!n) || (!bases) )
|
|
||||||
return 0;
|
|
||||||
if (!Getattr(n, "feature:contract"))
|
|
||||||
return 0;
|
|
||||||
|
|
||||||
local_name = Getattr(n, "name");
|
|
||||||
local_type = Getattr(n, "type");
|
|
||||||
local_decl = Getattr(n, "decl");
|
local_decl = Getattr(n, "decl");
|
||||||
if (local_decl) {
|
if (local_decl) {
|
||||||
local_decl = SwigType_typedef_resolve_all(local_decl);
|
local_decl = SwigType_typedef_resolve_all(local_decl);
|
||||||
} else {
|
} else {
|
||||||
return 0;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
str_inherit_pre = NewString(Getattr(n, "feature:inherit_preassert"));
|
|
||||||
str_assert_post = NewString(Getattr(n, "feature:postassert"));
|
|
||||||
if ( (Len(str_inherit_pre)==0) && ((Len(str_assert_post) ==0)) )
|
|
||||||
return 0; /* no need to modify inheritance of assertions */
|
|
||||||
|
|
||||||
/* Width first search */
|
/* Width first search */
|
||||||
for (int i = 0; i < Len(bases); i++) {
|
for (int i = 0; i < Len(bases); i++) {
|
||||||
b = Getitem(bases,i);
|
b = Getitem(bases,i);
|
||||||
temp_base = firstChild (b); /* member function/variable of the base class */
|
temp = firstChild (b);
|
||||||
|
while (temp) {
|
||||||
while (temp_base) {
|
base_decl = Getattr(temp, "decl");
|
||||||
base_decl = Getattr(temp_base, "decl");
|
|
||||||
if (base_decl) {
|
if (base_decl) {
|
||||||
base_decl = SwigType_typedef_resolve_all(base_decl);
|
base_decl = SwigType_typedef_resolve_all(base_decl);
|
||||||
if ( (checkAttribute(temp_base, "name", local_name)) &&
|
if ( (checkAttribute(temp, "storage", "virtual")) &&
|
||||||
(checkAttribute(temp_base, "type", local_type)) &&
|
(checkAttribute(temp, "name", name)) &&
|
||||||
|
(checkAttribute(temp, "type", type)) &&
|
||||||
(!Strcmp(local_decl, base_decl)) ) {
|
(!Strcmp(local_decl, base_decl)) ) {
|
||||||
/* same declaration in base, append the the base pre to the current inherit_perassertion */
|
/* Yes, match found. */
|
||||||
str_assert_pre = NewString(Getattr(temp_base, "feature:preassert"));
|
Hash *icontracts = Getattr(temp,"contract:rules");
|
||||||
if ( (Len(str_assert_pre)) && (Len(str_inherit_pre)) ) {
|
Hash *imessages = Getattr(temp,"contract:messages");
|
||||||
Printf(str_inherit_pre, " && %s", str_assert_pre);
|
found = 1;
|
||||||
|
if (icontracts && imessages) {
|
||||||
|
/* Add inherited contracts and messages to the contract rules above */
|
||||||
|
int j = 0;
|
||||||
|
for (j = 0; Rules[j].section; j++) {
|
||||||
|
String *t = Getattr(contracts, Rules[j].section);
|
||||||
|
String *s = Getattr(icontracts, Rules[j].section);
|
||||||
|
if (s) {
|
||||||
|
if (t) {
|
||||||
|
Insert(t,0,"(");
|
||||||
|
Printf(t,") %s (%s)", Rules[j].combiner, s);
|
||||||
|
String *m = Getattr(messages, Rules[j].section);
|
||||||
|
Printf(m," %s [%s from %s]", Rules[j].combiner, Getattr(imessages,Rules[j].section), Getattr(b,"name"));
|
||||||
|
} else {
|
||||||
|
Setattr(contracts, Rules[j].section, NewString(s));
|
||||||
|
Setattr(messages,Rules[j].section,NewStringf("[%s from %s]", Getattr(imessages,Rules[j].section), Getattr(b,"name")));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
str_inherit_post = NewString(Getattr(temp_base, "feature:inherit_postassert"));
|
|
||||||
if ( (Len(str_assert_post)) && (Len(str_inherit_post)) ) {
|
|
||||||
Printf(str_inherit_post, " || %s", str_assert_post);
|
|
||||||
Setattr(temp_base, "feature:inherit_postassert", str_inherit_post);
|
|
||||||
}
|
|
||||||
|
|
||||||
Delete(str_assert_pre);
|
|
||||||
Delete(str_inherit_post);
|
|
||||||
defined = 1;
|
|
||||||
}
|
}
|
||||||
Delete(base_decl);
|
Delete(base_decl);
|
||||||
} /* end of if */
|
}
|
||||||
temp_base = nextSibling(temp_base);
|
temp = nextSibling(temp);
|
||||||
} /* end of while(temp) */
|
}
|
||||||
} /* end of i */
|
}
|
||||||
|
Delete(local_decl);
|
||||||
if (Len(str_inherit_pre))
|
if (!found) {
|
||||||
Setattr(n, "feature:inherit_preassert", str_inherit_pre);
|
for (int j = 0; j < Len(bases); j++) {
|
||||||
Delete(local_decl);
|
b = Getitem(bases,j);
|
||||||
Delete(str_inherit_pre);
|
inherit_contracts(b,n,contracts,messages);
|
||||||
Delete(str_assert_post);
|
}
|
||||||
|
|
||||||
/* recursive search */
|
|
||||||
for (int j = 0; j < Len(bases); j++) {
|
|
||||||
b = Getitem(bases,j);
|
|
||||||
if (InheritAssertAppend(n, Getattr(b, "bases")))
|
|
||||||
defined = 1;
|
|
||||||
}
|
}
|
||||||
if (defined)
|
|
||||||
return 1;
|
|
||||||
return 0;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
int Contracts::AssertModify(Node *n, int flag) {
|
/* This function cleans up the assertion string by removing some extraneous characters.
|
||||||
String *str_assert, *expr = 0, *tag_sync;
|
Splitting the assertion into pieces */
|
||||||
|
|
||||||
|
String *Contracts::make_expression(String *s, Node *n) {
|
||||||
|
String *str_assert, *expr = 0;
|
||||||
List *list_assert;
|
List *list_assert;
|
||||||
|
|
||||||
if (flag == 1) { /* preassert */
|
str_assert = NewString(s);
|
||||||
str_assert = NewString(Getattr(n, "feature:preassert"));
|
/* Omit all useless characters and split by ; */
|
||||||
} else if (flag == 2){ /* postassert */
|
|
||||||
str_assert = NewString(Getattr(n, "feature:postassert"));
|
|
||||||
} else if (flag == 3){ /* invariant */
|
|
||||||
str_assert = NewString(Getattr(n, "feature:invariant"));
|
|
||||||
} else
|
|
||||||
return SWIG_ERROR;
|
|
||||||
|
|
||||||
if (!Len(str_assert))
|
|
||||||
return SWIG_OK;
|
|
||||||
|
|
||||||
/* Omit all unuseful characters and split by ; */
|
|
||||||
Replaceall(str_assert, "\n", "");
|
Replaceall(str_assert, "\n", "");
|
||||||
Replaceall(str_assert, "{", "");
|
Replaceall(str_assert, "{", "");
|
||||||
Replaceall(str_assert, "}", "");
|
Replaceall(str_assert, "}", "");
|
||||||
Replaceall(str_assert, " ", "");
|
Replace(str_assert, " ", "", DOH_REPLACE_ANY | DOH_REPLACE_NOQUOTE);
|
||||||
|
Replace(str_assert, "\t", "", DOH_REPLACE_ANY | DOH_REPLACE_NOQUOTE);
|
||||||
|
|
||||||
list_assert = Split(str_assert, ';', -1);
|
list_assert = Split(str_assert, ';', -1);
|
||||||
Delete(str_assert);
|
Delete(str_assert);
|
||||||
|
|
||||||
|
|
@ -326,265 +213,105 @@ int Contracts::AssertModify(Node *n, int flag) {
|
||||||
for (ei = First(list_assert); ei.item; ei = Next(ei)) {
|
for (ei = First(list_assert); ei.item; ei = Next(ei)) {
|
||||||
expr = ei.item;
|
expr = ei.item;
|
||||||
if (Len(expr)) {
|
if (Len(expr)) {
|
||||||
/* All sync staff are not complete and only experimental */
|
Replaceid(expr, Getattr(n,"name"), "result");
|
||||||
if (Strstr(expr, SWIG_BEFORE)) { /* before sync assertion */
|
if (Len(str_assert))
|
||||||
tag_sync = NewString(" SWIG_sync(");
|
Append(str_assert, "&&");
|
||||||
Append(tag_sync, Getattr(n, "name"));
|
Printf(str_assert, "(%s)", expr);
|
||||||
Append(tag_sync, ", ");
|
|
||||||
Replaceall(expr, SWIG_BEFORE, tag_sync);
|
|
||||||
Append(str_assert, expr);
|
|
||||||
Append(str_assert, ";\n");
|
|
||||||
Delete(tag_sync);
|
|
||||||
} else if (Strstr(expr, SWIG_AFTER)) { /* after sync assertion */
|
|
||||||
tag_sync = NewString(" SWIG_sync(");
|
|
||||||
Replaceall(expr, SWIG_AFTER, tag_sync);
|
|
||||||
Replaceall(expr, ")", ", ");
|
|
||||||
Append(str_assert, expr);
|
|
||||||
Append(str_assert, Getattr(n,"name"));
|
|
||||||
Append(str_assert, ");\n");
|
|
||||||
Delete(tag_sync);
|
|
||||||
} else { /* no sync assertion, only basic pre- post-, invar- */
|
|
||||||
Replaceid(expr, Getattr(n,"name"), "result");
|
|
||||||
if (Len(str_assert))
|
|
||||||
Append(str_assert, "&&");
|
|
||||||
Printf(str_assert, "(%s)", expr);
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (flag == 1) {
|
|
||||||
Setattr(n, "feature:preassert", str_assert);
|
|
||||||
} else if (flag == 2) {
|
|
||||||
Setattr(n, "feature:postassert", str_assert);
|
|
||||||
} else {
|
|
||||||
Setattr(n, "feature:invariant", str_assert);
|
|
||||||
}
|
|
||||||
|
|
||||||
Delete(str_assert);
|
|
||||||
Delete(list_assert);
|
Delete(list_assert);
|
||||||
return SWIG_OK;
|
return str_assert;
|
||||||
}
|
}
|
||||||
|
|
||||||
/* Modify format into { SWIG_xxxassert(...);\n ...} */
|
/* This function substitutes parameter names for argument names in the
|
||||||
int Contracts::AssertAddTag(Node *n) {
|
contract specification. Note: it is assumed that the wrapper code
|
||||||
String *str_assert, *tag;
|
uses arg1--argn for arguments. */
|
||||||
/* preassert */
|
|
||||||
str_assert = NewString(Getattr(n, "feature:preassert"));
|
|
||||||
if (Len(str_assert)) {
|
|
||||||
Setattr(n, "feature:preassert", NewStringf("SWIG_contract_assert(%s);\n", str_assert));
|
|
||||||
|
|
||||||
/*
|
|
||||||
tag = NewString(" SWIG_preassert(");
|
|
||||||
Append(tag, str_assert);
|
|
||||||
Append(tag, ");\n");
|
|
||||||
Setattr(n, "feature:inherit_preassert", tag);
|
|
||||||
Delete(tag);
|
|
||||||
*/
|
|
||||||
}
|
|
||||||
Delete(str_assert);
|
|
||||||
|
|
||||||
/* inherit_preassert */
|
void Contracts::substitute_parms(String *s, ParmList *p, int method) {
|
||||||
str_assert = NewString(Getattr(n, "feature:inherit_preassert"));
|
int argnum = 1;
|
||||||
if (Len(str_assert)) {
|
char argname[32];
|
||||||
Setattr(n, "feature:inherit_preassert", NewStringf("SWIG_contract_assert(%s);\n", str_assert));
|
|
||||||
/*
|
if (method) {
|
||||||
tag = NewString(" SWIG_inherit_preassert((");
|
Replaceid(s,"self","arg0");
|
||||||
Append(tag, str_assert);
|
argnum++;
|
||||||
Append(tag, "));\n");
|
|
||||||
Setattr(n, "feature:inherit_preassert", tag);
|
|
||||||
Delete(tag);
|
|
||||||
*/
|
|
||||||
}
|
}
|
||||||
Delete(str_assert);
|
while (p) {
|
||||||
|
sprintf(argname,"arg%d",argnum);
|
||||||
/* postassert */
|
String *name = Getattr(p,"name");
|
||||||
str_assert = NewString(Getattr(n, "feature:postassert"));
|
if (name) {
|
||||||
if (Len(str_assert)) {
|
Replaceid(s,name,argname);
|
||||||
Setattr(n, "feature:postassert", NewStringf("SWIG_contract_assert(%s);\n", str_assert));
|
}
|
||||||
/*
|
argnum++;
|
||||||
tag = NewString(" SWIG_postassert(");
|
p = nextSibling(p);
|
||||||
Append(tag, str_assert);
|
|
||||||
Append(tag, ");\n");
|
|
||||||
Setattr(n, "feature:postassert", tag);
|
|
||||||
Delete(tag);
|
|
||||||
*/
|
|
||||||
}
|
}
|
||||||
Delete(str_assert);
|
|
||||||
|
|
||||||
/* inherit_postassert */
|
|
||||||
str_assert = NewString(Getattr(n, "feature:inherit_postassert"));
|
|
||||||
if (Len(str_assert)) {
|
|
||||||
Setattr(n, "feature:inherit_postassert", NewStringf("SWIG_contract_assert(%s);\n", str_assert));
|
|
||||||
/*
|
|
||||||
tag = NewString(" SWIG_inherit_postassert((");
|
|
||||||
Append(tag, str_assert);
|
|
||||||
Append(tag, "));\n");
|
|
||||||
Setattr(n, "feature:inherit_postassert", tag);
|
|
||||||
Delete(tag);
|
|
||||||
*/
|
|
||||||
}
|
|
||||||
Delete(str_assert);
|
|
||||||
|
|
||||||
/* invariant */
|
|
||||||
str_assert = NewString(Getattr(n, "feature:invariant"));
|
|
||||||
if (Len(str_assert)) {
|
|
||||||
Setattr(n, "feature:invariant", NewStringf("SWIG_contract_assert(%s);\n", str_assert));
|
|
||||||
/*
|
|
||||||
tag = NewString(" SWIG_invariant(");
|
|
||||||
Append(tag, str_assert);
|
|
||||||
Append(tag, ");\n");
|
|
||||||
Setattr(n, "feature:invariant", tag);
|
|
||||||
Delete(tag);
|
|
||||||
*/
|
|
||||||
}
|
|
||||||
Delete(str_assert);
|
|
||||||
return SWIG_OK;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/* Append error message */
|
int Contracts::emit_contract(Node *n, int method) {
|
||||||
int Contracts::AssertAddErrorMsg(Node *n) {
|
Hash *contracts;
|
||||||
String *str_assert, *error_msg;
|
Hash *messages;
|
||||||
/* preassert */
|
String *c;
|
||||||
str_assert = NewString(Getattr(n, "feature:preassert"));
|
|
||||||
Replaceall(str_assert, ");\n", "");
|
|
||||||
if (Len(str_assert)) {
|
|
||||||
error_msg = NewString("Require assertion violation, ");
|
|
||||||
Printf(error_msg, "in function %s", Getattr(n, "name"));
|
|
||||||
Printf(str_assert, ", \"%s\");\n", error_msg);
|
|
||||||
Setattr(n, "feature:preassert", str_assert);
|
|
||||||
Delete(error_msg);
|
|
||||||
}
|
|
||||||
Delete(str_assert);
|
|
||||||
|
|
||||||
/* inherit_preassert */
|
ParmList *cparms;
|
||||||
str_assert = NewString(Getattr(n, "feature:inherit_preassert"));
|
|
||||||
Replaceall(str_assert, ");\n", "");
|
|
||||||
if (Len(str_assert)) {
|
|
||||||
error_msg = NewString("Require assertion violation (via inheritance), ");
|
|
||||||
Printf(error_msg, "in function %s", Getattr(n, "name"));
|
|
||||||
Printf(str_assert, ", \"%s\");\n", error_msg);
|
|
||||||
Setattr(n, "feature:inherit_preassert", str_assert);
|
|
||||||
Delete(error_msg);
|
|
||||||
}
|
|
||||||
Delete(str_assert);
|
|
||||||
|
|
||||||
/* postassert */
|
|
||||||
str_assert = NewString(Getattr(n, "feature:postassert"));
|
|
||||||
Replaceall(str_assert, ");\n", "");
|
|
||||||
if (Len(str_assert)) {
|
|
||||||
error_msg = NewString("Ensure assertion violation, ");
|
|
||||||
Printf(error_msg, "in function of %s", Getattr(n, "name"));
|
|
||||||
Printf(str_assert, ", \"%s\");\n", error_msg);
|
|
||||||
Setattr(n, "feature:postassert", str_assert);
|
|
||||||
Delete(error_msg);
|
|
||||||
}
|
|
||||||
Delete(str_assert);
|
|
||||||
|
|
||||||
/* inherit_postassert */
|
|
||||||
str_assert = NewString(Getattr(n, "feature:inherit_postassert"));
|
|
||||||
Replaceall(str_assert, ");\n", "");
|
|
||||||
if (Len(str_assert)) {
|
|
||||||
error_msg = NewString("Ensure assertion violation (via inheritance), ");
|
|
||||||
Printf(error_msg, "in function of %s", Getattr(n, "name"));
|
|
||||||
Printf(str_assert, ", \"%s\");\n", error_msg);
|
|
||||||
Setattr(n, "feature:inherit_postassert", str_assert);
|
|
||||||
Delete(error_msg);
|
|
||||||
}
|
|
||||||
Delete(str_assert);
|
|
||||||
|
|
||||||
/* invariant */
|
|
||||||
str_assert = NewString(Getattr(n, "feature:invariant"));
|
|
||||||
Replaceall(str_assert, ");\n", "");
|
|
||||||
if (Len(str_assert)) {
|
|
||||||
error_msg = NewString("Invariant assertion violation, ");
|
|
||||||
Printf(error_msg, "in function of %s", Getattr(n, "name"));
|
|
||||||
Printf(str_assert, ", \"%s\");\n", error_msg);
|
|
||||||
Setattr(n, "feature:invariant", str_assert);
|
|
||||||
Delete(error_msg);
|
|
||||||
}
|
|
||||||
Delete(str_assert);
|
|
||||||
return SWIG_OK;
|
|
||||||
}
|
|
||||||
|
|
||||||
int Contracts::AssertSetParms(Node *n) {
|
|
||||||
ParmList *list_params;
|
|
||||||
String *str_assert_pre,*str_assert_post,*str_assert_invar;
|
|
||||||
String *str_inherit_pre, *str_inherit_post;
|
|
||||||
|
|
||||||
str_assert_pre = NewString(Getattr(n, "feature:preassert"));
|
|
||||||
str_assert_post = NewString(Getattr(n, "feature:postassert"));
|
|
||||||
str_assert_invar = NewString(Getattr(n, "feature:invariant"));
|
|
||||||
str_inherit_pre = NewString(Getattr(n, "feature:inherit_preassert"));
|
|
||||||
str_inherit_post = NewString(Getattr(n, "feature:inherit_postassert"));
|
|
||||||
|
|
||||||
/* Set the params in preassert & postassert */
|
|
||||||
list_params = Getmeta(Getattr(n, "feature:contract"), "parms");
|
|
||||||
if (Getattr(n, "feature:contract_classparm")){
|
|
||||||
/* Insert function name as parm for class member functions */
|
|
||||||
String *type = NewString(Getattr(n,"type"));
|
|
||||||
String *name = NewString("self");
|
|
||||||
Parm *p = NewParm(type, name);
|
|
||||||
set_nextSibling(p, list_params);
|
|
||||||
list_params = p;
|
|
||||||
}
|
|
||||||
Setmeta(str_assert_pre, "parms", list_params);
|
|
||||||
Setmeta(str_assert_post, "parms", list_params);
|
|
||||||
Setmeta(str_assert_invar, "parms", list_params);
|
|
||||||
Setmeta(str_inherit_pre, "parms", list_params);
|
|
||||||
Setmeta(str_inherit_post, "parms", list_params);
|
|
||||||
|
|
||||||
if (Len(str_assert_pre))
|
|
||||||
Setattr(n, "feature:preassert", str_assert_pre);
|
|
||||||
if (Len(str_assert_post))
|
|
||||||
Setattr(n, "feature:postassert", str_assert_post);
|
|
||||||
if (Len(str_assert_invar))
|
|
||||||
Setattr(n, "feature:invariant", str_assert_invar);
|
|
||||||
if (Len(str_inherit_pre))
|
|
||||||
Setattr(n, "feature:inherit_preassert", str_inherit_pre);
|
|
||||||
if (Len(str_inherit_post))
|
|
||||||
Setattr(n, "feature:inherit_postassert", str_inherit_post);
|
|
||||||
|
|
||||||
Delete(list_params);
|
|
||||||
Delete(str_assert_pre);
|
|
||||||
Delete(str_assert_post);
|
|
||||||
Delete(str_assert_invar);
|
|
||||||
Delete(str_inherit_pre);
|
|
||||||
Delete(str_inherit_post);
|
|
||||||
return SWIG_OK;
|
|
||||||
}
|
|
||||||
|
|
||||||
int Contracts::emit_contract(Node *n) {
|
|
||||||
int ret = SWIG_OK;
|
|
||||||
|
|
||||||
if (!Getattr(n, "feature:contract"))
|
if (!Getattr(n, "feature:contract"))
|
||||||
return SWIG_ERROR;
|
return SWIG_ERROR;
|
||||||
|
|
||||||
/* Split contracqt into preassert & postassert */
|
/* Get contract parameters */
|
||||||
if (!ContractSplit(n))
|
cparms = Getmeta(Getattr(n, "feature:contract"), "parms");
|
||||||
return SWIG_ERROR;
|
|
||||||
|
|
||||||
/* Modify pre- , post- * invar- */
|
|
||||||
ret = ret && AssertModify(n, 1);
|
|
||||||
ret = ret && AssertModify(n, 2);
|
|
||||||
ret = ret && AssertModify(n, 3);
|
|
||||||
if (InClass) { ret = ret && InheritModify(n); }
|
|
||||||
if ((InClass) && (!InConstructor) && (!InDestructor)){
|
|
||||||
Setattr(n, "feature:contract_classparm", SWIG_CONTRACT_SET);
|
|
||||||
}
|
|
||||||
/* Add tags and error msgs later when emit,
|
|
||||||
and keep assertions as experisions in the parse tree */
|
|
||||||
|
|
||||||
AssertAddTag(n);
|
|
||||||
AssertAddErrorMsg(n);
|
|
||||||
AssertSetParms(n);
|
|
||||||
|
|
||||||
return ret;
|
/* Split contract into preassert & postassert */
|
||||||
|
contracts = ContractSplit(n);
|
||||||
|
if (!contracts) return SWIG_ERROR;
|
||||||
|
|
||||||
|
/* This messages hash is used to hold the error messages that will be displayed on
|
||||||
|
failed contract. */
|
||||||
|
|
||||||
|
messages = NewHash();
|
||||||
|
|
||||||
|
/* Take the different contract expressions and clean them up a bit */
|
||||||
|
Iterator i;
|
||||||
|
for (i = First(contracts); i.item; i = Next(i)) {
|
||||||
|
String *e = make_expression(i.item, n);
|
||||||
|
substitute_parms(e, cparms, method);
|
||||||
|
Setattr(contracts,i.key,e);
|
||||||
|
|
||||||
|
/* Make a string containing error messages */
|
||||||
|
Setattr(messages,i.key, NewString(e));
|
||||||
|
}
|
||||||
|
|
||||||
|
/* If we're in a class. We need to inherit other assertions. */
|
||||||
|
if (InClass) {
|
||||||
|
inherit_contracts(CurrentClass, n, contracts, messages);
|
||||||
|
}
|
||||||
|
|
||||||
|
/* Save information */
|
||||||
|
Setattr(n,"contract:rules", contracts);
|
||||||
|
Setattr(n,"contract:messages", messages);
|
||||||
|
|
||||||
|
/* Okay. Generate the contract runtime code. */
|
||||||
|
|
||||||
|
if ((c = Getattr(contracts,"require:"))) {
|
||||||
|
Setattr(n,"contract:preassert",
|
||||||
|
NewStringf("SWIG_contract_assert(%s, \"Contract violation: require: %s\");\n",
|
||||||
|
c, Getattr(messages,"require:")));
|
||||||
|
}
|
||||||
|
if ((c = Getattr(contracts,"ensure:"))) {
|
||||||
|
Setattr(n,"contract:postassert",
|
||||||
|
NewStringf("SWIG_contract_assert(%s, \"Contract violation: ensure: %s\");\n",
|
||||||
|
c, Getattr(messages,"ensure:")));
|
||||||
|
}
|
||||||
|
return SWIG_OK;
|
||||||
}
|
}
|
||||||
|
|
||||||
int Contracts::cDeclaration(Node *n) {
|
int Contracts::cDeclaration(Node *n) {
|
||||||
int ret = SWIG_OK;
|
int ret = SWIG_OK;
|
||||||
|
String *decl = Getattr(n,"decl");
|
||||||
|
|
||||||
|
/* Not a function. Don't even bother with it (for now) */
|
||||||
|
if (!SwigType_isfunction(decl)) return SWIG_OK;
|
||||||
|
|
||||||
if (Getattr(n, "feature:contract"))
|
if (Getattr(n, "feature:contract"))
|
||||||
ret = emit_contract(n);
|
ret = emit_contract(n, (InClass && !checkAttribute(n,"storage","static")));
|
||||||
return ret;
|
return ret;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -592,20 +319,11 @@ int Contracts::constructorDeclaration(Node *n){
|
||||||
int ret = SWIG_OK;
|
int ret = SWIG_OK;
|
||||||
InConstructor = 1;
|
InConstructor = 1;
|
||||||
if (Getattr(n, "feature:contract"))
|
if (Getattr(n, "feature:contract"))
|
||||||
ret = emit_contract(n);
|
ret = emit_contract(n,0);
|
||||||
InConstructor = 0;
|
InConstructor = 0;
|
||||||
return ret;
|
return ret;
|
||||||
}
|
}
|
||||||
|
|
||||||
int Contracts::destructorDeclaration(Node *n){
|
|
||||||
int ret = SWIG_OK;
|
|
||||||
InDestructor = 1;
|
|
||||||
if (Getattr(n, "feature:contract"))
|
|
||||||
ret = emit_contract(n);
|
|
||||||
InDestructor = 0;
|
|
||||||
return ret;
|
|
||||||
}
|
|
||||||
|
|
||||||
int Contracts::externDeclaration(Node *n) { return emit_children(n); }
|
int Contracts::externDeclaration(Node *n) { return emit_children(n); }
|
||||||
int Contracts::extendDirective(Node *n) { return emit_children(n); }
|
int Contracts::extendDirective(Node *n) { return emit_children(n); }
|
||||||
int Contracts::importDirective(Node *n) { return emit_children(n); }
|
int Contracts::importDirective(Node *n) { return emit_children(n); }
|
||||||
|
|
@ -615,17 +333,12 @@ int Contracts::classDeclaration(Node *n) {
|
||||||
int ret = SWIG_OK;
|
int ret = SWIG_OK;
|
||||||
InClass = 1;
|
InClass = 1;
|
||||||
CurrentClass = n;
|
CurrentClass = n;
|
||||||
ret = classHandler(n);
|
emit_children(n);
|
||||||
InClass = 0;
|
InClass = 0;
|
||||||
CurrentClass = 0;
|
CurrentClass = 0;
|
||||||
return ret;
|
return ret;
|
||||||
}
|
}
|
||||||
|
|
||||||
int Contracts::classHandler(Node *n) {
|
|
||||||
emit_children(n);
|
|
||||||
return SWIG_OK;
|
|
||||||
}
|
|
||||||
|
|
||||||
int Contracts::top(Node *n) {
|
int Contracts::top(Node *n) {
|
||||||
emit_children(n);
|
emit_children(n);
|
||||||
return SWIG_OK;
|
return SWIG_OK;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue