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_expr.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 
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(
49  dead_mapt &dest)
50 {
52  if(!it->is_end_function())
53  dest.insert(std::make_pair(it->location_number, it));
54 }
55 
58  const ai_baset &ai,
59  dead_mapt &dest)
60 {
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,
69  const dead_mapt &dead_map,
70  std::ostream &os)
71 {
72  assert(!goto_program.instructions.empty());
73  goto_programt::const_targett end_function=
75  --end_function;
76  assert(end_function->is_end_function());
77 
78  os << "\n*** " << end_function->function << " ***\n";
79 
80  for(dead_mapt::const_iterator it=dead_map.begin();
81  it!=dead_map.end();
82  ++it)
83  goto_program.output_instruction(ns, "", os, *it->second);
84 }
85 
86 static void add_to_xml(
87  const namespacet &ns,
89  const dead_mapt &dead_map,
90  xmlt &dest)
91 {
93  goto_programt::const_targett end_function=
95  --end_function;
96  DATA_INVARIANT(end_function->is_end_function(),
97  "The last instruction in a goto-program must be END_FUNCTION");
98 
99  xmlt &x = dest.new_element("function");
100  x.set_attribute("name", id2string(end_function->function));
101 
102  for(dead_mapt::const_iterator it=dead_map.begin();
103  it!=dead_map.end();
104  ++it)
105  {
106  xmlt &inst = x.new_element("instruction");
107  inst.set_attribute("location_number",
108  std::to_string(it->second->location_number));
109  inst.set_attribute("source_location",
110  it->second->source_location.as_string());
111  }
112  return;
113 }
114 
115 static void add_to_json(
116  const namespacet &ns,
118  const dead_mapt &dead_map,
119  json_arrayt &dest)
120 {
121  json_objectt &entry=dest.push_back().make_object();
122 
124  goto_programt::const_targett end_function=
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  entry["function"] = json_stringt(end_function->function);
131  entry["fileName"]=
133  id2string(end_function->source_location.get_working_directory()),
134  id2string(end_function->source_location.get_file())));
135 
136  json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
137 
138  for(dead_mapt::const_iterator it=dead_map.begin();
139  it!=dead_map.end();
140  ++it)
141  {
142  std::ostringstream oss;
143  goto_program.output_instruction(ns, "", oss, *it->second);
144  std::string s=oss.str();
145 
146  std::string::size_type n=s.find('\n');
147  assert(n!=std::string::npos);
148  s.erase(0, n+1);
149  n=s.find_first_not_of(' ');
150  assert(n!=std::string::npos);
151  s.erase(0, n);
152  assert(!s.empty());
153  s.erase(s.size()-1);
154 
155  // print info for file actually with full path
156  json_objectt &i_entry=dead_ins.push_back().make_object();
157  const source_locationt &l=it->second->source_location;
158  i_entry["sourceLocation"]=json(l);
159  i_entry["statement"]=json_stringt(s);
160  }
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  forall_goto_functions(f_it, goto_model.goto_functions)
175  {
176  if(!f_it->second.body_available())
177  continue;
178 
179  const goto_programt &goto_program=f_it->second.body;
180  dead_mapt dead_map;
181 
182  const symbolt &decl=ns.lookup(f_it->first);
183 
184  // f_it->first may be a link-time renamed version, use the
185  // base_name instead; do not list inlined functions
186  if(called.find(decl.base_name)!=called.end() ||
187  f_it->second.is_inlined())
189  else
190  all_unreachable(goto_program, dead_map);
191 
192  if(!dead_map.empty())
193  {
194  if(!json)
195  output_dead_plain(ns, goto_program, dead_map, os);
196  else
197  add_to_json(ns, goto_program, dead_map, json_result);
198  }
199  }
200 
201  if(json && !json_result.array.empty())
202  os << json_result << '\n';
203 }
204 
206  const goto_modelt &goto_model,
207  const ai_baset &ai,
208  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  forall_goto_functions(f_it, goto_model.goto_functions)
218  {
219  if(!f_it->second.body_available())
220  continue;
221 
222  const goto_programt &goto_program=f_it->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(ns, f_it->second.body, dead_map, json_result);
231  }
232  else if(options.get_bool_option("xml"))
233  {
234  add_to_xml(ns, f_it->second.body, dead_map, xml_result);
235  }
236  else
237  {
238  INVARIANT(options.get_bool_option("text"),
239  "Other output formats handled");
240  output_dead_plain(ns, f_it->second.body, dead_map, out);
241  }
242  }
243  }
244 
245  if(options.get_bool_option("json") && !json_result.array.empty())
246  out << json_result << '\n';
247  else if(options.get_bool_option("xml"))
248  out << xml_result << '\n';
249 
250  return false;
251 }
252 
253 
254 
256  const irep_idt &function,
257  const source_locationt &first_location,
258  const source_locationt &last_location,
259  json_arrayt &dest)
260 {
261  json_objectt &entry=dest.push_back().make_object();
262 
263  entry["function"] = json_stringt(function);
264  entry["file name"]=
266  id2string(first_location.get_working_directory()),
267  id2string(first_location.get_file())));
268  entry["first line"]=
269  json_numbert(id2string(first_location.get_line()));
270  entry["last line"]=
271  json_numbert(id2string(last_location.get_line()));
272 }
273 
275  const irep_idt &function,
276  const source_locationt &first_location,
277  const source_locationt &last_location,
278  xmlt &dest)
279 {
280  xmlt &x=dest.new_element("function");
281 
282  x.set_attribute("name", id2string(function));
283  x.set_attribute("file name",
285  id2string(first_location.get_working_directory()),
286  id2string(first_location.get_file())));
287  x.set_attribute("first line", id2string(first_location.get_line()));
288  x.set_attribute("last line", id2string(last_location.get_line()));
289 }
290 
291 static void list_functions(
292  const goto_modelt &goto_model,
293  const std::unordered_set<irep_idt> &called,
294  const optionst &options,
295  std::ostream &os,
296  bool unreachable)
297 {
298  json_arrayt json_result;
299  xmlt xml_result(unreachable ?
300  "unreachable-functions" :
301  "reachable-functions");
302 
303  const namespacet ns(goto_model.symbol_table);
304 
305  forall_goto_functions(f_it, goto_model.goto_functions)
306  {
307  const symbolt &decl=ns.lookup(f_it->first);
308 
309  // f_it->first may be a link-time renamed version, use the
310  // base_name instead; do not list inlined functions
311  if(unreachable ==
312  (called.find(decl.base_name)!=called.end() ||
313  f_it->second.is_inlined()))
314  continue;
315 
316  source_locationt first_location=decl.location;
317 
318  source_locationt last_location;
319  if(f_it->second.body_available())
320  {
321  const goto_programt &goto_program=f_it->second.body;
322 
323  goto_programt::const_targett end_function=
325 
326  // find the last instruction with a line number
327  // TODO(tautschnig): #918 will eventually ensure that every instruction
328  // has such
329  do
330  {
331  --end_function;
332  last_location = end_function->source_location;
333  }
334  while(
335  end_function != goto_program.instructions.begin() &&
336  last_location.get_line().empty());
337 
338  if(last_location.get_line().empty())
339  last_location = decl.location;
340  }
341  else
342  // completely ignore functions without a body, both for
343  // reachable and unreachable functions; we could also restrict
344  // this to macros/asm renaming
345  continue;
346 
347  if(options.get_bool_option("text"))
348  {
349  os << concat_dir_file(
350  id2string(first_location.get_working_directory()),
351  id2string(first_location.get_file())) << " "
352  << decl.base_name << " "
353  << first_location.get_line() << " "
354  << last_location.get_line() << "\n";
355  }
356  else if(options.get_bool_option("xml"))
357  {
359  decl.base_name,
360  first_location,
361  last_location,
362  xml_result);
363  }
364  else
366  decl.base_name,
367  first_location,
368  last_location,
369  json_result);
370  }
371 
372  if(options.get_bool_option("json") && !json_result.array.empty())
373  os << json_result << '\n';
374  else if(options.get_bool_option("xml"))
375  os << xml_result << '\n';
376 }
377 
379  const goto_modelt &goto_model,
380  const bool json,
381  std::ostream &os)
382 {
383  optionst options;
384  if(json)
385  options.set_option("json", true);
386  else
387  options.set_option("text", true);
388 
389  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
390 
391  list_functions(goto_model, called, options, os, true);
392 }
393 
395  const goto_modelt &goto_model,
396  const bool json,
397  std::ostream &os)
398 {
399  optionst options;
400  if(json)
401  options.set_option("json", true);
402  else
403  options.set_option("text", true);
404 
405  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
406 
407  list_functions(goto_model, called, options, os, false);
408 }
409 
410 std::unordered_set<irep_idt> compute_called_functions_from_ai(
411  const goto_modelt &goto_model,
412  const ai_baset &ai)
413 {
414  std::unordered_set<irep_idt> called;
415 
416  forall_goto_functions(f_it, goto_model.goto_functions)
417  {
418  if(!f_it->second.body_available())
419  continue;
420 
421  const goto_programt &p = f_it->second.body;
422 
423  if(!ai.abstract_state_before(p.instructions.begin()).is_bottom())
424  called.insert(f_it->first);
425  }
426 
427  return called;
428 }
429 
431  const goto_modelt &goto_model,
432  const ai_baset &ai,
433  const optionst &options,
435  std::ostream &out)
436 {
437  std::unordered_set<irep_idt> called =
438  compute_called_functions_from_ai(goto_model, ai);
439 
440  list_functions(goto_model, called, options, out, true);
441 
442  return false;
443 }
444 
446  const goto_modelt &goto_model,
447  const ai_baset &ai,
448  const optionst &options,
450  std::ostream &out)
451 {
452  std::unordered_set<irep_idt> called =
453  compute_called_functions_from_ai(goto_model, ai);
454 
455  list_functions(goto_model, called, options, out, false);
456 
457  return false;
458 }
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:134
const irep_idt & get_working_directory() const
static void build_dead_map_from_ai(const goto_programt &goto_program, const ai_baset &ai, dead_mapt &dest)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
std::unordered_set< irep_idt > compute_called_functions_from_ai(const goto_modelt &goto_model, const ai_baset &ai)
entry_mapt entry_map
Definition: cfg.h:106
static void xml_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, xmlt &dest)
static void json_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest)
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
unsignedbv_typet size_type()
Definition: c_types.cpp:58
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
virtual bool is_bottom() const =0
static void add_to_json(const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, json_arrayt &dest)
json_arrayt & make_array()
Definition: json.h:284
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
static void output_dead_plain(const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, std::ostream &os)
static void list_functions(const goto_modelt &goto_model, const std::unordered_set< irep_idt > &called, const optionst &options, std::ostream &os, bool unreachable)
jsont & push_back(const jsont &json)
Definition: json.h:163
const irep_idt & get_line() const
cfg_base_nodet< nodet, goto_programt::const_targett > nodet
Definition: graph.h:136
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
Expressions in JSON.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
Definition: xml.h:18
xmlt & new_element(const std::string &name)
Definition: xml.h:86
Query Called Functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
List all unreachable instructions.
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
const irep_idt & get_file() const
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
Abstract Interpretation.
Definition: ai.h:128
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
std::string to_string(const string_constraintt &expr)
Used for debug printing.
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void all_unreachable(const goto_programt &goto_program, dead_mapt &dest)
goto_programt & goto_program
Definition: cover.cpp:63
virtual const ai_domain_baset & abstract_state_before(goto_programt::const_targett t) const =0
Returns the abstract state before the given instruction.
Options.
json_objectt & make_object()
Definition: json.h:290
std::map< unsigned, goto_programt::const_targett > dead_mapt
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
arrayt array
Definition: json.h:129
Compute dominators for CFG of goto_function.
#define forall_goto_functions(it, functions)
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
static void add_to_xml(const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest)