[splint.git] / src / mtDeclarationNode.c

/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2002 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: splint@cs.virginia.edu
** To report a bug: splint-bug@cs.virginia.edu
** For more information: http://www.splint.org
*/
/*
** mtDeclarationNode.c
*/

# include "splintMacros.nf"
# include "basic.h"

extern mtDeclarationNode mtDeclarationNode_create (mttok name, mtDeclarationPieces pieces) /*@*/ 
{
  mtDeclarationNode res = (mtDeclarationNode) dmalloc (sizeof (*res));

  res->name = mttok_getText (name);
  res->loc = mttok_stealLoc (name);
  res->pieces = pieces;

  mttok_free (name);
  return res;
}

extern cstring mtDeclarationNode_unparse (mtDeclarationNode node) /*@*/ 
{
  return message ("state %s %q",
		  node->name,
		  mtDeclarationPieces_unparse (node->pieces));
}

extern void mtDeclarationNode_process (mtDeclarationNode node, bool isglobal)
{
  int i;
  int j;

  mtDeclarationPieces pieces;
  mtDeclarationPiece mtp;
  mtContextNode mtcontext;
  stateCombinationTable tsc;
  stateCombinationTable tmerge;
  cstringList mvals;
  metaStateInfo msinfo;
  int nvalues;

  cstring defaultMergeMessage = 
    cstring_makeLiteralTemp ("Incompatible state merge (default behavior)");

  pieces = node->pieces;

  /*
  ** First, we need to find the values piece.
  */

  mtp = mtDeclarationPieces_findPiece (pieces, MTP_VALUES);

  if (mtDeclarationPiece_isUndefined (mtp)) 
    {
      voptgenerror (FLG_SYNTAX,
		    message ("Metastate declaration missing values clause: %s",
			     mtDeclarationNode_getName (node)),
		    mtDeclarationNode_getLoc (node));
      return;
    }
  else 
    {
      mtValuesNode  mtv = mtDeclarationPiece_getValues (mtp);
      mvals = mtValuesNode_getValues (mtv);
    }

  /*@-usedef@*/ /*@i34 splint should figure this out... */
  nvalues = cstringList_size (mvals);
  /*@=usedef@*/

  mtp = mtDeclarationPieces_findPiece (pieces, MTP_CONTEXT);

  if (mtDeclarationPiece_isUndefined (mtp)) 
    {
      ; /* No context, assume anywhere is okay. */
      mtcontext = mtContextNode_createAny ();
    }
  else 
    {
      mtcontext = mtDeclarationPiece_stealContext (mtp);
    }

  if (isglobal)
    {
      /*
      ** For global state, instead of a transfers piece, we have constraints.
      */

      mtp = mtDeclarationPieces_findPiece (pieces, MTP_TRANSFERS);

      if (!mtDeclarationPiece_isUndefined (mtp)) 
	{
	  voptgenerror (FLG_SYNTAX,
			message ("Global state declaration uses transfers clause.  Should use preconditions and postconsitions clauses instead: %s",
				 mtDeclarationNode_getName (node)),
			mtDeclarationNode_getLoc (node));
	  mtContextNode_free (mtcontext);
	  return;
	} 

      mtp = mtDeclarationPieces_findPiece (pieces, MTP_PRECONDITIONS);
      
      if (mtDeclarationPiece_isUndefined (mtp)) 
	{
	  voptgenerror (FLG_SYNTAX,
			message ("Metastate declaration missing preconditions clause: %s",
				 mtDeclarationNode_getName (node)),
			mtDeclarationNode_getLoc (node));
	  mtContextNode_free (mtcontext);
	  return;
	} 
      else 
	{
	  mtTransferClauseList mtransfers = mtDeclarationPiece_getPreconditions (mtp);
	  tsc = stateCombinationTable_create (nvalues);
	  
	  mtTransferClauseList_elements (mtransfers, transfer)
	    {
	      cstring tfrom = mtTransferClause_getFrom (transfer);
	      cstring tto = mtTransferClause_getTo (transfer);
	      mtTransferAction taction = mtTransferClause_getAction (transfer);
	      cstring vname = mtTransferAction_getValue (taction);
	      
	      int fromindex;
	      int toindex;
	      int vindex;
	      
	      DPRINTF (("Transfer: %s", mtTransferClause_unparse (transfer)));
	      
	      if (cstringList_contains (mvals, tfrom)) 
		{
		  fromindex = cstringList_getIndex (mvals, tfrom);
		}
	      else
		{
		  voptgenerror
		    (FLG_SYNTAX,
		     message ("Precondition clause uses unrecognized caller value %s: %q",
			      tfrom, mtTransferClause_unparse (transfer)),
		     mtTransferClause_getLoc (transfer));
		  continue;
		}
	      
	      if (cstringList_contains (mvals, tto)) 
		{
		  toindex = cstringList_getIndex (mvals, tto);
		}
	      else
		{
		  voptgenerror
		    (FLG_SYNTAX,
		     message ("Precondition clause uses unrecognized constraint value %s: %q",
			      tto, mtTransferClause_unparse (transfer)),
		     mtTransferClause_getLoc (transfer));
		  continue;
		}
	      
	      if (mtTransferAction_isError (taction))
		{
		  vindex = metaState_error;
		}
	      else 
		{
		  if (cstringList_contains (mvals, vname)) 
		    {
		      vindex = cstringList_getIndex (mvals, vname);
		    }
		  else
		    {
		      voptgenerror
			(FLG_SYNTAX,
			 message ("Precondition clause uses unrecognized result state %s: %q",
				  vname, mtTransferClause_unparse (transfer)),
			 mtTransferClause_getLoc (transfer));
		      continue;
		    }
		}
	      
	      if (mtTransferAction_isError (taction))
		{
		  stateCombinationTable_set 
		    (tsc, fromindex, toindex,
		     vindex,
		     cstring_copy (mtTransferAction_getMessage (taction)));
		}
	      else
		{
		  stateCombinationTable_set (tsc, fromindex, toindex,
					     vindex,
					     cstring_undefined);
		}
	    } end_mtTransferClauseList_elements ;
	}
    }
  else
    {
      mtp = mtDeclarationPieces_findPiece (pieces, MTP_PRECONDITIONS);

      if (!mtDeclarationPiece_isUndefined (mtp)) 
	{
	  voptgenerror 
	    (FLG_SYNTAX,
	     message ("Non-global state declaration uses preconditions clause. "
		      "Should use transfers clause instead: %s",
		      mtDeclarationNode_getName (node)),
	     mtDeclarationNode_getLoc (node));
	  mtContextNode_free (mtcontext);
	  return;
	} 

      mtp = mtDeclarationPieces_findPiece (pieces, MTP_POSTCONDITIONS);

      if (!mtDeclarationPiece_isUndefined (mtp)) 
	{
	  voptgenerror 
	    (FLG_SYNTAX,
	     message ("Non-global state declaration uses postconditions clause. "
		      "Should use transfers clause instead: %s",
		      mtDeclarationNode_getName (node)),
	     mtDeclarationNode_getLoc (node));
	  mtContextNode_free (mtcontext);
	  return;
	} 

      mtp = mtDeclarationPieces_findPiece (pieces, MTP_TRANSFERS);
      
      if (mtDeclarationPiece_isUndefined (mtp)) 
	{
	  voptgenerror (FLG_SYNTAX,
			message ("Metastate declaration missing transfers clause: %s",
				 mtDeclarationNode_getName (node)),
			mtDeclarationNode_getLoc (node));
	  mtContextNode_free (mtcontext);
	  return;
	} 
      else 
	{
	  mtTransferClauseList mtransfers = mtDeclarationPiece_getTransfers (mtp);
	  tsc = stateCombinationTable_create (nvalues);
	  
	  mtTransferClauseList_elements (mtransfers, transfer)
	    {
	      cstring tfrom = mtTransferClause_getFrom (transfer);
	      cstring tto = mtTransferClause_getTo (transfer);
	      mtTransferAction taction = mtTransferClause_getAction (transfer);
	      cstring vname = mtTransferAction_getValue (taction);
	      
	      int fromindex;
	      int toindex;
	      int vindex;
	      
	      DPRINTF (("Transfer: %s", mtTransferClause_unparse (transfer)));
	      
	      if (cstringList_contains (mvals, tfrom)) 
		{
		  fromindex = cstringList_getIndex (mvals, tfrom);
		}
	      else
		{
		  voptgenerror
		    (FLG_SYNTAX,
		     message ("Transfer clause uses unrecognized from value %s: %q",
			      tfrom, mtTransferClause_unparse (transfer)),
		     mtTransferClause_getLoc (transfer));
		  continue;
		}
	      
	      if (cstringList_contains (mvals, tto)) 
		{
		  toindex = cstringList_getIndex (mvals, tto);
		}
	      else
		{
		  voptgenerror
		    (FLG_SYNTAX,
		     message ("Transfer clause uses unrecognized to value %s: %q",
			      tto, mtTransferClause_unparse (transfer)),
		     mtTransferClause_getLoc (transfer));
		  continue;
		}
	      
	      if (mtTransferAction_isError (taction))
		{
		  vindex = metaState_error;
		}
	      else 
		{
		  if (cstringList_contains (mvals, vname)) 
		    {
		      vindex = cstringList_getIndex (mvals, vname);
		    }
		  else
		    {
		      voptgenerror
			(FLG_SYNTAX,
			 message ("Transfer clause uses unrecognized result state %s: %q",
				  vname, mtTransferClause_unparse (transfer)),
			 mtTransferClause_getLoc (transfer));
		      continue;
		    }
		}
	      
	      if (mtTransferAction_isError (taction))
		{
		  stateCombinationTable_set 
		    (tsc, fromindex, toindex,
		     vindex,
		     cstring_copy (mtTransferAction_getMessage (taction)));
		}
	      else
		{
		  stateCombinationTable_set (tsc, fromindex, toindex,
					     vindex,
					     cstring_undefined);
		}
	    } end_mtTransferClauseList_elements ;
	}
    }

  mtp = mtDeclarationPieces_findPiece (pieces, MTP_LOSERS);

  if (mtDeclarationPiece_isDefined (mtp))
    {
      mtLoseReferenceList mlosers = mtDeclarationPiece_getLosers (mtp);
      
      mtLoseReferenceList_elements (mlosers, loseref)
	{
	  cstring tfrom = mtLoseReference_getFrom (loseref);
	  mtTransferAction taction = mtLoseReference_getAction (loseref);
	  int fromindex;
	  /* Losing reference is represented by transfer to nvalues */
	  int toindex = nvalues; 
	  int vindex = metaState_error;

	  llassert (mtTransferAction_isError (taction));

	  if (cstringList_contains (mvals, tfrom)) 
	    {
	      fromindex = cstringList_getIndex (mvals, tfrom);
	    }
	  else
	    {
	      voptgenerror
		(FLG_SYNTAX,
		 message ("Lose reference uses unrecognized from value %s: %q",
			  tfrom, mtLoseReference_unparse (loseref)),
		 mtLoseReference_getLoc (loseref));
	      continue;
	    }

	  /*@-usedef@*/
	  stateCombinationTable_set 
	    (tsc, fromindex, toindex, vindex,
	     cstring_copy (mtTransferAction_getMessage (taction)));
	  /*@=usedef@*/
	} end_mtLoseReferenceList_elements ;
    }
  
  /*@-usedef@*/
  DPRINTF (("metastate: %s", metaStateInfo_unparse (msinfo)));
  /*@=usedef@*/

  tmerge = stateCombinationTable_create (nvalues);

  /* Default merge is to make all incompatible mergers errors. */
  
  for (i = 0; i < nvalues; i++) 
    {
      for (j = 0; j < nvalues; j++)
	{
	  if (i != j) 
	    {
	      stateCombinationTable_set 
		(tmerge, i, j, metaState_error, cstring_copy (defaultMergeMessage));
	    }
	}
    }

  mtp = mtDeclarationPieces_findPiece (pieces, MTP_MERGE);
  
  if (mtDeclarationPiece_isDefined (mtp))
    {
      mtMergeNode mtmerge = mtDeclarationPiece_getMerge (mtp);
      mtMergeClauseList mclauses = mtMergeNode_getClauses (mtmerge);

      DPRINTF (("Merge node: %s", mtMergeNode_unparse (mtmerge)));

      mtMergeClauseList_elements (mclauses, merge)
	{
	  mtMergeItem item1 = mtMergeClause_getItem1 (merge);
	  mtMergeItem item2 = mtMergeClause_getItem2 (merge);
	  mtTransferAction taction = mtMergeClause_getAction (merge);
	  int low1index, high1index;
	  int low2index, high2index;
	  int vindex;

	  DPRINTF (("Merge %s X %s => %s",
		    mtMergeItem_unparse (item1),
		    mtMergeItem_unparse (item2),
		    mtTransferAction_unparse (taction)));
	  
	  if (!mtMergeItem_isStar (item1))
	    {
	      if (cstringList_contains (mvals, mtMergeItem_getValue (item1)))
		{
		  low1index = cstringList_getIndex (mvals, mtMergeItem_getValue (item1));
		  high1index = low1index;
		}
	      else
		{
		  voptgenerror
		    (FLG_SYNTAX,
		     message ("Merge clause uses unrecognized first value %s: %q",
			      mtMergeItem_getValue (item1), 
			      mtMergeClause_unparse (merge)),
		     mtMergeClause_getLoc (merge));
		  continue;
		}
	    }
	  else
	    {
	      low1index = 0;
	      high1index = nvalues - 1;
	    }

	  if (!mtMergeItem_isStar (item2))
	    {
	      if (cstringList_contains (mvals, mtMergeItem_getValue (item2))) 
		{
		  low2index = cstringList_getIndex (mvals, mtMergeItem_getValue (item2));
		  high2index = low2index;
		}
	      else
		{
		  voptgenerror
		    (FLG_SYNTAX,
		     message ("Merge clause uses unrecognized second value %s: %q",
			      mtMergeItem_getValue (item2), 
			      mtMergeClause_unparse (merge)),
		     mtMergeItem_getLoc (item2));
		  continue;
		}
	    }
	  else
	    {
	      low2index = 0;
	      high2index = nvalues - 1;
	    }
	  
	  if (mtTransferAction_isError (taction))
	    {
	      vindex = metaState_error;
	    }
	  else 
	    {
	      cstring vname = mtTransferAction_getValue (taction);

	      if (cstringList_contains (mvals, vname)) 
		{
		  vindex = cstringList_getIndex (mvals, vname);
		}
	      else
		{
		  voptgenerror
		    (FLG_SYNTAX,
		     message ("Merge clause uses unrecognized result state %s: %q",
			      vname, mtMergeClause_unparse (merge)),
		     mtTransferAction_getLoc (taction));
		  continue;
		}
	    }

	  for (i = low1index; i <= high1index; i++)
	    {
	      for (j = low2index; j <= high2index; j++)
		{
		  /*@i32 check for multiple definitions! */
		  
		  if (mtTransferAction_isError (taction))
		    {
		      stateCombinationTable_update
			(tmerge, 
			 i, j, 
			 vindex,
			 cstring_copy (mtTransferAction_getMessage (taction)));
		    }
		  else
		    {
		      stateCombinationTable_update
			(tmerge, 
			 i, j, 
			 vindex,
			 cstring_undefined);
		    }
		}
	    }

	  /*
	  ** Unless otherwise indicated, merging is symmetric:
	  */

	  for (i = low1index; i <= high1index; i++)
	    {
	      for (j = low2index; j <= high2index; j++)
		{
		  cstring msg;

		  if (stateCombinationTable_lookup (tmerge, j, i, &msg) == metaState_error)
		    {
		      if (cstring_equal (msg, defaultMergeMessage))
			{
			  /* Override the default action */
			  if (mtTransferAction_isError (taction))
			    {
			      stateCombinationTable_update
				(tmerge, 
				 j, i,
				 vindex,
				 cstring_copy (mtTransferAction_getMessage (taction)));
			    }
			  else
			    {
			      stateCombinationTable_update
				(tmerge, 
				 j, i, 
				 vindex,
				 cstring_undefined);
			    }
			}
		    }
		}
	    }
	} end_mtMergeClauseList_elements ;  
    }

  msinfo = metaStateInfo_create (cstring_copy (mtDeclarationNode_getName (node)),
				 cstringList_copy (mvals),
				 mtcontext,
				 /*@-usedef@*/ tsc, /*@=usedef@*/
				 tmerge,
				 fileloc_copy (mtDeclarationNode_getLoc (node)));

  mtp = mtDeclarationPieces_findPiece (pieces, MTP_ANNOTATIONS);

  if (mtDeclarationPiece_isDefined (mtp))
    {
      mtAnnotationsNode mtannots = mtDeclarationPiece_getAnnotations (mtp);
      mtAnnotationList mtalist = mtAnnotationsNode_getAnnotations (mtannots);

      DPRINTF (("Has annotations: %s", mtAnnotationList_unparse (mtalist)));      

      mtAnnotationList_elements (mtalist, annot) 
	{
	  cstring aname = mtAnnotationDecl_getName (annot);
	  cstring avalue = mtAnnotationDecl_getValue (annot);

	  DPRINTF (("Process annotation: %s", mtAnnotationDecl_unparse (annot)));
	  
	  if (cstringList_contains (mvals, avalue)) 
	    {
	      int vindex = cstringList_getIndex (mvals, avalue);
	      mtContextNode acontext = mtAnnotationDecl_stealContext (annot);
	      
	      context_addAnnotation 
		(annotationInfo_create (cstring_copy (aname), msinfo, 
					acontext, vindex,
					fileloc_copy (mtAnnotationDecl_getLoc (annot))));
	    }
	  else
	    {
	      voptgenerror
		(FLG_SYNTAX,
		 message ("Annotation declaration uses unrecognized value name %s: %q",
			  avalue, mtAnnotationDecl_unparse (annot)),
		 mtAnnotationDecl_getLoc (annot));
	    }

	} end_mtAnnotationList_elements ;
    }

  mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTS);

  if (mtDeclarationPiece_isDefined (mtp))
    {
      mtDefaultsNode mdn = mtDeclarationPiece_getDefaults (mtp);
      mtDefaultsDeclList mdecls = mtDefaultsNode_getDecls (mdn);
      
      llassert (!isglobal);

      mtDefaultsDeclList_elements (mdecls, mdecl)
	{
	  mtContextNode mcontext = mtDefaultsDecl_getContext (mdecl);
	  cstring mvalue = mtDefaultsDecl_getValue (mdecl);

	  if (cstringList_contains (mvals, mvalue)) 
	    {
	      int vindex = cstringList_getIndex (mvals, mvalue);
	      mtContextKind mkind;

	      if (mtContextNode_isReference (mcontext))
		{
		  mkind = MTC_REFERENCE;
		}
	      else if (mtContextNode_isParameter (mcontext))
		{
		  mkind = MTC_PARAM;
		}
	      else if (mtContextNode_isResult (mcontext))
		{
		  mkind = MTC_RESULT;
		}
	      else if (mtContextNode_isLiteral (mcontext))
		{
		  mkind = MTC_LITERAL;
		}
	      else if (mtContextNode_isNull (mcontext))
		{
		  mkind = MTC_NULL;
		}
	      else
		{
		  DPRINTF (("Bad: %s", mtContextNode_unparse (mcontext)));
		  BADBRANCH;
		}

	      if (metaStateInfo_getDefaultValueContext (msinfo, mkind) != stateValue_error)
		{
		  voptgenerror
		    (FLG_SYNTAX,
		     message ("Duplicate defaults declaration for context %q: %q",
			      mtContextNode_unparse (mcontext), 
			      mtDefaultsDecl_unparse (mdecl)),
		     mtDefaultsDecl_getLoc (mdecl));
		}
	      else
		{
		  metaStateInfo_setDefaultValueContext (msinfo, mkind, vindex);
		}
	    }
	  else
	    {
	      voptgenerror
		(FLG_SYNTAX,
		 message ("Defaults declaration uses unrecognized value name %s: %q",
			  mvalue, mtDefaultsDecl_unparse (mdecl)),
		 mtDefaultsDecl_getLoc (mdecl));
	    }
	} end_mtDefaultsDeclList_elements ;
    }

  mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTVALUE);

  if (mtDeclarationPiece_isDefined (mtp))
    {
      cstring mvalue = mtDeclarationPiece_getDefaultValue (mtp);
      llassert (isglobal);
      
      if (cstringList_contains (mvals, mvalue)) 
	{
	  int vindex = cstringList_getIndex (mvals, mvalue);
	  
	  if (metaStateInfo_getDefaultRefValue (msinfo) != stateValue_error)
	    {
	      voptgenerror
		(FLG_SYNTAX,
		 message ("Duplicate default value declaration for global state: %s",
			  mvalue),
		 mtDeclarationNode_getLoc (node));
	    }
	  else
	    {
	      metaStateInfo_setDefaultRefValue (msinfo, vindex);
	    }
	}
      else
	{
	  voptgenerror
	    (FLG_SYNTAX,
	     message ("Default value declaration uses unrecognized value name: %s",
		      mvalue),
	     mtDeclarationNode_getLoc (node));
	}
    }
  
  context_addMetaState (cstring_copy (mtDeclarationNode_getName (node)),
			msinfo);
}

