Symex: resolve pointer comparisons using the value-set

jbmc/regression/jbmc/exception-cleanup/test.desc

@@ -4,11 +4,8 @@ Test.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-1 remaining after simplification$
+0 remaining after simplification$
 --
 ^warning: ignoring
 --
-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.
+The function "unreachable" should be successfully noted as unreachable by symex.

jbmc/regression/jbmc/exception-cleanup/vccs.desc

@@ -3,8 +3,6 @@ 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

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.c

@@ -0,0 +1,181 @@
+#include <assert.h>
+
+static void noop()
+{
+}
+
+int test(int nondet_int_array[])
+{
+  int a = 1, b = 2, c = 3;
+  int *ptr_to_a = &a, *ptr_to_b = &b, *ptr_to_c = &c, *ptr_to_null = 0;
+
+  // Symex knows the value of ptr_to_a, ptr_to_b, ptr_to_c and ptr_to_null, so
+  // it should be able to evaluate simple conditions involving them.
+
+  // Equality "=="
+
+  // A non-null pointer and a matching value
+  int unconditionally_reachable_1;
+  if(ptr_to_a == &a)
+    unconditionally_reachable_1 = 7;
+
+  // A non-null pointer and a non-matching value (not a null pointer)
+  int unreachable_1;
+  if(ptr_to_a == &c)
+    unreachable_1 = 7;
+
+  // A non-null pointer and a non-matching value (a null pointer)
+  int unreachable_2;
+  if(ptr_to_a == 0)
+    unreachable_2 = 7;
+
+  // A null pointer and a matching value
+  int unconditionally_reachable_2;
+  if(ptr_to_null == 0)
+    unconditionally_reachable_2 = 7;
+
+  // A null pointer and a non-matching value
+  int unreachable_3;
+  if(ptr_to_null == &a)
+    unreachable_3 = 7;
+
+  // Disequality "!="
+
+  // A non-null pointer and a matching value
+  int unreachable_4;
+  if(ptr_to_a != &a)
+    unreachable_4 = 7;
+
+  // A non-null pointer and a non-matching value (not a null pointer)
+  int unconditionally_reachable_3;
+  if(ptr_to_a != &c)
+    unconditionally_reachable_3 = 7;
+
+  // A non-null pointer and a non-matching value (a null pointer)
+  int unconditionally_reachable_4;
+  if(ptr_to_a != 0)
+    unconditionally_reachable_4 = 7;
+
+  // A null pointer and a matching value
+  int unreachable_5;
+  if(ptr_to_null != 0)
+    unreachable_5 = 7;
+
+  // A null pointer and a non-matching value
+  int unconditionally_reachable_5;
+  if(ptr_to_null != &a)
+    unconditionally_reachable_5 = 7;
+
+  // Symex can't tell what ptr_to_a_or_b points to, but we can tell that it
+  // doesn't point to some things
+  int *ptr_to_a_or_b = nondet_int_array[0] == 0 ? &a : &b;
+  int *ptr_to_a_or_b_or_null =
+    nondet_int_array[1] == 0 ? &a : nondet_int_array[1] == 1 ? &b : 0;
+
+  // Equality "=="
+
+  // A non-null pointer and a matching value
+  int possibly_reachable_1;
+  if(ptr_to_a_or_b == &a)
+    possibly_reachable_1 = 7;
+
+  // A non-null pointer and a non-matching value (not a null pointer)
+  int unreachable_6;
+  if(ptr_to_a_or_b == &c)
+    unreachable_6 = 7;
+
+  // A non-null pointer and a non-matching value (a null pointer)
+  int unreachable_7;
+  if(ptr_to_a_or_b == 0)
+    unreachable_7 = 7;
+
+  // A possibly-null pointer and a matching value (not a null pointer)
+  int possibly_reachable_2;
+  if(ptr_to_a_or_b_or_null == &a)
+    possibly_reachable_2 = 7;
+
+  // A possibly-null pointer and a matching value (a null pointer)
+  int possibly_reachable_3;
+  if(ptr_to_a_or_b_or_null == 0)
+    possibly_reachable_3 = 7;
+
+  // A possibly-null pointer and a non-matching value
+  int unreachable_8;
+  if(ptr_to_a_or_b_or_null == &c)
+    unreachable_8 = 7;
+
+  // Disequality "!="
+
+  // A non-null pointer and a matching value
+  int possibly_reachable_4;
+  if(ptr_to_a_or_b != &a)
+    possibly_reachable_4 = 7;
+
+  // A non-null pointer and a non-matching value (not a null pointer)
+  int unconditionally_reachable_6;
+  if(ptr_to_a_or_b != &c)
+    unconditionally_reachable_6 = 7;
+
+  // A non-null pointer and a non-matching value (a null pointer)
+  int unconditionally_reachable_7;
+  if(ptr_to_a_or_b != 0)
+    unconditionally_reachable_7 = 7;
+
+  // A possibly-null pointer and a matching value (not a null pointer)
+  int possibly_reachable_5;
+  if(ptr_to_a_or_b_or_null != &a)
+    possibly_reachable_5 = 7;
+
+  // A possibly-null pointer and a matching value (a null pointer)
+  int possibly_reachable_6;
+  if(ptr_to_a_or_b_or_null != 0)
+    possibly_reachable_6 = 7;
+
+  // A possibly-null pointer and a non-matching value
+  int unconditionally_reachable_8;
+  if(ptr_to_a_or_b_or_null != &c)
+    unconditionally_reachable_8 = 7;
+
+  // We should also be able to do all of the above in compound expressions which
+  // use logical operators like AND, OR and NOT, or even ternary expressions.
+
+  int unconditionally_reachable_9;
+  if(!(ptr_to_a == &c) && ptr_to_a_or_b != 0)
+    unconditionally_reachable_9 = 7;
+
+  int unreachable_9;
+  if(!(ptr_to_null == 0) || ptr_to_a_or_b == 0)
+    unreachable_9 = 7;
+
+  int unconditionally_reachable_10;
+  if((ptr_to_a == &a && !(ptr_to_a_or_b == 0)) || ptr_to_a_or_b_or_null == &c)
+    unconditionally_reachable_10 = 7;
+
+  int unreachable_10;
+  if(ptr_to_a_or_b_or_null != 0 ? ptr_to_null != 0 : ptr_to_a_or_b == &c)
+    unreachable_10 = 7;
+
+  // And everything should work with the symbol on the left or the right
+
+  int unconditionally_reachable_11;
+  if(!(&c == ptr_to_a) && 0 != ptr_to_a_or_b)
+    unconditionally_reachable_11 = 7;
+
+  int unreachable_11;
+  if(!(0 == ptr_to_null) || 0 == ptr_to_a_or_b)
+    unreachable_11 = 7;
+
+  int unconditionally_reachable_12;
+  if((&a == ptr_to_a && !(0 == ptr_to_a_or_b)) || &c == ptr_to_a_or_b_or_null)
+    unconditionally_reachable_12 = 7;
+
+  int unreachable_12;
+  if(0 != ptr_to_a_or_b_or_null ? 0 != ptr_to_null : &c == ptr_to_a_or_b)
+    unreachable_12 = 7;
+
+  int possibly_reachable_7;
+  if(0 != ptr_to_a_or_b_or_null)
+    possibly_reachable_7 = 7;
+
+  assert(0);
+}

