src/constraintExpr.c

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