Merge pull request #3265 from diffblue/code_dead_operand

code_deadt operand is now typed

Author: Daniel Kroening

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -135,19 +135,19 @@ class remove_exceptionst
     goto_programt &goto_program,
     const goto_programt::targett &instr_it,
     const stack_catcht &stack_catch,
-    const std::vector<exprt> &locals);
+    const std::vector<symbol_exprt> &locals);
 
   bool instrument_throw(
     goto_programt &goto_program,
     const goto_programt::targett &,
     const stack_catcht &,
-    const std::vector<exprt> &);
+    const std::vector<symbol_exprt> &);
 
   bool instrument_function_call(
     goto_programt &goto_program,
     const goto_programt::targett &,
     const stack_catcht &,
-    const std::vector<exprt> &);
+    const std::vector<symbol_exprt> &);
 
   void instrument_exceptions(
     goto_programt &goto_program);
@@ -308,7 +308,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(
   goto_programt &goto_program,
   const goto_programt::targett &instr_it,
   const remove_exceptionst::stack_catcht &stack_catch,
-  const std::vector<exprt> &locals)
+  const std::vector<symbol_exprt> &locals)
 {
   // Jump to the universal handler or function end, as appropriate.
   // This will appear after the GOTO-based dynamic dispatch below
@@ -388,7 +388,7 @@ bool remove_exceptionst::instrument_throw(
   goto_programt &goto_program,
   const goto_programt::targett &instr_it,
   const remove_exceptionst::stack_catcht &stack_catch,
-  const std::vector<exprt> &locals)
+  const std::vector<symbol_exprt> &locals)
 {
   PRECONDITION(instr_it->type==THROW);
 
@@ -419,7 +419,7 @@ bool remove_exceptionst::instrument_function_call(
   goto_programt &goto_program,
   const goto_programt::targett &instr_it,
   const stack_catcht &stack_catch,
-  const std::vector<exprt> &locals)
+  const std::vector<symbol_exprt> &locals)
 {
   PRECONDITION(instr_it->type==FUNCTION_CALL);
 
@@ -473,8 +473,8 @@ void remove_exceptionst::instrument_exceptions(
   goto_programt &goto_program)
 {
   stack_catcht stack_catch; // stack of try-catch blocks
-  std::vector<std::vector<exprt>> stack_locals; // stack of local vars
-  std::vector<exprt> locals;
+  std::vector<std::vector<symbol_exprt>> stack_locals; // stack of local vars
+  std::vector<symbol_exprt> locals;
 
   if(goto_program.empty())
     return;

src/analyses/constant_propagator.cpp

@@ -134,7 +134,7 @@ void constant_propagator_domaint::transform(
   else if(from->is_dead())
   {
     const code_deadt &code_dead=to_code_dead(from->code);
-    values.set_to_top(to_symbol_expr(code_dead.symbol()));
+    values.set_to_top(code_dead.symbol());
   }
   else if(from->is_function_call())
   {

src/analyses/reaching_definitions.cpp

@@ -130,8 +130,7 @@ void rd_range_domaint::transform_dead(
   const namespacet &,
   locationt from)
 {
-  const irep_idt &identifier=
-    to_symbol_expr(to_code_dead(from->code).symbol()).get_identifier();
+  const irep_idt &identifier = to_code_dead(from->code).get_identifier();
 
   valuest::iterator entry=values.find(identifier);
 

src/goto-diff/change_impact.cpp

@@ -85,8 +85,8 @@ void full_slicert::operator()(
     }
     else if(e_it->first->is_dead())
     {
-      const exprt &s=to_code_dead(e_it->first->code).symbol();
-      decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
+      const auto &s=to_code_dead(e_it->first->code).symbol();
+      decl_dead[s.get_identifier()].push(e_it->second);
     }
   }
 

src/goto-instrument/full_slicer.cpp

@@ -315,8 +315,8 @@ void full_slicert::operator()(
     }
     else if(e_it->first->is_dead())
     {
-      const exprt &s=to_code_dead(e_it->first->code).symbol();
-      decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
+      const auto &s = to_code_dead(e_it->first->code).symbol();
+      decl_dead[s.get_identifier()].push(e_it->second);
     }
   }
 

src/goto-symex/symex_dead.cpp

@@ -26,7 +26,7 @@ void goto_symext::symex_dead(statet &state)
   // We increase the L2 renaming to make these non-deterministic.
   // We also prevent propagation of old values.
 
-  ssa_exprt ssa(to_symbol_expr(code.symbol()));
+  ssa_exprt ssa(code.symbol());
   state.rename(ssa, ns, goto_symex_statet::L1);
 
   // in case of pointers, put something into the value set

src/util/std_code.cpp

@@ -13,11 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "std_expr.h"
 
-const irep_idt &code_deadt::get_identifier() const
-{
-  return to_symbol_expr(symbol()).get_identifier();
-}
-
 /// If this `codet` is a \ref code_blockt (i.e.\ it represents a block of
 /// statements), return the unmodified input. Otherwise (i.e.\ the `codet`
 /// represents a single statement), convert it to a \ref code_blockt with the

src/util/std_code.h

@@ -335,28 +335,25 @@ inline code_declt &to_code_decl(codet &code)
 class code_deadt:public codet
 {
 public:
-  DEPRECATED("use code_deadt(symbol) instead")
-  code_deadt():codet(ID_dead)
+  explicit code_deadt(const symbol_exprt &symbol) : codet(ID_dead)
   {
-    operands().resize(1);
+    add_to_operands(symbol);
   }
 
-  explicit code_deadt(const exprt &symbol):codet(ID_dead)
+  symbol_exprt &symbol()
   {
-    copy_to_operands(symbol);
+    return static_cast<symbol_exprt &>(op0());
   }
 
-  exprt &symbol()
+  const symbol_exprt &symbol() const
   {
-    return op0();
+    return static_cast<const symbol_exprt &>(op0());
   }
 
-  const exprt &symbol() const
+  const irep_idt &get_identifier() const
   {
-    return op0();
+    return symbol().get_identifier();
   }
-
-  const irep_idt &get_identifier() const;
 };
 
 template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
@@ -374,6 +371,9 @@ inline const code_deadt &to_code_dead(const codet &code)
   PRECONDITION(code.get_statement() == ID_dead);
   DATA_INVARIANT(
     code.operands().size() == 1, "dead statement must have one operand");
+  DATA_INVARIANT(
+    to_unary_expr(code).op().id() == ID_symbol,
+    "dead statement must take symbol operand");
   return static_cast<const code_deadt &>(code);
 }
 
@@ -382,6 +382,9 @@ inline code_deadt &to_code_dead(codet &code)
   PRECONDITION(code.get_statement() == ID_dead);
   DATA_INVARIANT(
     code.operands().size() == 1, "dead statement must have one operand");
+  DATA_INVARIANT(
+    to_unary_expr(code).op().id() == ID_symbol,
+    "dead statement must take symbol operand");
   return static_cast<code_deadt &>(code);
 }