Make field sensitivity max array size configurable

This will allow the user of symex to set this limit as needed instead of
fixing it to an arbitrary value.

Author: romainbrenguier

src/goto-instrument/accelerate/scratch_program.cpp

@@ -38,6 +38,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
 
   symex_state = util_make_unique<goto_symex_statet>(
     symex_targett::sourcet(goto_functionst::entry_point(), *this),
+    symex.field_sensitivity,
     guard_manager,
     [this](const irep_idt &id) {
       return path_storage.get_unique_l2_index(id);

src/goto-symex/field_sensitivity.cpp

@@ -114,7 +114,7 @@ exprt field_sensitivityt::apply(
       if(
         l2_size.id() == ID_constant &&
         numeric_cast_v<mp_integer>(to_constant_expr(l2_size)) <=
-          MAX_FIELD_SENSITIVITY_ARRAY_SIZE)
+          max_field_sensitivity_array_size)
       {
         if(l2_index.get().id() == ID_constant)
         {
@@ -183,7 +183,7 @@ exprt field_sensitivityt::get_fields(
     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)
+      max_field_sensitivity_array_size)
   {
     const array_typet &type = to_array_type(ssa_expr.type());
     const std::size_t array_size =
@@ -305,7 +305,7 @@ 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)
+    if(array_size > max_field_sensitivity_array_size)
       return;
 
     exprt::operandst::const_iterator fs_it = lhs_fs.operands().begin();
@@ -339,7 +339,7 @@ void field_sensitivityt::field_assignments_rec(
   }
 }
 
-bool field_sensitivityt::is_divisible(const ssa_exprt &expr)
+bool field_sensitivityt::is_divisible(const ssa_exprt &expr) const
 {
   if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
     return true;
@@ -349,7 +349,7 @@ bool field_sensitivityt::is_divisible(const ssa_exprt &expr)
     expr.type().id() == ID_array &&
     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)
+      to_array_type(expr.type()).size())) <= max_field_sensitivity_array_size)
   {
     return true;
   }

src/goto-symex/field_sensitivity.h

@@ -62,7 +62,7 @@ class symex_targett;
 /// When `index` is not a constant, `array[index]` is replaced by
 ///  `{array[[0]]; array[[1]]; …index]`.
 /// Note that this process does not apply to arrays whose size is not constant,
-/// and arrays whose size exceed the bound \ref MAX_FIELD_SENSITIVITY_ARRAY_SIZE
+/// and arrays whose size exceed the bound \c max_field_sensitivity_array_size.
 /// See \ref field_sensitivityt::apply.
 ///
 /// ### Symbols representing arrays
@@ -80,6 +80,13 @@ class symex_targett;
 class field_sensitivityt
 {
 public:
+  /// \param max_array_size: maximum size for which field sensitivity will be
+  ///   applied to array cells
+  field_sensitivityt(std::size_t max_array_size)
+    : max_field_sensitivity_array_size(max_array_size)
+  {
+  }
+
   /// Assign to the individual fields of a non-expanded symbol \p lhs. This is
   /// required whenever prior steps have updated the full object rather than
   /// individual fields, e.g., in case of assignments to an array at an unknown
@@ -133,12 +140,14 @@ class field_sensitivityt
   /// \param expr: the expression to evaluate
   /// \return False, if and only if, \p expr would be a single field-sensitive
   /// SSA expression.
-  static bool is_divisible(const ssa_exprt &expr);
+  bool is_divisible(const ssa_exprt &expr) const;
 
 private:
   /// whether or not to invoke \ref field_sensitivityt::apply
   bool run_apply = true;
 
+  const std::size_t max_field_sensitivity_array_size;
+
   void field_assignments_rec(
     const namespacet &ns,
     goto_symex_statet &state,

src/goto-symex/goto_symex.h

@@ -70,6 +70,9 @@ struct symex_configt final
   /// includes diagnostic information about call stack and guard size.
   bool show_symex_steps;
 
+  /// Maximum sizes for which field sensitivity will be applied to array cells
+  std::size_t max_field_sensitivity_array_size;
+
   /// \brief Construct a symex_configt using options specified in an
   /// \ref optionst
   explicit symex_configt(const optionst &options);
@@ -104,6 +107,7 @@ class goto_symext
     guard_managert &guard_manager)
     : should_pause_symex(false),
       symex_config(options),
+      field_sensitivity(symex_config.max_field_sensitivity_array_size),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
       guard_manager(guard_manager),
@@ -259,6 +263,9 @@ class goto_symext
   /// if we know the source language in use, irep_idt() otherwise.
   irep_idt language_mode;
 
+  /// Functor controling granularity of object accesses
+  field_sensitivityt field_sensitivity;
+
 protected:
   /// The symbol table associated with the goto-program being executed.
   /// This symbol table will not have objects that are dynamically created as

src/goto-symex/goto_symex_state.cpp

@@ -34,10 +34,12 @@ static void get_l1_name(exprt &expr);
 
 goto_symex_statet::goto_symex_statet(
   const symex_targett::sourcet &_source,
+  field_sensitivityt &field_sensitivity,
   guard_managert &manager,
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider)
   : goto_statet(manager),
     source(_source),
+    field_sensitivity(field_sensitivity),
     guard_manager(manager),
     symex_target(nullptr),
     record_events({true}),
@@ -370,7 +372,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   }
 
   // only continue if an indivisible object is being accessed
