]> andersk Git - splint.git/blame - src/constraintGeneration.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Prewinter break editing commit.
[splint.git] / src / constraintGeneration.c
CommitLineData
4cccc6ad 1
2/*
3** constraintList.c
4*/
5
f5ac53de 6//#define DEBUGPRINT 1
7
4cccc6ad 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
4cccc6ad 18# include "exprData.i"
f5ac53de 19//# include "exprDataQuite.i"
20
21#ifndef exprNode_isError
22#warning wtf
23# define exprNode_isError(e) ((e) == exprNode_undefined)
24#else
25#warning strange
26#endif
27
28#define myexprNode_isError(e) ((e) == exprNode_undefined)
29
30
4cccc6ad 31
34f0c5e7 32bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
4cccc6ad 33static bool exprNode_handleError( exprNode p_e);
34
361091cc 35//static cstring exprNode_findConstraints ( exprNode p_e);
4cccc6ad 36static bool exprNode_isMultiStatement(exprNode p_e);
37static bool exprNode_multiStatement (exprNode p_e);
38bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint);
361091cc 39//static void exprNode_constraintPropagateUp (exprNode p_e);
40constraintList exprNode_traversRequiresConstraints (exprNode e);
41constraintList exprNode_traversEnsuresConstraints (exprNode e);
754746a0 42
43constraintList exprNode_traversTrueEnsuresConstraints (exprNode e);
44
45extern constraintList reflectChanges (constraintList pre2, constraintList post1);
46
361091cc 47void mergeResolve (exprNode parent, exprNode child1, exprNode child2);
34f0c5e7 48exprNode makeDataTypeConstraints (exprNode e);
49constraintList constraintList_makeFixedArrayConstraints (sRefSet s);
50constraintList checkCall (exprNode fcn, exprNodeList arglist);
4cccc6ad 51
f5ac53de 52bool exprNode_testd()
53{
54 /* if ( ( (exprNode_isError ) ) )
55 {
56 }
57 if ( ( (e_1 ) ) )
58 {
59 }
60 */
61}
62
4cccc6ad 63bool exprNode_isUnhandled (exprNode e)
64{
65 llassert( exprNode_isDefined(e) );
66 switch (e->kind)
67 {
68 case XPR_INITBLOCK:
69 case XPR_EMPTY:
70 case XPR_LABEL:
71 case XPR_CONST:
72 case XPR_VAR:
73 case XPR_BODY:
74 case XPR_OFFSETOF:
75 case XPR_ALIGNOFT:
76 case XPR_ALIGNOF:
77 case XPR_VAARG:
78 case XPR_ITERCALL:
79 case XPR_ITER:
80 case XPR_CAST:
81 case XPR_GOTO:
82 case XPR_CONTINUE:
83 case XPR_BREAK:
84 case XPR_COMMA:
85 case XPR_COND:
86 case XPR_TOK:
87 case XPR_FTDEFAULT:
88 case XPR_DEFAULT:
89 case XPR_SWITCH:
90 case XPR_FTCASE:
91 case XPR_CASE:
92 case XPR_INIT:
93 case XPR_NODE:
93307a76 94 DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
754746a0 95 return TRUE;
4cccc6ad 96 /*@notreached@*/
97 break;
98 default:
754746a0 99 return FALSE;
4cccc6ad 100
101 }
102 /*not reached*/
103 return FALSE;
104}
105
106bool exprNode_handleError( exprNode e)
107{
754746a0 108 if (exprNode_isError (e) || exprNode_isUnhandled(e) )
4cccc6ad 109 {
110 static /*@only@*/ cstring error = cstring_undefined;
111
112 if (!cstring_isDefined (error))
113 {
114 error = cstring_makeLiteral ("<error>");
115 }
116
117 /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
118 }
119 return FALSE;
120}
121
34f0c5e7 122bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
4cccc6ad 123{
754746a0 124 if (exprNode_isError (e) )
125 return FALSE;
4cccc6ad 126
754746a0 127 if (exprNode_isUnhandled (e) )
128 {
93307a76 129 DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) );
d8b37170 130 e->requiresConstraints = constraintList_new();
131 e->ensuresConstraints = constraintList_new();
132 e->trueEnsuresConstraints = constraintList_new();
133 e->falseEnsuresConstraints = constraintList_new();
134 // llassert(FALSE);
135 return FALSE;
754746a0 136 }
137
34f0c5e7 138
139 // e = makeDataTypeConstraints (e);
754746a0 140
93307a76 141 DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e),
754746a0 142 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
143
4cccc6ad 144 if (exprNode_isMultiStatement ( e) )
145 {
bf92e32c 146 exprNode_multiStatement(e);
4cccc6ad 147 }
148 else
149 {
754746a0 150 // llassert(FALSE);
151 return FALSE;
4cccc6ad 152 }
34f0c5e7 153
154 {
155 constraintList c;
156
157 c = constraintList_makeFixedArrayConstraints (e->uses);
158 e->requiresConstraints = reflectChanges (e->requiresConstraints, c);
159
160 // e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints);
161
162 }
163
93307a76 164 /* printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) );
165 printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); */
4cccc6ad 166 return FALSE;
167}
168
169
170/* handles multiple statements */
171
172bool exprNode_isMultiStatement(exprNode e)
173{
174if (exprNode_handleError (e) != NULL)
175 return FALSE;
176
177 switch (e->kind)
178 {
179 case XPR_FOR:
180 case XPR_FORPRED:
181 case XPR_IF:
182 case XPR_IFELSE:
183 case XPR_WHILE:
184 case XPR_WHILEPRED:
185 case XPR_DOWHILE:
186 case XPR_BLOCK:
187 case XPR_STMT:
188 case XPR_STMTLIST:
189 return TRUE;
190 default:
191 return FALSE;
192 }
193
194}
195
196bool exprNode_stmt (exprNode e)
197{
198 exprNode snode;
361091cc 199 fileloc loc;
200 bool notError;
4cccc6ad 201
202 if (exprNode_isError(e) )
203 {
204 return FALSE;
205 }
361091cc 206 e->requiresConstraints = constraintList_new();
207 e->ensuresConstraints = constraintList_new();
34f0c5e7 208 // e = makeDataTypeConstraints(e);
4cccc6ad 209
361091cc 210
211 DPRINTF(( "STMT:") );
212 DPRINTF ( ( cstring_toCharsSafe ( exprNode_unparse(e)) )
4cccc6ad 213 );
214 if (e->kind != XPR_STMT)
215 {
216
93307a76 217 DPRINTF (("Not Stmt") );
218 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
4cccc6ad 219 if (exprNode_isMultiStatement (e) )
220 {
221 return exprNode_multiStatement (e );
222 }
d8b37170 223 BPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) );
224 return TRUE;
225 // llassert(FALSE);
4cccc6ad 226 }
361091cc 227
93307a76 228 DPRINTF (("Stmt") );
229 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
361091cc 230
4cccc6ad 231 snode = exprData_getUopNode (e->edata);
232
233 /* could be stmt involving multiple statements:
234 i.e. if, while for ect.
235 */
236
237 if (exprNode_isMultiStatement (snode))
238 {
754746a0 239 // llassert(FALSE);
4cccc6ad 240 return exprNode_multiStatement (snode);
241 }
361091cc 242
243 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
244 notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
245 e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
93307a76 246 // printf ("For: %s \n", exprNode_unparse (e) );
247 // printf ("%s\n", constraintList_print(e->requiresConstraints) );
361091cc 248 e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
93307a76 249 // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
754746a0 250 // llassert(notError);
361091cc 251 return notError;
252
4cccc6ad 253}
254
255
256bool exprNode_stmtList (exprNode e)
257{
361091cc 258 exprNode stmt1, stmt2;
4cccc6ad 259 if (exprNode_isError (e) )
260 {
261 return FALSE;
262 }
361091cc 263
264 e->requiresConstraints = constraintList_new();
265 e->ensuresConstraints = constraintList_new();
34f0c5e7 266 // e = makeDataTypeConstraints(e);
361091cc 267
4cccc6ad 268 /*Handle case of stmtList with only one statement:
269 The parse tree stores this as stmt instead of stmtList*/
270 if (e->kind != XPR_STMTLIST)
271 {
272 return exprNode_stmt(e);
273 }
274 llassert (e->kind == XPR_STMTLIST);
93307a76 275 DPRINTF(( "STMTLIST:") );
276 DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
361091cc 277 stmt1 = exprData_getPairA (e->edata);
278 stmt2 = exprData_getPairB (e->edata);
279
6364363c 280
754746a0 281 DPRINTF((" stmtlist ") );
6364363c 282 DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
283
361091cc 284 exprNode_stmt (stmt1);
285 DPRINTF(("\nstmt after stmtList call " ));
286
287 exprNode_stmt (stmt2);
361091cc 288 mergeResolve (e, stmt1, stmt2 );
92c4a786 289
bf92e32c 290 DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
361091cc 291 constraintList_print(e->requiresConstraints),
292 constraintList_print(e->ensuresConstraints) ) ) );
293 return TRUE;
4cccc6ad 294}
295
361091cc 296
754746a0 297exprNode doIf (exprNode e, exprNode test, exprNode body)
298{
299 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
300 e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
301 e->requiresConstraints = reflectChanges (e->requiresConstraints,
302 test->ensuresConstraints);
303#warning bad
304 e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
305 return e;
306}
307
34f0c5e7 308constraintList constraintList_makeFixedArrayConstraints (sRefSet s)
309{
310 constraintList ret;
311 ret = constraintList_new();
312
313 sRefSet_elements (s, el)
314 {
d8b37170 315 // llassert (el);
34f0c5e7 316 if (sRef_isFixedArray(el) )
317 {
318 int s;
319 constraint con;
320 s = sRef_getArraySize(el);
321 DPRINTF( (message("%s is a fixed array with size %d",
322 sRef_unparse(el), s) ) );
323 con = constraint_makeSRefWriteSafeInt (el, (s - 1));
324 ret = constraintList_add(ret, con);
325 }
326 else
327 {
328 DPRINTF( (message("%s is not a fixed array",
329 sRef_unparse(el)) ) );
330 }
331 }
332 end_sRefSet_elements
333
334 return ret;
335}
336
337exprNode makeDataTypeConstraints (exprNode e)
338{
339 constraintList c;
340 DPRINTF(("makeDataTypeConstraints"));
341
342 c = constraintList_makeFixedArrayConstraints (e->uses);
343
344 e->ensuresConstraints = constraintList_addList (e->ensuresConstraints, c);
345
346/* sRefSet_elements (e->uses, el) */
347/* llassert (el); */
348/* if (sRef_isFixedArray(el) ) */
349/* { */
350/* int s; */
351/* constraint con; */
352/* s = sRef_getArraySize(el); */
353/* DPRINTF( (message("%s is a fixed array with size %d", */
354/* sRef_unparse(el), s) ) ); */
355/* con = constraint_makeSRefWriteSafeInt (el, (s - 1)); */
356/* e->ensuresConstraints = constraintList_add(e->ensuresConstraints, */
357/* con); */
358/* } */
359/* else */
360/* { */
361/* DPRINTF( (message("%s is not a fixed array", */
362/* sRef_unparse(el)) ) ); */
363/* } */
364/* end_sRefSet_elements */
365
366 return e;
367}
368
369
4cccc6ad 370bool exprNode_multiStatement (exprNode e)
371{
372
373 bool ret;
374 exprData data;
754746a0 375 exprNode e1, e2;
376 exprNode p, trueBranch, falseBranch;
377 exprNode forPred, forBody;
378 exprNode init, test, inc;
379 constraintList cons;
380 constraintList t, f;
381 e->requiresConstraints = constraintList_new();
382 e->ensuresConstraints = constraintList_new();
383 e->trueEnsuresConstraints = constraintList_new();
384 e->falseEnsuresConstraints = constraintList_new();
34f0c5e7 385
386 // e = makeDataTypeConstraints(e);
754746a0 387
4cccc6ad 388 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
389 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
390
391 if (exprNode_handleError (e))
392 {
393 return FALSE;
394 }
395
396 data = e->edata;
397
398 ret = TRUE;
399
400 switch (e->kind)
401 {
402
403 case XPR_FOR:
754746a0 404 // ret = message ("%s %s",
405 forPred = exprData_getPairA (data);
406 forBody = exprData_getPairB (data);
407
408
409 //first generate the constraints
410 exprNode_generateConstraints (forPred);
411 exprNode_generateConstraints (forBody);
412
413 //merge the constraints: modle as if statement
414 /* init
415 if (test)
416 for body
417 inc */
418 init = exprData_getTripleInit (forPred->edata);
419 test = exprData_getTripleTest (forPred->edata);
420 inc = exprData_getTripleInc (forPred->edata);
421
f5ac53de 422 // if ( ( (exprNode_isError (test) || (exprNode_isError(init) ) || (exprNode_isError) ) ) )
423 // if ( ( (myexprNode_isError (test) || (myexprNode_isError(init) ) || (myexprNode_isError) ) ) )
424
425 //if ( ( (exprNode_isError ) ) )
426 if ( ( (exprNode_isError (test) || (exprNode_isError(init) ) ) || (exprNode_isError (inc) ) ) )
d8b37170 427 {
f5ac53de 428 BPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) );
d8b37170 429 return ret;
430 }
431
754746a0 432 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
433 // e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
434 e->requiresConstraints = reflectChanges (e->requiresConstraints, test->ensuresConstraints);
435
4cccc6ad 436 break;
437
438 case XPR_FORPRED:
439 // ret = message ("for (%s; %s; %s)",
754746a0 440 exprNode_generateConstraints (exprData_getTripleInit (data) );
441 exprNode_exprTraverse (exprData_getTripleTest (data),FALSE, FALSE, exprNode_loc(e));
442 exprNode_generateConstraints (exprData_getTripleInc (data));
4cccc6ad 443 break;
444 case XPR_IF:
93307a76 445 DPRINTF(( "IF:") );
446 DPRINTF ((exprNode_unparse(e) ) );
754746a0 447 // ret = message ("if (%s) %s",
448 e1 = exprData_getPairA (data);
449 e2 = exprData_getPairB (data);
450
451 exprNode_exprTraverse (e1,
452 FALSE, FALSE, exprNode_loc(e1));
453
454 exprNode_generateConstraints (e2);
455
456 e = doIf (e, e1, e2);
457
458
459 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
4cccc6ad 460 break;
461
462 case XPR_IFELSE:
93307a76 463 DPRINTF(("Starting IFELSE"));
4cccc6ad 464 // ret = message ("if (%s) %s else %s",
754746a0 465 p = exprData_getTriplePred (data);
466 trueBranch = exprData_getTripleTrue (data);
467 falseBranch = exprData_getTripleFalse (data);
468
469 exprNode_exprTraverse (p,
470 FALSE, FALSE, exprNode_loc(p));
471 exprNode_generateConstraints (trueBranch);
472 exprNode_generateConstraints (falseBranch);
473
474 // do requires clauses
475
476 cons = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints);
477 cons = reflectChanges (cons,
478 p->ensuresConstraints);
479 e->requiresConstraints = constraintList_copy (cons);
480
481 cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints);
482 cons = reflectChanges (cons,
483 p->ensuresConstraints);
484 e->requiresConstraints = constraintList_addList (e->requiresConstraints,
485 cons);
486 e->requiresConstraints = constraintList_addList (e->requiresConstraints,
487 p->requiresConstraints);
488
489 // do ensures clauses
490 // find the the ensures lists for each subbranch
491 t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
492 t = constraintList_mergeEnsures (p->ensuresConstraints, t);
493
494 f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
495 f = constraintList_mergeEnsures (p->ensuresConstraints, f);
496
497 // find ensures for whole if/else statement
498
499 e->ensuresConstraints = constraintList_logicalOr (t, f);
93307a76 500 DPRINTF( ("Done IFELSE") );
4cccc6ad 501 break;
502 case XPR_WHILE:
754746a0 503 e1 = exprData_getPairA (data);
504 e2 = exprData_getPairB (data);
505 exprNode_exprTraverse (e1,
506 FALSE, FALSE, exprNode_loc(e1));
507
508 exprNode_generateConstraints (e2);
509
510 e1->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(e1);
511
512 e->requiresConstraints = reflectChanges (e2->requiresConstraints, e1->trueEnsuresConstraints);
513
514 e->requiresConstraints = reflectChanges (e->requiresConstraints,
515 e1->ensuresConstraints);
516#warning bad
517 e->ensuresConstraints = constraintList_copy (e1->ensuresConstraints);
518
4cccc6ad 519 // ret = message ("while (%s) %s",
520 exprNode_generateConstraints (exprData_getPairA (data));
521 exprNode_generateConstraints (exprData_getPairB (data));
522 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
523 break;
524
4cccc6ad 525 case XPR_DOWHILE:
526 // ret = message ("do { %s } while (%s)",
527 exprNode_generateConstraints (exprData_getPairB (data));
528 exprNode_generateConstraints (exprData_getPairA (data));
529 break;
530
531 case XPR_BLOCK:
532 // ret = message ("{ %s }",
533 exprNode_generateConstraints (exprData_getSingle (data));
361091cc 534 e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
535 e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
536 // e->constraints = (exprData_getSingle (data))->constraints;
4cccc6ad 537 break;
538
539 case XPR_STMT:
540 case XPR_STMTLIST:
541 return exprNode_stmtList (e);
542 /*@notreached@*/
543 break;
544 default:
545 ret=FALSE;
546 }
547 return ret;
548}
549
93307a76 550bool lltok_isBoolean_Op (lltok tok)
551{
552 /*this should really be a switch statement but
553 I don't want to violate the abstraction
554 maybe this should go in lltok.c */
555
556 if (lltok_isEq_Op (tok) )
557 {
558 return TRUE;
559 }
560 if (lltok_isAnd_Op (tok) )
561
562 {
563
564 return TRUE;
565 }
566 if (lltok_isOr_Op (tok) )
567 {
568 return TRUE;
569 }
570
34f0c5e7 571 if (lltok_isGt_Op (tok) )
572 {
573 return TRUE;
574 }
575 if (lltok_isLt_Op (tok) )
576 {
577 return TRUE;
578 }
579
580 if (lltok_isLe_Op (tok) )
581 {
582 return TRUE;
583 }
584
585 if (lltok_isGe_Op (tok) )
586 {
587 return TRUE;
588 }
589
93307a76 590 return FALSE;
591
592}
593
594
595void exprNode_booleanTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
596{
34f0c5e7 597 constraint cons;
598exprNode t1, t2;
599exprData data;
600lltok tok;
601constraintList tempList;
602data = e->edata;
603
604tok = exprData_getOpTok (data);
605
606
607t1 = exprData_getOpA (data);
608t2 = exprData_getOpB (data);
93307a76 609
93307a76 610
34f0c5e7 611/* arithmetic tests */
612
613if (lltok_isEq_Op (tok) )
614{
615 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
616 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
617}
618
619
620 if (lltok_isLt_Op (tok) )
621 {
622 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
623 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
624 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
625 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
626 }
627
628
629if (lltok_isGe_Op (tok) )
630{
93307a76 631
34f0c5e7 632 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
633 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
93307a76 634
34f0c5e7 635 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
636 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
93307a76 637
34f0c5e7 638}
93307a76 639
34f0c5e7 640
641 if (lltok_isGt_Op (tok) )
642{
643 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
644 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
645 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
646 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
647}
648
649if (lltok_isLe_Op (tok) )
650{
651 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
652 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
653
654 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
655 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
656}
657
658
659
660/*Logical operations */
661
662 if (lltok_isAnd_Op (tok) )
663
664 {
665 //true ensures
666 tempList = constraintList_copy (t1->trueEnsuresConstraints);
667 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
668 e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList);
669
93307a76 670 //false ensures: fens t1 or tens t1 and fens t2
34f0c5e7 671 tempList = constraintList_copy (t1->trueEnsuresConstraints);
672 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
673 tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
93307a76 674 e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList);
675
34f0c5e7 676 }
677
93307a76 678 if (lltok_isOr_Op (tok) )
679 {
680 //false ensures
681 tempList = constraintList_copy (t1->falseEnsuresConstraints);
682 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
683 e->falseEnsuresConstraints = constraintList_addList(e->falseEnsuresConstraints, tempList);
684
685 //true ensures: tens t1 or fens t1 and tens t2
686 tempList = constraintList_copy (t1->falseEnsuresConstraints);
687 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
688 tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
689 e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList);
690
691 }
692
693}
4cccc6ad 694
4cccc6ad 695bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
696{
697 exprNode t1, t2;
754746a0 698 lltok tok;
4cccc6ad 699 bool handledExprNode;
4cccc6ad 700 exprData data;
4cccc6ad 701 constraint cons;
361091cc 702
d8b37170 703 if (exprNode_isError(e) )
4cccc6ad 704 {
705 return FALSE;
706 }
754746a0 707
93307a76 708 DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
754746a0 709 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
710
711 e->requiresConstraints = constraintList_new();
712 e->ensuresConstraints = constraintList_new();
713 e->trueEnsuresConstraints = constraintList_new();;
714 e->falseEnsuresConstraints = constraintList_new();;
715
d8b37170 716 if (exprNode_isUnhandled (e) )
717 {
718 return FALSE;
719 }
34f0c5e7 720 // e = makeDataTypeConstraints (e);
721
4cccc6ad 722 handledExprNode = TRUE;
723
724 data = e->edata;
725
726 switch (e->kind)
727 {
754746a0 728
4cccc6ad 729
754746a0 730 case XPR_WHILEPRED:
731 t1 = exprData_getSingle (data);
732 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
733 e = exprNode_copyConstraints (e, t1);
734 break;
735
4cccc6ad 736 case XPR_FETCH:
737
4cccc6ad 738 if (definatelv )
739 {
740 t1 = (exprData_getPairA (data) );
741 t2 = (exprData_getPairB (data) );
361091cc 742 cons = constraint_makeWriteSafeExprNode (t1, t2);
4cccc6ad 743 }
744 else
745 {
746 t1 = (exprData_getPairA (data) );
747 t2 = (exprData_getPairB (data) );
361091cc 748 cons = constraint_makeReadSafeExprNode (t1, t2 );
4cccc6ad 749 }
361091cc 750
751 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
4cccc6ad 752 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
361091cc 753 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
bf92e32c 754 // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
755 // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
361091cc 756
4cccc6ad 757 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
758 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
759
760 /*@i325 Should check which is array/index. */
4cccc6ad 761 break;
762 case XPR_PREOP:
763 t1 = exprData_getUopNode(data);
754746a0 764 //lltok_unparse (exprData_getUopTok (data));
765 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
4cccc6ad 766 /*handle * pointer access */
767
768 /*@ i 325 do ++ and -- */
769 if (lltok_isMult( exprData_getUopTok (data) ) )
770 {
771 if (definatelv)
772 {
361091cc 773 cons = constraint_makeWriteSafeInt (t1, 0);
4cccc6ad 774 }
775 else
776 {
777 cons = constraint_makeReadSafeInt (t1, 0);
4cccc6ad 778 }
361091cc 779 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
780 }
754746a0 781
782 /* ! expr */
783 if (lltok_isNot_Op (exprData_getUopTok (data) ) )
361091cc 784 {
754746a0 785 e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints);
786 e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
4cccc6ad 787 }
4cccc6ad 788 break;
789
790 case XPR_PARENS:
791 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
361091cc 792 // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
bf92e32c 793 break;
4cccc6ad 794 case XPR_ASSIGN:
754746a0 795 t1 = exprData_getOpA (data);
796 t2 = exprData_getOpB (data);
797 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
4cccc6ad 798 lltok_unparse (exprData_getOpTok (data));
754746a0 799 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
800
d8b37170 801 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
802 if ( (!exprNode_isError (t1)) && (!exprNode_isError(t2)) )
803 {
804 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
805 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
806 }
754746a0 807
4cccc6ad 808 break;
809 case XPR_OP:
754746a0 810 t1 = exprData_getOpA (data);
811 t2 = exprData_getOpB (data);
4cccc6ad 812
754746a0 813 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
814 tok = exprData_getOpTok (data);
815 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
93307a76 816
817 if (lltok_isBoolean_Op (tok) )
818 exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
754746a0 819
361091cc 820 // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
4cccc6ad 821 break;
822 case XPR_SIZEOFT:
823 ctype_unparse (qtype_getType (exprData_getType (data) ) );
824
825 break;
826
93307a76 827 case XPR_SIZEOF:
4cccc6ad 828 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
361091cc 829 // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
4cccc6ad 830 break;
831
832 case XPR_CALL:
833 exprNode_exprTraverse (exprData_getFcn (data), definatelv, definaterv, sequencePoint );
834 exprNodeList_unparse (exprData_getArgs (data) );
93307a76 835 DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(exprData_getFcn(data) ), exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
836
837
838
839 e->requiresConstraints = constraintList_addList (e->requiresConstraints,
840 checkCall (exprData_getFcn (data), exprData_getArgs (data) ) );
4cccc6ad 841 // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) );
842 break;
843
844 case XPR_RETURN:
845 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
846 break;
847
848 case XPR_NULLRETURN:
849 cstring_makeLiteral ("return");;
850 break;
851
852
853 case XPR_FACCESS:
854 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
855 exprData_getFieldName (data) ;
856 break;
857
858 case XPR_ARROW:
859 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
860 exprData_getFieldName (data);
861 break;
862
863 case XPR_STRINGLITERAL:
864 cstring_copy (exprData_getLiteral (data));
865 break;
866
867 case XPR_NUMLIT:
868 cstring_copy (exprData_getLiteral (data));
869 break;
870 case XPR_POSTOP:
871
872 exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
873 lltok_unparse (exprData_getUopTok (data));
4cccc6ad 874 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
875 {
bf92e32c 876 DPRINTF(("doing ++"));
4cccc6ad 877 t1 = exprData_getUopNode (data);
361091cc 878 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
879 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
bf92e32c 880 // cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint );
881 //e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
4cccc6ad 882 }
883 break;
884 default:
885 handledExprNode = FALSE;
886 }
887
bf92e32c 888 e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints);
889 e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints);
890
4cccc6ad 891 return handledExprNode;
892}
893
754746a0 894
895constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
896{
897 // exprNode t1, t2;
898
899 bool handledExprNode;
900 // char * mes;
901 exprData data;
902 constraintList ret;
38496f11 903
754746a0 904 if (exprNode_handleError (e))
905 {
38496f11 906 ret = constraintList_new();
754746a0 907 return ret;
908 }
38496f11 909 ret = constraintList_copy (e->trueEnsuresConstraints );
754746a0 910
911 handledExprNode = TRUE;
912
913 data = e->edata;
914
915 switch (e->kind)
916 {
917
918 case XPR_FETCH:
919
920 ret = constraintList_addList (ret,
921 exprNode_traversTrueEnsuresConstraints
922 (exprData_getPairA (data) ) );
923
924 ret = constraintList_addList (ret,
925 exprNode_traversTrueEnsuresConstraints
926 (exprData_getPairB (data) ) );
927 break;
928 case XPR_PREOP:
929
930 ret = constraintList_addList (ret,
931 exprNode_traversTrueEnsuresConstraints
932 (exprData_getUopNode (data) ) );
933 break;
934
935 case XPR_PARENS:
936 ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints
937 (exprData_getUopNode (data) ) );
938 break;
939 case XPR_ASSIGN:
940 ret = constraintList_addList (ret,
941 exprNode_traversTrueEnsuresConstraints
942 (exprData_getOpA (data) ) );
943
944 ret = constraintList_addList (ret,
945 exprNode_traversTrueEnsuresConstraints
946 (exprData_getOpB (data) ) );
947 break;
948 case XPR_OP:
949 ret = constraintList_addList (ret,
950 exprNode_traversTrueEnsuresConstraints
951 (exprData_getOpA (data) ) );
952
953 ret = constraintList_addList (ret,
954 exprNode_traversTrueEnsuresConstraints
955 (exprData_getOpB (data) ) );
956 break;
957 case XPR_SIZEOFT:
958
959 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
960
961 break;
962
963 case XPR_SIZEOF:
964
965 ret = constraintList_addList (ret,
966 exprNode_traversTrueEnsuresConstraints
967 (exprData_getSingle (data) ) );
968 break;
969
970 case XPR_CALL:
971 ret = constraintList_addList (ret,
972 exprNode_traversTrueEnsuresConstraints
973 (exprData_getFcn (data) ) );
974 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
975 break;
976
977 case XPR_RETURN:
978 ret = constraintList_addList (ret,
979 exprNode_traversTrueEnsuresConstraints
980 (exprData_getSingle (data) ) );
981 break;
982
983 case XPR_NULLRETURN:
984 // cstring_makeLiteral ("return");;
985 break;
986
987 case XPR_FACCESS:
988 ret = constraintList_addList (ret,
989 exprNode_traversTrueEnsuresConstraints
990 (exprData_getFieldNode (data) ) );
991 //exprData_getFieldName (data) ;
992 break;
993
994 case XPR_ARROW:
995 ret = constraintList_addList (ret,
996 exprNode_traversTrueEnsuresConstraints
997 (exprData_getFieldNode (data) ) );
998 // exprData_getFieldName (data);
999 break;
1000
1001 case XPR_STRINGLITERAL:
1002 // cstring_copy (exprData_getLiteral (data));
1003 break;
1004
1005 case XPR_NUMLIT:
1006 // cstring_copy (exprData_getLiteral (data));
1007 break;
1008 case XPR_POSTOP:
1009
1010 ret = constraintList_addList (ret,
1011 exprNode_traversTrueEnsuresConstraints
1012 (exprData_getUopNode (data) ) );
1013 break;
1014 default:
1015 break;
1016 }
1017
1018 return ret;
1019}
1020
1021
361091cc 1022/* walk down the tree and get all requires Constraints in each subexpression*/
1023constraintList exprNode_traversRequiresConstraints (exprNode e)
1024{
1025 // exprNode t1, t2;
1026
1027 bool handledExprNode;
1028 // char * mes;
1029 exprData data;
1030 constraintList ret;
38496f11 1031
361091cc 1032 if (exprNode_handleError (e))
1033 {
38496f11 1034 ret = constraintList_new();
361091cc 1035 return ret;
1036 }
38496f11 1037 ret = constraintList_copy (e->requiresConstraints );
1038
361091cc 1039 handledExprNode = TRUE;
1040
1041 data = e->edata;
1042
1043 switch (e->kind)
1044 {
1045
1046 case XPR_FETCH:
1047
1048 ret = constraintList_addList (ret,
1049 exprNode_traversRequiresConstraints
1050 (exprData_getPairA (data) ) );
1051
1052 ret = constraintList_addList (ret,
1053 exprNode_traversRequiresConstraints
1054 (exprData_getPairB (data) ) );
1055 break;
1056 case XPR_PREOP:
1057
1058 ret = constraintList_addList (ret,
1059 exprNode_traversRequiresConstraints
1060 (exprData_getUopNode (data) ) );
1061 break;
1062
1063 case XPR_PARENS:
1064 ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
1065 (exprData_getUopNode (data) ) );
1066 break;
1067 case XPR_ASSIGN:
1068 ret = constraintList_addList (ret,
1069 exprNode_traversRequiresConstraints
1070 (exprData_getOpA (data) ) );
1071
1072 ret = constraintList_addList (ret,
1073 exprNode_traversRequiresConstraints
1074 (exprData_getOpB (data) ) );
1075 break;
1076 case XPR_OP:
1077 ret = constraintList_addList (ret,
1078 exprNode_traversRequiresConstraints
1079 (exprData_getOpA (data) ) );
1080
1081 ret = constraintList_addList (ret,
1082 exprNode_traversRequiresConstraints
1083 (exprData_getOpB (data) ) );
1084 break;
1085 case XPR_SIZEOFT:
1086
1087 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1088
1089 break;
1090
1091 case XPR_SIZEOF:
1092
1093 ret = constraintList_addList (ret,
1094 exprNode_traversRequiresConstraints
1095 (exprData_getSingle (data) ) );
1096 break;
1097
1098 case XPR_CALL:
1099 ret = constraintList_addList (ret,
1100 exprNode_traversRequiresConstraints
1101 (exprData_getFcn (data) ) );
1102 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1103 break;
1104
1105 case XPR_RETURN:
1106 ret = constraintList_addList (ret,
1107 exprNode_traversRequiresConstraints
1108 (exprData_getSingle (data) ) );
1109 break;
1110
1111 case XPR_NULLRETURN:
1112 // cstring_makeLiteral ("return");;
1113 break;
1114
1115 case XPR_FACCESS:
1116 ret = constraintList_addList (ret,
1117 exprNode_traversRequiresConstraints
1118 (exprData_getFieldNode (data) ) );
1119 //exprData_getFieldName (data) ;
1120 break;
1121
1122 case XPR_ARROW:
1123 ret = constraintList_addList (ret,
1124 exprNode_traversRequiresConstraints
1125 (exprData_getFieldNode (data) ) );
1126 // exprData_getFieldName (data);
1127 break;
1128
1129 case XPR_STRINGLITERAL:
1130 // cstring_copy (exprData_getLiteral (data));
1131 break;
1132
1133 case XPR_NUMLIT:
1134 // cstring_copy (exprData_getLiteral (data));
1135 break;
1136 case XPR_POSTOP:
1137
1138 ret = constraintList_addList (ret,
1139 exprNode_traversRequiresConstraints
1140 (exprData_getUopNode (data) ) );
1141 break;
1142 default:
1143 break;
1144 }
1145
1146 return ret;
1147}
1148
1149
1150/* walk down the tree and get all Ensures Constraints in each subexpression*/
1151constraintList exprNode_traversEnsuresConstraints (exprNode e)
1152{
1153 // exprNode t1, t2;
1154
1155 bool handledExprNode;
1156 // char * mes;
1157 exprData data;
1158 // constraintExpr tmp;
1159 // constraint cons;
1160 constraintList ret;
38496f11 1161
1162
361091cc 1163 if (exprNode_handleError (e))
1164 {
38496f11 1165 ret = constraintList_new();
361091cc 1166 return ret;
1167 }
1168
38496f11 1169 ret = constraintList_copy (e->ensuresConstraints );
361091cc 1170 handledExprNode = TRUE;
1171
1172 data = e->edata;
1173
1174 DPRINTF( (message (
1175 "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
1176 exprNode_unparse (e),
1177 constraintList_print(e->ensuresConstraints)
1178 )
1179 ));
1180
1181
1182 switch (e->kind)
1183 {
1184
1185 case XPR_FETCH:
1186
1187 ret = constraintList_addList (ret,
1188 exprNode_traversEnsuresConstraints
1189 (exprData_getPairA (data) ) );
1190
1191 ret = constraintList_addList (ret,
1192 exprNode_traversEnsuresConstraints
1193 (exprData_getPairB (data) ) );
1194 break;
1195 case XPR_PREOP:
1196
1197 ret = constraintList_addList (ret,
1198 exprNode_traversEnsuresConstraints
1199 (exprData_getUopNode (data) ) );
1200 break;
1201
1202 case XPR_PARENS:
1203 ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
1204 (exprData_getUopNode (data) ) );
1205 break;
1206 case XPR_ASSIGN:
1207 ret = constraintList_addList (ret,
1208 exprNode_traversEnsuresConstraints
1209 (exprData_getOpA (data) ) );
1210
1211 ret = constraintList_addList (ret,
1212 exprNode_traversEnsuresConstraints
1213 (exprData_getOpB (data) ) );
1214 break;
1215 case XPR_OP:
1216 ret = constraintList_addList (ret,
1217 exprNode_traversEnsuresConstraints
1218 (exprData_getOpA (data) ) );
1219
1220 ret = constraintList_addList (ret,
1221 exprNode_traversEnsuresConstraints
1222 (exprData_getOpB (data) ) );
1223 break;
1224 case XPR_SIZEOFT:
1225
1226 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1227
1228 break;
1229
1230 case XPR_SIZEOF:
1231
1232 ret = constraintList_addList (ret,
1233 exprNode_traversEnsuresConstraints
1234 (exprData_getSingle (data) ) );
1235 break;
1236
1237 case XPR_CALL:
1238 ret = constraintList_addList (ret,
1239 exprNode_traversEnsuresConstraints
1240 (exprData_getFcn (data) ) );
1241 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1242 break;
1243
1244 case XPR_RETURN:
1245 ret = constraintList_addList (ret,
1246 exprNode_traversEnsuresConstraints
1247 (exprData_getSingle (data) ) );
1248 break;
1249
1250 case XPR_NULLRETURN:
1251 // cstring_makeLiteral ("return");;
1252 break;
1253
1254 case XPR_FACCESS:
1255 ret = constraintList_addList (ret,
1256 exprNode_traversEnsuresConstraints
1257 (exprData_getFieldNode (data) ) );
1258 //exprData_getFieldName (data) ;
1259 break;
1260
1261 case XPR_ARROW:
1262 ret = constraintList_addList (ret,
1263 exprNode_traversEnsuresConstraints
1264 (exprData_getFieldNode (data) ) );
1265 // exprData_getFieldName (data);
1266 break;
1267
1268 case XPR_STRINGLITERAL:
1269 // cstring_copy (exprData_getLiteral (data));
1270 break;
1271
1272 case XPR_NUMLIT:
1273 // cstring_copy (exprData_getLiteral (data));
1274 break;
1275 case XPR_POSTOP:
1276
1277 ret = constraintList_addList (ret,
1278 exprNode_traversEnsuresConstraints
1279 (exprData_getUopNode (data) ) );
1280 break;
1281 default:
1282 break;
1283 }
1284DPRINTF( (message (
1285 "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s",
1286 exprNode_unparse (e),
1287 // constraintList_print(e->ensuresConstraints),
1288 constraintList_print(ret)
1289 )
1290 ));
1291
1292
1293 return ret;
1294}
1295
f5ac53de 1296
1297#ifndef exprNode_isError
1298#warning wtf
1299# define exprNode_isError(e) ((e) == exprNode_undefined)
1300#else
1301#warning strange
1302#endif
git-cvsimport mirror of splint
This page took 0.274153 seconds and 5 git commands to generate.