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
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"
40 static ctype constraintExpr_getOrigType (constraintExpr p_e);
41 static bool constraintExpr_hasTypeChange(constraintExpr p_e) /*@*/;
43 static /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/constraintExpr p_expr, int p_literal);
46 /*@only@*/ static constraintExpr
47 doSRefFixInvarConstraintTerm (/*@only@*/ constraintExpr p_e,
48 sRef p_s, ctype p_ct);
50 /*@only@*/ static constraintExpr
51 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr p_e, /*@temp@*/ /*@observer@*/ exprNodeList p_arglist) /*@modifies p_e@*/;
53 static /*@only@*/ constraintExpr
54 doFixResultTerm (/*@only@*/ constraintExpr p_e, /*@exposed@*/ exprNode p_fcnCall)
57 static bool constraintExpr_canGetCType (constraintExpr p_e) /*@*/;
59 static ctype constraintExpr_getCType (constraintExpr p_e);
61 static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr p_e, ctype p_ct);
63 /*@special@*/ /*@notnull@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
64 /* @allocates result->data @ @sets result->kind @ */ ;
66 void constraintExpr_free (/*@only@*/ constraintExpr expr)
68 if (constraintExpr_isDefined(expr) )
73 constraintExprData_freeUnaryExpr(expr->data);
76 constraintExprData_freeBinaryExpr(expr->data);
79 constraintExprData_freeTerm(expr->data);
90 llcontbug(message("attempted to free null pointer in constraintExpr_free"));
94 bool constraintExpr_isLit (constraintExpr expr)
96 llassert (expr != NULL);
98 if (expr->kind == term)
100 constraintTerm term = constraintExprData_termGetTerm (expr->data);
101 if (constraintTerm_isIntLiteral (term) )
110 static bool isZeroBinaryOp (constraintExpr expr)
114 llassert (expr != NULL); /* evans 2001-07-18 */
116 if (!constraintExpr_isBinaryExpr (expr) )
122 e2 = constraintExprData_binaryExprGetExpr2(expr->data);
124 llassert (e2 != NULL); /* evans 2001-07-18 */
126 if (constraintExpr_isBinaryExpr (e2) )
129 constraintExprBinaryOpKind op;
131 op = constraintExprData_binaryExprGetOp (e2->data);
133 e1 = constraintExprData_binaryExprGetExpr1(e2->data);
135 if (constraintExpr_isLit(e1) )
137 if (constraintExpr_getValue(e1) == 0 )
146 /* change expr + (o - expr) to (expr -expr) */
148 /*@only@*/ /*@notnull@*/ static constraintExpr removeZero (/*@only@*/ /*@returned@*/ constraintExpr expr)
150 constraintExpr expr1, expr2;
154 constraintExprBinaryOpKind op;
156 constraintExprBinaryOpKind tempOp;
158 llassert (expr != NULL); /* evans 2001-07-18 */
160 if (!isZeroBinaryOp(expr) )
164 expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
165 expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
166 op = constraintExprData_binaryExprGetOp(expr->data);
168 llassert( constraintExpr_isBinaryExpr(expr2) );
170 temp = constraintExprData_binaryExprGetExpr2 (expr2->data);
171 temp = constraintExpr_copy (temp);
173 tempOp = constraintExprData_binaryExprGetOp (expr2->data);
175 if (op == BINARYOP_PLUS)
177 else if (op == BINARYOP_MINUS)
179 if (tempOp == BINARYOP_PLUS)
181 else if (tempOp == BINARYOP_MINUS)
189 expr->data = constraintExprData_binaryExprSetExpr2(expr->data, temp);
190 expr->data = constraintExprData_binaryExprSetOp(expr->data, op);
196 /*@only@*//*@notnull@*/ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
197 /*@out@*/ bool * propagate,
198 /*@out@*/ int *literal)
200 constraintExpr expr1;
201 constraintExpr expr2;
202 bool propagate1, propagate2;
203 int literal1, literal2;
204 constraintExprBinaryOpKind op;
216 llassert (expr != NULL);
218 /* we simplify unaryExpr elsewhere */
219 if (expr->kind != binaryexpr)
222 op = constraintExprData_binaryExprGetOp (expr->data);
224 DPRINTF((message("constraintExpr_propagateConstants: binaryexpr: %s", constraintExpr_unparse(expr) ) ) );
226 expr = removeZero(expr);
228 expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
229 expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
231 expr1 = constraintExpr_copy(expr1);
232 expr2 = constraintExpr_copy(expr2);
234 expr1 = constraintExpr_propagateConstants (expr1, &propagate1, &literal1);
235 expr2 = constraintExpr_propagateConstants (expr2, &propagate2, &literal2);
237 expr1 = removeZero(expr1);
238 expr2 = removeZero(expr2);
241 *propagate = propagate1 || propagate2;
243 if (op == BINARYOP_PLUS)
244 *literal = literal1 + literal2;
245 else if (op == BINARYOP_MINUS)
246 *literal = literal1 - literal2;
250 if ( constraintExpr_isLit (expr1) && constraintExpr_isLit (expr2) )
253 t1 = constraintExpr_getValue (expr1);
254 t2 = constraintExpr_getValue (expr2);
255 llassert(*propagate == FALSE);
258 constraintExpr_free (expr);
259 constraintExpr_free (expr1);
260 constraintExpr_free (expr2);
262 if (op == BINARYOP_PLUS )
263 return (constraintExpr_makeIntLiteral ((t1+t2) ));
264 else if (op == BINARYOP_MINUS)
265 return (constraintExpr_makeIntLiteral ((t1-t2) ));
271 if (constraintExpr_isLit (expr1) )
275 *literal += constraintExpr_getValue (expr1);
277 if (op == BINARYOP_PLUS)
279 constraintExpr_free(expr1);
280 constraintExpr_free(expr);
283 else if (op == BINARYOP_MINUS)
288 /* this is an ugly kludge to deal with not
289 having a unary minus operation...*/
291 temp = constraintExpr_makeIntLiteral (0);
292 temp = constraintExpr_makeSubtractExpr (temp, expr2);
294 constraintExpr_free(expr1);
295 constraintExpr_free(expr);
297 llassert (constraintExpr_isDefined(temp) );
302 BADBRANCH; /* evans 2001-07-18 */
306 if (constraintExpr_isLit (expr2) )
310 if ( op == BINARYOP_PLUS )
311 *literal += constraintExpr_getValue (expr2);
312 else if (op == BINARYOP_MINUS)
313 *literal -= constraintExpr_getValue (expr2);
318 constraintExpr_free(expr2);
319 constraintExpr_free(expr);
323 DPRINTF((message("constraintExpr_propagateConstants returning: %s", constraintExpr_unparse(expr) ) ) );
325 expr->data = constraintExprData_binaryExprSetExpr1 (expr->data, expr1);
326 expr->data = constraintExprData_binaryExprSetExpr2 (expr->data, expr2);
328 expr = removeZero(expr);
332 /*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_combineConstants (/*@only@*/ constraintExpr expr ) /*@modifies expr@*/
337 DPRINTF ((message ("Before combine %s", constraintExpr_unparse(expr) ) ) );
338 expr = constraintExpr_propagateConstants (expr, &propagate, &literal);
347 ret = constraintExpr_makeBinaryOpConstraintExprIntLiteral (expr, literal);
351 DPRINTF ((message ("After combine %s", constraintExpr_unparse(expr) ) ) );
353 llassert(constraintExpr_isDefined(expr) );
358 static /*@notnull@*/ constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
361 ret = dmalloc (sizeof (*ret) );
365 ret->origType = ctype_undefined;
369 /*@only@*/ static constraintExprData copyExprData (/*@observer@*/ constraintExprData data, constraintExprKind kind)
371 constraintExprData ret;
372 llassert(constraintExprData_isDefined(data));
377 ret = constraintExprData_copyBinaryExpr(data);
380 ret = constraintExprData_copyUnaryExpr(data);
383 ret = constraintExprData_copyTerm(data);
391 constraintExpr constraintExpr_copy (constraintExpr expr)
394 ret = constraintExpr_alloc ();
397 /*drl 03/02/2003 this shouldn't be used to copy a null
398 expression but handle things cleanly if it is*/
399 llassert (!constraintExpr_isUndefined(expr) );
401 if (constraintExpr_isUndefined(expr) )
403 return constraintExpr_undefined;
406 ret->kind = expr->kind;
408 ret->data = copyExprData (expr->data, expr->kind);
410 ret->origType = expr->origType;
415 /*@only@*/ static constraintExpr oldconstraintExpr_makeTermExprNode ( /*@dependent@*/ exprNode e)
419 ret = constraintExpr_alloc();
421 ret->data = dmalloc (sizeof *(ret->data) );
422 t = constraintTerm_makeExprNode (e);
423 ret->data = constraintExprData_termSetTerm (ret->data, t);
425 ret->origType = ctype_undefined;
430 /*@access exprNode@*/
431 constraintExpr constraintExpr_makeExprNode (exprNode e)
434 constraintExpr ret, ce1, ce2;
439 llassert (e != NULL);
446 t = exprData_getSingle (data);
447 while (exprNode_isInParens (t) )
449 t = exprData_getUopNode (t->edata);
451 s = exprNode_getSref (t);
452 if (sRef_isFixedArray(s) )
456 size = (int) sRef_getArraySize(s);
457 ret = constraintExpr_makeIntLiteral (size);
459 else if (exprNode_isStringLiteral (t))
461 cstring str = multiVal_forceString (exprNode_getValue(t));
462 ret = constraintExpr_makeIntLiteral (size_toLong (cstring_length (str) + 1));
466 DPRINTF ((message ("could not determine the size of %s", exprNode_unparse (e) ) ) );
467 ret = oldconstraintExpr_makeTermExprNode (e);
472 DPRINTF ((message ("Examining operation %s", exprNode_unparse (e) ) ) );
473 t1 = exprData_getOpA (data);
474 t2 = exprData_getOpB (data);
475 tok = exprData_getOpTok (data);
477 if (lltok_isPlus_Op (tok) || lltok_isMinus_Op (tok) )
479 ce1 = constraintExpr_makeExprNode (t1);
480 ce2 = constraintExpr_makeExprNode (t2);
481 ret = constraintExpr_parseMakeBinaryOp (ce1, tok, ce2);
485 /* define this block to activate the cheesy heuristic
486 for handling sizeof expressions*/
493 We handle expressions containing sizeof with the rule
494 (sizeof type ) * Expr = Expr
496 This is the total wronge way to do this but...
497 it may be better than nothing
502 else if (lltok_isMult(tok) )
504 if ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
506 ret = constraintExpr_makeExprNode(t2);
508 else if ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
510 ret = constraintExpr_makeExprNode(t1);
514 ret = oldconstraintExpr_makeTermExprNode (e);
520 ret = oldconstraintExpr_makeTermExprNode (e);
524 t = exprData_getUopNode (data);
525 ret = constraintExpr_makeExprNode (t);
529 t = exprData_getUopNode (data);
530 tok = exprData_getUopTok (data);
531 if (lltok_isIncOp (tok))
534 temp = constraintExpr_makeExprNode(t);
535 ret = constraintExpr_makeIncConstraintExpr(temp);
537 else if (lltok_isDecOp (tok))
540 temp = constraintExpr_makeExprNode(t);
541 ret = constraintExpr_makeDecConstraintExpr(temp);
544 ret = oldconstraintExpr_makeTermExprNode (e);
548 t = exprData_getUopNode (data);
549 ret = constraintExpr_makeExprNode (t);
552 t = exprData_getCastNode (data);
553 ret = constraintExpr_makeExprNode (t);
556 t = exprData_getPairA(data);
557 ret = constraintExpr_makeExprNode(t);
560 ret = oldconstraintExpr_makeTermExprNode (e);
566 /*@noaccess exprNode@*/
571 /*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e)
573 return oldconstraintExpr_makeTermExprNode(e);
576 static constraintExpr constraintExpr_makeTerm (/*@only@*/ constraintTerm t)
580 ret = constraintExpr_alloc();
582 ret->data = dmalloc (sizeof *(ret->data) );
583 ret->data->term = NULL;
584 ret->data = constraintExprData_termSetTerm (ret->data, t);
586 ret->origType = ctype_undefined;
591 constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
595 ret = constraintExpr_alloc();
597 ret->data = dmalloc (sizeof *(ret->data) );
598 t = constraintTerm_makesRef (s);
599 ret->data = constraintExprData_termSetTerm (ret->data, t);
602 ret->origType = ctype_undefined;
607 /*@special@*/ /*@notnull@*/ static constraintExpr makeUnaryOpGeneric (void) /*@allocates result->data@*/ /*@defines result->kind@*/
610 ret = constraintExpr_alloc();
611 ret->kind = unaryExpr;
612 ret->data = dmalloc ( sizeof *(ret->data) );
613 ret->data->unaryOp.expr = constraintExpr_undefined;
617 /*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_makeUnaryOpConstraintExpr (/*@only@*/ constraintExpr cexpr)
620 ret = makeUnaryOpGeneric();
624 ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
625 ret->data = constraintExprData_unaryExprSetOp (ret->data, UNARYOP_UNDEFINED);
634 /*@only@*/ /*@notnull@*/static constraintExpr constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr, constraintExprUnaryOpKind Op )
637 ret = makeUnaryOpGeneric();
639 ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
640 ret->data = constraintExprData_unaryExprSetOp (ret->data, Op);
643 ret->origType = ctype_undefined;
648 /*@only@*/ /*@notnull@*/
649 static constraintExpr constraintExpr_makeUnaryOpExprNode (/*@exposed@*/ exprNode expr)
653 sub = constraintExpr_makeExprNode (expr);
654 ret = constraintExpr_makeUnaryOpConstraintExpr(sub);
659 /*@only@*/ /*@notnull@*/
660 static constraintExpr constraintExpr_makeMaxSetConstraintExpr (/*@only@*/ constraintExpr c)
663 ret = constraintExpr_makeUnaryOp (c, MAXSET);
668 /*@only@*/ /*@notnull@*/
669 static constraintExpr constraintExpr_makeSRefUnaryOp (/*@temp@*/ /*@observer@*/ sRef s, constraintExprUnaryOpKind op)
674 t = constraintExpr_makeTermsRef (s);
675 ret = constraintExpr_makeUnaryOpConstraintExpr (t);
676 ret->data = constraintExprData_unaryExprSetOp (ret->data, op);
682 constraintExpr constraintExpr_makeSRefMaxRead( sRef s)
684 return (constraintExpr_makeSRefUnaryOp (s, MAXREAD) );
688 constraintExpr constraintExpr_makeSRefMaxset ( sRef s)
690 return (constraintExpr_makeSRefUnaryOp (s, MAXSET) );
694 constraintExpr constraintExpr_parseMakeUnaryOp (lltok op, constraintExpr cexpr)
697 ret = constraintExpr_makeUnaryOpConstraintExpr ( cexpr);
699 switch (lltok_getTok (op))
702 ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXSET);
705 ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
708 llfatalbug (message ("Unhandled operation in constraint: %s", lltok_unparse (op)));
714 constraintExpr constraintExpr_makeMaxSetExpr (/*@exposed@*/ exprNode expr)
717 ret = constraintExpr_makeExprNode (expr);
719 ret = constraintExpr_makeMaxSetConstraintExpr (ret);
721 llassert (ret != NULL);
726 constraintExpr constraintExpr_makeMaxReadExpr (exprNode expr)
729 ret = constraintExpr_makeUnaryOpExprNode(expr);
730 ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
736 /*@unused@*/ static constraintExpr constraintExpr_makeMinSetExpr (/*@exposed@*/ exprNode expr)
739 ret = constraintExpr_makeUnaryOpExprNode(expr);
740 ret->data = constraintExprData_unaryExprSetOp (ret->data, MINSET);
745 /*@unused@*/ static constraintExpr constraintExpr_makeMinReadExpr (/*@exposed@*/ exprNode expr)
748 ret = constraintExpr_makeUnaryOpExprNode(expr);
749 ret->data = constraintExprData_unaryExprSetOp (ret->data, MINREAD);
755 constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode expr)
758 ret = constraintExpr_makeExprNode (expr);
762 /*@only@*/ /*@notnull@*/
763 constraintExpr constraintExpr_makeIntLiteral (long i)
767 ret = constraintExpr_alloc();
769 ret->data = dmalloc (sizeof *(ret->data) );
770 t = constraintTerm_makeIntLiteral (i);
771 ret->data = constraintExprData_termSetTerm (ret->data, t);
774 ret->origType = ctype_undefined;
780 constraintExpr constraintExpr_makeValueInt (int i)
782 return constraintExpr_makeIntLiteral (i);
786 /*@only@*/ /*@notnull@*/
787 /*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
788 /*@allocates result->data @*/ /*@sets result->kind @*/
791 ret = constraintExpr_alloc();
792 ret->kind = binaryexpr;
793 ret->data = dmalloc ( sizeof *(ret->data) );
795 ret->data->binaryOp.expr1 = constraintExpr_undefined;
796 ret->data->binaryOp.expr2 = constraintExpr_undefined;
802 static /*@notnull@*/ /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExpr (/*@only@*/constraintExpr expr1, /*@only@*/ constraintExpr expr2)
807 ret = constraintExpr_makeBinaryOp();
808 ret->data = constraintExprData_binaryExprSetExpr1 (ret->data, expr1);
809 ret->data = constraintExprData_binaryExprSetExpr2 (ret->data, expr2);
810 ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_UNDEFINED);
813 ret->origType = ctype_undefined;
819 constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr expr1, lltok op,/*@only@*/ constraintExpr expr2)
822 ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
824 if (lltok_getTok (op) == TPLUS)
826 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
828 else if (lltok_getTok (op) == TMINUS)
830 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
842 /*@unused@*/ static constraintExpr constraintExpr_makeBinaryOpExprNode (/*@exposed@*/ exprNode expr1, /*@exposed@*/ exprNode expr2)
845 constraintExpr sub1, sub2;
846 sub1 = constraintExpr_makeTermExprNode (expr1);
847 sub2 = constraintExpr_makeTermExprNode (expr2);
848 ret = constraintExpr_makeBinaryOpConstraintExpr(sub1, sub2);
853 static /*@notnull@*/ /*@only@*/
854 constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/ constraintExpr expr, int literal)
857 constraintExpr constExpr;
859 constExpr = constraintExpr_makeIntLiteral (literal);
860 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, constExpr);
861 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
866 constraintExpr constraintExpr_makeDecConstraintExpr (/*@only@*/constraintExpr expr)
871 inc = constraintExpr_makeIntLiteral (1);
872 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
873 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
878 /*@only@*/ constraintExpr constraintExpr_makeSubtractExpr (/*@only@*/ constraintExpr expr, /*@only@*/ constraintExpr addent)
882 DPRINTF ((message ("Making subtract expression") ) );
884 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
885 ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_MINUS);
890 constraintExpr constraintExpr_makeAddExpr (/*@only@*/
891 constraintExpr expr, /*@only@*/
892 constraintExpr addent)
896 DPRINTF ((message ("Doing addTerm simplification") ) );
898 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
899 ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_PLUS);
905 constraintExpr constraintExpr_makeIncConstraintExpr (/*@only@*/ constraintExpr expr)
910 inc = constraintExpr_makeIntLiteral (1);
911 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
912 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
917 static cstring constraintExprUnaryOpKind_print (constraintExprUnaryOpKind op)
922 return message("maxSet");
924 return message("minSet");
926 return message("maxRead");
928 return message("minRead");
931 return message ("<(Unary OP OTHER>");
937 static cstring constraintExprBinaryOpKind_print (constraintExprBinaryOpKind op)
949 return message ("<binary OP Unknown>");
953 bool constraintExpr_similar (constraintExpr expr1, constraintExpr expr2)
955 constraintExprKind kind;
957 llassert (expr1 != NULL);
958 llassert (expr2 != NULL);
959 if (expr1->kind != expr2->kind)
967 return constraintTerm_similar (constraintExprData_termGetTerm(expr1->data),
968 constraintExprData_termGetTerm(expr2->data) );
969 /*@notreached@*/ break;
972 if (constraintExprData_unaryExprGetOp (expr1->data) != constraintExprData_unaryExprGetOp (expr2->data) )
975 return (constraintExpr_similar (
976 constraintExprData_unaryExprGetExpr (expr1->data),
977 constraintExprData_unaryExprGetExpr (expr2->data)
981 if (constraintExprData_binaryExprGetOp (expr1->data) != constraintExprData_binaryExprGetOp (expr2->data) )
984 if (! constraintExpr_similar (constraintExprData_binaryExprGetExpr1 (expr1->data),
985 constraintExprData_binaryExprGetExpr1 (expr2->data)) )
988 if (! constraintExpr_similar (constraintExprData_binaryExprGetExpr2 (expr1->data),
989 constraintExprData_binaryExprGetExpr2 (expr2->data)) )
1004 bool constraintExpr_same (constraintExpr expr1, constraintExpr expr2)
1006 constraintExprKind kind;
1008 llassert (expr1 != NULL);
1009 llassert (expr2 != NULL);
1010 if (expr1->kind != expr2->kind)
1018 return constraintTerm_similar (constraintExprData_termGetTerm(expr1->data),
1019 constraintExprData_termGetTerm(expr2->data) );
1020 /*@notreached@*/ break;
1023 if (constraintExprData_unaryExprGetOp (expr1->data) != constraintExprData_unaryExprGetOp (expr2->data) )
1026 return (constraintExpr_same (
1027 constraintExprData_unaryExprGetExpr (expr1->data),
1028 constraintExprData_unaryExprGetExpr (expr2->data)
1033 if (constraintExprData_binaryExprGetOp (expr1->data) != constraintExprData_binaryExprGetOp (expr2->data) )
1036 if (! constraintExpr_same (constraintExprData_binaryExprGetExpr1 (expr1->data),
1037 constraintExprData_binaryExprGetExpr1 (expr2->data)) )
1040 if (! constraintExpr_same (constraintExprData_binaryExprGetExpr2 (expr1->data),
1041 constraintExprData_binaryExprGetExpr2 (expr2->data)) )
1045 /*@notreached@*/ break;
1057 constraintExpr_search (/*@observer@*/ constraintExpr c,
1058 /*@observer@*/ constraintExpr old)
1061 constraintExprKind kind;
1062 constraintExpr temp;
1064 if (constraintExpr_similar (c, old))
1066 DPRINTF (("Found %q", constraintExpr_unparse (old)));
1070 llassert (constraintExpr_isDefined (c) && constraintExpr_isDefined(old) );
1072 if ( !(constraintExpr_isDefined (c) && constraintExpr_isDefined(old) ) )
1082 temp = constraintExprData_unaryExprGetExpr (c->data);
1083 ret = ret || constraintExpr_search (temp, old);
1087 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1088 ret = ret || constraintExpr_search(temp, old);
1090 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1091 ret = ret || constraintExpr_search(temp, old);
1101 /*@only@*/ constraintExpr constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@temp@*/ constraintExpr old, /*@temp@*/ constraintExpr newExpr )
1103 constraintExprKind kind;
1104 constraintExpr temp;
1107 llassert(constraintExpr_isDefined (newExpr) && (constraintExpr_isDefined (old) && constraintExpr_isDefined(c) ) );
1109 if ( constraintExpr_similar (c, old) )
1112 ctype newType, cType;
1117 ret = constraintExpr_copy (newExpr);
1118 llassert(constraintExpr_isDefined(ret) );
1119 /*drl if newExpr != NULL then ret will != NULL*/
1121 DPRINTF((message ("Replacing %s with %s",
1122 constraintExpr_unparse(old), constraintExpr_unparse(newExpr)
1125 if (constraintExpr_canGetCType(c) && constraintExpr_canGetCType(newExpr) )
1127 cType = constraintExpr_getCType(c);
1128 newType = constraintExpr_getCType(newExpr);
1130 if (ctype_match(cType,newType) )
1132 DPRINTF(( message("constraintExpr_searchandreplace: replacing "
1133 " %s with type %s with %s with type %s",
1134 constraintExpr_print(c), ctype_unparse(cType),
1135 constraintExpr_print(newExpr), ctype_unparse(newType)
1140 ret->origType = cType;
1144 if (constraintExpr_hasMaxSet(c) )
1146 if (constraintExpr_hasTypeChange(c))
1148 DPRINTF(( message("constraintExpr_searchandreplace: encountered "
1149 "MaxSet with changed type %s ",
1150 constraintExpr_print(c) )
1153 /*fix this with a conversation */
1154 ret = constraintExpr_adjustMaxSetForCast(ret, constraintExpr_getOrigType(c));
1157 constraintExpr_free(c);
1169 temp = constraintExprData_unaryExprGetExpr (c->data);
1170 temp = constraintExpr_copy(temp);
1171 temp = constraintExpr_searchandreplace (temp, old, newExpr);
1172 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1176 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1177 temp = constraintExpr_copy(temp);
1178 temp = constraintExpr_searchandreplace (temp, old, newExpr);
1179 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1181 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1182 temp = constraintExpr_copy(temp);
1183 temp = constraintExpr_searchandreplace (temp, old, newExpr);
1184 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1192 /*@notnull@*/ static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ /*@notnull@*/ constraintExpr c)
1194 constraintExprKind kind;
1195 constraintExpr temp;
1204 temp = constraintExprData_unaryExprGetExpr (c->data);
1205 temp = constraintExpr_copy(temp);
1206 temp = constraintExpr_simplify (temp);
1207 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1210 DPRINTF((message("constraintExpr_simplfiyChildren: simplify binary expression: %s",constraintExpr_unparse(c) ) ) );
1211 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1212 temp = constraintExpr_copy(temp);
1213 temp = constraintExpr_simplify (temp);
1215 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1217 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1218 temp = constraintExpr_copy(temp);
1219 temp = constraintExpr_simplify (temp);
1221 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1231 constraintExpr constraintExpr_setFileloc (/*@returned@*/ constraintExpr c, fileloc loc) /*@modifies c @*/
1234 constraintExpr temp;
1236 llassert(c != NULL);
1241 t = constraintExprData_termGetTerm (c->data);
1242 t = constraintTerm_copy(t);
1243 t = constraintTerm_setFileloc (t, loc);
1244 c->data = constraintExprData_termSetTerm (c->data, t);
1248 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1249 temp = constraintExpr_copy(temp);
1250 temp = constraintExpr_setFileloc (temp, loc);
1251 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1253 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1254 temp = constraintExpr_copy(temp);
1255 temp = constraintExpr_setFileloc (temp, loc);
1256 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1259 temp = constraintExprData_unaryExprGetExpr (c->data);
1260 temp = constraintExpr_copy(temp);
1261 temp = constraintExpr_setFileloc (temp, loc);
1262 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1268 static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/ /*@notnull@*/ constraintExpr c)
1270 constraintExpr e1, e2;
1271 constraintExprBinaryOpKind op;
1273 e1 = constraintExprData_binaryExprGetExpr1 (c->data);
1274 e2 = constraintExprData_binaryExprGetExpr2 (c->data);
1276 if (constraintExpr_canGetValue (e1) && constraintExpr_canGetValue(e2) )
1280 i = constraintExpr_getValue(e1) + constraintExpr_getValue (e2);
1281 constraintExpr_free(c);
1282 c = constraintExpr_makeIntLiteral (i);
1286 op = constraintExprData_binaryExprGetOp (c->data);
1287 if (op == BINARYOP_MINUS)
1288 if (constraintExpr_similar(e1, e2) )
1290 constraintExpr_free(c);
1291 c = constraintExpr_makeIntLiteral (0);
1299 this thing takes the lexpr and expr of a constraint and modifies lexpr
1300 and returns a (possiblly new) value for expr
1302 /* 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 */
1304 /* the approach is a little Kludgy but seems to work. I should probably use something cleaner at some point ... */
1307 /*@only@*/ constraintExpr constraintExpr_solveBinaryExpr (constraintExpr lexpr, /*@only@*/ constraintExpr expr)
1309 constraintExpr expr1, expr2;
1310 constraintExprBinaryOpKind op;
1312 llassert(constraintExpr_isDefined (lexpr) && constraintExpr_isDefined (expr) );
1314 if (lexpr->kind != binaryexpr)
1317 expr2 = constraintExprData_binaryExprGetExpr2 (lexpr->data);
1318 expr1 = constraintExprData_binaryExprGetExpr1 (lexpr->data);
1320 op = constraintExprData_binaryExprGetOp (lexpr->data);
1322 expr1 = constraintExpr_copy(expr1);
1323 expr2 = constraintExpr_copy(expr2);
1325 llassert(constraintExpr_isDefined (expr1) && constraintExpr_isDefined (expr2) );
1327 /* drl possible problem : warning make sure this works */
1329 lexpr->kind = expr1->kind;
1330 sfree (lexpr->data);
1332 lexpr->data = copyExprData (expr1->data, expr1->kind);
1333 constraintExpr_free(expr1);
1335 if (op == BINARYOP_PLUS)
1336 expr = constraintExpr_makeSubtractExpr (expr, expr2);
1337 else if (op == BINARYOP_MINUS)
1338 expr = constraintExpr_makeAddExpr (expr, expr2);
1346 #warning this needs to be checked
1347 expr = constraintExpr_solveBinaryExpr (expr1, expr);
1349 expr = constraintExpr_solveBinaryExpr (expr2, expr);
1354 static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ constraintExpr c)
1358 llassert(constraintExpr_isDefined (c) );
1359 llassert (c->kind == unaryExpr);
1361 DPRINTF ((message ("Doing constraintExpr_simplifyunaryExpr:%s", constraintExpr_unparse (c) ) ) );
1363 if ((constraintExprData_unaryExprGetOp (c->data) != MAXSET) &&
1364 (constraintExprData_unaryExprGetOp (c->data) != MAXREAD) )
1369 exp = constraintExprData_unaryExprGetExpr (c->data);
1370 exp = constraintExpr_copy(exp);
1372 llassert(constraintExpr_isDefined (exp) );
1374 if (exp->kind == term)
1376 constraintTerm cterm;
1378 cterm = constraintExprData_termGetTerm (exp->data);
1380 if (constraintTerm_isStringLiteral(cterm) )
1383 val = constraintTerm_getStringLiteral (cterm);
1384 if (constraintExprData_unaryExprGetOp (c->data) == MAXSET)
1386 constraintExpr temp;
1388 temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
1390 constraintExpr_free(c);
1391 constraintExpr_free(exp);
1396 if (constraintExprData_unaryExprGetOp (c->data) == MAXREAD)
1398 constraintExpr temp;
1400 temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
1402 constraintExpr_free(c);
1403 constraintExpr_free(exp);
1410 /* slight Kludge to hanlde var [] = { , , };
1411 ** type syntax I don't think this is sounds but it should be good
1412 ** enough. The C stanrad is very confusing about initialization
1416 if (constraintTerm_isInitBlock(cterm) )
1418 constraintExpr temp;
1421 len = constraintTerm_getInitBlockLength(cterm);
1423 temp = constraintExpr_makeIntLiteral (len );
1425 constraintExpr_free(c);
1426 DPRINTF(( message("Changed too %q", constraintExpr_print(temp)
1428 constraintExpr_free(exp);
1432 constraintExpr_free(exp);
1436 if (exp->kind != binaryexpr)
1438 constraintExpr_free(exp);
1442 if (constraintExprData_binaryExprGetOp (exp->data) == BINARYOP_PLUS )
1445 /* if (constraintExpr_canGetValue (constraintExprData_binaryExprGetExpr2 (exp->data) ) ) */
1448 constraintExpr temp, temp2;
1450 DPRINTF ((message ("Doing fancy simplification") ) );
1452 temp = constraintExprData_binaryExprGetExpr2 (exp->data);
1454 temp2 = constraintExprData_binaryExprGetExpr1 (exp->data);
1456 temp2 = constraintExpr_copy(temp2);
1457 c->data = constraintExprData_unaryExprSetExpr (c->data, temp2);
1460 temp = constraintExpr_copy (temp);
1462 c = constraintExpr_makeSubtractExpr (c, temp);
1464 DPRINTF ((message ("Done fancy simplification:%s", constraintExpr_unparse (c) ) ) );
1468 DPRINTF ((message ("constraintExpr_simplifyUnaryExpr: Done simplification:%s", constraintExpr_unparse (c) ) ) );
1470 constraintExpr_free(exp);
1475 /*@only@*/ constraintExpr constraintExpr_simplify (/*@only@*/ constraintExpr c)
1477 constraintExprKind kind;
1481 DPRINTF ((message ("Doing constraintExpr_simplify:%s", constraintExpr_unparse (c) ) ) );
1485 llassert ( constraintExpr_isDefined (c) );
1486 if (constraintExpr_isUndefined (c) )
1488 return constraintExpr_undefined;
1491 ret = constraintExpr_copy(c);
1492 llassert(constraintExpr_isDefined (ret) );
1494 constraintExpr_free(c);
1496 ret = constraintExpr_simplifyChildren (ret);
1498 ret = constraintExpr_combineConstants (ret);
1500 ret = constraintExpr_simplifyChildren (ret);
1508 t = constraintExprData_termGetTerm (ret->data);
1509 t = constraintTerm_copy(t);
1510 t = constraintTerm_simplify (t);
1511 ret->data = constraintExprData_termSetTerm (ret->data, t);
1514 ret = constraintExpr_simplifyunaryExpr (ret);
1517 ret = constraintExpr_simplifybinaryExpr (ret);
1523 DPRINTF ((message ("constraintExpr_simplify returning :%s", constraintExpr_unparse (ret) ) ) );
1529 cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@*/
1532 constraintExprKind kind;
1534 llassert (ex != NULL);
1542 if (context_getFlag (FLG_PARENCONSTRAINT) )
1544 st = message ("(%q) ", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
1548 st = message ("%q", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
1552 st = message ("%q(%q)",
1553 constraintExprUnaryOpKind_print (constraintExprData_unaryExprGetOp (ex->data) ),
1554 constraintExpr_unparse (constraintExprData_unaryExprGetExpr (ex->data) )
1558 if (context_getFlag (FLG_PARENCONSTRAINT) )
1560 st = message ("(%q) %q (%q)",
1561 constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
1562 constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
1564 constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
1569 st = message ("%q %q %q",
1570 constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
1571 constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
1573 constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
1580 st = message ("error");
1584 DPRINTF((message ("constraintExpr_unparse: '%s'",st) ) );
1588 constraintExpr constraintExpr_doSRefFixBaseParam (/*@returned@*/ constraintExpr expr, exprNodeList arglist)
1590 constraintTerm Term;
1591 constraintExprKind kind;
1592 constraintExpr expr1, expr2;
1593 constraintExprData data;
1594 llassert (expr != NULL);
1603 Term = constraintExprData_termGetTerm(data);
1604 Term = constraintTerm_copy(Term);
1606 Term = constraintTerm_doSRefFixBaseParam (Term, arglist);
1607 data = constraintExprData_termSetTerm(data, Term);
1610 expr1 = constraintExprData_unaryExprGetExpr (data);
1611 expr1 = constraintExpr_copy(expr1);
1613 expr1 = constraintExpr_doSRefFixBaseParam (expr1, arglist);
1614 data = constraintExprData_unaryExprSetExpr (data, expr1);
1617 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1618 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1620 expr1 = constraintExpr_copy(expr1);
1621 expr2 = constraintExpr_copy(expr2);
1623 expr1 = constraintExpr_doSRefFixBaseParam (expr1, arglist);
1624 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1625 expr2 = constraintExpr_doSRefFixBaseParam (expr2, arglist);
1626 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1637 / *@only@* / constraintExpr constraintExpr_doSRefFixInvarConstraint (/ *@only@* / constraintExpr expr, sRef s, ctype ct)
1639 constraintExprKind kind;
1640 constraintExpr expr1, expr2;
1641 constraintExprData data;
1642 llassert (expr != NULL);
1651 expr = doSRefFixInvarConstraintTerm (expr, s, ct);
1654 expr1 = constraintExprData_unaryExprGetExpr (data);
1655 expr1 = constraintExpr_copy(expr1);
1656 expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
1657 data = constraintExprData_unaryExprSetExpr (data, expr1);
1660 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1661 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1663 expr1 = constraintExpr_copy(expr1);
1664 expr2 = constraintExpr_copy(expr2);
1666 expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
1667 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1668 expr2 = constraintExpr_doSRefFixInvarConstraint (expr2, s, ct);
1669 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1680 /*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@only@*/ constraintExpr expr, exprNodeList arglist) /*@modifies expr@*/
1682 constraintExprKind kind;
1683 constraintExpr expr1, expr2;
1684 constraintExprData data;
1685 llassert (expr != NULL);
1694 expr = doSRefFixConstraintParamTerm (expr, arglist);
1697 expr1 = constraintExprData_unaryExprGetExpr (data);
1698 expr1 = constraintExpr_copy(expr1);
1699 expr1 = constraintExpr_doSRefFixConstraintParam (expr1, arglist);
1700 data = constraintExprData_unaryExprSetExpr (data, expr1);
1703 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1704 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1706 expr1 = constraintExpr_copy(expr1);
1707 expr2 = constraintExpr_copy(expr2);
1709 expr1 = constraintExpr_doSRefFixConstraintParam (expr1, arglist);
1710 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1711 expr2 = constraintExpr_doSRefFixConstraintParam (expr2, arglist);
1712 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1722 /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/ constraintExpr expr, /*@observer@*/ exprNode fcnCall)
1724 constraintExprKind kind;
1725 constraintExpr expr1, expr2;
1726 constraintExprData data;
1727 llassert (expr != NULL);
1736 expr = doFixResultTerm (expr, fcnCall);
1739 expr1 = constraintExprData_unaryExprGetExpr (data);
1740 expr1 = constraintExpr_copy(expr1);
1742 expr1 = constraintExpr_doFixResult (expr1, fcnCall);
1743 data = constraintExprData_unaryExprSetExpr (data, expr1);
1746 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1747 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1749 expr1 = constraintExpr_copy(expr1);
1750 expr2 = constraintExpr_copy(expr2);
1752 expr1 = constraintExpr_doFixResult (expr1, fcnCall);
1753 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1754 expr2 = constraintExpr_doFixResult (expr2, fcnCall);
1755 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1765 cstring constraintExpr_print (constraintExpr expr) /*@*/
1767 return constraintExpr_unparse (expr);
1770 bool constraintExpr_hasMaxSet (constraintExpr expr) /*@*/
1774 t = constraintExpr_unparse(expr);
1776 if (cstring_containsLit(t, "maxSet") != NULL )
1790 /*returns 1 0 -1 like strcmp
1796 int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2)
1798 long value1, value2;
1800 if (constraintExpr_similar (expr1, expr2) )
1805 value1 = constraintExpr_getValue(expr1);
1806 value2 = constraintExpr_getValue(expr2);
1808 if (value1 > value2)
1811 if (value1 == value2)
1818 long constraintExpr_getValue (constraintExpr expr)
1820 llassert (constraintExpr_isDefined(expr) );
1821 llassert (expr->kind == term);
1823 return (constraintTerm_getValue (constraintExprData_termGetTerm (expr->data)));
1826 bool constraintExpr_canGetValue (constraintExpr expr)
1828 llassert ( constraintExpr_isDefined (expr) );
1829 if (constraintExpr_isUndefined (expr) )
1837 return constraintTerm_canGetValue (constraintExprData_termGetTerm (expr->data) );
1846 fileloc constraintExpr_getFileloc (constraintExpr expr)
1850 constraintExprKind kind;
1852 llassert ( constraintExpr_isDefined (expr) );
1853 if (constraintExpr_isUndefined (expr) )
1855 return fileloc_undefined;
1864 t = constraintExprData_termGetTerm (expr->data);
1865 return (constraintTerm_getFileloc (t) );
1869 e = constraintExprData_unaryExprGetExpr (expr->data);
1870 return (constraintExpr_getFileloc (e) );
1874 e = constraintExprData_binaryExprGetExpr1 (expr->data);
1875 return (constraintExpr_getFileloc (e) );
1880 return (fileloc_undefined);
1883 /*drl moved from constriantTerm.c 5/20/001*/
1884 static /*@only@*/ constraintExpr
1885 doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall)
1889 constraintExprData data;
1890 constraintExprKind kind;
1893 llassert (constraintExpr_isDefined (e) );
1898 llassert (kind == term);
1900 t = constraintExprData_termGetTerm (data);
1901 llassert (constraintTerm_isDefined (t));
1905 switch (constraintTerm_getKind (t))
1908 case CTT_INTLITERAL:
1912 s = constraintTerm_getSRef(t);
1913 if (sRef_isResult (s))
1915 ret = constraintExpr_makeExprNode(fcnCall);
1916 constraintExpr_free(e);
1934 /*to be used for structure checking */
1936 / *@only@* / static constraintExpr
1937 doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
1942 constraintExprData data = e->data;
1944 constraintExprKind kind = e->kind;
1948 llassert(kind == term);
1950 t = constraintExprData_termGetTerm (data);
1951 llassert (constraintTerm_isDefined(t) );
1955 DPRINTF (("Fixing: %s", constraintExpr_print (e)));
1957 switch (constraintTerm_getKind(t))
1960 DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
1961 fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
1963 case CTT_INTLITERAL:
1964 DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
1968 / * evans 2001-07-24: constants should use the original term * /
1969 if (!constraintTerm_canGetValue (t))
1972 DPRINTF ((message("Doing sRef_fixInvarConstraint for %q ",
1973 constraintTerm_unparse (t) ) ));
1975 snew = fixSref (ct, s, constraintTerm_getSRef(t));
1977 ret = constraintExpr_makeTermsRef(snew);
1979 constraintExpr_free (e);
1981 DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
1982 constraintExpr_print (ret) ) ));
1983 / *@-branchstate@* /
1984 } / *@=branchstate@* /
1996 /*drl moved from constriantTerm.c 5/20/001*/
1997 /*@only@*/ static constraintExpr
1998 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
2002 constraintExprData data;
2004 constraintExprKind kind;
2009 llassert(constraintExpr_isDefined (e) );
2017 llassert(kind == term);
2019 t = constraintExprData_termGetTerm (data);
2020 llassert (constraintTerm_isDefined(t) );
2024 DPRINTF (("Fixing: %s", constraintExpr_print (e)));
2026 switch (constraintTerm_getKind(t))
2029 DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
2030 fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
2032 case CTT_INTLITERAL:
2033 DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
2036 /* evans 2001-07-24: constants should use the original term */
2037 if (!constraintTerm_canGetValue (t))
2039 DPRINTF ((message("Doing sRef_fixConstraintParam for %q ",
2040 constraintTerm_unparse (t) ) ));
2041 ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
2043 constraintExpr_free (e);
2045 DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
2046 constraintExpr_print (ret) ) ));
2048 } /*@=branchstate@*/
2061 bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term)
2063 if (constraintTerm_hasTerm (expr->term, term) )
2066 if ((expr->expr) != NULL)
2068 return ( constraintExpr_includesTerm (expr->expr, term) );
2075 /*drl added 6/11/01 */
2076 bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c)
2079 llassert(constraintExpr_isDefined (c) );
2081 if ( ! (constraintExpr_isDefined (c) ) )
2084 if (c->kind == binaryexpr)
2091 /*drl added 8/08/001 */
2092 bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
2094 llassert(constraintExpr_isDefined (c) );
2096 if (c->kind == term)
2103 /*@observer@*/ /*@temp@*/ constraintTerm constraintExpr_getTerm ( /*@temp@*/ /*@observer@*/ constraintExpr c) /*@*/
2105 constraintTerm term;
2107 llassert(constraintExpr_isDefined (c) );
2109 llassert(constraintExpr_isTerm(c) );
2111 term = constraintExprData_termGetTerm(c->data);
2116 static void binaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
2118 constraintExpr expr1;
2119 constraintExprBinaryOpKind binaryOp;
2120 constraintExpr expr2;
2123 binaryOp = constraintExprData_binaryExprGetOp (data);
2125 fprintf(f, "%d\n", (int) binaryOp);
2127 expr1 = constraintExprData_binaryExprGetExpr1 (data);
2128 expr2 = constraintExprData_binaryExprGetExpr2 (data);
2132 constraintExpr_dump(expr1, f);
2135 constraintExpr_dump(expr2, f);
2139 static constraintExpr binaryExpr_undump (FILE *f)
2141 constraintExpr expr1;
2142 constraintExprBinaryOpKind binaryOp;
2143 constraintExpr expr2;
2152 os = mstring_create (MAX_DUMP_LINE_LENGTH);
2154 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2156 if (! mstring_isDefined(str) )
2158 llfatalbug(message("Library file is corrupted") );
2161 binaryOp = (constraintExprBinaryOpKind) reader_getInt(&str);
2163 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2165 if (! mstring_isDefined(str) )
2167 llfatalbug(message("Library file is corrupted") );
2170 reader_checkChar (&str, 'e');
2171 reader_checkChar (&str, '1');
2173 expr1 = constraintExpr_undump (f);
2175 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2177 reader_checkChar (&str, 'e');
2178 reader_checkChar (&str, '2');
2180 expr2 = constraintExpr_undump (f);
2182 ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
2183 ret->data = constraintExprData_binaryExprSetOp(ret->data, binaryOp);
2191 static void unaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
2194 constraintExpr expr;
2195 constraintExprUnaryOpKind unaryOp;
2197 unaryOp = constraintExprData_unaryExprGetOp (data);
2199 fprintf(f, "%d\n", (int) unaryOp);
2201 expr = constraintExprData_unaryExprGetExpr (data);
2203 constraintExpr_dump(expr, f);
2206 static constraintExpr unaryExpr_undump ( FILE *f)
2209 constraintExpr expr;
2210 constraintExprUnaryOpKind unaryOp;
2216 str = mstring_create (MAX_DUMP_LINE_LENGTH);
2218 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2220 if (! mstring_isDefined(str) )
2222 llfatalbug(message("Library file is corrupted") );
2225 unaryOp = (constraintExprUnaryOpKind) reader_getInt(&str);
2227 expr = constraintExpr_undump (f);
2229 ret = constraintExpr_makeUnaryOp (expr, unaryOp);
2236 void constraintExpr_dump (/*@observer@*/ constraintExpr expr, FILE *f)
2238 constraintExprKind kind;
2242 llassert(constraintExpr_isDefined(expr) );
2244 DPRINTF((message("constraintExpr_dump:: dumping constraintExpr %s",
2245 constraintExpr_unparse(expr)
2250 fprintf(f,"%d\n", (int) kind);
2255 t = constraintExprData_termGetTerm (expr->data);
2256 constraintTerm_dump (t, f);
2259 unaryExpr_dump (expr->data, f);
2262 binaryExpr_dump (expr->data, f);
2267 /*@only@*/ constraintExpr constraintExpr_undump (FILE *f)
2269 constraintExprKind kind;
2276 s = mstring_create (MAX_DUMP_LINE_LENGTH);
2280 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2282 if (! mstring_isDefined(s) )
2284 llfatalbug(message("Library file is corrupted") );
2287 kind = (constraintExprKind) reader_getInt(&s);
2294 t = constraintTerm_undump (f);
2295 ret = constraintExpr_makeTerm(t);
2298 ret = unaryExpr_undump (f);
2301 ret = binaryExpr_undump (f);
2309 int constraintExpr_getDepth (constraintExpr ex)
2313 constraintExprKind kind;
2315 llassert (ex != NULL);
2325 ret = constraintExpr_getDepth (constraintExprData_unaryExprGetExpr (ex->data) );
2331 ret = constraintExpr_getDepth (constraintExprData_binaryExprGetExpr1 (ex->data) );
2335 ret += constraintExpr_getDepth (constraintExprData_binaryExprGetExpr2 (ex->data) );
2346 bool constraintExpr_canGetCType (constraintExpr e) /*@*/
2348 if (constraintExpr_isUndefined(e) )
2351 if (e->kind == term)
2357 DPRINTF(( message("constraintExpr_canGetCType: can't get type for %s ",
2358 constraintExpr_print(e) ) ));
2363 ctype constraintExpr_getCType (constraintExpr e) /*@*/
2367 llassert(constraintExpr_isDefined(e) );
2369 llassert(constraintExpr_canGetCType(e) );
2374 t = constraintExprData_termGetTerm (e->data);
2375 return (constraintTerm_getCType(t) );
2376 /* assume that a unary expression will be an int ... */
2378 return ctype_signedintegral;
2380 /* drl for just return type of first operand */
2383 constraintExpr_getCType
2384 (constraintExprData_binaryExprGetExpr1 (e->data) )
2392 /* drl add 10-5-001 */
2394 static bool constraintExpr_hasTypeChange(constraintExpr e)
2396 llassert(constraintExpr_isDefined(e) );
2397 if (constraintExpr_isDefined((e)) && (e->ct == TRUE) )
2402 if (e->kind == unaryExpr)
2404 if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
2408 ce = constraintExprData_unaryExprGetExpr(e->data);
2410 return (constraintExpr_hasTypeChange(ce) );
2417 /* drl add 10-5-001 */
2419 static ctype constraintExpr_getOrigType (constraintExpr e)
2422 llassert(constraintExpr_isDefined(e) );
2423 llassert(constraintExpr_hasTypeChange(e) );
2431 if (e->kind == unaryExpr)
2433 if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
2437 ce = constraintExprData_unaryExprGetExpr(e->data);
2439 return (constraintExpr_getOrigType(ce) );
2447 /*drl added these around 10/18/001*/
2449 static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e, /*@unused@*/ ctype ct)
2455 /*@access exprNode@*/
2456 static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode(/*@only@*/ constraintExpr e, ctype ct)
2459 exprNode t1, t2, expr;
2463 llassert(constraintExpr_isDefined(e) );
2466 message("constraintTerm_simpleDivTypeExprNode e=%s, ct=%s",
2467 constraintExpr_print(e), ctype_unparse(ct)
2471 t = constraintExprData_termGetTerm(e->data);
2473 expr = constraintTerm_getExprNode(t);
2475 llassert(constraintExpr_isDefined(e) );
2476 llassert(exprNode_isDefined(expr) );
2478 if (expr->kind == XPR_OP)
2482 t1 = exprData_getOpA (data);
2483 t2 = exprData_getOpB (data);
2484 tok = exprData_getOpTok (data);
2485 if (lltok_isMult(tok) )
2487 llassert(exprNode_isDefined(t1) && exprNode_isDefined(t2) );
2488 /*drl 3/2/2003 we know this from the fact that it's a
2489 multiplication operation...*/
2491 if ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
2495 if (t1->kind == XPR_SIZEOFT)
2497 ct2 = qtype_getType (exprData_getType (t1->edata));
2503 tempE = exprData_getSingle (t1->edata);
2505 ct2 = exprNode_getType (tempE);
2507 if (ctype_match (ctype_makePointer(ct2), ct) )
2509 /* this is a bit sloopy but ... */
2510 constraintExpr_free(e);
2511 return constraintExpr_makeExprNode(t2);
2516 else if ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
2520 if (t2->kind == XPR_SIZEOFT)
2522 ct2 = qtype_getType (exprData_getType (t2->edata));
2529 exprTemp = exprData_getSingle (t2->edata);
2531 llassert(exprNode_isDefined(exprTemp) );
2532 eDTemp = exprTemp->edata;
2534 ct2 = qtype_getType (exprData_getType(eDTemp ) );
2537 if (ctype_match (ctype_makePointer(ct2),ct) )
2539 /*a bit of a sloopy way to do this but... */
2540 constraintExpr_free(e);
2541 return constraintExpr_makeExprNode(t1);
2551 return (constraintExpr_div (e, ct) );
2553 /*@noaccess exprNode@*/
2555 static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype ct)
2557 DPRINTF(( (message("simpleDiv got %s ", constraintExpr_unparse(e) ) )
2560 llassert(constraintExpr_isDefined(e) );
2569 t = constraintExprData_termGetTerm(e->data);
2572 if (constraintTerm_isExprNode (t) )
2574 return constraintTerm_simpleDivTypeExprNode(e, ct);
2576 /* search for * size of ct and remove */
2578 return constraintExpr_div (e, ct);
2583 constraintExpr temp;
2585 temp = constraintExprData_binaryExprGetExpr1 (e->data);
2586 temp = constraintExpr_copy(temp);
2587 temp = simpleDivType (temp, ct);
2589 e->data = constraintExprData_binaryExprSetExpr1 (e->data, temp);
2591 temp = constraintExprData_binaryExprGetExpr2 (e->data);
2592 temp = constraintExpr_copy(temp);
2593 temp = simpleDivType (temp, ct);
2594 e->data = constraintExprData_binaryExprSetExpr2 (e->data, temp);
2596 DPRINTF(( (message("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e) ) )
2602 return constraintExpr_div (e, ct);
2609 static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr e, ctype ct)
2612 DPRINTF(( (message("constraintExpr_adjustMaxSetForCast got %s ", constraintExpr_unparse(e) ) )
2615 e = constraintExpr_makeIncConstraintExpr(e);
2617 e = constraintExpr_simplify(e);
2620 e = simpleDivType (e, ct);
2622 e = constraintExpr_makeDecConstraintExpr(e);
2624 e = constraintExpr_simplify(e);
2626 DPRINTF(( (message("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e) ) )
2633 bool constraintExpr_isConstantOnly ( constraintExpr e )
2635 DPRINTF(( (message("constraintExpr_isConstantOnly %s ",
2636 constraintExpr_unparse(e) ) )
2639 llassert(constraintExpr_isDefined(e) );
2647 t = constraintExprData_termGetTerm(e->data);
2650 if (constraintTerm_isConstantOnly (t) )
2662 constraintExpr temp1, temp2;
2664 temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
2666 temp2 = constraintExprData_binaryExprGetExpr2 (e->data);
2668 if (constraintExpr_isConstantOnly(temp1) &&
2669 constraintExpr_isConstantOnly(temp2) )
2681 constraintExpr temp;
2683 temp = constraintExprData_unaryExprGetExpr (e->data );
2685 if (constraintExpr_isConstantOnly(temp) )