[splint.git] / src / constraintResolve.c

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

#include "constraintExpr.h"


constraintList reflectChanges (constraintList pre2, constraintList post1);
constraint substitute (constraint c, constraintList p);
constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2);
bool satifies (constraint pre, constraint post);
bool resolve (constraint c, constraintList p);
constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
constraint constraint_simplify (constraint c);

constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);

constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);

constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
constraint  inequalitySubstitute  (constraint c, constraintList p);

/*********************************************/

					    
constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
{
  constraintList ret;
  constraintList temp;
  ret = constraintList_new();
  
  ret = reflectChangesEnsures (list1, list2);
  ret = constraintList_fixConflicts (ret, list2);
  ret = constraintList_subsumeEnsures (ret, list2);
  list2 = constraintList_subsumeEnsures (list2, ret);
  temp = constraintList_copy(list2);

  temp = constraintList_addList (temp, ret);
  return temp;
  //ret = constraintList_addList (ret, list2);
  //return ret;
}

					    
/* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */
/* { */
  
/*   constraintList ret; */
/*   constraintList temp; */
/*   ret = constraintList_new(); */
  
/*   ret = reflectChangesEnsures (list1, list2); */
/*   ret = constraintList_fixConflicts (ret, list2); */
/*   ret = constraintList_subsumeEnsures (ret, list2); */
/*   list2 = constraintList_subsumeEnsures (list2, ret); */
/*   temp = constraintList_copy(list2); */

/*   temp = constraintList_addList (temp, ret); */
/*   return temp; */
/*   //ret = constraintList_addList (ret, list2); */
/*   //return ret; */
/* } */

void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint)
{
  temp->requiresConstraints = constraintList_new();
  temp->ensuresConstraints = constraintList_new();
  temp->trueEnsuresConstraints = constraintList_new();
  temp->falseEnsuresConstraints = constraintList_new();
  
  exprNodeList_elements (arglist, el)
    {
      exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
      el->requiresConstraints = exprNode_traversRequiresConstraints(el);
      el->ensuresConstraints  = exprNode_traversEnsuresConstraints(el);

      temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
							    el->requiresConstraints);
      
      temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
							   el->ensuresConstraints);
    }
  end_exprNodeList_elements;
  
}

constraintList checkCall (exprNode fcn, exprNodeList arglist)
{
  constraintList preconditions;
  uentry temp;
  DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );

  temp = exprNode_getUentry (fcn);

  preconditions = uentry_getFcnPreconditions (temp);

  if (preconditions)
    {
      preconditions = constraintList_copy(preconditions);
      preconditions= constraintList_togglePost (preconditions);   
      preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
    }
  else
    {
      preconditions = constraintList_new();
    }
  
  return preconditions;
}

constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
{
  constraintList postconditions;
  uentry temp;
  DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );

  temp = exprNode_getUentry (fcn);

  postconditions = uentry_getFcnPostconditions (temp);

  if (postconditions)
    {
      postconditions = constraintList_copy(postconditions);
      postconditions = constraintList_doFixResult (postconditions, fcnCall);
      postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
    }
  else
    {
      postconditions = constraintList_new();
    }
  
  return postconditions;
}

void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
{
  constraintList temp;

  DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));

  DPRINTF( (message (" children:  %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );

  if (exprNode_isError (child1)  || exprNode_isError(child2) )
     {
       if (exprNode_isError (child1) && !exprNode_isError(child2) )
	 {
	   parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
	   parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
	   DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
			     constraintList_print( child2->requiresConstraints),
			     constraintList_print (child2->ensuresConstraints)
			     )
		    ));
	   return;
	 }
       else
	 {
	   llassert(exprNode_isError(child2) );
	   parent->requiresConstraints = constraintList_new();
	   parent->ensuresConstraints = constraintList_new();
	   return;
	 }
     }

   llassert(!exprNode_isError (child1)  && ! exprNode_isError(child2) );
   
   DPRINTF( (message ("Child constraints are %s %s and %s %s",
		     constraintList_print (child1->requiresConstraints),
		     constraintList_print (child1->ensuresConstraints),
		     constraintList_print (child2->requiresConstraints),
		     constraintList_print (child2->ensuresConstraints)
		     ) ) );
 
  parent->requiresConstraints = constraintList_new();
  parent->ensuresConstraints = constraintList_new();

  parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
  
  temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
  parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp);

  parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
							   child2->ensuresConstraints);
  
  DPRINTF( (message ("Parent constraints are %s and %s ",
		     constraintList_print (parent->requiresConstraints),
		     constraintList_print (parent->ensuresConstraints)
		     ) ) );
 
}


constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
{
  constraintList ret;
  ret = constraintList_new();
  constraintList_elements (list1, el)
    {
      
      DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
      if (!resolve (el, list2) )
	{
	    ret = constraintList_add (ret, el);
	}
      else
	{
	  DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
	}
    } end_constraintList_elements;

    return ret;
}


constraintList reflectChanges (constraintList pre2, constraintList post1)
{
  
  constraintList ret;
  constraint temp;
  ret = constraintList_new();
  DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
  
  constraintList_elements (pre2, el)
    {
      if (!resolve (el, post1) )
	{
	  temp = substitute (el, post1);
	  if (!resolve (temp, post1) )
	    {
	      // try inequality substitution
	      constraint temp2;
	      
	      // the inequality substitution may cause us to lose information
	      //so we don't want to store the result but we do it anyway
	      temp2 = constraint_copy (temp);
	      temp2 = inequalitySubstitute (temp, post1);
	      if (!resolve (temp2, post1) )
		  ret = constraintList_add (ret, temp2);
	    }
	}
    } end_constraintList_elements;

    DPRINTF((message ("reflectChanges: returning %s", constraintList_print(ret) ) ) );
    return ret;
}


constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
{  
  constraintList ret;
  constraint temp;
  ret = constraintList_new();
  constraintList_elements (pre2, el)
    {
      if (!resolve (el, post1) )
	{
	  temp = substitute (el, post1);
	  llassert (temp != NULL);

	  if (!resolve (temp, post1) )
	    ret = constraintList_add (ret, temp);
	}
      else
	{
	  DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
	}
    } end_constraintList_elements;

    return ret;
}


bool constraint_conflict (constraint c1, constraint c2)
{
  
  if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
    {
      if (c1->ar == EQ)
	if (c1->ar == c2->ar)
	  {
	    DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
	    return TRUE;
	  }
    }  

  DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );

  return FALSE; 

}

void constraint_fixConflict (constraint good, constraint conflicting)
{
  constraint temp;
  if (conflicting->ar ==EQ )
    {
      good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
      temp = constraint_simplify (good);
      constraint_overWrite (good, temp);
    }


}

bool conflict (constraint c, constraintList list)
{
  
   constraintList_elements (list, el)
    {
      if ( constraint_conflict(el, c) )
	{
	  constraint_fixConflict (el, c);
	  return TRUE;
	}
    } end_constraintList_elements;

    return FALSE;
  

}

//check if constraint in list1 and conflict with constraints in List2.  If so we
//remove form list1 and (optionally) change list2.
constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
{
  constraintList ret;
  ret = constraintList_new();
  constraintList_elements (list1, el)
    {
      if (! conflict (el, list2) )
	{
	    ret = constraintList_add (ret, el);
	}
    } end_constraintList_elements;

    return ret;
  
    
}

bool resolve (constraint c, constraintList p)
{
  constraintList_elements (p, el)
    {
      if ( satifies (c, el) )
	{
	  DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
	  return TRUE;
	}
        DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) );
    }
  end_constraintList_elements;
  DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
  return FALSE;
}


/*returns true if cosntraint post satifies cosntriant pre */
bool satifies (constraint pre, constraint post)
{
  if (constraint_isAlwaysTrue (pre)  )
    return TRUE;
  
  if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
    {
      return FALSE;
    }
  if (post->expr == NULL)
    {
      llassert(FALSE);
      return FALSE;
    }

  return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
}

bool arithType_canResolve (arithType ar1, arithType ar2)
{
  switch (ar1)
    {
    case GTE:
    case GT:
      if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
	{
	  return TRUE;
	}
      break;

    case EQ:
      if (ar2 == EQ)
	return TRUE;
      break;

    case LT:
    case LTE:
      //      llassert(FALSE); 
      if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
	return TRUE;
    default:
      return FALSE;
    }
  return FALSE;	  
}

