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  forall_goto_functions(f_it, goto_model.goto_functions)
165  {
166  if(!f_it->second.body_available())
167  continue;
168 
169  const goto_programt &goto_program=f_it->second.body;
170  dead_mapt dead_map;
171 
172  const symbolt &decl=ns.lookup(f_it->first);
173 
174  // f_it->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, f_it->first, goto_program, dead_map, os);
189  else
190  add_to_json(ns, f_it->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  forall_goto_functions(f_it, goto_model.goto_functions)
210  {
211  if(!f_it->second.body_available())
212  continue;
213 
214  const goto_programt &goto_program=f_it->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(ns, f_it->first, f_it->second.body, dead_map, json_result);
223  }
224  else if(options.get_bool_option("xml"))
225  {
226  add_to_xml(f_it->first, f_it->second.body, dead_map, xml_result);
227  }
228  else
229  {
230  // text or console
231  output_dead_plain(ns, f_it->first, f_it->second.body, dead_map, out);
232  }
233  }
234  }
235 
236  if(options.get_bool_option("json") && !json_result.empty())
237  out << json_result << '\n';
238  else if(options.get_bool_option("xml"))
239  out << xml_result << '\n';
240 
241  return false;
242 }
243 
244 
245 
247  const irep_idt &function,
248  const source_locationt &first_location,
249  const source_locationt &last_location,
250  json_arrayt &dest)
251 {
252  json_objectt entry{
253  {"function", json_stringt(function)},
254  {"file name",
256  id2string(first_location.get_working_directory()),
257  id2string(first_location.get_file())))},
258  {"first line", json_numbert(id2string(first_location.get_line()))},
259  {"last line", json_numbert(id2string(last_location.get_line()))}};
260 
261  dest.push_back(std::move(entry));
262 }
263 
265  const irep_idt &function,
266  const source_locationt &first_location,
267  const source_locationt &last_location,
268  xmlt &dest)
269 {
270  xmlt &x=dest.new_element("function");
271 
272  x.set_attribute("name", id2string(function));
273  x.set_attribute("file name",
275  id2string(first_location.get_working_directory()),
276  id2string(first_location.get_file())));
277  x.set_attribute("first line", id2string(first_location.get_line()));
278  x.set_attribute("last line", id2string(last_location.get_line()));
279 }
280 
281 static void list_functions(
282  const goto_modelt &goto_model,
283  const std::unordered_set<irep_idt> &called,
284  const optionst &options,
285  std::ostream &os,
286  bool unreachable)
287 {
288  json_arrayt json_result;
289  xmlt xml_result(unreachable ?
290  "unreachable-functions" :
291  "reachable-functions");
292 
293  const namespacet ns(goto_model.symbol_table);
294 
295  forall_goto_functions(f_it, goto_model.goto_functions)
296  {
297  const symbolt &decl=ns.lookup(f_it->first);
298 
299  // f_it->first may be a link-time renamed version, use the
300  // base_name instead; do not list inlined functions
301  if(
302  unreachable == (called.find(decl.base_name) != called.end() ||
303  to_code_type(decl.type).get_inlined()))
304  {
305  continue;
306  }
307 
308  source_locationt first_location=decl.location;
309 
310  source_locationt last_location;
311  if(f_it->second.body_available())
312  {
313  const goto_programt &goto_program=f_it->second.body;
314 
315  goto_programt::const_targett end_function=
316  goto_program.instructions.end();
317 
318  // find the last instruction with a line number
319  // TODO(tautschnig): #918 will eventually ensure that every instruction
320  // has such
321  do
322  {
323  --end_function;
324  last_location = end_function->source_location;
325  }
326  while(
327  end_function != goto_program.instructions.begin() &&
328  last_location.get_line().empty());
329 
330  if(last_location.get_line().empty())
331  last_location = decl.location;
332  }
333  else
334  // completely ignore functions without a body, both for
335  // reachable and unreachable functions; we could also restrict
336  // this to macros/asm renaming
337  continue;
338 
339  if(options.get_bool_option("json"))
340  {
342  decl.base_name,
343  first_location,
344  last_location,
345  json_result);
346  }
347  else if(options.get_bool_option("xml"))
348  {
350  decl.base_name,
351  first_location,
352  last_location,
353  xml_result);
354  }
355  else
356  {
357  // text or console
358  os << concat_dir_file(
359  id2string(first_location.get_working_directory()),
360  id2string(first_location.get_file())) << " "
361  << decl.base_name << " "
362  << first_location.get_line() << " "
363  << last_location.get_line() << "\n";
364  }
365  }
366 
367  if(options.get_bool_option("json") && !json_result.empty())
368  os << json_result << '\n';
369  else if(options.get_bool_option("xml"))
370  os << xml_result << '\n';
371 }
372 
374  const goto_modelt &goto_model,
375  const bool json,
376  std::ostream &os)
377 {
378  optionst options;
379  if(json)
380  options.set_option("json", true);
381 
382  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
383 
384  list_functions(goto_model, called, options, os, true);
385 }
386 
388  const goto_modelt &goto_model,
389  const bool json,
390  std::ostream &os)
391 {
392  optionst options;
393  if(json)
394  options.set_option("json", true);
395 
396  std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
397 
398  list_functions(goto_model, called, options, os, false);
399 }
400 
401 std::unordered_set<irep_idt> compute_called_functions_from_ai(
402  const goto_modelt &goto_model,
403  const ai_baset &ai)
404 {
405  std::unordered_set<irep_idt> called;
406 
407  forall_goto_functions(f_it, goto_model.goto_functions)
408  {
409  if(!f_it->second.body_available())
410  continue;
411 
412  const goto_programt &p = f_it->second.body;
413 
414  if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
415  called.insert(f_it->first);
416  }
417 
418  return called;
419 }
420 
422  const goto_modelt &goto_model,
423  const ai_baset &ai,
424  const optionst &options,
425  std::ostream &out)
426 {
427  std::unordered_set<irep_idt> called =
428  compute_called_functions_from_ai(goto_model, ai);
429 
430  list_functions(goto_model, called, options, out, true);
431 
432  return false;
433 }
434 
436  const goto_modelt &goto_model,
437  const ai_baset &ai,
438  const optionst &options,
439  std::ostream &out)
440 {
441  std::unordered_set<irep_idt> called =
442  compute_called_functions_from_ai(goto_model, ai);
443 
444  list_functions(goto_model, called, options, out, false);
445 
446  return false;
447 }
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:103
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:221
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:264
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
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:85
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:281
reachable_functions
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:387
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:140
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
unreachable_functions
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
Definition: unreachable_instructions.cpp:373
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:44
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:41
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:401
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:585
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:435
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
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:73
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:867
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:246
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
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:421
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:48
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:1196
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