[splint.git] / src / forjunk.c

/*
** forjunk.c
*/

/* #define DEBUGPRINT 1 */

# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"

# include "exprChecks.h"
# include "exprNodeSList.h"

# include "exprDataQuite.i"

/*@access constraint, exprNode @*/

/*@access constraintExpr @*/

static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
{
  
  llassert(constraintExpr_isDefined(c) );
 if (c->kind == binaryexpr )
    {
      constraintExprBinaryOpKind binOP;
      constraintExpr t1, t2;
      t1 = constraintExprData_binaryExprGetExpr1 (c->data);
      t2 = constraintExprData_binaryExprGetExpr2 (c->data);

      binOP = constraintExprData_binaryExprGetOp (c->data);
      if (binOP == BINARYOP_PLUS)
	if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
	  {
	    return TRUE;
	  }
    }

 return FALSE;
}

/* look for constraints like cexrp = cexrp + 1 */
static bool incVar (/*@notnull@*/ constraint c) /*@*/
{
  constraintExpr t1;
  if (c->ar != EQ)
    {
      return FALSE;
    }
  if (! isInc (c->expr ) )
    return FALSE;

  llassert (constraintExpr_isDefined(c->expr) );
  llassert (c->expr->kind == binaryexpr);

  t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data);
  if (constraintExpr_similar (c->lexpr, t1) )
    return TRUE;

  return FALSE;
}
/*@noaccess constraintExpr @*/


static bool increments (/*@observer@*/ constraint c,
			/*@observer@*/ constraintExpr var)
{
  llassert(constraint_isDefined(c) );

  if (constraint_isUndefined(c) )
    {
      return FALSE;
    }

  llassert (incVar (c));
  if (constraintExpr_similar (c->lexpr, var) )
    return TRUE;
  else
    return FALSE;
}

static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
{
  
  exprNode init, test, inc, t1, t2;
  lltok tok;
  
  llassert(exprNode_isDefined (forPred) );
  llassert(exprNode_isDefined (forBody) );

  init  =  exprData_getTripleInit (forPred->edata);
  test  =   exprData_getTripleTest (forPred->edata);
  inc   =   exprData_getTripleInc (forPred->edata);

  llassert(exprNode_isDefined(test) );

  if (exprNode_isUndefined(test) )
    {
      return FALSE;
    }

  llassert(exprNode_isDefined(inc) );

  if (exprNode_isUndefined(inc) )
    {
      return FALSE;
    }

  if (test->kind != XPR_PREOP)
    return FALSE;
      
  tok = (exprData_getUopTok (test->edata));
  if (!lltok_isMult (tok) )
    {
      return FALSE;
    }

  /* should check preop too */
  if (inc->kind != XPR_POSTOP)
    {
      return FALSE;
    }
  
  tok = (exprData_getUopTok (inc->edata));
  if (lltok_isInc_Op (tok) )
      {
	t1 = exprData_getUopNode (test->edata);
	t2 = exprData_getUopNode (inc->edata);
	llassert(exprNode_isDefined(t2) && exprNode_isDefined(t2)  );

	if (exprNode_isUndefined(t1) || exprNode_isUndefined(t2)  )
	  {
	    return FALSE;
	  }

	if (sRef_sameName (t1->sref, t2->sref) )
	  {
	    return TRUE;
	  }
      }
  return FALSE;
}

static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c)
{
  constraintList ret;

  ret = constraintList_makeNew();
  constraintList_elements (c, el)
    {
      llassert(constraint_isDefined(el));
      if ( constraint_isUndefined(el)  )
      	continue;
      
      if (el->ar == LT || el->ar == LTE)
	{
	  constraint temp;
	  temp = constraint_copy(el);

	  ret = constraintList_add (ret, temp);
	}
    }
  end_constraintList_elements;

  return ret;
}

static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c)
{
  constraintList ret;

  ret = constraintList_makeNew();
  constraintList_elements (c, el)
    {
      llassert (constraint_isDefined (el));

      if (incVar (el) )
	{
	  constraint temp;
	  temp = constraint_copy(el);
	  ret = constraintList_add (ret, temp);
	}
    }
  end_constraintList_elements;
  
  return ret;
}