bool constraint_isAlwaysTrue (constraint c)
{
  constraintExpr l, r;
  bool lHasConstant, rHasConstant;
  int lConstant, rConstant;
  
  l = c->lexpr;
  r = c->expr;
    
  if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) )
    {
      int cmp;
      cmp = constraintExpr_compare (l, r);
      switch (c->ar)
	{
	case EQ:
	  return (cmp == 0);
	case GT:
	  return (cmp > 0);
	case GTE:
	  return (cmp >= 0);
	case LTE:
	  return (cmp <= 0);
	case LT:
	  return (cmp < 0);

	default:
	  BADEXIT;
	  break;
	}
    }

  if (constraintExpr_similar (l,r) )
    {
      switch (c->ar)
	{
	case EQ:
	case GTE:
	case LTE:
	  return TRUE;
	  
	case GT:
	case LT:
	  break;
	default:
	  BADEXIT;
	  break;
	}
    }

  l = constraintExpr_copy (c->lexpr);
  r = constraintExpr_copy (c->expr);

  //  l = constraintExpr_propagateConstants (l, &lHasConstant, &lConstant);
  r = constraintExpr_propagateConstants (r, &rHasConstant, &rConstant);

  if (constraintExpr_similar (l,r) )
    {
      DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants  %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) ));
      if (rHasConstant)
	{
	  DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is  %d", rConstant ) ));
	  switch (c->ar)
	    {
	    case EQ:
	      return (rConstant == 0);
	    case LT:
	      return (rConstant > 0);
	    case LTE:
	      return (rConstant >= 0);
	    case GTE:
	      return (rConstant <= 0);
	    case GT:
	      return (rConstant < 0);
	      
	    default:
	      BADEXIT;
	      break;
	    }
	}
      
    }  
  else
    {
      DPRINTF(( message("Constraint %s is not always true", constraint_print(c) ) ));
      return FALSE;
    }
  
  BADEXIT;
}

bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)

{
  DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));

  if (! arithType_canResolve (ar1, ar2) )
    return FALSE;
  
  switch (ar1)
 {
 case GTE:
      if (constraintExpr_similar (expr1, expr2) )
	 return TRUE;
 case GT:
   if (!  (constraintExpr_canGetValue (expr1) &&
	   constraintExpr_canGetValue (expr2) ) )
     {
       DPRINTF( ("Can't Get value"));
       return FALSE;
     }
   
   if (constraintExpr_compare (expr2, expr1) >= 0)
     return TRUE;
  
  return FALSE;
 case EQ:
   if (constraintExpr_similar (expr1, expr2) )
	 return TRUE;
   
   return FALSE;
 case LTE:
   if (constraintExpr_similar (expr1, expr2) )
	 return TRUE;
 case LT:
    if (!  (constraintExpr_canGetValue (expr1) &&
	   constraintExpr_canGetValue (expr2) ) )
     {
       DPRINTF( ("Can't Get value"));
       return FALSE;
     }
   
   if (constraintExpr_compare (expr2, expr1) <= 0)
     return TRUE;

   return FALSE;
   
 default:
     llcontbug((message("Unhandled case in switch: %s", arithType_print(ar1) ) ) );
 }
  BADEXIT;
  return FALSE;
}


constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new)
{
  DPRINTF (("Doing replace for lexpr") );
  c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
  DPRINTF (("Doing replace for expr") );
  c->expr = constraintExpr_searchandreplace (c->expr, old, new);
  return c;
}

bool constraint_search (constraint c, constraintExpr old)
{
  bool ret;
  ret = FALSE;

  ret  = constraintExpr_search (c->lexpr, old);
  ret = ret || constraintExpr_search (c->expr, old);
  return ret;
}

//adjust file locs and stuff
constraint constraint_adjust (constraint substitute, constraint old)
{
  fileloc loc1, loc2, loc3;

  DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
		     constraint_print(old))
		   ));

  loc1 = constraint_getFileloc (old);

  loc2 = constraintExpr_getFileloc (substitute->lexpr);

  loc3 = constraintExpr_getFileloc (substitute->expr);

  
  // special case of an equality that "contains itself"
  if (constraintExpr_search (substitute->expr, substitute->lexpr) )
      if (fileloc_closer (loc1, loc3, loc2))
      {
	constraintExpr temp;
	DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
		   ));
	temp = substitute->lexpr;
	substitute->lexpr = substitute->expr;
	substitute->expr  = temp;
	substitute = constraint_simplify(substitute);
      }

  return substitute;
  
}

constraint  inequalitySubstitute  (constraint c, constraintList p)
{
  if (c->ar != GTE)
    return c;
  
  constraintList_elements (p, el)
    {
       if ( el->ar == LT)
	 //	 if (!constraint_conflict (c, el) )
	   {
	     constraint temp;
	     temp = constraint_copy(el);
	     
	     //	     temp = constraint_adjust(temp, c);

	     if (constraintExpr_same (el->lexpr, c->expr) )
	       {
		 DPRINTF((message ("Replacing %s in %s with  %s",
				   constraintExpr_print (c->expr),
				   constraint_print (c),
				   constraintExpr_print (el->expr) )
			  ));
		 c->expr = constraintExpr_copy (el->expr);
	       }
	     
	   }
    }
  end_constraintList_elements;

  c = constraint_simplify(c);
  return c;
}

