src/mtscanner.c

   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 }