Merge pull request diffblue#4755 from romainbrenguier/unit/renaming_level

Clean-up and unit test the renaming level classes

Author: romainbrenguier

src/goto-symex/frame.h

@@ -32,7 +32,7 @@ struct framet
   exprt return_value = nil_exprt();
   bool hidden_function = false;
 
-  symex_renaming_levelt::current_namest old_level1;
+  symex_level1t old_level1;
 
   std::set<irep_idt> local_objects;
 

src/goto-symex/goto_symex_state.cpp

@@ -135,21 +135,22 @@ template <>
 renamedt<ssa_exprt, L0>
 goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
 {
-  return level0(std::move(ssa_expr), ns, source.thread_nr);
+  return symex_level0(std::move(ssa_expr), ns, source.thread_nr);
 }
 
 template <>
 renamedt<ssa_exprt, L1>
 goto_symex_statet::set_indices<L1>(ssa_exprt ssa_expr, const namespacet &ns)
 {
-  return level1(level0(std::move(ssa_expr), ns, source.thread_nr));
+  return level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr));
 }
 
 template <>
 renamedt<ssa_exprt, L2>
 goto_symex_statet::set_indices<L2>(ssa_exprt ssa_expr, const namespacet &ns)
 {
-  return level2(level1(level0(std::move(ssa_expr), ns, source.thread_nr)));
+  return level2(
+    level1(symex_level0(std::move(ssa_expr), ns, source.thread_nr)));
 }
 
 renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
@@ -437,7 +438,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
     if(a_s_read.second.empty())
     {
       increase_generation(l1_identifier, ssa_l1);
-      a_s_read.first=level2.current_count(l1_identifier);
+      a_s_read.first = level2.latest_index(l1_identifier);
     }
     const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
 
