X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/990ec8680b4718e26f8774a8f2ccff44fb97b3c5..acfb6ad9a989e335242f8ea98940827e213228b4:/src/constraint.c

diff --git a/src/constraint.c b/src/constraint.c
index 4bbf293..a17c1e5 100644
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -2,13 +2,14 @@
 ** constraint.c
 */
 
-//#define DEBUGPRINT 1
+/* #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 "exprNodeSList.h"
 
@@ -20,60 +21,23 @@
 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
 
 
-static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
-     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
-     
-/*  constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
+static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
+     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/
+     /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
      
-/*  { */
-/*    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; */
-/*  } */
-
-
 static void
 advanceField (char **s)
 {
   reader_checkChar (s, '@');
 }
 
-
-
+# if 0
 static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)    
 {
   char *t;
   int c;
   constraint ret;
-  ret = constraint_makeNew();
+  ret = constraint_makeNew ();
   llassert (constraintExpr_isDefined(l) );
       
   ret->lexpr = constraintExpr_copy (l);
@@ -94,23 +58,31 @@ static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode
   ret->expr = constraintExpr_makeIntLiteral (c);
 
   ret->post = TRUE;
-  //  ret->orig = ret;
   DPRINTF(("GENERATED CONSTRAINT:"));
   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
   return ret;
 }
+# endif
 
 bool constraint_same (constraint c1, constraint c2)
 {
-  
-  if (c1->ar != c2->ar)
-    return FALSE;
+  llassert (c1 != NULL);
+  llassert (c2 != NULL);
 
+  if (c1->ar != c2->ar)
+    {
+      return FALSE;
+    }
+  
   if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
-    return FALSE;
+    {
+      return FALSE;
+    }
 
   if (!constraintExpr_similar (c1->expr, c2->expr) )
-    return FALSE;
+    {
+      return FALSE;
+    }
 
   return TRUE;
 }
@@ -139,8 +111,8 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r
   ret->orig = constraint_copy(ret);
 
   ret = constraint_simplify (ret);
-  
-  //  ret->orig = ret;
+  /* ret->orig = ret; */
+
   DPRINTF(("GENERATED CONSTRAINT:"));
   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
   return ret;
@@ -151,8 +123,7 @@ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
   constraint ret;
 
   llassert (constraint_isDefined(c) );
-  // DPRINTF((message("Copying constraint %q", constraint_print) ));
-  
+
   ret = constraint_makeNew();
   ret->lexpr = constraintExpr_copy (c->lexpr);
   ret->ar = c->ar;
@@ -224,7 +195,8 @@ void constraint_overWrite (constraint c1, constraint c2)
 
 
 static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
-     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
+     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ 
+     /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
 {
   constraint ret;
   ret = dmalloc(sizeof (*ret) );
@@ -239,7 +211,7 @@ static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
   return ret;
 }
 
-constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
 {
     
   if (c->generatingExpr == NULL)
@@ -278,7 +250,7 @@ constraint constraint_setFcnPre (/*@returned@*/ constraint c )
   else
     {
       c->fcnPre = TRUE;
-      //      DPRINTF(( message("Warning Setting fcnPre directly") ));
+      DPRINTF(( message("Warning Setting fcnPre directly") ));
     }
   return c;
 }
@@ -306,19 +278,22 @@ static bool checkForMaxSet (constraint c)
 
 bool constraint_hasMaxSet(constraint c)
 {
+  if (checkForMaxSet(c) )
+    return TRUE;
+  
   if (c->orig != NULL)
     {
       if (checkForMaxSet(c->orig) )
 	return TRUE;
     }
 
-  return (checkForMaxSet(c) );
+  return FALSE;
 }
 
 constraint constraint_makeReadSafeExprNode (  exprNode po, exprNode ind)
 {
   constraint ret = constraint_makeNew();
-  //  constraintTerm term;
+
   po = po;
   ind = ind;
   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
@@ -416,12 +391,9 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, filelo
   constraint ret;
   
   ret = constraint_makeReadSafeExprNode(t1, t2);
-
-  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
-  
+  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);  
   ret->post = TRUE;  
 
-  //  fileloc_incColumn (ret->lexpr->term->loc);
   return ret;
 }
 
@@ -431,7 +403,6 @@ static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintE
   constraint ret;
   
   llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) );
-  //  llassert(sequencePoint);
 
   ret = constraint_makeNew();
   
@@ -453,11 +424,9 @@ static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@depe
     {
       llcontbug((message("null exprNode, Exprnodes are %s and %s",
 		       exprNode_unparse(e1), exprNode_unparse(e2) )
-	       ));
+		 ));
     }
 
