diff options
| -rw-r--r-- | Source/Core/Absy.cs | 35 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 3 | ||||
| -rw-r--r-- | Source/Core/Inline.cs | 3 | ||||
| -rw-r--r-- | Test/extractloops/Answer | 5 | ||||
| -rw-r--r-- | Test/extractloops/detLoopExtract1.bpl | 30 | ||||
| -rw-r--r-- | Test/extractloops/runtest.bat | 3 |
6 files changed, 61 insertions, 18 deletions
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<AssignLhs> lhsg = new List<AssignLhs>();
+ IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;
+ foreach (IdentifierExpr gl in globalsMods)
+ lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));
+ List<Expr> rhsg = new List<Expr>();
+ 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<AssignLhs> lhsg = new List<AssignLhs>();
- IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;
- foreach (IdentifierExpr gl in globalsMods)
- lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));
- List<Expr> rhsg = new List<Expr>();
- 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 -----
|