-  if(field_sensitivityt::is_divisible(expr))
+  if(field_sensitivity.is_divisible(expr))
     return false;
 
   const ssa_exprt ssa_l1 = remove_level_2(expr);
@@ -498,7 +500,7 @@ goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
   }
 
   // only continue if an indivisible object is being accessed
-  if(field_sensitivityt::is_divisible(expr))
+  if(field_sensitivity.is_divisible(expr))
     return write_is_shared_resultt::NOT_SHARED;
 
   if(atomic_section_id != 0)

src/goto-symex/goto_symex_state.h

@@ -47,6 +47,7 @@ class goto_symex_statet final : public goto_statet
 public:
   goto_symex_statet(
     const symex_targett::sourcet &,
+    field_sensitivityt &field_sensitivity,
     guard_managert &manager,
     std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
   ~goto_symex_statet();
@@ -67,6 +68,9 @@ class goto_symex_statet final : public goto_statet
   /// for error traces even after symbolic execution has finished.
   symbol_tablet symbol_table;
 
+  /// Reference to the functor, owned by goto_symext, used for renaming.
+  field_sensitivityt &field_sensitivity;
+
   // Manager is required to be able to resize the thread vector
   guard_managert &guard_manager;
   symex_target_equationt *symex_target;
@@ -120,8 +124,6 @@ class goto_symex_statet final : public goto_statet
     bool record_value,
     bool allow_pointer_unsoundness = false);
 
-  field_sensitivityt field_sensitivity;
-
 protected:
   template <levelt>
   void rename_address(exprt &expr, const namespacet &ns);

src/goto-symex/symex_assign.cpp

@@ -204,7 +204,7 @@ void symex_assignt::assign_non_struct_symbol(
     current_assignment_type);
 
   const ssa_exprt &l1_lhs = assignment.lhs;
-  if(field_sensitivityt::is_divisible(l1_lhs))
+  if(state.field_sensitivity.is_divisible(l1_lhs))
   {
     // Split composite symbol lhs into its components
     state.field_sensitivity.field_assignments(

src/goto-symex/symex_builtin_functions.cpp

@@ -394,7 +394,7 @@ void goto_symext::symex_printf(
   else
   {
     clean_expr(*va_args, state, false);
-    *va_args = field_sensitivityt{}.apply(ns, state, *va_args, false);
+    *va_args = field_sensitivity.apply(ns, state, *va_args, false);
     *va_args = state.rename(*va_args, ns).get();
     if(va_args->id() != ID_array)
     {

src/goto-symex/symex_goto.cpp

@@ -618,7 +618,7 @@ static void merge_names(
   }
 
   // field sensitivity: only merge on individual fields
-  if(field_sensitivityt::is_divisible(ssa))
+  if(dest_state.field_sensitivity.is_divisible(ssa))
     return;
 
   // shared variables are renamed on every access anyway, we don't need to

src/goto-symex/symex_main.cpp

@@ -44,7 +44,9 @@ symex_configt::symex_configt(const optionst &options)
     partial_loops(options.get_bool_option("partial-loops")),
     debug_level(unsafe_string2int(options.get_option("debug-level"))),
     run_validation_checks(options.get_bool_option("validate-ssa-equation")),
-    show_symex_steps(options.get_bool_option("show-goto-symex-steps"))
+    show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
+    max_field_sensitivity_array_size(
+      options.get_unsigned_int_option("max-field-sensitivity-array-size"))
 {
 }
 
@@ -347,6 +349,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
   // create and prepare the state
   auto state = util_make_unique<statet>(
     symex_targett::sourcet(entry_point_id, start_function->body),
+    field_sensitivity,
     guard_manager,
     [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); });