value_sets now have function identifiers

Daniel Kroening · Daniel Kroening · commit d0c7f41300f9 · 2018-10-09T18:09:35.000-04:00
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/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);
 }
diff --git a/src/analyses/flow_insensitive_analysis.h b/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);
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/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);
 }
diff --git a/src/pointer-analysis/goto_program_dereference.h b/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;
diff --git a/src/pointer-analysis/value_set_analysis.h b/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)
diff --git a/src/pointer-analysis/value_set_analysis_fi.h b/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);
diff --git a/src/pointer-analysis/value_set_analysis_fivr.h b/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);
diff --git a/src/pointer-analysis/value_set_analysis_fivrns.h b/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);
diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp
@@ -16,13 +16,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 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;
 
diff --git a/src/pointer-analysis/value_set_domain_fi.h b/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();
   }
diff --git a/src/pointer-analysis/value_set_domain_fivr.cpp b/src/pointer-analysis/value_set_domain_fivr.cpp
@@ -16,11 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bool value_set_domain_fivrt::transform(
   const namespacet &ns,
+  const irep_idt &function_from,
   locationt from_l,
+  const irep_idt &function_to,
   locationt to_l)
 {
-  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);
 
   #if 0
   std::cout << "Transforming: " <<
@@ -45,7 +47,7 @@ bool value_set_domain_fivrt::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;
     }
 
diff --git a/src/pointer-analysis/value_set_domain_fivr.h b/src/pointer-analysis/value_set_domain_fivr.h
@@ -24,33 +24,34 @@ class value_set_domain_fivrt:public flow_insensitive_abstract_domain_baset
 
   // overloading
 
-  virtual void output(
+  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();
   }
diff --git a/src/pointer-analysis/value_set_domain_fivrns.cpp b/src/pointer-analysis/value_set_domain_fivrns.cpp
diff --git a/src/pointer-analysis/value_set_domain_fivrns.h b/src/pointer-analysis/value_set_domain_fivrns.h
diff --git a/src/pointer-analysis/value_sets.h b/src/pointer-analysis/value_sets.h

Original file line number	Diff line number	Diff line change
`@@ -72,14 +72,14 @@ void flow_insensitive_analysis_baset::output(`
`72`	`72`	`{`
`73`	`73`	`out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";`
`74`	`74`
`75`		`- output(f_it->second.body, f_it->first, out);`
	`75`	`+ output(f_it->first, f_it->second.body, out);`
`76`	`76`	`}`
`77`	`77`	`}`
`78`	`78`
`79`	`79`	`void flow_insensitive_analysis_baset::output(`
`80`		`- const goto_programt &,`
`81`	`80`	`const irep_idt &,`
`82`		`- std::ostream &out) const`
	`81`	`+ const goto_programt &,`
	`82`	`+ std::ostream &out)`
`83`	`83`	`{`
`84`	`84`	`get_state().output(ns, out);`
`85`	`85`	`}`
Original file line number	Diff line number	Diff line change
`@@ -228,7 +228,7 @@ void goto_program_dereferencet::get_value_set(`
`228`	`228`	`const exprt &expr,`
`229`	`229`	`value_setst::valuest &dest)`
`230`	`230`	`{`
`231`		`- value_sets.get_values(current_target, expr, dest);`
	`231`	`+ value_sets.get_values(current_function, current_target, expr, dest);`
`232`	`232`	`}`
`233`	`233`
`234`	`234`	`void goto_program_dereferencet::dereference_expr(`
`@@ -348,9 +348,11 @@ void goto_program_dereferencet::dereference_instruction(`
`348`	`348`	`}`
`349`	`349`
`350`	`350`	`void goto_program_dereferencet::dereference_expression(`
	`351`	`+ const irep_idt &function_identifier,`
`351`	`352`	`goto_programt::const_targett target,`
`352`	`353`	`exprt &expr)`
`353`	`354`	`{`
	`355`	`+ current_function=function_identifier;`
`354`	`356`	`current_target=target;`
`355`	`357`	`#if 0`
`356`	`358`	`valid_local_variables=&target->local_variables;`
`@@ -427,6 +429,7 @@ void pointer_checks(`
`427`	`429`	`}`
`428`	`430`
`429`	`431`	`void dereference(`
	`432`	`+ const irep_idt &function_identifier,`
