[splint.git] / src / loopHeuristics.c

/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2003 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 splint: info@splint.org
** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/

/*
** loopHeuristics.c
*/

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

/* #define DEBUGPRINT 1 */

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

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

/* this file was created to split the loop heuristics functionality out of constraintGeneration.c and constraint.c*/
/*We need to access the internal representation of constraint
  see above for an explanation.
*/

/*@access  constraint @*/  

static bool isInc (/*@observer@*/ constraintExpr p_c) /*@*/;
static bool incVar (/*@notnull@*/ constraint p_c) /*@*/;


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 /*@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;
}

/*@access exprNode@*/
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_isIncOp (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;
}
/*@noaccess exprNode@*/


/*@access exprNode@*/
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_unparse (ltCon), constraintList_unparse (test->trueEnsuresConstraints) ) ));
  
  DPRINTF (( message ("getForTimes: incCon: %s from %s", constraintList_unparse (incCon), constraintList_unparse (inc->ensuresConstraints) ) ));
   
  constraintList_elements (ltCon, el) 
    {
      constraintList_elements (incCon, el2)
      {
	llassert(constraint_isDefined (el ) );
	
	if ( (constraint_isDefined (el ) ) && ( 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_isIncOp (tok) )
      {
	t1 = exprData_getUopNode (test->edata);
	t2 = exprData_getUopNode (inc->edata);
	
	llassert(exprNode_isDefined(t1)  && exprNode_isDefined(t2)  );
	if (sRef_sameName (t1->sref, t2->sref) )
	  {
	    return (constraintExpr_makeMaxSetExpr (t1) );
	  }
      }
  llassert ( FALSE);
  BADEXIT;
}
/*@noaccess exprNode@*/

/*@access constraintExpr @*/

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

    
  llassert (constraintExpr_isDefined (c) );
 
  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_isDefined (c) );
 
  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;
}

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


/*@access exprNode@*/


static void forLoopHeuristicsImpl ( exprNode e, exprNode forPred, /*@observer@*/ exprNode forBody)
{
  exprNode init, test, inc;

  constraintExpr iterations;

  llassert (exprNode_isDefined(forPred) );
  llassert (exprNode_isDefined(forBody) );
    
  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);
    }
}
/*@noaccess exprNode@*/

void exprNode_forLoopHeuristics ( exprNode e, exprNode forPred, exprNode forBody)
{
  forLoopHeuristicsImpl (e, forPred,  forBody);
}

 /*@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;
}
 /*@noaccess constraintExpr @*/

 /*@access constraintExpr @*/
/* 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 @*/


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