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