Do not let 'null' children slip into the AST

dafny-lang / dafny

Dafny is a verification-aware programming language

https://dafny.org

Other

2.82k stars 253 forks source link

Do not let 'null' children slip into the AST #5446

Closed keyboardDrummer closed 2 days ago

keyboardDrummer commented 2 weeks ago

Fixes https://github.com/dafny-lang/dafny/issues/5357, https://github.com/dafny-lang/dafny/issues/4129

Description

Prevent null from being returned by Node.Children

How has this been tested?

Added IDE tests that contain the code from the bug reports
Added a test that slowly types a large Dafny program from our test suite, triggering code completion and hover on each stroke, to see whether there are other instances where Dafny server can crash.

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

keyboardDrummer commented 1 week ago

How do we make sure those new tests introduce new concurrency issues?

I'm not sure what you're asking. This PR does not relate to concurrency issues, so the tests are not testing for them. The test EditDocumentTest will check whether code completion and hover operations of the IDE still work for various broken program states, without crashing the IDE, and it does this by incrementally typing a correct program and invoking those operations after each addition.

fabiomadge commented 1 week ago

Sure, but is it the case that only the tests that explicitly test for concurrency issues cause the issues we frequently experience?

keyboardDrummer commented 1 week ago

Sure, but is it the case that only the tests that explicitly test for concurrency issues cause the issues we frequently experience?

No it's not.

Instability in tests is not limited to any particular test, and it can and does also occur outside of IDE tests. However, it most frequently occurs in IDE tests because the IDE has many concurrent parts. Instability in IDE tests usually comes from a bug in the IDE code, not the test, but sometimes also comes from the test. There are particular IDE tests that are more liable to instability, namely those that tests performance in some way. These tests generally only pass if a particular performance threshold is met, and will retry up to X times until they meet that threshold.

We protect ourselves against making changes, either in tests or in any other location, that cause IDE test instability, by running the IDE tests twice in the build. I think it would be good if we run them more often but obviously there's a trade-off there.

fabiomadge commented 1 week ago

That's probably a tangential discussion, but it seems to me that we have a decent idea about which PRs are more likely to introduce instability. Maybe we should try being more targeted about where we do repeat runs. If we do that, we could even afford doing more runs where necessary.