Merge branch 'master' into issue-3859

.github/workflows/msbuild.yml

@@ -121,7 +121,8 @@ jobs:
  # LSP results
  reportgenerator \
  -reports:"./**/coverage.cobertura.xml" \
- -reporttypes:Cobertura -targetdir:coverage-cobertura
+ -reporttypes:Cobertura -targetdir:coverage-cobertura \
+ -classfilters:-Microsoft.Dafny.*PreType*
  # Generate HTML from combined report, leaving out XUnitExtensions
  reportgenerator \
  -reports:"coverage-cobertura/Cobertura.xml" \

Scripts/package.py

@@ -236,28 +236,20 @@ def pack(args, releases):
 def check_version_cs(args):
  # Checking Directory.Build.props
  with open(path.join(SOURCE_DIRECTORY, "Directory.Build.props")) as fp:
- match = re.search(r'\<VersionPrefix\>([0-9]+.[0-9]+.[0-9]+).([0-9]+)', fp.read())
+ match = re.search(r'\<VersionPrefix\>([0-9]+.[0-9]+.[0-9]+)', fp.read())
  if match:
- (v1, v2) = match.groups()
+ source_version = match.groups()[0]
  else:
  flush("The AssemblyVersion attribute in Directory.Build.props could not be found.")
  return False
- now = time.localtime()
- year = now[0]
- month = now[1]
- day = now[2]
- v3 = str(year-2018) + str(month).zfill(2) + str(day).zfill(2)
- if v2 != v3:
- flush("The date in Directory.Build.props does not agree with today's date: " + v3 + " vs. " + v2)
  if "-" in args.version:
  hy = args.version[:args.version.index('-')]
  else:
  hy = args.version
- if hy != v1:
- flush("The version number in Directory.Build.props does not agree with the given version: " + hy + " vs. " + v1)
- if (v2 != v3 or hy != v1):
+ if hy != source_version:
+ flush("The version number in Directory.Build.props does not agree with the given version: " + source_version + " vs. " + hy)
  return False
- flush("Creating release files for release \"" + args.version + "\" and internal version information: " + v1 + "." + v2)
+ flush("Creating release files for release \"" + args.version + "\" and internal version information: " + source_version)
  return True
 
 def parse_arguments():

Source/DafnyCore/AST/BuiltIns.cs

