value_sets now have function identifiers

Author: Daniel Kroening

src/analyses/flow_insensitive_analysis.cpp

@@ -56,14 +56,6 @@ void flow_insensitive_analysis_baset::operator()(
   fixedpoint(goto_functions);
 }
 
-void flow_insensitive_analysis_baset::operator()(
-  const goto_programt &goto_program)
-{
-  initialize(goto_program);
-  goto_functionst goto_functions;
-  fixedpoint(goto_program, goto_functions);
-}
-
 void flow_insensitive_analysis_baset::output(
   const goto_functionst &goto_functions,
   std::ostream &out)
@@ -72,14 +64,14 @@ void flow_insensitive_analysis_baset::output(
   {
     out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";
 
-    output(f_it->second.body, f_it->first, out);
+    output(f_it->first, f_it->second.body, out);
   }
 }
 
 void flow_insensitive_analysis_baset::output(
-  const goto_programt &,
   const irep_idt &,
-  std::ostream &out) const
+  const goto_programt &,
+  std::ostream &out)
 {
   get_state().output(ns, out);
 }
@@ -102,6 +94,7 @@ flow_insensitive_analysis_baset::get_next(
 }
 
 bool flow_insensitive_analysis_baset::fixedpoint(
+  const irep_idt &function_identifier,
   const goto_programt &goto_program,
   const goto_functionst &goto_functions)
 {
@@ -122,14 +115,15 @@ bool flow_insensitive_analysis_baset::fixedpoint(
   {
     locationt l=get_next(working_set);
 
-    if(visit(l, working_set, goto_program, goto_functions))
+    if(visit(function_identifier, l, working_set, goto_program, goto_functions))
       new_data=true;
   }
 
   return new_data;
 }
 
 bool flow_insensitive_analysis_baset::visit(
+  const irep_idt &function_identifier,
   locationt l,
   working_sett &working_set,
   const goto_programt &goto_program,
@@ -160,16 +154,17 @@ bool flow_insensitive_analysis_baset::visit(
       // this is a big special case
       const code_function_callt &code = to_code_function_call(l->code);
 
-      changed=
-        do_function_call_rec(
-          l,
-          code.function(),
-          code.arguments(),
-          get_state(),
-          goto_functions);
+      changed = do_function_call_rec(
+        function_identifier,
+        l,
+        code.function(),
+        code.arguments(),
+        get_state(),
+        goto_functions);
     }
     else
-      changed = get_state().transform(ns, l, to_l);
+      changed = get_state().transform(
+        ns, function_identifier, l, function_identifier, to_l);
 
     if(changed || !seen(to_l))
     {
@@ -196,6 +191,7 @@ bool flow_insensitive_analysis_baset::visit(
 }
 
 bool flow_insensitive_analysis_baset::do_function_call(
+  const irep_idt &calling_function,
   locationt l_call,
   const goto_functionst &goto_functions,
   const goto_functionst::function_mapt::const_iterator f_it,
@@ -225,9 +221,11 @@ bool flow_insensitive_analysis_baset::do_function_call(
     t->location_number=1;
 
     locationt l_next=l_call; l_next++;
-    bool new_data=state.transform(ns, l_call, r);
-    new_data = state.transform(ns, r, t) || new_data;
-    new_data = state.transform(ns, t, l_next) || new_data;
+    bool new_data =
+      state.transform(ns, calling_function, l_call, f_it->first, r);
+    new_data = state.transform(ns, f_it->first, r, f_it->first, t) || new_data;
+    new_data =
+      state.transform(ns, f_it->first, t, calling_function, l_next) || new_data;
 
     return new_data;
   }
@@ -244,7 +242,8 @@ bool flow_insensitive_analysis_baset::do_function_call(
       l_begin->function == f_it->first, "function names have to match");
 
     // do the edge from the call site to the beginning of the function
-    new_data=state.transform(ns, l_call, l_begin);
+    new_data =
+      state.transform(ns, calling_function, l_call, f_it->first, l_begin);
 
     // do each function at least once
     if(functions_done.find(f_it->first)==
@@ -258,7 +257,7 @@ bool flow_insensitive_analysis_baset::do_function_call(
     if(new_data)
     {
       // recursive call
-      fixedpoint(goto_function.body, goto_functions);
+      fixedpoint(f_it->first, goto_function.body, goto_functions);
       new_data=true; // could be reset by fixedpoint
     }
   }
@@ -272,13 +271,16 @@ bool flow_insensitive_analysis_baset::do_function_call(
     // do edge from end of function to instruction after call
     locationt l_next=l_call;
     l_next++;
-    new_data = state.transform(ns, l_end, l_next) || new_data;
+    new_data =
+      state.transform(ns, f_it->first, l_end, calling_function, l_next) ||
+      new_data;
   }
 
   return new_data;
 }
 
 bool flow_insensitive_analysis_baset::do_function_call_rec(
+  const irep_idt &calling_function,
   locationt l_call,
   const exprt &function,
   const exprt::operandst &arguments,
@@ -305,13 +307,8 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
     if(it==goto_functions.function_map.end())
       throw "failed to find function "+id2string(identifier);
 
-    new_data =
-      do_function_call(
-        l_call,
-        goto_functions,
-        it,
-        arguments,
-        state);
+    new_data = do_function_call(
+      calling_function, l_call, goto_functions, it, arguments, state);
 
     recursion_set.erase(identifier);
   }
@@ -320,21 +317,22 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
     if(function.operands().size()!=3)
       throw "if takes three arguments";
 
-    new_data =
-      do_function_call_rec(
-        l_call,
-        function.op1(),
-        arguments,
-        state,
-        goto_functions);
-
-    new_data =
-      do_function_call_rec(
-        l_call,
-        function.op2(),
-        arguments,
-        state,
-        goto_functions) || new_data;
+    new_data = do_function_call_rec(
+      calling_function,
+      l_call,
+      function.op1(),
+      arguments,
+      state,
+      goto_functions);
+
+    new_data = do_function_call_rec(
+                 calling_function,
+                 l_call,
+                 function.op2(),
+                 arguments,
+                 state,
+                 goto_functions) ||
+               new_data;
   }
   else if(function.id()==ID_dereference)
   {
@@ -356,13 +354,14 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
 
         if(it!=goto_functions.function_map.end())
         {
-          new_data =
-            do_function_call_rec(
-              l_call,
-              o.object(),
-              arguments,
-              state,
-              goto_functions) || new_data;
+          new_data = do_function_call_rec(
+                       calling_function,
+                       l_call,
+                       o.object(),
+                       arguments,
+                       state,
+                       goto_functions) ||
+                     new_data;
         }
       }
     }
@@ -405,7 +404,7 @@ bool flow_insensitive_analysis_baset::fixedpoint(
   const goto_functionst &goto_functions)
 {
   functions_done.insert(it->first);
-  return fixedpoint(it->second.body, goto_functions);
+  return fixedpoint(it->first, it->second.body, goto_functions);
 }
 
 void flow_insensitive_analysis_baset::update(const goto_functionst &)

src/analyses/flow_insensitive_analysis.h

@@ -47,8 +47,10 @@ class flow_insensitive_abstract_domain_baset
 
   virtual bool transform(
     const namespacet &ns,
+    const irep_idt &function_from,
     locationt from,
-    locationt to)=0;
+    const irep_idt &function_to,
+    locationt to) = 0;
 
   virtual ~flow_insensitive_abstract_domain_baset()
   {
@@ -146,20 +148,13 @@ class flow_insensitive_analysis_baset
     std::ostream &out);
 
   virtual void output(
+    const irep_idt &function_identifier,
     const goto_programt &goto_program,
-    std::ostream &out)
-  {
-    output(goto_program, "", out);
-  }
+    std::ostream &out);
 
 protected:
   const namespacet &ns;
 
