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 constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ constraintExpr old)
1056 {
1057   bool ret = FALSE;
1058   constraintExprKind kind;
1059   constraintExpr temp;
1060
1061   if ( constraintExpr_similar (c, old) )
1062     {
1063       DPRINTF((message ("Found  %q",
1064                         constraintExpr_unparse(old)
1065                         )));
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_print (constraintExprData_termGetTerm (ex->data)));
1547               }
1548             else
1549               {
1550                 st = message ("%q", constraintTerm_print (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 EXPRNODE:
1912       break;
1913     case INTLITERAL:
1914       break;
1915
1916     case SREF:
1917       s = constraintTerm_getSRef(t);
1918       if (sRef_isResult (s))
1919         {
1920           ret = constraintExpr_makeExprNode(fcnCall);
1921           constraintExpr_free(e);
1922           e = NULL;
1923         }
1924       else
1925         {
1926           e = NULL;
1927         }
1928       break;
1929     default:
1930       BADEXIT;
1931     }
1932
1933   return ret;
1934
1935 }
1936 /*
1937 / *@only@* / static constraintExpr
1938 doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
1939  sRef s, ctype ct)
1940 {
1941   constraintTerm t;
1942
1943   constraintExprData data = e->data;
1944
1945   constraintExprKind kind = e->kind;
1946
1947   constraintExpr ret;
1948
1949   llassert(kind == term);
1950
1951   t = constraintExprData_termGetTerm (data);
1952   llassert (constraintTerm_isDefined(t) );
1953
1954   ret = e;
1955
1956   DPRINTF (("Fixing: %s", constraintExpr_print (e)));
1957
1958   switch (constraintTerm_getKind(t))
1959     {
1960     case EXPRNODE:
1961       DPRINTF((message ("%q @ %q ", constraintTerm_print(t),
1962                         fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
1963       break;
1964     case INTLITERAL:
1965       DPRINTF((message (" %q ", constraintTerm_print (t)) ));
1966       break;
1967
1968     case SREF:
1969       / * evans 2001-07-24: constants should use the original term * /
1970       if (!constraintTerm_canGetValue (t))
1971         {
1972           sRef snew;
1973           DPRINTF ((message("Doing sRef_fixInvarConstraint for %q ",
1974                              constraintTerm_print (t) ) ));
1975
1976           snew = fixSref (ct, s, constraintTerm_getSRef(t));
1977
1978           ret = constraintExpr_makeTermsRef(snew);
1979
1980           constraintExpr_free (e);
1981
1982           DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
1983                              constraintExpr_print (ret) ) ));
1984           / *@-branchstate@* /
1985         } / *@=branchstate@* /
1986
1987       break;
1988     default:
1989       BADEXIT;
1990     }
1991
1992   return ret;
1993
1994 }
1995 */
1996
1997 /*drl moved from constriantTerm.c 5/20/001*/
1998 /*@only@*/ static constraintExpr
1999 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
2000 {
2001   constraintTerm t;
2002
2003   constraintExprData data;
2004
2005   constraintExprKind kind;
2006
2007   constraintExpr ret;
2008
2009
2010   llassert(constraintExpr_isDefined (e) );
2011
2012   data = e->data;
2013
2014   kind = e->kind;
2015
2016
2017
2018   llassert(kind == term);
2019
2020   t = constraintExprData_termGetTerm (data);
2021   llassert (constraintTerm_isDefined(t) );
2022
2023   ret = e;
2024
2025   DPRINTF (("Fixing: %s", constraintExpr_print (e)));
2026
2027   switch (constraintTerm_getKind(t))
2028     {
2029     case EXPRNODE:
2030       DPRINTF((message ("%q @ %q ", constraintTerm_print(t),
2031                         fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
2032       break;
2033     case INTLITERAL:
2034       DPRINTF((message (" %q ", constraintTerm_print (t)) ));
2035       break;
2036
2037     case SREF:
2038       /* evans 2001-07-24: constants should use the original term */
2039       if (!constraintTerm_canGetValue (t))
2040         {
2041           DPRINTF ((message("Doing sRef_fixConstraintParam for %q ",
2042                              constraintTerm_print (t) ) ));
2043           ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
2044
2045           constraintExpr_free (e);
2046
2047           DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
2048                              constraintExpr_print (ret) ) ));
2049           /*@-branchstate@*/
2050         } /*@=branchstate@*/
2051
2052       break;
2053     default:
2054       BADEXIT;
2055     }
2056
2057   return ret;
2058
2059 }
2060
2061
2062 #if 0
2063 bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term)
2064 {
2065   if (constraintTerm_hasTerm (expr->term, term) )
2066     return TRUE;
2067
2068   if ((expr->expr) != NULL)
2069     {
2070       return ( constraintExpr_includesTerm (expr->expr, term) );
2071     }
2072   return FALSE;
2073
2074 }
2075 #endif
2076
2077 /*drl added 6/11/01 */
2078 bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c)
2079 {
2080
2081   llassert(constraintExpr_isDefined (c) );
2082
2083   if ( ! (constraintExpr_isDefined (c) ) )
2084     return FALSE;
2085
2086   if (c->kind == binaryexpr)
2087     return TRUE;
2088
2089   else
2090     return FALSE;
2091 }
2092
2093 /*drl added 8/08/001 */
2094 bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
2095 {
2096   llassert(constraintExpr_isDefined (c) );
2097
2098   if (c->kind == term)
2099     return TRUE;
2100
2101   else
2102     return FALSE;
2103 }
2104
2105 /*@observer@*/ /*@temp@*/ constraintTerm constraintExpr_getTerm ( /*@temp@*/ /*@observer@*/ constraintExpr c) /*@*/
2106 {
2107   constraintTerm term;
2108
2109   llassert(constraintExpr_isDefined (c) );
2110
2111   llassert(constraintExpr_isTerm(c) );
2112
2113   term = constraintExprData_termGetTerm(c->data);
2114
2115   return term;
2116 }
2117
2118 static void  binaryExpr_dump (/*@observer@*/ constraintExprData data,  FILE *f)
2119 {
2120   constraintExpr expr1;
2121   constraintExprBinaryOpKind binaryOp;
2122   constraintExpr expr2;
2123
2124
2125   binaryOp = constraintExprData_binaryExprGetOp (data);
2126
2127   fprintf(f, "%d\n", (int) binaryOp);
2128
2129   expr1 = constraintExprData_binaryExprGetExpr1 (data);
2130   expr2 = constraintExprData_binaryExprGetExpr2 (data);
2131
2132   fprintf(f, "e1\n");
2133
2134   constraintExpr_dump(expr1, f);
2135
2136   fprintf(f, "e2\n");
2137   constraintExpr_dump(expr2, f);
2138 }
2139
2140
2141 static constraintExpr  binaryExpr_undump (FILE *f)
2142 {
2143   constraintExpr expr1;
2144   constraintExprBinaryOpKind binaryOp;
2145   constraintExpr expr2;
2146
2147   constraintExpr ret;
2148
2149
2150
2151   char * str;
2152   char * os;
2153
2154   os = mstring_create (MAX_DUMP_LINE_LENGTH);
2155
2156   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2157
2158   if (! mstring_isDefined(str) )
2159     {
2160       llfatalbug(message("Library file is corrupted") );
2161     }
2162
2163   binaryOp = (constraintExprBinaryOpKind) reader_getInt(&str);
2164
2165   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2166
2167   if (! mstring_isDefined(str) )
2168     {
2169       llfatalbug(message("Library file is corrupted") );
2170     }
2171
2172   reader_checkChar (&str, 'e');
2173   reader_checkChar (&str, '1');
2174
2175   expr1 = constraintExpr_undump (f);
2176
2177   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2178
2179   reader_checkChar (&str, 'e');
2180   reader_checkChar (&str, '2');
2181
2182   expr2 = constraintExpr_undump (f);
2183
2184   ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
2185   ret->data = constraintExprData_binaryExprSetOp(ret->data, binaryOp);
2186
2187   free(os);
2188   return ret;
2189 }
2190
2191
2192
2193 static void  unaryExpr_dump (/*@observer@*/ constraintExprData data,  FILE *f)
2194 {
2195
2196   constraintExpr expr;
2197   constraintExprUnaryOpKind unaryOp;
2198
2199   unaryOp = constraintExprData_unaryExprGetOp (data);
2200
2201   fprintf(f, "%d\n", (int) unaryOp);
2202
2203   expr = constraintExprData_unaryExprGetExpr (data);
2204
2205   constraintExpr_dump(expr, f);
2206 }
2207
2208 static  constraintExpr  unaryExpr_undump ( FILE *f)
2209 {
2210
2211   constraintExpr expr;
2212   constraintExprUnaryOpKind unaryOp;
2213   constraintExpr ret;
2214
2215   char * str;
2216   char * os;
2217
2218   str = mstring_create (MAX_DUMP_LINE_LENGTH);
2219   os = str;
2220   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2221
2222   if (! mstring_isDefined(str) )
2223     {
2224       llfatalbug(message("Library file is corrupted") );
2225     }
2226
2227   unaryOp = (constraintExprUnaryOpKind) reader_getInt(&str);
2228
2229   expr = constraintExpr_undump (f);
2230
2231   ret = constraintExpr_makeUnaryOp (expr, unaryOp);
2232
2233   free(os);
2234
2235   return ret;
2236 }
2237
2238 void  constraintExpr_dump (/*@observer@*/ constraintExpr expr,  FILE *f)
2239 {
2240   constraintExprKind kind;
2241   constraintTerm t;
2242
2243
2244   llassert(constraintExpr_isDefined(expr) );
2245
2246   DPRINTF((message("constraintExpr_dump:: dumping constraintExpr %s",
2247                    constraintExpr_unparse(expr)
2248                    ) ));
2249
2250   kind = expr->kind;
2251
2252   fprintf(f,"%d\n", (int) kind);
2253
2254   switch (kind)
2255     {
2256     case term:
2257       t = constraintExprData_termGetTerm (expr->data);
2258       constraintTerm_dump (t, f);
2259       break;
2260     case unaryExpr:
2261       unaryExpr_dump (expr->data, f);
2262       break;
2263     case binaryexpr:
2264       binaryExpr_dump  (expr->data, f);
2265       break;
2266     }
2267 }
2268
2269 /*@only@*/ constraintExpr  constraintExpr_undump (FILE *f)
2270 {
2271   constraintExprKind kind;
2272   constraintTerm t;
2273   constraintExpr ret;
2274
2275   char * s;
2276   char * os;
2277
2278   s = mstring_create (MAX_DUMP_LINE_LENGTH);
2279
2280   os = s;
2281
2282   s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
2283
2284   if (! mstring_isDefined(s) )
2285     {
2286       llfatalbug(message("Library file is corrupted") );
2287     }
2288
2289   kind = (constraintExprKind) reader_getInt(&s);
2290
2291   free (os);
2292
2293   switch (kind)
2294     {
2295     case term:
2296       t = constraintTerm_undump (f);
2297       ret = constraintExpr_makeTerm(t);
2298       break;
2299     case unaryExpr:
2300       ret = unaryExpr_undump (f);
2301       break;
2302     case binaryexpr:
2303       ret = binaryExpr_undump  (f);
2304       break;
2305     }
2306
2307   return ret;
2308
2309 }
2310
2311 int constraintExpr_getDepth (constraintExpr ex)
2312 {
2313   int ret;
2314
2315   constraintExprKind kind;
2316
2317   llassert (ex != NULL);
2318
2319   kind = ex->kind;
2320
2321   switch (kind)
2322     {
2323     case term:
2324       ret = 1;
2325       break;
2326     case unaryExpr:
2327       ret =  constraintExpr_getDepth (constraintExprData_unaryExprGetExpr (ex->data) );
2328       ret++;
2329
2330       break;
2331     case binaryexpr:
2332       ret = 0;
2333       ret = constraintExpr_getDepth (constraintExprData_binaryExprGetExpr1 (ex->data) );
2334
2335       ret++;
2336
2337       ret += constraintExpr_getDepth (constraintExprData_binaryExprGetExpr2 (ex->data) );
2338
2339       break;
2340     default:
2341       BADEXIT;
2342     }
2343
2344   return ret;
2345 }
2346
2347
2348 bool  constraintExpr_canGetCType (constraintExpr e) /*@*/
2349 {
2350   if (constraintExpr_isUndefined(e) )
2351     return FALSE;
2352
2353   if (e->kind == term)
2354     {
2355       return TRUE;
2356     }
2357   else
2358     {
2359       DPRINTF(( message("constraintExpr_canGetCType: can't get type for %s ",
2360                         constraintExpr_print(e) ) ));
2361       return FALSE;
2362     }
2363 }
2364
2365 ctype constraintExpr_getCType (constraintExpr e) /*@*/
2366 {
2367   constraintTerm t;
2368
2369   llassert(constraintExpr_isDefined(e) );
2370
2371   llassert(constraintExpr_canGetCType(e) );
2372
2373   switch (e->kind)
2374     {
2375     case term:
2376       t = constraintExprData_termGetTerm (e->data);
2377       return (constraintTerm_getCType(t) );
2378       /* assume that a unary expression will be an int ... */
2379     case unaryExpr:
2380       return ctype_signedintegral;
2381
2382       /* drl for just return type of first operand */
2383     case binaryexpr:
2384       return (
2385               constraintExpr_getCType
2386               (constraintExprData_binaryExprGetExpr1 (e->data) )
2387               );
2388     default:
2389       BADEXIT;
2390     }
2391   BADEXIT;
2392 }
2393
2394 /* drl add 10-5-001 */
2395
2396 static bool constraintExpr_hasTypeChange(constraintExpr e)
2397 {
2398   llassert(constraintExpr_isDefined(e) );
2399   if (constraintExpr_isDefined((e)) && (e->ct == TRUE) )
2400     {
2401       return TRUE;
2402     }
2403
2404   if (e->kind == unaryExpr)
2405     {
2406       if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
2407         {
2408           constraintExpr ce;
2409
2410           ce = constraintExprData_unaryExprGetExpr(e->data);
2411
2412           return (constraintExpr_hasTypeChange(ce) );
2413         }
2414
2415     }
2416   return FALSE;
2417 }
2418
2419 /* drl add 10-5-001 */
2420
2421 static ctype constraintExpr_getOrigType (constraintExpr e)
2422 {
2423
2424   llassert(constraintExpr_isDefined(e) );
2425   llassert(constraintExpr_hasTypeChange(e) );
2426
2427
2428   if (e->ct == TRUE)
2429     {
2430       return e->origType;
2431     }
2432
2433   if (e->kind == unaryExpr)
2434     {
2435       if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
2436         {
2437           constraintExpr ce;
2438
2439           ce = constraintExprData_unaryExprGetExpr(e->data);
2440
2441           return (constraintExpr_getOrigType(ce) );
2442         }
2443
2444     }
2445
2446   BADEXIT;
2447 }
2448
2449 /*drl added these around 10/18/001*/
2450
2451 static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e, /*@unused@*/ ctype ct)
2452 {
2453   return e;
2454 }
2455
2456
2457 /*@access exprNode@*/
2458 static /*@only@*/ constraintExpr  constraintTerm_simpleDivTypeExprNode(/*@only@*/ constraintExpr e, ctype ct)
2459 {
2460   exprData data;
2461   exprNode t1, t2, expr;
2462   lltok tok;
2463   constraintTerm t;
2464
2465   llassert(constraintExpr_isDefined(e) );
2466
2467   DPRINTF((
2468            message("constraintTerm_simpleDivTypeExprNode e=%s, ct=%s",
2469                    constraintExpr_print(e), ctype_unparse(ct)
2470                    )
2471            ));
2472
2473   t = constraintExprData_termGetTerm(e->data);
2474
2475   expr = constraintTerm_getExprNode(t);
2476
2477   llassert(constraintExpr_isDefined(e) );
2478   llassert(exprNode_isDefined(expr) );
2479
2480   if (expr->kind == XPR_OP)
2481     {
2482       data = expr->edata;
2483
2484       t1 = exprData_getOpA (data);
2485       t2 = exprData_getOpB (data);
2486       tok = exprData_getOpTok (data);
2487       if (lltok_isMult(tok) )
2488         {
2489           llassert(exprNode_isDefined(t1) && exprNode_isDefined(t2) );
2490           /*drl 3/2/2003 we know this from the fact that it's a
2491             multiplication operation...*/
2492
2493           if  ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
2494             {
2495               ctype ct2;
2496
2497               if (t1->kind == XPR_SIZEOFT)
2498                 {
2499                   ct2 = qtype_getType (exprData_getType (t1->edata));
2500                 }
2501               else
2502                 {
2503                   exprNode tempE;
2504
2505                   tempE = exprData_getSingle (t1->edata);
2506
2507                   ct2 =  exprNode_getType (tempE);
2508                 }
2509               if (ctype_match (ctype_makePointer(ct2), ct) )
2510                 {
2511                   /* this is a bit sloopy but ... */
2512                                   constraintExpr_free(e);
2513                   return constraintExpr_makeExprNode(t2);
2514                 }
2515             }
2516
2517
2518           else   if  ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
2519             {
2520               ctype ct2;
2521
2522               if (t2->kind == XPR_SIZEOFT)
2523                 {
2524                   ct2 = qtype_getType (exprData_getType (t2->edata));
2525                 }
2526               else
2527                 {
2528                   exprNode exprTemp;
2529                   exprData eDTemp;
2530
2531                   exprTemp = exprData_getSingle (t2->edata);
2532
2533                   llassert(exprNode_isDefined(exprTemp) );
2534                   eDTemp = exprTemp->edata;
2535
2536                   ct2 = qtype_getType (exprData_getType(eDTemp ) );
2537
2538                 }
2539               if (ctype_match (ctype_makePointer(ct2),ct) )
2540                 {
2541                   /* sloopy way to do this... */ /*@i22*/
2542                                   constraintExpr_free(e);
2543                   return constraintExpr_makeExprNode(t1);
2544                 }
2545             }
2546           else
2547             {
2548               /*empty*/
2549             }
2550
2551         }
2552     }
2553   return (constraintExpr_div (e, ct) );
2554 }
2555 /*@noaccess exprNode@*/
2556
2557 static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype ct)
2558 {
2559   /*@i333*/
2560   DPRINTF(( (message("simpleDiv got %s ", constraintExpr_unparse(e) ) )
2561             ));
2562
2563   llassert(constraintExpr_isDefined(e) );
2564
2565   switch (e->kind)
2566     {
2567     case term:
2568
2569       {
2570         constraintTerm t;
2571
2572         t = constraintExprData_termGetTerm(e->data);
2573
2574
2575         if (constraintTerm_isExprNode (t) )
2576         {
2577           return constraintTerm_simpleDivTypeExprNode(e, ct);
2578
2579           /* search for * size of ct and remove */
2580         }
2581         return constraintExpr_div (e, ct);
2582       }
2583
2584     case binaryexpr:
2585       {
2586         constraintExpr temp;
2587
2588         temp = constraintExprData_binaryExprGetExpr1 (e->data);
2589         temp = constraintExpr_copy(temp);
2590         temp = simpleDivType (temp, ct);
2591
2592         e->data = constraintExprData_binaryExprSetExpr1 (e->data, temp);
2593
2594         temp = constraintExprData_binaryExprGetExpr2 (e->data);
2595         temp = constraintExpr_copy(temp);
2596         temp = simpleDivType (temp, ct);
2597         e->data = constraintExprData_binaryExprSetExpr2 (e->data, temp);
2598
2599         DPRINTF(( (message("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e) ) )
2600             ));
2601
2602         return e;
2603       }
2604     case unaryExpr:
2605       return constraintExpr_div (e, ct);
2606
2607     default:
2608       BADEXIT;
2609     }
2610 }
2611
2612 static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr e, ctype ct)
2613 {
2614
2615   DPRINTF(( (message("constraintExpr_adjustMaxSetForCast got %s ", constraintExpr_unparse(e) ) )
2616             ));
2617
2618   e = constraintExpr_makeIncConstraintExpr(e);
2619
2620   e = constraintExpr_simplify(e);
2621
2622
2623   e = simpleDivType (e, ct);
2624
2625   e = constraintExpr_makeDecConstraintExpr(e);
2626
2627   e = constraintExpr_simplify(e);
2628
2629   DPRINTF(( (message("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e) ) )
2630             ));
2631
2632   return e;
2633 }
2634
2635
2636 bool  constraintExpr_isConstantOnly ( constraintExpr e )
2637 {
2638   DPRINTF(( (message("constraintExpr_isConstantOnly %s ",
2639                      constraintExpr_unparse(e) ) )
2640             ));
2641
2642   llassert(constraintExpr_isDefined(e) );
2643
2644   switch (e->kind)
2645     {
2646     case term:
2647       {
2648         constraintTerm t;
2649
2650         t = constraintExprData_termGetTerm(e->data);
2651
2652
2653         if (constraintTerm_isConstantOnly (t) )
2654           {
2655             return TRUE;
2656           }
2657         else
2658           {
2659             return FALSE;
2660           }
2661       }
2662
2663     case binaryexpr:
2664       {
2665         constraintExpr temp1, temp2;
2666
2667         temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
2668
2669         temp2 = constraintExprData_binaryExprGetExpr2 (e->data);
2670
2671         if (constraintExpr_isConstantOnly(temp1) &&
2672             constraintExpr_isConstantOnly(temp2) )
2673           {
2674             return TRUE;
2675           }
2676         else
2677           {
2678             return FALSE;
2679           }
2680       }
2681
2682     case unaryExpr:
2683       {
2684         constraintExpr temp;
2685
2686         temp = constraintExprData_unaryExprGetExpr (e->data );
2687
2688         if (constraintExpr_isConstantOnly(temp) )
2689           {
2690             return TRUE;
2691           }
2692         else
2693           {
2694             return FALSE;
2695           }
2696       }
2697     default:
2698       BADEXIT;
2699     }
2700 }
2701