From 5513d3c2396b260d2763d17cf76fd8ae3fbf7e8a Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Thu, 21 May 2020 17:35:34 -0400
Subject: [PATCH 174/193] FIXME: WIP on symbolic bindings

---
 gcc/analyzer/store2.cc                     | 38 +++++++---------------
 gcc/analyzer/store2.h                      | 28 +++-------------
 gcc/testsuite/gcc.dg/analyzer/symbolic-1.c | 12 +++++++
 gcc/testsuite/gcc.dg/analyzer/symbolic-2.c | 32 ++++++++++++++++++
 gcc/testsuite/gcc.dg/analyzer/symbolic-3.c | 12 +++++++
 gcc/testsuite/gcc.dg/analyzer/symbolic-4.c |  9 +++++
 6 files changed, 82 insertions(+), 49 deletions(-)
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/symbolic-1.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/symbolic-2.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/symbolic-3.c
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/symbolic-4.c

diff --git a/gcc/analyzer/store2.cc b/gcc/analyzer/store2.cc
index 51809a6c96e..de60129018a 100644
--- a/gcc/analyzer/store2.cc
+++ b/gcc/analyzer/store2.cc
@@ -81,22 +81,16 @@ binding_key2::make (store2_manager *mgr, const region2 *r,
 {
   region_offset offset = r->get_offset ();
   if (offset.symbolic_p ())
-#if 0
-    gcc_unreachable ();
-#else
-    return mgr->get_symbolic_binding (offset.get_base_region (), kind,
-				      offset.get_base_region ()); // FIXME
-#endif
-    else
-      {
-	bit_size_t bit_size;
-	if (r->get_bit_size (&bit_size))
-	  return mgr->get_concrete_binding (offset.get_bit_offset (),
-					    bit_size, kind);
-	else
-	  return mgr->get_symbolic_binding (offset.get_base_region (), kind,
-					    offset.get_base_region ()); // FIXME
-      }
+    return mgr->get_symbolic_binding (r, kind);
+  else
+    {
+      bit_size_t bit_size;
+      if (r->get_bit_size (&bit_size))
+	return mgr->get_concrete_binding (offset.get_bit_offset (),
+					  bit_size, kind);
+      else
+	return mgr->get_symbolic_binding (r, kind); // FIXME
+    }
 }
 
 /* FIXME.  */
@@ -197,7 +191,6 @@ concrete_binding2::overlaps_p (const concrete_binding2 &other) const
   return false;
 }
 
-#if 1
 /* class symbolic_binding2 : public binding_key2.  */
 
 void
@@ -206,10 +199,7 @@ symbolic_binding2::dump_to_pp (pretty_printer *pp, bool simple) const
   binding_key2::dump_to_pp (pp, simple);
   pp_string (pp, ", region: ");
   m_region->dump_to_pp (pp, simple);
-  pp_string (pp, ", concrete offset region: ");
-  m_concrete_offset_region->dump_to_pp (pp, simple);
 }
-#endif
 
 #endif
 
@@ -736,17 +726,13 @@ store2_manager::get_concrete_binding (bit_offset_t start_bit_offset,
   return m_concrete_binding_key_mgr.consolidate (b);
 }
 
-#if 1
 const symbolic_binding2 *
 store2_manager::get_symbolic_binding (const region2 *reg,
-				      enum binding_kind kind,
-				      const region2 *concrete_offset_region)
+				      enum binding_kind kind)
 {
-  symbolic_binding2 *b
-    = new symbolic_binding2 (reg, kind, concrete_offset_region);
+  symbolic_binding2 *b = new symbolic_binding2 (reg, kind);
   return m_symbolic_binding_key_mgr.consolidate (b);
 }
-#endif
 
 /* class store2.  */
 
diff --git a/gcc/analyzer/store2.h b/gcc/analyzer/store2.h
index c41629160a0..35c043c4250 100644
--- a/gcc/analyzer/store2.h
+++ b/gcc/analyzer/store2.h
@@ -141,40 +141,32 @@ private:
   bit_size_t m_size_in_bits;
 };
 
-#if 1
 class symbolic_binding2 : public binding_key2
 {
 public:
-  symbolic_binding2 (const region2 *region, enum binding_kind kind,
-		     const region2 *concrete_offset_region)
+  symbolic_binding2 (const region2 *region, enum binding_kind kind)
   : binding_key2 (kind),
-    m_region (region),
-    m_concrete_offset_region (concrete_offset_region)
+    m_region (region)
   {}
   bool concrete_p () const FINAL OVERRIDE { return false; }
 
   hashval_t hash () const
   {
     return (binding_key2::impl_hash ()
-	    ^ (long)m_region
-	    ^ (long)m_concrete_offset_region);
+	    ^ (long)m_region);
   }
   bool operator== (const symbolic_binding2 &other)
   {
     if (!binding_key2::impl_eq (other))
       return false;
-    return (m_region == other.m_region
-	    && m_concrete_offset_region == other.m_concrete_offset_region);
+    return (m_region == other.m_region);
   }
 
   void dump_to_pp (pretty_printer *pp, bool simple) const FINAL OVERRIDE;
 
 private:
