2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 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: splint@cs.virginia.edu
21 ** To report a bug: splint-bug@cs.virginia.edu
22 ** For more information: http://www.splint.org
29 /* #define DEBUGPRINT 1 */
31 # include "splintMacros.nf"
33 # include "cgrammar.h"
34 # include "cgrammar_tokens.h"
36 # include "exprChecks.h"
37 # include "exprNodeSList.h"
43 /*@access exprNode constraintExpr@*/
46 static /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/constraintExpr p_expr, int p_literal);
49 /*@only@*/ static constraintExpr
50 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr p_e, /*@temp@*/ /*@observer@*/ exprNodeList p_arglist) /*@modifies p_e@*/;
52 static /*@only@*/ constraintExpr
53 doFixResultTerm (/*@only@*/ constraintExpr p_e, /*@exposed@*/ exprNode p_fcnCall)
57 /*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
58 /* @allocates result->data @ @sets result->kind @ */ ;
60 void constraintExpr_free (/*@only@*/ constraintExpr expr)
62 if (constraintExpr_isDefined(expr) )
67 constraintExprData_freeUnaryExpr(expr->data);
70 constraintExprData_freeBinaryExpr(expr->data);
73 constraintExprData_freeTerm(expr->data);
84 llcontbug(message("attempted to free null pointer in constraintExpr_free"));
88 bool constraintExpr_isLit (constraintExpr expr)
90 llassert (expr != NULL);
92 if (expr->kind == term)
94 constraintTerm term = constraintExprData_termGetTerm (expr->data);
95 if (constraintTerm_isIntLiteral (term) )
104 static bool isZeroBinaryOp (constraintExpr expr)
108 llassert (expr != NULL); /* evans 2001-07-18 */
110 if (!constraintExpr_isBinaryExpr (expr) )
116 e2 = constraintExprData_binaryExprGetExpr2(expr->data);
118 llassert (e2 != NULL); /* evans 2001-07-18 */
120 if (constraintExpr_isBinaryExpr (e2) )
123 constraintExprBinaryOpKind op;
125 op = constraintExprData_binaryExprGetOp (e2->data);
127 e1 = constraintExprData_binaryExprGetExpr1(e2->data);
129 if (constraintExpr_isLit(e1) )
131 if (constraintExpr_getValue(e1) == 0 )
140 /* change expr + (o - expr) to (expr -expr) */
142 /*@only@*/ static constraintExpr removeZero (/*@only@*/ /*@returned@*/ constraintExpr expr)
144 constraintExpr expr1, expr2;
148 constraintExprBinaryOpKind op;
150 constraintExprBinaryOpKind tempOp;
152 if (!isZeroBinaryOp(expr) )
155 llassert (expr != NULL); /* evans 2001-07-18 */
157 expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
158 expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
159 op = constraintExprData_binaryExprGetOp(expr->data);
161 llassert( constraintExpr_isBinaryExpr(expr2) );
163 temp = constraintExprData_binaryExprGetExpr2 (expr2->data);
164 temp = constraintExpr_copy (temp);
166 tempOp = constraintExprData_binaryExprGetOp (expr2->data);
168 if (op == BINARYOP_PLUS)
170 else if (op == BINARYOP_MINUS)
172 if (tempOp == BINARYOP_PLUS)
174 else if (tempOp == BINARYOP_MINUS)
182 expr->data = constraintExprData_binaryExprSetExpr2(expr->data, temp);
183 expr->data = constraintExprData_binaryExprSetOp(expr->data, op);
189 /*@only@*/ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
190 /*@out@*/ bool * propagate,
191 /*@out@*/ int *literal)
193 constraintExpr expr1;
194 constraintExpr expr2;
195 bool propagate1, propagate2;
196 int literal1, literal2;
197 constraintExprBinaryOpKind op;
209 llassert (expr != NULL);
211 /* we simplify unaryExpr elsewhere */
212 if (expr->kind != binaryexpr)
215 op = constraintExprData_binaryExprGetOp (expr->data);
217 DPRINTF((message("constraintExpr_propagateConstants: binaryexpr: %s", constraintExpr_unparse(expr) ) ) );
219 expr = removeZero(expr);
221 expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
222 expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
224 expr1 = constraintExpr_copy(expr1);
225 expr2 = constraintExpr_copy(expr2);
227 expr1 = constraintExpr_propagateConstants (expr1, &propagate1, &literal1);
228 expr2 = constraintExpr_propagateConstants (expr2, &propagate2, &literal2);
230 expr1 = removeZero(expr1);
231 expr2 = removeZero(expr2);
234 *propagate = propagate1 || propagate2;
236 if (op == BINARYOP_PLUS)
237 *literal = literal1 + literal2;
238 else if (op == BINARYOP_MINUS)
239 *literal = literal1 - literal2;
243 if ( constraintExpr_isLit (expr1) && constraintExpr_isLit (expr2) )
246 t1 = constraintExpr_getValue (expr1);
247 t2 = constraintExpr_getValue (expr2);
248 llassert(*propagate == FALSE);
251 constraintExpr_free (expr);
252 constraintExpr_free (expr1);
253 constraintExpr_free (expr2);
255 if (op == BINARYOP_PLUS )
256 return (constraintExpr_makeIntLiteral ((t1+t2) ));
257 else if (op == BINARYOP_MINUS)
258 return (constraintExpr_makeIntLiteral ((t1-t2) ));
264 if (constraintExpr_isLit (expr1) )
268 *literal += constraintExpr_getValue (expr1);
270 if (op == BINARYOP_PLUS)
272 constraintExpr_free(expr1);
273 constraintExpr_free(expr);
276 else if (op == BINARYOP_MINUS)
281 /* this is an ugly kludge to deal with not
282 having a unary minus operation...*/
284 temp = constraintExpr_makeIntLiteral (0);
285 temp = constraintExpr_makeSubtractExpr (temp, expr2);
287 constraintExpr_free(expr1);
288 constraintExpr_free(expr);
294 BADBRANCH; /* evans 2001-07-18 */
298 if (constraintExpr_isLit (expr2) )
302 if ( op == BINARYOP_PLUS )
303 *literal += constraintExpr_getValue (expr2);
304 else if (op == BINARYOP_MINUS)
305 *literal -= constraintExpr_getValue (expr2);
310 constraintExpr_free(expr2);
311 constraintExpr_free(expr);
315 DPRINTF((message("constraintExpr_propagateConstants returning: %s", constraintExpr_unparse(expr) ) ) );
317 expr->data = constraintExprData_binaryExprSetExpr1 (expr->data, expr1);
318 expr->data = constraintExprData_binaryExprSetExpr2 (expr->data, expr2);
320 expr = removeZero(expr);
324 /*@only@*/ static constraintExpr constraintExpr_combineConstants (/*@only@*/ constraintExpr expr ) /*@modifies expr@*/
329 DPRINTF ((message ("Before combine %s", constraintExpr_unparse(expr) ) ) );
330 expr = constraintExpr_propagateConstants (expr, &propagate, &literal);
339 ret = constraintExpr_makeBinaryOpConstraintExprIntLiteral (expr, literal);
343 DPRINTF ((message ("After combine %s", constraintExpr_unparse(expr) ) ) );
348 static constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
351 ret = dmalloc (sizeof (*ret) );
357 /*@only@*/ static constraintExprData copyExprData (/*@observer@*/ constraintExprData data, constraintExprKind kind)
359 constraintExprData ret;
360 llassert(constraintExprData_isDefined(data));
365 ret = constraintExprData_copyBinaryExpr(data);
368 ret = constraintExprData_copyUnaryExpr(data);
371 ret = constraintExprData_copyTerm(data);
379 constraintExpr constraintExpr_copy (constraintExpr expr)
382 ret = constraintExpr_alloc();
383 ret->kind = expr->kind;
385 ret->data = copyExprData (expr->data, expr->kind);
390 /*@only@*/ static constraintExpr oldconstraintExpr_makeTermExprNode ( /*@dependent@*/ exprNode e)
394 ret = constraintExpr_alloc();
396 ret->data = dmalloc (sizeof *(ret->data) );
397 t = constraintTerm_makeExprNode (e);
398 ret->data = constraintExprData_termSetTerm (ret->data, t);
402 constraintExpr constraintExpr_makeExprNode (exprNode e)
405 constraintExpr ret, ce1, ce2;
411 llassert (e != NULL);
418 t = exprData_getSingle (data);
419 s = exprNode_getSref (t);
420 if (sRef_isFixedArray(s) )
424 size = (int) sRef_getArraySize(s);
425 ret = constraintExpr_makeIntLiteral (size);
429 DPRINTF ((message ("could not determine the size of %s", exprNode_unparse (e) ) ) );
430 ret = oldconstraintExpr_makeTermExprNode (e);
435 DPRINTF ((message ("Examining operation %s", exprNode_unparse (e) ) ) );
436 t1 = exprData_getOpA (data);
437 t2 = exprData_getOpB (data);
438 tok = exprData_getOpTok (data);
440 if (lltok_isPlus_Op (tok) || lltok_isMinus_Op (tok) )
442 ce1 = constraintExpr_makeExprNode (t1);
443 ce2 = constraintExpr_makeExprNode (t2);
444 ret = constraintExpr_parseMakeBinaryOp (ce1, tok, ce2);
449 We handle expressions containing sizeof with the rule
450 (sizeof type ) * Expr = Expr
452 This is the total wronge way to do this but...
453 it may be better than nothing
455 else if (lltok_isMult(tok) )
457 if ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
459 ret = constraintExpr_makeExprNode(t2);
461 else if ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
463 ret = constraintExpr_makeExprNode(t1);
467 ret = oldconstraintExpr_makeTermExprNode (e);
471 ret = oldconstraintExpr_makeTermExprNode (e);
475 t = exprData_getUopNode (data);
476 ret = constraintExpr_makeExprNode (t);
480 t = exprData_getUopNode (data);
481 tok = exprData_getUopTok (data);
482 if (lltok_isInc_Op (tok) )
485 temp = constraintExpr_makeExprNode(t);
486 ret = constraintExpr_makeIncConstraintExpr(temp);
488 else if (lltok_isDec_Op (tok) )
491 temp = constraintExpr_makeExprNode(t);
492 ret = constraintExpr_makeDecConstraintExpr(temp);
495 ret = oldconstraintExpr_makeTermExprNode (e);
499 t = exprData_getUopNode (data);
500 ret = constraintExpr_makeExprNode (t);
503 t = exprData_getCastNode (data);
504 ret = constraintExpr_makeExprNode (t);
507 t = exprData_getPairA(data);
508 ret = constraintExpr_makeExprNode(t);
509 /*@i3434*/ /* drl: I'm not sure if this is right. I'm adding a break to quiet Splint */
512 ret = oldconstraintExpr_makeTermExprNode (e);
518 /*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e)
520 return oldconstraintExpr_makeTermExprNode(e);
523 static constraintExpr constraintExpr_makeTerm (/*@only@*/ constraintTerm t)
527 ret = constraintExpr_alloc();
529 ret->data = dmalloc (sizeof *(ret->data) );
530 ret->data->term = NULL;
531 ret->data = constraintExprData_termSetTerm (ret->data, t);
536 constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
540 ret = constraintExpr_alloc();
542 ret->data = dmalloc (sizeof *(ret->data) );
543 t = constraintTerm_makesRef (s);
544 ret->data = constraintExprData_termSetTerm (ret->data, t);
548 /*@special@*/ static constraintExpr makeUnaryOpGeneric (void) /*@allocates result->data@*/ /*@defines result->kind@*/
551 ret = constraintExpr_alloc();
552 ret->kind = unaryExpr;
553 ret->data = dmalloc ( sizeof *(ret->data) );
554 ret->data->unaryOp.expr = constraintExpr_undefined;
558 /*@only@*/ static constraintExpr constraintExpr_makeUnaryOpConstraintExpr (/*@only@*/ constraintExpr cexpr)
561 ret = makeUnaryOpGeneric();
565 ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
566 ret->data = constraintExprData_unaryExprSetOp (ret->data, UNARYOP_UNDEFINED);
575 /*@only@*/ static constraintExpr constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr, constraintExprUnaryOpKind Op )
578 ret = makeUnaryOpGeneric();
580 ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
581 ret->data = constraintExprData_unaryExprSetOp (ret->data, Op);
587 static constraintExpr constraintExpr_makeMaxSetConstraintExpr (/*@only@*/ constraintExpr c)
590 ret = constraintExpr_makeUnaryOp (c, MAXSET);
595 static constraintExpr constraintExpr_makeUnaryOpExprNode (/*@exposed@*/ exprNode expr)
599 sub = constraintExpr_makeExprNode (expr);
600 ret = constraintExpr_makeUnaryOpConstraintExpr(sub);
608 static constraintExpr constraintExpr_makeSRefUnaryOp (/*@temp@*/ /*@observer@*/ sRef s, constraintExprUnaryOpKind op)
613 t = constraintExpr_makeTermsRef (s);
614 ret = constraintExpr_makeUnaryOpConstraintExpr (t);
615 ret->data = constraintExprData_unaryExprSetOp (ret->data, op);
621 constraintExpr constraintExpr_makeSRefMaxRead( sRef s)
623 return (constraintExpr_makeSRefUnaryOp (s, MAXREAD) );
627 constraintExpr constraintExpr_makeSRefMaxset ( sRef s)
629 return (constraintExpr_makeSRefUnaryOp (s, MAXSET) );
633 constraintExpr constraintExpr_parseMakeUnaryOp (lltok op, constraintExpr cexpr)
636 ret = constraintExpr_makeUnaryOpConstraintExpr ( cexpr);
641 ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXSET);
644 ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
647 llfatalbug(message("Unhandled Operation in Constraint") );
653 constraintExpr constraintExpr_makeMaxSetExpr (/*@exposed@*/ exprNode expr)
656 ret = constraintExpr_makeExprNode (expr);
658 ret = constraintExpr_makeMaxSetConstraintExpr (ret);
660 llassert (ret != NULL);
665 constraintExpr constraintExpr_makeMaxReadExpr (exprNode expr)
668 ret = constraintExpr_makeUnaryOpExprNode(expr);
669 ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
675 /*@unused@*/ static constraintExpr constraintExpr_makeMinSetExpr (/*@exposed@*/ exprNode expr)
678 ret = constraintExpr_makeUnaryOpExprNode(expr);
679 ret->data = constraintExprData_unaryExprSetOp (ret->data, MINSET);
684 /*@unused@*/ static constraintExpr constraintExpr_makeMinReadExpr (/*@exposed@*/ exprNode expr)
687 ret = constraintExpr_makeUnaryOpExprNode(expr);
688 ret->data = constraintExprData_unaryExprSetOp (ret->data, MINREAD);
694 constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode expr)
697 ret = constraintExpr_makeExprNode (expr);
702 constraintExpr constraintExpr_makeIntLiteral (long i)
706 ret = constraintExpr_alloc();
708 ret->data = dmalloc (sizeof *(ret->data) );
709 t = constraintTerm_makeIntLiteral (i);
710 ret->data = constraintExprData_termSetTerm (ret->data, t);
715 constraintExpr constraintExpr_makeValueInt (int i)
717 return constraintExpr_makeIntLiteral (i);
722 /*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
723 /*@allocates result->data @*/ /*@sets result->kind @*/
726 ret = constraintExpr_alloc();
727 ret->kind = binaryexpr;
728 ret->data = dmalloc ( sizeof *(ret->data) );
730 ret->data->binaryOp.expr1 = constraintExpr_undefined;
731 ret->data->binaryOp.expr2 = constraintExpr_undefined;
737 static /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExpr (/*@only@*/constraintExpr expr1, /*@only@*/ constraintExpr expr2)
742 ret = constraintExpr_makeBinaryOp();
743 ret->data = constraintExprData_binaryExprSetExpr1 (ret->data, expr1);
744 ret->data = constraintExprData_binaryExprSetExpr2 (ret->data, expr2);
745 ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_UNDEFINED);
750 constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr expr1, lltok op,/*@only@*/ constraintExpr expr2)
753 ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
755 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
756 else if (op.tok == TMINUS)
757 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
767 /*@unused@*/ static constraintExpr constraintExpr_makeBinaryOpExprNode (/*@exposed@*/ exprNode expr1, /*@exposed@*/ exprNode expr2)
770 constraintExpr sub1, sub2;
771 sub1 = constraintExpr_makeTermExprNode (expr1);
772 sub2 = constraintExpr_makeTermExprNode (expr2);
773 ret = constraintExpr_makeBinaryOpConstraintExpr(sub1, sub2);
779 constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/ constraintExpr expr, int literal)
782 constraintExpr constExpr;
784 constExpr = constraintExpr_makeIntLiteral (literal);
785 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, constExpr);
786 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
791 constraintExpr constraintExpr_makeDecConstraintExpr (/*@only@*/constraintExpr expr)
796 inc = constraintExpr_makeIntLiteral (1);
797 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
798 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
803 /*@only@*/ constraintExpr constraintExpr_makeSubtractExpr (/*@only@*/ constraintExpr expr, /*@only@*/ constraintExpr addent)
807 DPRINTF ((message ("Making subtract expression") ) );
809 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
810 ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_MINUS);
815 constraintExpr constraintExpr_makeAddExpr (/*@only@*/
816 constraintExpr expr, /*@only@*/
817 constraintExpr addent)
821 DPRINTF ((message ("Doing addTerm simplification") ) );
823 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
824 ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_PLUS);
830 constraintExpr constraintExpr_makeIncConstraintExpr (/*@only@*/ constraintExpr expr)
835 inc = constraintExpr_makeIntLiteral (1);
836 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
837 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
842 static cstring constraintExprUnaryOpKind_print (constraintExprUnaryOpKind op)
847 return message("maxSet");
849 return message("minSet");
851 return message("maxRead");
853 return message("minRead");
856 return message ("<(Unary OP OTHER>");
862 static cstring constraintExprBinaryOpKind_print (constraintExprBinaryOpKind op)
874 return message ("<binary OP Unknown>");
878 bool constraintExpr_similar (constraintExpr expr1, constraintExpr expr2)
880 constraintExprKind kind;
882 llassert (expr1 != NULL);
883 llassert (expr2 != NULL);
884 if (expr1->kind != expr2->kind)
892 return constraintTerm_similar (constraintExprData_termGetTerm(expr1->data),
893 constraintExprData_termGetTerm(expr2->data) );
894 /*@notreached@*/ break;
897 if (constraintExprData_unaryExprGetOp (expr1->data) != constraintExprData_unaryExprGetOp (expr2->data) )
900 return (constraintExpr_similar (
901 constraintExprData_unaryExprGetExpr (expr1->data),
902 constraintExprData_unaryExprGetExpr (expr2->data)
906 if (constraintExprData_binaryExprGetOp (expr1->data) != constraintExprData_binaryExprGetOp (expr2->data) )
909 if (! constraintExpr_similar (constraintExprData_binaryExprGetExpr1 (expr1->data),
910 constraintExprData_binaryExprGetExpr1 (expr2->data)) )
913 if (! constraintExpr_similar (constraintExprData_binaryExprGetExpr2 (expr1->data),
914 constraintExprData_binaryExprGetExpr2 (expr2->data)) )
929 bool constraintExpr_same (constraintExpr expr1, constraintExpr expr2)
931 constraintExprKind kind;
933 llassert (expr1 != NULL);
934 llassert (expr2 != NULL);
935 if (expr1->kind != expr2->kind)
943 return constraintTerm_similar (constraintExprData_termGetTerm(expr1->data),
944 constraintExprData_termGetTerm(expr2->data) );
945 /*@notreached@*/ break;
948 if (constraintExprData_unaryExprGetOp (expr1->data) != constraintExprData_unaryExprGetOp (expr2->data) )
951 return (constraintExpr_same (
952 constraintExprData_unaryExprGetExpr (expr1->data),
953 constraintExprData_unaryExprGetExpr (expr2->data)
958 if (constraintExprData_binaryExprGetOp (expr1->data) != constraintExprData_binaryExprGetOp (expr2->data) )
961 if (! constraintExpr_same (constraintExprData_binaryExprGetExpr1 (expr1->data),
962 constraintExprData_binaryExprGetExpr1 (expr2->data)) )
965 if (! constraintExpr_same (constraintExprData_binaryExprGetExpr2 (expr1->data),
966 constraintExprData_binaryExprGetExpr2 (expr2->data)) )
970 /*@notreached@*/ break;
981 bool constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ constraintExpr old)
984 constraintExprKind kind;
987 if ( constraintExpr_similar (c, old) )
989 DPRINTF((message ("Found %q",
990 constraintExpr_unparse(old)
1002 temp = constraintExprData_unaryExprGetExpr (c->data);
1003 ret = ret || constraintExpr_search (temp, old);
1007 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1008 ret = ret || constraintExpr_search(temp, old);
1010 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1011 ret = ret || constraintExpr_search(temp, old);
1021 /*@only@*/ constraintExpr constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@temp@*/ constraintExpr old, /*@temp@*/ constraintExpr newExpr )
1023 constraintExprKind kind;
1024 constraintExpr temp;
1026 if ( constraintExpr_similar (c, old) )
1029 DPRINTF((message ("Replacing %s with %s",
1030 constraintExpr_unparse(old), constraintExpr_unparse(newExpr)
1032 constraintExpr_free(c);
1033 return constraintExpr_copy (newExpr);
1043 temp = constraintExprData_unaryExprGetExpr (c->data);
1044 temp = constraintExpr_copy(temp);
1045 temp = constraintExpr_searchandreplace (temp, old, newExpr);
1046 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1050 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1051 temp = constraintExpr_copy(temp);
1052 temp = constraintExpr_searchandreplace (temp, old, newExpr);
1053 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1055 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1056 temp = constraintExpr_copy(temp);
1057 temp = constraintExpr_searchandreplace (temp, old, newExpr);
1058 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1067 static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ constraintExpr c)
1069 constraintExprKind kind;
1070 constraintExpr temp;
1079 temp = constraintExprData_unaryExprGetExpr (c->data);
1080 temp = constraintExpr_copy(temp);
1081 temp = constraintExpr_simplify (temp);
1082 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1085 DPRINTF((message("constraintExpr_simplfiyChildren: simplify binary expression: %s",constraintExpr_unparse(c) ) ) );
1086 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1087 temp = constraintExpr_copy(temp);
1088 temp = constraintExpr_simplify (temp);
1090 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1092 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1093 temp = constraintExpr_copy(temp);
1094 temp = constraintExpr_simplify (temp);
1096 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1106 constraintExpr constraintExpr_setFileloc (/*@returned@*/ constraintExpr c, fileloc loc) /*@modifies c @*/
1109 constraintExpr temp;
1111 llassert(c != NULL);
1116 t = constraintExprData_termGetTerm (c->data);
1117 t = constraintTerm_copy(t);
1118 t = constraintTerm_setFileloc (t, loc);
1119 c->data = constraintExprData_termSetTerm (c->data, t);
1123 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1124 temp = constraintExpr_copy(temp);
1125 temp = constraintExpr_setFileloc (temp, loc);
1126 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1128 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1129 temp = constraintExpr_copy(temp);
1130 temp = constraintExpr_setFileloc (temp, loc);
1131 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1134 temp = constraintExprData_unaryExprGetExpr (c->data);
1135 temp = constraintExpr_copy(temp);
1136 temp = constraintExpr_setFileloc (temp, loc);
1137 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1143 static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/constraintExpr c)
1145 constraintExpr e1, e2;
1146 constraintExprBinaryOpKind op;
1148 e1 = constraintExprData_binaryExprGetExpr1 (c->data);
1149 e2 = constraintExprData_binaryExprGetExpr2 (c->data);
1151 if (constraintExpr_canGetValue (e1) && constraintExpr_canGetValue(e2) )
1155 i = constraintExpr_getValue(e1) + constraintExpr_getValue (e2);
1156 constraintExpr_free(c);
1157 c = constraintExpr_makeIntLiteral (i);
1161 op = constraintExprData_binaryExprGetOp (c->data);
1162 if (op == BINARYOP_MINUS)
1163 if (constraintExpr_similar(e1, e2) )
1165 constraintExpr_free(c);
1166 c = constraintExpr_makeIntLiteral (0);
1174 this thing takes the lexpr and expr of a constraint and modifies lexpr
1175 and returns a (possiblly new) value for expr
1177 /* if lexpr is a binary express say x + y, we set lexpr to x and return a value for expr such as expr_old - y */
1179 /* the approach is a little Kludgy but seems to work. I should probably use something cleaner at some point ... */
1182 /*@only@*/ constraintExpr constraintExpr_solveBinaryExpr (constraintExpr lexpr, /*@only@*/ constraintExpr expr)
1184 constraintExpr expr1, expr2;
1185 constraintExprBinaryOpKind op;
1187 if (lexpr->kind != binaryexpr)
1190 expr2 = constraintExprData_binaryExprGetExpr2 (lexpr->data);
1191 expr1 = constraintExprData_binaryExprGetExpr1 (lexpr->data);
1193 op = constraintExprData_binaryExprGetOp (lexpr->data);
1195 expr1 = constraintExpr_copy(expr1);
1196 expr2 = constraintExpr_copy(expr2);
1198 /* drl possible problem : warning make sure this works */
1200 lexpr->kind = expr1->kind;
1201 sfree (lexpr->data);
1203 lexpr->data = copyExprData (expr1->data, expr1->kind);
1204 constraintExpr_free(expr1);
1206 if (op == BINARYOP_PLUS)
1207 expr = constraintExpr_makeSubtractExpr (expr, expr2);
1208 else if (op == BINARYOP_MINUS)
1209 expr = constraintExpr_makeAddExpr (expr, expr2);
1217 #warning this needs to be checked
1218 expr = constraintExpr_solveBinaryExpr (expr1, expr);
1220 expr = constraintExpr_solveBinaryExpr (expr2, expr);
1225 static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ constraintExpr c)
1229 llassert (c->kind == unaryExpr);
1231 DPRINTF ((message ("Doing constraintExpr_simplifyunaryExpr:%s", constraintExpr_unparse (c) ) ) );
1233 if ((constraintExprData_unaryExprGetOp (c->data) != MAXSET) &&
1234 (constraintExprData_unaryExprGetOp (c->data) != MAXREAD) )
1239 exp = constraintExprData_unaryExprGetExpr (c->data);
1240 exp = constraintExpr_copy(exp);
1242 if (exp->kind == term)
1244 constraintTerm cterm;
1246 cterm = constraintExprData_termGetTerm (exp->data);
1248 if (constraintTerm_isStringLiteral(cterm) )
1251 val = constraintTerm_getStringLiteral (cterm);
1252 if (constraintExprData_unaryExprGetOp (c->data) == MAXSET)
1254 constraintExpr temp;
1256 temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
1258 constraintExpr_free(c);
1259 constraintExpr_free(exp);
1264 if (constraintExprData_unaryExprGetOp (c->data) == MAXREAD)
1266 constraintExpr temp;
1268 temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
1270 constraintExpr_free(c);
1271 constraintExpr_free(exp);
1278 /* slight Kludge to hanlde var [] = { , , };
1279 ** type syntax I don't think this is sounds but it should be good
1280 ** enough. The C stanrad is very confusing about initialization
1284 if (constraintTerm_isInitBlock(cterm) )
1286 constraintExpr temp;
1289 len = constraintTerm_getInitBlockLength(cterm);
1291 temp = constraintExpr_makeIntLiteral (len );
1293 constraintExpr_free(c);
1294 DPRINTF(( message("Changed too %q", constraintExpr_print(temp)
1296 constraintExpr_free(exp);
1300 constraintExpr_free(exp);
1304 if (exp->kind != binaryexpr)
1306 constraintExpr_free(exp);
1310 if (constraintExprData_binaryExprGetOp (exp->data) == BINARYOP_PLUS )
1313 /* if (constraintExpr_canGetValue (constraintExprData_binaryExprGetExpr2 (exp->data) ) ) */
1316 constraintExpr temp, temp2;
1318 DPRINTF ((message ("Doing fancy simplification") ) );
1320 temp = constraintExprData_binaryExprGetExpr2 (exp->data);
1322 temp2 = constraintExprData_binaryExprGetExpr1 (exp->data);
1324 temp2 = constraintExpr_copy(temp2);
1325 c->data = constraintExprData_unaryExprSetExpr (c->data, temp2);
1328 temp = constraintExpr_copy (temp);
1330 c = constraintExpr_makeSubtractExpr (c, temp);
1332 DPRINTF ((message ("Done fancy simplification:%s", constraintExpr_unparse (c) ) ) );
1336 DPRINTF ((message ("constraintExpr_simplifyUnaryExpr: Done simplification:%s", constraintExpr_unparse (c) ) ) );
1338 constraintExpr_free(exp);
1343 /*@only@*/ constraintExpr constraintExpr_simplify (/*@only@*/ constraintExpr c)
1345 constraintExprKind kind;
1349 DPRINTF ((message ("Doing constraintExpr_simplify:%s", constraintExpr_unparse (c) ) ) );
1354 /* drl: I think this is an Splint bug */
1356 ret = constraintExpr_copy(c);
1358 constraintExpr_free(c);
1360 ret = constraintExpr_simplifyChildren (ret);
1362 ret = constraintExpr_combineConstants (ret);
1364 ret = constraintExpr_simplifyChildren (ret);
1372 t = constraintExprData_termGetTerm (ret->data);
1373 t = constraintTerm_copy(t);
1374 t = constraintTerm_simplify (t);
1375 ret->data = constraintExprData_termSetTerm (ret->data, t);
1378 ret = constraintExpr_simplifyunaryExpr (ret);
1381 ret = constraintExpr_simplifybinaryExpr (ret);
1387 DPRINTF ((message ("constraintExpr_simplify returning :%s", constraintExpr_unparse (ret) ) ) );
1393 cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@*/
1396 constraintExprKind kind;
1398 llassert (ex != NULL);
1406 if (context_getFlag (FLG_PARENCONSTRAINT) )
1408 st = message ("(%q) ", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
1412 st = message ("%q", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
1416 st = message ("%q(%q)",
1417 constraintExprUnaryOpKind_print (constraintExprData_unaryExprGetOp (ex->data) ),
1418 constraintExpr_unparse (constraintExprData_unaryExprGetExpr (ex->data) )
1422 if (context_getFlag (FLG_PARENCONSTRAINT) )
1424 st = message ("(%q) %q (%q)",
1425 constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
1426 constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
1428 constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
1433 st = message ("%q %q %q",
1434 constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
1435 constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
1437 constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
1444 st = message ("error");
1448 DPRINTF((message ("constraintExpr_unparse: '%s'",st) ) );
1452 constraintExpr constraintExpr_doSRefFixBaseParam (/*@returned@*/ constraintExpr expr, exprNodeList arglist)
1454 constraintTerm Term;
1455 constraintExprKind kind;
1456 constraintExpr expr1, expr2;
1457 constraintExprData data;
1458 llassert (expr != NULL);
1467 Term = constraintExprData_termGetTerm(data);
1468 Term = constraintTerm_copy(Term);
1470 Term = constraintTerm_doSRefFixBaseParam (Term, arglist);
1471 data = constraintExprData_termSetTerm(data, Term);
1474 expr1 = constraintExprData_unaryExprGetExpr (data);
1475 expr1 = constraintExpr_copy(expr1);
1477 expr1 = constraintExpr_doSRefFixBaseParam (expr1, arglist);
1478 data = constraintExprData_unaryExprSetExpr (data, expr1);
1481 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1482 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1484 expr1 = constraintExpr_copy(expr1);
1485 expr2 = constraintExpr_copy(expr2);
1487 expr1 = constraintExpr_doSRefFixBaseParam (expr1, arglist);
1488 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1489 expr2 = constraintExpr_doSRefFixBaseParam (expr2, arglist);
1490 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1500 /*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@only@*/ constraintExpr expr, exprNodeList arglist) /*@modifies expr@*/
1502 constraintExprKind kind;
1503 constraintExpr expr1, expr2;
1504 constraintExprData data;
1505 llassert (expr != NULL);
1514 expr = doSRefFixConstraintParamTerm (expr, arglist);
1517 expr1 = constraintExprData_unaryExprGetExpr (data);
1518 expr1 = constraintExpr_copy(expr1);
1519 expr1 = constraintExpr_doSRefFixConstraintParam (expr1, arglist);
1520 data = constraintExprData_unaryExprSetExpr (data, expr1);
1523 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1524 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1526 expr1 = constraintExpr_copy(expr1);
1527 expr2 = constraintExpr_copy(expr2);
1529 expr1 = constraintExpr_doSRefFixConstraintParam (expr1, arglist);
1530 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1531 expr2 = constraintExpr_doSRefFixConstraintParam (expr2, arglist);
1532 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1542 /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/ constraintExpr expr, /*@observer@*/ exprNode fcnCall)
1544 constraintExprKind kind;
1545 constraintExpr expr1, expr2;
1546 constraintExprData data;
1547 llassert (expr != NULL);
1556 expr = doFixResultTerm (expr, fcnCall);
1559 expr1 = constraintExprData_unaryExprGetExpr (data);
1560 expr1 = constraintExpr_copy(expr1);
1562 expr1 = constraintExpr_doFixResult (expr1, fcnCall);
1563 data = constraintExprData_unaryExprSetExpr (data, expr1);
1566 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1567 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1569 expr1 = constraintExpr_copy(expr1);
1570 expr2 = constraintExpr_copy(expr2);
1572 expr1 = constraintExpr_doFixResult (expr1, fcnCall);
1573 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1574 expr2 = constraintExpr_doFixResult (expr2, fcnCall);
1575 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1585 cstring constraintExpr_print (constraintExpr expr) /*@*/
1587 return constraintExpr_unparse (expr);
1590 bool constraintExpr_hasMaxSet (constraintExpr expr) /*@*/
1594 t = constraintExpr_unparse(expr);
1596 if (cstring_containsLit(t, "maxSet") != NULL )
1610 /*returns 1 0 -1 like strcmp
1616 int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2)
1618 long value1, value2;
1620 if (constraintExpr_similar (expr1, expr2) )
1625 value1 = constraintExpr_getValue(expr1);
1626 value2 = constraintExpr_getValue(expr2);
1628 if (value1 > value2)
1631 if (value1 == value2)
1638 long constraintExpr_getValue (constraintExpr expr)
1640 llassert (expr->kind == term);
1641 return (constraintTerm_getValue (constraintExprData_termGetTerm (expr->data)));
1644 bool constraintExpr_canGetValue (constraintExpr expr)
1649 return constraintTerm_canGetValue (constraintExprData_termGetTerm (expr->data) );
1658 fileloc constraintExpr_getFileloc (constraintExpr expr)
1662 constraintExprKind kind;
1669 t = constraintExprData_termGetTerm (expr->data);
1670 return (constraintTerm_getFileloc (t) );
1674 e = constraintExprData_unaryExprGetExpr (expr->data);
1675 return (constraintExpr_getFileloc (e) );
1679 e = constraintExprData_binaryExprGetExpr1 (expr->data);
1680 return (constraintExpr_getFileloc (e) );
1685 return (fileloc_undefined);
1688 /*drl moved from constriantTerm.c 5/20/001*/
1689 static /*@only@*/ constraintExpr
1690 doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall)
1694 /*maybe this should move to cosntraintExpr.c -drl7x 5/18/01*/
1697 constraintExprData data = e->data;
1698 constraintExprKind kind = e->kind;
1702 llassert(kind == term);
1704 t = constraintExprData_termGetTerm (data);
1705 llassert (constraintTerm_isDefined(t) );
1708 switch (constraintTerm_getKind(t) )
1716 s = constraintTerm_getSRef(t);
1717 if (sRef_isResult (s))
1719 ret = constraintExpr_makeExprNode(fcnCall);
1720 constraintExpr_free(e);
1736 /*drl moved from constriantTerm.c 5/20/001*/
1737 /*@only@*/ static constraintExpr
1738 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
1742 constraintExprData data = e->data;
1744 constraintExprKind kind = e->kind;
1748 llassert(kind == term);
1750 t = constraintExprData_termGetTerm (data);
1751 llassert (constraintTerm_isDefined(t) );
1755 DPRINTF (("Fixing: %s", constraintExpr_print (e)));
1757 switch (constraintTerm_getKind(t))
1760 DPRINTF((message ("%q @ %q ", constraintTerm_print(t),
1761 fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
1764 DPRINTF((message (" %q ", constraintTerm_print (t)) ));
1768 /* evans 2001-07-24: constants should use the original term */
1769 if (!constraintTerm_canGetValue (t))
1771 DPRINTF ((message("Doing sRef_fixConstraintParam for %q ",
1772 constraintTerm_print (t) ) ));
1773 ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
1775 constraintExpr_free (e);
1777 DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
1778 constraintExpr_print (ret) ) ));
1780 } /*@=branchstate@*/
1792 /* bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term) */
1794 /* if (constraintTerm_hasTerm (expr->term, term) ) */
1797 /* if ((expr->expr) != NULL) */
1799 /* return ( constraintExpr_includesTerm (expr->expr, term) ); */
1805 /*drl added 6/11/01 */
1806 bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c)
1808 if (c->kind == binaryexpr)
1815 /*drl added 8/08/001 */
1816 bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
1818 if (c->kind == term)
1825 /*@observer@*/ /*@temp@*/ constraintTerm constraintExpr_getTerm ( /*@temp@*/ /*@observer@*/ constraintExpr c) /*@*/
1827 constraintTerm term;
1829 llassert(constraintExpr_isTerm(c) );
1831 term = constraintExprData_termGetTerm(c->data);
1836 static void binaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
1838 constraintExpr expr1;
1839 constraintExprBinaryOpKind binaryOp;
1840 constraintExpr expr2;
1843 binaryOp = constraintExprData_binaryExprGetOp (data);
1845 fprintf(f, "%d\n", (int) binaryOp);
1847 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1848 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1852 constraintExpr_dump(expr1, f);
1855 constraintExpr_dump(expr2, f);
1859 static constraintExpr binaryExpr_undump (FILE *f)
1861 constraintExpr expr1;
1862 constraintExprBinaryOpKind binaryOp;
1863 constraintExpr expr2;
1872 os = mstring_create (MAX_DUMP_LINE_LENGTH);
1874 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1877 binaryOp = (constraintExprBinaryOpKind) reader_getInt(&str);
1879 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1881 reader_checkChar (&str, 'e');
1882 reader_checkChar (&str, '1');
1884 expr1 = constraintExpr_undump (f);
1886 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1888 reader_checkChar (&str, 'e');
1889 reader_checkChar (&str, '2');
1891 expr2 = constraintExpr_undump (f);
1893 ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
1894 ret->data = constraintExprData_binaryExprSetOp(ret->data, binaryOp);
1902 static void unaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
1905 constraintExpr expr;
1906 constraintExprUnaryOpKind unaryOp;
1908 unaryOp = constraintExprData_unaryExprGetOp (data);
1910 fprintf(f, "%d\n", (int) unaryOp);
1912 expr = constraintExprData_unaryExprGetExpr (data);
1914 constraintExpr_dump(expr, f);
1917 static constraintExpr unaryExpr_undump ( FILE *f)
1920 constraintExpr expr;
1921 constraintExprUnaryOpKind unaryOp;
1927 str = mstring_create (MAX_DUMP_LINE_LENGTH);
1929 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1931 unaryOp = (constraintExprUnaryOpKind) reader_getInt(&str);
1933 expr = constraintExpr_undump (f);
1935 ret = constraintExpr_makeUnaryOp (expr, unaryOp);
1942 void constraintExpr_dump (/*@observer@*/ constraintExpr expr, FILE *f)
1944 constraintExprKind kind;
1950 fprintf(f,"%d\n", (int) kind);
1955 t = constraintExprData_termGetTerm (expr->data);
1956 constraintTerm_dump (t, f);
1959 unaryExpr_dump (expr->data, f);
1962 binaryExpr_dump (expr->data, f);
1967 /*@only@*/ constraintExpr constraintExpr_undump (FILE *f)
1969 constraintExprKind kind;
1976 s = mstring_create (MAX_DUMP_LINE_LENGTH);
1980 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1982 kind = (constraintExprKind) reader_getInt(&s);
1989 t = constraintTerm_undump (f);
1990 ret = constraintExpr_makeTerm(t);
1993 ret = unaryExpr_undump (f);
1996 ret = binaryExpr_undump (f);
2004 int constraintExpr_getDepth (constraintExpr ex)
2008 constraintExprKind kind;
2010 llassert (ex != NULL);
2020 ret = constraintExpr_getDepth (constraintExprData_unaryExprGetExpr (ex->data) );
2026 ret = constraintExpr_getDepth (constraintExprData_binaryExprGetExpr1 (ex->data) );
2030 ret += constraintExpr_getDepth (constraintExprData_binaryExprGetExpr2 (ex->data) );