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