Merge pull request #3843 from tautschnig/function-goto_rw

goto_rw: store function name alongside instruction reference [blocks: #3126]

Author: tautschnig

src/analyses/dependence_graph.cpp

@@ -162,7 +162,7 @@ void dep_graph_domaint::data_dependencies(
   value_setst &value_sets=
     dep_graph.reaching_definitions().get_value_sets();
   rw_range_set_value_sett rw_set(ns, value_sets);
-  goto_rw(to, rw_set);
+  goto_rw(to->function, to, rw_set);
 
   forall_rw_range_set_r_objects(it, rw_set)
   {

src/analyses/goto_rw.cpp

@@ -717,35 +717,40 @@ void rw_guarded_range_set_value_sett::add(
     {range_start, {range_end, guard.as_expr()}});
 }
 
-void goto_rw(goto_programt::const_targett target,
-             const code_assignt &assign,
-             rw_range_sett &rw_set)
+static void goto_rw(
+  const irep_idt &function,
+  goto_programt::const_targett target,
+  const code_assignt &assign,
+  rw_range_sett &rw_set)
 {
-  rw_set.get_objects_rec(target, rw_range_sett::get_modet::LHS_W, assign.lhs());
-  rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, assign.rhs());
+  rw_set.get_objects_rec(
+    function, target, rw_range_sett::get_modet::LHS_W, assign.lhs());
+  rw_set.get_objects_rec(
+    function, target, rw_range_sett::get_modet::READ, assign.rhs());
 }
 
-void goto_rw(goto_programt::const_targett target,
-             const code_function_callt &function_call,
-             rw_range_sett &rw_set)
+static void goto_rw(
+  const irep_idt &function,
+  goto_programt::const_targett target,
+  const code_function_callt &function_call,
+  rw_range_sett &rw_set)
 {
   if(function_call.lhs().is_not_nil())
     rw_set.get_objects_rec(
-      target,
-      rw_range_sett::get_modet::LHS_W,
-      function_call.lhs());
+      function, target, rw_range_sett::get_modet::LHS_W, function_call.lhs());
 
   rw_set.get_objects_rec(
-    target,
-    rw_range_sett::get_modet::READ,
-    function_call.function());
+    function, target, rw_range_sett::get_modet::READ, function_call.function());
 
   forall_expr(it, function_call.arguments())
-    rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, *it);
+    rw_set.get_objects_rec(
+      function, target, rw_range_sett::get_modet::READ, *it);
 }
 
