Merge pull request #2167 from diffblue/parse_unwindset_options

move setup_unwind to parse_unwindset_options to prevent duplication

Author: Daniel Kroening

regression/goto-instrument/unwind-unwindset3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind 10 --unwindset main.0:-1
+--unwind 10 --unwindset main.0:
 ^Unwinding loop
 ^EXIT=0$
 ^SIGNAL=0$

src/cbmc/Makefile

@@ -30,9 +30,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../pointer-analysis/add_failed_symbols$(OBJEXT) \
       ../pointer-analysis/rewrite_index$(OBJEXT) \
       ../pointer-analysis/goto_program_dereference$(OBJEXT) \
-      ../goto-instrument/reachability_slicer$(OBJEXT) \
-      ../goto-instrument/full_slicer$(OBJEXT) \
-      ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/cover$(OBJEXT) \
       ../goto-instrument/cover_basic_blocks$(OBJEXT) \
       ../goto-instrument/cover_filter$(OBJEXT) \
@@ -43,6 +40,10 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
       ../goto-instrument/cover_instrument_other$(OBJEXT) \
       ../goto-instrument/cover_util$(OBJEXT) \
+      ../goto-instrument/reachability_slicer$(OBJEXT) \
+      ../goto-instrument/nondet_static$(OBJEXT) \
+      ../goto-instrument/full_slicer$(OBJEXT) \
+      ../goto-instrument/unwindset$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \

src/cbmc/bmc.cpp

@@ -15,8 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 
 #include <util/exit_codes.h>
-#include <util/string2int.h>
-#include <util/string_utils.h>
 
 #include <langapi/language_util.h>
 
@@ -319,7 +317,8 @@ void bmct::setup()
 
   symex.last_source_location.make_nil();
 
-    setup_unwind();
+  symex.unwindset.parse_unwind(options.get_option("unwind"));
+  symex.unwindset.parse_unwindset(options.get_option("unwindset"));
 }
 
 safety_checkert::resultt bmct::execute(
@@ -549,43 +548,6 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
   }
 }
 
-void bmct::setup_unwind()
-{
-  const std::string &set=options.get_option("unwindset");
-  std::vector<std::string> unwindset_loops;
-  split_string(set, ',', unwindset_loops, true, true);
-
-  for(auto &val : unwindset_loops)
-  {
-    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(":"));
-      long uw=unsafe_string2int(val.substr(val.rfind(":")+1));
-
-      if(thread_nr_set)
-        symex.set_unwind_thread_loop_limit(thread_nr, id, uw);
-      else
-        symex.set_unwind_loop_limit(id, uw);
-    }
-  }
-
-  if(options.get_option("unwind")!="")
-    symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
-}
-
 /// Perform core BMC, using an abstract model to supply GOTO function bodies
 /// (perhaps created on demand).
 /// \param opts: command-line options affecting BMC

src/cbmc/bmc.h

@@ -183,8 +183,6 @@ class bmct:public safety_checkert
     const goto_functionst &,
     prop_convt &);
 
-  // unwinding
-  virtual void setup_unwind();
   void do_conversion();
 
   virtual void freeze_program_variables();

src/cbmc/symex_bmc.cpp

@@ -25,8 +25,6 @@ symex_bmct::symex_bmct(
   path_storaget &path_storage)
   : goto_symext(mh, outer_symbol_table, _target, path_storage),
     record_coverage(false),
-    max_unwind(0),
-    max_unwind_is_set(false),
     symex_coverage(ns)
 {
 }
