Add --vsd-arrays up-to-n-elements option

jezhiggins · jezhiggins · commit 63203b16f50e · 2021-08-13T23:37:01.000+01:00
Default n is 10.
Additional --vsd-max-array-elements options gives finer control.
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/main.c b/regression/goto-analyzer/variable-sensitivity-array-access/main.c
@@ -0,0 +1,11 @@
+int main(void)
+{
+  int arr[] = {1, 2, 3, 4, 5};
+  arr[2] = 99;
+  int arr_0_after_write = arr[0];
+  int arr_1_after_write = arr[1];
+  int arr_2_after_write = arr[2];
+  int arr_3_after_write = arr[3];
+  int arr_4_after_write = arr[4];
+  return 0;
+}
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-every-element.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values constants --vsd-arrays every-element
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> 1
+main::1::arr_1_after_write \(\) -> 2
+main::1::arr_2_after_write \(\) -> 99
+main::1::arr_3_after_write \(\) -> 4
+main::1::arr_4_after_write \(\) -> 5
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-smash.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values constants --vsd-arrays smash
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> TOP
+main::1::arr_1_after_write \(\) -> TOP
+main::1::arr_2_after_write \(\) -> TOP
+main::1::arr_3_after_write \(\) -> TOP
+main::1::arr_4_after_write \(\) -> TOP
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-up-to-3-elements.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> 1
+main::1::arr_1_after_write \(\) -> 2
+main::1::arr_2_after_write \(\) -> TOP
+main::1::arr_3_after_write \(\) -> TOP
+main::1::arr_4_after_write \(\) -> TOP
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-every-element.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> \[1, 1\]
+main::1::arr_1_after_write \(\) -> \[2, 2\]
+main::1::arr_2_after_write \(\) -> \[63, 63\]
+main::1::arr_3_after_write \(\) -> \[4, 4\]
+main::1::arr_4_after_write \(\) -> \[5, 5\]
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-smash.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values intervals --vsd-arrays smash
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> \[1, 63\]
+main::1::arr_1_after_write \(\) -> \[1, 63\]
+main::1::arr_2_after_write \(\) -> \[1, 63\]
+main::1::arr_3_after_write \(\) -> \[1, 63\]
+main::1::arr_4_after_write \(\) -> \[1, 63\]
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-up-to-3-elements.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> \[1, 1\]
+main::1::arr_1_after_write \(\) -> \[2, 2\]
+main::1::arr_2_after_write \(\) -> \[3, 63\]
+main::1::arr_3_after_write \(\) -> \[3, 63\]
+main::1::arr_4_after_write \(\) -> \[3, 63\]
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-every-element.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 99 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 4 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 5 :value-set-end
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-smash.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end
diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-up-to-3-elements.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
diff --git a/regression/goto-analyzer/variable-sensitivity-array-constant-access/main.c b/regression/goto-analyzer/variable-sensitivity-array-constant-access/main.c
diff --git a/regression/goto-analyzer/variable-sensitivity-array-constant-access/test.desc b/regression/goto-analyzer/variable-sensitivity-array-constant-access/test.desc
diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/main.c b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/main.c
@@ -11,8 +11,8 @@ int main(void)
     ix = 2;
   }
 
-  // ix is between 0 and 4
-  // so this is between 1 and 5
+  // ix is between 0 and 2
+  // so this is between 1 and 3
   int arr_at_ix = arr[ix];
 
   int write_ix;
diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_at_ix \(\) -> TOP @ \[9\]
+main::1::arr_0_after_write \(\) -> TOP
+main::1::arr_1_after_write \(\) -> TOP
+main::1::arr_2_after_write \(\) -> TOP
+main::1::arr_3_after_write \(\) -> TOP
+main::1::arr_4_after_write \(\) -> TOP
diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\]
+main::1::arr_0_after_write \(\) -> \[1, 63\]
+main::1::arr_1_after_write \(\) -> \[2, 63\]
+main::1::arr_2_after_write \(\) -> \[3, 63\]
+main::1::arr_3_after_write \(\) -> \[3, 63\]
+main::1::arr_4_after_write \(\) -> \[3, 63\]
diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-up-to-3-elements.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3
+^EXIT=0$
+^SIGNAL=0$
+main::1::arr_at_ix \(\) -> value-set-begin: 1, 3, 4, 5 :value-set-end
+main::1::arr_0_after_write \(\) -> value-set-begin: 1, 99 :value-set-end
+main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end
+main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
+main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
+main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end
diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp
@@ -484,7 +484,7 @@ static eval_index_resultt eval_index(
   const namespacet &ns)
 {
   auto max_array_index = env.configuration().maximum_array_index;
-  bool overrun = (index > max_array_index);
+  bool overrun = (index >= max_array_index);
 
   return {true, overrun ? max_array_index : index, overrun};
 }
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp
@@ -47,8 +47,7 @@ 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);
+  config.maximum_array_index = configure_max_array_size(options);
 
   return config;
 }
@@ -105,12 +104,14 @@ 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},
+  {"up-to-n-elements", ARRAY_SENSITIVE},
   {"every-element", ARRAY_SENSITIVE}};
 
 const vsd_configt::option_size_mappingt
   vsd_configt::array_option_size_mappings = {
     {"top-bottom", 0},
     {"smash", 0},
+    {"up-to-n-elements", 10},
     {"every-element", std::numeric_limits<size_t>::max()}};
 
 const vsd_configt::option_mappingt vsd_configt::union_option_mappings = {
@@ -153,6 +154,17 @@ ABSTRACT_OBJECT_TYPET vsd_configt::option_to_abstract_type(
   return selected->second;
 }
 
+size_t vsd_configt::configure_max_array_size(const optionst &options)
+{
+  if(options.get_option("arrays") == "up-to-n-elements")
+  {
+    size_t max_elements = options.get_unsigned_int_option("array-max-elements");
+    if(max_elements != 0)
+      return max_elements - 1;
+  }
+  return option_to_size(options, "arrays", array_option_size_mappings);
+}
+
 size_t vsd_configt::option_to_size(
   const optionst &options,
   const std::string &option_name,
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h
@@ -87,6 +87,8 @@ struct vsd_configt
     const option_mappingt &mapping,
     ABSTRACT_OBJECT_TYPET default_type);
 
+  static size_t configure_max_array_size(const optionst &options);
+
   static size_t option_to_size(
     const optionst &options,
     const std::string &option_name,
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h
@@ -75,6 +75,7 @@
   "(vsd-values):"                                                              \
   "(vsd-structs):"                                                             \
   "(vsd-arrays):"                                                              \
+  "(vsd-array-max-elements):"                                                  \
   "(vsd-pointers):"                                                            \
   "(vsd-unions):"                                                              \
   "(vsd-flow-insensitive)"                                                     \
@@ -88,7 +89,9 @@
   " --vsd-structs                struct field sensitive analysis - "           \
   "top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */              \
   " --vsd-arrays                 array entry sensitive analysis - "            \
-  "top-bottom|smash|every-element\n" /* NOLINT(whitespace/line_length) */      \
+  "top-bottom|smash|up-to-n-elements|every-element\n" /* NOLINT(whitespace/line_length) */ \
+  " --vsd-array-max-elements     the n in --vsd-arrays up-to-n-elements - "    \
+  "defaults 10 if not given" /* 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"      \
@@ -102,6 +105,7 @@
   options.set_option("values", cmdline.get_value("vsd-values"));               \
   options.set_option("pointers", cmdline.get_value("vsd-pointers"));           \
   options.set_option("arrays", cmdline.get_value("vsd-arrays"));               \
+  options.set_option("array-max-elements", cmdline.get_value("vsd-array-max-elements")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("structs", cmdline.get_value("vsd-structs"));             \
   options.set_option("unions", cmdline.get_value("vsd-unions"));               \
   options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive")); /* NOLINT(whitespace/line_length) */ \
