From 5f907859dccf55a193d9128480d64852b20cfa92 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 9 Feb 2024 12:04:06 +0000 Subject: [PATCH 1/7] Add exprt::with_source_location with source_locationt parameter We already supported the fluent-style with_source_location for copying from another expression (since 917f9a0b3d4c). Now also support passing a source location directly. --- src/util/expr.h | 16 ++++++++++++++++ src/util/std_expr.h | 32 ++++++++++++++++++++++++++++++++ 2 files changed, 48 insertions(+) diff --git a/src/util/expr.h b/src/util/expr.h index 56e8611a7d3..08e1d57a7e0 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -97,6 +97,22 @@ class exprt:public irept const operandst &operands() const { return (const operandst &)get_sub(); } + /// Add the source location from \p location, if it is non-nil. + exprt &with_source_location(source_locationt location) & + { + if(location.is_not_nil()) + add_source_location() = std::move(location); + return *this; + } + + /// Add the source location from \p location, if it is non-nil. + exprt &&with_source_location(source_locationt location) && + { + if(location.is_not_nil()) + add_source_location() = std::move(location); + return std::move(*this); + } + /// Add the source location from \p other, if it has any. exprt &with_source_location(const exprt &other) & { diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 90b2877f1f4..431de0bfa00 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -161,6 +161,38 @@ class symbol_exprt : public nullary_exprt { return get(ID_identifier); } + + /// Add the source location from \p location, if it is non-nil. + symbol_exprt &with_source_location(source_locationt location) & + { + if(location.is_not_nil()) + add_source_location() = std::move(location); + return *this; + } + + /// Add the source location from \p location, if it is non-nil. + symbol_exprt &&with_source_location(source_locationt location) && + { + if(location.is_not_nil()) + add_source_location() = std::move(location); + return std::move(*this); + } + + /// Add the source location from \p other, if it has any. + symbol_exprt &with_source_location(const exprt &other) & + { + if(other.source_location().is_not_nil()) + add_source_location() = other.source_location(); + return *this; + } + + /// Add the source location from \p other, if it has any. + symbol_exprt &&with_source_location(const exprt &other) && + { + if(other.source_location().is_not_nil()) + add_source_location() = other.source_location(); + return std::move(*this); + } }; // NOLINTNEXTLINE(readability/namespace) From 5951105af4020bc387bf79d37e0142e0b7fdf6a3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 9 Feb 2024 12:07:50 +0000 Subject: [PATCH 2/7] Reduce the number of symbol_exprt without a source location Create or maintain source location information in symbol expressions. --- .../c_typecheck_gcc_polymorphic_builtins.cpp | 58 +++++++++++-------- src/assembler/remove_asm.cpp | 7 ++- .../value_set_dereference.cpp | 2 +- src/util/ssa_expr.cpp | 1 + src/util/symbol.cpp | 2 +- unit/path_strategies.cpp | 7 ++- 6 files changed, 48 insertions(+), 29 deletions(-) diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp index 162daad11d8..5632868d13a 100644 --- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp +++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp @@ -673,7 +673,8 @@ static void instantiate_atomic_fetch_op( 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"), + symbol_exprt::typeless("__atomic_thread_fence") + .with_source_location(source_location), {parameter_exprs[2]}, typet{}, source_location}}); @@ -736,7 +737,8 @@ static void instantiate_atomic_op_fetch( // this instruction implies an mfence, i.e., WRfence block.add(code_expressiont{side_effect_expr_function_callt{ - symbol_exprt::typeless("__atomic_thread_fence"), + symbol_exprt::typeless("__atomic_thread_fence") + .with_source_location(source_location), {parameter_exprs[2]}, typet{}, source_location}}); @@ -767,11 +769,11 @@ static void instantiate_sync_fetch( parameter_exprs[1], from_integer(std::memory_order_seq_cst, signed_int_type())}; - block.add(code_returnt{ - side_effect_expr_function_callt{symbol_exprt::typeless(atomic_name), - std::move(arguments), - typet{}, - source_location}}); + block.add(code_returnt{side_effect_expr_function_callt{ + symbol_exprt::typeless(atomic_name).with_source_location(source_location), + std::move(arguments), + typet{}, + source_location}}); } static void instantiate_sync_bool_compare_and_swap( @@ -790,7 +792,8 @@ static void instantiate_sync_bool_compare_and_swap( // _Bool __sync_bool_compare_and_swap(type *ptr, type old, type new, ...) block.add(code_returnt{side_effect_expr_function_callt{ - symbol_exprt::typeless(ID___atomic_compare_exchange), + symbol_exprt::typeless(ID___atomic_compare_exchange) + .with_source_location(source_location), {parameter_exprs[0], address_of_exprt{parameter_exprs[1]}, address_of_exprt{parameter_exprs[2]}, @@ -968,7 +971,8 @@ static void instantiate_atomic_load( dereference_exprt{parameter_exprs[0]}}); block.add(code_expressiont{side_effect_expr_function_callt{ - symbol_exprt::typeless("__atomic_thread_fence"), + symbol_exprt::typeless("__atomic_thread_fence") + .with_source_location(source_location), {parameter_exprs[2]}, typet{}, source_location}}); @@ -999,7 +1003,8 @@ static void instantiate_atomic_load_n( block.add(codet{ID_decl_block, {code_frontend_declt{result}}}); block.add(code_expressiont{side_effect_expr_function_callt{ - symbol_exprt::typeless(ID___atomic_load), + symbol_exprt::typeless(ID___atomic_load) + .with_source_location(source_location), {parameter_exprs[0], address_of_exprt{result}, parameter_exprs[1]}, typet{}, source_location}}); @@ -1028,7 +1033,8 @@ static void instantiate_atomic_store( dereference_exprt{parameter_exprs[1]}}); block.add(code_expressiont{side_effect_expr_function_callt{ - symbol_exprt::typeless("__atomic_thread_fence"), + symbol_exprt::typeless("__atomic_thread_fence") + .with_source_location(source_location), {parameter_exprs[2]}, typet{}, source_location}}); @@ -1051,13 +1057,14 @@ static void instantiate_atomic_store_n( // This built-in function implements an atomic store operation. It writes // val into *ptr. - block.add(code_expressiont{ - side_effect_expr_function_callt{symbol_exprt::typeless(ID___atomic_store), - {parameter_exprs[0], - address_of_exprt{parameter_exprs[1]}, - parameter_exprs[2]}, - typet{}, - source_location}}); + block.add(code_expressiont{side_effect_expr_function_callt{ + symbol_exprt::typeless(ID___atomic_store) + .with_source_location(source_location), + {parameter_exprs[0], + address_of_exprt{parameter_exprs[1]}, + parameter_exprs[2]}, + typet{}, + source_location}}); } static void instantiate_atomic_exchange( @@ -1083,7 +1090,8 @@ static void instantiate_atomic_exchange( dereference_exprt{parameter_exprs[1]}}); block.add(code_expressiont{side_effect_expr_function_callt{ - symbol_exprt::typeless("__atomic_thread_fence"), + symbol_exprt::typeless("__atomic_thread_fence") + .with_source_location(source_location), {parameter_exprs[3]}, typet{}, source_location}}); @@ -1114,7 +1122,8 @@ static void instantiate_atomic_exchange_n( block.add(codet{ID_decl_block, {code_frontend_declt{result}}}); block.add(code_expressiont{side_effect_expr_function_callt{ - symbol_exprt::typeless(ID___atomic_exchange), + symbol_exprt::typeless(ID___atomic_exchange) + .with_source_location(source_location), {parameter_exprs[0], address_of_exprt{parameter_exprs[1]}, address_of_exprt{result}, @@ -1171,7 +1180,8 @@ static void instantiate_atomic_compare_exchange( 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"), + symbol_exprt::typeless("__atomic_thread_fence") + .with_source_location(source_location), {parameter_exprs[4]}, typet{}, source_location}}; @@ -1181,7 +1191,8 @@ static void instantiate_atomic_compare_exchange( 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"), + symbol_exprt::typeless("__atomic_thread_fence") + .with_source_location(source_location), {parameter_exprs[5]}, typet{}, source_location}}; @@ -1212,7 +1223,8 @@ static void instantiate_atomic_compare_exchange_n( // desired, bool weak, int success_memorder, int failure_memorder) block.add(code_returnt{side_effect_expr_function_callt{ - symbol_exprt::typeless(ID___atomic_compare_exchange), + symbol_exprt::typeless(ID___atomic_compare_exchange) + .with_source_location(source_location), {parameter_exprs[0], parameter_exprs[1], address_of_exprt{parameter_exprs[2]}, diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp index e46b4b2ed15..43426ace345 100644 --- a/src/assembler/remove_asm.cpp +++ b/src/assembler/remove_asm.cpp @@ -133,7 +133,8 @@ void remove_asmt::gcc_asm_function_call( arguments.size(), code_typet::parametert{void_pointer}}, empty_typet()}; - symbol_exprt fkt(function_identifier, fkt_type); + auto fkt = symbol_exprt{function_identifier, fkt_type}.with_source_location( + code.source_location()); code_function_callt function_call(std::move(fkt), std::move(arguments)); @@ -189,8 +190,8 @@ void remove_asmt::msc_asm_function_call( arguments.size(), code_typet::parametert{void_pointer}}, empty_typet()}; - symbol_exprt fkt(function_identifier, fkt_type); - + auto fkt = symbol_exprt{function_identifier, fkt_type}.with_source_location( + code.source_location()); code_function_callt function_call(std::move(fkt), std::move(arguments)); dest.add( diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index f36cc67b453..0ae667630a4 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -236,7 +236,7 @@ exprt value_set_dereferencet::handle_dereference_base_case( pointer.type(), "derefd_pointer", "derefd_pointer", - source_locationt(), + pointer.find_source_location(), language_mode, new_symbol_table); diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index 5df2031434e..e92c79967e6 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -41,6 +41,7 @@ ssa_exprt::ssa_exprt(const exprt &expr) : symbol_exprt(expr.type()) { set(ID_C_SSA_symbol, true); add(ID_expression, expr); + with_source_location(expr.source_location()); std::ostringstream os; initialize_ssa_identifier(os, expr); const std::string id = os.str(); diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 12f60c5f01a..5335125c9c5 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -120,7 +120,7 @@ void symbolt::swap(symbolt &b) /// type of the symbol object. symbol_exprt symbolt::symbol_expr() const { - return symbol_exprt(name, type); + return symbol_exprt(name, type).with_source_location(location); } /// Check that the instance object is well formed. diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 3bdc97c2fd2..4b9ff978e99 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -337,8 +337,13 @@ void symex_eventt::validate_resume( REQUIRE(!events.empty()); int dst = 0; - if(!state.saved_target->source_location().get_line().empty()) + if( + state.saved_target->source_location().get_file() != + "" && + !state.saved_target->source_location().get_line().empty()) + { dst = std::stoi(state.saved_target->source_location().get_line().c_str()); + } if(state.has_saved_next_instruction) { From 0d29ab62c628620d717ab5292dce2a8d6298f895 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Aug 2023 12:53:38 +0000 Subject: [PATCH 3/7] Actually run goto-cc-multi-file regression suite We had this folder in place for a while, but it was neither included in the Makefile nor the CMake-based regression test execution. --- regression/CMakeLists.txt | 1 + regression/Makefile | 1 + regression/goto-cc-multi-file/CMakeLists.txt | 9 +++++++++ 3 files changed, 11 insertions(+) create mode 100644 regression/goto-cc-multi-file/CMakeLists.txt diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 1483ee0ea44..f243fd2087c 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -77,6 +77,7 @@ add_subdirectory(k-induction) add_subdirectory(goto-harness) add_subdirectory(goto-harness-multi-file-project) add_subdirectory(goto-cc-file-local) +add_subdirectory(goto-cc-multi-file) add_subdirectory(goto-cc-regression-gh-issue-5380) add_subdirectory(linking-goto-binaries) add_subdirectory(symtab2gb) diff --git a/regression/Makefile b/regression/Makefile index 7a8732ac264..c29abf01af7 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -50,6 +50,7 @@ DIRS = cbmc-shadow-memory \ goto-harness \ goto-harness-multi-file-project \ goto-cc-file-local \ + goto-cc-multi-file \ goto-cc-regression-gh-issue-5380 \ linking-goto-binaries \ symtab2gb \ diff --git a/regression/goto-cc-multi-file/CMakeLists.txt b/regression/goto-cc-multi-file/CMakeLists.txt new file mode 100644 index 00000000000..53647ddb692 --- /dev/null +++ b/regression/goto-cc-multi-file/CMakeLists.txt @@ -0,0 +1,9 @@ +if(WIN32) + set(is_windows true) +else() + set(is_windows false) +endif() + +add_test_pl_tests( + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ ${is_windows}" +) From 1a2918eb6e6e28297f06413a13ec116693cdd6ec Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Aug 2023 12:56:10 +0000 Subject: [PATCH 4/7] Maintain source location while replacing symbol expressions Linking (and also other workflows) use expression replacement. Doing so must not destroy the source location annotated to an expression. This left us with instructions without location. --- .../goto-cc-multi-file/maintain-location/main.c | 11 +++++++++++ .../goto-cc-multi-file/maintain-location/other.c | 6 ++++++ .../maintain-location/test.desc | 9 +++++++++ src/linking/linking.cpp | 6 ++++++ src/util/replace_symbol.cpp | 15 +++++++++++++++ 5 files changed, 47 insertions(+) create mode 100644 regression/goto-cc-multi-file/maintain-location/main.c create mode 100644 regression/goto-cc-multi-file/maintain-location/other.c create mode 100644 regression/goto-cc-multi-file/maintain-location/test.desc diff --git a/regression/goto-cc-multi-file/maintain-location/main.c b/regression/goto-cc-multi-file/maintain-location/main.c new file mode 100644 index 00000000000..a55afb81e20 --- /dev/null +++ b/regression/goto-cc-multi-file/maintain-location/main.c @@ -0,0 +1,11 @@ +int foo() +{ + return 0; +} + +int main() +{ + int result; + result = foo(); + return result; +} diff --git a/regression/goto-cc-multi-file/maintain-location/other.c b/regression/goto-cc-multi-file/maintain-location/other.c new file mode 100644 index 00000000000..6a794a79c27 --- /dev/null +++ b/regression/goto-cc-multi-file/maintain-location/other.c @@ -0,0 +1,6 @@ +int foo(); + +int bar() +{ + return foo(); +} diff --git a/regression/goto-cc-multi-file/maintain-location/test.desc b/regression/goto-cc-multi-file/maintain-location/test.desc new file mode 100644 index 00000000000..4cdabb403ff --- /dev/null +++ b/regression/goto-cc-multi-file/maintain-location/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +other.c +file main.c line 9 function main +^EXIT=0$ +^SIGNAL=0$ +-- +-- +We previously lost the location attached to the call of `foo` in function main. diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 5ed4d1dfb03..b4ba95fab2f 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -100,6 +100,11 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const const exprt &e = it->second; + source_locationt previous_source_location{s.source_location()}; + DATA_INVARIANT_WITH_DIAGNOSTICS( + previous_source_location.is_not_nil(), + "front-ends should construct symbol expressions with source locations", + s.pretty()); if(e.type().id() != ID_array && e.type().id() != ID_code) { typet type = s.type(); @@ -107,6 +112,7 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const } else static_cast(s) = e; + s.add_source_location() = std::move(previous_source_location); return false; } diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index ce30b84b239..7487f69c3bb 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -51,7 +51,12 @@ bool replace_symbolt::replace_symbol_expr(symbol_exprt &s) const s.type() == it->second.type(), "types to be replaced should match. s.type:\n" + s.type().pretty() + "\nit->second.type:\n" + it->second.type().pretty()); + source_locationt previous_source_location{s.source_location()}; static_cast(s) = it->second; + // back-end generated or internal symbols (like rounding mode) might not have + // a source location + if(s.source_location().is_nil() && previous_source_location.is_not_nil()) + s.add_source_location() = std::move(previous_source_location); return false; } @@ -334,7 +339,12 @@ bool unchecked_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const if(it == expr_map.end()) return true; + source_locationt previous_source_location{s.source_location()}; static_cast(s) = it->second; + // back-end generated or internal symbols (like rounding mode) might not have + // a source location + if(s.source_location().is_nil() && previous_source_location.is_not_nil()) + s.add_source_location() = std::move(previous_source_location); return false; } @@ -415,7 +425,12 @@ bool address_of_aware_replace_symbolt::replace_symbol_expr( // Note s_copy is no longer a symbol_exprt due to the replace operation, // and after this line `s` won't be either + source_locationt previous_source_location{s.source_location()}; s = s_copy; + // back-end generated or internal symbols (like rounding mode) might not have + // a source location + if(s.source_location().is_nil() && previous_source_location.is_not_nil()) + s.add_source_location() = std::move(previous_source_location); return false; } From 25f443688574060b6c7166fb105a5f916e2a8b92 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Nov 2023 09:59:39 +0000 Subject: [PATCH 5/7] All if-then-else goto conversion instructions have a location We must not produce goto-program instructions without location, even when they are considered dummy instructions: those instructions may subsequently be used to produce a source location, which was thus missing when converting nested if-then-else statements. --- regression/cbmc-cover/location3/main.c | 22 +++++++++++++ regression/cbmc-cover/location3/test.desc | 12 +++++++ src/goto-programs/goto_clean_expr.cpp | 9 +++++- src/goto-programs/goto_convert.cpp | 38 ++++++++++++++++++----- src/goto-programs/goto_convert_class.h | 2 ++ 5 files changed, 74 insertions(+), 9 deletions(-) create mode 100644 regression/cbmc-cover/location3/main.c create mode 100644 regression/cbmc-cover/location3/test.desc diff --git a/regression/cbmc-cover/location3/main.c b/regression/cbmc-cover/location3/main.c new file mode 100644 index 00000000000..d09b61f219e --- /dev/null +++ b/regression/cbmc-cover/location3/main.c @@ -0,0 +1,22 @@ +int main() +{ + int b, c; + + if(b) + { + if(c) + { + c = 1; + } + else + { + c = 2; + } + } + else + { + b = 0; + } + + return 1; +} diff --git a/regression/cbmc-cover/location3/test.desc b/regression/cbmc-cover/location3/test.desc new file mode 100644 index 00000000000..48e1a80f280 --- /dev/null +++ b/regression/cbmc-cover/location3/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--cover location +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.\d+\] file main.c line 9 function main block \d+ \(lines main.c:main:9,10\): SATISFIED$ +^\[main.coverage.\d+\] file main.c line 15 function main block \d+ \(lines main.c:main:15\): SATISFIED$ +^\*\* 7 of 7 covered \(100.0%\) +-- +^warning: ignoring +-- +All gotos must have a source location annotated. diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 35dce3e458a..2c9e1f32f4f 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -284,7 +284,14 @@ void goto_convertt::clean_expr( // generate guard for argument side-effects generate_ifthenelse( - if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode); + if_expr.cond(), + source_location, + tmp_true, + if_expr.true_case().source_location(), + tmp_false, + if_expr.false_case().source_location(), + dest, + mode); return; } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index b4e1a931982..4c0d74ecf52 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1613,17 +1613,34 @@ void goto_convertt::convert_ifthenelse( // convert 'then'-branch goto_programt tmp_then; convert(code.then_case(), tmp_then, mode); + source_locationt then_end_location = + code.then_case().get_statement() == ID_block + ? to_code_block(code.then_case()).end_location() + : code.then_case().source_location(); goto_programt tmp_else; + source_locationt else_end_location; if(has_else) + { convert(code.else_case(), tmp_else, mode); + else_end_location = code.else_case().get_statement() == ID_block + ? to_code_block(code.else_case()).end_location() + : code.else_case().source_location(); + } exprt tmp_guard=code.cond(); clean_expr(tmp_guard, dest, mode); generate_ifthenelse( - tmp_guard, tmp_then, tmp_else, source_location, dest, mode); + tmp_guard, + source_location, + tmp_then, + then_end_location, + tmp_else, + else_end_location, + dest, + mode); } void goto_convertt::collect_operands( @@ -1655,9 +1672,11 @@ static inline bool is_size_one(const goto_programt &g) /// if(guard) true_case; else false_case; void goto_convertt::generate_ifthenelse( const exprt &guard, + const source_locationt &source_location, goto_programt &true_case, + const source_locationt &then_end_location, goto_programt &false_case, - const source_locationt &source_location, + const source_locationt &else_end_location, goto_programt &dest, const irep_idt &mode) { @@ -1727,13 +1746,17 @@ void goto_convertt::generate_ifthenelse( // Flip around if no 'true' case code. if(is_empty(true_case)) + { return generate_ifthenelse( boolean_negate(guard), + source_location, false_case, + else_end_location, true_case, - source_location, + then_end_location, dest, mode); + } bool has_else=!is_empty(false_case); @@ -1753,14 +1776,13 @@ void goto_convertt::generate_ifthenelse( // do the x label goto_programt tmp_x; - goto_programt::targett x = tmp_x.add(goto_programt::make_incomplete_goto( - true_exprt(), true_case.instructions.back().source_location())); + goto_programt::targett x = tmp_x.add( + goto_programt::make_incomplete_goto(true_exprt(), then_end_location)); // do the z label goto_programt tmp_z; - goto_programt::targett z = tmp_z.add(goto_programt::make_skip()); - // We deliberately don't set a location for 'z', it's a dummy - // target. + goto_programt::targett z = tmp_z.add( + goto_programt::make_skip(has_else ? else_end_location : then_end_location)); // y: Q; goto_programt tmp_y; diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 661260dd1d8..ee10e914326 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -576,7 +576,9 @@ class goto_convertt:public messaget // if(cond) { true_case } else { false_case } void generate_ifthenelse( const exprt &cond, + const source_locationt &, goto_programt &true_case, + const source_locationt &, goto_programt &false_case, const source_locationt &, goto_programt &dest, From f3da348c5ae4db597b2ac091001478fa6a3ae180 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Nov 2023 12:00:48 +0000 Subject: [PATCH 6/7] switch-case conversion: ensure case selection has source location The expression operand was at times lacking a source location when it had been subject to expression simplification. Fixes the root cause in the C front-end, and makes sure the invariant is maintained during goto conversion. --- jbmc/src/java_bytecode/nondet.cpp | 4 +++- src/ansi-c/c_typecheck_expr.cpp | 19 +++++++++++++------ src/goto-programs/goto_convert.cpp | 7 +++++++ 3 files changed, 23 insertions(+), 7 deletions(-) diff --git a/jbmc/src/java_bytecode/nondet.cpp b/jbmc/src/java_bytecode/nondet.cpp index 3a6092092ab..5269e7004b3 100644 --- a/jbmc/src/java_bytecode/nondet.cpp +++ b/jbmc/src/java_bytecode/nondet.cpp @@ -123,7 +123,9 @@ code_blockt generate_nondet_switch( this_block.add(switch_case); this_block.add(code_breakt()); code_switch_caset this_case( - from_integer(case_number, switch_value.type()), this_block); + from_integer(case_number, switch_value.type()) + .with_source_location(source_location), + this_block); switch_block.add(std::move(this_case)); ++case_number; } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index ab278de784f..f4535763987 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1044,15 +1044,16 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr) new_expr = size_of_opt.value(); } + source_locationt location = expr.source_location(); new_expr.swap(expr); - + expr.add_source_location() = location; expr.add(ID_C_c_sizeof_type)=type; // The type may contain side-effects. if(!clean_code.empty()) { side_effect_exprt side_effect_expr( - ID_statement_expression, void_type(), expr.source_location()); + ID_statement_expression, void_type(), location); auto decl_block=code_blockt::from_list(clean_code); decl_block.set_statement(ID_decl_block); side_effect_expr.copy_to_operands(decl_block); @@ -1064,8 +1065,9 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr) // It is not obvious whether the type or 'e' should be evaluated // first. - binary_exprt comma_expr{ - std::move(side_effect_expr), ID_comma, expr, expr.type()}; + exprt comma_expr = + binary_exprt{std::move(side_effect_expr), ID_comma, expr, expr.type()} + .with_source_location(location); expr.swap(comma_expr); } } @@ -4656,6 +4658,8 @@ class is_compile_time_constantt void c_typecheck_baset::make_constant(exprt &expr) { + source_locationt location = expr.find_source_location(); + // Floating-point expressions may require a rounding mode. // ISO 9899:1999 F.7.2 says that the default is "round to nearest". // Some compilers have command-line options to override. @@ -4664,10 +4668,11 @@ void c_typecheck_baset::make_constant(exprt &expr) adjust_float_expressions(expr, rounding_mode); simplify(expr, *this); + expr.add_source_location() = location; if(!is_compile_time_constantt(*this)(expr)) { - error().source_location=expr.find_source_location(); + error().source_location = location; error() << "expected constant expression, but got '" << to_string(expr) << "'" << eom; throw 0; @@ -4676,13 +4681,15 @@ void c_typecheck_baset::make_constant(exprt &expr) void c_typecheck_baset::make_constant_index(exprt &expr) { + source_locationt location = expr.find_source_location(); make_constant(expr); make_index_type(expr); simplify(expr, *this); + expr.add_source_location() = location; if(!is_compile_time_constantt(*this)(expr)) { - error().source_location=expr.find_source_location(); + error().source_location = location; error() << "conversion to integer constant failed" << eom; throw 0; } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 4c0d74ecf52..f7725df3136 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -526,6 +526,13 @@ void goto_convertt::convert_switch_case( exprt::operandst &case_op_dest=cases_entry->second->second; case_op_dest.push_back(code.case_op()); + // make sure we have a source location in the case operand as otherwise we + // end up with a GOTO instruction without a source location + DATA_INVARIANT_WITH_DIAGNOSTICS( + case_op_dest.back().source_location().is_not_nil(), + "case operand should have a source location", + case_op_dest.back().pretty(), + code.pretty()); } } From 5d8abbe4ba1cf020a925ae0715d037050d15c73d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Nov 2023 12:02:48 +0000 Subject: [PATCH 7/7] Function pointer removal: ensure presence of source location Return type fix-up tried to use the source location from the function-call code, which had just been constructed and necessarily lacked a source location. Instead, explicitly pass a source location. --- src/goto-programs/remove_function_pointers.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index f8bc52605ec..7db4f3456b7 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -205,6 +205,7 @@ static void fix_argument_types(code_function_callt &function_call) static void fix_return_type( const irep_idt &in_function_id, code_function_callt &function_call, + const source_locationt &source_location, symbol_tablet &symbol_table, goto_programt &dest) { @@ -226,7 +227,7 @@ static void fix_return_type( code_type.return_type(), id2string(in_function_id), "tmp_return_val_" + id2string(function_symbol.base_name), - function_call.source_location(), + source_location, function_symbol.mode, symbol_table); @@ -239,7 +240,7 @@ static void fix_return_type( old_lhs, make_byte_extract( tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()), - function_call.source_location()))); + source_location))); } void remove_function_pointerst::remove_function_pointer( @@ -407,7 +408,8 @@ void remove_function_pointer( fix_argument_types(new_call); goto_programt tmp; - fix_return_type(function_id, new_call, symbol_table, tmp); + fix_return_type( + function_id, new_call, target->source_location(), symbol_table, tmp); auto call = new_code_calls.add( goto_programt::make_function_call(new_call, target->source_location()));