[splint.git] / src / constraint.c

/*
** constraintList.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"

/*@i33*/
/*@-fcnuse*/
/*@-assignexpose*/

constraint constraint_copy (constraint c)
{
  constraint ret;
  ret = constraint_makeNew();
  ret->c1 = c->c1;
  ret->t1 = c->t1;
  ret->ar = c->ar;
  ret->e1 = c->e1;
  ret->post = c->post;
  return ret;
}

bool constraint_resolve (/*@unused@*/ constraint c)
{
  return FALSE;
}

/*@notnull@*/ 
/*@special@*/ constraint constraint_makeNew (void)
     /*@post:isnull result->t1, result->e1, result->c1@*/
     /*@defines result->ar, result->post@*/
{
  constraint ret;
  ret = dmalloc(sizeof (*ret) );
  ret->t1 = NULL;
  ret->e1 = NULL;
  ret->c1 = NULL;
  ret->ar = LT;
  ret->post = FALSE;
  /*@i23*/return ret;
}
/*@-czechfcns@*/

/*@out@*/ constraintTerm new_constraintTermExpr (void)
{
  constraintTerm ret;
  ret = dmalloc (sizeof (* ret ) );
  
  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 intLit_makeConstraintTerm (int i)
{
  constraintTerm ret = new_constraintTermExpr();
  ret->value.intlit = i;
  ret->kind = INTLITERAL;
  ret->loc =  fileloc_undefined;
  return ret;
}
     

/*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
 /*@post:isnull result->e1@*/
     /*@post:notnull result->t1@*/
     /*@defines result->e1, result->t1, result->c1@, result->op*/
{
  constraintExpr ret;
  ret = dmalloc (sizeof (*ret) );
  ret->t1 = term;
  ret->e1 = NULL;
  ret->c1 = UNDEFINED;
  ret->op = PLUS;
  return ret;
}


 constraintExpr makeConstraintExprIntlit (int i)
{
  constraintExpr ret;
  ret = dmalloc (sizeof (*ret) );
  ret->t1 = intLit_makeConstraintTerm (i);
  ret->e1 = NULL;
  ret->c1 = VALUE;
  ret->op = PLUS;
  /*@i1*/ return ret;
}

				       
/*@i33*/
/*@null@*/ constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
{
  constraint ret = constraint_makeNew();
  constraintTerm term;
  po = exprNode_fakeCopy(po);
  ind = exprNode_fakeCopy(ind);
  printf ("Requires maxr(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
	  cstring_toCharsSafe ( exprNode_unparse (ind)  ) );
  ret->t1 = exprNode_makeConstraintTerm(po);
  ret->c1 = MAXREAD;
  ret->ar = GTE;

  term = exprNode_makeConstraintTerm (ind);
  
  ret->e1 =  makeConstraintExpr (term);
  ret->e1->c1 = VALUE;
  /*@i1*/return ret;
}

constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
{
  constraint ret = constraint_makeNew();
  constraintTerm term;
  printf ("Requires maxw(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
	 cstring_toCharsSafe( exprNode_unparse (ind)  ) );
  ret->t1 = exprNode_makeConstraintTerm(po);
  ret->c1 = MAXSET;
  ret->ar = GTE;

  term = exprNode_makeConstraintTerm(ind);
  
  ret->e1 =  makeConstraintExpr (term);
  ret->e1->c1 = VALUE;
  /*@i1*/return ret;
}


constraint constraint_makeReadSafeInt (exprNode t1, int index)
{
  constraint ret = constraint_makeNew();
  constraintTerm term;
  printf ("Ensures maxr((valueof(%s)) >= %d\n", cstring_toCharsSafe (exprNode_unparse (t1 ) ),
	  index   );
  t1 = exprNode_fakeCopy(t1);
  ret->t1 = exprNode_makeConstraintTerm(t1);
  ret->c1 = MAXREAD;
  ret->ar = GTE;
  ret->post = TRUE;
  term = intLit_makeConstraintTerm(index);
  
  ret->e1 =  makeConstraintExpr (term);
  ret->e1->c1 = VALUE;
  /*make this refer to element after preconditions */
  fileloc_incColumn (ret->t1->loc);
  /*@i1*/ return ret;
}


constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
{
  constraint ret = constraint_makeNew();
  constraintTerm term;

  t1 = exprNode_fakeCopy (t1);
  t2 = exprNode_fakeCopy (t2);
  
  ret->t1 = exprNode_makeConstraintTerm(t1);

  if (ret->t1->loc != NULL)
    fileloc_free(ret->t1->loc);
  
  ret->t1->loc = fileloc_copy (sequencePoint);
  ret->c1 = MAXREAD;
  ret->ar = GTE;
  ret->post = TRUE;  
  term = exprNode_makeConstraintTerm (t2);
  
  ret->e1 =  makeConstraintExpr (term);
  ret->e1->c1 = VALUE;
  /*make this refer to element after preconditions */
  fileloc_incColumn (ret->t1->loc);
  /*@i1*/ return ret;
}

constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint)
{
  constraint ret = constraint_makeNew();
  constraintTerm term;

  po = exprNode_fakeCopy (po);
  ind = exprNode_fakeCopy (ind);
  
  ret->t1 = exprNode_makeConstraintTerm(po);
  ret->c1 = MINREAD;
  ret->ar = LTE;
  ret->post = TRUE;
  term = exprNode_makeConstraintTerm (ind);
  
  ret->e1 =  makeConstraintExpr (term);
  ret->e1->c1 = VALUE;
  /*make this refer to element after preconditions */
  fileloc_incColumn (ret->t1->loc);
  /*@i1*/ return ret;
}

