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 
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 goto_programt &goto_program,
69  const dead_mapt &dead_map,
70  std::ostream &os)
71 {
72  assert(!goto_program.instructions.empty());
73  goto_programt::const_targett end_function=
74  goto_program.instructions.end();
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 goto_programt &goto_program,
88  const dead_mapt &dead_map,
89  xmlt &dest)
90 {
91  PRECONDITION(!goto_program.instructions.empty());
92  goto_programt::const_targett end_function=
93  goto_program.instructions.end();
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,
116  const goto_programt &goto_program,
117  const dead_mapt &dead_map,
118  json_arrayt &dest)
119 {
120  json_objectt &entry=dest.push_back().make_object();
121 
122  PRECONDITION(!goto_program.instructions.empty());
123  goto_programt::const_targett end_function=
124  goto_program.instructions.end();
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())
187  unreachable_instructions(goto_program, dead_map);
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  // text or console
237  output_dead_plain(ns, f_it->second.body, dead_map, out);
238  }
239  }
240  }
241 
242  if(options.get_bool_option("json") && !json_result.array.empty())
243  out << json_result << '\n';
244  else if(options.get_bool_option("xml"))
245  out << xml_result << '\n';
246 
247  return false;
248 }
249 
250 
251 
253  const irep_idt &function,
254  const source_locationt &first_location,
255  const source_locationt &last_location,
256  json_arrayt &dest)
257 {
258  json_objectt &entry=dest.push_back().make_object();
259 
260  entry["function"] = json_stringt(function);
261  entry["file name"]=
263  id2string(first_location.get_working_directory()),
264  id2string(first_location.get_file())));
265  entry["first line"]=
266  json_numbert(id2string(first_location.get_line()));
267  entry["last line"]=
268  json_numbert(id2string(last_location.get_line()));
269 }
270 
272  const irep_idt &function,
273  const source_locationt &first_location,
274  const source_locationt &last_location,
275  xmlt &dest)
276 {
277  xmlt &x=dest.new_element("function");
278 
279  x.set_attribute("name", id2string(function));
280  x.set_attribute("file name",
282  id2string(first_location.get_working_directory()),
283  id2string(first_location.get_file())));
284  x.set_attribute("first line", id2string(first_location.get_line()));
285  x.set_attribute("last line", id2string(last_location.get_line()));
286 }
287 
288 static void list_functions(
289  const goto_modelt &goto_model,
290  const std::unordered_set<irep_idt> &called,
291  const optionst &options,
292  std::ostream &os,
293  bool unreachable)
294 {
295  json_arrayt json_result;
296  xmlt xml_result(unreachable ?
297  "unreachable-functions" :
298  "reachable-functions");
299 
300  const namespacet ns(goto_model.symbol_table);
301 
302  forall_goto_functions(f_it, goto_model.goto_functions)
303  {
304  const symbolt &decl=ns.lookup(f_it->first);
305 
306  // f_it->first may be a link-time renamed version, use the
307  // base_name instead; do not list inlined functions
308  if(unreachable ==
309  (called.find(decl.base_name)!=called.end() ||
310  f_it->second.is_inlined()))
311  continue;
312 
313  source_locationt first_location=decl.location;
314 
315  source_locationt last_location;
316  if(f_it->second.body_available())
317  {
318  const goto_programt &goto_program=f_it->second.body;
319 
320  goto_programt::const_targett end_function=
321  goto_program.instructions.end();
322 
323  // find the last instruction with a line number
324  // TODO(tautschnig): #918 will eventually ensure that every instruction
325  // has such
326  do
327  {
328  --end_function;
329  last_location = end_function->source_location;
330  }
331  while(
332  end_function != goto_program.instructions.begin() &&
333  last_location.get_line().empty());
334 
335  if(last_location.get_line().empty())
336  last_location = decl.location;
337  }
338  else
339  // completely ignore functions without a body, both for
340  // reachable and unreachable functions; we could also restrict
341  // this to macros/asm renaming
342  continue;
343 
344  if(options.get_bool_option("json"))
345  {
347  decl.base_name,
348  first_location,
349  last_location,
350  json_result);
351  }
352  else if(options.get_bool_option("xml"))
353  {
355  decl.base_name,
356  first_location,
357  last_location,
358  xml_result);
359  }
360  else
361  {
362  // text or console
363  os << concat_dir_file(
364  id2string(first_location.get_working_directory()),
365  id2string(first_location.get_file())) << " "
366  << decl.base_name << " "
367  << first_location.get_line() << " "
368  << last_location.get_line() << "\n";
369  }
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 
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 
401  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
402 
403  list_functions(goto_model, called, options, os, false);
404 }
405 
406 std::unordered_set<irep_idt> compute_called_functions_from_ai(
407  const goto_modelt &goto_model,
408  const ai_baset &ai)
409 {
410  std::unordered_set<irep_idt> called;
411 
412  forall_goto_functions(f_it, goto_model.goto_functions)
413  {
414  if(!f_it->second.body_available())
415  continue;
416 
417  const goto_programt &p = f_it->second.body;
418 
419  if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
420  called.insert(f_it->first);
421  }
422 
423  return called;
424 }
425 
427  const goto_modelt &goto_model,
428  const ai_baset &ai,
429  const optionst &options,
430  std::ostream &out)
431 {
432  std::unordered_set<irep_idt> called =
433  compute_called_functions_from_ai(goto_model, ai);
434 
435  list_functions(goto_model, called, options, out, true);
436 
437  return false;
438 }
439 
441  const goto_modelt &goto_model,
442  const ai_baset &ai,
443  const optionst &options,
444  std::ostream &out)
445 {
446  std::unordered_set<irep_idt> called =
447  compute_called_functions_from_ai(goto_model, ai);
448 
449  list_functions(goto_model, called, options, out, false);
450 
451  return false;
452 }
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:141
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
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
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
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:170
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:420
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:175
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
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:35
Query Called Functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
List all unreachable instructions.
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
const irep_idt & get_file() const
xmlt & new_element(const std::string &key)
Definition: xml.h:86
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
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)
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:26
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
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:804
bool empty() const
Definition: dstring.h:75
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166