use unwindsett in goto-instrument

Author: 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/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();

src/goto-instrument/unwind.cpp

@@ -22,40 +22,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "loop_utils.h"
 
-void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
-{
-  assert(unwind_set.empty());
-
-  std::vector<std::string> result;
-  split_string(us, ',', result, true, true);
-  assert(!result.empty());
-
-  if(result.front().empty()) // allow empty string as unwindset
-    return;
-
-  for(std::vector<std::string>::const_iterator it=result.begin();
-      it!=result.end(); it++)
-  {
-    std::string loop;
-    std::string bound;
-
-    split_string(*it, ':', loop, bound, true);
-
-    std::string func;
-    std::string id;
-
-    split_string(loop, '.', func, id, true);
-
-    unsigned loop_id=std::stoi(id);
-    int loop_bound=std::stoi(bound);
-
-    if(loop_bound<-1)
-      throw "given unwind bound < -1";
-
-    unwind_set[func][loop_id]=loop_bound;
-  }
-}
-
 void goto_unwindt::copy_segment(
   const goto_programt::const_targett start,
   const goto_programt::const_targett end, // exclusive
@@ -290,37 +256,11 @@ void goto_unwindt::unwind(
   goto_program.destructive_insert(loop_exit, copies);
 }
 
-int goto_unwindt::get_k(
-  const irep_idt func,
-  const unsigned loop_id,
-  const int global_k,
-  const unwind_sett &unwind_set) const
-{
-  assert(global_k>=-1);
-
-  unwind_sett::const_iterator f_it=unwind_set.find(func);
-  if(f_it==unwind_set.end())
-    return global_k;
-
-  const std::map<unsigned, int> &m=f_it->second;
-  std::map<unsigned, int>::const_iterator l_it=m.find(loop_id);
-  if(l_it==m.end())
-    return global_k;
-
-  int k=l_it->second;
-  assert(k>=-1);
-
-  return k;
-}
-
 void goto_unwindt::unwind(
   goto_programt &goto_program,
-  const unwind_sett &unwind_set,
-  const int k,
+  const unwindsett &unwindset,
   const unwind_strategyt unwind_strategy)
 {
-  assert(k>=-1);
-
   for(goto_programt::const_targett i_it=goto_program.instructions.begin();
       i_it!=goto_program.instructions.end();)
   {
@@ -340,12 +280,14 @@ void goto_unwindt::unwind(
     const irep_idt func=i_it->function;
     assert(!func.empty());
 
-    unsigned loop_number=i_it->loop_number;
+    const irep_idt loop_id=
+      id2string(func) + "." + std::to_string(i_it->loop_number);
 
-    int final_k=get_k(func, loop_number, k, unwind_set);
+    auto limit=unwindset.get_limit(loop_id, 0);
 
-    if(final_k==-1)
+    if(!limit.has_value())
     {
+      // no unwinding given
       i_it++;
       continue;
     }
@@ -355,7 +297,7 @@ void goto_unwindt::unwind(
     loop_exit++;
     assert(loop_exit!=goto_program.instructions.end());
 
-    unwind(goto_program, loop_head, loop_exit, final_k, unwind_strategy);
+    unwind(goto_program, loop_head, loop_exit, *limit, unwind_strategy);
 
     // necessary as we change the goto program in the previous line
     i_it=loop_exit;
@@ -364,12 +306,9 @@ void goto_unwindt::unwind(
 
 void goto_unwindt::operator()(
   goto_functionst &goto_functions,
-  const unwind_sett &unwind_set,
-  const int k,
+  const unwindsett &unwindset,
   const unwind_strategyt unwind_strategy)
 {
-  assert(k>=-1);
-
   Forall_goto_functions(it, goto_functions)
   {
     goto_functionst::goto_functiont &goto_function=it->second;
@@ -383,7 +322,7 @@ void goto_unwindt::operator()(
 
     goto_programt &goto_program=goto_function.body;
 
-    unwind(goto_program, unwind_set, k, unwind_strategy);
+    unwind(goto_program, unwindset, unwind_strategy);
   }
 }
 

src/goto-instrument/unwind.h

@@ -13,17 +13,14 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_INSTRUMENT_UNWIND_H
 #define CPROVER_GOTO_INSTRUMENT_UNWIND_H
 
+#include "unwindset.h"
+
 #include <util/json.h>
 #include <util/json_expr.h>
 #include <goto-programs/goto_model.h>
 
 class goto_modelt;
 
-// -1: do not unwind loop
-typedef std::map<irep_idt, std::map<unsigned, int>> unwind_sett;
-
-void parse_unwindset(const std::string &us, unwind_sett &unwind_set);
-
 class goto_unwindt
 {
 public:
@@ -50,44 +47,22 @@ class goto_unwindt
 
   void unwind(
     goto_programt &goto_program,
-    const unwind_sett &unwind_set,
-    const int k=-1, // -1: no global bound
+    const unwindsett &unwindset,
     const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL);
 
   // unwind all functions
-
-  void operator()(
-    goto_functionst &goto_functions,
-    const unsigned k, // global bound
-    const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
-  {
-    const unwind_sett unwind_set;
-    operator()(goto_functions, unwind_set, k, unwind_strategy);
-  }
-
   void operator()(
     goto_functionst &,
-    const unwind_sett &unwind_set,
-    const int k=-1, // -1: no global bound
+    const unwindsett &unwindset,
     const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL);
 
   void operator()(
     goto_modelt &goto_model,
-    const unsigned k, // global bound
-    const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
-  {
-    const unwind_sett unwind_set;
-    operator()(goto_model.goto_functions, unwind_set, k, unwind_strategy);
-  }
-
-  void operator()(
-    goto_modelt &goto_model,
-    const unwind_sett &unwind_set,
-    const int k=-1, // -1: no global bound
+    const unwindsett &unwindset,
     const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
   {
     operator()(
-      goto_model.goto_functions, unwind_set, k, unwind_strategy);
+      goto_model.goto_functions, unwindset, unwind_strategy);
   }
 
   // unwind log
@@ -132,8 +107,7 @@ class goto_unwindt
   int get_k(
     const irep_idt func,
     const unsigned loop_id,
-    const int global_k,
-    const unwind_sett &unwind_set) const;
+    const unwindsett &unwindset) const;
 
   // copy goto program segment and redirect internal edges
   void copy_segment(

src/goto-instrument/unwindset.cpp

@@ -10,6 +10,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/string2int.h>
 #include <util/string_utils.h>
+#include <util/unicode.h>
+
+#include <fstream>
+#include <sstream>
 
 void unwindsett::parse_unwind(const std::string &unwind)
 {
@@ -77,3 +81,19 @@ unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
   // global, if any
   return global_limit;
 }
+
+void unwindsett::parse_unwindset_file(const std::string &file_name)
+{
+  #ifdef _MSC_VER
+  std::ifstream file(widen(file_name));
+  #else
+  std::ifstream file(file_name);
+  #endif
+
+  if(!file)
+    throw "cannot open file "+file_name;
+
+  std::stringstream buffer;
+  buffer << file.rdbuf();
+  parse_unwindset(buffer.str());
+}

src/goto-instrument/unwindset.h

@@ -36,6 +36,9 @@ class unwindsett
   // queries
   optionalt<unsigned> get_limit(const irep_idt &loop, unsigned thread_id) const;
 
+  // read unwindset directives from a file
+  void parse_unwindset_file(const std::string &file_name);
+
 protected:
   optionalt<unsigned> global_limit;