Improve definite assignment 4

[RustanLeino]

Fixes #3640

This PR fixes some issues with definite assignment and determinacy.

Recently, we changed the default rules for definite assignment in Dafny (PR #3052). The main change was to insist that all local variables and out-parameters be definitely assigned before they are used. This was followed up by PR #3311, which started considering := * assignments as fulfilling definite-assignment requirements. PR #3311 also fixed a point where #3052 had gone too far; with PR #3311, it is now again possible to allocate an array of an auto-init type without having to explicitly assign the array elements.

There was one more point where PR #3052 had gone too far (reported in #3640), and the present PR fixes that point. The issue regards fields of a class. The present PR once again allows fields to be auto-initialized (provided their types allow that).

This PR also makes /definiteAssignment:4 available in the legacy CLI. (Previously, it had been added internally, but not exposed in the legacy CLI.)

Finally, this PR reports an error in the --enforce-determinism mode for any class without a constructor. This was a latent omission in the previous checking. Together with once again allowing auto-initialization of fields, this change puts

class Cell { // constructor-less class not allowed with --enforce-determinism
  var data: int
}
method NondeterministicReturn() returns (r: int) {
  var c := new Cell;
  return c.data;
}

on the same footing as

class Cell {
  var data: int
  constructor () { // with --enforce-determinism, this constructor must initialize .data    
  }
}
method NondeterministicReturn() returns (r: int) {
  var c := new Cell();
  return c.data;
}

I argue this PR fixes the new definite-assignment mode in an important way and therefore should be included in Dafny 4.0.

The documentation (see, e.g., #3584) may need to be updated.

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

[davidcok]

To fix the failure of the build of DafnyRef.pdf, checkout the relevant branch, build dafny, cd to docs/DafnyRef, run make, and then commit any files that have changed, likely Options.txt

[RustanLeino]

@davidcok Confirming: Is this the definite-assignment issue you had mentioned in person?

[davidcok]

Partially at least. I guess in trying to explain auto-init and definite-assignment it seemed that the strict use of definite assignment (which is the default) made the existence of auto-init moot, as one had to initialize local variables explicitly anyway, auto-init or not. I still seems to me that the existence of an auto-init value for builtin types and for any type for which one can be inferred or a witness is explicitly given should mean that a declaration is implicitly definitely assigned to that value -- or is it that you don't want to impose such an initialization requirement on compiler backends or is it that the indefinite assignment is better for assuring correctness?

[robin-aws]

I'm worried that this (and previous PRs) are complicating the meaning of definite assignment inconsistently, doing a quick sanity check before it goes in.

[robin-aws]

Apologies for throwing a wrench in the works. My only ask is that we add some clarification to the reference manual (http://dafny.org/dafny/DafnyRef/DafnyRef#sec-definite-assignment) and the options documentation that these rules are specifically about variables and out-parameters only (?) and not all possible storage that a program could fail to initialize as it is construction. My confusion has sprung from assuming these rules apply to more program elements than they do, and it sounds like that's fine because this analysis ultimately just helps get better error messages rather than protecting against soundness.

[robin-aws]

I cut a follow up issue to improve the documentation, but I'm okay with this improvement going in.

Happy with follow up issue to improve documentation