]> andersk Git - splint.git/blame - src/constraintGeneration.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Periodic commit
[splint.git] / src / constraintGeneration.c
CommitLineData
4cccc6ad 1
2/*
3** constraintList.c
4*/
5
6# include <ctype.h> /* for isdigit */
7# include "lclintMacros.nf"
8# include "basic.h"
9# include "cgrammar.h"
10# include "cgrammar_tokens.h"
11
12# include "exprChecks.h"
13# include "aliasChecks.h"
14# include "exprNodeSList.h"
15# include "exprData.i"
16
17void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
18static bool exprNode_handleError( exprNode p_e);
19
20static cstring exprNode_findConstraints ( exprNode p_e);
21static bool exprNode_isMultiStatement(exprNode p_e);
22static bool exprNode_multiStatement (exprNode p_e);
23bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint);
24static void exprNode_constraintPropagateUp (exprNode p_e);
25
26
27bool exprNode_isUnhandled (exprNode e)
28{
29 llassert( exprNode_isDefined(e) );
30 switch (e->kind)
31 {
32 case XPR_INITBLOCK:
33 case XPR_EMPTY:
34 case XPR_LABEL:
35 case XPR_CONST:
36 case XPR_VAR:
37 case XPR_BODY:
38 case XPR_OFFSETOF:
39 case XPR_ALIGNOFT:
40 case XPR_ALIGNOF:
41 case XPR_VAARG:
42 case XPR_ITERCALL:
43 case XPR_ITER:
44 case XPR_CAST:
45 case XPR_GOTO:
46 case XPR_CONTINUE:
47 case XPR_BREAK:
48 case XPR_COMMA:
49 case XPR_COND:
50 case XPR_TOK:
51 case XPR_FTDEFAULT:
52 case XPR_DEFAULT:
53 case XPR_SWITCH:
54 case XPR_FTCASE:
55 case XPR_CASE:
56 case XPR_INIT:
57 case XPR_NODE:
58 DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
59 return FALSE;
60 /*@notreached@*/
61 break;
62 default:
63 return TRUE;
64
65 }
66 /*not reached*/
67 return FALSE;
68}
69
70bool exprNode_handleError( exprNode e)
71{
72 if (exprNode_isError (e) || !exprNode_isUnhandled(e) )
73 {
74 static /*@only@*/ cstring error = cstring_undefined;
75
76 if (!cstring_isDefined (error))
77 {
78 error = cstring_makeLiteral ("<error>");
79 }
80
81 /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
82 }
83 return FALSE;
84}
85
86void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
87{
88 DPRINTF((message ("exprNode_gnerateConstraints Analysising %s %s at", exprNode_unparse( e),
89 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
90
91 if (exprNode_isMultiStatement ( e) )
92 {
93 return exprNode_multiStatement(e);
94 }
95 else
96 {
97 llassert(FALSE);
98 }
99
100 return FALSE;
101}
102
103
104/* handles multiple statements */
105
106bool exprNode_isMultiStatement(exprNode e)
107{
108if (exprNode_handleError (e) != NULL)
109 return FALSE;
110
111 switch (e->kind)
112 {
113 case XPR_FOR:
114 case XPR_FORPRED:
115 case XPR_IF:
116 case XPR_IFELSE:
117 case XPR_WHILE:
118 case XPR_WHILEPRED:
119 case XPR_DOWHILE:
120 case XPR_BLOCK:
121 case XPR_STMT:
122 case XPR_STMTLIST:
123 return TRUE;
124 default:
125 return FALSE;
126 }
127
128}
129
130bool exprNode_stmt (exprNode e)
131{
132 exprNode snode;
133
134 if (exprNode_isError(e) )
135 {
136 return FALSE;
137 }
138
139 TPRINTF(( "STMT:") );
140 TPRINTF ( ( cstring_toCharsSafe ( exprNode_unparse(e)) )
141 );
142 if (e->kind != XPR_STMT)
143 {
144
145 TPRINTF (("Not Stmt") );
146 if (exprNode_isMultiStatement (e) )
147 {
148 return exprNode_multiStatement (e );
149 }
150 llassert(FALSE);
151 }
152
153 snode = exprData_getUopNode (e->edata);
154
155 /* could be stmt involving multiple statements:
156 i.e. if, while for ect.
157 */
158
159 if (exprNode_isMultiStatement (snode))
160 {
161 llassert(FALSE);
162 return exprNode_multiStatement (snode);
163 }
164 else
165 {
166 fileloc loc;
167 bool notError;
168 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
169 notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
170 llassert(notError);
171 fileloc_free (loc);
172 return notError;
173 }
174}
175
176
177bool exprNode_stmtList (exprNode e)
178{
179 if (exprNode_isError (e) )
180 {
181 return FALSE;
182 }
183 /*Handle case of stmtList with only one statement:
184 The parse tree stores this as stmt instead of stmtList*/
185 if (e->kind != XPR_STMTLIST)
186 {
187 return exprNode_stmt(e);
188 }
189 llassert (e->kind == XPR_STMTLIST);
190 TPRINTF(( "STMTLIST:") );
191 TPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
192 (void) exprNode_stmt (exprData_getPairA (e->edata));
193 TPRINTF(("\nstmt after stmtList call " ));
194 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (e->edata), exprData_getPairB (e->edata) );
195 return exprNode_stmt (exprData_getPairB (e->edata));
196}
197
198bool exprNode_multiStatement (exprNode e)
199{
200
201 bool ret;
202 exprData data;
203
204
205 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
206 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
207
208 if (exprNode_handleError (e))
209 {
210 return FALSE;
211 }
212
213 data = e->edata;
214
215 ret = TRUE;
216
217 switch (e->kind)
218 {
219
220 case XPR_FOR:
221 // ret = message ("%s %s",
222 exprNode_generateConstraints (exprData_getPairA (data));
223 exprNode_generateConstraints (exprData_getPairB (data));
224 break;
225
226 case XPR_FORPRED:
227 // ret = message ("for (%s; %s; %s)",
228 exprNode_generateConstraints (exprData_getTripleInit (data));
229 exprNode_generateConstraints (exprData_getTripleTest (data));
230 exprNode_generateConstraints (exprData_getTripleInc (data));
231 break;
232 case XPR_IF:
233 TPRINTF(( "IF:") );
234 TPRINTF ((exprNode_unparse(e) ) );
235 // ret = message ("if (%s) %s",
236 exprNode_generateConstraints (exprData_getPairA (data));
237 exprNode_generateConstraints (exprData_getPairB (data));
238 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
239 break;
240
241 case XPR_IFELSE:
242 // ret = message ("if (%s) %s else %s",
243 exprNode_generateConstraints (exprData_getTriplePred (data));
244 exprNode_generateConstraints (exprData_getTripleTrue (data));
245 exprNode_generateConstraints (exprData_getTripleFalse (data));
246 break;
247 case XPR_WHILE:
248 // ret = message ("while (%s) %s",
249 exprNode_generateConstraints (exprData_getPairA (data));
250 exprNode_generateConstraints (exprData_getPairB (data));
251 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
252 break;
253
254 case XPR_WHILEPRED:
255 // ret =
256 // cstring_copy (
257 exprNode_generateConstraints (exprData_getSingle (data));
258 break;
259
260 case XPR_DOWHILE:
261 // ret = message ("do { %s } while (%s)",
262 exprNode_generateConstraints (exprData_getPairB (data));
263 exprNode_generateConstraints (exprData_getPairA (data));
264 break;
265
266 case XPR_BLOCK:
267 // ret = message ("{ %s }",
268 exprNode_generateConstraints (exprData_getSingle (data));
269 e->constraints = (exprData_getSingle (data))->constraints;
270 break;
271
272 case XPR_STMT:
273 case XPR_STMTLIST:
274 return exprNode_stmtList (e);
275 /*@notreached@*/
276 break;
277 default:
278 ret=FALSE;
279 }
280 return ret;
281}
282
283
284/* void upwrap (exprNode e) */
285/* { */
286/* printf ("in upwrap with e = %X\n" , e); */
287/* printf ("%s\n", exprNode_unparse (e) ); */
288/* } */
289
290
291
292bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
293{
294 exprNode t1, t2;
295
296 bool handledExprNode;
297 char * mes;
298 exprData data;
299 constraintExpr tmp;
300 constraint cons;
301
302 DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
303 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
304
305 if (exprNode_handleError (e))
306 {
307 return FALSE;
308 }
309
310 handledExprNode = TRUE;
311
312 data = e->edata;
313
314 switch (e->kind)
315 {
316
317 case XPR_FETCH:
318
319 /*
320 Make sure these are right!
321
322 if (rvalue)
323 valueOf (index) <= maxRead (array)
324 valueOf (index) >= minRead (array)
325 else lvalue
326 valueOf (index) <= maxSet (array)
327 valueOf (index) >= minSet (array)
328 */
329 if (definatelv )
330 {
331 t1 = (exprData_getPairA (data) );
332 t2 = (exprData_getPairB (data) );
333 cons = constraint_makeWriteSafeExprNode (t1, t2);
334 }
335 else
336 {
337 t1 = (exprData_getPairA (data) );
338 t2 = (exprData_getPairB (data) );
339 cons = constraint_makeReadSafeExprNode (t1, t2 );
340 }
341 e->constraints = constraintList_add(e->constraints, cons);
342 constraint_print (cons);
343 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
344 constraint_print (cons);
345 cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
346 constraint_print (cons);
347
348 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
349 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
350
351 /*@i325 Should check which is array/index. */
352
353
354 break;
355 case XPR_PREOP:
356 t1 = exprData_getUopNode(data);
357 lltok_unparse (exprData_getUopTok (data));
358 exprNode_exprTraverse (exprData_getUopNode (data), definatelv, definaterv, sequencePoint );
359 /*handle * pointer access */
360
361 /*@ i 325 do ++ and -- */
362 if (lltok_isMult( exprData_getUopTok (data) ) )
363 {
364 if (definatelv)
365 {
366 printf ("Requires maxs(%s) > %d \n", exprNode_unparse (exprData_getUopNode (data) ), 0 );
367 }
368 else
369 {
370 cons = constraint_makeReadSafeInt (t1, 0);
371 constraint_print(cons);
372 }
373 }
374
375 break;
376
377 case XPR_PARENS:
378 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
379 e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
380 break;
381 case XPR_ASSIGN:
382 exprNode_exprTraverse (exprData_getOpA (data), TRUE, definaterv, sequencePoint );
383 lltok_unparse (exprData_getOpTok (data));
384 exprNode_exprTraverse (exprData_getOpB (data), definatelv, TRUE, sequencePoint );
385 e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) );
386 break;
387 case XPR_OP:
388 exprNode_exprTraverse (exprData_getOpA (data), definatelv, definaterv, sequencePoint );
389 lltok_unparse (exprData_getOpTok (data));
390 exprNode_exprTraverse (exprData_getOpB (data), definatelv, definaterv, sequencePoint );
391
392 e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
393 break;
394 case XPR_SIZEOFT:
395 ctype_unparse (qtype_getType (exprData_getType (data) ) );
396
397 break;
398
399 case XPR_SIZEOF:
400 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
401 e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
402 break;
403
404 case XPR_CALL:
405 exprNode_exprTraverse (exprData_getFcn (data), definatelv, definaterv, sequencePoint );
406 exprNodeList_unparse (exprData_getArgs (data) );
407 // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) );
408 break;
409
410 case XPR_RETURN:
411 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
412 break;
413
414 case XPR_NULLRETURN:
415 cstring_makeLiteral ("return");;
416 break;
417
418
419 case XPR_FACCESS:
420 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
421 exprData_getFieldName (data) ;
422 break;
423
424 case XPR_ARROW:
425 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
426 exprData_getFieldName (data);
427 break;
428
429 case XPR_STRINGLITERAL:
430 cstring_copy (exprData_getLiteral (data));
431 break;
432
433 case XPR_NUMLIT:
434 cstring_copy (exprData_getLiteral (data));
435 break;
436 case XPR_POSTOP:
437
438 exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
439 lltok_unparse (exprData_getUopTok (data));
440 e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
441 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
442 {
443 t1 = exprData_getUopNode (data);
444 cons = constraint_makeSideEffectPostIncrement (t1, sequencePoint );
445 constraint_print (cons);
446 // printf("Side Effect: %s = (%s)0 +1 ", exprNode_unparse (exprData_getUopNode (data) ), exprNode_unparse (exprData_getUopNode(data) ) );
447 }
448 break;
449 default:
450 handledExprNode = FALSE;
451 }
452
453 return handledExprNode;
454}
455
456/* void exprNode_constraintPropagateUp (exprNode e) */
457/* { */
458
459/* cstring ret; */
460/* exprData data; */
461
462/* if (exprNode_handleError (e) ) */
463/* { */
464/* return; */
465/* } */
466
467/* data = e->edata; */
468
469/* switch (e->kind) */
470/* { */
471/* case XPR_PARENS: */
472/* e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined); */
473/* break; */
474/* case XPR_ASSIGN: */
475/* e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) ); */
476/* break; */
477/* case XPR_CALL: */
478/* // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) ); */
479/* break; */
480/* case XPR_INITBLOCK: */
481/* //("{ %q }" */
482/* exprNodeList_unparse (exprData_getArgs (data) ); */
483/* // e->constraints = constraintList_exprNodemerge (exprData_getArgs (data), exprData_getOpB (data) ); */
484/* break; */
485
486/* case XPR_OP: */
487/* // ret = message ("%s %s %s", */
488/* exprNode_generateConstraints (exprData_getOpA (data)), */
489/* lltok_unparse (exprData_getOpTok (data)), */
490/* exprNode_generateConstraints (exprData_getOpB (data))); */
491/* e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data); */
492/* break; */
493
494/* case XPR_ALIGNOF: */
495/* e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined); */
496/* break; */
497
498/* case XPR_VAARG: */
499/* e->constraints = constraintList_exprNodemerge (exprData_getCastNode (data), exprNode_undefined); */
500/* break; */
501
502/* case XPR_ITERCALL: */
503/* // ret = message ("%q(%q)", */
504/* // uentry_getName (exprData_getIterCallIter (data)), */
505/* // exprNodeList_unparse (exprData_getIterCallArgs (data))); */
506/* //// e->constraints = constraintList_exprNodemerge (exprData_getIterCallArgs (data), exprNode_undefined); */
507/* break; */
508/* case XPR_ITER: */
509/* DPRINTF(("XPR_ITER NOT IMPLEMENTED" )); */
510/* // ret = message ("%q(%q) %s %q", */
511/* // uentry_getName (exprData_getIterSname (data)), */
512/* // exprNodeList_unparse (exprData_getIterAlist (data)), */
513/* // exprNode_generateConstraints (exprData_getIterBody (data)), */
514/* // uentry_getName (exprData_getIterEname (data))); */
515/* break; */
516/* case XPR_CAST: */
517/* e->constraints = constraintList_exprNodemerge (exprData_getCastNode (data), exprNode_undefined); */
518/* break; */
519
520/* default: */
521/* DPRINTF(("NOT Currently IMplemented")); */
522/* } */
523/* } */
524
525/* //Not used below */
526
527/* case XPR_FOR: */
528/* ret = message ("%s %s", */
529/* exprNode_generateConstraints (exprData_getPairA (data)), */
530/* exprNode_generateConstraints (exprData_getPairB (data))); */
531/* break; */
532
533/* case XPR_FORPRED: */
534/* ret = message ("for (%s; %s; %s)", */
535/* exprNode_generateConstraints (exprData_getTripleInit (data)), */
536/* exprNode_generateConstraints (exprData_getTripleTest (data)), */
537/* exprNode_generateConstraints (exprData_getTripleInc (data))); */
538/* break; */
539
540/* case XPR_GOTO: */
541/* ret = message ("goto %s", exprData_getLiteral (data)); */
542/* break; */
543
544/* case XPR_CONTINUE: */
545/* ret = cstring_makeLiteral ("continue"); */
546/* break; */
547
548/* case XPR_BREAK: */
549/* ret = cstring_makeLiteral ("break"); */
550/* break; */
551
552/* case XPR_RETURN: */
553/* ret = message ("return %s", exprNode_generateConstraints (exprData_getSingle (data))); */
554/* break; */
555
556/* case XPR_NULLRETURN: */
557/* ret = cstring_makeLiteral ("return"); */
558/* break; */
559
560/* case XPR_COMMA: */
561/* ret = message ("%s, %s", */
562/* exprNode_generateConstraints (exprData_getPairA (data)), */
563/* exprNode_generateConstraints (exprData_getPairB (data))); */
564/* break; */
565
566/* case XPR_COND: */
567/* ret = message ("%s ? %s : %s", */
568/* exprNode_generateConstraints (exprData_getTriplePred (data)), */
569/* exprNode_generateConstraints (exprData_getTripleTrue (data)), */
570/* exprNode_generateConstraints (exprData_getTripleFalse (data))); */
571/* break; */
572/* case XPR_IF: */
573/* ret = message ("if (%s) %s", */
574/* exprNode_generateConstraints (exprData_getPairA (data)), */
575/* exprNode_generateConstraints (exprData_getPairB (data))); */
576/* e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data)); */
577/* break; */
578
579/* case XPR_IFELSE: */
580/* ret = message ("if (%s) %s else %s", */
581/* exprNode_generateConstraints (exprData_getTriplePred (data)), */
582/* exprNode_generateConstraints (exprData_getTripleTrue (data)), */
583/* exprNode_generateConstraints (exprData_getTripleFalse (data))); */
584/* break; */
585/* case XPR_WHILE: */
586/* ret = message ("while (%s) %s", */
587/* exprNode_generateConstraints (exprData_getPairA (data)), */
588/* exprNode_generateConstraints (exprData_getPairB (data))); */
589/* e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) ); */
590/* break; */
591
592/* case XPR_WHILEPRED: */
593/* ret = cstring_copy (exprNode_generateConstraints (exprData_getSingle (data))); */
594/* break; */
595
596/* case XPR_TOK: */
597/* ret = cstring_copy (lltok_unparse (exprData_getTok (data))); */
598/* break; */
599
600/* case XPR_DOWHILE: */
601/* ret = message ("do { %s } while (%s)", */
602/* exprNode_generateConstraints (exprData_getPairB (data)), */
603/* exprNode_generateConstraints (exprData_getPairA (data))); */
604/* break; */
605
606/* case XPR_BLOCK: */
607/* ret = message ("{ %s }", exprNode_generateConstraints (exprData_getSingle (data))); */
608/* e->constraints = (exprData_getSingle (data))->constraints; */
609/* break; */
610
611/* case XPR_STMT: */
612/* ret = cstring_copy (exprNode_generateConstraints (exprData_getSingle (data))); */
613/* e->constraints = (exprData_getSingle (data))->constraints; */
614/* break; */
615
616/* case XPR_STMTLIST: */
617/* ret = message ("%s; %s", */
618/* exprNode_generateConstraints (exprData_getPairA (data)), */
619/* exprNode_generateConstraints (exprData_getPairB (data))); */
620/* e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) ); */
621/* break; */
622
623/* case XPR_FTDEFAULT: */
624/* case XPR_DEFAULT: */
625/* ret = cstring_makeLiteral ("default:"); */
626/* break; */
627
628/* case XPR_SWITCH: */
629/* ret = message ("switch (%s) %s", */
630/* exprNode_generateConstraints (exprData_getPairA (data)), */
631/* exprNode_generateConstraints (exprData_getPairB (data))); */
632/* break; */
633
634/* case XPR_FTCASE: */
635/* case XPR_CASE: */
636/* ret = message ("case %s:", */
637/* exprNode_generateConstraints (exprData_getSingle (data))); */
638/* break; */
639
640/* case XPR_INIT: */
641/* ret = message ("%s = %s", */
642/* idDecl_getName (exprData_getInitId (data)), */
643/* exprNode_generateConstraints (exprData_getInitNode (data))); */
644/* break; */
645
646/* case XPR_FACCESS: */
647/* ret = message ("%s.%s", */
648/* exprNode_generateConstraints (exprData_getFieldNode (data)), */
649/* exprData_getFieldName (data)); */
650/* break; */
651
652/* case XPR_ARROW: */
653/* ret = message ("%s->%s", */
654/* exprNode_generateConstraints (exprData_getFieldNode (data)), */
655/* exprData_getFieldName (data)); */
656/* break; */
657
658/* case XPR_STRINGLITERAL: */
659/* ret = cstring_copy (exprData_getLiteral (data)); */
660/* break; */
661
662/* case XPR_NUMLIT: */
663/* ret = cstring_copy (exprData_getLiteral (data)); */
664/* break; */
665
666/* case XPR_NODE: */
667/* ret = cstring_makeLiteral ("<node>"); */
668/* break; */
669/* } */
670
671/* return ret; */
672/* } */
git-cvsimport mirror of splint
This page took 0.618575 seconds and 5 git commands to generate.