From eb339de72a530275bb9d427fa6d09234c87b4c02 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Thu, 11 Jun 2020 08:19:24 -0400
Subject: [PATCH 226/251] FIXME: WIP on widening

---
 gcc/analyzer/constraint-manager2.cc |  22 +++++-
 gcc/analyzer/region-model2.cc       | 117 +++++++++++++++++++++++++++-
 gcc/analyzer/region-model2.h        |   4 +
 3 files changed, 137 insertions(+), 6 deletions(-)

diff --git a/gcc/analyzer/constraint-manager2.cc b/gcc/analyzer/constraint-manager2.cc
index a8779f35e71..d6708c191ba 100644
--- a/gcc/analyzer/constraint-manager2.cc
+++ b/gcc/analyzer/constraint-manager2.cc
@@ -919,7 +919,8 @@ constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id,
 }
 
 /* Look for SVAL within the equivalence classes of this constraint_manager2;
-   if found, write the id to *OUT and return true, otherwise return false.  */
+   if found, return true, writing the id to *OUT if OUT is non-NULL,
+   otherwise return false.  */
 
 bool
 constraint_manager2::get_equiv_class2_by_svalue2 (const svalue2 *sval,
@@ -935,7 +936,8 @@ constraint_manager2::get_equiv_class2_by_svalue2 (const svalue2 *sval,
       FOR_EACH_VEC_ELT (ec->m_vars, j, iv)
 	if (iv == sval)
 	  {
-	    *out = equiv_class2_id (i);
+	    if (out)
+	      *out = equiv_class2_id (i);
 	    return true;
 	  }
     }
@@ -1362,6 +1364,19 @@ public:
   void on_fact (const svalue2 *lhs, enum tree_code code, const svalue2 *rhs)
     FINAL OVERRIDE
   {
+    /* Special-case for widening.  */
+    /* FIXME: should only do this if LHS isn't mentioned anywhere in
+       m_cm_b's model, rather than just in m_cb_b?  */
+    if (lhs->get_kind () == svalue2::SK_WIDENING)
+      if (!m_cm_b->get_equiv_class2_by_svalue2 (lhs, NULL))
+	{
+	  /* LHS isn't constrained within m_cm_b.  */
+	  /* FIXME: for now, treat it as "unmentioned".  */
+	  bool sat = m_out->add_constraint (lhs, code, rhs);
+	  gcc_assert (sat);
+	  return;
+	}
+
     if (m_cm_b->eval_condition (lhs, code, rhs).is_true ())
       {
 	bool sat = m_out->add_constraint (lhs, code, rhs);
@@ -1397,6 +1412,9 @@ constraint_manager2::merge (const constraint_manager2 &cm_a,
      and add those to *OUT.  */
   merger2_fact_visitor v (&copy_cm_b, out);
   copy_cm_a.for_each_fact (&v);
+
+  /* FIXME and the other way around, since things could be implicit in one
+     and explicit in the other?  */
 }
 
 /* A subroutine of constraint_manager2::merge.
diff --git a/gcc/analyzer/region-model2.cc b/gcc/analyzer/region-model2.cc
index 75189c7be2e..3882334d7de 100644
--- a/gcc/analyzer/region-model2.cc
+++ b/gcc/analyzer/region-model2.cc
@@ -261,8 +261,6 @@ svalue2::can_merge_p (const svalue2 *other,
   if (tree cst0 = maybe_get_constant ())
     if (tree cst1 = other->maybe_get_constant ())
       {
-	/* FIXME: we also need to distinguish these via the stmt (or
-	   program_point?) so we can handle nested loops.  */
 	return mgr->get_or_create_widening_svalue2 (other->get_type (),
 						    point, other, this);
       }
@@ -785,8 +783,9 @@ widening_svalue2::dump_to_pp (pretty_printer *pp, bool simple) const
   if (simple)
     {
       pp_string (pp, "WIDENING(");
+      pp_character (pp, '{');
       m_point.print (pp, format (false));
-      pp_string (pp, ", ");
+      pp_string (pp, "}, ");
       m_base_sval->dump_to_pp (pp, simple);
       pp_string (pp, ", ");
       m_iter_sval->dump_to_pp (pp, simple);
@@ -797,8 +796,9 @@ widening_svalue2::dump_to_pp (pretty_printer *pp, bool simple) const
       pp_string (pp, "widening_svalue2 (");
       // TODO: type?
       pp_string (pp, ", ");
+      pp_character (pp, '{');
       m_point.print (pp, format (false));
-      pp_string (pp, ", ");
+      pp_string (pp, "}, ");
       m_base_sval->dump_to_pp (pp, simple);
       pp_string (pp, ", ");
       m_iter_sval->dump_to_pp (pp, simple);
@@ -9605,7 +9605,12 @@ test_state_merging ()
     assert_region_model2s_merge (x, int_42, int_113, &merged, &merged_x_sval);
 
     /* In particular, there should be an unknown value for "x".  */
+    // FIXME
+#if WIDENING
+    ASSERT_EQ (merged_x_sval->get_kind (), svalue2::SK_WIDENING);
+#else
     ASSERT_EQ (merged_x_sval->get_kind (), svalue2::SK_UNKNOWN);
+#endif
   }
 
   /* Uninit and constant.  */
@@ -9884,6 +9889,108 @@ test_constraint_merging ()
 	     tristate (tristate::TS_UNKNOWN));
 }
 
