Skip to content

Commit 09efc90

Browse files
author
Matthias Güdemann
committed
Re-Resolve function calls if only java.lang.Object was found.
This fixes an issue in test-generator where a call to `toString` is dispatched to the `toString` method from `java.lang.Object` is used instead of the overridden method from `ArrayList`. Cite from the issue about the current implementation: > It tracks a `visited` set preventing it from listing callees twice when > multiple inheritance is in play (e.g. Java interfaces). Unfortunately this > malfunctions when we visit a type twice, once via its interfaces and once via > its concrete subclass which provides a definition This extends the original implementation, by resolving dispatch entries where an initial step resolved to a java.lang.Object function. This case can be an error, as some classes might be visited multiple times, first for an interface and then for the concrete class. The original implementation kept a visited set that recorded visited classes which resulted in some functions not correctly being resolved. This set is replaced with a map from class identifiers to dispatch table entries.
1 parent a619e48 commit 09efc90

File tree

2 files changed

+101
-22
lines changed

2 files changed

+101
-22
lines changed

src/goto-programs/remove_virtual_functions.cpp

+100-22
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ class remove_virtual_functionst
5757
const symbol_exprt &,
5858
const irep_idt &,
5959
dispatch_table_entriest &,
60-
std::set<irep_idt> &visited,
60+
dispatch_table_entries_mapt &,
6161
const function_call_resolvert &) const;
6262
exprt
6363
get_method(const irep_idt &class_id, const irep_idt &component_name) const;
@@ -163,11 +163,18 @@ void remove_virtual_functionst::remove_virtual_function(
163163
newinst->source_location=vcall_source_loc;
164164
}
165165

166+
// get initial identifier for grouping
167+
INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");
168+
auto last_id = functions.back().symbol_expr.get_identifier();
169+
// record class_ids for disjunction
170+
std::set<irep_idt> class_ids;
171+
166172
std::map<irep_idt, goto_programt::targett> calls;
167173
// Note backwards iteration, to get the fallback candidate first.
168174
for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
169175
{
170176
const auto &fun=*it;
177+
class_ids.insert(fun.class_id);
171178
auto insertit=calls.insert(
172179
{fun.symbol_expr.get_identifier(), goto_programt::targett()});
173180

@@ -209,15 +216,50 @@ void remove_virtual_functionst::remove_virtual_function(
209216
t3->make_goto(t_final, true_exprt());
210217
}
211218

219+
// Emit target if end of dispatch table is reached or if the next element is
220+
// dispatched to another function call. Assumes entries in the functions
221+
// variable to be sorted for the identifier of the function to be called.
222+
auto l_it = std::next(it);
223+
bool next_emit_target =
224+
(l_it == functions.crend()) ||
225+
l_it->symbol_expr.get_identifier() != fun.symbol_expr.get_identifier();
226+
227+
// The root function call is done via fall-through, so nothing to emit
228+
// explicitly for this.
229+
if(next_emit_target && fun.symbol_expr == last_function_symbol)
230+
{
231+
class_ids.clear();
232+
}
233+
212234
// If this calls the fallback function we just fall through.
213235
// Otherwise branch to the right call:
214236
if(fallback_action!=virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION ||
215237
fun.symbol_expr!=last_function_symbol)
216238
{
217-
exprt c_id1=constant_exprt(fun.class_id, string_typet());
218-
goto_programt::targett t4=new_code_gotos.add_instruction();
219-
t4->source_location=vcall_source_loc;
220-
t4->make_goto(insertit.first->second, equal_exprt(c_id1, c_id2));
239+
// create a disjunction of class_ids to test
240+
if(next_emit_target && fun.symbol_expr != last_function_symbol)
241+
{
242+
exprt::operandst or_ops;
243+
for(const auto &id : class_ids)
244+
{
245+
const constant_exprt c_id1(id, string_typet());
246+
const equal_exprt class_id_test(c_id1, c_id2);
247+
or_ops.push_back(class_id_test);
248+
}
249+
250+
goto_programt::targett t4 = new_code_gotos.add_instruction();
251+
t4->source_location = vcall_source_loc;
252+
t4->make_goto(insertit.first->second, disjunction(or_ops));
253+
254+
last_id = fun.symbol_expr.get_identifier();
255+
class_ids.clear();
256+
}
257+
// record class_id
258+
else if(next_emit_target)
259+
{
260+
last_id = fun.symbol_expr.get_identifier();
261+
class_ids.clear();
262+
}
221263
}
222264
}
223265

