Boogie: added type 'real' with overloaded arithmetic operations plus real division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';

Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)

17 files changed, 169 insertions, 15 deletions

diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index dd5bcff2..bfe185e7 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -268,7 +268,7 @@ implementation p()
 

   A:

     assume {:inferred} true;

-    assume 0 - 1 <= x;

+    assume -1 <= x;

     assume {:inferred} -1 <= x;

     goto B, E;

 

diff --git a/Test/inline/Answer b/Test/inline/Answer
index 655143fa..eddeb64f 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -566,7 +566,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
   var b: bool;

 

   anon0:

-    ret := 0 - 1;

+    ret := -1;

     b := false;

     found := b;

     i := 0;

@@ -659,7 +659,7 @@ implementation main(x: int)
     goto inline$find$0$anon0;

 

   inline$find$0$anon0:

-    inline$find$0$ret := 0 - 1;

+    inline$find$0$ret := -1;

     inline$find$0$b := false;

     inline$find$0$found := inline$find$0$b;

     inline$find$0$i := 0;

@@ -756,7 +756,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
   var inline$check$0$ret: bool;

 

   anon0:

-    ret := 0 - 1;

+    ret := -1;

     b := false;

     found := b;

     i := 0;

diff --git a/Test/test0/Answer b/Test/test0/Answer
index d57e7647..0eda9e2e 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -34,6 +34,12 @@ const y: int;
 

 const z: int;

 

+const r: real;

+

+const s: real;

+

+const t: real;

+

 const P: bool;

 

 const Q: bool;

@@ -56,6 +62,36 @@ axiom x + y mod z == y mod z + x;
 

 axiom (x + y) mod z == x mod z + y mod z;

 

+axiom x / y / z == x / (y / z);

+

+axiom x / y / (z / x) == x / y / z;

+

+axiom x / s / z == x / (s / z);

+

+axiom x / s / (z / x) == x / s / z;

+

+axiom r / s / t == r / (s / t);

+

+axiom r / s / (t / r) == r / s / t;

+

+axiom r * s / t == r * s / t;

+

+axiom r / s * t == r / s * t;

+

+axiom (r * s) ** t == r ** t * s ** t;

+

+axiom r ** (s + t) == r ** s * r ** t;

+

+axiom int(real(x)) == x;

+

+axiom r >= 0e0 ==> real(int(r)) <= r;

+

+axiom int(0e0 - 2e-2) == 0;

+

+axiom int(0e0 - 35e0) == -35;

+

+axiom int(27e-1) == 2;

+

 axiom x - y - z == x - (y - z);

 

 axiom x - y - (z - x) == x - y - z;

diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl
index cb69aa5f..5fffc20a 100644
--- a/Test/test0/ModifiedBag.bpl
+++ b/Test/test0/ModifiedBag.bpl
@@ -1,5 +1,5 @@
 // ----------- BEGIN PRELUDE

-type real;

+

 

 type elements;

 

diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl
index 955faad8..7e4a9ce7 100644
--- a/Test/test0/PrettyPrint.bpl
+++ b/Test/test0/PrettyPrint.bpl
@@ -1,6 +1,9 @@
 const x: int;

 const y: int;

 const z: int;

+const r: real;

+const s: real;

+const t: real;

 const P: bool;

 const Q: bool;

 const R: bool;

@@ -17,6 +20,25 @@ axiom (x div y) div (z div x) == (x div y) div z;
 axiom x + y mod z == ((y mod z) + x);

 axiom (x + y) mod z == (x mod z) + (y mod z);

 

+axiom x / y / z == (x / (y / z));

+axiom (x / y) / (z / x) == (x / y) / z;

+axiom x / s / z == (x / (s / z));

+axiom (x / s) / (z / x) == (x / s) / z;

+axiom r / s / t == (r / (s / t));

+axiom (r / s) / (t / r) == (r / s) / t;

+

+axiom ((r * s) / t) == r * s / t;

+axiom ((r / s) * t) == (r / s) * t;

+

+axiom (r * s) ** t == (r ** t) * (s ** t);

+axiom r ** (s + t) == r ** s * r ** t;

+

+axiom int(real(x)) == x;

+axiom r >= 0.0 ==> real(int(r)) <= r;

+axiom int(0e-3 - 0.02) == 0;

+axiom int(0e2 - 3.5e1) == -35;

+axiom int(27e-1) == 2;

+

 axiom x - y - z == (x - (y - z));

 axiom (x - y) - (z - x) == (x - y) - z;

 

diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl
index ac87476f..79a4d2ab 100644
--- a/Test/test0/Prog0.bpl
+++ b/Test/test0/Prog0.bpl
@@ -1,5 +1,5 @@
 // BoogiePL Examples

