CEGIS refactor preprocessing & CE extraction.

Author: pkesseli

src/cegis/Makefile

@@ -59,11 +59,11 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       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/preprocessing/refactor_preprocessing.cpp refactor/preprocessing/collect_counterexamples.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/options/refactoring_type.cpp refactor/options/refactor_program.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 \

src/cegis/cegis-util/cbmc_runner.cpp

@@ -1,3 +1,5 @@
+#include <algorithm>
+
 #include <util/config.h>
 #include <util/substitute.h>
 
@@ -11,6 +13,12 @@
 #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
 {
 bool exists(const std::string &name)
@@ -33,14 +41,48 @@ std::string get_next_goto_file_name()
   return get_goto_file_name(index);
 }
 
-const char * ARGV[]= { "cbmc", "--stop-on-fail" };
-const char * GCC_ARGV[]= { "cbmc", "--stop-on-fail", "-gcc" };
+bool is_gcc()
+{
+  return configt::ansi_ct::flavourt::GCC == config.ansi_c.mode;
+}
+
+std::vector<std::string> get_args()
+{
+  std::vector<std::string> result= { "cbmc", "--stop-on-fail" };
+  if (is_gcc()) result.push_back("--gcc");
+  return result;
+}
+
+std::vector<const char *> get_argv(const std::vector<std::string> &args)
+{
+  std::vector<const char *> result;
+  std::transform(args.begin(), args.end(), std::back_inserter(result),
+      std::mem_fun_ref(std::string::c_str));
+  return result;
+}
+
+class args_providert
+{
+  const std::vector<std::string> args;
+  std::vector<const char *> arg_ref;
+public:
+  args_providert() :
+      args(get_args()), arg_ref(get_argv(args))
+  {
+  }
 
-bool is_gcc() { return configt::ansi_ct::flavourt::GCC == config.ansi_c.mode; }
-int get_argc() { return is_gcc() ? 3 : 2; }
-const char ** get_argv() { return is_gcc() ? GCC_ARGV : ARGV; }
+  int argc()
+  {
+    return arg_ref.size();
+  }
+
+  const char * *argv()
+  {
+    return arg_ref.data();
+  }
+};
 
