diff options
Diffstat (limited to 'Source/Core/Inline.cs')
| -rw-r--r-- | Source/Core/Inline.cs | 1538 |
1 files changed, 769 insertions, 769 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index cfeaeb8a..958051d5 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -1,770 +1,770 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.Boogie {
-
- using System;
- using System.IO;
- using System.Collections;
- using System.Collections.Generic;
- using System.Diagnostics.Contracts;
- using BoogiePL=Microsoft.Boogie;
- using System.Diagnostics;
- using System.Text.RegularExpressions; // for procedure inlining
-
- public delegate void InlineCallback(Implementation/*!*/ impl);
-
- public class Inliner : Duplicator {
- protected bool inlinedSomething;
-
- protected Program program;
-
- private InlineCallback inlineCallback;
-
- protected CodeCopier/*!*/ codeCopier;
-
- protected Dictionary<string/*!*/, int>/*!*/ /* Procedure.Name -> int */ recursiveProcUnrollMap;
-
- protected Dictionary<string/*!*/, int>/*!*/ /* Procedure.Name -> int */ inlinedProcLblMap;
-
- protected int inlineDepth;
-
- protected List<Variable>/*!*/ newLocalVars;
-
- protected List<IdentifierExpr>/*!*/ newModifies;
-
- protected string prefix;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(program != null);
- Contract.Invariant(newLocalVars != null);
- Contract.Invariant(newModifies != null);
- Contract.Invariant(codeCopier != null);
- Contract.Invariant(recursiveProcUnrollMap != null);
- Contract.Invariant(inlinedProcLblMap != null);
- }
-
- public override Expr VisitCodeExpr(CodeExpr node)
- {
- Inliner codeExprInliner = new Inliner(program, inlineCallback, CommandLineOptions.Clo.InlineDepth);
- codeExprInliner.newLocalVars.AddRange(node.LocVars);
- codeExprInliner.inlinedProcLblMap = this.inlinedProcLblMap;
- List<Block> newCodeExprBlocks = codeExprInliner.DoInlineBlocks(node.Blocks, ref inlinedSomething);
- return new CodeExpr(codeExprInliner.newLocalVars, newCodeExprBlocks);
- }
-
- protected void NextInlinedProcLabel(string procName) {
- Contract.Requires(procName != null);
- int currentId;
- if (inlinedProcLblMap.TryGetValue(procName, out currentId)) {
- inlinedProcLblMap[procName] = currentId + 1;
- } else {
- inlinedProcLblMap.Add(procName, 0);
- }
- }
-
- protected string GetInlinedProcLabel(string procName) {
- Contract.Requires(procName != null);
- Contract.Ensures(Contract.Result<string>() != null);
- return prefix + procName + "$" + inlinedProcLblMap[procName];
- }
-
- protected string GetProcVarName(string procName, string formalName) {
- Contract.Requires(formalName != null);
- Contract.Requires(procName != null);
- Contract.Ensures(Contract.Result<string>() != null);
- return GetInlinedProcLabel(procName) + "$" + formalName;
- }
-
- public Inliner(Program program, InlineCallback cb, int inlineDepth) {
- this.program = program;
- this.inlinedProcLblMap = new Dictionary<string/*!*/, int>();
- this.recursiveProcUnrollMap = new Dictionary<string/*!*/, int>();
- this.inlineDepth = inlineDepth;
- this.codeCopier = new CodeCopier();
- this.inlineCallback = cb;
- this.newLocalVars = new List<Variable>();
- this.newModifies = new List<IdentifierExpr>();
- this.prefix = null;
- }
-
- // This method calculates a prefix (storing it in the prefix field) so that prepending it to any string
- // is guaranteed not to create a conflict with the names of variables and blocks in scope inside impl.
- protected void ComputePrefix(Program program, Implementation impl)
- {
- this.prefix = "inline$";
- foreach (var v in impl.InParams)
- {
- DistinguishPrefix(v.Name);
- }
- foreach (var v in impl.OutParams)
- {
- DistinguishPrefix(v.Name);
- }
- foreach (var v in impl.LocVars)
- {
- DistinguishPrefix(v.Name);
- }
- foreach (var v in program.GlobalVariables)
- {
- DistinguishPrefix(v.Name);
- }
- foreach (Block b in impl.Blocks)
- {
- DistinguishPrefix(b.Label);
- }
- }
-
- private void DistinguishPrefix(string s)
- {
- if (!s.StartsWith(prefix)) return;
- for (int i = prefix.Length; i < s.Length; i++)
- {
- prefix = prefix + "$";
- if (s[i] != '$') break;
- }
- if (prefix == s)
- {
- prefix = prefix + "$";
- }
- }
-
- protected static void ProcessImplementation(Program program, Implementation impl, Inliner inliner) {
- Contract.Requires(impl != null);
- Contract.Requires(impl.Proc != null);
-
- inliner.ComputePrefix(program, impl);
-
- inliner.newLocalVars.AddRange(impl.LocVars);
- inliner.newModifies.AddRange(impl.Proc.Modifies);
-
- bool inlined = false;
- List<Block> newBlocks = inliner.DoInlineBlocks(impl.Blocks, ref inlined);
- Contract.Assert(cce.NonNullElements(newBlocks));
-
- if (!inlined)
- return;
-
- impl.InParams = new List<Variable>(impl.InParams);
- impl.OutParams = new List<Variable>(impl.OutParams);
- impl.LocVars = inliner.newLocalVars;
- impl.Proc.Modifies = inliner.newModifies;
- impl.Blocks = newBlocks;
-
- impl.ResetImplFormalMap();
-
- // we need to resolve the new code
- inliner.ResolveImpl(impl);
-
- if (CommandLineOptions.Clo.PrintInlined) {
- inliner.EmitImpl(impl);
- }
- }
-
- 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(program, 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, new Inliner(program, null, -1));
- }
-
- protected void EmitImpl(Implementation impl) {
- Contract.Requires(impl != null);
- Contract.Requires(impl.Proc != null);
- Console.WriteLine("after inlining procedure calls");
- impl.Proc.Emit(new TokenTextWriter("<console>", Console.Out, /*pretty=*/ false), 0);
- impl.Emit(new TokenTextWriter("<console>", Console.Out, /*pretty=*/ false), 0);
- }
-
- private sealed class DummyErrorSink : IErrorSink {
- public void Error(IToken tok, string msg) {
- //Contract.Requires(msg != null);
- //Contract.Requires(tok != null);
- // FIXME
- // noop.
- // This is required because during the resolution, some resolution errors happen
- // (such as the ones caused addion of loop invariants J_(block.Label) by the AI package
- }
- }
-
- protected void ResolveImpl(Implementation impl) {
- Contract.Requires(impl != null);
- Contract.Ensures(impl.Proc != null);
- ResolutionContext rc = new ResolutionContext(new DummyErrorSink());
-
- foreach (var decl in program.TopLevelDeclarations) {
- decl.Register(rc);
- }
-
- impl.Proc = null; // to force Resolve() redo the operation
- impl.Resolve(rc);
-
- TypecheckingContext tc = new TypecheckingContext(new DummyErrorSink());
-
- impl.Typecheck(tc);
- }
-
- // Redundant for this class; but gives a chance for other classes to
- // override this and implement their own inlining policy
- protected virtual int GetInlineCount(CallCmd callCmd, Implementation impl)
- {
- return GetInlineCount(impl);
- }
-
- // returns true if it is ok to further unroll the procedure
- // otherwise, the procedure is not inlined at the call site
- protected int GetInlineCount(Implementation impl) {
- Contract.Requires(impl != null);
- Contract.Requires(impl.Proc != null);
-
- string/*!*/ procName = impl.Name;
- Contract.Assert(procName != null);
- int c;
- if (recursiveProcUnrollMap.TryGetValue(procName, out c)) {
- return c;
- }
-
- c = -1; // TryGetValue above always overwrites c
- impl.CheckIntAttribute("inline", ref c);
- // procedure attribute overrides implementation
- impl.Proc.CheckIntAttribute("inline", ref c);
-
- recursiveProcUnrollMap[procName] = c;
- return c;
- }
-
- void CheckRecursion(Implementation impl, Stack<Procedure/*!*/>/*!*/ callStack) {
- Contract.Requires(impl != null);
- Contract.Requires(cce.NonNullElements(callStack));
- foreach (Procedure/*!*/ p in callStack) {
- Contract.Assert(p != null);
- if (p == impl.Proc) {
- string msg = "";
- foreach (Procedure/*!*/ q in callStack) {
- Contract.Assert(q != null);
- msg = q.Name + " -> " + msg;
- }
- msg += p.Name;
- //checkingCtx.Error(impl, "inlined procedure is recursive, call stack: {0}", msg);
- }
- }
- }
-
- private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, List<Cmd> newCmds, List<Block> newBlocks, int lblCount)
- {
- Contract.Assume(impl != null);
- Contract.Assert(cce.NonNull(impl.OriginalBlocks).Count > 0);
-
- // do inline now
- int nextlblCount = lblCount + 1;
- string nextBlockLabel = block.Label + "$" + nextlblCount;
-
- // run the callback before each inline
- if (inlineCallback != null)
- {
- inlineCallback(impl);
- }
-
- // increment the counter for the procedure to be used in constructing the locals and formals
- NextInlinedProcLabel(impl.Proc.Name);
-
- BeginInline(impl);
-
- List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, impl, nextBlockLabel);
- Contract.Assert(cce.NonNullElements(inlinedBlocks));
-
- EndInline();
-
- if (inlineDepth >= 0)
- {
- Debug.Assert(inlineDepth > 0);
- inlineDepth = inlineDepth - 1;
- }
- else
- {
- recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;
- }
-
- bool inlinedSomething = true;
- inlinedBlocks = DoInlineBlocks(inlinedBlocks, ref inlinedSomething);
-
- if (inlineDepth >= 0)
- {
- inlineDepth = inlineDepth + 1;
- }
- else
- {
- recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;
- }
-
- Block/*!*/ startBlock = inlinedBlocks[0];
- Contract.Assert(startBlock != null);
-
- GotoCmd gotoCmd = new GotoCmd(Token.NoToken, new List<String> { startBlock.Label });
- Block newBlock = new Block(block.tok, ((lblCount == 0) ? (block.Label) : (block.Label + "$" + lblCount)), newCmds, gotoCmd);
-
- newBlocks.Add(newBlock);
- newBlocks.AddRange(inlinedBlocks);
-
- return nextlblCount;
- }
-
- public virtual List<Block/*!*/>/*!*/ DoInlineBlocks(List<Block/*!*/>/*!*/ blocks, ref bool inlinedSomething) {
- Contract.Requires(cce.NonNullElements(blocks));
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
- List<Block/*!*/>/*!*/ newBlocks = new List<Block/*!*/>();
-
- foreach (Block block in blocks) {
- TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd);
- List<Cmd> cmds = block.Cmds;
- List<Cmd> newCmds = new List<Cmd>();
- int lblCount = 0;
-
- for (int i = 0; i < cmds.Count; ++i)
- {
- Cmd cmd = cmds[i];
-
- if (cmd is CallCmd)
- {
- CallCmd callCmd = (CallCmd)cmd;
- Implementation impl = FindProcImpl(program, callCmd.Proc);
- if (impl == null)
- {
- newCmds.Add(codeCopier.CopyCmd(callCmd));
- continue;
- }
- int inline = inlineDepth >= 0 ? inlineDepth : GetInlineCount(callCmd, impl);
- if (inline > 0)
- {
- inlinedSomething = true;
- lblCount = InlineCallCmd(block, callCmd, impl, newCmds, newBlocks, lblCount);
- newCmds = new List<Cmd>();
- }
- else if (inline == 0)
- {
- inlinedSomething = true;
- if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert)
- {
- // add assert
- newCmds.Add(new AssertCmd(callCmd.tok, Expr.False));
- }
- else if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assume)
- {
- // add assume
- newCmds.Add(new AssumeCmd(callCmd.tok, Expr.False));
- }
- else
- {
- // add call
- newCmds.Add(codeCopier.CopyCmd(callCmd));
- }
- }
- else
- {
- newCmds.Add(codeCopier.CopyCmd(callCmd));
- }
- }
- else if (cmd is PredicateCmd)
- {
- PredicateCmd predCmd = (PredicateCmd)cmd;
- this.inlinedSomething = false;
- Expr newExpr = this.VisitExpr(predCmd.Expr);
- if (this.inlinedSomething)
- {
- inlinedSomething = true;
- PredicateCmd newPredCmd = (PredicateCmd)codeCopier.CopyCmd(predCmd);
- newPredCmd.Expr = newExpr;
- newCmds.Add(newPredCmd);
- }
- else
- {
- newCmds.Add(codeCopier.CopyCmd(predCmd));
- }
- }
- else if (cmd is AssignCmd)
- {
- AssignCmd assignCmd = (AssignCmd)cmd;
- this.inlinedSomething = false;
- List<Expr> newRhss = new List<Expr>();
- foreach (Expr rhsExpr in assignCmd.Rhss)
- {
- newRhss.Add(this.VisitExpr(rhsExpr));
- }
- if (this.inlinedSomething)
- {
- inlinedSomething = true;
- AssignCmd newAssignCmd = (AssignCmd)codeCopier.CopyCmd(assignCmd);
- newAssignCmd.Rhss = newRhss;
- newCmds.Add(newAssignCmd);
- }
- else
- {
- newCmds.Add(codeCopier.CopyCmd(assignCmd));
- }
- }
- else
- {
- newCmds.Add(codeCopier.CopyCmd(cmd));
- }
- }
-
- Block newBlock = new Block(block.tok, ((lblCount == 0) ? (block.Label) : (block.Label + "$" + lblCount)), newCmds, codeCopier.CopyTransferCmd(transferCmd));
- newBlocks.Add(newBlock);
- }
-
- return newBlocks;
- }
-
- protected void BeginInline(Implementation impl) {
- Contract.Requires(impl != null);
- Contract.Requires(impl.Proc != null);
- Contract.Requires(newModifies != null);
- Contract.Requires(newLocalVars != null);
-
- Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
- Procedure proc = impl.Proc;
-
- foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) {
- Contract.Assert(locVar != null);
- LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, locVar.Name), locVar.TypedIdent.Type, locVar.TypedIdent.WhereExpr));
- localVar.Attributes = locVar.Attributes; // copy attributes
- newLocalVars.Add(localVar);
- IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar);
- substMap.Add(locVar, ie);
- }
-
- for (int i = 0; i < impl.InParams.Count; i++) {
- Variable inVar = cce.NonNull(impl.InParams[i]);
- LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, inVar.Name), inVar.TypedIdent.Type, inVar.TypedIdent.WhereExpr));
- newLocalVars.Add(localVar);
- if (impl.Proc != null) localVar.Attributes = impl.Proc.InParams[i].Attributes; // copy attributes
- IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar);
- substMap.Add(inVar, ie);
- // also add a substitution from the corresponding formal occurring in the PROCEDURE declaration
- Variable procInVar = cce.NonNull(proc.InParams[i]);
- if (procInVar != inVar) {
- substMap.Add(procInVar, ie);
- }
- }
-
- for (int i = 0; i < impl.OutParams.Count; i++) {
- Variable outVar = cce.NonNull(impl.OutParams[i]);
- LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, outVar.Name), outVar.TypedIdent.Type, outVar.TypedIdent.WhereExpr));
- if (impl.Proc != null) localVar.Attributes = impl.Proc.OutParams[i].Attributes; // copy attributes
- newLocalVars.Add(localVar);
- IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar);
- substMap.Add(outVar, ie);
- // also add a substitution from the corresponding formal occurring in the PROCEDURE declaration
- Variable procOutVar = cce.NonNull(proc.OutParams[i]);
- if (procOutVar != outVar) {
- substMap.Add(procOutVar, ie);
- }
- }
-
- Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();
-
- foreach (IdentifierExpr/*!*/ mie in proc.Modifies) {
- Contract.Assert(mie != null);
- Variable/*!*/ mVar = cce.NonNull(mie.Decl);
- LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, mVar.Name), mVar.TypedIdent.Type));
- newLocalVars.Add(localVar);
- IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar);
- substMapOld.Add(mVar, ie);
- // FIXME why are we doing this? the modifies list should already include them.
- // add the modified variable to the modifies list of the procedure
- if (!newModifies.Contains(mie)) {
- newModifies.Add(mie);
- }
- }
-
- codeCopier.Subst = Substituter.SubstitutionFromHashtable(substMap);
- codeCopier.OldSubst = Substituter.SubstitutionFromHashtable(substMapOld);
- }
-
- protected void EndInline() {
- codeCopier.Subst = null;
- codeCopier.OldSubst = null;
- }
-
- private Cmd InlinedRequires(CallCmd callCmd, Requires req) {
- Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
- if (req.Free)
- reqCopy.Condition = Expr.True;
- else
- reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
- AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);
- a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
- return a;
- }
-
- private Cmd InlinedEnsures(CallCmd callCmd, Ensures ens) {
- if (QKeyValue.FindBoolAttribute(ens.Attributes, "InlineAssume")) {
- return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
- } else if (ens.Free) {
- return new AssumeCmd(ens.tok, Expr.True);
- } else {
- Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());
- ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
- return new AssertEnsuresCmd(ensCopy);
- }
- }
-
- private List<Cmd> RemoveAsserts(List<Cmd> cmds) {
- List<Cmd> newCmdSeq = new List<Cmd>();
- for (int i = 0; i < cmds.Count; 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);
- Contract.Requires(impl != null);
- Contract.Requires(impl.Proc != null);
- Contract.Requires(callCmd != null);
- Contract.Requires(codeCopier.Subst != null);
-
- Contract.Requires(codeCopier.OldSubst != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
- List<Block/*!*/>/*!*/ implBlocks = cce.NonNull(impl.OriginalBlocks);
- Contract.Assert(implBlocks.Count > 0);
-
- Procedure proc = impl.Proc;
- string startLabel = implBlocks[0].Label;
-
- List<Block/*!*/>/*!*/ inlinedBlocks = new List<Block/*!*/>();
-
- // create in block
- List<Cmd> inCmds = new List<Cmd>();
-
- // assign in parameters
- for (int i = 0; i < impl.InParams.Count; ++i) {
- Cmd cmd = Cmd.SimpleAssign(impl.tok,
- (IdentifierExpr)cce.NonNull(codeCopier.Subst)(cce.NonNull(impl.InParams[i])),
- cce.NonNull(callCmd.Ins[i]));
- inCmds.Add(cmd);
- }
-
- // inject requires
- for (int i = 0; i < proc.Requires.Count; i++) {
- Requires/*!*/ req = cce.NonNull(proc.Requires[i]);
- inCmds.Add(InlinedRequires(callCmd, req));
- }
-
- List<Variable> locVars = cce.NonNull(impl.OriginalLocVars);
-
- // havoc locals and out parameters in case procedure is invoked in a loop
- List<IdentifierExpr> havocVars = new List<IdentifierExpr>();
- foreach (Variable v in locVars)
- {
- havocVars.Add((IdentifierExpr)codeCopier.Subst(v));
- }
- foreach (Variable v in impl.OutParams)
- {
- havocVars.Add((IdentifierExpr)codeCopier.Subst(v));
- }
- if (havocVars.Count > 0)
- {
- inCmds.Add(new HavocCmd(Token.NoToken, havocVars));
- }
-
- // add where clauses of local vars as assume
- for (int i = 0; i < locVars.Count; ++i) {
- Expr whereExpr = (cce.NonNull(locVars[i])).TypedIdent.WhereExpr;
- if (whereExpr != null) {
- whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);
- // FIXME we cannot overwrite it, can we?!
- (cce.NonNull(locVars[i])).TypedIdent.WhereExpr = whereExpr;
- AssumeCmd/*!*/ a = new AssumeCmd(Token.NoToken, whereExpr);
- Contract.Assert(a != null);
- inCmds.Add(a);
- }
- }
-
- // add where clauses of output params as assume
- for (int i = 0; i < impl.OutParams.Count; ++i) {
- Expr whereExpr = (cce.NonNull(impl.OutParams[i])).TypedIdent.WhereExpr;
- if (whereExpr != null) {
- whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);
- // FIXME likewise
- (cce.NonNull(impl.OutParams[i])).TypedIdent.WhereExpr = whereExpr;
- AssumeCmd/*!*/ a = new AssumeCmd(Token.NoToken, whereExpr);
- Contract.Assert(a != null);
- inCmds.Add(a);
- }
- }
-
- // assign modifies old values
- foreach (IdentifierExpr/*!*/ mie in proc.Modifies) {
- Contract.Assert(mie != null);
- Variable/*!*/ mvar = cce.NonNull(mie.Decl);
- AssignCmd assign = Cmd.SimpleAssign(impl.tok, (IdentifierExpr)cce.NonNull(codeCopier.OldSubst(mvar)), mie);
- inCmds.Add(assign);
- }
-
- GotoCmd inGotoCmd = new GotoCmd(callCmd.tok, new List<String> { GetInlinedProcLabel(proc.Name) + "$" + startLabel });
- Block inBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Entry", inCmds, inGotoCmd);
- inlinedBlocks.Add(inBlock);
-
- // inject the blocks of the implementation
- Block intBlock;
- foreach (Block block in implBlocks) {
- List<Cmd> 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);
- }
-
- // create out block
- List<Cmd> outCmds = new List<Cmd>();
-
- // inject ensures
- for (int i = 0; i < proc.Ensures.Count; i++) {
- Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);
- outCmds.Add(InlinedEnsures(callCmd, ens));
- }
-
- // assign out params
- for (int i = 0; i < impl.OutParams.Count; ++i) {
- Expr/*!*/ cout_exp = (IdentifierExpr)cce.NonNull(codeCopier.Subst(cce.NonNull(impl.OutParams[i])));
- Cmd cmd = Cmd.SimpleAssign(impl.tok, cce.NonNull(callCmd.Outs[i]), cout_exp);
- outCmds.Add(cmd);
- }
-
- // create out block
- GotoCmd outGotoCmd = new GotoCmd(Token.NoToken, new List<String> { nextBlockLabel });
- Block outBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Return", outCmds, outGotoCmd);
- inlinedBlocks.Add(outBlock);
-
- return inlinedBlocks;
- }
-
- protected TransferCmd CreateInlinedTransferCmd(TransferCmd transferCmd, string procLabel) {
- Contract.Requires(procLabel != null);
- Contract.Requires(transferCmd != null);
- TransferCmd newTransferCmd;
-
- GotoCmd gotoCmd = transferCmd as GotoCmd;
- if (gotoCmd != null) {
- List<String> gotoSeq = gotoCmd.labelNames;
- List<String> newGotoSeq = new List<String>();
- foreach (string/*!*/ blockLabel in cce.NonNull(gotoSeq)) {
- Contract.Assert(blockLabel != null);
- newGotoSeq.Add(procLabel + "$" + blockLabel);
- }
- newTransferCmd = new GotoCmd(transferCmd.tok, newGotoSeq);
- } else {
- newTransferCmd = new GotoCmd(transferCmd.tok, new List<String> { procLabel + "$Return" });
- }
-
- return newTransferCmd;
- }
-
- protected static Implementation FindProcImpl(Program program, Procedure proc) {
- Contract.Requires(program != null);
- foreach (var impl in program.Implementations) {
- if (impl.Proc == proc) {
- return impl;
- }
- }
- return null;
- }
- }
-
- ///////////////////////////////////////////////////////////////////////////////////////////////////////////////
-
- public class CodeCopier {
- public Substitution Subst;
- public Substitution OldSubst;
-
- public CodeCopier(Dictionary<Variable, Expr> substMap) {
- Contract.Requires(substMap != null);
- Subst = Substituter.SubstitutionFromHashtable(substMap);
- }
-
- public CodeCopier(Dictionary<Variable, Expr> substMap, Dictionary<Variable, Expr> oldSubstMap) {
- Contract.Requires(oldSubstMap != null);
- Contract.Requires(substMap != null);
- Subst = Substituter.SubstitutionFromHashtable(substMap);
- OldSubst = Substituter.SubstitutionFromHashtable(oldSubstMap);
- }
-
- public CodeCopier() {
- }
-
- public List<Cmd> CopyCmdSeq(List<Cmd> cmds) {
- Contract.Requires(cmds != null);
- Contract.Ensures(Contract.Result<List<Cmd>>() != null);
- List<Cmd> newCmds = new List<Cmd>();
- foreach (Cmd/*!*/ cmd in cmds) {
- Contract.Assert(cmd != null);
- newCmds.Add(CopyCmd(cmd));
- }
- return newCmds;
- }
-
- public TransferCmd CopyTransferCmd(TransferCmd cmd) {
- Contract.Requires(cmd != null);
- Contract.Ensures(Contract.Result<TransferCmd>() != null);
- TransferCmd transferCmd;
- GotoCmd gotocmd = cmd as GotoCmd;
- if (gotocmd != null) {
- Contract.Assert(gotocmd.labelNames != null);
- List<String> labels = new List<String>();
- labels.AddRange(gotocmd.labelNames);
- transferCmd = new GotoCmd(cmd.tok, labels);
- } else {
- ReturnExprCmd returnExprCmd = cmd as ReturnExprCmd;
- if (returnExprCmd != null)
- {
- transferCmd = new ReturnExprCmd(cmd.tok, CopyExpr(returnExprCmd.Expr));
- }
- else
- {
- transferCmd = new ReturnCmd(cmd.tok);
- }
- }
- return transferCmd;
- }
-
- public Cmd CopyCmd(Cmd cmd) {
- Contract.Requires(cmd != null);
- Contract.Ensures(Contract.Result<Cmd>() != null);
- if (Subst == null) {
- return cmd;
- } else if (OldSubst == null) {
- return Substituter.Apply(Subst, cmd);
- } else {
- return Substituter.ApplyReplacingOldExprs(Subst, OldSubst, cmd);
- }
- }
-
- public Expr CopyExpr(Expr expr) {
- Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<Expr>() != null);
- if (Subst == null) {
- return expr;
- } else if (OldSubst == null) {
- return Substituter.Apply(Subst, expr);
- } else {
- return Substituter.ApplyReplacingOldExprs(Subst, OldSubst, expr);
- }
- }
- } // end class CodeCopier
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.Boogie { + + using System; + using System.IO; + using System.Collections; + using System.Collections.Generic; + using System.Diagnostics.Contracts; + using BoogiePL=Microsoft.Boogie; + using System.Diagnostics; + using System.Text.RegularExpressions; // for procedure inlining + + public delegate void InlineCallback(Implementation/*!*/ impl); + + public class Inliner : Duplicator { + protected bool inlinedSomething; + + protected Program program; + + private InlineCallback inlineCallback; + + protected CodeCopier/*!*/ codeCopier; + + protected Dictionary<string/*!*/, int>/*!*/ /* Procedure.Name -> int */ recursiveProcUnrollMap; + + protected Dictionary<string/*!*/, int>/*!*/ /* Procedure.Name -> int */ inlinedProcLblMap; + + protected int inlineDepth; + + protected List<Variable>/*!*/ newLocalVars; + + protected List<IdentifierExpr>/*!*/ newModifies; + + protected string prefix; + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(program != null); + Contract.Invariant(newLocalVars != null); + Contract.Invariant(newModifies != null); + Contract.Invariant(codeCopier != null); + Contract.Invariant(recursiveProcUnrollMap != null); + Contract.Invariant(inlinedProcLblMap != null); + } + + public override Expr VisitCodeExpr(CodeExpr node) + { + Inliner codeExprInliner = new Inliner(program, inlineCallback, CommandLineOptions.Clo.InlineDepth); + codeExprInliner.newLocalVars.AddRange(node.LocVars); + codeExprInliner.inlinedProcLblMap = this.inlinedProcLblMap; + List<Block> newCodeExprBlocks = codeExprInliner.DoInlineBlocks(node.Blocks, ref inlinedSomething); + return new CodeExpr(codeExprInliner.newLocalVars, newCodeExprBlocks); + } + + protected void NextInlinedProcLabel(string procName) { + Contract.Requires(procName != null); + int currentId; + if (inlinedProcLblMap.TryGetValue(procName, out currentId)) { + inlinedProcLblMap[procName] = currentId + 1; + } else { + inlinedProcLblMap.Add(procName, 0); + } + } + + protected string GetInlinedProcLabel(string procName) { + Contract.Requires(procName != null); + Contract.Ensures(Contract.Result<string>() != null); + return prefix + procName + "$" + inlinedProcLblMap[procName]; + } + + protected string GetProcVarName(string procName, string formalName) { + Contract.Requires(formalName != null); + Contract.Requires(procName != null); + Contract.Ensures(Contract.Result<string>() != null); + return GetInlinedProcLabel(procName) + "$" + formalName; + } + + public Inliner(Program program, InlineCallback cb, int inlineDepth) { + this.program = program; + this.inlinedProcLblMap = new Dictionary<string/*!*/, int>(); + this.recursiveProcUnrollMap = new Dictionary<string/*!*/, int>(); + this.inlineDepth = inlineDepth; + this.codeCopier = new CodeCopier(); + this.inlineCallback = cb; + this.newLocalVars = new List<Variable>(); + this.newModifies = new List<IdentifierExpr>(); + this.prefix = null; + } + + // This method calculates a prefix (storing it in the prefix field) so that prepending it to any string + // is guaranteed not to create a conflict with the names of variables and blocks in scope inside impl. + protected void ComputePrefix(Program program, Implementation impl) + { + this.prefix = "inline$"; + foreach (var v in impl.InParams) + { + DistinguishPrefix(v.Name); + } + foreach (var v in impl.OutParams) + { + DistinguishPrefix(v.Name); + } + foreach (var v in impl.LocVars) + { + DistinguishPrefix(v.Name); + } + foreach (var v in program.GlobalVariables) + { + DistinguishPrefix(v.Name); + } + foreach (Block b in impl.Blocks) + { + DistinguishPrefix(b.Label); + } + } + + private void DistinguishPrefix(string s) + { + if (!s.StartsWith(prefix)) return; + for (int i = prefix.Length; i < s.Length; i++) + { + prefix = prefix + "$"; + if (s[i] != '$') break; + } + if (prefix == s) + { + prefix = prefix + "$"; + } + } + + protected static void ProcessImplementation(Program program, Implementation impl, Inliner inliner) { + Contract.Requires(impl != null); + Contract.Requires(impl.Proc != null); + + inliner.ComputePrefix(program, impl); + + inliner.newLocalVars.AddRange(impl.LocVars); + inliner.newModifies.AddRange(impl.Proc.Modifies); + + bool inlined = false; + List<Block> newBlocks = inliner.DoInlineBlocks(impl.Blocks, ref inlined); + Contract.Assert(cce.NonNullElements(newBlocks)); + + if (!inlined) + return; + + impl.InParams = new List<Variable>(impl.InParams); + impl.OutParams = new List<Variable>(impl.OutParams); + impl.LocVars = inliner.newLocalVars; + impl.Proc.Modifies = inliner.newModifies; + impl.Blocks = newBlocks; + + impl.ResetImplFormalMap(); + + // we need to resolve the new code + inliner.ResolveImpl(impl); + + if (CommandLineOptions.Clo.PrintInlined) { + inliner.EmitImpl(impl); + } + } + + 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(program, 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, new Inliner(program, null, -1)); + } + + protected void EmitImpl(Implementation impl) { + Contract.Requires(impl != null); + Contract.Requires(impl.Proc != null); + Console.WriteLine("after inlining procedure calls"); + impl.Proc.Emit(new TokenTextWriter("<console>", Console.Out, /*pretty=*/ false), 0); + impl.Emit(new TokenTextWriter("<console>", Console.Out, /*pretty=*/ false), 0); + } + + private sealed class DummyErrorSink : IErrorSink { + public void Error(IToken tok, string msg) { + //Contract.Requires(msg != null); + //Contract.Requires(tok != null); + // FIXME + // noop. + // This is required because during the resolution, some resolution errors happen + // (such as the ones caused addion of loop invariants J_(block.Label) by the AI package + } + } + + protected void ResolveImpl(Implementation impl) { + Contract.Requires(impl != null); + Contract.Ensures(impl.Proc != null); + ResolutionContext rc = new ResolutionContext(new DummyErrorSink()); + + foreach (var decl in program.TopLevelDeclarations) { + decl.Register(rc); + } + + impl.Proc = null; // to force Resolve() redo the operation + impl.Resolve(rc); + + TypecheckingContext tc = new TypecheckingContext(new DummyErrorSink()); + + impl.Typecheck(tc); + } + + // Redundant for this class; but gives a chance for other classes to + // override this and implement their own inlining policy + protected virtual int GetInlineCount(CallCmd callCmd, Implementation impl) + { + return GetInlineCount(impl); + } + + // returns true if it is ok to further unroll the procedure + // otherwise, the procedure is not inlined at the call site + protected int GetInlineCount(Implementation impl) { + Contract.Requires(impl != null); + Contract.Requires(impl.Proc != null); + + string/*!*/ procName = impl.Name; + Contract.Assert(procName != null); + int c; + if (recursiveProcUnrollMap.TryGetValue(procName, out c)) { + return c; + } + + c = -1; // TryGetValue above always overwrites c + impl.CheckIntAttribute("inline", ref c); + // procedure attribute overrides implementation + impl.Proc.CheckIntAttribute("inline", ref c); + + recursiveProcUnrollMap[procName] = c; + return c; + } + + void CheckRecursion(Implementation impl, Stack<Procedure/*!*/>/*!*/ callStack) { + Contract.Requires(impl != null); + Contract.Requires(cce.NonNullElements(callStack)); + foreach (Procedure/*!*/ p in callStack) { + Contract.Assert(p != null); + if (p == impl.Proc) { + string msg = ""; + foreach (Procedure/*!*/ q in callStack) { + Contract.Assert(q != null); + msg = q.Name + " -> " + msg; + } + msg += p.Name; + //checkingCtx.Error(impl, "inlined procedure is recursive, call stack: {0}", msg); + } + } + } + + private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, List<Cmd> newCmds, List<Block> newBlocks, int lblCount) + { + Contract.Assume(impl != null); + Contract.Assert(cce.NonNull(impl.OriginalBlocks).Count > 0); + + // do inline now + int nextlblCount = lblCount + 1; + string nextBlockLabel = block.Label + "$" + nextlblCount; + + // run the callback before each inline + if (inlineCallback != null) + { + inlineCallback(impl); + } + + // increment the counter for the procedure to be used in constructing the locals and formals + NextInlinedProcLabel(impl.Proc.Name); + + BeginInline(impl); + + List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, impl, nextBlockLabel); + Contract.Assert(cce.NonNullElements(inlinedBlocks)); + + EndInline(); + + if (inlineDepth >= 0) + { + Debug.Assert(inlineDepth > 0); + inlineDepth = inlineDepth - 1; + } + else + { + recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1; + } + + bool inlinedSomething = true; + inlinedBlocks = DoInlineBlocks(inlinedBlocks, ref inlinedSomething); + + if (inlineDepth >= 0) + { + inlineDepth = inlineDepth + 1; + } + else + { + recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1; + } + + Block/*!*/ startBlock = inlinedBlocks[0]; + Contract.Assert(startBlock != null); + + GotoCmd gotoCmd = new GotoCmd(Token.NoToken, new List<String> { startBlock.Label }); + Block newBlock = new Block(block.tok, ((lblCount == 0) ? (block.Label) : (block.Label + "$" + lblCount)), newCmds, gotoCmd); + + newBlocks.Add(newBlock); + newBlocks.AddRange(inlinedBlocks); + + return nextlblCount; + } + + public virtual List<Block/*!*/>/*!*/ DoInlineBlocks(List<Block/*!*/>/*!*/ blocks, ref bool inlinedSomething) { + Contract.Requires(cce.NonNullElements(blocks)); + Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>())); + List<Block/*!*/>/*!*/ newBlocks = new List<Block/*!*/>(); + + foreach (Block block in blocks) { + TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd); + List<Cmd> cmds = block.Cmds; + List<Cmd> newCmds = new List<Cmd>(); + int lblCount = 0; + + for (int i = 0; i < cmds.Count; ++i) + { + Cmd cmd = cmds[i]; + + if (cmd is CallCmd) + { + CallCmd callCmd = (CallCmd)cmd; + Implementation impl = FindProcImpl(program, callCmd.Proc); + if (impl == null) + { + newCmds.Add(codeCopier.CopyCmd(callCmd)); + continue; + } + int inline = inlineDepth >= 0 ? inlineDepth : GetInlineCount(callCmd, impl); + if (inline > 0) + { + inlinedSomething = true; + lblCount = InlineCallCmd(block, callCmd, impl, newCmds, newBlocks, lblCount); + newCmds = new List<Cmd>(); + } + else if (inline == 0) + { + inlinedSomething = true; + if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) + { + // add assert + newCmds.Add(new AssertCmd(callCmd.tok, Expr.False)); + } + else if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assume) + { + // add assume + newCmds.Add(new AssumeCmd(callCmd.tok, Expr.False)); + } + else + { + // add call + newCmds.Add(codeCopier.CopyCmd(callCmd)); + } + } + else + { + newCmds.Add(codeCopier.CopyCmd(callCmd)); + } + } + else if (cmd is PredicateCmd) + { + PredicateCmd predCmd = (PredicateCmd)cmd; + this.inlinedSomething = false; + Expr newExpr = this.VisitExpr(predCmd.Expr); + if (this.inlinedSomething) + { + inlinedSomething = true; + PredicateCmd newPredCmd = (PredicateCmd)codeCopier.CopyCmd(predCmd); + newPredCmd.Expr = newExpr; + newCmds.Add(newPredCmd); + } + else + { + newCmds.Add(codeCopier.CopyCmd(predCmd)); + } + } + else if (cmd is AssignCmd) + { + AssignCmd assignCmd = (AssignCmd)cmd; + this.inlinedSomething = false; + List<Expr> newRhss = new List<Expr>(); + foreach (Expr rhsExpr in assignCmd.Rhss) + { + newRhss.Add(this.VisitExpr(rhsExpr)); + } + if (this.inlinedSomething) + { + inlinedSomething = true; + AssignCmd newAssignCmd = (AssignCmd)codeCopier.CopyCmd(assignCmd); + newAssignCmd.Rhss = newRhss; + newCmds.Add(newAssignCmd); + } + else + { + newCmds.Add(codeCopier.CopyCmd(assignCmd)); + } + } + else + { + newCmds.Add(codeCopier.CopyCmd(cmd)); + } + } + + Block newBlock = new Block(block.tok, ((lblCount == 0) ? (block.Label) : (block.Label + "$" + lblCount)), newCmds, codeCopier.CopyTransferCmd(transferCmd)); + newBlocks.Add(newBlock); + } + + return newBlocks; + } + + protected void BeginInline(Implementation impl) { + Contract.Requires(impl != null); + Contract.Requires(impl.Proc != null); + Contract.Requires(newModifies != null); + Contract.Requires(newLocalVars != null); + + Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>(); + Procedure proc = impl.Proc; + + foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) { + Contract.Assert(locVar != null); + LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, locVar.Name), locVar.TypedIdent.Type, locVar.TypedIdent.WhereExpr)); + localVar.Attributes = locVar.Attributes; // copy attributes + newLocalVars.Add(localVar); + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar); + substMap.Add(locVar, ie); + } + + for (int i = 0; i < impl.InParams.Count; i++) { + Variable inVar = cce.NonNull(impl.InParams[i]); + LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, inVar.Name), inVar.TypedIdent.Type, inVar.TypedIdent.WhereExpr)); + newLocalVars.Add(localVar); + if (impl.Proc != null) localVar.Attributes = impl.Proc.InParams[i].Attributes; // copy attributes + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar); + substMap.Add(inVar, ie); + // also add a substitution from the corresponding formal occurring in the PROCEDURE declaration + Variable procInVar = cce.NonNull(proc.InParams[i]); + if (procInVar != inVar) { + substMap.Add(procInVar, ie); + } + } + + for (int i = 0; i < impl.OutParams.Count; i++) { + Variable outVar = cce.NonNull(impl.OutParams[i]); + LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, outVar.Name), outVar.TypedIdent.Type, outVar.TypedIdent.WhereExpr)); + if (impl.Proc != null) localVar.Attributes = impl.Proc.OutParams[i].Attributes; // copy attributes + newLocalVars.Add(localVar); + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar); + substMap.Add(outVar, ie); + // also add a substitution from the corresponding formal occurring in the PROCEDURE declaration + Variable procOutVar = cce.NonNull(proc.OutParams[i]); + if (procOutVar != outVar) { + substMap.Add(procOutVar, ie); + } + } + + Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>(); + + foreach (IdentifierExpr/*!*/ mie in proc.Modifies) { + Contract.Assert(mie != null); + Variable/*!*/ mVar = cce.NonNull(mie.Decl); + LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, mVar.Name), mVar.TypedIdent.Type)); + newLocalVars.Add(localVar); + IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar); + substMapOld.Add(mVar, ie); + // FIXME why are we doing this? the modifies list should already include them. + // add the modified variable to the modifies list of the procedure + if (!newModifies.Contains(mie)) { + newModifies.Add(mie); + } + } + + codeCopier.Subst = Substituter.SubstitutionFromHashtable(substMap); + codeCopier.OldSubst = Substituter.SubstitutionFromHashtable(substMapOld); + } + + protected void EndInline() { + codeCopier.Subst = null; + codeCopier.OldSubst = null; + } + + private Cmd InlinedRequires(CallCmd callCmd, Requires req) { + Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone()); + if (req.Free) + reqCopy.Condition = Expr.True; + else + reqCopy.Condition = codeCopier.CopyExpr(req.Condition); + AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy); + a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced; + return a; + } + + private Cmd InlinedEnsures(CallCmd callCmd, Ensures ens) { + if (QKeyValue.FindBoolAttribute(ens.Attributes, "InlineAssume")) { + return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition)); + } else if (ens.Free) { + return new AssumeCmd(ens.tok, Expr.True); + } else { + Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone()); + ensCopy.Condition = codeCopier.CopyExpr(ens.Condition); + return new AssertEnsuresCmd(ensCopy); + } + } + + private List<Cmd> RemoveAsserts(List<Cmd> cmds) { + List<Cmd> newCmdSeq = new List<Cmd>(); + for (int i = 0; i < cmds.Count; 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); + Contract.Requires(impl != null); + Contract.Requires(impl.Proc != null); + Contract.Requires(callCmd != null); + Contract.Requires(codeCopier.Subst != null); + + Contract.Requires(codeCopier.OldSubst != null); + Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>())); + List<Block/*!*/>/*!*/ implBlocks = cce.NonNull(impl.OriginalBlocks); + Contract.Assert(implBlocks.Count > 0); + + Procedure proc = impl.Proc; + string startLabel = implBlocks[0].Label; + + List<Block/*!*/>/*!*/ inlinedBlocks = new List<Block/*!*/>(); + + // create in block + List<Cmd> inCmds = new List<Cmd>(); + + // assign in parameters + for (int i = 0; i < impl.InParams.Count; ++i) { + Cmd cmd = Cmd.SimpleAssign(impl.tok, + (IdentifierExpr)cce.NonNull(codeCopier.Subst)(cce.NonNull(impl.InParams[i])), + cce.NonNull(callCmd.Ins[i])); + inCmds.Add(cmd); + } + + // inject requires + for (int i = 0; i < proc.Requires.Count; i++) { + Requires/*!*/ req = cce.NonNull(proc.Requires[i]); + inCmds.Add(InlinedRequires(callCmd, req)); + } + + List<Variable> locVars = cce.NonNull(impl.OriginalLocVars); + + // havoc locals and out parameters in case procedure is invoked in a loop + List<IdentifierExpr> havocVars = new List<IdentifierExpr>(); + foreach (Variable v in locVars) + { + havocVars.Add((IdentifierExpr)codeCopier.Subst(v)); + } + foreach (Variable v in impl.OutParams) + { + havocVars.Add((IdentifierExpr)codeCopier.Subst(v)); + } + if (havocVars.Count > 0) + { + inCmds.Add(new HavocCmd(Token.NoToken, havocVars)); + } + + // add where clauses of local vars as assume + for (int i = 0; i < locVars.Count; ++i) { + Expr whereExpr = (cce.NonNull(locVars[i])).TypedIdent.WhereExpr; + if (whereExpr != null) { + whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr); + // FIXME we cannot overwrite it, can we?! + (cce.NonNull(locVars[i])).TypedIdent.WhereExpr = whereExpr; + AssumeCmd/*!*/ a = new AssumeCmd(Token.NoToken, whereExpr); + Contract.Assert(a != null); + inCmds.Add(a); + } + } + + // add where clauses of output params as assume + for (int i = 0; i < impl.OutParams.Count; ++i) { + Expr whereExpr = (cce.NonNull(impl.OutParams[i])).TypedIdent.WhereExpr; + if (whereExpr != null) { + whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr); + // FIXME likewise + (cce.NonNull(impl.OutParams[i])).TypedIdent.WhereExpr = whereExpr; + AssumeCmd/*!*/ a = new AssumeCmd(Token.NoToken, whereExpr); + Contract.Assert(a != null); + inCmds.Add(a); + } + } + + // assign modifies old values + foreach (IdentifierExpr/*!*/ mie in proc.Modifies) { + Contract.Assert(mie != null); + Variable/*!*/ mvar = cce.NonNull(mie.Decl); + AssignCmd assign = Cmd.SimpleAssign(impl.tok, (IdentifierExpr)cce.NonNull(codeCopier.OldSubst(mvar)), mie); + inCmds.Add(assign); + } + + GotoCmd inGotoCmd = new GotoCmd(callCmd.tok, new List<String> { GetInlinedProcLabel(proc.Name) + "$" + startLabel }); + Block inBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Entry", inCmds, inGotoCmd); + inlinedBlocks.Add(inBlock); + + // inject the blocks of the implementation + Block intBlock; + foreach (Block block in implBlocks) { + List<Cmd> 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); + } + + // create out block + List<Cmd> outCmds = new List<Cmd>(); + + // inject ensures + for (int i = 0; i < proc.Ensures.Count; i++) { + Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]); + outCmds.Add(InlinedEnsures(callCmd, ens)); + } + + // assign out params + for (int i = 0; i < impl.OutParams.Count; ++i) { + Expr/*!*/ cout_exp = (IdentifierExpr)cce.NonNull(codeCopier.Subst(cce.NonNull(impl.OutParams[i]))); + Cmd cmd = Cmd.SimpleAssign(impl.tok, cce.NonNull(callCmd.Outs[i]), cout_exp); + outCmds.Add(cmd); + } + + // create out block + GotoCmd outGotoCmd = new GotoCmd(Token.NoToken, new List<String> { nextBlockLabel }); + Block outBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Return", outCmds, outGotoCmd); + inlinedBlocks.Add(outBlock); + + return inlinedBlocks; + } + + protected TransferCmd CreateInlinedTransferCmd(TransferCmd transferCmd, string procLabel) { + Contract.Requires(procLabel != null); + Contract.Requires(transferCmd != null); + TransferCmd newTransferCmd; + + GotoCmd gotoCmd = transferCmd as GotoCmd; + if (gotoCmd != null) { + List<String> gotoSeq = gotoCmd.labelNames; + List<String> newGotoSeq = new List<String>(); + foreach (string/*!*/ blockLabel in cce.NonNull(gotoSeq)) { + Contract.Assert(blockLabel != null); + newGotoSeq.Add(procLabel + "$" + blockLabel); + } + newTransferCmd = new GotoCmd(transferCmd.tok, newGotoSeq); + } else { + newTransferCmd = new GotoCmd(transferCmd.tok, new List<String> { procLabel + "$Return" }); + } + + return newTransferCmd; + } + + protected static Implementation FindProcImpl(Program program, Procedure proc) { + Contract.Requires(program != null); + foreach (var impl in program.Implementations) { + if (impl.Proc == proc) { + return impl; + } + } + return null; + } + } + + /////////////////////////////////////////////////////////////////////////////////////////////////////////////// + + public class CodeCopier { + public Substitution Subst; + public Substitution OldSubst; + + public CodeCopier(Dictionary<Variable, Expr> substMap) { + Contract.Requires(substMap != null); + Subst = Substituter.SubstitutionFromHashtable(substMap); + } + + public CodeCopier(Dictionary<Variable, Expr> substMap, Dictionary<Variable, Expr> oldSubstMap) { + Contract.Requires(oldSubstMap != null); + Contract.Requires(substMap != null); + Subst = Substituter.SubstitutionFromHashtable(substMap); + OldSubst = Substituter.SubstitutionFromHashtable(oldSubstMap); + } + + public CodeCopier() { + } + + public List<Cmd> CopyCmdSeq(List<Cmd> cmds) { + Contract.Requires(cmds != null); + Contract.Ensures(Contract.Result<List<Cmd>>() != null); + List<Cmd> newCmds = new List<Cmd>(); + foreach (Cmd/*!*/ cmd in cmds) { + Contract.Assert(cmd != null); + newCmds.Add(CopyCmd(cmd)); + } + return newCmds; + } + + public TransferCmd CopyTransferCmd(TransferCmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result<TransferCmd>() != null); + TransferCmd transferCmd; + GotoCmd gotocmd = cmd as GotoCmd; + if (gotocmd != null) { + Contract.Assert(gotocmd.labelNames != null); + List<String> labels = new List<String>(); + labels.AddRange(gotocmd.labelNames); + transferCmd = new GotoCmd(cmd.tok, labels); + } else { + ReturnExprCmd returnExprCmd = cmd as ReturnExprCmd; + if (returnExprCmd != null) + { + transferCmd = new ReturnExprCmd(cmd.tok, CopyExpr(returnExprCmd.Expr)); + } + else + { + transferCmd = new ReturnCmd(cmd.tok); + } + } + return transferCmd; + } + + public Cmd CopyCmd(Cmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result<Cmd>() != null); + if (Subst == null) { + return cmd; + } else if (OldSubst == null) { + return Substituter.Apply(Subst, cmd); + } else { + return Substituter.ApplyReplacingOldExprs(Subst, OldSubst, cmd); + } + } + + public Expr CopyExpr(Expr expr) { + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result<Expr>() != null); + if (Subst == null) { + return expr; + } else if (OldSubst == null) { + return Substituter.Apply(Subst, expr); + } else { + return Substituter.ApplyReplacingOldExprs(Subst, OldSubst, expr); + } + } + } // end class CodeCopier } // end namespace
\ No newline at end of file |