constraint substitute (constraint c, constraintList p)
{
  constraintList_elements (p, el)
    {
       if ( el->ar == EQ)
	 if (!constraint_conflict (c, el) )

	   {
	     constraint temp;
	     temp = constraint_copy(el);
	     
	     temp = constraint_adjust(temp, c);

	     DPRINTF((message ("Substituting %s for %s",
			       constraint_print (temp), constraint_print (c)
			       ) ) );
			       
	  
	     c = constraint_searchandreplace (c, temp->lexpr, temp->expr);
	   }
    }
  end_constraintList_elements;

  c = constraint_simplify(c);
  return c;
}


constraint constraint_solve (constraint c)
{
  DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
  c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
  DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );

  return c;
}

static arithType flipAr (arithType ar)
{
  switch (ar)
    {
    case LT:
      return GT;
    case LTE:
      return GTE;
    case EQ:
      return EQ;
    case GT:
      return LT;
    case GTE:
      return LTE;
    default:
      llcontbug (("unexpected value: case not handled"));
    }
  BADEXIT;
}

static constraint  constraint_swapLeftRight (constraint c)
{
  constraintExpr temp;
  c->ar = flipAr (c->ar);
  temp = c->lexpr;
  c->lexpr = c->expr;
  c->expr = temp;
  DPRINTF(("Swaped left and right sides of constraint"));
  return c;
}

constraint constraint_simplify (constraint c)
{
  c->lexpr = constraintExpr_simplify (c->lexpr);
  c->expr  = constraintExpr_simplify (c->expr);
  
  c = constraint_solve (c);
  
  c->lexpr = constraintExpr_simplify (c->lexpr);
  c->expr  = constraintExpr_simplify (c->expr);

  if (constraintExpr_isLit(c->lexpr) && (!constraintExpr_isLit(c->expr) ) )
    {
      c = constraint_swapLeftRight(c);
      /*I don't think this will be an infinate loop*/
      constraint_simplify(c);
    }
  return c;
}


/* returns true  if fileloc for term1 is closer to file for term2 than term3*/

bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3)
{
   if ( fileloc_lessthan (loc1, loc2) )
     {
       if (fileloc_lessthan (loc2, loc3) )
	 {
	   llassert (fileloc_lessthan (loc1, loc3) );
	   return TRUE;
	 }
       else
	 {
	   return FALSE;
	 }
     }

   if ( !fileloc_lessthan (loc1, loc2) )
     {
       if (!fileloc_lessthan (loc2, loc3) )
	 {
	   llassert (!fileloc_lessthan (loc1, loc3) );
	   return TRUE;
	 }
       else
	 {
	   return FALSE;
	 }
     }

   llassert(FALSE);
   return FALSE;
}
Commit	Line	Data
616915dd	1	/*
	2	*
	3	** constraintResolve.c
	4	*/
	5
	6	//#define DEBUGPRINT 1
	7
	8	# include <ctype.h> /* for isdigit */
	9	# include "lclintMacros.nf"
	10	# include "basic.h"
	11	# include "cgrammar.h"
	12	# include "cgrammar_tokens.h"
	13
	14	# include "exprChecks.h"
	15	# include "aliasChecks.h"
	16	# include "exprNodeSList.h"
	17	//# include "exprData.i"
	18
	19	#include "constraintExpr.h"
	20
	21
	22
	23
	24
	25	constraintList reflectChanges (constraintList pre2, constraintList post1);
	26	constraint substitute (constraint c, constraintList p);
	27	constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
	28	bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2);
	29	bool satifies (constraint pre, constraint post);
	30	bool resolve (constraint c, constraintList p);
	31	constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
	32	constraint constraint_simplify (constraint c);
	33
	34	constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);
	35
	36	constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
	37
	38	constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
	39	constraint inequalitySubstitute (constraint c, constraintList p);
	40
	41	/*********************************************/
	42
	43
	44	constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
	45	{
	46	constraintList ret;
	47	constraintList temp;
	48	ret = constraintList_new();
	49
	50	ret = reflectChangesEnsures (list1, list2);
	51	ret = constraintList_fixConflicts (ret, list2);
	52	ret = constraintList_subsumeEnsures (ret, list2);
	53	list2 = constraintList_subsumeEnsures (list2, ret);
	54	temp = constraintList_copy(list2);
	55
	56	temp = constraintList_addList (temp, ret);
	57	return temp;
	58	//ret = constraintList_addList (ret, list2);
	59	//return ret;
	60	}
	61
	62
	63	/* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */
	64	/* { */
