From be0787499fd4ae849a8ddf771e2f0f65754a5b67 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 16 Feb 2024 16:26:11 +0100 Subject: [PATCH] Do not crash when required parameters occur after optional ones (#5074) Fixes #4809 ### Description Do not crash when required parameters occur after optional ones ### How has this been tested? Added a littish test By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../NameResolutionAndTypeInference.cs | 6 ++---- .../Resolver/PreType/PreTypeResolve.ActualParameters.cs | 6 ++---- .../LitTests/LitTest/ast/defaultParameterResolution.dfy | 7 +++++++ .../LitTest/ast/defaultParameterResolution.dfy.expect | 2 ++ .../ast/defaultParameterResolution.dfy.refresh.expect | 3 +++ .../LitTests/LitTest/dafny0/DefaultParameters.dfy | 2 +- docs/dev/news/4809.fix | 1 + 7 files changed, 18 insertions(+), 9 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.refresh.expect create mode 100644 docs/dev/news/4809.fix diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index dbab944825b..df58fb647c3 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -3341,16 +3341,14 @@ void ResolveActualParameters(ActualBindings bindings, List formals, ITok substMap.Add(formal, n); } else { // parameter has no value - if (onlyPositionalArguments) { - // a simple error message has already been reported - Contract.Assert(simpleErrorReported); - } else { + if (!simpleErrorReported) { var formalDescription = whatKind + (context is Method ? " in-parameter" : " parameter"); var nameWithIndex = formal.HasName && formal is not ImplicitFormal ? "'" + formal.Name + "'" : ""; if (formals.Count > 1 || nameWithIndex == "") { nameWithIndex += nameWithIndex == "" ? "" : " "; nameWithIndex += $"at index {formalIndex}"; } + var message = $"{formalDescription} {nameWithIndex} requires an argument of type {formal.Type}"; reporter.Error(MessageSource.Resolver, callTok, message); } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs index b8b0a8dd331..6b6a9af13a9 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs @@ -139,16 +139,14 @@ void ResolveActualParameters(ActualBindings bindings, List formals, ITok substMap.Add(formal, n); } else { // parameter has no value - if (onlyPositionalArguments) { - // a simple error message has already been reported - Contract.Assert(simpleErrorReported); - } else { + if (!simpleErrorReported) { var formalDescription = whatKind + (context is Method ? " in-parameter" : " parameter"); var nameWithIndex = formal.HasName && formal is not ImplicitFormal ? "'" + formal.Name + "'" : ""; if (formals.Count > 1 || nameWithIndex == "") { nameWithIndex += nameWithIndex == "" ? "" : " "; nameWithIndex += $"at index {formalIndex}"; } + var message = $"{formalDescription} {nameWithIndex} requires an argument of type {formal.Type}"; ReportError(callTok, message); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy new file mode 100644 index 00000000000..350760d2978 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy @@ -0,0 +1,7 @@ +// RUN: %testDafnyForEachResolver "%s" --expect-exit-code=2 + +function SumFromTo(sequence: nat -> real, start: nat := 0, end: nat): real + +function PartialSums(sequence: nat -> real): nat -> real { + (n: nat) => SumFromTo(sequence, n) +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.expect new file mode 100644 index 00000000000..4391e6e3405 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.expect @@ -0,0 +1,2 @@ +defaultParameterResolution.dfy(6,23): Error: function parameter 'end' at index 2 requires an argument of type nat +1 resolution/type errors detected in defaultParameterResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.refresh.expect new file mode 100644 index 00000000000..a4303115875 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.refresh.expect @@ -0,0 +1,3 @@ +defaultParameterResolution.dfy(3,59): Error: a required parameter must precede all optional parameters +defaultParameterResolution.dfy(6,23): Error: function parameter 'end' at index 2 requires an argument of type nat +2 resolution/type errors detected in defaultParameterResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy index 3f161d37a21..ad5ff33c388 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy @@ -600,4 +600,4 @@ module ExtremeNat { lemma TestLeastZero(y: int, z: int, v: int, w: int, a: int, b: int, o: nat) { assert Q#[o](b); // error: does not hold for o == 0 } -} +} \ No newline at end of file diff --git a/docs/dev/news/4809.fix b/docs/dev/news/4809.fix new file mode 100644 index 00000000000..a71ea9febec --- /dev/null +++ b/docs/dev/news/4809.fix @@ -0,0 +1 @@ +Dafny no longer crashes when required parameters occur after optional ones. \ No newline at end of file