[splint.git] / src / constraint.c

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

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

/*@notnull@*/ constraint constraint_makeNew (void);


constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
     
{
  char *t;
  int c;
  constraint ret;
  ret = constraint_makeNew();
  llassert (sRef_isValid(x) );
  if (!sRef_isValid(x))
    return ret;
 
    
  ret->lexpr = constraintExpr_makeTermsRef (x);
  #warning fix abstraction

  if (relOp.tok == GE_OP)
      ret->ar = GTE;
  else if (relOp.tok == LE_OP)
    ret->ar = LTE;
  else if (relOp.tok == EQ_OP)
    ret->ar = EQ;
  else
    llfatalbug(message ("Unsupported relational operator") );


  t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  c = atoi( t );
  ret->expr = constraintExpr_makeIntLiteral (c);

  ret->post = TRUE;
  //  ret->orig = ret;
  DPRINTF(("GENERATED CONSTRAINT:"));
  DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  return ret;
}

constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
     
{
  char *t;
  int c;
  constraint ret;
  ret = constraint_makeNew();
  llassert (l!=NULL);
  if (!l)
    return ret;
 
    
  ret->lexpr = constraintExpr_copy (l);
  #warning fix abstraction

  if (relOp.tok == GE_OP)
      ret->ar = GTE;
  else if (relOp.tok == LE_OP)
    ret->ar = LTE;
  else if (relOp.tok == EQ_OP)
    ret->ar = EQ;
  else
  llfatalbug(message("Unsupported relational operator") );


  t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  c = atoi( t );
  ret->expr = constraintExpr_makeIntLiteral (c);

  ret->post = TRUE;
  //  ret->orig = ret;
  DPRINTF(("GENERATED CONSTRAINT:"));
  DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  return ret;
}


constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)     
{
  constraint ret;
  ret = constraint_makeNew();
  llassert (l !=NULL);
  if (!l)
    return ret;
 
    
  ret->lexpr = constraintExpr_copy (l);
  #warning fix abstraction

  if (relOp.tok == GE_OP)
      ret->ar = GTE;
  else if (relOp.tok == LE_OP)
    ret->ar = LTE;
  else if (relOp.tok == EQ_OP)
    ret->ar = EQ;
  else
  llfatalbug( message("Unsupported relational operator") );

  ret->expr = constraintExpr_copy (r);

  ret->post = TRUE;
  //  ret->orig = ret;
  DPRINTF(("GENERATED CONSTRAINT:"));
  DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  return ret;
}

constraint constraint_copy (constraint c)
{
  constraint ret;
  ret = constraint_makeNew();
  ret->lexpr = constraintExpr_copy (c->lexpr);
  ret->ar = c->ar;
  ret->expr =  constraintExpr_copy (c->expr);
  ret->post = c->post;
  ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
  
  /*@i33 fix this*/
  if (c->orig != NULL)
    ret->orig = constraint_copy (c->orig);
  else
    ret->orig = NULL;
  return ret;
}

/*like copy expect it doesn't allocate memory for the constraint*/

void constraint_overWrite (constraint c1, constraint c2)
{
  c1->lexpr = constraintExpr_copy (c2->lexpr);
  c1->ar = c2->ar;
  c1->expr =  constraintExpr_copy (c2->expr);
  c1->post = c2->post;
  /*@i33 fix this*/
  if (c2->orig != NULL)
    c1->orig = constraint_copy (c2->orig);
  else
    c1->orig = NULL;
  c1->generatingExpr = exprNode_fakeCopy (c2->generatingExpr );
}

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


/*@notnull@*/ constraint constraint_makeNew (void)
{
  constraint ret;
  ret = dmalloc(sizeof (*ret) );
  ret->lexpr = NULL;
  ret->expr = NULL;
  ret->ar = LT;
  ret->post = FALSE;
  ret->orig = NULL;
  ret->generatingExpr = NULL;
  return ret;
}

constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
{
    
  if (c->generatingExpr == NULL)
    {
      c->generatingExpr = exprNode_fakeCopy(e);
      DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
    }
  else
    {
      DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
    }
  return c;
}

fileloc constraint_getFileloc (constraint c)
{
  if (c->generatingExpr)
    return (exprNode_getfileloc (c->generatingExpr) );
	    
  return (constraintExpr_getFileloc (c->lexpr) );


}

static bool checkForMaxSet (constraint c)
{
  if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
    return TRUE;

  return FALSE;
}

