Merge pull request #6421 from tautschnig/cleanup-nonconst

Rewrite use of *_nonconst()

Author: tautschnig

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -358,17 +358,16 @@ void remove_exceptionst::add_exception_dispatch_sequence(
         stack_catch[i][j].second;
       if(!stack_catch[i][j].first.empty())
       {
-        // Normal exception handler, make an instanceof check.
-        goto_programt::targett t_exc = goto_program.insert_after(
-          instr_it,
-          goto_programt::make_goto(
-            new_state_pc, true_exprt(), instr_it->source_location()));
-
         // use instanceof to check that this is the correct handler
         struct_tag_typet type(stack_catch[i][j].first);
 
         java_instanceof_exprt check(exc_thrown, type);
-        t_exc->condition_nonconst() = check;
+
+        // Normal exception handler, make an instanceof check.
+        goto_programt::targett t_exc = goto_program.insert_after(
+          instr_it,
+          goto_programt::make_goto(
+            new_state_pc, check, instr_it->source_location()));
 
         if(remove_added_instanceof)
         {

jbmc/src/java_bytecode/replace_java_nondet.cpp

@@ -294,10 +294,7 @@ 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_nonconst() =
-      code_assignt(nondet_var, inserted_expr);
-    target_instruction->code_nonconst().add_source_location() =
-      target_instruction->source_location();
+    target_instruction->assign_rhs_nonconst() = inserted_expr;
   }
 
   goto_program.update();

src/analyses/interval_analysis.cpp

@@ -77,9 +77,9 @@ void instrument_intervals(
     {
       goto_programt::targett t=i_it;
       goto_function.body.insert_before_swap(i_it);
-      *t = goto_programt::make_assumption(conjunction(assertion));
       i_it++; // goes to original instruction
-      t->source_location_nonconst() = i_it->source_location();
+      *t = goto_programt::make_assumption(
+        conjunction(assertion), i_it->source_location());
     }
   }
 }

src/ansi-c/goto_check_c.cpp

@@ -1724,20 +1724,25 @@ void goto_check_ct::add_guarded_property(
 
   if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second)
   {
-    auto t = new_code.add(
-      enable_assert_to_assume ? goto_programt::make_assumption(
-                                  std::move(guarded_expr), source_location)
-                              : goto_programt::make_assertion(
-                                  std::move(guarded_expr), source_location));
-
     std::string source_expr_string;
     get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
 
-    t->source_location_nonconst().set_comment(
-      comment + " in " + source_expr_string);
-    t->source_location_nonconst().set_property_class(property_class);
+    source_locationt annotated_location = source_location;
+    annotated_location.set_comment(comment + " in " + source_expr_string);
+    annotated_location.set_property_class(property_class);
+
+    add_all_disable_named_check_pragmas(annotated_location);
 
-    add_all_disable_named_check_pragmas(t->source_location_nonconst());
+    if(enable_assert_to_assume)
+    {
+      new_code.add(goto_programt::make_assumption(
+        std::move(guarded_expr), annotated_location));
+    }
+    else
+    {
+      new_code.add(goto_programt::make_assertion(
+        std::move(guarded_expr), annotated_location));
+    }
   }
 }
 
@@ -2120,15 +2125,21 @@ void goto_check_ct::goto_check(
     {
       if(std::find(i.labels.begin(), i.labels.end(), label) != i.labels.end())
       {
-        auto t = new_code.add(
-          enable_assert_to_assume
-            ? goto_programt::make_assumption(false_exprt{}, i.source_location())
-            : goto_programt::make_assertion(
-                false_exprt{}, i.source_location()));
-
-        t->source_location_nonconst().set_property_class("error label");
-        t->source_location_nonconst().set_comment("error label " + label);
-        t->source_location_nonconst().set("user-provided", true);
+        source_locationt annotated_location = i.source_location();
+        annotated_location.set_property_class("error label");
+        annotated_location.set_comment("error label " + label);
+        annotated_location.set("user-provided", true);
+
+        if(enable_assert_to_assume)
+        {
+          new_code.add(
+            goto_programt::make_assumption(false_exprt{}, annotated_location));
+        }
+        else
+        {
+          new_code.add(
+            goto_programt::make_assertion(false_exprt{}, annotated_location));
+        }
       }
     }
 
@@ -2210,10 +2221,9 @@ void goto_check_ct::goto_check(
             side_effect_expr_nondett(bool_typet(), i.source_location()),
             std::move(address_of_expr),
             lhs);
-          goto_programt::targett t =
-            new_code.add(goto_programt::make_assignment(
-              std::move(lhs), std::move(rhs), i.source_location()));
-          t->code_nonconst().add_source_location() = i.source_location();
+          new_code.add(goto_programt::make_assignment(
+            code_assignt{std::move(lhs), std::move(rhs), i.source_location()},
+            i.source_location()));
         }
       }
     }

src/goto-analyzer/taint_analysis.cpp

@@ -179,12 +179,13 @@ void taint_analysist::instrument(
                 where,
                 ID_get_may,
                 address_of_exprt(string_constantt(rule.taint))};
-              goto_programt::targett t =
-                insert_before.add(goto_programt::make_assertion(
-                  not_exprt(get_may), instruction.source_location()));
-              t->source_location_nonconst().set_property_class(
+              source_locationt annotated_location =
+                instruction.source_location();
+              annotated_location.set_property_class(
                 "taint rule " + id2string(rule.id));
-              t->source_location_nonconst().set_comment(rule.message);
+              annotated_location.set_comment(rule.message);
+              insert_before.add(goto_programt::make_assertion(
+                not_exprt(get_may), annotated_location));
               break;
             }
 

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -164,8 +164,8 @@ void memory_snapshot_harness_generatort::add_init_section(
 
   auto ins_it1 = goto_program.insert_before(
     start_it,
-    goto_programt::make_goto(goto_program.const_cast_target(start_it)));
-  ins_it1->condition_nonconst() = func_init_done_var;
+    goto_programt::make_goto(
+      goto_program.const_cast_target(start_it), func_init_done_var));
 
   auto ins_it2 = goto_program.insert_after(
     ins_it1,

src/goto-instrument/accelerate/overflow_instrumenter.cpp

@@ -52,15 +52,13 @@ void overflow_instrumentert::add_overflow_checks(
 
   if(t->is_assign())
   {
-    code_assignt &assignment = to_code_assign(t->code_nonconst());
-
-    if(assignment.lhs()==overflow_var)
+    if(t->assign_lhs() == overflow_var)
     {
       return;
     }
 
-    add_overflow_checks(t, assignment.lhs(), added);
-    add_overflow_checks(t, assignment.rhs(), added);
+    add_overflow_checks(t, t->assign_lhs_nonconst(), added);
+    add_overflow_checks(t, t->assign_rhs_nonconst(), added);
   }
 
   if(t->has_condition())

src/goto-instrument/accelerate/scratch_program.cpp

@@ -145,12 +145,10 @@ void scratch_programt::fix_types()
   {
     if(it->is_assign())
     {
-      code_assignt &code = to_code_assign(it->code_nonconst());
-
-      if(code.lhs().type()!=code.rhs().type())
+      if(it->assign_lhs().type() != it->assign_rhs().type())
       {
-        typecast_exprt typecast(code.rhs(), code.lhs().type());
-        code.rhs()=typecast;
+        typecast_exprt typecast{it->assign_rhs(), it->assign_lhs().type()};
+        it->assign_rhs_nonconst() = typecast;
       }
     }
     else if(it->is_assume() || it->is_assert())

src/goto-instrument/contracts/contracts.cpp

@@ -278,10 +278,9 @@ void code_contractst::check_apply_loop_contracts(
   {
     code_assertt assertion{initial_invariant_val};
     assertion.add_source_location() = loop_head_location;
+    assertion.add_source_location().set_comment(
+      "Check loop invariant before entry");
     converter.goto_convert(assertion, pre_loop_head_instrs, mode);
-    pre_loop_head_instrs.instructions.back()
-      .source_location_nonconst()
-      .set_comment("Check loop invariant before entry");
   }
 
   // Insert the first block of pre_loop_head_instrs,
@@ -396,10 +395,9 @@ void code_contractst::check_apply_loop_contracts(
   {
     code_assertt assertion{invariant};
     assertion.add_source_location() = loop_head_location;
+    assertion.add_source_location().set_comment(
+      "Check that loop invariant is preserved");
     converter.goto_convert(assertion, pre_loop_end_instrs, mode);
-    pre_loop_end_instrs.instructions.back()
-      .source_location_nonconst()
-      .set_comment("Check that loop invariant is preserved");
   }
 
   // Generate: assignments to store the multidimensional decreases clause's
@@ -421,11 +419,10 @@ void code_contractst::check_apply_loop_contracts(
       generate_lexicographic_less_than_check(
         new_decreases_vars, old_decreases_vars)};
     monotonic_decreasing_assertion.add_source_location() = loop_head_location;
+    monotonic_decreasing_assertion.add_source_location().set_comment(
+      "Check decreases clause on loop iteration");
     converter.goto_convert(
       monotonic_decreasing_assertion, pre_loop_end_instrs, mode);
-    pre_loop_end_instrs.instructions.back()
-      .source_location_nonconst()
-      .set_comment("Check decreases clause on loop iteration");
 
     // Discard the temporary variables that store decreases clause's value
     for(size_t i = 0; i < old_decreases_vars.size(); i++)
@@ -464,12 +461,12 @@ void code_contractst::check_apply_loop_contracts(
 
     goto_programt pre_loop_exit_instrs;
     // Assertion to check that step case was checked if we entered the loop.
+    source_locationt annotated_location = loop_head_location;
+    annotated_location.set_comment(
+      "Check that loop instrumentation was not truncated");
     pre_loop_exit_instrs.add(goto_programt::make_assertion(
       or_exprt{not_exprt{entered_loop}, not_exprt{in_base_case}},
-      loop_head_location));
-    pre_loop_exit_instrs.instructions.back()
-      .source_location_nonconst()
-      .set_comment("Check that loop instrumentation was not truncated");
+      annotated_location));
     // Instructions to make all the temporaries go dead.
     pre_loop_exit_instrs.add(
       goto_programt::make_dead(in_base_case, loop_head_location));
@@ -873,9 +870,8 @@ void code_contractst::apply_function_contract(
         goto_programt::make_decl(to_symbol_expr(call_ret), loc));
 
     side_effect_expr_nondett expr(type, location);
-    auto target = havoc_instructions.add(
-      goto_programt::make_assignment(call_ret, expr, loc));
-    target->code_nonconst().add_source_location() = loc;
+    havoc_instructions.add(goto_programt::make_assignment(
+      code_assignt{call_ret, std::move(expr), loc}, loc));
   }
 
   // Insert havoc instructions immediately before the call site.

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

@@ -83,9 +83,9 @@ void havoc_assigns_clause_targetst::havoc_if_valid(
   {
     // OTHER __CPROVER_havoc_object(target_snapshot_var)
     codet code(ID_havoc_object, {car.lower_bound_var()});
-    const auto &inst =
-      dest.add(goto_programt::make_other(code, source_location));
-    inst->source_location_nonconst().set_comment(tracking_comment);
+    source_locationt annotated_location = source_location;
+    annotated_location.set_comment(tracking_comment);
+    dest.add(goto_programt::make_other(code, annotated_location));
   }
   else if(car.havoc_method == car_havoc_methodt::HAVOC_SLICE)
   {
@@ -106,12 +106,13 @@ void havoc_assigns_clause_targetst::havoc_if_valid(
     // ASSIGN *(target.type() *)__car_lb = nondet(car.target().type())
     const auto &target_type = car.target().type();
     side_effect_expr_nondett nondet(target_type, source_location);
-    const auto &inst = dest.add(goto_programt::make_assignment(
+    source_locationt annotated_location = source_location;
+    annotated_location.set_comment(tracking_comment);
+    dest.add(goto_programt::make_assignment(
       dereference_exprt{typecast_exprt::conditional_cast(
         car.lower_bound_var(), pointer_type(target_type))},
       nondet,
-      source_location));
-    inst->source_location_nonconst().set_comment(tracking_comment);
+      annotated_location));
   }
   else
   {
@@ -154,10 +155,11 @@ void havoc_assigns_clause_targetst::havoc_static_local(
 
   const auto &target_type = car.target().type();
   side_effect_expr_nondett nondet(target_type, source_location);
-  const auto &inst = dest.add(
-    goto_programt::make_assignment(car.target(), nondet, source_location));
-  inst->source_location_nonconst().set_comment(tracking_comment);
-  add_propagate_static_local_pragma(inst->source_location_nonconst());
+  source_locationt annotated_location = source_location;
+  annotated_location.set_comment(tracking_comment);
+  add_propagate_static_local_pragma(annotated_location);
+  dest.add(
+    goto_programt::make_assignment(car.target(), nondet, annotated_location));
 
   dest.destructive_append(skip_program);