Skip to content

Object factory: ensure generated assignments are exactly type-consistent [blocks: #3966] #4126

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Feb 8, 2019
Merged

Object factory: ensure generated assignments are exactly type-consistent [blocks: #3966] #4126

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cf85073
Java object factory: create initialiser using exact LHS type
smowton Feb 8, 2019
814426b
Object factory: assert exact type consistency
smowton Feb 8, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 19 additions & 1 deletion jbmc/src/java_bytecode/java_object_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -890,7 +890,7 @@ void java_object_factoryt::gen_nondet_struct_init(

// This code mirrors the `remove_java_new` pass:
auto initial_object =
zero_initializer(struct_type, source_locationt(), ns);
zero_initializer(expr.type(), source_locationt(), ns);
CHECK_RETURN(initial_object.has_value());
const irep_idt qualified_clsid = "java::" + id2string(class_identifier);
set_class_identifier(
Expand Down Expand Up @@ -1498,6 +1498,22 @@ void java_object_factoryt::gen_nondet_enum_init(
assignments.add(enum_assign);
}

static void assert_type_consistency(const code_blockt &assignments)
{
// In future we'll be able to use codet::validate for this;
// at present that only verifies `lhs.type base_type_eq right.type`,
// whereas we want to check exact equality.
for(const auto &code : assignments.statements())
{
if(code.get_statement() != ID_assign)
continue;
const auto &assignment = to_code_assign(code);
INVARIANT(
assignment.lhs().type() == assignment.rhs().type(),
"object factory should produce type-consistent assignments");
}
}

/// Similar to `gen_nondet_init` below, but instead of allocating and
/// non-deterministically initializing the the argument `expr` passed to that
/// function, we create a static global object of type \p type and
Expand Down Expand Up @@ -1558,6 +1574,7 @@ exprt object_factory(
state.add_created_symbol(main_symbol_ptr);
state.declare_created_symbols(init_code);

assert_type_consistency(assignments);
init_code.append(assignments);
return object;
}
Expand Down Expand Up @@ -1628,6 +1645,7 @@ void gen_nondet_init(

state.declare_created_symbols(init_code);

assert_type_consistency(assignments);
init_code.append(assignments);
}

Expand Down