Merge pull request #2434 from tautschnig/vs-ui

Do not artificially separate message handler and uit

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -523,8 +523,7 @@ int jbmc_parse_optionst::doit()
       path_strategy_chooser,
       options,
       goto_model,
-      ui_message_handler.get_ui(),
-      *this,
+      ui_message_handler,
       configure_bmc);
   }
   else
@@ -557,15 +556,13 @@ int jbmc_parse_optionst::doit()
 
     // The `configure_bmc` callback passed will enable enum-unwind-static if
     // applicable.
-    return
-      bmct::do_language_agnostic_bmc(
-        path_strategy_chooser,
-        options,
-        lazy_goto_model,
-        ui_message_handler.get_ui(),
-        *this,
-        configure_bmc,
-        callback_after_symex);
+    return bmct::do_language_agnostic_bmc(
+      path_strategy_chooser,
+      options,
+      lazy_goto_model,
+      ui_message_handler,
+      configure_bmc,
+      callback_after_symex);
   }
 }
 
@@ -618,8 +615,7 @@ int jbmc_parse_optionst::get_goto_program(
     {
       class_hierarchyt hierarchy;
       hierarchy(lazy_goto_model.symbol_table);
-      show_class_hierarchy(
-        hierarchy, get_message_handler(), ui_message_handler.get_ui());
+      show_class_hierarchy(hierarchy, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
 

jbmc/src/jdiff/java_syntactic_diff.h

@@ -21,7 +21,7 @@ class java_syntactic_difft : public goto_difft
     const goto_modelt &_goto_model1,
     const goto_modelt &_goto_model2,
     const optionst &_options,
-    message_handlert &_message_handler)
+    ui_message_handlert &_message_handler)
     : goto_difft(_goto_model1, _goto_model2, _options, _message_handler)
   {
   }

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -274,8 +274,7 @@ int jdiff_parse_optionst::doit()
   }
 
   java_syntactic_difft sd(
-    goto_model1, goto_model2, options, get_message_handler());
-  sd.set_ui(get_ui());
+    goto_model1, goto_model2, options, ui_message_handler);
   sd();
   sd.output_functions();
 

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -152,8 +152,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
   bv_refinementt::infot info;
   info.ns=&ns;
   info.prop=&sat_check;
-  const auto ui=ui_message_handlert::uit::PLAIN;
-  info.ui=ui;
+  info.output_xml = false;
   bv_refinementt solver(info);
   solver << expr;
   return solver();

src/cbmc/all_properties.cpp

