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 /* #define DEBUGPRINT 1 */
32 # include "splintMacros.nf"
35 /*@access constraint, exprNode @*/ /*!!! NO! Don't do this so recklessly - design your code more carefully so you don't need to! */
37 static constraint
inequalitySubstitute (/*@returned@*/ constraint p_c
, constraintList p_p
);
38 static bool rangeCheck (arithType p_ar1
, /*@observer@*/ constraintExpr p_expr1
, arithType p_ar2
, /*@observer@*/ constraintExpr p_expr2
);
40 static constraint
inequalitySubstituteUnsound (/*@returned@*/ constraint p_c
, constraintList p_p
);
41 static constraint
inequalitySubstituteStrong (/*@returned@*/ constraint p_c
, constraintList p_p
);
43 static constraint
constraint_searchandreplace (/*@returned@*/ constraint p_c
, constraintExpr p_old
, constraintExpr p_newExpr
);
45 static constraint
constraint_addOr (/*@returned@*/ constraint p_orig
, /*@observer@*/ constraint p_orConstr
);
47 static bool resolveOr (/*@temp@*/constraint p_c
, /*@observer@*/ /*@temp@*/ constraintList p_list
);
49 static /*@only@*/ constraintList
reflectChangesEnsuresFree1 (/*@only@*/ constraintList p_pre2
, constraintList p_post1
);
51 static /*@only@*/ constraintList
constraintList_subsumeEnsures (constraintList p_list1
, constraintList p_list2
);
52 static /*@only@*/ constraintList
constraintList_fixConflicts (constraintList p_list1
, constraintList p_list2
);
54 static bool fileloc_closer (/*@observer@*/ fileloc p_loc1
,
55 /*@observer@*/ fileloc p_loc2
,
56 /*@observer@*/ fileloc p_loc3
) /*@*/;
59 /*@only@*/ constraintList
constraintList_mergeEnsuresFreeFirst (constraintList list1
, constraintList list2
)
63 ret
= constraintList_mergeEnsures (list1
, list2
);
65 constraintList_free(list1
);
69 /*@only@*/ constraintList
constraintList_mergeEnsures (constraintList list1
, constraintList list2
)
74 llassert(constraintList_isDefined(list1
) );
75 llassert(constraintList_isDefined(list2
) );
77 DPRINTF(( message ("constraintList_mergeEnsures: list1 %s list2 %s",
78 constraintList_unparse(list1
), constraintList_unparse(list2
)
81 ret
= constraintList_fixConflicts (list1
, list2
);
82 ret
= reflectChangesEnsuresFree1 (ret
, list2
);
83 temp
= constraintList_subsumeEnsures (ret
, list2
);
84 constraintList_free(ret
);
87 temp
= constraintList_subsumeEnsures (list2
, ret
);
89 temp
= constraintList_addList (temp
, ret
);
90 constraintList_free(ret
);
92 DPRINTF(( message ("constraintList_mergeEnsures: returning %s ",
93 constraintList_unparse(temp
) )
101 /*@only@*/ constraintList
constraintList_mergeRequiresFreeFirst (/*@only@*/ constraintList list1
, constraintList list2
)
105 ret
= constraintList_mergeRequires(list1
, list2
);
107 constraintList_free(list1
);
112 /*@only@*/ constraintList
constraintList_mergeRequires (constraintList list1
, constraintList list2
)
117 DPRINTF((message ("constraintList_mergeRequires: merging %s and %s ", constraintList_unparse (list1
), constraintList_unparse(list2
) ) ) );
119 if (context_getFlag (FLG_REDUNDANTCONSTRAINTS
) )
121 ret
= constraintList_copy(list1
);
122 ret
= constraintList_addList(ret
, list2
);
126 /* get constraints in list1 not satified by list2 */
127 temp
= constraintList_reflectChanges(list1
, list2
);
128 DPRINTF((message ("constraintList_mergeRequires: temp = %s", constraintList_unparse(temp
) ) ) );
130 /*get constraints in list2 not satified by temp*/
131 ret
= constraintList_reflectChanges(list2
, temp
);
133 DPRINTF((message ("constraintList_mergeRequires: ret = %s", constraintList_unparse(ret
) ) ) );
135 ret
= constraintList_addListFree (ret
, temp
);
137 DPRINTF((message ("constraintList_mergeRequires: returning %s", constraintList_unparse(ret
) ) ) );
142 /* old name mergeResolve renamed for czech naming convention */
143 void exprNode_mergeResolve (exprNode parent
, exprNode child1
, exprNode child2
)
145 constraintList temp
, temp2
;
147 DPRINTF((message ("magically merging constraint into parent:%s for", exprNode_unparse (parent
) )) );
149 DPRINTF((message (" children: %s and %s", exprNode_unparse (child1
), exprNode_unparse(child2
) ) ) );
152 if (exprNode_isUndefined(parent
) )
154 llassert (exprNode_isDefined(parent
) );
159 if (exprNode_isError (child1
) || exprNode_isError(child2
) )
161 if (exprNode_isError (child1
) && !exprNode_isError(child2
) )
163 constraintList_free(parent
->requiresConstraints
);
165 parent
->requiresConstraints
= constraintList_copy (child2
->requiresConstraints
);
166 constraintList_free(parent
->ensuresConstraints
);
168 parent
->ensuresConstraints
= constraintList_copy (child2
->ensuresConstraints
);
169 DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
170 constraintList_unparse( child2
->requiresConstraints
),
171 constraintList_unparse (child2
->ensuresConstraints
)
178 llassert(exprNode_isError(child2
) );
183 llassert(!exprNode_isError (child1
) && ! exprNode_isError(child2
) );
185 DPRINTF((message ("Child constraints are %s %s and %s %s",
186 constraintList_unparse (child1
->requiresConstraints
),
187 constraintList_unparse (child1
->ensuresConstraints
),
188 constraintList_unparse (child2
->requiresConstraints
),
189 constraintList_unparse (child2
->ensuresConstraints
)
193 constraintList_free(parent
->requiresConstraints
);
195 parent
->requiresConstraints
= constraintList_copy (child1
->requiresConstraints
);
197 if ( context_getFlag (FLG_ORCONSTRAINT
) )
198 temp
= constraintList_reflectChangesOr (child2
->requiresConstraints
, child1
->ensuresConstraints
);
200 temp
= constraintList_reflectChanges(child2
->requiresConstraints
, child1
->ensuresConstraints
);
202 temp2
= constraintList_mergeRequires (parent
->requiresConstraints
, temp
);
203 constraintList_free(parent
->requiresConstraints
);
204 constraintList_free(temp
);
206 parent
->requiresConstraints
= temp2
;
208 DPRINTF((message ("Parent requires constraints are %s ",
209 constraintList_unparse (parent
->requiresConstraints
)
212 constraintList_free(parent
->ensuresConstraints
);
214 parent
->ensuresConstraints
= constraintList_mergeEnsures(child1
->ensuresConstraints
,
215 child2
->ensuresConstraints
);
218 DPRINTF((message ("Parent constraints are %s and %s ",
219 constraintList_unparse (parent
->requiresConstraints
),
220 constraintList_unparse (parent
->ensuresConstraints
)
225 static /*@only@*/ constraintList
constraintList_subsumeEnsures (constraintList list1
, constraintList list2
)
228 ret
= constraintList_makeNew();
229 constraintList_elements (list1
, el
)
232 DPRINTF ((message ("Examining %s", constraint_unparse (el
) ) ) );
233 if (!constraintList_resolve (el
, list2
) )
236 temp
= constraint_copy(el
);
237 ret
= constraintList_add (ret
, temp
);
241 DPRINTF ((message ("Subsuming %s", constraint_unparse (el
) ) ) );
243 } end_constraintList_elements
;
250 /*used to be reflectChangesFreePre renamed for Czech naming conventino*/
251 /* tries to resolve constraints in list pre2 using post1 */
252 /*@only@*/ constraintList
constraintList_reflectChangesFreePre (/*@only@*/ constraintList pre2
, /*@observer@*/ constraintList post1
)
256 ret
= constraintList_reflectChanges(pre2
, post1
);
258 constraintList_free (pre2
);
263 /* tries to resolve constraints in list pre2 using post1 */
265 static /*@only@*/ constraintList
reflectChangesNoOr (/*@observer@*/ /*@temp@*/ constraintList pre2
, /*@observer@*/ /*@temp@*/ constraintList post1
)
272 llassert (! context_getFlag (FLG_ORCONSTRAINT
) );
274 ret
= constraintList_makeNew();
275 DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_unparse(pre2
), constraintList_unparse(post1
) )));
277 constraintList_elements (pre2
, el
)
279 if (!constraintList_resolve (el
, post1
) )
281 temp
= constraint_substitute (el
, post1
);
282 if (!constraintList_resolve (temp
, post1
) )
284 /* try inequality substitution
285 the inequality substitution may cause us to lose information
286 so we don't want to store the result but we do it anyway
288 temp2
= constraint_copy (temp
);
289 temp2
= inequalitySubstitute (temp2
, post1
);
290 if (!constraintList_resolve (temp2
, post1
) )
292 temp2
= inequalitySubstituteUnsound (temp2
, post1
);
293 if (!constraintList_resolve (temp2
, post1
) )
294 ret
= constraintList_add (ret
, temp2
);
296 constraint_free(temp2
);
300 constraint_free(temp2
);
303 constraint_free(temp
);
305 } end_constraintList_elements
;
307 DPRINTF((message ("reflectChanges: returning %s", constraintList_unparse(ret
) ) ) );
311 /* tries to resolve constraints in list pre2 using post1 */
312 /*@only@*/ constraintList
constraintList_reflectChanges(/*@observer@*/ constraintList pre2
, /*@observer@*/ constraintList post1
)
316 if ( context_getFlag (FLG_ORCONSTRAINT
) )
318 temp
= constraintList_reflectChangesOr (pre2
, post1
);
320 temp
= reflectChangesNoOr(pre2
, post1
);
325 static constraint
constraint_addOr (/*@returned@*/ constraint orig
, /*@observer@*/ constraint orConstr
)
329 llassert(constraint_isDefined(orig
) );
333 DPRINTF((message("constraint_addor: oring %s onto %s", constraint_unparseOr(orConstr
), constraint_unparseOr(orig
) ) ));
335 while (c
->or != NULL
)
340 c
->or = constraint_copy(orConstr
);
342 DPRINTF((message("constraint_addor: returning %s",constraint_unparseOr(orig
) ) ));
348 static bool resolveOr ( /*@temp@*/ constraint c
, /*@observer@*/ /*@temp@*/ constraintList list
)
356 llassert(constraint_isDefined(c
) );
358 DPRINTF(( message("resolveOr: constraint %s and list %s", constraint_unparseOr(c
), constraintList_unparse(list
) ) ));
364 if (constraintList_resolve (temp
, list
) )
368 llassert(numberOr
<= 10);
370 while (constraint_isDefined(temp
));
375 /*This is a "helper" function for doResolveOr */
377 static /*@only@*/ constraint
doResolve (/*@only@*/ constraint c
, constraintList post1
, bool * resolved
)
381 llassert(constraint_isDefined (c
) );
383 DPRINTF((message("doResolve:: call on constraint c = : %q and constraintList %q",
384 constraint_unparseOr(c
), constraintList_unparse(post1
)
388 if (!resolveOr (c
, post1
) )
391 temp
= constraint_substitute (c
, post1
);
393 DPRINTF((message("doResolve:: after substitute temp is %q",
394 constraint_unparseOr(temp
)
398 if (!resolveOr (temp
, post1
) )
400 /* try inequality substitution */
403 /* the inequality substitution may cause us to lose information
404 so we don't want to store the result but we do anyway
406 temp2
= constraint_copy (c
);
407 temp2
= inequalitySubstitute (temp2
, post1
);
409 if (!resolveOr (temp2
, post1
) )
412 temp3
= constraint_copy(temp2
);
414 temp3
= inequalitySubstituteStrong (temp3
, post1
);
415 if (!resolveOr (temp3
, post1
) )
417 temp2
= inequalitySubstituteUnsound (temp2
, post1
);
418 if (!resolveOr (temp2
, post1
) )
420 if (!constraint_same (temp
, temp2
) )
422 /* drl added 8/28/2002*/
423 /*make sure that the information from
424 a post condition like i = i + 1 is transfered
427 tempSub
= constraint_substitute (temp2
, post1
);
430 message("doResolve: adding %s ",
431 constraint_unparseOr(tempSub
)
436 message("doResolve: not adding %s ",
437 constraint_unparseOr(temp2
)
441 temp
= constraint_addOr (temp
, tempSub
);
442 constraint_free(tempSub
);
445 if (!constraint_same (temp
, temp3
) && !constraint_same (temp3
, temp2
) )
447 /* drl added 8/28/2002*/
448 /*make sure that the information from
449 a post condition like i = i + 1 is transfered
453 tempSub
= constraint_substitute (temp3
, post1
);
456 message("doResolve: adding %s ",
457 constraint_unparseOr(tempSub
)
463 message("doResolve: not adding %s ",
464 constraint_unparseOr(temp3
)
468 temp
= constraint_addOr (temp
, tempSub
);
470 constraint_free(tempSub
);
474 constraint_free(temp2
);
475 constraint_free(temp3
);
480 constraint_free(temp2
);
481 constraint_free(temp3
);
485 constraint_free(temp2
);
486 constraint_free(temp3
);
491 constraint_free(temp2
);
495 constraint_free(temp
);
503 static /*@only@*/ constraint
doResolveOr (/*@observer@*/ /*@temp@*/ constraint c
, constraintList post1
, /*@out@*/bool * resolved
)
509 DPRINTF(( message("doResolveOr: constraint %s and list %s", constraint_unparseOr(c
), constraintList_unparse(post1
) ) ));
513 llassert(constraint_isDefined(c
) );
515 ret
= constraint_copy(c
);
517 llassert(constraint_isDefined(ret
) );
519 if (constraintList_isEmpty(post1
) )
527 ret
= doResolve (ret
, post1
, resolved
);
532 constraint_free(next
);
534 /*we don't need to free ret when resolved is false because ret is null*/
535 llassert(ret
== NULL
);
546 curr
= doResolve (curr
, post1
, resolved
);
550 /* curr is null so we don't try to free it*/
551 llassert(curr
== NULL
);
554 constraint_free(next
);
556 constraint_free(ret
);
559 ret
= constraint_addOr (ret
, curr
);
560 constraint_free(curr
);
563 DPRINTF(( message("doResolveOr: returning ret = %s", constraint_unparseOr(ret
) ) ));
568 /* tries to resolve constraints in list pr2 using post1 */
569 /*@only@*/ constraintList
constraintList_reflectChangesOr (constraintList pre2
, constraintList post1
)
574 ret
= constraintList_makeNew();
575 DPRINTF((message ("constraintList_reflectChangesOr: lists %s and %s", constraintList_unparse(pre2
), constraintList_unparse(post1
) )));
577 constraintList_elements (pre2
, el
)
579 temp
= doResolveOr (el
, post1
, &resolved
);
583 ret
= constraintList_add(ret
, temp
);
587 /* we don't need to free temp when
588 resolved is false because temp is null */
589 llassert(temp
== NULL
);
592 } end_constraintList_elements
;
594 DPRINTF((message ("constraintList_reflectChangesOr: returning %s", constraintList_unparse(ret
) ) ) );
598 static /*@only@*/ constraintList
reflectChangesEnsures (/*@observer@*/ constraintList pre2
, constraintList post1
)
602 ret
= constraintList_makeNew();
603 constraintList_elements (pre2
, el
)
605 if (!constraintList_resolve (el
, post1
) )
607 temp
= constraint_substitute (el
, post1
);
608 llassert (temp
!= NULL
);
610 if (!constraintList_resolve (temp
, post1
) )
611 ret
= constraintList_add (ret
, temp
);
613 constraint_free(temp
);
617 DPRINTF ((message ("Resolved away %s ", constraint_unparse(el
) ) ) );
619 } end_constraintList_elements
;
625 static /*@only@*/ constraintList
reflectChangesEnsuresFree1 (/*@only@*/ constraintList pre2
, constraintList post1
)
629 ret
= reflectChangesEnsures (pre2
, post1
);
631 constraintList_free(pre2
);
637 static bool constraint_conflict (constraint c1
, constraint c2
)
639 if (!constraint_isDefined(c1
) || !constraint_isDefined(c2
))
644 if (constraintExpr_similar (c1
->lexpr
, c2
->lexpr
))
647 if (c1
->ar
== c2
->ar
)
649 DPRINTF (("%s conflicts with %s", constraint_unparse (c1
), constraint_unparse (c2
)));
654 /* This is a slight kludge to prevent circular constraints like
655 strlen(str) == maxRead(s) + strlen(str);
658 /*this code is functional but it may be worth cleaning up at some point. */
661 if (c1
->ar
== c2
->ar
)
663 if (constraintExpr_search (c1
->lexpr
, c2
->expr
) )
664 if (constraintExpr_isTerm(c1
->lexpr
) )
668 term
= constraintExpr_getTerm(c1
->lexpr
);
670 if (constraintTerm_isExprNode(term
) )
672 DPRINTF ((message ("%s conflicts with %s ", constraint_unparse (c1
), constraint_unparse(c2
) ) ) );
678 if (constraint_tooDeep(c1
) || constraint_tooDeep(c2
) )
680 DPRINTF ((message ("%s conflicts with %s (constraint is too deep", constraint_unparse (c1
), constraint_unparse(c2
) ) ) );
684 DPRINTF ((message ("%s doesn't conflict with %s ", constraint_unparse (c1
), constraint_unparse(c2
) ) ) );
690 static void constraint_fixConflict (/*@temp@*/ constraint good
, /*@temp@*/ /*@observer@*/ constraint conflicting
) /*@modifies good@*/
692 llassert(constraint_isDefined(conflicting
) );
694 if (conflicting
->ar
== EQ
)
696 llassert (constraint_isDefined(good
));
697 DPRINTF (("Replacing here!"));
698 good
->expr
= constraintExpr_searchandreplace (good
->expr
, conflicting
->lexpr
, conflicting
->expr
);
699 good
= constraint_simplify (good
);
705 static bool conflict (constraint c
, constraintList list
)
708 constraintList_elements (list
, el
)
710 if ( constraint_conflict(el
, c
) )
712 constraint_fixConflict (el
, c
);
715 } end_constraintList_elements
;
722 check if constraint in list1 conflicts with constraints in List2. If so we
723 remove form list1 and change list2.
726 static constraintList
constraintList_fixConflicts (constraintList list1
, constraintList list2
)
729 ret
= constraintList_makeNew();
730 llassert(constraintList_isDefined(list1
) );
731 constraintList_elements (list1
, el
)
733 if (! conflict (el
, list2
) )
736 temp
= constraint_copy(el
);
737 ret
= constraintList_add (ret
, temp
);
739 } end_constraintList_elements
;
744 /*returns true if constraint post satisfies cosntriant pre */
746 static bool constraintResolve_satisfies (constraint pre
, constraint post
)
748 if (!constraint_isDefined (pre
))
753 if (!constraint_isDefined(post
))
758 if (constraint_isAlwaysTrue (pre
))
761 if (!constraintExpr_similar (pre
->lexpr
, post
->lexpr
) )
766 if (constraintExpr_isUndefined(post
->expr
))
772 return rangeCheck (pre
->ar
, pre
->expr
, post
->ar
, post
->expr
);
776 bool constraintList_resolve (/*@temp@*/ /*@observer@*/ constraint c
,
777 /*@temp@*/ /*@observer@*/ constraintList p
)
779 DPRINTF (("[resolve] Trying to resolve constraint: %s using %s",
780 constraint_unparse (c
),
781 constraintList_unparse (p
)));
783 constraintList_elements (p
, el
)
785 if (constraintResolve_satisfies (c
, el
))
787 DPRINTF (("constraintList_resolve: %s satifies %s",
788 constraint_unparse (el
), constraint_unparse (c
)));
792 DPRINTF (("constraintList_resolve: %s does not satify %s\n ",
793 constraint_unparse (el
), constraint_unparse (c
)));
795 end_constraintList_elements
;
797 DPRINTF (("No constraints satify: %s", constraint_unparse (c
)));
801 static bool arithType_canResolve (arithType ar1
, arithType ar2
)
807 if ((ar2
== GT
) || (ar2
== GTE
) || (ar2
== EQ
))
820 if ((ar2
== LT
) || (ar2
== LTE
) || (ar2
== EQ
))
829 /*checks for the case expr2 == sizeof buf1 and buf1 is a fixed array*/
830 static bool sizeofBufComp(constraintExpr buf1
, constraintExpr expr2
)
836 llassert(constraintExpr_isDefined(buf1
) && constraintExpr_isDefined(expr2
) );
838 /*@access constraintExpr@*/
840 if ((expr2
->kind
!= term
) && (buf1
->kind
!= term
) )
844 ct
= constraintExprData_termGetTerm(expr2
->data
);
846 if (!constraintTerm_isExprNode(ct
) )
849 e
= constraintTerm_getExprNode(ct
);
851 llassert (exprNode_isDefined(e
));
853 if (! (exprNode_isDefined(e
)))
856 if (e
->kind
!= XPR_SIZEOF
)
859 t
= exprData_getSingle (e
->edata
);
860 s1
= exprNode_getSref (t
);
862 s2
= constraintTerm_getsRef(constraintExprData_termGetTerm(buf1
->data
) );
864 /*drl this may be the wronge thing to test for but this
865 seems to work correctly*/
866 if (sRef_similarRelaxed(s1
, s2
) || sRef_sameName (s1
, s2
) )
868 /* origly checked that ctype_isFixedArray(sRef_getType(s2)) but
875 /* look for the special case of
876 maxSet(buf) >= sizeof(buf) - 1
879 /*drl eventually it would be good to check that
880 buf is of type char.*/
882 static bool sizeOfMaxSet( /*@observer@*/ /*@temp@*/ constraint c
)
884 constraintExpr l
, r
, buf1
, buf2
, con
;
886 DPRINTF(( message("sizeOfMaxSet: checking %s ", constraint_unparse(c
) )
889 llassert (constraint_isDefined(c
) );
894 if (!((c
->ar
== EQ
) || (c
->ar
== GTE
) || (c
->ar
== LTE
) ) )
897 llassert (constraintExpr_isDefined(l
) );
898 llassert (constraintExpr_isDefined(r
) );
900 /*check if the constraintExpr is MaxSet(buf) */
901 if (l
->kind
== unaryExpr
)
903 if (constraintExprData_unaryExprGetOp(l
->data
) == MAXSET
)
905 buf1
= constraintExprData_unaryExprGetExpr(l
->data
);
914 if (r
->kind
!= binaryexpr
)
917 buf2
= constraintExprData_binaryExprGetExpr1(r
->data
);
918 con
= constraintExprData_binaryExprGetExpr2(r
->data
);
920 if (constraintExprData_binaryExprGetOp(r
->data
) == BINARYOP_MINUS
)
922 if (constraintExpr_canGetValue(con
) )
926 i
= constraintExpr_getValue(con
);
936 if (constraintExprData_binaryExprGetOp(r
->data
) == BINARYOP_PLUS
)
938 if (constraintExpr_canGetValue(con
) )
942 i
= constraintExpr_getValue(con
);
952 if (sizeofBufComp(buf1
, buf2
))
961 /*@noaccess constraintExpr@*/
963 /* We look for constraint which are tautologies */
965 bool constraint_isAlwaysTrue (/*@observer@*/ /*@temp@*/ constraint c
)
972 llassert (constraint_isDefined(c
) );
977 DPRINTF(( message("constraint_IsAlwaysTrue:examining %s", constraint_unparse(c
) ) ));
979 if (sizeOfMaxSet(c
) )
982 if (constraintExpr_canGetValue(l
) && constraintExpr_canGetValue(r
) )
985 cmp
= constraintExpr_compare (l
, r
);
1006 if (constraintExpr_similar (l
,r
))
1025 l
= constraintExpr_copy (c
->lexpr
);
1026 r
= constraintExpr_copy (c
->expr
);
1028 r
= constraintExpr_propagateConstants (r
, &rHasConstant
, &rConstant
);
1030 if (constraintExpr_similar (l
,r
) && (rHasConstant
) )
1032 DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants %s and %s are similar", constraintExpr_unparse(l
), constraintExpr_unparse(r
) ) ));
1033 DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is %d", rConstant
) ));
1035 constraintExpr_free(l
);
1036 constraintExpr_free(r
);
1041 return (rConstant
== 0);
1043 return (rConstant
> 0);
1045 return (rConstant
>= 0);
1047 return (rConstant
<= 0);
1049 return (rConstant
< 0);
1059 constraintExpr_free(l
);
1060 constraintExpr_free(r
);
1061 DPRINTF(( message("Constraint %s is not always true", constraint_unparse(c
) ) ));
1068 static bool rangeCheck (arithType ar1
, /*@observer@*/ constraintExpr expr1
, arithType ar2
, /*@observer@*/ constraintExpr expr2
)
1071 DPRINTF (("Doing range check %s and %s",
1072 constraintExpr_unparse (expr1
), constraintExpr_unparse (expr2
)));
1074 if (!arithType_canResolve (ar1
, ar2
))
1080 if (constraintExpr_similar (expr1
, expr2
) )
1084 if (! (constraintExpr_canGetValue (expr1
) &&
1085 constraintExpr_canGetValue (expr2
) ) )
1087 constraintExpr e1
, e2
;
1091 e1
= constraintExpr_copy(expr1
);
1092 e2
= constraintExpr_copy(expr2
);
1094 e1
= constraintExpr_propagateConstants (e1
, &p1
, &const1
);
1095 e2
= constraintExpr_propagateConstants (e2
, &p2
, &const2
);
1105 if (const1
<= const2
)
1106 if (constraintExpr_similar (e1
, e2
) )
1108 constraintExpr_free(e1
);
1109 constraintExpr_free(e2
);
1113 DPRINTF(("Can't Get value"));
1115 constraintExpr_free(e1
);
1116 constraintExpr_free(e2
);
1120 if (constraintExpr_compare (expr2
, expr1
) >= 0)
1125 if (constraintExpr_similar (expr1
, expr2
) )
1130 if (constraintExpr_similar (expr1
, expr2
) )
1134 if (! (constraintExpr_canGetValue (expr1
) &&
1135 constraintExpr_canGetValue (expr2
) ) )
1137 constraintExpr e1
, e2
;
1141 e1
= constraintExpr_copy(expr1
);
1142 e2
= constraintExpr_copy(expr2
);
1144 e1
= constraintExpr_propagateConstants (e1
, &p1
, &const1
);
1146 e2
= constraintExpr_propagateConstants (e2
, &p2
, &const2
);
1156 if (const1
>= const2
)
1157 if (constraintExpr_similar (e1
, e2
) )
1159 constraintExpr_free(e1
);
1160 constraintExpr_free(e2
);
1164 constraintExpr_free(e1
);
1165 constraintExpr_free(e2
);
1167 DPRINTF(("Can't Get value"));
1171 if (constraintExpr_compare (expr2
, expr1
) <= 0)
1177 llcontbug((message("Unhandled case in switch: %q", arithType_print(ar1
) ) ) );
1182 static constraint
constraint_searchandreplace (/*@returned@*/ constraint c
, constraintExpr old
, constraintExpr newExpr
)
1184 llassert (constraint_isDefined(c
));
1186 DPRINTF (("Starting replace lexpr [%p]: %s < %s ==> %s > in %s", c
,
1187 constraintExpr_unparse (c
->lexpr
),
1188 constraintExpr_unparse (old
), constraintExpr_unparse (newExpr
),
1189 constraint_unparse (c
)));
1190 c
->lexpr
= constraintExpr_searchandreplace (c
->lexpr
, old
, newExpr
);
1191 DPRINTF (("Finished replace lexpr [%p]: %s", c
, constraintExpr_unparse (c
->lexpr
)));
1192 c
->expr
= constraintExpr_searchandreplace (c
->expr
, old
, newExpr
);
1196 bool constraint_search (constraint c
, constraintExpr old
) /*@*/
1201 llassert (constraint_isDefined (c
));
1203 ret
= constraintExpr_search (c
->lexpr
, old
);
1204 ret
= ret
|| constraintExpr_search (c
->expr
, old
);
1208 /* adjust file locs and stuff */
1209 static constraint
constraint_adjust (/*@returned@*/ constraint substitute
, /*@observer@*/ constraint old
)
1211 fileloc loc1
, loc2
, loc3
;
1213 DPRINTF ((message("Start adjust on %s and %s", constraint_unparse(substitute
),
1214 constraint_unparse(old
))
1217 llassert(constraint_isDefined(substitute
));
1218 llassert(constraint_isDefined(old
));
1220 loc1
= constraint_getFileloc (old
);
1221 loc2
= constraintExpr_loc (substitute
->lexpr
);
1222 loc3
= constraintExpr_loc (substitute
->expr
);
1224 /* special case of an equality that "contains itself" */
1225 if (constraintExpr_search (substitute
->expr
, substitute
->lexpr
) )
1226 if (fileloc_closer (loc1
, loc3
, loc2
))
1228 constraintExpr temp
;
1229 DPRINTF ((message("Doing adjust on %s", constraint_unparse(substitute
) )
1231 temp
= substitute
->lexpr
;
1232 substitute
->lexpr
= substitute
->expr
;
1233 substitute
->expr
= temp
;
1234 substitute
= constraint_simplify(substitute
);
1237 fileloc_free (loc1
);
1238 fileloc_free (loc2
);
1239 fileloc_free (loc3
);
1245 /* If function preforms substitutes based on inequality
1247 It uses the rule x >= y && b < y ===> x >= b + 1
1249 Warning this is sound but throws out information
1252 constraint
inequalitySubstitute (/*@returned@*/ constraint c
, constraintList p
)
1254 llassert(constraint_isDefined(c
) );
1259 constraintList_elements (p
, el
)
1262 llassert(constraint_isDefined(el
) );
1266 constraintExpr temp2
;
1268 if (constraintExpr_same (el
->expr
, c
->expr
) )
1270 DPRINTF((message ("inequalitySubstitute Replacing %q in %q with %q",
1271 constraintExpr_print (c
->expr
),
1272 constraint_unparse (c
),
1273 constraintExpr_print (el
->expr
) )
1275 temp2
= constraintExpr_copy (el
->lexpr
);
1276 constraintExpr_free(c
->expr
);
1277 c
->expr
= constraintExpr_makeIncConstraintExpr (temp2
);
1283 end_constraintList_elements
;
1285 c
= constraint_simplify(c
);
1292 THis function is like inequalitySubstitute but it adds the rule
1293 added the rules x >= y && y <= b ===> x >= b
1294 x >= y && y < b ===> x >= b + 1
1296 This is sound but sonce it throws out additional information it should only one used
1297 if we're oring constraints.
1300 static constraint
inequalitySubstituteStrong (/*@returned@*/ constraint c
, constraintList p
)
1302 DPRINTF (( message ("inequalitySubstituteStrong examining substituting for %q", constraint_unparse(c
) ) ));
1304 llassert(constraint_isDefined(c
) );
1306 if (! (constraint_isDefined(c
) ) )
1314 DPRINTF (( message ("inequalitySubstituteStrong examining substituting for %q with %q",
1315 constraint_unparse(c
), constraintList_unparse(p
) ) ));
1316 constraintList_elements (p
, el
)
1319 DPRINTF (( message ("inequalitySubstituteStrong examining substituting %s on %s", constraint_unparse(el
), constraint_unparse(c
) ) ));
1321 llassert(constraint_isDefined(el
) );
1322 if ((el
->ar
== LT
) || (el
->ar
== LTE
) )
1324 constraintExpr temp2
;
1326 if (constraintExpr_same (el
->lexpr
, c
->expr
) )
1328 DPRINTF((message ("inequalitySubstitute Replacing %s in %s with %s",
1329 constraintExpr_print (c
->expr
),
1330 constraint_unparse (c
),
1331 constraintExpr_print (el
->expr
) )
1333 temp2
= constraintExpr_copy (el
->expr
);
1334 constraintExpr_free(c
->expr
);
1341 c
->expr
= constraintExpr_makeIncConstraintExpr (temp2
);
1347 end_constraintList_elements
;
1349 c
= constraint_simplify(c
);
1354 /* This function performs substitutions based on the rule:
1355 for a constraint of the form expr1 >= expr2; a < b =>
1356 a = b -1 for all a in expr1. This will work in most cases.
1358 Like inequalitySubstitute we're throwing away some information
1361 static constraint
inequalitySubstituteUnsound (/*@returned@*/ constraint c
, constraintList p
)
1363 DPRINTF (( message ("Doing inequalitySubstituteUnsound " ) ));
1365 llassert(constraint_isDefined(c
) );
1370 constraintList_elements (p
, el
)
1373 llassert(constraint_isDefined(el
) );
1375 DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s", constraint_unparse(el
), constraint_unparse(c
) ) ));
1376 if (( el
->ar
== LTE
) || (el
->ar
== LT
) )
1378 constraintExpr temp2
;
1380 temp2
= constraintExpr_copy (el
->expr
);
1383 temp2
= constraintExpr_makeDecConstraintExpr (temp2
);
1385 DPRINTF((message ("Replacing %s in %s with %s",
1386 constraintExpr_print (el
->lexpr
),
1387 constraintExpr_print (c
->lexpr
),
1388 constraintExpr_print (temp2
) ) ));
1390 c
->lexpr
= constraintExpr_searchandreplace (c
->lexpr
, el
->lexpr
, temp2
);
1391 constraintExpr_free(temp2
);
1394 end_constraintList_elements
;
1396 c
= constraint_simplify(c
);
1400 /*@only@*/ constraint
constraint_substitute (/*@observer@*/ /*@temp@*/ constraint c
, constraintList p
)
1402 constraint ret
= constraint_copy (c
);
1404 constraintList_elements (p
, el
)
1406 if (constraint_isDefined (el
))
1409 if (!constraint_conflict (ret
, el
))
1411 constraint temp
= constraint_copy(el
);
1412 temp
= constraint_adjust(temp
, ret
);
1414 llassert(constraint_isDefined(temp
) );
1417 DPRINTF (("constraint_substitute :: Substituting in %s using %s",
1418 constraint_unparse (ret
), constraint_unparse (temp
)));
1420 ret
= constraint_searchandreplace (ret
, temp
->lexpr
, temp
->expr
);
1421 DPRINTF (("constraint_substitute :: The new constraint is %s", constraint_unparse (ret
)));;
1422 constraint_free(temp
);
1426 end_constraintList_elements
;
1428 ret
= constraint_simplify (ret
);
1429 DPRINTF(( message (" constraint_substitute :: The final new constraint is %s", constraint_unparse (ret
) ) ));
1434 /* we try to do substitutions on each constraint in target using the constraint in sublist*/
1436 static /*@only@*/ constraintList
1437 constraintList_substitute (constraintList target
,/*2observer@*/ constraintList subList
)
1442 ret
= constraintList_makeNew();
1444 constraintList_elements(target
, el
)
1447 /* drl possible problem : warning make sure that a side effect is not expected */
1449 temp
= constraint_substitute(el
, subList
);
1450 ret
= constraintList_add (ret
, temp
);
1452 end_constraintList_elements
;
1457 /*@only@*/ constraintList
constraintList_substituteFreeTarget (/*@only@*/ constraintList target
, /*@observer@*/ constraintList subList
)
1460 ret
= constraintList_substitute (target
, subList
);
1461 constraintList_free(target
);
1466 static constraint
constraint_solve (/*@returned@*/ constraint c
)
1469 llassert(constraint_isDefined(c
) );
1471 DPRINTF((message ("Solving %s\n", constraint_unparse(c
) ) ) );
1472 c
->expr
= constraintExpr_solveBinaryExpr (c
->lexpr
, c
->expr
);
1473 DPRINTF((message ("Solved and got %s\n", constraint_unparse(c
) ) ) );
1478 static arithType
flipAr (arithType ar
)
1493 llcontbug (message("unexpected value: case not handled"));
1498 static constraint
constraint_swapLeftRight (/*@returned@*/ constraint c
)
1500 constraintExpr temp
;
1502 llassert(constraint_isDefined(c
) );
1504 c
->ar
= flipAr (c
->ar
);
1508 DPRINTF(("Swaped left and right sides of constraint"));
1514 constraint
constraint_simplify ( /*@returned@*/ constraint c
)
1517 llassert(constraint_isDefined(c
) );
1519 DPRINTF(( message("constraint_simplify on %q ", constraint_unparse(c
) ) ));
1521 if (constraint_tooDeep(c
))
1523 DPRINTF(( message("constraint_simplify: constraint to complex aborting %q ", constraint_unparse(c
) ) ));
1528 c
->lexpr
= constraintExpr_simplify (c
->lexpr
);
1529 c
->expr
= constraintExpr_simplify (c
->expr
);
1531 if (constraintExpr_isBinaryExpr (c
->lexpr
) )
1533 c
= constraint_solve (c
);
1535 c
->lexpr
= constraintExpr_simplify (c
->lexpr
);
1536 c
->expr
= constraintExpr_simplify (c
->expr
);
1539 if (constraintExpr_isLit(c
->lexpr
) && (!constraintExpr_isLit(c
->expr
) ) )
1541 c
= constraint_swapLeftRight(c
);
1542 /*I don't think this will be an infinate loop*/
1543 c
= constraint_simplify(c
);
1546 DPRINTF(( message("constraint_simplify returning %q ", constraint_unparse(c
) ) ));
1554 /* returns true if fileloc for term1 is closer to file for term2 than term3*/
1556 static bool fileloc_closer (fileloc loc1
, fileloc loc2
, fileloc loc3
)
1559 if (!fileloc_isDefined (loc1
) )
1562 if (!fileloc_isDefined (loc2
) )
1565 if (!fileloc_isDefined (loc3
) )
1571 if (fileloc_equal (loc2
, loc3
) )
1574 if (fileloc_equal (loc1
, loc2
) )
1577 if (fileloc_equal (loc1
, loc3
) )
1580 if ( fileloc_lessthan (loc1
, loc2
) )
1582 if (fileloc_lessthan (loc2
, loc3
) )
1584 llassert (fileloc_lessthan (loc1
, loc3
) );
1593 if ( !fileloc_lessthan (loc1
, loc2
) )
1595 if (!fileloc_lessthan (loc2
, loc3
) )
1597 llassert (!fileloc_lessthan (loc1
, loc3
) );