Merge pull request #6510 from tautschnig/thread-unwind

Document and test thread-specific unwindset option

Author: tautschnig

doc/cprover-manual/cbmc-unwinding.md

@@ -90,10 +90,12 @@ 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 initial thread has index 0, and threads are
+consecutively numbered in program order of threads being spawned. The
+`--unwindset` 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,12 @@ 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. Thread numbers are set as follows: The
+initial thread has index 0, and threads are consecutively numbered in program
+order of threads being spawned.  The`--unwindset` option can be given multiple
+times.
 .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-checker/module_dependencies.txt

@@ -1,5 +1,6 @@
 cbmc # symex_bmc will be moved next
 goto-checker
+goto-instrument
 goto-programs
 goto-symex
 linking

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -108,7 +108,6 @@ Author: Daniel Kroening, [email protected]
 #include "thread_instrumentation.h"
 #include "undefined_functions.h"
 #include "unwind.h"
-#include "unwindset.h"
 #include "value_set_fi_fp_removal.h"
 
 /// invoke main modules
@@ -1726,7 +1725,6 @@ void goto_instrument_parse_optionst::help()
     HELP_DUMP_C
     "\n"
     "Diagnosis:\n"
-    " --show-loops                 show the loops in the program\n"
     HELP_SHOW_PROPERTIES
     " --show-symbol-table          show loaded symbol table\n"
     " --list-symbols               list symbols with type information\n"
@@ -1763,8 +1761,7 @@ void goto_instrument_parse_optionst::help()
     "\n"
     "Semantic transformations:\n"
     << HELP_NONDET_VOLATILE <<
-    " --unwind <n>                 unwinds the loops <n> times\n"
-    " --unwindset L:B,...          unwind loop L with a bound of B\n"
+    HELP_UNWINDSET
     " --unwindset-file <file>      read unwindset from file\n"
     " --partial-loops              permit paths with partial loops\n"
     " --unwinding-assertions       generate unwinding assertions\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -41,6 +41,7 @@ Author: Daniel Kroening, [email protected]
 #include "nondet_volatile.h"
 #include "replace_calls.h"
 #include "uninitialized.h"
+#include "unwindset.h"
 #include "wmm/weak_memory.h"
 
 // clang-format off
@@ -54,7 +55,8 @@ Author: Daniel Kroening, [email protected]
   OPT_UNINITIALIZED_CHECK \
   OPT_WMM \
   "(race-check)" \
-  "(unwind):(unwindset):(unwindset-file):" \
+  OPT_UNWINDSET \
+  "(unwindset-file):" \
   "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
   "(log):" \
   "(call-graph)(reachable-call-graph)" \
@@ -86,7 +88,7 @@ Author: Daniel Kroening, [email protected]
   OPT_TIMESTAMP \
   "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
   "(string-abstraction)" \
-  "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
+  "(verbosity):(version)(xml-ui)(json-ui)" \
   "(accelerate)(constant-propagator)" \
   "(k-induction):(step-case)(base-case)" \
   "(show-call-sequences)(check-call-sequence)" \

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