Merge pull request #8643 from tautschnig/unwindsett-constructor

kroening · web-flow · commit 15b00035c2de · 2025-08-23T17:44:23.000-07:00
unwindsett: goto_model is only needed for options processing
diff --git a/src/goto-checker/bmc_util.cpp b/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(
diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h
@@ -69,11 +69,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 &,
diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/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::
diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/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 *>(
diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/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(
diff --git a/src/goto-checker/symex_bmc.h b/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;
 
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
@@ -1480,8 +1480,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);
   }
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/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);
   }
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/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);
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/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);
         }
 
diff --git a/src/goto-programs/unwindset.cpp b/src/goto-programs/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);
 }
diff --git a/src/goto-programs/unwindset.h b/src/goto-programs/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);
 };
 
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
@@ -409,7 +409,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
@@ -422,7 +425,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),
@@ -445,7 +448,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),

Original file line number	Diff line number	Diff line change
`@@ -29,9 +29,11 @@ single_path_symex_only_checkert::single_path_symex_only_checkert(`
`29`	`29`	`goto_model(goto_model),`
`30`	`30`	`ns(goto_model.get_symbol_table(), symex_symbol_table),`
`31`	`31`	`worklist(get_path_strategy(options.get_option("exploration-strategy"))),`
`32`		`- symex_runtime(0),`
`33`		`- unwindset(goto_model)`
	`32`	`+ symex_runtime(0)`
`34`	`33`	`{`
	`34`	`+ unwindset.parse_unwind(options.get_option("unwind"));`
	`35`	`+ unwindset.parse_unwindset(`
	`36`	`+ options.get_list_option("unwindset"), goto_model, ui_message_handler);`
`35`	`37`	`}`
`36`	`38`
`37`	`39`	`incremental_goto_checkert::resultt single_path_symex_only_checkert::`
`@@ -152,7 +154,7 @@ void single_path_symex_only_checkert::equation_output(`
`152`	`154`
`153`	`155`	`void single_path_symex_only_checkert::setup_symex(symex_bmct &symex)`
`154`	`156`	`{`
`155`		`- ::setup_symex(symex, ns, options, ui_message_handler);`
	`157`	`+ ::setup_symex(symex, ns, ui_message_handler);`
`156`	`158`	`}`
`157`	`159`
`158`	`160`	`void single_path_symex_only_checkert::update_properties(`
Original file line number	Diff line number	Diff line change
`@@ -1480,8 +1480,9 @@ void code_contractst::apply_loop_contracts(`
`1480`	`1480`	`// unwind all transformed loops twice.`
`1481`	`1481`	`if(loop_contract_config.unwind_transformed_loops)`
`1482`	`1482`	`{`
`1483`		`- unwindsett unwindset{goto_model};`
`1484`		`- unwindset.parse_unwindset(loop_names, log.get_message_handler());`
	`1483`	`+ unwindsett unwindset;`
	`1484`	`+ unwindset.parse_unwindset(`
	`1485`	`+ loop_names, goto_model, log.get_message_handler());`
`1485`	`1486`	`goto_unwindt goto_unwind;`
`1486`	`1487`	`goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);`
`1487`	`1488`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1208,8 +1208,8 @@ void dfcc_instrumentt::apply_loop_contracts(`
`1208`	`1208`	`// If required, unwind all transformed loops to yield base and step cases`
`1209`	`1209`	`if(loop_contract_config.unwind_transformed_loops)`
`1210`	`1210`	`{`
`1211`		`- unwindsett unwindset{goto_model};`
`1212`		`- unwindset.parse_unwindset(to_unwind, log.get_message_handler());`
	`1211`	`+ unwindsett unwindset;`
	`1212`	`+ unwindset.parse_unwindset(to_unwind, goto_model, log.get_message_handler());`
`1213`	`1213`	`goto_unwindt goto_unwind;`
`1214`	`1214`	`goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);`
`1215`	`1215`	`}`
Original file line number	Diff line number	Diff line change
`@@ -183,21 +183,24 @@ int goto_instrument_parse_optionst::doit()`
`183`	`183`
`184`	`184`	`if(unwind_given \|\| unwindset_given \|\| unwindset_file_given)`
`185`	`185`	`{`
`186`		`- unwindsett unwindset{goto_model};`
	`186`	`+ unwindsett unwindset;`
`187`	`187`
`188`	`188`	`if(unwind_given)`
`189`	`189`	`unwindset.parse_unwind(cmdline.get_value("unwind"));`
`190`	`190`
`191`	`191`	`if(unwindset_file_given)`
`192`	`192`	`{`
`193`	`193`	`unwindset.parse_unwindset_file(`
`194`		`- cmdline.get_value("unwindset-file"), ui_message_handler);`
	`194`	`+ cmdline.get_value("unwindset-file"),`
	`195`	`+ goto_model,`
	`196`	`+ ui_message_handler);`
`195`	`197`	`}`
`196`	`198`
`197`	`199`	`if(unwindset_given)`
`198`	`200`	`{`
`199`	`201`	`unwindset.parse_unwindset(`
`200`	`202`	`cmdline.get_comma_separated_values("unwindset"),`
	`203`	`+ goto_model,`
`201`	`204`	`ui_message_handler);`
`202`	`205`	`}`
`203`	`206`