@@ -252,11 +294,12 @@ void remove_virtual_functionst::remove_virtual_function(
252294

253295
/// Used by get_functions to track the most-derived parent that provides an
254296
/// override of a given function.
255-
/// \par parameters: `this_id`: class name
256-
/// `last_method_defn`: the most-derived parent of `this_id` to define the
257-
/// requested function
258-
/// `component_name`: name of the function searched for
259-
/// `resolve_function_call`: function to resolve abstract method call
297+
/// \param parameters: `this_id`: class name
298+
/// \param `last_method_defn`: the most-derived parent of `this_id` to define
299+
/// the requested function
300+
/// \param `component_name`: name of the function searched for
301+
/// \param `entry_map`: map of class identifiers to dispatch table entries
302+
/// \param `resolve_function_call`: function to resolve abstract method call
260303
/// \return `functions` is assigned a list of {class name, function symbol}
261304
/// pairs indicating that if `this` is of the given class, then the call will
262305
/// target the given function. Thus if A <: B <: C and A and C provide
@@ -267,7 +310,7 @@ void remove_virtual_functionst::get_child_functions_rec(
267310
const symbol_exprt &last_method_defn,
268311
const irep_idt &component_name,
269312
dispatch_table_entriest &functions,
270-
std::set<irep_idt> &visited,
313+
dispatch_table_entries_mapt &entry_map,
271314
const function_call_resolvert &resolve_function_call) const
272315
{
273316
auto findit=class_hierarchy.class_map.find(this_id);
@@ -276,9 +319,18 @@ void remove_virtual_functionst::get_child_functions_rec(
276319

277320
for(const auto &child : findit->second.children)
278321
{
279-
if(!visited.insert(child).second)
322+
// Skip if we have already visited this and we found a function call that
323+
// did not resolve to non java.lang.Object.
324+
auto it = entry_map.find(child);
325+
if(
326+
it != entry_map.end() &&
327+
!has_prefix(
328+
id2string(it->second.symbol_expr.get_identifier()),
329+
"java::java.lang.Object"))
330+
{
280331
continue;
281-
exprt method=get_method(child, component_name);
332+
}
333+
exprt method = get_method(child, component_name);
282334
dispatch_table_entryt function(child);
283335
if(method.is_not_nil())
284336
{
@@ -305,37 +357,43 @@ void remove_virtual_functionst::get_child_functions_rec(
305357
}
306358
}
307359
functions.push_back(function);
360+
entry_map.insert({child, function});
308361

309362
get_child_functions_rec(
310363
child,
311364
function.symbol_expr,
312365
component_name,
313366
functions,
314-
visited,
367+
entry_map,
315368
resolve_function_call);
316369
}
317370
}
318371

372+
/// Used to get dispatch entries to call for the given function
373+
/// \param function: function that should be called
374+
/// \param[out] functions: is assigned a list of dispatch entries, i.e., pairs
375+
/// of class names and function symbol to call when encountering the class.
319376
void remove_virtual_functionst::get_functions(
320377
const exprt &function,
321378
dispatch_table_entriest &functions)
322379
{
380+
// class part of function to call
323381
const irep_idt class_id=function.get(ID_C_class);
324382
const std::string class_id_string(id2string(class_id));
325-
const irep_idt component_name=function.get(ID_component_name);
326-
const std::string component_name_string(id2string(component_name));
383+
const irep_idt function_name = function.get(ID_component_name);
384+
const std::string function_name_string(id2string(function_name));
327385
INVARIANT(!class_id.empty(), "All virtual functions must have a class");
328386

329387
resolve_concrete_function_callt get_virtual_call_target(
330388
symbol_table, class_hierarchy);
331389
const function_call_resolvert resolve_function_call =
332390
[&get_virtual_call_target](
333-
const irep_idt &class_id, const irep_idt &component_name) {
334-
return get_virtual_call_target(class_id, component_name);
391+
const irep_idt &class_id, const irep_idt &function_name) {
392+
return get_virtual_call_target(class_id, function_name);
335393
};
336394

337395
const resolve_concrete_function_callt::concrete_function_callt
338-
&resolved_call = get_virtual_call_target(class_id, component_name);
396+
&resolved_call = get_virtual_call_target(class_id, function_name);
339397

340398
dispatch_table_entryt root_function;
341399

@@ -357,17 +415,37 @@ void remove_virtual_functionst::get_functions(
357415
}
358416

359417
// iterate over all children, transitively
360-
std::set<irep_idt> visited;
418+
dispatch_table_entries_mapt entry_map;
361419
get_child_functions_rec(
362420
class_id,
363421
root_function.symbol_expr,
364-
component_name,
422+
function_name,
365423
functions,
366-
visited,
424+
entry_map,
367425
resolve_function_call);
368426

369427
if(root_function.symbol_expr!=symbol_exprt())
370428
functions.push_back(root_function);
429+
430+
// Sort for the identifier of the function call symbol expression, grouping
431+
// together calls to the same function. Keep java.lang.Object entries at the
432+
// end for fall through. The reasoning is that this is the case with most
433+
// entries in realistic cases.
434+
std::sort(
435+
functions.begin(),
436+
functions.end(),
437+
[&root_function](const dispatch_table_entryt &a, dispatch_table_entryt &b) {
438+
if(
439+
has_prefix(
440+
id2string(a.symbol_expr.get_identifier()), "java::java.lang.Object"))
441+
return false;
442+
else if(
443+
has_prefix(
444+
id2string(b.symbol_expr.get_identifier()), "java::java.lang.Object"))
445+
return true;
446+
else
447+
return a.symbol_expr.get_identifier() < b.symbol_expr.get_identifier();
448+
});
371449
}
372450

373451
exprt remove_virtual_functionst::get_method(

src/goto-programs/remove_virtual_functions.h

+1
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@ class dispatch_table_entryt
5656
};
5757

5858
typedef std::vector<dispatch_table_entryt> dispatch_table_entriest;
59+
typedef std::map<irep_idt, dispatch_table_entryt> dispatch_table_entries_mapt;
5960

6061
void remove_virtual_function(
6162
goto_modelt &goto_model,

0 commit comments

Comments
 (0)