[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 "aliasChecks.h"
# include "exprNodeSList.h"

# include "exprData.i"
# 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 == 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)
    {
      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) )
    {
      #warning mem leak

      constraintExpr new;
      
      cstring cPrint;
      
      cPrint = constraintExpr_unparse(c);
      
      
      new = constraintExpr_makeAddConstraintExpr (c, constraintExpr_copy(add) );

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

  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;
  
}

/*@only@*/ 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 new;
	  new = constraint_copy (el);

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

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