Simplifier: a sizeof factor of one keeps its annotation

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;
+}

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].

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.

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'],

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)

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;
+      }
     }
   }