From 7552293514e40a6dcd9749d3668519d7d32049d5 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 1 Jun 2012 01:36:11 -0700 Subject: 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an assume. 2. Fix for deterministic loop extraction, and a new regression. 3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change. --- Source/Core/Absy.cs | 35 +++++++++++++++++++---------------- Source/Core/CommandLineOptions.cs | 3 ++- Source/Core/Inline.cs | 3 ++- Test/extractloops/Answer | 5 +++++ Test/extractloops/detLoopExtract1.bpl | 30 ++++++++++++++++++++++++++++++ Test/extractloops/runtest.bat | 3 +++ 6 files changed, 61 insertions(+), 18 deletions(-) create mode 100644 Test/extractloops/detLoopExtract1.bpl diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index d7fcca7a..148a739d 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -590,7 +590,25 @@ namespace Microsoft.Boogie { if (!found) { Block auxNewBlock = new Block(); auxNewBlock.Label = ((Block)bl).Label; - auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)block).Cmds); + auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds); + //add restoration code for such blocks + if (loopHeaderToAssignCmd.ContainsKey(header)) + { + AssignCmd assignCmd = loopHeaderToAssignCmd[header]; + auxNewBlock.Cmds.Add(assignCmd); + } + List lhsg = new List(); + IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies; + foreach (IdentifierExpr gl in globalsMods) + lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl)); + List rhsg = new List(); + foreach (IdentifierExpr gl in globalsMods) + rhsg.Add(new OldExpr(Token.NoToken, gl)); + if (lhsg.Count != 0) + { + AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg); + auxNewBlock.Cmds.Add(globalAssignCmd); + } blockMap[(Block)bl] = auxNewBlock; } } @@ -666,21 +684,6 @@ namespace Microsoft.Boogie { if (newTargets.Length == 0) { if (!detLoopExtract) newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); - else { - if (loopHeaderToAssignCmd.ContainsKey(header)) { - AssignCmd assignCmd = loopHeaderToAssignCmd[header]; - newBlock.Cmds.Add(assignCmd); - } - List lhsg = new List(); - IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies; - foreach (IdentifierExpr gl in globalsMods) - lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl)); - List rhsg = new List(); - foreach (IdentifierExpr gl in globalsMods) - rhsg.Add(new OldExpr(Token.NoToken, gl)); - AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg); - newBlock.Cmds.Add(globalAssignCmd); - } newBlock.TransferCmd = new ReturnCmd(Token.NoToken); } else { newBlock.TransferCmd = new GotoCmd(Token.NoToken, newLabels, newTargets); diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 5baf8667..c28d8c8a 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1222,7 +1222,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("contractInfer", ref ContractInfer) || ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) || ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) || - ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) + ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) || + ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ) { // one of the boolean flags matched return true; diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 71f7bbb4..88512025 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -402,7 +402,8 @@ namespace Microsoft.Boogie { return new AssertEnsuresCmd(ensCopy); } else { - return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition)); + //return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition)); + return new AssumeCmd(ens.tok, Expr.True); } } diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer index b9083fae..48ca65e9 100644 --- a/Test/extractloops/Answer +++ b/Test/extractloops/Answer @@ -88,3 +88,8 @@ Stratified Inlining: Reached recursion bound of 4 Boogie program verifier finished with 1 verified, 0 errors ----- +----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops +Stratified Inlining: Reached recursion bound of 4 + +Boogie program verifier finished with 1 verified, 0 errors +----- diff --git a/Test/extractloops/detLoopExtract1.bpl b/Test/extractloops/detLoopExtract1.bpl new file mode 100644 index 00000000..8388cd57 --- /dev/null +++ b/Test/extractloops/detLoopExtract1.bpl @@ -0,0 +1,30 @@ +var g:int; + +procedure {:entrypoint} Foo(a:int) +requires a >= 0; +modifies g; +{ + var b: int; + b := 0; + g := a; + +LH: + goto L_true, L_false; + +L_true: + assume (b < a); + goto L6; + +L6: + b := b + 1; + g := 5; + goto LH; + +L_false: + assume (b >= a); + goto L_end; + +L_end: + assume (b != a); //modeling assert for stratified inlining + return; +} diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat index 05bfae55..6bd151cb 100644 --- a/Test/extractloops/runtest.bat +++ b/Test/extractloops/runtest.bat @@ -19,4 +19,7 @@ echo ----- echo ----- Running regression test detLoopExtract.bpl with deterministicExtractLoops %BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract.bpl echo ----- +echo ----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops +%BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract1.bpl +echo ----- -- cgit v1.2.3