From bf92e32cf4958be7a9035826b51d0ea8bba57ded Mon Sep 17 00:00:00 2001 From: drl7x Date: Wed, 27 Sep 2000 21:59:15 +0000 Subject: [PATCH] *** empty log message *** --- src/Headers/constraint.h | 28 +++++------ src/Headers/forwardTypes.h | 3 ++ src/constraint.c | 64 ++++++++++++++++++++++--- src/constraintGeneration.c | 26 ++++++----- src/constraintList.c | 45 +++++++++++++++++- src/constraintResolve.c | 96 ++++++++++++++++++++++++++++---------- src/constraintTerm.c | 86 ++++++++++++++++++++++++++++++++-- 7 files changed, 289 insertions(+), 59 deletions(-) diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 1878521..12a52a6 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -1,10 +1,20 @@ typedef union constraintTermValue_ { + constraintExpr constrExpr; exprNode expr; sRef sref; int intlit; } constraintTermValue; + +typedef enum +{ + EXPRNODE, SREF, + CONSTRAINTEXPR, + INTLITERAL +} constraintTermType; + + typedef enum { LT, LTE, GT, GTE, EQ, NONNEGATIVE, POSITIVE @@ -13,10 +23,10 @@ arithType; typedef enum { - BUFFSIZE, STRINGLEN, VALUE, CALLSAFE, + //BUFFSIZE, STRINGLEN, + VALUE, CALLSAFE, MAXSET, MINSET, MAXREAD, MINREAD, NULLTERMINATED, - INCOP, UNDEFINED } constraintType; @@ -29,13 +39,6 @@ typedef enum constraintExprOp; -typedef enum -{ -EXPRNODE, SREF, -INTLITERAL -} constraintTermType; - - struct _constraintTerm { constraintType constrType; fileloc loc; @@ -53,19 +56,18 @@ struct constraintExpr_ { }; # define constraintExpr_undefined ((constraintExpr)NULL) -typedef struct constraintExpr_ * constraintExpr; -abst_typedef struct constr_ * constr; + +//abst_typedef struct constr_ * constr; struct _constraint { + constraint orig; constraintExpr lexpr; arithType ar; constraintExpr expr; bool post; } ; -#define max_constraints 100 - //constraint constraint_create (exprNode e1, exprNode e2, arithType restriction, constraintType kind); constraint constraint_createReadSafe (exprNode p_e1, exprNode p_e2); diff --git a/src/Headers/forwardTypes.h b/src/Headers/forwardTypes.h index 4d13347..5d575f5 100644 --- a/src/Headers/forwardTypes.h +++ b/src/Headers/forwardTypes.h @@ -23,6 +23,9 @@ abst_typedef /*@null@*/ struct _environmentTable *environmentTable; abst_typedef /*@null@*/ struct _constraint *constraint; +/* DRL modified 9 26 00 */ + +abst_typedef struct constraintExpr_ * constraintExpr; /*@-cppnames@*/ typedef int bool; diff --git a/src/constraint.c b/src/constraint.c index f609083..4b7b5c2 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -26,10 +26,15 @@ constraint constraint_copy (constraint c) { constraint ret; ret = constraint_makeNew(); - ret->lexpr = c->lexpr; + ret->lexpr = constraintExpr_copy (c->lexpr); ret->ar = c->ar; - ret->expr = c->expr; + ret->expr = constraintExpr_copy (c->expr); ret->post = c->post; + /*@i33 fix this*/ + if (c->orig != NULL) + ret->orig = constraint_copy (c->orig); + else + ret->orig = NULL; return ret; } @@ -49,6 +54,7 @@ bool constraint_resolve (/*@unused@*/ constraint c) ret->expr = NULL; ret->ar = LT; ret->post = FALSE; + ret->orig = NULL; /*@i23*/return ret; } /*@-czechfcns@*/ @@ -76,7 +82,7 @@ constraintExpr constraintExpr_copy (constraintExpr expr) { ret->expr = NULL; } - + return ret; } constraintExpr constraintExpr_makeMaxSetExpr (exprNode expr) @@ -227,8 +233,7 @@ constraintExpr makeMaxSetPostOpInc (exprNode e) { constraintExpr ret; ret = constraintExpr_makeValueExpr (e); - ret->term = constraintTerm_makeMaxSetexpr (e); - ret->op = MINUS; + ret->op = PLUS; ret->expr = makeConstraintExprIntlit (1); return ret; } @@ -239,7 +244,7 @@ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc seq //constraintTerm term; exprNode t2; e = exprNode_fakeCopy(e); - ret->lexpr = constraintExpr_makeMaxSetExpr(e); + ret->lexpr = constraintExpr_makeValueExpr (e); ret->ar = EQ; ret->post = TRUE; ret->expr = makeMaxSetPostOpInc(e); @@ -334,6 +339,22 @@ cstring constraintExpr_print (constraintExpr ex) } +cstring constraint_printDetailed (constraint c) +{ + cstring st = cstring_undefined; + + if (!c->post) + { + + st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(c->orig) ); + } + else + { + st = message ("Function Post condition:\nBased on the constraint %s this function appears to have the post condition %s", constraint_print (c), constraint_print(c->orig) ); + } + return st; +} + cstring constraint_print (constraint c) { cstring st = cstring_undefined; @@ -356,6 +377,37 @@ cstring constraint_print (constraint c) return st; } +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; +} + +bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term) +{ + if (constraintTerm_hasTerm (expr->term, term) ) + return TRUE; + + if ( (expr->expr) != NULL) + { + return ( constraintExpr_includesTerm (expr->expr, term) ); + } + return FALSE; + +} + +constraint constraint_preserveOrig (constraint c) +{ + c->orig = constraint_copy (c); + return c; +} /*@=fcnuse*/ /*@=assignexpose*/ /*@=czechfcns@*/ diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index e7f4f7b..ed0bbd7 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -94,13 +94,14 @@ void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e) if (exprNode_isMultiStatement ( e) ) { - return exprNode_multiStatement(e); + exprNode_multiStatement(e); } else { llassert(FALSE); } - + printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) ); + printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); return FALSE; } @@ -178,9 +179,9 @@ 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 ("%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; @@ -217,7 +218,7 @@ bool exprNode_stmtList (exprNode e) exprNode_stmt (stmt2); mergeResolve (e, stmt1, stmt2 ); - TPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", + DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_print(e->requiresConstraints), constraintList_print(e->ensuresConstraints) ) ) ); return TRUE; @@ -356,8 +357,8 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel e->requiresConstraints = constraintList_add(e->requiresConstraints, cons); cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint); e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); - cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint); - e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); + // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint); + // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons); exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint); exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint); @@ -393,7 +394,7 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel case XPR_PARENS: exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint); // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined); - break; + break; case XPR_ASSIGN: exprNode_exprTraverse (exprData_getOpA (data), TRUE, definaterv, sequencePoint ); lltok_unparse (exprData_getOpTok (data)); @@ -455,18 +456,21 @@ bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, filel lltok_unparse (exprData_getUopTok (data)); if (lltok_isInc_Op (exprData_getUopTok (data) ) ) { - TPRINTF(("doing ++")); + DPRINTF(("doing ++")); t1 = exprData_getUopNode (data); cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint ); e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); - cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint ); - e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); + // cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint ); + //e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons); } break; default: handledExprNode = FALSE; } + e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints); + e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints); + return handledExprNode; } diff --git a/src/constraintList.c b/src/constraintList.c index 88488b6..21bd987 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -120,6 +120,41 @@ constraintList_print (constraintList s) return st; } + +cstring +constraintList_printDetailed (constraintList s) +{ + int i; + cstring st = cstring_undefined; + bool first = TRUE; + + if (s->nelements == 0) + st = cstring_makeLiteral(""); + + for (i = 0; i < s->nelements; i++) + { + cstring type = cstring_undefined; + constraint current = s->elements[i]; + + if (current != NULL) + { + cstring temp1 = constraint_printDetailed (current); + type = message ("%s %s\n", type, temp1 ); + } + + if (first) + { + st = type; + first = FALSE; + } + else + { + st = message ("%s %s", st, type); + } + } + return st; +} + void constraintList_free (constraintList s) { @@ -146,4 +181,12 @@ constraintList_copy (constraintList s) return ret; } - +constraintList constraintList_preserveOrig (constraintList c) +{ + constraintList_elements (c, el); + { + el = constraint_preserveOrig (el); + } + end_constraintList_elements; + return c; +} diff --git a/src/constraintResolve.c b/src/constraintResolve.c index e85e4d1..24d43cf 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -89,11 +89,10 @@ bool satifies (constraint pre, constraint post) { return FALSE; } - if (post->expr->expr == NULL) + if (post->expr == NULL) return FALSE; + return rangeCheck (pre->ar, pre->expr, post->ar, post->expr); - - return TRUE; } constraintExpr constraintExpr_simplify (constraintExpr expr) @@ -101,18 +100,30 @@ constraintExpr constraintExpr_simplify (constraintExpr expr) expr->term = constraintTerm_simplify (expr->term); if (expr->expr == NULL) - return expr; + { + if ( (expr->term->kind == CONSTRAINTEXPR) && (expr->term->constrType == VALUE) ) + { + expr->op = expr->term->value.constrExpr->op; + expr->expr = expr->term->value.constrExpr->expr; + expr->term = expr->term->value.constrExpr->term; + } + + return expr; + } expr->expr = constraintExpr_simplify (expr->expr); - if ( (expr->term->constrType == INTLITERAL) && (expr->expr->term->constrType == INTLITERAL) ) + + + + if ( (expr->term->kind == INTLITERAL) && (expr->expr->term->kind == INTLITERAL) ) { - TPRINTF( ("EVENTUAL IMPLEMENTATION OF LITERAL MERGE " )); + DPRINTF( ("INTLITERAL MERGE " )); - TPRINTF ( (message ("Expression is %s ", constraintExpr_print (expr) ) ) ); + DPRINTF ( (message ("Expression is %s ", constraintExpr_print (expr) ) ) ); if (expr->op == PLUS ) { - TPRINTF( (message ("Adding %d and %d ", expr->term->value.intlit, + DPRINTF( (message ("Adding %d and %d ", expr->term->value.intlit, expr->expr->term->value.intlit) ) ); expr->term->value.intlit += expr->expr->term->value.intlit; } @@ -124,6 +135,7 @@ constraintExpr constraintExpr_simplify (constraintExpr expr) expr->expr = expr->expr->expr; } + return expr; } @@ -165,7 +177,7 @@ constraint solveforterm (constraint c) p = c->lexpr; while (p->expr != NULL) { - TPRINTF( (message("Moving %s", constraintExpr_print (c->expr) ) ) ); + DPRINTF( (message("Moving %s", constraintExpr_print (c->expr) ) ) ); c->expr = termMove(c->expr, p); p->op = p->expr->op; #warning memleak @@ -189,24 +201,57 @@ bool resolve (constraint c, constraintList p) { if ( satifies (c, el) ) { - TPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); + DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); return TRUE; } } end_constraintList_elements; - TPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) )); + DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) )); return FALSE; } + +constraintTerm constraintTerm_substituteTerm (constraintTerm term, constraintTerm oldterm, constraintExpr replacement) +{ + if ( constraintTerm_similar (term, oldterm) ) + { + // do the substitution + term->kind = CONSTRAINTEXPR; + term->value.constrExpr = constraintExpr_copy (replacement); + } + return term; +} + +constraintExpr constraintExpr_substituteTerm (constraintExpr expr, constraintTerm oldterm, constraintExpr replacement) +{ + expr->term = constraintTerm_substituteTerm (expr->term, oldterm, replacement); + if (expr->expr != NULL) + expr->expr = constraintExpr_substituteTerm (expr->expr, oldterm, replacement); + + return expr; +} +constraint constraint_substituteTerm (constraint c, constraintTerm oldterm, constraintExpr replacement) +{ + c->lexpr = constraintExpr_substituteTerm (c->lexpr, oldterm, replacement); + c->expr = constraintExpr_substituteTerm (c->expr, oldterm, replacement); + return c; +} + constraint substitute (constraint c, constraintList p) { constraintList_elements (p, el) { - if (constraintTerm_same(c->lexpr->term, el->lexpr->term) ) - { - if ( el->ar == EQ) + if ( el->ar == EQ) + if (constraint_hasTerm (c, el->lexpr->term) ) + // constraintTerm_same(c->lexpr->term, el->lexpr->term) ) + { { - c->lexpr = constraintExpr_copy (el->expr); + DPRINTF((message ("doing substitute for %s", constraint_print (c) ) ) ); + c = constraint_substituteTerm (c, el->lexpr->term, el->expr); + 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; } @@ -250,7 +295,7 @@ bool constraintExpr_hasTerm (constraint c, constraintTerm term) p = p->expr->expr; } - TPRINTF(( + DPRINTF(( message ("constraintExpr_hasTerm returned fallse for %s %S", constraint_print(c), constraintTerm_print(term) ) @@ -262,10 +307,10 @@ constraintExpr solveEq (constraint c, constraintTerm t) { constraintExpr p; c = constraint_copy (c); - TPRINTF(("\ndoing solveEq\n")); + DPRINTF(("\ndoing solveEq\n")); if (! constraintTerm_same (c->expr->term, t) ) { - TPRINTF ( (message ("\n\nconstraintTerms: %s %s not same ", constraintTerm_print(c->expr->term), + DPRINTF ( (message ("\n\nconstraintTerms: %s %s not same ", constraintTerm_print(c->expr->term), constraintTerm_print(t) ) ) ); return NULL; @@ -274,7 +319,7 @@ constraintExpr solveEq (constraint c, constraintTerm t) p = c->expr; while (p->expr != NULL) { - TPRINTF( (message("\n\nMoving %s", constraintExpr_print (c->expr) ) ) ); + DPRINTF( (message("\n\nMoving %s", constraintExpr_print (c->expr) ) ) ); c->lexpr = termMove(c->lexpr, p); p->expr = p->expr->expr; } @@ -285,13 +330,13 @@ constraintExpr solveEq (constraint c, constraintTerm t) constraint updateConstraint (constraint c, constraintList p) { - TPRINTF(("start updateConstraints")); + DPRINTF(("start updateConstraints")); constraintList_elements (p, el) { if (constraintTerm_same(c->lexpr->term, el->lexpr->term) ) { - TPRINTF(("")); + DPRINTF(("")); if ( el->ar == EQ) { TPRINTF(("")); @@ -314,7 +359,7 @@ constraint updateConstraint (constraint c, constraintList p) end_constraintList_elements; c = constraint_simplify(c); - TPRINTF(("end updateConstraints")); + DPRINTF(("end updateConstraints")); return c; } @@ -340,7 +385,7 @@ constraintList reflectChangesEnsures (constraintList pre2, constraintList post1) void mergeResolve (exprNode parent, exprNode child1, exprNode child2) { constraintList temp; - TPRINTF( (message ("magically merging constraint into parent:%s for children: %s and %s", exprNode_unparse (parent), exprNode_unparse (child1), exprNode_unparse(child2) ) + DPRINTF( (message ("magically merging constraint into parent:%s for children: %s and %s", exprNode_unparse (parent), exprNode_unparse (child1), exprNode_unparse(child2) ) ) ); llassert (!exprNode_isError (child1) || !exprNode_isError(child2) ); if (exprNode_isError (child1) ) @@ -357,7 +402,7 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2) llassert(!exprNode_isError(child2) ); - TPRINTF( (message ("Child constraints are %s %s and %s %s", + DPRINTF( (message ("Child constraints are %s %s and %s %s", constraintList_print (child1->requiresConstraints), constraintList_print (child1->ensuresConstraints), constraintList_print (child2->requiresConstraints), @@ -380,10 +425,11 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2) parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints); parent->ensuresConstraints = constraintList_addList (parent->ensuresConstraints, temp); - TPRINTF( (message ("Parent constraints are %s and %s ", + DPRINTF( (message ("Parent constraints are %s and %s ", constraintList_print (parent->requiresConstraints), constraintList_print (parent->ensuresConstraints) ) ) ); } + diff --git a/src/constraintTerm.c b/src/constraintTerm.c index 8f2418e..471dae7 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -51,7 +51,39 @@ constraintTerm constraintTerm_simplify (constraintTerm term) } } + + if (term->kind == CONSTRAINTEXPR ) + { + if ( (term->constrType == MAXREAD) || (term->constrType == MAXSET) ) + { + // 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; + } + + } + + } + + return term; + } constraintTerm constraintTerm_copy (constraintTerm term) @@ -219,13 +251,29 @@ cstring constraintTerm_print (constraintTerm term) 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); + s = message (" %s ( %s ) ", constraintType_print (term->constrType), s); return s; } +bool constraintTerm_hasTerm (constraintTerm term, constraintTerm searchTerm) +{ + if (term->kind == CONSTRAINTEXPR) + return (constraintExpr_includesTerm (term->value.constrExpr, searchTerm) ); + + if ( (term->kind == EXPRNODE) && (searchTerm->kind == EXPRNODE) ) + { + return sRef_same (term->value.expr->sref, searchTerm->value.expr->sref); + } + return FALSE; + +} + +/* same and similar are similar but not the same*/ bool constraintTerm_same (constraintTerm term1, constraintTerm term2) { @@ -248,12 +296,44 @@ bool constraintTerm_same (constraintTerm term1, constraintTerm term2) if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) ) { - TPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + return TRUE; + } + else + { + DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + return FALSE; + } + +} + +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; + } + + DPRINTF ( (message + ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2) + ) + ) + ); + + if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) ) + { + DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); return TRUE; } else { - TPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); return FALSE; } -- 2.45.2