From 867dd0bb7f1d159bc3cbed51a549f2c36dd2530f Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Tue, 24 Mar 2026 17:19:48 -0400
Subject: [PATCH 32/98] FIXME: WIP on data flow events for divide-by-zero

---
 gcc/analyzer/call-info.cc                     |  10 ++
 gcc/analyzer/checker-event.cc                 |  41 +++++
 gcc/analyzer/checker-event.h                  |  32 ++++
 gcc/analyzer/common.h                         |  33 ++++
 gcc/analyzer/diagnostic-manager.cc            | 101 ++++++++++++-
 gcc/analyzer/diagnostic-manager.h             |  13 +-
 gcc/analyzer/engine.cc                        |  14 +-
 gcc/analyzer/exploded-graph.h                 |   7 +
 gcc/analyzer/exploded-path.cc                 |  84 +++++++----
 gcc/analyzer/exploded-path.h                  |  30 +++-
 gcc/analyzer/feasible-graph.cc                |   4 +-
 gcc/analyzer/ops.cc                           | 142 ++++++++++++++++++
 gcc/analyzer/ops.h                            |  55 +++++++
 gcc/analyzer/pending-diagnostic.cc            |  16 ++
 gcc/analyzer/pending-diagnostic.h             |   4 +
 gcc/analyzer/region-model.cc                  |  18 ++-
 gcc/digraph.cc                                |   3 +
 gcc/shortest-paths.h                          |   4 +-
 .../c-c++-common/analyzer/divide-by-zero-2.c  |  14 ++
 .../c-c++-common/analyzer/divide-by-zero-3.c  |  19 +++
 .../c-c++-common/analyzer/divide-by-zero-4.c  |  34 +++++
 .../gcc.dg/analyzer/divide-by-zero-float.c    |   2 +-
 22 files changed, 626 insertions(+), 54 deletions(-)
 create mode 100644 gcc/testsuite/c-c++-common/analyzer/divide-by-zero-2.c
 create mode 100644 gcc/testsuite/c-c++-common/analyzer/divide-by-zero-3.c
 create mode 100644 gcc/testsuite/c-c++-common/analyzer/divide-by-zero-4.c

diff --git a/gcc/analyzer/call-info.cc b/gcc/analyzer/call-info.cc
index 10022b43f343..b5d2ddbcb9c4 100644
--- a/gcc/analyzer/call-info.cc
+++ b/gcc/analyzer/call-info.cc
@@ -78,6 +78,16 @@ custom_edge_info::create_enode (exploded_graph &eg,
   return eg.get_or_create_node (point, state, enode_for_diag);
 }
 
+eedge_annotation
+custom_edge_info::update_annotation_backwards (rewind_context &ctxt,
+					       const eedge_annotation &ann,
+					       logger *) const
+{
+  // FIXME:
+  // gcc_unreachable (); // FIXME
+  return ann;
+}
+
 /* class call_info : public custom_edge_info.  */
 
 /* Implementation of custom_edge_info::print vfunc for call_info.  */
diff --git a/gcc/analyzer/checker-event.cc b/gcc/analyzer/checker-event.cc
index d1e9b4429f9d..6bd6bc71d2ac 100644
--- a/gcc/analyzer/checker-event.cc
+++ b/gcc/analyzer/checker-event.cc
@@ -67,6 +67,8 @@ event_kind_to_string (enum event_kind ek)
       return "stmt";
     case event_kind::region_creation:
       return "region_creation";
+    case event_kind::data_flow:
+      return "data_flow";
     case event_kind::function_entry:
       return "function_entry";
     case event_kind::state_change:
@@ -301,6 +303,45 @@ statement_event::print_desc (pretty_printer &pp) const
   pp_gimple_stmt_1 (&pp, m_stmt, 0, (dump_flags_t)0);
 }
 
+/* class data_flow_event : public checker_event.  */
+
+void
+data_flow_event::print_desc (pretty_printer &pp) const
+{
+  gcc_assert (m_src_reg != m_dst_reg);
+  gcc_assert (m_dst_reg);
+
+  if (m_src_reg)
+    {
+      if (m_src_reg->get_parent_region () == m_dst_reg->get_parent_region ())
+	if (tree src_decl = m_src_reg->maybe_get_decl ())
+	  if (tree dst_decl = m_dst_reg->maybe_get_decl ())
+	    {
+	      if (TREE_CODE (src_decl) == SSA_NAME
+		  && TREE_CODE (dst_decl) == SSA_NAME
+		  && SSA_NAME_VAR (src_decl) == SSA_NAME_VAR (dst_decl))
+		{
+		  pp_printf (&pp, "value of %qE unchanged here",
+			     SSA_NAME_VAR (src_decl));
+		  return;
+		}
+	    }
+
+      // FIXME:
+      gcc_assert (m_src_reg_expr);
+      gcc_assert (m_dst_reg_expr);
+
+      pp_printf (&pp, "copying value from %qE at (FIXME) to %qE",
+		 m_src_reg_expr, m_dst_reg_expr);
+      return;
+    }
+  else
+    {
+      pp_printf (&pp, "value originates here");
+    }
+}
+
+
 /* class region_creation_event : public checker_event.  */
 
 region_creation_event::region_creation_event (const event_loc_info &loc_info)
diff --git a/gcc/analyzer/checker-event.h b/gcc/analyzer/checker-event.h
index be39a89a7b17..8d2098c2991a 100644
--- a/gcc/analyzer/checker-event.h
+++ b/gcc/analyzer/checker-event.h
@@ -37,6 +37,7 @@ enum class event_kind
   custom,
   stmt,
   region_creation,