-  //  llassert (sequencePoint);
-  
   e  =  e1;
   c1 =  constraintExpr_makeValueExpr (e);
   
@@ -580,26 +549,19 @@ constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequen
 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;
@@ -607,8 +569,6 @@ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc seq
   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;
 }
 
@@ -636,47 +596,31 @@ void constraint_free (/*@only@*/ constraint c)
   
 }
 
-
-// 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 (" < ");
+      st = cstring_makeLiteral ("<");
       break;
     case	LTE:
-      st = cstring_makeLiteral (" <= ");
+      st = cstring_makeLiteral ("<=");
       break;
     case 	GT:
-      st = cstring_makeLiteral (" > ");
+      st = cstring_makeLiteral (">");
       break;
     case 	GTE:
-      st = cstring_makeLiteral (" >= ");
+      st = cstring_makeLiteral (">=");
       break;
     case	EQ:
-      st = cstring_makeLiteral (" == ");
+      st = cstring_makeLiteral ("==");
       break;
     case	NONNEGATIVE:
-      st = cstring_makeLiteral (" NONNEGATIVE ");
+      st = cstring_makeLiteral ("NONNEGATIVE");
       break;
     case	POSITIVE:
-      st = cstring_makeLiteral (" POSITIVE ");
+      st = cstring_makeLiteral ("POSITIVE");
       break;
     default:
       llassert(FALSE);
@@ -710,6 +654,22 @@ void constraint_printErrorPostCondition (constraint c, fileloc loc)
     }
 }
 
+ /*drl added 8-11-001*/
+cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
+{
+  cstring string, ret;
+  fileloc errorLoc;
+  
+  string = constraint_print(c);
+
+  errorLoc = constraint_getFileloc(c);
+
+  ret = message ("constraint: %q @ %q", string, fileloc_unparse(errorLoc) );
+
+  fileloc_free(errorLoc);
+  return ret;
+
+}
 
 
 
@@ -722,37 +682,34 @@ void constraint_printError (constraint c, fileloc loc)
 
   errorLoc = loc;
 
-  loc = NULL;
-
   temp = constraint_getFileloc(c);
 
   if (fileloc_isDefined(temp) )
     {
       errorLoc = temp;
-      
-      if (c->post)
-	{
-	  voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
-	}
-      else
-	{
-	  voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
-	}
+    }
+  else
+    {
+      llassert(FALSE);
+      DPRINTF (("constraint %s had undefined fileloc %s", constraint_print(c), fileloc_unparse(temp)));
       fileloc_free(temp);
-      errorLoc = NULL;
+      errorLoc = fileloc_copy(errorLoc);
+    }
+      
+  if (c->post)
+    {
+      voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
     }
   else
     {
-      if (c->post)
-	{
-	  voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
-	}
+      if (constraint_hasMaxSet (c) )
+	voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
       else
-	{
-	  voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
-	}
-      errorLoc = NULL;
+	voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
     }
+
+  fileloc_free(errorLoc);
+
 }
 
 
