Introduce symex value set as interface to value set

src/goto-symex/Makefile

@@ -12,6 +12,7 @@ SRC = auto_objects.cpp \
       path_storage.cpp \
       postcondition.cpp \
       precondition.cpp \
+      renamed.cpp \
       renaming_level.cpp \
       show_program.cpp \
       show_vcc.cpp \

src/goto-symex/goto_state.cpp

@@ -104,7 +104,11 @@ void goto_statet::apply_condition(
         else if(propagation_entry->get() != rhs)
           propagation.replace(l1_identifier, rhs);
 
-        value_set.assign(l1_lhs, rhs, ns, true, false);
+        auto l1_lhs_checked = check_l1_renaming(l1_lhs);
+        CHECK_RETURN(l1_lhs_checked);
+        auto l1_rhs_checked = check_l1_renaming(rhs);
+        CHECK_RETURN(l1_rhs_checked);
+        value_set.assign(*l1_lhs_checked, *l1_rhs_checked, ns, true, false);
       }
     }
   }

src/goto-symex/goto_state.h

@@ -16,9 +16,9 @@ Author: Romain Brenguier, [email protected]
 
 #include <analyses/guard.h>
 #include <analyses/local_safe_pointers.h>
-#include <pointer-analysis/value_set.h>
 
 #include "renaming_level.h"
+#include "symex_value_set.h"
 
 /// Container for data that varies per program point, e.g. the constant
 /// propagator state, when state needs to branch. This is copied out of
@@ -40,7 +40,7 @@ class goto_statet
   }
 
   /// Uses level 1 names, and is used to do dereferencing
-  value_sett value_set;
+  symex_value_sett value_set;
 
   // A guard is a particular condition that has to pass for an instruction
   // to be executed. The easiest example is an if/else: each instruction along

src/goto-symex/goto_symex.h

@@ -392,9 +392,9 @@ class goto_symext
   void try_filter_value_sets(
     goto_symex_statet &state,
     exprt condition,
-    const value_sett &original_value_set,
-    value_sett *jump_taken_value_set,
-    value_sett *jump_not_taken_value_set,
+    const symex_value_sett &original_value_set,
+    symex_value_sett *jump_taken_value_set,
+    symex_value_sett *jump_not_taken_value_set,
     const namespacet &ns);
 
   virtual void vcc(

src/goto-symex/goto_symex_state.cpp

@@ -47,90 +47,6 @@ goto_symex_statet::goto_symex_statet(
 
 goto_symex_statet::~goto_symex_statet()=default;
 
-/// Check that \p expr is correctly renamed to level 2 and return true in case
-/// an error is detected.
-static bool check_renaming(const exprt &expr);
-
-static bool check_renaming(const typet &type)
-{
-  if(type.id()==ID_array)
-    return check_renaming(to_array_type(type).size());
-  else if(type.id() == ID_struct || type.id() == ID_union)
-  {
-    for(const auto &c : to_struct_union_type(type).components())
-      if(check_renaming(c.type()))
-        return true;
-  }
-  else if(type.has_subtype())
-    return check_renaming(to_type_with_subtype(type).subtype());
-
-  return false;
-}
-
-static bool check_renaming_l1(const exprt &expr)
-{
-  if(check_renaming(expr.type()))
-    return true;
-
-  if(expr.id()==ID_symbol)
-  {
-    const auto &type = expr.type();
-    if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
-    if(!to_ssa_expr(expr).get_level_2().empty())
-      return true;
-    if(to_ssa_expr(expr).get_original_expr().type() != type)
-      return true;
-  }
-  else
-  {
-    forall_operands(it, expr)
-      if(check_renaming_l1(*it))
-        return true;
-  }
-
-  return false;
-}
-
-static bool check_renaming(const exprt &expr)
-{
-  if(check_renaming(expr.type()))
-    return true;
-
-  if(
-    expr.id() == ID_address_of &&
-    to_address_of_expr(expr).object().id() == ID_symbol)
-  {
-    return check_renaming_l1(to_address_of_expr(expr).object());
-  }
-  else if(
-    expr.id() == ID_address_of &&
-    to_address_of_expr(expr).object().id() == ID_index)
-  {
-    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
-    return check_renaming_l1(index_expr.array()) ||
-           check_renaming(index_expr.index());
-  }
-  else if(expr.id()==ID_symbol)
-  {
-    const auto &type = expr.type();
-    if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
-    if(to_ssa_expr(expr).get_level_2().empty())
-      return true;
-    if(to_ssa_expr(expr).get_original_expr().type() != type)
-      return true;
-  }
-  else
-  {
-    forall_operands(it, expr)
-      if(check_renaming(*it))
-        return true;
-  }
-
-  return false;
-}
-
 template <>
 renamedt<ssa_exprt, L0>
 goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)
@@ -170,7 +86,7 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
   lhs.update_type();
   if(run_validation_checks)
   {
-    DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
+    DATA_INVARIANT(is_l1_renamed(lhs), "lhs renaming failed on l1");
   }
   const ssa_exprt l1_lhs = lhs;
 
@@ -192,8 +108,8 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
 
   if(run_validation_checks)
   {
-    DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
-    DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
+    DATA_INVARIANT(is_l2_renamed(lhs), "lhs renaming failed on l2");
+    DATA_INVARIANT(is_l2_renamed(rhs), "rhs renaming failed on l2");
   }
 
   // see #305 on GitHub for a simple example and possible discussion
@@ -222,13 +138,13 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
     ssa_exprt l1_lhs(lhs);
     l1_lhs.remove_level_2();
 
-    if(run_validation_checks)
-    {
-      DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
-      DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
-    }
+    auto l1_lhs_checked = check_l1_renaming(l1_lhs);
+    DATA_INVARIANT(l1_lhs_checked, "lhs renaming failed on l1");
+    auto l1_rhs_checked = check_l1_renaming(l1_rhs);
+    DATA_INVARIANT(l1_rhs_checked, "rhs renaming failed on l1");
 
-    value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
+    value_set.assign(
+      *l1_lhs_checked, *l1_rhs_checked, ns, rhs_is_simplified, is_shared);
   }
 
 #if 0
