Added null object range extraction.

Author: Pascal Kesseli

regression/cegis/cegis_refactor_benchmark_01/Runner.class

@@ -28,4 +28,6 @@ void print(ITaxCalculator calc, double price) {
   System.out.print(percentage);
   System.out.println('%');
 }
+static void main() {
+}
 }

regression/cegis/cegis_refactor_benchmark_01/Runner.java

@@ -0,0 +1,8 @@
+CORE
+Runner.class
+--gcc --cegis-refactor --cegis-refactor-null-object --cegis-statistics --cegis-genetic
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cegis/cegis_refactor_benchmark_01/test.desc

@@ -59,6 +59,7 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       refactor/verify/refactor_symex_verify.cpp \
       refactor/facade/refactor_runner.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 \
       genetic/instruction_set_info_factory.cpp genetic/random_mutate.cpp genetic/random_cross.cpp \
@@ -68,7 +69,7 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       cegis-util/task_pool.cpp cegis-util/constant_width.cpp cegis-util/irep_pipe.cpp cegis-util/program_helper.cpp \
       cegis-util/temporary_output_block.cpp cegis-util/cbmc_runner.cpp cegis-util/module_helper.cpp \
       cegis-util/inline_user_program.cpp cegis-util/counterexample_vars.cpp cegis-util/string_helper.cpp \
-      cegis-util/type_helper.cpp \
+      cegis-util/instruction_iterator.cpp cegis-util/type_helper.cpp \
       learn/insert_counterexample.cpp learn/constraint_helper.cpp \
       constant/add_constant.cpp constant/literals_collector.cpp constant/default_cegis_constant_strategy.cpp \
       instrument/cegis_library.cpp instrument/instrument_var_ops.cpp instrument/meta_variables.cpp \

src/cegis/Makefile

@@ -0,0 +1,17 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, [email protected]
+         Pascal Kesseli, [email protected]
+
+\*******************************************************************/
+
+#include <goto-programs/goto_program.h>
+
+/**
+ * @brief
+ *
+ * @details
+ */
+typedef std::pair<goto_programt::targett, goto_programt::targett> goto_ranget;

src/cegis/cegis-util/goto_range.h

@@ -4,7 +4,6 @@
 #include <goto-programs/goto_inline.h>
 
 #include <cegis/cegis-util/program_helper.h>
-#include <cegis/cegis-util/inline_user_program.h>
 
 namespace
 {

src/cegis/cegis-util/inline_user_program.cpp

@@ -9,7 +9,7 @@
 int run_refactor(optionst &options, messaget::mstreamt &result,
     const symbol_tablet &st, const goto_functionst &gf)
 {
-  refactor_preprocessingt preproc;
+  refactor_preprocessingt preproc(options, st, gf);
   refactor_symex_learnt learn_cfg;
   refactor_symex_verifyt verify_cfg;
   cegis_symex_learnt<refactor_preprocessingt, refactor_symex_learnt> learn(

src/cegis/refactor/facade/refactor_runner.cpp

@@ -0,0 +1,76 @@
+#include <cegis/cegis-util/instruction_iterator.h>
+
+#include <cegis/refactor/options/refactor_program.h>
+#include <cegis/refactor/nullobject/range_collector.h>
+
+// XXX: Debug
+#include <iostream>
+// XXX: Debug
+
+namespace
+{
+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;
+}
+
+goto_ranget get_then_range(const goto_programt::targett &else_range_last)
+{
+  const goto_programt::targett then_range_first(else_range_last);
+  const goto_programt::targett last_else_instr(std::prev(else_range_last));
+  if (GOTO != last_else_instr->type)
+    return goto_ranget(then_range_first, then_range_first);
+  return goto_ranget(then_range_first, last_else_instr->get_target());
+}
+}
+
+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 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.spec_ranges.push_back(else_range);
+      prog.input_ranges.push_back(then_range);
+    } else
+    {
+      prog.spec_ranges.push_back(then_range);
+      prog.input_ranges.push_back(else_range);
+    }
+  }
+  // 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/nullobject/range_collector.cpp

