More precise control-flow graph using the simplifier

src/analyses/ai.cpp

@@ -367,7 +367,7 @@ bool ai_baset::visit(
 
       new_values.transform(l, to_l, *this, ns);
 
-      if(merge(new_values, l, to_l))
+      if(merge(new_values, l, to_l, ns))
         have_new_values=true;
     }
 
@@ -400,7 +400,7 @@ bool ai_baset::do_function_call(
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
     tmp_state->transform(l_call, l_return, *this, ns);
 
-    return merge(*tmp_state, l_call, l_return);
+    return merge(*tmp_state, l_call, l_return, ns);
   }
 
   assert(!goto_function.body.instructions.empty());
@@ -420,7 +420,7 @@ bool ai_baset::do_function_call(
     bool new_data=false;
 
     // merge the new stuff
-    if(merge(*tmp_state, l_call, l_begin))
+    if(merge(*tmp_state, l_call, l_begin, ns))
       new_data=true;
 
     // do we need to do/re-do the fixedpoint of the body?
@@ -445,7 +445,7 @@ bool ai_baset::do_function_call(
     tmp_state->transform(l_end, l_return, *this, ns);
 
     // Propagate those
-    return merge(*tmp_state, l_end, l_return);
+    return merge(*tmp_state, l_end, l_return, ns);
   }
 }
 
@@ -581,7 +581,7 @@ void ai_baset::concurrent_fixedpoint(
       put_in_working_set(working_set, wl_pair.second);
 
       statet &begin_state=get_state(wl_pair.second);
-      merge(begin_state, sh_target, wl_pair.second);
+      merge(begin_state, sh_target, wl_pair.second, ns);
 
       while(!working_set.empty())
       {

src/analyses/ai.h

@@ -360,7 +360,11 @@ class ai_baset
 
   // abstract methods
 
-  virtual bool merge(const statet &src, locationt from, locationt to)=0;
+  virtual bool merge(
+    const statet &src,
+    locationt from,
+    locationt to,
+    const namespacet &ns)=0;
   // for concurrent fixedpoint
   virtual bool merge_shared(
     const statet &src,
@@ -436,11 +440,15 @@ class ait:public ai_baset
     return it->second;
   }
 
-  bool merge(const statet &src, locationt from, locationt to) override
+  virtual bool merge(
+    const statet &src,
+    locationt from,
+    locationt to,
+    const namespacet &ns) override
   {
     statet &dest=get_state(to);
     return static_cast<domainT &>(dest).merge(
-      static_cast<const domainT &>(src), from, to);
+      static_cast<const domainT &>(src), from, to, ns);
   }
 
   std::unique_ptr<statet> make_temporary_state(const statet &s) override

src/analyses/cfg_dominators.h

@@ -22,18 +22,22 @@ Author: Georg Weissenbacher, [email protected]
 #include <goto-programs/goto_program.h>
 #include <goto-programs/cfg.h>
 
-template <class P, class T, bool post_dom>
+template <class P, class T, bool post_dom, bool syntactic=false>
 class cfg_dominators_templatet
 {
 public:
+  explicit cfg_dominators_templatet(const namespacet &ns):cfg(ns)
+  {
+  }
+
   typedef std::set<T> target_sett;
 
   struct nodet
   {
     target_sett dominators;
   };
 
-  typedef procedure_local_cfg_baset<nodet, P, T> cfgt;
+  typedef procedure_local_cfg_baset<nodet, P, T, !syntactic> cfgt;
   cfgt cfg;
 
   void operator()(P &program);
@@ -48,33 +52,36 @@ class cfg_dominators_templatet
 };
 
 /// Print the result of the dominator computation
-template <class P, class T, bool post_dom>
+template <class P, class T, bool post_dom, bool syntactic>
 std::ostream &operator << (
   std::ostream &out,
-  const cfg_dominators_templatet<P, T, post_dom> &cfg_dominators)
+  const cfg_dominators_templatet<P, T, post_dom, syntactic> &cfg_dominators)
 {
   cfg_dominators.output(out);
   return out;
 }
 
 /// Compute dominators
