Merge pull request #4407 from smowton/smowton/feature/dead-always-uses-generation-zero

Symex code_deadt: always use L2 generation zero

Author: smowton

jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.withDependency  --max-nondet-string-length 10000
+--function Test.withDependency  --max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 48 .*: SUCCESS

jbmc/regression/jbmc/throwing-function-return-value/test.desc

@@ -3,11 +3,13 @@ Test.class
 --function Test.main --show-vcc
 java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\d+\)
 java::Test\.main:\(Z\)V::9::x!0@1#\d+ = 5 \+ java::Test\.main:\(Z\)V::9::x!0@1#\d+
+java::Test\.g:\(\)I#return_value!0#[0-9]+ = 5
 ^EXIT=0$
 ^SIGNAL=0$
 --
 return_value!0#0
 java::Sub\.g:\(\)
+java::Test\.g:\(\)I#return_value!0#[0-9]+ = [^5]
 --
 This checks that when a function may throw, we can nonetheless constant-propagate
 and populate the value-set for the normal-return path. In particular we don't
@@ -16,3 +18,6 @@ reading the return-value when not defined), nor do we expect to see any code
 from the Sub class, which is not accessible and can only be reached when
 constant propagation has lost information to the point we're not sure which type
 virtual calls against Test may find.
+The final check ensures there is no uncertainty about whether Test.g() may throw,
+which would result in a nondet return-value (corresponding to the hypothetical
+throwing path).

src/goto-symex/goto_symex_state.cpp

@@ -469,19 +469,6 @@ bool goto_symex_statet::l2_thread_read_encoding(
   return true;
 }
 
-/// Allocates a fresh L2 name for the given L1 identifier, and makes it the
-/// latest generation on this path. Does nothing if there isn't an expression
-/// keyed by the l1 identifier.
-void goto_symex_statet::increase_generation_if_exists(const irep_idt identifier)
-{
-  // If we can't find the name in the local scope, this is a no-op.
-  auto current_names_iter = level2.current_names.find(identifier);
-  if(current_names_iter == level2.current_names.end())
-    return;
-
-  current_names_iter->second.second = fresh_l2_name_provider(identifier);
-}
-
 goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
   const ssa_exprt &expr,
   const namespacet &ns) const

src/goto-symex/goto_symex_state.h

@@ -223,16 +223,18 @@ class goto_symex_statet final : public goto_statet
       l1_identifier, lhs, fresh_l2_name_provider);
   }
 
-  /// Increases the generation of the L1 identifier. Does nothing if there
-  /// isn't an expression keyed by it.
-  void increase_generation_if_exists(const irep_idt identifier);
-
   /// Drops an L1 name from the local L2 map
   void drop_l1_name(symex_renaming_levelt::current_namest::const_iterator it)
   {
     level2.current_names.erase(it);
   }
 
+  /// Drops an L1 name from the local L2 map
+  void drop_l1_name(const irep_idt &l1_identifier)
+  {
+    level2.current_names.erase(l1_identifier);
+  }
+
   std::function<std::size_t(const irep_idt &)> get_l2_name_provider() const
   {
     return fresh_l2_name_provider;

src/goto-symex/symex_dead.cpp

@@ -30,7 +30,10 @@ void goto_symext::symex_dead(statet &state)
   // can no longer appear
   state.value_set.values.erase(l1_identifier);
   state.propagation.erase(l1_identifier);
-  // increment the L2 index to ensure a merge on join points will propagate the
-  // value for branches that are still live
-  state.increase_generation_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 dropped by
+  // `goto_symext::merge_goto` on merging with branches where the identifier
+  // is still live.
+  state.drop_l1_name(l1_identifier);
 }