Refactor entry point validation towards symex-callers

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.

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 <util/exception_utils.h>
 #include <util/ui_message.h>
 
 #include <goto-symex/shadow_memory.h>
@@ -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);
 

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 <util/exception_utils.h>
 #include <util/structured_data.h>
 
 #include <goto-symex/slice.h>
@@ -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);
 

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 <util/exception_utils.h>
 #include <util/ui_message.h>
 
 #include <goto-symex/path_storage.h>
@@ -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);
 }

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<statet>
   initialize_entry_point_state(const get_goto_functiont &get_goto_function);
 

src/goto-symex/symex_main.cpp

@@ -399,23 +399,19 @@ std::unique_ptr<goto_symext::statet> 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.
   auto *storage = &path_storage;
 
   // create and prepare the state
   auto state = std::make_unique<statet>(
-    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::statet> 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 = &target;
 
@@ -440,17 +436,17 @@ std::unique_ptr<goto_symext::statet> 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);
   }