From 51b7e8146f413b83a412572fcc9e3a1a8b302b79 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Thu, 17 Mar 2016 13:01:10 -0600 Subject: modified floating point syntax and modified floating point constants to use bitvector values --- Source/AbsInt/IntervalDomain.cs | 6 ++-- Source/Basetypes/BigFloat.cs | 43 ++++++++++------------------- Source/BoogieDriver/BoogieDriver.cs | 2 +- Source/Core/AbsyExpr.cs | 4 +-- Source/Core/Parser.cs | 46 ++++++++++++++++++------------- Source/Provers/SMTLib/SMTLibLineariser.cs | 12 +------- Source/VCExpr/VCExprAST.cs | 2 +- float_test.bpl | 16 +++++------ 8 files changed, 57 insertions(+), 74 deletions(-) diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 0c954f9a..d5a5efc9 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -695,10 +695,10 @@ namespace Microsoft.Boogie.AbstractInterpretation Lo = floor; Hi = ceiling; } else if (node.Val is BigFloat) { - BigInteger floor, ceiling; + BigNum floor, ceiling; ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling); - Lo = floor; - Hi = ceiling; + Lo = floor.ToBigInteger; + Hi = ceiling.ToBigInteger; } else if (node.Val is bool) { if ((bool)node.Val) { // true diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs index 8cde2cb9..a0ce03a5 100644 --- a/Source/Basetypes/BigFloat.cs +++ b/Source/Basetypes/BigFloat.cs @@ -129,7 +129,7 @@ namespace Microsoft.Basetypes this.exponentSize = exponentSize; this.exponent = exponent; this.significand = significand; - this.significandSize = significandSize; + this.significandSize = significandSize+1; this.isNeg = sign; this.value = ""; } @@ -141,33 +141,6 @@ namespace Microsoft.Basetypes this.significand = BigNum.ZERO; this.value = value; this.isNeg = value[0] == '-'; - //Special cases: - if (this.value.Equals("+oo") || this.value.Equals("-oo") || this.value.Equals("-zero")) - return; - if (this.value.ToLower().Equals("nan")) { - this.value = "NaN"; - return; - } - if (this.value.Equals("INF") || this.value.Equals("+INF")) - { - this.value = "+oo"; - return; - } - if (this.value.Equals("-INF")) - { - this.value = "-oo"; - return; - } - if (this.value.Equals("+zero")) - { - this.value = "0.0"; - return; - } - //End special cases - if (this.value.IndexOf('.') == -1 && this.value.IndexOf('e') == -1) - this.value += ".0"; //Assures that the decimal value is a "real" number - if (this.value.IndexOf('.') == 0) - this.value = "0" + this.value; //Assures that decimals always have a 0 in front } private BigNum maxsignificand() @@ -335,6 +308,18 @@ namespace Microsoft.Basetypes } } + 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 + ")"; + } + else { + return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")"; + } + } + [Pure] public string ToDecimalString() { Contract.Ensures(Contract.Result() != null); @@ -430,7 +415,7 @@ namespace Microsoft.Basetypes get { if (value == "") return false; - return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("-zero")); + return (value.Equals("NaN") || value.Equals("+oo") || value.Equals("-oo") || value.Equals("zero") || value.Equals("-zero")); } } diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 2345cc1e..fa038803 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -90,7 +90,7 @@ namespace Microsoft.Boogie { } } ExecutionEngine.ProcessFiles(fileList); - return 0; + return 0; END: if (CommandLineOptions.Clo.XmlSink != null) { diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index ad537288..6b2e1201 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.GetFloatType(v.ExponentSize, v.MantissaSize); + Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize); if (immutable) CachedHashCode = ComputeHashCode(); } @@ -639,7 +639,7 @@ namespace Microsoft.Boogie { return Type.Real; } else if (Val is BigFloat) { BigFloat temp = (BigFloat)Val; - return Type.GetFloatType(temp.ExponentSize, temp.MantissaSize); + return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize); } else if (Val is BvConst) { return Type.GetBvType(((BvConst)Val).Bits); } else { diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index bf35ccbe..77100d1c 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -669,7 +669,7 @@ private class BvBounds : Expr { } else if (la.kind == 98) { Get(); if (la.kind == 3) { - Expect(3); + Get(); switch (Int32.Parse(t.val)) { case 16: ty = new FloatType(t, 5, 11); @@ -689,13 +689,14 @@ private class BvBounds : Expr { } } else { - Expect(19); + Expect(19); //< Expect(3); int exp = Int32.Parse(t.val); + Expect(12); //, Expect(3); int man = Int32.Parse(t.val); ty = new FloatType(t, exp, man); - Expect(20); + Expect(20); //> } } else if (la.kind == 16) { Get(); @@ -1909,32 +1910,39 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { { if (la.kind == 97) { bool negative = false; - int exp, sig; + int exp, sig, size; BigNum exp_val, sig_val, value; - //Expected format = fp(sign exp_val sig_val) || fp(value) - Get(); //Skip the fp token - Get(); - if (t.val == "(") { + //Expected format = float(sign exp_val sig_val) || float(value) + Get(); //Skip the float token + if (la.val == "(") { Get(); + Expect(16); //bool negative = Boolean.Parse(t.val); + 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 (t.val == "<") { - Expect(14); + else if (la.val == "<") { + Get(); + Expect(3); exp = Int32.Parse(t.val); - Expect(14); + Expect(12); + Expect(3); sig = Int32.Parse(t.val); - int size; - BvLit(out value, out size); - if (size != exp + sig) - { - this.SemErr("The given bitvector size of " + size + "does not match the provided floating-point size of " + (exp + sig)); - n = BigFloat.ZERO(8, 24); - return; + Expect(20); //> + Expect(9); //( + if (la.kind == 4) { + Get(); + n = new BigFloat(t.val, exp, sig); + } + else { + BvLit(out value, out size); + n = new BigFloat(value.ToString(), exp, sig); } - n = new BigFloat(t.val, exp, sig); + Expect(10); //) } else { throw new FormatException(); diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 59b6b7e7..96d5b290 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -204,17 +204,7 @@ namespace Microsoft.Boogie.SMTLib else if (node is VCExprFloatLit) { BigFloat lit = ((VCExprFloatLit)node).Val; - if (lit.IsSpecialType) { - wr.Write("(_ " + lit.Decimal + " " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ")"); - return true; - } - wr.Write("((_ to_fp " + lit.ExponentSize.ToString() + " " + lit.SignificandSize.ToString() + ") RNE "); - 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(")"); + wr.Write("(" + lit.ToBVString() + ")"); } else { Contract.Assert(false); diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 3f6e3b7a..b22853ce 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -887,7 +887,7 @@ namespace Microsoft.Boogie.VCExprAST { { public readonly BigFloat Val; internal VCExprFloatLit(BigFloat val) - : base(Type.GetFloatType(val.ExponentSize, val.MantissaSize)) + : base(Type.GetFloatType(val.ExponentSize, val.SignificandSize)) { this.Val = val; } diff --git a/float_test.bpl b/float_test.bpl index fbf8e4e3..e893e098 100644 --- a/float_test.bpl +++ b/float_test.bpl @@ -1,13 +1,13 @@ //Translation from addsub_double_exact.c //Should Verify 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(10000000 11 53); - y := x + fp(1 11 53); - z := x - fp(1 11 53); + 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(2 11 53); + assert r == fp<11, 53> (2bv64); } \ No newline at end of file -- cgit v1.2.3