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.

Fixes: #1847

Author: tautschnig

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -11,8 +11,11 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "multi_path_symex_only_checker.h"
 
+#include <util/exception_utils.h>
 #include <util/ui_message.h>
 
+#include <goto-programs/goto_functions.h>
+
 #include <goto-symex/shadow_memory.h>
 #include <goto-symex/show_program.h>
 #include <goto-symex/show_vcc.h>
@@ -80,6 +83,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_path_symex_only_checker.cpp

@@ -11,8 +11,11 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "single_path_symex_only_checker.h"
 
+#include <util/exception_utils.h>
 #include <util/ui_message.h>
 
+#include <goto-programs/goto_functions.h>
+
 #include <goto-symex/path_storage.h>
 #include <goto-symex/shadow_memory.h>
 #include <goto-symex/show_program.h>
@@ -80,6 +83,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-checker/symex_bmc_incremental_one_loop.cpp

@@ -8,8 +8,10 @@ Author: Peter Schrammel, Daniel Kroening, [email protected]
 
 #include "symex_bmc_incremental_one_loop.h"
 
+#include <util/exception_utils.h>
 #include <util/structured_data.h>
 
+#include <goto-programs/goto_functions.h>
 #include <goto-programs/unwindset.h>
 
 #include <limits>
@@ -126,6 +128,11 @@ bool symex_bmc_incremental_one_loopt::from_entry_point_of(
   const get_goto_functiont &get_goto_function,
   symbol_tablet &new_symbol_table)
 {
+  // 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");
+
   state = initialize_entry_point_state(get_goto_function);
 
   new_symbol_table = symex_with_state(*state, get_goto_function);

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);
   }