-class cbmc_runnert: public cbmc_parse_optionst
+class cbmc_runnert: public args_providert, public cbmc_parse_optionst
 {
   const symbol_tablet &st;
   const goto_functionst &gf;
@@ -49,30 +91,24 @@ class cbmc_runnert: public cbmc_parse_optionst
   const bool keep_goto_programs;
 
 public:
-  cbmc_runnert(
-    const symbol_tablet &st,
-    const goto_functionst &gf,
-    cbmc_resultt &result,
-    const bool keep_goto_programs) :
-    cbmc_parse_optionst(get_argc(), get_argv()), st(st), gf(gf), result(
-          result), bmc_result(safety_checkert::UNSAFE), keep_goto_programs(
-          keep_goto_programs)
+  cbmc_runnert(const symbol_tablet &st, const goto_functionst &gf,
+      cbmc_resultt &result, const bool keep_goto_programs) :
+      cbmc_parse_optionst(argc(), argv()), st(st), gf(gf), result(result), bmc_result(
+          safety_checkert::UNSAFE), keep_goto_programs(keep_goto_programs)
   {
   }
 
   virtual ~cbmc_runnert()=default;
 
-  virtual int get_goto_program(
-    const optionst &options,
-    bmct &bmc,
-    goto_functionst &goto_functions)
+  virtual int get_goto_program(const optionst &options, bmct &bmc,
+      goto_functionst &goto_functions)
   {
     symbol_table.clear();
     symbol_table=st;
     goto_functions.clear();
     goto_functions.copy_from(gf);
-    if(process_goto_program(options, goto_functions)) return 6;
-    if(keep_goto_programs)
+    if (process_goto_program(options, goto_functions)) return 6;
+    if (keep_goto_programs)
     {
       const std::string path(get_next_goto_file_name());
       message_handlert &msg=get_message_handler();
@@ -101,11 +137,9 @@ class cbmc_runnert: public cbmc_parse_optionst
 };
 }
 
-safety_checkert::resultt run_cbmc(
-  const symbol_tablet &st,
-  const goto_functionst &gf,
-  cbmc_resultt &cbmc_result,
-  const bool keep_goto_programs)
+safety_checkert::resultt run_cbmc(const symbol_tablet &st,
+    const goto_functionst &gf, cbmc_resultt &cbmc_result,
+    const bool keep_goto_programs)
 {
   const temporary_output_blockt disable_output;
   cbmc_runnert runner(st, gf, cbmc_result, keep_goto_programs);
@@ -116,11 +150,9 @@ safety_checkert::resultt run_cbmc(
   return runner.get_bmc_result();
 }
 
-safety_checkert::resultt run_cbmc(
-  const symbol_tablet &st,
-  const goto_functionst &gf,
-  cbmc_resultt &cbmc_result,
-  const optionst &o)
+safety_checkert::resultt run_cbmc(const symbol_tablet &st,
+    const goto_functionst &gf, cbmc_resultt &cbmc_result, const optionst &o)
 {
-  return run_cbmc(st, gf, cbmc_result, o.get_bool_option(CEGIS_KEEP_GOTO_PROGRAMS));
+  return run_cbmc(st, gf, cbmc_result,
+      o.get_bool_option(CEGIS_KEEP_GOTO_PROGRAMS));
 }

src/cegis/cegis-util/cbmc_runner.h

@@ -61,6 +61,6 @@ safety_checkert::resultt run_cbmc(
     const class symbol_tablet &st,
     const class goto_functionst &gf,
     cbmc_resultt &result,
-    const optionst &options);
+    const class optionst &options);
 
 #endif /* CEGIS_UTIL_CBMC_RUNNER_H_ */

src/cegis/cegis-util/counterexample_vars.cpp

@@ -8,20 +8,31 @@
 #include <cegis/cegis-util/program_helper.h>
 #include <cegis/cegis-util/counterexample_vars.h>
 
-void collect_counterexample_locations(goto_programt::targetst &locs,
+namespace
+{
+size_t collect_counterexample_locations(goto_programt::targetst &locs,
     const char * const marker_prefix, goto_programt &prog,
-    const std::function<bool(goto_programt::const_targett target)> is_meta)
+    const std::function<bool(goto_programt::const_targett target)> is_meta,
+    size_t marker_index)
 {
   goto_programt::instructionst &body=prog.instructions;
   const goto_programt::targett end(body.end());
-  size_t marker_index=0;
   for (goto_programt::targett instr=body.begin(); instr != end; ++instr)
     if (is_nondet(instr, end) && !is_meta(instr))
     {
       assert(instr->labels.empty());
       instr->labels.push_back(marker_prefix + std::to_string(marker_index++));
       locs.push_back(instr);
     }
+  return marker_index;
+}
+}
+
+void collect_counterexample_locations(goto_programt::targetst &locs,
+    const char * const marker_prefix, goto_programt &prog,
+    const std::function<bool(goto_programt::const_targett target)> is_meta)
+{
+  collect_counterexample_locations(locs, marker_prefix, prog, is_meta, 0);
 }
 
 #define TMP_IF_EXPR_PREFIX "tmp_if_expr$"
@@ -58,6 +69,15 @@ void collect_counterexample_locations(goto_programt::targetst &locs,
       is_meta);
 }
 
