]> andersk Git - splint.git/blame_incremental - src/constraintTerm.c
Committing after merging Evan's changes.
[splint.git] / src / constraintTerm.c
... / ...
CommitLineData
1/*
2** Splint - annotation-assisted static program checker
3** Copyright (C) 1994-2003 University of Virginia,
4** Massachusetts Institute of Technology
5**
6** This program is free software; you can redistribute it and/or modify it
7** under the terms of the GNU General Public License as published by the
8** Free Software Foundation; either version 2 of the License, or (at your
9** option) any later version.
10**
11** This program is distributed in the hope that it will be useful, but
12** WITHOUT ANY WARRANTY; without even the implied warranty of
13** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14** General Public License for more details.
15**
16** The GNU General Public License is available from http://www.gnu.org/ or
17** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18** MA 02111-1307, USA.
19**
20** For information on splint: info@splint.org
21** To report a bug: splint-bug@splint.org
22** For more information: http://www.splint.org
23*/
24
25/*
26** constraintTerm.c
27*/
28
29/* #define DEBUGPRINT 1 */
30
31# include <ctype.h> /* for isdigit */
32# include "splintMacros.nf"
33# include "basic.h"
34# include "cgrammar.h"
35# include "cgrammar_tokens.h"
36
37# include "exprChecks.h"
38# include "exprNodeSList.h"
39
40bool constraintTerm_isDefined (constraintTerm t)
41{
42 return t != NULL;
43}
44
45void constraintTerm_free (/*@only@*/ constraintTerm term)
46{
47 llassert (constraintTerm_isDefined (term));
48
49 fileloc_free (term->loc);
50
51 switch (term->kind)
52 {
53 case CTT_EXPR:
54 /* we don't free an exprNode*/
55 break;
56 case CTT_SREF:
57 /* sref */
58 sRef_free (term->value.sref);
59 break;
60 case CTT_INTLITERAL:
61 /* don't free an int */
62 break;
63 case CTT_ERRORBADCONSTRAINTTERMTYPE:
64 default:
65 /* type was set incorrectly */
66 llcontbug (message("constraintTerm_free type was set incorrectly"));
67 }
68
69 term->kind = CTT_ERRORBADCONSTRAINTTERMTYPE;
70 free (term);
71}
72
73/*@only@*/ static/*@out@*/ constraintTerm new_constraintTermExpr (void)
74{
75 constraintTerm ret;
76 ret = dmalloc (sizeof (* ret ) );
77 ret->value.intlit = 0;
78 return ret;
79}
80
81
82bool constraintTerm_isIntLiteral (constraintTerm term)
83{
84 llassert(term != NULL);
85
86 if (term->kind == CTT_INTLITERAL)
87 return TRUE;
88
89 return FALSE;
90}
91
92
93bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
94{
95 llassert (c != NULL);
96
97 if (c->kind == CTT_EXPR)
98 {
99 if (exprNode_isInitBlock (c->value.expr))
100 {
101 return TRUE;
102 }
103 }
104 return FALSE;
105}
106
107
108bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
109{
110 llassert (c != NULL);
111
112 if (c->kind == CTT_EXPR)
113 {
114 return TRUE;
115 }
116 return FALSE;
117}
118
119/*@access exprNode@*/
120int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
121{
122 exprNodeList list;
123 int ret;
124 llassert (c != NULL);
125 llassert (constraintTerm_isInitBlock (c) );
126 llassert (c->kind == CTT_EXPR);
127
128 llassert(exprNode_isDefined(c->value.expr) );
129
130 if (exprNode_isUndefined(c->value.expr) )
131 {
132 return 1;
133 }
134
135 if (c->value.expr->edata == exprData_undefined)
136 {
137 return 1;
138 }
139 list = exprData_getArgs(c->value.expr->edata);
140
141 ret = exprNodeList_size(list);
142
143 return ret;
144}
145/*@noaccess exprNode@*/
146
147
148bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/
149{
150 llassert (c != NULL);
151 if (c->kind == CTT_EXPR)
152 {
153 if (exprNode_knownStringValue(c->value.expr) )
154 {
155 return TRUE;
156 }
157 }
158 return FALSE;
159}
160
161
162
163cstring constraintTerm_getStringLiteral (constraintTerm c)
164{
165 llassert (c != NULL);
166 llassert (constraintTerm_isStringLiteral (c) );
167 llassert (c->kind == CTT_EXPR);
168
169 return (cstring_copy ( multiVal_forceString (exprNode_getValue (c->value.expr) ) ) );
170}
171
172constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/
173{
174 if (term->kind == CTT_EXPR)
175 {
176 if ( exprNode_knownIntValue (term->value.expr ) )
177 {
178 long int temp;
179
180 temp = exprNode_getLongValue (term->value.expr);
181 term->value.intlit = (int)temp;
182 term->kind = CTT_INTLITERAL;
183 }
184 }
185 return term;
186}
187
188fileloc constraintTerm_getFileloc (constraintTerm t)
189{
190 llassert (constraintTerm_isDefined (t));
191 return (fileloc_copy (t->loc) );
192}
193
194constraintTermType constraintTerm_getKind (constraintTerm t)
195{
196 llassert (constraintTerm_isDefined(t) );
197
198 return (t->kind);
199}
200
201/*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm t)
202{
203 llassert (constraintTerm_isDefined(t) );
204 llassert (t->kind == CTT_SREF);
205
206 return (t->value.sref);
207}
208
209/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e)
210{
211 constraintTerm ret = new_constraintTermExpr();
212 ret->loc = fileloc_copy(exprNode_getfileloc(e));
213 ret->value.expr = e;
214 ret->kind = CTT_EXPR;
215 ret = constraintTerm_simplify(ret);
216 return ret;
217}
218
219/*@only@*/ constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s)
220{
221 constraintTerm ret = new_constraintTermExpr();
222 ret->loc = fileloc_undefined;
223 ret->value.sref = sRef_saveCopy(s);
224 ret->kind = CTT_SREF;
225 ret = constraintTerm_simplify(ret);
226 return ret;
227}
228
229
230
231constraintTerm constraintTerm_copy (constraintTerm term)
232{
233 constraintTerm ret;
234 ret = new_constraintTermExpr();
235 ret->loc = fileloc_copy (term->loc);
236
237 switch (term->kind)
238 {
239 case CTT_EXPR:
240 ret->value.expr = term->value.expr;
241 break;
242 case CTT_INTLITERAL:
243 ret->value.intlit = term->value.intlit;
244 break;
245
246 case CTT_SREF:
247 ret->value.sref = sRef_saveCopy(term->value.sref);
248 break;
249 default:
250 BADEXIT;
251 }
252 ret->kind = term->kind;
253 return ret;
254}
255
256constraintTerm constraintTerm_setFileloc (/*@returned@*/ constraintTerm term, fileloc loc)
257{
258 llassert(term != NULL);
259
260 if ( fileloc_isDefined( term->loc ) )
261 fileloc_free(term->loc);
262
263 term->loc = fileloc_copy(loc);
264 return term;
265}
266
267
268static cstring constraintTerm_getName (constraintTerm term)
269{
270 cstring s;
271 s = cstring_undefined;
272
273 llassert (term != NULL);
274
275 switch (term->kind)
276 {
277 case CTT_EXPR:
278
279 s = message ("%s", exprNode_unparse (term->value.expr) );
280 break;
281 case CTT_INTLITERAL:
282 s = message (" %d ", (int) term->value.intlit);
283 break;
284
285 case CTT_SREF:
286 s = message ("%q", sRef_unparse (term->value.sref) );
287
288 break;
289 default:
290 BADEXIT;
291 /*@notreached@*/
292 break;
293 }
294
295 return s;
296}
297
298constraintTerm
299constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeList arglist) /*@modifies term@*/
300{
301 llassert (term != NULL);
302
303 switch (term->kind)
304 {
305 case CTT_EXPR:
306
307 break;
308 case CTT_INTLITERAL:
309 break;
310
311 case CTT_SREF:
312 term->value.sref = sRef_fixBaseParam (term->value.sref, arglist);
313 break;
314 default:
315 BADEXIT;
316 }
317 return term;
318
319}
320
321cstring constraintTerm_unparse (constraintTerm term) /*@*/
322{
323 cstring s;
324 s = cstring_undefined;
325
326 llassert (term != NULL);
327
328 switch (term->kind)
329 {
330 case CTT_EXPR:
331
332 s = message ("%s @ %q", exprNode_unparse (term->value.expr),
333 fileloc_unparse (term->loc) );
334 break;
335 case CTT_INTLITERAL:
336 s = message ("%d", (int)term->value.intlit);
337 break;
338
339 case CTT_SREF:
340 s = message ("%q", sRef_unparseDebug (term->value.sref) );
341
342 break;
343 default:
344 BADEXIT;
345 }
346
347 return s;
348}
349
350
351constraintTerm constraintTerm_makeIntLiteral (long i)
352{
353 constraintTerm ret = new_constraintTermExpr();
354 ret->value.intlit = i;
355 ret->kind = CTT_INTLITERAL;
356 ret->loc = fileloc_undefined;
357 return ret;
358}
359
360bool constraintTerm_canGetValue (constraintTerm term)
361{
362 if (term->kind == CTT_INTLITERAL)
363 {
364 return TRUE;
365 }
366 else if (term->kind == CTT_SREF)
367 {
368 if (sRef_hasValue (term->value.sref))
369 {
370 multiVal mval = sRef_getValue (term->value.sref);
371
372 return multiVal_isInt (mval); /* for now, only try to deal with int values */
373 }
374 else
375 {
376 return FALSE;
377 }
378 }
379 else if (term->kind == CTT_EXPR)
380 {
381 return FALSE;
382 }
383 else
384 {
385 return FALSE;
386 }
387}
388
389long constraintTerm_getValue (constraintTerm term)
390{
391 llassert (constraintTerm_canGetValue (term));
392
393 if (term->kind == CTT_INTLITERAL)
394 {
395 return term->value.intlit;
396 }
397 else if (term->kind == CTT_SREF)
398 {
399 if (sRef_hasValue (term->value.sref))
400 {
401 multiVal mval = sRef_getValue (term->value.sref);
402
403 return multiVal_forceInt (mval); /* for now, only try to deal with int values */
404 }
405 else
406 {
407 BADBRANCH;
408 }
409 }
410 else if (term->kind == CTT_EXPR)
411 {
412 BADBRANCH;
413 }
414 else
415 {
416 BADBRANCH;
417 }
418
419 BADEXIT;
420}
421
422/*drl added this 10.30.001
423 */
424
425/*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t)
426{
427 llassert (t != NULL);
428
429 llassert (t->kind == CTT_EXPR);
430
431 return t->value.expr;
432
433}
434
435 /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t)
436{
437 llassert (t != NULL);
438 if (t->kind == CTT_EXPR)
439 {
440 return exprNode_getSref(t->value.expr);
441 }
442
443 if (t->kind == CTT_SREF)
444 {
445 return t->value.sref;
446 }
447
448 return sRef_undefined;
449}
450
451bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2)
452{
453 cstring s1, s2;
454
455 llassert (term1 !=NULL && term2 !=NULL);
456
457 DPRINTF ((message
458 ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2)
459 )
460 )
461 );
462
463 s1 = constraintTerm_getName (term1);
464 s2 = constraintTerm_getName (term2);
465
466 if (cstring_equal (s1, s2) )
467 {
468 DPRINTF ((message (" %q and %q are same", s1, s2 ) ) );
469 return TRUE;
470 }
471 else
472 {
473 DPRINTF ((message (" %q and %q are not same", s1, s2 ) ) );
474 return FALSE;
475 }
476}
477
478bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
479{
480 sRef s1, s2;
481
482 llassert (term1 !=NULL && term2 !=NULL);
483
484 if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2))
485
486 /*3/30/2003 comment updated to reflect name change form INTLITERAL to CTT_INTLITERAL*/
487 /* evans 2001-07-24: was (term1->kind == CTT_INTLITERAL) && (term2->kind == CTT_INTLITERAL) ) */
488 {
489 long t1, t2;
490
491 t1 = constraintTerm_getValue (term1);
492 t2 = constraintTerm_getValue (term2);
493
494 return (t1 == t2);
495 }
496
497 if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2))
498 {
499 /* evans 2001-07-24: is this right? */ /*@i534@*/
500 return FALSE;
501 }
502
503 s1 = constraintTerm_getsRef (term1);
504 s2 = constraintTerm_getsRef (term2);
505
506 if (!(sRef_isValid(s1) && sRef_isValid(s2)))
507 {
508 return FALSE;
509 }
510
511 DPRINTF((message
512 ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2)
513 )
514 )
515 );
516
517 if (sRef_similarRelaxed(s1, s2) || sRef_sameName (s1, s2) )
518 {
519 DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
520 return TRUE;
521 }
522 else
523 {
524 DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
525 return FALSE;
526 }
527}
528
529void constraintTerm_dump (/*@observer@*/ constraintTerm t, FILE *f)
530{
531 fileloc loc;
532 constraintTermValue value;
533 constraintTermType kind;
534 uentry u;
535
536 loc = t->loc;
537
538 value = t->value;
539
540 kind = t->kind;
541
542 fprintf(f, "%d\n", (int) kind);
543
544 switch (kind)
545 {
546
547 case CTT_EXPR:
548 u = exprNode_getUentry(t->value.expr);
549 fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
550 break;
551
552 case CTT_SREF:
553 {
554 sRef s;
555
556 s = t->value.sref;
557
558 if (sRef_isResult (s ) )
559 {
560 fprintf(f, "Result\n");
561 }
562 else if (sRef_isParam (s))
563 {
564 int param;
565 ctype ct;
566 cstring ctString;
567
568
569 ct = sRef_getType (s);
570 param = sRef_getParam(s);
571
572 ctString = ctype_dump(ct);
573
574 fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param );
575 cstring_free(ctString);
576 }
577 else if (sRef_isField (s) )
578 {
579 fprintf(f, "sRef_dump %s\n", cstring_toCharsSafe(sRef_dump(s)) );
580 }
581 else
582 {
583 u = sRef_getUentry(s);
584 fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
585 }
586
587 }
588 break;
589
590 case CTT_INTLITERAL:
591 fprintf (f, "%ld\n", t->value.intlit);
592 break;
593
594 default:
595 BADEXIT;
596 }
597
598}
599
600
601/*@only@*/ constraintTerm constraintTerm_undump (FILE *f)
602{
603 constraintTermType kind;
604 constraintTerm ret;
605
606 uentry ue;
607
608 char *str;
609 char *os;
610
611 os = mstring_create (MAX_DUMP_LINE_LENGTH);
612
613 str = fgets (os, MAX_DUMP_LINE_LENGTH, f);
614
615 llassert (str != NULL);
616
617 kind = (constraintTermType) reader_getInt(&str);
618 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
619
620 llassert (str != NULL);
621
622 switch (kind)
623 {
624
625 case CTT_SREF:
626 {
627 sRef s;
628 char * term;
629 term = reader_getWord(&str);
630
631 if (term == NULL)
632 {
633 llfatalbug (message ("Library file appears to be corrupted.") );
634 }
635 if (strcmp (term, "Result") == 0 )
636 {
637 s = sRef_makeResult (ctype_unknown);
638 }
639 else if (strcmp (term, "Param" ) == 0 )
640 {
641 int param;
642 char *str2, *ostr2;
643
644 ctype t;
645
646 reader_checkChar(&str, ' ');
647 str2 = reader_getWord(&str);
648 param = reader_getInt(&str);
649
650 if (str2 == NULL)
651 {
652 llfatalbug (message ("Library file appears to be corrupted.") );
653 }
654
655 ostr2 = str2;
656 t = ctype_undump(&str2) ;
657 s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc, SA_CREATED));
658 free (ostr2);
659 }
660 else if (strcmp (term, "sRef_dump" ) == 0 )
661 {
662 reader_checkChar(&str, ' ');
663 s = sRef_undump (&str);
664 }
665 else /* This must be an identified that we can search for in usymTab */
666 {
667 cstring termStr = cstring_makeLiteralTemp(term);
668
669 ue = usymtab_lookup (termStr);
670 s = uentry_getSref(ue);
671 }
672
673 ret = constraintTerm_makesRef(s);
674
675 free(term);
676 }
677 break;
678
679 case CTT_EXPR:
680 {
681 sRef s;
682 char * term;
683 cstring termStr;
684
685 term = reader_getWord(&str);
686
687 if (term == NULL)
688 {
689 llfatalbug (message ("Library file appears to be corrupted.") );
690 }
691
692 /* This must be an identifier that we can search for in usymTab */
693 termStr = cstring_makeLiteralTemp(term);
694
695 ue = usymtab_lookup (termStr);
696 s = uentry_getSref(ue);
697 ret = constraintTerm_makesRef(s);
698
699 free (term);
700 }
701 break;
702
703
704 case CTT_INTLITERAL:
705 {
706 int i;
707
708 i = reader_getInt(&str);
709 ret = constraintTerm_makeIntLiteral (i);
710 }
711 break;
712
713 default:
714 BADEXIT;
715 }
716 free (os);
717
718 return ret;
719}
720
721
722
723/* drl added sometime before 10/17/001*/
724ctype constraintTerm_getCType (constraintTerm term)
725{
726 ctype ct;
727
728 switch (term->kind)
729 {
730 case CTT_EXPR:
731 ct = exprNode_getType (term->value.expr);
732 break;
733
734 case CTT_INTLITERAL:
735 /*@i888*/ /* hack */
736 ct = ctype_signedintegral;
737 break;
738
739 case CTT_SREF:
740 ct = sRef_getType (term->value.sref) ;
741 break;
742 default:
743 BADEXIT;
744 }
745 return ct;
746}
747
748bool constraintTerm_isConstantOnly (constraintTerm term)
749{
750 switch (term->kind)
751 {
752 case CTT_EXPR:
753 if (exprNode_isNumLiteral (term->value.expr) ||
754 exprNode_isStringLiteral (term->value.expr) ||
755 exprNode_isCharLiteral (term->value.expr) )
756 {
757 return TRUE;
758 }
759 else
760 {
761 return FALSE;
762 }
763
764 case CTT_INTLITERAL:
765 return TRUE;
766
767 case CTT_SREF:
768 if ( sRef_isConst (term->value.sref) )
769 {
770 return TRUE;
771 }
772 else
773 {
774 return FALSE;
775 }
776 default:
777 BADEXIT;
778 }
779
780 BADEXIT;
781}
This page took 0.199204 seconds and 5 git commands to generate.