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,47 @@ std::size_t goto_statet::increase_generation(
 
   return current_emplace_res.first->second.second;
 }
+
+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

@@ -82,6 +82,11 @@ class goto_statet
     value_set = std::move(other_state.value_set);
   }
 
+  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,28 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/dirty.h>
 #include <util/simplify_expr.h>
 
+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;
@@ -228,6 +250,16 @@ void goto_symext::symex_goto(statet &state)
 
     symex_transition(state, state_pc, backward);
 
+    if(!symex_config.doing_path_exploration)
+    {
+      // In --paths mode we would require the GOTO condition as a constraint
+      // as well, effectively treating the branch like an assumption.
+      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.
         //