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,
62 ctype p_tfrom, ctype p_tto,
65 /*@special@*/ /*@notnull@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
66 /* @allocates result->data @ @sets result->kind @ */ ;
68 void constraintExpr_free (/*@only@*/ constraintExpr expr)
70 if (constraintExpr_isDefined(expr) )
75 constraintExprData_freeUnaryExpr(expr->data);
78 constraintExprData_freeBinaryExpr(expr->data);
81 constraintExprData_freeTerm(expr->data);
92 llcontbug(message("attempted to free null pointer in constraintExpr_free"));
96 bool constraintExpr_isLit (constraintExpr expr)
98 llassert (expr != NULL);
100 if (expr->kind == term)
102 constraintTerm term = constraintExprData_termGetTerm (expr->data);
103 if (constraintTerm_isIntLiteral (term) )
112 static bool isZeroBinaryOp (constraintExpr expr)
116 llassert (expr != NULL); /* evans 2001-07-18 */
118 if (!constraintExpr_isBinaryExpr (expr) )
124 e2 = constraintExprData_binaryExprGetExpr2(expr->data);
126 llassert (e2 != NULL); /* evans 2001-07-18 */
128 if (constraintExpr_isBinaryExpr (e2) )
131 constraintExprBinaryOpKind op;
133 op = constraintExprData_binaryExprGetOp (e2->data);
135 e1 = constraintExprData_binaryExprGetExpr1(e2->data);
137 if (constraintExpr_isLit(e1) )
139 if (constraintExpr_getValue(e1) == 0 )
148 /* change expr + (o - expr) to (expr -expr) */
150 /*@only@*/ /*@notnull@*/ static constraintExpr removeZero (/*@only@*/ /*@returned@*/ constraintExpr expr)
152 constraintExpr expr1, expr2;
156 constraintExprBinaryOpKind op;
158 constraintExprBinaryOpKind tempOp;
160 llassert (expr != NULL); /* evans 2001-07-18 */
162 if (!isZeroBinaryOp(expr) )
166 expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
167 expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
168 op = constraintExprData_binaryExprGetOp(expr->data);
170 llassert( constraintExpr_isBinaryExpr(expr2) );
172 temp = constraintExprData_binaryExprGetExpr2 (expr2->data);
173 temp = constraintExpr_copy (temp);
175 tempOp = constraintExprData_binaryExprGetOp (expr2->data);
177 if (op == BINARYOP_PLUS)
179 else if (op == BINARYOP_MINUS)
181 if (tempOp == BINARYOP_PLUS)
183 else if (tempOp == BINARYOP_MINUS)
191 expr->data = constraintExprData_binaryExprSetExpr2(expr->data, temp);
192 expr->data = constraintExprData_binaryExprSetOp(expr->data, op);
198 /*@only@*//*@notnull@*/ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
199 /*@out@*/ bool * propagate,
200 /*@out@*/ int *literal)
202 constraintExpr expr1;
203 constraintExpr expr2;
204 bool propagate1, propagate2;
205 int literal1, literal2;
206 constraintExprBinaryOpKind op;
218 llassert (expr != NULL);
220 /* we simplify unaryExpr elsewhere */
221 if (expr->kind != binaryexpr)
224 op = constraintExprData_binaryExprGetOp (expr->data);
226 DPRINTF((message("constraintExpr_propagateConstants: binaryexpr: %s", constraintExpr_unparse(expr) ) ) );
228 expr = removeZero(expr);
230 expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
231 expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
233 expr1 = constraintExpr_copy(expr1);
234 expr2 = constraintExpr_copy(expr2);
236 expr1 = constraintExpr_propagateConstants (expr1, &propagate1, &literal1);
237 expr2 = constraintExpr_propagateConstants (expr2, &propagate2, &literal2);
239 expr1 = removeZero(expr1);
240 expr2 = removeZero(expr2);
243 *propagate = propagate1 || propagate2;
245 if (op == BINARYOP_PLUS)
246 *literal = literal1 + literal2;
247 else if (op == BINARYOP_MINUS)
248 *literal = literal1 - literal2;
252 if ( constraintExpr_isLit (expr1) && constraintExpr_isLit (expr2) )
255 t1 = constraintExpr_getValue (expr1);
256 t2 = constraintExpr_getValue (expr2);
257 llassert(*propagate == FALSE);
260 constraintExpr_free (expr);
261 constraintExpr_free (expr1);
262 constraintExpr_free (expr2);
264 if (op == BINARYOP_PLUS )
265 return (constraintExpr_makeIntLiteral ((t1+t2) ));
266 else if (op == BINARYOP_MINUS)
267 return (constraintExpr_makeIntLiteral ((t1-t2) ));
273 if (constraintExpr_isLit (expr1) )
277 *literal += constraintExpr_getValue (expr1);
279 if (op == BINARYOP_PLUS)
281 constraintExpr_free(expr1);
282 constraintExpr_free(expr);
285 else if (op == BINARYOP_MINUS)
290 /* this is an ugly kludge to deal with not
291 having a unary minus operation...*/
293 temp = constraintExpr_makeIntLiteral (0);
294 temp = constraintExpr_makeSubtractExpr (temp, expr2);
296 constraintExpr_free(expr1);
297 constraintExpr_free(expr);
299 llassert (constraintExpr_isDefined(temp) );
304 BADBRANCH; /* evans 2001-07-18 */
308 if (constraintExpr_isLit (expr2) )
312 if ( op == BINARYOP_PLUS )
313 *literal += constraintExpr_getValue (expr2);
314 else if (op == BINARYOP_MINUS)
315 *literal -= constraintExpr_getValue (expr2);
320 constraintExpr_free(expr2);
321 constraintExpr_free(expr);
325 DPRINTF((message("constraintExpr_propagateConstants returning: %s", constraintExpr_unparse(expr) ) ) );
327 expr->data = constraintExprData_binaryExprSetExpr1 (expr->data, expr1);
328 expr->data = constraintExprData_binaryExprSetExpr2 (expr->data, expr2);
330 expr = removeZero(expr);
334 /*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_combineConstants (/*@only@*/ constraintExpr expr ) /*@modifies expr@*/
339 DPRINTF ((message ("Before combine %s", constraintExpr_unparse(expr) ) ) );
340 expr = constraintExpr_propagateConstants (expr, &propagate, &literal);
349 ret = constraintExpr_makeBinaryOpConstraintExprIntLiteral (expr, literal);
353 DPRINTF ((message ("After combine %s", constraintExpr_unparse(expr) ) ) );
355 llassert(constraintExpr_isDefined(expr) );
360 static /*@notnull@*/ constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
363 ret = dmalloc (sizeof (*ret) );
367 ret->origType = ctype_undefined;
371 /*@only@*/ static constraintExprData copyExprData (/*@observer@*/ constraintExprData data, constraintExprKind kind)
373 constraintExprData ret;
374 llassert(constraintExprData_isDefined(data));
379 ret = constraintExprData_copyBinaryExpr(data);
382 ret = constraintExprData_copyUnaryExpr(data);
385 ret = constraintExprData_copyTerm(data);
393 constraintExpr constraintExpr_copy (constraintExpr expr)
396 ret = constraintExpr_alloc ();
399 /*drl 03/02/2003 this shouldn't be used to copy a null
400 expression but handle things cleanly if it is*/
401 llassert (!constraintExpr_isUndefined(expr) );
403 if (constraintExpr_isUndefined(expr) )
405 return constraintExpr_undefined;
408 ret->kind = expr->kind;
410 ret->data = copyExprData (expr->data, expr->kind);
412 ret->origType = expr->origType;
417 /*@only@*/ static constraintExpr oldconstraintExpr_makeTermExprNode ( /*@dependent@*/ exprNode e)
421 ret = constraintExpr_alloc();
423 ret->data = dmalloc (sizeof *(ret->data) );
424 t = constraintTerm_makeExprNode (e);
425 ret->data = constraintExprData_termSetTerm (ret->data, t);
427 ret->origType = ctype_undefined;
432 /*@access exprNode@*/
433 constraintExpr constraintExpr_makeExprNode (exprNode e)
436 constraintExpr ret, ce1, ce2;
441 if (exprNode_isUndefined (e))
443 return constraintExpr_undefined;
451 t = exprData_getSingle (data);
452 while (exprNode_isInParens (t) )
454 t = exprData_getUopNode (t->edata);
456 s = exprNode_getSref (t);
457 if (sRef_isFixedArray(s) )
461 size = (int) sRef_getArraySize(s);
462 ret = constraintExpr_makeIntLiteral (size);
464 else if (exprNode_isStringLiteral (t))
466 cstring str = multiVal_forceString (exprNode_getValue(t));
467 ret = constraintExpr_makeIntLiteral (size_toLong (cstring_length (str) + 1));
471 DPRINTF ((message ("could not determine the size of %s", exprNode_unparse (e) ) ) );
472 ret = oldconstraintExpr_makeTermExprNode (e);
477 DPRINTF ((message ("Examining operation %s", exprNode_unparse (e) ) ) );
478 t1 = exprData_getOpA (data);
479 t2 = exprData_getOpB (data);
480 tok = exprData_getOpTok (data);
482 if (lltok_isPlus_Op (tok) || lltok_isMinus_Op (tok) )
484 ce1 = constraintExpr_makeExprNode (t1);
485 ce2 = constraintExpr_makeExprNode (t2);
486 ret = constraintExpr_parseMakeBinaryOp (ce1, tok, ce2);
490 /* define this block to activate the cheesy heuristic
491 for handling sizeof expressions*/
498 We handle expressions containing sizeof with the rule
499 (sizeof type ) * Expr = Expr
501 This is the total wronge way to do this but...
502 it may be better than nothing
507 else if (lltok_isMult(tok) )
509 if ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
511 ret = constraintExpr_makeExprNode(t2);
513 else if ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
515 ret = constraintExpr_makeExprNode(t1);
519 ret = oldconstraintExpr_makeTermExprNode (e);
525 ret = oldconstraintExpr_makeTermExprNode (e);
529 t = exprData_getUopNode (data);
530 ret = constraintExpr_makeExprNode (t);
534 t = exprData_getUopNode (data);
535 tok = exprData_getUopTok (data);
536 if (lltok_isIncOp (tok))
539 temp = constraintExpr_makeExprNode(t);
540 ret = constraintExpr_makeIncConstraintExpr(temp);
542 else if (lltok_isDecOp (tok))
545 temp = constraintExpr_makeExprNode(t);
546 ret = constraintExpr_makeDecConstraintExpr(temp);
549 ret = oldconstraintExpr_makeTermExprNode (e);
553 t = exprData_getUopNode (data);
554 ret = constraintExpr_makeExprNode (t);
557 t = exprData_getCastNode (data);
558 ret = constraintExpr_makeExprNode (t);
561 t = exprData_getPairA (data);
562 ret = constraintExpr_makeExprNode(t);
565 ret = oldconstraintExpr_makeTermExprNode (e);
571 /*@noaccess exprNode@*/
576 /*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e)
578 return oldconstraintExpr_makeTermExprNode(e);
581 static constraintExpr constraintExpr_makeTerm (/*@only@*/ constraintTerm t)
585 ret = constraintExpr_alloc();
587 ret->data = dmalloc (sizeof *(ret->data) );
588 ret->data->term = NULL;
589 ret->data = constraintExprData_termSetTerm (ret->data, t);
591 ret->origType = ctype_undefined;
596 constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
600 ret = constraintExpr_alloc();
602 ret->data = dmalloc (sizeof *(ret->data) );
603 t = constraintTerm_makesRef (s);
604 ret->data = constraintExprData_termSetTerm (ret->data, t);
607 ret->origType = ctype_undefined;
612 /*@special@*/ /*@notnull@*/ static constraintExpr makeUnaryOpGeneric (void) /*@allocates result->data@*/ /*@defines result->kind@*/
615 ret = constraintExpr_alloc();
616 ret->kind = unaryExpr;
617 ret->data = dmalloc (sizeof *(ret->data));
618 ret->data->unaryOp.expr = constraintExpr_undefined;
622 /*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_makeUnaryOpConstraintExpr (/*@only@*/ constraintExpr cexpr)
625 ret = makeUnaryOpGeneric();
629 ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
630 ret->data = constraintExprData_unaryExprSetOp (ret->data, UNARYOP_UNDEFINED);
639 /*@only@*/ /*@notnull@*/ static constraintExpr
640 constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr, constraintExprUnaryOpKind Op)
643 ret = makeUnaryOpGeneric();
645 ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
646 ret->data = constraintExprData_unaryExprSetOp (ret->data, Op);
649 ret->origType = ctype_undefined;
654 /*@only@*/ /*@notnull@*/
655 static constraintExpr constraintExpr_makeUnaryOpExprNode (/*@exposed@*/ exprNode expr)
659 sub = constraintExpr_makeExprNode (expr);
660 ret = constraintExpr_makeUnaryOpConstraintExpr(sub);
665 /*@only@*/ /*@notnull@*/
666 static constraintExpr constraintExpr_makeMaxSetConstraintExpr (/*@only@*/ constraintExpr c)
669 ret = constraintExpr_makeUnaryOp (c, MAXSET);
674 /*@only@*/ /*@notnull@*/
675 static constraintExpr constraintExpr_makeSRefUnaryOp (/*@temp@*/ /*@observer@*/ sRef s, constraintExprUnaryOpKind op)
680 t = constraintExpr_makeTermsRef (s);
681 ret = constraintExpr_makeUnaryOpConstraintExpr (t);
682 ret->data = constraintExprData_unaryExprSetOp (ret->data, op);
688 constraintExpr constraintExpr_makeSRefMaxRead( sRef s)
690 return (constraintExpr_makeSRefUnaryOp (s, MAXREAD) );
694 constraintExpr constraintExpr_makeSRefMaxset ( sRef s)
696 return (constraintExpr_makeSRefUnaryOp (s, MAXSET) );
700 constraintExpr constraintExpr_parseMakeUnaryOp (lltok op, constraintExpr cexpr)
703 ret = constraintExpr_makeUnaryOpConstraintExpr ( cexpr);
705 switch (lltok_getTok (op))
708 ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXSET);
711 ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
714 llfatalbug (message ("Unhandled operation in constraint: %s", lltok_unparse (op)));
720 constraintExpr constraintExpr_makeMaxSetExpr (/*@exposed@*/ exprNode expr)
723 ret = constraintExpr_makeExprNode (expr);
725 ret = constraintExpr_makeMaxSetConstraintExpr (ret);
727 llassert (ret != NULL);
732 constraintExpr constraintExpr_makeMaxReadExpr (exprNode expr)
735 ret = constraintExpr_makeUnaryOpExprNode(expr);
736 ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
742 /*@unused@*/ static constraintExpr constraintExpr_makeMinSetExpr (/*@exposed@*/ exprNode expr)
745 ret = constraintExpr_makeUnaryOpExprNode(expr);
746 ret->data = constraintExprData_unaryExprSetOp (ret->data, MINSET);
751 /*@unused@*/ static constraintExpr constraintExpr_makeMinReadExpr (/*@exposed@*/ exprNode expr)
754 ret = constraintExpr_makeUnaryOpExprNode(expr);
755 ret->data = constraintExprData_unaryExprSetOp (ret->data, MINREAD);
761 constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode expr)
764 ret = constraintExpr_makeExprNode (expr);
768 /*@only@*/ /*@notnull@*/
769 constraintExpr constraintExpr_makeIntLiteral (long i)
773 ret = constraintExpr_alloc();
775 ret->data = dmalloc (sizeof *(ret->data) );
776 t = constraintTerm_makeIntLiteral (i);
777 ret->data = constraintExprData_termSetTerm (ret->data, t);
780 ret->origType = ctype_undefined;
786 constraintExpr constraintExpr_makeValueInt (int i)
788 return constraintExpr_makeIntLiteral (i);
792 /*@only@*/ /*@notnull@*/
793 /*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
794 /*@allocates result->data @*/ /*@sets result->kind @*/
797 ret = constraintExpr_alloc();
798 ret->kind = binaryexpr;
799 ret->data = dmalloc ( sizeof *(ret->data) );
801 ret->data->binaryOp.expr1 = constraintExpr_undefined;
802 ret->data->binaryOp.expr2 = constraintExpr_undefined;
808 static /*@notnull@*/ /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExpr (/*@only@*/constraintExpr expr1, /*@only@*/ constraintExpr expr2)
813 ret = constraintExpr_makeBinaryOp();
814 ret->data = constraintExprData_binaryExprSetExpr1 (ret->data, expr1);
815 ret->data = constraintExprData_binaryExprSetExpr2 (ret->data, expr2);
816 ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_UNDEFINED);
819 ret->origType = ctype_undefined;
825 constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr expr1, lltok op,/*@only@*/ constraintExpr expr2)
828 ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
830 if (lltok_getTok (op) == TPLUS)
832 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
834 else if (lltok_getTok (op) == TMINUS)
836 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
848 /*@unused@*/ static constraintExpr constraintExpr_makeBinaryOpExprNode (/*@exposed@*/ exprNode expr1, /*@exposed@*/ exprNode expr2)
851 constraintExpr sub1, sub2;
852 sub1 = constraintExpr_makeTermExprNode (expr1);
853 sub2 = constraintExpr_makeTermExprNode (expr2);
854 ret = constraintExpr_makeBinaryOpConstraintExpr(sub1, sub2);
859 static /*@notnull@*/ /*@only@*/
860 constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/ constraintExpr expr, int literal)
863 constraintExpr constExpr;
865 constExpr = constraintExpr_makeIntLiteral (literal);
866 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, constExpr);
867 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
872 constraintExpr constraintExpr_makeDecConstraintExpr (/*@only@*/constraintExpr expr)
877 inc = constraintExpr_makeIntLiteral (1);
878 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
879 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
884 /*@only@*/ constraintExpr constraintExpr_makeSubtractExpr (/*@only@*/ constraintExpr expr, /*@only@*/ constraintExpr addent)
888 DPRINTF ((message ("Making subtract expression") ) );
890 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
891 ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_MINUS);
896 constraintExpr constraintExpr_makeAddExpr (/*@only@*/
897 constraintExpr expr, /*@only@*/
898 constraintExpr addent)
902 DPRINTF ((message ("Doing addTerm simplification") ) );
904 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
905 ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_PLUS);
911 constraintExpr constraintExpr_makeIncConstraintExpr (/*@only@*/ constraintExpr expr)
916 inc = constraintExpr_makeIntLiteral (1);
917 ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
918 ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
923 static cstring constraintExprUnaryOpKind_print (constraintExprUnaryOpKind op)
928 return message("maxSet");
930 return message("minSet");
932 return message("maxRead");
934 return message("minRead");
937 return message ("<(Unary OP OTHER>");
943 static cstring constraintExprBinaryOpKind_print (constraintExprBinaryOpKind op)
955 return message ("<binary OP Unknown>");
959 bool constraintExpr_similar (constraintExpr expr1, constraintExpr expr2)
961 constraintExprKind kind;
963 llassert (expr1 != NULL);
964 llassert (expr2 != NULL);
965 if (expr1->kind != expr2->kind)
973 return constraintTerm_similar (constraintExprData_termGetTerm(expr1->data),
974 constraintExprData_termGetTerm(expr2->data) );
975 /*@notreached@*/ break;
978 if (constraintExprData_unaryExprGetOp (expr1->data) != constraintExprData_unaryExprGetOp (expr2->data) )
981 return (constraintExpr_similar (
982 constraintExprData_unaryExprGetExpr (expr1->data),
983 constraintExprData_unaryExprGetExpr (expr2->data)
987 if (constraintExprData_binaryExprGetOp (expr1->data) != constraintExprData_binaryExprGetOp (expr2->data) )
990 if (! constraintExpr_similar (constraintExprData_binaryExprGetExpr1 (expr1->data),
991 constraintExprData_binaryExprGetExpr1 (expr2->data)) )
994 if (! constraintExpr_similar (constraintExprData_binaryExprGetExpr2 (expr1->data),
995 constraintExprData_binaryExprGetExpr2 (expr2->data)) )
1010 bool constraintExpr_same (constraintExpr expr1, constraintExpr expr2)
1012 constraintExprKind kind;
1014 llassert (expr1 != NULL);
1015 llassert (expr2 != NULL);
1016 if (expr1->kind != expr2->kind)
1024 return constraintTerm_similar (constraintExprData_termGetTerm(expr1->data),
1025 constraintExprData_termGetTerm(expr2->data) );
1026 /*@notreached@*/ break;
1029 if (constraintExprData_unaryExprGetOp (expr1->data) != constraintExprData_unaryExprGetOp (expr2->data) )
1032 return (constraintExpr_same (
1033 constraintExprData_unaryExprGetExpr (expr1->data),
1034 constraintExprData_unaryExprGetExpr (expr2->data)
1039 if (constraintExprData_binaryExprGetOp (expr1->data) != constraintExprData_binaryExprGetOp (expr2->data) )
1042 if (! constraintExpr_same (constraintExprData_binaryExprGetExpr1 (expr1->data),
1043 constraintExprData_binaryExprGetExpr1 (expr2->data)) )
1046 if (! constraintExpr_same (constraintExprData_binaryExprGetExpr2 (expr1->data),
1047 constraintExprData_binaryExprGetExpr2 (expr2->data)) )
1051 /*@notreached@*/ break;
1063 constraintExpr_search (/*@observer@*/ constraintExpr c,
1064 /*@observer@*/ constraintExpr old)
1067 constraintExprKind kind;
1068 constraintExpr temp;
1070 if (constraintExpr_similar (c, old))
1072 DPRINTF (("Found %q", constraintExpr_unparse (old)));
1076 llassert (constraintExpr_isDefined (c) && constraintExpr_isDefined(old) );
1078 if ( !(constraintExpr_isDefined (c) && constraintExpr_isDefined(old) ) )
1088 temp = constraintExprData_unaryExprGetExpr (c->data);
1089 ret = ret || constraintExpr_search (temp, old);
1093 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1094 ret = ret || constraintExpr_search(temp, old);
1096 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1097 ret = ret || constraintExpr_search(temp, old);
1107 /*@only@*/ constraintExpr
1108 constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@temp@*/ constraintExpr old,
1109 /*@temp@*/ constraintExpr newExpr )
1111 constraintExprKind kind;
1112 constraintExpr temp;
1115 llassert (constraintExpr_isDefined (newExpr) && (constraintExpr_isDefined (old) && constraintExpr_isDefined(c) ) );
1117 if (constraintExpr_similar (c, old))
1119 ctype newType = ctype_unknown;
1120 ctype cType = ctype_unknown;
1122 ret = constraintExpr_copy (newExpr);
1123 llassert(constraintExpr_isDefined(ret) );
1124 /*drl if newExpr != NULL then ret will != NULL*/
1126 DPRINTF (("Replacing %s with %s in %s",
1127 constraintExpr_unparse (old), constraintExpr_unparse (newExpr),
1128 constraintExpr_unparse (c)));
1130 if (constraintExpr_canGetCType (c) && constraintExpr_canGetCType (newExpr))
1132 cType = constraintExpr_getCType(c);
1133 newType = constraintExpr_getCType (newExpr);
1135 if (ctype_match (cType,newType))
1137 DPRINTF (("constraintExpr_searchandreplace: replacing "
1138 " %s with type %s with %s with type %s",
1139 constraintExpr_unparse (c), ctype_unparse(cType),
1140 constraintExpr_unparse (newExpr), ctype_unparse(newType)));
1143 ret->origType = cType;
1144 DPRINTF (("Type: %s", ctype_unparse (constraintExpr_getCType (ret))));
1148 if (constraintExpr_hasMaxSet (c))
1150 if (constraintExpr_hasTypeChange (c))
1152 fileloc loc = constraintExpr_loc (c);
1153 DPRINTF (("constraintExpr_searchandreplace: encountered "
1154 "MaxSet with changed type %s ",
1155 constraintExpr_unparse (c)));
1157 if (c->kind == unaryExpr)
1159 constraintExpr ce = constraintExprData_unaryExprGetExpr (c->data);
1160 DPRINTF (("Its a unary! %s / %s",
1161 ctype_unparse (constraintExpr_getCType (ce)),
1162 ctype_unparse (constraintExpr_getOrigType (ce))));
1163 ret = constraintExpr_adjustMaxSetForCast (ret, constraintExpr_getCType (ce),
1164 constraintExpr_getOrigType (ce),
1169 /* fix this with a conversation */
1170 DPRINTF (("Types: %s / %s", ctype_unparse (newType), ctype_unparse (cType)));
1171 ret = constraintExpr_adjustMaxSetForCast (ret, constraintExpr_getCType (c),
1172 constraintExpr_getOrigType(c),
1178 constraintExpr_free (c);
1179 DPRINTF (("ret: %s", constraintExpr_unparse (ret)));
1190 DPRINTF (("Making unary expression!"));
1191 temp = constraintExprData_unaryExprGetExpr (c->data);
1192 temp = constraintExpr_copy (temp);
1193 temp = constraintExpr_searchandreplace (temp, old, newExpr);
1194 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1197 DPRINTF (("Making binary expression!"));
1198 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1199 temp = constraintExpr_copy (temp);
1200 temp = constraintExpr_searchandreplace (temp, old, newExpr);
1201 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1203 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1204 temp = constraintExpr_copy (temp);
1205 temp = constraintExpr_searchandreplace (temp, old, newExpr);
1206 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1212 DPRINTF (("ret: %s", constraintExpr_unparse (c)));
1216 /*@notnull@*/ static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ /*@notnull@*/ constraintExpr c)
1218 constraintExprKind kind;
1219 constraintExpr temp;
1228 temp = constraintExprData_unaryExprGetExpr (c->data);
1229 temp = constraintExpr_copy(temp);
1230 temp = constraintExpr_simplify (temp);
1231 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1234 DPRINTF((message("constraintExpr_simplfiyChildren: simplify binary expression: %s",constraintExpr_unparse(c) ) ) );
1235 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1236 temp = constraintExpr_copy(temp);
1237 temp = constraintExpr_simplify (temp);
1239 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1241 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1242 temp = constraintExpr_copy(temp);
1243 temp = constraintExpr_simplify (temp);
1245 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1255 constraintExpr constraintExpr_setFileloc (/*@returned@*/ constraintExpr c, fileloc loc) /*@modifies c @*/
1258 constraintExpr temp;
1260 llassert(c != NULL);
1265 t = constraintExprData_termGetTerm (c->data);
1266 t = constraintTerm_copy(t);
1267 t = constraintTerm_setFileloc (t, loc);
1268 c->data = constraintExprData_termSetTerm (c->data, t);
1272 temp = constraintExprData_binaryExprGetExpr1 (c->data);
1273 temp = constraintExpr_copy(temp);
1274 temp = constraintExpr_setFileloc (temp, loc);
1275 c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1277 temp = constraintExprData_binaryExprGetExpr2 (c->data);
1278 temp = constraintExpr_copy(temp);
1279 temp = constraintExpr_setFileloc (temp, loc);
1280 c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1283 temp = constraintExprData_unaryExprGetExpr (c->data);
1284 temp = constraintExpr_copy(temp);
1285 temp = constraintExpr_setFileloc (temp, loc);
1286 c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1292 static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/ /*@notnull@*/ constraintExpr c)
1294 constraintExpr e1, e2;
1295 constraintExprBinaryOpKind op;
1297 e1 = constraintExprData_binaryExprGetExpr1 (c->data);
1298 e2 = constraintExprData_binaryExprGetExpr2 (c->data);
1300 if (constraintExpr_canGetValue (e1) && constraintExpr_canGetValue(e2) )
1304 i = constraintExpr_getValue(e1) + constraintExpr_getValue (e2);
1305 constraintExpr_free(c);
1306 c = constraintExpr_makeIntLiteral (i);
1310 op = constraintExprData_binaryExprGetOp (c->data);
1311 if (op == BINARYOP_MINUS)
1312 if (constraintExpr_similar(e1, e2) )
1314 constraintExpr_free(c);
1315 c = constraintExpr_makeIntLiteral (0);
1323 this thing takes the lexpr and expr of a constraint and modifies lexpr
1324 and returns a (possiblly new) value for expr
1326 /* 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 */
1328 /* the approach is a little Kludgy but seems to work. I should probably use something cleaner at some point ... */
1331 /*@only@*/ constraintExpr constraintExpr_solveBinaryExpr (constraintExpr lexpr, /*@only@*/ constraintExpr expr)
1333 constraintExpr expr1, expr2;
1334 constraintExprBinaryOpKind op;
1336 llassert(constraintExpr_isDefined (lexpr) && constraintExpr_isDefined (expr) );
1338 if (lexpr->kind != binaryexpr)
1341 expr2 = constraintExprData_binaryExprGetExpr2 (lexpr->data);
1342 expr1 = constraintExprData_binaryExprGetExpr1 (lexpr->data);
1344 op = constraintExprData_binaryExprGetOp (lexpr->data);
1346 expr1 = constraintExpr_copy(expr1);
1347 expr2 = constraintExpr_copy(expr2);
1349 llassert(constraintExpr_isDefined (expr1) && constraintExpr_isDefined (expr2) );
1351 /* drl possible problem : warning make sure this works */
1353 lexpr->kind = expr1->kind;
1354 sfree (lexpr->data);
1356 lexpr->data = copyExprData (expr1->data, expr1->kind);
1357 constraintExpr_free(expr1);
1359 if (op == BINARYOP_PLUS)
1360 expr = constraintExpr_makeSubtractExpr (expr, expr2);
1361 else if (op == BINARYOP_MINUS)
1362 expr = constraintExpr_makeAddExpr (expr, expr2);
1370 #warning this needs to be checked
1371 expr = constraintExpr_solveBinaryExpr (expr1, expr);
1373 expr = constraintExpr_solveBinaryExpr (expr2, expr);
1378 static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ constraintExpr c)
1382 llassert(constraintExpr_isDefined (c) );
1383 llassert (c->kind == unaryExpr);
1385 DPRINTF ((message ("Doing constraintExpr_simplifyunaryExpr:%s", constraintExpr_unparse (c) ) ) );
1387 if ((constraintExprData_unaryExprGetOp (c->data) != MAXSET) &&
1388 (constraintExprData_unaryExprGetOp (c->data) != MAXREAD) )
1393 exp = constraintExprData_unaryExprGetExpr (c->data);
1394 exp = constraintExpr_copy(exp);
1396 llassert(constraintExpr_isDefined (exp) );
1398 if (exp->kind == term)
1400 constraintTerm cterm;
1402 cterm = constraintExprData_termGetTerm (exp->data);
1404 if (constraintTerm_isStringLiteral(cterm) )
1407 val = constraintTerm_getStringLiteral (cterm);
1408 if (constraintExprData_unaryExprGetOp (c->data) == MAXSET)
1410 constraintExpr temp;
1412 temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
1414 constraintExpr_free(c);
1415 constraintExpr_free(exp);
1420 if (constraintExprData_unaryExprGetOp (c->data) == MAXREAD)
1422 constraintExpr temp;
1424 temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
1426 constraintExpr_free(c);
1427 constraintExpr_free(exp);
1434 /* slight Kludge to handle var [] = { , , };
1435 ** type syntax I don't think this is sound but it should be good
1436 ** enough. The C standard is very confusing about initialization
1440 if (constraintTerm_isInitBlock(cterm) )
1442 constraintExpr temp;
1445 len = constraintTerm_getInitBlockLength(cterm);
1447 /* -- drl 12/08/2003 : decrementing to fix off by one error */
1451 temp = constraintExpr_makeIntLiteral (len );
1453 constraintExpr_free(c);
1454 DPRINTF(( message("Changed to %q", constraintExpr_print(temp)
1456 constraintExpr_free(exp);
1460 constraintExpr_free(exp);
1464 if (exp->kind != binaryexpr)
1466 constraintExpr_free(exp);
1470 if (constraintExprData_binaryExprGetOp (exp->data) == BINARYOP_PLUS )
1473 /* if (constraintExpr_canGetValue (constraintExprData_binaryExprGetExpr2 (exp->data) ) ) */
1476 constraintExpr temp, temp2;
1478 DPRINTF ((message ("Doing fancy simplification") ) );
1480 temp = constraintExprData_binaryExprGetExpr2 (exp->data);
1482 temp2 = constraintExprData_binaryExprGetExpr1 (exp->data);
1484 temp2 = constraintExpr_copy(temp2);
1485 c->data = constraintExprData_unaryExprSetExpr (c->data, temp2);
1488 temp = constraintExpr_copy (temp);
1490 c = constraintExpr_makeSubtractExpr (c, temp);
1492 DPRINTF ((message ("Done fancy simplification:%s", constraintExpr_unparse (c) ) ) );
1496 DPRINTF ((message ("constraintExpr_simplifyUnaryExpr: Done simplification:%s", constraintExpr_unparse (c) ) ) );
1498 constraintExpr_free(exp);
1503 /*@only@*/ constraintExpr constraintExpr_simplify (/*@only@*/ constraintExpr c)
1505 constraintExprKind kind;
1509 DPRINTF ((message ("Doing constraintExpr_simplify:%s", constraintExpr_unparse (c) ) ) );
1513 llassert ( constraintExpr_isDefined (c) );
1514 if (constraintExpr_isUndefined (c) )
1516 return constraintExpr_undefined;
1519 ret = constraintExpr_copy(c);
1520 llassert(constraintExpr_isDefined (ret) );
1522 constraintExpr_free(c);
1524 ret = constraintExpr_simplifyChildren (ret);
1526 ret = constraintExpr_combineConstants (ret);
1528 ret = constraintExpr_simplifyChildren (ret);
1536 t = constraintExprData_termGetTerm (ret->data);
1537 t = constraintTerm_copy(t);
1538 t = constraintTerm_simplify (t);
1539 ret->data = constraintExprData_termSetTerm (ret->data, t);
1542 ret = constraintExpr_simplifyunaryExpr (ret);
1545 ret = constraintExpr_simplifybinaryExpr (ret);
1551 DPRINTF ((message ("constraintExpr_simplify returning :%s", constraintExpr_unparse (ret) ) ) );
1557 cstring constraintExpr_unparse (/*@temp@*/ constraintExpr ex) /*@*/
1560 constraintExprKind kind;
1562 llassert (ex != NULL);
1569 if (context_getFlag (FLG_PARENCONSTRAINT) )
1571 st = message ("(%q) ", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
1575 st = message ("%q", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
1579 st = message ("%q(%q)",
1580 constraintExprUnaryOpKind_print (constraintExprData_unaryExprGetOp (ex->data) ),
1581 constraintExpr_unparse (constraintExprData_unaryExprGetExpr (ex->data) )
1585 if (context_getFlag (FLG_PARENCONSTRAINT) )
1587 st = message ("(%q) %q (%q)",
1588 constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
1589 constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)),
1590 constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
1595 st = message ("%q %q %q",
1596 constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data)),
1597 constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)),
1598 constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data))
1605 st = message ("error");
1609 DPRINTF((message ("constraintExpr_unparse: '%s'",st) ) );
1613 constraintExpr constraintExpr_doSRefFixBaseParam (/*@returned@*/ constraintExpr expr, exprNodeList arglist)
1615 constraintTerm Term;
1616 constraintExprKind kind;
1617 constraintExpr expr1, expr2;
1618 constraintExprData data;
1619 llassert (expr != NULL);
1628 Term = constraintExprData_termGetTerm(data);
1629 Term = constraintTerm_copy(Term);
1631 Term = constraintTerm_doSRefFixBaseParam (Term, arglist);
1632 data = constraintExprData_termSetTerm(data, Term);
1635 expr1 = constraintExprData_unaryExprGetExpr (data);
1636 expr1 = constraintExpr_copy(expr1);
1638 expr1 = constraintExpr_doSRefFixBaseParam (expr1, arglist);
1639 data = constraintExprData_unaryExprSetExpr (data, expr1);
1642 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1643 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1645 expr1 = constraintExpr_copy(expr1);
1646 expr2 = constraintExpr_copy(expr2);
1648 expr1 = constraintExpr_doSRefFixBaseParam (expr1, arglist);
1649 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1650 expr2 = constraintExpr_doSRefFixBaseParam (expr2, arglist);
1651 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1662 / *@only@* / constraintExpr constraintExpr_doSRefFixInvarConstraint (/ *@only@* / constraintExpr expr, sRef s, ctype ct)
1664 constraintExprKind kind;
1665 constraintExpr expr1, expr2;
1666 constraintExprData data;
1667 llassert (expr != NULL);
1676 expr = doSRefFixInvarConstraintTerm (expr, s, ct);
1679 expr1 = constraintExprData_unaryExprGetExpr (data);
1680 expr1 = constraintExpr_copy(expr1);
1681 expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
1682 data = constraintExprData_unaryExprSetExpr (data, expr1);
1685 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1686 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1688 expr1 = constraintExpr_copy(expr1);
1689 expr2 = constraintExpr_copy(expr2);
1691 expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
1692 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1693 expr2 = constraintExpr_doSRefFixInvarConstraint (expr2, s, ct);
1694 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1705 /*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@only@*/ constraintExpr expr, exprNodeList arglist) /*@modifies expr@*/
1707 constraintExprKind kind;
1708 constraintExpr expr1, expr2;
1709 constraintExprData data;
1710 llassert (expr != NULL);
1719 expr = doSRefFixConstraintParamTerm (expr, arglist);
1722 expr1 = constraintExprData_unaryExprGetExpr (data);
1723 expr1 = constraintExpr_copy(expr1);
1724 expr1 = constraintExpr_doSRefFixConstraintParam (expr1, arglist);
1725 data = constraintExprData_unaryExprSetExpr (data, expr1);
1728 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1729 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1731 expr1 = constraintExpr_copy(expr1);
1732 expr2 = constraintExpr_copy(expr2);
1734 expr1 = constraintExpr_doSRefFixConstraintParam (expr1, arglist);
1735 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1736 expr2 = constraintExpr_doSRefFixConstraintParam (expr2, arglist);
1737 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1747 /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/ constraintExpr expr, /*@observer@*/ exprNode fcnCall)
1749 constraintExprKind kind;
1750 constraintExpr expr1, expr2;
1751 constraintExprData data;
1752 llassert (expr != NULL);
1761 expr = doFixResultTerm (expr, fcnCall);
1764 expr1 = constraintExprData_unaryExprGetExpr (data);
1765 expr1 = constraintExpr_copy(expr1);
1767 expr1 = constraintExpr_doFixResult (expr1, fcnCall);
1768 data = constraintExprData_unaryExprSetExpr (data, expr1);
1771 expr1 = constraintExprData_binaryExprGetExpr1 (data);
1772 expr2 = constraintExprData_binaryExprGetExpr2 (data);
1774 expr1 = constraintExpr_copy(expr1);
1775 expr2 = constraintExpr_copy(expr2);
1777 expr1 = constraintExpr_doFixResult (expr1, fcnCall);
1778 data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1779 expr2 = constraintExpr_doFixResult (expr2, fcnCall);
1780 data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1790 cstring constraintExpr_print (constraintExpr expr) /*@*/
1792 return constraintExpr_unparse (expr);
1795 bool constraintExpr_hasMaxSet (constraintExpr expr) /*@*/
1799 t = constraintExpr_unparse(expr);
1801 if (cstring_containsLit(t, "maxSet") != NULL )
1815 /*returns 1 0 -1 like strcmp
1821 int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2)
1823 long value1, value2;
1825 if (constraintExpr_similar (expr1, expr2) )
1830 value1 = constraintExpr_getValue(expr1);
1831 value2 = constraintExpr_getValue(expr2);
1833 if (value1 > value2)
1836 if (value1 == value2)
1843 long constraintExpr_getValue (constraintExpr expr)
1845 llassert (constraintExpr_isDefined(expr) );
1846 llassert (expr->kind == term);
1848 return (constraintTerm_getValue (constraintExprData_termGetTerm (expr->data)));
1851 bool constraintExpr_canGetValue (constraintExpr expr)
1853 llassert ( constraintExpr_isDefined (expr) );
1854 if (constraintExpr_isUndefined (expr) )
1862 return constraintTerm_canGetValue (constraintExprData_termGetTerm (expr->data) );
1871 fileloc constraintExpr_loc (constraintExpr expr)
1875 constraintExprKind kind;
1877 llassert ( constraintExpr_isDefined (expr) );
1878 if (constraintExpr_isUndefined (expr) )
1880 return fileloc_undefined;
1889 t = constraintExprData_termGetTerm (expr->data);
1890 return (constraintTerm_getFileloc (t) );
1894 e = constraintExprData_unaryExprGetExpr (expr->data);
1895 return (constraintExpr_loc (e) );
1899 e = constraintExprData_binaryExprGetExpr1 (expr->data);
1900 return (constraintExpr_loc (e) );
1905 return (fileloc_undefined);
1908 /*drl moved from constriantTerm.c 5/20/001*/
1909 static /*@only@*/ constraintExpr
1910 doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall)
1914 constraintExprData data;
1915 constraintExprKind kind;
1918 llassert (constraintExpr_isDefined (e) );
1923 llassert (kind == term);
1925 t = constraintExprData_termGetTerm (data);
1926 llassert (constraintTerm_isDefined (t));
1930 switch (constraintTerm_getKind (t))
1933 case CTT_INTLITERAL:
1937 s = constraintTerm_getSRef(t);
1938 if (sRef_isResult (s))
1940 ret = constraintExpr_makeExprNode(fcnCall);
1941 constraintExpr_free(e);
1959 /*to be used for structure checking */
1961 / *@only@* / static constraintExpr
1962 doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e, sRef s, ctype ct)
1966 constraintExprData data = e->data;
1968 constraintExprKind kind = e->kind;
1972 llassert(kind == term);
1974 t = constraintExprData_termGetTerm (data);
1975 llassert (constraintTerm_isDefined(t) );
1979 DPRINTF (("Fixing: %s", constraintExpr_print (e)));
1981 switch (constraintTerm_getKind(t))
1984 DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
1985 fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
1987 case CTT_INTLITERAL:
1988 DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
1992 / * evans 2001-07-24: constants should use the original term * /
1993 if (!constraintTerm_canGetValue (t))
1996 DPRINTF ((message("Doing sRef_fixInvarConstraint for %q ",
1997 constraintTerm_unparse (t) ) ));
1999 snew = fixSref (ct, s, constraintTerm_getSRef(t));
2001 ret = constraintExpr_makeTermsRef(snew);
2003 constraintExpr_free (e);
2005 DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
2006 constraintExpr_print (ret) ) ));
2007 / *@-branchstate@* /
2008 } / *@=branchstate@* /
2020 /*drl moved from constriantTerm.c 5/20/001*/
2021 /*@only@*/ static constraintExpr
2022 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
2026 constraintExprData data;
2028 constraintExprKind kind;
2033 llassert(constraintExpr_isDefined (e) );
2041 llassert(kind == term);
2043 t = constraintExprData_termGetTerm (data);
2044 llassert (constraintTerm_isDefined(t) );
2048 DPRINTF (("Fixing: %s", constraintExpr_print (e)));
2050 switch (constraintTerm_getKind(t))
2053 DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
2054 fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
2056 case CTT_INTLITERAL:
2057 DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
2060 /* evans 2001-07-24: constants should use the original term */
2061 if (!constraintTerm_canGetValue (t))
2063 DPRINTF ((message("Doing sRef_fixConstraintParam for %q ",
2064 constraintTerm_unparse (t) ) ));
2065 ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
2067 constraintExpr_free (e);
2069 DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
2070 constraintExpr_print (ret) ) ));
2072 } /*@=branchstate@*/
2085 bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term)
2087 if (constraintTerm_hasTerm (expr->term, term) )
2090 if ((expr->expr) != NULL)
2092 return ( constraintExpr_includesTerm (expr->expr, term) );
2099 /*drl added 6/11/01 */
2100 bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c)
2103 llassert(constraintExpr_isDefined (c) );
2105 if ( ! (constraintExpr_isDefined (c) ) )
2108 if (c->kind == binaryexpr)
2115 /*drl added 8/08/001 */
2116 bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
2118 llassert(constraintExpr_isDefined (c) );
2120 if (c->kind == term)
2127 /*@observer@*/ /*@temp@*/ constraintTerm constraintExpr_getTerm ( /*@temp@*/ /*@observer@*/ constraintExpr c) /*@*/
2129 constraintTerm term;
2131 llassert(constraintExpr_isDefined (c) );
2133 llassert(constraintExpr_isTerm(c) );
2135 term = constraintExprData_termGetTerm(c->data);
2140 static void binaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
2142 constraintExpr expr1;
2143 constraintExprBinaryOpKind binaryOp;
2144 constraintExpr expr2;
2147 binaryOp = constraintExprData_binaryExprGetOp (data);
2149 fprintf(f, "%d\n", (int) binaryOp);
2151 expr1 = constraintExprData_binaryExprGetExpr1 (data);
2152 expr2 = constraintExprData_binaryExprGetExpr2 (data);
2156 constraintExpr_dump(expr1, f);
2159 constraintExpr_dump(expr2, f);
2163 static constraintExpr binaryExpr_undump (FILE *f)
2165 constraintExpr expr1;
2166 constraintExprBinaryOpKind binaryOp;
2167 constraintExpr expr2;
2176 os = mstring_create (MAX_DUMP_LINE_LENGTH);
2178 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2180 if (! mstring_isDefined(str) )
2182 llfatalbug(message("Library file is corrupted") );
2185 binaryOp = (constraintExprBinaryOpKind) reader_getInt(&str);
2187 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2189 if (! mstring_isDefined(str) )
2191 llfatalbug(message("Library file is corrupted") );
2194 reader_checkChar (&str, 'e');
2195 reader_checkChar (&str, '1');
2197 expr1 = constraintExpr_undump (f);
2199 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2201 reader_checkChar (&str, 'e');
2202 reader_checkChar (&str, '2');
2204 expr2 = constraintExpr_undump (f);
2206 ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
2207 ret->data = constraintExprData_binaryExprSetOp(ret->data, binaryOp);
2215 static void unaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
2218 constraintExpr expr;
2219 constraintExprUnaryOpKind unaryOp;
2221 unaryOp = constraintExprData_unaryExprGetOp (data);
2223 fprintf(f, "%d\n", (int) unaryOp);
2225 expr = constraintExprData_unaryExprGetExpr (data);
2227 constraintExpr_dump(expr, f);
2230 static constraintExpr unaryExpr_undump ( FILE *f)
2233 constraintExpr expr;
2234 constraintExprUnaryOpKind unaryOp;
2240 str = mstring_create (MAX_DUMP_LINE_LENGTH);
2242 str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2244 if (! mstring_isDefined(str) )
2246 llfatalbug(message("Library file is corrupted") );
2249 unaryOp = (constraintExprUnaryOpKind) reader_getInt(&str);
2251 expr = constraintExpr_undump (f);
2253 ret = constraintExpr_makeUnaryOp (expr, unaryOp);
2260 void constraintExpr_dump (/*@observer@*/ constraintExpr expr, FILE *f)
2262 constraintExprKind kind;
2266 llassert(constraintExpr_isDefined(expr) );
2268 DPRINTF((message("constraintExpr_dump:: dumping constraintExpr %s",
2269 constraintExpr_unparse(expr)
2274 fprintf(f,"%d\n", (int) kind);
2279 t = constraintExprData_termGetTerm (expr->data);
2280 constraintTerm_dump (t, f);
2283 unaryExpr_dump (expr->data, f);
2286 binaryExpr_dump (expr->data, f);
2291 /*@only@*/ constraintExpr constraintExpr_undump (FILE *f)
2293 constraintExprKind kind;
2300 s = mstring_create (MAX_DUMP_LINE_LENGTH);
2304 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2306 if (! mstring_isDefined(s) )
2308 llfatalbug(message("Library file is corrupted") );
2311 kind = (constraintExprKind) reader_getInt(&s);
2318 t = constraintTerm_undump (f);
2319 ret = constraintExpr_makeTerm(t);
2322 ret = unaryExpr_undump (f);
2325 ret = binaryExpr_undump (f);
2333 int constraintExpr_getDepth (constraintExpr ex)
2337 constraintExprKind kind;
2339 llassert (ex != NULL);
2349 ret = constraintExpr_getDepth (constraintExprData_unaryExprGetExpr (ex->data) );
2355 ret = constraintExpr_getDepth (constraintExprData_binaryExprGetExpr1 (ex->data) );
2359 ret += constraintExpr_getDepth (constraintExprData_binaryExprGetExpr2 (ex->data) );
2370 bool constraintExpr_canGetCType (constraintExpr e) /*@*/
2372 if (constraintExpr_isUndefined(e))
2375 if (e->kind == term)
2381 DPRINTF (("constraintExpr_canGetCType: can't get type for %s", constraintExpr_unparse (e)));
2386 ctype constraintExpr_getCType (constraintExpr e) /*@*/
2390 llassert (constraintExpr_isDefined (e));
2391 llassert (constraintExpr_canGetCType (e));
2396 t = constraintExprData_termGetTerm (e->data);
2397 return (constraintTerm_getCType(t) );
2398 /* assume that a unary expression will be an int ... */
2400 return ctype_unknown; /* was ctype_signedintegral; */
2401 /* drl for just return type of first operand */
2403 return (constraintExpr_getCType (constraintExprData_binaryExprGetExpr1 (e->data)));
2410 /* drl add 10-5-001 */
2412 static bool constraintExpr_hasTypeChange (constraintExpr e)
2414 llassert(constraintExpr_isDefined(e));
2416 if (constraintExpr_isDefined((e)) && (e->ct == TRUE))
2421 if (e->kind == unaryExpr)
2423 if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
2425 constraintExpr ce = constraintExprData_unaryExprGetExpr(e->data);
2426 DPRINTF (("Unary type change: [%x] %s", ce, constraintExpr_unparse (ce)));
2427 DPRINTF (("Types: %s / %s", ctype_unparse (constraintExpr_getCType (ce)),
2428 ctype_unparse (constraintExpr_getOrigType (ce))));
2429 return (constraintExpr_hasTypeChange(ce));
2436 /* drl add 10-5-001 */
2438 static ctype constraintExpr_getOrigType (constraintExpr e)
2440 llassert (constraintExpr_isDefined (e));
2441 llassert (constraintExpr_hasTypeChange (e));
2448 if (e->kind == unaryExpr)
2450 if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
2452 constraintExpr ce = constraintExprData_unaryExprGetExpr (e->data);
2453 return (constraintExpr_getOrigType(ce));
2461 /*drl added these around 10/18/001*/
2463 static /*@only@*/ constraintExpr
2464 constraintExpr_div (/*@only@*/ constraintExpr e, ctype tfrom, ctype tto, fileloc loc)
2466 int sizefrom = ctype_getSize (tfrom);
2467 int sizeto = ctype_getSize (tto);
2469 DPRINTF (("constraintExpr_div: %s", constraintExpr_unparse (e)));
2470 DPRINTF (("Types: %s / %s",
2471 ctype_unparse (tfrom),
2472 ctype_unparse (tto)));
2474 if (sizefrom == -1) {
2475 llbug (message ("constraintExpr_div: type size unknown: %s", ctype_unparse (tfrom)));
2479 llbug (message ("constraintExpr_div: type size unknown: %s", ctype_unparse (tto)));
2482 if (sizeto == sizefrom)
2484 DPRINTF (("Sizes match: %d / %d", sizeto, sizefrom));
2485 ; /* Sizes match, a-ok */
2489 float scale = (float) sizefrom / (float) sizeto;
2495 llassert (e != NULL);
2496 llassert (e->kind == term);
2497 ct = constraintExprData_termGetTerm (e->data);
2498 DPRINTF (("constraint: %s / %s", constraintExpr_unparse (e), constraintTerm_unparse (ct)));
2499 llassert (constraintTerm_canGetValue (ct));
2500 val = constraintTerm_getValue (ct);
2502 DPRINTF (("Scaling constraints by: %ld * %f", val, scale));
2504 fnewval = ((float) val) * scale;
2505 newval = (long) fnewval;
2507 DPRINTF (("Values: %f / %ld", fnewval, newval));
2509 if ((fnewval - (float) newval) > FLT_EPSILON)
2511 voptgenerror (FLG_ALLOCMISMATCH,
2512 message ("Allocated memory is converted to type %s of (size %d), "
2513 "which is not divisible into original allocation of space "
2514 "for %d elements of type %s (size %d)",
2515 ctype_unparse (tto), sizeto,
2516 long_toInt (val), ctype_unparse (tfrom), sizefrom),
2520 constraintTerm_setValue (ct, newval);
2523 DPRINTF (("After div: %s", constraintExpr_unparse (e)));
2528 /*@access exprNode@*/
2529 static /*@only@*/ constraintExpr
2530 constraintTerm_simpleDivTypeExprNode (/*@only@*/ constraintExpr e, ctype tfrom, ctype tto, fileloc loc)
2533 exprNode t1, t2, expr;
2537 llassert (constraintExpr_isDefined(e) );
2539 DPRINTF (("constraintTerm_simpleDivTypeExprNode e=%s [%s => %s]", constraintExpr_print(e),
2540 ctype_unparse(tfrom), ctype_unparse (tto)));
2542 t = constraintExprData_termGetTerm (e->data);
2544 expr = constraintTerm_getExprNode (t);
2546 llassert (constraintExpr_isDefined(e));
2547 llassert (exprNode_isDefined(expr));
2549 if (expr->kind == XPR_OP)
2553 t1 = exprData_getOpA (data);
2554 t2 = exprData_getOpB (data);
2555 tok = exprData_getOpTok (data);
2557 if (lltok_isMult (tok))
2560 ** If the sizeof is first, flip them.
2563 llassert (exprNode_isDefined(t1) && exprNode_isDefined(t2));
2565 if (t2->kind == XPR_SIZEOF || t2->kind == XPR_SIZEOFT)
2572 /*drl 3/2/2003 we know this from the fact that it's a
2573 multiplication operation...*/
2575 if (t1->kind == XPR_SIZEOF || t1->kind == XPR_SIZEOFT)
2579 if (t1->kind == XPR_SIZEOFT)
2581 multype = qtype_getType (exprData_getType (t1->edata));
2585 exprNode tempE = exprData_getSingle (t1->edata);
2586 multype = exprNode_getType (tempE);
2589 DPRINTF (("Here we go sizeof: %s / %s / %s",
2590 ctype_unparse (multype), ctype_unparse (tfrom), ctype_unparse (tto)));
2591 llassert (ctype_isPointer (tfrom));
2593 if (ctype_almostEqual (ctype_makePointer (multype), tto))
2595 /* this is a bit sloopy but ... */
2596 constraintExpr_free (e);
2597 DPRINTF (("Sizeof types match okay!"));
2598 return constraintExpr_makeExprNode (t2);
2602 int sizemul = ctype_getSize (multype);
2603 ctype tobase = ctype_baseArrayPtr (tto);
2604 int sizeto = ctype_getSize (tobase);
2606 DPRINTF (("Types: %s / %s / %s",
2607 ctype_unparse (tfrom), ctype_unparse (tto), ctype_unparse (multype)));
2609 voptgenerror (FLG_ALLOCMISMATCH,
2610 message ("Allocated memory is used as a different type (%s) from the sizeof type (%s)",
2611 ctype_unparse (tobase), ctype_unparse (multype)),
2614 if (sizemul == sizeto)
2616 constraintExpr_free (e);
2617 DPRINTF (("Sizeof types match okay!"));
2618 return constraintExpr_makeExprNode (t2);
2622 /* nothing was here */
2623 DPRINTF (("MISMATCHING TYPES!"));
2624 return (constraintExpr_div (constraintExpr_makeExprNode (t2), multype, tto, loc));
2630 DPRINTF (("NOT A SIZEOF!"));
2636 DPRINTF (("Not a mult: %s", constraintExpr_unparse (e)));
2640 return (constraintExpr_div (e, tfrom, tto, loc));
2642 /*@noaccess exprNode@*/
2644 static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype tfrom, ctype tto, fileloc loc)
2646 DPRINTF (("simpleDiv got %s", constraintExpr_unparse(e)));
2647 DPRINTF (("Types: %s / %s",
2648 ctype_unparse (tfrom),
2649 ctype_unparse (tto)));
2651 llassert (constraintExpr_isDefined(e));
2657 constraintTerm t = constraintExprData_termGetTerm (e->data);
2659 DPRINTF (("Term: %s", constraintTerm_unparse (t)));
2661 if (constraintTerm_isExprNode (t))
2663 return constraintTerm_simpleDivTypeExprNode (e, tfrom, tto, loc);
2665 /* search for * size of ct and remove */
2667 DPRINTF (("Here: %s / %s -> %s", constraintExpr_unparse (e), ctype_unparse (tfrom), ctype_unparse (tto)));
2668 return constraintExpr_div (e, tfrom, tto, loc);
2673 constraintExpr temp;
2675 temp = constraintExprData_binaryExprGetExpr1 (e->data);
2676 temp = constraintExpr_copy(temp);
2677 temp = simpleDivType (temp, tfrom, tto, loc);
2679 e->data = constraintExprData_binaryExprSetExpr1 (e->data, temp);
2681 temp = constraintExprData_binaryExprGetExpr2 (e->data);
2682 temp = constraintExpr_copy(temp);
2683 temp = simpleDivType (temp, tfrom, tto, loc);
2684 e->data = constraintExprData_binaryExprSetExpr2 (e->data, temp);
2686 DPRINTF (("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e)));
2691 return constraintExpr_div (e, tfrom, tto, loc);
2699 static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast (/*@only@*/ constraintExpr e, ctype tfrom,
2700 ctype tto, fileloc loc)
2702 DPRINTF (("constraintExpr_adjustMaxSetForCast got %s [%s => %s]", constraintExpr_unparse(e),
2703 ctype_unparse (tfrom), ctype_unparse (tto)));
2705 e = constraintExpr_makeIncConstraintExpr (e);
2706 e = constraintExpr_simplify (e);
2707 e = simpleDivType (e, tfrom, tto, loc);
2708 e = constraintExpr_makeDecConstraintExpr (e);
2709 e = constraintExpr_simplify (e);
2711 DPRINTF (("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e)));
2716 bool constraintExpr_isConstantOnly (constraintExpr e)
2718 DPRINTF (("constraintExpr_isConstantOnly %s ", constraintExpr_unparse(e)));
2719 llassert (constraintExpr_isDefined(e));
2725 constraintTerm t = constraintExprData_termGetTerm(e->data);
2727 if (constraintTerm_isConstantOnly (t))
2739 constraintExpr temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
2740 constraintExpr temp2 = constraintExprData_binaryExprGetExpr2 (e->data);
2742 if (constraintExpr_isConstantOnly(temp1) &&
2743 constraintExpr_isConstantOnly(temp2) )
2755 constraintExpr temp;
2757 temp = constraintExprData_unaryExprGetExpr (e->data );
2759 if (constraintExpr_isConstantOnly(temp) )