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