From c830360de8fc2b6ba26d0f775512a82b280f5904 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 24 Feb 2021 11:10:38 +0000 Subject: [PATCH] introduce instructiont::decl_symbol() This addresses the issue of the ambiguous dual-use of code_declt in both the C front-end and the goto-program API by replacing the use of code_declt by directly returning the symbol_exprt. The client code is simplified. --- jbmc/src/java_bytecode/remove_exceptions.cpp | 3 +-- src/analyses/constant_propagator.cpp | 3 +-- src/analyses/custom_bitvector_analysis.cpp | 8 +++--- src/analyses/escape_analysis.cpp | 7 ++---- src/analyses/global_may_alias.cpp | 5 +--- src/analyses/goto_rw.cpp | 8 ++---- src/analyses/interval_domain.cpp | 2 +- src/analyses/local_bitvector_analysis.cpp | 5 +--- src/analyses/local_may_alias.cpp | 6 ++--- src/analyses/locals.cpp | 2 +- src/analyses/uninitialized_domain.cpp | 2 +- .../variable_sensitivity_domain.cpp | 5 ++-- src/goto-diff/change_impact.cpp | 2 +- src/goto-instrument/code_contracts.cpp | 2 +- src/goto-instrument/full_slicer.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 2 +- src/goto-instrument/uninitialized.cpp | 3 +-- src/goto-programs/goto_program.cpp | 17 +++++-------- src/goto-programs/goto_program.h | 25 +++++++++++++++++++ src/goto-programs/string_abstraction.cpp | 2 +- src/goto-symex/symex_decl.cpp | 9 +------ 21 files changed, 57 insertions(+), 63 deletions(-) diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 7a31fea2a6d..4734fbc86a6 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -512,8 +512,7 @@ void remove_exceptionst::instrument_exceptions( { if(instr_it->is_decl()) { - code_declt decl = instr_it->get_decl(); - locals.push_back(decl.symbol()); + locals.push_back(instr_it->decl_symbol()); } // Is it a handler push/pop or catch landing-pad? else if(instr_it->type==CATCH) diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index b040ca51b8d..3ef70106160 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -158,8 +158,7 @@ void constant_propagator_domaint::transform( if(from->is_decl()) { - const auto &code_decl = from->get_decl(); - const symbol_exprt &symbol = code_decl.symbol(); + const symbol_exprt &symbol = from->decl_symbol(); values.set_to_top(symbol); } else if(from->is_assign()) diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index 833c001d1d7..99e0763c10f 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -294,12 +294,12 @@ void custom_bitvector_domaint::transform( case DECL: { - const code_declt &code_decl=to_code_decl(instruction.code); - assign_lhs(code_decl.symbol(), vectorst()); + const auto &decl_symbol = instruction.decl_symbol(); + assign_lhs(decl_symbol, vectorst()); // is it a pointer? - if(code_decl.symbol().type().id()==ID_pointer) - assign_lhs(dereference_exprt(code_decl.symbol()), vectorst()); + if(decl_symbol.type().id() == ID_pointer) + assign_lhs(dereference_exprt(decl_symbol), vectorst()); } break; diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 81f5b89621b..d6e49eb444d 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -202,11 +202,8 @@ void escape_domaint::transform( break; case DECL: - { - const code_declt &code_decl=to_code_decl(instruction.code); - aliases.isolate(code_decl.get_identifier()); - assign_lhs_cleanup(code_decl.symbol(), std::set()); - } + aliases.isolate(instruction.decl_symbol().get_identifier()); + assign_lhs_cleanup(instruction.decl_symbol(), std::set()); break; case DEAD: diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 72ae9fe7760..908f7bd26ff 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -120,11 +120,8 @@ void global_may_alias_domaint::transform( } case DECL: - { - const code_declt &code_decl = to_code_decl(instruction.code); - aliases.isolate(code_decl.get_identifier()); + aliases.isolate(instruction.decl_symbol().get_identifier()); break; - } case DEAD: { diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 056564e221e..a6732a9d6bf 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -822,13 +822,9 @@ void goto_rw( break; case DECL: + rw_set.get_objects_rec(function, target, target->decl_symbol().type()); rw_set.get_objects_rec( - function, target, to_code_decl(target->code).symbol().type()); - rw_set.get_objects_rec( - function, - target, - rw_range_sett::get_modet::LHS_W, - to_code_decl(target->code).symbol()); + function, target, rw_range_sett::get_modet::LHS_W, target->decl_symbol()); break; case FUNCTION_CALL: diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 96514e4355b..3bbb0491dfb 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -71,7 +71,7 @@ void interval_domaint::transform( switch(instruction.type) { case DECL: - havoc_rec(to_code_decl(instruction.code).symbol()); + havoc_rec(instruction.decl_symbol()); break; case DEAD: diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 17f635e54ec..e482c8068c2 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -282,15 +282,12 @@ void local_bitvector_analysist::build() } case DECL: - { - const code_declt &code_decl = to_code_decl(instruction.code); assign_lhs( - code_decl.symbol(), + instruction.decl_symbol(), exprt(ID_uninitialized), loc_info_src, loc_info_dest); break; - } case DEAD: { diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index 5198b1cbb15..ccf23000fbc 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -383,11 +383,9 @@ void local_may_aliast::build(const goto_functiont &goto_function) } case DECL: - { - const code_declt &code_decl = to_code_decl(instruction.code); - assign_lhs(code_decl.symbol(), nil_exprt(), loc_info_src, loc_info_dest); + assign_lhs( + instruction.decl_symbol(), nil_exprt(), loc_info_src, loc_info_dest); break; - } case DEAD: { diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp index 5704df2d77b..7c3a2cae363 100644 --- a/src/analyses/locals.cpp +++ b/src/analyses/locals.cpp @@ -20,7 +20,7 @@ void localst::build(const goto_functiont &goto_function) for(const auto &instruction : goto_function.body.instructions) { if(instruction.is_decl()) - locals.insert(instruction.get_decl().get_identifier()); + locals.insert(instruction.decl_symbol().get_identifier()); } locals.insert( diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index 2ed9b4d0561..c4e5a0e24c0 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -33,7 +33,7 @@ void uninitialized_domaint::transform( if(from->is_decl()) { - const irep_idt &identifier = to_code_decl(from->code).get_identifier(); + const irep_idt &identifier = from->decl_symbol().get_identifier(); const symbolt &symbol = ns.lookup(identifier); if(!symbol.is_static_lifetime) diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index 768b2d47083..d6feb97b106 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -46,10 +46,9 @@ void variable_sensitivity_domaint::transform( abstract_object_pointert top_object = abstract_state .abstract_object_factory( - to_code_decl(instruction.code).symbol().type(), ns, true, false) + instruction.decl_symbol().type(), ns, true, false) ->update_location_context(write_location, true); - abstract_state.assign( - to_code_decl(instruction.code).symbol(), top_object, ns); + abstract_state.assign(instruction.decl_symbol(), top_object, ns); } // We now store top. break; diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp index eaabbd0a356..4210c115356 100644 --- a/src/goto-diff/change_impact.cpp +++ b/src/goto-diff/change_impact.cpp @@ -79,7 +79,7 @@ void full_slicert::operator()( jumps.push_back(instruction_node_index); else if(instruction->is_decl()) { - const auto &s=to_code_decl(instruction->code).symbol(); + const auto &s=instruction->decl_symbol(); decl_dead[s.get_identifier()].push(instruction_node_index); } else if(instruction->is_dead()) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 2095f0e1a3a..7b1fac1bcef 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -669,7 +669,7 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) { if(instruction_iterator->is_decl()) { - freely_assignable_exprs.insert(instruction_iterator->get_decl().symbol()); + freely_assignable_exprs.insert(instruction_iterator->decl_symbol()); } else if(instruction_iterator->is_assign()) { diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index bed5c47be44..5d83f191472 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -285,7 +285,7 @@ void full_slicert::operator()( jumps.push_back(instruction_node_index); else if(instruction->is_decl()) { - const auto &s = to_code_decl(instruction->code).symbol(); + const auto &s = instruction->decl_symbol(); decl_dead[s.get_identifier()].push(instruction_node_index); } else if(instruction->is_dead()) diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 379414c0bb3..bc1c0b95ed8 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -450,7 +450,7 @@ goto_programt::const_targett goto_program2codet::convert_decl( goto_programt::const_targett upper_bound, code_blockt &dest) { - code_declt d = target->get_decl(); + code_declt d = code_declt{target->decl_symbol()}; symbol_exprt &symbol = d.symbol(); goto_programt::const_targett next=target; diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index b091546ccb9..cd59eb105ff 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -109,8 +109,7 @@ void uninitializedt::add_assertions( // if we track it, add declaration and assignment // for tracking variable! - const irep_idt &identifier= - to_code_decl(instruction.code).get_identifier(); + const irep_idt &identifier = instruction.decl_symbol().get_identifier(); if(tracking.find(identifier)!=tracking.end()) { diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index c74bad5cd0b..15306f9ccc4 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -240,8 +240,7 @@ void goto_programt::get_decl_identifiers( DATA_INVARIANT( instruction.code.operands().size() == 1, "declaration statement expects one operand"); - const symbol_exprt &symbol_expr = to_symbol_expr(instruction.code.op0()); - decl_identifiers.insert(symbol_expr.get_identifier()); + decl_identifiers.insert(instruction.decl_symbol().get_identifier()); } } } @@ -871,9 +870,9 @@ void goto_programt::instructiont::validate( source_location); DATA_CHECK_WITH_DIAGNOSTICS( vm, - !ns.lookup(get_decl().get_identifier(), table_symbol), + !ns.lookup(decl_symbol().get_identifier(), table_symbol), "declared symbols should be known", - id2string(get_decl().get_identifier()), + id2string(decl_symbol().get_identifier()), source_location); break; case DEAD: @@ -954,13 +953,9 @@ void goto_programt::instructiont::transform( case DECL: { - auto new_symbol = f(get_decl().symbol()); + auto new_symbol = f(decl_symbol()); if(new_symbol.has_value()) - { - auto new_decl = get_decl(); - new_decl.symbol() = to_symbol_expr(*new_symbol); - set_decl(new_decl); - } + decl_symbol() = to_symbol_expr(*new_symbol); } break; @@ -1046,7 +1041,7 @@ void goto_programt::instructiont::apply( break; case DECL: - f(get_decl().symbol()); + f(decl_symbol()); break; case DEAD: diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index b461b7f0c6f..b06a30a0551 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -196,6 +197,7 @@ class goto_programt } /// Get the declaration for DECL + DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead")) const code_declt &get_decl() const { PRECONDITION(is_decl()); @@ -206,7 +208,30 @@ class goto_programt return decl; } + /// Get the declared symbol for DECL + const symbol_exprt &decl_symbol() const + { + PRECONDITION(is_decl()); + auto &decl = expr_checked_cast(code); + INVARIANT( + !decl.initial_value(), + "code_declt in goto program may not contain initialization."); + return decl.symbol(); + } + + /// Get the declared symbol for DECL + symbol_exprt &decl_symbol() + { + PRECONDITION(is_decl()); + auto &decl = expr_checked_cast(code); + INVARIANT( + !decl.initial_value(), + "code_declt in goto program may not contain initialization."); + return decl.symbol(); + } + /// Set the declaration for DECL + DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead")) void set_decl(code_declt c) { PRECONDITION(is_decl()); diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index a72c76160d6..a29c80f7bb8 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -251,7 +251,7 @@ void string_abstractiont::declare_define_locals(goto_programt &dest) // same name may exist several times due to inlining, make sure the first // declaration is used available_decls.insert( - std::make_pair(it->get_decl().get_identifier(), it)); + std::make_pair(it->decl_symbol().get_identifier(), it)); // declare (and, if necessary, define) locals for(const auto &l : locals) diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index 3f4197af873..9efe1de7ef3 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -16,14 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com void goto_symext::symex_decl(statet &state) { const goto_programt::instructiont &instruction=*state.source.pc; - - const auto &code = instruction.get_decl(); - - // two-operand decl not supported here - // we handle the decl with only one operand - PRECONDITION(code.operands().size() == 1); - - symex_decl(state, code.symbol()); + symex_decl(state, instruction.decl_symbol()); } void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)