Re-use symex state initialisation helper in loop acceleration

The local attempt of initialisation did not keep up with changes and
assumptions made by goto_symext, resulting in segmentation faults when
trying to use this code.

Author: tautschnig

src/goto-instrument/accelerate/scratch_program.cpp

@@ -36,20 +36,20 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
   output(ns, "scratch", std::cout);
 #endif
 
-  symex_state = util_make_unique<goto_symex_statet>(
-    symex_targett::sourcet(goto_functionst::entry_point(), *this),
-    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
-    guard_manager,
-    [this](const irep_idt &id) {
-      return path_storage.get_unique_l2_index(id);
-    });
-
-  symex.symex_with_state(
-    *symex_state,
-    [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {
+  goto_functiont this_goto_function;
+  this_goto_function.body.copy_from(*this);
+  auto get_goto_function =
+    [this, &this_goto_function](
+      const irep_idt &key) -> const goto_functionst::goto_functiont & {
+    if(key == goto_functionst::entry_point())
+      return this_goto_function;
+    else
       return functions.function_map.at(key);
-    },
-    symex_symbol_table);
+  };
+
+  symex_state = symex.initialize_entry_point_state(get_goto_function);
+
+  symex.symex_with_state(*symex_state, get_goto_function, symex_symbol_table);
 
   if(do_slice)
   {

src/goto-instrument/accelerate/scratch_program.h

@@ -33,6 +33,33 @@ Author: Matt Lewis
 
 #include "path.h"
 
+// Wrapper around goto_symext to make initialize_entry_point_state available.
+struct scratch_program_symext : public goto_symext
+{
+  scratch_program_symext(
+    message_handlert &mh,
+    const symbol_tablet &outer_symbol_table,
+    symex_target_equationt &_target,
+    const optionst &options,
+    path_storaget &path_storage,
+    guard_managert &guard_manager)
+    : goto_symext(
+        mh,
+        outer_symbol_table,
+        _target,
+        options,
+        path_storage,
+        guard_manager)
+  {
+  }
+
+  std::unique_ptr<statet>
+  initialize_entry_point_state(const get_goto_functiont &get_goto_function)
+  {
+    return goto_symext::initialize_entry_point_state(get_goto_function);
+  }
+};
+
 class scratch_programt:public goto_programt
 {
 public:
@@ -85,7 +112,7 @@ class scratch_programt:public goto_programt
   symex_target_equationt equation;
   path_fifot path_storage;
   optionst options;
-  goto_symext symex;
+  scratch_program_symext symex;
 
   std::unique_ptr<propt> satcheck;
   bv_pointerst satchecker;