git-svn-id: https://swig.svn.sourceforge.net/svnroot/swig/trunk/SWIG@4875 626c5289-ae23-0410-ae9c-e8d60b6d4f22
398 lines
12 KiB
C++
398 lines
12 KiB
C++
/* -----------------------------------------------------------------------------
|
|
* contract.cxx
|
|
*
|
|
* Support for Wrap by Contract in SWIG
|
|
*
|
|
* Author(s) : Songyan Feng (Tiger) (songyanf@cs.uchicago.edu)
|
|
*
|
|
* Department of Computer Science
|
|
* University of Chicago
|
|
*
|
|
* Copyright (C) 1999-2003. The University of Chicago
|
|
* See the file LICENSE for information on usage and redistribution.
|
|
* ----------------------------------------------------------------------------- */
|
|
|
|
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 Contract_Mode = 0; /* contract option */
|
|
|
|
static int InClass = 0; /* Parsing C++ or not */
|
|
static Node *CurrentClass = 0;
|
|
static int InConstructor = 0;
|
|
static int InDestructor = 0;
|
|
|
|
void Swig_contract_mode_set(int flag) {
|
|
Contract_Mode = flag;
|
|
}
|
|
|
|
int Swig_contract_mode_get() {
|
|
return Contract_Mode;
|
|
}
|
|
|
|
class Contracts : public Dispatcher {
|
|
|
|
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, *expr, *tag_sync;
|
|
List *list_assert;
|
|
|
|
if (flag == 1) { /* preassert */
|
|
str_assert = NewString(Getattr(n, "feature:preassert"));
|
|
} 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;
|
|
|
|
/* 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 (expr = Firstitem(list_assert); expr; expr = Nextitem(list_assert)) {
|
|
if (Len(expr)) {
|
|
/* All sync staff are not complete and only experimental */
|
|
if (Strstr(expr, SWIG_BEFORE)) { /* before sync assertion */
|
|
tag_sync = NewString(" SWIG_sync(");
|
|
Append(tag_sync, Getattr(n, "name"));
|
|
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(expr);
|
|
return SWIG_OK;
|
|
}
|
|
|
|
/* Modify format into { SWIG_xxxassert(...);\n ...} */
|
|
int AssertAddTag(Node *n) {
|
|
String *str_assert, *tag;
|
|
/* preassert */
|
|
str_assert = NewString(Getattr(n, "feature:preassert"));
|
|
if (Len(str_assert)) {
|
|
tag = NewString(" SWIG_preassert(");
|
|
Append(tag, str_assert);
|
|
Append(tag, ");\n");
|
|
Setattr(n, "feature:preassert", tag);
|
|
Delete(tag);
|
|
}
|
|
Delete(str_assert);
|
|
|
|
/* postassert */
|
|
str_assert = NewString(Getattr(n, "feature:postassert"));
|
|
if (Len(str_assert)) {
|
|
tag = NewString(" SWIG_postassert(");
|
|
Append(tag, str_assert);
|
|
Append(tag, ");\n");
|
|
Setattr(n, "feature:postassert", tag);
|
|
Delete(tag);
|
|
}
|
|
Delete(str_assert);
|
|
|
|
/* invariant */
|
|
str_assert = NewString(Getattr(n, "feature:invariant"));
|
|
if (Len(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 AssertAddErrorMsg(Node *n) {
|
|
String *str_assert, *error_msg;
|
|
/* preassert */
|
|
str_assert = NewString(Getattr(n, "feature:preassert"));
|
|
Replaceall(str_assert, ");\n", "");
|
|
if (Len(str_assert)) {
|
|
error_msg = NewString("\\nRequire assertion violation,");
|
|
Printf(error_msg, "in function of <<%s>>\\n", Getattr(n, "name"));
|
|
Printf(str_assert, ", \"%s\");\n", error_msg);
|
|
Setattr(n, "feature: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("\\nEnsure assertion violation,");
|
|
Printf(error_msg, "in function of <<%s>>\\n", Getattr(n, "name"));
|
|
Printf(str_assert, ", \"%s\");\n", error_msg);
|
|
Setattr(n, "feature: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("\\nInvariant assertion violation,");
|
|
Printf(error_msg, "in function of <<%s>>\\n", 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 AssertSetParms(Node *n) {
|
|
ParmList *list_params;
|
|
String *str_assert_pre,*str_assert_post,*str_assert_invar;
|
|
|
|
str_assert_pre = NewString(Getattr(n, "feature:preassert"));
|
|
str_assert_post = NewString(Getattr(n, "feature:postassert"));
|
|
str_assert_invar = NewString(Getattr(n, "feature:invariant"));
|
|
|
|
/* 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_pre, "parms", list_params);
|
|
Setmeta(str_assert_post, "parms", list_params);
|
|
Setmeta(str_assert_invar, "parms", list_params);
|
|
|
|
Setattr(n, "feature:preassert", str_assert_pre);
|
|
Setattr(n, "feature:postassert", str_assert_post);
|
|
Setattr(n, "feature:invariant", str_assert_invar);
|
|
|
|
Delete(list_params);
|
|
Delete(str_assert_pre);
|
|
Delete(str_assert_post);
|
|
Delete(str_assert_invar);
|
|
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 contracqt into preassert & postassert */
|
|
if (!SliptContract(n))
|
|
return SWIG_ERROR;
|
|
|
|
/* Modify pre- , post- * invar- */
|
|
ret = ret && AssertModify(n, 1);
|
|
ret = ret && AssertModify(n, 2);
|
|
ret = ret && AssertModify(n, 3);
|
|
ret = ret && AssertAddTag(n);
|
|
ret = ret && AssertAddErrorMsg(n);
|
|
ret = ret && AssertSetParms(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 top(Node *n) {
|
|
emit_children(n);
|
|
return SWIG_OK;
|
|
}
|
|
};
|
|
|
|
void Swig_contracts(Node *n) {
|
|
Printf(stdout,"Applying contracts (experimental version)\n");
|
|
|
|
Contracts *a = new Contracts;
|
|
a->top(n);
|
|
delete a;
|
|
}
|