goto-symex: optionally support updates across member boundaries

If using the new option --symex-no-member-bounds, goto-symex will
rewrite all indexed writes that constant propagation does not show to be
within bounds to writes to the member object.

Author: tautschnig

regression/cbmc/member_bounds1/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---no-simplify
+--no-simplify --symex-no-member-bounds
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
@@ -9,3 +9,5 @@ main.c
 --
 This test passes when using the simplifier, but results in "WITH" expressions
 that update elements outside their bounds without the simplifier.
+--symex-no-member-bounds ensures that such expressions are rewritten by
+goto-symex.

regression/cbmc/member_bounds2/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
-
+--symex-no-member-bounds
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
@@ -9,3 +9,5 @@ main.c
 --
 Field sensitivity makes it (currently) impossible to update bytes outside the
 particular field.
+--symex-no-member-bounds ensures that such expressions are rewritten by
+goto-symex.

src/goto-checker/bmc_util.h

@@ -197,6 +197,7 @@ void run_property_decider(
   "(unwind-max):" \
   "(ignore-properties-before-unwind-min)" \
   "(symex-cache-dereferences)" \
+  "(symex-no-member-bounds)" \
 
 #define HELP_BMC \
   " --paths [strategy]           explore paths one at a time\n" \
@@ -252,6 +253,7 @@ void run_property_decider(
   "                              gets blacklisted\n" \
   " --graphml-witness filename   write the witness in GraphML format to filename\n" /* NOLINT(*) */ \
   " --symex-cache-dereferences   enable caching of repeated dereferences" \
+  " --symex-no-member-bounds     support updates beyond bounds of a compound member" /* NOLINT(*) */ \
 // clang-format on
 
 #endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H

src/goto-symex/symex_assign.cpp

@@ -11,12 +11,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "symex_assign.h"
 
-#include "expr_skeleton.h"
-#include "goto_symex_state.h"
+#include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/expr_util.h>
+#include <util/pointer_offset_size.h>
 #include <util/range.h>
 
+#include "expr_skeleton.h"
+#include "goto_symex_state.h"
 #include "symex_config.h"
 
 // We can either use with_exprt or update_exprt when building expressions that
@@ -253,11 +255,90 @@ void symex_assignt::assign_array(
 {
   const exprt &lhs_array=lhs.array();
   const exprt &lhs_index=lhs.index();
-  const typet &lhs_index_type = lhs_array.type();
+  const array_typet &lhs_array_type = to_array_type(lhs_array.type());
+
+  const bool may_be_out_of_bounds =
+    symex_config.updates_across_member_bounds &&
+    (lhs_index.id() != ID_constant ||
+     lhs_array_type.size().id() != ID_constant ||
+     numeric_cast_v<mp_integer>(to_constant_expr(lhs_index)) < 0 ||
+     numeric_cast_v<mp_integer>(to_constant_expr(lhs_index)) >=
+       numeric_cast_v<mp_integer>(to_constant_expr(lhs_array_type.size())));
+
+  if(
+    may_be_out_of_bounds &&
+    (lhs_array.id() == ID_member || lhs_array.id() == ID_index))
+  {
+    const auto subtype_bytes_opt = size_of_expr(lhs_array.type().subtype(), ns);
+    CHECK_RETURN(subtype_bytes_opt.has_value());
 
-  PRECONDITION(lhs_index_type.id() == ID_array);
+    exprt new_offset = mult_exprt{
+      lhs_index,
+      typecast_exprt::conditional_cast(*subtype_bytes_opt, lhs_index.type())};
 
-  if(use_update)
+    exprt parent;
+    if(lhs_array.id() == ID_member)
+    {
+      const member_exprt &member = to_member_expr(lhs_array);
+      const auto member_offset = member_offset_expr(member, ns);
+      CHECK_RETURN(member_offset.has_value());
+
+      parent = member.compound();
+      new_offset = plus_exprt{
+        typecast_exprt::conditional_cast(*member_offset, new_offset.type()),
+        new_offset};
+    }
+    else
+    {
+      const index_exprt &index = to_index_expr(lhs_array);
+
+      const auto element_size_opt =
+        size_of_expr(to_array_type(index.array().type()).subtype(), ns);
+      CHECK_RETURN(element_size_opt.has_value());
+
+      parent = index.array();
+      new_offset =
+        plus_exprt{mult_exprt{typecast_exprt::conditional_cast(
+                                *element_size_opt, new_offset.type()),
+                              typecast_exprt::conditional_cast(
+                                index.index(), new_offset.type())},
+                   new_offset};
+    }
+
+    if(symex_config.simplify_opt)
+      simplify(new_offset, ns);
+
+    const byte_update_exprt new_rhs = make_byte_update(parent, new_offset, rhs);
+    const expr_skeletont new_skeleton =
+      full_lhs.compose(expr_skeletont::remove_op0(lhs_array));
+    assign_rec(parent, new_skeleton, new_rhs, guard);
+  }
+  else if(
+    may_be_out_of_bounds && (lhs_array.id() == ID_byte_extract_big_endian ||
+                             lhs_array.id() == ID_byte_extract_little_endian))
+  {
+    const byte_extract_exprt &byte_extract = to_byte_extract_expr(lhs_array);
+
+    const auto subtype_bytes_opt = size_of_expr(lhs_array.type().subtype(), ns);
+    CHECK_RETURN(subtype_bytes_opt.has_value());
+
+    exprt new_offset =
+      plus_exprt{mult_exprt{lhs_index,
+                            typecast_exprt::conditional_cast(
+                              *subtype_bytes_opt, lhs_index.type())},
+                 typecast_exprt::conditional_cast(
+                   byte_extract.offset(), lhs_index.type())};
+
+    if(symex_config.simplify_opt)
+      simplify(new_offset, ns);
+
+    byte_extract_exprt new_lhs = byte_extract;
+    new_lhs.offset() = new_offset;
+    new_lhs.type() = rhs.type();
+
+    assign_rec(new_lhs, full_lhs, rhs, guard);
+  }
+  else if(use_update)
   {
     // turn
     //   a[i]=e

src/goto-symex/symex_config.h

@@ -63,6 +63,10 @@ struct symex_configt final
   ///   Used in goto_symext::dereference_rec
   bool cache_dereferences;
 
+  /// Handle assignments beyond the bounds prescribed by a struct or array
+  /// access path. See tests in regression/cbmc/member_bounds* for examples.
+  bool updates_across_member_bounds;
+
   /// \brief Construct a symex_configt using options specified in an
   /// \ref optionst
   explicit symex_configt(const optionst &options);

src/goto-symex/symex_main.cpp

@@ -56,7 +56,9 @@ symex_configt::symex_configt(const optionst &options)
             : DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE),
     complexity_limits_active(
       options.get_signed_int_option("symex-complexity-limit") > 0),
-    cache_dereferences{options.get_bool_option("symex-cache-dereferences")}
+    cache_dereferences{options.get_bool_option("symex-cache-dereferences")},
+    updates_across_member_bounds{
+      options.get_bool_option("symex-no-member-bounds")}
 {
 }