Use depth_begin() and depth_end() to selectively mutate renamed expressions

Author: smowton

src/goto-symex/renaming_level.h

@@ -15,6 +15,7 @@ Author: Romain Brenguier, [email protected]
 #include <map>
 #include <unordered_set>
 
+#include <util/expr_iterator.h>
 #include <util/irep.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
@@ -67,31 +68,6 @@ struct symex_renaming_levelt
   }
 };
 
-template <typename underlyingt, levelt level>
-class renamedt;
-
-template <typename underlyingt, levelt level>
-class renamed_vectort
-{
-public:
-  void for_each(std::function<void(renamedt<underlyingt, level>&)> f)
-  {
-    for(auto &op : values)
-    {
-      auto op_as_renamed = renamedt<underlyingt, level>{op};
-      f(op_as_renamed);
-      op = op_as_renamed.value;
-    }
-  }
-
-private:
-  std::vector<underlyingt> &values;
-
-  explicit renamed_vectort(std::vector<underlyingt> &values) : values(values){};
-
-  friend renamedt<underlyingt, level>;
-};
-
 /// Wrapper for expressions or types which have been renamed up to a given
 /// \p level
 template <typename underlyingt, levelt level>
@@ -108,19 +84,32 @@ class renamedt
     return value;
   }
 
-  renamed_vectort<underlyingt, level> operands()
-  {
-    return renamed_vectort<underlyingt, level>{value.operands()};
-  };
-
-  const renamed_vectort<underlyingt, level> operands() const
+  void simplify(const namespacet &ns)
   {
-    return renamed_vectort<underlyingt, level>{value.operands()};
+    (void)::simplify(value, ns);
   }
 
-  void simplify(const namespacet &ns)
+  typedef std::function<optionalt<renamedt<exprt, level>>(const exprt &)>
+    expr_mutator_functiont;
+
+  /// 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.
+  void selectively_mutate(expr_mutator_functiont get_mutated_expr)
   {
-    (void)::simplify(value, ns);
+    for(
+      auto it = value.depth_begin(), itend = value.depth_end();
+      it != itend;
+      ++it)
+    {
+      auto replacement = get_mutated_expr(*it);
+      if(replacement)
+        it.mutate() = replacement->get();
+    }
   }
 
 private:
@@ -130,7 +119,6 @@ class renamedt
   friend struct symex_level1t;
   friend struct symex_level2t;
   friend class goto_symex_statet;
-  friend renamed_vectort<underlyingt, level>;
   template <levelt make_renamed_level>
   friend renamedt<exprt, make_renamed_level> make_renamed(constant_exprt constant);
 

src/goto-symex/symex_goto.cpp

