L1 renaming at each declaration

This was done up until c8f0f7b.

Author: tautschnig

regression/cbmc/Local_out_of_scope4/main.c

@@ -0,0 +1,10 @@
+int g;
+
+int main()
+{
+  for(int i = 0; i < 4; ++i)
+  {
+    int *x;
+    *&x = &g;
+  }
+}

regression/cbmc/Local_out_of_scope4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-programs/goto_clean_expr.cpp

@@ -45,7 +45,8 @@ symbol_exprt goto_convertt::make_compound_literal(
 
   // The lifetime of compound literals is really that of
   // the block they are in.
-  copy(code_declt(result), DECL, dest);
+  if(!new_symbol.is_static_lifetime)
+    copy(code_declt(result), DECL, dest);
 
   code_assignt code_assign(result, expr);
   code_assign.add_source_location()=source_location;

src/goto-symex/goto_symex_state.cpp

@@ -785,3 +785,34 @@ void goto_symex_statet::output_propagation_map(std::ostream &out)
     out << name_value.first << " <- " << format(name_value.second) << "\n";
   }
 }
+
+void goto_symex_statet::add_object(
+  ssa_exprt &ssa,
+  std::size_t l1_index,
+  const namespacet &ns)
+{
+  framet &frame = top();
+
+  const irep_idt l0_name = ssa.get_identifier();
+
+  // save old L1 name, if any
+  auto c_it = level1.current_names.find(l0_name);
+
+  if(c_it != level1.current_names.end())
+  {
+    frame.old_level1[l0_name] = c_it->second;
+    c_it->second = std::make_pair(ssa, l1_index);
+  }
+  else
+  {
+    c_it = level1.current_names.emplace(l0_name, std::make_pair(ssa, l1_index))
+             .first;
+  }
+
+  rename(ssa, ns, goto_symex_statet::L1);
+  const irep_idt &l1_name = ssa.get_identifier();
+
+  // unique -- store
+  if(!frame.local_objects.insert(l1_name).second)
+    PRECONDITION(false);
+}

src/goto-symex/goto_symex_state.h

@@ -58,9 +58,6 @@ class goto_symex_statet final
   symex_targett::sourcet source;
   symex_target_equationt *symex_target;
 
-  // we remember all L1 renamings
-  std::set<irep_idt> l1_history;
-
   symex_level0t level0;
   symex_level1t level1;
   symex_level2t level2;
@@ -239,6 +236,10 @@ class goto_symex_statet final
 
   const framet &previous_frame() { return *(--(--call_stack().end())); }
 
+  /// Turn L0-renamed \p ssa into an L1-renamed SSA expression with an L1 index
+  /// \p l1_index that must not have previously been used.
+  void add_object(ssa_exprt &ssa, std::size_t l1_index, const namespacet &ns);
+
   void print_backtrace(std::ostream &) const;
 
   // threads

src/goto-symex/path_storage.h

@@ -85,11 +85,24 @@ class path_storaget
     return size() == 0;
   };
 
+  /// Provide a unique index for a given \p id, starting from \p minimum_index.
+  std::size_t get_unique_index(const irep_idt &id, std::size_t minimum_index)
+  {
+    auto entry = unique_index_map.emplace(id, minimum_index);
+
+    if(!entry.second)
+      entry.first->second = std::max(entry.first->second + 1, minimum_index);
+
+    return entry.first->second;
+  }
+
 private:
   // Derived classes should override these methods, allowing the base class to
   // enforce preconditions.
   virtual patht &private_peek() = 0;
   virtual void private_pop() = 0;
+
+  std::unordered_map<irep_idt, std::size_t> unique_index_map;
 };
 
 /// \brief LIFO save queue: depth-first search, try to finish paths

src/goto-symex/symex_dead.cpp

@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_symex.h"
 
-#include <cassert>
-
 #include <util/std_expr.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
@@ -23,9 +21,6 @@ void goto_symext::symex_dead(statet &state)
 
   const code_deadt &code = to_code_dead(instruction.code);
 
-  // We increase the L2 renaming to make these non-deterministic.
-  // We also prevent propagation of old values.
-
   ssa_exprt ssa(code.symbol());
   state.rename(ssa, ns, goto_symex_statet::L1);
 
@@ -45,14 +40,13 @@ void goto_symext::symex_dead(statet &state)
     state.value_set.assign(ssa, rhs, ns, true, false);
   }
 
-  ssa_exprt ssa_lhs=to_ssa_expr(ssa);
-  const irep_idt &l1_identifier=ssa_lhs.get_identifier();
-
-  // prevent propagation
-  state.propagation.erase(l1_identifier);
-
-  // L2 renaming
-  auto level2_it = state.level2.current_names.find(l1_identifier);
+  // would be nicer to do
+  // state.remove_object(ssa, ns);
+  // but the l1 renaming information is not local to a path
+  state.propagation.erase(ssa.get_identifier());
+  // increment the L2 index to ensure a merge on join points will propagate the
+  // value for branches that are still live
+  auto level2_it = state.level2.current_names.find(ssa.get_identifier());
   if(level2_it != state.level2.current_names.end())
     symex_renaming_levelt::increase_counter(level2_it);
 }

