From 52aa9b8f63a3d955031e7a0dfd6e575ca7cf76b3 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Mon, 13 Jul 2015 19:40:09 -0600 Subject: Modified internal abstract float representation to allow user-defined mantissa and exponent --- Source/Core/AbsyType.cs | 197 +++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 188 insertions(+), 9 deletions(-) (limited to 'Source/Core/AbsyType.cs') diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index ae307f7a..50fde975 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -325,6 +325,27 @@ namespace Microsoft.Boogie { } } + public virtual bool isFloat { + get { + return false; + } + } + public virtual int FloatMantissa { + get { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.FloatMantissa should never be called + } + } + public virtual int FloatExponent { + get { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.FloatExponent should never be called + } + } public virtual bool IsBv { get { return false; @@ -341,7 +362,6 @@ namespace Microsoft.Boogie { public static readonly Type/*!*/ Int = new BasicType(SimpleType.Int); public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real); - public static readonly Type/*!*/ Float = new BasicType(SimpleType.Float); public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool); private static BvType[] bvtypeCache; @@ -364,6 +384,14 @@ namespace Microsoft.Boogie { } } + static public FloatType GetFloatType(int exp, int man) { + Contract.Requires(0 <= exp); + Contract.Requires(0 <= man); + Contract.Ensures(Contract.Result() != null); + + return new FloatType(exp, man); + } + //------------ Match formal argument types on actual argument types //------------ and return the resulting substitution of type variables @@ -877,8 +905,6 @@ namespace Microsoft.Boogie { return "int"; case SimpleType.Real: return "real"; - case SimpleType.Float: - return "float"; case SimpleType.Bool: return "bool"; } @@ -1001,11 +1027,6 @@ namespace Microsoft.Boogie { return this.T == SimpleType.Real; } } - public override bool IsFloat { - get { - return this.T == SimpleType.Float; - } - } public override bool IsBool { get { return this.T == SimpleType.Bool; @@ -1021,6 +1042,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); + Mantissa = mantissa; + Exponent = exponent; + } + + public FloatType(int exponent, int mantissa) + : base(Token.NoToken) { + Mantissa = mantissa; + Exponent = exponent; + } + + //----------- 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/*!*/ varMap) + { + //Contract.Requires(cce.NonNullElements(varMap)); + Contract.Ensures(Contract.Result() != null); + // FloatTypes are immutable anyway, we do not clone + return this; + } + + public override Type CloneUnresolved() + { + Contract.Ensures(Contract.Result() != 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() != null); + return "(_ FP " + Exponent + " " + Mantissa + ")"; + } + + //----------- Equality ---------------------------------- + + [Pure] + public override bool Equals(Type/*!*/ that, + List/*!*/ thisBoundVariables, + List/*!*/ 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/*!*/ unifiableVariables, + // an idempotent substitution that describes the + // unification result up to a certain point + IDictionary/*!*/ 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/*!*/ subst) + { + Contract.Ensures(Contract.Result() != null); + return this; + } + + //----------- Hashcodes ---------------------------------- + + [Pure] + public override int GetHashCode(List boundVariables) + { + return this.Mantissa.GetHashCode() + this.Exponent.GetHashCode(); + } + + //----------- Resolution ---------------------------------- + + public override Type ResolveType(ResolutionContext rc) + { + //Contract.Requires(rc != null); + Contract.Ensures(Contract.Result() != null); + // nothing to resolve + return this; + } + + // determine the free variables in a type, in the order in which the variables occur + public override List/*!*/ FreeVariables + { + get + { + Contract.Ensures(Contract.Result>() != null); + + return new List(); // bitvector-type are closed + } + } + + public override List/*!*/ FreeProxies + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return new List(); + } + } + + //----------- 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() != null); + return visitor.VisitFloatType(this); + } + + } + + //===================================================================== + public class BvType : Type { public readonly int Bits; @@ -3554,7 +3734,6 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); public enum SimpleType { Int, Real, - Float, Bool }; -- cgit v1.2.3