[splint.git] / src / mtDeclarationNode.c

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

# include "lclintMacros.nf"
# include "basic.h"
# include "mtgrammar.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;

  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 lclint 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_makeLiteral ("Incompatible state merge (default behavior)"));
	    }
	}
    }

  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);
		    }
		}
	    }
	} 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);

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