From af8621462cf6b25a6dd29b63ed251629109d6bfb Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Sat, 16 Jul 2016 02:49:06 -0600 Subject: Changed the syntax reading of the float type --- Source/AbsInt/IntervalDomain.cs | 2 +- Source/Core/AbsyExpr.cs | 8 +++--- Source/Core/AbsyType.cs | 48 ++++++++++++++++++++++--------- Source/Provers/SMTLib/SMTLibLineariser.cs | 2 +- Source/VCExpr/Boogie2VCExpr.cs | 18 ++++++------ 5 files changed, 50 insertions(+), 28 deletions(-) (limited to 'Source') diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 0dd78cbb..9d37476f 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -232,7 +232,7 @@ namespace Microsoft.Boogie.AbstractInterpretation } else if (ty.IsReal) { return Expr.Literal(Basetypes.BigDec.FromBigInt(n)); } else if (ty.IsFloat) { - return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatMantissa)); + return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatSignificand)); } else { Contract.Assume(ty.IsInt); return Expr.Literal(Basetypes.BigNum.FromBigInt(n)); diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 5fc5fd54..bc2b4391 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1724,10 +1724,10 @@ namespace Microsoft.Boogie { return Type.Real; } if (arg0type.IsFloat && arg0type.Unify(arg1type)) { - return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); + return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand); } if (arg1type.IsFloat && arg1type.Unify(arg0type)) { - return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); + return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand); } goto BAD_TYPE; case Opcode.Div: @@ -1742,10 +1742,10 @@ namespace Microsoft.Boogie { return Type.Real; } if (arg0type.IsFloat && arg0type.Unify(arg1type)) { - return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); + return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand); } if (arg1type.IsFloat && arg1type.Unify(arg0type)) { - return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); + return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand); } goto BAD_TYPE; case Opcode.Pow: diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 96de5c0b..08cf37cc 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -340,12 +340,12 @@ namespace Microsoft.Boogie { } // Type.FloatExponent should never be called } } - public virtual int FloatMantissa { + public virtual int FloatSignificand { get { { Contract.Assert(false); throw new cce.UnreachableException(); - } // Type.FloatMantissa should never be called + } // Type.FloatSignificand should never be called } } public virtual bool IsBv { @@ -1046,20 +1046,20 @@ namespace Microsoft.Boogie { //Note that the functions in this class were directly copied from the BV class just below public class FloatType : Type { - public readonly int Mantissa; //Size of mantissa in bits + public readonly int Significand; //Size of Significand in bits public readonly int Exponent; //Size of exponent in bits - public FloatType(IToken token, int exponent, int mantissa) + public FloatType(IToken token, int significand, int exponent) : base(token) { Contract.Requires(token != null); + Significand = significand; Exponent = exponent; - Mantissa = mantissa; } - public FloatType(int exponent, int mantissa) + public FloatType(int significand, int exponent) : base(Token.NoToken) { + Significand = significand; Exponent = exponent; - Mantissa = mantissa; } //----------- Cloning ---------------------------------- @@ -1094,7 +1094,7 @@ namespace Microsoft.Boogie { public override string ToString() { Contract.Ensures(Contract.Result() != null); - return "float (" + Exponent + " " + Mantissa + ")"; + return "float (" + Exponent + " " + Significand + ")"; } //----------- Equality ---------------------------------- @@ -1105,7 +1105,7 @@ namespace Microsoft.Boogie { List/*!*/ thatBoundVariables) { FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType; - return thatFloatType != null && this.Mantissa == thatFloatType.Mantissa && this.Exponent == thatFloatType.Exponent; + return thatFloatType != null && this.Significand == thatFloatType.Significand && this.Exponent == thatFloatType.Exponent; } //----------- Unification of types ----------- @@ -1141,7 +1141,7 @@ namespace Microsoft.Boogie { [Pure] public override int GetHashCode(List boundVariables) { - return this.Mantissa.GetHashCode() + this.Exponent.GetHashCode(); + return this.Significand.GetHashCode() + this.Exponent.GetHashCode(); } //----------- Resolution ---------------------------------- @@ -1181,9 +1181,9 @@ namespace Microsoft.Boogie { return true; } } - public override int FloatMantissa { + public override int FloatSignificand { get { - return Mantissa; + return Significand; } } public override int FloatExponent { @@ -1481,7 +1481,7 @@ Contract.Requires(that != null); public override Type ResolveType(ResolutionContext rc) { //Contract.Requires(rc != null); Contract.Ensures(Contract.Result() != null); - // first case: the type name denotes a bitvector-type + // first case: the type name denotes a bitvector-type or float-type if (Name.StartsWith("bv") && Name.Length > 2) { bool is_bv = true; for (int i = 2; i < Name.Length; ++i) { @@ -1500,6 +1500,28 @@ Contract.Requires(that != null); } } + if (Name.StartsWith("float") && Name.Length > 5) + { + bool is_float = true; + int i = 5; + for (; is_float && Name[i] != 'e'; i++) + if (i >= Name.Length-1 || !char.IsDigit(Name[i])) //There must be an e + is_float = false; + int mid = i; + i++; + for (; i < Name.Length && is_float; i++) + if (!char.IsDigit(Name[i])) + is_float = false; + if (is_float) { + if (Arguments.Count > 0) { + rc.Error(this, + "float types must not be applied to arguments: {0}", + Name); + } + return new FloatType(tok, int.Parse(Name.Substring(5, mid-5)), int.Parse(Name.Substring(mid+1))); + } + } + // second case: the identifier is resolved to a type variable TypeVariable var = rc.LookUpTypeBinder(Name); if (var != null) { diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 99dd849d..7b2525f7 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -146,7 +146,7 @@ namespace Microsoft.Boogie.SMTLib else if (t.IsReal) return "Real"; else if (t.IsFloat) - return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; + return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatSignificand + ")"; else if (t.IsBv) { return "(_ BitVec " + t.BvBits + ")"; } else { diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index a3364ad8..1bcb6afc 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -1087,7 +1087,7 @@ namespace Microsoft.Boogie.VCExprAST { return Gen.Function(VCExpressionGenerator.AddROp, args); } else { //t is float - return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "+"), args); + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "+"), args); } case BinaryOperator.Opcode.Sub: if (t.IsInt) { @@ -1097,7 +1097,7 @@ namespace Microsoft.Boogie.VCExprAST { return Gen.Function(VCExpressionGenerator.SubROp, args); } else { //t is float - return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "-"), args); + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "-"), args); } case BinaryOperator.Opcode.Mul: if (t.IsInt) { @@ -1108,7 +1108,7 @@ namespace Microsoft.Boogie.VCExprAST { } else { //t is float - return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "*"), args); + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "*"), args); } case BinaryOperator.Opcode.Div: return Gen.Function(VCExpressionGenerator.DivIOp, args); @@ -1116,7 +1116,7 @@ namespace Microsoft.Boogie.VCExprAST { return Gen.Function(VCExpressionGenerator.ModOp, args); case BinaryOperator.Opcode.RealDiv: if (t.IsFloat) { - return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "/"), args); + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "/"), args); } VCExpr arg0 = cce.NonNull(args[0]); VCExpr arg1 = cce.NonNull(args[1]); @@ -1133,25 +1133,25 @@ namespace Microsoft.Boogie.VCExprAST { case BinaryOperator.Opcode.Iff: // we don't distinguish between equality and equivalence at this point if (t.IsFloat) - return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "=="), args); + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "=="), args); return Gen.Function(VCExpressionGenerator.EqOp, args); case BinaryOperator.Opcode.Neq: return Gen.Function(VCExpressionGenerator.NeqOp, args); case BinaryOperator.Opcode.Lt: if (t.IsFloat) - return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "<"), args); + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<"), args); return Gen.Function(VCExpressionGenerator.LtOp, args); case BinaryOperator.Opcode.Le: if (t.IsFloat) - return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "<="), args); + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<="), args); return Gen.Function(VCExpressionGenerator.LeOp, args); case BinaryOperator.Opcode.Ge: if (t.IsFloat) - return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, ">="), args); + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">="), args); return Gen.Function(VCExpressionGenerator.GeOp, args); case BinaryOperator.Opcode.Gt: if (t.IsFloat) - return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, ">"), args); + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">"), args); return Gen.Function(VCExpressionGenerator.GtOp, args); case BinaryOperator.Opcode.Imp: return Gen.Function(VCExpressionGenerator.ImpliesOp, args); -- cgit v1.2.3