+size_t collect_counterexample_locations(goto_programt::targetst &locs,
+    goto_programt &prog,
+    const std::function<bool(goto_programt::const_targett target)> is_meta,
+    const size_t marker_index_offset)
+{
+  return collect_counterexample_locations(locs, DEFAULT_MARKER_LABEL_PREFIX,
+      prog, is_meta, marker_index_offset);
+}
+
 namespace
 {
 goto_programt::instructiont::labelst::const_iterator find_ce_label(

src/cegis/cegis-util/counterexample_vars.h

@@ -75,6 +75,24 @@ void collect_counterexample_locations(
     goto_programt &prog,
     const std::function<bool(goto_programt::const_targett target)> is_meta);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param locs
+ * @param prog
+ * @param is_meta
+ * @param marker_index_offset
+ *
+ * @return
+ */
+size_t collect_counterexample_locations(
+    goto_programt::targetst &locs,
+    goto_programt &prog,
+    const std::function<bool(goto_programt::const_targett target)> is_meta,
+    size_t marker_index_offset);
+
 /**
  * @brief
  *

src/cegis/cegis-util/program_helper.cpp

@@ -1,4 +1,5 @@
 #include <algorithm>
+#include <functional>
 
 #include <util/type_eq.h>
 #include <goto-programs/goto_functions.h>
@@ -315,3 +316,32 @@ goto_programt::targett add_return_assignment(goto_programt &body,
   pos->code=code_assignt(get_ret_val_var(func_id, value.type()), value);
   return pos;
 }
+
+namespace
+{
+goto_programt::targett insert_preserving_source_location(
+    goto_programt::targett pos,
+    const std::function<goto_programt::targett(goto_programt::targett)> &inserter)
+{
+  const source_locationt &loc=pos->source_location;
+  const irep_idt &func_name=pos->function;
+  pos=inserter(pos);
+  pos->source_location=loc;
+  pos->function=func_name;
+  return pos;
+}
+}
+
+goto_programt::targett insert_after_preserving_source_location(
+    goto_programt &body, goto_programt::targett pos)
+{
+  const auto op=std::bind1st(std::mem_fun(goto_programt::insert_after), &body);
+  return insert_preserving_source_location(pos, op);
+}
+
+goto_programt::targett insert_before_preserving_source_location(
+    goto_programt &body, goto_programt::targett pos)
+{
+  const auto op=std::bind1st(std::mem_fun(goto_programt::insert_before), &body);
+  return insert_preserving_source_location(pos, op);
+}

src/cegis/cegis-util/program_helper.h

@@ -346,4 +346,32 @@ goto_programt::targett add_return_assignment(
     const irep_idt &func_id,
     const exprt &value);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param body
+ * @param pos
+ *
+ * @return
+ */
+goto_programt::targett insert_after_preserving_source_location(
+    goto_programt &body,
+    goto_programt::targett pos);
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param body
+ * @param pos
+ *
+ * @return
+ */
+goto_programt::targett insert_before_preserving_source_location(
+    goto_programt &body,
+    goto_programt::targett pos);
+
 #endif /* CEGIS_PROGRAM_HELPER_H_ */

src/cegis/cegis-util/temporary_output_block.cpp

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

src/cegis/instrument/literals.h

@@ -23,5 +23,6 @@
 #define CEGIS_CONSTANT_PREFIX "CEGIS_CONSTANT_"
 #define CEGIS_FITNESS_TEST_FUNC "__CPROVER_cegis_test_fitness"
 #define CPROVER_INIT CPROVER_PREFIX "initialize"
+#define CONSTRAINT_CALLER_NAME CEGIS_PREFIX "constraint_caller"
 
 #endif /* CEGIS_LITERALS_H_ */

src/cegis/learn/insert_counterexample.cpp

@@ -189,8 +189,7 @@ plus_exprt increment(const symbol_exprt &symbol)
   return plus_exprt(symbol, one);
 }
 
-void add_ce_goto(symbol_tablet &st, goto_functionst &gf,
-    const std::set<irep_idt> &ce_keys, const size_t num_ces,
+void add_ce_goto(symbol_tablet &st, goto_functionst &gf, const size_t num_ces,
     const goto_programt::targett &begin)
 {
   goto_programt &body=get_entry_body(gf);
@@ -267,6 +266,6 @@ void insert_counterexamples(symbol_tablet &st, goto_functionst &gf,
   const goto_programt::targett begin(find_cprover_initialize(body));
   add_array_declarations(st, gf, ces, begin);
   add_array_indexes(ce_keys, st, gf);
-  add_ce_goto(st, gf, ce_keys, ces.size(), begin);
+  add_ce_goto(st, gf, ces.size(), begin);
   assign_ce_values(st, gf, ce_locs);
 }