Counterexamples - fix integer parsing bug and improve code quality #2461
Conversation
| @@ -137,7 +139,7 @@ public class DafnyModel { | |||
| } else if (fn.Name.StartsWith("#") && fn.Name.IndexOf('.') != -1 && fn.Name[1] != '#') { | |||
| foreach (var tpl in fn.Apps) { | |||
| var elt = tpl.Result; | |||
| datatypeValues.Add(elt, tpl); | |||
| datatypeValues[elt] = tpl; | |||
There was a problem hiding this comment.
Before, you would be ensuring an exception if the element already existed. Can you please explain me why you are confident we don't need to check this?
There was a problem hiding this comment.
Type aliasing can lead to an element being associated with different datatype functions in the Model so we should not be throwing exceptions in this case. My goal is also to prevent exceptions from arising as much as possible - in some cases, for instance, the tool might not be able to figure out the type of a variable and return UnknownType but this will not break the execution and some counterexample will still be extracted, even if a portion of it will not have complete information.
On related note, would VSCode extension crash if there were an exception in counterexample extraction? I am not aware of any situations in which this would happen (aside from the ones I fix in this PR) but adding a try-catch somewhere might still make sense to prevent issues in the future. Do you know what’s the best place for this would be?
There was a problem hiding this comment.
If the language server crashes because of an unhandled exception, many times the VSCode extension will not be responsive anymore.
So I understand why you want to avoid crashes and I'm with you on this refactoring.
I'm just wondering whether if you could store the information somewhere if for any reason the same key was assigned two different values. At least for example, in a log file, or at best in some log message about the counter-example sent via the counterexample API (so that it's easier to debug, and to handle later when the UI for counterexamples will change). I think the log file would be fine.
In general it's better to add the try-catch to the closest place where the exception might be thrown, if not, where it makes the most sense.
There was a problem hiding this comment.
Adding a logging functionality would make sense! I would keep that separate from this PR, if possible, but I already have some logging functionality for test generation on my fork, so I might be adding it in the near future.
Co-authored-by: Mikaël Mayer <[email protected]>
Co-authored-by: Mikaël Mayer <[email protected]>
Co-authored-by: Mikaël Mayer <[email protected]>
|
Thank you, @MikaelMayer! Have adopted the changes. |
|
Have now fixed all nullability warnings. Let me know if you would like me to make any other changes! |
|
Thank you, @MikaelMayer! I don't add any new functionality, so it shouldn't break anything. |
This pull request does not add any new functionality to counterexamples but instead makes several code quality improvements and bug fixes. Here is a summary:
Microsoft.Dafny.Typein place ofDafnyModelTypeto improve readability and reduce the amount of string processing.I also added relevant tests and made a change to test generation to support the move from DafnyModelType to Microsoft.Dafny.Type
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.