CBMC
unreachable_instructions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: List all unreachable instructions
4 
5 Author: Michael Tautschnig
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
13 
15 
16 #include <util/json_irep.h>
17 #include <util/options.h>
18 #include <util/xml.h>
19 
21 
22 #include <analyses/ai.h>
24 
25 #include <filesystem>
26 
27 typedef std::map<unsigned, goto_programt::const_targett> dead_mapt;
28 
30  const goto_programt &goto_program,
31  dead_mapt &dest)
32 {
33  cfg_dominatorst dominators;
34  dominators(goto_program);
35 
36  for(cfg_dominatorst::cfgt::entry_mapt::const_iterator
37  it=dominators.cfg.entry_map.begin();
38  it!=dominators.cfg.entry_map.end();
39  ++it)
40  {
41  const cfg_dominatorst::cfgt::nodet &n=dominators.cfg[it->second];
42  if(n.dominators.empty())
43  dest.insert(std::make_pair(it->first->location_number,
44  it->first));
45  }
46 }
47 
48 static void all_unreachable(
49  const goto_programt &goto_program,
50  dead_mapt &dest)
51 {
52  forall_goto_program_instructions(it, goto_program)
53  if(!it->is_end_function())
54  dest.insert(std::make_pair(it->location_number, it));
55 }
56 
58  const goto_programt &goto_program,
59  const ai_baset &ai,
60  dead_mapt &dest)
61 {
62  forall_goto_program_instructions(it, goto_program)
63  if(ai.abstract_state_before(it)->is_bottom())
64  dest.insert(std::make_pair(it->location_number, it));
65 }
66 
67 static void output_dead_plain(
68  const namespacet &ns,
69  const irep_idt &function_identifier,
70  const goto_programt &goto_program,
71  const dead_mapt &dead_map,
72  std::ostream &os)
73 {
74  os << "\n*** " << function_identifier << " ***\n";
75 
76  for(dead_mapt::const_iterator it=dead_map.begin();
77  it!=dead_map.end();
78  ++it)
79  it->second->output(os);
80 }
81 
82 static void add_to_xml(
83  const irep_idt &function_identifier,
84  const goto_programt &goto_program,
85  const dead_mapt &dead_map,
86  xmlt &dest)
87 {
88  xmlt &x = dest.new_element("function");
89  x.set_attribute("name", id2string(function_identifier));
90 
91  for(dead_mapt::const_iterator it=dead_map.begin();
92  it!=dead_map.end();
93  ++it)
94  {
95  xmlt &inst = x.new_element("instruction");
96  inst.set_attribute("location_number",
97  std::to_string(it->second->location_number));
98  inst.set_attribute(
99  "source_location", it->second->source_location().as_string());
100  }
101  return;
102 }
103 
104 static std::optional<std::string>
105 file_name_string_opt(const source_locationt &source_location)
106 {
107  if(source_location.get_file().empty())
108  return {};
109 
110  return std::filesystem::path(
111  id2string(source_location.get_working_directory()))
112  .append(id2string(source_location.get_file()))
113  .string();
114 }
115 
116 static void add_to_json(
117  const namespacet &ns,
118  const irep_idt &function_identifier,
119  const goto_programt &goto_program,
120  const dead_mapt &dead_map,
121  json_arrayt &dest)
122 {
123  PRECONDITION(!goto_program.instructions.empty());
124  goto_programt::const_targett end_function=
125  goto_program.instructions.end();
126  --end_function;
127  DATA_INVARIANT(end_function->is_end_function(),
128  "The last instruction in a goto-program must be END_FUNCTION");
129 
130  json_objectt entry{{"function", json_stringt(function_identifier)}};
131  if(auto file_name_opt = file_name_string_opt(end_function->source_location()))
132  entry["file"] = json_stringt{*file_name_opt};
133 
134  json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
135 
136  for(dead_mapt::const_iterator it=dead_map.begin();
137  it!=dead_map.end();
138  ++it)
139  {
140  std::ostringstream oss;
141  it->second->output(oss);
142  std::string s=oss.str();
143 
144  std::string::size_type n=s.find('\n');
145  CHECK_RETURN(n != std::string::npos);
146  s.erase(0, n+1);
147  n=s.find_first_not_of(' ');
148  CHECK_RETURN(n != std::string::npos);
149  s.erase(0, n);
150  CHECK_RETURN(!s.empty());
151  s.erase(s.size()-1);
152 
153  // print info for file actually with full path
154  const source_locationt &l = it->second->source_location();
155  json_objectt i_entry{{"sourceLocation", json(l)},
156  {"statement", json_stringt(s)}};
157  dead_ins.push_back(std::move(i_entry));
158  }
159 
160  dest.push_back(std::move(entry));
161 }
162 
164  const goto_modelt &goto_model,
165  const bool json,
166  std::ostream &os)
167 {
168  json_arrayt json_result;
169 
170  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
171 
172  const namespacet ns(goto_model.symbol_table);
173 
174  for(const auto &gf_entry : goto_model.goto_functions.function_map)
175  {
176  if(!gf_entry.second.body_available())
177  continue;
178 
179  const goto_programt &goto_program = gf_entry.second.body;
180  dead_mapt dead_map;
181 
182  const symbolt &decl = ns.lookup(gf_entry.first);
183 
184  if(
185  called.find(decl.name) != called.end() ||
186  to_code_type(decl.type).get_inlined())
187  {
188  unreachable_instructions(goto_program, dead_map);
189  }
190  else
191  all_unreachable(goto_program, dead_map);
192 
193  if(!dead_map.empty())
194  {
195  if(!json)
196  output_dead_plain(ns, gf_entry.first, goto_program, dead_map, os);
197  else
198  add_to_json(ns, gf_entry.first, goto_program, dead_map, json_result);
199  }
200  }
201 
202  if(json && !json_result.empty())
203  os << json_result << '\n';
204 }
205 
207  const goto_modelt &goto_model,
208  const ai_baset &ai,
209  const optionst &options,
210  std::ostream &out)
211 {
212  json_arrayt json_result;
213  xmlt xml_result("unreachable-instructions");
214 
215  const namespacet ns(goto_model.symbol_table);
216 
217  for(const auto &gf_entry : goto_model.goto_functions.function_map)
218  {
219  if(!gf_entry.second.body_available())
220  continue;
221 
222  const goto_programt &goto_program = gf_entry.second.body;
223  dead_mapt dead_map;
224  build_dead_map_from_ai(goto_program, ai, dead_map);
225 
226  if(!dead_map.empty())
227  {
228  if(options.get_bool_option("json"))
229  {
230  add_to_json(
231  ns, gf_entry.first, gf_entry.second.body, dead_map, json_result);
232  }
233  else if(options.get_bool_option("xml"))
234  {
235  add_to_xml(gf_entry.first, gf_entry.second.body, dead_map, xml_result);
236  }
237  else
238  {
239  // text or console
241  ns, gf_entry.first, gf_entry.second.body, dead_map, out);
242  }
243  }
244  }
245 
246  if(options.get_bool_option("json") && !json_result.empty())
247  out << json_result << '\n';
248  else if(options.get_bool_option("xml"))
249  out << xml_result << '\n';
250 
251  return false;
252 }
253 
254 static std::optional<std::string>
255 line_string_opt(const source_locationt &source_location)
256 {
257  const irep_idt &line = source_location.get_line();
258 
259  if(line.empty())
260  return {};
261  else
262  return id2string(line);
263 }
264 
266  const irep_idt &function,
267  const source_locationt &first_location,
268  const source_locationt &last_location,
269  json_arrayt &dest)
270 {
271  json_objectt entry{{"function", json_stringt(function)}};
272  if(auto file_name_opt = file_name_string_opt(first_location))
273  entry["file"] = json_stringt{*file_name_opt};
274  if(auto line_opt = line_string_opt(first_location))
275  entry["firstLine"] = json_numbert{*line_opt};
276  if(auto line_opt = line_string_opt(last_location))
277  entry["lastLine"] = json_numbert{*line_opt};
278 
279  dest.push_back(std::move(entry));
280 }
281 
283  const irep_idt &function,
284  const source_locationt &first_location,
285  const source_locationt &last_location,
286  xmlt &dest)
287 {
288  xmlt &x=dest.new_element("function");
289 
290  x.set_attribute("name", id2string(function));
291  if(auto file_name_opt = file_name_string_opt(first_location))
292  x.set_attribute("file", *file_name_opt);
293  if(auto line_opt = line_string_opt(first_location))
294  x.set_attribute("first_line", *line_opt);
295  if(auto line_opt = line_string_opt(last_location))
296  x.set_attribute("last_line", *line_opt);
297 }
298 
299 static void list_functions(
300  const goto_modelt &goto_model,
301  const std::unordered_set<irep_idt> &called,
302  const optionst &options,
303  std::ostream &os,
304  bool unreachable)
305 {
306  json_arrayt json_result;
307  xmlt xml_result(unreachable ?
308  "unreachable-functions" :
309  "reachable-functions");
310 
311  const namespacet ns(goto_model.symbol_table);
312 
313  for(const auto &gf_entry : goto_model.goto_functions.function_map)
314  {
315  const symbolt &decl = ns.lookup(gf_entry.first);
316 
317  if(
318  unreachable == (called.find(decl.name) != called.end() ||
319  to_code_type(decl.type).get_inlined()))
320  {
321  continue;
322  }
323 
324  source_locationt first_location=decl.location;
325 
326  source_locationt last_location;
327  if(gf_entry.second.body_available())
328  {
329  const goto_programt &goto_program = gf_entry.second.body;
330 
331  goto_programt::const_targett end_function=
332  goto_program.instructions.end();
333 
334  // find the last instruction with a line number
335  // TODO(tautschnig): #918 will eventually ensure that every instruction
336  // has such
337  do
338  {
339  --end_function;
340  last_location = end_function->source_location();
341  }
342  while(
343  end_function != goto_program.instructions.begin() &&
344  last_location.get_line().empty());
345 
346  if(last_location.get_line().empty())
347  last_location = decl.location;
348  }
349  else
350  // completely ignore functions without a body, both for
351  // reachable and unreachable functions; we could also restrict
352  // this to macros/asm renaming
353  continue;
354 
355  if(options.get_bool_option("json"))
356  {
358  decl.base_name,
359  first_location,
360  last_location,
361  json_result);
362  }
363  else if(options.get_bool_option("xml"))
364  {
366  decl.base_name,
367  first_location,
368  last_location,
369  xml_result);
370  }
371  else
372  {
373  // text or console
374  if(auto file_name_opt = file_name_string_opt(first_location))
375  os << *file_name_opt << ' ';
376  os << decl.base_name;
377  if(auto line_opt = line_string_opt(first_location))
378  os << ' ' << *line_opt;
379  if(auto line_opt = line_string_opt(last_location))
380  os << ' ' << *line_opt;
381  os << '\n';
382  }
383  }
384 
385  if(options.get_bool_option("json") && !json_result.empty())
386  os << json_result << '\n';
387  else if(options.get_bool_option("xml"))
388  os << xml_result << '\n';
389 }
390 
392  const goto_modelt &goto_model,
393  const bool json,
394  std::ostream &os)
395 {
396  optionst options;
397  if(json)
398  options.set_option("json", true);
399 
400  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
401 
402  list_functions(goto_model, called, options, os, true);
403 }
404 
406  const goto_modelt &goto_model,
407  const bool json,
408  std::ostream &os)
409 {
410  optionst options;
411  if(json)
412  options.set_option("json", true);
413 
414  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
415 
416  list_functions(goto_model, called, options, os, false);
417 }
418 
419 std::unordered_set<irep_idt> compute_called_functions_from_ai(
420  const goto_modelt &goto_model,
421  const ai_baset &ai)
422 {
423  std::unordered_set<irep_idt> called;
424 
425  for(const auto &gf_entry : goto_model.goto_functions.function_map)
426  {
427  if(!gf_entry.second.body_available())
428  continue;
429 
430  const goto_programt &p = gf_entry.second.body;
431 
432  if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
433  called.insert(gf_entry.first);
434  }
435 
436  return called;
437 }
438 
440  const goto_modelt &goto_model,
441  const ai_baset &ai,
442  const optionst &options,
443  std::ostream &out)
444 {
445  std::unordered_set<irep_idt> called =
446  compute_called_functions_from_ai(goto_model, ai);
447 
448  list_functions(goto_model, called, options, out, true);
449 
450  return false;
451 }
452 
454  const goto_modelt &goto_model,
455  const ai_baset &ai,
456  const optionst &options,
457  std::ostream &out)
458 {
459  std::unordered_set<irep_idt> called =
460  compute_called_functions_from_ai(goto_model, ai);
461 
462  list_functions(goto_model, called, options, out, false);
463 
464  return false;
465 }
Abstract Interpretation.
Compute dominators for CFG of goto_function.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:117
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
iterator end()
Definition: cfg.h:118
iterator begin()
Definition: cfg.h:114
entry_mapt entry_map
Definition: cfg.h:152
bool get_inlined() const
Definition: std_types.h:709
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
instructionst::const_iterator const_targett
Definition: goto_program.h:615
jsont & push_back(const jsont &json)
Definition: json.h:212
bool empty() const
Definition: json.h:207
json_arrayt & make_array()
Definition: json.h:418
void output(std::ostream &out) const
Definition: json.h:90
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
const irep_idt & get_working_directory() const
const irep_idt & get_line() const
const irep_idt & get_file() const
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
Definition: xml.h:21
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
xmlt & new_element(const std::string &key)
Definition: xml.h:95
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
Query Called Functions.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
Options.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
#define size_type
Definition: unistd.c:347
static void all_unreachable(const goto_programt &goto_program, dead_mapt &dest)
static std::optional< std::string > line_string_opt(const source_locationt &source_location)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
std::unordered_set< irep_idt > compute_called_functions_from_ai(const goto_modelt &goto_model, const ai_baset &ai)
static void list_functions(const goto_modelt &goto_model, const std::unordered_set< irep_idt > &called, const optionst &options, std::ostream &os, bool unreachable)
static void build_dead_map_from_ai(const goto_programt &goto_program, const ai_baset &ai, dead_mapt &dest)
static void add_to_xml(const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest)
static void xml_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, xmlt &dest)
static void add_to_json(const namespacet &ns, const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, json_arrayt &dest)
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
static std::optional< std::string > file_name_string_opt(const source_locationt &source_location)
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void json_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest)
std::map< unsigned, goto_programt::const_targett > dead_mapt
static void output_dead_plain(const namespacet &ns, const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, std::ostream &os)
List all unreachable instructions.