Fix: Use correct type for map update expression

[MikaelMayer]

This PR fixes #3059
The solution was similar to the one implemented in #2059
It consists in not setting the type of the expression m[k := v] as the same type of m, but as the partially resolved type of m (whatever this means, I just took the code in other branches).
I added a corresponding test.

This PR also introduces the command-line argument --nonzero-exit-code-if-errors set by default to true so that we can use the new Dafny CLI with %baredafny verify %args_0 for files that are supposed to fail.

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

[MikaelMayer]

@keyboardDrummer yay ! we can use the new CLI for tests now.

[cpitclaudel]

This does not look right to me — there's no member selection here. Instead, shouldn't we just revert to the base type? (e.Seq.Type with the constraints removed?)

[MikaelMayer]

We can't because at this point the type are not resolved. We first need to resolve identifier names (such as "foo"), hence the need to "partially resolve")

[cpitclaudel]

It's a bit uncommon to have such a flag. Shouldn't we find another solution in the test suite itself?

[MikaelMayer]

We already have this option in a substantial portion of our 1400+ tests, whenever you have %dafny_0, it means you have this flag.
Since %baredafny verify only takes new arguments, we need to expose this option to make it work.
I don't know of another simple way.

What we could do is hide this option to users, but I don't know how to do that. @keyboardDrummer ?

[cpitclaudel]

But the description of that flag says "deprecated" in the old CLI:

  /countVerificationErrors:<n>
      (deprecated)
      0 - Set exit code to 0 regardless of the presence of any other errors.
      1 (default) - Emit usual exit code (cf. beginning of the help message).

[cpitclaudel]

I think for this test we should just use the old CLI. And we can then (in a separate PR) enhance LitTests.cs to accept || true at the end of a command line, which is the "right" way to ignore an exit code. WDYT?

[RustanLeino]

The proposed fix does not eliminate the problem. Here is an example where it remains:

type foo = m: map<int, int> | forall n <- m.Keys :: m[n] < 5

method addToFoo() returns (r: foo)
  ensures false
{
  var m; // The type of m is to be inferred, but that won't happen until
         // after type inference has processed the assignment to r.
  r := m[1 := 7];
  // To trigger the unsoundness, the verifier needs to be reminded that
  // r is a variable of type foot. That is done by the following little
  // trick:
  ghost var u := RecoverType(r);
}

function RecoverType(a: foo): foo { a }

As @cpitclaudel says above, we'd like to revert to the base type. The problem is that we can't get that directly from expr.Type, because the type may not have been resolved yet. I think the way to fix this problem is to create two new type proxies (call them resultKeyType and resultValueType) and set expr.Type to a new MapType using those two type proxies as type arguments. Then, add a constraint that expr.Type is a subtype of that new MapType.

[fabiomadge]

Suggested change

	var ty = PartiallyResolveTypeForMemberSelection(expr.tok, e.Seq.Type);
	expr.Type = ty;
	expr.Type = PartiallyResolveTypeForMemberSelection(expr.tok, e.Seq.Type);

[cpitclaudel]

I think the way to fix this problem is to create two new type proxies (call them resultKeyType and resultValueType) and set expr.Type to a new MapType using those two type proxies as type arguments. Then, add a constraint that expr.Type is a subtype of that new MapType.

That would be nice, but it's not that simple (I think?): we don't know yet that m is a map, either. At that point in the program all we know is that is should satisfy SeqUpdatable. But I think InferredTypeProxys drop constraints by default, so wouldn't that do?

[MikaelMayer]

The proposed fix does not eliminate the problem. Here is an example where it remains:

I just tested Clement's fix against your example and it worked.