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