From ab03eafe1c01840e7baab8fd51b4f00f11076d6a Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 4 Jan 2013 14:42:40 -0800 Subject: bug fix for interaction between inlining and loops --- Test/inline/Answer | 73 ++++++++++++++++++++++++++++------------ Test/inline/InliningAndLoops.bpl | 20 +++++++++++ Test/inline/runtest.bat | 4 +++ 3 files changed, 75 insertions(+), 22 deletions(-) create mode 100644 Test/inline/InliningAndLoops.bpl (limited to 'Test') diff --git a/Test/inline/Answer b/Test/inline/Answer index eddeb64f..ff2a5e71 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -101,6 +101,7 @@ implementation Main() inline$inc$0$Entry: inline$inc$0$x := x; inline$inc$0$i := 5; + havoc inline$inc$0$y; goto inline$inc$0$anon0; inline$inc$0$anon0: @@ -119,6 +120,7 @@ implementation Main() inline$incdec$0$Entry: inline$incdec$0$x := x; inline$incdec$0$y := 2; + havoc inline$incdec$0$z; goto inline$incdec$0$anon0; inline$incdec$0$anon0: @@ -129,6 +131,7 @@ implementation Main() inline$dec$0$Entry: inline$dec$0$x := inline$incdec$0$z; inline$dec$0$i := inline$incdec$0$y; + havoc inline$dec$0$y; goto inline$dec$0$anon0; inline$dec$0$anon0: @@ -174,6 +177,7 @@ implementation {:inline 1} incdec(x: int, y: int) returns (z: int) inline$dec$0$Entry: inline$dec$0$x := z; inline$dec$0$i := y; + havoc inline$dec$0$y; goto inline$dec$0$anon0; inline$dec$0$anon0: @@ -253,6 +257,7 @@ implementation calculate() inline$increase$0$Entry: inline$increase$0$i := y; + havoc inline$increase$0$j, inline$increase$0$k; inline$increase$0$glb := glb; goto inline$increase$0$anon0; @@ -344,6 +349,7 @@ implementation recursivetest() inline$recursive$0$Entry: inline$recursive$0$x := glb; + havoc inline$recursive$0$k, inline$recursive$0$y; goto inline$recursive$0$anon0; inline$recursive$0$anon0: @@ -360,6 +366,7 @@ implementation recursivetest() inline$recursive$1$Entry: inline$recursive$1$x := inline$recursive$0$x - 1; + havoc inline$recursive$1$k, inline$recursive$1$y; goto inline$recursive$1$anon0; inline$recursive$1$anon0: @@ -376,6 +383,7 @@ implementation recursivetest() inline$recursive$2$Entry: inline$recursive$2$x := inline$recursive$1$x - 1; + havoc inline$recursive$2$k, inline$recursive$2$y; goto inline$recursive$2$anon0; inline$recursive$2$anon0: @@ -448,6 +456,7 @@ implementation {:inline 3} recursive(x: int) returns (y: int) inline$recursive$0$Entry: inline$recursive$0$x := x - 1; + havoc inline$recursive$0$k, inline$recursive$0$y; goto inline$recursive$0$anon0; inline$recursive$0$anon0: @@ -464,6 +473,7 @@ implementation {:inline 3} recursive(x: int) returns (y: int) inline$recursive$1$Entry: inline$recursive$1$x := inline$recursive$0$x - 1; + havoc inline$recursive$1$k, inline$recursive$1$y; goto inline$recursive$1$anon0; inline$recursive$1$anon0: @@ -480,6 +490,7 @@ implementation {:inline 3} recursive(x: int) returns (y: int) inline$recursive$2$Entry: inline$recursive$2$x := inline$recursive$1$x - 1; + havoc inline$recursive$2$k, inline$recursive$2$y; goto inline$recursive$2$anon0; inline$recursive$2$anon0: @@ -656,6 +667,7 @@ implementation main(x: int) inline$find$0$A := A; inline$find$0$size := size; inline$find$0$x := x; + havoc inline$find$0$i, inline$find$0$b, inline$find$0$ret, inline$find$0$found; goto inline$find$0$anon0; inline$find$0$anon0: @@ -677,6 +689,7 @@ implementation main(x: int) inline$check$0$i := inline$find$0$i; inline$check$0$c := inline$find$0$x; assert inline$check$0$i >= 0; + havoc inline$check$0$ret; goto inline$check$0$anon0; inline$check$0$anon0: @@ -774,6 +787,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in inline$check$0$i := i; inline$check$0$c := x; assert inline$check$0$i >= 0; + havoc inline$check$0$ret; goto inline$check$0$anon0; inline$check$0$anon0: @@ -819,38 +833,38 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in } -(68,4): Error BP5003: A postcondition might not hold on this return path. +(70,4): Error BP5003: A postcondition might not hold on this return path. (78,2): Related location: This is the postcondition that might not hold. Execution trace: (19,0): anon0 - (28,0): inline$find$0$anon0 - (38,0): inline$find$0$anon4_LoopBody - (42,0): inline$check$0$Entry - (57,0): inline$check$0$anon4_Else - (62,0): inline$check$0$anon3 - (65,0): inline$check$0$Return -(100,4): Error BP5001: This assertion might not hold. + (29,0): inline$find$0$anon0 + (39,0): inline$find$0$anon4_LoopBody + (43,0): inline$check$0$Entry + (59,0): inline$check$0$anon4_Else + (64,0): inline$check$0$anon3 + (67,0): inline$check$0$Return +(102,4): Error BP5001: This assertion might not hold. Execution trace: (19,0): anon0 - (28,0): inline$find$0$anon0 - (38,0): inline$find$0$anon4_LoopBody - (42,0): inline$check$0$Entry - (52,0): inline$check$0$anon4_Then - (65,0): inline$check$0$Return - (73,0): inline$find$0$anon5_Then - (87,0): inline$find$0$anon3 - (90,0): inline$find$0$Return - (95,0): anon0$1 - (98,0): anon3_Then -(50,4): Error BP5003: A postcondition might not hold on this return path. + (29,0): inline$find$0$anon0 + (39,0): inline$find$0$anon4_LoopBody + (43,0): inline$check$0$Entry + (54,0): inline$check$0$anon4_Then + (67,0): inline$check$0$Return + (75,0): inline$find$0$anon5_Then + (89,0): inline$find$0$anon3 + (92,0): inline$find$0$Return + (97,0): anon0$1 + (100,0): anon3_Then +(51,4): Error BP5003: A postcondition might not hold on this return path. (78,2): Related location: This is the postcondition that might not hold. Execution trace: (10,0): anon0 (20,0): anon4_LoopBody (24,0): inline$check$0$Entry - (39,0): inline$check$0$anon4_Else - (44,0): inline$check$0$anon3 - (47,0): inline$check$0$Return + (40,0): inline$check$0$anon4_Else + (45,0): inline$check$0$anon3 + (48,0): inline$check$0$Return (99,0): Error BP5003: A postcondition might not hold on this return path. (78,2): Related location: This is the postcondition that might not hold. Execution trace: @@ -1540,3 +1554,18 @@ Execution trace: polyInline.bpl(27,3): anon0 Boogie program verifier finished with 0 verified, 2 errors +-------------------- InliningAndLoops.bpl -------------------- +InliningAndLoops.bpl(12,5): Error BP5001: This assertion might not hold. +Execution trace: + InliningAndLoops.bpl(5,10): anon0#3 + InliningAndLoops.bpl(6,3): anon4_LoopHead#3 + InliningAndLoops.bpl(8,5): anon4_LoopBody#3 + InliningAndLoops.bpl(8,5): anon4_LoopBody$1#3 + InliningAndLoops.bpl(6,3): anon4_LoopHead#2 + InliningAndLoops.bpl(8,5): anon4_LoopBody#2 + InliningAndLoops.bpl(8,5): anon4_LoopBody$1#2 + InliningAndLoops.bpl(6,3): anon4_LoopHead#1 + InliningAndLoops.bpl(6,3): anon4_LoopDone#3 + InliningAndLoops.bpl(12,5): anon5_Then#3 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/inline/InliningAndLoops.bpl b/Test/inline/InliningAndLoops.bpl new file mode 100644 index 00000000..970591a5 --- /dev/null +++ b/Test/inline/InliningAndLoops.bpl @@ -0,0 +1,20 @@ +procedure foo(N: int) + requires N == 2; +{ + var n, sum, recent: int; + n, sum := 0, 0; + while (n < N) + { + call recent := bar(); + sum, n := sum + recent, n + 1; + } + if (n == 2) { + assert sum == recent + recent; // no reason to believe this always to be true + } +} + +procedure {:inline 1} bar() returns (r: int) +{ + var x: int; + r := x; +} diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat index f56d55a0..cd404bfa 100644 --- a/Test/inline/runtest.bat +++ b/Test/inline/runtest.bat @@ -37,3 +37,7 @@ echo -------------------- fundef.bpl -------------------- echo -------------------- polyInline.bpl -------------------- %BGEXE% %* /typeEncoding:predicates /logPrefix:p polyInline.bpl %BGEXE% %* /typeEncoding:arguments /logPrefix:a polyInline.bpl + +echo -------------------- InliningAndLoops.bpl -------------------- +%BGEXE% %* /loopUnroll:3 /soundLoopUnrolling InliningAndLoops.bpl + -- cgit v1.2.3