[splint.git] / src / checking.c

/*
** 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 "llbasic.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;
}
Commit	Line	Data
616915dd	1	/*
11db3170	2	** Splint - annotation-assisted static program checker
c59f5181	3	** Copyright (C) 1994-2003 University of Virginia,
616915dd	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	**
155af98d	20	** For information on splint: info@splint.org
155af98d	21	** To report a bug: splint-bug@splint.org
11db3170	22	** For more information: http://www.splint.org
616915dd	23	*/
	24	/*
	25	** checking.c
	26	**
	27	** sort checking.
	28	**
	29	** AUTHOR:
	30	** Yang Meng Tan,
	31	** Massachusetts Institute of Technology
	32	*/
	33
1b8ae690	34	# include "splintMacros.nf"
616915dd	35	# include "llbasic.h"
	36	# include "llgrammar.h"
	37	# include "checking.h"
	38	# include "lclscan.h"
	39
	40	/@+ignorequals@/
	41
	42	static /@only@/ cstring printBadArgs (sortSetList p_args);
	43	static /@only@/ sortSet
53306cab	44	standardOperators (/@null@/ nameNode p_n, sortSetList p_argSorts, sort p_q);
616915dd	45	static bool isStandardOperator (/@null@/ nameNode p_n);
	46	static void assignSorts (termNode p_t, sort p_s);
	47
	48	/@null@/ termNode
	49	computePossibleSorts (/@returned@/ /@null@/ termNode t)
	50	{
	51	ltoken errtok;
	52
	53	if (t != (termNode) 0)
	54	{
	55	switch (t->kind)
	56	{
	57	case TRM_LITERAL:
	58	case TRM_CONST:
	59	case TRM_VAR:
	60	case TRM_ZEROARY:
	61	case TRM_SIZEOF:
	62	case TRM_UNCHANGEDALL:
	63	case TRM_UNCHANGEDOTHERS:
	64	case TRM_QUANTIFIER:
	65	break;
	66	case TRM_APPLICATION:
	67	{
	68	bool fail = FALSE;
	69	sortSetList argSorts = sortSetList_new ();
	70	lslOpSet ops;
	71	sortSet standards;
	72
	73	if (termNodeList_size (t->args) != 0)
	74	{
	75	termNodeList_elements (t->args, arg)
	76	{
	77	(void) computePossibleSorts (arg);
	78
	79	if (sortSet_size (arg->possibleSorts) == 0)
	80	{
	81	fail = TRUE;
	82	}
	83	else
	84	{
	85	sortSetList_addh (argSorts, arg->possibleSorts);
	86	}
	87	} end_termNodeList_elements;
	88
	89	if (fail)
	90	{
	91	lslOpSet_free (t->possibleOps);
	92	sortSetList_free (argSorts);
	93	t->possibleOps = lslOpSet_new ();
	94	return t;
	95	}
	96	}
	97
	98	ops = symtable_opsWithLegalDomain (g_symtab, t->name, argSorts, t->given);
	99	lslOpSet_free (t->possibleOps);
	100	t->possibleOps = ops;
	101
	102	lslOpSet_elements (t->possibleOps, op)
	103	{
	104	sort sort;
	105	sort = sigNode_rangeSort (op->signature);
	106	(void) sortSet_insert (t->possibleSorts, sort);
	107	} end_lslOpSet_elements;
	108
109	standards = standardOperators (t->name, argSorts, t->given);
110
111	sortSet_elements (standards, el)
112	{
113	(void) sortSet_insert (t->possibleSorts, el);
114	} end_sortSet_elements;
115
116	sortSet_free (standards);
117
118	if (!(t->error_reported) && sortSet_size (t->possibleSorts) == 0)
119	{
120	unsigned int arity = termNodeList_size (t->args);
121	errtok = nameNode_errorToken (t->name);
122
28bf4b0b	123	/* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
616915dd	124
	125	if (isStandardOperator (t->name))
	126	{
	127	lclerror (errtok,
	128	message ("Type error: %q not declared for %q",
	129	nameNode_unparse (t->name), printBadArgs (argSorts)));
	130	}
	131	else if (t->name != NULL
	132	&& symtable_opExistsWithArity (g_symtab, t->name, arity))
	133	{
	134	sigNodeSet possibleOps = symtable_possibleOps (g_symtab, t->name);
	135	cstring opName = nameNode_unparse (t->name);
	136
	137	/*
	138	** all these will be standardOperators soon...
	139	*/
	140
	141	if (cstring_equalLit (opName, "__ [__]"))
	142	{
	143	lclerror (errtok,
	144	message ("Type error: %q not declared for %q",
	145	opName, printBadArgs (argSorts)));
	146	}
	147	else
	148	{
	149	lclerror (errtok,
	150	message ("Type error: %q declared: %q\ngiven: %q",
	151	opName,
	152	sigNodeSet_unparseSomeSigs (possibleOps),
	153	printBadArgs (argSorts)));
	154	}
	155	}
	156	else
	157	{
	158	sigNodeSet possibleOps;
	159	int npossibleOps;
	160
	161	llassert (t->name != NULL);
	162
	163	possibleOps = symtable_possibleOps (g_symtab, t->name);
	164	npossibleOps = sigNodeSet_size (possibleOps);
	165
	166	/*
	167	** evs --- check is it is wrong arity...
	168	*/
	169
	170	if (npossibleOps == 0)
	171	{
	172	lclerror
	173	(errtok,
	174	message ("Undeclared operator: %q", nameNode_unparse (t->name)));
	175	}
	176	else
	177	{
	178	lclerror
	179	(errtok,
	180	message ("Operator %q declared for %q arguments, given %d",
	181	nameNode_unparse (t->name),
	182	sigNodeSet_unparsePossibleAritys (possibleOps),
	183	arity));
	184	}
	185	}
	186	t->error_reported = TRUE;
	187	}
188	sortSetList_free (argSorts);
189	break;
190	}
191	}
192	}
193
194	return t;
195	}
196
197	static /@only@/ cstring
198	printBadArgs (sortSetList args)
199	{
200	if (sortSetList_size (args) == 1)
201	{
202	return (sortSet_unparseOr (sortSetList_head (args)));
203	}
204	else
205	{
206	cstring s = cstring_undefined;
207	int argno = 1;
208
209	sortSetList_elements (args, ss)
210	{
211	if (argno == 1)
212	s = message ("arg %d: %q", argno, sortSet_unparseOr (ss));
213	else
214	s = message ("%q; arg %d: %q", s, argno, sortSet_unparseOr (ss));
215	argno++;
216	} end_sortSetList_elements;
217
218	return s;
219	}
220	}
221
222	termNode
223	checkSort (/@returned@/ termNode t)
224	{
225	sortSet sorts;
226	sort theSort;
227	int size;
228	ltoken errtok;
229
230	(void) computePossibleSorts (t);
231	sorts = t->possibleSorts;
232
233	llassert (sortSet_isDefined (sorts));
234
235	size = sortSet_size (sorts);
236	switch (size)
237	{
238	case 0: /* complain later */
239	break;
240	case 1: /* just right */
241	theSort = sortSet_choose (sorts);
242	assignSorts (t, theSort);
243	break;
244	default:
245	/* we allow C literals to have multiple sorts */
246	if (t->kind != TRM_LITERAL)
247	{
248	errtok = termNode_errorToken (t);
249	t->error_reported = TRUE;
250
251	lclerror (errtok,
252	message ("Term %q: can have more than one possible type. Possible types: %q",
253	termNode_unparse (t), sortSet_unparseClean (sorts)));
254	}
255	}
256	return t;
257	}
258
259	static void
260	assignSorts (termNode t, sort s)
261	{
262	/* other kinds are already assigned bottom-up */
263	ltoken errtok;
264
265	switch (t->kind)
266	{
267	case TRM_ZEROARY: /* pick s to be the sort chosen */
268	case TRM_LITERAL:
269	sortSet_elements (t->possibleSorts, s2)
270	{
28bf4b0b	271	if (sort_equal (s2, s))
616915dd	272	{
	273	sortSet_free (t->possibleSorts);
	274	t->possibleSorts = sortSet_new ();
	275	(void) sortSet_insert (t->possibleSorts, s);
	276	t->sort = s;
	277	}
	278	return;
	279	} end_sortSet_elements;
	280	break;
	281	case TRM_APPLICATION:
	282	{
	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;
	288	bool found = FALSE;
	289
	290	errtok = nameNode_errorToken (name);
	291
	292	/* why compute again? to check for duplicates */
	293	lslOpSet_elements (sigs, sig)
	294	{
	295	sort rsort = sigNode_rangeSort (sig->signature);
	296
28bf4b0b	297	if (sort_equal (s, rsort))
616915dd	298	{
	299	lslOp iop;
	300
	301	if (found)
	302	{
	303	t->error_reported = TRUE;
	304
	305	lclerror (errtok,
	306	message ("Ambiguous operator %q: %q or %q",
	307	nameNode_unparse (name),
	308	sigNode_unparse (op),
	309	sigNode_unparse (sig->signature)));
	310	return;
	311	}
	312
	313	iop = (lslOp) dmalloc (sizeof (*iop));
	314	found = TRUE;
	315	op = sig->signature;
	316
	317	oldops = t->possibleOps;
	318	t->possibleOps = lslOpSet_new ();
	319	iop->name = nameNode_copy (name);
	320	iop->signature = op;
	321	(void) lslOpSet_insert (t->possibleOps, iop);
	322	t->sort = s;
	323	/@-branchstate@/
	324	}
	325	/@=branchstate@/
	326	} end_lslOpSet_elements;
	327
	328	lslOpSet_free (oldops);
	329
	330	if (!found)
	331	{
	332	if (sortSet_size (t->possibleSorts) == 1)
	333	{
	334	t->sort = sortSet_choose (t->possibleSorts);
	335	}
	336	else
	337	{
28bf4b0b	338	/* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
616915dd	339	t->error_reported = TRUE;
	340
	341	lclerror (errtok, message ("Operator not found: %q",
	342	nameNode_unparse (name)));
	343	/* evs --- ??? */
	344	}
	345	return;
	346	}
	347
	348	if (termNodeList_empty (args))
	349	{
	350	if (op != (sigNode) 0)
	351	{
	352	/* was --- NB: copy to avoid interference */
	353	/* shouldn't need to copy --- its a fresh list */
	354	sortList dom = sigNode_domain (op);
	355
	356	sortList_reset (dom);
	357	termNodeList_elements (args, arg)
	358	{
	359	assignSorts (arg, sortList_current (dom));
	360	sortList_advance (dom);
	361	} end_termNodeList_elements;
	362
	363	sortList_free (dom);
	364	}
	365	else
	366	{
	367	errtok = nameNode_errorToken (name);
28bf4b0b	368	/* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
616915dd	369	t->error_reported = TRUE;
	370
	371	lclerror (errtok, message ("No matching operator: %q",
	372	nameNode_unparse (name)));
	373	}
	374	return;
	375	}
	376	break;
	377	}
	378	default: /* do nothing */
	379	break;
	380	}
	381	}
	382
	383	void
	384	checkLclPredicate (ltoken t, lclPredicateNode n)
	385	{
	386	sort theSort;
	387
	388	if ((n == NULL) \|\| (n->predicate == NULL))
	389	{
	390	llcontbuglit ("checkLclPredicate expects valid lclPredicate. "
	391	"Skipping current check");
	392	return;
	393	}
	394
	395	/* check only if there are no previous errors */
	396
	397	if (!n->predicate->error_reported)
	398	{
	399	/* check that the sort of n is boolean */
	400	theSort = n->predicate->sort;
2a6e9c30	401	if (!sort_compatible (theSort, g_sortCapBool))
616915dd	402	{
	403	if (sort_isNoSort (theSort))
	404	{
	405	; /* "Expects a boolean term. Given term has unknown sort" */
	406	}
	407	else
	408	{
	409	cstring clauset = ltoken_getRawString (t);
	410
	411	if (cstring_firstChar (clauset) == '(')
	412	{
	413	clauset = cstring_makeLiteral ("Equality");
	414	}
	415	else
	416	{
	417	/* uppercase first letter */
	418	clauset = cstring_copy (clauset);
	419	cstring_setChar (clauset, 1,
	420	(char) toupper (cstring_firstChar (clauset)));
	421	}
	422
	423	lclerror (t, message ("%q expects a boolean term, given %q.",
	424	clauset, sort_unparse (theSort)));
	425
	426	}
	427	}
	428	}
	429	}
	430
	431	/*
	432	** these should not be doing string comparisons!
	433	*/
	434
	435	static bool isDeRefOperator (cstring s)
	436	{
	437	return (cstring_equalLit (s, "*"));
	438	}
	439
	440	static bool isStateOperator (cstring s)
	441	{
	442	return (cstring_equalLit (s, "^") \|\|
	443	cstring_equalLit (s, "'") \|\|
	444	cstring_equalLit (s, "\\any") \|\|
	445	cstring_equalLit (s, "\\pre") \|\|
	446	cstring_equalLit (s, "\\post"));
	447	}
	448
	449	static bool isCompareOperator (cstring s) /* YUCK!!! */
	450	{
	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, "=="));
	457	}
	458
	459	static bool isStandardOperator (/@null@/ nameNode n)
	460	{
	461	if (n != (nameNode) 0)
	462	{
	463	if (!n->isOpId)
	464	{
	465	opFormNode opf = n->content.opform;
466
467	llassert (opf != NULL);
468
469	switch (opf->kind)
470	{
471	case OPF_IF: return TRUE;
472	case OPF_ANYOP:
473	break;
474	case OPF_MANYOP:
475	{
476	cstring s = ltoken_getRawString (opf->content.anyop);
477
478	if (isStateOperator (s)) return TRUE;
479	return FALSE;
480	}
481	case OPF_ANYOPM:
482	/* operator: __ /
483	{
484	cstring s = ltoken_getRawString (opf->content.anyop);
485
486	return (isDeRefOperator (s));
487	}
488	case OPF_MANYOPM:
489	{
490	cstring s = ltoken_getRawString (opf->content.anyop);
491
492	return (isCompareOperator (s));
493	}
494	case OPF_MIDDLE:
495	break;
496	case OPF_MMIDDLE:
497	break;
498	case OPF_MIDDLEM:
499	break;
500	case OPF_MMIDDLEM:
501	break;
502	case OPF_BMIDDLE:
503	break;
504	case OPF_BMMIDDLE:
505	break;
506	case OPF_BMIDDLEM:
507	break;
508	case OPF_BMMIDDLEM:
509	break;
510	case OPF_SELECT:
511	break;
512	case OPF_MAP:
513	break;
514	case OPF_MSELECT:
515	break;
516	case OPF_MMAP:
517	break;
518	default:
519	break;
520	}
521	}
522	else
523	{
524	int code = ltoken_getCode (n->content.opid);
525
526	if (code == simpleId)
527	{
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"));
533
534	cstring_free (text);
535	return ret;
536	}
537
538	return (code == LLT_MODIFIES \|\| code == LLT_FRESH
539	\|\| code == LLT_UNCHANGED \|\| code == LLT_SIZEOF);
540	}
541	}
542	return FALSE;
543	}
544
545	static /@only@/ sortSet
53306cab	546	standardOperators (/@null@/ nameNode n, sortSetList argSorts, /@unused@/ sort q)
616915dd	547	{
	548	sortSet argSet;
	549	sortSet ret = sortSet_new ();
	550
	551	if (n == (nameNode) 0) return ret;
	552
	553	if (n->isOpId)
	554	{
	555	int code = ltoken_getCode (n->content.opid);
	556
	557	if (sortSetList_size (argSorts) == 1)
	558	{
	559	sortSetList_reset (argSorts);
	560
	561	argSet = sortSetList_current (argSorts);
	562
	563	sortSet_elements (argSet, current)
	564	{
	565	sortNode sn;
	566
	567	sn = sort_quietLookup (current);
	568
28bf4b0b	569	while (sn->kind == SRT_SYN)
616915dd	570	{
28bf4b0b	571	sn = sort_quietLookup (sn->baseSort);
616915dd	572	}
	573
	574	/@-loopswitchbreak@/
	575	switch (code)
	576	{
	577	case simpleId:
	578	{
	579	cstring text = ltoken_getRawString (n->content.opid);
	580
	581	if (cstring_equalLit (text, "trashed")) /* GACK! */
	582	{
28bf4b0b	583	if (sn->kind == SRT_OBJ \|\|
28bf4b0b	584	sn->kind == SRT_ARRAY)
2a6e9c30	585	(void) sortSet_insert (ret, g_sortBool);
616915dd	586	}
	587
	588	if (cstring_equalLit (text, "maxIndex") \|\|
	589	cstring_equalLit (text, "minIndex"))
	590	{
28bf4b0b	591	if (sn->kind == SRT_ARRAY \|\| sn->kind == SRT_PTR)
2a6e9c30	592	(void) sortSet_insert (ret, g_sortInt);
616915dd	593
	594	/* if (lsymbol_fromChars ("maxIndex") */
	595	}
	596	}
	597	break;
	598	case LLT_MODIFIES:
	599	case LLT_FRESH:
	600	case LLT_UNCHANGED:
28bf4b0b	601	if (sn->kind == SRT_OBJ \|\|
28bf4b0b	602	sn->kind == SRT_ARRAY)
616915dd	603	{
2a6e9c30	604	(void) sortSet_insert (ret, g_sortBool);
616915dd	605	}
	606	break;
	607	case LLT_SIZEOF:
28bf4b0b	608	if (sn->kind == SRT_OBJ \|\|
	609	sn->kind == SRT_ARRAY \|\|
	610	sn->kind == SRT_VECTOR)
2a6e9c30	611	(void) sortSet_insert (ret, g_sortInt);
616915dd	612	break;
	613	default:
	614	break;
	615	}
	616	} end_sortSet_elements;
	617	}
	618	}
	619	else
	620	{
	621	opFormNode opf = n->content.opform;
	622
	623	llassert (opf != NULL);
	624
	625	switch (opf->kind)
	626	{
	627	case OPF_IF:
	628	/*
	629	** if __ then __ else __ : bool, S, S -> S
	630	** is defined for all sorts
	631	*/
	632
	633	if (sortSetList_size (argSorts) == 3)
	634	{
	635	argSet = sortSetList_head (argSorts);
	636
2a6e9c30	637	if (sortSet_member (argSet, g_sortBool))
616915dd	638	{
	639	sortSetList_reset (argSorts);
	640	sortSetList_advance (argSorts);
	641
	642	argSet = sortSetList_current (argSorts);
	643
	644	if (sortSet_size (argSet) == 1)
	645	{
	646	sort clause = sortSet_choose (argSet);
	647	sort clause2;
	648
	649	sortSetList_advance (argSorts);
	650	argSet = sortSetList_current (argSorts);
	651
	652	clause2 = sortSet_choose (argSet);
	653
	654	if (sortSet_size (argSet) == 1 &&
28bf4b0b	655	sort_equal (clause, clause2))
616915dd	656	{
	657	(void) sortSet_insert (ret, clause);
	658	}
	659	}
	660	}
	661	}
	662	break;
	663	case OPF_MANYOP:
	664	{
	665	cstring s = ltoken_getRawString (opf->content.anyop);
	666
	667	if (isStateOperator (s))
	668	{
	669	if (sortSetList_size (argSorts) == 1)
	670	{
	671	sortSetList_reset (argSorts);
	672
	673	argSet = sortSetList_current (argSorts);
	674
	675	sortSet_elements (argSet, current)
	676	{
	677	sortNode sn;
	678
	679	sn = sort_quietLookup (current);
	680
28bf4b0b	681	while (sn->kind == SRT_SYN)
616915dd	682	{
28bf4b0b	683	sn = sort_quietLookup (sn->baseSort);
616915dd	684	}
616915dd	685
28bf4b0b	686	switch (sn->kind)
616915dd	687	{
616915dd	688	case SRT_OBJ:
28bf4b0b	689	(void) sortSet_insert (ret, sn->baseSort);
616915dd	690	break;
	691	case SRT_ARRAY:
	692	(void) sortSet_insert (ret,
	693	sort_makeVec (ltoken_undefined, current));
	694	break;
	695	case SRT_STRUCT:
	696	(void) sortSet_insert (ret,
	697	sort_makeTuple (ltoken_undefined, current));
	698	break;
	699	case SRT_UNION:
	700	(void) sortSet_insert (ret,
	701	sort_makeUnionVal (ltoken_undefined, current));
	702	break;
	703	case SRT_TUPLE:
	704	case SRT_UNIONVAL:
	705	case SRT_ENUM:
	706	case SRT_LAST:
	707	case SRT_FIRST:
	708	case SRT_NONE:
	709	case SRT_HOF:
	710	case SRT_PRIM:
	711	case SRT_PTR:
	712	case SRT_VECTOR:
	713	break;
	714	case SRT_SYN:
	715	llbuglit ("standardOperators: Synonym in switch");
	716	}
	717	} end_sortSet_elements ;
	718	}
	719	}
	720	}
	721	break;
	722	case OPF_ANYOPM:
	723	/* operator: __ /
	724	{
	725	cstring s = ltoken_getRawString (opf->content.anyop);
	726
	727	if (isDeRefOperator (s))
	728	{
	729	if (sortSetList_size (argSorts) == 1)
	730	{
	731	sortSetList_reset (argSorts);
	732
	733	argSet = sortSetList_current (argSorts);
	734
	735	sortSet_elements (argSet, current)
	736	{
	737	sortNode sn;
	738
	739	sn = sort_quietLookup (current);
	740
28bf4b0b	741	while (sn->kind == SRT_SYN)
616915dd	742	{
28bf4b0b	743	sn = sort_quietLookup (sn->baseSort);
616915dd	744	}
616915dd	745
28bf4b0b	746	if (sn->kind == SRT_PTR)
616915dd	747	{
28bf4b0b	748	(void) sortSet_insert (ret, sn->baseSort);
616915dd	749	}
	750	} end_sortSet_elements;
	751	}
	752	}
	753	}
	754	break;
	755	case OPF_ANYOP:
	756	break;
	757	case OPF_MANYOPM:
	758	{
	759	cstring s = ltoken_getRawString (opf->content.anyop);
	760
	761	if (isCompareOperator (s))
	762	{
	763	if (sortSetList_size (argSorts) == 2)
	764	{
	765	sortSet argSet2;
	766
	767	sortSetList_reset (argSorts);
	768
	769	argSet = sortSetList_current (argSorts);
	770	sortSetList_advance (argSorts);
	771	argSet2 = sortSetList_current (argSorts);
	772
	773	if (sortSet_size (argSet) == 1)
	774	{
	775	sortSet_elements (argSet, cl)
	776	{
	777	sortSet_elements (argSet2, cl2)
	778	{
28bf4b0b	779	if (sort_equal (cl, cl2))
616915dd	780	{
2a6e9c30	781	(void) sortSet_insert (ret, g_sortBool);
616915dd	782	}
	783	} end_sortSet_elements;
	784	} end_sortSet_elements;
	785	}
	786	}
	787	}
	788	}
	789	break;
	790	case OPF_MIDDLE:
	791	break;
	792	case OPF_MMIDDLE:
	793	break;
	794	case OPF_MIDDLEM:
	795	break;
	796	case OPF_MMIDDLEM:
	797	break;
	798	case OPF_BMIDDLE:
	799	break;
	800	case OPF_BMMIDDLE:
	801	break;
	802	case OPF_BMIDDLEM:
	803	break;
	804	case OPF_BMMIDDLEM:
	805	break;
	806	case OPF_SELECT:
	807	break;
	808	case OPF_MAP:
	809	break;
	810	case OPF_MSELECT:
	811	break;
	812	case OPF_MMAP:
	813	break;
	814	default:
	815	break;
	816	}
	817	/@=loopswitchbreak@/
	818	}
	819	return ret;
	820	}