X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/92c4a78635fd7baf52eb7ede90b735be84089dd7..22b8afc959f05820d93be5f55d2251e42ebc3bd8:/src/constraint.c

diff --git a/src/constraint.c b/src/constraint.c
index 133f99f..2187b0d 100644
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -2,6 +2,8 @@
 ** constraintList.c
 */
 
+//#define DEBUGPRINT 1
+
 # include <ctype.h> /* for isdigit */
 # include "lclintMacros.nf"
 # include "basic.h"
@@ -11,16 +13,117 @@
 # include "exprChecks.h"
 # include "aliasChecks.h"
 # include "exprNodeSList.h"
-# include "exprData.i"
+//# include "exprData.i"
 
 /*@i33*/
 /*@-fcnuse*/
 /*@-assignexpose*/
 
-/*@notnull@*/ 
-/*@special@*/ constraint constraint_makeNew (void)
-     /*@post:isnull result->term, result->expr, result->constrType@*/
-     /*@defines result->ar, result->post@*/;
+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("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);
+  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("Unsupported relational operator");
+
+
+  t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
+  c = atoi( t );
+  ret->expr = constraintExpr_makeIntLiteral (c);
+
+  ret->post = TRUE;
+  //  ret->orig = ret;
+  DPRINTF(("GENERATED CONSTRAINT:"));
+  DPRINTF( (message ("%s", constraint_print(ret) ) ) );
+  return ret;
+}
+
+
+constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)     
+{
+  constraint ret;
+  ret = constraint_makeNew();
+  llassert (l);
+  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("Unsupported relational operator");
+
+  ret->expr = constraintExpr_copy (r);
+
+  ret->post = TRUE;
+  //  ret->orig = ret;
+  DPRINTF(("GENERATED CONSTRAINT:"));
+  DPRINTF( (message ("%s", constraint_print(ret) ) ) );
+  return ret;
+}
 
 constraint constraint_copy (constraint c)
 {
@@ -30,6 +133,8 @@ constraint constraint_copy (constraint c)
   ret->ar = c->ar;
   ret->expr =  constraintExpr_copy (c->expr);
   ret->post = c->post;
+  ret->generatingExpr = c->generatingExpr;
+  
   /*@i33 fix this*/
   if (c->orig != NULL)
     ret->orig = constraint_copy (c->orig);
@@ -51,7 +156,7 @@ void constraint_overWrite (constraint c1, constraint c2)
     c1->orig = constraint_copy (c2->orig);
   else
     c1->orig = NULL;
-
+  c1->generatingExpr = c2->generatingExpr;
 }
 
 bool constraint_resolve (/*@unused@*/ constraint c)
@@ -59,10 +164,9 @@ bool constraint_resolve (/*@unused@*/ constraint c)
   return FALSE;
 }
 
-/*@notnull@*/ 
-/*@special@*/ constraint constraint_makeNew (void)
-     /*@post:isnull result->term, result->expr, result->constrType@*/
-     /*@defines result->ar, result->post@*/
+
+
+constraint constraint_makeNew (void)
 {
   constraint ret;
   ret = dmalloc(sizeof (*ret) );
@@ -71,16 +175,54 @@ bool constraint_resolve (/*@unused@*/ constraint c)
   ret->ar = LT;
   ret->post = FALSE;
   ret->orig = NULL;
+  ret->generatingExpr = NULL;
   /*@i23*/return ret;
 }
 
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+{
+    
+  if (c->generatingExpr == NULL)
+    {
+      c->generatingExpr = 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)
+    {
+      if (checkForMaxSet(c->orig) )
+	return TRUE;
+    }
+
+  return (checkForMaxSet(c) );
+}
+
 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 {
   constraint ret = constraint_makeNew();
@@ -103,7 +245,44 @@ constraint constraint_makeWriteSafeInt (exprNode po, int ind)
   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();
@@ -114,7 +293,8 @@ constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
   ret->expr =  constraintExpr_makeValueExpr (ind);
   /*@i1*/return ret;
 }
-			       
+
+
 constraint constraint_makeReadSafeInt ( exprNode po, int ind)
 {
   constraint ret = constraint_makeNew();
@@ -146,6 +326,85 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, filelo
 }
 
 
+static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
+{
+  constraint ret = constraint_makeNew();
+  exprNode e;
+  
+  e = exprNode_fakeCopy(e1);
+  if (! (e1 && e2) )
+    {
+      llcontbug((message("null exprNode, Exprnodes are %s and %s",
+		       exprNode_unparse(e1), exprNode_unparse(e2) )
+	       ));
+    }
+		       
+  ret->lexpr = constraintExpr_makeValueExpr (e);
+  ret->ar = ar;
+  ret->post = TRUE;
+  e = exprNode_fakeCopy(e2);
+  ret->expr =  constraintExpr_makeValueExpr (e);
+  
+  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+  return ret;
+}
+
+
+/* make constraint ensures e1 == e2 */
+
+constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
+}
+
+/*make constraint ensures e1 < e2 */
+constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
+}
+
+constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
+}
+
+constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
+}
+
+constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
+{
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
+}
+
+
+exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
+{
+  dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
+  dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
+  dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
+  dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
+  return dst;
+}
+
+constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
+{
+  constraint ret = constraint_makeNew();
+  //constraintTerm term;
+
+  e = exprNode_fakeCopy(e);
+  ret->lexpr = constraintExpr_makeValueExpr (e);
+  ret->ar = EQ;
+  ret->post = TRUE;
+  ret->expr =  constraintExpr_makeValueExpr (e);
+  ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
+
+  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+//   fileloc_incColumn (  ret->lexpr->term->loc);
+//   fileloc_incColumn (  ret->lexpr->term->loc);
+  return ret;
+}
 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 {
   constraint ret = constraint_makeNew();
@@ -158,12 +417,14 @@ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc seq
   ret->expr =  constraintExpr_makeValueExpr (e);
   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 
-  ret->expr = constraintExpr_setFileloc (ret->expr, sequencePoint);
+  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();
@@ -212,24 +473,70 @@ cstring arithType_print (arithType ar)
   return st;
 }
 
+void constraint_printError (constraint c, fileloc loc)
+{
+  cstring string;
+  fileloc errorLoc;
+  
+  string = constraint_printDetailed (c);
+
+  errorLoc = loc;
+
+  if (constraint_getFileloc(c) )
+    errorLoc = constraint_getFileloc(c);
+  
+  
+  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)  
+      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));
       
-    st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(c->orig) );
     }
   else
     {
-    st = message ("Function Post condition:\nThis function appears to have the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
+      if (c->orig)
+	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  constraint_print (constraint c) /*@*/
 {
   cstring st = cstring_undefined;
   cstring type = cstring_undefined;
@@ -251,6 +558,38 @@ cstring  constraint_print (constraint c)
   return st;
 }
 
+constraint constraint_doSRefFixBaseParam (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) ) ) );