Skip phi assignment if neither merged state has an initialised object

With non-deterministic initialisation performed on declaration and allocation,
the only remaining sources are pointer dereferencing, where uninitialised
objects necessarily refer to invalid objects.

This is a cleaner implementation of 369f077 as well as removing the dubious
init_l1 from "Explicitly initialise non-static objects with non-deterministic
values".

Author: tautschnig

src/goto-symex/goto_symex.h

@@ -271,8 +271,6 @@ class goto_symext
   irep_idt guard_identifier;
 
   // symex
-  irep_idt init_l1;
-
   virtual void symex_transition(
     statet &,
     goto_programt::const_targett to,

src/goto-symex/symex_assign.cpp

@@ -199,26 +199,6 @@ void goto_symext::symex_assign_symbol(
   guardt &guard,
   assignment_typet assignment_type)
 {
-  // do not assign to L1 objects that have gone out of scope --
-  // pointer dereferencing may yield such objects; parameters do not
-  // have an L2 entry set up beforehand either, so exempt them from
-  // this check (all other L1 objects should have seen a declaration)
-  const symbolt *s;
-  if(
-    init_l1 != lhs.get_identifier() && !ns.lookup(lhs.get_object_name(), s) &&
-    !s->is_parameter && !lhs.get_level_1().empty() &&
-    state.level2.current_count(lhs.get_identifier()) == 0)
-  {
-    return;
-  }
-  else if(init_l1 == lhs.get_identifier())
-  {
-    // the assignment about to happen is the initialisation, clear the
-    // identifier to make sure future steps are not treated as initialisation
-    // steps (and we thus cannot reach the early return above
-    init_l1.clear();
-  }
-
   exprt ssa_rhs=rhs;
 
   // put assignment guard into the rhs

src/goto-symex/symex_decl.cpp

@@ -55,7 +55,6 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   if(state.level2.current_names.find(l1_identifier)==
      state.level2.current_names.end())
     state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
-  init_l1 = l1_identifier;
 
   // optimisation: skip non-deterministic initialisation if the next instruction
   // will take care of initialisation (but ensure int x=x; is handled properly)

src/goto-symex/symex_goto.cpp

@@ -447,17 +447,23 @@ void goto_symext::phi_function(
     //  1. Either guard is false, so we can't follow that branch.
     //  2. Either identifier is of generation zero, and so hasn't been
     //     initialized and therefor an invalid target.
-    if(dest_state.guard.is_false())
-      rhs=goto_state_rhs;
-    else if(goto_state.guard.is_false())
-      rhs=dest_state_rhs;
-    else if(goto_state.level2_current_count(l1_identifier) == 0)
+    if(
+      dest_state.guard.is_false() ||
+      dest_state.level2.current_count(l1_identifier) == 0)
     {
-      rhs = dest_state_rhs;
+      if(goto_state.level2_current_count(l1_identifier) == 0)
+        continue;
+
+      rhs=goto_state_rhs;
     }
-    else if(dest_state.level2.current_count(l1_identifier) == 0)
+    else if(
+      goto_state.guard.is_false() ||
+      goto_state.level2_current_count(l1_identifier) == 0)
     {
-      rhs = goto_state_rhs;
+      if(dest_state.level2.current_count(l1_identifier) == 0)
+        continue;
+
+      rhs=dest_state_rhs;
     }
     else
     {