+  data_flow,
   function_entry,
   state_change,
   start_cfg_edge,
@@ -68,6 +69,7 @@ extern const char *event_kind_to_string (enum event_kind ek);
        custom_event (event_kind::custom)
 	 precanned_custom_event
        statement_event (event_kind::stmt)
+       data_flow_event (event_kind::data_flow)
        region_creation_event (event_kind::region_creation)
        function_entry_event (event_kind::function_entry)
        state_change_event (event_kind::state_change)
@@ -245,6 +247,36 @@ public:
   const program_state m_dst_state;
 };
 
+// FIXME
+
+class data_flow_event : public checker_event
+{
+public:
+  data_flow_event (const event_loc_info &loc_info,
+		   const region *src_reg,
+		   tree src_reg_expr,
+		   const region *dst_reg,
+		   tree dst_reg_expr)
+  : checker_event (event_kind::data_flow, loc_info),
+    m_src_reg (src_reg),
+    m_src_reg_expr (src_reg_expr),
+    m_dst_reg (dst_reg),
+    m_dst_reg_expr (dst_reg_expr),
+    m_prev_event (nullptr)
+  {
+    gcc_assert (src_reg != dst_reg);
+    gcc_assert (dst_reg);
+  }
+
+  void print_desc (pretty_printer &) const final override;
+
+  const region *m_src_reg;
+  tree m_src_reg_expr;
+  const region *m_dst_reg;
+  tree m_dst_reg_expr;
+  const data_flow_event *m_prev_event;
+};
+
 /* An abstract event subclass describing the creation of a region that
    is significant for a diagnostic.
 
diff --git a/gcc/analyzer/common.h b/gcc/analyzer/common.h
index 741b52cfd581..2a2a2784e90f 100644
--- a/gcc/analyzer/common.h
+++ b/gcc/analyzer/common.h
@@ -375,6 +375,34 @@ enum class access_direction
   write
 };
 
+// FIXME:
+
+struct eedge_annotation
+{
+  eedge_annotation ()
+  : m_region_holding_value (nullptr)
+  {
+  }
+
+  void dump_to_pp (pretty_printer *) const;
+  void dump () const;
+
+  bool
+  operator== (const eedge_annotation &other) const
+  {
+    return m_region_holding_value == other.m_region_holding_value;
+  }
+  bool
+  operator!= (const eedge_annotation &other) const
+  {
+    return !(*this == other);
+  }
+
+  const region *m_region_holding_value;
+};
+
+struct rewind_context;
+
 /* Abstract base class for associating custom data with an
    exploded_edge, for handling non-standard edges such as
    rewinding from a longjmp, signal handlers, etc.
@@ -414,6 +442,11 @@ public:
 				       program_state &&state,
 				       exploded_node *enode_for_diag,
 				       region_model_context *ctxt) const;
+
+  virtual eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const;
 };
 
 /* Abstract base class for splitting state.
diff --git a/gcc/analyzer/diagnostic-manager.cc b/gcc/analyzer/diagnostic-manager.cc
index a0f149e9c522..c4825ff9826e 100644
--- a/gcc/analyzer/diagnostic-manager.cc
+++ b/gcc/analyzer/diagnostic-manager.cc
@@ -917,7 +917,7 @@ compatible_epath_p (const exploded_path *lhs_path,
       while (lhs_eedge_idx >= 0)
 	{
 	  /* Find LHS_PATH's next superedge.  */
-	  lhs_eedge = lhs_path->m_edges[lhs_eedge_idx];
+	  lhs_eedge = lhs_path->m_elements[lhs_eedge_idx].m_eedge;
 	  if (lhs_eedge->m_sedge)
 	    break;
 	  else
