]>
Commit | Line | Data |
---|---|---|
616915dd | 1 | /* |
2 | * | |
3 | ** constraintResolve.c | |
4 | */ | |
5 | ||
6 | //#define DEBUGPRINT 1 | |
7 | ||
8 | # include <ctype.h> /* for isdigit */ | |
9 | # include "lclintMacros.nf" | |
10 | # include "basic.h" | |
11 | # include "cgrammar.h" | |
12 | # include "cgrammar_tokens.h" | |
13 | ||
14 | # include "exprChecks.h" | |
15 | # include "aliasChecks.h" | |
16 | # include "exprNodeSList.h" | |
17 | //# include "exprData.i" | |
18 | ||
616915dd | 19 | |
c3e695ff | 20 | /*@access constraint @*/ |
616915dd | 21 | |
22 | ||
90bc41f7 | 23 | constraint inequalitySubstituteUnsound (constraint c, constraintList p); |
616915dd | 24 | |
25 | constraintList reflectChanges (constraintList pre2, constraintList post1); | |
26 | constraint substitute (constraint c, constraintList p); | |
27 | constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new); | |
28 | bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2); | |
29 | bool satifies (constraint pre, constraint post); | |
30 | bool resolve (constraint c, constraintList p); | |
31 | constraintList reflectChangesEnsures (constraintList pre2, constraintList post1); | |
32 | constraint constraint_simplify (constraint c); | |
33 | ||
34 | constraintList constraintList_fixConflicts (constraintList list1, constraintList list2); | |
35 | ||
36 | constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2); | |
37 | ||
38 | constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2); | |
39 | constraint inequalitySubstitute (constraint c, constraintList p); | |
40 | ||
41 | /*********************************************/ | |
42 | ||
43 | ||
44 | constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2) | |
45 | { | |
46 | constraintList ret; | |
47 | constraintList temp; | |
470b7798 | 48 | |
c3e695ff | 49 | //ret = constraintList_makeNew(); |
90bc41f7 | 50 | |
51 | llassert(list1); | |
52 | llassert(list2); | |
53 | ||
54 | DPRINTF(( message ("constraintList_mergeEnsures: list1 %s list2 %s", | |
55 | constraintList_print(list1), constraintList_print(list2) | |
56 | ))); | |
616915dd | 57 | |
90bc41f7 | 58 | ret = constraintList_fixConflicts (list1, list2); |
59 | ret = reflectChangesEnsures (ret, list2); | |
616915dd | 60 | ret = constraintList_subsumeEnsures (ret, list2); |
61 | list2 = constraintList_subsumeEnsures (list2, ret); | |
62 | temp = constraintList_copy(list2); | |
63 | ||
64 | temp = constraintList_addList (temp, ret); | |
90bc41f7 | 65 | |
66 | DPRINTF(( message ("constraintList_mergeEnsures: returning %s ", | |
67 | constraintList_print(temp) ) | |
68 | )); | |
69 | ||
70 | ||
616915dd | 71 | return temp; |
72 | //ret = constraintList_addList (ret, list2); | |
73 | //return ret; | |
74 | } | |
75 | ||
470b7798 | 76 | constraintList constraintList_mergeRequires (constraintList list1, constraintList list2) |
77 | { | |
78 | constraintList ret; | |
79 | constraintList temp; | |
80 | ||
81 | DPRINTF((message ("constraintList_mergeRequires: merging %s and %s ", constraintList_print (list1), constraintList_print(list2) ) ) ); | |
82 | ||
83 | /* get constraints in list1 not satified by list2 */ | |
84 | temp = reflectChanges (list1, list2); | |
85 | DPRINTF((message ("constraintList_mergeRequires: temp = %s", constraintList_print(temp) ) ) ); | |
86 | ||
87 | /*get constraints in list2 not satified by temp*/ | |
88 | ret = reflectChanges (list2, temp); | |
89 | ||
90 | DPRINTF((message ("constraintList_mergeRequires: ret = %s", constraintList_print(ret) ) ) ); | |
91 | ||
92 | ret = constraintList_addList (ret, temp); | |
93 | ||
94 | DPRINTF((message ("constraintList_mergeRequires: returning %s", constraintList_print(ret) ) ) ); | |
95 | ||
96 | return ret; | |
97 | } | |
616915dd | 98 | |
9280addf | 99 | void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint) |
100 | { | |
c3e695ff | 101 | temp->requiresConstraints = constraintList_makeNew(); |
102 | temp->ensuresConstraints = constraintList_makeNew(); | |
103 | temp->trueEnsuresConstraints = constraintList_makeNew(); | |
104 | temp->falseEnsuresConstraints = constraintList_makeNew(); | |
9280addf | 105 | |
106 | exprNodeList_elements (arglist, el) | |
107 | { | |
108 | exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint); | |
109 | el->requiresConstraints = exprNode_traversRequiresConstraints(el); | |
110 | el->ensuresConstraints = exprNode_traversEnsuresConstraints(el); | |
111 | ||
112 | temp->requiresConstraints = constraintList_addList(temp->requiresConstraints, | |
113 | el->requiresConstraints); | |
114 | ||
115 | temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints, | |
116 | el->ensuresConstraints); | |
117 | } | |
118 | end_exprNodeList_elements; | |
119 | ||
120 | } | |
616915dd | 121 | |
122 | constraintList checkCall (exprNode fcn, exprNodeList arglist) | |
123 | { | |
124 | constraintList preconditions; | |
125 | uentry temp; | |
126 | DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) ); | |
127 | ||
128 | temp = exprNode_getUentry (fcn); | |
129 | ||
130 | preconditions = uentry_getFcnPreconditions (temp); | |
131 | ||
132 | if (preconditions) | |
133 | { | |
134 | preconditions = constraintList_copy(preconditions); | |
135 | preconditions= constraintList_togglePost (preconditions); | |
136 | preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist); | |
137 | } | |
138 | else | |
139 | { | |
c3e695ff | 140 | preconditions = constraintList_makeNew(); |
616915dd | 141 | } |
142 | ||
143 | return preconditions; | |
144 | } | |
145 | ||
146 | constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall) | |
147 | { | |
148 | constraintList postconditions; | |
149 | uentry temp; | |
150 | DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) ); | |
151 | ||
152 | temp = exprNode_getUentry (fcn); | |
153 | ||
154 | postconditions = uentry_getFcnPostconditions (temp); | |
155 | ||
156 | if (postconditions) | |
157 | { | |
158 | postconditions = constraintList_copy(postconditions); | |
159 | postconditions = constraintList_doFixResult (postconditions, fcnCall); | |
160 | postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist); | |
161 | } | |
162 | else | |
163 | { | |
c3e695ff | 164 | postconditions = constraintList_makeNew(); |
616915dd | 165 | } |
166 | ||
167 | return postconditions; | |
168 | } | |
169 | ||
170 | void mergeResolve (exprNode parent, exprNode child1, exprNode child2) | |
171 | { | |
172 | constraintList temp; | |
173 | ||
174 | DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) ))); | |
175 | ||
176 | DPRINTF( (message (" children: %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) ); | |
177 | ||
178 | if (exprNode_isError (child1) || exprNode_isError(child2) ) | |
179 | { | |
180 | if (exprNode_isError (child1) && !exprNode_isError(child2) ) | |
181 | { | |
182 | parent->requiresConstraints = constraintList_copy (child2->requiresConstraints); | |
183 | parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints); | |
184 | DPRINTF((message ("Copied child constraints: pre: %s and post: %s", | |
185 | constraintList_print( child2->requiresConstraints), | |
186 | constraintList_print (child2->ensuresConstraints) | |
187 | ) | |
188 | )); | |
189 | return; | |
190 | } | |
191 | else | |
192 | { | |
193 | llassert(exprNode_isError(child2) ); | |
c3e695ff | 194 | parent->requiresConstraints = constraintList_makeNew(); |
195 | parent->ensuresConstraints = constraintList_makeNew(); | |
616915dd | 196 | return; |
197 | } | |
198 | } | |
199 | ||
200 | llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) ); | |
201 | ||
9280addf | 202 | DPRINTF( (message ("Child constraints are %s %s and %s %s", |
616915dd | 203 | constraintList_print (child1->requiresConstraints), |
204 | constraintList_print (child1->ensuresConstraints), | |
205 | constraintList_print (child2->requiresConstraints), | |
206 | constraintList_print (child2->ensuresConstraints) | |
207 | ) ) ); | |
208 | ||
c3e695ff | 209 | parent->requiresConstraints = constraintList_makeNew(); |
210 | parent->ensuresConstraints = constraintList_makeNew(); | |
616915dd | 211 | |
212 | parent->requiresConstraints = constraintList_copy (child1->requiresConstraints); | |
470b7798 | 213 | |
90bc41f7 | 214 | if ( context_getFlag (FLG_ORCONSTRAINT) ) |
215 | temp = reflectChangesOr (child2->requiresConstraints, child1->ensuresConstraints); | |
216 | else | |
217 | temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints); | |
218 | ||
470b7798 | 219 | parent->requiresConstraints = constraintList_mergeRequires (parent->requiresConstraints, temp); |
616915dd | 220 | |
221 | parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints, | |
222 | child2->ensuresConstraints); | |
223 | ||
224 | DPRINTF( (message ("Parent constraints are %s and %s ", | |
225 | constraintList_print (parent->requiresConstraints), | |
226 | constraintList_print (parent->ensuresConstraints) | |
227 | ) ) ); | |
228 | ||
229 | } | |
230 | ||
231 | ||
232 | ||
233 | ||
234 | constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2) | |
235 | { | |
236 | constraintList ret; | |
c3e695ff | 237 | ret = constraintList_makeNew(); |
616915dd | 238 | constraintList_elements (list1, el) |
239 | { | |
240 | ||
241 | DPRINTF ((message ("Examining %s", constraint_print (el) ) ) ); | |
242 | if (!resolve (el, list2) ) | |
243 | { | |
244 | ret = constraintList_add (ret, el); | |
245 | } | |
246 | else | |
247 | { | |
248 | DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) ); | |
249 | } | |
250 | } end_constraintList_elements; | |
251 | ||
252 | return ret; | |
253 | } | |
254 | ||
90bc41f7 | 255 | |
256 | /* tries to resolve constraints in list pre2 using post1 */ | |
616915dd | 257 | constraintList reflectChanges (constraintList pre2, constraintList post1) |
258 | { | |
259 | ||
260 | constraintList ret; | |
261 | constraint temp; | |
c3e695ff | 262 | ret = constraintList_makeNew(); |
616915dd | 263 | DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) ))); |
264 | ||
265 | constraintList_elements (pre2, el) | |
266 | { | |
267 | if (!resolve (el, post1) ) | |
268 | { | |
269 | temp = substitute (el, post1); | |
270 | if (!resolve (temp, post1) ) | |
271 | { | |
272 | // try inequality substitution | |
273 | constraint temp2; | |
274 | ||
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 | |
277 | temp2 = constraint_copy (temp); | |
90bc41f7 | 278 | // if (context_getFlag (FLG_ORCONSTRAINT) ) |
279 | temp2 = inequalitySubstitute (temp, post1); | |
280 | if (!resolve (temp2, post1) ) | |
281 | { | |
282 | temp2 = inequalitySubstituteUnsound (temp2, post1); | |
283 | if (!resolve (temp2, post1) ) | |
284 | ret = constraintList_add (ret, temp2); | |
285 | } | |
616915dd | 286 | } |
287 | } | |
288 | } end_constraintList_elements; | |
289 | ||
290 | DPRINTF((message ("reflectChanges: returning %s", constraintList_print(ret) ) ) ); | |
291 | return ret; | |
292 | } | |
293 | ||
294 | ||
90bc41f7 | 295 | constraint constraint_addOr (constraint orig, constraint or) |
296 | { | |
297 | constraint c; | |
298 | c = orig; | |
299 | ||
300 | DPRINTF((message("constraint_addor: oring %s onto %s", constraint_printOr(or), constraint_printOr(orig) ) )); | |
301 | ||
302 | while (c->or != NULL) | |
303 | { | |
304 | c = c->or; | |
305 | } | |
306 | c->or = constraint_copy(or); | |
307 | ||
308 | DPRINTF((message("constraint_addor: returning %s",constraint_printOr(orig) ) )); | |
309 | ||
310 | return orig; | |
311 | } | |
312 | ||
313 | ||
314 | bool resolveOr (constraint c, constraintList list) | |
315 | { | |
316 | constraint temp; | |
317 | ||
318 | DPRINTF(( message("resolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(list) ) )); | |
319 | temp = c; | |
320 | ||
321 | do | |
322 | { | |
323 | if (resolve (temp, list) ) | |
324 | return TRUE; | |
325 | temp = temp->or; | |
326 | } | |
327 | while (temp); | |
328 | ||
329 | return FALSE; | |
330 | } | |
331 | ||
332 | ||
333 | constraint doResolve (constraint c, constraintList post1, bool * resolved) | |
334 | { | |
335 | constraint temp; | |
336 | ||
337 | if (!resolveOr (c, post1) ) | |
338 | { | |
339 | temp = substitute (c, post1); | |
340 | if (!resolveOr (temp, post1) ) | |
341 | { | |
342 | // try inequality substitution | |
343 | constraint temp2; | |
344 | ||
345 | // the inequality substitution may cause us to lose information | |
346 | //so we don't want to store the result but we do it anyway | |
347 | temp2 = constraint_copy (c); | |
348 | // if (context_getFlag (FLG_ORCONSTRAINT) ) | |
349 | temp2 = inequalitySubstitute (temp2, post1); | |
350 | if (!resolveOr (temp2, post1) ) | |
351 | { | |
352 | temp2 = inequalitySubstituteUnsound (temp2, post1); | |
353 | if (!resolveOr (temp2, post1) ) | |
354 | { | |
355 | if (!constraint_same (temp, temp2) ) | |
356 | temp = constraint_addOr (temp, temp2); | |
357 | *resolved = FALSE; | |
358 | return temp; | |
359 | } | |
360 | } | |
361 | } | |
362 | } | |
363 | ||
364 | *resolved = TRUE; | |
365 | return NULL; | |
366 | ||
367 | ||
368 | ||
369 | } | |
370 | ||
371 | constraint doResolveOr (constraint c, constraintList post1, bool * resolved) | |
372 | { | |
373 | constraint ret; | |
374 | constraint next; | |
375 | constraint curr; | |
376 | ||
377 | *resolved = FALSE; | |
378 | ret = constraint_copy(c); | |
379 | next = ret->or; | |
380 | ret->or = NULL; | |
381 | ||
382 | ret = doResolve (ret, post1, resolved); | |
383 | while (next) | |
384 | { | |
385 | curr = next; | |
386 | next = curr->or; | |
387 | curr->or = NULL; | |
388 | ||
389 | curr = doResolve (curr, post1, resolved); | |
390 | if (*resolved) | |
391 | return NULL; | |
392 | ||
393 | ret = constraint_addOr (ret, curr); | |
394 | } | |
395 | ||
396 | return ret; | |
397 | } | |
398 | ||
399 | ||
400 | ||
401 | ||
402 | ||
403 | /* tries to resolve constraints in list pr2 using post1 */ | |
404 | constraintList reflectChangesOr (constraintList pre2, constraintList post1) | |
405 | { | |
406 | bool resolved; | |
407 | constraintList ret; | |
408 | constraint temp; | |
c3e695ff | 409 | ret = constraintList_makeNew(); |
90bc41f7 | 410 | DPRINTF((message ("reflectChangesOr: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) ))); |
411 | ||
412 | constraintList_elements (pre2, el) | |
413 | { | |
414 | temp = doResolveOr (el, post1, &resolved); | |
415 | ||
416 | if (!resolved) | |
417 | { | |
418 | ret = constraintList_add(ret, temp); | |
419 | } | |
420 | } end_constraintList_elements; | |
421 | ||
422 | DPRINTF((message ("reflectChangesOr: returning %s", constraintList_print(ret) ) ) ); | |
423 | return ret; | |
424 | } | |
616915dd | 425 | |
426 | constraintList reflectChangesEnsures (constraintList pre2, constraintList post1) | |
427 | { | |
428 | constraintList ret; | |
429 | constraint temp; | |
c3e695ff | 430 | ret = constraintList_makeNew(); |
616915dd | 431 | constraintList_elements (pre2, el) |
432 | { | |
433 | if (!resolve (el, post1) ) | |
434 | { | |
435 | temp = substitute (el, post1); | |
436 | llassert (temp != NULL); | |
437 | ||
438 | if (!resolve (temp, post1) ) | |
439 | ret = constraintList_add (ret, temp); | |
440 | } | |
441 | else | |
442 | { | |
443 | DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) ); | |
444 | } | |
445 | } end_constraintList_elements; | |
446 | ||
447 | return ret; | |
448 | } | |
449 | ||
450 | ||
451 | bool constraint_conflict (constraint c1, constraint c2) | |
452 | { | |
453 | ||
454 | if (constraintExpr_similar(c1->lexpr, c2->lexpr) ) | |
455 | { | |
456 | if (c1->ar == EQ) | |
457 | if (c1->ar == c2->ar) | |
458 | { | |
459 | DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); | |
460 | return TRUE; | |
461 | } | |
462 | } | |
463 | ||
464 | DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) ); | |
465 | ||
466 | return FALSE; | |
467 | ||
468 | } | |
469 | ||
470 | void constraint_fixConflict (constraint good, constraint conflicting) | |
471 | { | |
472 | constraint temp; | |
473 | if (conflicting->ar ==EQ ) | |
474 | { | |
475 | good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr); | |
476 | temp = constraint_simplify (good); | |
477 | constraint_overWrite (good, temp); | |
478 | } | |
479 | ||
480 | ||
481 | } | |
482 | ||
483 | bool conflict (constraint c, constraintList list) | |
484 | { | |
90bc41f7 | 485 | |
486 | constraintList_elements (list, el) | |
616915dd | 487 | { |
488 | if ( constraint_conflict(el, c) ) | |
489 | { | |
490 | constraint_fixConflict (el, c); | |
491 | return TRUE; | |
492 | } | |
493 | } end_constraintList_elements; | |
494 | ||
495 | return FALSE; | |
616915dd | 496 | |
497 | } | |
498 | ||
499 | //check if constraint in list1 and conflict with constraints in List2. If so we | |
90bc41f7 | 500 | //remove form list1 and change list2. |
501 | constraintList constraintList_fixConflicts (/*@returned@*/constraintList list1, constraintList list2) | |
616915dd | 502 | { |
503 | constraintList ret; | |
c3e695ff | 504 | ret = constraintList_makeNew(); |
90bc41f7 | 505 | llassert(list1); |
616915dd | 506 | constraintList_elements (list1, el) |
507 | { | |
508 | if (! conflict (el, list2) ) | |
509 | { | |
510 | ret = constraintList_add (ret, el); | |
511 | } | |
512 | } end_constraintList_elements; | |
513 | ||
514 | return ret; | |
515 | ||
516 | ||
517 | } | |
518 | ||
519 | bool resolve (constraint c, constraintList p) | |
520 | { | |
521 | constraintList_elements (p, el) | |
522 | { | |
523 | if ( satifies (c, el) ) | |
524 | { | |
525 | DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); | |
526 | return TRUE; | |
527 | } | |
528 | DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) ); | |
529 | } | |
530 | end_constraintList_elements; | |
531 | DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) )); | |
532 | return FALSE; | |
533 | } | |
534 | ||
535 | ||
90bc41f7 | 536 | /*returns true if constraint post satifies cosntriant pre */ |
616915dd | 537 | bool satifies (constraint pre, constraint post) |
538 | { | |
539 | if (constraint_isAlwaysTrue (pre) ) | |
540 | return TRUE; | |
541 | ||
542 | if (!constraintExpr_similar (pre->lexpr, post->lexpr) ) | |
543 | { | |
544 | return FALSE; | |
545 | } | |
546 | if (post->expr == NULL) | |
547 | { | |
548 | llassert(FALSE); | |
549 | return FALSE; | |
550 | } | |
551 | ||
552 | return rangeCheck (pre->ar, pre->expr, post->ar, post->expr); | |
553 | } | |
554 | ||
555 | bool arithType_canResolve (arithType ar1, arithType ar2) | |
556 | { | |
557 | switch (ar1) | |
558 | { | |
559 | case GTE: | |
560 | case GT: | |
561 | if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) ) | |
562 | { | |
563 | return TRUE; | |
564 | } | |
565 | break; | |
566 | ||
567 | case EQ: | |
568 | if (ar2 == EQ) | |
569 | return TRUE; | |
570 | break; | |
571 | ||
572 | case LT: | |
573 | case LTE: | |
574 | // llassert(FALSE); | |
575 | if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) ) | |
576 | return TRUE; | |
577 | default: | |
578 | return FALSE; | |
579 | } | |
580 | return FALSE; | |
581 | } | |
582 | ||
90bc41f7 | 583 | /* We look for constraint which are tautologies */ |
584 | ||
616915dd | 585 | bool constraint_isAlwaysTrue (constraint c) |
586 | { | |
587 | constraintExpr l, r; | |
9280addf | 588 | bool lHasConstant, rHasConstant; |
589 | int lConstant, rConstant; | |
590 | ||
616915dd | 591 | l = c->lexpr; |
592 | r = c->expr; | |
90bc41f7 | 593 | |
594 | DPRINTF(( message("constraint_IsAlwaysTrue:examining %s", constraint_print(c) ) )); | |
9280addf | 595 | |
616915dd | 596 | if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) ) |
597 | { | |
598 | int cmp; | |
599 | cmp = constraintExpr_compare (l, r); | |
600 | switch (c->ar) | |
601 | { | |
602 | case EQ: | |
603 | return (cmp == 0); | |
604 | case GT: | |
605 | return (cmp > 0); | |
606 | case GTE: | |
607 | return (cmp >= 0); | |
608 | case LTE: | |
609 | return (cmp <= 0); | |
610 | case LT: | |
611 | return (cmp < 0); | |
612 | ||
613 | default: | |
9280addf | 614 | BADEXIT; |
615 | break; | |
616 | } | |
617 | } | |
618 | ||
619 | if (constraintExpr_similar (l,r) ) | |
620 | { | |
621 | switch (c->ar) | |
622 | { | |
623 | case EQ: | |
624 | case GTE: | |
625 | case LTE: | |
626 | return TRUE; | |
627 | ||
628 | case GT: | |
629 | case LT: | |
630 | break; | |
631 | default: | |
632 | BADEXIT; | |
616915dd | 633 | break; |
634 | } | |
635 | } | |
9280addf | 636 | |
637 | l = constraintExpr_copy (c->lexpr); | |
638 | r = constraintExpr_copy (c->expr); | |
639 | ||
640 | // l = constraintExpr_propagateConstants (l, &lHasConstant, &lConstant); | |
641 | r = constraintExpr_propagateConstants (r, &rHasConstant, &rConstant); | |
642 | ||
90bc41f7 | 643 | if (constraintExpr_similar (l,r) && (rHasConstant ) ) |
9280addf | 644 | { |
645 | DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) )); | |
90bc41f7 | 646 | DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is %d", rConstant ) )); |
647 | switch (c->ar) | |
9280addf | 648 | { |
90bc41f7 | 649 | case EQ: |
650 | return (rConstant == 0); | |
651 | case LT: | |
652 | return (rConstant > 0); | |
653 | case LTE: | |
654 | return (rConstant >= 0); | |
655 | case GTE: | |
656 | return (rConstant <= 0); | |
657 | case GT: | |
658 | return (rConstant < 0); | |
659 | ||
660 | default: | |
661 | BADEXIT; | |
662 | break; | |
9280addf | 663 | } |
9280addf | 664 | } |
90bc41f7 | 665 | else |
666 | { | |
667 | DPRINTF(( message("Constraint %s is not always true", constraint_print(c) ) )); | |
668 | return FALSE; | |
669 | } | |
9280addf | 670 | |
671 | BADEXIT; | |
616915dd | 672 | } |
673 | ||
674 | bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2) | |
675 | ||
676 | { | |
677 | DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) )); | |
678 | ||
679 | if (! arithType_canResolve (ar1, ar2) ) | |
680 | return FALSE; | |
681 | ||
682 | switch (ar1) | |
683 | { | |
684 | case GTE: | |
685 | if (constraintExpr_similar (expr1, expr2) ) | |
686 | return TRUE; | |
687 | case GT: | |
688 | if (! (constraintExpr_canGetValue (expr1) && | |
689 | constraintExpr_canGetValue (expr2) ) ) | |
690 | { | |
90bc41f7 | 691 | constraintExpr e1, e2; |
692 | bool p1, p2; | |
693 | int const1, const2; | |
694 | ||
695 | e1 = constraintExpr_propagateConstants (expr1, &p1, &const1); | |
696 | ||
697 | e2 = constraintExpr_propagateConstants (expr2, &p2, &const2); | |
698 | ||
699 | if (p1 && p2) | |
700 | if (const1 <= const2) | |
701 | if (constraintExpr_similar (e1, e2) ) | |
702 | return TRUE; | |
703 | ||
616915dd | 704 | DPRINTF( ("Can't Get value")); |
705 | return FALSE; | |
706 | } | |
707 | ||
708 | if (constraintExpr_compare (expr2, expr1) >= 0) | |
709 | return TRUE; | |
710 | ||
711 | return FALSE; | |
712 | case EQ: | |
713 | if (constraintExpr_similar (expr1, expr2) ) | |
714 | return TRUE; | |
715 | ||
716 | return FALSE; | |
717 | case LTE: | |
718 | if (constraintExpr_similar (expr1, expr2) ) | |
719 | return TRUE; | |
720 | case LT: | |
721 | if (! (constraintExpr_canGetValue (expr1) && | |
722 | constraintExpr_canGetValue (expr2) ) ) | |
723 | { | |
90bc41f7 | 724 | constraintExpr e1, e2; |
725 | bool p1, p2; | |
726 | int const1, const2; | |
727 | ||
728 | e1 = constraintExpr_propagateConstants (expr1, &p1, &const1); | |
729 | ||
730 | e2 = constraintExpr_propagateConstants (expr2, &p2, &const2); | |
731 | ||
732 | if (p1 && p2) | |
733 | if (const1 >= const2) | |
734 | if (constraintExpr_similar (e1, e2) ) | |
735 | return TRUE; | |
736 | ||
616915dd | 737 | DPRINTF( ("Can't Get value")); |
738 | return FALSE; | |
739 | } | |
740 | ||
741 | if (constraintExpr_compare (expr2, expr1) <= 0) | |
742 | return TRUE; | |
743 | ||
744 | return FALSE; | |
745 | ||
746 | default: | |
747 | llcontbug((message("Unhandled case in switch: %s", arithType_print(ar1) ) ) ); | |
748 | } | |
749 | BADEXIT; | |
750 | return FALSE; | |
751 | } | |
752 | ||
753 | ||
754 | constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new) | |
755 | { | |
756 | DPRINTF (("Doing replace for lexpr") ); | |
757 | c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new); | |
758 | DPRINTF (("Doing replace for expr") ); | |
759 | c->expr = constraintExpr_searchandreplace (c->expr, old, new); | |
760 | return c; | |
761 | } | |
762 | ||
763 | bool constraint_search (constraint c, constraintExpr old) | |
764 | { | |
765 | bool ret; | |
766 | ret = FALSE; | |
767 | ||
768 | ret = constraintExpr_search (c->lexpr, old); | |
769 | ret = ret || constraintExpr_search (c->expr, old); | |
770 | return ret; | |
771 | } | |
772 | ||
773 | //adjust file locs and stuff | |
774 | constraint constraint_adjust (constraint substitute, constraint old) | |
775 | { | |
776 | fileloc loc1, loc2, loc3; | |
777 | ||
778 | DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute), | |
779 | constraint_print(old)) | |
780 | )); | |
781 | ||
782 | loc1 = constraint_getFileloc (old); | |
783 | ||
784 | loc2 = constraintExpr_getFileloc (substitute->lexpr); | |
785 | ||
786 | loc3 = constraintExpr_getFileloc (substitute->expr); | |
787 | ||
788 | ||
789 | // special case of an equality that "contains itself" | |
790 | if (constraintExpr_search (substitute->expr, substitute->lexpr) ) | |
791 | if (fileloc_closer (loc1, loc3, loc2)) | |
792 | { | |
793 | constraintExpr temp; | |
794 | DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) ) | |
795 | )); | |
796 | temp = substitute->lexpr; | |
797 | substitute->lexpr = substitute->expr; | |
798 | substitute->expr = temp; | |
799 | substitute = constraint_simplify(substitute); | |
800 | } | |
801 | ||
802 | return substitute; | |
803 | ||
804 | } | |
805 | ||
90bc41f7 | 806 | /* If function preforms substitutes based on inequality |
807 | ||
808 | It uses the rule x >= y && b < y ===> x >= b + 1 | |
809 | ||
810 | Warning this is sound but throws out information | |
811 | */ | |
616915dd | 812 | constraint inequalitySubstitute (constraint c, constraintList p) |
813 | { | |
814 | if (c->ar != GTE) | |
815 | return c; | |
816 | ||
817 | constraintList_elements (p, el) | |
818 | { | |
819 | if ( el->ar == LT) | |
820 | // if (!constraint_conflict (c, el) ) | |
821 | { | |
822 | constraint temp; | |
90bc41f7 | 823 | constraintExpr temp2; |
824 | ||
616915dd | 825 | temp = constraint_copy(el); |
826 | ||
827 | // temp = constraint_adjust(temp, c); | |
828 | ||
90bc41f7 | 829 | if (constraintExpr_same (el->expr, c->expr) ) |
616915dd | 830 | { |
90bc41f7 | 831 | DPRINTF((message ("inequalitySubstitute Replacing %s in %s with %s", |
616915dd | 832 | constraintExpr_print (c->expr), |
833 | constraint_print (c), | |
834 | constraintExpr_print (el->expr) ) | |
835 | )); | |
90bc41f7 | 836 | temp2 = constraintExpr_copy (el->lexpr); |
837 | c->expr = constraintExpr_makeIncConstraintExpr (temp2); | |
616915dd | 838 | } |
839 | ||
840 | } | |
841 | } | |
842 | end_constraintList_elements; | |
843 | ||
844 | c = constraint_simplify(c); | |
845 | return c; | |
846 | } | |
847 | ||
90bc41f7 | 848 | /* This function performs substitutions based on the rule: |
849 | for a constraint of the form expr1 >= expr2; a < b => | |
850 | a = b -1 for all a in expr1. This will work in most cases. | |
851 | ||
852 | Like inequalitySubstitute we're throwing away some information | |
853 | */ | |
854 | ||
855 | constraint inequalitySubstituteUnsound (constraint c, constraintList p) | |
856 | { | |
857 | DPRINTF (( message ("Doing inequalitySubstituteUnsound " ) )); | |
858 | ||
859 | if (c->ar != GTE) | |
860 | return c; | |
861 | ||
862 | constraintList_elements (p, el) | |
863 | { | |
864 | DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s", constraint_print(el), constraint_print(c) ) )); | |
865 | if ( ( el->ar == LTE) || (el->ar == LT) ) | |
866 | // if (!constraint_conflict (c, el) ) | |
867 | { | |
868 | constraint temp; | |
869 | constraintExpr temp2; | |
870 | ||
871 | temp = constraint_copy(el); | |
872 | ||
873 | // temp = constraint_adjust(temp, c); | |
874 | temp2 = constraintExpr_copy (el->expr); | |
875 | ||
876 | if (el->ar == LT) | |
877 | temp2 = constraintExpr_makeDecConstraintExpr (temp2); | |
878 | ||
879 | DPRINTF((message ("Replacing %s in %s with %s", | |
880 | constraintExpr_print (el->lexpr), | |
881 | constraintExpr_print (c->lexpr), | |
882 | constraintExpr_print (temp2) ) )); | |
883 | ||
884 | c->lexpr = constraintExpr_searchandreplace (c->lexpr, el->lexpr, temp2); | |
885 | } | |
886 | } | |
887 | end_constraintList_elements; | |
888 | ||
889 | c = constraint_simplify(c); | |
890 | return c; | |
891 | } | |
892 | ||
616915dd | 893 | constraint substitute (constraint c, constraintList p) |
894 | { | |
90bc41f7 | 895 | constraint ret; |
896 | ||
897 | ret = constraint_copy(c); | |
616915dd | 898 | constraintList_elements (p, el) |
899 | { | |
900 | if ( el->ar == EQ) | |
90bc41f7 | 901 | if (!constraint_conflict (ret, el) ) |
616915dd | 902 | |
903 | { | |
904 | constraint temp; | |
905 | temp = constraint_copy(el); | |
906 | ||
90bc41f7 | 907 | temp = constraint_adjust(temp, ret); |
616915dd | 908 | |
470b7798 | 909 | DPRINTF((message ("Substituting %s in the constraint %s", |
90bc41f7 | 910 | constraint_print (temp), constraint_print (ret) |
616915dd | 911 | ) ) ); |
912 | ||
913 | ||
90bc41f7 | 914 | ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr); |
915 | DPRINTF(( message ("The new constraint is %s", constraint_print (ret) ) )); | |
616915dd | 916 | } |
917 | } | |
918 | end_constraintList_elements; | |
919 | ||
90bc41f7 | 920 | ret = constraint_simplify(ret); |
921 | return ret; | |
616915dd | 922 | } |
923 | ||
c3e695ff | 924 | /* we try to do substitutions on each constraint in target using the constraint in sublist*/ |
925 | ||
926 | constraintList constraintList_substitute (constraintList target, constraintList subList) | |
927 | { | |
928 | ||
929 | constraintList ret; | |
930 | ||
931 | ret = constraintList_makeNew(); | |
932 | ||
933 | constraintList_elements(target, el) | |
934 | { | |
935 | el = substitute(el, subList); | |
936 | ret = constraintList_add (ret, el); | |
937 | } | |
938 | end_constraintList_elements; | |
939 | #warning mem leak | |
940 | return ret; | |
941 | } | |
942 | ||
943 | constraint constraint_solveWithFlag (constraint c, bool *b) | |
944 | { | |
945 | #warning abstraction | |
946 | *b = FALSE; | |
947 | if (c->lexpr->kind == binaryexpr) | |
948 | { | |
949 | *b = TRUE; | |
950 | DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) ); | |
951 | c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr); | |
952 | DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) ); | |
953 | } | |
954 | return c; | |
955 | } | |
616915dd | 956 | |
957 | constraint constraint_solve (constraint c) | |
958 | { | |
959 | DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) ); | |
960 | c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr); | |
961 | DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) ); | |
962 | ||
963 | return c; | |
964 | } | |
965 | ||
966 | static arithType flipAr (arithType ar) | |
967 | { | |
968 | switch (ar) | |
969 | { | |
970 | case LT: | |
971 | return GT; | |
972 | case LTE: | |
973 | return GTE; | |
974 | case EQ: | |
975 | return EQ; | |
976 | case GT: | |
977 | return LT; | |
978 | case GTE: | |
979 | return LTE; | |
980 | default: | |
981 | llcontbug (("unexpected value: case not handled")); | |
982 | } | |
983 | BADEXIT; | |
984 | } | |
985 | ||
986 | static constraint constraint_swapLeftRight (constraint c) | |
987 | { | |
988 | constraintExpr temp; | |
989 | c->ar = flipAr (c->ar); | |
990 | temp = c->lexpr; | |
991 | c->lexpr = c->expr; | |
992 | c->expr = temp; | |
993 | DPRINTF(("Swaped left and right sides of constraint")); | |
994 | return c; | |
995 | } | |
996 | ||
c3e695ff | 997 | |
998 | ||
616915dd | 999 | constraint constraint_simplify (constraint c) |
1000 | { | |
1001 | c->lexpr = constraintExpr_simplify (c->lexpr); | |
1002 | c->expr = constraintExpr_simplify (c->expr); | |
616915dd | 1003 | |
c3e695ff | 1004 | #warning check this 5/11/01 |
1005 | ||
1006 | if (c->lexpr->kind == binaryexpr) | |
1007 | { | |
1008 | c = constraint_solve (c); | |
1009 | ||
1010 | c->lexpr = constraintExpr_simplify (c->lexpr); | |
1011 | c->expr = constraintExpr_simplify (c->expr); | |
1012 | } | |
1013 | ||
616915dd | 1014 | if (constraintExpr_isLit(c->lexpr) && (!constraintExpr_isLit(c->expr) ) ) |
1015 | { | |
1016 | c = constraint_swapLeftRight(c); | |
1017 | /*I don't think this will be an infinate loop*/ | |
1018 | constraint_simplify(c); | |
1019 | } | |
1020 | return c; | |
1021 | } | |
1022 | ||
1023 | ||
1024 | ||
1025 | ||
1026 | /* returns true if fileloc for term1 is closer to file for term2 than term3*/ | |
1027 | ||
1028 | bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3) | |
1029 | { | |
c3e695ff | 1030 | |
1031 | if (!fileloc_isDefined (loc1) ) | |
1032 | return FALSE; | |
1033 | ||
1034 | if (!fileloc_isDefined (loc2) ) | |
1035 | return FALSE; | |
1036 | ||
1037 | if (!fileloc_isDefined (loc3) ) | |
1038 | return TRUE; | |
1039 | ||
1040 | ||
1041 | ||
1042 | ||
1043 | if (fileloc_equal (loc2, loc3) ) | |
1044 | return FALSE; | |
1045 | ||
1046 | if (fileloc_equal (loc1, loc2) ) | |
1047 | return TRUE; | |
1048 | ||
1049 | if (fileloc_equal (loc1, loc3) ) | |
1050 | return FALSE; | |
1051 | ||
616915dd | 1052 | if ( fileloc_lessthan (loc1, loc2) ) |
1053 | { | |
1054 | if (fileloc_lessthan (loc2, loc3) ) | |
1055 | { | |
1056 | llassert (fileloc_lessthan (loc1, loc3) ); | |
1057 | return TRUE; | |
1058 | } | |
1059 | else | |
1060 | { | |
1061 | return FALSE; | |
1062 | } | |
1063 | } | |
1064 | ||
1065 | if ( !fileloc_lessthan (loc1, loc2) ) | |
1066 | { | |
1067 | if (!fileloc_lessthan (loc2, loc3) ) | |
1068 | { | |
1069 | llassert (!fileloc_lessthan (loc1, loc3) ); | |
1070 | return TRUE; | |
1071 | } | |
1072 | else | |
1073 | { | |
1074 | return FALSE; | |
1075 | } | |
1076 | } | |
1077 | ||
1078 | llassert(FALSE); | |
1079 | return FALSE; | |
1080 | } | |
1081 | ||
1082 |