Add three new history options that use local_control_flow_historyt

These allow the user to track just forwards, just backwards or both
kinds of jump.  This gives per-path analysis (up to the limit of number
of times visiting each location), loop unwinding or both.

Author: martin

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -48,6 +48,7 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/goto_check.h>
 #include <analyses/interval_domain.h>
 #include <analyses/is_threaded.h>
+#include <analyses/local_control_flow_history.h>
 #include <analyses/local_may_alias.h>
 
 #include <langapi/mode.h>
@@ -295,6 +296,34 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
         "call-stack-recursion-limit", cmdline.get_value("call-stack"));
       options.set_option("history set", true);
     }
+    else if(cmdline.isset("loop-unwind"))
+    {
+      options.set_option("local-control-flow-history", true);
+      options.set_option("local-control-flow-history-forward", false);
+      options.set_option("local-control-flow-history-backward", true);
+      options.set_option(
+        "local-control-flow-history-limit", cmdline.get_value("loop-unwind"));
+      options.set_option("history set", true);
+    }
+    else if(cmdline.isset("branching"))
+    {
+      options.set_option("local-control-flow-history", true);
+      options.set_option("local-control-flow-history-forward", true);
+      options.set_option("local-control-flow-history-backward", false);
+      options.set_option(
+        "local-control-flow-history-limit", cmdline.get_value("branching"));
+      options.set_option("history set", true);
+    }
+    else if(cmdline.isset("loop-unwind-and-branching"))
+    {
+      options.set_option("local-control-flow-history", true);
+      options.set_option("local-control-flow-history-forward", true);
+      options.set_option("local-control-flow-history-backward", true);
+      options.set_option(
+        "local-control-flow-history-limit",
+        cmdline.get_value("loop-unwind-and-branching"));
+      options.set_option("history set", true);
+    }
 
     if(!options.get_bool_option("history set"))
     {
@@ -400,6 +429,13 @@ ai_baset *goto_analyzer_parse_optionst::build_analyzer(
       hf = util_make_unique<call_stack_history_factoryt>(
         options.get_unsigned_int_option("call-stack-recursion-limit"));
     }
+    else if(options.get_bool_option("local-control-flow-history"))
+    {
+      hf = util_make_unique<local_control_flow_history_factoryt>(
+        options.get_bool_option("local-control-flow-history-forward"),
+        options.get_bool_option("local-control-flow-history-backward"),
+        options.get_unsigned_int_option("local-control-flow-history-limit"));
+    }
 
     // Build the domain factory
     std::unique_ptr<ai_domain_factory_baset> df = nullptr;
@@ -855,6 +891,18 @@ void goto_analyzer_parse_optionst::help()
     " --call-stack n               track the calling location stack for each function\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     "                              limiting to at most n recursive loops, 0 to disable\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --loop-unwind n              track the number of loop iterations within a function\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "                              limited to n histories per location, 0 is unlimited\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --branching n                track the forwards jumps (if, switch, etc.) within a function\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "                              limited to n histories per location, 0 is unlimited\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --loop-unwind-and-branching n track all local control flow\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "                              limited to n histories per location, 0 is unlimited\n"
     "\n"
     "Domain options:\n"
     " --constants                  a constant for each variable if possible\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -120,7 +120,10 @@ class optionst;
 
 #define GOTO_ANALYSER_OPTIONS_HISTORY \
   "(ahistorical)" \
-  "(call-stack):"
+  "(call-stack):" \
+  "(loop-unwind):" \
+  "(branching):" \
+  "(loop-unwind-and-branching):"
 
 #define GOTO_ANALYSER_OPTIONS_DOMAIN \
   "(intervals)" \