diff --git a/regression/goto-analyzer/show-on-source/main.c b/regression/goto-analyzer/show-on-source/main.c new file mode 100644 index 00000000000..159b8257326 --- /dev/null +++ b/regression/goto-analyzer/show-on-source/main.c @@ -0,0 +1,12 @@ +int i = 1; + +int main() +{ + int j; + _Bool nondet; + + if(j >= 1 && j <= 10) + { + i++; + } +} diff --git a/regression/goto-analyzer/show-on-source/main.desc b/regression/goto-analyzer/show-on-source/main.desc new file mode 100644 index 00000000000..269485ca11f --- /dev/null +++ b/regression/goto-analyzer/show-on-source/main.desc @@ -0,0 +1,10 @@ +CORE +main.c +--intervals --show-on-source +^EXIT=0$ +^SIGNAL=0$ +^ if\(j >= 1 && j <= 10\)$ +^ 1 <= i <= 1$ +^ 1 <= main::1::j <= 10$ +-- +^warning: ignoring diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index 2d4a9d99785..6e69ea1ce93 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -3,6 +3,7 @@ SRC = goto_analyzer_main.cpp \ taint_analysis.cpp \ taint_parser.cpp \ unreachable_instructions.cpp \ + show_on_source.cpp \ static_show_domain.cpp \ static_simplifier.cpp \ static_verifier.cpp \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index cc392a93697..1cdaace76ee 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -57,11 +57,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "taint_analysis.h" -#include "unreachable_instructions.h" +#include "show_on_source.h" #include "static_show_domain.h" #include "static_simplifier.h" #include "static_verifier.h" +#include "taint_analysis.h" +#include "unreachable_instructions.h" goto_analyzer_parse_optionst::goto_analyzer_parse_optionst( int argc, @@ -191,6 +192,11 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("show", true); options.set_option("general-analysis", true); } + else if(cmdline.isset("show-on-source")) + { + options.set_option("show-on-source", true); + options.set_option("general-analysis", true); + } else if(cmdline.isset("verify")) { options.set_option("verify", true); @@ -629,6 +635,11 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) static_show_domain(goto_model, *analyzer, options, out); return CPROVER_EXIT_SUCCESS; } + else if(options.get_bool_option("show-on-source")) + { + show_on_source(goto_model, *analyzer, get_message_handler()); + return CPROVER_EXIT_SUCCESS; + } else if(options.get_bool_option("verify")) { result = static_verifier(goto_model, @@ -800,7 +811,8 @@ void goto_analyzer_parse_optionst::help() " goto-analyzer file.c ... source file names\n" "\n" "Task options:\n" - " --show display the abstract domains\n" + " --show display the abstract states on the goto program\n" // NOLINT(*) + " --show-on-source display the abstract states on the source\n" // NOLINTNEXTLINE(whitespace/line_length) " --verify use the abstract domains to check assertions\n" // NOLINTNEXTLINE(whitespace/line_length) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 9392ab2e7f8..64c8f949977 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -146,6 +146,7 @@ class optionst; "(constants)" \ "(dependence-graph)" \ "(show)(verify)(simplify):" \ + "(show-on-source)" \ "(location-sensitive)(concurrent)" \ "(no-simplify-slicing)" \ // clang-format on diff --git a/src/goto-analyzer/show_on_source.cpp b/src/goto-analyzer/show_on_source.cpp new file mode 100644 index 00000000000..15f3ed13553 --- /dev/null +++ b/src/goto-analyzer/show_on_source.cpp @@ -0,0 +1,145 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "show_on_source.h" + +#include +#include +#include + +#include + +#include + +/// get the name of the file referred to at a location loc, +/// if any +static optionalt +show_location(const ai_baset &ai, ai_baset::locationt loc) +{ + const auto abstract_state = ai.abstract_state_before(loc); + if(abstract_state->is_top()) + return {}; + + if(loc->source_location.get_line().empty()) + return {}; + + return loc->source_location.full_path(); +} + +/// get the source files with non-top abstract states +static std::set +get_source_files(const goto_modelt &goto_model, const ai_baset &ai) +{ + std::set files; + + for(const auto &f : goto_model.goto_functions.function_map) + { + forall_goto_program_instructions(i_it, f.second.body) + { + const auto file = show_location(ai, i_it); + if(file.has_value()) + files.insert(file.value()); + } + } + + return files; +} + +/// print a string with indent to match given sample line +static void print_with_indent( + const std::string &src, + const std::string &indent_line, + std::ostream &out) +{ + const std::size_t p = indent_line.find_first_not_of(" \t"); + const std::string indent = + p == std::string::npos ? std::string("") : std::string(indent_line, 0, p); + std::istringstream in(src); + std::string src_line; + while(std::getline(in, src_line)) + out << indent << src_line << '\n'; +} + +/// output source code annotated with abstract states for given file +void show_on_source( + const std::string &source_file, + const goto_modelt &goto_model, + const ai_baset &ai, + message_handlert &message_handler) +{ +#ifdef _MSC_VER + std::ifstream in(widen(source_file)); +#else + std::ifstream in(source_file); +#endif + + messaget message(message_handler); + + if(!in) + { + message.warning() << "Failed to open `" << source_file << "'" + << messaget::eom; + return; + } + + std::map line_map; + + // Collect line numbers with non-top abstract states. + // We pick the _first_ state for each line. + for(const auto &f : goto_model.goto_functions.function_map) + { + forall_goto_program_instructions(i_it, f.second.body) + { + const auto file = show_location(ai, i_it); + if(file.has_value() && file.value() == source_file) + { + const std::size_t line_no = + stoull(id2string(i_it->source_location.get_line())); + if(line_map.find(line_no) == line_map.end()) + line_map[line_no] = i_it; + } + } + } + + // now print file to message handler + const namespacet ns(goto_model.symbol_table); + + std::string line; + for(std::size_t line_no = 1; std::getline(in, line); line_no++) + { + const auto map_it = line_map.find(line_no); + if(map_it != line_map.end()) + { + auto abstract_state = ai.abstract_state_before(map_it->second); + std::ostringstream state_str; + abstract_state->output(state_str, ai, ns); + if(!state_str.str().empty()) + { + message.result() << messaget::blue; + print_with_indent(state_str.str(), line, message.result()); + message.result() << messaget::reset; + } + } + + message.result() << line << messaget::eom; + } +} + +/// output source code annotated with abstract states +void show_on_source( + const goto_modelt &goto_model, + const ai_baset &ai, + message_handlert &message_handler) +{ + // first gather the source files that have something to show + const auto source_files = get_source_files(goto_model, ai); + + // now show file-by-file + for(const auto &source_file : source_files) + show_on_source(source_file, goto_model, ai, message_handler); +} diff --git a/src/goto-analyzer/show_on_source.h b/src/goto-analyzer/show_on_source.h new file mode 100644 index 00000000000..80a4cdafe4b --- /dev/null +++ b/src/goto-analyzer/show_on_source.h @@ -0,0 +1,18 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_SHOW_ON_SOURCE_H +#define CPROVER_GOTO_ANALYZER_SHOW_ON_SOURCE_H + +class ai_baset; +class goto_modelt; +class message_handlert; + +void show_on_source(const goto_modelt &, const ai_baset &, message_handlert &); + +#endif // CPROVER_GOTO_ANALYZER_SHOW_ON_SOURCE_H