65
66	/* constraintList ret; */
67	/* constraintList temp; */
68	/* ret = constraintList_new(); */
69
70	/* ret = reflectChangesEnsures (list1, list2); */
71	/* ret = constraintList_fixConflicts (ret, list2); */
72	/* ret = constraintList_subsumeEnsures (ret, list2); */
73	/* list2 = constraintList_subsumeEnsures (list2, ret); */
74	/* temp = constraintList_copy(list2); */
75
76	/* temp = constraintList_addList (temp, ret); */
77	/* return temp; */
78	/* //ret = constraintList_addList (ret, list2); */
79	/* //return ret; */
80	/* } */
81
9280addf	82	void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint)
	83	{
	84	temp->requiresConstraints = constraintList_new();
	85	temp->ensuresConstraints = constraintList_new();
	86	temp->trueEnsuresConstraints = constraintList_new();
	87	temp->falseEnsuresConstraints = constraintList_new();
	88
	89	exprNodeList_elements (arglist, el)
	90	{
	91	exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
	92	el->requiresConstraints = exprNode_traversRequiresConstraints(el);
	93	el->ensuresConstraints = exprNode_traversEnsuresConstraints(el);
	94
	95	temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
	96	el->requiresConstraints);
	97
	98	temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
	99	el->ensuresConstraints);
	100	}
	101	end_exprNodeList_elements;
	102
	103	}
