diff options
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 8985 |
1 files changed, 4529 insertions, 4456 deletions
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<CallSite>/*!*/ _returnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints
-
- public HashSet<CallSite>/*!*/ ReturnPoints {
- get {
- Contract.Ensures(Contract.Result<HashSet<CallSite>>() != 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<CallSite>();
- }
-
- } // class
-
- public class ProcedureSummary : ArrayList/*<ProcedureSummaryEntry>*/
- {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(
- !IsReadOnly && !IsFixedSize);
- }
-
- public new ProcedureSummaryEntry/*!*/ this[int i] {
- get {
- Contract.Requires(0 <= i && i < Count);
- Contract.Ensures(Contract.Result<ProcedureSummaryEntry>() != 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<object>;
-
- [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<IToken>() != 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);
-
- /// <summary>
- /// Requires the object to have been successfully resolved.
- /// </summary>
- /// <param name="tc"></param>
- [NeedsContracts]
- public abstract void Typecheck(TypecheckingContext/*!*/ tc);
- /// <summary>
- /// Intorduced this so the uniqueId is not the same on a cloned object.
- /// </summary>
- /// <param name="tc"></param>
- public virtual Absy Clone() {
- Contract.Ensures(Contract.Result<Absy>() != 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<Object>(this.InternalNumberedMetadata);
- }
-
- return result;
- }
-
- public virtual Absy StdDispatch(StandardVisitor visitor) {
- Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != 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<Object> 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();
-
- /// <summary>
- /// Gets the number of meta data objects associated with this instance
- /// </summary>
- /// <value>The numbered meta data count.</value>
- public int NumberedMetaDataCount
- {
- get { return InternalNumberedMetadata == null? 0: InternalNumberedMetadata.Count; }
- }
-
- /// <summary>
- /// Gets an IEnumerable over the numbered metadata associated
- /// with this instance.
- /// </summary>
- /// <value>
- /// The numbered meta data enumerable that looks like the Enumerable
- /// of a dictionary.
- /// </value>
- public IEnumerable<KeyValuePair<int, Object>> NumberedMetadata
- {
- get {
- if (InternalNumberedMetadata == null)
- return Enumerable.Empty<KeyValuePair<int,Object>>();
- else
- return InternalNumberedMetadata.Select((v, index) => new KeyValuePair<int, Object>(index, v));
- }
- }
-
- /// <summary>
- /// 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.
- /// </summary>
- /// <returns>The stored metadata of type T</returns>
- /// <param name="index">The index of the metadata</param>
- /// <typeparam name="T">The type of the metadata object required</typeparam>
- public T GetMetadata<T>(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<Object>();
- }
- }
- }
-
- /// <summary>
- /// Sets the metadata for this instace at a specified index.
- /// </summary>
- /// <param name="index">The index of the metadata</param>
- /// <param name="value">The value to set</param>
- /// <typeparam name="T">The type of value</typeparam>
- public void SetMetadata<T>(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<out TGet>
- {
- TGet ErrorData
- {
- get;
- }
- }
-
- public interface IPotentialErrorNode<out TGet, in TSet> : IPotentialErrorNode<TGet>
- {
- 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<Declaration>();
- }
-
- public void Emit(TokenTextWriter stream) {
- Contract.Requires(stream != null);
- stream.SetToken(this);
- this.topLevelDeclarations.Emit(stream);
- }
-
- public void ProcessDatatypeConstructors() {
- Dictionary<string, DatatypeConstructor> constructors = new Dictionary<string, DatatypeConstructor>();
- List<Declaration> prunedTopLevelDeclarations = new List<Declaration>();
- 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);
- }
- }
-
- /// <summary>
- /// Returns the number of name resolution errors.
- /// </summary>
- /// <returns></returns>
- 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<Declaration/*!*/>();
- 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<TypeCtorDecl>()) {
- if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
- d.Resolve(rc);
- }
-
- // collect type synonym declarations
- List<TypeSynonymDecl/*!*/>/*!*/ synonymDecls = new List<TypeSynonymDecl/*!*/>();
- foreach (var d in TopLevelDeclarations.OfType<TypeSynonymDecl>()) {
- 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<Declaration>();
- cloned.AddTopLevelDeclarations(topLevelDeclarations);
- return cloned;
- }
-
- [Rep]
- private List<Declaration/*!*/>/*!*/ topLevelDeclarations;
-
- public IEnumerable<Declaration> TopLevelDeclarations
- {
- get
- {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Declaration>>()));
- 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<Declaration> 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<Declaration> 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<string, Implementation> implementationsCache;
- public IEnumerable<Implementation> Implementations
- {
- get
- {
- if (implementationsCache != null)
- {
- return implementationsCache.Values;
- }
- var result = TopLevelDeclarations.OfType<Implementation>();
- 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<Axiom> axiomsCache;
- public IEnumerable<Axiom> Axioms
- {
- get
- {
- if (axiomsCache != null)
- {
- return axiomsCache;
- }
- var result = TopLevelDeclarations.OfType<Axiom>();
- if (topLevelDeclarationsAreFrozen)
- {
- axiomsCache = result.ToList();
- }
- return result;
- }
- }
-
- Dictionary<string, Procedure> proceduresCache;
- public IEnumerable<Procedure> Procedures
- {
- get
- {
- if (proceduresCache != null)
- {
- return proceduresCache.Values;
- }
- var result = TopLevelDeclarations.OfType<Procedure>();
- 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<string, Function> functionsCache;
- public IEnumerable<Function> Functions
- {
- get
- {
- if (functionsCache != null)
- {
- return functionsCache.Values;
- }
- var result = TopLevelDeclarations.OfType<Function>();
- 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<Variable> Variables
- {
- get
- {
- return TopLevelDeclarations.OfType<Variable>();
- }
- }
-
- public IEnumerable<Constant> Constants
- {
- get
- {
- return TopLevelDeclarations.OfType<Constant>();
- }
- }
-
- private IEnumerable<GlobalVariable/*!*/> globalVariablesCache = null;
- public List<GlobalVariable/*!*/>/*!*/ GlobalVariables
- {
- get
- {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<GlobalVariable>>()));
-
- if (globalVariablesCache == null)
- globalVariablesCache = TopLevelDeclarations.OfType<GlobalVariable>();
-
- return new List<GlobalVariable>(globalVariablesCache);
- }
- }
-
- public IEnumerable<Block> Blocks()
- {
- return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);
- }
-
- public void ComputeStronglyConnectedComponents() {
- foreach (var d in this.TopLevelDeclarations) {
- d.ComputeStronglyConnectedComponents();
- }
- }
-
- /// <summary>
- /// Reset the abstract stated computed before
- /// </summary>
- 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<Block/*!*/>/*!*/ g,
- List<Implementation/*!*/>/*!*/ loopImpls,
- Dictionary<string, Dictionary<string, Block>> 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<Block/*!*/, List<Variable>/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, List<Variable>/*!*/>();
- Dictionary<Block/*!*/, List<Variable>/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, List<Variable>/*!*/>();
- Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>();
- Dictionary<Block/*!*/, LoopProcedure/*!*/>/*!*/ loopHeaderToLoopProc = new Dictionary<Block/*!*/, LoopProcedure/*!*/>();
- Dictionary<Block/*!*/, CallCmd/*!*/>/*!*/ loopHeaderToCallCmd1 = new Dictionary<Block/*!*/, CallCmd/*!*/>();
- Dictionary<Block, CallCmd> loopHeaderToCallCmd2 = new Dictionary<Block, CallCmd>();
- Dictionary<Block, AssignCmd> loopHeaderToAssignCmd = new Dictionary<Block, AssignCmd>();
-
- foreach (Block/*!*/ header in g.Headers) {
- Contract.Assert(header != null);
- Contract.Assert(header != null);
- List<Variable> inputs = new List<Variable>();
- List<Variable> outputs = new List<Variable>();
- List<Expr> callInputs1 = new List<Expr>();
- List<IdentifierExpr> callOutputs1 = new List<IdentifierExpr>();
- List<Expr> callInputs2 = new List<Expr>();
- List<IdentifierExpr> callOutputs2 = new List<IdentifierExpr>();
- List<AssignLhs> lhss = new List<AssignLhs>();
- List<Expr> rhss = new List<Expr>();
- Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>(); // Variable -> IdentifierExpr
-
- List<Variable>/*!*/ targets = new List<Variable>();
- HashSet<Variable> footprint = new HashSet<Variable>();
-
- 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<IdentifierExpr>/*!*/ globalMods = new List<IdentifierExpr>();
- 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<Block, Block> newBlocksCreated = new Dictionary<Block, Block>();
-
- bool headRecursion = false; // testing an option to put recursive call before loop body
-
- IEnumerable<Block> sortedHeaders = g.SortHeadersByDominance();
- foreach (Block/*!*/ header in sortedHeaders)
- {
- Contract.Assert(header != null);
- LoopProcedure loopProc = loopHeaderToLoopProc[header];
- Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
- HashSet<string> dummyBlocks = new HashSet<string>();
-
- CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]); // fix me
- List<Variable> inputs = loopHeaderToInputs[header];
- List<Variable> 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<AssignLhs> lhsg = new List<AssignLhs>();
- List<IdentifierExpr>/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;
- foreach (IdentifierExpr gl in globalsMods)
- lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));
- List<Expr> rhsg = new List<Expr>();
- 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<Cmd> cmdSeq;
- if (headRecursion)
- cmdSeq = new List<Cmd>();
- else
- {
- CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone();
- addUniqueCallAttr(si_unique_loc, callCmd);
- si_unique_loc++;
- cmdSeq = new List<Cmd> { callCmd };
- }
-
- Block/*!*/ block1 = new Block(Token.NoToken, source.Label + "_dummy",
- new List<Cmd>{ 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<String>/*!*/ newLabels = new List<String>();
- List<Block>/*!*/ newTargets = new List<Block>();
- 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<Block/*!*/>/*!*/ blocks = new List<Block/*!*/>();
- Block exit = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
- GotoCmd cmd = new GotoCmd(Token.NoToken,
- new List<String> { cce.NonNull(blockMap[header]).Label, exit.Label },
- new List<Block> { blockMap[header], exit });
-
- if (detLoopExtract) //cutting the non-determinism
- cmd = new GotoCmd(Token.NoToken,
- new List<String> { cce.NonNull(blockMap[header]).Label },
- new List<Block> { blockMap[header] });
-
- Block entry;
- List<Cmd> initCmds = new List<Cmd>();
- 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<String> newLabels = new List<String>();
- List<Block> newTargets = new List<Block>();
- 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<TypeVariable>(), inputs, outputs, new List<Variable>(), 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<Cmd> { loopHeaderToCallCmd1[header] };
- header.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { lastIterBlockName }, new List<Block> { 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<object>();
- 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<string, Dictionary<string, Block>> fullMap, string procName, string blockName, Block block)
- {
- if (!fullMap.ContainsKey(procName))
- fullMap[procName] = new Dictionary<string, Block>();
- fullMap[procName][blockName] = block;
- }
-
- public static Graph<Implementation> BuildCallGraph(Program program) {
- Graph<Implementation> callGraph = new Graph<Implementation>();
- Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
- foreach (var proc in program.Procedures) {
- procToImpls[proc] = new HashSet<Implementation>();
- }
- 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<Block/*!*/>/*!*/ GraphFromImpl(Implementation impl) {
- Contract.Requires(impl != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().Nodes));
- Contract.Ensures(Contract.Result<Graph<Block>>() != null);
-
- Graph<Block/*!*/> g = new Graph<Block/*!*/>();
- 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<Block> ProcessLoops(Implementation impl) {
- while (true) {
- impl.PruneUnreachableBlocks();
- impl.ComputePredecessorsForBlocks();
- Graph<Block/*!*/>/*!*/ 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<Cmd> newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds);
- TransferCmd newTransferCmd;
- GotoCmd splitGotoCmd = splitCandidate.TransferCmd as GotoCmd;
- if (splitGotoCmd == null) {
- newTransferCmd = new ReturnCmd(splitCandidate.tok);
- }
- else {
- List<String> newLabelNames = new List<String>();
- newLabelNames.AddRange(splitGotoCmd.labelNames);
- List<Block> newLabelTargets = new List<Block>();
- 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<string, Dictionary<string, Block>> ExtractLoops()
- {
- HashSet<string> procsWithIrreducibleLoops = null;
- return ExtractLoops(out procsWithIrreducibleLoops);
- }
-
- public Dictionary<string, Dictionary<string, Block>> ExtractLoops(out HashSet<string> procsWithIrreducibleLoops)
- {
- procsWithIrreducibleLoops = new HashSet<string>();
- List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>();
- Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();
- foreach (var impl in this.Implementations)
- {
- if (impl.Blocks != null && impl.Blocks.Count > 0)
- {
- try
- {
- Graph<Block> 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<string, Block>();
- 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<string, Block>();
- 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<Absy>() != 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<object>(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);
- }
- }
-
- /// <summary>
- /// 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.
- /// </summary>
- 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;
- }
-
- /// <summary>
- /// Find and return the last occurrence of an attribute with the name "name", if any. If none, return null.
- /// </summary>
- 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<object/*!*/>(vals), Attributes);
- }
- }
-
- public abstract void Emit(TokenTextWriter/*!*/ stream, int level);
- public abstract void Register(ResolutionContext/*!*/ rc);
-
- /// <summary>
- /// Compute the strongly connected components of the declaration.
- /// By default, it does nothing
- /// </summary>
- public virtual void ComputeStronglyConnectedComponents() { /* Does nothing */
- }
-
- /// <summary>
- /// Reset the abstract stated computed before
- /// </summary>
- 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<Expr>() != 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<Function> functionDependencies;
-
- public ISet<Function> FunctionDependencies
- {
- get { return functionDependencies; }
- }
-
- public void AddFunctionDependency(Function function)
- {
- Contract.Requires(function != null);
-
- if (functionDependencies == null)
- {
- functionDependencies = new HashSet<Function>();
- }
- 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<Absy>() != 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<string>() != 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<string>() != 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<Absy>() != null);
- return visitor.VisitTypeCtorDecl(this);
- }
- }
-
- public class TypeSynonymDecl : NamedDeclaration {
- private List<TypeVariable>/*!*/ typeParameters;
-
- public List<TypeVariable> TypeParameters {
- get {
- Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
- return this.typeParameters;
- }
- set {
- Contract.Requires(value != null);
- this.typeParameters = value;
- }
- }
-
- private Type/*!*/ body;
-
- public Type Body {
- get {
- Contract.Ensures(Contract.Result<Type>() != 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<TypeVariable>/*!*/ 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<TypeVariable>/*!*/ 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<TypeSynonymDecl/*!*/>/*!*/ synonymDecls, ResolutionContext/*!*/ rc) {
- Contract.Requires(cce.NonNullElements(synonymDecls));
- Contract.Requires(rc != null);
- // then discover all dependencies between type synonyms
- IDictionary<TypeSynonymDecl/*!*/, List<TypeSynonymDecl/*!*/>/*!*/>/*!*/ deps =
- new Dictionary<TypeSynonymDecl/*!*/, List<TypeSynonymDecl/*!*/>/*!*/>();
- foreach (TypeSynonymDecl/*!*/ decl in synonymDecls) {
- Contract.Assert(decl != null);
- List<TypeSynonymDecl/*!*/>/*!*/ declDeps = new List<TypeSynonymDecl/*!*/>();
- FindDependencies(decl.Body, declDeps, rc);
- deps.Add(decl, declDeps);
- }
-
- List<TypeSynonymDecl/*!*/>/*!*/ resolved = new List<TypeSynonymDecl/*!*/>();
-
- 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<TypeSynonymDecl/*!*/>/*!*/ 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<Absy>() != null);
- return visitor.VisitTypeSynonymDecl(this);
- }
- }
-
- public abstract class Variable : NamedDeclaration {
- private TypedIdent/*!*/ typedIdent;
-
- public TypedIdent TypedIdent {
- get {
- Contract.Ensures(Contract.Result<TypedIdent>() != 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<ConstantParent/*!*/> 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<ConstantParent/*!*/> 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<ConstantParent>(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<Absy>() != 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<Absy>() != 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);
- }
-
- /// <summary>
- /// 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.
- /// </summary>
- public static List<Variable> StripWhereClauses(List<Variable> w) {
- Contract.Requires(w != null);
- Contract.Ensures(Contract.Result<List<Variable>>() != null);
- List<Variable> s = new List<Variable>();
- 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<Absy>() != 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<Absy>() != 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<Absy>() != null);
- return visitor.VisitBoundVariable(this);
- }
- }
-
- public abstract class DeclWithFormals : NamedDeclaration {
- public List<TypeVariable>/*!*/ TypeParameters;
-
- private /*readonly--except in StandardVisitor*/ List<Variable>/*!*/ inParams, outParams;
-
- public List<Variable>/*!*/ InParams {
- get {
- Contract.Ensures(Contract.Result<List<Variable>>() != null);
- return this.inParams;
- }
- set {
- Contract.Requires(value != null);
- this.inParams = value;
- }
- }
-
- public List<Variable>/*!*/ OutParams
- {
- get {
- Contract.Ensures(Contract.Result<List<Variable>>() != 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<TypeVariable> typeParams,
- List<Variable> inParams, List<Variable> 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<Function>();
- 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<Function>(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<Procedure> procedureDependencies;
-
- public ISet<Procedure> ProcedureDependencies
- {
- get { return procedureDependencies; }
- }
-
- public void AddProcedureDependency(Procedure procedure)
- {
- Contract.Requires(procedure != null);
-
- if (procedureDependencies == null)
- {
- procedureDependencies = new HashSet<Procedure>();
- }
- procedureDependencies.Add(procedure);
- }
-
- ISet<Function> functionDependencies;
-
- public ISet<Function> FunctionDependencies
- {
- get { return functionDependencies; }
- }
-
- public void AddFunctionDependency(Function function)
- {
- Contract.Requires(function != null);
-
- if (functionDependencies == null)
- {
- functionDependencies = new HashSet<Function>();
- }
- 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<Type>/*!*/ allTypes = new List<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray());
- Contract.Assert(allTypes != null);
- allTypes.AddRange(new List<Type>(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()));
- TypeParameters = Type.SortTypeParams(TypeParameters, allTypes, null);
- }
-
- /// <summary>
- /// 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.
- /// </summary>
- /// <param name="rc"></param>
- protected void RegisterFormals(List<Variable> 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);
- }
- }
-
- /// <summary>
- /// Resolves the where clauses (and attributes) of the formals.
- /// </summary>
- /// <param name="rc"></param>
- protected void ResolveFormals(List<Variable> 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<DatatypeSelector> 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<DatatypeSelector>();
- }
-
- public override void Resolve(ResolutionContext rc) {
- HashSet<string> selectorNames = new HashSet<string>();
- 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<Variable> { 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<Variable> { 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<Axiom> otherDefinitionAxioms;
- public IEnumerable<Axiom> OtherDefinitionAxioms
- {
- get
- {
- return otherDefinitionAxioms;
- }
- }
-
- public void AddOtherDefinitionAxiom(Axiom axiom)
- {
- Contract.Requires(axiom != null);
-
- if (otherDefinitionAxioms == null)
- {
- otherDefinitionAxioms = new List<Axiom>();
- }
- otherDefinitionAxioms.Add(axiom);
- }
-
- public bool doingExpansion;
-
- private bool neverTrigger;
- private bool neverTriggerComputed;
-
- public Function(IToken tok, string name, List<Variable> args, Variable result)
- : this(tok, name, new List<TypeVariable>(), args, result, null) {
- Contract.Requires(result != null);
- Contract.Requires(args != null);
- Contract.Requires(name != null);
- Contract.Requires(tok != null);
- //:this(tok, name, new List<TypeVariable>(), args, result, null);
- }
- public Function(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> 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<Variable> args, Variable result, string comment)
- : this(tok, name, new List<TypeVariable>(), args, result, comment) {
- Contract.Requires(result != null);
- Contract.Requires(args != null);
- Contract.Requires(name != null);
- Contract.Requires(tok != null);
- //:this(tok, name, new List<TypeVariable>(), args, result, comment);
- }
- public Function(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> args, Variable/*!*/ result, string comment)
- : base(tok, name, typeParams, args, new List<Variable> { 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<TypeVariable> typeParams, List<Variable> 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<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),
- new List<Type>(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<Absy>() != null);
- return visitor.VisitFunction(this);
- }
-
- public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null) {
- Contract.Requires(definition != null);
-
- List<Variable> dummies = new List<Variable>();
- List<Expr> callArgs = new List<Expr>();
- 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<TypeVariable>/*!*/ quantifiedTypeVars = new List<TypeVariable>();
- 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<Expr> { call }, null),
- def);
- }
- DefinitionAxiom = new Axiom(tok, def);
- return DefinitionAxiom;
- }
- }
-
- public class Macro : Function {
- public Macro(IToken tok, string name, List<Variable> args, Variable result)
- : base(tok, name, args, result) { }
- }
-
- public class Requires : Absy, IPotentialErrorNode<string, string> {
- public readonly bool Free;
-
- private Expr/*!*/ _condition;
-
- public Expr/*!*/ Condition {
- get {
- Contract.Ensures(Contract.Result<Expr>() != 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<string, string> {
- public readonly bool Free;
-
- private Expr/*!*/ _condition;
-
- public Expr/*!*/ Condition {
- get {
- Contract.Ensures(Contract.Result<Expr>() != 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>/*!*/ Requires;
- public List<IdentifierExpr>/*!*/ Modifies;
- public List<Ensures>/*!*/ 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<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams,
- List<Requires>/*!*/ requires, List<IdentifierExpr>/*!*/ modifies, List<Ensures>/*!*/ 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<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams,
- List<Requires>/*!*/ @requires, List<IdentifierExpr>/*!*/ @modifies, List<Ensures>/*!*/ @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<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),
- new List<Type>(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<Absy>() != null);
- return visitor.VisitProcedure(this);
- }
- }
-
- public class LoopProcedure : Procedure
- {
- public Implementation enclosingImpl;
- private Dictionary<Block, Block> blockMap;
- private Dictionary<string, Block> blockLabelMap;
-
- public LoopProcedure(Implementation impl, Block header,
- List<Variable> inputs, List<Variable> outputs, List<IdentifierExpr> globalMods)
- : base(Token.NoToken, impl.Name + "_loop_" + header.ToString(),
- new List<TypeVariable>(), inputs, outputs,
- new List<Requires>(), globalMods, new List<Ensures>())
- {
- enclosingImpl = impl;
- }
-
- public void setBlockMap(Dictionary<Block, Block> bm)
- {
- blockMap = bm;
- blockLabelMap = new Dictionary<string, Block>();
- 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<Variable>/*!*/ LocVars;
- [Rep]
- public StmtList StructuredStmts;
- [Rep]
- public List<Block/*!*/>/*!*/ Blocks;
- public Procedure Proc;
-
- // Blocks before applying passification etc.
- // Both are used only when /inline is set.
- public List<Block/*!*/> OriginalBlocks;
- public List<Variable> OriginalLocVars;
-
- public readonly ISet<byte[]> AssertionChecksums = new HashSet<byte[]>(ChecksumComparer.Default);
-
- public sealed class ChecksumComparer : IEqualityComparer<byte[]>
- {
- static IEqualityComparer<byte[]> defaultComparer;
- public static IEqualityComparer<byte[]> 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<byte[]> AssertionChecksumsInCachedSnapshot { get; set; }
-
- public bool IsAssertionChecksumInCachedSnapshot(byte[] checksum)
- {
- Contract.Requires(AssertionChecksumsInCachedSnapshot != null);
-
- return AssertionChecksumsInCachedSnapshot.Contains(checksum);
- }
-
- public IList<AssertCmd> RecycledFailingAssertions { get; protected set; }
-
- public void AddRecycledFailingAssertion(AssertCmd assertion)
- {
- if (RecycledFailingAssertions == null)
- {
- RecycledFailingAssertions = new List<AssertCmd>();
- }
- RecycledFailingAssertions.Add(assertion);
- }
-
- // Strongly connected components
- private StronglyConnectedComponents<Block/*!*/> 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<byte[], object> ErrorChecksumToCachedError { get; private set; }
-
- public bool IsErrorChecksumInCachedSnapshot(byte[] checksum)
- {
- Contract.Requires(ErrorChecksumToCachedError != null);
-
- return ErrorChecksumToCachedError.ContainsKey(checksum);
- }
-
- public void SetErrorChecksumToCachedError(IEnumerable<Tuple<byte[], byte[], object>> errors)
- {
- Contract.Requires(errors != null);
-
- ErrorChecksumToCachedError = new Dictionary<byte[], object>(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<LocalVariable> injectedAssumptionVariables;
- public IList<LocalVariable> InjectedAssumptionVariables
- {
- get
- {
- return injectedAssumptionVariables != null ? injectedAssumptionVariables : new List<LocalVariable>();
- }
- }
-
- IList<LocalVariable> doomedInjectedAssumptionVariables;
- public IList<LocalVariable> DoomedInjectedAssumptionVariables
- {
- get
- {
- return doomedInjectedAssumptionVariables != null ? doomedInjectedAssumptionVariables : new List<LocalVariable>();
- }
- }
-
- public List<LocalVariable> RelevantInjectedAssumptionVariables(Dictionary<Variable, Expr> 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<LocalVariable> RelevantDoomedInjectedAssumptionVariables(Dictionary<Variable, Expr> 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<Variable, Expr> 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<LocalVariable>();
- }
- doomedInjectedAssumptionVariables.Add(variable);
- }
- else
- {
- if (injectedAssumptionVariables == null)
- {
- injectedAssumptionVariables = new List<LocalVariable>();
- }
- injectedAssumptionVariables.Add(variable);
- }
- }
-
- public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> 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<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> 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<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> 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<TypeVariable>/*!*/ typeParams,
- List<Variable>/*!*/ inParams,
- List<Variable>/*!*/ outParams,
- List<Variable>/*!*/ 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<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] List<Block/*!*/> 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<TypeVariable>/*!*/ typeParams,
- List<Variable>/*!*/ inParams,
- List<Variable>/*!*/ outParams,
- List<Variable>/*!*/ localVariables,
- [Captured] List<Block/*!*/>/*!*/ 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<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),
- new List<Type>(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<IdentifierExpr> 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<Variable>/*!*/ implFormals, List<Variable>/*!*/ 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<TypeVariable/*!*/, Type/*!*/>/*!*/ subst1 =
- new Dictionary<TypeVariable/*!*/, Type/*!*/>();
- IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst2 =
- new Dictionary<TypeVariable/*!*/, Type/*!*/>();
-
- 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<Variable, Expr>/*?*/ formalMap = null;
- public void ResetImplFormalMap() {
- this.formalMap = null;
- }
- public Dictionary<Variable, Expr>/*!*/ GetImplFormalMap() {
- Contract.Ensures(Contract.Result<Dictionary<Variable, Expr>>() != null);
-
- if (this.formalMap != null)
- return this.formalMap;
- else {
- Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (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>", 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;
- }
- }
-
- /// <summary>
- /// Return a collection of blocks that are reachable from the block passed as a parameter.
- /// The block must be defined in the current implementation
- /// </summary>
- public ICollection<Block/*!*/> GetConnectedComponents(Block startingBlock) {
- Contract.Requires(startingBlock != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<Block>>(), 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<Block/*!*/> 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.
- }
-
- /// <summary>
- /// 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
- /// </summary>
- override public void ComputeStronglyConnectedComponents() {
- if (!this.BlockPredecessorsComputed)
- ComputePredecessorsForBlocks();
-
- Adjacency<Block/*!*/> next = new Adjacency<Block/*!*/>(Successors);
- Adjacency<Block/*!*/> prev = new Adjacency<Block/*!*/>(Predecessors);
-
- this.scc = new StronglyConnectedComponents<Block/*!*/>(this.Blocks, next, prev);
- scc.Compute();
-
-
- foreach (Block/*!*/ block in this.Blocks) {
- Contract.Assert(block != null);
- block.Predecessors = new List<Block>();
- }
-
- }
-
- /// <summary>
- /// Reset the abstract stated computed before
- /// </summary>
- override public void ResetAbstractInterpretationState() {
- foreach (Block/*!*/ b in this.Blocks) {
- Contract.Assert(b != null);
- b.ResetAbstractInterpretationState();
- }
- }
-
- /// <summary>
- /// A private method used as delegate for the strongly connected components.
- /// It return, given a node, the set of its successors
- /// </summary>
- private IEnumerable/*<Block!>*//*!*/ Successors(Block node) {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<IEnumerable>() != 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<Block/*!*/>();
- }
- }
-
- /// <summary>
- /// A private method used as delegate for the strongly connected components.
- /// It return, given a node, the set of its predecessors
- /// </summary>
- private IEnumerable/*<Block!>*//*!*/ Predecessors(Block node) {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<IEnumerable>() != null);
-
- Contract.Assert(this.BlockPredecessorsComputed);
-
- return node.Predecessors;
- }
-
- /// <summary>
- /// Compute the predecessor informations for the blocks
- /// </summary>
- public void ComputePredecessorsForBlocks() {
- foreach (Block b in this.Blocks) {
- b.Predecessors = new List<Block>();
- }
- 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<Block/*!*/> reachableBlocks = new List<Block/*!*/>();
- HashSet<Block> reachable = new HashSet<Block>(); // 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<Absy>() != 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<Cmd> newCmds = new List<Cmd>();
- 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<object>() { 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<string>() != null);
- return this._name;
- }
- set {
- Contract.Requires(value != null);
- this._name = value;
- }
- }
-
- private Type/*!*/ _type;
-
- public Type/*!*/ Type {
- get {
- Contract.Ensures(Contract.Result<Type>() != 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<Absy>() != null);
- return visitor.VisitTypedIdent(this);
- }
- }
-
- #region Helper methods for generic Sequences
-
- public static class TypeVariableSeqAlgorithms {
- public static void AppendWithoutDups(this List<TypeVariable> tvs, List<TypeVariable> 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<Declaration/*!*/>/*!*/ 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<String> 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<Expr> 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<IdentifierExpr> 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<Variable> 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<Type> 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<TypeVariable> 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<Variable> vars) {
- //Contract.Requires(vars != null);
- throw new NotImplementedException();
- }
- }
- public class AtomicRE : RE {
- private Block/*!*/ _b;
-
- public Block b
- {
- get
- {
- Contract.Ensures(Contract.Result<Block>() != 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<Absy>() != 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<RE>() != null);
- return this._first;
- }
- set {
- Contract.Requires(value != null);
- this._first = value;
- }
- }
-
- private RE/*!*/ _second;
-
- public RE/*!*/ second {
- get {
- Contract.Ensures(Contract.Result<RE>() != 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<Absy>() != null);
- return visitor.VisitSequential(this);
- }
- }
- public class Choice : CompoundRE {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(this._rs != null);
- }
-
- private List<RE>/*!*/ _rs;
-
- public List<RE>/*!*/ rs { //Rename this (and _rs) if possible
- get {
- Contract.Ensures(Contract.Result<List<RE>>() != null);
- return this._rs;
- }
- set {
- Contract.Requires(value != null);
- this._rs = value;
- }
- }
-
- public Choice(List<RE> 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<Absy>() != null);
- return visitor.VisitChoice(this);
- }
- }
- public class DAG2RE {
- public static RE Transform(Block b) {
- Contract.Requires(b != null);
- Contract.Ensures(Contract.Result<RE>() != 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<RE> rs = new List<RE>();
- 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<CallSite>/*!*/ _returnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints + + public HashSet<CallSite>/*!*/ ReturnPoints { + get { + Contract.Ensures(Contract.Result<HashSet<CallSite>>() != 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<CallSite>(); + } + + } // class + + public class ProcedureSummary : ArrayList/*<ProcedureSummaryEntry>*/ + { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant( + !IsReadOnly && !IsFixedSize); + } + + public new ProcedureSummaryEntry/*!*/ this[int i] { + get { + Contract.Requires(0 <= i && i < Count); + Contract.Ensures(Contract.Result<ProcedureSummaryEntry>() != 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<object>; + + [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<IToken>() != 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); + + /// <summary> + /// Requires the object to have been successfully resolved. + /// </summary> + /// <param name="tc"></param> + [NeedsContracts] + public abstract void Typecheck(TypecheckingContext/*!*/ tc); + /// <summary> + /// Intorduced this so the uniqueId is not the same on a cloned object. + /// </summary> + /// <param name="tc"></param> + public virtual Absy Clone() { + Contract.Ensures(Contract.Result<Absy>() != 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<Object>(this.InternalNumberedMetadata); + } + + return result; + } + + public virtual Absy StdDispatch(StandardVisitor visitor) { + Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result<Absy>() != 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<Object> 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(); + + /// <summary> + /// Gets the number of meta data objects associated with this instance + /// </summary> + /// <value>The numbered meta data count.</value> + public int NumberedMetaDataCount + { + get { return InternalNumberedMetadata == null? 0: InternalNumberedMetadata.Count; } + } + + /// <summary> + /// Gets an IEnumerable over the numbered metadata associated + /// with this instance. + /// </summary> + /// <value> + /// The numbered meta data enumerable that looks like the Enumerable + /// of a dictionary. + /// </value> + public IEnumerable<KeyValuePair<int, Object>> NumberedMetadata + { + get { + if (InternalNumberedMetadata == null) + return Enumerable.Empty<KeyValuePair<int,Object>>(); + else + return InternalNumberedMetadata.Select((v, index) => new KeyValuePair<int, Object>(index, v)); + } + } + + /// <summary> + /// 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. + /// </summary> + /// <returns>The stored metadata of type T</returns> + /// <param name="index">The index of the metadata</param> + /// <typeparam name="T">The type of the metadata object required</typeparam> + public T GetMetadata<T>(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<Object>(); + } + } + } + + /// <summary> + /// Sets the metadata for this instace at a specified index. + /// </summary> + /// <param name="index">The index of the metadata</param> + /// <param name="value">The value to set</param> + /// <typeparam name="T">The type of value</typeparam> + public void SetMetadata<T>(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<out TGet> + { + TGet ErrorData + { + get; + } + } + + public interface IPotentialErrorNode<out TGet, in TSet> : IPotentialErrorNode<TGet> + { + 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<Declaration>(); + } + + public void Emit(TokenTextWriter stream) { + Contract.Requires(stream != null); + stream.SetToken(this); + this.topLevelDeclarations.Emit(stream); + } + + public void ProcessDatatypeConstructors() { + Dictionary<string, DatatypeConstructor> constructors = new Dictionary<string, DatatypeConstructor>(); + List<Declaration> prunedTopLevelDeclarations = new List<Declaration>(); + 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); + } + } + + /// <summary> + /// Returns the number of name resolution errors. + /// </summary> + /// <returns></returns> + 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<Declaration/*!*/>(); + 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<TypeCtorDecl>()) { + if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) + d.Resolve(rc); + } + + // collect type synonym declarations + List<TypeSynonymDecl/*!*/>/*!*/ synonymDecls = new List<TypeSynonymDecl/*!*/>(); + foreach (var d in TopLevelDeclarations.OfType<TypeSynonymDecl>()) { + 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<Declaration>(); + cloned.AddTopLevelDeclarations(topLevelDeclarations); + return cloned; + } + + [Rep] + private List<Declaration/*!*/>/*!*/ topLevelDeclarations; + + public IEnumerable<Declaration> TopLevelDeclarations + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Declaration>>())); + 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<Declaration> 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<Declaration> 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<string, Implementation> implementationsCache; + public IEnumerable<Implementation> Implementations + { + get + { + if (implementationsCache != null) + { + return implementationsCache.Values; + } + var result = TopLevelDeclarations.OfType<Implementation>(); + 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<Axiom> axiomsCache; + public IEnumerable<Axiom> Axioms + { + get + { + if (axiomsCache != null) + { + return axiomsCache; + } + var result = TopLevelDeclarations.OfType<Axiom>(); + if (topLevelDeclarationsAreFrozen) + { + axiomsCache = result.ToList(); + } + return result; + } + } + + Dictionary<string, Procedure> proceduresCache; + public IEnumerable<Procedure> Procedures + { + get + { + if (proceduresCache != null) + { + return proceduresCache.Values; + } + var result = TopLevelDeclarations.OfType<Procedure>(); + 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<string, Function> functionsCache; + public IEnumerable<Function> Functions + { + get + { + if (functionsCache != null) + { + return functionsCache.Values; + } + var result = TopLevelDeclarations.OfType<Function>(); + 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<Variable> Variables + { + get + { + return TopLevelDeclarations.OfType<Variable>(); + } + } + + public IEnumerable<Constant> Constants + { + get + { + return TopLevelDeclarations.OfType<Constant>(); + } + } + + private IEnumerable<GlobalVariable/*!*/> globalVariablesCache = null; + public List<GlobalVariable/*!*/>/*!*/ GlobalVariables + { + get + { + Contract.Ensures(cce.NonNullElements(Contract.Result<List<GlobalVariable>>())); + + if (globalVariablesCache == null) + globalVariablesCache = TopLevelDeclarations.OfType<GlobalVariable>(); + + return new List<GlobalVariable>(globalVariablesCache); + } + } + + public readonly ISet<string> NecessaryAssumes = new HashSet<string>(); + + public IEnumerable<Block> Blocks() + { + return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); + } + + public void ComputeStronglyConnectedComponents() { + foreach (var d in this.TopLevelDeclarations) { + d.ComputeStronglyConnectedComponents(); + } + } + + /// <summary> + /// Reset the abstract stated computed before + /// </summary> + 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(); + } + } + } + + + /// <summary> + /// Finds blocks that break out of a loop in NaturalLoops(header, backEdgeNode) + /// </summary> + /// <param name="header"></param> + /// <param name="backEdgeNode"></param> + /// <returns></returns> + private HashSet<Block> GetBreakBlocksOfLoop(Block header, Block backEdgeNode, Graph<Block/*!*/>/*!*/ g) + { + Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option"); + var immSuccBlks = new HashSet<Block>(); + 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<Block> GetBlocksInAllNaturalLoops(Block header, Graph<Block/*!*/>/*!*/ g) + { + Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option"); + var allBlocksInNaturalLoops = new HashSet<Block>(); + 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<Block/*!*/>/*!*/ g, + List<Implementation/*!*/>/*!*/ loopImpls, + Dictionary<string, Dictionary<string, Block>> 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<Block/*!*/, List<Variable>/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, List<Variable>/*!*/>(); + Dictionary<Block/*!*/, List<Variable>/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, List<Variable>/*!*/>(); + Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>(); + Dictionary<Block/*!*/, LoopProcedure/*!*/>/*!*/ loopHeaderToLoopProc = new Dictionary<Block/*!*/, LoopProcedure/*!*/>(); + Dictionary<Block/*!*/, CallCmd/*!*/>/*!*/ loopHeaderToCallCmd1 = new Dictionary<Block/*!*/, CallCmd/*!*/>(); + Dictionary<Block, CallCmd> loopHeaderToCallCmd2 = new Dictionary<Block, CallCmd>(); + Dictionary<Block, AssignCmd> loopHeaderToAssignCmd = new Dictionary<Block, AssignCmd>(); + + foreach (Block/*!*/ header in g.Headers) { + Contract.Assert(header != null); + Contract.Assert(header != null); + List<Variable> inputs = new List<Variable>(); + List<Variable> outputs = new List<Variable>(); + List<Expr> callInputs1 = new List<Expr>(); + List<IdentifierExpr> callOutputs1 = new List<IdentifierExpr>(); + List<Expr> callInputs2 = new List<Expr>(); + List<IdentifierExpr> callOutputs2 = new List<IdentifierExpr>(); + List<AssignLhs> lhss = new List<AssignLhs>(); + List<Expr> rhss = new List<Expr>(); + Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>(); // Variable -> IdentifierExpr + + List<Variable>/*!*/ targets = new List<Variable>(); + HashSet<Variable> footprint = new HashSet<Variable>(); + + foreach (Block/*!*/ b in g.BackEdgeNodes(header)) + { + Contract.Assert(b != null); + HashSet<Block> immSuccBlks = new HashSet<Block>(); + 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<IdentifierExpr>/*!*/ globalMods = new List<IdentifierExpr>(); + 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<Block, Block> newBlocksCreated = new Dictionary<Block, Block>(); + + bool headRecursion = false; // testing an option to put recursive call before loop body + + IEnumerable<Block> sortedHeaders = g.SortHeadersByDominance(); + foreach (Block/*!*/ header in sortedHeaders) + { + Contract.Assert(header != null); + LoopProcedure loopProc = loopHeaderToLoopProc[header]; + Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>(); + HashSet<string> dummyBlocks = new HashSet<string>(); + + CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]); // fix me + List<Variable> inputs = loopHeaderToInputs[header]; + List<Variable> 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<AssignLhs> lhsg = new List<AssignLhs>(); + List<IdentifierExpr>/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies; + foreach (IdentifierExpr gl in globalsMods) + lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl)); + List<Expr> rhsg = new List<Expr>(); + 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<Cmd> cmdSeq; + if (headRecursion) + cmdSeq = new List<Cmd>(); + else + { + CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone(); + addUniqueCallAttr(si_unique_loc, callCmd); + si_unique_loc++; + cmdSeq = new List<Cmd> { callCmd }; + } + + Block/*!*/ block1 = new Block(Token.NoToken, source.Label + "_dummy", + new List<Cmd>{ 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<String>/*!*/ newLabels = new List<String>(); + List<Block>/*!*/ newTargets = new List<Block>(); + 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<Block/*!*/>/*!*/ blocks = new List<Block/*!*/>(); + Block exit = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken)); + GotoCmd cmd = new GotoCmd(Token.NoToken, + new List<String> { cce.NonNull(blockMap[header]).Label, exit.Label }, + new List<Block> { blockMap[header], exit }); + + if (detLoopExtract) //cutting the non-determinism + cmd = new GotoCmd(Token.NoToken, + new List<String> { cce.NonNull(blockMap[header]).Label }, + new List<Block> { blockMap[header] }); + + Block entry; + List<Cmd> initCmds = new List<Cmd>(); + 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<String> newLabels = new List<String>(); + List<Block> newTargets = new List<Block>(); + 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<TypeVariable>(), inputs, outputs, new List<Variable>(), 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<Cmd> { loopHeaderToCallCmd1[header] }; + header.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { lastIterBlockName }, new List<Block> { 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<object>(); + 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<string, Dictionary<string, Block>> fullMap, string procName, string blockName, Block block) + { + if (!fullMap.ContainsKey(procName)) + fullMap[procName] = new Dictionary<string, Block>(); + fullMap[procName][blockName] = block; + } + + public static Graph<Implementation> BuildCallGraph(Program program) { + Graph<Implementation> callGraph = new Graph<Implementation>(); + Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>(); + foreach (var proc in program.Procedures) { + procToImpls[proc] = new HashSet<Implementation>(); + } + 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<Block/*!*/>/*!*/ GraphFromImpl(Implementation impl) { + Contract.Requires(impl != null); + Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().Nodes)); + Contract.Ensures(Contract.Result<Graph<Block>>() != null); + + Graph<Block/*!*/> g = new Graph<Block/*!*/>(); + 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<Block> ProcessLoops(Implementation impl) { + while (true) { + impl.PruneUnreachableBlocks(); + impl.ComputePredecessorsForBlocks(); + Graph<Block/*!*/>/*!*/ 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<Cmd> newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds); + TransferCmd newTransferCmd; + GotoCmd splitGotoCmd = splitCandidate.TransferCmd as GotoCmd; + if (splitGotoCmd == null) { + newTransferCmd = new ReturnCmd(splitCandidate.tok); + } + else { + List<String> newLabelNames = new List<String>(); + newLabelNames.AddRange(splitGotoCmd.labelNames); + List<Block> newLabelTargets = new List<Block>(); + 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<string, Dictionary<string, Block>> ExtractLoops() + { + HashSet<string> procsWithIrreducibleLoops = null; + return ExtractLoops(out procsWithIrreducibleLoops); + } + + public Dictionary<string, Dictionary<string, Block>> ExtractLoops(out HashSet<string> procsWithIrreducibleLoops) + { + procsWithIrreducibleLoops = new HashSet<string>(); + List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>(); + Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>(); + foreach (var impl in this.Implementations) + { + if (impl.Blocks != null && impl.Blocks.Count > 0) + { + try + { + Graph<Block> 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<string, Block>(); + 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<string, Block>(); + 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<Absy>() != 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<object>(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); + } + } + + /// <summary> + /// 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. + /// </summary> + 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; + } + + /// <summary> + /// Find and return the last occurrence of an attribute with the name "name", if any. If none, return null. + /// </summary> + 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<object/*!*/>(vals), Attributes); + } + } + + public abstract void Emit(TokenTextWriter/*!*/ stream, int level); + public abstract void Register(ResolutionContext/*!*/ rc); + + /// <summary> + /// Compute the strongly connected components of the declaration. + /// By default, it does nothing + /// </summary> + public virtual void ComputeStronglyConnectedComponents() { /* Does nothing */ + } + + /// <summary> + /// Reset the abstract stated computed before + /// </summary> + 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<Expr>() != 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<Function> functionDependencies; + + public ISet<Function> FunctionDependencies + { + get { return functionDependencies; } + } + + public void AddFunctionDependency(Function function) + { + Contract.Requires(function != null); + + if (functionDependencies == null) + { + functionDependencies = new HashSet<Function>(); + } + 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<Absy>() != 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<string>() != 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<string>() != 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<Absy>() != null); + return visitor.VisitTypeCtorDecl(this); + } + } + + public class TypeSynonymDecl : NamedDeclaration { + private List<TypeVariable>/*!*/ typeParameters; + + public List<TypeVariable> TypeParameters { + get { + Contract.Ensures(Contract.Result<List<TypeVariable>>() != null); + return this.typeParameters; + } + set { + Contract.Requires(value != null); + this.typeParameters = value; + } + } + + private Type/*!*/ body; + + public Type Body { + get { + Contract.Ensures(Contract.Result<Type>() != 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<TypeVariable>/*!*/ 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<TypeVariable>/*!*/ 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<TypeSynonymDecl/*!*/>/*!*/ synonymDecls, ResolutionContext/*!*/ rc) { + Contract.Requires(cce.NonNullElements(synonymDecls)); + Contract.Requires(rc != null); + // then discover all dependencies between type synonyms + IDictionary<TypeSynonymDecl/*!*/, List<TypeSynonymDecl/*!*/>/*!*/>/*!*/ deps = + new Dictionary<TypeSynonymDecl/*!*/, List<TypeSynonymDecl/*!*/>/*!*/>(); + foreach (TypeSynonymDecl/*!*/ decl in synonymDecls) { + Contract.Assert(decl != null); + List<TypeSynonymDecl/*!*/>/*!*/ declDeps = new List<TypeSynonymDecl/*!*/>(); + FindDependencies(decl.Body, declDeps, rc); + deps.Add(decl, declDeps); + } + + List<TypeSynonymDecl/*!*/>/*!*/ resolved = new List<TypeSynonymDecl/*!*/>(); + + 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<TypeSynonymDecl/*!*/>/*!*/ 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<Absy>() != null); + return visitor.VisitTypeSynonymDecl(this); + } + } + + public abstract class Variable : NamedDeclaration { + private TypedIdent/*!*/ typedIdent; + + public TypedIdent TypedIdent { + get { + Contract.Ensures(Contract.Result<TypedIdent>() != 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<ConstantParent/*!*/> 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<ConstantParent/*!*/> 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<ConstantParent>(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<Absy>() != 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<Absy>() != 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); + } + + /// <summary> + /// 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. + /// </summary> + public static List<Variable> StripWhereClauses(List<Variable> w) { + Contract.Requires(w != null); + Contract.Ensures(Contract.Result<List<Variable>>() != null); + List<Variable> s = new List<Variable>(); + 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<Absy>() != 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<Absy>() != 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<Absy>() != null); + return visitor.VisitBoundVariable(this); + } + } + + public abstract class DeclWithFormals : NamedDeclaration { + public List<TypeVariable>/*!*/ TypeParameters; + + private /*readonly--except in StandardVisitor*/ List<Variable>/*!*/ inParams, outParams; + + public List<Variable>/*!*/ InParams { + get { + Contract.Ensures(Contract.Result<List<Variable>>() != null); + return this.inParams; + } + set { + Contract.Requires(value != null); + this.inParams = value; + } + } + + public List<Variable>/*!*/ OutParams + { + get { + Contract.Ensures(Contract.Result<List<Variable>>() != 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<TypeVariable> typeParams, + List<Variable> inParams, List<Variable> 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<Function>(); + 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<Function>(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<Procedure> procedureDependencies; + + public ISet<Procedure> ProcedureDependencies + { + get { return procedureDependencies; } + } + + public void AddProcedureDependency(Procedure procedure) + { + Contract.Requires(procedure != null); + + if (procedureDependencies == null) + { + procedureDependencies = new HashSet<Procedure>(); + } + procedureDependencies.Add(procedure); + } + + ISet<Function> functionDependencies; + + public ISet<Function> FunctionDependencies + { + get { return functionDependencies; } + } + + public void AddFunctionDependency(Function function) + { + Contract.Requires(function != null); + + if (functionDependencies == null) + { + functionDependencies = new HashSet<Function>(); + } + 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("<no file>", strWr, false, false)) + { + EmitSignature(tokTxtWr, this is Function); + sig = strWr.ToString(); + } + + using (var otherStrWr = new System.IO.StringWriter()) + using (var otherTokTxtWr = new TokenTextWriter("<no file>", 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<Type>/*!*/ allTypes = new List<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()); + Contract.Assert(allTypes != null); + allTypes.AddRange(new List<Type>(OutParams.Select(Item => Item.TypedIdent.Type).ToArray())); + TypeParameters = Type.SortTypeParams(TypeParameters, allTypes, null); + } + + /// <summary> + /// 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. + /// </summary> + /// <param name="rc"></param> + protected void RegisterFormals(List<Variable> 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); + } + } + + /// <summary> + /// Resolves the where clauses (and attributes) of the formals. + /// </summary> + /// <param name="rc"></param> + protected void ResolveFormals(List<Variable> 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<DatatypeSelector> 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<DatatypeSelector>(); + } + + public override void Resolve(ResolutionContext rc) { + HashSet<string> selectorNames = new HashSet<string>(); + 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<Variable> { 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<Variable> { 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<Axiom> otherDefinitionAxioms; + public IEnumerable<Axiom> OtherDefinitionAxioms + { + get + { + return otherDefinitionAxioms; + } + } + + public void AddOtherDefinitionAxiom(Axiom axiom) + { + Contract.Requires(axiom != null); + + if (otherDefinitionAxioms == null) + { + otherDefinitionAxioms = new List<Axiom>(); + } + otherDefinitionAxioms.Add(axiom); + } + + public bool doingExpansion; + + private bool neverTrigger; + private bool neverTriggerComputed; + + public string OriginalLambdaExprAsString; + + public Function(IToken tok, string name, List<Variable> args, Variable result) + : this(tok, name, new List<TypeVariable>(), args, result, null) { + Contract.Requires(result != null); + Contract.Requires(args != null); + Contract.Requires(name != null); + Contract.Requires(tok != null); + //:this(tok, name, new List<TypeVariable>(), args, result, null); + } + public Function(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> 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<Variable> args, Variable result, string comment) + : this(tok, name, new List<TypeVariable>(), args, result, comment) { + Contract.Requires(result != null); + Contract.Requires(args != null); + Contract.Requires(name != null); + Contract.Requires(tok != null); + //:this(tok, name, new List<TypeVariable>(), args, result, comment); + } + public Function(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> args, Variable/*!*/ result, string comment) + : base(tok, name, typeParams, args, new List<Variable> { 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<TypeVariable> typeParams, List<Variable> 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<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()), + new List<Type>(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<Absy>() != null); + return visitor.VisitFunction(this); + } + + public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null) { + Contract.Requires(definition != null); + + List<Variable> dummies = new List<Variable>(); + List<Expr> callArgs = new List<Expr>(); + 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<TypeVariable>/*!*/ quantifiedTypeVars = new List<TypeVariable>(); + 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<Expr> { call }, null), + def); + } + DefinitionAxiom = new Axiom(tok, def); + return DefinitionAxiom; + } + } + + public class Macro : Function { + public Macro(IToken tok, string name, List<Variable> args, Variable result) + : base(tok, name, args, result) { } + } + + public class Requires : Absy, IPotentialErrorNode<string, string> { + public readonly bool Free; + + private Expr/*!*/ _condition; + + public Expr/*!*/ Condition { + get { + Contract.Ensures(Contract.Result<Expr>() != 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<string, string> { + public readonly bool Free; + + private Expr/*!*/ _condition; + + public Expr/*!*/ Condition { + get { + Contract.Ensures(Contract.Result<Expr>() != 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>/*!*/ Requires; + public List<IdentifierExpr>/*!*/ Modifies; + public List<Ensures>/*!*/ 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<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams, + List<Requires>/*!*/ requires, List<IdentifierExpr>/*!*/ modifies, List<Ensures>/*!*/ 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<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ inParams, List<Variable>/*!*/ outParams, + List<Requires>/*!*/ @requires, List<IdentifierExpr>/*!*/ @modifies, List<Ensures>/*!*/ @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<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()), + new List<Type>(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<Absy>() != null); + return visitor.VisitProcedure(this); + } + } + + public class LoopProcedure : Procedure + { + public Implementation enclosingImpl; + private Dictionary<Block, Block> blockMap; + private Dictionary<string, Block> blockLabelMap; + + public LoopProcedure(Implementation impl, Block header, + List<Variable> inputs, List<Variable> outputs, List<IdentifierExpr> globalMods) + : base(Token.NoToken, impl.Name + "_loop_" + header.ToString(), + new List<TypeVariable>(), inputs, outputs, + new List<Requires>(), globalMods, new List<Ensures>()) + { + enclosingImpl = impl; + } + + public void setBlockMap(Dictionary<Block, Block> bm) + { + blockMap = bm; + blockLabelMap = new Dictionary<string, Block>(); + 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<Variable>/*!*/ LocVars; + [Rep] + public StmtList StructuredStmts; + [Rep] + public List<Block/*!*/>/*!*/ Blocks; + public Procedure Proc; + + // Blocks before applying passification etc. + // Both are used only when /inline is set. + public List<Block/*!*/> OriginalBlocks; + public List<Variable> OriginalLocVars; + + public readonly ISet<byte[]> AssertionChecksums = new HashSet<byte[]>(ChecksumComparer.Default); + + public sealed class ChecksumComparer : IEqualityComparer<byte[]> + { + static IEqualityComparer<byte[]> defaultComparer; + public static IEqualityComparer<byte[]> 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<byte[]> AssertionChecksumsInCachedSnapshot { get; set; } + + public bool IsAssertionChecksumInCachedSnapshot(byte[] checksum) + { + Contract.Requires(AssertionChecksumsInCachedSnapshot != null); + + return AssertionChecksumsInCachedSnapshot.Contains(checksum); + } + + public IList<AssertCmd> RecycledFailingAssertions { get; protected set; } + + public void AddRecycledFailingAssertion(AssertCmd assertion) + { + if (RecycledFailingAssertions == null) + { + RecycledFailingAssertions = new List<AssertCmd>(); + } + RecycledFailingAssertions.Add(assertion); + } + + public Cmd ExplicitAssumptionAboutCachedPrecondition { get; set; } + + // Strongly connected components + private StronglyConnectedComponents<Block/*!*/> 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<byte[], object> ErrorChecksumToCachedError { get; private set; } + + public bool IsErrorChecksumInCachedSnapshot(byte[] checksum) + { + Contract.Requires(ErrorChecksumToCachedError != null); + + return ErrorChecksumToCachedError.ContainsKey(checksum); + } + + public void SetErrorChecksumToCachedError(IEnumerable<Tuple<byte[], byte[], object>> errors) + { + Contract.Requires(errors != null); + + ErrorChecksumToCachedError = new Dictionary<byte[], object>(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<LocalVariable> injectedAssumptionVariables; + public IList<LocalVariable> InjectedAssumptionVariables + { + get + { + return injectedAssumptionVariables != null ? injectedAssumptionVariables : new List<LocalVariable>(); + } + } + + IList<LocalVariable> doomedInjectedAssumptionVariables; + public IList<LocalVariable> DoomedInjectedAssumptionVariables + { + get + { + return doomedInjectedAssumptionVariables != null ? doomedInjectedAssumptionVariables : new List<LocalVariable>(); + } + } + + public List<LocalVariable> RelevantInjectedAssumptionVariables(Dictionary<Variable, Expr> 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<LocalVariable> RelevantDoomedInjectedAssumptionVariables(Dictionary<Variable, Expr> 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<Variable, Expr> 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<LocalVariable>(); + } + doomedInjectedAssumptionVariables.Add(variable); + } + else + { + if (injectedAssumptionVariables == null) + { + injectedAssumptionVariables = new List<LocalVariable>(); + } + injectedAssumptionVariables.Add(variable); + } + } + + public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> 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<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> 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<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> 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<TypeVariable>/*!*/ typeParams, + List<Variable>/*!*/ inParams, + List<Variable>/*!*/ outParams, + List<Variable>/*!*/ 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<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] List<Block/*!*/> 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<TypeVariable>/*!*/ typeParams, + List<Variable>/*!*/ inParams, + List<Variable>/*!*/ outParams, + List<Variable>/*!*/ localVariables, + [Captured] List<Block/*!*/>/*!*/ 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<Type>(InParams.Select(Item => Item.TypedIdent.Type).ToArray()), + new List<Type>(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<IdentifierExpr> 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<Variable>/*!*/ implFormals, List<Variable>/*!*/ 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<TypeVariable/*!*/, Type/*!*/>/*!*/ subst1 = + new Dictionary<TypeVariable/*!*/, Type/*!*/>(); + IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst2 = + new Dictionary<TypeVariable/*!*/, Type/*!*/>(); + + 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<Variable, Expr>/*?*/ formalMap = null; + public void ResetImplFormalMap() { + this.formalMap = null; + } + public Dictionary<Variable, Expr>/*!*/ GetImplFormalMap() { + Contract.Ensures(Contract.Result<Dictionary<Variable, Expr>>() != null); + + if (this.formalMap != null) + return this.formalMap; + else { + Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (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>", 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; + } + } + + /// <summary> + /// Return a collection of blocks that are reachable from the block passed as a parameter. + /// The block must be defined in the current implementation + /// </summary> + public ICollection<Block/*!*/> GetConnectedComponents(Block startingBlock) { + Contract.Requires(startingBlock != null); + Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<Block>>(), 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<Block/*!*/> 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. + } + + /// <summary> + /// 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 + /// </summary> + override public void ComputeStronglyConnectedComponents() { + if (!this.BlockPredecessorsComputed) + ComputePredecessorsForBlocks(); + + Adjacency<Block/*!*/> next = new Adjacency<Block/*!*/>(Successors); + Adjacency<Block/*!*/> prev = new Adjacency<Block/*!*/>(Predecessors); + + this.scc = new StronglyConnectedComponents<Block/*!*/>(this.Blocks, next, prev); + scc.Compute(); + + + foreach (Block/*!*/ block in this.Blocks) { + Contract.Assert(block != null); + block.Predecessors = new List<Block>(); + } + + } + + /// <summary> + /// Reset the abstract stated computed before + /// </summary> + override public void ResetAbstractInterpretationState() { + foreach (Block/*!*/ b in this.Blocks) { + Contract.Assert(b != null); + b.ResetAbstractInterpretationState(); + } + } + + /// <summary> + /// A private method used as delegate for the strongly connected components. + /// It return, given a node, the set of its successors + /// </summary> + private IEnumerable/*<Block!>*//*!*/ Successors(Block node) { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result<IEnumerable>() != 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<Block/*!*/>(); + } + } + + /// <summary> + /// A private method used as delegate for the strongly connected components. + /// It return, given a node, the set of its predecessors + /// </summary> + private IEnumerable/*<Block!>*//*!*/ Predecessors(Block node) { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result<IEnumerable>() != null); + + Contract.Assert(this.BlockPredecessorsComputed); + + return node.Predecessors; + } + + /// <summary> + /// Compute the predecessor informations for the blocks + /// </summary> + public void ComputePredecessorsForBlocks() { + foreach (Block b in this.Blocks) { + b.Predecessors = new List<Block>(); + } + 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<Block/*!*/> reachableBlocks = new List<Block/*!*/>(); + HashSet<Block> reachable = new HashSet<Block>(); // 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<Absy>() != 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<Cmd> newCmds = new List<Cmd>(); + 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<object>() { 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<string>() != null); + return this._name; + } + set { + Contract.Requires(value != null); + this._name = value; + } + } + + private Type/*!*/ _type; + + public Type/*!*/ Type { + get { + Contract.Ensures(Contract.Result<Type>() != 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<Absy>() != null); + return visitor.VisitTypedIdent(this); + } + } + + #region Helper methods for generic Sequences + + public static class TypeVariableSeqAlgorithms { + public static void AppendWithoutDups(this List<TypeVariable> tvs, List<TypeVariable> 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<Declaration/*!*/>/*!*/ 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<String> 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<Expr> 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<IdentifierExpr> 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<Variable> 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<Type> 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<TypeVariable> 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<Variable> vars) { + //Contract.Requires(vars != null); + throw new NotImplementedException(); + } + } + public class AtomicRE : RE { + private Block/*!*/ _b; + + public Block b + { + get + { + Contract.Ensures(Contract.Result<Block>() != 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<Absy>() != 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<RE>() != null); + return this._first; + } + set { + Contract.Requires(value != null); + this._first = value; + } + } + + private RE/*!*/ _second; + + public RE/*!*/ second { + get { + Contract.Ensures(Contract.Result<RE>() != 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<Absy>() != null); + return visitor.VisitSequential(this); + } + } + public class Choice : CompoundRE { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(this._rs != null); + } + + private List<RE>/*!*/ _rs; + + public List<RE>/*!*/ rs { //Rename this (and _rs) if possible + get { + Contract.Ensures(Contract.Result<List<RE>>() != null); + return this._rs; + } + set { + Contract.Requires(value != null); + this._rs = value; + } + } + + public Choice(List<RE> 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<Absy>() != null); + return visitor.VisitChoice(this); + } + } + public class DAG2RE { + public static RE Transform(Block b) { + Contract.Requires(b != null); + Contract.Ensures(Contract.Result<RE>() != 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<RE> rs = new List<RE>(); + 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(); + } + } + } +} |