static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
{
  
  exprNode init, test, inc, t1, t2;
  constraintList ltCon;
  constraintList incCon;
  constraintExpr ret;
  
  lltok tok;
  
  init  =  exprData_getTripleInit (forPred->edata);
  test  =  exprData_getTripleTest (forPred->edata);
  inc   =  exprData_getTripleInc (forPred->edata);

  llassert(exprNode_isDefined(test) );
  llassert(exprNode_isDefined(inc) );
  
  ltCon =  getLessThanConstraints (test->trueEnsuresConstraints);
  incCon = getIncConstraints (inc->ensuresConstraints);
  
  DPRINTF(( message ("getForTimes: ltCon: %s from %s", constraintList_print(ltCon), constraintList_print(test->trueEnsuresConstraints) ) ));
  
  DPRINTF(( message ("getForTimes: incCon: %s from %s", constraintList_print(incCon), constraintList_print(inc->ensuresConstraints) ) ));
   
  constraintList_elements (ltCon, el) 
    {
      constraintList_elements(incCon, el2)
      {
	if ( increments(el2, el->lexpr) )
	  {
	    DPRINTF(( message ("getForTimes: %s increments %s", constraint_print(el2), constraint_print(el) ) ));
	    ret =  constraintExpr_copy (el->expr);
	    constraintList_free(ltCon);
	    constraintList_free(incCon);
	    return ret;

	  }
	else
	  DPRINTF(( message ("getForTimes: %s doesn't increment %s", constraint_print(el2), constraint_print(el) )   ));
      }
      end_constraintList_elements;
    }

  end_constraintList_elements;

  constraintList_free(ltCon);
  constraintList_free(incCon);
  
  DPRINTF (( message ("getForTimes: %s  %s resorting to ugly hack", exprNode_unparse(forPred), exprNode_unparse(forBody) ) ));
  if (! canGetForTimes (forPred, forBody) )
    {
      return NULL;
    }


  if (test->kind != XPR_PREOP)
    llassert (FALSE);
      
  tok = (exprData_getUopTok (test->edata));
  if (!lltok_isMult (tok) )
    {
      llassert ( FALSE );
    }

  /* should check preop too */
  if (inc->kind != XPR_POSTOP)
    {
      llassert (FALSE );
    }
  
  tok = (exprData_getUopTok (inc->edata));
  if (lltok_isInc_Op (tok) )
      {
	t1 = exprData_getUopNode (test->edata);
	t2 = exprData_getUopNode (inc->edata);
	if (sRef_sameName (t1->sref, t2->sref) )
	  {
	    return (constraintExpr_makeMaxSetExpr (t1) );
	  }
      }
  llassert( FALSE);
  BADEXIT;
}

/*@access constraintExpr @*/

