Addressing constant domain review comments by Daniel Poetzl.

Author: martin

src/analyses/Makefile

@@ -22,7 +22,6 @@ SRC = ai.cpp \
       locals.cpp \
       natural_loops.cpp \
       reaching_definitions.cpp \
-      replace_symbol_ext.cpp \
       static_analysis.cpp \
       uncaught_exceptions_analysis.cpp \
       uninitialized_domain.cpp \

src/analyses/constant_propagator.cpp

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Constant Propagation
+Module: Constant propagation
 
 Author: Peter Schrammel
 
@@ -18,6 +18,7 @@ Author: Peter Schrammel
 #include <util/find_symbols.h>
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
+#include <util/cprover_prefix.h>
 
 void constant_propagator_domaint::assign_rec(
   valuest &values,
@@ -32,7 +33,7 @@ void constant_propagator_domaint::assign_rec(
 
   exprt tmp=rhs;
   values.replace_const(tmp);
-  tmp=simplify_expr(tmp, ns);
+  simplify(tmp, ns);
 
   if(tmp.is_constant())
     values.set_to(s, tmp);
@@ -122,13 +123,13 @@ void constant_propagator_domaint::transform(
 
       if(to==next)
       {
-        if(id=="__CPROVER_set_must" ||
-           id=="__CPROVER_get_must" ||
-           id=="__CPROVER_set_may" ||
-           id=="__CPROVER_get_may" ||
-           id=="__CPROVER_cleanup" ||
-           id=="__CPROVER_clear_may" ||
-           id=="__CPROVER_clear_must")
+        if(id==CPROVER_PREFIX "set_must" ||
+           id==CPROVER_PREFIX "get_must" ||
+           id==CPROVER_PREFIX "set_may" ||
+           id==CPROVER_PREFIX "get_may" ||
+           id==CPROVER_PREFIX "cleanup" ||
+           id==CPROVER_PREFIX "clear_may" ||
+           id==CPROVER_PREFIX "clear_must")
         {
           // no effect on constants
         }
@@ -149,17 +150,19 @@ void constant_propagator_domaint::transform(
         const code_typet &code_type=to_code_type(symbol.type);
         const code_typet::parameterst &parameters=code_type.parameters();
 
-        const code_function_callt::argumentst &arguments
-          =function_call.arguments();
+        const code_function_callt::argumentst &arguments=
+          function_call.arguments();
 
-        unsigned n=std::min(arguments.size(), parameters.size());
-
-        for(unsigned i=0; i<n; i++)
+        code_typet::parameterst::const_iterator p_it=parameters.begin();
+        for(const auto &arg : arguments)
         {
-          const symbol_exprt &parameter_expr
-            =symbol_exprt(parameters[i].get_identifier(), arguments[i].type());
+          if(p_it==parameters.end())
+            break;
+
+          const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type());
+          assign_rec(values, parameter_expr, arg, ns);
 
-          assign_rec(values, parameter_expr, arguments[i], ns);
+          ++p_it;
         }
       }
     }
@@ -183,18 +186,8 @@ void constant_propagator_domaint::transform(
 
     const code_typet &type=to_code_type(symbol.type);
 
-    typedef code_typet::parameterst parameterst;
-    const parameterst &parameters=type.parameters();
-
-    for(parameterst::const_iterator it=parameters.begin();
-        it!=parameters.end(); it++)
-    {
-      // normal parameter
-      const irep_idt par=it->get_identifier();
-
-      // this erases the parameter from the map
-      values.set_to_top(par);
-    }
+    for(const auto &param : type.parameters())
+      values.set_to_top(param.get_identifier());
   }
 
   INVARIANT(from->is_goto() || !values.is_bottom,
@@ -218,6 +211,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
 
   bool change=false;
 
+  // this seems to be buggy at present
 #if 0
   if(expr.id()==ID_and)
   {
@@ -318,25 +312,20 @@ bool constant_propagator_domaint::valuest::is_constant_address_of(
 /// Do not call this when iterating over replace_const.expr_map!
 bool constant_propagator_domaint::valuest::set_to_top(const irep_idt &id)
 {
-  replace_symbolt::expr_mapt::iterator r_it
-    =replace_const.expr_map.find(id);
+  replace_symbolt::expr_mapt::size_type n_erased=
+    replace_const.expr_map.erase(id);
 
-  if(r_it!=replace_const.expr_map.end())
-  {
-    assert(!is_bottom);
-    replace_const.expr_map.erase(r_it);
-    return true;
-  }
+  INVARIANT(n_erased==0 || !is_bottom, "bottom => 0 erased");
 
-  return false;
+  return n_erased>0;
 }
 
 
 void constant_propagator_domaint::valuest::set_dirty_to_top(
   const dirtyt &dirty,
   const namespacet &ns)
 {
-  typedef replace_symbol_extt::expr_mapt expr_mapt;
+  typedef replace_symbolt::expr_mapt expr_mapt;
   expr_mapt &expr_map=replace_const.expr_map;
 
   for(expr_mapt::iterator it=expr_map.begin();
@@ -375,12 +364,9 @@ void constant_propagator_domaint::valuest::output(
     return;
   }
 
-  for(replace_symbolt::expr_mapt::const_iterator
-      it=replace_const.expr_map.begin();
-      it!=replace_const.expr_map.end();
-      ++it)
+  for(const auto &p : replace_const.expr_map)
   {
-    out << ' ' << it->first << "=" << from_expr(ns, "", it->second) << '\n';
+    out << ' ' << p.first << "=" << from_expr(ns, "", p.second) << '\n';
   }
 }
 
@@ -396,10 +382,6 @@ void constant_propagator_domaint::output(
 /// \return Return true if "this" has changed.
 bool constant_propagator_domaint::valuest::merge(const valuest &src)
 {
-  // dummy
-  const symbol_tablet symbol_table;
-  const namespacet ns(symbol_table);
-
   // nothing to do
   if(src.is_bottom)
     return false;
@@ -417,8 +399,8 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
 
   bool changed=false;
 
-  replace_symbol_extt::expr_mapt &expr_map=replace_const.expr_map;
-  const replace_symbol_extt::expr_mapt &src_expr_map=src.replace_const.expr_map;
+  replace_symbolt::expr_mapt &expr_map=replace_const.expr_map;
+  const replace_symbolt::expr_mapt &src_expr_map=src.replace_const.expr_map;
 
   // handle top
   if(src_expr_map.empty())
@@ -427,8 +409,6 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
     changed=!expr_map.empty();
 
     set_to_top();
-    assert(expr_map.empty());
-    assert(!is_bottom);
 
     return changed;
   }
@@ -475,29 +455,26 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src)
   if(src.is_bottom || is_bottom)
     return false;
 
-  bool changed = false;
+  bool changed=false;
 
-  for(replace_symbolt::expr_mapt::const_iterator
-      it=src.replace_const.expr_map.begin();
-      it!=src.replace_const.expr_map.end();
-      ++it)
+  for(const auto &m : src.replace_const.expr_map)
   {
     replace_symbolt::expr_mapt::iterator
-      c_it = replace_const.expr_map.find(it->first);
+      c_it=replace_const.expr_map.find(m.first);
 
     if(c_it!=replace_const.expr_map.end())
     {
-      if(c_it->second!=it->second)
+      if(c_it->second!=m.second)
       {
         set_to_bottom();
-        changed = true;
+        changed=true;
         break;
       }
     }
     else
     {
-      set_to(it->first, it->second);
-      changed = true;
+      set_to(m.first, m.second);
+      changed=true;
     }
   }
 
@@ -510,31 +487,7 @@ bool constant_propagator_domaint::merge(
   locationt from,
   locationt to)
 {
-  const symbol_tablet symbol_table;
-  const namespacet ns(symbol_table);
-
-#if 0
-  if(to->is_skip())
-  {
-    std::cout << "This:\n";
-    values.output(std::cout, ns);
-    std::cout << "Other:\n";
-    other.values.output(std::cout, ns);
-  }
-#endif
-
-  bool b;
-  b=values.merge(other.values);
-
-#if 0
-  if(to->is_skip())
-  {
-    std::cout << "Merge result:\n";
-    values.output(std::cout, ns);
-  }
-#endif
-
-  return b;
+  return values.merge(other.values);
 }
 
 void constant_propagator_ait::replace(
@@ -563,21 +516,22 @@ void constant_propagator_ait::replace(
     if(it->is_goto() || it->is_assume() || it->is_assert())
     {
       s_it->second.values.replace_const(it->guard);
-      it->guard = simplify_expr(it->guard, ns);
+      simplify(it->guard, ns);
     }
     else if(it->is_assign())
     {
       exprt &rhs=to_code_assign(it->code).rhs();
       s_it->second.values.replace_const(rhs);
-      rhs=simplify_expr(rhs, ns);
+      simplify(rhs, ns);
       if(rhs.id()==ID_constant)
         rhs.add_source_location()=it->code.op0().source_location();
     }
     else if(it->is_function_call())
     {
       s_it->second.values.replace_const(
         to_code_function_call(it->code).function());
-      simplify_expr(to_code_function_call(it->code).function(), ns);
+
+      simplify(to_code_function_call(it->code).function(), ns);
 
       exprt::operandst &args=
         to_code_function_call(it->code).arguments();
@@ -586,7 +540,7 @@ void constant_propagator_ait::replace(
           o_it!=args.end(); ++o_it)
       {
         s_it->second.values.replace_const(*o_it);
-        *o_it=simplify_expr(*o_it, ns);
+        simplify(*o_it, ns);
       }
     }
     else if(it->is_other())

src/analyses/constant_propagator.h

@@ -12,13 +12,12 @@ Author: Peter Schrammel
 #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
 #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H
 
-#include <iostream>
+#include <iosfwd>
+#include <util/replace_symbol.h>
 
 #include "ai.h"
 #include "dirty.h"
 
-#include "replace_symbol_ext.h"
-
 class constant_propagator_domaint:public ai_domain_baset
 {
 public:
@@ -63,7 +62,7 @@ class constant_propagator_domaint:public ai_domain_baset
     valuest():is_bottom(true) {}
 
     // maps variables to constants
-    replace_symbol_extt replace_const;
+    replace_symbolt replace_const;
     bool is_bottom;
 
     bool merge(const valuest &src);