protect instructiont::code

This PR is a step towards removing direct access to instructiont::code, with
the long-term goal of removing the use of codet expressions in goto programs.

Author: kroening

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -93,7 +93,7 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
   // We only expect to find nondets in the rhs of an assignments, and in return
   // statements if remove_returns has not been run, but we do a more general
   // check on all operands in case this changes
-  for(exprt &op : target->code.operands())
+  for(exprt &op : target->code_nonconst().operands())
   {
     if(!is_nondet_pointer(op))
     {

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -200,8 +200,7 @@ bool remove_exceptionst::function_or_callees_may_throw(
 
     if(instruction.is_function_call())
     {
-      const exprt &function_expr =
-        to_code_function_call(instruction.code).function();
+      const exprt &function_expr = instruction.get_function_call().function();
       DATA_INVARIANT(
         function_expr.id()==ID_symbol,
         "identifier expected to be a symbol");
@@ -235,8 +234,8 @@ void remove_exceptionst::instrument_exception_handler(
   if(may_catch)
   {
     // retrieve the exception variable
-    const exprt &thrown_exception_local=
-      to_code_landingpad(instr_it->code).catch_expr();
+    const exprt &thrown_exception_local =
+      to_code_landingpad(instr_it->get_code()).catch_expr();
 
     const symbol_exprt thrown_global_symbol=
       get_inflight_exception_global();
@@ -408,8 +407,8 @@ bool remove_exceptionst::instrument_throw(
 {
   PRECONDITION(instr_it->type==THROW);
 
-  const exprt &exc_expr=
-    uncaught_exceptions_domaint::get_exception_symbol(instr_it->code);
+  const exprt &exc_expr =
+    uncaught_exceptions_domaint::get_exception_symbol(instr_it->get_code());
 
   add_exception_dispatch_sequence(
     function_identifier, goto_program, instr_it, stack_catch, locals);
@@ -424,7 +423,7 @@ bool remove_exceptionst::instrument_throw(
     typecast_exprt(exc_expr, exc_thrown.type()));
   // now turn the `throw' into `assignment'
   instr_it->type=ASSIGN;
-  instr_it->code=assignment;
+  instr_it->code_nonconst() = assignment;
 
   return true;
 }
@@ -518,7 +517,7 @@ void remove_exceptionst::instrument_exceptions(
     // Is it a handler push/pop or catch landing-pad?
     else if(instr_it->type==CATCH)
     {
-      const irep_idt &statement=instr_it->code.get_statement();
+      const irep_idt &statement = instr_it->get_code().get_statement();
       // Is it an exception landing pad (start of a catch block)?
       if(statement==ID_exception_landingpad)
       {
@@ -558,8 +557,8 @@ void remove_exceptionst::instrument_exceptions(
           stack_catch.back();
 
         // copy targets
-        const code_push_catcht::exception_listt &exception_list=
-          to_code_push_catch(instr_it->code).exception_list();
+        const code_push_catcht::exception_listt &exception_list =
+          to_code_push_catch(instr_it->get_code()).exception_list();
 
         // The target list can be empty if `finish_catch_push_targets` found that
         // the targets were unreachable (in which case no exception can truly

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -244,8 +244,9 @@ bool remove_instanceoft::lower_instanceof(
   goto_programt &goto_program,
   goto_programt::targett target)
 {
-  if(target->is_target() &&
-     (contains_instanceof(target->code) || contains_instanceof(target->guard)))
+  if(
+    target->is_target() && (contains_instanceof(target->get_code()) ||
+                            contains_instanceof(target->guard)))
   {
     // If this is a branch target, add a skip beforehand so we can splice new
     // GOTO programs before the target instruction without inserting into the
@@ -257,7 +258,7 @@ bool remove_instanceoft::lower_instanceof(
   }
 
   return lower_instanceof(
-           function_identifier, target->code, goto_program, target) |
+           function_identifier, target->code_nonconst(), goto_program, target) |
          lower_instanceof(
            function_identifier, target->guard, goto_program, target);
 }

jbmc/src/java_bytecode/replace_java_nondet.cpp

@@ -88,11 +88,11 @@ is_nondet_returning_object(const code_function_callt &function_call)
 static nondet_instruction_infot
 get_nondet_instruction_info(const goto_programt::const_targett &instr)
 {
-  if(!(instr->is_function_call() && instr->code.id() == ID_code))
+  if(!(instr->is_function_call() && instr->get_code().id() == ID_code))
   {
     return nondet_instruction_infot();
   }
-  const auto &code = instr->code;
+  const auto &code = instr->get_code();
   INVARIANT(
     code.get_statement() == ID_function_call,
     "function_call should have ID_function_call");
@@ -209,14 +209,13 @@ static goto_programt::targett check_and_replace_target(
   // If we haven't removed returns yet, our function call will have a variable
   // on its left hand side.
   const bool remove_returns_not_run =
-    to_code_function_call(target->code).lhs().is_not_nil();
+    target->get_function_call().lhs().is_not_nil();
 
   irep_idt return_identifier;
   if(remove_returns_not_run)
   {
     return_identifier =
-      to_symbol_expr(to_code_function_call(target->code).lhs())
-        .get_identifier();
+      to_symbol_expr(target->get_function_call().lhs()).get_identifier();
   }
   else
   {
@@ -282,8 +281,8 @@ static goto_programt::targett check_and_replace_target(
     inserted_expr.set_nullable(
       instr_info.get_nullable_type() ==
       nondet_instruction_infot::is_nullablet::TRUE);
-    target_instruction->code = code_returnt(inserted_expr);
-    target_instruction->code.add_source_location() =
+    target_instruction->code_nonconst() = code_returnt(inserted_expr);
+    target_instruction->code_nonconst().add_source_location() =
       target_instruction->source_location;
   }
   else if(target_instruction->is_assign())
@@ -296,8 +295,9 @@ static goto_programt::targett check_and_replace_target(
     inserted_expr.set_nullable(
       instr_info.get_nullable_type() ==
       nondet_instruction_infot::is_nullablet::TRUE);
-    target_instruction->code = code_assignt(nondet_var, inserted_expr);
-    target_instruction->code.add_source_location() =
+    target_instruction->code_nonconst() =
+      code_assignt(nondet_var, inserted_expr);
+    target_instruction->code_nonconst().add_source_location() =
       target_instruction->source_location;
   }
 

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

@@ -63,7 +63,7 @@ static bool is_call_to(
 {
   if(!inst->is_function_call())
     return false;
-  const exprt &callee_expr = to_code_function_call(inst->code).function();
+  const exprt &callee_expr = inst->get_function_call().function();
   if(callee_expr.id() != ID_symbol)
     return false;
   return to_symbol_expr(callee_expr).get_identifier() == callee;

jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

@@ -22,7 +22,7 @@ static bool is_expected_virtualmethod_call(
 {
   if(instruction.type != FUNCTION_CALL)
     return false;
-  const auto &virtual_call = to_code_function_call(instruction.code);
+  const auto &virtual_call = instruction.get_function_call();
   const auto &called_function = virtual_call.function();
   if(!can_cast_expr<class_method_descriptor_exprt>(called_function))
     return false;
@@ -81,9 +81,10 @@ SCENARIO(
               instrend = main_function.body.instructions.end();
             instrit != instrend; ++instrit)
         {
-          for(auto it = instrit->code.depth_begin(),
-                itend = instrit->code.depth_end();
-              it != itend; ++it)
+          for(auto it = instrit->get_code().depth_begin(),
+                   itend = instrit->get_code().depth_end();
+              it != itend;
+              ++it)
           {
             if(it->id() == ID_dereference)
             {

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -41,7 +41,7 @@ void validate_nondet_method_removed(
     // Check that our NONDET(<type>) exists on a rhs somewhere.
     if(inst.is_assign())
     {
-      const code_assignt &assignment = to_code_assign(inst.code);
+      const code_assignt &assignment = inst.get_assign();
       if(assignment.rhs().id() == ID_side_effect)
       {
         const side_effect_exprt &see = to_side_effect_expr(assignment.rhs());
@@ -68,8 +68,7 @@ void validate_nondet_method_removed(
     // And check to see that our nondet method call has been removed.
     if(inst.is_function_call())
     {
-      const code_function_callt &function_call =
-        to_code_function_call(inst.code);
+      const code_function_callt &function_call = inst.get_function_call();
 
       // Small check to make sure the instruction is a symbol.
       if(function_call.function().id() != ID_symbol)
@@ -101,9 +100,8 @@ void validate_nondets_converted(
     // Check that our NONDET(<type>) exists on a rhs somewhere.
     exprt target_expression =
       (inst.is_assign()
-         ? to_code_assign(inst.code).rhs()
-         : inst.is_return() ? to_code_return(inst.code).return_value()
-                            : inst.code);
+         ? inst.get_assign().rhs()
+         : inst.is_return() ? inst.return_value() : inst.get_code());
 
     if(
       const auto side_effect =

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

@@ -32,7 +32,7 @@ void check_function_call(
   for(const auto &target : targets)
   {
     REQUIRE(target->type == goto_program_instruction_typet::FUNCTION_CALL);
-    const code_function_callt &call = to_code_function_call(target->code);
+    const code_function_callt &call = target->get_function_call();
     REQUIRE(call.function().id() == ID_symbol);
     REQUIRE(to_symbol_expr(call.function()).get_identifier() == function_name);
   }

src/analyses/cfg_dominators.h

@@ -246,7 +246,7 @@ inline void dominators_pretty_print_node(
   const goto_programt::targett& target,
   std::ostream& out)
 {
-  out << target->code.pretty();
+  out << target->get_code().pretty();
 }
 
 /// Print the result of the dominator computation

src/analyses/constant_propagator.cpp

@@ -758,7 +758,7 @@ void constant_propagator_ait::replace(
     if(d.is_bottom())
       continue;
 
-    replace_types_rec(d.values.replace_const, it->code);
+    replace_types_rec(d.values.replace_const, it->code_nonconst());
 
     if(it->is_goto() || it->is_assume() || it->is_assert())
     {

src/analyses/goto_check.cpp

@@ -302,8 +302,7 @@ void goto_checkt::collect_allocations(
       if(!instruction.is_function_call())
         continue;
 
-      const code_function_callt &call=
-        to_code_function_call(instruction.code);
+      const code_function_callt &call = instruction.get_function_call();
       if(call.function().id()!=ID_symbol ||
          to_symbol_expr(call.function()).get_identifier()!=
          CPROVER_PREFIX "allocated_memory")
@@ -1973,7 +1972,7 @@ void goto_checkt::goto_check(
     }
     else if(i.is_assign())
     {
-      const code_assignt &code_assign=to_code_assign(i.code);
+      const code_assignt &code_assign = i.get_assign();
 
       // Reset the no_enum_check with the flag reset for exception
       // safety
@@ -1991,16 +1990,19 @@ void goto_checkt::goto_check(
            return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
          }))
       {
-        exprt &rhs = to_code_assign(i.code).rhs();
+        const exprt &rhs = i.get_assign().rhs();
         auto rw_ok_cond = rw_ok_check(rhs);
         if(rw_ok_cond.has_value())
-          rhs = *rw_ok_cond;
+        {
+          auto new_assign = i.get_assign(); // copy
+          new_assign.rhs() = *rw_ok_cond;
+          i.set_assign(new_assign);
+        }
       }
     }
     else if(i.is_function_call())
     {
-      const code_function_callt &code_function_call=
-        to_code_function_call(i.code);
+      const code_function_callt &code_function_call = i.get_function_call();
 
       // for Java, need to check whether 'this' is null
       // on non-static method invocations
@@ -2055,13 +2057,14 @@ void goto_checkt::goto_check(
     }
     else if(i.is_throw())
     {
-      if(i.code.get_statement()==ID_expression &&
-         i.code.operands().size()==1 &&
-         i.code.op0().operands().size()==1)
+      if(
+        i.get_code().get_statement() == ID_expression &&
+        i.get_code().operands().size() == 1 &&
+        i.get_code().op0().operands().size() == 1)
       {
         // must not throw NULL
 
-        exprt pointer = to_unary_expr(i.code.op0()).op();
+        exprt pointer = to_unary_expr(i.get_code().op0()).op();
 
         const notequal_exprt not_eq_null(
           pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
@@ -2102,8 +2105,7 @@ void goto_checkt::goto_check(
     {
       if(enable_pointer_check || enable_pointer_primitive_check)
       {
-        assert(i.code.operands().size()==1);
-        const symbol_exprt &variable=to_symbol_expr(i.code.op0());
+        const symbol_exprt &variable = i.dead_symbol();
 
         // is it dirty?
         if(local_bitvector_analysis->dirty(variable))
@@ -2119,7 +2121,7 @@ void goto_checkt::goto_check(
           goto_programt::targett t =
             new_code.add(goto_programt::make_assignment(
               std::move(lhs), std::move(rhs), i.source_location));
-          t->code.add_source_location()=i.source_location;
+          t->code_nonconst().add_source_location() = i.source_location;
         }
       }
     }

src/analyses/invariant_set_domain.cpp

@@ -56,22 +56,22 @@ void invariant_set_domaint::transform(
 
   case ASSIGN:
     {
-      const code_assignt &assignment=to_code_assign(from_l->code);
+      const code_assignt &assignment = from_l->get_assign();
       invariant_set.assignment(assignment.lhs(), assignment.rhs());
     }
     break;
 
   case OTHER:
     if(from_l->get_other().is_not_nil())
-      invariant_set.apply_code(from_l->code);
+      invariant_set.apply_code(from_l->get_code());
     break;
 
   case DECL:
-    invariant_set.apply_code(from_l->code);
+    invariant_set.apply_code(from_l->get_code());
     break;
 
   case FUNCTION_CALL:
-    invariant_set.apply_code(from_l->code);
+    invariant_set.apply_code(from_l->get_code());
     break;
 
   case START_THREAD:

src/analyses/local_bitvector_analysis.cpp

@@ -275,7 +275,7 @@ void local_bitvector_analysist::build()
     {
     case ASSIGN:
     {
-      const code_assignt &code_assign = to_code_assign(instruction.code);
+      const code_assignt &code_assign = instruction.get_assign();
       assign_lhs(
         code_assign.lhs(), code_assign.rhs(), loc_info_src, loc_info_dest);
       break;
@@ -300,7 +300,7 @@ void local_bitvector_analysist::build()
     case FUNCTION_CALL:
     {
       const code_function_callt &code_function_call =
-        to_code_function_call(instruction.code);
+        instruction.get_function_call();
       if(code_function_call.lhs().is_not_nil())
         assign_lhs(
           code_function_call.lhs(), nil_exprt(), loc_info_src, loc_info_dest);

src/analyses/uncaught_exceptions_analysis.cpp

@@ -66,7 +66,7 @@ void uncaught_exceptions_domaint::transform(
   {
   case THROW:
   {
-    const exprt &exc_symbol=get_exception_symbol(instruction.code);
+    const exprt &exc_symbol = get_exception_symbol(instruction.get_code());
     // retrieve the static type of the thrown exception
     const irep_idt &type_id=get_exception_type(exc_symbol.type());
     join(type_id);
@@ -79,15 +79,15 @@ void uncaught_exceptions_domaint::transform(
   }
   case CATCH:
   {
-    if(!instruction.code.has_operands())
+    if(!instruction.get_code().has_operands())
     {
       if(!instruction.targets.empty()) // push
       {
         std::set<irep_idt> caught;
         stack_caught.push_back(caught);
         std::set<irep_idt> &last_caught=stack_caught.back();
-        const irept::subt &exception_list=
-          instruction.code.find(ID_exception_list).get_sub();
+        const irept::subt &exception_list =
+          instruction.get_code().find(ID_exception_list).get_sub();
 
         for(const auto &exc : exception_list)
         {
@@ -114,8 +114,7 @@ void uncaught_exceptions_domaint::transform(
   }
   case FUNCTION_CALL:
   {
-    const exprt &function_expr=
-      to_code_function_call(instruction.code).function();
+    const exprt &function_expr = instruction.get_function_call().function();
     DATA_INVARIANT(
       function_expr.id()==ID_symbol,
       "identifier expected to be a symbol");