@@ -461,7 +377,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
       source,
       symex_targett::assignment_typet::PHI);
 
-    INVARIANT(!check_renaming(ssa_l2), "expr should be renamed to L2");
+    INVARIANT(is_l2_renamed(ssa_l2), "expr should be renamed to L2");
     expr = std::move(ssa_l2);
 
     a_s_read.second.push_back(guard);

src/goto-symex/renamed.cpp

@@ -0,0 +1,134 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Class for expressions or types renamed up to a given level
+
+#include "renamed.h"
+#include <util/ssa_expr.h>
+#include <util/std_expr.h>
+
+template <levelt level>
+renamedt<exprt, level> make_renamed(constant_exprt constant)
+{
+  return renamedt<exprt, level>(std::move(constant));
+}
+
+// Force template instantiations for the three levels
+template renamedt<exprt, L0> make_renamed(constant_exprt constant);
+template renamedt<exprt, L1> make_renamed(constant_exprt constant);
+template renamedt<exprt, L2> make_renamed(constant_exprt constant);
+
+bool is_l1_renamed(const exprt &expr)
+{
+  if(expr.id() == ID_symbol)
+  {
+    const auto &type = expr.type();
+    if(!expr.get_bool(ID_C_SSA_symbol))
+      return type.id() == ID_code || type.id() == ID_mathematical_function;
+    if(!to_ssa_expr(expr).get_level_2().empty())
+      return false;
+    if(to_ssa_expr(expr).get_original_expr().type() != type)
+      return false;
+  }
+  else
+  {
+    forall_operands(it, expr)
+      if(!is_l1_renamed(*it))
+        return false;
+  }
+
+  return true;
+}
+
+bool is_l2_renamed(const typet &type)
+{
+  if(type.id() == ID_array)
+  {
+    if(!is_l2_renamed(to_array_type(type).size()))
+      return false;
+  }
+  else if(type.id() == ID_struct || type.id() == ID_union)
+  {
+    for(const auto &c : to_struct_union_type(type).components())
+      if(!is_l2_renamed(c.type()))
+        return false;
+  }
+  else if(
+    type.has_subtype() && !is_l2_renamed(to_type_with_subtype(type).subtype()))
+  {
+    return false;
+  }
+  return true;
+}
+
+bool is_l2_renamed(const exprt &expr)
+{
+  if(!is_l2_renamed(expr.type()))
+    return false;
+
+  if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_symbol)
+  {
+    return is_l1_renamed(to_address_of_expr(expr).object());
+  }
+  else if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_index)
+  {
+    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
+    return is_l1_renamed(index_expr.array()) &&
+           is_l2_renamed(index_expr.index());
+  }
+  else if(expr.id() == ID_symbol)
+  {
+    const auto &type = expr.type();
+    if(!expr.get_bool(ID_C_SSA_symbol))
+      return (type.id() == ID_code || type.id() == ID_mathematical_function);
+    if(to_ssa_expr(expr).get_level_2().empty())
+      return false;
+    if(to_ssa_expr(expr).get_original_expr().type() != type)
+      return false;
+  }
+  else
+  {
+    forall_operands(it, expr)
+      if(!is_l2_renamed(*it))
+        return false;
+  }
+  return true;
+}
+
+optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr)
+{
+  if(is_l1_renamed(expr))
+    return renamedt<exprt, L1>(std::move(expr));
+  return {};
+}
+
+optionalt<renamedt<ssa_exprt, L1>> check_l1_renaming(ssa_exprt expr)
+{
+  if(is_l1_renamed(expr))
+    return renamedt<ssa_exprt, L1>(std::move(expr));
+  return {};
+}
+
+optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr)
+{
+  if(is_l2_renamed(expr))
+    return renamedt<exprt, L2>(std::move(expr));
+  return {};
+}
+
+optionalt<renamedt<typet, L2>> check_l2_renaming(typet type)
+{
+  if(is_l2_renamed(type))
+    return renamedt<typet, L2>(std::move(type));
+  return {};
+}

