diff options
45 files changed, 1956 insertions, 97 deletions
diff --git a/Binaries/Boogie.vshost.exe.manifest b/Binaries/Boogie.vshost.exe.manifest new file mode 100644 index 00000000..061c9ca9 --- /dev/null +++ b/Binaries/Boogie.vshost.exe.manifest @@ -0,0 +1,11 @@ +<?xml version="1.0" encoding="UTF-8" standalone="yes"?> +<assembly xmlns="urn:schemas-microsoft-com:asm.v1" manifestVersion="1.0"> + <assemblyIdentity version="1.0.0.0" name="MyApplication.app"/> + <trustInfo xmlns="urn:schemas-microsoft-com:asm.v2"> + <security> + <requestedPrivileges xmlns="urn:schemas-microsoft-com:asm.v3"> + <requestedExecutionLevel level="asInvoker" uiAccess="false"/> + </requestedPrivileges> + </security> + </trustInfo> +</assembly> diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 2fd37463..0dd78cbb 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -180,8 +180,7 @@ namespace Microsoft.Boogie.AbstractInterpretation } } return e; - } else { - Contract.Assert(V.TypedIdent.Type.IsReal); + } else if (V.TypedIdent.Type.IsReal){ Expr e = Expr.True; if (Lo != null && Hi != null && Lo == Hi) { // produce an equality @@ -199,6 +198,30 @@ namespace Microsoft.Boogie.AbstractInterpretation } } return e; + } else { + Contract.Assert(V.TypedIdent.Type.IsFloat); + Expr e = Expr.True; + if (Lo != null && Hi != null && Lo == Hi) + { + // produce an equality + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type))); + } + else + { + // produce a (possibly empty) conjunction of inequalities + if (Lo != null) + { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide)); + } + if (Hi != null) + { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type))); + } + } + return e; } } } @@ -208,6 +231,8 @@ namespace Microsoft.Boogie.AbstractInterpretation return null; } 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)); } else { Contract.Assume(ty.IsInt); return Expr.Literal(Basetypes.BigNum.FromBigInt(n)); @@ -669,6 +694,11 @@ namespace Microsoft.Boogie.AbstractInterpretation ((BigDec)node.Val).FloorCeiling(out floor, out ceiling); Lo = floor; Hi = ceiling; + } else if (node.Val is BigFloat) { + BigNum floor, ceiling; + ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling); + Lo = floor.ToBigInteger; + Hi = ceiling.ToBigInteger; } else if (node.Val is bool) { if ((bool)node.Val) { // true diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj index ffe22b9f..5b425bc5 100644 --- a/Source/Basetypes/Basetypes.csproj +++ b/Source/Basetypes/Basetypes.csproj @@ -163,6 +163,7 @@ </Compile> <Compile Include="BigDec.cs" /> <Compile Include="BigNum.cs" /> + <Compile Include="BigFloat.cs" /> <Compile Include="Rational.cs" /> <Compile Include="Set.cs" /> </ItemGroup> diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs new file mode 100644 index 00000000..3c4cc40a --- /dev/null +++ b/Source/Basetypes/BigFloat.cs @@ -0,0 +1,475 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Basetypes
+{
+ using BIM = System.Numerics.BigInteger;
+
+ /// <summary>
+ /// A representation of a 32-bit floating point value
+ /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit significand
+ /// </summary>
+ public struct BigFloat
+ {
+ //Please note that this code outline is copy-pasted from BigDec.cs
+
+ // the internal representation
+ [Rep]
+ internal readonly BigNum significand; //Note that the significand arrangement matches standard fp arrangement (most significant bit is farthest left)
+ [Rep]
+ internal readonly int significandSize;
+ [Rep]
+ internal readonly BigNum exponent; //The value of the exponent is always positive as per fp representation requirements
+ [Rep]
+ internal readonly int exponentSize; //The bit size of the exponent
+ [Rep]
+ internal readonly String value; //Only used with second syntax
+ [Rep]
+ internal readonly bool isNeg;
+
+ public BigNum Significand {
+ get {
+ return significand;
+ }
+ }
+
+ public BigNum Exponent {
+ get {
+ return exponent;
+ }
+ }
+
+ public int SignificandSize {
+ get {
+ return significandSize;
+ }
+ }
+
+ public int ExponentSize {
+ get {
+ return exponentSize;
+ }
+ }
+
+ public bool IsNegative {
+ get {
+ return this.isNeg;
+ }
+ }
+
+ public String Value {
+ get {
+ return value;
+ }
+ }
+
+ public static BigFloat ZERO(int exponentSize, int significandSize) { return new BigFloat(false, BigNum.ZERO, BigNum.ZERO, exponentSize, significandSize); } //Does not include negative zero
+
+ private static readonly BigNum two = new BigNum(2);
+ private static readonly BigNum one = new BigNum(1);
+ private static BigNum two_n(int n) {
+ BigNum toReturn = one;
+ for (int i = 0; i < n; i++)
+ toReturn = toReturn * two;
+ return toReturn;
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Constructors
+
+ //Please note that these constructors will be called throughout boogie
+ //For a complete summary of where this class has been added, simply view constructor references
+
+ [Pure]
+ public static BigFloat FromInt(int v) {
+ return new BigFloat(v.ToString(), 8, 24);
+ }
+
+ public static BigFloat FromInt(int v, int exponentSize, int significandSize)
+ {
+ return new BigFloat(v.ToString(), exponentSize, significandSize);
+ }
+
+ public static BigFloat FromBigInt(BIM v) {
+ return new BigFloat(v.ToString(), 8, 24);
+ }
+
+ public static BigFloat FromBigInt(BIM v, int exponentSize, int significandSize)
+ {
+ return new BigFloat(v.ToString(), exponentSize, significandSize);
+ }
+
+ public static BigFloat FromBigDec(BigDec v)
+ {
+ return new BigFloat(v.ToDecimalString(), 8, 24);
+ }
+
+ public static BigFloat FromBigDec(BigDec v, int exponentSize, int significandSize)
+ {
+ return new BigFloat(v.ToDecimalString(), exponentSize, significandSize);
+ }
+
+ [Pure]
+ public static BigFloat FromString(String v, int exp, int sig) { //String must be
+ return new BigFloat(v, exp, sig);
+ }
+
+ public BigFloat(bool sign, BigNum exponent, BigNum significand, int exponentSize, int significandSize) {
+ this.exponentSize = exponentSize;
+ this.exponent = exponent;
+ this.significand = significand;
+ this.significandSize = significandSize+1;
+ this.isNeg = sign;
+ this.value = "";
+ }
+
+ public BigFloat(String value, int exponentSize, int significandSize) {
+ this.exponentSize = exponentSize;
+ this.significandSize = significandSize;
+ this.exponent = BigNum.ZERO;
+ this.significand = BigNum.ZERO;
+ this.value = value;
+ this.isNeg = value[0] == '-';
+ }
+
+ private BigNum maxsignificand()
+ {
+ BigNum result = one;
+ for (int i = 0; i < significandSize; i++)
+ result = result * two;
+ return result - one;
+ }
+ private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }
+
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Basic object operations
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is BigFloat))
+ return false;
+
+ return (this == (BigFloat)obj);
+ }
+
+ [Pure]
+ public override int GetHashCode() {
+ return significand.GetHashCode() * 13 + Exponent.GetHashCode();
+ }
+
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Conversion operations
+
+ /// <summary>
+ /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!
+ /// Converts the given decimal value (provided as a string) to the nearest floating point approximation
+ /// the returned fp assumes the given significand and exponent size
+ /// </summary>
+ /// <param name="value"></param>
+ /// <param name="significandSize"></param>
+ /// <param name="exponentSize"></param>
+ /// <returns></returns>
+ public static BigFloat Round(String value, int exponentSize, int significandSize)
+ {
+ int i = value.IndexOf('.');
+ if (i == -1)
+ return Round(BigNum.FromString(value), BigNum.ZERO, exponentSize, significandSize);
+ return Round(i == 0 ? BigNum.ZERO : BigNum.FromString(value.Substring(0, i)), BigNum.FromString(value.Substring(i + 1, value.Length - i - 1)), exponentSize, significandSize);
+ }
+
+ /// <summary>
+ /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!!
+ /// Converts value.dec_value to a the closest float approximation with the given significandSize, exponentSize
+ /// Returns the result of this calculation
+ /// </summary>
+ /// <param name="value"></param>
+ /// <param name="power"></param>
+ /// <param name="significandSize"></param>
+ /// <param name="exponentSize"></param>
+ /// <returns></returns>
+ public static BigFloat Round(BigNum value, BigNum dec_value, int exponentSize, int significandSize)
+ {
+ int exp = 0;
+ BigNum one = new BigNum(1);
+ BigNum ten = new BigNum(10);
+ BigNum dec_max = new BigNum(0); //represents the order of magnitude of dec_value for carrying during calculations
+
+ //First, determine the exponent
+ while (value > one) { //Divide by two, increment exponent by 1
+ if (!(value % two).IsZero) { //Add "1.0" to the decimal
+ dec_max = new BigNum(10);
+ while (dec_max < dec_value)
+ dec_max = dec_max * ten;
+ dec_value = dec_value + dec_max;
+ }
+ value = value / two;
+ if (!(dec_value % ten).IsZero)
+ dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division
+ dec_value = dec_value / two;
+ exp++;
+ }
+ if (value.IsZero && !dec_value.IsZero) {
+ dec_max = new BigNum(10);
+ while (dec_max < dec_value)
+ dec_max = dec_max * ten;
+ while (value.IsZero) {//Multiply by two, decrement exponent by 1
+ dec_value = dec_value * two;
+ if (dec_value >= dec_max) {
+ dec_value = dec_value - dec_max;
+ value = value + one;
+ }
+ exp--;
+ }
+ }
+
+ //Second, calculate the significand
+ value = new BigNum(0); //remove implicit bit
+ dec_max = new BigNum(10);
+ while (dec_max < dec_value)
+ dec_max = dec_max * ten;
+ for (int i = significandSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the significand is fully calculated
+ dec_value = dec_value * two;
+ if (dec_value >= dec_max) {
+ dec_value = dec_value - dec_max;
+ value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation
+ }
+ }
+
+ return new BigFloat(false, BigNum.ZERO, BigNum.FromString(value.ToString()), exponentSize, significandSize); //Sign not actually checked...
+ }
+
+ // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
+ /// <summary>
+ /// NOTE: THIS PROBABLY WON'T GIVE USEFUL OUTPUT!!!
+ /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
+ /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
+ /// </summary>
+ /// <param name="floor">The Floor (rounded towards negative infinity)</param>
+ /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>
+ public void FloorCeiling(out BigNum floor, out BigNum ceiling) {
+ //TODO: fix for fp functionality
+ BigNum n = Significand;
+ BigNum e = Exponent;
+ if (n.IsZero) {
+ floor = ceiling = n;
+ } else if (BigNum.ZERO <= e) {
+ // it's an integer
+ for (; BigNum.ZERO < e; e = e - one)
+ {
+ n = n * two;
+ }
+ floor = ceiling = n;
+ } else {
+ // it's a non-zero integer, so the ceiling is one more than the floor
+ for (; BigNum.ZERO < e && !n.IsZero; e = e + one)
+ {
+ n = n / two; // Division rounds towards negative infinity
+ }
+
+ if (!IsNegative) {
+ floor = n;
+ ceiling = n + one;
+ } else {
+ ceiling = n;
+ floor = n - one;
+ }
+ }
+ Debug.Assert(floor <= ceiling, "Invariant was not maintained");
+ }
+
+ [Pure]
+ public String ToDecimalString(int maxDigits) {
+ //TODO: fix for fp functionality
+ {
+ throw new NotImplementedException();
+ }
+ }
+
+ public String ToBVString(){
+ if (this.IsSpecialType) {
+ return "_ " + this.value + " " + this.exponentSize + " " + this.significandSize;
+ }
+ else if (this.Value == "") {
+ return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")";
+ }
+ else {
+ return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")";
+ }
+ }
+
+ [Pure]
+ public string ToDecimalString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return value=="" ? String.Format("{0}x2^{1}", significand.ToString(), Exponent.ToString()) : value;
+ }
+
+ [Pure]
+ public static string Zeros(int n) {
+ //TODO: fix for fp functionality
+ Contract.Requires(0 <= n);
+ if (n <= 10) {
+ var tenZeros = "0000000000";
+ return tenZeros.Substring(0, n);
+ } else {
+ var d = n / 2;
+ var s = Zeros(d);
+ if (n % 2 == 0) {
+ return s + s;
+ } else {
+ return s + s + "0";
+ }
+ }
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Basic arithmetic operations
+
+ [Pure]
+ public BigFloat Abs {
+ get {
+ return new BigFloat(true, Exponent, Significand, ExponentSize, SignificandSize);
+ }
+ }
+
+ [Pure]
+ public BigFloat Negate {
+ get {
+ if (value != "")
+ return value[0] == '-' ? new BigFloat(value.Remove(0, 1), ExponentSize, significandSize) : new BigFloat("-" + value, ExponentSize, significandSize);
+ return new BigFloat(!isNeg, Exponent, Significand, ExponentSize, SignificandSize);
+ }
+ }
+
+ [Pure]
+ public static BigFloat operator -(BigFloat x) {
+ return x.Negate;
+ }
+
+ [Pure]
+ public static BigFloat operator +(BigFloat x, BigFloat y) {
+ //TODO: Modify for correct fp functionality
+ Contract.Requires(x.ExponentSize == y.ExponentSize);
+ Contract.Requires(x.significandSize == y.significandSize);
+ BigNum m1 = x.significand;
+ BigNum e1 = x.Exponent;
+ BigNum m2 = y.significand;
+ BigNum e2 = y.Exponent;
+ m1 = m1 + two_n(x.significandSize + 1); //Add implicit bit
+ m2 = m2 + two_n(y.significandSize + 1);
+ if (e2 > e1) {
+ m1 = y.significand;
+ e1 = y.Exponent;
+ m2 = x.significand;
+ e2 = x.Exponent;
+ }
+
+ while (e2 < e1) {
+ m2 = m2 / two;
+ e2 = e2 + one;
+ }
+
+ return new BigFloat(false, e1, m1 + m2, x.significandSize, x.ExponentSize);
+ }
+
+ [Pure]
+ public static BigFloat operator -(BigFloat x, BigFloat y) {
+ return x + y.Negate;
+ }
+
+ [Pure]
+ public static BigFloat operator *(BigFloat x, BigFloat y) {
+ Contract.Requires(x.ExponentSize == y.ExponentSize);
+ Contract.Requires(x.significandSize == y.significandSize);
+ return new BigFloat(x.isNeg ^ y.isNeg, x.Exponent + y.Exponent, x.significand * y.significand, x.significandSize, x.ExponentSize);
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Some basic comparison operations
+
+ public bool IsSpecialType {
+ get {
+ if (value == "")
+ return false;
+ return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero"));
+ }
+ }
+
+ public bool IsPositive {
+ get {
+ return !IsNegative;
+ }
+ }
+
+ public bool IsZero {
+ get {
+ return significand.Equals(BigNum.ZERO) && Exponent == BigNum.ZERO;
+ }
+ }
+
+ [Pure]
+ public int CompareTo(BigFloat that) {
+ if (this.exponent > that.exponent)
+ return 1;
+ if (this.exponent < that.exponent)
+ return -1;
+ if (this.significand == that.significand)
+ return 0;
+ return this.significand > that.significand ? 1 : -1;
+ }
+
+ [Pure]
+ public static bool operator ==(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) == 0;
+ }
+
+ [Pure]
+ public static bool operator !=(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) != 0;
+ }
+
+ [Pure]
+ public static bool operator <(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) < 0;
+ }
+
+ [Pure]
+ public static bool operator >(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) > 0;
+ }
+
+ [Pure]
+ public static bool operator <=(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) <= 0;
+ }
+
+ [Pure]
+ public static bool operator >=(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) >= 0;
+ }
+ }
+}
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 2953f15e..96de5c0b 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -244,6 +244,11 @@ namespace Microsoft.Boogie { return false; } } + public virtual bool IsFloat { + get { + return false; + } + } public virtual bool IsBool { get { return false; @@ -320,6 +325,29 @@ namespace Microsoft.Boogie { } } + public virtual bool isFloat { + get { + return false; + } + } + public virtual int FloatExponent + { + get + { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.FloatExponent should never be called + } + } + public virtual int FloatMantissa { + get { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.FloatMantissa should never be called + } + } public virtual bool IsBv { get { return false; @@ -358,6 +386,14 @@ namespace Microsoft.Boogie { } } + static public FloatType GetFloatType(int exp, int man) { + Contract.Requires(0 <= exp); + Contract.Requires(0 <= man); + Contract.Ensures(Contract.Result<FloatType>() != null); + + return new FloatType(exp, man); + } + //------------ Match formal argument types on actual argument types //------------ and return the resulting substitution of type variables @@ -1008,6 +1044,165 @@ 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 Exponent; //Size of exponent in bits + + public FloatType(IToken token, int exponent, int mantissa) + : base(token) { + Contract.Requires(token != null); + Exponent = exponent; + Mantissa = mantissa; + } + + public FloatType(int exponent, int mantissa) + : base(Token.NoToken) { + Exponent = exponent; + Mantissa = mantissa; + } + + //----------- Cloning ---------------------------------- + // We implement our own clone-method, because bound type variables + // have to be created in the right way. It is /not/ ok to just clone + // everything recursively. + + public override Type Clone(IDictionary<TypeVariable/*!*/, TypeVariable/*!*/>/*!*/ varMap) + { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result<Type>() != null); + // FloatTypes are immutable anyway, we do not clone + return this; + } + + public override Type CloneUnresolved() + { + Contract.Ensures(Contract.Result<Type>() != null); + return this; + } + + //----------- Linearisation ---------------------------------- + + public override void Emit(TokenTextWriter stream, int contextBindingStrength) + { + //Contract.Requires(stream != null); + // no parentheses are necessary for bitvector-types + stream.SetToken(this); + stream.Write("{0}", this); + } + + public override string ToString() + { + Contract.Ensures(Contract.Result<string>() != null); + return "float (" + Exponent + " " + Mantissa + ")"; + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type/*!*/ that, + List<TypeVariable>/*!*/ thisBoundVariables, + List<TypeVariable>/*!*/ thatBoundVariables) + { + FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType; + return thatFloatType != null && this.Mantissa == thatFloatType.Mantissa && this.Exponent == thatFloatType.Exponent; + } + + //----------- Unification of types ----------- + + public override bool Unify(Type/*!*/ that, + List<TypeVariable>/*!*/ unifiableVariables, + // an idempotent substitution that describes the + // unification result up to a certain point + IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) + { + //Contract.Requires(that != null); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(cce.NonNullElements(unifier)); + that = that.Expanded; + if (that is TypeProxy || that is TypeVariable) { + return that.Unify(this, unifiableVariables, unifier); + } + else { + return this.Equals(that); + } + } + + //----------- Substitution of free variables with types not containing bound variables ----------------- + + public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) + { + Contract.Ensures(Contract.Result<Type>() != null); + return this; + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List<TypeVariable> boundVariables) + { + return this.Mantissa.GetHashCode() + this.Exponent.GetHashCode(); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) + { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result<Type>() != null); + // nothing to resolve + return this; + } + + // determine the free variables in a type, in the order in which the variables occur + public override List<TypeVariable>/*!*/ FreeVariables + { + get + { + Contract.Ensures(Contract.Result<List<TypeVariable>>() != null); + + return new List<TypeVariable>(); // bitvector-type are closed + } + } + + public override List<TypeProxy/*!*/>/*!*/ FreeProxies + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeProxy>>())); + return new List<TypeProxy/*!*/>(); + } + } + + //----------- Getters/Issers ---------------------------------- + + public override bool IsFloat { + get { + return true; + } + } + public override int FloatMantissa { + get { + return Mantissa; + } + } + public override int FloatExponent { + get { + return Exponent; + } + } + + public override Absy StdDispatch(StandardVisitor visitor) + { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != null); + return visitor.VisitFloatType(this); + } + + } + + //===================================================================== + public class BvType : Type { public readonly int Bits; @@ -1899,6 +2094,12 @@ Contract.Requires(that != null); return p != null && p.IsReal; } } + public override bool IsFloat { + get { + Type p = ProxyFor; + return p != null && p.IsFloat; + } + } public override bool IsBool { get { Type p = ProxyFor; @@ -2747,11 +2948,20 @@ Contract.Requires(that != null); return ExpandedType.IsInt; } } - public override bool IsReal { - get { + public override bool IsReal + { + get + { return ExpandedType.IsReal; } } + public override bool IsFloat + { + get + { + return ExpandedType.IsFloat; + } + } public override bool IsBool { get { return ExpandedType.IsBool; diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index af525fab..7c4cb7ae 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -186,7 +186,7 @@ </ItemGroup> <ItemGroup> <ProjectReference Include="..\Basetypes\Basetypes.csproj"> - <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project> + <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project> <Name>Basetypes</Name> </ProjectReference> <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj"> diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 793bb96e..1f8d17d6 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -24,7 +24,8 @@ public class Parser { public const int _string = 4; public const int _decimal = 5; public const int _float = 6; - public const int maxT = 96; + public const int _fp = 97; + public const int maxT = 98; const bool T = true; const bool x = false; @@ -365,7 +366,7 @@ private class BvBounds : Expr { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); - } else SynErr(97); + } else SynErr(99); if (la.kind == 27) { Get(); Expression(out tmp); @@ -373,7 +374,7 @@ private class BvBounds : Expr { Expect(28); } else if (la.kind == 8) { Get(); - } else SynErr(98); + } else SynErr(100); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); @@ -664,8 +665,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 == 98) { + Get(); + ty = FType(); + } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Bool); } else if (la.kind == 9) { @@ -675,6 +679,39 @@ private class BvBounds : Expr { } else SynErr(101); } + FloatType FType() { + if (t.val.Length > 5) { + switch (Int32.Parse(t.val.Substring(5))) { + case 16: + return new FloatType(t, 5, 11); + case 32: + return new FloatType(t, 8, 24); + case 64: + return new FloatType(t, 11, 53); + case 128: + return new FloatType(t, 15, 113); + default: + SynErr(3); + return new FloatType(t, 0, 0); + } + } + else { + try { + Expect(19); //< + Expect(3); //int + int exp = Int32.Parse(t.val); + Expect(12); //, + Expect(3); //int + int man = Int32.Parse(t.val); + Expect(20); //> + return new FloatType(t, exp, man); + } + catch (Exception) { + return new FloatType(t, 0, 0); + } + } + } + void Ident(out IToken/*!*/ x) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); Expect(1); @@ -1619,7 +1656,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Get(); } else if (la.kind == 81) { Get(); - } else SynErr(121); + } else SynErr(123); } void CoercionExpression(out Expr/*!*/ e) { @@ -1643,7 +1680,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(122); + } else SynErr(124); } } @@ -1714,7 +1751,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } void AtomExpression(out Expr/*!*/ e) { - Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; + Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; BigFloat fp; List<Expr>/*!*/ es; List<Variable>/*!*/ ds; Trigger trig; List<TypeVariable>/*!*/ typeParams; IdentifierExpr/*!*/ id; @@ -1739,11 +1776,16 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new LiteralExpr(t, bn); break; } - case 5: case 6: { + case 5: case 6: { Dec(out bd); e = new LiteralExpr(t, bd); break; } + case 97: { + Float(out fp); + e = new LiteralExpr(t, fp); + break; + } case 2: { BvLit(out bn, out n); e = new LiteralExpr(t, bn, n); @@ -1759,7 +1801,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new NAryExpr(x, new FunctionCall(id), es); } else if (la.kind == 10) { e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); - } else SynErr(123); + } else SynErr(125); Expect(10); } break; @@ -1791,6 +1833,15 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List<Expr>{ e }); break; } + case 98: { + Get(); + x = t; + Expect(19); + Expression(out e); + Expect(20); + e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List<Expr> { e }); + break; + } case 9: { Get(); if (StartOf(9)) { @@ -1818,7 +1869,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { SemErr("triggers not allowed in lambda expressions"); if (typeParams.Count + ds.Count > 0) e = new LambdaExpr(x, typeParams, ds, kv, e); - } else SynErr(124); + } else SynErr(126); Expect(10); break; } @@ -1831,7 +1882,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new CodeExpr(locals, blocks); break; } - default: SynErr(125); break; + default: SynErr(127); break; } } @@ -1843,7 +1894,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 6) { Get(); s = t.val; - } else SynErr(126); + } else SynErr(128); try { n = BigDec.FromString(s); } catch (FormatException) { @@ -1853,6 +1904,77 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } + /// <summary> + /// Creates a floating point from the current token value + /// </summary> + /// <param name="n"></param> + void Float(out BigFloat n) + { + try + { + if (la.kind == 97) { + bool negative = false; + int exp, sig, size; + BigNum exp_val, sig_val, value; + //Expected format = float(sign exp_val sig_val) || float<exp sig>(value) + Get(); //Skip the float token + if (la.val == "(") { + Get(); + if (la.val == "false") + negative = false; + else if (la.val == "true") + negative = true; + else + throw new FormatException(); + Get(); + Expect(12); //, + BvLit(out exp_val, out exp); + Expect(12); + BvLit(out sig_val, out sig); + n = new BigFloat(negative, exp_val, sig_val, exp, sig); + Expect(10); //) + } + else if (la.val == "<") { + Get(); + Expect(3); + exp = Int32.Parse(t.val); + Expect(12); + Expect(3); + sig = Int32.Parse(t.val); + Expect(20); //> + Expect(9); //( + if (la.kind == 1) { //NaN + Get(); + n = new BigFloat(t.val, exp, sig); + } + else if (la.kind == 74 || la.kind == 75) { //+ or - + Get(); + String s = t.val; + Get(); + n = new BigFloat(s + t.val, exp, sig); + } + else { + BvLit(out value, out size); + n = new BigFloat(value.ToString(), exp, sig); + } + Expect(10); //) + } + else { + throw new FormatException(); + } + } + else { + n = BigFloat.ZERO(8, 24); + SynErr(137); + } + } + catch (FormatException) + { + this.SemErr("incorrectly formatted floating point"); + n = BigFloat.ZERO(8, 24); + } + } + void BvLit(out BigNum n, out int m) { Expect(2); int pos = t.val.IndexOf("bv"); @@ -1874,7 +1996,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Get(); } else if (la.kind == 89) { Get(); - } else SynErr(127); + } else SynErr(129); } void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds, @@ -1892,7 +2014,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } } else if (la.kind == 1 || la.kind == 27) { BoundVars(q, out ds); - } else SynErr(128); + } else SynErr(130); QSep(); while (la.kind == 27) { AttributeOrTrigger(ref kv, ref trig); @@ -1905,7 +2027,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Get(); } else if (la.kind == 91) { Get(); - } else SynErr(129); + } else SynErr(131); } void Lambda() { @@ -1913,7 +2035,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Get(); } else if (la.kind == 93) { Get(); - } else SynErr(130); + } else SynErr(132); } void IfThenElseExpression(out Expr/*!*/ e) { @@ -1983,7 +2105,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Get(); Expression(out e); b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(131); + } else SynErr(133); Expect(8); } @@ -2040,7 +2162,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(132); + } else SynErr(134); Expect(28); } @@ -2055,7 +2177,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } else if (StartOf(9)) { Expression(out e); o = e; - } else SynErr(133); + } else SynErr(135); } void QSep() { @@ -2063,7 +2185,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Get(); } else if (la.kind == 95) { Get(); - } else SynErr(134); + } else SynErr(136); } @@ -2078,24 +2200,24 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Expect(0); } - static readonly bool[,]/*!*/ set = { - {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x} + static readonly bool[,]/*!*/ set = { //grid is 17 x 100 + {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x}, + {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x}, + {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x} }; } // end Parser @@ -2117,6 +2239,12 @@ public class Errors { count++; } + /// <summary> + /// Returns a string corresponding to the syntax error of the given type + /// Note that many of these errors (0-98) correspond to token types (e.g. the la token) + /// </summary> + /// <param name="n"></param> + /// <returns></returns> string GetSyntaxErrorString(int n) { string s; switch (n) { @@ -2217,44 +2345,47 @@ public class Errors { case 94: s = "\"::\" expected"; break; case 95: s = "\"\\u2022\" expected"; break; case 96: s = "??? expected"; break; - case 97: s = "invalid Function"; break; - case 98: s = "invalid Function"; break; - case 99: s = "invalid Procedure"; break; - case 100: s = "invalid Type"; break; - case 101: s = "invalid TypeAtom"; break; - case 102: s = "invalid TypeArgs"; break; - case 103: s = "invalid Spec"; break; - case 104: s = "invalid SpecPrePost"; break; - case 105: s = "invalid LabelOrCmd"; break; - case 106: s = "invalid StructuredCmd"; break; - case 107: s = "invalid TransferCmd"; break; - case 108: s = "invalid IfCmd"; break; - case 109: s = "invalid Guard"; break; - case 110: s = "invalid LabelOrAssign"; break; - case 111: s = "invalid CallParams"; break; - case 112: s = "invalid EquivOp"; break; - case 113: s = "invalid ImpliesOp"; break; - case 114: s = "invalid ExpliesOp"; break; - case 115: s = "invalid AndOp"; break; - case 116: s = "invalid OrOp"; break; - case 117: s = "invalid RelOp"; break; - case 118: s = "invalid AddOp"; break; - case 119: s = "invalid MulOp"; break; - case 120: s = "invalid UnaryExpression"; break; - case 121: s = "invalid NegOp"; break; - case 122: s = "invalid CoercionExpression"; break; - case 123: s = "invalid AtomExpression"; break; - case 124: s = "invalid AtomExpression"; break; + case 97: s = "fp expected"; break; + case 98: s = "\"float\" expected"; break; + case 99: s = "invalid Function"; break; + case 100: s = "invalid Function"; break; + case 101: s = "invalid Procedure"; break; + case 102: s = "invalid Type"; break; + case 103: s = "invalid TypeAtom"; break; + case 104: s = "invalid TypeArgs"; break; + case 105: s = "invalid Spec"; break; + case 106: s = "invalid SpecPrePost"; break; + case 107: s = "invalid LabelOrCmd"; break; + case 108: s = "invalid StructuredCmd"; break; + case 109: s = "invalid TransferCmd"; break; + case 110: s = "invalid IfCmd"; break; + case 111: s = "invalid Guard"; break; + case 112: s = "invalid LabelOrAssign"; break; + case 113: s = "invalid CallParams"; break; + case 114: s = "invalid EquivOp"; break; + case 115: s = "invalid ImpliesOp"; break; + case 116: s = "invalid ExpliesOp"; break; + case 117: s = "invalid AndOp"; break; + case 118: s = "invalid OrOp"; break; + case 119: s = "invalid RelOp"; break; + case 120: s = "invalid AddOp"; break; + case 121: s = "invalid MulOp"; break; + case 122: s = "invalid UnaryExpression"; break; + case 123: s = "invalid NegOp"; break; + case 124: s = "invalid CoercionExpression"; break; case 125: s = "invalid AtomExpression"; break; - case 126: s = "invalid Dec"; break; - case 127: s = "invalid Forall"; break; - case 128: s = "invalid QuantifierBody"; break; - case 129: s = "invalid Exists"; break; - case 130: s = "invalid Lambda"; break; - case 131: s = "invalid SpecBlock"; break; - case 132: s = "invalid AttributeOrTrigger"; break; - case 133: s = "invalid AttributeParameter"; break; - case 134: s = "invalid QSep"; break; + case 126: s = "invalid AtomExpression"; break; + case 127: s = "invalid AtomExpression"; break; + case 128: s = "invalid Dec"; break; + case 129: s = "invalid Forall"; break; + case 130: s = "invalid QuantifierBody"; break; + case 131: s = "invalid Exists"; break; + case 132: s = "invalid Lambda"; break; + case 133: s = "invalid SpecBlock"; break; + case 134: s = "invalid AttributeOrTrigger"; break; + case 135: s = "invalid AttributeParameter"; break; + case 136: s = "invalid QSep"; break; + case 137: s = "invalid Float"; break; default: s = "error " + n; break; } diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index e068fc4b..69023555 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -508,6 +508,8 @@ public class Scanner { case "int": t.kind = 14; break; case "real": t.kind = 15; break; case "bool": t.kind = 16; break; + case "fp": t.kind = 97; break; + case "float": case "float16": case "float32": case "float64": case "float128": t.kind = 98; break; case "const": t.kind = 21; break; case "unique": t.kind = 22; break; case "extends": t.kind = 23; break; diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index c845a589..c3d8a672 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -103,6 +103,12 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Type>() != null); return this.VisitType(node); } + public virtual Type VisitFloatType(FloatType node) + { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result<Type>() != null); + return this.VisitType(node); + } public virtual Expr VisitBvConcatExpr(BvConcatExpr node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result<Expr>() != null); diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 06aa5bbe..99dd849d 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -121,7 +121,7 @@ namespace Microsoft.Boogie.SMTLib } sb.Append(']'); TypeToStringHelper(m.Result, sb); - } else if (t.IsBool || t.IsInt || t.IsReal || t.IsBv) { + } else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv) { sb.Append(TypeToString(t)); } else { System.IO.StringWriter buffer = new System.IO.StringWriter(); @@ -145,6 +145,8 @@ namespace Microsoft.Boogie.SMTLib return "Int"; else if (t.IsReal) return "Real"; + else if (t.IsFloat) + return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; else if (t.IsBv) { return "(_ BitVec " + t.BvBits + ")"; } else { @@ -204,6 +206,11 @@ namespace Microsoft.Boogie.SMTLib else wr.Write(lit.ToDecimalString()); } + else if (node is VCExprFloatLit) + { + BigFloat lit = ((VCExprFloatLit)node).Val; + wr.Write("(" + lit.ToBVString() + ")"); + } else { Contract.Assert(false); throw new cce.UnreachableException(); @@ -630,6 +637,78 @@ namespace Microsoft.Boogie.SMTLib return true; } + public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.add RNE", node, options); + return true; + } + + public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.sub RNE", node, options); + return true; + } + + public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.mul RNE", node, options); + return true; + } + + public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.div RNE", node, options); + return true; + } + + public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.rem RNE", node, options); + return true; + } + + public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.min", node, options); + return true; + } + + public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.max", node, options); + return true; + } + + public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.leq", node, options); + return true; + } + + public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.lt", node, options); + return true; + } + + public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.geq", node, options); + return true; + } + + public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.gt", node, options); + return true; + } + + public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.eq", node, options); + return true; + } + static char[] hex = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f' }; public bool VisitBvOp(VCExprNAry node, LineariserOptions options) { diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj index 61215d48..24fd8c45 100644 --- a/Source/UnitTests/CoreTests/CoreTests.csproj +++ b/Source/UnitTests/CoreTests/CoreTests.csproj @@ -54,7 +54,7 @@ </ItemGroup> <ItemGroup> <ProjectReference Include="..\..\Basetypes\Basetypes.csproj"> - <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project> + <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project> <Name>Basetypes</Name> </ProjectReference> <ProjectReference Include="..\..\Core\Core.csproj"> diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs index b83983b6..86018d9b 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.BigFloat.FromInt(0), /*immutable=*/true); + Assert.AreEqual(literal5.ComputeHashCode(), literal5.GetHashCode()); } [Test()] diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 0c817756..a3364ad8 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -334,7 +334,10 @@ namespace Microsoft.Boogie.VCExprAST { return Gen.Integer(node.asBigNum); } else if (node.Val is BigDec) { return Gen.Real(node.asBigDec); - } else if (node.Val is BvConst) { + } else if (node.Val is BigFloat) { + return Gen.Float(node.asBigFloat); + } + else if (node.Val is BvConst) { return Gen.Bitvector((BvConst)node.Val); } else { System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString()); @@ -1002,9 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST { if (cce.NonNull(e.Type).IsInt) { return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e); } - else { + else {// if (cce.NonNull(e.Type).IsReal) { return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e); } + //else {//is float + //return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e); + //} } else { return Gen.Not(this.args); @@ -1070,34 +1076,48 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result<VCExpr>() != null); Contract.Assert(args.Count == 2); + Type t = cce.NonNull(cce.NonNull(args[0]).Type); switch (app.Op) { case BinaryOperator.Opcode.Add: - if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + if (t.IsInt) { return Gen.Function(VCExpressionGenerator.AddIOp, args); } - else { + else if (t.IsReal) { return Gen.Function(VCExpressionGenerator.AddROp, args); } + else { //t is float + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "+"), args); + } case BinaryOperator.Opcode.Sub: - if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + if (t.IsInt) { return Gen.Function(VCExpressionGenerator.SubIOp, args); } - else { + else if (t.IsReal) { return Gen.Function(VCExpressionGenerator.SubROp, args); } + else { //t is float + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "-"), args); + } case BinaryOperator.Opcode.Mul: - if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) { + if (t.IsInt) { return Gen.Function(VCExpressionGenerator.MulIOp, args); } - else { + else if (t.IsReal) { return Gen.Function(VCExpressionGenerator.MulROp, args); } + else + { //t is float + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "*"), args); + } case BinaryOperator.Opcode.Div: return Gen.Function(VCExpressionGenerator.DivIOp, args); case BinaryOperator.Opcode.Mod: return Gen.Function(VCExpressionGenerator.ModOp, args); case BinaryOperator.Opcode.RealDiv: + if (t.IsFloat) { + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "/"), args); + } VCExpr arg0 = cce.NonNull(args[0]); VCExpr arg1 = cce.NonNull(args[1]); if (cce.NonNull(arg0.Type).IsInt) { @@ -1112,16 +1132,26 @@ namespace Microsoft.Boogie.VCExprAST { case BinaryOperator.Opcode.Eq: 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(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(VCExpressionGenerator.LtOp, args); case BinaryOperator.Opcode.Le: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "<="), 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(VCExpressionGenerator.GeOp, args); case BinaryOperator.Opcode.Gt: + if (t.IsFloat) + return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, ">"), args); return Gen.Function(VCExpressionGenerator.GtOp, args); case BinaryOperator.Opcode.Imp: return Gen.Function(VCExpressionGenerator.ImpliesOp, args); diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index b554c331..1a4374f8 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -380,9 +380,22 @@ namespace Microsoft.Boogie.VCExprAST { internal const string realSubName = "realSub"; internal const string realMulName = "realMul"; internal const string realDivName = "realDiv"; + internal const string floatAddName = "floatAdd"; + internal const string floatSubName = "floatSub"; + internal const string floatMulName = "floatMul"; + internal const string floatDivName = "floatDiv"; + internal const string floatRemName = "floatRem"; + internal const string floatMinName = "floatMin"; + internal const string floatMaxName = "floatMax"; + internal const string floatLeqName = "floatLeq"; + internal const string floatLtName = "floatLt"; + internal const string floatGeqName = "floatGeq"; + internal const string floatGtName = "floatGt"; + internal const string floatEqName = "floatEq"; internal const string realPowName = "realPow"; internal const string toIntName = "toIntCoercion"; internal const string toRealName = "toRealCoercion"; + internal const string toFloatName = "toFloatCoercion"; internal void AssertAsTerm(string x, LineariserOptions options) { Contract.Requires(options != null); @@ -883,7 +896,104 @@ namespace Microsoft.Boogie.VCExprAST { return true; } - public bool VisitBvOp(VCExprNAry node, LineariserOptions options) { + public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatAddName, node, options); + return true; + } + + public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatSubName, node, options); + return true; + } + + public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatMulName, node, options); + return true; + } + + public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatDivName, node, options); + return true; + } + + public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatRemName, node, options); + return true; + } + + public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatMinName, node, options); + return true; + } + + public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatMaxName, node, options); + return true; + } + + public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatLeqName, node, options); + return true; + } + + public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatLtName, node, options); + return true; + } + + public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatGeqName, node, options); + return true; + } + + public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatGtName, node, options); + return true; + } + + public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteTermApplication(floatEqName, node, options); + return true; + } + + public bool VisitBvOp(VCExprNAry node, LineariserOptions options) + { //Contract.Requires(options != null); //Contract.Requires(node != null); WriteTermApplication("$make_bv" + node.Type.BvBits, node, options); @@ -955,9 +1065,12 @@ namespace Microsoft.Boogie.VCExprAST { if (node.Type.IsInt) { WriteTermApplication(intSubName, node, options); } - else { + else if (node.Type.IsReal) { WriteTermApplication(realSubName, node, options); } + else { + WriteTermApplication(floatSubName, node, options); + } return true; } @@ -967,9 +1080,12 @@ namespace Microsoft.Boogie.VCExprAST { if (node.Type.IsInt) { WriteTermApplication(intMulName, node, options); } - else { + else if (node.Type.IsReal) { WriteTermApplication(realMulName, node, options); } + else { + WriteTermApplication(floatMulName, node, options); + } return true; } @@ -1057,6 +1173,14 @@ namespace Microsoft.Boogie.VCExprAST { return true; } + public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + WriteApplication(toFloatName, node, options); + return true; + } + public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) { //Contract.Requires(options != null); //Contract.Requires(node != null); diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 76340f97..c2d99d77 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -1424,6 +1424,13 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<VCExpr>() != null); return CastArguments(node, Type.Real, bindings, 0); } + /*public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArguments(node, Type.Float, bindings, 0); + }*/ public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); @@ -1472,6 +1479,90 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<VCExpr>() != null); return CastArgumentsToOldType(node, bindings, 0); } + public override VCExpr VisitFloatAddOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatSubOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatMulOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatRemOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatMinOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatMaxOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatLeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatLtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatGeqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatGtOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitFloatEqOp(VCExprNAry node, VariableBindings bindings) + { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return CastArgumentsToOldType(node, bindings, 0); + } public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 2c77a252..b5d4dfb5 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -55,6 +55,13 @@ namespace Microsoft.Boogie { return new VCExprRealLit(x); } + public VCExpr/*!*/ Float(BigFloat x) + { + Contract.Ensures(Contract.Result<VCExpr>() != null); + + return new VCExprFloatLit(x); + } + public VCExpr/*!*/ Function(VCExprOp/*!*/ op, List<VCExpr/*!*/>/*!*/ arguments, List<Type/*!*/>/*!*/ typeArguments) { @@ -319,10 +326,13 @@ namespace Microsoft.Boogie { public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real); public static readonly VCExprOp SubIOp = new VCExprNAryOp(2, Type.Int); public static readonly VCExprOp SubROp = new VCExprNAryOp(2, Type.Real); + // public static readonly VCExprOp SubFOp = new VCExprNAryOp(2, Type.Float); public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int); public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real); + //public static readonly VCExprOp MulFOp = new VCExprNAryOp(2, Type.Float); public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int); public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real); + //public static readonly VCExprOp DivFOp = new VCExprNAryOp(2, Type.Float); public static readonly VCExprOp ModOp = new VCExprNAryOp(2, Type.Int); public static readonly VCExprOp PowOp = new VCExprNAryOp(2, Type.Real); public static readonly VCExprOp LtOp = new VCExprNAryOp(2, Type.Bool); @@ -336,6 +346,7 @@ namespace Microsoft.Boogie { public static readonly VCExprOp IfThenElseOp = new VCExprIfThenElseOp(); public static readonly VCExprOp ToIntOp = new VCExprNAryOp(1, Type.Int); public static readonly VCExprOp ToRealOp = new VCExprNAryOp(1, Type.Real); + //public static readonly VCExprOp ToFloatOp = new VCExprNAryOp(1, Type.Float); public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool); @@ -351,6 +362,17 @@ namespace Microsoft.Boogie { return new VCExprBoogieFunctionOp(func); } + // Float nodes + + public VCExprOp BinaryFloatOp(int exp, int man, string op) + { + Contract.Requires(exp > 0); + Contract.Requires(man > 0); + Contract.Requires(op != null); + Contract.Ensures(Contract.Result<VCExpr>() != null); + return new VCExprBinaryFloatOp(exp, man, op); + } + // Bitvector nodes public VCExpr Bitvector(BvConst bv) { @@ -406,7 +428,8 @@ namespace Microsoft.Boogie { Subtype3Op, BvConcatOp, ToIntOp, - ToRealOp + ToRealOp, + ToFloatOp }; internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict; [ContractInvariantMethod] @@ -427,10 +450,13 @@ namespace Microsoft.Boogie { SingletonOpDict.Add(AddROp, SingletonOp.AddOp); SingletonOpDict.Add(SubIOp, SingletonOp.SubOp); SingletonOpDict.Add(SubROp, SingletonOp.SubOp); + //SingletonOpDict.Add(SubFOp, SingletonOp.SubOp); SingletonOpDict.Add(MulIOp, SingletonOp.MulOp); SingletonOpDict.Add(MulROp, SingletonOp.MulOp); + //SingletonOpDict.Add(MulFOp, SingletonOp.MulOp); SingletonOpDict.Add(DivIOp, SingletonOp.DivOp); SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp); + //SingletonOpDict.Add(DivFOp, SingletonOp.FloatDivOp); SingletonOpDict.Add(ModOp, SingletonOp.ModOp); SingletonOpDict.Add(PowOp, SingletonOp.PowOp); SingletonOpDict.Add(LtOp, SingletonOp.LtOp); @@ -441,6 +467,7 @@ namespace Microsoft.Boogie { SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op); SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp); SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp); + //SingletonOpDict.Add(ToFloatOp, SingletonOp.ToFloatOp); } //////////////////////////////////////////////////////////////////////////////// @@ -862,6 +889,31 @@ namespace Microsoft.Boogie.VCExprAST { } } + public class VCExprFloatLit : VCExprLiteral + { + public readonly BigFloat Val; + internal VCExprFloatLit(BigFloat val) + : base(Type.GetFloatType(val.ExponentSize, val.SignificandSize)) + { + this.Val = val; + } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object that) + { + if (Object.ReferenceEquals(this, that)) + return true; + if (that is VCExprFloatLit) + return Val == ((VCExprFloatLit)that).Val; + return false; + } + [Pure] + public override int GetHashCode() + { + return Val.GetHashCode() * 72321; + } + } + ///////////////////////////////////////////////////////////////////////////////// // Operator expressions with fixed arity [ContractClassFor(typeof(VCExprNAry))] @@ -1639,6 +1691,86 @@ namespace Microsoft.Boogie.VCExprAST { } ///////////////////////////////////////////////////////////////////////////////// + // Float operators + + public class VCExprBinaryFloatOp : VCExprOp { + public readonly int Mantissa; + public readonly int Exponent; + private string op; + + public override int Arity { + get { + return 2; + } + } + public override int TypeParamArity { + get { + return 2; + } + } + public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) { + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); + Contract.Ensures(Contract.Result<Type>() != null); + return Type.GetFloatType(Exponent, Mantissa); + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object that) { + if (Object.ReferenceEquals(this, that)) + return true; + if (that is VCExprBinaryFloatOp) + return this.Exponent == ((VCExprBinaryFloatOp)that).Exponent && this.Mantissa == ((VCExprBinaryFloatOp)that).Mantissa; + return false; + } + [Pure] + public override int GetHashCode() { + return Exponent * 81748912 + Mantissa * 67867979; + } + + internal VCExprBinaryFloatOp(int exp, int man, string op) { + this.Exponent = exp; + this.Mantissa = man; + this.op = op; + } + public override Result Accept<Result, Arg> + (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) { + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); + switch (op) { + case ("+"): + return visitor.VisitFloatAddOp(expr, arg); + case ("-"): + return visitor.VisitFloatSubOp(expr, arg); + case ("*"): + return visitor.VisitFloatMulOp(expr, arg); + case ("/"): + return visitor.VisitFloatDivOp(expr, arg); + case ("rem"): + return visitor.VisitFloatRemOp(expr, arg); + case ("min"): + return visitor.VisitFloatMinOp(expr, arg); + case ("max"): + return visitor.VisitFloatMaxOp(expr, arg); + case ("<="): + return visitor.VisitFloatLeqOp(expr, arg); + case ("<"): + return visitor.VisitFloatLtOp(expr, arg); + case (">="): + return visitor.VisitFloatGeqOp(expr, arg); + case (">"): + return visitor.VisitFloatGtOp(expr, arg); + case ("=="): + return visitor.VisitFloatEqOp(expr, arg); + default: + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + } + + ///////////////////////////////////////////////////////////////////////////////// // Bitvector operators public class VCExprBvOp : VCExprOp { diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index 2af4708d..dac9604c 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -242,6 +242,78 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return PrintNAry("Store", node, wr); } + public bool VisitFloatAddOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.add", node, wr); + } + public bool VisitFloatSubOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.sub", node, wr); + } + public bool VisitFloatMulOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.mul", node, wr); + } + public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.div", node, wr); + } + public bool VisitFloatRemOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.rem", node, wr); + } + public bool VisitFloatMinOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.min", node, wr); + } + public bool VisitFloatMaxOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.max", node, wr); + } + public bool VisitFloatLeqOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.leq", node, wr); + } + public bool VisitFloatLtOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.lt", node, wr); + } + public bool VisitFloatGeqOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.geq", node, wr); + } + public bool VisitFloatGtOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.gt", node, wr); + } + public bool VisitFloatEqOp(VCExprNAry node, TextWriter wr) + { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + return PrintNAry("fp.eq", node, wr); + } public bool VisitBvOp(VCExprNAry node, TextWriter wr) { //Contract.Requires(wr != null); //Contract.Requires(node != null); diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index fc1bdd65..a23aaf8a 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -68,6 +68,18 @@ namespace Microsoft.Boogie.VCExprAST { Result VisitLabelOp(VCExprNAry node, Arg arg); Result VisitSelectOp(VCExprNAry node, Arg arg); Result VisitStoreOp(VCExprNAry node, Arg arg); + Result VisitFloatAddOp(VCExprNAry node, Arg arg); + Result VisitFloatSubOp(VCExprNAry node, Arg arg); + Result VisitFloatMulOp(VCExprNAry node, Arg arg); + Result VisitFloatDivOp(VCExprNAry node, Arg arg); + Result VisitFloatRemOp(VCExprNAry node, Arg arg); + Result VisitFloatMinOp(VCExprNAry node, Arg arg); + Result VisitFloatMaxOp(VCExprNAry node, Arg arg); + Result VisitFloatLeqOp(VCExprNAry node, Arg arg); + Result VisitFloatLtOp(VCExprNAry node, Arg arg); + Result VisitFloatGeqOp(VCExprNAry node, Arg arg); + Result VisitFloatGtOp(VCExprNAry node, Arg arg); + Result VisitFloatEqOp(VCExprNAry node, Arg arg); Result VisitBvOp(VCExprNAry node, Arg arg); Result VisitBvExtractOp(VCExprNAry node, Arg arg); Result VisitBvConcatOp(VCExprNAry node, Arg arg); @@ -144,6 +156,78 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException(); } + public Result VisitFloatAddOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatSubOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatMulOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatDivOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatRemOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatMinOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatMaxOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatLeqOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatLtOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatGeqOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatGtOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitFloatEqOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + public Result VisitBvOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -234,6 +318,12 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException(); } + public Result VisitToFloat(VCExprNAry node, Arg arg) //TODO: modify later + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -1438,6 +1528,65 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return StandardResult(node, arg); } + public virtual Result VisitFloatAddOp(VCExprNAry node, Arg arg) { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatSubOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatMulOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatDivOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatRemOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatMinOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatMaxOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatLeqOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatLtOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatGeqOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatGtOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitFloatEqOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } public virtual Result VisitBvOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); @@ -1518,6 +1667,11 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return StandardResult(node, arg); } + public virtual Result VisitToFloatOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl new file mode 100644 index 00000000..b1a240be --- /dev/null +++ b/Test/floats/float0.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : real) returns (r : float<8, 24>) +{ + r := 15; // Error + r := 15.0; // Error + r := fp(false, 1bv8, 0bv22); // Error + r := fp<8, 23>(1bv31); // Error + r := x; // Error + r := fp<8, 23>(1bv31) + fp<8, 23>(1bv31); // Error + r := fp<8, 24>(1bv32) + fp<8, 23>(1bv31); // Error + + return; +}
\ No newline at end of file diff --git a/Test/floats/float0.bpl.expect b/Test/floats/float0.bpl.expect new file mode 100644 index 00000000..4c934700 --- /dev/null +++ b/Test/floats/float0.bpl.expect @@ -0,0 +1,8 @@ +float0.bpl(5,1): Error: mismatched types in assignment command (cannot assign int to float (8 24))
+float0.bpl(6,1): Error: mismatched types in assignment command (cannot assign real to float (8 24))
+float0.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float0.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float0.bpl(9,1): Error: mismatched types in assignment command (cannot assign real to float (8 24))
+float0.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float0.bpl(11,23): Error: invalid argument types (float (8 24) and float (8 23)) to binary operator +
+7 type checking errors detected in float0.bpl
diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl new file mode 100644 index 00000000..9ed62579 --- /dev/null +++ b/Test/floats/float1.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : float<8, 24>) returns (r : float<8, 24>)
+{
+ r := fp(false, 1bv8, 0bv23);
+ r := fp<8, 24>(1bv32);
+ r := x;
+ r := x + fp<8, 24>(1bv32);
+ r := fp<8, 24>(1bv32) + fp<8, 24>(1bv32);
+ assert(r == fp<8, 24>(2bv32));
+
+ return;
+}
\ No newline at end of file diff --git a/Test/floats/float1.bpl.expect b/Test/floats/float1.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float10.bpl b/Test/floats/float10.bpl new file mode 100644 index 00000000..bf07aec6 --- /dev/null +++ b/Test/floats/float10.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); + +procedure double_range_true() returns () { + var x : float64; + havoc x; + if (x >= TO_FLOAT64_REAL(-1e307) && x <= TO_FLOAT64_REAL(1e307)) { + assert(x==x); + } +} + +procedure double_range_false() returns () { + var x : float64; + havoc x; + assert(x==x); +}
\ No newline at end of file diff --git a/Test/floats/float10.bpl.expect b/Test/floats/float10.bpl.expect new file mode 100644 index 00000000..cae8d781 --- /dev/null +++ b/Test/floats/float10.bpl.expect @@ -0,0 +1,5 @@ +float10.bpl(17,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ float10.bpl(16,2): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/floats/float11.bpl b/Test/floats/float11.bpl new file mode 100644 index 00000000..424c5a2d --- /dev/null +++ b/Test/floats/float11.bpl @@ -0,0 +1,22 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
+
+procedure main() returns () {
+ var tick : float32;
+ var time : float32;
+ var i: int;
+
+ tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
+ time := TO_FLOAT32_INT(0);
+
+ i := 0;
+ while (i < 10)
+ {
+ time := time + tick;
+ i := i + 1;
+ }
+ assert time == TO_FLOAT32_INT(1);
+}
\ No newline at end of file diff --git a/Test/floats/float11.bpl.expect b/Test/floats/float11.bpl.expect new file mode 100644 index 00000000..9365da58 --- /dev/null +++ b/Test/floats/float11.bpl.expect @@ -0,0 +1,7 @@ +float11.bpl(21,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ float11.bpl(12,7): anon0
+ float11.bpl(16,2): anon3_LoopHead
+ float11.bpl(16,2): anon3_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/floats/float12.bpl b/Test/floats/float12.bpl new file mode 100644 index 00000000..349abb41 --- /dev/null +++ b/Test/floats/float12.bpl @@ -0,0 +1,16 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); + +procedure main() returns () { + var x : float64; + var y : float32; + + x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1); + y := TO_FLOAT32_FLOAT64(x); + assert x != TO_FLOAT64_FLOAT32(y); +}
\ No newline at end of file diff --git a/Test/floats/float12.bpl.expect b/Test/floats/float12.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float12.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float2.bpl b/Test/floats/float2.bpl new file mode 100644 index 00000000..1a4d02cd --- /dev/null +++ b/Test/floats/float2.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo(x : float16) returns(r : float32) {
+ var y : float64;
+ var z : float128;
+
+ r := x; // Error
+ r := y; // Error
+ r := z; // Error
+ y := x; // Error
+ y := z; // Error
+ z := x; // Error
+
+ return;
+}
\ No newline at end of file diff --git a/Test/floats/float2.bpl.expect b/Test/floats/float2.bpl.expect new file mode 100644 index 00000000..62348741 --- /dev/null +++ b/Test/floats/float2.bpl.expect @@ -0,0 +1,7 @@ +float2.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (8 24))
+float2.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (11 53) to float (8 24))
+float2.bpl(9,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (8 24))
+float2.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (11 53))
+float2.bpl(11,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (11 53))
+float2.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (15 113))
+6 type checking errors detected in float2.bpl
diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl new file mode 100644 index 00000000..34059f80 --- /dev/null +++ b/Test/floats/float3.bpl @@ -0,0 +1,27 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+ var x : float32;
+ var y : float32;
+ var z : float32;
+
+ z := x + y;
+ z := x - y;
+ z := x * y;
+ assume(y != fp<8, 24>(0bv32));
+ z := x / y;
+
+ z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32);
+ assert(z == fp<8, 24>(2bv32));
+
+ z := fp<8, 24>(2bv32) - fp<8, 24>(1bv32);
+ assert(z == fp<8, 24>(1bv32));
+
+ z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23);
+ assert(z == fp(false, 127bv8, 0bv23));
+
+ z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32);
+ assert(z == fp(false, 127bv8, 0bv23));
+
+ return;
+}
\ No newline at end of file diff --git a/Test/floats/float3.bpl.expect b/Test/floats/float3.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float3.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl new file mode 100644 index 00000000..7bb24250 --- /dev/null +++ b/Test/floats/float4.bpl @@ -0,0 +1,11 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo() returns (r : float32) {
+ r := fp<8, 24>(NaN);
+ r := fp<8, 24>(+oo);
+ r := fp<8, 24>(-oo);
+ r := fp<8, 24>(+zero);
+ r := fp<8, 24>(-zero);
+
+ return;
+}
\ No newline at end of file diff --git a/Test/floats/float4.bpl.expect b/Test/floats/float4.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/floats/float4.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float5.bpl b/Test/floats/float5.bpl new file mode 100644 index 00000000..fd630394 --- /dev/null +++ b/Test/floats/float5.bpl @@ -0,0 +1,24 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_INT(int) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_REAL(real) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV31(bv31) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV32(bv32) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_FLOAT824(float<8, 24>) returns (float<8, 23>);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT823(float<8, 23>) returns (float<8, 24>);
+
+procedure foo(x : float<8, 24>) returns (r : float<8, 24>) {
+ r := TO_FLOAT823_INT(5); // Error
+ r := TO_FLOAT823_REAL(5.0); // Error
+ r := TO_FLOAT823_BV31(0bv31); // Error
+ r := TO_FLOAT823_BV32(0bv32); // Error
+ r := TO_FLOAT823_FLOAT824(fp<8, 24>(1bv32)); // Error
+ r := TO_FLOAT824_FLOAT823(fp<8, 24>(1bv32)); // Error
+ r := TO_FLOAT824_FLOAT823(fp<8, 23>(1bv31));
+
+ r := TO_FLOAT823_FLOAT824(x); // Error
+ r := TO_FLOAT824_FLOAT823(x); // Error
+
+ return;
+}
\ No newline at end of file diff --git a/Test/floats/float5.bpl.expect b/Test/floats/float5.bpl.expect new file mode 100644 index 00000000..6c0b86af --- /dev/null +++ b/Test/floats/float5.bpl.expect @@ -0,0 +1,9 @@ +float5.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(13,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(14,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(15,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(16,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(17,42): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23))
+float5.bpl(20,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24))
+float5.bpl(21,27): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23))
+8 type checking errors detected in float5.bpl
diff --git a/Test/floats/float6.bpl b/Test/floats/float6.bpl new file mode 100644 index 00000000..fe0eab0e --- /dev/null +++ b/Test/floats/float6.bpl @@ -0,0 +1,50 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_INT(int) returns (float<8, 24>);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_REAL(real) returns (float<8, 24>);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_BV32(bv32) returns (float<8, 24>);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT1153_BV64(bv64) returns (float<11, 53>);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT32(float32) returns (float<8, 24>); //Should just be an identity function
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT824(float<8, 24>) returns (float32); //Should just be an identity function
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32);
+function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64);
+
+procedure main() returns () {
+ var i : int;
+ var r : real;
+ var f824 : float<8, 24>;
+ var f32 : float32;
+ var f1153 : float<11, 53>;
+ var f64 : float64;
+
+ f824 := TO_FLOAT824_INT(5);
+ f32 := TO_FLOAT824_INT(5);
+ f824 := TO_FLOAT824_REAL(5.0);
+ f32 := TO_FLOAT824_REAL(5.0);
+
+ f824 := TO_FLOAT824_BV32(0bv32);
+ f32 := TO_FLOAT824_BV32(0bv32);
+ f1153 := TO_FLOAT1153_BV64(0bv64);
+ f64 := TO_FLOAT1153_BV64(0bv64);
+
+ f824 := TO_FLOAT824_FLOAT32(fp<8, 24>(0bv32));
+ f32 := TO_FLOAT32_FLOAT824(fp<8, 24>(0bv32));
+ f824 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32));
+ f32 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32));
+ f1153 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32));
+ f64 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32));
+
+ f824 := TO_FLOAT824_INT(5);
+ f32 := TO_FLOAT32_FLOAT824(f824);
+ assert(f32 == f824);
+
+ f32 := TO_FLOAT824_INT(5);
+ f824 := TO_FLOAT824_FLOAT32(f32);
+ assert(f32 == f824);
+
+ f32 := TO_FLOAT32_FLOAT64(f64);
+ f64 := TO_FLOAT64_FLOAT32(f32);
+
+ return;
+}
\ No newline at end of file diff --git a/Test/floats/float6.bpl.expect b/Test/floats/float6.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float6.bpl.expect @@ -0,0 +1,2 @@ +
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float7.bpl b/Test/floats/float7.bpl new file mode 100644 index 00000000..f330b2ea --- /dev/null +++ b/Test/floats/float7.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+ var x : float<11, 53>;
+ var y : float<11, 53>;
+ var z : float<11, 53>;
+ var r : float<11, 53>;
+ x := fp<11, 53> (10000000bv64);
+ y := x + fp<11, 53>(1bv64);
+ z := x - fp<11, 53>(1bv64);
+ r := y - z;
+ assert r == fp<11, 53> (2bv64);
+}
\ No newline at end of file diff --git a/Test/floats/float7.bpl.expect b/Test/floats/float7.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float7.bpl.expect @@ -0,0 +1,2 @@ +
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl new file mode 100644 index 00000000..78c11a2b --- /dev/null +++ b/Test/floats/float8.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main() returns () {
+ var x : float32;
+ var y : float32;
+ var z : float32;
+ var r : float32;
+ x := fp<8, 24>(3221225472bv32);
+ y := x + fp<8, 24>(1bv32);
+ z := x - fp<8, 24>(1bv32);
+ r := y - z;
+ assert r == fp<8, 24>(2bv32);
+}
\ No newline at end of file diff --git a/Test/floats/float8.bpl.expect b/Test/floats/float8.bpl.expect new file mode 100644 index 00000000..426c21e0 --- /dev/null +++ b/Test/floats/float8.bpl.expect @@ -0,0 +1,5 @@ +float8.bpl(12,2): Error BP5001: This assertion might not hold.
+Execution trace:
+ float8.bpl(8,4): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/floats/float9.bpl b/Test/floats/float9.bpl new file mode 100644 index 00000000..cb4f3afd --- /dev/null +++ b/Test/floats/float9.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
+function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
+
+procedure main() returns () {
+ var x : float32;
+ var y : float32;
+ var z : float32;
+ var r : float32;
+ x := TO_FLOAT32_REAL(1e7);
+ y := x + TO_FLOAT32_INT(1);
+ z := x - TO_FLOAT32_INT(1);
+ r := y - z;
+ assert r == TO_FLOAT32_INT(2);
+}
\ No newline at end of file diff --git a/Test/floats/float9.bpl.expect b/Test/floats/float9.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float9.bpl.expect @@ -0,0 +1,2 @@ +
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test1/IntReal.bpl.expect b/Test/test1/IntReal.bpl.expect index 021a8389..b532d22a 100644 --- a/Test/test1/IntReal.bpl.expect +++ b/Test/test1/IntReal.bpl.expect @@ -12,8 +12,8 @@ IntReal.bpl(19,12): Error: invalid argument types (real and int) to binary opera IntReal.bpl(25,8): Error: invalid argument types (int and real) to binary operator ** IntReal.bpl(29,14): Error: invalid argument types (real and int) to binary operator == IntReal.bpl(31,13): Error: invalid argument types (int and real) to binary operator == -IntReal.bpl(34,6): Error: argument type int does not match expected type real -IntReal.bpl(35,6): Error: argument type real does not match expected type int +IntReal.bpl(34,6): Error: argument type int does not match expected type real or type float +IntReal.bpl(35,6): Error: argument type real does not match expected type int or type float IntReal.bpl(47,8): Error: invalid argument types (real and int) to binary operator div IntReal.bpl(48,8): Error: invalid argument types (real and int) to binary operator mod 18 type checking errors detected in IntReal.bpl |