diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Source/Core/Inline.ssc | |
Initial set of files.
Diffstat (limited to 'Source/Core/Inline.ssc')
| -rw-r--r-- | Source/Core/Inline.ssc | 907 |
1 files changed, 907 insertions, 0 deletions
diff --git a/Source/Core/Inline.ssc b/Source/Core/Inline.ssc new file mode 100644 index 00000000..931c35eb --- /dev/null +++ b/Source/Core/Inline.ssc @@ -0,0 +1,907 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie {
+
+ using System;
+ using System.IO;
+ using System.Collections;
+ using System.Collections.Generic;
+ using BoogiePL;
+ using System.Diagnostics;
+ using System.Text.RegularExpressions; // for procedure inlining
+
+ // this callback is called before inlining a procedure
+ public delegate void InlineCallback(Implementation! impl);
+
+ public class Inliner
+ {
+ private InlineCallback inlineCallback;
+ private TypecheckingContext! checkingCtx;
+
+ // Maximum number of unrolling per procedure.
+ // This is now given as a commnd line option.
+ // While typically this number will be given with the :inline attribute in the source code
+ // we set this bound in case the programmer does not provide the number along with the :inline attribute.
+ public static int MaxUnrollPerProcedure = 3;
+
+ protected CodeCopier! codeCopier;
+
+ protected Dictionary<string!,int>! /* Procedure.Name -> int */ recursiveProcUnrollMap;
+
+ protected Dictionary<string!,int>! /* Procedure.Name -> int */ inlinedProcLblMap;
+
+ protected void NextInlinedProcLabel(string! procName) {
+ int currentId;
+ if (inlinedProcLblMap.TryGetValue(procName, out currentId)) {
+ inlinedProcLblMap[procName] = currentId + 1;
+ } else {
+ inlinedProcLblMap.Add(procName, 0);
+ }
+ }
+
+ protected string! GetInlinedProcLabel(string! procName) {
+ int currentId;
+ if (!inlinedProcLblMap.TryGetValue(procName, out currentId)) {
+ currentId = 0;
+ inlinedProcLblMap.Add(procName, currentId);
+ }
+ return "inline$" + procName + "$" + currentId;
+ }
+
+ protected string! GetProcVarName(string! procName, string! formalName) {
+ string! prefix = GetInlinedProcLabel(procName);
+ return prefix + "$" + formalName;
+ }
+
+ protected Inliner(TypecheckingContext! ctx, InlineCallback cb) {
+ inlinedProcLblMap = new Dictionary<string!,int>();
+ recursiveProcUnrollMap = new Dictionary<string!,int>();
+ codeCopier = new CodeCopier();
+ inlineCallback = cb;
+ checkingCtx = ctx;
+ }
+
+ public static void ProcessImplementation(TypecheckingContext! ctx, Program! program, Implementation! impl, InlineCallback cb)
+ requires impl.Proc != null;
+ {
+ Inliner inliner = new Inliner(ctx, cb);
+
+ VariableSeq! newInParams = new VariableSeq(impl.InParams);
+ VariableSeq! newOutParams = new VariableSeq(impl.OutParams);
+ VariableSeq! newLocalVars = new VariableSeq(impl.LocVars);
+
+ IdentifierExprSeq! newModifies = new IdentifierExprSeq(impl.Proc.Modifies);
+
+ bool inlined = false;
+ List<Block!>! newBlocks = inliner.DoInline(impl.Blocks, program, newLocalVars, newModifies, out inlined);
+
+ if (!inlined) return;
+
+ impl.InParams = newInParams;
+ impl.OutParams = newOutParams;
+ impl.LocVars = newLocalVars;
+ impl.Blocks = newBlocks;
+ impl.Proc.Modifies = newModifies;
+
+ impl.ResetImplFormalMap();
+
+ // we need to resolve the new code
+ inliner.ResolveImpl(program, impl);
+
+ if(CommandLineOptions.Clo.PrintInlined) {
+ inliner.EmitImpl(impl);
+ }
+ }
+
+
+ public static void ProcessImplementation(TypecheckingContext! ctx, Program! program, Implementation! impl)
+ requires impl.Proc != null;
+ {
+
+ ProcessImplementation(ctx, program, impl, null);
+ }
+
+ protected void EmitImpl(Implementation! impl)
+ requires impl.Proc != null;
+ {
+ Console.WriteLine("after inlining procedure calls");
+ impl.Proc.Emit(new TokenTextWriter("<console>", Console.Out), 0);
+ impl.Emit(new TokenTextWriter("<console>", Console.Out), 0);
+ }
+
+ private sealed class DummyErrorSink : IErrorSink
+ {
+ public void Error(IToken! tok, string! msg) {
+ // 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(Program! program, Implementation! impl)
+ ensures impl.Proc != null;
+ {
+ ResolutionContext rc = new ResolutionContext(new DummyErrorSink());
+
+ foreach(Declaration 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);
+ }
+
+
+ // returns true if it is ok to further unroll the procedure
+ // otherwise, the procedure is not inlined at the call site
+ protected bool CheckInline(Implementation! impl) {
+ string! procName = impl.Name;
+ int c;
+ if (recursiveProcUnrollMap.TryGetValue(procName, out c)) {
+ if(c > 0) {
+ if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Bounded) {
+ recursiveProcUnrollMap[procName] = c - 1;
+ }
+ return true;
+ }
+ recursiveProcUnrollMap[procName] = 0;
+ return false;
+ }
+
+ bool doinline = false;
+
+ QKeyValue kv = null;
+ // try proc attributes
+ if(impl.Proc != null) {
+ kv = impl.Proc.Attributes;
+ while(kv != null) {
+ if(kv.Key.Equals("inline")) {
+ doinline = true;
+ break;
+ }
+ kv = kv.Next;
+ }
+ }
+ // try impl attributes
+ if(!doinline) {
+ kv = impl.Attributes;
+ while(kv != null) {
+ if(kv.Key.Equals("inline")) {
+ doinline = true;
+ break;
+ }
+ kv = kv.Next;
+ }
+ }
+
+ // try impl attributes
+ if(doinline) {
+ assert(kv != null && kv.Key.Equals("inline"));
+ // check the recursion
+ if (!recursiveProcUnrollMap.TryGetValue(procName, out c)) {
+ c = MaxUnrollPerProcedure;
+ if (kv.Params.Count == 1) {
+ LiteralExpr lit = kv.Params[0] as LiteralExpr;
+ if (lit != null && lit.isBigNum) {
+ c = lit.asBigNum.ToIntSafe;
+ }
+ }
+ recursiveProcUnrollMap.Add(procName, c);
+ }
+
+ if(c > 0) {
+ if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Bounded) {
+ recursiveProcUnrollMap[procName] = c - 1;
+ }
+ return true;
+ }
+ recursiveProcUnrollMap[procName] = 0;
+ return false;
+ }
+
+ // if not inlined, then record its inline count as 0
+ recursiveProcUnrollMap[procName] = 0;
+ return false;
+ }
+
+
+ private List<Block!>! DoInlineBlocks(Stack<Procedure!>! callStack, List<Block!>! blocks, Program! program,
+ VariableSeq! newLocalVars, IdentifierExprSeq! newModifies, ref bool inlinedSomething)
+ {
+ List<Block!>! newBlocks = new List<Block!>();
+
+ foreach(Block block in blocks) {
+
+ TransferCmd! transferCmd = (!) block.TransferCmd;
+
+ CmdSeq cmds = block.Cmds;
+ CmdSeq newCmds = new CmdSeq();
+ Block newBlock;
+ string label = block.Label;
+ int lblCount = 0;
+
+ for(int i = 0; i < cmds.Length; ++i) {
+ Cmd cmd = cmds[i];
+
+ CallCmd callCmd = cmd as CallCmd;
+
+ if(callCmd == null) {
+ // if not call command, leave it as is
+ newCmds.Add(codeCopier.CopyCmd(cmd));
+
+ } else {
+ assert(callCmd.Proc != null);
+ Procedure proc = null;
+ Implementation impl = null;
+ string calleeName = callCmd.Proc.Name;
+
+ bool inline = false;
+
+ // *** now we do not allow constructors to be inlined
+ if(! calleeName.Contains("..ctor")) {
+ // FIXME why on earth are we searching by name?!
+ bool implExists = FindProcImpl(program, calleeName, out proc, out impl);
+ assume(!implExists || (proc != null && impl != null));
+ if(implExists) {
+ if(CheckInline((!)impl)) {
+ inline = true;
+ inlinedSomething = true;
+ }
+ }
+ }
+
+ if (impl != null && CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.MacroLike) {
+ foreach (Procedure! p in callStack) {
+ if (p == impl.Proc) {
+ inline = false;
+ string msg = "";
+ foreach (Procedure! p in callStack) {
+ msg = p.Name + " -> " + msg;
+ }
+ msg += p.Name;
+ checkingCtx.Error(impl, "the inlined procedure is recursive, call stack: {0}", msg);
+ }
+ }
+ }
+
+ assert(!inline || (impl != null));
+
+ if(inline) { // at least one block should exist
+ assume(impl != null && proc != null);
+ assert(((!)impl.OriginalBlocks).Count > 0);
+
+ // do inline now
+ int nextlblCount = lblCount + 1;
+ string nextBlockLabel = 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(proc.Name);
+
+ BeginInline(newLocalVars, newModifies, proc, impl);
+
+ List<Block!>! inlinedBlocks = CreateInlinedBlocks(callCmd, proc, impl, nextBlockLabel);
+
+ EndInline();
+
+ callStack.Push((!)impl.Proc);
+ inlinedBlocks = DoInlineBlocks(callStack, inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);
+ callStack.Pop();
+
+ Block! startBlock = inlinedBlocks[0];
+
+ GotoCmd gotoCmd = new GotoCmd(Token.NoToken, new StringSeq(startBlock.Label));
+ newBlock = new Block(block.tok, ((lblCount == 0) ? (label) : (label + "$" + lblCount)), newCmds, gotoCmd);
+
+ newBlocks.Add(newBlock);
+ newBlocks.AddRange(inlinedBlocks);
+
+ lblCount = nextlblCount;
+ newCmds = new CmdSeq();
+
+ } else {
+ // if this call will not be inlined, so leave it as is
+ newCmds.Add(codeCopier.CopyCmd(callCmd));
+ }
+ }
+ }
+
+ newBlock = new Block(block.tok, ((lblCount == 0) ? (label) : (label + "$" + lblCount)), newCmds, codeCopier.CopyTransferCmd(transferCmd));
+ newBlocks.Add(newBlock);
+ }
+
+ return newBlocks;
+ }
+
+ protected List<Block!>! DoInline(List<Block!>! blocks, Program! program, VariableSeq! newLocalVars, IdentifierExprSeq! newModifies, out bool inlined)
+ {
+ inlinedProcLblMap.Clear();
+ recursiveProcUnrollMap.Clear();
+
+ inlined = false;
+ return DoInlineBlocks(new Stack<Procedure!>(), blocks, program, newLocalVars, newModifies, ref inlined);
+ }
+
+ protected void BeginInline(VariableSeq! newLocalVars, IdentifierExprSeq! newModifies, Procedure! proc, Implementation! impl) {
+ Hashtable substMap = new Hashtable();
+
+ foreach(Variable! locVar in (!)impl.OriginalLocVars) {
+ LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, locVar.Name), locVar.TypedIdent.Type, locVar.TypedIdent.WhereExpr));
+ newLocalVars.Add(localVar);
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, localVar);
+ substMap.Add(locVar, ie);
+ }
+
+ for (int i = 0; i < impl.InParams.Length; i++) {
+ Variable inVar = (!) 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);
+ 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 = (!)proc.InParams[i];
+ if (procInVar != inVar) {
+ substMap.Add(procInVar, ie);
+ }
+ }
+
+ for (int i = 0; i < impl.OutParams.Length; i++) {
+ Variable outVar = (!) impl.OutParams[i];
+ LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, outVar.Name), outVar.TypedIdent.Type, outVar.TypedIdent.WhereExpr));
+ 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 = (!)proc.OutParams[i];
+ if (procOutVar != outVar) {
+ substMap.Add(procOutVar, ie);
+ }
+ }
+
+ Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/();
+
+ foreach (IdentifierExpr! mie in proc.Modifies) {
+ Variable! mVar = (!) 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.Has(mie)) {
+ newModifies.Add(mie);
+ }
+ }
+
+ codeCopier.Subst = Substituter.SubstitutionFromHashtable(substMap);
+ codeCopier.SubstForOld = Substituter.SubstitutionFromHashtable(substMapOld);
+ }
+
+ protected void EndInline() {
+ codeCopier.Subst = null;
+ codeCopier.SubstForOld = null;
+ }
+
+
+ // result[0] is the entry block
+ protected List<Block!>! CreateInlinedBlocks(CallCmd! callCmd, Procedure! proc, Implementation! impl, string! nextBlockLabel)
+ requires (codeCopier.Subst != null);
+ requires (codeCopier.SubstForOld != null);
+ {
+
+ List<Block!>! implBlocks = (!)impl.OriginalBlocks;
+ assert (implBlocks.Count > 0);
+
+ string startLabel = implBlocks[0].Label;
+
+ List<Block!>! inlinedBlocks = new List<Block!>();
+
+ // create in block
+ CmdSeq inCmds = new CmdSeq();
+
+ // assign in parameters
+ for(int i = 0; i < impl.InParams.Length; ++i) {
+ Cmd cmd = Cmd.SimpleAssign(impl.tok,
+ (IdentifierExpr) (!) codeCopier.Subst( (!)impl.InParams[i]),
+ (!)callCmd.Ins[i]);
+ inCmds.Add(cmd);
+ }
+
+ // inject non-free requires
+ for (int i = 0; i < proc.Requires.Length; i++) {
+ Requires! req = (!) proc.Requires[i];
+ if (!req.Free) {
+ Requires! reqCopy = (Requires!) req.Clone();
+ reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
+ AssertCmd! a = new AssertRequiresCmd(callCmd, reqCopy);
+ a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
+ inCmds.Add(a);
+ }
+ }
+
+ VariableSeq locVars = (!)impl.OriginalLocVars;
+
+ // add where clauses of local vars as assume
+ for(int i = 0; i < locVars.Length; ++i) {
+ Expr whereExpr = ((!)locVars[i]).TypedIdent.WhereExpr;
+ if(whereExpr != null) {
+ whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);
+ // FIXME we cannot overwrite it, can we?!
+ ((!)locVars[i]).TypedIdent.WhereExpr = whereExpr;
+ AssumeCmd! a = new AssumeCmd(Token.NoToken, whereExpr);
+ inCmds.Add(a);
+ }
+ }
+
+ // add where clauses of output params as assume
+ for(int i = 0; i < impl.OutParams.Length; ++i) {
+ Expr whereExpr = ((!)impl.OutParams[i]).TypedIdent.WhereExpr;
+ if(whereExpr != null) {
+ whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);
+ // FIXME likewise
+ ((!)impl.OutParams[i]).TypedIdent.WhereExpr = whereExpr;
+ AssumeCmd! a = new AssumeCmd(Token.NoToken, whereExpr);
+ inCmds.Add(a);
+ }
+ }
+
+ // assign modifies old values
+ foreach (IdentifierExpr! mie in proc.Modifies)
+ {
+ Variable! mvar = (!) mie.Decl;
+ AssignCmd assign = Cmd.SimpleAssign(impl.tok, (IdentifierExpr) (!) codeCopier.SubstForOld(mvar), mie);
+ inCmds.Add(assign);
+ }
+
+ GotoCmd inGotoCmd = new GotoCmd(callCmd.tok, new StringSeq(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) {
+ CmdSeq copyCmds = codeCopier.CopyCmdSeq(block.Cmds);
+ TransferCmd transferCmd = CreateInlinedTransferCmd((!) block.TransferCmd, GetInlinedProcLabel(proc.Name));
+ intBlock = new Block(block.tok, GetInlinedProcLabel(proc.Name) + "$" + block.Label, copyCmds, transferCmd);
+ inlinedBlocks.Add(intBlock);
+ }
+
+ // create out block
+ CmdSeq outCmds = new CmdSeq();
+
+ // inject non-free ensures
+ for (int i = 0; i < proc.Ensures.Length; i++) {
+ Ensures! ens = (!) proc.Ensures[i];
+ if (!ens.Free) {
+ Ensures! ensCopy = (Ensures!) ens.Clone();
+ ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
+ AssertCmd! a = new AssertEnsuresCmd(ensCopy);
+ outCmds.Add(a);
+ }
+ }
+
+ // assign out params
+ for(int i = 0; i < impl.OutParams.Length; ++i) {
+ Expr! cout_exp = (IdentifierExpr) (!) codeCopier.Subst((!)impl.OutParams[i]);
+ Cmd cmd = Cmd.SimpleAssign(impl.tok, (!)callCmd.Outs[i], cout_exp);
+ outCmds.Add(cmd);
+ }
+
+ // create out block
+ GotoCmd outGotoCmd = new GotoCmd(Token.NoToken, new StringSeq(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) {
+ TransferCmd newTransferCmd;
+
+ GotoCmd gotoCmd = transferCmd as GotoCmd;
+ if(gotoCmd != null) {
+ StringSeq gotoSeq = gotoCmd.labelNames;
+ StringSeq newGotoSeq = new StringSeq();
+ foreach(string! blockLabel in (!) gotoSeq) {
+ newGotoSeq.Add(procLabel + "$" + blockLabel);
+ }
+ newTransferCmd = new GotoCmd(transferCmd.tok, newGotoSeq);
+ } else {
+ newTransferCmd = new GotoCmd(transferCmd.tok, new StringSeq(procLabel + "$Return"));
+ }
+
+ return newTransferCmd;
+ }
+
+ protected static bool FindProcImpl(Program! program, string! procName, out Procedure outProc, out Implementation outImpl)
+ {
+ // this assumes that there is at most one procedure and only one associated implementation in the current context
+
+ foreach(Declaration decl in program.TopLevelDeclarations) {
+ Implementation impl = decl as Implementation;
+ if(impl != null) {
+ if(impl.Name.Equals(procName)) {
+ assert(impl.Proc != null);
+ outProc = impl.Proc;
+ outImpl = impl;
+ return true;
+ }
+ }
+ }
+
+ foreach(Declaration decl in program.TopLevelDeclarations) {
+ Procedure proc = decl as Procedure;
+ if(proc != null) {
+ if(proc.Name.Equals(procName)) {
+ outProc = proc;
+ outImpl = null;
+ return false;
+ }
+ }
+ }
+
+ outProc = null;
+ outImpl = null;
+ return false;
+ }
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////////////////////////////////
+
+ public class CodeCopier
+ {
+
+ private DefaultDuplicator! dupl;
+
+ private sealed class DefaultDuplicator : Duplicator
+ {
+ public Substitution subst;
+ public Substitution oldSubst;
+ private bool insideOldExpr = false;
+ public DefaultDuplicator(Substitution subst, Substitution oldSubst) {
+ this.subst = subst;
+ this.oldSubst = oldSubst;
+ base();
+ }
+ public override Cmd! VisitAssumeCmd(AssumeCmd! node)
+ {
+ return new AssumeCmd(node.tok, VisitExpr(node.Expr));
+ }
+ public override Cmd! VisitAssertCmd(AssertCmd! node)
+ {
+ return new AssertCmd(node.tok, VisitExpr(node.Expr));
+ }
+ public override Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)
+ {
+ return new AssertRequiresCmd((CallCmd)VisitCallCmd(node.Call), VisitRequires(node.Requires));
+ }
+ public override Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)
+ {
+ return new AssertEnsuresCmd(VisitEnsures(node.Ensures));
+ }
+
+ public override Cmd! VisitCallCmd(CallCmd! node)
+ {
+ List<Expr>! newIns = new List<Expr> ();
+ List<IdentifierExpr>! newOuts = new List<IdentifierExpr> ();
+ foreach (Expr e in node.Ins)
+ newIns.Add(e == null ? null : this.VisitExpr(e));
+ foreach (IdentifierExpr e in node.Outs)
+ newOuts.Add(e == null ? null : (IdentifierExpr)this.VisitIdentifierExpr(e));
+
+ CallCmd! newCmd = new CallCmd(node.tok, ((!)node.Proc).Name, newIns, newOuts);
+ newCmd.Proc = node.Proc;
+ return newCmd;
+ }
+ public override Expr! VisitIdentifierExpr(IdentifierExpr! node)
+ {
+ Expr e = null;
+ if(insideOldExpr && oldSubst != null) {
+ e = oldSubst((!)node.Decl);
+ }
+ if(e == null) {
+ if(subst != null) {
+ e = subst((!)node.Decl);
+ return e == null ? base.VisitIdentifierExpr(node) : e;
+ } else {
+ return base.VisitIdentifierExpr(node);
+ }
+ }
+ return e;
+ }
+ public override Expr! VisitOldExpr(OldExpr! node)
+ {
+ if(this.oldSubst != null) {
+ bool previouslyInOld = insideOldExpr;
+ insideOldExpr = true;
+ Expr! e = (Expr!)this.Visit(node.Expr);
+ insideOldExpr = previouslyInOld;
+ return e;
+ } else {
+ return base.VisitOldExpr(node);
+ }
+ }
+ }
+
+ public CodeCopier(Hashtable! substMap) {
+ this.dupl = new DefaultDuplicator(Substituter.SubstitutionFromHashtable(substMap), null);
+ }
+
+ public CodeCopier(Hashtable! substMap, Hashtable! oldSubstMap) {
+ this.dupl = new DefaultDuplicator(Substituter.SubstitutionFromHashtable(substMap), Substituter.SubstitutionFromHashtable(oldSubstMap));
+ }
+
+ public CodeCopier() {
+ this.dupl = new DefaultDuplicator(null, null);
+ }
+
+ public Substitution Subst {
+ set {
+ this.dupl.subst = value;
+ }
+ get {
+ return this.dupl.subst;
+ }
+ }
+
+ public Substitution SubstForOld {
+ set {
+ this.dupl.oldSubst = value;
+ }
+ get {
+ return this.dupl.oldSubst;
+ }
+ }
+
+ public Duplicator! Dupl {
+ get {
+ return this.dupl;
+ }
+ }
+
+ public List<Block!>! CopyBlocks(List<Block!>! blocks) {
+
+ List<Block!>! newBlocks = new List<Block!>();
+
+ foreach(Block block in blocks) {
+ Block newBlock = CopyBlock(block);
+ newBlocks.Add(newBlock);
+ }
+
+ return newBlocks;
+ }
+
+ public List<Block!>! CopyBlocks(List<Block!>! blocks, string! prefix) {
+
+ List<Block!>! newBlocks = new List<Block!>();
+
+ foreach(Block block in blocks) {
+ Block newBlock = CopyBlock(block, prefix);
+ newBlocks.Add(newBlock);
+ }
+
+ return newBlocks;
+ }
+
+
+ #region CopyBlock
+ public Block! CopyBlock(Block! block) {
+
+ assert(block.TransferCmd != null);
+ Block newBlock = new Block(block.tok, block.Label, CopyCmdSeq(block.Cmds), CopyTransferCmd(block.TransferCmd));
+
+ return newBlock;
+
+ }
+
+ public Block! CopyBlock(Block! block, string! prefix) {
+
+ assert(block.TransferCmd != null);
+ Block newBlock = new Block(block.tok, prefix + "$" + block.Label, CopyCmdSeq(block.Cmds), CopyTransferCmd(block.TransferCmd));
+
+ return newBlock;
+
+ }
+ #endregion
+
+ #region CopyCmdSeq
+ public CmdSeq! CopyCmdSeq(CmdSeq! cmds) {
+
+ CmdSeq newCmds = new CmdSeq();
+
+ for (int i = 0; i < cmds.Length; ++i) {
+ newCmds.Add(CopyCmd(cmds[i]));
+ }
+
+ return newCmds;
+
+ }
+ #endregion
+
+
+ #region CopyTransferCmd
+ public TransferCmd! CopyTransferCmd(TransferCmd! cmd) {
+ TransferCmd transferCmd;
+ GotoCmd gotocmd = cmd as GotoCmd;
+ if(gotocmd != null) {
+ assert(gotocmd.labelNames != null);
+ StringSeq labels = new StringSeq();
+ labels.AddRange(gotocmd.labelNames);
+ transferCmd = new GotoCmd(cmd.tok, labels);
+ } else {
+ transferCmd = new ReturnCmd(cmd.tok);
+ }
+ return transferCmd;
+ }
+
+ public TransferCmd! CopyTransferCmd(TransferCmd! cmd, string! prefix) {
+ TransferCmd transferCmd;
+ GotoCmd gotocmd = cmd as GotoCmd;
+ if(gotocmd != null) {
+ assert(gotocmd.labelNames != null);
+ StringSeq labels = new StringSeq();
+ foreach(string label in gotocmd.labelNames) {
+ labels.Add(prefix + "$" + label);
+ }
+ transferCmd = new GotoCmd(cmd.tok, labels);
+ } else {
+ transferCmd = new ReturnCmd(cmd.tok);
+ }
+ return transferCmd;
+ }
+ #endregion
+
+
+
+ #region CopyCmd
+ public Cmd! CopyCmd(Cmd! cmd) {
+ Cmd newCmd = (Cmd) Dupl.Visit(cmd);
+ return newCmd;
+ }
+ #endregion
+
+ #region CopyExpr
+ public Expr! CopyExpr(Expr! expr) {
+ Expr newExpr = (Expr) Dupl.Visit(expr);
+ return newExpr;
+ }
+ #endregion
+
+ } // end class CodeCopier
+
+
+ public class AxiomExpander : Duplicator
+ {
+ readonly Program! program;
+ readonly TypecheckingContext! tc;
+
+ public AxiomExpander(Program! prog, TypecheckingContext! t)
+ {
+ program = prog;
+ tc = t;
+ }
+
+ public void CollectExpansions()
+ {
+ foreach (Declaration! decl in program.TopLevelDeclarations) {
+ Axiom ax = decl as Axiom;
+ if (ax != null) {
+ bool expand = false;
+ if (!ax.CheckBooleanAttribute("inline", ref expand)) {
+ Error(decl.tok, "{:inline ...} expects either true or false as the argument");
+ }
+ if (expand) {
+ AddExpansion(ax.Expr, ax.FindStringAttribute("ignore"));
+ }
+ }
+ Function f = decl as Function;
+ if (f != null && f.Body != null) {
+ Variable[]! formals = new Variable [f.InParams.Length];
+ for (int i = 0; i < formals.Length; ++i)
+ formals[i] = f.InParams[i];
+ AddExpansion(f, new Expansion(null, f.Body,
+ new TypeVariableSeq (f.TypeParameters),
+ formals));
+ }
+ }
+ }
+
+ void Error(IToken! tok, string msg)
+ {
+ tc.Error(tok, "expansion: " + msg);
+ }
+
+ void AddExpansion(Expr! axiomBody, string? ignore)
+ {
+ // it would be sooooooooo much easier with pattern matching
+ ForallExpr all = axiomBody as ForallExpr;
+ if (all != null) {
+ NAryExpr nary = all.Body as NAryExpr;
+ BinaryOperator bin = nary == null ? null : nary.Fun as BinaryOperator;
+ //System.Console.WriteLine("{0} {1} {2}", nary==null, bin==null, bin==null?0 : bin.Op);
+ if (nary != null && bin != null && (bin.Op == BinaryOperator.Opcode.Eq || bin.Op == BinaryOperator.Opcode.Iff)) {
+ NAryExpr? func = nary.Args[0] as NAryExpr;
+ //System.Console.WriteLine("{0} {1}", func == null, func == null ? null : func.Fun.GetType());
+ while (func != null && func.Fun is TypeCoercion)
+ func = func.Args[0] as NAryExpr;
+ if (func != null && func.Fun is FunctionCall) {
+ Function fn = (!)((FunctionCall)func.Fun).Func;
+ Expansion exp = new Expansion(ignore, (!)nary.Args[1],
+ new TypeVariableSeq (),
+ new Variable[func.Args.Length]);
+ int pos = 0;
+ Dictionary<Declaration, bool> parms = new Dictionary<Declaration, bool>();
+ foreach (Expr! e in func.Args) {
+ IdentifierExpr id = e as IdentifierExpr;
+ if (id == null) {
+ Error(e.tok, "only identifiers supported as function arguments");
+ return;
+ }
+ exp.formals[pos++] = id.Decl;
+ if (parms.ContainsKey(id.Decl)) {
+ Error(all.tok, "an identifier was used more than once");
+ return;
+ }
+ parms[id.Decl] = true;
+ if (!all.Dummies.Has(id.Decl)) {
+ Error(all.tok, "identifier was not quantified over");
+ return;
+ }
+ }
+ if (func.Args.Length != all.Dummies.Length) {
+ Error(all.tok, "more variables quantified over, than used in function");
+ return;
+ }
+
+ Dictionary<TypeVariable!, bool> typeVars = new Dictionary<TypeVariable!, bool>();
+ foreach (TypeVariable! v in ((!)func.TypeParameters).FormalTypeParams) {
+ if (!func.TypeParameters[v].IsVariable) {
+ Error(all.tok, "only identifiers supported as type parameters");
+ return;
+ }
+ TypeVariable! formal = func.TypeParameters[v].AsVariable;
+ exp.TypeParameters.Add(formal);
+ if (typeVars.ContainsKey(formal)) {
+ Error(all.tok, "an identifier was used more than once");
+ return;
+ }
+ typeVars[formal] = true;
+ if (!all.TypeParameters.Has(formal)) {
+ Error(all.tok, "identifier was not quantified over");
+ return;
+ }
+ }
+ if (((FunctionCall)func.Fun).Func.TypeParameters.Length != all.TypeParameters.Length) {
+ Error(all.tok, "more variables quantified over, than used in function");
+ return;
+ }
+ AddExpansion(fn, exp);
+ return;
+ }
+ }
+ }
+
+ Error(axiomBody.tok, "axiom to be expanded must have form (forall VARS :: f(VARS) == expr(VARS))");
+ }
+
+ void AddExpansion(Function! fn, Expansion! x) {
+ if (fn.expansions == null) {
+ fn.expansions = new List<Expansion!>();
+ }
+ fn.expansions.Add(x);
+ }
+ }
+} // end namespace
+
|