introduce unwindsett for unwinding limits

Author: kroening

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, kroening@kroening.com
 #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

@@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/source_location.h>
 #include <util/simplify_expr.h>
+#include <util/string_utils.h>
+#include <util/string2int.h>
 
 symex_bmct::symex_bmct(
   message_handlert &mh,
@@ -25,8 +27,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 +131,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 +174,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, kroening@kroening.com
 #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/unwindset.cpp

@@ -0,0 +1,78 @@
+/*******************************************************************\
+
+Module: Loop unwinding setup
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "unwindset.h"
+
+#include <util/string2int.h>
+#include <util/string_utils.h>
+
+void unwindsett::parse_unwind(const std::string &unwind)
+{
+  if(!unwind.empty())
+    global_limit = unsafe_string2unsigned(unwind);
+}
+
+void unwindsett::parse_unwindset(const std::string &unwindset)
+{
+  std::vector<std::string> unwindset_loops;
+  split_string(unwindset, ',', 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(":"));
+      std::string uw_string = val.substr(val.rfind(":") + 1);
+
+      optionalt<unsigned> uw;
+
+      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;
+    }
+  }
+}
+
+optionalt<unsigned>
+unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
+{
+  // We use the most specific limit we have
+
+  // thread x loop
+  auto tl_it =
+    thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
+
+  if(tl_it != thread_loop_map.end())
+    return tl_it->second;
+
+  // loop
+  auto l_it = loop_map.find(loop_id);
+
+  if(l_it != loop_map.end())
+    return l_it->second;
+
+  // global, if any
+  return global_limit;
+}

src/goto-instrument/unwindset.h

@@ -0,0 +1,53 @@
+/*******************************************************************\
+
+Module: Loop unwinding setup
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/// \file
+/// Loop unwinding
+
+#ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
+#define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
+
+#include <map>
+#include <string>
+
+#include <util/irep.h>
+#include <util/optional.h>
+
+class unwindsett
+{
+public:
+  // We have
+  // 1) a global limit
+  // 2) a limit per loop, all threads
+  // 3) a limit for a particular thread.
+  // We use the most specific of the above.
+
+  // global limit for all loops
+  void parse_unwind(const std::string &unwind);
+
+  // limit for instances of a loop
+  void parse_unwindset(const std::string &unwindset);
+
+  // queries
+  optionalt<unsigned> get_limit(const irep_idt &loop, unsigned thread_id) const;
+
+protected:
+  optionalt<unsigned> global_limit;
+
+  // Limit for all instances of a loop.
+  // This may have 'no value'.
+  typedef std::map<irep_idt, optionalt<unsigned>> loop_mapt;
+  loop_mapt loop_map;
+
+  // separate limits per thread
+  using thread_loop_mapt =
+    std::map<std::pair<irep_idt, unsigned>, optionalt<unsigned>>;
+  thread_loop_mapt thread_loop_map;
+};
+
+#endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H