Document and test thread-specific unwindset option

We had working support for thread-specific limits as of 7f7e3c4,
but seemingly never exposed this in documentation.

Also cleaned up the command-line parsing code to avoid repeated
find/rfind operations.

Author: tautschnig

doc/cprover-manual/cbmc-unwinding.md

@@ -90,10 +90,10 @@ 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
+    --unwindset [T:]L:B
 
-where `L` denotes a loop ID and `B` denotes the bound for that loop. The
-option can be given multiple times.
+where `L` denotes a loop ID and `B` denotes the bound for that loop in thread T,
+if a thread number is included. The option can be given multiple times.
 
 As an example, consider a program with two loops in the function main:
 

doc/man/cbmc.1

@@ -137,8 +137,9 @@ Only show program expression
 Limit search depth
 .IP "--unwind nr "
 Unwind loops nr times
-.IP "--unwindset L:B,..."
-Unwind loop L with a bound of B (use \-\-show\-loops to get the loop IDs)
+.IP "--unwindset [T:]L:B,..."
+Unwind loop L with a bound of B, optionally restricted to thread T (use
+\-\-show\-loops to get the loop IDs)
 .IP --show-vcc
 Show the verification conditions
 .IP --slice-formula

regression/cbmc-concurrency/loop_unwinding2/main.c

@@ -0,0 +1,18 @@
+void *thr1(void *arg)
+{
+  for(int i = 0; i < *(int *)arg; ++i)
+    ;
+
+  return 0;
+}
+
+int l1 = 1;
+int l2 = 2;
+
+int main()
+{
+__CPROVER_ASYNC_1:
+  thr1(&l1);
+__CPROVER_ASYNC_2:
+  thr1(&l2);
+}

regression/cbmc-concurrency/loop_unwinding2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwindset 1:thr1.0:2,2:thr1.0:3 --unwinding-assertions
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-checker/bmc_util.h

@@ -17,6 +17,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-symex/build_goto_trace.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include "incremental_goto_checker.h"
 #include "properties.h"
 
@@ -172,7 +174,6 @@ void run_property_decider(
 #define OPT_BMC \
   "(program-only)" \
   "(show-byte-ops)" \
-  "(show-loops)" \
   "(show-vcc)" \
   "(show-goto-symex-steps)" \
   "(show-points-to-sets)" \
@@ -185,18 +186,17 @@ void run_property_decider(
   "(paths):" \
   "(show-symex-strategies)" \
   "(depth):" \
-  "(unwind):" \
   "(max-field-sensitivity-array-size):" \
   "(no-array-field-sensitivity)" \
   "(graphml-witness):" \
-  "(unwindset):" \
   "(symex-complexity-limit):" \
   "(symex-complexity-failed-child-loops-limit):" \
   "(incremental-loop):" \
   "(unwind-min):" \
   "(unwind-max):" \
   "(ignore-properties-before-unwind-min)" \
   "(symex-cache-dereferences)" \
+  OPT_UNWINDSET \
 
 #define HELP_BMC \
   " --paths [strategy]           explore paths one at a time\n" \
@@ -207,7 +207,6 @@ void run_property_decider(
   "                              pointer dereference. Requires --json-ui.\n" \
   " --program-only               only show program expression\n" \
   " --show-byte-ops              show all byte extracts and updates\n" \
-  " --show-loops                 show the loops in the program\n" \
   " --depth nr                   limit search depth\n" \
   " --max-field-sensitivity-array-size M\n" \
   "                              maximum size M of arrays for which field\n" \
@@ -218,9 +217,7 @@ void run_property_decider(
   "this is\n" \
   "                              equivalent to setting the maximum field \n" \
   "                              sensitivity size for arrays to 0\n" \
-  " --unwind nr                  unwind nr times\n" \
-  " --unwindset L:B,...          unwind loop L with a bound of B\n" \
-  "                              (use --show-loops to get the loop IDs)\n" \
+  HELP_UNWINDSET \
   " --incremental-loop L         check properties after each unwinding\n" \
   "                              of loop L\n" \
   "                              (use --show-loops to get the loop IDs)\n" \

src/goto-instrument/unwindset.cpp

@@ -25,21 +25,26 @@ void unwindsett::parse_unwind(const std::string &unwind)
 
 void unwindsett::parse_unwindset_one_loop(std::string val)
 {
-  unsigned thread_nr = 0;
-  bool thread_nr_set = false;
+  if(val.empty())
+    return;
 
-  if(!val.empty() && isdigit(val[0]) && val.find(":") != std::string::npos)
+  optionalt<unsigned> thread_nr;
+  if(isdigit(val[0]))
   {
-    std::string nr = val.substr(0, val.find(":"));
-    thread_nr = unsafe_string2unsigned(nr);
-    thread_nr_set = true;
-    val.erase(0, nr.size() + 1);
+    auto c_pos = val.find(':');
+    if(c_pos != std::string::npos)
+    {
+      std::string nr = val.substr(0, c_pos);
+      thread_nr = unsafe_string2unsigned(nr);
+      val.erase(0, nr.size() + 1);
+    }
   }
 
-  if(val.rfind(":") != std::string::npos)
+  auto last_c_pos = val.rfind(':');
+  if(last_c_pos != std::string::npos)
   {
-    std::string id = val.substr(0, val.rfind(":"));
-    std::string uw_string = val.substr(val.rfind(":") + 1);
+    std::string id = val.substr(0, last_c_pos);
+    std::string uw_string = val.substr(last_c_pos + 1);
 
     // the below initialisation makes g++-5 happy
     optionalt<unsigned> uw(0);
@@ -49,8 +54,8 @@ void unwindsett::parse_unwindset_one_loop(std::string val)
     else
       uw = unsafe_string2unsigned(uw_string);
 
-    if(thread_nr_set)
-      thread_loop_map[std::pair<irep_idt, unsigned>(id, thread_nr)] = uw;
+    if(thread_nr.has_value())
+      thread_loop_map[std::pair<irep_idt, unsigned>(id, *thread_nr)] = uw;
     else
       loop_map[id] = uw;
   }

src/goto-instrument/unwindset.h

@@ -56,4 +56,16 @@ class unwindsett
   void parse_unwindset_one_loop(std::string loop_limit);
 };
 
+#define OPT_UNWINDSET                                                          \
+  "(show-loops)"                                                               \
+  "(unwind):"                                                                  \
+  "(unwindset):"
+
+#define HELP_UNWINDSET                                                         \
+  " --show-loops                 show the loops in the program\n"              \
+  " --unwind nr                  unwind nr times\n"                            \
+  " --unwindset [T:]L:B,...      unwind loop L with a bound of B\n"            \
+  "                              (optionally restricted to thread T)\n"        \
+  "                              (use --show-loops to get the loop IDs)\n"
+
 #endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H