[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*/

/*@access exprNode @*/

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;
}

bool constraint_same (constraint c1, constraint c2)
{
  
  if (c1->ar != c2->ar)
    return FALSE;

  if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
    return FALSE;

  if (!constraintExpr_similar (c1->expr, c2->expr) )
    return FALSE;

  return TRUE;
}

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 = constraint_copy(ret);

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

constraint constraint_copy (constraint c)
{
  constraint ret;

  llassert (constraint_isDefined(c) );
  
  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;

  if (c->or != NULL)
    ret->or = constraint_copy (c->or);
  else
    ret->or = 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;

  if (c2->or != NULL)
    c1->or = constraint_copy (c2->or);
  else
    c1->or = 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->or = 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 (exprNode_isDefined(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_makeIntLiteral (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_makeIntLiteral (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_makeIntLiteral (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_makeIntLiteral (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_makeIntLiteral (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;
}

cstring  constraint_printOr (constraint c) /*@*/
{
  cstring ret;
  constraint temp;

  ret = cstring_undefined;
  temp = c;

  ret = cstring_concat (ret, constraint_print(temp) );

  temp = temp->or;
  
  while ( constraint_isDefined(temp) ) 
    {
      ret = cstring_concat (ret, cstring_makeLiteral (" OR ") );
      ret = cstring_concat (ret, constraint_print(temp) );
      temp = temp->or;
    }

  return ret;

}

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