Add --vsd-arrays smash option

The "smash" array abstraction sets the maximum size of the
full_array_abstract_object to 1. All writes to the array are merged, and
all reads return the same value.

Author: jezhiggins

…-array-nondet-access/test-constants.desc …access/test-constants-every-element.descregression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants.desc renamed to regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants.desc renamed to regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values constants --vsd-arrays smash
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_at_ix \(\) -> TOP @ \[9\]
+main::1::arr_0_after_write \(\) -> TOP @ \[18\]
+main::1::arr_1_after_write \(\) -> TOP @ \[20\]
+main::1::arr_2_after_write \(\) -> TOP @ \[22\]

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values intervals --vsd-arrays smash
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_at_ix \(\) -> \[1, 3\] @ \[9\]
+main::1::arr_0_after_write \(\) -> \[1, 4\] @ \[18\]
+main::1::arr_1_after_write \(\) -> \[1, 4\] @ \[20\]
+main::1::arr_2_after_write \(\) -> \[1, 4\] @ \[22\]

…-array-nondet-access/test-intervals.desc …access/test-intervals-every-element.descregression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals.desc renamed to regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals.desc renamed to regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_at_ix \(\) -> value-set-begin: 1, 2, 3 :value-set-end
+main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4 :value-set-end

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc

@@ -30,6 +30,10 @@ static eval_index_resultt eval_index(
   const exprt &expr,
   const abstract_environmentt &env,
   const namespacet &ns);
+static eval_index_resultt eval_index(
+  const mp_integer &index,
+  const abstract_environmentt &env,
+  const namespacet &ns);
 
 template <typename index_fn>
 abstract_object_pointert apply_to_index_range(
@@ -83,11 +87,12 @@ full_array_abstract_objectt::full_array_abstract_objectt(
 {
   if(expr.id() == ID_array)
   {
-    int index = 0;
+    mp_integer i = 0;
     for(const exprt &entry : expr.operands())
     {
-      map.insert(mp_integer(index), environment.eval(entry, ns));
-      ++index;
+      auto index = eval_index(i, environment, ns);
+      map_put(index.value, environment.eval(entry, ns), index.overrun);
+      ++i;
     }
     set_not_top();
   }
@@ -467,9 +472,19 @@ static eval_index_resultt eval_index(
 
   mp_integer out_index;
   bool result = to_integer(to_constant_expr(value), out_index);
+  if(result)
+    return {false};
+
+  return eval_index(out_index, env, ns);
+}
 
+static eval_index_resultt eval_index(
+  const mp_integer &index,
+  const abstract_environmentt &env,
+  const namespacet &ns)
+{
   auto max_array_index = env.configuration().maximum_array_index;
-  bool overrun = (out_index > max_array_index);
+  bool overrun = (index > max_array_index);
 
-  return {!result, overrun ? max_array_index : out_index, overrun};
+  return {true, overrun ? max_array_index : index, overrun};
 }

…array-nondet-access/test-value-sets.desc …ccess/test-value-sets-every-element.descregression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets.desc renamed to regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-every-element.desc regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets.desc renamed to regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-every-element.desc

@@ -10,6 +10,7 @@
 /// domain abstractions are used, flow sensitivity, etc
 #include "variable_sensitivity_configuration.h"
 
+#include <limits>
 #include <util/options.h>
 
 vsd_configt vsd_configt::from_options(const optionst &options)
@@ -41,6 +42,9 @@ vsd_configt vsd_configt::from_options(const optionst &options)
                               ? flow_sensitivityt::insensitive
                               : flow_sensitivityt::sensitive;
 
+  config.maximum_array_index =
+    option_to_size(options, "arrays", array_option_size_mappings);
+
   return config;
 }
 
@@ -52,6 +56,7 @@ vsd_configt vsd_configt::constant_domain()
   config.pointer_abstract_type = POINTER_SENSITIVE;
   config.struct_abstract_type = STRUCT_SENSITIVE;
   config.array_abstract_type = ARRAY_SENSITIVE;
+  config.maximum_array_index = std::numeric_limits<size_t>::max();
   return config;
 }
 
@@ -62,6 +67,7 @@ vsd_configt vsd_configt::value_set()
   config.pointer_abstract_type = VALUE_SET_OF_POINTERS;
   config.struct_abstract_type = STRUCT_SENSITIVE;
   config.array_abstract_type = ARRAY_SENSITIVE;
+  config.maximum_array_index = std::numeric_limits<size_t>::max();
   return config;
 }
 