@@ -796,28 +797,18 @@ ssa_exprt goto_symex_statet::add_object(
 {
   framet &frame = call_stack().top();
 
-  ssa_exprt ssa = rename_ssa<L0>(ssa_exprt{expr}, ns).get();
-  const irep_idt l0_name = ssa.get_identifier();
-  const std::size_t l1_index = index_generator(l0_name);
+  const renamedt<ssa_exprt, L0> renamed = rename_ssa<L0>(ssa_exprt{expr}, ns);
+  const irep_idt l0_name = renamed.get_identifier();
+  const auto l1_index = narrow_cast<unsigned>(index_generator(l0_name));
 
-  const auto r_opt = level1.current_names.find(l0_name);
-
-  if(!r_opt)
-  {
-    level1.current_names.insert(l0_name, std::make_pair(ssa, l1_index));
-  }
-  else
+  if(const auto old_value = level1.insert_or_replace(renamed, l1_index))
   {
     // save old L1 name
-    if(!frame.old_level1.has_key(l0_name))
-    {
-      frame.old_level1.insert(l0_name, r_opt->get());
-    }
-
-    level1.current_names.replace(l0_name, std::make_pair(ssa, l1_index));
+    if(!frame.old_level1.has(renamed))
+      frame.old_level1.insert(renamed, old_value->second);
   }
 
-  ssa = rename_ssa<L1>(std::move(ssa), ns).get();
+  const ssa_exprt ssa = rename_ssa<L1>(renamed.get(), ns).get();
   const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
   INVARIANT(inserted, "l1_name expected to be unique by construction");
 

src/goto-symex/goto_symex_state.h

@@ -70,7 +70,6 @@ class goto_symex_statet final : public goto_statet
   guard_managert &guard_manager;
   symex_target_equationt *symex_target;
 
-  symex_level0t level0;
   symex_level1t level1;
 
   /// Rewrites symbol expressions in \ref exprt, applying a suffix to each

src/goto-symex/renamed.h

@@ -0,0 +1,103 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+/// \file
+/// Class for expressions or types renamed up to a given level
+
+#ifndef CPROVER_GOTO_SYMEX_RENAMED_H
+#define CPROVER_GOTO_SYMEX_RENAMED_H
+
+/// Symex renaming level names.
+enum levelt
+{
+  L0 = 0,
+  L1 = 1,
+  L2 = 2
+};
+
+/// Wrapper for expressions or types which have been renamed up to a given
+/// \p level
+template <typename underlyingt, levelt level>
+class renamedt : private underlyingt
+{
+public:
+  static_assert(
+    std::is_base_of<exprt, underlyingt>::value ||
+      std::is_base_of<typet, underlyingt>::value,
+    "underlyingt should inherit from exprt or typet");
+
+  const underlyingt &get() const
+  {
+    return static_cast<const underlyingt &>(*this);
+  }
+
+  void simplify(const namespacet &ns)
+  {
+    (void)::simplify(value(), ns);
+  }
+
+  using mutator_functiont =
+    std::function<optionalt<renamedt>(const renamedt &)>;
+
+private:
+  underlyingt &value()
+  {
+    return static_cast<underlyingt &>(*this);
+  };
+
+  friend renamedt<ssa_exprt, L0>
+  symex_level0(ssa_exprt, const namespacet &, unsigned);
+  friend struct symex_level1t;
+  friend struct symex_level2t;
+  friend class goto_symex_statet;
+
+  template <levelt make_renamed_level>
+  friend renamedt<exprt, make_renamed_level>
+  make_renamed(constant_exprt constant);
+
+  template <levelt selectively_mutate_level>
+  friend void selectively_mutate(
+    renamedt<exprt, selectively_mutate_level> &renamed,
+    typename renamedt<exprt, selectively_mutate_level>::mutator_functiont
+      get_mutated_expr);
+
+  /// Only the friend classes can create renamedt objects
+  explicit renamedt(underlyingt value) : underlyingt(std::move(value))
+  {
+  }
+};
+
+template <levelt level>
+renamedt<exprt, level> make_renamed(constant_exprt constant)
+{
+  return renamedt<exprt, level>(std::move(constant));
+}
+
+/// This permits replacing subexpressions of the renamed value, so long as
+/// each replacement is consistent with our current renaming level (for
+/// example, replacing subexpressions of L2 expressions with ones which are
+/// themselves L2 renamed).
+/// The passed function will be called with each expression node in preorder
+/// (i.e. parent expressions before children), and should return an empty
+/// optional to make no change or a renamed expression to make a change.
+template <levelt level>
+void selectively_mutate(
+  renamedt<exprt, level> &renamed,
+  typename renamedt<exprt, level>::mutator_functiont get_mutated_expr)
+{
+  for(auto it = renamed.depth_begin(), itend = renamed.depth_end(); it != itend;
+      ++it)
+  {
+    optionalt<renamedt<exprt, level>> replacement =
+      get_mutated_expr(static_cast<const renamedt<exprt, level> &>(*it));
+
+    if(replacement)
+      it.mutate() = std::move(replacement->value());
+  }
+}
+
+#endif // CPROVER_GOTO_SYMEX_RENAMED_H

src/goto-symex/renaming_level.cpp

@@ -17,8 +17,21 @@ Author: Romain Brenguier, [email protected]
 
 #include "goto_symex_state.h"
 
-renamedt<ssa_exprt, L0> symex_level0t::
-operator()(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) const
+void get_variables(
+  const symex_renaming_levelt &current_names,
+  std::unordered_set<ssa_exprt, irep_hash> &vars)
+{
+  symex_renaming_levelt::viewt view;
+  current_names.get_view(view);
+
+  for(const auto &pair : view)
+  {
+    vars.insert(pair.second.first);
+  }
+}
+
+renamedt<ssa_exprt, L0>
+symex_level0(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr)
 {
   // already renamed?
   if(!ssa_expr.get_level_0().empty())
@@ -43,6 +56,33 @@ operator()(ssa_exprt ssa_expr, const namespacet &ns, unsigned thread_nr) const
   return renamedt<ssa_exprt, L0>{ssa_expr};
 }
 
+void symex_level1t::insert(const renamedt<ssa_exprt, L0> &ssa, unsigned index)
+{
+  current_names.insert(
+    ssa.get().get_identifier(), std::make_pair(ssa.get(), index));
+}
+
+optionalt<std::pair<ssa_exprt, unsigned>> symex_level1t::insert_or_replace(
+  const renamedt<ssa_exprt, L0> &ssa,
+  unsigned index)
+{
+  const irep_idt &identifier = ssa.get().get_identifier();
+  const auto old_value = current_names.find(identifier);
+  if(old_value)
+  {
+    std::pair<ssa_exprt, unsigned> result = *old_value;
+    current_names.replace(identifier, std::make_pair(ssa.get(), index));
+    return result;
+  }
+  current_names.insert(identifier, std::make_pair(ssa.get(), index));
+  return {};
+}
+
+bool symex_level1t::has(const renamedt<ssa_exprt, L0> &ssa) const
+{
+  return current_names.has_key(ssa.get().get_identifier());
+}
+
 renamedt<ssa_exprt, L1> symex_level1t::
 operator()(renamedt<ssa_exprt, L0> l0_expr) const
 {
@@ -72,14 +112,14 @@ operator()(renamedt<ssa_exprt, L1> l1_expr) const
 {
   if(!l1_expr.get().get_level_2().empty())
     return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
-  l1_expr.value().set_level_2(current_count(l1_expr.get().get_identifier()));
+  l1_expr.value().set_level_2(latest_index(l1_expr.get().get_identifier()));
   return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
 }
 
-void symex_level1t::restore_from(const current_namest &other)
+void symex_level1t::restore_from(const symex_level1t &other)
 {
-  current_namest::delta_viewt delta_view;
-  other.get_delta_view(current_names, delta_view, false);
+  symex_renaming_levelt::delta_viewt delta_view;
+  other.current_names.get_delta_view(current_names, delta_view, false);
 
   for(const auto &delta_item : delta_view)
   {
@@ -97,6 +137,12 @@ void symex_level1t::restore_from(const current_namest &other)
   }
 }
 
+unsigned symex_level2t::latest_index(const irep_idt &identifier) const
+{
+  const auto r_opt = current_names.find(identifier);
+  return !r_opt ? 0 : r_opt->get().second;
+}
+
 exprt get_original_name(exprt expr)
 {
   expr.type() = get_original_name(std::move(expr.type()));