diff options
Diffstat (limited to 'Source/Core/AbsyType.cs')
| -rw-r--r-- | Source/Core/AbsyType.cs | 238 |
1 files changed, 235 insertions, 3 deletions
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 2953f15e..ab6ef5e9 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 FloatSignificand { + get { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } // Type.FloatSignificand should never be called + } + } public virtual bool IsBv { get { return false; @@ -358,6 +386,14 @@ namespace Microsoft.Boogie { } } + static public FloatType GetFloatType(int sig, int exp) { + Contract.Requires(0 <= exp); + Contract.Requires(0 <= sig); + Contract.Ensures(Contract.Result<FloatType>() != null); + + return new FloatType(sig, exp); + } + //------------ 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 Significand; //Size of Significand in bits + public readonly int Exponent; //Size of exponent in bits + + public FloatType(IToken token, int significand, int exponent) + : base(token) { + Contract.Requires(token != null); + Significand = significand; + Exponent = exponent; + } + + public FloatType(int significand, int exponent) + : base(Token.NoToken) { + Significand = significand; + 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<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" + Significand + "e" + Exponent; + } + + //----------- 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.Significand == thatFloatType.Significand && 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.Significand.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 FloatSignificand { + get { + return Significand; + } + } + 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; @@ -1286,7 +1481,7 @@ Contract.Requires(that != null); public override Type ResolveType(ResolutionContext rc) { //Contract.Requires(rc != null); Contract.Ensures(Contract.Result<Type>() != null); - // first case: the type name denotes a bitvector-type + // first case: the type name denotes a bitvector-type or float-type if (Name.StartsWith("bv") && Name.Length > 2) { bool is_bv = true; for (int i = 2; i < Name.Length; ++i) { @@ -1305,6 +1500,28 @@ Contract.Requires(that != null); } } + if (Name.StartsWith("float") && Name.Length > 5) + { + bool is_float = true; + int i = 5; + for (; is_float && Name[i] != 'e'; i++) + if (i >= Name.Length-1 || !char.IsDigit(Name[i])) //There must be an e + is_float = false; + int mid = i; + i++; + for (; i < Name.Length && is_float; i++) + if (!char.IsDigit(Name[i])) + is_float = false; + if (is_float) { + if (Arguments.Count > 0) { + rc.Error(this, + "float types must not be applied to arguments: {0}", + Name); + } + return new FloatType(tok, int.Parse(Name.Substring(5, mid-5)), int.Parse(Name.Substring(mid+1))); + } + } + // second case: the identifier is resolved to a type variable TypeVariable var = rc.LookUpTypeBinder(Name); if (var != null) { @@ -1899,6 +2116,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 +2970,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; |