summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/AbsInt/IntervalDomain.cs6
-rw-r--r--Source/Basetypes/BigFloat.cs43
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs2
-rw-r--r--Source/Core/AbsyExpr.cs4
-rw-r--r--Source/Core/Parser.cs46
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs12
-rw-r--r--Source/VCExpr/VCExprAST.cs2
-rw-r--r--float_test.bpl16
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<string>() != 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<exp sig>(value)
- Get(); //Skip the fp token
- Get();
- if (t.val == "(") {
+ //Expected format = float(sign exp_val sig_val) || float<exp sig>(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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 10:15:43 +0000