cprover
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/file_util.h>
17 #include <util/json_irep.h>
18 #include <util/options.h>
19 #include <util/xml.h>
20 
22 
23 #include <analyses/ai.h>
25 
26 typedef std::map<unsigned, goto_programt::const_targett> dead_mapt;
27 
29  const goto_programt &goto_program,
30  dead_mapt &dest)
31 {
32  cfg_dominatorst dominators;
33  dominators(goto_program);
34 
35  for(cfg_dominatorst::cfgt::entry_mapt::const_iterator
36  it=dominators.cfg.entry_map.begin();
37  it!=dominators.cfg.entry_map.end();
38  ++it)
39  {
40  const cfg_dominatorst::cfgt::nodet &n=dominators.cfg[it->second];
41  if(n.dominators.empty())
42  dest.insert(std::make_pair(it->first->location_number,
43  it->first));
44  }
45 }
46 
47 static void all_unreachable(
48  const goto_programt &goto_program,
49  dead_mapt &dest)
50 {
51  forall_goto_program_instructions(it, goto_program)
52  if(!it->is_end_function())
53  dest.insert(std::make_pair(it->location_number, it));
54 }
55 
57  const goto_programt &goto_program,
58  const ai_baset &ai,
59  dead_mapt &dest)
60 {
61  forall_goto_program_instructions(it, goto_program)
62  if(ai.abstract_state_before(it)->is_bottom())
63  dest.insert(std::make_pair(it->location_number, it));
64 }
65 
66 static void output_dead_plain(
67  const namespacet &ns,
68  const irep_idt &function_identifier,
69  const goto_programt &goto_program,
70  const dead_mapt &dead_map,
71  std::ostream &os)
72 {
73  os << "\n*** " << function_identifier << " ***\n";
74 
75  for(dead_mapt::const_iterator it=dead_map.begin();
76  it!=dead_map.end();
77  ++it)
78  goto_program.output_instruction(ns, function_identifier, os, *it->second);
79 }
80 
81 static void add_to_xml(
82  const irep_idt &function_identifier,
83  const goto_programt &goto_program,
84  const dead_mapt &dead_map,
85  xmlt &dest)
86 {
87  xmlt &x = dest.new_element("function");
88  x.set_attribute("name", id2string(function_identifier));
89 
90  for(dead_mapt::const_iterator it=dead_map.begin();
91  it!=dead_map.end();
92  ++it)
93  {
94  xmlt &inst = x.new_element("instruction");
95  inst.set_attribute("location_number",
96  std::to_string(it->second->location_number));
97  inst.set_attribute("source_location",
98  it->second->source_location.as_string());
99  }
100  return;
101 }
102 
104 file_name_string_opt(const source_locationt &source_location)
105 {
106  if(source_location.get_file().empty())
107  return nullopt;
108 
109  return concat_dir_file(
110  id2string(source_location.get_working_directory()),
111  id2string(source_location.get_file()));
112 }
113 
114 static void add_to_json(
115  const namespacet &ns,
116  const irep_idt &function_identifier,
117  const goto_programt &goto_program,
118  const dead_mapt &dead_map,
119  json_arrayt &dest)
120 {
121  PRECONDITION(!goto_program.instructions.empty());
122  goto_programt::const_targett end_function=
123  goto_program.instructions.end();
124  --end_function;
125  DATA_INVARIANT(end_function->is_end_function(),
126  "The last instruction in a goto-program must be END_FUNCTION");
127 
128  json_objectt entry{{"function", json_stringt(function_identifier)}};
129  if(auto file_name_opt = file_name_string_opt(end_function->source_location))
130  entry["file"] = json_stringt{*file_name_opt};
131 
132  json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
133 
134  for(dead_mapt::const_iterator it=dead_map.begin();
135  it!=dead_map.end();
136  ++it)
137  {
138  std::ostringstream oss;
139  goto_program.output_instruction(ns, function_identifier, oss, *it->second);
140  std::string s=oss.str();
141 
142  std::string::size_type n=s.find('\n');
143  assert(n!=std::string::npos);
144  s.erase(0, n+1);
145  n=s.find_first_not_of(' ');
146  assert(n!=std::string::npos);
147  s.erase(0, n);
148  assert(!s.empty());
149  s.erase(s.size()-1);
150 
151  // print info for file actually with full path
152  const source_locationt &l=it->second->source_location;
153  json_objectt i_entry{{"sourceLocation", json(l)},
154  {"statement", json_stringt(s)}};
155  dead_ins.push_back(std::move(i_entry));
156  }
157 
158  dest.push_back(std::move(entry));
159 }
160 
162  const goto_modelt &goto_model,
163  const bool json,
164  std::ostream &os)
165 {
166  json_arrayt json_result;
167 
168  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
169 
170  const namespacet ns(goto_model.symbol_table);
171 
172  for(const auto &gf_entry : goto_model.goto_functions.function_map)
173  {
174  if(!gf_entry.second.body_available())
175  continue;
176 
177  const goto_programt &goto_program = gf_entry.second.body;
178  dead_mapt dead_map;
179 
180  const symbolt &decl = ns.lookup(gf_entry.first);
181 
182  // gf_entry.first may be a link-time renamed version, use the
183  // base_name instead; do not list inlined functions
184  if(
185  called.find(decl.base_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 
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 nullopt;
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  // gf_entry.first may be a link-time renamed version, use the
318  // base_name instead; do not list inlined functions
319  if(
320  unreachable == (called.find(decl.base_name) != called.end() ||
321  to_code_type(decl.type).get_inlined()))
322  {
323  continue;
324  }
325 
326  source_locationt first_location=decl.location;
327 
328  source_locationt last_location;
329  if(gf_entry.second.body_available())
330  {
331  const goto_programt &goto_program = gf_entry.second.body;
332 
333  goto_programt::const_targett end_function=
334  goto_program.instructions.end();
335 
336  // find the last instruction with a line number
337  // TODO(tautschnig): #918 will eventually ensure that every instruction
338  // has such
339  do
340  {
341  --end_function;
342  last_location = end_function->source_location;
343  }
344  while(
345  end_function != goto_program.instructions.begin() &&
346  last_location.get_line().empty());
347 
348  if(last_location.get_line().empty())
349  last_location = decl.location;
350  }
351  else
352  // completely ignore functions without a body, both for
353  // reachable and unreachable functions; we could also restrict
354  // this to macros/asm renaming
355  continue;
356 
357  if(options.get_bool_option("json"))
358  {
360  decl.base_name,
361  first_location,
362  last_location,
363  json_result);
364  }
365  else if(options.get_bool_option("xml"))
366  {
368  decl.base_name,
369  first_location,
370  last_location,
371  xml_result);
372  }
373  else
374  {
375  // text or console
376  if(auto file_name_opt = file_name_string_opt(first_location))
377  os << *file_name_opt << ' ';
378  os << decl.base_name;
379  if(auto line_opt = line_string_opt(first_location))
380  os << ' ' << *line_opt;
381  if(auto line_opt = line_string_opt(last_location))
382  os << ' ' << *line_opt;
383  os << '\n';
384  }
385  }
386 
387  if(options.get_bool_option("json") && !json_result.empty())
388  os << json_result << '\n';
389  else if(options.get_bool_option("xml"))
390  os << xml_result << '\n';
391 }
392 
394  const goto_modelt &goto_model,
395  const bool json,
396  std::ostream &os)
397 {
398  optionst options;
399  if(json)
400  options.set_option("json", true);
401 
402  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
403 
404  list_functions(goto_model, called, options, os, true);
405 }
406 
408  const goto_modelt &goto_model,
409  const bool json,
410  std::ostream &os)
411 {
412  optionst options;
413  if(json)
414  options.set_option("json", true);
415 
416  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
417 
418  list_functions(goto_model, called, options, os, false);
419 }
420 
421 std::unordered_set<irep_idt> compute_called_functions_from_ai(
422  const goto_modelt &goto_model,
423  const ai_baset &ai)
424 {
425  std::unordered_set<irep_idt> called;
426 
427  for(const auto &gf_entry : goto_model.goto_functions.function_map)
428  {
429  if(!gf_entry.second.body_available())
430  continue;
431 
432  const goto_programt &p = gf_entry.second.body;
433 
434  if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
435  called.insert(gf_entry.first);
436  }
437 
438  return called;
439 }
440 
442  const goto_modelt &goto_model,
443  const ai_baset &ai,
444  const optionst &options,
445  std::ostream &out)
446 {
447  std::unordered_set<irep_idt> called =
448  compute_called_functions_from_ai(goto_model, ai);
449 
450  list_functions(goto_model, called, options, out, true);
451 
452  return false;
453 }
454 
456  const goto_modelt &goto_model,
457  const ai_baset &ai,
458  const optionst &options,
459  std::ostream &out)
460 {
461  std::unordered_set<irep_idt> called =
462  compute_called_functions_from_ai(goto_model, ai);
463 
464  list_functions(goto_model, called, options, out, false);
465 
466  return false;
467 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
json_numbert
Definition: json.h:291
json_arrayt::empty
bool empty() const
Definition: json.h:207
add_to_json
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)
Definition: unreachable_instructions.cpp:114
static_unreachable_instructions
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:206
file_util.h
optionst
Definition: options.h:23
dead_mapt
std::map< unsigned, goto_programt::const_targett > dead_mapt
Definition: unreachable_instructions.cpp:26
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
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:223
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
all_unreachable
static void all_unreachable(const goto_programt &goto_program, dead_mapt &dest)
Definition: unreachable_instructions.cpp:47
options.h
Options.
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
xml_output_function
static void xml_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, xmlt &dest)
Definition: unreachable_instructions.cpp:282
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
add_to_xml
static void add_to_xml(const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest)
Definition: unreachable_instructions.cpp:81
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
xml.h
json_irep.h
Util.
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:45
json_arrayt
Definition: json.h:165
cfg_dominators.h
Compute dominators for CFG of goto_function.
compute_called_functions
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
Definition: compute_called_functions.cpp:88
json_objectt
Definition: json.h:300
list_functions
static void list_functions(const goto_modelt &goto_model, const std::unordered_set< irep_idt > &called, const optionst &options, std::ostream &os, bool unreachable)
Definition: unreachable_instructions.cpp:299
reachable_functions
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:407
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
build_dead_map_from_ai
static void build_dead_map_from_ai(const goto_programt &goto_program, const ai_baset &ai, dead_mapt &dest)
Definition: unreachable_instructions.cpp:56
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
unreachable_functions
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:393
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
line_string_opt
static optionalt< std::string > line_string_opt(const source_locationt &source_location)
Definition: unreachable_instructions.cpp:255
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:47
concat_dir_file
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:159
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:116
unreachable_instructions.h
List all unreachable instructions.
dstringt::empty
bool empty() const
Definition: dstring.h:88
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
ai.h
Abstract Interpretation.
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
xmlt
Definition: xml.h:21
unreachable_instructions
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
Definition: unreachable_instructions.cpp:28
source_locationt
Definition: source_location.h:19
compute_called_functions_from_ai
std::unordered_set< irep_idt > compute_called_functions_from_ai(const goto_modelt &goto_model, const ai_baset &ai)
Definition: unreachable_instructions.cpp:421
cfg_baset::entry_map
entry_mapt entry_map
Definition: cfg.h:152
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
file_name_string_opt
static optionalt< std::string > file_name_string_opt(const source_locationt &source_location)
Definition: unreachable_instructions.cpp:104
output_dead_plain
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)
Definition: unreachable_instructions.cpp:66
cfg_baset< nodet, const goto_programt, goto_programt::const_targett >::nodet
base_grapht::nodet nodet
Definition: cfg.h:92
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
static_reachable_functions
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:455
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:665
json_output_function
static void json_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest)
Definition: unreachable_instructions.cpp:265
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:35
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
compute_called_functions.h
Query Called Functions.
static_unreachable_functions
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Definition: unreachable_instructions.cpp:441
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
source_locationt::get_working_directory
const irep_idt & get_working_directory() const
Definition: source_location.h:40
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
cfg_dominators_templatet::cfg
cfgt cfg
Definition: cfg_dominators.h:47
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1255
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false >
json_stringt
Definition: json.h:270