How to handle unspecified behaviour like OutOfMemoryError?

I would like to ask how unspecified method contracts should be handled.

For example, the JDK I use explicitly throws java.lang.OutOfMemoryError inside the function java.lang.AbstractStringBuilder.hugeCapacity. Now, I detect bugs, which are certainly valid with my JDK (String greater max size), but where the benchmark contract expects a correctness_witness.

One example where this happens is the StringConcatenation01 benchmark:

https://github.com/sosy-lab/sv-benchmarks/blob/master/java/jbmc-regression/StringConcatenation01/Main.java#L24

assert tmp.equals(args[0] + args[1]);  // problematic code section

javac converts args[0] + args[1] into a StringBuilder append. Now, when the two input string lengths combined are greater than the maximum String length, the function java.lang.AbstractStringBuilder.hugeCapacity explicitly thows the java.lang.OutOfMemoryError. But this exception is not part of the official method contract. It's just there in an official java jdk.

In my opinion, this is undefined behaviour, and should be constrained in the benchmark itself. Another solution from my side would be to ignore java.lang.OutOfMemoryError.

Yes, I think the benchmark inputs should be constrained so that this cannot occur on a machine with SV-COMP hardware specs. Shall we explicitly define the heap limit in the rules?

I would vote against the proposition from @peterschrammel . For SV-COMP 2019, we agreed to ignore java.lang.OutOfMemoryError as only assertion violations has been tracked and the OutOfMemoryError is not an AssertionError.

From my point of view, we cannot make a decision here, before there is a final decision on #884.
Just cutting away the error by limiting the input space feels wrong from my point of view.

I suspect the benchmark StringConcatenation01 is incorrectly classified. It is possible to create an violation_witness without an OOM Error. Looking at the following line:

sv-benchmarks/java/jbmc-regression/StringConcatenation01/Main.java

Line 23 in f86649d

String tmp = s1.concat(s2);

Lets look into the implementation of String.concat and Arrays.copyOf:

public String concat(String str) {
        int otherLen = str.length();
        if (otherLen == 0) {
            return this;
        }
        int len = value.length;
        char buf[] = Arrays.copyOf(value, len + otherLen);
        str.getChars(buf, len);
        return new String(buf, true);
    }

Arrays.copyOf:

    public static char[] copyOf(char[] original, int newLength) {
        char[] copy = new char[newLength];
        System.arraycopy(original, 0, copy, 0,
                         Math.min(original.length, newLength));
        return copy;
    }

if s1.length + s2.length overflows, Arrays.copyOf will get an negative newLength --> allocation of an negative array causes an NegativeArraySizeException

Reproducer:

import java.util.Arrays;
public class Example {
  public static void main(String[] args) {
    char[] chars = new char[Integer.MAX_VALUE / 2 + 1];
    Arrays.fill(chars, 'a');
    String s1 = new String(chars);
    String s2 = new String(chars);
    System.out.println("s1.length = " + s1.length());
    System.out.println("s2.length = " + s2.length());
    System.out.println("s1.length + s2.length = " + (s1.length() + s2.length()));
    s1.concat(s2);
  }
}

javac Example.java && java -Xmx12G Example
s1.length = 1073741824
s2.length = 1073741824
s1.length + s2.length = -2147483648
Exception in thread "main" java.lang.NegativeArraySizeException
	at java.util.Arrays.copyOf(Arrays.java:3332)
	at java.lang.String.concat(String.java:2032)
	at Example.main(Example.java:14)

Thank you @pointhi for this example. I agree that it is necessary to discuss those kinds of RuntimeExceptions in the future as part of the Java Track. As we currently do not track any other errors than assertion violations and used to ignore all paths that terminate before reaching the assertion part of the verification tasks, this counter example does not justify a label change given the current rule set, IMHO.

To change the label, you would have to demonstrate an example that passes line 23:

sv-benchmarks/java/jbmc-regression/StringConcatenation01/Main.java

Line 23 in f86649d

String tmp = s1.concat(s2);

without any error and fails the assertion in line 24:

sv-benchmarks/java/jbmc-regression/StringConcatenation01/Main.java

Line 24 in f86649d

assert tmp.equals(args[0] + args[1]);

The presented counter example does not qualify for this requirement.

I my opinion, your example demonstrates that NegativeArraySizeException should become a verification property as suggested and motivated in #884.