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 <sstream>
17 
18 #include <util/json.h>
19 #include <util/json_expr.h>
20 #include <util/file_util.h>
21 
23 
26 
27 typedef std::map<unsigned, goto_programt::const_targett> dead_mapt;
28 
30  const goto_programt &goto_program,
31  dead_mapt &dest)
32 {
33  cfg_dominatorst dominators;
34  dominators(goto_program);
35 
36  for(cfg_dominatorst::cfgt::entry_mapt::const_iterator
37  it=dominators.cfg.entry_map.begin();
38  it!=dominators.cfg.entry_map.end();
39  ++it)
40  {
41  const cfg_dominatorst::cfgt::nodet &n=dominators.cfg[it->second];
42  if(n.dominators.empty())
43  dest.insert(std::make_pair(it->first->location_number,
44  it->first));
45  }
46 }
47 
48 static void all_unreachable(
49  const goto_programt &goto_program,
50  dead_mapt &dest)
51 {
52  forall_goto_program_instructions(it, goto_program)
53  if(!it->is_end_function())
54  dest.insert(std::make_pair(it->location_number, it));
55 }
56 
57 static void output_dead_plain(
58  const namespacet &ns,
59  const goto_programt &goto_program,
60  const dead_mapt &dead_map,
61  std::ostream &os)
62 {
63  assert(!goto_program.instructions.empty());
64  goto_programt::const_targett end_function=
65  goto_program.instructions.end();
66  --end_function;
67  assert(end_function->is_end_function());
68 
69  os << "\n*** " << end_function->function << " ***\n";
70 
71  for(dead_mapt::const_iterator it=dead_map.begin();
72  it!=dead_map.end();
73  ++it)
74  goto_program.output_instruction(ns, "", os, it->second);
75 }
76 
77 static void add_to_json(
78  const namespacet &ns,
79  const goto_programt &goto_program,
80  const dead_mapt &dead_map,
81  json_arrayt &dest)
82 {
83  json_objectt &entry=dest.push_back().make_object();
84 
85  assert(!goto_program.instructions.empty());
86  goto_programt::const_targett end_function=
87  goto_program.instructions.end();
88  --end_function;
89  assert(end_function->is_end_function());
90 
91  entry["function"]=json_stringt(id2string(end_function->function));
92  entry["fileName"]=
94  id2string(end_function->source_location.get_working_directory()),
95  id2string(end_function->source_location.get_file())));
96 
97  json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
98 
99  for(dead_mapt::const_iterator it=dead_map.begin();
100  it!=dead_map.end();
101  ++it)
102  {
103  std::ostringstream oss;
104  goto_program.output_instruction(ns, "", oss, it->second);
105  std::string s=oss.str();
106 
107  std::string::size_type n=s.find('\n');
108  assert(n!=std::string::npos);
109  s.erase(0, n+1);
110  n=s.find_first_not_of(' ');
111  assert(n!=std::string::npos);
112  s.erase(0, n);
113  assert(!s.empty());
114  s.erase(s.size()-1);
115 
116  // print info for file actually with full path
117  json_objectt &i_entry=dead_ins.push_back().make_object();
118  const source_locationt &l=it->second->source_location;
119  i_entry["sourceLocation"]=json(l);
120  i_entry["statement"]=json_stringt(s);
121  }
122 }
123 
125  const goto_modelt &goto_model,
126  const bool json,
127  std::ostream &os)
128 {
129  json_arrayt json_result;
130 
131  std::set<irep_idt> called;
132  compute_called_functions(goto_model, called);
133 
134  const namespacet ns(goto_model.symbol_table);
135 
136  forall_goto_functions(f_it, goto_model.goto_functions)
137  {
138  if(!f_it->second.body_available())
139  continue;
140 
141  const goto_programt &goto_program=f_it->second.body;
142  dead_mapt dead_map;
143 
144  const symbolt &decl=ns.lookup(f_it->first);
145 
146  // f_it->first may be a link-time renamed version, use the
147  // base_name instead; do not list inlined functions
148  if(called.find(decl.base_name)!=called.end() ||
149  f_it->second.is_inlined())
150  unreachable_instructions(goto_program, dead_map);
151  else
152  all_unreachable(goto_program, dead_map);
153 
154  if(!dead_map.empty())
155  {
156  if(!json)
157  output_dead_plain(ns, goto_program, dead_map, os);
158  else
159  add_to_json(ns, goto_program, dead_map, json_result);
160  }
161  }
162 
163  if(json && !json_result.array.empty())
164  os << json_result << '\n';
165 }
166 
168  const irep_idt &function,
169  const source_locationt &first_location,
170  const source_locationt &last_location,
171  json_arrayt &dest)
172 {
173  json_objectt &entry=dest.push_back().make_object();
174 
175  entry["function"]=json_stringt(id2string(function));
176  entry["file name"]=
178  id2string(first_location.get_working_directory()),
179  id2string(first_location.get_file())));
180  entry["first line"]=
181  json_numbert(id2string(first_location.get_line()));
182  entry["last line"]=
183  json_numbert(id2string(last_location.get_line()));
184 }
185 
186 static void list_functions(
187  const goto_modelt &goto_model,
188  const bool json,
189  std::ostream &os,
190  bool unreachable)
191 {
192  json_arrayt json_result;
193 
194  std::set<irep_idt> called;
195  compute_called_functions(goto_model, called);
196 
197  const namespacet ns(goto_model.symbol_table);
198 
199  forall_goto_functions(f_it, goto_model.goto_functions)
200  {
201  const symbolt &decl=ns.lookup(f_it->first);
202 
203  // f_it->first may be a link-time renamed version, use the
204  // base_name instead; do not list inlined functions
205  if(unreachable ==
206  (called.find(decl.base_name)!=called.end() ||
207  f_it->second.is_inlined()))
208  continue;
209 
210  source_locationt first_location=decl.location;
211 
212  source_locationt last_location;
213  if(f_it->second.body_available())
214  {
215  const goto_programt &goto_program=f_it->second.body;
216 
217  goto_programt::const_targett end_function=
218  goto_program.instructions.end();
219  --end_function;
220  assert(end_function->is_end_function());
221  last_location=end_function->source_location;
222  }
223  else
224  // completely ignore functions without a body, both for
225  // reachable and unreachable functions; we could also restrict
226  // this to macros/asm renaming
227  continue;
228 
229  if(!json)
230  {
231  os << concat_dir_file(
232  id2string(first_location.get_working_directory()),
233  id2string(first_location.get_file())) << " "
234  << decl.base_name << " "
235  << first_location.get_line() << " "
236  << last_location.get_line() << "\n";
237  }
238  else
240  decl.base_name,
241  first_location,
242  last_location,
243  json_result);
244  }
245 
246  if(json && !json_result.array.empty())
247  os << json_result << '\n';
248 }
249 
251  const goto_modelt &goto_model,
252  const bool json,
253  std::ostream &os)
254 {
255  list_functions(goto_model, json, os, true);
256 }
257 
259  const goto_modelt &goto_model,
260  const bool json,
261  std::ostream &os)
262 {
263  list_functions(goto_model, json, os, false);
264 }
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:128
const irep_idt & get_working_directory() const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
entry_mapt entry_map
Definition: cfg.h:87
instructionst instructions
The list of instructions in the goto program.
static void json_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest)
unsignedbv_typet size_type()
Definition: c_types.cpp:57
symbol_tablet symbol_table
Definition: goto_model.h:25
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static void list_functions(const goto_modelt &goto_model, const bool json, std::ostream &os, bool unreachable)
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:228
static void output_dead_plain(const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, std::ostream &os)
jsont & push_back(const jsont &json)
Definition: json.h:157
Symbol Table + CFG.
instructionst::const_iterator const_targett
const irep_idt & get_line() const
cfg_base_nodet< nodet, goto_programt::const_targett > nodet
Definition: graph.h:135
Expressions in JSON.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Query Called Functions.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
List all unreachable instructions.
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
const irep_idt & get_file() const
void compute_called_functions(const goto_functionst &goto_functions, std::set< irep_idt > &functions)
computes the functions that are (potentially) called
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
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)
json_objectt & make_object()
Definition: json.h:234
std::map< unsigned, goto_programt::const_targett > dead_mapt
arrayt array
Definition: json.h:126
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)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
goto_functionst goto_functions
Definition: goto_model.h:26
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:23