[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_makeSRefReadSafeInt (sRef s, int ind)
{
  constraint ret = constraint_makeNew();

 
  ret->lexpr = constraintExpr_makeSRefMaxRead (s);
  ret->ar = GTE;
  ret->expr =  constraintExpr_makeValueInt (ind);
  ret->post = TRUE;
  /*@i1*/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_makeEnsuresOpConstraintExpr (constraintExpr c1, constraintExpr c2, fileloc sequencePoint,  arithType  ar)
{

  constraint ret;
  
  llassert(c1 && c2);
  //  llassert(sequencePoint);

  ret = constraint_makeNew();
  
  ret->lexpr = c1;
  ret->ar = ar;
  ret->post = TRUE;
  ret->expr =  c2;
  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
  return ret;
}

static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
{
  constraintExpr c1, c2;
  constraint ret;
  exprNode e;

  if (! (e1 && e2) )
    {
      llcontbug((message("null exprNode, Exprnodes are %s and %s",
		       exprNode_unparse(e1), exprNode_unparse(e2) )
	       ));
    }

  //  llassert (sequencePoint);
  
  e  =  exprNode_fakeCopy(e1);
  c1 =  constraintExpr_makeValueExpr (e);
  
  e  =  exprNode_fakeCopy(e2);
  c2 =  constraintExpr_makeValueExpr (e);

  ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
  
  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)
{
  constraintExpr t1, t2;

  t1 = constraintExpr_makeValueExpr (e1);
  t2 = constraintExpr_makeValueExpr (e2);

  /*change this to e1 <= (e2 -1) */

  t2 = constraintExpr_makeDecConstraintExpr (t2);
  
 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
}

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)
{
  constraintExpr t1, t2;

  t1 = constraintExpr_makeValueExpr (e1);
  t2 = constraintExpr_makeValueExpr (e2);


  /* change this to e1 >= (e2 + 1) */
  t2 = constraintExpr_makeIncConstraintExpr (t2);
  
  
 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
}

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
470b7798	310	constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
	311	{
	312	constraint ret = constraint_makeNew();
	313
	314
	315	ret->lexpr = constraintExpr_makeSRefMaxRead (s);
	316	ret->ar = GTE;
	317	ret->expr = constraintExpr_makeValueInt (ind);
	318	ret->post = TRUE;
	319	/@i1/return ret;
	320	}
	321
616915dd	322	constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
	323	{
	324	constraint ret = constraint_makeNew();
	325
	326
	327	e1 = exprNode_fakeCopy (e1);
	328	t2 = exprNode_fakeCopy (t2);
	329
	330	ret = constraint_makeReadSafeExprNode(e1, t2);
	331
	332	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
	333
	334	ret->post = TRUE;
	335
	336	// fileloc_incColumn (ret->lexpr->term->loc);
	337	return ret;
	338	}
	339
470b7798	340	static constraint constraint_makeEnsuresOpConstraintExpr (constraintExpr c1, constraintExpr c2, fileloc sequencePoint, arithType ar)
	341	{
	342
	343	constraint ret;
	344
	345	llassert(c1 && c2);
	346	// llassert(sequencePoint);
	347
	348	ret = constraint_makeNew();
	349
	350	ret->lexpr = c1;
	351	ret->ar = ar;
	352	ret->post = TRUE;
	353	ret->expr = c2;
	354	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
	355	return ret;
	356	}
616915dd	357
	358	static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint, arithType ar)
	359	{
470b7798	360	constraintExpr c1, c2;
470b7798	361	constraint ret;
616915dd	362	exprNode e;
470b7798	363
616915dd	364	if (! (e1 && e2) )
	365	{
	366	llcontbug((message("null exprNode, Exprnodes are %s and %s",
	367	exprNode_unparse(e1), exprNode_unparse(e2) )
	368	));
	369	}
470b7798	370
	371	// llassert (sequencePoint);
	372
	373	e = exprNode_fakeCopy(e1);
	374	c1 = constraintExpr_makeValueExpr (e);
	375
	376	e = exprNode_fakeCopy(e2);
	377	c2 = constraintExpr_makeValueExpr (e);
	378
	379	ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
616915dd	380
616915dd	381	return ret;
	382	}
	383
	384
	385	/* make constraint ensures e1 == e2 */
	386
	387	constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
	388	{
	389	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
	390	}
	391
	392	/make constraint ensures e1 < e2 /
	393	constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
	394	{
470b7798	395	constraintExpr t1, t2;
	396
	397	t1 = constraintExpr_makeValueExpr (e1);
	398	t2 = constraintExpr_makeValueExpr (e2);
	399
	400	/change this to e1 <= (e2 -1) /
	401
	402	t2 = constraintExpr_makeDecConstraintExpr (t2);
	403
	404	return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
616915dd	405	}
	406
	407	constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
	408	{
	409	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
	410	}
	411
	412	constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
	413	{
470b7798	414	constraintExpr t1, t2;
	415
	416	t1 = constraintExpr_makeValueExpr (e1);
	417	t2 = constraintExpr_makeValueExpr (e2);
	418
	419
	420	/* change this to e1 >= (e2 + 1) */
	421	t2 = constraintExpr_makeIncConstraintExpr (t2);
	422
	423
	424	return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
616915dd	425	}
	426
	427	constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
	428	{
	429	return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
	430	}
	431
	432
	433	exprNode exprNode_copyConstraints (/@returned@/ exprNode dst, exprNode src)
	434	{
	435	dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
	436	dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
	437	dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
	438	dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
	439	return dst;
	440	}
	441
	442	constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
	443	{
	444	constraint ret = constraint_makeNew();
	445	//constraintTerm term;
	446
	447	e = exprNode_fakeCopy(e);
	448	ret->lexpr = constraintExpr_makeValueExpr (e);
	449	ret->ar = EQ;
	450	ret->post = TRUE;
	451	ret->expr = constraintExpr_makeValueExpr (e);
	452	ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
	453
	454	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
	455	// fileloc_incColumn ( ret->lexpr->term->loc);
	456	// fileloc_incColumn ( ret->lexpr->term->loc);
	457	return ret;
	458	}
	459	constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
	460	{
	461	constraint ret = constraint_makeNew();
	462	//constraintTerm term;
	463
	464	e = exprNode_fakeCopy(e);
	465	ret->lexpr = constraintExpr_makeValueExpr (e);
	466	ret->ar = EQ;
	467	ret->post = TRUE;
	468	ret->expr = constraintExpr_makeValueExpr (e);
	469	ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
	470
	471	ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
	472	// fileloc_incColumn ( ret->lexpr->term->loc);
	473	// fileloc_incColumn ( ret->lexpr->term->loc);
	474	return ret;
	475	}
	476
	477
	478
	479	// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
	480	// {
	481	// constraint ret = constraint_makeNew();
	482	// //constraintTerm term;
	483
	484	// e = exprNode_fakeCopy(e);
	485	// ret->lexpr = constraintExpr_makeMaxReadExpr(e);
	486	// ret->ar = EQ;
	487	// ret->post = TRUE;
	488	// ret->expr = constraintExpr_makeIncConstraintExpr (e);
