Sequence display with generic type causes Java assertion failure

[mattmccutchen-amazon]

When Dafny code compiled to Java is run with Java assertions enabled (java -ea), evaluation of a sequence display whose element type is generic causes an assertion failure in the Dafny Java runtime library.

Java assertions (assert CONDITION; statements) are typically disabled by default, including when running the program with dafny /compile:3; I'm guessing that's why no one noticed the problem yet. But I wanted to run the compiled code under JQF in order to test a larger Java program that uses the Dafny code, and JQF enables Java assertions by default.

Example Dafny code that triggers the bug:

function method singletonSeq<T>(x: T): seq<T> {
  [x]
}

datatype MyDatatype = MyDatatype

method Main() {
  // OK
  print [MyDatatype], "\n";

  // Assertion failure
  print singletonSeq(MyDatatype), "\n";
}

Tested with Dafny version: 0e4b2bb (master as of a few days ago)

Steps to reproduce: (Replace $DAFNY with the path to your Dafny working tree.)

1. Save the above code to a file named assertionerror-test.dfy.
2. Compile with $DAFNY/Scripts/dafny /compile:1 /compileTarget:java assertionerror-test.dfy.
3. Run with java -ea -cp assertionerror-test-java:$DAFNY/Binaries/DafnyRuntime.jar assertionerror_test.

Expected output:

[MyDatatype.MyDatatype]
[MyDatatype.MyDatatype]

Actual output:

[MyDatatype.MyDatatype]
Exception in thread "main" java.lang.AssertionError
	at dafny.Array.<init>(Array.java:29)
	at dafny.Array.wrap(Array.java:96)
	at dafny.DafnySequence.of(DafnySequence.java:25)
	at _System.__default.singletonSeq(__default.java:12)
	at _System.__default.Main(__default.java:18)
	at _System.__default.__Main(__default.java:22)
	at dafny.Helpers.withHaltHandling(Helpers.java:205)
	at assertionerror_test.main(assertionerror_test.java:10)

My analysis of the bug:

The failing assertion is here:

dafny/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Array.java

Lines 28 to 33 in 0e4b2bb

	private Array(TypeDescriptor<T> eltType, Object array) {
	assert eltType.arrayType().isInstance(array);
	this.eltType = eltType;
	this.array = array;
	}

This code appears to be checking that the runtime element type of the Java array matches the Dafny type descriptor for the element type. The Java array is being created implicitly by the following varargs call to DafnySequence.of in the compiled code:

  public static <__T> dafny.DafnySequence<? extends __T> singletonSeq(dafny.TypeDescriptor<__T> _td___T, __T x)
  {
    return dafny.DafnySequence.of(_td___T, x);
  }

Since __T is not reified at runtime, the Java compiler doesn't know any better than to use its upper bound (Object) as the runtime element type, and this does not match the Dafny type descriptor for MyDatatype. So the assertion is making an assumption that does not always hold based on the way that Dafny code is currently compiled to Java.

As a workaround, I commented out the failing assertion as well as this similar-looking assertion, which IIRC failed under slightly different circumstances. That didn't seem to have any other harmful effects, but I don't know if it's the best solution.

[robin-aws]

Thanks for the detailed bug report! It does look to me like both assertions are overly optimistic and don't always hold given how the type systems are currently mapped. I believe the more correct assertion would be array.getClass().isAssignableFrom(eltType.arrayType()) - that is, the array should support at least all values specified by the type descriptor, although its element type may be a supertype like Object. Does that version pass for you?

[mattmccutchen-amazon]

array.getClass().isAssignableFrom(eltType.arrayType()) is not quite right: eltType.arrayType() is a dafny.TypeDescriptor and we need a java.lang.Class. I assume you meant array.getClass().isAssignableFrom(eltType.arrayType().javaClass).

That change does seem to fix the issue described here, and my original program passes with it. However, I wonder if it might break other things. The original assertion allows array to be a subtype of eltType.arrayType(), and the new assertion doesn't. Does Dafny ever use arrays of a subtype here? If Dafny has test cases of compilation to Java, running them with assertions enabled might be a good way to check for these issues.

Separately, I wonder if this assertion is providing enough value in terms of catching realistic Dafny bugs to be worth keeping at all, but you're the best one to judge that, not me.

[tbean79]

I came across this problem too. Replacing both assertions in Array.java with array.getClass().isAssignableFrom(eltType.arrayType().javaClass) does not emit an error when running SequenceTest.java, which does feature unbound generic types.

However, that doesn't answer @mattmccutchen-amazon's question of compilation tests. I'm not aware of any such tests within Dafny, I'm afraid.

[cpitclaudel]

However, that doesn't answer @mattmccutchen-amazon's question of compilation tests. I'm not aware of any such tests within Dafny, I'm afraid.

Dafny does have compilation tests, though not very comprehensive ones; there are in the Test/comp/ directory.

[alex-chew]

Thanks for the detailed bug report! It does look to me like both assertions are overly optimistic and don't always hold given how the type systems are currently mapped.

Can we confirm whether or not the failing assertion could lead to soundness bugs? It seems to me that a program written exclusively in Dafny is probably sound even if this assertion fails with -ea, because as @robin-aws mentions, the RTTI isn't sufficient to check the assertion as written. On the other hand, an application in which Dafny components and Java components interoperate, might be unsound unless the (intended) assertion actually holds.

[alex-chew]

Users of generic libraries functions like Seq.MapWithResult will also run into the same error, for example:

// Tmp.dfy; include/import statements omitted
method Main() {
  var arr := [1];
  var res := MapWithResult(x => Result<int, ()>.Success(x), arr);
  if res.Success? {
    print res.value, "\n";
  }
}

$ dafny -version
Dafny 3.9.1.41027

$ dafny build -t java Tmp.dfy
Dafny program verifier finished with 2 verified, 0 errors

$ java -cp Tmp-java:Tmp-java/DafnyRuntime.jar Tmp
[1]

$ java -cp Tmp-java:Tmp-java/DafnyRuntime.jar -ea Tmp
Exception in thread "main" java.lang.AssertionError
        at dafny.Array.<init>(Array.java:29)
        at dafny.Array.wrap(Array.java:96)
        at dafny.DafnySequence.of(DafnySequence.java:25)
        at Seq_Compile.__default.MapWithResult(__default.java:266)
        at _System.__default.Main(__default.java:25)
        at _System.__default.__Main(__default.java:34)
        at Tmp.lambda$main$0(Tmp.java:18)
        at dafny.Helpers.withHaltHandling(Helpers.java:214)
        at Tmp.main(Tmp.java:18)

[RustanLeino]

I agree with what's been said above that the assertion seems mistaken and should be removed. Since the JVM does not support type parameters, I don't think it's realistic to be able to provide an alternative assertion that would capture all situations.

There are other known problems with compilation of Dafny arrays into Java (see #3055). When those get fixed (and I think the fix is to mimic for Java what we do for Go arrays, see #2818), then the code in Array.java will change substantially.