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

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