2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
25 ** mtDeclarationNode.c
28 # include "splintMacros.nf"
31 extern mtDeclarationNode mtDeclarationNode_create (mttok name, mtDeclarationPieces pieces) /*@*/
33 mtDeclarationNode res = (mtDeclarationNode) dmalloc (sizeof (*res));
35 res->name = mttok_getText (name);
36 res->loc = mttok_stealLoc (name);
43 extern cstring mtDeclarationNode_unparse (mtDeclarationNode node) /*@*/
45 return message ("state %s %q",
47 mtDeclarationPieces_unparse (node->pieces));
50 extern void mtDeclarationNode_process (mtDeclarationNode node, bool isglobal)
55 mtDeclarationPieces pieces;
56 mtDeclarationPiece mtp;
57 mtContextNode mtcontext;
58 stateCombinationTable tsc;
59 stateCombinationTable tmerge;
64 cstring defaultMergeMessage =
65 cstring_makeLiteralTemp ("Incompatible state merge (default behavior)");
67 pieces = node->pieces;
70 ** First, we need to find the values piece.
73 mtp = mtDeclarationPieces_findPiece (pieces, MTP_VALUES);
75 if (mtDeclarationPiece_isUndefined (mtp))
77 voptgenerror (FLG_SYNTAX,
78 message ("Metastate declaration missing values clause: %s",
79 mtDeclarationNode_getName (node)),
80 mtDeclarationNode_getLoc (node));
85 mtValuesNode mtv = mtDeclarationPiece_getValues (mtp);
86 mvals = mtValuesNode_getValues (mtv);
89 /*@-usedef@*/ /*@i34 splint should figure this out... */
90 nvalues = cstringList_size (mvals);
93 mtp = mtDeclarationPieces_findPiece (pieces, MTP_CONTEXT);
95 if (mtDeclarationPiece_isUndefined (mtp))
97 ; /* No context, assume anywhere is okay. */
98 mtcontext = mtContextNode_createAny ();
102 mtcontext = mtDeclarationPiece_stealContext (mtp);
108 ** For global state, instead of a transfers piece, we have constraints.
111 mtp = mtDeclarationPieces_findPiece (pieces, MTP_TRANSFERS);
113 if (!mtDeclarationPiece_isUndefined (mtp))
115 voptgenerror (FLG_SYNTAX,
116 message ("Global state declaration uses transfers clause. Should use preconditions and postconsitions clauses instead: %s",
117 mtDeclarationNode_getName (node)),
118 mtDeclarationNode_getLoc (node));
119 mtContextNode_free (mtcontext);
123 mtp = mtDeclarationPieces_findPiece (pieces, MTP_PRECONDITIONS);
125 if (mtDeclarationPiece_isUndefined (mtp))
127 voptgenerror (FLG_SYNTAX,
128 message ("Metastate declaration missing preconditions clause: %s",
129 mtDeclarationNode_getName (node)),
130 mtDeclarationNode_getLoc (node));
131 mtContextNode_free (mtcontext);
136 mtTransferClauseList mtransfers = mtDeclarationPiece_getPreconditions (mtp);
137 tsc = stateCombinationTable_create (nvalues);
139 mtTransferClauseList_elements (mtransfers, transfer)
141 cstring tfrom = mtTransferClause_getFrom (transfer);
142 cstring tto = mtTransferClause_getTo (transfer);
143 mtTransferAction taction = mtTransferClause_getAction (transfer);
144 cstring vname = mtTransferAction_getValue (taction);
150 DPRINTF (("Transfer: %s", mtTransferClause_unparse (transfer)));
152 if (cstringList_contains (mvals, tfrom))
154 fromindex = cstringList_getIndex (mvals, tfrom);
160 message ("Precondition clause uses unrecognized caller value %s: %q",
161 tfrom, mtTransferClause_unparse (transfer)),
162 mtTransferClause_getLoc (transfer));
166 if (cstringList_contains (mvals, tto))
168 toindex = cstringList_getIndex (mvals, tto);
174 message ("Precondition clause uses unrecognized constraint value %s: %q",
175 tto, mtTransferClause_unparse (transfer)),
176 mtTransferClause_getLoc (transfer));
180 if (mtTransferAction_isError (taction))
182 vindex = metaState_error;
186 if (cstringList_contains (mvals, vname))
188 vindex = cstringList_getIndex (mvals, vname);
194 message ("Precondition clause uses unrecognized result state %s: %q",
195 vname, mtTransferClause_unparse (transfer)),
196 mtTransferClause_getLoc (transfer));
201 if (mtTransferAction_isError (taction))
203 stateCombinationTable_set
204 (tsc, fromindex, toindex,
206 cstring_copy (mtTransferAction_getMessage (taction)));
210 stateCombinationTable_set (tsc, fromindex, toindex,
214 } end_mtTransferClauseList_elements ;
219 mtp = mtDeclarationPieces_findPiece (pieces, MTP_PRECONDITIONS);
221 if (!mtDeclarationPiece_isUndefined (mtp))
225 message ("Non-global state declaration uses preconditions clause. "
226 "Should use transfers clause instead: %s",
227 mtDeclarationNode_getName (node)),
228 mtDeclarationNode_getLoc (node));
229 mtContextNode_free (mtcontext);
233 mtp = mtDeclarationPieces_findPiece (pieces, MTP_POSTCONDITIONS);
235 if (!mtDeclarationPiece_isUndefined (mtp))
239 message ("Non-global state declaration uses postconditions clause. "
240 "Should use transfers clause instead: %s",
241 mtDeclarationNode_getName (node)),
242 mtDeclarationNode_getLoc (node));
243 mtContextNode_free (mtcontext);
247 mtp = mtDeclarationPieces_findPiece (pieces, MTP_TRANSFERS);
249 if (mtDeclarationPiece_isUndefined (mtp))
251 voptgenerror (FLG_SYNTAX,
252 message ("Metastate declaration missing transfers clause: %s",
253 mtDeclarationNode_getName (node)),
254 mtDeclarationNode_getLoc (node));
255 mtContextNode_free (mtcontext);
260 mtTransferClauseList mtransfers = mtDeclarationPiece_getTransfers (mtp);
261 tsc = stateCombinationTable_create (nvalues);
263 mtTransferClauseList_elements (mtransfers, transfer)
265 cstring tfrom = mtTransferClause_getFrom (transfer);
266 cstring tto = mtTransferClause_getTo (transfer);
267 mtTransferAction taction = mtTransferClause_getAction (transfer);
268 cstring vname = mtTransferAction_getValue (taction);
274 DPRINTF (("Transfer: %s", mtTransferClause_unparse (transfer)));
276 if (cstringList_contains (mvals, tfrom))
278 fromindex = cstringList_getIndex (mvals, tfrom);
284 message ("Transfer clause uses unrecognized from value %s: %q",
285 tfrom, mtTransferClause_unparse (transfer)),
286 mtTransferClause_getLoc (transfer));
290 if (cstringList_contains (mvals, tto))
292 toindex = cstringList_getIndex (mvals, tto);
298 message ("Transfer clause uses unrecognized to value %s: %q",
299 tto, mtTransferClause_unparse (transfer)),
300 mtTransferClause_getLoc (transfer));
304 if (mtTransferAction_isError (taction))
306 vindex = metaState_error;
310 if (cstringList_contains (mvals, vname))
312 vindex = cstringList_getIndex (mvals, vname);
318 message ("Transfer clause uses unrecognized result state %s: %q",
319 vname, mtTransferClause_unparse (transfer)),
320 mtTransferClause_getLoc (transfer));
325 if (mtTransferAction_isError (taction))
327 stateCombinationTable_set
328 (tsc, fromindex, toindex,
330 cstring_copy (mtTransferAction_getMessage (taction)));
334 stateCombinationTable_set (tsc, fromindex, toindex,
338 } end_mtTransferClauseList_elements ;
342 mtp = mtDeclarationPieces_findPiece (pieces, MTP_LOSERS);
344 if (mtDeclarationPiece_isDefined (mtp))
346 mtLoseReferenceList mlosers = mtDeclarationPiece_getLosers (mtp);
348 mtLoseReferenceList_elements (mlosers, loseref)
350 cstring tfrom = mtLoseReference_getFrom (loseref);
351 mtTransferAction taction = mtLoseReference_getAction (loseref);
353 /* Losing reference is represented by transfer to nvalues */
354 int toindex = nvalues;
355 int vindex = metaState_error;
357 llassert (mtTransferAction_isError (taction));
359 if (cstringList_contains (mvals, tfrom))
361 fromindex = cstringList_getIndex (mvals, tfrom);
367 message ("Lose reference uses unrecognized from value %s: %q",
368 tfrom, mtLoseReference_unparse (loseref)),
369 mtLoseReference_getLoc (loseref));
374 stateCombinationTable_set
375 (tsc, fromindex, toindex, vindex,
376 cstring_copy (mtTransferAction_getMessage (taction)));
378 } end_mtLoseReferenceList_elements ;
381 tmerge = stateCombinationTable_create (nvalues);
383 /* Default merge is to make all incompatible mergers errors. */
385 for (i = 0; i < nvalues; i++)
387 for (j = 0; j < nvalues; j++)
391 stateCombinationTable_set
392 (tmerge, i, j, metaState_error, cstring_copy (defaultMergeMessage));
397 mtp = mtDeclarationPieces_findPiece (pieces, MTP_MERGE);
399 if (mtDeclarationPiece_isDefined (mtp))
401 mtMergeNode mtmerge = mtDeclarationPiece_getMerge (mtp);
402 mtMergeClauseList mclauses = mtMergeNode_getClauses (mtmerge);
404 DPRINTF (("Merge node: %s", mtMergeNode_unparse (mtmerge)));
406 mtMergeClauseList_elements (mclauses, merge)
408 mtMergeItem item1 = mtMergeClause_getItem1 (merge);
409 mtMergeItem item2 = mtMergeClause_getItem2 (merge);
410 mtTransferAction taction = mtMergeClause_getAction (merge);
411 int low1index, high1index;
412 int low2index, high2index;
415 DPRINTF (("Merge %s X %s => %s",
416 mtMergeItem_unparse (item1),
417 mtMergeItem_unparse (item2),
418 mtTransferAction_unparse (taction)));
420 if (!mtMergeItem_isStar (item1))
422 if (cstringList_contains (mvals, mtMergeItem_getValue (item1)))
424 low1index = cstringList_getIndex (mvals, mtMergeItem_getValue (item1));
425 high1index = low1index;
431 message ("Merge clause uses unrecognized first value %s: %q",
432 mtMergeItem_getValue (item1),
433 mtMergeClause_unparse (merge)),
434 mtMergeClause_getLoc (merge));
441 high1index = nvalues - 1;
444 if (!mtMergeItem_isStar (item2))
446 if (cstringList_contains (mvals, mtMergeItem_getValue (item2)))
448 low2index = cstringList_getIndex (mvals, mtMergeItem_getValue (item2));
449 high2index = low2index;
455 message ("Merge clause uses unrecognized second value %s: %q",
456 mtMergeItem_getValue (item2),
457 mtMergeClause_unparse (merge)),
458 mtMergeItem_getLoc (item2));
465 high2index = nvalues - 1;
468 if (mtTransferAction_isError (taction))
470 vindex = metaState_error;
474 cstring vname = mtTransferAction_getValue (taction);
476 if (cstringList_contains (mvals, vname))
478 vindex = cstringList_getIndex (mvals, vname);
484 message ("Merge clause uses unrecognized result state %s: %q",
485 vname, mtMergeClause_unparse (merge)),
486 mtTransferAction_getLoc (taction));
491 for (i = low1index; i <= high1index; i++)
493 for (j = low2index; j <= high2index; j++)
495 /*@i32 check for multiple definitions! */
497 if (mtTransferAction_isError (taction))
499 stateCombinationTable_update
503 cstring_copy (mtTransferAction_getMessage (taction)));
507 stateCombinationTable_update
517 ** Unless otherwise indicated, merging is symmetric:
520 for (i = low1index; i <= high1index; i++)
522 for (j = low2index; j <= high2index; j++)
526 if (stateCombinationTable_lookup (tmerge, j, i, &msg) == metaState_error)
528 if (cstring_equal (msg, defaultMergeMessage))
530 /* Override the default action */
531 if (mtTransferAction_isError (taction))
533 stateCombinationTable_update
537 cstring_copy (mtTransferAction_getMessage (taction)));
541 stateCombinationTable_update
551 } end_mtMergeClauseList_elements ;
554 msinfo = metaStateInfo_create (cstring_copy (mtDeclarationNode_getName (node)),
555 cstringList_copy (mvals),
557 /*@-usedef@*/ tsc, /*@=usedef@*/
559 fileloc_copy (mtDeclarationNode_getLoc (node)));
561 mtp = mtDeclarationPieces_findPiece (pieces, MTP_ANNOTATIONS);
563 if (mtDeclarationPiece_isDefined (mtp))
565 mtAnnotationsNode mtannots = mtDeclarationPiece_getAnnotations (mtp);
566 mtAnnotationList mtalist = mtAnnotationsNode_getAnnotations (mtannots);
568 DPRINTF (("Has annotations: %s", mtAnnotationList_unparse (mtalist)));
570 mtAnnotationList_elements (mtalist, annot)
572 cstring aname = mtAnnotationDecl_getName (annot);
573 cstring avalue = mtAnnotationDecl_getValue (annot);
575 DPRINTF (("Process annotation: %s", mtAnnotationDecl_unparse (annot)));
577 if (cstringList_contains (mvals, avalue))
579 int vindex = cstringList_getIndex (mvals, avalue);
580 mtContextNode acontext = mtAnnotationDecl_stealContext (annot);
582 context_addAnnotation
583 (annotationInfo_create (cstring_copy (aname), msinfo,
585 fileloc_copy (mtAnnotationDecl_getLoc (annot))));
591 message ("Annotation declaration uses unrecognized value name %s: %q",
592 avalue, mtAnnotationDecl_unparse (annot)),
593 mtAnnotationDecl_getLoc (annot));
596 } end_mtAnnotationList_elements ;
599 mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTS);
601 if (mtDeclarationPiece_isDefined (mtp))
603 mtDefaultsNode mdn = mtDeclarationPiece_getDefaults (mtp);
604 mtDefaultsDeclList mdecls = mtDefaultsNode_getDecls (mdn);
606 llassert (!isglobal);
608 mtDefaultsDeclList_elements (mdecls, mdecl)
610 mtContextNode mcontext = mtDefaultsDecl_getContext (mdecl);
611 cstring mvalue = mtDefaultsDecl_getValue (mdecl);
613 if (cstringList_contains (mvals, mvalue))
615 int vindex = cstringList_getIndex (mvals, mvalue);
618 if (mtContextNode_isReference (mcontext))
620 mkind = MTC_REFERENCE;
622 else if (mtContextNode_isParameter (mcontext))
626 else if (mtContextNode_isResult (mcontext))
630 else if (mtContextNode_isLiteral (mcontext))
634 else if (mtContextNode_isNull (mcontext))
640 DPRINTF (("Bad: %s", mtContextNode_unparse (mcontext)));
644 if (metaStateInfo_getDefaultValueContext (msinfo, mkind) != stateValue_error)
648 message ("Duplicate defaults declaration for context %q: %q",
649 mtContextNode_unparse (mcontext),
650 mtDefaultsDecl_unparse (mdecl)),
651 mtDefaultsDecl_getLoc (mdecl));
655 metaStateInfo_setDefaultValueContext (msinfo, mkind, vindex);
662 message ("Defaults declaration uses unrecognized value name %s: %q",
663 mvalue, mtDefaultsDecl_unparse (mdecl)),
664 mtDefaultsDecl_getLoc (mdecl));
666 } end_mtDefaultsDeclList_elements ;
669 mtp = mtDeclarationPieces_findPiece (pieces, MTP_DEFAULTVALUE);
671 if (mtDeclarationPiece_isDefined (mtp))
673 cstring mvalue = mtDeclarationPiece_getDefaultValue (mtp);
676 if (cstringList_contains (mvals, mvalue))
678 int vindex = cstringList_getIndex (mvals, mvalue);
680 if (metaStateInfo_getDefaultRefValue (msinfo) != stateValue_error)
684 message ("Duplicate default value declaration for global state: %s",
686 mtDeclarationNode_getLoc (node));
690 metaStateInfo_setDefaultRefValue (msinfo, vindex);
697 message ("Default value declaration uses unrecognized value name: %s",
699 mtDeclarationNode_getLoc (node));
703 context_addMetaState (cstring_copy (mtDeclarationNode_getName (node)),
707 extern void mtDeclarationNode_free (/*@only@*/ mtDeclarationNode node)
709 mtDeclarationPieces_free (node->pieces);
710 cstring_free (node->name);
711 fileloc_free (node->loc);
715 extern fileloc mtDeclarationNode_getLoc (mtDeclarationNode node)
720 extern /*@observer@*/ cstring mtDeclarationNode_getName (mtDeclarationNode node)