merge line terminators

Author: Peter Schrammel

regression/cegis/cegis_control_benchmark_02/example-a_SCHEMA2_IMPL1.c

@@ -0,0 +1,7 @@
+CORE
+example-a_SCHEMA2_IMPL1.c
+--gcc --cegis-control --cegis-statistics --cegis-genetic --cegis-max-size 1
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cegis/cegis_control_benchmark_02/test.desc

@@ -60,6 +60,8 @@ 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 \
+      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 \
       instrument/find_cprover_initialize.cpp \

src/cegis/Makefile

@@ -100,3 +100,28 @@ void show_assignments(std::ostream &os,
     os << "</assignment>" << std::endl;
   }
 }
+
+namespace
+{
+bool is_marker(const irep_idt &label)
+{
+  return std::string::npos != id2string(label).find(DEFAULT_MARKER_LABEL_PREFIX);
+}
+
+typedef goto_programt::instructiont::labelst labelst;
+}
+
+bool has_counterexample_marker(const goto_programt::const_targett pos)
+{
+  const labelst &l=pos->labels;
+  return l.end() != std::find_if(l.begin(), l.end(), is_marker);
+}
+
+const irep_idt &get_counterexample_marker(
+    const goto_programt::const_targett pos)
+{
+  const labelst &l=pos->labels;
+  const labelst::const_iterator it=std::find_if(l.begin(), l.end(), is_marker);
+  assert(l.end() != it);
+  return *it;
+}

src/cegis/cegis-util/counterexample_vars.cpp

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_program.h>
 
+#include <cegis/cegis-util/labelled_assignments.h>
+
 #define DEFAULT_MARKER_LABEL_PREFIX CPROVER_PREFIX "_cegis_ce_location_"
 
 /**
@@ -93,8 +95,7 @@ bool default_cegis_meta_criterion(const goto_programt::const_targett pos);
  *
  * @return
  */
-std::map<const irep_idt, exprt::operandst> extract_counterexample(
-    const class goto_tracet &trace);
+labelled_assignmentst extract_counterexample(const class goto_tracet &trace);
 
 /**
  * @brief
@@ -104,6 +105,28 @@ std::map<const irep_idt, exprt::operandst> extract_counterexample(
  * @param assignments
  */
 void show_assignments(std::ostream &os,
-    const std::map<const irep_idt, exprt::operandst> &assignments);
+    const labelled_assignmentst &assignments);
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param pos
+ *
+ * @return
+ */
+bool has_counterexample_marker(goto_programt::const_targett pos);
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param pos
+ *
+ * @return
+ */
+const irep_idt &get_counterexample_marker(goto_programt::const_targett pos);
 
 #endif /* CEGIS_COUNTEREXAMPLE_VARS_H_ */

src/cegis/cegis-util/counterexample_vars.h

@@ -0,0 +1,31 @@
+/*******************************************************************
+
+Module: Counterexample-Guided Inductive Synthesis
+
+Author: Daniel Kroening, [email protected]
+        Pascal Kesseli, [email protected]
+
+\*******************************************************************/
+
+#ifndef CEGIS_UTIL_LABELLED_ASSIGNMENTS_H_
+#define CEGIS_UTIL_LABELLED_ASSIGNMENTS_H_
+
+#include <deque>
+
+#include <util/expr.h>
+
+/**
+ * @brief
+ *
+ * @details
+ */
+typedef std::map<const irep_idt, exprt::operandst> labelled_assignmentst;
+
+/**
+ * @brief
+ *
+ * @details
+ */
+typedef std::deque<labelled_assignmentst> labelled_counterexamplest;
+
+#endif /* CEGIS_UTIL_LABELLED_ASSIGNMENTS_H_ */

src/cegis/cegis-util/labelled_assignments.h

