From 8e4a2c2d75a7af69acfdf04c97bb12f0fdb2222d Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 21 Jul 2025 14:18:12 +0200 Subject: [PATCH 1/7] Allow empty ghost const field --- Source/DafnyCore/Resolver/ModuleResolver.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 36d812e55ff..31dde9fc327 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1872,8 +1872,8 @@ private void CheckIsOkayWithoutRHS(ConstantField f, bool giveNonReferenceTypeTra var statik = f.IsStatic ? "static " : ""; if (f.IsGhost && !f.Type.IsNonempty) { - reporter.Error(MessageSource.Resolver, f.Origin, - $"{statik}ghost const field '{f.Name}' of type '{f.Type}' (which may be empty) must give a defining value{hint}"); + // reporter.Error(MessageSource.Resolver, f.Origin, + // $"{statik}ghost const field '{f.Name}' of type '{f.Type}' (which may be empty) must give a defining value{hint}"); } else if (!f.IsGhost && !f.Type.HasCompilableValue) { reporter.Error(MessageSource.Resolver, f.Origin, $"{statik}non-ghost const field '{f.Name}' of type '{f.Type}' (which does not have a default compiled value) must give a defining value{hint}"); From aafee80f39048e8b06857baa122533c6ee9f21da Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 21 Jul 2025 14:30:35 +0200 Subject: [PATCH 2/7] Allow assigning to array elements in ghost code --- Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs index d7578e44e4c..0b26f7389c1 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs @@ -120,7 +120,7 @@ public static NonGhostKind LhsIsToGhost_Which(Expression lhs) { } } else { // LHS denotes an array element, which is always non-ghost - return NonGhostKind.ArrayElement; + return NonGhostKind.IsGhost; } return NonGhostKind.IsGhost; } From 5c77593ddb9663187328a881fbcce4d56e6e265b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 22 Jul 2025 15:48:28 +0200 Subject: [PATCH 3/7] Fixes --- Source/DafnyCore/Resolver/ModuleResolver.cs | 21 +++++++++++--- .../LitTest/git-issues/git-issue-1148.dfy | 16 ++++++++++- .../git-issues/git-issue-1148.dfy.expect | 28 +++++++++++-------- 3 files changed, 48 insertions(+), 17 deletions(-) diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 31dde9fc327..9eef8619ab2 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1543,6 +1543,21 @@ public void ResolveTopLevelDecls_Core(List declarations, CheckIsOkayWithoutRHS(f, false); } } + foreach (var member in cl.InheritedMembers) { + if (member is ConstantField f && f.Rhs == null && !f.IsExtern(Options, out _, out _)) { + if (f.IsGhost && !f.Type.IsNonempty) { + reporter.Error(MessageSource.Resolver, cl.Origin, + $"{cl.WhatKindAndName} must not inherit a ghost const field '{f.Name}' of type '{f.Type}' (which may be empty) without a defining value"); + break; + } + + if (!f.IsGhost && !f.Type.HasCompilableValue) { + reporter.Error(MessageSource.Resolver, cl.Origin, + $"{cl.WhatKindAndName} must not inherit a non-ghost const field '{f.Name}' of type '{f.Type}' (which does not have a default compiled value) without a defining value"); + break; + } + } + } } continue; } @@ -1553,8 +1568,6 @@ public void ResolveTopLevelDecls_Core(List declarations, if (member is ConstantField f && f.Rhs == null && !f.IsExtern(Options, out _, out _)) { if (f.IsStatic) { CheckIsOkayWithoutRHS(f, false); - } else if (!traitDecl.IsReferenceTypeDecl) { - CheckIsOkayWithoutRHS(f, true); } } } @@ -1872,8 +1885,8 @@ private void CheckIsOkayWithoutRHS(ConstantField f, bool giveNonReferenceTypeTra var statik = f.IsStatic ? "static " : ""; if (f.IsGhost && !f.Type.IsNonempty) { - // reporter.Error(MessageSource.Resolver, f.Origin, - // $"{statik}ghost const field '{f.Name}' of type '{f.Type}' (which may be empty) must give a defining value{hint}"); + reporter.Error(MessageSource.Resolver, f.Origin, + $"{statik}ghost const field '{f.Name}' of type '{f.Type}' (which may be empty) must give a defining value{hint}"); } else if (!f.IsGhost && !f.Type.HasCompilableValue) { reporter.Error(MessageSource.Resolver, f.Origin, $"{statik}non-ghost const field '{f.Name}' of type '{f.Type}' (which does not have a default compiled value) must give a defining value{hint}"); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy index 239af68a517..695c0b8eb4c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype module AutoInitRegressions { @@ -42,6 +42,13 @@ module AutoInitRegressions { static const Static: Y // error: Y is not auto-init const Instance: Y // error: Y is not auto-init } + + trait PossiblyDatatypeTrait { + static const StaticField: Y // error: Y is not nonempty + const InstanceField: Y + } + + datatype PossiblyDatatypeTraitImpl extends PossiblyDatatypeTrait = PossiblyDatatypeTraitImpl { } // error } module NonemptyRegressions { @@ -79,4 +86,11 @@ module NonemptyRegressions { ghost static const Static: Y // error: Y is not nonempty ghost const Instance: Y // error: Y is not nonempty } + + trait PossiblyDatatypeTrait { + ghost static const StaticField: Y // error: Y is not nonempty + ghost const InstanceField: Y + } + + datatype PossiblyDatatypeTraitImpl extends PossiblyDatatypeTrait = PossiblyDatatypeTraitImpl { } // error } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy.expect index 2bce27b1007..490d5aa1737 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy.expect @@ -9,15 +9,19 @@ git-issue-1148.dfy(36,17): Error: static non-ghost const field 'Static' of type git-issue-1148.dfy(37,10): Error: non-ghost const field 'Instance' of type 'Y' (which does not have a default compiled value) must give a defining value git-issue-1148.dfy(42,17): Error: static non-ghost const field 'Static' of type 'Y' (which does not have a default compiled value) must give a defining value git-issue-1148.dfy(43,10): Error: non-ghost const field 'Instance' of type 'Y' (which does not have a default compiled value) must give a defining value -git-issue-1148.dfy(56,14): Error: static ghost const field 'Global' of type 'Y' (which may be empty) must give a defining value -git-issue-1148.dfy(52,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value -git-issue-1148.dfy(53,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value -git-issue-1148.dfy(59,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value -git-issue-1148.dfy(58,8): Error: class 'Class' with fields without known initializers, like 'InstanceField' of type 'Y', must declare a constructor -git-issue-1148.dfy(64,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value -git-issue-1148.dfy(68,8): Error: class 'TraitImpl' with fields without known initializers, like 'InstanceField' of type 'Y', must declare a constructor -git-issue-1148.dfy(73,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value -git-issue-1148.dfy(74,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value -git-issue-1148.dfy(79,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value -git-issue-1148.dfy(80,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value -22 resolution/type errors detected in git-issue-1148.dfy +git-issue-1148.dfy(47,17): Error: static non-ghost const field 'StaticField' of type 'Y' (which does not have a default compiled value) must give a defining value +git-issue-1148.dfy(51,11): Error: datatype 'PossiblyDatatypeTraitImpl' may not inherit a non-ghost const field 'InstanceField' of type 'Y' (which does not have a default compiled value) without a defining value +git-issue-1148.dfy(63,14): Error: static ghost const field 'Global' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(59,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(60,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(66,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(65,8): Error: class 'Class' with fields without known initializers, like 'InstanceField' of type 'Y', must declare a constructor +git-issue-1148.dfy(71,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(75,8): Error: class 'TraitImpl' with fields without known initializers, like 'InstanceField' of type 'Y', must declare a constructor +git-issue-1148.dfy(80,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(81,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(86,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(87,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(91,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value +git-issue-1148.dfy(95,11): Error: datatype 'PossiblyDatatypeTraitImpl' must not inherit a ghost const field 'InstanceField' of type 'Y' (which may be empty) without a defining value +26 resolution/type errors detected in git-issue-1148.dfy From 30f060a48a1f9672894be5bf6f1144b0d2fae6f6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Jul 2025 13:22:50 +0200 Subject: [PATCH 4/7] Revert one change --- Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs index 0b26f7389c1..d7578e44e4c 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs @@ -120,7 +120,7 @@ public static NonGhostKind LhsIsToGhost_Which(Expression lhs) { } } else { // LHS denotes an array element, which is always non-ghost - return NonGhostKind.IsGhost; + return NonGhostKind.ArrayElement; } return NonGhostKind.IsGhost; } From 9026ac6eb41539d97f798566d94903b3b3c52d14 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Jul 2025 13:47:43 +0200 Subject: [PATCH 5/7] Update test --- .../LitTests/LitTest/traits/NonReferenceTraits.dfy | 6 +++--- .../LitTests/LitTest/traits/NonReferenceTraits.dfy.expect | 5 +---- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy index a50e74bc7bb..37209e1b693 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy @@ -216,14 +216,14 @@ module UninitializedConsts { ghost const A: AutoInit ghost const B: AutoInit := 15 - const g: Nonempty // error: requires initialization + const g: Nonempty const h: Nonempty := 15 ghost const G: Nonempty ghost const H: Nonempty := 15 - const s: PossiblyEmpty // error: requires initialization + const s: PossiblyEmpty const t: PossiblyEmpty := 15 - ghost const S: PossiblyEmpty // error: requires initialization + ghost const S: PossiblyEmpty ghost const T: PossiblyEmpty := 15 } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy.expect index 797c7653f70..2bc71c6cd48 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy.expect @@ -77,9 +77,6 @@ NonReferenceTraits.dfy(192,16): Error: ghost const field 'S' of type 'PossiblyEm NonReferenceTraits.dfy(202,10): Error: non-ghost const field 'g' of type 'Nonempty' (which does not have a default compiled value) must give a defining value NonReferenceTraits.dfy(207,10): Error: non-ghost const field 's' of type 'PossiblyEmpty' (which does not have a default compiled value) must give a defining value NonReferenceTraits.dfy(209,16): Error: ghost const field 'S' of type 'PossiblyEmpty' (which may be empty) must give a defining value -NonReferenceTraits.dfy(219,10): Error: non-ghost const field 'g' of type 'Nonempty' (which does not have a default compiled value) must give a defining value (consider changing the field to be a function, or restricting the enclosing trait to be a reference type by adding 'extends object') -NonReferenceTraits.dfy(224,10): Error: non-ghost const field 's' of type 'PossiblyEmpty' (which does not have a default compiled value) must give a defining value (consider changing the field to be a function, or restricting the enclosing trait to be a reference type by adding 'extends object') -NonReferenceTraits.dfy(226,16): Error: ghost const field 'S' of type 'PossiblyEmpty' (which may be empty) must give a defining value (consider changing the field to be a function, or restricting the enclosing trait to be a reference type by adding 'extends object') NonReferenceTraits.dfy(279,8): Error: class 'ClassWithParentWithoutConstructor' with fields without known initializers, like 'g' of type 'Nonempty', must declare a constructor NonReferenceTraits.dfy(295,17): Error: static non-ghost const field 'g' of type 'Nonempty' (which does not have a default compiled value) must give a defining value NonReferenceTraits.dfy(300,17): Error: static non-ghost const field 's' of type 'PossiblyEmpty' (which does not have a default compiled value) must give a defining value @@ -112,4 +109,4 @@ NonReferenceTraits.dfy(460,9): Error: == can only be applied to expressions of t NonReferenceTraits.dfy(470,9): Error: == can only be applied to expressions of types that support equality (got TraitA) NonReferenceTraits.dfy(471,9): Error: == can only be applied to expressions of types that support equality (got TraitB) NonReferenceTraits.dfy(472,14): Error: set argument type must support equality (got TraitA) -62 resolution/type errors detected in NonReferenceTraits.dfy +59 resolution/type errors detected in NonReferenceTraits.dfy From 474983588ae2d5048d5241048d6da5cd899b8a27 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Jul 2025 14:07:17 +0200 Subject: [PATCH 6/7] Fix expect file --- .../LitTests/LitTest/git-issues/git-issue-1148.dfy.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy.expect index 490d5aa1737..b95699b433f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy.expect @@ -10,7 +10,7 @@ git-issue-1148.dfy(37,10): Error: non-ghost const field 'Instance' of type 'Y' ( git-issue-1148.dfy(42,17): Error: static non-ghost const field 'Static' of type 'Y' (which does not have a default compiled value) must give a defining value git-issue-1148.dfy(43,10): Error: non-ghost const field 'Instance' of type 'Y' (which does not have a default compiled value) must give a defining value git-issue-1148.dfy(47,17): Error: static non-ghost const field 'StaticField' of type 'Y' (which does not have a default compiled value) must give a defining value -git-issue-1148.dfy(51,11): Error: datatype 'PossiblyDatatypeTraitImpl' may not inherit a non-ghost const field 'InstanceField' of type 'Y' (which does not have a default compiled value) without a defining value +git-issue-1148.dfy(51,11): Error: datatype 'PossiblyDatatypeTraitImpl' must not inherit a non-ghost const field 'InstanceField' of type 'Y' (which does not have a default compiled value) without a defining value git-issue-1148.dfy(63,14): Error: static ghost const field 'Global' of type 'Y' (which may be empty) must give a defining value git-issue-1148.dfy(59,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value git-issue-1148.dfy(60,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value From c62e0b8e41c40b7411d02ce284bfc2b4b7bb1ef1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 23 Jul 2025 14:09:04 +0200 Subject: [PATCH 7/7] Add release note --- docs/dev/news/6314.feat | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/6314.feat diff --git a/docs/dev/news/6314.feat b/docs/dev/news/6314.feat new file mode 100644 index 00000000000..3ef4b4795e8 --- /dev/null +++ b/docs/dev/news/6314.feat @@ -0,0 +1 @@ +Allow value traits (those that do not extend from object), to declare const fields without initializers. \ No newline at end of file