new L1 locality

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@892 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/goto-symex/goto_symex_state.cpp

@@ -286,13 +286,9 @@ void goto_symex_statet::assignment(
   #endif
 
   // do the l2 renaming 
-  unsigned &count=level2.current_names[l1_identifier];
-
-  count++;
-    
-  level2.rename(l1_identifier, count);
-  
-  lhs.set_identifier(level2.name(l1_identifier, count));
+  unsigned new_count=level2.current_count(l1_identifier)+1;
+  level2.rename(l1_identifier, new_count);
+  lhs.set_identifier(level2.name(l1_identifier, new_count));
 
   // for value propagation -- the RHS is L2
 

src/goto-symex/goto_symex_state.h

@@ -37,10 +37,10 @@ class goto_symex_statet
   // we have a two-level renaming
 
   typedef std::map<irep_idt, irep_idt> original_identifierst;
-  typedef std::set<irep_idt> declaration_historyt;
 
-  // we remember all declarations
-  declaration_historyt declaration_history; 
+  // we remember all L1 renamings
+  typedef std::set<irep_idt> l1_historyt;
+  l1_historyt l1_history; 
 
   struct renaming_levelt
   {
@@ -58,7 +58,7 @@ class goto_symex_statet
     void get_original_name(typet &type) const;
     void print(std::ostream &out) const;
     unsigned current_count(const irep_idt &identifier) const;
-
+    
     irep_idt operator()(const irep_idt &identifier)
     {
       // see if it's already renamed
@@ -172,7 +172,7 @@ class goto_symex_statet
       // _always_ rename
       return name(identifier, current_count(identifier));
     }
-
+    
     level2t() { }
     virtual ~level2t() { }
   } level2;

src/goto-symex/symex_decl.cpp

@@ -43,30 +43,21 @@ void goto_symext::symex_decl(statet &state)
   if(code.op0().id()!=ID_symbol)
     throw "decl expects symbol as first operand";
 
-  // just do the L1 renaming to preserve locality
+  // We increase the L2 renaming to make these non-deterministic.
+  // We also prevent propagation of old values.
+  
   const irep_idt &identifier=
     to_symbol_expr(code.op0()).get_identifier();
 
-  const irep_idt l0_identifier=
-    state.rename(identifier, ns, goto_symex_statet::L0);
+  const irep_idt l1_identifier=
+    state.rename(identifier, ns, goto_symex_statet::L1);
 
-  irep_idt l1_identifier;
-
-  do
-  {
-    unsigned index=state.top().level1.current_names[l0_identifier];
-    state.top().level1.rename(l0_identifier, index+1);
-    l1_identifier=state.top().level1(l0_identifier);
-  }
-  while(state.declaration_history.find(l1_identifier)!=
-        state.declaration_history.end());
-
-  // forget the old L2 renaming to avoid SSA for it
-  state.level2.remove(l1_identifier);
+  // prevent propagation
   state.propagation.remove(l1_identifier);
-  state.declaration_history.insert(l1_identifier); 
-  
-  state.top().local_variables.insert(l1_identifier);
+
+  // L2 renaming
+  unsigned new_count=state.level2.current_count(l1_identifier)+1;
+  state.level2.rename(l1_identifier, new_count);
 
   // in case of pointers, put something into the value set
   if(ns.follow(code.op0().type()).id()==ID_pointer)

src/goto-symex/symex_function.cpp

@@ -388,12 +388,24 @@ void goto_symext::locality(
     // get L0 name
     irep_idt l0_name=state.rename(*it, ns, goto_symex_statet::L0);
 
-    // do L1 renaming
-    frame.level1.rename(l0_name, frame_nr);
-
-    // store
-    irep_idt l1_name=frame.level1(l0_name);
+    // do L1 renaming -- these need not be unique, as
+    // identifiers may be shared among functions
+    // (e.g., due to inlining or other code restructuring)
+    
+    irep_idt l1_name;
+    unsigned offset=0;
+    
+    do
+    {
+      frame.level1.rename(l0_name, frame_nr+offset);
+      l1_name=frame.level1(l0_name);
+      offset++;
+    }
+    while(state.l1_history.find(l1_name)!=state.l1_history.end());
+    
+    // now unique -- store
     frame.local_variables.insert(l1_name);
+    state.l1_history.insert(l1_name);
   }
 }