-template <class P, class T, bool post_dom>
-void cfg_dominators_templatet<P, T, post_dom>::operator()(P &program)
+template <class P, class T, bool post_dom, bool syntactic>
+void cfg_dominators_templatet<P, T, post_dom, syntactic>::operator()(
+  P &program)
 {
   initialise(program);
   fixedpoint(program);
 }
 
 /// Initialises the elements of the fixed point analysis
-template <class P, class T, bool post_dom>
-void cfg_dominators_templatet<P, T, post_dom>::initialise(P &program)
+template <class P, class T, bool post_dom, bool syntactic>
+void cfg_dominators_templatet<P, T, post_dom, syntactic>::initialise(
+  P &program)
 {
   cfg(program);
 }
 
 /// Computes the MOP for the dominator analysis
-template <class P, class T, bool post_dom>
-void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
+template <class P, class T, bool post_dom, bool syntactic>
+void cfg_dominators_templatet<P, T, post_dom, syntactic>::fixedpoint(
+  P &program)
 {
   std::list<T> worklist;
 
@@ -181,8 +188,9 @@ inline void dominators_pretty_print_node(
 }
 
 /// Print the result of the dominator computation
-template <class P, class T, bool post_dom>
-void cfg_dominators_templatet<P, T, post_dom>::output(std::ostream &out) const
+template <class P, class T, bool post_dom, bool syntactic>
+void cfg_dominators_templatet<P, T, post_dom, syntactic>::output(
+  std::ostream &out) const
 {
   for(const auto &node : cfg.entry_map)
   {
@@ -206,11 +214,11 @@ void cfg_dominators_templatet<P, T, post_dom>::output(std::ostream &out) const
 }
 
 typedef cfg_dominators_templatet<
-          const goto_programt, goto_programt::const_targett, false>
+          const goto_programt, goto_programt::const_targett, false, false>
         cfg_dominatorst;
 
 typedef cfg_dominators_templatet<
-          const goto_programt, goto_programt::const_targett, true>
+          const goto_programt, goto_programt::const_targett, true, false>
         cfg_post_dominatorst;
 
 template<>

src/analyses/constant_propagator.cpp

@@ -498,7 +498,8 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src)
 bool constant_propagator_domaint::merge(
   const constant_propagator_domaint &other,
   locationt from,
-  locationt to)
+  locationt to,
+  const namespacet &ns)
 {
   return values.merge(other.values);
 }

src/analyses/constant_propagator.h

@@ -25,7 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset
     locationt from,
     locationt to,
     ai_baset &ai_base,
-    const namespacet &ns) final override;
+    const namespacet &ns) override;
 
   virtual void output(
     std::ostream &out,
@@ -35,7 +35,8 @@ class constant_propagator_domaint:public ai_domain_baset
   bool merge(
     const constant_propagator_domaint &other,
     locationt from,
-    locationt to);
+    locationt to,
+    const namespacet &);
 
   virtual bool ai_simplify(
     exprt &condition,

src/analyses/custom_bitvector_analysis.cpp

@@ -590,7 +590,8 @@ void custom_bitvector_domaint::output(
 bool custom_bitvector_domaint::merge(
   const custom_bitvector_domaint &b,
   locationt from,
-  locationt to)
+  locationt to,
+  const namespacet &ns)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();

src/analyses/custom_bitvector_analysis.h

@@ -70,7 +70,8 @@ class custom_bitvector_domaint:public ai_domain_baset
   bool merge(
     const custom_bitvector_domaint &b,
     locationt from,
-    locationt to);
+    locationt to,
+    const namespacet &ns);
 
   typedef unsigned long long bit_vectort;
 

src/analyses/dependence_graph.cpp