@@ -73,6 +79,7 @@ vsd_configt vsd_configt::intervals()
   config.pointer_abstract_type = POINTER_SENSITIVE;
   config.struct_abstract_type = STRUCT_SENSITIVE;
   config.array_abstract_type = ARRAY_SENSITIVE;
+  config.maximum_array_index = std::numeric_limits<size_t>::max();
   return config;
 }
 
@@ -92,15 +99,23 @@ const vsd_configt::option_mappingt vsd_configt::struct_option_mappings = {
 
 const vsd_configt::option_mappingt vsd_configt::array_option_mappings = {
   {"top-bottom", ARRAY_INSENSITIVE},
+  {"smash", ARRAY_SENSITIVE},
   {"every-element", ARRAY_SENSITIVE}};
 
+const vsd_configt::option_size_mappingt
+  vsd_configt::array_option_size_mappings = {
+    {"top-bottom", 0},
+    {"smash", 0},
+    {"every-element", std::numeric_limits<size_t>::max()}};
+
 const vsd_configt::option_mappingt vsd_configt::union_option_mappings = {
   {"top-bottom", UNION_INSENSITIVE}};
 
-invalid_command_line_argument_exceptiont vsd_configt::invalid_argument(
+template <class mappingt>
+invalid_command_line_argument_exceptiont invalid_argument(
   const std::string &option_name,
   const std::string &bad_argument,
-  const option_mappingt &mapping)
+  const mappingt &mapping)
 {
   auto option = "--vsd-" + option_name;
   auto choices = std::string("");
@@ -132,3 +147,22 @@ ABSTRACT_OBJECT_TYPET vsd_configt::option_to_abstract_type(
   }
   return selected->second;
 }
+
+size_t vsd_configt::option_to_size(
+  const optionst &options,
+  const std::string &option_name,
+  const option_size_mappingt &mapping)
+{
+  const size_t def = std::numeric_limits<size_t>::max();
+  const auto argument = options.get_option(option_name);
+
+  if(argument.empty())
+    return def;
+
+  auto selected = mapping.find(argument);
+  if(selected == mapping.end())
+  {
+    throw invalid_argument(option_name, argument, mapping);
+  }
+  return selected->second;
+}

regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-smash.desc

@@ -11,7 +11,6 @@
 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_CONFIGURATION_H
 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_CONFIGURATION_H
 
-#include <limits>
 #include <map>
 
 #include <util/exception_utils.h>
@@ -52,7 +51,7 @@ struct vsd_configt
 
   flow_sensitivityt flow_sensitivity;
 
-  size_t maximum_array_index = std::numeric_limits<size_t>::max();
+  size_t maximum_array_index = 0;
 
   struct
   {
@@ -80,22 +79,24 @@ struct vsd_configt
 
 private:
   using option_mappingt = std::map<std::string, ABSTRACT_OBJECT_TYPET>;
+  using option_size_mappingt = std::map<std::string, size_t>;
 
   static ABSTRACT_OBJECT_TYPET option_to_abstract_type(
     const optionst &options,
     const std::string &option_name,
     const option_mappingt &mapping,
     ABSTRACT_OBJECT_TYPET default_type);
 
-  static invalid_command_line_argument_exceptiont invalid_argument(
+  static size_t option_to_size(
+    const optionst &options,
     const std::string &option_name,
-    const std::string &bad_argument,
-    const option_mappingt &mapping);
+    const option_size_mappingt &mapping);
 
   static const option_mappingt value_option_mappings;
   static const option_mappingt pointer_option_mappings;
   static const option_mappingt struct_option_mappings;
   static const option_mappingt array_option_mappings;
+  static const option_size_mappingt array_option_size_mappings;
   static const option_mappingt union_option_mappings;
 };
 

src/analyses/variable-sensitivity/full_array_abstract_object.cpp

@@ -88,7 +88,7 @@
   " --vsd-structs                struct field sensitive analysis - "           \
   "top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */              \
   " --vsd-arrays                 array entry sensitive analysis - "            \
-  "top-bottom|every-element\n" /* NOLINT(whitespace/line_length) */            \
+  "top-bottom|smash|every-element\n" /* NOLINT(whitespace/line_length) */      \
   " --vsd-pointers               pointer sensitive analysis - "                \
   "top-bottom|constants|value-set\n" /* NOLINT(whitespace/line_length) */      \
   " --vsd-unions                 union sensitive analysis - top-bottom\n"      \