cprover
show_on_source.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: goto-analyzer
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "show_on_source.h"
10 
11 #include <util/file_util.h>
12 #include <util/message.h>
13 #include <util/unicode.h>
14 
15 #include <analyses/ai.h>
16 
17 #include <fstream>
18 
23 {
24  const auto abstract_state = ai.abstract_state_before(loc);
25  if(abstract_state->is_top())
26  return {};
27 
28  if(loc->source_location.get_line().empty())
29  return {};
30 
31  return loc->source_location.full_path();
32 }
33 
35 static std::set<std::string>
36 get_source_files(const goto_modelt &goto_model, const ai_baset &ai)
37 {
38  std::set<std::string> files;
39 
40  for(const auto &f : goto_model.goto_functions.function_map)
41  {
42  forall_goto_program_instructions(i_it, f.second.body)
43  {
44  const auto file = show_location(ai, i_it);
45  if(file.has_value())
46  files.insert(file.value());
47  }
48  }
49 
50  return files;
51 }
52 
54 static void print_with_indent(
55  const std::string &src,
56  const std::string &indent_line,
57  std::ostream &out)
58 {
59  const std::size_t p = indent_line.find_first_not_of(" \t");
60  const std::string indent =
61  p == std::string::npos ? std::string() : std::string(indent_line, 0, p);
62  std::istringstream in(src);
63  std::string src_line;
64  while(std::getline(in, src_line))
65  out << indent << src_line << '\n';
66 }
67 
70  const std::string &source_file,
71  const goto_modelt &goto_model,
72  const ai_baset &ai,
73  message_handlert &message_handler)
74 {
75 #ifdef _MSC_VER
76  std::ifstream in(widen(source_file));
77 #else
78  std::ifstream in(source_file);
79 #endif
80 
81  messaget message(message_handler);
82 
83  if(!in)
84  {
85  message.warning() << "Failed to open '" << source_file << "'"
86  << messaget::eom;
87  return;
88  }
89 
90  std::map<std::size_t, ai_baset::locationt> line_map;
91 
92  // Collect line numbers with non-top abstract states.
93  // We pick the _first_ state for each line.
94  for(const auto &f : goto_model.goto_functions.function_map)
95  {
96  forall_goto_program_instructions(i_it, f.second.body)
97  {
98  const auto file = show_location(ai, i_it);
99  if(file.has_value() && file.value() == source_file)
100  {
101  const std::size_t line_no =
102  stoull(id2string(i_it->source_location.get_line()));
103  if(line_map.find(line_no) == line_map.end())
104  line_map[line_no] = i_it;
105  }
106  }
107  }
108 
109  // now print file to message handler
110  const namespacet ns(goto_model.symbol_table);
111 
112  std::string line;
113  for(std::size_t line_no = 1; std::getline(in, line); line_no++)
114  {
115  const auto map_it = line_map.find(line_no);
116  if(map_it != line_map.end())
117  {
118  auto abstract_state = ai.abstract_state_before(map_it->second);
119  std::ostringstream state_str;
120  abstract_state->output(state_str, ai, ns);
121  if(!state_str.str().empty())
122  {
123  message.result() << messaget::blue;
124  print_with_indent(state_str.str(), line, message.result());
125  message.result() << messaget::reset;
126  }
127  }
128 
129  message.result() << line << messaget::eom;
130  }
131 }
132 
135  const goto_modelt &goto_model,
136  const ai_baset &ai,
137  message_handlert &message_handler)
138 {
139  // first gather the source files that have something to show
140  const auto source_files = get_source_files(goto_model, ai);
141 
142  // now show file-by-file
143  for(const auto &source_file : source_files)
144  show_on_source(source_file, goto_model, ai, message_handler);
145 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
ai_baset::locationt
goto_programt::const_targett locationt
Definition: ai.h:126
file_util.h
get_source_files
static std::set< std::string > get_source_files(const goto_modelt &goto_model, const ai_baset &ai)
get the source files with non-top abstract states
Definition: show_on_source.cpp:36
file
Definition: kdev_t.h:19
goto_modelt
Definition: goto_model.h:26
ai_baset::abstract_state_before
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
Definition: ai.h:221
show_location
static optionalt< std::string > show_location(const ai_baset &ai, ai_baset::locationt loc)
get the name of the file referred to at a location loc, if any
Definition: show_on_source.cpp:22
messaget::eom
static eomt eom
Definition: message.h:297
print_with_indent
static void print_with_indent(const std::string &src, const std::string &indent_line, std::ostream &out)
print a string with indent to match given sample line
Definition: show_on_source.cpp:54
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
message_handlert
Definition: message.h:28
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:50
ai.h
Abstract Interpretation.
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
show_on_source.h
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
unicode.h
show_on_source
void show_on_source(const std::string &source_file, const goto_modelt &goto_model, const ai_baset &ai, message_handlert &message_handler)
output source code annotated with abstract states for given file
Definition: show_on_source.cpp:69
message.h
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
messaget::blue
static const commandt blue
render text with blue foreground color
Definition: message.h:355
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196