/*
-/*
+*
** constraintResolve.c
*/
+//#define DEBUGPRINT 1
+
# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"
# include "exprChecks.h"
# include "aliasChecks.h"
# include "exprNodeSList.h"
-# include "exprData.i"
+//# include "exprData.i"
#include "constraintExpr.h"
+
+
constraintList reflectChanges (constraintList pre2, constraintList post1);
constraint substitute (constraint c, constraintList p);
constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
constraint constraint_simplify (constraint c);
+constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);
+
+constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
+
+constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
+constraint inequalitySubstitute (constraint c, constraintList p);
+
+/*********************************************/
+
+
+constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
+{
+ constraintList ret;
+ constraintList temp;
+ ret = constraintList_new();
+
+ ret = reflectChangesEnsures (list1, list2);
+ ret = constraintList_fixConflicts (ret, list2);
+ ret = constraintList_subsumeEnsures (ret, list2);
+ list2 = constraintList_subsumeEnsures (list2, ret);
+ temp = constraintList_copy(list2);
+
+ temp = constraintList_addList (temp, ret);
+ return temp;
+ //ret = constraintList_addList (ret, list2);
+ //return ret;
+}
+
+
+/* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */
+/* { */
+
+/* constraintList ret; */
+/* constraintList temp; */
+/* ret = constraintList_new(); */
+
+/* ret = reflectChangesEnsures (list1, list2); */
+/* ret = constraintList_fixConflicts (ret, list2); */
+/* ret = constraintList_subsumeEnsures (ret, list2); */
+/* list2 = constraintList_subsumeEnsures (list2, ret); */
+/* temp = constraintList_copy(list2); */
+
+/* temp = constraintList_addList (temp, ret); */
+/* return temp; */
+/* //ret = constraintList_addList (ret, list2); */
+/* //return ret; */
+/* } */
+
+
+constraintList checkCall (exprNode fcn, exprNodeList arglist)
+{
+ constraintList preconditions;
+ uentry temp;
+ DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
+
+ temp = exprNode_getUentry (fcn);
+
+ preconditions = uentry_getFcnPreconditions (temp);
+
+ if (preconditions)
+ {
+ preconditions = constraintList_copy(preconditions);
+ preconditions = constraintList_doSRefFixBaseParam (preconditions, arglist);
+ }
+ else
+ {
+ preconditions = constraintList_new();
+ }
+
+ return preconditions;
+}
+
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) )
- ) );
- if (exprNode_isError (child1) || exprNode_isError(child2) )
+
+ DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));
+
+ DPRINTF( (message (" children: %s and %s", 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",
+ DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
constraintList_print( child2->requiresConstraints),
constraintList_print (child2->ensuresConstraints)
)
llassert(!exprNode_isError (child1) && ! 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),
temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp);
+ parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
+ child2->ensuresConstraints);
- temp = reflectChangesEnsures (child1->ensuresConstraints, child2->ensuresConstraints);
- // temp = constraintList_copy (child1->ensuresConstraints);
-
- 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 ",
+ DPRINTF( (message ("Parent constraints are %s and %s ",
constraintList_print (parent->requiresConstraints),
constraintList_print (parent->ensuresConstraints)
) ) );
+
+constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
+{
+ constraintList ret;
+ ret = constraintList_new();
+ constraintList_elements (list1, el)
+ {
+
+ DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
+ if (!resolve (el, list2) )
+ {
+ ret = constraintList_add (ret, el);
+ }
+ else
+ {
+ DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
+ }
+ } end_constraintList_elements;
+
+ return ret;
+}
+
+
constraintList reflectChanges (constraintList pre2, constraintList post1)
{
if (!resolve (el, post1) )
{
temp = substitute (el, post1);
- ret = constraintList_add (ret, temp);
+ if (!resolve (temp, post1) )
+ {
+ // try inequality substitution
+ constraint temp2;
+
+ // the inequality substitution may cause us to lose information
+ //so we don't want to store the result but we do it anyway
+ temp2 = constraint_copy (temp);
+ temp2 = inequalitySubstitute (temp, post1);
+ if (!resolve (temp2, post1) )
+ ret = constraintList_add (ret, temp2);
+ }
}
} end_constraintList_elements;
if (!resolve (el, post1) )
{
temp = substitute (el, post1);
- if (temp != NULL)
+ llassert (temp != NULL);
+
+ if (!resolve (temp, post1) )
ret = constraintList_add (ret, temp);
}
+ else
+ {
+ DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
+ }
} end_constraintList_elements;
return ret;
if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
{
- if (c1->ar == c2->ar)
- {
- TPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
- return TRUE;
- }
+ if (c1->ar == EQ)
+ if (c1->ar == c2->ar)
+ {
+ DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
+ return TRUE;
+ }
}
- TPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
+ DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
return FALSE;
{
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;
}
return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
}
+bool arithType_canResolve (arithType ar1, arithType ar2)
+{
+ switch (ar1)
+ {
+ case GTE:
+ case GT:
+ if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
+ {
+ return TRUE;
+ }
+ break;
+
+ case EQ:
+ if (ar2 == EQ)
+ return TRUE;
+ break;
+
+ case LT:
+ case LTE:
+ // llassert(FALSE);
+ if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
+ return TRUE;
+ }
+ return FALSE;
+}
bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)
{
- TPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
+ DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
+
+ if (! arithType_canResolve (ar1, ar2) )
+ return FALSE;
+
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;
+ if (! (constraintExpr_canGetValue (expr1) &&
+ constraintExpr_canGetValue (expr2) ) )
+ {
+ DPRINTF( ("Can't Get value"));
+ return FALSE;
+ }
+
+ if (constraintExpr_compare (expr2, expr1) >= 0)
+ return TRUE;
+
+ return FALSE;
+ case EQ:
+ if (constraintExpr_similar (expr1, expr2) )
+ return TRUE;
+
+ return FALSE;
+
default:
- TPRINTF(("case not handled"));
+ DPRINTF(("case not handled"));
}
return FALSE;
}
+
constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new)
{
- TPRINTF (("Doing replace for lexpr") );
+ DPRINTF (("Doing replace for lexpr") );
c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
- TPRINTF (("Doing replace for expr") );
+ DPRINTF (("Doing replace for expr") );
c->expr = constraintExpr_searchandreplace (c->expr, old, new);
return c;
}
+bool constraint_search (constraint c, constraintExpr old)
+{
+ bool ret;
+ ret = FALSE;
+
+ ret = constraintExpr_search (c->lexpr, old);
+ ret = ret || constraintExpr_search (c->expr, old);
+ return ret;
+}
+//adjust file locs and stuff
constraint constraint_adjust (constraint substitute, constraint old)
{
fileloc loc1, loc2, loc3;
+ DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
+ constraint_print(old))
+ ));
+
loc1 = constraint_getFileloc (old);
loc2 = constraintExpr_getFileloc (substitute->lexpr);
loc3 = constraintExpr_getFileloc (substitute->expr);
- if (fileloc_closer (loc1, loc3, loc2))
+
+ // special case of an equality that "contains itself"
+ if (constraintExpr_search (substitute->expr, substitute->lexpr) )
+ if (fileloc_closer (loc1, loc3, loc2))
{
constraintExpr temp;
+ DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
+ ));
temp = substitute->lexpr;
substitute->lexpr = substitute->expr;
substitute->expr = temp;
}
+constraint inequalitySubstitute (constraint c, constraintList p)
+{
+ if (c->ar != GTE)
+ return c;
+
+ constraintList_elements (p, el)
+ {
+ if ( el->ar == LT)
+ // if (!constraint_conflict (c, el) )
+ {
+ constraint temp;
+ temp = constraint_copy(el);
+
+ // temp = constraint_adjust(temp, c);
+
+ if (constraintExpr_same (el->lexpr, c->expr) )
+ {
+ DPRINTF((message ("Replacing %s in %s with %s",
+ constraintExpr_print (c->expr),
+ constraint_print (c),
+ constraintExpr_print (el->expr) )
+ ));
+ c->expr = constraintExpr_copy (el->expr);
+ }
+
+ }
+ }
+ end_constraintList_elements;
+
+ c = constraint_simplify(c);
+ return c;
+}
+
constraint substitute (constraint c, constraintList p)
{
constraintList_elements (p, el)
if (!constraint_conflict (c, el) )
{
-
constraint temp;
temp = constraint_copy(el);
temp = constraint_adjust(temp, c);
+
+ DPRINTF((message ("Substituting %s for %s",
+ constraint_print (temp), constraint_print (c)
+ ) ) );
+
- c = constraint_searchandreplace (c, el->lexpr, el->expr);
+ c = constraint_searchandreplace (c, temp->lexpr, temp->expr);
}
}
end_constraintList_elements;
constraint constraint_solve (constraint c)
{
- TPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
+ DPRINTF( (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) ) ) );
+ DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
return c;
}
c->expr = constraintExpr_simplify (c->expr);
c = constraint_solve (c);
- /*
+
c->lexpr = constraintExpr_simplify (c->lexpr);
c->expr = constraintExpr_simplify (c->expr);
- */
+
return c;
}
return FALSE;
}
+
andersk / splint.git / blobdiff