src/goto-symex/renamed.h

@@ -11,6 +11,17 @@ Author: Romain Brenguier, [email protected]
 #ifndef CPROVER_GOTO_SYMEX_RENAMED_H
 #define CPROVER_GOTO_SYMEX_RENAMED_H
 
+#include <functional>
+#include <type_traits>
+#include <util/nodiscard.h>
+#include <util/optional.h>
+#include <util/simplify_expr.h>
+
+class constant_exprt;
+class exprt;
+class ssa_exprt;
+class typet;
+
 /// Symex renaming level names.
 enum levelt
 {
@@ -65,17 +76,19 @@ class renamedt : private underlyingt
     typename renamedt<exprt, selectively_mutate_level>::mutator_functiont
       get_mutated_expr);
 
+  friend optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr);
+  friend optionalt<renamedt<ssa_exprt, L1>> check_l1_renaming(ssa_exprt expr);
+  friend optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr);
+  friend optionalt<renamedt<typet, L2>> check_l2_renaming(typet type);
+
   /// 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));
-}
+renamedt<exprt, level> make_renamed(constant_exprt constant);
 
 /// This permits replacing subexpressions of the renamed value, so long as
 /// each replacement is consistent with our current renaming level (for
@@ -100,4 +113,24 @@ void selectively_mutate(
   }
 }
 
+/// \return true if \p expr has been renamed to level 2
+bool is_l2_renamed(const exprt &expr);
+
+/// \return true if \p type has been renamed to level 2
+bool is_l2_renamed(const typet &type);
+
+/// \return true if \p expr has been renamed to level 1
+bool is_l1_renamed(const exprt &expr);
+
+/// \return a renamed object if \p expr has been renamed to level 1
+NODISCARD optionalt<renamedt<exprt, L1>> check_l1_renaming(exprt expr);
+
+NODISCARD optionalt<renamedt<ssa_exprt, L1>> check_l1_renaming(ssa_exprt expr);
+
+/// \return a renamed object if \p expr has been renamed to level 2
+NODISCARD optionalt<renamedt<exprt, L2>> check_l2_renaming(exprt expr);
+
+/// \return a renamed object if \p type has been renamed to level 2
+NODISCARD optionalt<renamedt<typet, L2>> check_l2_renaming(typet type);
+
 #endif // CPROVER_GOTO_SYMEX_RENAMED_H