5 /* #define DEBUGPRINT 1 */
7 # include <ctype.h> /* for isdigit */
8 # include "lclintMacros.nf"
10 # include "cgrammar.h"
11 # include "cgrammar_tokens.h"
13 # include "exprChecks.h"
14 # include "exprNodeSList.h"
18 /*@access exprNode @*/
21 static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
24 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
25 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
26 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
29 advanceField (char **s)
31 reader_checkChar (s, '@');
35 static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
40 ret = constraint_makeNew ();
41 llassert (constraintExpr_isDefined(l) );
43 ret->lexpr = constraintExpr_copy (l);
46 if (relOp.tok == GE_OP)
48 else if (relOp.tok == LE_OP)
50 else if (relOp.tok == EQ_OP)
53 llfatalbug(message("Unsupported relational operator") );
56 t = cstring_toCharsSafe (exprNode_unparse(cconstant));
58 ret->expr = constraintExpr_makeIntLiteral (c);
61 DPRINTF(("GENERATED CONSTRAINT:"));
62 DPRINTF( (message ("%s", constraint_print(ret) ) ) );
67 bool constraint_same (constraint c1, constraint c2)
69 llassert (c1 != NULL);
70 llassert (c2 != NULL);
77 if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
82 if (!constraintExpr_similar (c1->expr, c2->expr) )
90 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
93 ret = constraint_makeNew();
94 llassert (constraintExpr_isDefined(l) );
96 ret->lexpr = constraintExpr_copy (l);
98 if (relOp.tok == GE_OP)
100 else if (relOp.tok == LE_OP)
102 else if (relOp.tok == EQ_OP)
105 llfatalbug( message("Unsupported relational operator") );
107 ret->expr = constraintExpr_copy (r);
111 ret->orig = constraint_copy(ret);
113 ret = constraint_simplify (ret);
114 /* ret->orig = ret; */
116 DPRINTF(("GENERATED CONSTRAINT:"));
117 DPRINTF( (message ("%s", constraint_print(ret) ) ) );
121 constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
125 llassert (constraint_isDefined(c) );
127 ret = constraint_makeNew();
128 ret->lexpr = constraintExpr_copy (c->lexpr);
130 ret->expr = constraintExpr_copy (c->expr);
133 ret->generatingExpr = c->generatingExpr;
138 ret->orig = constraint_copy (c->orig);
143 ret->or = constraint_copy (c->or);
147 ret->fcnPre = c->fcnPre;
152 /*like copy expect it doesn't allocate memory for the constraint*/
154 void constraint_overWrite (constraint c1, constraint c2)
156 llassert (constraint_isDefined(c1) );
160 DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1),
161 constraint_print(c2) ) ));
163 constraintExpr_free(c1->lexpr);
164 constraintExpr_free(c1->expr);
166 c1->lexpr = constraintExpr_copy (c2->lexpr);
168 c1->expr = constraintExpr_copy (c2->expr);
171 if (c1->orig != NULL)
172 constraint_free (c1->orig);
174 if (c2->orig != NULL)
175 c1->orig = constraint_copy (c2->orig);
179 /*@i33 make sure that the or is freed correctly*/
181 constraint_free (c1->or);
184 c1->or = constraint_copy (c2->or);
188 c1->fcnPre = c2->fcnPre;
191 c1->generatingExpr = c2->generatingExpr;
197 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
198 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/
199 /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
202 ret = dmalloc(sizeof (*ret) );
209 ret->generatingExpr = NULL;
214 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
217 if (c->generatingExpr == NULL)
219 c->generatingExpr = e;
220 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
224 DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
229 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
232 if (c->orig != constraint_undefined)
234 c->orig = constraint_addGeneratingExpr(c->orig, e);
238 DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
243 constraint constraint_setFcnPre (/*@returned@*/ constraint c )
246 if (c->orig != constraint_undefined)
248 c->orig->fcnPre = TRUE;
253 DPRINTF(( message("Warning Setting fcnPre directly") ));
261 fileloc constraint_getFileloc (constraint c)
263 if (exprNode_isDefined(c->generatingExpr) )
264 return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) );
266 return (constraintExpr_getFileloc (c->lexpr) );
271 static bool checkForMaxSet (constraint c)
273 if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
279 bool constraint_hasMaxSet(constraint c)
281 if (checkForMaxSet(c) )
286 if (checkForMaxSet(c->orig) )
293 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
295 constraint ret = constraint_makeNew();
299 ret->lexpr = constraintExpr_makeMaxReadExpr(po);
301 ret->expr = constraintExpr_makeValueExpr (ind);
306 constraint constraint_makeWriteSafeInt ( exprNode po, int ind)
308 constraint ret = constraint_makeNew();
311 ret->lexpr =constraintExpr_makeMaxSetExpr(po);
313 ret->expr = constraintExpr_makeIntLiteral (ind);
317 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
319 constraint ret = constraint_makeNew();
320 ret->lexpr = constraintExpr_makeSRefMaxset (s);
322 ret->expr = constraintExpr_makeIntLiteral ((int)size);
327 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
329 constraint ret = constraint_makeNew();
332 ret->lexpr = constraintExpr_makeSRefMaxset ( s );
334 ret->expr = constraintExpr_makeIntLiteral (ind);
339 /* drl added 01/12/2000
341 makes the constraint: Ensures index <= MaxRead(buffer) */
343 constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
345 constraint ret = constraint_makeNew();
347 ret->lexpr = constraintExpr_makeValueExpr (index);
349 ret->expr = constraintExpr_makeMaxReadExpr(buffer);
354 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
356 constraint ret = constraint_makeNew();
359 ret->lexpr =constraintExpr_makeMaxSetExpr(po);
361 ret->expr = constraintExpr_makeValueExpr (ind);
366 constraint constraint_makeReadSafeInt ( exprNode t1, int index)
368 constraint ret = constraint_makeNew();
370 ret->lexpr = constraintExpr_makeMaxReadExpr(t1);
372 ret->expr = constraintExpr_makeIntLiteral (index);
377 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
379 constraint ret = constraint_makeNew();
382 ret->lexpr = constraintExpr_makeSRefMaxRead (s );
384 ret->expr = constraintExpr_makeIntLiteral (ind);
389 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
393 ret = constraint_makeReadSafeExprNode(t1, t2);
394 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
400 static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar)
405 llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) );
407 ret = constraint_makeNew();
413 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
417 static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint, arithType ar)
419 constraintExpr c1, c2;
423 if (! (exprNode_isDefined(e1) && exprNode_isDefined(e2) ) )
425 llcontbug((message("null exprNode, Exprnodes are %s and %s",
426 exprNode_unparse(e1), exprNode_unparse(e2) )
431 c1 = constraintExpr_makeValueExpr (e);
434 c2 = constraintExpr_makeValueExpr (e);
436 ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
442 /* make constraint ensures e1 == e2 */
444 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
446 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
449 /*make constraint ensures e1 < e2 */
450 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
452 constraintExpr t1, t2;
454 t1 = constraintExpr_makeValueExpr (e1);
455 t2 = constraintExpr_makeValueExpr (e2);
457 /*change this to e1 <= (e2 -1) */
459 t2 = constraintExpr_makeDecConstraintExpr (t2);
461 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
464 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
466 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
469 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
471 constraintExpr t1, t2;
473 t1 = constraintExpr_makeValueExpr (e1);
474 t2 = constraintExpr_makeValueExpr (e2);
477 /* change this to e1 >= (e2 + 1) */
478 t2 = constraintExpr_makeIncConstraintExpr (t2);
481 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
484 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
486 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
490 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
492 constraintList_free(dst->ensuresConstraints);
493 constraintList_free(dst->requiresConstraints);
494 constraintList_free(dst->trueEnsuresConstraints);
495 constraintList_free(dst->falseEnsuresConstraints);
497 dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
498 dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
499 dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
500 dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
504 /* Makes the constraint e = e + f */
505 constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
507 constraintExpr x1, x2, y;
510 ret = constraint_makeNew();
512 x1 = constraintExpr_makeValueExpr (e);
513 x2 = constraintExpr_copy(x1);
514 y = constraintExpr_makeValueExpr (f);
519 ret->expr = constraintExpr_makeAddExpr (x2, y);
521 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
527 /* Makes the constraint e = e - f */
528 constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
530 constraintExpr x1, x2, y;
533 ret = constraint_makeNew();
535 x1 = constraintExpr_makeValueExpr (e);
536 x2 = constraintExpr_copy(x1);
537 y = constraintExpr_makeValueExpr (f);
542 ret->expr = constraintExpr_makeSubtractExpr (x2, y);
544 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
549 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
551 constraint ret = constraint_makeNew();
553 ret->lexpr = constraintExpr_makeValueExpr (e);
556 ret->expr = constraintExpr_makeValueExpr (e);
557 ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
558 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
561 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
563 constraint ret = constraint_makeNew();
565 ret->lexpr = constraintExpr_makeValueExpr (e);
568 ret->expr = constraintExpr_makeValueExpr (e);
569 ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
571 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
576 void constraint_free (/*@only@*/ constraint c)
578 llassert(constraint_isDefined (c) );
581 if (constraint_isDefined(c->orig) )
582 constraint_free (c->orig);
583 if ( constraint_isDefined(c->or) )
584 constraint_free (c->or);
587 constraintExpr_free(c->lexpr);
588 constraintExpr_free(c->expr);
599 cstring arithType_print (arithType ar) /*@*/
601 cstring st = cstring_undefined;
605 st = cstring_makeLiteral ("<");
608 st = cstring_makeLiteral ("<=");
611 st = cstring_makeLiteral (">");
614 st = cstring_makeLiteral (">=");
617 st = cstring_makeLiteral ("==");
620 st = cstring_makeLiteral ("NONNEGATIVE");
623 st = cstring_makeLiteral ("POSITIVE");
632 void constraint_printErrorPostCondition (constraint c, fileloc loc)
635 fileloc errorLoc, temp;
637 string = constraint_printDetailedPostCondition (c);
643 temp = constraint_getFileloc(c);
645 if (fileloc_isDefined(temp) )
648 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
653 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
657 /*drl added 8-11-001*/
658 cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
663 string = constraint_print(c);
665 errorLoc = constraint_getFileloc(c);
667 ret = message ("constraint: %q @ %q", string, fileloc_unparse(errorLoc) );
669 fileloc_free(errorLoc);
676 void constraint_printError (constraint c, fileloc loc)
679 fileloc errorLoc, temp;
681 string = constraint_printDetailed (c);
685 temp = constraint_getFileloc(c);
687 if (fileloc_isDefined(temp) )
694 DPRINTF (("constraint %s had undefined fileloc %s", constraint_print(c), fileloc_unparse(temp)));
696 errorLoc = fileloc_copy(errorLoc);
701 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
705 if (constraint_hasMaxSet (c) )
706 voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
708 voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
711 fileloc_free(errorLoc);
716 static cstring constraint_printDeep (constraint c)
719 cstring st = cstring_undefined;
721 st = constraint_print(c);
724 if (c->orig != constraint_undefined)
726 st = cstring_appendChar(st, '\n');
727 genExpr = exprNode_unparse(c->orig->generatingExpr);
731 st = cstring_concatFree(st, (message(" derived from %s precondition: %q", genExpr, constraint_printDeep(c->orig) )
734 st = cstring_concatFree(st,(message(" needed to satisfy precondition:\n%q",
735 constraint_printDeep(c->orig) )
741 st = cstring_concatFree(st,(message("derived from: %q",
742 constraint_printDeep(c->orig) )
752 static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
754 cstring st = cstring_undefined;
757 st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
759 genExpr = exprNode_unparse (c->generatingExpr);
761 if (context_getFlag (FLG_CONSTRAINTLOCATION) )
765 temp = message ("\nOriginal Generating expression %q: %s\n",
766 fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
768 st = cstring_concatFree (st, temp);
770 if (constraint_hasMaxSet(c) )
772 temp = message ("Has MaxSet\n");
773 st = cstring_concatFree (st, temp);
779 cstring constraint_printDetailed (constraint c)
781 cstring st = cstring_undefined;
782 cstring temp = cstring_undefined;
787 st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c) );
791 st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
794 if (constraint_hasMaxSet(c) )
796 temp = cstring_makeLiteral("Possible out-of-bounds store:\n");
800 temp = cstring_makeLiteral("Possible out-of-bounds read:\n");
803 genExpr = exprNode_unparse (c->generatingExpr);
805 if (context_getFlag (FLG_CONSTRAINTLOCATION) )
808 temp2 = message ("%s\n", genExpr );
809 temp = cstring_concatFree (temp, temp2);
812 st = cstring_concatFree(temp,st);
817 /*@only@*/ cstring constraint_print (constraint c) /*@*/
819 cstring st = cstring_undefined;
820 cstring type = cstring_undefined;
824 if (context_getFlag (FLG_PARENCONSTRAINT) )
826 type = cstring_makeLiteral ("ensures: ");
830 type = cstring_makeLiteral ("ensures");
835 if (context_getFlag (FLG_PARENCONSTRAINT) )
837 type = cstring_makeLiteral ("requires: ");
841 type = cstring_makeLiteral ("requires");
845 if (context_getFlag (FLG_PARENCONSTRAINT) )
847 st = message ("%q: %q %q %q",
849 constraintExpr_print (c->lexpr),
850 arithType_print(c->ar),
851 constraintExpr_print(c->expr)
856 st = message ("%q %q %q %q",
858 constraintExpr_print (c->lexpr),
859 arithType_print(c->ar),
860 constraintExpr_print(c->expr)
866 cstring constraint_printOr (constraint c) /*@*/
871 ret = cstring_undefined;
874 ret = cstring_concatFree (ret, constraint_print(temp) );
878 while ( constraint_isDefined(temp) )
880 ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
881 ret = cstring_concatFree (ret, constraint_print(temp) );
889 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
890 exprNodeList arglist)
892 precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
894 precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
901 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
903 postcondition = constraint_copy (postcondition);
904 postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
905 postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
907 return postcondition;
910 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
911 exprNodeList arglist)
914 precondition = constraint_copy (precondition);
915 precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
916 precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
918 precondition->fcnPre = FALSE;
922 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
925 DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
927 if (c->orig == constraint_undefined)
928 c->orig = constraint_copy (c);
930 else if (c->orig->fcnPre)
936 /* avoid infinite loop */
938 c->orig = constraint_copy (c);
939 if (c->orig->orig == NULL)
941 c->orig->orig = temp;
946 llcontbug((message("Expected c->orig->orig to be null" ) ));
947 constraint_free(c->orig->orig);
948 c->orig->orig = temp;
954 DPRINTF( (message("Not changing constraint") ));
957 DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
966 constraint constraint_togglePost (/*@returned@*/ constraint c)
972 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
975 c->orig = constraint_togglePost(c->orig);
979 bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
988 constraint constraint_undump (FILE *f)
995 constraintExpr lexpr;
1003 s = mstring_create (MAX_DUMP_LINE_LENGTH);
1007 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1009 /*@i33*/ /*this should probably be wrappered...*/
1011 fcnPre = (bool) reader_getInt (&s);
1013 post = (bool) reader_getInt (&s);
1015 ar = (arithType) reader_getInt (&s);
1017 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1019 reader_checkChar (&s, 'l');
1021 lexpr = constraintExpr_undump (f);
1023 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1025 reader_checkChar (&s, 'r');
1026 expr = constraintExpr_undump (f);
1028 c = constraint_makeNew();
1038 c = constraint_preserveOrig(c);
1043 void constraint_dump (/*@observer@*/ constraint c, FILE *f)
1049 constraintExpr lexpr;
1050 constraintExpr expr;
1059 fprintf(f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1061 constraintExpr_dump (lexpr, f);
1063 constraintExpr_dump (expr, f);
1067 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
1073 llassert(constraint_isDefined(*c1) );
1074 llassert(constraint_isDefined(*c2) );
1076 if (constraint_isUndefined(*c1) )
1078 if (constraint_isUndefined(*c2) )
1084 if (constraint_isUndefined(*c2) )
1089 loc1 = constraint_getFileloc(*c1);
1090 loc2 = constraint_getFileloc(*c2);
1092 ret = fileloc_compare(loc1, loc2);
1101 bool constraint_isPost (/*@observer@*/ /*@temp@*/ constraint c)
1103 llassert(constraint_isDefined(c) );
1105 if (constraint_isUndefined(c) )
1112 static int constraint_getDepth(/*@observer@*/ /*@temp@*/ constraint c)
1116 l = constraintExpr_getDepth(c->lexpr);
1117 r = constraintExpr_getDepth(c->expr);
1121 DPRINTF(( message("constraint depth returning %d for %s", l, constraint_print(c) ) ));
1126 DPRINTF(( message("constraint depth returning %d for %s", r, constraint_print(c) ) ));
1132 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
1136 temp = constraint_getDepth(c);