zero_initializer without message_handlert

Throws a string instead of 0.

Author: tautschnig

src/cegis/control/facade/control_runner.cpp

@@ -7,8 +7,6 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <linking/zero_initializer.h>
-
 #include <cegis/symex/cegis_symex_learn.h>
 #include <cegis/symex/cegis_symex_verify.h>
 #include <cegis/facade/runner_helper.h>

src/cegis/control/verify/insert_solution.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
-#include <util/message.h>
 #include <linking/zero_initializer.h>
 
 #include <cegis/cegis-util/program_helper.h>
@@ -56,8 +55,7 @@ struct_exprt to_struct_expr(const symbol_tablet &st,
   const symbol_typet &type=control_solution_type(st);
   const namespacet ns(st);
   const struct_typet &struct_type=to_struct_type(ns.follow(type));
-  null_message_handlert msg;
-  const exprt zero(zero_initializer(type, loc, ns, msg));
+  const exprt zero(zero_initializer(type, loc, ns));
   struct_exprt result(to_struct_expr(zero));
   struct_exprt::operandst &ops=result.operands();
   set_array(ops, st, struct_type, solution.a, CEGIS_CONTROL_A_MEMBER_NAME);

src/cegis/control/verify/zero_solutions.cpp

@@ -32,8 +32,7 @@ namespace
 struct_exprt make_zero(const namespacet &ns, const symbol_typet &type)
 {
   const source_locationt loc(default_cegis_source_location());
-  null_message_handlert msg;
-  return to_struct_expr(zero_initializer(type, loc, ns, msg));
+  return to_struct_expr(zero_initializer(type, loc, ns));
 }
 }
 
@@ -59,6 +58,5 @@ void zero_vector_solutiont::operator ()(
   const namespacet ns(st);
   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));
+  solution.K=to_array_expr(zero_initializer(type, loc, ns));
 }

src/cegis/jsa/learn/jsa_symex_learn.cpp

@@ -45,7 +45,6 @@ void jsa_symex_learnt::process(const counterexamplest &counterexamples,
 
 void jsa_symex_learnt::process(const size_t max_solution_size)
 {
-  null_message_handlert msg;
   const namespacet ns(original_program.st);
   counterexamplest counterexamples(1);
   counterexamplet &counterexample=counterexamples.front();
@@ -55,7 +54,7 @@ void jsa_symex_learnt::process(const size_t max_solution_size)
     const irep_idt &key=pos->labels.front();
     const typet &type=get_affected_type(*pos);
     const source_locationt &loc=pos->source_location;
-    const exprt value(zero_initializer(type, loc, ns, msg));
+    const exprt value(zero_initializer(type, loc, ns));
     counterexample.insert(std::make_pair(key, value));
   }
   process(counterexamples, max_solution_size);

src/cegis/jsa/preprocessing/add_synthesis_library.cpp

@@ -93,7 +93,6 @@ void zero_new_global_vars(const symbol_tablet &st, goto_functionst &gf)
   assert(init.body_available());
   goto_programt &body=init.body;
   goto_programt::targett pos=std::prev(body.instructions.end(), 2);
-  null_message_handlert msg;
   const source_locationt loc(jsa_builtin_source_location());
   const namespacet ns(st);
   for (const symbol_tablet::symbolst::value_type &symbol : st.symbols)
@@ -103,7 +102,7 @@ void zero_new_global_vars(const symbol_tablet &st, goto_functionst &gf)
       pos->type=goto_program_instruction_typet::ASSIGN;
       pos->source_location=loc;
       const symbol_exprt lhs(ns.lookup(symbol.first).symbol_expr());
-      const exprt rhs(zero_initializer(lhs.type(), loc, ns, msg));
+      const exprt rhs(zero_initializer(lhs.type(), loc, ns));
       pos->code=code_assignt(lhs, rhs);
     }
 }

src/cegis/learn/insert_counterexample.cpp

