introduce INCOMPLETE_GOTO and turn guarded goto into a stateless pass

regression/cbmc/goto5/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main(void)
+{
+  int r = 0;
+
+  if(r == 0)
+  {
+    goto l1;
+    r = 1;
+  }
+
+l1:
+  assert(r != 0); // expected to fail
+}

regression/cbmc/goto5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/analyses/goto_rw.cpp

@@ -719,6 +719,7 @@ void goto_rw(goto_programt::const_targett target,
   switch(target->type)
   {
   case NO_INSTRUCTION_TYPE:
+  case INCOMPLETE_GOTO:
     UNREACHABLE;
     break;
 

src/goto-instrument/goto_program2code.cpp

@@ -245,6 +245,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
       return convert_catch(target, upper_bound, dest);
 
     case NO_INSTRUCTION_TYPE:
+    case INCOMPLETE_GOTO:
       UNREACHABLE;
   }
 

src/goto-programs/cfg.h

@@ -418,6 +418,7 @@ void cfg_baset<T, P, I>::compute_edges(
     break;
 
   case NO_INSTRUCTION_TYPE:
+  case INCOMPLETE_GOTO:
     UNREACHABLE;
     break;
   }

src/goto-programs/goto_convert.cpp

@@ -138,9 +138,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
         throw 0;
       }
 
-      i.type=GOTO;
-      i.targets.clear();
-      i.targets.push_back(l_it->second.first);
+      i.complete_goto(l_it->second.first);
 
       // If the goto recorded a destructor stack, execute as much as is
       // appropriate for however many automatic variables leave scope.
@@ -234,45 +232,49 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program)
   targets.computed_gotos.clear();
 }
 
-/// For each if(x) goto z; goto y; z: emitted, see if any destructor statements
-/// were inserted between goto z and z, and if not, simplify into if(!x) goto y;
+/// Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;"
+/// This only works if the "goto y" is not a branch target.
 /// \par parameters: Destination goto program
