Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix static analysis and code actions (#5966)
Fixes #5962 ### Description This [commit](bf1aac6) 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: ```dafny [ DeclareVar(name, typ, None), Assign(name, rhs)] ``` was combined into a single ```dafny 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: ```dafny var name: int; name := name + 2; ``` and ```dafny 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: ```rs 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](bf1aac6) 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 <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
81b8216
commit 5666571