@@ -766,6 +723,7 @@ static cstring constraint_printDeep (constraint c)
   
   if (c->orig != constraint_undefined)
     {
+      st = cstring_appendChar(st, '\n');
       genExpr =  exprNode_unparse(c->orig->generatingExpr);
       if (!c->post)
 	{
@@ -773,7 +731,7 @@ static cstring constraint_printDeep (constraint c)
 	    st = cstring_concatFree(st, (message(" derived from %s precondition: %q", genExpr, constraint_printDeep(c->orig) )
 					 ) );
 	  else
-	    st = cstring_concatFree(st,(message(" needed to satisfy %q",
+	    st = cstring_concatFree(st,(message(" needed to satisfy precondition:\n%q",
 						constraint_printDeep(c->orig) )
 					) );
 	  
@@ -803,8 +761,9 @@ static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/
   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
     {
       cstring temp;
-      // llassert (c->generatingExpr);
-      temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
+
+      temp = message ("\nOriginal Generating expression %q: %s\n", 
+		      fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 		      genExpr );
       st = cstring_concatFree (st, temp);
 
@@ -820,33 +779,38 @@ static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/
 cstring  constraint_printDetailed (constraint c)
 {
   cstring st = cstring_undefined;
-  cstring genExpr;
+  cstring temp = cstring_undefined;
+    cstring genExpr;
   
   if (!c->post)
     {
-      st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
+      st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c) );
     }
   else
     {
       st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
     }
 
+  if (constraint_hasMaxSet(c) )
+    {
+      temp = cstring_makeLiteral("Possible out-of-bounds store:\n");
+    }
+  else
+    {
+      temp = cstring_makeLiteral("Possible out-of-bounds read:\n");
+    }
+  
   genExpr = exprNode_unparse (c->generatingExpr);
-
+  
   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
     {
-      cstring temp;
-      // llassert (c->generatingExpr);
-      temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
-		      genExpr );
-      st = cstring_concatFree (st, temp);
-
-      if (constraint_hasMaxSet(c) )
-	{
-	  temp = message ("Has MaxSet\n");
-	  st = cstring_concatFree (st, temp);
-	}
+      cstring temp2;
+      temp2 = message ("%s\n", genExpr );
+      temp = cstring_concatFree (temp, temp2);
     }
+
+  st  = cstring_concatFree(temp,st);
+  
   return st;
 }
 
@@ -857,18 +821,45 @@ cstring  constraint_printDetailed (constraint c)
   llassert (c !=NULL);
   if (c->post)
     {
-      type = cstring_makeLiteral ("Ensures: ");
+      if (context_getFlag (FLG_PARENCONSTRAINT) )
+	{
+	  type = cstring_makeLiteral ("ensures: ");
+	}
+      else
+	{
+	   type = cstring_makeLiteral ("ensures");
+	}
     }
   else
     {
-      type = cstring_makeLiteral ("Requires: ");
+      if (context_getFlag (FLG_PARENCONSTRAINT) )
+	{
+	  type = cstring_makeLiteral ("requires: ");
+	}
+      else
+	{
+	  type = cstring_makeLiteral ("requires");
+	}
+	
     }
-  st = message ("%q: %q %q %q",
-		type,
-		constraintExpr_print (c->lexpr),
-		arithType_print(c->ar),
-		constraintExpr_print(c->expr)
+      if (context_getFlag (FLG_PARENCONSTRAINT) )
+	{
+	  st = message ("%q: %q %q %q",
+			type,
+			constraintExpr_print (c->lexpr),
+			arithType_print(c->ar),
+			constraintExpr_print(c->expr)
+			);
+	}
+      else
+	{
+	  st = message ("%q %q %q %q",
+			type,
+			constraintExpr_print (c->lexpr),
+			arithType_print(c->ar),
+			constraintExpr_print(c->expr)
 		);
+	}
   return st;
 }
 
@@ -928,19 +919,6 @@ constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exp
   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;
-// }
-
 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
 {
 
@@ -1057,6 +1035,7 @@ constraint constraint_undump (FILE *f)
   c->expr =  expr;
 
   free(os);
+  c = constraint_preserveOrig(c);
   return c;
 }
 
@@ -1085,3 +1064,82 @@ void constraint_dump (/*@observer@*/ constraint c,  FILE *f)
 }
 
 
+int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
+{
+  fileloc loc1, loc2;
+
+  int ret;
+  
+  llassert(constraint_isDefined(*c1) );
+  llassert(constraint_isDefined(*c2) );
+
+  if (constraint_isUndefined(*c1) )
+    {
+        if (constraint_isUndefined(*c2) )
+	  return 0;
+	else
+	  return 1;
+    }
+
+  if (constraint_isUndefined(*c2) )
+    {
+      return -1;
+    }
+    
+  loc1 = constraint_getFileloc(*c1);
+  loc2 = constraint_getFileloc(*c2);
+
+  ret = fileloc_compare(loc1, loc2);
+
+  fileloc_free(loc1);
+  fileloc_free(loc2);
+    
+  return ret;
+}
+
+
+bool constraint_isPost  (/*@observer@*/ /*@temp@*/ constraint c)
+{
+  llassert(constraint_isDefined(c) );
+
+  if (constraint_isUndefined(c) )
+    return FALSE;
+  
+  return (c->post);
+}
+
+
+static int constraint_getDepth(/*@observer@*/ /*@temp@*/ constraint c)
+{
+  int l , r;
+
+  l = constraintExpr_getDepth(c->lexpr);
+  r = constraintExpr_getDepth(c->expr);
+
+  if (l > r)
+    {
+      DPRINTF(( message("constraint depth returning %d for %s", l, constraint_print(c) ) ));
+      return l;
+    }
+  else
+    {
+      DPRINTF(( message("constraint depth returning %d for %s", r, constraint_print(c) ) ));
+      return r;
+    }
+}
+
+
+bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
+{
+  int temp;
+
+  temp = constraint_getDepth(c);
+
+  if (temp >= 20 )
+    {
+      return TRUE;
+    }
+
+  return FALSE;
+  
+}