-void goto_rw(goto_programt::const_targett target,
-             rw_range_sett &rw_set)
+void goto_rw(
+  const irep_idt &function,
+  goto_programt::const_targett target,
+  rw_range_sett &rw_set)
 {
   switch(target->type)
   {
@@ -758,9 +763,7 @@ void goto_rw(goto_programt::const_targett target,
   case ASSUME:
   case ASSERT:
     rw_set.get_objects_rec(
-      target,
-      rw_range_sett::get_modet::READ,
-      target->guard);
+      function, target, rw_range_sett::get_modet::READ, target->guard);
     break;
 
   case RETURN:
@@ -769,6 +772,7 @@ void goto_rw(goto_programt::const_targett target,
         to_code_return(target->code);
       if(code_return.has_return_value())
         rw_set.get_objects_rec(
+          function,
           target,
           rw_range_sett::get_modet::READ,
           code_return.return_value());
@@ -780,7 +784,8 @@ void goto_rw(goto_programt::const_targett target,
     if(target->code.get(ID_statement)==ID_printf)
     {
       forall_expr(it, target->code.operands())
-        rw_set.get_objects_rec(target, rw_range_sett::get_modet::READ, *it);
+        rw_set.get_objects_rec(
+          function, target, rw_range_sett::get_modet::READ, *it);
     }
     break;
 
@@ -797,35 +802,40 @@ void goto_rw(goto_programt::const_targett target,
     break;
 
   case ASSIGN:
-    goto_rw(target, to_code_assign(target->code), rw_set);
+    goto_rw(function, target, to_code_assign(target->code), rw_set);
     break;
 
   case DEAD:
     rw_set.get_objects_rec(
+      function,
       target,
       rw_range_sett::get_modet::LHS_W,
       to_code_dead(target->code).symbol());
     break;
 
   case DECL:
     rw_set.get_objects_rec(
-      to_code_decl(target->code).symbol().type());
+      function, target, to_code_decl(target->code).symbol().type());
     rw_set.get_objects_rec(
+      function,
       target,
       rw_range_sett::get_modet::LHS_W,
       to_code_decl(target->code).symbol());
     break;
 
   case FUNCTION_CALL:
-    goto_rw(target, to_code_function_call(target->code), rw_set);
+    goto_rw(function, target, to_code_function_call(target->code), rw_set);
     break;
   }
 }
 
-void goto_rw(const goto_programt &goto_program, rw_range_sett &rw_set)
+void goto_rw(
+  const irep_idt &function,
+  const goto_programt &goto_program,
+  rw_range_sett &rw_set)
 {
   forall_goto_program_instructions(i_it, goto_program)
-    goto_rw(i_it, rw_set);
+    goto_rw(function, i_it, rw_set);
 }
 
 void goto_rw(const goto_functionst &goto_functions,
@@ -839,6 +849,6 @@ void goto_rw(const goto_functionst &goto_functions,
   {
     const goto_programt &body=f_it->second.body;
 
-    goto_rw(body, rw_set);
+    goto_rw(f_it->first, body, rw_set);
   }
 }

src/analyses/goto_rw.h

@@ -32,11 +32,15 @@ Date: April 2010
 class rw_range_sett;
 class goto_modelt;
 
-void goto_rw(goto_programt::const_targett target,
-             rw_range_sett &rw_set);
+void goto_rw(
+  const irep_idt &function,
+  goto_programt::const_targett target,
+  rw_range_sett &rw_set);
 
-void goto_rw(const goto_programt &,
-             rw_range_sett &rw_set);
+void goto_rw(
+  const irep_idt &function,
+  const goto_programt &,
+  rw_range_sett &rw_set);
 
 void goto_rw(const goto_functionst &,
              const irep_idt &function,
@@ -141,14 +145,21 @@ class rw_range_sett
   enum class get_modet { LHS_W, READ };
 
   virtual void get_objects_rec(
+    const irep_idt &,
     goto_programt::const_targett,
     get_modet mode,
     const exprt &expr)
   {
     get_objects_rec(mode, expr);
   }
 
-  virtual void get_objects_rec(const typet &type);
+  virtual void get_objects_rec(
+    const irep_idt &,
+    goto_programt::const_targett,
+    const typet &type)
+  {
+    get_objects_rec(type);
+  }
 
   void output(std::ostream &out) const;
 
@@ -161,6 +172,8 @@ class rw_range_sett
     get_modet mode,
     const exprt &expr);
 
+  virtual void get_objects_rec(const typet &type);
+
   virtual void get_objects_complex_real(
     get_modet mode,
     const complex_real_exprt &expr,
@@ -265,28 +278,41 @@ class rw_range_set_value_sett:public rw_range_sett
   {
   }
 
-  using rw_range_sett::get_objects_rec;
-
-  virtual void get_objects_rec(
+  void get_objects_rec(
+    const irep_idt &_function,
     goto_programt::const_targett _target,
     get_modet mode,
-    const exprt &expr)
+    const exprt &expr) override
   {
+    function = _function;
     target=_target;
 
     rw_range_sett::get_objects_rec(mode, expr);
   }
 
+  void get_objects_rec(
+    const irep_idt &_function,
+    goto_programt::const_targett _target,
+    const typet &type) override
+  {
+    function = _function;
+    target = _target;
+
+    rw_range_sett::get_objects_rec(type);
+  }
+
 protected:
   value_setst &value_sets;
-
+  irep_idt function;
   goto_programt::const_targett target;
 
-  virtual void get_objects_dereference(
+  using rw_range_sett::get_objects_rec;
+
+  void get_objects_dereference(
     get_modet mode,
     const dereference_exprt &deref,
     const range_spect &range_start,
-    const range_spect &size);
+    const range_spect &size) override;
 };
 
 class guarded_range_domaint:public range_domain_baset
@@ -338,32 +364,41 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
     return static_cast<const guarded_range_domaint &>(*it->second);
   }
 
-  virtual void get_objects_rec(
+  void get_objects_rec(
+    const irep_idt &_function,
     goto_programt::const_targett _target,
     get_modet mode,
-    const exprt &expr)
+    const exprt &expr) override
   {
     guard = true_exprt();
 
-    rw_range_set_value_sett::get_objects_rec(_target, mode, expr);
+    rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);
+  }
+
+  void get_objects_rec(
+    const irep_idt &function,
+    goto_programt::const_targett target,
+    const typet &type) override
+  {
+    rw_range_sett::get_objects_rec(function, target, type);
   }
 
 protected:
   guardt guard;
 
   using rw_range_sett::get_objects_rec;
 
-  virtual void get_objects_if(
+  void get_objects_if(
     get_modet mode,
     const if_exprt &if_expr,
     const range_spect &range_start,
-    const range_spect &size);
+    const range_spect &size) override;
 
-  virtual void add(
+  void add(
     get_modet mode,
     const irep_idt &identifier,
     const range_spect &range_start,
-    const range_spect &range_end);
+    const range_spect &range_end) override;
 };
 
 #endif // CPROVER_ANALYSES_GOTO_RW_H