489	// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
490	// return ret;
491	// }
492
493
dc92450f	494	cstring arithType_print (arithType ar) /@/
616915dd	495	{
	496	cstring st = cstring_undefined;
	497	switch (ar)
	498	{
	499	case LT:
	500	st = cstring_makeLiteral (" < ");
	501	break;
	502	case LTE:
	503	st = cstring_makeLiteral (" <= ");
	504	break;
	505	case GT:
	506	st = cstring_makeLiteral (" > ");
	507	break;
	508	case GTE:
	509	st = cstring_makeLiteral (" >= ");
	510	break;
	511	case EQ:
	512	st = cstring_makeLiteral (" == ");
	513	break;
	514	case NONNEGATIVE:
	515	st = cstring_makeLiteral (" NONNEGATIVE ");
	516	break;
	517	case POSITIVE:
	518	st = cstring_makeLiteral (" POSITIVE ");
	519	break;
	520	default:
	521	llassert(FALSE);
	522	break;
	523	}
	524	return st;
	525	}
	526
	527	void constraint_printError (constraint c, fileloc loc)
	528	{
	529	cstring string;
9280addf	530	fileloc errorLoc;
9280addf	531
616915dd	532	string = constraint_printDetailed (c);
9280addf	533
	534	errorLoc = loc;
	535
	536	if (constraint_getFileloc(c) )
dc92450f	537	/@-branchstate@/
	538	errorLoc = constraint_getFileloc(c);
	539	/@=branchstate@/
616915dd	540
	541	if (c->post)
	542	{
9280addf	543	voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
616915dd	544	}
	545	else
	546	{
9280addf	547	voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
616915dd	548	}
	549
	550	}
	551
	552	cstring constraint_printDetailed (constraint c)
	553	{
	554	cstring st = cstring_undefined;
	555
	556
	557	if (!c->post)
	558	{
dc92450f	559	if (c->orig != NULL)
616915dd	560	st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
	561	else
	562	st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
	563
	564	}
	565	else
	566	{
dc92450f	567	if (c->orig != NULL)
616915dd	568	st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
	569	else
	570	st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
	571	}
9280addf	572
	573	if (context_getFlag (FLG_CONSTRAINTLOCATION) )
	574	{
	575	cstring temp;
	576	// llassert (c->generatingExpr);
	577	temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
	578	exprNode_unparse(c->generatingExpr) );
	579	st = cstring_concat (st, temp);
	580
	581	if (constraint_hasMaxSet(c) )
	582	{
	583	cstring temp2;
	584	temp2 = message ("\nHas MaxSet\n");
	585	st = cstring_concat (st, temp2);
	586	}
	587	}
