Extended null object CEGIS implementation.

Author: Pascal Kesseli

src/cegis/cegis-util/type_helper.cpp

@@ -1,8 +1,12 @@
+#include <algorithm>
+
 #include <util/std_types.h>
 #include <util/symbol_table.h>
 #include <util/type_eq.h>
 #include <util/namespace.h>
 
+#include <cegis/cegis-util/type_helper.h>
+
 #define TAG_PREFIX "tag-"
 
 const typet &replace_struct_by_symbol_type(const symbol_tablet &st,
@@ -42,3 +46,17 @@ bool instanceof(const symbol_tablet &st, const typet &lhs, const typet &rhs)
     return type_eq(resolved_lhs, resolved_rhs, ns);
   return instanceof(resolved_lhs, resolved_rhs, ns);
 }
+
+instanceof_anyt::instanceof_anyt(const symbol_tablet &st,
+    const std::set<typet> &types) :
+    st(st), types(types)
+{
+}
+
+bool instanceof_anyt::operator ()(const typet &type) const
+{
+  return types.end()
+      != std::find_if(types.begin(), types.end(),
+          [this, &type](const typet &rhs)
+          { return instanceof(st, type, rhs);});
+}

src/cegis/cegis-util/type_helper.h

@@ -10,6 +10,8 @@
 #ifndef CEGIS_UTIL_TYPE_HELPER_H_
 #define CEGIS_UTIL_TYPE_HELPER_H_
 
+#include <set>
+
 /**
  * @brief
  *
@@ -33,4 +35,36 @@ const class typet &replace_struct_by_symbol_type(
  */
 bool instanceof(const symbol_tablet &st, const typet &lhs, const typet &rhs);
 
+/**
+ * @brief
+ *
+ * @details
+ */
+class instanceof_anyt
+{
+  const symbol_tablet &st;
+  const std::set<typet> &types;
+public:
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @param st
+   * @param types
+   */
+  instanceof_anyt(const symbol_tablet &st, const std::set<typet> &types);
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @param type
+   *
+   * @return
+   */
+  bool operator()(const typet &type) const;
+};
+
 #endif /* CEGIS_UTIL_TYPE_HELPER_H_ */

src/cegis/refactor/environment/instrument_state_vars.cpp

@@ -2,15 +2,15 @@
 
 void instrument_state_vars(goto_programt &body,
     const goto_programt::targett &first, const goto_programt::targett &last,
-    std::function<bool(const goto_programt::instructiont &)> predicate)
+    const std::function<bool(const typet &)> predicate)
 {
   // TODO: Implement
   assert(false);
 }
 
 namespace
 {
-bool yes(const goto_programt::instructiont &instr)
+bool yes(const typet &instr)
 {
   return true;
 }

src/cegis/refactor/environment/instrument_state_vars.h

@@ -28,7 +28,7 @@ void instrument_state_vars(
     goto_programt &body,
     const goto_programt::targett &first,
     const goto_programt::targett &last,
-    std::function<bool(const goto_programt::instructiont &)> predicate);
+    std::function<bool(const typet &)> predicate);
 
 /**
  * @brief

src/cegis/refactor/instructionset/create_cegis_processor.cpp

@@ -16,17 +16,17 @@ class type_collectort: public const_expr_visitort
 };
 }
 
-std::set<typet> collect_context_types(goto_programt::const_targett first,
-    const goto_programt::const_targett &last)
+std::set<typet> collect_context_types(const goto_ranget &range)
 {
   type_collectort collector;
-  for (; first != last; ++first)
-    first->code.visit(collector);
+  for (goto_programt::const_targett it(range.first); it != range.second; ++it)
+    it->code.visit(collector);
   return collector.types;
 }
 
 void create_cegis_processor(const std::set<typet> &state_types,
     const size_t var_slots_per_state_type, const std::set<typet> &context_types)
 {
-
+  // TODO: Implement
+  assert(false);
 }

src/cegis/refactor/instructionset/create_cegis_processor.h

@@ -13,21 +13,19 @@
 #include <set>
 
 #include <util/type.h>
-#include <goto-programs/goto_program.h>
+
+#include <cegis/cegis-util/goto_range.h>
 
 /**
  * @brief
  *
  * @details
  *
- * @param first
- * @param last
+ * @param range
  *
  * @return
  */
-std::set<typet> collect_context_types(
-    goto_programt::const_targett first,
-    const goto_programt::const_targett &last);
+std::set<typet> collect_context_types(const goto_ranget &range);
 
 /**
  * @brief

src/cegis/refactor/nullobject/range_collector.cpp

@@ -50,9 +50,8 @@ void collect_nullobject_ranges(refactor_programt &prog)
       sketch.spec_range=else_range;
       sketch.input_range=then_range;
     }
-    sketch.types=collect_context_types(then_range.first, then_range.second);
-    const std::set<typet> tmp(
-        collect_context_types(else_range.first, else_range.second));
+    sketch.types=collect_context_types(then_range);
+    const std::set<typet> tmp(collect_context_types(else_range));
     sketch.types.insert(tmp.begin(), tmp.end());
   }
 }

src/cegis/refactor/preprocessing/refactor_preprocessing.cpp

@@ -5,6 +5,7 @@
 #include <cegis/options/parameters.h>
 #include <cegis/cegis-util/inline_user_program.h>
 #include <cegis/cegis-util/program_helper.h>
+#include <cegis/cegis-util/type_helper.h>
 #include <cegis/refactor/environment/instrument_state_vars.h>
 #include <cegis/refactor/nullobject/range_collector.h>
 #include <cegis/refactor/preprocessing/refactor_preprocessing.h>
@@ -27,9 +28,7 @@ void refactor_preprocessingt::operator()()
     {
       goto_ranget &input_range=sketch.input_range;
       goto_programt &body=get_body(gf, input_range.first);
-      const std::function<bool(const goto_programt::instructiont &)> pred=
-          [&st, &sketch](const goto_programt::instructiont &instr)
-          { return false;};
+      const instanceof_anyt pred(st, sketch.types);
       instrument_state_vars(body, input_range.first, input_range.second, pred);
     }
     // TODO: collect_