goto-symex: apply_condition should not change L2 index

Updating the L2 index would result in additional phi assignments, which
can result in more costly verification. One such example is that the use
of `i != size` instead of `i < size` in loop conditions resulted
increased verification time when we would expect not-equal to be cheaper
than less-than.

Author: tautschnig

regression/cbmc-cover/pointer-function-parameters/test.desc

@@ -5,7 +5,7 @@ main.c
 ^Test suite:$
 ^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$
 ^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0@1)$
-^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0@1)$
+^(a=&tmp(\$\d+)?!0@1, tmp(\$\d+)?=(-?[012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=(-?[012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0@1)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

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

@@ -106,14 +106,11 @@ void goto_statet::apply_condition(
         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

@@ -354,15 +354,19 @@ goto_symext::try_evaluate_constant_string(
     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 {};
 }
 
 optionalt<std::reference_wrapper<const constant_exprt>>
@@ -373,16 +377,25 @@ goto_symext::try_evaluate_constant(const statet &state, const exprt &expr)
     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 optionalt<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 optionalt<std::reference_wrapper<const constant_exprt>>(
+      to_constant_expr(b_entry->get()));
   }
 
-  return optionalt<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

@@ -110,6 +110,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_is_constantt(ns)(rhs))
   {
     const auto propagation_entry = propagation.find(l1_identifier);
@@ -212,14 +213,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));
@@ -430,7 +436,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{});