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/AbsyExpr.cs | 49 +++----- Source/Core/AbsyType.cs | 197 ++++++++++++++++++++++++++++-- Source/Core/Parser.cs | 12 +- Source/Core/StandardVisitor.cs | 6 + Source/Provers/SMTLib/SMTLibLineariser.cs | 4 +- Source/Provers/SMTLib/SMTLibProcess.cs | 1 + Source/VCExpr/Boogie2VCExpr.cs | 8 +- Source/VCExpr/TypeErasure.cs | 4 +- Source/VCExpr/VCExprAST.cs | 19 +-- 9 files changed, 242 insertions(+), 58 deletions(-) diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 9297bcbc..7e7ed10a 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -561,7 +561,7 @@ namespace Microsoft.Boogie { { Contract.Requires(tok != null); Val = v; - Type = Type.Float; + Type = Type.GetFloatType(v.ExponentSize, v.MantissaSize); if (immutable) CachedHashCode = ComputeHashCode(); } @@ -638,7 +638,8 @@ namespace Microsoft.Boogie { } else if (Val is BigDec) { return Type.Real; } else if (Val is BigFloat) { - return Type.Float; + BigFloat temp = (BigFloat)Val; + return Type.GetFloatType(temp.ExponentSize, temp.MantissaSize); } else if (Val is BvConst) { return Type.GetBvType(((BvConst)Val).Bits); } else { @@ -1376,9 +1377,9 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real)) { return Type.Real; } - if (arg0type.Unify(Type.Float)) { - return Type.Float; - } + //if (arg0type.Unify(Type.Float)) { + //return Type.Float; + //} goto BAD_TYPE; case Opcode.Not: if (arg0type.Unify(Type.Bool)) { @@ -1519,7 +1520,7 @@ namespace Microsoft.Boogie { case Opcode.RealDiv: return "/"; case Opcode.FloatDiv: - return "/f"; + return "/"; case Opcode.Pow: return "**"; case Opcode.Eq: @@ -1706,10 +1707,10 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { return Type.Real; } - if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float)) - { - return Type.Float; - } + //if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float)) + //{ + //return Type.Float; + //} goto BAD_TYPE; case Opcode.Div: case Opcode.Mod: @@ -1723,13 +1724,6 @@ namespace Microsoft.Boogie { return Type.Real; } goto BAD_TYPE; - case Opcode.FloatDiv: //TODO: Modify - if ((arg0type.Unify(Type.Int) || arg0type.Unify(Type.Real) || arg0type.Unify(Type.Float)) && - (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real) || arg0type.Unify(Type.Float))) - { - return Type.Float; - } - goto BAD_TYPE; case Opcode.Pow: if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { return Type.Real; @@ -1761,10 +1755,10 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { return Type.Bool; } - if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float)) - { - return Type.Bool; - } + //if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float)) + //{ + //return Type.Bool; + //} goto BAD_TYPE; case Opcode.And: case Opcode.Or: @@ -1809,8 +1803,8 @@ namespace Microsoft.Boogie { case Opcode.Pow: return Type.Real; - case Opcode.FloatDiv: - return Type.Float; + //case Opcode.FloatDiv: + //return Type.Float; case Opcode.Eq: case Opcode.Neq: @@ -2267,23 +2261,14 @@ namespace Microsoft.Boogie { this.name = "int"; this.type = Type.Int; this.argType = Type.Real; - this.argType2 = Type.Float; this.hashCode = 1; break; case CoercionType.ToReal: this.name = "real"; this.type = Type.Real; this.argType = Type.Int; - this.argType2 = Type.Float; this.hashCode = 2; break; - case CoercionType.ToFloat: - this.name = "float"; - this.type = Type.Float; - this.argType = Type.Int; - this.argType2 = Type.Real; - this.hashCode = 3; - break; default: Contract.Assert(false); break; 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 }; diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 6f793503..bb372cfb 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -668,7 +668,17 @@ private class BvBounds : Expr { ty = new BasicType(t, SimpleType.Real); } else if (la.kind == 98) { Get(); - ty = new BasicType(t, SimpleType.Float); + if (la.kind == 9) { + Get(); + Expect(3); + int exp = Int32.Parse(t.val); + Expect(3); + int man = Int32.Parse(t.val); + ty = new FloatType(t, exp, man); + Expect(10); + } + else + ty = new FloatType(t, 8, 23); } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Bool); diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 0323d4db..97215cfb 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -103,6 +103,12 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return this.VisitType(node); } + public virtual Type VisitFloatType(FloatType node) + { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + return this.VisitType(node); + } public virtual Expr VisitBvConcatExpr(BvConcatExpr node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index b834aa6b..c7ae9d57 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -141,7 +141,7 @@ namespace Microsoft.Boogie.SMTLib else if (t.IsReal) return "Real"; else if (t.IsFloat) - return "Real"; //TODO: Make to be a float + return t.ToString(); //TODO: Match z3 syntax else if (t.IsBv) { return "(_ BitVec " + t.BvBits + ")"; } else { @@ -690,7 +690,7 @@ namespace Microsoft.Boogie.SMTLib } public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options) - { + { //TODO: match z3 WriteApplication("/f", node, options); return true; } diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 4a1331c5..2b09362b 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -93,6 +93,7 @@ namespace Microsoft.Boogie.SMTLib log = log.Replace("\r", "").Replace("\n", " "); Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log); } + Console.WriteLine(cmd); //TODO: Remove This Line toProver.WriteLine(cmd); } diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 942116eb..f0dc505d 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -1005,12 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST { if (cce.NonNull(e.Type).IsInt) { return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e); } - else if (cce.NonNull(e.Type).IsReal) { + 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 {//is float + //return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e); + //} } else { return Gen.Not(this.args); diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 4632b1e4..5e821ea2 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -1424,13 +1424,13 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result() != null); return CastArguments(node, Type.Real, bindings, 0); } - public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) + /*public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); return CastArguments(node, Type.Float, bindings, 0); - } + }*/ public override VCExpr VisitPowOp(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 291d6d42..36692f30 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -324,16 +324,16 @@ namespace Microsoft.Boogie { public static readonly VCExprOp AddIOp = new VCExprNAryOp(2, Type.Int); public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real); - public static readonly VCExprOp AddFOp = new VCExprNAryOp(2, Type.Float); + //public static readonly VCExprOp AddFOp = new VCExprNAryOp(2, Type.Float); 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 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 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 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); @@ -347,7 +347,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 ToFloatOp = new VCExprNAryOp(1, Type.Float); public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool); @@ -433,13 +433,16 @@ namespace Microsoft.Boogie { SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp); SingletonOpDict.Add(AddIOp, SingletonOp.AddOp); SingletonOpDict.Add(AddROp, SingletonOp.AddOp); + //SingletonOpDict.Add(AddFOp, 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(DivFOp, SingletonOp.FloatDivOp); SingletonOpDict.Add(ModOp, SingletonOp.ModOp); SingletonOpDict.Add(PowOp, SingletonOp.PowOp); SingletonOpDict.Add(LtOp, SingletonOp.LtOp); @@ -450,7 +453,7 @@ namespace Microsoft.Boogie { SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op); SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp); SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp); - SingletonOpDict.Add(ToFloatOp, SingletonOp.ToFloatOp); + //SingletonOpDict.Add(ToFloatOp, SingletonOp.ToFloatOp); } //////////////////////////////////////////////////////////////////////////////// @@ -876,7 +879,7 @@ namespace Microsoft.Boogie.VCExprAST { { public readonly BigFloat Val; internal VCExprFloatLit(BigFloat val) - : base(Type.Float) + : base(Type.GetFloatType(val.ExponentSize, val.MantissaSize)) { this.Val = val; } -- cgit v1.2.3