Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[Dafny-to-Rust] Avoir using MaybePlacebo when assignments are straigh…
…tforward (#5959) ### Description Given the following dafny file ```dfy method Test(i: int) returns (j: int) { j := i; } method Main() { var j := Test(1); var k := Test(j); } ``` the Dafny to Rust code generator used to produce this: ```rs pub fn Test(i: &DafnyInt) -> DafnyInt { let mut j = MaybePlacebo::<DafnyInt>::new(); j = MaybePlacebo::from(i.clone()); return j.read(); } pub fn Main(_noArgsParameter: &Sequence<Sequence<DafnyChar>>) -> () { let mut j = MaybePlacebo::<DafnyInt>::new(); let mut _out0 = MaybePlacebo::<DafnyInt>::new(); _out0 = MaybePlacebo::from(_default::Test(&int!(1))); j = MaybePlacebo::from(_out0.read()); let mut k = MaybePlacebo::<DafnyInt>::new(); let mut _out1 = MaybePlacebo::<DafnyInt>::new(); _out1 = MaybePlacebo::from(_default::Test(&j.read())); k = MaybePlacebo::from(_out1.read()); return (); } ``` While Dafny lets users declare a variable while assigning it conditionally, Rust does not support this pattern as it needs to know if the variable was assigned so that it can deallocate it. The current solution supports all cases. It uses `MaybePlacebo`, a synonym of the Option type, so that we can declare a placebo holder even if the type does not implement the `Default trait` (looking at you, functions). However, this encoding is still tracking a boolean, and furthermore, it makes the code harder to read and debug. With this PR, Dafny performs static analysis of assignments, determine that the variables will be surely assigned, and is able to determine at the declaration of the yet undefined variable if it's going to be surely assigned or surely not assigned. In either case, it removes the MaybePlacebo wrapper. This works for output variables of method calls, as well as variables declared but not defined. ```rs pub fn Test(i: &DafnyInt) -> DafnyInt { let mut j: DafnyInt = i.clone(); return j.clone(); } pub fn Main(_noArgsParameter: &Sequence<Sequence<DafnyChar>>) -> () { let mut j: DafnyInt; let mut _out0: DafnyInt = _default::Test(&int!(1)); j = _out0.clone(); let mut k: DafnyInt; let mut _out1: DafnyInt = _default::Test(&j); k = _out1.clone(); return (); } ``` There are still a few clones and one day we might be able to get rid of the intermediate variable, but this is out of scope for this PR. ### How has this been tested? - The test above has been added - The behavior of determining assignment status has a thorough new test executed from `DafnyCore.Test` <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
- Loading branch information
1 parent
de81b69
commit bf1aac6