Merge pull request #7394 from tautschnig/bugfixes/array-out-of-bounds

get_subexpression_at_offset: do not permit out-of-bounds access

Author: tautschnig

jbmc/src/java_bytecode/java_trace_validation.cpp

@@ -285,18 +285,7 @@ static void check_rhs_assumptions(
   // check byte extract rhs structure
   else if(const auto byte = expr_try_dynamic_cast<byte_extract_exprt>(rhs))
   {
-    DATA_CHECK_WITH_DIAGNOSTICS(
-      vm,
-      byte->operands().size() == 2,
-      "RHS",
-      rhs.pretty(),
-      "Expecting a byte extract with two operands.");
-    DATA_CHECK_WITH_DIAGNOSTICS(
-      vm,
-      can_cast_expr<constant_exprt>(simplify_expr(byte->op(), ns)),
-      "RHS",
-      rhs.pretty(),
-      "Expecting a byte extract with constant value.");
+    check_rhs_assumptions(simplify_expr(byte->op(), ns), ns, vm);
     DATA_CHECK_WITH_DIAGNOSTICS(
       vm,
       can_cast_expr<constant_exprt>(simplify_expr(byte->offset(), ns)),

regression/cbmc/union-unequal-element-size1/test.desc

@@ -1,10 +1,8 @@
-KNOWNBUG
+CORE
 main.c
 --verbosity 10
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
---
-assert(s) fails with field sensitivity, but passes without

src/solvers/flattening/boolbv_get.cpp

@@ -297,16 +297,11 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
   exprt size=simplify_expr(get(size_expr), ns);
 
   // get the numeric value, unless it's infinity
-  mp_integer size_mpint = 0;
+  const auto size_opt = numeric_cast<mp_integer>(size);
 
-  if(size.is_not_nil() && size.id() != ID_infinity)
-  {
-    const auto size_opt = numeric_cast<mp_integer>(size);
-    if(size_opt.has_value() && *size_opt >= 0)
-      size_mpint = *size_opt;
-  }
-
-  // search array indices
+  // search array indices, and only use those applicable to a particular model
+  // (array theory may have seen other indices, which might only be live under a
+  // different model)
 
   typedef std::map<mp_integer, exprt> valuest;
   valuest values;
@@ -336,7 +331,9 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
       {
         const auto index_mpint = numeric_cast<mp_integer>(index_value);
 
-        if(index_mpint.has_value())
+        if(
+          index_mpint.has_value() && *index_mpint >= 0 &&
+          (!size_opt.has_value() || *index_mpint < *size_opt))
         {
           if(value.is_nil())
             values[*index_mpint] =
@@ -350,7 +347,7 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
 
   exprt result;
 
-  if(values.size() != size_mpint)
+  if(!size_opt.has_value() || values.size() != *size_opt)
   {
     result = array_list_exprt({}, to_array_type(type));
 
@@ -370,17 +367,18 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
     result=exprt(ID_array, type);
 
     // allocate operands
-    std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
+    std::size_t size_int = numeric_cast_v<std::size_t>(*size_opt);
     result.operands().resize(size_int, exprt{ID_unknown});
 
     // search uninterpreted functions
 
     for(valuest::iterator it=values.begin();
         it!=values.end();
         it++)
-      if(it->first>=0 && it->first<size_mpint)
-        result.operands()[numeric_cast_v<std::size_t>(it->first)].swap(
-          it->second);
+    {
+      result.operands()[numeric_cast_v<std::size_t>(it->first)].swap(
+        it->second);
+    }
   }
 
   return result;

src/util/pointer_offset_size.cpp

@@ -633,17 +633,22 @@ optionalt<exprt> get_subexpression_at_offset(
 
     // no arrays of non-byte-aligned, zero-, or unknown-sized objects
     if(
-      elem_size_bits.has_value() && *elem_size_bits > 0 &&
-      *elem_size_bits % config.ansi_c.char_width == 0 &&
+      array_type.size().is_constant() && elem_size_bits.has_value() &&
+      *elem_size_bits > 0 && *elem_size_bits % config.ansi_c.char_width == 0 &&
       *target_size_bits <= *elem_size_bits)
     {
+      const mp_integer array_size =
+        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
       const mp_integer elem_size_bytes =
         *elem_size_bits / config.ansi_c.char_width;
+      const mp_integer index = offset_bytes / elem_size_bytes;
       const auto offset_inside_elem = offset_bytes % elem_size_bytes;
       const auto target_size_bytes =
         *target_size_bits / config.ansi_c.char_width;
       // only recurse if the cell completely contains the target
-      if(offset_inside_elem + target_size_bytes <= elem_size_bytes)
+      if(
+        index < array_size &&
+        offset_inside_elem + target_size_bytes <= elem_size_bytes)
       {
         return get_subexpression_at_offset(
           index_exprt(