Merge pull request #6392 from diffblue/instruction_guard

Goto instruction guard/condition API

Author: tautschnig

src/analyses/invariant_propagation.cpp

@@ -270,6 +270,6 @@ void invariant_propagationt::simplify(goto_programt &goto_program)
     ::simplify(simplified_guard, ns);
 
     if(invariant_set.implies(simplified_guard).is_true())
-      i_it->set_condition(true_exprt());
+      i_it->condition_nonconst() = true_exprt();
   }
 }

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

@@ -195,7 +195,7 @@ void variable_sensitivity_dependence_domaint::data_dependencies(
   }
   else if(to->is_goto())
   {
-    eval_data_deps(to->guard, ns, domain_data_deps);
+    eval_data_deps(to->condition(), ns, domain_data_deps);
   }
 }
 

src/goto-checker/symex_bmc.cpp

@@ -57,7 +57,7 @@ void symex_bmct::symex_step(
 
   if(
     !state.guard.is_false() && state.source.pc->is_assume() &&
-    simplify_expr(state.source.pc->guard, ns).is_false())
+    simplify_expr(state.source.pc->condition(), ns).is_false())
   {
     log.statistics() << "aborting path on assume(false) at "
                      << state.source.pc->source_location << " thread "
@@ -86,7 +86,7 @@ void symex_bmct::symex_step(
     // sure the goto is considered covered
     if(
       cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
-      cur_pc->guard.is_true())
+      cur_pc->condition().is_true())
       symex_coverage.covered(cur_pc, cur_pc->get_target());
     else if(!state.guard.is_false())
       symex_coverage.covered(cur_pc, state.source.pc);
@@ -109,7 +109,7 @@ void symex_bmct::merge_goto(
     // could the branch possibly be taken?
     !prev_guard.is_false() && !state.guard.is_false() &&
     // branches only, no single-successor goto
-    !prev_pc->guard.is_true())
+    !prev_pc->condition().is_true())
     symex_coverage.covered(prev_pc, state.source.pc);
 }
 

src/goto-instrument/concurrency.cpp

@@ -112,9 +112,7 @@ void concurrency_instrumentationt::instrument(
     }
     else if(it->is_assume() || it->is_assert() || it->is_goto())
     {
-      exprt cond = it->get_condition();
-      instrument(cond);
-      it->set_condition(cond);
+      instrument(it->condition_nonconst());
     }
     else if(it->is_function_call())
     {

src/goto-instrument/cover_instrument_branch.cpp

@@ -25,7 +25,8 @@ void cover_branch_instrumentert::instrument(
 
   const bool is_function_entry_point =
     i_it == goto_program.instructions.begin();
-  const bool is_conditional_goto = i_it->is_goto() && !i_it->guard.is_true();
+  const bool is_conditional_goto =
+    i_it->is_goto() && !i_it->condition().is_true();
   if(!is_function_entry_point && !is_conditional_goto)
     return;
 
@@ -52,7 +53,7 @@ void cover_branch_instrumentert::instrument(
     std::string true_comment = "block " + b + " branch true";
     std::string false_comment = "block " + b + " branch false";
 
-    exprt guard = i_it->guard;
+    exprt guard = i_it->condition();
     source_locationt source_location = i_it->source_location;
 
     goto_program.insert_before_swap(i_it);

src/goto-programs/goto_convert.cpp

@@ -269,7 +269,7 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
     if(it->get_target()->target_number == it_z->target_number)
     {
       it->set_target(it_goto_y->get_target());
-      it->set_condition(boolean_negate(it->get_condition()));
+      it->condition_nonconst() = boolean_negate(it->condition());
       it_goto_y->turn_into_skip();
     }
   }
@@ -876,7 +876,7 @@ void goto_convertt::convert_loop_contracts(
     }
 
     PRECONDITION(loop->is_goto());
-    loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
+    loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
   }
 
   if(!decreases_clause.is_nil())
@@ -889,7 +889,7 @@ void goto_convertt::convert_loop_contracts(
     }
 
     PRECONDITION(loop->is_goto());
-    loop->guard.add(ID_C_spec_decreases).swap(decreases_clause);
+    loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
   }
 }
 

