@@ -31,6 +31,75 @@ the instrumenter.
31
31
#include < util/msgstream.h>
32
32
#include < summaries/summary_dump.h>
33
33
#include < exception>
34
+ #include < iostream>
35
+
36
+
37
+ /* ******************************************************************\
38
+
39
+ Function: remove_calls_to_functions_without_bodies
40
+
41
+ Inputs:
42
+
43
+ Outputs:
44
+
45
+ Purpose: The function remove all functions without bodies from the passed
46
+ goto_functions and symbol_table and also all call instructions
47
+ to those functions.
48
+
49
+ \*******************************************************************/
50
+ static void remove_calls_to_functions_without_bodies (
51
+ goto_functionst &goto_functions,
52
+ symbol_tablet &symbol_table)
53
+ {
54
+ std::set<irep_idt> fns_without_bodies;
55
+ for (auto &fname_prog : goto_functions.function_map )
56
+ {
57
+ std::vector<goto_programt::targett> to_remove;
58
+ for (auto it=fname_prog.second .body .instructions .begin ();
59
+ it!=fname_prog.second .body .instructions .end ();
60
+ ++it)
61
+ {
62
+ if (it->type ==FUNCTION_CALL)
63
+ {
64
+ auto fn_call=to_code_function_call (it->code );
65
+ if (fn_call.function ().id ()==ID_symbol)
66
+ {
67
+ auto s=to_symbol_expr (fn_call.function ());
68
+ auto fit=goto_functions.function_map .find (s.get_identifier ());
69
+ if (fit==goto_functions.function_map .end () ||
70
+ fit->second .body .instructions .empty ())
71
+ {
72
+ fns_without_bodies.insert (s.get_identifier ());
73
+ to_remove.push_back (it);
74
+ ++it;
75
+ if (it!=fname_prog.second .body .instructions .end () &&
76
+ it->type ==ASSIGN)
77
+ {
78
+ auto asgn=to_code_assign (it->code );
79
+ if (asgn.lhs ().id ()==ID_symbol)
80
+ {
81
+ auto lhs=to_symbol_expr (asgn.lhs ());
82
+ if (as_string (lhs.get_identifier ())==
83
+ as_string (s.get_identifier ())+RETURN_VALUE_SUFFIX)
84
+ {
85
+ to_remove.push_back (it);
86
+ }
87
+ }
88
+ }
89
+ }
90
+ }
91
+ }
92
+ }
93
+ for (auto &tgt : to_remove)
94
+ {
95
+ assert (tgt->targets .empty ());
96
+ tgt->make_skip ();
97
+ }
98
+ }
99
+ for (const auto &fn_name : fns_without_bodies)
100
+ symbol_table.remove (fn_name);
101
+ }
102
+
34
103
35
104
/* ******************************************************************\
36
105
@@ -55,6 +124,7 @@ Function: add_nondet_retval_assignments_after_calls
55
124
\*******************************************************************/
56
125
static void add_nondet_retval_assignments_after_calls (
57
126
goto_programt &goto_program,
127
+ const irep_idt &caller_name,
58
128
const std::string &callee_name,
59
129
const typet &callee_ret_type)
60
130
{
@@ -75,6 +145,7 @@ static void add_nondet_retval_assignments_after_calls(
75
145
instr_it->code =code_assignt (
76
146
symbol_exprt (callee_name+RETURN_VALUE_SUFFIX,callee_ret_type),
77
147
side_effect_expr_nondett (callee_ret_type));
148
+ instr_it->function =caller_name;
78
149
}
79
150
}
80
151
}
@@ -156,6 +227,7 @@ std::pair<taint_slicing_taskt,std::string> build_slicing_task(
156
227
if (fid_fn.second .body_available ())
157
228
add_nondet_retval_assignments_after_calls (
158
229
fid_fn.second .body ,
230
+ fid_fn.first ,
159
231
fid,
160
232
symbol_table.lookup (fid+RETURN_VALUE_SUFFIX).type );
161
233
}
@@ -201,6 +273,11 @@ std::pair<taint_slicing_taskt,std::string> build_slicing_task(
201
273
}
202
274
}
203
275
276
+ // And we do the final clean-up: we remove all functions without bodies
277
+ // from the goto_functions and symbol_table and also all call instructions
278
+ // to those functions.
279
+ remove_calls_to_functions_without_bodies (goto_functions, symbol_table);
280
+
204
281
// Finally, we have to "update" the GOTO program - mandatory step fixing
205
282
// uniquenes of program locations, etc.
206
283
goto_functions.update ();
@@ -230,6 +307,23 @@ std::pair<taint_slicing_taskt,std::string> build_slicing_task(
230
307
std::atoi (loc.get_line ().c_str ())});
231
308
}
232
309
310
+ // Check for issues in the program w.r.t. requirements of the slicer
311
+ // and try to fix them.
312
+ for (auto &fname_prog : goto_functions.function_map )
313
+ for (auto &I : fname_prog.second .body .instructions )
314
+ if (I.function .empty ())
315
+ {
316
+ logger->status ()
317
+ << " WARNING: Instruction without 'function' reference:\n "
318
+ << " loc.: " << I.location_number << " \n "
319
+ << " func: " << fname_prog.first << " \n "
320
+ << " code: " ;
321
+ dump_instruction_code_in_html (
322
+ I, namespacet (symbol_table), logger->status ());
323
+ logger->status () << " \n Fixing the issue.\n " ;
324
+ I.function =fname_prog.first ;
325
+ }
326
+
233
327
// Finally save the constructed slicing task on the disc as GOTO program
234
328
// binary.
235
329
const bool fail=write_goto_binary (
0 commit comments