Unwindset parsing: support labels as loop identifiers

Labels can enable a more stable loop identification when code bases are
subject to change.

Author: tautschnig

regression/cbmc/unwindset1/label.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwindset main.for_loop:2,main.1:6
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-instrument/unwindset.cpp

@@ -49,6 +49,7 @@ void unwindsett::parse_unwindset_one_loop(std::string val)
     // 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.
+    // 3) F.L where F is a function name and L is a label.
     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)
@@ -99,8 +100,33 @@ void unwindsett::parse_unwindset_one_loop(std::string val)
       }
       else
       {
-        throw invalid_command_line_argument_exceptiont{
-          "invalid loop identifier " + id, "unwindset"};
+        optionalt<unsigned> nr;
+        optionalt<source_locationt> location;
+        for(const auto &instruction : goto_function.body.instructions)
+        {
+          if(
+            std::find(
+              instruction.labels.begin(),
+              instruction.labels.end(),
+              loop_nr_label) != instruction.labels.end())
+          {
+            location = instruction.source_location();
+          }
+          if(
+            location.has_value() && instruction.is_backwards_goto() &&
+            instruction.source_location() == *location)
+          {
+            nr = instruction.loop_number;
+            break;
+          }
+        }
+        if(!nr.has_value())
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "loop identifier " + id + " does not match any loop", "unwindset"};
+        }
+        else
+          id = function_id + "." + std::to_string(*nr);
       }
     }