From 625265fc6064efd5566e3824b1c2488bb2db32cd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jan 2022 16:32:02 +0000 Subject: [PATCH] Java front-end and allocate objects: reduce reliance on goto code types Code that deals with symbol tables only should not create codet structures defined in goto-programs/goto_instruction_code.h. code_function_callt remains in place as an exception to this rule as the Java front-end wide relies on it. --- .../java_bytecode/assignments_from_json.cpp | 65 ++++++++++--------- .../java_static_initializers.cpp | 21 +++--- jbmc/src/java_bytecode/nondet.cpp | 2 +- .../java_bytecode/simple_method_stubbing.cpp | 4 +- src/goto-programs/allocate_objects.cpp | 4 +- src/goto-programs/allocate_objects.h | 3 - 6 files changed, 52 insertions(+), 47 deletions(-) diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index 83a937baf89..4e6a240cfe5 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -8,16 +8,6 @@ Author: Diffblue Ltd. #include "assignments_from_json.h" -#include "ci_lazy_methods_needed.h" -#include "code_with_references.h" -#include "java_static_initializers.h" -#include "java_string_literals.h" -#include "java_types.h" -#include "java_utils.h" - -#include -#include - #include #include #include @@ -26,6 +16,17 @@ Author: Diffblue Ltd. #include #include +#include +#include +#include + +#include "ci_lazy_methods_needed.h" +#include "code_with_references.h" +#include "java_static_initializers.h" +#include "java_string_literals.h" +#include "java_types.h" +#include "java_utils.h" + /// Values passed around between most functions of the recursive deterministic /// assignment algorithm entered from \ref assign_from_json. /// The values in a given `object_creation_infot` are never reassigned, but the @@ -345,43 +346,44 @@ assign_primitive_from_json(const exprt &expr, const jsont &json) return result; if(expr.type() == java_boolean_type()) { - result.add(code_assignt{ + result.add(code_frontend_assignt{ expr, json.is_true() ? (exprt)true_exprt{} : (exprt)false_exprt{}}); } else if( expr.type() == java_int_type() || expr.type() == java_byte_type() || expr.type() == java_short_type() || expr.type() == java_long_type()) { - result.add( - code_assignt{expr, from_integer(std::stoll(json.value), expr.type())}); + result.add(code_frontend_assignt{ + expr, from_integer(std::stoll(json.value), expr.type())}); } else if(expr.type() == java_double_type()) { ieee_floatt ieee_float(to_floatbv_type(expr.type())); ieee_float.from_double(std::stod(json.value)); - result.add(code_assignt{expr, ieee_float.to_expr()}); + result.add(code_frontend_assignt{expr, ieee_float.to_expr()}); } else if(expr.type() == java_float_type()) { ieee_floatt ieee_float(to_floatbv_type(expr.type())); ieee_float.from_float(std::stof(json.value)); - result.add(code_assignt{expr, ieee_float.to_expr()}); + result.add(code_frontend_assignt{expr, ieee_float.to_expr()}); } else if(expr.type() == java_char_type()) { const std::wstring wide_value = utf8_to_utf16_native_endian(json.value); PRECONDITION(wide_value.length() == 1); - result.add( - code_assignt{expr, from_integer(wide_value.front(), expr.type())}); + result.add(code_frontend_assignt{ + expr, from_integer(wide_value.front(), expr.type())}); } return result; } /// One of the base cases of the recursive algorithm. See /// \ref assign_from_json_rec. -static code_assignt assign_null(const exprt &expr) +static code_frontend_assignt assign_null(const exprt &expr) { - return code_assignt{expr, null_pointer_exprt{to_pointer_type(expr.type())}}; + return code_frontend_assignt{ + expr, null_pointer_exprt{to_pointer_type(expr.type())}}; } /// In the case of an assignment of an array given a JSON representation, this @@ -405,7 +407,8 @@ static code_with_references_listt assign_array_data_component_from_json( info.allocate_objects.allocate_automatic_local_object( data_member_expr.type(), "user_specified_array_data_init"); code_with_references_listt result; - result.add(code_assignt{array_init_data, data_member_expr, info.loc}); + result.add( + code_frontend_assignt{array_init_data, data_member_expr, info.loc}); size_t index = 0; const optionalt inferred_element_type = @@ -432,8 +435,8 @@ nondet_length(allocate_objectst &allocate, source_locationt loc) symbol_exprt length_expr = allocate.allocate_automatic_local_object( java_int_type(), "user_specified_array_length"); code_with_references_listt code; - code.add( - code_assignt{length_expr, side_effect_expr_nondett{java_int_type(), loc}}); + code.add(code_frontend_assignt{ + length_expr, side_effect_expr_nondett{java_int_type(), loc}}); code.add(code_assumet{binary_predicate_exprt{ length_expr, ID_ge, from_integer(0, java_int_type())}}); return std::make_pair(length_expr, std::move(code)); @@ -506,16 +509,17 @@ static code_with_references_listt assign_nondet_length_array_from_json( /// One of the cases in the recursive algorithm: the case where \p expr /// represents a string. /// See \ref assign_from_json_rec. -static code_assignt assign_string_from_json( +static code_frontend_assignt assign_string_from_json( const jsont &json, const exprt &expr, object_creation_infot &info) { const auto json_string = get_untyped_string(json); PRECONDITION(json_string.is_string()); - return code_assignt{expr, - get_or_create_string_literal_symbol( - json_string.value, info.symbol_table, true)}; + return code_frontend_assignt{ + expr, + get_or_create_string_literal_symbol( + json_string.value, info.symbol_table, true)}; } /// Helper function for \ref assign_struct_from_json which recursively assigns @@ -586,7 +590,7 @@ static code_with_references_listt assign_struct_from_json( to_struct_expr(*initial_object), ns, struct_tag_typet("java::" + id2string(java_class_type.get_tag()))); - result.add(code_assignt{expr, *initial_object}); + result.add(code_frontend_assignt{expr, *initial_object}); result.append(assign_struct_components_from_json(expr, json, info)); } return result; @@ -646,7 +650,7 @@ static code_with_references_listt assign_enum_from_json( const exprt ordinal_expr = from_integer(std::stoi(json["ordinal"].value), java_int_type()); - result.add(code_assignt{ + result.add(code_frontend_assignt{ expr, typecast_exprt::conditional_cast( array_element_from_pointer(values_data, ordinal_expr), expr.type())}); @@ -696,7 +700,8 @@ static code_with_references_listt assign_pointer_with_given_type_from_json( } auto result = assign_pointer_from_json(new_symbol, json, info); - result.add(code_assignt{expr, typecast_exprt{new_symbol, pointer_type}}); + result.add( + code_frontend_assignt{expr, typecast_exprt{new_symbol, pointer_type}}); return result; } else @@ -828,7 +833,7 @@ static code_with_references_listt assign_reference_from_json( assign_struct_from_json(dereference_exprt(reference.expr), json, info)); } } - result.add(code_assignt{ + result.add(code_frontend_assignt{ expr, typecast_exprt::conditional_cast(reference.expr, expr.type())}); return result; } diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 5e97df5a83f..b424b33df89 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -8,15 +8,6 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "java_static_initializers.h" -#include "assignments_from_json.h" -#include "ci_lazy_methods_needed.h" -#include "java_object_factory.h" -#include "java_object_factory_parameters.h" -#include "java_types.h" -#include "java_utils.h" - -#include - #include #include #include @@ -24,6 +15,16 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include +#include +#include + +#include "assignments_from_json.h" +#include "ci_lazy_methods_needed.h" +#include "java_object_factory.h" +#include "java_object_factory_parameters.h" +#include "java_types.h" +#include "java_utils.h" + /// The three states in which a `` method for a class can be before, /// after, and during static class initialization. These states are only used /// when the thread safe version of the clinit wrapper is generated. @@ -580,7 +581,7 @@ code_blockt get_thread_safe_clinit_wrapper_body( // bool init_complete; { - code_declt decl(init_complete.symbol_expr()); + code_frontend_declt decl(init_complete.symbol_expr()); function_body.add(decl); } diff --git a/jbmc/src/java_bytecode/nondet.cpp b/jbmc/src/java_bytecode/nondet.cpp index 26ee6036080..3a6092092ab 100644 --- a/jbmc/src/java_bytecode/nondet.cpp +++ b/jbmc/src/java_bytecode/nondet.cpp @@ -49,7 +49,7 @@ symbol_exprt generate_nondet_int( // Declare a symbol for the non deterministic integer. const symbol_exprt &nondet_symbol = alocate_local_symbol(int_type, basename_prefix); - instructions.add(code_declt(nondet_symbol)); + instructions.add(code_frontend_declt(nondet_symbol)); // Assign the symbol any non deterministic integer value. // int_type name_prefix::nondet_int = NONDET(int_type) diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp index 77cf3dd7d8d..06f3908e0c9 100644 --- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp +++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp @@ -188,7 +188,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol) symbol.name, symbol_table); const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr(); - code_assignt get_argument( + code_frontend_assignt get_argument( init_symbol_expression, symbol_exprt(this_argument.get_identifier(), this_type)); get_argument.add_source_location() = synthesized_source_location; @@ -242,7 +242,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol) 0, false, false); - new_instructions.add(code_returnt(to_return)); + new_instructions.add(code_frontend_returnt(to_return)); } } diff --git a/src/goto-programs/allocate_objects.cpp b/src/goto-programs/allocate_objects.cpp index 91de4260ea0..7c743725b33 100644 --- a/src/goto-programs/allocate_objects.cpp +++ b/src/goto-programs/allocate_objects.cpp @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "goto_instruction_code.h" + /// Allocates a new object, either by creating a local variable with automatic /// lifetime, a global variable with static lifetime, or by dynamically /// allocating memory via ALLOCATE(). Code is added to `assignments` which @@ -233,7 +235,7 @@ void allocate_objectst::declare_created_symbols(code_blockt &init_code) const symbolt &symbol = ns.lookup(symbol_id); if(!symbol.is_static_lifetime) { - code_declt decl{symbol.symbol_expr()}; + code_frontend_declt decl{symbol.symbol_expr()}; decl.add_source_location() = source_location; init_code.add(decl); } diff --git a/src/goto-programs/allocate_objects.h b/src/goto-programs/allocate_objects.h index cd5ba334c5f..bdef7c5edf8 100644 --- a/src/goto-programs/allocate_objects.h +++ b/src/goto-programs/allocate_objects.h @@ -9,10 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H #define CPROVER_UTIL_ALLOCATE_OBJECTS_H -#include "goto_instruction_code.h" - #include -#include #include /// Selects the kind of objects allocated