From 6f7fc01346c0ebe9072e61ace2cfede4fcedea09 Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 31 May 2016 12:08:07 -0600 Subject: Initial round of testing works with new syntax. Fixed an error where floating points could not be given as a function argument --- Source/Core/Parser.cs | 27 ++++++++++++------------ Source/Core/Scanner.cs | 2 +- float_test11.bpl | 57 ++++++++++++++++++++++++++++++++------------------ float_test13.bpl | 16 +++++++------- float_test14.bpl | 19 ++++++++++------- float_test2.bpl | 20 +++++++++++------- float_test3.bpl | 16 +++++++------- float_test4.bpl | 38 +++++++++++++++++++++------------ float_test5.bpl | 13 +++++++----- float_test8.bpl | 16 ++++++++------ 10 files changed, 134 insertions(+), 90 deletions(-) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 77100d1c..8161544f 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -668,9 +668,8 @@ private class BvBounds : Expr { ty = new BasicType(t, SimpleType.Real); } else if (la.kind == 98) { Get(); - if (la.kind == 3) { - Get(); - switch (Int32.Parse(t.val)) { + if (t.val.Length > 5) { + switch (Int32.Parse(t.val.Substring(5))) { case 16: ty = new FloatType(t, 5, 11); break; @@ -690,10 +689,10 @@ private class BvBounds : Expr { } else { Expect(19); //< - Expect(3); + Expect(3); //int int exp = Int32.Parse(t.val); Expect(12); //, - Expect(3); + Expect(3); //int int man = Int32.Parse(t.val); ty = new FloatType(t, exp, man); Expect(20); //> @@ -1830,14 +1829,14 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { break; } case 98: { - Get(); - x = t; - Expect(19); - Expression(out e); - Expect(20); - e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List { e }); - break; - } + Get(); + x = t; + Expect(19); + Expression(out e); + Expect(20); + e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToFloat), new List { e }); + break; + } case 9: { Get(); if (StartOf(9)) { @@ -2188,7 +2187,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { static readonly bool[,]/*!*/ set = { //grid is 17 x 100 {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, - {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x}, diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index bc294aba..ca7db1e1 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -509,7 +509,7 @@ public class Scanner { case "real": t.kind = 15; break; case "bool": t.kind = 16; break; case "fp": t.kind = 97; break; - case "float": t.kind = 98; break; + case "float": case "float16": case "float32": case "float64": case "float128": t.kind = 98; break; case "const": t.kind = 21; break; case "unique": t.kind = 22; break; case "extends": t.kind = 23; break; diff --git a/float_test11.bpl b/float_test11.bpl index cf9fd3a2..cee3e36e 100644 --- a/float_test11.bpl +++ b/float_test11.bpl @@ -1,38 +1,55 @@ //Translation from interpolation.c //Should Verify -//Returns inconclusize? What does that mean? +//Returns inconclusive? What does that mean? +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); procedure main() returns () { var i : int; - var z : float; - var t : float; - var min : [int] float; - var max : [int] float; + var z : float32; + var t : float32; + var min : [int] float32; + var max : [int] float32; - min[0] := fp(5); - min[1] := fp(10); - min[2] := fp(12); - min[3] := fp(30); - min[4] := fp(150); + min[0] := TO_FLOAT32_INT(5); + min[1] := TO_FLOAT32_INT(10); + min[2] := TO_FLOAT32_INT(12); + min[3] := TO_FLOAT32_INT(30); + min[4] := TO_FLOAT32_INT(150); - max[0] := fp(10); - max[1] := fp(12); - max[2] := fp(30); - max[3] := fp(150); - max[4] := fp(300); + max[0] := TO_FLOAT32_INT(10); + max[1] := TO_FLOAT32_INT(12); + max[2] := TO_FLOAT32_INT(30); + max[3] := TO_FLOAT32_INT(150); + max[4] := TO_FLOAT32_INT(300); havoc t; assume(t >= min[0] && t <= max[4]); i := 0; - while (i < 5) { - if (t <= max[i]) { - break; - } + //while (i < 5) { + //if (t <= max[i]) { + //break; + //} + //i := i + 1; + //} + + if (t > max[0]) { //1 + i := i + 1; + } + if (t > max[1]) { //2 + i := i + 1; + } + if (t > max[2]) { //3 + i := i + 1; + } + if (t > max[3]) { //4 + i := i + 1; + } + if (t > max[4]) { //5 i := i + 1; } z := (t - min[i]) / (max[i] - min[i]); - assert(z >= fp(0) && z <= fp(1)); + assert(z >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1)); } \ No newline at end of file diff --git a/float_test13.bpl b/float_test13.bpl index d073836d..e5402539 100644 --- a/float_test13.bpl +++ b/float_test13.bpl @@ -1,17 +1,19 @@ //Translation from inv_square_false-unreach-call.c //Should return an error (without crashing) +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); + procedure main() returns () { - var x : float; - var y : float; - var z : float; + var x : float32; + var y : float32; + var z : float32; havoc x; - assume(x >= fp(-1) && x <= fp(1)); + assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); - if (x != fp(0)) { + if (x != TO_FLOAT32_INT(0)) { y := x * x; - assert(y != fp(0)); - z := fp(1) / y; + assert(y != TO_FLOAT32_INT(0)); + z := TO_FLOAT32_INT(1) / y; } } \ No newline at end of file diff --git a/float_test14.bpl b/float_test14.bpl index 9b5dab0a..1505c361 100644 --- a/float_test14.bpl +++ b/float_test14.bpl @@ -1,17 +1,20 @@ -//Translation from inv_square_false-unreach-call.c +//Translation from inv_square_true-unreach-call.c //Should Verify +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32); + procedure main() returns () { - var x : float; - var y : float; - var z : float; + var x : float32; + var y : float32; + var z : float32; havoc x; - assume(x >= fp(-1) && x <= fp(1)); + assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); - if (x <= fp(-.00000000000000000001) || x >= fp(.00000000000000000001)) { + if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) { y := x * x; - assert(y != fp(0)); - z := fp(1) / y; + assert(y != TO_FLOAT32_INT(0)); + z := TO_FLOAT32_INT(1) / y; } } \ No newline at end of file diff --git a/float_test2.bpl b/float_test2.bpl index da74909b..d78c339d 100644 --- a/float_test2.bpl +++ b/float_test2.bpl @@ -1,13 +1,17 @@ //Translation from addsub_float_exact.c //Should Verify + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32); + procedure main() returns () { - var x : float; - var y : float; - var z : float; - var r : float; - x := fp(1000000); - y := x + fp(1); - z := x - fp(1); + var x : float32; + var y : float32; + var z : float32; + var r : float32; + x := TO_FLOAT32_REAL(1e7); + y := x + TO_FLOAT32_INT(1); + z := x - TO_FLOAT32_INT(1); r := y - z; - assert r == fp(2); + assert r == TO_FLOAT32_INT(2); } \ No newline at end of file diff --git a/float_test3.bpl b/float_test3.bpl index dd0c1ba4..67c6ba48 100644 --- a/float_test3.bpl +++ b/float_test3.bpl @@ -1,13 +1,13 @@ //Translation from addsub_float_inexact.c //Should give an error procedure main() returns () { - var x : float; - var y : float; - var z : float; - var r : float; - x := fp(10000000); - y := x + fp(1); - z := x - fp(1); + var x : float32; + var y : float32; + var z : float32; + var r : float32; + x := fp<8, 24>(3221225472bv32); + y := x + fp<8, 24>(1bv32); + z := x - fp<8, 24>(1bv32); r := y - z; - assert r == fp(0); + assert r == fp<8, 24>(2bv32); } \ No newline at end of file diff --git a/float_test4.bpl b/float_test4.bpl index a7aa8c4b..a31aa215 100644 --- a/float_test4.bpl +++ b/float_test4.bpl @@ -1,20 +1,32 @@ //Translation from drift_tenth.c -//Should Verify -//FAILS; note that it succeeds when tick == fp(.1) +//Should Fail + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32); procedure main() returns () { - var tick : float; - var time : float; + var tick : float32; + var time : float32; var i: int; - tick := fp(1)/fp(10); - time := fp(0); + tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10); + time := TO_FLOAT32_INT(0); - i := 0; - while (i < 10) - { - time := time + tick; - i := i + 1; - } - assert(time == fp(1)); + //i := 0; + //while (i < 10) + //{ + // time := time + tick; + // i := i + 1; + //} + time := time + tick;//1 + time := time + tick;//2 + time := time + tick;//3 + time := time + tick;//4 + time := time + tick;//5 + time := time + tick;//6 + time := time + tick;//7 + time := time + tick;//8 + time := time + tick;//9 + time := time + tick;//10 + assert time == TO_FLOAT32_INT(1); } \ No newline at end of file diff --git a/float_test5.bpl b/float_test5.bpl index ce5d2bc7..7536f8fd 100644 --- a/float_test5.bpl +++ b/float_test5.bpl @@ -1,15 +1,18 @@ //Translation from filter1.c //Should Verify +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); + procedure main() returns () { - var E0 : float(11 53); - var E1 : float(11 53); - var S : float(11 53); + var E0 : float64; + var E1 : float64; + var S : float64); var i : int; var rand : int; - E1 := fp(0 11 53); - S := fp(0 11 53); + E1 := TO_FLOAT64_INT(0); + S := TO_FLOAT64_INT(0); i := 0; while (i <= 1000000) diff --git a/float_test8.bpl b/float_test8.bpl index 995ed4fa..7e78e206 100644 --- a/float_test8.bpl +++ b/float_test8.bpl @@ -1,12 +1,16 @@ //Translation from float_double.c //Should Verify -//FAILS: I don't have this functionality yet... + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); procedure main() returns () { - var x : float(11 53); - var y : float; + var x : float64; + var y : float32; - x := fp(100000000000000000001 11 53); - y := x; - assert(x != y); + x := TO_FLOAT64_REAL(1e20)+TO_FLOAT64_INT(1); + y := TO_FLOAT32_FLOAT64(x); + assert x != TO_FLOAT64_FLOAT32(y); } \ No newline at end of file -- cgit v1.2.3