src/goto-symex/symex_decl.cpp

@@ -34,11 +34,14 @@ void goto_symext::symex_decl(statet &state)
 
 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
 {
-  // We increase the L2 renaming to make these non-deterministic.
-  // We also prevent propagation of old values.
+  // each declaration introduces a new object, which we record as a fresh L1
+  // index
 
   ssa_exprt ssa(expr);
-  state.rename(ssa, ns, goto_symex_statet::L1);
+  state.rename(ssa, ns, goto_symex_statet::L0);
+  const std::size_t fresh_l1_index =
+    path_storage.get_unique_index(ssa.get_identifier(), 1);
+  state.add_object(ssa, fresh_l1_index, ns);
   const irep_idt &l1_identifier=ssa.get_identifier();
 
   // rename type to L2
@@ -62,16 +65,10 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     state.value_set.assign(ssa, rhs, ns, true, false);
   }
 
-  // prevent propagation
-  state.propagation.erase(l1_identifier);
-
   // L2 renaming
-  // inlining may yield multiple declarations of the same identifier
-  // within the same L1 context
-  const auto level2_it =
-    state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 0))
-      .first;
-  symex_renaming_levelt::increase_counter(level2_it);
+  if(!state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 1))
+        .second)
+    CHECK_RETURN(false);
   const bool record_events=state.record_events;
   state.record_events=false;
   state.rename(ssa, ns);

src/goto-symex/symex_function_call.cpp

@@ -376,8 +376,8 @@ void goto_symext::symex_end_of_function(statet &state)
   pop_frame(state);
 }
 
-/// preserves locality of local variables of a given function by applying L1
-/// renaming to the local identifiers
+/// preserves locality of parameters of a given function by applying L1
+/// renaming to them
 void goto_symext::locality(
   const irep_idt &function_identifier,
   statet &state,
@@ -387,57 +387,15 @@ void goto_symext::locality(
     state.threads[state.source.thread_nr].function_frame[function_identifier];
   frame_nr++;
 
-  std::set<irep_idt> local_identifiers;
-
-  get_local_identifiers(goto_function, local_identifiers);
-
-  statet::framet &frame=state.top();
-
-  for(std::set<irep_idt>::const_iterator
-      it=local_identifiers.begin();
-      it!=local_identifiers.end();
-      it++)
+  for(const auto &param : goto_function.type.parameters())
   {
     // get L0 name
-    ssa_exprt ssa(ns.lookup(*it).symbol_expr());
+    ssa_exprt ssa(ns.lookup(param.get_identifier()).symbol_expr());
     state.rename(ssa, ns, goto_symex_statet::L0);
-    const irep_idt l0_name=ssa.get_identifier();
-
-    // save old L1 name for popping the frame
-    auto c_it = state.level1.current_names.find(l0_name);
-
-    if(c_it != state.level1.current_names.end())
-    {
-      frame.old_level1[l0_name]=c_it->second;
-      c_it->second = std::make_pair(ssa, frame_nr);
-    }
-    else
-    {
-      c_it = state.level1.current_names
-               .emplace(l0_name, std::make_pair(ssa, frame_nr))
-               .first;
-    }
-
-    // do L1 renaming -- these need not be unique, as
-    // identifiers may be shared among functions
-    // (e.g., due to inlining or other code restructuring)
-
-    state.rename(ssa, ns, goto_symex_statet::L1);
-
-    irep_idt l1_name=ssa.get_identifier();
-    unsigned offset=0;
-
-    while(state.l1_history.find(l1_name)!=state.l1_history.end())
-    {
-      symex_renaming_levelt::increase_counter(c_it);
-      ++offset;
-      ssa.set_level_1(frame_nr+offset);
-      l1_name=ssa.get_identifier();
-    }
 
-    // now unique -- store
-    frame.local_objects.insert(l1_name);
-    state.l1_history.insert(l1_name);
+    const std::size_t fresh_l1_index =
+      path_storage.get_unique_index(ssa.get_identifier(), frame_nr);
+    state.add_object(ssa, fresh_l1_index, ns);
   }
 }
 

src/goto-symex/symex_start_thread.cpp

@@ -66,6 +66,9 @@ void goto_symext::symex_start_thread(statet &state)
 
     // get L0 name for current thread
     lhs.set_level_0(t);
+    const irep_idt &l0_name = lhs.get_identifier();
+    std::size_t l1_index = path_storage.get_unique_index(l0_name, 0);
+    CHECK_RETURN(l1_index == 0);
 
     // set up L1 name
     if(!state.level1.current_names.insert(
@@ -75,7 +78,6 @@ void goto_symext::symex_start_thread(statet &state)
     state.rename(lhs, ns, goto_symex_statet::L1);
     const irep_idt l1_name=lhs.get_l1_object_identifier();
     // store it
-    state.l1_history.insert(l1_name);
     new_thread.call_stack.back().local_objects.insert(l1_name);
 
     // make copy