Symex: propagate constants implied by assumptions and conditions

When passing `assume(symbol == constant)` or `if symbol == constant then GOTO`, we can populate the
constant propagator accordingly and use that information until the next merge point without that
constraint. We implement this by allocating and defining a fresh L2 generation on this path, which
will be merged as "real", assignment-derived generations are. Symbols are subject to propagation under
the same conditions as they are on assignment (e.g. requiring that they are not subject to concurrent
modification by other threads).

Author: smowton

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>
 
@@ -34,3 +36,59 @@ std::size_t goto_statet::increase_generation(
 
   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
+/// \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

@@ -75,6 +75,11 @@ class goto_statet
   {
   }
 
+  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,

src/goto-symex/goto_symex_state.h

@@ -233,6 +233,11 @@ class goto_symex_statet final : public goto_statet
     level2.current_names.erase(it);
   }
 
+  std::function<std::size_t(const irep_idt &)> get_l2_name_provider() const
+  {
+    return fresh_l2_name_provider;
+  }
+
 private:
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 

src/goto-symex/symex_goto.cpp

@@ -22,6 +22,36 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/dirty.h>
 #include <util/simplify_expr.h>
 
+/// Propagate constants and points-to information implied by a GOTO condition.
+/// See \ref goto_statet::apply_condition for aspects of this which are common
+/// to GOTO and ASSUME instructions.
+/// \param current_state: state prior to the GOTO instruction
+/// \param jump_taken_state: state following taking the GOTO
+/// \param jump_not_taken_state: fall-through state
+/// \param new_guard: GOTO condition, L2 renamed and simplified
+/// \param ns: global namespace
+static void apply_goto_condition(
+  const goto_symex_statet &current_state,
+  goto_statet &jump_taken_state,
+  goto_statet &jump_not_taken_state,
+  const exprt &new_guard,
+  const namespacet &ns)
+{
+  jump_taken_state.apply_condition(new_guard, current_state, ns);
+
+  // Try to find a negative condition that implies an equality constraint on
+  // the branch-not-taken path.
+  // Could use not_exprt + simplify, but let's avoid paying that cost on quite
+  // a hot path:
+  if(new_guard.id() == ID_not)
+    jump_not_taken_state.apply_condition(new_guard.op0(), current_state, ns);
+  else if(new_guard.id() == ID_notequal)
+  {
+    jump_not_taken_state.apply_condition(
+      equal_exprt(new_guard.op0(), new_guard.op1()), current_state, ns);
+  }
+}
+
 void goto_symext::symex_goto(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
@@ -230,6 +260,17 @@ void goto_symext::symex_goto(statet &state)
 
     symex_transition(state, state_pc, backward);
 
+    if(!symex_config.doing_path_exploration)
+    {
+      // This doesn't work for --paths (single-path mode) yet, as in multi-path
+      // mode we remove the implied constants at a control-flow merge, but in
+      // single-path mode we don't run merge_gotos.
+      auto &taken_state = backward ? state : goto_state_list.back().second;
+      auto &not_taken_state = backward ? goto_state_list.back().second : state;
+
+      apply_goto_condition(state, taken_state, not_taken_state, new_guard, ns);
+    }
+
     // produce new guard symbol
     exprt guard_expr;
 

src/goto-symex/symex_main.cpp

@@ -160,6 +160,8 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
   if(state.atomic_section_id!=0 &&
      state.guard.is_false())
     symex_atomic_end(state);
+
+  state.apply_condition(cond, state, ns);
 }
 
 void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)

unit/path_strategies.cpp

@@ -160,23 +160,27 @@ SCENARIO("path strategies")
       "/*  1 */   int main()                          \n"
       "/*  2 */   {                                   \n"
       "/*  3 */     int x;                            \n"
-      "/*  4 */     " CPROVER_PREFIX
-      "assume(x == 1); \n"
+      "/*  4 */     if(x == 1) {                      \n"
       "/*  5 */                                       \n"
-      "/*  6 */     while(x)                          \n"
-      "/*  7 */       --x;                            \n"
+      "/*  6 */       while(x)                        \n"
+      "/*  7 */         --x;                          \n"
       "/*  8 */                                       \n"
-      "/*  9 */     assert(x);                        \n"
-      "/* 10 */   }                                   \n";
+      "/*  9 */       assert(x);                      \n"
+      "/* 10 */     }                                 \n"
+      "/* 11 */   }                                   \n";
     // clang-format on
 
     check_with_strategy(
       "lifo",
       opts_callback,
       c,
       {
+        // The path where x != 1 and we have nothing to check:
+        symex_eventt::resume(symex_eventt::enumt::JUMP, 11),
+
         // The path where we skip the loop body. Successful because the path is
         // implausible, we cannot have skipped the body if x == 1.
+        symex_eventt::resume(symex_eventt::enumt::NEXT, 6),
         symex_eventt::resume(symex_eventt::enumt::JUMP, 9),
         symex_eventt::result(symex_eventt::enumt::SUCCESS),
 
@@ -200,6 +204,12 @@ SCENARIO("path strategies")
       opts_callback,
       c,
       {
+        // First the path where we enter the if-block at line 4 then on hitting
+        // the branch at line 6 consider skipping straight to the end, but find
+        // nothing there to investigate:
+        symex_eventt::resume(symex_eventt::enumt::NEXT, 6),
+        symex_eventt::resume(symex_eventt::enumt::JUMP, 11),
+
         // The path where we skip the loop body. Successful because the path is
         // implausible, we cannot have skipped the body if x == 1.
         //