src/mtscanner.c

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