bool constraint_hasMaxSet(constraint c)
{
  if (c->orig != NULL)
    {
      if (checkForMaxSet(c->orig) )
	return TRUE;
    }

  return (checkForMaxSet(c) );
}

constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
{
  constraint ret = constraint_makeNew();
  //  constraintTerm term;
  po = exprNode_fakeCopy(po);
  ind = exprNode_fakeCopy(ind);
  ret->lexpr = constraintExpr_makeMaxReadExpr(po);
  ret->ar    = GTE;
  ret->expr  = constraintExpr_makeValueExpr (ind);
  return ret;
}

constraint constraint_makeWriteSafeInt (exprNode po, int ind)
{
  constraint ret = constraint_makeNew();

 
  ret->lexpr =constraintExpr_makeMaxSetExpr(po);
  ret->ar = GTE;
  ret->expr =  constraintExpr_makeValueInt (ind);
  /*@i1*/return ret;
}

constraint constraint_makeSRefSetBufferSize (sRef s, int size)
{
 constraint ret = constraint_makeNew();
 ret->lexpr = constraintExpr_makeSRefMaxset (s);
 ret->ar = EQ;
 ret->expr =  constraintExpr_makeValueInt (size);
 ret->post = TRUE;
 /*@i1*/return ret;
}

constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
{
  constraint ret = constraint_makeNew();

 
  ret->lexpr = constraintExpr_makeSRefMaxset (s);
  ret->ar = GTE;
  ret->expr =  constraintExpr_makeValueInt (ind);
  ret->post = TRUE;
  /*@i1*/return ret;
}

/* drl added 01/12/2000
   
  makes the constraint: Ensures index <= MaxRead(buffer) */

constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
{
  constraint ret = constraint_makeNew();

  ret->lexpr = constraintExpr_makeValueExpr (index);
  ret->ar = LTE;
  ret->expr = constraintExpr_makeMaxReadExpr(buffer);
  ret->post = TRUE;
  return ret;
}

constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
{
  constraint ret = constraint_makeNew();

 
  ret->lexpr =constraintExpr_makeMaxSetExpr(po);
  ret->ar = GTE;
  ret->expr =  constraintExpr_makeValueExpr (ind);
  /*@i1*/return ret;
}


constraint constraint_makeReadSafeInt ( exprNode po, int ind)
{
  constraint ret = constraint_makeNew();

  po = exprNode_fakeCopy(po);
  
  ret->lexpr = constraintExpr_makeMaxReadExpr(po);
  ret->ar    = GTE;
  ret->expr  = constraintExpr_makeValueInt (ind);
  return ret;
}

constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
{
  constraint ret = constraint_makeNew();


  e1 = exprNode_fakeCopy (e1);
  t2 = exprNode_fakeCopy (t2);
  
  ret = constraint_makeReadSafeExprNode(e1, t2);

  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
  
  ret->post = TRUE;  

  //  fileloc_incColumn (ret->lexpr->term->loc);
  return ret;
}


static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
{
  constraint ret = constraint_makeNew();
  exprNode e;
  
  e = exprNode_fakeCopy(e1);
  if (! (e1 && e2) )
    {
      llcontbug((message("null exprNode, Exprnodes are %s and %s",
		       exprNode_unparse(e1), exprNode_unparse(e2) )
	       ));
    }
		       
  ret->lexpr = constraintExpr_makeValueExpr (e);
  ret->ar = ar;
  ret->post = TRUE;
  e = exprNode_fakeCopy(e2);
  ret->expr =  constraintExpr_makeValueExpr (e);
  
  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
  return ret;
}


/* make constraint ensures e1 == e2 */

constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
}

/*make constraint ensures e1 < e2 */
constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
}

constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
}

constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
{
 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
}

constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
{
 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
}


exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
{
  dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
  dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
  dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
  dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
  return dst;
}

constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
{
  constraint ret = constraint_makeNew();
  //constraintTerm term;

  e = exprNode_fakeCopy(e);
  ret->lexpr = constraintExpr_makeValueExpr (e);
  ret->ar = EQ;
  ret->post = TRUE;
  ret->expr =  constraintExpr_makeValueExpr (e);
  ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);

  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