@@ -926,7 +926,7 @@ compatible_epath_p (const exploded_path *lhs_path,
       while (rhs_eedge_idx >= 0)
 	{
 	  /* Find RHS_PATH's next superedge.  */
-	  rhs_eedge = rhs_path->m_edges[rhs_eedge_idx];
+	  rhs_eedge = rhs_path->m_elements[rhs_eedge_idx].m_eedge;
 	  if (rhs_eedge->m_sedge)
 	    break;
 	  else
@@ -1555,7 +1555,7 @@ diagnostic_manager::emit_saved_diagnostic (const exploded_graph &eg,
        sd.get_index (), sd.m_d->get_kind (), sd.get_supernode ()->m_id);
   log ("num dupes: %i", sd.get_num_dupes ());
 
-  const exploded_path *epath = sd.get_best_epath ();
+  exploded_path *epath = sd.get_best_epath ();
   gcc_assert (epath);
 
   /* Precompute all enodes from which the diagnostic is reachable.  */
@@ -1567,6 +1567,9 @@ diagnostic_manager::emit_saved_diagnostic (const exploded_graph &eg,
 			      eg.get_ext_state (),
 			      get_logger ());
 
+  // FIXME:
+  annotate_exploded_path (pb, *epath);
+
   /* Populate emission_path with a full description of EPATH.  */
   build_emission_path (pb, *epath, &emission_path);
 
@@ -1640,6 +1643,52 @@ diagnostic_manager::get_logical_location_manager () const
   return *mgr;
 }
 
+// FIXME
+
+void
+diagnostic_manager::annotate_exploded_path (const path_builder &pb,
+					    exploded_path &epath) const
+{
+  // FIXME:
+  LOG_SCOPE (get_logger ());
+
+  // FIXME: consolidate this with build_emission_path?
+  interesting_t interest;
+  pb.get_pending_diagnostic ()->mark_interesting_stuff (&interest);
+
+  gcc_assert (epath.m_elements.length () > 0);
+
+  eedge_annotation curr_annotation;
+
+  if (interest.m_read_regions.length () > 0)
+    curr_annotation.m_region_holding_value = interest.m_read_regions[0];
+
+  // Walk epath backwards, propagating annotation information
+  for (int idx = epath.m_elements.length () - 1; idx > 0; --idx)
+    {
+      exploded_path::element_t &iter_element = epath.m_elements[idx];
+      iter_element.m_annotation_at_dst = curr_annotation;
+      eedge_annotation &annotation_at_src = iter_element.m_annotation_at_src;
+      const exploded_edge *eedge = iter_element.m_eedge;
+      gcc_assert (eedge);
+
+      rewind_context ctxt (*eedge);
+      if (eedge->m_custom_info)
+	annotation_at_src
+	  = eedge->m_custom_info->update_annotation_backwards (ctxt,
+							       curr_annotation,
+							       get_logger ());
+      else if (const operation *op = eedge->maybe_get_op ())
+	annotation_at_src = op->update_annotation_backwards (ctxt,
+							     curr_annotation,
+							     get_logger ());
+      else
+	annotation_at_src = curr_annotation;
+
+      curr_annotation = annotation_at_src;
+    }
+}
+
 /* Emit a "path" of events to EMISSION_PATH describing the exploded path
    EPATH within EG.  */
 
@@ -1683,10 +1732,20 @@ diagnostic_manager::build_emission_path (const path_builder &pb,
   }
 
   /* Walk EPATH, adding events as appropriate.  */
-  for (unsigned i = 0; i < epath.m_edges.length (); i++)
+  for (unsigned i = 0; i < epath.m_elements.length (); i++)
     {
-      const exploded_edge *eedge = epath.m_edges[i];
+      const exploded_edge *eedge = epath.m_elements[i].m_eedge;
+      gcc_assert (eedge);
       add_events_for_eedge (pb, *eedge, emission_path, &interest);
+
+      if (epath.m_elements[i].m_annotation_at_src
+	  != epath.m_elements[i].m_annotation_at_dst)
+	maybe_add_dataflow_event
+	  (pb,
+	   *epath.m_elements[i].m_eedge,
+	   epath.m_elements[i].m_annotation_at_src,
+	   epath.m_elements[i].m_annotation_at_dst,
+	   *emission_path);
     }
   add_event_on_final_node (pb, epath.get_final_enode (),
 			   emission_path, &interest);
@@ -2046,6 +2105,37 @@ diagnostic_manager::add_events_for_eedge (const path_builder &pb,
     }
 }
 
+void
+diagnostic_manager::maybe_add_dataflow_event (const path_builder &pb,
+					      const exploded_edge &eedge,
+					      const eedge_annotation &src_ann,
+					      const eedge_annotation &dst_ann,
+					      checker_path &emission_path) const
+{
+  gcc_assert (src_ann.m_region_holding_value
+	      != dst_ann.m_region_holding_value);
+  gcc_assert (dst_ann.m_region_holding_value);
+
+  const region *src_reg = src_ann.m_region_holding_value;
+  tree src_reg_expr = NULL_TREE;
+  if (src_reg)
+    src_reg_expr
+      = eedge.m_src->get_state ().m_region_model->get_representative_tree
+	  (src_reg);
+
+  const region *dst_reg = dst_ann.m_region_holding_value;
+  tree dst_reg_expr
+    = eedge.m_dest->get_state ().m_region_model->get_representative_tree
+	(dst_reg);
+
+  emission_path.add_event
+    (std::make_unique<data_flow_event> (eedge.m_src->get_point (),
+					src_reg,
+					src_reg_expr,
+					dst_reg,
+					dst_reg_expr));
+}
+
 /* Return true if EEDGE is a significant edge in the path to the diagnostic
    for PB.
 
@@ -2238,6 +2328,7 @@ diagnostic_manager::prune_for_sm_diagnostic (checker_path *path,
 	  break;
 
 	case event_kind::region_creation:
+	case event_kind::data_flow:
 	  /* Don't filter these.  */
 	  break;
 
diff --git a/gcc/analyzer/diagnostic-manager.h b/gcc/analyzer/diagnostic-manager.h
index 58c016649655..5ccbf09d91c6 100644
--- a/gcc/analyzer/diagnostic-manager.h
+++ b/gcc/analyzer/diagnostic-manager.h
@@ -101,7 +101,7 @@ public:
   }
 
   bool calc_best_epath (epath_finder *pf);
-  const exploded_path *get_best_epath () const { return m_best_epath.get (); }
+  exploded_path *get_best_epath () const { return m_best_epath.get (); }
   unsigned get_epath_length () const;
 
   void add_duplicate (saved_diagnostic *other);
@@ -201,6 +201,10 @@ private:
   const diagnostics::logical_locations::manager &
   get_logical_location_manager () const;
 
+  void
+  annotate_exploded_path (const path_builder &pb,
+			  exploded_path &epath) const;
+
   void build_emission_path (const path_builder &pb,
 			    const exploded_path &epath,
 			    checker_path *emission_path) const;
@@ -215,6 +219,13 @@ private:
 			     checker_path *emission_path,
 			     interesting_t *interest) const;
 
+  void
+  maybe_add_dataflow_event (const path_builder &pb,
+			    const exploded_edge &eedge,
+			    const eedge_annotation &src_ann,
+			    const eedge_annotation &dst_ann,
+			    checker_path &emission_path) const;
+
   bool significant_edge_p (const path_builder &pb,
 			   const exploded_edge &eedge) const;
 
