Fix: null pointer exception in the case of hovering local variables

[MikaelMayer]

Fixes #2438

• The variables are not cloned, but stay linked. That way, hovering them works.
• I added a robustness check on the type to avoid the following problem: when hovering such variable, the IDE jumps to the internal error/crash, so it's disruptive when working on something that is not related to the hovering.

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

[fabiomadge]

I'm somewhat hesitant about this change. We should probably come up with a different name and comment, if you really just want to clone part of it. What about CloneRBranchExpr? Also, the tests fail.

[MikaelMayer]

Yes :-(

[MikaelMayer]

I'm somewhat hesitant about this change. We should probably come up with a different name and comment, if you really just want to clone part of it. What about CloneRBranchExpr? Also, the tests fail.

I just pushed a more conservative version of the changes which prevent local variables from being cloned if their type is not yet assigned, that way, any type assigned later on a local variable of a cloned tree will make the original local variable (which is the same) have the same type.

[fabiomadge]

It's still not clear to me that this is safe. Couldn't we re-infer the type on all branches? Would you mind soliciting someone else's review?

[MikaelMayer]

Ok, that's fair to ask. I'm very much puzzled by the code that deals with nested match statements. Let me ask @RustanLeino

[fabiomadge]

Suggested change

	return new RBranchStmt(branch.Tok, branch.BranchID,
	branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)), new List<Statement>(branch.Body), cloner.CloneAttributes(branch.Attributes));
	return new RBranchStmt(branch.Tok, branch.BranchID, branch.Patterns.ConvertAll(x => cloner.CloneExtendedPattern(x)),
	new List<Statement>(branch.Body), cloner.CloneAttributes(branch.Attributes));

[RustanLeino]

Is the following correct? The user hovers over the local variable, then the language server finds the cloned variable. The cloned variable at that time has no .type filled in, and this caused the crash?

The way NestedMatchStmt and NestedMatchExpr work today is that they are desugared by the resolver into simpler MatchStmt and MatchExpr AST nodes. I presume that's where the clone operation (which in this PR has been changed to the special cloner) happens. I'm wondering which one (NestedMatch... or Match...) is used by the language server's look-up. Could it be that the sugared match has the .type filled in, but the desugared one does not, or perhaps vice versa? If so, then a possible fix would be to change where the language server looks up this variable.

[MikaelMayer]

Is the following correct? The user hovers over the local variable, then the language server finds the cloned variable. The cloned variable at that time has no .type filled in, and this caused the crash?

If by "cloned variable" you mean "the original variable before it was cloned", then your interpretation is correct.

Could it be that the sugared match has the .type filled in, but the desugared one does not, or perhaps vice versa?

It's the second time that I observe that the sugared match does not have .type filled in, but the desugared one has it.

I think your approach for the LSP would work (to look up for the desugared version and collect symbols there instead of the original NestedMatchStmt). But that fix alone has some problems. For compilers that don't rely on the desugaring (e.g. DafnyLite), they don't have access to the resolved type of local variables, which is problematic.

[RustanLeino]

Could it be that the sugared match has the .type filled in, but the desugared one does not, or perhaps vice versa?

It's the second time that I observe that the sugared match does not have .type filled in, but the desugared one has it.

I think your approach for the LSP would work (to look up for the desugared version and collect symbols there instead of the original NestedMatchStmt). But that fix alone has some problems. For compilers that don't rely on the desugaring (e.g. DafnyLite), they don't have access to the resolved type of local variables, which is problematic.

This may be okay for now. We've seen several issues with the fact that the desugaring happens here (as opposed to keeping the original "nested" match), so I predict we'll rewrite this in the near future.