Skip to content

Commit 77ac3a2

Browse files
committed
Fix Java object factory recursion set
Previously it was vulnerable to indirect recursion (i.e. A has a B*, B has an A*); this removes that possibility and also simplifies use of the recursion set to only consider pointer edges rather than directly nested struct types, which can't be used to construct an infinite object graph by themselves. This should address some of the cases of prematurely truncated object graphs the incorrect recursion test was trying to solve.
1 parent 935825e commit 77ac3a2

File tree

1 file changed

+2
-7
lines changed

1 file changed

+2
-7
lines changed

src/java_bytecode/java_object_factory.cpp

+2-7
Original file line numberDiff line numberDiff line change
@@ -316,9 +316,8 @@ void java_object_factoryt::gen_nondet_init(
316316
{
317317
const struct_typet &struct_type=to_struct_type(subtype);
318318
const irep_idt struct_tag=struct_type.get_tag();
319-
// set to null if found in recursion set and not a sub-type
320-
if(recursion_set.find(struct_tag)!=recursion_set.end() &&
321-
struct_tag==class_identifier)
319+
// If this is a recursive type of some kind, set null.
320+
if(!recursion_set.insert(struct_tag).second)
322321
{
323322
if(update_in_place==NO_UPDATE_IN_PLACE)
324323
set_null(expr, pointer_type);
@@ -403,9 +402,6 @@ void java_object_factoryt::gen_nondet_init(
403402
if(!is_sub)
404403
class_identifier=struct_tag;
405404

406-
recursion_set.insert(struct_tag);
407-
assert(!recursion_set.empty());
408-
409405
for(const auto &component : components)
410406
{
411407
const typet &component_type=component.type();
@@ -460,7 +456,6 @@ void java_object_factoryt::gen_nondet_init(
460456
substruct_in_place);
461457
}
462458
}
463-
recursion_set.erase(struct_tag);
464459
}
465460
else
466461
{

0 commit comments

Comments
 (0)