@@ -11,24 +11,12 @@
 
 goto_programt &get_entry_body(goto_functionst &gf)
 {
-  const irep_idt id(goto_functionst::entry_point());
-  goto_functionst::function_mapt &function_map=gf.function_map;
-  const goto_functionst::function_mapt::iterator it=function_map.find(id);
-  assert(function_map.end() != it && "Danger program function missing.");
-  goto_function_templatet<goto_programt> &f=it->second;
-  assert(f.body_available() && "Danger program function body missing.");
-  return f.body;
+  return get_body(gf, id2string(goto_functionst::entry_point()));
 }
 
 const goto_programt &get_entry_body(const goto_functionst &gf)
 {
-  const irep_idt id(goto_functionst::entry_point());
-  const goto_functionst::function_mapt &function_map=gf.function_map;
-  const goto_functionst::function_mapt::const_iterator it=function_map.find(id);
-  assert(function_map.end() != it && "Danger program function missing.");
-  const goto_function_templatet<goto_programt> &f=it->second;
-  assert(f.body_available() && "Danger program function body missing.");
-  return f.body;
+  return get_body(gf, id2string(goto_functionst::entry_point()));
 }
 
 class goto_programt &get_body(

src/cegis/cegis-util/program_helper.cpp

@@ -0,0 +1,15 @@
+#include <util/std_types.h>
+#include <util/symbol_table.h>
+
+#define TAG_PREFIX "tag-"
+
+const typet &replace_struct_by_symbol_type(const symbol_tablet &st,
+    const typet &type)
+{
+  const irep_idt &type_id=type.id();
+  if (ID_struct != type_id && ID_incomplete_struct != type_id
+      && ID_union != type_id && ID_incomplete_union != type_id) return type;
+  std::string tag(TAG_PREFIX);
+  tag+=id2string(to_struct_union_type(type).get_tag());
+  return st.lookup(tag).type;
+}

src/cegis/cegis-util/type_helper.cpp

@@ -0,0 +1,25 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, [email protected]
+         Pascal Kesseli, [email protected]
+
+ \*******************************************************************/
+
+#ifndef CEGIS_UTIL_TYPE_HELPER_H_
+#define CEGIS_UTIL_TYPE_HELPER_H_
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param st
+ * @param type
+ */
+const class typet &replace_struct_by_symbol_type(
+    const class symbol_tablet &st,
+    const typet &type);
+
+#endif /* CEGIS_UTIL_TYPE_HELPER_H_ */

src/cegis/cegis-util/type_helper.h

@@ -1,3 +1,5 @@
+#include <cegis/learn/constraint_helper.h>
+#include <cegis/learn/insert_counterexample.h>
 #include <cegis/control/learn/nondet_solution.h>
 #include <cegis/control/learn/control_symex_learn.h>
 
@@ -11,11 +13,14 @@ void control_symex_learnt::process(const counterexamplest &counterexamples,
     const size_t max_solution_size)
 {
   current_program=original_program;
-  const symbol_tablet &st=current_program.st;
+  symbol_tablet &st=current_program.st;
   goto_functionst &gf=current_program.gf;
   nondet_control_solution(st, gf);
-  // TODO: Implement
-  assert(false);
+  transform_asserts_to_assumes(gf);
+  const goto_programt::targetst &ce_locs=
+      current_program.counterexample_locations;
+  insert_counterexamples(st, gf, counterexamples, ce_locs);
+  gf.update();
 }
 
 const symbol_tablet &control_symex_learnt::get_symbol_table() const

src/cegis/control/learn/control_symex_learn.cpp

@@ -1,15 +1,110 @@
+#include <deque>
+#include <algorithm>
+
 #include <cegis/control/value/control_vars.h>
 #include <cegis/cegis-util/program_helper.h>
+#include <cegis/instrument/literals.h>
 #include <cegis/instrument/find_cprover_initialize.h>
 #include <cegis/control/learn/nondet_solution.h>
 
+namespace
+{
+bool is_sol_assign(const goto_programt::instructiont &instr)
+{
+  if (goto_program_instruction_typet::ASSIGN != instr.type) return false;
+  const std::string &var=id2string(get_affected_variable(instr));
+  return CEGIS_CONTROL_SOLUTION_VAR_NAME == var;
+}
+
+void remove_solution_assignment_from_cprover_init(goto_functionst &gf)
+{
+  goto_programt::instructionst &i=get_body(gf, CPROVER_INIT).instructions;
+  const goto_programt::targett end(i.end());
+  const goto_programt::targett pos=std::find_if(i.begin(), end, is_sol_assign);
+  assert(end != pos);
+  i.erase(pos);
+}
+
+const exprt &get_comp(const namespacet &ns, const struct_exprt &value,
+    const char * const comp)
+{
+  const struct_typet &type=to_struct_type(ns.follow(value.type()));
+  const struct_typet::componentst &comps=type.components();
+  for (size_t i=0; i < comps.size(); ++i)
+    if (id2string(comps[i].get_name()) == comp) return value.operands()[i];
+  assert(!"Solution component not found.");
+}
+
+const exprt &get_a_size(const namespacet &ns, const struct_exprt &value)
+{
+  return get_comp(ns, value, CEGIS_CONTROL_A_SIZE_MEMBER_NAME);
+}
+
+const exprt &get_b_size(const namespacet &ns, const struct_exprt &value)
+{
+  return get_comp(ns, value, CEGIS_CONTROL_B_SIZE_MEMBER_NAME);
+}
+
+class replace_sizes_visitort: public expr_visitort
+{
+  std::deque<exprt *> a_sizes, b_sizes;
+  const exprt &a_size;
+  const exprt &b_size;
+public:
+  replace_sizes_visitort(const exprt &a_size, const exprt &b_size) :
+      a_size(a_size), b_size(b_size)
+  {
+  }
+
+  virtual ~replace_sizes_visitort()
+  {
+    for (exprt * const expr : a_sizes)
+      *expr=a_size;
+    for (exprt * const expr : b_sizes)
+      *expr=b_size;
+  }
+
+  virtual void operator()(exprt &expr)
+  {
+    if (ID_member != expr.id()) return;
+    const member_exprt &member=to_member_expr(expr);
+    const exprt &struct_op=member.struct_op();
+    if (ID_symbol != struct_op.id()) return;
+    const symbol_exprt &symbol=to_symbol_expr(struct_op);
+    const std::string &var=id2string(symbol.get_identifier());
+    if (CEGIS_CONTROL_SOLUTION_VAR_NAME != var) return;
+    const std::string &comp=id2string(member.get_component_name());
+    if (CEGIS_CONTROL_A_SIZE_MEMBER_NAME == comp) a_sizes.push_back(&expr);
+    else if (CEGIS_CONTROL_B_SIZE_MEMBER_NAME == comp) b_sizes.push_back(&expr);
+  }
+};
+
+void replace_controller_sizes(const symbol_tablet &st, goto_functionst &gf)
+{
+  const symbolt &symbol=st.lookup(CEGIS_CONTROL_SOLUTION_VAR_NAME);
+  const struct_exprt &controller_value=to_struct_expr(symbol.value);
+  const namespacet ns(st);
+  const exprt &a_size=get_a_size(ns, controller_value);
+  const exprt &b_size=get_b_size(ns, controller_value);
+  replace_sizes_visitort visitor(a_size, b_size);
+  goto_programt &body=get_entry_body(gf);
+  for (goto_programt::instructiont &instr : body.instructions)
+  {
+    instr.code.visit(visitor);
+    instr.guard.visit(visitor);
+  }
+}
+}
+
 void nondet_control_solution(const symbol_tablet &st, goto_functionst &gf)
 {
-  const irep_idt name(CEGIS_CONTROL_SOLUTION_VAR_NAME);
+  const std::string name(CEGIS_CONTROL_SOLUTION_VAR_NAME);
   const symbolt &symbol=st.lookup(name);
+  replace_controller_sizes(st, gf);
   const side_effect_expr_nondett value(symbol.type);
   const symbol_exprt solution_var(symbol.symbol_expr());
   goto_programt &body=get_entry_body(gf);
-  const goto_programt::targett pos(find_cprover_initialize(body));
-  cegis_assign_user_variable(st, gf, pos, name, value);
+  goto_programt::targett pos(find_cprover_initialize(body));
+  pos=cegis_assign_user_variable(st, gf, std::prev(pos), name, value);
+  remove_solution_assignment_from_cprover_init(gf);
 }

src/cegis/control/learn/nondet_solution.cpp

@@ -13,5 +13,6 @@
 #define CEGIS_CONTROL_SOLUTION_VAR_NAME "controller"
 #define CEGIS_CONTROL_A_MEMBER_NAME "a"
 #define CEGIS_CONTROL_A_SIZE_MEMBER_NAME "a_size"
+#define CEGIS_CONTROL_B_SIZE_MEMBER_NAME "b_size"
 
 #endif /* CEGIS_CONTROL_VARS_H_ */

src/cegis/control/value/control_vars.h

@@ -12,6 +12,7 @@ void control_symex_verifyt::process(const candidatet &candidate)
 {
   current_program=original_program;
   insert_solution(current_program, candidate);
+  current_program.gf.update();
 }
 
 const symbol_tablet &control_symex_verifyt::get_symbol_table() const

src/cegis/control/verify/control_symex_verify.cpp

@@ -69,7 +69,7 @@ void insert_solution(control_programt &program,
   goto_functionst &gf=program.gf;
   goto_programt &body=get_entry_body(gf);
   const goto_programt::targett pos=find_cprover_initialize(body);
-  const irep_idt name(CEGIS_CONTROL_SOLUTION_VAR_NAME);
+  const std::string name(CEGIS_CONTROL_SOLUTION_VAR_NAME);
   const symbol_tablet &st=program.st;
   const source_locationt &loc=pos->source_location;
   const struct_exprt value(to_struct_expr(st, solution, loc));

src/cegis/control/verify/insert_solution.cpp

@@ -19,3 +19,10 @@ goto_programt::targett find_cprover_initialize(goto_programt &body)
   assert(end != pos);
   return pos;
 }
+
+goto_programt::targett find_last_instr(goto_programt &body)
+{
+  goto_programt::targett result=body.instructions.end();
+  assert(goto_program_instruction_typet::END_FUNCTION == (--result)->type);
+  return --result;
+}

src/cegis/instrument/find_cprover_initialize.cpp

@@ -23,4 +23,15 @@
  */
 goto_programt::targett find_cprover_initialize(goto_programt &body);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param body
+ *
+ * @return
+ */
+goto_programt::targett find_last_instr(goto_programt &body);
+
 #endif /* CEGIS_FIND_CPROVER_INITIALIZE_H_ */