From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Core/Absy.cs | 8985 ++++++++++++++++++++++++++------------------------- 1 file changed, 4529 insertions(+), 4456 deletions(-) (limited to 'Source/Core/Absy.cs') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index a1a54024..8a8558bf 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1,4456 +1,4529 @@ -//----------------------------------------------------------------------------- -// -// 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(); - } - } - } - - 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); - foreach (Block/*!*/ block in g.NaturalLoops(header, b)) - { - 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); - foreach(var bl in auxGotoCmd.labelTargets) { - bool found = false; - foreach(var n in g.NaturalLoops(header, source)) { //very expensive, can we do a contains? - if (bl == n) { //clarify: is this the right comparison? - found = true; - break; - } - } - if (!found) { - Block auxNewBlock = new Block(); - auxNewBlock.Label = ((Block)bl).Label; - 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); - } - - 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 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); - } - - // 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(); - } - } - } -} +//----------------------------------------------------------------------------- +// +// 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 readonly ISet NecessaryAssumes = new HashSet(); + + 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 (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g) + !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 readonly Variable OriginalVariable; + 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; + OriginalVariable = var; + } + + } + 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(); + } + } + } +} -- cgit v1.2.3