cprover
Loading...
Searching...
No Matches
unreachable_instructions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: List all unreachable instructions
4
5Author: Michael Tautschnig
6
7Date: 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
26typedef std::map<unsigned, goto_programt::const_targett> dead_mapt;
27
29 const goto_programt &goto_program,
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
47static void all_unreachable(
48 const goto_programt &goto_program,
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,
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
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
81static 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(
98 "source_location", it->second->source_location().as_string());
99 }
100 return;
101}
102
105{
106 if(source_location.get_file().empty())
107 return nullopt;
108
109 return concat_dir_file(
110 id2string(source_location.get_working_directory()),
111 id2string(source_location.get_file()));
112}
113
114static void add_to_json(
115 const namespacet &ns,
116 const irep_idt &function_identifier,
117 const goto_programt &goto_program,
118 const dead_mapt &dead_map,
120{
121 PRECONDITION(!goto_program.instructions.empty());
123 goto_program.instructions.end();
124 --end_function;
125 DATA_INVARIANT(end_function->is_end_function(),
126 "The last instruction in a goto-program must be END_FUNCTION");
127
128 json_objectt entry{{"function", json_stringt(function_identifier)}};
129 if(auto file_name_opt = file_name_string_opt(end_function->source_location()))
130 entry["file"] = json_stringt{*file_name_opt};
131
132 json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
133
134 for(dead_mapt::const_iterator it=dead_map.begin();
135 it!=dead_map.end();
136 ++it)
137 {
138 std::ostringstream oss;
139 goto_program.output_instruction(ns, function_identifier, oss, *it->second);
140 std::string s=oss.str();
141
142 std::string::size_type n=s.find('\n');
143 assert(n!=std::string::npos);
144 s.erase(0, n+1);
145 n=s.find_first_not_of(' ');
146 assert(n!=std::string::npos);
147 s.erase(0, n);
148 assert(!s.empty());
149 s.erase(s.size()-1);
150
151 // print info for file actually with full path
152 const source_locationt &l = it->second->source_location();
153 json_objectt i_entry{{"sourceLocation", json(l)},
154 {"statement", json_stringt(s)}};
155 dead_ins.push_back(std::move(i_entry));
156 }
157
158 dest.push_back(std::move(entry));
159}
160
162 const goto_modelt &goto_model,
163 const bool json,
164 std::ostream &os)
165{
167
168 std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
169
170 const namespacet ns(goto_model.symbol_table);
171
172 for(const auto &gf_entry : goto_model.goto_functions.function_map)
173 {
174 if(!gf_entry.second.body_available())
175 continue;
176
177 const goto_programt &goto_program = gf_entry.second.body;
178 dead_mapt dead_map;
179
180 const symbolt &decl = ns.lookup(gf_entry.first);
181
182 if(
183 called.find(decl.name) != called.end() ||
185 {
186 unreachable_instructions(goto_program, dead_map);
187 }
188 else
189 all_unreachable(goto_program, dead_map);
190
191 if(!dead_map.empty())
192 {
193 if(!json)
194 output_dead_plain(ns, gf_entry.first, goto_program, dead_map, os);
195 else
196 add_to_json(ns, gf_entry.first, goto_program, dead_map, json_result);
197 }
198 }
199
200 if(json && !json_result.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{
211 xmlt xml_result("unreachable-instructions");
212
213 const namespacet ns(goto_model.symbol_table);
214
215 for(const auto &gf_entry : goto_model.goto_functions.function_map)
216 {
217 if(!gf_entry.second.body_available())
218 continue;
219
220 const goto_programt &goto_program = gf_entry.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 {
229 ns, gf_entry.first, gf_entry.second.body, dead_map, json_result);
230 }
231 else if(options.get_bool_option("xml"))
232 {
233 add_to_xml(gf_entry.first, gf_entry.second.body, dead_map, xml_result);
234 }
235 else
236 {
237 // text or console
239 ns, gf_entry.first, gf_entry.second.body, dead_map, out);
240 }
241 }
242 }
243
244 if(options.get_bool_option("json") && !json_result.empty())
245 out << json_result << '\n';
246 else if(options.get_bool_option("xml"))
247 out << xml_result << '\n';
248
249 return false;
250}
251
253line_string_opt(const source_locationt &source_location)
254{
255 const irep_idt &line = source_location.get_line();
256
257 if(line.empty())
258 return nullopt;
259 else
260 return id2string(line);
261}
262
264 const irep_idt &function,
268{
269 json_objectt entry{{"function", json_stringt(function)}};
271 entry["file"] = json_stringt{*file_name_opt};
273 entry["firstLine"] = json_numbert{*line_opt};
275 entry["lastLine"] = json_numbert{*line_opt};
276
277 dest.push_back(std::move(entry));
278}
279
281 const irep_idt &function,
284 xmlt &dest)
285{
286 xmlt &x=dest.new_element("function");
287
288 x.set_attribute("name", id2string(function));
290 x.set_attribute("file", *file_name_opt);
292 x.set_attribute("first_line", *line_opt);
294 x.set_attribute("last_line", *line_opt);
295}
296
297static void list_functions(
298 const goto_modelt &goto_model,
299 const std::unordered_set<irep_idt> &called,
300 const optionst &options,
301 std::ostream &os,
302 bool unreachable)
303{
306 "unreachable-functions" :
307 "reachable-functions");
308
309 const namespacet ns(goto_model.symbol_table);
310
311 for(const auto &gf_entry : goto_model.goto_functions.function_map)
312 {
313 const symbolt &decl = ns.lookup(gf_entry.first);
314
315 if(
316 unreachable == (called.find(decl.name) != called.end() ||
318 {
319 continue;
320 }
321
323
325 if(gf_entry.second.body_available())
326 {
327 const goto_programt &goto_program = gf_entry.second.body;
328
330 goto_program.instructions.end();
331
332 // find the last instruction with a line number
333 // TODO(tautschnig): #918 will eventually ensure that every instruction
334 // has such
335 do
336 {
337 --end_function;
338 last_location = end_function->source_location();
339 }
340 while(
341 end_function != goto_program.instructions.begin() &&
342 last_location.get_line().empty());
343
344 if(last_location.get_line().empty())
345 last_location = decl.location;
346 }
347 else
348 // completely ignore functions without a body, both for
349 // reachable and unreachable functions; we could also restrict
350 // this to macros/asm renaming
351 continue;
352
353 if(options.get_bool_option("json"))
354 {
356 decl.base_name,
360 }
361 else if(options.get_bool_option("xml"))
362 {
364 decl.base_name,
367 xml_result);
368 }
369 else
370 {
371 // text or console
373 os << *file_name_opt << ' ';
374 os << decl.base_name;
376 os << ' ' << *line_opt;
378 os << ' ' << *line_opt;
379 os << '\n';
380 }
381 }
382
383 if(options.get_bool_option("json") && !json_result.empty())
384 os << json_result << '\n';
385 else if(options.get_bool_option("xml"))
386 os << xml_result << '\n';
387}
388
390 const goto_modelt &goto_model,
391 const bool json,
392 std::ostream &os)
393{
394 optionst options;
395 if(json)
396 options.set_option("json", true);
397
398 std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
399
400 list_functions(goto_model, called, options, os, true);
401}
402
404 const goto_modelt &goto_model,
405 const bool json,
406 std::ostream &os)
407{
408 optionst options;
409 if(json)
410 options.set_option("json", true);
411
412 std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
413
414 list_functions(goto_model, called, options, os, false);
415}
416
417std::unordered_set<irep_idt> compute_called_functions_from_ai(
418 const goto_modelt &goto_model,
419 const ai_baset &ai)
420{
421 std::unordered_set<irep_idt> called;
422
423 for(const auto &gf_entry : goto_model.goto_functions.function_map)
424 {
425 if(!gf_entry.second.body_available())
426 continue;
427
428 const goto_programt &p = gf_entry.second.body;
429
430 if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
431 called.insert(gf_entry.first);
432 }
433
434 return called;
435}
436
438 const goto_modelt &goto_model,
439 const ai_baset &ai,
440 const optionst &options,
441 std::ostream &out)
442{
443 std::unordered_set<irep_idt> called =
445
446 list_functions(goto_model, called, options, out, true);
447
448 return false;
449}
450
452 const goto_modelt &goto_model,
453 const ai_baset &ai,
454 const optionst &options,
455 std::ostream &out)
456{
457 std::unordered_set<irep_idt> called =
459
460 list_functions(goto_model, called, options, out, false);
461
462 return false;
463}
Abstract Interpretation.
Compute dominators for CFG of goto_function.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:119
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:223
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
iterator end()
Definition cfg.h:118
iterator begin()
Definition cfg.h:114
entry_mapt entry_map
Definition cfg.h:152
bool get_inlined() const
Definition std_types.h:665
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool get_bool_option(const std::string &option) const
Definition options.cpp:44
void set_option(const std::string &option, const bool value)
Definition options.cpp:28
const irep_idt & get_working_directory() const
const irep_idt & get_file() const
const irep_idt & get_line() const
Symbol table entry.
Definition symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
Definition xml.h:21
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
Query Called Functions.
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
Options.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
static optionalt< std::string > file_name_string_opt(const source_locationt &source_location)
static optionalt< std::string > line_string_opt(const source_locationt &source_location)
static void all_unreachable(const goto_programt &goto_program, dead_mapt &dest)
bool static_unreachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
static void list_functions(const goto_modelt &goto_model, const std::unordered_set< irep_idt > &called, const optionst &options, std::ostream &os, bool unreachable)
static void build_dead_map_from_ai(const goto_programt &goto_program, const ai_baset &ai, dead_mapt &dest)
static void add_to_xml(const irep_idt &function_identifier, const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest)
static void xml_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, xmlt &dest)
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)
bool static_unreachable_instructions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
std::unordered_set< irep_idt > compute_called_functions_from_ai(const goto_modelt &goto_model, const ai_baset &ai)
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
void unreachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void unreachable_instructions(const goto_programt &goto_program, dead_mapt &dest)
void reachable_functions(const goto_modelt &goto_model, const bool json, std::ostream &os)
static void json_output_function(const irep_idt &function, const source_locationt &first_location, const source_locationt &last_location, json_arrayt &dest)
std::map< unsigned, goto_programt::const_targett > dead_mapt
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)
List all unreachable instructions.