Prewinter break editing commit.

[splint.git] / src / constraintResolve.c

diff --git a/src/constraintResolve.c b/src/constraintResolve.c
index 3749dad0e48bc7f4db8e0478aa15ea298b20359a..223cf7de3384e36b9d1d212ccd757653d26791b0 100644 (file)
--- a/src/constraintResolve.c
+++ b/src/constraintResolve.c
@@ -3,6 +3,8 @@
 ** constraintResolve.c
 */
 
+//#define DEBUGPRINT 1
+
 # include <ctype.h> /* for isdigit */
 # include "lclintMacros.nf"
 # include "basic.h"
@@ -12,10 +14,12 @@
 # include "exprChecks.h"
 # include "aliasChecks.h"
 # include "exprNodeSList.h"
-# include "exprData.i"
+//# 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);
@@ -30,7 +34,7 @@ constraintList constraintList_fixConflicts (constraintList list1, constraintList
 constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
 
 constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
-
+constraint  inequalitySubstitute  (constraint c, constraintList p);
 
 /*********************************************/
 
@@ -53,13 +57,57 @@ constraintList constraintList_mergeEnsures (constraintList list1, constraintList
   //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; */
+/* } */
+
+
+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_doSRefFixBaseParam (preconditions, arglist);
+    }
+  else
+    {
+      preconditions = constraintList_new();
+    }
+  
+  return preconditions;
+}
+
 void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 {
   constraintList temp;
 
-  TPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));
+  DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));
 
-  TPRINTF( (message (" children:  %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );
+  DPRINTF( (message (" children:  %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );
 
   if (exprNode_isError (child1)  || exprNode_isError(child2) )
      {
@@ -67,7 +115,7 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
         {
           parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
           parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
-          TPRINTF((message ("Copied child constraints: pre: %s and post: %s",
+          DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
                             constraintList_print( child2->requiresConstraints),
                             constraintList_print (child2->ensuresConstraints)
                             )
@@ -85,7 +133,7 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 
    llassert(!exprNode_isError (child1)  && ! exprNode_isError(child2) );
    
-  TPRINTF( (message ("Child constraints are %s %s and %s %s",
+  DPRINTF( (message ("Child constraints are %s %s and %s %s",
                     constraintList_print (child1->requiresConstraints),
                     constraintList_print (child1->ensuresConstraints),
                     constraintList_print (child2->requiresConstraints),
@@ -103,7 +151,7 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
   parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
                                                           child2->ensuresConstraints);
   
-  TPRINTF( (message ("Parent constraints are %s and %s ",
+  DPRINTF( (message ("Parent constraints are %s and %s ",
                     constraintList_print (parent->requiresConstraints),
                     constraintList_print (parent->ensuresConstraints)
                     ) ) );
@@ -120,14 +168,14 @@ constraintList constraintList_subsumeEnsures (constraintList list1, constraintLi
   constraintList_elements (list1, el)
     {
       
-      TPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
+      DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
       if (!resolve (el, list2) )
        {
            ret = constraintList_add (ret, el);
        }
       else
        {
-         TPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
+         DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
        }
     } end_constraintList_elements;
 
@@ -147,7 +195,17 @@ constraintList reflectChanges (constraintList pre2, constraintList post1)
        {
          temp = substitute (el, post1);
          if (!resolve (temp, post1) )
-           ret = constraintList_add (ret, temp);
+           {
+             // 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;
 
@@ -173,7 +231,7 @@ constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
        }
       else
        {
-         TPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
+         DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
        }
     } end_constraintList_elements;
 
@@ -189,7 +247,7 @@ bool constraint_conflict (constraint c1, constraint c2)
       if (c1->ar == EQ)
        if (c1->ar == c2->ar)
          {
-           TPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
+           DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
            return TRUE;
          }
     }  
@@ -255,7 +313,7 @@ bool resolve (constraint c, constraintList p)
     {
       if ( satifies (c, el) )
        {
-         TPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
+         DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
          return TRUE;
        }
     }
@@ -300,7 +358,7 @@ bool arithType_canResolve (arithType ar1, arithType ar2)
 
     case LT:
     case LTE:
-      llassert(FALSE); 
+      //      llassert(FALSE); 
       if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
        return TRUE;
     }
@@ -362,7 +420,7 @@ bool constraint_search (constraint c, constraintExpr old)
   return ret;
 }
 
-
+//adjust file locs and stuff
 constraint constraint_adjust (constraint substitute, constraint old)
 {
   fileloc loc1, loc2, loc3;
@@ -395,6 +453,39 @@ constraint constraint_adjust (constraint substitute, constraint old)
   
 }
 
+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)