src/mtDeclarationNode.c

   1 /*
   2 ** LCLint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2001 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 lclint: lclint-request@cs.virginia.edu
  21 ** To report a bug: lclint-bug@cs.virginia.edu
  22 ** For more information: http://lclint.cs.virginia.edu
  23 */
  24 /*
  25 ** mtDeclarationNode.c
  26 */
  27
  28 # include "lclintMacros.nf"
  29 # include "basic.h"
  30 # include "mtgrammar.h"
  31
  32 extern mtDeclarationNode mtDeclarationNode_create (mttok name, mtDeclarationPieces pieces) /*@*/
  33 {
  34   mtDeclarationNode res = (mtDeclarationNode) dmalloc (sizeof (*res));
  35
  36   res->name = mttok_getText (name);
  37   res->loc = mttok_stealLoc (name);
  38   res->pieces = pieces;
  39
  40   mttok_free (name);
  41   return res;
  42 }
  43
  44 extern cstring mtDeclarationNode_unparse (mtDeclarationNode node) /*@*/
  45 {
  46   return message ("state %s %q",
  47                   node->name,
  48                   mtDeclarationPieces_unparse (node->pieces));
  49 }
  50
  51 extern void mtDeclarationNode_process (mtDeclarationNode node, bool isglobal)
  52 {
  53   int i;
  54   int j;
  55
  56   mtDeclarationPieces pieces;
  57   mtDeclarationPiece mtp;
  58   mtContextNode mtcontext;
  59   stateCombinationTable tsc;
  60   stateCombinationTable tmerge;
  61   cstringList mvals;
  62   metaStateInfo msinfo;
  63   int nvalues;
  64
  65   pieces = node->pieces;
  66
  67   /*
  68   ** First, we need to find the values piece.
  69   */
  70
  71   mtp = mtDeclarationPieces_findPiece (pieces, MTP_VALUES);
  72
  73   if (mtDeclarationPiece_isUndefined (mtp))
  74     {
  75       voptgenerror (FLG_SYNTAX,
  76                     message ("Metastate declaration missing values clause: %s",
  77                              mtDeclarationNode_getName (node)),
  78                     mtDeclarationNode_getLoc (node));
  79       return;
  80     }
  81   else
  82     {
  83       mtValuesNode  mtv = mtDeclarationPiece_getValues (mtp);
  84       mvals = mtValuesNode_getValues (mtv);
  85     }
  86
  87   /*@-usedef@*/ /*@i34 lclint should figure this out... */
  88   nvalues = cstringList_size (mvals);
  89   /*@=usedef@*/
  90
  91   mtp = mtDeclarationPieces_findPiece (pieces, MTP_CONTEXT);
  92
  93   if (mtDeclarationPiece_isUndefined (mtp))
  94     {
  95       ; /* No context, assume anywhere is okay. */
  96       mtcontext = mtContextNode_createAny ();
  97     }
  98   else
  99     {
 100       mtcontext = mtDeclarationPiece_stealContext (mtp);
 101     }
 102
 103   if (isglobal)
 104     {
 105       /*
 106       ** For global state, instead of a transfers piece, we have constraints.
 107       */
 108
 109       mtp = mtDeclarationPieces_findPiece (pieces, MTP_TRANSFERS);
 110
 111       if (!mtDeclarationPiece_isUndefined (mtp))
 112         {
 113           voptgenerror (FLG_SYNTAX,
 114                         message ("Global state declaration uses transfers clause.  Should use preconditions and postconsitions clauses instead: %s",
 115                                  mtDeclarationNode_getName (node)),
 116                         mtDeclarationNode_getLoc (node));
 117           mtContextNode_free (mtcontext);
 118           return;
 119         }
 120
 121       mtp = mtDeclarationPieces_findPiece (pieces, MTP_PRECONDITIONS);
 122
 123       if (mtDeclarationPiece_isUndefined (mtp))
 124         {
 125           voptgenerror (FLG_SYNTAX,
 126                         message ("Metastate declaration missing preconditions clause: %s",
 127                                  mtDeclarationNode_getName (node)),
 128                         mtDeclarationNode_getLoc (node));
 129           mtContextNode_free (mtcontext);
 130           return;
 131         }
 132       else
 133         {
 134           mtTransferClauseList mtransfers = mtDeclarationPiece_getPreconditions (mtp);
 135           tsc = stateCombinationTable_create (nvalues);
 136
 137           mtTransferClauseList_elements (mtransfers, transfer)
 138             {
 139               cstring tfrom = mtTransferClause_getFrom (transfer);
 140               cstring tto = mtTransferClause_getTo (transfer);
 141               mtTransferAction taction = mtTransferClause_getAction (transfer);
 142               cstring vname = mtTransferAction_getValue (taction);
 143
 144               int fromindex;
 145               int toindex;
 146               int vindex;
 147
 148               DPRINTF (("Transfer: %s", mtTransferClause_unparse (transfer)));
 149
 150               if (cstringList_contains (mvals, tfrom))
 151                 {
 152                   fromindex = cstringList_getIndex (mvals, tfrom);
 153                 }
 154               else
 155                 {
 156                   voptgenerror
 157                     (FLG_SYNTAX,
 158                      message ("Precondition clause uses unrecognized caller value %s: %q",
 159                               tfrom, mtTransferClause_unparse (transfer)),
 160                      mtTransferClause_getLoc (transfer));
 161                   continue;
 162                 }
 163
 164               if (cstringList_contains (mvals, tto))
 165                 {
 166                   toindex = cstringList_getIndex (mvals, tto);
 167                 }
 168               else
 169                 {
 170                   voptgenerror
 171                     (FLG_SYNTAX,
 172                      message ("Precondition clause uses unrecognized constraint value %s: %q",
 173                               tto, mtTransferClause_unparse (transfer)),
 174                      mtTransferClause_getLoc (transfer));
 175                   continue;
 176                 }
 177
 178               if (mtTransferAction_isError (taction))
 179                 {
 180                   vindex = metaState_error;
 181                 }
 182               else
 183                 {
 184                   if (cstringList_contains (mvals, vname))
 185                     {
 186                       vindex = cstringList_getIndex (mvals, vname);
 187                     }
 188                   else
 189                     {
 190                       voptgenerror
 191                         (FLG_SYNTAX,
 192                          message ("Precondition clause uses unrecognized result state %s: %q",
 193                                   vname, mtTransferClause_unparse (transfer)),
 194                          mtTransferClause_getLoc (transfer));
 195                       continue;
 196                     }
 197                 }
 198
 199               if (mtTransferAction_isError (taction))
 200                 {
 201                   stateCombinationTable_set
 202                     (tsc, fromindex, toindex,
 203                      vindex,
 204                      cstring_copy (mtTransferAction_getMessage (taction)));
 205                 }
 206               else
 207                 {
 208                   stateCombinationTable_set (tsc, fromindex, toindex,
 209                                              vindex,
 210                                              cstring_undefined);
 211                 }
 212             } end_mtTransferClauseList_elements ;
 213         }
 214     }
 215   else
 216     {
 217       mtp = mtDeclarationPieces_findPiece (pieces, MTP_PRECONDITIONS);
 218
 219       if (!mtDeclarationPiece_isUndefined (mtp))
 220         {
 221           voptgenerror
 222             (FLG_SYNTAX,
 223              message ("Non-global state declaration uses preconditions clause. "
 224                       "Should use transfers clause instead: %s",
 225                       mtDeclarationNode_getName (node)),
 226              mtDeclarationNode_getLoc (node));
 227           mtContextNode_free (mtcontext);
 228           return;
 229         }
 230
 231       mtp = mtDeclarationPieces_findPiece (pieces, MTP_POSTCONDITIONS);
 232
 233       if (!mtDeclarationPiece_isUndefined (mtp))
 234         {
 235           voptgenerror
 236             (FLG_SYNTAX,
 237              message ("Non-global state declaration uses postconditions clause. "
 238                       "Should use transfers clause instead: %s",
 239                       mtDeclarationNode_getName (node)),
 240              mtDeclarationNode_getLoc (node));
 241           mtContextNode_free (mtcontext);
 242           return;
 243         }
 244
 245       mtp = mtDeclarationPieces_findPiece (pieces, MTP_TRANSFERS);
 246
 247       if (mtDeclarationPiece_isUndefined (mtp))
 248         {
 249           voptgenerror (FLG_SYNTAX,
 250                         message ("Metastate declaration missing transfers clause: %s",
 251                                  mtDeclarationNode_getName (node)),
 252                         mtDeclarationNode_getLoc (node));
 253           mtContextNode_free (mtcontext);
 254           return;
 255         }
 256       else
 257         {
 258           mtTransferClauseList mtransfers = mtDeclarationPiece_getTransfers (mtp);
 259           tsc = stateCombinationTable_create (nvalues);
 260
 261           mtTransferClauseList_elements (mtransfers, transfer)
 262             {
 263               cstring tfrom = mtTransferClause_getFrom (transfer);
 264               cstring tto = mtTransferClause_getTo (transfer);
 265               mtTransferAction taction = mtTransferClause_getAction (transfer);
 266               cstring vname = mtTransferAction_getValue (taction);
 267
 268               int fromindex;
 269               int toindex;
 270               int vindex;
 271
 272               DPRINTF (("Transfer: %s", mtTransferClause_unparse (transfer)));
 273
 274               if (cstringList_contains (mvals, tfrom))
 275                 {
 276                   fromindex = cstringList_getIndex (mvals, tfrom);
 277                 }
 278               else
 279                 {
 280                   voptgenerror
 281                     (FLG_SYNTAX,
 282                      message ("Transfer clause uses unrecognized from value %s: %q",
 283                               tfrom, mtTransferClause_unparse (transfer)),
 284                      mtTransferClause_getLoc (transfer));
 285                   continue;
 286                 }
 287
 288               if (cstringList_contains (mvals, tto))
 289                 {
 290                   toindex = cstringList_getIndex (mvals, tto);
 291                 }
 292               else
 293                 {
 294                   voptgenerror
 295                     (FLG_SYNTAX,
 296                      message ("Transfer clause uses unrecognized to value %s: %q",
 297                               tto, mtTransferClause_unparse (transfer)),
 298                      mtTransferClause_getLoc (transfer));
 299                   continue;
 300                 }
 301
 302               if (mtTransferAction_isError (taction))
 303                 {
 304                   vindex = metaState_error;
 305                 }
 306               else
 307                 {
 308                   if (cstringList_contains (mvals, vname))
 309                     {
 310                       vindex = cstringList_getIndex (mvals, vname);
 311                     }
 312                   else
 313                     {
 314                       voptgenerror
 315                         (FLG_SYNTAX,
 316                          message ("Transfer clause uses unrecognized result state %s: %q",
 317                                   vname, mtTransferClause_unparse (transfer)),
 318                          mtTransferClause_getLoc (transfer));
 319                       continue;
 320                     }
 321                 }
 322
 323               if (mtTransferAction_isError (taction))
 324                 {
 325                   stateCombinationTable_set
 326                     (tsc, fromindex, toindex,
 327                      vindex,
 328                      cstring_copy (mtTransferAction_getMessage (taction)));
 329                 }
 330               else
 331                 {
 332                   stateCombinationTable_set (tsc, fromindex, toindex,
 333                                              vindex,
 334                                              cstring_undefined);
 335                 }
 336             } end_mtTransferClauseList_elements ;
 337         }
 338     }
 339
 340   mtp = mtDeclarationPieces_findPiece (pieces, MTP_LOSERS);
 341
 342   if (mtDeclarationPiece_isDefined (mtp))
 343     {
 344       mtLoseReferenceList mlosers = mtDeclarationPiece_getLosers (mtp);
 345
 346       mtLoseReferenceList_elements (mlosers, loseref)
 347         {
 348           cstring tfrom = mtLoseReference_getFrom (loseref);
 349           mtTransferAction taction = mtLoseReference_getAction (loseref);
 350           int fromindex;
 351           /* Losing reference is represented by transfer to nvalues */
 352           int toindex = nvalues;
 353           int vindex = metaState_error;
 354
 355           llassert (mtTransferAction_isError (taction));
 356
 357           if (cstringList_contains (mvals, tfrom))
 358             {
 359               fromindex = cstringList_getIndex (mvals, tfrom);
 360             }
 361           else
 362             {
 363               voptgenerror
 364                 (FLG_SYNTAX,
 365                  message ("Lose reference uses unrecognized from value %s: %q",
 366                           tfrom, mtLoseReference_unparse (loseref)),
 367                  mtLoseReference_getLoc (loseref));
 368               continue;
 369             }
 370
 371           /*@-usedef@*/
 372           stateCombinationTable_set
 373             (tsc, fromindex, toindex, vindex,
 374              cstring_copy (mtTransferAction_getMessage (taction)));
 375           /*@=usedef@*/
 376         } end_mtLoseReferenceList_elements ;
 377     }
 378
 379   /*@-usedef@*/
 380   DPRINTF (("metastate: %s", metaStateInfo_unparse (msinfo)));
 381   /*@=usedef@*/
 382
 383   tmerge = stateCombinationTable_create (nvalues);
 384
 385   /* Default merge is to make all incompatible mergers errors. */
 386
 387   for (i = 0; i < nvalues; i++)
 388     {
 389       for (j = 0; j < nvalues; j++)
 390         {
 391           if (i != j)
 392             {
 393               stateCombinationTable_set
 394                 (tmerge, i, j, metaState_error,
 395                  cstring_makeLiteral ("Incompatible state merge (default behavior)"));
 396             }
 397         }
 398     }
 399
 400   mtp = mtDeclarationPieces_findPiece (pieces, MTP_MERGE);
 401
 402   if (mtDeclarationPiece_isDefined (mtp))
 403     {
 404       mtMergeNode mtmerge = mtDeclarationPiece_getMerge (mtp);
 405       mtMergeClauseList mclauses = mtMergeNode_getClauses (mtmerge);
 406
 407       DPRINTF (("Merge node: %s", mtMergeNode_unparse (mtmerge)));
 408
 409       mtMergeClauseList_elements (mclauses, merge)
 410         {
 411           mtMergeItem item1 = mtMergeClause_getItem1 (merge);
 412           mtMergeItem item2 = mtMergeClause_getItem2 (merge);
 413           mtTransferAction taction = mtMergeClause_getAction (merge);
 414           int low1index, high1index;
 415           int low2index, high2index;
 416           int vindex;
 417
 418           DPRINTF (("Merge %s X %s => %s",
 419                     mtMergeItem_unparse (item1),
 420                     mtMergeItem_unparse (item2),
 421                     mtTransferAction_unparse (taction)));
 422
 423           if (!mtMergeItem_isStar (item1))
 424             {
 425               if (cstringList_contains (mvals, mtMergeItem_getValue (item1)))
 426                 {
 427                   low1index = cstringList_getIndex (mvals, mtMergeItem_getValue (item1));
 428                   high1index = low1index;
 429                 }
 430               else
 431                 {
 432                   voptgenerror
 433                     (FLG_SYNTAX,
 434                      message ("Merge clause uses unrecognized first value %s: %q",
 435                               mtMergeItem_getValue (item1),
 436                               mtMergeClause_unparse (merge)),
 437                      mtMergeClause_getLoc (merge));
 438                   continue;
 439                 }
 440             }
 441           else
 442             {
 443               low1index = 0;
 444               high1index = nvalues - 1;
 445             }
 446
 447           if (!mtMergeItem_isStar (item2))
 448             {
 449               if (cstringList_contains (mvals, mtMergeItem_getValue (item2)))
 450                 {
 451                   low2index = cstringList_getIndex (mvals, mtMergeItem_getValue (item2));
 452                   high2index = low2index;
 453                 }
 454               else
 455                 {
 456                   voptgenerror
 457                     (FLG_SYNTAX,
 458                      message ("Merge clause uses unrecognized second value %s: %q",
 459                               mtMergeItem_getValue (item2),
 460                               mtMergeClause_unparse (merge)),
 461                      mtMergeItem_getLoc (item2));
 462                   continue;
 463                 }
 464             }
 465           else
 466             {
 467               low2index = 0;
 468               high2index = nvalues - 1;
 469             }
 470
 471           if (mtTransferAction_isError (taction))
 472             {
 473               vindex = metaState_error;
 474             }
 475           else
 476             {
 477               cstring vname = mtTransferAction_getValue (taction);
 478
 479               if (cstringList_contains (mvals, vname))
 480                 {
 481                   vindex = cstringList_getIndex (mvals, vname);
 482                 }
 483               else
 484                 {
 485                   voptgenerror
 486                     (FLG_SYNTAX,
 487                      message ("Merge clause uses unrecognized result state %s: %q",
 488                               vname, mtMergeClause_unparse (merge)),
 489                      mtTransferAction_getLoc (taction));
 490                   continue;
 491                 }
 492             }
 493
 494           for (i = low1index; i <= high1index; i++)
 495             {
 496               for (j = low2index; j <= high2index; j++)
 497                 {
 498                   /*@i32 check for multiple definitions! */
 499
 500                   if (mtTransferAction_isError (taction))
 501                     {
 502                       stateCombinationTable_update
 503                         (tmerge,
 504                          i, j,
 505                          vindex,
 506                          cstring_copy (mtTransferAction_getMessage (taction)));
 507                     }
 508                   else
 509                     {
 510                       stateCombinationTable_update
 511                         (tmerge,
 512                          i, j,
 513                          vindex,
 514                          cstring_undefined);
 515                     }
 516                 }
 517             }
 518         } end_mtMergeClauseList_elements ;
 519     }
 520
 521   msinfo = metaStateInfo_create (cstring_copy (mtDeclarationNode_getName (node)),
 522                                  cstringList_copy (mvals),
 523                                  mtcontext,
 524                                  /*@-usedef@*/ tsc, /*@=usedef@*/
 525                                  tmerge,
 526                                  fileloc_copy (mtDeclarationNode_getLoc (node)));
 527
 528   mtp = mtDeclarationPieces_findPiece (pieces, MTP_ANNOTATIONS);
 529
 530   if (mtDeclarationPiece_isDefined (mtp))
 531     {
 532       mtAnnotationsNode mtannots = mtDeclarationPiece_getAnnotations (mtp);
 533       mtAnnotationList mtalist = mtAnnotationsNode_getAnnotations (mtannots);
 534
 535       DPRINTF (("Has annotations: %s", mtAnnotationList_unparse (mtalist)));
 536
 537       mtAnnotationList_elements (mtalist, annot)
 538         {
 539           cstring aname = mtAnnotationDecl_getName (annot);
 540           cstring avalue = mtAnnotationDecl_getValue (annot);
 541
 542           DPRINTF (("Process annotation: %s", mtAnnotationDecl_unparse (annot)));
 543
 544           if (cstringList_contains (mvals, avalue))
 545             {
 546               int vindex = cstringList_getIndex (mvals, avalue);
 547               mtContextNode acontext = mtAnnotationDecl_stealContext (annot);
 548
 549               context_addAnnotation
 550                 (annotationInfo_create (cstring_copy (aname), msinfo,
 551                                         acontext, vindex,
 552                                         fileloc_copy (mtAnnotationDecl_getLoc (annot))));
 553             }
 554           else
 555             {
 556               voptgenerror
 557                 (FLG_SYNTAX,
 558                  message ("Annotation declaration uses unrecognized value name %s: %q",
 559                           avalue, mtAnnotationDecl_unparse (annot)),
 560                  mtAnnotationDecl_getLoc (annot));
 561             }
 562
 563         } end_mtAnnotationList_elements ;
 564     }
 565
 566   mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTS);
 567
 568   if (mtDeclarationPiece_isDefined (mtp))
 569     {
 570       mtDefaultsNode mdn = mtDeclarationPiece_getDefaults (mtp);
 571       mtDefaultsDeclList mdecls = mtDefaultsNode_getDecls (mdn);
 572
 573       llassert (!isglobal);
 574
 575       mtDefaultsDeclList_elements (mdecls, mdecl)
 576         {
 577           mtContextNode mcontext = mtDefaultsDecl_getContext (mdecl);
 578           cstring mvalue = mtDefaultsDecl_getValue (mdecl);
 579
 580           if (cstringList_contains (mvals, mvalue))
 581             {
 582               int vindex = cstringList_getIndex (mvals, mvalue);
 583
 584               if (mtContextNode_isRef (mcontext))
 585                 {
 586                   if (metaStateInfo_getDefaultRefValue (msinfo) != stateValue_error)
 587                     {
 588                       voptgenerror
 589                         (FLG_SYNTAX,
 590                          message ("Duplicate defaults declaration for context %q: %q",
 591                                   mtContextNode_unparse (mcontext),
 592                                   mtDefaultsDecl_unparse (mdecl)),
 593                          mtDefaultsDecl_getLoc (mdecl));
 594                     }
 595                   else
 596                     {
 597                       metaStateInfo_setDefaultRefValue (msinfo, vindex);
 598                     }
 599                 }
 600               else if (mtContextNode_isParameter (mcontext))
 601                 {
 602                   if (metaStateInfo_getDefaultParamValue (msinfo) != stateValue_error)
 603                     {
 604                       voptgenerror
 605                         (FLG_SYNTAX,
 606                          message ("Duplicate defaults declaration for context %q: %q",
 607                                   mtContextNode_unparse (mcontext),
 608                                   mtDefaultsDecl_unparse (mdecl)),
 609                          mtDefaultsDecl_getLoc (mdecl));
 610                     }
 611                   else
 612                     {
 613                       metaStateInfo_setDefaultParamValue (msinfo, vindex);
 614                     }
 615                 }
 616               else
 617                 {
 618                   BADBRANCH;
 619                 }
 620             }
 621           else
 622             {
 623               voptgenerror
 624                 (FLG_SYNTAX,
 625                  message ("Defaults declaration uses unrecognized value name %s: %q",
 626                           mvalue, mtDefaultsDecl_unparse (mdecl)),
 627                  mtDefaultsDecl_getLoc (mdecl));
 628             }
 629         } end_mtDefaultsDeclList_elements ;
 630     }
 631
 632   mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTVALUE);
 633
 634   if (mtDeclarationPiece_isDefined (mtp))
 635     {
 636       cstring mvalue = mtDeclarationPiece_getDefaultValue (mtp);
 637       llassert (isglobal);
 638
 639       if (cstringList_contains (mvals, mvalue))
 640         {
 641           int vindex = cstringList_getIndex (mvals, mvalue);
 642
 643           if (metaStateInfo_getDefaultRefValue (msinfo) != stateValue_error)
 644             {
 645               voptgenerror
 646                 (FLG_SYNTAX,
 647                  message ("Duplicate default value declaration for global state: %s",
 648                           mvalue),
 649                  mtDeclarationNode_getLoc (node));
 650             }
 651           else
 652             {
 653               metaStateInfo_setDefaultRefValue (msinfo, vindex);
 654             }
 655         }
 656       else
 657         {
 658           voptgenerror
 659             (FLG_SYNTAX,
 660              message ("Default value declaration uses unrecognized value name: %s",
 661                       mvalue),
 662              mtDeclarationNode_getLoc (node));
 663         }
 664     }
 665
 666   context_addMetaState (cstring_copy (mtDeclarationNode_getName (node)),
 667                         msinfo);
 668 }
 669
 670 extern void mtDeclarationNode_free (/*@only@*/ mtDeclarationNode node)
 671 {
 672   mtDeclarationPieces_free (node->pieces);
 673   cstring_free (node->name);
 674   fileloc_free (node->loc);
 675   sfree (node);
 676 }
 677
 678 extern fileloc mtDeclarationNode_getLoc (mtDeclarationNode node)
 679 {
 680   return node->loc;
 681 }
 682
 683 extern /*@observer@*/ cstring mtDeclarationNode_getName (mtDeclarationNode node)
 684 {
 685   return node->name;
 686 }