-type real;

+

 type elements;

 

 var x:int;  var y:real;  var z:ref;		// Variables

diff --git a/Test/test1/Answer b/Test/test1/Answer
index a8b73b53..94bf2d9a 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -145,3 +145,22 @@ Lambda.bpl(12,8): Error: the type variable T does not occur in types of the lamb
 Lambda.bpl(12,2): Error: mismatched types in assignment command (cannot assign <T>[int]int to [int]int)

 Lambda.bpl(18,27): Error: invalid argument types (bool and int) to binary operator +

 5 type checking errors detected in Lambda.bpl

+IntReal.bpl(5,8): Error: invalid argument types (int and real) to binary operator >=

+IntReal.bpl(6,8): Error: invalid argument types (int and real) to binary operator <=

+IntReal.bpl(7,8): Error: invalid argument types (int and real) to binary operator <

+IntReal.bpl(8,8): Error: invalid argument types (int and real) to binary operator >

+IntReal.bpl(10,9): Error: invalid argument types (int and real) to binary operator ==

+IntReal.bpl(11,8): Error: invalid argument types (int and real) to binary operator +

+IntReal.bpl(12,8): Error: invalid argument types (int and real) to binary operator -

+IntReal.bpl(13,8): Error: invalid argument types (int and real) to binary operator *

+IntReal.bpl(14,8): Error: invalid argument types (int and real) to binary operator div

+IntReal.bpl(15,8): Error: invalid argument types (int and real) to binary operator mod

+IntReal.bpl(17,12): Error: invalid argument types (real and int) to binary operator ==

+IntReal.bpl(23,8): Error: invalid argument types (int and real) to binary operator **

+IntReal.bpl(27,14): Error: invalid argument types (real and int) to binary operator ==

+IntReal.bpl(29,13): Error: invalid argument types (int and real) to binary operator ==

+IntReal.bpl(32,6): Error: argument type int does not match expected type real

+IntReal.bpl(33,6): Error: argument type real does not match expected type int

+IntReal.bpl(45,8): Error: invalid argument types (real and int) to binary operator div

+IntReal.bpl(46,8): Error: invalid argument types (real and int) to binary operator mod

+18 type checking errors detected in IntReal.bpl
\ No newline at end of file
diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl
new file mode 100644
index 00000000..fac41d57
--- /dev/null
+++ b/Test/test1/IntReal.bpl
@@ -0,0 +1,48 @@
+const i: int;

+const r: real;

+

+axiom i == 0;

+axiom i >= 0.0;				// type errror

+axiom i <= 0.0e0;			// type errror

+axiom i < 0.0e-0;			// type errror

+axiom i > 0.0e20;			// type errror

+

+axiom -i == r;				// type errror

+axiom i + r == 0.0;			// type errror

+axiom i - r == 0.0;			// type errror

+axiom i * r == 0.0;			// type errror

+axiom i div r == 0;			// type errror

+axiom i mod r == 0;			// type errror

+

+axiom i / i == 0;			// type errror

+axiom i / i == 0.0;

+axiom i / r == 0.0;

+axiom r / i == 0.0;

+axiom r / r == 0.0;

+

+axiom i ** r == 0.0;		// type errror

+axiom r ** r == 0.0;

+

+axiom real(i) == 0.0;

+axiom real(i) == i;			// type errror

+axiom int(r) == 0;

+axiom int(r) == r;			// type errror

+axiom int(real(i)) == i;

+axiom real(int(r)) == r;

+axiom int(int(r)) == i;		// type errror

+axiom real(real(i)) == r;	// type errror

+

+axiom i == 0;

+axiom real(i) >= 0.0;

+axiom real(i) <= 0.0e0;

+axiom r < 0.0e-0;

+axiom r > 0.0e20;

+

+axiom -r == real(i);

+axiom real(i) + r == 0.0;

+axiom r - real(0) == 0.0;

+axiom r * r == 0.0;

+axiom r div 0 == 0;			// type errror

+axiom r mod 0 == 0;			// type errror

+

+axiom r ** r == 0.0;

diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat
index 979c36e4..149e6dc9 100644
--- a/Test/test1/runtest.bat
+++ b/Test/test1/runtest.bat
@@ -19,3 +19,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe
 %BGEXE% %* /noVerify FunBody.bpl

 %BGEXE% %* /noVerify IfThenElse0.bpl

 %BGEXE% %* /noVerify Lambda.bpl

+%BGEXE% %* /noVerify IntReal.bpl

diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl
index c8ef88c8..6aee18ea 100644
--- a/Test/test2/strings-no-where.bpl
+++ b/Test/test2/strings-no-where.bpl
@@ -1,4 +1,4 @@
-type real;

+

 

 type elements;

 

diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl
index 05e392cb..f196899f 100644
--- a/Test/test2/strings-where.bpl
+++ b/Test/test2/strings-where.bpl
@@ -1,4 +1,4 @@
-type real;

+

 

 type elements;

 

diff --git a/Test/test20/Answer b/Test/test20/Answer
index efa5bced..fa33507e 100644
--- a/Test/test20/Answer
+++ b/Test/test20/Answer
@@ -118,7 +118,7 @@ axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3));
 

 const intSet1: Set int;

 

-axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3));

+axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3));

 

 procedure P();

 

@@ -126,7 +126,7 @@ procedure P();
 

 implementation P()

 {

-    assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3));

+    assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3));

 }

 

 

@@ -143,7 +143,7 @@ axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3);
 

 const intSet1: Set int;

 

-axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3);

+axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3);

 

 procedure P();

 

@@ -151,7 +151,7 @@ procedure P();
 

 implementation P()

 {

-    assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3);

+    assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3);

 }

 

 

diff --git a/Test/test20/Prog0.bpl b/Test/test20/Prog0.bpl
index ea71b8a8..8fc7b7c7 100644
--- a/Test/test20/Prog0.bpl
+++ b/Test/test20/Prog0.bpl
@@ -1,5 +1,5 @@
 // Let's test some Boogie 2 features ...

-type real;

+

 type elements;

 

 type Field a;

diff --git a/Test/test20/Prog1.bpl b/Test/test20/Prog1.bpl
index 1d75805c..0e9413c1 100644
--- a/Test/test20/Prog1.bpl
+++ b/Test/test20/Prog1.bpl
@@ -1,5 +1,5 @@
 // Let's test some Boogie 2 features ...

-type real;

+

 type elements;

 

 type Field a;

diff --git a/Test/test21/Answer b/Test/test21/Answer
index 914e56a1..28aa4e8b 100644
--- a/Test/test21/Answer
+++ b/Test/test21/Answer
@@ -278,6 +278,9 @@ Execution trace:
     LargeLiterals0.bpl(7,5): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

+--------------------- File Real.bpl ----------------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

 --------------------- File NameClash.bpl ----------------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

@@ -549,6 +552,9 @@ Execution trace:
     LargeLiterals0.bpl(7,5): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

+--------------------- File Real.bpl ----------------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

 --------------------- File NameClash.bpl ----------------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

@@ -826,6 +832,9 @@ Execution trace:
     LargeLiterals0.bpl(7,5): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

+--------------------- File Real.bpl ----------------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

 --------------------- File NameClash.bpl ----------------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl
new file mode 100644
index 00000000..3dcf3ea3
--- /dev/null
+++ b/Test/test21/Real.bpl
@@ -0,0 +1,17 @@
+axiom (forall r: real :: r == 0.0 || r / r == 1.0);

+

+procedure P(a: real, b: real) returns () {

+  assume a >= b && a != 0.0 && a >= 1.3579;

+

+  assert 2e0 * (a + 3.0) - 0.5 >= b;

+  assert 2e0 * (a + 3.0) - 0.5 > b;

+  assert b <= 2e0 * (a + 3.0) - 0.5;

+  assert b < 2e0 * (a + 3.0) - 0.5;

+

+  assert 1/2 <= 0.65;

+  assert a > 100e-2 ==> 1 / a <= a;

+  assert a / 2 != a || a == 0.00;

+  assert a != 0.0 ==> a / a == 1.0;

+

+  assert int(a) >= 0 ==> real(3) * a > a;

+}
\ No newline at end of file
diff --git a/Test/test21/runtest.bat b/Test/test21/runtest.bat
index d994a4da..bfdcc570 100644
--- a/Test/test21/runtest.bat
+++ b/Test/test21/runtest.bat
@@ -4,6 +4,7 @@ setlocal
 set BGEXE=..\..\Binaries\Boogie.exe

 rem set BGEXE=mono ..\..\Binaries\Boogie.exe

 

+

 for %%m in (

               n p a

             ) do (

@@ -16,7 +17,8 @@ for %%f in (DisjointDomains.bpl DisjointDomains2.bpl FunAxioms.bpl
             Keywords.bpl Casts.bpl BooleanQuantification.bpl EmptyList.bpl Boxing.bpl

             MapOutputTypeParams.bpl ParallelAssignment.bpl BooleanQuantification2.bpl

             Flattening.bpl Orderings.bpl Orderings2.bpl Orderings3.bpl Orderings4.bpl

-            EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl) do (

+            EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl

+            Real.bpl) do (

   echo --------------------- File %%f ----------------------------

   %BGEXE% %* /typeEncoding:%%m /logPrefix:0%%m %%f

 )