From 4a710c7d84667e98a2d39dfb0d701755b4704b22 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 4 Sep 2018 21:02:25 +0100 Subject: [PATCH 1/2] Factor out bmct building blocks into bmc_util This is an intermediate step in order to reuse the building blocks in the new implementation of bmct. The old implementation is functional until it can be replaced by the new one. --- jbmc/src/jbmc/Makefile | 1 + jbmc/unit/Makefile | 1 + src/cbmc/Makefile | 1 + src/cbmc/all_properties.cpp | 10 +- src/cbmc/bmc.cpp | 271 +++----------------------------- src/cbmc/bmc.h | 14 -- src/cbmc/bmc_cover.cpp | 6 +- src/cbmc/bmc_util.cpp | 267 +++++++++++++++++++++++++++++++ src/cbmc/bmc_util.h | 74 +++++++++ src/cbmc/fault_localization.cpp | 18 ++- unit/Makefile | 1 + 11 files changed, 390 insertions(+), 274 deletions(-) create mode 100644 src/cbmc/bmc_util.cpp create mode 100644 src/cbmc/bmc_util.h diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index 57eb5ad31e7..c60416ed92a 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -40,6 +40,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \ ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \ + ../$(CPROVER_DIR)/src/cbmc/bmc_util$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \ diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index d1e009b831c..c9570574da3 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -85,6 +85,7 @@ java-testing-utils-clean: BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \ + $(CPROVER_DIR)/src/cbmc/bmc_util$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 4dec22ee526..5ba3d3d8e0d 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -1,6 +1,7 @@ SRC = all_properties.cpp \ bmc.cpp \ bmc_cover.cpp \ + bmc_util.cpp \ cbmc_languages.cpp \ cbmc_main.cpp \ cbmc_parse_options.cpp \ diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 35b4286d33c..8b6379adc11 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include @@ -55,7 +57,9 @@ safety_checkert::resultt bmc_all_propertiest::operator()() auto solver_start=std::chrono::steady_clock::now(); - bmc.do_conversion(); + convert_symex_target_equation( + bmc.equation, bmc.prop_conv, get_message_handler()); + bmc.freeze_program_variables(); // Collect _all_ goals in `goal_map'. // This maps property IDs to 'goalt' @@ -144,9 +148,9 @@ safety_checkert::resultt bmc_all_propertiest::operator()() bool safe=(cover_goals.number_covered()==0); if(safe) - bmc.report_success(); // legacy, might go away + report_success(bmc.ui_message_handler); // legacy, might go away else - bmc.report_failure(); // legacy, might go away + report_failure(bmc.ui_message_handler); // legacy, might go away return safe?safety_checkert::resultt::SAFE:safety_checkert::resultt::UNSAFE; } diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 3bbfe3764c5..54b174d5e67 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -19,21 +19,14 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include -#include -#include - -#include -#include #include #include -#include -#include #include #include +#include "bmc_util.h" #include "counterexample_beautification.h" #include "fault_localization.h" @@ -48,84 +41,6 @@ void bmct::freeze_program_variables() // this is a hook for cegis } -void bmct::error_trace() -{ - status() << "Building error trace" << eom; - - goto_tracet &goto_trace=safety_checkert::error_trace; - build_goto_trace(equation, prop_conv, ns, goto_trace); - - switch(ui_message_handler.get_ui()) - { - case ui_message_handlert::uit::PLAIN: - result() << "Counterexample:" << eom; - show_goto_trace(result(), ns, goto_trace, trace_options()); - result() << eom; - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml; - convert(ns, goto_trace, xml); - status() << xml; - } - break; - - case ui_message_handlert::uit::JSON_UI: - { - if(status().tellp() > 0) - status() << eom; // force end of previous message - json_stream_objectt &json_result = - 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()); - json_result["description"] = - json_stringt(step.pc->source_location.get_comment()); - json_result["status"]=json_stringt("failed"); - json_stream_arrayt &json_trace = - json_result.push_back_stream_array("trace"); - convert(ns, goto_trace, json_trace, trace_options()); - } - break; - } -} - -/// outputs witnesses in graphml format -void bmct::output_graphml(resultt result) -{ - const std::string graphml=options.get_option("graphml-witness"); - if(graphml.empty()) - return; - - graphml_witnesst graphml_witness(ns); - if(result==resultt::UNSAFE) - graphml_witness(safety_checkert::error_trace); - else if(result==resultt::SAFE) - graphml_witness(equation); - else - return; - - if(graphml=="-") - write_graphml(graphml_witness.graph(), std::cout); - else - { - std::ofstream out(graphml); - write_graphml(graphml_witness.graph(), out); - } -} - -void bmct::do_conversion() -{ - status() << "converting SSA" << eom; - - // convert SSA - equation.convert(prop_conv); - - // hook for cegis to freeze synthesis program vars - freeze_program_variables(); -} - decision_proceduret::resultt bmct::run_decision_procedure() { status() << "Passing problem to " @@ -135,7 +50,10 @@ decision_proceduret::resultt bmct::run_decision_procedure() auto solver_start = std::chrono::steady_clock::now(); - do_conversion(); + convert_symex_target_equation(equation, prop_conv, get_message_handler()); + + // hook for cegis to freeze synthesis program vars + freeze_program_variables(); status() << "Running " << prop_conv.decision_procedure_text() << eom; @@ -151,103 +69,6 @@ decision_proceduret::resultt bmct::run_decision_procedure() return dec_result; } -void bmct::report_success() -{ - report_success(*this, ui_message_handler); -} - -void bmct::report_success(messaget &log, ui_message_handlert &handler) -{ - log.result() << log.bold << "VERIFICATION SUCCESSFUL" << log.reset << log.eom; - - switch(handler.get_ui()) - { - case ui_message_handlert::uit::PLAIN: - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml("cprover-status"); - xml.data="SUCCESS"; - log.result() << xml; - } - break; - - case ui_message_handlert::uit::JSON_UI: - { - json_objectt json_result({{"cProverStatus", json_stringt("success")}}); - log.result() << json_result; - } - break; - } -} - -void bmct::report_failure() -{ - report_failure(*this, ui_message_handler); -} - -void bmct::report_failure(messaget &log, ui_message_handlert &handler) -{ - log.result() << log.bold << "VERIFICATION FAILED" << log.reset << log.eom; - - switch(handler.get_ui()) - { - case ui_message_handlert::uit::PLAIN: - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml("cprover-status"); - xml.data="FAILURE"; - log.result() << xml; - } - break; - - case ui_message_handlert::uit::JSON_UI: - { - json_objectt json_result({{"cProverStatus", json_stringt("failure")}}); - log.result() << json_result; - } - break; - } -} - -void bmct::get_memory_model() -{ - const std::string mm=options.get_option("mm"); - - if(mm.empty() || mm=="sc") - memory_model=util_make_unique(ns); - else if(mm=="tso") - memory_model=util_make_unique(ns); - else if(mm=="pso") - memory_model=util_make_unique(ns); - else - { - throw invalid_command_line_argument_exceptiont( - "invalid parameter " + mm, "--mm", "try values of sc, tso, pso"); - } -} - -void bmct::setup() -{ - get_memory_model(); - - { - const symbolt *init_symbol; - if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol)) - symex.language_mode=init_symbol->mode; - } - - status() << "Starting Bounded Model Checking" << eom; - - symex.last_source_location.make_nil(); - - symex.unwindset.parse_unwind(options.get_option("unwind")); - symex.unwindset.parse_unwindset(options.get_option("unwindset")); -} - safety_checkert::resultt bmct::execute( abstract_goto_modelt &goto_model) { @@ -293,7 +114,7 @@ safety_checkert::resultt bmct::execute( << equation.SSA_steps.size() << " steps" << eom; - slice(); + slice(symex, equation, ns, options, ui_message_handler); // coverage report std::string cov_out=options.get_option("symex-coverage-report"); @@ -330,8 +151,8 @@ safety_checkert::resultt bmct::execute( { if(options.is_set("paths")) return safety_checkert::resultt::PAUSED; - report_success(); - output_graphml(resultt::SAFE); + report_success(ui_message_handler); + output_graphml(resultt::SAFE, error_trace, equation, ns, options); return safety_checkert::resultt::SAFE; } @@ -372,55 +193,12 @@ safety_checkert::resultt bmct::execute( } } -void bmct::slice() -{ - if(options.get_option("slice-by-trace")!="") - { - symex_slice_by_tracet symex_slice_by_trace(ns); - - symex_slice_by_trace.slice_by_trace - (options.get_option("slice-by-trace"), - equation); - } - // any properties to check at all? - if(equation.has_threads()) - { - // we should build a thread-aware SSA slicer - statistics() << "no slicing due to threads" << eom; - } - else - { - if(options.get_bool_option("slice-formula")) - { - ::slice(equation); - statistics() << "slicing removed " - << equation.count_ignored_SSA_steps() - << " assignments"<(prop_conv), equation); - error_trace(); - output_graphml(resultt::UNSAFE); + build_error_trace( + error_trace, ns, equation, prop_conv, ui_message_handler); + output_error_trace(error_trace, ns, trace_options(), ui_message_handler); + output_graphml(resultt::UNSAFE, error_trace, equation, ns, options); } - report_failure(); + report_failure(ui_message_handler); return resultt::UNSAFE; default: @@ -619,11 +386,11 @@ int bmct::do_language_agnostic_bmc( { case safety_checkert::resultt::SAFE: if(opts.is_set("paths")) - report_success(message, ui); + report_success(ui); return CPROVER_EXIT_VERIFICATION_SAFE; case safety_checkert::resultt::UNSAFE: if(opts.is_set("paths")) - report_failure(message, ui); + report_failure(ui); return CPROVER_EXIT_VERIFICATION_UNSAFE; case safety_checkert::resultt::ERROR: return CPROVER_EXIT_INTERNAL_ERROR; diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 160c1558c47..1f230a34ed5 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -181,8 +181,6 @@ class bmct:public safety_checkert virtual resultt decide(const goto_functionst &); - void do_conversion(); - virtual void freeze_program_variables(); trace_optionst trace_options() @@ -192,18 +190,6 @@ class bmct:public safety_checkert virtual resultt all_properties(const goto_functionst &goto_functions); virtual resultt stop_on_fail(); - virtual void report_success(); - virtual void report_failure(); - - static void report_success(messaget &, ui_message_handlert &); - static void report_failure(messaget &, ui_message_handlert &); - - virtual void error_trace(); - void output_graphml(resultt result); - - void get_memory_model(); - void slice(); - void show(); bool cover(const goto_functionst &goto_functions); diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 6e1ca3e06c4..24cd4d9ea36 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include #include @@ -209,7 +211,9 @@ bool bmc_covert::operator()() // Do conversion to next solver layer - bmc.do_conversion(); + convert_symex_target_equation( + bmc.equation, bmc.prop_conv, get_message_handler()); + bmc.freeze_program_variables(); // get the conditions for these goals from formula // collect all 'instances' of the goals diff --git a/src/cbmc/bmc_util.cpp b/src/cbmc/bmc_util.cpp new file mode 100644 index 00000000000..5a617d2b56b --- /dev/null +++ b/src/cbmc/bmc_util.cpp @@ -0,0 +1,267 @@ +/*******************************************************************\ + +Module: Bounded Model Checking Utilities + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Bounded Model Checking Utilities + +#include "bmc_util.h" + +#include +#include + +#include + +#include +#include +#include + +#include +#include +#include +#include +#include + +#include + +#include + +#include +#include + +void build_error_trace( + goto_tracet &goto_trace, + const namespacet &ns, + const symex_target_equationt &symex_target_equation, + const prop_convt &prop_conv, + ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + msg.status() << "Building error trace" << messaget::eom; + + build_goto_trace(symex_target_equation, prop_conv, ns, goto_trace); +} + +void output_error_trace( + const goto_tracet &goto_trace, + const namespacet &ns, + const trace_optionst &trace_options, + ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + msg.result() << "Counterexample:" << messaget::eom; + show_goto_trace(msg.result(), ns, goto_trace, trace_options); + msg.result() << messaget::eom; + break; + + case ui_message_handlert::uit::XML_UI: + { + xmlt xml; + convert(ns, goto_trace, xml); + msg.status() << xml; + } + break; + + case ui_message_handlert::uit::JSON_UI: + { + json_stream_objectt &json_result = + 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()); + json_result["description"] = + json_stringt(step.pc->source_location.get_comment()); + json_result["status"] = json_stringt("failed"); + json_stream_arrayt &json_trace = + json_result.push_back_stream_array("trace"); + convert(ns, goto_trace, json_trace, trace_options); + } + break; + } +} + +/// outputs witnesses in graphml format +void output_graphml( + safety_checkert::resultt result, + const goto_tracet &goto_trace, + const symex_target_equationt &symex_target_equation, + const namespacet &ns, + const optionst &options) +{ + const std::string graphml = options.get_option("graphml-witness"); + if(graphml.empty()) + return; + + graphml_witnesst graphml_witness(ns); + if(result == safety_checkert::resultt::UNSAFE) + graphml_witness(goto_trace); + else if(result == safety_checkert::resultt::SAFE) + graphml_witness(symex_target_equation); + else + return; + + if(graphml == "-") + write_graphml(graphml_witness.graph(), std::cout); + else + { + std::ofstream out(graphml); + write_graphml(graphml_witness.graph(), out); + } +} + +void convert_symex_target_equation( + symex_target_equationt &equation, + prop_convt &prop_conv, + message_handlert &message_handler) +{ + messaget msg(message_handler); + msg.status() << "converting SSA" << messaget::eom; + + // convert SSA + equation.convert(prop_conv); +} + +std::unique_ptr +get_memory_model(const optionst &options, const namespacet &ns) +{ + const std::string mm = options.get_option("mm"); + + if(mm.empty() || mm == "sc") + return util_make_unique(ns); + else if(mm == "tso") + return util_make_unique(ns); + else if(mm == "pso") + return util_make_unique(ns); + else + { + throw "invalid memory model '" + mm + "': use one of sc, tso, pso"; + } +} + +void setup_symex( + symex_bmct &symex, + const namespacet &ns, + const optionst &options, + ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + const symbolt *init_symbol; + if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol)) + symex.language_mode = init_symbol->mode; + + msg.status() << "Starting Bounded Model Checking" << messaget::eom; + + symex.last_source_location.make_nil(); + + symex.unwindset.parse_unwind(options.get_option("unwind")); + symex.unwindset.parse_unwindset(options.get_option("unwindset")); +} + +void slice( + symex_bmct &symex, + symex_target_equationt &symex_target_equation, + const namespacet &ns, + const optionst &options, + ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + if(options.get_option("slice-by-trace") != "") + { + symex_slice_by_tracet symex_slice_by_trace(ns); + + symex_slice_by_trace.slice_by_trace( + options.get_option("slice-by-trace"), symex_target_equation); + } + // any properties to check at all? + if(symex_target_equation.has_threads()) + { + // we should build a thread-aware SSA slicer + msg.statistics() << "no slicing due to threads" << messaget::eom; + } + else + { + if(options.get_bool_option("slice-formula")) + { + ::slice(symex_target_equation); + msg.statistics() << "slicing removed " + << symex_target_equation.count_ignored_SSA_steps() + << " assignments" << messaget::eom; + } + else + { + if(options.get_list_option("cover").empty()) + { + simple_slice(symex_target_equation); + msg.statistics() << "simple slicing removed " + << symex_target_equation.count_ignored_SSA_steps() + << " assignments" << messaget::eom; + } + } + } + msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), " + << symex.get_remaining_vccs() + << " remaining after simplification" << messaget::eom; +} + +void report_success(ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom; + + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + break; + + case ui_message_handlert::uit::XML_UI: + { + xmlt xml("cprover-status"); + xml.data = "SUCCESS"; + msg.result() << xml; + } + break; + + case ui_message_handlert::uit::JSON_UI: + { + json_objectt json_result; + json_result["cProverStatus"] = json_stringt("success"); + msg.result() << json_result; + } + break; + } +} + +void report_failure(ui_message_handlert &ui_message_handler) +{ + messaget msg(ui_message_handler); + msg.result() << "VERIFICATION FAILED" << messaget::eom; + + switch(ui_message_handler.get_ui()) + { + case ui_message_handlert::uit::PLAIN: + break; + + case ui_message_handlert::uit::XML_UI: + { + xmlt xml("cprover-status"); + xml.data = "FAILURE"; + msg.result() << xml; + } + break; + + case ui_message_handlert::uit::JSON_UI: + { + json_objectt json_result; + json_result["cProverStatus"] = json_stringt("failure"); + msg.result() << json_result; + } + break; + } +} diff --git a/src/cbmc/bmc_util.h b/src/cbmc/bmc_util.h new file mode 100644 index 00000000000..0c3ac4f216d --- /dev/null +++ b/src/cbmc/bmc_util.h @@ -0,0 +1,74 @@ +/*******************************************************************\ + +Module: Bounded Model Checking Utilities + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Bounded Model Checking Utilities + +#ifndef CPROVER_CBMC_BMC_UTIL_H +#define CPROVER_CBMC_BMC_UTIL_H + +#include + +#include + +class goto_tracet; +class memory_model_baset; +class message_handlert; +class namespacet; +class optionst; +class prop_convt; +class symex_bmct; +class symex_target_equationt; +struct trace_optionst; +class ui_message_handlert; + +void convert_symex_target_equation( + symex_target_equationt &, + prop_convt &, + message_handlert &); + +void report_failure(ui_message_handlert &); +void report_success(ui_message_handlert &); + +void build_error_trace( + goto_tracet &, + const namespacet &, + const symex_target_equationt &, + const prop_convt &, + ui_message_handlert &); + +void output_error_trace( + const goto_tracet &, + const namespacet &, + const trace_optionst &, + ui_message_handlert &); + +void output_graphml( + safety_checkert::resultt, + const goto_tracet &, + const symex_target_equationt &, + const namespacet &, + const optionst &); + +std::unique_ptr +get_memory_model(const optionst &options, const namespacet &); + +void setup_symex( + symex_bmct &, + const namespacet &, + const optionst &, + ui_message_handlert &); + +void slice( + symex_bmct &, + symex_target_equationt &symex_target_equation, + const namespacet &, + const optionst &, + ui_message_handlert &); + +#endif // CPROVER_CBMC_BMC_UTIL_H diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index 588ff63d1ff..10b01098497 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -26,6 +26,7 @@ Author: Peter Schrammel #include #include +#include "bmc_util.h" #include "counterexample_beautification.h" void fault_localizationt::freeze_guards() @@ -247,7 +248,9 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv) auto solver_start=std::chrono::steady_clock::now(); - bmc.do_conversion(); + convert_symex_target_equation( + bmc.equation, bmc.prop_conv, get_message_handler()); + bmc.freeze_program_variables(); freeze_guards(); @@ -272,7 +275,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail() switch(run_decision_procedure(bmc.prop_conv)) { case decision_proceduret::resultt::D_UNSATISFIABLE: - bmc.report_success(); + report_success(bmc.ui_message_handler); return safety_checkert::resultt::SAFE; case decision_proceduret::resultt::D_SATISFIABLE: @@ -282,7 +285,14 @@ safety_checkert::resultt fault_localizationt::stop_on_fail() counterexample_beautificationt()( dynamic_cast(bmc.prop_conv), bmc.equation); - bmc.error_trace(); + build_error_trace( + bmc.error_trace, + bmc.ns, + bmc.equation, + bmc.prop_conv, + bmc.ui_message_handler); + output_error_trace( + bmc.error_trace, bmc.ns, bmc.trace_options(), bmc.ui_message_handler); } // localize faults @@ -307,7 +317,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail() break; } - bmc.report_failure(); + report_failure(bmc.ui_message_handler); return safety_checkert::resultt::UNSAFE; default: diff --git a/unit/Makefile b/unit/Makefile index d24a82f5d90..4c436e0b63c 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -88,6 +88,7 @@ testing-utils-clean: BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ ../src/cbmc/bmc$(OBJEXT) \ ../src/cbmc/bmc_cover$(OBJEXT) \ + ../src/cbmc/bmc_util$(OBJEXT) \ ../src/cbmc/cbmc_languages$(OBJEXT) \ ../src/cbmc/cbmc_parse_options$(OBJEXT) \ ../src/cbmc/counterexample_beautification$(OBJEXT) \ From c343989a72ad4f645ba33e8f2341167c9c947374 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 16 Sep 2018 18:22:00 +0100 Subject: [PATCH 2/2] Move bmc_util to goto_checker module --- jbmc/src/jbmc/Makefile | 1 - jbmc/unit/Makefile | 1 - src/cbmc/Makefile | 1 - src/cbmc/all_properties.cpp | 2 +- src/cbmc/bmc.cpp | 2 +- src/cbmc/bmc_cover.cpp | 2 +- src/cbmc/fault_localization.cpp | 3 ++- src/goto-checker/Makefile | 3 ++- src/{cbmc => goto-checker}/bmc_util.cpp | 0 src/{cbmc => goto-checker}/bmc_util.h | 6 +++--- src/goto-checker/module_dependencies.txt | 2 ++ unit/Makefile | 1 - 12 files changed, 12 insertions(+), 12 deletions(-) rename src/{cbmc => goto-checker}/bmc_util.cpp (100%) rename src/{cbmc => goto-checker}/bmc_util.h (92%) diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index c60416ed92a..57eb5ad31e7 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -40,7 +40,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \ ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \ - ../$(CPROVER_DIR)/src/cbmc/bmc_util$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \ diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index c9570574da3..d1e009b831c 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -85,7 +85,6 @@ java-testing-utils-clean: BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \ - $(CPROVER_DIR)/src/cbmc/bmc_util$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 5ba3d3d8e0d..4dec22ee526 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -1,7 +1,6 @@ SRC = all_properties.cpp \ bmc.cpp \ bmc_cover.cpp \ - bmc_util.cpp \ cbmc_languages.cpp \ cbmc_main.cpp \ cbmc_parse_options.cpp \ diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 8b6379adc11..d5a6daeff62 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 54b174d5e67..f3a044ca482 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -24,9 +24,9 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include -#include "bmc_util.h" #include "counterexample_beautification.h" #include "fault_localization.h" diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 24cd4d9ea36..847bd9d00b8 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index 10b01098497..36329a34b03 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -26,7 +26,8 @@ Author: Peter Schrammel #include #include -#include "bmc_util.h" +#include + #include "counterexample_beautification.h" void fault_localizationt::freeze_guards() diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index e68e48d2423..b6d2d98a003 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -1,4 +1,5 @@ -SRC = solver_factory.cpp \ +SRC = bmc_util.cpp \ + solver_factory.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/cbmc/bmc_util.cpp b/src/goto-checker/bmc_util.cpp similarity index 100% rename from src/cbmc/bmc_util.cpp rename to src/goto-checker/bmc_util.cpp diff --git a/src/cbmc/bmc_util.h b/src/goto-checker/bmc_util.h similarity index 92% rename from src/cbmc/bmc_util.h rename to src/goto-checker/bmc_util.h index 0c3ac4f216d..1aa7e74506b 100644 --- a/src/cbmc/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -9,8 +9,8 @@ Author: Daniel Kroening, Peter Schrammel /// \file /// Bounded Model Checking Utilities -#ifndef CPROVER_CBMC_BMC_UTIL_H -#define CPROVER_CBMC_BMC_UTIL_H +#ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H +#define CPROVER_GOTO_CHECKER_BMC_UTIL_H #include @@ -71,4 +71,4 @@ void slice( const optionst &, ui_message_handlert &); -#endif // CPROVER_CBMC_BMC_UTIL_H +#endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H diff --git a/src/goto-checker/module_dependencies.txt b/src/goto-checker/module_dependencies.txt index 0e4c6e86335..c290a452604 100644 --- a/src/goto-checker/module_dependencies.txt +++ b/src/goto-checker/module_dependencies.txt @@ -1,5 +1,7 @@ +cbmc # symex_bmc will be moved next goto-checker goto-programs goto-symex +linking solvers util diff --git a/unit/Makefile b/unit/Makefile index 4c436e0b63c..d24a82f5d90 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -88,7 +88,6 @@ testing-utils-clean: BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ ../src/cbmc/bmc$(OBJEXT) \ ../src/cbmc/bmc_cover$(OBJEXT) \ - ../src/cbmc/bmc_util$(OBJEXT) \ ../src/cbmc/cbmc_languages$(OBJEXT) \ ../src/cbmc/cbmc_parse_options$(OBJEXT) \ ../src/cbmc/counterexample_beautification$(OBJEXT) \