Symex: propagate assumptions and conditions

jbmc/regression/jbmc/exception-cleanup/Test.java

@@ -0,0 +1,44 @@
+public class Test {
+
+  public static void main(int unknown) {
+
+    try {
+      mayThrow(unknown % 7 == 5);
+    }
+    catch(Exception e) {
+    }
+
+    // This test checks that symex can tell there is no exception in flight
+    // (i.e. @inflight_exception is null) at this point, requiring it to
+    // converge the `if @inflight_exception == null` test on mayThrow's return
+    // with the explicit `@inflight_exception = null;` assignment that concludes
+    // the catch block.
+
+    // If it knows that, it will also know the following catch block is
+    // unreachable; if not it will pursue both paths.
+    try {
+      mayThrow(false);
+    }
+    catch(Exception e) {
+      unreachable();
+    }
+
+    // Try it once more, to check we also know after an unreachable catch that
+    // there is still no inflight exception
+    try {
+      mayThrow(false);
+    }
+    catch(Exception e) {
+      unreachable();
+    }
+
+  }
+
+  public static void mayThrow(boolean shouldThrow) throws Exception {
+    if(shouldThrow)
+      throw new Exception();
+  }
+
+  public static void unreachable() { assert false; }
+
+}

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

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+1 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.

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

@@ -0,0 +1,15 @@
+CORE
+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
+java::Test\.unreachable:\(\)V
+^warning: ignoring
+--
+Supplemental to test.desc, check that the right condition remains to be tested by the solver,
+and the unreachable function indeed does not occur in the VCCs.

regression/cbmc/condition-propagation-1/test.c

@@ -0,0 +1,5 @@
+int main(int argc, char **argv)
+{
+  if(argc == 1)
+    assert(argc == 1);
+}

regression/cbmc/condition-propagation-1/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

regression/cbmc/condition-propagation-2/test.c

@@ -0,0 +1,5 @@
+int main(int argc, char **argv)
+{
+  __CPROVER_assume(argc == 1);
+  assert(argc == 1);
+}

regression/cbmc/condition-propagation-2/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

regression/cbmc/condition-propagation-3/test.c

@@ -0,0 +1,10 @@
+int main(int argc, char **argv)
+{
+  if(argc != 1)
+  {
+  }
+  else
+  {
+    assert(argc == 1);
+  }
+}

regression/cbmc/condition-propagation-3/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

regression/cbmc/condition-propagation-4/test.c

@@ -0,0 +1,15 @@
+int main(int argc, char **argv)
+{
+  int unknown;
+
+  if(argc != 1)
+  {
+  }
+  else
+  {
+    if(unknown == argc)
+    {
+      assert(unknown == 1);
+    }
+  }
+}

regression/cbmc/condition-propagation-4/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

src/goto-symex/goto_state.cpp

@@ -7,6 +7,8 @@ Author: Romain Brenguier, [email protected]
 \*******************************************************************/
 
 #include "goto_state.h"
+#include "goto_symex_is_constant.h"
+#include "goto_symex_state.h"
 
 #include <util/format_expr.h>
 
@@ -20,3 +22,74 @@ void goto_statet::output_propagation_map(std::ostream &out)
     out << name_value.first << " <- " << format(name_value.second) << "\n";
   }
 }
+
+std::size_t goto_statet::increase_generation(
+  const irep_idt l1_identifier,
+  const ssa_exprt &lhs,
+  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
+{
+  auto current_emplace_res =
+    level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0));
+
+  current_emplace_res.first->second.second =
+    fresh_l2_name_provider(l1_identifier);
+
+  return current_emplace_res.first->second.second;
+}
+
+/// Given a condition that must hold on this path, propagate as much knowledge
+/// as possible. For example, if the condition is (x == 5), whether that's an
+/// assumption or a GOTO condition that we just passed through, we can propagate
+/// the constant '5' for future 'x' references. If the condition is (y == &o1)
+/// then we can use that to populate the value set.
+/// \param condition: condition that must hold on this path. Expected to already
+///   be L2-renamed.
+/// \param previous_state: currently active state, not necessarily the same as
+///   *this. For a GOTO instruction this is the state immediately preceding the
+///   branch while *this is the state that will be used on the taken- or
+///   not-taken path. For an ASSUME instruction \p previous_state and *this are
+///   equal.
+/// \param ns: global namespace
+void goto_statet::apply_condition(
+  const exprt &condition,
+  const goto_symex_statet &previous_state,
+  const namespacet &ns)
+{
+  if(condition.id() == ID_and)
+  {
+    for(const auto &op : condition.operands())
+      apply_condition(op, previous_state, ns);
+  }
+  else if(condition.id() == ID_equal)
+  {
+    exprt lhs = condition.op0();
+    exprt rhs = condition.op1();
+    if(is_ssa_expr(rhs))
+      std::swap(lhs, rhs);
+
+    if(is_ssa_expr(lhs) && goto_symex_is_constantt()(rhs))
+    {
+      const ssa_exprt &ssa_lhs = to_ssa_expr(lhs);
+      INVARIANT(
+        !ssa_lhs.get_level_2().empty(),
+        "apply_condition operand should be L2 renamed");
+
+      if(
+        previous_state.threads.size() == 1 ||
+        previous_state.write_is_shared(ssa_lhs, ns) !=
+          goto_symex_statet::write_is_shared_resultt::SHARED)
+      {
+        ssa_exprt l1_lhs = ssa_lhs;
+        l1_lhs.remove_level_2();
+        const irep_idt &l1_identifier = l1_lhs.get_identifier();
+
+        increase_generation(
+          l1_identifier, l1_lhs, previous_state.get_l2_name_provider());
+
+        propagation[l1_identifier] = rhs;
+
+        value_set.assign(l1_lhs, rhs, ns, true, false);
+      }
+    }
+  }
+}

src/goto-symex/goto_state.h

@@ -74,6 +74,16 @@ class goto_statet
     : guard(true_exprt(), guard_manager)
   {
   }
+
+  void apply_condition(
+    const exprt &condition, // L2
+    const goto_symex_statet &previous_state,
+    const namespacet &ns);
+
+  std::size_t increase_generation(
+    const irep_idt l1_identifier,
+    const ssa_exprt &lhs,
+    std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H

src/goto-symex/goto_symex_is_constant.h

@@ -0,0 +1,53 @@
+/*******************************************************************\
+
+Module: Symbolic Execution Constant Propagation
+
+Author: Michael Tautschig, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// GOTO Symex constant propagation
+
+#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
+#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H
+
+#include <util/expr.h>
+#include <util/expr_util.h>
+
+class goto_symex_is_constantt : public is_constantt
+{
+protected:
+  bool is_constant(const exprt &expr) const override
+  {
+    if(expr.id() == ID_mult)
+    {
+      // propagate stuff with sizeof in it
+      forall_operands(it, expr)
+      {
+        if(it->find(ID_C_c_sizeof_type).is_not_nil())
+          return true;
+        else if(!is_constant(*it))
+          return false;
+      }
+
+      return true;
+    }
+    else if(expr.id() == ID_with)
+    {
+      // this is bad
+      /*
+      forall_operands(it, expr)
+      if(!is_constant(expr.op0()))
+      return false;
+
+      return true;
+      */
+      return false;
+    }
+
+    return is_constantt::is_constant(expr);
+  }
+};
+
+#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H