Fixed CEGIS control benchmark 2

Interface for control benchmark 2 changed. Adapted front-end to new input
format.

Author: pkesseli

regression/cegis/cegis_control_benchmark_02/eigen_charpoly.c

@@ -48,6 +48,8 @@ const digital_system_state_space _controller=
     .nOutputs = NOUTPUTS
 };
 
+extern __CPROVER_EIGEN_fixedbvt K_fxp[4][4];
+
 
 //typedef int __CPROVER_EIGEN_fixedbvt;
 #define __CPROVER_EIGEN_MATRIX_SIZE 3u
@@ -164,9 +166,9 @@ void __CPROVER_EIGEN_charpoly(void) {
 }
 
 /*void init(void) {
-  _controller.K[0][0] = nondet_double();
-  _controller.K[0][1] = nondet_double();
-  _controller.K[0][2] = nondet_double();
+  K_fxp[0][0] = nondet_double();
+  K_fxp[0][1] = nondet_double();
+  K_fxp[0][2] = nondet_double();
 }*/
 
 __CPROVER_EIGEN_fixedbvt __CPROVER_EIGEN_matrix_multiplication_result[4][4];
@@ -197,7 +199,7 @@ void double_matrix_multiplication(void/* unsigned int i1, unsigned int j1, unsig
   //unsigned int __mm_j2;
 #define __mm_m1 _controller.B
   //__CPROVER_EIGEN_fixedbvt __mm_m1[4][4];
-#define __mm_m2 _controller.K
+#define __mm_m2 K_fxp
   //__CPROVER_EIGEN_fixedbvt __mm_m2[4][4];
 #define __mm_m3 __CPROVER_EIGEN_matrix_multiplication_result
   //__CPROVER_EIGEN_fixedbvt __mm_m3[4][4];
@@ -248,7 +250,7 @@ void closed_loop(void)
     NINPUTS,
     NSTATES,
     _controller.B,
-    _controller.K,
+    K_fxp,
     result1);*/
   double_matrix_multiplication();
 
@@ -271,7 +273,7 @@ void closed_loop(void)
     _controller.nInputs,
     _controller.nStates,
     _controller.D,
-    _controller.K,
+    K_fxp,
     result1);
 
   double_sub_matrix(
@@ -288,9 +290,9 @@ int main(void) {
   __CPROVER_EIGEN_charpoly();
   //__CPROVER_assert(check_stability(), "");
   __CPROVER_assume(check_stability() == 0);
-  __CPROVER_EIGEN_fixedbvt __trace_K0 = _controller.K[0][0];
-  __CPROVER_EIGEN_fixedbvt __trace_K1 = _controller.K[0][1];
-  __CPROVER_EIGEN_fixedbvt __trace_K2 = _controller.K[0][2];
+  __CPROVER_EIGEN_fixedbvt __trace_K0 = K_fxp[0][0];
+  __CPROVER_EIGEN_fixedbvt __trace_K1 = K_fxp[0][1];
+  __CPROVER_EIGEN_fixedbvt __trace_K2 = K_fxp[0][2];
   __CPROVER_EIGEN_fixedbvt counterexample_var;
   __CPROVER_assume(0.0 <= counterexample_var && counterexample_var <= 10.0);
   __CPROVER_assert(__trace_K0 > counterexample_var, "");

regression/cegis/cegis_control_benchmark_03/safety_stability.c

@@ -231,7 +231,7 @@ void closed_loop(void)
 
 void inputs_equal_ref_minus_k_times_states(void)
   {
-    __controller_typet states_fxp[NSTATES];
+    __controller_typet states_fxp[NSTATES] = { 0.0 };
     //single input
     __controller_typet result_fxp=zero_type;
 
@@ -453,7 +453,7 @@ int safety_stability(void) {
 #endif
 
 #ifdef CPROVER
-  __controller_typet K_fxp_trace[NSTATES];
+  __controller_typet K_fxp_trace[NSTATES] = { 0.0 };
   __CPROVER_array_copy(K_fxp_trace, K_fxp);
   __CPROVER_assert(0 == 1, "");
 #endif

src/cegis/control/facade/control_runner.cpp

@@ -15,10 +15,6 @@
 #include <cegis/control/verify/zero_solutions.h>
 #include <cegis/control/facade/control_runner.h>
 
-// XXX: Debug
-#include <iostream>
-// XXX: Debug
-
 namespace
 {
 template<class solution_configt, class zero_solutiont>

src/cegis/control/learn/vector_solution_configuration.cpp

@@ -23,21 +23,19 @@ bool is_solution(const goto_trace_stept &step)
   return CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME == id;
 }
 
-const struct_exprt &find_solution(const goto_tracet &trace)
+const array_exprt &find_solution(const goto_tracet &trace)
 {
   const goto_tracet::stepst &steps=trace.steps;
   const auto it=std::find_if(steps.begin(), steps.end(), is_solution);
   assert(steps.end() != it);
-  return to_struct_expr(it->full_lhs_value);
+  return to_array_expr(it->full_lhs_value);
 }
 }
 
 void vector_solution_configurationt::convert(solutiont &current_candidate,
     const goto_tracet &trace, const symbol_tablet &st)
 {
-  const namespacet ns(st);
-  const struct_exprt &value=find_solution(trace);
-  current_candidate.K=get_K_controller_comp(ns, value);
+  current_candidate.K=find_solution(trace);
 }
 
 void vector_solution_configurationt::show_candidate(messaget::mstreamt &os,

src/cegis/control/preprocessing/control_preprocessing.cpp

@@ -1,16 +1,22 @@
+#include <util/cprover_prefix.h>
+
 #include <cegis/cegis-util/string_helper.h>
 #include <cegis/cegis-util/inline_user_program.h>
 #include <cegis/cegis-util/counterexample_vars.h>
 #include <cegis/cegis-util/program_helper.h>
+#include <cegis/instrument/literals.h>
 #include <cegis/control/value/control_vars.h>
 #include <cegis/control/simplify/remove_unused_elements.h>
 #include <cegis/control/preprocessing/propagate_controller_sizes.h>
 #include <cegis/control/preprocessing/control_preprocessing.h>
+#include <goto-programs/remove_returns.h>
 
 // XXX: Debug
 #include <iostream>
 // XXX: Debug
 
+#define TMP_MARKER "$tmp"
+
 control_preprocessingt::control_preprocessingt(const symbol_tablet &st,
     const goto_functionst &gf) :
     control_program(st, gf)
@@ -33,11 +39,34 @@ 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;
-  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;
+  if (goto_program_instruction_typet::ASSIGN != pos->type
+      && goto_program_instruction_typet::DECL != pos->type) return false;
+  const std::string &var=id2string(get_affected_variable(*pos));
+  if (contains(var, TMP_MARKER) || contains(var, RETURN_VALUE_SUFFIX)
+      || contains(var, CPROVER_PREFIX)) return true;
+  return CEGIS_CONTROL_SOLUTION_VAR_NAME == var
+      || CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME == var;
+}
+
+void add_explicit_nondet_for_extern_vars(goto_programt::targetst &locs,
+    const symbol_tablet &st, goto_functionst &gf)
+{
+  goto_programt &entry_body=get_body(gf, CPROVER_INIT);
+  goto_programt::instructionst &instrs=entry_body.instructions;
+  goto_programt::targett pos=std::prev(instrs.end(), 1);
+  for (const symbol_tablet::symbolst::value_type &id_and_symbol : st.symbols)
+  {
+    const symbolt &symbol=id_and_symbol.second;
+    if (!symbol.is_extern) continue;
+    const source_locationt &loc=pos->source_location;
+    pos=entry_body.insert_before(pos);
+    pos->source_location=loc;
+    pos->type=goto_program_instruction_typet::ASSIGN;
+    const side_effect_expr_nondett rhs(symbol.type);
+    pos->code=code_assignt(symbol.symbol_expr(), rhs);
+  }
+  entry_body.update();
+  collect_counterexample_locations(locs, entry_body, is_meta, locs.size());
 }
 }
 
@@ -50,6 +79,7 @@ void control_preprocessingt::operator ()()
   goto_programt::targetst &locs=control_program.counterexample_locations;
   goto_programt &body=get_entry_body(gf);
   collect_counterexample_locations(locs, body, is_meta);
+  add_explicit_nondet_for_extern_vars(locs, st, gf);
   // XXX: Debug
   for (const goto_programt::const_targett target : locs)
   {

src/cegis/control/preprocessing/propagate_controller_sizes.cpp

@@ -46,13 +46,6 @@ const array_exprt &get_b_controller_comp(const namespacet &ns,
       get_controller_comp(ns, value, CEGIS_CONTROL_B_MEMBER_NAME));
 }
 
-const array_exprt &get_K_controller_comp(const namespacet &ns,
-    const struct_exprt &value)
-{
-  return to_array_expr(
-      get_controller_comp(ns, value, CEGIS_CONTROL_K_MEMBER_NAME));
-}
-
 namespace
 {
 const exprt &get_a_size(const namespacet &ns, const struct_exprt &value)

src/cegis/control/preprocessing/propagate_controller_sizes.h

@@ -68,20 +68,6 @@ const array_exprt &get_b_controller_comp(
     const namespacet &ns,
     const struct_exprt &value);
 
-/**
- * @brief
- *
- * @details
- *
- * @param ns
- * @param value
- *
- * @return
- */
-const array_exprt &get_K_controller_comp(
-    const namespacet &ns,
-    const struct_exprt &value);
-
 /**
  * @brief
  *

src/cegis/control/value/control_types.cpp

@@ -9,9 +9,9 @@ const symbol_typet &control_solution_type(const symbol_tablet &st)
   return to_symbol_type(st.lookup(CEGIS_CONTROL_SOLUTION_VAR_NAME).type);
 }
 
-const symbol_typet &control_vector_solution_type(const symbol_tablet &st)
+const array_typet &control_vector_solution_type(const symbol_tablet &st)
 {
-  return to_symbol_type(st.lookup(CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME).type);
+  return to_array_type(st.lookup(CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME).type);
 }
 
 namespace

src/cegis/control/value/control_types.h

@@ -30,7 +30,7 @@ const class symbol_typet &control_solution_type(const class symbol_tablet &st);
  *
  * @return
  */
-const class symbol_typet &control_vector_solution_type(const class symbol_tablet &st);
+const class array_typet &control_vector_solution_type(const class symbol_tablet &st);
 
 /**
  * @brief

src/cegis/control/value/control_vars.h

@@ -11,7 +11,7 @@
 #define CPROVER_CEGIS_CONTROL_VALUE_CONTROL_VARS_H
 
 #define CEGIS_CONTROL_SOLUTION_VAR_NAME "controller"
-#define CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME "_controller"
+#define CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME "K_fxp"
 #define __CEGIS_ALTERNATIVE_MEMBER_NAMES
 #ifndef __CEGIS_ALTERNATIVE_MEMBER_NAMES
 #define CEGIS_CONTROL_A_MEMBER_NAME "a"
@@ -21,7 +21,6 @@
 #else
 #define CEGIS_CONTROL_A_MEMBER_NAME "den"
 #define CEGIS_CONTROL_B_MEMBER_NAME "num"
-#define CEGIS_CONTROL_K_MEMBER_NAME "K"
 #define CEGIS_CONTROL_A_SIZE_MEMBER_NAME "den_size"
 #define CEGIS_CONTROL_B_SIZE_MEMBER_NAME "num_size"
 #endif

src/cegis/control/verify/insert_solution.cpp

@@ -96,8 +96,5 @@ void insert_solution(control_programt &program,
   const is_assignment_tot pred(CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME);
   const goto_programt::targett it=std::find_if(instrs.begin(), end, pred);
   assert(end != it);
-  struct_exprt &value=to_struct_expr(to_code_assign(it->code).rhs());
-  const namespacet ns(program.st);
-  exprt &k=get_controller_comp(ns, value, CEGIS_CONTROL_K_MEMBER_NAME);
-  k=solution.K;
+  to_code_assign(it->code).rhs()=solution.K;
 }

src/cegis/control/verify/zero_solutions.cpp

@@ -10,12 +10,7 @@
 
 bool is_vector_solution_config(const symbol_tablet &st)
 {
-  if (!st.has_symbol(CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME)) return false;
-  const typet &type=st.lookup(CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME).type;
-  const typet &resolved=namespacet(st).follow(type);
-  if (ID_struct != resolved.id()) return false;
-  const struct_typet &struct_type=to_struct_type(resolved);
-  return struct_type.has_component(CEGIS_CONTROL_K_MEMBER_NAME);
+  return st.has_symbol(CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME);
 }
 
 zero_rational_solutiont::zero_rational_solutiont(const symbol_tablet &st) :
@@ -52,8 +47,9 @@ void zero_vector_solutiont::operator ()(
     control_vector_solutiont &solution) const
 {
   if (!solution.K.operands().empty()) return;
-  const symbol_typet &type=control_vector_solution_type(st);
   const namespacet ns(st);
-  const struct_exprt zero_struct=make_zero(ns, type);
-  solution.K=get_K_controller_comp(ns, zero_struct);
+  const array_typet &type=control_vector_solution_type(st);
+  const source_locationt loc(default_cegis_source_location());
+  null_message_handlert msg;
+  solution.K=to_array_expr(zero_initializer(type, loc, ns, msg));
 }