@@ -131,25 +129,12 @@ bool symex_bmct::get_unwind(
   // / --unwind options to decide:
   if(abort_unwind_decision.is_unknown())
   {
-    // We use the most specific limit we have,
-    // and 'infinity' when we have none.
+    auto limit=unwindset.get_limit(id, source.thread_nr);
 
-    loop_limitst &this_thread_limits=
-      thread_loop_limits[source.thread_nr];
-
-    loop_limitst::const_iterator l_it=this_thread_limits.find(id);
-    if(l_it!=this_thread_limits.end())
-      this_loop_limit=l_it->second;
+    if(!limit.has_value())
+      abort_unwind_decision = tvt(false);
     else
-    {
-      l_it=loop_limits.find(id);
-      if(l_it!=loop_limits.end())
-        this_loop_limit=l_it->second;
-      else if(max_unwind_is_set)
-        this_loop_limit=max_unwind;
-    }
-
-    abort_unwind_decision = tvt(unwind >= this_loop_limit);
+      abort_unwind_decision = tvt(unwind >= *limit);
   }
 
   INVARIANT(
@@ -187,25 +172,12 @@ bool symex_bmct::get_unwind_recursion(
   // / --unwind options to decide:
   if(abort_unwind_decision.is_unknown())
   {
-    // We use the most specific limit we have,
-    // and 'infinity' when we have none.
-
-    loop_limitst &this_thread_limits=
-      thread_loop_limits[thread_nr];
+    auto limit=unwindset.get_limit(id, thread_nr);
 
-    loop_limitst::const_iterator l_it=this_thread_limits.find(id);
-    if(l_it!=this_thread_limits.end())
-      this_loop_limit=l_it->second;
+    if(!limit.has_value())
+      abort_unwind_decision = tvt(false);
     else
-    {
-      l_it=loop_limits.find(id);
-      if(l_it!=loop_limits.end())
-        this_loop_limit=l_it->second;
-      else if(max_unwind_is_set)
-        this_loop_limit=max_unwind;
-    }
-
-    abort_unwind_decision = tvt(unwind>this_loop_limit);
+      abort_unwind_decision = tvt(unwind > *limit);
   }
 
   INVARIANT(

src/cbmc/symex_bmc.h

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 #include <goto-symex/path_storage.h>
 #include <goto-symex/goto_symex.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include "symex_coverage.h"
 
 class symex_bmct: public goto_symext
@@ -32,29 +34,6 @@ class symex_bmct: public goto_symext
   // To show progress
   source_locationt last_source_location;
 
-  // Control unwinding.
-
-  void set_unwind_limit(unsigned limit)
-  {
-    max_unwind=limit;
-    max_unwind_is_set=true;
-  }
-
-  void set_unwind_thread_loop_limit(
-    unsigned thread_nr,
-    const irep_idt &id,
-    unsigned limit)
-  {
-    thread_loop_limits[thread_nr][id]=limit;
-  }
-
-  void set_unwind_loop_limit(
-    const irep_idt &id,
-    unsigned limit)
-  {
-    loop_limits[id]=limit;
-  }
-
   /// Loop unwind handlers take the function ID and loop number, the unwind
   /// count so far, and an out-parameter specifying an advisory maximum, which
   /// they may set. If set the advisory maximum is set it is *only* used to
@@ -101,26 +80,12 @@ class symex_bmct: public goto_symext
 
   bool record_coverage;
 
-protected:
-  // We have
-  // 1) a global limit (max_unwind)
-  // 2) a limit per loop, all threads
-  // 3) a limit for a particular thread.
-  // 4) zero or more handler functions that can special-case particular
-  //    functions or loops
-  // We use the most specific of the above.
-
-  unsigned max_unwind;
-  bool max_unwind_is_set;
-
-  typedef std::unordered_map<irep_idt, unsigned> loop_limitst;
-  loop_limitst loop_limits;
-
-  typedef std::map<unsigned, loop_limitst> thread_loop_limitst;
-  thread_loop_limitst thread_loop_limits;
+  unwindsett unwindset;
 
+protected:
   /// Callbacks that may provide an unwind/do-not-unwind decision for a loop
   std::vector<loop_unwind_handlert> loop_unwind_handlers;
+
   /// Callbacks that may provide an unwind/do-not-unwind decision for a
   /// recursive call
   std::vector<recursion_unwind_handlert> recursion_unwind_handlers;

src/goto-instrument/Makefile

@@ -61,6 +61,7 @@ SRC = accelerate/accelerate.cpp \
       undefined_functions.cpp \
       uninitialized.cpp \
       unwind.cpp \
+      unwindset.cpp \
       wmm/abstract_event.cpp \
       wmm/cycle_collection.cpp \
       wmm/data_dp.cpp \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -139,43 +139,26 @@ int goto_instrument_parse_optionst::doit()
     instrument_goto_program();
 
     {
-      bool unwind=cmdline.isset("unwind");
-      bool unwindset=cmdline.isset("unwindset");
-      bool unwindset_file=cmdline.isset("unwindset-file");
+      bool unwind_given=cmdline.isset("unwind");
+      bool unwindset_given=cmdline.isset("unwindset");
+      bool unwindset_file_given=cmdline.isset("unwindset-file");
 
-      if(unwindset && unwindset_file)
+      if(unwindset_given && unwindset_file_given)
         throw "only one of --unwindset and --unwindset-file supported at a "
               "time";
 
-      if(unwind || unwindset || unwindset_file)
+      if(unwind_given || unwindset_given || unwindset_file_given)
       {
-        int k=-1;
+        unwindsett unwindset;
 
-        if(unwind)
-          k=std::stoi(cmdline.get_value("unwind"));
+        if(unwind_given)
+          unwindset.parse_unwind(cmdline.get_value("unwind"));
 
-        unwind_sett unwind_set;
+        if(unwindset_file_given)
+          unwindset.parse_unwindset_file(cmdline.get_value("unwindset-file"));
 
-        if(unwindset_file)
-        {
-          std::string us;
-          std::string fn=cmdline.get_value("unwindset-file");
-
-#ifdef _MSC_VER
-          std::ifstream file(widen(fn));
-#else
-          std::ifstream file(fn);
-#endif
-          if(!file)
-            throw "cannot open file "+fn;
-
-          std::stringstream buffer;
-          buffer << file.rdbuf();
-          us=buffer.str();
-          parse_unwindset(us, unwind_set);
-        }
-        else if(unwindset)
-          parse_unwindset(cmdline.get_value("unwindset"), unwind_set);
+        if(unwindset_given)
+          unwindset.parse_unwindset(cmdline.get_value("unwindset"));
 
         bool unwinding_assertions=cmdline.isset("unwinding-assertions");
         bool partial_loops=cmdline.isset("partial-loops");
@@ -202,7 +185,7 @@ int goto_instrument_parse_optionst::doit()
         }
 
         goto_unwindt goto_unwind;
-        goto_unwind(goto_model, unwind_set, k, unwind_strategy);
+        goto_unwind(goto_model, unwindset, unwind_strategy);
 
         goto_model.goto_functions.update();
         goto_model.goto_functions.compute_loop_numbers();