616915dd	588	return st;
	589	}
	590
	591	cstring constraint_print (constraint c) /@/
	592	{
	593	cstring st = cstring_undefined;
	594	cstring type = cstring_undefined;
dc92450f	595	llassert (c !=NULL);
616915dd	596	if (c->post)
	597	{
	598	type = cstring_makeLiteral ("Ensures: ");
	599	}
	600	else
	601	{
	602	type = cstring_makeLiteral ("Requires: ");
	603	}
	604	st = message ("%s: %s %s %s",
	605	type,
	606	constraintExpr_print (c->lexpr),
	607	arithType_print(c->ar),
	608	constraintExpr_print(c->expr)
	609	);
	610	return st;
	611	}
	612
dc92450f	613	/@only@/ constraint constraint_doSRefFixBaseParam (/@returned@/ /@only@/ constraint precondition,
616915dd	614	exprNodeList arglist)
	615	{
	616	precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
	617	arglist);
	618	precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
	619	arglist);
	620
	621	return precondition;
	622	}
	623
	624
	625	constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
	626	{
	627	postcondition = constraint_copy (postcondition);
	628	postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
	629	postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
	630
	631	return postcondition;
	632	}
	633
	634	constraint constraint_doSRefFixConstraintParam (constraint precondition,
	635	exprNodeList arglist)
	636	{
	637
	638	precondition = constraint_copy (precondition);
	639	precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
	640	precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
	641
	642	return precondition;
	643	}
	644
	645	// bool constraint_hasTerm (constraint c, constraintTerm term)
	646	// {
	647	// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
	648
	649	// if (constraintExpr_includesTerm (c->lexpr, term) )
	650	// return TRUE;
	651
	652	// if (constraintExpr_includesTerm (c->expr, term) )
	653	// return TRUE;
	654
	655	// return FALSE;
	656	// }
	657
dc92450f	658	/@only@/ constraint constraint_preserveOrig (/@returned@/ /@only@/ constraint c) /@modifies c @/
616915dd	659	{
	660	c->orig = constraint_copy (c);
	661	return c;
	662	}
	663	/@=fcnuse/
	664	/@=assignexpose/
	665	/@=czechfcns@/