Merge pull request #73 from tautschnig/no-dead-instructions

Do not generate necessarily dead instructions

Author: Daniel Kroening

src/goto-analyzer/unreachable_instructions.cpp

@@ -47,12 +47,6 @@ static void unreachable_instructions(
       it!=dominators.cfg.entry_map.end();
       ++it)
   {
-    if(it->first->is_dead() ||
-       (it->first->is_assign() &&
-        to_code_assign(it->first->code).lhs().get(ID_identifier)==
-        "__CPROVER_dead_object"))
-      continue;
-
     const cfg_dominatorst::cfgt::nodet &n=dominators.cfg[it->second];
     if(n.dominators.empty())
       dest.insert(std::make_pair(it->first->location_number,
@@ -78,11 +72,7 @@ static void all_unreachable(
   dead_mapt &dest)
 {
   forall_goto_program_instructions(it, goto_program)
-    if(!it->is_end_function() &&
-       !it->is_dead() &&
-       !(it->is_assign() &&
-         to_code_assign(it->code).lhs().get(ID_identifier)==
-         "__CPROVER_dead_object"))
+    if(!it->is_end_function())
       dest.insert(std::make_pair(it->location_number, it));
 }
 

src/goto-programs/goto_convert.cpp

@@ -419,8 +419,6 @@ void goto_convertt::convert(
   const codet &code,
   goto_programt &dest)
 {
-  std::size_t old_tmp_symbols_size=tmp_symbols.size();
-
   const irep_idt &statement=code.get_statement();
 
   if(statement==ID_block)
@@ -542,19 +540,6 @@ void goto_convertt::convert(
   else
     copy(code, OTHER, dest);
 
-  // We only need to kill the temporaries if control
-  // can get to the end of the block.
-  #if 0
-  if(!dest.empty() &&
-     dest.instructions.back().is_goto() &&
-     dest.instructions.back().guard.is_true())
-    tmp_symbols.resize(old_tmp_symbols_size);
-  else
-    kill_tmp_symbols(old_tmp_symbols_size, dest);
-  #else
-  kill_tmp_symbols(old_tmp_symbols_size, dest);
-  #endif
-
   // make sure dest is never empty
   if(dest.instructions.empty())
   {
@@ -566,31 +551,6 @@ void goto_convertt::convert(
 
 /*******************************************************************\
 
-Function: goto_convertt::kill_tmp_symbols
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void goto_convertt::kill_tmp_symbols(
-  std::size_t final_size,
-  goto_programt &dest)
-{
-  while(tmp_symbols.size()>final_size)
-  {
-    symbol_exprt symbol=tmp_symbols.back();
-    tmp_symbols.pop_back();
-    dest.add_instruction(DEAD);
-    dest.instructions.back().code=code_deadt(symbol);
-  }
-}
-
-/*******************************************************************\
-
 Function: goto_convertt::convert_block
 
   Inputs:
@@ -617,7 +577,8 @@ void goto_convertt::convert_block(
     convert(b_code, dest);
   }
 
-  // see if we need to do any destructors
+  // see if we need to do any destructors -- may have been processed
+  // in a prior break/continue/return already, don't create dead code
   if(!dest.empty() &&
      dest.instructions.back().is_goto() &&
      dest.instructions.back().guard.is_true())
@@ -2564,11 +2525,10 @@ symbolt &goto_convertt::new_tmp_symbol(
     new_symbol.location=source_location;
   } while(symbol_table.move(new_symbol, symbol_ptr));    
 
-  tmp_symbols.push_back(symbol_ptr->symbol_expr());
-  
-  goto_programt::targett t=dest.add_instruction(DECL);
-  t->code=code_declt(symbol_ptr->symbol_expr());
-  t->source_location=source_location;
+  code_declt decl;
+  decl.symbol()=symbol_ptr->symbol_expr();
+  decl.add_source_location()=source_location;
+  convert_decl(decl, dest);
 
   return *symbol_ptr;  
 }

src/goto-programs/goto_convert_class.h

@@ -63,9 +63,6 @@ class goto_convertt:public message_streamt
   symbol_exprt make_compound_literal(
     const exprt &expr,
     goto_programt &dest);
-  
-  typedef std::list<symbol_exprt> tmp_symbolst;
-  tmp_symbolst tmp_symbols;
 
   //
   // translation of C expressions (with side effects)
@@ -87,8 +84,6 @@ class goto_convertt:public message_streamt
     exprt &expr,
     const std::string &suffix,
     goto_programt &);
-    
-  void kill_tmp_symbols(std::size_t, goto_programt &);
 
   void rewrite_boolean(exprt &dest);
 

src/goto-programs/goto_convert_side_effect.cpp

@@ -417,8 +417,6 @@ void goto_convertt::remove_function_call(
 
   new_name(new_symbol);
 
-  tmp_symbols.push_back(new_symbol.symbol_expr());
-  
   {
     code_declt decl;
     decl.symbol()=new_symbol.symbol_expr();
@@ -488,7 +486,11 @@ void goto_convertt::remove_cpp_new(
   new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
 
   new_name(new_symbol);
-  tmp_symbols.push_back(new_symbol.symbol_expr());
+
+  code_declt decl;
+  decl.symbol()=new_symbol.symbol_expr();
+  decl.add_source_location()=new_symbol.location;
+  convert_decl(decl, dest);
 
   call=code_assignt(new_symbol.symbol_expr(), expr);
 
@@ -560,7 +562,6 @@ void goto_convertt::remove_malloc(
     new_symbol.location=expr.source_location();
 
     new_name(new_symbol);
-    tmp_symbols.push_back(new_symbol.symbol_expr());
 
     code_declt decl;
     decl.symbol()=new_symbol.symbol_expr();
@@ -703,15 +704,9 @@ void goto_convertt::remove_statement_expression(
            id2string(last.get(ID_statement))+"'";
 
   {
-    // this likely needs to be a proper stack
-    tmp_symbolst old_tmp_symbols;
-    old_tmp_symbols.swap(tmp_symbols);
-    
     goto_programt tmp;  
     convert(code, tmp);
     dest.destructive_append(tmp);
-  
-    old_tmp_symbols.swap(tmp_symbols);
   }
 
   static_cast<exprt &>(expr)=tmp_symbol_expr;