Enable constant propagation of WITH, array, and struct expressions

jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc

@@ -3,9 +3,10 @@ Test
 --function Test.main --show-vcc --max-field-sensitivity-array-size 9 -cp target/classes
 ^EXIT=0$
 ^SIGNAL=0$
-symex_dynamic::dynamic_array#[0-9]\[1\]
 --
 symex_dynamic::dynamic_array#[0-9]\[\[[0-9]\]\]
 --
-This checks that field sensitvity is not applied to an array of size 10
-when the max is set to 9.
+This checks that field sensitivity is not applied to an array of size 10
+when the max is set to 9. The non-field-sensitive array access
+(dynamic_array#N[1]) may be fully propagated and not appear in the VCC;
+the key check is the absence of [[index]] notation.

jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc

@@ -3,9 +3,10 @@ Test
 --function Test.main --show-vcc --no-array-field-sensitivity -cp target/classes
 ^EXIT=0$
 ^SIGNAL=0$
-symex_dynamic::dynamic_array#[0-9]\[1\]
 --
 symex_dynamic::dynamic_array#[0-9]\[\[[0-9]\]\]
 --
-This checks that field sensitvity is not applied to arrays when
-no-array-field-sensitivity is used.
+This checks that field sensitivity is not applied to arrays when
+no-array-field-sensitivity is used. The non-field-sensitive array access
+(dynamic_array#N[1]) may be fully propagated and not appear in the VCC;
+the key check is the absence of [[index]] notation.

regression/cbmc/Array_UF22/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE
 main.c
 --arrays-uf-always --no-propagation --no-simplify
 ^VERIFICATION SUCCESSFUL$
@@ -7,4 +7,5 @@ main.c
 --
 ^warning: ignoring
 --
-This test demonstrates the need for implementing the extensionality rule.
+This test demonstrates the need for implementing the extensionality rule, but
+can also be solved by expression propagation.

regression/cbmc/array-cell-sensitivity2/test.desc

@@ -2,7 +2,6 @@ CORE
 test.c
 --show-vcc
 main::1::array!0@1#2 = with\(main::1::array!0@1#1, (main::argc!0@1#1 \+ -1|cast\(main::argc!0@1#1 \+ -1, signedbv\[64\]\)), 1\)
-main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -11,3 +10,5 @@ main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\)
 This checks that arrays of uncertain size are always treated as aggregates and
 are not expanded into individual cell symbols (which use the [[index]] notation
 to distinguish them from the index operator (array[index]))
+The second WITH (array#3) may be fully propagated and thus not appear in the
+VCC output; the key check is the absence of [[index]] notation.

src/goto-symex/goto_symex_can_forward_propagate.h

@@ -43,18 +43,19 @@ class goto_symex_can_forward_propagatet : public can_forward_propagatet
     }
     else if(expr.id() == ID_with)
     {
-      // this is bad
-#if 0
-      for(const auto &op : expr.operands())
-      {
-        if(!is_constant(op))
-          return false;
-      }
-
+      // Propagate WITH expressions so that indexing at unchanged
+      // positions can be simplified (e.g., (a WITH [2]:=x)[0] -> a[0]).
+      return true;
+    }
+    else if(expr.id() == ID_array || expr.id() == ID_struct)
+    {
+      // Propagate array/struct literals even when they contain
+      // non-constant elements so that constant-index access can
+      // extract the constant parts. This is needed when a WITH
+      // expression is simplified to the base array/struct and that
+      // base contains a mix of constant and non-constant elements
+      // (e.g., DFCC assigns clause tracking arrays).
       return true;
-#else
-      return false;
-#endif
     }
 
     return can_forward_propagatet::is_constant(expr);

src/solvers/flattening/boolbv_byte_update.cpp

@@ -60,9 +60,22 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 
       const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);
 
+      // When the update value is not a multiple of the byte width,
+      // lower_byte_update places the value at the high end of the
+      // last partial byte (concatenating {value, remaining_low_bits}).
+      // For little-endian the high end is at higher bit indices, so
+      // we shift the trailing partial byte's bits up. For big-endian
+      // the endianness map already places bit 0 at the MSB.
+      const std::size_t tail_bits = update_width % byte_width;
+      const std::size_t tail_shift =
+        little_endian && tail_bits != 0 ? byte_width - tail_bits : 0;
+
       for(std::size_t i = 0; i < update_width; i++)
       {
-        size_t index_op = map_op.map_bit(offset_i + i);
+        // Apply the shift only to bits in the last partial byte
+        const std::size_t shift =
+          (i >= update_width - tail_bits && tail_shift != 0) ? tail_shift : 0;
+        size_t index_op = map_op.map_bit(offset_i + shift + i);
         size_t index_value = map_value.map_bit(i);
 
         INVARIANT(