constraintExpr makePostOpInc (exprNode t1)
{
  constraintExpr ret;
  constraintTerm term;

  t1 = exprNode_fakeCopy (t1);
  term =   exprNode_makeConstraintTerm(t1);
  ret = makeConstraintExpr (term);
  ret->op = PLUS;
  ret->c1 = VALUE;
  ret->e1 =  makeConstraintExprIntlit (1);
  return ret;
}

constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc sequencePoint)
{
  constraint ret = constraint_makeNew();
  //constraintTerm term;
  exprNode t2;
  t1 = exprNode_fakeCopy(t1);
  t2 = exprNode_fakeCopy(t1);
  
  ret->t1 = exprNode_makeConstraintTerm(t1);
  ret->c1 = VALUE;
  ret->ar = EQ;
  ret->post = TRUE;
  ret->e1 = makePostOpInc(t2);

  fileloc_incColumn (  ret->t1->loc);
  fileloc_incColumn (  ret->t1->loc);
  
  /*@i6*/return ret;
}

void constraintType_print (constraintType c1)
{
  switch (c1)
    {
    case VALUE:
      printf("VALUE");
      break;
    case CALLSAFE:
      printf("CALLSAFE");
      break;
    case  MAXSET:
      printf ("MAXSET");
      break;
    case    MINSET:
      printf ("MINSET");
      break;
    case MAXREAD:
      printf ("MAXREAD");
      break;
    case MINREAD:
      printf ("MINREAD");
      break;
    case NULLTERMINATED:
      printf ("NULLTERMINATED");
      break;
    case UNDEFINED:
      TPRINTF(("Unhandled value for constraintType"));
      llassert(FALSE);
      break;
    default:
      TPRINTF(("Unhandled value for constraintType"));
      llassert(FALSE);
    }
}
void constraintTerm_print (constraintTerm term)
{
  cstring s;

  llassert (term != NULL);
  switch (term->kind)
    {
    case EXPRNODE:
      s = exprNode_unparse (term->value.expr);
      printf(" %s", cstring_toCharsSafe(s) );
      s = fileloc_unparse (term->loc);
      printf("@ %s", cstring_toCharsSafe(s) );
      cstring_free(s);
      break;
    case INTLITERAL:
    {
      char * buf = malloc (15);
      /*@i1*/snprintf (buf, 14, "intliteral(%d)", term->value.intlit);
      /*@i1*/ printf(" %s  ", buf);
      free (buf);
      break;
    }
    case SREF:
      TPRINTF( ("Not Implemented\n"));
      llassert(FALSE);
      break;
    }
    /*@-unreachable*/
  return;
  /*@=unreachable*/
}