src/goto-programs/goto_inline_class.cpp

@@ -282,9 +282,8 @@ void goto_inlinet::insert_function_body(
 
       if(instruction.has_condition())
       {
-        exprt c = instruction.get_condition();
-        replace_location(c, target->source_location);
-        instruction.set_condition(c);
+        replace_location(
+          instruction.condition_nonconst(), target->source_location);
       }
     }
   }

src/goto-programs/goto_program.h

@@ -328,7 +328,8 @@ class goto_programt
     goto_program_instruction_typet type;
 
     /// Guard for gotos, assume, assert
-    /// Use get_condition() to read, and set_condition(c) to write.
+    /// Use condition() method to access.
+    /// This member will eventually be protected.
     exprt guard;
 
     /// Does this instruction have a condition?
@@ -338,19 +339,35 @@ class goto_programt
     }
 
     /// Get the condition of gotos, assume, assert
+    DEPRECATED(SINCE(2021, 10, 12, "Use condition() instead"))
     const exprt &get_condition() const
     {
       PRECONDITION(has_condition());
       return guard;
     }
 
     /// Set the condition of gotos, assume, assert
+    DEPRECATED(SINCE(2021, 10, 12, "Use condition_nonconst() instead"))
     void set_condition(exprt c)
     {
       PRECONDITION(has_condition());
       guard = std::move(c);
     }
 
+    /// Get the condition of gotos, assume, assert
+    const exprt &condition() const
+    {
+      PRECONDITION(has_condition());
+      return guard;
+    }
+
+    /// Get the condition of gotos, assume, assert
+    exprt &condition_nonconst()
+    {
+      PRECONDITION(has_condition());
+      return guard;
+    }
+
     // The below will eventually become a single target only.
     /// The target for gotos and for start_thread nodes
     typedef std::list<instructiont>::iterator targett;

src/goto-programs/remove_virtual_functions.cpp

@@ -421,8 +421,8 @@ static goto_programt::targett replace_virtual_function_with_dispatch_table(
           !new_code_gotos.empty(),
           "a dispatch table entry has been processed already, "
           "which should have created a GOTO");
-        new_code_gotos.instructions.back().guard =
-          or_exprt(new_code_gotos.instructions.back().guard, class_id_test);
+        new_code_gotos.instructions.back().condition_nonconst() = or_exprt(
+          new_code_gotos.instructions.back().condition(), class_id_test);
       }
       else
       {

src/goto-programs/show_goto_functions_json.cpp

@@ -95,11 +95,11 @@ json_objectt show_goto_functions_jsont::convert(
           instruction_entry["operands"] = std::move(operand_array);
         }
 
-        if(!instruction.guard.is_true())
+        if(instruction.has_condition())
         {
-          json_objectt guard_object=
+          json_objectt guard_object =
             no_comments_irep_converter.convert_from_irep(
-              instruction.guard);
+              instruction.condition());
 
           instruction_entry["guard"] = std::move(guard_object);
         }

src/goto-programs/write_goto_binary.cpp

@@ -98,7 +98,11 @@ bool write_goto_binary(
         irepconverter.reference_convert(instruction.get_code(), out);
         irepconverter.reference_convert(instruction.source_location, out);
         write_gb_word(out, (long)instruction.type);
-        irepconverter.reference_convert(instruction.guard, out);
+
+        const auto condition =
+          instruction.has_condition() ? instruction.condition() : true_exprt();
+        irepconverter.reference_convert(condition, out);
+
         write_gb_word(out, instruction.target_number);
 
         write_gb_word(out, instruction.targets.size());