diff --git a/.github/workflows/runtime-tests.yml b/.github/workflows/runtime-tests.yml index d189f0c1728..56f0cf895f4 100644 --- a/.github/workflows/runtime-tests.yml +++ b/.github/workflows/runtime-tests.yml @@ -6,6 +6,9 @@ on: branches: [ master, main-* ] merge_group: +env: + dotnet-version: 6.0.x # SDK Version for building Dafny + concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true @@ -25,6 +28,10 @@ jobs: uses: actions/checkout@v4 with: submodules: true + - name: Setup dotnet + uses: actions/setup-dotnet@v4 + with: + dotnet-version: ${{env.dotnet-version}} - name: Set up JDK 18 uses: actions/setup-java@v4 with: diff --git a/Source/DafnyCore.Test/ClonerTest.cs b/Source/DafnyCore.Test/ClonerTest.cs index 67d6023266e..dcf80afe369 100644 --- a/Source/DafnyCore.Test/ClonerTest.cs +++ b/Source/DafnyCore.Test/ClonerTest.cs @@ -27,11 +27,11 @@ public void ClonerKeepsBodyStartTok() { var rangeToken = new RangeToken(Token.NoToken, Token.NoToken); var specificationFrame = new LiteralExpr(Microsoft.Dafny.Token.NoToken, 1); var formal1 = new Formal(Token.NoToken, "a", Microsoft.Dafny.Type.Bool, true, false, null) { - RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart), + RangeOrigin = new RangeToken(tokenBodyStart, tokenBodyStart), IsTypeExplicit = true }; var formal2 = new Formal(Token.NoToken, "b", Microsoft.Dafny.Type.Bool, true, false, null) { - RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart), + RangeOrigin = new RangeToken(tokenBodyStart, tokenBodyStart), IsTypeExplicit = false }; var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"), @@ -45,9 +45,9 @@ public void ClonerKeepsBodyStartTok() { var cloner = new Cloner(); var dummyDecl2 = cloner.CloneMethod(dummyDecl); Assert.Equal(2, dummyDecl2.BodyStartTok.line); - Assert.Equal(2, dummyDecl2.Ins[0].RangeToken.StartToken.line); + Assert.Equal(2, dummyDecl2.Ins[0].Origin.StartToken.line); Assert.True(dummyDecl2.Ins[0].IsTypeExplicit); - Assert.Equal(2, dummyDecl2.Ins[1].RangeToken.StartToken.line); + Assert.Equal(2, dummyDecl2.Ins[1].Origin.StartToken.line); Assert.False(dummyDecl2.Ins[1].IsTypeExplicit); } } \ No newline at end of file diff --git a/Source/DafnyCore.Test/NodeTests.cs b/Source/DafnyCore.Test/NodeTests.cs index a5cab96ec0c..842833b02ee 100644 --- a/Source/DafnyCore.Test/NodeTests.cs +++ b/Source/DafnyCore.Test/NodeTests.cs @@ -6,13 +6,20 @@ namespace DafnyCore.Test; public class NodeTests { class ConcreteNode : Node { - public ConcreteNode(RangeToken rangeOrigin, IEnumerable? children = null) { - RangeToken = rangeOrigin; + private IOrigin origin; + + public ConcreteNode(IOrigin rangeToken, IEnumerable? children = null) { + origin = rangeToken; Children = children ?? Enumerable.Empty(); } - public override RangeToken RangeToken { get; set; } - public override IOrigin Tok => RangeToken.StartToken; + public override IOrigin Origin => origin; + + public override IOrigin RangeOrigin { + set => origin = value; + } + + public override IOrigin Tok => origin.StartToken; public override IEnumerable Children { get; } public override IEnumerable PreResolveChildren => Children; } diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index 89be3e915b6..f493e074b82 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -306,7 +306,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib var bindings = atAttribute.UserSuppliedPreResolveBindings; if (name == null) { - program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, "Attribute not recognized: " + atAttribute.ToString()); + program.Reporter.Error(MessageSource.Resolver, atAttribute.Origin, "Attribute not recognized: " + atAttribute.ToString()); return null; } @@ -316,7 +316,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib } if (!builtinSyntax.CanBeApplied(attributeHost)) { - program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind); + program.Reporter.Error(MessageSource.Resolver, atAttribute.Origin, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind); } var resolver = new ModuleResolver(new ProgramResolver(program), program.Options) { @@ -614,7 +614,7 @@ private static void ResolveLikeDatatypeConstructor(Program program, Formal[] for // Verify that provided arguments are given literally foreach (var binding in bindings.ArgumentBindings) { if (binding.Actual is not LiteralExpr) { - program.Reporter.Error(MessageSource.Resolver, binding.Actual.RangeToken, $"Argument to attribute {attrName} must be a literal"); + program.Reporter.Error(MessageSource.Resolver, binding.Actual.Origin, $"Argument to attribute {attrName} must be a literal"); } } } diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 8ce07333688..fddec9b207b 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -66,7 +66,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne if (d is AbstractTypeDecl) { var dd = (AbstractTypeDecl)d; - return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, + return new AbstractTypeDecl(Origin(dd.Origin), dd.NameNode.Clone(this), newParent, CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam), dd.ParentTraits.ConvertAll(CloneType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); @@ -75,23 +75,23 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne !(d is NonNullTypeDecl)); // don't clone the non-null type declaration; close the class, which will create a new non-null type declaration var dd = (SubsetTypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); - return new SubsetTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps, + return new SubsetTypeDecl(Origin(dd.Origin), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps, newParent, CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness), CloneAttributes(dd.Attributes)); } else if (d is TypeSynonymDecl) { var dd = (TypeSynonymDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); - return new TypeSynonymDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps, + return new TypeSynonymDecl(Origin(dd.Origin), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps, newParent, CloneType(dd.Rhs), CloneAttributes(dd.Attributes)); } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Var == null) { - return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent, + return new NewtypeDecl(Origin(dd.Origin), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent, CloneType(dd.BaseType), dd.WitnessKind, CloneExpr(dd.Witness), dd.ParentTraits.ConvertAll(CloneType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); } else { - return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent, + return new NewtypeDecl(Origin(dd.Origin), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent, CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness), dd.ParentTraits.ConvertAll(CloneType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); @@ -104,7 +104,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var ctors = dd.Ctors.ConvertAll(CloneCtor); - var dt = new IndDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, ctors, + var dt = new IndDatatypeDecl(Origin(dd.Origin), dd.NameNode.Clone(this), newParent, tps, ctors, dd.ParentTraits.ConvertAll(CloneType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); return dt; @@ -112,7 +112,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne var dd = (CoDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var ctors = dd.Ctors.ConvertAll(CloneCtor); - var dt = new CoDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, ctors, + var dt = new CoDatatypeDecl(Origin(dd.Origin), dd.NameNode.Clone(this), newParent, tps, ctors, dd.ParentTraits.ConvertAll(CloneType), dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining); return dt; @@ -129,7 +129,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne var ens = dd.Ensures.ConvertAll(CloneAttributedExpr); var yens = dd.YieldEnsures.ConvertAll(CloneAttributedExpr); var body = CloneBlockStmt(dd.Body); - var iter = new IteratorDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, + var iter = new IteratorDecl(Origin(dd.Origin), dd.NameNode.Clone(this), newParent, tps, ins, outs, reads, mod, decr, req, ens, yreq, yens, body, CloneAttributes(dd.Attributes), dd.SignatureEllipsis); @@ -138,7 +138,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne var dd = (TraitDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var mm = dd.Members.ConvertAll(member => CloneMember(member, false)); - var cl = new TraitDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, mm, + var cl = new TraitDecl(Origin(dd.Origin), dd.NameNode.Clone(this), newParent, tps, mm, CloneAttributes(dd.Attributes), dd.IsRefining, dd.ParentTraits.ConvertAll(CloneType)); return cl; } else if (d is DefaultClassDecl) { @@ -150,7 +150,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne var dd = (ClassDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var mm = dd.Members.ConvertAll(member => CloneMember(member, false)); - return new ClassDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, mm, + return new ClassDecl(Origin(dd.Origin), dd.NameNode.Clone(this), newParent, tps, mm, CloneAttributes(dd.Attributes), dd.IsRefining, dd.ParentTraits.ConvertAll(CloneType)); } else if (d is ModuleDecl) { if (d is LiteralModuleDecl moduleDecl) { @@ -188,13 +188,13 @@ public TypeParameter.TypeParameterCharacteristics CloneTPChar( } public DatatypeCtor CloneCtor(DatatypeCtor ct) { - return new DatatypeCtor(Range(ct.RangeToken), ct.NameNode.Clone(this), ct.IsGhost, + return new DatatypeCtor(Origin(ct.Origin), ct.NameNode.Clone(this), ct.IsGhost, ct.Formals.ConvertAll(bv => CloneFormal(bv, false)), CloneAttributes(ct.Attributes)); } public TypeParameter CloneTypeParam(TypeParameter tp) { return (TypeParameter)typeParameterClones.GetOrCreate(tp, - () => new TypeParameter(Range(tp.RangeToken), tp.NameNode.Clone(this), tp.VarianceSyntax, + () => new TypeParameter(Origin(tp.Origin), tp.NameNode.Clone(this), tp.VarianceSyntax, CloneTPChar(tp.Characteristics), tp.TypeBounds.ConvertAll(CloneType))); } @@ -237,7 +237,7 @@ public virtual Type CloneType(Type t) { return new MapType(this, mapType); } else if (t is ArrowType) { var tt = (ArrowType)t; - return new ArrowType(Tok(tt.tok), tt.Args.ConvertAll(CloneType), CloneType(tt.Result)); + return new ArrowType(Origin(tt.tok), tt.Args.ConvertAll(CloneType), CloneType(tt.Result)); } else if (t is UserDefinedType) { var tt = (UserDefinedType)t; #if TEST_TYPE_SYNONYM_TRANSPARENCY @@ -269,10 +269,10 @@ public virtual Type CloneType(Type t) { public virtual Formal CloneFormal(Formal formal, bool isReference) { return (Formal)clones.GetOrCreate(formal, () => isReference ? formal - : new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost, + : new Formal(Origin(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost, CloneExpr(formal.DefaultValue), CloneAttributes(formal.Attributes), formal.IsOld, formal.IsNameOnly, formal.IsOlder, formal.NameForCompilation) { - RangeToken = formal.RangeToken, + RangeOrigin = formal.Origin, IsTypeExplicit = formal.IsTypeExplicit }); } @@ -283,7 +283,7 @@ public virtual BoundVar CloneBoundVar(BoundVar bv, bool isReference) { return bv; } - var bvNew = new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.SyntacticType)); + var bvNew = new BoundVar(Origin(bv.tok), bv.Name, CloneType(bv.SyntacticType)); bvNew.IsGhost = bv.IsGhost; return bvNew; }); @@ -335,9 +335,9 @@ public Attributes CloneAttributes(Attributes attrs) { // skip this attribute, since it would have been produced during resolution return CloneAttributes(attrs.Prev); } else if (attrs is UserSuppliedAttributes usa) { - return new UserSuppliedAttributes(Tok(usa.tok), Tok(usa.OpenBrace), Tok(usa.CloseBrace), + return new UserSuppliedAttributes(Origin(usa.tok), Origin(usa.OpenBrace), Origin(usa.CloseBrace), attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)) { - RangeToken = Tok(usa.RangeToken) + RangeOrigin = Origin(usa.Origin) }; } else if (attrs is UserSuppliedAtAttribute usaa) { var arg = CloneExpr(usaa.Arg); @@ -345,27 +345,27 @@ public Attributes CloneAttributes(Attributes attrs) { arg.Type = usaa.Arg.Type; arg.PreType = usaa.Arg.PreType; } - return new UserSuppliedAtAttribute(Tok(usaa.tok), arg, CloneAttributes(usaa.Prev)) { - RangeToken = Tok(usaa.RangeToken), + return new UserSuppliedAtAttribute(Origin(usaa.tok), arg, CloneAttributes(usaa.Prev)) { + RangeOrigin = Origin(usaa.Origin), Builtin = usaa.Builtin }; } else { return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)) { - RangeToken = Tok(attrs.RangeToken) + RangeOrigin = Origin(attrs.Origin) }; } } public AttributedExpression CloneAttributedExpr(AttributedExpression expr) { - var mfe = new AttributedExpression(CloneExpr(expr.E), - expr.Label == null ? null : new AssertLabel(Tok(expr.Label.Tok), expr.Label.Name), + var mfe = new AttributedExpression(Origin(expr.Origin), CloneExpr(expr.E), + expr.Label == null ? null : new AssertLabel(Origin(expr.Label.Tok), expr.Label.Name), CloneAttributes(expr.Attributes)); mfe.Attributes = CloneAttributes(expr.Attributes); return mfe; } public virtual ActualBinding CloneActualBinding(ActualBinding binding) { - return new ActualBinding(binding.FormalParameterName == null ? null : Tok(binding.FormalParameterName), + return new ActualBinding(binding.FormalParameterName, CloneExpr(binding.Actual)); } @@ -384,13 +384,13 @@ public virtual Expression CloneExpr(Expression expr) { public MatchCaseExpr CloneMatchCaseExpr(MatchCaseExpr c) { Contract.Requires(c != null); Contract.Requires(c.Arguments != null); - return new MatchCaseExpr(Tok(c.tok), c.Ctor, c.FromBoundVar, + return new MatchCaseExpr(Origin(c.tok), c.Ctor, c.FromBoundVar, c.Arguments.ConvertAll(bv => CloneBoundVar(bv, false)), CloneExpr(c.Body), CloneAttributes(c.Attributes)); } public NestedMatchCaseExpr CloneNestedMatchCaseExpr(NestedMatchCaseExpr c) { Contract.Requires(c != null); - return new NestedMatchCaseExpr(Tok(c.Tok), CloneExtendedPattern(c.Pat), CloneExpr(c.Body), + return new NestedMatchCaseExpr(Origin(c.Tok), CloneExtendedPattern(c.Pat), CloneExpr(c.Body), CloneAttributes(c.Attributes)); } @@ -418,7 +418,7 @@ public virtual BlockStmt CloneBlockStmt(BlockStmt stmt) { if (stmt == null) { return null; } else { - return new BlockStmt(Tok(stmt.RangeToken), stmt.Body.ConvertAll(stmt1 => CloneStmt(stmt1, false))); + return new BlockStmt(Origin(stmt.Origin), stmt.Body.ConvertAll(stmt1 => CloneStmt(stmt1, false))); } } @@ -426,8 +426,8 @@ public virtual DividedBlockStmt CloneDividedBlockStmt(DividedBlockStmt stmt) { if (stmt == null) { return null; } else { - return new DividedBlockStmt(Tok(stmt.RangeToken), stmt.BodyInit.ConvertAll(stmt1 => CloneStmt(stmt1, false)), - stmt.SeparatorTok == null ? null : Tok(stmt.SeparatorTok), stmt.BodyProper.ConvertAll(stmt1 => CloneStmt(stmt1, false))); + return new DividedBlockStmt(Origin(stmt.Origin), stmt.BodyInit.ConvertAll(stmt1 => CloneStmt(stmt1, false)), + stmt.SeparatorTok == null ? null : Origin(stmt.SeparatorTok), stmt.BodyProper.ConvertAll(stmt1 => CloneStmt(stmt1, false))); } } @@ -461,7 +461,7 @@ public virtual Statement CloneStmt(Statement stmt, bool isReference) { public MatchCaseStmt CloneMatchCaseStmt(MatchCaseStmt c) { Contract.Requires(c != null); Contract.Assert(c.Arguments != null); - return new MatchCaseStmt(Tok(c.RangeToken), c.Ctor, c.FromBoundVar, + return new MatchCaseStmt(Origin(c.Origin), c.Ctor, c.FromBoundVar, c.Arguments.ConvertAll(v => CloneBoundVar(v, false)), c.Body.ConvertAll(stmt => CloneStmt(stmt, false)), CloneAttributes(c.Attributes)); } @@ -505,26 +505,26 @@ public void AddStmtLabels(Statement s, LList