Use symex_value_sett instead of value_sett in symex

This ensures that in symex the value set are always indexed using l1
renamed symbols.

Author: romainbrenguier

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

@@ -19,6 +19,7 @@ Author: Romain Brenguier, [email protected]
 #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 +41,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

@@ -138,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(is_l1_renamed(l1_lhs), "lhs renaming failed on l1");
-      DATA_INVARIANT(is_l1_renamed(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

src/goto-symex/symex_assign.cpp

@@ -508,7 +508,9 @@ void goto_symext::symex_assign_symbol(
     // have it in the propagation table and the value set while doing the field
     // assignments, thus we cannot skip putting it in there above.
     state.propagation.erase_if_exists(l1_lhs.get_identifier());
-    state.value_set.erase_symbol(l1_lhs, ns);
+    auto l1_lhs_checked = check_l1_renaming(l1_lhs);
+    CHECK_RETURN(l1_lhs_checked);
+    state.value_set.erase_symbol(*l1_lhs_checked, ns);
   }
 }
 

src/goto-symex/symex_dead.cpp

@@ -40,7 +40,7 @@ void goto_symext::symex_dead(statet &state, const symbol_exprt &symbol_expr)
     // information is not local to a path, but removing it from the propagation
     // map and value-set is safe as 1) it is local to a path and 2) this
     // instance can no longer appear.
-    state.value_set.values.erase_if_exists(l1_identifier);
+    state.value_set.erase_if_exists(l1_identifier);
     state.propagation.erase_if_exists(l1_identifier);
     // Remove from the local L2 renaming map; this means any reads from the dead
     // identifier will use generation 0 (e.g. x!N@M#0, where N and M are

src/goto-symex/symex_decl.cpp

@@ -59,8 +59,10 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     else
       rhs=exprt(ID_invalid);
 
-    exprt l1_rhs = state.rename<L1>(std::move(rhs), ns).get();
-    state.value_set.assign(ssa, l1_rhs, ns, true, false);
+    renamedt<exprt, L1> l1_rhs = state.rename<L1>(std::move(rhs), ns);
+    auto l1_ssa = check_l1_renaming(ssa);
+    CHECK_RETURN(l1_ssa.has_value());
+    state.value_set.assign(*l1_ssa, l1_rhs, ns, true, false);
   }
 
   // L2 renaming

src/goto-symex/symex_dereference_state.cpp

@@ -86,7 +86,10 @@ void symex_dereference_statet::get_value_set(
   const exprt &expr,
   value_setst::valuest &value_set) const
 {
-  state.value_set.get_value_set(expr, value_set, ns);
+  auto l1_expr = check_l1_renaming(expr);
+  CHECK_RETURN(l1_expr);
+  for(const auto e : state.value_set.get_value_set(*l1_expr, ns))
+    value_set.push_back(e);
 
 #ifdef DEBUG
   std::cout << "symex_dereference_statet state.value_set={\n";
@@ -112,5 +115,7 @@ void symex_dereference_statet::get_value_set(
 std::vector<exprt>
 symex_dereference_statet::get_value_set(const exprt &expr) const
 {
-  return state.value_set.get_value_set(expr, ns);
+  auto l1_expr = check_l1_renaming(expr);
+  CHECK_RETURN(l1_expr);
+  return state.value_set.get_value_set(*l1_expr, ns);
 }

src/goto-symex/symex_goto.cpp

@@ -83,7 +83,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
   const irep_idt &operation,
   const symbol_exprt &symbol_expr,
   const exprt &other_operand,
-  const value_sett &value_set,
+  const symex_value_sett &value_set,
   const irep_idt language_mode,
   const namespacet &ns)
 {
@@ -102,8 +102,10 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
 
   ssa_exprt l1_expr{*ssa_symbol_expr};
   l1_expr.remove_level_2();
+  const auto checked_l1_expr = check_l1_renaming((exprt)l1_expr);
+  CHECK_RETURN(checked_l1_expr);
   const std::vector<exprt> value_set_elements =
-    value_set.get_value_set(l1_expr, ns);
+    value_set.get_value_set(*checked_l1_expr, ns);
 
   bool constant_found = false;
 
@@ -169,7 +171,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
 ///   return that, otherwise we return an empty optionalt
 static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
   const renamedt<exprt, L2> &renamed_expr,
-  const value_sett &value_set,
+  const symex_value_sett &value_set,
   const irep_idt &language_mode,
   const namespacet &ns)
 {
@@ -200,7 +202,7 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
 
 renamedt<exprt, L2> try_evaluate_pointer_comparisons(
   renamedt<exprt, L2> condition,
-  const value_sett &value_set,
+  const symex_value_sett &value_set,
   const irep_idt &language_mode,
   const namespacet &ns)
 {

src/goto-symex/symex_main.cpp

@@ -689,9 +689,9 @@ find_unique_pointer_typed_symbol(const exprt &expr)
 void goto_symext::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)
 {
   condition = state.rename<L1>(std::move(condition), ns).get();
@@ -704,10 +704,10 @@ void goto_symext::try_filter_value_sets(
     return;
   }
 
-  const pointer_typet &symbol_type = to_pointer_type(symbol_expr->type());
-
+  const auto l1_symbol_expr = check_l1_renaming(*symbol_expr);
+  CHECK_RETURN(l1_symbol_expr);
   const std::vector<exprt> value_set_elements =
-    original_value_set.get_value_set(*symbol_expr, ns);
+    original_value_set.get_value_set(*l1_symbol_expr, ns);
 
   std::unordered_set<exprt, irep_hash> erase_from_jump_taken_value_set;
   std::unordered_set<exprt, irep_hash> erase_from_jump_not_taken_value_set;
@@ -775,16 +775,12 @@ void goto_symext::try_filter_value_sets(
   }
   if(jump_taken_value_set && !erase_from_jump_taken_value_set.empty())
   {
-    auto entry_index = jump_taken_value_set->get_index_of_symbol(
-      symbol_expr->get_identifier(), symbol_type, "", ns);
-    jump_taken_value_set->erase_values_from_entry(
-      *entry_index, erase_from_jump_taken_value_set);
+    jump_taken_value_set->erase(
+      *symbol_expr, ns, erase_from_jump_taken_value_set);
   }
   if(jump_not_taken_value_set && !erase_from_jump_not_taken_value_set.empty())
   {
-    auto entry_index = jump_not_taken_value_set->get_index_of_symbol(
-      symbol_expr->get_identifier(), symbol_type, "", ns);
-    jump_not_taken_value_set->erase_values_from_entry(
-      *entry_index, erase_from_jump_not_taken_value_set);
+    jump_not_taken_value_set->erase(
+      *symbol_expr, ns, erase_from_jump_not_taken_value_set);
   }
 }