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 }
#define loc()
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::const_targett locationt
Definition: ai.h:36
std::wstring widen(const char *s)
Definition: unicode.cpp:52
static const commandt blue
render text with blue foreground color
Definition: message.h:342
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
mstreamt & warning() const
Definition: message.h:391
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
nonstd::optional< T > optionalt
Definition: optional.h:35
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
static eomt eom
Definition: message.h:284
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
mstreamt & result() const
Definition: message.h:396
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
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
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
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Definition: kdev_t.h:19