[splint.git] / src / mtscanner.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
*/
/*
** mtscanner.c
**
** Because flex is so lame, we can't use two flex scanners at once.  Instead,
** we have to write a manual scanner.  Should look into some real parser 
** generator tools one day...
*/

# include "lclintMacros.nf"
# include "llbasic.h"
# include "mtgrammar.h"
# include "mtscanner.h"

static inputStream scanFile;  /* file to scan */
static mttok mtscanner_getNextToken (void);
static /*@only@*/ cstringTable tokenTable = cstringTable_undefined;
static bool isInitialized = FALSE;

/*@constant int MT_TOKENTABLESIZE@*/
# define MT_TOKENTABLESIZE 64

static void mtscanner_initMod (void)
{
  llassert (cstringTable_isUndefined (tokenTable));
  tokenTable = cstringTable_create (MT_TOKENTABLESIZE);

  cstringTable_insert (tokenTable, cstring_makeLiteral ("attribute"), MT_STATE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("global"), MT_GLOBAL);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("context"), MT_CONTEXT);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("oneof"), MT_ONEOF);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("defaults"), MT_DEFAULTS);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("default"), MT_DEFAULT);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("parameter"), MT_PARAMETER);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("result"), MT_RESULT);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("reference"), MT_REFERENCE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("clause"), MT_CLAUSE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("annotations"), MT_ANNOTATIONS);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("merge"), MT_MERGE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("transfers"), MT_TRANSFERS);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("preconditions"), MT_PRECONDITIONS);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("postconditions"), MT_POSTCONDITIONS);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("losereference"), MT_LOSEREFERENCE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("error"), MT_ERROR);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("end"), MT_END);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("as"), MT_AS);

  /*
  ** C Types
  */

  cstringTable_insert (tokenTable, cstring_makeLiteral ("char"), MT_CHAR);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("int"), MT_INT);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("float"), MT_FLOAT);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("double"), MT_DOUBLE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("void"), MT_VOID);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("anytype"), MT_ANYTYPE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("integraltype"), MT_INTEGRALTYPE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("unsignedintegraltype"), MT_UNSIGNEDINTEGRALTYPE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("signedintegraltype"), MT_SIGNEDINTEGRALTYPE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("const"), MT_CONST);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("volatile"), MT_VOLATILE);

  /*
  ** Punctuation
  */

  cstringTable_insert (tokenTable, cstring_makeLiteral ("==>"), MT_ARROW);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("+"), MT_PLUS);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("*"), MT_STAR);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("{"), MT_LBRACE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("}"), MT_RBRACE);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("("), MT_LPAREN);
  cstringTable_insert (tokenTable, cstring_makeLiteral (")"), MT_RPAREN);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("["), MT_LBRACKET);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("]"), MT_RBRACKET);
  cstringTable_insert (tokenTable, cstring_makeLiteral (","), MT_COMMA);
  cstringTable_insert (tokenTable, cstring_makeLiteral ("|"), MT_BAR);

  isInitialized = TRUE;
}

void mtscanner_reset (inputStream sourceFile)
{
  if (!isInitialized) 
    {
      mtscanner_initMod ();
    }

  scanFile = sourceFile;
}

int mtlex (YYSTYPE *mtlval)
{
  llassert (isInitialized);

  /* This is important!  Bison expects this */

  /*@ignore@*/
  mtlval->tok = mtscanner_getNextToken ();
  DPRINTF (("Return token: %s", mttok_unparse (mtlval->tok)));
  llassert (fileloc_isDefined (mttok_getLoc (mtlval->tok)));
  return (mttok_getTok (mtlval->tok));
  /*@end@*/
}

