Added support in the abstract interpreter for an attribute {:identity}, which says that a function is an identity function.

2 files changed, 266 insertions, 1 deletions

diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index dabe9710..961b3c33 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -124,5 +124,45 @@ Execution trace:
     Intervals.bpl(87,5): anon0

     Intervals.bpl(88,3): loop_head

     Intervals.bpl(91,3): after_loop

+Intervals.bpl(138,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(133,5): anon0

+    Intervals.bpl(134,3): anon3_LoopHead

+    Intervals.bpl(134,3): anon3_LoopDone

+Intervals.bpl(149,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(144,5): anon0

+    Intervals.bpl(145,3): anon3_LoopHead

+    Intervals.bpl(145,3): anon3_LoopDone

+Intervals.bpl(200,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(190,8): anon0

+    Intervals.bpl(191,3): anon4_LoopHead

+    Intervals.bpl(191,3): anon4_LoopDone

+Intervals.bpl(238,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(233,5): anon0

+    Intervals.bpl(234,3): anon3_LoopHead

+    Intervals.bpl(234,3): anon3_LoopDone

+Intervals.bpl(250,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(244,8): anon0

+    Intervals.bpl(245,3): anon3_LoopHead

+    Intervals.bpl(245,3): anon3_LoopDone

+Intervals.bpl(261,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(256,5): anon0

+    Intervals.bpl(257,3): anon3_LoopHead

+    Intervals.bpl(257,3): anon3_LoopDone

+Intervals.bpl(283,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(278,5): anon0

+    Intervals.bpl(279,3): anon3_LoopHead

+    Intervals.bpl(279,3): anon3_LoopDone

+Intervals.bpl(305,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    Intervals.bpl(300,5): anon0

+    Intervals.bpl(301,3): anon3_LoopHead

+    Intervals.bpl(301,3): anon3_LoopDone

 

-Boogie program verifier finished with 5 verified, 3 errors

+Boogie program verifier finished with 15 verified, 11 errors

diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 4520a032..6a588bbe 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -91,3 +91,228 @@ procedure UnaryNegation1() returns (x: int)  // this was once buggy
   after_loop:

   assert x == 1;  // error

 }

+

+// --------------------------- test {:identity} annotation --------------------

+

+function {:identity} MyId(x: int): int;

+function MyStealthyId(x: int): int;  // this one messes up the abstract interpretation

+function {:identity false} {:identity}/*the last attribute rules*/ MyPolyId<T>(x: T): T;

+function {:identity /*this is a lie*/} MyBogusId(x: int): int { -x }

+function {:identity /*ignored, since the function takes more than one argument*/} MultipleArgs(x: int, y: int): int;

+function {:identity /*ignored, since the return type is not equal to the argument type*/} BoolToInt(b: bool): int;

+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId0<T>(x: T): int;

+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId1<T>(x: int): T;

+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId2<T,U>(x: T): U;

+

+

+procedure Id0(n: int)

+{

+  var i: int;

+  i := 0;

+  while (i < n)

+  {

+    i := i + 1;

+  }

+  assert 0 <= i;

+}

+

+procedure Id1(n: int)

+{

+  var i: int;

+  i := MyId(0);

+  while (i < n)

+  {

+    i := i + MyId(1);

+  }

+  assert 0 <= i;

+}

+

+procedure Id2(n: int)

+{

+  var i: int;

+  i := MyStealthyId(0);

+  while (i < n)

+  {

+    i := i + 1;

+  }

+  assert 0 <= i;  // error: abstract interpreter does not figure this one out

+}

+

+procedure Id3(n: int)

+{

+  var i: int;

+  i := 0;

+  while (i < n)

+  {

+    i := i + MyStealthyId(1);

+  }

+  assert 0 <= i;  // error: abstract interpreter does not figure this one out

+}

+

+procedure Id4(n: int)

+{

+  var i: int;

+  i := MyPolyId(0);

+  while (i < n)

+  {

+    i := i + MyPolyId(1);

+  }

+  assert 0 <= i;

+}

+

+procedure Id5(n: int)

+{

+  var i: int;

+  var b: bool;

+  i, b := 0, false;

+  while (i < n)

+  {

+    i, b := i + 1, false;

+  }

+  assert !b;

+}

+

+procedure Id6(n: int)

+{

+  var i: int;

+  var b: bool;

+  i, b := 0, MyPolyId(false);

+  while (i < n)

+  {

+    i, b := i + 1, false;

+  }

+  assert !b;

+}

+

+procedure Id7(n: int)

+{

+  var i, k, y, z: int;

+  i, k := 0, 0;

+  while (i < n)

+  {

+    i := i + 1;

+    y, z := MyBogusId(5), -5;

+    k := k + z;

+    if (*) {

+      assert y == z;  // fine

+    }

+  }

+  assert 0 <= k;  // error: this does not hold -- k may very well be negative

+}

+

+procedure Id8(n: int)

+{

+  var i, k: int;

+  i, k := 0, 0;

+  while (i < n)

+  {

+    i := i + 1;

+    k := k + MyBogusId(5);

+  }

+  assert 0 <= k;  // since we lied about MyBogusId being an {:identity} function, the abstract interpreter gives us this bogus invariant

+}

+

+procedure Id9(n: int)

+  requires 0 < n;

+{

+  var i, k: int;

+  i, k := 0, 0;

+  while (i < n)

+    invariant i <= n && -k == 5*i;

+  {

+    i := i + 1;

+    k := k + MyBogusId(5);

+  }

+  assert -k == 5*n;

+  assert false;  // this just shows the effect of MyBogusId even more; there is no complaint about this assert

+}

+

+procedure Id10(n: int)

+{

+  var i: int;

+  i := 0;

+  while (i < n)

+  {

+    i := i + MultipleArgs(19, 23);

+  }

+  assert 0 <= i;  // error: no information is known about i

+}

+

+procedure Id11(n: int)

+{

+  var i, k: int;

+  i, k := 0, 0;

+  while (i < n)

+  {

+    i := i + 1;

+    k := k + BoolToInt(false);  // this should not be treated as an identity function, since it goes from one type to another

+  }

+  assert 0 <= k;  // error: no information is known about k

+}

+

+procedure Id12(n: int)

+{

+  var i: int;

+  i := 0;

+  while (i < n)

+  {

+    i := i + SometimesId0(false);

+  }

+  assert 0 <= i;  // error: no information is known about i

+}

+

+procedure Id13(n: int)

+{

+  var i: int;

+  i := 0;

+  while (i < n)

+  {

+    i := i + SometimesId0(1);

+  }

+  assert 0 <= i;

+}

+

+procedure Id14(n: int)

+{

+  var i: int;

+  i := 0;

+  while (i < n)

+  {

+    i := i + SometimesId0(-1);

+  }

+  assert 0 <= i;  // error: this does not hold

+}

+

+procedure Id15(n: int)

+{

+  var i: int;

+  i := 0;

+  while (i < n)

+  {

+    i := i + SometimesId1(1);

+  }

+  assert 0 <= i;  // fine: SometimesId1 claims to be an identity and the use of it is int->int

+}

+

+procedure Id16(n: int)

+{

+  var i: int;

+  i := 0;

+  while (i < n)

+  {

+    i := i + SometimesId2(false);

+  }

+  assert 0 <= i;  // error: no information is known about i

+}

+

+procedure Id17(n: int)

+{

+  var i: int;

+  i := 0;

+  while (i < n)

+  {

+    i := i + SometimesId2(1);

+  }

+  assert 0 <= i;  // fine: SometimesId2 claims to be an identity and the use of it is int->int

+}

+