CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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/json_irep.h>
17#include <util/options.h>
18#include <util/xml.h>
19
21
22#include <analyses/ai.h>
24
25#include <filesystem>
26
27typedef 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
48static 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
58 const goto_programt &goto_program,
59 const ai_baset &ai,
60 dead_mapt &dest)
61{
62 forall_goto_program_instructions(it, goto_program)
63 if(ai.abstract_state_before(it)->is_bottom())
64 dest.insert(std::make_pair(it->location_number, it));
65}
66
68 const namespacet &ns,
69 const irep_idt &function_identifier,
70 const goto_programt &goto_program,
71 const dead_mapt &dead_map,
72 std::ostream &os)
73{
74 os << "\n*** " << function_identifier << " ***\n";
75
76 for(dead_mapt::const_iterator it=dead_map.begin();
77 it!=dead_map.end();
78 ++it)
79 it->second->output(os);
80}
81
82static void add_to_xml(
83 const irep_idt &function_identifier,
84 const goto_programt &goto_program,
85 const dead_mapt &dead_map,
86 xmlt &dest)
87{
88 xmlt &x = dest.new_element("function");
89 x.set_attribute("name", id2string(function_identifier));
90
91 for(dead_mapt::const_iterator it=dead_map.begin();
92 it!=dead_map.end();
93 ++it)
94 {
95 xmlt &inst = x.new_element("instruction");
96 inst.set_attribute("location_number",
97 std::to_string(it->second->location_number));
98 inst.set_attribute(
99 "source_location", it->second->source_location().as_string());
100 }
101 return;
102}
103
104static std::optional<std::string>
106{
107 if(source_location.get_file().empty())
108 return {};
109
110 return std::filesystem::path(
111 id2string(source_location.get_working_directory()))
112 .append(id2string(source_location.get_file()))
113 .string();
114}
115
116static void add_to_json(
117 const namespacet &ns,
118 const irep_idt &function_identifier,
119 const goto_programt &goto_program,
120 const dead_mapt &dead_map,
121 json_arrayt &dest)
122{
123 PRECONDITION(!goto_program.instructions.empty());
125 goto_program.instructions.end();
126 --end_function;
127 DATA_INVARIANT(end_function->is_end_function(),
128 "The last instruction in a goto-program must be END_FUNCTION");
129
130 json_objectt entry{{"function", json_stringt(function_identifier)}};
131 if(auto file_name_opt = file_name_string_opt(end_function->source_location()))
132 entry["file"] = json_stringt{*file_name_opt};
133
134 json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
135
136 for(dead_mapt::const_iterator it=dead_map.begin();
137 it!=dead_map.end();
138 ++it)
139 {
140 std::ostringstream oss;
141 it->second->output(oss);
142 std::string s=oss.str();
143
144 std::string::size_type n=s.find('\n');
145 CHECK_RETURN(n != std::string::npos);
146 s.erase(0, n+1);
147 n=s.find_first_not_of(' ');
148 CHECK_RETURN(n != std::string::npos);
149 s.erase(0, n);
150 CHECK_RETURN(!s.empty());
151 s.erase(s.size()-1);
152
153 // print info for file actually with full path
154 const source_locationt &l = it->second->source_location();
155 json_objectt i_entry{{"sourceLocation", json(l)},
156 {"statement", json_stringt(s)}};
157 dead_ins.push_back(std::move(i_entry));
158 }
159
160 dest.push_back(std::move(entry));
161}
162
164 const goto_modelt &goto_model,
165 const bool json,
166 std::ostream &os)
167{
169
170 std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
171
172 const namespacet ns(goto_model.symbol_table);
173
174 for(const auto &gf_entry : goto_model.goto_functions.function_map)
175 {
176 if(!gf_entry.second.body_available())
177 continue;
178
179 const goto_programt &goto_program = gf_entry.second.body;
180 dead_mapt dead_map;
181
182 const symbolt &decl = ns.lookup(gf_entry.first);
183
184 if(
185 called.find(decl.name) != called.end() ||
186 to_code_type(decl.type).get_inlined())
187 {
188 unreachable_instructions(goto_program, dead_map);
189 }
190 else
191 all_unreachable(goto_program, dead_map);
192
193 if(!dead_map.empty())
194 {
195 if(!json)
196 output_dead_plain(ns, gf_entry.first, goto_program, dead_map, os);
197 else
198 add_to_json(ns, gf_entry.first, goto_program, dead_map, json_result);
199 }
200 }
201
202 if(json && !json_result.empty())
203 os << json_result << '\n';
204}
205
207 const goto_modelt &goto_model,
208 const ai_baset &ai,
209 const optionst &options,
210 std::ostream &out)
211{
213 xmlt xml_result("unreachable-instructions");
214
215 const namespacet ns(goto_model.symbol_table);
216
217 for(const auto &gf_entry : goto_model.goto_functions.function_map)
218 {
219 if(!gf_entry.second.body_available())
220 continue;
221
222 const goto_programt &goto_program = gf_entry.second.body;
223 dead_mapt dead_map;
224 build_dead_map_from_ai(goto_program, ai, dead_map);
225
226 if(!dead_map.empty())
227 {
228 if(options.get_bool_option("json"))
229 {
231 ns, gf_entry.first, gf_entry.second.body, dead_map, json_result);
232 }
233 else if(options.get_bool_option("xml"))
234 {
235 add_to_xml(gf_entry.first, gf_entry.second.body, dead_map, xml_result);
236 }
237 else
238 {
239 // text or console
241 ns, gf_entry.first, gf_entry.second.body, dead_map, out);
242 }
243 }
244 }
245
246 if(options.get_bool_option("json") && !json_result.empty())
247 out << json_result << '\n';
248 else if(options.get_bool_option("xml"))
249 out << xml_result << '\n';
250
251 return false;
252}
253
254static std::optional<std::string>
255line_string_opt(const source_locationt &source_location)
256{
257 const irep_idt &line = source_location.get_line();
258
259 if(line.empty())
260 return {};
261 else
262 return id2string(line);
263}
264
266 const irep_idt &function,
269 json_arrayt &dest)
270{
271 json_objectt entry{{"function", json_stringt(function)}};
273 entry["file"] = json_stringt{*file_name_opt};
275 entry["firstLine"] = json_numbert{*line_opt};
277 entry["lastLine"] = json_numbert{*line_opt};
278
279 dest.push_back(std::move(entry));
280}
281
283 const irep_idt &function,
286 xmlt &dest)
287{
288 xmlt &x=dest.new_element("function");
289
290 x.set_attribute("name", id2string(function));
292 x.set_attribute("file", *file_name_opt);
294 x.set_attribute("first_line", *line_opt);
296 x.set_attribute("last_line", *line_opt);
297}
298
299static void list_functions(
300 const goto_modelt &goto_model,
301 const std::unordered_set<irep_idt> &called,
302 const optionst &options,
303 std::ostream &os,
304 bool unreachable)
305{
308 "unreachable-functions" :
309 "reachable-functions");
310
311 const namespacet ns(goto_model.symbol_table);
312
313 for(const auto &gf_entry : goto_model.goto_functions.function_map)
314 {
315 const symbolt &decl = ns.lookup(gf_entry.first);
316
317 if(
318 unreachable == (called.find(decl.name) != called.end() ||
319 to_code_type(decl.type).get_inlined()))
320 {
321 continue;
322 }
323
325
327 if(gf_entry.second.body_available())
328 {
329 const goto_programt &goto_program = gf_entry.second.body;
330
332 goto_program.instructions.end();
333
334 // find the last instruction with a line number
335 // TODO(tautschnig): #918 will eventually ensure that every instruction
336 // has such
337 do
338 {
339 --end_function;
340 last_location = end_function->source_location();
341 }
342 while(
343 end_function != goto_program.instructions.begin() &&
344 last_location.get_line().empty());
345
346 if(last_location.get_line().empty())
347 last_location = decl.location;
348 }
349 else
350 // completely ignore functions without a body, both for
351 // reachable and unreachable functions; we could also restrict
352 // this to macros/asm renaming
353 continue;
354
355 if(options.get_bool_option("json"))
356 {
358 decl.base_name,
362 }
363 else if(options.get_bool_option("xml"))
364 {
366 decl.base_name,
369 xml_result);
370 }
371 else
372 {
373 // text or console
375 os << *file_name_opt << ' ';
376 os << decl.base_name;
378 os << ' ' << *line_opt;
380 os << ' ' << *line_opt;
381 os << '\n';
382 }
383 }
384
385 if(options.get_bool_option("json") && !json_result.empty())
386 os << json_result << '\n';
387 else if(options.get_bool_option("xml"))
388 os << xml_result << '\n';
389}
390
392 const goto_modelt &goto_model,
393 const bool json,
394 std::ostream &os)
395{
396 optionst options;
397 if(json)
398 options.set_option("json", true);
399
400 std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
401
402 list_functions(goto_model, called, options, os, true);
403}
404
406 const goto_modelt &goto_model,
407 const bool json,
408 std::ostream &os)
409{
410 optionst options;
411 if(json)
412 options.set_option("json", true);
413
414 std::unordered_set<irep_idt> called = compute_called_functions(goto_model);
415
416 list_functions(goto_model, called, options, os, false);
417}
418
419std::unordered_set<irep_idt> compute_called_functions_from_ai(
420 const goto_modelt &goto_model,
421 const ai_baset &ai)
422{
423 std::unordered_set<irep_idt> called;
424
425 for(const auto &gf_entry : goto_model.goto_functions.function_map)
426 {
427 if(!gf_entry.second.body_available())
428 continue;
429
430 const goto_programt &p = gf_entry.second.body;
431
432 if(!ai.abstract_state_before(p.instructions.begin())->is_bottom())
433 called.insert(gf_entry.first);
434 }
435
436 return called;
437}
438
440 const goto_modelt &goto_model,
441 const ai_baset &ai,
442 const optionst &options,
443 std::ostream &out)
444{
445 std::unordered_set<irep_idt> called =
447
448 list_functions(goto_model, called, options, out, true);
449
450 return false;
451}
452
454 const goto_modelt &goto_model,
455 const ai_baset &ai,
456 const optionst &options,
457 std::ostream &out)
458{
459 std::unordered_set<irep_idt> called =
461
462 list_functions(goto_model, called, options, out, false);
463
464 return false;
465}
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:117
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
iterator end()
Definition cfg.h:118
iterator begin()
Definition cfg.h:114
entry_mapt entry_map
Definition cfg.h:152
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
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
jsont & push_back(const jsont &json)
Definition json.h:212
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
xmlt & new_element(const std::string &key)
Definition xml.h:95
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
Query Called Functions.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Options.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#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:788
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)
static std::optional< std::string > file_name_string_opt(const source_locationt &source_location)
bool static_reachable_functions(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
static std::optional< std::string > line_string_opt(const source_locationt &source_location)
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.