+/* Verify merging constraints for states simulating successive iterations
+   of a loop.
+   Simulate:
+     for (i = 0; i < 256; i++)
+       [...body...]
+   i.e. this gimple:.
+     i_15 = 0;
+     goto <bb 4>;
+
+   <bb 4> :
+     i_11 = PHI <i_15(2), i_23(3)>
+     if (i_11 <= 255)
+       goto <bb 3>;
+     else
+       goto [AFTER LOOP]
+
+   <bb 3> :
+     [LOOP BODY]
+     i_23 = i_11 + 1;
+
+   and thus these ops (and resultant states):
+     i_11 = PHI()
+       {i_11: 0}
+     add_constraint (i_11 <= 255) [for the true edge]
+       {i_11: 0}  [constraint was a no-op]
+     i_23 = i_11 + 1;
+       {i_22: 1}
+     i_11 = PHI()
+       {i_11: WIDENED (at phi, 0, 1)}
+     add_constraint (i_11 <= 255) [for the true edge]
+       {i_11: WIDENED (at phi, 0, 1); WIDENED <= 255}
+     i_23 = i_11 + 1;
+       {i_23: (WIDENED (at phi, 0, 1) + 1); WIDENED <= 255}
+     i_11 = PHI()
+       {i_11: WIDENED (at phi, 0, 1); WIDENED <= 256}
+         [changing meaning of "WIDENED" here]
+     if (i_11 <= 255)
+        T: {i_11: WIDENED (at phi, 0, 1); WIDENED <= 255}; cache hit
+        F: {i_11: 256}
+
+	FIXME.
+	TODO: rename?
+ */
+
+static void
+test_iteration_1 ()
+{
+#if WIDENING
+  program_point point (program_point::origin ());
+
+  tree int_0 = build_int_cst (integer_type_node, 0);
+  tree int_1 = build_int_cst (integer_type_node, 1);
+  tree int_256 = build_int_cst (integer_type_node, 256);
+  tree i = build_global_decl ("i", integer_type_node);
+
+  region_model2_manager mgr;
+  test_region_model2_context ctxt;
+
+  /* model0: i: 0.  */
+  region_model2 model0 (&mgr);
+  model0.set_value (i, int_0, &ctxt);
+
+  /* model1: i: 1.  */
+  region_model2 model1 (&mgr);
+  model1.set_value (i, int_1, &ctxt);
+
+  /* FIXME: should merge to a widened value.  */
+  region_model2 model2 (&mgr);
+  ASSERT_TRUE (model1.can_merge_with_p (model0, point, &model2));
+  const svalue2 *merged_i = model2.get_rvalue (i, &ctxt);
+  ASSERT_EQ (merged_i->get_kind (), svalue2::SK_WIDENING);
+  /* Add constraint: i < 256  */
+  model2.add_constraint (i, LT_EXPR, int_256, &ctxt);
+  ASSERT_EQ (model2.eval_condition (i, LT_EXPR, int_256, &ctxt),
+	     tristate (tristate::TS_TRUE));
+
+  /* Try merging with the initial state.  */
+  region_model2 model3 (&mgr);
+  ASSERT_TRUE (model2.can_merge_with_p (model0, point, &model3));
+  /* Merging the merged value with the initial value should be idempotent,
+     so that the analysis converges.  */
+  ASSERT_EQ (model3.get_rvalue (i, &ctxt), merged_i);
+  /* Merger of 0 and a widening value with constraint < CST
+     should retain the constraint, even though it was implicit
+     for the 0 case.  */
+  ASSERT_EQ (model3.eval_condition (i, LT_EXPR, int_256, &ctxt),
+	     tristate (tristate::TS_TRUE));
+  /* ...and we should have equality: the analysis should have converged.  */
+  ASSERT_EQ (model3, model2);
+
+  // TODO
+#endif
+}
+
+// TODO: as above, but with comparison against "n", rather than a constant
+
+static void
+test_iteration_2 ()
+{
+  // TODO
+}
+
 #if 0
 
 /* Verify that if we mark a pointer to a malloc-ed region2 as non-NULL,
@@ -10245,6 +10352,8 @@ analyzer_region_model2_cc_tests ()
 #endif
   test_state_merging ();
   test_constraint_merging ();
+  test_iteration_1 ();
+  test_iteration_2 ();
 #if 0
   test_malloc_constraints ();
 #endif
diff --git a/gcc/analyzer/region-model2.h b/gcc/analyzer/region-model2.h
index 43ffe6e78b0..10c7d646db2 100644
--- a/gcc/analyzer/region-model2.h
+++ b/gcc/analyzer/region-model2.h
@@ -892,6 +892,10 @@ namespace ana {
    representing a possible fixed point in an iteration from the base to
    +ve infinity, or -ve infinity, and thus useful for representing a value
    within a loop.
+   We also need to capture the program_point at which the merger happens,
+   so that distinguish between different iterators, and thus handle
+   nested loops.
+
    FIXME: firm this up; clarify the above.  */
 
 class widening_svalue2 : public svalue2
-- 
2.26.2

