Merge pull request diffblue#5128 from romainbrenguier/bugfix/negative-size-arrays

[TG-9313] Fix invariant failure in case of negative size arrays

Author: romainbrenguier

jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.class

@@ -0,0 +1,11 @@
+public class Test {
+  public static void check(Integer t) {
+    if (t != null)
+      try {
+        Integer[] arr = new Integer[-7];
+        assert false;
+      } catch (NegativeArraySizeException e) {
+        assert false;
+      }
+  }
+}

jbmc/regression/jbmc/array-cell-sensitivity-negative-size/Test.java

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.check
+line 5 Array size should be >= 0: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that defining an array with negative size does not crash JBMC

jbmc/regression/jbmc/array-cell-sensitivity-negative-size/test.desc

@@ -180,14 +180,15 @@ exprt field_sensitivityt::get_fields(
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     ssa_expr.type().id() == ID_array &&
-    to_array_type(ssa_expr.type()).size().id() == ID_constant &&
-    numeric_cast_v<mp_integer>(
-      to_constant_expr(to_array_type(ssa_expr.type()).size())) <=
-      max_field_sensitivity_array_size)
+    to_array_type(ssa_expr.type()).size().id() == ID_constant)
   {
+    const mp_integer mp_array_size = numeric_cast_v<mp_integer>(
+      to_constant_expr(to_array_type(ssa_expr.type()).size()));
+    if(mp_array_size < 0 || mp_array_size > max_field_sensitivity_array_size)
+      return ssa_expr;
+
     const array_typet &type = to_array_type(ssa_expr.type());
-    const std::size_t array_size =
-      numeric_cast_v<std::size_t>(to_constant_expr(type.size()));
+    const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
 
     array_exprt result(type);
     result.reserve_operands(array_size);

src/goto-symex/field_sensitivity.cpp

@@ -141,7 +141,10 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
       if(total>(1<<30)) // realistic limit
         throw analysis_exceptiont("array too large for flattening");
 
-      entry.total_width = numeric_cast_v<std::size_t>(total);
+      if(total < 0)
+        entry.total_width = 0;
+      else
+        entry.total_width = numeric_cast_v<std::size_t>(total);
     }
   }
   else if(type_id==ID_vector)