goto-symex: apply_condition should not change L2 index

regression/cbmc/apply_condition2/main.c

@@ -0,0 +1,12 @@
+int main()
+{
+  int s;
+
+  int i = 0;
+  if(i != s)
+    ++i;
+  else
+    __CPROVER_assert(s == 0, "constant propagate");
+
+  int s2 = s;
+}

regression/cbmc/apply_condition2/test.desc

@@ -0,0 +1,12 @@
+CORE paths-lifo-expected-failure
+main.c
+--program-only
+s2!0@1#2 == s!0@1#1
+^EXIT=0$
+^SIGNAL=0$
+--
+ASSERT
+s2!0@1#[3-9]
+--
+The branch condition should yield constant propagation on s without introducing
+fresh assignments to s.

regression/validate-trace-xml-schema/check.py

@@ -38,6 +38,7 @@
     ['Quantifiers-simplify', 'simplify_not_forall.desc'],
     ['array-cell-sensitivity15', 'test.desc'],
     ['saturating_arithmetric', 'output-formula.desc'],
+    ['apply_condition2', 'test.desc'],
     # these test for invalid command line handling
     ['bad_option', 'test_multiple.desc'],
     ['bad_option', 'test.desc'],

src/goto-symex/goto_state.cpp

@@ -107,14 +107,11 @@
         const ssa_exprt l1_lhs = remove_level_2(ssa_lhs);
         const irep_idt &l1_identifier = l1_lhs.get_identifier();
 
-        level2.increase_generation(
-          l1_identifier, l1_lhs, previous_state.get_l2_name_provider());
-
-        const auto propagation_entry = propagation.find(l1_identifier);
+        const auto propagation_entry = branch_propagation.find(l1_identifier);
         if(!propagation_entry.has_value())
-          propagation.insert(l1_identifier, rhs);
+          branch_propagation.insert(l1_identifier, rhs);
         else if(propagation_entry->get() != rhs)
-          propagation.replace(l1_identifier, rhs);
+          branch_propagation.replace(l1_identifier, rhs);
 
         value_set.assign(l1_lhs, rhs, ns, true, false);
       }

src/goto-symex/goto_state.h

@@ -68,7 +68,10 @@ class goto_statet
   // "constants" can include symbols, but only in the context of an address-of
   // op (i.e. &x can be propagated), and an address-taken thing should only be
   // L1.
-  sharing_mapt<irep_idt, exprt> propagation;
+  //
+  // Entries in branch_propagation are local to the current branch and will
+  // never be merged back in phi nodes.
+  sharing_mapt<irep_idt, exprt> propagation, branch_propagation;
 
   void output_propagation_map(std::ostream &);
 

src/goto-symex/goto_symex.cpp

@@ -372,15 +372,19 @@
     return {};
   }
 
-  const auto s_pointer_opt =
-    state.propagation.find(to_symbol_expr(content).get_identifier());
+  const irep_idt &content_id = to_symbol_expr(content).get_identifier();
 
-  if(!s_pointer_opt)
-  {
-    return {};
-  }
+  const auto s_pointer_opt = state.propagation.find(content_id);
+
+  if(s_pointer_opt)
+    return try_get_string_data_array(s_pointer_opt->get(), ns);
+
+  const auto b_entry = state.branch_propagation.find(content_id);
+
+  if(b_entry)
+    return try_get_string_data_array(b_entry->get(), ns);
 
-  return try_get_string_data_array(s_pointer_opt->get(), ns);
+  return {};
 }
 
 std::optional<std::reference_wrapper<const constant_exprt>>
@@ -391,16 +395,25 @@
     return {};
   }
 
-  const auto constant_expr_opt =
-    state.propagation.find(to_symbol_expr(expr).get_identifier());
+  const irep_idt &expr_id = to_symbol_expr(expr).get_identifier();
 
-  if(!constant_expr_opt || !constant_expr_opt->get().is_constant())
+  const auto constant_expr_opt = state.propagation.find(expr_id);
+
+  if(constant_expr_opt && constant_expr_opt->get().is_constant())
   {
-    return {};
+    return std::optional<std::reference_wrapper<const constant_exprt>>(
+      to_constant_expr(constant_expr_opt->get()));
+  }
+
+  const auto b_entry = state.branch_propagation.find(expr_id);
+
+  if(b_entry && b_entry->get().id() == ID_constant)
+  {
+    return std::optional<std::reference_wrapper<const constant_exprt>>(
+      to_constant_expr(b_entry->get()));
   }
 
