Extended CEGIS null object instrumentation.

Author: pkesseli

regression/cegis/cegis_refactor_benchmark_01/Runner.class

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

regression/cegis/cegis_refactor_benchmark_01/Runner.java

@@ -58,12 +58,13 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       refactor/instructionset/processor_types.cpp refactor/instructionset/cegis_processor_body_factory.cpp \
       refactor/instructionset/instruction_description.cpp refactor/instructionset/cegis_instruction_factory.cpp \
       refactor/instructionset/processor_symbols.cpp \
+      refactor/constraint/constraint_factory.cpp \
       refactor/preprocessing/refactor_preprocessing.cpp \
       refactor/learn/refactor_symex_learn.cpp \
       refactor/verify/refactor_symex_verify.cpp \
       refactor/facade/refactor_runner.cpp \
       refactor/options/refactoring_type.cpp refactor/options/refactor_program.cpp refactor/value/refactor_solution.cpp \
-      refactor/nullobject/range_collector.cpp \
+      refactor/nullobject/range_collector.cpp refactor/nullobject/nullable_analysis.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 \

src/cegis/Makefile

@@ -30,7 +30,8 @@ goto_programt &get_body(goto_functionst &gf, const std::string &func_name)
   return f.body;
 }
 
-goto_programt &get_body(goto_functionst &gf, const goto_programt::const_targett pos)
+goto_programt &get_body(goto_functionst &gf,
+    const goto_programt::const_targett pos)
 {
   return get_body(gf, id2string(pos->function));
 }
@@ -122,7 +123,8 @@ bool is_nondet(goto_programt::const_targett target,
 
 bool is_return_value_name(const std::string &name)
 {
-  return contains(name, "return_value___") || contains(name, RETURN_VALUE_SUFFIX);
+  return contains(name, "return_value___")
+      || contains(name, RETURN_VALUE_SUFFIX);
 }
 
 const typet &get_affected_type(const goto_programt::instructiont &instr)
@@ -177,23 +179,38 @@ bool is_global_const(const irep_idt &name, const typet &type)
   return std::string::npos == n.find(NS_SEP);
 }
 
-void move_labels(goto_programt &body, const goto_programt::targett &from,
-    const goto_programt::targett &to)
+void move_labels(goto_programt::instructionst &body,
+    const goto_programt::targett &from, const goto_programt::targett &to)
 {
-  for (goto_programt::instructiont &instr : body.instructions)
+  for (goto_programt::instructiont &instr : body)
     for (goto_programt::targett &target : instr.targets)
       if (from == target) target=to;
 }
 
+void move_labels(goto_programt &body, const goto_programt::targett &from,
+    const goto_programt::targett &to)
+{
+  move_labels(body.instructions, from, to);
+}
+
+goto_programt::targett insert_before_preserve_labels(goto_programt &body,
+    const goto_programt::targett &target)
+{
+  const goto_programt::targett result=body.insert_before(target);
+  move_labels(body, target, result);
+  return result;
+}
+
 bool is_builtin(const source_locationt &loc)
 {
   if (loc.is_nil()) return true;
   const std::string &file=id2string(loc.get_file());
   return file.empty() || file.at(0) == '<';
 }
 
-symbolt &create_local_cegis_symbol(symbol_tablet &st, const std::string &full_name,
-    const std::string &base_name, const typet &type)
+symbolt &create_local_cegis_symbol(symbol_tablet &st,
+    const std::string &full_name, const std::string &base_name,
+    const typet &type)
 {
   symbolt new_symbol;
   new_symbol.name=full_name;
@@ -288,11 +305,8 @@ void remove_return(goto_programt &body, const goto_programt::targett pos)
   call.lhs().make_nil();
 }
 
