From 9ea6cd6921d7528524ad6dd39ce333b821fc93b9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 8 Oct 2026 08:50:45 +0000
Subject: [PATCH] Simplifier: a sizeof factor of one keeps its annotation

symex_allocate takes the element type of `malloc(sizeof(T) * n)' from
the product's sizeof annotation.  simplify_mult deleted a factor of one
together with its annotation, so with n a constant computed from another
sizeof -- `sizeof(char) * (5 * sizeof(long))', as libstdc++'s
num_put::_M_insert_int allocates its digit buffer -- the object became a
long[5], and every char store a byte_update that constant propagation
could not see through.  The factor is still deleted (kept, it would
leave `1 * n' in the formula of every char allocation), but its
annotation moves onto the product; and a typecast simplified to a
constant keeps its own annotation over its operand's, so `(size_t)ilen'
stays a char size once ilen is propagated.  New test
cbmc/alloca_sizeof_char_times_sizeof_constant.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 .../main.c                                     | 15 +++++++++++++++
 .../test.desc                                  | 11 +++++++++++
 .../test_verify.desc                           | 12 ++++++++++++
 regression/validate-trace-xml-schema/check.py  |  2 ++
 src/util/simplify_expr.cpp                     | 12 +++++++++---
 src/util/simplify_expr_int.cpp                 | 18 +++++++++++++++---
 6 files changed, 64 insertions(+), 6 deletions(-)
 create mode 100644 regression/cbmc/alloca_sizeof_char_times_sizeof_constant/main.c
 create mode 100644 regression/cbmc/alloca_sizeof_char_times_sizeof_constant/test.desc
 create mode 100644 regression/cbmc/alloca_sizeof_char_times_sizeof_constant/test_verify.desc

diff --git a/regression/cbmc/alloca_sizeof_char_times_sizeof_constant/main.c b/regression/cbmc/alloca_sizeof_char_times_sizeof_constant/main.c
new file mode 100644
index 000000000000..e9d8a710c728
--- /dev/null
+++ b/regression/cbmc/alloca_sizeof_char_times_sizeof_constant/main.c
@@ -0,0 +1,15 @@
+// The element type of an allocation `sizeof(char) * n' is char even when n
+// is a constant computed from another sizeof (libstdc++'s
+// num_put::_M_insert_int allocates its digit buffer this way).  With a
+// buffer of long elements every char store became a byte_update that
+// constant propagation could not see through.
+int main()
+{
+  const int ilen = 5 * sizeof(long);
+  char *p = __builtin_alloca(sizeof(char) * ilen);
+  p[ilen - 2] = '4';
+  if(p[ilen - 2] == '4')
+    p[ilen - 1] = '2';
+  __CPROVER_assert(p[ilen - 1] == '2', "stored");
+  return 0;
+}
diff --git a/regression/cbmc/alloca_sizeof_char_times_sizeof_constant/test.desc b/regression/cbmc/alloca_sizeof_char_times_sizeof_constant/test.desc
new file mode 100644
index 000000000000..4e94178d57a4
--- /dev/null
+++ b/regression/cbmc/alloca_sizeof_char_times_sizeof_constant/test.desc
@@ -0,0 +1,11 @@
+CORE gcc-only
+main.c
+--program-only
+nondet_symbol<char \[
+^EXIT=0$
+^SIGNAL=0$
+--
+nondet_symbol<signed long int \[
+byte_update
+--
+The allocated object must have type char[40], not long[5].
diff --git a/regression/cbmc/alloca_sizeof_char_times_sizeof_constant/test_verify.desc b/regression/cbmc/alloca_sizeof_char_times_sizeof_constant/test_verify.desc
new file mode 100644
index 000000000000..ffebc01faeb0
--- /dev/null
+++ b/regression/cbmc/alloca_sizeof_char_times_sizeof_constant/test_verify.desc
@@ -0,0 +1,12 @@
+CORE gcc-only
+main.c
+
+^\[main\.assertion\.1\] line \d+ stored: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The verification counterpart of test.desc; it also passes on bin53, where
+the stores are byte_updates of a long[5] object.
diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py
index 8ede2e47dd33..bb5ad3fadb64 100644
--- a/regression/validate-trace-xml-schema/check.py
+++ b/regression/validate-trace-xml-schema/check.py
@@ -15,6 +15,8 @@
     # these tests dump the raw SMT2 output (using --outfile)
     ['array_of_bool_as_bitvec', 'test-smt2-outfile.desc'],
     ['deterministic-smt-output', 'test.desc'],
+    # this test prints the goto program (--program-only), not a trace
+    ['alloca_sizeof_char_times_sizeof_constant', 'test.desc'],
     ['z3-lambda-unflatten', 'test.desc'],
     # these tests expect input from stdin
     ['json-interface1', 'test_wrong_option.desc'],
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index eaa011b67e96..43f1f44aa428 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1116,9 +1116,15 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
   {
     const irep_idt &value=to_constant_expr(operand).get_value();
 
-    // preserve the sizeof type annotation
-    typet c_sizeof_type=
-      static_cast<const typet &>(operand.find(ID_C_c_sizeof_type));
+    // preserve the sizeof type annotation, the cast's own first (simplify_mult
+    // moves that of a `sizeof(char)' factor of one onto `(size_t)n')
+    typet c_sizeof_type =
+      static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
+    if(c_sizeof_type.is_nil())
+    {
+      c_sizeof_type =
+        static_cast<const typet &>(operand.find(ID_C_c_sizeof_type));
+    }
 
     if(op_type_id==ID_integer ||
        op_type_id==ID_natural)
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 12e64cca620c..3bebcb83fd30 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -251,15 +251,27 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mult(const mult_exprt &expr)
   }
   else
   {
-    // if the constant is a one and there are other factors
+    // if the constant is a one and there are other factors, delete it; a
+    // one that is `sizeof(T)' (T a character type) leaves its annotation on
+    // the product: it records the element type of an allocation
+    // `malloc(sizeof(T) * n)' (see symex_allocate) also once n has a value
+    // of its own, which may carry the annotation of another sizeof.  (Kept
+    // as a factor, it left `1 * n' in the formula of every char allocation:
+    // 260 more variables in benchcomp's aws_byte_buf_cat.)
     if(constant_found && *constant == 1)
     {
-      // just delete it
+      // just delete it, but keep a sizeof annotation on the product
+      const irept sizeof_type = constant->find(ID_C_c_sizeof_type);
       new_operands.erase(constant);
       no_change = false;
 
       if(new_operands.size() == 1)
-        return new_operands.front();
+      {
+        exprt result = new_operands.front();
+        if(sizeof_type.is_not_nil())
+          result.set(ID_C_c_sizeof_type, sizeof_type);
+        return result;
+      }
     }
   }