First working CEGIS null object refactoring.

Author: pkesseli

src/cegis/Makefile

@@ -60,7 +60,7 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       refactor/instructionset/processor_symbols.cpp \
       refactor/constraint/constraint_factory.cpp \
       refactor/preprocessing/refactor_preprocessing.cpp refactor/preprocessing/collect_counterexamples.cpp \
-      refactor/learn/refactor_symex_learn.cpp \
+      refactor/learn/refactor_symex_learn.cpp refactor/learn/instrument_counterexamples.cpp \
       refactor/verify/refactor_symex_verify.cpp \
       refactor/facade/refactor_runner.cpp \
       refactor/options/refactoring_type.cpp refactor/options/refactor_program.cpp \

src/cegis/cegis-util/cbmc_runner.cpp

@@ -14,10 +14,6 @@
 #include <cegis/cegis-util/temporary_output_block.h>
 #include <cegis/cegis-util/cbmc_runner.h>
 
-// XXX: Debug
-#include <iostream>
-// XXX: Debug
-
 #define ARGV_MAX_SIZE 5u
 
 namespace

src/cegis/cegis-util/program_helper.cpp

@@ -235,17 +235,23 @@ symbolt &create_cegis_symbol(symbol_tablet &st, const std::string &full_name,
   return create_local_cegis_symbol(st, full_name, full_name, type);
 }
 
