2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
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
31 ** Massachusetts Institute of Technology
34 # include "splintMacros.nf"
36 # include "llgrammar.h"
37 # include "checking.h"
42 static /*@only@*/ cstring printBadArgs (sortSetList p_args);
43 static /*@only@*/ sortSet
44 standardOperators (/*@null@*/ nameNode p_n, sortSetList p_argSorts, sort p_q);
45 static bool isStandardOperator (/*@null@*/ nameNode p_n);
46 static void assignSorts (termNode p_t, sort p_s);
49 computePossibleSorts (/*@returned@*/ /*@null@*/ termNode t)
53 if (t != (termNode) 0)
62 case TRM_UNCHANGEDALL:
63 case TRM_UNCHANGEDOTHERS:
69 sortSetList argSorts = sortSetList_new ();
73 if (termNodeList_size (t->args) != 0)
75 termNodeList_elements (t->args, arg)
77 (void) computePossibleSorts (arg);
79 if (sortSet_size (arg->possibleSorts) == 0)
85 sortSetList_addh (argSorts, arg->possibleSorts);
87 } end_termNodeList_elements;
91 lslOpSet_free (t->possibleOps);
92 sortSetList_free (argSorts);
93 t->possibleOps = lslOpSet_new ();
98 ops = symtable_opsWithLegalDomain (g_symtab, t->name, argSorts, t->given);
99 lslOpSet_free (t->possibleOps);
100 t->possibleOps = ops;
102 lslOpSet_elements (t->possibleOps, op)
105 sort = sigNode_rangeSort (op->signature);
106 (void) sortSet_insert (t->possibleSorts, sort);
107 } end_lslOpSet_elements;
109 standards = standardOperators (t->name, argSorts, t->given);
111 sortSet_elements (standards, el)
113 (void) sortSet_insert (t->possibleSorts, el);
114 } end_sortSet_elements;
116 sortSet_free (standards);
118 if (!(t->error_reported) && sortSet_size (t->possibleSorts) == 0)
120 unsigned int arity = termNodeList_size (t->args);
121 errtok = nameNode_errorToken (t->name);
123 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
125 if (isStandardOperator (t->name))
128 message ("Type error: %q not declared for %q",
129 nameNode_unparse (t->name), printBadArgs (argSorts)));
131 else if (t->name != NULL
132 && symtable_opExistsWithArity (g_symtab, t->name, arity))
134 sigNodeSet possibleOps = symtable_possibleOps (g_symtab, t->name);
135 cstring opName = nameNode_unparse (t->name);
138 ** all these will be standardOperators soon...
141 if (cstring_equalLit (opName, "__ [__]"))
144 message ("Type error: %q not declared for %q",
145 opName, printBadArgs (argSorts)));
150 message ("Type error: %q declared: %q\ngiven: %q",
152 sigNodeSet_unparseSomeSigs (possibleOps),
153 printBadArgs (argSorts)));
158 sigNodeSet possibleOps;
161 llassert (t->name != NULL);
163 possibleOps = symtable_possibleOps (g_symtab, t->name);
164 npossibleOps = sigNodeSet_size (possibleOps);
167 ** evs --- check is it is wrong arity...
170 if (npossibleOps == 0)
174 message ("Undeclared operator: %q", nameNode_unparse (t->name)));
180 message ("Operator %q declared for %q arguments, given %d",
181 nameNode_unparse (t->name),
182 sigNodeSet_unparsePossibleAritys (possibleOps),
186 t->error_reported = TRUE;
188 sortSetList_free (argSorts);
197 static /*@only@*/ cstring
198 printBadArgs (sortSetList args)
200 if (sortSetList_size (args) == 1)
202 return (sortSet_unparseOr (sortSetList_head (args)));
206 cstring s = cstring_undefined;
209 sortSetList_elements (args, ss)
212 s = message ("arg %d: %q", argno, sortSet_unparseOr (ss));
214 s = message ("%q; arg %d: %q", s, argno, sortSet_unparseOr (ss));
216 } end_sortSetList_elements;
223 checkSort (/*@returned@*/ termNode t)
230 (void) computePossibleSorts (t);
231 sorts = t->possibleSorts;
233 llassert (sortSet_isDefined (sorts));
235 size = sortSet_size (sorts);
238 case 0: /* complain later */
240 case 1: /* just right */
241 theSort = sortSet_choose (sorts);
242 assignSorts (t, theSort);
245 /* we allow C literals to have multiple sorts */
246 if (t->kind != TRM_LITERAL)
248 errtok = termNode_errorToken (t);
249 t->error_reported = TRUE;
252 message ("Term %q: can have more than one possible type. Possible types: %q",
253 termNode_unparse (t), sortSet_unparseClean (sorts)));
260 assignSorts (termNode t, sort s)
262 /* other kinds are already assigned bottom-up */
267 case TRM_ZEROARY: /* pick s to be the sort chosen */
269 sortSet_elements (t->possibleSorts, s2)
271 if (sort_equal (s2, s))
273 sortSet_free (t->possibleSorts);
274 t->possibleSorts = sortSet_new ();
275 (void) sortSet_insert (t->possibleSorts, s);
279 } end_sortSet_elements;
281 case TRM_APPLICATION:
283 lslOpSet sigs = t->possibleOps;
284 lslOpSet oldops = lslOpSet_undefined;
285 sigNode op = (sigNode) 0;
286 nameNode name = t->name;
287 termNodeList args = t->args;
290 errtok = nameNode_errorToken (name);
292 /* why compute again? to check for duplicates */
293 lslOpSet_elements (sigs, sig)
295 sort rsort = sigNode_rangeSort (sig->signature);
297 if (sort_equal (s, rsort))
303 t->error_reported = TRUE;
306 message ("Ambiguous operator %q: %q or %q",
307 nameNode_unparse (name),
308 sigNode_unparse (op),
309 sigNode_unparse (sig->signature)));
313 iop = (lslOp) dmalloc (sizeof (*iop));
317 oldops = t->possibleOps;
318 t->possibleOps = lslOpSet_new ();
319 iop->name = nameNode_copy (name);
321 (void) lslOpSet_insert (t->possibleOps, iop);
326 } end_lslOpSet_elements;
328 lslOpSet_free (oldops);
332 if (sortSet_size (t->possibleSorts) == 1)
334 t->sort = sortSet_choose (t->possibleSorts);
338 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
339 t->error_reported = TRUE;
341 lclerror (errtok, message ("Operator not found: %q",
342 nameNode_unparse (name)));
348 if (termNodeList_empty (args))
350 if (op != (sigNode) 0)
352 /* was --- NB: copy to avoid interference */
353 /* shouldn't need to copy --- its a fresh list */
354 sortList dom = sigNode_domain (op);
356 sortList_reset (dom);
357 termNodeList_elements (args, arg)
359 assignSorts (arg, sortList_current (dom));
360 sortList_advance (dom);
361 } end_termNodeList_elements;
367 errtok = nameNode_errorToken (name);
368 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
369 t->error_reported = TRUE;
371 lclerror (errtok, message ("No matching operator: %q",
372 nameNode_unparse (name)));
378 default: /* do nothing */
384 checkLclPredicate (ltoken t, lclPredicateNode n)
388 if ((n == NULL) || (n->predicate == NULL))
390 llcontbuglit ("checkLclPredicate expects valid lclPredicate. "
391 "Skipping current check");
395 /* check only if there are no previous errors */
397 if (!n->predicate->error_reported)
399 /* check that the sort of n is boolean */
400 theSort = n->predicate->sort;
401 if (!sort_compatible (theSort, g_sortCapBool))
403 if (sort_isNoSort (theSort))
405 ; /* "Expects a boolean term. Given term has unknown sort" */
409 cstring clauset = ltoken_getRawString (t);
411 if (cstring_firstChar (clauset) == '(')
413 clauset = cstring_makeLiteral ("Equality");
417 /* uppercase first letter */
418 clauset = cstring_copy (clauset);
419 cstring_setChar (clauset, 1,
420 (char) toupper (cstring_firstChar (clauset)));
423 lclerror (t, message ("%q expects a boolean term, given %q.",
424 clauset, sort_unparse (theSort)));
432 ** these should not be doing string comparisons!
435 static bool isDeRefOperator (cstring s)
437 return (cstring_equalLit (s, "*"));
440 static bool isStateOperator (cstring s)
442 return (cstring_equalLit (s, "^") ||
443 cstring_equalLit (s, "'") ||
444 cstring_equalLit (s, "\\any") ||
445 cstring_equalLit (s, "\\pre") ||
446 cstring_equalLit (s, "\\post"));
449 static bool isCompareOperator (cstring s) /* YUCK!!! */
451 return (cstring_equalLit (s, "\\eq") ||
452 cstring_equalLit (s, "\\neq") ||
453 cstring_equalLit (s, "=") ||
454 cstring_equalLit (s, "!=") ||
455 cstring_equalLit (s, "~=") ||
456 cstring_equalLit (s, "=="));
459 static bool isStandardOperator (/*@null@*/ nameNode n)
461 if (n != (nameNode) 0)
465 opFormNode opf = n->content.opform;
467 llassert (opf != NULL);
471 case OPF_IF: return TRUE;
476 cstring s = ltoken_getRawString (opf->content.anyop);
478 if (isStateOperator (s)) return TRUE;
484 cstring s = ltoken_getRawString (opf->content.anyop);
486 return (isDeRefOperator (s));
490 cstring s = ltoken_getRawString (opf->content.anyop);
492 return (isCompareOperator (s));
524 int code = ltoken_getCode (n->content.opid);
526 if (code == simpleId)
528 cstring text = nameNode_unparse (n);
529 bool ret = (cstring_equalLit (text, "trashed")
530 || cstring_equalLit (text, "maxIndex")
531 || cstring_equalLit (text, "minIndex")
532 || cstring_equalLit (text, "isSub"));
538 return (code == LLT_MODIFIES || code == LLT_FRESH
539 || code == LLT_UNCHANGED || code == LLT_SIZEOF);
545 static /*@only@*/ sortSet
546 standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sort q)
549 sortSet ret = sortSet_new ();
551 if (n == (nameNode) 0) return ret;
555 int code = ltoken_getCode (n->content.opid);
557 if (sortSetList_size (argSorts) == 1)
559 sortSetList_reset (argSorts);
561 argSet = sortSetList_current (argSorts);
563 sortSet_elements (argSet, current)
567 sn = sort_quietLookup (current);
569 while (sn->kind == SRT_SYN)
571 sn = sort_quietLookup (sn->baseSort);
574 /*@-loopswitchbreak@*/
579 cstring text = ltoken_getRawString (n->content.opid);
581 if (cstring_equalLit (text, "trashed")) /* GACK! */
583 if (sn->kind == SRT_OBJ ||
584 sn->kind == SRT_ARRAY)
585 (void) sortSet_insert (ret, g_sortBool);
588 if (cstring_equalLit (text, "maxIndex") ||
589 cstring_equalLit (text, "minIndex"))
591 if (sn->kind == SRT_ARRAY || sn->kind == SRT_PTR)
592 (void) sortSet_insert (ret, g_sortInt);
594 /* if (lsymbol_fromChars ("maxIndex") */
601 if (sn->kind == SRT_OBJ ||
602 sn->kind == SRT_ARRAY)
604 (void) sortSet_insert (ret, g_sortBool);
608 if (sn->kind == SRT_OBJ ||
609 sn->kind == SRT_ARRAY ||
610 sn->kind == SRT_VECTOR)
611 (void) sortSet_insert (ret, g_sortInt);
616 } end_sortSet_elements;
621 opFormNode opf = n->content.opform;
623 llassert (opf != NULL);
629 ** if __ then __ else __ : bool, S, S -> S
630 ** is defined for all sorts
633 if (sortSetList_size (argSorts) == 3)
635 argSet = sortSetList_head (argSorts);
637 if (sortSet_member (argSet, g_sortBool))
639 sortSetList_reset (argSorts);
640 sortSetList_advance (argSorts);
642 argSet = sortSetList_current (argSorts);
644 if (sortSet_size (argSet) == 1)
646 sort clause = sortSet_choose (argSet);
649 sortSetList_advance (argSorts);
650 argSet = sortSetList_current (argSorts);
652 clause2 = sortSet_choose (argSet);
654 if (sortSet_size (argSet) == 1 &&
655 sort_equal (clause, clause2))
657 (void) sortSet_insert (ret, clause);
665 cstring s = ltoken_getRawString (opf->content.anyop);
667 if (isStateOperator (s))
669 if (sortSetList_size (argSorts) == 1)
671 sortSetList_reset (argSorts);
673 argSet = sortSetList_current (argSorts);
675 sortSet_elements (argSet, current)
679 sn = sort_quietLookup (current);
681 while (sn->kind == SRT_SYN)
683 sn = sort_quietLookup (sn->baseSort);
689 (void) sortSet_insert (ret, sn->baseSort);
692 (void) sortSet_insert (ret,
693 sort_makeVec (ltoken_undefined, current));
696 (void) sortSet_insert (ret,
697 sort_makeTuple (ltoken_undefined, current));
700 (void) sortSet_insert (ret,
701 sort_makeUnionVal (ltoken_undefined, current));
715 llbuglit ("standardOperators: Synonym in switch");
717 } end_sortSet_elements ;
725 cstring s = ltoken_getRawString (opf->content.anyop);
727 if (isDeRefOperator (s))
729 if (sortSetList_size (argSorts) == 1)
731 sortSetList_reset (argSorts);
733 argSet = sortSetList_current (argSorts);
735 sortSet_elements (argSet, current)
739 sn = sort_quietLookup (current);
741 while (sn->kind == SRT_SYN)
743 sn = sort_quietLookup (sn->baseSort);
746 if (sn->kind == SRT_PTR)
748 (void) sortSet_insert (ret, sn->baseSort);
750 } end_sortSet_elements;
759 cstring s = ltoken_getRawString (opf->content.anyop);
761 if (isCompareOperator (s))
763 if (sortSetList_size (argSorts) == 2)
767 sortSetList_reset (argSorts);
769 argSet = sortSetList_current (argSorts);
770 sortSetList_advance (argSorts);
771 argSet2 = sortSetList_current (argSorts);
773 if (sortSet_size (argSet) == 1)
775 sortSet_elements (argSet, cl)
777 sortSet_elements (argSet2, cl2)
779 if (sort_equal (cl, cl2))
781 (void) sortSet_insert (ret, g_sortBool);
783 } end_sortSet_elements;
784 } end_sortSet_elements;
817 /*@=loopswitchbreak@*/