protect goto_instructiont::guard

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -368,7 +368,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(
         struct_tag_typet type(stack_catch[i][j].first);
 
         java_instanceof_exprt check(exc_thrown, type);
-        t_exc->guard=check;
+        t_exc->condition_nonconst() = check;
 
         if(remove_added_instanceof)
         {

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -243,7 +243,8 @@ bool remove_instanceoft::lower_instanceof(
 {
   if(
     target->is_target() &&
-    (contains_instanceof(target->code()) || contains_instanceof(target->guard)))
+    (contains_instanceof(target->code()) ||
+     (target->has_condition() && contains_instanceof(target->condition()))))
   {
     // 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
@@ -256,8 +257,12 @@ bool remove_instanceoft::lower_instanceof(
 
   return lower_instanceof(
            function_identifier, target->code_nonconst(), goto_program, target) |
-         lower_instanceof(
-           function_identifier, target->guard, goto_program, target);
+         (target->has_condition() ? lower_instanceof(
+                                      function_identifier,
+                                      target->condition_nonconst(),
+                                      goto_program,
+                                      target)
+                                  : false);
 }
 
 /// Replace every instanceof in the passed function body with an explicit

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

@@ -71,7 +71,7 @@ static bool is_call_to(
 
 static bool is_assume_false(goto_programt::const_targett inst)
 {
-  return inst->is_assume() && inst->guard.is_false();
+  return inst->is_assume() && inst->condition().is_false();
 }
 
 /// Interpret `program`, resolving classid comparisons assuming any actual
@@ -90,7 +90,7 @@ static goto_programt::const_targett interpret_classid_comparison(
   {
     if(pc->type() == GOTO)
     {
-      exprt guard = pc->guard;
+      exprt guard = pc->condition();
       guard = resolve_classid_test(guard, actual_class_id, ns);
       if(guard.is_true())
       {

jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

@@ -92,15 +92,20 @@ SCENARIO(
             }
           }
 
-          for(auto it = instrit->guard.depth_begin(),
-                itend = instrit->guard.depth_end();
-              it != itend; ++it)
+          if(instrit->has_condition())
           {
-            if(it->id() == ID_dereference)
+            const auto &condition = instrit->condition();
+
+            for(auto it = condition.depth_begin(),
+                     itend = condition.depth_end();
+                it != itend;
+                ++it)
             {
-              const auto &deref = to_dereference_expr(*it);
-              REQUIRE(
-                safe_pointers.is_safe_dereference(deref, instrit));
+              if(it->id() == ID_dereference)
+              {
+                const auto &deref = to_dereference_expr(*it);
+                REQUIRE(safe_pointers.is_safe_dereference(deref, instrit));
+              }
             }
           }
         }

jbmc/unit/java_bytecode/java_virtual_functions/virtual_functions.cpp

@@ -71,11 +71,12 @@ SCENARIO(
             // branching for class C and one for class D or O.
             if(instruction.type() == goto_program_instruction_typet::GOTO)
             {
-              if(instruction.guard.id() == ID_equal)
+              if(instruction.condition().id() == ID_equal)
               {
                 THEN("Class C should call its specific method")
                 {
-                  const equal_exprt &eq_expr = to_equal_expr(instruction.guard);
+                  const equal_exprt &eq_expr =
+                    to_equal_expr(instruction.condition());
                   check_function_call(
                     eq_expr,
                     "java::C",
@@ -84,11 +85,12 @@ SCENARIO(
                 }
               }
 
-              else if(instruction.guard.id() == ID_or)
+              else if(instruction.condition().id() == ID_or)
               {
                 THEN("Classes D and O should both call O.toString()")
                 {
-                  const or_exprt &disjunction = to_or_expr(instruction.guard);
+                  const or_exprt &disjunction =
+                    to_or_expr(instruction.condition());
                   REQUIRE(
                     (disjunction.op0().id() == ID_equal &&
                      disjunction.op1().id() == ID_equal));

src/analyses/interval_analysis.cpp

@@ -50,7 +50,7 @@ void instrument_intervals(
       {
         // we follow a branch, instrument
       }
-      else if(previous->is_function_call() && !previous->guard.is_true())
+      else if(previous->is_function_call())
       {
         // we follow a function call, instrument
       }

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -79,13 +79,13 @@ void variable_sensitivity_domaint::transform(
         if(to == from->get_target())
         {
           // The AI is exploring the branch where the jump is taken
-          assume(instruction.guard, ns);
+          assume(instruction.condition(), ns);
         }
         else
         {
           // Exploring the path where the jump is not taken - therefore assume
           // the condition is false
-          assume(not_exprt(instruction.guard), ns);
+          assume(not_exprt(instruction.condition()), ns);
         }
       }
       // ignore jumps to the next line, we can assume nothing
@@ -94,7 +94,7 @@ void variable_sensitivity_domaint::transform(
   break;
 
   case ASSUME:
-    assume(instruction.guard, ns);
+    assume(instruction.condition(), ns);
     break;
 
   case FUNCTION_CALL:

src/goto-cc/linker_script_merge.cpp

@@ -258,8 +258,11 @@ int linker_script_merget::pointerize_linker_defined_symbols(
     goto_programt &program=gf.second.body;
     for(auto &instruction : program.instructions)
     {
-      for(exprt *insts : std::list<exprt *>(
-            {&(instruction.code_nonconst()), &(instruction.guard)}))
+      std::list<exprt *> expressions = {&instruction.code_nonconst()};
+      if(instruction.has_condition())
+        expressions.push_back(&instruction.condition_nonconst());
+
+      for(exprt *insts : expressions)
       {
         std::list<symbol_exprt> to_pointerize;
         symbols_to_pointerize(linker_values, *insts, to_pointerize);

src/goto-checker/symex_coverage.cpp

@@ -214,7 +214,7 @@ void goto_program_coverage_recordt::compute_coverage_lines(
       it->is_end_function())
       continue;
 
-    const bool is_branch = it->is_goto() && !it->guard.is_constant();
+    const bool is_branch = it->is_goto() && !it->condition().is_constant();
 
     unsigned l =
       safe_string2unsigned(id2string(it->source_location().get_line()));

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -165,7 +165,7 @@ 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->guard = func_init_done_var;
+  ins_it1->condition_nonconst() = func_init_done_var;
 
   auto ins_it2 = goto_program.insert_after(
     ins_it1,

src/goto-instrument/cover_basic_blocks.cpp

@@ -21,7 +21,9 @@ optionalt<std::size_t> cover_basic_blockst::continuation_of_block(
     return {};
 
   const goto_programt::targett in_t = *instruction->incoming_edges.cbegin();
-  if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->guard.is_true())
+  if(
+    in_t->is_goto() && !in_t->is_backwards_goto() &&
+    in_t->condition().is_true())
     return block_map[in_t];
 
   return {};

src/goto-instrument/cover_instrument_other.cpp

@@ -40,7 +40,7 @@ void cover_assertion_instrumentert::instrument(
   // turn into 'assert(false)' to avoid simplification
   if(is_non_cover_assertion(i_it))
   {
-    i_it->guard = false_exprt();
+    i_it->condition_nonconst() = false_exprt();
     initialize_source_location(
       i_it, id2string(i_it->source_location().get_comment()), function_id);
   }

src/goto-instrument/goto_program2code.cpp

@@ -199,7 +199,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
       return target;
 
     case ASSUME:
-      dest.add(code_assumet(target->guard));
+      dest.add(code_assumet(target->condition()));
       return target;
 
     case GOTO:
@@ -514,7 +514,7 @@ goto_programt::const_targett goto_program2codet::convert_do_while(
 {
   assert(loop_end->is_goto() && loop_end->is_backwards_goto());
 
-  code_dowhilet d(loop_end->guard, code_blockt());
+  code_dowhilet d(loop_end->condition(), code_blockt());
   simplify(d.cond(), ns);
 
   copy_source_location(loop_end->targets.front(), d);
@@ -547,7 +547,7 @@ goto_programt::const_targett goto_program2codet::convert_goto(
       (upper_bound==goto_program.instructions.end() ||
        upper_bound->location_number > loop_entry->second->location_number))
     return convert_goto_while(target, loop_entry->second, dest);
-  else if(!target->guard.is_true())
+  else if(!target->condition().is_true())
     return convert_goto_switch(target, upper_bound, dest);
   else if(!loop_last_stack.empty())
     return convert_goto_break_continue(target, upper_bound, dest);
@@ -574,10 +574,10 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
 
   if(target->get_target()==after_loop)
   {
-    w.cond()=not_exprt(target->guard);
+    w.cond() = not_exprt(target->condition());
     simplify(w.cond(), ns);
   }
-  else if(target->guard.is_true())
+  else if(target->condition().is_true())
   {
     target = convert_goto_goto(target, to_code_block(w.body()));
   }
@@ -594,13 +594,13 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
   loop_last_stack.pop_back();
 
   convert_labels(loop_end, to_code_block(w.body()));
-  if(loop_end->guard.is_false())
+  if(loop_end->condition().is_false())
   {
     to_code_block(w.body()).add(code_breakt());
   }
-  else if(!loop_end->guard.is_true())
+  else if(!loop_end->condition().is_true())
   {
-    code_ifthenelset i(not_exprt(loop_end->guard), code_breakt());
+    code_ifthenelset i(not_exprt(loop_end->condition()), code_breakt());
     simplify(i.cond(), ns);
 
     copy_source_location(target, i);
@@ -661,9 +661,9 @@ goto_programt::const_targett goto_program2codet::get_cases(
       cases_it!=upper_bound && cases_it!=first_target;
       ++cases_it)
   {
-    if(cases_it->is_goto() &&
-       !cases_it->is_backwards_goto() &&
-       cases_it->guard.is_true())
+    if(
+      cases_it->is_goto() && !cases_it->is_backwards_goto() &&
+      cases_it->condition().is_true())
     {
       default_target=cases_it->get_target();
 
@@ -684,16 +684,16 @@ goto_programt::const_targett goto_program2codet::get_cases(
       ++cases_it;
       break;
     }
-    else if(cases_it->is_goto() &&
-            !cases_it->is_backwards_goto() &&
-            (cases_it->guard.id()==ID_equal ||
-             cases_it->guard.id()==ID_or))
+    else if(
+      cases_it->is_goto() && !cases_it->is_backwards_goto() &&
+      (cases_it->condition().id() == ID_equal ||
+       cases_it->condition().id() == ID_or))
     {
       exprt::operandst eqs;
-      if(cases_it->guard.id()==ID_equal)
-        eqs.push_back(cases_it->guard);
+      if(cases_it->condition().id() == ID_equal)
+        eqs.push_back(cases_it->condition());
       else
-        eqs=cases_it->guard.operands();
+        eqs = cases_it->condition().operands();
 
       // goto conversion builds disjunctions in reverse order
       // to ensure convergence, we turn this around again
@@ -839,9 +839,9 @@ bool goto_program2codet::remove_default(
     }
 
     // jumps to default are ok
-    if(it->case_last->is_goto() &&
-       it->case_last->guard.is_true() &&
-       it->case_last->get_target()==default_target)
+    if(
+      it->case_last->is_goto() && it->case_last->condition().is_true() &&
+      it->case_last->get_target() == default_target)
       continue;
 
     // fall-through is ok
@@ -860,7 +860,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
   code_blockt &dest)
 {
   // try to figure out whether this was a switch/case
-  exprt eq_cand=target->guard;
+  exprt eq_cand = target->condition();
   if(eq_cand.id()==ID_or)
     eq_cand = to_or_expr(eq_cand).op0();
 
@@ -985,7 +985,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
       {
         UNREACHABLE;
         goto_programt::instructiont i=*(it->case_selector);
-        i.guard=true_exprt();
+        i.condition_nonconst() = true_exprt();
         goto_programt tmp;
         tmp.insert_before_swap(tmp.insert_before(tmp.instructions.end()), i);
         convert_goto_goto(tmp.instructions.begin(), c);
@@ -1048,13 +1048,13 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
       return target;
     }
 
-    has_else=
+    has_else =
       before_else->is_goto() &&
       before_else->get_target()->location_number > end_if->location_number &&
-      before_else->guard.is_true() &&
-      (upper_bound==goto_program.instructions.end() ||
-       upper_bound->location_number>=
-       before_else->get_target()->location_number);
+      before_else->condition().is_true() &&
+      (upper_bound == goto_program.instructions.end() ||
+       upper_bound->location_number >=
+         before_else->get_target()->location_number);
 
     if(has_else)
       end_if=before_else->get_target();
@@ -1071,7 +1071,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
       return convert_goto_goto(target, dest);
   }
 
-  code_ifthenelset i(not_exprt(target->guard), code_blockt());
+  code_ifthenelset i(not_exprt(target->condition()), code_blockt());
   copy_source_location(target, i);
   simplify(i.cond(), ns);
 
@@ -1132,7 +1132,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
   if(target->get_target()==loop_end &&
      loop_last_stack.back().second)
   {
-    code_ifthenelset i(target->guard, code_continuet());
+    code_ifthenelset i(target->condition(), code_continuet());
     simplify(i.cond(), ns);
 
     copy_source_location(target, i);
@@ -1156,7 +1156,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
 
   if(target->get_target()==after_loop)
   {
-    code_ifthenelset i(target->guard, code_breakt());
+    code_ifthenelset i(target->condition(), code_breakt());
     simplify(i.cond(), ns);
 
     copy_source_location(target, i);
@@ -1214,7 +1214,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_goto(
 
   code_gotot goto_code(label.str());
 
-  code_ifthenelset i(target->guard, std::move(goto_code));
+  code_ifthenelset i(target->condition(), std::move(goto_code));
   simplify(i.cond(), ns);
 
   copy_source_location(target, i);
@@ -1281,9 +1281,12 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
   // END THREAD
   // 2: code in existing thread
   /* check the structure and compute the iterators */
-  assert(next->is_goto() && next->guard.is_true());
-  assert(!next->is_backwards_goto());
-  assert(thread_start->location_number < next->get_target()->location_number);
+  DATA_INVARIANT(
+    next->is_goto() && next->condition().is_true(), "START THREAD pattern");
+  DATA_INVARIANT(!next->is_backwards_goto(), "START THREAD pattern");
+  DATA_INVARIANT(
+    thread_start->location_number < next->get_target()->location_number,
+    "START THREAD pattern");
   goto_programt::const_targett after_thread_start=thread_start;
   ++after_thread_start;