src/mtgrammar.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 ** mtgrammar.y
  26 **
  27 ** Grammar for .mts files.
  28 */
  29
  30 %{
  31
  32 # include "bison.reset"
  33 # include "splintMacros.nf"
  34 # include "llbasic.h"
  35
  36 # ifndef S_SPLINT_S
  37 extern ctype mtscanner_lookupType (mttok p_tok) /*@modifies p_tok@*/ ;
  38 # endif
  39
  40   /*@i523@*/ /* can't include these here
  41     # include "mtgrammar.h"
  42     # include "mtscanner.h"
  43   */
  44
  45 static /*@noreturn@*/ void mterror (char *);
  46
  47 /*@-noparams@*/ /* Can't list params since YYSTYPE isn't defined yet. */
  48 extern int mtlex () ;
  49 static void yyprint (/*FILE *p_file, int p_type, YYSTYPE p_value */);
  50 /*@=noparams@*/
  51
  52 # define YYPRINT(file, type, value) yyprint (file, type, value)
  53
  54 # define YYDEBUG 1
  55
  56 # include "bison.head"
  57
  58 %}
  59
  60 %pure_parser
  61
  62 %union {
  63   mttok tok;
  64   mtDeclarationNode mtdecl;
  65   mtDeclarationPiece mtpiece;
  66   mtDeclarationPieces mtpieces;
  67   mtContextNode mtcontext;
  68   mtValuesNode mtvalues;
  69   mtDefaultsNode mtdefaults;
  70   mtDefaultsDeclList mtdeflist;
  71   mtAnnotationsNode mtannotations;
  72   mtAnnotationList mtannotlist;
  73   mtAnnotationDecl mtannotdecl;
  74   mtMergeNode mtmerge;
  75   mtMergeItem mtmergeitem;
  76   mtMergeClauseList mtmergeclauselist;
  77   mtMergeClause mtmergeclause;
  78   mtTransferClauseList mttransferclauselist;
  79   mtTransferClause mttransferclause;
  80   mtTransferAction mttransferaction;
  81   mtLoseReferenceList mtlosereferencelist;
  82   mtLoseReference mtlosereference;
  83
  84   /*@only@*/ cstringList cstringlist;
  85   ctype ctyp;
  86   /*@only@*/ qtype qtyp;
  87   int count;
  88 }
  89
  90 /* Don't forget to enter all tokens in mtscanner.c */
  91 %token <tok> MT_BADTOK
  92
  93 %token <tok> MT_END
  94 %token <tok> MT_STATE MT_GLOBAL
  95
  96 %token <tok> MT_CONTEXT
  97 %token <tok> MT_ONEOF
  98
  99 %token <tok> MT_DEFAULTS MT_DEFAULT
 100 %token <tok> MT_REFERENCE MT_PARAMETER MT_RESULT MT_CLAUSE MT_LITERAL MT_NULL
 101
 102 %token <tok> MT_ANNOTATIONS
 103 %token <tok> MT_ARROW
 104
 105 %token <tok> MT_MERGE
 106 %token <tok> MT_TRANSFERS MT_PRECONDITIONS MT_POSTCONDITIONS
 107 %token <tok> MT_LOSEREFERENCE
 108
 109 %token <tok> MT_AS
 110 %token <tok> MT_ERROR
 111
 112 %token <tok> MT_PLUS MT_STAR MT_BAR
 113 %token <tok> MT_LPAREN MT_RPAREN
 114 %token <tok> MT_LBRACKET MT_RBRACKET
 115 %token <tok> MT_LBRACE MT_RBRACE
 116 %token <tok> MT_COMMA
 117
 118 %token <tok> MT_CHAR MT_INT MT_FLOAT MT_DOUBLE MT_VOID  MT_ANYTYPE MT_INTEGRALTYPE MT_UNSIGNEDINTEGRALTYPE
 119 %token <tok> MT_SIGNEDINTEGRALTYPE
 120 %token <tok> MT_CONST MT_VOLATILE
 121 %token <tok> MT_STRINGLIT
 122 %token <tok> MT_IDENT
 123
 124 %type <count> pointers
 125 %type <ctyp> optType typeSpecifier typeName abstractDecl abstractDeclBase
 126 %type <qtyp> typeExpression
 127 %type <qtyp> completeType completeTypeAux optCompleteType
 128 %type <mtpiece> declarationPiece
 129 %type <mtcontext> contextDeclaration
 130 %type <mtcontext> contextSelection optContextSelection
 131 %type <mtvalues> valuesDeclaration
 132 %type <tok> defaultNode
 133 %type <mtdefaults> defaultsDeclaration
 134 %type <mtdeflist> defaultDeclarationList
 135 %type <mtannotations> annotationsDeclaration
 136 %type <mtannotlist> annotationsDeclarationList
 137 %type <mtannotdecl> annotationDeclaration
 138 %type <mtmerge> mergeDeclaration
 139 %type <mtmergeitem> mergeItem
 140 %type <mtmergeclauselist> mergeClauses
 141 %type <mtmergeclause> mergeClause
 142 %type <mttransferclauselist> transfersDeclaration transferClauses preconditionsDeclaration postconditionsDeclaration
 143 %type <mttransferclause> transferClause
 144 %type <mttransferaction> transferAction errorAction
 145 %type <mtlosereferencelist> loseReferenceDeclaration lostClauses
 146 %type <mtlosereference> lostClause
 147 %type <cstringlist> valuesList
 148 %type <mtdecl> declarationNode
 149 %type <mtpieces> declarationPieces
 150 %type <tok> valueChoice
 151
 152
 153 %start file
 154
 155 %%
 156
 157 file
 158 : {}
 159 | mtsDeclaration {}
 160
 161 mtsDeclaration
 162 : MT_STATE declarationNode MT_END
 163   { mtreader_processDeclaration ($2); }
 164 | MT_GLOBAL MT_STATE declarationNode MT_END
 165   { mtreader_processGlobalDeclaration ($3); }
 166
 167 declarationNode
 168 : MT_IDENT declarationPieces
 169   { $$ = mtDeclarationNode_create ($1, $2); }
 170
 171 declarationPieces
 172 : { $$ = mtDeclarationPieces_create (); }
 173 | declarationPiece declarationPieces
 174   { $$ = mtDeclarationPieces_append ($2, $1); }
 175
 176 declarationPiece
 177 : contextDeclaration { $$ = mtDeclarationPiece_createContext ($1); }
 178 | valuesDeclaration { $$ = mtDeclarationPiece_createValues ($1); }
 179 | defaultsDeclaration { $$ = mtDeclarationPiece_createDefaults ($1); }
 180 | defaultNode { $$ = mtDeclarationPiece_createValueDefault ($1); }
 181 | annotationsDeclaration { $$ = mtDeclarationPiece_createAnnotations ($1); }
 182 | mergeDeclaration { $$ = mtDeclarationPiece_createMerge ($1); }
 183 | transfersDeclaration { $$ = mtDeclarationPiece_createTransfers ($1); }
 184 | preconditionsDeclaration { $$ = mtDeclarationPiece_createPreconditions ($1); }
 185 | postconditionsDeclaration { $$ = mtDeclarationPiece_createPostconditions ($1); }
 186 | loseReferenceDeclaration { $$ = mtDeclarationPiece_createLosers ($1); }
 187
 188 contextDeclaration
 189 : MT_CONTEXT contextSelection { $$ = $2; }
 190   /* ??? should it be a list? */
 191
 192 optContextSelection
 193 : /* empty */ { $$ = mtContextNode_createAny (); }
 194 | contextSelection
 195
 196 contextSelection
 197 : MT_PARAMETER optType { $$ = mtContextNode_createParameter ($2); }
 198 | MT_REFERENCE optType { $$ = mtContextNode_createReference ($2); }
 199 | MT_RESULT optType    { $$ = mtContextNode_createResult ($2); }
 200 | MT_CLAUSE optType    { $$ = mtContextNode_createClause ($2); }
 201 | MT_LITERAL optType   { $$ = mtContextNode_createLiteral ($2); }
 202 | MT_NULL optType      { $$ = mtContextNode_createNull ($2); }
 203
 204 /*
 205 ** Wish I could share the C grammar here...cut-and-paste instead.
 206 */
 207
 208 optType
 209 : /* empty */ { $$ = ctype_unknown; }
 210 | typeExpression { DPRINTF (("Type: %s", qtype_unparse ($1))); $$ = qtype_getType ($1); }
 211
 212 typeExpression
 213 : completeType
 214 | completeType abstractDecl  { $$ = qtype_newBase ($1, $2); }
 215
 216 completeType
 217 : completeTypeAux { $$ = $1; }
 218 | completeType MT_BAR typeExpression
 219   { $$ = qtype_mergeAlt ($1, $3); }
 220
 221 completeTypeAux
 222 : typeSpecifier optCompleteType { $$ = qtype_combine ($2, $1); }
 223
 224 optCompleteType
 225 : /* empty */ { $$ = qtype_unknown (); }
 226 | completeType { $$ = $1; }
 227
 228
 229 abstractDecl
 230  : pointers { $$ = ctype_adjustPointers ($1, ctype_unknown); }
 231  | abstractDeclBase
 232  | pointers abstractDeclBase { $$ = ctype_adjustPointers ($1, $2); }
 233
 234 pointers
 235  : MT_STAR { $$ = 1; }
 236  | MT_STAR innerModsList { $$ = 1; }
 237  | MT_STAR pointers { $$ = 1 + $2; }
 238  | MT_STAR innerModsList pointers { $$ = 1 + $3; }
 239
 240 innerMods
 241  : MT_CONST    { /* ignored for now */; }
 242  | MT_VOLATILE { ; }
 243
 244 innerModsList
 245  : innerMods { ; }
 246  | innerModsList innerMods { ; }
 247
 248 abstractDeclBase
 249  : MT_LPAREN abstractDecl MT_RPAREN { $$ = ctype_expectFunction ($2); }
 250  | MT_LBRACKET MT_RBRACKET { $$ = ctype_makeArray (ctype_unknown); }
 251  | abstractDeclBase MT_LBRACKET MT_RBRACKET { $$ = ctype_makeArray ($1); }
 252 /*
 253  | abstractDeclBase MT_LBRACKET constantExpr MT_RBRACKET
 254    { $$ = ctype_makeFixedArray ($1, exprNode_getLongValue ($3)); }
 255 */
 256
 257 typeSpecifier
 258 : MT_CHAR { $$ = ctype_char; }
 259 | MT_INT { $$ = ctype_int; }
 260 | MT_FLOAT { $$ = ctype_float; }
 261 | MT_DOUBLE { $$ = ctype_double; }
 262 | MT_VOID { $$ = ctype_void; }
 263 | MT_ANYTYPE { $$ = ctype_unknown; }
 264 | MT_INTEGRALTYPE { $$ = ctype_anyintegral; }
 265 | MT_UNSIGNEDINTEGRALTYPE { $$ = ctype_unsignedintegral; }
 266 | MT_SIGNEDINTEGRALTYPE { $$ = ctype_signedintegral; }
 267 | typeName
 268  /* | suSpc
 269  | enumSpc
 270  | typeModifier NotType { $$ = ctype_fromQual ($1); } */
 271
 272 typeName
 273  : MT_IDENT { $$ = mtscanner_lookupType ($1); }
 274
 275 valuesDeclaration
 276 : MT_ONEOF valuesList { $$ = mtValuesNode_create ($2); }
 277
 278 valuesList
 279 : MT_IDENT { $$ = cstringList_single (mttok_getText ($1)); }
 280 | MT_IDENT MT_COMMA valuesList
 281   { $$ = cstringList_prepend ($3, mttok_getText ($1)); }
 282
 283 defaultNode
 284 : MT_DEFAULT valueChoice { $$ = $2; }
 285
 286 defaultsDeclaration
 287 : MT_DEFAULTS defaultDeclarationList { $$ = mtDefaultsNode_create ($1, $2); }
 288
 289 defaultDeclarationList
 290 : contextSelection MT_ARROW valueChoice
 291 { $$ = mtDefaultsDeclList_single (mtDefaultsDecl_create ($1, $3)); }
 292 | contextSelection MT_ARROW valueChoice defaultDeclarationList
 293 { $$ = mtDefaultsDeclList_prepend ($4, mtDefaultsDecl_create ($1, $3)); }
 294
 295 annotationsDeclaration
 296 : MT_ANNOTATIONS annotationsDeclarationList { $$ = mtAnnotationsNode_create ($2); }
 297
 298 annotationsDeclarationList
 299 : annotationDeclaration { $$ = mtAnnotationList_single ($1); }
 300 | annotationDeclaration annotationsDeclarationList
 301   { $$ = mtAnnotationList_prepend ($2, $1); }
 302
 303 annotationDeclaration
 304 : MT_IDENT optContextSelection MT_ARROW valueChoice
 305   { $$ = mtAnnotationDecl_create ($1, $2, $4); }
 306
 307 mergeDeclaration
 308 : MT_MERGE mergeClauses { $$ = mtMergeNode_create ($2); }
 309
 310 mergeClauses
 311 : mergeClause { $$ = mtMergeClauseList_single ($1); }
 312 | mergeClause mergeClauses { $$ = mtMergeClauseList_prepend ($2, $1); }
 313
 314 mergeClause
 315 : mergeItem MT_PLUS mergeItem MT_ARROW transferAction
 316   { $$ = mtMergeClause_create ($1, $3, $5); }
 317
 318 mergeItem
 319 : valueChoice { $$ = mtMergeItem_createValue ($1); }
 320 | MT_STAR { $$ = mtMergeItem_createStar ($1); }
 321
 322 preconditionsDeclaration
 323 : MT_PRECONDITIONS transferClauses { $$ = $2; }
 324
 325 postconditionsDeclaration
 326 : MT_POSTCONDITIONS transferClauses { $$ = $2; }
 327
 328 transfersDeclaration
 329 : MT_TRANSFERS transferClauses { $$ = $2; }
 330
 331 loseReferenceDeclaration
 332 : MT_LOSEREFERENCE lostClauses { $$ = $2; }
 333
 334 lostClauses
 335 : lostClause { $$ = mtLoseReferenceList_single ($1); }
 336 | lostClause lostClauses { $$ = mtLoseReferenceList_prepend ($2, $1); }
 337
 338 lostClause
 339 : valueChoice MT_ARROW errorAction { $$ = mtLoseReference_create ($1, $3); }
 340
 341 transferClauses
 342 : transferClause { $$ = mtTransferClauseList_single ($1); }
 343 | transferClause transferClauses { $$ = mtTransferClauseList_prepend ($2, $1); }
 344
 345 transferClause
 346 : valueChoice MT_AS valueChoice MT_ARROW transferAction
 347   { $$ = mtTransferClause_create ($1, $3, $5); }
 348
 349 transferAction
 350 : valueChoice { $$ = mtTransferAction_createValue ($1); }
 351 | errorAction { $$ = $1; }
 352
 353 errorAction
 354 : MT_ERROR { $$ = mtTransferAction_createError ($1); }
 355 | MT_ERROR MT_STRINGLIT { $$ = mtTransferAction_createErrorMessage ($2); }
 356
 357 valueChoice
 358  : MT_IDENT
 359
 360 %%
 361
 362 # include "bison.reset"
 363
 364 extern char *yytext;
 365
 366 static void mterror (char *s)
 367 {
 368
 369   if (s != NULL)
 370     {
 371       llparseerror
 372         (message ("Parse error in meta-state file: %s", cstring_fromChars (s)));
 373     }
 374   else
 375     {
 376       llparseerror
 377         (message ("Parse error in meta-state file"));
 378     }
 379
 380 }
 381
 382 static void yyprint (FILE *file, int type, YYSTYPE value)
 383 {
 384   cstring tname = mttok_unparse (value.tok);
 385   fprintf (file, " (%s)", cstring_toCharsSafe (tname));
 386   cstring_free (tname);
 387 }
 388
 389
 390
 391