Cleaned up body in primitive CEGIS processor.

Author: pkesseli

src/cegis/refactor/instructionset/cegis_processor_body_factory.cpp

@@ -1,3 +1,5 @@
+#include <algorithm>
+
 #include <ansi-c/expr2c.h>
 #include <util/arith_tools.h>
 #include <util/expr_util.h>
@@ -13,6 +15,10 @@
 #define OPERAND_TMP_RESULT_PREFIX "result_op_"
 #define INSTR_INDEX "i"
 
+// XXX: Debug
+#include <iostream>
+// XXX: Debug
+
 std::string cegis_operand_base_name(const size_t op)
 {
   std::string name(OPERAND_ID_MEMBER_NAME_PREFIX);
@@ -370,6 +376,49 @@ class body_factoryt
     add_goto(guard, loop_head);
   }
 };
+
+bool is_forward_goto(const goto_programt::instructiont &instr)
+{
+  return instr.is_goto() && !instr.is_backwards_goto();
+}
+
+void remove_singleton_switch_cases(goto_programt &body)
+{
+  body.compute_location_numbers();
+  goto_programt::instructionst &instrs=body.instructions;
+  const goto_programt::targett end(instrs.end());
+  for (goto_programt::targett pos=instrs.begin(); pos != end; ++pos)
+  {
+    if (!is_forward_goto(*pos)) continue;
+    const auto pred(std::mem_fun_ref(goto_programt::instructiont::is_skip));
+    const goto_programt::targett tail=std::find_if(pos, end, pred);
+    assert(end != tail);
+    if (pos->get_target() == tail) instrs.erase(pos);
+    pos=tail;
+  }
+}
+
+void remove_goto_next(goto_programt::instructionst &instrs)
+{
+  for (goto_programt::targett pos=instrs.begin(); pos != instrs.end(); ++pos)
+    if (is_forward_goto(*pos) && pos->get_target() == std::next(pos))
+      pos=instrs.erase(pos);
+}
+
+void remove_skips(goto_programt::instructionst &instrs)
+{
+  const goto_programt::targett first(instrs.begin());
+  const goto_programt::targett last(instrs.end());
+  for (goto_programt::targett pos=first; pos != last; ++pos)
+  {
+    if (!pos->is_skip()) continue;
+    const goto_programt::targett successor(std::next(pos));
+    for (goto_programt::instructiont &instr : instrs)
+      for (goto_programt::targett &target : instr.targets)
+        if (target == pos) target=successor;
+    pos=instrs.erase(pos);
+  }
+}
 }
 
 void generate_processor_body(symbol_tablet &st, goto_programt &body,
@@ -387,9 +436,9 @@ void generate_processor_body(symbol_tablet &st, goto_programt &body,
     factory.add_index_goto();
   }
   body.add_instruction(goto_program_instruction_typet::END_FUNCTION);
-  // TODO: Remove single-switch-cases
-  // TODO: Remove goto-next
-  // TODO: Remove skips
+  remove_singleton_switch_cases(body);
+  remove_goto_next(body.instructions);
+  remove_skips(body.instructions);
   body.compute_loop_numbers();
   body.update();
 }