Merge branch 'master' into issue-4939

# Conflicts:
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeTests.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2139.dfy.expect

Source/DafnyCore/Compilers/Python/PythonBackend.cs

@@ -48,10 +48,10 @@ public class PythonBackend : ExecutableBackend {
  }
 
  private static readonly Dictionary<OSPlatform, string> PlatformDefaults = new() {
- {OSPlatform.Linux, "python3"},
- {OSPlatform.Windows, "python"},
- {OSPlatform.FreeBSD, "python3"},
- {OSPlatform.OSX, "python3"},
+ { OSPlatform.Linux, "python3" },
+ { OSPlatform.Windows, "python" },
+ { OSPlatform.FreeBSD, "python3" },
+ { OSPlatform.OSX, "python3" },
  };
  private static string DefaultPythonCommand => PlatformDefaults.SingleOrDefault(
  kv => RuntimeInformation.IsOSPlatform(kv.Key),

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1293,18 +1293,22 @@ public partial class ModuleResolver {
  }
 
  // Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support
- foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
- if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
- // do the following check once per SCC, so call it on each SCC representative
- SccStratosphereCheck(dtd, datatypeDependencies);
- DetermineEqualitySupport(dtd, datatypeDependencies);
+ if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { // because SccStratosphereCheck depends on subset-type/newtype base types being successfully resolved
+ foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
+ if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
+ // do the following check once per SCC, so call it on each SCC representative
+ SccStratosphereCheck(dtd, datatypeDependencies);
+ DetermineEqualitySupport(dtd, datatypeDependencies);
+ }
  }
  }
 
  // Set the SccRepr field of codatatypes
