Defined CEGIS null object preprocessing tasks.

Author: Pascal Kesseli

src/cegis/Makefile

@@ -58,7 +58,7 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       refactor/learn/refactor_symex_learn.cpp \
       refactor/verify/refactor_symex_verify.cpp \
       refactor/facade/refactor_runner.cpp \
-      refactor/options/refactor_program.cpp refactor/value/refactor_solution.cpp \
+      refactor/options/refactoring_type.cpp refactor/options/refactor_program.cpp refactor/value/refactor_solution.cpp \
       refactor/nullobject/range_collector.cpp \
       wordsize/restrict_bv_size.cpp value/program_individual_serialisation.cpp value/assignments_printer.cpp \
       seed/literals_seed.cpp \

src/cegis/cegis-util/type_helper.cpp

@@ -55,6 +55,7 @@ instanceof_anyt::instanceof_anyt(const symbol_tablet &st,
 
 bool instanceof_anyt::operator ()(const typet &type) const
 {
+  if (types.empty()) return true;
   return types.end()
       != std::find_if(types.begin(), types.end(),
           [this, &type](const typet &rhs)

src/cegis/control/preprocessing/control_preprocessing.cpp

@@ -17,7 +17,7 @@ namespace
 const char * const excluded_functions[]={
     "verify_stability_closedloop_using_dslib", "check_stability_closedloop",
     "fxp_double_to_fxp", "fxp_to_double", "ft_closedloop_series", "poly_mult",
-    "poly_sum", "internal_pow" };
+    "poly_sum", "internal_pow", "fxp_check", "fxp_control_floatt_to_fxp" };
 
 bool is_meta(const goto_programt::const_targett pos)
 {

src/cegis/refactor/environment/instrument_state_vars.cpp

@@ -1,7 +1,36 @@
 #include <cegis/refactor/environment/instrument_state_vars.h>
 
-void instrument_state_vars(goto_programt &body,
-    const goto_programt::targett &first, const goto_programt::targett &last,
+namespace
+{
+class var_findert: public const_expr_visitort
+{
+public:
+  std::set<irep_idt> vars;
+
+  virtual ~var_findert()=default;
+
+  virtual void operator()(const exprt &expr)
+  {
+    if (ID_symbol != expr.id()) return;
+    vars.insert(to_symbol_expr(expr).get_identifier());
+  }
+};
+}
+
+std::set<irep_idt> collect_state_vars(goto_programt::const_targett first,
+    const goto_programt::const_targett last)
+{
+  var_findert visitor;
+  for (; first != last; ++first)
+  {
+    first->code.visit(visitor);
+    first->guard.visit(visitor);
+  }
+  return visitor.vars;
+}
+
+void instrument_program_ops(goto_programt &body, goto_programt::targett pos,
+    const std::set<irep_idt> &state_vars,
     const std::function<bool(const typet &)> predicate)
 {
   // TODO: Implement
@@ -10,14 +39,14 @@ void instrument_state_vars(goto_programt &body,
 
 namespace
 {
-bool yes(const typet &instr)
+bool use_all(const typet &instr)
 {
   return true;
 }
 }
 
-void instrument_state_vars(goto_programt &body,
-    const goto_programt::targett &first, const goto_programt::targett &last)
+void instrument_program_ops(goto_programt &body, goto_programt::targett pos,
+    const std::set<irep_idt> &state_vars)
 {
-  instrument_state_vars(body, first, last, yes);
+  instrument_program_ops(body, pos, state_vars, use_all);
 }

src/cegis/refactor/environment/instrument_state_vars.h

@@ -19,15 +19,29 @@
  *
  * @details
  *
- * @param body
  * @param first
  * @param last
+ *
+ * @return
+ */
+std::set<irep_idt> collect_state_vars(
+    goto_programt::const_targett first,
+    goto_programt::const_targett last);
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param body
+ * @param pos
+ * @param state_vars
  * @param predicate
  */
-void instrument_state_vars(
+void instrument_program_ops(
     goto_programt &body,
-    const goto_programt::targett &first,
-    const goto_programt::targett &last,
+    goto_programt::targett pos,
+    const std::set<irep_idt> &state_vars,
     std::function<bool(const typet &)> predicate);
 
 /**
@@ -36,12 +50,12 @@ void instrument_state_vars(
  * @details
  *
  * @param body
- * @param first
- * @param last
+ * @param pos
+ * @param state_vars
  */
-void instrument_state_vars(
+void instrument_program_ops(
     goto_programt &body,
-    const goto_programt::targett &first,
-    const goto_programt::targett &last);
+    goto_programt::targett pos,
+    const std::set<irep_idt> &state_vars);
 
 #endif /* CEGIS_REFACTOR_ENVIRONMENT_INSTRUMENT_STATE_VARS_H_ */

src/cegis/refactor/nullobject/range_collector.cpp

@@ -36,11 +36,12 @@ void collect_nullobject_ranges(refactor_programt &prog)
     if (goto_program_instruction_typet::GOTO != it->type) continue;
     const exprt &guard=it->guard;
     if (!is_null_comparison(guard)) continue;
+    prog.sketches.push_back(refactor_programt::sketcht());
+    refactor_programt::sketcht &sketch=prog.sketches.back();
+    sketch.init=it;
     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));
-    prog.sketches.push_back(refactor_programt::sketcht());
-    refactor_programt::sketcht &sketch=prog.sketches.back();
     if (ID_equal == guard.id())
     {
       sketch.spec_range=then_range;

src/cegis/refactor/options/refactor_program.h

@@ -42,8 +42,10 @@ class refactor_programt
   class sketcht
   {
   public:
+    goto_programt::targett init;
     goto_ranget input_range;
     goto_ranget spec_range;
+    std::set<irep_idt> state_vars;
     std::set<typet> types;
   };
 

src/cegis/refactor/options/refactoring_type.cpp

@@ -0,0 +1,13 @@
+#include <cassert>
+
+#include <util/options.h>
+
+#include <cegis/options/parameters.h>
+#include <cegis/refactor/options/refactoring_type.h>
+
+refactoring_typet get_refactoring_type(const class optionst &options)
+{
+  if (options.get_bool_option(CEGIS_NULL_OBJECT_REFACTOR))
+    return refactoring_typet::NULL_OBJECT;
+  assert(!"Invalid refactoring type selected.");
+}

src/cegis/refactor/options/refactoring_type.h

@@ -0,0 +1,29 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, [email protected]
+         Pascal Kesseli, [email protected]
+
+ \*******************************************************************/
+
+#ifndef CEGIS_REFACTOR_OPTIONS_REFACTORING_TYPE_H_
+#define CEGIS_REFACTOR_OPTIONS_REFACTORING_TYPE_H_
+
+typedef enum
+{
+  NULL_OBJECT
+} refactoring_typet;
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param options
+ *
+ * @return
+ */
+refactoring_typet get_refactoring_type(const class optionst &options);
+
+#endif /* CEGIS_REFACTOR_OPTIONS_REFACTORING_TYPE_H_ */

src/cegis/refactor/preprocessing/refactor_preprocessing.cpp

@@ -2,10 +2,10 @@
 
 #include <util/options.h>
 
-#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/options/refactoring_type.h>
 #include <cegis/refactor/environment/instrument_state_vars.h>
 #include <cegis/refactor/nullobject/range_collector.h>
 #include <cegis/refactor/preprocessing/refactor_preprocessing.h>
@@ -21,19 +21,25 @@ void refactor_preprocessingt::operator()()
   const symbol_tablet &st=original_program.st;
   goto_functionst &gf=original_program.gf;
   inline_user_program(st, gf);
-  if (options.get_bool_option(CEGIS_NULL_OBJECT_REFACTOR))
+  const refactoring_typet type(get_refactoring_type(options));
+  switch (type)
   {
+  case refactoring_typet::NULL_OBJECT:
     collect_nullobject_ranges(original_program);
-    for (refactor_programt::sketcht &sketch : original_program.sketches)
-    {
-      goto_ranget &input_range=sketch.input_range;
-      goto_programt &body=get_body(gf, input_range.first);
-      const instanceof_anyt pred(st, sketch.types);
-      instrument_state_vars(body, input_range.first, input_range.second, pred);
-    }
-    // TODO: collect_
+    // TODO: Insert GOTOs between ranges
+    break;
+  }
+  for (refactor_programt::sketcht &s : original_program.sketches)
+    s.state_vars=collect_state_vars(s.spec_range.first, s.spec_range.second);
+  // TODO: Insert extern programs.
+  // TODO: construct_instruction_set(original_program); // Multiple?
+  switch (type)
+  {
+  case refactoring_typet::NULL_OBJECT:
+    // TODO: Replace method calls by program execution.
+    // TODO: Instrument ops (globals + params from corresponding replaced method call)
+    break;
   }
-  // TODO: construct_instruction_set(original_program);
   // TODO: Implement
   assert(false);
 }