-goto_programt::targett add_return_assignment(
-    goto_programt &body,
-    goto_programt::targett pos,
-    const irep_idt &func_id,
-    const exprt &value)
+goto_programt::targett add_return_assignment(goto_programt &body,
+    goto_programt::targett pos, const irep_idt &func_id, const exprt &value)
 {
   const source_locationt &loc=pos->source_location;
   pos=body.insert_after(pos);

src/cegis/cegis-util/program_helper.cpp

@@ -145,6 +145,19 @@ const irep_idt &get_affected_variable(const goto_programt::instructiont &instr);
  */
 bool is_global_const(const irep_idt &name, const typet &type);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param body
+ * @param from
+ * @param to
+ */
+void move_labels(
+    goto_programt::instructionst &body,
+    const goto_programt::targett &from,
+    const goto_programt::targett &to);
 
 /**
  * @brief
@@ -155,9 +168,25 @@ bool is_global_const(const irep_idt &name, const typet &type);
  * @param from
  * @param to
  */
-void move_labels(goto_programt &body, const goto_programt::targett &from,
+void move_labels(
+    goto_programt &body,
+    const goto_programt::targett &from,
     const goto_programt::targett &to);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param body
+ * @param target
+ *
+ * @return
+ */
+goto_programt::targett insert_before_preserve_labels(
+    goto_programt &body,
+    const goto_programt::targett &target);
+
 /**
  * @brief
  *

src/cegis/cegis-util/program_helper.h

@@ -4,3 +4,16 @@ bool contains(const std::string &haystack, const std::string &needle)
 {
   return std::string::npos != haystack.find(needle);
 }
+
+bool starts_with(const std::string &haystack, const std::string &prefix)
+{
+  return haystack.substr(0, prefix.size()) == prefix;
+}
+
+bool ends_with(const std::string &haystack, const std::string &suffix)
+{
+  const std::string::size_type haystack_sz=haystack.size();
+  const std::string::size_type suffix_sz=suffix.size();
+  if (haystack_sz < suffix_sz) return false;
+  return haystack.substr(haystack_sz - suffix_sz) == suffix;
+}

src/cegis/cegis-util/string_helper.cpp

@@ -24,4 +24,28 @@ Author: Daniel Kroening, [email protected]
  */
 bool contains(const std::string &haystack, const std::string &needle);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param haystack
+ * @param prefix
+ *
+ * @return
+ */
+bool starts_with(const std::string &haystack, const std::string &prefix);
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param haystack
+ * @param suffix
+ *
+ * @return
+ */
+bool ends_with(const std::string &haystack, const std::string &suffix);
+
 #endif /* CEGIS_STRING_HELPER_H_ */

src/cegis/cegis-util/string_helper.h

@@ -19,14 +19,6 @@ void erase_target(goto_programt::instructionst &body,
   body.erase(target);
 }
 
-goto_programt::targett insert_before_preserve_labels(goto_programt &body,
-    const goto_programt::targett &target)
-{
-  const goto_programt::targett result=body.insert_before(target);
-  move_labels(body, target, result);
-  return result;
-}
-
 void restrict_bv_size(invariant_programt &prog, const size_t width_in_bits)
 {
   restrict_bv_size(prog.st, prog.gf, width_in_bits);

src/cegis/invariant/util/invariant_program_helper.cpp

@@ -23,17 +23,6 @@
 void erase_target(goto_programt::instructionst &body,
     const goto_programt::targett &target);
 
-/**
- * @brief
- *
- * @details
- *
- * @param body
- * @param target
- */
-goto_programt::targett insert_before_preserve_labels(goto_programt &body,
-    const goto_programt::targett &target);
-
 /**
  * @brief
  *

src/cegis/invariant/util/invariant_program_helper.h

@@ -0,0 +1,20 @@
+#include <cegis/refactor/options/refactor_program.h>
+
+void create_constraint_function_caller(refactor_programt &prog)
+{
+  // * Create function calling all refactored methods
+}
+
+void link_refactoring_ranges(refactor_programt &prog)
+{
+  // * Goto input/spec range
+  //   * Repeat possibly skipped local declarations
+}
+
+void create_refactoring_constraint(refactor_programt &prog)
+{
+  // * Nondet state vars at beginning of ranges
+  // * Clone state vars
+  // * Replace used variables in input range by clones
+  // * Generate assertion based on used variables
+}

src/cegis/refactor/constraint/constraint_factory.cpp

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

src/cegis/refactor/constraint/constraint_factory.h

@@ -4,29 +4,34 @@ namespace
 {
 class var_findert: public const_expr_visitort
 {
+  std::set<irep_idt> &vars;
 public:
-  std::set<irep_idt> vars;
+  var_findert(std::set<irep_idt> &vars) :
+      vars(vars)
+  {
+  }
 
   virtual ~var_findert()=default;
 
   virtual void operator()(const exprt &expr)
   {
     if (ID_symbol != expr.id()) return;
+    if (ID_code == expr.type().id()) return;
+    // TODO: Follow function calls
     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)
+void collect_state_vars(std::set<irep_idt> &result,
+    goto_programt::const_targett first, const goto_programt::const_targett last)
 {
-  var_findert visitor;
+  var_findert visitor(result);
   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,

src/cegis/refactor/environment/instrument_state_vars.cpp

@@ -19,12 +19,12 @@
  *
  * @details
  *
+ * @param result
  * @param first
  * @param last
- *
- * @return
  */
-std::set<irep_idt> collect_state_vars(
+void collect_state_vars(
+    std::set<irep_idt> &result,
     goto_programt::const_targett first,
     goto_programt::const_targett last);
 

src/cegis/refactor/environment/instrument_state_vars.h

@@ -77,8 +77,7 @@ ordered_instructionst get_instructions_for_types(
   for (const cegis_operand_datat::value_type &typeWithSlots : signature)
   {
     const typet &type=typeWithSlots.first;
-    if (!is_cegis_primitive(type))
-    assert(!"Class type operand generation not supported.");
+    if (!is_cegis_primitive(type)) continue; // TODO: Add support for class types
     const arithmetic_instructionst arith(type);
     insert(result, arith.plus());
     insert(result, arith.minus());

src/cegis/refactor/instructionset/cegis_instruction_factory.cpp

@@ -11,18 +11,13 @@
 #include <cegis/refactor/instructionset/cegis_instruction_factory.h>
 #include <cegis/refactor/instructionset/cegis_processor_body_factory.h>
 
-// XXX: Debug
-#include <iostream>
-// XXX: Debug
-
 #define NUM_PRIMITIVE_OPERANDS 3u
 
 namespace
 {
 size_t cegis_max_operands(const typet &type)
 {
-  if (!is_cegis_primitive(type))
-  assert(!"Class type operand generation not supported.");
+  if (!is_cegis_primitive(type)) return 0;  // TODO: Add support for class types
   return NUM_PRIMITIVE_OPERANDS;
 }
 }
@@ -251,9 +246,7 @@ void remove_skips(goto_programt::instructionst &instrs)
   {
     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;
+    move_labels(instrs, pos, successor);
     pos=instrs.erase(pos);
   }
 }
@@ -273,8 +266,8 @@ void generate_processor_body(symbol_tablet &st, goto_programt &body,
   }
   body.add_instruction(goto_program_instruction_typet::END_FUNCTION);
   //remove_singleton_switch_cases(body);
-  remove_goto_next(body);
-  remove_skips(body.instructions);
+  //remove_goto_next(body);
+  //remove_skips(body.instructions);
   body.compute_loop_numbers();
   body.update();
 }