src/constraintExpr.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2003 University of Virginia,
   4 **         Massachusetts Institute of Technology
   5 **
   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.
  10 **
  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.
  15 **
  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.
  19 **
  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
  23 */
  24
  25 /*
  26 ** constraintExpr.c
  27 */
  28
  29 /* #define DEBUGPRINT 1 */
  30
  31 # include "splintMacros.nf"
  32 # include "basic.h"
  33 # include "cgrammar.h"
  34 # include "cgrammar_tokens.h"
  35
  36 # include "exprChecks.h"
  37 # include "exprNodeSList.h"
  38
  39
  40 static ctype constraintExpr_getOrigType (constraintExpr p_e);
  41 static bool constraintExpr_hasTypeChange(constraintExpr p_e) /*@*/;
  42
  43 static /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/constraintExpr p_expr, int p_literal);
  44
  45
  46 /*@only@*/ static constraintExpr
  47 doSRefFixInvarConstraintTerm (/*@only@*/ constraintExpr p_e,
  48                               sRef p_s, ctype p_ct);
  49
  50 /*@only@*/ static constraintExpr
  51 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr p_e, /*@temp@*/ /*@observer@*/ exprNodeList p_arglist) /*@modifies p_e@*/;
  52
  53 static /*@only@*/ constraintExpr
  54 doFixResultTerm (/*@only@*/ constraintExpr p_e, /*@exposed@*/ exprNode p_fcnCall)
  55      /*@modifies p_e@*/;
  56
  57 static   bool  constraintExpr_canGetCType (constraintExpr p_e) /*@*/;
  58
  59 static ctype constraintExpr_getCType (constraintExpr p_e);
  60
  61 static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr p_e, ctype p_ct);
  62
  63 /*@special@*/ /*@notnull@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
  64      /* @allocates result->data @ @sets result->kind @ */ ;
  65
  66 void constraintExpr_free (/*@only@*/ constraintExpr expr)
  67 {
  68   if (constraintExpr_isDefined(expr) )
  69     {
  70       switch (expr->kind)
  71         {
  72         case unaryExpr:
  73           constraintExprData_freeUnaryExpr(expr->data);
  74           break;
  75         case binaryexpr:
  76           constraintExprData_freeBinaryExpr(expr->data);
  77           break;
  78         case term:
  79           constraintExprData_freeTerm(expr->data);
  80           break;
  81         default:
  82           BADEXIT;
  83         }
  84
  85       expr->data = NULL;
  86       free (expr);
  87     }
  88   else
  89     {
  90       llcontbug(message("attempted to free null pointer in constraintExpr_free"));
  91     }
  92 }
  93
  94 bool constraintExpr_isLit (constraintExpr expr)
  95 {
  96   llassert (expr != NULL);
  97
  98   if (expr->kind == term)
  99     {
 100       constraintTerm term = constraintExprData_termGetTerm (expr->data);
 101       if (constraintTerm_isIntLiteral (term) )
 102         {
 103           return TRUE;
 104         }
 105
 106     }
 107   return FALSE;
 108 }
 109
 110 static bool isZeroBinaryOp (constraintExpr expr)
 111 {
 112   constraintExpr e2;
 113
 114   llassert (expr != NULL); /* evans 2001-07-18 */
 115
 116   if (!constraintExpr_isBinaryExpr (expr) )
 117     {
 118       return FALSE;
 119     }
 120
 121
 122   e2 = constraintExprData_binaryExprGetExpr2(expr->data);
 123
 124   llassert (e2 != NULL); /* evans 2001-07-18 */
 125
 126   if (constraintExpr_isBinaryExpr (e2) )
 127     {
 128       constraintExpr e1;
 129       constraintExprBinaryOpKind  op;
 130
 131       op = constraintExprData_binaryExprGetOp (e2->data);
 132
 133       e1 = constraintExprData_binaryExprGetExpr1(e2->data);
 134
 135         if (constraintExpr_isLit(e1) )
 136           {
 137             if (constraintExpr_getValue(e1) == 0 )
 138               {
 139                 return TRUE;
 140               }
 141           }
 142     }
 143   return FALSE;
 144 }
 145
 146 /* change expr + (o - expr) to (expr -expr) */
 147
 148 /*@only@*/ /*@notnull@*/ static constraintExpr removeZero (/*@only@*/ /*@returned@*/ constraintExpr expr)
 149 {
 150   constraintExpr expr1, expr2;
 151
 152   constraintExpr temp;
 153
 154   constraintExprBinaryOpKind  op;
 155
 156   constraintExprBinaryOpKind  tempOp;
 157
 158   llassert (expr != NULL); /* evans 2001-07-18 */
 159
 160   if (!isZeroBinaryOp(expr) )
 161     return expr;
 162
 163
 164   expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
 165   expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
 166   op = constraintExprData_binaryExprGetOp(expr->data);
 167
 168   llassert( constraintExpr_isBinaryExpr(expr2) );
 169
 170   temp = constraintExprData_binaryExprGetExpr2 (expr2->data);
 171   temp = constraintExpr_copy (temp);
 172
 173   tempOp = constraintExprData_binaryExprGetOp (expr2->data);
 174
 175   if (op == BINARYOP_PLUS)
 176     op = tempOp;
 177   else if (op == BINARYOP_MINUS)
 178     {
 179       if (tempOp == BINARYOP_PLUS)
 180         op = BINARYOP_MINUS;
 181       else if (tempOp == BINARYOP_MINUS)
 182         op = BINARYOP_PLUS;
 183       else
 184         BADEXIT;
 185     }
 186   else
 187     BADEXIT;
 188
 189   expr->data = constraintExprData_binaryExprSetExpr2(expr->data, temp);
 190   expr->data = constraintExprData_binaryExprSetOp(expr->data, op);
 191
 192   return expr;
 193 }
 194
 195
 196 /*@only@*//*@notnull@*/  constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
 197                                                 /*@out@*/ bool * propagate,
 198                                                   /*@out@*/ int *literal)
 199 {
 200   constraintExpr expr1;
 201   constraintExpr expr2;
 202   bool propagate1, propagate2;
 203   int literal1, literal2;
 204   constraintExprBinaryOpKind  op;
 205
 206   propagate1 = FALSE;
 207   propagate2 = FALSE;
 208
 209   literal1 = 0;
 210   literal2 = 0;
 211
 212   *propagate = FALSE;
 213   *literal = 0;
 214
 215
 216   llassert (expr != NULL);
 217
 218   /* we simplify unaryExpr elsewhere */
 219   if (expr->kind != binaryexpr)
 220     return expr;
 221
 222   op = constraintExprData_binaryExprGetOp (expr->data);
 223
 224   DPRINTF((message("constraintExpr_propagateConstants: binaryexpr: %s", constraintExpr_unparse(expr) ) ) );
 225
 226   expr = removeZero(expr);
 227
 228   expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
 229   expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
 230
 231   expr1 = constraintExpr_copy(expr1);
 232   expr2 = constraintExpr_copy(expr2);
 233
 234   expr1 = constraintExpr_propagateConstants (expr1, &propagate1, &literal1);
 235   expr2 = constraintExpr_propagateConstants (expr2, &propagate2, &literal2);
 236
 237   expr1 = removeZero(expr1);
 238   expr2 = removeZero(expr2);
 239
 240
 241   *propagate = propagate1 || propagate2;
 242
 243   if (op == BINARYOP_PLUS)
 244     *literal    = literal1 +  literal2;
 245   else   if (op == BINARYOP_MINUS)
 246     *literal    = literal1 -  literal2;
 247   else
 248     BADEXIT;
 249
 250   if ( constraintExpr_isLit (expr1) && constraintExpr_isLit (expr2) )
 251     {
 252       long t1, t2;
 253       t1 = constraintExpr_getValue (expr1);
 254       t2 = constraintExpr_getValue (expr2);
 255       llassert(*propagate == FALSE);
 256       *propagate = FALSE;
 257
 258       constraintExpr_free (expr);
 259       constraintExpr_free (expr1);
 260       constraintExpr_free (expr2);
 261
 262       if (op == BINARYOP_PLUS )
 263         return (constraintExpr_makeIntLiteral ((t1+t2) ));
 264       else if (op ==  BINARYOP_MINUS)
 265         return (constraintExpr_makeIntLiteral ((t1-t2) ));
 266       else
 267         BADEXIT;
 268     }
 269
 270
 271   if (constraintExpr_isLit (expr1) )
 272     {
 273       *propagate = TRUE;
 274
 275       *literal += constraintExpr_getValue (expr1);
 276
 277       if (op == BINARYOP_PLUS)
 278         {
 279           constraintExpr_free(expr1);
 280           constraintExpr_free(expr);
 281           return expr2;
 282         }
 283       else if (op == BINARYOP_MINUS)
 284         {
 285
 286           constraintExpr temp;
 287
 288           /* this is an ugly kludge to deal with not
 289              having a unary minus operation...*/
 290
 291           temp = constraintExpr_makeIntLiteral (0);
 292           temp = constraintExpr_makeSubtractExpr (temp, expr2);
 293
 294           constraintExpr_free(expr1);
 295           constraintExpr_free(expr);
 296
 297           llassert (constraintExpr_isDefined(temp) );
 298           return temp;
 299         }
 300       else
 301         {
 302           BADBRANCH; /* evans 2001-07-18 */
 303         }
 304     }
 305
 306   if (constraintExpr_isLit (expr2) )
 307     {
 308       *propagate = TRUE;
 309
 310       if ( op == BINARYOP_PLUS )
 311         *literal += constraintExpr_getValue (expr2);
 312       else if (op ==  BINARYOP_MINUS)
 313         *literal -= constraintExpr_getValue (expr2);
 314       else
 315         BADEXIT;
 316
 317
 318       constraintExpr_free(expr2);
 319       constraintExpr_free(expr);
 320       return expr1;
 321     }
 322
 323   DPRINTF((message("constraintExpr_propagateConstants returning: %s", constraintExpr_unparse(expr) ) ) );
 324
 325   expr->data = constraintExprData_binaryExprSetExpr1 (expr->data, expr1);
 326   expr->data = constraintExprData_binaryExprSetExpr2 (expr->data, expr2);
 327
 328   expr = removeZero(expr);
 329   return expr;
 330 }
 331
 332 /*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_combineConstants (/*@only@*/ constraintExpr expr ) /*@modifies expr@*/
 333 {
 334   bool propagate;
 335   int literal;
 336
 337   DPRINTF ((message ("Before combine %s", constraintExpr_unparse(expr) ) ) );
 338   expr = constraintExpr_propagateConstants (expr, &propagate, &literal);
 339
 340
 341   if (propagate)
 342     {
 343       constraintExpr ret;
 344
 345       if (literal != 0)
 346         {
 347           ret = constraintExpr_makeBinaryOpConstraintExprIntLiteral (expr, literal);
 348           expr = ret;
 349         }
 350     }
 351    DPRINTF ((message ("After combine %s", constraintExpr_unparse(expr) ) ) );
 352
 353    llassert(constraintExpr_isDefined(expr) );
 354    return expr;
 355 }
 356
 357 /*@special@*/
 358 static /*@notnull@*/ constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
 359 {
 360   constraintExpr ret;
 361   ret = dmalloc (sizeof (*ret) );
 362   ret->kind = term;
 363   ret->data = NULL;
 364   ret->ct = FALSE;
 365   ret->origType = ctype_undefined;
 366   return ret;
 367 }
 368
 369 /*@only@*/ static constraintExprData copyExprData (/*@observer@*/ constraintExprData data, constraintExprKind kind)
 370 {
 371   constraintExprData ret;
 372   llassert(constraintExprData_isDefined(data));
 373
 374   switch (kind)
 375     {
 376     case binaryexpr:
 377       ret = constraintExprData_copyBinaryExpr(data);
 378       break;
 379     case unaryExpr:
 380       ret = constraintExprData_copyUnaryExpr(data);
 381       break;
 382     case term:
 383       ret = constraintExprData_copyTerm(data);
 384       break;
 385     default:
 386       BADEXIT;
 387     }
 388   return ret;
 389 }
 390
 391 constraintExpr constraintExpr_copy (constraintExpr expr)
 392 {
 393   constraintExpr ret;
 394   ret = constraintExpr_alloc ();
 395
 396
 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) );
 400
 401   if (constraintExpr_isUndefined(expr) )
 402     {
 403       return constraintExpr_undefined;
 404     }
 405
 406   ret->kind = expr->kind;
 407
 408   ret->data = copyExprData (expr->data, expr->kind);
 409   ret->ct = expr->ct;
 410   ret->origType = expr->origType;
 411   return ret;
 412 }
 413
 414
 415 /*@only@*/ static constraintExpr oldconstraintExpr_makeTermExprNode ( /*@dependent@*/ exprNode e)
 416 {
 417   constraintExpr ret;
 418   constraintTerm t;
 419   ret = constraintExpr_alloc();
 420   ret->kind = term;
 421   ret->data = dmalloc (sizeof *(ret->data) );
 422   t = constraintTerm_makeExprNode (e);
 423   ret->data = constraintExprData_termSetTerm (ret->data, t);
 424   ret->ct = FALSE;
 425   ret->origType = ctype_undefined;
 426
 427   return ret;
 428 }
 429
 430 /*@access exprNode@*/
 431 constraintExpr constraintExpr_makeExprNode (exprNode e)
 432 {
 433  sRef s;
 434  constraintExpr ret, ce1, ce2;
 435  exprData data;
 436  exprNode t, t1, t2;
 437  lltok tok;
 438
 439  llassert (e != NULL);
 440
 441  data = e->edata;
 442
 443  switch (e->kind)
 444    {
 445    case XPR_SIZEOF:
 446      t = exprData_getSingle (data);
 447      while (exprNode_isInParens (t) )
 448        {
 449          t = exprData_getUopNode (t->edata);
 450        }
 451      s = exprNode_getSref (t);
 452      if (sRef_isFixedArray(s) )
 453       {
 454         int size;
 455
 456         size = (int) sRef_getArraySize(s);
 457         ret = constraintExpr_makeIntLiteral (size);
 458       }
 459      else if (exprNode_isStringLiteral (t))
 460       {
 461         cstring str = multiVal_forceString (exprNode_getValue(t));
 462         ret = constraintExpr_makeIntLiteral (size_toLong (cstring_length (str) + 1));
 463       }
 464      else
 465        {
 466          DPRINTF ((message ("could not determine the size of %s", exprNode_unparse (e) ) ) );
 467          ret = oldconstraintExpr_makeTermExprNode (e);
 468        }
 469      break;
 470
 471    case XPR_OP:
 472       DPRINTF ((message ("Examining operation %s", exprNode_unparse (e) ) ) );
 473      t1 = exprData_getOpA (data);
 474      t2 = exprData_getOpB (data);
 475      tok = exprData_getOpTok (data);
 476
 477      if (lltok_isPlus_Op (tok) || lltok_isMinus_Op (tok) )
 478        {
 479          ce1 = constraintExpr_makeExprNode (t1);
 480          ce2 = constraintExpr_makeExprNode (t2);
 481          ret = constraintExpr_parseMakeBinaryOp (ce1, tok, ce2);
 482        }
 483
 484
 485      /*@i333*/
 486      /* uncomment this block to activate the cheesy heuristic
 487         for handling sizeof expressions
 488
 489      / *
 490        drl 8-11-001
 491
 492        We handle expressions containing sizeof with the rule
 493        (sizeof type ) * Expr = Expr
 494
 495        This is the total wronge way to do this but...
 496        it may be better than nothing
 497      * /
 498
 499
 500
 501      else if (lltok_isMult(tok) )
 502        {
 503          if  ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
 504            {
 505              ret = constraintExpr_makeExprNode(t2);
 506            }
 507          else if  ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
 508            {
 509              ret = constraintExpr_makeExprNode(t1);
 510              }
 511          else
 512            {
 513            ret =  oldconstraintExpr_makeTermExprNode (e);
 514            }
 515        }
 516      */
 517      else
 518         ret = oldconstraintExpr_makeTermExprNode (e);
 519
 520      break;
 521    case XPR_PARENS:
 522      t = exprData_getUopNode (data);
 523      ret = constraintExpr_makeExprNode (t);
 524      break;
 525
 526    case XPR_PREOP:
 527       t = exprData_getUopNode (data);
 528       tok =  exprData_getUopTok (data);
 529       if (lltok_isIncOp (tok))
 530         {
 531           constraintExpr temp;
 532           temp = constraintExpr_makeExprNode(t);
 533           ret = constraintExpr_makeIncConstraintExpr(temp);
 534         }
 535       else if (lltok_isDecOp (tok))
 536         {
 537           constraintExpr temp;
 538           temp = constraintExpr_makeExprNode(t);
 539           ret = constraintExpr_makeDecConstraintExpr(temp);
 540         }
 541       else
 542         ret =  oldconstraintExpr_makeTermExprNode (e);
 543       break;
 544
 545    case XPR_POSTOP:
 546      t = exprData_getUopNode (data);
 547           ret = constraintExpr_makeExprNode (t);
 548      break;
 549    case XPR_CAST:
 550      t = exprData_getCastNode (data);
 551      ret = constraintExpr_makeExprNode (t);
 552      break;
 553    case XPR_COMMA:
 554      t = exprData_getPairA(data);
 555      ret = constraintExpr_makeExprNode(t);
 556      /*@i3434*/ /* drl: I'm not sure if this is right.  I'm adding a break to quiet Splint */
 557      break;
 558    default:
 559      ret = oldconstraintExpr_makeTermExprNode (e);
 560
 561    }
 562   return ret;
 563 }
 564
 565 /*@noaccess exprNode@*/
 566
 567
 568
 569
 570 /*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e)
 571 {
 572   return  oldconstraintExpr_makeTermExprNode(e);
 573 }
 574
 575 static constraintExpr constraintExpr_makeTerm (/*@only@*/  constraintTerm t)
 576 {
 577   constraintExpr ret;
 578
 579   ret = constraintExpr_alloc();
 580   ret->kind = term;
 581   ret->data = dmalloc (sizeof *(ret->data) );
 582   ret->data->term = NULL;
 583   ret->data = constraintExprData_termSetTerm (ret->data, t);
 584   ret->ct = FALSE;
 585   ret->origType = ctype_undefined;
 586
 587   return ret;
 588 }
 589
 590 constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
 591 {
 592   constraintExpr ret;
 593   constraintTerm t;
 594   ret = constraintExpr_alloc();
 595   ret->kind = term;
 596   ret->data = dmalloc (sizeof *(ret->data) );
 597   t = constraintTerm_makesRef (s);
 598   ret->data = constraintExprData_termSetTerm (ret->data, t);
 599
 600   ret->ct = FALSE;
 601   ret->origType = ctype_undefined;
 602
 603   return ret;
 604 }
 605
 606 /*@special@*/ /*@notnull@*/ static constraintExpr makeUnaryOpGeneric (void) /*@allocates result->data@*/ /*@defines result->kind@*/
 607 {
 608   constraintExpr ret;
 609   ret = constraintExpr_alloc();
 610   ret->kind = unaryExpr;
 611   ret->data = dmalloc ( sizeof *(ret->data) );
 612   ret->data->unaryOp.expr = constraintExpr_undefined;
 613   return ret;
 614 }
 615
 616 /*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_makeUnaryOpConstraintExpr (/*@only@*/ constraintExpr cexpr)
 617 {
 618   constraintExpr ret;
 619   ret = makeUnaryOpGeneric();
 620
 621   /*@-uniondef@*/
 622   /*@-compdef@*/
 623   ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
 624   ret->data = constraintExprData_unaryExprSetOp (ret->data, UNARYOP_UNDEFINED);
 625
 626   return ret;
 627
 628   /*@=compdef@*/
 629   /*@=uniondef@*/
 630 }
 631
 632
 633 /*@only@*/ /*@notnull@*/static constraintExpr constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr,   constraintExprUnaryOpKind Op )
 634 {
 635   constraintExpr ret;
 636   ret = makeUnaryOpGeneric();
 637
 638   ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
 639   ret->data = constraintExprData_unaryExprSetOp (ret->data, Op);
 640
 641   ret->ct = FALSE;
 642   ret->origType = ctype_undefined;
 643
 644   return ret;
 645 }
 646
 647 /*@only@*/ /*@notnull@*/
 648 static constraintExpr constraintExpr_makeUnaryOpExprNode (/*@exposed@*/ exprNode expr)
 649 {
 650   constraintExpr ret;
 651   constraintExpr sub;
 652   sub = constraintExpr_makeExprNode (expr);
 653   ret = constraintExpr_makeUnaryOpConstraintExpr(sub);
 654
 655   return ret;
 656 }
 657
 658 /*@only@*/ /*@notnull@*/
 659 static constraintExpr constraintExpr_makeMaxSetConstraintExpr (/*@only@*/ constraintExpr c)
 660 {
 661   constraintExpr ret;
 662   ret = constraintExpr_makeUnaryOp (c, MAXSET);
 663   return ret;
 664 }
 665
 666
 667 /*@only@*/ /*@notnull@*/
 668 static constraintExpr constraintExpr_makeSRefUnaryOp (/*@temp@*/ /*@observer@*/ sRef s,  constraintExprUnaryOpKind op)
 669 {
 670   constraintExpr ret;
 671   constraintExpr t;
 672
 673   t = constraintExpr_makeTermsRef (s);
 674   ret = constraintExpr_makeUnaryOpConstraintExpr (t);
 675   ret->data = constraintExprData_unaryExprSetOp (ret->data, op);
 676
 677   return ret;
 678 }
 679
 680 /*@only@*/
 681 constraintExpr constraintExpr_makeSRefMaxRead( sRef s)
 682 {
 683   return (constraintExpr_makeSRefUnaryOp (s, MAXREAD) );
 684 }
 685
 686 /*@only@*/
 687 constraintExpr constraintExpr_makeSRefMaxset ( sRef s)
 688 {
 689   return (constraintExpr_makeSRefUnaryOp (s, MAXSET) );
 690 }
 691
 692 /*@only@*/
 693 constraintExpr constraintExpr_parseMakeUnaryOp (lltok op, constraintExpr cexpr)
 694 {
 695   constraintExpr ret;
 696   ret = constraintExpr_makeUnaryOpConstraintExpr ( cexpr);
 697
 698   switch (lltok_getTok (op))
 699     {
 700     case QMAXSET:
 701       ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXSET);
 702       break;
 703     case QMAXREAD:
 704       ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
 705       break;
 706     default:
 707       llfatalbug (message ("Unhandled operation in constraint: %s", lltok_unparse (op)));
 708     }
 709   return ret;
 710 }
 711
 712 /*@only@*/
 713 constraintExpr constraintExpr_makeMaxSetExpr (/*@exposed@*/ exprNode expr)
 714 {
 715   constraintExpr ret;
 716   ret = constraintExpr_makeExprNode (expr);
 717
 718   ret = constraintExpr_makeMaxSetConstraintExpr (ret);
 719
 720   llassert (ret != NULL);
 721   return ret;
 722 }
 723
 724 /*@only@*/
 725 constraintExpr  constraintExpr_makeMaxReadExpr (exprNode expr)
 726 {
 727   constraintExpr ret;
 728   ret = constraintExpr_makeUnaryOpExprNode(expr);
 729   ret->data      = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
 730   return ret;
 731 }
 732
 733 # if 0
 734 /*@only@*/
 735 /*@unused@*/ static constraintExpr  constraintExpr_makeMinSetExpr (/*@exposed@*/ exprNode expr)
 736 {
 737   constraintExpr ret;
 738   ret = constraintExpr_makeUnaryOpExprNode(expr);
 739   ret->data      = constraintExprData_unaryExprSetOp (ret->data, MINSET);
 740   return ret;
 741 }
 742
 743 /*@only@*/
 744 /*@unused@*/ static constraintExpr constraintExpr_makeMinReadExpr (/*@exposed@*/ exprNode expr)
 745 {
 746   constraintExpr ret;
 747   ret = constraintExpr_makeUnaryOpExprNode(expr);
 748   ret->data      = constraintExprData_unaryExprSetOp (ret->data, MINREAD);
 749   return ret;
 750 }
 751 # endif
 752
 753 /*@only@*/
 754 constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode expr)
 755 {
 756   constraintExpr ret;
 757   ret = constraintExpr_makeExprNode (expr);
 758   return ret;
 759 }
 760
 761 /*@only@*/ /*@notnull@*/
 762 constraintExpr constraintExpr_makeIntLiteral (long i)
 763 {
 764   constraintExpr ret;
 765   constraintTerm t;
 766   ret = constraintExpr_alloc();
 767   ret->kind = term;
 768   ret->data = dmalloc (sizeof *(ret->data) );
 769   t = constraintTerm_makeIntLiteral (i);
 770   ret->data = constraintExprData_termSetTerm (ret->data, t);
 771
 772   ret->ct = FALSE;
 773   ret->origType = ctype_undefined;
 774
 775   return ret;
 776 }
 777
 778 /*
 779 constraintExpr constraintExpr_makeValueInt (int i)
 780 {
 781   return constraintExpr_makeIntLiteral (i);
 782 }
 783 */
 784
 785 /*@only@*/ /*@notnull@*/
 786  /*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
 787       /*@allocates result->data @*/ /*@sets result->kind @*/
 788 {
 789   constraintExpr ret;
 790   ret = constraintExpr_alloc();
 791   ret->kind = binaryexpr;
 792   ret->data = dmalloc ( sizeof *(ret->data) );
 793
 794   ret->data->binaryOp.expr1 = constraintExpr_undefined;
 795   ret->data->binaryOp.expr2 = constraintExpr_undefined;
 796
 797   return ret;
 798 }
 799
 800
 801 static /*@notnull@*/ /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExpr (/*@only@*/constraintExpr expr1, /*@only@*/ constraintExpr expr2)
 802
 803 {
 804   constraintExpr ret;
 805
 806   ret = constraintExpr_makeBinaryOp();
 807   ret->data = constraintExprData_binaryExprSetExpr1 (ret->data, expr1);
 808   ret->data = constraintExprData_binaryExprSetExpr2 (ret->data, expr2);
 809   ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_UNDEFINED);
 810
 811   ret->ct = FALSE;
 812   ret->origType = ctype_undefined;
 813
 814   return ret;
 815 }
 816
 817 /*@only@*/
 818 constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr expr1, lltok op,/*@only@*/ constraintExpr expr2)
 819 {
 820   constraintExpr ret;
 821   ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
 822
 823   if (lltok_getTok (op) == TPLUS)
 824     {
 825       ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
 826     }
 827   else if (lltok_getTok (op) == TMINUS)
 828     {
 829       ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
 830     }
 831   else
 832     {
 833       llassert (FALSE);
 834     }
 835
 836   return ret;
 837 }
 838
 839 # if 0
 840 /*@only@*/
 841 /*@unused@*/ static constraintExpr constraintExpr_makeBinaryOpExprNode (/*@exposed@*/ exprNode expr1, /*@exposed@*/ exprNode expr2)
 842 {
 843   constraintExpr ret;
 844   constraintExpr sub1, sub2;
 845   sub1 = constraintExpr_makeTermExprNode (expr1);
 846   sub2 = constraintExpr_makeTermExprNode (expr2);
 847   ret = constraintExpr_makeBinaryOpConstraintExpr(sub1, sub2);
 848   return ret;
 849 }
 850 # endif
 851
 852 static /*@notnull@*/ /*@only@*/
 853 constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/ constraintExpr expr, int literal)
 854 {
 855   constraintExpr ret;
 856   constraintExpr constExpr;
 857
 858   constExpr = constraintExpr_makeIntLiteral (literal);
 859   ret = constraintExpr_makeBinaryOpConstraintExpr (expr, constExpr);
 860   ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
 861   return ret;
 862 }
 863
 864 /*@only@*/
 865 constraintExpr constraintExpr_makeDecConstraintExpr (/*@only@*/constraintExpr expr)
 866 {
 867   constraintExpr ret;
 868   constraintExpr inc;
 869
 870   inc = constraintExpr_makeIntLiteral (1);
 871   ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
 872   ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
 873   return ret;
 874 }
 875
 876
 877 /*@only@*/  constraintExpr constraintExpr_makeSubtractExpr (/*@only@*/ constraintExpr expr, /*@only@*/ constraintExpr addent)
 878 {
 879   constraintExpr  ret;
 880
 881   DPRINTF ((message ("Making  subtract expression") ) );
 882
 883   ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
 884   ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_MINUS);
 885   return ret;
 886 }
 887
 888 /*@only@*/
 889 constraintExpr constraintExpr_makeAddExpr (/*@only@*/
 890 constraintExpr expr, /*@only@*/
 891 constraintExpr addent)
 892 {
 893   constraintExpr  ret;
 894
 895   DPRINTF ((message ("Doing addTerm simplification") ) );
 896
 897   ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
 898   ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_PLUS);
 899   return ret;
 900 }
 901
 902
 903 /*@only@*/
 904 constraintExpr constraintExpr_makeIncConstraintExpr (/*@only@*/ constraintExpr expr)
 905 {
 906   constraintExpr ret;
 907   constraintExpr inc;
 908
 909   inc = constraintExpr_makeIntLiteral (1);
 910   ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
 911   ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
 912   return ret;
 913 }
 914
 915 /*@only@*/
 916 static cstring constraintExprUnaryOpKind_print (constraintExprUnaryOpKind op)
 917 {
 918   switch (op)
 919     {
 920     case MAXSET:
 921       return message("maxSet");
 922     case MINSET:
 923       return message("minSet");
 924     case MAXREAD:
 925       return message("maxRead");
 926     case MINREAD:
 927       return message("minRead");
 928     default:
 929       llassert(FALSE);
 930       return message ("<(Unary OP OTHER>");
 931     }
 932 }
 933
 934
 935 /*@only@*/
 936 static cstring constraintExprBinaryOpKind_print (constraintExprBinaryOpKind op)
 937 {
 938
 939   switch (op)
 940     {
 941     case BINARYOP_PLUS:
 942       return message("+");
 943     case BINARYOP_MINUS:
 944       return message("-");
 945
 946     default:
 947       llassert(FALSE);
 948       return message ("<binary OP Unknown>");
 949     }
 950 }
 951
 952 bool constraintExpr_similar (constraintExpr expr1, constraintExpr expr2)
 953 {
 954   constraintExprKind kind;
 955
 956   llassert (expr1 != NULL);
 957   llassert (expr2 != NULL);
 958   if (expr1->kind != expr2->kind)
 959     return FALSE;
 960
 961   kind = expr1->kind;
 962
 963   switch (kind)
 964     {
 965     case term:
 966       return constraintTerm_similar (constraintExprData_termGetTerm(expr1->data),
 967                                   constraintExprData_termGetTerm(expr2->data) );
 968       /*@notreached@*/ break;
 969
 970     case unaryExpr:
 971       if (constraintExprData_unaryExprGetOp (expr1->data) != constraintExprData_unaryExprGetOp (expr2->data) )
 972         return FALSE;
 973
 974       return (constraintExpr_similar (
 975               constraintExprData_unaryExprGetExpr (expr1->data),
 976               constraintExprData_unaryExprGetExpr (expr2->data)
 977               ));
 978
 979     case binaryexpr:
 980       if (constraintExprData_binaryExprGetOp (expr1->data) != constraintExprData_binaryExprGetOp (expr2->data) )
 981         return FALSE;
 982
 983       if (! constraintExpr_similar (constraintExprData_binaryExprGetExpr1 (expr1->data),
 984                                  constraintExprData_binaryExprGetExpr1 (expr2->data)) )
 985         return FALSE;
 986
 987       if (! constraintExpr_similar (constraintExprData_binaryExprGetExpr2 (expr1->data),
 988                                  constraintExprData_binaryExprGetExpr2 (expr2->data)) )
 989         return FALSE;
 990       else
 991         return TRUE;
 992       /*@notreached@*/
 993       break;
 994
 995     default:
 996       llassert(FALSE);
 997       return FALSE;
 998     }
 999   /*@notreached@*/
1000   return FALSE;
1001 }
1002
1003 bool constraintExpr_same (constraintExpr expr1, constraintExpr expr2)
1004 {
1005   constraintExprKind kind;
1006
1007   llassert (expr1 != NULL);
1008   llassert (expr2 != NULL);
1009   if (expr1->kind != expr2->kind)
1010     return FALSE;
1011
1012   kind = expr1->kind;
1013
1014   switch (kind)
1015     {
1016     case term:
1017       return constraintTerm_similar (constraintExprData_termGetTerm(expr1->data),
1018                                   constraintExprData_termGetTerm(expr2->data) );
1019       /*@notreached@*/ break;
1020
1021     case unaryExpr:
1022       if (constraintExprData_unaryExprGetOp (expr1->data) != constraintExprData_unaryExprGetOp (expr2->data) )
1023         return FALSE;
1024
1025       return (constraintExpr_same (
1026               constraintExprData_unaryExprGetExpr (expr1->data),
1027               constraintExprData_unaryExprGetExpr (expr2->data)
1028               ));
1029
1030
1031     case binaryexpr:
1032       if (constraintExprData_binaryExprGetOp (expr1->data) != constraintExprData_binaryExprGetOp (expr2->data) )
1033         return FALSE;
1034
1035       if (! constraintExpr_same (constraintExprData_binaryExprGetExpr1 (expr1->data),
1036                                  constraintExprData_binaryExprGetExpr1 (expr2->data)) )
1037         return FALSE;
1038
1039       if (! constraintExpr_same (constraintExprData_binaryExprGetExpr2 (expr1->data),
1040                                  constraintExprData_binaryExprGetExpr2 (expr2->data)) )
1041         return FALSE;
1042       else
1043         return TRUE;
1044       /*@notreached@*/ break;
1045
1046     default:
1047       llassert(FALSE);
1048       return FALSE;
1049     }
1050
1051   /*@notreached@*/
1052   BADEXIT;
1053 }
1054
1055 bool
1056 constraintExpr_search (/*@observer@*/ constraintExpr c,
1057                        /*@observer@*/ constraintExpr old)
1058 {
1059   bool ret = FALSE;
1060   constraintExprKind kind;
1061   constraintExpr temp;
1062
1063   if (constraintExpr_similar (c, old))
1064     {
1065       DPRINTF (("Found  %q", constraintExpr_unparse (old)));
1066       return TRUE;
1067     }
1068
1069   llassert (constraintExpr_isDefined (c) && constraintExpr_isDefined(old) );
1070
1071   if ( !(constraintExpr_isDefined (c) && constraintExpr_isDefined(old) ) )
1072     return FALSE;
1073
1074   kind = c->kind;
1075
1076   switch (kind)
1077     {
1078     case term:
1079       break;
1080     case unaryExpr:
1081       temp = constraintExprData_unaryExprGetExpr (c->data);
1082       ret = ret || constraintExpr_search (temp, old);
1083       break;
1084     case binaryexpr:
1085
1086       temp = constraintExprData_binaryExprGetExpr1 (c->data);
1087       ret = ret || constraintExpr_search(temp, old);
1088
1089       temp = constraintExprData_binaryExprGetExpr2 (c->data);
1090       ret = ret || constraintExpr_search(temp, old);
1091       break;
1092     default:
1093       llassert(FALSE);
1094     }
1095   return ret;
1096
1097 }
1098
1099
1100 /*@only@*/ constraintExpr constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@temp@*/ constraintExpr old, /*@temp@*/ constraintExpr newExpr )
1101 {
1102   constraintExprKind kind;
1103   constraintExpr temp;
1104   constraintExpr ret;
1105
1106   llassert(constraintExpr_isDefined (newExpr) && (constraintExpr_isDefined (old) && constraintExpr_isDefined(c) ) );
1107
1108   if ( constraintExpr_similar (c, old) )
1109     {
1110
1111       ctype newType, cType;
1112
1113
1114
1115
1116       ret = constraintExpr_copy (newExpr);
1117       llassert(constraintExpr_isDefined(ret) );
1118       /*drl if newExpr != NULL then ret will != NULL*/
1119
1120       DPRINTF((message ("Replacing %s with %s",
1121                         constraintExpr_unparse(old), constraintExpr_unparse(newExpr)
1122                         )));
1123
1124       if (constraintExpr_canGetCType(c) && constraintExpr_canGetCType(newExpr) )
1125         {
1126           cType = constraintExpr_getCType(c);
1127           newType =  constraintExpr_getCType(newExpr);
1128
1129           if (ctype_match(cType,newType) )
1130             {
1131               DPRINTF(( message("constraintExpr_searchandreplace: replacing "
1132                                 " %s with type %s with %s with type %s",
1133                                 constraintExpr_print(c), ctype_unparse(cType),
1134                                 constraintExpr_print(newExpr), ctype_unparse(newType)
1135                                 )
1136                         ));
1137
1138               ret->ct = TRUE;
1139               ret->origType = cType;
1140             }
1141         }
1142
1143       if (constraintExpr_hasMaxSet(c) )
1144         {
1145           if (constraintExpr_hasTypeChange(c))
1146           {
1147           DPRINTF(( message("constraintExpr_searchandreplace: encountered "
1148                             "MaxSet with changed type %s ",
1149                             constraintExpr_print(c) )
1150                     ));
1151
1152           /*fix this with a conversation */
1153           ret = constraintExpr_adjustMaxSetForCast(ret, constraintExpr_getOrigType(c));
1154           }
1155         }
1156       constraintExpr_free(c);
1157
1158       return ret;
1159     }
1160
1161   kind = c->kind;
1162
1163   switch (kind)
1164     {
1165     case term:
1166       break;
1167     case unaryExpr:
1168       temp = constraintExprData_unaryExprGetExpr (c->data);
1169       temp = constraintExpr_copy(temp);
1170       temp = constraintExpr_searchandreplace (temp, old, newExpr);
1171       c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1172       break;
1173     case binaryexpr:
1174
1175       temp = constraintExprData_binaryExprGetExpr1 (c->data);
1176       temp = constraintExpr_copy(temp);
1177       temp = constraintExpr_searchandreplace (temp, old, newExpr);
1178       c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1179
1180       temp = constraintExprData_binaryExprGetExpr2 (c->data);
1181       temp = constraintExpr_copy(temp);
1182       temp = constraintExpr_searchandreplace (temp, old, newExpr);
1183       c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1184       break;
1185     default:
1186       llassert(FALSE);
1187     }
1188   return c;
1189 }
1190
1191 /*@notnull@*/ static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ /*@notnull@*/ constraintExpr c)
1192 {
1193   constraintExprKind kind;
1194   constraintExpr temp;
1195
1196   kind = c->kind;
1197
1198   switch (kind)
1199     {
1200     case term:
1201       break;
1202     case unaryExpr:
1203       temp = constraintExprData_unaryExprGetExpr (c->data);
1204       temp = constraintExpr_copy(temp);
1205       temp = constraintExpr_simplify (temp);
1206       c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1207       break;
1208     case binaryexpr:
1209       DPRINTF((message("constraintExpr_simplfiyChildren: simplify binary expression: %s",constraintExpr_unparse(c) ) ) );
1210       temp = constraintExprData_binaryExprGetExpr1 (c->data);
1211       temp = constraintExpr_copy(temp);
1212       temp = constraintExpr_simplify (temp);
1213
1214       c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1215
1216       temp = constraintExprData_binaryExprGetExpr2 (c->data);
1217       temp = constraintExpr_copy(temp);
1218       temp = constraintExpr_simplify (temp);
1219
1220       c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1221       break;
1222     default:
1223       llassert(FALSE);
1224     }
1225   return c;
1226
1227 }
1228
1229
1230 constraintExpr constraintExpr_setFileloc (/*@returned@*/ constraintExpr c, fileloc loc) /*@modifies c @*/
1231 {
1232   constraintTerm t;
1233   constraintExpr temp;
1234
1235   llassert(c != NULL);
1236
1237   switch (c->kind)
1238     {
1239     case term:
1240       t = constraintExprData_termGetTerm (c->data);
1241       t = constraintTerm_copy(t);
1242       t = constraintTerm_setFileloc (t, loc);
1243       c->data = constraintExprData_termSetTerm (c->data, t);
1244       break;
1245     case binaryexpr:
1246
1247       temp = constraintExprData_binaryExprGetExpr1 (c->data);
1248       temp = constraintExpr_copy(temp);
1249       temp = constraintExpr_setFileloc (temp, loc);
1250       c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
1251
1252       temp = constraintExprData_binaryExprGetExpr2 (c->data);
1253       temp = constraintExpr_copy(temp);
1254       temp = constraintExpr_setFileloc (temp, loc);
1255       c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
1256       break;
1257     case unaryExpr:
1258       temp = constraintExprData_unaryExprGetExpr (c->data);
1259       temp = constraintExpr_copy(temp);
1260       temp = constraintExpr_setFileloc (temp, loc);
1261       c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
1262       break;
1263     }
1264   return c;
1265 }
1266
1267 static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/ /*@notnull@*/ constraintExpr c)
1268 {
1269   constraintExpr e1, e2;
1270   constraintExprBinaryOpKind  op;
1271
1272   e1 = constraintExprData_binaryExprGetExpr1 (c->data);
1273   e2 = constraintExprData_binaryExprGetExpr2 (c->data);
1274
1275   if (constraintExpr_canGetValue (e1) && constraintExpr_canGetValue(e2) )
1276     {
1277       long i;
1278
1279       i = constraintExpr_getValue(e1) + constraintExpr_getValue (e2);
1280       constraintExpr_free(c);
1281       c = constraintExpr_makeIntLiteral (i);
1282     }
1283   else
1284     {
1285       op = constraintExprData_binaryExprGetOp (c->data);
1286       if (op == BINARYOP_MINUS)
1287         if (constraintExpr_similar(e1, e2) )
1288           {
1289             constraintExpr_free(c);
1290             c =  constraintExpr_makeIntLiteral (0);
1291           }
1292     }
1293
1294   return c;
1295 }
1296
1297 /*
1298   this thing takes the lexpr and expr of a constraint and modifies lexpr
1299   and returns a (possiblly new) value for expr
1300 */
1301 /* 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 */
1302
1303 /* the approach is a little Kludgy but seems to work.  I should probably use something cleaner at some point ... */
1304
1305
1306 /*@only@*/ constraintExpr constraintExpr_solveBinaryExpr (constraintExpr lexpr, /*@only@*/ constraintExpr expr)
1307 {
1308   constraintExpr expr1, expr2;
1309   constraintExprBinaryOpKind op;
1310
1311   llassert(constraintExpr_isDefined (lexpr)  && constraintExpr_isDefined (expr)  );
1312
1313   if (lexpr->kind != binaryexpr)
1314     return expr;
1315
1316   expr2 = constraintExprData_binaryExprGetExpr2 (lexpr->data);
1317   expr1 = constraintExprData_binaryExprGetExpr1 (lexpr->data);
1318
1319   op    = constraintExprData_binaryExprGetOp (lexpr->data);
1320
1321   expr1 = constraintExpr_copy(expr1);
1322   expr2 = constraintExpr_copy(expr2);
1323
1324   llassert(constraintExpr_isDefined (expr1)  && constraintExpr_isDefined (expr2)  );
1325
1326   /* drl possible problem : warning make sure this works */
1327
1328   lexpr->kind = expr1->kind;
1329   sfree (lexpr->data);
1330
1331   lexpr->data = copyExprData (expr1->data, expr1->kind);
1332   constraintExpr_free(expr1);
1333
1334   if (op == BINARYOP_PLUS)
1335     expr = constraintExpr_makeSubtractExpr (expr, expr2);
1336   else if (op == BINARYOP_MINUS)
1337     expr = constraintExpr_makeAddExpr (expr, expr2);
1338   else
1339     BADEXIT;
1340
1341
1342   return expr;
1343
1344   /*
1345     #warning this needs to be checked
1346     expr = constraintExpr_solveBinaryExpr (expr1, expr);
1347
1348     expr = constraintExpr_solveBinaryExpr (expr2, expr);
1349     return expr;
1350   */
1351 }
1352
1353 static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ constraintExpr c)
1354 {
1355   constraintExpr exp;
1356
1357   llassert(constraintExpr_isDefined (c) );
1358   llassert (c->kind == unaryExpr);
1359
1360   DPRINTF ((message ("Doing constraintExpr_simplifyunaryExpr:%s", constraintExpr_unparse (c) ) ) );
1361
1362   if ((constraintExprData_unaryExprGetOp (c->data) != MAXSET) &&
1363        (constraintExprData_unaryExprGetOp (c->data) != MAXREAD) )
1364     {
1365       return c;
1366     }
1367
1368   exp = constraintExprData_unaryExprGetExpr (c->data);
1369   exp = constraintExpr_copy(exp);
1370
1371   llassert(constraintExpr_isDefined (exp)  );
1372
1373   if (exp->kind == term)
1374     {
1375       constraintTerm cterm;
1376
1377       cterm = constraintExprData_termGetTerm (exp->data);
1378
1379       if (constraintTerm_isStringLiteral(cterm) )
1380         {
1381           cstring val;
1382           val = constraintTerm_getStringLiteral (cterm);
1383           if (constraintExprData_unaryExprGetOp (c->data) == MAXSET)
1384             {
1385               constraintExpr temp;
1386
1387               temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
1388               cstring_free(val);
1389               constraintExpr_free(c);
1390               constraintExpr_free(exp);
1391
1392               return temp;
1393
1394             }
1395           if (constraintExprData_unaryExprGetOp (c->data) == MAXREAD)
1396             {
1397               constraintExpr temp;
1398
1399               temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
1400               cstring_free(val);
1401               constraintExpr_free(c);
1402               constraintExpr_free(exp);
1403
1404               return temp;
1405             }
1406           BADEXIT;
1407         }
1408
1409       /* slight Kludge to hanlde var [] = { , , };
1410       ** type syntax  I don't think this is sounds but it should be good
1411       ** enough.  The C stanrad is very confusing about initialization
1412       ** -- DRL 7/25/01
1413       */
1414
1415       if (constraintTerm_isInitBlock(cterm) )
1416         {
1417           constraintExpr temp;
1418           int len;
1419
1420           len = constraintTerm_getInitBlockLength(cterm);
1421
1422           temp = constraintExpr_makeIntLiteral (len );
1423
1424           constraintExpr_free(c);
1425           DPRINTF(( message("Changed too %q", constraintExpr_print(temp)
1426                             ) ));
1427           constraintExpr_free(exp);
1428           return temp;
1429         }
1430
1431       constraintExpr_free(exp);
1432       return c;
1433     }
1434
1435   if (exp->kind != binaryexpr)
1436     {
1437       constraintExpr_free(exp);
1438       return c;
1439     }
1440
1441   if (constraintExprData_binaryExprGetOp (exp->data) == BINARYOP_PLUS  )
1442     {
1443
1444       /* if (constraintExpr_canGetValue (constraintExprData_binaryExprGetExpr2 (exp->data) ) ) */
1445         {
1446
1447           constraintExpr  temp, temp2;
1448
1449           DPRINTF ((message ("Doing fancy simplification") ) );
1450
1451           temp = constraintExprData_binaryExprGetExpr2 (exp->data);
1452
1453           temp2 = constraintExprData_binaryExprGetExpr1 (exp->data);
1454
1455           temp2 = constraintExpr_copy(temp2);
1456           c->data = constraintExprData_unaryExprSetExpr (c->data, temp2);
1457
1458
1459           temp = constraintExpr_copy (temp);
1460
1461           c = constraintExpr_makeSubtractExpr (c, temp);
1462
1463           DPRINTF ((message ("Done fancy simplification:%s", constraintExpr_unparse (c) ) ) );
1464         }
1465     }
1466
1467   DPRINTF ((message ("constraintExpr_simplifyUnaryExpr: Done simplification:%s", constraintExpr_unparse (c) ) ) );
1468
1469   constraintExpr_free(exp);
1470   return c;
1471 }
1472
1473
1474 /*@only@*/ constraintExpr constraintExpr_simplify (/*@only@*/ constraintExpr c)
1475 {
1476   constraintExprKind kind;
1477   constraintExpr ret;
1478   constraintTerm t;
1479
1480   DPRINTF ((message ("Doing constraintExpr_simplify:%s", constraintExpr_unparse (c) ) ) );
1481
1482
1483   /*@i22*/
1484
1485   /* drl: I think this is an Splint bug */
1486
1487   llassert ( constraintExpr_isDefined (c) );
1488   if (constraintExpr_isUndefined (c) )
1489     {
1490       return constraintExpr_undefined;
1491     }
1492
1493   ret =  constraintExpr_copy(c);
1494   llassert(constraintExpr_isDefined (ret) );
1495
1496   constraintExpr_free(c);
1497
1498   ret = constraintExpr_simplifyChildren (ret);
1499
1500   ret = constraintExpr_combineConstants (ret);
1501
1502   ret = constraintExpr_simplifyChildren (ret);
1503
1504
1505   kind = ret->kind;
1506
1507   switch (kind)
1508     {
1509     case term:
1510       t = constraintExprData_termGetTerm (ret->data);
1511       t = constraintTerm_copy(t);
1512       t = constraintTerm_simplify (t);
1513       ret->data = constraintExprData_termSetTerm (ret->data, t);
1514       break;
1515     case unaryExpr:
1516       ret = constraintExpr_simplifyunaryExpr (ret);
1517       break;
1518     case binaryexpr:
1519       ret = constraintExpr_simplifybinaryExpr (ret);
1520       break;
1521     default:
1522       llassert(FALSE);
1523     }
1524
1525   DPRINTF ((message ("constraintExpr_simplify returning :%s", constraintExpr_unparse (ret) ) ) );
1526   return ret;
1527
1528 }
1529
1530 /*@only@*/
1531 cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@*/
1532 {
1533   cstring st;
1534   constraintExprKind kind;
1535
1536   llassert (ex != NULL);
1537
1538   kind = ex->kind;
1539
1540   switch (kind)
1541     {
1542     case term:
1543
1544             if (context_getFlag (FLG_PARENCONSTRAINT) )
1545               {
1546                 st = message ("(%q) ", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
1547               }
1548             else
1549               {
1550                 st = message ("%q", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
1551               }
1552       break;
1553     case unaryExpr:
1554       st = message ("%q(%q)",
1555                     constraintExprUnaryOpKind_print (constraintExprData_unaryExprGetOp (ex->data) ),
1556                     constraintExpr_unparse (constraintExprData_unaryExprGetExpr (ex->data) )
1557                     );
1558       break;
1559     case binaryexpr:
1560       if (context_getFlag (FLG_PARENCONSTRAINT) )
1561         {
1562           st = message ("(%q) %q (%q)",
1563                     constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
1564                     constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
1565                                                      ),
1566                     constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
1567                     );
1568         }
1569       else
1570         {
1571           st = message ("%q %q %q",
1572                         constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
1573                         constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
1574                                                           ),
1575                         constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
1576                         );
1577         }
1578
1579       break;
1580     default:
1581       llassert(FALSE);
1582       st = message ("error");
1583
1584     }
1585
1586   DPRINTF((message ("constraintExpr_unparse: '%s'",st) ) );
1587   return st;
1588 }
1589
1590 constraintExpr constraintExpr_doSRefFixBaseParam (/*@returned@*/  constraintExpr expr, exprNodeList arglist)
1591 {
1592   constraintTerm Term;
1593   constraintExprKind kind;
1594   constraintExpr expr1, expr2;
1595   constraintExprData data;
1596   llassert (expr != NULL);
1597
1598   data = expr->data;
1599
1600   kind = expr->kind;
1601
1602   switch (kind)
1603     {
1604     case term:
1605       Term = constraintExprData_termGetTerm(data);
1606       Term = constraintTerm_copy(Term);
1607
1608       Term = constraintTerm_doSRefFixBaseParam (Term, arglist);
1609       data = constraintExprData_termSetTerm(data, Term);
1610       break;
1611     case unaryExpr:
1612       expr1 = constraintExprData_unaryExprGetExpr (data);
1613       expr1 = constraintExpr_copy(expr1);
1614
1615       expr1 = constraintExpr_doSRefFixBaseParam (expr1, arglist);
1616       data = constraintExprData_unaryExprSetExpr (data, expr1);
1617       break;
1618     case binaryexpr:
1619       expr1 = constraintExprData_binaryExprGetExpr1 (data);
1620       expr2 = constraintExprData_binaryExprGetExpr2 (data);
1621
1622       expr1 = constraintExpr_copy(expr1);
1623       expr2 = constraintExpr_copy(expr2);
1624
1625       expr1 = constraintExpr_doSRefFixBaseParam (expr1, arglist);
1626       data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1627       expr2 = constraintExpr_doSRefFixBaseParam (expr2, arglist);
1628       data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1629
1630       break;
1631     default:
1632       llassert(FALSE);
1633       data = NULL;
1634     }
1635   return expr;
1636 }
1637
1638 /*
1639 / *@only@* / constraintExpr constraintExpr_doSRefFixInvarConstraint (/ *@only@* / constraintExpr expr, sRef s, ctype ct)
1640 {
1641   constraintExprKind kind;
1642   constraintExpr expr1, expr2;
1643   constraintExprData data;
1644   llassert (expr != NULL);
1645
1646   data = expr->data;
1647
1648   kind = expr->kind;
1649
1650   switch (kind)
1651     {
1652     case term:
1653       expr = doSRefFixInvarConstraintTerm (expr, s, ct);
1654       break;
1655     case unaryExpr:
1656       expr1 = constraintExprData_unaryExprGetExpr (data);
1657       expr1 = constraintExpr_copy(expr1);
1658       expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
1659       data = constraintExprData_unaryExprSetExpr (data, expr1);
1660       break;
1661     case binaryexpr:
1662       expr1 = constraintExprData_binaryExprGetExpr1 (data);
1663       expr2 = constraintExprData_binaryExprGetExpr2 (data);
1664
1665       expr1 = constraintExpr_copy(expr1);
1666       expr2 = constraintExpr_copy(expr2);
1667
1668       expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
1669       data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1670       expr2 = constraintExpr_doSRefFixInvarConstraint (expr2, s, ct);
1671       data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1672
1673       break;
1674     default:
1675       llassert(FALSE);
1676       data = NULL;
1677     }
1678   return expr;
1679 }
1680 */
1681
1682 /*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@only@*/ constraintExpr expr, exprNodeList arglist) /*@modifies expr@*/
1683 {
1684   constraintExprKind kind;
1685   constraintExpr expr1, expr2;
1686   constraintExprData data;
1687   llassert (expr != NULL);
1688
1689   data = expr->data;
1690
1691   kind = expr->kind;
1692
1693   switch (kind)
1694     {
1695     case term:
1696       expr = doSRefFixConstraintParamTerm (expr, arglist);
1697       break;
1698     case unaryExpr:
1699       expr1 = constraintExprData_unaryExprGetExpr (data);
1700       expr1 = constraintExpr_copy(expr1);
1701       expr1 = constraintExpr_doSRefFixConstraintParam (expr1, arglist);
1702       data = constraintExprData_unaryExprSetExpr (data, expr1);
1703       break;
1704     case binaryexpr:
1705       expr1 = constraintExprData_binaryExprGetExpr1 (data);
1706       expr2 = constraintExprData_binaryExprGetExpr2 (data);
1707
1708       expr1 = constraintExpr_copy(expr1);
1709       expr2 = constraintExpr_copy(expr2);
1710
1711       expr1 = constraintExpr_doSRefFixConstraintParam (expr1, arglist);
1712       data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1713       expr2 = constraintExpr_doSRefFixConstraintParam (expr2, arglist);
1714       data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1715
1716       break;
1717     default:
1718       llassert(FALSE);
1719       data = NULL;
1720     }
1721   return expr;
1722 }
1723
1724 /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/  constraintExpr expr, /*@observer@*/ exprNode fcnCall)
1725 {
1726   constraintExprKind kind;
1727   constraintExpr expr1, expr2;
1728   constraintExprData data;
1729   llassert (expr != NULL);
1730
1731   data = expr->data;
1732
1733   kind = expr->kind;
1734
1735   switch (kind)
1736     {
1737     case term:
1738       expr = doFixResultTerm (expr, fcnCall);
1739       break;
1740     case unaryExpr:
1741       expr1 = constraintExprData_unaryExprGetExpr (data);
1742       expr1 = constraintExpr_copy(expr1);
1743
1744       expr1 = constraintExpr_doFixResult (expr1, fcnCall);
1745       data = constraintExprData_unaryExprSetExpr (data, expr1);
1746       break;
1747     case binaryexpr:
1748       expr1 = constraintExprData_binaryExprGetExpr1 (data);
1749       expr2 = constraintExprData_binaryExprGetExpr2 (data);
1750
1751       expr1 = constraintExpr_copy(expr1);
1752       expr2 = constraintExpr_copy(expr2);
1753
1754       expr1 = constraintExpr_doFixResult (expr1, fcnCall);
1755       data = constraintExprData_binaryExprSetExpr1 (data, expr1);
1756       expr2 = constraintExpr_doFixResult (expr2, fcnCall);
1757       data = constraintExprData_binaryExprSetExpr2 (data, expr2);
1758
1759       break;
1760     default:
1761       llassert(FALSE);
1762       data = NULL;
1763     }
1764   return expr;
1765 }
1766
1767 cstring constraintExpr_print (constraintExpr expr) /*@*/
1768 {
1769   return constraintExpr_unparse (expr);
1770 }
1771
1772 bool constraintExpr_hasMaxSet (constraintExpr expr) /*@*/
1773 {
1774   cstring t;
1775
1776   t = constraintExpr_unparse(expr);
1777
1778   if (cstring_containsLit(t, "maxSet") != NULL )
1779     {
1780       cstring_free(t);
1781       return (TRUE);
1782     }
1783   else
1784     {
1785       cstring_free(t);
1786       return FALSE;
1787     }
1788 }
1789
1790
1791
1792       /*returns 1 0 -1 like strcmp
1793         1 => expr1 > expr2
1794         0 => expr1 == expr2
1795         -1 => expr1 < expr2
1796        */
1797
1798 int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2)
1799 {
1800   long value1, value2;
1801
1802   if (constraintExpr_similar (expr1, expr2) )
1803     {
1804       return 0;
1805     }
1806
1807   value1 = constraintExpr_getValue(expr1);
1808   value2 = constraintExpr_getValue(expr2);
1809
1810   if (value1 > value2)
1811     return 1;
1812
1813   if (value1 == value2)
1814     return 0;
1815
1816   else
1817     return -1;
1818 }
1819
1820 long constraintExpr_getValue (constraintExpr expr)
1821 {
1822   llassert (constraintExpr_isDefined(expr) );
1823   llassert (expr->kind == term);
1824
1825   return (constraintTerm_getValue (constraintExprData_termGetTerm (expr->data)));
1826 }
1827
1828 bool constraintExpr_canGetValue (constraintExpr expr)
1829 {
1830   llassert ( constraintExpr_isDefined (expr) );
1831   if (constraintExpr_isUndefined (expr) )
1832     {
1833       return FALSE;
1834     }
1835
1836   switch (expr->kind)
1837     {
1838     case term:
1839       return constraintTerm_canGetValue (constraintExprData_termGetTerm (expr->data) );
1840     default:
1841       return FALSE;
1842
1843     }
1844
1845   BADEXIT;
1846 }
1847
1848 fileloc constraintExpr_getFileloc (constraintExpr expr)
1849 {
1850   constraintExpr e;
1851 constraintTerm t;
1852   constraintExprKind kind;
1853
1854   llassert ( constraintExpr_isDefined (expr) );
1855   if (constraintExpr_isUndefined (expr) )
1856     {
1857       return fileloc_undefined;
1858     }
1859
1860
1861  kind = expr->kind;
1862
1863   switch (kind)
1864     {
1865     case term:
1866       t = constraintExprData_termGetTerm (expr->data);
1867       return (constraintTerm_getFileloc (t) );
1868       /*@notreached@*/
1869       break;
1870     case unaryExpr:
1871       e = constraintExprData_unaryExprGetExpr (expr->data);
1872       return (constraintExpr_getFileloc (e) );
1873       /*@notreached@*/
1874       break;
1875     case binaryexpr:
1876       e = constraintExprData_binaryExprGetExpr1 (expr->data);
1877       return (constraintExpr_getFileloc (e) );
1878       /*@notreached@*/
1879       break;
1880     }
1881   llassert (FALSE);
1882   return (fileloc_undefined);
1883 }
1884
1885 /*drl moved from constriantTerm.c 5/20/001*/
1886 static /*@only@*/ constraintExpr
1887 doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall)
1888 {
1889   constraintTerm t;
1890   sRef s;
1891
1892
1893   constraintExprData data;
1894   constraintExprKind kind;
1895
1896   constraintExpr ret;
1897
1898   llassert(constraintExpr_isDefined (e) );
1899
1900   data = e->data;
1901   kind = e->kind;
1902
1903   llassert(kind == term);
1904
1905   t = constraintExprData_termGetTerm (data);
1906   llassert (constraintTerm_isDefined(t) );
1907
1908   ret = e;
1909   switch (constraintTerm_getKind(t) )
1910     {
1911     case CTT_EXPR:
1912     case CTT_INTLITERAL:
1913       break;
1914
1915     case CTT_SREF:
1916       s = constraintTerm_getSRef(t);
1917       if (sRef_isResult (s))
1918         {
1919           ret = constraintExpr_makeExprNode(fcnCall);
1920           constraintExpr_free(e);
1921           e = NULL;
1922         }
1923       else
1924         {
1925           e = NULL;
1926         }
1927       break;
1928     default:
1929       BADEXIT;
1930     }
1931
1932   return ret;
1933
1934 }
1935 /*
1936 / *@only@* / static constraintExpr
1937 doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
1938  sRef s, ctype ct)
1939 {
1940   constraintTerm t;
1941
1942   constraintExprData data = e->data;
1943
1944   constraintExprKind kind = e->kind;
1945
1946   constraintExpr ret;
1947
1948   llassert(kind == term);
1949
1950   t = constraintExprData_termGetTerm (data);
1951   llassert (constraintTerm_isDefined(t) );
1952
1953   ret = e;
1954
1955   DPRINTF (("Fixing: %s", constraintExpr_print (e)));
1956
1957   switch (constraintTerm_getKind(t))
1958     {
1959     case CTT_EXPR:
1960       DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
1961                         fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
1962       break;
1963     case CTT_INTLITERAL:
1964       DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
1965       break;
1966
1967     case CTT_SREF:
1968       / * evans 2001-07-24: constants should use the original term * /
1969       if (!constraintTerm_canGetValue (t))
1970         {
1971           sRef snew;
1972           DPRINTF ((message("Doing sRef_fixInvarConstraint for %q ",
1973                              constraintTerm_unparse (t) ) ));
1974
1975           snew = fixSref (ct, s, constraintTerm_getSRef(t));
1976
1977           ret = constraintExpr_makeTermsRef(snew);
1978
1979           constraintExpr_free (e);
1980
1981           DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
1982                              constraintExpr_print (ret) ) ));
1983           / *@-branchstate@* /
1984         } / *@=branchstate@* /
1985
1986       break;
1987     default:
1988       BADEXIT;
1989     }
1990
1991   return ret;
1992
1993 }
1994 */
1995
1996 /*drl moved from constriantTerm.c 5/20/001*/
1997 /*@only@*/ static constraintExpr
1998 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
1999 {
2000   constraintTerm t;
2001
2002   constraintExprData data;
2003
2004   constraintExprKind kind;
2005
2006   constraintExpr ret;
2007
2008
2009   llassert(constraintExpr_isDefined (e) );
2010
2011   data = e->data;
2012
2013   kind = e->kind;
2014
2015
2016
2017   llassert(kind == term);
2018
2019   t = constraintExprData_termGetTerm (data);
2020   llassert (constraintTerm_isDefined(t) );
2021
2022   ret = e;
2023
2024   DPRINTF (("Fixing: %s", constraintExpr_print (e)));
2025
2026   switch (constraintTerm_getKind(t))
2027     {
2028     case CTT_EXPR:
2029       DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
2030                         fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
2031       break;
2032     case CTT_INTLITERAL:
2033       DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
2034       break;
2035     case CTT_SREF:
2036       /* evans 2001-07-24: constants should use the original term */
2037       if (!constraintTerm_canGetValue (t))
2038         {
2039           DPRINTF ((message("Doing sRef_fixConstraintParam for %q ",
2040                              constraintTerm_unparse (t) ) ));
2041           ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
2042
2043           constraintExpr_free (e);
2044
2045           DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
2046                              constraintExpr_print (ret) ) ));
2047           /*@-branchstate@*/
2048         } /*@=branchstate@*/
2049
2050       break;
2051     default:
2052       BADEXIT;
2053     }
2054
2055   return ret;
2056
2057 }
2058
2059
2060 #if 0
2061 bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term)
2062 {
2063   if (constraintTerm_hasTerm (expr->term, term) )
2064     return TRUE;
2065
2066   if ((expr->expr) != NULL)
2067     {
2068       return ( constraintExpr_includesTerm (expr->expr, term) );
2069     }
2070   return FALSE;
2071
2072 }
2073 #endif
2074
2075 /*drl added 6/11/01 */
2076 bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c)
2077 {
2078
2079   llassert(constraintExpr_isDefined (c) );
2080
2081   if ( ! (constraintExpr_isDefined (c) ) )
2082     return FALSE;
2083
2084   if (c->kind == binaryexpr)
2085     return TRUE;
2086
2087   else
2088     return FALSE;
2089 }
2090
2091 /*drl added 8/08/001 */
2092 bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
2093 {
2094   llassert(constraintExpr_isDefined (c) );
2095
2096   if (c->kind == term)
2097     return TRUE;
2098
2099   else
2100     return FALSE;
2101 }
2102
2103 /*@observer@*/ /*@temp@*/ constraintTerm constraintExpr_getTerm ( /*@temp@*/ /*@observer@*/ constraintExpr c) /*@*/
2104 {
2105   constraintTerm term;
2106
2107   llassert(constraintExpr_isDefined (c) );
2108
2109   llassert(constraintExpr_isTerm(c) );
2110
2111   term = constraintExprData_termGetTerm(c->data);
2112
2113   return term;
2114 }
2115
2116 static void  binaryExpr_dump (/*@observer@*/ constraintExprData data,  FILE *f)
2117 {
2118   constraintExpr expr1;
2119   constraintExprBinaryOpKind binaryOp;
2120   constraintExpr expr2;
2121
2122
2123   binaryOp = constraintExprData_binaryExprGetOp (data);
2124
2125   fprintf(f, "%d\n", (int) binaryOp);
2126
2127   expr1 = constraintExprData_binaryExprGetExpr1 (data);
2128   expr2 = constraintExprData_binaryExprGetExpr2 (data);
2129
2130   fprintf(f, "e1\n");
2131
2132   constraintExpr_dump(expr1, f);
2133
2134   fprintf(f, "e2\n");
2135   constraintExpr_dump(expr2, f);
2136 }
2137
2138
2139 static constraintExpr  binaryExpr_undump (FILE *f)
2140 {
2141   constraintExpr expr1;
2142   constraintExprBinaryOpKind binaryOp;
2143   constraintExpr expr2;
2144
2145   constraintExpr ret;
2146
2147
2148
2149   char * str;
2150   char * os;
2151
2152   os = mstring_create (MAX_DUMP_LINE_LENGTH);
2153
2154   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2155
2156   if (! mstring_isDefined(str) )
2157     {
2158       llfatalbug(message("Library file is corrupted") );
2159     }
2160
2161   binaryOp = (constraintExprBinaryOpKind) reader_getInt(&str);
2162
2163   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2164
2165   if (! mstring_isDefined(str) )
2166     {
2167       llfatalbug(message("Library file is corrupted") );
2168     }
2169
2170   reader_checkChar (&str, 'e');
2171   reader_checkChar (&str, '1');
2172
2173   expr1 = constraintExpr_undump (f);
2174
2175   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2176
2177   reader_checkChar (&str, 'e');
2178   reader_checkChar (&str, '2');
2179
2180   expr2 = constraintExpr_undump (f);
2181
2182   ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
2183   ret->data = constraintExprData_binaryExprSetOp(ret->data, binaryOp);
2184
2185   free(os);
2186   return ret;
2187 }
2188
2189
2190
2191 static void  unaryExpr_dump (/*@observer@*/ constraintExprData data,  FILE *f)
2192 {
2193
2194   constraintExpr expr;
2195   constraintExprUnaryOpKind unaryOp;
2196
2197   unaryOp = constraintExprData_unaryExprGetOp (data);
2198
2199   fprintf(f, "%d\n", (int) unaryOp);
2200
2201   expr = constraintExprData_unaryExprGetExpr (data);
2202
2203   constraintExpr_dump(expr, f);
2204 }
2205
2206 static  constraintExpr  unaryExpr_undump ( FILE *f)
2207 {
2208
2209   constraintExpr expr;
2210   constraintExprUnaryOpKind unaryOp;
2211   constraintExpr ret;
2212
2213   char * str;
2214   char * os;
2215
2216   str = mstring_create (MAX_DUMP_LINE_LENGTH);
2217   os = str;
2218   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2219
2220   if (! mstring_isDefined(str) )
2221     {
2222       llfatalbug(message("Library file is corrupted") );
2223     }
2224
2225   unaryOp = (constraintExprUnaryOpKind) reader_getInt(&str);
2226
2227   expr = constraintExpr_undump (f);
2228
2229   ret = constraintExpr_makeUnaryOp (expr, unaryOp);
2230
2231   free(os);
2232
2233   return ret;
2234 }
2235
2236 void  constraintExpr_dump (/*@observer@*/ constraintExpr expr,  FILE *f)
2237 {
2238   constraintExprKind kind;
2239   constraintTerm t;
2240
2241
2242   llassert(constraintExpr_isDefined(expr) );
2243
2244   DPRINTF((message("constraintExpr_dump:: dumping constraintExpr %s",
2245                    constraintExpr_unparse(expr)
2246                    ) ));
2247
2248   kind = expr->kind;
2249
2250   fprintf(f,"%d\n", (int) kind);
2251
2252   switch (kind)
2253     {
2254     case term:
2255       t = constraintExprData_termGetTerm (expr->data);
2256       constraintTerm_dump (t, f);
2257       break;
2258     case unaryExpr:
2259       unaryExpr_dump (expr->data, f);
2260       break;
2261     case binaryexpr:
2262       binaryExpr_dump  (expr->data, f);
2263       break;
2264     }
2265 }
2266
2267 /*@only@*/ constraintExpr  constraintExpr_undump (FILE *f)
2268 {
2269   constraintExprKind kind;
2270   constraintTerm t;
2271   constraintExpr ret;
2272
2273   char * s;
2274   char * os;
2275
2276   s = mstring_create (MAX_DUMP_LINE_LENGTH);
2277
2278   os = s;
2279
2280   s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2281
2282   if (! mstring_isDefined(s) )
2283     {
2284       llfatalbug(message("Library file is corrupted") );
2285     }
2286
2287   kind = (constraintExprKind) reader_getInt(&s);
2288
2289   free (os);
2290
2291   switch (kind)
2292     {
2293     case term:
2294       t = constraintTerm_undump (f);
2295       ret = constraintExpr_makeTerm(t);
2296       break;
2297     case unaryExpr:
2298       ret = unaryExpr_undump (f);
2299       break;
2300     case binaryexpr:
2301       ret = binaryExpr_undump  (f);
2302       break;
2303     }
2304
2305   return ret;
2306
2307 }
2308
2309 int constraintExpr_getDepth (constraintExpr ex)
2310 {
2311   int ret;
2312
2313   constraintExprKind kind;
2314
2315   llassert (ex != NULL);
2316
2317   kind = ex->kind;
2318
2319   switch (kind)
2320     {
2321     case term:
2322       ret = 1;
2323       break;
2324     case unaryExpr:
2325       ret =  constraintExpr_getDepth (constraintExprData_unaryExprGetExpr (ex->data) );
2326       ret++;
2327
2328       break;
2329     case binaryexpr:
2330       ret = 0;
2331       ret = constraintExpr_getDepth (constraintExprData_binaryExprGetExpr1 (ex->data) );
2332
2333       ret++;
2334
2335       ret += constraintExpr_getDepth (constraintExprData_binaryExprGetExpr2 (ex->data) );
2336
2337       break;
2338     default:
2339       BADEXIT;
2340     }
2341
2342   return ret;
2343 }
2344
2345
2346 bool  constraintExpr_canGetCType (constraintExpr e) /*@*/
2347 {
2348   if (constraintExpr_isUndefined(e) )
2349     return FALSE;
2350
2351   if (e->kind == term)
2352     {
2353       return TRUE;
2354     }
2355   else
2356     {
2357       DPRINTF(( message("constraintExpr_canGetCType: can't get type for %s ",
2358                         constraintExpr_print(e) ) ));
2359       return FALSE;
2360     }
2361 }
2362
2363 ctype constraintExpr_getCType (constraintExpr e) /*@*/
2364 {
2365   constraintTerm t;
2366
2367   llassert(constraintExpr_isDefined(e) );
2368
2369   llassert(constraintExpr_canGetCType(e) );
2370
2371   switch (e->kind)
2372     {
2373     case term:
2374       t = constraintExprData_termGetTerm (e->data);
2375       return (constraintTerm_getCType(t) );
2376       /* assume that a unary expression will be an int ... */
2377     case unaryExpr:
2378       return ctype_signedintegral;
2379
2380       /* drl for just return type of first operand */
2381     case binaryexpr:
2382       return (
2383               constraintExpr_getCType
2384               (constraintExprData_binaryExprGetExpr1 (e->data) )
2385               );
2386     default:
2387       BADEXIT;
2388     }
2389   BADEXIT;
2390 }
2391
2392 /* drl add 10-5-001 */
2393
2394 static bool constraintExpr_hasTypeChange(constraintExpr e)
2395 {
2396   llassert(constraintExpr_isDefined(e) );
2397   if (constraintExpr_isDefined((e)) && (e->ct == TRUE) )
2398     {
2399       return TRUE;
2400     }
2401
2402   if (e->kind == unaryExpr)
2403     {
2404       if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
2405         {
2406           constraintExpr ce;
2407
2408           ce = constraintExprData_unaryExprGetExpr(e->data);
2409
2410           return (constraintExpr_hasTypeChange(ce) );
2411         }
2412
2413     }
2414   return FALSE;
2415 }
2416
2417 /* drl add 10-5-001 */
2418
2419 static ctype constraintExpr_getOrigType (constraintExpr e)
2420 {
2421
2422   llassert(constraintExpr_isDefined(e) );
2423   llassert(constraintExpr_hasTypeChange(e) );
2424
2425
2426   if (e->ct == TRUE)
2427     {
2428       return e->origType;
2429     }
2430
2431   if (e->kind == unaryExpr)
2432     {
2433       if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
2434         {
2435           constraintExpr ce;
2436
2437           ce = constraintExprData_unaryExprGetExpr(e->data);
2438
2439           return (constraintExpr_getOrigType(ce) );
2440         }
2441
2442     }
2443
2444   BADEXIT;
2445 }
2446
2447 /*drl added these around 10/18/001*/
2448
2449 static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e, /*@unused@*/ ctype ct)
2450 {
2451   return e;
2452 }
2453
2454
2455 /*@access exprNode@*/
2456 static /*@only@*/ constraintExpr  constraintTerm_simpleDivTypeExprNode(/*@only@*/ constraintExpr e, ctype ct)
2457 {
2458   exprData data;
2459   exprNode t1, t2, expr;
2460   lltok tok;
2461   constraintTerm t;
2462
2463   llassert(constraintExpr_isDefined(e) );
2464
2465   DPRINTF((
2466            message("constraintTerm_simpleDivTypeExprNode e=%s, ct=%s",
2467                    constraintExpr_print(e), ctype_unparse(ct)
2468                    )
2469            ));
2470
2471   t = constraintExprData_termGetTerm(e->data);
2472
2473   expr = constraintTerm_getExprNode(t);
2474
2475   llassert(constraintExpr_isDefined(e) );
2476   llassert(exprNode_isDefined(expr) );
2477
2478   if (expr->kind == XPR_OP)
2479     {
2480       data = expr->edata;
2481
2482       t1 = exprData_getOpA (data);
2483       t2 = exprData_getOpB (data);
2484       tok = exprData_getOpTok (data);
2485       if (lltok_isMult(tok) )
2486         {
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...*/
2490
2491           if  ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
2492             {
2493               ctype ct2;
2494
2495               if (t1->kind == XPR_SIZEOFT)
2496                 {
2497                   ct2 = qtype_getType (exprData_getType (t1->edata));
2498                 }
2499               else
2500                 {
2501                   exprNode tempE;
2502
2503                   tempE = exprData_getSingle (t1->edata);
2504
2505                   ct2 =  exprNode_getType (tempE);
2506                 }
2507               if (ctype_match (ctype_makePointer(ct2), ct) )
2508                 {
2509                   /* this is a bit sloopy but ... */
2510                                   constraintExpr_free(e);
2511                   return constraintExpr_makeExprNode(t2);
2512                 }
2513             }
2514
2515
2516           else   if  ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
2517             {
2518               ctype ct2;
2519
2520               if (t2->kind == XPR_SIZEOFT)
2521                 {
2522                   ct2 = qtype_getType (exprData_getType (t2->edata));
2523                 }
2524               else
2525                 {
2526                   exprNode exprTemp;
2527                   exprData eDTemp;
2528
2529                   exprTemp = exprData_getSingle (t2->edata);
2530
2531                   llassert(exprNode_isDefined(exprTemp) );
2532                   eDTemp = exprTemp->edata;
2533
2534                   ct2 = qtype_getType (exprData_getType(eDTemp ) );
2535
2536                 }
2537               if (ctype_match (ctype_makePointer(ct2),ct) )
2538                 {
2539                   /* sloopy way to do this... */ /*@i22*/
2540                                   constraintExpr_free(e);
2541                   return constraintExpr_makeExprNode(t1);
2542                 }
2543             }
2544           else
2545             {
2546               /*empty*/
2547             }
2548
2549         }
2550     }
2551   return (constraintExpr_div (e, ct) );
2552 }
2553 /*@noaccess exprNode@*/
2554
2555 static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype ct)
2556 {
2557   /*@i333*/
2558   DPRINTF(( (message("simpleDiv got %s ", constraintExpr_unparse(e) ) )
2559             ));
2560
2561   llassert(constraintExpr_isDefined(e) );
2562
2563   switch (e->kind)
2564     {
2565     case term:
2566
2567       {
2568         constraintTerm t;
2569
2570         t = constraintExprData_termGetTerm(e->data);
2571
2572
2573         if (constraintTerm_isExprNode (t) )
2574         {
2575           return constraintTerm_simpleDivTypeExprNode(e, ct);
2576
2577           /* search for * size of ct and remove */
2578         }
2579         return constraintExpr_div (e, ct);
2580       }
2581
2582     case binaryexpr:
2583       {
2584         constraintExpr temp;
2585
2586         temp = constraintExprData_binaryExprGetExpr1 (e->data);
2587         temp = constraintExpr_copy(temp);
2588         temp = simpleDivType (temp, ct);
2589
2590         e->data = constraintExprData_binaryExprSetExpr1 (e->data, temp);
2591
2592         temp = constraintExprData_binaryExprGetExpr2 (e->data);
2593         temp = constraintExpr_copy(temp);
2594         temp = simpleDivType (temp, ct);
2595         e->data = constraintExprData_binaryExprSetExpr2 (e->data, temp);
2596
2597         DPRINTF(( (message("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e) ) )
2598             ));
2599
2600         return e;
2601       }
2602     case unaryExpr:
2603       return constraintExpr_div (e, ct);
2604
2605     default:
2606       BADEXIT;
2607     }
2608 }
2609
2610 static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr e, ctype ct)
2611 {
2612
2613   DPRINTF(( (message("constraintExpr_adjustMaxSetForCast got %s ", constraintExpr_unparse(e) ) )
2614             ));
2615
2616   e = constraintExpr_makeIncConstraintExpr(e);
2617
2618   e = constraintExpr_simplify(e);
2619
2620
2621   e = simpleDivType (e, ct);
2622
2623   e = constraintExpr_makeDecConstraintExpr(e);
2624
2625   e = constraintExpr_simplify(e);
2626
2627   DPRINTF(( (message("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e) ) )
2628             ));
2629
2630   return e;
2631 }
2632
2633
2634 bool  constraintExpr_isConstantOnly ( constraintExpr e )
2635 {
2636   DPRINTF(( (message("constraintExpr_isConstantOnly %s ",
2637                      constraintExpr_unparse(e) ) )
2638             ));
2639
2640   llassert(constraintExpr_isDefined(e) );
2641
2642   switch (e->kind)
2643     {
2644     case term:
2645       {
2646         constraintTerm t;
2647
2648         t = constraintExprData_termGetTerm(e->data);
2649
2650
2651         if (constraintTerm_isConstantOnly (t) )
2652           {
2653             return TRUE;
2654           }
2655         else
2656           {
2657             return FALSE;
2658           }
2659       }
2660
2661     case binaryexpr:
2662       {
2663         constraintExpr temp1, temp2;
2664
2665         temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
2666
2667         temp2 = constraintExprData_binaryExprGetExpr2 (e->data);
2668
2669         if (constraintExpr_isConstantOnly(temp1) &&
2670             constraintExpr_isConstantOnly(temp2) )
2671           {
2672             return TRUE;
2673           }
2674         else
2675           {
2676             return FALSE;
2677           }
2678       }
2679
2680     case unaryExpr:
2681       {
2682         constraintExpr temp;
2683
2684         temp = constraintExprData_unaryExprGetExpr (e->data );
2685
2686         if (constraintExpr_isConstantOnly(temp) )
2687           {
2688             return TRUE;
2689           }
2690         else
2691           {
2692             return FALSE;
2693           }
2694       }
2695     default:
2696       BADEXIT;
2697     }
2698 }
2699