Fix static analysis and code actions

[MikaelMayer]

Fixes #5962

Description

This commit removed one optimization that was gathering declaration and assignment in a single assignment in the Dafny intermediate representation. That is, before that commit, this piece:

[ DeclareVar(name, typ, None), Assign(name, rhs)]

was combined into a single

DeclareVar(name, typ, Some(rhs))`

before being translated to Rust.
The commit above removed that optimization because it can detect that "name" is going to be immediately assigned, and give it a type without Maybeplacebo tracking (that tracks whether the variable was assigned at all). And when optimizing the resulting Rust code, a declaration followed by an assignment is combined into a single statement.

It seems for some reason that the Rust optimization was not applied in the problem reported in #5962. I could not reproduce it, but because I recognized that the optimization was not applied, I decided to reinstate the optimization on the Dafny AST level itself.
Note that the splitting between the declaration and the assignment is an artefact from the code generator. Dafny declare and assign are stored in two different statements, which prevents shadowing variables. Indeed, the following two pieces of code are not equivalent. The first one is what Dafny resolves to, the second one is what users write:

var name: int;
name := name + 2;

and

var name: int := name + 2;

In the second case, the name refers to the variable name before itself, whereas in the first case, the name is not assigned.
All other backends than Dafny-based backends add counters to variables to disambiguate them. However, the Rust code generator has decent shadowing rules so it makes sense to compile the Dafny
If the rhs contained "name", in Dafny it referred to a previous eponymous variable. In Rust as well. However, in the intermediate representation, since it does not add unique counters to variables, the second one is translatable in Rust whereas the first one is not:

let mut name: DafnyInt := name + int!(2);

By reinstating this optimization on the Dafny intermediate representation, it should make the code generation more robust in the future.

The second error commit introduced was that the static analyzer was faulty in the case of if-then-else statements, as it would forget the part after the if-then-else block and wrongly infer that a variable was not assigned when it was actually unknown.
I fixed the analyzer the following way:

• I wrote a test case that was failing
• I fixed the analyzer.

Then, in an effort to make everything more robust,

• I created a simple "by method" part of the function so that it would not need to extract subsequences and also could compute the function lazily, only when it needs more information
• Once the by method passed, I modified the specification part so that I would clearly separate 1) the part that analyzes the current statement, if it assigns the variable and/or if it's a stop statement, and 2) the continuation of the analysis on the rest of the sequence;

The function still matched the method body so I'm now pretty much more confident of the analysis.

This PR also adds two more fixes in code actions I needed to figure out termination

• The key for storing code action was not the same as the key for retrieving it in a file system where one folder contained a space. The first one was correct, but the second one was based on an URI converted to JSON without going through string, so it contained a %20. This means that no code actions could work when working with such files. By ensuring the key is the same for both the cache storage and the client, the code actions work again
• The insertion point of a code action was wrong. I reproduced the issue on a small test case, and fixed it.

How has this been tested?

• For the first issue, I temporarily deactivated the expression optimization to reproduce the exact issue on an existing test case (datatypes.dfy). I fixed it and verified it worked, and then put again the expression optimization.
• I added a test in DefsCoverage for the second issue
• I added an intermediate variable for the key so that we ensure it's the same in both places.
• I added a code action test for the fourth issue

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[alex-chew]

Thanks for the quick fixes!

[alex-chew]

Relying on this implementation detail of the Dafny IR makes me a little uneasy, but if the implementation changes then the tests you added should catch it, so I think it's a reasonable fix.

Would it make sense for the Dafny IR to represent this case more explicitly, in case we want to use shadowing like this for other backends?

[MikaelMayer]

I think it would make sense for the DafnyCodeGenerator to emit Dafny IR that is suitable for shadowing immediately, that is, do not separate the declaration and the assignment upfront. But that's a bit difficult given the current way it's piggy backing on other code generators. However, that'd be the right thing to do, so that we could remove this "optimization". Thanks for your concern.