-  virtual void output(
-    const goto_programt &goto_program,
-    const irep_idt &identifier,
-    std::ostream &out) const;
-
   typedef std::priority_queue<locationt> working_sett;
 
   locationt get_next(working_sett &working_set);
@@ -173,6 +168,7 @@ class flow_insensitive_analysis_baset
 
   // true = found something new
   bool fixedpoint(
+    const irep_idt &function_identifier,
     const goto_programt &goto_program,
     const goto_functionst &goto_functions);
 
@@ -185,6 +181,7 @@ class flow_insensitive_analysis_baset
 
   // true = found something new
   bool visit(
+    const irep_idt &function_identifier,
     locationt l,
     working_sett &working_set,
     const goto_programt &goto_program,
@@ -206,13 +203,15 @@ class flow_insensitive_analysis_baset
 
   // function calls
   bool do_function_call_rec(
+    const irep_idt &calling_function,
     locationt l_call,
     const exprt &function,
     const exprt::operandst &arguments,
     statet &new_state,
     const goto_functionst &goto_functions);
 
   bool do_function_call(
+    const irep_idt &calling_function,
     locationt l_call,
     const goto_functionst &goto_functions,
     const goto_functionst::function_mapt::const_iterator f_it,

src/goto-symex/precondition.cpp

@@ -113,7 +113,8 @@ void preconditiont::compute_rec(exprt &dest)
     // aliasing may happen here
 
     value_setst::valuest expr_set;
-    value_sets.get_values(target, deref_expr.pointer(), expr_set);
+    value_sets.get_values(
+      SSA_step.source.function, target, deref_expr.pointer(), expr_set);
     std::unordered_set<irep_idt> symbols;
 
     for(value_setst::valuest::const_iterator

src/pointer-analysis/goto_program_dereference.cpp

@@ -228,7 +228,7 @@ void goto_program_dereferencet::get_value_set(
   const exprt &expr,
   value_setst::valuest &dest)
 {
-  value_sets.get_values(current_target, expr, dest);
+  value_sets.get_values(current_function, current_target, expr, dest);
 }
 
 void goto_program_dereferencet::dereference_expr(
@@ -348,9 +348,11 @@ void goto_program_dereferencet::dereference_instruction(
 }
 
 void goto_program_dereferencet::dereference_expression(
+  const irep_idt &function_identifier,
   goto_programt::const_targett target,
   exprt &expr)
 {
+  current_function = function_identifier;
   current_target=target;
   #if 0
   valid_local_variables=&target->local_variables;
@@ -427,6 +429,7 @@ void pointer_checks(
 }
 
 void dereference(
+  const irep_idt &function_identifier,
   goto_programt::const_targett target,
   exprt &expr,
   const namespacet &ns,
@@ -436,5 +439,6 @@ void dereference(
   symbol_tablet new_symbol_table;
   goto_program_dereferencet
     goto_program_dereference(ns, new_symbol_table, options, value_sets);
-  goto_program_dereference.dereference_expression(target, expr);
+  goto_program_dereference.dereference_expression(
+    function_identifier, target, expr);
 }

src/pointer-analysis/goto_program_dereference.h

@@ -50,6 +50,7 @@ class goto_program_dereferencet:protected dereference_callbackt
   void pointer_checks(goto_functionst &goto_functions);
 
   void dereference_expression(
+    const irep_idt &function,
     goto_programt::const_targett target,
     exprt &expr);
 
@@ -92,6 +93,7 @@ class goto_program_dereferencet:protected dereference_callbackt
   const std::set<irep_idt> *valid_local_variables;
 #endif
   source_locationt dereference_location;
+  irep_idt current_function;
   goto_programt::const_targett current_target;
 
   std::set<exprt> assertions;

src/pointer-analysis/value_set_analysis.h

@@ -59,6 +59,7 @@ class value_set_analysis_templatet:
 public:
   // interface value_sets
   virtual void get_values(
+    const irep_idt &function_identifier,
     locationt l,
     const exprt &expr,
     value_setst::valuest &dest)

src/pointer-analysis/value_set_analysis_fi.h

@@ -35,8 +35,8 @@ class value_set_analysis_fit:
 
   typedef flow_insensitive_analysist<value_set_domain_fit> baset;
 
-  virtual void initialize(const goto_programt &goto_program);
-  virtual void initialize(const goto_functionst &goto_functions);
+  void initialize(const goto_programt &goto_program) override;
+  void initialize(const goto_functionst &goto_functions) override;
 
 protected:
   track_optionst track_options;
@@ -58,15 +58,16 @@ class value_set_analysis_fit:
 
 public:
   // interface value_sets
-  virtual void get_values(
+  void get_values(
+    const irep_idt &function_identifier,
     locationt l,
     const exprt &expr,
-    std::list<exprt> &dest)
+    std::list<exprt> &dest) override
   {
     state.value_set.from_function =
-      state.value_set.function_numbering.number(l->function);
+      state.value_set.function_numbering.number(function_identifier);
     state.value_set.to_function =
-      state.value_set.function_numbering.number(l->function);
+      state.value_set.function_numbering.number(function_identifier);
     state.value_set.from_target_index = l->location_number;
     state.value_set.to_target_index = l->location_number;
     state.value_set.get_value_set(expr, dest, ns);