Merge pull request #5861 from diffblue/goto_instruction_decl

introduce instructiont::decl_symbol()

Author: tautschnig

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -512,8 +512,7 @@ void remove_exceptionst::instrument_exceptions(
   {
     if(instr_it->is_decl())
     {
-      code_declt decl = instr_it->get_decl();
-      locals.push_back(decl.symbol());
+      locals.push_back(instr_it->decl_symbol());
     }
     // Is it a handler push/pop or catch landing-pad?
     else if(instr_it->type==CATCH)

src/analyses/constant_propagator.cpp

@@ -158,8 +158,7 @@ void constant_propagator_domaint::transform(
 
   if(from->is_decl())
   {
-    const auto &code_decl = from->get_decl();
-    const symbol_exprt &symbol = code_decl.symbol();
+    const symbol_exprt &symbol = from->decl_symbol();
     values.set_to_top(symbol);
   }
   else if(from->is_assign())

src/analyses/custom_bitvector_analysis.cpp

@@ -294,12 +294,12 @@ void custom_bitvector_domaint::transform(
 
   case DECL:
     {
-      const code_declt &code_decl=to_code_decl(instruction.code);
-      assign_lhs(code_decl.symbol(), vectorst());
+      const auto &decl_symbol = instruction.decl_symbol();
+      assign_lhs(decl_symbol, vectorst());
 
       // is it a pointer?
-      if(code_decl.symbol().type().id()==ID_pointer)
-        assign_lhs(dereference_exprt(code_decl.symbol()), vectorst());
+      if(decl_symbol.type().id() == ID_pointer)
+        assign_lhs(dereference_exprt(decl_symbol), vectorst());
     }
     break;
 

src/analyses/escape_analysis.cpp

@@ -202,11 +202,8 @@ void escape_domaint::transform(
     break;
 
   case DECL:
-    {
-      const code_declt &code_decl=to_code_decl(instruction.code);
-      aliases.isolate(code_decl.get_identifier());
-      assign_lhs_cleanup(code_decl.symbol(), std::set<irep_idt>());
-    }
+    aliases.isolate(instruction.decl_symbol().get_identifier());
+    assign_lhs_cleanup(instruction.decl_symbol(), std::set<irep_idt>());
     break;
 
   case DEAD:

src/analyses/global_may_alias.cpp

@@ -120,11 +120,8 @@ void global_may_alias_domaint::transform(
   }
 
   case DECL:
-  {
-    const code_declt &code_decl = to_code_decl(instruction.code);
-    aliases.isolate(code_decl.get_identifier());
+    aliases.isolate(instruction.decl_symbol().get_identifier());
     break;
-  }
 
   case DEAD:
     aliases.isolate(instruction.dead_symbol().get_identifier());

src/analyses/goto_rw.cpp

@@ -811,13 +811,9 @@ void goto_rw(
     break;
 
   case DECL:
+    rw_set.get_objects_rec(function, target, target->decl_symbol().type());
     rw_set.get_objects_rec(
-      function, target, to_code_decl(target->code).symbol().type());
-    rw_set.get_objects_rec(
-      function,
-      target,
-      rw_range_sett::get_modet::LHS_W,
-      to_code_decl(target->code).symbol());
+      function, target, rw_range_sett::get_modet::LHS_W, target->decl_symbol());
     break;
 
   case FUNCTION_CALL:

src/analyses/interval_domain.cpp

@@ -71,7 +71,7 @@ void interval_domaint::transform(
   switch(instruction.type)
   {
   case DECL:
-    havoc_rec(to_code_decl(instruction.code).symbol());
+    havoc_rec(instruction.decl_symbol());
     break;
 
   case DEAD:

src/analyses/local_bitvector_analysis.cpp

@@ -282,15 +282,12 @@ void local_bitvector_analysist::build()
     }
 
     case DECL:
-    {
-      const code_declt &code_decl = to_code_decl(instruction.code);
       assign_lhs(
-        code_decl.symbol(),
+        instruction.decl_symbol(),
         exprt(ID_uninitialized),
         loc_info_src,
         loc_info_dest);
       break;
-    }
 
     case DEAD:
       assign_lhs(

src/analyses/local_may_alias.cpp

@@ -383,11 +383,9 @@ void local_may_aliast::build(const goto_functiont &goto_function)
     }
 
     case DECL:
-    {
-      const code_declt &code_decl = to_code_decl(instruction.code);
-      assign_lhs(code_decl.symbol(), nil_exprt(), loc_info_src, loc_info_dest);
+      assign_lhs(
+        instruction.decl_symbol(), nil_exprt(), loc_info_src, loc_info_dest);
       break;
-    }
 
     case DEAD:
       assign_lhs(

src/analyses/locals.cpp

@@ -20,7 +20,7 @@ void localst::build(const goto_functiont &goto_function)
   for(const auto &instruction : goto_function.body.instructions)
   {
     if(instruction.is_decl())
-      locals.insert(instruction.get_decl().get_identifier());
+      locals.insert(instruction.decl_symbol().get_identifier());
   }
 
   locals.insert(

src/analyses/uninitialized_domain.cpp

@@ -33,7 +33,7 @@ void uninitialized_domaint::transform(
 
   if(from->is_decl())
   {
-    const irep_idt &identifier = to_code_decl(from->code).get_identifier();
+    const irep_idt &identifier = from->decl_symbol().get_identifier();
     const symbolt &symbol = ns.lookup(identifier);
 
     if(!symbol.is_static_lifetime)

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -46,10 +46,9 @@ void variable_sensitivity_domaint::transform(
     abstract_object_pointert top_object =
       abstract_state
         .abstract_object_factory(
-          to_code_decl(instruction.code).symbol().type(), ns, true, false)
+          instruction.decl_symbol().type(), ns, true, false)
         ->update_location_context(write_location, true);
-    abstract_state.assign(
-      to_code_decl(instruction.code).symbol(), top_object, ns);
+    abstract_state.assign(instruction.decl_symbol(), top_object, ns);
   }
   // We now store top.
   break;

src/goto-diff/change_impact.cpp

@@ -79,7 +79,7 @@ void full_slicert::operator()(
       jumps.push_back(instruction_node_index);
     else if(instruction->is_decl())
     {
-      const auto &s=to_code_decl(instruction->code).symbol();
+      const auto &s=instruction->decl_symbol();
       decl_dead[s.get_identifier()].push(instruction_node_index);
     }
     else if(instruction->is_dead())

src/goto-instrument/code_contracts.cpp

@@ -669,7 +669,7 @@ bool code_contractst::add_pointer_checks(const std::string &function_name)
   {
     if(instruction_iterator->is_decl())
     {
-      freely_assignable_exprs.insert(instruction_iterator->get_decl().symbol());
+      freely_assignable_exprs.insert(instruction_iterator->decl_symbol());
     }
     else if(instruction_iterator->is_assign())
     {

src/goto-instrument/full_slicer.cpp

@@ -285,7 +285,7 @@ void full_slicert::operator()(
       jumps.push_back(instruction_node_index);
     else if(instruction->is_decl())
     {
-      const auto &s = to_code_decl(instruction->code).symbol();
+      const auto &s = instruction->decl_symbol();
       decl_dead[s.get_identifier()].push(instruction_node_index);
     }
     else if(instruction->is_dead())

src/goto-instrument/goto_program2code.cpp

@@ -448,7 +448,7 @@ goto_programt::const_targett goto_program2codet::convert_decl(
   goto_programt::const_targett upper_bound,
   code_blockt &dest)
 {
-  code_declt d = target->get_decl();
+  code_declt d = code_declt{target->decl_symbol()};
   symbol_exprt &symbol = d.symbol();
 
   goto_programt::const_targett next=target;

src/goto-instrument/uninitialized.cpp

@@ -109,8 +109,7 @@ void uninitializedt::add_assertions(
       // if we track it, add declaration and assignment
       // for tracking variable!
 
-      const irep_idt &identifier=
-        to_code_decl(instruction.code).get_identifier();
+      const irep_idt &identifier = instruction.decl_symbol().get_identifier();
 
       if(tracking.find(identifier)!=tracking.end())
       {

src/goto-programs/goto_program.cpp

@@ -240,8 +240,7 @@ void goto_programt::get_decl_identifiers(
       DATA_INVARIANT(
         instruction.code.operands().size() == 1,
         "declaration statement expects one operand");
-      const symbol_exprt &symbol_expr = to_symbol_expr(instruction.code.op0());
-      decl_identifiers.insert(symbol_expr.get_identifier());
+      decl_identifiers.insert(instruction.decl_symbol().get_identifier());
     }
   }
 }
@@ -870,9 +869,9 @@ void goto_programt::instructiont::validate(
       source_location);
     DATA_CHECK_WITH_DIAGNOSTICS(
       vm,
-      !ns.lookup(get_decl().get_identifier(), table_symbol),
+      !ns.lookup(decl_symbol().get_identifier(), table_symbol),
       "declared symbols should be known",
-      id2string(get_decl().get_identifier()),
+      id2string(decl_symbol().get_identifier()),
       source_location);
     break;
   case DEAD:
@@ -949,13 +948,9 @@ void goto_programt::instructiont::transform(
 
   case DECL:
   {
-    auto new_symbol = f(get_decl().symbol());
+    auto new_symbol = f(decl_symbol());
     if(new_symbol.has_value())
-    {
-      auto new_decl = get_decl();
-      new_decl.symbol() = to_symbol_expr(*new_symbol);
-      set_decl(new_decl);
-    }
+      decl_symbol() = to_symbol_expr(*new_symbol);
   }
   break;
 
@@ -1037,7 +1032,7 @@ void goto_programt::instructiont::apply(
     break;
 
   case DECL:
-    f(get_decl().symbol());
+    f(decl_symbol());
     break;
 
   case DEAD:

src/goto-programs/goto_program.h

@@ -197,6 +197,7 @@ class goto_programt
     }
 
     /// Get the declaration for DECL
+    DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead"))
     const code_declt &get_decl() const
     {
       PRECONDITION(is_decl());
@@ -207,7 +208,30 @@ class goto_programt
       return decl;
     }
 
+    /// Get the declared symbol for DECL
+    const symbol_exprt &decl_symbol() const
+    {
+      PRECONDITION(is_decl());
+      auto &decl = expr_checked_cast<code_declt>(code);
+      INVARIANT(
+        !decl.initial_value(),
+        "code_declt in goto program may not contain initialization.");
+      return decl.symbol();
+    }
+
+    /// Get the declared symbol for DECL
+    symbol_exprt &decl_symbol()
+    {
+      PRECONDITION(is_decl());
+      auto &decl = expr_checked_cast<code_declt>(code);
+      INVARIANT(
+        !decl.initial_value(),
+        "code_declt in goto program may not contain initialization.");
+      return decl.symbol();
+    }
+
     /// Set the declaration for DECL
+    DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead"))
     void set_decl(code_declt c)
     {
       PRECONDITION(is_decl());

src/goto-programs/string_abstraction.cpp

@@ -251,7 +251,7 @@ void string_abstractiont::declare_define_locals(goto_programt &dest)
       // same name may exist several times due to inlining, make sure the first
       // declaration is used
       available_decls.insert(
-        std::make_pair(it->get_decl().get_identifier(), it));
+        std::make_pair(it->decl_symbol().get_identifier(), it));
 
   // declare (and, if necessary, define) locals
   for(const auto &l : locals)

src/goto-symex/symex_decl.cpp

@@ -16,14 +16,7 @@ Author: Daniel Kroening, [email protected]
 void goto_symext::symex_decl(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
-
-  const auto &code = instruction.get_decl();
-
-  // two-operand decl not supported here
-  // we handle the decl with only one operand
-  PRECONDITION(code.operands().size() == 1);
-
-  symex_decl(state, code.symbol());
+  symex_decl(state, instruction.decl_symbol());
 }
 
 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)