Extended draft implementation for CEGIS null object.

Author: pkesseli

src/cegis/cegis-util/instruction_iterator.cpp

@@ -71,9 +71,4 @@ instr_iteratort::operator goto_programt::targett() const
   return prog_it;
 }
 
-goto_programt::targett instr_iteratort::body_end() const
-{
-  return func_it->second.body.instructions.end();
-}
-
 const instr_iteratort instr_iteratort::end;

src/cegis/cegis-util/instruction_iterator.h

@@ -105,15 +105,6 @@ class instr_iteratort: public std::iterator<std::input_iterator_tag,
    */
   operator goto_programt::targett() const;
 
-  /**
-   * @brief
-   *
-   * @details
-   *
-   * @return
-   */
-  goto_programt::targett body_end() const;
-
   /**
    * @brief
    *

src/cegis/cegis-util/program_helper.cpp

@@ -19,9 +19,7 @@ const goto_programt &get_entry_body(const goto_functionst &gf)
   return get_body(gf, id2string(goto_functionst::entry_point()));
 }
 
-class goto_programt &get_body(
-    class goto_functionst &gf,
-    const std::string &func_name)
+goto_programt &get_body(goto_functionst &gf, const std::string &func_name)
 {
   const irep_idt id(func_name);
   goto_functionst::function_mapt &function_map=gf.function_map;
@@ -32,8 +30,12 @@ class goto_programt &get_body(
   return f.body;
 }
 
-const goto_programt &get_body(
-    const goto_functionst &gf,
+goto_programt &get_body(goto_functionst &gf, const goto_programt::const_targett pos)
+{
+  return get_body(gf, id2string(pos->function));
+}
+
+const goto_programt &get_body(const goto_functionst &gf,
     const std::string &func_name)
 {
   const irep_idt id(func_name);

src/cegis/cegis-util/program_helper.h

@@ -44,10 +44,24 @@ const goto_programt &get_entry_body(const goto_functionst &gf);
  *
  * @return
  */
-class goto_programt &get_body(
-    class goto_functionst &gf,
+goto_programt &get_body(
+    goto_functionst &gf,
     const std::string &func_name);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param gf
+ * @param pos
+ *
+ * @return
+ */
+goto_programt &get_body(
+    goto_functionst &gf,
+    goto_programt::const_targett pos);
+
 /**
  * @brief
  *

src/cegis/cegis-util/type_helper.cpp

@@ -1,5 +1,7 @@
 #include <util/std_types.h>
 #include <util/symbol_table.h>
+#include <util/type_eq.h>
+#include <util/namespace.h>
 
 #define TAG_PREFIX "tag-"
 
@@ -13,3 +15,30 @@ const typet &replace_struct_by_symbol_type(const symbol_tablet &st,
   tag+=id2string(to_struct_union_type(type).get_tag());
   return st.lookup(tag).type;
 }
+
+namespace
+{
+bool instanceof(const typet &lhs, const typet &rhs, const namespacet &ns)
+{
+  if (type_eq(lhs, rhs, ns)) return true;
+  assert(ID_class == lhs.id());
+  const class_typet &lhs_class=to_class_type(lhs);
+  const irept::subt &bases=lhs_class.bases();
+  for (const irept &base : bases)
+  {
+    const typet &type=static_cast<const typet &>(base.find(ID_type));
+    if (instanceof(ns.follow(type), rhs, ns)) return true;
+  }
+  return false;
+}
+}
+
+bool instanceof(const symbol_tablet &st, const typet &lhs, const typet &rhs)
+{
+  const namespacet ns(st);
+  const typet &resolved_lhs=ns.follow(lhs);
+  const typet &resolved_rhs=ns.follow(rhs);
+  if (ID_class != resolved_lhs.id() || ID_class != resolved_rhs.id())
+    return type_eq(resolved_lhs, resolved_rhs, ns);
+  return instanceof(resolved_lhs, resolved_rhs, ns);
+}

src/cegis/cegis-util/type_helper.h

@@ -22,4 +22,15 @@ const class typet &replace_struct_by_symbol_type(
     const class symbol_tablet &st,
     const typet &type);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param lhs
+ * @param rhs
+ * @param st
+ */
+bool instanceof(const symbol_tablet &st, const typet &lhs, const typet &rhs);
+
 #endif /* CEGIS_UTIL_TYPE_HELPER_H_ */

src/cegis/refactor/environment/instrument_state_vars.cpp

@@ -1,8 +1,23 @@
 #include <cegis/refactor/environment/instrument_state_vars.h>
 
-void instrument_state_vars(const goto_programt::const_targett first,
-    const goto_programt::const_targett last)
+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)
 {
   // TODO: Implement
   assert(false);
 }
+
+namespace
+{
+bool yes(const goto_programt::instructiont &instr)
+{
+  return true;
+}
+}
+
+void instrument_state_vars(goto_programt &body,
+    const goto_programt::targett &first, const goto_programt::targett &last)
+{
+  instrument_state_vars(body, first, last, yes);
+}

src/cegis/refactor/environment/instrument_state_vars.h

