2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
4 ** Massachusetts Institute of Technology
6 ** This program is free software; you can redistribute it and/or modify it
7 ** under the terms of the GNU General Public License as published by the
8 ** Free Software Foundation; either version 2 of the License, or (at your
9 ** option) any later version.
11 ** This program is distributed in the hope that it will be useful, but
12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14 ** General Public License for more details.
16 ** The GNU General Public License is available from http://www.gnu.org/ or
17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18 ** MA 02111-1307, USA.
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
27 ** constraintResolve.c
30 # include "splintMacros.nf"
33 /*@access constraint, exprNode @*/ /*!!! NO! Don't do this so recklessly - design your code more carefully so you don't need to! */
35 static constraint
inequalitySubstitute (/*@returned@*/ constraint p_c
, constraintList p_p
);
36 static bool rangeCheck (arithType p_ar1
, /*@observer@*/ constraintExpr p_expr1
, arithType p_ar2
, /*@observer@*/ constraintExpr p_expr2
);
38 static constraint
inequalitySubstituteUnsound (/*@returned@*/ constraint p_c
, constraintList p_p
);
39 static constraint
inequalitySubstituteStrong (/*@returned@*/ constraint p_c
, constraintList p_p
);
41 static constraint
constraint_searchandreplace (/*@returned@*/ constraint p_c
, constraintExpr p_old
, constraintExpr p_newExpr
);
43 static constraint
constraint_addOr (/*@returned@*/ constraint p_orig
, /*@observer@*/ constraint p_orConstr
);
45 static bool resolveOr (/*@temp@*/constraint p_c
, /*@observer@*/ /*@temp@*/ constraintList p_list
);
47 static /*@only@*/ constraintList
reflectChangesEnsuresFree1 (/*@only@*/ constraintList p_pre2
, constraintList p_post1
);
49 static /*@only@*/ constraintList
constraintList_subsumeEnsures (constraintList p_list1
, constraintList p_list2
);
50 static /*@only@*/ constraintList
constraintList_fixConflicts (constraintList p_list1
, constraintList p_list2
);
52 static bool fileloc_closer (/*@observer@*/ fileloc p_loc1
,
53 /*@observer@*/ fileloc p_loc2
,
54 /*@observer@*/ fileloc p_loc3
) /*@*/;
57 /*@only@*/ constraintList
constraintList_mergeEnsuresFreeFirst (constraintList list1
, constraintList list2
)
61 ret
= constraintList_mergeEnsures (list1
, list2
);
63 constraintList_free(list1
);
67 /*@only@*/ constraintList
constraintList_mergeEnsures (constraintList list1
, constraintList list2
)
72 llassert (constraintList_isDefined(list1
));
73 llassert (constraintList_isDefined(list2
));
75 DPRINTF(( message ("constraintList_mergeEnsures: list1 %s list2 %s",
76 constraintList_unparse(list1
), constraintList_unparse(list2
))));
78 ret
= constraintList_fixConflicts (list1
, list2
);
79 ret
= reflectChangesEnsuresFree1 (ret
, list2
);
80 temp
= constraintList_subsumeEnsures (ret
, list2
);
81 constraintList_free(ret
);
84 temp
= constraintList_subsumeEnsures (list2
, ret
);
86 temp
= constraintList_addList (temp
, ret
);
87 constraintList_free(ret
);
89 DPRINTF(( message ("constraintList_mergeEnsures: returning %s ",
90 constraintList_unparse(temp
))));
96 /*@only@*/ constraintList
constraintList_mergeRequiresFreeFirst (/*@only@*/ constraintList list1
, constraintList list2
)
100 ret
= constraintList_mergeRequires(list1
, list2
);
102 constraintList_free(list1
);
107 /*@only@*/ constraintList
constraintList_mergeRequires (constraintList list1
, constraintList list2
)
112 DPRINTF((message ("constraintList_mergeRequires: merging %s and %s ", constraintList_unparse (list1
), constraintList_unparse(list2
) ) ) );
114 if (context_getFlag (FLG_REDUNDANTCONSTRAINTS
) )
116 ret
= constraintList_copy(list1
);
117 ret
= constraintList_addList(ret
, list2
);
121 /* get constraints in list1 not satified by list2 */
122 temp
= constraintList_reflectChanges(list1
, list2
);
123 DPRINTF((message ("constraintList_mergeRequires: temp = %s", constraintList_unparse(temp
) ) ) );
125 /*get constraints in list2 not satified by temp*/
126 ret
= constraintList_reflectChanges(list2
, temp
);
128 DPRINTF((message ("constraintList_mergeRequires: ret = %s", constraintList_unparse(ret
) ) ) );
130 ret
= constraintList_addListFree (ret
, temp
);
132 DPRINTF((message ("constraintList_mergeRequires: returning %s", constraintList_unparse(ret
) ) ) );
137 /* old name mergeResolve renamed for czech naming convention */
138 void exprNode_mergeResolve (exprNode parent
, exprNode child1
, exprNode child2
)
140 constraintList temp
, temp2
;
142 DPRINTF((message ("magically merging constraint into parent:%s for", exprNode_unparse (parent
))));
143 DPRINTF((message (" children: %s and %s", exprNode_unparse (child1
), exprNode_unparse(child2
))));
145 if (exprNode_isUndefined(parent
))
147 llassert (exprNode_isDefined(parent
));
151 if (exprNode_isUndefined (child1
) || exprNode_isUndefined(child2
))
153 if (exprNode_isUndefined (child1
) && exprNode_isDefined(child2
))
155 constraintList_free(parent
->requiresConstraints
);
157 parent
->requiresConstraints
= constraintList_copy (child2
->requiresConstraints
);
158 constraintList_free(parent
->ensuresConstraints
);
160 parent
->ensuresConstraints
= constraintList_copy (child2
->ensuresConstraints
);
161 DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
162 constraintList_unparse( child2
->requiresConstraints
),
163 constraintList_unparse (child2
->ensuresConstraints
)
170 llassert (exprNode_isUndefined(child2
));
175 llassertfatal (exprNode_isDefined (child1
) && exprNode_isDefined(child2
));
177 DPRINTF((message ("Child constraints are %s %s and %s %s",
178 constraintList_unparse (child1
->requiresConstraints
),
179 constraintList_unparse (child1
->ensuresConstraints
),
180 constraintList_unparse (child2
->requiresConstraints
),
181 constraintList_unparse (child2
->ensuresConstraints
))));
183 constraintList_free(parent
->requiresConstraints
);
185 parent
->requiresConstraints
= constraintList_copy (child1
->requiresConstraints
);
187 if ( context_getFlag (FLG_ORCONSTRAINT
) )
188 temp
= constraintList_reflectChangesOr (child2
->requiresConstraints
, child1
->ensuresConstraints
);
190 temp
= constraintList_reflectChanges(child2
->requiresConstraints
, child1
->ensuresConstraints
);
192 temp2
= constraintList_mergeRequires (parent
->requiresConstraints
, temp
);
193 constraintList_free(parent
->requiresConstraints
);
194 constraintList_free(temp
);
196 parent
->requiresConstraints
= temp2
;
198 DPRINTF((message ("Parent requires constraints are %s ",
199 constraintList_unparse (parent
->requiresConstraints
)
202 constraintList_free(parent
->ensuresConstraints
);
204 parent
->ensuresConstraints
= constraintList_mergeEnsures(child1
->ensuresConstraints
,
205 child2
->ensuresConstraints
);
208 DPRINTF((message ("Parent constraints are %s and %s ",
209 constraintList_unparse (parent
->requiresConstraints
),
210 constraintList_unparse (parent
->ensuresConstraints
)
215 static /*@only@*/ constraintList
constraintList_subsumeEnsures (constraintList list1
, constraintList list2
)
218 ret
= constraintList_makeNew();
219 constraintList_elements (list1
, el
)
222 DPRINTF ((message ("Examining %s", constraint_unparse (el
) ) ) );
223 if (!constraintList_resolve (el
, list2
) )
226 temp
= constraint_copy(el
);
227 ret
= constraintList_add (ret
, temp
);
231 DPRINTF ((message ("Subsuming %s", constraint_unparse (el
) ) ) );
233 } end_constraintList_elements
;
240 /*used to be reflectChangesFreePre renamed for Czech naming conventino*/
241 /* tries to resolve constraints in list pre2 using post1 */
242 /*@only@*/ constraintList
constraintList_reflectChangesFreePre (/*@only@*/ constraintList pre2
, /*@observer@*/ constraintList post1
)
246 ret
= constraintList_reflectChanges(pre2
, post1
);
248 constraintList_free (pre2
);
253 /* tries to resolve constraints in list pre2 using post1 */
255 static /*@only@*/ constraintList
reflectChangesNoOr (/*@observer@*/ /*@temp@*/ constraintList pre2
, /*@observer@*/ /*@temp@*/ constraintList post1
)
262 llassert (!context_getFlag (FLG_ORCONSTRAINT
));
264 ret
= constraintList_makeNew();
265 DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_unparse(pre2
), constraintList_unparse(post1
) )));
267 constraintList_elements (pre2
, el
)
269 if (!constraintList_resolve (el
, post1
) )
271 temp
= constraint_substitute (el
, post1
);
272 if (!constraintList_resolve (temp
, post1
) )
274 /* try inequality substitution
275 the inequality substitution may cause us to lose information
276 so we don't want to store the result but we do it anyway
278 temp2
= constraint_copy (temp
);
279 temp2
= inequalitySubstitute (temp2
, post1
);
280 if (!constraintList_resolve (temp2
, post1
) )
282 temp2
= inequalitySubstituteUnsound (temp2
, post1
);
283 if (!constraintList_resolve (temp2
, post1
) )
284 ret
= constraintList_add (ret
, temp2
);
286 constraint_free(temp2
);
290 constraint_free(temp2
);
293 constraint_free(temp
);
295 } end_constraintList_elements
;
297 DPRINTF((message ("reflectChanges: returning %s", constraintList_unparse(ret
) ) ) );
301 /* tries to resolve constraints in list pre2 using post1 */
302 /*@only@*/ constraintList
constraintList_reflectChanges(/*@observer@*/ constraintList pre2
, /*@observer@*/ constraintList post1
)
306 if ( context_getFlag (FLG_ORCONSTRAINT
) )
308 temp
= constraintList_reflectChangesOr (pre2
, post1
);
310 temp
= reflectChangesNoOr(pre2
, post1
);
315 static constraint
constraint_addOr (/*@returned@*/ constraint orig
, /*@observer@*/ constraint orConstr
)
319 llassertfatal (constraint_isDefined(orig
));
323 DPRINTF((message("constraint_addor: oring %s onto %s", constraint_unparseOr(orConstr
), constraint_unparseOr(orig
) ) ));
325 while (c
->or != NULL
)
330 c
->or = constraint_copy(orConstr
);
332 DPRINTF((message("constraint_addor: returning %s",constraint_unparseOr(orig
) ) ));
338 static bool resolveOr ( /*@temp@*/ constraint c
, /*@observer@*/ /*@temp@*/ constraintList list
)
343 llassertfatal (constraint_isDefined(c
));
345 DPRINTF(( message("resolveOr: constraint %s and list %s", constraint_unparseOr(c
), constraintList_unparse(list
) ) ));
351 if (constraintList_resolve (temp
, list
))
355 llassert (numberOr
<= 10);
357 while (constraint_isDefined(temp
));
362 /*This is a "helper" function for doResolveOr */
364 static /*@only@*/ constraint
doResolve (/*@only@*/ constraint c
, constraintList post1
, bool * resolved
)
368 llassert (constraint_isDefined (c
));
370 DPRINTF((message("doResolve:: call on constraint c = : %q and constraintList %q",
371 constraint_unparseOr(c
), constraintList_unparse(post1
))));
373 if (!resolveOr (c
, post1
))
375 temp
= constraint_substitute (c
, post1
);
377 DPRINTF((message("doResolve:: after substitute temp is %q",
378 constraint_unparseOr(temp
))));
380 if (!resolveOr (temp
, post1
))
382 /* try inequality substitution */
385 /* the inequality substitution may cause us to lose information
386 so we don't want to store the result but we do anyway
388 temp2
= constraint_copy (c
);
389 temp2
= inequalitySubstitute (temp2
, post1
);
391 if (!resolveOr (temp2
, post1
))
394 temp3
= constraint_copy(temp2
);
396 temp3
= inequalitySubstituteStrong (temp3
, post1
);
397 if (!resolveOr (temp3
, post1
) )
399 temp2
= inequalitySubstituteUnsound (temp2
, post1
);
400 if (!resolveOr (temp2
, post1
) )
402 if (!constraint_same (temp
, temp2
) )
404 /* drl added 8/28/2002*/
405 /*make sure that the information from
406 a post condition like i = i + 1 is transfered
409 tempSub
= constraint_substitute (temp2
, post1
);
412 message("doResolve: adding %s ",
413 constraint_unparseOr(tempSub
)
418 message("doResolve: not adding %s ",
419 constraint_unparseOr(temp2
)
423 temp
= constraint_addOr (temp
, tempSub
);
424 constraint_free(tempSub
);
427 if (!constraint_same (temp
, temp3
) && !constraint_same (temp3
, temp2
) )
429 /* drl added 8/28/2002*/
430 /*make sure that the information from
431 a post condition like i = i + 1 is transfered
435 tempSub
= constraint_substitute (temp3
, post1
);
438 message("doResolve: adding %s ",
439 constraint_unparseOr(tempSub
)
445 message("doResolve: not adding %s ",
446 constraint_unparseOr(temp3
)
450 temp
= constraint_addOr (temp
, tempSub
);
452 constraint_free(tempSub
);
456 constraint_free(temp2
);
457 constraint_free(temp3
);
462 constraint_free(temp2
);
463 constraint_free(temp3
);
467 constraint_free(temp2
);
468 constraint_free(temp3
);
473 constraint_free(temp2
);
477 constraint_free(temp
);
485 static /*@only@*/ constraint
doResolveOr (/*@observer@*/ /*@temp@*/ constraint c
, constraintList post1
, /*@out@*/bool * resolved
)
491 DPRINTF ((message("doResolveOr: constraint %s and list %s",
492 constraint_unparseOr(c
), constraintList_unparse(post1
))));
496 llassert (constraint_isDefined(c
));
498 ret
= constraint_copy(c
);
500 llassertfatal (constraint_isDefined(ret
));
502 if (constraintList_isEmpty(post1
))
510 ret
= doResolve (ret
, post1
, resolved
);
515 constraint_free(next
);
517 /*we don't need to free ret when resolved is false because ret is null*/
518 llassert(ret
== NULL
);
529 curr
= doResolve (curr
, post1
, resolved
);
533 /* curr is null so we don't try to free it*/
534 llassert(curr
== NULL
);
537 constraint_free(next
);
539 constraint_free(ret
);
542 ret
= constraint_addOr (ret
, curr
);
543 constraint_free(curr
);
546 DPRINTF(( message("doResolveOr: returning ret = %s", constraint_unparseOr(ret
) ) ));
551 /* tries to resolve constraints in list pr2 using post1 */
552 /*@only@*/ constraintList
constraintList_reflectChangesOr (constraintList pre2
, constraintList post1
)
557 ret
= constraintList_makeNew();
558 DPRINTF((message ("constraintList_reflectChangesOr: lists %s and %s", constraintList_unparse(pre2
), constraintList_unparse(post1
) )));
560 constraintList_elements (pre2
, el
)
562 temp
= doResolveOr (el
, post1
, &resolved
);
566 ret
= constraintList_add(ret
, temp
);
570 /* we don't need to free temp when
571 resolved is false because temp is null */
572 llassert(temp
== NULL
);
575 } end_constraintList_elements
;
577 DPRINTF((message ("constraintList_reflectChangesOr: returning %s", constraintList_unparse(ret
) ) ) );
581 static /*@only@*/ constraintList
reflectChangesEnsures (/*@observer@*/ constraintList pre2
, constraintList post1
)
585 ret
= constraintList_makeNew();
586 constraintList_elements (pre2
, el
)
588 if (!constraintList_resolve (el
, post1
) )
590 temp
= constraint_substitute (el
, post1
);
591 llassert (temp
!= NULL
);
593 if (!constraintList_resolve (temp
, post1
) )
594 ret
= constraintList_add (ret
, temp
);
596 constraint_free(temp
);
600 DPRINTF ((message ("Resolved away %s ", constraint_unparse(el
) ) ) );
602 } end_constraintList_elements
;
608 static /*@only@*/ constraintList
reflectChangesEnsuresFree1 (/*@only@*/ constraintList pre2
, constraintList post1
)
612 ret
= reflectChangesEnsures (pre2
, post1
);
614 constraintList_free(pre2
);
620 static bool constraint_conflict (constraint c1
, constraint c2
)
622 if (!constraint_isDefined(c1
) || !constraint_isDefined(c2
))
627 if (constraintExpr_similar (c1
->lexpr
, c2
->lexpr
))
630 if (c1
->ar
== c2
->ar
)
632 DPRINTF (("%s conflicts with %s", constraint_unparse (c1
), constraint_unparse (c2
)));
637 /* This is a slight kludge to prevent circular constraints like
638 strlen(str) == maxRead(s) + strlen(str);
641 /*this code is functional but it may be worth cleaning up at some point. */
644 if (c1
->ar
== c2
->ar
)
646 if (constraintExpr_search (c1
->lexpr
, c2
->expr
) )
647 if (constraintExpr_isTerm(c1
->lexpr
) )
651 term
= constraintExpr_getTerm(c1
->lexpr
);
653 if (constraintTerm_isExprNode(term
) )
655 DPRINTF ((message ("%s conflicts with %s ", constraint_unparse (c1
), constraint_unparse(c2
) ) ) );
661 if (constraint_tooDeep(c1
) || constraint_tooDeep(c2
) )
663 DPRINTF ((message ("%s conflicts with %s (constraint is too deep", constraint_unparse (c1
), constraint_unparse(c2
) ) ) );
667 DPRINTF ((message ("%s doesn't conflict with %s ", constraint_unparse (c1
), constraint_unparse(c2
) ) ) );
673 static void constraint_fixConflict (/*@temp@*/ constraint good
, /*@temp@*/ /*@observer@*/ constraint conflicting
) /*@modifies good@*/
675 llassertfatal (constraint_isDefined(conflicting
));
677 if (conflicting
->ar
== EQ
)
679 llassertfatal (constraint_isDefined(good
));
680 DPRINTF (("Replacing here!"));
681 good
->expr
= constraintExpr_searchandreplace (good
->expr
, conflicting
->lexpr
, conflicting
->expr
);
682 good
= constraint_simplify (good
);
688 static bool conflict (constraint c
, constraintList list
)
691 constraintList_elements (list
, el
)
693 if ( constraint_conflict(el
, c
) )
695 constraint_fixConflict (el
, c
);
698 } end_constraintList_elements
;
705 check if constraint in list1 conflicts with constraints in List2. If so we
706 remove form list1 and change list2.
709 static constraintList
constraintList_fixConflicts (constraintList list1
, constraintList list2
)
712 ret
= constraintList_makeNew();
713 llassert(constraintList_isDefined(list1
) );
714 constraintList_elements (list1
, el
)
716 if (! conflict (el
, list2
) )
719 temp
= constraint_copy(el
);
720 ret
= constraintList_add (ret
, temp
);
722 } end_constraintList_elements
;
727 /*returns true if constraint post satisfies cosntriant pre */
729 static bool constraintResolve_satisfies (constraint pre
, constraint post
)
731 if (!constraint_isDefined (pre
))
736 if (!constraint_isDefined(post
))
741 if (constraint_isAlwaysTrue (pre
))
744 if (!constraintExpr_similar (pre
->lexpr
, post
->lexpr
) )
749 if (constraintExpr_isUndefined(post
->expr
))
755 return rangeCheck (pre
->ar
, pre
->expr
, post
->ar
, post
->expr
);
759 bool constraintList_resolve (/*@temp@*/ /*@observer@*/ constraint c
,
760 /*@temp@*/ /*@observer@*/ constraintList p
)
762 DPRINTF (("[resolve] Trying to resolve constraint: %s using %s",
763 constraint_unparse (c
),
764 constraintList_unparse (p
)));
766 constraintList_elements (p
, el
)
768 if (constraintResolve_satisfies (c
, el
))
770 DPRINTF (("constraintList_resolve: %s satifies %s",
771 constraint_unparse (el
), constraint_unparse (c
)));
775 DPRINTF (("constraintList_resolve: %s does not satify %s\n ",
776 constraint_unparse (el
), constraint_unparse (c
)));
778 end_constraintList_elements
;
780 DPRINTF (("No constraints satify: %s", constraint_unparse (c
)));
784 static bool arithType_canResolve (arithType ar1
, arithType ar2
)
790 if ((ar2
== GT
) || (ar2
== GTE
) || (ar2
== EQ
))
803 if ((ar2
== LT
) || (ar2
== LTE
) || (ar2
== EQ
))
812 /*checks for the case expr2 == sizeof buf1 and buf1 is a fixed array*/
813 static bool sizeofBufComp(constraintExpr buf1
, constraintExpr expr2
)
819 llassertfatal (constraintExpr_isDefined(buf1
) && constraintExpr_isDefined(expr2
));
821 /*@access constraintExpr@*/
823 if ((expr2
->kind
!= term
) && (buf1
->kind
!= term
) )
827 ct
= constraintExprData_termGetTerm(expr2
->data
);
829 if (!constraintTerm_isExprNode(ct
) )
832 e
= constraintTerm_getExprNode(ct
);
834 llassert (exprNode_isDefined(e
));
835 if (!exprNode_isDefined(e
))
838 if (e
->kind
!= XPR_SIZEOF
)
841 t
= exprData_getSingle (e
->edata
);
842 s1
= exprNode_getSref (t
);
844 s2
= constraintTerm_getsRef(constraintExprData_termGetTerm(buf1
->data
) );
846 /*drl this may be the wronge thing to test for but this
847 seems to work correctly*/
848 if (sRef_similarRelaxed(s1
, s2
) || sRef_sameName (s1
, s2
) )
850 /* origly checked that ctype_isFixedArray(sRef_getType(s2)) but
857 /* look for the special case of
858 maxSet(buf) >= sizeof(buf) - 1
861 /*drl eventually it would be good to check that
862 buf is of type char.*/
864 static bool sizeOfMaxSet( /*@observer@*/ /*@temp@*/ constraint c
)
866 constraintExpr l
, r
, buf1
, buf2
, con
;
868 DPRINTF ((message("sizeOfMaxSet: checking %s ", constraint_unparse(c
))));
870 llassertfatal (constraint_isDefined(c
));
875 if (!((c
->ar
== EQ
) || (c
->ar
== GTE
) || (c
->ar
== LTE
)))
878 llassertfatal (constraintExpr_isDefined(l
));
879 llassertfatal (constraintExpr_isDefined(r
));
881 /*check if the constraintExpr is MaxSet(buf) */
882 if (l
->kind
== unaryExpr
)
884 if (constraintExprData_unaryExprGetOp(l
->data
) == MAXSET
)
886 buf1
= constraintExprData_unaryExprGetExpr(l
->data
);
895 if (r
->kind
!= binaryexpr
)
898 buf2
= constraintExprData_binaryExprGetExpr1(r
->data
);
899 con
= constraintExprData_binaryExprGetExpr2(r
->data
);
901 if (constraintExprData_binaryExprGetOp(r
->data
) == BINARYOP_MINUS
)
903 if (constraintExpr_canGetValue(con
) )
907 i
= constraintExpr_getValue(con
);
917 if (constraintExprData_binaryExprGetOp(r
->data
) == BINARYOP_PLUS
)
919 if (constraintExpr_canGetValue(con
) )
923 i
= constraintExpr_getValue(con
);
933 if (sizeofBufComp(buf1
, buf2
))
942 /*@noaccess constraintExpr@*/
944 /* We look for constraint which are tautologies */
946 bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c
)
952 llassertfatal (constraint_isDefined(c
));
957 DPRINTF(( message("constraint_IsAlwaysTrue:examining %s", constraint_unparse(c
) ) ));
959 if (sizeOfMaxSet(c
) )
962 if (constraintExpr_canGetValue(l
) && constraintExpr_canGetValue(r
) )
965 cmp
= constraintExpr_compare (l
, r
);
986 if (constraintExpr_similar (l
,r
))
1005 l
= constraintExpr_copy (c
->lexpr
);
1006 r
= constraintExpr_copy (c
->expr
);
1008 r
= constraintExpr_propagateConstants (r
, &rHasConstant
, &rConstant
);
1010 if (constraintExpr_similar (l
,r
) && (rHasConstant
) )
1012 DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants %s and %s are similar", constraintExpr_unparse(l
), constraintExpr_unparse(r
) ) ));
1013 DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is %d", rConstant
) ));
1015 constraintExpr_free(l
);
1016 constraintExpr_free(r
);
1021 return (rConstant
== 0);
1023 return (rConstant
> 0);
1025 return (rConstant
>= 0);
1027 return (rConstant
<= 0);
1029 return (rConstant
< 0);
1039 constraintExpr_free(l
);
1040 constraintExpr_free(r
);
1041 DPRINTF(( message("Constraint %s is not always true", constraint_unparse(c
) ) ));
1048 static bool rangeCheck (arithType ar1
, /*@observer@*/ constraintExpr expr1
, arithType ar2
, /*@observer@*/ constraintExpr expr2
)
1051 DPRINTF (("Doing range check %s and %s",
1052 constraintExpr_unparse (expr1
), constraintExpr_unparse (expr2
)));
1054 if (!arithType_canResolve (ar1
, ar2
))
1060 if (constraintExpr_similar (expr1
, expr2
) )
1064 if (! (constraintExpr_canGetValue (expr1
) &&
1065 constraintExpr_canGetValue (expr2
) ) )
1067 constraintExpr e1
, e2
;
1071 e1
= constraintExpr_copy(expr1
);
1072 e2
= constraintExpr_copy(expr2
);
1074 e1
= constraintExpr_propagateConstants (e1
, &p1
, &const1
);
1075 e2
= constraintExpr_propagateConstants (e2
, &p2
, &const2
);
1085 if (const1
<= const2
)
1086 if (constraintExpr_similar (e1
, e2
) )
1088 constraintExpr_free(e1
);
1089 constraintExpr_free(e2
);
1093 DPRINTF(("Can't Get value"));
1095 constraintExpr_free(e1
);
1096 constraintExpr_free(e2
);
1100 if (constraintExpr_compare (expr2
, expr1
) >= 0)
1105 if (constraintExpr_similar (expr1
, expr2
) )
1110 if (constraintExpr_similar (expr1
, expr2
) )
1114 if (! (constraintExpr_canGetValue (expr1
) &&
1115 constraintExpr_canGetValue (expr2
) ) )
1117 constraintExpr e1
, e2
;
1121 e1
= constraintExpr_copy(expr1
);
1122 e2
= constraintExpr_copy(expr2
);
1124 e1
= constraintExpr_propagateConstants (e1
, &p1
, &const1
);
1126 e2
= constraintExpr_propagateConstants (e2
, &p2
, &const2
);
1136 if (const1
>= const2
)
1137 if (constraintExpr_similar (e1
, e2
) )
1139 constraintExpr_free(e1
);
1140 constraintExpr_free(e2
);
1144 constraintExpr_free(e1
);
1145 constraintExpr_free(e2
);
1147 DPRINTF(("Can't Get value"));
1151 if (constraintExpr_compare (expr2
, expr1
) <= 0)
1157 llcontbug((message("Unhandled case in switch: %q", arithType_print(ar1
) ) ) );
1162 static constraint
constraint_searchandreplace (/*@returned@*/ constraint c
, constraintExpr old
, constraintExpr newExpr
)
1164 llassertfatal (constraint_isDefined(c
));
1166 DPRINTF (("Starting replace lexpr [%p]: %s < %s ==> %s > in %s", c
,
1167 constraintExpr_unparse (c
->lexpr
),
1168 constraintExpr_unparse (old
), constraintExpr_unparse (newExpr
),
1169 constraint_unparse (c
)));
1170 c
->lexpr
= constraintExpr_searchandreplace (c
->lexpr
, old
, newExpr
);
1171 DPRINTF (("Finished replace lexpr [%p]: %s", c
, constraintExpr_unparse (c
->lexpr
)));
1172 c
->expr
= constraintExpr_searchandreplace (c
->expr
, old
, newExpr
);
1176 bool constraint_search (constraint c
, constraintExpr old
) /*@*/
1181 llassertfatal (constraint_isDefined (c
));
1183 ret
= constraintExpr_search (c
->lexpr
, old
);
1184 ret
= ret
|| constraintExpr_search (c
->expr
, old
);
1188 /* adjust file locs and stuff */
1189 static constraint
constraint_adjust (/*@returned@*/ constraint substitute
, /*@observer@*/ constraint old
)
1191 fileloc loc1
, loc2
, loc3
;
1193 DPRINTF ((message("Start adjust on %s and %s", constraint_unparse(substitute
),
1194 constraint_unparse(old
))));
1196 llassertfatal (constraint_isDefined(substitute
));
1197 llassert (constraint_isDefined(old
));
1199 loc1
= constraint_getFileloc (old
);
1200 loc2
= constraintExpr_loc (substitute
->lexpr
);
1201 loc3
= constraintExpr_loc (substitute
->expr
);
1203 /* special case of an equality that "contains itself" */
1204 if (constraintExpr_search (substitute
->expr
, substitute
->lexpr
) )
1205 if (fileloc_closer (loc1
, loc3
, loc2
))
1207 constraintExpr temp
;
1208 DPRINTF ((message("Doing adjust on %s", constraint_unparse(substitute
))));
1209 temp
= substitute
->lexpr
;
1210 substitute
->lexpr
= substitute
->expr
;
1211 substitute
->expr
= temp
;
1212 substitute
= constraint_simplify(substitute
);
1215 fileloc_free (loc1
);
1216 fileloc_free (loc2
);
1217 fileloc_free (loc3
);
1222 /* If function preforms substitutes based on inequality
1224 It uses the rule x >= y && b < y ===> x >= b + 1
1226 Warning this is sound but throws out information
1229 constraint
inequalitySubstitute (/*@returned@*/ constraint c
, constraintList p
)
1231 llassertfatal (constraint_isDefined(c
));
1236 constraintList_elements (p
, el
)
1238 llassertfatal (constraint_isDefined(el
));
1242 constraintExpr temp2
;
1244 if (constraintExpr_same (el
->expr
, c
->expr
) )
1246 DPRINTF((message ("inequalitySubstitute Replacing %q in %q with %q",
1247 constraintExpr_print (c
->expr
),
1248 constraint_unparse (c
),
1249 constraintExpr_print (el
->expr
) )
1251 temp2
= constraintExpr_copy (el
->lexpr
);
1252 constraintExpr_free(c
->expr
);
1253 c
->expr
= constraintExpr_makeIncConstraintExpr (temp2
);
1259 end_constraintList_elements
;
1261 c
= constraint_simplify(c
);
1268 THis function is like inequalitySubstitute but it adds the rule
1269 added the rules x >= y && y <= b ===> x >= b
1270 x >= y && y < b ===> x >= b + 1
1272 This is sound but sonce it throws out additional information it should only one used
1273 if we're oring constraints.
1276 static constraint
inequalitySubstituteStrong (/*@returned@*/ constraint c
, constraintList p
)
1278 DPRINTF (( message ("inequalitySubstituteStrong examining substituting for %q", constraint_unparse(c
) ) ));
1280 llassert (constraint_isDefined(c
));
1282 if (!constraint_isDefined(c
))
1290 DPRINTF (( message ("inequalitySubstituteStrong examining substituting for %q with %q",
1291 constraint_unparse(c
), constraintList_unparse(p
) ) ));
1292 constraintList_elements (p
, el
)
1294 DPRINTF (( message ("inequalitySubstituteStrong examining substituting %s on %s",
1295 constraint_unparse(el
), constraint_unparse(c
))));
1297 llassertfatal (constraint_isDefined(el
));
1298 if ((el
->ar
== LT
) || (el
->ar
== LTE
) )
1300 constraintExpr temp2
;
1302 if (constraintExpr_same (el
->lexpr
, c
->expr
) )
1304 DPRINTF((message ("inequalitySubstitute Replacing %s in %s with %s",
1305 constraintExpr_print (c
->expr
),
1306 constraint_unparse (c
),
1307 constraintExpr_print (el
->expr
))));
1308 temp2
= constraintExpr_copy (el
->expr
);
1309 constraintExpr_free(c
->expr
);
1316 c
->expr
= constraintExpr_makeIncConstraintExpr (temp2
);
1322 end_constraintList_elements
;
1324 c
= constraint_simplify(c
);
1329 /* This function performs substitutions based on the rule:
1330 for a constraint of the form expr1 >= expr2; a < b =>
1331 a = b -1 for all a in expr1. This will work in most cases.
1333 Like inequalitySubstitute we're throwing away some information
1336 static constraint
inequalitySubstituteUnsound (/*@returned@*/ constraint c
, constraintList p
)
1338 DPRINTF (( message ("Doing inequalitySubstituteUnsound " ) ));
1340 llassertfatal (constraint_isDefined(c
));
1345 constraintList_elements (p
, el
)
1347 llassertfatal (constraint_isDefined(el
));
1349 DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s",
1350 constraint_unparse(el
), constraint_unparse(c
))));
1351 if (( el
->ar
== LTE
) || (el
->ar
== LT
) )
1353 constraintExpr temp2
;
1355 temp2
= constraintExpr_copy (el
->expr
);
1358 temp2
= constraintExpr_makeDecConstraintExpr (temp2
);
1360 DPRINTF((message ("Replacing %s in %s with %s",
1361 constraintExpr_print (el
->lexpr
),
1362 constraintExpr_print (c
->lexpr
),
1363 constraintExpr_print (temp2
) ) ));
1365 c
->lexpr
= constraintExpr_searchandreplace (c
->lexpr
, el
->lexpr
, temp2
);
1366 constraintExpr_free(temp2
);
1369 end_constraintList_elements
;
1371 c
= constraint_simplify(c
);
1375 /*@only@*/ constraint
constraint_substitute (/*@observer@*/ /*@temp@*/ constraint c
, constraintList p
)
1377 constraint ret
= constraint_copy (c
);
1379 constraintList_elements (p
, el
)
1381 if (constraint_isDefined (el
))
1384 if (!constraint_conflict (ret
, el
))
1386 constraint temp
= constraint_copy(el
);
1387 temp
= constraint_adjust(temp
, ret
);
1389 llassertfatal (constraint_isDefined(temp
));
1391 DPRINTF (("constraint_substitute :: Substituting in %s using %s",
1392 constraint_unparse (ret
), constraint_unparse (temp
)));
1394 ret
= constraint_searchandreplace (ret
, temp
->lexpr
, temp
->expr
);
1395 DPRINTF (("constraint_substitute :: The new constraint is %s", constraint_unparse (ret
)));;
1396 constraint_free(temp
);
1400 end_constraintList_elements
;
1402 ret
= constraint_simplify (ret
);
1403 DPRINTF(( message (" constraint_substitute :: The final new constraint is %s", constraint_unparse (ret
) ) ));
1408 /* we try to do substitutions on each constraint in target using the constraint in sublist*/
1410 static /*@only@*/ constraintList
1411 constraintList_substitute (constraintList target
,/*2observer@*/ constraintList subList
)
1416 ret
= constraintList_makeNew();
1418 constraintList_elements(target
, el
)
1421 /* drl possible problem : warning make sure that a side effect is not expected */
1423 temp
= constraint_substitute(el
, subList
);
1424 ret
= constraintList_add (ret
, temp
);
1426 end_constraintList_elements
;
1431 /*@only@*/ constraintList
constraintList_substituteFreeTarget (/*@only@*/ constraintList target
, /*@observer@*/ constraintList subList
)
1434 ret
= constraintList_substitute (target
, subList
);
1435 constraintList_free(target
);
1440 static constraint
constraint_solve (/*@returned@*/ constraint c
)
1442 llassertfatal (constraint_isDefined(c
));
1444 DPRINTF((message ("Solving %s\n", constraint_unparse(c
) ) ) );
1445 c
->expr
= constraintExpr_solveBinaryExpr (c
->lexpr
, c
->expr
);
1446 DPRINTF((message ("Solved and got %s\n", constraint_unparse(c
) ) ) );
1451 static arithType
flipAr (arithType ar
)
1466 llcontbug (message("unexpected value: case not handled"));
1471 static constraint
constraint_swapLeftRight (/*@returned@*/ constraint c
)
1473 constraintExpr temp
;
1475 llassertfatal (constraint_isDefined(c
));
1477 c
->ar
= flipAr (c
->ar
);
1481 DPRINTF(("Swaped left and right sides of constraint"));
1486 constraint
constraint_simplify ( /*@returned@*/ constraint c
)
1488 llassertfatal (constraint_isDefined(c
));
1490 DPRINTF(( message("constraint_simplify on %q ", constraint_unparse(c
) ) ));
1492 if (constraint_tooDeep(c
))
1494 DPRINTF(( message("constraint_simplify: constraint to complex aborting %q ", constraint_unparse(c
) ) ));
1498 c
->lexpr
= constraintExpr_simplify (c
->lexpr
);
1499 c
->expr
= constraintExpr_simplify (c
->expr
);
1501 if (constraintExpr_isBinaryExpr (c
->lexpr
) )
1503 c
= constraint_solve (c
);
1505 c
->lexpr
= constraintExpr_simplify (c
->lexpr
);
1506 c
->expr
= constraintExpr_simplify (c
->expr
);
1509 if (constraintExpr_isLit(c
->lexpr
) && (!constraintExpr_isLit(c
->expr
) ) )
1511 c
= constraint_swapLeftRight(c
);
1512 /*I don't think this will be an infinate loop*/
1513 c
= constraint_simplify(c
);
1516 DPRINTF(( message("constraint_simplify returning %q ", constraint_unparse(c
) ) ));
1524 /* returns true if fileloc for term1 is closer to file for term2 than term3*/
1526 static bool fileloc_closer (fileloc loc1
, fileloc loc2
, fileloc loc3
)
1529 if (!fileloc_isDefined (loc1
) )
1532 if (!fileloc_isDefined (loc2
) )
1535 if (!fileloc_isDefined (loc3
) )
1541 if (fileloc_equal (loc2
, loc3
) )
1544 if (fileloc_equal (loc1
, loc2
) )
1547 if (fileloc_equal (loc1
, loc3
) )
1550 if ( fileloc_lessthan (loc1
, loc2
) )
1552 if (fileloc_lessthan (loc2
, loc3
) )
1554 llassert (fileloc_lessthan (loc1
, loc3
) );
1563 if ( !fileloc_lessthan (loc1
, loc2
) )
1565 if (!fileloc_lessthan (loc2
, loc3
) )
1567 llassert (!fileloc_lessthan (loc1
, loc3
) );