introduce instructiont::decl_symbol()

This addresses the issue of the ambiguous dual-use of code_declt in both the
C front-end and the goto-program API by replacing the use of code_declt by
directly returning the symbol_exprt.  The client code is simplified.

Author: kroening

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/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/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/goto_program2code.cpp

@@ -450,7 +450,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-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());
     }
   }
 }
@@ -871,9 +870,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:
@@ -954,13 +953,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;
 
@@ -1046,7 +1041,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

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <sstream>
 #include <string>
 
+#include <util/deprecate.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/source_location.h>
@@ -196,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());
@@ -206,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)