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