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

@@ -796,3 +796,29 @@ 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)
+{
+  framet &frame = top();
+
+  const irep_idt l0_name = ssa.get_identifier();
+
+  // save old L1 name, if any
+  auto existing_or_new_entry = level1.current_names.emplace(
+    std::piecewise_construct,
+    std::forward_as_tuple(l0_name),
+    std::forward_as_tuple(ssa, l1_index));
+
+  if(!existing_or_new_entry.second)
+  {
+    frame.old_level1.emplace(l0_name, existing_or_new_entry.first->second);
+    existing_or_new_entry.first->second = std::make_pair(ssa, l1_index);
+  }
+
+  ssa = rename_ssa<L1>(std::move(ssa), ns);
+  const bool inserted = frame.local_objects.insert(ssa.get_identifier()).second;
+  INVARIANT(inserted, "l1_name expected to be unique by construction");
+}

src/goto-symex/goto_symex_state.h

@@ -144,9 +144,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;
 
@@ -257,6 +254,10 @@ 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);
+
   void print_backtrace(std::ostream &) const;
 
   // threads

src/goto-symex/path_storage.h

@@ -98,11 +98,24 @@ class path_storaget
   /// error-handling paths.
   std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
 
+  /// 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,10 +34,16 @@ 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.
-
-  ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{expr}, ns);
+  // each declaration introduces a new object, which we record as a fresh L1
+  // index
+
+  ssa_exprt ssa = state.rename_ssa<L0>(ssa_exprt{expr}, ns);
+  // We use "1" as the first level-1 index, which is in line with doing so for
+  // level-2 indices (but it's an arbitrary choice, we have just always been
+  // doing it this way).
+  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
@@ -57,16 +63,11 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
     state.value_set.assign(ssa, l1_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;
   exprt expr_l2 = state.rename(std::move(ssa), ns);

src/goto-symex/symex_function_call.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 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);
 
@@ -305,7 +306,7 @@ void goto_symext::symex_function_call_code(
   framet &frame = state.new_frame();
 
   // preserve locality of local variables
-  locality(identifier, state, goto_function, ns);
+  locality(identifier, state, path_storage, goto_function, ns);
 
   // assign actuals to formal parameters
   parameter_assignments(identifier, goto_function, state, arguments);
@@ -381,68 +382,27 @@ 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)
 {
   unsigned &frame_nr=
     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 =
-      state.rename_ssa<L0>(ssa_exprt{ns.lookup(*it).symbol_expr()}, ns);
-    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)
-
-    ssa_exprt ssa_l1 = state.rename_ssa<L1>(std::move(ssa), ns);
-
-    irep_idt l1_name = ssa_l1.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_l1.set_level_1(frame_nr + offset);
-      l1_name = ssa_l1.get_identifier();
-    }
+    ssa_exprt ssa = state.rename_ssa<L0>(
+      ssa_exprt{ns.lookup(param.get_identifier()).symbol_expr()}, ns);
 
-    // 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);
   }
 }