-  return std::optional<std::reference_wrapper<const constant_exprt>>(
-    to_constant_expr(constant_expr_opt->get()));
+  return {};
 }
 
 void goto_symext::constant_propagate_empty_string(

src/goto-symex/goto_symex_state.cpp

@@ -112,6 +112,7 @@ renamedt<ssa_exprt, L2> goto_symex_statet::assignment(
       "pointer handling for concurrency is unsound");
 
   // Update constant propagation map -- the RHS is L2
+  branch_propagation.erase_if_exists(l1_identifier);
   if(!is_shared && record_value && goto_symex_can_forward_propagatet(ns)(rhs))
   {
     const auto propagation_entry = propagation.find(l1_identifier);
@@ -214,14 +215,19 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       {
         // We also consider propagation if we go up to L2.
         // L1 identifiers are used for propagation!
-        auto p_it = propagation.find(ssa.get_identifier());
+        const auto &l1_identifier = ssa.get_identifier();
+        auto p_it = propagation.find(l1_identifier);
 
         if(p_it.has_value())
         {
           return renamedt<exprt, level>(*p_it); // already L2
         }
         else
         {
+          auto b_entry = branch_propagation.find(l1_identifier);
+          if(b_entry.has_value())
+            return renamedt<exprt, level>(*b_entry);
+
           if(level == L2)
             ssa = set_indices<L2>(std::move(ssa), ns).get();
           return renamedt<exprt, level>(std::move(ssa));
@@ -457,7 +463,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
     // written this object within the atomic section. We must actually do this,
     // because goto_state::apply_condition may have placed the latest value in
     // the propagation map without recording an assignment.
-    auto p_it = propagation.find(ssa_l1.get_identifier());
+    auto p_it = branch_propagation.find(ssa_l1.get_identifier());
     const exprt l2_true_case =
       p_it.has_value() ? *p_it : set_indices<L2>(ssa_l1, ns).get();
 

src/goto-symex/symex_dead.cpp

@@ -41,6 +41,7 @@ static void remove_l1_object_rec(
       state.value_set.values.erase_if_exists(l1_identifier);
     }
     state.propagation.erase_if_exists(l1_identifier);
+    state.branch_propagation.erase_if_exists(l1_identifier);
     // Remove from the local L2 renaming map; this means any reads from the dead
     // identifier will use generation 0 (e.g. x!N@M#0, where N and M are
     // positive integers), which is never defined by any write, and will be

src/goto-symex/symex_goto.cpp

@@ -799,7 +799,13 @@ static void merge_names(
     if(p_it.has_value())
       goto_state_rhs = *p_it;
     else
-      to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
+    {
+      auto b_entry = goto_state.branch_propagation.find(l1_identifier);
+      if(b_entry.has_value())
+        goto_state_rhs = *b_entry;
+      else
+        to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
+    }
   }
 
   {
@@ -808,7 +814,13 @@ static void merge_names(
     if(p_it.has_value())
       dest_state_rhs = *p_it;
     else
-      to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
+    {
+      auto b_entry = dest_state.branch_propagation.find(l1_identifier);
+      if(b_entry.has_value())
+        dest_state_rhs = *b_entry;
+      else
+        to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
+    }
   }
 
   exprt rhs;
@@ -921,6 +933,12 @@ void goto_symext::phi_function(
       goto_count,
       dest_count);
   }
+
+  sharing_mapt<irep_idt, exprt>::delta_viewt bp_delta_view =
+    dest_state.branch_propagation.get_delta_view(
+      goto_state.branch_propagation, false);
+  for(const auto &delta_item : bp_delta_view)
+    dest_state.branch_propagation.erase(delta_item.k);
 }
 
 void goto_symext::loop_bound_exceeded(

unit/goto-symex/apply_condition.cpp

@@ -60,7 +60,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'true'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == true_exprt{});
@@ -74,7 +74,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'false'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == false_exprt{});
@@ -88,7 +88,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'true'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == true_exprt{});
@@ -102,7 +102,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'false'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == false_exprt{});
@@ -116,7 +116,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'false'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == false_exprt{});
@@ -130,7 +130,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'true'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == true_exprt{});
@@ -144,7 +144,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'false'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == false_exprt{});
@@ -158,7 +158,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'true'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == true_exprt{});
@@ -172,7 +172,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'true'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == true_exprt{});
@@ -186,7 +186,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'false'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == false_exprt{});
@@ -200,7 +200,7 @@ SCENARIO(
 
     THEN("b should be in the constant propagator with value 'true'")
     {
-      auto it = goto_state.propagation.find(
+      auto it = goto_state.branch_propagation.find(
         to_ssa_expr(renamed_b).get_l1_object_identifier());
       REQUIRE(it);
       REQUIRE(it->get() == true_exprt{});