From 02326abeca88715427d09f8995ee5ccfd9dab397 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Fri, 17 Apr 2015 12:29:04 -0600 Subject: adding references to the floating point type wherever references to the real type exist. This remains a work in progress --- Source/Basetypes/Basetypes.csproj | 2 +- Source/Basetypes/fp32.cs | 62 +++++++++++++------------- Source/Core/AbsyExpr.cs | 15 +++++++ Source/Core/AbsyType.cs | 11 +++++ Source/Core/Core.csproj | 4 +- Source/Core/Parser.cs | 7 ++- Source/UnitTests/CoreTests/CoreTests.csproj | 2 +- Source/UnitTests/CoreTests/ExprImmutability.cs | 3 ++ 8 files changed, 69 insertions(+), 37 deletions(-) diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj index fea8eebc..84a6ffd1 100644 --- a/Source/Basetypes/Basetypes.csproj +++ b/Source/Basetypes/Basetypes.csproj @@ -163,7 +163,7 @@ - + diff --git a/Source/Basetypes/fp32.cs b/Source/Basetypes/fp32.cs index c64afa54..5d76737b 100644 --- a/Source/Basetypes/fp32.cs +++ b/Source/Basetypes/fp32.cs @@ -11,7 +11,7 @@ using System.Text; using System.Diagnostics.Contracts; using System.Diagnostics; -namespace Basetypes +namespace Microsoft.Basetypes { using BIM = System.Numerics.BigInteger; @@ -19,7 +19,7 @@ namespace Basetypes /// A representation of a 32-bit floating point value /// Note that this value has a 1-bit sign, 8-bit exponent, and 23-bit mantissa /// - public struct fp32 + public struct FP32 { //Please note that this code outline is copy-pasted from BigDec.cs @@ -43,7 +43,7 @@ namespace Basetypes } } - public static readonly fp32 ZERO = FromInt(0); + public static readonly FP32 ZERO = FromInt(0); private static readonly BIM two = new BIM(2); private static readonly BIM ten = new BIM(10); @@ -55,17 +55,17 @@ namespace Basetypes //For a complete summary of where this class has been added, simply view constructor references [Pure] - public static fp32 FromInt(int v) { - return new fp32(v, 0, v < 0); //TODO: modify for correct fp representation + public static FP32 FromInt(int v) { + return new FP32(v, 0, v < 0); //TODO: modify for correct fp representation } [Pure] - public static fp32 FromBigInt(BIM v) { - return new fp32(v, 0, v < 0); //TODO: modify for correct fp representation + public static FP32 FromBigInt(BIM v) { + return new FP32(v, 0, v < 0); //TODO: modify for correct fp representation } [Pure] - public static fp32 FromString(string v) { + public static FP32 FromString(string v) { //TODO: completely copied from BigDec.cs at the moment if (v == null) throw new FormatException(); @@ -100,10 +100,10 @@ namespace Basetypes fractionLen = fractionLen - 1; } } - return new fp32(integral - fraction, exponent, integral.Sign == -1); + return new FP32(integral - fraction, exponent, integral.Sign == -1); } - internal fp32(BIM mantissa, int exponent, bool isNegative) { + internal FP32(BIM mantissa, int exponent, bool isNegative) { this.isNegative = isNegative; if (mantissa.IsZero) { this.mantissa = mantissa; @@ -128,10 +128,10 @@ namespace Basetypes public override bool Equals(object obj) { if (obj == null) return false; - if (!(obj is fp32)) + if (!(obj is FP32)) return false; - return (this == (fp32)obj); + return (this == (FP32)obj); } [Pure] @@ -152,7 +152,7 @@ namespace Basetypes // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). /// - /// Computes the floor and ceiling of this fp32. Note the choice of rounding towards negative + /// Computes the floor and ceiling of this FP32. Note the choice of rounding towards negative /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way. /// /// The Floor (rounded towards negative infinity) @@ -277,28 +277,28 @@ namespace Basetypes // Basic arithmetic operations [Pure] - public fp32 Abs { + public FP32 Abs { //TODO: fix for fp functionality get { - return new fp32(BIM.Abs(this.mantissa), this.exponent, false); + return new FP32(BIM.Abs(this.mantissa), this.exponent, false); } } [Pure] - public fp32 Negate { + public FP32 Negate { //TODO: Modify for correct fp functionality get { - return new fp32(BIM.Negate(this.mantissa), this.exponent, this.Mantissa >= 0); + return new FP32(BIM.Negate(this.mantissa), this.exponent, this.Mantissa >= 0); } } [Pure] - public static fp32 operator -(fp32 x) { + public static FP32 operator -(FP32 x) { return x.Negate; } [Pure] - public static fp32 operator +(fp32 x, fp32 y) { + public static FP32 operator +(FP32 x, FP32 y) { //TODO: Modify for correct fp functionality BIM m1 = x.mantissa; int e1 = x.exponent; @@ -316,18 +316,18 @@ namespace Basetypes e2 = e2 - 1; } - return new fp32(m1 + m2, e1, true); + return new FP32(m1 + m2, e1, true); } [Pure] - public static fp32 operator -(fp32 x, fp32 y) { + public static FP32 operator -(FP32 x, FP32 y) { return x + y.Negate; } [Pure] - public static fp32 operator *(fp32 x, fp32 y) { + public static FP32 operator *(FP32 x, FP32 y) { //TODO: modify for correct fp functionality - return new fp32(x.mantissa * y.mantissa, x.exponent + y.exponent, false); + return new FP32(x.mantissa * y.mantissa, x.exponent + y.exponent, false); } @@ -353,44 +353,44 @@ namespace Basetypes } [Pure] - public int CompareTo(fp32 that) { + public int CompareTo(FP32 that) { //TODO: Modify for correct fp functionality if (this.mantissa == that.mantissa && this.exponent == that.exponent) { return 0; } else { - fp32 d = this - that; + FP32 d = this - that; return d.IsNegative ? -1 : 1; } } [Pure] - public static bool operator ==(fp32 x, fp32 y) { + public static bool operator ==(FP32 x, FP32 y) { return x.CompareTo(y) == 0; } [Pure] - public static bool operator !=(fp32 x, fp32 y) { + public static bool operator !=(FP32 x, FP32 y) { return x.CompareTo(y) != 0; } [Pure] - public static bool operator <(fp32 x, fp32 y) { + public static bool operator <(FP32 x, FP32 y) { return x.CompareTo(y) < 0; } [Pure] - public static bool operator >(fp32 x, fp32 y) { + public static bool operator >(FP32 x, FP32 y) { return x.CompareTo(y) > 0; } [Pure] - public static bool operator <=(fp32 x, fp32 y) { + public static bool operator <=(FP32 x, FP32 y) { return x.CompareTo(y) <= 0; } [Pure] - public static bool operator >=(fp32 x, fp32 y) { + public static bool operator >=(FP32 x, FP32 y) { return x.CompareTo(y) >= 0; } } diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index f3a943b8..00306a5e 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -552,6 +552,21 @@ namespace Microsoft.Boogie { CachedHashCode = ComputeHashCode(); } + /// + /// Creates a literal expression for the floating point value "v". + /// + /// + /// + public LiteralExpr(IToken/*!*/ tok, FP32 v, bool immutable = false) + : base(tok, immutable) + { + Contract.Requires(tok != null); + Val = v; + Type = Type.Float; + if (immutable) + CachedHashCode = ComputeHashCode(); + } + [Pure] [Reads(ReadsAttribute.Reads.Nothing)] public override bool Equals(object obj) { diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 97309155..ec8cd9e2 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -336,6 +336,7 @@ namespace Microsoft.Boogie { public static readonly Type/*!*/ Int = new BasicType(SimpleType.Int); public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real); + public static readonly Type/*!*/ Float = new BasicType(SimpleType.Float); public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool); private static BvType[] bvtypeCache; @@ -871,6 +872,8 @@ namespace Microsoft.Boogie { return "int"; case SimpleType.Real: return "real"; + case SimpleType.Float: + return "float"; case SimpleType.Bool: return "bool"; } @@ -993,6 +996,13 @@ namespace Microsoft.Boogie { return this.T == SimpleType.Real; } } + public override bool IsFloat + { + get + { + return this.T == SimpleType.Float; + } + } public override bool IsBool { get { return this.T == SimpleType.Bool; @@ -3526,6 +3536,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); public enum SimpleType { Int, Real, + Float, Bool }; diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 27f4eea7..fbb23cfe 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -34,7 +34,7 @@ false false true - Client + Client true @@ -186,7 +186,7 @@ - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} + {43dfad18-3e35-4558-9be2-caff6b5ba8a0} Basetypes diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 9a0bab51..1d4b38b8 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -664,8 +664,11 @@ private class BvBounds : Expr { ty = new BasicType(t, SimpleType.Int); } else if (la.kind == 15) { Get(); - ty = new BasicType(t, SimpleType.Real); - } else if (la.kind == 16) { + ty = new BasicType(t, SimpleType.Real); + } else if (la.kind == 112837) { + Get(); + ty = new BasicType(t, SimpleType.Float); + } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Bool); } else if (la.kind == 9) { diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj index 9b319d85..ddf310be 100644 --- a/Source/UnitTests/CoreTests/CoreTests.csproj +++ b/Source/UnitTests/CoreTests/CoreTests.csproj @@ -54,7 +54,7 @@ - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} + {43dfad18-3e35-4558-9be2-caff6b5ba8a0} Basetypes diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index b83983b6..7f266074 100644 --- a/Source/UnitTests/CoreTests/ExprImmutability.cs +++ b/Source/UnitTests/CoreTests/ExprImmutability.cs @@ -29,6 +29,9 @@ namespace CoreTests var literal4 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 8, /*immutable=*/true); Assert.AreEqual(literal4.ComputeHashCode(), literal4.GetHashCode()); + + var literal5 = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.FP32.FromInt(0), /*immutable=*/true); + Assert.AreEqual(literal5.ComputeHashCode(), literal5.GetHashCode()); } [Test()] -- cgit v1.2.3