value_sets now have function identifiers

Author: kroening

src/analyses/flow_insensitive_analysis.cpp

@@ -72,14 +72,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);
 }

src/analyses/flow_insensitive_analysis.h

@@ -47,7 +47,9 @@ class flow_insensitive_abstract_domain_baset
 
   virtual bool transform(
     const namespacet &ns,
+    const irep_idt &function_from,
     locationt from,
+    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);

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,5 @@ 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);

src/pointer-analysis/value_set_analysis_fivr.h

@@ -35,25 +35,31 @@ class value_set_analysis_fivrt:
 
   typedef flow_insensitive_analysist<value_set_domain_fivrt> 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;
 
   using baset::output;
-  void output(locationt l, std::ostream &out)
+  void output(
+    const irep_idt &function_identifier,
+    locationt l,
+    std::ostream &out)
   {
-    state.value_set.set_from(l->function, l->location_number);
-    state.value_set.set_to(l->function, l->location_number);
+    state.value_set.set_from(function_identifier, l->location_number);
+    state.value_set.set_to(function_identifier, l->location_number);
     state.output(ns, out);
   }
 
-  void output(const goto_programt &goto_program, std::ostream &out)
+  void output(
+    const irep_idt &function_identifier,
+    const goto_programt &goto_program,
+    std::ostream &out) override
   {
     forall_goto_program_instructions(it, goto_program)
     {
       out << "**** " << it->source_location << '\n';
-      output(it, out);
+      output(function_identifier, it, out);
       out << '\n';
-      goto_program.output_instruction(ns, "", out, *it);
+      goto_program.output_instruction(ns, function_identifier, out, *it);
       out << '\n';
     }
   }
@@ -78,15 +84,16 @@ class value_set_analysis_fivrt:
 
 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);

src/pointer-analysis/value_set_analysis_fivrns.h

@@ -41,21 +41,27 @@ class value_set_analysis_fivrnst:
 
   using baset::output;
 
-  virtual void output(locationt l, std::ostream &out)
+  void output(
+    const irep_idt &function_identifier,
+    locationt l,
+    std::ostream &out)
   {
-    state.value_set.set_from(l->function, l->location_number);
-    state.value_set.set_to(l->function, l->location_number);
+    state.value_set.set_from(function_identifier, l->location_number);
+    state.value_set.set_to(function_identifier, l->location_number);
     state.output(ns, out);
   }
 
-  void output(const goto_programt &goto_program, std::ostream &out)
+  void output(
+    const irep_idt &function_identifier,
+    const goto_programt &goto_program,
+    std::ostream &out)
   {
     forall_goto_program_instructions(it, goto_program)
     {
       out << "**** " << it->source_location << '\n';
-      output(it, out);
+      output(function_identifier, it, out);
       out << '\n';
-      goto_program.output_instruction(ns, "", out, *it);
+      goto_program.output_instruction(ns, function_identifier, out, *it);
       out << '\n';
     }
   }
@@ -81,14 +87,15 @@ class value_set_analysis_fivrnst:
 public:
   // interface value_sets
   virtual void get_values(
+    const irep_idt &function_identifier,
     locationt l,
     const exprt &expr,
     std::list<exprt> &dest)
   {
     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);

src/pointer-analysis/value_set_domain_fi.cpp

@@ -16,13 +16,15 @@ Author: Daniel Kroening, [email protected]
 
 bool value_set_domain_fit::transform(
   const namespacet &ns,
+  const irep_idt &function_from,
   locationt from_l,
+  const irep_idt &function_to,
   locationt to_l)
 {
   value_set.changed = false;
 
-  value_set.set_from(from_l->function, from_l->location_number);
-  value_set.set_to(to_l->function, to_l->location_number);
+  value_set.set_from(function_from, from_l->location_number);
+  value_set.set_to(function_to, to_l->location_number);
 
 //  std::cout << "transforming: " <<
 //      from_l->function << " " << from_l->location_number << " to " <<
@@ -49,7 +51,7 @@ bool value_set_domain_fit::transform(
       const code_function_callt &code=
         to_code_function_call(from_l->code);
 
-      value_set.do_function_call(to_l->function, code.arguments(), ns);
+      value_set.do_function_call(function_to, code.arguments(), ns);
     }
     break;
 

src/pointer-analysis/value_set_domain_fi.h

@@ -31,30 +31,32 @@ class value_set_domain_fit:public flow_insensitive_abstract_domain_baset
 
   virtual void output(
     const namespacet &ns,
-    std::ostream &out) const
+    std::ostream &out) const override
   {
     value_set.output(ns, out);
   }
 
-  virtual void initialize(const namespacet &)
+  void initialize(const namespacet &) override
   {
     value_set.clear();
   }
 
-  virtual bool transform(
+  bool transform(
     const namespacet &ns,
+    const irep_idt &function_from,
     locationt from_l,
-    locationt to_l);
+    const irep_idt &function_to,
+    locationt to_l) override;
 
-  virtual void get_reference_set(
+  void get_reference_set(
     const namespacet &ns,
     const exprt &expr,
-    expr_sett &expr_set)
+    expr_sett &expr_set) override
   {
     value_set.get_reference_set(expr, expr_set, ns);
   }
 
-  virtual void clear(void)
+  void clear(void) override
   {
     value_set.clear();
   }