diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 3 | ||||
| -rw-r--r-- | Source/Core/Inline.cs | 64 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 17 |
3 files changed, 48 insertions, 36 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 4073c722..7e2ea87a 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -390,8 +390,7 @@ namespace Microsoft.Boogie { inline = true;
}
}
- if ((inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) ||
- CommandLineOptions.Clo.InlineDepth >= 0) {
+ if (inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) {
foreach (Declaration d in TopLevelDeclarations) {
Implementation impl = d as Implementation;
if (impl != null) {
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index c9f6445c..07a8e8a9 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -66,19 +66,18 @@ namespace Microsoft.Boogie { return prefix + "$" + formalName;
}
- protected Inliner(InlineCallback cb) {
- inlinedProcLblMap = new Dictionary<string/*!*/, int>();
- recursiveProcUnrollMap = new Dictionary<string/*!*/, int>();
- inlineDepth = CommandLineOptions.Clo.InlineDepth;
- codeCopier = new CodeCopier();
- inlineCallback = cb;
+ protected Inliner(InlineCallback cb, int inlineDepth) {
+ this.inlinedProcLblMap = new Dictionary<string/*!*/, int>();
+ this.recursiveProcUnrollMap = new Dictionary<string/*!*/, int>();
+ this.inlineDepth = inlineDepth;
+ this.codeCopier = new CodeCopier();
+ this.inlineCallback = cb;
}
- public static void ProcessImplementation(Program program, Implementation impl, InlineCallback cb) {
+ private static void ProcessImplementation(Program program, Implementation impl, Inliner inliner) {
Contract.Requires(impl != null);
Contract.Requires(program != null);
Contract.Requires(impl.Proc != null);
- Inliner inliner = new Inliner(cb);
VariableSeq/*!*/ newInParams = new VariableSeq(impl.InParams);
Contract.Assert(newInParams != null);
@@ -90,7 +89,7 @@ namespace Microsoft.Boogie { Contract.Assert(newModifies != null);
bool inlined = false;
- List<Block/*!*/>/*!*/ newBlocks = inliner.DoInline(impl.Blocks, program, newLocalVars, newModifies, out inlined);
+ List<Block> newBlocks = inliner.DoInlineBlocks(impl.Blocks, program, newLocalVars, newModifies, ref inlined);
Contract.Assert(cce.NonNullElements(newBlocks));
if (!inlined)
@@ -112,12 +111,18 @@ namespace Microsoft.Boogie { }
}
+ public static void ProcessImplementationForHoudini(Program program, Implementation impl) {
+ Contract.Requires(impl != null);
+ Contract.Requires(program != null);
+ Contract.Requires(impl.Proc != null);
+ ProcessImplementation(program, impl, new Inliner(null, CommandLineOptions.Clo.InlineDepth));
+ }
public static void ProcessImplementation(Program program, Implementation impl) {
Contract.Requires(impl != null);
Contract.Requires(program != null);
Contract.Requires(impl.Proc != null);
- ProcessImplementation(program, impl, null);
+ ProcessImplementation(program, impl, new Inliner(null, -1));
}
protected void EmitImpl(Implementation impl) {
@@ -231,10 +236,10 @@ namespace Microsoft.Boogie { newCmds.Add(codeCopier.CopyCmd(cmd));
continue;
}
-
- int inline = GetInlineCount(impl);
- if (inline > 0 || (inline == -1 && inlineDepth > 0)) { // at least one block should exist
+ int inline = inlineDepth >= 0 ? inlineDepth : GetInlineCount(impl);
+
+ if (inline > 0) { // at least one block should exist
Contract.Assume(impl != null);
Contract.Assert(cce.NonNull(impl.OriginalBlocks).Count > 0);
inlinedSomething = true;
@@ -258,17 +263,22 @@ namespace Microsoft.Boogie { EndInline();
- if (inline > 0)
- recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;
- else
+ if (inlineDepth >= 0) {
+ Debug.Assert(inlineDepth > 0);
inlineDepth = inlineDepth - 1;
+ }
+ else {
+ recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;
+ }
inlinedBlocks = DoInlineBlocks(inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);
- if (inline > 0)
- recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;
- else
+ if (inlineDepth >= 0) {
inlineDepth = inlineDepth + 1;
+ }
+ else {
+ recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;
+ }
Block/*!*/ startBlock = inlinedBlocks[0];
Contract.Assert(startBlock != null);
@@ -281,7 +291,7 @@ namespace Microsoft.Boogie { lblCount = nextlblCount;
newCmds = new CmdSeq();
- } else if (inline == 0 || (inline == -1 && inlineDepth == 0)) {
+ } else if (inline == 0) {
inlinedSomething = true;
if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {
// add assert
@@ -306,20 +316,6 @@ namespace Microsoft.Boogie { return newBlocks;
}
- protected List<Block/*!*/>/*!*/ DoInline(List<Block/*!*/>/*!*/ blocks, Program program, VariableSeq newLocalVars, IdentifierExprSeq newModifies, out bool inlined) {
- Contract.Requires(newModifies != null);
- Contract.Requires(newLocalVars != null);
- Contract.Requires(program != null);
- Contract.Requires(cce.NonNullElements(blocks));
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
- inlinedProcLblMap.Clear();
- recursiveProcUnrollMap.Clear();
- inlineDepth = CommandLineOptions.Clo.InlineDepth;
-
- inlined = false;
- return DoInlineBlocks(blocks, program, newLocalVars, newModifies, ref inlined);
- }
-
protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Implementation impl) {
Contract.Requires(impl != null);
Contract.Requires(impl.Proc != null);
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 2c202022..ed3d1afc 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -261,6 +261,7 @@ namespace Microsoft.Boogie.Houdini { this.callGraph = BuildCallGraph();
this.continueAtError = continueAtError;
this.houdiniConstants = CollectExistentialConstants();
+ Inline();
this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
@@ -277,6 +278,22 @@ namespace Microsoft.Boogie.Houdini { this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
}
+ private void Inline() {
+ if (CommandLineOptions.Clo.InlineDepth < 0)
+ return;
+ foreach (Implementation impl in callGraph.Nodes) {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ foreach (Implementation impl in callGraph.Nodes) {
+ Inliner.ProcessImplementationForHoudini(program, impl);
+ }
+ foreach (Implementation impl in callGraph.Nodes) {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+
private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {
Dictionary<string, IdentifierExpr> existentialConstants = new Dictionary<string, IdentifierExpr>();
foreach (Declaration decl in program.TopLevelDeclarations) {
|