diff --git a/.github/workflows/nightly-build.yml b/.github/workflows/nightly-build.yml index a64c037e76..bfe5ae7e35 100644 --- a/.github/workflows/nightly-build.yml +++ b/.github/workflows/nightly-build.yml @@ -30,12 +30,3 @@ jobs: ref: master secrets: nuget_api_key: ${{ secrets.NUGET_API_KEY }} - - nightly-build-for-4-4: - if: github.repository_owner == 'dafny-lang' - uses: ./.github/workflows/nightly-build-reusable.yml - with: - ref: 4.4 - publish-prerelease: true - secrets: - nuget_api_key: ${{ secrets.NUGET_API_KEY }} diff --git a/Source/DafnyCore/AST/Formatting.dfy b/Source/DafnyCore/AST/Formatting.dfy index 819e027141..0d9269e440 100644 --- a/Source/DafnyCore/AST/Formatting.dfy +++ b/Source/DafnyCore/AST/Formatting.dfy @@ -31,7 +31,7 @@ module {:extern "Microsoft"} {:options "-functionSyntax:4"} Microsoft { ensures allocated(x) { } - /** Prints the entire program while fixing identation, based on + /** Prints the entire program while fixing indentation, based on 1) indentation information provided by the IIndentationFormatter reindent 2) Reindentation algorithm provided by the same reindent */ method ReindentProgramFromFirstToken(firstToken: IToken, reindent: IIndentationFormatter) returns (s: CsString) diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index 21b2959b1e..3515cb202a 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -170,4 +170,6 @@ public interface RedirectingTypeDecl : ICallable { SubsetTypeDecl.WKind WitnessKind { get; } Expression/*?*/ Witness { get; } // non-null iff WitnessKind is Compiled or Ghost FreshIdGenerator IdGenerator { get; } + + [FilledInDuringResolution] bool ConstraintIsCompilable { get; set; } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index 215d2439b4..8455b0f63e 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/Source/DafnyCore/AST/SystemModuleManager.cs @@ -103,6 +103,7 @@ public SystemModuleManager(DafnyOptions options) { NatDecl = new SubsetTypeDecl(RangeToken.NoToken, new Name("nat"), new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false), new List(), SystemModule, bvNat, natConstraint, SubsetTypeDecl.WKind.CompiledZero, null, ax); + ((RedirectingTypeDecl)NatDecl).ConstraintIsCompilable = true; SystemModule.SourceDecls.Add(NatDecl); // create trait 'object' ObjectDecl = new TraitDecl(RangeToken.NoToken, new Name("object"), SystemModule, new List(), new List(), DontCompile(), false, null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index abd9b684fd..ce41305f19 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -15,6 +15,12 @@ public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, Redirect public SubsetTypeDecl.WKind WitnessKind { get; set; } = SubsetTypeDecl.WKind.CompiledZero; public Expression/*?*/ Witness { get; set; } // non-null iff WitnessKind is Compiled or Ghost [FilledInDuringResolution] public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers) + + [FilledInDuringResolution] bool RedirectingTypeDecl.ConstraintIsCompilable { get; set; } + + [FilledInDuringResolution] public bool NativeTypeRangeImpliesAllConstraints; // indicates that all values in the range of the native type are values of the newtype + [FilledInDuringResolution] public bool TargetTypeCoversAllBitPatterns; // "target complete" -- indicates that any bit pattern that can fill the target type is a value of the newtype + public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Type baseType, List parentTraits, List members, Attributes attributes, bool isRefining) : base(rangeToken, name, module, new List(), members, attributes, isRefining, parentTraits) { @@ -24,6 +30,7 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Ty Contract.Requires(isRefining ^ (baseType != null)); Contract.Requires(members != null); BaseType = baseType; + this.NewSelfSynonym(); } public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, BoundVar bv, Expression constraint, SubsetTypeDecl.WKind witnessKind, Expression witness, List parentTraits, List members, Attributes attributes, bool isRefining) diff --git a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs index a7549b338a..8d235f2708 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs @@ -11,8 +11,10 @@ public class SubsetTypeDecl : TypeSynonymDecl, RedirectingTypeDecl, ICanAutoReve public enum WKind { CompiledZero, Compiled, Ghost, OptOut, Special } public readonly WKind WitnessKind; public Expression/*?*/ Witness; // non-null iff WitnessKind is Compiled or Ghost - [FilledInDuringResolution] public bool ConstraintIsCompilable; [FilledInDuringResolution] public bool CheckedIfConstraintIsCompilable = false; // Set to true lazily by the Resolver when the Resolver fills in "ConstraintIsCompilable". + + [FilledInDuringResolution] bool RedirectingTypeDecl.ConstraintIsCompilable { get; set; } + public SubsetTypeDecl(RangeToken rangeToken, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, BoundVar id, Expression constraint, WKind witnessKind, Expression witness, Attributes attributes) diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index 4017f3bdad..308b7f542f 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -64,6 +64,12 @@ public Type RhsWithArgumentIgnoringScope(List typeArgs) { ModuleDefinition RedirectingTypeDecl.Module { get { return EnclosingModuleDefinition; } } BoundVar RedirectingTypeDecl.Var { get { return null; } } Expression RedirectingTypeDecl.Constraint { get { return null; } } + + bool RedirectingTypeDecl.ConstraintIsCompilable { + get => false; + set => throw new NotSupportedException(); + } + SubsetTypeDecl.WKind RedirectingTypeDecl.WitnessKind { get { return SubsetTypeDecl.WKind.CompiledZero; } } Expression RedirectingTypeDecl.Witness { get { return null; } } FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index d0507a351b..6baad4d367 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -292,14 +292,15 @@ public Type UseInternalSynonym() { [System.Diagnostics.Contracts.Pure] public abstract bool Equals(Type that, bool keepConstraints = false); - public bool IsBoolType { get { return NormalizeExpand() is BoolType; } } - public bool IsCharType { get { return NormalizeExpand() is CharType; } } - public bool IsIntegerType { get { return NormalizeExpand() is IntType; } } - public bool IsRealType { get { return NormalizeExpand() is RealType; } } - public bool IsBigOrdinalType { get { return NormalizeExpand() is BigOrdinalType; } } - public bool IsBitVectorType { get { return AsBitVectorType != null; } } - public bool IsStringType { get { return AsSeqType?.Arg.IsCharType == true; } } - public BitvectorType AsBitVectorType { get { return NormalizeExpand() as BitvectorType; } } + public bool IsBoolType => NormalizeExpand() is BoolType; + public bool IsCharType => NormalizeExpand() is CharType; + public bool IsIntegerType => NormalizeExpand() is IntType; + public bool IsRealType => NormalizeExpand() is RealType; + public bool IsBigOrdinalType => NormalizeExpand() is BigOrdinalType; + public bool IsBitVectorType => AsBitVectorType != null; + public bool IsStringType => AsSeqType?.Arg.IsCharType == true; + public BitvectorType AsBitVectorType => NormalizeExpand() as BitvectorType; + public bool IsNumericBased() { var t = NormalizeExpand(); return t.IsIntegerType || t.IsRealType || t.AsNewtype != null; @@ -702,58 +703,32 @@ public bool IsArrowTypeWithoutPreconditions { } } } - public bool IsArrowType { - get { return AsArrowType != null; } - } - public ArrowType AsArrowType { - get { - var t = NormalizeExpand(); - return t as ArrowType; - } - } + public bool IsArrowType => AsArrowType != null; + + public ArrowType AsArrowType => NormalizeExpand() as ArrowType; + + public bool IsMapType => NormalizeExpand() is MapType { Finite: true }; + + public bool IsIMapType => NormalizeExpand() is MapType { Finite: false }; + + public bool IsISetType => NormalizeExpand() is SetType { Finite: false }; - public bool IsMapType { - get { - var t = NormalizeExpand() as MapType; - return t != null && t.Finite; - } - } - public bool IsIMapType { - get { - var t = NormalizeExpand() as MapType; - return t != null && !t.Finite; - } - } - public bool IsISetType { - get { - var t = NormalizeExpand() as SetType; - return t != null && !t.Finite; - } - } public NewtypeDecl AsNewtype { get { var udt = NormalizeExpand() as UserDefinedType; - return udt == null ? null : udt.ResolvedClass as NewtypeDecl; + return udt?.ResolvedClass as NewtypeDecl; } } public TypeSynonymDecl AsTypeSynonym { get { var udt = this as UserDefinedType; // note, it is important to use 'this' here, not 'this.NormalizeExpand()' - if (udt == null) { - return null; - } else { - return udt.ResolvedClass as TypeSynonymDecl; - } + return udt?.ResolvedClass as TypeSynonymDecl; } } public InternalTypeSynonymDecl AsInternalTypeSynonym { get { var udt = this as UserDefinedType; // note, it is important to use 'this' here, not 'this.NormalizeExpand()' - if (udt == null) { - return null; - } else { - return udt.ResolvedClass as InternalTypeSynonymDecl; - } + return udt?.ResolvedClass as InternalTypeSynonymDecl; } } public RedirectingTypeDecl AsRedirectingType { @@ -769,59 +744,33 @@ public RedirectingTypeDecl AsRedirectingType { public RevealableTypeDecl AsRevealableType { get { var udt = this as UserDefinedType; - if (udt == null) { - return null; - } else { - return (udt.ResolvedClass as RevealableTypeDecl); - } - } - } - public bool IsRevealableType { - get { return AsRevealableType != null; } - } - public bool IsDatatype { - get { - return AsDatatype != null; + return udt?.ResolvedClass as RevealableTypeDecl; } } + public bool IsRevealableType => AsRevealableType != null; + + public bool IsDatatype => AsDatatype != null; + public DatatypeDecl AsDatatype { get { var udt = NormalizeExpand() as UserDefinedType; - if (udt == null) { - return null; - } else { - return udt.ResolvedClass as DatatypeDecl; - } - } - } - public bool IsIndDatatype { - get { - return AsIndDatatype != null; + return udt?.ResolvedClass as DatatypeDecl; } } + public bool IsIndDatatype => AsIndDatatype != null; + public IndDatatypeDecl AsIndDatatype { get { var udt = NormalizeExpand() as UserDefinedType; - if (udt == null) { - return null; - } else { - return udt.ResolvedClass as IndDatatypeDecl; - } - } - } - public bool IsCoDatatype { - get { - return AsCoDatatype != null; + return udt?.ResolvedClass as IndDatatypeDecl; } } + public bool IsCoDatatype => AsCoDatatype != null; + public CoDatatypeDecl AsCoDatatype { get { var udt = NormalizeExpand() as UserDefinedType; - if (udt == null) { - return null; - } else { - return udt.ResolvedClass as CoDatatypeDecl; - } + return udt?.ResolvedClass as CoDatatypeDecl; } } public bool InvolvesCoDatatype { @@ -829,23 +778,18 @@ public bool InvolvesCoDatatype { return IsCoDatatype; // TODO: should really check structure of the type recursively } } - public bool IsTypeParameter { - get { - return AsTypeParameter != null; - } - } - public bool IsInternalTypeSynonym { - get { return AsInternalTypeSynonym != null; } - } + public bool IsTypeParameter => AsTypeParameter != null; + + public bool IsInternalTypeSynonym => AsInternalTypeSynonym != null; + public TypeParameter AsTypeParameter { get { var ct = NormalizeExpandKeepConstraints() as UserDefinedType; return ct?.ResolvedClass as TypeParameter; } } - public bool IsAbstractType { - get { return AsAbstractType != null; } - } + public bool IsAbstractType => AsAbstractType != null; + public AbstractTypeDecl AsAbstractType { get { var udt = this.Normalize() as UserDefinedType; // note, it is important to use 'this.Normalize()' here, not 'this.NormalizeExpand()' diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index 61a7c3b705..f5c283f664 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs @@ -3291,6 +3291,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody, } else { Contract.Assert(false, $"not implemented for C#: {e.E.Type} -> {e.ToType}"); } + } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) { + wr.Append(Expr(e.E, inLetExprBody, wStmts)); } else { Contract.Assert(false, $"not implemented for C#: {e.E.Type} -> {e.ToType}"); } diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs index 7f7b64650c..1db454938d 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs @@ -2356,11 +2356,14 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody, wr.Write(".{0}()", Capitalize(GetNativeTypeName(nt))); } } - } else { - Contract.Assert(e.E.Type.IsBigOrdinalType); + } else if (e.E.Type.IsBigOrdinalType) { Contract.Assert(e.ToType.IsNumericBased(Type.NumericPersuasion.Int)); // identity will do wr.Append(Expr(e.E, inLetExprBody, wStmts)); + } else { + // identity will do + Contract.Assert(e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null); + wr.Append(Expr(e.E, inLetExprBody, wStmts)); } } diff --git a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs index ea506f6cae..359434bd4c 100644 --- a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs @@ -3576,6 +3576,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody, wr.Write(".{0}()", Capitalize(GetNativeTypeName(nt))); } } + } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) { + wr.Append(Expr(e.E, inLetExprBody, wStmts)); } else { Contract.Assert(false, $"not implemented for go: {e.E.Type} -> {e.ToType}"); } diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index face2a1e8d..d2c7254b86 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -4186,6 +4186,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody, } else { Contract.Assert(false, $"not implemented for java: {fromType} -> {toType}"); } + } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) { + wr.Append(Expr(e.E, inLetExprBody, wStmts)); } else { Contract.Assert(false, $"not implemented for java: {fromType} -> {toType}"); } diff --git a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs index 249c8395a6..fc31dc63a2 100644 --- a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs +++ b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs @@ -2432,6 +2432,8 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody, if (e.ToType.IsCharType) { wr.Write(").toNumber())"); } + } else if (e.E.Type.Equals(e.ToType) || e.E.Type.AsNewtype != null || e.ToType.AsNewtype != null) { + wr.Append(Expr(e.E, inLetExprBody, wStmts)); } else { Contract.Assert(false, $"not implemented for javascript: {e.E.Type} -> {e.ToType}"); } diff --git a/Source/DafnyCore/Compilers/Python/PythonBackend.cs b/Source/DafnyCore/Compilers/Python/PythonBackend.cs index 41189692bb..247f858e9a 100644 --- a/Source/DafnyCore/Compilers/Python/PythonBackend.cs +++ b/Source/DafnyCore/Compilers/Python/PythonBackend.cs @@ -4,6 +4,7 @@ using System.IO; using System.Linq; using System.Text.RegularExpressions; +using System.Runtime.InteropServices; namespace Microsoft.Dafny.Compilers; @@ -46,6 +47,17 @@ private static string FindModuleName(string externFilename) { return Path.GetExtension(externFilename) == ".py" ? Path.GetFileNameWithoutExtension(externFilename) : null; } + private static readonly Dictionary PlatformDefaults = new() { + {OSPlatform.Linux, "python3"}, + {OSPlatform.Windows, "python"}, + {OSPlatform.FreeBSD, "python3"}, + {OSPlatform.OSX, "python3"}, + }; + private static string DefaultPythonCommand => PlatformDefaults.SingleOrDefault( + kv => RuntimeInformation.IsOSPlatform(kv.Key), + new(OSPlatform.Linux, "python3") + ).Value; + bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextWriter outputWriter) { // Grossly, we need to look in the file to figure out where to put it var moduleName = FindModuleName(externFilename); @@ -88,7 +100,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target } } if (!runAfterCompile) { - var psi = PrepareProcessStartInfo("python3"); + var psi = PrepareProcessStartInfo(DefaultPythonCommand); psi.Arguments = $"-m compileall -q {Path.GetDirectoryName(targetFilename)}"; return 0 == RunProcess(psi, outputWriter, outputWriter, "Error while compiling Python files."); } @@ -99,7 +111,7 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, TextWriter errorWriter) { Contract.Requires(targetFilename != null || otherFileNames.Count == 0); - var psi = PrepareProcessStartInfo("python3", Options.MainArgs.Prepend(targetFilename)); + var psi = PrepareProcessStartInfo(DefaultPythonCommand, Options.MainArgs.Prepend(targetFilename)); psi.EnvironmentVariables["PYTHONIOENCODING"] = "utf8"; return 0 == RunProcess(psi, outputWriter, errorWriter); } diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index 0e7a3d1527..82673af45f 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs @@ -669,10 +669,10 @@ private ConcreteSyntaxTree CreateGuardedForeachLoop( ) { wr = CreateForeachLoop(tmpVarName, collectionElementType, tok, out var collectionWriter, wr); collection(collectionWriter); - wr = MaybeInjectSubtypeConstraint(tmpVarName, collectionElementType, boundVar.Type, inLetExprBody, tok, wr); + wr = MaybeInjectSubtypeConstraintWrtTraits(tmpVarName, collectionElementType, boundVar.Type, inLetExprBody, tok, wr); EmitDowncastVariableAssignment(IdName(boundVar), boundVar.Type, tmpVarName, collectionElementType, introduceBoundVar, tok, wr); - wr = MaybeInjectSubsetConstraint(boundVar, boundVar.Type, collectionElementType, inLetExprBody, tok, wr); + wr = MaybeInjectSubsetConstraint(boundVar, boundVar.Type, inLetExprBody, tok, wr); return wr; } @@ -686,7 +686,7 @@ protected abstract Action GetSubtypeCondition( string tmpVarName, Type boundVarType, IToken tok, ConcreteSyntaxTree wPreconditions); /// - /// Emit an (already verified) downcast assignment like: + /// Emit an upcast or (already verified) downcast assignment like: /// /// var boundVarName:boundVarType := tmpVarName as boundVarType; /// [[bodyWriter]] @@ -1410,6 +1410,13 @@ protected abstract void EmitMapDisplay(MapType mt, IToken tok, List protected abstract string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr); + /// + /// Returns a pair (ty, f) where + /// * "f" is a closure that, to a given writer, emits code that enumerates an integer-valued range from + /// "wLo" to "wHi" using the target type of "type" + /// * "ty" is a Dafny type whose target type is the same as the target type of "type" + /// It is assumed that "type" is some integer-based type (not a bitvector type, for example). + /// protected virtual (Type, Action) EmitIntegerRange(Type type, Action wLo, Action wHi) { Type result; if (AsNativeType(type) != null) { @@ -3776,6 +3783,12 @@ protected virtual ConcreteSyntaxTree EmitAnd(Action lhs, Con return wr; } + /// + /// Returns a type whose target type is the same as the target type of the values returned by the emitted enumeration. + /// The output value of "collectionWriter" is an action that emits the enumeration. + /// Note that, while the values returned bny the enumeration have the target representation of "bv.Type", they may + /// not be legal "bv.Type" values -- that is, it could be that "bv.Type" has further constraints that need to be checked. + /// Type CompileCollection(ComprehensionExpr.BoundedPool bound, IVariable bv, bool inLetExprBody, bool includeDuplicates, Substituter/*?*/ su, out Action collectionWriter, ConcreteSyntaxTree wStmts, List/*?*/ bounds = null, List/*?*/ boundVars = null, int boundIndex = 0) { @@ -5527,13 +5540,13 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn var tmpVarName = ProtectedFreshId(e is ForallExpr ? "_forall_var_" : "_exists_var_"); ConcreteSyntaxTree newWBody = CreateLambda(new List { collectionElementType }, e.tok, new List { tmpVarName }, Type.Bool, wBody, wStmts, untyped: true); wStmts = newWBody.Fork(); - newWBody = MaybeInjectSubtypeConstraint( + newWBody = MaybeInjectSubtypeConstraintWrtTraits( tmpVarName, collectionElementType, bv.Type, inLetExprBody, e.tok, newWBody, true, e is ForallExpr); EmitDowncastVariableAssignment( IdName(bv), bv.Type, tmpVarName, collectionElementType, true, e.tok, newWBody); newWBody = MaybeInjectSubsetConstraint( - bv, bv.Type, collectionElementType, inLetExprBody, e.tok, newWBody, true, e is ForallExpr); + bv, bv.Type, inLetExprBody, e.tok, newWBody, isReturning: true, elseReturnValue: e is ForallExpr); wBody = newWBody; } EmitExpr(logicalBody, inLetExprBody, wBody, wStmts); @@ -5698,7 +5711,7 @@ protected void WriteTypeDescriptors(TopLevelDecl decl, List typeArguments, /// ... /// } /// - /// MaybeInjectSubtypeConstraint emits a subtype constraint that tmpVarName should be of type boundVarType, typically of the form + /// MaybeInjectSubtypeConstraintWrtTraits emits a subtype constraint that tmpVarName should be of type boundVarType, typically of the form /// /// if([tmpVarName] is [boundVarType]) { /// // This is where 'wr' will write @@ -5708,19 +5721,21 @@ protected void WriteTypeDescriptors(TopLevelDecl decl, List typeArguments, /// to use in the lambdas used by forall and exists statements: /// /// if([tmpVarName] is [boundVarType]) { - /// return // This is where 'wr' will write + /// // This is where 'wr' will write /// } else { /// return [elseReturnValue]; /// } /// /// - /// - private ConcreteSyntaxTree MaybeInjectSubtypeConstraint(string tmpVarName, - Type collectionElementType, Type boundVarType, bool inLetExprBody, - IToken tok, ConcreteSyntaxTree wr, bool isReturning = false, bool elseReturnValue = false - ) { - var iterationValuesNeedToBeChecked = IsTargetSupertype(collectionElementType, boundVarType); - if (iterationValuesNeedToBeChecked) { + private ConcreteSyntaxTree MaybeInjectSubtypeConstraintWrtTraits(string tmpVarName, Type collectionElementType, Type boundVarType, + bool inLetExprBody, IToken tok, ConcreteSyntaxTree wr, + bool isReturning = false, bool elseReturnValue = false) { + + if (Type.IsSupertype(boundVarType, collectionElementType)) { + // Every value of the collection enumeration is a value of the bound variable's type, so the assignment can be done unconditionally. + // (The caller may still need to insert an upcast, depending on the target language.) + } else { + // We need to perform a run-time check to see if the collection value can be assigned to the bound variable. var preconditions = wr.Fork(); var conditions = GetSubtypeCondition(tmpVarName, boundVarType, tok, preconditions); if (conditions == null) { @@ -5732,9 +5747,7 @@ private ConcreteSyntaxTree MaybeInjectSubtypeConstraint(string tmpVarName, wr = EmitBlock(wr); var wStmts = wr.Fork(); wr = EmitReturnExpr(wr); - var elseLiteral = new LiteralExpr(tok, elseReturnValue) { - Type = Type.Bool - }; + var elseLiteral = Expression.CreateBoolLiteral(tok, elseReturnValue); EmitExpr(elseLiteral, inLetExprBody, wr, wStmts); } wr = thenWriter; @@ -5743,50 +5756,48 @@ private ConcreteSyntaxTree MaybeInjectSubtypeConstraint(string tmpVarName, return wr; } + /// + /// If needed, emit an if-statement wrapper that checks that the value stored in "boundVar" satisfies any (subset-type or newtype) constraints + /// of "boundVarType". + /// private ConcreteSyntaxTree MaybeInjectSubsetConstraint(IVariable boundVar, Type boundVarType, - Type collectionElementType, bool inLetExprBody, - IToken tok, ConcreteSyntaxTree wr, bool isReturning = false, bool elseReturnValue = false, - bool isSubfiltering = false) { - if (!boundVarType.Equals(collectionElementType, true) && - boundVarType.NormalizeExpand(true) is UserDefinedType { - TypeArgs: var typeArgs, - ResolvedClass: - SubsetTypeDecl { - TypeArgs: var typeParametersArgs, - Var: var variable, - Constraint: var constraint + bool inLetExprBody, IToken tok, ConcreteSyntaxTree wr, + bool isReturning = false, bool elseReturnValue = false, bool isSubfiltering = false) { + + if (boundVarType.NormalizeExpandKeepConstraints() is UserDefinedType { ResolvedClass: RedirectingTypeDecl and var declWithConstraint } udt) { + if (declWithConstraint is SubsetTypeDecl or NewtypeDecl { NativeTypeRangeImpliesAllConstraints: false }) { + // the type is a subset type or newtype with non-trivial constraints + + var baseType = (declWithConstraint.Var?.Type ?? ((NewtypeDecl)declWithConstraint).BaseType).NormalizeExpandKeepConstraints(); + if (baseType is UserDefinedType { ResolvedClass: SubsetTypeDecl or NewtypeDecl } normalizedVariableType) { + wr = MaybeInjectSubsetConstraint(boundVar, normalizedVariableType, + inLetExprBody, tok, wr, isReturning: isReturning, elseReturnValue: elseReturnValue, isSubfiltering: true); + } + + if (declWithConstraint.Var != null) { + var typeMap = TypeParameter.SubstitutionMap(declWithConstraint.TypeArgs, udt.TypeArgs); + var instantiatedBaseType = baseType.Subst(typeMap); + var theValue = new ConversionExpr(tok, new IdentifierExpr(tok, boundVar), instantiatedBaseType) { Type = instantiatedBaseType }; + var subContract = new Substituter(null, + new Dictionary() { + {declWithConstraint.Var, theValue} + }, + typeMap + ); + var constraintInContext = subContract.Substitute(declWithConstraint.Constraint); + var wStmts = wr.Fork(); + var thenWriter = EmitIf(out var guardWriter, hasElse: isReturning, wr); + EmitExpr(constraintInContext, inLetExprBody, guardWriter, wStmts); + if (isReturning) { + var elseBranch = wr; + elseBranch = EmitBlock(elseBranch); + elseBranch = EmitReturnExpr(elseBranch); + wStmts = elseBranch.Fork(); + EmitExpr(new LiteralExpr(tok, elseReturnValue), inLetExprBody, elseBranch, wStmts); } - }) { - if (variable.Type.NormalizeExpandKeepConstraints() is UserDefinedType { - ResolvedClass: SubsetTypeDecl - } normalizedVariableType) { - wr = MaybeInjectSubsetConstraint(boundVar, normalizedVariableType, collectionElementType, - inLetExprBody, tok, wr, isReturning, elseReturnValue, true); - } - - var bvIdentifier = new IdentifierExpr(tok, boundVar); - var typeParameters = TypeParameter.SubstitutionMap(typeParametersArgs, typeArgs); - var subContract = new Substituter(null, - new Dictionary() - { - {variable, bvIdentifier} - }, - new Dictionary( - typeParameters - ) - ); - var constraintInContext = subContract.Substitute(constraint); - var wStmts = wr.Fork(); - var thenWriter = EmitIf(out var guardWriter, hasElse: isReturning, wr); - EmitExpr(constraintInContext, inLetExprBody, guardWriter, wStmts); - if (isReturning) { - var elseBranch = wr; - elseBranch = EmitBlock(elseBranch); - elseBranch = EmitReturnExpr(elseBranch); - wStmts = elseBranch.Fork(); - EmitExpr(new LiteralExpr(tok, elseReturnValue), inLetExprBody, elseBranch, wStmts); - } - wr = thenWriter; + wr = thenWriter; + } + } } if (isReturning && !isSubfiltering) { diff --git a/Source/DafnyCore/Generic/ErrorReporter.cs b/Source/DafnyCore/Generic/ErrorReporter.cs index 60a6b980fc..6e57bc90ad 100644 --- a/Source/DafnyCore/Generic/ErrorReporter.cs +++ b/Source/DafnyCore/Generic/ErrorReporter.cs @@ -58,7 +58,7 @@ public void Error(MessageSource source, Enum errorId, IToken tok, string format, Contract.Requires(tok != null); Contract.Requires(format != null); Contract.Requires(args != null); - Error(source, errorId.ToString(), tok, String.Format(format, args)); + Error(source, errorId.ToString(), tok, string.Format(format, args)); } public void Error(MessageSource source, Enum errorId, IToken tok, string msg) { diff --git a/Source/DafnyCore/Resolver/BoundsDiscovery.cs b/Source/DafnyCore/Resolver/BoundsDiscovery.cs index f7ccac387f..8ac1512104 100644 --- a/Source/DafnyCore/Resolver/BoundsDiscovery.cs +++ b/Source/DafnyCore/Resolver/BoundsDiscovery.cs @@ -303,7 +303,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte // Note, in the following loop, it's important to go backwards, because DiscoverAllBounds_Aux_SingleVar assumes "knownBounds" has been // filled in for higher-indexed variables. for (var j = bvars.Count; 0 <= --j;) { - var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity, knownBounds); + var bounds = DiscoverAllBounds_Aux_SingleVar(bvars, j, expr, polarity, knownBounds, out _); knownBounds[j] = ComprehensionExpr.BoundedPool.GetBest(bounds); #if DEBUG_PRINT if (knownBounds[j] is ComprehensionExpr.IntBoundedPool) { @@ -321,9 +321,11 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte return knownBounds; } - public static List DiscoverAllBounds_SingleVar(VT v, Expression expr) where VT : IVariable { + public static List DiscoverAllBounds_SingleVar(VT v, Expression expr, + out bool constraintConsistsSolelyOfRangeConstraints) where VT : IVariable { expr = Expression.CreateAnd(GetImpliedTypeConstraint(v, v.Type), expr); - return DiscoverAllBounds_Aux_SingleVar(new List { v }, 0, expr, true, new List() { null }); + return DiscoverAllBounds_Aux_SingleVar(new List { v }, 0, expr, true, + new List() { null }, out constraintConsistsSolelyOfRangeConstraints); } /// @@ -331,7 +333,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte /// that is not bounded. /// private static List DiscoverAllBounds_Aux_SingleVar(List bvars, int j, Expression expr, - bool polarity, List knownBounds) where VT : IVariable { + bool polarity, List knownBounds, out bool constraintConsistsSolelyOfRangeConstraints) where VT : IVariable { Contract.Requires(bvars != null); Contract.Requires(0 <= j && j < bvars.Count); Contract.Requires(expr != null); @@ -354,7 +356,14 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte } // Go through the conjuncts of the range expression to look for bounds. + // Only very specific conjuncts qualify for "constraintConsistsSolelyOfRangeConstraints". To make the bookkeeping + // of these simple, we count the total number of conjuncts and the number of qualifying conjuncts. Then, after the + // loop, we can compare these. + var totalNumberOfConjuncts = 0; + var conjunctsQualifyingAsRangeConstraints = 0; foreach (var conjunct in NormalizedConjuncts(expr, polarity)) { + totalNumberOfConjuncts++; + if (conjunct is IdentifierExpr) { var ide = (IdentifierExpr)conjunct; if (ide.Var == (IVariable)bv) { @@ -426,6 +435,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte case BinaryExpr.ResolvedOpcode.SeqEq: case BinaryExpr.ResolvedOpcode.MultiSetEq: case BinaryExpr.ResolvedOpcode.MapEq: + conjunctsQualifyingAsRangeConstraints++; var otherOperand = whereIsBv == 0 ? e1 : e0; bounds.Add(new ComprehensionExpr.ExactBoundedPool(otherOperand)); break; @@ -435,6 +445,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte throw new cce.UnreachableException(); // promised by postconditions of NormalizedConjunct case BinaryExpr.ResolvedOpcode.Lt: if (e0.Type.IsNumericBased(Type.NumericPersuasion.Int)) { + conjunctsQualifyingAsRangeConstraints++; if (whereIsBv == 0) { // bv < E bounds.Add(new ComprehensionExpr.IntBoundedPool(null, e1)); @@ -445,6 +456,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte } break; case BinaryExpr.ResolvedOpcode.Le: + conjunctsQualifyingAsRangeConstraints++; if (e0.Type.IsNumericBased(Type.NumericPersuasion.Int)) { if (whereIsBv == 0) { // bv <= E @@ -469,6 +481,7 @@ protected override bool VisitOneExpression(Expression expr, BoundsDiscoveryConte break; } } + constraintConsistsSolelyOfRangeConstraints = conjunctsQualifyingAsRangeConstraints == totalNumberOfConjuncts; return bounds; } diff --git a/Source/DafnyCore/Resolver/ConstantFolder.cs b/Source/DafnyCore/Resolver/ConstantFolder.cs new file mode 100644 index 0000000000..8ff8fa2a50 --- /dev/null +++ b/Source/DafnyCore/Resolver/ConstantFolder.cs @@ -0,0 +1,487 @@ +//----------------------------------------------------------------------------- +// +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Numerics; +using System.Diagnostics.Contracts; +using JetBrains.Annotations; +using static Microsoft.Dafny.ResolutionErrors; + +namespace Microsoft.Dafny { + class ConstantFolder { + /// + /// Returns the largest value that can be stored in bitvector type "t". + /// + public static BigInteger MaxBv(Type t) { + Contract.Requires(t != null); + Contract.Requires(t.IsBitVectorType); + return MaxBv(t.AsBitVectorType.Width); + } + + /// + /// Returns the largest value that can be stored in bitvector type of "bits" width. + /// + public static BigInteger MaxBv(int bits) { + Contract.Requires(0 <= bits); + return BigInteger.Pow(new BigInteger(2), bits) - BigInteger.One; + } + + /// + /// Folds "e" into an integer literal, if possible. + /// Returns "null" if not possible (or not easy). + /// + public static BigInteger? TryFoldInteger(Expression e) { + var ee = GetAnyConst(e.Resolved ?? e, new Stack()); + return ee as BigInteger?; + } + + public static bool IsUnconstrainedType(Type t) { + return AsUnconstrainedType(t) != null; + } + + /// + /// Returns null if the argument is a constrained newtype (recursively) + /// Returns the transitive base type if the argument is recursively unconstrained + /// + public static Type AsUnconstrainedType(Type t) { + while (true) { + if (t.AsNewtype == null) { + return t; + } + + if (t.AsNewtype.Constraint != null) { + return null; + } + + t = t.AsNewtype.BaseType; + } + } + + /// + /// Try to fold "e" into constants. + /// Return null if folding is not possible. + /// If an operation is undefined (divide by zero, conversion out of range, etc.), then null is returned. + /// + /// Caution: This method defines the semantics of some expressions. It is important that these be the same + /// as what the verifier and compilers use. For example, it is essential that no undefined expressions + /// are folded. Yet, this method is likely to receive much less testing than the verifier and compiler, + /// since it's not common for all of these expressions to appear in expressions where folding is applied. + /// + [CanBeNull] + static object GetAnyConst(Expression e, Stack constants) { + e = e.Resolved; + + if (e is LiteralExpr l) { + return l.Value; + + } else if (e is UnaryOpExpr un) { + if (un.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot && GetAnyConst(un.E, constants) is bool b) { + return !b; + } + if (un.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BVNot && GetAnyConst(un.E, constants) is BigInteger i) { + return ((BigInteger.One << un.Type.AsBitVectorType.Width) - 1) ^ i; + } + // TODO: This only handles strings; generalize to other collections? + if (un.ResolvedOp == UnaryOpExpr.ResolvedOpcode.SeqLength && GetAnyConst(un.E, constants) is string ss) { + return (BigInteger)(ss.Length); + } + + } else if (e is MemberSelectExpr m) { + if (m.Member is ConstantField { IsStatic: true, Rhs: { } } c) { + // This aspect of type resolution happens before the check for cyclic references + // so we have to do a check here as well. If cyclic, null is silently returned, + // counting on the later error message to alert the user. + if (constants.Contains(c)) { + return null; + } + constants.Push(c); + var o = GetAnyConst(c.Rhs, constants); + constants.Pop(); + return o; + } else if (m.Member is SpecialField { Name: "Floor" }) { + var ee = GetAnyConst(m.Obj, constants); + if (ee != null && m.Obj.Type.IsNumericBased(Type.NumericPersuasion.Real)) { + ((BaseTypes.BigDec)ee).FloorCeiling(out var f, out _); + return f; + } + } + + } else if (e is BinaryExpr bin) { + var e0 = GetAnyConst(bin.E0, constants); + if (e0 == null) { + return null; + } + var e1 = GetAnyConst(bin.E1, constants); + + if (bin.E0.Type == Type.Bool && bin.E1.Type == Type.Bool) { + return FoldBoolean(bin, (bool)e0, (bool?)e1); + } + + if (e1 == null) { + return null; + } + + if (bin.E0.Type.IsNumericBased(Type.NumericPersuasion.Int) && bin.E1.Type.IsNumericBased(Type.NumericPersuasion.Int)) { + return FoldInteger(bin, (BigInteger)e0, (BigInteger)e1); + } else if (bin.E0.Type.IsBitVectorType && (bin.E1.Type.IsBitVectorType || bin.E1.Type.IsNumericBased(Type.NumericPersuasion.Int))) { + return FoldBitvector(bin, (BigInteger)e0, (BigInteger)e1); + } else if (bin.E0.Type.IsNumericBased(Type.NumericPersuasion.Real) && bin.E1.Type.IsNumericBased(Type.NumericPersuasion.Real)) { + return FoldReal(bin, (BaseTypes.BigDec)e0, (BaseTypes.BigDec)e1); + } else if (e0 is string s0 && e1 is string s1) { + return FoldCharOrString(bin, s0, s1); + } + + } else if (e is ConversionExpr ce) { + var o = GetAnyConst(ce.E, constants); + if (o != null) { + return FoldConversion(o, ce.E.Type, ce.ToType); + } + + } else if (e is SeqSelectExpr sse) { + if (GetAnyConst(sse.Seq, constants) is string b && GetAnyConst(sse.E0, constants) is BigInteger index) { + if (0 <= index && index < b.Length && index <= int.MaxValue) { + return b[(int)index].ToString(); + } + } + + } else if (e is ITEExpr ite) { + if (GetAnyConst(ite.Test, constants) is bool b) { + return b ? GetAnyConst(ite.Thn, constants) : GetAnyConst(ite.Els, constants); + } + } + + return null; + } + + private static bool? FoldBoolean(BinaryExpr bin, bool e0, bool? e1) { + switch (bin.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.And: + if (e0) { + return e1; + } else { + return false; + } + case BinaryExpr.ResolvedOpcode.Or: + if (e0) { + return true; + } else { + return e1; + } + case BinaryExpr.ResolvedOpcode.Imp: + if (e0) { + return e1; + } else { + return true; + } + case BinaryExpr.ResolvedOpcode.Iff: + case BinaryExpr.ResolvedOpcode.EqCommon: + if (e1 != null) { + return e0 == (bool)e1; + } + break; + case BinaryExpr.ResolvedOpcode.NeqCommon: + if (e1 != null) { + return e0 != (bool)e1; + } + break; + } + return null; + } + + private static object FoldInteger(BinaryExpr bin, BigInteger e0, BigInteger e1) { + var isUnconstrained = IsUnconstrainedType(bin.Type); + + switch (bin.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Add: + if (isUnconstrained) { + return e0 + e1; + } + break; + case BinaryExpr.ResolvedOpcode.Sub: + if (isUnconstrained) { + return e0 - e1; + } + break; + case BinaryExpr.ResolvedOpcode.Mul: + if (isUnconstrained) { + return e0 * e1; + } + break; + case BinaryExpr.ResolvedOpcode.Div: + if (isUnconstrained && e1 != 0) { + // use Euclidean division + var d = e0 / e1; + if (0 <= e0 || e0 == d * e1) { + return d; + } else if (0 < e1) { + return d - 1; + } else { + return d + 1; + } + } + break; + case BinaryExpr.ResolvedOpcode.Mod: + if (isUnconstrained && e1 != 0) { + // use Euclidean modulo + var a = BigInteger.Abs(e1); + var d = e0 % a; + return 0 <= e0 ? d : d + a; + } + break; + case BinaryExpr.ResolvedOpcode.Gt: + return e0 > e1; + case BinaryExpr.ResolvedOpcode.Ge: + return e0 >= e1; + case BinaryExpr.ResolvedOpcode.Lt: + return e0 < e1; + case BinaryExpr.ResolvedOpcode.Le: + return e0 <= e1; + case BinaryExpr.ResolvedOpcode.EqCommon: + return e0 == e1; + case BinaryExpr.ResolvedOpcode.NeqCommon: + return e0 != e1; + } + return null; + } + + private static object FoldBitvector(BinaryExpr bin, BigInteger e0, BigInteger e1) { + Contract.Assert(0 <= e0); + + switch (bin.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Add: + // modular arithmetic + return (e0 + e1) & MaxBv(bin.Type); + case BinaryExpr.ResolvedOpcode.Sub: + // modular arithmetic + return (e0 - e1) & MaxBv(bin.Type); + case BinaryExpr.ResolvedOpcode.Mul: + // modular arithmetic + return (e0 * e1) & MaxBv(bin.Type); + case BinaryExpr.ResolvedOpcode.Div: + if (e1 != 0) { + return e0 / e1; + } + break; + case BinaryExpr.ResolvedOpcode.Mod: + if (e1 != 0) { + return e0 % e1; + } + break; + case BinaryExpr.ResolvedOpcode.BitwiseAnd: + return e0 & e1; + case BinaryExpr.ResolvedOpcode.BitwiseOr: + return e0 | e1; + case BinaryExpr.ResolvedOpcode.BitwiseXor: + return e0 ^ e1; + case BinaryExpr.ResolvedOpcode.LeftShift: + if (0 <= e1 && e1 <= bin.Type.AsBitVectorType.Width) { + return (e0 << (int)e1) & MaxBv(bin.E0.Type); + } + break; + case BinaryExpr.ResolvedOpcode.RightShift: + if (0 <= e1 && e1 <= bin.Type.AsBitVectorType.Width) { + return e0 >> (int)e1; + } + break; + case BinaryExpr.ResolvedOpcode.Gt: + return e0 > e1; + case BinaryExpr.ResolvedOpcode.Ge: + return e0 >= e1; + case BinaryExpr.ResolvedOpcode.Lt: + return e0 < e1; + case BinaryExpr.ResolvedOpcode.Le: + return e0 <= e1; + case BinaryExpr.ResolvedOpcode.EqCommon: + return e0 == e1; + case BinaryExpr.ResolvedOpcode.NeqCommon: + return e0 != e1; + } + return null; + } + + private static object FoldReal(BinaryExpr bin, BaseTypes.BigDec e0, BaseTypes.BigDec e1) { + var isUnconstrained = IsUnconstrainedType(bin.Type); + + switch (bin.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Add: + if (isUnconstrained) { + return e0 + e1; + } + break; + case BinaryExpr.ResolvedOpcode.Sub: + if (isUnconstrained) { + return e0 - e1; + } + break; + case BinaryExpr.ResolvedOpcode.Mul: + if (isUnconstrained) { + return e0 * e1; + } + break; + case BinaryExpr.ResolvedOpcode.Gt: + return e0 > e1; + case BinaryExpr.ResolvedOpcode.Ge: + return e0 >= e1; + case BinaryExpr.ResolvedOpcode.Lt: + return e0 < e1; + case BinaryExpr.ResolvedOpcode.Le: + return e0 <= e1; + case BinaryExpr.ResolvedOpcode.EqCommon: + return e0 == e1; + case BinaryExpr.ResolvedOpcode.NeqCommon: + return e0 != e1; + } + return null; + } + + private static object FoldCharOrString(BinaryExpr bin, string e0, string e1) { + if (bin.E0.Type.IsCharType) { + Contract.Assert(bin.E1.Type.IsCharType); + Contract.Assert(e0.Length == 1); + Contract.Assert(e1.Length == 1); + } + + switch (bin.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Concat: + return e0 + e1; + case BinaryExpr.ResolvedOpcode.GtChar: + Contract.Assert(bin.E0.Type.IsCharType); + return e0[0] > e1[0]; + case BinaryExpr.ResolvedOpcode.GeChar: + Contract.Assert(bin.E0.Type.IsCharType); + return e0[0] >= e1[0]; + case BinaryExpr.ResolvedOpcode.LtChar: + Contract.Assert(bin.E0.Type.IsCharType); + return e0[0] < e1[0]; + case BinaryExpr.ResolvedOpcode.LeChar: + Contract.Assert(bin.E0.Type.IsCharType); + return e0[0] <= e1[0]; + case BinaryExpr.ResolvedOpcode.ProperPrefix: + return e1.StartsWith(e0) && e0 != e1; ; + case BinaryExpr.ResolvedOpcode.Prefix: + return e1.StartsWith(e0); + case BinaryExpr.ResolvedOpcode.EqCommon: + Contract.Assert(bin.E0.Type.IsCharType); // the string case is handled in SeqEq + return e0[0] == e1[0]; + case BinaryExpr.ResolvedOpcode.NeqCommon: + Contract.Assert(bin.E0.Type.IsCharType); // the string case is handled in SeqEq + return e0[0] != e1[0]; + case BinaryExpr.ResolvedOpcode.SeqEq: + return e0 == e1; + case BinaryExpr.ResolvedOpcode.SeqNeq: + return e0 != e1; + } + return null; + } + + private static object FoldConversion(object value, Type fromType, Type toType) { + if (fromType == toType) { + return value; + } + if (!IsUnconstrainedType(toType)) { + return null; + } + + if (fromType.IsNumericBased(Type.NumericPersuasion.Real) && toType.IsBitVectorType) { + ((BaseTypes.BigDec)value).FloorCeiling(out var ff, out _); + if (ff < 0 || ff > MaxBv(toType)) { + return null; // Out of range + } + if (((BaseTypes.BigDec)value) != BaseTypes.BigDec.FromBigInt(ff)) { + return null; // Out of range + } + return ff; + } + + if (fromType.IsNumericBased(Type.NumericPersuasion.Real) && toType.IsNumericBased(Type.NumericPersuasion.Int)) { + ((BaseTypes.BigDec)value).FloorCeiling(out var ff, out _); + if (((BaseTypes.BigDec)value) != BaseTypes.BigDec.FromBigInt(ff)) { + return null; // Argument not an integer + } + return ff; + } + + if (fromType.IsBitVectorType && toType.IsNumericBased(Type.NumericPersuasion.Int)) { + return value; + } + + if (fromType.IsBitVectorType && toType.IsNumericBased(Type.NumericPersuasion.Real)) { + return BaseTypes.BigDec.FromBigInt((BigInteger)value); + } + + if (fromType.IsNumericBased(Type.NumericPersuasion.Int) && toType.IsBitVectorType) { + var b = (BigInteger)value; + if (b < 0 || b > MaxBv(toType)) { + return null; // Argument out of range + } + return value; + } + + if (fromType.IsNumericBased(Type.NumericPersuasion.Int) && toType.IsNumericBased(Type.NumericPersuasion.Int)) { + // This case includes int-based newtypes to int-based new types + return value; + } + + if (fromType.IsNumericBased(Type.NumericPersuasion.Real) && toType.IsNumericBased(Type.NumericPersuasion.Real)) { + // This case includes real-based newtypes to real-based new types + return value; + } + + if (fromType.IsBitVectorType && toType.IsBitVectorType) { + var b = (BigInteger)value; + if (b < 0 || b > MaxBv(toType)) { + return null; // Argument out of range + } + return value; + } + + if (fromType.IsNumericBased(Type.NumericPersuasion.Int) && toType.IsNumericBased(Type.NumericPersuasion.Real)) { + return BaseTypes.BigDec.FromBigInt((BigInteger)value); + } + + if (fromType.IsCharType && toType.IsNumericBased(Type.NumericPersuasion.Int)) { + var c = ((String)value)[0]; + return new BigInteger(((string)value)[0]); + } + + if (fromType.IsCharType && toType.IsBitVectorType) { + var c = ((String)value)[0]; + if ((int)c > MaxBv(toType)) { + return null; // Argument out of range + } + return new BigInteger(((string)value)[0]); + } + + if ((fromType.IsNumericBased(Type.NumericPersuasion.Int) || fromType.IsBitVectorType) && toType.IsCharType) { + var b = (BigInteger)value; + if (b < BigInteger.Zero || b > new BigInteger(65535)) { + return null; // Argument out of range + } + return ((char)(int)b).ToString(); + } + + if (fromType.IsCharType && toType.IsNumericBased(Type.NumericPersuasion.Real)) { + return BaseTypes.BigDec.FromInt(((string)value)[0]); + } + + if (fromType.IsNumericBased(Type.NumericPersuasion.Real) && toType.IsCharType) { + ((BaseTypes.BigDec)value).FloorCeiling(out var ff, out _); + if (((BaseTypes.BigDec)value) != BaseTypes.BigDec.FromBigInt(ff)) { + return null; // Argument not an integer + } + if (ff < BigInteger.Zero || ff > new BigInteger(65535)) { + return null; // Argument out of range + } + return ((char)(int)ff).ToString(); + } + + return null; + } + } +} diff --git a/Source/DafnyCore/Resolver/ExpressionTester.cs b/Source/DafnyCore/Resolver/ExpressionTester.cs index 603d5bd9fe..fa43076d63 100644 --- a/Source/DafnyCore/Resolver/ExpressionTester.cs +++ b/Source/DafnyCore/Resolver/ExpressionTester.cs @@ -357,7 +357,7 @@ public static bool IsTypeTestCompilable(TypeTestExpr tte) { // TODO: It would be nice to allow some subset types in test tests in compiled code. But for now, such cases // are allowed only in ghost contexts. var udtTo = (UserDefinedType)tte.ToType.NormalizeExpandKeepConstraints(); - if (udtTo.ResolvedClass is SubsetTypeDecl && !(udtTo.ResolvedClass is NonNullTypeDecl)) { + if (udtTo.ResolvedClass is SubsetTypeDecl and not NonNullTypeDecl) { return false; } @@ -368,7 +368,7 @@ public static bool IsTypeTestCompilable(TypeTestExpr tte) { // In other words, we CAN perform the type test at run time if the type parameters of A uniquely determine the type parameters of B. // Let T be a list of type parameters (in particular, we will use the formal TypeParameter's declared in type B). Then, represent // B in parent type A, and let's say the result is A for some type expression U. If U contains all type parameters from T, - // then the mapping from B to A is unique, which means the mapping frmo B to A is unique, which means we can check if an + // then the mapping from B to A is unique, which means the mapping from B to A is unique, which means we can check if an // A value is a B value by checking if the value is of type B<...>. var B = ((UserDefinedType)tte.ToType.NormalizeExpandKeepConstraints()).ResolvedClass; // important to keep constraints here, so no type parameters are lost var B_T = UserDefinedType.FromTopLevelDecl(tte.tok, B); diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 6e78491a43..b697df8ac0 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1166,6 +1166,25 @@ public void ResolveTopLevelDecls_Core(List declarations, // Compute ghost interests, figure out native types, check agreement among datatype destructors, and determine tail calls. if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { foreach (TopLevelDecl d in declarations) { + void CheckIfCompilable(RedirectingTypeDecl declWithConstraint) { + var constraintIsCompilable = true; + + // Check base type + var baseType = (declWithConstraint.Var?.Type ?? ((NewtypeDecl)declWithConstraint).BaseType).NormalizeExpandKeepConstraints(); + if (baseType.AsRedirectingType is (SubsetTypeDecl or NewtypeDecl) and var baseDecl) { + CheckIfCompilable(baseDecl); + constraintIsCompilable &= baseDecl.ConstraintIsCompilable; + } + + // Check the type's constraint + if (declWithConstraint.Constraint != null) { + constraintIsCompilable &= ExpressionTester.CheckIsCompilable(Options, null, declWithConstraint.Constraint, + new CodeContextWrapper(declWithConstraint, true)); + } + + declWithConstraint.ConstraintIsCompilable = constraintIsCompilable; + } + if (d is IteratorDecl) { var iter = (IteratorDecl)d; iter.SubExpressions.ForEach(e => CheckExpression(e, this, iter)); @@ -1177,9 +1196,7 @@ public void ResolveTopLevelDecls_Core(List declarations, } else if (d is SubsetTypeDecl subsetTypeDecl) { Contract.Assert(subsetTypeDecl.Constraint != null); CheckExpression(subsetTypeDecl.Constraint, this, new CodeContextWrapper(subsetTypeDecl, true)); - subsetTypeDecl.ConstraintIsCompilable = - ExpressionTester.CheckIsCompilable(Options, null, subsetTypeDecl.Constraint, new CodeContextWrapper(subsetTypeDecl, true)); - subsetTypeDecl.CheckedIfConstraintIsCompilable = true; + CheckIfCompilable(subsetTypeDecl); if (subsetTypeDecl.Witness != null) { CheckExpression(subsetTypeDecl.Witness, this, new CodeContextWrapper(subsetTypeDecl, subsetTypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost)); @@ -1193,13 +1210,15 @@ public void ResolveTopLevelDecls_Core(List declarations, if (newtypeDecl.Var != null) { Contract.Assert(newtypeDecl.Constraint != null); CheckExpression(newtypeDecl.Constraint, this, new CodeContextWrapper(newtypeDecl, true)); - if (newtypeDecl.Witness != null) { - CheckExpression(newtypeDecl.Witness, this, new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost)); - } } - if (newtypeDecl.Witness != null && newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Compiled) { - var codeContext = new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost); - ExpressionTester.CheckIsCompilable(Options, this, newtypeDecl.Witness, codeContext); + CheckIfCompilable(newtypeDecl); + + if (newtypeDecl.Witness != null) { + CheckExpression(newtypeDecl.Witness, this, new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost)); + if (newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Compiled) { + var codeContext = new CodeContextWrapper(newtypeDecl, newtypeDecl.WitnessKind == SubsetTypeDecl.WKind.Ghost); + ExpressionTester.CheckIsCompilable(Options, this, newtypeDecl.Witness, codeContext); + } } FigureOutNativeType(newtypeDecl); @@ -1628,8 +1647,11 @@ public void ResolveTopLevelDecls_Core(List declarations, } } } - // Verifies that, in all compiled places, subset types in comprehensions have a compilable constraint - new SubsetConstraintGhostChecker(this.Reporter).Traverse(declarations); + + if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { + // Verifies that, in all compiled places, subset types in comprehensions have a compilable constraint + new SubsetConstraintGhostChecker(this.Reporter).Traverse(declarations); + } } /// @@ -2048,23 +2070,6 @@ public static void ReportCycleError(ErrorReporter reporter, List cycle, Fu reporter.Error(MessageSource.Resolver, toTok(start), $"{msg}: {cy} -> {toString(start)}"); } - /// - /// Returns the largest value that can be stored in bitvector type "t". - /// - public static BigInteger MaxBV(Type t) { - Contract.Requires(t != null); - Contract.Requires(t.IsBitVectorType); - return MaxBV(t.AsBitVectorType.Width); - } - - /// - /// Returns the largest value that can be stored in bitvector type of "bits" width. - /// - public static BigInteger MaxBV(int bits) { - Contract.Requires(0 <= bits); - return BigInteger.Pow(new BigInteger(2), bits) - BigInteger.One; - } - private void FigureOutNativeType(NewtypeDecl dd) { Contract.Requires(dd != null); @@ -2124,574 +2129,52 @@ private void FigureOutNativeType(NewtypeDecl dd) { ddConstraint = ddWhereConstraintsAre.Constraint; } List bounds; + bool constraintConsistsSolelyOfRangeConstraints; if (ddVar == null) { // There are no bounds at all bounds = new List(); + constraintConsistsSolelyOfRangeConstraints = true; } else { - bounds = DiscoverAllBounds_SingleVar(ddVar, ddConstraint); - } - - // Returns null if the argument is a constrained newtype (recursively) - // Returns the transitive base type if the argument is recusively unconstrained - Type AsUnconstrainedType(Type t) { - while (true) { - if (t.AsNewtype == null) { - return t; - } - - if (t.AsNewtype.Constraint != null) { - return null; - } - - t = t.AsNewtype.BaseType; - } + bounds = DiscoverAllBounds_SingleVar(ddVar, ddConstraint, out constraintConsistsSolelyOfRangeConstraints); } // Find which among the allowable native types can hold "dd". Give an // error for any user-specified native type that's not big enough. var bigEnoughNativeTypes = new List(); - // But first, define a local, recursive function GetConst/GetAnyConst: - // These fold any constant computations, including symbolic constants, - // returning null if folding is not possible. If an operation is undefined - // (divide by zero, conversion out of range, etc.), then null is returned. - Func GetConst = null; - Func, Object> GetAnyConst = null; - GetAnyConst = (Expression e, Stack consts) => { - if (e is LiteralExpr l) { - return l.Value; - } else if (e is UnaryOpExpr un) { - if (un.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot && GetAnyConst(un.E, consts) is bool b) { - return !b; - } - if (un.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BVNot && GetAnyConst(un.E, consts) is BigInteger i) { - return ((BigInteger.One << un.Type.AsBitVectorType.Width) - 1) ^ i; - } - // TODO: This only handles strings; generalize to other collections? - if (un.ResolvedOp == UnaryOpExpr.ResolvedOpcode.SeqLength && GetAnyConst(un.E, consts) is string ss) { - return (BigInteger)(ss.Length); - } - } else if (e is MemberSelectExpr m) { - if (m.Member is ConstantField c && c.IsStatic && c.Rhs != null) { - // This aspect of type resolution happens before the check for cyclic references - // so we have to do a check here as well. If cyclic, null is silently returned, - // counting on the later error message to alert the user. - if (consts.Contains(c)) { return null; } - consts.Push(c); - Object o = GetAnyConst(c.Rhs, consts); - consts.Pop(); - return o; - } else if (m.Member is SpecialField sf) { - string nm = sf.Name; - if (nm == "Floor") { - Object ee = GetAnyConst(m.Obj, consts); - if (ee != null && m.Obj.Type.IsNumericBased(Type.NumericPersuasion.Real)) { - ((BaseTypes.BigDec)ee).FloorCeiling(out var f, out _); - return f; - } - } - } - } else if (e is BinaryExpr bin) { - Object e0 = GetAnyConst(bin.E0, consts); - Object e1 = GetAnyConst(bin.E1, consts); - bool isBool = bin.E0.Type == Type.Bool && bin.E1.Type == Type.Bool; - bool shortCircuit = isBool && (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And - || bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or - || bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp); - - if (e0 == null || (!shortCircuit && e1 == null)) { return null; } - bool isAnyReal = bin.E0.Type.IsNumericBased(Type.NumericPersuasion.Real) - && bin.E1.Type.IsNumericBased(Type.NumericPersuasion.Real); - bool isAnyInt = bin.E0.Type.IsNumericBased(Type.NumericPersuasion.Int) - && bin.E1.Type.IsNumericBased(Type.NumericPersuasion.Int); - bool isReal = bin.Type.IsRealType; - bool isInt = bin.Type.IsIntegerType; - bool isBV = bin.E0.Type.IsBitVectorType; - int width = isBV ? bin.E0.Type.AsBitVectorType.Width : 0; - bool isString = e0 is string && e1 is string; - switch (bin.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.Add: - if (isInt) { - return (BigInteger)e0 + (BigInteger)e1; - } - - if (isBV) { - return ((BigInteger)e0 + (BigInteger)e1) & MaxBV(bin.Type); - } - - if (isReal) { - return (BaseTypes.BigDec)e0 + (BaseTypes.BigDec)e1; - } - - break; - case BinaryExpr.ResolvedOpcode.Concat: - if (isString) { - return (string)e0 + (string)e1; - } - - break; - case BinaryExpr.ResolvedOpcode.Sub: - if (isInt) { - return (BigInteger)e0 - (BigInteger)e1; - } - - if (isBV) { - return ((BigInteger)e0 - (BigInteger)e1) & MaxBV(bin.Type); - } - - if (isReal) { - return (BaseTypes.BigDec)e0 - (BaseTypes.BigDec)e1; - } - // Allow a special case: If the result type is a newtype that is integer-based (i.e., isInt && !isInteger) - // then we generally do not fold the operations, because we do not determine whether the - // result of the operation satisfies the new type constraint. However, on the occasion that - // a newtype aliases int without a constraint, it occurs that a value of the newtype is initialized - // with a negative value, which is represented as "0 - N", that is, it comes to this case. It - // is a nuisance not to constant-fold the result, as not doing so can alter the determination - // of the representation type. - if (isAnyInt && AsUnconstrainedType(bin.Type) != null) { - return ((BigInteger)e0) - ((BigInteger)e1); - } - break; - case BinaryExpr.ResolvedOpcode.Mul: - if (isInt) { - return (BigInteger)e0 * (BigInteger)e1; - } - - if (isBV) { - return ((BigInteger)e0 * (BigInteger)e1) & MaxBV(bin.Type); - } - - if (isReal) { - return (BaseTypes.BigDec)e0 * (BaseTypes.BigDec)e1; - } - - break; - case BinaryExpr.ResolvedOpcode.BitwiseAnd: - Contract.Assert(isBV); - return (BigInteger)e0 & (BigInteger)e1; - case BinaryExpr.ResolvedOpcode.BitwiseOr: - Contract.Assert(isBV); - return (BigInteger)e0 | (BigInteger)e1; - case BinaryExpr.ResolvedOpcode.BitwiseXor: - Contract.Assert(isBV); - return (BigInteger)e0 ^ (BigInteger)e1; - case BinaryExpr.ResolvedOpcode.Div: - if (isInt) { - if ((BigInteger)e1 == 0) { - return null; // Divide by zero - } else { - BigInteger a0 = (BigInteger)e0; - BigInteger a1 = (BigInteger)e1; - BigInteger d = a0 / a1; - return a0 >= 0 || a0 == d * a1 ? d : a1 > 0 ? d - 1 : d + 1; - } - } - if (isBV) { - if ((BigInteger)e1 == 0) { - return null; // Divide by zero - } else { - return ((BigInteger)e0) / ((BigInteger)e1); - } - } - if (isReal) { - if ((BaseTypes.BigDec)e1 == BaseTypes.BigDec.ZERO) { - return null; // Divide by zero - } else { - // BigDec does not have divide and is not a representation of rationals, so we don't do constant folding - return null; - } - } - - break; - case BinaryExpr.ResolvedOpcode.Mod: - if (isInt) { - if ((BigInteger)e1 == 0) { - return null; // Mod by zero - } else { - BigInteger a = BigInteger.Abs((BigInteger)e1); - BigInteger d = (BigInteger)e0 % a; - return (BigInteger)e0 >= 0 ? d : d + a; - } - } - if (isBV) { - if ((BigInteger)e1 == 0) { - return null; // Mod by zero - } else { - return (BigInteger)e0 % (BigInteger)e1; - } - } - break; - case BinaryExpr.ResolvedOpcode.LeftShift: { - if ((BigInteger)e1 < 0) { - return null; // Negative shift - } - if ((BigInteger)e1 > bin.Type.AsBitVectorType.Width) { - return null; // Shift is too large - } - return ((BigInteger)e0 << (int)(BigInteger)e1) & MaxBV(bin.E0.Type); - } - case BinaryExpr.ResolvedOpcode.RightShift: { - if ((BigInteger)e1 < 0) { - return null; // Negative shift - } - if ((BigInteger)e1 > bin.Type.AsBitVectorType.Width) { - return null; // Shift too large - } - return (BigInteger)e0 >> (int)(BigInteger)e1; - } - case BinaryExpr.ResolvedOpcode.And: { - if ((bool)e0 && e1 == null) { - return null; - } - - return (bool)e0 && (bool)e1; - } - case BinaryExpr.ResolvedOpcode.Or: { - if (!(bool)e0 && e1 == null) { - return null; - } - - return (bool)e0 || (bool)e1; - } - case BinaryExpr.ResolvedOpcode.Imp: { // ==> and <== - if ((bool)e0 && e1 == null) { - return null; - } - - return !(bool)e0 || (bool)e1; - } - case BinaryExpr.ResolvedOpcode.Iff: return (bool)e0 == (bool)e1; // <==> - case BinaryExpr.ResolvedOpcode.Gt: - if (isAnyInt) { - return (BigInteger)e0 > (BigInteger)e1; - } - - if (isBV) { - return (BigInteger)e0 > (BigInteger)e1; - } - - if (isAnyReal) { - return (BaseTypes.BigDec)e0 > (BaseTypes.BigDec)e1; - } - - break; - case BinaryExpr.ResolvedOpcode.GtChar: - if (bin.E0.Type.IsCharType) { - return ((string)e0)[0] > ((string)e1)[0]; - } - - break; - case BinaryExpr.ResolvedOpcode.Ge: - if (isAnyInt) { - return (BigInteger)e0 >= (BigInteger)e1; - } - - if (isBV) { - return (BigInteger)e0 >= (BigInteger)e1; - } - - if (isAnyReal) { - return (BaseTypes.BigDec)e0 >= (BaseTypes.BigDec)e1; - } - - break; - case BinaryExpr.ResolvedOpcode.GeChar: - if (bin.E0.Type.IsCharType) { - return ((string)e0)[0] >= ((string)e1)[0]; - } - - break; - case BinaryExpr.ResolvedOpcode.Lt: - if (isAnyInt) { - return (BigInteger)e0 < (BigInteger)e1; - } - - if (isBV) { - return (BigInteger)e0 < (BigInteger)e1; - } - - if (isAnyReal) { - return (BaseTypes.BigDec)e0 < (BaseTypes.BigDec)e1; - } - - break; - case BinaryExpr.ResolvedOpcode.LtChar: - if (bin.E0.Type.IsCharType) { - return ((string)e0)[0] < ((string)e1)[0]; - } - - break; - case BinaryExpr.ResolvedOpcode.ProperPrefix: - if (isString) { - return ((string)e1).StartsWith((string)e0) && !((string)e1).Equals((string)e0); - } - - break; - case BinaryExpr.ResolvedOpcode.Le: - if (isAnyInt) { - return (BigInteger)e0 <= (BigInteger)e1; - } - - if (isBV) { - return (BigInteger)e0 <= (BigInteger)e1; - } - - if (isAnyReal) { - return (BaseTypes.BigDec)e0 <= (BaseTypes.BigDec)e1; - } - - break; - case BinaryExpr.ResolvedOpcode.LeChar: - if (bin.E0.Type.IsCharType) { - return ((string)e0)[0] <= ((string)e1)[0]; - } - - break; - case BinaryExpr.ResolvedOpcode.Prefix: - if (isString) { - return ((string)e1).StartsWith((string)e0); - } - - break; - case BinaryExpr.ResolvedOpcode.EqCommon: { - if (isBool) { - return (bool)e0 == (bool)e1; - } else if (isAnyInt || isBV) { - return (BigInteger)e0 == (BigInteger)e1; - } else if (isAnyReal) { - return (BaseTypes.BigDec)e0 == (BaseTypes.BigDec)e1; - } else if (bin.E0.Type.IsCharType) { - return ((string)e0)[0] == ((string)e1)[0]; - } - break; - } - case BinaryExpr.ResolvedOpcode.SeqEq: - if (isString) { - return (string)e0 == (string)e1; - } - break; - case BinaryExpr.ResolvedOpcode.SeqNeq: - if (isString) { - return (string)e0 != (string)e1; - } - break; - case BinaryExpr.ResolvedOpcode.NeqCommon: { - if (isBool) { - return (bool)e0 != (bool)e1; - } else if (isAnyInt || isBV) { - return (BigInteger)e0 != (BigInteger)e1; - } else if (isAnyReal) { - return (BaseTypes.BigDec)e0 != (BaseTypes.BigDec)e1; - } else if (bin.E0.Type.IsCharType) { - return ((string)e0)[0] != ((string)e1)[0]; - } else if (isString) { - return (string)e0 != (string)e1; - } - break; - } - } - } else if (e is ConversionExpr ce) { - object o = GetAnyConst(ce.E, consts); - if (o == null || ce.E.Type == ce.Type) { - return o; - } - - if (ce.E.Type.IsNumericBased(Type.NumericPersuasion.Real) && - ce.Type.IsBitVectorType) { - ((BaseTypes.BigDec)o).FloorCeiling(out var ff, out _); - if (ff < 0 || ff > MaxBV(ce.Type)) { - return null; // Out of range - } - if (((BaseTypes.BigDec)o) != BaseTypes.BigDec.FromBigInt(ff)) { - return null; // Out of range - } - return ff; - } - - if (ce.E.Type.IsNumericBased(Type.NumericPersuasion.Real) && - ce.Type.IsNumericBased(Type.NumericPersuasion.Int)) { - ((BaseTypes.BigDec)o).FloorCeiling(out var ff, out _); - if (AsUnconstrainedType(ce.Type) == null) { - return null; - } - - if (((BaseTypes.BigDec)o) != BaseTypes.BigDec.FromBigInt(ff)) { - return null; // Argument not an integer - } - return ff; - } - - if (ce.E.Type.IsBitVectorType && - ce.Type.IsNumericBased(Type.NumericPersuasion.Int)) { - if (AsUnconstrainedType(ce.Type) == null) { - return null; - } - - return o; - } - - if (ce.E.Type.IsBitVectorType && - ce.Type.IsNumericBased(Type.NumericPersuasion.Real)) { - if (AsUnconstrainedType(ce.Type) == null) { - return null; - } - - return BaseTypes.BigDec.FromBigInt((BigInteger)o); - } - - if (ce.E.Type.IsNumericBased(Type.NumericPersuasion.Int) && - ce.Type.IsBitVectorType) { - BigInteger b = (BigInteger)o; - if (b < 0 || b > MaxBV(ce.Type)) { - return null; // Argument out of range - } - return o; - } - - if (ce.E.Type.IsNumericBased(Type.NumericPersuasion.Int) && - ce.Type.IsNumericBased(Type.NumericPersuasion.Int)) { - // This case includes int-based newtypes to int-based new types - if (AsUnconstrainedType(ce.Type) == null) { - return null; - } - - return o; - } - - if (ce.E.Type.IsNumericBased(Type.NumericPersuasion.Real) && - ce.Type.IsNumericBased(Type.NumericPersuasion.Real)) { - // This case includes real-based newtypes to real-based new types - if (AsUnconstrainedType(ce.Type) == null) { - return null; - } - - return o; - } - - if (ce.E.Type.IsBitVectorType && ce.Type.IsBitVectorType) { - BigInteger b = (BigInteger)o; - if (b < 0 || b > MaxBV(ce.Type)) { - return null; // Argument out of range - } - return o; - } - - if (ce.E.Type.IsNumericBased(Type.NumericPersuasion.Int) && - ce.Type.IsNumericBased(Type.NumericPersuasion.Real)) { - if (AsUnconstrainedType(ce.Type) == null) { - return null; - } - - return BaseTypes.BigDec.FromBigInt((BigInteger)o); - } - - if (ce.E.Type.IsCharType && ce.Type.IsNumericBased(Type.NumericPersuasion.Int)) { - char c = ((String)o)[0]; - if (AsUnconstrainedType(ce.Type) == null) { - return null; - } - - return new BigInteger(((string)o)[0]); - } - - if (ce.E.Type.IsCharType && ce.Type.IsBitVectorType) { - char c = ((String)o)[0]; - if ((int)c > MaxBV(ce.Type)) { - return null; // Argument out of range - } - return new BigInteger(((string)o)[0]); - } - - if ((ce.E.Type.IsNumericBased(Type.NumericPersuasion.Int) || ce.E.Type.IsBitVectorType) && - ce.Type.IsCharType) { - BigInteger b = (BigInteger)o; - if (b < BigInteger.Zero || b > new BigInteger(65535)) { - return null; // Argument out of range - } - return ((char)(int)b).ToString(); - } - - if (ce.E.Type.IsCharType && - ce.Type.IsNumericBased(Type.NumericPersuasion.Real)) { - if (AsUnconstrainedType(ce.Type) == null) { - return null; - } - - return BaseTypes.BigDec.FromInt(((string)o)[0]); - } - - if (ce.E.Type.IsNumericBased(Type.NumericPersuasion.Real) && - ce.Type.IsCharType) { - ((BaseTypes.BigDec)o).FloorCeiling(out var ff, out _); - if (((BaseTypes.BigDec)o) != BaseTypes.BigDec.FromBigInt(ff)) { - return null; // Argument not an integer - } - if (ff < BigInteger.Zero || ff > new BigInteger(65535)) { - return null; // Argument out of range - } - return ((char)(int)ff).ToString(); - } - - } else if (e is SeqSelectExpr sse) { - var b = GetAnyConst(sse.Seq, consts) as string; - BigInteger index = (BigInteger)GetAnyConst(sse.E0, consts); - if (b == null) { - return null; - } - - if (index < 0 || index >= b.Length || index > Int32.MaxValue) { - return null; // Index out of range + BigInteger? lowBound = null; + BigInteger? highBound = null; + foreach (var bound in bounds) { + void UpdateBounds(BigInteger? lo, BigInteger? hi) { + if (lo != null && (lowBound == null || lowBound < lo)) { + lowBound = lo; // we found a more restrictive lower bound } - return b[(int)index].ToString(); - } else if (e is ITEExpr ite) { - Object b = GetAnyConst(ite.Test, consts); - if (b == null) { - return null; + if (hi != null && (highBound == null || hi < highBound)) { + highBound = hi; // we found a more restrictive lower bound } + } - return ((bool)b) ? GetAnyConst(ite.Thn, consts) : GetAnyConst(ite.Els, consts); - } else if (e is ConcreteSyntaxExpression n) { - return GetAnyConst(n.ResolvedExpression, consts); - } else { - return null; - } - return null; - }; - GetConst = (Expression e) => { - Object ee = GetAnyConst(e.Resolved ?? e, new Stack()); - return ee as BigInteger?; - }; - // Now, then, let's go through them types. - // FIXME - should first go through the bounds to find the most constraining values - // then check those values against the possible types. Note that also presumes the types are in order. - BigInteger? lowest = null; - BigInteger? highest = null; - foreach (var bound in bounds) { - if (bound is ComprehensionExpr.IntBoundedPool) { - var bnd = (ComprehensionExpr.IntBoundedPool)bound; - if (bnd.LowerBound != null) { - BigInteger? lower = GetConst(bnd.LowerBound); - if (lower != null && (lowest == null || lower < lowest)) { - lowest = lower; - } + if (bound is ComprehensionExpr.IntBoundedPool range) { + if (range.LowerBound != null && ConstantFolder.TryFoldInteger(range.LowerBound) is not null and var lo) { + UpdateBounds(lo, null); } - if (bnd.UpperBound != null) { - BigInteger? upper = GetConst(bnd.UpperBound); - if (upper != null && (highest == null || upper > highest)) { - highest = upper; - } + if (range.UpperBound != null && ConstantFolder.TryFoldInteger(range.UpperBound) is not null and var hi) { + UpdateBounds(null, hi); } + } else if (bound is ComprehensionExpr.ExactBoundedPool exact && ConstantFolder.TryFoldInteger(exact.E) is not null and var value) { + UpdateBounds(value, value + 1); } } + + var emptyRange = lowBound != null && highBound != null && highBound <= lowBound; foreach (var nativeT in nativeTypeChoices ?? NativeTypes) { - bool lowerOk = (lowest != null && nativeT.LowerBound <= lowest); - bool upperOk = (highest != null && nativeT.UpperBound >= highest); + bool lowerOk = emptyRange || (lowBound != null && nativeT.LowerBound <= lowBound); + bool upperOk = emptyRange || (highBound != null && nativeT.UpperBound >= highBound); if (lowerOk && upperOk) { bigEnoughNativeTypes.Add(nativeT); } else if (nativeTypeChoices != null) { reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics failed to confirm '{0}' to be a compatible native type. " + - "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'", + "Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'", nativeT.Name); return; } @@ -2702,6 +2185,13 @@ Type AsUnconstrainedType(Type t) { foreach (var nativeT in bigEnoughNativeTypes) { if (Options.Backend.SupportedNativeTypes.Contains(nativeT.Name)) { dd.NativeType = nativeT; + if (constraintConsistsSolelyOfRangeConstraints) { + dd.NativeTypeRangeImpliesAllConstraints = true; + } + if (constraintConsistsSolelyOfRangeConstraints && nativeT.Sel != NativeType.Selection.Number && + lowBound == nativeT.LowerBound && highBound == nativeT.UpperBound) { + dd.TargetTypeCoversAllBitPatterns = true; + } break; } } @@ -2710,8 +2200,15 @@ Type AsUnconstrainedType(Type t) { // one particular native type, in which case that must have been the one picked. if (nativeTypeChoices != null && nativeTypeChoices.Count == 1) { Contract.Assert(dd.NativeType == nativeTypeChoices[0]); + if (dd.TargetTypeCoversAllBitPatterns) { + reporter.Info(MessageSource.Resolver, dd.tok, + $"newtype {dd.Name} is target-complete for {{:nativeType \"{dd.NativeType.Name}\"}}"); + } } else { - reporter.Info(MessageSource.Resolver, dd.tok, "newtype " + dd.Name + " resolves as {:nativeType \"" + dd.NativeType.Name + "\"} (Detected Range: " + lowest + " .. " + highest + ")"); + var detectedRange = emptyRange ? "empty" : $"{lowBound} .. {highBound}"; + var targetComplete = dd.TargetTypeCoversAllBitPatterns ? "target-complete " : ""; + reporter.Info(MessageSource.Resolver, dd.tok, + $"newtype {dd.Name} resolves as {{:nativeType \"{dd.NativeType.Name}\"}} (detected range: {detectedRange})"); } } else if (nativeTypeChoices != null) { reporter.Error(MessageSource.Resolver, dd, @@ -2719,7 +2216,7 @@ Type AsUnconstrainedType(Type t) { } else if (mustUseNativeType) { reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type. " + - "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'"); + "Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)'"); } } diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs index 054e0e3dbe..e9333ead4f 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs @@ -116,7 +116,7 @@ protected override void PostVisitOneExpression(Expression expr, TypeInferenceChe var n = (BigInteger)e.Value; var absN = n < 0 ? -n : n; // For bitvectors, check that the magnitude fits the width - if (e.Type.IsBitVectorType && ModuleResolver.MaxBV(e.Type.AsBitVectorType.Width) < absN) { + if (e.Type.IsBitVectorType && ConstantFolder.MaxBv(e.Type.AsBitVectorType.Width) < absN) { resolver.ReportError(ResolutionErrors.ErrorId.r_literal_too_large_for_bitvector, e.tok, "literal ({0}) is too large for the bitvector type {1}", absN, e.Type); } // For bitvectors and ORDINALs, check for a unary minus that, earlier, was mistaken for a negative literal diff --git a/Source/DafnyCore/Resolver/PreType/PreType.cs b/Source/DafnyCore/Resolver/PreType/PreType.cs index 8f161298c7..8eaf472be8 100644 --- a/Source/DafnyCore/Resolver/PreType/PreType.cs +++ b/Source/DafnyCore/Resolver/PreType/PreType.cs @@ -137,7 +137,7 @@ public static Dictionary PreTypeSubstMap(List.PushResult ScopePushAndReport(Scope scope, st return r; } -#if THIS_COMES_LATER - public void PostResolveChecks(List declarations) { - Contract.Requires(declarations != null); - foreach (TopLevelDecl topd in declarations) { - TopLevelDecl d = topd is ClassLikeDecl ? ((ClassLikeDecl)topd).NonNullTypeDecl : topd; - - if (ErrorCount == prevErrorCount) { - // Check type inference, which also discovers bounds, in newtype/subset-type constraints and const declarations - foreach (TopLevelDecl topd in declarations) { - TopLevelDecl d = topd is ClassLikeDecl ? ((ClassLikeDecl)topd).NonNullTypeDecl : topd; - if (topd is TopLevelDeclWithMembers cl) { - foreach (var member in cl.Members) { - if (member is ConstantField field && field.Rhs != null) { - // make sure initialization only refers to constant field or literal expression - if (CheckIsConstantExpr(field, field.Rhs)) { - AddAssignableConstraint(field.tok, field.Type, field.Rhs.Type, - "type for constant '" + field.Name + "' is '{0}', but its initialization value type is '{1}'"); - } - - } - } - } - } - } - - } - } -#endif - void AddSubtypeConstraint(PreType super, PreType sub, IToken tok, string errorFormatString) { Constraints.AddSubtypeConstraint(super, sub, tok, errorFormatString); } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeSubtypeConstraint.cs b/Source/DafnyCore/Resolver/PreType/PreTypeSubtypeConstraint.cs index 595af29135..05b01cb721 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeSubtypeConstraint.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeSubtypeConstraint.cs @@ -79,7 +79,7 @@ public bool Apply(PreTypeConstraints constraints) { if (ptSuper.Decl is not TraitDecl) { var arguments = CreateProxiesForTypesAccordingToVariance(tok, ptSuper.Decl.TypeArgs, ptSuper.Arguments, false, constraints); var pt = new DPreType(ptSuper.Decl, arguments); - constraints.AddEqualityConstraint(sub, pt, tok, ErrorFormatString); + constraints.AddEqualityConstraint(pt, sub, tok, ErrorFormatString); return true; } } else if (ptSub != null) { diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs b/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs index 474ae83373..855a427baa 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeToType.cs @@ -174,7 +174,7 @@ protected override void PostVisitOneExpression(Expression expr, IASTVisitorConte } // Case: fixed pre-type type - if (expr is LiteralExpr or ThisExpr or UnaryExpr or BinaryExpr) { + if (expr is LiteralExpr or ThisExpr or UnaryExpr or BinaryExpr or NegationExpression) { // Note, for the LiteralExpr "null", we expect to get a possibly-null type, whereas for a reference-type ThisExpr, we expect // to get the non-null type. The .PreType of these two distinguish between those cases, because the latter has a .PrintablePreType // field that gives the non-null type. diff --git a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs index f65473cb43..dfbd66676c 100644 --- a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs +++ b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs @@ -285,7 +285,7 @@ protected override void VisitOneExpr(Expression expr) { var n = (BigInteger)e.Value; var absN = n < 0 ? -n : n; // For bitvectors, check that the magnitude fits the width - if (PreTypeResolver.IsBitvectorName(familyDeclName, out var width) && ModuleResolver.MaxBV(width) < absN) { + if (PreTypeResolver.IsBitvectorName(familyDeclName, out var width) && ConstantFolder.MaxBv(width) < absN) { cus.ReportError(e.tok, "literal ({0}) is too large for the bitvector type {1}", absN, e.PreType); } // For bitvectors and ORDINALs, check for a unary minus that, earlier, was mistaken for a negative literal @@ -357,14 +357,6 @@ protected override void VisitOneExpr(Expression expr) { // by specializing for IdentifierExpr, error messages will be clearer CheckPreTypeIsDetermined(expr.tok, expr.PreType, "variable"); - } else if (expr is ConversionExpr) { - var e = (ConversionExpr)expr; - CheckPreTypeIsDetermined(e.tok, e.PreType, "cast target"); - - } else if (expr is TypeTestExpr) { - var e = (TypeTestExpr)expr; - CheckPreTypeIsDetermined(e.tok, e.PreType, "type test target"); - } else if (CheckPreTypeIsDetermined(expr.tok, expr.PreType, "expression")) { if (expr is UnaryOpExpr uop) { var resolvedOp = (uop.Op, PreTypeResolver.AncestorName(uop.E.PreType)) switch { diff --git a/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs b/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs index 488d2fdab0..f7b3db3939 100644 --- a/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs +++ b/Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs @@ -81,28 +81,16 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN return base.Traverse(expr, field, parent); } - string what = e.WhatKind; - - if (e is ForallExpr || e is ExistsExpr || e is SetComprehension || e is MapComprehension) { + if (e is QuantifierExpr or SetComprehension or MapComprehension) { foreach (var boundVar in e.BoundVars) { - if (boundVar.Type.AsSubsetType is { - Constraint: var constraint, - ConstraintIsCompilable: false and var constraintIsCompilable - } and var subsetTypeDecl - ) { - if (!subsetTypeDecl.CheckedIfConstraintIsCompilable) { - // Builtin types were never resolved. - constraintIsCompilable = - ExpressionTester.CheckIsCompilable(reporter.Options, null, constraint, new CodeContextWrapper(subsetTypeDecl, true)); - subsetTypeDecl.CheckedIfConstraintIsCompilable = true; - subsetTypeDecl.ConstraintIsCompilable = constraintIsCompilable; - } + if (boundVar.Type.NormalizeExpandKeepConstraints().AsRedirectingType is (SubsetTypeDecl or NewtypeDecl) and var declWithConstraint) { + if (!declWithConstraint.ConstraintIsCompilable) { - if (!constraintIsCompilable) { IToken finalToken = boundVar.tok; - if (constraint.tok.line != 0) { + if (declWithConstraint.Constraint != null && declWithConstraint.Constraint.tok.line != 0) { var errorCollector = new FirstErrorCollector(reporter.Options); - ExpressionTester.CheckIsCompilable(null, errorCollector, constraint, new CodeContextWrapper(subsetTypeDecl, true)); + ExpressionTester.CheckIsCompilable(null, errorCollector, declWithConstraint.Constraint, + new CodeContextWrapper(declWithConstraint, true)); if (errorCollector.Collected) { finalToken = new NestedToken(finalToken, errorCollector.FirstCollectedToken, "The constraint is not compilable because " + errorCollector.FirstCollectedMessage @@ -110,7 +98,8 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN } } this.reporter.Error(MessageSource.Resolver, finalToken, - $"{boundVar.Type} is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in {what}."); + $"{boundVar.Type} is a {declWithConstraint.WhatKind} and its constraint is not compilable, " + + $"hence it cannot yet be used as the type of a bound variable in {e.WhatKind}."); } } } diff --git a/Source/DafnyCore/Rewriters/ExpectContracts.cs b/Source/DafnyCore/Rewriters/ExpectContracts.cs index 79feda0ddb..738996a252 100644 --- a/Source/DafnyCore/Rewriters/ExpectContracts.cs +++ b/Source/DafnyCore/Rewriters/ExpectContracts.cs @@ -1,7 +1,6 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; -using Microsoft.Extensions.Logging.Abstractions; using static Microsoft.Dafny.RewriterErrors; namespace Microsoft.Dafny; @@ -222,39 +221,50 @@ private static void RegisterResolvedByMethod(Function f, TopLevelDeclWithMembers } /// - /// Add wrappers for certain top-level declarations in the given module. - /// This runs after the first pass of resolution so that it has access to - /// ghostness information, attributes and call targets. + /// Adds wrappers for certain top-level declarations in the given + /// program and redirects callers to call those wrappers instead of + /// the original members. + /// + /// This runs after resolution so that it has access to ghostness + /// information, attributes and call targets and after verification + /// because that makes the interaction with the refinement transformer + /// more straightforward. /// - /// The module to generate wrappers for and in. - internal override void PostResolveIntermediate(ModuleDefinition moduleDefinition) { - // Keep a list of members to wrap so that we don't modify the collection we're iterating over. - List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new(); - - moduleDefinition.CallRedirector = new(Reporter); - - // Find module members to wrap. - foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType()) { - foreach (var decl in topLevelDecl.Members) { - if (ShouldGenerateWrapper(decl)) { - membersToWrap.Add((topLevelDecl, decl)); + /// The program to generate wrappers for and in. + public override void PostVerification(Program program) { + // Create wrappers + foreach (var moduleDefinition in program.Modules()) { + + // Keep a list of members to wrap so that we don't modify the collection we're iterating over. + List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new(); + + moduleDefinition.CallRedirector = new(Reporter); + + // Find module members to wrap. + foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType()) { + foreach (var decl in topLevelDecl.Members) { + if (ShouldGenerateWrapper(decl)) { + membersToWrap.Add((topLevelDecl, decl)); + } } } - } - // Generate a wrapper for each of the members identified above. - foreach (var (topLevelDecl, decl) in membersToWrap) { - GenerateWrapper(moduleDefinition, topLevelDecl, decl); - } - moduleDefinition.CallRedirector.NewRedirections = wrappedDeclarations; - } + // Generate a wrapper for each of the members identified above. This + // need to happen after all declarations to wrap have been identified + // because it adds new declarations and would invalidate the iterator + // used during identification. + foreach (var (topLevelDecl, decl) in membersToWrap) { + GenerateWrapper(moduleDefinition, topLevelDecl, decl); + } + moduleDefinition.CallRedirector.NewRedirections = wrappedDeclarations; - public override void PostVerification(Program program) { - foreach (var module in program.CompileModules) { - foreach (var topLevelDecl in module.TopLevelDecls.OfType()) { + // Put redirections in place. Any wrappers to call will be in either + // this module or to a previously-processed module, so they'll already + // exist. + foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType()) { foreach (var decl in topLevelDecl.Members) { if (decl is ICallable callable) { - module.CallRedirector?.Visit(callable, decl); + moduleDefinition.CallRedirector?.Visit(callable, decl); } } } @@ -264,7 +274,7 @@ public override void PostVerification(Program program) { return; } - foreach (var module in program.CompileModules) { + foreach (var module in program.Modules()) { if (module.CallRedirector == null) { continue; } diff --git a/Source/DafnyCore/Triggers/QuantifiersCollector.cs b/Source/DafnyCore/Triggers/QuantifiersCollector.cs index 9603f82c36..13038fa9c6 100644 --- a/Source/DafnyCore/Triggers/QuantifiersCollector.cs +++ b/Source/DafnyCore/Triggers/QuantifiersCollector.cs @@ -21,15 +21,12 @@ public QuantifierCollector(ErrorReporter reporter) { } protected override bool VisitOneExpr(Expression expr, ref OldExpr/*?*/ enclosingOldContext) { - var e = expr as ComprehensionExpr; - // only consider quantifiers that are not empty (Bound.Vars.Count > 0) - if (e != null && e.BoundVars.Count > 0 && !quantifiers.Contains(e)) { - if (e is SetComprehension || e is MapComprehension) { + if (expr is ComprehensionExpr e && e.BoundVars.Count > 0 && !quantifiers.Contains(e)) { + if (e is SetComprehension or MapComprehension) { quantifiers.Add(e); quantifierCollections.Add(new QuantifiersCollection(e, Enumerable.Repeat(e, 1), reporter)); - } else if (e is ForallExpr || e is ExistsExpr) { - var quantifier = e as QuantifierExpr; + } else if (e is QuantifierExpr quantifier) { quantifiers.Add(quantifier); if (quantifier.SplitQuantifier != null) { var collection = quantifier.SplitQuantifier.Select(q => q as ComprehensionExpr).Where(q => q != null); @@ -41,8 +38,8 @@ protected override bool VisitOneExpr(Expression expr, ref OldExpr/*?*/ enclosing } } - if (expr is OldExpr) { - enclosingOldContext = (OldExpr)expr; + if (expr is OldExpr oldExpr) { + enclosingOldContext = oldExpr; } else if (enclosingOldContext != null) { // FIXME be more restrctive on the type of stuff that we annotate // Add the association (expr, oldContext) to exprsInOldContext. However, due to chaining expressions, // expr may already be a key in exprsInOldContext. diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index e84b7b142f..d740e69906 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1019,8 +1019,6 @@ void CheckOperand(Expression operand) { CheckOperand(e.E0); CheckOperand(e.E1); } - - } break; default: diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index cca3b5ce9b..7d376e6195 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -755,7 +755,7 @@ IEnumerable GuessWitnesses(BoundVar x, Expression expr) { yield return lit; } - var bounds = ModuleResolver.DiscoverAllBounds_SingleVar(x, expr); + var bounds = ModuleResolver.DiscoverAllBounds_SingleVar(x, expr, out _); foreach (var bound in bounds) { if (bound is ComprehensionExpr.IntBoundedPool) { var bnd = (ComprehensionExpr.IntBoundedPool)bound; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect index 1be0e48ded..2245d753c5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/diagnosticsFormats.legacy.dfy.expect @@ -10,7 +10,7 @@ Dafny program verifier finished with 1 verified, 2 errors Dafny program verifier finished with 1 verified, 2 errors {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":15,"character":0}}},"severity":2,"message":"module-level const declarations are always non-instance, so the \u0027static\u0027 keyword is not allowed here","source":"Parser","relatedInformation":[]} -{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":14,"character":8}}},"severity":4,"message":"newtype byte resolves as {:nativeType \u0022byte\u0022} (Detected Range: 0 .. 256)","source":"Resolver","relatedInformation":[]} +{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":14,"character":8}}},"severity":4,"message":"newtype byte resolves as {:nativeType \u0022byte\u0022} (detected range: 0 .. 256)","source":"Resolver","relatedInformation":[]} {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":16,"character":17}}},"severity":1,"message":"Error: result of operation might violate newtype constraint for \u0027byte\u0027","source":"Verifier","relatedInformation":[]} {"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":19,"character":16}}},"severity":1,"message":"Error: a precondition for this call could not be proved","source":"Verifier","relatedInformation":[{"location":{"filename":"diagnosticsFormats.legacy.dfy","uri":"file:///diagnosticsFormats.legacy.dfy","range":{"start":{"line":18,"character":35}}},"message":"Related location: this is the precondition that could not be proved"}]} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs new file mode 100644 index 0000000000..c6d90d8e16 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs @@ -0,0 +1,10 @@ +using System.Numerics; + +namespace M { + + public partial class __default { + public static BigInteger ExternMethod() { + return new BigInteger(5); + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs new file mode 100644 index 0000000000..efd74ded43 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs @@ -0,0 +1,10 @@ +using System.Numerics; + +namespace M { + + public partial class __default { + public static BigInteger ExternMethod() { + return new BigInteger(-5); + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy index eeabf52dd9..b9d761d758 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy @@ -1,4 +1,4 @@ -// RUN: ! %baredafny test %args --no-verify --unicode-char:false --test-assumptions=externs %s %s.externs.cs > %t +// RUN: ! %baredafny test %args --unicode-char:false --test-assumptions=externs %s %s.externs.cs > %t // RUN: %diff "%s.expect" "%t" // RUN: %OutputCheck --file-to-check "%S/AllExterns.cs" "%s" // CHECK: .*Foo____dafny__checked\(x\).* diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect index 347491a3cc..0cf0890ae3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect @@ -1,7 +1,7 @@ + +Dafny program verifier finished with 0 verified, 0 errors CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state. CheckExtern.dfy(22,12): Warning: The ensures clause at this location cannot be compiled to be tested at runtime because it references ghost state. - -Dafny program verifier did not attempt verification FooTest: FAILED CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy(3,12) BarTest: FAILED diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy new file mode 100644 index 0000000000..499fdeab85 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy @@ -0,0 +1,14 @@ +// RUN: %run "%s" --input "%S/AbstractExtern1.cs" --test-assumptions Externs +// RUN: %exits-with 3 %run "%s" --input "%S/AbstractExtern2.cs" --test-assumptions Externs +abstract module A { + method {:extern "ExternMethod"} Method() returns (r: int) + ensures r > 0 +} + +module M refines A { +} + +method Main() { + var x := M.Method(); + print x, "\n"; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy index 4cd380a97d..8986374753 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy @@ -1,4 +1,4 @@ -// RUN: ! %dafny /compile:4 /noVerify /runAllTests:1 /spillTargetCode:3 /testContracts:TestedExterns %s %s.externs.cs > %t +// RUN: ! %dafny /compile:4 /runAllTests:1 /spillTargetCode:3 /testContracts:TestedExterns %s %s.externs.cs > %t // RUN: %diff "%s.expect" "%t" // RUN: %OutputCheck --file-to-check "%S/TestedExterns.cs" "%s" // CHECK-NOT: .*Foo____dafny__checked\(x\).* diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect index 489654892a..3d25b4f587 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect @@ -1,7 +1,7 @@ + +Dafny program verifier finished with 0 verified, 0 errors CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state. CheckExtern.dfy(22,12): Warning: The ensures clause at this location cannot be compiled to be tested at runtime because it references ghost state. - -Dafny program verifier did not attempt verification TestedExterns.dfy(10,17): Warning: No :test code calls NotCalled FooTest: FAILED CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy(3,12) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy.expect index fdbf9742a3..db6ee0f352 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy.expect @@ -1,23 +1,23 @@ -NativeTypeResolution.dfy(4,8): Info: newtype V resolves as {:nativeType "byte"} (Detected Range: 0 .. 200) -NativeTypeResolution.dfy(5,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)' -NativeTypeResolution.dfy(6,35): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)' -NativeTypeResolution.dfy(8,42): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)' -NativeTypeResolution.dfy(10,50): Info: newtype A resolves as {:nativeType "int"} (Detected Range: 0 .. 256) -NativeTypeResolution.dfy(11,50): Info: newtype B resolves as {:nativeType "byte"} (Detected Range: 0 .. 256) -NativeTypeResolution.dfy(12,50): Info: newtype C resolves as {:nativeType "int"} (Detected Range: 0 .. 256) +NativeTypeResolution.dfy(4,8): Info: newtype V resolves as {:nativeType "byte"} (detected range: 0 .. 200) +NativeTypeResolution.dfy(5,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' +NativeTypeResolution.dfy(6,35): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' +NativeTypeResolution.dfy(8,42): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' +NativeTypeResolution.dfy(10,50): Info: newtype A resolves as {:nativeType "int"} (detected range: 0 .. 256) +NativeTypeResolution.dfy(11,50): Info: newtype B resolves as {:nativeType "byte"} (detected range: 0 .. 256) +NativeTypeResolution.dfy(12,50): Info: newtype C resolves as {:nativeType "int"} (detected range: 0 .. 256) NativeTypeResolution.dfy(14,35): Error: :nativeType 'reallylong' not known NativeTypeResolution.dfy(15,41): Error: :nativeType 'reallylong' not known NativeTypeResolution.dfy(17,31): Error: None of the types given in :nativeType arguments is supported by the current compilation target. Try supplying others. NativeTypeResolution.dfy(18,40): Error: None of the types given in :nativeType arguments is supported by the current compilation target. Try supplying others. -NativeTypeResolution.dfy(21,22): Error: Dafny's heuristics cannot find a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)' -NativeTypeResolution.dfy(22,22): Info: newtype I resolves as {:nativeType "sbyte"} (Detected Range: -2 .. 30) -NativeTypeResolution.dfy(23,27): Error: Dafny's heuristics cannot find a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)' -NativeTypeResolution.dfy(24,27): Info: newtype K resolves as {:nativeType "sbyte"} (Detected Range: -2 .. 30) +NativeTypeResolution.dfy(21,22): Error: Dafny's heuristics cannot find a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' +NativeTypeResolution.dfy(22,22): Info: newtype I resolves as {:nativeType "sbyte"} (detected range: -2 .. 30) +NativeTypeResolution.dfy(23,27): Error: Dafny's heuristics cannot find a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' +NativeTypeResolution.dfy(24,27): Info: newtype K resolves as {:nativeType "sbyte"} (detected range: -2 .. 30) NativeTypeResolution.dfy(29,27): Error: unexpected :nativeType argument NativeTypeResolution.dfy(30,21): Error: unexpected :nativeType argument NativeTypeResolution.dfy(31,28): Error: :nativeType can only be used on integral types -NativeTypeResolution.dfy(33,29): Error: Dafny's heuristics failed to confirm 'long' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)' -NativeTypeResolution.dfy(34,29): Error: Dafny's heuristics failed to confirm 'long' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)' -NativeTypeResolution.dfy(38,8): Info: newtype FF resolves as {:nativeType "sbyte"} (Detected Range: -20 .. 20) -NativeTypeResolution.dfy(39,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)' +NativeTypeResolution.dfy(33,29): Error: Dafny's heuristics failed to confirm 'long' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' +NativeTypeResolution.dfy(34,29): Error: Dafny's heuristics failed to confirm 'long' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' +NativeTypeResolution.dfy(38,8): Info: newtype FF resolves as {:nativeType "sbyte"} (detected range: -20 .. 20) +NativeTypeResolution.dfy(39,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' 15 resolution/type errors detected in NativeTypeResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraintsRefresh.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraintsRefresh.dfy.expect index fa6b4a359f..d851547554 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraintsRefresh.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraintsRefresh.dfy.expect @@ -1,6 +1,6 @@ TypeConstraintsRefresh.dfy(40,15): Error: RHS (of type bool) not assignable to LHS (of type int) TypeConstraintsRefresh.dfy(48,15): Error: RHS (of type bool) not assignable to LHS (of type int) -TypeConstraintsRefresh.dfy(56,15): Error: RHS (of type bool) not assignable to LHS (of type int) +TypeConstraintsRefresh.dfy(56,15): Error: RHS (of type int) not assignable to LHS (of type bool) TypeConstraintsRefresh.dfy(65,6): Error: RHS (of type bool) not assignable to LHS (of type int) TypeConstraintsRefresh.dfy(80,6): Error: RHS (of type MyInt) not assignable to LHS (of type int) TypeConstraintsRefresh.dfy(81,6): Error: RHS (of type int) not assignable to LHS (of type MyInt) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy index cfd65a9f6b..b76128e5e3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy @@ -962,35 +962,51 @@ module StaticReceivers { } } +module UnaryMinus { + // This modules contains some regression tests to make sure that -nat is an int, not a nat. + // This remains a problem in the old resolver, and was once a problem (for different reasons) + // in the new resolver. -/**************************************************************************************** - ******** TO DO ************************************************************************* - **************************************************************************************** + predicate Simple(n: nat, d: nat) { + var x := -d; // type of x should be inferred to be int, not nat + n == x + } -module StaticReceivers { - ghost predicate Caller0(s: seq, list: LinkedList) - { - s == list.StaticFunction(s) // uses "list" as an object to discard + function Abs(n: int): nat { + if n < 0 then -n else n } - ghost predicate Caller1(s: seq) + predicate IsNat(n: int) + ensures IsNat(n) <==> 0 <= n { - s == LinkedList.StaticFunction(s) // type parameters inferred + AtMost(n, 0) } - ghost predicate Caller2(s: seq) + predicate AtMost(n: int, d: nat) + requires d <= Abs(n) + ensures AtMost(n, d) <==> d <= n + decreases Abs(n) - d { - s == LinkedList.StaticFunction(s) + n == d || (n + d != 0 && AtMost(n, d + 1)) } - method Caller3() + predicate AtMost'(n: int, d: nat) + requires d <= Abs(n) + ensures AtMost'(n, d) <==> d <= n + decreases Abs(n) - d { - var s: seq; - var b := s == LinkedList.StaticFunction(s); + if n == d then + true + else if n == -d then // the -d here should not pose any problems + false + else + AtMost'(n, d + 1) } - class LinkedList { - static ghost function StaticFunction(sq: seq): seq + lemma Same(n: int, d: nat) + requires d <= Abs(n) + ensures AtMost(n, d) == AtMost'(n, d) + { } } @@ -1032,34 +1048,4 @@ datatype Tree = // Dafny rejects the call to MaxF, claiming that forall t | t in ts :: default <= f(t) might not hold. But default is 0 and f(t) // has type nat, so it should hold — and in fact just uncommenting the definition of fn above solves the issue… even if fn isn’t used. - -// ------------------ -// In this program, one has to write "n + d != 0" instead of "n != -d", because of a previously known problem with type inference - -predicate method ge0'(n: int) - ensures ge0'(n) <==> 0 <= n -{ - downup_search'(n, 0) -} - -function method Abs(n: int): nat { - if n < 0 then -n else n -} - -predicate method downup_search'(n: int, d: nat) - requires d <= Abs(n) - ensures downup_search'(n, d) <==> d <= n - decreases Abs(n) - d -{ - n == d || (n + d != 0 && downup_search'(n, d + 1)) - /* - if n - d == 0 then - true - else if n + d == 0 then - false - else - downup_search'(n, d + 1) - */ -} - ****************************************************************************************/ diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect index f8a277ab42..1f4e7c1309 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect @@ -11,4 +11,4 @@ TypeInferenceRefresh.dfy(633,24): Error: value does not satisfy the subset const TypeInferenceRefresh.dfy(145,30): Error: element might not be in domain TypeInferenceRefresh.dfy(216,26): Error: result of operation might violate newtype constraint for 'int8' -Dafny program verifier finished with 77 verified, 10 errors +Dafny program verifier finished with 83 verified, 10 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefreshErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefreshErrors.dfy.expect index 71446ed9e2..a196e13f80 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefreshErrors.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefreshErrors.dfy.expect @@ -6,8 +6,8 @@ TypeInferenceRefreshErrors.dfy(22,10): Error: a reads-clause expression must den TypeInferenceRefreshErrors.dfy(33,12): Error: type cast to reference type 'C' must be from an expression assignable to it (got 'D') TypeInferenceRefreshErrors.dfy(34,12): Error: type cast to reference type 'D' must be from an expression assignable to it (got 'C') TypeInferenceRefreshErrors.dfy(49,8): Error: the type ('E?') of this variable is underspecified -TypeInferenceRefreshErrors.dfy(50,16): Error: the type ('E') of this cast target is underspecified -TypeInferenceRefreshErrors.dfy(51,16): Error: the type ('E>') of this cast target is underspecified +TypeInferenceRefreshErrors.dfy(50,16): Error: the type ('E') of this expression is underspecified +TypeInferenceRefreshErrors.dfy(51,16): Error: the type ('E>') of this expression is underspecified TypeInferenceRefreshErrors.dfy(64,8): Error: the type ('map') of this local variable is underspecified TypeInferenceRefreshErrors.dfy(65,8): Error: the type ('map') of this local variable is underspecified TypeInferenceRefreshErrors.dfy(66,8): Error: the type ('map') of this local variable is underspecified diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue90.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue90.dfy index 04e3e9b990..007ddeb40c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue90.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue90.dfy @@ -1,8 +1,6 @@ -// RUN: %exits-with 2 %dafny /compile:3 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code 2 "%s" + const x: MyInt := 200 const y: int := x as int + 180 newtype MyInt = k | 0 <= k < y - - diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue90.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue90.dfy.refresh.expect new file mode 100644 index 0000000000..21682fc56c --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue90.dfy.refresh.expect @@ -0,0 +1,2 @@ +git-issue90.dfy(4,6): Error: const definition contains a cycle: x -> MyInt -> y -> x +1 resolution/type errors detected in git-issue90.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276.dfy.expect index 039d4aa8d2..c584b4f05c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276.dfy.expect @@ -1,20 +1,20 @@ -git-issue-276.dfy(7,10): Info: newtype byte resolves as {:nativeType "byte"} (Detected Range: 0 .. 256) -git-issue-276.dfy(8,10): Info: newtype b0 resolves as {:nativeType "ushort"} (Detected Range: 0 .. 2560) -git-issue-276.dfy(9,10): Info: newtype b1 resolves as {:nativeType "byte"} (Detected Range: 0 .. 5) -git-issue-276.dfy(10,10): Info: newtype b2 resolves as {:nativeType "byte"} (Detected Range: 0 .. 10) -git-issue-276.dfy(11,10): Info: newtype b3 resolves as {:nativeType "byte"} (Detected Range: 0 .. 5) -git-issue-276.dfy(12,10): Info: newtype b3a resolves as {:nativeType "byte"} (Detected Range: 0 .. 5) -git-issue-276.dfy(13,10): Info: newtype b4 resolves as {:nativeType "byte"} (Detected Range: 0 .. 7) -git-issue-276.dfy(14,10): Info: newtype b4a resolves as {:nativeType "byte"} (Detected Range: 0 .. 7) -git-issue-276.dfy(15,10): Info: newtype b5 resolves as {:nativeType "byte"} (Detected Range: 0 .. 42) -git-issue-276.dfy(16,10): Info: newtype b6 resolves as {:nativeType "byte"} (Detected Range: 0 .. 20) -git-issue-276.dfy(17,10): Info: newtype b7 resolves as {:nativeType "byte"} (Detected Range: 0 .. 42) -git-issue-276.dfy(18,10): Info: newtype b8 resolves as {:nativeType "byte"} (Detected Range: 0 .. 20) -git-issue-276.dfy(19,10): Info: newtype b9 resolves as {:nativeType "byte"} (Detected Range: 0 .. 42) -git-issue-276.dfy(20,10): Info: newtype ba resolves as {:nativeType "byte"} (Detected Range: 0 .. 20) -git-issue-276.dfy(21,10): Info: newtype b3b resolves as {:nativeType "byte"} (Detected Range: 0 .. 6) -git-issue-276.dfy(22,10): Info: newtype b4b resolves as {:nativeType "byte"} (Detected Range: 0 .. 10) -git-issue-276.dfy(38,10): Info: newtype cx resolves as {:nativeType "byte"} (Detected Range: 0 .. 4) +git-issue-276.dfy(7,10): Info: newtype byte resolves as {:nativeType "byte"} (detected range: 0 .. 256) +git-issue-276.dfy(8,10): Info: newtype b0 resolves as {:nativeType "ushort"} (detected range: 0 .. 2560) +git-issue-276.dfy(9,10): Info: newtype b1 resolves as {:nativeType "byte"} (detected range: 0 .. 5) +git-issue-276.dfy(10,10): Info: newtype b2 resolves as {:nativeType "byte"} (detected range: 0 .. 10) +git-issue-276.dfy(11,10): Info: newtype b3 resolves as {:nativeType "byte"} (detected range: 0 .. 5) +git-issue-276.dfy(12,10): Info: newtype b3a resolves as {:nativeType "byte"} (detected range: 0 .. 5) +git-issue-276.dfy(13,10): Info: newtype b4 resolves as {:nativeType "byte"} (detected range: 0 .. 7) +git-issue-276.dfy(14,10): Info: newtype b4a resolves as {:nativeType "byte"} (detected range: 0 .. 7) +git-issue-276.dfy(15,10): Info: newtype b5 resolves as {:nativeType "byte"} (detected range: 0 .. 42) +git-issue-276.dfy(16,10): Info: newtype b6 resolves as {:nativeType "byte"} (detected range: 0 .. 20) +git-issue-276.dfy(17,10): Info: newtype b7 resolves as {:nativeType "byte"} (detected range: 0 .. 42) +git-issue-276.dfy(18,10): Info: newtype b8 resolves as {:nativeType "byte"} (detected range: 0 .. 20) +git-issue-276.dfy(19,10): Info: newtype b9 resolves as {:nativeType "byte"} (detected range: 0 .. 42) +git-issue-276.dfy(20,10): Info: newtype ba resolves as {:nativeType "byte"} (detected range: 0 .. 20) +git-issue-276.dfy(21,10): Info: newtype b3b resolves as {:nativeType "byte"} (detected range: 0 .. 6) +git-issue-276.dfy(22,10): Info: newtype b4b resolves as {:nativeType "byte"} (detected range: 0 .. 10) +git-issue-276.dfy(38,10): Info: newtype cx resolves as {:nativeType "byte"} (detected range: 0 .. 4) git-issue-276.dfy(25,17): Error: result of operation might violate newtype constraint for 'byte' git-issue-276.dfy(29,18): Error: result of operation might violate newtype constraint for 'b2' git-issue-276.dfy(32,18): Error: result of operation might violate newtype constraint for 'b3' diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy index 36cd4ec144..4c0e395ac6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy @@ -30,3 +30,48 @@ module Main { newtype c3 = x | 0 <= x < "abcde"[6] as int } +module Regression { + newtype GoodUint32 = i: int | 0 <= i < + if "abcrimini"[2 + 1 - 1] == 'c' then + 0x1_0000_0000 + 1 - 1 + else + 3 + + // Regression test: The following once crashed, because it had expected + // the SeqSelect index to really be a folded integer + newtype NotUint32 = i: int | 0 <= i < + if "abcrimini"[2 + 1 - 1 + k] == 'c' then + 0x1_0000_0000 + 1 - 1 + else + 3 + + const k: int +} + +module MoreTests { + const bv: bv19 := 203 + + newtype EmptyFitsIntoUint8 = i: int | + -0x8000_0000 <= i < if !true then 128 else -0x1_0000_0000 // empty range + witness * + + newtype int8 = i: int | + -128 <= i < if !true then -200 else 128 + + newtype AnotherInt8 = i: int | + -128 <= i < if true ==> bv == 203 then 128 else -200 + + newtype Int16 = i: int | + -128 <= i < if true ==> bv == 204 then 128 else 1234 +} + +module NotJustInequalityConstraints { + newtype Just7 = x: int | 0 <= x < 256 && x == 7 witness 7 // 7..8 + newtype Just8 = x: int | x == 8 && x == 8 witness 8 // 8..9 + newtype Also8 = x: int | 8 == x && x < 10 && x < 100 && -2 <= x witness 8 // 8..9 + newtype Small = x: int | x < 10 && x < 100 && -2 <= x witness 8 // -2..10 + newtype Only8ButDoesNotDetectCompleteRange = x: int | x == 8 && true witness 8 // 8..9 + newtype Empty = x: int | 8 == x == 7 && 0 <= x < 256 witness * // empty + newtype Byte = x: int | x in {2, 3, 5} witness 3 + newtype ByteWithKnownRange = x: int | x in {2, 3, 5} && 2 <= x <= 5 witness 3 // 2..6 +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy.expect index 8aed05ec05..5954875ab3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276a.dfy.expect @@ -1,6 +1,18 @@ -git-issue-276a.dfy(23,10): Info: newtype c0 resolves as {:nativeType "byte"} (Detected Range: 0 .. 100) -git-issue-276a.dfy(27,10): Info: newtype c1 resolves as {:nativeType "byte"} (Detected Range: 0 .. 100) -git-issue-276a.dfy(28,10): Info: newtype c2 resolves as {:nativeType "byte"} (Detected Range: 0 .. 50) +git-issue-276a.dfy(23,10): Info: newtype c0 resolves as {:nativeType "byte"} (detected range: 0 .. 100) +git-issue-276a.dfy(27,10): Info: newtype c1 resolves as {:nativeType "byte"} (detected range: 0 .. 100) +git-issue-276a.dfy(28,10): Info: newtype c2 resolves as {:nativeType "byte"} (detected range: 0 .. 50) +git-issue-276a.dfy(34,10): Info: newtype GoodUint32 resolves as {:nativeType "uint"} (detected range: 0 .. 4294967296) +git-issue-276a.dfy(54,10): Info: newtype EmptyFitsIntoUint8 resolves as {:nativeType "byte"} (detected range: empty) +git-issue-276a.dfy(58,10): Info: newtype int8 resolves as {:nativeType "sbyte"} (detected range: -128 .. 128) +git-issue-276a.dfy(61,10): Info: newtype AnotherInt8 resolves as {:nativeType "sbyte"} (detected range: -128 .. 128) +git-issue-276a.dfy(64,10): Info: newtype Int16 resolves as {:nativeType "short"} (detected range: -128 .. 1234) +git-issue-276a.dfy(69,10): Info: newtype Just7 resolves as {:nativeType "byte"} (detected range: 7 .. 8) +git-issue-276a.dfy(70,10): Info: newtype Just8 resolves as {:nativeType "byte"} (detected range: 8 .. 9) +git-issue-276a.dfy(71,10): Info: newtype Also8 resolves as {:nativeType "byte"} (detected range: 8 .. 9) +git-issue-276a.dfy(72,10): Info: newtype Small resolves as {:nativeType "sbyte"} (detected range: -2 .. 10) +git-issue-276a.dfy(73,10): Info: newtype Only8ButDoesNotDetectCompleteRange resolves as {:nativeType "byte"} (detected range: 8 .. 9) +git-issue-276a.dfy(74,10): Info: newtype Empty resolves as {:nativeType "byte"} (detected range: empty) +git-issue-276a.dfy(76,10): Info: newtype ByteWithKnownRange resolves as {:nativeType "byte"} (detected range: 2 .. 6) git-issue-276a.dfy(5,10): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type git-issue-276a.dfy(5,26): Related location git-issue-276a.dfy(5,29): Error: possible division by zero @@ -37,5 +49,6 @@ git-issue-276a.dfy(21,40): Error: shift amount must be non-negative git-issue-276a.dfy(30,10): Error: cannot find witness that shows type is inhabited (only tried 0); try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type git-issue-276a.dfy(30,26): Related location git-issue-276a.dfy(30,35): Error: index out of range +git-issue-276a.dfy(43,18): Error: index out of range -Dafny program verifier finished with 4 verified, 27 errors +Dafny program verifier finished with 15 verified, 28 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276b.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276b.dfy.expect index 36fc8e9cca..80e07c3f25 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276b.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276b.dfy.expect @@ -1,12 +1,12 @@ -git-issue-276b.dfy(6,10): Info: newtype b0 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276b.dfy(7,10): Info: newtype b1 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276b.dfy(8,10): Info: newtype b2 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276b.dfy(9,10): Info: newtype b3 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276b.dfy(10,10): Info: newtype b4 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276b.dfy(11,10): Info: newtype b5 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276b.dfy(12,10): Info: newtype b6 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276b.dfy(13,10): Info: newtype b7 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276b.dfy(14,10): Info: newtype b8 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276b.dfy(15,10): Info: newtype b9 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) +git-issue-276b.dfy(6,10): Info: newtype b0 resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276b.dfy(7,10): Info: newtype b1 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276b.dfy(8,10): Info: newtype b2 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276b.dfy(9,10): Info: newtype b3 resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276b.dfy(10,10): Info: newtype b4 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276b.dfy(11,10): Info: newtype b5 resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276b.dfy(12,10): Info: newtype b6 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276b.dfy(13,10): Info: newtype b7 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276b.dfy(14,10): Info: newtype b8 resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276b.dfy(15,10): Info: newtype b9 resolves as {:nativeType "byte"} (detected range: 0 .. 30) Dafny program verifier finished with 10 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276c.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276c.dfy.expect index b5c6b296b0..f91383ad20 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276c.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276c.dfy.expect @@ -1,19 +1,19 @@ -git-issue-276c.dfy(8,10): Info: newtype b0 resolves as {:nativeType "byte"} (Detected Range: 0 .. 10) -git-issue-276c.dfy(9,10): Info: newtype b1 resolves as {:nativeType "byte"} (Detected Range: 0 .. 101) -git-issue-276c.dfy(10,10): Info: newtype b2 resolves as {:nativeType "byte"} (Detected Range: 0 .. 101) -git-issue-276c.dfy(11,10): Info: newtype b3 resolves as {:nativeType "byte"} (Detected Range: 0 .. 20) -git-issue-276c.dfy(12,10): Info: newtype b4 resolves as {:nativeType "byte"} (Detected Range: 0 .. 200) -git-issue-276c.dfy(13,10): Info: newtype b5 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276c.dfy(14,10): Info: newtype b6 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276c.dfy(15,10): Info: newtype b7 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276c.dfy(16,10): Info: newtype b8 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276c.dfy(17,10): Info: newtype b9 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276c.dfy(18,10): Info: newtype ba resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276c.dfy(19,10): Info: newtype bb resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276c.dfy(20,10): Info: newtype bc resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276c.dfy(21,10): Info: newtype bd resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276c.dfy(22,10): Info: newtype be resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276c.dfy(23,10): Info: newtype bf resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276c.dfy(24,10): Info: newtype bg resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) +git-issue-276c.dfy(8,10): Info: newtype b0 resolves as {:nativeType "byte"} (detected range: 0 .. 10) +git-issue-276c.dfy(9,10): Info: newtype b1 resolves as {:nativeType "byte"} (detected range: 0 .. 101) +git-issue-276c.dfy(10,10): Info: newtype b2 resolves as {:nativeType "byte"} (detected range: 0 .. 101) +git-issue-276c.dfy(11,10): Info: newtype b3 resolves as {:nativeType "byte"} (detected range: 0 .. 20) +git-issue-276c.dfy(12,10): Info: newtype b4 resolves as {:nativeType "byte"} (detected range: 0 .. 200) +git-issue-276c.dfy(13,10): Info: newtype b5 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276c.dfy(14,10): Info: newtype b6 resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276c.dfy(15,10): Info: newtype b7 resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276c.dfy(16,10): Info: newtype b8 resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276c.dfy(17,10): Info: newtype b9 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276c.dfy(18,10): Info: newtype ba resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276c.dfy(19,10): Info: newtype bb resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276c.dfy(20,10): Info: newtype bc resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276c.dfy(21,10): Info: newtype bd resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276c.dfy(22,10): Info: newtype be resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276c.dfy(23,10): Info: newtype bf resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276c.dfy(24,10): Info: newtype bg resolves as {:nativeType "byte"} (detected range: 0 .. 30) Dafny program verifier finished with 18 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276r.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276r.dfy.expect index eecf2b5275..f299e12505 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276r.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276r.dfy.expect @@ -1,18 +1,18 @@ -git-issue-276r.dfy(6,10): Info: newtype b0 resolves as {:nativeType "byte"} (Detected Range: 0 .. 5) -git-issue-276r.dfy(7,10): Info: newtype b1 resolves as {:nativeType "byte"} (Detected Range: 0 .. 1) -git-issue-276r.dfy(8,10): Info: newtype b2 resolves as {:nativeType "byte"} (Detected Range: 0 .. 6) -git-issue-276r.dfy(10,10): Info: newtype b4 resolves as {:nativeType "byte"} (Detected Range: 0 .. 2) -git-issue-276r.dfy(11,10): Info: newtype b5 resolves as {:nativeType "ushort"} (Detected Range: 0 .. 1000) -git-issue-276r.dfy(12,10): Info: newtype b6 resolves as {:nativeType "byte"} (Detected Range: 0 .. 99) -git-issue-276r.dfy(13,10): Info: newtype b7 resolves as {:nativeType "ushort"} (Detected Range: 0 .. 2000) -git-issue-276r.dfy(14,10): Info: newtype b8 resolves as {:nativeType "byte"} (Detected Range: 0 .. 20) -git-issue-276r.dfy(15,10): Info: newtype b9 resolves as {:nativeType "byte"} (Detected Range: 0 .. 20) -git-issue-276r.dfy(16,10): Info: newtype b10 resolves as {:nativeType "byte"} (Detected Range: 0 .. 30) -git-issue-276r.dfy(17,10): Info: newtype b11 resolves as {:nativeType "byte"} (Detected Range: 0 .. 35) -git-issue-276r.dfy(18,10): Info: newtype b12 resolves as {:nativeType "byte"} (Detected Range: 0 .. 35) -git-issue-276r.dfy(19,10): Info: newtype b13 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276r.dfy(20,10): Info: newtype b14 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276r.dfy(21,10): Info: newtype b15 resolves as {:nativeType "byte"} (Detected Range: 0 .. 40) -git-issue-276r.dfy(22,10): Info: newtype b16 resolves as {:nativeType "byte"} (Detected Range: 0 .. 35) +git-issue-276r.dfy(6,10): Info: newtype b0 resolves as {:nativeType "byte"} (detected range: 0 .. 5) +git-issue-276r.dfy(7,10): Info: newtype b1 resolves as {:nativeType "byte"} (detected range: 0 .. 1) +git-issue-276r.dfy(8,10): Info: newtype b2 resolves as {:nativeType "byte"} (detected range: 0 .. 6) +git-issue-276r.dfy(10,10): Info: newtype b4 resolves as {:nativeType "byte"} (detected range: 0 .. 2) +git-issue-276r.dfy(11,10): Info: newtype b5 resolves as {:nativeType "ushort"} (detected range: 0 .. 1000) +git-issue-276r.dfy(12,10): Info: newtype b6 resolves as {:nativeType "byte"} (detected range: 0 .. 99) +git-issue-276r.dfy(13,10): Info: newtype b7 resolves as {:nativeType "ushort"} (detected range: 0 .. 2000) +git-issue-276r.dfy(14,10): Info: newtype b8 resolves as {:nativeType "byte"} (detected range: 0 .. 20) +git-issue-276r.dfy(15,10): Info: newtype b9 resolves as {:nativeType "byte"} (detected range: 0 .. 20) +git-issue-276r.dfy(16,10): Info: newtype b10 resolves as {:nativeType "byte"} (detected range: 0 .. 30) +git-issue-276r.dfy(17,10): Info: newtype b11 resolves as {:nativeType "byte"} (detected range: 0 .. 35) +git-issue-276r.dfy(18,10): Info: newtype b12 resolves as {:nativeType "byte"} (detected range: 0 .. 35) +git-issue-276r.dfy(19,10): Info: newtype b13 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276r.dfy(20,10): Info: newtype b14 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276r.dfy(21,10): Info: newtype b15 resolves as {:nativeType "byte"} (detected range: 0 .. 40) +git-issue-276r.dfy(22,10): Info: newtype b16 resolves as {:nativeType "byte"} (detected range: 0 .. 35) Dafny program verifier finished with 17 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276v.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276v.dfy.expect index 5766d66e02..d79e1fbf89 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276v.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276v.dfy.expect @@ -1,20 +1,20 @@ -git-issue-276v.dfy(8,10): Info: newtype b0 resolves as {:nativeType "byte"} (Detected Range: 0 .. 57) -git-issue-276v.dfy(9,10): Info: newtype b1 resolves as {:nativeType "byte"} (Detected Range: 0 .. 239) -git-issue-276v.dfy(10,10): Info: newtype b2 resolves as {:nativeType "byte"} (Detected Range: 0 .. 228) -git-issue-276v.dfy(11,10): Info: newtype b3 resolves as {:nativeType "byte"} (Detected Range: 0 .. 1) -git-issue-276v.dfy(12,10): Info: newtype b4 resolves as {:nativeType "byte"} (Detected Range: 0 .. 17) -git-issue-276v.dfy(13,10): Info: newtype b5 resolves as {:nativeType "byte"} (Detected Range: 0 .. 17) -git-issue-276v.dfy(14,10): Info: newtype b6 resolves as {:nativeType "byte"} (Detected Range: 0 .. 4) -git-issue-276v.dfy(15,10): Info: newtype b7 resolves as {:nativeType "byte"} (Detected Range: 0 .. 49) -git-issue-276v.dfy(16,10): Info: newtype b8 resolves as {:nativeType "byte"} (Detected Range: 0 .. 53) -git-issue-276v.dfy(17,10): Info: newtype b9 resolves as {:nativeType "byte"} (Detected Range: 0 .. 235) -git-issue-276v.dfy(18,10): Info: newtype ba resolves as {:nativeType "byte"} (Detected Range: 0 .. 24) -git-issue-276v.dfy(19,10): Info: newtype bb resolves as {:nativeType "byte"} (Detected Range: 0 .. 24) -git-issue-276v.dfy(20,10): Info: newtype bc resolves as {:nativeType "byte"} (Detected Range: 0 .. 56) -git-issue-276v.dfy(21,10): Info: newtype bd resolves as {:nativeType "byte"} (Detected Range: 0 .. 56) -git-issue-276v.dfy(22,10): Info: newtype be resolves as {:nativeType "byte"} (Detected Range: 0 .. 56) -git-issue-276v.dfy(23,10): Info: newtype bf resolves as {:nativeType "byte"} (Detected Range: 0 .. 24) -git-issue-276v.dfy(24,10): Info: newtype bg resolves as {:nativeType "byte"} (Detected Range: 0 .. 64) -git-issue-276v.dfy(25,10): Info: newtype bh resolves as {:nativeType "byte"} (Detected Range: 0 .. 18) +git-issue-276v.dfy(8,10): Info: newtype b0 resolves as {:nativeType "byte"} (detected range: 0 .. 57) +git-issue-276v.dfy(9,10): Info: newtype b1 resolves as {:nativeType "byte"} (detected range: 0 .. 239) +git-issue-276v.dfy(10,10): Info: newtype b2 resolves as {:nativeType "byte"} (detected range: 0 .. 228) +git-issue-276v.dfy(11,10): Info: newtype b3 resolves as {:nativeType "byte"} (detected range: 0 .. 1) +git-issue-276v.dfy(12,10): Info: newtype b4 resolves as {:nativeType "byte"} (detected range: 0 .. 17) +git-issue-276v.dfy(13,10): Info: newtype b5 resolves as {:nativeType "byte"} (detected range: 0 .. 17) +git-issue-276v.dfy(14,10): Info: newtype b6 resolves as {:nativeType "byte"} (detected range: 0 .. 4) +git-issue-276v.dfy(15,10): Info: newtype b7 resolves as {:nativeType "byte"} (detected range: 0 .. 49) +git-issue-276v.dfy(16,10): Info: newtype b8 resolves as {:nativeType "byte"} (detected range: 0 .. 53) +git-issue-276v.dfy(17,10): Info: newtype b9 resolves as {:nativeType "byte"} (detected range: 0 .. 235) +git-issue-276v.dfy(18,10): Info: newtype ba resolves as {:nativeType "byte"} (detected range: 0 .. 24) +git-issue-276v.dfy(19,10): Info: newtype bb resolves as {:nativeType "byte"} (detected range: 0 .. 24) +git-issue-276v.dfy(20,10): Info: newtype bc resolves as {:nativeType "byte"} (detected range: 0 .. 56) +git-issue-276v.dfy(21,10): Info: newtype bd resolves as {:nativeType "byte"} (detected range: 0 .. 56) +git-issue-276v.dfy(22,10): Info: newtype be resolves as {:nativeType "byte"} (detected range: 0 .. 56) +git-issue-276v.dfy(23,10): Info: newtype bf resolves as {:nativeType "byte"} (detected range: 0 .. 24) +git-issue-276v.dfy(24,10): Info: newtype bg resolves as {:nativeType "byte"} (detected range: 0 .. 64) +git-issue-276v.dfy(25,10): Info: newtype bh resolves as {:nativeType "byte"} (detected range: 0 .. 18) Dafny program verifier finished with 18 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy new file mode 100644 index 0000000000..1a30cd5996 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy @@ -0,0 +1,15 @@ +// RUN: %dafny /compile:0 /typeSystemRefresh:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +class Element { } + +class Foo { + function Collect(M: set): bool + reads this, set a | a in M + // The legacy resolver inferred "a" in the following line to have type "Foo", + // which results in a type error. This has been fixed in the new resolver. + decreases (set a | a in M) + {this} + { + true + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy.expect new file mode 100644 index 0000000000..012f5b9937 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy new file mode 100644 index 0000000000..56d6e389f1 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy @@ -0,0 +1,15 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=0 "%s" + +module A +{ + export + provides T + + newtype T = int +} + +module B +{ + import A + type X = A.T +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy.expect new file mode 100644 index 0000000000..012f5b9937 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4893.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy new file mode 100644 index 0000000000..172c568fe6 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy @@ -0,0 +1,200 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" + + +method Main() { + Tests.Test(); + SubsetTypeSubsetType.Test(); + SubsetTypeNewtype.Test(); + NewtypeSubsetType.Test(); + NewtypeNewtype.Test(); +} + +module Tests { + ghost predicate P(x: int) { x != 3 } + + type PlainInt = int // type synonym + type PInt = x: int | P(x) + type PNat = x: int | 0 <= x && P(x) + + newtype MyPlainInt = int + newtype MyPInt = x: int | P(x) + newtype MyPNat = x: int | 0 <= x && P(x) + + class Cell { + const k: int + constructor (k: int) { this.k := k; } + } + + type Cell5 = c: Cell | c.k == 5 witness * + + method Test() { + var nats; + nats := set nx: nat | 2 <= nx < 5; + print |nats|, "\n"; // 3 + + var r0, r1, r2; + r0 := set n0: PlainInt | 0 <= n0 < 5; + r1 := set n1: PInt | 2 <= n1 < 5; // error: this set comprehension is not compilable + r2 := set n2: PNat | n2 < 5; // error: this set comprehension is not compilable + print |r0|, " ", |r1|, " ", |r2|, "\n"; // 5 2 4 + var b0, b1; + b0 := forall k0: PInt | 2 <= k0 < 5 :: k0 != 3; // error: this set comprehension is not compilable + b1 := forall k1: PNat | k1 < 5 :: k1 != 4; // error: this set comprehension is not compilable + print b0, " ", b1, "\n"; // true false + + var s0, s1, s2; + s0 := set m0: MyPlainInt | 0 <= m0 < 5; + s1 := set m1: MyPInt | 2 <= m1 < 5; // error: this set comprehension is not compilable + s2 := set m2: MyPNat | m2 < 5; // error: this set comprehension is not compilable + print |s0|, " ", |s1|, " ", |s2|, "\n"; // 5 2 4 + b0 := forall l0: MyPInt | 2 <= l0 < 5 :: l0 as int != 3; // error: this set comprehension is not compilable + b1 := forall l1: MyPNat | l1 < 5 :: l1 != 4; // error: this set comprehension is not compilable + print b0, " ", b1, "\n"; // true false + + var c0 := new Cell(4); + var c1 := new Cell(5); + var cc: set := {null, c0, c1}; + var cc'0 := set y0: Cell? | y0 in cc; + var cc'1 := set y1: Cell | y1 in cc; + var cc'2 := set y2: Cell5 | y2 in cc; + print |cc|, " ", |cc'0|, " ", |cc'1|, " ", |cc'2|, "\n"; // 3 3 2 1 + } +} + +// check a compilable constraint with a non-compilable base type + +module SubsetTypeSubsetType { + ghost predicate P(x: int) { x != 3 } + + type NonCompilableTest = x: int | P(x) + type NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x) + + type Type0 = x: NonCompilableTest | true + type Type1 = NonCompilableTest + type Type2 = x: NonCompilableTestInt32 | true + type Type3 = NonCompilableTestInt32 + + predicate Q(x: int) { x != 5 } + + type CompilableTest = x: int | Q(x) && x < 8 + type Type4 = x: CompilableTest | true + type Type5 = CompilableTest + type Type6 = x: CompilableTest | 0 <= x + + method Test() { + var r0, r1, r2, r3; + r0 := set y: Type0 | 2 <= y < 6; // error: this set comprehension is not compilable + r1 := set y: Type1 | 2 <= y < 6; // error: this set comprehension is not compilable + r2 := set y: Type2 | 2 <= y < 6; // error: this set comprehension is not compilable + r3 := set y: Type3 | 2 <= y < 6; // error: this set comprehension is not compilable + print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3 + + var r4, r5, r6; + r4 := set y: Type4 | 2 <= y; + r5 := set y: Type5 | 2 <= y; + r6 := set y: Type6 | 2 <= y; + print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5 + } +} + +module SubsetTypeNewtype { + ghost predicate P(x: int) { x != 3 } + + type NonCompilableTest = x: int | P(x) + type NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x) + + newtype Type0 = x: NonCompilableTest | true + newtype Type1 = NonCompilableTest + newtype Type2 = x: NonCompilableTestInt32 | true + newtype Type3 = NonCompilableTestInt32 + + predicate Q(x: int) { x != 5 } + + type CompilableTest = x: int | Q(x) && x < 8 + newtype Type4 = x: CompilableTest | true + newtype Type5 = CompilableTest + newtype Type6 = x: CompilableTest | 0 <= x + + method Test() { + var r0, r1, r2, r3; + r0 := set y: Type0 | 2 <= y < 6; // error: this set comprehension is not compilable + r1 := set y: Type1 | 2 <= y < 6; // error: this set comprehension is not compilable + r2 := set y: Type2 | 2 <= y < 6; // error: this set comprehension is not compilable + r3 := set y: Type3 | 2 <= y < 6; // error: this set comprehension is not compilable + print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3 + + var r4, r5, r6; + r4 := set y: Type4 | 2 <= y; + r5 := set y: Type5 | 2 <= y; + r6 := set y: Type6 | 2 <= y; + print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5 + } +} + +module NewtypeSubsetType { + ghost predicate P(x: int) { x != 3 } + + newtype NonCompilableTest = x: int | P(x) + newtype NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x) + + type Type0 = x: NonCompilableTest | true + type Type1 = NonCompilableTest + type Type2 = x: NonCompilableTestInt32 | true + type Type3 = NonCompilableTestInt32 + + predicate Q(x: int) { x != 5 } + + newtype CompilableTest = x: int | Q(x) && x < 8 + type Type4 = x: CompilableTest | true + type Type5 = CompilableTest + type Type6 = x: CompilableTest | 0 <= x + + method Test() { + var r0, r1, r2, r3; + r0 := set y: Type0 | 2 <= y < 6; // error: this set comprehension is not compilable + r1 := set y: Type1 | 2 <= y < 6; // error: this set comprehension is not compilable + r2 := set y: Type2 | 2 <= y < 6; // error: this set comprehension is not compilable + r3 := set y: Type3 | 2 <= y < 6; // error: this set comprehension is not compilable + print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3 + + var r4, r5, r6; + r4 := set y: Type4 | 2 <= y; + r5 := set y: Type5 | 2 <= y; + r6 := set y: Type6 | 2 <= y; + print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5 + } +} + +module NewtypeNewtype { + ghost predicate P(x: int) { x != 3 } + + newtype NonCompilableTest = x: int | P(x) + newtype NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x) + + newtype Type0 = x: NonCompilableTest | true + newtype Type1 = NonCompilableTest + newtype Type2 = x: NonCompilableTestInt32 | true + newtype Type3 = NonCompilableTestInt32 + + predicate Q(x: int) { x != 5 } + + newtype CompilableTest = x: int | Q(x) && x < 8 + newtype Type4 = x: CompilableTest | true + newtype Type5 = CompilableTest + newtype Type6 = x: CompilableTest | 0 <= x + + method Test() { + var r0, r1, r2, r3; + r0 := set y: Type0 | 2 <= y < 6; // error: this set comprehension is not compilable + r1 := set y: Type1 | 2 <= y < 6; // error: this set comprehension is not compilable + r2 := set y: Type2 | 2 <= y < 6; // error: this set comprehension is not compilable + r3 := set y: Type3 | 2 <= y < 6; // error: this set comprehension is not compilable + print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3 + + var r4, r5, r6; + r4 := set y: Type4 | 2 <= y; + r5 := set y: Type5 | 2 <= y; + r6 := set y: Type6 | 2 <= y; + print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5 + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy.expect new file mode 100644 index 0000000000..644f539fc2 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697i.dfy.expect @@ -0,0 +1,26 @@ +git-issue-697i.dfy(37,14): Error: PInt is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(16,23) +git-issue-697i.dfy(38,14): Error: PNat is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(17,33) +git-issue-697i.dfy(41,17): Error: PInt is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(16,23) +git-issue-697i.dfy(42,17): Error: PNat is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(17,33) +git-issue-697i.dfy(47,14): Error: MyPInt is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(20,28) +git-issue-697i.dfy(48,14): Error: MyPNat is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(21,38) +git-issue-697i.dfy(50,17): Error: MyPInt is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(20,28) +git-issue-697i.dfy(51,17): Error: MyPNat is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(21,38) +git-issue-697i.dfy(86,14): Error: Type0 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(87,14): Error: Type1 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(69,36) +git-issue-697i.dfy(88,14): Error: Type2 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(89,14): Error: Type3 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(70,76) +git-issue-697i.dfy(120,14): Error: Type0 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(121,14): Error: Type1 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(122,14): Error: Type2 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(123,14): Error: Type3 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(154,14): Error: Type0 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(155,14): Error: Type1 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(137,39) +git-issue-697i.dfy(156,14): Error: Type2 is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(157,14): Error: Type3 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The constraint is not compilable because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate without the 'ghost' keyword) git-issue-697i.dfy(138,79) +git-issue-697i.dfy(188,14): Error: Type0 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(189,14): Error: Type1 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(190,14): Error: Type2 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(191,14): Error: Type3 is a newtype and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. +git-issue-697i.dfy(12,7): Error: not resolving module '_module' because there were errors in resolving its nested module 'Tests' +25 resolution/type errors detected in git-issue-697i.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy new file mode 100644 index 0000000000..b47a2f4cc6 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy @@ -0,0 +1,305 @@ +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" + +method Main() { + Tests.Test(); + + AnotherTest.Test(); + + SubsetTypeSubsetType.Test(); + SubsetTypeNewtype.Test(); + NewtypeSubsetType.Test(); + NewtypeNewtype.Test(); + + MoreNativeTypes.Test(); + + Regressions.Test0(); + Regressions.Test1(); + + EvolvingNativeTypes.Test(); +} + +module Tests { + predicate P(x: int) { x != 3 } + + type PlainInt = int // type synonym + type PInt = x: int | P(x) + type PNat = x: int | 0 <= x && P(x) + + newtype MyPlainInt = int + newtype MyPInt = x: int | P(x) + newtype MyPNat = x: int | 0 <= x && P(x) + + class Cell { + const k: int + constructor (k: int) { this.k := k; } + } + + type Cell5 = c: Cell | c.k == 5 witness * + + method Test() { + var nats; + nats := set nx: nat | 2 <= nx < 5; + print |nats|, "\n"; // 3 + + var r0, r1, r2; + r0 := set n0: PlainInt | 0 <= n0 < 5; + r1 := set n1: PInt | 2 <= n1 < 5; + r2 := set n2: PNat | n2 < 5; + print |r0|, " ", |r1|, " ", |r2|, "\n"; // 5 2 4 + var b0, b1; + b0 := forall k0: PInt | 2 <= k0 < 5 :: k0 != 3; + b1 := forall k1: PNat | k1 < 5 :: k1 != 4; + print b0, " ", b1, "\n"; // true false + + var s0, s1, s2; + s0 := set m0: MyPlainInt | 0 <= m0 < 5; + s1 := set m1: MyPInt | 2 <= m1 < 5; + s2 := set m2: MyPNat | m2 < 5; + print |s0|, " ", |s1|, " ", |s2|, "\n"; // 5 2 4 + b0 := forall l0: MyPInt | 2 <= l0 < 5 :: l0 as int != 3; + b1 := forall l1: MyPNat | l1 < 5 :: l1 != 4; + print b0, " ", b1, "\n"; // true false + + var c0 := new Cell(4); + var c1 := new Cell(5); + var cc: set := {null, c0, c1}; + var cc'0 := set y0: Cell? | y0 in cc; + var cc'1 := set y1: Cell | y1 in cc; + var cc'2 := set y2: Cell5 | y2 in cc; + print |cc|, " ", |cc'0|, " ", |cc'1|, " ", |cc'2|, "\n"; // 3 3 2 1 + } +} + +module AnotherTest { + predicate P(s: seq) { |s| <= 1 } + + type T = seq + type SST = s: T | P(s) + + method Test() { + var a0: T := []; + var a1: T := [25]; + var a2: T := [100, 101]; + var a3: T := [22]; + var S: set := { a0, a1, a2, a3 }; + var s1 := set m: SST | m in S; + print |s1|, "\n"; // 3 + } +} + +module SubsetTypeSubsetType { + predicate P(x: int) { x != 3 } + + type NonCompilableTest = x: int | P(x) + type NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x) + + type Type0 = x: NonCompilableTest | true + type Type1 = NonCompilableTest + type Type2 = x: NonCompilableTestInt32 | true + type Type3 = NonCompilableTestInt32 + + predicate Q(x: int) { x != 5 } + + type CompilableTest = x: int | Q(x) && x < 8 + type Type4 = x: CompilableTest | true + type Type5 = CompilableTest + type Type6 = x: CompilableTest | 0 <= x + + method Test() { + var r0, r1, r2, r3; + r0 := set y: Type0 | 2 <= y < 6; + r1 := set y: Type1 | 2 <= y < 6; + r2 := set y: Type2 | 2 <= y < 6; + r3 := set y: Type3 | 2 <= y < 6; + print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3 + + var r4, r5, r6; + r4 := set y: Type4 | 2 <= y; + r5 := set y: Type5 | 2 <= y; + r6 := set y: Type6 | 2 <= y; + print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5 + } +} + +module SubsetTypeNewtype { + predicate P(x: int) { x != 3 } + + type NonCompilableTest = x: int | P(x) + type NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x) + + newtype Type0 = x: NonCompilableTest | true + newtype Type1 = NonCompilableTest + newtype Type2 = x: NonCompilableTestInt32 | true + newtype Type3 = NonCompilableTestInt32 + + predicate Q(x: int) { x != 5 } + + type CompilableTest = x: int | Q(x) && x < 8 + newtype Type4 = x: CompilableTest | true + newtype Type5 = CompilableTest + newtype Type6 = x: CompilableTest | 0 <= x + + method Test() { + var r0, r1, r2, r3; + r0 := set y: Type0 | 2 <= y < 6; + r1 := set y: Type1 | 2 <= y < 6; + r2 := set y: Type2 | 2 <= y < 6; + r3 := set y: Type3 | 2 <= y < 6; + print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3 + + var r4, r5, r6; + r4 := set y: Type4 | 2 <= y; + r5 := set y: Type5 | 2 <= y; + r6 := set y: Type6 | 2 <= y; + print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5 + } +} + +module NewtypeSubsetType { + predicate P(x: int) { x != 3 } + + newtype NonCompilableTest = x: int | P(x) + newtype NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x) + + type Type0 = x: NonCompilableTest | true + type Type1 = NonCompilableTest + type Type2 = x: NonCompilableTestInt32 | true + type Type3 = NonCompilableTestInt32 + + predicate Q(x: int) { x != 5 } + + newtype CompilableTest = x: int | Q(x) && x < 8 + type Type4 = x: CompilableTest | true + type Type5 = CompilableTest + type Type6 = x: CompilableTest | 0 <= x + + method Test() { + var r0, r1, r2, r3; + r0 := set y: Type0 | 2 <= y < 6; + r1 := set y: Type1 | 2 <= y < 6; + r2 := set y: Type2 | 2 <= y < 6; + r3 := set y: Type3 | 2 <= y < 6; + print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3 + + var r4, r5, r6; + r4 := set y: Type4 | 2 <= y; + r5 := set y: Type5 | 2 <= y; + r6 := set y: Type6 | 2 <= y; + print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5 + } +} + +module NewtypeNewtype { + predicate P(x: int) { x != 3 } + + newtype NonCompilableTest = x: int | P(x) + newtype NonCompilableTestInt32 = x: int | -0x8000_0000 <= x < 0x8000_0000 && P(x) + + newtype Type0 = x: NonCompilableTest | true + newtype Type1 = NonCompilableTest + newtype Type2 = x: NonCompilableTestInt32 | true + newtype Type3 = NonCompilableTestInt32 + + predicate Q(x: int) { x != 5 } + + newtype CompilableTest = x: int | Q(x) && x < 8 + newtype Type4 = x: CompilableTest | true + newtype Type5 = CompilableTest + newtype Type6 = x: CompilableTest | 0 <= x + + method Test() { + var r0, r1, r2, r3; + r0 := set y: Type0 | 2 <= y < 6; + r1 := set y: Type1 | 2 <= y < 6; + r2 := set y: Type2 | 2 <= y < 6; + r3 := set y: Type3 | 2 <= y < 6; + print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, "\n"; // 3 3 3 3 + + var r4, r5, r6; + r4 := set y: Type4 | 2 <= y; + r5 := set y: Type5 | 2 <= y; + r6 := set y: Type6 | 2 <= y; + print |r4|, " ", |r5|, " ", |r6|, "\n"; // 5 5 5 + } +} + +module MoreNativeTypes { + type LoSubset = x: int | -0x8000_0000 <= x + newtype LoNewtype = x: int | -0x8000_0000 <= x + + newtype Int32a = x: LoSubset | x < 0x8000_0000 + newtype Int32b = x: LoNewtype | x < 0x8000_0000 + + type Int32c = x: Int32a | x != 3 + type Int32d = x: Int32b | x != 3 + newtype Int32e = x: Int32a | x != 3 + newtype Int32f = x: Int32b | x != 3 + + method Test() { + var r0, r1; + r0 := set y: Int32a | 2 <= y < 6; + r1 := set y: Int32b | 2 <= y < 6; + + var r2, r3, r4, r5; + r2 := set y: Int32c | 2 <= y < 6; + r3 := set y: Int32d | 2 <= y < 6; + r4 := set y: Int32e | 2 <= y < 6; + r5 := set y: Int32f | 2 <= y < 6; + + print |r0|, " ", |r1|, " ", |r2|, " ", |r3|, " ", |r4|, " ", |r5|, "\n"; // 4 4 3 3 3 3 + } +} + +module Regressions { + type byte = x | x < 256 && x != 7 && 0 <= x + + predicate P(x: int) { x == 7 || x == 9 } + + method Test0() { + var s := set b: byte | 5 <= b < 12 && P(b as int); + assert 9 in s; + var u :| u in s; + print u, "\n"; // 9 + } + + // ----------------------------- + + newtype NewByte = x | x < 256 && x != 7 && 0 <= x + + newtype ByteBase = x: int | x != 7 + type Byyyte = x: ByteBase | x < 256 && 0 <= x + + predicate Filter(x: int) { + x % 2 == 1 && x < 10 + } + + method Test1() { + var s := set b: byte | Filter(b as int); + var t := set b: NewByte | Filter(b as int); + var u := set b: Byyyte | Filter(b as int); + + print |s|, " ", |t|, " ", |u|, "\n"; // 4 4 4 + } +} + +module EvolvingNativeTypes { + newtype Nat = x: int | 0 <= x && x != 1 + newtype uint32 = x: Nat | x < 0x1_0000_0000 && x != 3 + newtype byte = x: uint32 | x < 256 && x != 5 + newtype Not7Either = x: byte | x != 7 + + predicate R(x: int) { + match x + case 5 => true + case 1 | 3 | 7 | 9 => true + case _ => false + } + + method Test() { + assert R(7); + var u: byte :| R(u as int) && u != 9; + assert R(9); + var v: Not7Either :| R(v as int); + print u, " ", v, "\n"; // 7 9 + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.expect new file mode 100644 index 0000000000..d70a0d3c3a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.expect @@ -0,0 +1,19 @@ +3 +5 2 4 +true false +5 2 4 +true false +3 3 2 1 +3 +3 3 3 3 +5 5 5 +3 3 3 3 +5 5 5 +3 3 3 3 +5 5 5 +3 3 3 3 +5 5 5 +4 4 3 3 3 3 +9 +4 4 4 +7 9 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect new file mode 100644 index 0000000000..f4e6be29b1 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect @@ -0,0 +1,49 @@ +git-issue-697j.dfy(41,12): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(45,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(46,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(47,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(50,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(51,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(55,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(56,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(57,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(59,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(60,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(110,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(111,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(112,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(113,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(117,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(118,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(119,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(144,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(145,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(146,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(147,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(151,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(152,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(153,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(178,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(179,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(180,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(181,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(185,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(186,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(187,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(212,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(213,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(214,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(215,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(219,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(220,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(221,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(240,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(241,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(244,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(245,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(246,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(247,10): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(259,13): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(277,13): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(278,13): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(279,13): Warning: /!\ No terms found to trigger on. diff --git a/docs/DafnyRef/Attributes.1.expect b/docs/DafnyRef/Attributes.1.expect index d0c9ed9455..1f16520357 100644 --- a/docs/DafnyRef/Attributes.1.expect +++ b/docs/DafnyRef/Attributes.1.expect @@ -1,2 +1,2 @@ -text.dfy(2,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)' +text.dfy(2,29): Error: Dafny's heuristics failed to confirm 'byte' to be a compatible native type. Hint: try writing a newtype constraint of the form 'i: int | lowerBound <= i < upperBound && (...any additional constraints...)' 1 resolution/type errors detected in text.dfy diff --git a/docs/dev/news/4737.fix b/docs/dev/news/4737.fix new file mode 100644 index 0000000000..1c51f55dbd --- /dev/null +++ b/docs/dev/news/4737.fix @@ -0,0 +1 @@ +Fix resolution of unary minus in new resolver diff --git a/docs/dev/news/4919.fix b/docs/dev/news/4919.fix new file mode 100644 index 0000000000..a1ed74df99 --- /dev/null +++ b/docs/dev/news/4919.fix @@ -0,0 +1 @@ +Compile run-time constraint checks for newtypes in comprehensions diff --git a/docs/dev/news/4921.fix b/docs/dev/news/4921.fix new file mode 100644 index 0000000000..1ab493755e --- /dev/null +++ b/docs/dev/news/4921.fix @@ -0,0 +1 @@ +Fix null dereference in constant-folding invalid string-indexing expressions diff --git a/docs/dev/news/4930.fix b/docs/dev/news/4930.fix new file mode 100644 index 0000000000..e5715cf937 --- /dev/null +++ b/docs/dev/news/4930.fix @@ -0,0 +1 @@ +Initialize additional fields in the AST