Merge pull request #5186 from diffblue/multi-unwindset

multiple --unwindset options

Author: Daniel Kroening

doc/cprover-manual/cbmc-unwinding.md

@@ -90,13 +90,14 @@ first use:
 to obtain a list of all loops in the program. Then identify the loops
 you need to set a separate bound for, and note their loop ID. Then use:
 
-    --unwindset L:B,L:B,...
+    --unwindset L:B
 
-where `L` denotes a loop ID and `B` denotes the bound for that loop.
+where `L` denotes a loop ID and `B` denotes the bound for that loop. The
+option can be given multiple times.
 
 As an example, consider a program with two loops in the function main:
 
-    --unwindset c::main.0:10,c::main.1:20
+    --unwindset main.0:10 --unwindset main.1:20
 
 This sets a bound of 10 for the first loop, and a bound of 20 for the
 second loop.

src/cbmc/cbmc_parse_options.cpp

@@ -287,7 +287,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   if(cmdline.isset("unwindset"))
-    options.set_option("unwindset", cmdline.get_value("unwindset"));
+    options.set_option("unwindset", cmdline.get_values("unwindset"));
 
   // constant propagation
   if(cmdline.isset("no-propagation"))

src/goto-checker/bmc_util.cpp

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

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -175,7 +175,7 @@ int goto_instrument_parse_optionst::doit()
           unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
 
         if(unwindset_given)
-          unwindset.parse_unwindset(cmdline.get_value("unwindset"));
+          unwindset.parse_unwindset(cmdline.get_values("unwindset"));
 
         bool unwinding_assertions=cmdline.isset("unwinding-assertions");
         bool partial_loops=cmdline.isset("partial-loops");

src/goto-instrument/unwindset.cpp

@@ -21,43 +21,52 @@ void unwindsett::parse_unwind(const std::string &unwind)
     global_limit = unsafe_string2unsigned(unwind);
 }
 
-void unwindsett::parse_unwindset(const std::string &unwindset)
+void unwindsett::parse_unwindset_one_loop(std::string val)
 {
-  std::vector<std::string> unwindset_loops =
-    split_string(unwindset, ',', true, true);
+  unsigned thread_nr = 0;
+  bool thread_nr_set = false;
 
-  for(auto &val : unwindset_loops)
+  if(!val.empty() && isdigit(val[0]) && val.find(":") != std::string::npos)
   {
-    unsigned thread_nr = 0;
-    bool thread_nr_set = false;
-
-    if(!val.empty() && isdigit(val[0]) && val.find(":") != std::string::npos)
-    {
-      std::string nr = val.substr(0, val.find(":"));
-      thread_nr = unsafe_string2unsigned(nr);
-      thread_nr_set = true;
-      val.erase(0, nr.size() + 1);
-    }
-
-    if(val.rfind(":") != std::string::npos)
-    {
-      std::string id = val.substr(0, val.rfind(":"));
-      std::string uw_string = val.substr(val.rfind(":") + 1);
-
-      // the below initialisation makes g++-5 happy
-      optionalt<unsigned> uw(0);
-
-      if(uw_string.empty())
-        uw = { };
-      else
-        uw = unsafe_string2unsigned(uw_string);
-
-      if(thread_nr_set)
-        thread_loop_map[std::pair<irep_idt, unsigned>(id, thread_nr)] = uw;
-      else
-        loop_map[id] = uw;
-    }
+    std::string nr = val.substr(0, val.find(":"));
+    thread_nr = unsafe_string2unsigned(nr);
+    thread_nr_set = true;
+    val.erase(0, nr.size() + 1);
   }
+
+  if(val.rfind(":") != std::string::npos)
+  {
+    std::string id = val.substr(0, val.rfind(":"));
+    std::string uw_string = val.substr(val.rfind(":") + 1);
+
+    // the below initialisation makes g++-5 happy
+    optionalt<unsigned> uw(0);
+
+    if(uw_string.empty())
+      uw = {};
+    else
+      uw = unsafe_string2unsigned(uw_string);
+
+    if(thread_nr_set)
+      thread_loop_map[std::pair<irep_idt, unsigned>(id, thread_nr)] = uw;
+    else
+      loop_map[id] = uw;
+  }
+}
+
+void unwindsett::parse_unwindset(const std::string &unwindset)
+{
+  std::vector<std::string> unwindset_elements =
+    split_string(unwindset, ',', true, true);
+
+  for(auto &element : unwindset_elements)
+    parse_unwindset_one_loop(element);
+}
+
+void unwindsett::parse_unwindset(const std::list<std::string> &unwindset)
+{
+  for(auto &element : unwindset)
+    parse_unwindset(element);
 }
 
 optionalt<unsigned>

src/goto-instrument/unwindset.h

@@ -12,9 +12,11 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
 #define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
 
+#include <list>
 #include <map>
 #include <string>
 
+#include <util/deprecate.h>
 #include <util/irep.h>
 #include <util/optional.h>
 
@@ -31,8 +33,12 @@ class unwindsett
   void parse_unwind(const std::string &unwind);
 
   // limit for instances of a loop
+  DEPRECATED(SINCE(2019, 11, 15, "use parse_unwindset(list) instead"))
   void parse_unwindset(const std::string &unwindset);
 
+  // limit for instances of a loop
+  void parse_unwindset(const std::list<std::string> &unwindset);
+
   // queries
   optionalt<unsigned> get_limit(const irep_idt &loop, unsigned thread_id) const;
 
@@ -51,6 +57,8 @@ class unwindsett
   using thread_loop_mapt =
     std::map<std::pair<irep_idt, unsigned>, optionalt<unsigned>>;
   thread_loop_mapt thread_loop_map;
+
+  void parse_unwindset_one_loop(std::string loop_limit);
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H