Merge pull request #3980 from tautschnig/block-scope

L1 renaming at each declaration

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

@@ -766,3 +766,29 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
         << frame.calling_location.pc->location_number << "\n";
   }
 }
+
+void goto_symex_statet::add_object(
+  ssa_exprt &ssa,
+  std::size_t l1_index,
+  const namespacet &ns)
+{
+  framet &frame = call_stack().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

@@ -60,9 +60,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;
 
@@ -141,6 +138,11 @@ class goto_symex_statet final : public goto_statet
     return threads[source.thread_nr].call_stack;
   }
 
+  /// Create a new instance of the L0-renamed object \p ssa. As part of this,
+  /// turn \p ssa into an L1-renamed SSA expression. When doing so, use
+  /// \p l1_index as the L1 index, which must not previously have 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,25 @@ 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;
+
+  /// Storage used by \ref get_unique_index.
+  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 = instruction.get_dead();
 
-  // 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{code.symbol()}, ns);
 
   // in case of pointers, put something into the value set
@@ -43,10 +38,13 @@ void goto_symext::symex_dead(statet &state)
 
   const irep_idt &l1_identifier = ssa.get_identifier();
 
-  // prevent propagation
+  // we cannot remove the object from the L1 renaming map, because L1 renaming
+  // information is not local to a path, but removing it from the propagation
+  // map is safe as 1) it is local to a path and 2) this instance can no longer
+  // appear
   state.propagation.erase(l1_identifier);
-
-  // L2 renaming
+  // 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(l1_identifier);
   if(level2_it != state.level2.current_names.end())
     symex_renaming_levelt::increase_counter(level2_it);

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);