From c0d7491f2e6c42fc8c3f141de1f22a47651f1d8f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 30 Nov 2025 13:21:06 +0000 Subject: [PATCH] Refactor entry point validation towards symex-callers We can detect the absence of an entry point much earlier and do not need to perform unnecessary work before inevitably failing. This also fixes a bug where `can_produce_function` did not accurately reflect what functions could be produced. Fixes: #1847 --- .../java_bytecode/lazy_goto_functions_map.h | 12 +++++++-- .../multi_path_symex_only_checker.cpp | 6 +++++ .../single_loop_incremental_symex_checker.cpp | 6 +++++ .../single_path_symex_only_checker.cpp | 6 +++++ src/goto-symex/goto_symex.h | 3 +++ src/goto-symex/symex_main.cpp | 26 ++++++++----------- 6 files changed, 42 insertions(+), 17 deletions(-) diff --git a/jbmc/src/java_bytecode/lazy_goto_functions_map.h b/jbmc/src/java_bytecode/lazy_goto_functions_map.h index 4d7e2dcd641..1301412e596 100644 --- a/jbmc/src/java_bytecode/lazy_goto_functions_map.h +++ b/jbmc/src/java_bytecode/lazy_goto_functions_map.h @@ -123,8 +123,16 @@ class lazy_goto_functions_mapt final /// it a bodyless stub. bool can_produce_function(const key_type &name) const { - return language_files.can_convert_lazy_method(name) || - driver_program_can_generate_function_body(name); + if( + language_files.can_convert_lazy_method(name) || + driver_program_can_generate_function_body(name)) + { + return true; + } + + const symbolt *sym_ptr = symbol_table.lookup(name); + return sym_ptr && sym_ptr->type.id() == ID_code && + sym_ptr->value.is_not_nil(); } /// Remove the function named \p name from the function map, if it exists. diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index ce81e072e1d..9b38f4cf367 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, Peter Schrammel #include "multi_path_symex_only_checker.h" +#include #include #include @@ -80,6 +81,11 @@ void multi_path_symex_only_checkert::generate_equation() const auto symex_start = std::chrono::steady_clock::now(); + // Validate that the entry point exists before calling symex + const irep_idt entry_point_id = goto_functionst::entry_point(); + if(!goto_model.can_produce_function(entry_point_id)) + throw invalid_input_exceptiont("the program has no entry point"); + symex_symbol_table = symex.symex_from_entry_point_of( goto_symext::get_goto_function(goto_model), fields); diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp index f264a728f58..e1b729a8787 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, Peter Schrammel #include "single_loop_incremental_symex_checker.h" +#include #include #include @@ -77,6 +78,11 @@ operator()(propertiest &properties) // we haven't got an equation yet if(!initial_equation_generated) { + // Validate that the entry point exists before calling symex + const irep_idt entry_point_id = goto_functionst::entry_point(); + if(!goto_model.can_produce_function(entry_point_id)) + throw invalid_input_exceptiont("the program has no entry point"); + full_equation_generated = !symex.from_entry_point_of( goto_symext::get_goto_function(goto_model), symex_symbol_table); diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp index 7a5e8ffe5b7..923c51aff57 100644 --- a/src/goto-checker/single_path_symex_only_checker.cpp +++ b/src/goto-checker/single_path_symex_only_checker.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, Peter Schrammel #include "single_path_symex_only_checker.h" +#include #include #include @@ -80,6 +81,11 @@ void single_path_symex_only_checkert::initialize_worklist() const auto fields = shadow_memoryt::gather_field_declarations(goto_model, ui_message_handler); + // Validate that the entry point exists before calling symex + const irep_idt entry_point_id = goto_functionst::entry_point(); + if(!goto_model.can_produce_function(entry_point_id)) + throw invalid_input_exceptiont("the program has no entry point"); + symex.initialize_path_storage_from_entry_point_of( goto_symext::get_goto_function(goto_model), symex_symbol_table, fields); } diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 5980573f0cd..915465984e1 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -189,6 +189,9 @@ class goto_symext /// the beginning of the entry point function. /// \param get_goto_function: producer for GOTO functions /// \return Initialized symex state. + /// \pre The entry point function must exist in the model provided by + /// get_goto_function. Callers should validate this before calling this + /// method to ensure proper error reporting. std::unique_ptr initialize_entry_point_state(const get_goto_functiont &get_goto_function); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 4fe53bc7c61..a2a69db4bf6 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -399,15 +399,11 @@ std::unique_ptr goto_symext::initialize_entry_point_state( { const irep_idt entry_point_id = goto_functionst::entry_point(); - const goto_functionst::goto_functiont *start_function; - try - { - start_function = &get_goto_function(entry_point_id); - } - catch(const std::out_of_range &) - { - throw unsupported_operation_exceptiont("the program has no entry point"); - } + // Entry point existence must be validated by callers before calling + // this function. If get_goto_function throws std::out_of_range, it + // indicates a precondition violation. + const goto_functionst::goto_functiont &start_function = + get_goto_function(entry_point_id); // Get our path_storage pointer because this state will live beyond // this instance of goto_symext, so we can't take the reference directly. @@ -415,7 +411,7 @@ std::unique_ptr goto_symext::initialize_entry_point_state( // create and prepare the state auto state = std::make_unique( - symex_targett::sourcet(entry_point_id, start_function->body), + symex_targett::sourcet(entry_point_id, start_function.body), symex_config.max_field_sensitivity_array_size, symex_config.simplify_opt, language_mode, @@ -426,11 +422,11 @@ std::unique_ptr goto_symext::initialize_entry_point_state( CHECK_RETURN(!state->call_stack().empty()); goto_programt::const_targett limit = - std::prev(start_function->body.instructions.end()); + std::prev(start_function.body.instructions.end()); state->call_stack().top().end_of_function = limit; state->call_stack().top().calling_location.pc = state->call_stack().top().end_of_function; - state->call_stack().top().hidden_function = start_function->is_hidden(); + state->call_stack().top().hidden_function = start_function.is_hidden(); state->symex_target = ⌖ @@ -440,17 +436,17 @@ std::unique_ptr goto_symext::initialize_entry_point_state( auto emplace_safe_pointers_result = path_storage.safe_pointers.emplace(entry_point_id, local_safe_pointerst{}); if(emplace_safe_pointers_result.second) - emplace_safe_pointers_result.first->second(start_function->body); + emplace_safe_pointers_result.first->second(start_function.body); path_storage.dirty.populate_dirty_for_function( - entry_point_id, *start_function); + entry_point_id, start_function); state->dirty = &path_storage.dirty; // Only enable loop analysis when complexity is enabled. if(symex_config.complexity_limits_active) { // Set initial loop analysis. - path_storage.add_function_loops(entry_point_id, start_function->body); + path_storage.add_function_loops(entry_point_id, start_function.body); state->call_stack().top().loops_info = path_storage.get_loop_analysis(entry_point_id); }