616915dd	104
	105	constraintList checkCall (exprNode fcn, exprNodeList arglist)
	106	{
	107	constraintList preconditions;
	108	uentry temp;
	109	DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
	110
	111	temp = exprNode_getUentry (fcn);
	112
	113	preconditions = uentry_getFcnPreconditions (temp);
	114
	115	if (preconditions)
	116	{
	117	preconditions = constraintList_copy(preconditions);
	118	preconditions= constraintList_togglePost (preconditions);
	119	preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
	120	}
	121	else
	122	{
	123	preconditions = constraintList_new();
	124	}
	125
	126	return preconditions;
	127	}
	128
	129	constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
	130	{
	131	constraintList postconditions;
	132	uentry temp;
	133	DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
	134
	135	temp = exprNode_getUentry (fcn);
	136
	137	postconditions = uentry_getFcnPostconditions (temp);
	138
	139	if (postconditions)
	140	{
	141	postconditions = constraintList_copy(postconditions);
	142	postconditions = constraintList_doFixResult (postconditions, fcnCall);
	143	postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
	144	}
	145	else
	146	{
	147	postconditions = constraintList_new();
	148	}
	149
	150	return postconditions;
	151	}
	152
	153	void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
	154	{
	155	constraintList temp;
	156
	157	DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));
	158
	159	DPRINTF( (message (" children: %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );
	160
	161	if (exprNode_isError (child1) \|\| exprNode_isError(child2) )
	162	{
	163	if (exprNode_isError (child1) && !exprNode_isError(child2) )
	164	{
	165	parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
	166	parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
	167	DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
168	constraintList_print( child2->requiresConstraints),
169	constraintList_print (child2->ensuresConstraints)
170	)
171	));
172	return;
173	}
174	else
175	{
176	llassert(exprNode_isError(child2) );
177	parent->requiresConstraints = constraintList_new();
178	parent->ensuresConstraints = constraintList_new();
179	return;
180	}
181	}
182
183	llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) );
184
9280addf	185	DPRINTF( (message ("Child constraints are %s %s and %s %s",
616915dd	186	constraintList_print (child1->requiresConstraints),
	187	constraintList_print (child1->ensuresConstraints),
	188	constraintList_print (child2->requiresConstraints),
	189	constraintList_print (child2->ensuresConstraints)
	190	) ) );
	191
	192	parent->requiresConstraints = constraintList_new();
	193	parent->ensuresConstraints = constraintList_new();
	194
	195	parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
	196
	197	temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
	198	parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp);
	199
	200	parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
	201	child2->ensuresConstraints);
	202
	203	DPRINTF( (message ("Parent constraints are %s and %s ",
	204	constraintList_print (parent->requiresConstraints),
	205	constraintList_print (parent->ensuresConstraints)
	206	) ) );
	207
	208	}
	209
	210
	211
	212
	213	constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
	214	{
	215	constraintList ret;
	216	ret = constraintList_new();
	217	constraintList_elements (list1, el)
	218	{
	219
	220	DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
	221	if (!resolve (el, list2) )
	222	{
	223	ret = constraintList_add (ret, el);
	224	}
	225	else
	226	{
	227	DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
	228	}
	229	} end_constraintList_elements;
	230
	231	return ret;
	232	}
	233
	234
	235	constraintList reflectChanges (constraintList pre2, constraintList post1)
	236	{
	237
	238	constraintList ret;
	239	constraint temp;
	240	ret = constraintList_new();
	241	DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
	242
	243	constraintList_elements (pre2, el)
	244	{
	245	if (!resolve (el, post1) )
	246	{
	247	temp = substitute (el, post1);
	248	if (!resolve (temp, post1) )
	249	{
250	// try inequality substitution
251	constraint temp2;
252
253	// the inequality substitution may cause us to lose information
254	//so we don't want to store the result but we do it anyway
255	temp2 = constraint_copy (temp);
256	temp2 = inequalitySubstitute (temp, post1);
257	if (!resolve (temp2, post1) )
258	ret = constraintList_add (ret, temp2);
259	}
260	}
261	} end_constraintList_elements;
262
263	DPRINTF((message ("reflectChanges: returning %s", constraintList_print(ret) ) ) );
264	return ret;
265	}
266
267
268
269	constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
270	{
271	constraintList ret;
272	constraint temp;
273	ret = constraintList_new();
274	constraintList_elements (pre2, el)
275	{
276	if (!resolve (el, post1) )
277	{
278	temp = substitute (el, post1);
279	llassert (temp != NULL);
280
281	if (!resolve (temp, post1) )
282	ret = constraintList_add (ret, temp);
283	}
284	else
285	{
286	DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
287	}
288	} end_constraintList_elements;
289
290	return ret;
291	}
292
293
294	bool constraint_conflict (constraint c1, constraint c2)
295	{
296
297	if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
298	{
299	if (c1->ar == EQ)
300	if (c1->ar == c2->ar)
301	{
302	DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
303	return TRUE;
304	}
305	}
306
307	DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
308
309	return FALSE;
310
311	}
312
313	void constraint_fixConflict (constraint good, constraint conflicting)
314	{
315	constraint temp;
316	if (conflicting->ar ==EQ )
317	{
318	good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
319	temp = constraint_simplify (good);
320	constraint_overWrite (good, temp);
321	}
322
323
324	}
325
326	bool conflict (constraint c, constraintList list)
327	{
328
329	constraintList_elements (list, el)
330	{
331	if ( constraint_conflict(el, c) )
332	{
333	constraint_fixConflict (el, c);
334	return TRUE;
335	}
336	} end_constraintList_elements;
337
338	return FALSE;
339
340
341	}
342
343	//check if constraint in list1 and conflict with constraints in List2. If so we
344	//remove form list1 and (optionally) change list2.
345	constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
346	{
347	constraintList ret;
348	ret = constraintList_new();
349	constraintList_elements (list1, el)
350	{
351	if (! conflict (el, list2) )
352	{
353	ret = constraintList_add (ret, el);
354	}
355	} end_constraintList_elements;
356
357	return ret;
358
359
360	}
361
362	bool resolve (constraint c, constraintList p)
363	{
364	constraintList_elements (p, el)
365	{
366	if ( satifies (c, el) )
367	{
368	DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
369	return TRUE;
370	}
371	DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) );
372	}
373	end_constraintList_elements;
374	DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
375	return FALSE;
376	}
377
378
379	/returns true if cosntraint post satifies cosntriant pre /
380	bool satifies (constraint pre, constraint post)
381	{
382	if (constraint_isAlwaysTrue (pre) )
383	return TRUE;
384
385	if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
386	{
387	return FALSE;
388	}
389	if (post->expr == NULL)
390	{
391	llassert(FALSE);
392	return FALSE;
393	}
394
395	return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
396	}
397
398	bool arithType_canResolve (arithType ar1, arithType ar2)
399	{
400	switch (ar1)
401	{
402	case GTE:
403	case GT:
404	if ( (ar2 == GT) \|\| (ar2 == GTE) \|\| (ar2 == EQ) )
405	{
406	return TRUE;
407	}
408	break;
409
410	case EQ:
411	if (ar2 == EQ)
412	return TRUE;
413	break;
414
415	case LT:
416	case LTE:
417	// llassert(FALSE);
418	if ( (ar2 == LT) \|\| (ar2 == LTE) \|\| (ar2 == EQ) )
419	return TRUE;
420	default:
421	return FALSE;
422	}
423	return FALSE;
424	}
425
426	bool constraint_isAlwaysTrue (constraint c)
427	{
428	constraintExpr l, r;
9280addf	429	bool lHasConstant, rHasConstant;
	430	int lConstant, rConstant;
	431
616915dd	432	l = c->lexpr;
616915dd	433	r = c->expr;
9280addf	434
616915dd	435	if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) )
	436	{
	437	int cmp;
	438	cmp = constraintExpr_compare (l, r);
	439	switch (c->ar)
	440	{
	441	case EQ:
	442	return (cmp == 0);
	443	case GT:
	444	return (cmp > 0);
	445	case GTE:
	446	return (cmp >= 0);
	447	case LTE:
	448	return (cmp <= 0);
	449	case LT:
	450	return (cmp < 0);
	451
	452	default:
9280addf	453	BADEXIT;
	454	break;
	455	}
	456	}
	457
	458	if (constraintExpr_similar (l,r) )
	459	{
	460	switch (c->ar)
	461	{
	462	case EQ:
	463	case GTE:
	464	case LTE:
	465	return TRUE;
	466
	467	case GT:
	468	case LT:
	469	break;
	470	default:
	471	BADEXIT;
616915dd	472	break;
	473	}
	474	}