//   fileloc_incColumn (  ret->lexpr->term->loc);
//   fileloc_incColumn (  ret->lexpr->term->loc);
  return ret;
}
constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
{
  constraint ret = constraint_makeNew();
  //constraintTerm term;

  e = exprNode_fakeCopy(e);
  ret->lexpr = constraintExpr_makeValueExpr (e);
  ret->ar = EQ;
  ret->post = TRUE;
  ret->expr =  constraintExpr_makeValueExpr (e);
  ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);

  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
//   fileloc_incColumn (  ret->lexpr->term->loc);
//   fileloc_incColumn (  ret->lexpr->term->loc);
  return ret;
}


// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
// {
//   constraint ret = constraint_makeNew();
//   //constraintTerm term;

//   e = exprNode_fakeCopy(e);
//   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
//   ret->ar = EQ;
//   ret->post = TRUE;
//   ret->expr = constraintExpr_makeIncConstraintExpr (e);
//   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
//   return ret;
// }


cstring arithType_print (arithType ar) /*@*/
{
  cstring st = cstring_undefined;
  switch (ar)
    {
    case LT:
      st = cstring_makeLiteral (" < ");
      break;
    case	LTE:
      st = cstring_makeLiteral (" <= ");
      break;
    case 	GT:
      st = cstring_makeLiteral (" > ");
      break;
    case 	GTE:
      st = cstring_makeLiteral (" >= ");
      break;
    case	EQ:
      st = cstring_makeLiteral (" == ");
      break;
    case	NONNEGATIVE:
      st = cstring_makeLiteral (" NONNEGATIVE ");
      break;
    case	POSITIVE:
      st = cstring_makeLiteral (" POSITIVE ");
      break;
    default:
      llassert(FALSE);
      break;
    }
  return st;
}

void constraint_printError (constraint c, fileloc loc)
{
  cstring string;
  fileloc errorLoc;
  
  string = constraint_printDetailed (c);

  errorLoc = loc;

  if (constraint_getFileloc(c) )
    /*@-branchstate@*/
      errorLoc = constraint_getFileloc(c);
  /*@=branchstate@*/
  
  if (c->post)
    {
       voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
    }
  else
    {
      voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
    }
      
}

cstring  constraint_printDetailed (constraint c)
{
  cstring st = cstring_undefined;


  if (!c->post)
    {
    if (c->orig != NULL)  
      st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
    else
      st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
      
    }
  else
    {
      if (c->orig != NULL)
	st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
      else
	st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));	
    }

  if (context_getFlag (FLG_CONSTRAINTLOCATION) )
    {
      cstring temp;
      // llassert (c->generatingExpr);
      temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
		      exprNode_unparse(c->generatingExpr) );
      st = cstring_concat (st, temp);

      if (constraint_hasMaxSet(c) )
	{
	  cstring temp2;
	  temp2 = message ("\nHas MaxSet\n");
	  st = cstring_concat (st, temp2);
	}
    }
  return st;
}

cstring  constraint_print (constraint c) /*@*/
{
  cstring st = cstring_undefined;
  cstring type = cstring_undefined;
  llassert (c !=NULL);
  if (c->post)
    {
      type = cstring_makeLiteral ("Ensures: ");
    }
  else
    {
      type = cstring_makeLiteral ("Requires: ");
    }
  st = message ("%s: %s %s %s",
		type,
		constraintExpr_print (c->lexpr),
		arithType_print(c->ar),
		constraintExpr_print(c->expr)
		);
  return st;
}

/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
						   exprNodeList arglist)
{
  precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
							   arglist);
  precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
							   arglist);

  return precondition;
}


constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
{
  postcondition = constraint_copy (postcondition);
  postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
  postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);

  return postcondition;
}

constraint constraint_doSRefFixConstraintParam (constraint precondition,
						   exprNodeList arglist)
{

  precondition = constraint_copy (precondition);
  precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
  precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);

  return precondition;
}

// bool constraint_hasTerm (constraint c, constraintTerm term)
// {
//   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
  
//   if (constraintExpr_includesTerm (c->lexpr, term) )
//     return TRUE;

//   if (constraintExpr_includesTerm (c->expr, term) )
//     return TRUE;

//   return FALSE;
// }

