Improve error message locations for function calls and call arguments

[keyboardDrummer]

What was changed?

Added a method for updating test expect files based on CI output. This is contained in the C# project Scripts

Call arguments

Errors that relate to call arguments are reported on the argument, instead of on the (.

Example:

r := new C<char>.Orig('h'); // error incorrect argument type for constructor 
                            // in-parameter 'x' (expected X, found char)
                      ^ new location
                 ^ old location
                     

Function calls

Errors that relate to function or method calls are now consistently reported on the (. This was already done for method calls, while for function calls the error was reported on the center of the callee expression. It's better to report on the (, to distinguish from errors in computing the callee, which are reported on the center of the callee expression.

Example:

ghost const objs: set<object> := getObjs()
                                        ^ new location
                                 ^ old location
// Error: insufficient reads clause to invoke function

Assertions

Currently, errors about assertions (assert/ensure/invariant) are reported on the center of the condition. Since this PR changes the center of expressions that call functions, the locations for 'assertion might not hold' can change as well. Example:

assert !Even(N(17));
        ^^^^|^^^^^^ new origin
        |^^^ previous origin
// Error: assertion might not hold

Another example:

ensures Pos(UpIList(n))
           ^ new location
        ^ old location
// Related location: this is the postcondition that could not be proved

How has this been tested?

• Updated existing tests

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

[MikaelMayer]

Can you please clarify the following example:

assert !Even(N(17));
            ^ new location
       ^ previous location
// Error: assertion might not hold

I think that, in the case of negation, the error location cannot be anywhere else than the negation operator.
!A is equivalent to A ==> false and what can't be proved is false, not A which is an assumption.

[MikaelMayer]

It think it's a great idea.
Could you please add a section about the supported commands as well and briefly what they do?

[keyboardDrummer]

You can get that documentation by running dotnet run --project Source/Scripts/Scripts.csproj -- --help:

Description:
  Various scripts that help develop Dafny

Usage:
  Scripts [command] [options]

Options:
  --version       Show version information
  -?, -h, --help  Show help and usage information

Commands:
  update-expect-files <fileinfo>  Use the 'log archive' file downloaded from CI to update the integration tests

and you can do:

% dotnet run --project Source/Scripts/Scripts.csproj -- update-expect-files --help
Description:
  Use the 'log archive' file downloaded from CI to update the integration tests

Usage:
  Scripts update-expect-files <fileinfo> [options]

Arguments:
  <fileinfo>

Options:
  -?, -h, --help  Show help and usage information

[MikaelMayer]

Nice. It would be great if you could make this command available on the main makefile, like make script name=X or similar.

[keyboardDrummer]

Can you please clarify the following example:

assert !Even(N(17));
            ^ new location
       ^ previous location
// Error: assertion might not hold

I think that, in the case of negation, the error location cannot be anywhere else than the negation operator. !A is equivalent to A ==> false and what can't be proved is false, not A which is an assumption.

That's because of how splitting of ! is implemented in Dafny:

        case UnaryOpExpr opExpr: {
            var e = opExpr;
            if (e.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot) {
              var ss = new List<SplitExprInfo>();
              if (TrSplitExpr(context, e.E, ss, !position, heightLimit, applyInduction, etran)) {
                foreach (var s in ss) {
                  splits.Add(ToSplitExprInfo(s.Kind, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E)));
^ note the 's.E.tok' in the above line. 
                }
                return true;
              }
            }

            break;
          }

So assert 0:!(1:A || 2:B); will become 1: assert !A; 2: assert !B;. You could argue the diagnostics should have 0 as main location and 1 or 2 as a related location, but let's leave that for another PR.

[MikaelMayer]

Can you please clarify the following example:

assert !Even(N(17));
            ^ new location
       ^ previous location
// Error: assertion might not hold

I think that, in the case of negation, the error location cannot be anywhere else than the negation operator. !A is equivalent to A ==> false and what can't be proved is false, not A which is an assumption.

That's because of how splitting of ! is implemented in Dafny:

        case UnaryOpExpr opExpr: {
            var e = opExpr;
            if (e.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot) {
              var ss = new List<SplitExprInfo>();
              if (TrSplitExpr(context, e.E, ss, !position, heightLimit, applyInduction, etran)) {
                foreach (var s in ss) {
                  splits.Add(ToSplitExprInfo(s.Kind, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E)));
^ note the 's.E.tok' in the above line. 
                }
                return true;
              }
            }

            break;
          }

So assert 0:!(1:A || 2:B); will become 1: assert !A; 2: assert !B;. You could argue the diagnostics should have 0 as main location and 1 or 2 as a related location, but let's leave that for another PR.

Oh I better understand thanks to this example. I did not think of splitting. Thanks for the investigation and the precise details.
Now that I think of it, it feels to me that the reporting token is thus wrong, and this PR would be introducing a regression if we don't do anything, and I don't feel comfortable with that.
When expressions can't be proved and they are explicitly provided, modulo a split, I think it's crucial that there is no ambiguity regarding what is not proved, and omitting the not from the position would add to ambiguity.

Could you please replace this

s.E.tok

by

new NestedToken(s.E.tok, e.Tok, "Negation argument")

?
That would alleviate my fear of regression.

[keyboardDrummer]

Could you please replace this

s.E.tok

by

new NestedToken(s.E.tok, e.Tok, "Negation argument")

? That would alleviate my fear of regression.

But then we're being inconsistent between different logical operators in how we handle splits. Also, I don't think there would be a regression because we're currently not reporting on the !, but on the E. Sorry this was a mistake in the PR description. I've updated it.

Here's the actual change:

assert !Even(N(17));
        ^^^^|^^^^^^ new diagnostic location
        |^^^ previous diagnostic location
// Error: assertion might not hold

I'm happy to make the update you describe, but then let's do it for all operators and in a follow-up PR.

[MikaelMayer]

Ok if it's not a regression, let's go for it. Happy to review another PR to fix this8 split error positioning.

[MikaelMayer]

Nice. It would be great if you could make this command available on the main makefile, like make script name=X or similar.