From cf85073aca6783b694f5c490a5f6a26153d3aa8c Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 8 Feb 2019 10:11:34 +0000 Subject: [PATCH 1/2] Java object factory: create initialiser using exact LHS type Previously the initialiser could have a followed (e.g. struct) type, while the LHS being set up could have a tag type. --- jbmc/src/java_bytecode/java_object_factory.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 9f9a52efec7..efa03aa81ca 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -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( From 814426b97f3518f4608be49f8a8d3896136a5622 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 8 Feb 2019 10:35:56 +0000 Subject: [PATCH 2/2] Object factory: assert exact type consistency At the moment --validate-goto-model doesn't give this strong a guarantee, but at least within the object factory we should only be producing exactly type-consistent statements. --- jbmc/src/java_bytecode/java_object_factory.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index efa03aa81ca..06e1d7f6fbc 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -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 @@ -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; } @@ -1628,6 +1645,7 @@ void gen_nondet_init( state.declare_created_symbols(init_code); + assert_type_consistency(assignments); init_code.append(assignments); }