@@ -79,8 +79,9 @@ void goto_symext::apply_goto_condition(
 /// \param value_set: The value-set for looking up what the symbol can point to
 /// \param language_mode: The language mode
 /// \param ns: A namespace
-static void try_evaluate_pointer_comparisons_base_case(
-  renamedt<exprt, L2> &condition,
+static optionalt<renamedt<exprt, L2>>
+try_evaluate_pointer_comparison(
+  irep_idt operation,
   const symbol_exprt &symbol_expr,
   const exprt &other_operand,
   const value_sett &value_set,
@@ -116,7 +117,7 @@ static void try_evaluate_pointer_comparisons_base_case(
     {
       // If ID_unknown or ID_invalid are in the value-set then we can't
       // conclude anything about it
-      return;
+      return {};
     }
 
     if(!constant_found)
@@ -142,20 +143,22 @@ static void try_evaluate_pointer_comparisons_base_case(
   {
     // The symbol cannot possibly have the value \p other_operand because it
     // isn't in the symbol's value-set
-    condition = condition.get().id() == ID_equal ? make_renamed<L2>(false_exprt{})
-                                           : make_renamed<L2>(true_exprt{});
+    return operation == ID_equal ? make_renamed<L2>(false_exprt{})
+                                            : make_renamed<L2>(true_exprt{});
   }
   else if(value_set_elements.size() == 1)
   {
     // The symbol must have the value \p other_operand because it is the only
     // thing in the symbol's value-set
-    condition = condition.get().id() == ID_equal ? make_renamed<L2>(true_exprt{})
-                                           : make_renamed<L2>(false_exprt{});
+    return operation == ID_equal ? make_renamed<L2>(true_exprt{})
+                                            : make_renamed<L2>(false_exprt{});
+  }
+  else
+  {
+    return {};
   }
 }
 
-
-
 /// Check if we have a simple pointer comparison, and if so try to evaluate it.
 /// \param [in,out] condition: An L2- renamed expression of the form
 ///   "symbol_expr == other" or "symbol_expr != other" (or one of those with
@@ -168,30 +171,34 @@ static void try_evaluate_pointer_comparisons_base_case(
 /// \param value_set: The value-set for looking up what the symbol can point to
 /// \param language_mode: The language mode
 /// \param ns: A namespace
-static bool try_evaluate_pointer_comparisons_base_case_with_check(
-  renamedt<exprt, L2> &condition,
-  const exprt &symbol_expr,
-  const exprt &other_operand,
+static optionalt<renamedt<exprt, L2>>
+try_evaluate_pointer_comparison(
+  const exprt &expr,
   const value_sett &value_set,
   const irep_idt language_mode,
   const namespacet &ns)
 {
+  if(expr.id() != ID_equal && expr.id() != ID_notequal)
+    return {};
+
+  if(!can_cast_type<pointer_typet>(expr.op0().type()))
+    return {};
+
+  exprt lhs = expr.op0(), rhs = expr.op1();
+  if(can_cast_expr<symbol_exprt>(rhs))
+    std::swap(lhs, rhs);
+
   const symbol_exprt *symbol_expr_lhs =
-    expr_try_dynamic_cast<symbol_exprt>(symbol_expr);
+    expr_try_dynamic_cast<symbol_exprt>(lhs);
 
   if(!symbol_expr_lhs)
-  {
-    return false;
-  }
+    return {};
 
-  if(!goto_symex_is_constantt()(other_operand))
-  {
-    return false;
-  }
+  if(!goto_symex_is_constantt()(rhs))
+    return {};
 
-  try_evaluate_pointer_comparisons_base_case(
-    condition, *symbol_expr_lhs, other_operand, value_set, language_mode, ns);
-  return true;
+  return try_evaluate_pointer_comparison(
+    expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
 }
 
 /// Try to evaluate pointer comparisons where they can be trivially determined
@@ -208,37 +215,11 @@ static renamedt<exprt, L2> try_evaluate_pointer_comparisons(
   const irep_idt language_mode,
   const namespacet &ns)
 {
-  const exprt &condition_expr = condition.get();
-  if(condition_expr.id() == ID_equal || condition_expr.id() == ID_notequal)
-  {
-    if(can_cast_type<pointer_typet>(condition_expr.op0().type()))
-    {
-      // Check if this is the form "symbol rel constant" or "constant rel symbol"
-      if(!try_evaluate_pointer_comparisons_base_case_with_check(
-        condition,
-        condition_expr.op0(),
-        condition_expr.op1(),
-        value_set,
-        language_mode,
-        ns))
-      {
-        try_evaluate_pointer_comparisons_base_case_with_check(
-          condition,
-          condition_expr.op1(),
-          condition_expr.op0(),
-          value_set,
-          language_mode,
-          ns);
-      }
-    }
-  }
-  else
-  {
-    condition.operands().for_each([&](renamedt<exprt, L2> &op) {
-      op = try_evaluate_pointer_comparisons(
-        std::move(op), value_set, language_mode, ns);
+  condition.selectively_mutate(
+    [&value_set, &language_mode, &ns](const exprt &expr) {
+      return try_evaluate_pointer_comparison(
+        expr, value_set, language_mode, ns);
     });
-  }
 
   return condition;
 }