[splint.git] / src / constraintTerm.c

/*
** constraintTerm.c
*/

# 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"

int constraintTerm_getValue (constraintTerm term)
{
  if (term->kind == EXPRNODE)
    {
      return (multiVal_forceInt (term->value.expr->val) );
    }
  if (term->kind == INTLITERAL )
    {
      return (term->value.intlit);
    }
  llassert(FALSE);
  return 0;
}

/*@out@*/ static  constraintTerm new_constraintTermExpr (void)
{
  constraintTerm ret;
  ret = dmalloc (sizeof (* ret ) );
  return ret;
}

constraintTerm constraintTerm_simplify (constraintTerm term)
{
  if (term->constrType == VALUE)
    {
      if (term->kind == EXPRNODE)
	{
	  if ( exprNode_knownIntValue (term->value.expr ) )
	    {
	      int temp;
	      temp  = exprNode_getLongValue (term->value.expr);
	      term->value.intlit = temp;
	      term->kind = INTLITERAL;
	    }
	  
	}

    }

  if (term->kind == CONSTRAINTEXPR )
    {
      if ( (term->constrType == MAXREAD) || (term->constrType == MAXSET) )
	{
	  // ms(var + intlit) = ms (var) - intlit
	  if (term->value.constrExpr->expr == NULL)
	    return term;

	  if (term->value.constrExpr->expr->term->kind == INTLITERAL)
	    {
	      if (term->constrType == MAXREAD) 
		term->value.constrExpr->term->constrType = MAXREAD;
	      else if (term->constrType == MAXSET) 
		term->value.constrExpr->term->constrType = MAXSET;
	      else
		llassert(FALSE);

	      term->constrType = VALUE;

	      if (term->value.constrExpr->op == PLUS)
		term->value.constrExpr->op = MINUS;
	      else
		term->value.constrExpr->op = PLUS;
	    }
	  
	}
      
    }
  

  return term;

}

constraintTerm constraintTerm_copy (constraintTerm term)
{
  constraintTerm ret;
  ret = new_constraintTermExpr();
  ret->constrType = term->constrType;
  ret->loc = fileloc_copy (term->loc);
  ret->value= term->value;
  ret->kind = term->kind;
  return ret;
}

constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e)
{
  constraintTerm ret = new_constraintTermExpr();
  ret->loc =  exprNode_getfileloc(e);
  ret->value.expr = e;
  ret->kind = EXPRNODE;
  return ret;
}


constraintTerm constraintTerm_makeMaxSetexpr (exprNode e)
{
  constraintTerm ret;
  ret = exprNode_makeConstraintTerm (e);
  ret->constrType = MAXSET;
  return ret;
}

constraintTerm constraintTerm_makeMinSetexpr (exprNode e)
{
  constraintTerm ret;
  ret = exprNode_makeConstraintTerm (e);
  ret->constrType = MINSET;
  return ret;
}

constraintTerm constraintTerm_makeMaxReadexpr (exprNode e)
{
  constraintTerm ret;
  ret = exprNode_makeConstraintTerm (e);
  ret->constrType = MAXREAD;
  return ret;
}

constraintTerm constraintTerm_makeMinReadexpr (exprNode e)
{
  constraintTerm ret;
  ret = exprNode_makeConstraintTerm (e);
  ret->constrType = MINREAD;
  return ret;
}

constraintTerm constraintTerm_makeValueexpr (exprNode e)
{
  constraintTerm ret;
  ret = exprNode_makeConstraintTerm (e);
  ret->constrType = VALUE;
  ret = constraintTerm_simplify (ret);
  return ret;
}


constraintTerm intLit_makeConstraintTerm (int i)
{
  constraintTerm ret = new_constraintTermExpr();
  ret->value.intlit = i;
  ret->kind = INTLITERAL;
  ret->loc =  fileloc_undefined;
  return ret;
}


constraintTerm constraintTerm_makeIntLitValue (int i)
{
  constraintTerm ret;
  ret = intLit_makeConstraintTerm (i);
  ret->constrType = VALUE;
  return ret;

}

/* constraintTerm constraintTerm_makeMinSetexpr (int i) */
/* { */
/*   constraintTerm ret; */
/*   ret = intLit_makeConstraintTerm (i); */
/*   ret->constrType = MINSET; */
/* } */

/* constraintTerm constraintTerm_makeMaxReadexpr (int i) */
/* { */
/*   constraintTerm ret; */
/*   ret = intLit_makeConstraintTerm (i); */
/*   ret->constrType = MAXREAD; */
/* } */
/* constraintTerm constraintTerm_makeMinReadexpr (int i) */
/* { */
/*   constraintTerm ret; */
/*   ret = exprNode_makeConstraintTerm (i); */
/*   ret->constrType = MINREAD; */
/* } */


