Merge pull request #4656 from diffblue/revert-4444-value-set-filtering-infeasible-branch

Revert "Symex: resolve pointer comparisons using the value-set"

Author: tautschnig

Diff for: jbmc/regression/jbmc/exception-cleanup/test.desc

@@ -4,8 +4,11 @@ Test.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-0 remaining after simplification$
+1 remaining after simplification$
 --
 ^warning: ignoring
 --
-The function "unreachable" should be successfully noted as unreachable by symex.
+The function "unreachable" should be successfully noted as unreachable by symex,
+but the final uncaught-exception test in __CPROVER__start is not yet decidable
+in symex, as it requires symex to note that within a catch block
+@inflight_exception is definitely *not* null, which it can't just yet.

Diff for: jbmc/regression/jbmc/exception-cleanup/vccs.desc

@@ -3,6 +3,8 @@ Test.class
 --function Test.main --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
+file Test\.java line 6 function java::Test.main:\(I\)V
+no uncaught exception
 --
 file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5
 assertion at file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5

Diff for: regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c

@@ -15,9 +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/sharing_map.h>
 #include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
@@ -89,9 +87,6 @@ class renamedt : private underlyingt
     (void)::simplify(value(), ns);
   }
 
-  using mutator_functiont =
-    std::function<optionalt<renamedt>(const renamedt &)>;
-
 private:
   underlyingt &value()
   {
@@ -103,51 +98,12 @@ class renamedt : private underlyingt
   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());
-  }
-}
-
 /// Functor to set the level 0 renaming of SSA expressions.
 /// Level 0 corresponds to threads.
 /// The renaming is built for one particular interleaving.