Closed ajewellamz closed 2 days ago
Thanks for the report; do you mind showing the output without the {:tailrecursion}
attribute? The variable capture may happen due to that optimization.
The output is exactly the same.
This is expected, because all {:tailrecursion}
does is throw an error if tail recursion isn't possible.
(Documenting for anyone watching) workaround: assign a fresh name to shortMap
in the else
branch
Among all possible solutions, I found that this one works pretty straightforward. We change the recursive name variable to unique names independent of the parameter names, and then we assign the parameter names at the beginning of the loop.
1 #![allow(warnings, unconditional_panic)]
2 #![allow(nonstandard_style)]
3
4 pub mod _module {
5 pub struct _default {}
6
7 impl _default {
8 pub fn GetMaps(opts: &::dafny_runtime::Sequence<::dafny_runtime::DafnyChar>, shortMap: &::dafny_runtime::Map<::dafny_runtime::DafnyChar, ::dafny_runtime::Sequence<::dafny_runtime::DafnyChar>>) -> ::dafny_runtime::Map<::dafny_runtime::DafnyChar, ::dafny_runtime::Sequence<::dafny_runtime::DafnyChar>> {
9 let mut _r0 = opts;
10 let mut _r1 = shortMap;
11 'TAIL_CALL_START: loop {
11bis let opts = _r0;
11ter let shortMap = _r1;
12 if opts.cardinality() == ::dafny_runtime::int!(0) {
13 return shortMap.clone();
14 } else {
15 let mut shortMap: ::dafny_runtime::Map<::dafny_runtime::DafnyChar, ::dafny_runtime::Sequence<::dafny_runtime::DafnyChar>> = shortMap.update_index(&opts.get(&::dafny_runtime::int!(0)), &::dafny_runtime::string_of("spoo"));
16 let mut _in0: ::dafny_runtime::Sequence<::dafny_runtime::DafnyChar> = opts.drop(&::dafny_runtime::int!(1));
17 let mut _in1: ::dafny_runtime::Map<::dafny_runtime::DafnyChar, ::dafny_runtime::Sequence<::dafny_runtime::DafnyChar>> = shortMap.clone();
18 _r0 = _in0.clone();
19 _r1 = _in1.clone();
20 continue 'TAIL_CALL_START;
21 }
22 }
23 }
24 }
25 }
The rationale is the following:
Dafny version
latest feat-rust
Code to produce this issue
Command to run and resulting output
What happened?
Line 10 declares shortMap, which is the return value.
Line 15 declares a shadowing shortMap.
Line 19 updates the shadow defined on line 15, not the "real" one defined on line 10.
Then the function returns an empty map, instead of one with data in it.
What type of operating system are you experiencing the problem on?
Mac