cstring  constraintType_print (constraintType constrType)
{
  cstring st = cstring_undefined;
  
  switch (constrType)
    {
    case VALUE:
      st = cstring_makeLiteral("VALUE");
      break;
    case CALLSAFE:
      st = cstring_makeLiteral("CALLSAFE");
      break;
    case  MAXSET:
      st = cstring_makeLiteral ("MAXSET");
      break;
    case    MINSET:
      st = cstring_makeLiteral ("MINSET");
      break;
    case MAXREAD:
      st = cstring_makeLiteral ("MAXREAD");
      break;
    case MINREAD:
      st = cstring_makeLiteral ("MINREAD");
      break;
    case NULLTERMINATED:
      st = cstring_makeLiteral ("NULLTERMINATED");
      break;
    case UNDEFINED:
      st = cstring_makeLiteral (("Unhandled value for constraintType"));
      llassert(FALSE);
      break;
    default:
      st = cstring_makeLiteral (("Unhandled value for constraintType"));
      llassert(FALSE);
    }
  return st;
}
cstring constraintTerm_print (constraintTerm term)
{
  cstring s;
  s = cstring_undefined;
  
  llassert (term != NULL);

  switch (term->kind)
    {
    case EXPRNODE:
      /*@i334*/  //wtf
      s = message ("%s @ %s ", exprNode_unparse (term->value.expr),
		   fileloc_unparse (term->loc) );
      break;
    case INTLITERAL:
    {
      s = message (" %d ", term->value.intlit);
      break;
    }
    case SREF:
      s = cstring_makeLiteral("Not Implemented\n");
      llassert(FALSE);
      break;
    case CONSTRAINTEXPR:
      s = message ("%s ", constraintExpr_print (term->value.constrExpr) );
    }
  s = message (" %s  ( %s ) ", constraintType_print (term->constrType), s);
  return s;
  
}


bool constraintTerm_hasTerm (constraintTerm term, constraintTerm searchTerm)
{
  if (term->kind == CONSTRAINTEXPR)
    return (constraintExpr_includesTerm (term->value.constrExpr, searchTerm) );

  if ( (term->kind == EXPRNODE) && (searchTerm->kind == EXPRNODE) )
    {
      return sRef_same (term->value.expr->sref, searchTerm->value.expr->sref);
    }
  return FALSE;
    
}

/* same and similar are similar but not the same*/

bool constraintTerm_same (constraintTerm term1, constraintTerm term2)
{
  llassert (term1 !=NULL && term2 !=NULL);

  if (term1->constrType != term2->constrType)
    {
      return FALSE;
    }
  if ( (term1->kind != term2->kind) || (term1->kind != EXPRNODE) )
    {
      return FALSE;
    }
      
 DPRINTF ( (message
	    ("Comparing srefs for %s and  %s ", constraintTerm_print(term1), constraintTerm_print(term2)
	     )
	    )
	   );
 
 if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) )
   {
     DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
     return TRUE;
   }
 else
   {
     DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
     return FALSE;
   }     
    
}

bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
{
  llassert (term1 !=NULL && term2 !=NULL);

  //  if (term1->constrType != term2->constrType)
  //    {
  //      return FALSE;
  //    }
  if ( (term1->kind != term2->kind) || (term1->kind != EXPRNODE) )
    {
      return FALSE;
    }
      
 DPRINTF ( (message
	    ("Comparing srefs for %s and  %s ", constraintTerm_print(term1), constraintTerm_print(term2)
	     )
	    )
	   );
 
 if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) )
   {
     DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
     return TRUE;
   }
 else
   {
     DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
     return FALSE;
   }     
    
}
Commit	Line	Data
361091cc	1	/*
	2	** constraintTerm.c
	3	*/
	4
	5	# include <ctype.h> /* for isdigit */
	6	# include "lclintMacros.nf"
	7	# include "basic.h"
	8	# include "cgrammar.h"
	9	# include "cgrammar_tokens.h"
	10
	11	# include "exprChecks.h"
	12	# include "aliasChecks.h"
	13	# include "exprNodeSList.h"
	14	# include "exprData.i"
	15
	16	int constraintTerm_getValue (constraintTerm term)
	17	{
	18	if (term->kind == EXPRNODE)
	19	{
	20	return (multiVal_forceInt (term->value.expr->val) );
	21	}
	22	if (term->kind == INTLITERAL )
	23	{
	24	return (term->value.intlit);
	25	}
	26	llassert(FALSE);
	27	return 0;
	28	}
	29
	30	/@out@/ static constraintTerm new_constraintTermExpr (void)
	31	{
	32	constraintTerm ret;
	33	ret = dmalloc (sizeof (* ret ) );
	34	return ret;
	35	}
	36
	37	constraintTerm constraintTerm_simplify (constraintTerm term)
	38	{
	39	if (term->constrType == VALUE)
	40	{
	41	if (term->kind == EXPRNODE)
	42	{
	43	if ( exprNode_knownIntValue (term->value.expr ) )
	44	{
	45	int temp;
	46	temp = exprNode_getLongValue (term->value.expr);
	47	term->value.intlit = temp;
	48	term->kind = INTLITERAL;
	49	}
	50
	51	}
	52
	53	}
bf92e32c	54
	55	if (term->kind == CONSTRAINTEXPR )
	56	{
	57	if ( (term->constrType == MAXREAD) \|\| (term->constrType == MAXSET) )
	58	{
	59	// ms(var + intlit) = ms (var) - intlit
	60	if (term->value.constrExpr->expr == NULL)
	61	return term;
	62
	63	if (term->value.constrExpr->expr->term->kind == INTLITERAL)
	64	{
	65	if (term->constrType == MAXREAD)
	66	term->value.constrExpr->term->constrType = MAXREAD;
	67	else if (term->constrType == MAXSET)
	68	term->value.constrExpr->term->constrType = MAXSET;
	69	else
	70	llassert(FALSE);
	71
	72	term->constrType = VALUE;
	73
	74	if (term->value.constrExpr->op == PLUS)
	75	term->value.constrExpr->op = MINUS;
	76	else
	77	term->value.constrExpr->op = PLUS;
	78	}
	79
	80	}
	81
	82	}
	83
	84
361091cc	85	return term;
bf92e32c	86
361091cc	87	}
	88
	89	constraintTerm constraintTerm_copy (constraintTerm term)
	90	{
	91	constraintTerm ret;
	92	ret = new_constraintTermExpr();
	93	ret->constrType = term->constrType;
	94	ret->loc = fileloc_copy (term->loc);
	95	ret->value= term->value;
	96	ret->kind = term->kind;
	97	return ret;
	98	}
	99
	100	constraintTerm exprNode_makeConstraintTerm (/@only@/ exprNode e)
	101	{
	102	constraintTerm ret = new_constraintTermExpr();
	103	ret->loc = exprNode_getfileloc(e);
	104	ret->value.expr = e;
	105	ret->kind = EXPRNODE;
	106	return ret;
	107	}
	108
	109
	110	constraintTerm constraintTerm_makeMaxSetexpr (exprNode e)
	111	{
	112	constraintTerm ret;
	113	ret = exprNode_makeConstraintTerm (e);
	114	ret->constrType = MAXSET;
	115	return ret;
	116	}
	117
	118	constraintTerm constraintTerm_makeMinSetexpr (exprNode e)
	119	{
	120	constraintTerm ret;
	121	ret = exprNode_makeConstraintTerm (e);
	122	ret->constrType = MINSET;
	123	return ret;
	124	}
	125
	126	constraintTerm constraintTerm_makeMaxReadexpr (exprNode e)
	127	{
	128	constraintTerm ret;
	129	ret = exprNode_makeConstraintTerm (e);
	130	ret->constrType = MAXREAD;
	131	return ret;
	132	}
	133
	134	constraintTerm constraintTerm_makeMinReadexpr (exprNode e)
	135	{
	136	constraintTerm ret;
	137	ret = exprNode_makeConstraintTerm (e);
	138	ret->constrType = MINREAD;
	139	return ret;
	140	}
	141
	142	constraintTerm constraintTerm_makeValueexpr (exprNode e)
	143	{
	144	constraintTerm ret;
	145	ret = exprNode_makeConstraintTerm (e);
	146	ret->constrType = VALUE;
	147	ret = constraintTerm_simplify (ret);
	148	return ret;
	149	}
	150
