src/signature.y

   1 /*;-*-C-*-;
   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: splint@cs.virginia.edu
  21 ** To report a bug: splint-bug@cs.virginia.edu
  22 ** For more information: http://www.splint.org
  23 */
  24 /*
  25 ** signature.y
  26 **
  27 ** Grammar for parsing LSL signatures.
  28 **
  29 ** Original author: Yang Meng Tan, Massachusetts Institute of Technology
  30 */
  31
  32 %{
  33
  34 # include <stdio.h>
  35 # include "splintMacros.nf"
  36 # include "basic.h"
  37 # include "lslparse.h"
  38 # include "signature.h"
  39
  40 static void lslerror (char *);
  41 extern int lsllex ();
  42
  43 /*@dependent@*/ /*@null@*/ lslOp importedlslOp;
  44
  45 /*@-noparams@*/ /* Can't list params since YYSTYPE isn't defined yet. */
  46 static void yyprint (/*FILE *p_file, int p_type, YYSTYPE p_value */);
  47 /*@=noparams@*/
  48
  49 # define YYPRINT(file, type, value) yyprint (file, type, value)
  50
  51 # define YYDEBUG 1
  52
  53 /*@-redef@*/
  54 /*@-readonlytrans@*/
  55 /*@-nullassign@*/
  56
  57 %}
  58
  59 %pure_parser
  60
  61 /* CONVENTIONS:  Reserved words are in ALL CAPS (plus markerSym)
  62                 Characters appearing in the grammar are reserved:
  63                                                 % ( ) , : \ */
  64
  65 /* Changes made
  66    - added LBRACKET stuff in OpForm (missing in LSL)
  67    - dif from LCL: open vs openSym, close vs closeSym
  68    - yylval vs yylval.tok
  69 */
  70
  71 %union {
  72   ltoken ltok;  /* a leaf is also an ltoken */
  73   unsigned int count;
  74   /*@only@*/  ltokenList ltokenList;
  75   /*@only@*/  opFormNode opform;
  76   /*@owned@*/ sigNode signature;
  77   /*@only@*/  nameNode name;
  78   /*@owned@*/ lslOp operator;
  79   /*@only@*/  lslOpList operators;
  80   /*@-redef@*/ /*@-matchfields@*/
  81 }
  82 /*@=redef@*/ /*@=matchfields@*/
  83
  84 %token <ltok> LST_SIMPLEID
  85 %token <ltok> LST_LOGICALOP         /* \implies, \and, \not, \or */
  86 %token <ltok> LST_EQOP              /* \eq, \neq, ==, != */
  87 %token <ltok> LST_SIMPLEOP          /* opSym - reserved */
  88 %token <ltok> LST_MAPSYM            /* LSL's -> */
  89   /* FIELDMAPSYM = "\\field_arrow", only for LCL symtable import */
  90 %token <ltok> LST_FIELDMAPSYM       /* LCL's struct field operator -> */
  91 %token <ltok> LST_MARKERSYM         /* \marker, __ */
  92 %token <ltok> LST_ifTOKEN LST_thenTOKEN LST_elseTOKEN
  93   /* different from LSL: separate LBRACKET from openSym and
  94      RBRACKET from closeSym */
  95 %token <ltok> LST_LBRACKET LST_RBRACKET
  96 %token <ltok> LST_SELECTSYM         /* \select or . */
  97 %token <ltok> LST_SEPSYM LST_OPENSYM LST_CLOSESYM
  98 %token <ltok> LST_COLON             /* : */
  99 %token <ltok> LST_COMMA             /* , */
 100 %token <ltok> LST_EOL LST_COMMENTSYM LST_WHITESPACE
 101
 102 %token LST_WHITESPACE
 103 %token LST_QUANTIFIERSYM
 104 %token LST_EQUATIONSYM
 105 %token LST_EQSEPSYM
 106 %token LST_COMPOSESYM
 107 %token LST_LPAR
 108 %token LST_RPAR
 109 %token LST_assertsTOKEN
 110 %token LST_assumesTOKEN
 111 %token LST_byTOKEN
 112 %token LST_convertsTOKEN
 113 %token LST_enumerationTOKEN
 114 %token LST_equationsTOKEN
 115 %token LST_exemptingTOKEN
 116 %token LST_forTOKEN
 117 %token LST_generatedTOKEN
 118 %token LST_impliesTOKEN
 119 %token LST_includesTOKEN
 120 %token LST_introducesTOKEN
 121 %token LST_ofTOKEN
 122 %token LST_partitionedTOKEN
 123 %token LST_traitTOKEN
 124 %token LST_tupleTOKEN
 125 %token LST_unionTOKEN
 126 %token LST_BADTOKEN
 127
 128 %type <ltok> anyOp separator sortId opId
 129 %type <count> middle placeList
 130 %type <ltokenList> domain sortList
 131 %type <opform> opForm
 132 %type <signature> signature
 133 %type <name> name
 134 %type <operator> operator
 135 %type <operators> operatorList top
 136
 137 %%
 138
 139 top: operatorList { lslOpList_free ($1); }
 140   ;
 141
 142 operatorList: operator
 143               { lslOpList x = lslOpList_new ();
 144                 g_importedlslOp = $1;
 145                 lslOpList_add (x, $1);
 146                 $$ = x; }
 147             | operatorList operator
 148               { lslOpList_add ($1, $2);
 149                 $$ = $1; }
 150 ;
 151
 152 operator: name LST_COLON signature
 153           { $$ = makelslOpNode ($1, $3); }
 154 /* The next production is never used in the output of lsl -syms
 155           |  name
 156           { $$ = makelslOpNode ($1, (sigNode)0); } */
 157 ;
 158
 159 name: opId /* check for the case of if_then_else */
 160       { $$ = makeNameNodeId ($1); }
 161     | opForm
 162       { $$ = makeNameNodeForm ($1); }
 163 ;
 164
 165 opForm
 166      : LST_ifTOKEN LST_MARKERSYM LST_thenTOKEN LST_MARKERSYM LST_elseTOKEN LST_MARKERSYM
 167        { $$ = makeOpFormNode ($1, OPF_IF, opFormUnion_createMiddle (0), ltoken_undefined); }
 168      | anyOp
 169        { $$ = makeOpFormNode ($1, OPF_ANYOP, opFormUnion_createAnyOp ($1), ltoken_undefined); }
 170      | LST_MARKERSYM anyOp
 171        { $$ = makeOpFormNode ($1, OPF_MANYOP, opFormUnion_createAnyOp ($2), ltoken_undefined); }
 172      | anyOp LST_MARKERSYM
 173        { $$ = makeOpFormNode ($1, OPF_ANYOPM, opFormUnion_createAnyOp ($1), ltoken_undefined); }
 174      | LST_MARKERSYM anyOp LST_MARKERSYM
 175        { $$ = makeOpFormNode ($1, OPF_MANYOPM, opFormUnion_createAnyOp ($2), ltoken_undefined); }
 176      | LST_OPENSYM middle LST_CLOSESYM
 177        { $$ = makeOpFormNode ($1, OPF_MIDDLE, opFormUnion_createMiddle ($2), $3); }
 178      | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM
 179        { $$ = makeOpFormNode ($2, OPF_MMIDDLE, opFormUnion_createMiddle ($3), $4); }
 180      | LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM
 181        { $$ = makeOpFormNode ($1, OPF_MIDDLEM, opFormUnion_createMiddle ($2), $3); }
 182      | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM
 183        { $$ = makeOpFormNode ($2, OPF_MMIDDLEM,
 184                               opFormUnion_createMiddle ($3), $4); }
 185      | LST_LBRACKET middle LST_RBRACKET
 186        { $$ = makeOpFormNode ($1, OPF_BMIDDLE,
 187                               opFormUnion_createMiddle ($2), $3); }
 188      | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET
 189        { $$ = makeOpFormNode ($2, OPF_BMMIDDLE,
 190                               opFormUnion_createMiddle ($3), $4); }
 191      | LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM
 192      { $$ = makeOpFormNode ($1, OPF_BMIDDLEM,
 193                             opFormUnion_createMiddle ($2), $3); }
 194      | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM
 195      { $$ = makeOpFormNode ($2, OPF_BMMIDDLEM,
 196                             opFormUnion_createMiddle ($3), $4); }
 197      | LST_SELECTSYM LST_SIMPLEID
 198      { $$ = makeOpFormNode ($1, OPF_SELECT,
 199                             opFormUnion_createAnyOp ($2), ltoken_undefined); }
 200      | LST_MARKERSYM LST_SELECTSYM LST_SIMPLEID
 201      { $$ = makeOpFormNode ($1, OPF_MSELECT,
 202                             opFormUnion_createAnyOp ($3), ltoken_undefined); }
 203         /* not in LSL, need FILEDMAPSYM to distinguish it from MAPSYM */
 204         /* LST_FIELDMAPSYM = "\\field_arrow", only for LCL symtable import */
 205      | LST_MARKERSYM LST_FIELDMAPSYM LST_SIMPLEID
 206      { $$ = makeOpFormNode ($1, OPF_MMAP,
 207                             opFormUnion_createAnyOp ($3), ltoken_undefined); }
 208 ;
 209
 210 anyOp: LST_SIMPLEOP
 211        { $$ = $1; }
 212      | LST_LOGICALOP
 213        { $$ = $1; }
 214      | LST_EQOP
 215        { $$ = $1; }
 216 ;
 217
 218 middle: /* empty */
 219         { $$ = 0; }
 220       | placeList
 221         { $$ = $1; }
 222 ;
 223
 224 placeList: LST_MARKERSYM
 225            { $$ = 1; }
 226          | placeList separator LST_MARKERSYM
 227            { $$ = $1 + 1; }
 228 ;
 229
 230 separator: LST_COMMA
 231            { $$ = $1; }
 232          | LST_SEPSYM
 233            { $$ = $1; }
 234 ;
 235
 236 signature: domain LST_MAPSYM sortId
 237            { $$ = makesigNode ($2, $1, $3); }
 238 ;
 239
 240 domain: /* empty */
 241         { $$ = ltokenList_new (); }
 242       | sortList
 243         { $$ = $1; }
 244 ;
 245
 246 sortList: sortId
 247           { $$ = ltokenList_singleton ($1); }
 248         | sortList LST_COMMA sortId
 249           { $$ = ltokenList_push ($1, $3); }
 250 ;
 251
 252 sortId: LST_SIMPLEID
 253         {
 254           $$ = $1;
 255           ltoken_setText ($$, processTraitSortId (ltoken_getText ($1)));
 256         }
 257 ;
 258
 259 opId: LST_SIMPLEID
 260       { $$ = $1; }
 261 ;
 262
 263 %%
 264
 265 # include "bison.reset"
 266
 267 extern char *yytext;
 268
 269 void lslerror (char *s)
 270 {
 271   llfatalbug
 272     (cstring_makeLiteral
 273      ("There has been a problem in the parser with LSL signatures. This is believed to result "
 274       "from a problem with bison v. 1.25.  Please try rebuidling Splint "
 275       "using the pre-compiled grammar files by commenting out the "
 276       "BISON= line in the top-level Makefile."));
 277 }
 278
 279 static void yyprint (FILE *file, int type, YYSTYPE value)
 280 {
 281   fprintf (file, " (%u:%u type: %d; text: %s) ",
 282            ltoken_getLine (value.ltok),
 283            ltoken_getCol (value.ltok),
 284            type,
 285            ltoken_getRawTextChars (value.ltok));
 286 }
 287
 288 extern void PrintToken (ltoken tok) {
 289   char *codStr;
 290
 291   switch (ltoken_getCode (tok))
 292     {
 293     case NOTTOKEN:          codStr = "*** NOTTOKEN ***"; break;
 294     case LST_QUANTIFIERSYM: codStr = "QUANTIFIERSYM"; break;
 295     case LST_LOGICALOP:     codStr = "LOGICALOP: "; break;
 296     case LST_SELECTSYM:     codStr = "LST_SELECTSYM"; break;
 297     case LST_OPENSYM:       codStr = "LST_OPENSYM"; break;
 298     case LST_SEPSYM:        codStr = "SEPSYM"; break;
 299     case LST_CLOSESYM:      codStr = "LST_CLOSESYM"; break;
 300     case LST_SIMPLEID:      codStr = "LST_SIMPLEID"; break;
 301     case LST_MAPSYM:        codStr = "MAPSYM"; break;
 302     case LST_MARKERSYM:     codStr = "LST_MARKERSYM"; break;
 303     case LST_COMMENTSYM:    codStr = "COMMENTSYM"; break;
 304     case LST_SIMPLEOP:      codStr = "SIMPLEOP"; break;
 305     case LST_COLON:         codStr = "LST_COLON"; break;
 306     case LST_COMMA:         codStr = "COMMA"; break;
 307     case LST_LBRACKET:      codStr = "LST_LBRACKET"; break;
 308     case LST_LPAR:          codStr = "LST_LPAR"; break;
 309     case LST_RBRACKET:      codStr = "LST_RBRACKET"; break;
 310     case LST_RPAR:          codStr = "LST_RPAR"; break;
 311     case LST_EQOP:          codStr = "LST_EQOP"; break;
 312     case LST_WHITESPACE:    codStr = "WHITESPACE,"; break;
 313     case LST_EOL:           codStr = "LST_EOL"; break;
 314     case LST_elseTOKEN:     codStr = "elseTOKEN"; break;
 315     case LST_ifTOKEN:       codStr = "ifTOKEN"; break;
 316     case LST_thenTOKEN:     codStr = "thenTOKEN"; break;
 317     case LST_BADTOKEN:      codStr = "*** BADTOKEN ***"; break;
 318     case LEOFTOKEN: /* can't reach LEOFTOKEN easily */
 319       codStr = "LEOFTOKEN"; break;
 320     default:
 321       codStr = "*** invalid token code ***";
 322       break;
 323     } /* end switch */
 324
 325   /* only used for debugging */
 326   printf ("%u:%u: Token Code (%u): %s",
 327           ltoken_getLine (tok), ltoken_getCol (tok),
 328           ltoken_getCode (tok), codStr);
 329   if (ltoken_getRawText (tok) != 0)
 330     {
 331       printf (", Token String (%lu): %s\n",
 332               ltoken_getRawText (tok), ltoken_getRawTextChars (tok));
 333     }
 334   else printf ("\n");
 335 }
 336
 337
 338
 339