Bad Rust code generated when local variable shares name with return variable.

[ajewellamz]

Dafny version

4.10 and also HEAD of master

Code to produce this issue

https://github.com/aws/aws-database-encryption-sdk-dynamodb/

Command to run and resulting output

clone https://github.com/aws/aws-database-encryption-sdk-dynamodb/
cd DynamoDbEncryption
make polymorph_rust transpile_rust test_rust
note that test_rust successfully compiles

Edit the file dafny/DynamoDbEncryption/src/FilterExpr.dfy
In the definition of apply_function on line 1267 (or so) change
returns (result : Result<StackValue, Error>)
to
returns (ret : Result<StackValue, Error>)

make transpile_rust test_rust
note that test_rust does not compile, even though it should, and in fact does in all the other languages.

It seems that code on 1274 that starts
var ret :- 
confuses Dafny, in that the variable has the same name as the return variable

What happened?

Generated rust code does not compile.
I expected it to compile, or at a minimum Dafny should have complained at transpilation time.

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

Mac

[MikaelMayer]

I was able to reproduce it with this minimal example:

datatype Option<T> = None | Some(i: T)
{
  predicate IsFailure() { None? }
  function PropagateFailure<U>(): Option<U> requires IsFailure() { None }
  function Extract(): T requires !IsFailure() { i }
}

method TwoVar(i: int) returns (ret: Option<int>) {
  if i % 2 == 0 {
    var ret :- Some(Some(1));
    return Some(ret.i);
  }
  return None;
}

[MikaelMayer]

Even shorter example without elephant operator.

method TwoVars() returns (ret: int)
  ensures ret == 1
{
  {
    var ret := true;
    return if ret then 1 else 0;
  }
}
method Main() {
  var ret := TwoVars();
  print ret, "\n";
}