From 0324757fb1a12d76861a51be988690bf8de75f64 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Wed, 14 Oct 2015 12:57:50 -0600 Subject: Modified translation so that z3 runs with type checking for simple binary operations --- Source/Basetypes/BigFloat.cs | 48 +++------- Source/Core/AbsyExpr.cs | 1 - Source/Provers/SMTLib/SMTLibLineariser.cs | 76 ++++++++++++++- Source/Provers/SMTLib/Z3.cs | 4 +- Source/VCExpr/Boogie2VCExpr.cs | 36 +++++-- Source/VCExpr/SimplifyLikeLineariser.cs | 120 ++++++++++++++++++++--- Source/VCExpr/TypeErasure.cs | 84 ++++++++++++++++ Source/VCExpr/VCExprAST.cs | 56 ++++++++--- Source/VCExpr/VCExprASTPrinter.cs | 72 ++++++++++++++ Source/VCExpr/VCExprASTVisitors.cs | 154 +++++++++++++++++++++++++++--- 10 files changed, 567 insertions(+), 84 deletions(-) (limited to 'Source') diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs index e9d5e670..9e798959 100644 --- a/Source/Basetypes/BigFloat.cs +++ b/Source/Basetypes/BigFloat.cs @@ -33,7 +33,7 @@ namespace Microsoft.Basetypes [Rep] internal readonly int exponentSize; //The bit size of the exponent [Rep] - internal readonly BigDec dec_value; + internal readonly String dec_value; [Rep] internal readonly bool isDec; @@ -61,7 +61,7 @@ namespace Microsoft.Basetypes } } - public BigDec Decimal { + public String Decimal { get { return dec_value; } @@ -102,7 +102,7 @@ namespace Microsoft.Basetypes public static BigFloat FromBigDec(BigDec v) { - return new BigFloat(v, 8, 24); + return new BigFloat(v.ToDecimalString(), 8, 24); } [Pure] @@ -114,11 +114,11 @@ namespace Microsoft.Basetypes { switch (vals.Length) { case 1: - return new BigFloat(BigDec.FromString(vals[0]), 8, 24); + return new BigFloat(vals[0], 8, 24); case 2: return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24); case 3: - return new BigFloat(BigDec.FromString(vals[0]), Int32.Parse(vals[1]), Int32.Parse(vals[2])); + return new BigFloat(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2])); case 4: return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3])); default: @@ -136,10 +136,10 @@ namespace Microsoft.Basetypes this.mantissa = mantissa; this.mantissaSize = mantissaSize; this.isDec = false; - this.dec_value = BigDec.ZERO; + this.dec_value = ""; } - internal BigFloat(BigDec dec_value, int exponentSize, int mantissaSize) { + internal BigFloat(String dec_value, int exponentSize, int mantissaSize) { this.exponentSize = exponentSize; this.mantissaSize = mantissaSize; this.exponent = 0; @@ -181,7 +181,7 @@ namespace Microsoft.Basetypes [Pure] public override string/*!*/ ToString() { Contract.Ensures(Contract.Result() != null); - return String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString()); + return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString()); } @@ -313,34 +313,8 @@ namespace Microsoft.Basetypes [Pure] public string ToDecimalString() { - //TODO: fix for fp functionality - string m = Mantissa.ToString(); - var e = Exponent; - if (0 <= Exponent) { - return m + Zeros(e) + ".0"; - } else { - e = -e; - // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string) - var maxK = e < m.Length ? e : m.Length - 1; - var last = m.Length - 1; - var k = 0; - while (k < maxK && m[last - k] == '0') { - k++; - } - if (0 < k) { - // chop off the suffix of k zeros from m and adjust e accordingly - m = m.Substring(0, m.Length - k); - e -= k; - } - if (e == 0) { - return m; - } else if (e < m.Length) { - var n = m.Length - e; - return m.Substring(0, n) + "." + m.Substring(n); - } else { - return "0." + Zeros(e - m.Length) + m; - } - } + Contract.Ensures(Contract.Result() != null); + return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString()); } [Pure] @@ -436,7 +410,7 @@ namespace Microsoft.Basetypes public bool IsNegative { get { - return (isDec && dec_value >= BigDec.ZERO) || mantissa >= 0; + return (isDec && dec_value[0] == '-') || mantissa < 0; } } diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index cf6fb922..ad537288 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1642,7 +1642,6 @@ namespace Microsoft.Boogie { case Opcode.Div: case Opcode.Mod: case Opcode.RealDiv: - case Opcode.FloatDiv: case Opcode.Pow: case Opcode.Neq: // Neq is allowed, but not Eq case Opcode.Subtype: diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index f030870e..629f7e2d 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 "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; //TODO: Match z3 syntax + return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; else if (t.IsBv) { return "(_ BitVec " + t.BvBits + ")"; } else { @@ -204,11 +204,13 @@ namespace Microsoft.Boogie.SMTLib else if (node is VCExprFloatLit) { BigFloat lit = ((VCExprFloatLit)node).Val; + wr.Write(("((_ to_fp 8 24) roundTowardZero ")); if (lit.IsNegative) // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols") wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString()); else wr.Write(lit.ToDecimalString()); + wr.Write(")"); } else { Contract.Assert(false); @@ -616,6 +618,78 @@ namespace Microsoft.Boogie.SMTLib return true; } + public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.add roundTowardZero", node, options); + return true; + } + + public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.sub roundTowardZero", node, options); + return true; + } + + public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.mul roundTowardZero", node, options); + return true; + } + + public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.div roundTowardZero", node, options); + return true; + } + + public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("fp.rem roundTowardZero", 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/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 8e8b2d55..250e04c9 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -253,7 +253,7 @@ namespace Microsoft.Boogie.SMTLib //if (options.Inspector != null) // options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100"); - options.AddWeakSmtOption("TYPE_CHECK", "false"); + options.AddWeakSmtOption("TYPE_CHECK", "true"); options.AddWeakSmtOption("smt.BV.REFLECT", "true"); if (options.TimeLimit > 0) @@ -334,7 +334,7 @@ namespace Microsoft.Boogie.SMTLib //if (options.Inspector != null) // options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100"); - options.AddWeakSmtOption("TYPE_CHECK", "false"); + options.AddWeakSmtOption("TYPE_CHECK", "true"); options.AddWeakSmtOption("BV_REFLECT", "true"); if (options.TimeLimit > 0) diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index f0dc505d..ad319c0e 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -1076,34 +1076,48 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result() != 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) { @@ -1118,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 0ff6d67f..6f74fe08 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -384,6 +384,14 @@ namespace Microsoft.Boogie.VCExprAST { 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"; @@ -888,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); @@ -948,11 +1053,8 @@ namespace Microsoft.Boogie.VCExprAST { WriteTermApplication(intAddName, node, options); } } - else if (node.Type.IsReal) { - WriteTermApplication(realAddName, node, options); - } else { - WriteTermApplication(floatAddName, node, options); + WriteTermApplication(realAddName, node, options); } return true; } @@ -1008,14 +1110,6 @@ namespace Microsoft.Boogie.VCExprAST { 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 VisitPowOp(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 5e821ea2..6fb38c27 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -1479,6 +1479,90 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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 c44800fc..3f6e3b7a 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -324,7 +324,6 @@ 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 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); @@ -359,11 +358,13 @@ namespace Microsoft.Boogie { // Float nodes - public VCExpr AddFOp(VCExpr f1, VCExpr f2) + public VCExprOp BinaryFloatOp(int exp, int man, string op) { - Contract.Requires(f1 != null); - Contract.Requires(f2 != null); - return Function(new VCExprFloatOp(f1.Type.FloatExponent, f1.Type.FloatMantissa)); + Contract.Requires(exp > 0); + Contract.Requires(man > 0); + Contract.Requires(op != null); + Contract.Ensures(Contract.Result() != null); + return new VCExprBinaryFloatOp(exp, man, op); } // Bitvector nodes @@ -441,7 +442,6 @@ 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); @@ -1677,18 +1677,19 @@ namespace Microsoft.Boogie.VCExprAST { ///////////////////////////////////////////////////////////////////////////////// // Float operators - public class VCExprFloatOp : VCExprOp { + public class VCExprBinaryFloatOp : VCExprOp { public readonly int Mantissa; public readonly int Exponent; + private string op; public override int Arity { get { - return 1; + return 2; } } public override int TypeParamArity { get { - return 0; + return 2; } } public override Type InferType(List args, List/*!*/ typeArgs) { @@ -1703,8 +1704,8 @@ namespace Microsoft.Boogie.VCExprAST { public override bool Equals(object that) { if (Object.ReferenceEquals(this, that)) return true; - if (that is VCExprFloatOp) - return this.Exponent == ((VCExprFloatOp)that).Exponent && this.Mantissa == ((VCExprFloatOp)that).Mantissa; + if (that is VCExprBinaryFloatOp) + return this.Exponent == ((VCExprBinaryFloatOp)that).Exponent && this.Mantissa == ((VCExprBinaryFloatOp)that).Mantissa; return false; } [Pure] @@ -1712,15 +1713,44 @@ namespace Microsoft.Boogie.VCExprAST { return Exponent * 81748912 + Mantissa * 67867979; } - internal VCExprFloatOp(int exp, int man) { + internal VCExprBinaryFloatOp(int exp, int man, string op) { this.Exponent = exp; this.Mantissa = man; + this.op = op; } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { //Contract.Requires(visitor != null); //Contract.Requires(expr != null); - return visitor.VisitBvOp(expr, arg); + 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(); + } } } diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index 00e6fb9c..8e2f5d12 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 a1fb2ff4..c81f69e5 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(); @@ -189,12 +273,6 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException(); } - public Result VisitFloatDivOp(VCExprNAry node, Arg arg) - { - Contract.Requires(node != null); - throw new NotImplementedException(); - } - public Result VisitPowOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -1450,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); @@ -1494,11 +1631,6 @@ namespace Microsoft.Boogie.VCExprAST { //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 VisitPowOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); -- cgit v1.2.3