@@ -24,7 +24,8 @@ Date: August 2013
 bool dep_graph_domaint::merge(
   const dep_graph_domaint &src,
   goto_programt::const_targett from,
-  goto_programt::const_targett to)
+  goto_programt::const_targett to,
+  const namespacet &ns)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();

src/analyses/dependence_graph.h

@@ -77,7 +77,8 @@ class dep_graph_domaint:public ai_domain_baset
   bool merge(
     const dep_graph_domaint &src,
     goto_programt::const_targett from,
-    goto_programt::const_targett to);
+    goto_programt::const_targett to,
+    const namespacet &ns);
 
   void transform(
     goto_programt::const_targett from,
@@ -210,7 +211,8 @@ class dependence_grapht:
     if(!goto_program.empty())
     {
       const irep_idt id=goto_programt::get_function_id(goto_program);
-      cfg_post_dominatorst &pd=post_dominators[id];
+      cfg_post_dominatorst &pd=
+        post_dominators.insert({id, cfg_post_dominatorst(ns)}).first->second;
       pd(goto_program);
     }
   }

src/analyses/escape_analysis.cpp

@@ -302,7 +302,8 @@ void escape_domaint::output(
 bool escape_domaint::merge(
   const escape_domaint &b,
   locationt from,
-  locationt to)
+  locationt to,
+  const namespacet &ns)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();

src/analyses/escape_analysis.h

@@ -40,7 +40,8 @@ class escape_domaint:public ai_domain_baset
   bool merge(
     const escape_domaint &b,
     locationt from,
-    locationt to);
+    locationt to,
+    const namespacet &ns);
 
   void make_bottom() final override
   {

src/analyses/global_may_alias.cpp

@@ -159,7 +159,8 @@ void global_may_alias_domaint::output(
 bool global_may_alias_domaint::merge(
   const global_may_alias_domaint &b,
   locationt from,
-  locationt to)
+  locationt to,
+  const namespacet &ns)
 {
   bool changed=has_values.is_false();
   has_values=tvt::unknown();

src/analyses/global_may_alias.h

@@ -40,7 +40,8 @@ class global_may_alias_domaint:public ai_domain_baset
   bool merge(
     const global_may_alias_domaint &b,
     locationt from,
-    locationt to);
+    locationt to,
+    const namespacet &ns);
 
   void make_bottom() final override
   {

src/analyses/interval_domain.h

@@ -48,7 +48,8 @@ class interval_domaint:public ai_domain_baset
   bool merge(
     const interval_domaint &b,
     locationt from,
-    locationt to)
+    locationt to,
+    const namespacet &ns)
   {
     return join(b);
   }

src/analyses/invariant_set_domain.h

@@ -32,7 +32,8 @@ class invariant_set_domaint:public ai_domain_baset
   bool merge(
     const invariant_set_domaint &other,
     locationt from,
-    locationt to)
+    locationt to,
+    const namespacet &ns)
   {
     bool changed=invariant_set.make_union(other.invariant_set) ||
                  has_values.is_false();

src/analyses/is_threaded.cpp

@@ -31,7 +31,8 @@ class is_threaded_domaint:public ai_domain_baset
   bool merge(
     const is_threaded_domaint &src,
     locationt from,
-    locationt to)
+    locationt to,
+    const namespacet &ns)
   {
     INVARIANT(src.reachable,
               "Abstract states are only merged at reachable locations");

src/analyses/natural_loops.cpp

@@ -15,11 +15,13 @@ void show_natural_loops(
   const goto_modelt &goto_model,
   std::ostream &out)
 {
+  namespacet ns(goto_model.symbol_table);
+
   forall_goto_functions(it, goto_model.goto_functions)
   {
     out << "*** " << it->first << '\n';
 
-    natural_loopst natural_loops;
+    natural_loopst natural_loops(ns);
     natural_loops(it->second.body);
     natural_loops.output(out);