Merge pull request #5362 from thk123/assume-relation

Assume relation between two symbols

Author: Thomas Kiley

regression/goto-analyzer/intervals_simple-loops/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+const int g_N = 2;
+
+void main(void)
+{
+  for(int i = 0; i < g_N; i++)
+  {
+    assert(0);
+  }
+
+  for(int j = 4; j >= g_N; j--)
+  {
+    assert(0);
+  }
+}

regression/goto-analyzer/intervals_simple-loops/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line 8 assertion 0: UNKNOWN
+\[main\.assertion\.2\] line 13 assertion 0: UNKNOWN
+--
+--
+Test comparision between two symbols does not mark the
+result as bottom

src/analyses/interval_domain.cpp

@@ -329,10 +329,10 @@ void interval_domaint::assume_rec(
     {
       integer_intervalt &lhs_i=int_map[lhs_identifier];
       integer_intervalt &rhs_i=int_map[rhs_identifier];
-      lhs_i.meet(rhs_i);
-      rhs_i=lhs_i;
-      if(rhs_i.is_bottom())
-        make_bottom();
+      if(id == ID_lt && !lhs_i.is_less_than(rhs_i))
+        lhs_i.make_less_than(rhs_i);
+      if(id == ID_le && !lhs_i.is_less_than_eq(rhs_i))
+        lhs_i.make_less_than_eq(rhs_i);
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {

src/util/interval_template.h

@@ -143,6 +143,47 @@ template<class T> class interval_templatet
     }
   }
 
+  void make_bottom()
+  {
+    lower_set = upper_set = true;
+    upper = T();
+    lower = upper + 1;
+  }
+
+  void make_less_than_eq(interval_templatet &i)
+  {
+    if(upper_set && i.upper_set)
+      upper = std::min(upper, i.upper);
+    if(lower_set && i.lower_set)
+      i.lower = std::max(lower, i.lower);
+  }
+
+  void make_less_than(interval_templatet &i)
+  {
+    make_less_than_eq(i);
+    if(singleton() && i.singleton() && lower == i.lower)
+    {
+      make_bottom();
+      i.make_bottom();
+    }
+  }
+
+  bool is_less_than_eq(const interval_templatet &i)
+  {
+    if(i.lower_set && upper_set && upper <= i.lower)
+      return true;
+    else
+      return false;
+  }
+
+  bool is_less_than(const interval_templatet &i)
+  {
+    if(i.lower_set && upper_set && upper < i.lower)
+      return true;
+    else
+      return false;
+  }
+
   void approx_union_with(const interval_templatet &i)
   {
     if(i.lower_set && lower_set)