/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** under the terms of the GNU General Public License as published by the
** Free Software Foundation; either version 2 of the License, or (at your
** option) any later version.
**
** This program is distributed in the hope that it will be useful, but
** WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
** General Public License for more details.
**
** The GNU General Public License is available from http://www.gnu.org/ or
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
** For information on splint: info@splint.org
** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/
/*
** checking.c
**
** sort checking.
**
** AUTHOR:
** Yang Meng Tan,
** Massachusetts Institute of Technology
*/
# include "splintMacros.nf"
# include "basic.h"
# include "llgrammar.h"
# include "checking.h"
# include "lclscan.h"
/*@+ignorequals@*/
static /*@only@*/ cstring printBadArgs (sortSetList p_args);
static /*@only@*/ sortSet
standardOperators (/*@null@*/ nameNode p_n, sortSetList p_argSorts, sort p_q);
static bool isStandardOperator (/*@null@*/ nameNode p_n);
static void assignSorts (termNode p_t, sort p_s);
/*@null@*/ termNode
computePossibleSorts (/*@returned@*/ /*@null@*/ termNode t)
{
ltoken errtok;
if (t != (termNode) 0)
{
switch (t->kind)
{
case TRM_LITERAL:
case TRM_CONST:
case TRM_VAR:
case TRM_ZEROARY:
case TRM_SIZEOF:
case TRM_UNCHANGEDALL:
case TRM_UNCHANGEDOTHERS:
case TRM_QUANTIFIER:
break;
case TRM_APPLICATION:
{
bool fail = FALSE;
sortSetList argSorts = sortSetList_new ();
lslOpSet ops;
sortSet standards;
if (termNodeList_size (t->args) != 0)
{
termNodeList_elements (t->args, arg)
{
(void) computePossibleSorts (arg);
if (sortSet_size (arg->possibleSorts) == 0)
{
fail = TRUE;
}
else
{
sortSetList_addh (argSorts, arg->possibleSorts);
}
} end_termNodeList_elements;
if (fail)
{
lslOpSet_free (t->possibleOps);
sortSetList_free (argSorts);
t->possibleOps = lslOpSet_new ();
return t;
}
}
ops = symtable_opsWithLegalDomain (g_symtab, t->name, argSorts, t->given);
lslOpSet_free (t->possibleOps);
t->possibleOps = ops;
lslOpSet_elements (t->possibleOps, op)
{
sort sort;
sort = sigNode_rangeSort (op->signature);
(void) sortSet_insert (t->possibleSorts, sort);
} end_lslOpSet_elements;
standards = standardOperators (t->name, argSorts, t->given);
sortSet_elements (standards, el)
{
(void) sortSet_insert (t->possibleSorts, el);
} end_sortSet_elements;
sortSet_free (standards);
if (!(t->error_reported) && sortSet_size (t->possibleSorts) == 0)
{
unsigned int arity = termNodeList_size (t->args);
errtok = nameNode_errorToken (t->name);
/* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
if (isStandardOperator (t->name))
{
lclerror (errtok,
message ("Type error: %q not declared for %q",
nameNode_unparse (t->name), printBadArgs (argSorts)));
}
else if (t->name != NULL
&& symtable_opExistsWithArity (g_symtab, t->name, arity))
{
sigNodeSet possibleOps = symtable_possibleOps (g_symtab, t->name);
cstring opName = nameNode_unparse (t->name);
/*
** all these will be standardOperators soon...
*/
if (cstring_equalLit (opName, "__ [__]"))
{
lclerror (errtok,
message ("Type error: %q not declared for %q",
opName, printBadArgs (argSorts)));
}
else
{
lclerror (errtok,
message ("Type error: %q declared: %q\ngiven: %q",
opName,
sigNodeSet_unparseSomeSigs (possibleOps),
printBadArgs (argSorts)));
}
}
else
{
sigNodeSet possibleOps;
int npossibleOps;
llassert (t->name != NULL);
possibleOps = symtable_possibleOps (g_symtab, t->name);
npossibleOps = sigNodeSet_size (possibleOps);
/*
** evs --- check is it is wrong arity...
*/
if (npossibleOps == 0)
{
lclerror
(errtok,
message ("Undeclared operator: %q", nameNode_unparse (t->name)));
}
else
{
lclerror
(errtok,
message ("Operator %q declared for %q arguments, given %d",
nameNode_unparse (t->name),
sigNodeSet_unparsePossibleAritys (possibleOps),
arity));
}
}
t->error_reported = TRUE;
}
sortSetList_free (argSorts);
break;
}
}
}
return t;
}
static /*@only@*/ cstring
printBadArgs (sortSetList args)
{
if (sortSetList_size (args) == 1)
{
return (sortSet_unparseOr (sortSetList_head (args)));
}
else
{
cstring s = cstring_undefined;
int argno = 1;
sortSetList_elements (args, ss)
{
if (argno == 1)
s = message ("arg %d: %q", argno, sortSet_unparseOr (ss));
else
s = message ("%q; arg %d: %q", s, argno, sortSet_unparseOr (ss));
argno++;
} end_sortSetList_elements;
return s;
}
}
termNode
checkSort (/*@returned@*/ termNode t)
{
sortSet sorts;
sort theSort;
int size;
ltoken errtok;
(void) computePossibleSorts (t);
sorts = t->possibleSorts;
llassert (sortSet_isDefined (sorts));
size = sortSet_size (sorts);
switch (size)
{
case 0: /* complain later */
break;
case 1: /* just right */
theSort = sortSet_choose (sorts);
assignSorts (t, theSort);
break;
default:
/* we allow C literals to have multiple sorts */
if (t->kind != TRM_LITERAL)
{
errtok = termNode_errorToken (t);
t->error_reported = TRUE;
lclerror (errtok,
message ("Term %q: can have more than one possible type. Possible types: %q",
termNode_unparse (t), sortSet_unparseClean (sorts)));
}
}
return t;
}
static void
assignSorts (termNode t, sort s)
{
/* other kinds are already assigned bottom-up */
ltoken errtok;
switch (t->kind)
{
case TRM_ZEROARY: /* pick s to be the sort chosen */
case TRM_LITERAL:
sortSet_elements (t->possibleSorts, s2)
{
if (sort_equal (s2, s))
{
sortSet_free (t->possibleSorts);
t->possibleSorts = sortSet_new ();
(void) sortSet_insert (t->possibleSorts, s);
t->sort = s;
}
return;
} end_sortSet_elements;
break;
case TRM_APPLICATION:
{
lslOpSet sigs = t->possibleOps;
lslOpSet oldops = lslOpSet_undefined;
sigNode op = (sigNode) 0;
nameNode name = t->name;
termNodeList args = t->args;
bool found = FALSE;
errtok = nameNode_errorToken (name);
/* why compute again? to check for duplicates */
lslOpSet_elements (sigs, sig)
{
sort rsort = sigNode_rangeSort (sig->signature);
if (sort_equal (s, rsort))
{
lslOp iop;
if (found)
{
t->error_reported = TRUE;
lclerror (errtok,
message ("Ambiguous operator %q: %q or %q",
nameNode_unparse (name),
sigNode_unparse (op),
sigNode_unparse (sig->signature)));
return;
}
iop = (lslOp) dmalloc (sizeof (*iop));
found = TRUE;
op = sig->signature;
oldops = t->possibleOps;
t->possibleOps = lslOpSet_new ();
iop->name = nameNode_copy (name);
iop->signature = op;
(void) lslOpSet_insert (t->possibleOps, iop);
t->sort = s;
/*@-branchstate@*/
}
/*@=branchstate@*/
} end_lslOpSet_elements;
lslOpSet_free (oldops);
if (!found)
{
if (sortSet_size (t->possibleSorts) == 1)
{
t->sort = sortSet_choose (t->possibleSorts);
}
else
{
/* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
t->error_reported = TRUE;
lclerror (errtok, message ("Operator not found: %q",
nameNode_unparse (name)));
/* evs --- ??? */
}
return;
}
if (termNodeList_empty (args))
{
if (op != (sigNode) 0)
{
/* was --- NB: copy to avoid interference */
/* shouldn't need to copy --- its a fresh list */
sortList dom = sigNode_domain (op);
sortList_reset (dom);
termNodeList_elements (args, arg)
{
assignSorts (arg, sortList_current (dom));
sortList_advance (dom);
} end_termNodeList_elements;
sortList_free (dom);
}
else
{
errtok = nameNode_errorToken (name);
/* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
t->error_reported = TRUE;
lclerror (errtok, message ("No matching operator: %q",
nameNode_unparse (name)));
}
return;
}
break;
}
default: /* do nothing */
break;
}
}
void
checkLclPredicate (ltoken t, lclPredicateNode n)
{
sort theSort;
if ((n == NULL) || (n->predicate == NULL))
{
llcontbuglit ("checkLclPredicate expects valid lclPredicate. "
"Skipping current check");
return;
}
/* check only if there are no previous errors */
if (!n->predicate->error_reported)
{
/* check that the sort of n is boolean */
theSort = n->predicate->sort;
if (!sort_compatible (theSort, g_sortCapBool))
{
if (sort_isNoSort (theSort))
{
; /* "Expects a boolean term. Given term has unknown sort" */
}
else
{
cstring clauset = ltoken_getRawString (t);
if (cstring_firstChar (clauset) == '(')
{
clauset = cstring_makeLiteral ("Equality");
}
else
{
/* uppercase first letter */
clauset = cstring_copy (clauset);
cstring_setChar (clauset, 1,
(char) toupper (cstring_firstChar (clauset)));
}
lclerror (t, message ("%q expects a boolean term, given %q.",
clauset, sort_unparse (theSort)));
}
}
}
}
/*
** these should not be doing string comparisons!
*/
static bool isDeRefOperator (cstring s)
{
return (cstring_equalLit (s, "*"));
}
static bool isStateOperator (cstring s)
{
return (cstring_equalLit (s, "^") ||
cstring_equalLit (s, "'") ||
cstring_equalLit (s, "\\any") ||
cstring_equalLit (s, "\\pre") ||
cstring_equalLit (s, "\\post"));
}
static bool isCompareOperator (cstring s) /* YUCK!!! */
{
return (cstring_equalLit (s, "\\eq") ||
cstring_equalLit (s, "\\neq") ||
cstring_equalLit (s, "=") ||
cstring_equalLit (s, "!=") ||
cstring_equalLit (s, "~=") ||
cstring_equalLit (s, "=="));
}
static bool isStandardOperator (/*@null@*/ nameNode n)
{
if (n != (nameNode) 0)
{
if (!n->isOpId)
{
opFormNode opf = n->content.opform;
llassert (opf != NULL);
switch (opf->kind)
{
case OPF_IF: return TRUE;
case OPF_ANYOP:
break;
case OPF_MANYOP:
{
cstring s = ltoken_getRawString (opf->content.anyop);
if (isStateOperator (s)) return TRUE;
return FALSE;
}
case OPF_ANYOPM:
/* operator: *__ */
{
cstring s = ltoken_getRawString (opf->content.anyop);
return (isDeRefOperator (s));
}
case OPF_MANYOPM:
{
cstring s = ltoken_getRawString (opf->content.anyop);
return (isCompareOperator (s));
}
case OPF_MIDDLE:
break;
case OPF_MMIDDLE:
break;
case OPF_MIDDLEM:
break;
case OPF_MMIDDLEM:
break;
case OPF_BMIDDLE:
break;
case OPF_BMMIDDLE:
break;
case OPF_BMIDDLEM:
break;
case OPF_BMMIDDLEM:
break;
case OPF_SELECT:
break;
case OPF_MAP:
break;
case OPF_MSELECT:
break;
case OPF_MMAP:
break;
default:
break;
}
}
else
{
int code = ltoken_getCode (n->content.opid);
if (code == simpleId)
{
cstring text = nameNode_unparse (n);
bool ret = (cstring_equalLit (text, "trashed")
|| cstring_equalLit (text, "maxIndex")
|| cstring_equalLit (text, "minIndex")
|| cstring_equalLit (text, "isSub"));
cstring_free (text);
return ret;
}
return (code == LLT_MODIFIES || code == LLT_FRESH
|| code == LLT_UNCHANGED || code == LLT_SIZEOF);
}
}
return FALSE;
}
static /*@only@*/ sortSet
standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sort q)
{
sortSet argSet;
sortSet ret = sortSet_new ();
if (n == (nameNode) 0) return ret;
if (n->isOpId)
{
int code = ltoken_getCode (n->content.opid);
if (sortSetList_size (argSorts) == 1)
{
sortSetList_reset (argSorts);
argSet = sortSetList_current (argSorts);
sortSet_elements (argSet, current)
{
sortNode sn;
sn = sort_quietLookup (current);
while (sn->kind == SRT_SYN)
{
sn = sort_quietLookup (sn->baseSort);
}
/*@-loopswitchbreak@*/
switch (code)
{
case simpleId:
{
cstring text = ltoken_getRawString (n->content.opid);
if (cstring_equalLit (text, "trashed")) /* GACK! */
{
if (sn->kind == SRT_OBJ ||
sn->kind == SRT_ARRAY)
(void) sortSet_insert (ret, g_sortBool);
}
if (cstring_equalLit (text, "maxIndex") ||
cstring_equalLit (text, "minIndex"))
{
if (sn->kind == SRT_ARRAY || sn->kind == SRT_PTR)
(void) sortSet_insert (ret, g_sortInt);
/* if (lsymbol_fromChars ("maxIndex") */
}
}
break;
case LLT_MODIFIES:
case LLT_FRESH:
case LLT_UNCHANGED:
if (sn->kind == SRT_OBJ ||
sn->kind == SRT_ARRAY)
{
(void) sortSet_insert (ret, g_sortBool);
}
break;
case LLT_SIZEOF:
if (sn->kind == SRT_OBJ ||
sn->kind == SRT_ARRAY ||
sn->kind == SRT_VECTOR)
(void) sortSet_insert (ret, g_sortInt);
break;
default:
break;
}
} end_sortSet_elements;
}
}
else
{
opFormNode opf = n->content.opform;
llassert (opf != NULL);
switch (opf->kind)
{
case OPF_IF:
/*
** if __ then __ else __ : bool, S, S -> S
** is defined for all sorts
*/
if (sortSetList_size (argSorts) == 3)
{
argSet = sortSetList_head (argSorts);
if (sortSet_member (argSet, g_sortBool))
{
sortSetList_reset (argSorts);
sortSetList_advance (argSorts);
argSet = sortSetList_current (argSorts);
if (sortSet_size (argSet) == 1)
{
sort clause = sortSet_choose (argSet);
sort clause2;
sortSetList_advance (argSorts);
argSet = sortSetList_current (argSorts);
clause2 = sortSet_choose (argSet);
if (sortSet_size (argSet) == 1 &&
sort_equal (clause, clause2))
{
(void) sortSet_insert (ret, clause);
}
}
}
}
break;
case OPF_MANYOP:
{
cstring s = ltoken_getRawString (opf->content.anyop);
if (isStateOperator (s))
{
if (sortSetList_size (argSorts) == 1)
{
sortSetList_reset (argSorts);
argSet = sortSetList_current (argSorts);
sortSet_elements (argSet, current)
{
sortNode sn;
sn = sort_quietLookup (current);
while (sn->kind == SRT_SYN)
{
sn = sort_quietLookup (sn->baseSort);
}
switch (sn->kind)
{
case SRT_OBJ:
(void) sortSet_insert (ret, sn->baseSort);
break;
case SRT_ARRAY:
(void) sortSet_insert (ret,
sort_makeVec (ltoken_undefined, current));
break;
case SRT_STRUCT:
(void) sortSet_insert (ret,
sort_makeTuple (ltoken_undefined, current));
break;
case SRT_UNION:
(void) sortSet_insert (ret,
sort_makeUnionVal (ltoken_undefined, current));
break;
case SRT_TUPLE:
case SRT_UNIONVAL:
case SRT_ENUM:
case SRT_LAST:
case SRT_FIRST:
case SRT_NONE:
case SRT_HOF:
case SRT_PRIM:
case SRT_PTR:
case SRT_VECTOR:
break;
case SRT_SYN:
llbuglit ("standardOperators: Synonym in switch");
}
} end_sortSet_elements ;
}
}
}
break;
case OPF_ANYOPM:
/* operator: *__ */
{
cstring s = ltoken_getRawString (opf->content.anyop);
if (isDeRefOperator (s))
{
if (sortSetList_size (argSorts) == 1)
{
sortSetList_reset (argSorts);
argSet = sortSetList_current (argSorts);
sortSet_elements (argSet, current)
{
sortNode sn;
sn = sort_quietLookup (current);
while (sn->kind == SRT_SYN)
{
sn = sort_quietLookup (sn->baseSort);
}
if (sn->kind == SRT_PTR)
{
(void) sortSet_insert (ret, sn->baseSort);
}
} end_sortSet_elements;
}
}
}
break;
case OPF_ANYOP:
break;
case OPF_MANYOPM:
{
cstring s = ltoken_getRawString (opf->content.anyop);
if (isCompareOperator (s))
{
if (sortSetList_size (argSorts) == 2)
{
sortSet argSet2;
sortSetList_reset (argSorts);
argSet = sortSetList_current (argSorts);
sortSetList_advance (argSorts);
argSet2 = sortSetList_current (argSorts);
if (sortSet_size (argSet) == 1)
{
sortSet_elements (argSet, cl)
{
sortSet_elements (argSet2, cl2)
{
if (sort_equal (cl, cl2))
{
(void) sortSet_insert (ret, g_sortBool);
}
} end_sortSet_elements;
} end_sortSet_elements;
}
}
}
}
break;
case OPF_MIDDLE:
break;
case OPF_MMIDDLE:
break;
case OPF_MIDDLEM:
break;
case OPF_MMIDDLEM:
break;
case OPF_BMIDDLE:
break;
case OPF_BMMIDDLE:
break;
case OPF_BMIDDLEM:
break;
case OPF_BMMIDDLEM:
break;
case OPF_SELECT:
break;
case OPF_MAP:
break;
case OPF_MSELECT:
break;
case OPF_MMAP:
break;
default:
break;
}
/*@=loopswitchbreak@*/
}
return ret;
}
syntax highlighted by Code2HTML, v. 0.9.1