unwindset: Warn about non-existent loops

f170ba1 introduced validation of loop identifiers. Syntactically
invalid ones result in exceptions being thrown. Syntactically valid, but
non-existent ones previously also failed an exception. This is now
reduced to a warning to avoid breaking verification workflows that use
the same unwindset specifications with `goto-instrument` followed by
`cbmc`: `goto-instrument` would unwind the loops already, therefore
removing them from the goto program seen by CBMC. Such workflows should
likely be cleaned up, but we shouldn't immediately break them.

Author: tautschnig

regression/cbmc/unwindset1/test.desc

@@ -1,10 +1,9 @@
 CORE
 main.c
 --unwindset main.0:2,main.2:2
-^Invalid User Input$
-^Option: unwindset$
-^Reason: invalid loop identifier main\.2$
-^EXIT=1$
+^loop identifier main.2 provided with unwindset does not match any loop$
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/goto-checker/bmc_util.cpp

@@ -192,7 +192,8 @@ void setup_symex(
   symex.last_source_location.make_nil();
 
   symex.unwindset.parse_unwind(options.get_option("unwind"));
-  symex.unwindset.parse_unwindset(options.get_list_option("unwindset"));
+  symex.unwindset.parse_unwindset(
+    options.get_list_option("unwindset"), ui_message_handler);
 }
 
 void slice(

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -171,10 +171,16 @@ int goto_instrument_parse_optionst::doit()
           unwindset.parse_unwind(cmdline.get_value("unwind"));
 
         if(unwindset_file_given)
-          unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
+        {
+          unwindset.parse_unwindset_file(
+            cmdline.get_value("unwindset-file"), ui_message_handler);
+        }
 
         if(unwindset_given)
-          unwindset.parse_unwindset(cmdline.get_values("unwindset"));
+        {
+          unwindset.parse_unwindset(
+            cmdline.get_values("unwindset"), ui_message_handler);
+        }
 
         bool unwinding_assertions=cmdline.isset("unwinding-assertions");
         bool partial_loops=cmdline.isset("partial-loops");

src/goto-instrument/unwindset.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "unwindset.h"
 
 #include <util/exception_utils.h>
+#include <util/message.h>
 #include <util/string2int.h>
 #include <util/string_utils.h>
 
@@ -24,7 +25,9 @@ void unwindsett::parse_unwind(const std::string &unwind)
     global_limit = unsafe_string2unsigned(unwind);
 }
 
-void unwindsett::parse_unwindset_one_loop(std::string val)
+void unwindsett::parse_unwindset_one_loop(
+  std::string val,
+  message_handlert &message_handler)
 {
   if(val.empty())
     return;
@@ -94,8 +97,11 @@ void unwindsett::parse_unwindset_one_loop(std::string val)
           });
         if(!found)
         {
-          throw invalid_command_line_argument_exceptiont{
-            "invalid loop identifier " + id, "unwindset"};
+          messaget log{message_handler};
+          log.warning() << "loop identifier " << id
+                        << " provided with unwindset does not match any loop"
+                        << messaget::eom;
+          return;
         }
       }
       else
@@ -122,8 +128,11 @@ void unwindsett::parse_unwindset_one_loop(std::string val)
         }
         if(!nr.has_value())
         {
-          throw invalid_command_line_argument_exceptiont{
-            "loop identifier " + id + " does not match any loop", "unwindset"};
+          messaget log{message_handler};
+          log.warning() << "loop identifier " << id
+                        << " provided with unwindset does not match any loop"
+                        << messaget::eom;
+          return;
         }
         else
           id = function_id + "." + std::to_string(*nr);
@@ -147,15 +156,17 @@ void unwindsett::parse_unwindset_one_loop(std::string val)
   }
 }
 
-void unwindsett::parse_unwindset(const std::list<std::string> &unwindset)
+void unwindsett::parse_unwindset(
+  const std::list<std::string> &unwindset,
+  message_handlert &message_handler)
 {
   for(auto &element : unwindset)
   {
     std::vector<std::string> unwindset_elements =
       split_string(element, ',', true, true);
 
     for(auto &element : unwindset_elements)
-      parse_unwindset_one_loop(element);
+      parse_unwindset_one_loop(element, message_handler);
   }
 }
 
@@ -181,7 +192,9 @@ unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
   return global_limit;
 }
 
-void unwindsett::parse_unwindset_file(const std::string &file_name)
+void unwindsett::parse_unwindset_file(
+  const std::string &file_name,
+  message_handlert &message_handler)
 {
   #ifdef _MSC_VER
   std::ifstream file(widen(file_name));
@@ -199,5 +212,5 @@ void unwindsett::parse_unwindset_file(const std::string &file_name)
     split_string(buffer.str(), ',', true, true);
 
   for(auto &element : unwindset_elements)
-    parse_unwindset_one_loop(element);
+    parse_unwindset_one_loop(element, message_handler);
 }

src/goto-instrument/unwindset.h

@@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <map>
 #include <string>
 
+class message_handlert;
+
 class unwindsett
 {
 public:
@@ -34,13 +36,17 @@ class unwindsett
   void parse_unwind(const std::string &unwind);
 
   // limit for instances of a loop
-  void parse_unwindset(const std::list<std::string> &unwindset);
+  void parse_unwindset(
+    const std::list<std::string> &unwindset,
+    message_handlert &message_handler);
 
   // queries
   optionalt<unsigned> get_limit(const irep_idt &loop, unsigned thread_id) const;
 
   // read unwindset directives from a file
-  void parse_unwindset_file(const std::string &file_name);
+  void parse_unwindset_file(
+    const std::string &file_name,
+    message_handlert &message_handler);
 
 protected:
   abstract_goto_modelt &goto_model;
@@ -57,7 +63,9 @@ class unwindsett
     std::map<std::pair<irep_idt, unsigned>, optionalt<unsigned>>;
   thread_loop_mapt thread_loop_map;
 
-  void parse_unwindset_one_loop(std::string loop_limit);
+  void parse_unwindset_one_loop(
+    std::string loop_limit,
+    message_handlert &message_handler);
 };
 
 #define OPT_UNWINDSET                                                          \