`430`	`433`	`goto_programt::const_targett target,`
`431`	`434`	`exprt &expr,`
`432`	`435`	`const namespacet &ns,`
`@@ -436,5 +439,5 @@ void dereference(`
`436`	`439`	`symbol_tablet new_symbol_table;`
`437`	`440`	`goto_program_dereferencet`
`438`	`441`	`goto_program_dereference(ns, new_symbol_table, options, value_sets);`
`439`		`- goto_program_dereference.dereference_expression(target, expr);`
	`442`	`+ goto_program_dereference.dereference_expression(function_identifier, target, expr);`
`440`	`443`	`}`
Original file line number	Diff line number	Diff line change
`@@ -31,30 +31,32 @@ class value_set_domain_fit:public flow_insensitive_abstract_domain_baset`
`31`	`31`
`32`	`32`	`virtual void output(`
`33`	`33`	`const namespacet &ns,`
`34`		`- std::ostream &out) const`
	`34`	`+ std::ostream &out) const override`
`35`	`35`	`{`
`36`	`36`	`value_set.output(ns, out);`
`37`	`37`	`}`
`38`	`38`
`39`		`- virtual void initialize(const namespacet &)`
	`39`	`+ void initialize(const namespacet &) override`
`40`	`40`	`{`
`41`	`41`	`value_set.clear();`
`42`	`42`	`}`
`43`	`43`
`44`		`- virtual bool transform(`
	`44`	`+ bool transform(`
`45`	`45`	`const namespacet &ns,`
	`46`	`+ const irep_idt &function_from,`
`46`	`47`	`locationt from_l,`
`47`		`- locationt to_l);`
	`48`	`+ const irep_idt &function_to,`
	`49`	`+ locationt to_l) override;`
`48`	`50`
`49`		`- virtual void get_reference_set(`
	`51`	`+ void get_reference_set(`
`50`	`52`	`const namespacet &ns,`
`51`	`53`	`const exprt &expr,`
`52`		`- expr_sett &expr_set)`
	`54`	`+ expr_sett &expr_set) override`
`53`	`55`	`{`
`54`	`56`	`value_set.get_reference_set(expr, expr_set, ns);`
`55`	`57`	`}`
`56`	`58`
`57`		`- virtual void clear(void)`
	`59`	`+ void clear(void) override`
`58`	`60`	`{`
`59`	`61`	`value_set.clear();`
`60`	`62`	`}`
Original file line number	Diff line number	Diff line change
`@@ -24,33 +24,34 @@ class value_set_domain_fivrt:public flow_insensitive_abstract_domain_baset`
`24`	`24`
`25`	`25`	`// overloading`
`26`	`26`
`27`		`- virtual void output(`
	`27`	`+ void output(`
`28`	`28`	`const namespacet &ns,`
`29`		`- std::ostream &out) const`
	`29`	`+ std::ostream &out) const override`
`30`	`30`	`{`
`31`	`31`	`value_set.output(ns, out);`
`32`	`32`	`}`
`33`	`33`
`34`		`- virtual void initialize(`
`35`		`- const namespacet &)`
	`34`	`+ void initialize(const namespacet &) override`
`36`	`35`	`{`
`37`	`36`	`value_set.clear();`
`38`	`37`	`}`
`39`	`38`
`40`		`- virtual bool transform(`
	`39`	`+ bool transform(`
`41`	`40`	`const namespacet &ns,`
	`41`	`+ const irep_idt &function_from,`
`42`	`42`	`locationt from_l,`
`43`		`- locationt to_l);`
	`43`	`+ const irep_idt &function_to,`
	`44`	`+ locationt to_l) override;`
`44`	`45`
`45`		`- virtual void get_reference_set(`
	`46`	`+ void get_reference_set(`
`46`	`47`	`const namespacet &ns,`
`47`	`48`	`const exprt &expr,`
`48`		`- expr_sett &expr_set)`
	`49`	`+ expr_sett &expr_set) override`
`49`	`50`	`{`
`50`	`51`	`value_set.get_reference_set(expr, expr_set, ns);`
`51`	`52`	`}`
`52`	`53`
`53`		`- virtual void clear(void)`
	`54`	`+ void clear(void) override`
`54`	`55`	`{`
`55`	`56`	`value_set.clear();`
`56`	`57`	`}`