More precise control-flow graph using the simplifier

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/dependence_graph.h

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

src/analyses/natural_loops.h

@@ -20,7 +20,7 @@ Author: Georg Weissenbacher, [email protected]
 
 #include "cfg_dominators.h"
 
-template<class P, class T>
+template<class P, class T, bool syntactic>
 class natural_loops_templatet
 {
 public:
@@ -38,35 +38,47 @@ class natural_loops_templatet
 
   void output(std::ostream &) const;
 
-  const cfg_dominators_templatet<P, T, false> &get_dominator_info() const
+  const cfg_dominators_templatet<P, T, false, syntactic>&
+    get_dominator_info() const
   {
     return cfg_dominators;
   }
 
-  natural_loops_templatet()
+  explicit natural_loops_templatet(const namespacet &ns):
+    cfg_dominators(ns)
   {
   }
 
-  explicit natural_loops_templatet(P &program)
+  natural_loops_templatet(P &program, const namespacet &ns):
+    cfg_dominators(ns)
   {
     compute(program);
   }
 
 protected:
-  cfg_dominators_templatet<P, T, false> cfg_dominators;
-  typedef typename cfg_dominators_templatet<P, T, false>::cfgt::nodet nodet;
+  cfg_dominators_templatet<P, T, false, syntactic> cfg_dominators;
+  typedef typename cfg_dominators_templatet<P, T, false, syntactic>::
+    cfgt::nodet nodet;
 
   void compute(P &program);
   void compute_natural_loop(T, T);
 };
 
 class natural_loopst:
     public natural_loops_templatet<const goto_programt,
-                                   goto_programt::const_targett>
+                                   goto_programt::const_targett,
+                                   false>
 {
+public:
+  explicit natural_loopst(const namespacet &ns):
+    natural_loops_templatet<const goto_programt,
+                            goto_programt::const_targett,
+                            false>(ns)
+  {
+  }
 };
 
