]>
Commit | Line | Data |
---|---|---|
361091cc | 1 | /* |
754746a0 | 2 | * |
361091cc | 3 | ** constraintResolve.c |
4 | */ | |
5 | ||
f5ac53de | 6 | //#define DEBUGPRINT 1 |
7 | ||
361091cc | 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" | |
93307a76 | 17 | //# include "exprData.i" |
361091cc | 18 | |
92c4a786 | 19 | #include "constraintExpr.h" |
361091cc | 20 | |
f5ac53de | 21 | |
22 | ||
ef2aa32a | 23 | |
24 | ||
92c4a786 | 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); | |
361091cc | 33 | |
754746a0 | 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); | |
f5ac53de | 39 | constraint inequalitySubstitute (constraint c, constraintList p); |
754746a0 | 40 | |
41 | /*********************************************/ | |
42 | ||
43 | ||
44 | constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2) | |
45 | { | |
46 | constraintList ret; | |
47 | constraintList temp; | |
48 | ret = constraintList_new(); | |
49 | ||
50 | ret = reflectChangesEnsures (list1, list2); | |
51 | ret = constraintList_fixConflicts (ret, list2); | |
52 | ret = constraintList_subsumeEnsures (ret, list2); | |
53 | list2 = constraintList_subsumeEnsures (list2, ret); | |
54 | temp = constraintList_copy(list2); | |
55 | ||
56 | temp = constraintList_addList (temp, ret); | |
57 | return temp; | |
58 | //ret = constraintList_addList (ret, list2); | |
59 | //return ret; | |
60 | } | |
61 | ||
34f0c5e7 | 62 | |
63 | /* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */ | |
64 | /* { */ | |
65 | ||
66 | /* constraintList ret; */ | |
67 | /* constraintList temp; */ | |
68 | /* ret = constraintList_new(); */ | |
69 | ||
70 | /* ret = reflectChangesEnsures (list1, list2); */ | |
71 | /* ret = constraintList_fixConflicts (ret, list2); */ | |
72 | /* ret = constraintList_subsumeEnsures (ret, list2); */ | |
73 | /* list2 = constraintList_subsumeEnsures (list2, ret); */ | |
74 | /* temp = constraintList_copy(list2); */ | |
75 | ||
76 | /* temp = constraintList_addList (temp, ret); */ | |
77 | /* return temp; */ | |
78 | /* //ret = constraintList_addList (ret, list2); */ | |
79 | /* //return ret; */ | |
80 | /* } */ | |
81 | ||
82 | ||
93307a76 | 83 | constraintList checkCall (exprNode fcn, exprNodeList arglist) |
84 | { | |
85 | constraintList preconditions; | |
86 | uentry temp; | |
87 | DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) ); | |
88 | ||
89 | temp = exprNode_getUentry (fcn); | |
90 | ||
91 | preconditions = uentry_getFcnPreconditions (temp); | |
92 | ||
93 | if (preconditions) | |
94 | { | |
95 | preconditions = constraintList_copy(preconditions); | |
ef2aa32a | 96 | preconditions= constraintList_togglePost (preconditions); |
97 | preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist); | |
93307a76 | 98 | } |
99 | else | |
100 | { | |
101 | preconditions = constraintList_new(); | |
102 | } | |
103 | ||
104 | return preconditions; | |
105 | } | |
106 | ||
ef2aa32a | 107 | constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall) |
108 | { | |
109 | constraintList postconditions; | |
110 | uentry temp; | |
111 | DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) ); | |
112 | ||
113 | temp = exprNode_getUentry (fcn); | |
114 | ||
115 | postconditions = uentry_getFcnPostconditions (temp); | |
116 | ||
117 | if (postconditions) | |
118 | { | |
119 | postconditions = constraintList_copy(postconditions); | |
120 | postconditions = constraintList_doFixResult (postconditions, fcnCall); | |
121 | postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist); | |
122 | } | |
123 | else | |
124 | { | |
125 | postconditions = constraintList_new(); | |
126 | } | |
127 | ||
128 | return postconditions; | |
129 | } | |
130 | ||
92c4a786 | 131 | void mergeResolve (exprNode parent, exprNode child1, exprNode child2) |
361091cc | 132 | { |
92c4a786 | 133 | constraintList temp; |
754746a0 | 134 | |
93307a76 | 135 | DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) ))); |
754746a0 | 136 | |
93307a76 | 137 | DPRINTF( (message (" children: %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) ); |
754746a0 | 138 | |
139 | if (exprNode_isError (child1) || exprNode_isError(child2) ) | |
92c4a786 | 140 | { |
141 | if (exprNode_isError (child1) && !exprNode_isError(child2) ) | |
142 | { | |
143 | parent->requiresConstraints = constraintList_copy (child2->requiresConstraints); | |
144 | parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints); | |
93307a76 | 145 | DPRINTF((message ("Copied child constraints: pre: %s and post: %s", |
92c4a786 | 146 | constraintList_print( child2->requiresConstraints), |
147 | constraintList_print (child2->ensuresConstraints) | |
148 | ) | |
149 | )); | |
150 | return; | |
151 | } | |
152 | else | |
153 | { | |
154 | llassert(exprNode_isError(child2) ); | |
155 | parent->requiresConstraints = constraintList_new(); | |
156 | parent->ensuresConstraints = constraintList_new(); | |
157 | return; | |
158 | } | |
159 | } | |
361091cc | 160 | |
92c4a786 | 161 | llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) ); |
162 | ||
93307a76 | 163 | DPRINTF( (message ("Child constraints are %s %s and %s %s", |
92c4a786 | 164 | constraintList_print (child1->requiresConstraints), |
165 | constraintList_print (child1->ensuresConstraints), | |
166 | constraintList_print (child2->requiresConstraints), | |
167 | constraintList_print (child2->ensuresConstraints) | |
168 | ) ) ); | |
169 | ||
170 | parent->requiresConstraints = constraintList_new(); | |
171 | parent->ensuresConstraints = constraintList_new(); | |
361091cc | 172 | |
92c4a786 | 173 | parent->requiresConstraints = constraintList_copy (child1->requiresConstraints); |
174 | ||
175 | temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints); | |
176 | parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp); | |
361091cc | 177 | |
754746a0 | 178 | parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints, |
179 | child2->ensuresConstraints); | |
92c4a786 | 180 | |
93307a76 | 181 | DPRINTF( (message ("Parent constraints are %s and %s ", |
92c4a786 | 182 | constraintList_print (parent->requiresConstraints), |
183 | constraintList_print (parent->ensuresConstraints) | |
184 | ) ) ); | |
185 | ||
361091cc | 186 | } |
187 | ||
361091cc | 188 | |
92c4a786 | 189 | |
754746a0 | 190 | |
191 | constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2) | |
192 | { | |
193 | constraintList ret; | |
194 | ret = constraintList_new(); | |
195 | constraintList_elements (list1, el) | |
196 | { | |
197 | ||
93307a76 | 198 | DPRINTF ((message ("Examining %s", constraint_print (el) ) ) ); |
754746a0 | 199 | if (!resolve (el, list2) ) |
200 | { | |
201 | ret = constraintList_add (ret, el); | |
202 | } | |
203 | else | |
204 | { | |
93307a76 | 205 | DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) ); |
754746a0 | 206 | } |
207 | } end_constraintList_elements; | |
208 | ||
209 | return ret; | |
210 | } | |
211 | ||
212 | ||
92c4a786 | 213 | constraintList reflectChanges (constraintList pre2, constraintList post1) |
214 | { | |
215 | ||
216 | constraintList ret; | |
217 | constraint temp; | |
218 | ret = constraintList_new(); | |
ef2aa32a | 219 | DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) ))); |
220 | ||
92c4a786 | 221 | constraintList_elements (pre2, el) |
361091cc | 222 | { |
92c4a786 | 223 | if (!resolve (el, post1) ) |
224 | { | |
225 | temp = substitute (el, post1); | |
754746a0 | 226 | if (!resolve (temp, post1) ) |
34f0c5e7 | 227 | { |
228 | // try inequality substitution | |
229 | constraint temp2; | |
230 | ||
231 | // the inequality substitution may cause us to lose information | |
232 | //so we don't want to store the result but we do it anyway | |
233 | temp2 = constraint_copy (temp); | |
234 | temp2 = inequalitySubstitute (temp, post1); | |
235 | if (!resolve (temp2, post1) ) | |
236 | ret = constraintList_add (ret, temp2); | |
237 | } | |
92c4a786 | 238 | } |
239 | } end_constraintList_elements; | |
361091cc | 240 | |
ef2aa32a | 241 | DPRINTF((message ("reflectChanges: returning %s", constraintList_print(ret) ) ) ); |
92c4a786 | 242 | return ret; |
361091cc | 243 | } |
244 | ||
361091cc | 245 | |
361091cc | 246 | |
92c4a786 | 247 | constraintList reflectChangesEnsures (constraintList pre2, constraintList post1) |
248 | { | |
249 | constraintList ret; | |
250 | constraint temp; | |
251 | ret = constraintList_new(); | |
252 | constraintList_elements (pre2, el) | |
361091cc | 253 | { |
92c4a786 | 254 | if (!resolve (el, post1) ) |
255 | { | |
256 | temp = substitute (el, post1); | |
754746a0 | 257 | llassert (temp != NULL); |
258 | ||
259 | if (!resolve (temp, post1) ) | |
92c4a786 | 260 | ret = constraintList_add (ret, temp); |
261 | } | |
754746a0 | 262 | else |
263 | { | |
93307a76 | 264 | DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) ); |
754746a0 | 265 | } |
92c4a786 | 266 | } end_constraintList_elements; |
bf92e32c | 267 | |
92c4a786 | 268 | return ret; |
361091cc | 269 | } |
270 | ||
92c4a786 | 271 | |
272 | bool constraint_conflict (constraint c1, constraint c2) | |
361091cc | 273 | { |
274 | ||
92c4a786 | 275 | if (constraintExpr_similar(c1->lexpr, c2->lexpr) ) |
bf92e32c | 276 | { |
754746a0 | 277 | if (c1->ar == EQ) |
278 | if (c1->ar == c2->ar) | |
279 | { | |
93307a76 | 280 | DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) ); |
754746a0 | 281 | return TRUE; |
282 | } | |
92c4a786 | 283 | } |
bf92e32c | 284 | |
754746a0 | 285 | DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) ); |
361091cc | 286 | |
92c4a786 | 287 | return FALSE; |
361091cc | 288 | |
361091cc | 289 | } |
290 | ||
92c4a786 | 291 | void constraint_fixConflict (constraint good, constraint conflicting) |
361091cc | 292 | { |
92c4a786 | 293 | constraint temp; |
294 | if (conflicting->ar ==EQ ) | |
361091cc | 295 | { |
92c4a786 | 296 | good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr); |
297 | temp = constraint_simplify (good); | |
298 | constraint_overWrite (good, temp); | |
361091cc | 299 | } |
300 | ||
361091cc | 301 | |
361091cc | 302 | } |
303 | ||
92c4a786 | 304 | bool conflict (constraint c, constraintList list) |
361091cc | 305 | { |
361091cc | 306 | |
92c4a786 | 307 | constraintList_elements (list, el) |
308 | { | |
309 | if ( constraint_conflict(el, c) ) | |
310 | { | |
311 | constraint_fixConflict (el, c); | |
312 | return TRUE; | |
313 | } | |
314 | } end_constraintList_elements; | |
361091cc | 315 | |
92c4a786 | 316 | return FALSE; |
317 | ||
361091cc | 318 | |
361091cc | 319 | } |
320 | ||
92c4a786 | 321 | //check if constraint in list1 and conflict with constraints in List2. If so we |
322 | //remove form list1 and (optionally) change list2. | |
323 | constraintList constraintList_fixConflicts (constraintList list1, constraintList list2) | |
6364363c | 324 | { |
92c4a786 | 325 | constraintList ret; |
326 | ret = constraintList_new(); | |
327 | constraintList_elements (list1, el) | |
328 | { | |
329 | if (! conflict (el, list2) ) | |
330 | { | |
331 | ret = constraintList_add (ret, el); | |
332 | } | |
333 | } end_constraintList_elements; | |
6364363c | 334 | |
92c4a786 | 335 | return ret; |
336 | ||
337 | ||
361091cc | 338 | } |
339 | ||
340 | bool resolve (constraint c, constraintList p) | |
341 | { | |
342 | constraintList_elements (p, el) | |
343 | { | |
344 | if ( satifies (c, el) ) | |
345 | { | |
93307a76 | 346 | DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) ); |
361091cc | 347 | return TRUE; |
348 | } | |
ef2aa32a | 349 | DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) ); |
361091cc | 350 | } |
351 | end_constraintList_elements; | |
754746a0 | 352 | DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) )); |
361091cc | 353 | return FALSE; |
354 | } | |
355 | ||
bf92e32c | 356 | |
92c4a786 | 357 | /*returns true if cosntraint post satifies cosntriant pre */ |
358 | bool satifies (constraint pre, constraint post) | |
bf92e32c | 359 | { |
ef2aa32a | 360 | if (constraint_isAlwaysTrue (pre) ) |
361 | return TRUE; | |
362 | ||
92c4a786 | 363 | if (!constraintExpr_similar (pre->lexpr, post->lexpr) ) |
bf92e32c | 364 | { |
92c4a786 | 365 | return FALSE; |
366 | } | |
367 | if (post->expr == NULL) | |
368 | { | |
369 | llassert(FALSE); | |
370 | return FALSE; | |
bf92e32c | 371 | } |
92c4a786 | 372 | |
373 | return rangeCheck (pre->ar, pre->expr, post->ar, post->expr); | |
bf92e32c | 374 | } |
375 | ||
754746a0 | 376 | bool arithType_canResolve (arithType ar1, arithType ar2) |
377 | { | |
378 | switch (ar1) | |
379 | { | |
380 | case GTE: | |
381 | case GT: | |
382 | if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) ) | |
383 | { | |
384 | return TRUE; | |
385 | } | |
386 | break; | |
387 | ||
388 | case EQ: | |
389 | if (ar2 == EQ) | |
390 | return TRUE; | |
391 | break; | |
392 | ||
393 | case LT: | |
394 | case LTE: | |
34f0c5e7 | 395 | // llassert(FALSE); |
754746a0 | 396 | if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) ) |
397 | return TRUE; | |
ef2aa32a | 398 | default: |
399 | return FALSE; | |
754746a0 | 400 | } |
401 | return FALSE; | |
402 | } | |
92c4a786 | 403 | |
ef2aa32a | 404 | bool constraint_isAlwaysTrue (constraint c) |
405 | { | |
406 | constraintExpr l, r; | |
407 | l = c->lexpr; | |
408 | r = c->expr; | |
409 | ||
410 | if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) ) | |
411 | { | |
412 | int cmp; | |
413 | cmp = constraintExpr_compare (l, r); | |
414 | switch (c->ar) | |
415 | { | |
416 | case EQ: | |
417 | return (cmp == 0); | |
418 | case GT: | |
419 | return (cmp > 0); | |
420 | case GTE: | |
421 | return (cmp >= 0); | |
422 | case LTE: | |
423 | return (cmp <= 0); | |
424 | case LT: | |
425 | return (cmp < 0); | |
426 | ||
427 | default: | |
428 | llassert(FALSE); | |
429 | break; | |
430 | } | |
431 | } | |
432 | else | |
433 | { | |
434 | return FALSE; | |
435 | } | |
436 | BADEXIT; | |
437 | } | |
438 | ||
92c4a786 | 439 | bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2) |
440 | ||
bf92e32c | 441 | { |
754746a0 | 442 | DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) )); |
443 | ||
444 | if (! arithType_canResolve (ar1, ar2) ) | |
445 | return FALSE; | |
446 | ||
92c4a786 | 447 | switch (ar1) |
448 | { | |
449 | case GTE: | |
ef2aa32a | 450 | if (constraintExpr_similar (expr1, expr2) ) |
451 | return TRUE; | |
92c4a786 | 452 | case GT: |
754746a0 | 453 | if (! (constraintExpr_canGetValue (expr1) && |
454 | constraintExpr_canGetValue (expr2) ) ) | |
455 | { | |
456 | DPRINTF( ("Can't Get value")); | |
457 | return FALSE; | |
458 | } | |
459 | ||
460 | if (constraintExpr_compare (expr2, expr1) >= 0) | |
461 | return TRUE; | |
462 | ||
463 | return FALSE; | |
464 | case EQ: | |
465 | if (constraintExpr_similar (expr1, expr2) ) | |
466 | return TRUE; | |
467 | ||
468 | return FALSE; | |
ef2aa32a | 469 | case LTE: |
470 | if (constraintExpr_similar (expr1, expr2) ) | |
471 | return TRUE; | |
472 | case LT: | |
473 | if (! (constraintExpr_canGetValue (expr1) && | |
474 | constraintExpr_canGetValue (expr2) ) ) | |
475 | { | |
476 | DPRINTF( ("Can't Get value")); | |
477 | return FALSE; | |
478 | } | |
479 | ||
480 | if (constraintExpr_compare (expr2, expr1) <= 0) | |
481 | return TRUE; | |
482 | ||
483 | return FALSE; | |
754746a0 | 484 | |
92c4a786 | 485 | default: |
ef2aa32a | 486 | llcontbug((message("Unhandled case in switch: %s", arithType_print(ar1) ) ) ); |
92c4a786 | 487 | } |
ef2aa32a | 488 | BADEXIT; |
92c4a786 | 489 | return FALSE; |
490 | } | |
bf92e32c | 491 | |
754746a0 | 492 | |
92c4a786 | 493 | constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new) |
494 | { | |
754746a0 | 495 | DPRINTF (("Doing replace for lexpr") ); |
92c4a786 | 496 | c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new); |
754746a0 | 497 | DPRINTF (("Doing replace for expr") ); |
92c4a786 | 498 | c->expr = constraintExpr_searchandreplace (c->expr, old, new); |
499 | return c; | |
bf92e32c | 500 | } |
6364363c | 501 | |
754746a0 | 502 | bool constraint_search (constraint c, constraintExpr old) |
503 | { | |
504 | bool ret; | |
505 | ret = FALSE; | |
506 | ||
507 | ret = constraintExpr_search (c->lexpr, old); | |
508 | ret = ret || constraintExpr_search (c->expr, old); | |
509 | return ret; | |
510 | } | |
511 | ||
34f0c5e7 | 512 | //adjust file locs and stuff |
92c4a786 | 513 | constraint constraint_adjust (constraint substitute, constraint old) |
bf92e32c | 514 | { |
92c4a786 | 515 | fileloc loc1, loc2, loc3; |
6364363c | 516 | |
754746a0 | 517 | DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute), |
518 | constraint_print(old)) | |
519 | )); | |
520 | ||
92c4a786 | 521 | loc1 = constraint_getFileloc (old); |
6364363c | 522 | |
92c4a786 | 523 | loc2 = constraintExpr_getFileloc (substitute->lexpr); |
6364363c | 524 | |
92c4a786 | 525 | loc3 = constraintExpr_getFileloc (substitute->expr); |
6364363c | 526 | |
754746a0 | 527 | |
528 | // special case of an equality that "contains itself" | |
529 | if (constraintExpr_search (substitute->expr, substitute->lexpr) ) | |
530 | if (fileloc_closer (loc1, loc3, loc2)) | |
6364363c | 531 | { |
92c4a786 | 532 | constraintExpr temp; |
754746a0 | 533 | DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) ) |
534 | )); | |
92c4a786 | 535 | temp = substitute->lexpr; |
536 | substitute->lexpr = substitute->expr; | |
537 | substitute->expr = temp; | |
538 | substitute = constraint_simplify(substitute); | |
6364363c | 539 | } |
540 | ||
92c4a786 | 541 | return substitute; |
542 | ||
bf92e32c | 543 | } |
544 | ||
34f0c5e7 | 545 | constraint inequalitySubstitute (constraint c, constraintList p) |
546 | { | |
547 | if (c->ar != GTE) | |
548 | return c; | |
549 | ||
550 | constraintList_elements (p, el) | |
551 | { | |
552 | if ( el->ar == LT) | |
553 | // if (!constraint_conflict (c, el) ) | |
554 | { | |
555 | constraint temp; | |
556 | temp = constraint_copy(el); | |
557 | ||
558 | // temp = constraint_adjust(temp, c); | |
559 | ||
560 | if (constraintExpr_same (el->lexpr, c->expr) ) | |
561 | { | |
562 | DPRINTF((message ("Replacing %s in %s with %s", | |
563 | constraintExpr_print (c->expr), | |
564 | constraint_print (c), | |
565 | constraintExpr_print (el->expr) ) | |
566 | )); | |
567 | c->expr = constraintExpr_copy (el->expr); | |
568 | } | |
569 | ||
570 | } | |
571 | } | |
572 | end_constraintList_elements; | |
573 | ||
574 | c = constraint_simplify(c); | |
575 | return c; | |
576 | } | |
577 | ||
361091cc | 578 | constraint substitute (constraint c, constraintList p) |
579 | { | |
580 | constraintList_elements (p, el) | |
581 | { | |
92c4a786 | 582 | if ( el->ar == EQ) |
583 | if (!constraint_conflict (c, el) ) | |
584 | ||
585 | { | |
92c4a786 | 586 | constraint temp; |
587 | temp = constraint_copy(el); | |
588 | ||
589 | temp = constraint_adjust(temp, c); | |
754746a0 | 590 | |
591 | DPRINTF((message ("Substituting %s for %s", | |
592 | constraint_print (temp), constraint_print (c) | |
593 | ) ) ); | |
594 | ||
92c4a786 | 595 | |
754746a0 | 596 | c = constraint_searchandreplace (c, temp->lexpr, temp->expr); |
92c4a786 | 597 | } |
361091cc | 598 | } |
599 | end_constraintList_elements; | |
600 | ||
601 | c = constraint_simplify(c); | |
602 | return c; | |
603 | } | |
604 | ||
361091cc | 605 | |
92c4a786 | 606 | constraint constraint_solve (constraint c) |
6364363c | 607 | { |
754746a0 | 608 | DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) ); |
92c4a786 | 609 | c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr); |
754746a0 | 610 | DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) ); |
361091cc | 611 | |
92c4a786 | 612 | return c; |
361091cc | 613 | } |
614 | ||
ef2aa32a | 615 | static arithType flipAr (arithType ar) |
616 | { | |
617 | switch (ar) | |
618 | { | |
619 | case LT: | |
620 | return GT; | |
621 | case LTE: | |
622 | return GTE; | |
623 | case EQ: | |
624 | return EQ; | |
625 | case GT: | |
626 | return LT; | |
627 | case GTE: | |
628 | return LTE; | |
629 | default: | |
630 | llcontbug (("unexpected value: case not handled")); | |
631 | } | |
632 | BADEXIT; | |
633 | } | |
634 | ||
635 | static constraint constraint_swapLeftRight (constraint c) | |
636 | { | |
637 | constraintExpr temp; | |
638 | c->ar = flipAr (c->ar); | |
639 | temp = c->lexpr; | |
640 | c->lexpr = c->expr; | |
641 | c->expr = temp; | |
642 | DPRINTF(("Swaped left and right sides of constraint")); | |
643 | return c; | |
644 | } | |
361091cc | 645 | |
92c4a786 | 646 | constraint constraint_simplify (constraint c) |
361091cc | 647 | { |
92c4a786 | 648 | c->lexpr = constraintExpr_simplify (c->lexpr); |
649 | c->expr = constraintExpr_simplify (c->expr); | |
361091cc | 650 | |
92c4a786 | 651 | c = constraint_solve (c); |
754746a0 | 652 | |
92c4a786 | 653 | c->lexpr = constraintExpr_simplify (c->lexpr); |
654 | c->expr = constraintExpr_simplify (c->expr); | |
ef2aa32a | 655 | |
656 | if (constraintExpr_isLit(c->lexpr) && (!constraintExpr_isLit(c->expr) ) ) | |
657 | { | |
658 | c = constraint_swapLeftRight(c); | |
659 | /*I don't think this will be an infinate loop*/ | |
660 | constraint_simplify(c); | |
661 | } | |
361091cc | 662 | return c; |
663 | } | |
664 | ||
665 | ||
361091cc | 666 | |
361091cc | 667 | |
92c4a786 | 668 | /* returns true if fileloc for term1 is closer to file for term2 than term3*/ |
669 | ||
670 | bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3) | |
361091cc | 671 | { |
92c4a786 | 672 | if ( fileloc_lessthan (loc1, loc2) ) |
6364363c | 673 | { |
92c4a786 | 674 | if (fileloc_lessthan (loc2, loc3) ) |
6364363c | 675 | { |
92c4a786 | 676 | llassert (fileloc_lessthan (loc1, loc3) ); |
677 | return TRUE; | |
6364363c | 678 | } |
679 | else | |
680 | { | |
92c4a786 | 681 | return FALSE; |
6364363c | 682 | } |
683 | } | |
684 | ||
92c4a786 | 685 | if ( !fileloc_lessthan (loc1, loc2) ) |
686 | { | |
687 | if (!fileloc_lessthan (loc2, loc3) ) | |
688 | { | |
689 | llassert (!fileloc_lessthan (loc1, loc3) ); | |
690 | return TRUE; | |
691 | } | |
692 | else | |
693 | { | |
694 | return FALSE; | |
695 | } | |
696 | } | |
361091cc | 697 | |
92c4a786 | 698 | llassert(FALSE); |
699 | return FALSE; | |
361091cc | 700 | } |
701 | ||
754746a0 | 702 |