L1 renaming at each declaration

This was done up until c8f0f7b. The
(observable) problem tackled here is that objects declared in loops got the same
L1 name, which implies they had the same address. Thus objects were spuriously
reported as dead when their address was taken, because a pointer to the latest
(live) object would be the same as one to an earlier (genuinely dead) object.

A side effect of this change is objects generated for test suites now have L1
indices, as witnessed in the pointer-function-parameters test.

Author: tautschnig

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

@@ -4,8 +4,8 @@ main.c
 ^\*\* 5 of 5 covered \(100\.0%\)$
 ^Test suite:$
 ^(tmp(\$\d+)?=[^,]*, a=\(\(signed int \*\)NULL\))|(a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*)$
-^(a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4)|(tmp(\$\d+)?=4, a=&tmp(\$\d+)?!0)$
-^(a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+))|(tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+), a=&tmp(\$\d+)?!0)$
+^(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)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

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

regression/cbmc/vla3/test.desc

@@ -7,5 +7,4 @@ main.c
 --
 ^warning: ignoring
 --
-Renaming is inconsistent across loop iterations as we map L1 names to types, but
-do not actually introduce new L1 ids each time we declare an object.
+The array decision procedure does not yet handle member expressions.

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

@@ -842,3 +842,35 @@ void goto_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,
+  const field_sensitivityt &field_sensitivity)
+{
+  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.emplace(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, field_sensitivity, 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

@@ -148,9 +148,6 @@ class goto_symex_statet final : public goto_statet
 
   symex_target_equationt *symex_target;
 
-  // we remember all L1 renamings
-  std::set<irep_idt> l1_history;
-
   symex_level0t level0;
   symex_level1t level1;
 
@@ -269,6 +266,14 @@ class goto_symex_statet final : public goto_statet
 
   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,
+    const field_sensitivityt &field_sensitivity);
+
   void print_backtrace(std::ostream &) const;
 
   // threads

src/goto-symex/path_storage.h

@@ -90,11 +90,24 @@ class path_storaget
   /// Counter for nondet objects, which require unique names
   symex_nondet_generatort build_symex_nondet;
 
+  /// 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_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, field_sensitivity, goto_symex_statet::L1);
+  state.rename(ssa, ns, field_sensitivity, 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, field_sensitivity);
   const irep_idt &l1_identifier=ssa.get_identifier();
 
   // rename type to L2
@@ -62,16 +65,11 @@ 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);
+  bool is_new =
+    state.level2.current_names.emplace(l1_identifier, std::make_pair(ssa, 1))
+      .second;
+  CHECK_RETURN(is_new);
   const bool record_events=state.record_events;
   state.record_events=false;
   state.rename(ssa, ns, field_sensitivity);

src/goto-symex/symex_function_call.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 static void locality(
   const irep_idt &function_identifier,
   goto_symext::statet &state,
+  path_storaget &path_storage,
   const goto_functionst::goto_functiont &goto_function,
   const namespacet &ns,
   const field_sensitivityt &field_sensitivity);
@@ -306,7 +307,8 @@ void goto_symext::symex_function_call_code(
   framet &frame = state.new_frame();
 
   // preserve locality of local variables
-  locality(identifier, state, goto_function, ns, field_sensitivity);
+  locality(
+    identifier, state, path_storage, goto_function, ns, field_sensitivity);
 
   // assign actuals to formal parameters
   parameter_assignments(identifier, goto_function, state, arguments);
@@ -381,11 +383,12 @@ 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
 static void locality(
   const irep_idt &function_identifier,
   goto_symext::statet &state,
+  path_storaget &path_storage,
   const goto_functionst::goto_functiont &goto_function,
   const namespacet &ns,
   const field_sensitivityt &field_sensitivity)
@@ -394,57 +397,15 @@ static void 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);
-
-  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, field_sensitivity, 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.emplace(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, field_sensitivity, 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, field_sensitivity);
   }
 }
 

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);
 
     // setup L1 name
     // with field sensitivity this insert may happen multiple times
@@ -75,7 +78,6 @@ void goto_symext::symex_start_thread(statet &state)
     state.rename(lhs, ns, field_sensitivity, 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