From ea068f2bddb4be2eb4827f75418f46f52fd3a1f9 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Fri, 17 Apr 2015 11:55:39 -0600 Subject: Added the fp32 class, copied from the previously existing BigDec class. No significant changes from BigDec have been made --- Binaries/Boogie.vshost.exe.manifest | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 Binaries/Boogie.vshost.exe.manifest (limited to 'Binaries/Boogie.vshost.exe.manifest') diff --git a/Binaries/Boogie.vshost.exe.manifest b/Binaries/Boogie.vshost.exe.manifest new file mode 100644 index 00000000..061c9ca9 --- /dev/null +++ b/Binaries/Boogie.vshost.exe.manifest @@ -0,0 +1,11 @@ + + + + + + + + + + + -- cgit v1.2.3 From 28a20e6eba2919e008f70874b4c12a3ce7ad049c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Thu, 17 Sep 2015 03:14:27 -0600 Subject: Added initial support for float addition --- Binaries/Boogie.vshost.exe.manifest | 22 ++++++------ Source/Basetypes/BigFloat.cs | 12 +++---- Source/Core/AbsyExpr.cs | 16 ++++----- Source/Core/Parser.cs | 4 +-- Source/Provers/SMTLib/SMTLibProcess.cs | 1 + Source/Provers/SMTLib/Z3.cs | 4 +-- Source/VCExpr/VCExprAST.cs | 62 ++++++++++++++++++++++++++++++++-- Source/VCExpr/VCExprASTVisitors.cs | 1 - float_test5.bpl | 4 +-- 9 files changed, 89 insertions(+), 37 deletions(-) (limited to 'Binaries/Boogie.vshost.exe.manifest') diff --git a/Binaries/Boogie.vshost.exe.manifest b/Binaries/Boogie.vshost.exe.manifest index 061c9ca9..f96b1d6b 100644 --- a/Binaries/Boogie.vshost.exe.manifest +++ b/Binaries/Boogie.vshost.exe.manifest @@ -1,11 +1,11 @@ - - - - - - - - - - - + + + + + + + + + + + diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs index 1fb05005..33860a4f 100644 --- a/Source/Basetypes/BigFloat.cs +++ b/Source/Basetypes/BigFloat.cs @@ -17,7 +17,7 @@ namespace Microsoft.Basetypes /// /// A representation of a 32-bit floating point value - /// Note that this value has a 1-bit sign, 8-bit exponent, and 23-bit mantissa + /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit mantissa /// public struct BigFloat { @@ -85,17 +85,17 @@ namespace Microsoft.Basetypes [Pure] public static BigFloat FromInt(int v) { - return new BigFloat(v, 0, 23, 8); //TODO: modify for correct fp representation + return new BigFloat(v, 0, 24, 8); //TODO: modify for correct fp representation } [Pure] public static BigFloat FromBigInt(BIM v) { - return new BigFloat(0, v, 8, 23); //TODO: modify for correct fp representation + return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation } public static BigFloat FromBigDec(BIM v) { - return new BigFloat(0, v, 8, 23); //TODO: modify for correct fp representation + return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation } [Pure] @@ -107,9 +107,9 @@ namespace Microsoft.Basetypes { switch (vals.Length) { case 1: - return Round(vals[0], 8, 23); + return Round(vals[0], 8, 24); case 2: - return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 23); + return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24); case 3: return Round(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2])); case 4: diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 7e7ed10a..181076a7 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1519,8 +1519,6 @@ namespace Microsoft.Boogie { return "mod"; case Opcode.RealDiv: return "/"; - case Opcode.FloatDiv: - return "/"; case Opcode.Pow: return "**"; case Opcode.Eq: @@ -1583,10 +1581,6 @@ namespace Microsoft.Boogie { opBindingStrength = 0x50; fragileRightContext = true; break; - case Opcode.FloatDiv: //TODO: Modify (potentially) - opBindingStrength = 0x50; - fragileRightContext = true; - break; case Opcode.Pow: opBindingStrength = 0x60; fragileRightContext = true; @@ -1707,10 +1701,12 @@ 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.IsFloat && arg0type.Unify(arg1type)) { + return new FloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); + } + if (arg1type.IsFloat && arg1type.Unify(arg0type)) { + return new FloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); + } goto BAD_TYPE; case Opcode.Div: case Opcode.Mod: diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 2550c334..889d7be8 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -678,7 +678,7 @@ private class BvBounds : Expr { Expect(10); } else - ty = new FloatType(t, 8, 23); + ty = new FloatType(t, 8, 24); } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Bool); @@ -1914,7 +1914,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { catch (FormatException) { this.SemErr("incorrectly formatted floating point"); - n = BigFloat.ZERO(8, 23); + n = BigFloat.ZERO(8, 24); } } diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 4a1331c5..4982d81e 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); toProver.WriteLine(cmd); } diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 250e04c9..8e8b2d55 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", "true"); + options.AddWeakSmtOption("TYPE_CHECK", "false"); 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", "true"); + options.AddWeakSmtOption("TYPE_CHECK", "false"); options.AddWeakSmtOption("BV_REFLECT", "true"); if (options.TimeLimit > 0) diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 36692f30..c44800fc 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -357,6 +357,15 @@ namespace Microsoft.Boogie { return new VCExprBoogieFunctionOp(func); } + // Float nodes + + public VCExpr AddFOp(VCExpr f1, VCExpr f2) + { + Contract.Requires(f1 != null); + Contract.Requires(f2 != null); + return Function(new VCExprFloatOp(f1.Type.FloatExponent, f1.Type.FloatMantissa)); + } + // Bitvector nodes public VCExpr Bitvector(BvConst bv) { @@ -403,7 +412,6 @@ namespace Microsoft.Boogie { DivOp, ModOp, RealDivOp, - FloatDivOp, PowOp, LtOp, LeOp, @@ -1309,8 +1317,6 @@ namespace Microsoft.Boogie.VCExprAST { return visitor.VisitModOp(expr, arg); case VCExpressionGenerator.SingletonOp.RealDivOp: return visitor.VisitRealDivOp(expr, arg); - case VCExpressionGenerator.SingletonOp.FloatDivOp: - return visitor.VisitFloatDivOp(expr, arg); case VCExpressionGenerator.SingletonOp.PowOp: return visitor.VisitPowOp(expr, arg); case VCExpressionGenerator.SingletonOp.LtOp: @@ -1668,6 +1674,56 @@ namespace Microsoft.Boogie.VCExprAST { } } + ///////////////////////////////////////////////////////////////////////////////// + // Float operators + + public class VCExprFloatOp : VCExprOp { + public readonly int Mantissa; + public readonly int Exponent; + + public override int Arity { + get { + return 1; + } + } + public override int TypeParamArity { + get { + return 0; + } + } + public override Type InferType(List args, List/*!*/ typeArgs) { + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); + Contract.Ensures(Contract.Result() != null); + return Type.GetFloatType(Exponent, Mantissa); + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + 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; + return false; + } + [Pure] + public override int GetHashCode() { + return Exponent * 81748912 + Mantissa * 67867979; + } + + internal VCExprFloatOp(int exp, int man) { + this.Exponent = exp; + this.Mantissa = man; + } + public override Result Accept + (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); + return visitor.VisitBvOp(expr, arg); + } + } + ///////////////////////////////////////////////////////////////////////////////// // Bitvector operators diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 1bcce113..a1fb2ff4 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -77,7 +77,6 @@ namespace Microsoft.Boogie.VCExprAST { Result VisitDivOp(VCExprNAry node, Arg arg); Result VisitModOp(VCExprNAry node, Arg arg); Result VisitRealDivOp(VCExprNAry node, Arg arg); - Result VisitFloatDivOp(VCExprNAry node, Arg arg); //TODO: Add this to references from above and below Result VisitPowOp(VCExprNAry node, Arg arg); Result VisitLtOp(VCExprNAry node, Arg arg); Result VisitLeOp(VCExprNAry node, Arg arg); diff --git a/float_test5.bpl b/float_test5.bpl index 2f565b27..c3d279f2 100644 --- a/float_test5.bpl +++ b/float_test5.bpl @@ -1,5 +1,5 @@ procedure F() returns () { var x : float; - x := fp (0 0); - assert x == fp (0 0 8 30); + var y : float; + assert x + y == fp(0); } \ No newline at end of file -- cgit v1.2.3 From 0c22f92b10430cd70507649b1fdae62eaffac0c9 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:40:06 -0600 Subject: minor changes --- Binaries/Boogie.vshost.exe.manifest | 22 +++++++++++----------- Test/floats/float1.bpl.expect | 4 ++-- Test/floats/float12.bpl.expect | 4 ++-- 3 files changed, 15 insertions(+), 15 deletions(-) (limited to 'Binaries/Boogie.vshost.exe.manifest') diff --git a/Binaries/Boogie.vshost.exe.manifest b/Binaries/Boogie.vshost.exe.manifest index f96b1d6b..061c9ca9 100644 --- a/Binaries/Boogie.vshost.exe.manifest +++ b/Binaries/Boogie.vshost.exe.manifest @@ -1,11 +1,11 @@ - - - - - - - - - - - + + + + + + + + + + + diff --git a/Test/floats/float1.bpl.expect b/Test/floats/float1.bpl.expect index 6abb715b..37fad75c 100644 --- a/Test/floats/float1.bpl.expect +++ b/Test/floats/float1.bpl.expect @@ -1,2 +1,2 @@ - -Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float12.bpl.expect b/Test/floats/float12.bpl.expect index 6abb715b..37fad75c 100644 --- a/Test/floats/float12.bpl.expect +++ b/Test/floats/float12.bpl.expect @@ -1,2 +1,2 @@ - -Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors -- cgit v1.2.3