static void skipComments (void)
{
  int tchar;
  bool gotone = FALSE;
  tchar = inputStream_peekChar (scanFile);

  if (tchar == (int) '/' && inputStream_peekNChar (scanFile, 1) == (int) '*') 
    {
      check ((int) '/' == inputStream_nextChar (scanFile));
      check ((int) '*' == inputStream_nextChar (scanFile));
      
      while ((tchar = inputStream_nextChar (scanFile)) != EOF) 
	{
	  if (tchar == (int) '*' && inputStream_peekChar (scanFile) == (int) '/')
	    {
	      tchar = inputStream_nextChar (scanFile);
	      break;
	    }
	}

      if (tchar == EOF)
	{
	  llfatalerror 
	    (cstring_makeLiteral ("Reached end of metastate file inside comment."));
	  BADBRANCH;
	}
      else
	{
	  check ((int) '/' == tchar);
	  gotone = TRUE;
	}
    }

  if (isspace (tchar)) 
    {
      while (isspace (inputStream_peekChar (scanFile)))
	{
	  tchar = inputStream_nextChar (scanFile);
	}

      gotone = TRUE;
    }

  if (gotone)
    {
      /* If there was a comment or whitespace, need to skip again... */
      skipComments ();
    }
}

static mttok mtscanner_getNextToken ()
{
  int tchar;
  int mtcode;
  cstring tok;
  mttok res;
  fileloc loc;

  skipComments ();
  loc = fileloc_copy (g_currentloc);
  tchar = inputStream_nextChar (scanFile);

  if (tchar == EOF) 
    {
      return mttok_create (EOF, cstring_undefined, loc);
    }

  tok = cstring_newEmpty ();

  DPRINTF (("tchar: %c", (char) tchar));

  if (tchar == (int) '\"') 
    {
      bool escaped = FALSE;

      /* String literal */
      while ((tchar = inputStream_peekChar (scanFile)) != EOF) {
	if (escaped) {
	  escaped = FALSE;
	} else if (tchar == (int) '\\') {
	  escaped = TRUE;
	} else if (tchar == (int) '\"') {
	  break;
	} else {
	  ;
	}

	tok = cstring_appendChar (tok, (char) tchar);
	check (tchar == inputStream_nextChar (scanFile));
      }

      if (tchar == EOF)
	{
	  llfatalerror 
	    (cstring_makeLiteral ("Reached end of metastate file inside string literal."));
	}
      else
	{
	  check ((int) '\"' == inputStream_nextChar (scanFile));
	  return mttok_create (MT_STRINGLIT, tok, loc);
	}
    }
  
  tok = cstring_appendChar (tok, (char) tchar);

  DPRINTF (("tok: %s", tok));

  if (isalpha (tchar)) 
    {
      while ((tchar = inputStream_peekChar (scanFile)) != EOF) {
	if (!isalnum (tchar) && (tchar != (int) '_') && (tchar != (int) '$')) {
	  break;
	}
	
	tok = cstring_appendChar (tok, (char) tchar);
	check (tchar == inputStream_nextChar (scanFile));
      }

      mtcode = cstringTable_lookup (tokenTable, tok);

      if (mtcode == NOT_FOUND) {
	DPRINTF (("Returning identifier: %s", tok));
	return mttok_create (MT_IDENT, tok, loc);
      }
    } 
  else 
    {
      /* Read until next space */
      DPRINTF (("Here we are: %s", tok));

      while ((tchar = inputStream_peekChar (scanFile)) != EOF) {
	if (isspace (tchar) || isalnum (tchar)) {
	  break;
	}
	
	tok = cstring_appendChar (tok, (char) tchar);
	DPRINTF (("Here we are: %s", tok));
	check (tchar == inputStream_nextChar (scanFile));
      }

      DPRINTF (("Here we are: [%s]", tok));
      mtcode = cstringTable_lookup (tokenTable, tok);
      
      if (mtcode == NOT_FOUND) {
	mtcode = MT_BADTOK;
      }
    }
  
  DPRINTF (("Read %s / %d", tok, mtcode));
  cstring_free (tok);

  res = mttok_create (mtcode, cstring_undefined, loc);
  DPRINTF (("Return token: %s", mttok_unparse (res)));
  return res;
}

