From 998b16361cd76af53aee92dec27550c27137a8ad Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 11 Oct 2021 20:16:29 +0100 Subject: [PATCH] introduce code_frontend_assignt Basically all frontends are using code_assignt, which is meant to be used in goto program instructions only. This commit separates out the two uses. --- .../java_bytecode/code_with_references.cpp | 6 +- .../create_array_with_type_intrinsic.cpp | 9 +- .../java_bytecode_convert_class.cpp | 9 +- .../java_bytecode_typecheck_code.cpp | 2 +- jbmc/src/java_bytecode/java_entry_point.cpp | 19 ++- .../src/java_bytecode/java_object_factory.cpp | 43 +++---- .../java_static_initializers.cpp | 18 +-- jbmc/src/java_bytecode/lambda_synthesis.cpp | 4 +- src/ansi-c/ansi_c_entry_point.cpp | 2 +- src/ansi-c/c_nondet_symbol_factory.cpp | 10 +- .../c_typecheck_gcc_polymorphic_builtins.cpp | 47 ++++---- src/ansi-c/c_typecheck_type.cpp | 2 +- src/ansi-c/expr2c.cpp | 6 +- src/ansi-c/expr2c_class.h | 3 +- src/cpp/cpp_typecheck_constructor.cpp | 6 +- src/cpp/cpp_typecheck_destructor.cpp | 2 +- src/cpp/cpp_typecheck_initializer.cpp | 4 +- src/util/allocate_objects.cpp | 18 +-- src/util/allocate_objects.h | 3 +- src/util/nondet.cpp | 2 +- src/util/std_code.cpp | 2 +- src/util/std_code.h | 113 +++++++++++++++++- 22 files changed, 225 insertions(+), 105 deletions(-) diff --git a/jbmc/src/java_bytecode/code_with_references.cpp b/jbmc/src/java_bytecode/code_with_references.cpp index 61d3aa4048d..0ccd76b6351 100644 --- a/jbmc/src/java_bytecode/code_with_references.cpp +++ b/jbmc/src/java_bytecode/code_with_references.cpp @@ -23,7 +23,7 @@ codet allocate_array( pointer_type.subtype().set(ID_element_type, element_type); side_effect_exprt java_new_array{ ID_java_new_array, {array_length_expr}, pointer_type, loc}; - return code_assignt{expr, java_new_array, loc}; + return code_frontend_assignt{expr, java_new_array, loc}; } code_blockt @@ -41,8 +41,8 @@ reference_allocationt::to_code(reference_substitutiont &references) const // or the "@id" json field corresponding to `reference_id` doesn't appear in // the file. code_blockt code; - code.add(code_assignt{*reference.array_length, - side_effect_expr_nondett{java_int_type(), loc}}); + code.add(code_frontend_assignt{ + *reference.array_length, side_effect_expr_nondett{java_int_type(), loc}}); code.add(code_assumet{binary_predicate_exprt{ *reference.array_length, ID_ge, from_integer(0, java_int_type())}}); code.add(allocate_array(reference.expr, *reference.array_length, loc)); diff --git a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp index 8dab3198699..e895d7d7d7a 100644 --- a/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp +++ b/jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp @@ -14,9 +14,9 @@ Author: Diffblue Ltd. #include #include -#include #include #include +#include #include /// Returns the symbol name for `org.cprover.CProver.createArrayWithType` @@ -81,7 +81,7 @@ codet create_array_with_type_body( side_effect_exprt new_array_expr{ ID_java_new_array, new_array_symbol.type, source_locationt{}}; new_array_expr.copy_to_operands(length_argument_symbol_expr); - code_block.add(code_assignt(new_array_symbol_expr, new_array_expr)); + code_block.add(code_frontend_assignt(new_array_symbol_expr, new_array_expr)); dereference_exprt existing_array(existing_array_argument_symbol_expr); dereference_exprt new_array(new_array_symbol_expr); @@ -99,9 +99,10 @@ codet create_array_with_type_body( member_exprt new_array_element_classid( new_array, JAVA_ARRAY_ELEMENT_CLASSID_FIELD_NAME, string_typet()); - code_block.add(code_assignt(new_array_dimension, old_array_dimension)); code_block.add( - code_assignt(new_array_element_classid, old_array_element_classid)); + code_frontend_assignt(new_array_dimension, old_array_dimension)); + code_block.add(code_frontend_assignt( + new_array_element_classid, old_array_element_classid)); // return new_array code_block.add(code_returnt(new_array_symbol_expr)); diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 9b8e12e33ad..fbad011e704 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -909,7 +909,7 @@ void add_java_array_types(symbol_tablet &symbol_table) member_exprt old_length( old_array, length_component.get_name(), length_component.type()); java_new_array.copy_to_operands(old_length); - code_assignt create_blank(local_symexpr, java_new_array); + code_frontend_assignt create_blank(local_symexpr, java_new_array); codet copy_type_information = code_skipt(); if(l == 'a') @@ -930,8 +930,9 @@ void add_java_array_types(symbol_tablet &symbol_table) new_array, array_element_classid_component); copy_type_information = code_blockt{ - {code_assignt(new_array_dimension, old_array_dimension), - code_assignt(new_array_element_classid, old_array_element_classid)}}; + {code_frontend_assignt(new_array_dimension, old_array_dimension), + code_frontend_assignt( + new_array_element_classid, old_array_element_classid)}}; } member_exprt old_data( @@ -971,7 +972,7 @@ void add_java_array_types(symbol_tablet &symbol_table) from_integer(0, index_symexpr.type()), old_length, index_symexpr, - code_assignt(std::move(new_cell), std::move(old_cell)), + code_frontend_assignt(std::move(new_cell), std::move(old_cell)), location); member_exprt new_base_class( diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp index 652fc2d6713..dcad9bbdf59 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_code.cpp @@ -19,7 +19,7 @@ void java_bytecode_typecheckt::typecheck_code(codet &code) if(statement==ID_assign) { - code_assignt &code_assign=to_code_assign(code); + code_frontend_assignt &code_assign = to_code_frontend_assign(code); typecheck_expr(code_assign.lhs()); typecheck_expr(code_assign.rhs()); diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 193806c15b6..02d235a9446 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -122,8 +122,8 @@ void java_static_lifetime_init( const symbol_exprt rounding_mode = symbol_table.lookup_ref(rounding_mode_identifier()).symbol_expr(); - code_block.add( - code_assignt{rounding_mode, from_integer(0, rounding_mode.type())}); + code_block.add(code_frontend_assignt{rounding_mode, + from_integer(0, rounding_mode.type())}); object_factory_parameters.function_id = initialize_symbol.name; @@ -226,7 +226,7 @@ void java_static_lifetime_init( to_struct_expr(*zero_object), ns, to_struct_tag_type(sym.type)); code_block.add( - std::move(code_assignt(sym.symbol_expr(), *zero_object))); + std::move(code_frontend_assignt(sym.symbol_expr(), *zero_object))); // Then call the init function: code_block.add(std::move(initializer_call)); @@ -257,7 +257,7 @@ void java_static_lifetime_init( } else if(sym.value.is_not_nil()) { - code_assignt assignment(sym.symbol_expr(), sym.value); + code_frontend_assignt assignment(sym.symbol_expr(), sym.value); assignment.add_source_location()=source_location; code_block.add(assignment); } @@ -333,7 +333,7 @@ std::pair> java_build_arguments( .symbol_expr(); main_arguments[param_number] = result; init_code.add(code_declt{result}); - init_code.add(code_assignt{ + init_code.add(code_frontend_assignt{ result, side_effect_exprt{ID_java_new, {}, p.type(), function.location}}); continue; @@ -417,10 +417,9 @@ std::pair> java_build_arguments( function.location, pointer_type_selector, message_handler); - init_code_for_type.add( - code_assignt( - result_symbol.symbol_expr(), - typecast_exprt(init_expr_for_parameter, p.type()))); + init_code_for_type.add(code_frontend_assignt( + result_symbol.symbol_expr(), + typecast_exprt(init_expr_for_parameter, p.type()))); cases.push_back(init_code_for_type); } @@ -672,7 +671,7 @@ bool generate_java_start_function( symbol_table.add(exc_symbol); // Zero-initialise the top-level exception catch variable: - init_code.add(code_assignt( + init_code.add(code_frontend_assignt( exc_symbol.symbol_expr(), null_pointer_exprt(to_pointer_type(exc_symbol.type)))); diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index beb8baa6212..029bb708acb 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -399,7 +399,7 @@ void initialize_nondet_string_fields( allocate_objects.allocate_automatic_local_object( java_int_type(), "tmp_object_factory"); const side_effect_expr_nondett nondet_length(length_expr.type(), loc); - code.add(code_assignt(length_expr, nondet_length)); + code.add(code_frontend_assignt(length_expr, nondet_length)); // assume (length_expr >= min_nondet_string_length); const exprt min_length = @@ -508,8 +508,8 @@ void java_object_factoryt::gen_nondet_pointer_init( // Having created a pointer to object of type replacement_pointer_type // we now assign it back to the original pointer with a cast // from pointer_type to replacement_pointer_type - assignments.add( - code_assignt(expr, typecast_exprt(real_pointer_symbol, pointer_type))); + assignments.add(code_frontend_assignt( + expr, typecast_exprt(real_pointer_symbol, pointer_type))); return; } @@ -539,8 +539,8 @@ void java_object_factoryt::gen_nondet_pointer_init( { if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE) { - assignments.add( - code_assignt{expr, null_pointer_exprt{pointer_type}, location}); + assignments.add(code_frontend_assignt{ + expr, null_pointer_exprt{pointer_type}, location}); } // Otherwise leave it as it is. return; @@ -615,7 +615,7 @@ void java_object_factoryt::gen_nondet_pointer_init( update_in_placet::NO_UPDATE_IN_PLACE, location); - const code_assignt set_null_inst{ + const code_frontend_assignt set_null_inst{ expr, null_pointer_exprt{pointer_type}, location}; const bool allow_null = depth > object_factory_parameters.min_null_tree_depth; @@ -734,7 +734,7 @@ alternate_casest get_string_input_values_code( { const symbol_exprt s = get_or_create_string_literal_symbol(val, symbol_table, true); - cases.push_back(code_assignt(expr, s)); + cases.push_back(code_frontend_assignt(expr, s)); } return cases; } @@ -843,7 +843,7 @@ void java_object_factoryt::gen_nondet_struct_init( allocate_objects); } - assignments.add(code_assignt(expr, *initial_object)); + assignments.add(code_frontend_assignt(expr, *initial_object)); } for(const auto &component : components) @@ -865,7 +865,7 @@ void java_object_factoryt::gen_nondet_struct_init( // which is necessary to support concurrency. if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE) continue; - code_assignt code(me, from_integer(0, me.type())); + code_frontend_assignt code(me, from_integer(0, me.type())); code.add_source_location() = location; assignments.add(code); } @@ -950,7 +950,7 @@ static code_blockt assume_expr_integral( allocate_local_symbol(java_int_type(), "assume_integral_tmp"); assignments.add(code_declt(aux_int), location); exprt nondet_rhs = side_effect_expr_nondett(java_int_type(), location); - code_assignt aux_assign(aux_int, nondet_rhs); + code_frontend_assignt aux_assign(aux_int, nondet_rhs); aux_assign.add_source_location() = location; assignments.add(aux_assign); assignments.add( @@ -1068,7 +1068,7 @@ void java_object_factoryt::gen_nondet_init( exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, location) : side_effect_expr_nondett(type, location); - code_assignt assign(expr, rhs); + code_frontend_assignt assign(expr, rhs); assign.add_source_location() = location; assignments.add(assign); @@ -1084,7 +1084,7 @@ void java_object_factoryt::gen_nondet_init( if(auto singleton = interval.as_singleton()) { assignments.add( - code_assignt{expr, from_integer(*singleton, expr.type())}); + code_frontend_assignt{expr, from_integer(*singleton, expr.type())}); } else { @@ -1158,7 +1158,7 @@ static void allocate_nondet_length_array( java_new_array.copy_to_operands(length_sym_expr); java_new_array.set(ID_length_upper_bound, max_length_expr); java_new_array.type().subtype().set(ID_element_type, element_type); - code_assignt assign(lhs, java_new_array); + code_frontend_assignt assign(lhs, java_new_array); assign.add_source_location() = location; assignments.add(assign); } @@ -1204,13 +1204,15 @@ static void array_primitive_init_code( // *array_data_init = NONDET(TYPE [max_length_expr]); side_effect_expr_nondett nondet_data(array_type, location); const dereference_exprt data_pointer_deref{tmp_finite_array_pointer}; - assignments.add(code_assignt(data_pointer_deref, std::move(nondet_data))); + assignments.add( + code_frontend_assignt(data_pointer_deref, std::move(nondet_data))); assignments.statements().back().add_source_location() = location; // init_array_expr = *array_data_init; address_of_exprt tmp_nondet_pointer( index_exprt(data_pointer_deref, from_integer(0, java_int_type()))); - assignments.add(code_assignt(init_array_expr, std::move(tmp_nondet_pointer))); + assignments.add( + code_frontend_assignt(init_array_expr, std::move(tmp_nondet_pointer))); assignments.statements().back().add_source_location() = location; } @@ -1251,7 +1253,7 @@ code_blockt java_object_factoryt::assign_element( // If we're updating an existing array item, read the existing object that // we (may) alter: if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE) - assignments.add(code_assignt(init_expr, element)); + assignments.add(code_frontend_assignt(init_expr, element)); } // MUST_UPDATE_IN_PLACE only applies to this object. @@ -1277,7 +1279,7 @@ code_blockt java_object_factoryt::assign_element( { // We used a temporary variable to update or initialise an array item; // now write it into the array: - assignments.add(code_assignt(element, init_expr)); + assignments.add(code_frontend_assignt(element, init_expr)); } return assignments; } @@ -1337,7 +1339,7 @@ static void array_loop_init_code( const symbol_exprt &array_init_symexpr = allocate_local_symbol(init_array_expr.type(), "array_data_init"); - code_assignt data_assign(array_init_symexpr, init_array_expr); + code_frontend_assignt data_assign(array_init_symexpr, init_array_expr); data_assign.add_source_location() = location; assignments.add(data_assign); @@ -1505,7 +1507,8 @@ bool java_object_factoryt::gen_nondet_enum_init( const dereference_exprt element_at_index = array_element_from_pointer(enum_array_expr, index_expr); - code_assignt enum_assign(expr, typecast_exprt(element_at_index, expr.type())); + code_frontend_assignt enum_assign( + expr, typecast_exprt(element_at_index, expr.type())); assignments.add(enum_assign); return true; @@ -1520,7 +1523,7 @@ static void assert_type_consistency(const code_blockt &assignments) { if(code.get_statement() != ID_assign) continue; - const auto &assignment = to_code_assign(code); + const auto &assignment = to_code_frontend_assign(code); INVARIANT( assignment.lhs().type() == assignment.rhs().type(), "object factory should produce type-consistent assignments"); diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 41ee14b8951..2bb7d17b206 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -179,20 +179,20 @@ static irep_idt clinit_local_init_complete_var_name(const irep_idt &class_name) return id2string(class_name) + CPROVER_PREFIX "clinit_wrapper::init_complete"; } -/// Generates a code_assignt for clinit_statest +/// Generates a code_frontend_assignt for clinit_statest /// /param expr: /// expression to be used as the LHS of generated assignment. /// /param state: /// execution state of the clint_wrapper, used as the RHS of the generated /// assignment. -/// /return returns a code_assignt, assigning \p expr to the integer +/// /return returns a code_frontend_assignt, assigning \p expr to the integer /// representation of \p state -static code_assignt +static code_frontend_assignt gen_clinit_assign(const exprt &expr, const clinit_statest state) { mp_integer initv(static_cast(state)); constant_exprt init_s = from_integer(initv, clinit_states_type()); - return code_assignt(expr, init_s); + return code_frontend_assignt(expr, init_s); } /// Generates an equal_exprt for clinit_statest @@ -596,7 +596,7 @@ code_blockt get_thread_safe_clinit_wrapper_body( // C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE; { - code_assignt assign = gen_clinit_assign( + code_frontend_assignt assign = gen_clinit_assign( clinit_thread_local_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE); function_body.add(assign); @@ -629,7 +629,8 @@ code_blockt get_thread_safe_clinit_wrapper_body( code_ifthenelset init_conditional( gen_clinit_eqexpr( clinit_state_sym.symbol_expr(), clinit_statest::INIT_COMPLETE), - code_blockt({code_assignt(init_complete.symbol_expr(), true_exprt())})); + code_blockt( + {code_frontend_assignt(init_complete.symbol_expr(), true_exprt())})); code_ifthenelset not_init_conditional( gen_clinit_eqexpr( @@ -637,7 +638,7 @@ code_blockt get_thread_safe_clinit_wrapper_body( code_blockt( {gen_clinit_assign( clinit_state_sym.symbol_expr(), clinit_statest::IN_PROGRESS), - code_assignt(init_complete.symbol_expr(), false_exprt())}), + code_frontend_assignt(init_complete.symbol_expr(), false_exprt())}), std::move(init_conditional)); function_body.add(std::move(not_init_conditional)); @@ -757,7 +758,8 @@ code_ifthenelset get_clinit_wrapper_body( false_exprt()); // add the "already-run = false" statement - code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt()); + code_frontend_assignt set_already_run( + already_run_symbol.symbol_expr(), true_exprt()); code_blockt init_body({set_already_run}); clinit_wrapper_do_recursive_calls( diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index a15eb922f67..48deaec0944 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -531,7 +531,7 @@ codet invokedynamic_synthetic_constructor( if(parameter.get_this()) continue; - code_assignt assign_field( + code_frontend_assignt assign_field( member_exprt(deref_this, field_iterator->get_name(), parameter.type()), symbol_exprt(parameter.get_identifier(), parameter.type())); result.add(assign_field); @@ -605,7 +605,7 @@ static symbol_exprt instantiate_new_object( // Instantiate the object: side_effect_exprt java_new_expr(ID_java_new, created_type, {}); - result.add(code_assignt{new_instance_var, java_new_expr}); + result.add(code_frontend_assignt{new_instance_var, java_new_expr}); return new_instance_var; } diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 78bee7d9e35..0f7b7e360c7 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -411,7 +411,7 @@ bool generate_ansi_c_start_function( // disable bounds check on that one index_expr.set(ID_C_bounds_check, false); - init_code.add(code_assignt(index_expr, null)); + init_code.add(code_frontend_assignt(index_expr, null)); } if(parameters.size()==3) diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 4adcb948b4c..ad3cc091755 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -57,8 +57,8 @@ void symbol_factoryt::gen_nondet_init( // Handle the pointer-to-code case separately: // leave as nondet_ptr to allow `remove_function_pointers` // to replace the pointer. - assignments.add( - code_assignt{expr, side_effect_expr_nondett{pointer_type, loc}}); + assignments.add(code_frontend_assignt{ + expr, side_effect_expr_nondett{pointer_type, loc}}); return; } @@ -71,7 +71,7 @@ void symbol_factoryt::gen_nondet_init( depth >= object_factory_params.max_nondet_tree_depth) { assignments.add( - code_assignt{expr, null_pointer_exprt{pointer_type}, loc}); + code_frontend_assignt{expr, null_pointer_exprt{pointer_type}, loc}); return; } @@ -104,7 +104,7 @@ void symbol_factoryt::gen_nondet_init( // > // And the next line is labelled label2 - const code_assignt set_null_inst{ + const code_frontend_assignt set_null_inst{ expr, null_pointer_exprt{pointer_type}, loc}; code_ifthenelset null_check( @@ -154,7 +154,7 @@ void symbol_factoryt::gen_nondet_init( // = NONDET(type); exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc) : side_effect_expr_nondett(type, loc); - code_assignt assign(expr, rhs); + code_frontend_assignt assign(expr, rhs); assign.add_source_location()=loc; assignments.add(std::move(assign)); diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp index 386943e029c..26acdf68a4e 100644 --- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp +++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp @@ -647,7 +647,7 @@ static void instantiate_atomic_fetch_op( // build *ptr const dereference_exprt deref_ptr{parameter_exprs[0]}; - block.add(code_assignt{result, deref_ptr}); + block.add(code_frontend_assignt{result, deref_ptr}); // build *ptr = result OP arguments[1]; irep_idt op_id = identifier == ID___atomic_fetch_add @@ -664,7 +664,7 @@ static void instantiate_atomic_fetch_op( ? ID_bitnand : ID_nil; binary_exprt op_expr{result, op_id, parameter_exprs[1], type}; - block.add(code_assignt{deref_ptr, std::move(op_expr)}); + block.add(code_frontend_assignt{deref_ptr, std::move(op_expr)}); block.add(code_expressiont{side_effect_expr_function_callt{ symbol_exprt::typeless("__atomic_thread_fence"), @@ -724,9 +724,9 @@ static void instantiate_atomic_op_fetch( ? ID_bitnand : ID_nil; binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type}; - block.add(code_assignt{result, std::move(op_expr)}); + block.add(code_frontend_assignt{result, std::move(op_expr)}); - block.add(code_assignt{deref_ptr, result}); + block.add(code_frontend_assignt{deref_ptr, result}); // this instruction implies an mfence, i.e., WRfence block.add(code_expressiont{side_effect_expr_function_callt{ @@ -822,9 +822,9 @@ static void instantiate_sync_val_compare_and_swap( // build *ptr const dereference_exprt deref_ptr{parameter_exprs[0]}; - block.add(code_assignt{result, deref_ptr}); + block.add(code_frontend_assignt{result, deref_ptr}); - code_assignt assign{deref_ptr, parameter_exprs[2]}; + code_frontend_assignt assign{deref_ptr, parameter_exprs[2]}; assign.add_source_location() = source_location; block.add(code_ifthenelset{equal_exprt{result, parameter_exprs[1]}, std::move(assign)}); @@ -880,9 +880,9 @@ static void instantiate_sync_lock_test_and_set( // build *ptr const dereference_exprt deref_ptr{parameter_exprs[0]}; - block.add(code_assignt{result, deref_ptr}); + block.add(code_frontend_assignt{result, deref_ptr}); - block.add(code_assignt{deref_ptr, parameter_exprs[1]}); + block.add(code_frontend_assignt{deref_ptr, parameter_exprs[1]}); // This built-in function is not a full barrier, but rather an acquire // barrier. @@ -922,9 +922,9 @@ static void instantiate_sync_lock_release( code_typet{{}, void_type()}, source_location}}); - block.add(code_assignt{dereference_exprt{parameter_exprs[0]}, - typecast_exprt::conditional_cast( - from_integer(0, signed_int_type()), type)}); + block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[0]}, + typecast_exprt::conditional_cast( + from_integer(0, signed_int_type()), type)}); // This built-in function is not a full barrier, but rather a release // barrier. @@ -958,8 +958,8 @@ static void instantiate_atomic_load( code_typet{{}, void_type()}, source_location}}); - block.add(code_assignt{dereference_exprt{parameter_exprs[1]}, - dereference_exprt{parameter_exprs[0]}}); + block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[1]}, + dereference_exprt{parameter_exprs[0]}}); block.add(code_expressiont{side_effect_expr_function_callt{ symbol_exprt::typeless("__atomic_thread_fence"), @@ -1018,8 +1018,8 @@ static void instantiate_atomic_store( code_typet{{}, void_type()}, source_location}}); - block.add(code_assignt{dereference_exprt{parameter_exprs[0]}, - dereference_exprt{parameter_exprs[1]}}); + block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[0]}, + dereference_exprt{parameter_exprs[1]}}); block.add(code_expressiont{side_effect_expr_function_callt{ symbol_exprt::typeless("__atomic_thread_fence"), @@ -1071,10 +1071,10 @@ static void instantiate_atomic_exchange( code_typet{{}, void_type()}, source_location}}); - block.add(code_assignt{dereference_exprt{parameter_exprs[2]}, - dereference_exprt{parameter_exprs[0]}}); - block.add(code_assignt{dereference_exprt{parameter_exprs[0]}, - dereference_exprt{parameter_exprs[1]}}); + block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[2]}, + dereference_exprt{parameter_exprs[0]}}); + block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[0]}, + dereference_exprt{parameter_exprs[1]}}); block.add(code_expressiont{side_effect_expr_function_callt{ symbol_exprt::typeless("__atomic_thread_fence"), @@ -1154,14 +1154,15 @@ static void instantiate_atomic_compare_exchange( // build *ptr const dereference_exprt deref_ptr{parameter_exprs[0]}; - block.add(code_assignt{ + block.add(code_frontend_assignt{ result, typecast_exprt::conditional_cast( equal_exprt{deref_ptr, dereference_exprt{parameter_exprs[1]}}, result.type())}); // we never fail spuriously, and ignore parameter_exprs[3] - code_assignt assign{deref_ptr, dereference_exprt{parameter_exprs[2]}}; + code_frontend_assignt assign{deref_ptr, + dereference_exprt{parameter_exprs[2]}}; assign.add_source_location() = source_location; code_expressiont success_fence{side_effect_expr_function_callt{ symbol_exprt::typeless("__atomic_thread_fence"), @@ -1170,8 +1171,8 @@ static void instantiate_atomic_compare_exchange( source_location}}; success_fence.add_source_location() = source_location; - code_assignt assign_not_equal{dereference_exprt{parameter_exprs[1]}, - deref_ptr}; + code_frontend_assignt assign_not_equal{dereference_exprt{parameter_exprs[1]}, + deref_ptr}; assign_not_equal.add_source_location() = source_location; code_expressiont failure_fence{side_effect_expr_function_callt{ symbol_exprt::typeless("__atomic_thread_fence"), diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index aa44d7dbbfa..92eee6ba345 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -637,7 +637,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) code_declt declaration(symbol_expr); declaration.add_source_location() = size_source_location; - code_assignt assignment; + code_frontend_assignt assignment; assignment.lhs()=symbol_expr; assignment.rhs() = new_symbol.value; assignment.add_source_location() = size_source_location; diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 91ba5aa039e..811de978e5c 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3022,7 +3022,7 @@ std::string expr2ct::convert_code( return convert_code_dead(src, indent); if(statement==ID_assign) - return convert_code_assign(to_code_assign(src), indent); + return convert_code_frontend_assign(to_code_frontend_assign(src), indent); if(statement=="lock") return convert_code_lock(src, indent); @@ -3062,8 +3062,8 @@ std::string expr2ct::convert_code( return convert_norep(src, precedence); } -std::string expr2ct::convert_code_assign( - const code_assignt &src, +std::string expr2ct::convert_code_frontend_assign( + const code_frontend_assignt &src, unsigned indent) { return indent_str(indent) + diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 513f8969bfa..fa382335800 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -199,7 +199,8 @@ class expr2ct // NOLINTNEXTLINE(whitespace/line_length) std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent); std::string convert_code_asm(const code_asmt &src, unsigned indent); - std::string convert_code_assign(const code_assignt &src, unsigned indent); + std::string + convert_code_frontend_assign(const code_frontend_assignt &, unsigned indent); // NOLINTNEXTLINE(whitespace/line_length) std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent); std::string convert_code_for(const code_fort &src, unsigned indent); diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index 10d761075fe..de445ac2754 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -42,7 +42,7 @@ static void copy_parent( op1.get_sub().push_back(cpp_namet(arg_name, source_location)); op1.add_source_location()=source_location; - code_assignt code(dereference_exprt(op0), op1); + code_frontend_assignt code(dereference_exprt(op0), op1); code.add_source_location() = source_location; block.operands().push_back(code); @@ -239,7 +239,7 @@ void cpp_typecheckt::default_cpctor( ptrmember.set(ID_component_name, mem_c.get_name()); ptrmember.operands().push_back(exprt("cpp-this")); - code_assignt assign(ptrmember, address); + code_frontend_assignt assign(ptrmember, address); initializers.move_to_sub(assign); continue; } @@ -691,7 +691,7 @@ void cpp_typecheckt::full_member_initialization( ptrmember.set(ID_component_name, c.get_name()); ptrmember.operands().push_back(exprt("cpp-this")); - code_assignt assign(ptrmember, address); + code_frontend_assignt assign(ptrmember, address); final_initializers.move_to_sub(assign); continue; } diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index 8135dd5f585..824d0f3e604 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -88,7 +88,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol, const symbol_exprt &this_expr) ptrmember.set(ID_component_name, c.get_name()); ptrmember.operands().push_back(this_expr); - code_assignt assign(ptrmember, address); + code_frontend_assignt assign(ptrmember, address); block.add(assign); continue; } diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 4d37932b849..8e6c7a995f4 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -303,7 +303,7 @@ void cpp_typecheckt::zero_initializer( typecast_exprt::conditional_cast(from_integer(0, enum_type), type); already_typechecked_exprt::make_already_typechecked(zero); - code_assignt assign; + code_frontend_assignt assign; assign.lhs()=object; assign.rhs()=zero; assign.add_source_location()=source_location; @@ -326,7 +326,7 @@ void cpp_typecheckt::zero_initializer( throw 0; } - code_assignt assign(object, *value); + code_frontend_assignt assign(object, *value); assign.add_source_location()=source_location; typecheck_expr(assign.lhs()); diff --git a/src/util/allocate_objects.cpp b/src/util/allocate_objects.cpp index cd238e1ae86..1c73b829edc 100644 --- a/src/util/allocate_objects.cpp +++ b/src/util/allocate_objects.cpp @@ -129,9 +129,10 @@ exprt allocate_objectst::allocate_dynamic_object_symbol( if(allocate_type.id() == ID_empty) { // make null - code_assignt code{target_expr, - null_pointer_exprt{to_pointer_type(target_expr.type())}, - source_location}; + code_frontend_assignt code{ + target_expr, + null_pointer_exprt{to_pointer_type(target_expr.type())}, + source_location}; output_code.add(std::move(code)); return exprt(); @@ -154,14 +155,14 @@ exprt allocate_objectst::allocate_dynamic_object_symbol( symbols_created.push_back(&malloc_sym); - code_assignt assign = + code_frontend_assignt assign = make_allocate_code(malloc_sym.symbol_expr(), object_size.value()); output_code.add(assign); exprt malloc_symbol_expr = typecast_exprt::conditional_cast( malloc_sym.symbol_expr(), target_expr.type()); - code_assignt code(target_expr, malloc_symbol_expr); + code_frontend_assignt code(target_expr, malloc_symbol_expr); code.add_source_location() = source_location; output_code.add(code); @@ -198,7 +199,7 @@ exprt allocate_objectst::allocate_non_dynamic_object( exprt aoe = typecast_exprt::conditional_cast( address_of_exprt(aux_symbol.symbol_expr()), target_expr.type()); - code_assignt code(target_expr, aoe); + code_frontend_assignt code(target_expr, aoe); code.add_source_location() = source_location; assignments.add(code); @@ -252,9 +253,10 @@ void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code) } } -code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size) +code_frontend_assignt +make_allocate_code(const symbol_exprt &lhs, const exprt &size) { side_effect_exprt alloc{ ID_allocate, {size, false_exprt()}, lhs.type(), lhs.source_location()}; - return code_assignt(lhs, alloc); + return code_frontend_assignt(lhs, alloc); } diff --git a/src/util/allocate_objects.h b/src/util/allocate_objects.h index 09a0a737596..1de4e917a16 100644 --- a/src/util/allocate_objects.h +++ b/src/util/allocate_objects.h @@ -119,6 +119,7 @@ class allocate_objectst /// \param lhs: pointer which will be allocated /// \param size: size of the object /// \return code allocating the object and assigning it to `lhs` -code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size); +code_frontend_assignt +make_allocate_code(const symbol_exprt &lhs, const exprt &size); #endif // CPROVER_UTIL_ALLOCATE_OBJECTS_H diff --git a/src/util/nondet.cpp b/src/util/nondet.cpp index 3c3b43ba245..3634580c838 100644 --- a/src/util/nondet.cpp +++ b/src/util/nondet.cpp @@ -52,7 +52,7 @@ symbol_exprt generate_nondet_int( // Assign the symbol any non deterministic integer value. // int_type name_prefix::nondet_int = NONDET(int_type) - instructions.add(code_assignt( + instructions.add(code_frontend_assignt( nondet_symbol, side_effect_expr_nondett(int_type, source_location))); // Constrain the non deterministic integer with a lower bound of `min_value`. diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp index 4246ee996f0..3efece6cf68 100644 --- a/src/util/std_code.cpp +++ b/src/util/std_code.cpp @@ -227,7 +227,7 @@ code_fort code_fort::from_index_bounds( location); return code_fort{ - code_assignt{loop_index, std::move(start_index)}, + code_frontend_assignt{loop_index, std::move(start_index)}, binary_relation_exprt{loop_index, ID_lt, std::move(end_index)}, std::move(inc), std::move(body)}; diff --git a/src/util/std_code.h b/src/util/std_code.h index 04aaa27d53d..59a77796a75 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -34,7 +34,7 @@ class codet:public exprt public: /// \param statement: Specifies the type of the `codet` to be constructed, /// e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a - /// \ref code_assignt. + /// \ref code_frontend_assignt. explicit codet(const irep_idt &statement) : exprt(ID_code, empty_typet()) { set_statement(statement); @@ -48,7 +48,7 @@ class codet:public exprt /// \param statement: Specifies the type of the `codet` to be constructed, /// e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a - /// \ref code_assignt. + /// \ref code_frontend_assignt. /// \param _op: any operands to be added explicit codet(const irep_idt &statement, operandst _op) : codet(statement) { @@ -162,6 +162,115 @@ inline codet &to_code(exprt &expr) return static_cast(expr); } +/// A \ref codet representing an assignment in the program. +/// For example, if an expression `e1` is represented as an \ref exprt `expr1` +/// and an expression `e2` is represented as an \ref exprt `expr2`, the +/// (nonstandard) assignment statement `e1 = e2;` can be represented +/// as `code_frontend_assignt(expr1, expr2)`. +class code_frontend_assignt : public codet +{ +public: + code_frontend_assignt() : codet(ID_assign) + { + operands().resize(2); + } + + code_frontend_assignt(exprt lhs, exprt rhs) + : codet(ID_assign, {std::move(lhs), std::move(rhs)}) + { + } + + code_frontend_assignt(exprt lhs, exprt rhs, source_locationt loc) + : codet(ID_assign, {std::move(lhs), std::move(rhs)}, std::move(loc)) + { + } + + exprt &lhs() + { + return op0(); + } + + exprt &rhs() + { + return op1(); + } + + const exprt &lhs() const + { + return op0(); + } + + const exprt &rhs() const + { + return op1(); + } + + static void check( + const codet &code, + const validation_modet vm = validation_modet::INVARIANT) + { + DATA_CHECK( + vm, code.operands().size() == 2, "assignment must have two operands"); + } + + static void validate( + const codet &code, + const namespacet &, + const validation_modet vm = validation_modet::INVARIANT) + { + check(code, vm); + + DATA_CHECK( + vm, + code.op0().type() == code.op1().type(), + "lhs and rhs of assignment must have same type"); + } + + static void validate_full( + const codet &code, + const namespacet &ns, + const validation_modet vm = validation_modet::INVARIANT) + { + for(const exprt &op : code.operands()) + { + validate_full_expr(op, ns, vm); + } + + validate(code, ns, vm); + } + +protected: + using codet::op0; + using codet::op1; + using codet::op2; + using codet::op3; +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return detail::can_cast_code_impl(base, ID_assign); +} + +inline void validate_expr(const code_frontend_assignt &x) +{ + code_frontend_assignt::check(x); +} + +inline const code_frontend_assignt &to_code_frontend_assign(const codet &code) +{ + PRECONDITION(code.get_statement() == ID_assign); + code_frontend_assignt::check(code); + return static_cast(code); +} + +inline code_frontend_assignt &to_code_frontend_assign(codet &code) +{ + PRECONDITION(code.get_statement() == ID_assign); + code_frontend_assignt::check(code); + return static_cast(code); +} + /// A \ref codet representing sequential composition of program statements. /// Each operand represents a statement in the block. class code_blockt:public codet