-  // TODO
   const region2 *m_region;
-  const region2 *m_concrete_offset_region;
 };
-#endif
 
 /* All of the bindings within a store for regions that share the same
    base region.  */
@@ -344,24 +336,14 @@ class store2_manager
 public:
   store2_manager (region_model2_manager *mgr) : m_mgr (mgr) {}
 
-#if 0
-  const concrete_binding2 *
-  get_binding_range (const region2 *region,
-#else
   /* binding consolidation.  */
   const concrete_binding2 *
   get_concrete_binding (bit_offset_t start_bit_offset,
 			bit_offset_t size_in_bits,
 			enum binding_kind kind);
-
-  // TODO:
-#if 1
   const symbolic_binding2 *
   get_symbolic_binding (const region2 *region,
-			enum binding_kind kind,
-			const region2 *concrete_offset_region);
-#endif
-#endif
+			enum binding_kind kind);
 
   region_model2_manager *get_svalue2_manager () const
   {
diff --git a/gcc/testsuite/gcc.dg/analyzer/symbolic-1.c b/gcc/testsuite/gcc.dg/analyzer/symbolic-1.c
new file mode 100644
index 00000000000..1e9af88fd5d
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/symbolic-1.c
@@ -0,0 +1,12 @@
+#include "analyzer-decls.h"
+
+void test_1 (int i, int j)
+{
+  char arr[1024];
+  arr[0] = 42;
+  arr[1] = 17;
+  __analyzer_eval (arr[0] == 42); /* { dg-warning "TRUE" } */
+  __analyzer_eval (arr[1] == 17); /* { dg-warning "TRUE" } */
+  // TODO: add symbolic binding:
+  // arr[i] = j;  
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/symbolic-2.c b/gcc/testsuite/gcc.dg/analyzer/symbolic-2.c
new file mode 100644
index 00000000000..70c00ce3867
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/symbolic-2.c
@@ -0,0 +1,32 @@
+#include "analyzer-decls.h"
+
+struct foo
+{
+  int ival;
+  int iarr[10];
+};
+
+void test_1 (int i, int j)
+{
+  struct foo fooarr[4];
+  fooarr[1].ival = 42;
+  fooarr[1].iarr[3] = 27;
+  fooarr[2].iarr[1] = 17;
+  __analyzer_eval (fooarr[1].ival == 42); /* { dg-warning "TRUE" } */
+  __analyzer_eval (fooarr[1].iarr[3] == 27); /* { dg-warning "TRUE" } */
+  __analyzer_eval (fooarr[2].iarr[1] == 17); /* { dg-warning "TRUE" } */
+
+  /* Symbolic binding.  */
+  fooarr[2].iarr[i] = j;
+  __analyzer_eval (fooarr[2].iarr[i] == j); /* { dg-warning "TRUE" } */
+
+  /* We should have lost our knowledge about fooarr[2].
+     It's not clear to me if we should also lose our knowledge about
+     fooarr[1] (for the case where i is negative).  For now, we do.  */
+  __analyzer_eval (fooarr[1].ival == 42); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (fooarr[1].iarr[3] == 27); /* { dg-warning "UNKNOWN" } */
+  __analyzer_eval (fooarr[2].iarr[1] == 17); /* { dg-warning "UNKNOWN" } */
+  /* Should also be safe to read from fooarr[2];
+     it isn't known to be uninit anymore.  */
+  __analyzer_eval (fooarr[2].iarr[10] == 17); /* { dg-warning "UNKNOWN" } */
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/symbolic-3.c b/gcc/testsuite/gcc.dg/analyzer/symbolic-3.c
new file mode 100644
index 00000000000..da4cdbbc54c
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/symbolic-3.c
@@ -0,0 +1,12 @@
+#include "analyzer-decls.h"
+
+int iarr[16];
+
+void test_1 (int i, int j)
+{
+  int init_el_8 = iarr[8];
+  __analyzer_eval (init_el_8 == iarr[8]); /* { dg-warning "TRUE" } */
+
+  iarr[i] = j;
+  __analyzer_eval (init_el_8 == iarr[8]); /* { dg-warning "UNKNOWN" } */
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/symbolic-4.c b/gcc/testsuite/gcc.dg/analyzer/symbolic-4.c
new file mode 100644
index 00000000000..1c313343b56
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/symbolic-4.c
@@ -0,0 +1,9 @@
+#include "analyzer-decls.h"
+
+void test_1 (int i, int j, int k)
+{
+  int iarr[16];
+  iarr[i] = j;
+  __analyzer_eval (iarr[i] == j); /* { dg-warning "TRUE" } */
+  __analyzer_eval (iarr[k] == j); /* { dg-warning "UNKNOWN" } */
+}
-- 
2.21.0

