//----------------------------------------------------------------------------- // // Copyright (C) Microsoft Corporation. All Rights Reserved. // //----------------------------------------------------------------------------- //--------------------------------------------------------------------------------------------- // BoogiePL - Absy.cs //--------------------------------------------------------------------------------------------- namespace Microsoft.Boogie.AbstractInterpretation { using System.Diagnostics; using System.Diagnostics.Contracts; using System.Collections; using System.Collections.Generic; using System.Linq; public class CallSite { public readonly Implementation/*!*/ Impl; public readonly Block/*!*/ Block; public readonly int Statement; // invariant: Block[Statement] is CallCmd public readonly ProcedureSummaryEntry/*!*/ SummaryEntry; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Impl != null); Contract.Invariant(Block != null); Contract.Invariant(SummaryEntry != null); } public CallSite(Implementation impl, Block b, int stmt, ProcedureSummaryEntry summaryEntry) { Contract.Requires(summaryEntry != null); Contract.Requires(b != null); Contract.Requires(impl != null); this.Impl = impl; this.Block = b; this.Statement = stmt; this.SummaryEntry = summaryEntry; } } public class ProcedureSummaryEntry { private HashSet/*!*/ _returnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints public HashSet/*!*/ ReturnPoints { get { Contract.Ensures(Contract.Result>() != null); return this._returnPoints; } set { Contract.Requires(value != null); this._returnPoints = value; } } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this._returnPoints != null); } public ProcedureSummaryEntry() { this._returnPoints = new HashSet(); } } // class public class ProcedureSummary : ArrayList/**/ { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant( !IsReadOnly && !IsFixedSize); } public new ProcedureSummaryEntry/*!*/ this[int i] { get { Contract.Requires(0 <= i && i < Count); Contract.Ensures(Contract.Result() != null); return cce.NonNull((ProcedureSummaryEntry/*!*/)base[i]); } } } // class } // namespace namespace Microsoft.Boogie { using System; using System.Linq; using System.Collections; using System.Diagnostics; using System.Collections.Generic; using System.Collections.ObjectModel; using System.Diagnostics.Contracts; using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie.GraphUtil; using Set = GSet; [ContractClass(typeof(AbsyContracts))] public abstract class Absy { private IToken/*!*/ _tok; private int uniqueId; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this._tok != null); } public IToken tok { //Rename this property and "_tok" if possible get { Contract.Ensures(Contract.Result() != null); return this._tok; } set { Contract.Requires(value != null); this._tok = value; } } public int Line { get { return tok != null ? tok.line : -1; } } public int Col { get { return tok != null ? tok.col : -1; } } public Absy(IToken tok) { Contract.Requires(tok != null); this._tok = tok; this.uniqueId = System.Threading.Interlocked.Increment(ref CurrentAbsyNodeId); } private static int CurrentAbsyNodeId = -1; // We uniquely number every AST node to make them // suitable for our implementation of functional maps. // public int UniqueId { get { return this.uniqueId; } } private const int indent_size = 2; protected static string Indent(int level) { return new string(' ', (indent_size * level)); } [NeedsContracts] public abstract void Resolve(ResolutionContext/*!*/ rc); /// /// Requires the object to have been successfully resolved. /// /// [NeedsContracts] public abstract void Typecheck(TypecheckingContext/*!*/ tc); /// /// Intorduced this so the uniqueId is not the same on a cloned object. /// /// public virtual Absy Clone() { Contract.Ensures(Contract.Result() != null); Absy/*!*/ result = cce.NonNull((Absy/*!*/)this.MemberwiseClone()); result.uniqueId = System.Threading.Interlocked.Increment(ref CurrentAbsyNodeId); // BUGBUG?? if (InternalNumberedMetadata != null) { // This should probably use the lock result.InternalNumberedMetadata = new List(this.InternalNumberedMetadata); } return result; } public virtual Absy StdDispatch(StandardVisitor visitor) { Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); System.Diagnostics.Debug.Fail("Unknown Absy node type: " + this.GetType()); throw new System.NotImplementedException(); } #region numberedmetadata // Implementation of Numbered Metadata // This allows any number of arbitrary objects to be // associated with an instance of an Absy at run time // in a type safe manner using an integer as a key. // We could use a dictionary but we use a List for look up speed // For this to work well the user needs to use small integers as // keys. The list is created lazily to minimise memory overhead. private volatile List InternalNumberedMetadata = null; // The lock exists to ensure that InternalNumberedMetadata is a singleton // for every instance of this class. // It is static to minimise the memory overhead (we don't want a lock per instance). private static readonly Object NumberedMetadataLock = new object(); /// /// Gets the number of meta data objects associated with this instance /// /// The numbered meta data count. public int NumberedMetaDataCount { get { return InternalNumberedMetadata == null? 0: InternalNumberedMetadata.Count; } } /// /// Gets an IEnumerable over the numbered metadata associated /// with this instance. /// /// /// The numbered meta data enumerable that looks like the Enumerable /// of a dictionary. /// public IEnumerable> NumberedMetadata { get { if (InternalNumberedMetadata == null) return Enumerable.Empty>(); else return InternalNumberedMetadata.Select((v, index) => new KeyValuePair(index, v)); } } /// /// Gets the metatdata at specified index. /// ArgumentOutOfRange exception is raised if it is not available. /// InvalidCastExcpetion is raised if the metadata is available but the wrong type was requested. /// /// The stored metadata of type T /// The index of the metadata /// The type of the metadata object required public T GetMetadata(int index) { // We aren't using NumberedMetadataLock for speed. Perhaps we should be using it? if (InternalNumberedMetadata == null) throw new ArgumentOutOfRangeException(); if (InternalNumberedMetadata[index] is T) return (T) InternalNumberedMetadata[index]; else if (InternalNumberedMetadata[index] == null) { throw new InvalidCastException("Numbered metadata " + index + " is null which cannot be casted to " + typeof(T)); } else { throw new InvalidCastException("Numbered metadata " + index + " is of type " + InternalNumberedMetadata[index].GetType() + " rather than requested type " + typeof(T)); } } private void InitialiseNumberedMetadata() { // Ensure InternalNumberedMetadata is a singleton if (InternalNumberedMetadata == null) { lock (NumberedMetadataLock) { if (InternalNumberedMetadata == null) InternalNumberedMetadata = new List(); } } } /// /// Sets the metadata for this instace at a specified index. /// /// The index of the metadata /// The value to set /// The type of value public void SetMetadata(int index, T value) { InitialiseNumberedMetadata(); if (index < 0) throw new IndexOutOfRangeException(); lock (NumberedMetadataLock) { if (index < InternalNumberedMetadata.Count) InternalNumberedMetadata[index] = value; else { // Make sure expansion only happens once whilst we pad if (InternalNumberedMetadata.Capacity <= index) { // Use the next available power of 2 InternalNumberedMetadata.Capacity = (int) Math.Pow(2, Math.Ceiling(Math.Log(index+1,2))); } // Pad with nulls while (InternalNumberedMetadata.Count < index) InternalNumberedMetadata.Add (null); InternalNumberedMetadata.Add(value); Debug.Assert(InternalNumberedMetadata.Count == (index + 1)); } } } #endregion } [ContractClassFor(typeof(Absy))] public abstract class AbsyContracts : Absy { public override void Resolve(ResolutionContext rc) { Contract.Requires(rc != null); throw new NotImplementedException(); } public AbsyContracts() :base(null){ } public override void Typecheck(TypecheckingContext tc) { Contract.Requires(tc != null); throw new NotImplementedException(); } } public interface IPotentialErrorNode { TGet ErrorData { get; } } public interface IPotentialErrorNode : IPotentialErrorNode { new TSet ErrorData { set; } } public class Program : Absy { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(this.topLevelDeclarations)); Contract.Invariant(cce.NonNullElements(this.globalVariablesCache, true)); } public Program() : base(Token.NoToken) { this.topLevelDeclarations = new List(); } public void Emit(TokenTextWriter stream) { Contract.Requires(stream != null); stream.SetToken(this); this.topLevelDeclarations.Emit(stream); } public void ProcessDatatypeConstructors() { Dictionary constructors = new Dictionary(); List prunedTopLevelDeclarations = new List(); foreach (Declaration decl in TopLevelDeclarations) { Function func = decl as Function; if (func == null || !QKeyValue.FindBoolAttribute(decl.Attributes, "constructor")) { prunedTopLevelDeclarations.Add(decl); continue; } if (constructors.ContainsKey(func.Name)) continue; DatatypeConstructor constructor = new DatatypeConstructor(func); constructors.Add(func.Name, constructor); prunedTopLevelDeclarations.Add(constructor); } ClearTopLevelDeclarations(); AddTopLevelDeclarations(prunedTopLevelDeclarations); foreach (DatatypeConstructor f in constructors.Values) { for (int i = 0; i < f.InParams.Count; i++) { DatatypeSelector selector = new DatatypeSelector(f, i); f.selectors.Add(selector); AddTopLevelDeclaration(selector); } DatatypeMembership membership = new DatatypeMembership(f); f.membership = membership; AddTopLevelDeclaration(membership); } } /// /// Returns the number of name resolution errors. /// /// public int Resolve() { return Resolve((IErrorSink)null); } public int Resolve(IErrorSink errorSink) { ResolutionContext rc = new ResolutionContext(errorSink); Resolve(rc); return rc.ErrorCount; } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); Helpers.ExtraTraceInformation("Starting resolution"); foreach (var d in TopLevelDeclarations) { d.Register(rc); } ResolveTypes(rc); var prunedTopLevelDecls = new List(); foreach (var d in TopLevelDeclarations) { if (QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) { continue; } // resolve all the non-type-declarations if (!(d is TypeCtorDecl || d is TypeSynonymDecl)) { int e = rc.ErrorCount; d.Resolve(rc); if (CommandLineOptions.Clo.OverlookBoogieTypeErrors && rc.ErrorCount != e && d is Implementation) { // ignore this implementation System.Console.WriteLine("Warning: Ignoring implementation {0} because of translation resolution errors", ((Implementation)d).Name); rc.ErrorCount = e; continue; } } prunedTopLevelDecls.Add(d); } ClearTopLevelDeclarations(); AddTopLevelDeclarations(prunedTopLevelDecls); foreach (var v in Variables) { v.ResolveWhere(rc); } } private void ResolveTypes(ResolutionContext rc) { Contract.Requires(rc != null); // first resolve type constructors foreach (var d in TopLevelDeclarations.OfType()) { if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) d.Resolve(rc); } // collect type synonym declarations List/*!*/ synonymDecls = new List(); foreach (var d in TopLevelDeclarations.OfType()) { Contract.Assert(d != null); if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) synonymDecls.Add((TypeSynonymDecl)d); } // then resolve the type synonyms by a simple // fixed-point iteration TypeSynonymDecl.ResolveTypeSynonyms(synonymDecls, rc); } public int Typecheck() { return this.Typecheck((IErrorSink)null); } public int Typecheck(IErrorSink errorSink) { TypecheckingContext tc = new TypecheckingContext(errorSink); Typecheck(tc); return tc.ErrorCount; } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); Helpers.ExtraTraceInformation("Starting typechecking"); int oldErrorCount = tc.ErrorCount; foreach (var d in TopLevelDeclarations) { d.Typecheck(tc); } if (oldErrorCount == tc.ErrorCount) { // check whether any type proxies have remained uninstantiated TypeAmbiguitySeeker/*!*/ seeker = new TypeAmbiguitySeeker(tc); foreach (var d in TopLevelDeclarations) { seeker.Visit(d); } } } public override Absy Clone() { var cloned = (Program)base.Clone(); cloned.topLevelDeclarations = new List(); cloned.AddTopLevelDeclarations(topLevelDeclarations); return cloned; } [Rep] private List/*!*/ topLevelDeclarations; public IEnumerable TopLevelDeclarations { get { Contract.Ensures(cce.NonNullElements(Contract.Result>())); return topLevelDeclarations.AsReadOnly(); } set { Contract.Requires(value != null); // materialize the decls, in case there is any dependency // back on topLevelDeclarations var v = value.ToList(); // remove null elements v.RemoveAll(d => (d == null)); // now clear the decls ClearTopLevelDeclarations(); // and add the values AddTopLevelDeclarations(v); } } public void AddTopLevelDeclaration(Declaration decl) { Contract.Requires(!TopLevelDeclarationsAreFrozen); Contract.Requires(decl != null); topLevelDeclarations.Add(decl); this.globalVariablesCache = null; } public void AddTopLevelDeclarations(IEnumerable decls) { Contract.Requires(!TopLevelDeclarationsAreFrozen); Contract.Requires(cce.NonNullElements(decls)); topLevelDeclarations.AddRange(decls); this.globalVariablesCache = null; } public void RemoveTopLevelDeclaration(Declaration decl) { Contract.Requires(!TopLevelDeclarationsAreFrozen); topLevelDeclarations.Remove(decl); this.globalVariablesCache = null; } public void RemoveTopLevelDeclarations(Predicate match) { Contract.Requires(!TopLevelDeclarationsAreFrozen); topLevelDeclarations.RemoveAll(match); this.globalVariablesCache = null; } public void ClearTopLevelDeclarations() { Contract.Requires(!TopLevelDeclarationsAreFrozen); topLevelDeclarations.Clear(); this.globalVariablesCache = null; } bool topLevelDeclarationsAreFrozen; public bool TopLevelDeclarationsAreFrozen { get { return topLevelDeclarationsAreFrozen; } } public void FreezeTopLevelDeclarations() { topLevelDeclarationsAreFrozen = true; } Dictionary implementationsCache; public IEnumerable Implementations { get { if (implementationsCache != null) { return implementationsCache.Values; } var result = TopLevelDeclarations.OfType(); if (topLevelDeclarationsAreFrozen) { implementationsCache = result.ToDictionary(p => p.Id); } return result; } } public Implementation FindImplementation(string id) { Implementation result = null; if (implementationsCache != null && implementationsCache.TryGetValue(id, out result)) { return result; } else { return Implementations.FirstOrDefault(i => i.Id == id); } } List axiomsCache; public IEnumerable Axioms { get { if (axiomsCache != null) { return axiomsCache; } var result = TopLevelDeclarations.OfType(); if (topLevelDeclarationsAreFrozen) { axiomsCache = result.ToList(); } return result; } } Dictionary proceduresCache; public IEnumerable Procedures { get { if (proceduresCache != null) { return proceduresCache.Values; } var result = TopLevelDeclarations.OfType(); if (topLevelDeclarationsAreFrozen) { proceduresCache = result.ToDictionary(p => p.Name); } return result; } } public Procedure FindProcedure(string name) { Procedure result = null; if (proceduresCache != null && proceduresCache.TryGetValue(name, out result)) { return result; } else { return Procedures.FirstOrDefault(p => p.Name == name); } } Dictionary functionsCache; public IEnumerable Functions { get { if (functionsCache != null) { return functionsCache.Values; } var result = TopLevelDeclarations.OfType(); if (topLevelDeclarationsAreFrozen) { functionsCache = result.ToDictionary(f => f.Name); } return result; } } public Function FindFunction(string name) { Function result = null; if (functionsCache != null && functionsCache.TryGetValue(name, out result)) { return result; } else { return Functions.FirstOrDefault(f => f.Name == name); } } public IEnumerable Variables { get { return TopLevelDeclarations.OfType(); } } public IEnumerable Constants { get { return TopLevelDeclarations.OfType(); } } private IEnumerable globalVariablesCache = null; public List/*!*/ GlobalVariables { get { Contract.Ensures(cce.NonNullElements(Contract.Result>())); if (globalVariablesCache == null) globalVariablesCache = TopLevelDeclarations.OfType(); return new List(globalVariablesCache); } } public IEnumerable Blocks() { return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); } public void ComputeStronglyConnectedComponents() { foreach (var d in this.TopLevelDeclarations) { d.ComputeStronglyConnectedComponents(); } } /// /// Reset the abstract stated computed before /// public void ResetAbstractInterpretationState() { foreach (var d in this.TopLevelDeclarations) { d.ResetAbstractInterpretationState(); } } public void UnrollLoops(int n, bool uc) { Contract.Requires(0 <= n); foreach (var impl in Implementations) { if (impl.Blocks != null && impl.Blocks.Count > 0) { cce.BeginExpose(impl); { Block start = impl.Blocks[0]; Contract.Assume(start != null); Contract.Assume(cce.IsConsistent(start)); impl.Blocks = LoopUnroll.UnrollLoops(start, n, uc); impl.FreshenCaptureStates(); } cce.EndExpose(); } } } /// /// Finds blocks that break out of a loop in NaturalLoops(header, backEdgeNode) /// /// /// /// private HashSet GetBreakBlocksOfLoop(Block header, Block backEdgeNode, Graph/*!*/ g) { Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option"); var immSuccBlks = new HashSet(); var loopBlocks = g.NaturalLoops(header, backEdgeNode); foreach (Block/*!*/ block in loopBlocks) { Contract.Assert(block != null); var auxCmd = block.TransferCmd as GotoCmd; if (auxCmd == null) continue; foreach (var bl in auxCmd.labelTargets) { if (loopBlocks.Contains(bl)) continue; immSuccBlks.Add(bl); } } return immSuccBlks; } private HashSet GetBlocksInAllNaturalLoops(Block header, Graph/*!*/ g) { Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option"); var allBlocksInNaturalLoops = new HashSet(); foreach (Block/*!*/ source in g.BackEdgeNodes(header)) { Contract.Assert(source != null); g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b)); } return allBlocksInNaturalLoops; } void CreateProceduresForLoops(Implementation impl, Graph/*!*/ g, List/*!*/ loopImpls, Dictionary> fullMap) { Contract.Requires(impl != null); Contract.Requires(cce.NonNullElements(loopImpls)); // Enumerate the headers // for each header h: // create implementation p_h with // inputs = inputs, outputs, and locals of impl // outputs = outputs and locals of impl // locals = empty set // add call o := p_h(i) at the beginning of the header block // break the back edges whose target is h // Enumerate the headers again to create the bodies of p_h // for each header h: // compute the loop corresponding to h // make copies of all blocks in the loop for h // delete all target edges that do not go to a block in the loop // create a new entry block and a new return block // add edges from entry block to the loop header and the return block // add calls o := p_h(i) at the end of the blocks that are sources of back edges foreach (Block block in impl.Blocks) { AddToFullMap(fullMap, impl.Name, block.Label, block); } bool detLoopExtract = CommandLineOptions.Clo.DeterministicExtractLoops; Dictionary/*!*/>/*!*/ loopHeaderToInputs = new Dictionary/*!*/>(); Dictionary/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary/*!*/>(); Dictionary/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary/*!*/>(); Dictionary/*!*/ loopHeaderToLoopProc = new Dictionary(); Dictionary/*!*/ loopHeaderToCallCmd1 = new Dictionary(); Dictionary loopHeaderToCallCmd2 = new Dictionary(); Dictionary loopHeaderToAssignCmd = new Dictionary(); foreach (Block/*!*/ header in g.Headers) { Contract.Assert(header != null); Contract.Assert(header != null); List inputs = new List(); List outputs = new List(); List callInputs1 = new List(); List callOutputs1 = new List(); List callInputs2 = new List(); List callOutputs2 = new List(); List lhss = new List(); List rhss = new List(); Dictionary substMap = new Dictionary(); // Variable -> IdentifierExpr List/*!*/ targets = new List(); HashSet footprint = new HashSet(); foreach (Block/*!*/ b in g.BackEdgeNodes(header)) { Contract.Assert(b != null); HashSet immSuccBlks = new HashSet(); if (detLoopExtract) { //Need to get the blocks that exit the loop, as we need to add them to targets and footprint immSuccBlks = GetBreakBlocksOfLoop(header, b, g); } foreach (Block/*!*/ block in g.NaturalLoops(header, b).Union(immSuccBlks)) { Contract.Assert(block != null); foreach (Cmd/*!*/ cmd in block.Cmds) { Contract.Assert(cmd != null); cmd.AddAssignedVariables(targets); VariableCollector c = new VariableCollector(); c.Visit(cmd); footprint.UnionWith(c.usedVars); } } } List/*!*/ globalMods = new List(); Set targetSet = new Set(); foreach (Variable/*!*/ v in targets) { Contract.Assert(v != null); if (targetSet.Contains(v)) continue; targetSet.Add(v); if (v is GlobalVariable) globalMods.Add(new IdentifierExpr(Token.NoToken, v)); } foreach (Variable v in impl.InParams) { Contract.Assert(v != null); if (!footprint.Contains(v)) continue; callInputs1.Add(new IdentifierExpr(Token.NoToken, v)); Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in_" + v.Name, v.TypedIdent.Type), true); inputs.Add(f); callInputs2.Add(new IdentifierExpr(Token.NoToken, f)); substMap[v] = new IdentifierExpr(Token.NoToken, f); } foreach (Variable v in impl.OutParams) { Contract.Assert(v != null); if (!footprint.Contains(v)) continue; callInputs1.Add(new IdentifierExpr(Token.NoToken, v)); Formal f1 = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in_" + v.Name, v.TypedIdent.Type), true); inputs.Add(f1); if (targetSet.Contains(v)) { callOutputs1.Add(new IdentifierExpr(Token.NoToken, v)); Formal f2 = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out_" + v.Name, v.TypedIdent.Type), false); outputs.Add(f2); callInputs2.Add(new IdentifierExpr(Token.NoToken, f2)); callOutputs2.Add(new IdentifierExpr(Token.NoToken, f2)); lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, f2))); rhss.Add(new IdentifierExpr(Token.NoToken, f1)); substMap[v] = new IdentifierExpr(Token.NoToken, f2); } else { callInputs2.Add(new IdentifierExpr(Token.NoToken, f1)); substMap[v] = new IdentifierExpr(Token.NoToken, f1); } } foreach (Variable v in impl.LocVars) { Contract.Assert(v != null); if (!footprint.Contains(v)) continue; callInputs1.Add(new IdentifierExpr(Token.NoToken, v)); Formal f1 = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in_" + v.Name, v.TypedIdent.Type), true); inputs.Add(f1); if (targetSet.Contains(v)) { callOutputs1.Add(new IdentifierExpr(Token.NoToken, v)); Formal f2 = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out_" + v.Name, v.TypedIdent.Type), false); outputs.Add(f2); callInputs2.Add(new IdentifierExpr(Token.NoToken, f2)); callOutputs2.Add(new IdentifierExpr(Token.NoToken, f2)); lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, f2))); rhss.Add(new IdentifierExpr(Token.NoToken, f1)); substMap[v] = new IdentifierExpr(Token.NoToken, f2); } else { callInputs2.Add(new IdentifierExpr(Token.NoToken, f1)); substMap[v] = new IdentifierExpr(Token.NoToken, f1); } } loopHeaderToInputs[header] = inputs; loopHeaderToOutputs[header] = outputs; loopHeaderToSubstMap[header] = substMap; LoopProcedure loopProc = new LoopProcedure(impl, header, inputs, outputs, globalMods); loopHeaderToLoopProc[header] = loopProc; CallCmd callCmd1 = new CallCmd(Token.NoToken, loopProc.Name, callInputs1, callOutputs1); callCmd1.Proc = loopProc; loopHeaderToCallCmd1[header] = callCmd1; CallCmd callCmd2 = new CallCmd(Token.NoToken, loopProc.Name, callInputs2, callOutputs2); callCmd2.Proc = loopProc; loopHeaderToCallCmd2[header] = callCmd2; Debug.Assert(lhss.Count == rhss.Count); if (lhss.Count > 0) { AssignCmd assignCmd = new AssignCmd(Token.NoToken, lhss, rhss); loopHeaderToAssignCmd[header] = assignCmd; } } // Keep track of the new blocks created: maps a header node to the // header_last block that was created because of splitting header. Dictionary newBlocksCreated = new Dictionary(); bool headRecursion = false; // testing an option to put recursive call before loop body IEnumerable sortedHeaders = g.SortHeadersByDominance(); foreach (Block/*!*/ header in sortedHeaders) { Contract.Assert(header != null); LoopProcedure loopProc = loopHeaderToLoopProc[header]; Dictionary blockMap = new Dictionary(); HashSet dummyBlocks = new HashSet(); CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]); // fix me List inputs = loopHeaderToInputs[header]; List outputs = loopHeaderToOutputs[header]; int si_unique_loc = 1; // Added by AL: to distinguish the back edges foreach (Block/*!*/ source in g.BackEdgeNodes(header)) { Contract.Assert(source != null); foreach (Block/*!*/ block in g.NaturalLoops(header, source)) { Contract.Assert(block != null); if (blockMap.ContainsKey(block)) continue; Block newBlock = new Block(); newBlock.Label = block.Label; if (headRecursion && block == header) { CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone(); addUniqueCallAttr(si_unique_loc, callCmd); si_unique_loc++; newBlock.Cmds.Add(callCmd); // add the recursive call at head of loop var rest = codeCopier.CopyCmdSeq(block.Cmds); newBlock.Cmds.AddRange(rest); } else newBlock.Cmds = codeCopier.CopyCmdSeq(block.Cmds); blockMap[block] = newBlock; if (newBlocksCreated.ContainsKey(block)) { Block newBlock2 = new Block(); newBlock2.Label = newBlocksCreated[block].Label; newBlock2.Cmds = codeCopier.CopyCmdSeq(newBlocksCreated[block].Cmds); blockMap[newBlocksCreated[block]] = newBlock2; } //for detLoopExtract, need the immediate successors even outside the loop if (detLoopExtract) { GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd; Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null && auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1); //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source); foreach(var bl in auxGotoCmd.labelTargets) { if (!loopNodes.Contains(bl)) { Block auxNewBlock = new Block(); auxNewBlock.Label = ((Block)bl).Label; //these blocks may have read/write locals that are not present in naturalLoops //we need to capture these variables auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds); //add restoration code for such blocks if (loopHeaderToAssignCmd.ContainsKey(header)) { AssignCmd assignCmd = loopHeaderToAssignCmd[header]; auxNewBlock.Cmds.Add(assignCmd); } List lhsg = new List(); List/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies; foreach (IdentifierExpr gl in globalsMods) lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl)); List rhsg = new List(); foreach (IdentifierExpr gl in globalsMods) rhsg.Add(new OldExpr(Token.NoToken, gl)); if (lhsg.Count != 0) { AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg); auxNewBlock.Cmds.Add(globalAssignCmd); } blockMap[(Block)bl] = auxNewBlock; } } } } List cmdSeq; if (headRecursion) cmdSeq = new List(); else { CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone(); addUniqueCallAttr(si_unique_loc, callCmd); si_unique_loc++; cmdSeq = new List { callCmd }; } Block/*!*/ block1 = new Block(Token.NoToken, source.Label + "_dummy", new List{ new AssumeCmd(Token.NoToken, Expr.False) }, new ReturnCmd(Token.NoToken)); Block/*!*/ block2 = new Block(Token.NoToken, block1.Label, cmdSeq, new ReturnCmd(Token.NoToken)); impl.Blocks.Add(block1); dummyBlocks.Add(block1.Label); GotoCmd gotoCmd = source.TransferCmd as GotoCmd; Contract.Assert(gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Count >= 1); List/*!*/ newLabels = new List(); List/*!*/ newTargets = new List(); for (int i = 0; i < gotoCmd.labelTargets.Count; i++) { if (gotoCmd.labelTargets[i] == header) continue; newTargets.Add(gotoCmd.labelTargets[i]); newLabels.Add(gotoCmd.labelNames[i]); } newTargets.Add(block1); newLabels.Add(block1.Label); gotoCmd.labelNames = newLabels; gotoCmd.labelTargets = newTargets; blockMap[block1] = block2; } List/*!*/ blocks = new List(); Block exit = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); GotoCmd cmd = new GotoCmd(Token.NoToken, new List { cce.NonNull(blockMap[header]).Label, exit.Label }, new List { blockMap[header], exit }); if (detLoopExtract) //cutting the non-determinism cmd = new GotoCmd(Token.NoToken, new List { cce.NonNull(blockMap[header]).Label }, new List { blockMap[header] }); Block entry; List initCmds = new List(); if (loopHeaderToAssignCmd.ContainsKey(header)) { AssignCmd assignCmd = loopHeaderToAssignCmd[header]; initCmds.Add(assignCmd); } entry = new Block(Token.NoToken, "entry", initCmds, cmd); blocks.Add(entry); foreach (Block/*!*/ block in blockMap.Keys) { Contract.Assert(block != null); Block/*!*/ newBlock = cce.NonNull(blockMap[block]); GotoCmd gotoCmd = block.TransferCmd as GotoCmd; if (gotoCmd == null) { newBlock.TransferCmd = new ReturnCmd(Token.NoToken); } else { Contract.Assume(gotoCmd.labelNames != null && gotoCmd.labelTargets != null); List newLabels = new List(); List newTargets = new List(); for (int i = 0; i < gotoCmd.labelTargets.Count; i++) { Block target = gotoCmd.labelTargets[i]; if (blockMap.ContainsKey(target)) { newLabels.Add(gotoCmd.labelNames[i]); newTargets.Add(blockMap[target]); } } if (newTargets.Count == 0) { if (!detLoopExtract) newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); newBlock.TransferCmd = new ReturnCmd(Token.NoToken); } else { newBlock.TransferCmd = new GotoCmd(Token.NoToken, newLabels, newTargets); } } blocks.Add(newBlock); } blocks.Add(exit); Implementation loopImpl = new Implementation(Token.NoToken, loopProc.Name, new List(), inputs, outputs, new List(), blocks); loopImpl.Proc = loopProc; loopImpls.Add(loopImpl); // Make a (shallow) copy of the header before splitting it Block origHeader = new Block(header.tok, header.Label, header.Cmds, header.TransferCmd); // Finally, add call to the loop in the containing procedure string lastIterBlockName = header.Label + "_last"; Block lastIterBlock = new Block(Token.NoToken, lastIterBlockName, header.Cmds, header.TransferCmd); newBlocksCreated[header] = lastIterBlock; header.Cmds = new List { loopHeaderToCallCmd1[header] }; header.TransferCmd = new GotoCmd(Token.NoToken, new List { lastIterBlockName }, new List { lastIterBlock }); impl.Blocks.Add(lastIterBlock); blockMap[origHeader] = blockMap[header]; blockMap.Remove(header); Contract.Assert(fullMap[impl.Name][header.Label] == header); fullMap[impl.Name][header.Label] = origHeader; foreach (Block block in blockMap.Keys) { // Don't add dummy blocks to the map if (dummyBlocks.Contains(blockMap[block].Label)) continue; // Following two statements are for nested loops: compose map if (!fullMap[impl.Name].ContainsKey(block.Label)) continue; var target = fullMap[impl.Name][block.Label]; AddToFullMap(fullMap, loopProc.Name, blockMap[block].Label, target); } fullMap[impl.Name].Remove(header.Label); fullMap[impl.Name][lastIterBlockName] = origHeader; } } private void addUniqueCallAttr(int val, CallCmd cmd) { var a = new List(); a.Add(new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(val))); cmd.Attributes = new QKeyValue(Token.NoToken, "si_unique_call", a, cmd.Attributes); } private void AddToFullMap(Dictionary> fullMap, string procName, string blockName, Block block) { if (!fullMap.ContainsKey(procName)) fullMap[procName] = new Dictionary(); fullMap[procName][blockName] = block; } public static Graph BuildCallGraph(Program program) { Graph callGraph = new Graph(); Dictionary> procToImpls = new Dictionary>(); foreach (var proc in program.Procedures) { procToImpls[proc] = new HashSet(); } foreach (var impl in program.Implementations) { if (impl.SkipVerification) continue; callGraph.AddSource(impl); procToImpls[impl.Proc].Add(impl); } foreach (var impl in program.Implementations) { if (impl.SkipVerification) continue; foreach (Block b in impl.Blocks) { foreach (Cmd c in b.Cmds) { CallCmd cc = c as CallCmd; if (cc == null) continue; foreach (Implementation callee in procToImpls[cc.Proc]) { callGraph.AddEdge(impl, callee); } } } } return callGraph; } public static Graph/*!*/ GraphFromImpl(Implementation impl) { Contract.Requires(impl != null); Contract.Ensures(cce.NonNullElements(Contract.Result>().Nodes)); Contract.Ensures(Contract.Result>() != null); Graph g = new Graph(); g.AddSource(impl.Blocks[0]); // there is always at least one node in the graph foreach (Block b in impl.Blocks) { Contract.Assert(b != null); GotoCmd gtc = b.TransferCmd as GotoCmd; if (gtc != null) { foreach (Block/*!*/ dest in cce.NonNull(gtc.labelTargets)) { Contract.Assert(dest != null); g.AddEdge(b, dest); } } } return g; } public class IrreducibleLoopException : Exception {} public Graph ProcessLoops(Implementation impl) { while (true) { impl.PruneUnreachableBlocks(); impl.ComputePredecessorsForBlocks(); Graph/*!*/ g = GraphFromImpl(impl); g.ComputeLoops(); if (g.Reducible) { return g; } throw new IrreducibleLoopException(); #if USED_CODE System.Diagnostics.Debug.Assert(g.SplitCandidates.Count > 0); Block splitCandidate = null; foreach (Block b in g.SplitCandidates) { if (b.Predecessors.Length > 1) { splitCandidate = b; break; } } System.Diagnostics.Debug.Assert(splitCandidate != null); int count = 0; foreach (Block b in splitCandidate.Predecessors) { GotoCmd gotoCmd = (GotoCmd)b.TransferCmd; gotoCmd.labelNames.Remove(splitCandidate.Label); gotoCmd.labelTargets.Remove(splitCandidate); CodeCopier codeCopier = new CodeCopier(new Hashtable(), new Hashtable()); List newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds); TransferCmd newTransferCmd; GotoCmd splitGotoCmd = splitCandidate.TransferCmd as GotoCmd; if (splitGotoCmd == null) { newTransferCmd = new ReturnCmd(splitCandidate.tok); } else { List newLabelNames = new List(); newLabelNames.AddRange(splitGotoCmd.labelNames); List newLabelTargets = new List(); newLabelTargets.AddRange(splitGotoCmd.labelTargets); newTransferCmd = new GotoCmd(splitCandidate.tok, newLabelNames, newLabelTargets); } Block copy = new Block(splitCandidate.tok, splitCandidate.Label + count++, newCmdSeq, newTransferCmd); impl.Blocks.Add(copy); gotoCmd.AddTarget(copy); } #endif } } public Dictionary> ExtractLoops() { HashSet procsWithIrreducibleLoops = null; return ExtractLoops(out procsWithIrreducibleLoops); } public Dictionary> ExtractLoops(out HashSet procsWithIrreducibleLoops) { procsWithIrreducibleLoops = new HashSet(); List/*!*/ loopImpls = new List(); Dictionary> fullMap = new Dictionary>(); foreach (var impl in this.Implementations) { if (impl.Blocks != null && impl.Blocks.Count > 0) { try { Graph g = ProcessLoops(impl); CreateProceduresForLoops(impl, g, loopImpls, fullMap); } catch (IrreducibleLoopException) { System.Diagnostics.Debug.Assert(!fullMap.ContainsKey(impl.Name)); fullMap[impl.Name] = null; procsWithIrreducibleLoops.Add(impl.Name); if (CommandLineOptions.Clo.ExtractLoopsUnrollIrreducible) { // statically unroll loops in this procedure // First, build a map of the current blocks var origBlocks = new Dictionary(); foreach (var blk in impl.Blocks) origBlocks.Add(blk.Label, blk); // unroll Block start = impl.Blocks[0]; impl.Blocks = LoopUnroll.UnrollLoops(start, CommandLineOptions.Clo.RecursionBound, false); // Now construct the "map back" information // Resulting block label -> original block var blockMap = new Dictionary(); foreach (var blk in impl.Blocks) { var sl = LoopUnroll.sanitizeLabel(blk.Label); if (sl == blk.Label) blockMap.Add(blk.Label, blk); else { Contract.Assert(origBlocks.ContainsKey(sl)); blockMap.Add(blk.Label, origBlocks[sl]); } } fullMap[impl.Name] = blockMap; } } } } foreach (Implementation/*!*/ loopImpl in loopImpls) { Contract.Assert(loopImpl != null); AddTopLevelDeclaration(loopImpl); AddTopLevelDeclaration(loopImpl.Proc); } return fullMap; } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitProgram(this); } int extractedFunctionCount; public string FreshExtractedFunctionName() { var c = System.Threading.Interlocked.Increment(ref extractedFunctionCount); return string.Format("##extracted_function##{0}", c); } private int invariantGenerationCounter = 0; public Constant MakeExistentialBoolean() { Constant ExistentialBooleanConstant = new Constant(Token.NoToken, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false); invariantGenerationCounter++; ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True }); AddTopLevelDeclaration(ExistentialBooleanConstant); return ExistentialBooleanConstant; } public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null) { Constant ExistentialBooleanConstant = MakeExistentialBoolean(); IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant); PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e)); if (tag != null) invariant.Attributes = new QKeyValue(Token.NoToken, "tag", new List(new object[] { tag }), null); return invariant; } } //--------------------------------------------------------------------- // Declarations [ContractClass(typeof(DeclarationContracts))] public abstract class Declaration : Absy { public QKeyValue Attributes; public Declaration(IToken tok) : base(tok) { Contract.Requires(tok != null); } protected void EmitAttributes(TokenTextWriter stream) { Contract.Requires(stream != null); for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) { kv.Emit(stream); stream.Write(" "); } } protected void ResolveAttributes(ResolutionContext rc) { Contract.Requires(rc != null); for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) { kv.Resolve(rc); } } protected void TypecheckAttributes(TypecheckingContext rc) { Contract.Requires(rc != null); for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) { kv.Typecheck(rc); } } /// /// If the declaration has an attribute {:name} or {:name true}, then set "result" to "true" and return "true". /// If the declaration has an attribute {:name false}, then set "result" to "false" and return "true". /// Otherwise, return "false" and leave "result" unchanged (which gives the caller an easy way to indicate /// a default value if the attribute is not mentioned). /// If there is more than one attribute called :name, then the last attribute rules. /// public bool CheckBooleanAttribute(string name, ref bool result) { Contract.Requires(name != null); var kv = FindAttribute(name); if (kv != null) { if (kv.Params.Count == 0) { result = true; return true; } else if (kv.Params.Count == 1) { var lit = kv.Params[0] as LiteralExpr; if (lit != null && lit.isBool) { result = lit.asBool; return true; } } } return false; } /// /// Find and return the last occurrence of an attribute with the name "name", if any. If none, return null. /// public QKeyValue FindAttribute(string name) { Contract.Requires(name != null); QKeyValue res = null; for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) { if (kv.Key == name) { res = kv; } } return res; } // Look for {:name expr} in list of attributes. public Expr FindExprAttribute(string name) { Contract.Requires(name != null); Expr res = null; for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) { if (kv.Key == name) { if (kv.Params.Count == 1 && kv.Params[0] is Expr) { res = (Expr)kv.Params[0]; } } } return res; } // Look for {:name string} in list of attributes. public string FindStringAttribute(string name) { Contract.Requires(name != null); return QKeyValue.FindStringAttribute(this.Attributes, name); } // Look for {:name N} or {:name N} in list of attributes. Return result in 'result' // (which is not touched if there is no attribute specified). // // Returns false is there was an error processing the flag, true otherwise. public bool CheckIntAttribute(string name, ref int result) { Contract.Requires(name != null); Expr expr = FindExprAttribute(name); if (expr != null) { if (expr is LiteralExpr && ((LiteralExpr)expr).isBigNum) { result = ((LiteralExpr)expr).asBigNum.ToInt; } else { return false; } } return true; } public void AddAttribute(string name, params object[] vals) { Contract.Requires(name != null); QKeyValue kv; for (kv = this.Attributes; kv != null; kv = kv.Next) { if (kv.Key == name) { kv.AddParams(vals); break; } } if (kv == null) { Attributes = new QKeyValue(tok, name, new List(vals), Attributes); } } public abstract void Emit(TokenTextWriter/*!*/ stream, int level); public abstract void Register(ResolutionContext/*!*/ rc); /// /// Compute the strongly connected components of the declaration. /// By default, it does nothing /// public virtual void ComputeStronglyConnectedComponents() { /* Does nothing */ } /// /// Reset the abstract stated computed before /// public virtual void ResetAbstractInterpretationState() { /* does nothing */ } } [ContractClassFor(typeof(Declaration))] public abstract class DeclarationContracts : Declaration { public DeclarationContracts() :base(null){ } public override void Register(ResolutionContext rc) { Contract.Requires(rc != null); throw new NotImplementedException(); } public override void Emit(TokenTextWriter stream, int level) { Contract.Requires(stream != null); throw new NotImplementedException(); } } public class Axiom : Declaration { private Expr/*!*/ expression; public Expr Expr { get { Contract.Ensures(Contract.Result() != null); return this.expression; } set { Contract.Requires(value != null); this.expression = value; } } [ContractInvariantMethod] void ExprInvariant() { Contract.Invariant(this.expression != null); } public string Comment; public Axiom(IToken tok, Expr expr) : this(tok, expr, null) { Contract.Requires(expr != null); Contract.Requires(tok != null); } public Axiom(IToken/*!*/ tok, Expr/*!*/ expr, string comment) : base(tok) { Contract.Requires(tok != null); Contract.Requires(expr != null); this.expression = expr; Comment = comment; } public Axiom(IToken tok, Expr expr, string comment, QKeyValue kv) : this(tok, expr, comment) { Contract.Requires(expr != null); Contract.Requires(tok != null); this.Attributes = kv; } public bool DependenciesCollected { get; set; } ISet functionDependencies; public ISet FunctionDependencies { get { return functionDependencies; } } public void AddFunctionDependency(Function function) { Contract.Requires(function != null); if (functionDependencies == null) { functionDependencies = new HashSet(); } functionDependencies.Add(function); } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); if (Comment != null) { stream.WriteLine(this, level, "// " + Comment); } stream.Write(this, level, "axiom "); EmitAttributes(stream); this.Expr.Emit(stream); stream.WriteLine(";"); } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddAxiom(this); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); ResolveAttributes(rc); rc.StateMode = ResolutionContext.State.StateLess; Expr.Resolve(rc); rc.StateMode = ResolutionContext.State.Single; } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); TypecheckAttributes(tc); Expr.Typecheck(tc); Contract.Assert(Expr.Type != null); // follows from postcondition of Expr.Typecheck if (!Expr.Type.Unify(Type.Bool)) { tc.Error(this, "axioms must be of type bool"); } } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitAxiom(this); } } public abstract class NamedDeclaration : Declaration { private string/*!*/ name; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(name != null); } public string/*!*/ Name { get { Contract.Ensures(Contract.Result() != null); return this.name; } set { Contract.Requires(value != null); this.name = value; } } public int TimeLimit { get { int tl = CommandLineOptions.Clo.ProverKillTime; CheckIntAttribute("timeLimit", ref tl); return tl; } } public NamedDeclaration(IToken/*!*/ tok, string/*!*/ name) : base(tok) { Contract.Requires(tok != null); Contract.Requires(name != null); this.name = name; } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); return cce.NonNull(Name); } } public class TypeCtorDecl : NamedDeclaration { public readonly int Arity; public TypeCtorDecl(IToken/*!*/ tok, string/*!*/ name, int Arity) : base(tok, name) { Contract.Requires(tok != null); Contract.Requires(name != null); this.Arity = Arity; } public TypeCtorDecl(IToken/*!*/ tok, string/*!*/ name, int Arity, QKeyValue kv) : base(tok, name) { Contract.Requires(tok != null); Contract.Requires(name != null); this.Arity = Arity; this.Attributes = kv; } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.Write(this, level, "type "); EmitAttributes(stream); stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(Name)); for (int i = 0; i < Arity; ++i) stream.Write(" _"); stream.WriteLine(";"); } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddType(this); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); ResolveAttributes(rc); } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); TypecheckAttributes(tc); } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitTypeCtorDecl(this); } } public class TypeSynonymDecl : NamedDeclaration { private List/*!*/ typeParameters; public List TypeParameters { get { Contract.Ensures(Contract.Result>() != null); return this.typeParameters; } set { Contract.Requires(value != null); this.typeParameters = value; } } private Type/*!*/ body; public Type Body { get { Contract.Ensures(Contract.Result() != null); return this.body; } set { Contract.Requires(value != null); this.body = value; } } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this.body != null); Contract.Invariant(this.typeParameters != null); } public TypeSynonymDecl(IToken/*!*/ tok, string/*!*/ name, List/*!*/ typeParams, Type/*!*/ body) : base(tok, name) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(typeParams != null); Contract.Requires(body != null); this.typeParameters = typeParams; this.body = body; } public TypeSynonymDecl(IToken/*!*/ tok, string/*!*/ name, List/*!*/ typeParams, Type/*!*/ body, QKeyValue kv) : base(tok, name) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(typeParams != null); Contract.Requires(body != null); this.typeParameters = typeParams; this.body = body; this.Attributes = kv; } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.Write(this, level, "type "); EmitAttributes(stream); stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(Name)); if (TypeParameters.Count > 0) stream.Write(" "); TypeParameters.Emit(stream, " "); stream.Write(" = "); Body.Emit(stream); stream.WriteLine(";"); } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddType(this); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); ResolveAttributes(rc); int previousState = rc.TypeBinderState; try { foreach (TypeVariable/*!*/ v in TypeParameters) { Contract.Assert(v != null); rc.AddTypeBinder(v); } Body = Body.ResolveType(rc); } finally { rc.TypeBinderState = previousState; } } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); TypecheckAttributes(tc); } public static void ResolveTypeSynonyms(List/*!*/ synonymDecls, ResolutionContext/*!*/ rc) { Contract.Requires(cce.NonNullElements(synonymDecls)); Contract.Requires(rc != null); // then discover all dependencies between type synonyms IDictionary/*!*/>/*!*/ deps = new Dictionary/*!*/>(); foreach (TypeSynonymDecl/*!*/ decl in synonymDecls) { Contract.Assert(decl != null); List/*!*/ declDeps = new List(); FindDependencies(decl.Body, declDeps, rc); deps.Add(decl, declDeps); } List/*!*/ resolved = new List(); int unresolved = synonymDecls.Count - resolved.Count; while (unresolved > 0) { foreach (TypeSynonymDecl/*!*/ decl in synonymDecls) { Contract.Assert(decl != null); if (!resolved.Contains(decl) && deps[decl].All(d => resolved.Contains(d))) { decl.Resolve(rc); resolved.Add(decl); } } int newUnresolved = synonymDecls.Count - resolved.Count; if (newUnresolved < unresolved) { // we are making progress unresolved = newUnresolved; } else { // there have to be cycles in the definitions foreach (TypeSynonymDecl/*!*/ decl in synonymDecls) { Contract.Assert(decl != null); if (!resolved.Contains(decl)) { rc.Error(decl, "type synonym could not be resolved because of cycles: {0}" + " (replacing body with \"bool\" to continue resolving)", decl.Name); // we simply replace the bodies of all remaining type // synonyms with "bool" so that resolution can continue decl.Body = Type.Bool; decl.Resolve(rc); } } unresolved = 0; } } } // determine a list of all type synonyms that occur in "type" private static void FindDependencies(Type/*!*/ type, List/*!*/ deps, ResolutionContext/*!*/ rc) { Contract.Requires(type != null); Contract.Requires(cce.NonNullElements(deps)); Contract.Requires(rc != null); if (type.IsVariable || type.IsBasic) { // nothing } else if (type.IsUnresolved) { UnresolvedTypeIdentifier/*!*/ unresType = type.AsUnresolved; Contract.Assert(unresType != null); TypeSynonymDecl dep = rc.LookUpTypeSynonym(unresType.Name); if (dep != null) deps.Add(dep); foreach (Type/*!*/ subtype in unresType.Arguments) { Contract.Assert(subtype != null); FindDependencies(subtype, deps, rc); } } else if (type.IsMap) { MapType/*!*/ mapType = type.AsMap; Contract.Assert(mapType != null); foreach (Type/*!*/ subtype in mapType.Arguments) { Contract.Assert(subtype != null); FindDependencies(subtype, deps, rc); } FindDependencies(mapType.Result, deps, rc); } else if (type.IsCtor) { // this can happen because we allow types to be resolved multiple times CtorType/*!*/ ctorType = type.AsCtor; Contract.Assert(ctorType != null); foreach (Type/*!*/ subtype in ctorType.Arguments) { Contract.Assert(subtype != null); FindDependencies(subtype, deps, rc); } } else { System.Diagnostics.Debug.Fail("Did not expect this type during resolution: " + type); } } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitTypeSynonymDecl(this); } } public abstract class Variable : NamedDeclaration { private TypedIdent/*!*/ typedIdent; public TypedIdent TypedIdent { get { Contract.Ensures(Contract.Result() != null); return this.typedIdent; } set { Contract.Requires(value != null); this.typedIdent = value; } } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this.typedIdent != null); } public Variable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent) : base(tok, typedIdent.Name) { Contract.Requires(tok != null); Contract.Requires(typedIdent != null); this.typedIdent = typedIdent; } public Variable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, QKeyValue kv) : base(tok, typedIdent.Name) { Contract.Requires(tok != null); Contract.Requires(typedIdent != null); this.typedIdent = typedIdent; this.Attributes = kv; } public abstract bool IsMutable { get; } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.Write(this, level, "var "); EmitVitals(stream, level, true); stream.WriteLine(";"); } public void EmitVitals(TokenTextWriter stream, int level, bool emitAttributes) { Contract.Requires(stream != null); if (emitAttributes) { EmitAttributes(stream); } if (CommandLineOptions.Clo.PrintWithUniqueASTIds && this.TypedIdent.HasName) { stream.Write("h{0}^^", this.GetHashCode()); // the idea is that this will prepend the name printed by TypedIdent.Emit } this.TypedIdent.Emit(stream); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); this.TypedIdent.Resolve(rc); } public void ResolveWhere(ResolutionContext rc) { Contract.Requires(rc != null); if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && this.TypedIdent.WhereExpr != null) { rc.Error(tok, "assumption variable may not be declared with a where clause"); } if (this.TypedIdent.WhereExpr != null) { this.TypedIdent.WhereExpr.Resolve(rc); } ResolveAttributes(rc); } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); TypecheckAttributes(tc); this.TypedIdent.Typecheck(tc); if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && !this.TypedIdent.Type.IsBool) { tc.Error(tok, "assumption variable must be of type 'bool'"); } } } public class VariableComparer : IComparer { public int Compare(object a, object b) { Variable A = a as Variable; Variable B = b as Variable; if (A == null || B == null) { throw new ArgumentException("VariableComparer works only on objects of type Variable"); } return cce.NonNull(A.Name).CompareTo(B.Name); } } // class to specify the <:-parents of the values of constants public class ConstantParent { public readonly IdentifierExpr/*!*/ Parent; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Parent != null); } // if true, the sub-dag underneath this constant-parent edge is // disjoint from all other unique sub-dags public readonly bool Unique; public ConstantParent(IdentifierExpr parent, bool unique) { Contract.Requires(parent != null); Parent = parent; Unique = unique; } } public class Constant : Variable { // when true, the value of this constant is meant to be distinct // from all other constants. public readonly bool Unique; // the <:-parents of the value of this constant. If the field is // null, no information about the parents is provided, which means // that the parental situation is unconstrained. public readonly ReadOnlyCollection Parents; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(Parents, true)); } // if true, it is assumed that the immediate <:-children of the // value of this constant are completely specified public readonly bool ChildrenComplete; public Constant(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent) : base(tok, typedIdent) { Contract.Requires(tok != null); Contract.Requires(typedIdent != null); Contract.Requires(typedIdent.Name != null && (!typedIdent.HasName || typedIdent.Name.Length > 0)); Contract.Requires(typedIdent.WhereExpr == null); this.Unique = true; this.Parents = null; this.ChildrenComplete = false; } public Constant(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, bool unique) : base(tok, typedIdent) { Contract.Requires(tok != null); Contract.Requires(typedIdent != null); Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0); Contract.Requires(typedIdent.WhereExpr == null); this.Unique = unique; this.Parents = null; this.ChildrenComplete = false; } public Constant(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, bool unique, IEnumerable parents, bool childrenComplete, QKeyValue kv) : base(tok, typedIdent, kv) { Contract.Requires(tok != null); Contract.Requires(typedIdent != null); Contract.Requires(cce.NonNullElements(parents, true)); Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0); Contract.Requires(typedIdent.WhereExpr == null); this.Unique = unique; this.Parents = parents == null ? null : new ReadOnlyCollection(parents.ToList()); this.ChildrenComplete = childrenComplete; } public override bool IsMutable { get { return false; } } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.Write(this, level, "const "); EmitAttributes(stream); if (this.Unique) { stream.Write(this, level, "unique "); } EmitVitals(stream, level, false); if (Parents != null || ChildrenComplete) { stream.Write(this, level, " extends"); string/*!*/ sep = " "; foreach (ConstantParent/*!*/ p in cce.NonNull(Parents)) { Contract.Assert(p != null); stream.Write(this, level, sep); sep = ", "; if (p.Unique) stream.Write(this, level, "unique "); p.Parent.Emit(stream); } if (ChildrenComplete) stream.Write(this, level, " complete"); } stream.WriteLine(";"); } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddVariable(this, true); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); base.Resolve(rc); if (Parents != null) { foreach (ConstantParent/*!*/ p in Parents) { Contract.Assert(p != null); p.Parent.Resolve(rc); if (p.Parent.Decl != null && !(p.Parent.Decl is Constant)) rc.Error(p.Parent, "the parent of a constant has to be a constant"); if (this.Equals(p.Parent.Decl)) rc.Error(p.Parent, "constant cannot be its own parent"); } } // check that no parent occurs twice // (could be optimised) if (Parents != null) { for (int i = 0; i < Parents.Count; ++i) { if (Parents[i].Parent.Decl != null) { for (int j = i + 1; j < Parents.Count; ++j) { if (Parents[j].Parent.Decl != null && cce.NonNull(Parents[i].Parent.Decl).Equals(Parents[j].Parent.Decl)) rc.Error(Parents[j].Parent, "{0} occurs more than once as parent", Parents[j].Parent.Decl); } } } } } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); base.Typecheck(tc); if (Parents != null) { foreach (ConstantParent/*!*/ p in Parents) { Contract.Assert(p != null); p.Parent.Typecheck(tc); if (!cce.NonNull(p.Parent.Decl).TypedIdent.Type.Unify(this.TypedIdent.Type)) tc.Error(p.Parent, "parent of constant has incompatible type ({0} instead of {1})", p.Parent.Decl.TypedIdent.Type, this.TypedIdent.Type); } } } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitConstant(this); } } public class GlobalVariable : Variable { public GlobalVariable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent) : base(tok, typedIdent) { Contract.Requires(tok != null); Contract.Requires(typedIdent != null); } public GlobalVariable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, QKeyValue kv) : base(tok, typedIdent, kv) { Contract.Requires(tok != null); Contract.Requires(typedIdent != null); } public override bool IsMutable { get { return true; } } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddVariable(this, true); } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitGlobalVariable(this); } } public class Formal : Variable { public bool InComing; public Formal(IToken tok, TypedIdent typedIdent, bool incoming, QKeyValue kv) : base(tok, typedIdent, kv) { Contract.Requires(typedIdent != null); Contract.Requires(tok != null); InComing = incoming; } public Formal(IToken tok, TypedIdent typedIdent, bool incoming) : this(tok, typedIdent, incoming, null) { Contract.Requires(typedIdent != null); Contract.Requires(tok != null); } public override bool IsMutable { get { return !InComing; } } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddVariable(this, false); } /// /// Given a sequence of Formal declarations, returns sequence of Formals like the given one but without where clauses /// and without any attributes. /// The Type of each Formal is cloned. /// public static List StripWhereClauses(List w) { Contract.Requires(w != null); Contract.Ensures(Contract.Result>() != null); List s = new List(); foreach (Variable/*!*/ v in w) { Contract.Assert(v != null); Formal f = (Formal)v; TypedIdent ti = f.TypedIdent; s.Add(new Formal(f.tok, new TypedIdent(ti.tok, ti.Name, ti.Type.CloneUnresolved()), f.InComing, null)); } return s; } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitFormal(this); } } public class LocalVariable : Variable { public LocalVariable(IToken tok, TypedIdent typedIdent, QKeyValue kv) : base(tok, typedIdent, kv) { Contract.Requires(typedIdent != null); Contract.Requires(tok != null); } public LocalVariable(IToken tok, TypedIdent typedIdent) : base(tok, typedIdent, null) { Contract.Requires(typedIdent != null); Contract.Requires(tok != null); } public override bool IsMutable { get { return true; } } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddVariable(this, false); } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitLocalVariable(this); } } public class Incarnation : LocalVariable { public int incarnationNumber; public Incarnation(Variable/*!*/ var, int i) : base( var.tok, new TypedIdent(var.TypedIdent.tok, var.TypedIdent.Name + "@" + i, var.TypedIdent.Type) ) { Contract.Requires(var != null); incarnationNumber = i; } } public class BoundVariable : Variable { public BoundVariable(IToken tok, TypedIdent typedIdent) : base(tok, typedIdent) { Contract.Requires(typedIdent != null); Contract.Requires(tok != null); Contract.Requires(typedIdent.WhereExpr == null); } public BoundVariable(IToken tok, TypedIdent typedIdent, QKeyValue kv) : base(tok, typedIdent, kv) { Contract.Requires(typedIdent != null); Contract.Requires(tok != null); Contract.Requires(typedIdent.WhereExpr == null); } public override bool IsMutable { get { return false; } } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddVariable(this, false); } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitBoundVariable(this); } } public abstract class DeclWithFormals : NamedDeclaration { public List/*!*/ TypeParameters; private /*readonly--except in StandardVisitor*/ List/*!*/ inParams, outParams; public List/*!*/ InParams { get { Contract.Ensures(Contract.Result>() != null); return this.inParams; } set { Contract.Requires(value != null); this.inParams = value; } } public List/*!*/ OutParams { get { Contract.Ensures(Contract.Result>() != null); return this.outParams; } set { Contract.Requires(value != null); this.outParams = value; } } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(TypeParameters != null); Contract.Invariant(this.inParams != null); Contract.Invariant(this.outParams != null); } public DeclWithFormals(IToken tok, string name, List typeParams, List inParams, List outParams) : base(tok, name) { Contract.Requires(inParams != null); Contract.Requires(outParams != null); Contract.Requires(typeParams != null); Contract.Requires(name != null); Contract.Requires(tok != null); this.TypeParameters = typeParams; this.inParams = inParams; this.outParams = outParams; } protected DeclWithFormals(DeclWithFormals that) : base(that.tok, cce.NonNull(that.Name)) { Contract.Requires(that != null); this.TypeParameters = that.TypeParameters; this.inParams = cce.NonNull(that.InParams); this.outParams = cce.NonNull(that.OutParams); } public byte[] MD5Checksum_; public byte[] MD5Checksum { get { if (MD5Checksum_ == null) { var c = Checksum; if (c != null) { MD5Checksum_ = System.Security.Cryptography.MD5.Create().ComputeHash(System.Text.Encoding.UTF8.GetBytes(c)); } } return MD5Checksum_; } } public byte[] MD5DependencyChecksum_; public byte[] MD5DependencyChecksum { get { Contract.Requires(DependenciesCollected); if (MD5DependencyChecksum_ == null && MD5Checksum != null) { var c = MD5Checksum; var transFuncDeps = new HashSet(); if (procedureDependencies != null) { foreach (var p in procedureDependencies) { if (p.FunctionDependencies != null) { foreach (var f in p.FunctionDependencies) { transFuncDeps.Add(f); } } var pc = p.MD5Checksum; if (pc == null) { return null; } c = ChecksumHelper.CombineChecksums(c, pc, true); } } if (FunctionDependencies != null) { foreach (var f in FunctionDependencies) { transFuncDeps.Add(f); } } var q = new Queue(transFuncDeps); while (q.Any()) { var f = q.Dequeue(); var fc = f.MD5Checksum; if (fc == null) { return null; } c = ChecksumHelper.CombineChecksums(c, fc, true); if (f.FunctionDependencies != null) { foreach (var d in f.FunctionDependencies) { if (!transFuncDeps.Contains(d)) { transFuncDeps.Add(d); q.Enqueue(d); } } } } MD5DependencyChecksum_ = c; } return MD5DependencyChecksum_; } } public string Checksum { get { return FindStringAttribute("checksum"); } } string dependencyChecksum; public string DependencyChecksum { get { if (dependencyChecksum == null && DependenciesCollected && MD5DependencyChecksum != null) { dependencyChecksum = BitConverter.ToString(MD5DependencyChecksum); } return dependencyChecksum; } } public bool DependenciesCollected { get; set; } ISet procedureDependencies; public ISet ProcedureDependencies { get { return procedureDependencies; } } public void AddProcedureDependency(Procedure procedure) { Contract.Requires(procedure != null); if (procedureDependencies == null) { procedureDependencies = new HashSet(); } procedureDependencies.Add(procedure); } ISet functionDependencies; public ISet FunctionDependencies { get { return functionDependencies; } } public void AddFunctionDependency(Function function) { Contract.Requires(function != null); if (functionDependencies == null) { functionDependencies = new HashSet(); } functionDependencies.Add(function); } public bool SignatureEquals(DeclWithFormals other) { Contract.Requires(other != null); string sig = null; string otherSig = null; using (var strWr = new System.IO.StringWriter()) using (var tokTxtWr = new TokenTextWriter("", strWr, false, false)) { EmitSignature(tokTxtWr, this is Function); sig = strWr.ToString(); } using (var otherStrWr = new System.IO.StringWriter()) using (var otherTokTxtWr = new TokenTextWriter("", otherStrWr, false, false)) { EmitSignature(otherTokTxtWr, other is Function); otherSig = otherStrWr.ToString(); } return sig == otherSig; } protected void EmitSignature(TokenTextWriter stream, bool shortRet) { Contract.Requires(stream != null); Type.EmitOptionalTypeParams(stream, TypeParameters); stream.Write("("); stream.push(); InParams.Emit(stream, true); stream.Write(")"); stream.sep(); if (shortRet) { Contract.Assert(OutParams.Count == 1); stream.Write(" : "); cce.NonNull(OutParams[0]).TypedIdent.Type.Emit(stream); } else if (OutParams.Count > 0) { stream.Write(" returns ("); OutParams.Emit(stream, true); stream.Write(")"); } stream.pop(); } // Register all type parameters at the resolution context protected void RegisterTypeParameters(ResolutionContext rc) { Contract.Requires(rc != null); foreach (TypeVariable/*!*/ v in TypeParameters) { Contract.Assert(v != null); rc.AddTypeBinder(v); } } protected void SortTypeParams() { List/*!*/ allTypes = new List(InParams.Select(Item => Item.TypedIdent.Type).ToArray()); Contract.Assert(allTypes != null); allTypes.AddRange(new List(OutParams.Select(Item => Item.TypedIdent.Type).ToArray())); TypeParameters = Type.SortTypeParams(TypeParameters, allTypes, null); } /// /// Adds the given formals to the current variable context, and then resolves /// the types of those formals. Does NOT resolve the where clauses of the /// formals. /// Relies on the caller to first create, and later tear down, that variable /// context. /// /// protected void RegisterFormals(List formals, ResolutionContext rc) { Contract.Requires(rc != null); Contract.Requires(formals != null); foreach (Formal/*!*/ f in formals) { Contract.Assert(f != null); if (f.Name != TypedIdent.NoName) { rc.AddVariable(f, false); } f.Resolve(rc); } } /// /// Resolves the where clauses (and attributes) of the formals. /// /// protected void ResolveFormals(List formals, ResolutionContext rc) { Contract.Requires(rc != null); Contract.Requires(formals != null); foreach (Formal/*!*/ f in formals) { Contract.Assert(f != null); f.ResolveWhere(rc); } } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); TypecheckAttributes(tc); foreach (Formal/*!*/ p in InParams) { Contract.Assert(p != null); p.Typecheck(tc); } foreach (Formal/*!*/ p in OutParams) { Contract.Assert(p != null); p.Typecheck(tc); } } } public class DatatypeConstructor : Function { public List selectors; public DatatypeMembership membership; public DatatypeConstructor(Function func) : base(func.tok, func.Name, func.TypeParameters, func.InParams, func.OutParams[0], func.Comment, func.Attributes) { selectors = new List(); } public override void Resolve(ResolutionContext rc) { HashSet selectorNames = new HashSet(); foreach (DatatypeSelector selector in selectors) { if (selector.Name.StartsWith("#")) { rc.Error(selector.tok, "The selector must be a non-empty string"); } else { if (selectorNames.Contains(selector.Name)) rc.Error(this.tok, "The selectors for a constructor must be distinct strings"); else selectorNames.Add(selector.Name); } } base.Resolve(rc); } public override void Typecheck(TypecheckingContext tc) { CtorType outputType = this.OutParams[0].TypedIdent.Type as CtorType; if (outputType == null || !outputType.IsDatatype()) { tc.Error(tok, "The output type of a constructor must be a datatype"); } base.Typecheck(tc); } } public class DatatypeSelector : Function { public Function constructor; public int index; public DatatypeSelector(Function constructor, int index) : base(constructor.InParams[index].tok, constructor.InParams[index].Name + "#" + constructor.Name, new List { new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true) }, new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.InParams[index].TypedIdent.Type), false)) { this.constructor = constructor; this.index = index; } public override void Emit(TokenTextWriter stream, int level) { } } public class DatatypeMembership : Function { public Function constructor; public DatatypeMembership(Function constructor) : base(constructor.tok, "is#" + constructor.Name, new List { new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true) }, new Formal(constructor.tok, new TypedIdent(constructor.tok, "", Type.Bool), false)) { this.constructor = constructor; } public override void Emit(TokenTextWriter stream, int level) { } } public class Function : DeclWithFormals { public string Comment; // the body is only set if the function is declared with {:inline} public Expr Body; public Axiom DefinitionAxiom; public IList otherDefinitionAxioms; public IEnumerable OtherDefinitionAxioms { get { return otherDefinitionAxioms; } } public void AddOtherDefinitionAxiom(Axiom axiom) { Contract.Requires(axiom != null); if (otherDefinitionAxioms == null) { otherDefinitionAxioms = new List(); } otherDefinitionAxioms.Add(axiom); } public bool doingExpansion; private bool neverTrigger; private bool neverTriggerComputed; public string OriginalLambdaExprAsString; public Function(IToken tok, string name, List args, Variable result) : this(tok, name, new List(), args, result, null) { Contract.Requires(result != null); Contract.Requires(args != null); Contract.Requires(name != null); Contract.Requires(tok != null); //:this(tok, name, new List(), args, result, null); } public Function(IToken tok, string name, List typeParams, List args, Variable result) : this(tok, name, typeParams, args, result, null) { Contract.Requires(result != null); Contract.Requires(args != null); Contract.Requires(typeParams != null); Contract.Requires(name != null); Contract.Requires(tok != null); //:this(tok, name, typeParams, args, result, null); } public Function(IToken tok, string name, List args, Variable result, string comment) : this(tok, name, new List(), args, result, comment) { Contract.Requires(result != null); Contract.Requires(args != null); Contract.Requires(name != null); Contract.Requires(tok != null); //:this(tok, name, new List(), args, result, comment); } public Function(IToken tok, string name, List typeParams, List args, Variable/*!*/ result, string comment) : base(tok, name, typeParams, args, new List { result }) { Contract.Requires(result != null); Contract.Requires(args != null); Contract.Requires(typeParams != null); Contract.Requires(name != null); Contract.Requires(tok != null); Comment = comment; } public Function(IToken tok, string name, List typeParams, List args, Variable result, string comment, QKeyValue kv) : this(tok, name, typeParams, args, result, comment) { Contract.Requires(args != null); Contract.Requires(result != null); Contract.Requires(typeParams != null); Contract.Requires(name != null); Contract.Requires(tok != null); //:this(tok, name, typeParams, args, result, comment); this.Attributes = kv; } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); if (Comment != null) { stream.WriteLine(this, level, "// " + Comment); } stream.Write(this, level, "function "); EmitAttributes(stream); if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline")) { // Boogie inlines any function whose .Body field is non-null. The parser populates the .Body field // is the :inline attribute is present, but if someone creates the Boogie file directly as an AST, then // the :inline attribute may not be there. We'll make sure it's printed, so one can see that this means // that the body will be inlined. stream.Write("{:inline} "); } if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { stream.Write("h{0}^^{1}", this.GetHashCode(), TokenTextWriter.SanitizeIdentifier(this.Name)); } else { stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); } EmitSignature(stream, true); if (Body != null) { stream.WriteLine(); stream.WriteLine("{"); stream.Write(level + 1, ""); Body.Emit(stream); stream.WriteLine(); stream.WriteLine("}"); } else { stream.WriteLine(";"); } } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddProcedure(this); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); int previousTypeBinderState = rc.TypeBinderState; try { RegisterTypeParameters(rc); rc.PushVarContext(); RegisterFormals(InParams, rc); RegisterFormals(OutParams, rc); ResolveAttributes(rc); if (Body != null) { rc.StateMode = ResolutionContext.State.StateLess; Body.Resolve(rc); rc.StateMode = ResolutionContext.State.Single; } rc.PopVarContext(); Type.CheckBoundVariableOccurrences(TypeParameters, new List(InParams.Select(Item => Item.TypedIdent.Type).ToArray()), new List(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()), this.tok, "function arguments", rc); } finally { rc.TypeBinderState = previousTypeBinderState; } SortTypeParams(); } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); // PR: why was the base call left out previously? base.Typecheck(tc); // TypecheckAttributes(tc); if (Body != null) { Body.Typecheck(tc); if (!cce.NonNull(Body.Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type)) tc.Error(Body, "function body with invalid type: {0} (expected: {1})", Body.Type, cce.NonNull(OutParams[0]).TypedIdent.Type); } } public bool NeverTrigger { get { if (!neverTriggerComputed) { this.CheckBooleanAttribute("never_pattern", ref neverTrigger); neverTriggerComputed = true; } return neverTrigger; } } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitFunction(this); } public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null) { Contract.Requires(definition != null); List dummies = new List(); List callArgs = new List(); int i = 0; foreach (Formal/*!*/ f in InParams) { Contract.Assert(f != null); string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i; dummies.Add(new BoundVariable(f.tok, new TypedIdent(f.tok, nm, f.TypedIdent.Type))); callArgs.Add(new IdentifierExpr(f.tok, nm)); i++; } List/*!*/ quantifiedTypeVars = new List(); foreach (TypeVariable/*!*/ t in TypeParameters) { Contract.Assert(t != null); quantifiedTypeVars.Add(new TypeVariable(tok, t.Name)); } Expr call = new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, Name)), callArgs); // specify the type of the function, because it might be that // type parameters only occur in the output type call = Expr.CoerceType(tok, call, (Type)OutParams[0].TypedIdent.Type.Clone()); Expr def = Expr.Binary(tok, BinaryOperator.Opcode.Eq, call, definition); if (quantifiedTypeVars.Count != 0 || dummies.Count != 0) { def = new ForallExpr(tok, quantifiedTypeVars, dummies, kv, new Trigger(tok, true, new List { call }, null), def); } DefinitionAxiom = new Axiom(tok, def); return DefinitionAxiom; } } public class Macro : Function { public Macro(IToken tok, string name, List args, Variable result) : base(tok, name, args, result) { } } public class Requires : Absy, IPotentialErrorNode { public readonly bool Free; private Expr/*!*/ _condition; public Expr/*!*/ Condition { get { Contract.Ensures(Contract.Result() != null); return this._condition; } set { Contract.Requires(value != null); this._condition = value; } } public string Comment; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this._condition != null); } // TODO: convert to use generics private string errorData; public string ErrorData { get { return errorData; } set { errorData = value; } } private MiningStrategy errorDataEnhanced; public MiningStrategy ErrorDataEnhanced { get { return errorDataEnhanced; } set { errorDataEnhanced = value; } } public QKeyValue Attributes; public String ErrorMessage { get { return QKeyValue.FindStringAttribute(Attributes, "msg"); } } public Requires(IToken token, bool free, Expr condition, string comment, QKeyValue kv) : base(token) { Contract.Requires(condition != null); Contract.Requires(token != null); this.Free = free; this._condition = condition; this.Comment = comment; this.Attributes = kv; } public Requires(IToken token, bool free, Expr condition, string comment) : this(token, free, condition, comment, null) { Contract.Requires(condition != null); Contract.Requires(token != null); //:this(token, free, condition, comment, null); } public Requires(bool free, Expr condition) : this(Token.NoToken, free, condition, null) { Contract.Requires(condition != null); //:this(Token.NoToken, free, condition, null); } public Requires(bool free, Expr condition, string comment) : this(Token.NoToken, free, condition, comment) { Contract.Requires(condition != null); //:this(Token.NoToken, free, condition, comment); } public void Emit(TokenTextWriter stream, int level) { Contract.Requires(stream != null); if (Comment != null) { stream.WriteLine(this, level, "// " + Comment); } stream.Write(this, level, "{0}requires ", Free ? "free " : ""); Cmd.EmitAttributes(stream, Attributes); this.Condition.Emit(stream); stream.WriteLine(";"); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); this.Condition.Resolve(rc); } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); this.Condition.Typecheck(tc); Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck if (!this.Condition.Type.Unify(Type.Bool)) { tc.Error(this, "preconditions must be of type bool"); } } public override Absy StdDispatch(StandardVisitor visitor) { return visitor.VisitRequires(this); } } public class Ensures : Absy, IPotentialErrorNode { public readonly bool Free; private Expr/*!*/ _condition; public Expr/*!*/ Condition { get { Contract.Ensures(Contract.Result() != null); return this._condition; } set { Contract.Requires(value != null); this._condition = value; } } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this._condition != null); } public string Comment; // TODO: convert to use generics private string errorData; public string ErrorData { get { return errorData; } set { errorData = value; } } private MiningStrategy errorDataEnhanced; public MiningStrategy ErrorDataEnhanced { get { return errorDataEnhanced; } set { errorDataEnhanced = value; } } public String ErrorMessage { get { return QKeyValue.FindStringAttribute(Attributes, "msg"); } } public QKeyValue Attributes; public Ensures(IToken token, bool free, Expr/*!*/ condition, string comment, QKeyValue kv) : base(token) { Contract.Requires(condition != null); Contract.Requires(token != null); this.Free = free; this._condition = condition; this.Comment = comment; this.Attributes = kv; } public Ensures(IToken token, bool free, Expr condition, string comment) : this(token, free, condition, comment, null) { Contract.Requires(condition != null); Contract.Requires(token != null); //:this(token, free, condition, comment, null); } public Ensures(bool free, Expr condition) : this(Token.NoToken, free, condition, null) { Contract.Requires(condition != null); //:this(Token.NoToken, free, condition, null); } public Ensures(bool free, Expr condition, string comment) : this(Token.NoToken, free, condition, comment) { Contract.Requires(condition != null); //:this(Token.NoToken, free, condition, comment); } public void Emit(TokenTextWriter stream, int level) { Contract.Requires(stream != null); if (Comment != null) { stream.WriteLine(this, level, "// " + Comment); } stream.Write(this, level, "{0}ensures ", Free ? "free " : ""); Cmd.EmitAttributes(stream, Attributes); this.Condition.Emit(stream); stream.WriteLine(";"); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); this.Condition.Resolve(rc); } public override void Typecheck(TypecheckingContext tc) { this.Condition.Typecheck(tc); Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck if (!this.Condition.Type.Unify(Type.Bool)) { tc.Error(this, "postconditions must be of type bool"); } } public override Absy StdDispatch(StandardVisitor visitor) { return visitor.VisitEnsures(this); } } public class Procedure : DeclWithFormals { public List/*!*/ Requires; public List/*!*/ Modifies; public List/*!*/ Ensures; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Requires != null); Contract.Invariant(Modifies != null); Contract.Invariant(Ensures != null); Contract.Invariant(Summary != null); } // Abstract interpretation: Procedure-specific invariants... [Rep] public readonly ProcedureSummary/*!*/ Summary; public Procedure(IToken/*!*/ tok, string/*!*/ name, List/*!*/ typeParams, List/*!*/ inParams, List/*!*/ outParams, List/*!*/ requires, List/*!*/ modifies, List/*!*/ ensures) : this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(typeParams != null); Contract.Requires(inParams != null); Contract.Requires(outParams != null); Contract.Requires(requires != null); Contract.Requires(modifies != null); Contract.Requires(ensures != null); //:this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null); } public Procedure(IToken/*!*/ tok, string/*!*/ name, List/*!*/ typeParams, List/*!*/ inParams, List/*!*/ outParams, List/*!*/ @requires, List/*!*/ @modifies, List/*!*/ @ensures, QKeyValue kv ) : base(tok, name, typeParams, inParams, outParams) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(typeParams != null); Contract.Requires(inParams != null); Contract.Requires(outParams != null); Contract.Requires(@requires != null); Contract.Requires(@modifies != null); Contract.Requires(@ensures != null); this.Requires = @requires; this.Modifies = @modifies; this.Ensures = @ensures; this.Summary = new ProcedureSummary(); this.Attributes = kv; } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.Write(this, level, "procedure "); EmitAttributes(stream); stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); EmitSignature(stream, false); stream.WriteLine(";"); level++; foreach (Requires/*!*/ e in this.Requires) { Contract.Assert(e != null); e.Emit(stream, level); } if (this.Modifies.Count > 0) { stream.Write(level, "modifies "); this.Modifies.Emit(stream, false); stream.WriteLine(";"); } foreach (Ensures/*!*/ e in this.Ensures) { Contract.Assert(e != null); e.Emit(stream, level); } if (!CommandLineOptions.Clo.IntraproceduralInfer) { for (int s = 0; s < this.Summary.Count; s++) { ProcedureSummaryEntry/*!*/ entry = cce.NonNull(this.Summary[s]); stream.Write(level + 1, "// "); stream.WriteLine(); } } stream.WriteLine(); stream.WriteLine(); } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); rc.AddProcedure(this); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); rc.PushVarContext(); foreach (IdentifierExpr/*!*/ ide in Modifies) { Contract.Assert(ide != null); ide.Resolve(rc); } int previousTypeBinderState = rc.TypeBinderState; try { RegisterTypeParameters(rc); RegisterFormals(InParams, rc); ResolveFormals(InParams, rc); // "where" clauses of in-parameters are resolved without the out-parameters in scope foreach (Requires/*!*/ e in Requires) { Contract.Assert(e != null); e.Resolve(rc); } RegisterFormals(OutParams, rc); ResolveFormals(OutParams, rc); // "where" clauses of out-parameters are resolved with both in- and out-parametes in scope rc.StateMode = ResolutionContext.State.Two; foreach (Ensures/*!*/ e in Ensures) { Contract.Assert(e != null); e.Resolve(rc); } rc.StateMode = ResolutionContext.State.Single; ResolveAttributes(rc); Type.CheckBoundVariableOccurrences(TypeParameters, new List(InParams.Select(Item => Item.TypedIdent.Type).ToArray()), new List(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()), this.tok, "procedure arguments", rc); } finally { rc.TypeBinderState = previousTypeBinderState; } rc.PopVarContext(); SortTypeParams(); } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); base.Typecheck(tc); foreach (IdentifierExpr/*!*/ ide in Modifies) { Contract.Assert(ide != null); Contract.Assume(ide.Decl != null); if (!ide.Decl.IsMutable) { tc.Error(this, "modifies list contains constant: {0}", ide.Name); } ide.Typecheck(tc); } foreach (Requires/*!*/ e in Requires) { Contract.Assert(e != null); e.Typecheck(tc); } bool oldYields = tc.Yields; tc.Yields = QKeyValue.FindBoolAttribute(Attributes, "yields"); foreach (Ensures/*!*/ e in Ensures) { Contract.Assert(e != null); e.Typecheck(tc); } tc.Yields = oldYields; } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitProcedure(this); } } public class LoopProcedure : Procedure { public Implementation enclosingImpl; private Dictionary blockMap; private Dictionary blockLabelMap; public LoopProcedure(Implementation impl, Block header, List inputs, List outputs, List globalMods) : base(Token.NoToken, impl.Name + "_loop_" + header.ToString(), new List(), inputs, outputs, new List(), globalMods, new List()) { enclosingImpl = impl; } public void setBlockMap(Dictionary bm) { blockMap = bm; blockLabelMap = new Dictionary(); foreach (var kvp in bm) { blockLabelMap.Add(kvp.Key.Label, kvp.Value); } } public Block getBlock(string label) { if (blockLabelMap.ContainsKey(label)) return blockLabelMap[label]; return null; } } public class Implementation : DeclWithFormals { public List/*!*/ LocVars; [Rep] public StmtList StructuredStmts; [Rep] public List/*!*/ Blocks; public Procedure Proc; // Blocks before applying passification etc. // Both are used only when /inline is set. public List OriginalBlocks; public List OriginalLocVars; public readonly ISet AssertionChecksums = new HashSet(ChecksumComparer.Default); public sealed class ChecksumComparer : IEqualityComparer { static IEqualityComparer defaultComparer; public static IEqualityComparer Default { get { if (defaultComparer == null) { defaultComparer = new ChecksumComparer(); } return defaultComparer; } } public bool Equals(byte[] x, byte[] y) { if (x == null || y == null) { return x == y; } else { return x.SequenceEqual(y); } } public int GetHashCode(byte[] checksum) { if (checksum == null) { throw new ArgumentNullException("checksum"); } else { var result = 17; for (int i = 0; i < checksum.Length; i++) { result = result * 23 + checksum[i]; } return result; } } } public void AddAssertionChecksum(byte[] checksum) { Contract.Requires(checksum != null); if (AssertionChecksums != null) { AssertionChecksums.Add(checksum); } } public ISet AssertionChecksumsInCachedSnapshot { get; set; } public bool IsAssertionChecksumInCachedSnapshot(byte[] checksum) { Contract.Requires(AssertionChecksumsInCachedSnapshot != null); return AssertionChecksumsInCachedSnapshot.Contains(checksum); } public IList RecycledFailingAssertions { get; protected set; } public void AddRecycledFailingAssertion(AssertCmd assertion) { if (RecycledFailingAssertions == null) { RecycledFailingAssertions = new List(); } RecycledFailingAssertions.Add(assertion); } public Cmd ExplicitAssumptionAboutCachedPrecondition { get; set; } // Strongly connected components private StronglyConnectedComponents scc; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(LocVars != null); Contract.Invariant(cce.NonNullElements(Blocks)); Contract.Invariant(cce.NonNullElements(OriginalBlocks, true)); Contract.Invariant(cce.NonNullElements(scc, true)); } private bool BlockPredecessorsComputed; public bool StronglyConnectedComponentsComputed { get { return this.scc != null; } } public bool SkipVerification { get { bool verify = true; cce.NonNull(this.Proc).CheckBooleanAttribute("verify", ref verify); this.CheckBooleanAttribute("verify", ref verify); if (!verify) { return true; } if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert || CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assume) { Expr inl = this.FindExprAttribute("inline"); if (inl == null) inl = this.Proc.FindExprAttribute("inline"); if (inl != null && inl is LiteralExpr && ((LiteralExpr)inl).isBigNum && ((LiteralExpr)inl).asBigNum.Signum > 0) { return true; } } if (CommandLineOptions.Clo.StratifiedInlining > 0) { return !QKeyValue.FindBoolAttribute(Attributes, "entrypoint"); } return false; } } public string Id { get { var id = FindStringAttribute("id"); if (id == null) { id = Name + GetHashCode().ToString() + ":0"; } return id; } } public int Priority { get { int priority = 0; CheckIntAttribute("priority", ref priority); if (priority <= 0) { priority = 1; } return priority; } } public IDictionary ErrorChecksumToCachedError { get; private set; } public bool IsErrorChecksumInCachedSnapshot(byte[] checksum) { Contract.Requires(ErrorChecksumToCachedError != null); return ErrorChecksumToCachedError.ContainsKey(checksum); } public void SetErrorChecksumToCachedError(IEnumerable> errors) { Contract.Requires(errors != null); ErrorChecksumToCachedError = new Dictionary(ChecksumComparer.Default); foreach (var kv in errors) { ErrorChecksumToCachedError[kv.Item1] = kv.Item3; if (kv.Item2 != null) { ErrorChecksumToCachedError[kv.Item2] = null; } } } public bool HasCachedSnapshot { get { return ErrorChecksumToCachedError != null && AssertionChecksumsInCachedSnapshot != null; } } public bool AnyErrorsInCachedSnapshot { get { Contract.Requires(ErrorChecksumToCachedError != null); return ErrorChecksumToCachedError.Any(); } } IList injectedAssumptionVariables; public IList InjectedAssumptionVariables { get { return injectedAssumptionVariables != null ? injectedAssumptionVariables : new List(); } } IList doomedInjectedAssumptionVariables; public IList DoomedInjectedAssumptionVariables { get { return doomedInjectedAssumptionVariables != null ? doomedInjectedAssumptionVariables : new List(); } } public List RelevantInjectedAssumptionVariables(Dictionary incarnationMap) { return InjectedAssumptionVariables.Where(v => { Expr e; if (incarnationMap.TryGetValue(v, out e)) { var le = e as LiteralExpr; return le == null || !le.IsTrue; } else { return false; } }).ToList(); } public List RelevantDoomedInjectedAssumptionVariables(Dictionary incarnationMap) { return DoomedInjectedAssumptionVariables.Where(v => { Expr e; if (incarnationMap.TryGetValue(v, out e)) { var le = e as LiteralExpr; return le == null || !le.IsTrue; } else { return false; } }).ToList(); } public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary incarnationMap, out bool isTrue) { Contract.Requires(incarnationMap != null); var vars = RelevantInjectedAssumptionVariables(incarnationMap).Select(v => incarnationMap[v]).ToList(); isTrue = vars.Count == 0; return LiteralExpr.BinaryTreeAnd(vars); } public void InjectAssumptionVariable(LocalVariable variable, bool isDoomed = false) { LocVars.Add(variable); if (isDoomed) { if (doomedInjectedAssumptionVariables == null) { doomedInjectedAssumptionVariables = new List(); } doomedInjectedAssumptionVariables.Add(variable); } else { if (injectedAssumptionVariables == null) { injectedAssumptionVariables = new List(); } injectedAssumptionVariables.Add(variable); } } public Implementation(IToken tok, string name, List typeParams, List inParams, List outParams, List localVariables, [Captured] StmtList structuredStmts, QKeyValue kv) : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) { Contract.Requires(structuredStmts != null); Contract.Requires(localVariables != null); Contract.Requires(outParams != null); Contract.Requires(inParams != null); Contract.Requires(typeParams != null); Contract.Requires(name != null); Contract.Requires(tok != null); //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()); } public Implementation(IToken tok, string name, List typeParams, List inParams, List outParams, List localVariables, [Captured] StmtList structuredStmts) : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()) { Contract.Requires(structuredStmts != null); Contract.Requires(localVariables != null); Contract.Requires(outParams != null); Contract.Requires(inParams != null); Contract.Requires(typeParams != null); Contract.Requires(name != null); Contract.Requires(tok != null); //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, new Errors()); } public Implementation(IToken tok, string name, List typeParams, List inParams, List outParams, List localVariables, [Captured] StmtList structuredStmts, Errors errorHandler) : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler) { Contract.Requires(errorHandler != null); Contract.Requires(structuredStmts != null); Contract.Requires(localVariables != null); Contract.Requires(outParams != null); Contract.Requires(inParams != null); Contract.Requires(typeParams != null); Contract.Requires(name != null); Contract.Requires(tok != null); //:this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, null, errorHandler); } public Implementation(IToken/*!*/ tok, string/*!*/ name, List/*!*/ typeParams, List/*!*/ inParams, List/*!*/ outParams, List/*!*/ localVariables, [Captured] StmtList/*!*/ structuredStmts, QKeyValue kv, Errors/*!*/ errorHandler) : base(tok, name, typeParams, inParams, outParams) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(typeParams != null); Contract.Requires(inParams != null); Contract.Requires(outParams != null); Contract.Requires(localVariables != null); Contract.Requires(structuredStmts != null); Contract.Requires(errorHandler != null); LocVars = localVariables; StructuredStmts = structuredStmts; BigBlocksResolutionContext ctx = new BigBlocksResolutionContext(structuredStmts, errorHandler); Blocks = ctx.Blocks; BlockPredecessorsComputed = false; scc = null; Attributes = kv; } public Implementation(IToken tok, string name, List typeParams, List inParams, List outParams, List localVariables, [Captured] List block) : this(tok, name, typeParams, inParams, outParams, localVariables, block, null) { Contract.Requires(cce.NonNullElements(block)); Contract.Requires(localVariables != null); Contract.Requires(outParams != null); Contract.Requires(inParams != null); Contract.Requires(typeParams != null); Contract.Requires(name != null); Contract.Requires(tok != null); //:this(tok, name, typeParams, inParams, outParams, localVariables, block, null); } public Implementation(IToken/*!*/ tok, string/*!*/ name, List/*!*/ typeParams, List/*!*/ inParams, List/*!*/ outParams, List/*!*/ localVariables, [Captured] List/*!*/ blocks, QKeyValue kv) : base(tok, name, typeParams, inParams, outParams) { Contract.Requires(name != null); Contract.Requires(inParams != null); Contract.Requires(outParams != null); Contract.Requires(localVariables != null); Contract.Requires(cce.NonNullElements(blocks)); LocVars = localVariables; Blocks = blocks; BlockPredecessorsComputed = false; scc = null; Attributes = kv; } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.Write(this, level, "implementation "); EmitAttributes(stream); stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); EmitSignature(stream, false); stream.WriteLine(); stream.WriteLine(level, "{0}", '{'); foreach (Variable/*!*/ v in this.LocVars) { Contract.Assert(v != null); v.Emit(stream, level + 1); } if (this.StructuredStmts != null && !CommandLineOptions.Clo.PrintInstrumented && !CommandLineOptions.Clo.PrintInlined) { if (this.LocVars.Count > 0) { stream.WriteLine(); } if (CommandLineOptions.Clo.PrintUnstructured < 2) { if (CommandLineOptions.Clo.PrintUnstructured == 1) { stream.WriteLine(this, level + 1, "/*** structured program:"); } this.StructuredStmts.Emit(stream, level + 1); if (CommandLineOptions.Clo.PrintUnstructured == 1) { stream.WriteLine(level + 1, "**** end structured program */"); } } } if (this.StructuredStmts == null || 1 <= CommandLineOptions.Clo.PrintUnstructured || CommandLineOptions.Clo.PrintInstrumented || CommandLineOptions.Clo.PrintInlined) { foreach (Block b in this.Blocks) { b.Emit(stream, level + 1); } } stream.WriteLine(level, "{0}", '}'); stream.WriteLine(); stream.WriteLine(); } public override void Register(ResolutionContext rc) { //Contract.Requires(rc != null); // nothing to register } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); if (Proc != null) { // already resolved return; } DeclWithFormals dwf = rc.LookUpProcedure(cce.NonNull(this.Name)); Proc = dwf as Procedure; if (dwf == null) { rc.Error(this, "implementation given for undeclared procedure: {0}", this.Name); } else if (Proc == null) { rc.Error(this, "implementations given for function, not procedure: {0}", this.Name); } int previousTypeBinderState = rc.TypeBinderState; try { RegisterTypeParameters(rc); rc.PushVarContext(); RegisterFormals(InParams, rc); RegisterFormals(OutParams, rc); foreach (Variable/*!*/ v in LocVars) { Contract.Assert(v != null); v.Register(rc); v.Resolve(rc); } foreach (Variable/*!*/ v in LocVars) { Contract.Assert(v != null); v.ResolveWhere(rc); } rc.PushProcedureContext(); foreach (Block b in Blocks) { b.Register(rc); } ResolveAttributes(rc); rc.StateMode = ResolutionContext.State.Two; foreach (Block b in Blocks) { b.Resolve(rc); } rc.StateMode = ResolutionContext.State.Single; rc.PopProcedureContext(); rc.PopVarContext(); Type.CheckBoundVariableOccurrences(TypeParameters, new List(InParams.Select(Item => Item.TypedIdent.Type).ToArray()), new List(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()), this.tok, "implementation arguments", rc); } finally { rc.TypeBinderState = previousTypeBinderState; } SortTypeParams(); } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); base.Typecheck(tc); Contract.Assume(this.Proc != null); if (this.TypeParameters.Count != Proc.TypeParameters.Count) { tc.Error(this, "mismatched number of type parameters in procedure implementation: {0}", this.Name); } else { // if the numbers of type parameters are different, it is // difficult to compare the argument types MatchFormals(this.InParams, Proc.InParams, "in", tc); MatchFormals(this.OutParams, Proc.OutParams, "out", tc); } foreach (Variable/*!*/ v in LocVars) { Contract.Assert(v != null); v.Typecheck(tc); } List oldFrame = tc.Frame; bool oldYields = tc.Yields; tc.Frame = Proc.Modifies; tc.Yields = QKeyValue.FindBoolAttribute(Proc.Attributes, "yields"); foreach (Block b in Blocks) { b.Typecheck(tc); } Contract.Assert(tc.Frame == Proc.Modifies); tc.Frame = oldFrame; tc.Yields = oldYields; } void MatchFormals(List/*!*/ implFormals, List/*!*/ procFormals, string/*!*/ inout, TypecheckingContext/*!*/ tc) { Contract.Requires(implFormals != null); Contract.Requires(procFormals != null); Contract.Requires(inout != null); Contract.Requires(tc != null); if (implFormals.Count != procFormals.Count) { tc.Error(this, "mismatched number of {0}-parameters in procedure implementation: {1}", inout, this.Name); } else { // unify the type parameters so that types can be compared Contract.Assert(Proc != null); Contract.Assert(this.TypeParameters.Count == Proc.TypeParameters.Count); IDictionary/*!*/ subst1 = new Dictionary(); IDictionary/*!*/ subst2 = new Dictionary(); for (int i = 0; i < this.TypeParameters.Count; ++i) { TypeVariable/*!*/ newVar = new TypeVariable(Token.NoToken, Proc.TypeParameters[i].Name); Contract.Assert(newVar != null); subst1.Add(Proc.TypeParameters[i], newVar); subst2.Add(this.TypeParameters[i], newVar); } for (int i = 0; i < implFormals.Count; i++) { // the names of the formals are allowed to change from the proc to the impl // but types must be identical Type t = cce.NonNull((Variable)implFormals[i]).TypedIdent.Type.Substitute(subst2); Type u = cce.NonNull((Variable)procFormals[i]).TypedIdent.Type.Substitute(subst1); if (!t.Equals(u)) { string/*!*/ a = cce.NonNull((Variable)implFormals[i]).Name; Contract.Assert(a != null); string/*!*/ b = cce.NonNull((Variable)procFormals[i]).Name; Contract.Assert(b != null); string/*!*/ c; if (a == b) { c = a; } else { c = String.Format("{0} (named {1} in implementation)", b, a); } tc.Error(this, "mismatched type of {0}-parameter in implementation {1}: {2}", inout, this.Name, c); } } } } private Dictionary/*?*/ formalMap = null; public void ResetImplFormalMap() { this.formalMap = null; } public Dictionary/*!*/ GetImplFormalMap() { Contract.Ensures(Contract.Result>() != null); if (this.formalMap != null) return this.formalMap; else { Dictionary/*!*/ map = new Dictionary (InParams.Count + OutParams.Count); Contract.Assume(this.Proc != null); Contract.Assume(InParams.Count == Proc.InParams.Count); for (int i = 0; i < InParams.Count; i++) { Variable/*!*/ v = InParams[i]; Contract.Assert(v != null); IdentifierExpr ie = new IdentifierExpr(v.tok, v); Variable/*!*/ pv = Proc.InParams[i]; Contract.Assert(pv != null); map.Add(pv, ie); } System.Diagnostics.Debug.Assert(OutParams.Count == Proc.OutParams.Count); for (int i = 0; i < OutParams.Count; i++) { Variable/*!*/ v = cce.NonNull(OutParams[i]); IdentifierExpr ie = new IdentifierExpr(v.tok, v); Variable pv = cce.NonNull(Proc.OutParams[i]); map.Add(pv, ie); } this.formalMap = map; if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { Console.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name); using (TokenTextWriter stream = new TokenTextWriter("", Console.Out, /*setTokens=*/false, /*pretty=*/ false)) { foreach (var e in map) { Console.Write(" "); cce.NonNull((Variable/*!*/)e.Key).Emit(stream, 0); Console.Write(" --> "); cce.NonNull((Expr)e.Value).Emit(stream); Console.WriteLine(); } } } return map; } } /// /// Return a collection of blocks that are reachable from the block passed as a parameter. /// The block must be defined in the current implementation /// public ICollection GetConnectedComponents(Block startingBlock) { Contract.Requires(startingBlock != null); Contract.Ensures(cce.NonNullElements(Contract.Result>(), true)); Contract.Assert(this.Blocks.Contains(startingBlock)); if (!this.BlockPredecessorsComputed) ComputeStronglyConnectedComponents(); #if DEBUG_PRINT System.Console.WriteLine("* Strongly connected components * \n{0} \n ** ", scc); #endif foreach (ICollection component in cce.NonNull(this.scc)) { foreach (Block/*!*/ b in component) { Contract.Assert(b != null); if (b == startingBlock) // We found the compontent that owns the startingblock { return component; } } } { Contract.Assert(false); throw new cce.UnreachableException(); } // if we are here, it means that the block is not in one of the components. This is an error. } /// /// Compute the strongly connected compontents of the blocks in the implementation. /// As a side effect, it also computes the "predecessor" relation for the block in the implementation /// override public void ComputeStronglyConnectedComponents() { if (!this.BlockPredecessorsComputed) ComputePredecessorsForBlocks(); Adjacency next = new Adjacency(Successors); Adjacency prev = new Adjacency(Predecessors); this.scc = new StronglyConnectedComponents(this.Blocks, next, prev); scc.Compute(); foreach (Block/*!*/ block in this.Blocks) { Contract.Assert(block != null); block.Predecessors = new List(); } } /// /// Reset the abstract stated computed before /// override public void ResetAbstractInterpretationState() { foreach (Block/*!*/ b in this.Blocks) { Contract.Assert(b != null); b.ResetAbstractInterpretationState(); } } /// /// A private method used as delegate for the strongly connected components. /// It return, given a node, the set of its successors /// private IEnumerable/**//*!*/ Successors(Block node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); GotoCmd gotoCmd = node.TransferCmd as GotoCmd; if (gotoCmd != null) { // If it is a gotoCmd Contract.Assert(gotoCmd.labelTargets != null); return gotoCmd.labelTargets; } else { // otherwise must be a ReturnCmd Contract.Assert(node.TransferCmd is ReturnCmd); return new List(); } } /// /// A private method used as delegate for the strongly connected components. /// It return, given a node, the set of its predecessors /// private IEnumerable/**//*!*/ Predecessors(Block node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(this.BlockPredecessorsComputed); return node.Predecessors; } /// /// Compute the predecessor informations for the blocks /// public void ComputePredecessorsForBlocks() { foreach (Block b in this.Blocks) { b.Predecessors = new List(); } foreach (Block b in this.Blocks) { GotoCmd gtc = b.TransferCmd as GotoCmd; if (gtc != null) { Contract.Assert(gtc.labelTargets != null); foreach (Block/*!*/ dest in gtc.labelTargets) { Contract.Assert(dest != null); dest.Predecessors.Add(b); } } } this.BlockPredecessorsComputed = true; } public void PruneUnreachableBlocks() { ArrayList /*Block!*/ visitNext = new ArrayList /*Block!*/ (); List reachableBlocks = new List(); HashSet reachable = new HashSet(); // the set of elements in "reachableBlocks" visitNext.Add(this.Blocks[0]); while (visitNext.Count != 0) { Block b = cce.NonNull((Block)visitNext[visitNext.Count - 1]); visitNext.RemoveAt(visitNext.Count - 1); if (!reachable.Contains(b)) { reachableBlocks.Add(b); reachable.Add(b); if (b.TransferCmd is GotoCmd) { if (CommandLineOptions.Clo.PruneInfeasibleEdges) { foreach (Cmd/*!*/ s in b.Cmds) { Contract.Assert(s != null); if (s is PredicateCmd) { LiteralExpr e = ((PredicateCmd)s).Expr as LiteralExpr; if (e != null && e.IsFalse) { // This statement sequence will never reach the end, because of this "assume false" or "assert false". // Hence, it does not reach its successors. b.TransferCmd = new ReturnCmd(b.TransferCmd.tok); goto NEXT_BLOCK; } } } } // it seems that the goto statement at the end may be reached foreach (Block succ in cce.NonNull((GotoCmd)b.TransferCmd).labelTargets) { Contract.Assume(succ != null); visitNext.Add(succ); } } } NEXT_BLOCK: { } } this.Blocks = reachableBlocks; } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitImplementation(this); } public void FreshenCaptureStates() { // Assume commands with the "captureState" attribute allow model states to be // captured for error reporting. // Some program transformations, such as loop unrolling, duplicate parts of the // program, leading to "capture-state-assumes" being duplicated. This leads // to ambiguity when getting a state from the model. // This method replaces the key of every "captureState" attribute with something // unique int FreshCounter = 0; foreach(var b in Blocks) { List newCmds = new List(); for (int i = 0; i < b.Cmds.Count(); i++) { var a = b.Cmds[i] as AssumeCmd; if (a != null && (QKeyValue.FindStringAttribute(a.Attributes, "captureState") != null)) { string StateName = QKeyValue.FindStringAttribute(a.Attributes, "captureState"); newCmds.Add(new AssumeCmd(Token.NoToken, a.Expr, FreshenCaptureState(a.Attributes, FreshCounter))); FreshCounter++; } else { newCmds.Add(b.Cmds[i]); } } b.Cmds = newCmds; } } private QKeyValue FreshenCaptureState(QKeyValue Attributes, int FreshCounter) { // Returns attributes identical to Attributes, but: // - reversed (for ease of implementation; should not matter) // - with the value for "captureState" replaced by a fresh value Contract.Requires(QKeyValue.FindStringAttribute(Attributes, "captureState") != null); string FreshValue = QKeyValue.FindStringAttribute(Attributes, "captureState") + "$renamed$" + Name + "$" + FreshCounter; QKeyValue result = null; while (Attributes != null) { if (Attributes.Key.Equals("captureState")) { result = new QKeyValue(Token.NoToken, Attributes.Key, new List() { FreshValue }, result); } else { result = new QKeyValue(Token.NoToken, Attributes.Key, Attributes.Params, result); } Attributes = Attributes.Next; } return result; } } public class TypedIdent : Absy { public const string NoName = ""; private string/*!*/ _name; public string/*!*/ Name { get { Contract.Ensures(Contract.Result() != null); return this._name; } set { Contract.Requires(value != null); this._name = value; } } private Type/*!*/ _type; public Type/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return this._type; } set { Contract.Requires(value != null); this._type = value; } } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this._name != null); Contract.Invariant(this._type != null); } public Expr WhereExpr; // [NotDelayed] public TypedIdent(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type) : this(tok, name, type, null) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(type != null); Contract.Ensures(this.WhereExpr == null); //PM: needed to verify BoogiePropFactory.FreshBoundVariable //:this(tok, name, type, null); // here for aesthetic reasons } // [NotDelayed] public TypedIdent(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type, Expr whereExpr) : base(tok) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(type != null); Contract.Ensures(this.WhereExpr == whereExpr); this._name = name; this._type = type; this.WhereExpr = whereExpr; } public bool HasName { get { return this.Name != NoName; } } public void Emit(TokenTextWriter stream) { Contract.Requires(stream != null); stream.SetToken(this); stream.push(); if (this.Name != NoName) { stream.Write("{0}: ", TokenTextWriter.SanitizeIdentifier(this.Name)); } this.Type.Emit(stream); if (this.WhereExpr != null) { stream.sep(); stream.Write(" where "); this.WhereExpr.Emit(stream); } stream.pop(); } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); // NOTE: WhereExpr needs to be resolved by the caller, because the caller must provide a modified ResolutionContext this.Type = this.Type.ResolveType(rc); } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); // type variables can occur when working with polymorphic functions/procedures // if (!this.Type.IsClosed) // tc.Error(this, "free variables in type of an identifier: {0}", // this.Type.FreeVariables); if (this.WhereExpr != null) { this.WhereExpr.Typecheck(tc); Contract.Assert(this.WhereExpr.Type != null); // follows from postcondition of Expr.Typecheck if (!this.WhereExpr.Type.Unify(Type.Bool)) { tc.Error(this, "where clauses must be of type bool"); } } } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitTypedIdent(this); } } #region Helper methods for generic Sequences public static class TypeVariableSeqAlgorithms { public static void AppendWithoutDups(this List tvs, List s1) { Contract.Requires(s1 != null); for (int i = 0; i < s1.Count; i++) { TypeVariable/*!*/ next = s1[i]; Contract.Assert(next != null); if (!tvs.Contains(next)) tvs.Add(next); } } } public static class Emitter { public static void Emit(this List/*!*/ decls, TokenTextWriter stream) { Contract.Requires(stream != null); Contract.Requires(cce.NonNullElements(decls)); bool first = true; foreach (Declaration d in decls) { if (d == null) continue; if (first) { first = false; } else { stream.WriteLine(); } d.Emit(stream, 0); } } public static void Emit(this List ss, TokenTextWriter stream) { Contract.Requires(stream != null); string sep = ""; foreach (string/*!*/ s in ss) { Contract.Assert(s != null); stream.Write(sep); sep = ", "; stream.Write(s); } } public static void Emit(this IList ts, TokenTextWriter stream) { Contract.Requires(stream != null); string sep = ""; stream.push(); foreach (Expr/*!*/ e in ts) { Contract.Assert(e != null); stream.Write(sep); sep = ", "; stream.sep(); e.Emit(stream); } stream.pop(); } public static void Emit(this List ids, TokenTextWriter stream, bool printWhereComments) { Contract.Requires(stream != null); string sep = ""; foreach (IdentifierExpr/*!*/ e in ids) { Contract.Assert(e != null); stream.Write(sep); sep = ", "; e.Emit(stream); if (printWhereComments && e.Decl != null && e.Decl.TypedIdent.WhereExpr != null) { stream.Write(" /* where "); e.Decl.TypedIdent.WhereExpr.Emit(stream); stream.Write(" */"); } } } public static void Emit(this List vs, TokenTextWriter stream, bool emitAttributes) { Contract.Requires(stream != null); string sep = ""; stream.push(); foreach (Variable/*!*/ v in vs) { Contract.Assert(v != null); stream.Write(sep); sep = ", "; stream.sep(); v.EmitVitals(stream, 0, emitAttributes); } stream.pop(); } public static void Emit(this List tys, TokenTextWriter stream, string separator) { Contract.Requires(separator != null); Contract.Requires(stream != null); string sep = ""; foreach (Type/*!*/ v in tys) { Contract.Assert(v != null); stream.Write(sep); sep = separator; v.Emit(stream); } } public static void Emit(this List tvs, TokenTextWriter stream, string separator) { Contract.Requires(separator != null); Contract.Requires(stream != null); string sep = ""; foreach (TypeVariable/*!*/ v in tvs) { Contract.Assert(v != null); stream.Write(sep); sep = separator; v.Emit(stream); } } } #endregion #region Regular Expressions // a data structure to recover the "program structure" from the flow graph public abstract class RE : Cmd { public RE() : base(Token.NoToken) { } public override void AddAssignedVariables(List vars) { //Contract.Requires(vars != null); throw new NotImplementedException(); } } public class AtomicRE : RE { private Block/*!*/ _b; public Block b { get { Contract.Ensures(Contract.Result() != null); return this._b; } set { Contract.Requires(value != null); this._b = value; } } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this._b != null); } public AtomicRE(Block block) { Contract.Requires(block != null); this._b = block; } public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); b.Resolve(rc); } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); b.Typecheck(tc); } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); b.Emit(stream, level); } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitAtomicRE(this); } } public abstract class CompoundRE : RE { public override void Resolve(ResolutionContext rc) { //Contract.Requires(rc != null); return; } public override void Typecheck(TypecheckingContext tc) { //Contract.Requires(tc != null); return; } } public class Sequential : CompoundRE { private RE/*!*/ _first; public RE/*!*/ first { get { Contract.Ensures(Contract.Result() != null); return this._first; } set { Contract.Requires(value != null); this._first = value; } } private RE/*!*/ _second; public RE/*!*/ second { get { Contract.Ensures(Contract.Result() != null); return this._second; } set { Contract.Requires(value != null); this._second = value; } } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this._first != null); Contract.Invariant(this._second != null); } public Sequential(RE first, RE second) { Contract.Requires(first != null); Contract.Requires(second != null); this._first = first; this._second = second; } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.WriteLine(); stream.WriteLine("{0};", Indent(stream.UseForComputingChecksums ? 0 : level)); first.Emit(stream, level + 1); second.Emit(stream, level + 1); } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitSequential(this); } } public class Choice : CompoundRE { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(this._rs != null); } private List/*!*/ _rs; public List/*!*/ rs { //Rename this (and _rs) if possible get { Contract.Ensures(Contract.Result>() != null); return this._rs; } set { Contract.Requires(value != null); this._rs = value; } } public Choice(List operands) { Contract.Requires(operands != null); this._rs = operands; } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.WriteLine(); stream.WriteLine("{0}[]", Indent(stream.UseForComputingChecksums ? 0 : level)); foreach (RE/*!*/ r in rs) { Contract.Assert(r != null); r.Emit(stream, level + 1); } } public override Absy StdDispatch(StandardVisitor visitor) { //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitChoice(this); } } public class DAG2RE { public static RE Transform(Block b) { Contract.Requires(b != null); Contract.Ensures(Contract.Result() != null); TransferCmd tc = b.TransferCmd; if (tc is ReturnCmd) { return new AtomicRE(b); } else if (tc is GotoCmd) { GotoCmd/*!*/ g = (GotoCmd)tc; Contract.Assert(g != null); Contract.Assume(g.labelTargets != null); if (g.labelTargets.Count == 1) { return new Sequential(new AtomicRE(b), Transform(cce.NonNull(g.labelTargets[0]))); } else { List rs = new List(); foreach (Block/*!*/ target in g.labelTargets) { Contract.Assert(target != null); RE r = Transform(target); rs.Add(r); } RE second = new Choice(rs); return new Sequential(new AtomicRE(b), second); } } else { Contract.Assume(false); throw new cce.UnreachableException(); } } } #endregion // NOTE: This class is here for convenience, since this file's // classes are used pretty much everywhere. public class BoogieDebug { public static bool DoPrinting = false; public static void Write(string format, params object[] args) { Contract.Requires(args != null); Contract.Requires(format != null); if (DoPrinting) { Console.Error.Write(format, args); } } public static void WriteLine(string format, params object[] args) { Contract.Requires(args != null); Contract.Requires(format != null); if (DoPrinting) { Console.Error.WriteLine(format, args); } } public static void WriteLine() { if (DoPrinting) { Console.Error.WriteLine(); } } } }