@@ -9,7 +9,7 @@ namespace Microsoft.Dafny;
 public class BuiltIns {
  public DafnyOptions Options { get; }
  public readonly ModuleDefinition SystemModule = new ModuleDefinition(RangeToken.NoToken, new Name("_System"), new List<IToken>(), false, false, null, null, null, true, true, true);
- readonly Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();
+ internal readonly Dictionary<int, ClassDecl> arrayTypeDecls = new Dictionary<int, ClassDecl>();
  public readonly Dictionary<int, ArrowTypeDecl> ArrowTypeDecls = new Dictionary<int, ArrowTypeDecl>();
  public readonly Dictionary<int, SubsetTypeDecl> PartialArrowTypeDecls = new Dictionary<int, SubsetTypeDecl>(); // same keys as arrowTypeDecl
  public readonly Dictionary<int, SubsetTypeDecl> TotalArrowTypeDecls = new Dictionary<int, SubsetTypeDecl>(); // same keys as arrowTypeDecl

Source/DafnyCore/AST/DafnyAst.cs

@@ -393,6 +393,11 @@ string SanitizedName {
  string CompileName {
  get;
  }
+
+ PreType PreType {
+ get;
+ set;
+ }
  Type Type {
  get;
  }
@@ -456,6 +461,9 @@ public Type OptionalType {
  throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
  }
  }
+
+ public PreType PreType { get; set; }
+
  public bool IsMutable {
  get {
  throw new NotImplementedException();
@@ -556,6 +564,8 @@ public static string SanitizeName(string nm) {
  Type type;
  public bool IsTypeExplicit = false;
  public Type SyntacticType { get { return type; } } // returns the non-normalized type
+ public PreType PreType { get; set; }
+
  public Type Type {
  get {
  Contract.Ensures(Contract.Result<Type>() != null);

Source/DafnyCore/AST/Expressions/Expressions.cs

@@ -18,7 +18,7 @@ void ObjectInvariant() {
 
  [System.Diagnostics.Contracts.Pure]
  public bool WasResolved() {
- return Type != null;
+ return PreType != null || Type != null;
  }
 
  public Expression Resolved {
@@ -41,6 +41,9 @@ public Expression Resolved {
  }
  }
 
+
+ public PreType PreType;
+
  public virtual IEnumerable<Expression> TerminalExpressions {
  get {
  yield return this;
@@ -979,6 +982,7 @@ public class DatatypeValue : Expression, IHasUsages, ICloneable<DatatypeValue>,
 
  [FilledInDuringResolution] public DatatypeCtor Ctor;
  [FilledInDuringResolution] public List<Type> InferredTypeArgs = new List<Type>();
+ [FilledInDuringResolution] public List<PreType> InferredPreTypeArgs = new List<PreType>();
  [FilledInDuringResolution] public bool IsCoCall;
  [ContractInvariantMethod]
  void ObjectInvariant() {
@@ -1253,6 +1257,7 @@ public Resolver_IdentifierExpr(IToken tok, TopLevelDecl decl, List<Type> typeArg
  Decl = decl;
  TypeArgs = typeArgs;
  Type = decl is ModuleDecl ? (Type)new ResolverType_Module() : new ResolverType_Type();
+ PreType = decl is ModuleDecl ? new PreTypePlaceholderModule() : new PreTypePlaceholderType();
  }
  public Resolver_IdentifierExpr(IToken tok, TypeParameter tp)
  : this(tok, tp, new List<Type>()) {
@@ -1488,6 +1493,8 @@ public class FunctionCallExpr : Expression, IHasUsages, ICloneable<FunctionCallE
  public readonly Label/*?*/ AtLabel;
  public readonly ActualBindings Bindings;
  public List<Expression> Args => Bindings.Arguments;
+ [FilledInDuringResolution] public List<PreType> PreTypeApplication_AtEnclosingClass;
+ [FilledInDuringResolution] public List<PreType> PreTypeApplication_JustFunction;
  [FilledInDuringResolution] public List<Type> TypeApplication_AtEnclosingClass;
  [FilledInDuringResolution] public List<Type> TypeApplication_JustFunction;
  [FilledInDuringResolution] public bool IsByMethodCall;

Source/DafnyCore/AST/Expressions/IdPattern.cs

@@ -11,6 +11,7 @@ namespace Microsoft.Dafny;
 public class IdPattern : ExtendedPattern, IHasUsages {
  public bool HasParenthesis { get; }
  public String Id;
+ public PreType PreType;
  public Type Type; // This is the syntactic type, ExtendedPatterns dissapear during resolution.
  public IVariable BoundVar { get; set; }
  public List<ExtendedPattern> Arguments; // null if just an identifier; possibly empty argument list if a constructor call

Source/DafnyCore/AST/Expressions/MemberSelectExpr.cs

@@ -11,6 +11,18 @@ public class MemberSelectExpr : Expression, IHasUsages, ICloneable<MemberSelectE
  [FilledInDuringResolution] public Label /*?*/ AtLabel; // non-null for a two-state selection
  [FilledInDuringResolution] public bool InCompiledContext;
 
+ /// <summary>
+ /// PreTypeApplication_AtEnclosingClass is the list of type arguments used to instantiate the type that
+ /// declares Member (which is some supertype of the receiver type).
+ /// </summary>
+ [FilledInDuringResolution] public List<PreType> PreTypeApplication_AtEnclosingClass;
+
+ /// <summary>
+ /// PreTypeApplication_JustMember is the list of type arguments used to instantiate the type parameters
+ /// of Member.
+ /// </summary>
+ [FilledInDuringResolution] public List<PreType> PreTypeApplication_JustMember;
+
  /// <summary>
  /// TypeApplication_AtEnclosingClass is the list of type arguments used to instantiate the type that
  /// declares Member (which is some supertype of the receiver type).
@@ -63,6 +75,46 @@ public Dictionary<TypeParameter, Type> TypeArgumentSubstitutionsAtMemberDeclarat
  return subst;
  }
 
+ /// <summary>
+ /// Returns a mapping from formal type parameters to actual pre-type arguments. For example, given
+ /// trait T<A> {
+ /// function F<X>(): bv8 { ... }
+ /// }
+ /// class C<B, D> extends T<map<B, D>> { }
+ /// and MemberSelectExpr o.F<int> where o has type C<real, bool>, the type map returned is
+ /// A -> map<real, bool>
+ /// X -> int
+ /// To also include B and D in the mapping, use PreTypeArgumentSubstitutionsWithParents instead.
+ /// </summary>
+ public Dictionary<TypeParameter, PreType> PreTypeArgumentSubstitutionsAtMemberDeclaration() {
+ Contract.Requires(WasResolved());
+ Contract.Ensures(Contract.Result<Dictionary<TypeParameter, Type>>() != null);
+
+ var subst = new Dictionary<TypeParameter, PreType>();
+
+ // Add the mappings from the member's own type parameters
+ if (Member is ICallable icallable) {
+ Contract.Assert(PreTypeApplication_JustMember.Count == icallable.TypeArgs.Count);
+ for (var i = 0; i < icallable.TypeArgs.Count; i++) {
+ subst.Add(icallable.TypeArgs[i], PreTypeApplication_JustMember[i]);
+ }
+ } else {
+ Contract.Assert(PreTypeApplication_JustMember.Count == 0);
+ }
+
+ // Add the mappings from the enclosing class.
+ TopLevelDecl cl = Member.EnclosingClass;
+ // Expand the type down to its non-null type, if any
+ if (cl != null) {
+ Contract.Assert(cl.TypeArgs.Count == PreTypeApplication_AtEnclosingClass.Count);
+ for (var i = 0; i < cl.TypeArgs.Count; i++) {
+ subst.Add(cl.TypeArgs[i], PreTypeApplication_AtEnclosingClass[i]);
+ }
+ }
+
+ return subst;
+ }
+
  /// <summary>
  /// Returns a mapping from formal type parameters to actual type arguments. For example, given
  /// trait T<A> {

Source/DafnyCore/AST/Function.cs

@@ -84,6 +84,7 @@ public TailStatus
  public readonly List<TypeParameter> TypeArgs;
  public readonly List<Formal> Formals;
  public readonly Formal Result;
+ public PreType ResultPreType;
  public readonly Type ResultType;
  public readonly List<AttributedExpression> Req;
  public readonly List<FrameExpression> Reads;
@@ -363,6 +364,7 @@ public void Resolve(Resolver resolver) {
  if (Attributes.ContainsBool(Attributes, "warnShadowing", ref warnShadowing)) {
  resolver.Options.WarnShadowing = warnShadowing; // set the value according to the attribute
  }
+ resolver.DominatingStatementLabels.PushMarker();
 
  resolver.scope.PushMarker();
  if (IsStatic) {
@@ -375,9 +377,9 @@ public void Resolve(Resolver resolver) {
 
  resolver.ResolveParameterDefaultValues(Formals, ResolutionContext.FromCodeContext(this));
 
- foreach (AttributedExpression e in Req) {
- resolver.ResolveAttributes(e, new ResolutionContext(this, this is TwoStateFunction));
- Expression r = e.E;
+ foreach (var req in Req) {
+ resolver.ResolveAttributes(req, new ResolutionContext(this, this is TwoStateFunction));
+ Expression r = req.E;
  resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction));
  Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
  resolver.ConstrainTypeExprBool(r, "Precondition must be a boolean (got {0})");
@@ -407,10 +409,23 @@ public void Resolve(Resolver resolver) {
  resolver.SolveAllTypeConstraints(); // solve type constraints in the specification
 
  if (Body != null) {
+
+ resolver.DominatingStatementLabels.PushMarker();
+ foreach (var req in Req) {
+ if (req.Label != null) {
+ if (resolver.DominatingStatementLabels.Find(req.Label.Name) != null) {
+ resolver.reporter.Error(MessageSource.Resolver, req.Label.Tok, "assert label shadows a dominating label");
+ } else {
+ var rr = resolver.DominatingStatementLabels.Push(req.Label.Name, req.Label);
+ Contract.Assert(rr == Scope<Label>.PushResult.Success); // since we just checked for duplicates, we expect the Push to succeed
+ }
+ }
+ }
  resolver.ResolveExpression(Body, new ResolutionContext(this, this is TwoStateFunction));
  Contract.Assert(Body.Type != null); // follows from postcondition of ResolveExpression
  resolver.AddAssignableConstraint(tok, ResultType, Body.Type, "Function body type mismatch (expected {0}, got {1})");
  resolver.SolveAllTypeConstraints();
+ resolver.DominatingStatementLabels.PopMarker();
  }
 
  resolver.scope.PushMarker();
@@ -436,6 +451,7 @@ public void Resolve(Resolver resolver) {
  }
 
  resolver.Options.WarnShadowing = warnShadowingOption; // restore the original warnShadowing value
+ resolver.DominatingStatementLabels.PopMarker();
  }
 
  protected override string GetTriviaContainingDocstring() {

Source/DafnyCore/AST/MemberDecls.cs

@@ -97,6 +97,7 @@ public class Field : MemberDecl, ICanFormat, IHasDocstring {
  public override string WhatKind => "field";
  public readonly bool IsMutable; // says whether or not the field can ever change values
  public readonly bool IsUserMutable; // says whether or not code is allowed to assign to the field (IsUserMutable implies IsMutable)
+ public PreType PreType;
  public readonly Type Type;
  [ContractInvariantMethod]
  void ObjectInvariant() {

Source/DafnyCore/AST/Method.cs

@@ -26,6 +26,7 @@ public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext,
  public readonly Specification<Expression> Decreases;
  [FilledInDuringResolution] public bool IsRecursive;
  [FilledInDuringResolution] public bool IsTailRecursive;
+ [FilledInDuringResolution] public Function FunctionFromWhichThisIsByMethodDecl;
  public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();
  public Method OverriddenMethod;
  public Method Original => OverriddenMethod == null ? this : OverriddenMethod.Original;

Source/DafnyCore/AST/Statements/Statements.cs

@@ -556,6 +556,7 @@ public TypeRhs(Cloner cloner, TypeRhs original)
 
  public Type Path;
  [FilledInDuringResolution] public CallStmt InitCall; // may be null (and is definitely null for arrays),
+ [FilledInDuringResolution] public PreType PreType;
  [FilledInDuringResolution] public Type Type;
  [ContractInvariantMethod]
  void ObjectInvariant() {
@@ -877,6 +878,9 @@ public Type Type {
  return type.Normalize();
  }
  }
+
+ public PreType PreType { get; set; }
+
  public bool IsMutable {
  get {
  return true;

Source/DafnyCore/AST/TopLevelDeclarations.cs

@@ -2217,6 +2217,7 @@ public interface RevealableTypeDecl {
 public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, RedirectingTypeDecl, IHasDocstring {
  public override string WhatKind { get { return "newtype"; } }
  public override bool CanBeRevealed() { return true; }
+ public PreType BasePreType;
  public Type BaseType { get; set; } // null when refining
  public BoundVar Var { get; set; } // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType))
  public Expression Constraint { get; set; } // is null iff Var is

Source/DafnyCore/Dafny.atg

@@ -2923,7 +2923,7 @@ OneStmt<out Statement/*!*/ s>
  | IfStmt<out s>
  | WhileStmt<out s>
  | ForLoopStmt<out s>
- | AssertStmt<out s, false>
+ | AssertStmt<out s>
  | AssumeStmt<out s>
  | BreakStmt<out s>
  | CalcStmt<out s>
@@ -3639,7 +3639,7 @@ CaseStmt<out NestedMatchCaseStmt/*!*/ c>
  .
 
 /*------------------------------------------------------------------------*/
-AssertStmt<out Statement/*!*/ s, bool inExprContext>
+AssertStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
  Expression e = dummyExpr; Attributes attrs = null;
  IToken dotdotdot = null;
@@ -3650,7 +3650,7 @@ AssertStmt<out Statement/*!*/ s, bool inExprContext>
  .)
  "assert" (. x = t; startToken = t; .)
  { Attribute<ref attrs> }
- ( [ IF(IsLabel(!inExprContext))
+ ( [ IF(IsLabel(true))
  LabelName<out lbl> ":"
  ]
  Expression<out e, false, true>
@@ -4677,7 +4677,7 @@ IfExpression<out Expression e, bool allowLemma, bool allowLambda, bool allowBitw
 /*------------------------------------------------------------------------*/
 StmtInExpr<out Statement s>
 = (. s = dummyStmt; .)
- ( AssertStmt<out s, true>
+ ( AssertStmt<out s>
  | ExpectStmt<out s>
  | AssumeStmt<out s>
  | RevealStmt<out s>

Source/DafnyCore/DafnyCore.csproj

@@ -27,10 +27,12 @@
  <ItemGroup>
  <PackageReference Include="JetBrains.Annotations" Version="2021.1.0" />
  <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="3.7.0" />
+ <PackageReference Include="Microsoft.Extensions.FileSystemGlobbing" Version="5.0.0" />
  <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
  <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
  <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
  <PackageReference Include="Boogie.ExecutionEngine" Version="2.16.4" />
+ <PackageReference Include="Tomlyn" Version="0.16.2" />
  </ItemGroup>
 
  <ItemGroup>

Source/DafnyCore/DafnyOptions.cs

@@ -35,7 +35,8 @@ public enum QuantifierSyntaxOptions {
  public record Options(IDictionary<Option, object> OptionArguments);
 
  public class DafnyOptions : Bpl.CommandLineOptions {
-
+ public static DafnyOptions Default = new DafnyOptions();
+ public ProjectFile ProjectFile { get; set; }
  public bool NonGhostsUseHeap => Allocated == 1 || Allocated == 2;
  public bool AlwaysUseHeap => Allocated == 2;
  public bool CommonHeapUse => Allocated >= 2;

Source/DafnyCore/Options/ICommandSpec.cs

@@ -15,7 +15,7 @@ public interface ICommandSpec {
  static ICommandSpec() {
  FilesArgument = new("file", r => {
  return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList();
- }, true, "input files");
+ }, true, "Dafny input files and/or a Dafny project file");
  }
 
  public static Argument<List<FileInfo>> FilesArgument { get; }