/*@only@*/ constraint constraint_preserveOrig (/*@returned@*/ /*@only@*/ constraint c) /*@modifies c @*/
{
  c->orig = constraint_copy (c);
  return c;
}
/*@=fcnuse*/
/*@=assignexpose*/
/*@=czechfcns@*/
Commit	Line	Data
616915dd	1	/*
	2	** constraintList.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	//# include "exprData.i"
	17
	18	/@i33/
	19	/@-fcnuse/
	20	/@-assignexpose/
	21
dc92450f	22	/@notnull@/ constraint constraint_makeNew (void);
616915dd	23
	24
	25	constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
	26
	27	{
	28	char *t;
	29	int c;
	30	constraint ret;
	31	ret = constraint_makeNew();
	32	llassert (sRef_isValid(x) );
	33	if (!sRef_isValid(x))
	34	return ret;
	35
	36
	37	ret->lexpr = constraintExpr_makeTermsRef (x);
	38	#warning fix abstraction
	39
	40	if (relOp.tok == GE_OP)
	41	ret->ar = GTE;
	42	else if (relOp.tok == LE_OP)
	43	ret->ar = LTE;
	44	else if (relOp.tok == EQ_OP)
	45	ret->ar = EQ;
	46	else
dc92450f	47	llfatalbug(message ("Unsupported relational operator") );
616915dd	48
	49
	50	t = cstring_toCharsSafe (exprNode_unparse(cconstant));
	51	c = atoi( t );
	52	ret->expr = constraintExpr_makeIntLiteral (c);
	53
	54	ret->post = TRUE;
	55	// ret->orig = ret;
	56	DPRINTF(("GENERATED CONSTRAINT:"));
	57	DPRINTF( (message ("%s", constraint_print(ret) ) ) );
	58	return ret;
	59	}
	60
	61	constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
	62
	63	{
	64	char *t;
	65	int c;
	66	constraint ret;
	67	ret = constraint_makeNew();
dc92450f	68	llassert (l!=NULL);
616915dd	69	if (!l)
	70	return ret;
	71
	72
	73	ret->lexpr = constraintExpr_copy (l);
	74	#warning fix abstraction
	75
	76	if (relOp.tok == GE_OP)
	77	ret->ar = GTE;
	78	else if (relOp.tok == LE_OP)
	79	ret->ar = LTE;
	80	else if (relOp.tok == EQ_OP)
	81	ret->ar = EQ;
	82	else
dc92450f	83	llfatalbug(message("Unsupported relational operator") );
616915dd	84
	85
	86	t = cstring_toCharsSafe (exprNode_unparse(cconstant));
	87	c = atoi( t );
	88	ret->expr = constraintExpr_makeIntLiteral (c);
	89
	90	ret->post = TRUE;
	91	// ret->orig = ret;
	92	DPRINTF(("GENERATED CONSTRAINT:"));
	93	DPRINTF( (message ("%s", constraint_print(ret) ) ) );
	94	return ret;
	95	}
	96
	97
	98	constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
	99	{
	100	constraint ret;
	101	ret = constraint_makeNew();
dc92450f	102	llassert (l !=NULL);
616915dd	103	if (!l)
	104	return ret;
	105
	106
	107	ret->lexpr = constraintExpr_copy (l);
	108	#warning fix abstraction
	109
	110	if (relOp.tok == GE_OP)
	111	ret->ar = GTE;
	112	else if (relOp.tok == LE_OP)
	113	ret->ar = LTE;
	114	else if (relOp.tok == EQ_OP)
	115	ret->ar = EQ;
	116	else
dc92450f	117	llfatalbug( message("Unsupported relational operator") );
616915dd	118
	119	ret->expr = constraintExpr_copy (r);
	120
	121	ret->post = TRUE;
	122	// ret->orig = ret;
	123	DPRINTF(("GENERATED CONSTRAINT:"));
	124	DPRINTF( (message ("%s", constraint_print(ret) ) ) );
	125	return ret;
	126	}
	127
	128	constraint constraint_copy (constraint c)
	129	{
	130	constraint ret;
	131	ret = constraint_makeNew();
	132	ret->lexpr = constraintExpr_copy (c->lexpr);
	133	ret->ar = c->ar;
	134	ret->expr = constraintExpr_copy (c->expr);
	135	ret->post = c->post;
dc92450f	136	ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
9280addf	137
616915dd	138	/@i33 fix this/
	139	if (c->orig != NULL)
	140	ret->orig = constraint_copy (c->orig);
	141	else
	142	ret->orig = NULL;
	143	return ret;
	144	}
	145
	146	/like copy expect it doesn't allocate memory for the constraint/
	147
	148	void constraint_overWrite (constraint c1, constraint c2)
	149	{
	150	c1->lexpr = constraintExpr_copy (c2->lexpr);
	151	c1->ar = c2->ar;
	152	c1->expr = constraintExpr_copy (c2->expr);
	153	c1->post = c2->post;
	154	/@i33 fix this/
	155	if (c2->orig != NULL)
	156	c1->orig = constraint_copy (c2->orig);
	157	else
	158	c1->orig = NULL;
dc92450f	159	c1->generatingExpr = exprNode_fakeCopy (c2->generatingExpr );
616915dd	160	}
	161
	162	bool constraint_resolve (/@unused@/ constraint c)
	163	{
	164	return FALSE;
	165	}
	166
	167
	168
dc92450f	169	/@notnull@/ constraint constraint_makeNew (void)
616915dd	170	{
	171	constraint ret;
	172	ret = dmalloc(sizeof (*ret) );
	173	ret->lexpr = NULL;
	174	ret->expr = NULL;
	175	ret->ar = LT;
	176	ret->post = FALSE;
	177	ret->orig = NULL;
9280addf	178	ret->generatingExpr = NULL;
dc92450f	179	return ret;
616915dd	180	}
616915dd	181
9280addf	182	constraint constraint_addGeneratingExpr (/@returned@/ constraint c, exprNode e)
	183	{
	184
	185	if (c->generatingExpr == NULL)
	186	{
dc92450f	187	c->generatingExpr = exprNode_fakeCopy(e);
9280addf	188	DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
	189	}
	190	else
	191	{
	192	DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
	193	}
	194	return c;
	195	}
	196
616915dd	197	fileloc constraint_getFileloc (constraint c)
616915dd	198	{
9280addf	199	if (c->generatingExpr)
	200	return (exprNode_getfileloc (c->generatingExpr) );
	201
616915dd	202	return (constraintExpr_getFileloc (c->lexpr) );
	203
	204
	205	}
	206
9280addf	207	static bool checkForMaxSet (constraint c)
	208	{
	209	if (constraintExpr_hasMaxSet(c->lexpr) \|\| constraintExpr_hasMaxSet(c->expr) )
	210	return TRUE;
	211
	212	return FALSE;
	213	}
	214
	215	bool constraint_hasMaxSet(constraint c)
	216	{
dc92450f	217	if (c->orig != NULL)
9280addf	218	{
	219	if (checkForMaxSet(c->orig) )
	220	return TRUE;
	221	}
	222
	223	return (checkForMaxSet(c) );
	224	}
	225
616915dd	226	constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
	227	{
	228	constraint ret = constraint_makeNew();
	229	// constraintTerm term;
	230	po = exprNode_fakeCopy(po);
	231	ind = exprNode_fakeCopy(ind);
	232	ret->lexpr = constraintExpr_makeMaxReadExpr(po);
	233	ret->ar = GTE;
	234	ret->expr = constraintExpr_makeValueExpr (ind);
	235	return ret;
	236	}
	237
	238	constraint constraint_makeWriteSafeInt (exprNode po, int ind)
	239	{
	240	constraint ret = constraint_makeNew();
	241
	242
	243	ret->lexpr =constraintExpr_makeMaxSetExpr(po);
	244	ret->ar = GTE;
	245	ret->expr = constraintExpr_makeValueInt (ind);
	246	/@i1/return ret;
	247	}
	248
	249	constraint constraint_makeSRefSetBufferSize (sRef s, int size)
	250	{
	251	constraint ret = constraint_makeNew();
	252	ret->lexpr = constraintExpr_makeSRefMaxset (s);
	253	ret->ar = EQ;
	254	ret->expr = constraintExpr_makeValueInt (size);
	255	ret->post = TRUE;
	256	/@i1/return ret;
	257	}
	258
	259	constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
	260	{
	261	constraint ret = constraint_makeNew();
	262
	263
	264	ret->lexpr = constraintExpr_makeSRefMaxset (s);
	265	ret->ar = GTE;
	266	ret->expr = constraintExpr_makeValueInt (ind);
	267	ret->post = TRUE;
	268	/@i1/return ret;
	269	}
	270
	271	/* drl added 01/12/2000
	272
	273	makes the constraint: Ensures index <= MaxRead(buffer) */
	274
	275	constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
	276	{
	277	constraint ret = constraint_makeNew();
	278
	279	ret->lexpr = constraintExpr_makeValueExpr (index);
	280	ret->ar = LTE;
	281	ret->expr = constraintExpr_makeMaxReadExpr(buffer);
	282	ret->post = TRUE;
	283	return ret;
	284	}
	285
	286	constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
	287	{
	288	constraint ret = constraint_makeNew();
	289
290
291	ret->lexpr =constraintExpr_makeMaxSetExpr(po);
292	ret->ar = GTE;
293	ret->expr = constraintExpr_makeValueExpr (ind);
294	/@i1/return ret;
295	}
296
297
298	constraint constraint_makeReadSafeInt ( exprNode po, int ind)
299	{
300	constraint ret = constraint_makeNew();
301
302	po = exprNode_fakeCopy(po);
303
304	ret->lexpr = constraintExpr_makeMaxReadExpr(po);
305	ret->ar = GTE;
306	ret->expr = constraintExpr_makeValueInt (ind);
307	return ret;
308	}
309
310	constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
311	{
312	constraint ret = constraint_makeNew();
313
314
315	e1 = exprNode_fakeCopy (e1);
316	t2 = exprNode_fakeCopy (t2);
317
318	ret = constraint_makeReadSafeExprNode(e1, t2);
319
320	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
321
322	ret->post = TRUE;
323
324	// fileloc_incColumn (ret->lexpr->term->loc);
325	return ret;
326	}
327
328
329	static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar)
330	{
331	constraint ret = constraint_makeNew();
332	exprNode e;
333
334	e = exprNode_fakeCopy(e1);
335	if (! (e1 && e2) )
336	{
337	llcontbug((message("null exprNode, Exprnodes are %s and %s",
338	exprNode_unparse(e1), exprNode_unparse(e2) )
339	));
340	}
341
342	ret->lexpr = constraintExpr_makeValueExpr (e);
343	ret->ar = ar;
344	ret->post = TRUE;
345	e = exprNode_fakeCopy(e2);
346	ret->expr = constraintExpr_makeValueExpr (e);
347
348	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
349	return ret;
350	}
351
352
353	/* make constraint ensures e1 == e2 */
354
355	constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
356	{
357	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
358	}
359
360	/make constraint ensures e1 < e2 /
361	constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
362	{
363	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
364	}
365
366	constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
367	{
368	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
369	}
370
371	constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
372	{
373	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
374	}
375
376	constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
377	{
378	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
379	}
380
381
382	exprNode exprNode_copyConstraints (/@returned@/ exprNode dst, exprNode src)
383	{
384	dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
385	dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
386	dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
387	dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
388	return dst;
389	}
390
391	constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
392	{
393	constraint ret = constraint_makeNew();
394	//constraintTerm term;
395
396	e = exprNode_fakeCopy(e);
397	ret->lexpr = constraintExpr_makeValueExpr (e);
398	ret->ar = EQ;
399	ret->post = TRUE;
400	ret->expr = constraintExpr_makeValueExpr (e);
401	ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
402
403	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
404	// fileloc_incColumn ( ret->lexpr->term->loc);
405	// fileloc_incColumn ( ret->lexpr->term->loc);
406	return ret;
407	}
408	constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
409	{
410	constraint ret = constraint_makeNew();
411	//constraintTerm term;
412
413	e = exprNode_fakeCopy(e);
414	ret->lexpr = constraintExpr_makeValueExpr (e);
415	ret->ar = EQ;
416	ret->post = TRUE;
417	ret->expr = constraintExpr_makeValueExpr (e);
418	ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
419
420	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
421	// fileloc_incColumn ( ret->lexpr->term->loc);
422	// fileloc_incColumn ( ret->lexpr->term->loc);
423	return ret;
424	}
425
426
427
428	// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
429	// {
430	// constraint ret = constraint_makeNew();
431	// //constraintTerm term;
432
433	// e = exprNode_fakeCopy(e);
434	// ret->lexpr = constraintExpr_makeMaxReadExpr(e);
435	// ret->ar = EQ;
436	// ret->post = TRUE;
437	// ret->expr = constraintExpr_makeIncConstraintExpr (e);
438	// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
439	// return ret;
440	// }
441
442
dc92450f	443	cstring arithType_print (arithType ar) /@/
616915dd	444	{
	445	cstring st = cstring_undefined;
	446	switch (ar)
	447	{
	448	case LT:
	449	st = cstring_makeLiteral (" < ");
	450	break;
	451	case LTE:
	452	st = cstring_makeLiteral (" <= ");
	453	break;
	454	case GT:
	455	st = cstring_makeLiteral (" > ");
	456	break;
	457	case GTE:
	458	st = cstring_makeLiteral (" >= ");
	459	break;
	460	case EQ:
	461	st = cstring_makeLiteral (" == ");
	462	break;
	463	case NONNEGATIVE:
	464	st = cstring_makeLiteral (" NONNEGATIVE ");
	465	break;
	466	case POSITIVE:
	467	st = cstring_makeLiteral (" POSITIVE ");
	468	break;
	469	default:
	470	llassert(FALSE);
	471	break;
	472	}
	473	return st;
	474	}
	475
	476	void constraint_printError (constraint c, fileloc loc)
	477	{
	478	cstring string;
9280addf	479	fileloc errorLoc;
9280addf	480
616915dd	481	string = constraint_printDetailed (c);
9280addf	482
	483	errorLoc = loc;
	484
	485	if (constraint_getFileloc(c) )
dc92450f	486	/@-branchstate@/
	487	errorLoc = constraint_getFileloc(c);
	488	/@=branchstate@/
616915dd	489
	490	if (c->post)
	491	{
9280addf	492	voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
616915dd	493	}
	494	else
	495	{
9280addf	496	voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
616915dd	497	}
	498
	499	}
	500
	501	cstring constraint_printDetailed (constraint c)
	502	{
	503	cstring st = cstring_undefined;
	504
	505
	506	if (!c->post)
	507	{
dc92450f	508	if (c->orig != NULL)
616915dd	509	st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
	510	else
	511	st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
	512
	513	}
	514	else
	515	{
dc92450f	516	if (c->orig != NULL)
616915dd	517	st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
	518	else
	519	st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
	520	}
9280addf	521
	522	if (context_getFlag (FLG_CONSTRAINTLOCATION) )
	523	{
	524	cstring temp;
	525	// llassert (c->generatingExpr);
	526	temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
	527	exprNode_unparse(c->generatingExpr) );
	528	st = cstring_concat (st, temp);
	529
	530	if (constraint_hasMaxSet(c) )
	531	{
	532	cstring temp2;
	533	temp2 = message ("\nHas MaxSet\n");
	534	st = cstring_concat (st, temp2);
	535	}
	536	}