9280addf	475
	476	l = constraintExpr_copy (c->lexpr);
	477	r = constraintExpr_copy (c->expr);
	478
	479	// l = constraintExpr_propagateConstants (l, &lHasConstant, &lConstant);
	480	r = constraintExpr_propagateConstants (r, &rHasConstant, &rConstant);
	481
	482	if (constraintExpr_similar (l,r) )
	483	{
	484	DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) ));
	485	if (rHasConstant)
	486	{
	487	DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is %d", rConstant ) ));
	488	switch (c->ar)
	489	{
	490	case EQ:
	491	return (rConstant == 0);
	492	case LT:
	493	return (rConstant > 0);
	494	case LTE:
	495	return (rConstant >= 0);
	496	case GTE:
	497	return (rConstant <= 0);
	498	case GT:
	499	return (rConstant < 0);
	500
	501	default:
	502	BADEXIT;
	503	break;
	504	}
	505	}
	506
	507	}
616915dd	508	else
616915dd	509	{
9280addf	510	DPRINTF(( message("Constraint %s is not always true", constraint_print(c) ) ));
616915dd	511	return FALSE;
616915dd	512	}
9280addf	513
9280addf	514	BADEXIT;
616915dd	515	}
	516
	517	bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)
	518
	519	{
	520	DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
	521
	522	if (! arithType_canResolve (ar1, ar2) )
	523	return FALSE;
	524
	525	switch (ar1)
	526	{
	527	case GTE:
	528	if (constraintExpr_similar (expr1, expr2) )
	529	return TRUE;
	530	case GT:
	531	if (! (constraintExpr_canGetValue (expr1) &&
	532	constraintExpr_canGetValue (expr2) ) )
	533	{
	534	DPRINTF( ("Can't Get value"));
	535	return FALSE;
	536	}
	537
	538	if (constraintExpr_compare (expr2, expr1) >= 0)
	539	return TRUE;
	540
	541	return FALSE;
	542	case EQ:
	543	if (constraintExpr_similar (expr1, expr2) )
	544	return TRUE;
	545
	546	return FALSE;
	547	case LTE:
	548	if (constraintExpr_similar (expr1, expr2) )
	549	return TRUE;
	550	case LT:
	551	if (! (constraintExpr_canGetValue (expr1) &&
	552	constraintExpr_canGetValue (expr2) ) )
	553	{
	554	DPRINTF( ("Can't Get value"));
	555	return FALSE;
	556	}
	557
	558	if (constraintExpr_compare (expr2, expr1) <= 0)
	559	return TRUE;
	560
	561	return FALSE;
	562
	563	default:
	564	llcontbug((message("Unhandled case in switch: %s", arithType_print(ar1) ) ) );
	565	}
	566	BADEXIT;
	567	return FALSE;
	568	}
	569
	570
	571	constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new)
	572	{
	573	DPRINTF (("Doing replace for lexpr") );
	574	c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
	575	DPRINTF (("Doing replace for expr") );
	576	c->expr = constraintExpr_searchandreplace (c->expr, old, new);
	577	return c;
	578	}
