added show_on_source for abstract domains
The abstract states are shown in a different color on the source code text of the program, as opposed to the goto-program dump. Indentation of the output of the abstract is made to match the indentation of the source code.
This commit is contained in:
parent
f33dc9d51e
commit
5dd37608c1
|
@ -0,0 +1,12 @@
|
|||
int i = 1;
|
||||
|
||||
int main()
|
||||
{
|
||||
int j;
|
||||
_Bool nondet;
|
||||
|
||||
if(j >= 1 && j <= 10)
|
||||
{
|
||||
i++;
|
||||
}
|
||||
}
|
|
@ -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
|
|
@ -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 \
|
||||
|
|
|
@ -57,11 +57,12 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/unicode.h>
|
||||
#include <util/version.h>
|
||||
|
||||
#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)
|
||||
|
|
|
@ -145,7 +145,7 @@ class optionst;
|
|||
"(non-null)(show-non-null)" \
|
||||
"(constants)" \
|
||||
"(dependence-graph)" \
|
||||
"(show)(verify)(simplify):" \
|
||||
"(show)(verify)(simplify):(show-on-source)" \
|
||||
"(location-sensitive)(concurrent)" \
|
||||
"(no-simplify-slicing)" \
|
||||
// clang-format on
|
||||
|
|
|
@ -0,0 +1,145 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: goto-analyzer
|
||||
|
||||
Author: Daniel Kroening, kroening@kroening.com
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
#include "show_on_source.h"
|
||||
|
||||
#include <util/file_util.h>
|
||||
#include <util/message.h>
|
||||
#include <util/unicode.h>
|
||||
|
||||
#include <analyses/ai.h>
|
||||
|
||||
#include <fstream>
|
||||
|
||||
/// get the name of the file referred to at a location loc,
|
||||
/// if any
|
||||
static optionalt<std::string>
|
||||
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<std::string>
|
||||
get_source_files(const goto_modelt &goto_model, const ai_baset &ai)
|
||||
{
|
||||
std::set<std::string> 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<std::size_t, ai_baset::locationt> 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);
|
||||
}
|
|
@ -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
|
Loading…
Reference in New Issue