From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Core/Inline.cs | 1538 ++++++++++++++++++++++++------------------------- 1 file changed, 769 insertions(+), 769 deletions(-) (limited to 'Source/Core/Inline.cs') 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/*!*/ /* Procedure.Name -> int */ recursiveProcUnrollMap; - - protected Dictionary/*!*/ /* Procedure.Name -> int */ inlinedProcLblMap; - - protected int inlineDepth; - - protected List/*!*/ newLocalVars; - - protected List/*!*/ 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 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() != 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() != null); - return GetInlinedProcLabel(procName) + "$" + formalName; - } - - public Inliner(Program program, InlineCallback cb, int inlineDepth) { - this.program = program; - this.inlinedProcLblMap = new Dictionary(); - this.recursiveProcUnrollMap = new Dictionary(); - this.inlineDepth = inlineDepth; - this.codeCopier = new CodeCopier(); - this.inlineCallback = cb; - this.newLocalVars = new List(); - this.newModifies = new List(); - 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 newBlocks = inliner.DoInlineBlocks(impl.Blocks, ref inlined); - Contract.Assert(cce.NonNullElements(newBlocks)); - - if (!inlined) - return; - - impl.InParams = new List(impl.InParams); - impl.OutParams = new List(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.Out, /*pretty=*/ false), 0); - impl.Emit(new TokenTextWriter("", 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/*!*/ 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 newCmds, List 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/*!*/ 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 { 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/*!*/ DoInlineBlocks(List/*!*/ blocks, ref bool inlinedSomething) { - Contract.Requires(cce.NonNullElements(blocks)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List/*!*/ newBlocks = new List(); - - foreach (Block block in blocks) { - TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd); - List cmds = block.Cmds; - List newCmds = new List(); - 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(); - } - 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 newRhss = new List(); - 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 substMap = new Dictionary(); - 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 substMapOld = new Dictionary(); - - 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 RemoveAsserts(List cmds) { - List newCmdSeq = new List(); - 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/*!*/ 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/*!*/ implBlocks = cce.NonNull(impl.OriginalBlocks); - Contract.Assert(implBlocks.Count > 0); - - Procedure proc = impl.Proc; - string startLabel = implBlocks[0].Label; - - List/*!*/ inlinedBlocks = new List(); - - // create in block - List inCmds = new List(); - - // 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 locVars = cce.NonNull(impl.OriginalLocVars); - - // havoc locals and out parameters in case procedure is invoked in a loop - List havocVars = new List(); - 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 { 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 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 outCmds = new List(); - - // 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 { 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 gotoSeq = gotoCmd.labelNames; - List newGotoSeq = new List(); - 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 { 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 substMap) { - Contract.Requires(substMap != null); - Subst = Substituter.SubstitutionFromHashtable(substMap); - } - - public CodeCopier(Dictionary substMap, Dictionary oldSubstMap) { - Contract.Requires(oldSubstMap != null); - Contract.Requires(substMap != null); - Subst = Substituter.SubstitutionFromHashtable(substMap); - OldSubst = Substituter.SubstitutionFromHashtable(oldSubstMap); - } - - public CodeCopier() { - } - - public List CopyCmdSeq(List cmds) { - Contract.Requires(cmds != null); - Contract.Ensures(Contract.Result>() != null); - List newCmds = new List(); - 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() != null); - TransferCmd transferCmd; - GotoCmd gotocmd = cmd as GotoCmd; - if (gotocmd != null) { - Contract.Assert(gotocmd.labelNames != null); - List labels = new List(); - 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() != 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() != 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/*!*/ /* Procedure.Name -> int */ recursiveProcUnrollMap; + + protected Dictionary/*!*/ /* Procedure.Name -> int */ inlinedProcLblMap; + + protected int inlineDepth; + + protected List/*!*/ newLocalVars; + + protected List/*!*/ 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 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() != 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() != null); + return GetInlinedProcLabel(procName) + "$" + formalName; + } + + public Inliner(Program program, InlineCallback cb, int inlineDepth) { + this.program = program; + this.inlinedProcLblMap = new Dictionary(); + this.recursiveProcUnrollMap = new Dictionary(); + this.inlineDepth = inlineDepth; + this.codeCopier = new CodeCopier(); + this.inlineCallback = cb; + this.newLocalVars = new List(); + this.newModifies = new List(); + 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 newBlocks = inliner.DoInlineBlocks(impl.Blocks, ref inlined); + Contract.Assert(cce.NonNullElements(newBlocks)); + + if (!inlined) + return; + + impl.InParams = new List(impl.InParams); + impl.OutParams = new List(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.Out, /*pretty=*/ false), 0); + impl.Emit(new TokenTextWriter("", 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/*!*/ 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 newCmds, List 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/*!*/ 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 { 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/*!*/ DoInlineBlocks(List/*!*/ blocks, ref bool inlinedSomething) { + Contract.Requires(cce.NonNullElements(blocks)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List/*!*/ newBlocks = new List(); + + foreach (Block block in blocks) { + TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd); + List cmds = block.Cmds; + List newCmds = new List(); + 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(); + } + 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 newRhss = new List(); + 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 substMap = new Dictionary(); + 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 substMapOld = new Dictionary(); + + 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 RemoveAsserts(List cmds) { + List newCmdSeq = new List(); + 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/*!*/ 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/*!*/ implBlocks = cce.NonNull(impl.OriginalBlocks); + Contract.Assert(implBlocks.Count > 0); + + Procedure proc = impl.Proc; + string startLabel = implBlocks[0].Label; + + List/*!*/ inlinedBlocks = new List(); + + // create in block + List inCmds = new List(); + + // 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 locVars = cce.NonNull(impl.OriginalLocVars); + + // havoc locals and out parameters in case procedure is invoked in a loop + List havocVars = new List(); + 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 { 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 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 outCmds = new List(); + + // 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 { 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 gotoSeq = gotoCmd.labelNames; + List newGotoSeq = new List(); + 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 { 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 substMap) { + Contract.Requires(substMap != null); + Subst = Substituter.SubstitutionFromHashtable(substMap); + } + + public CodeCopier(Dictionary substMap, Dictionary oldSubstMap) { + Contract.Requires(oldSubstMap != null); + Contract.Requires(substMap != null); + Subst = Substituter.SubstitutionFromHashtable(substMap); + OldSubst = Substituter.SubstitutionFromHashtable(oldSubstMap); + } + + public CodeCopier() { + } + + public List CopyCmdSeq(List cmds) { + Contract.Requires(cmds != null); + Contract.Ensures(Contract.Result>() != null); + List newCmds = new List(); + 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() != null); + TransferCmd transferCmd; + GotoCmd gotocmd = cmd as GotoCmd; + if (gotocmd != null) { + Contract.Assert(gotocmd.labelNames != null); + List labels = new List(); + 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() != 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() != 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 -- cgit v1.2.3