src/analyses/reaching_definitions.cpp

@@ -91,13 +91,13 @@ void rd_range_domaint::transform(
     transform_function_call(ns, function_from, from, function_to, *rd);
   // cleanup parameters
   else if(from->is_end_function())
-    transform_end_function(ns, function_from, from, to, *rd);
+    transform_end_function(ns, function_from, from, function_to, to, *rd);
   // lhs assignments
   else if(from->is_assign())
-    transform_assign(ns, from, from, *rd);
+    transform_assign(ns, from, function_from, from, *rd);
   // initial (non-deterministic) value
   else if(from->is_decl())
-    transform_assign(ns, from, from, *rd);
+    transform_assign(ns, from, function_from, from, *rd);
 
 #if 0
   // handle return values
@@ -233,14 +233,15 @@ void rd_range_domaint::transform_function_call(
   {
     // handle return values of undefined functions
     if(to_code_function_call(from->code).lhs().is_not_nil())
-      transform_assign(ns, from, from, rd);
+      transform_assign(ns, from, function_from, from, rd);
   }
 }
 
 void rd_range_domaint::transform_end_function(
   const namespacet &ns,
   const irep_idt &function_from,
   locationt from,
+  const irep_idt &function_to,
   locationt to,
   reaching_definitions_analysist &rd)
 {
@@ -301,18 +302,19 @@ void rd_range_domaint::transform_end_function(
     assert(rd_state!=0);
     rd_state->
 #endif
-      transform_assign(ns, from, call, rd);
+    transform_assign(ns, from, function_to, call, rd);
   }
 }
 
 void rd_range_domaint::transform_assign(
   const namespacet &ns,
   locationt from,
+  const irep_idt &function_to,
   locationt to,
   reaching_definitions_analysist &rd)
 {
   rw_range_set_value_sett rw_set(ns, rd.get_value_sets());
-  goto_rw(to, rw_set);
+  goto_rw(function_to, to, rw_set);
   const bool is_must_alias=rw_set.get_w_set().size()==1;
 
   forall_rw_range_set_w_objects(it, rw_set)

src/analyses/reaching_definitions.h

@@ -309,11 +309,13 @@ class rd_range_domaint:public ai_domain_baset
     const namespacet &ns,
     const irep_idt &function_from,
     locationt from,
+    const irep_idt &function_to,
     locationt to,
     reaching_definitions_analysist &rd);
   void transform_assign(
     const namespacet &ns,
     locationt from,
+    const irep_idt &function_to,
     locationt to,
     reaching_definitions_analysist &rd);