]> andersk Git - splint.git/blame - src/constraintResolve.c
Making changes to try to support loops.
[splint.git] / src / constraintResolve.c
CommitLineData
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 25constraintList reflectChanges (constraintList pre2, constraintList post1);
26constraint substitute (constraint c, constraintList p);
27constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
28bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2);
29bool satifies (constraint pre, constraint post);
30bool resolve (constraint c, constraintList p);
31constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
32constraint constraint_simplify (constraint c);
361091cc 33
754746a0 34constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);
35
36constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
37
38constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
f5ac53de 39constraint inequalitySubstitute (constraint c, constraintList p);
754746a0 40
41/*********************************************/
42
43
44constraintList 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 83constraintList 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 107constraintList 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 131void 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
191constraintList 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 213constraintList 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 247constraintList 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
272bool 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 291void 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 304bool 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.
323constraintList 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
340bool 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 */
358bool 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 376bool 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 404bool 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 439bool 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 493constraint 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 502bool 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 513constraint 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 545constraint 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 578constraint 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 606constraint 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 615static 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
635static 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 646constraint 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
670bool 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
This page took 0.800868 seconds and 5 git commands to generate.