diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index c809c097033..ebd1447c5bb 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -45,7 +45,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \ - ../$(CPROVER_DIR)/src/cbmc/show_vcc$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \ # Empty last line diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 25e3afac7dd..cf0b1200aa3 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -66,7 +66,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \ - $(CPROVER_DIR)/src/cbmc/show_vcc$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \ diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index e6851ecd196..f57389ca16a 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -8,7 +8,6 @@ SRC = all_properties.cpp \ cbmc_solvers.cpp \ counterexample_beautification.cpp \ fault_localization.cpp \ - show_vcc.cpp \ symex_bmc.cpp \ symex_coverage.cpp \ xml_interface.cpp \ diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 9796257f8de..9a01fa233ec 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -293,7 +294,7 @@ safety_checkert::resultt bmct::execute( if(options.get_bool_option("show-vcc")) { - show_vcc(); + show_vcc(options, get_message_handler(), ui, ns, equation); return safety_checkert::resultt::SAFE; // to indicate non-error } @@ -419,7 +420,7 @@ void bmct::show() { if(options.get_bool_option("show-vcc")) { - show_vcc(); + show_vcc(options, get_message_handler(), ui, ns, equation); } if(options.get_bool_option("program-only")) diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 356fcf5250c..91cc217a85d 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -199,10 +199,6 @@ class bmct:public safety_checkert virtual void freeze_program_variables(); - virtual void show_vcc(); - virtual void show_vcc_plain(std::ostream &out); - virtual void show_vcc_json(std::ostream &out); - trace_optionst trace_options() { return trace_optionst(options); diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp deleted file mode 100644 index b50eb3df2f6..00000000000 --- a/src/cbmc/show_vcc.cpp +++ /dev/null @@ -1,180 +0,0 @@ -/*******************************************************************\ - -Module: Symbolic Execution of ANSI-C - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Symbolic Execution of ANSI-C - -#include "bmc.h" - -#include -#include - -#include -#include - -#include -#include - -void bmct::show_vcc_plain(std::ostream &out) -{ - bool has_threads=equation.has_threads(); - bool first=true; - - for(symex_target_equationt::SSA_stepst::iterator - s_it=equation.SSA_steps.begin(); - s_it!=equation.SSA_steps.end(); - s_it++) - { - if(!s_it->is_assert()) - continue; - - if(first) - first=false; - else - out << '\n'; - - if(s_it->source.pc->source_location.is_not_nil()) - out << s_it->source.pc->source_location << "\n"; - - if(s_it->comment!="") - out << s_it->comment << "\n"; - - symex_target_equationt::SSA_stepst::const_iterator - p_it=equation.SSA_steps.begin(); - - // we show everything in case there are threads - symex_target_equationt::SSA_stepst::const_iterator - last_it=has_threads?equation.SSA_steps.end():s_it; - - for(std::size_t count=1; p_it!=last_it; p_it++) - if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) - { - if(!p_it->ignore) - { - std::string string_value= - from_expr(ns, p_it->source.pc->function, p_it->cond_expr); - out << "{-" << count << "} " << string_value << "\n"; - - #if 0 - languages.from_expr(p_it->guard_expr, string_value); - out << "GUARD: " << string_value << "\n"; - out << "\n"; - #endif - - count++; - } - } - - // Unicode equivalent of "|--------------------------" - out << u8"\u251c"; - for(unsigned i=0; i<26; i++) out << u8"\u2500"; - out << '\n'; - - std::string string_value= - from_expr(ns, s_it->source.pc->function, s_it->cond_expr); - out << "{" << 1 << "} " << string_value << "\n"; - } -} - -void bmct::show_vcc_json(std::ostream &out) -{ - json_objectt json_result; - - json_arrayt &json_vccs=json_result["vccs"].make_array(); - - bool has_threads=equation.has_threads(); - - for(symex_target_equationt::SSA_stepst::iterator - s_it=equation.SSA_steps.begin(); - s_it!=equation.SSA_steps.end(); - s_it++) - { - if(!s_it->is_assert()) - continue; - - // vcc object - json_objectt &object=json_vccs.push_back(jsont()).make_object(); - - const source_locationt &source_location=s_it->source.pc->source_location; - if(source_location.is_not_nil()) - object["sourceLocation"]=json(source_location); - - const std::string &s=s_it->comment; - if(!s.empty()) - object["comment"]=json_stringt(s); - - // we show everything in case there are threads - symex_target_equationt::SSA_stepst::const_iterator - last_it=has_threads?equation.SSA_steps.end():s_it; - - json_arrayt &json_constraints=object["constraints"].make_array(); - - for(symex_target_equationt::SSA_stepst::const_iterator p_it - =equation.SSA_steps.begin(); - p_it!=last_it; p_it++) - { - if((p_it->is_assume() || - p_it->is_assignment() || - p_it->is_constraint()) && - !p_it->ignore) - { - std::string string_value= - from_expr(ns, p_it->source.pc->function, p_it->cond_expr); - json_constraints.push_back(json_stringt(string_value)); - } - } - - std::string string_value= - from_expr(ns, s_it->source.pc->function, s_it->cond_expr); - object["expression"]=json_stringt(string_value); - } - - out << ",\n" << json_result; -} - -void bmct::show_vcc() -{ - const std::string &filename=options.get_option("outfile"); - bool have_file=!filename.empty() && filename!="-"; - - std::ofstream of; - - if(have_file) - { - of.open(filename); - if(!of) - throw "failed to open file "+filename; - } - - std::ostream &out=have_file?of:std::cout; - - switch(ui) - { - case ui_message_handlert::uit::XML_UI: - error() << "XML UI not supported" << eom; - return; - - case ui_message_handlert::uit::JSON_UI: - show_vcc_json(out); - break; - - case ui_message_handlert::uit::PLAIN: - status() << "VERIFICATION CONDITIONS:\n" << eom; - if(have_file) - show_vcc_plain(out); - else - { - show_vcc_plain(status()); - status() << eom; - } - break; - } - - if(have_file) - of.close(); -} diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index 9e86b60e8f9..c95cd1ff2f3 100644 --- a/src/goto-symex/Makefile +++ b/src/goto-symex/Makefile @@ -12,6 +12,7 @@ SRC = auto_objects.cpp \ precondition.cpp \ rewrite_union.cpp \ show_program.cpp \ + show_vcc.cpp \ slice.cpp \ slice_by_trace.cpp \ symex_assign.cpp \ diff --git a/src/goto-symex/show_vcc.cpp b/src/goto-symex/show_vcc.cpp new file mode 100644 index 00000000000..6116759b66c --- /dev/null +++ b/src/goto-symex/show_vcc.cpp @@ -0,0 +1,197 @@ +/*******************************************************************\ + +Module: Output of the verification conditions (VCCs) + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Output of the verification conditions (VCCs) + +#include "show_vcc.h" + +#include +#include + +#include + +#include +#include + +#include +#include +#include + +void show_vcc_plain( + std::ostream &out, + const namespacet &ns, + const symex_target_equationt &equation) +{ + bool has_threads = equation.has_threads(); + bool first = true; + + for(symex_target_equationt::SSA_stepst::const_iterator s_it = + equation.SSA_steps.begin(); + s_it != equation.SSA_steps.end(); + s_it++) + { + if(!s_it->is_assert()) + continue; + + if(first) + first = false; + else + out << '\n'; + + if(s_it->source.pc->source_location.is_not_nil()) + out << s_it->source.pc->source_location << "\n"; + + if(s_it->comment != "") + out << s_it->comment << "\n"; + + symex_target_equationt::SSA_stepst::const_iterator p_it = + equation.SSA_steps.begin(); + + // we show everything in case there are threads + symex_target_equationt::SSA_stepst::const_iterator last_it = + has_threads ? equation.SSA_steps.end() : s_it; + + for(std::size_t count = 1; p_it != last_it; p_it++) + if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) + { + if(!p_it->ignore) + { + std::string string_value = + from_expr(ns, p_it->source.pc->function, p_it->cond_expr); + out << "{-" << count << "} " << string_value << "\n"; + +#if 0 + languages.from_expr(p_it->guard_expr, string_value); + out << "GUARD: " << string_value << "\n"; + out << "\n"; +#endif + + count++; + } + } + + // Unicode equivalent of "|--------------------------" + out << u8"\u251c"; + for(unsigned i = 0; i < 26; i++) + out << u8"\u2500"; + out << '\n'; + + std::string string_value = + from_expr(ns, s_it->source.pc->function, s_it->cond_expr); + out << "{" << 1 << "} " << string_value << "\n"; + } +} + +void show_vcc_json( + std::ostream &out, + const namespacet &ns, + const symex_target_equationt &equation) +{ + json_objectt json_result; + + json_arrayt &json_vccs = json_result["vccs"].make_array(); + + bool has_threads = equation.has_threads(); + + for(symex_target_equationt::SSA_stepst::const_iterator s_it = + equation.SSA_steps.begin(); + s_it != equation.SSA_steps.end(); + s_it++) + { + if(!s_it->is_assert()) + continue; + + // vcc object + json_objectt &object = json_vccs.push_back(jsont()).make_object(); + + const source_locationt &source_location = s_it->source.pc->source_location; + if(source_location.is_not_nil()) + object["sourceLocation"] = json(source_location); + + const std::string &s = s_it->comment; + if(!s.empty()) + object["comment"] = json_stringt(s); + + // we show everything in case there are threads + symex_target_equationt::SSA_stepst::const_iterator last_it = + has_threads ? equation.SSA_steps.end() : s_it; + + json_arrayt &json_constraints = object["constraints"].make_array(); + + for(symex_target_equationt::SSA_stepst::const_iterator p_it = + equation.SSA_steps.begin(); + p_it != last_it; + p_it++) + { + if( + (p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) && + !p_it->ignore) + { + std::string string_value = + from_expr(ns, p_it->source.pc->function, p_it->cond_expr); + json_constraints.push_back(json_stringt(string_value)); + } + } + + std::string string_value = + from_expr(ns, s_it->source.pc->function, s_it->cond_expr); + object["expression"] = json_stringt(string_value); + } + + out << ",\n" << json_result; +} + +void show_vcc( + const optionst &options, + message_handlert &message_handler, + ui_message_handlert::uit ui, + const namespacet &ns, + const symex_target_equationt &equation) +{ + messaget msg(message_handler); + + const std::string &filename = options.get_option("outfile"); + bool have_file = !filename.empty() && filename != "-"; + + std::ofstream of; + + if(have_file) + { + of.open(filename); + if(!of) + throw "failed to open file " + filename; + } + + std::ostream &out = have_file ? of : std::cout; + + switch(ui) + { + case ui_message_handlert::uit::XML_UI: + msg.error() << "XML UI not supported" << messaget::eom; + return; + + case ui_message_handlert::uit::JSON_UI: + show_vcc_json(out, ns, equation); + break; + + case ui_message_handlert::uit::PLAIN: + msg.status() << "VERIFICATION CONDITIONS:\n" << messaget::eom; + if(have_file) + show_vcc_plain(out, ns, equation); + else + { + show_vcc_plain(msg.status(), ns, equation); + msg.status() << messaget::eom; + } + break; + } + + if(have_file) + of.close(); +} diff --git a/src/goto-symex/show_vcc.h b/src/goto-symex/show_vcc.h new file mode 100644 index 00000000000..da3fe20a7aa --- /dev/null +++ b/src/goto-symex/show_vcc.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: Output of the verification conditions (VCCs) + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Output of the verification conditions (VCCs) + +#ifndef CPROVER_GOTO_SYMEX_SHOW_VCC_H +#define CPROVER_GOTO_SYMEX_SHOW_VCC_H + +#include + +class namespacet; +class optionst; +class symex_target_equationt; + +void show_vcc( + const optionst &options, + message_handlert &message_handler, + ui_message_handlert::uit ui, + const namespacet &ns, + const symex_target_equationt &equation); + +#endif // CPROVER_GOTO_SYMEX_SHOW_VCC_H diff --git a/unit/Makefile b/unit/Makefile index 488f61d1975..8b63c27bf7c 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -68,7 +68,6 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ ../src/cbmc/cbmc_solvers$(OBJEXT) \ ../src/cbmc/counterexample_beautification$(OBJEXT) \ ../src/cbmc/fault_localization$(OBJEXT) \ - ../src/cbmc/show_vcc$(OBJEXT) \ ../src/cbmc/symex_bmc$(OBJEXT) \ ../src/cbmc/symex_coverage$(OBJEXT) \ ../src/cbmc/xml_interface$(OBJEXT) \