[splint.git] / src / mtDeclarationNode.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
*/
/*
** 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@*/ /* 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 ;
    }
  
  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++)
		{
		  /* Need to add checks 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
c59f5181	3	** Copyright (C) 1994-2003 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	**
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
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
b73d1009	89	/@-usedef@/ /* 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
28bf4b0b	381	tmerge = stateCombinationTable_create (nvalues);
	382
	383	/* Default merge is to make all incompatible mergers errors. */
	384
	385	for (i = 0; i < nvalues; i++)
	386	{
	387	for (j = 0; j < nvalues; j++)
	388	{
	389	if (i != j)
	390	{
	391	stateCombinationTable_set
12f2ffe9	392	(tmerge, i, j, metaState_error, cstring_copy (defaultMergeMessage));
28bf4b0b	393	}
	394	}
	395	}
	396
	397	mtp = mtDeclarationPieces_findPiece (pieces, MTP_MERGE);
	398
	399	if (mtDeclarationPiece_isDefined (mtp))
	400	{
	401	mtMergeNode mtmerge = mtDeclarationPiece_getMerge (mtp);
	402	mtMergeClauseList mclauses = mtMergeNode_getClauses (mtmerge);
	403
	404	DPRINTF (("Merge node: %s", mtMergeNode_unparse (mtmerge)));
	405
	406	mtMergeClauseList_elements (mclauses, merge)
	407	{
	408	mtMergeItem item1 = mtMergeClause_getItem1 (merge);
	409	mtMergeItem item2 = mtMergeClause_getItem2 (merge);
	410	mtTransferAction taction = mtMergeClause_getAction (merge);
	411	int low1index, high1index;
	412	int low2index, high2index;
	413	int vindex;
	414
	415	DPRINTF (("Merge %s X %s => %s",
	416	mtMergeItem_unparse (item1),
	417	mtMergeItem_unparse (item2),
	418	mtTransferAction_unparse (taction)));
	419
	420	if (!mtMergeItem_isStar (item1))
	421	{
	422	if (cstringList_contains (mvals, mtMergeItem_getValue (item1)))
	423	{
	424	low1index = cstringList_getIndex (mvals, mtMergeItem_getValue (item1));
	425	high1index = low1index;
	426	}
	427	else
	428	{
	429	voptgenerror
	430	(FLG_SYNTAX,
	431	message ("Merge clause uses unrecognized first value %s: %q",
	432	mtMergeItem_getValue (item1),
	433	mtMergeClause_unparse (merge)),
	434	mtMergeClause_getLoc (merge));
	435	continue;
	436	}
	437	}
	438	else
	439	{
	440	low1index = 0;
	441	high1index = nvalues - 1;
	442	}
	443
	444	if (!mtMergeItem_isStar (item2))
	445	{
	446	if (cstringList_contains (mvals, mtMergeItem_getValue (item2)))
	447	{
	448	low2index = cstringList_getIndex (mvals, mtMergeItem_getValue (item2));
	449	high2index = low2index;
	450	}
	451	else
	452	{
	453	voptgenerror
	454	(FLG_SYNTAX,
	455	message ("Merge clause uses unrecognized second value %s: %q",
	456	mtMergeItem_getValue (item2),
457	mtMergeClause_unparse (merge)),
458	mtMergeItem_getLoc (item2));
459	continue;
460	}
461	}
462	else
463	{
464	low2index = 0;
465	high2index = nvalues - 1;
466	}
467
468	if (mtTransferAction_isError (taction))
469	{
470	vindex = metaState_error;
471	}
472	else
473	{
474	cstring vname = mtTransferAction_getValue (taction);
475
476	if (cstringList_contains (mvals, vname))
477	{
478	vindex = cstringList_getIndex (mvals, vname);
479	}
480	else
481	{
482	voptgenerror
483	(FLG_SYNTAX,
484	message ("Merge clause uses unrecognized result state %s: %q",
485	vname, mtMergeClause_unparse (merge)),
486	mtTransferAction_getLoc (taction));
487	continue;
488	}
489	}
490
491	for (i = low1index; i <= high1index; i++)
492	{
493	for (j = low2index; j <= high2index; j++)
494	{
b73d1009	495	/* Need to add checks for multiple definitions! */
28bf4b0b	496
	497	if (mtTransferAction_isError (taction))
	498	{
	499	stateCombinationTable_update
	500	(tmerge,
	501	i, j,
	502	vindex,
	503	cstring_copy (mtTransferAction_getMessage (taction)));
	504	}
	505	else
	506	{
	507	stateCombinationTable_update
	508	(tmerge,
	509	i, j,
	510	vindex,
	511	cstring_undefined);
	512	}
	513	}
	514	}
12f2ffe9	515
	516	/*
	517	** Unless otherwise indicated, merging is symmetric:
	518	*/
	519
	520	for (i = low1index; i <= high1index; i++)
	521	{
	522	for (j = low2index; j <= high2index; j++)
	523	{
	524	cstring msg;
	525
	526	if (stateCombinationTable_lookup (tmerge, j, i, &msg) == metaState_error)
	527	{
	528	if (cstring_equal (msg, defaultMergeMessage))
	529	{
	530	/* Override the default action */
	531	if (mtTransferAction_isError (taction))
	532	{
	533	stateCombinationTable_update
	534	(tmerge,
	535	j, i,
	536	vindex,
	537	cstring_copy (mtTransferAction_getMessage (taction)));
	538	}
	539	else
	540	{
	541	stateCombinationTable_update
	542	(tmerge,
	543	j, i,
	544	vindex,
	545	cstring_undefined);
	546	}
	547	}
	548	}
	549	}
	550	}
28bf4b0b	551	} end_mtMergeClauseList_elements ;
	552	}
	553
	554	msinfo = metaStateInfo_create (cstring_copy (mtDeclarationNode_getName (node)),
	555	cstringList_copy (mvals),
	556	mtcontext,
	557	/@-usedef@/ tsc, /@=usedef@/
	558	tmerge,
	559	fileloc_copy (mtDeclarationNode_getLoc (node)));
	560
	561	mtp = mtDeclarationPieces_findPiece (pieces, MTP_ANNOTATIONS);
	562
	563	if (mtDeclarationPiece_isDefined (mtp))
	564	{
	565	mtAnnotationsNode mtannots = mtDeclarationPiece_getAnnotations (mtp);
	566	mtAnnotationList mtalist = mtAnnotationsNode_getAnnotations (mtannots);
	567
	568	DPRINTF (("Has annotations: %s", mtAnnotationList_unparse (mtalist)));
	569
	570	mtAnnotationList_elements (mtalist, annot)
	571	{
	572	cstring aname = mtAnnotationDecl_getName (annot);
	573	cstring avalue = mtAnnotationDecl_getValue (annot);
	574
	575	DPRINTF (("Process annotation: %s", mtAnnotationDecl_unparse (annot)));
	576
	577	if (cstringList_contains (mvals, avalue))
	578	{
	579	int vindex = cstringList_getIndex (mvals, avalue);
	580	mtContextNode acontext = mtAnnotationDecl_stealContext (annot);
	581
	582	context_addAnnotation
	583	(annotationInfo_create (cstring_copy (aname), msinfo,
	584	acontext, vindex,
	585	fileloc_copy (mtAnnotationDecl_getLoc (annot))));
	586	}
	587	else
	588	{
	589	voptgenerror
	590	(FLG_SYNTAX,
	591	message ("Annotation declaration uses unrecognized value name %s: %q",
	592	avalue, mtAnnotationDecl_unparse (annot)),
	593	mtAnnotationDecl_getLoc (annot));
	594	}
	595
	596	} end_mtAnnotationList_elements ;
	597	}
	598
	599	mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTS);
	600
	601	if (mtDeclarationPiece_isDefined (mtp))
	602	{
	603	mtDefaultsNode mdn = mtDeclarationPiece_getDefaults (mtp);
	604	mtDefaultsDeclList mdecls = mtDefaultsNode_getDecls (mdn);
	605
	606	llassert (!isglobal);
	607
	608	mtDefaultsDeclList_elements (mdecls, mdecl)
	609	{
	610	mtContextNode mcontext = mtDefaultsDecl_getContext (mdecl);
	611	cstring mvalue = mtDefaultsDecl_getValue (mdecl);
	612
	613	if (cstringList_contains (mvals, mvalue))
	614	{
615	int vindex = cstringList_getIndex (mvals, mvalue);
12f2ffe9	616	mtContextKind mkind;
28bf4b0b	617
b072092f	618	if (mtContextNode_isReference (mcontext))
28bf4b0b	619	{
12f2ffe9	620	mkind = MTC_REFERENCE;
28bf4b0b	621	}
	622	else if (mtContextNode_isParameter (mcontext))
	623	{
12f2ffe9	624	mkind = MTC_PARAM;
28bf4b0b	625	}
b072092f	626	else if (mtContextNode_isResult (mcontext))
b072092f	627	{
12f2ffe9	628	mkind = MTC_RESULT;
	629	}
	630	else if (mtContextNode_isLiteral (mcontext))
	631	{
	632	mkind = MTC_LITERAL;
	633	}
	634	else if (mtContextNode_isNull (mcontext))
	635	{
	636	mkind = MTC_NULL;
b072092f	637	}
28bf4b0b	638	else
28bf4b0b	639	{
12f2ffe9	640	DPRINTF (("Bad: %s", mtContextNode_unparse (mcontext)));
28bf4b0b	641	BADBRANCH;
28bf4b0b	642	}
12f2ffe9	643
	644	if (metaStateInfo_getDefaultValueContext (msinfo, mkind) != stateValue_error)
	645	{
	646	voptgenerror
	647	(FLG_SYNTAX,
	648	message ("Duplicate defaults declaration for context %q: %q",
	649	mtContextNode_unparse (mcontext),
	650	mtDefaultsDecl_unparse (mdecl)),
	651	mtDefaultsDecl_getLoc (mdecl));
	652	}
	653	else
	654	{
	655	metaStateInfo_setDefaultValueContext (msinfo, mkind, vindex);
	656	}
28bf4b0b	657	}
	658	else
	659	{
	660	voptgenerror
	661	(FLG_SYNTAX,
	662	message ("Defaults declaration uses unrecognized value name %s: %q",
	663	mvalue, mtDefaultsDecl_unparse (mdecl)),
	664	mtDefaultsDecl_getLoc (mdecl));
	665	}
	666	} end_mtDefaultsDeclList_elements ;
	667	}
	668
	669	mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTVALUE);
	670
	671	if (mtDeclarationPiece_isDefined (mtp))
	672	{
	673	cstring mvalue = mtDeclarationPiece_getDefaultValue (mtp);
	674	llassert (isglobal);
	675
	676	if (cstringList_contains (mvals, mvalue))
	677	{
	678	int vindex = cstringList_getIndex (mvals, mvalue);
	679
	680	if (metaStateInfo_getDefaultRefValue (msinfo) != stateValue_error)
	681	{
	682	voptgenerror
	683	(FLG_SYNTAX,
	684	message ("Duplicate default value declaration for global state: %s",
	685	mvalue),
	686	mtDeclarationNode_getLoc (node));
	687	}
	688	else
	689	{
	690	metaStateInfo_setDefaultRefValue (msinfo, vindex);
	691	}
	692	}
	693	else
	694	{
	695	voptgenerror
	696	(FLG_SYNTAX,
	697	message ("Default value declaration uses unrecognized value name: %s",
	698	mvalue),
	699	mtDeclarationNode_getLoc (node));
	700	}
	701	}
	702
	703	context_addMetaState (cstring_copy (mtDeclarationNode_getName (node)),
	704	msinfo);
	705	}
	706
	707	extern void mtDeclarationNode_free (/@only@/ mtDeclarationNode node)
	708	{
	709	mtDeclarationPieces_free (node->pieces);
	710	cstring_free (node->name);
	711	fileloc_free (node->loc);
	712	sfree (node);
	713	}
	714
	715	extern fileloc mtDeclarationNode_getLoc (mtDeclarationNode node)
	716	{
	717	return node->loc;
	718	}
	719
	720	extern /@observer@/ cstring mtDeclarationNode_getName (mtDeclarationNode node)
721	{
722	return node->name;
723	}