unwindsett: goto_model is only needed for options processing

An `unwindsett` does not need an `abstract_goto_modelt` as part of its
state.

Author: tautschnig

src/goto-checker/bmc_util.cpp

@@ -178,7 +178,6 @@ get_memory_model(const optionst &options, const namespacet &ns)
 void setup_symex(
   symex_bmct &symex,
   const namespacet &ns,
-  const optionst &options,
   ui_message_handlert &ui_message_handler)
 {
   messaget msg(ui_message_handler);
@@ -189,10 +188,6 @@ void setup_symex(
   msg.status() << "Starting Bounded Model Checking" << messaget::eom;
 
   symex.last_source_location.make_nil();
-
-  symex.unwindset.parse_unwind(options.get_option("unwind"));
-  symex.unwindset.parse_unwindset(
-    options.get_list_option("unwindset"), ui_message_handler);
 }
 
 void slice(

src/goto-checker/bmc_util.h

@@ -68,11 +68,7 @@ void output_graphml(
 std::unique_ptr<memory_model_baset>
 get_memory_model(const optionst &options, const namespacet &);
 
-void setup_symex(
-  symex_bmct &,
-  const namespacet &,
-  const optionst &,
-  ui_message_handlert &);
+void setup_symex(symex_bmct &, const namespacet &, ui_message_handlert &);
 
 void slice(
   symex_bmct &,

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -27,7 +27,6 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     equation(ui_message_handler),
-    unwindset(goto_model),
     symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
@@ -37,7 +36,10 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
       guard_manager,
       unwindset)
 {
-  setup_symex(symex, ns, options, ui_message_handler);
+  unwindset.parse_unwind(options.get_option("unwind"));
+  unwindset.parse_unwindset(
+    options.get_list_option("unwindset"), goto_model, ui_message_handler);
+  setup_symex(symex, ns, ui_message_handler);
 }
 
 incremental_goto_checkert::resultt multi_path_symex_only_checkert::

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -28,7 +28,6 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     equation(ui_message_handler),
-    unwindset(goto_model),
     symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
@@ -40,7 +39,10 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
       ui_message_handler.get_ui()),
     property_decider(options, ui_message_handler, equation, ns)
 {
-  setup_symex(symex, ns, options, ui_message_handler);
+  unwindset.parse_unwind(options.get_option("unwind"));
+  unwindset.parse_unwindset(
+    options.get_list_option("unwindset"), goto_model, ui_message_handler);
+  setup_symex(symex, ns, ui_message_handler);
 
   // Freeze all symbols if we are using a prop_conv_solvert
   prop_conv_solvert *prop_conv_solver = dynamic_cast<prop_conv_solvert *>(

src/goto-checker/single_path_symex_only_checker.cpp

@@ -29,9 +29,11 @@ single_path_symex_only_checkert::single_path_symex_only_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     worklist(get_path_strategy(options.get_option("exploration-strategy"))),
-    symex_runtime(0),
-    unwindset(goto_model)
+    symex_runtime(0)
 {
+  unwindset.parse_unwind(options.get_option("unwind"));
+  unwindset.parse_unwindset(
+    options.get_list_option("unwindset"), goto_model, ui_message_handler);
 }
 
 incremental_goto_checkert::resultt single_path_symex_only_checkert::
@@ -152,7 +154,7 @@ void single_path_symex_only_checkert::equation_output(
 
 void single_path_symex_only_checkert::setup_symex(symex_bmct &symex)
 {
-  ::setup_symex(symex, ns, options, ui_message_handler);
+  ::setup_symex(symex, ns, ui_message_handler);
 }
 
 void single_path_symex_only_checkert::update_properties(

src/goto-checker/symex_bmc.h

@@ -81,9 +81,9 @@ class symex_bmct : public goto_symext
 
   const bool record_coverage;
 
+protected:
   unwindsett &unwindset;
 
-protected:
   /// Callbacks that may provide an unwind/do-not-unwind decision for a loop
   std::vector<loop_unwind_handlert> loop_unwind_handlers;
 

src/goto-instrument/contracts/contracts.cpp

@@ -1493,8 +1493,9 @@ void code_contractst::apply_loop_contracts(
   // unwind all transformed loops twice.
   if(loop_contract_config.unwind_transformed_loops)
   {
-    unwindsett unwindset{goto_model};
-    unwindset.parse_unwindset(loop_names, log.get_message_handler());
+    unwindsett unwindset;
+    unwindset.parse_unwindset(
+      loop_names, goto_model, log.get_message_handler());
     goto_unwindt goto_unwind;
     goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
   }

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp

@@ -1208,8 +1208,8 @@ void dfcc_instrumentt::apply_loop_contracts(
   // If required, unwind all transformed loops to yield base and step cases
   if(loop_contract_config.unwind_transformed_loops)
   {
-    unwindsett unwindset{goto_model};
-    unwindset.parse_unwindset(to_unwind, log.get_message_handler());
+    unwindsett unwindset;
+    unwindset.parse_unwindset(to_unwind, goto_model, log.get_message_handler());
     goto_unwindt goto_unwind;
     goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
   }

src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp

@@ -439,7 +439,6 @@ void dfcc_libraryt::specialize(const std::size_t contract_assigns_size)
     "dfcc_libraryt::specialize_functions can only be called once");
 
   specialized = true;
-  unwindsett unwindset{goto_model};
   std::list<std::string> loop_names;
 
   for(const auto &entry : to_unwind)
@@ -452,7 +451,8 @@ void dfcc_libraryt::specialize(const std::size_t contract_assigns_size)
     const auto &str = stream.str();
     loop_names.push_back(str);
   }
-  unwindset.parse_unwindset(loop_names, message_handler);
+  unwindsett unwindset;
+  unwindset.parse_unwindset(loop_names, goto_model, message_handler);
   goto_unwindt goto_unwind;
   goto_unwind(
     goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSERT_ASSUME);

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -183,21 +183,24 @@ int goto_instrument_parse_optionst::doit()
 
       if(unwind_given || unwindset_given || unwindset_file_given)
       {
-        unwindsett unwindset{goto_model};
+        unwindsett unwindset;
 
         if(unwind_given)
           unwindset.parse_unwind(cmdline.get_value("unwind"));
 
         if(unwindset_file_given)
         {
           unwindset.parse_unwindset_file(
-            cmdline.get_value("unwindset-file"), ui_message_handler);
+            cmdline.get_value("unwindset-file"),
+            goto_model,
+            ui_message_handler);
         }
 
         if(unwindset_given)
         {
           unwindset.parse_unwindset(
             cmdline.get_comma_separated_values("unwindset"),
+            goto_model,
             ui_message_handler);
         }
 

src/goto-instrument/unwindset.cpp

@@ -28,6 +28,7 @@ void unwindsett::parse_unwind(const std::string &unwind)
 
 void unwindsett::parse_unwindset_one_loop(
   std::string val,
+  abstract_goto_modelt &goto_model,
   message_handlert &message_handler)
 {
   if(val.empty())
@@ -181,10 +182,11 @@ void unwindsett::parse_unwindset_one_loop(
 
 void unwindsett::parse_unwindset(
   const std::list<std::string> &unwindset,
+  abstract_goto_modelt &goto_model,
   message_handlert &message_handler)
 {
   for(auto &element : unwindset)
-    parse_unwindset_one_loop(element, message_handler);
+    parse_unwindset_one_loop(element, goto_model, message_handler);
 }
 
 std::optional<unsigned>
@@ -211,6 +213,7 @@ unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
 
 void unwindsett::parse_unwindset_file(
   const std::string &file_name,
+  abstract_goto_modelt &goto_model,
   message_handlert &message_handler)
 {
   std::ifstream file(widen_if_needed(file_name));
@@ -225,5 +228,5 @@ void unwindsett::parse_unwindset_file(
     split_string(buffer.str(), ',', true, true);
 
   for(auto &element : unwindset_elements)
-    parse_unwindset_one_loop(element, message_handler);
+    parse_unwindset_one_loop(element, goto_model, message_handler);
 }

src/goto-instrument/unwindset.h

@@ -30,16 +30,15 @@ class unwindsett
   // 2) a limit per loop, all threads
   // 3) a limit for a particular thread.
   // We use the most specific of the above.
-  explicit unwindsett(abstract_goto_modelt &goto_model) : goto_model(goto_model)
-  {
-  }
+  unwindsett() = default;
 
   // global limit for all loops
   void parse_unwind(const std::string &unwind);
 
   // limit for instances of a loop
   void parse_unwindset(
     const std::list<std::string> &unwindset,
+    abstract_goto_modelt &goto_model,
     message_handlert &message_handler);
 
   // queries
@@ -49,11 +48,10 @@ class unwindsett
   // read unwindset directives from a file
   void parse_unwindset_file(
     const std::string &file_name,
+    abstract_goto_modelt &goto_model,
     message_handlert &message_handler);
 
 protected:
-  abstract_goto_modelt &goto_model;
-
   std::optional<unsigned> global_limit;
 
   // Limit for all instances of a loop.
@@ -68,6 +66,7 @@ class unwindsett
 
   void parse_unwindset_one_loop(
     std::string loop_limit,
+    abstract_goto_modelt &goto_model,
     message_handlert &message_handler);
 };
 

unit/path_strategies.cpp

@@ -415,7 +415,10 @@ void _check_with_strategy(
   propertiest properties(initialize_properties(goto_model));
   std::unique_ptr<path_storaget> worklist = get_path_strategy(strategy);
   guard_managert guard_manager;
-  unwindsett unwindset{goto_model};
+  unwindsett unwindset;
+  unwindset.parse_unwind(options.get_option("unwind"));
+  unwindset.parse_unwindset(
+    options.get_list_option("unwindset"), goto_model, ui_message_handler);
 
   {
     // Put initial state into the work list
@@ -428,7 +431,7 @@ void _check_with_strategy(
       *worklist,
       guard_manager,
       unwindset);
-    setup_symex(symex, ns, options, ui_message_handler);
+    setup_symex(symex, ns, ui_message_handler);
 
     symex.initialize_path_storage_from_entry_point_of(
       goto_symext::get_goto_function(goto_model),
@@ -451,7 +454,7 @@ void _check_with_strategy(
       *worklist,
       guard_manager,
       unwindset);
-    setup_symex(symex, ns, options, ui_message_handler);
+    setup_symex(symex, ns, ui_message_handler);
 
     symex_symbol_table = symex.resume_symex_from_saved_state(
       goto_symext::get_goto_function(goto_model),