- foreach (var repr in codatatypeDependencies.TopologicallySortedComponents()) {
- foreach (var codt in codatatypeDependencies.GetSCC(repr)) {
- codt.SscRepr = repr;
+ if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
+ foreach (var repr in codatatypeDependencies.TopologicallySortedComponents()) {
+ foreach (var codt in codatatypeDependencies.GetSCC(repr)) {
+ codt.SscRepr = repr;
+ }
  }
  }
 

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs

@@ -28,15 +28,15 @@ class CheckTypeInferenceVisitor : ASTVisitor<TypeInferenceCheckingContext> {
  if (decl is NewtypeDecl newtypeDecl) {
  if (newtypeDecl.Var != null) {
  if (!IsDetermined(newtypeDecl.BaseType.NormalizeExpand())) {
- resolver.ReportError(ResolutionErrors.ErrorId.r_newtype_base_undetermined, newtypeDecl.tok, "newtype's base type is not fully determined; add an explicit type for '{0}'",
- newtypeDecl.Var.Name);
+ resolver.ReportError(ResolutionErrors.ErrorId.r_newtype_base_undetermined, newtypeDecl.tok,
+ $"{newtypeDecl.WhatKind}'s base type is not fully determined; add an explicit type for bound variable '{newtypeDecl.Var.Name}'");
  }
  }
 
  } else if (decl is SubsetTypeDecl subsetTypeDecl) {
  if (!IsDetermined(subsetTypeDecl.Rhs.NormalizeExpand())) {
  resolver.ReportError(ResolutionErrors.ErrorId.r_subset_type_base_undetermined, subsetTypeDecl.tok,
- "subset type's base type is not fully determined; add an explicit type for '{0}'", subsetTypeDecl.Var.Name);
+ $"{subsetTypeDecl.WhatKind}'s base type is not fully determined; add an explicit type for bound variable '{subsetTypeDecl.Var.Name}'");
  }
 
  } else if (decl is DatatypeDecl datatypeDecl) {

Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs

@@ -468,10 +468,14 @@ public class PreTypeConstraints {
  return false;
  }
 
- public void AddConfirmation(CommonConfirmationBag check, PreType preType, IToken tok, string errorFormatString) {
+ public void AddConfirmation(CommonConfirmationBag check, PreType preType, IToken tok, string errorFormatString, Action onProxyAction = null) {
  confirmations.Add(() => {
  if (!ConfirmConstraint(check, preType, null)) {
- PreTypeResolver.ReportError(tok, errorFormatString, preType);
+ if (preType.Normalize() is PreTypeProxy && onProxyAction != null) {
+ onProxyAction();
+ } else {
+ PreTypeResolver.ReportError(tok, errorFormatString, preType);
+ }
  }
  });
  }

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -476,8 +476,8 @@ private PreTypeResolver(ModuleResolver resolver, PreTypeInferenceModuleState pre
  Constraints.AddSubtypeConstraint(super, sub, tok, errorFormatString);
  }
 
- void AddConfirmation(PreTypeConstraints.CommonConfirmationBag check, PreType preType, IToken tok, string errorFormatString) {
- Constraints.AddConfirmation(check, preType, tok, errorFormatString);
+ void AddConfirmation(PreTypeConstraints.CommonConfirmationBag check, PreType preType, IToken tok, string errorFormatString, Action onProxyAction = null) {
+ Constraints.AddConfirmation(check, preType, tok, errorFormatString, onProxyAction);
  }
 
  void AddComparableConstraint(PreType a, PreType b, IToken tok, string errorFormatString) {
@@ -691,12 +691,16 @@ private PreTypeResolver(ModuleResolver resolver, PreTypeInferenceModuleState pre
  Contract.Assert(object.ReferenceEquals(nd.BaseType, nd.Var.Type));
  nd.Var.PreType = nd.BasePreType;
  }
+ var onProxyAction = () => {
+ resolver.ReportError(ResolutionErrors.ErrorId.r_newtype_base_undetermined, nd.tok,
+ $"{nd.WhatKind}'s base type is not fully determined; add an explicit type for bound variable '{nd.Var.Name}'");
+ };
  if (resolver.Options.Get(CommonOptionBag.GeneralNewtypes)) {
  AddConfirmation(PreTypeConstraints.CommonConfirmationBag.IsNewtypeBaseTypeGeneral, nd.BasePreType, nd.tok,
- "a newtype must be based on some non-reference, non-trait, non-ORDINAL type (got {0})");
+ "a newtype must be based on some non-reference, non-trait, non-ORDINAL type (got {0})", onProxyAction);
  } else {
  AddConfirmation(PreTypeConstraints.CommonConfirmationBag.IsNewtypeBaseTypeLegacy, nd.BasePreType, nd.tok,
- "a newtype must be based on some numeric type (got {0})");
+ "a newtype must be based on some numeric type (got {0})", onProxyAction);
  }
  ResolveConstraintAndWitness(nd, true);
 

Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs

@@ -55,6 +55,9 @@ public UnderspecificationDetector(ModuleResolver resolver)
 
  } else if (d is SubsetTypeDecl) {
  var dd = (SubsetTypeDecl)d;
+ if (!DetectUnderspecificationVisitor.IsDetermined(dd.Var.PreType)) {
+ ReportError(dd, $"{dd.WhatKind}'s base type is not fully determined; add an explicit type for bound variable '{dd.Var.Name}'");
+ }
  CheckExpression(dd.Constraint, context);
  if (dd.Witness != null) {
  CheckExpression(dd.Witness, context);
@@ -64,7 +67,7 @@ public UnderspecificationDetector(ModuleResolver resolver)
  var dd = (NewtypeDecl)d;
  if (dd.Var != null) {
  if (!DetectUnderspecificationVisitor.IsDetermined(dd.BasePreType)) {
- ReportError(dd, "newtype's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name);
+ ReportError(dd, $"{dd.WhatKind}'s base type is not fully determined; add an explicit type for bound variable '{dd.Var.Name}'");
  }
  CheckExpression(dd.Constraint, context);
  if (dd.Witness != null) {

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -862,6 +862,9 @@ AND Apply(f,h0,bxs) == Apply(f,h0,bxs)
  return null;
  } else if (typ.IsAbstractType || typ.IsInternalTypeSynonym) {
  return null;
+ } else if (typ.IsTraitType) {
+ Contract.Assert(options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy);
+ return null;
  } else {
  Contract.Assume(false); // unexpected type
  return null;

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OnDemandResolutionCycle.dfy.expect

@@ -3,7 +3,7 @@ OnDemandResolutionCycle.dfy(9,9): Error: Cyclic dependency among declarations: F
 OnDemandResolutionCycle.dfy(7,5): Error: Cyclic dependency among declarations: B -> B -> FB -> b
 OnDemandResolutionCycle.dfy(11,6): Error: Cyclic dependency among declarations: c0 -> c1 -> c0
 OnDemandResolutionCycle.dfy(15,6): Error: Cyclic dependency among declarations: d -> D -> d
-OnDemandResolutionCycle.dfy(14,8): Error: a newtype must be based on some numeric type (got ?1)
+OnDemandResolutionCycle.dfy(14,8): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'x'
 OnDemandResolutionCycle.dfy(19,9): Error: Cyclic dependency among declarations: FE -> E -> FE -> e
 OnDemandResolutionCycle.dfy(17,8): Error: Cyclic dependency among declarations: E -> E -> FE -> e
 OnDemandResolutionCycle.dfy(22,9): Error: Cyclic dependency among declarations: f -> F -> f

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2134.dfy.expect

@@ -1,11 +1,11 @@
 git-issue-2134.dfy(8,12): Error: Cyclic dependency among declarations: P -> A -> B -> P
-git-issue-2134.dfy(5,10): Error: a newtype must be based on some numeric type (got ?1)
+git-issue-2134.dfy(5,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'b'
 git-issue-2134.dfy(15,12): Error: Cyclic dependency among declarations: P -> A -> Q -> B -> P
-git-issue-2134.dfy(12,10): Error: a newtype must be based on some numeric type (got ?1)
+git-issue-2134.dfy(12,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'b'
 git-issue-2134.dfy(22,12): Error: Cyclic dependency among declarations: P -> B -> P
-git-issue-2134.dfy(20,10): Error: a newtype must be based on some numeric type (got ?1)
+git-issue-2134.dfy(20,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'b'
 git-issue-2134.dfy(27,8): Error: Cyclic dependency among declarations: X -> B -> X
-git-issue-2134.dfy(26,10): Error: a newtype must be based on some numeric type (got ?1)
+git-issue-2134.dfy(26,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'b'
 git-issue-2134.dfy(32,11): Error: Cyclic dependency among declarations: X -> B -> X
 git-issue-2134.dfy(31,10): Error: Cyclic dependency among declarations: B -> B -> X
 git-issue-2134.dfy(41,12): Error: Cyclic dependency among declarations: P -> A -> B -> P

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2303.dfy

@@ -1,12 +1,15 @@
-// RUN: %exits-with 2 %verify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"
+
 
 module A {
  newtype int0 = x | true // newtype's base type is not fully determined; add an explicit type for 'x'
 }
 
 module B {
- newtype int0 = x | true
+ newtype int0 = y | true
  const x: int0 := 0 // type for constant 'x' is 'int0', but its initialization value type is 'int'
 }
 
+module C {
+ type int0 = x | true // subset type's base type is not fully determined; add an explicit type for 'x'
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2303.dfy.expect

@@ -1,3 +1,4 @@
-git-issue-2303.dfy(5,10): Error: newtype's base type is not fully determined; add an explicit type for 'x'
+git-issue-2303.dfy(5,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'x'
 git-issue-2303.dfy(10,8): Error: type for constant 'x' is 'int0', but its initialization value type is 'int'
-2 resolution/type errors detected in git-issue-2303.dfy
+git-issue-2303.dfy(14,7): Error: subset type's base type is not fully determined; add an explicit type for bound variable 'x'
+3 resolution/type errors detected in git-issue-2303.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2303.dfy.refresh.expect

@@ -0,0 +1,5 @@
+git-issue-2303.dfy(5,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'x'
+git-issue-2303.dfy(9,10): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'y'
+git-issue-2303.dfy(10,19): Error: integer literal used as if it had type int0
+git-issue-2303.dfy(14,7): Error: subset type's base type is not fully determined; add an explicit type for bound variable 'x'
+4 resolution/type errors detected in git-issue-2303.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946a.dfy

@@ -0,0 +1,20 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype
+
+trait ProgramTrait {
+ method Compute() returns (r: Result)
+}
+
+type Program = ProgramTrait | true // error: 'ProgramTrait' is a bound variable here, and its type is undetermined
+
+datatype Result =
+ | Bounce(next: Program)
+ | Done()
+
+datatype Trivial extends ProgramTrait =
+ Trivial()
+{
+ method Compute() returns (r: Result)
+ {
+ return Done();
+ }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946a.dfy.expect

@@ -0,0 +1,2 @@
+git-issue-4946a.dfy(7,5): Error: subset type's base type is not fully determined; add an explicit type for bound variable 'ProgramTrait'
+1 resolution/type errors detected in git-issue-4946a.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946b.dfy

@@ -0,0 +1,7 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --general-traits=legacy
+
+trait GeneralTrait { }
+trait ReferenceTrait extends object { }
+
+type SubsetType = x: GeneralTrait | true // error: cannot find witness (tried null)
+type Reference = x: ReferenceTrait | true // error: cannot find witness (tried null)

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946b.dfy.expect

@@ -0,0 +1,4 @@
+git-issue-4946b.dfy(6,5): Error: trying witness null: value of expression (of type 'GeneralTrait?') is not known to be an instance of type 'GeneralTrait', because it might be null
+git-issue-4946b.dfy(7,5): Error: trying witness null: value of expression (of type 'ReferenceTrait?') is not known to be an instance of type 'ReferenceTrait', because it might be null
+
+Dafny program verifier finished with 0 verified, 2 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946c.dfy

@@ -0,0 +1,7 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --general-traits=datatype
+
+trait GeneralTrait { }
+trait ReferenceTrait extends object { }
+
+type SubsetType = x: GeneralTrait | true // error: cannot find witness (didn't try anything)
+type Reference = x: ReferenceTrait | true // error: cannot find witness (tried null)

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946c.dfy.expect

@@ -0,0 +1,4 @@
+git-issue-4946c.dfy(6,5): Error: cannot find witness that shows type is inhabited; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
+git-issue-4946c.dfy(7,5): Error: trying witness null: value of expression (of type 'ReferenceTrait?') is not known to be an instance of type 'ReferenceTrait', because it might be null
+
+Dafny program verifier finished with 0 verified, 2 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946d.dfy

@@ -0,0 +1,9 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype --general-newtypes
+
+type Small = x: int | 0 <= x < 10
+
+newtype NewProgram = Small | true // error: 'Small' is a bound variable here, and its type is undetermined
+
+datatype Result =
+ | NewBounce(newNext: NewProgram)
+ | Done()

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946d.dfy.expect

@@ -0,0 +1,2 @@
+git-issue-4946d.dfy(5,8): Error: newtype's base type is not fully determined; add an explicit type for bound variable 'Small'
+1 resolution/type errors detected in git-issue-4946d.dfy

docs/dev/news/4956.fix

@@ -0,0 +1,3 @@
+Fix: check that subset-type variable's type is determined (resolver refresh).
+Fix crash in verifier when there was a previous error in determining subset-type/newtype base type.
+Fix crash in verifier when a subset type has no explicit `witness` clause and has a non-reference trait as its base type.