@@ -152,7 +152,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
 void bmc_all_propertiest::report(const cover_goalst &cover_goals)
 {
-  switch(bmc.ui)
+  switch(bmc.ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     {
@@ -202,8 +202,10 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
 
     case ui_message_handlert::uit::JSON_UI:
     {
+      if(result().tellp() > 0)
+        result() << eom; // force end of previous message
       json_stream_objectt &json_result =
-        result().json_stream().push_back_stream_object();
+        bmc.ui_message_handler.get_json_stream().push_back_stream_object();
       json_stream_arrayt &result_array =
         json_result.push_back_stream_array("result");
 

src/cbmc/bmc.cpp

@@ -54,7 +54,7 @@ void bmct::error_trace()
   goto_tracet &goto_trace=safety_checkert::error_trace;
   build_goto_trace(equation, prop_conv, ns, goto_trace);
 
-  switch(ui)
+  switch(ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     result() << "Counterexample:" << eom;
@@ -72,8 +72,10 @@ void bmct::error_trace()
 
   case ui_message_handlert::uit::JSON_UI:
     {
+      if(status().tellp() > 0)
+        status() << eom; // force end of previous message
       json_stream_objectt &json_result =
-        status().json_stream().push_back_stream_object();
+        ui_message_handler.get_json_stream().push_back_stream_object();
       const goto_trace_stept &step=goto_trace.steps.back();
       json_result["property"] =
         json_stringt(step.pc->source_location.get_property_id());
@@ -153,7 +155,7 @@ void bmct::report_success()
 {
   result() << "VERIFICATION SUCCESSFUL" << eom;
 
-  switch(ui)
+  switch(ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -180,7 +182,7 @@ void bmct::report_failure()
 {
   result() << "VERIFICATION FAILED" << eom;
 
-  switch(ui)
+  switch(ui_message_handler.get_ui())
   {
   case ui_message_handlert::uit::PLAIN:
     break;
@@ -294,7 +296,7 @@ safety_checkert::resultt bmct::execute(
 
     if(options.get_bool_option("show-vcc"))
     {
-      show_vcc(options, get_message_handler(), ui, ns, equation);
+      show_vcc(options, ui_message_handler, ns, equation);
       return safety_checkert::resultt::SAFE; // to indicate non-error
     }
 
@@ -420,7 +422,7 @@ void bmct::show()
 {
   if(options.get_bool_option("show-vcc"))
   {
-    show_vcc(options, get_message_handler(), ui, ns, equation);
+    show_vcc(options, ui_message_handler, ns, equation);
   }
 
   if(options.get_bool_option("program-only"))
@@ -478,15 +480,14 @@ int bmct::do_language_agnostic_bmc(
   const path_strategy_choosert &path_strategy_chooser,
   const optionst &opts,
   abstract_goto_modelt &model,
-  const ui_message_handlert::uit &ui,
-  messaget &message,
+  ui_message_handlert &ui,
   std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc,
   std::function<bool(void)> callback_after_symex)
 {
   safety_checkert::resultt final_result = safety_checkert::resultt::UNKNOWN;
   safety_checkert::resultt tmp_result = safety_checkert::resultt::UNKNOWN;
   const symbol_tablet &symbol_table = model.get_symbol_table();
-  message_handlert &mh = message.get_message_handler();
+  messaget message(ui);
   std::unique_ptr<path_storaget> worklist;
   std::string strategy = opts.get_option("exploration-strategy");
   INVARIANT(
@@ -496,13 +497,15 @@ int bmct::do_language_agnostic_bmc(
   try
   {
     {
-      cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
-      solvers.set_ui(ui);
+      cbmc_solverst solvers(
+        opts,
+        symbol_table,
+        ui,
+        ui.get_ui() == ui_message_handlert::uit::XML_UI);
       std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
       cbmc_solver = solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
-      bmct bmc(opts, symbol_table, mh, pc, *worklist, callback_after_symex);
-      bmc.set_ui(ui);
+      bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex);
       if(driver_configure_bmc)
         driver_configure_bmc(bmc, symbol_table);
       tmp_result = bmc.run(model);
@@ -546,16 +549,19 @@ int bmct::do_language_agnostic_bmc(
                          << "Starting new path (" << worklist->size()
                          << " to go)\n"
                          << message.eom;
-      cbmc_solverst solvers(opts, symbol_table, message.get_message_handler());
-      solvers.set_ui(ui);
+      cbmc_solverst solvers(
+        opts,
+        symbol_table,
+        ui,
+        ui.get_ui() == ui_message_handlert::uit::XML_UI);
       std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
       cbmc_solver = solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
       path_storaget::patht &resume = worklist->peek();
       path_explorert pe(
         opts,
         symbol_table,
-        mh,
+        ui,
         pc,
         resume.equation,
         resume.state,

src/cbmc/bmc.h

@@ -66,7 +66,7 @@ class bmct:public safety_checkert
   bmct(
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
-    message_handlert &_message_handler,
+    ui_message_handlert &_message_handler,
     prop_convt &_prop_conv,
     path_storaget &_path_storage,
     std::function<bool(void)> callback_after_symex)
@@ -83,7 +83,7 @@ class bmct:public safety_checkert
         options,
         path_storage),
       prop_conv(_prop_conv),
-      ui(ui_message_handlert::uit::PLAIN),
+      ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
     symex.constant_propagation=options.get_bool_option("propagation");
@@ -103,8 +103,6 @@ class bmct:public safety_checkert
   safety_checkert::resultt execute(abstract_goto_modelt &);
   virtual ~bmct() { }
 
-  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
-
   // the safety_checkert interface
   virtual resultt operator()(
     const goto_functionst &goto_functions)
@@ -127,10 +125,9 @@ class bmct:public safety_checkert
     const path_strategy_choosert &path_strategy_chooser,
     const optionst &opts,
     abstract_goto_modelt &goto_model,
-    const ui_message_handlert::uit &ui,
-    messaget &message,
-    std::function<void(bmct &, const symbol_tablet &)>
-      driver_configure_bmc = nullptr,
+    ui_message_handlert &ui,
+    std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc =
+      nullptr,
     std::function<bool(void)> callback_after_symex = nullptr);
 
 protected:
@@ -144,7 +141,7 @@ class bmct:public safety_checkert
   bmct(
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
-    message_handlert &_message_handler,
+    ui_message_handlert &_message_handler,
     prop_convt &_prop_conv,
     symex_target_equationt &_equation,
     path_storaget &_path_storage,
@@ -162,7 +159,7 @@ class bmct:public safety_checkert
         options,
         path_storage),
       prop_conv(_prop_conv),
-      ui(ui_message_handlert::uit::PLAIN),
+      ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
     symex.constant_propagation = options.get_bool_option("propagation");
@@ -186,7 +183,7 @@ class bmct:public safety_checkert
   prop_convt &prop_conv;
   std::unique_ptr<memory_model_baset> memory_model;
   // use gui format
-  ui_message_handlert::uit ui;
+  ui_message_handlert &ui_message_handler;
 
   virtual decision_proceduret::resultt
     run_decision_procedure(prop_convt &prop_conv);
@@ -259,7 +256,7 @@ class path_explorert : public bmct
   path_explorert(
     const optionst &_options,
     const symbol_tablet &outer_symbol_table,
-    message_handlert &_message_handler,
+    ui_message_handlert &_message_handler,
     prop_convt &_prop_conv,
     symex_target_equationt &saved_equation,
     const goto_symex_statet &saved_state,

src/cbmc/bmc_cover.cpp

@@ -261,7 +261,7 @@ bool bmc_covert::operator()()
     if(g.second.satisfied)
       goals_covered++;
 
-  switch(bmc.ui)
+  switch(bmc.ui_message_handler.get_ui())
   {
     case ui_message_handlert::uit::PLAIN:
     {
@@ -341,8 +341,10 @@ bool bmc_covert::operator()()
 
     case ui_message_handlert::uit::JSON_UI:
     {
+      if(status().tellp() > 0)
+        status() << eom; // force end of previous message
       json_stream_objectt &json_result =
-        status().json_stream().push_back_stream_object();
+        bmc.ui_message_handler.get_json_stream().push_back_stream_object();
       for(const auto &goal_pair : goal_map)
       {
         const goalt &goal=goal_pair.second;
@@ -406,7 +408,7 @@ bool bmc_covert::operator()()
                << (cover_goals.iterations()==1?"":"s")
                << eom;
 
-  if(bmc.ui==ui_message_handlert::uit::PLAIN)
+  if(bmc.ui_message_handler.get_ui() == ui_message_handlert::uit::PLAIN)
   {
     result() << "Test suite:" << '\n';
 

src/cbmc/cbmc_parse_options.cpp

@@ -527,11 +527,7 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
   return bmct::do_language_agnostic_bmc(
-    path_strategy_chooser,
-    options,
-    goto_model,
-    ui_message_handler.get_ui(),
-    *this);
+    path_strategy_chooser, options, goto_model, ui_message_handler);
 }
 
 bool cbmc_parse_optionst::set_properties()

src/cbmc/cbmc_solvers.cpp

@@ -72,7 +72,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
     solver->set_prop(util_make_unique<satcheckt>());
   }
 
-  solver->prop().set_message_handler(get_message_handler());
+  solver->prop().set_message_handler(message_handler);
 
   auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
 
@@ -92,7 +92,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
   no_incremental_check();
 
   auto prop=util_make_unique<dimacs_cnft>();
-  prop->set_message_handler(get_message_handler());
+  prop->set_message_handler(message_handler);
 
   std::string filename=options.get_option("outfile");
 
@@ -113,12 +113,12 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
     return util_make_unique<satcheck_no_simplifiert>();
   }();
 
-  prop->set_message_handler(get_message_handler());
+  prop->set_message_handler(message_handler);
 
   bv_refinementt::infot info;
   info.ns=&ns;
   info.prop=prop.get();
-  info.ui=ui;
+  info.output_xml = output_xml_in_refinement;
 
   // we allow setting some parameters
   if(options.get_bool_option("max-node-refinement"))
@@ -141,10 +141,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   string_refinementt::infot info;
   info.ns=&ns;
   auto prop=util_make_unique<satcheck_no_simplifiert>();
-  prop->set_message_handler(get_message_handler());
+  prop->set_message_handler(message_handler);
   info.prop=prop.get();
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
-  info.ui=ui;
+  info.output_xml = output_xml_in_refinement;
   if(options.get_bool_option("max-node-refinement"))
     info.max_node_refinement=
       options.get_unsigned_int_option("max-node-refinement");
@@ -197,7 +197,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
     if(options.get_bool_option("fpa"))
       smt2_conv->use_FPA_theory=true;
 
-    smt2_conv->set_message_handler(get_message_handler());
+    smt2_conv->set_message_handler(message_handler);
 
     return util_make_unique<solvert>(std::move(smt2_conv));
   }
@@ -226,7 +226,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
     if(options.get_bool_option("fpa"))
       smt2_conv->use_FPA_theory=true;
 
-    smt2_conv->set_message_handler(get_message_handler());
+    smt2_conv->set_message_handler(message_handler);
 
     return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
   }