regression/cbmc/symex_should_evaluate_simple_pointer_conditions/test.desc

@@ -0,0 +1,60 @@
+CORE paths-lifo-expected-failure
+test.c
+--function test --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+test::1::unconditionally_reachable_1[^\s]+ = 7$
+test::1::unconditionally_reachable_2[^\s]+ = 7$
+test::1::unconditionally_reachable_3[^\s]+ = 7$
+test::1::unconditionally_reachable_4[^\s]+ = 7$
+test::1::unconditionally_reachable_5[^\s]+ = 7$
+test::1::unconditionally_reachable_6[^\s]+ = 7$
+test::1::unconditionally_reachable_7[^\s]+ = 7$
+test::1::unconditionally_reachable_8[^\s]+ = 7$
+test::1::unconditionally_reachable_9[^\s]+ = 7$
+test::1::unconditionally_reachable_10[^\s]+ = 7$
+test::1::possibly_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_1[^\s]+\)$
+test::1::possibly_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_2[^\s]+\)$
+test::1::possibly_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_3[^\s]+\)$
+test::1::possibly_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_4[^\s]+\)$
+test::1::possibly_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_5[^\s]+\)$
+test::1::possibly_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_6[^\s]+\)$
+test::1::possibly_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::possibly_reachable_7[^\s]+\)$
+--
+test::1::unconditionally_reachable_1[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_1[^\s]+\)$
+test::1::unconditionally_reachable_2[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_2[^\s]+\)$
+test::1::unconditionally_reachable_3[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_3[^\s]+\)$
+test::1::unconditionally_reachable_4[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_4[^\s]+\)$
+test::1::unconditionally_reachable_5[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_5[^\s]+\)$
+test::1::unconditionally_reachable_6[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_6[^\s]+\)$
+test::1::unconditionally_reachable_7[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_7[^\s]+\)$
+test::1::unconditionally_reachable_8[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_8[^\s]+\)$
+test::1::unconditionally_reachable_9[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_9[^\s]+\)$
+test::1::unconditionally_reachable_10[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_10[^\s]+\)$
+test::1::unconditionally_reachable_11[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_11[^\s]+\)$
+test::1::unconditionally_reachable_12[^\s]+ = \(goto_symex::\\guard[^\s]+ \? 7 : test::1::unconditionally_reachable_12[^\s]+\)$
+test::1::unreachable_1[^\s]+ = 7$
+test::1::unreachable_2[^\s]+ = 7$
+test::1::unreachable_3[^\s]+ = 7$
+test::1::unreachable_4[^\s]+ = 7$
+test::1::unreachable_5[^\s]+ = 7$
+test::1::unreachable_6[^\s]+ = 7$
+test::1::unreachable_7[^\s]+ = 7$
+test::1::unreachable_8[^\s]+ = 7$
+test::1::unreachable_9[^\s]+ = 7$
+test::1::unreachable_10[^\s]+ = 7$
+test::1::unreachable_11[^\s]+ = 7$
+test::1::unreachable_12[^\s]+ = 7$
+^warning: ignoring
+unreachable_1[3-9]
+unreachable[2-9][0-9]
+unconditionally_reachable_1[3-9]
+unconditionally_reachable[2-9][0-9]
+possibly_reachable_[8-9]
+possibly_reachable_[1-9][0-9]
+--
+Pointer comparisons will be resolved in symex by a mixture of constant
+propagation and value-set filtering in try_evaluate_pointer_comparisons.
+
+The expected failure for path-symex is because the lines we check for
+possibly_reachable_* would only appear when there is convergence behaviour.

src/goto-symex/renaming_level.h

@@ -15,7 +15,9 @@ 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>
@@ -87,6 +89,9 @@ class renamedt : private underlyingt
     (void)::simplify(value(), ns);
   }
 
+  using mutator_functiont =
+    std::function<optionalt<renamedt>(const renamedt &)>;
+
 private:
   underlyingt &value()
   {
@@ -98,12 +103,51 @@ 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.