Experimental contract work.
git-svn-id: https://swig.svn.sourceforge.net/svnroot/swig/trunk@4806 626c5289-ae23-0410-ae9c-e8d60b6d4f22
This commit is contained in:
Tiger Feng
parent
baa333b1ed
commit
5a9a3b5d56
3 changed files with 310 additions and 93 deletions
|
|
@ -1,9 +1,12 @@
|
|||
/* -----------------------------------------------------------------------------
|
||||
* contract.cxx
|
||||
*
|
||||
* Experimental support for contracts
|
||||
* Support for Design by Contract in SWIG
|
||||
*
|
||||
* Author(s) : Aquinas Hobor (aahobor@cs.uchicago.edu)
|
||||
* Author(s) : Songyan Feng (Tiger) (songyanf@cs.uchicago.edu)
|
||||
*
|
||||
* Department of Computer Science
|
||||
* University of Chicago
|
||||
*
|
||||
* Copyright (C) 1999-2000. The University of Chicago
|
||||
* See the file LICENSE for information on usage and redistribution.
|
||||
|
|
@ -13,106 +16,300 @@ char cvsroot_contract_cxx[] = "$Header$";
|
|||
|
||||
#include "swigmod.h"
|
||||
|
||||
#define SWIG_PREASSERT "require:"
|
||||
#define SWIG_POSTASSERT "ensure:"
|
||||
#define SWIG_INVARIANT "invariant:"
|
||||
#define SWIG_BEFORE "swig_before("
|
||||
#define SWIG_AFTER "swig_after("
|
||||
|
||||
static int InClass = 0; /* Parsing C++ or not */
|
||||
static Node *CurrentClass = 0;
|
||||
static int InConstructor = 0;
|
||||
static int InDestructor = 0;
|
||||
|
||||
class Contracts : public Dispatcher {
|
||||
|
||||
public:
|
||||
virtual int top(Node *n) {
|
||||
public:
|
||||
|
||||
int SliptContract(Node *n) {
|
||||
String *contract = Getattr(n, "feature:contract");
|
||||
if (!contract)
|
||||
return SWIG_ERROR;
|
||||
String *preassert = NewString("");
|
||||
String *postassert = NewString("");
|
||||
String *invariant = NewString("");
|
||||
char *mark_pre = Strstr(contract, SWIG_PREASSERT);
|
||||
char *mark_post = Strstr(contract, SWIG_POSTASSERT);
|
||||
char *mark_invar = Strstr(contract, SWIG_INVARIANT);
|
||||
int len_pre = Len(SWIG_PREASSERT);
|
||||
int len_post = Len(SWIG_POSTASSERT);
|
||||
int len_invar = Len(SWIG_INVARIANT);
|
||||
|
||||
if (!mark_invar) { // No invar-
|
||||
if (!mark_post) { // No post-
|
||||
if ( !mark_pre ) { // No pre-, default is preassert
|
||||
preassert = contract;
|
||||
} else { // with pre- only
|
||||
mark_pre[len_pre-1]='{';
|
||||
mark_pre[len_pre]='\n';
|
||||
preassert = mark_pre+len_pre-1;
|
||||
}
|
||||
} else { // with post-
|
||||
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;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Setattr(n, "feature:preassert", preassert);
|
||||
Setattr(n, "feature:postassert", postassert);
|
||||
Setattr(n, "feature:invariant", invariant);
|
||||
Delete(contract);
|
||||
return SWIG_OK;
|
||||
}
|
||||
|
||||
int AssertModify(Node *n, int flag) {
|
||||
String *str_assert, *s, *tag, *tag_sync;
|
||||
List *list_assert;
|
||||
ParmList *list_params;
|
||||
|
||||
if (flag == 1) { // preassert
|
||||
str_assert = NewString(Getattr(n, "feature:preassert"));
|
||||
tag = NewString(" SWIG_preassert(");
|
||||
} else if (flag == 2){ //postassert
|
||||
str_assert = NewString(Getattr(n, "feature:postassert"));
|
||||
tag = NewString(" SWIG_postassert(");
|
||||
} else if (flag == 3){
|
||||
str_assert = NewString(Getattr(n, "feature:invariant"));
|
||||
tag = NewString(" SWIG_invariant(");
|
||||
} else
|
||||
return SWIG_ERROR;
|
||||
|
||||
// Modify format into { SWIG_xxxassert(...);\n ...}
|
||||
// Omit all unuseful characters and split by ;
|
||||
Replaceall(str_assert, "\n", "");
|
||||
Replaceall(str_assert, "{", "");
|
||||
Replaceall(str_assert, "}", "");
|
||||
Replaceall(str_assert, " ", "");
|
||||
list_assert = Split(str_assert, ';', -1);
|
||||
Delete(str_assert);
|
||||
|
||||
// build up new assertion
|
||||
str_assert = NewString("{");
|
||||
for (s = Firstitem(list_assert); s; s = Nextitem(list_assert)) {
|
||||
if (Len(s)) {
|
||||
//Printf(stdout, "%s\n", s);
|
||||
if (Strstr(s, SWIG_BEFORE)) { //before sync assertion
|
||||
tag_sync = NewString(" SWIG_sync(");
|
||||
Append(tag_sync, Getattr(n, "name"));
|
||||
Append(tag_sync, ", ");
|
||||
Replaceall(s, SWIG_BEFORE, tag_sync);
|
||||
Append(str_assert, s);
|
||||
Append(str_assert, ";\n");
|
||||
Delete(tag_sync);
|
||||
} else if (Strstr(s, SWIG_AFTER)) { //after sync assertion
|
||||
tag_sync = NewString(" SWIG_sync(");
|
||||
Replaceall(s, SWIG_AFTER, tag_sync);
|
||||
Replaceall(s, ")", ", ");
|
||||
Append(str_assert, s);
|
||||
Append(str_assert, Getattr(n,"name"));
|
||||
Append(str_assert, ");\n");
|
||||
Delete(tag_sync);
|
||||
} else { // no sync assertion
|
||||
Append(str_assert, tag);
|
||||
Append(str_assert, s);
|
||||
Append(str_assert, ");\n");
|
||||
}
|
||||
}
|
||||
}
|
||||
Append(str_assert, "}");
|
||||
|
||||
// Set the params in preassert & postassert
|
||||
list_params = Getmeta(Getattr(n, "feature:contract"), "parms");
|
||||
if ((InClass) && (!InConstructor) && (!InDestructor)){
|
||||
// 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, "parms", list_params);
|
||||
|
||||
if (flag == 1) {
|
||||
Replaceid(str_assert, Getattr(n,"name"), "result");
|
||||
Setattr(n, "feature:preassert", str_assert);
|
||||
} else if (flag == 2) {
|
||||
Replaceid(str_assert, Getattr(n,"name"), "result");
|
||||
Setattr(n, "feature:postassert", str_assert);
|
||||
} else {
|
||||
Setattr(n, "feature:invariant", str_assert);
|
||||
}
|
||||
|
||||
Delete(list_assert);
|
||||
Delete(list_params);
|
||||
Delete(s);
|
||||
Delete(tag);
|
||||
return SWIG_OK;
|
||||
}
|
||||
|
||||
int emit_contract(Node *n) {
|
||||
int ret = SWIG_OK;
|
||||
if (!Getattr(n, "feature:contract"))
|
||||
return SWIG_ERROR;
|
||||
//Printf(stdout, "--------In emit_contract code:\nname is : %s\n",
|
||||
// Getattr(n,"name"));
|
||||
// Split contract into preassert & postassert
|
||||
if (!SliptContract(n))
|
||||
return SWIG_ERROR;
|
||||
|
||||
// Modify pre- , post- * invar-
|
||||
ret = AssertModify(n, 1);
|
||||
ret = AssertModify(n, 2);
|
||||
ret = AssertModify(n, 3);
|
||||
/*
|
||||
Printf(stdout, "preassert after Setmeta :\n%s\n",
|
||||
Getattr(n, "feature:preassert"));
|
||||
Printf(stdout, "postassert after Setmeta :\n%s\n",
|
||||
Getattr(n, "feature:postassert"));
|
||||
Printf(stdout, "invariant after Setmeta :\n%s\n",
|
||||
Getattr(n, "feature:invariant"));
|
||||
*/
|
||||
return ret;
|
||||
}
|
||||
|
||||
/*
|
||||
virtual int emit_one(Node *n) {
|
||||
int ret = SWIG_OK;
|
||||
char *tag = Char(nodeType(n));
|
||||
|
||||
if (!n) return SWIG_OK;
|
||||
|
||||
if (strcmp(tag,"include") == 0)
|
||||
ret = emit_children(n);
|
||||
else if (strcmp(tag, "top") == 0)
|
||||
ret = top(n);
|
||||
else if (Getattr(n, "feature:contract")) {
|
||||
ret = emit_contract(n);
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
*/
|
||||
int cDeclaration(Node *n) {
|
||||
int ret = SWIG_OK;
|
||||
if (Getattr(n, "feature:contract"))
|
||||
ret = emit_contract(n);
|
||||
return ret;
|
||||
}
|
||||
|
||||
int constructorDeclaration(Node *n){
|
||||
int ret = SWIG_OK;
|
||||
InConstructor = 1;
|
||||
if (Getattr(n, "feature:contract"))
|
||||
ret = emit_contract(n);
|
||||
InConstructor = 0;
|
||||
return ret;
|
||||
}
|
||||
|
||||
int destructorDeclaration(Node *n){
|
||||
int ret = SWIG_OK;
|
||||
InDestructor = 1;
|
||||
if (Getattr(n, "feature:contract"))
|
||||
ret = emit_contract(n);
|
||||
InDestructor = 0;
|
||||
return ret;
|
||||
}
|
||||
|
||||
int externDeclaration(Node *n) { return emit_children(n); }
|
||||
int extendDirective(Node *n) { return emit_children(n); }
|
||||
int importDirective(Node *n) { return emit_children(n); }
|
||||
int includeDirective(Node *n) { return emit_children(n); }
|
||||
int classDeclaration(Node *n) {
|
||||
int ret = SWIG_OK;
|
||||
InClass = 1;
|
||||
CurrentClass = n;
|
||||
ret = classHandler(n);
|
||||
InClass = 0;
|
||||
CurrentClass = 0;
|
||||
return ret;
|
||||
}
|
||||
int classHandler(Node *n) {
|
||||
emit_children(n);
|
||||
return SWIG_OK;
|
||||
}
|
||||
|
||||
virtual int importDirective(Node *n) { return emit_children(n); }
|
||||
virtual int includeDirective(Node *n) { return emit_children(n); } // ?
|
||||
virtual int externDeclaration(Node *n) { return emit_children(n); }
|
||||
|
||||
String * strParms(ParmList *l) {
|
||||
int comma = 0;
|
||||
int i = 0;
|
||||
Parm *p = l;
|
||||
SwigType *pt;
|
||||
String * returns = NewString("");
|
||||
while(p) {
|
||||
String *pname;
|
||||
pt = Getattr(p,"type");
|
||||
if ((SwigType_type(pt) != T_VOID)) {
|
||||
if (comma) Printf(returns,",");
|
||||
pname = Swig_cparm_name(p,i);
|
||||
Printf(returns,"%s",SwigType_rcaststr(pt,pname));
|
||||
comma = 1;
|
||||
i++;
|
||||
}
|
||||
p = nextSibling(p);
|
||||
}
|
||||
return returns;
|
||||
}
|
||||
|
||||
virtual int cDeclaration(Node *n) {
|
||||
String *name = Getattr(n,"name");
|
||||
String *k = Getattr(n,"feature:contract");
|
||||
|
||||
if(k)
|
||||
{
|
||||
/* make the names */
|
||||
ParmList *l = Getmeta(k,"parms");
|
||||
String *params = ParmList_str(l);
|
||||
String *transformed = strParms(l);
|
||||
if(DohStrcmp(params,"")==0) {
|
||||
DohDelete(params);
|
||||
params = DohNewString("void");
|
||||
}
|
||||
String *contractName = DohNewStringf("__SWIG_precontract_%s",name);
|
||||
|
||||
/* make the contract */
|
||||
String *contract = DohNewStringf("int %s(%s,int rt[2])\n{\n",contractName,params);
|
||||
SwigScanner * ss = NewSwigScanner();
|
||||
SwigScanner_clear(ss);
|
||||
SwigScanner_push(ss,Copy(k));
|
||||
SwigScanner_token(ss); // Get rid of the '{' at the begining
|
||||
|
||||
/* loop over the clauses */
|
||||
int clauseNum = 1;
|
||||
int token = -1;
|
||||
while(1) {
|
||||
String *clause = DohNewString(""); /*BUG -- should free*/
|
||||
while((token=SwigScanner_token(ss))) {
|
||||
if ((token==SWIG_TOKEN_SEMI)||(token==SWIG_TOKEN_RBRACE))
|
||||
break;
|
||||
// if (token != SWIG_TOKEN_ENDLINE)
|
||||
Printf(clause,"%s",SwigScanner_text(ss));
|
||||
}
|
||||
if (DohStrcmp(clause,"\n") != 0) {
|
||||
Printf(contract,"if (!(%s",clause);
|
||||
Printf(contract,")) {\nrt[0]=__LINE__;\nrt[1]=%i;\nreturn 1;\n}\n",clauseNum);
|
||||
}
|
||||
if(token==SWIG_TOKEN_RBRACE) break;
|
||||
clauseNum++;
|
||||
}
|
||||
|
||||
/* finish it off and attach it to the main tree */
|
||||
Printf(contract,"return 0;\n}\n");
|
||||
Setattr(n,"wrap:code",contract); /*BUG -- WHAT IF SOMETHING IS ALREADY THERE*/
|
||||
|
||||
/* Generate the calling code */
|
||||
String * calling = DohNewString("{\nint cfail[2];\nchar message[255];\n");
|
||||
Printf(calling,"if (%s(%s,cfail)) {\n",contractName,transformed);
|
||||
Printf(calling,"sprintf(message,\"Contract %s failed on clause %%i (line %%i)!\",cfail[1],cfail[0]);\n",contractName);
|
||||
Printf(calling,"PyErr_SetString(PyExc_Exception,message);return NULL;\n}\n");
|
||||
Printf(calling,"}\n");
|
||||
/* Setattr(n,"feature:preassert",calling); */
|
||||
}
|
||||
/*There are two attributes "feature:preassert" and "feature:postassert".*/
|
||||
|
||||
|
||||
virtual int top(Node *n) {
|
||||
emit_children(n);
|
||||
return SWIG_OK;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
void Swig_contracts(Node *n) {
|
||||
Printf(stdout,"Applying contracts (experimental v0.09)\n");
|
||||
Printf(stdout,"Applying contracts (experimental version)\n");
|
||||
|
||||
Contracts *a = new Contracts;
|
||||
a->top(n);
|
||||
delete a;
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -364,6 +364,7 @@ void replace_args(Parm *p, String *s) {
|
|||
/* replace_contract_args. This function replaces argument names in contract
|
||||
specifications. Used in conjunction with the %contract directive. */
|
||||
|
||||
//replace_contract_args(Getmeta(tm,"parms"), Getattr(n,"parms"),tm);
|
||||
static
|
||||
void replace_contract_args(Parm *cp, Parm *rp, String *s) {
|
||||
while (cp && rp) {
|
||||
|
|
@ -374,7 +375,7 @@ void replace_contract_args(Parm *cp, Parm *rp, String *s) {
|
|||
cp = nextSibling(cp);
|
||||
rp = nextSibling(rp);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* -----------------------------------------------------------------------------
|
||||
* int emit_action()
|
||||
|
|
@ -429,6 +430,16 @@ void emit_action(Node *n, Wrapper *f) {
|
|||
tm = Getattr(n,"feature:preassert");
|
||||
if (tm) {
|
||||
replace_contract_args(Getmeta(tm,"parms"), Getattr(n,"parms"),tm);
|
||||
/* Printf(stdout, "name: %s, preassert: %s\n", Getattr(n,"name"), tm); */
|
||||
Printv(f->code,tm,"\n",NIL);
|
||||
}
|
||||
|
||||
/* Invariant -- EXPERIMENTAL */
|
||||
tm = Getattr(n,"feature:invariant");
|
||||
if (tm) {
|
||||
replace_contract_args(Getmeta(tm,"parms"), Getattr(n,"parms"),tm);
|
||||
Replaceid(tm, "SWIG_invariant", "SWIG_invariant_begin");
|
||||
/* Printf(stdout, "name: %s, invarassert: %s\n", Getattr(n,"name"), tm); */
|
||||
Printv(f->code,tm,"\n",NIL);
|
||||
}
|
||||
|
||||
|
|
@ -476,10 +487,19 @@ void emit_action(Node *n, Wrapper *f) {
|
|||
Printf(f->code,"catch(...) { throw; }\n");
|
||||
}
|
||||
|
||||
/* Invariant -- EXPERIMENTAL */
|
||||
tm = Getattr(n,"feature:invariant");
|
||||
if (tm) {
|
||||
replace_contract_args(Getmeta(tm,"parms"), Getattr(n,"parms"),tm);
|
||||
Replaceid(tm, "SWIG_invariant", "SWIG_invariant_end");
|
||||
/* Printf(stdout, "name: %s, invarassert: %s\n", Getattr(n,"name"), tm); */
|
||||
Printv(f->code,tm,"\n",NIL);
|
||||
}
|
||||
/* Postassert - EXPERIMENTAL */
|
||||
tm = Getattr(n,"feature:postassert");
|
||||
if (tm) {
|
||||
replace_contract_args(Getmeta(tm,"parms"), Getattr(n,"parms"),tm);
|
||||
/* Printf(stdout, "name: %s, postassert: %s\n", Getattr(n,"name"), tm); */
|
||||
Printv(f->code,tm,"\n",NIL);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -621,9 +621,6 @@ int SWIG_main(int argc, char *argv[], Language *l) {
|
|||
if (dump_tags) {
|
||||
Swig_print_tags(top,0);
|
||||
}
|
||||
if (dump_tree) {
|
||||
Swig_print_tree(top);
|
||||
}
|
||||
if (top) {
|
||||
if (!Getattr(top,"name")) {
|
||||
Printf(stderr,"*** No module name specified using %%module or -module.\n");
|
||||
|
|
@ -656,6 +653,9 @@ int SWIG_main(int argc, char *argv[], Language *l) {
|
|||
}
|
||||
}
|
||||
}
|
||||
if (dump_tree) {
|
||||
Swig_print_tree(top);
|
||||
}
|
||||
}
|
||||
if (tm_debug) Swig_typemap_debug();
|
||||
if (memory_debug) DohMemoryDebug();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue