From 7fbe519af9271420e5b513021dd1f846a4337e7e Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 5 Jul 2013 14:37:11 -0700 Subject: Added support in the abstract interpreter for an attribute {:identity}, which says that a function is an identity function. --- Test/aitest0/Answer | 42 ++++++++- Test/aitest0/Intervals.bpl | 225 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 266 insertions(+), 1 deletion(-) (limited to 'Test/aitest0') 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(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(x: T): int; +function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId1(x: int): T; +function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId2(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 +} + -- cgit v1.2.3