Merge pull request #5637 from jezhiggins/flow-insensitivity-option

VSD flow insensitivity option

Author: martin-cs

regression/goto-analyzer/flow-insensitive-function-call-recursive/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int fun(int other)
+{
+  if(other > 0)
+  {
+    int value = fun(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int main(int argc, char *argv[])
+{
+  int z = fun(0);
+  assert(
+    z ==
+    0); // Unknown as flow-insensitive fails to stop the recursive case being explored
+}

regression/goto-analyzer/flow-insensitive-function-call-recursive/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-flow-insensitive --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion z == 0: UNKNOWN$
+--
+^warning: ignoring

regression/goto-analyzer/flow-insensitive-if/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int y = 1;
+  int z;
+  if(y)
+  {
+    assert(y != 0);
+    z = 1;
+  }
+  else
+  {
+    assert(y == 0);
+    z = 0;
+  }
+  assert(z == 1);
+}

regression/goto-analyzer/flow-insensitive-if/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-flow-insensitive --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion y != 0: SUCCESS$
+^\[main\.assertion\.2\] .* assertion y == 0: FAILURE \(if reachable\)$
+^\[main\.assertion\.3\] .* assertion z == 1: UNKNOWN$
+--
+^warning: ignoring

regression/goto-analyzer/flow-sensitive-function-call-recursive/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+int fun(int other)
+{
+  if(other > 0)
+  {
+    int value = fun(other - 1);
+    return value + 1;
+  }
+  else
+  {
+    return 0;
+  }
+}
+
+int main(int argc, char *argv[])
+{
+  int z = fun(0);
+  assert(z == 0); // Success because flow-sensitivity blocks the branch
+}

regression/goto-analyzer/flow-sensitive-function-call-recursive/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion z == 0: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/flow-sensitive-if/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  int y = 1;
+  int z;
+  if(y)
+  {
+    assert(y != 0);
+    z = 1;
+  }
+  else
+  {
+    assert(y == 0);
+    z = 0;
+  }
+  assert(z == 1);
+}

regression/goto-analyzer/flow-sensitive-if/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion y != 0: SUCCESS$
+^\[main\.assertion\.2\] .* assertion y == 0: SUCCESS \(unreachable\)$
+^\[main\.assertion\.3\] .* assertion z == 1: SUCCESS$
+--
+^warning: ignoring

src/analyses/Makefile

@@ -60,6 +60,7 @@ SRC = ai.cpp \
       variable-sensitivity/value_set_pointer_abstract_object.cpp \
       variable-sensitivity/value_set_array_abstract_object.cpp \
       variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
+      variable-sensitivity/variable_sensitivity_configuration.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp

@@ -0,0 +1,146 @@
+/*******************************************************************\
+
+ Module: variable sensitivity domain configuration
+
+ Author: Jez Higgins
+
+\*******************************************************************/
+/// \file
+/// Captures the user-supplied configuration for VSD, determining which
+/// domain abstractions are used, flow sensitivity, etc
+#include "variable_sensitivity_configuration.h"
+
+vsd_configt vsd_configt::from_options(const optionst &options)
+{
+  vsd_configt config{};
+
+  if(
+    options.get_bool_option("value-set") &&
+    options.get_bool_option("data-dependencies"))
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "Value set is not currently supported with data dependency analysis",
+      "--value-set --data-dependencies",
+      "--data-dependencies"};
+  }
+
+  config.value_abstract_type =
+    option_to_abstract_type(options, "values", value_option_mappings, CONSTANT);
+
+  config.pointer_abstract_type = option_to_abstract_type(
+    options, "pointers", pointer_option_mappings, POINTER_INSENSITIVE);
+
+  config.struct_abstract_type = option_to_abstract_type(
+    options, "structs", struct_option_mappings, STRUCT_INSENSITIVE);
+
+  config.array_abstract_type = option_to_abstract_type(
+    options, "arrays", array_option_mappings, ARRAY_INSENSITIVE);
+
+  config.union_abstract_type = option_to_abstract_type(
+    options, "unions", union_option_mappings, UNION_INSENSITIVE);
+
+  // This should always be on (for efficeny with 3-way merge)
+  // Does not work with value set
+  config.context_tracking.last_write_context =
+    (config.value_abstract_type != VALUE_SET) &&
+    (config.pointer_abstract_type != VALUE_SET);
+  config.context_tracking.data_dependency_context =
+    options.get_bool_option("data-dependencies");
+  config.advanced_sensitivities.new_value_set =
+    options.get_bool_option("new-value-set");
+
+  config.flow_sensitivity = (options.get_bool_option("flow-insensitive"))
+                              ? flow_sensitivityt::insensitive
+                              : flow_sensitivityt::sensitive;
+
+  return config;
+}
+
+vsd_configt vsd_configt::constant_domain()
+{
+  vsd_configt config{};
+  config.context_tracking.last_write_context = true;
+  config.value_abstract_type = CONSTANT;
+  config.pointer_abstract_type = POINTER_SENSITIVE;
+  config.struct_abstract_type = STRUCT_SENSITIVE;
+  config.array_abstract_type = ARRAY_SENSITIVE;
+  return config;
+}
+
+vsd_configt vsd_configt::value_set()
+{
+  vsd_configt config{};
+  config.value_abstract_type = VALUE_SET;
+  config.pointer_abstract_type = VALUE_SET;
+  config.struct_abstract_type = STRUCT_SENSITIVE;
+  config.array_abstract_type = ARRAY_SENSITIVE;
+  return config;
+}
+
+vsd_configt vsd_configt::intervals()
+{
+  vsd_configt config{};
+  config.context_tracking.last_write_context = true;
+  config.value_abstract_type = INTERVAL;
+  config.pointer_abstract_type = POINTER_SENSITIVE;
+  config.struct_abstract_type = STRUCT_SENSITIVE;
+  config.array_abstract_type = ARRAY_SENSITIVE;
+  return config;
+}
+
+const vsd_configt::option_mappingt vsd_configt::value_option_mappings = {
+  {"intervals", INTERVAL},
+  {"constants", CONSTANT},
+  {"set-of-constants", VALUE_SET}};
+
+const vsd_configt::option_mappingt vsd_configt::pointer_option_mappings = {
+  {"top-bottom", POINTER_INSENSITIVE},
+  {"constants", POINTER_SENSITIVE},
+  {"value-set", VALUE_SET}};
+
+const vsd_configt::option_mappingt vsd_configt::struct_option_mappings = {
+  {"top-bottom", STRUCT_INSENSITIVE},
+  {"every-field", STRUCT_SENSITIVE}};
+
+const vsd_configt::option_mappingt vsd_configt::array_option_mappings = {
+  {"top-bottom", ARRAY_INSENSITIVE},
+  {"every-element", ARRAY_SENSITIVE}};
+
+const vsd_configt::option_mappingt vsd_configt::union_option_mappings = {
+  {"top-bottom", UNION_INSENSITIVE}};
+
+invalid_command_line_argument_exceptiont vsd_configt::invalid_argument(
+  const std::string &option_name,
+  const std::string &bad_argument,
+  const option_mappingt &mapping)
+{
+  auto option = "--vsd-" + option_name;
+  auto choices = std::string("");
+  for(auto &kv : mapping)
+  {
+    choices += (!choices.empty() ? "|" : "");
+    choices += kv.first;
+  }
+
+  return invalid_command_line_argument_exceptiont{
+    "Unknown argument '" + bad_argument + "'", option, option + " " + choices};
+}
+
+ABSTRACT_OBJECT_TYPET vsd_configt::option_to_abstract_type(
+  const optionst &options,
+  const std::string &option_name,
+  const option_mappingt &mapping,
+  ABSTRACT_OBJECT_TYPET default_type)
+{
+  const auto argument = options.get_option(option_name);
+
+  if(argument.empty())
+    return default_type;
+
+  auto selected = mapping.find(argument);
+  if(selected == mapping.end())
+  {
+    throw invalid_argument(option_name, argument, mapping);
+  }
+  return selected->second;
+}