@@ -0,0 +1,20 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, [email protected]
+         Pascal Kesseli, [email protected]
+
+ \*******************************************************************/
+
+#ifndef CEGIS_REFACTOR_NULLOBJECT_RANGE_COLLECTOR_H_
+#define CEGIS_REFACTOR_NULLOBJECT_RANGE_COLLECTOR_H_
+
+/**
+ * @brief
+ *
+ * @details
+ */
+void collect_nullobject_ranges(class refactor_programt &prog);
+
+#endif /* CEGIS_REFACTOR_NULLOBJECT_RANGE_COLLECTOR_H_ */

src/cegis/refactor/nullobject/range_collector.h

@@ -10,8 +10,12 @@
 #ifndef CEGIS_REFACTOR_OPTIONS_REFACTOR_PROGRAM_H_
 #define CEGIS_REFACTOR_OPTIONS_REFACTOR_PROGRAM_H_
 
+#include <deque>
+
 #include <goto-programs/goto_functions.h>
 
+#include <cegis/cegis-util/goto_range.h>
+
 /**
  * @brief
  *
@@ -30,6 +34,20 @@ class refactor_programt
    */
   goto_programt::targetst counterexample_locations;
 
+  /**
+   * @brief
+   *
+   * @details
+   */
+  std::deque<goto_ranget> input_ranges;
+
+  /**
+   * @brief
+   *
+   * @details
+   */
+  std::deque<goto_ranget> spec_ranges;
+
   /**
    * @brief
    *

src/cegis/refactor/options/refactor_program.h

@@ -1,11 +1,23 @@
+#include <util/options.h>
+
+#include <cegis/options/parameters.h>
+#include <cegis/cegis-util/inline_user_program.h>
+#include <cegis/refactor/nullobject/range_collector.h>
 #include <cegis/refactor/preprocessing/refactor_preprocessing.h>
 
-refactor_preprocessingt::refactor_preprocessingt()
+refactor_preprocessingt::refactor_preprocessingt(const optionst &options,
+    const symbol_tablet &st, const goto_functionst &gf) :
+    options(options), original_program(st, gf)
 {
 }
 
 void refactor_preprocessingt::operator()()
 {
+  inline_user_program(original_program.st, original_program.gf);
+  if (options.get_bool_option(CEGIS_NULL_OBJECT_REFACTOR))
+  {
+    collect_nullobject_ranges(original_program);
+  }
   // TODO: Implement
   assert(false);
 }

src/cegis/refactor/preprocessing/refactor_preprocessing.cpp

@@ -19,13 +19,23 @@
  */
 class refactor_preprocessingt
 {
+  const class optionst &options;
+  refactor_programt original_program;
+  refactor_programt current_program;
 public:
   /**
    * @brief
    *
    * @details
+   *
+   * @param options
+   * @param st
+   * @param gf
    */
-  explicit refactor_preprocessingt();
+  explicit refactor_preprocessingt(
+      const optionst &options,
+      const symbol_tablet &st,
+      const goto_functionst &gf);
 
   /**
    * @brief

src/cegis/refactor/preprocessing/refactor_preprocessing.h

@@ -88,6 +88,7 @@ void cegis_parse_optionst::get_command_line_options(optionst &options)
     options.set_option(CEGIS_SHOW_ITERATIONS, cmdline.isset(CEGIS_SHOW_ITERATIONS));
     options.set_option(CEGIS_KEEP_GOTO_PROGRAMS, cmdline.isset(CEGIS_KEEP_GOTO_PROGRAMS));
     set_integer_option(options, cmdline, CEGIS_MAX_RUNTIME, 300u);
+    options.set_option(CEGIS_NULL_OBJECT_REFACTOR, cmdline.isset(CEGIS_NULL_OBJECT_REFACTOR));
   }
 }
 

src/cegis/runner/cegis_parse_options.cpp

@@ -20,7 +20,8 @@ Author: Daniel Kroening, [email protected]
   "(cegis-genetic-mutation-rate):(cegis-genetic-replace-rate):" \
   "(cegis-limit-wordsize)(cegis-parallel-verify)(cegis-symex-head-start):" \
   "(safety)(danger)(jsa)(danger-max-size):(danger-no-ranking)" \
-  "(cegis-control)"
+  "(cegis-control)" \
+  "(cegis-refactor)(cegis-refactor-null-object)"
 
 class cegis_parse_optionst: public cbmc_parse_optionst
 {