src/signature.y

   1 /*;-*-C-*-;
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2002 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 "llbasic.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 operatorList: operator
 142               { lslOpList x = lslOpList_new ();
 143                 g_importedlslOp = $1;
 144                 lslOpList_add (x, $1);
 145                 $$ = x; }
 146             | operatorList operator
 147               { lslOpList_add ($1, $2);
 148                 $$ = $1; }
 149
 150 operator: name LST_COLON signature
 151           { $$ = makelslOpNode ($1, $3); }
 152 /* The next production is never used in the output of lsl -syms
 153           |  name
 154           { $$ = makelslOpNode ($1, (sigNode)0); } */
 155
 156 name: opId /* check for the case of if_then_else */
 157       { $$ = makeNameNodeId ($1); }
 158     | opForm
 159       { $$ = makeNameNodeForm ($1); }
 160
 161 opForm
 162      : LST_ifTOKEN LST_MARKERSYM LST_thenTOKEN LST_MARKERSYM LST_elseTOKEN LST_MARKERSYM
 163        { $$ = makeOpFormNode ($1, OPF_IF, opFormUnion_createMiddle (0), ltoken_undefined); }
 164      | anyOp
 165        { $$ = makeOpFormNode ($1, OPF_ANYOP, opFormUnion_createAnyOp ($1), ltoken_undefined); }
 166      | LST_MARKERSYM anyOp
 167        { $$ = makeOpFormNode ($1, OPF_MANYOP, opFormUnion_createAnyOp ($2), ltoken_undefined); }
 168      | anyOp LST_MARKERSYM
 169        { $$ = makeOpFormNode ($1, OPF_ANYOPM, opFormUnion_createAnyOp ($1), ltoken_undefined); }
 170      | LST_MARKERSYM anyOp LST_MARKERSYM
 171        { $$ = makeOpFormNode ($1, OPF_MANYOPM, opFormUnion_createAnyOp ($2), ltoken_undefined); }
 172      | LST_OPENSYM middle LST_CLOSESYM
 173        { $$ = makeOpFormNode ($1, OPF_MIDDLE, opFormUnion_createMiddle ($2), $3); }
 174      | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM
 175        { $$ = makeOpFormNode ($2, OPF_MMIDDLE, opFormUnion_createMiddle ($3), $4); }
 176      | LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM
 177        { $$ = makeOpFormNode ($1, OPF_MIDDLEM, opFormUnion_createMiddle ($2), $3); }
 178      | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM
 179        { $$ = makeOpFormNode ($2, OPF_MMIDDLEM,
 180                               opFormUnion_createMiddle ($3), $4); }
 181      | LST_LBRACKET middle LST_RBRACKET
 182        { $$ = makeOpFormNode ($1, OPF_BMIDDLE,
 183                               opFormUnion_createMiddle ($2), $3); }
 184      | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET
 185        { $$ = makeOpFormNode ($2, OPF_BMMIDDLE,
 186                               opFormUnion_createMiddle ($3), $4); }
 187      | LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM
 188      { $$ = makeOpFormNode ($1, OPF_BMIDDLEM,
 189                             opFormUnion_createMiddle ($2), $3); }
 190      | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM
 191      { $$ = makeOpFormNode ($2, OPF_BMMIDDLEM,
 192                             opFormUnion_createMiddle ($3), $4); }
 193      | LST_SELECTSYM LST_SIMPLEID
 194      { $$ = makeOpFormNode ($1, OPF_SELECT,
 195                             opFormUnion_createAnyOp ($2), ltoken_undefined); }
 196      | LST_MARKERSYM LST_SELECTSYM LST_SIMPLEID
 197      { $$ = makeOpFormNode ($1, OPF_MSELECT,
 198                             opFormUnion_createAnyOp ($3), ltoken_undefined); }
 199         /* not in LSL, need FILEDMAPSYM to distinguish it from MAPSYM */
 200         /* LST_FIELDMAPSYM = "\\field_arrow", only for LCL symtable import */
 201      | LST_MARKERSYM LST_FIELDMAPSYM LST_SIMPLEID
 202      { $$ = makeOpFormNode ($1, OPF_MMAP,
 203                             opFormUnion_createAnyOp ($3), ltoken_undefined); }
 204
 205
 206 anyOp: LST_SIMPLEOP
 207        { $$ = $1; }
 208      | LST_LOGICALOP
 209        { $$ = $1; }
 210      | LST_EQOP
 211        { $$ = $1; }
 212
 213 middle: /* empty */
 214         { $$ = 0; }
 215       | placeList
 216         { $$ = $1; }
 217
 218 placeList: LST_MARKERSYM
 219            { $$ = 1; }
 220          | placeList separator LST_MARKERSYM
 221            { $$ = $1 + 1; }
 222
 223 separator: LST_COMMA
 224            { $$ = $1; }
 225          | LST_SEPSYM
 226            { $$ = $1; }
 227
 228 signature: domain LST_MAPSYM sortId
 229            { $$ = makesigNode ($2, $1, $3); }
 230
 231 domain: /* empty */
 232         { $$ = ltokenList_new (); }
 233       | sortList
 234         { $$ = $1; }
 235
 236 sortList: sortId
 237           { $$ = ltokenList_singleton ($1); }
 238         | sortList LST_COMMA sortId
 239           { $$ = ltokenList_push ($1, $3); }
 240
 241 sortId: LST_SIMPLEID
 242         {
 243           $$ = $1;
 244           ltoken_setText ($$, processTraitSortId (ltoken_getText ($1)));
 245         }
 246
 247 opId: LST_SIMPLEID
 248       { $$ = $1; }
 249 %%
 250
 251 # include "bison.reset"
 252
 253 extern char *yytext;
 254
 255 void lslerror (char *s)
 256 {
 257   llfatalbug
 258     (cstring_makeLiteral
 259      ("There has been a problem in the parser with LSL signatures. This is believed to result "
 260       "from a problem with bison v. 1.25.  Please try rebuidling Splint "
 261       "using the pre-compiled grammar files by commenting out the "
 262       "BISON= line in the top-level Makefile."));
 263 }
 264
 265 static void yyprint (FILE *file, int type, YYSTYPE value)
 266 {
 267   fprintf (file, " (%u:%u type: %d; text: %s) ",
 268            ltoken_getLine (value.ltok),
 269            ltoken_getCol (value.ltok),
 270            type,
 271            ltoken_getRawTextChars (value.ltok));
 272 }
 273
 274 extern void PrintToken (ltoken tok) {
 275   char *codStr;
 276
 277   switch (ltoken_getCode (tok))
 278     {
 279     case NOTTOKEN:          codStr = "*** NOTTOKEN ***"; break;
 280     case LST_QUANTIFIERSYM: codStr = "QUANTIFIERSYM"; break;
 281     case LST_LOGICALOP:     codStr = "LOGICALOP: "; break;
 282     case LST_SELECTSYM:     codStr = "LST_SELECTSYM"; break;
 283     case LST_OPENSYM:       codStr = "LST_OPENSYM"; break;
 284     case LST_SEPSYM:        codStr = "SEPSYM"; break;
 285     case LST_CLOSESYM:      codStr = "LST_CLOSESYM"; break;
 286     case LST_SIMPLEID:      codStr = "LST_SIMPLEID"; break;
 287     case LST_MAPSYM:        codStr = "MAPSYM"; break;
 288     case LST_MARKERSYM:     codStr = "LST_MARKERSYM"; break;
 289     case LST_COMMENTSYM:    codStr = "COMMENTSYM"; break;
 290     case LST_SIMPLEOP:      codStr = "SIMPLEOP"; break;
 291     case LST_COLON:         codStr = "LST_COLON"; break;
 292     case LST_COMMA:         codStr = "COMMA"; break;
 293     case LST_LBRACKET:      codStr = "LST_LBRACKET"; break;
 294     case LST_LPAR:          codStr = "LST_LPAR"; break;
 295     case LST_RBRACKET:      codStr = "LST_RBRACKET"; break;
 296     case LST_RPAR:          codStr = "LST_RPAR"; break;
 297     case LST_EQOP:          codStr = "LST_EQOP"; break;
 298     case LST_WHITESPACE:    codStr = "WHITESPACE,"; break;
 299     case LST_EOL:           codStr = "LST_EOL"; break;
 300     case LST_elseTOKEN:     codStr = "elseTOKEN"; break;
 301     case LST_ifTOKEN:       codStr = "ifTOKEN"; break;
 302     case LST_thenTOKEN:     codStr = "thenTOKEN"; break;
 303     case LST_BADTOKEN:      codStr = "*** BADTOKEN ***"; break;
 304     case LEOFTOKEN: /* can't reach LEOFTOKEN easily */
 305       codStr = "LEOFTOKEN"; break;
 306     default:
 307       codStr = "*** invalid token code ***";
 308       break;
 309     } /* end switch */
 310
 311   /* only used for debugging */
 312   printf ("%u:%u: Token Code (%u): %s",
 313           ltoken_getLine (tok), ltoken_getCol (tok),
 314           ltoken_getCode (tok), codStr);
 315   if (ltoken_getRawText (tok) != 0)
 316     {
 317       printf (", Token String (%lu): %s\n",
 318               ltoken_getRawText (tok), ltoken_getRawTextChars (tok));
 319     }
 320   else printf ("\n");
 321 }
 322
 323
 324
 325