extern void mtDeclarationNode_free (/*@only@*/ mtDeclarationNode node)
{
  mtDeclarationPieces_free (node->pieces);
  cstring_free (node->name);
  fileloc_free (node->loc);
  sfree (node);
}

extern fileloc mtDeclarationNode_getLoc (mtDeclarationNode node) 
{
  return node->loc;
}

extern /*@observer@*/ cstring mtDeclarationNode_getName (mtDeclarationNode node)
{
  return node->name;
}
Commit	Line	Data
28bf4b0b	1	/*
11db3170	2	** Splint - annotation-assisted static program checker
77d37419	3	** Copyright (C) 1994-2002 University of Virginia,
28bf4b0b	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	**
1b8ae690	20	** For information on splint: splint@cs.virginia.edu
1b8ae690	21	** To report a bug: splint-bug@cs.virginia.edu
11db3170	22	** For more information: http://www.splint.org
28bf4b0b	23	*/
	24	/*
	25	** mtDeclarationNode.c
	26	*/
	27
1b8ae690	28	# include "splintMacros.nf"
28bf4b0b	29	# include "basic.h"
28bf4b0b	30
	31	extern mtDeclarationNode mtDeclarationNode_create (mttok name, mtDeclarationPieces pieces) /@/
	32	{
	33	mtDeclarationNode res = (mtDeclarationNode) dmalloc (sizeof (*res));
	34
	35	res->name = mttok_getText (name);
	36	res->loc = mttok_stealLoc (name);
	37	res->pieces = pieces;
	38
	39	mttok_free (name);
	40	return res;
	41	}
	42
	43	extern cstring mtDeclarationNode_unparse (mtDeclarationNode node) /@/
	44	{
	45	return message ("state %s %q",
	46	node->name,
	47	mtDeclarationPieces_unparse (node->pieces));
	48	}
	49
	50	extern void mtDeclarationNode_process (mtDeclarationNode node, bool isglobal)
	51	{
	52	int i;
	53	int j;
	54
	55	mtDeclarationPieces pieces;
	56	mtDeclarationPiece mtp;
	57	mtContextNode mtcontext;
	58	stateCombinationTable tsc;
	59	stateCombinationTable tmerge;
	60	cstringList mvals;
	61	metaStateInfo msinfo;
	62	int nvalues;
	63
12f2ffe9	64	cstring defaultMergeMessage =
	65	cstring_makeLiteralTemp ("Incompatible state merge (default behavior)");
	66
28bf4b0b	67	pieces = node->pieces;
	68
	69	/*
	70	** First, we need to find the values piece.
	71	*/
	72
	73	mtp = mtDeclarationPieces_findPiece (pieces, MTP_VALUES);
	74
	75	if (mtDeclarationPiece_isUndefined (mtp))
	76	{
	77	voptgenerror (FLG_SYNTAX,
	78	message ("Metastate declaration missing values clause: %s",
	79	mtDeclarationNode_getName (node)),
	80	mtDeclarationNode_getLoc (node));
	81	return;
	82	}
	83	else
	84	{
	85	mtValuesNode mtv = mtDeclarationPiece_getValues (mtp);
	86	mvals = mtValuesNode_getValues (mtv);
	87	}
	88
1b8ae690	89	/@-usedef@/ /@i34 splint should figure this out... /
28bf4b0b	90	nvalues = cstringList_size (mvals);
	91	/@=usedef@/
	92
	93	mtp = mtDeclarationPieces_findPiece (pieces, MTP_CONTEXT);
	94
	95	if (mtDeclarationPiece_isUndefined (mtp))
	96	{
	97	; /* No context, assume anywhere is okay. */
	98	mtcontext = mtContextNode_createAny ();
	99	}
	100	else
	101	{
	102	mtcontext = mtDeclarationPiece_stealContext (mtp);
	103	}
	104
	105	if (isglobal)
	106	{
	107	/*
	108	** For global state, instead of a transfers piece, we have constraints.
	109	*/
	110
	111	mtp = mtDeclarationPieces_findPiece (pieces, MTP_TRANSFERS);
	112
	113	if (!mtDeclarationPiece_isUndefined (mtp))
	114	{
	115	voptgenerror (FLG_SYNTAX,
	116	message ("Global state declaration uses transfers clause. Should use preconditions and postconsitions clauses instead: %s",
	117	mtDeclarationNode_getName (node)),
	118	mtDeclarationNode_getLoc (node));
	119	mtContextNode_free (mtcontext);
	120	return;
	121	}
	122
	123	mtp = mtDeclarationPieces_findPiece (pieces, MTP_PRECONDITIONS);
	124
	125	if (mtDeclarationPiece_isUndefined (mtp))
	126	{
	127	voptgenerror (FLG_SYNTAX,
	128	message ("Metastate declaration missing preconditions clause: %s",
	129	mtDeclarationNode_getName (node)),
	130	mtDeclarationNode_getLoc (node));
	131	mtContextNode_free (mtcontext);
	132	return;
	133	}
	134	else
	135	{
	136	mtTransferClauseList mtransfers = mtDeclarationPiece_getPreconditions (mtp);
	137	tsc = stateCombinationTable_create (nvalues);
	138
	139	mtTransferClauseList_elements (mtransfers, transfer)
	140	{
	141	cstring tfrom = mtTransferClause_getFrom (transfer);
	142	cstring tto = mtTransferClause_getTo (transfer);
	143	mtTransferAction taction = mtTransferClause_getAction (transfer);
	144	cstring vname = mtTransferAction_getValue (taction);
	145
	146	int fromindex;
	147	int toindex;
	148	int vindex;
	149
	150	DPRINTF (("Transfer: %s", mtTransferClause_unparse (transfer)));
	151
	152	if (cstringList_contains (mvals, tfrom))
	153	{
154	fromindex = cstringList_getIndex (mvals, tfrom);
155	}
156	else
157	{
158	voptgenerror
159	(FLG_SYNTAX,
160	message ("Precondition clause uses unrecognized caller value %s: %q",
161	tfrom, mtTransferClause_unparse (transfer)),
162	mtTransferClause_getLoc (transfer));
163	continue;
164	}
165
166	if (cstringList_contains (mvals, tto))
167	{
168	toindex = cstringList_getIndex (mvals, tto);
169	}
170	else
171	{
172	voptgenerror
173	(FLG_SYNTAX,
174	message ("Precondition clause uses unrecognized constraint value %s: %q",
175	tto, mtTransferClause_unparse (transfer)),
176	mtTransferClause_getLoc (transfer));
177	continue;
178	}
179
180	if (mtTransferAction_isError (taction))
181	{
182	vindex = metaState_error;
183	}
184	else
185	{
186	if (cstringList_contains (mvals, vname))
187	{
188	vindex = cstringList_getIndex (mvals, vname);
189	}
190	else
191	{
192	voptgenerror
193	(FLG_SYNTAX,
194	message ("Precondition clause uses unrecognized result state %s: %q",
195	vname, mtTransferClause_unparse (transfer)),
196	mtTransferClause_getLoc (transfer));
197	continue;
198	}
199	}
200
201	if (mtTransferAction_isError (taction))
202	{
203	stateCombinationTable_set
204	(tsc, fromindex, toindex,
205	vindex,
206	cstring_copy (mtTransferAction_getMessage (taction)));
207	}
208	else
209	{
210	stateCombinationTable_set (tsc, fromindex, toindex,
211	vindex,
212	cstring_undefined);
213	}
214	} end_mtTransferClauseList_elements ;
215	}
216	}
217	else
218	{
219	mtp = mtDeclarationPieces_findPiece (pieces, MTP_PRECONDITIONS);
220
221	if (!mtDeclarationPiece_isUndefined (mtp))
222	{
223	voptgenerror
224	(FLG_SYNTAX,
225	message ("Non-global state declaration uses preconditions clause. "
226	"Should use transfers clause instead: %s",
227	mtDeclarationNode_getName (node)),
228	mtDeclarationNode_getLoc (node));
229	mtContextNode_free (mtcontext);
230	return;
231	}
232
233	mtp = mtDeclarationPieces_findPiece (pieces, MTP_POSTCONDITIONS);
234
235	if (!mtDeclarationPiece_isUndefined (mtp))
236	{
237	voptgenerror
238	(FLG_SYNTAX,
239	message ("Non-global state declaration uses postconditions clause. "
240	"Should use transfers clause instead: %s",
241	mtDeclarationNode_getName (node)),
242	mtDeclarationNode_getLoc (node));
243	mtContextNode_free (mtcontext);
244	return;
245	}
246
247	mtp = mtDeclarationPieces_findPiece (pieces, MTP_TRANSFERS);
248
249	if (mtDeclarationPiece_isUndefined (mtp))
250	{
251	voptgenerror (FLG_SYNTAX,
252	message ("Metastate declaration missing transfers clause: %s",
253	mtDeclarationNode_getName (node)),
254	mtDeclarationNode_getLoc (node));
255	mtContextNode_free (mtcontext);
256	return;
257	}
258	else
259	{
260	mtTransferClauseList mtransfers = mtDeclarationPiece_getTransfers (mtp);
261	tsc = stateCombinationTable_create (nvalues);
262
263	mtTransferClauseList_elements (mtransfers, transfer)
264	{
265	cstring tfrom = mtTransferClause_getFrom (transfer);
266	cstring tto = mtTransferClause_getTo (transfer);
267	mtTransferAction taction = mtTransferClause_getAction (transfer);
268	cstring vname = mtTransferAction_getValue (taction);
269
270	int fromindex;
271	int toindex;
272	int vindex;
273
274	DPRINTF (("Transfer: %s", mtTransferClause_unparse (transfer)));
275
276	if (cstringList_contains (mvals, tfrom))
277	{
278	fromindex = cstringList_getIndex (mvals, tfrom);
279	}
280	else
281	{
282	voptgenerror
283	(FLG_SYNTAX,
284	message ("Transfer clause uses unrecognized from value %s: %q",
285	tfrom, mtTransferClause_unparse (transfer)),
286	mtTransferClause_getLoc (transfer));
287	continue;
288	}
289
290	if (cstringList_contains (mvals, tto))
291	{
292	toindex = cstringList_getIndex (mvals, tto);
293	}
294	else
295	{
296	voptgenerror
297	(FLG_SYNTAX,
298	message ("Transfer clause uses unrecognized to value %s: %q",
299	tto, mtTransferClause_unparse (transfer)),
300	mtTransferClause_getLoc (transfer));
301	continue;
302	}
303
304	if (mtTransferAction_isError (taction))
305	{
306	vindex = metaState_error;
307	}
308	else
309	{
310	if (cstringList_contains (mvals, vname))
311	{
312	vindex = cstringList_getIndex (mvals, vname);
313	}
314	else
315	{
316	voptgenerror
317	(FLG_SYNTAX,
318	message ("Transfer clause uses unrecognized result state %s: %q",
319	vname, mtTransferClause_unparse (transfer)),
320	mtTransferClause_getLoc (transfer));
321	continue;
322	}
323	}
324
325	if (mtTransferAction_isError (taction))
326	{
327	stateCombinationTable_set
328	(tsc, fromindex, toindex,
329	vindex,
330	cstring_copy (mtTransferAction_getMessage (taction)));
331	}
332	else
333	{
334	stateCombinationTable_set (tsc, fromindex, toindex,
335	vindex,
336	cstring_undefined);
337	}
338	} end_mtTransferClauseList_elements ;
339	}
340	}
341
342	mtp = mtDeclarationPieces_findPiece (pieces, MTP_LOSERS);
343
344	if (mtDeclarationPiece_isDefined (mtp))
345	{
346	mtLoseReferenceList mlosers = mtDeclarationPiece_getLosers (mtp);
347
348	mtLoseReferenceList_elements (mlosers, loseref)
349	{
350	cstring tfrom = mtLoseReference_getFrom (loseref);
351	mtTransferAction taction = mtLoseReference_getAction (loseref);
352	int fromindex;
353	/* Losing reference is represented by transfer to nvalues */
354	int toindex = nvalues;
355	int vindex = metaState_error;
356
357	llassert (mtTransferAction_isError (taction));
358
359	if (cstringList_contains (mvals, tfrom))
360	{
361	fromindex = cstringList_getIndex (mvals, tfrom);
362	}
363	else
364	{
365	voptgenerror
366	(FLG_SYNTAX,
367	message ("Lose reference uses unrecognized from value %s: %q",
368	tfrom, mtLoseReference_unparse (loseref)),
369	mtLoseReference_getLoc (loseref));
370	continue;
371	}
372
373	/@-usedef@/
374	stateCombinationTable_set
375	(tsc, fromindex, toindex, vindex,
376	cstring_copy (mtTransferAction_getMessage (taction)));
377	/@=usedef@/
378	} end_mtLoseReferenceList_elements ;
379	}
380
381	/@-usedef@/
382	DPRINTF (("metastate: %s", metaStateInfo_unparse (msinfo)));
383	/@=usedef@/
384
385	tmerge = stateCombinationTable_create (nvalues);
386
387	/* Default merge is to make all incompatible mergers errors. */
388
389	for (i = 0; i < nvalues; i++)
390	{
391	for (j = 0; j < nvalues; j++)
392	{
393	if (i != j)
394	{
395	stateCombinationTable_set
12f2ffe9	396	(tmerge, i, j, metaState_error, cstring_copy (defaultMergeMessage));
28bf4b0b	397	}
	398	}
	399	}
	400
	401	mtp = mtDeclarationPieces_findPiece (pieces, MTP_MERGE);
	402
	403	if (mtDeclarationPiece_isDefined (mtp))
	404	{
	405	mtMergeNode mtmerge = mtDeclarationPiece_getMerge (mtp);
	406	mtMergeClauseList mclauses = mtMergeNode_getClauses (mtmerge);
	407
	408	DPRINTF (("Merge node: %s", mtMergeNode_unparse (mtmerge)));
	409
	410	mtMergeClauseList_elements (mclauses, merge)
	411	{
	412	mtMergeItem item1 = mtMergeClause_getItem1 (merge);
	413	mtMergeItem item2 = mtMergeClause_getItem2 (merge);
	414	mtTransferAction taction = mtMergeClause_getAction (merge);
	415	int low1index, high1index;
	416	int low2index, high2index;
	417	int vindex;
	418
	419	DPRINTF (("Merge %s X %s => %s",
	420	mtMergeItem_unparse (item1),
	421	mtMergeItem_unparse (item2),
	422	mtTransferAction_unparse (taction)));
	423
	424	if (!mtMergeItem_isStar (item1))
	425	{
	426	if (cstringList_contains (mvals, mtMergeItem_getValue (item1)))
	427	{
	428	low1index = cstringList_getIndex (mvals, mtMergeItem_getValue (item1));
	429	high1index = low1index;
	430	}
	431	else
	432	{
	433	voptgenerror
	434	(FLG_SYNTAX,
	435	message ("Merge clause uses unrecognized first value %s: %q",
	436	mtMergeItem_getValue (item1),
	437	mtMergeClause_unparse (merge)),
	438	mtMergeClause_getLoc (merge));
	439	continue;
	440	}
	441	}
	442	else
	443	{
	444	low1index = 0;
	445	high1index = nvalues - 1;
	446	}
	447
	448	if (!mtMergeItem_isStar (item2))
	449	{
	450	if (cstringList_contains (mvals, mtMergeItem_getValue (item2)))
	451	{
	452	low2index = cstringList_getIndex (mvals, mtMergeItem_getValue (item2));
	453	high2index = low2index;
	454	}
	455	else
	456	{
	457	voptgenerror
	458	(FLG_SYNTAX,
	459	message ("Merge clause uses unrecognized second value %s: %q",
	460	mtMergeItem_getValue (item2),
461	mtMergeClause_unparse (merge)),
462	mtMergeItem_getLoc (item2));
463	continue;
464	}
465	}
466	else
467	{
468	low2index = 0;
469	high2index = nvalues - 1;
470	}
471
472	if (mtTransferAction_isError (taction))
473	{
474	vindex = metaState_error;
475	}
476	else
477	{
478	cstring vname = mtTransferAction_getValue (taction);
479
480	if (cstringList_contains (mvals, vname))
481	{
482	vindex = cstringList_getIndex (mvals, vname);
483	}
484	else
485	{
486	voptgenerror
487	(FLG_SYNTAX,
488	message ("Merge clause uses unrecognized result state %s: %q",
489	vname, mtMergeClause_unparse (merge)),
490	mtTransferAction_getLoc (taction));
491	continue;
492	}
493	}
494
495	for (i = low1index; i <= high1index; i++)
496	{
497	for (j = low2index; j <= high2index; j++)
498	{
499	/@i32 check for multiple definitions! /
500
501	if (mtTransferAction_isError (taction))
502	{
503	stateCombinationTable_update
504	(tmerge,
505	i, j,
506	vindex,
507	cstring_copy (mtTransferAction_getMessage (taction)));
508	}
509	else
510	{
511	stateCombinationTable_update
512	(tmerge,
513	i, j,
514	vindex,
515	cstring_undefined);
516	}
517	}
518	}
12f2ffe9	519
	520	/*
	521	** Unless otherwise indicated, merging is symmetric:
	522	*/
	523
	524	for (i = low1index; i <= high1index; i++)
	525	{
	526	for (j = low2index; j <= high2index; j++)
	527	{
	528	cstring msg;
	529
	530	if (stateCombinationTable_lookup (tmerge, j, i, &msg) == metaState_error)
	531	{
	532	if (cstring_equal (msg, defaultMergeMessage))
	533	{
	534	/* Override the default action */
	535	if (mtTransferAction_isError (taction))
	536	{
	537	stateCombinationTable_update
	538	(tmerge,
	539	j, i,
	540	vindex,
	541	cstring_copy (mtTransferAction_getMessage (taction)));
	542	}
	543	else
	544	{
	545	stateCombinationTable_update
	546	(tmerge,
	547	j, i,
	548	vindex,
	549	cstring_undefined);
	550	}
	551	}
	552	}
	553	}
	554	}
28bf4b0b	555	} end_mtMergeClauseList_elements ;
	556	}
	557
	558	msinfo = metaStateInfo_create (cstring_copy (mtDeclarationNode_getName (node)),
	559	cstringList_copy (mvals),
	560	mtcontext,
	561	/@-usedef@/ tsc, /@=usedef@/
	562	tmerge,
	563	fileloc_copy (mtDeclarationNode_getLoc (node)));
	564
	565	mtp = mtDeclarationPieces_findPiece (pieces, MTP_ANNOTATIONS);
	566
	567	if (mtDeclarationPiece_isDefined (mtp))
	568	{
	569	mtAnnotationsNode mtannots = mtDeclarationPiece_getAnnotations (mtp);
	570	mtAnnotationList mtalist = mtAnnotationsNode_getAnnotations (mtannots);
	571
	572	DPRINTF (("Has annotations: %s", mtAnnotationList_unparse (mtalist)));
	573
	574	mtAnnotationList_elements (mtalist, annot)
	575	{
	576	cstring aname = mtAnnotationDecl_getName (annot);
	577	cstring avalue = mtAnnotationDecl_getValue (annot);
	578
	579	DPRINTF (("Process annotation: %s", mtAnnotationDecl_unparse (annot)));
	580
	581	if (cstringList_contains (mvals, avalue))
	582	{
	583	int vindex = cstringList_getIndex (mvals, avalue);
	584	mtContextNode acontext = mtAnnotationDecl_stealContext (annot);
	585
	586	context_addAnnotation
	587	(annotationInfo_create (cstring_copy (aname), msinfo,
	588	acontext, vindex,
	589	fileloc_copy (mtAnnotationDecl_getLoc (annot))));
	590	}
	591	else
	592	{
	593	voptgenerror
	594	(FLG_SYNTAX,
	595	message ("Annotation declaration uses unrecognized value name %s: %q",
	596	avalue, mtAnnotationDecl_unparse (annot)),
	597	mtAnnotationDecl_getLoc (annot));
	598	}
	599
	600	} end_mtAnnotationList_elements ;
	601	}
	602
	603	mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTS);
	604
	605	if (mtDeclarationPiece_isDefined (mtp))
	606	{
	607	mtDefaultsNode mdn = mtDeclarationPiece_getDefaults (mtp);
	608	mtDefaultsDeclList mdecls = mtDefaultsNode_getDecls (mdn);
	609
	610	llassert (!isglobal);
	611
	612	mtDefaultsDeclList_elements (mdecls, mdecl)
	613	{
	614	mtContextNode mcontext = mtDefaultsDecl_getContext (mdecl);
	615	cstring mvalue = mtDefaultsDecl_getValue (mdecl);
	616
	617	if (cstringList_contains (mvals, mvalue))
	618	{
619	int vindex = cstringList_getIndex (mvals, mvalue);
12f2ffe9	620	mtContextKind mkind;
28bf4b0b	621
b072092f	622	if (mtContextNode_isReference (mcontext))
28bf4b0b	623	{
12f2ffe9	624	mkind = MTC_REFERENCE;
28bf4b0b	625	}
	626	else if (mtContextNode_isParameter (mcontext))
	627	{
12f2ffe9	628	mkind = MTC_PARAM;
28bf4b0b	629	}
b072092f	630	else if (mtContextNode_isResult (mcontext))
b072092f	631	{
12f2ffe9	632	mkind = MTC_RESULT;
	633	}
	634	else if (mtContextNode_isLiteral (mcontext))
	635	{
	636	mkind = MTC_LITERAL;
	637	}
	638	else if (mtContextNode_isNull (mcontext))
	639	{
	640	mkind = MTC_NULL;
b072092f	641	}
28bf4b0b	642	else
28bf4b0b	643	{
12f2ffe9	644	DPRINTF (("Bad: %s", mtContextNode_unparse (mcontext)));
28bf4b0b	645	BADBRANCH;
28bf4b0b	646	}
12f2ffe9	647
	648	if (metaStateInfo_getDefaultValueContext (msinfo, mkind) != stateValue_error)
	649	{
	650	voptgenerror
	651	(FLG_SYNTAX,
	652	message ("Duplicate defaults declaration for context %q: %q",
	653	mtContextNode_unparse (mcontext),
	654	mtDefaultsDecl_unparse (mdecl)),
	655	mtDefaultsDecl_getLoc (mdecl));
	656	}
	657	else
	658	{
	659	metaStateInfo_setDefaultValueContext (msinfo, mkind, vindex);
	660	}
28bf4b0b	661	}
	662	else
	663	{
	664	voptgenerror
	665	(FLG_SYNTAX,
	666	message ("Defaults declaration uses unrecognized value name %s: %q",
	667	mvalue, mtDefaultsDecl_unparse (mdecl)),
	668	mtDefaultsDecl_getLoc (mdecl));
	669	}
	670	} end_mtDefaultsDeclList_elements ;
	671	}
	672
	673	mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTVALUE);
	674
	675	if (mtDeclarationPiece_isDefined (mtp))
	676	{
	677	cstring mvalue = mtDeclarationPiece_getDefaultValue (mtp);
	678	llassert (isglobal);
	679
	680	if (cstringList_contains (mvals, mvalue))
	681	{
	682	int vindex = cstringList_getIndex (mvals, mvalue);
	683
	684	if (metaStateInfo_getDefaultRefValue (msinfo) != stateValue_error)
	685	{
	686	voptgenerror
	687	(FLG_SYNTAX,
	688	message ("Duplicate default value declaration for global state: %s",
	689	mvalue),
	690	mtDeclarationNode_getLoc (node));
	691	}
	692	else
	693	{
	694	metaStateInfo_setDefaultRefValue (msinfo, vindex);
	695	}
	696	}
	697	else
	698	{
	699	voptgenerror
	700	(FLG_SYNTAX,
	701	message ("Default value declaration uses unrecognized value name: %s",
	702	mvalue),
	703	mtDeclarationNode_getLoc (node));
	704	}
	705	}
	706
	707	context_addMetaState (cstring_copy (mtDeclarationNode_getName (node)),
	708	msinfo);
	709	}
	710
	711	extern void mtDeclarationNode_free (/@only@/ mtDeclarationNode node)
	712	{
	713	mtDeclarationPieces_free (node->pieces);
	714	cstring_free (node->name);
	715	fileloc_free (node->loc);
	716	sfree (node);
	717	}
	718
	719	extern fileloc mtDeclarationNode_getLoc (mtDeclarationNode node)
	720	{
	721	return node->loc;
	722	}
	723
	724	extern /@observer@/ cstring mtDeclarationNode_getName (mtDeclarationNode node)
725	{
726	return node->name;
727	}