From 34e50ac76b685f39a0a90abde61d5d14a1917b60 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 2 Jan 2024 03:41:31 -0800 Subject: [PATCH] refactor: Extract constant folding into separate file (#4921) This PR does a refactoring of the code that partially evaluates expressions--that is, that performs constant folding. It also fixes a null dereference error along the way. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore/Resolver/ConstantFolder.cs | 487 +++++++++++++++ Source/DafnyCore/Resolver/ModuleResolver.cs | 589 +----------------- .../CheckTypeInferenceVisitor.cs | 2 +- .../PreType/UnderspecificationDetector.cs | 2 +- .../cli/diagnosticsFormats.legacy.dfy.expect | 2 +- .../dafny0/NativeTypeResolution.dfy.expect | 30 +- .../git-issues/git-issue-276.dfy.expect | 34 +- .../LitTest/git-issues/git-issue-276a.dfy | 45 ++ .../git-issues/git-issue-276a.dfy.expect | 21 +- .../git-issues/git-issue-276b.dfy.expect | 20 +- .../git-issues/git-issue-276c.dfy.expect | 34 +- .../git-issues/git-issue-276r.dfy.expect | 32 +- .../git-issues/git-issue-276v.dfy.expect | 36 +- docs/DafnyRef/Attributes.1.expect | 2 +- docs/dev/news/4921.fix | 1 + 15 files changed, 672 insertions(+), 665 deletions(-) create mode 100644 Source/DafnyCore/Resolver/ConstantFolder.cs create mode 100644 docs/dev/news/4921.fix diff --git a/Source/DafnyCore/Resolver/ConstantFolder.cs b/Source/DafnyCore/Resolver/ConstantFolder.cs new file mode 100644 index 00000000000..8ff8fa2a500 --- /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/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 6e78491a439..b8a980b4121 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2048,23 +2048,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); @@ -2131,567 +2114,43 @@ private void FigureOutNativeType(NewtypeDecl dd) { 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; - } - } - // 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; } @@ -2711,7 +2170,9 @@ Type AsUnconstrainedType(Type t) { if (nativeTypeChoices != null && nativeTypeChoices.Count == 1) { Contract.Assert(dd.NativeType == nativeTypeChoices[0]); } 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}"; + 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 +2180,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 054e0e3dbe7..e9333ead4fc 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/UnderspecificationDetector.cs b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs index f65473cb43f..f1fdc1a8876 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 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 1be0e48ded3..2245d753c52 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/dafny0/NativeTypeResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy.expect index fdbf9742a37..db6ee0f3520 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/git-issues/git-issue-276.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-276.dfy.expect index 039d4aa8d20..c584b4f05c4 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 36cd4ec1444..4c0e395ac6b 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 8aed05ec055..5954875ab30 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 36fc8e9cca7..80e07c3f25f 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 b5c6b296b0e..f91383ad20f 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 eecf2b52758..f299e125052 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 5766d66e02c..d79e1fbf890 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/docs/DafnyRef/Attributes.1.expect b/docs/DafnyRef/Attributes.1.expect index d0c9ed9455e..1f165203575 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/4921.fix b/docs/dev/news/4921.fix new file mode 100644 index 00000000000..1ab493755e5 --- /dev/null +++ b/docs/dev/news/4921.fix @@ -0,0 +1 @@ +Fix null dereference in constant-folding invalid string-indexing expressions