Unwindset parsing: check loop identifiers

We silently accepted unwindset specifications that included non-existent
loop identifiers.

Author: tautschnig

regression/cbmc/unwindset1/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int x;
+for_loop:
+  for(int i = 0; i < x; ++i)
+    --x;
+  for(int j = 0; j < 5; ++j)
+    ++x;
+  __CPROVER_assert(0, "can be reached");
+}

regression/cbmc/unwindset1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--unwindset main.0:2,main.2:2
+^Invalid User Input$
+^Option: unwindset$
+^Reason: invalid loop identifier main\.2$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-checker/multi_path_symex_only_checker.cpp

@@ -28,13 +28,15 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     equation(ui_message_handler),
+    unwindset(goto_model),
     symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
       equation,
       options,
       path_storage,
-      guard_manager)
+      guard_manager,
+      unwindset)
 {
   setup_symex(symex, ns, options, ui_message_handler);
 }

src/goto-checker/multi_path_symex_only_checker.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include "symex_bmc.h"
 
 class multi_path_symex_only_checkert : public incremental_goto_checkert
@@ -35,6 +37,7 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert
   symex_target_equationt equation;
   guard_managert guard_manager;
   path_fifot path_storage; // should go away
+  unwindsett unwindset;
   symex_bmct symex;
 
   /// Generates the equation by running goto-symex

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -30,13 +30,15 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     equation(ui_message_handler),
+    unwindset(goto_model),
     symex(
       ui_message_handler,
       goto_model.get_symbol_table(),
       equation,
       options,
       path_storage,
       guard_manager,
+      unwindset,
       ui_message_handler.get_ui()),
     property_decider(options, ui_message_handler, equation, ns)
 {

src/goto-checker/single_loop_incremental_symex_checker.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include "goto_symex_property_decider.h"
 #include "goto_trace_provider.h"
 #include "incremental_goto_checker.h"
@@ -57,6 +59,7 @@ class single_loop_incremental_symex_checkert : public incremental_goto_checkert,
   symex_target_equationt equation;
   path_fifot path_storage; // should go away
   guard_managert guard_manager;
+  unwindsett unwindset;
   symex_bmc_incremental_one_loopt symex;
   bool initial_equation_generated = false;
   bool full_equation_generated = false;

src/goto-checker/single_path_symex_only_checker.cpp

@@ -30,7 +30,8 @@ single_path_symex_only_checkert::single_path_symex_only_checkert(
     goto_model(goto_model),
     ns(goto_model.get_symbol_table(), symex_symbol_table),
     worklist(get_path_strategy(options.get_option("exploration-strategy"))),
-    symex_runtime(0)
+    symex_runtime(0),
+    unwindset(goto_model)
 {
 }
 
@@ -70,7 +71,8 @@ void single_path_symex_only_checkert::initialize_worklist()
     equation,
     options,
     *worklist,
-    guard_manager);
+    guard_manager,
+    unwindset);
   setup_symex(symex);
 
   symex.initialize_path_storage_from_entry_point_of(
@@ -95,7 +97,8 @@ bool single_path_symex_only_checkert::resume_path(path_storaget::patht &path)
     path.equation,
     options,
     *worklist,
-    guard_manager);
+    guard_manager,
+    unwindset);
   setup_symex(symex);
 
   symex.resume_symex_from_saved_state(

src/goto-checker/single_path_symex_only_checker.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include <chrono>
 
 class symex_bmct;
@@ -40,6 +42,7 @@ class single_path_symex_only_checkert : public incremental_goto_checkert
   guard_managert guard_manager;
   std::unique_ptr<path_storaget> worklist;
   std::chrono::duration<double> symex_runtime;
+  unwindsett unwindset;
 
   void equation_output(
     const symex_bmct &symex,

src/goto-checker/symex_bmc.cpp

@@ -16,13 +16,16 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/source_location.h>
 
+#include <goto-instrument/unwindset.h>
+
 symex_bmct::symex_bmct(
   message_handlert &mh,
   const symbol_tablet &outer_symbol_table,
   symex_target_equationt &_target,
   const optionst &options,
   path_storaget &path_storage,
-  guard_managert &guard_manager)
+  guard_managert &guard_manager,
+  unwindsett &unwindset)
   : goto_symext(
       mh,
       outer_symbol_table,
@@ -33,6 +36,7 @@ symex_bmct::symex_bmct(
     record_coverage(!options.get_option("symex-coverage-report").empty()),
     havoc_bodyless_functions(
       options.get_bool_option("havoc-undefined-functions")),
+    unwindset(unwindset),
     symex_coverage(ns)
 {
 }

src/goto-checker/symex_bmc.h

@@ -16,10 +16,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-symex/goto_symex.h>
 
-#include <goto-instrument/unwindset.h>
-
 #include "symex_coverage.h"
 
+class unwindsett;
+
 class symex_bmct : public goto_symext
 {
 public:
@@ -29,7 +29,8 @@ class symex_bmct : public goto_symext
     symex_target_equationt &_target,
     const optionst &options,
     path_storaget &path_storage,
-    guard_managert &guard_manager);
+    guard_managert &guard_manager,
+    unwindsett &unwindset);
 
   // To show progress
   source_locationt last_source_location;
@@ -81,7 +82,7 @@ class symex_bmct : public goto_symext
   const bool record_coverage;
   const bool havoc_bodyless_functions;
 
-  unwindsett unwindset;
+  unwindsett &unwindset;
 
 protected:
   /// Callbacks that may provide an unwind/do-not-unwind decision for a loop

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -12,21 +12,25 @@ Author: Peter Schrammel, Daniel Kroening, [email protected]
 
 #include <util/structured_data.h>
 
+#include <goto-instrument/unwindset.h>
+
 symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
   message_handlert &message_handler,
   const symbol_tablet &outer_symbol_table,
   symex_target_equationt &target,
   const optionst &options,
   path_storaget &path_storage,
   guard_managert &guard_manager,
+  unwindsett &unwindset,
   ui_message_handlert::uit output_ui)
   : symex_bmct(
       message_handler,
       outer_symbol_table,
       target,
       options,
       path_storage,
-      guard_manager),
+      guard_manager,
+      unwindset),
     incr_loop_id(options.get_option("incremental-loop")),
     incr_max_unwind(
       options.is_set("unwind-max") ? options.get_signed_int_option("unwind-max")

src/goto-checker/symex_bmc_incremental_one_loop.h

@@ -22,6 +22,7 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
     const optionst &,
     path_storaget &,
     guard_managert &,
+    unwindsett &,
     ui_message_handlert::uit output_ui);
 
   /// Return true if symex can be resumed

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -166,7 +166,7 @@ int goto_instrument_parse_optionst::doit()
 
       if(unwind_given || unwindset_given || unwindset_file_given)
       {
-        unwindsett unwindset;
+        unwindsett unwindset{goto_model};
 
         if(unwind_given)
           unwindset.parse_unwind(cmdline.get_value("unwind"));

src/goto-instrument/unwindset.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "unwindset.h"
 
+#include <util/exception_utils.h>
 #include <util/string2int.h>
 #include <util/string_utils.h>
 
@@ -44,6 +45,65 @@ void unwindsett::parse_unwindset_one_loop(std::string val)
   if(last_c_pos != std::string::npos)
   {
     std::string id = val.substr(0, last_c_pos);
+
+    // The loop id can take three forms:
+    // 1) Just a function name to limit recursion.
+    // 2) F.N where F is a function name and N is a loop number.
+    const symbol_tablet &symbol_table = goto_model.get_symbol_table();
+    const symbolt *maybe_fn = symbol_table.lookup(id);
+    if(maybe_fn && maybe_fn->type.id() == ID_code)
+    {
+      // ok, recursion limit
+    }
+    else
+    {
+      auto last_dot_pos = val.rfind('.');
+      if(last_dot_pos == std::string::npos)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "invalid loop identifier " + id, "unwindset"};
+      }
+
+      std::string function_id = id.substr(0, last_dot_pos);
+      std::string loop_nr_label = id.substr(last_dot_pos + 1);
+
+      if(loop_nr_label.empty() || !goto_model.can_produce_function(function_id))
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "invalid loop identifier " + id, "unwindset"};
+      }
+
+      const goto_functiont &goto_function =
+        goto_model.get_goto_function(function_id);
+      if(isdigit(loop_nr_label[0]))
+      {
+        auto nr = string2optional_unsigned(loop_nr_label);
+        if(!nr.has_value())
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "invalid loop identifier " + id, "unwindset"};
+        }
+
+        bool found = std::any_of(
+          goto_function.body.instructions.begin(),
+          goto_function.body.instructions.end(),
+          [&nr](const goto_programt::instructiont &instruction) {
+            return instruction.is_backwards_goto() &&
+                   instruction.loop_number == nr;
+          });
+        if(!found)
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "invalid loop identifier " + id, "unwindset"};
+        }
+      }
+      else
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "invalid loop identifier " + id, "unwindset"};
+      }
+    }
+
     std::string uw_string = val.substr(last_c_pos + 1);
 
     // the below initialisation makes g++-5 happy

