Merge pull request #5690 from tautschnig/negative-size

process_array_expr must not generate arrays of negative size

Author: tautschnig

regression/cbmc-library/memcpy-07/main.c

@@ -0,0 +1,29 @@
+// #include <string.h> intentionally omitted
+
+struct c
+{
+  int d;
+};
+
+struct e
+{
+  struct c *f;
+};
+
+struct g
+{
+  const char *b;
+};
+
+int main()
+{
+  unsigned long nondet;
+
+  struct g *r = (struct g *)nondet;
+  r->b = "";
+
+  struct e *x = (struct e *)nondet;
+  int *d = &x->f->d;
+
+  memcpy(d + 2, 0, 0);
+}

regression/cbmc-library/memcpy-07/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+Invariant check failed
+--
+memcpy invocations must not result in generating arrays of negative size, which
+process_array_expr previously generated when trying to access a string literal
+out of bounds.

src/goto-symex/symex_clean_expr.cpp

@@ -113,7 +113,12 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
       exprt subtype_size = typecast_exprt::conditional_cast(
         subtype_size_opt.value(), array_size_type);
       new_offset = div_exprt(new_offset, subtype_size);
-      minus_exprt new_size(prev_array_type.size(), new_offset);
+      minus_exprt subtraction{prev_array_type.size(), new_offset};
+      if_exprt new_size{
+        binary_predicate_exprt{
+          subtraction, ID_ge, from_integer(0, subtraction.type())},
+        subtraction,
+        from_integer(0, subtraction.type())};
       if(do_simplify)
         simplify(new_size, ns);
 

src/util/simplify_expr.cpp

@@ -1886,6 +1886,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   }
 
   const auto el_size = pointer_offset_bits(expr.type(), ns);
+  if(el_size.has_value() && *el_size < 0)
+    return unchanged(expr);
 
   // byte_extract(byte_extract(root, offset1), offset2) =>
   // byte_extract(root, offset1+offset2)