-goto_programt::targett cegis_assign(const symbol_tablet &st,
-    goto_programt &body, const goto_programt::targett &insert_after_pos,
+void cegis_assign(const symbol_tablet &st, goto_programt::instructiont &instr,
     const exprt &lhs, const exprt &rhs, const source_locationt &loc)
 {
-  goto_programt::targett assign=body.insert_after(insert_after_pos);
-  assign->type=goto_program_instruction_typet::ASSIGN;
-  assign->source_location=loc;
+  instr.type=goto_program_instruction_typet::ASSIGN;
+  instr.source_location=loc;
   const namespacet ns(st);
   const typet &type=lhs.type();
-  if (type_eq(type, rhs.type(), ns)) assign->code=code_assignt(lhs, rhs);
-  else assign->code=code_assignt(lhs, typecast_exprt(rhs, type));
+  if (type_eq(type, rhs.type(), ns)) instr.code=code_assignt(lhs, rhs);
+  else instr.code=code_assignt(lhs, typecast_exprt(rhs, type));
+}
+
+goto_programt::targett cegis_assign(const symbol_tablet &st,
+    goto_programt &body, const goto_programt::targett &insert_after_pos,
+    const exprt &lhs, const exprt &rhs, const source_locationt &loc)
+{
+  const goto_programt::targett assign=body.insert_after(insert_after_pos);
+  cegis_assign(st, *assign, lhs, rhs, loc);
   return assign;
 }
 

src/cegis/cegis-util/program_helper.h

@@ -244,6 +244,20 @@ goto_programt::targett cegis_assign(const symbol_tablet &st,
     goto_functionst &gf, const goto_programt::targett &insert_after_pos,
     const exprt &lhs, const exprt &rhs);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param st
+ * @param instr
+ * @param lhs
+ * @param rhs
+ * @param loc
+ */
+void cegis_assign(const symbol_tablet &st, goto_programt::instructiont &instr,
+    const exprt &lhs, const exprt &rhs, const source_locationt &loc);
+
 /**
  * @brief
  *

src/cegis/cegis-util/temporary_output_block.cpp

@@ -4,8 +4,7 @@
 
 temporary_output_blockt::temporary_output_blockt()
 {
-  // XXX: Debug
-  //std::cout.setstate(std::ios_base::failbit);
+  std::cout.setstate(std::ios_base::failbit);
 }
 
 temporary_output_blockt::~temporary_output_blockt()

src/cegis/instrument/literals.h

@@ -24,5 +24,7 @@
 #define CEGIS_FITNESS_TEST_FUNC "__CPROVER_cegis_test_fitness"
 #define CPROVER_INIT CPROVER_PREFIX "initialize"
 #define CONSTRAINT_CALLER_NAME CEGIS_PREFIX "constraint_caller"
+#define CONSTRAINT_CALLER CONSTRAINT_CALLER_NAME ":()V"
+#define CONSTRAINT_CALLER_ID "java::" CONSTRAINT_CALLER
 
 #endif /* CEGIS_LITERALS_H_ */

src/cegis/instrument/meta_variables.cpp

@@ -32,13 +32,19 @@ std::string get_local_meta_name(const std::string &func, const std::string &var)
 
 namespace
 {
+void declare_local_var(goto_programt::instructiont &instr,
+    const symbolt &symbol)
+{
+  instr.type=goto_program_instruction_typet::DECL;
+  instr.code=code_declt(symbol.symbol_expr());
+  instr.source_location=default_cegis_source_location();
+}
+
 goto_programt::targett declare_local_var(goto_programt &body,
     goto_programt::targett pos, const symbolt &symbol)
 {
   pos=body.insert_after(pos);
-  pos->type=goto_program_instruction_typet::DECL;
-  pos->code=code_declt(symbol.symbol_expr());
-  pos->source_location=default_cegis_source_location();
+  declare_local_var(*pos, symbol);
   return pos;
 }
 }
@@ -53,13 +59,19 @@ goto_programt::targett declare_cegis_meta_variable(symbol_tablet &st,
 }
 
 goto_programt::targett declare_local_meta_variable(symbol_tablet &st,
-    const std::string &func_name, goto_programt &body,
-    const goto_programt::targett &insert_after_pos,
-    const std::string &base_name, const typet &type)
+    const std::string &fn, goto_programt &body,
+    const goto_programt::targett &insert_after_pos, const std::string &bn,
+    const typet &t)
 {
-  const std::string symbol_name(get_local_meta_name(func_name, base_name));
-  const symbolt &symbol=create_cegis_symbol(st, symbol_name, type);
-  return declare_local_var(body, insert_after_pos, symbol);
+  const symbolt &smb=create_cegis_symbol(st, get_local_meta_name(fn, bn), t);
+  return declare_local_var(body, insert_after_pos, smb);
+}
+
+void declare_local_meta_variable(symbol_tablet &st, const std::string &fn,
+    goto_programt::instructiont &instr, const std::string &bn, const typet &t)
+{
+  const symbolt &smb=create_cegis_symbol(st, get_local_meta_name(fn, bn), t);
+  declare_local_var(instr, smb);
 }
 
 goto_programt::targett assign_cegis_meta_variable(const symbol_tablet &st,

src/cegis/instrument/meta_variables.h

@@ -69,6 +69,21 @@ goto_programt::targett declare_local_meta_variable(symbol_tablet &st,
     const goto_programt::targett &insert_after_pos,
     const std::string &base_name, const typet &type);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param st
+ * @param func_name
+ * @param instr
+ * @param base_name
+ * @param type
+ */
+void declare_local_meta_variable(symbol_tablet &st,
+    const std::string &func_name, goto_programt::instructiont &instr,
+    const std::string &base_name, const typet &type);
+
 /**
  * @brief
  *

src/cegis/learn/constraint_helper.cpp

@@ -1,9 +1,15 @@
+#include <goto-programs/goto_functions.h>
+
 #include <cegis/cegis-util/program_helper.h>
 
 void transform_asserts_to_assumes(goto_functionst &gf)
 {
-  goto_programt &body=get_entry_body(gf);
-  for (goto_programt::instructiont &instr : body.instructions)
-    if (goto_program_instruction_typet::ASSERT == instr.type)
-      instr.type=goto_program_instruction_typet::ASSUME;
+  typedef goto_functionst::function_mapt fmapt;
+  fmapt &fmap=gf.function_map;
+  for (fmapt::value_type &entry : fmap)
+  {
+    if (!entry.second.body_available()) continue;
+    for (goto_programt::instructiont &instr : entry.second.body.instructions)
+      if (ASSERT == instr.type) instr.type=ASSUME;
+  }
 }

src/cegis/learn/insert_counterexample.cpp

@@ -14,18 +14,12 @@
 #include <cegis/learn/insert_counterexample.h>
 
 #define CE_ARRAY_PREFIX CPROVER_PREFIX "ce_array_"
-#define CE_ARRAY_INDEX CPROVER_PREFIX "ce_array_index"
 #define CE_VALUES_INDEX_PREFIX CPROVER_PREFIX "ce_values_index_"
 
-namespace
-{
-typedef std::map<const irep_idt, exprt> zero_valuest;
-
-zero_valuest get_zero_values(const symbol_tablet &st, const goto_functionst &gf,
+zero_valuest get_zero_values(const symbol_tablet &st,
     const goto_programt::targetst &ce_locs)
 {
   std::map<const irep_idt, exprt> zero_values;
-  const goto_programt::instructionst &body=get_entry_body(gf).instructions;
   const source_locationt loc(default_cegis_source_location());
   const namespacet ns(st);
   null_message_handlert msg;
@@ -39,16 +33,7 @@ zero_valuest get_zero_values(const symbol_tablet &st, const goto_functionst &gf,
   return zero_values;
 }
 
-std::set<irep_idt> get_all_keys(const zero_valuest &zv)
-{
-  std::set<irep_idt> result;
-  std::transform(zv.begin(), zv.end(), std::inserter(result, result.end()),
-      [](const zero_valuest::value_type &v)
-      { return v.first;});
-  return result;
-}
-
-void normalise(const std::set<irep_idt> ce_keys, const zero_valuest &zv,
+void normalise(const std::set<irep_idt> &ce_keys, const zero_valuest &zv,
     labelled_counterexamplest &ces)
 {
   const exprt::operandst no_values;
@@ -89,7 +74,16 @@ void normalise(const std::set<irep_idt> ce_keys, const zero_valuest &zv,
     }
 }
 
-typedef std::map<labelled_assignmentst::key_type, array_exprt> array_valuest;
+namespace
+{
+std::set<irep_idt> get_all_keys(const zero_valuest &zv)
+{
+  std::set<irep_idt> result;
+  std::transform(zv.begin(), zv.end(), std::inserter(result, result.end()),
+      [](const zero_valuest::value_type &v)
+      { return v.first;});
+  return result;
+}
 
 array_exprt to_values(const exprt::operandst &ops)
 {
@@ -101,6 +95,7 @@ array_exprt to_values(const exprt::operandst &ops)
   copy(ops.begin(), ops.end(), std::back_inserter(result.operands()));
   return result;
 }
+}
 
 array_valuest get_array_values(const labelled_counterexamplest &ces)
 {
@@ -123,12 +118,20 @@ array_valuest get_array_values(const labelled_counterexamplest &ces)
   return result;
 }
 
-std::string get_array_name(const irep_idt &loc_id)
+std::string get_ce_array_name(const irep_idt &loc_id)
 {
   std::string base_name(CE_ARRAY_PREFIX);
   return base_name+=id2string(loc_id);
 }
 
+std::string get_ce_value_index_name(const irep_idt &loc)
+{
+  std::string label(CE_VALUES_INDEX_PREFIX);
+  return label+=id2string(loc);
+}
+
+namespace
+{
 void add_array_declarations(symbol_tablet &st, goto_functionst &gf,
     const labelled_counterexamplest &ces, const goto_programt::targett &begin)
 {
@@ -141,25 +144,16 @@ void add_array_declarations(symbol_tablet &st, goto_functionst &gf,
   for (const labelled_counterexamplest::value_type::value_type &value : prototype)
   {
     const labelled_assignmentst::value_type::first_type loc_id=value.first;
-    const typet &org_type=value.second.front().type();
     const array_valuest::const_iterator array_val=array_values.find(loc_id);
     assert(array_values.end() != array_val);
     const array_exprt &array_expr=array_val->second;
-    const typet &array_type=array_expr.type();
-    const typet &element_type=array_type.subtype();
-    const std::string base_name(get_array_name(loc_id));
-    pos=declare_cegis_meta_variable(st, gf, pos, base_name, array_type);
+    const std::string base_name(get_ce_array_name(loc_id));
+    pos=declare_cegis_meta_variable(st, gf, pos, base_name, array_expr.type());
     assert(array_expr.operands().size() == ces.size());
-    pos=assign_cegis_meta_variable(st, gf, pos, base_name, array_val->second);
+    pos=assign_cegis_meta_variable(st, gf, pos, base_name, array_expr);
   }
 }
 
-std::string get_value_index(const irep_idt &loc)
-{
-  std::string label(CE_VALUES_INDEX_PREFIX);
-  return label+=id2string(loc);
-}
-
 void add_array_indexes(const std::set<irep_idt> &ce_keys, symbol_tablet &st,
     goto_functionst &gf)
 {
@@ -176,7 +170,7 @@ void add_array_indexes(const std::set<irep_idt> &ce_keys, symbol_tablet &st,
   pos=cprover_init;
   for (const irep_idt &key : ce_keys)
   {
-    const std::string label(get_value_index(key));
+    const std::string label(get_ce_value_index_name(key));
     pos=declare_cegis_meta_variable(st, gf, pos, label, type);
     pos=assign_cegis_meta_variable(st, gf, pos, label, zero);
   }
@@ -218,10 +212,10 @@ const index_exprt get_array_val_expr(const symbol_tablet &st,
 {
   const std::string index_name(get_cegis_meta_name(CE_ARRAY_INDEX));
   const symbol_exprt index(st.lookup(index_name).symbol_expr());
-  const std::string array_name(get_cegis_meta_name(get_array_name(loc)));
+  const std::string array_name(get_cegis_meta_name(get_ce_array_name(loc)));
   const symbol_exprt array(st.lookup(array_name).symbol_expr());
   const index_exprt ce(array, index);
-  const std::string value_index(get_cegis_meta_name(get_value_index(loc)));
+  const std::string value_index(get_cegis_meta_name(get_ce_value_index_name(loc)));
   const symbol_exprt value_index_expr(st.lookup(value_index).symbol_expr());
   return index_exprt(ce, value_index_expr);
 }
@@ -247,7 +241,7 @@ void assign_ce_values(symbol_tablet &st, goto_functionst &gf,
     default:
       assert(!"Unsupported counterexample location type.");
     }
-    const std::string value_index(get_cegis_meta_name(get_value_index(label)));
+    const std::string value_index(get_cegis_meta_name(get_ce_value_index_name(label)));
     const symbol_exprt value_index_expr(st.lookup(value_index).symbol_expr());
     const plus_exprt inc(increment(value_index_expr));
     cegis_assign(st, gf, pos, value_index_expr, inc);
@@ -259,7 +253,7 @@ void insert_counterexamples(symbol_tablet &st, goto_functionst &gf,
     labelled_counterexamplest ces, const goto_programt::targetst &ce_locs)
 {
   assert(!ces.empty());
-  const zero_valuest zero_values(get_zero_values(st, gf, ce_locs));
+  const zero_valuest zero_values(get_zero_values(st, ce_locs));
   const std::set<irep_idt> ce_keys(get_all_keys(zero_values));
   normalise(ce_keys, zero_values, ces);
   goto_programt &body=get_entry_body(gf);