-typedef natural_loops_templatet<goto_programt, goto_programt::targett>
+typedef natural_loops_templatet<goto_programt, goto_programt::targett, false>
     natural_loops_mutablet;
 
 void show_natural_loops(
@@ -78,8 +90,8 @@ void show_natural_loops(
 #include <iostream>
 #endif
 
-template<class P, class T>
-void natural_loops_templatet<P, T>::compute(P &program)
+template<class P, class T, bool S>
+void natural_loops_templatet<P, T, S>::compute(P &program)
 {
   cfg_dominators(program);
 
@@ -115,8 +127,8 @@ void natural_loops_templatet<P, T>::compute(P &program)
 }
 
 /// Computes the natural loop for a given back-edge (see Muchnick section 7.4)
-template<class P, class T>
-void natural_loops_templatet<P, T>::compute_natural_loop(T m, T n)
+template<class P, class T, bool S>
+void natural_loops_templatet<P, T, S>::compute_natural_loop(T m, T n)
 {
   assert(n->location_number<=m->location_number);
 
@@ -150,8 +162,8 @@ void natural_loops_templatet<P, T>::compute_natural_loop(T m, T n)
 }
 
 /// Print all natural loops that were found
-template<class P, class T>
-void natural_loops_templatet<P, T>::output(std::ostream &out) const
+template<class P, class T, bool S>
+void natural_loops_templatet<P, T, S>::output(std::ostream &out) const
 {
   for(const auto &loop : loop_map)
   {

src/goto-analyzer/unreachable_instructions.cpp

@@ -29,9 +29,10 @@ typedef std::map<unsigned, goto_programt::const_targett> dead_mapt;
 
 static void unreachable_instructions(
   const goto_programt &goto_program,
-  dead_mapt &dest)
+  dead_mapt &dest,
+  const namespacet &ns)
 {
-  cfg_dominatorst dominators;
+  cfg_dominatorst dominators(ns);
   dominators(goto_program);
 
   for(cfg_dominatorst::cfgt::entry_mapt::const_iterator
@@ -188,7 +189,7 @@ void unreachable_instructions(
     // base_name instead; do not list inlined functions
     if(called.find(decl.base_name)!=called.end() ||
        f_it->second.is_inlined())
-      unreachable_instructions(goto_program, dead_map);
+      unreachable_instructions(goto_program, dead_map, ns);
     else
       all_unreachable(goto_program, dead_map);
 

src/goto-instrument/accelerate/accelerate.h

@@ -40,6 +40,7 @@ class acceleratet
       goto_functions(_goto_model.goto_functions),
       symbol_table(_goto_model.symbol_table),
       ns(_goto_model.symbol_table),
+      natural_loops(ns),
       utils(symbol_table, message_handler, goto_functions),
       use_z3(_use_z3)
   {

src/goto-instrument/code_contracts.cpp

@@ -225,7 +225,7 @@ void code_contractst::code_contracts(
   goto_functionst::goto_functiont &goto_function)
 {
   local_may_aliast local_may_alias(goto_function);
-  natural_loops_mutablet natural_loops(goto_function.body);
+  natural_loops_mutablet natural_loops(goto_function.body, ns);
 
   // iterate over the (natural) loops in the function
   for(natural_loops_mutablet::loop_mapt::const_iterator

src/goto-instrument/count_eloc.cpp

@@ -97,7 +97,8 @@ void print_path_lengths(const goto_modelt &goto_model)
   };
 
   typedef cfg_baset<visited_cfg_nodet> cfgt;
-  cfgt cfg;
+  namespacet ns(goto_model.symbol_table);
+  cfgt cfg(ns);
   cfg(goto_model.goto_functions);
 
   const goto_programt &start_program=start->second.body;

src/goto-instrument/full_slicer.cpp

@@ -307,7 +307,13 @@ void full_slicert::operator()(
       add_to_queue(queue, e_it->second, e_it->first);
     else if(implicit(e_it->first))
       add_to_queue(queue, e_it->second, e_it->first);
-    else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
+    // any jump (control transfer to an instruction other than the next one)
+    // that will always be taken, i.e., also include conditional jumps the
+    // condition of which always evaluates to true
+    else if((e_it->first->is_goto() &&
+             cfg[e_it->second].out.size()==1 &&
+             cfg[cfg[e_it->second].out.begin()->first].PC!=
+             std::next(e_it->first)) ||
             e_it->first->is_throw())
       jumps.push_back(e_it->second);
     else if(e_it->first->is_decl())
@@ -372,22 +378,24 @@ void full_slicer(
   const namespacet &ns,
   slicing_criteriont &criterion)
 {
-  full_slicert()(goto_functions, ns, criterion);
+  full_slicert s(ns);
+  s(goto_functions, ns, criterion);
 }
 
 void full_slicer(
   goto_functionst &goto_functions,
   const namespacet &ns)
 {
   assert_criteriont a;
-  full_slicert()(goto_functions, ns, a);
+  full_slicert s(ns);
+  s(goto_functions, ns, a);
 }
 
 void full_slicer(goto_modelt &goto_model)
 {
   assert_criteriont a;
   const namespacet ns(goto_model.symbol_table);
-  full_slicert()(goto_model.goto_functions, ns, a);
+  full_slicer(goto_model.goto_functions, ns);
 }
 
 void property_slicer(
@@ -396,7 +404,8 @@ void property_slicer(
   const std::list<std::string> &properties)
 {
   properties_criteriont p(properties);
-  full_slicert()(goto_functions, ns, p);
+  full_slicert s(ns);
+  s(goto_functions, ns, p);
 }
 
 void property_slicer(

src/goto-instrument/full_slicer_class.h

@@ -38,6 +38,11 @@ echo 'digraph g {' > c.dot ; cat c.goto | \
 class full_slicert
 {
 public:
+  explicit full_slicert(const namespacet &ns):
+    cfg(ns)
+  {
+  }
+
   void operator()(
     goto_functionst &goto_functions,
     const namespacet &ns,

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -395,7 +395,7 @@ int goto_instrument_parse_optionst::doit()
       namespacet ns(goto_model.symbol_table);
 
       status() << "Pointer Analysis" << eom;
-      points_tot points_to;
+      points_tot points_to(ns);
       points_to(goto_model);
       points_to.output(std::cout);
       return CPROVER_EXIT_SUCCESS;