Chore: Fixed a spurious CI failure

[MikaelMayer]

Description

I recently stumbled on this random Mac failure:
https://github.com/dafny-lang/dafny/actions/runs/10359400713/job/28675744622?pr=5684 After careful investigation of the stack trace, it looks like the static constructor of DafnyFile did not run before OptionRegistry.CheckOptionsAreKnown(AllOptions);, resulting in the option DoNotVerifyDependencies to not be registered. This PR fixes that by forcing the execution of the static DafnyFile constructor, guaranteed to not run if that constructor was already called. https://learn.microsoft.com/en-us/dotnet/api/system.runtime.compilerservices.runtimehelpers.runclassconstructor?view=net-8.0

How has this been tested?

I can't think of a way this change can be tested, the failure happens extremely rarely. Please make yourself convinced that this PR solves the issue given in the link.

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

Doubts

[keyboardDrummer]

I don't understand how the exception you linked to in the PR details, and the new exception that this PR build triggers (https://github.com/dafny-lang/dafny/actions/runs/10361859583/job/28683650633?pr=5685), could ever occur. The option DoNotVerifyDependencies is declared in the same file as in which it is registered, so this option can not be referenced without triggering the static constructor that registers it.

Maybe the real issue is that the dictionaries in OptionRegistry are not concurrent, and they are losing entries because multiple items are added concurrently.

[MikaelMayer]

I looks like the CI identified another similar issue.
Here is why I'm very confident that this PR fixes both the one I identified, and the other one you identifier.

The exception that is thrown comes from OptionRegistry.CheckOptionsAreKnown(AllOptions);, which is called only in DafnyNewCli.cs after a set of AddCommand(), each command registering the options into OptionScopes.
That check looks like this:

   var unsupportedOptions = allOptions.ToHashSet()
      .Where(o =>
        !OptionScopes.ContainsKey(o))
      .ToList();
    if (unsupportedOptions.Any()) {
      throw new Exception($"Internal error - unsupported options registered: {{\n{string.Join(",\n", unsupportedOptions)}\n}}");
    }

Note the OptionsScope.

On DafnyFile, there is a static initialization code:

  static DafnyFile() {
    OptionRegistry.RegisterGlobalOption(DoNotVerifyDependencies, OptionCompatibility.OptionLibraryImpliesLocalError);
  }

that is actually assigning OptionScopes[option] = OptionScope.Global;, so if that code was run before the check, it should have succeeded. This demonstrate that the static code of DafnyFile is not always executed before the code that check that all used options are registered.

I hope this helps!

[MikaelMayer]

Update: I realized there were many many more cases with RegisterOption and RegisterGlobalOption. I updated the PR to fix them all and also add a comment on static constructors so that if ever one wants to do the same, they will see this comment and hopefully update the code in DafnyNewCli.cs.
But overall, I realize that migrating options into static constructors is not a good refactoring as there is no guarantee of ordering in static constructors. Still, let's fix that for now.

[MikaelMayer]

Update: Seems like the calls using reflection did not work. Using real calls to ensure options are correctly registered, but without async issues.

[keyboardDrummer]

so if that code was run before the check, it should have succeeded.

As I mentioned before, I don't draw that conclusion. Because of the way static initialization works, I do think the registration was run before the check. What can explain the failures is that the assignment OptionScopes[option] = OptionScope.Global; failed due to a concurrent assignment to the same dictionary, which caused at least one of the multitude of assignments to be forgotten.

While I do think the changes in this PR resolve the issue, since they prevent the concurrent registrations, I think a simpler and more future proof solution is to make the dictionaries in OptionsRegistry a ConcurrentDictionary

[keyboardDrummer]

_

[MikaelMayer]

failed due to a concurrent assignment to the same dictionary, which caused at least one of the multitude of assignments to be forgotten.

Oh that's a brilliant observation too, now it makes sense to me. Let's try this simple fix first and see whether the issue reappears. I've force pushed it to this branch.

[keyboardDrummer]

Updated the doo files and (sorry) snuck in a Boogie update

[MikaelMayer]

The boogie update changed the count of verifiable, which failed everything.
Maybe it's worth separating the PR in two?

[keyboardDrummer]

The boogie update changed the count of verifiable, which failed everything. Maybe it's worth separating the PR in two?

Jep, sorry.