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