void arithType_print (arithType ar)
{
  switch (ar)
    {
    case LT:
      printf(" <  ");
      return;
    case	LTE:
      printf(" <= ");
      return;
    case 	GT:
      printf(" >  ");
      return;
    case 	GTE:
      printf(" <= ");
      return;
    case	EQ:
      printf(" == ");
      return;
    case	NONNEGATIVE:
      printf(" NONNEGATIVE ");
      return;
    case	POSITIVE:
      printf(" POSITIVE ");
      return;
    default:
      llassert(FALSE);
    }
}

void constraintExpr_print (constraintExpr ex)
{
  llassert (ex != NULL);
  constraintType_print (ex->c1 );
  constraintTerm_print (ex->t1);
  if (ex->e1 != NULL)
    {
      if (ex->op == PLUS)
	{
	  printf(" + ");
	}
      else
	{
	  printf (" - ");
	}
      
      constraintExpr_print (ex->e1);
    }
  
}


void constraint_print (constraint c)
{
  if (c->post)
    {
      printf("Ensures: ");
    }
  else
    {
      printf("requires: ");
    }
  
  constraintType_print (c->c1);
  constraintTerm_print (c->t1);
  arithType_print(c->ar);
  constraintExpr_print(c->e1);
  printf("\n");
}

/*@=fcnuse*/
/*@=assignexpose*/
/*@=czechfcns@*/
Commit	Line	Data
4cccc6ad	1	/*
	2	** constraintList.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	/@i33/
	17	/@-fcnuse/
	18	/@-assignexpose/
	19
	20	constraint constraint_copy (constraint c)
	21	{
	22	constraint ret;
	23	ret = constraint_makeNew();
	24	ret->c1 = c->c1;
	25	ret->t1 = c->t1;
	26	ret->ar = c->ar;
	27	ret->e1 = c->e1;
	28	ret->post = c->post;
	29	return ret;
	30	}
	31
	32	bool constraint_resolve (/@unused@/ constraint c)
	33	{
	34	return FALSE;
	35	}
	36
	37	/@notnull@/
	38	/@special@/ constraint constraint_makeNew (void)
	39	/@post:isnull result->t1, result->e1, result->c1@/
	40	/@defines result->ar, result->post@/
	41	{
	42	constraint ret;
	43	ret = dmalloc(sizeof (*ret) );
	44	ret->t1 = NULL;
	45	ret->e1 = NULL;
	46	ret->c1 = NULL;
	47	ret->ar = LT;
	48	ret->post = FALSE;
	49	/@i23/return ret;
	50	}
	51	/@-czechfcns@/
	52
	53	/@out@/ constraintTerm new_constraintTermExpr (void)
	54	{
	55	constraintTerm ret;
	56	ret = dmalloc (sizeof (* ret ) );
	57
	58	return ret;
	59	}
	60
	61	constraintTerm exprNode_makeConstraintTerm (/@only@/ exprNode e)
	62	{
	63	constraintTerm ret = new_constraintTermExpr();
	64	ret->loc = exprNode_getfileloc(e);
65	ret->value.expr = e;
66	ret->kind = EXPRNODE;
67	return ret;
68	}
69
70
71	constraintTerm intLit_makeConstraintTerm (int i)
72	{
73	constraintTerm ret = new_constraintTermExpr();
74	ret->value.intlit = i;
75	ret->kind = INTLITERAL;
76	ret->loc = fileloc_undefined;
77	return ret;
78	}
79
80
81	/@special@/ constraintExpr makeConstraintExpr (/@only@/ /@notnull@/ constraintTerm term)
82	/@post:isnull result->e1@/
83	/@post:notnull result->t1@/
84	/@defines result->e1, result->t1, result->c1@, result->op/
85	{
86	constraintExpr ret;
87	ret = dmalloc (sizeof (*ret) );
88	ret->t1 = term;
89	ret->e1 = NULL;
90	ret->c1 = UNDEFINED;
91	ret->op = PLUS;
92	return ret;
93	}
94
95
96	constraintExpr makeConstraintExprIntlit (int i)
97	{
98	constraintExpr ret;
99	ret = dmalloc (sizeof (*ret) );
100	ret->t1 = intLit_makeConstraintTerm (i);
101	ret->e1 = NULL;
102	ret->c1 = VALUE;
103	ret->op = PLUS;
104	/@i1/ return ret;
105	}
106
107
108	/@i33/
109	/@null@/ constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
110	{
111	constraint ret = constraint_makeNew();
112	constraintTerm term;
113	po = exprNode_fakeCopy(po);
114	ind = exprNode_fakeCopy(ind);
115	printf ("Requires maxr(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
116	cstring_toCharsSafe ( exprNode_unparse (ind) ) );
117	ret->t1 = exprNode_makeConstraintTerm(po);
118	ret->c1 = MAXREAD;
119	ret->ar = GTE;
120
121	term = exprNode_makeConstraintTerm (ind);
122
123	ret->e1 = makeConstraintExpr (term);
124	ret->e1->c1 = VALUE;
125	/@i1/return ret;
126	}
127
128	constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
129	{
130	constraint ret = constraint_makeNew();
131	constraintTerm term;
132	printf ("Requires maxw(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
133	cstring_toCharsSafe( exprNode_unparse (ind) ) );
134	ret->t1 = exprNode_makeConstraintTerm(po);
135	ret->c1 = MAXSET;
136	ret->ar = GTE;
137
138	term = exprNode_makeConstraintTerm(ind);
139
140	ret->e1 = makeConstraintExpr (term);
141	ret->e1->c1 = VALUE;
142	/@i1/return ret;
143	}
144
145
146	constraint constraint_makeReadSafeInt (exprNode t1, int index)
147	{
148	constraint ret = constraint_makeNew();
149	constraintTerm term;
150	printf ("Ensures maxr((valueof(%s)) >= %d\n", cstring_toCharsSafe (exprNode_unparse (t1 ) ),
151	index );
152	t1 = exprNode_fakeCopy(t1);
153	ret->t1 = exprNode_makeConstraintTerm(t1);
154	ret->c1 = MAXREAD;
155	ret->ar = GTE;
156	ret->post = TRUE;
157	term = intLit_makeConstraintTerm(index);
158
159	ret->e1 = makeConstraintExpr (term);
160	ret->e1->c1 = VALUE;
161	/make this refer to element after preconditions /
162	fileloc_incColumn (ret->t1->loc);
163	/@i1/ return ret;
164	}
165
166
167	constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
168	{
169	constraint ret = constraint_makeNew();
170	constraintTerm term;
171
172	t1 = exprNode_fakeCopy (t1);
173	t2 = exprNode_fakeCopy (t2);
174
175	ret->t1 = exprNode_makeConstraintTerm(t1);
176
177	if (ret->t1->loc != NULL)
178	fileloc_free(ret->t1->loc);
179
180	ret->t1->loc = fileloc_copy (sequencePoint);
181	ret->c1 = MAXREAD;
182	ret->ar = GTE;
183	ret->post = TRUE;
184	term = exprNode_makeConstraintTerm (t2);
185
186	ret->e1 = makeConstraintExpr (term);
187	ret->e1->c1 = VALUE;
188	/make this refer to element after preconditions /
189	fileloc_incColumn (ret->t1->loc);
190	/@i1/ return ret;
191	}
192
193	constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint)
194	{
195	constraint ret = constraint_makeNew();
196	constraintTerm term;
197
198	po = exprNode_fakeCopy (po);
199	ind = exprNode_fakeCopy (ind);
200
201	ret->t1 = exprNode_makeConstraintTerm(po);
202	ret->c1 = MINREAD;
203	ret->ar = LTE;
204	ret->post = TRUE;
205	term = exprNode_makeConstraintTerm (ind);
206
207	ret->e1 = makeConstraintExpr (term);
208	ret->e1->c1 = VALUE;
209	/make this refer to element after preconditions /
210	fileloc_incColumn (ret->t1->loc);
211	/@i1/ return ret;
212	}
213
214	constraintExpr makePostOpInc (exprNode t1)
215	{
216	constraintExpr ret;
217	constraintTerm term;
218
219	t1 = exprNode_fakeCopy (t1);
220	term = exprNode_makeConstraintTerm(t1);
221	ret = makeConstraintExpr (term);
222	ret->op = PLUS;
223	ret->c1 = VALUE;
224	ret->e1 = makeConstraintExprIntlit (1);
225	return ret;
226	}
227
228	constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc sequencePoint)
229	{
230	constraint ret = constraint_makeNew();
231	//constraintTerm term;
232	exprNode t2;
233	t1 = exprNode_fakeCopy(t1);
234	t2 = exprNode_fakeCopy(t1);
235
236	ret->t1 = exprNode_makeConstraintTerm(t1);
237	ret->c1 = VALUE;
238	ret->ar = EQ;
239	ret->post = TRUE;
240	ret->e1 = makePostOpInc(t2);
241
242	fileloc_incColumn ( ret->t1->loc);
243	fileloc_incColumn ( ret->t1->loc);
244
245	/@i6/return ret;
246	}
247
248	void constraintType_print (constraintType c1)
249	{
250	switch (c1)
251	{
252	case VALUE:
253	printf("VALUE");
254	break;
255	case CALLSAFE:
256	printf("CALLSAFE");
257	break;
258	case MAXSET:
259	printf ("MAXSET");
260	break;
261	case MINSET:
262	printf ("MINSET");
263	break;
264	case MAXREAD:
265	printf ("MAXREAD");
266	break;
267	case MINREAD:
268	printf ("MINREAD");
269	break;
270	case NULLTERMINATED:
271	printf ("NULLTERMINATED");
272	break;
273	case UNDEFINED:
274	TPRINTF(("Unhandled value for constraintType"));
275	llassert(FALSE);
276	break;
277	default:
278	TPRINTF(("Unhandled value for constraintType"));
279	llassert(FALSE);
280	}
281	}
282	void constraintTerm_print (constraintTerm term)
283	{
284	cstring s;
285
286	llassert (term != NULL);
287	switch (term->kind)
288	{
289	case EXPRNODE:
290	s = exprNode_unparse (term->value.expr);
291	printf(" %s", cstring_toCharsSafe(s) );
292	s = fileloc_unparse (term->loc);
293	printf("@ %s", cstring_toCharsSafe(s) );
294	cstring_free(s);
295	break;
296	case INTLITERAL:
297	{
298	char * buf = malloc (15);
299	/@i1/snprintf (buf, 14, "intliteral(%d)", term->value.intlit);
300	/@i1/ printf(" %s ", buf);
301	free (buf);
302	break;
303	}
304	case SREF:
305	TPRINTF( ("Not Implemented\n"));
306	llassert(FALSE);
307	break;
308	}
309	/@-unreachable/
310	return;
311	/@=unreachable/
312	}
313
314	void arithType_print (arithType ar)
315	{
316	switch (ar)
317	{
318	case LT:
319	printf(" < ");
320	return;
321	case LTE:
322	printf(" <= ");
323	return;
324	case GT:
325	printf(" > ");
326	return;
327	case GTE:
328	printf(" <= ");
329	return;
330	case EQ:
331	printf(" == ");
332	return;
333	case NONNEGATIVE:
334	printf(" NONNEGATIVE ");
335	return;
336	case POSITIVE:
337	printf(" POSITIVE ");
338	return;
339	default:
340	llassert(FALSE);
341	}
342	}
343
344	void constraintExpr_print (constraintExpr ex)
345	{
346	llassert (ex != NULL);
347	constraintType_print (ex->c1 );
348	constraintTerm_print (ex->t1);
349	if (ex->e1 != NULL)
350	{
351	if (ex->op == PLUS)
352	{
353	printf(" + ");
354	}
355	else
356	{
357	printf (" - ");
358	}
359
360	constraintExpr_print (ex->e1);
361	}
362
363	}
364
365
366	void constraint_print (constraint c)
367	{
368	if (c->post)
369	{
370	printf("Ensures: ");
371	}
372	else
373	{
374	printf("requires: ");
375	}
376
377	constraintType_print (c->c1);
378	constraintTerm_print (c->t1);
379	arithType_print(c->ar);
380	constraintExpr_print(c->e1);
381	printf("\n");
382	}
383
384	/@=fcnuse/
385	/@=assignexpose/
386	/@=czechfcns@/
387