-void goto_convertt::finish_guarded_gotos(goto_programt &dest)
+void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
 {
-  for(auto &gg : guarded_gotos)
+  // We cannot use a set of targets, as target iterators
+  // cannot be compared at this stage.
+
+  // collect targets: reset marking
+  for(auto &i : dest.instructions)
+    i.target_number = goto_programt::instructiont::nil_target;
+
+  // mark the goto targets
+  unsigned cnt = 0;
+  for(const auto &i : dest.instructions)
+    if(i.is_goto())
+      i.get_target()->target_number = (++cnt);
+
+  for(auto it = dest.instructions.begin(); it != dest.instructions.end(); it++)
   {
-    // Check if any destructor code has been inserted:
-    bool destructor_present=false;
-    for(auto it=gg.ifiter;
-        it!=gg.gotoiter && !destructor_present;
-        ++it)
-    {
-      if(!(it->is_goto() || it->is_skip()))
-        destructor_present=true;
-    }
+    if(!it->is_goto())
+      continue;
+
+    auto it_goto_y = std::next(it);
 
-    // If so, can't simplify.
-    if(destructor_present)
+    if(
+      it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
+      !it_goto_y->guard.is_true() || it_goto_y->is_target())
       continue;
 
-    // Simplify: remove whatever code was generated for the condition
-    // and attach the original guard to the goto instruction.
-    gg.gotoiter->guard=gg.guard;
-    // inherit the source location (otherwise the guarded goto will
-    // have the source location of the else branch)
-    gg.gotoiter->source_location=gg.ifiter->source_location;
-    // goto_programt doesn't provide an erase operation,
-    // perhaps for a good reason, so let's be cautious and just
-    // flatten the unneeded instructions into skips.
-    for(auto it=gg.ifiter, itend=gg.gotoiter; it!=itend; ++it)
-      it->make_skip();
-  }
+    auto it_z = std::next(it_goto_y);
 
-  // Must clear this, as future functions may be converted
-  // using the same instance of goto_convertt, typically via
-  // goto_convert_functions.
+    if(it_z == dest.instructions.end())
+      continue;
 
-  guarded_gotos.clear();
+    // cannot compare iterators, so compare target number instead
+    if(it->get_target()->target_number == it_z->target_number)
+    {
+      it->set_target(it_goto_y->get_target());
+      it->guard = boolean_negate(it->guard);
+      it_goto_y->make_skip();
+    }
+  }
 }
 
 void goto_convertt::goto_convert(
@@ -288,14 +290,11 @@ void goto_convertt::goto_convert_rec(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  // Check that guarded_gotos was cleared after any previous use of this
-  // converter instance:
-  PRECONDITION(guarded_gotos.empty());
   convert(code, dest, mode);
 
   finish_gotos(dest, mode);
   finish_computed_gotos(dest);
-  finish_guarded_gotos(dest);
+  optimize_guarded_gotos(dest);
   finish_catch_push_targets(dest);
 }
 
@@ -493,13 +492,11 @@ void goto_convertt::convert(
   else if(statement==ID_continue)
     convert_continue(to_code_continue(code), dest, mode);
   else if(statement==ID_goto)
-    convert_goto(code, dest);
+    convert_goto(to_code_goto(code), dest);
   else if(statement==ID_gcc_computed_goto)
     convert_gcc_computed_goto(code, dest);
   else if(statement==ID_skip)
     convert_skip(code, dest);
-  else if(statement=="non-deterministic-goto")
-    convert_non_deterministic_goto(code, dest);
   else if(statement==ID_ifthenelse)
     convert_ifthenelse(to_code_ifthenelse(code), dest, mode);
   else if(statement==ID_start_thread)
@@ -1456,16 +1453,12 @@ void goto_convertt::convert_continue(
   t->source_location=code.source_location();
 }
 
-void goto_convertt::convert_goto(
-  const codet &code,
-  goto_programt &dest)
+void goto_convertt::convert_goto(const code_gotot &code, goto_programt &dest)
 {
   // this instruction will be completed during post-processing
-  // it is required to mark this as GOTO in order to enable
-  // simplifications in generate_ifthenelse
-  goto_programt::targett t = dest.add_instruction(GOTO);
+  goto_programt::targett t = dest.add_instruction();
+  t->make_incomplete_goto(code);
   t->source_location=code.source_location();
-  t->code=code;
 
   // remember it to do the target later
   targets.gotos.push_back(std::make_pair(t, targets.destructor_stack));
@@ -1484,13 +1477,6 @@ void goto_convertt::convert_gcc_computed_goto(
   targets.computed_gotos.push_back(t);
 }
 
-void goto_convertt::convert_non_deterministic_goto(
-  const codet &code,
-  goto_programt &dest)
-{
-  convert_goto(code, dest);
-}
-
 void goto_convertt::convert_start_thread(
   const codet &code,
   goto_programt &dest)
@@ -1649,24 +1635,7 @@ void goto_convertt::generate_ifthenelse(
     return;
   }
 
-  bool is_guarded_goto=false;
-
-  // do guarded gotos directly
-  if(is_empty(false_case) &&
-     is_size_one(true_case) &&
-     true_case.instructions.back().is_goto() &&
-     true_case.instructions.back().guard.is_true() &&
-     true_case.instructions.back().labels.empty())
-  {
-    // The above conjunction deliberately excludes the instance
-    // if(some) { label: goto somewhere; }
-    // Don't perform the transformation here, as code might get inserted into
-    // the true case to perform destructors.
-    // This will be attempted in finish_guarded_gotos.
-    is_guarded_goto=true;
-  }
-
-  // similarly, do guarded assertions directly
+  // do guarded assertions directly
   if(is_size_one(true_case) &&
      true_case.instructions.back().is_assert() &&
      true_case.instructions.back().guard.is_false() &&
@@ -1779,13 +1748,6 @@ void goto_convertt::generate_ifthenelse(
   assert(!tmp_w.instructions.empty());
   x->source_location=tmp_w.instructions.back().source_location;
 
-  // See if we can simplify this guarded goto later.
-  // Note this depends on the fact that `instructions` is a std::list
-  // and so goto-program-destructive-append preserves iterator validity.
-  if(is_guarded_goto)
-    guarded_gotos.push_back(
-      {tmp_v.instructions.begin(), tmp_w.instructions.begin(), guard});
-
   dest.destructive_append(tmp_v);
   dest.destructive_append(tmp_w);
 

src/goto-programs/goto_convert_class.h

@@ -268,10 +268,9 @@ class goto_convertt:public messaget
     const irep_idt &mode);
   void
   convert_init(const codet &code, goto_programt &dest, const irep_idt &mode);
-  void convert_goto(const codet &code, goto_programt &dest);
+  void convert_goto(const code_gotot &code, goto_programt &dest);
   void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
   void convert_skip(const codet &code, goto_programt &dest);
-  void convert_non_deterministic_goto(const codet &code, goto_programt &dest);
   void convert_label(
     const code_labelt &code,
     goto_programt &dest,
@@ -355,7 +354,7 @@ class goto_convertt:public messaget
 
   void finish_gotos(goto_programt &dest, const irep_idt &mode);
   void finish_computed_gotos(goto_programt &dest);
-  void finish_guarded_gotos(goto_programt &dest);
+  void optimize_guarded_gotos(goto_programt &dest);
 
   typedef std::map<irep_idt,
                    std::pair<goto_programt::targett, destructor_stackt>>
@@ -545,15 +544,6 @@ class goto_convertt:public messaget
     std::size_t leave_stack_size;
   };
 
-  struct guarded_gotot
-  {
-    goto_programt::targett ifiter;
-    goto_programt::targett gotoiter;
-    exprt guard;
-  };
-  typedef std::list<guarded_gotot> guarded_gotost;
-  guarded_gotost guarded_gotos;
-
   exprt case_guard(
     const exprt &value,
     const caset &case_op);

src/goto-programs/goto_program.h

@@ -28,25 +28,26 @@ Author: Daniel Kroening, [email protected]
 /// The type of an instruction in a GOTO program.
 enum goto_program_instruction_typet
 {
-  NO_INSTRUCTION_TYPE=0,
-  GOTO=1,           // branch, possibly guarded
-  ASSUME=2,         // non-failing guarded self loop
-  ASSERT=3,         // assertions
-  OTHER=4,          // anything else
-  SKIP=5,           // just advance the PC
-  START_THREAD=6,   // spawns an asynchronous thread
-  END_THREAD=7,     // end the current thread
-  LOCATION=8,       // semantically like SKIP
-  END_FUNCTION=9,   // exit point of a function
-  ATOMIC_BEGIN=10,  // marks a block without interleavings
-  ATOMIC_END=11,    // end of a block without interleavings
-  RETURN=12,        // set function return value (no control-flow change)
-  ASSIGN=13,        // assignment lhs:=rhs
-  DECL=14,          // declare a local variable
-  DEAD=15,          // marks the end-of-live of a local variable
-  FUNCTION_CALL=16, // call a function
-  THROW=17,         // throw an exception
-  CATCH=18          // push, pop or enter an exception handler
+  NO_INSTRUCTION_TYPE = 0,
+  GOTO = 1,            // branch, possibly guarded
+  ASSUME = 2,          // non-failing guarded self loop
+  ASSERT = 3,          // assertions
+  OTHER = 4,           // anything else
+  SKIP = 5,            // just advance the PC
+  START_THREAD = 6,    // spawns an asynchronous thread
+  END_THREAD = 7,      // end the current thread
+  LOCATION = 8,        // semantically like SKIP
+  END_FUNCTION = 9,    // exit point of a function
+  ATOMIC_BEGIN = 10,   // marks a block without interleavings
+  ATOMIC_END = 11,     // end of a block without interleavings
+  RETURN = 12,         // set function return value (no control-flow change)
+  ASSIGN = 13,         // assignment lhs:=rhs
+  DECL = 14,           // declare a local variable
+  DEAD = 15,           // marks the end-of-live of a local variable
+  FUNCTION_CALL = 16,  // call a function
+  THROW = 17,          // throw an exception
+  CATCH = 18,          // push, pop or enter an exception handler
+  INCOMPLETE_GOTO = 19 // goto where target is yet to be determined
 };
 
 std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
@@ -253,6 +254,12 @@ class goto_programt
     void make_atomic_end() { clear(ATOMIC_END); }
     void make_end_function() { clear(END_FUNCTION); }
 
+    void make_incomplete_goto(const code_gotot &_code)
+    {
+      clear(INCOMPLETE_GOTO);
+      code = _code;
+    }
+
     void make_goto(targett _target)
     {
       clear(GOTO);
@@ -265,6 +272,13 @@ class goto_programt
       guard=g;
     }
 
+    void complete_goto(targett _target)
+    {
+      PRECONDITION(type == INCOMPLETE_GOTO);
+      targets.push_back(_target);
+      type = GOTO;
+    }
+
     void make_assignment(const codet &_code)
     {
       clear(ASSIGN);
@@ -301,6 +315,10 @@ class goto_programt
     bool is_start_thread () const { return type==START_THREAD;  }
     bool is_end_thread   () const { return type==END_THREAD;    }
     bool is_end_function () const { return type==END_FUNCTION;  }
+    bool is_incomplete_goto() const
+    {
+      return type == INCOMPLETE_GOTO;
+    }
 
     instructiont():
       instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)

src/goto-programs/string_abstraction.cpp

@@ -490,6 +490,8 @@ goto_programt::targett string_abstractiont::abstract(
   case OTHER:
   case LOCATION:
     break;
+
+  case INCOMPLETE_GOTO:
   case NO_INSTRUCTION_TYPE:
     UNREACHABLE;
     break;