From: drl7x Date: Fri, 13 Oct 2000 00:28:00 +0000 (+0000) Subject: Converted to new API for constraintExpr X-Git-Tag: prewinterbreak~8 X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/commitdiff_plain/92c4a78635fd7baf52eb7ede90b735be84089dd7 Converted to new API for constraintExpr g++; g++; is now handled correctly. --- diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 12a52a6..e6d7824 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -1,19 +1,6 @@ -typedef union constraintTermValue_ -{ - constraintExpr constrExpr; - exprNode expr; - sRef sref; - int intlit; -} constraintTermValue; - - -typedef enum -{ - EXPRNODE, SREF, - CONSTRAINTEXPR, - INTLITERAL -} constraintTermType; +#ifndef __constraint_h__ +#define __constraint_h__ typedef enum { @@ -21,42 +8,6 @@ typedef enum } arithType; -typedef enum -{ - //BUFFSIZE, STRINGLEN, - VALUE, CALLSAFE, - MAXSET, MINSET, MAXREAD, MINREAD, - NULLTERMINATED, - UNDEFINED -} -constraintType; - -typedef enum -{ - PLUS, - MINUS -} -constraintExprOp; - - -struct _constraintTerm { - constraintType constrType; - fileloc loc; - constraintTermValue value; - constraintTermType kind; -}; - -abst_typedef struct _constraintTerm * constraintTerm; - -struct constraintExpr_ { - - constraintTerm term; - constraintExprOp op; - struct constraintExpr_ * expr; -}; -# define constraintExpr_undefined ((constraintExpr)NULL) - - //abst_typedef struct constr_ * constr; @@ -68,6 +19,8 @@ struct _constraint { bool post; } ; +abst_typedef struct _constraintTerm * constraintTerm; + //constraint constraint_create (exprNode e1, exprNode e2, arithType restriction, constraintType kind); constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2); @@ -101,7 +54,6 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode p_t1, exprNode p_t2, fi constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint); constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint); -cstring constraintType_print (constraintType c1); constraint constraint_copy (constraint c); @@ -114,13 +66,14 @@ cstring constraintTerm_print (constraintTerm term); cstring arithType_print (arithType ar); cstring constraintExpr_print (constraintExpr ex); - +fileloc constraint_getFileloc (constraint c); cstring constraint_print (constraint c); /*@=czechfcns*/ #warning take this out #include "constraintList.h" +#include "constraintExpr.h" #include "constraintTerm.h" - +#endif diff --git a/src/Headers/constraintTerm.h b/src/Headers/constraintTerm.h index be1c39e..9eaf7e8 100644 --- a/src/Headers/constraintTerm.h +++ b/src/Headers/constraintTerm.h @@ -1,7 +1,25 @@ +#ifndef __constraintTerm_h__ + +#define __constraintTerm_h__ + +constraintTerm constraintTerm_simplify (constraintTerm term); + +constraintTerm constraintTerm_makeExprNode (/*@only@*/ exprNode e); + constraintTerm constraintTerm_copy (constraintTerm term); -constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e); +constraintTerm exprNode_makeConstraintTerm ( exprNode e); + + +bool constraintTerm_same (constraintTerm term1, constraintTerm term2); + +bool constraintTerm_similar (constraintTerm term1, constraintTerm term2); + +bool constraintTerm_canGetValue (constraintTerm term); +int constraintTerm_getValue (constraintTerm term); + +fileloc constraintTerm_getFileloc (constraintTerm t); constraintTerm constraintTerm_makeMaxSetexpr (exprNode e); @@ -17,8 +35,14 @@ constraintTerm intLit_makeConstraintTerm (int i); constraintTerm constraintTerm_makeIntLitValue (int i); -cstring constraintType_print (constraintType constrType); +bool constraintTerm_isIntLiteral (constraintTerm term); cstring constraintTerm_print (constraintTerm term); +#endif + + + + + diff --git a/src/Makefile.sources b/src/Makefile.sources index 7e8cf28..a936d99 100644 --- a/src/Makefile.sources +++ b/src/Makefile.sources @@ -27,6 +27,8 @@ GENERALSRC = cstring.c fileloc.c message.c source.c \ fileTable.c hashTable.c llerror.c messageLog.c \ constraint.c \ constraintTerm.c \ + constraintExpr.c \ + constraintExprData.c \ constraintResolve.c \ environmentTable.c \ constraintList.c \ diff --git a/src/constraint.c b/src/constraint.c index 7693e2f..133f99f 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -38,6 +38,22 @@ constraint constraint_copy (constraint c) return ret; } +/*like copy expect it doesn't allocate memory for the constraint*/ + +void constraint_overWrite (constraint c1, constraint c2) +{ + c1->lexpr = constraintExpr_copy (c2->lexpr); + c1->ar = c2->ar; + c1->expr = constraintExpr_copy (c2->expr); + c1->post = c2->post; + /*@i33 fix this*/ + if (c2->orig != NULL) + c1->orig = constraint_copy (c2->orig); + else + c1->orig = NULL; + +} + bool constraint_resolve (/*@unused@*/ constraint c) { return FALSE; @@ -57,102 +73,14 @@ bool constraint_resolve (/*@unused@*/ constraint c) ret->orig = NULL; /*@i23*/return ret; } -/*@-czechfcns@*/ -constraintExpr constraintExpr_alloc () -{ - constraintExpr ret; - ret = dmalloc (sizeof (*ret) ); - ret->term = NULL; - ret->expr = NULL; - ret->op = PLUS; - return ret; -} - -constraintExpr constraintExpr_copy (constraintExpr expr) -{ - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_copy(expr->term); - ret->op = expr->op; - if (expr->expr != NULL) - { - ret->expr = constraintExpr_copy (expr->expr); - } - else - { - ret->expr = NULL; - } - return ret; -} - -constraintExpr constraintExpr_makeMaxSetExpr (exprNode expr) -{ - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeMaxSetexpr(expr); - return ret; -} - -constraintExpr constraintExpr_makeMaxReadExpr (exprNode expr) -{ - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeMaxReadexpr(expr); - return ret; -} -constraintExpr constraintExpr_makeMinSetExpr (exprNode expr) +fileloc constraint_getFileloc (constraint c) { - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeMinSetexpr(expr); - return ret; -} - -constraintExpr constraintExpr_makeMinReadExpr (exprNode expr) -{ - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeMinReadexpr(expr); - return ret; -} - -constraintExpr constraintExpr_makeValueExpr (exprNode expr) -{ - constraintExpr ret; - ret = constraintExpr_alloc(); - ret->term = constraintTerm_makeValueexpr(expr); - return ret; -} - - -constraintExpr makeConstraintExprIntlit (int i) -{ - constraintExpr ret; - ret = dmalloc (sizeof (*ret) ); - ret->term = constraintTerm_makeIntLitValue(i); - ret->expr = NULL; - ret->op = PLUS; - /*@i1*/ return ret; -} + return (constraintExpr_getFileloc (c->lexpr) ); -constraintExpr constraintExpr_makeValueInt (int i) -{ - return makeConstraintExprIntlit(i); } -constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) -{ - constraint ret = constraint_makeNew(); - constraintTerm term; - - ret->lexpr =constraintExpr_makeMaxSetExpr(po); - ret->ar = GTE; - ret->expr = constraintExpr_makeValueExpr (ind); - /*@i1*/return ret; -} - constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind) { constraint ret = constraint_makeNew(); @@ -168,14 +96,25 @@ constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind) constraint constraint_makeWriteSafeInt (exprNode po, int ind) { constraint ret = constraint_makeNew(); - constraintTerm term; + ret->lexpr =constraintExpr_makeMaxSetExpr(po); ret->ar = GTE; ret->expr = constraintExpr_makeValueInt (ind); /*@i1*/return ret; } - + +constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) +{ + constraint ret = constraint_makeNew(); + + + ret->lexpr =constraintExpr_makeMaxSetExpr(po); + ret->ar = GTE; + ret->expr = constraintExpr_makeValueExpr (ind); + /*@i1*/return ret; +} + constraint constraint_makeReadSafeInt ( exprNode po, int ind) { constraint ret = constraint_makeNew(); @@ -191,94 +130,53 @@ constraint constraint_makeReadSafeInt ( exprNode po, int ind) constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint) { constraint ret = constraint_makeNew(); - constraintTerm term; + e1 = exprNode_fakeCopy (e1); t2 = exprNode_fakeCopy (t2); ret = constraint_makeReadSafeExprNode(e1, t2); - if (ret->lexpr->term->loc != NULL) - fileloc_free(ret->lexpr->term->loc); + + ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); - ret->lexpr->term->loc = fileloc_copy (sequencePoint); ret->post = TRUE; - fileloc_incColumn (ret->lexpr->term->loc); + // fileloc_incColumn (ret->lexpr->term->loc); return ret; } -constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint) -{ - constraint ret = constraint_makeNew(); - constraintTerm term; - po = exprNode_fakeCopy(po); - ind = exprNode_fakeCopy(ind); - - ret->lexpr = constraintExpr_makeMinReadExpr(po); - ret->ar = LTE; - ret->expr = constraintExpr_makeValueExpr (ind); - ret->post = TRUE; - - if (ret->lexpr->term->loc != NULL) - fileloc_free(ret->lexpr->term->loc); - - ret->lexpr->term->loc = fileloc_copy (sequencePoint); - /*make this refer to element after preconditions */ - fileloc_incColumn (ret->lexpr->term->loc); - /*@i1*/ return ret; -} - -constraintExpr makeMaxSetPostOpInc (exprNode e) -{ - constraintExpr ret; - ret = constraintExpr_makeValueExpr (e); - ret->op = PLUS; - ret->expr = makeConstraintExprIntlit (1); - return ret; -} - constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint) { constraint ret = constraint_makeNew(); //constraintTerm term; - exprNode t2; + e = exprNode_fakeCopy(e); ret->lexpr = constraintExpr_makeValueExpr (e); ret->ar = EQ; ret->post = TRUE; - ret->expr = makeMaxSetPostOpInc(e); - - fileloc_incColumn ( ret->lexpr->term->loc); - fileloc_incColumn ( ret->lexpr->term->loc); - return ret; -} + ret->expr = constraintExpr_makeValueExpr (e); + ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr); -constraintExpr makeMaxReadPostOpInc (exprNode e) -{ - constraintExpr ret; - ret = constraintExpr_makeValueExpr (e); - ret->term = constraintTerm_makeMaxReadexpr (e); - ret->op = MINUS; - ret->expr = makeConstraintExprIntlit (1); + ret->expr = constraintExpr_setFileloc (ret->expr, sequencePoint); +// fileloc_incColumn ( ret->lexpr->term->loc); +// fileloc_incColumn ( ret->lexpr->term->loc); return ret; } -constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint) -{ - constraint ret = constraint_makeNew(); - //constraintTerm term; - exprNode t2; - e = exprNode_fakeCopy(e); - ret->lexpr = constraintExpr_makeMaxReadExpr(e); - ret->ar = EQ; - ret->post = TRUE; - ret->expr = makeMaxReadPostOpInc(e); +// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint) +// { +// constraint ret = constraint_makeNew(); +// //constraintTerm term; - fileloc_incColumn ( ret->lexpr->term->loc); - fileloc_incColumn ( ret->lexpr->term->loc); - return ret; -} +// e = exprNode_fakeCopy(e); +// ret->lexpr = constraintExpr_makeMaxReadExpr(e); +// ret->ar = EQ; +// ret->post = TRUE; +// ret->expr = constraintExpr_makeIncConstraintExpr (e); +// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint); +// return ret; +// } cstring arithType_print (arithType ar) @@ -314,30 +212,6 @@ cstring arithType_print (arithType ar) return st; } -cstring constraintExpr_print (constraintExpr ex) -{ - cstring st; - cstring opStr; - llassert (ex != NULL); - - st = message ("%s", - constraintTerm_print (ex->term)); - - if (ex->expr != NULL) - { - if (ex->op == PLUS) - { - opStr = cstring_makeLiteral (" + "); - } - else - { - opStr = cstring_makeLiteral (" - "); - } - st = message ("%s %s %s", st, opStr, constraintExpr_print (ex->expr) ); - } - return st; -} - cstring constraint_printDetailed (constraint c) { @@ -377,31 +251,18 @@ cstring constraint_print (constraint c) return st; } -bool constraint_hasTerm (constraint c, constraintTerm term) -{ - DPRINTF((message ("Constraint %s", constraint_print (c) ) ) ); +// bool constraint_hasTerm (constraint c, constraintTerm term) +// { +// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) ); - if (constraintExpr_includesTerm (c->lexpr, term) ) - return TRUE; - - if (constraintExpr_includesTerm (c->expr, term) ) - return TRUE; - - return FALSE; -} +// if (constraintExpr_includesTerm (c->lexpr, term) ) +// return TRUE; -bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term) -{ - if (constraintTerm_hasTerm (expr->term, term) ) - return TRUE; +// if (constraintExpr_includesTerm (c->expr, term) ) +// return TRUE; - if ( (expr->expr) != NULL) - { - return ( constraintExpr_includesTerm (expr->expr, term) ); - } - return FALSE; - -} +// return FALSE; +// } constraint constraint_preserveOrig (constraint c) { diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 70e1ae8..763a7ac 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -179,9 +179,10 @@ bool exprNode_stmt (exprNode e) loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */ notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc); e->requiresConstraints = exprNode_traversRequiresConstraints(snode); - // printf ("%s\n", constraintList_print(e->requiresConstraints) ); + printf ("For: %s \n", exprNode_unparse (e) ); + printf ("%s\n", constraintList_print(e->requiresConstraints) ); e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode); - // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) ); + printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) ); llassert(notError); return notError; @@ -220,6 +221,7 @@ bool exprNode_stmtList (exprNode e) exprNode_stmt (stmt2); mergeResolve (e, stmt1, stmt2 ); + DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_print(e->requiresConstraints), constraintList_print(e->ensuresConstraints) ) ) ); diff --git a/src/constraintResolve.c b/src/constraintResolve.c index 6367d5c..dc4b919 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -14,201 +14,183 @@ # include "exprNodeSList.h" # include "exprData.i" +#include "constraintExpr.h" -int constraintExpr_getValue (constraintExpr expr) -{ - if (expr->expr != NULL) - { - TPRINTF( ( "Not Implemented" )); - llassert(FALSE); - } - return (constraintTerm_getValue (expr->term) ); -} +constraintList reflectChanges (constraintList pre2, constraintList post1); +constraint substitute (constraint c, constraintList p); +constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new); +bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2); +bool satifies (constraint pre, constraint post); +bool resolve (constraint c, constraintList p); +constraintList reflectChangesEnsures (constraintList pre2, constraintList post1); +constraint constraint_simplify (constraint c); -// returns 1 0 -1 like strcopy -int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2) +void mergeResolve (exprNode parent, exprNode child1, exprNode child2) { - int value1, value2; + constraintList temp; + TPRINTF( (message ("magically merging constraint into parent:%s for children: %s and %s", exprNode_unparse (parent), exprNode_unparse (child1), exprNode_unparse(child2) ) + ) ); + if (exprNode_isError (child1) || exprNode_isError(child2) ) + { + if (exprNode_isError (child1) && !exprNode_isError(child2) ) + { + parent->requiresConstraints = constraintList_copy (child2->requiresConstraints); + parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints); + TPRINTF((message ("Copied child constraints: pre: %s and post: %s", + constraintList_print( child2->requiresConstraints), + constraintList_print (child2->ensuresConstraints) + ) + )); + return; + } + else + { + llassert(exprNode_isError(child2) ); + parent->requiresConstraints = constraintList_new(); + parent->ensuresConstraints = constraintList_new(); + return; + } + } - value1 = constraintExpr_getValue(expr1); - value2 = constraintExpr_getValue(expr2); + llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) ); + + TPRINTF( (message ("Child constraints are %s %s and %s %s", + constraintList_print (child1->requiresConstraints), + constraintList_print (child1->ensuresConstraints), + constraintList_print (child2->requiresConstraints), + constraintList_print (child2->ensuresConstraints) + ) ) ); + + parent->requiresConstraints = constraintList_new(); + parent->ensuresConstraints = constraintList_new(); - if (value1 > value2) - return 1; + parent->requiresConstraints = constraintList_copy (child1->requiresConstraints); + + temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints); + parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp); - if (value1 == value2) - return 0; + + temp = reflectChangesEnsures (child1->ensuresConstraints, child2->ensuresConstraints); + // temp = constraintList_copy (child1->ensuresConstraints); - else - return -1; + temp = constraintList_fixConflicts (temp, child2->ensuresConstraints); + + parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints); + parent->ensuresConstraints = constraintList_addList (parent->ensuresConstraints, temp); + + TPRINTF( (message ("Parent constraints are %s and %s ", + constraintList_print (parent->requiresConstraints), + constraintList_print (parent->ensuresConstraints) + ) ) ); + } -bool constraintExpr_canCompare (constraintExpr expr1, constraintExpr expr2) -{ - if (expr1->expr != NULL) - { - return FALSE; - } - if (expr2->expr != NULL) + +constraintList reflectChanges (constraintList pre2, constraintList post1) +{ + + constraintList ret; + constraint temp; + ret = constraintList_new(); + constraintList_elements (pre2, el) { - return FALSE; - } + if (!resolve (el, post1) ) + { + temp = substitute (el, post1); + ret = constraintList_add (ret, temp); + } + } end_constraintList_elements; - return TRUE; + return ret; } -bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2) -{ - switch (ar1) - { - case GTE: - case GT: - /*irst constraint is > only > => or == cosntraint can satify it */ - if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) ) - { - if (! constraintExpr_canCompare (expr1, expr2) ) - return FALSE; - - if (constraintExpr_compare (expr2, expr1) >= 0) - return TRUE; - - } - return FALSE; - default: - TPRINTF(("case not handled")); - } - return FALSE; -} -/*returns true if cosntraint post satifies cosntriant pre */ -bool satifies (constraint pre, constraint post) -{ - if (!constraintTerm_same(pre->lexpr->term, post->lexpr->term) ) +constraintList reflectChangesEnsures (constraintList pre2, constraintList post1) +{ + constraintList ret; + constraint temp; + ret = constraintList_new(); + constraintList_elements (pre2, el) { - return FALSE; - } - if (post->expr == NULL) - return FALSE; + if (!resolve (el, post1) ) + { + temp = substitute (el, post1); + if (temp != NULL) + ret = constraintList_add (ret, temp); + } + } end_constraintList_elements; - return rangeCheck (pre->ar, pre->expr, post->ar, post->expr); + return ret; } -constraintExpr constraintExpr_simplify (constraintExpr expr) + +bool constraint_conflict (constraint c1, constraint c2) { - expr->term = constraintTerm_simplify (expr->term); - if (expr->expr == NULL) + if (constraintExpr_similar(c1->lexpr, c2->lexpr) ) { - if ( (expr->term->kind == CONSTRAINTEXPR) && (expr->term->constrType == VALUE) ) + if (c1->ar == c2->ar) { - expr->op = expr->term->value.constrExpr->op; - expr->expr = expr->term->value.constrExpr->expr; - expr->term = expr->term->value.constrExpr->term; + TPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); + return TRUE; } - - return expr; - } - - expr->expr = constraintExpr_simplify (expr->expr); + } - - - if ( (expr->term->kind == INTLITERAL) && (expr->expr->term->kind == INTLITERAL) ) - { - DPRINTF( ("INTLITERAL MERGE " )); + TPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); - DPRINTF ( (message ("Expression is %s ", constraintExpr_print (expr) ) ) ); - - if (expr->op == PLUS ) - { - DPRINTF( (message ("Adding %d and %d ", expr->term->value.intlit, - expr->expr->term->value.intlit) ) ); - expr->term->value.intlit += expr->expr->term->value.intlit; - } - else if (expr->op == MINUS ) - { - expr->term->value.intlit -= expr->expr->term->value.intlit; - } - expr->op = expr->expr->op; + return FALSE; - expr->expr = expr->expr->expr; - } - - return expr; - } -constraintExpr constraintExpr_add (constraintExpr e, constraintTerm term, constraintExprOp op) +void constraint_fixConflict (constraint good, constraint conflicting) { - constraintExpr p; - - p = e; - while (p->expr != NULL) + constraint temp; + if (conflicting->ar ==EQ ) { - p = p->expr; + good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr); + temp = constraint_simplify (good); + constraint_overWrite (good, temp); } - p->op = op; - p->expr = constraintExpr_alloc(); - p->expr->term = term; - return e; } -constraintExpr termMove (constraintExpr dst, constraintExpr src) +bool conflict (constraint c, constraintList list) { - constraintTerm term; - llassert (src->expr != NULL); - term = src->expr->term; - if (src->op == PLUS) - dst = constraintExpr_add (dst, term, MINUS); - else - if (src->op == MINUS) - dst = constraintExpr_add (dst, term, PLUS); - return dst; -} + constraintList_elements (list, el) + { + if ( constraint_conflict(el, c) ) + { + constraint_fixConflict (el, c); + return TRUE; + } + } end_constraintList_elements; -constraint solveforterm (constraint c) -{ - constraintExpr p; - p = c->lexpr; - while (p->expr != NULL) - { - DPRINTF( (message("Moving %s", constraintExpr_print (c->expr) ) ) ); - c->expr = termMove(c->expr, p); - p->op = p->expr->op; - #warning memleak + return FALSE; + - p->expr = p->expr->expr; - } - return c; } -constraint solveforOther (constraint c) +//check if constraint in list1 and conflict with constraints in List2. If so we +//remove form list1 and (optionally) change list2. +constraintList constraintList_fixConflicts (constraintList list1, constraintList list2) { - constraintExpr p; - p = c->expr; - while (p->expr != NULL) - { - TPRINTF( (message("Moving %s", constraintExpr_print (c->expr) ) ) ); - c->lexpr = termMove(c->lexpr, p); - p->op = p->expr->op; - #warning memleak - - p->expr = p->expr->expr; - } - return c; -} + constraintList ret; + ret = constraintList_new(); + constraintList_elements (list1, el) + { + if (! conflict (el, list2) ) + { + ret = constraintList_add (ret, el); + } + } end_constraintList_elements; -constraint constraint_simplify (constraint c) -{ - c = solveforterm (c); - c->lexpr = constraintExpr_simplify (c->lexpr); - c->expr = constraintExpr_simplify (c->expr); - return c; + return ret; + + } bool resolve (constraint c, constraintList p) @@ -217,125 +199,116 @@ bool resolve (constraint c, constraintList p) { if ( satifies (c, el) ) { - DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); + TPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); return TRUE; } } end_constraintList_elements; - DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) )); + TPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) )); return FALSE; } -constraintTerm constraintTerm_substituteTerm (constraintTerm term, constraintTerm oldterm, constraintExpr replacement) +/*returns true if cosntraint post satifies cosntriant pre */ +bool satifies (constraint pre, constraint post) { - if ( constraintTerm_similar (term, oldterm) ) + if (!constraintExpr_similar (pre->lexpr, post->lexpr) ) { - // do the substitution - term->kind = CONSTRAINTEXPR; - term->value.constrExpr = constraintExpr_copy (replacement); + return FALSE; + } + if (post->expr == NULL) + { + llassert(FALSE); + return FALSE; } - return term; + + return rangeCheck (pre->ar, pre->expr, post->ar, post->expr); } -constraintExpr constraintExpr_substituteTerm (constraintExpr expr, constraintTerm oldterm, constraintExpr replacement) + +bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2) + { - expr->term = constraintTerm_substituteTerm (expr->term, oldterm, replacement); - if (expr->expr != NULL) - expr->expr = constraintExpr_substituteTerm (expr->expr, oldterm, replacement); + TPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) )); + switch (ar1) + { + case GTE: + case GT: + /*irst constraint is > only > => or == cosntraint can satify it */ + if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) ) + { + if (! constraintExpr_canGetValue (expr1) ) + { + TPRINTF( ("Can't Get value")); + return FALSE; + } + if (! constraintExpr_canGetValue (expr2) ) + { + TPRINTF( ("Can't Get value")); + return FALSE; + } + + if (constraintExpr_compare (expr2, expr1) >= 0) + return TRUE; + + } + + return FALSE; + default: + TPRINTF(("case not handled")); + } + return FALSE; +} - return expr; +constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new) +{ + TPRINTF (("Doing replace for lexpr") ); + c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new); + TPRINTF (("Doing replace for expr") ); + c->expr = constraintExpr_searchandreplace (c->expr, old, new); + return c; } -/* returns true if fileloc for term2 is closer to file for term1 than is term3*/ -bool fileloc_closer (constraintTerm term1, constraintTerm term2, constraintTerm term3) +constraint constraint_adjust (constraint substitute, constraint old) { - if ( fileloc_lessthan (term1->loc, term2->loc) ) - { - if (fileloc_lessthan (term2->loc, term3->loc) ) - { - llassert (fileloc_lessthan (term1->loc, term3->loc) ); - return TRUE; - } - else - { - return FALSE; - } - } - - if ( ! (fileloc_lessthan (term1->loc, term2->loc) ) ) - { - if (!fileloc_lessthan (term2->loc, term3->loc) ) - { - llassert (fileloc_lessthan (term3->loc, term1->loc) ); - return TRUE; - } - else - { - return FALSE; - - } - } + fileloc loc1, loc2, loc3; - llassert(FALSE); - return FALSE; -} + loc1 = constraint_getFileloc (old); -constraint constraint_substituteTerm (constraint c, constraint subs) -{ - constraintTerm oldterm; - constraintExpr replacement; - - llassert(subs->lexpr->expr == NULL); - + loc2 = constraintExpr_getFileloc (substitute->lexpr); - oldterm = subs->lexpr->term; - replacement = subs->expr; - - // Chessy hack assumes that subs always has the form g:1 = g:2 + expr + loc3 = constraintExpr_getFileloc (substitute->expr); - /*@i2*/ - - /*find out which value to substitute*/ - TPRINTF((message ("doing substitute for %s and %s", constraint_print (c), constraint_print(subs) ) ) ); - if ( constraintExpr_containsTerm (subs->expr, subs->lexpr->term) ) + if (fileloc_closer (loc1, loc3, loc2)) { - TPRINTF(("doing new stuff")); - if (fileloc_closer (c->lexpr->term, subs->expr->term, subs->lexpr->term) ) - { - // use the other term - constraint new; - new = constraint_copy (subs); - new = solveforOther(new); - oldterm = new->expr->term; - replacement = new->lexpr; - } + constraintExpr temp; + temp = substitute->lexpr; + substitute->lexpr = substitute->expr; + substitute->expr = temp; + substitute = constraint_simplify(substitute); } - c->lexpr = constraintExpr_substituteTerm (c->lexpr, oldterm, replacement); - c->expr = constraintExpr_substituteTerm (c->expr, oldterm, replacement); - return c; + return substitute; + } constraint substitute (constraint c, constraintList p) { constraintList_elements (p, el) { - if ( el->ar == EQ) - if (constraint_hasTerm (c, el->lexpr->term) ) - { - llassert(el->lexpr->expr == NULL); - DPRINTF((message ("doing substitute for %s", constraint_print (c) ) ) ); - - c = constraint_substituteTerm (c, el); - DPRINTF((message ("substituted constraint is now %s", constraint_print (c) ) ) ); - // c->lexpr = constraintExpr_copy (el->expr); - c = constraint_simplify(c); - c = constraint_simplify(c); - c = constraint_simplify(c); - return c; - } + if ( el->ar == EQ) + if (!constraint_conflict (c, el) ) + + { + + constraint temp; + temp = constraint_copy(el); + + temp = constraint_adjust(temp, c); + + c = constraint_searchandreplace (c, el->lexpr, el->expr); + } } end_constraintList_elements; @@ -343,201 +316,64 @@ constraint substitute (constraint c, constraintList p) return c; } - -constraintList reflectChanges (constraintList pre2, constraintList post1) -{ - - constraintList ret; - constraint temp; - ret = constraintList_new(); - constraintList_elements (pre2, el) - { - if (!resolve (el, post1) ) - { - temp = substitute (el, post1); - ret = constraintList_add (ret, temp); - } - } end_constraintList_elements; - return ret; -} - -bool constraintExpr_containsTerm (constraintExpr p, constraintTerm term) +constraint constraint_solve (constraint c) { - TPRINTF(("constraintExpr_containsTerm")); - - while (p != NULL) - { - if (constraintTerm_similar (p->term, term) ) - return TRUE; - - p = p->expr->expr; - } - DPRINTF(( - message ("constraintExpr_hasTerm returned fallse for %s %S", - constraint_print(c), constraintTerm_print(term) - ) - )); - return FALSE; -} - - -/*check if rvalue side has term*/ -bool constraintExpr_hasTerm (constraint c, constraintTerm term) -{ - constraintExpr p; - p = c->expr; - while (p != NULL) - { - if (constraintTerm_same (p->term, term) ) - return TRUE; + TPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) ); + c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr); + TPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) ); - p = p->expr->expr; - } - DPRINTF(( - message ("constraintExpr_hasTerm returned fallse for %s %S", - constraint_print(c), constraintTerm_print(term) - ) - )); - return FALSE; + return c; } -constraintExpr solveEq (constraint c, constraintTerm t) -{ - constraintExpr p; - c = constraint_copy (c); - DPRINTF(("\ndoing solveEq\n")); - if (! constraintTerm_same (c->expr->term, t) ) - { - DPRINTF ( (message ("\n\nconstraintTerms: %s %s not same ", constraintTerm_print(c->expr->term), - constraintTerm_print(t) ) - ) ); - return NULL; - } - - p = c->expr; - while (p->expr != NULL) - { - DPRINTF( (message("\n\nMoving %s", constraintExpr_print (c->expr) ) ) ); - c->lexpr = termMove(c->lexpr, p); - p->expr = p->expr->expr; - } - - return c->lexpr; - -} -constraint updateConstraint (constraint c, constraintList p) +constraint constraint_simplify (constraint c) { - TPRINTF(("start updateConstraints")); - constraintList_elements (p, el) - { - - if (constraintTerm_same(c->lexpr->term, el->lexpr->term) ) - { - TPRINTF(("")); - if ( el->ar == EQ) - { - TPRINTF(("j")); - - if (constraintExpr_hasTerm (el, c->lexpr->term) ) - { - constraintExpr solve; - TPRINTF(("")); - solve = solveEq (el, c->lexpr->term); - if (solve) - { - c->lexpr = constraintExpr_copy (solve); - c = constraint_simplify(c); - return c; - } - } - } - } - } - end_constraintList_elements; - c = constraint_simplify(c); + c->lexpr = constraintExpr_simplify (c->lexpr); + c->expr = constraintExpr_simplify (c->expr); - DPRINTF(("end updateConstraints")); + c = constraint_solve (c); + /* + c->lexpr = constraintExpr_simplify (c->lexpr); + c->expr = constraintExpr_simplify (c->expr); + */ return c; } -constraintList reflectChangesEnsures (constraintList pre2, constraintList post1) -{ - constraintList ret; - constraint temp; - ret = constraintList_new(); - constraintList_elements (pre2, el) - { - if (!resolve (el, post1) ) - { - temp = substitute (el, post1); - if (temp != NULL) - ret = constraintList_add (ret, temp); - } - } end_constraintList_elements; - return ret; -} -void mergeResolve (exprNode parent, exprNode child1, exprNode child2) +/* returns true if fileloc for term1 is closer to file for term2 than term3*/ + +bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3) { - constraintList temp; - DPRINTF( (message ("magically merging constraint into parent:%s for children: %s and %s", exprNode_unparse (parent), exprNode_unparse (child1), exprNode_unparse(child2) ) - ) ); - if (exprNode_isError (child1) || exprNode_isError(child2) ) + if ( fileloc_lessthan (loc1, loc2) ) { - if (exprNode_isError (child1) && !exprNode_isError(child2) ) + if (fileloc_lessthan (loc2, loc3) ) { - parent->requiresConstraints = constraintList_copy (child2->requiresConstraints); - parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints); - DPRINTF((message ("Copied child constraints: pre: %s and post: %s", - constraintList_print( child2->requiresConstraints), - constraintList_print (child2->ensuresConstraints) - ) - )); - return; + llassert (fileloc_lessthan (loc1, loc3) ); + return TRUE; } else { - llassert(exprNode_isError(child2) ); - parent->requiresConstraints = constraintList_new(); - parent->ensuresConstraints = constraintList_new(); - return; + return FALSE; } } - llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) ); - - DPRINTF( (message ("Child constraints are %s %s and %s %s", - constraintList_print (child1->requiresConstraints), - constraintList_print (child1->ensuresConstraints), - constraintList_print (child2->requiresConstraints), - constraintList_print (child2->ensuresConstraints) - ) ) ); - - parent->requiresConstraints = constraintList_new(); - parent->ensuresConstraints = constraintList_new(); - - parent->requiresConstraints = constraintList_copy (child1->requiresConstraints); - - temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints); - parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp); - - - temp = reflectChangesEnsures (child1->ensuresConstraints, child2->ensuresConstraints); - // temp = constraintList_copy (child1->ensuresConstraints); + if ( !fileloc_lessthan (loc1, loc2) ) + { + if (!fileloc_lessthan (loc2, loc3) ) + { + llassert (!fileloc_lessthan (loc1, loc3) ); + return TRUE; + } + else + { + return FALSE; + } + } - - parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints); - parent->ensuresConstraints = constraintList_addList (parent->ensuresConstraints, temp); - - DPRINTF( (message ("Parent constraints are %s and %s ", - constraintList_print (parent->requiresConstraints), - constraintList_print (parent->ensuresConstraints) - ) ) ); - + llassert(FALSE); + return FALSE; } - diff --git a/src/constraintTerm.c b/src/constraintTerm.c index e7f0551..163baf8 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -1,5 +1,5 @@ /* -** constraintTerm.c +** constraintExpr.c */ # include /* for isdigit */ @@ -13,221 +13,67 @@ # include "exprNodeSList.h" # include "exprData.i" -int constraintTerm_getValue (constraintTerm term) -{ - if (term->kind == EXPRNODE) - { - return (multiVal_forceInt (term->value.expr->val) ); - } - if (term->kind == INTLITERAL ) - { - return (term->value.intlit); - } - llassert(FALSE); - return 0; -} +/*@-czechfcns@*/ + +//#include "constraintExpr.h" -/*@out@*/ static constraintTerm new_constraintTermExpr (void) +bool constraintTerm_isIntLiteral (constraintTerm term) { - constraintTerm ret; - ret = dmalloc (sizeof (* ret ) ); - return ret; + llassert(term); + + if (term->kind == INTLITERAL) + return TRUE; + + return FALSE; } constraintTerm constraintTerm_simplify (constraintTerm term) { - if (term->constrType == VALUE) - { - if (term->kind == EXPRNODE) - { - if ( exprNode_knownIntValue (term->value.expr ) ) - { - int temp; - temp = exprNode_getLongValue (term->value.expr); - term->value.intlit = temp; - term->kind = INTLITERAL; - } - - } - - } - - if (term->kind == CONSTRAINTEXPR ) + if (term->kind == EXPRNODE) { - if ( (term->constrType == MAXREAD) || (term->constrType == MAXSET) ) + if ( exprNode_knownIntValue (term->value.expr ) ) { - // ms(var + intlit) = ms (var) - intlit - if (term->value.constrExpr->expr == NULL) - return term; - - if (term->value.constrExpr->expr->term->kind == INTLITERAL) - { - if (term->constrType == MAXREAD) - term->value.constrExpr->term->constrType = MAXREAD; - else if (term->constrType == MAXSET) - term->value.constrExpr->term->constrType = MAXSET; - else - llassert(FALSE); - - term->constrType = VALUE; - - if (term->value.constrExpr->op == PLUS) - term->value.constrExpr->op = MINUS; - else - term->value.constrExpr->op = PLUS; - } - + int temp; + temp = exprNode_getLongValue (term->value.expr); + term->value.intlit = temp; + term->kind = INTLITERAL; } - } - - return term; - } -constraintTerm constraintTerm_copy (constraintTerm term) +fileloc constraintTerm_getFileloc (constraintTerm t) { - constraintTerm ret; - ret = new_constraintTermExpr(); - ret->constrType = term->constrType; - ret->loc = fileloc_copy (term->loc); - ret->value= term->value; - ret->kind = term->kind; - return ret; + return (fileloc_copy (t->loc) ); } -constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e) +constraintTerm constraintTerm_makeExprNode (/*@only@*/ exprNode e) { constraintTerm ret = new_constraintTermExpr(); ret->loc = exprNode_getfileloc(e); ret->value.expr = e; ret->kind = EXPRNODE; + ret = constraintTerm_simplify(ret); return ret; } - -constraintTerm constraintTerm_makeMaxSetexpr (exprNode e) -{ - constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = MAXSET; - return ret; -} - -constraintTerm constraintTerm_makeMinSetexpr (exprNode e) -{ - constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = MINSET; - return ret; -} - -constraintTerm constraintTerm_makeMaxReadexpr (exprNode e) -{ - constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = MAXREAD; - return ret; -} - -constraintTerm constraintTerm_makeMinReadexpr (exprNode e) -{ - constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = MINREAD; - return ret; -} - -constraintTerm constraintTerm_makeValueexpr (exprNode e) +constraintTerm constraintTerm_copy (constraintTerm term) { constraintTerm ret; - ret = exprNode_makeConstraintTerm (e); - ret->constrType = VALUE; - ret = constraintTerm_simplify (ret); - return ret; -} - - -constraintTerm intLit_makeConstraintTerm (int i) -{ - constraintTerm ret = new_constraintTermExpr(); - ret->value.intlit = i; - ret->kind = INTLITERAL; - ret->loc = fileloc_undefined; + ret = new_constraintTermExpr(); + ret->loc = fileloc_copy (term->loc); + ret->value= term->value; + ret->kind = term->kind; return ret; } - -constraintTerm constraintTerm_makeIntLitValue (int i) +constraintTerm constraintTerm_setFileloc (constraintTerm term, fileloc loc) { - constraintTerm ret; - ret = intLit_makeConstraintTerm (i); - ret->constrType = VALUE; - return ret; - + llassert(term); + term->loc = fileloc_copy(loc); + return term; } -/* constraintTerm constraintTerm_makeMinSetexpr (int i) */ -/* { */ -/* constraintTerm ret; */ -/* ret = intLit_makeConstraintTerm (i); */ -/* ret->constrType = MINSET; */ -/* } */ - -/* constraintTerm constraintTerm_makeMaxReadexpr (int i) */ -/* { */ -/* constraintTerm ret; */ -/* ret = intLit_makeConstraintTerm (i); */ -/* ret->constrType = MAXREAD; */ -/* } */ -/* constraintTerm constraintTerm_makeMinReadexpr (int i) */ -/* { */ -/* constraintTerm ret; */ -/* ret = exprNode_makeConstraintTerm (i); */ -/* ret->constrType = MINREAD; */ -/* } */ - - - - -cstring constraintType_print (constraintType constrType) -{ - cstring st = cstring_undefined; - - switch (constrType) - { - case VALUE: - st = cstring_makeLiteral("VALUE"); - break; - case CALLSAFE: - st = cstring_makeLiteral("CALLSAFE"); - break; - case MAXSET: - st = cstring_makeLiteral ("MAXSET"); - break; - case MINSET: - st = cstring_makeLiteral ("MINSET"); - break; - case MAXREAD: - st = cstring_makeLiteral ("MAXREAD"); - break; - case MINREAD: - st = cstring_makeLiteral ("MINREAD"); - break; - case NULLTERMINATED: - st = cstring_makeLiteral ("NULLTERMINATED"); - break; - case UNDEFINED: - st = cstring_makeLiteral (("Unhandled value for constraintType")); - llassert(FALSE); - break; - default: - st = cstring_makeLiteral (("Unhandled value for constraintType")); - llassert(FALSE); - } - return st; -} cstring constraintTerm_print (constraintTerm term) { cstring s; @@ -243,46 +89,50 @@ cstring constraintTerm_print (constraintTerm term) fileloc_unparse (term->loc) ); break; case INTLITERAL: - { s = message (" %d ", term->value.intlit); break; - } + case SREF: s = cstring_makeLiteral("Not Implemented\n"); llassert(FALSE); break; - case CONSTRAINTEXPR: - s = message ("%s ", constraintExpr_print (term->value.constrExpr) ); } - s = message (" %s ( %s ) ", constraintType_print (term->constrType), s); - return s; + return s; } -bool constraintTerm_hasTerm (constraintTerm term, constraintTerm searchTerm) +constraintTerm constraintTerm_makeIntLiteral (int i) +{ + constraintTerm ret = new_constraintTermExpr(); + ret->value.intlit = i; + ret->kind = INTLITERAL; + ret->loc = fileloc_undefined; + return ret; +} + +bool constraintTerm_canGetValue (constraintTerm term) { - if (term->kind == CONSTRAINTEXPR) - return (constraintExpr_includesTerm (term->value.constrExpr, searchTerm) ); + if (term->kind == INTLITERAL) + return TRUE; + else + return FALSE; +} - if ( (term->kind == EXPRNODE) && (searchTerm->kind == EXPRNODE) ) - { - return sRef_same (term->value.expr->sref, searchTerm->value.expr->sref); - } - return FALSE; - +int constraintTerm_getValue (constraintTerm term) +{ + llassert (term->kind == INTLITERAL); + return term->value.intlit; } + + /* same and similar are similar but not the same*/ bool constraintTerm_same (constraintTerm term1, constraintTerm term2) { llassert (term1 !=NULL && term2 !=NULL); - if (term1->constrType != term2->constrType) - { - return FALSE; - } if ( (term1->kind != term2->kind) || (term1->kind != EXPRNODE) ) { return FALSE; @@ -311,10 +161,6 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) { llassert (term1 !=NULL && term2 !=NULL); - // if (term1->constrType != term2->constrType) - // { - // return FALSE; - // } if ( (term1->kind != term2->kind) || (term1->kind != EXPRNODE) ) { return FALSE; @@ -339,3 +185,5 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) } + +