@@ -10,18 +10,38 @@
 #ifndef CEGIS_REFACTOR_ENVIRONMENT_INSTRUMENT_STATE_VARS_H_
 #define CEGIS_REFACTOR_ENVIRONMENT_INSTRUMENT_STATE_VARS_H_
 
+#include <functional>
+
 #include <goto-programs/goto_program.h>
 
 /**
  * @brief
  *
  * @details
  *
+ * @param body
+ * @param first
+ * @param last
+ * @param predicate
+ */
+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);
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param body
  * @param first
  * @param last
  */
 void instrument_state_vars(
-    goto_programt::const_targett first,
-    goto_programt::const_targett last);
+    goto_programt &body,
+    const goto_programt::targett &first,
+    const goto_programt::targett &last);
 
 #endif /* CEGIS_REFACTOR_ENVIRONMENT_INSTRUMENT_STATE_VARS_H_ */

src/cegis/refactor/instructionset/create_cegis_processor.cpp

@@ -1,5 +1,30 @@
 #include <cegis/refactor/instructionset/create_cegis_processor.h>
 
+namespace
+{
+class type_collectort: public const_expr_visitort
+{
+public:
+  std::set<typet> types;
+
+  virtual ~type_collectort()=default;
+
+  virtual void operator()(const exprt &expr)
+  {
+    types.insert(expr.type());
+  }
+};
+}
+
+std::set<typet> collect_context_types(goto_programt::const_targett first,
+    const goto_programt::const_targett &last)
+{
+  type_collectort collector;
+  for (; first != last; ++first)
+    first->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)
 {

src/cegis/refactor/instructionset/create_cegis_processor.h

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

src/cegis/refactor/nullobject/range_collector.cpp

@@ -1,40 +1,22 @@
 #include <cegis/cegis-util/instruction_iterator.h>
-
 #include <cegis/refactor/options/refactor_program.h>
+#include <cegis/refactor/instructionset/create_cegis_processor.h>
 #include <cegis/refactor/nullobject/range_collector.h>
 
-// XXX: Debug
-#include <iostream>
-// XXX: Debug
-
 namespace
 {
+bool is_null(const exprt &expr)
+{
+  if (ID_constant != expr.id()) return false;
+  return ID_NULL == to_constant_expr(expr).get_value();
+}
+
 bool is_null_comparison(const exprt &guard)
 {
   const irep_idt &id=guard.id();
   if (ID_equal != id && ID_notequal != id) return false;
   const binary_relation_exprt &binary=to_binary_relation_expr(guard);
-  return ID_NULL == binary.lhs().id() || ID_NULL == binary.rhs().id();
-}
-
-class null_reference_type_extractort: public const_expr_visitort
-{
-public:
-  typet reference_type;
-
-  virtual ~null_reference_type_extractort()=default;
-
-  virtual void operator()(const exprt &expr)
-  {
-    if (ID_symbol == expr.id()) reference_type=expr.type();
-  }
-};
-
-typet get_reference_type(const exprt &guard)
-{
-  null_reference_type_extractort extractor;
-  guard.visit(extractor);
-  return extractor.reference_type;
+  return is_null(binary.lhs()) || is_null(binary.rhs());
 }
 
 goto_ranget get_then_range(const goto_programt::targett &else_range_last)
@@ -52,25 +34,25 @@ void collect_nullobject_ranges(refactor_programt &prog)
   for (instr_iteratort it(prog.gf); it != instr_iteratort::end; ++it)
   {
     if (goto_program_instruction_typet::GOTO != it->type) continue;
-    if (!is_null_comparison(it->guard)) continue;
+    const exprt &guard=it->guard;
+    if (!is_null_comparison(guard)) continue;
     const goto_programt::targett else_range_last(it->get_target());
     const goto_ranget else_range(++it, else_range_last);
     const goto_ranget then_range(get_then_range(else_range_last));
-    if (ID_equal == it->guard.id())
+    prog.sketches.push_back(refactor_programt::sketcht());
+    refactor_programt::sketcht &sketch=prog.sketches.back();
+    if (ID_equal == guard.id())
     {
-      prog.spec_ranges.push_back(else_range);
-      prog.input_ranges.push_back(then_range);
+      sketch.spec_range=then_range;
+      sketch.input_range=else_range;
     } else
     {
-      prog.spec_ranges.push_back(then_range);
-      prog.input_ranges.push_back(else_range);
+      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.insert(tmp.begin(), tmp.end());
   }
-  // XXX: Debug
-  std::cout << "<collect_nullobject_range>" << std::endl;
-  prog.gf.output(namespacet(prog.st), std::cout);
-  std::cout << "</collect_nullobject_range>" << std::endl;
-  // XXX: Debug
-  // TODO: Implement
-  assert(false);
 }

src/cegis/refactor/options/refactor_program.h

@@ -39,14 +39,20 @@ class refactor_programt
    *
    * @details
    */
-  std::deque<goto_ranget> input_ranges;
+  class sketcht
+  {
+  public:
+    goto_ranget input_range;
+    goto_ranget spec_range;
+    std::set<typet> types;
+  };
 
   /**
    * @brief
    *
    * @details
    */
-  std::deque<goto_ranget> spec_ranges;
+  std::deque<sketcht> sketches;
 
   /**
    * @brief