From 5cff8cd77c629ec8e48a2498b1e704173306586a Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 21:09:06 -0600 Subject: finished testing, fixed several minor compiler bugs --- Source/Basetypes/BigFloat.cs | 2 +- Source/Core/Parser.cs | 82 ++++++++++++++++++++-------------- Source/Provers/SMTLib/SMTLibProcess.cs | 2 +- Test/floats/float0.bpl | 14 ++++++ Test/floats/float0.bpl.expect | 8 ++++ Test/floats/float1.bpl | 13 ++++++ Test/floats/float1.bpl.expect | 2 + Test/floats/float10.bpl | 18 ++++++++ Test/floats/float10.bpl.expect | 5 +++ Test/floats/float11.bpl | 22 +++++++++ Test/floats/float11.bpl.expect | 7 +++ Test/floats/float12.bpl | 16 +++++++ Test/floats/float12.bpl.expect | 2 + Test/floats/float13.bpl | 23 ++++++++++ Test/floats/float14.bpl | 17 +++++++ Test/floats/float15.bpl | 36 +++++++++++++++ Test/floats/float16.bpl | 40 +++++++++++++++++ Test/floats/float17.bpl | 38 ++++++++++++++++ Test/floats/float18.bpl | 16 +++++++ Test/floats/float19.bpl | 34 ++++++++++++++ Test/floats/float2.bpl | 15 +++++++ Test/floats/float2.bpl.expect | 7 +++ Test/floats/float20.bpl | 14 ++++++ Test/floats/float21.bpl | 35 +++++++++++++++ Test/floats/float22.bpl | 20 +++++++++ Test/floats/float23.bpl | 8 ++++ Test/floats/float3.bpl | 27 +++++++++++ Test/floats/float3.bpl.expect | 2 + Test/floats/float4.bpl | 11 +++++ Test/floats/float4.bpl.expect | 2 + Test/floats/float5.bpl | 24 ++++++++++ Test/floats/float5.bpl.expect | 9 ++++ Test/floats/float6.bpl | 50 +++++++++++++++++++++ Test/floats/float6.bpl.expect | 2 + Test/floats/float7.bpl | 13 ++++++ Test/floats/float7.bpl.expect | 2 + Test/floats/float8.bpl | 13 ++++++ Test/floats/float8.bpl.expect | 5 +++ Test/floats/float9.bpl | 17 +++++++ Test/floats/float9.bpl.expect | 2 + Test/floats/modpath.py | 13 ++++++ Test/floats/test1.bpl | 13 ------ Test/floats/test10.bpl | 20 --------- Test/floats/test11.bpl | 55 ----------------------- Test/floats/test12.bpl | 43 ------------------ Test/floats/test13.bpl | 19 -------- Test/floats/test14.bpl | 20 --------- Test/floats/test15.bpl | 24 ---------- Test/floats/test16.bpl | 8 ---- Test/floats/test17.bpl | 11 ----- Test/floats/test18.bpl | 36 --------------- Test/floats/test19.bpl | 36 --------------- Test/floats/test2.bpl | 17 ------- Test/floats/test20.bpl | 14 ------ Test/floats/test3.bpl | 13 ------ Test/floats/test4.bpl | 32 ------------- Test/floats/test5.bpl | 36 --------------- Test/floats/test6.bpl | 40 ----------------- Test/floats/test7.bpl | 38 ---------------- Test/floats/test8.bpl | 16 ------- Test/floats/test9.bpl | 34 -------------- 61 files changed, 653 insertions(+), 560 deletions(-) create mode 100644 Test/floats/float0.bpl create mode 100644 Test/floats/float0.bpl.expect create mode 100644 Test/floats/float1.bpl create mode 100644 Test/floats/float1.bpl.expect create mode 100644 Test/floats/float10.bpl create mode 100644 Test/floats/float10.bpl.expect create mode 100644 Test/floats/float11.bpl create mode 100644 Test/floats/float11.bpl.expect create mode 100644 Test/floats/float12.bpl create mode 100644 Test/floats/float12.bpl.expect create mode 100644 Test/floats/float13.bpl create mode 100644 Test/floats/float14.bpl create mode 100644 Test/floats/float15.bpl create mode 100644 Test/floats/float16.bpl create mode 100644 Test/floats/float17.bpl create mode 100644 Test/floats/float18.bpl create mode 100644 Test/floats/float19.bpl create mode 100644 Test/floats/float2.bpl create mode 100644 Test/floats/float2.bpl.expect create mode 100644 Test/floats/float20.bpl create mode 100644 Test/floats/float21.bpl create mode 100644 Test/floats/float22.bpl create mode 100644 Test/floats/float23.bpl create mode 100644 Test/floats/float3.bpl create mode 100644 Test/floats/float3.bpl.expect create mode 100644 Test/floats/float4.bpl create mode 100644 Test/floats/float4.bpl.expect create mode 100644 Test/floats/float5.bpl create mode 100644 Test/floats/float5.bpl.expect create mode 100644 Test/floats/float6.bpl create mode 100644 Test/floats/float6.bpl.expect create mode 100644 Test/floats/float7.bpl create mode 100644 Test/floats/float7.bpl.expect create mode 100644 Test/floats/float8.bpl create mode 100644 Test/floats/float8.bpl.expect create mode 100644 Test/floats/float9.bpl create mode 100644 Test/floats/float9.bpl.expect create mode 100644 Test/floats/modpath.py delete mode 100644 Test/floats/test1.bpl delete mode 100644 Test/floats/test10.bpl delete mode 100644 Test/floats/test11.bpl delete mode 100644 Test/floats/test12.bpl delete mode 100644 Test/floats/test13.bpl delete mode 100644 Test/floats/test14.bpl delete mode 100644 Test/floats/test15.bpl delete mode 100644 Test/floats/test16.bpl delete mode 100644 Test/floats/test17.bpl delete mode 100644 Test/floats/test18.bpl delete mode 100644 Test/floats/test19.bpl delete mode 100644 Test/floats/test2.bpl delete mode 100644 Test/floats/test20.bpl delete mode 100644 Test/floats/test3.bpl delete mode 100644 Test/floats/test4.bpl delete mode 100644 Test/floats/test5.bpl delete mode 100644 Test/floats/test6.bpl delete mode 100644 Test/floats/test7.bpl delete mode 100644 Test/floats/test8.bpl delete mode 100644 Test/floats/test9.bpl diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs index a0ce03a5..3c4cc40a 100644 --- a/Source/Basetypes/BigFloat.cs +++ b/Source/Basetypes/BigFloat.cs @@ -313,7 +313,7 @@ namespace Microsoft.Basetypes 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 + ")"; + return "fp (_ bv" + (this.isNeg ? "1" : "0") + " 1) (_ bv" + this.exponent + " " + this.exponentSize + ") (_ bv" + this.significand + " " + (this.significandSize-1) + ")"; } else { return "(_ to_fp " + this.exponentSize + " " + this.significandSize + ") (_ bv" + this.value + " " + (this.exponentSize + this.significandSize).ToString() + ")"; diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 8161544f..7982f594 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -668,35 +668,7 @@ private class BvBounds : Expr { ty = new BasicType(t, SimpleType.Real); } else if (la.kind == 98) { Get(); - if (t.val.Length > 5) { - switch (Int32.Parse(t.val.Substring(5))) { - case 16: - ty = new FloatType(t, 5, 11); - break; - case 32: - ty = new FloatType(t, 8, 24); - break; - case 64: - ty = new FloatType(t, 11, 53); - break; - case 128: - ty = new FloatType(t, 15, 113); - break; - default: - SynErr(3); - break; - } - } - else { - Expect(19); //< - Expect(3); //int - int exp = Int32.Parse(t.val); - Expect(12); //, - Expect(3); //int - int man = Int32.Parse(t.val); - ty = new FloatType(t, exp, man); - Expect(20); //> - } + ty = FType(); } else if (la.kind == 16) { Get(); ty = new BasicType(t, SimpleType.Bool); @@ -707,6 +679,39 @@ private class BvBounds : Expr { } else SynErr(101); } + FloatType FType() { + if (t.val.Length > 5) { + switch (Int32.Parse(t.val.Substring(5))) { + case 16: + return new FloatType(t, 5, 11); + case 32: + return new FloatType(t, 8, 24); + case 64: + return new FloatType(t, 11, 53); + case 128: + return new FloatType(t, 15, 113); + default: + SynErr(3); + return new FloatType(t, 0, 0); + } + } + else { + try { + Expect(19); //< + Expect(3); //int + int exp = Int32.Parse(t.val); + Expect(12); //, + Expect(3); //int + int man = Int32.Parse(t.val); + Expect(20); //> + return new FloatType(t, exp, man); + } + catch (Exception) { + return new FloatType(t, 0, 0); + } + } + } + void Ident(out IToken/*!*/ x) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); Expect(1); @@ -1915,8 +1920,13 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Get(); //Skip the float token if (la.val == "(") { Get(); - Expect(16); //bool - negative = Boolean.Parse(t.val); + if (la.val == "false") + negative = false; + else if (la.val == "true") + negative = true; + else + throw new FormatException(); + Get(); Expect(12); //, BvLit(out exp_val, out exp); Expect(12); @@ -1933,10 +1943,16 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { sig = Int32.Parse(t.val); Expect(20); //> Expect(9); //( - if (la.kind == 4) { + if (la.kind == 1) { //NaN Get(); n = new BigFloat(t.val, exp, sig); } + else if (la.kind == 74 || la.kind == 75) { //+ or - + Get(); + String s = t.val; + Get(); + n = new BigFloat(s + t.val, exp, sig); + } else { BvLit(out value, out size); n = new BigFloat(value.ToString(), exp, sig); @@ -2194,7 +2210,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { {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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,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,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,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,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,T,T,T, x,T,T,x, x,T,x,x, x,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, 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,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,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, 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,T, x,x,x,x, T,T,T,T, T,T,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,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,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,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,T,T,T, T,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}, diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 4982d81e..bc94e253 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -93,7 +93,7 @@ namespace Microsoft.Boogie.SMTLib log = log.Replace("\r", "").Replace("\n", " "); Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log); } - Console.WriteLine(cmd); + //Console.WriteLine(cmd); toProver.WriteLine(cmd); } diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl new file mode 100644 index 00000000..b1a240be --- /dev/null +++ b/Test/floats/float0.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : real) returns (r : float<8, 24>) +{ + r := 15; // Error + r := 15.0; // Error + r := fp(false, 1bv8, 0bv22); // Error + r := fp<8, 23>(1bv31); // Error + r := x; // Error + r := fp<8, 23>(1bv31) + fp<8, 23>(1bv31); // Error + r := fp<8, 24>(1bv32) + fp<8, 23>(1bv31); // Error + + return; +} \ No newline at end of file diff --git a/Test/floats/float0.bpl.expect b/Test/floats/float0.bpl.expect new file mode 100644 index 00000000..4c934700 --- /dev/null +++ b/Test/floats/float0.bpl.expect @@ -0,0 +1,8 @@ +float0.bpl(5,1): Error: mismatched types in assignment command (cannot assign int to float (8 24)) +float0.bpl(6,1): Error: mismatched types in assignment command (cannot assign real to float (8 24)) +float0.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24)) +float0.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24)) +float0.bpl(9,1): Error: mismatched types in assignment command (cannot assign real to float (8 24)) +float0.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24)) +float0.bpl(11,23): Error: invalid argument types (float (8 24) and float (8 23)) to binary operator + +7 type checking errors detected in float0.bpl diff --git a/Test/floats/float1.bpl b/Test/floats/float1.bpl new file mode 100644 index 00000000..9ed62579 --- /dev/null +++ b/Test/floats/float1.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : float<8, 24>) returns (r : float<8, 24>) +{ + r := fp(false, 1bv8, 0bv23); + r := fp<8, 24>(1bv32); + r := x; + r := x + fp<8, 24>(1bv32); + r := fp<8, 24>(1bv32) + fp<8, 24>(1bv32); + assert(r == fp<8, 24>(2bv32)); + + return; +} \ No newline at end of file diff --git a/Test/floats/float1.bpl.expect b/Test/floats/float1.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float10.bpl b/Test/floats/float10.bpl new file mode 100644 index 00000000..bf07aec6 --- /dev/null +++ b/Test/floats/float10.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64); + +procedure double_range_true() returns () { + var x : float64; + havoc x; + if (x >= TO_FLOAT64_REAL(-1e307) && x <= TO_FLOAT64_REAL(1e307)) { + assert(x==x); + } +} + +procedure double_range_false() returns () { + var x : float64; + havoc x; + assert(x==x); +} \ No newline at end of file diff --git a/Test/floats/float10.bpl.expect b/Test/floats/float10.bpl.expect new file mode 100644 index 00000000..cae8d781 --- /dev/null +++ b/Test/floats/float10.bpl.expect @@ -0,0 +1,5 @@ +float10.bpl(17,2): Error BP5001: This assertion might not hold. +Execution trace: + float10.bpl(16,2): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/floats/float11.bpl b/Test/floats/float11.bpl new file mode 100644 index 00000000..424c5a2d --- /dev/null +++ b/Test/floats/float11.bpl @@ -0,0 +1,22 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +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 : float32; + var time : float32; + var i: int; + + 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 == TO_FLOAT32_INT(1); +} \ No newline at end of file diff --git a/Test/floats/float11.bpl.expect b/Test/floats/float11.bpl.expect new file mode 100644 index 00000000..19e55fef --- /dev/null +++ b/Test/floats/float11.bpl.expect @@ -0,0 +1,7 @@ +..\Test\floats\float11.bpl(21,2): Error BP5001: This assertion might not hold. +Execution trace: + ..\Test\floats\float11.bpl(12,7): anon0 + ..\Test\floats\float11.bpl(16,2): anon3_LoopHead + ..\Test\floats\float11.bpl(16,2): anon3_LoopDone + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/floats/float12.bpl b/Test/floats/float12.bpl new file mode 100644 index 00000000..349abb41 --- /dev/null +++ b/Test/floats/float12.bpl @@ -0,0 +1,16 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +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 : float64; + var y : float32; + + 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 diff --git a/Test/floats/float12.bpl.expect b/Test/floats/float12.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float12.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float13.bpl b/Test/floats/float13.bpl new file mode 100644 index 00000000..4fe25140 --- /dev/null +++ b/Test/floats/float13.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +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 : float64; + var y : float64; + + havoc x; + assume(x >= TO_FLOAT64_INT(0) && x <= TO_FLOAT64_INT(10)); + + y := x*x - x; + if (y >= TO_FLOAT64_INT(0)) { + y := x / TO_FLOAT64_INT(10); + } + else { + y := x*x + TO_FLOAT64_INT(2); + } + + assert(y >= TO_FLOAT64_INT(0) && y <= TO_FLOAT64_INT(105)); +} \ No newline at end of file diff --git a/Test/floats/float14.bpl b/Test/floats/float14.bpl new file mode 100644 index 00000000..46c1b07d --- /dev/null +++ b/Test/floats/float14.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +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 : float64; + var y : float64; + var r : float64; + + x := TO_FLOAT64_INT(77617); + y := TO_FLOAT64_INT(33096); + r := y*y*y*y*y*y * TO_FLOAT64_REAL(333.75) + x*x * (x*x*y*y*TO_FLOAT64_INT(11) - y*y*y*y*y*y - y*y*y*y * TO_FLOAT64_INT(121) - TO_FLOAT64_INT(2)) + y*y*y*y*y*y*y*y * TO_FLOAT64_REAL(5.5) + x / (y*TO_FLOAT64_INT(2)); + + assert(r >= TO_FLOAT64_INT(0)); +} \ No newline at end of file diff --git a/Test/floats/float15.bpl b/Test/floats/float15.bpl new file mode 100644 index 00000000..7536f8fd --- /dev/null +++ b/Test/floats/float15.bpl @@ -0,0 +1,36 @@ +//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 : float64; + var E1 : float64; + var S : float64); + var i : int; + var rand : int; + + E1 := TO_FLOAT64_INT(0); + S := TO_FLOAT64_INT(0); + + i := 0; + while (i <= 1000000) + { + havoc E0; + assume(E0 >= fp(-1 11 53) && E0 <= fp(1 11 53)); + + havoc rand; + if (rand != 0) { + S := fp(0 11 53); + } + else { + S := fp(0.999 11 53) * S + E0 - E1; + } + E1 := E0; + + //assert(1==0); + assert(S >= fp(-1 11 53) && S <= fp(1 11 53)); + i := i + 1; + } +} \ No newline at end of file diff --git a/Test/floats/float16.bpl b/Test/floats/float16.bpl new file mode 100644 index 00000000..6bef1137 --- /dev/null +++ b/Test/floats/float16.bpl @@ -0,0 +1,40 @@ +//Translation from filter2.c +//Should give an error +//FAILS; doesn't generate terms! + +procedure main() returns () { + var E : float(11 53); + var E0 : float(11 53); + var E1 : float(11 53); + var S : float(11 53); + var S0 : float(11 53); + var S1 : float(11 53); + var i: int; + + havoc E; + havoc E0; + assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53)); + assume(E0 >= fp(0.0 11 53) && E0 <= fp(1.0 11 53)); + + E1 := fp(0.0 11 53); + S1 := fp(0.0 11 53); + S0 := fp(0.0 11 53); + S := fp(0.0 11 53); + + i := 0; +// while (i <= 1000000) +// { + E1 := E0; + E0 := E; + + havoc E; + assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53)); + + S1 := S0; + S0 := S; + S := E*fp(0.7 11 53) - E0*fp(1.3 11 53) + E1*fp(1.1 11 53) + S0*fp(1.4 11 53) - S1*fp(0.7 11 53); + + assert(S >= fp(-4.0 11 53) && S <= fp(4.0 11 53)); + //i := i + 1; +// } +} \ No newline at end of file diff --git a/Test/floats/float17.bpl b/Test/floats/float17.bpl new file mode 100644 index 00000000..8e07878d --- /dev/null +++ b/Test/floats/float17.bpl @@ -0,0 +1,38 @@ +//Translation from filter2.c +//Should give an error +//Same as the previous one; it works with reals! + +procedure main() returns () { + var E : real; + var E0 : real; + var E1 : real; + var S : real; + var S0 : real; + var S1 : real; + var i: int; + + havoc E; + havoc E0; + assume(E >= 0.0 && E <= 1.0); + assume(E0 >= 0.0 && E0 <= 1.0); + + S0 := 0.0; + S := 0.0; + + i := 0; + while (i <= 1000000) + { + E1 := E0; + E0 := E; + + havoc E; + assume(E >= 0.0 && E <= 1.0); + + S1 := S0; + S0 := S; + S := E*0.7 - E0*1.3 + E1*1.1 + S0*1.4 - S1*0.7; + + assert(S >= -4.0 && S <= 4.0); + i := i + 1; + } +} \ No newline at end of file diff --git a/Test/floats/float18.bpl b/Test/floats/float18.bpl new file mode 100644 index 00000000..7e78e206 --- /dev/null +++ b/Test/floats/float18.bpl @@ -0,0 +1,16 @@ +//Translation from float_double.c +//Should Verify + +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 : float64; + var y : float32; + + 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 diff --git a/Test/floats/float19.bpl b/Test/floats/float19.bpl new file mode 100644 index 00000000..c3a42e6b --- /dev/null +++ b/Test/floats/float19.bpl @@ -0,0 +1,34 @@ +//Translation from feedback_diverge.c +//Should give an error +//Not sure on this one... + +procedure main() returns () { + var A : float; + var B : float; + var X : float; + var i : int; + var rand : int; + + A := fp(0); + B := fp(0); + + i := 0; + while (i < 3600000) { + + havoc rand; + if (rand != 0) { + havoc X; + assume(X >= fp(-20) && X <= fp(20)); + } + else { + X := B; + } + + B := B - (B * fp(2.0) - A - X) * fp(.005); + A := X; + + i := i + 1; + } + + assert(A >= fp(-100) && A <= fp(100)); +} \ No newline at end of file diff --git a/Test/floats/float2.bpl b/Test/floats/float2.bpl new file mode 100644 index 00000000..1a4d02cd --- /dev/null +++ b/Test/floats/float2.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : float16) returns(r : float32) { + var y : float64; + var z : float128; + + r := x; // Error + r := y; // Error + r := z; // Error + y := x; // Error + y := z; // Error + z := x; // Error + + return; +} \ No newline at end of file diff --git a/Test/floats/float2.bpl.expect b/Test/floats/float2.bpl.expect new file mode 100644 index 00000000..62348741 --- /dev/null +++ b/Test/floats/float2.bpl.expect @@ -0,0 +1,7 @@ +float2.bpl(7,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (8 24)) +float2.bpl(8,1): Error: mismatched types in assignment command (cannot assign float (11 53) to float (8 24)) +float2.bpl(9,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (8 24)) +float2.bpl(10,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (11 53)) +float2.bpl(11,1): Error: mismatched types in assignment command (cannot assign float (15 113) to float (11 53)) +float2.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (5 11) to float (15 113)) +6 type checking errors detected in float2.bpl diff --git a/Test/floats/float20.bpl b/Test/floats/float20.bpl new file mode 100644 index 00000000..57c605fd --- /dev/null +++ b/Test/floats/float20.bpl @@ -0,0 +1,14 @@ +//Should return an error? +//Translation from Rump_double.c + +procedure main() returns () { + var x : float(11 53); + var y : float(11 53); + var r : float(11 53); + + x := fp(77617 11 53); + y := fp(33096 11 53); + r := y*y*y*y*y*y * fp(333.75 11 53) + x*x * (x*x*y*y*fp(11 11 53) - y*y*y*y*y*y - y*y*y*y * fp(121 11 53) - fp(2 11 53)) + y*y*y*y*y*y*y*y * fp(5.5 11 53) + x / (y*fp(2 11 53)); + + assert(r >= fp(0 11 53)); +} \ No newline at end of file diff --git a/Test/floats/float21.bpl b/Test/floats/float21.bpl new file mode 100644 index 00000000..5fad5859 --- /dev/null +++ b/Test/floats/float21.bpl @@ -0,0 +1,35 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +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 : float32; + var y : float32; + var z : float32; + + havoc x; + assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); + + if (x != TO_FLOAT32_INT(0)) { + y := x * x; + assert(y != TO_FLOAT32_INT(0)); + z := TO_FLOAT32_INT(1) / y; + } +} + +procedure main() returns () { + var x : float32; + var y : float32; + var z : float32; + + havoc x; + assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); + + if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) { + y := x * x; + assert(y != TO_FLOAT32_INT(0)); + z := TO_FLOAT32_INT(1) / y; + } +} \ No newline at end of file diff --git a/Test/floats/float22.bpl b/Test/floats/float22.bpl new file mode 100644 index 00000000..1505c361 --- /dev/null +++ b/Test/floats/float22.bpl @@ -0,0 +1,20 @@ +//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 : float32; + var y : float32; + var z : float32; + + havoc x; + assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); + + if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) { + y := x * x; + assert(y != TO_FLOAT32_INT(0)); + z := TO_FLOAT32_INT(1) / y; + } +} \ No newline at end of file diff --git a/Test/floats/float23.bpl b/Test/floats/float23.bpl new file mode 100644 index 00000000..69ae243d --- /dev/null +++ b/Test/floats/float23.bpl @@ -0,0 +1,8 @@ +//Translation from nan_double_false-unreach-call.c +//Should return an error + +procedure main() returns () { + var x : float(11 53); + havoc x; + assert(x==x); +} \ No newline at end of file diff --git a/Test/floats/float3.bpl b/Test/floats/float3.bpl new file mode 100644 index 00000000..34059f80 --- /dev/null +++ b/Test/floats/float3.bpl @@ -0,0 +1,27 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + var x : float32; + var y : float32; + var z : float32; + + z := x + y; + z := x - y; + z := x * y; + assume(y != fp<8, 24>(0bv32)); + z := x / y; + + z := (fp<8, 24>(1bv32) + fp<8, 24>(1bv32)) + fp<8, 24>(0bv32); + assert(z == fp<8, 24>(2bv32)); + + z := fp<8, 24>(2bv32) - fp<8, 24>(1bv32); + assert(z == fp<8, 24>(1bv32)); + + z := fp(false, 127bv8, 0bv23) * fp(false, 127bv8, 0bv23); + assert(z == fp(false, 127bv8, 0bv23)); + + z := fp<8, 24>(1bv32) / fp<8, 24>(1bv32); + assert(z == fp(false, 127bv8, 0bv23)); + + return; +} \ No newline at end of file diff --git a/Test/floats/float3.bpl.expect b/Test/floats/float3.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float3.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float4.bpl b/Test/floats/float4.bpl new file mode 100644 index 00000000..7bb24250 --- /dev/null +++ b/Test/floats/float4.bpl @@ -0,0 +1,11 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo() returns (r : float32) { + r := fp<8, 24>(NaN); + r := fp<8, 24>(+oo); + r := fp<8, 24>(-oo); + r := fp<8, 24>(+zero); + r := fp<8, 24>(-zero); + + return; +} \ No newline at end of file diff --git a/Test/floats/float4.bpl.expect b/Test/floats/float4.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float4.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float5.bpl b/Test/floats/float5.bpl new file mode 100644 index 00000000..fd630394 --- /dev/null +++ b/Test/floats/float5.bpl @@ -0,0 +1,24 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_INT(int) returns (float<8, 23>); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_REAL(real) returns (float<8, 23>); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV31(bv31) returns (float<8, 23>); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_BV32(bv32) returns (float<8, 23>); +function {:builtin "(_ to_fp 8 23) RNE"} TO_FLOAT823_FLOAT824(float<8, 24>) returns (float<8, 23>); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT823(float<8, 23>) returns (float<8, 24>); + +procedure foo(x : float<8, 24>) returns (r : float<8, 24>) { + r := TO_FLOAT823_INT(5); // Error + r := TO_FLOAT823_REAL(5.0); // Error + r := TO_FLOAT823_BV31(0bv31); // Error + r := TO_FLOAT823_BV32(0bv32); // Error + r := TO_FLOAT823_FLOAT824(fp<8, 24>(1bv32)); // Error + r := TO_FLOAT824_FLOAT823(fp<8, 24>(1bv32)); // Error + r := TO_FLOAT824_FLOAT823(fp<8, 23>(1bv31)); + + r := TO_FLOAT823_FLOAT824(x); // Error + r := TO_FLOAT824_FLOAT823(x); // Error + + return; +} \ No newline at end of file diff --git a/Test/floats/float5.bpl.expect b/Test/floats/float5.bpl.expect new file mode 100644 index 00000000..6c0b86af --- /dev/null +++ b/Test/floats/float5.bpl.expect @@ -0,0 +1,9 @@ +float5.bpl(12,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24)) +float5.bpl(13,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24)) +float5.bpl(14,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24)) +float5.bpl(15,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24)) +float5.bpl(16,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24)) +float5.bpl(17,42): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23)) +float5.bpl(20,1): Error: mismatched types in assignment command (cannot assign float (8 23) to float (8 24)) +float5.bpl(21,27): Error: invalid type for argument 0 in application of TO_FLOAT824_FLOAT823: float (8 24) (expected: float (8 23)) +8 type checking errors detected in float5.bpl diff --git a/Test/floats/float6.bpl b/Test/floats/float6.bpl new file mode 100644 index 00000000..fe0eab0e --- /dev/null +++ b/Test/floats/float6.bpl @@ -0,0 +1,50 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_INT(int) returns (float<8, 24>); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_REAL(real) returns (float<8, 24>); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_BV32(bv32) returns (float<8, 24>); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT1153_BV64(bv64) returns (float<11, 53>); +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT824_FLOAT32(float32) returns (float<8, 24>); //Should just be an identity function +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT824(float<8, 24>) returns (float32); //Should just be an identity function +function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_FLOAT64(float64) returns (float32); +function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_FLOAT32(float32) returns (float64); + +procedure main() returns () { + var i : int; + var r : real; + var f824 : float<8, 24>; + var f32 : float32; + var f1153 : float<11, 53>; + var f64 : float64; + + f824 := TO_FLOAT824_INT(5); + f32 := TO_FLOAT824_INT(5); + f824 := TO_FLOAT824_REAL(5.0); + f32 := TO_FLOAT824_REAL(5.0); + + f824 := TO_FLOAT824_BV32(0bv32); + f32 := TO_FLOAT824_BV32(0bv32); + f1153 := TO_FLOAT1153_BV64(0bv64); + f64 := TO_FLOAT1153_BV64(0bv64); + + f824 := TO_FLOAT824_FLOAT32(fp<8, 24>(0bv32)); + f32 := TO_FLOAT32_FLOAT824(fp<8, 24>(0bv32)); + f824 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32)); + f32 := TO_FLOAT32_FLOAT64(fp<11, 53>(0bv32)); + f1153 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32)); + f64 := TO_FLOAT64_FLOAT32(fp<8, 24>(0bv32)); + + f824 := TO_FLOAT824_INT(5); + f32 := TO_FLOAT32_FLOAT824(f824); + assert(f32 == f824); + + f32 := TO_FLOAT824_INT(5); + f824 := TO_FLOAT824_FLOAT32(f32); + assert(f32 == f824); + + f32 := TO_FLOAT32_FLOAT64(f64); + f64 := TO_FLOAT64_FLOAT32(f32); + + return; +} \ No newline at end of file diff --git a/Test/floats/float6.bpl.expect b/Test/floats/float6.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float6.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float7.bpl b/Test/floats/float7.bpl new file mode 100644 index 00000000..f330b2ea --- /dev/null +++ b/Test/floats/float7.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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<11, 53> (10000000bv64); + y := x + fp<11, 53>(1bv64); + z := x - fp<11, 53>(1bv64); + r := y - z; + assert r == fp<11, 53> (2bv64); +} \ No newline at end of file diff --git a/Test/floats/float7.bpl.expect b/Test/floats/float7.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float7.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/float8.bpl b/Test/floats/float8.bpl new file mode 100644 index 00000000..78c11a2b --- /dev/null +++ b/Test/floats/float8.bpl @@ -0,0 +1,13 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure main() returns () { + 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<8, 24>(2bv32); +} \ No newline at end of file diff --git a/Test/floats/float8.bpl.expect b/Test/floats/float8.bpl.expect new file mode 100644 index 00000000..426c21e0 --- /dev/null +++ b/Test/floats/float8.bpl.expect @@ -0,0 +1,5 @@ +float8.bpl(12,2): Error BP5001: This assertion might not hold. +Execution trace: + float8.bpl(8,4): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/floats/float9.bpl b/Test/floats/float9.bpl new file mode 100644 index 00000000..cb4f3afd --- /dev/null +++ b/Test/floats/float9.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +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 : 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 == TO_FLOAT32_INT(2); +} \ No newline at end of file diff --git a/Test/floats/float9.bpl.expect b/Test/floats/float9.bpl.expect new file mode 100644 index 00000000..6abb715b --- /dev/null +++ b/Test/floats/float9.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/floats/modpath.py b/Test/floats/modpath.py new file mode 100644 index 00000000..90707701 --- /dev/null +++ b/Test/floats/modpath.py @@ -0,0 +1,13 @@ +import sys + +f = open(sys.argv[1], 'r') +to_write = "" + +for i in f: + to_write += i.replace("..\\Test\\floats\\", "") + +f.close() + +f = open(sys.argv[1], 'w') + +f.write(to_write) \ No newline at end of file diff --git a/Test/floats/test1.bpl b/Test/floats/test1.bpl deleted file mode 100644 index e893e098..00000000 --- a/Test/floats/test1.bpl +++ /dev/null @@ -1,13 +0,0 @@ -//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<11, 53> (10000000bv64); - y := x + fp<11, 53>(1bv64); - z := x - fp<11, 53>(1bv64); - r := y - z; - assert r == fp<11, 53> (2bv64); -} \ No newline at end of file diff --git a/Test/floats/test10.bpl b/Test/floats/test10.bpl deleted file mode 100644 index 566f7a56..00000000 --- a/Test/floats/test10.bpl +++ /dev/null @@ -1,20 +0,0 @@ -//Translation from loop.c -//Should return an error? (The real case does as well...) - -procedure main() returns () { - var x : float; - var y : float; - var z : float; - - x := fp(1); - y := fp(10000000); - z := fp(42); - - while (x < y) { - x := x + fp(1); - y := y - fp(1); - z := z + fp(1); - } - - assert(z >= fp(0) && z <= fp(10000000)); -} \ No newline at end of file diff --git a/Test/floats/test11.bpl b/Test/floats/test11.bpl deleted file mode 100644 index cee3e36e..00000000 --- a/Test/floats/test11.bpl +++ /dev/null @@ -1,55 +0,0 @@ -//Translation from interpolation.c -//Should Verify -//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 : float32; - var t : float32; - var min : [int] float32; - var max : [int] float32; - - 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] := 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; - //} - //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 >= TO_FLOAT32_INT(0) && z <= TO_FLOAT32_INT(1)); -} \ No newline at end of file diff --git a/Test/floats/test12.bpl b/Test/floats/test12.bpl deleted file mode 100644 index c733b9f4..00000000 --- a/Test/floats/test12.bpl +++ /dev/null @@ -1,43 +0,0 @@ -//Translation from inv_Newton.c -//Should Verify -//Unfinished code! - -procedure inv(float(11 53)) returns(float(11 53)) { - var z : float(11 53); - var t : float(11 53); - var t : float(11 53); - - -} - -procedure main() returns () { - var t : float(11 53); - var t : float(11 53); - - min[0] := fp(5); - min[1] := fp(10); - min[2] := fp(12); - min[3] := fp(30); - min[4] := fp(150); - - max[0] := fp(10); - max[1] := fp(12); - max[2] := fp(30); - max[3] := fp(150); - max[4] := fp(300); - - havoc t; - assume(t >= min[0] && t <= max[4]); - - i := 0; - while (i < 5) { - if (t <= max[i]) { - break; - } - i := i + 1; - } - - z := (t - min[i]) / (max[i] - min[i]); - - assert(z >= fp(0) && z <= fp(1)); -} \ No newline at end of file diff --git a/Test/floats/test13.bpl b/Test/floats/test13.bpl deleted file mode 100644 index e5402539..00000000 --- a/Test/floats/test13.bpl +++ /dev/null @@ -1,19 +0,0 @@ -//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 : float32; - var y : float32; - var z : float32; - - havoc x; - assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); - - if (x != TO_FLOAT32_INT(0)) { - y := x * x; - assert(y != TO_FLOAT32_INT(0)); - z := TO_FLOAT32_INT(1) / y; - } -} \ No newline at end of file diff --git a/Test/floats/test14.bpl b/Test/floats/test14.bpl deleted file mode 100644 index 1505c361..00000000 --- a/Test/floats/test14.bpl +++ /dev/null @@ -1,20 +0,0 @@ -//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 : float32; - var y : float32; - var z : float32; - - havoc x; - assume(x >= TO_FLOAT32_INT(-1) && x <= TO_FLOAT32_INT(1)); - - if (x <= TO_FLOAT32_REAL(-1e-20) || x >= TO_FLOAT32_REAL(1e-20)) { - y := x * x; - assert(y != TO_FLOAT32_INT(0)); - z := TO_FLOAT32_INT(1) / y; - } -} \ No newline at end of file diff --git a/Test/floats/test15.bpl b/Test/floats/test15.bpl deleted file mode 100644 index 1dc549ac..00000000 --- a/Test/floats/test15.bpl +++ /dev/null @@ -1,24 +0,0 @@ -//Translation from Muller_Kahan.c -//Should Verify -//NOTE: (fp(....)) causes a compiler error! -//FAILS! Heavily... - -procedure main() returns () { - var x0 : float(11 53); - var x1 : float(11 53); - var x2 : float(11 53); - var i : int; - - x0 := fp(11 11 53) / fp(2 11 53); - x1 := fp(61 11 53) / fp(11 11 53); - i := 0; - while (i < 100) { - x2 := fp(1130 11 53) - fp(3000 11 53) / x0; - x2 := fp(111 11 53) - x2 / x1; - x0 := x1; - x1 := x2; - i := i + 1; - } - - assert(x0 >= fp(99 11 53) && x0 <= fp(101 11 53)); -} \ No newline at end of file diff --git a/Test/floats/test16.bpl b/Test/floats/test16.bpl deleted file mode 100644 index 69ae243d..00000000 --- a/Test/floats/test16.bpl +++ /dev/null @@ -1,8 +0,0 @@ -//Translation from nan_double_false-unreach-call.c -//Should return an error - -procedure main() returns () { - var x : float(11 53); - havoc x; - assert(x==x); -} \ No newline at end of file diff --git a/Test/floats/test17.bpl b/Test/floats/test17.bpl deleted file mode 100644 index caa1fa74..00000000 --- a/Test/floats/test17.bpl +++ /dev/null @@ -1,11 +0,0 @@ -//Translation from nan_double_range_true-unreach-call.c -//Should verify -//Uggghhhh, should I add support for e? - -procedure main() returns () { - var x : float(11 53); - havoc x; - if (x >= fp(-100000000000000000000000000 11 53) && x <= fp(100000000000000000000000000 11 53)) { - assert(x==x); - } -} \ No newline at end of file diff --git a/Test/floats/test18.bpl b/Test/floats/test18.bpl deleted file mode 100644 index 71eb5286..00000000 --- a/Test/floats/test18.bpl +++ /dev/null @@ -1,36 +0,0 @@ -//Translation from rlim_exit.c -//Should verify -//Unary - unsupported float operations (on my end)... - -procedure main() returns () { - var X : float; - var Y : float; - var S : float; - var R : float; - var D : float; - var i : int; - - Y := fp(0); - - i := 0; - while (i < 100000) { - havoc X; - havoc D; - assume(X >= fp(-128) && X <= fp(128)); - assume(D >= fp(0) && D <= fp(16)); - - S := Y; - Y := X; - R := X - S; - if (R <= fp(0)-D) { - Y := S - D; - } - else if(R >= D) { - Y := S + D; - } - - i := i + 1; - } - - assert(Y >= fp(-129) && Y <= fp(129)); -} \ No newline at end of file diff --git a/Test/floats/test19.bpl b/Test/floats/test19.bpl deleted file mode 100644 index f00d8a2b..00000000 --- a/Test/floats/test19.bpl +++ /dev/null @@ -1,36 +0,0 @@ -//Translation from flim_invariant.c -//Should verify -//Unary - unsupported float operations (on my end)... - -procedure main() returns () { - var X : float; - var Y : float; - var S : float; - var R : float; - var D : float; - var i : int; - - Y := fp(0); - - i := 0; - while (i < 100000) { - havoc X; - havoc D; - assume(X >= fp(-128) && X <= fp(128)); - assume(D >= fp(0) && D <= fp(16)); - - S := Y; - Y := X; - R := X - S; - if (R <= fp(0)-D) { - Y := S - D; - } - else if(R >= D) { - Y := S + D; - } - - assert(Y >= fp(-129) && Y <= fp(129)); - - i := i + 1; - } -} \ No newline at end of file diff --git a/Test/floats/test2.bpl b/Test/floats/test2.bpl deleted file mode 100644 index d78c339d..00000000 --- a/Test/floats/test2.bpl +++ /dev/null @@ -1,17 +0,0 @@ -//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 : 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 == TO_FLOAT32_INT(2); -} \ No newline at end of file diff --git a/Test/floats/test20.bpl b/Test/floats/test20.bpl deleted file mode 100644 index 57c605fd..00000000 --- a/Test/floats/test20.bpl +++ /dev/null @@ -1,14 +0,0 @@ -//Should return an error? -//Translation from Rump_double.c - -procedure main() returns () { - var x : float(11 53); - var y : float(11 53); - var r : float(11 53); - - x := fp(77617 11 53); - y := fp(33096 11 53); - r := y*y*y*y*y*y * fp(333.75 11 53) + x*x * (x*x*y*y*fp(11 11 53) - y*y*y*y*y*y - y*y*y*y * fp(121 11 53) - fp(2 11 53)) + y*y*y*y*y*y*y*y * fp(5.5 11 53) + x / (y*fp(2 11 53)); - - assert(r >= fp(0 11 53)); -} \ No newline at end of file diff --git a/Test/floats/test3.bpl b/Test/floats/test3.bpl deleted file mode 100644 index 67c6ba48..00000000 --- a/Test/floats/test3.bpl +++ /dev/null @@ -1,13 +0,0 @@ -//Translation from addsub_float_inexact.c -//Should give an error -procedure main() returns () { - 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<8, 24>(2bv32); -} \ No newline at end of file diff --git a/Test/floats/test4.bpl b/Test/floats/test4.bpl deleted file mode 100644 index a31aa215..00000000 --- a/Test/floats/test4.bpl +++ /dev/null @@ -1,32 +0,0 @@ -//Translation from drift_tenth.c -//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 : float32; - var time : float32; - var i: int; - - 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; - //} - 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/Test/floats/test5.bpl b/Test/floats/test5.bpl deleted file mode 100644 index 7536f8fd..00000000 --- a/Test/floats/test5.bpl +++ /dev/null @@ -1,36 +0,0 @@ -//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 : float64; - var E1 : float64; - var S : float64); - var i : int; - var rand : int; - - E1 := TO_FLOAT64_INT(0); - S := TO_FLOAT64_INT(0); - - i := 0; - while (i <= 1000000) - { - havoc E0; - assume(E0 >= fp(-1 11 53) && E0 <= fp(1 11 53)); - - havoc rand; - if (rand != 0) { - S := fp(0 11 53); - } - else { - S := fp(0.999 11 53) * S + E0 - E1; - } - E1 := E0; - - //assert(1==0); - assert(S >= fp(-1 11 53) && S <= fp(1 11 53)); - i := i + 1; - } -} \ No newline at end of file diff --git a/Test/floats/test6.bpl b/Test/floats/test6.bpl deleted file mode 100644 index 6bef1137..00000000 --- a/Test/floats/test6.bpl +++ /dev/null @@ -1,40 +0,0 @@ -//Translation from filter2.c -//Should give an error -//FAILS; doesn't generate terms! - -procedure main() returns () { - var E : float(11 53); - var E0 : float(11 53); - var E1 : float(11 53); - var S : float(11 53); - var S0 : float(11 53); - var S1 : float(11 53); - var i: int; - - havoc E; - havoc E0; - assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53)); - assume(E0 >= fp(0.0 11 53) && E0 <= fp(1.0 11 53)); - - E1 := fp(0.0 11 53); - S1 := fp(0.0 11 53); - S0 := fp(0.0 11 53); - S := fp(0.0 11 53); - - i := 0; -// while (i <= 1000000) -// { - E1 := E0; - E0 := E; - - havoc E; - assume(E >= fp(0.0 11 53) && E <= fp(1.0 11 53)); - - S1 := S0; - S0 := S; - S := E*fp(0.7 11 53) - E0*fp(1.3 11 53) + E1*fp(1.1 11 53) + S0*fp(1.4 11 53) - S1*fp(0.7 11 53); - - assert(S >= fp(-4.0 11 53) && S <= fp(4.0 11 53)); - //i := i + 1; -// } -} \ No newline at end of file diff --git a/Test/floats/test7.bpl b/Test/floats/test7.bpl deleted file mode 100644 index 8e07878d..00000000 --- a/Test/floats/test7.bpl +++ /dev/null @@ -1,38 +0,0 @@ -//Translation from filter2.c -//Should give an error -//Same as the previous one; it works with reals! - -procedure main() returns () { - var E : real; - var E0 : real; - var E1 : real; - var S : real; - var S0 : real; - var S1 : real; - var i: int; - - havoc E; - havoc E0; - assume(E >= 0.0 && E <= 1.0); - assume(E0 >= 0.0 && E0 <= 1.0); - - S0 := 0.0; - S := 0.0; - - i := 0; - while (i <= 1000000) - { - E1 := E0; - E0 := E; - - havoc E; - assume(E >= 0.0 && E <= 1.0); - - S1 := S0; - S0 := S; - S := E*0.7 - E0*1.3 + E1*1.1 + S0*1.4 - S1*0.7; - - assert(S >= -4.0 && S <= 4.0); - i := i + 1; - } -} \ No newline at end of file diff --git a/Test/floats/test8.bpl b/Test/floats/test8.bpl deleted file mode 100644 index 7e78e206..00000000 --- a/Test/floats/test8.bpl +++ /dev/null @@ -1,16 +0,0 @@ -//Translation from float_double.c -//Should Verify - -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 : float64; - var y : float32; - - 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 diff --git a/Test/floats/test9.bpl b/Test/floats/test9.bpl deleted file mode 100644 index c3a42e6b..00000000 --- a/Test/floats/test9.bpl +++ /dev/null @@ -1,34 +0,0 @@ -//Translation from feedback_diverge.c -//Should give an error -//Not sure on this one... - -procedure main() returns () { - var A : float; - var B : float; - var X : float; - var i : int; - var rand : int; - - A := fp(0); - B := fp(0); - - i := 0; - while (i < 3600000) { - - havoc rand; - if (rand != 0) { - havoc X; - assume(X >= fp(-20) && X <= fp(20)); - } - else { - X := B; - } - - B := B - (B * fp(2.0) - A - X) * fp(.005); - A := X; - - i := i + 1; - } - - assert(A >= fp(-100) && A <= fp(100)); -} \ No newline at end of file -- cgit v1.2.3