Skip to content

Commit 688e7d0

Browse files
davidcokdavidcok
davidcok
and
davidcok
authored
Staging corrections to improved testing (#4106)
<small>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).</small> --------- Co-authored-by: davidcok <davidcok@github.com>
1 parent cda490c commit 688e7d0

16 files changed

+239
-113
lines changed

‎Source/DafnyCore/AST/Grammar/ParseErrors.cs

+60-5
Original file line numberDiff line numberDiff line change
@@ -10,28 +10,30 @@ public class ParseErrors {
1010

1111
public enum ErrorId {
1212
// ReSharper disable once InconsistentNaming
13-
g_include_has_errors, // In Reporting.cs
13+
none,
1414
p_generic_syntax_error,
15-
p_generic_semantic_error,
1615
p_duplicate_modifier,
1716
p_abstract_not_allowed,
1817
p_no_ghost_for_by_method,
1918
p_ghost_forbidden_default,
2019
p_ghost_forbidden,
2120
p_no_static,
2221
p_no_opaque,
23-
p_deprecated_attribute, // TODO
22+
p_deprecated_attribute,
2423
p_literal_string_required,
2524
p_no_leading_underscore,
2625
p_bitvector_too_large,
2726
p_array_dimension_too_large,
2827
p_superfluous_export,
2928
p_bad_module_decl,
29+
p_misplaced_least_or_greatest,
3030
p_extraneous_comma_in_export,
3131
p_top_level_field,
3232
p_bad_datatype_refinement,
3333
p_no_mutable_fields_in_value_types,
34+
p_module_level_always_static,
3435
p_const_decl_missing_identifier,
36+
p_module_level_const_always_static,
3537
p_bad_const_initialize_op,
3638
p_const_is_missing_type_or_init,
3739
p_misplaced_ellipsis_in_newtype,
@@ -127,14 +129,18 @@ public enum ErrorId {
127129
p_deprecated_modify_statement_with_block,
128130
p_deprecated_opaque_as_identifier,
129131
p_deprecated_semicolon,
132+
p_deprecated_this_in_constructor_modifies_clause,
130133
sc_malformed_pragma, // TODO no description is provided
131134
sc_unknown_pragma, // TODO no description is provided
132-
p_file_has_no_code, // TODO no description yet
135+
p_cli_option_error, // Has no description yet
136+
p_internal_exception,
137+
p_file_has_no_code,
138+
p_include_has_errors
133139
}
134140

135141
static ParseErrors() {
136142

137-
Add(ErrorId.g_include_has_errors,
143+
Add(ErrorId.p_include_has_errors,
138144
@"
139145
This error is shown when parsing a file A that includes another file B when B has errors of its own.
140146
Without this message it can be easy to miss the fact that other errors in A are in fact caused
@@ -248,6 +254,16 @@ Such an import would likely cause a circular module dependency error.
248254
OneAction("remove '" + range.PrintOriginal() + "'", range, "", true)
249255
});
250256

257+
Add(ErrorId.p_misplaced_least_or_greatest,
258+
@"
259+
A `least` or `greatest` token between `export` and `predicate` is a bit ambiguous:
260+
it can be either the name of the export set or associated with the `predicate` declaration.
261+
The parser associates it with the `export`. To avoid this warning, do not put the
262+
`least` or `greatest` token on the same line as the `predicate` token.
263+
If you intend for the `least` to go with the predicate, change the order of the
264+
declarations.
265+
"); // TODO - could use a quick fix
266+
251267
Add(ErrorId.p_extraneous_comma_in_export,
252268
@"
253269
An export declaration consists of one or more `reveals`, `provides`, and extends clauses. Each clause contains
@@ -276,12 +292,24 @@ It is only allowed to add members to the body of the datatype.
276292
`const` declarations can be members of value-types, such as datatypes.
277293
", Replace("const"));
278294

295+
Add(ErrorId.p_module_level_always_static,
296+
@"
297+
All names declared in a module (outside a class-like entity) are implicitly `static`.
298+
Dafny does not allow them to be explictly, redundantly, declared `static`.
299+
", Remove(true));
300+
279301
Add(ErrorId.p_const_decl_missing_identifier,
280302
@"
281303
This error arises from a truncated declarations of a const field, namely just a const keyword.
282304
To correct the error, add an identifier and either or both a type and initializing expression (or remove the const keyword).
283305
");
284306

307+
Add(ErrorId.p_module_level_const_always_static,
308+
@"
309+
All names declared in a module (outside a class-like entity) are implicitly `static`.
310+
Dafny does not allow them to be explictly, redundantly, declared `static`.
311+
", Remove(true));
312+
285313
Add(ErrorId.p_bad_const_initialize_op,
286314
@"
287315
Dafny's syntax for initialization of const fields uses `:=`, not `=`.
@@ -1052,6 +1080,17 @@ This error message is not reachable in current Dafny.
10521080
If it occurs, please report an internal bug (or obsolete documentation).
10531081
");
10541082

1083+
Add(ErrorId.p_deprecated_this_in_constructor_modifies_clause,
1084+
@"
1085+
The purpose of a constructor is to initialize a newly allocated instance of a class.
1086+
Hence it always modifies the `this` object.
1087+
Previously it was required to list `this` in the modifies clause of the
1088+
constructor to specify this property, but now `this` is always implicitly
1089+
a part of the modifies clause.
1090+
If the constructor only modifies its own object (as is the very common case)
1091+
then no explicit modifies clause is needed at all.
1092+
"); // TODO _ add a quick fix to remove the this, or maybe the whole clause
1093+
10551094
Add(ErrorId.p_bad_number_format,
10561095
@"
10571096
This error can only result from an internal bug in the Dafny parser.
@@ -1076,6 +1115,22 @@ and then passes that string to a library routine to create a BigDecimal.
10761115
Given the parser logic, that parsing should never fail.
10771116
");
10781117

1118+
Add(ErrorId.p_generic_syntax_error,
1119+
@"
1120+
This ""invalid something"" message where the something is typically
1121+
the name of an internal parser non-terminal means that the text being parsed
1122+
is a badly malformed instance of whatever parser entity was being parsed.
1123+
This is an automatically generated message by the CoCo parser generator
1124+
for a situation in which no specific recovery or a
1125+
more informative error message has been implemented.
1126+
1127+
The only advice we can give is to carefully scrutinize the location of the
1128+
error to see what might be wrong with the text. If you think this is a
1129+
common or confusing enough occurrence to warrant special error handling,
1130+
please suggest the improvement, with this sample code, to the Dafny team.
1131+
");
1132+
1133+
10791134
Add(ErrorId.p_deprecated_semicolon,
10801135
@"
10811136
Semicolons are required after statements and declarations in method bodies,

‎Source/DafnyCore/AST/Grammar/ProgramParser.cs

+3-2
Original file line numberDiff line numberDiff line change
@@ -230,8 +230,9 @@ protected virtual DfyParseResult ParseFile(DafnyOptions options, TextReader read
230230
val = string.Empty
231231
};
232232
var reporter = new BatchErrorReporter(options);
233-
reporter.Error(MessageSource.Parser, internalErrorDummyToken,
234-
"[internal error] Parser exception: " + e.Message);
233+
reporter.Error(MessageSource.Parser, ErrorId.p_internal_exception, internalErrorDummyToken,
234+
"[internal error] Parser exception: " + e.Message + (!options.Verbose ? "" :
235+
"\n" + e.StackTrace));
235236
return new DfyParseResult(reporter, null, new Action<BuiltIns>[] { });
236237
}
237238
}

‎Source/DafnyCore/Coco/Parser.frame

+5-18
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ public class Parser {
6565
errDist = 0;
6666
}
6767

68-
public void SemErr(ErrorId errorId, IToken tok, string msg) {
68+
public void SemErr(Enum errorId, IToken tok, string msg) {
6969
Contract.Requires(tok != null);
7070
Contract.Requires(msg != null);
7171
errors.SemErr(errorId, tok, msg);
@@ -167,14 +167,7 @@ public class Errors {
167167
return s;
168168
}
169169

170-
public void SemErr(IToken tok, string msg) { // semantic errors
171-
Contract.Requires(tok != null);
172-
Contract.Requires(msg != null);
173-
ErrorCount++;
174-
Reporting.Error(MessageSource.Parser, "", tok, msg);
175-
}
176-
177-
public void SemErr(ErrorId errorId, IToken tok, string msg) { // semantic errors
170+
public void SemErr(Enum errorId, IToken tok, string msg) { // semantic errors
178171
Contract.Requires(tok != null);
179172
Contract.Requires(msg != null);
180173
ErrorCount++;
@@ -187,22 +180,16 @@ public class Errors {
187180
Reporting.Error(MessageSource.Parser, errorId, uri, line, col, msg);
188181
}
189182

190-
public void Deprecated(ErrorId errorId, IToken tok, string msg) {
183+
public void Deprecated(Enum errorId, IToken tok, string msg) {
191184
Contract.Requires(tok != null);
192185
Contract.Requires(msg != null);
193186
Reporting.Deprecated(MessageSource.Parser, errorId, tok, msg);
194187
}
195188

196-
public void Deprecated(IToken tok, string msg) {
197-
Contract.Requires(tok != null);
198-
Contract.Requires(msg != null);
199-
Reporting.Deprecated(MessageSource.Parser, ErrorId.p_generic_semantic_error, tok, msg);
200-
}
201-
202-
public void Warning(IToken tok, string msg) {
189+
public void Warning(ErrorId errorId, IToken tok, string msg) {
203190
Contract.Requires(tok != null);
204191
Contract.Requires(msg != null);
205-
Reporting.Warning(MessageSource.Parser, ErrorId.p_generic_semantic_error, tok, msg);
192+
Reporting.Warning(MessageSource.Parser, errorId, tok, msg);
206193
}
207194

208195
} // Errors

‎Source/DafnyCore/Dafny.atg

+7-6
Original file line numberDiff line numberDiff line change
@@ -128,8 +128,8 @@ bool CheckAttribute(Errors errors, IToken attr, RangeToken range) {
128128
// attr is the identifier of the Attribute
129129
// range is from opening brace to closing brace
130130
if (attr.val == "ignore") {
131-
errors.Warning(
132-
attr,
131+
errors.Warning(ErrorId.p_deprecated_attribute,
132+
range,
133133
$"attribute :{attr.val} is deprecated");
134134
return false;
135135
}
@@ -1096,7 +1096,8 @@ ModuleExport<ModuleDefinition parent, out ModuleDecl submodule>
10961096
[ IF(IsIdentifier(la.kind) || la.kind==_digits) ExportId<out exportId> // If the next token is 'least' or 'greatest' use it as the export id,
10971097
// not the beginning of a subsequent extreme predicate declaration
10981098
(. if (exportId.line == la.line && (exportId.val == "least" || exportId.val == "greatest") && la.kind == _predicate)
1099-
errors.Warning(exportId, $"the {exportId.val} token is the identifier for the export set, not an adjective for an extreme predicate");
1099+
errors.Warning(ErrorId.p_misplaced_least_or_greatest, exportId,
1100+
$"the {exportId.val} token is the identifier for the export set, not an adjective for an extreme predicate");
11001101
.)
11011102
]
11021103
[ ellipsis (. isRefining = true; .) ]
@@ -1294,13 +1295,13 @@ ClassMemberDecl<. DeclModifierData dmod, List<MemberDecl> mm, bool allowConstruc
12941295
| ConstantFieldDecl<dmod, mm, moduleLevelDecl>
12951296
| IF(IsFunctionDecl())
12961297
(. if (moduleLevelDecl && dmod.StaticToken != null) {
1297-
errors.Warning(dmod.StaticToken, "module-level functions are always non-instance, so the 'static' keyword is not allowed here");
1298+
errors.Warning(ErrorId.p_module_level_always_static, dmod.StaticToken, "module-level functions are always non-instance, so the 'static' keyword is not allowed here");
12981299
dmod.IsStatic = false;
12991300
}
13001301
.)
13011302
FunctionDecl<dmod, out f> (. mm.Add(f); .)
13021303
| (. if (moduleLevelDecl && dmod.StaticToken != null) {
1303-
errors.Warning(dmod.StaticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here");
1304+
errors.Warning(ErrorId.p_module_level_always_static, dmod.StaticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here");
13041305
dmod.IsStatic = false;
13051306
}
13061307
.)
@@ -1422,7 +1423,7 @@ ConstantFieldDecl<.DeclModifierData dmod, List<MemberDecl/*!*/>/*!*/ mm, bool mo
14221423
Type/*!*/ ty;
14231424
Expression e = null;
14241425
if (moduleLevelDecl && dmod.StaticToken != null) {
1425-
errors.Warning(dmod.StaticToken, "module-level const declarations are always non-instance, so the 'static' keyword is not allowed here");
1426+
errors.Warning(ErrorId.p_module_level_const_always_static, dmod.StaticToken, "module-level const declarations are always non-instance, so the 'static' keyword is not allowed here");
14261427
dmod.IsStatic = false;
14271428
}
14281429
CheckDeclModifiers(ref dmod, "field", AllowedDeclModifiers.Ghost | AllowedDeclModifiers.Static | AllowedDeclModifiers.Opaque);

‎Source/DafnyCore/DafnyOptions.cs

+1-1
Original file line numberDiff line numberDiff line change
@@ -1562,7 +1562,7 @@ public ErrorReportingCommandLineParseState(string[] args, string toolName, Error
15621562
}
15631563

15641564
public override void Error(string message, params string[] args) {
1565-
errors.SemErr(token, string.Format(message, args));
1565+
errors.SemErr(GenericErrors.ErrorId.g_cli_option_error, token, string.Format(message, args));
15661566
EncounteredErrors = true;
15671567
}
15681568
}

‎Source/DafnyCore/Generic/GenericErrors.cs

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
// Copyright by the contributors to the Dafny Project
2+
// SPDX-License-Identifier: MIT
3+
4+
namespace Microsoft.Dafny;
5+
6+
public class GenericErrors {
7+
8+
public enum ErrorId {
9+
g_cli_option_error,
10+
g_include_has_errors, // In Reporting.cs
11+
12+
g_fuel_must_increase,
13+
g_no_old_unicode_char,
14+
g_unicode_escape_must_have_six_digits,
15+
g_unicode_escape_is_too_large,
16+
g_unicode_escape_may_not_be_surogate,
17+
g_U_unicode_chars_are_disallowed,
18+
g_deprecated_this_in_constructor_modifies_clause
19+
20+
}
21+
}

0 commit comments

Comments
 (0)