static constraint inequalitySubstituteUnsound (/*@returned@*/ constraint p_c, constraintList p_p);
+static constraint inequalitySubstituteStrong (/*@returned@*/ constraint p_c, constraintList p_p);
+
static constraint constraint_searchandreplace (/*@returned@*/ constraint p_c, constraintExpr p_old, constraintExpr p_newExpr);
}
+
/* tries to resolve constraints in list pre2 using post1 */
-/*@only@*/ constraintList constraintList_reflectChanges(/*@observer@*/ constraintList pre2, /*@observer@*/ constraintList post1)
+
+static /*@only@*/ constraintList reflectChangesNoOr (/*@observer@*/ /*@temp@*/ constraintList pre2, /*@observer@*/ /*@temp@*/ constraintList post1)
{
constraintList ret;
constraint temp;
constraint temp2;
+ llassert (! context_getFlag (FLG_ORCONSTRAINT) );
+
ret = constraintList_makeNew();
DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
return ret;
}
+/* tries to resolve constraints in list pre2 using post1 */
+/*@only@*/ constraintList constraintList_reflectChanges(/*@observer@*/ constraintList pre2, /*@observer@*/ constraintList post1)
+{
+ constraintList temp;
+
+ if ( context_getFlag (FLG_ORCONSTRAINT) )
+
+ temp = constraintList_reflectChangesOr (pre2, post1);
+ else
+ temp = reflectChangesNoOr(pre2, post1);
+
+ return temp;
+}
static constraint constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint orConstr)
{
{
c = c->or;
}
+
c->or = constraint_copy(orConstr);
DPRINTF((message("constraint_addor: returning %s",constraint_printOr(orig) ) ));
{
constraint temp;
+ int numberOr;
+
+ numberOr = 0;
DPRINTF(( message("resolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(list) ) ));
temp = c;
if (constraintList_resolve (temp, list) )
return TRUE;
temp = temp->or;
+ numberOr++;
+ llassert(numberOr <= 10);
}
while (constraint_isDefined(temp));
static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList post1, bool * resolved)
{
constraint temp;
+
+ llassert(constraint_isUndefined (c->or ) );
- if (!resolveOr (c, post1) )
+ if (!resolveOr (c, post1) )
+ {
+
+ temp = constraint_substitute (c, post1);
+
+ if (!resolveOr (temp, post1) )
{
-
- temp = constraint_substitute (c, post1);
+ // try inequality substitution
+ constraint temp2;
- if (!resolveOr (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
+ //so we don't want to store the result but we do anyway
temp2 = constraint_copy (c);
// if (context_getFlag (FLG_ORCONSTRAINT) )
- temp2 = inequalitySubstitute (temp2, post1);
+ temp2 = inequalitySubstitute (temp2, post1);
if (!resolveOr (temp2, post1) )
{
- temp2 = inequalitySubstituteUnsound (temp2, post1);
- if (!resolveOr (temp2, post1) )
+ constraint temp3;
+ temp3 = constraint_copy(temp2);
+
+ temp3 = inequalitySubstituteStrong (temp3, post1);
+ if (!resolveOr (temp3, post1) )
{
- if (!constraint_same (temp, temp2) )
- temp = constraint_addOr (temp, temp2);
- *resolved = FALSE;
-
+ temp2 = inequalitySubstituteUnsound (temp2, post1);
+ if (!resolveOr (temp2, post1) )
+ {
+ if (!constraint_same (temp, temp2) )
+ temp = constraint_addOr (temp, temp2);
+
+ if (!constraint_same (temp, temp3) && !constraint_same (temp3, temp2) )
+ temp = constraint_addOr (temp, temp3);
+
+ *resolved = FALSE;
+
+ constraint_free(temp2);
+ constraint_free(temp3);
+ constraint_free(c);
+
+ return temp;
+ }
constraint_free(temp2);
- constraint_free(c);
-
- return temp;
+ constraint_free(temp3);
+ }
+ else
+ {
+ constraint_free(temp2);
+ constraint_free(temp3);
}
}
-
- constraint_free(temp2);
+ else
+ {
+ constraint_free(temp2);
+ }
+
}
constraint_free(temp);
}
-
constraint_free(c);
*resolved = TRUE;
return NULL;
-
-
}
-static /*@only@*/ constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * resolved)
+static /*@only@*/ constraint doResolveOr (/*@observer@*/ /*@temp@*/ constraint c, constraintList post1, /*@out@*/bool * resolved)
{
constraint ret;
constraint next;
constraint curr;
+
+
+ DPRINTF(( message("doResolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(post1) ) ));
+
+
*resolved = FALSE;
+
+
ret = constraint_copy(c);
+
+ if (constraintList_isEmpty(post1) )
+ {
+ return ret;
+ }
+
next = ret->or;
ret->or = NULL;
{
if (next != NULL)
constraint_free(next);
-
+
/*we don't need to free ret when resolved is false because ret is null*/
llassert(ret == NULL);
- return NULL;
+ return NULL;
}
-
+
while (next != NULL)
{
curr = next;
curr->or = NULL;
curr = doResolve (curr, post1, resolved);
+
if (*resolved)
{
/* curr is null so we don't try to free it*/
ret = constraint_addOr (ret, curr);
constraint_free(curr);
}
-
return ret;
}
-
-
-
-
/* tries to resolve constraints in list pr2 using post1 */
/*@only@*/ constraintList constraintList_reflectChangesOr (constraintList pre2, constraintList post1)
{
}
else
{
- /*we don't need to free ret when resolved is false because ret is null*/
+ /* we don't need to free temp when
+ resolved is false because temp is null */
llassert(temp == NULL);
}
} end_constraintList_elements;
- DPRINTF((message ("constraintList_reflectChangesOr: returning %s", constraintList_print(ret) ) ) );
+ DPRINTF((message ("constraintList_reflectChangesOr: returning %s", constraintList_print(ret) ) ) );
return ret;
}
+
static /*@only@*/ constraintList reflectChangesEnsures (/*@observer@*/ constraintList pre2, constraintList post1)
{
constraintList ret;
}
}
+ // This is a slight kludg to prevent circular constraints like
+ // strlen(str) == maxRead(s) + strlen(str);
+
+ /*@i324234*/ //clean this up
+
+ if (c1->ar == EQ)
+ if (c1->ar == c2->ar)
+ {
+ if (constraintExpr_search (c1->lexpr, c2->expr) )
+ if (constraintExpr_isTerm(c1->lexpr) )
+ {
+ constraintTerm term;
+
+ term = constraintExpr_getTerm(c1->lexpr);
+
+ if (constraintTerm_isExprNode(term) )
+ {
+ DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
+ return TRUE;
+ }
+ }
+ }
+
+ if (constraint_tooDeep(c1) || constraint_tooDeep(c2) )
+ {
+ DPRINTF ( (message ("%s conflicts with %s (constraint is too deep", constraint_print (c1), constraint_print(c2) ) ) );
+ return TRUE;
+ }
+
DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
return FALSE;
bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c)
{
constraintExpr l, r;
- bool /*@unused@*/ lHasConstant, rHasConstant;
- int /*@unused@*/ lConstant, rConstant;
+ bool rHasConstant;
+ int rConstant;
l = c->lexpr;
r = c->expr;
Warning this is sound but throws out information
*/
+
constraint inequalitySubstitute (/*@returned@*/ constraint c, constraintList p)
{
if (c->ar != GTE)
constraintList_elements (p, el)
{
- if ( el->ar == LT)
+ if ( (el->ar == LT ) )
// if (!constraint_conflict (c, el) )
{
//constraint temp;
if (constraintExpr_same (el->expr, c->expr) )
{
- DPRINTF((message ("inequalitySubstitute Replacing %s in %s with %s",
+ DPRINTF((message ("inequalitySubstitute Replacing %q in %q with %q",
constraintExpr_print (c->expr),
constraint_print (c),
constraintExpr_print (el->expr) )
temp2 = constraintExpr_copy (el->lexpr);
constraintExpr_free(c->expr);
c->expr = constraintExpr_makeIncConstraintExpr (temp2);
+
}
}
return c;
}
+
+/* drl7x 7/26/001
+
+ THis function is like inequalitySubstitute but it adds the rule
+ added the rules x >= y && y <= b ===> x >= b
+ x >= y && y < b ===> x >= b + 1
+
+ This is sound but sonce it throws out additional information it should only one used
+ if we're oring constraints.
+ */
+
+static constraint inequalitySubstituteStrong (/*@returned@*/ constraint c, constraintList p)
+{
+ DPRINTF (( message ("inequalitySubstituteStrong examining substituting for %q", constraint_print(c) ) ));
+
+ if (c->ar != GTE)
+ return c;
+
+ DPRINTF (( message ("inequalitySubstituteStrong examining substituting for %q with %q",
+ constraint_print(c), constraintList_print(p) ) ));
+ constraintList_elements (p, el)
+ {
+ DPRINTF (( message ("inequalitySubstituteStrong examining substituting %s on %s", constraint_print(el), constraint_print(c) ) ));
+
+ if ( (el->ar == LT ) || (el->ar == LTE ) )
+ // if (!constraint_conflict (c, el) )
+ {
+ //constraint temp;
+ constraintExpr temp2;
+
+ /*@i22*/
+
+ //temp = constraint_copy(el);
+
+ // temp = constraint_adjust(temp, c);
+
+ if (constraintExpr_same (el->lexpr, c->expr) )
+ {
+ DPRINTF((message ("inequalitySubstitute Replacing %s in %s with %s",
+ constraintExpr_print (c->expr),
+ constraint_print (c),
+ constraintExpr_print (el->expr) )
+ ));
+ temp2 = constraintExpr_copy (el->expr);
+ constraintExpr_free(c->expr);
+ if ( (el->ar == LTE ) )
+ {
+ c->expr = temp2;
+ }
+ else
+ {
+ c->expr = constraintExpr_makeIncConstraintExpr (temp2);
+ }
+ }
+
+ }
+ }
+ end_constraintList_elements;
+
+ c = constraint_simplify(c);
+ return c;
+}
+
+
/* This function performs substitutions based on the rule:
for a constraint of the form expr1 >= expr2; a < b =>
a = b -1 for all a in expr1. This will work in most cases.
constraint constraint_simplify ( /*@returned@*/ constraint c)
{
+
+ DPRINTF(( message("constraint_simplify on %q ", constraint_print(c) ) ));
+
+ if (constraint_tooDeep(c))
+ {
+ DPRINTF(( message("constraint_simplify: constraint to complex aborting %q ", constraint_print(c) ) ));
+ return c;
+
+ }
+
c->lexpr = constraintExpr_simplify (c->lexpr);
c->expr = constraintExpr_simplify (c->expr);
/*I don't think this will be an infinate loop*/
c = constraint_simplify(c);
}
+
+ DPRINTF(( message("constraint_simplify returning %q ", constraint_print(c) ) ));
+
return c;
}
andersk / splint.git / blobdiff