Unsoundness with Arrays in JBMC

[lks9]

Environment

CBMC version: 6.1.1 (cbmc-6.1.1-34-gc193c276ab)
Operating system: Linux 5.15.0-119-generic #129~20.04.1-Ubuntu SMP x86_64

Explanation

In ExampleTraceAssertion.zip, I have two files Example.java and example.c. I am checking example() in both versions.

Both versions should lead to VERIFICATION FAILED because the assertion in line 14 (reached from example()) is counter satisfiable. However the jbmc version reports SUCCESS.

Exact command line resulting in the issue:

jbmc   "Example.example:([III)V" --throw-runtime-exceptions --disable-uncaught-exception-check  --unwind 9 --unwinding-assertions

Expected (JBMC version)

The assertion verification should fail:

** Results:
Example.java function java::Example.example:([III)V
[java::Example.example:([III)V.unwind.1] line 35 unwinding assertion loop 1: SUCCESS
[java::Example.example:([III)V.unwind.0] line 45 unwinding assertion loop 0: SUCCESS
[java::Example.example:([III)V.assertion.1] line 54 assertion at file Example.java line 54 function java::Example.example:([III)V bytecode-index 247: SUCCESS

Example.java function java::Example.next_elem:(I)V
[java::Example.next_elem:(I)V.assertion.1] line 14 assertion at file Example.java line 14 function java::Example.next_elem:(I)V bytecode-index 29: FAILURE

** 1 of 4 failed (2 iterations)
VERIFICATION FAILED

What happened instead (JBMC version)

But instead jbmc reports false success:

** Results:
Example.java function java::Example.example:([III)V
[java::Example.example:([III)V.unwind.1] line 35 unwinding assertion loop 1: SUCCESS
[java::Example.example:([III)V.unwind.0] line 45 unwinding assertion loop 0: SUCCESS
[java::Example.example:([III)V.assertion.1] line 54 assertion at file Example.java line 54 function java::Example.example:([III)V bytecode-index 210: SUCCESS

Example.java function java::Example.next_elem:(I)V
[java::Example.next_elem:(I)V.assertion.1] line 14 assertion at file Example.java line 14 function java::Example.next_elem:(I)V bytecode-index 29: SUCCESS

** 0 of 4 failed (1 iterations)
VERIFICATION SUCCESSFUL

Variation I as expected

cbmc with example.c gives the expected result:

cbmc example.c --function example --no-standard-checks --unwind 9 --unwinding-assertions

Variation II as expected

jbmc with a concrete array int[] a = { 413, 134, 1, 41, -32, 0, -500, 413, 1 }; gives the expected result. Just comment out that line and comment in int[] a = a2;.

Variation III as expected

Change assert(index != 18) to assert(index != 17) in line 14 of Example.java.

Further remarks

This is a simplified excerpt of one of my retracing examples, DualPivotQuicksort from https://github.com/ProRunVis/ProRunVis-examples. I can show you the full example if needed.

[lks9]

By chance, I finally found out what is the problem.

Simplified test file:

public class Unsound {
    public static void foo(int[] a) {
        if (a != null && a.length > 5) {
            assert false;
        }
    }
}

Then:

javac -g Unsound.java
jbmc "Unsound.foo:([I)V"

Result:

** 0 of 14 failed (1 iterations)
VERIFICATION SUCCESSFUL

But with --max-nondet-array-length 30 we get VERIFICATION FAILED:

jbmc "Unsound.foo:([I)V" --max-nondet-array-length 30

Apparently, --max-nondet-array-length defaults to 5. This makes it unsound.

I would suggest to fix the unsoundness or give a proper warning in the verification result, that array length <= 5 is assumed. For soundness, one could add some --nondet-length-assertions similar to --unwinding-assertions to automatically prove such assumptions. By the way, 5 is still a rather low limit, but I could imagine you have it so low because of the performance impact.

[peterschrammel]

Correct. This is currently quite intransparent. It would be better to clearly display the configured bound in the output to avoid such surprises.

because of the performance impact.

Yes the choice has been made to have bounds by default because JBMC is not going to terminate on almost any program otherwise.

one could add some --nondet-length-assertions

What specifically do you have in mind how this should work?

[lks9]

one could add some --nondet-length-assertions

What specifically do you have in mind how this should work?

I was thinking to leave the length unconstrained until the first access of an array element. Only then, the assumption length <= 5 is needed. For my Unsound.foo example, we don't need the assumption at all because there is no array element access.

In some cases, it already follows from the path condition that length <= 5, so we could also prove the assumption at that state. Example:

public class ArrayLengthExample {
    public static int bar(int[] a, int i) {
        if (a.length == 4 && 0 <= i && i < 4) {
            return a[i];
        }
        return -1;
    }
}

Here the verification with --nondet-length-assertions would check a.length <= 5 just before the access of a[i]. And this would succeed because of the if-guard in the line before.

But I could imagine that this would be hard to implement.

[lks9]

one could add some --nondet-length-assertions

What specifically do you have in mind how this should work?

I was thinking to leave the length unconstrained until the first access of an array element. Only then, the assumption length <= 5 is needed. For my Unsound.foo example, we don't need the assumption at all because there is no array element access.

After sleeping over this, I realized that there is a better solution. For any nondet array, JBMC just creates max_nondet_array_length elements, regardless of the size. So the reason for the a.length <= max_nondet_array_length assumption is that any access with an index outside can't be modeled.

New suggestion:

• Remove the assumption a.length <= max_nondet_array_length.
• Whenever an array access a[i] happens, add the assumption i < max_nondet_array_length after the usual out-of-bounds exception check (so we already know i < a.length).
• The out of bounds exception check 0 < i or i >= a.length is done without any unsound assumptions. We no longer assume anything on the array length and we do not assume i < max_nondet_array_length for the out-of-bounds check.
• The new flag --nondet-array-assertions would place the assertions i < max_nondet_array_length before an array access. And this should be provable in much more cases than my previous idea (the new assertion follows from a.length <= max_nondet_array_length after a successful bounds check).

Insertion sort example:

public void sort (int[] a, right) {
    for (int i = 0; i < right; i++) {
       // access only a[0],...,a[i]
    }
}

For any unwind bound smaller max_nondet_array_length, it follows that i < max_nondet_array_length.

This would also make a modified Unsound example work without increasing the max_nondet_array_length, since there is no upper limit assumption on a.length:

public class Unsound {
    public static void foo(int[] a) {
        if (a != null && a.length > 5) {
            a[0] = 3;
            assert false;
        }
    }
}

For the access a[0], the assumption 0 < a.length follows from the path condition.

There is also the option to completely change how arrays are modeled to achieve soundness without a max_nondet_array_length (and in theory, this is indeed possible), but I could imagine you did not do it because of the performance.

[lks9]

With 511be72 I found out that completely resolving the unsoundness issue is actually not so complicated:

• Remove the assumption a.length <= max_nondet_array_length but keep the assumption 0 <= a.length.
• Remove the ID_length_upper_bound property.
• remove_java_new.cpp#L243-L252 already includes a check when ID_length_upper_bound is missing. Then the array size remains unconstrained. Apparently, the handling of such arrays is already there...

Apparently, the trace output makes use of --max-nondet-array-length somehow, so for a reliable trace output, I still needed to set the limit appropriately.

For my examples, the run-time was not much affected. I called it quickfix, because it completely ignores max_nondet_array_length. For keeping a user provided limit, some modifications need to be done. Also, I did not really test it. And finally, I do not know in which way you want this to be fixed.

[lks9]

Closed with #8432