@@ -31,12 +31,11 @@ zero_valuest get_zero_values(const symbol_tablet &st,
   std::map<const irep_idt, exprt> zero_values;
   const source_locationt loc(default_cegis_source_location());
   const namespacet ns(st);
-  null_message_handlert msg;
   for (const goto_programt::const_targett pos : ce_locs)
   {
     const irep_idt &marker=get_counterexample_marker(pos);
     const typet &type=get_affected_type(*pos);
-    const exprt value(zero_initializer(type, loc, ns, msg));
+    const exprt value(zero_initializer(type, loc, ns));
     zero_values.insert(std::make_pair(marker, value));
   }
   return zero_values;
@@ -172,8 +171,7 @@ void add_array_indexes(const std::set<irep_idt> &ce_keys, symbol_tablet &st,
   pos=declare_cegis_meta_variable(st, gf, std::prev(pos), CE_ARRAY_INDEX, type);
   const source_locationt loc(default_cegis_source_location());
   const namespacet ns(st);
-  null_message_handlert msg;
-  const exprt zero(zero_initializer(type, loc, ns, msg));
+  const exprt zero(zero_initializer(type, loc, ns));
   assign_cegis_meta_variable(st, gf, pos, CE_ARRAY_INDEX, zero);
   pos=cprover_init;
   for (const irep_idt &key : ce_keys)

src/cegis/refactor/instructionset/create_cegis_processor.cpp

@@ -7,8 +7,9 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <ansi-c/c_types.h>
 #include <util/arith_tools.h>
+
+#include <ansi-c/c_types.h>
 #include <linking/zero_initializer.h>
 
 #include <cegis/instrument/literals.h>
@@ -83,8 +84,7 @@ void create_variable_array(symbol_tablet &st, goto_functionst &gf,
   pos->source_location=new_symbol.location;
   const symbol_exprt lhs(st.lookup(name).symbol_expr());
   const namespacet ns(st);
-  null_message_handlert msg;
-  const exprt rhs(zero_initializer(array_type, new_symbol.location, ns, msg));
+  const exprt rhs(zero_initializer(array_type, new_symbol.location, ns));
   pos->code=code_assignt(lhs, rhs);
   body.update();
 }

src/cegis/refactor/verify/refactor_symex_verify.cpp

@@ -28,14 +28,13 @@ void refactor_symex_verifyt::process(const candidatet &candidate)
   symbol_tablet &st=current_program.st;
   goto_functionst &gf=current_program.gf;
   const namespacet ns(st);
-  null_message_handlert msg;
   for (const irep_idt &program : current_program.programs)
   {
     symbolt &symbol=st.lookup(program);
     const candidatet::const_iterator it=candidate.find(program);
     if (candidate.end() == it)
     {
-      const exprt zero(zero_initializer(symbol.type, symbol.location, ns, msg));
+      const exprt zero(zero_initializer(symbol.type, symbol.location, ns));
       assign_in_cprover_init(gf, symbol, zero);
     } else assign_in_cprover_init(gf, symbol, it->second);
   }

src/goto-symex/symex_start_thread.cpp

@@ -6,8 +6,6 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <util/message.h>
-
 #include <linking/zero_initializer.h>
 
 #include "goto_symex.h"
@@ -116,10 +114,7 @@ void goto_symext::symex_start_thread(statet &state)
 
     exprt rhs=symbol.value;
     if(rhs.is_nil())
-    {
-      null_message_handlert null_message;
-      rhs=zero_initializer(symbol.type, symbol.location, ns, null_message);
-    }
+      rhs=zero_initializer(symbol.type, symbol.location, ns);
 
     guardt guard;
     symex_assign_symbol(state, lhs, nil_exprt(), rhs, guard, symex_targett::HIDDEN);

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
+#include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/expanding_vector.h>
 #include <util/string2int.h>

src/linking/zero_initializer.cpp

@@ -6,9 +6,11 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <sstream>
+
+#include <util/namespace.h>
 #include <util/message.h>
 #include <util/arith_tools.h>
-#include <util/expr_util.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
 #include <util/pointer_offset_size.h>
@@ -298,3 +300,34 @@ exprt zero_initializer(
   zero_initializert z_i(ns, message_handler);
   return z_i(type, source_location);
 }
+
+/*******************************************************************\
+
+Function: zero_initializer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt zero_initializer(
+  const typet &type,
+  const source_locationt &source_location,
+  const namespacet &ns)
+{
+  std::ostringstream oss;
+  stream_message_handlert mh(oss);
+
+  try
+  {
+    zero_initializert z_i(ns, mh);
+    return z_i(type, source_location);
+  }
+  catch(int)
+  {
+    throw oss.str();
+  }
+}

src/linking/zero_initializer.h

@@ -10,13 +10,21 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_LINKING_ZERO_INITIALIZER_H
 
 #include <util/expr.h>
-#include <util/namespace.h>
-#include <util/message.h>
+
+class message_handlert;
+class namespacet;
+class source_locationt;
 
 exprt zero_initializer(
   const typet &,
   const source_locationt &,
   const namespacet &,
   message_handlert &);
 
+// throws a char* in case of failure
+exprt zero_initializer(
+  const typet &,
+  const source_locationt &,
+  const namespacet &);
+
 #endif // CPROVER_LINKING_ZERO_INITIALIZER_H