diff options
| -rw-r--r-- | Source/Core/Inline.cs | 32 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 53 | ||||
| -rw-r--r-- | Test/houdini/Answer | 9 | ||||
| -rw-r--r-- | Test/houdini/runtest.bat | 2 |
4 files changed, 76 insertions, 20 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 07a8e8a9..71f7bbb4 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -406,6 +406,16 @@ namespace Microsoft.Boogie { }
}
+ private CmdSeq RemoveAsserts(CmdSeq cmds) {
+ CmdSeq newCmdSeq = new CmdSeq();
+ for (int i = 0; i < cmds.Length; i++) {
+ Cmd cmd = cmds[i];
+ if (cmd is AssertCmd) continue;
+ newCmdSeq.Add(cmd);
+ }
+ return newCmdSeq;
+ }
+
// result[0] is the entry block
protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Implementation impl, string nextBlockLabel) {
Contract.Requires(nextBlockLabel != null);
@@ -439,16 +449,6 @@ namespace Microsoft.Boogie { for (int i = 0; i < proc.Requires.Length; i++) {
Requires/*!*/ req = cce.NonNull(proc.Requires[i]);
inCmds.Add(InlinedRequires(impl, callCmd, req));
- /*
- if (!req.Free && !QKeyValue.FindBoolAttribute(req.Attributes, "candidate")) {
- Requires reqCopy = (Requires)cce.NonNull(req.Clone());
- reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
- AssertCmd a = new AssertRequiresCmd(callCmd, reqCopy);
- Contract.Assert(a != null);
- a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
- inCmds.Add(a);
- }
- */
}
VariableSeq locVars = cce.NonNull(impl.OriginalLocVars);
@@ -495,6 +495,9 @@ namespace Microsoft.Boogie { Block intBlock;
foreach (Block block in implBlocks) {
CmdSeq copyCmds = codeCopier.CopyCmdSeq(block.Cmds);
+ if (0 <= inlineDepth) {
+ copyCmds = RemoveAsserts(copyCmds);
+ }
TransferCmd transferCmd = CreateInlinedTransferCmd(cce.NonNull(block.TransferCmd), GetInlinedProcLabel(proc.Name));
intBlock = new Block(block.tok, GetInlinedProcLabel(proc.Name) + "$" + block.Label, copyCmds, transferCmd);
inlinedBlocks.Add(intBlock);
@@ -507,15 +510,6 @@ namespace Microsoft.Boogie { for (int i = 0; i < proc.Ensures.Length; i++) {
Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);
outCmds.Add(InlinedEnsures(impl, callCmd, ens));
- /*
- if (!ens.Free && !QKeyValue.FindBoolAttribute(ens.Attributes, "candidate")) {
- Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());
- ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
- AssertCmd a = new AssertEnsuresCmd(ensCopy);
- Contract.Assert(a != null);
- outCmds.Add(a);
- }
- */
}
// assign out params
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 6cd961ac..ce02d173 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -247,6 +247,49 @@ namespace Microsoft.Boogie.Houdini { }
}
+ public class InlineRequiresVisitor : StandardVisitor {
+ public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
+ Contract.Requires(cmdSeq != null);
+ Contract.Ensures(Contract.Result<CmdSeq>() != null);
+ CmdSeq newCmdSeq = new CmdSeq();
+ for (int i = 0, n = cmdSeq.Length; i < n; i++) {
+ Cmd cmd = cmdSeq[i];
+ CallCmd callCmd = cmd as CallCmd;
+ if (callCmd != null) {
+ newCmdSeq.AddRange(InlineRequiresForCallCmd(callCmd));
+ }
+ else {
+ newCmdSeq.Add((Cmd)this.Visit(cmd));
+ }
+ }
+ return newCmdSeq;
+ }
+ private CmdSeq InlineRequiresForCallCmd(CallCmd node) {
+ Hashtable substMap = new Hashtable();
+ for (int i = 0; i < node.Proc.InParams.Length; i++) {
+ substMap.Add(node.Proc.InParams[i], node.Ins[i]);
+ }
+ Substitution substitution = Substituter.SubstitutionFromHashtable(substMap);
+ CmdSeq cmds = new CmdSeq();
+ foreach (Requires requires in node.Proc.Requires) {
+ if (requires.Free) continue;
+ Requires requiresCopy = new Requires(false, Substituter.Apply(substitution, requires.Condition));
+ cmds.Add(new AssertRequiresCmd(node, requiresCopy));
+ }
+ cmds.Add(node);
+ return cmds;
+ }
+ }
+
+ public class FreeRequiresVisitor : StandardVisitor {
+ public override Requires VisitRequires(Requires requires) {
+ if (requires.Free)
+ return base.VisitRequires(requires);
+ else
+ return new Requires(true, requires.Condition);
+ }
+ }
+
public class Houdini : ObservableHoudini {
private Program program;
private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;
@@ -306,6 +349,16 @@ namespace Microsoft.Boogie.Houdini { return;
foreach (Implementation impl in callGraph.Nodes) {
+ InlineRequiresVisitor inlineRequiresVisitor = new InlineRequiresVisitor();
+ inlineRequiresVisitor.Visit(impl);
+ }
+
+ foreach (Implementation impl in callGraph.Nodes) {
+ FreeRequiresVisitor freeRequiresVisitor = new FreeRequiresVisitor();
+ freeRequiresVisitor.Visit(impl);
+ }
+
+ foreach (Implementation impl in callGraph.Nodes) {
impl.OriginalBlocks = impl.Blocks;
impl.OriginalLocVars = impl.LocVars;
}
diff --git a/Test/houdini/Answer b/Test/houdini/Answer index b8e22af3..6053b442 100644 --- a/Test/houdini/Answer +++ b/Test/houdini/Answer @@ -146,3 +146,12 @@ b15 = False b16 = False
Boogie program verifier finished with 5 verified, 0 errors
+.
+-------------------- test10.bpl --------------------
+Assignment computed by Houdini:
+b1 = True
+b2 = True
+b3 = True
+b4 = True
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat index de2e6099..f0065b0d 100644 --- a/Test/houdini/runtest.bat +++ b/Test/houdini/runtest.bat @@ -9,7 +9,7 @@ for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bp %BGEXE% %* /nologo /noinfer /contractInfer %%f
)
-for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl) do (
+for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
echo .
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /contractInfer /inlineDepth:1 %%f
|