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