579
580	bool constraint_search (constraint c, constraintExpr old)
581	{
582	bool ret;
583	ret = FALSE;
584
585	ret = constraintExpr_search (c->lexpr, old);
586	ret = ret \|\| constraintExpr_search (c->expr, old);
587	return ret;
588	}
589
590	//adjust file locs and stuff
591	constraint constraint_adjust (constraint substitute, constraint old)
592	{
593	fileloc loc1, loc2, loc3;
594
595	DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
596	constraint_print(old))
597	));
598
599	loc1 = constraint_getFileloc (old);
600
601	loc2 = constraintExpr_getFileloc (substitute->lexpr);
602
603	loc3 = constraintExpr_getFileloc (substitute->expr);
604
605
606	// special case of an equality that "contains itself"
607	if (constraintExpr_search (substitute->expr, substitute->lexpr) )
608	if (fileloc_closer (loc1, loc3, loc2))
609	{
610	constraintExpr temp;
611	DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
612	));
613	temp = substitute->lexpr;
614	substitute->lexpr = substitute->expr;
615	substitute->expr = temp;
616	substitute = constraint_simplify(substitute);
617	}
618
619	return substitute;
620
621	}
622
623	constraint inequalitySubstitute (constraint c, constraintList p)
624	{
625	if (c->ar != GTE)
626	return c;
627
628	constraintList_elements (p, el)
629	{
630	if ( el->ar == LT)
631	// if (!constraint_conflict (c, el) )
632	{
633	constraint temp;
634	temp = constraint_copy(el);
635
636	// temp = constraint_adjust(temp, c);
637
638	if (constraintExpr_same (el->lexpr, c->expr) )
639	{
640	DPRINTF((message ("Replacing %s in %s with %s",
641	constraintExpr_print (c->expr),
642	constraint_print (c),
643	constraintExpr_print (el->expr) )
644	));
645	c->expr = constraintExpr_copy (el->expr);
646	}
647
648	}
649	}
650	end_constraintList_elements;
651
652	c = constraint_simplify(c);
653	return c;
654	}
655
656	constraint substitute (constraint c, constraintList p)
657	{
658	constraintList_elements (p, el)
659	{
660	if ( el->ar == EQ)
661	if (!constraint_conflict (c, el) )
662
663	{
664	constraint temp;
665	temp = constraint_copy(el);
666
667	temp = constraint_adjust(temp, c);
668
669	DPRINTF((message ("Substituting %s for %s",
670	constraint_print (temp), constraint_print (c)
671	) ) );
672
673
674	c = constraint_searchandreplace (c, temp->lexpr, temp->expr);
675	}
676	}
677	end_constraintList_elements;
678
679	c = constraint_simplify(c);
680	return c;
681	}
682
683
684	constraint constraint_solve (constraint c)
685	{
686	DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
687	c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
688	DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
689
690	return c;
691	}
692
693	static arithType flipAr (arithType ar)
694	{
695	switch (ar)
696	{
697	case LT:
698	return GT;
699	case LTE:
700	return GTE;
701	case EQ:
702	return EQ;
703	case GT:
704	return LT;
705	case GTE:
706	return LTE;
707	default:
708	llcontbug (("unexpected value: case not handled"));
709	}
710	BADEXIT;
711	}
712
713	static constraint constraint_swapLeftRight (constraint c)
714	{
715	constraintExpr temp;
716	c->ar = flipAr (c->ar);
717	temp = c->lexpr;
718	c->lexpr = c->expr;
719	c->expr = temp;
720	DPRINTF(("Swaped left and right sides of constraint"));
721	return c;
722	}
723
724	constraint constraint_simplify (constraint c)
725	{
726	c->lexpr = constraintExpr_simplify (c->lexpr);
727	c->expr = constraintExpr_simplify (c->expr);
728
729	c = constraint_solve (c);
730
731	c->lexpr = constraintExpr_simplify (c->lexpr);
732	c->expr = constraintExpr_simplify (c->expr);
733
734	if (constraintExpr_isLit(c->lexpr) && (!constraintExpr_isLit(c->expr) ) )
735	{
736	c = constraint_swapLeftRight(c);
737	/I don't think this will be an infinate loop/
738	constraint_simplify(c);
739	}
740	return c;
741	}
742
743
744
745
746	/* returns true if fileloc for term1 is closer to file for term2 than term3*/
747
748	bool fileloc_closer (fileloc loc1, fileloc loc2, fileloc loc3)
749	{
750	if ( fileloc_lessthan (loc1, loc2) )
751	{
752	if (fileloc_lessthan (loc2, loc3) )
753	{
754	llassert (fileloc_lessthan (loc1, loc3) );
755	return TRUE;
756	}
757	else
758	{
759	return FALSE;
760	}
761	}
762
763	if ( !fileloc_lessthan (loc1, loc2) )
764	{
765	if (!fileloc_lessthan (loc2, loc3) )
766	{
767	llassert (!fileloc_lessthan (loc1, loc3) );
768	return TRUE;
769	}
770	else
771	{
772	return FALSE;
773	}
774	}
775
776	llassert(FALSE);
777	return FALSE;
778	}
779
780