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 
103 static void add_to_json(
104  const namespacet &ns,
105  const irep_idt &function_identifier,
106  const goto_programt &goto_program,
107  const dead_mapt &dead_map,
108  json_arrayt &dest)
109 {
110  PRECONDITION(!goto_program.instructions.empty());
111  goto_programt::const_targett end_function=
112  goto_program.instructions.end();
113  --end_function;
114  DATA_INVARIANT(end_function->is_end_function(),
115  "The last instruction in a goto-program must be END_FUNCTION");
116 
117  json_objectt entry{
118  {"function", json_stringt(function_identifier)},
119  {"fileName",
121  id2string(end_function->source_location.get_working_directory()),
122  id2string(end_function->source_location.get_file())))}};
123 
124  json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
125 
126  for(dead_mapt::const_iterator it=dead_map.begin();
127  it!=dead_map.end();
128  ++it)
129  {
130  std::ostringstream oss;
131  goto_program.output_instruction(ns, function_identifier, oss, *it->second);
132  std::string s=oss.str();
133 
134  std::string::size_type n=s.find('\n');
135  assert(n!=std::string::npos);
136  s.erase(0, n+1);
137  n=s.find_first_not_of(' ');
138  assert(n!=std::string::npos);
139  s.erase(0, n);
140  assert(!s.empty());
141  s.erase(s.size()-1);
142 
143  // print info for file actually with full path
144  const source_locationt &l=it->second->source_location;
145  json_objectt i_entry{{"sourceLocation", json(l)},
146  {"statement", json_stringt(s)}};
147  dead_ins.push_back(std::move(i_entry));
148  }
149 
150  dest.push_back(std::move(entry));
151 }
152 
154  const goto_modelt &goto_model,
155  const bool json,
156  std::ostream &os)
157 {
158  json_arrayt json_result;
159 
160  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
161 
162  const namespacet ns(goto_model.symbol_table);
163 
164  for(const auto &gf_entry : goto_model.goto_functions.function_map)
165  {
166  if(!gf_entry.second.body_available())
167  continue;
168 
169  const goto_programt &goto_program = gf_entry.second.body;
170  dead_mapt dead_map;
171 
172  const symbolt &decl = ns.lookup(gf_entry.first);
173 
174  // gf_entry.first may be a link-time renamed version, use the
175  // base_name instead; do not list inlined functions
176  if(
177  called.find(decl.base_name) != called.end() ||
178  to_code_type(decl.type).get_inlined())
179  {
180  unreachable_instructions(goto_program, dead_map);
181  }
182  else
183  all_unreachable(goto_program, dead_map);
184 
185  if(!dead_map.empty())
186  {
187  if(!json)
188  output_dead_plain(ns, gf_entry.first, goto_program, dead_map, os);
189  else
190  add_to_json(ns, gf_entry.first, goto_program, dead_map, json_result);
191  }
192  }
193 
194  if(json && !json_result.empty())
195  os << json_result << '\n';
196 }
197 
199  const goto_modelt &goto_model,
200  const ai_baset &ai,
201  const optionst &options,
202  std::ostream &out)
203 {
204  json_arrayt json_result;
205  xmlt xml_result("unreachable-instructions");
206 
207  const namespacet ns(goto_model.symbol_table);
208 
209  for(const auto &gf_entry : goto_model.goto_functions.function_map)
210  {
211  if(!gf_entry.second.body_available())
212  continue;
213 
214  const goto_programt &goto_program = gf_entry.second.body;
215  dead_mapt dead_map;
216  build_dead_map_from_ai(goto_program, ai, dead_map);
217 
218  if(!dead_map.empty())
219  {
220  if(options.get_bool_option("json"))
221  {
222  add_to_json(
223  ns, gf_entry.first, gf_entry.second.body, dead_map, json_result);
224  }
225  else if(options.get_bool_option("xml"))
226  {
227  add_to_xml(gf_entry.first, gf_entry.second.body, dead_map, xml_result);
228  }
229  else
230  {
231  // text or console
233  ns, gf_entry.first, gf_entry.second.body, dead_map, out);
234  }
235  }
236  }
237 
238  if(options.get_bool_option("json") && !json_result.empty())
239  out << json_result << '\n';
240  else if(options.get_bool_option("xml"))
241  out << xml_result << '\n';
242 
243  return false;
244 }
245 
246 
247 
249  const irep_idt &function,
250  const source_locationt &first_location,
251  const source_locationt &last_location,
252  json_arrayt &dest)
253 {
254  json_objectt entry{
255  {"function", json_stringt(function)},
256  {"file name",
258  id2string(first_location.get_working_directory()),
259  id2string(first_location.get_file())))},
260  {"first line", json_numbert(id2string(first_location.get_line()))},
261  {"last line", json_numbert(id2string(last_location.get_line()))}};
262 
263  dest.push_back(std::move(entry));
264 }
265 
267  const irep_idt &function,
268  const source_locationt &first_location,
269  const source_locationt &last_location,
270  xmlt &dest)
271 {
272  xmlt &x=dest.new_element("function");
273 
274  x.set_attribute("name", id2string(function));
275  x.set_attribute("file name",
277  id2string(first_location.get_working_directory()),
278  id2string(first_location.get_file())));
279  x.set_attribute("first line", id2string(first_location.get_line()));
280  x.set_attribute("last line", id2string(last_location.get_line()));
281 }
282 
283 static void list_functions(
284  const goto_modelt &goto_model,
285  const std::unordered_set<irep_idt> &called,
286  const optionst &options,
287  std::ostream &os,
288  bool unreachable)
289 {
290  json_arrayt json_result;
291  xmlt xml_result(unreachable ?
292  "unreachable-functions" :
293  "reachable-functions");
294 
295  const namespacet ns(goto_model.symbol_table);
296 
297  for(const auto &gf_entry : goto_model.goto_functions.function_map)
298  {
299  const symbolt &decl = ns.lookup(gf_entry.first);
300 
301  // gf_entry.first may be a link-time renamed version, use the
302  // base_name instead; do not list inlined functions
303  if(
304  unreachable == (called.find(decl.base_name) != called.end() ||
305  to_code_type(decl.type).get_inlined()))
306  {
307  continue;
308  }
309 
310  source_locationt first_location=decl.location;
311 
312  source_locationt last_location;
313  if(gf_entry.second.body_available())
314  {
315  const goto_programt &goto_program = gf_entry.second.body;
316 
317  goto_programt::const_targett end_function=
318  goto_program.instructions.end();
319 
320  // find the last instruction with a line number
321  // TODO(tautschnig): #918 will eventually ensure that every instruction
322  // has such
323  do
324  {
325  --end_function;
326  last_location = end_function->source_location;
327  }
328  while(
329  end_function != goto_program.instructions.begin() &&
330  last_location.get_line().empty());
331 
332  if(last_location.get_line().empty())
333  last_location = decl.location;
334  }
335  else
336  // completely ignore functions without a body, both for
337  // reachable and unreachable functions; we could also restrict
338  // this to macros/asm renaming
339  continue;
340 
341  if(options.get_bool_option("json"))
342  {
344  decl.base_name,
345  first_location,
346  last_location,
347  json_result);
348  }
349  else if(options.get_bool_option("xml"))
350  {
352  decl.base_name,
353  first_location,
354  last_location,
355  xml_result);
356  }
357  else
358  {
359  // text or console
360  os << concat_dir_file(
361  id2string(first_location.get_working_directory()),
362  id2string(first_location.get_file())) << " "
363  << decl.base_name << " "
364  << first_location.get_line() << " "
365  << last_location.get_line() << "\n";
366  }
367  }
368 
369  if(options.get_bool_option("json") && !json_result.empty())
370  os << json_result << '\n';
371  else if(options.get_bool_option("xml"))
372  os << xml_result << '\n';
373 }
374 
376  const goto_modelt &goto_model,
377  const bool json,
378  std::ostream &os)
379 {
380  optionst options;
381  if(json)
382  options.set_option("json", true);
383 
384  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
385 
386  list_functions(goto_model, called, options, os, true);
387 }
388 
390  const goto_modelt &goto_model,
391  const bool json,
392  std::ostream &os)
393 {
394  optionst options;
395  if(json)
396  options.set_option("json", true);
397 
398  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
399 
400  list_functions(goto_model, called, options, os, false);
401 }
402 
403 std::unordered_set<irep_idt> compute_called_functions_from_ai(
404  const goto_modelt &goto_model,
405  const ai_baset &ai)
406 {
407  std::unordered_set<irep_idt> called;
408 
409  for(const auto &gf_entry : goto_model.goto_functions.function_map)
410  {
411  if(!gf_entry.second.body_available())
412  continue;
413 
414  const goto_programt &p = gf_entry.second.body;
415 
416  if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
417  called.insert(gf_entry.first);
418  }
419 
420  return called;
421 }
422 
424  const goto_modelt &goto_model,
425  const ai_baset &ai,
426  const optionst &options,
427  std::ostream &out)
428 {
429  std::unordered_set<irep_idt> called =
430  compute_called_functions_from_ai(goto_model, ai);
431 
432  list_functions(goto_model, called, options, out, true);
433 
434  return false;
435 }
436 
438  const goto_modelt &goto_model,
439  const ai_baset &ai,
440  const optionst &options,
441  std::ostream &out)
442 {
443  std::unordered_set<irep_idt> called =
444  compute_called_functions_from_ai(goto_model, ai);
445 
446  list_functions(goto_model, called, options, out, false);
447 
448  return false;
449 }
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:103
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:198
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:112
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:222
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:266
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
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:27
xml.h
json_irep.h
Util.
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:46
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:86
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:283
reachable_functions
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:389
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:141
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
unreachable_functions
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:375
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:511
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:42
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:464
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
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.
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:20
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:403
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:569
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:437
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:120
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:659
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:248
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
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:423
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:41
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:1180
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