src/goto-instrument/unwindset.h

@@ -12,13 +12,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
 #define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
 
+#include <goto-programs/goto_model.h>
+
 #include <list>
 #include <map>
 #include <string>
 
-#include <util/irep.h>
-#include <util/optional.h>
-
 class unwindsett
 {
 public:
@@ -27,6 +26,9 @@ class unwindsett
   // 2) a limit per loop, all threads
   // 3) a limit for a particular thread.
   // We use the most specific of the above.
+  explicit unwindsett(abstract_goto_modelt &goto_model) : goto_model(goto_model)
+  {
+  }
 
   // global limit for all loops
   void parse_unwind(const std::string &unwind);
@@ -41,6 +43,8 @@ class unwindsett
   void parse_unwindset_file(const std::string &file_name);
 
 protected:
+  abstract_goto_modelt &goto_model;
+
   optionalt<unsigned> global_limit;
 
   // Limit for all instances of a loop.

unit/path_strategies.cpp

@@ -24,6 +24,8 @@ Author: Kareem Khazem <[email protected]>, 2018
 
 #include <goto-symex/path_storage.h>
 
+#include <goto-instrument/unwindset.h>
+
 #include <langapi/mode.h>
 
 #include <util/cmdline.h>
@@ -408,6 +410,7 @@ void _check_with_strategy(
   propertiest properties(initialize_properties(goto_model));
   std::unique_ptr<path_storaget> worklist = get_path_strategy(strategy);
   guard_managert guard_manager;
+  unwindsett unwindset{goto_model};
 
   {
     // Put initial state into the work list
@@ -418,7 +421,8 @@ void _check_with_strategy(
       equation,
       options,
       *worklist,
-      guard_manager);
+      guard_manager,
+      unwindset);
     setup_symex(symex, ns, options, ui_message_handler);
 
     symex.initialize_path_storage_from_entry_point_of(
@@ -438,7 +442,8 @@ void _check_with_strategy(
       resume.equation,
       options,
       *worklist,
-      guard_manager);
+      guard_manager,
+      unwindset);
     setup_symex(symex, ns, options, ui_message_handler);
 
     symex.resume_symex_from_saved_state(