First full CEGIS control symex synthesis.

Author: Pascal Kesseli

regression/cegis/cegis_control_benchmark_01/example-a_SCHEMA1_IMPL1.c

@@ -1,6 +1,6 @@
 CORE
 example-a_SCHEMA1_IMPL1.c
---gcc --cegis-control --cegis-statistics --cegis-genetic
+--gcc --cegis-control --cegis-statistics --cegis-genetic --cegis-max-size 1
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cegis/cegis_control_benchmark_01/test.desc

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

regression/cegis/cegis_control_benchmark_02/example-a_SCHEMA2_IMPL1.c

@@ -46,11 +46,13 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       jsa/genetic/jsa_source_provider.cpp jsa/genetic/dynamic_jsa_test_runner.cpp jsa/genetic/random_jsa_mutate.cpp \
       jsa/genetic/random_jsa_cross.cpp jsa/genetic/jsa_genetic_convert.cpp jsa/genetic/jsa_random.cpp \
       jsa/genetic/solution_helper.cpp jsa/genetic/jsa_serialiser.cpp jsa/genetic/jsa_paragon_wrapper.cpp \
-      control/facade/control_runner.cpp control/preprocessing/control_preprocessing.cpp \
+      control/facade/control_runner.cpp \
+      control/preprocessing/control_preprocessing.cpp control/preprocessing/propagate_controller_sizes.cpp \
       control/options/control_program.cpp \
       control/learn/control_symex_learn.cpp control/learn/nondet_solution.cpp \
+      control/simplify/remove_unused_elements.cpp \
       control/verify/control_symex_verify.cpp control/verify/insert_solution.cpp \
-      control/value/control_types.cpp \
+      control/value/float_helper.cpp control/value/control_types.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 \

regression/cegis/cegis_control_benchmark_03/example-a_PLANT2_SCHEMA4_IMPL3.c

@@ -1,5 +1,11 @@
+#include <goto-programs/goto_trace.h>
+
+#include <cegis/cegis-util/program_helper.h>
 #include <cegis/learn/constraint_helper.h>
 #include <cegis/learn/insert_counterexample.h>
+#include <cegis/control/value/control_vars.h>
+#include <cegis/control/value/float_helper.h>
+#include <cegis/control/preprocessing/propagate_controller_sizes.h>
 #include <cegis/control/learn/nondet_solution.h>
 #include <cegis/control/learn/control_symex_learn.h>
 
@@ -37,11 +43,50 @@ void control_symex_learnt::set_word_width(const size_t word_width_in_bits) const
 {
 }
 
+namespace
+{
+const struct_exprt &find_solution(const goto_tracet &trace)
+{
+  for (const goto_trace_stept &step : trace.steps)
+  {
+    const exprt &lhs=step.full_lhs;
+    if (ID_symbol != lhs.id()) continue;
+    const std::string &id=id2string(to_symbol_expr(lhs).get_identifier());
+    if (CEGIS_CONTROL_SOLUTION_VAR_NAME != id) continue;
+    return to_struct_expr(step.full_lhs_value);
+  }
+  assert(!"Control solution not found in trace.");
+}
+
+const array_exprt &get_a(const namespacet &ns, const struct_exprt &solution)
+{
+  return to_array_expr(
+      get_controller_comp(ns, solution, CEGIS_CONTROL_A_MEMBER_NAME));
+}
+
+const array_exprt &get_b(const namespacet &ns, const struct_exprt &solution)
+{
+  return to_array_expr(
+      get_controller_comp(ns, solution, CEGIS_CONTROL_B_MEMBER_NAME));
+}
+
+void extract(std::vector<double> &data, const array_exprt &array)
+{
+  const exprt::operandst &ops=array.operands();
+  const size_t size=ops.size();
+  data.resize(size);
+  for (size_t i=0; i < size; ++i)
+    data[i]=to_control_float(to_constant_expr(ops[i]));
+}
+}
+
 void control_symex_learnt::convert(candidatet &current_candidate,
     const goto_tracet &trace, const size_t max_solution_size) const
 {
-  // TODO: Implement
-  assert(false);
+  const struct_exprt &solution=find_solution(trace);
+  const namespacet ns(current_program.st);
+  extract(current_candidate.a, get_a(ns, solution));
+  extract(current_candidate.b, get_b(ns, solution));
 }
 
 namespace

