src/signature.y

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