Set a limit size for array cell propagation

The use of field_sensitivity for arrays can be expensive for big arrays
so we have to set a limit on the size of constant arrays which get
processed.
The value 64 was determined by changing the size of the array in the
test regression/cbmc/variable-access-to-constant-array and reducing it
until there was no significant difference in execution time between the
versions of CBMC with and without array cell propagation.
For the chosen value the execution time was around 0.05 second in both
cases (for comparison with size 1024 the time with propagation was 0.5
sec, against 0.1 without).

Author: romainbrenguier

src/goto-symex/field_sensitivity.cpp

@@ -97,14 +97,19 @@ exprt field_sensitivityt::apply(
       // SSA expression
       ssa_exprt tmp = to_ssa_expr(index.array());
       bool was_l2 = !tmp.get_level_2().empty();
-
-      tmp.remove_level_2();
-      index.array() = tmp.get_original_expr();
-      tmp.set_expression(index);
-      if(was_l2)
-        return state.rename(std::move(tmp), ns).get();
-      else
-        return std::move(tmp);
+      if(
+        l2_size.id() == ID_constant &&
+        numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=
+          MAX_FIELD_SENSITIVITY_ARRAY_SIZE)
+      {
+        tmp.remove_level_2();
+        index.array() = tmp.get_original_expr();
+        tmp.set_expression(index);
+        if(was_l2)
+          return state.rename(std::move(tmp), ns).get();
+        else
+          return std::move(tmp);
+      }
     }
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
@@ -147,7 +152,10 @@ exprt field_sensitivityt::get_fields(
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     ssa_expr.type().id() == ID_array &&
-    to_array_type(ssa_expr.type()).size().id() == ID_constant)
+    to_array_type(ssa_expr.type()).size().id() == ID_constant &&
+    numeric_cast_v<mp_integer>(
+      to_constant_expr(to_array_type(ssa_expr.type()).size())) <=
+      MAX_FIELD_SENSITIVITY_ARRAY_SIZE)
   {
     const array_typet &type = to_array_type(ssa_expr.type());
     const std::size_t array_size =
@@ -269,6 +277,9 @@ void field_sensitivityt::field_assignments_rec(
       numeric_cast_v<std::size_t>(to_constant_expr(type->size()));
     PRECONDITION(lhs_fs.operands().size() == array_size);
 
+    if(array_size > MAX_FIELD_SENSITIVITY_ARRAY_SIZE)
+      return;
+
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
     for(std::size_t i = 0; i < array_size; ++i)
     {
@@ -308,7 +319,9 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr)
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   if(
     expr.type().id() == ID_array &&
-    to_array_type(expr.type()).size().id() == ID_constant)
+    to_array_type(expr.type()).size().id() == ID_constant &&
+    numeric_cast_v<mp_integer>(to_constant_expr(
+      to_array_type(expr.type()).size())) <= MAX_FIELD_SENSITIVITY_ARRAY_SIZE)
   {
     return true;
   }

src/goto-symex/field_sensitivity.h

@@ -9,6 +9,8 @@ Author: Michael Tautschnig
 #ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 
+#include <util/magic.h>
+
 class exprt;
 class ssa_exprt;
 class namespacet;

src/util/magic.h

@@ -16,4 +16,8 @@ const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26;
 // The top end of the range of integers for which dstrings are precomputed
 constexpr std::size_t DSTRING_NUMBERS_MAX = 64;
 
+/// Limit the size of arrays for which field_sensitivity gets applied.
+/// Necessary because large constant arrays slow-down the process.
+constexpr std::size_t MAX_FIELD_SENSITIVITY_ARRAY_SIZE = 64;
+
 #endif