616915dd	537	return st;
	538	}
	539
	540	cstring constraint_print (constraint c) /@/
	541	{
	542	cstring st = cstring_undefined;
	543	cstring type = cstring_undefined;
dc92450f	544	llassert (c !=NULL);
616915dd	545	if (c->post)
	546	{
	547	type = cstring_makeLiteral ("Ensures: ");
	548	}
	549	else
	550	{
	551	type = cstring_makeLiteral ("Requires: ");
	552	}
	553	st = message ("%s: %s %s %s",
	554	type,
	555	constraintExpr_print (c->lexpr),
	556	arithType_print(c->ar),
	557	constraintExpr_print(c->expr)
	558	);
	559	return st;
	560	}
	561
dc92450f	562	/@only@/ constraint constraint_doSRefFixBaseParam (/@returned@/ /@only@/ constraint precondition,
616915dd	563	exprNodeList arglist)
	564	{
	565	precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
	566	arglist);
	567	precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
	568	arglist);
	569
	570	return precondition;
	571	}
	572
	573
	574	constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
	575	{
	576	postcondition = constraint_copy (postcondition);
	577	postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
	578	postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
	579
	580	return postcondition;
	581	}
	582
	583	constraint constraint_doSRefFixConstraintParam (constraint precondition,
	584	exprNodeList arglist)
	585	{
	586
	587	precondition = constraint_copy (precondition);
	588	precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
	589	precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
	590
	591	return precondition;
	592	}
	593
	594	// bool constraint_hasTerm (constraint c, constraintTerm term)
	595	// {
	596	// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
	597
	598	// if (constraintExpr_includesTerm (c->lexpr, term) )
	599	// return TRUE;
	600
	601	// if (constraintExpr_includesTerm (c->expr, term) )
	602	// return TRUE;
	603
	604	// return FALSE;
	605	// }
	606
dc92450f	607	/@only@/ constraint constraint_preserveOrig (/@returned@/ /@only@/ constraint c) /@modifies c @/
616915dd	608	{
	609	c->orig = constraint_copy (c);
	610	return c;
	611	}
	612	/@=fcnuse/
	613	/@=assignexpose/
	614	/@=czechfcns@/