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(
88  const dead_mapt &dead_map,
89  xmlt &dest)
90 {
92  goto_programt::const_targett end_function=
94  --end_function;
95  DATA_INVARIANT(end_function->is_end_function(),
96  "The last instruction in a goto-program must be END_FUNCTION");
97 
98  xmlt &x = dest.new_element("function");
99  x.set_attribute("name", id2string(end_function->function));
100 
101  for(dead_mapt::const_iterator it=dead_map.begin();
102  it!=dead_map.end();
103  ++it)
104  {
105  xmlt &inst = x.new_element("instruction");
106  inst.set_attribute("location_number",
107  std::to_string(it->second->location_number));
108  inst.set_attribute("source_location",
109  it->second->source_location.as_string());
110  }
111  return;
112 }
113 
114 static void add_to_json(
115  const namespacet &ns,
117  const dead_mapt &dead_map,
118  json_arrayt &dest)
119 {
120  json_objectt &entry=dest.push_back().make_object();
121 
123  goto_programt::const_targett end_function=
125  --end_function;
126  DATA_INVARIANT(end_function->is_end_function(),
127  "The last instruction in a goto-program must be END_FUNCTION");
128 
129  entry["function"] = json_stringt(end_function->function);
130  entry["fileName"]=
132  id2string(end_function->source_location.get_working_directory()),
133  id2string(end_function->source_location.get_file())));
134 
135  json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
136 
137  for(dead_mapt::const_iterator it=dead_map.begin();
138  it!=dead_map.end();
139  ++it)
140  {
141  std::ostringstream oss;
142  goto_program.output_instruction(ns, "", oss, *it->second);
143  std::string s=oss.str();
144 
145  std::string::size_type n=s.find('\n');
146  assert(n!=std::string::npos);
147  s.erase(0, n+1);
148  n=s.find_first_not_of(' ');
149  assert(n!=std::string::npos);
150  s.erase(0, n);
151  assert(!s.empty());
152  s.erase(s.size()-1);
153 
154  // print info for file actually with full path
155  json_objectt &i_entry=dead_ins.push_back().make_object();
156  const source_locationt &l=it->second->source_location;
157  i_entry["sourceLocation"]=json(l);
158  i_entry["statement"]=json_stringt(s);
159  }
160 }
161 
163  const goto_modelt &goto_model,
164  const bool json,
165  std::ostream &os)
166 {
167  json_arrayt json_result;
168 
169  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
170 
171  const namespacet ns(goto_model.symbol_table);
172 
173  forall_goto_functions(f_it, goto_model.goto_functions)
174  {
175  if(!f_it->second.body_available())
176  continue;
177 
178  const goto_programt &goto_program=f_it->second.body;
179  dead_mapt dead_map;
180 
181  const symbolt &decl=ns.lookup(f_it->first);
182 
183  // f_it->first may be a link-time renamed version, use the
184  // base_name instead; do not list inlined functions
185  if(called.find(decl.base_name)!=called.end() ||
186  f_it->second.is_inlined())
188  else
189  all_unreachable(goto_program, dead_map);
190 
191  if(!dead_map.empty())
192  {
193  if(!json)
194  output_dead_plain(ns, goto_program, dead_map, os);
195  else
196  add_to_json(ns, goto_program, dead_map, json_result);
197  }
198  }
199 
200  if(json && !json_result.array.empty())
201  os << json_result << '\n';
202 }
203 
205  const goto_modelt &goto_model,
206  const ai_baset &ai,
207  const optionst &options,
208  std::ostream &out)
209 {
210  json_arrayt json_result;
211  xmlt xml_result("unreachable-instructions");
212 
213  const namespacet ns(goto_model.symbol_table);
214 
215  forall_goto_functions(f_it, goto_model.goto_functions)
216  {
217  if(!f_it->second.body_available())
218  continue;
219 
220  const goto_programt &goto_program=f_it->second.body;
221  dead_mapt dead_map;
222  build_dead_map_from_ai(goto_program, ai, dead_map);
223 
224  if(!dead_map.empty())
225  {
226  if(options.get_bool_option("json"))
227  {
228  add_to_json(ns, f_it->second.body, dead_map, json_result);
229  }
230  else if(options.get_bool_option("xml"))
231  {
232  add_to_xml(f_it->second.body, dead_map, xml_result);
233  }
234  else
235  {
236  INVARIANT(options.get_bool_option("text"),
237  "Other output formats handled");
238  output_dead_plain(ns, f_it->second.body, dead_map, out);
239  }
240  }
241  }
242 
243  if(options.get_bool_option("json") && !json_result.array.empty())
244  out << json_result << '\n';
245  else if(options.get_bool_option("xml"))
246  out << xml_result << '\n';
247 
248  return false;
249 }
250 
251 
252 
254  const irep_idt &function,
255  const source_locationt &first_location,
256  const source_locationt &last_location,
257  json_arrayt &dest)
258 {
259  json_objectt &entry=dest.push_back().make_object();
260 
261  entry["function"] = json_stringt(function);
262  entry["file name"]=
264  id2string(first_location.get_working_directory()),
265  id2string(first_location.get_file())));
266  entry["first line"]=
267  json_numbert(id2string(first_location.get_line()));
268  entry["last line"]=
269  json_numbert(id2string(last_location.get_line()));
270 }
271 
273  const irep_idt &function,
274  const source_locationt &first_location,
275  const source_locationt &last_location,
276  xmlt &dest)
277 {
278  xmlt &x=dest.new_element("function");
279 
280  x.set_attribute("name", id2string(function));
281  x.set_attribute("file name",
283  id2string(first_location.get_working_directory()),
284  id2string(first_location.get_file())));
285  x.set_attribute("first line", id2string(first_location.get_line()));
286  x.set_attribute("last line", id2string(last_location.get_line()));
287 }
288 
289 static void list_functions(
290  const goto_modelt &goto_model,
291  const std::unordered_set<irep_idt> &called,
292  const optionst &options,
293  std::ostream &os,
294  bool unreachable)
295 {
296  json_arrayt json_result;
297  xmlt xml_result(unreachable ?
298  "unreachable-functions" :
299  "reachable-functions");
300 
301  const namespacet ns(goto_model.symbol_table);
302 
303  forall_goto_functions(f_it, goto_model.goto_functions)
304  {
305  const symbolt &decl=ns.lookup(f_it->first);
306 
307  // f_it->first may be a link-time renamed version, use the
308  // base_name instead; do not list inlined functions
309  if(unreachable ==
310  (called.find(decl.base_name)!=called.end() ||
311  f_it->second.is_inlined()))
312  continue;
313 
314  source_locationt first_location=decl.location;
315 
316  source_locationt last_location;
317  if(f_it->second.body_available())
318  {
319  const goto_programt &goto_program=f_it->second.body;
320 
321  goto_programt::const_targett end_function=
323 
324  // find the last instruction with a line number
325  // TODO(tautschnig): #918 will eventually ensure that every instruction
326  // has such
327  do
328  {
329  --end_function;
330  last_location = end_function->source_location;
331  }
332  while(
333  end_function != goto_program.instructions.begin() &&
334  last_location.get_line().empty());
335 
336  if(last_location.get_line().empty())
337  last_location = decl.location;
338  }
339  else
340  // completely ignore functions without a body, both for
341  // reachable and unreachable functions; we could also restrict
342  // this to macros/asm renaming
343  continue;
344 
345  if(options.get_bool_option("text"))
346  {
347  os << concat_dir_file(
348  id2string(first_location.get_working_directory()),
349  id2string(first_location.get_file())) << " "
350  << decl.base_name << " "
351  << first_location.get_line() << " "
352  << last_location.get_line() << "\n";
353  }
354  else if(options.get_bool_option("xml"))
355  {
357  decl.base_name,
358  first_location,
359  last_location,
360  xml_result);
361  }
362  else
364  decl.base_name,
365  first_location,
366  last_location,
367  json_result);
368  }
369 
370  if(options.get_bool_option("json") && !json_result.array.empty())
371  os << json_result << '\n';
372  else if(options.get_bool_option("xml"))
373  os << xml_result << '\n';
374 }
375 
377  const goto_modelt &goto_model,
378  const bool json,
379  std::ostream &os)
380 {
381  optionst options;
382  if(json)
383  options.set_option("json", true);
384  else
385  options.set_option("text", true);
386 
387  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
388 
389  list_functions(goto_model, called, options, os, true);
390 }
391 
393  const goto_modelt &goto_model,
394  const bool json,
395  std::ostream &os)
396 {
397  optionst options;
398  if(json)
399  options.set_option("json", true);
400  else
401  options.set_option("text", true);
402 
403  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
404 
405  list_functions(goto_model, called, options, os, false);
406 }
407 
408 std::unordered_set<irep_idt> compute_called_functions_from_ai(
409  const goto_modelt &goto_model,
410  const ai_baset &ai)
411 {
412  std::unordered_set<irep_idt> called;
413 
414  forall_goto_functions(f_it, goto_model.goto_functions)
415  {
416  if(!f_it->second.body_available())
417  continue;
418 
419  const goto_programt &p = f_it->second.body;
420 
421  if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
422  called.insert(f_it->first);
423  }
424 
425  return called;
426 }
427 
429  const goto_modelt &goto_model,
430  const ai_baset &ai,
431  const optionst &options,
432  std::ostream &out)
433 {
434  std::unordered_set<irep_idt> called =
435  compute_called_functions_from_ai(goto_model, ai);
436 
437  list_functions(goto_model, called, options, out, true);
438 
439  return false;
440 }
441 
443  const goto_modelt &goto_model,
444  const ai_baset &ai,
445  const optionst &options,
446  std::ostream &out)
447 {
448  std::unordered_set<irep_idt> called =
449  compute_called_functions_from_ai(goto_model, ai);
450 
451  list_functions(goto_model, called, options, out, false);
452 
453  return false;
454 }
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:44
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
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
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
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 std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Accessing individual domains at particular locations (without needing to know what kind of domain or ...
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:204
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
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
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:242
Definition: xml.h:18
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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
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.
The basic interface of an abstract interpreter.
Definition: ai.h:32
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)
static void add_to_xml(const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest)
goto_programt & goto_program
Definition: cover.cpp:63
Options.
json_objectt & make_object()
Definition: json.h:290
std::map< unsigned, goto_programt::const_targett > dead_mapt
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
arrayt array
Definition: json.h:129
Compute dominators for CFG of goto_function.
#define forall_goto_functions(it, functions)
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
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:73
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:136