Feature request: verify resolved methods even if other methods can't be resolved

[cpitclaudel]

Making modifications to a large Dafny file (e.g. changing a datatype definition) will often break many functions (e.g. all the functions that match on a changed datatype).

Right now Dafny forces users to first fix all resolution errors, and then fix all verification errors. This is not an ideal process: fixing resolution for a broken function requires me to understand what it does, and so does fixing verification, so I'd prefer to do both at the same time. Otherwise by the time I'm done fixing all resolution errors I need to go back to functions that I fixed resolution for much earlier, and by that point I've lost the relevant context.

method incorrect() {
  assert false; // Not reported until the error below is fixed.
}

method unresolvable() {
  assert true + 1;
}

[MikaelMayer]

How would you interpret a call to an unresolvable method?

[cpitclaudel]

How would you interpret a call to an unresolvable method?

You wouldn't: in this proposal you would verify fully resolved methods and report resolution errors for other methods.

[MikaelMayer]

That's VERY interesting now, but we might have to split the resolving phase for that. To figure out if a method depends on an unresolvable method, you still have to resolve some symbols, right? Assuming we can do this. it would be now definitely doable, because if we verify a given method, only its direct dependencies (including methods and functions it calls) are actually sent to the solver, if I'm not mistaken, right @keyboardDrummer ?

[cpitclaudel]

To figure out if a method depends on an unresolvable method, you still have to resolve some symbols, right?

To figure out if M1 depends on M2, you need to fully resolve the body of M1, and see if it (transitively) mentions M2. You don't need M2 to be resolved to do that :)

if we verify a given method, only its direct dependencies (including methods and functions it calls) are actually sent to the solver, if I'm not mistaken

I think that's right!

[MikaelMayer]

In this case, here is something you could do to figure out which methods do not have transitive resolution errors, which would not impact performance, so that it would make it possible to launch verification only on them. 1) You could add three boolean fields ResolutionStarted, ResolutionFinished and HasTransitiveResolutionErrors to methods, set to false by default. Alternatively, you could store them in three dictionaries set for that purpose. 3) At the beginning of the same Resolver.ResolveMethod if ResolutionStarted is true, you immediately return 4) Right after, you add ResolutionStarted = true so that you prevent recursive loops. 5) At the end of the method resolution, you add ResolutionFinished = true and set HasTransitiveResolutionErrors to true if the number of errors between the beginning and the end of the method is different. 2) Every time a method call symbol is resolved, we call Resolver.ResolveMethod(m) immediately on it In Resolver.ResolveMethod,

An alternative is to inspect the resolution report and try to see if there are errors in methods, but that would require to compute the graph of transitivity again.

In the language server or in DafnyDriver, after resolution, even if there are errors, we would detect if there are methods that do not have errors, and if so, continue with verification on them.