[splint.git] / src / loopHeuristics.c

/*
** LCLint - annotation-assisted static program checker
** Copyright (C) 1994-2001 University of Virginia,
**         Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** under the terms of the GNU General Public License as published by the
** Free Software Foundation; either version 2 of the License, or (at your
** option) any later version.
** 
** This program is distributed in the hope that it will be useful, but
** WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
** General Public License for more details.
** 
** The GNU General Public License is available from http://www.gnu.org/ or
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
** For information on lclint: lclint-request@cs.virginia.edu
** To report a bug: lclint-bug@cs.virginia.edu
** For more information: http://lclint.cs.virginia.edu
*/

/*
** loopHeuristics.c
*/

/*This file was formerly called forjunk.c C
  renamed Oct 8, 2001 - DRL
*/

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