summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Unknown <shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com>2012-06-01 01:36:11 -0700
committerGravatar Unknown <shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com>2012-06-01 01:36:11 -0700
commit7552293514e40a6dcd9749d3668519d7d32049d5 (patch)
tree2ae7fec112e8228b808d652e07b6bd19d4722a4a
parent622c64cbbba5d3619eaf4de03458111ff6589027 (diff)
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.
-rw-r--r--Source/Core/Absy.cs35
-rw-r--r--Source/Core/CommandLineOptions.cs3
-rw-r--r--Source/Core/Inline.cs3
-rw-r--r--Test/extractloops/Answer5
-rw-r--r--Test/extractloops/detLoopExtract1.bpl30
-rw-r--r--Test/extractloops/runtest.bat3
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 -----