static /*@only@*/ constraintExpr constraintExpr_searchAndAdd (/*@only@*/ constraintExpr c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
{
  constraintExprKind kind;
  constraintExpr temp;

  DPRINTF(( message ("Doing constraintExpr_searchAndAdd  %s %s %s ",
		     constraintExpr_unparse(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
  
  if ( constraintExpr_similar (c, find) )
    {

      constraintExpr newExpr;
      
      cstring cPrint;
      
      cPrint = constraintExpr_unparse(c);
      
      
      newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy(add) );

      DPRINTF((message ("Replacing %q with %q",
			cPrint, constraintExpr_unparse(newExpr)
			)));
      return newExpr;
    }

  kind = c->kind;
  
  switch (kind)
    {
    case term:
      break;      
    case unaryExpr:
      temp = constraintExprData_unaryExprGetExpr (c->data);
      temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
      c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
      break;           
    case binaryexpr:
      
      temp = constraintExprData_binaryExprGetExpr1 (c->data);
      temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
      c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
       
      temp = constraintExprData_binaryExprGetExpr2 (c->data);
      temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
      c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
      break;
    default:
      llassert(FALSE);
    }
  return c;
  
}

/*@noaccess constraintExpr @*/

static constraint  constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
{
  
  llassert (constraint_search (c, find)  );
  DPRINTF(( message ("Doing constraint_searchAndAdd  %s %s %s ",
		     constraint_print(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
  
  c->lexpr = constraintExpr_searchAndAdd (c->lexpr, find, add);
  c->expr =  constraintExpr_searchAndAdd (c->expr, find, add);

   c = constraint_simplify (c);
   c = constraint_simplify (c);

  return c;
  
}

 static constraintList constraintList_searchAndAdd (/*@returned@*/ constraintList list,
						   /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
{
  constraintList newConstraints;
  constraintList ret;
  
  newConstraints = constraintList_makeNew();
  
  constraintList_elements (list, el)
    {
      if (constraint_search (el, find) )
	{
	  constraint newExpr;
	  newExpr = constraint_copy (el);

	  newExpr = constraint_searchAndAdd (newExpr, find, add);
	  	  DPRINTF (( (message ("Adding constraint %s ", constraint_print (newExpr)) )  ));
	  newConstraints = constraintList_add (newConstraints, newExpr);
	}

    }
  end_constraintList_elements;
  
  ret =  constraintList_addListFree (list, newConstraints);
  return ret;
}

static void doAdjust(/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations)
{
  
  constraintList_elements (forBody->ensuresConstraints, el)
    {
      /* look for var = var + 1 */
      if (incVar(el) )
	{
	  DPRINTF((message ("Found inc variable constraint : %s", constraint_print (el) )  ));
	  forBody->requiresConstraints = constraintList_searchAndAdd(forBody->requiresConstraints, el->lexpr, iterations);
	}
    }
  end_constraintList_elements;
}

void exprNode_forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody)
{
  exprNode init, test, inc;

  constraintExpr iterations;
  
  init  =  exprData_getTripleInit (forPred->edata);
  test =   exprData_getTripleTest (forPred->edata);
  inc  =   exprData_getTripleInc (forPred->edata);

  if (exprNode_isError (test) || exprNode_isError (inc) )
    return;
  
  iterations = getForTimes (forPred, forBody );

  if (constraintExpr_isDefined (iterations) )
    {
      doAdjust ( e, forPred, forBody, iterations);
      constraintExpr_free(iterations);
    }
}


/*    else */
/*      { */
/*        DPRINTF (("Can't get for time ")); */
/*      } */
  
/*    if (exprNode_isError(init) ) */
/*      { */
/*        return; */
/*      } */
  
/*    if (init->kind == XPR_ASSIGN) */
/*      { */
/*        t1 = exprData_getOpA (init->edata); */
/*        t2 = exprData_getOpB (init->edata); */
      
/*        if (! (t1->kind == XPR_VAR) ) */
/*  	return; */
/*      } */
/*    else */
/*      return; */
  
/*    if (test->kind == XPR_FETCH) */
/*      { */
/*        t3 = exprData_getPairA (test->edata); */
/*        t4 = exprData_getPairB (test->edata); */
      
/*        if (sRef_sameName(t1->sref, t4->sref) ) */
/*  	{ */
/*  	  DPRINTF((message ("Found a for loop matching heuristic:%s", exprNode_unparse (forPred) ) )); */
/*  	  con = constraint_makeEnsureLteMaxRead(t1, t3); */
/*  	  forPred->ensuresConstraints = constraintList_add(forPred->ensuresConstraints, con);	   */
/*  	} */
/*        else */
/*  	{ */
/*  	  DPRINTF((message ("Didn't Find a for loop matching heuristic:%s %s and %s differ", exprNode_unparse (forPred), exprNode_unparse(t1), exprNode_unparse(t3) ) )); */
/*  	} */
/*        return; */
/*      } */
Commit	Line	Data
3aaedf88	1	/*
	2	** forjunk.c
	3	*/
	4
b7b694d6	5	/* #define DEBUGPRINT 1 */
3aaedf88	6
	7	# include <ctype.h> /* for isdigit */
	8	# include "lclintMacros.nf"
	9	# include "basic.h"
	10	# include "cgrammar.h"
	11	# include "cgrammar_tokens.h"
	12
	13	# include "exprChecks.h"
3aaedf88	14	# include "exprNodeSList.h"
3aaedf88	15
3aaedf88	16	# include "exprDataQuite.i"
3aaedf88	17
84c9ffbf	18	/@access constraint, exprNode @/
	19
	20	/@access constraintExpr @/
	21
bb25bea6	22	static bool isInc (/@observer@/ constraintExpr c) /@/
84c9ffbf	23	{
	24
	25	llassert(constraintExpr_isDefined(c) );
	26	if (c->kind == binaryexpr )
	27	{
	28	constraintExprBinaryOpKind binOP;
	29	constraintExpr t1, t2;
	30	t1 = constraintExprData_binaryExprGetExpr1 (c->data);
	31	t2 = constraintExprData_binaryExprGetExpr2 (c->data);
	32
	33	binOP = constraintExprData_binaryExprGetOp (c->data);
0c91982e	34	if (binOP == BINARYOP_PLUS)
84c9ffbf	35	if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
	36	{
	37	return TRUE;
	38	}
	39	}
	40
	41	return FALSE;
	42	}
	43
b7b694d6	44	/* look for constraints like cexrp = cexrp + 1 */
84c9ffbf	45	static bool incVar (/@notnull@/ constraint c) /@/
3aaedf88	46	{
	47	constraintExpr t1;
	48	if (c->ar != EQ)
	49	{
	50	return FALSE;
	51	}
	52	if (! isInc (c->expr ) )
	53	return FALSE;
	54
84c9ffbf	55	llassert (constraintExpr_isDefined(c->expr) );
3aaedf88	56	llassert (c->expr->kind == binaryexpr);
84c9ffbf	57
3aaedf88	58	t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data);
	59	if (constraintExpr_similar (c->lexpr, t1) )
	60	return TRUE;
	61
	62	return FALSE;
	63	}
84c9ffbf	64	/@noaccess constraintExpr @/
3aaedf88	65
3aaedf88	66
bb25bea6	67	static bool increments (/@observer@/ constraint c,
bb25bea6	68	/@observer@/ constraintExpr var)
3aaedf88	69	{
84c9ffbf	70	llassert(constraint_isDefined(c) );
	71
	72	if (constraint_isUndefined(c) )
	73	{
	74	return FALSE;
	75	}
	76
3aaedf88	77	llassert (incVar (c));
	78	if (constraintExpr_similar (c->lexpr, var) )
	79	return TRUE;
	80	else
	81	return FALSE;
	82	}
	83
84c9ffbf	84	static bool canGetForTimes (/@notnull@/ exprNode forPred, /@notnull@/ exprNode forBody)
3aaedf88	85	{
	86
	87	exprNode init, test, inc, t1, t2;
	88	lltok tok;
	89
84c9ffbf	90	llassert(exprNode_isDefined (forPred) );
	91	llassert(exprNode_isDefined (forBody) );
	92
3aaedf88	93	init = exprData_getTripleInit (forPred->edata);
	94	test = exprData_getTripleTest (forPred->edata);
	95	inc = exprData_getTripleInc (forPred->edata);
	96
84c9ffbf	97	llassert(exprNode_isDefined(test) );
	98
	99	if (exprNode_isUndefined(test) )
	100	{
	101	return FALSE;
	102	}
	103
	104	llassert(exprNode_isDefined(inc) );
	105
	106	if (exprNode_isUndefined(inc) )
	107	{
	108	return FALSE;
	109	}
	110
3aaedf88	111	if (test->kind != XPR_PREOP)
	112	return FALSE;
	113
	114	tok = (exprData_getUopTok (test->edata));
	115	if (!lltok_isMult (tok) )
	116	{
	117	return FALSE;
	118	}
	119
b7b694d6	120	/* should check preop too */
3aaedf88	121	if (inc->kind != XPR_POSTOP)
	122	{
	123	return FALSE;
	124	}
	125
	126	tok = (exprData_getUopTok (inc->edata));
	127	if (lltok_isInc_Op (tok) )
	128	{
	129	t1 = exprData_getUopNode (test->edata);
	130	t2 = exprData_getUopNode (inc->edata);
84c9ffbf	131	llassert(exprNode_isDefined(t2) && exprNode_isDefined(t2) );
	132
	133	if (exprNode_isUndefined(t1) \|\| exprNode_isUndefined(t2) )
	134	{
	135	return FALSE;
	136	}
	137
3aaedf88	138	if (sRef_sameName (t1->sref, t2->sref) )
	139	{
	140	return TRUE;
	141	}
	142	}
	143	return FALSE;
	144	}
	145
bb25bea6	146	static /@only@/ constraintList getLessThanConstraints (/@observer@/ constraintList c)
3aaedf88	147	{
	148	constraintList ret;
	149
c3e695ff	150	ret = constraintList_makeNew();
3aaedf88	151	constraintList_elements (c, el)
3aaedf88	152	{
84c9ffbf	153	llassert(constraint_isDefined(el));
	154	if ( constraint_isUndefined(el) )
	155	continue;
	156
3aaedf88	157	if (el->ar == LT \|\| el->ar == LTE)
3aaedf88	158	{
d46ce6a4	159	constraint temp;
	160	temp = constraint_copy(el);
	161
	162	ret = constraintList_add (ret, temp);
3aaedf88	163	}
	164	}
	165	end_constraintList_elements;
	166
	167	return ret;
	168	}
	169
bb25bea6	170	static /@only@/ constraintList getIncConstraints (/@observer@/ constraintList c)
3aaedf88	171	{
	172	constraintList ret;
	173
c3e695ff	174	ret = constraintList_makeNew();
3aaedf88	175	constraintList_elements (c, el)
3aaedf88	176	{
60eced23	177	llassert (constraint_isDefined (el));
60eced23	178
3aaedf88	179	if (incVar (el) )
3aaedf88	180	{
d46ce6a4	181	constraint temp;
	182	temp = constraint_copy(el);
	183	ret = constraintList_add (ret, temp);
3aaedf88	184	}
	185	}
	186	end_constraintList_elements;
	187
	188	return ret;
	189	}
	190
bb25bea6	191	static /@only@/ constraintExpr getForTimes (/@notnull@/ exprNode forPred, /@notnull@/ exprNode forBody)
3aaedf88	192	{
	193
	194	exprNode init, test, inc, t1, t2;
	195	constraintList ltCon;
	196	constraintList incCon;
bb25bea6	197	constraintExpr ret;
3aaedf88	198
	199	lltok tok;
	200
	201	init = exprData_getTripleInit (forPred->edata);
	202	test = exprData_getTripleTest (forPred->edata);
	203	inc = exprData_getTripleInc (forPred->edata);
	204
84c9ffbf	205	llassert(exprNode_isDefined(test) );
84c9ffbf	206	llassert(exprNode_isDefined(inc) );
3aaedf88	207
	208	ltCon = getLessThanConstraints (test->trueEnsuresConstraints);
	209	incCon = getIncConstraints (inc->ensuresConstraints);
	210
	211	DPRINTF(( message ("getForTimes: ltCon: %s from %s", constraintList_print(ltCon), constraintList_print(test->trueEnsuresConstraints) ) ));
	212
	213	DPRINTF(( message ("getForTimes: incCon: %s from %s", constraintList_print(incCon), constraintList_print(inc->ensuresConstraints) ) ));
	214
	215	constraintList_elements (ltCon, el)
	216	{
dc92450f	217	constraintList_elements(incCon, el2)
3aaedf88	218	{
	219	if ( increments(el2, el->lexpr) )
	220	{
	221	DPRINTF(( message ("getForTimes: %s increments %s", constraint_print(el2), constraint_print(el) ) ));
bb25bea6	222	ret = constraintExpr_copy (el->expr);
	223	constraintList_free(ltCon);
	224	constraintList_free(incCon);
	225	return ret;
3aaedf88	226
	227	}
	228	else
	229	DPRINTF(( message ("getForTimes: %s doesn't increment %s", constraint_print(el2), constraint_print(el) ) ));
	230	}
	231	end_constraintList_elements;
	232	}
	233
	234	end_constraintList_elements;
bb25bea6	235
	236	constraintList_free(ltCon);
	237	constraintList_free(incCon);
3aaedf88	238
	239	DPRINTF (( message ("getForTimes: %s %s resorting to ugly hack", exprNode_unparse(forPred), exprNode_unparse(forBody) ) ));
	240	if (! canGetForTimes (forPred, forBody) )
	241	{
	242	return NULL;
	243	}
	244
	245
	246	if (test->kind != XPR_PREOP)
	247	llassert (FALSE);
	248
	249	tok = (exprData_getUopTok (test->edata));
	250	if (!lltok_isMult (tok) )
	251	{
	252	llassert ( FALSE );
	253	}
	254
b7b694d6	255	/* should check preop too */
3aaedf88	256	if (inc->kind != XPR_POSTOP)
	257	{
	258	llassert (FALSE );
	259	}
	260
	261	tok = (exprData_getUopTok (inc->edata));
	262	if (lltok_isInc_Op (tok) )
	263	{
	264	t1 = exprData_getUopNode (test->edata);
	265	t2 = exprData_getUopNode (inc->edata);
	266	if (sRef_sameName (t1->sref, t2->sref) )
	267	{
	268	return (constraintExpr_makeMaxSetExpr (t1) );
	269	}
	270	}
	271	llassert( FALSE);
	272	BADEXIT;
	273	}
	274
84c9ffbf	275	/@access constraintExpr @/
3aaedf88	276
bb25bea6	277	static /@only@/ constraintExpr constraintExpr_searchAndAdd (/@only@/ constraintExpr c, /@observer@/ constraintExpr find, /@observer@/ constraintExpr add)
3aaedf88	278	{
	279	constraintExprKind kind;
	280	constraintExpr temp;
	281
	282	DPRINTF(( message ("Doing constraintExpr_searchAndAdd %s %s %s ",
	283	constraintExpr_unparse(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
	284
	285	if ( constraintExpr_similar (c, find) )
	286	{
3aaedf88	287
28bf4b0b	288	constraintExpr newExpr;
bb25bea6	289
	290	cstring cPrint;
	291
	292	cPrint = constraintExpr_unparse(c);
	293
	294
28bf4b0b	295	newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy(add) );
3aaedf88	296
bb25bea6	297	DPRINTF((message ("Replacing %q with %q",
28bf4b0b	298	cPrint, constraintExpr_unparse(newExpr)
3aaedf88	299	)));
28bf4b0b	300	return newExpr;
3aaedf88	301	}
	302
	303	kind = c->kind;
	304
	305	switch (kind)
	306	{
	307	case term:
	308	break;
	309	case unaryExpr:
	310	temp = constraintExprData_unaryExprGetExpr (c->data);
bb25bea6	311	temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
3aaedf88	312	c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
	313	break;
	314	case binaryexpr:
	315
	316	temp = constraintExprData_binaryExprGetExpr1 (c->data);
bb25bea6	317	temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
3aaedf88	318	c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
	319
	320	temp = constraintExprData_binaryExprGetExpr2 (c->data);
bb25bea6	321	temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
3aaedf88	322	c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
	323	break;
	324	default:
	325	llassert(FALSE);
	326	}
	327	return c;
	328
	329	}
	330
84c9ffbf	331	/@noaccess constraintExpr @/
84c9ffbf	332
bb25bea6	333	static constraint constraint_searchAndAdd (/@returned@/ constraint c, /@observer@/ constraintExpr find, /@observer@/ constraintExpr add)
3aaedf88	334	{
	335
	336	llassert (constraint_search (c, find) );
	337	DPRINTF(( message ("Doing constraint_searchAndAdd %s %s %s ",
	338	constraint_print(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
	339
	340	c->lexpr = constraintExpr_searchAndAdd (c->lexpr, find, add);
	341	c->expr = constraintExpr_searchAndAdd (c->expr, find, add);
	342
	343	c = constraint_simplify (c);
	344	c = constraint_simplify (c);
	345
	346	return c;
	347
	348	}
	349
28bf4b0b	350	static constraintList constraintList_searchAndAdd (/@returned@/ constraintList list,
bb25bea6	351	/@observer@/ constraintExpr find, /@observer@/ constraintExpr add)
3aaedf88	352	{
	353	constraintList newConstraints;
	354	constraintList ret;
	355
c3e695ff	356	newConstraints = constraintList_makeNew();
3aaedf88	357
	358	constraintList_elements (list, el)
	359	{
	360	if (constraint_search (el, find) )
	361	{
28bf4b0b	362	constraint newExpr;
28bf4b0b	363	newExpr = constraint_copy (el);
3aaedf88	364
28bf4b0b	365	newExpr = constraint_searchAndAdd (newExpr, find, add);
	366	DPRINTF (( (message ("Adding constraint %s ", constraint_print (newExpr)) ) ));
	367	newConstraints = constraintList_add (newConstraints, newExpr);
3aaedf88	368	}
	369
	370	}
	371	end_constraintList_elements;
	372
4ab867d6	373	ret = constraintList_addListFree (list, newConstraints);
3aaedf88	374	return ret;
	375	}
	376
bb25bea6	377	static void doAdjust(/@unused@/ exprNode e, /@unused@/ exprNode forPred, /@observer@/ exprNode forBody, /@observer@/ constraintExpr iterations)
3aaedf88	378	{
	379
	380	constraintList_elements (forBody->ensuresConstraints, el)
	381	{
b7b694d6	382	/* look for var = var + 1 */
3aaedf88	383	if (incVar(el) )
	384	{
	385	DPRINTF((message ("Found inc variable constraint : %s", constraint_print (el) ) ));
	386	forBody->requiresConstraints = constraintList_searchAndAdd(forBody->requiresConstraints, el->lexpr, iterations);
	387	}
	388	}
	389	end_constraintList_elements;
	390	}
	391
28bf4b0b	392	void exprNode_forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody)
3aaedf88	393	{
84c9ffbf	394	exprNode init, test, inc;
84c9ffbf	395
3aaedf88	396	constraintExpr iterations;
	397
	398	init = exprData_getTripleInit (forPred->edata);
	399	test = exprData_getTripleTest (forPred->edata);
	400	inc = exprData_getTripleInc (forPred->edata);
	401
	402	if (exprNode_isError (test) \|\| exprNode_isError (inc) )
	403	return;
	404
	405	iterations = getForTimes (forPred, forBody );
	406
28bf4b0b	407	if (constraintExpr_isDefined (iterations) )
3aaedf88	408	{
3aaedf88	409	doAdjust ( e, forPred, forBody, iterations);
bb25bea6	410	constraintExpr_free(iterations);
3aaedf88	411	}
3aaedf88	412	}
	413
	414
	415	/* else */
	416	/* { */
	417	/* DPRINTF (("Can't get for time ")); */
	418	/* } */
	419
	420	/* if (exprNode_isError(init) ) */
	421	/* { */
	422	/* return; */
	423	/* } */
	424
	425	/* if (init->kind == XPR_ASSIGN) */
	426	/* { */
	427	/* t1 = exprData_getOpA (init->edata); */
	428	/* t2 = exprData_getOpB (init->edata); */
	429
	430	/* if (! (t1->kind == XPR_VAR) ) */
	431	/* return; */
	432	/* } */
	433	/* else */
	434	/* return; */
	435
	436	/* if (test->kind == XPR_FETCH) */
	437	/* { */
	438	/* t3 = exprData_getPairA (test->edata); */
	439	/* t4 = exprData_getPairB (test->edata); */
	440
	441	/* if (sRef_sameName(t1->sref, t4->sref) ) */
	442	/* { */
	443	/* DPRINTF((message ("Found a for loop matching heuristic:%s", exprNode_unparse (forPred) ) )); */
	444	/* con = constraint_makeEnsureLteMaxRead(t1, t3); */
	445	/* forPred->ensuresConstraints = constraintList_add(forPred->ensuresConstraints, con); */
	446	/* } */
	447	/* else */
	448	/* { */
	449	/* DPRINTF((message ("Didn't Find a for loop matching heuristic:%s %s and %s differ", exprNode_unparse (forPred), exprNode_unparse(t1), exprNode_unparse(t3) ) )); */
	450	/* } */
	451	/* return; */
	452	/* } */