regression/cegis/cegis_control_benchmark_03/test.desc

@@ -1,110 +1,19 @@
-#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);
-  }
-}
-}
+#include <cegis/control/value/control_vars.h>
+#include <cegis/control/preprocessing/propagate_controller_sizes.h>
 
 void nondet_control_solution(const symbol_tablet &st, goto_functionst &gf)
 {
   const std::string name(CEGIS_CONTROL_SOLUTION_VAR_NAME);
   const symbolt &symbol=st.lookup(name);
-  replace_controller_sizes(st, gf);
+  propagate_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);
-  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);
+  const goto_programt::targett pos(find_cprover_initialize(body));
+  cegis_assign_user_variable(st, gf, std::prev(pos), name, value);
+  goto_programt &init=get_body(gf, CPROVER_INIT);
+  remove_solution_assignment(init);
 }

src/cegis/Makefile

@@ -2,6 +2,8 @@
 #include <cegis/cegis-util/inline_user_program.h>
 #include <cegis/cegis-util/counterexample_vars.h>
 #include <cegis/cegis-util/program_helper.h>
+#include <cegis/control/value/control_vars.h>
+#include <cegis/control/simplify/remove_unused_elements.h>
 #include <cegis/control/preprocessing/control_preprocessing.h>
 
 control_preprocessingt::control_preprocessingt(const symbol_tablet &st,
@@ -12,7 +14,7 @@ control_preprocessingt::control_preprocessingt(const symbol_tablet &st,
 
 namespace
 {
-const char * const excluded_functions[]= {
+const char * const excluded_functions[]={
     "verify_stability_closedloop_using_dslib", "check_stability_closedloop",
     "fxp_double_to_fxp", "fxp_to_double", "ft_closedloop_series", "poly_mult",
     "poly_sum", "internal_pow" };
@@ -24,14 +26,20 @@ bool is_meta(const goto_programt::const_targett pos)
   const std::string &func=id2string(loc.get_function());
   for (const char * const excluded : excluded_functions)
     if (contains(func, excluded)) return true;
-  return false;
+  if (goto_program_instruction_typet::ASSIGN != pos->type) return false;
+  const exprt &lhs=to_code_assign(pos->code).lhs();
+  if (ID_symbol != lhs.id()) return false;
+  const std::string &var=id2string(to_symbol_expr(lhs).get_identifier());
+  return CEGIS_CONTROL_SOLUTION_VAR_NAME == var;
 }
 }
 
 void control_preprocessingt::operator ()()
 {
+  symbol_tablet &st=control_program.st;
   goto_functionst &gf=control_program.gf;
-  inline_user_program(control_program.st, gf);
+  remove_unused_elements(st, gf);
+  inline_user_program(st, gf);
   goto_programt::targetst &locs=control_program.counterexample_locations;
   goto_programt &body=get_entry_body(gf);
   collect_counterexample_locations(locs, body, is_meta);

src/cegis/control/learn/control_symex_learn.cpp

@@ -0,0 +1,104 @@
+#include <deque>
+#include <algorithm>
+
+#include <goto-programs/goto_functions.h>
+
+#include <cegis/cegis-util/program_helper.h>
+#include <cegis/control/value/control_vars.h>
+
+const exprt &get_controller_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.");
+}
+
+namespace
+{
+const exprt &get_a_size(const namespacet &ns, const struct_exprt &value)
+{
+  return get_controller_comp(ns, value, CEGIS_CONTROL_A_SIZE_MEMBER_NAME);
+}
+
+const exprt &get_b_size(const namespacet &ns, const struct_exprt &value)
+{
+  return get_controller_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 propagate_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);
+  }
+}
+
+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;
+}
+}
+
+goto_programt::targett get_solution_assignment(goto_programt &body)
+{
+  goto_programt::instructionst &i=body.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);
+  return pos;
+}
+
+void remove_solution_assignment(goto_programt &body)
+{
+  body.instructions.erase(get_solution_assignment(body));
+}