diff options
Diffstat (limited to 'Source/Core/Inline.cs')
| -rw-r--r-- | Source/Core/Inline.cs | 595 |
1 files changed, 339 insertions, 256 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 0db27d6d..7ae3a098 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -4,29 +4,38 @@ //
//-----------------------------------------------------------------------------
namespace Microsoft.Boogie {
-
+
using System;
using System.IO;
using System.Collections;
using System.Collections.Generic;
- using BoogiePL;
+ using System.Diagnostics.Contracts;
+ using BoogiePL=Microsoft.Boogie;
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 delegate void InlineCallback(Implementation/*!*/ impl);
- public class Inliner
- {
+ public class Inliner {
private InlineCallback inlineCallback;
-
- protected CodeCopier! codeCopier;
-
- protected Dictionary<string!,int>! /* Procedure.Name -> int */ recursiveProcUnrollMap;
-
- protected Dictionary<string!,int>! /* Procedure.Name -> int */ inlinedProcLblMap;
-
- protected void NextInlinedProcLabel(string! procName) {
+
+ protected CodeCopier/*!*/ codeCopier;
+
+ protected Dictionary<string/*!*/, int>/*!*/ /* Procedure.Name -> int */ recursiveProcUnrollMap;
+
+ protected Dictionary<string/*!*/, int>/*!*/ /* Procedure.Name -> int */ inlinedProcLblMap;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(codeCopier != null);
+ Contract.Invariant(cce.NonNullElements(recursiveProcUnrollMap));
+ Contract.Invariant(cce.NonNullElements(inlinedProcLblMap));
+ }
+
+
+ protected void NextInlinedProcLabel(string procName) {
+ Contract.Requires(procName != null);
int currentId;
if (inlinedProcLblMap.TryGetValue(procName, out currentId)) {
inlinedProcLblMap[procName] = currentId + 1;
@@ -34,8 +43,10 @@ namespace Microsoft.Boogie { inlinedProcLblMap.Add(procName, 0);
}
}
-
- protected string! GetInlinedProcLabel(string! procName) {
+
+ protected string GetInlinedProcLabel(string procName) {
+ Contract.Requires(procName != null);
+ Contract.Ensures(Contract.Result<string>() != null);
int currentId;
if (!inlinedProcLblMap.TryGetValue(procName, out currentId)) {
currentId = 0;
@@ -43,69 +54,81 @@ namespace Microsoft.Boogie { }
return "inline$" + procName + "$" + currentId;
}
-
- protected string! GetProcVarName(string! procName, string! formalName) {
- string! prefix = GetInlinedProcLabel(procName);
+
+ protected string GetProcVarName(string procName, string formalName) {
+ Contract.Requires(formalName != null);
+ Contract.Requires(procName != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ string/*!*/ prefix = GetInlinedProcLabel(procName);
+ Contract.Assert(prefix != null);
return prefix + "$" + formalName;
- }
-
- protected Inliner(InlineCallback cb) {
- inlinedProcLblMap = new Dictionary<string!,int>();
- recursiveProcUnrollMap = new Dictionary<string!,int>();
+ }
+
+ protected Inliner(InlineCallback cb) {
+ inlinedProcLblMap = new Dictionary<string/*!*/, int>();
+ recursiveProcUnrollMap = new Dictionary<string/*!*/, int>();
codeCopier = new CodeCopier();
inlineCallback = cb;
}
-
- public static void ProcessImplementation(Program! program, Implementation! impl, InlineCallback cb)
- requires impl.Proc != null;
- {
+
+ public static void ProcessImplementation(Program program, Implementation impl, InlineCallback cb) {
+ Contract.Requires(impl != null);
+ Contract.Requires(program != null);
+ Contract.Requires(impl.Proc != null);
Inliner inliner = new Inliner(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);
-
+
+ VariableSeq/*!*/ newInParams = new VariableSeq(impl.InParams);
+ Contract.Assert(newInParams != null);
+ VariableSeq/*!*/ newOutParams = new VariableSeq(impl.OutParams);
+ Contract.Assert(newOutParams != null);
+ VariableSeq/*!*/ newLocalVars = new VariableSeq(impl.LocVars);
+ Contract.Assert(newLocalVars != null);
+ IdentifierExprSeq/*!*/ newModifies = new IdentifierExprSeq(impl.Proc.Modifies);
+ Contract.Assert(newModifies != null);
+
bool inlined = false;
- List<Block!>! newBlocks = inliner.DoInline(impl.Blocks, program, newLocalVars, newModifies, out inlined);
+ List<Block/*!*/>/*!*/ newBlocks = inliner.DoInline(impl.Blocks, program, newLocalVars, newModifies, out inlined);
+ Contract.Assert(cce.NonNullElements(newBlocks));
+
+ if (!inlined)
+ return;
- 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) {
+
+ if (CommandLineOptions.Clo.PrintInlined) {
inliner.EmitImpl(impl);
}
}
-
-
- public static void ProcessImplementation(Program! program, Implementation! impl)
- requires impl.Proc != null;
- {
+
+
+ public static void ProcessImplementation(Program program, Implementation impl) {
+ Contract.Requires(impl != null);
+ Contract.Requires(program != null);
+ Contract.Requires(impl.Proc != null);
ProcessImplementation(program, impl, null);
}
-
- protected void EmitImpl(Implementation! impl)
- requires impl.Proc != null;
- {
+
+ 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), 0);
impl.Emit(new TokenTextWriter("<console>", Console.Out), 0);
}
-
- private sealed class DummyErrorSink : IErrorSink
- {
- public void Error(IToken! tok, string! msg) {
+
+ 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
@@ -113,28 +136,31 @@ namespace Microsoft.Boogie { }
}
- protected void ResolveImpl(Program! program, Implementation! impl)
- ensures impl.Proc != null;
- {
+ protected void ResolveImpl(Program program, Implementation impl) {
+ Contract.Requires(impl != null);
+ Contract.Requires(program != null);
+ Contract.Ensures(impl.Proc != null);
ResolutionContext rc = new ResolutionContext(new DummyErrorSink());
-
- foreach(Declaration decl in program.TopLevelDeclarations) {
+
+ 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 int GetInlineCount(Implementation! impl) {
- string! procName = impl.Name;
+ protected int GetInlineCount(Implementation impl) {
+ Contract.Requires(impl != null);
+ string/*!*/ procName = impl.Name;
+ Contract.Assert(procName != null);
int c;
if (recursiveProcUnrollMap.TryGetValue(procName, out c)) {
return c;
@@ -146,103 +172,115 @@ namespace Microsoft.Boogie { if (impl.Proc != null) {
impl.Proc.CheckIntAttribute("inline", ref c);
}
-
+
recursiveProcUnrollMap[procName] = c;
return c;
}
-
- void CheckRecursion(Implementation! impl, Stack<Procedure!>! callStack) {
- foreach (Procedure! p in callStack) {
+
+ 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! p in callStack) {
- msg = p.Name + " -> " + 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 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; + private List<Block/*!*/>/*!*/ DoInlineBlocks(Stack<Procedure/*!*/>/*!*/ callStack, List<Block/*!*/>/*!*/ blocks, Program/*!*/ program,
+ VariableSeq/*!*/ newLocalVars, IdentifierExprSeq/*!*/ newModifies, ref bool inlinedSomething) {
+ Contract.Requires(cce.NonNullElements(callStack));
+ Contract.Requires(cce.NonNullElements(blocks));
+ Contract.Requires(program != null);
+ Contract.Requires(newLocalVars != null);
+ Contract.Requires(newModifies != null);
+ 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);
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]; +
+ for (int i = 0; i < cmds.Length; ++i) {
+ Cmd cmd = cmds[i];
CallCmd callCmd = cmd as CallCmd;
-
- if(callCmd == null) {
+
+ if (callCmd == null) {
// if not call command, leave it as is
- newCmds.Add(codeCopier.CopyCmd(cmd)); + newCmds.Add(codeCopier.CopyCmd(cmd));
} else {
- assert(callCmd.Proc != null);
+ Contract.Assert(callCmd.Proc != null);
Procedure proc = null;
Implementation impl = null;
string calleeName = callCmd.Proc.Name;
-
+
int inline = -1;
// *** 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));
+ Contract.Assume(!implExists || (proc != null && impl != null));
if (implExists) {
- inline = GetInlineCount((!)impl);
+ inline = GetInlineCount(cce.NonNull(impl));
}
- }
+ }
+
+ Contract.Assert(inline == -1 || impl != null);
- assert(inline == -1 || impl != null);
-
if (inline > 0) { // at least one block should exist
- assume(impl != null && proc != null);
- assert(((!)impl.OriginalBlocks).Count > 0);
+ Contract.Assume(impl != null && proc != null);
+ Contract.Assert(cce.NonNull(impl.OriginalBlocks).Count > 0);
inlinedSomething = true;
-
+
// do inline now
int nextlblCount = lblCount + 1;
string nextBlockLabel = label + "$" + nextlblCount;
-
+
// run the callback before each inline
- if(inlineCallback != null) {
+ 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);
-
+
+ List<Block/*!*/>/*!*/ inlinedBlocks = CreateInlinedBlocks(callCmd, proc, impl, nextBlockLabel);
+ Contract.Assert(cce.NonNullElements(inlinedBlocks));
+
EndInline();
- recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;
- callStack.Push((!)impl.Proc);
+ recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] - 1;
+ callStack.Push(cce.NonNull(impl.Proc));
inlinedBlocks = DoInlineBlocks(callStack, inlinedBlocks, program, newLocalVars, newModifies, ref inlinedSomething);
callStack.Pop();
recursiveProcUnrollMap[impl.Name] = recursiveProcUnrollMap[impl.Name] + 1;
-
- Block! startBlock = inlinedBlocks[0];
+
+ Block/*!*/ startBlock = inlinedBlocks[0];
+ Contract.Assert(startBlock != null);
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(); + newCmds = new CmdSeq();
} else if (inline == 0) {
inlinedSomething = true;
if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {
@@ -256,11 +294,11 @@ namespace Microsoft.Boogie { newCmds.Add(codeCopier.CopyCmd(callCmd));
}
} else {
- newCmds.Add(codeCopier.CopyCmd(callCmd));
- }
+ newCmds.Add(codeCopier.CopyCmd(callCmd));
+ }
}
}
-
+
newBlock = new Block(block.tok, ((lblCount == 0) ? (label) : (label + "$" + lblCount)), newCmds, codeCopier.CopyTransferCmd(transferCmd));
newBlocks.Add(newBlock);
}
@@ -268,271 +306,300 @@ namespace Microsoft.Boogie { return newBlocks;
}
- protected List<Block!>! DoInline(List<Block!>! blocks, Program! program, VariableSeq! newLocalVars, IdentifierExprSeq! newModifies, out bool inlined)
- {
+ protected List<Block/*!*/>/*!*/ DoInline(List<Block/*!*/>/*!*/ blocks, Program program, VariableSeq newLocalVars, IdentifierExprSeq newModifies, out bool inlined) {
+ Contract.Requires(newModifies != null);
+ Contract.Requires(newLocalVars != null);
+ Contract.Requires(program != null);
+ Contract.Requires(cce.NonNullElements(blocks));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
inlinedProcLblMap.Clear();
recursiveProcUnrollMap.Clear();
-
+
inlined = false;
- return DoInlineBlocks(new Stack<Procedure!>(), blocks, program, newLocalVars, newModifies, ref inlined);
+ return DoInlineBlocks(new Stack<Procedure/*!*/>(), blocks, program, newLocalVars, newModifies, ref inlined);
}
-
- protected void BeginInline(VariableSeq! newLocalVars, IdentifierExprSeq! newModifies, Procedure! proc, Implementation! impl) {
+
+ protected void BeginInline(VariableSeq newLocalVars, IdentifierExprSeq newModifies, Procedure proc, Implementation impl) {
+ Contract.Requires(impl != null);
+ Contract.Requires(proc != null);
+ Contract.Requires(newModifies != null);
+ Contract.Requires(newLocalVars != null);
Hashtable substMap = new Hashtable();
-
- foreach(Variable! locVar in (!)impl.OriginalLocVars) {
+
+ 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));
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];
+ 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);
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];
+ Variable procInVar = cce.NonNull(proc.InParams[i]);
if (procInVar != inVar) {
substMap.Add(procInVar, ie);
}
}
-
+
for (int i = 0; i < impl.OutParams.Length; i++) {
- Variable outVar = (!) impl.OutParams[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));
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];
+ Variable procOutVar = cce.NonNull(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;
+
+ 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.Has(mie)) {
+ if (!newModifies.Has(mie)) {
newModifies.Add(mie);
}
}
-
- codeCopier.Subst = Substituter.SubstitutionFromHashtable(substMap); - codeCopier.OldSubst = Substituter.SubstitutionFromHashtable(substMapOld); +
+ codeCopier.Subst = Substituter.SubstitutionFromHashtable(substMap);
+ codeCopier.OldSubst = Substituter.SubstitutionFromHashtable(substMapOld);
}
-
+
protected void EndInline() {
codeCopier.Subst = null;
codeCopier.OldSubst = 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.OldSubst != null);
- {
-
- List<Block!>! implBlocks = (!)impl.OriginalBlocks;
- assert (implBlocks.Count > 0);
-
+ protected List<Block/*!*/>/*!*/ CreateInlinedBlocks(CallCmd callCmd, Procedure proc, Implementation impl, string nextBlockLabel) {
+ Contract.Requires(nextBlockLabel != null);
+ Contract.Requires(impl != null);
+ Contract.Requires(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);
+
string startLabel = implBlocks[0].Label;
-
- List<Block!>! inlinedBlocks = new List<Block!>();
-
+
+ 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) {
+ for (int i = 0; i < impl.InParams.Length; ++i) {
Cmd cmd = Cmd.SimpleAssign(impl.tok,
- (IdentifierExpr) (!) codeCopier.Subst( (!)impl.InParams[i]),
- (!)callCmd.Ins[i]);
+ (IdentifierExpr)cce.NonNull(codeCopier.Subst)(cce.NonNull(impl.InParams[i])),
+ cce.NonNull(callCmd.Ins[i]));
inCmds.Add(cmd);
}
-
+
// inject non-free requires
for (int i = 0; i < proc.Requires.Length; i++) {
- Requires! req = (!) proc.Requires[i];
+ Requires/*!*/ req = cce.NonNull(proc.Requires[i]);
if (!req.Free) {
- Requires! reqCopy = (Requires!) req.Clone();
+ Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone());
reqCopy.Condition = codeCopier.CopyExpr(req.Condition);
- AssertCmd! a = new AssertRequiresCmd(callCmd, reqCopy);
+ AssertCmd/*!*/ a = new AssertRequiresCmd(callCmd, reqCopy);
+ Contract.Assert(a != null);
a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced;
inCmds.Add(a);
}
}
- VariableSeq locVars = (!)impl.OriginalLocVars; -
+ VariableSeq locVars = cce.NonNull(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) {
+ for (int i = 0; i < locVars.Length; ++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?!
- ((!)locVars[i]).TypedIdent.WhereExpr = whereExpr;
- AssumeCmd! a = new AssumeCmd(Token.NoToken, whereExpr);
+ (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.Length; ++i) {
- Expr whereExpr = ((!)impl.OutParams[i]).TypedIdent.WhereExpr;
- if(whereExpr != null) {
+ for (int i = 0; i < impl.OutParams.Length; ++i) {
+ Expr whereExpr = (cce.NonNull(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);
+ (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)
- {
- Variable! mvar = (!) mie.Decl;
- AssignCmd assign = Cmd.SimpleAssign(impl.tok, (IdentifierExpr) (!) codeCopier.OldSubst(mvar), mie);
+ 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 StringSeq(GetInlinedProcLabel(proc.Name) + "$" + startLabel));
Block inBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Entry", inCmds, inGotoCmd);
- inlinedBlocks.Add(inBlock); -
+ 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));
+ CmdSeq copyCmds = codeCopier.CopyCmdSeq(block.Cmds);
+ 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); + 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];
+ Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]);
if (!ens.Free) {
- Ensures! ensCopy = (Ensures!) ens.Clone();
+ Ensures/*!*/ ensCopy = (Ensures/*!*/)cce.NonNull(ens.Clone());
ensCopy.Condition = codeCopier.CopyExpr(ens.Condition);
- AssertCmd! a = new AssertEnsuresCmd(ensCopy);
+ AssertCmd/*!*/ a = new AssertEnsuresCmd(ensCopy);
+ Contract.Assert(a != null);
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);
+ for (int i = 0; i < impl.OutParams.Length; ++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 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) {
+
+ 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) {
+ if (gotoCmd != null) {
StringSeq gotoSeq = gotoCmd.labelNames;
StringSeq newGotoSeq = new StringSeq();
- foreach(string! blockLabel in (!) gotoSeq) {
+ 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 StringSeq(procLabel + "$Return"));
}
-
+
return newTransferCmd;
}
-
- protected static bool FindProcImpl(Program! program, string! procName, out Procedure outProc, out Implementation outImpl)
- {
+
+ protected static bool FindProcImpl(Program program, string procName, out Procedure outProc, out Implementation outImpl) {
+ Contract.Requires(procName != null);
+ Contract.Requires(program != null);
// this assumes that there is at most one procedure and only one associated implementation in the current context
-
- foreach(Declaration decl in program.TopLevelDeclarations) {
+
+ foreach (Declaration decl in program.TopLevelDeclarations) {
Implementation impl = decl as Implementation;
- if(impl != null) {
- if(impl.Name.Equals(procName)) {
- assert(impl.Proc != null);
+ if (impl != null) {
+ if (impl.Name.Equals(procName)) {
+ Contract.Assert(impl.Proc != null);
outProc = impl.Proc;
outImpl = impl;
return true;
}
}
}
-
- foreach(Declaration decl in program.TopLevelDeclarations) {
+
+ foreach (Declaration decl in program.TopLevelDeclarations) {
Procedure proc = decl as Procedure;
- if(proc != null) {
- if(proc.Name.Equals(procName)) {
+ if (proc != null) {
+ if (proc.Name.Equals(procName)) {
outProc = proc;
outImpl = null;
return false;
}
}
}
-
+
outProc = null;
outImpl = null;
return false;
}
}
-
+
///////////////////////////////////////////////////////////////////////////////////////////////////////////////
-
- public class CodeCopier
- {
+
+ public class CodeCopier {
public Substitution Subst;
public Substitution OldSubst;
- public CodeCopier(Hashtable! substMap) {
+ public CodeCopier(Hashtable substMap) {
+ Contract.Requires(substMap != null);
Subst = Substituter.SubstitutionFromHashtable(substMap);
}
-
- public CodeCopier(Hashtable! substMap, Hashtable! oldSubstMap) {
+
+ public CodeCopier(Hashtable substMap, Hashtable oldSubstMap) {
+ Contract.Requires(oldSubstMap != null);
+ Contract.Requires(substMap != null);
Subst = Substituter.SubstitutionFromHashtable(substMap);
OldSubst = Substituter.SubstitutionFromHashtable(oldSubstMap);
}
-
+
public CodeCopier() {
}
-
- public CmdSeq! CopyCmdSeq(CmdSeq! cmds) {
+
+ public CmdSeq CopyCmdSeq(CmdSeq cmds) {
+ Contract.Requires(cmds != null);
+ Contract.Ensures(Contract.Result<CmdSeq>() != null);
CmdSeq newCmds = new CmdSeq();
- foreach (Cmd! cmd in cmds) {
+ foreach (Cmd/*!*/ cmd in cmds) {
+ Contract.Assert(cmd != null);
newCmds.Add(CopyCmd(cmd));
}
return newCmds;
}
-
- public TransferCmd! CopyTransferCmd(TransferCmd! cmd) {
+
+ 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) {
- assert(gotocmd.labelNames != null);
+ if (gotocmd != null) {
+ Contract.Assert(gotocmd.labelNames != null);
StringSeq labels = new StringSeq();
labels.AddRange(gotocmd.labelNames);
transferCmd = new GotoCmd(cmd.tok, labels);
@@ -541,8 +608,10 @@ namespace Microsoft.Boogie { }
return transferCmd;
}
-
- public Cmd! CopyCmd(Cmd! cmd) {
+
+ public Cmd CopyCmd(Cmd cmd) {
+ Contract.Requires(cmd != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
if (Subst == null) {
return cmd;
} else if (OldSubst == null) {
@@ -551,8 +620,10 @@ namespace Microsoft.Boogie { return Substituter.ApplyReplacingOldExprs(Subst, OldSubst, cmd);
}
}
-
- public Expr! CopyExpr(Expr! expr) {
+
+ public Expr CopyExpr(Expr expr) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
if (Subst == null) {
return expr;
} else if (OldSubst == null) {
@@ -564,20 +635,26 @@ namespace Microsoft.Boogie { } // end class CodeCopier
- public class AxiomExpander : Duplicator
- {
- readonly Program! program;
- readonly TypecheckingContext! tc;
+ public class AxiomExpander : Duplicator {
+ readonly Program/*!*/ program;
+ readonly TypecheckingContext/*!*/ tc;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(program != null);
+ Contract.Invariant(tc != null);
+ }
+
- public AxiomExpander(Program! prog, TypecheckingContext! t)
- {
+ public AxiomExpander(Program prog, TypecheckingContext t) {
+ Contract.Requires(t != null);
+ Contract.Requires(prog != null);
program = prog;
tc = t;
}
- public void CollectExpansions()
- {
- foreach (Declaration! decl in program.TopLevelDeclarations) {
+ public void CollectExpansions() {
+ foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {
+ Contract.Assert(decl != null);
Axiom ax = decl as Axiom;
if (ax != null) {
bool expand = false;
@@ -590,23 +667,24 @@ namespace Microsoft.Boogie { }
Function f = decl as Function;
if (f != null && f.Body != null) {
- Variable[]! formals = new Variable [f.InParams.Length];
+ Variable[]/*!*/ formals = new Variable[f.InParams.Length];
+ Contract.Assert(formals != null);
for (int i = 0; i < formals.Length; ++i)
formals[i] = f.InParams[i];
AddExpansion(f, new Expansion(null, f.Body,
- new TypeVariableSeq (f.TypeParameters),
+ new TypeVariableSeq(f.TypeParameters),
formals));
}
}
}
- void Error(IToken! tok, string msg)
- {
+ void Error(IToken tok, string msg) {
+ Contract.Requires(tok != null);
tc.Error(tok, "expansion: " + msg);
}
- void AddExpansion(Expr! axiomBody, string? ignore)
- {
+ void AddExpansion(Expr axiomBody, string ignore) {
+ Contract.Requires(axiomBody != null);
// it would be sooooooooo much easier with pattern matching
ForallExpr all = axiomBody as ForallExpr;
if (all != null) {
@@ -614,18 +692,20 @@ namespace Microsoft.Boogie { 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;
+
+ 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 (),
+ Function fn = cce.NonNull((FunctionCall)func.Fun).Func;
+ Expansion exp = new Expansion(ignore, cce.NonNull(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) {
+ foreach (Expr/*!*/ e in func.Args) {
+ Contract.Assert(e != null);
IdentifierExpr id = e as IdentifierExpr;
if (id == null) {
Error(e.tok, "only identifiers supported as function arguments");
@@ -647,13 +727,15 @@ namespace Microsoft.Boogie { return;
}
- Dictionary<TypeVariable!, bool> typeVars = new Dictionary<TypeVariable!, bool>();
- foreach (TypeVariable! v in ((!)func.TypeParameters).FormalTypeParams) {
+ Dictionary<TypeVariable/*!*/, bool> typeVars = new Dictionary<TypeVariable/*!*/, bool>();
+ foreach (TypeVariable/*!*/ v in cce.NonNull(func.TypeParameters).FormalTypeParams) {
+ Contract.Assert(v != null);
if (!func.TypeParameters[v].IsVariable) {
Error(all.tok, "only identifiers supported as type parameters");
return;
}
- TypeVariable! formal = func.TypeParameters[v].AsVariable;
+ TypeVariable/*!*/ formal = func.TypeParameters[v].AsVariable;
+ Contract.Assert(formal != null);
exp.TypeParameters.Add(formal);
if (typeVars.ContainsKey(formal)) {
Error(all.tok, "an identifier was used more than once");
@@ -678,12 +760,13 @@ namespace Microsoft.Boogie { Error(axiomBody.tok, "axiom to be expanded must have form (forall VARS :: f(VARS) == expr(VARS))");
}
- void AddExpansion(Function! fn, Expansion! x) {
+ void AddExpansion(Function fn, Expansion x) {
+ Contract.Requires(x != null);
+ Contract.Requires(fn != null);
if (fn.expansions == null) {
- fn.expansions = new List<Expansion!>();
+ fn.expansions = new List<Expansion/*!*/>();
}
fn.expansions.Add(x);
}
}
-} // end namespace
-
+} // end namespace
\ No newline at end of file |