Dafny generated code not necessarily backwards compatible with code generated by older Dafny versions

[robin-aws]

Dafny version

Combination of 4.2 and 4.6

Code to produce this issue

// in Library.dfy
module Library {
  datatype Option<+T> = Some(value: T) | None
}

// in App.dfy
include "Library.dfy"

module App {

  import opened Library

  function Foo(): Option<int> {
    Some(42)
  }
}

Command to run and resulting output

% ~/dafnies/dafny-4.6.0/dafny translate java Library.dfy --compile-suffix --include-runtime

Dafny program verifier finished with 0 verified, 0 errors

% javac -cp Library-java Library-java/Library.java   

% ~/dafnies/dafny-4.2.0/dafny translate java App.dfy --library Library.dfy

Dafny program verifier finished with 0 verified, 0 errors

% javac -cp App-java:Library-java App-java/App_Compile/__default.java
App-java/App_Compile/__default.java:12: error: method create_Some in class Option<T#2> cannot be applied to given types;
    System.out.print(java.lang.String.valueOf(Library_Compile.Option.<java.math.BigInteger>create_Some(java.math.BigInteger.valueOf(42L))));
                                                                    ^
  required: TypeDescriptor<T#1>,T#1
  found:    BigInteger
  reason: actual and formal argument lists differ in length
  where T#1,T#2 are type-variables:
    T#1 extends Object declared in method <T#1>create_Some(TypeDescriptor<T#1>,T#1)
    T#2 extends Object declared in class Option
App-java/App_Compile/__default.java:12: error: incompatible types: BigInteger cannot be converted to TypeDescriptor<BigInteger>
    System.out.print(java.lang.String.valueOf(Library_Compile.Option.<java.math.BigInteger>create_Some(java.math.BigInteger.valueOf(42L))));

What happened?

The root cause is that there was a change in how TypeDescriptors are used in generated Java code in Dafny 4.3.

This is an issue because it means the library in this case can't be rebuilt with a newer version of Dafny without breaking older consuming projects still using an older version of Dafny. That means every Dafny upgrade can potentially force a major version bump of the target language library built with it, which is not intended and has high operational impact.

What type of operating system are you experiencing the problem on?

Mac

[robin-aws]

I've called this a bug even though there's no explicit claim anywhere that this will work, just because it's a natural assumption of how Dafny versioning should work: a minor version change of Dafny should not be expected to cause a major version bump in artifacts generated using it.

[robin-aws]

As a fix to the specific problem described above (which is the real release blocker), I'm going to add a hidden option to generate overloads of methods like create_Some that do not take type descriptors, and initialize them internally to null instead. This may re-introduce the bug that adding these type descriptors was intended to fix (will dig up the original PR for context), but code that is compiling now by definition shouldn't be hitting those cases.

Even if this allows us to remove the release-blocker label, this issue should stay open until we have regression testing for this general requirement.

[keyboardDrummer]

I don't see how this is a release blocker since it's an already released issue. It's not better to resolve it in 4.7 than in a later version. The more important thing IMO is when we resolve it, which doesn't need to be any different if we resolve it in 4.8 than in a delayed 4.7.

This is an issue because it means the library in this case can't be rebuilt with a newer version of Dafny without breaking older consuming projects still using an older version of Dafny.

By "breaking older consuming projects still using an older version of Dafny", do you mean preventing those projects from updating to the newer library version, without also updating their Dafny version?

a minor version change of Dafny should not be expected to cause a major version bump in artifacts generated using it.

Seems fair. Would be nice if the code generators were versioned independently, where each code generator version would be compatible with a range of Dafny versions. That way users could update to newer Dafny versions while still keeping an older code generator so they do not incur a major version bump in the generated artifacts.

[robin-aws]

I don't see how this is a release blocker since it's an already released issue. It's not better to resolve it in 4.7 than in a later version. The more important thing IMO is when we resolve it, which doesn't need to be any different if we resolve it in 4.8 than in a delayed 4.7.

That's fair, and I only wanted to block 4.7 on it assuming the fix is quick, and therefore doesn't delay it by much. If that turns out not to be the case it probably is smarter to get 4.7 out first.

By "breaking older consuming projects still using an older version of Dafny", do you mean preventing those projects from updating to the newer library version, without also updating their Dafny version?

Yup, and the bigger issue is that it's pretty easy for a Java build system to automatically attempt to use the newer version without any changes to the consuming library, say when resolving version conflicts. Bumping the major version of the library is the best way to prevent that.

Seems fair. Would be nice if the code generators were versioned independently, where each code generator version would be compatible with a range of Dafny versions. That way users could update to newer Dafny versions while still keeping an older code generator so they do not incur a major version bump in the generated artifacts.

I think that's a great state to move towards, possibly having each code generator as a separately-managed compiler plugin in general.