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