Java code generator casts java.lang.Integer to byte instead of using conversion method

[ssomayyajula]

Dafny version

4.10.1, but at least since 4.9.2

Code to produce this issue

datatype Option<A> = Some(value: A) | None()

import opened Std.BoundedInts

method M(bucket: Option<uint32>) returns (out: uint8)
  requires bucket.Some?
{
  out := bucket.value as uint8;
}

Command to run and resulting output

dafny build --no-verify --target=java --standard-libraries

error: incompatible types: Integer cannot be converted to byte
      out = ((byte) ((bucket).dtor_value()));
                    ^
1 error

What happened?

Should compile, but a workaround is to write (bucket.value as int) as uint8.

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

Mac

[RustanLeino]

The problem in the target code seems to be that it's missing a cast from Java's java.lang.Integer (which is the type of the value stored in the bucket) to Java's int, which is required before doing the cast to Java's byte.

A workaround is to first assign bucket.value to a variable of type uint32, which lets the target code rely on Java's automatic conversion from java.lang.Integer to int.

Using two statements:

var w := bucket.value;
out := w as uint8;

Or using a let expression:

out := var w := bucket.value; w as uint8;