diff --git a/gcc/analyzer/engine.cc b/gcc/analyzer/engine.cc
index 1a7022edd724..f7bd822064fc 100644
--- a/gcc/analyzer/engine.cc
+++ b/gcc/analyzer/engine.cc
@@ -308,10 +308,10 @@ public:
 	       after the SSA name was set? (if any).  */
 
 	    for (unsigned idx = idx_of_def_stmt + 1;
-		 idx < epath.m_edges.length ();
+		 idx < epath.m_elements.length ();
 		 ++idx)
 	      {
-		const exploded_edge *eedge = epath.m_edges[idx];
+		const exploded_edge *eedge = epath.m_elements[idx].m_eedge;
 		if (logger)
 		  logger->log ("eedge[%i]: EN %i -> EN %i",
 			       idx,
@@ -353,9 +353,10 @@ public:
 
 	log_scope sentinel (logger, "walking backward along epath");
 	int idx;
-	const exploded_edge *eedge;
-	FOR_EACH_VEC_ELT_REVERSE (epath.m_edges, idx, eedge)
+	exploded_path::element_t *element;
+	FOR_EACH_VEC_ELT_REVERSE (epath.m_elements, idx, element)
 	  {
+	    const exploded_edge *eedge = element->m_eedge;
 	    if (logger)
 	      {
 		logger->log ("eedge[%i]: EN %i -> EN %i",
@@ -404,9 +405,10 @@ private:
     LOG_SCOPE (logger);
 
     int idx;
-    const exploded_edge *eedge;
-    FOR_EACH_VEC_ELT_REVERSE (epath.m_edges, idx, eedge)
+    exploded_path::element_t *element;
+    FOR_EACH_VEC_ELT_REVERSE (epath.m_elements, idx, element)
       {
+	const exploded_edge *eedge = element->m_eedge;
 	if (eedge->m_src->get_stack_depth ()
 	    != eedge->m_dest->get_stack_depth ())
 	  {
diff --git a/gcc/analyzer/exploded-graph.h b/gcc/analyzer/exploded-graph.h
index 0972e217baf5..c5d87d135260 100644
--- a/gcc/analyzer/exploded-graph.h
+++ b/gcc/analyzer/exploded-graph.h
@@ -465,6 +465,13 @@ public:
 			   const exploded_edge &eedge,
 			   pending_diagnostic &pd) const final override;
 
+#if 0
+  eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const final override;
+#endif
+
   program_point
   get_point_before_setjmp () const
   {
diff --git a/gcc/analyzer/exploded-path.cc b/gcc/analyzer/exploded-path.cc
index b10761a9388a..44d4a2b8cf26 100644
--- a/gcc/analyzer/exploded-path.cc
+++ b/gcc/analyzer/exploded-path.cc
@@ -26,17 +26,34 @@ along with GCC; see the file COPYING3.  If not see
 
 namespace ana {
 
+// struct eedge_annotation
+
+void
+eedge_annotation::dump_to_pp (pretty_printer *pp) const
+{
+  if (m_region_holding_value)
+    m_region_holding_value->dump_to_pp (pp, true);
+}
+
+void
+eedge_annotation::dump () const
+{
+  tree_dump_pretty_printer pp (stderr);
+  dump_to_pp (&pp);
+  pp_newline (&pp);
+}
+
 /* class exploded_path.  */
 
 /* Copy ctor.  */
 
 exploded_path::exploded_path (const exploded_path &other)
-: m_edges (other.m_edges.length ())
+: m_elements (other.m_elements.length ())
 {
   int i;
-  const exploded_edge *eedge;
-  FOR_EACH_VEC_ELT (other.m_edges, i, eedge)
-    m_edges.quick_push (eedge);
+  element_t *element;
+  FOR_EACH_VEC_ELT (other.m_elements, i, element)
+    m_elements.quick_push (*element);
 }
 
 /* Look for the last use of SEARCH_STMT within this path.
@@ -48,30 +65,33 @@ exploded_path::find_stmt_backwards (const gimple *search_stmt,
 				    int *out_idx) const
 {
   int i;
-  const exploded_edge *eedge;
-  FOR_EACH_VEC_ELT_REVERSE (m_edges, i, eedge)
-    if (search_stmt->code == GIMPLE_PHI)
-      {
-	/* Each phis_for_edge_op instance handles multiple phi stmts
-	   at once, so we have to special-case the search for a phi stmt.  */
-	if (auto op = eedge->maybe_get_op ())
-	  if (auto phis_op = op->dyn_cast_phis_for_edge_op ())
-	    if (phis_op->defines_ssa_name_p (gimple_phi_result (search_stmt)))
+  element_t *element;
+  FOR_EACH_VEC_ELT_REVERSE (m_elements, i, element)
+    {
+      const exploded_edge *eedge = element->m_eedge;
+      if (search_stmt->code == GIMPLE_PHI)
+	{
+	  /* Each phis_for_edge_op instance handles multiple phi stmts
+	     at once, so we have to special-case the search for a phi stmt.  */
+	  if (auto op = eedge->maybe_get_op ())
+	    if (auto phis_op = op->dyn_cast_phis_for_edge_op ())
+	      if (phis_op->defines_ssa_name_p (gimple_phi_result (search_stmt)))
+		{
+		  *out_idx = i;
+		  return true;
+		}
+	}
+      else
+	{
+	  /* Non-phi stmt.  */
+	  if (const gimple *stmt = eedge->maybe_get_stmt ())
+	    if (stmt == search_stmt)
 	      {
 		*out_idx = i;
 		return true;
 	      }
-      }
-    else
-      {
-	/* Non-phi stmt.  */
-	if (const gimple *stmt = eedge->maybe_get_stmt ())
-	  if (stmt == search_stmt)
-	    {
-	      *out_idx = i;
-	      return true;
-	    }
-      }
+	}
+    }
   return false;
 }
 
@@ -80,8 +100,8 @@ exploded_path::find_stmt_backwards (const gimple *search_stmt,
 exploded_node *
 exploded_path::get_final_enode () const
 {
-  gcc_assert (m_edges.length () > 0);
-  return m_edges[m_edges.length () - 1]->m_dest;
+  gcc_assert (m_elements.length () > 0);
+  return m_elements[m_elements.length () - 1].m_eedge->m_dest;
 }
 
 /* Check state along this path, returning true if it is feasible.
@@ -99,9 +119,9 @@ exploded_path::feasible_p (logger *logger,
 			   eg->get_supergraph ());
 
   /* Traverse the path, updating this state.  */
-  for (unsigned edge_idx = 0; edge_idx < m_edges.length (); edge_idx++)
+  for (unsigned edge_idx = 0; edge_idx < m_elements.length (); edge_idx++)
     {
-      const exploded_edge *eedge = m_edges[edge_idx];
+      const exploded_edge *eedge = m_elements[edge_idx].m_eedge;
       if (logger)
 	logger->log ("considering edge %i: EN:%i -> EN:%i",
 		     edge_idx,
@@ -140,13 +160,15 @@ void
 exploded_path::dump_to_pp (pretty_printer *pp,
 			   const extrinsic_state *ext_state) const
 {
-  for (unsigned i = 0; i < m_edges.length (); i++)
+  for (unsigned i = 0; i < m_elements.length (); i++)
     {
-      const exploded_edge *eedge = m_edges[i];
-      pp_printf (pp, "m_edges[%i]: EN %i -> EN %i",
+      const element_t &element = m_elements[i];
+      const exploded_edge *eedge = element.m_eedge;
+      pp_printf (pp, "m_elements[%i]: EN %i -> EN %i",
 		 i,
 		 eedge->m_src->m_index,
 		 eedge->m_dest->m_index);
+      // FIXME: print info about annotations
       pp_newline (pp);
 
       if (ext_state)
diff --git a/gcc/analyzer/exploded-path.h b/gcc/analyzer/exploded-path.h
index 8c5ce9766a1b..157998e52edd 100644
--- a/gcc/analyzer/exploded-path.h
+++ b/gcc/analyzer/exploded-path.h
@@ -30,10 +30,22 @@ namespace ana {
 class exploded_path
 {
 public:
-  exploded_path () : m_edges () {}
+  struct element_t
+  {
+    element_t (const exploded_edge *eedge)
+    : m_eedge (eedge)
+    {
+    }
+
+    const exploded_edge *m_eedge;
+    eedge_annotation m_annotation_at_src;
+    eedge_annotation m_annotation_at_dst;
+  };
+
+  exploded_path () : m_elements () {}
   exploded_path (const exploded_path &other);
 
-  unsigned length () const { return m_edges.length (); }
+  unsigned length () const { return m_elements.length (); }
 
   bool find_stmt_backwards (const gimple *search_stmt,
 			    int *out_idx) const;
@@ -50,7 +62,19 @@ public:
   bool feasible_p (logger *logger, std::unique_ptr<feasibility_problem> *out,
 		    engine *eng, const exploded_graph *eg) const;
 
-  auto_vec<const exploded_edge *> m_edges;
+  void
+  append_edge (const exploded_edge *edge)
+  {
+    m_elements.safe_push (edge);
+  }
+
+  void
+  reverse ()
+  {
+    m_elements.reverse ();
+  }
+
+  auto_vec<element_t> m_elements;
 };
 
 /* Finding the shortest exploded_path within an exploded_graph.  */
diff --git a/gcc/analyzer/feasible-graph.cc b/gcc/analyzer/feasible-graph.cc
index b3097f189a1b..e6513cd4e2a5 100644
--- a/gcc/analyzer/feasible-graph.cc
+++ b/gcc/analyzer/feasible-graph.cc
@@ -187,12 +187,12 @@ feasible_graph::make_epath (feasible_node *fnode) const
       gcc_assert (fnode->m_preds.length () == 1);
       feasible_edge *pred_fedge
 	= static_cast <feasible_edge *> (fnode->m_preds[0]);
-      epath->m_edges.safe_push (pred_fedge->get_inner_edge ());
+      epath->m_elements.safe_push (pred_fedge->get_inner_edge ());
       fnode = static_cast <feasible_node *> (pred_fedge->m_src);
     }
 
   /* Now reverse it.  */
-  epath->m_edges.reverse ();
+  epath->m_elements.reverse ();
 
   return epath;
 }
diff --git a/gcc/analyzer/ops.cc b/gcc/analyzer/ops.cc
index b40e078c928b..1975ea6dd6d3 100644
--- a/gcc/analyzer/ops.cc
+++ b/gcc/analyzer/ops.cc
@@ -663,8 +663,87 @@ gimple_stmt_op::add_any_events_for_eedge (const exploded_edge &eedge,
     }
 }
 
+// class gasm_op : public gimple_stmt_op
+
+eedge_annotation
+gasm_op::update_annotation_backwards (rewind_context &ctxt,
+				      const eedge_annotation &ann,
+				      logger *logger) const
+{
+  LOG_SCOPE (logger);
+  gcc_unreachable (); // FIXME
+}
+
 // class gassign_op : public gimple_stmt_op
 
+eedge_annotation
+gassign_op::update_annotation_backwards (rewind_context &ctxt,
+					 const eedge_annotation &ann,
+					 logger *logger) const
+{
+  LOG_SCOPE (logger);
+  if (logger)
+    {
+      logger->start_log_line ();
+      pp_gimple_stmt_1 (logger->get_printer (), &get_stmt (), 0,
+			(dump_flags_t)0);
+      logger->end_log_line ();
+    }
+
+  const gassign &assign = get_gassign ();
+  tree lhs = gimple_assign_lhs (&assign);
+  tree rhs1 = gimple_assign_rhs1 (&assign);
+  enum tree_code op = gimple_assign_rhs_code (&assign);
+
+  eedge_annotation result (ann);
+
+  switch (op)
+    {
+    default:
+      gcc_unreachable (); // FIXME
+
+    case SSA_NAME:
+    case VAR_DECL:
+    case PARM_DECL:
+    case COMPONENT_REF:
+      {
+	const region *dst_reg_in_dst_enode
+	  = ctxt.m_eedge.m_dest->get_state ().m_region_model->get_lvalue
+	      (lhs, nullptr);
+	if (ann.m_region_holding_value == dst_reg_in_dst_enode)
+	  {
+	    if (logger)
+	      logger->log ("updating m_region_holding_value for assign");
+	    const region *src_reg_in_src_enode
+	      = ctxt.m_eedge.m_src->get_state ().m_region_model->get_lvalue
+		  (rhs1, nullptr);
+	    result.m_region_holding_value = src_reg_in_src_enode;
+	  }
+      }
+      break;
+
+    case INTEGER_CST:
+    case REAL_CST:
+      if (logger)
+	logger->log ("value comes from here");
+      result.m_region_holding_value = nullptr;
+      break;
+    }
+
+  return result;
+}
+
+// class predict_op : public gimple_stmt_op
+
+eedge_annotation
+predict_op::update_annotation_backwards (rewind_context &ctxt,
+					 const eedge_annotation &ann,
+					 logger *logger) const
+{
+  LOG_SCOPE (logger);
+  gcc_unreachable (); // FIXME
+}
+
 // class greturn_op : public gimple_stmt_op
 
 void
@@ -734,6 +813,16 @@ greturn_op::add_any_events_for_eedge (const exploded_edge &,
   // No-op.
 }
 
+eedge_annotation
+greturn_op::update_annotation_backwards (rewind_context &ctxt,
+					 const eedge_annotation &ann,
+					 logger *logger) const
+{
+  LOG_SCOPE (logger);
+  //gcc_unreachable (); // FIXME
+  return ann;
+}
+
 // class call_and_return_op : public gimple_stmt_op
 
 std::unique_ptr<operation>
@@ -1023,6 +1112,16 @@ replay_call_summaries (operation_context &op_ctxt,
     }
 }
 
+eedge_annotation
+call_and_return_op::update_annotation_backwards (rewind_context &ctxt,
+						 const eedge_annotation &ann,
+						 logger *logger) const
+{
+  LOG_SCOPE (logger);
+  // gcc_unreachable (); // FIXME
+  return ann; // FIXME
+}
+
 /* A concrete call_info subclass representing a replay of a call summary.  */
 
 class call_summary_edge_info : public call_info
@@ -1314,6 +1413,15 @@ execute_for_feasibility (const exploded_edge &eedge,
 			    out_rc);
 }
 
+eedge_annotation
+control_flow_op::update_annotation_backwards (rewind_context &ctxt,
+					      const eedge_annotation &ann,
+					      logger *logger) const
+{
+  LOG_SCOPE (logger);
+  return ann;
+}
+
 // class gcond_edge_op : public control_flow_op
 
 gcond_edge_op::gcond_edge_op (::edge cfg_edge,
@@ -2350,6 +2458,31 @@ phis_for_edge_op::add_any_events_for_eedge (const exploded_edge &,
   // No-op
 }
 
+eedge_annotation
+phis_for_edge_op::update_annotation_backwards (rewind_context &ctxt,
+					       const eedge_annotation &ann,
+					       logger *logger) const
+{
+  LOG_SCOPE (logger);
+  eedge_annotation result (ann);
+  for (auto iter : m_pairs)
+    {
+      const region *dst_reg_in_dst_enode
+	= ctxt.m_eedge.m_dest->get_state ().m_region_model->get_lvalue
+	    (iter.m_dst, nullptr);
+      if (ann.m_region_holding_value == dst_reg_in_dst_enode)
+	{
+	  if (logger)
+	    logger->log ("updating m_region_holding_value_at_dst for phi");
+	  const region *src_reg_in_src_enode
+	    = ctxt.m_eedge.m_src->get_state ().m_region_model->get_lvalue
+	    (iter.m_src, nullptr);
+	  result.m_region_holding_value = src_reg_in_src_enode;
+	}
+    }
+  return result;
+}
+
 // class resx_op : public gimple_stmt_op
 
 void
@@ -2388,6 +2521,15 @@ resx_op::add_any_events_for_eedge (const exploded_edge &,
 {
 }
 
+eedge_annotation
+resx_op::update_annotation_backwards (rewind_context &ctxt,
+				      const eedge_annotation &ann,
+				      logger *logger) const
+{
+  LOG_SCOPE (logger);
+  gcc_unreachable (); // FIXME
+}
+
 } // namespace ana
 
 #endif /* #if ENABLE_ANALYZER */
diff --git a/gcc/analyzer/ops.h b/gcc/analyzer/ops.h
index f1c67d4e7710..1a901b0c6957 100644
--- a/gcc/analyzer/ops.h
+++ b/gcc/analyzer/ops.h
@@ -74,6 +74,16 @@ struct operation_context
   const superedge &m_sedge;
 };
 
+struct rewind_context
+{
+  rewind_context (const exploded_edge &eedge)
+  : m_eedge (eedge)
+  {
+  }
+
+  const exploded_edge &m_eedge;
+};
+
 /* Abstract base class for an operation along a superedge.  */
 
 class operation
@@ -163,6 +173,11 @@ class operation
 
   enum kind get_kind () const { return m_kind; }
 
+  virtual eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const = 0;
+
 protected:
   operation (enum kind kind_)
   : m_kind (kind_)
@@ -257,6 +272,11 @@ public:
   {
     return *as_a <const gasm *> (&get_stmt ());
   }
+
+  eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const final override;
 };
 
 /* An operation subclass representing the effect of a GIMPLE_ASSIGN stmt.  */
@@ -279,6 +299,11 @@ public:
   {
     return *as_a <const gassign *> (&get_stmt ());
   }
+
+  eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const final override;
 };
 
 /* An operation subclass for a GIMPLE_PREDICT stmt.
@@ -300,6 +325,11 @@ public:
   {
     return std::make_unique<predict_op> (get_stmt ());
   }
+
+  eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const final override;
 };
 
 /* An operation subclass representing both:
@@ -350,6 +380,11 @@ public:
   {
     return gimple_return_retval (&get_greturn ());
   }
+
+  eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const final override;
 };
 
 /* A concrete operation subclass representing the effect of a GIMPLE_CALL stmt.
@@ -428,6 +463,11 @@ public:
   const known_function *
   maybe_get_known_function (const call_details &cd) const;
 
+  eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const final override;
+
 private:
   cgraph_edge *
   get_any_cgraph_edge (operation_context &op_ctxt) const;
@@ -580,6 +620,11 @@ public:
   void
   add_any_events_for_eedge (const exploded_edge &eedge,
 			    checker_path &out_path) const final override;
+
+  eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const final override;
 };
 
 /* An abstract subclass of operation representing the filtering effect on
@@ -638,6 +683,11 @@ public:
 
   const gimple &get_ctrlflow_stmt () const { return m_ctrlflow_stmt; }
 
+  eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const final override;
+
 protected:
   control_flow_op (enum kind kind_,
 		   ::edge cfg_edge,
@@ -983,6 +1033,11 @@ public:
   add_any_events_for_eedge (const exploded_edge &eedge,
 			    checker_path &out_path) const final override;
 
+  eedge_annotation
+  update_annotation_backwards (rewind_context &ctxt,
+			       const eedge_annotation &ann,
+			       logger *) const final override;
+
   const std::vector<pair> &get_pairs () const { return m_pairs; }
 
 private:
diff --git a/gcc/analyzer/pending-diagnostic.cc b/gcc/analyzer/pending-diagnostic.cc
index 2d90a91766f7..faf66aed70bc 100644
--- a/gcc/analyzer/pending-diagnostic.cc
+++ b/gcc/analyzer/pending-diagnostic.cc
@@ -58,6 +58,15 @@ interesting_t::add_region_creation (const region *reg)
   m_region_creation.safe_push (reg);
 }
 
+// FIXME
+
+void
+interesting_t::add_read_region (const region *reg)
+{
+  gcc_assert (reg);
+  m_read_regions.safe_push (reg);
+}
+
 void
 interesting_t::dump_to_pp (pretty_printer *pp, bool simple) const
 {
@@ -70,6 +79,13 @@ interesting_t::dump_to_pp (pretty_printer *pp, bool simple) const
 	pp_string (pp, ", ");
       reg->dump_to_pp (pp, simple);
     }
+  pp_string (pp, "], read regions: [");
+  FOR_EACH_VEC_ELT (m_read_regions, i, reg)
+    {
+      if (i > 0)
+	pp_string (pp, ", ");
+      reg->dump_to_pp (pp, simple);
+    }
   pp_string (pp, "]}");
 }
 
diff --git a/gcc/analyzer/pending-diagnostic.h b/gcc/analyzer/pending-diagnostic.h
index 4236acc780f0..cbed366af34b 100644
--- a/gcc/analyzer/pending-diagnostic.h
+++ b/gcc/analyzer/pending-diagnostic.h
@@ -26,6 +26,7 @@ along with GCC; see the file COPYING3.  If not see
 
 namespace ana {
 
+// FIXME:
 /* A bundle of information about things that are of interest to a
    pending_diagnostic.
 
@@ -37,9 +38,12 @@ struct interesting_t
 {
   void add_region_creation (const region *reg);
 
+  void add_read_region (const region *reg);
+
   void dump_to_pp (pretty_printer *pp, bool simple) const;
 
   auto_vec<const region *> m_region_creation;
+  auto_vec<const region *> m_read_regions;
 };
 
 /* Various bundles of information used for generating more precise
diff --git a/gcc/analyzer/region-model.cc b/gcc/analyzer/region-model.cc
index e4bafebbaa49..50738ab338fc 100644
--- a/gcc/analyzer/region-model.cc
+++ b/gcc/analyzer/region-model.cc
@@ -859,8 +859,10 @@ class div_by_zero_diagnostic
 : public pending_diagnostic_subclass<div_by_zero_diagnostic>
 {
 public:
-  div_by_zero_diagnostic (const gassign *assign)
-  : m_assign (assign)
+  div_by_zero_diagnostic (const gassign *assign,
+			  const region *divisor_reg)
+  : m_assign (assign),
+    m_divisor_reg (divisor_reg)
   {}
 
   const char *get_kind () const final override
@@ -891,8 +893,15 @@ public:
     return true;
   }
 
+  void
+  mark_interesting_stuff (interesting_t *interest)
+  {
+    interest->add_read_region (m_divisor_reg);
+  }
+
 private:
   const gassign *m_assign;
+  const region *m_divisor_reg;
 };
 
 /* Check the pointer subtraction SVAL_A - SVAL_B at ASSIGN and add
@@ -1130,8 +1139,11 @@ region_model::get_gassign_result (const gassign *assign,
 		{
 		  if (ctxt)
 		    {
+		      const region *rhs2_reg
+			= get_lvalue (gimple_assign_rhs2 (assign), nullptr);
 		      ctxt->warn
-			(std::make_unique<div_by_zero_diagnostic> (assign));
+			(std::make_unique<div_by_zero_diagnostic> (assign,
+								   rhs2_reg));
 		      ctxt->terminate_path ();
 		    }
 		  return nullptr;
diff --git a/gcc/digraph.cc b/gcc/digraph.cc
index 724d541e68f5..fc015b8330bd 100644
--- a/gcc/digraph.cc
+++ b/gcc/digraph.cc
@@ -96,6 +96,9 @@ struct test_cluster : public cluster<test_graph_traits>
 
 struct test_path
 {
+  void append_edge (const test_edge *edge) { m_edges.safe_push (edge); }
+  void reverse () { m_edges.reverse (); }
+
   auto_vec<const test_edge *> m_edges;
 };
 
diff --git a/gcc/shortest-paths.h b/gcc/shortest-paths.h
index dd0d4d2a1934..5351b7e37374 100644
--- a/gcc/shortest-paths.h
+++ b/gcc/shortest-paths.h
@@ -187,7 +187,7 @@ get_shortest_path (const node_t *other_node) const
 
   while (m_best_edge[other_node->m_index])
     {
-      result.m_edges.safe_push (m_best_edge[other_node->m_index]);
+      result.append_edge (m_best_edge[other_node->m_index]);
       if (m_sense == SPS_FROM_GIVEN_ORIGIN)
 	other_node = m_best_edge[other_node->m_index]->m_src;
       else
@@ -195,7 +195,7 @@ get_shortest_path (const node_t *other_node) const
     }
 
   if (m_sense == SPS_FROM_GIVEN_ORIGIN)
-    result.m_edges.reverse ();
+    result.reverse ();
 
   return result;
 }
diff --git a/gcc/testsuite/c-c++-common/analyzer/divide-by-zero-2.c b/gcc/testsuite/c-c++-common/analyzer/divide-by-zero-2.c
new file mode 100644
index 000000000000..c6bc16c0e912
--- /dev/null
+++ b/gcc/testsuite/c-c++-common/analyzer/divide-by-zero-2.c
@@ -0,0 +1,14 @@
+/* { dg-additional-options "-fno-analyzer-state-merge" } */
+
+extern int
+get_value (void);
+
+int
+test (int flag)
+{
+  int x = 42;
+  int y = 0;
+  if (flag)
+    y = get_value ();
+  return x / y; /* { dg-warning "division by zero" } */
+}
diff --git a/gcc/testsuite/c-c++-common/analyzer/divide-by-zero-3.c b/gcc/testsuite/c-c++-common/analyzer/divide-by-zero-3.c
new file mode 100644
index 000000000000..6be3e763f55f
--- /dev/null
+++ b/gcc/testsuite/c-c++-common/analyzer/divide-by-zero-3.c
@@ -0,0 +1,19 @@
+/* { dg-additional-options "-fno-analyzer-state-merge" } */
+
+extern int
+get_value (void);
+
+int
+test (int flag, int flag_2, int flag_3)
+{
+  int x = 42;
+  int y = 10;
+  int z = 0;
+  if (flag)
+    y = get_value ();
+  if (flag_2)
+    z = get_value ();
+  if (flag_3)
+    y = z;
+  return x / y; /* { dg-warning "division by zero" } */
+}
diff --git a/gcc/testsuite/c-c++-common/analyzer/divide-by-zero-4.c b/gcc/testsuite/c-c++-common/analyzer/divide-by-zero-4.c
new file mode 100644
index 000000000000..139dbf535e36
--- /dev/null
+++ b/gcc/testsuite/c-c++-common/analyzer/divide-by-zero-4.c
@@ -0,0 +1,34 @@
+/* { dg-additional-options "-fno-analyzer-state-merge" } */
+
+int
+get_zero (void)
+{
+  return 0;
+}
+
+struct foo { int x; int y; };
+
+void
+init_foo (struct foo *f, int x, int y)
+{
+  f->x = x;
+  f->y = y;
+}
+
+int
+do_divide (struct foo *f)
+{
+  return f->x / f->y;
+}
+
+int
+test (int flag, int flag_2, int flag_3)
+{
+  struct foo f;
+  int a = 42;
+  int b = 10;
+  if (flag)
+    b = get_zero ();
+  init_foo (&f, a, b);
+  return do_divide (&f);
+}
diff --git a/gcc/testsuite/gcc.dg/analyzer/divide-by-zero-float.c b/gcc/testsuite/gcc.dg/analyzer/divide-by-zero-float.c
index 3aaee568bc1c..940c57251690 100644
--- a/gcc/testsuite/gcc.dg/analyzer/divide-by-zero-float.c
+++ b/gcc/testsuite/gcc.dg/analyzer/divide-by-zero-float.c
@@ -7,7 +7,7 @@ test_1 ()
 static float __attribute__((noinline))
 get_zero ()
 {
-  return 0.f;
+  return 0.f; /* { dg-message "value originates here" } */
 }
 
 float
-- 
2.49.0