ctype mtscanner_lookupType (mttok tok)
{
  cstring tname;
  uentry ue;

  llassert (mttok_isIdentifier (tok));
  tname = mttok_observeText (tok);

  DPRINTF (("Lookup type:  %s", tname));

  ue = usymtab_lookupSafe (tname);

  if (uentry_isValid (ue) && uentry_isDatatype (ue))
    {
      DPRINTF (("Found it: %s / %s", uentry_unparse (ue),
		ctype_unparse (uentry_getAbstractType (ue))));
    
      return uentry_getAbstractType (ue);
    }
  else
    {
      ctype ct;
      ue = uentry_makeDatatype (tname, ctype_unknown, MAYBE, MAYBE, mttok_stealLoc (tok));
      DPRINTF (("Making mts entry: %s", uentry_unparse (ue)));
      ct = usymtab_supForwardTypeEntry (ue);
      DPRINTF (("Type: %s", ctype_unparse (ct)));
      return ct;
    }
}
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	** mtscanner.c
	26	**
	27	** Because flex is so lame, we can't use two flex scanners at once. Instead,
	28	** we have to write a manual scanner. Should look into some real parser
	29	** generator tools one day...
	30	*/
	31
	32	# include "lclintMacros.nf"
	33	# include "llbasic.h"
	34	# include "mtgrammar.h"
	35	# include "mtscanner.h"
	36
	37	static inputStream scanFile; /* file to scan */
	38	static mttok mtscanner_getNextToken (void);
	39	static /@only@/ cstringTable tokenTable = cstringTable_undefined;
	40	static bool isInitialized = FALSE;
	41
	42	/@constant int MT_TOKENTABLESIZE@/
	43	# define MT_TOKENTABLESIZE 64
	44
	45	static void mtscanner_initMod (void)
	46	{
	47	llassert (cstringTable_isUndefined (tokenTable));
	48	tokenTable = cstringTable_create (MT_TOKENTABLESIZE);
	49
e26e911c	50	cstringTable_insert (tokenTable, cstring_makeLiteral ("attribute"), MT_STATE);
28bf4b0b	51	cstringTable_insert (tokenTable, cstring_makeLiteral ("global"), MT_GLOBAL);
	52	cstringTable_insert (tokenTable, cstring_makeLiteral ("context"), MT_CONTEXT);
	53	cstringTable_insert (tokenTable, cstring_makeLiteral ("oneof"), MT_ONEOF);
	54	cstringTable_insert (tokenTable, cstring_makeLiteral ("defaults"), MT_DEFAULTS);
	55	cstringTable_insert (tokenTable, cstring_makeLiteral ("default"), MT_DEFAULT);
	56	cstringTable_insert (tokenTable, cstring_makeLiteral ("parameter"), MT_PARAMETER);
b072092f	57	cstringTable_insert (tokenTable, cstring_makeLiteral ("result"), MT_RESULT);
28bf4b0b	58	cstringTable_insert (tokenTable, cstring_makeLiteral ("reference"), MT_REFERENCE);
	59	cstringTable_insert (tokenTable, cstring_makeLiteral ("clause"), MT_CLAUSE);
	60	cstringTable_insert (tokenTable, cstring_makeLiteral ("annotations"), MT_ANNOTATIONS);
	61	cstringTable_insert (tokenTable, cstring_makeLiteral ("merge"), MT_MERGE);
	62	cstringTable_insert (tokenTable, cstring_makeLiteral ("transfers"), MT_TRANSFERS);
	63	cstringTable_insert (tokenTable, cstring_makeLiteral ("preconditions"), MT_PRECONDITIONS);
	64	cstringTable_insert (tokenTable, cstring_makeLiteral ("postconditions"), MT_POSTCONDITIONS);
	65	cstringTable_insert (tokenTable, cstring_makeLiteral ("losereference"), MT_LOSEREFERENCE);
	66	cstringTable_insert (tokenTable, cstring_makeLiteral ("error"), MT_ERROR);
	67	cstringTable_insert (tokenTable, cstring_makeLiteral ("end"), MT_END);
	68	cstringTable_insert (tokenTable, cstring_makeLiteral ("as"), MT_AS);
	69
	70	/*
	71	** C Types
	72	*/
	73
	74	cstringTable_insert (tokenTable, cstring_makeLiteral ("char"), MT_CHAR);
	75	cstringTable_insert (tokenTable, cstring_makeLiteral ("int"), MT_INT);
	76	cstringTable_insert (tokenTable, cstring_makeLiteral ("float"), MT_FLOAT);
	77	cstringTable_insert (tokenTable, cstring_makeLiteral ("double"), MT_DOUBLE);
	78	cstringTable_insert (tokenTable, cstring_makeLiteral ("void"), MT_VOID);
	79	cstringTable_insert (tokenTable, cstring_makeLiteral ("anytype"), MT_ANYTYPE);
	80	cstringTable_insert (tokenTable, cstring_makeLiteral ("integraltype"), MT_INTEGRALTYPE);
	81	cstringTable_insert (tokenTable, cstring_makeLiteral ("unsignedintegraltype"), MT_UNSIGNEDINTEGRALTYPE);
	82	cstringTable_insert (tokenTable, cstring_makeLiteral ("signedintegraltype"), MT_SIGNEDINTEGRALTYPE);
	83	cstringTable_insert (tokenTable, cstring_makeLiteral ("const"), MT_CONST);
	84	cstringTable_insert (tokenTable, cstring_makeLiteral ("volatile"), MT_VOLATILE);
	85
	86	/*
	87	** Punctuation
	88	*/
	89
	90	cstringTable_insert (tokenTable, cstring_makeLiteral ("==>"), MT_ARROW);
	91	cstringTable_insert (tokenTable, cstring_makeLiteral ("+"), MT_PLUS);
	92	cstringTable_insert (tokenTable, cstring_makeLiteral ("*"), MT_STAR);
	93	cstringTable_insert (tokenTable, cstring_makeLiteral ("{"), MT_LBRACE);
	94	cstringTable_insert (tokenTable, cstring_makeLiteral ("}"), MT_RBRACE);
	95	cstringTable_insert (tokenTable, cstring_makeLiteral ("("), MT_LPAREN);
	96	cstringTable_insert (tokenTable, cstring_makeLiteral (")"), MT_RPAREN);
	97	cstringTable_insert (tokenTable, cstring_makeLiteral ("["), MT_LBRACKET);
	98	cstringTable_insert (tokenTable, cstring_makeLiteral ("]"), MT_RBRACKET);
	99	cstringTable_insert (tokenTable, cstring_makeLiteral (","), MT_COMMA);
	100	cstringTable_insert (tokenTable, cstring_makeLiteral ("\|"), MT_BAR);
	101
	102	isInitialized = TRUE;
	103	}
	104
	105	void mtscanner_reset (inputStream sourceFile)
	106	{
	107	if (!isInitialized)
	108	{
	109	mtscanner_initMod ();
	110	}
	111
	112	scanFile = sourceFile;
	113	}
	114
	115	int mtlex (YYSTYPE *mtlval)
	116	{
	117	llassert (isInitialized);
	118
	119	/* This is important! Bison expects this */
	120
	121	/@ignore@/
122	mtlval->tok = mtscanner_getNextToken ();
123	DPRINTF (("Return token: %s", mttok_unparse (mtlval->tok)));
124	llassert (fileloc_isDefined (mttok_getLoc (mtlval->tok)));
125	return (mttok_getTok (mtlval->tok));
126	/@end@/
127	}
128
129	static void skipComments (void)
130	{
131	int tchar;
132	bool gotone = FALSE;
133	tchar = inputStream_peekChar (scanFile);
134
135	if (tchar == (int) '/' && inputStream_peekNChar (scanFile, 1) == (int) '*')
136	{
137	check ((int) '/' == inputStream_nextChar (scanFile));
138	check ((int) '*' == inputStream_nextChar (scanFile));
139
140	while ((tchar = inputStream_nextChar (scanFile)) != EOF)
141	{
142	if (tchar == (int) '*' && inputStream_peekChar (scanFile) == (int) '/')
143	{
144	tchar = inputStream_nextChar (scanFile);
145	break;
146	}
147	}
148
149	if (tchar == EOF)
150	{
151	llfatalerror
152	(cstring_makeLiteral ("Reached end of metastate file inside comment."));
153	BADBRANCH;
154	}
155	else
156	{
157	check ((int) '/' == tchar);
158	gotone = TRUE;
159	}
160	}
161
162	if (isspace (tchar))
163	{
164	while (isspace (inputStream_peekChar (scanFile)))
165	{
166	tchar = inputStream_nextChar (scanFile);
167	}
168
169	gotone = TRUE;
170	}
171
172	if (gotone)
173	{
174	/* If there was a comment or whitespace, need to skip again... */
175	skipComments ();
176	}
177	}
178
179	static mttok mtscanner_getNextToken ()
180	{
181	int tchar;
182	int mtcode;
183	cstring tok;
184	mttok res;
185	fileloc loc;
186
187	skipComments ();
188	loc = fileloc_copy (g_currentloc);
189	tchar = inputStream_nextChar (scanFile);
190
191	if (tchar == EOF)
192	{
193	return mttok_create (EOF, cstring_undefined, loc);
194	}
195
196	tok = cstring_newEmpty ();
197
198	DPRINTF (("tchar: %c", (char) tchar));
199
200	if (tchar == (int) '\"')
201	{
202	bool escaped = FALSE;
203
204	/* String literal */
205	while ((tchar = inputStream_peekChar (scanFile)) != EOF) {
206	if (escaped) {
207	escaped = FALSE;
208	} else if (tchar == (int) '\\') {
209	escaped = TRUE;
210	} else if (tchar == (int) '\"') {
211	break;
212	} else {
213	;
214	}
215
216	tok = cstring_appendChar (tok, (char) tchar);
217	check (tchar == inputStream_nextChar (scanFile));
218	}
219
220	if (tchar == EOF)
221	{
222	llfatalerror
223	(cstring_makeLiteral ("Reached end of metastate file inside string literal."));
224	}
225	else
226	{
227	check ((int) '\"' == inputStream_nextChar (scanFile));
228	return mttok_create (MT_STRINGLIT, tok, loc);
229	}
230	}
231
232	tok = cstring_appendChar (tok, (char) tchar);
233
234	DPRINTF (("tok: %s", tok));
235
236	if (isalpha (tchar))
237	{
238	while ((tchar = inputStream_peekChar (scanFile)) != EOF) {
239	if (!isalnum (tchar) && (tchar != (int) '_') && (tchar != (int) '$')) {
240	break;
241	}
242
243	tok = cstring_appendChar (tok, (char) tchar);
244	check (tchar == inputStream_nextChar (scanFile));
245	}
246
247	mtcode = cstringTable_lookup (tokenTable, tok);
248
249	if (mtcode == NOT_FOUND) {
250	DPRINTF (("Returning identifier: %s", tok));
251	return mttok_create (MT_IDENT, tok, loc);
252	}
253	}
254	else
255	{
256	/* Read until next space */
257	DPRINTF (("Here we are: %s", tok));
258
259	while ((tchar = inputStream_peekChar (scanFile)) != EOF) {
260	if (isspace (tchar) \|\| isalnum (tchar)) {
261	break;
262	}
263
264	tok = cstring_appendChar (tok, (char) tchar);
265	DPRINTF (("Here we are: %s", tok));
266	check (tchar == inputStream_nextChar (scanFile));
267	}
268
269	DPRINTF (("Here we are: [%s]", tok));
270	mtcode = cstringTable_lookup (tokenTable, tok);
271
272	if (mtcode == NOT_FOUND) {
273	mtcode = MT_BADTOK;
274	}
275	}
276
277	DPRINTF (("Read %s / %d", tok, mtcode));
278	cstring_free (tok);
279
280	res = mttok_create (mtcode, cstring_undefined, loc);
281	DPRINTF (("Return token: %s", mttok_unparse (res)));
282	return res;
283	}
284
285	ctype mtscanner_lookupType (mttok tok)
286	{
287	cstring tname;
288	uentry ue;
289
290	llassert (mttok_isIdentifier (tok));
291	tname = mttok_observeText (tok);
292
293	DPRINTF (("Lookup type: %s", tname));
294
295	ue = usymtab_lookupSafe (tname);
296
297	if (uentry_isValid (ue) && uentry_isDatatype (ue))
298	{
299	DPRINTF (("Found it: %s / %s", uentry_unparse (ue),
300	ctype_unparse (uentry_getAbstractType (ue))));
301
302	return uentry_getAbstractType (ue);
303	}
304	else
305	{
306	ctype ct;
307	ue = uentry_makeDatatype (tname, ctype_unknown, MAYBE, MAYBE, mttok_stealLoc (tok));
308	DPRINTF (("Making mts entry: %s", uentry_unparse (ue)));
309	ct = usymtab_supForwardTypeEntry (ue);
310	DPRINTF (("Type: %s", ctype_unparse (ct)));
311	return ct;
312	}
313	}