Merge pull request #6711 from tautschnig/bugfixes/dependence-graph-return-values

Program dependence graph: track SET_RETURN_VALUE instruction

Author: kroening

regression/cbmc/return3/full-slice.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/analyses/dependence_graph.cpp

@@ -188,6 +188,24 @@ void dep_graph_domaint::data_dependencies(
 
     dep_graph.reaching_definitions()[to].clear_cache(read_object_entry.first);
   }
+
+  if(to->is_set_return_value())
+  {
+    auto entry = dep_graph.end_function_map.find(function_to);
+    CHECK_RETURN(entry != dep_graph.end_function_map.end());
+
+    goto_programt::const_targett end_function = entry->second;
+
+    dep_graph_domaint *s =
+      dynamic_cast<dep_graph_domaint *>(&(dep_graph.get_state(end_function)));
+    CHECK_RETURN(s != nullptr);
+
+    if(s->is_bottom())
+      s->has_values = tvt::unknown();
+
+    if(s->data_deps.insert(to).second)
+      s->has_changed = true;
+  }
 }
 
 void dep_graph_domaint::transform(

src/analyses/dependence_graph.h

@@ -224,6 +224,16 @@ class dependence_grapht:
   {
     ait<dep_graph_domaint>::initialize(goto_functions);
     rd(goto_functions, ns);
+
+    for(const auto &entry : goto_functions.function_map)
+    {
+      const goto_programt &goto_program = entry.second.body;
+      if(!goto_program.empty())
+      {
+        end_function_map.emplace(
+          entry.first, std::prev(goto_program.instructions.end()));
+      }
+    }
   }
 
   void initialize(const irep_idt &function, const goto_programt &goto_program)
@@ -238,6 +248,9 @@ class dependence_grapht:
     {
       cfg_post_dominatorst &pd = post_dominators[function];
       pd(goto_program);
+
+      end_function_map.emplace(
+        function, std::prev(goto_program.instructions.end()));
     }
   }
 
@@ -273,6 +286,7 @@ class dependence_grapht:
 
   post_dominators_mapt post_dominators;
   reaching_definitions_analysist rd;
+  std::map<irep_idt, goto_programt::const_targett> end_function_map;
 };
 
 #endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H

src/analyses/reaching_definitions.cpp

@@ -126,41 +126,6 @@ void rd_range_domaint::transform(
   // initial (non-deterministic) value
   else if(from->is_decl())
     transform_assign(ns, from, function_from, from, *rd);
-
-#if 0
-  // handle return values
-  if(to->is_function_call())
-  {
-    const code_function_callt &code=to_code_function_call(to->code);
-
-    if(code.lhs().is_not_nil())
-    {
-      rw_range_set_value_sett rw_set(ns, rd->get_value_sets());
-      goto_rw(to, rw_set);
-      const bool is_must_alias=rw_set.get_w_set().size()==1;
-
-      for(const auto &written_object_entry : rw_set.get_w_set())
-      {
-        const irep_idt &identifier = written_object_entry.first;
-        // ignore symex::invalid_object
-        const symbolt *symbol_ptr;
-        if(ns.lookup(identifier, symbol_ptr))
-          continue;
-        assert(symbol_ptr!=0);
-
-        const range_domaint &ranges =
-          rw_set.get_ranges(written_object_entry.second);
-
-        if(is_must_alias &&
-           (!rd->get_is_threaded()(from) ||
-            (!symbol_ptr->is_shared() &&
-             !rd->get_is_dirty()(identifier))))
-          for(const auto &range : ranges)
-            kill(identifier, range.first, range.second);
-      }
-    }
-  }
-#endif
 }
 
 /// Computes an instance obtained from a `*this` by transformation over `DEAD v`
@@ -322,12 +287,6 @@ void rd_range_domaint::transform_end_function(
   // handle return values
   if(call->call_lhs().is_not_nil())
   {
-#if 0
-    rd_range_domaint *rd_state=
-      dynamic_cast<rd_range_domaint*>(&(rd.get_state(call)));
-    assert(rd_state!=0);
-    rd_state->
-#endif
     transform_assign(ns, from, function_to, call, rd);
   }
 }