151
152	constraintTerm intLit_makeConstraintTerm (int i)
153	{
154	constraintTerm ret = new_constraintTermExpr();
155	ret->value.intlit = i;
156	ret->kind = INTLITERAL;
157	ret->loc = fileloc_undefined;
158	return ret;
159	}
160
161
162	constraintTerm constraintTerm_makeIntLitValue (int i)
163	{
164	constraintTerm ret;
165	ret = intLit_makeConstraintTerm (i);
166	ret->constrType = VALUE;
167	return ret;
168
169	}
170
171	/* constraintTerm constraintTerm_makeMinSetexpr (int i) */
172	/* { */
173	/* constraintTerm ret; */
174	/* ret = intLit_makeConstraintTerm (i); */
175	/* ret->constrType = MINSET; */
176	/* } */
177
178	/* constraintTerm constraintTerm_makeMaxReadexpr (int i) */
179	/* { */
180	/* constraintTerm ret; */
181	/* ret = intLit_makeConstraintTerm (i); */
182	/* ret->constrType = MAXREAD; */
183	/* } */
184	/* constraintTerm constraintTerm_makeMinReadexpr (int i) */
185	/* { */
186	/* constraintTerm ret; */
187	/* ret = exprNode_makeConstraintTerm (i); */
188	/* ret->constrType = MINREAD; */
189	/* } */
190
191
192
193
194	cstring constraintType_print (constraintType constrType)
195	{
196	cstring st = cstring_undefined;
197
198	switch (constrType)
199	{
200	case VALUE:
201	st = cstring_makeLiteral("VALUE");
202	break;
203	case CALLSAFE:
204	st = cstring_makeLiteral("CALLSAFE");
205	break;
206	case MAXSET:
207	st = cstring_makeLiteral ("MAXSET");
208	break;
209	case MINSET:
210	st = cstring_makeLiteral ("MINSET");
211	break;
212	case MAXREAD:
213	st = cstring_makeLiteral ("MAXREAD");
214	break;
215	case MINREAD:
216	st = cstring_makeLiteral ("MINREAD");
217	break;
218	case NULLTERMINATED:
219	st = cstring_makeLiteral ("NULLTERMINATED");
220	break;
221	case UNDEFINED:
222	st = cstring_makeLiteral (("Unhandled value for constraintType"));
223	llassert(FALSE);
224	break;
225	default:
226	st = cstring_makeLiteral (("Unhandled value for constraintType"));
227	llassert(FALSE);
228	}
229	return st;
230	}
231	cstring constraintTerm_print (constraintTerm term)
232	{
233	cstring s;
234	s = cstring_undefined;
235
236	llassert (term != NULL);
237
238	switch (term->kind)
239	{
240	case EXPRNODE:
241	/@i334/ //wtf
242	s = message ("%s @ %s ", exprNode_unparse (term->value.expr),
243	fileloc_unparse (term->loc) );
244	break;
245	case INTLITERAL:
246	{
247	s = message (" %d ", term->value.intlit);
248	break;
249	}
250	case SREF:
251	s = cstring_makeLiteral("Not Implemented\n");
252	llassert(FALSE);
253	break;
bf92e32c	254	case CONSTRAINTEXPR:
bf92e32c	255	s = message ("%s ", constraintExpr_print (term->value.constrExpr) );
361091cc	256	}
bf92e32c	257	s = message (" %s ( %s ) ", constraintType_print (term->constrType), s);
361091cc	258	return s;
	259
	260	}
	261
	262
bf92e32c	263	bool constraintTerm_hasTerm (constraintTerm term, constraintTerm searchTerm)
	264	{
	265	if (term->kind == CONSTRAINTEXPR)
	266	return (constraintExpr_includesTerm (term->value.constrExpr, searchTerm) );
	267
	268	if ( (term->kind == EXPRNODE) && (searchTerm->kind == EXPRNODE) )
	269	{
	270	return sRef_same (term->value.expr->sref, searchTerm->value.expr->sref);
	271	}
	272	return FALSE;
	273
	274	}
	275
	276	/* same and similar are similar but not the same*/
361091cc	277
	278	bool constraintTerm_same (constraintTerm term1, constraintTerm term2)
	279	{
	280	llassert (term1 !=NULL && term2 !=NULL);
	281
	282	if (term1->constrType != term2->constrType)
	283	{
	284	return FALSE;
	285	}
	286	if ( (term1->kind != term2->kind) \|\| (term1->kind != EXPRNODE) )
	287	{
	288	return FALSE;
	289	}
	290
	291	DPRINTF ( (message
	292	("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2)
	293	)
	294	)
	295	);
	296
	297	if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) )
	298	{
bf92e32c	299	DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
	300	return TRUE;
	301	}
	302	else
	303	{
	304	DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
	305	return FALSE;
	306	}
	307
	308	}
	309
	310	bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
	311	{
	312	llassert (term1 !=NULL && term2 !=NULL);
	313
	314	// if (term1->constrType != term2->constrType)
	315	// {
	316	// return FALSE;
	317	// }
	318	if ( (term1->kind != term2->kind) \|\| (term1->kind != EXPRNODE) )
	319	{
	320	return FALSE;
	321	}
	322
	323	DPRINTF ( (message
	324	("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2)
	325	)
	326	)
	327	);
	328
	329	if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) )
	330	{
	331	DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
361091cc	332	return TRUE;
	333	}
	334	else
	335	{
bf92e32c	336	DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
361091cc	337	return FALSE;
	338	}
	339
	340	}
	341