From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/AIFramework/Lattice.cs | 1918 ++++++++++++++++++++--------------------- 1 file changed, 959 insertions(+), 959 deletions(-) (limited to 'Source/AIFramework/Lattice.cs') diff --git a/Source/AIFramework/Lattice.cs b/Source/AIFramework/Lattice.cs index ab10be9a..1796f1f6 100644 --- a/Source/AIFramework/Lattice.cs +++ b/Source/AIFramework/Lattice.cs @@ -1,960 +1,960 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -namespace Microsoft.AbstractInterpretationFramework { - using System; - using System.Diagnostics.Contracts; - using System.Collections; - using G = System.Collections.Generic; - using System.Diagnostics; - using Microsoft.AbstractInterpretationFramework.Collections; - using Microsoft.Boogie; - +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework { + using System; + using System.Diagnostics.Contracts; + using System.Collections; + using G = System.Collections.Generic; + using System.Diagnostics; + using Microsoft.AbstractInterpretationFramework.Collections; + using Microsoft.Boogie; + using ArraySet = Microsoft.Boogie.GSet; - using IMutableSet = Microsoft.Boogie.GSet; - using HashSet = Microsoft.Boogie.GSet; - using ISet = Microsoft.Boogie.GSet; - using Set = Microsoft.Boogie.GSet; - - - /// - /// Specifies the operations (e.g., join) on a mathematical lattice that depend - /// only on the elements of the lattice. - /// - [ContractClass(typeof(MathematicalLatticeContracts))] - public abstract class MathematicalLattice { - #region Element - /// - /// An element of the lattice. This class should be derived from in any - /// implementation of MathematicalLattice. - /// - [ContractClass(typeof(ElementContracts))] - public abstract class Element : System.ICloneable { - /// - /// Print out a debug-useful representation of the internal data structure of the lattice element. - /// - public virtual void Dump(string/*!*/ msg) { - Contract.Requires(msg != null); - System.Console.WriteLine("Dump({0}) = {1}", msg, this); - } - - public abstract Element/*!*/ Clone(); - object/*!*/ System.ICloneable.Clone() { - return this.Clone(); - } - - public abstract G.ICollection/*!*/ FreeVariables(); - - } - [ContractClassFor(typeof(Element))] - public abstract class ElementContracts : Element { - public override Element Clone() { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - - } - - public override System.Collections.Generic.ICollection FreeVariables() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - Contract.Ensures(Contract.Result>().IsReadOnly); - throw new System.NotImplementedException(); - } - } - #endregion - - public abstract Element/*!*/ Top { - get; - } - public abstract Element/*!*/ Bottom { - get; - } - - public abstract bool IsTop(Element/*!*/ e); - public abstract bool IsBottom(Element/*!*/ e); - - /// - /// Returns true if a <= this. - /// - protected abstract bool AtMost(Element/*!*/ a, Element/*!*/ b); - /* The following cases are handled elsewhere and need not be considered in subclass. */ - // requires a.GetType() == b.GetType(); - // requires ! a.IsTop; - // requires ! a.IsBottom; - // requires ! b.IsTop; - // requires ! b.IsBottom; - - - protected Answer TrivialLowerThan(Element/*!*/ a, Element/*!*/ b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - if (a.GetType() != b.GetType()) { - throw new System.InvalidOperationException( - "operands to <= must be of same Element type" - ); - } - if (IsBottom(a)) { - return Answer.Yes; - } - if (IsTop(b)) { - return Answer.Yes; - } - if (IsTop(a)) { - return Answer.No; - } - if (IsBottom(b)) { - return Answer.No; - } - - return Answer.Maybe; - } - - // Is 'a' better information than 'b'? - // - public bool LowerThan(Element/*!*/ a, Element/*!*/ b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - Answer ans = TrivialLowerThan(a, b); - return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, b); - } - - // Is 'a' worse information than 'b'? - // - public bool HigherThan(Element/*!*/ a, Element/*!*/ b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - return LowerThan(b, a); - } - - // Are 'a' and 'b' equivalent? - // - public bool Equivalent(Element/*!*/ a, Element/*!*/ b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - return LowerThan(a, b) && LowerThan(b, a); - } - - public abstract Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b); - /* The following cases are handled elsewhere and need not be considered in subclass. */ - // requires a.GetType() == b.GetType(); - // requires ! a.IsTop; - // requires ! a.IsBottom; - // requires ! b.IsTop; - // requires ! b.IsBottom; - - - protected Element/*?*/ TrivialJoin(Element/*!*/ a, Element/*!*/ b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - if (a.GetType() != b.GetType()) { - throw new System.InvalidOperationException( - "operands to Join must be of same Lattice.Element type" - ); - } - if (IsTop(a)) { - return a; - } - if (IsTop(b)) { - return b; - } - if (IsBottom(a)) { - return b; - } - if (IsBottom(b)) { - return a; - } - - return null; - } - - public Element/*!*/ Join(Element/*!*/ a, Element/*!*/ b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - Element/*?*/ r = TrivialJoin(a, b); - return r != null ? r : NontrivialJoin(a, b); - } - - public abstract Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) - /* The following cases are handled elsewhere and need not be considered in subclass. */ - // requires a.GetType() == b.GetType(); - // requires ! a.IsTop; - // requires ! a.IsBottom; - // requires ! b.IsTop; - // requires ! b.IsBottom; - ; - - protected Element/*?*/ TrivialMeet(Element/*!*/ a, Element/*!*/ b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - if (a.GetType() != b.GetType()) { - throw new System.InvalidOperationException( - "operands to Meet must be of same Lattice.Element type" - ); - } - if (IsTop(a)) { - return b; - } - if (IsTop(b)) { - return a; - } - if (IsBottom(a)) { - return a; - } - if (IsBottom(b)) { - return b; - } - - return null; - } - - public Element/*!*/ Meet(Element/*!*/ a, Element/*!*/ b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - Element/*?*/ r = TrivialMeet(a, b); - return r != null ? r : NontrivialMeet(a, b); - } - - public abstract Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b); - - public virtual void Validate() { - Debug.Assert(IsTop(Top)); - Debug.Assert(IsBottom(Bottom)); - Debug.Assert(!IsBottom(Top)); - Debug.Assert(!IsTop(Bottom)); - - Debug.Assert(LowerThan(Top, Top)); - Debug.Assert(LowerThan(Bottom, Top)); - Debug.Assert(LowerThan(Bottom, Bottom)); - - Debug.Assert(IsTop(Join(Top, Top))); - Debug.Assert(IsBottom(Join(Bottom, Bottom))); - } - } - [ContractClassFor(typeof(MathematicalLattice))] - public abstract class MathematicalLatticeContracts : MathematicalLattice { - public override MathematicalLattice.Element Top { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - - public override MathematicalLattice.Element Bottom { - get { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - - public override bool IsTop(MathematicalLattice.Element e) { - Contract.Requires(e != null); - throw new NotImplementedException(); - } - - public override bool IsBottom(MathematicalLattice.Element e) { - Contract.Requires(e != null); - throw new NotImplementedException(); - } - - protected override bool AtMost(MathematicalLattice.Element a, MathematicalLattice.Element b) { - Contract.Requires(a != null); - Contract.Requires(b != null); - throw new NotImplementedException(); - } - - public override MathematicalLattice.Element NontrivialJoin(MathematicalLattice.Element a, MathematicalLattice.Element b) { - Contract.Requires(a != null); - Contract.Requires(b != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - - public override MathematicalLattice.Element NontrivialMeet(MathematicalLattice.Element a, MathematicalLattice.Element b) { - Contract.Requires(a != null); - Contract.Requires(b != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - - public override MathematicalLattice.Element Widen(MathematicalLattice.Element a, MathematicalLattice.Element b) { - Contract.Requires(a != null); - Contract.Requires(b != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - - - /// - /// Provides an abstract interface for the operations of a lattice specific - /// to abstract interpretation (i.e., that deals with the expression language). - /// - [ContractClass(typeof(LatticeContracts))] - public abstract class Lattice : MathematicalLattice { - internal readonly IValueExprFactory/*!*/ valueExprFactory; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(valueExprFactory != null); - } - - - public Lattice(IValueExprFactory/*!*/ valueExprFactory) { - Contract.Requires(valueExprFactory != null); - this.valueExprFactory = valueExprFactory; - // base(); - } - - #region Primitives that commands translate into - - public abstract Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable); - - public abstract Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName); - - public abstract Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr); - - #endregion - - - // TODO keep this? - // public Element! Eliminate(Element! e, VariableSeq! variables) - // { - // Lattice.Element result = e; - // foreach (IVariable var in variables) - // { - // result = this.Eliminate(result, var); - // } - // return result; - // } - - - //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - // Note! - // - // Concrete classes that implement Lattice must implement one of the AtMost - // overloads. We provide here a default implementation for one given a "real" - // implementation of the other. Otherwise, there will be an infinite loop! - //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - - protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) { - //Contract.Requires(b != null); - //Contract.Requires(a != null); - return AtMost(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map); - } - - protected virtual bool AtMost(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { - Contract.Requires(bToResult != null); - Contract.Requires(b != null); - Contract.Requires(aToResult != null); - Contract.Requires(a != null); - return AtMost(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult)); - } - - public bool LowerThan(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { - Contract.Requires(bToResult != null); - Contract.Requires(b != null); - Contract.Requires(aToResult != null); - Contract.Requires(a != null); - Answer ans = TrivialLowerThan(a, b); - return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, aToResult, b, bToResult); - } - - public bool HigherThan(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { - Contract.Requires(bToResult != null); - Contract.Requires(b != null); - Contract.Requires(aToResult != null); - Contract.Requires(a != null); - return LowerThan(b, bToResult, a, aToResult); - } - - - //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - // Note! - // - // Concrete classes that implement Lattice must implement one of the NontrivialJoin - // overloads. We provide here a default implementation for one given a "real" - // implementation of the other. Otherwise, there will be an infinite loop! - //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - - public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) { - //Contract.Requires(b != null); - //Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - return NontrivialJoin(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map); - } - - public virtual Element/*!*/ NontrivialJoin(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { - Contract.Requires(bToResult != null); - Contract.Requires(b != null); - Contract.Requires(aToResult != null); - Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - return NontrivialJoin(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult)); - } - - public Element/*!*/ Join(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { - Contract.Requires(bToResult != null); - Contract.Requires(b != null); - Contract.Requires(aToResult != null); - Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - Element/*?*/ r = TrivialJoin(a, b); - return r != null ? r : NontrivialJoin(a, aToResult, b, bToResult); - } - - - //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - // Note! - // - // Concrete classes that implement Lattice must implement one of the Widen - // overloads. We provide here a default implementation for one given a "real" - // implementation of the other. Otherwise, there will be an infinite loop! - //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - - public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) { - //Contract.Requires(b != null); - //Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - return Widen(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map); - } - - public virtual Element/*!*/ Widen(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { - Contract.Requires(bToResult != null); - Contract.Requires(b != null); - Contract.Requires(aToResult != null); - Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - return Widen(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult)); - } - - - - /// - /// A default implementation of the given - /// the appropriate expression factories by calling CheckPredicate. - /// - protected Answer DefaultCheckVariableDisequality(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valExprFactory, Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) { - Contract.Requires(propExprFactory != null); - Contract.Requires(valExprFactory != null); - Contract.Requires(e != null); - Contract.Requires(var1 != null); - Contract.Requires(var2 != null); - return this.CheckPredicate(e, propExprFactory.Not(valExprFactory.Eq(var1, var2))); - } - - private Element/*!*/ ApplyCombineNameMap(Element/*!*/ e, ICombineNameMap/*!*/ eToResult) { - Contract.Requires(eToResult != null); - Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - Element/*!*/ result = e; - - foreach (G.KeyValuePair*//*!*/> entry in eToResult.GetSourceToResult()) { - IVariable/*!*/ sourceName = entry.Key; - Contract.Assert(sourceName != null); - ISet/**//*!*/>/*!*/ emptyDictionary1 = new G.Dictionary*//*!*/>(); - private static readonly G.Dictionary/*!*/ emptyDictionary2 = new G.Dictionary(); - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Map != null); - Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary1) && Contract.ForAll(emptyDictionary1.Values, set =>/*cce.NonNullElements(set)*/set != null)); - Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary2)); - Contract.Invariant(indexMap != null); - Contract.Invariant(reverseIndexMap != null); - - } - - - public ISet/**//*?*/ GetResultNames(IVariable/*!*/ srcname) { - //Contract.Requires(srcname != null); - ArraySet a = new ArraySet(); - a.Add(srcname); - return a; - } - - public IVariable/*?*/ GetSourceName(IVariable/*!*/ resname) { - //Contract.Requires(resname != null); - return resname; - } - - //TODO: uncomment when works in compiler - //public G.IEnumerable*/!>> GetSourceToResult() - public IEnumerable/*!*/ GetSourceToResult() { - Contract.Ensures(Contract.Result() != null); - return emptyDictionary1; - } - - //public G.IEnumerable> GetResultToSource() - public IEnumerable/*!*/ GetResultToSource() { - Contract.Ensures(Contract.Result() != null); - return emptyDictionary2; - } - - private IdentityCombineNameMap() { - } - } - - #region Support for MultiLattice to uniquely number every subclass of Lattice - - - private static Hashtable/**//*!*/ indexMap = new Hashtable(); - private static Hashtable/**//*!*/ reverseIndexMap = new Hashtable(); - private static int globalCount = 0; - - protected virtual object/*!*/ UniqueId { - get { - Contract.Ensures(Contract.Result() != null); - return cce.NonNull(this.GetType()); - } - } - - public int Index { - get { - object unique = this.UniqueId; - if (indexMap.ContainsKey(unique)) { - object index = indexMap[unique]; - Contract.Assert(index != null); // this does nothing for nonnull analysis - if (index != null) { - return (int)index; - } - return 0; - } else { - int myIndex = globalCount++; - indexMap[unique] = myIndex; - reverseIndexMap[myIndex] = this; - return myIndex; - } - } - } - - public static Lattice GetGlobalLattice(int i) { - return reverseIndexMap[i] as Lattice; - } - #endregion - - public static bool LogSwitch = false; - /// - /// Returns the predicate that corresponds to the given lattice element. - /// - public abstract IExpr/*!*/ ToPredicate(Element/*!*/ e); - - /// - /// Allows the lattice to specify whether it understands a particular function symbol. - /// - /// The lattice is always allowed to return "true" even when it really can't do anything - /// with such functions; however, it is advantageous to say "false" when possible to - /// avoid being called to do certain things. - /// - /// The arguments to a function are provided for context so that the lattice can say - /// true or false for the same function symbol in different situations. For example, - /// a lattice may understand the multiplication of a variable and a constant but not - /// of two variables. The implementation of a lattice should not hold on to the - /// arguments. - /// - /// The function symbol. - /// The argument context. - /// True if it may understand f, false if it does not understand f. - public abstract bool Understands(IFunctionSymbol/*!*/ f, IList/**//*!*/ args); - - /// - /// Return an expression that is equivalent to the given expression that does not - /// contain the given variable according to the lattice element and queryable. - /// - /// The lattice element. - /// A queryable for asking addtional information. - /// The expression to find an equivalent expression. - /// The variable to eliminate. - /// The set of variables that can't be used in the resulting expression. - /// - /// An equivalent expression to without - /// or null if not possible. - /// - public abstract IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, Set/**//*!*/ prohibitedVars); - - /// - /// Answers a query about whether the given predicate holds given the lattice element. - /// - /// The lattice element. - /// The predicate. - /// Yes, No, or Maybe. - public abstract Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred); - - /// - /// Answers a disequality about two variables. The same information could be obtained - /// by asking CheckPredicate, but a different implementation may be simpler and more - /// efficient. - /// - /// The lattice element. - /// The first variable. - /// The second variable. - /// Yes, No, or Maybe. - public abstract Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2); - - public abstract string/*!*/ ToString(Element/*!*/ e); // for debugging - - } - [ContractClassFor(typeof(Lattice))] - abstract class LatticeContracts : Lattice { - public LatticeContracts() - : base(null) { - } - public override IExpr ToPredicate(MathematicalLattice.Element e) { - Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - public override bool Understands(IFunctionSymbol f, IList args) { - Contract.Requires(f != null); - Contract.Requires(args != null); - throw new NotImplementedException(); - } - public override IExpr EquivalentExpr(MathematicalLattice.Element e, IQueryable q, IExpr expr, IVariable var, Set prohibitedVars) { - Contract.Requires(e != null); - Contract.Requires(q != null); - Contract.Requires(expr != null); - Contract.Requires(var != null); - Contract.Requires(prohibitedVars != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - public override Answer CheckPredicate(MathematicalLattice.Element e, IExpr pred) { - Contract.Requires(e != null); - Contract.Requires(pred != null); - throw new NotImplementedException(); - } - public override Answer CheckVariableDisequality(MathematicalLattice.Element e, IVariable var1, IVariable var2) { - Contract.Requires(e != null); - Contract.Requires(var1 != null); - Contract.Requires(var2 != null); - throw new NotImplementedException(); - } - public override string ToString(Element e) { - Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - public override MathematicalLattice.Element Eliminate(MathematicalLattice.Element e, IVariable variable) { - Contract.Requires(e != null); - Contract.Requires(variable != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - public override MathematicalLattice.Element Rename(MathematicalLattice.Element e, IVariable oldName, IVariable newName) { - Contract.Requires(e != null); - Contract.Requires(oldName != null); - Contract.Requires(newName != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - public override MathematicalLattice.Element Constrain(MathematicalLattice.Element e, IExpr expr) { - Contract.Requires(e != null); - Contract.Requires(expr != null); - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - } - - /// - /// Defines the relation between names used in the respective input lattice elements to the - /// various combination operators (Join,Widen,Meet,AtMost) and the names that should be used - /// in the resulting lattice element. - /// - [ContractClass(typeof(ICombineNameMapContracts))] - public interface ICombineNameMap { - ISet/**//*?*/ GetResultNames(IVariable/*!*/ srcname); - IVariable/*?*/ GetSourceName(IVariable/*!*/ resname); - - //TODO: uncommet when works in compiler - //G.IEnumerable*/!>> GetSourceToResult(); - IEnumerable/*!*/ GetSourceToResult(); - //G.IEnumerable> GetResultToSource(); - IEnumerable/*!*/ GetResultToSource(); - } - [ContractClassFor(typeof(ICombineNameMap))] - public abstract class ICombineNameMapContracts : ICombineNameMap { - #region ICombineNameMap Members - - public Set GetResultNames(IVariable srcname) { - Contract.Requires(srcname != null); - throw new NotImplementedException(); - } - - public IVariable GetSourceName(IVariable resname) { - Contract.Requires(resname != null); - throw new NotImplementedException(); - } - - public IEnumerable GetSourceToResult() { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - - public IEnumerable GetResultToSource() { - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); - } - - #endregion - } - - /// - /// Provides statistics on the number of times an operation is performed - /// and forwards the real operations to the given lattice in the constructor. - /// - public class StatisticsLattice : Lattice { - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(lattice != null); - } - - readonly Lattice/*!*/ lattice; - int eliminateCount; - int renameCount; - int constrainCount; - int toPredicateCount; - int atMostCount; - int topCount; - int bottomCount; - int isTopCount; - int isBottomCount; - int joinCount; - int meetCount; - int widenCount; - int understandsCount; - int equivalentExprCount; - int checkPredicateCount; - int checkVariableDisequalityCount; - - public StatisticsLattice(Lattice/*!*/ lattice) - : base(lattice.valueExprFactory) { - Contract.Requires(lattice != null); - this.lattice = lattice; - // base(lattice.valueExprFactory); - } - - public override Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable) { - //Contract.Requires(variable != null); - //Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - eliminateCount++; - return lattice.Eliminate(e, variable); - } - - public override Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName) { - //Contract.Requires(newName != null); - //Contract.Requires(oldName != null); - //Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - renameCount++; - return lattice.Rename(e, oldName, newName); - } - - public override Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr) { - //Contract.Requires(expr != null); - //Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - constrainCount++; - return lattice.Constrain(e, expr); - } - - - public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) { - //Contract.Requires(args != null); - //Contract.Requires(f != null); - understandsCount++; - return lattice.Understands(f, args); - } - - - public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/**//*!*/ prohibitedVars) { - //Contract.Requires(prohibitedVars != null); - //Contract.Requires(var != null); - //Contract.Requires(expr != null); - //Contract.Requires(q != null); - //Contract.Requires(e != null); - equivalentExprCount++; - return lattice.EquivalentExpr(e, q, expr, var, prohibitedVars); - } - - - public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) { - //Contract.Requires(pred != null); - //Contract.Requires(e != null); - checkPredicateCount++; - return lattice.CheckPredicate(e, pred); - } - - - public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) { - //Contract.Requires(var2 != null); - //Contract.Requires(var1 != null); - //Contract.Requires(e != null); - checkVariableDisequalityCount++; - return lattice.CheckVariableDisequality(e, var1, var2); - } - - - - public override IExpr/*!*/ ToPredicate(Element/*!*/ e) { - //Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - toPredicateCount++; - return lattice.ToPredicate(e); - } - - public override string/*!*/ ToString(Element/*!*/ e) { - //Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - return lattice.ToString(e); - } - - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - return string.Format( - "StatisticsLattice: #Eliminate={0} #Rename={1} #Constrain={2} #ToPredicate={3} " + - "#Understands={4} #EquivalentExpr={5} #CheckPredicate={6} #CheckVariableDisequality={7} " + - "#AtMost={8} #Top={9} #Bottom={9} #IsTop={10} #IsBottom={11} " + - "#NonTrivialJoin={12} #NonTrivialMeet={13} #Widen={14}", - eliminateCount, renameCount, constrainCount, toPredicateCount, - understandsCount, equivalentExprCount, checkPredicateCount, checkVariableDisequalityCount, - atMostCount, topCount, bottomCount, isTopCount, isBottomCount, - joinCount, meetCount, widenCount); - } - - protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) { - //Contract.Requires(b != null); - //Contract.Requires(a != null); - atMostCount++; - return lattice.LowerThan(a, b); - } - - public override Element/*!*/ Top { - get { - Contract.Ensures(Contract.Result() != null); - topCount++; - return lattice.Top; - } - } - public override Element/*!*/ Bottom { - get { - Contract.Ensures(Contract.Result() != null); - bottomCount++; - return lattice.Bottom; - } - } - - public override bool IsTop(Element/*!*/ e) { - //Contract.Requires(e != null); - isTopCount++; - return lattice.IsTop(e); - } - - public override bool IsBottom(Element/*!*/ e) { - //Contract.Requires(e != null); - isBottomCount++; - return lattice.IsBottom(e); - } - - public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) { - //Contract.Requires(b != null); - //Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - joinCount++; - return lattice.NontrivialJoin(a, b); - } - - public override Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) { - //Contract.Requires(b != null); - //Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - meetCount++; - return lattice.NontrivialMeet(a, b); - } - - public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) { - //Contract.Requires(b != null); - //Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); - widenCount++; - return lattice.Widen(a, b); - } - - public override void Validate() { - base.Validate(); - lattice.Validate(); - } - - protected override object/*!*/ UniqueId { - get { - Contract.Ensures(Contract.Result() != null); - // use the base id, not the underlying-lattice id (is that the right thing to do?) - return base.UniqueId; - } - } - } - - - public sealed class LatticeQueryable : IQueryable { - private Lattice/*!*/ lattice; - private Lattice.Element/*!*/ element; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(lattice != null); - Contract.Invariant(element != null); - } - - - public LatticeQueryable(Lattice/*!*/ lattice, Lattice.Element/*!*/ element) { - Contract.Requires(element != null); - Contract.Requires(lattice != null); - this.lattice = lattice; - this.element = element; - // base(); - } - - public Answer CheckPredicate(IExpr/*!*/ pred) { - //Contract.Requires(pred != null); - return lattice.CheckPredicate(element, pred); - } - - public Answer CheckVariableDisequality(IVariable/*!*/ var1, IVariable/*!*/ var2) { - //Contract.Requires(var2 != null); - //Contract.Requires(var1 != null); - return lattice.CheckVariableDisequality(element, var1, var2); - } - } -} + using IMutableSet = Microsoft.Boogie.GSet; + using HashSet = Microsoft.Boogie.GSet; + using ISet = Microsoft.Boogie.GSet; + using Set = Microsoft.Boogie.GSet; + + + /// + /// Specifies the operations (e.g., join) on a mathematical lattice that depend + /// only on the elements of the lattice. + /// + [ContractClass(typeof(MathematicalLatticeContracts))] + public abstract class MathematicalLattice { + #region Element + /// + /// An element of the lattice. This class should be derived from in any + /// implementation of MathematicalLattice. + /// + [ContractClass(typeof(ElementContracts))] + public abstract class Element : System.ICloneable { + /// + /// Print out a debug-useful representation of the internal data structure of the lattice element. + /// + public virtual void Dump(string/*!*/ msg) { + Contract.Requires(msg != null); + System.Console.WriteLine("Dump({0}) = {1}", msg, this); + } + + public abstract Element/*!*/ Clone(); + object/*!*/ System.ICloneable.Clone() { + return this.Clone(); + } + + public abstract G.ICollection/*!*/ FreeVariables(); + + } + [ContractClassFor(typeof(Element))] + public abstract class ElementContracts : Element { + public override Element Clone() { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + + } + + public override System.Collections.Generic.ICollection FreeVariables() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(Contract.Result>().IsReadOnly); + throw new System.NotImplementedException(); + } + } + #endregion + + public abstract Element/*!*/ Top { + get; + } + public abstract Element/*!*/ Bottom { + get; + } + + public abstract bool IsTop(Element/*!*/ e); + public abstract bool IsBottom(Element/*!*/ e); + + /// + /// Returns true if a <= this. + /// + protected abstract bool AtMost(Element/*!*/ a, Element/*!*/ b); + /* The following cases are handled elsewhere and need not be considered in subclass. */ + // requires a.GetType() == b.GetType(); + // requires ! a.IsTop; + // requires ! a.IsBottom; + // requires ! b.IsTop; + // requires ! b.IsBottom; + + + protected Answer TrivialLowerThan(Element/*!*/ a, Element/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + if (a.GetType() != b.GetType()) { + throw new System.InvalidOperationException( + "operands to <= must be of same Element type" + ); + } + if (IsBottom(a)) { + return Answer.Yes; + } + if (IsTop(b)) { + return Answer.Yes; + } + if (IsTop(a)) { + return Answer.No; + } + if (IsBottom(b)) { + return Answer.No; + } + + return Answer.Maybe; + } + + // Is 'a' better information than 'b'? + // + public bool LowerThan(Element/*!*/ a, Element/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Answer ans = TrivialLowerThan(a, b); + return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, b); + } + + // Is 'a' worse information than 'b'? + // + public bool HigherThan(Element/*!*/ a, Element/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + return LowerThan(b, a); + } + + // Are 'a' and 'b' equivalent? + // + public bool Equivalent(Element/*!*/ a, Element/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + return LowerThan(a, b) && LowerThan(b, a); + } + + public abstract Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b); + /* The following cases are handled elsewhere and need not be considered in subclass. */ + // requires a.GetType() == b.GetType(); + // requires ! a.IsTop; + // requires ! a.IsBottom; + // requires ! b.IsTop; + // requires ! b.IsBottom; + + + protected Element/*?*/ TrivialJoin(Element/*!*/ a, Element/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + if (a.GetType() != b.GetType()) { + throw new System.InvalidOperationException( + "operands to Join must be of same Lattice.Element type" + ); + } + if (IsTop(a)) { + return a; + } + if (IsTop(b)) { + return b; + } + if (IsBottom(a)) { + return b; + } + if (IsBottom(b)) { + return a; + } + + return null; + } + + public Element/*!*/ Join(Element/*!*/ a, Element/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + Element/*?*/ r = TrivialJoin(a, b); + return r != null ? r : NontrivialJoin(a, b); + } + + public abstract Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) + /* The following cases are handled elsewhere and need not be considered in subclass. */ + // requires a.GetType() == b.GetType(); + // requires ! a.IsTop; + // requires ! a.IsBottom; + // requires ! b.IsTop; + // requires ! b.IsBottom; + ; + + protected Element/*?*/ TrivialMeet(Element/*!*/ a, Element/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + if (a.GetType() != b.GetType()) { + throw new System.InvalidOperationException( + "operands to Meet must be of same Lattice.Element type" + ); + } + if (IsTop(a)) { + return b; + } + if (IsTop(b)) { + return a; + } + if (IsBottom(a)) { + return a; + } + if (IsBottom(b)) { + return b; + } + + return null; + } + + public Element/*!*/ Meet(Element/*!*/ a, Element/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + Element/*?*/ r = TrivialMeet(a, b); + return r != null ? r : NontrivialMeet(a, b); + } + + public abstract Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b); + + public virtual void Validate() { + Debug.Assert(IsTop(Top)); + Debug.Assert(IsBottom(Bottom)); + Debug.Assert(!IsBottom(Top)); + Debug.Assert(!IsTop(Bottom)); + + Debug.Assert(LowerThan(Top, Top)); + Debug.Assert(LowerThan(Bottom, Top)); + Debug.Assert(LowerThan(Bottom, Bottom)); + + Debug.Assert(IsTop(Join(Top, Top))); + Debug.Assert(IsBottom(Join(Bottom, Bottom))); + } + } + [ContractClassFor(typeof(MathematicalLattice))] + public abstract class MathematicalLatticeContracts : MathematicalLattice { + public override MathematicalLattice.Element Top { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + public override MathematicalLattice.Element Bottom { + get { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + public override bool IsTop(MathematicalLattice.Element e) { + Contract.Requires(e != null); + throw new NotImplementedException(); + } + + public override bool IsBottom(MathematicalLattice.Element e) { + Contract.Requires(e != null); + throw new NotImplementedException(); + } + + protected override bool AtMost(MathematicalLattice.Element a, MathematicalLattice.Element b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + throw new NotImplementedException(); + } + + public override MathematicalLattice.Element NontrivialJoin(MathematicalLattice.Element a, MathematicalLattice.Element b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + + public override MathematicalLattice.Element NontrivialMeet(MathematicalLattice.Element a, MathematicalLattice.Element b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + + public override MathematicalLattice.Element Widen(MathematicalLattice.Element a, MathematicalLattice.Element b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + + /// + /// Provides an abstract interface for the operations of a lattice specific + /// to abstract interpretation (i.e., that deals with the expression language). + /// + [ContractClass(typeof(LatticeContracts))] + public abstract class Lattice : MathematicalLattice { + internal readonly IValueExprFactory/*!*/ valueExprFactory; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(valueExprFactory != null); + } + + + public Lattice(IValueExprFactory/*!*/ valueExprFactory) { + Contract.Requires(valueExprFactory != null); + this.valueExprFactory = valueExprFactory; + // base(); + } + + #region Primitives that commands translate into + + public abstract Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable); + + public abstract Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName); + + public abstract Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr); + + #endregion + + + // TODO keep this? + // public Element! Eliminate(Element! e, VariableSeq! variables) + // { + // Lattice.Element result = e; + // foreach (IVariable var in variables) + // { + // result = this.Eliminate(result, var); + // } + // return result; + // } + + + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // Note! + // + // Concrete classes that implement Lattice must implement one of the AtMost + // overloads. We provide here a default implementation for one given a "real" + // implementation of the other. Otherwise, there will be an infinite loop! + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + + protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires(b != null); + //Contract.Requires(a != null); + return AtMost(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map); + } + + protected virtual bool AtMost(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { + Contract.Requires(bToResult != null); + Contract.Requires(b != null); + Contract.Requires(aToResult != null); + Contract.Requires(a != null); + return AtMost(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult)); + } + + public bool LowerThan(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { + Contract.Requires(bToResult != null); + Contract.Requires(b != null); + Contract.Requires(aToResult != null); + Contract.Requires(a != null); + Answer ans = TrivialLowerThan(a, b); + return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, aToResult, b, bToResult); + } + + public bool HigherThan(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { + Contract.Requires(bToResult != null); + Contract.Requires(b != null); + Contract.Requires(aToResult != null); + Contract.Requires(a != null); + return LowerThan(b, bToResult, a, aToResult); + } + + + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // Note! + // + // Concrete classes that implement Lattice must implement one of the NontrivialJoin + // overloads. We provide here a default implementation for one given a "real" + // implementation of the other. Otherwise, there will be an infinite loop! + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + + public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires(b != null); + //Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + return NontrivialJoin(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map); + } + + public virtual Element/*!*/ NontrivialJoin(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { + Contract.Requires(bToResult != null); + Contract.Requires(b != null); + Contract.Requires(aToResult != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + return NontrivialJoin(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult)); + } + + public Element/*!*/ Join(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { + Contract.Requires(bToResult != null); + Contract.Requires(b != null); + Contract.Requires(aToResult != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + Element/*?*/ r = TrivialJoin(a, b); + return r != null ? r : NontrivialJoin(a, aToResult, b, bToResult); + } + + + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // Note! + // + // Concrete classes that implement Lattice must implement one of the Widen + // overloads. We provide here a default implementation for one given a "real" + // implementation of the other. Otherwise, there will be an infinite loop! + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + + public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires(b != null); + //Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + return Widen(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map); + } + + public virtual Element/*!*/ Widen(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) { + Contract.Requires(bToResult != null); + Contract.Requires(b != null); + Contract.Requires(aToResult != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + return Widen(ApplyCombineNameMap(a, aToResult), ApplyCombineNameMap(b, bToResult)); + } + + + + /// + /// A default implementation of the given + /// the appropriate expression factories by calling CheckPredicate. + /// + protected Answer DefaultCheckVariableDisequality(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valExprFactory, Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) { + Contract.Requires(propExprFactory != null); + Contract.Requires(valExprFactory != null); + Contract.Requires(e != null); + Contract.Requires(var1 != null); + Contract.Requires(var2 != null); + return this.CheckPredicate(e, propExprFactory.Not(valExprFactory.Eq(var1, var2))); + } + + private Element/*!*/ ApplyCombineNameMap(Element/*!*/ e, ICombineNameMap/*!*/ eToResult) { + Contract.Requires(eToResult != null); + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + Element/*!*/ result = e; + + foreach (G.KeyValuePair*//*!*/> entry in eToResult.GetSourceToResult()) { + IVariable/*!*/ sourceName = entry.Key; + Contract.Assert(sourceName != null); + ISet/**//*!*/>/*!*/ emptyDictionary1 = new G.Dictionary*//*!*/>(); + private static readonly G.Dictionary/*!*/ emptyDictionary2 = new G.Dictionary(); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Map != null); + Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary1) && Contract.ForAll(emptyDictionary1.Values, set =>/*cce.NonNullElements(set)*/set != null)); + Contract.Invariant(cce.NonNullDictionaryAndValues(emptyDictionary2)); + Contract.Invariant(indexMap != null); + Contract.Invariant(reverseIndexMap != null); + + } + + + public ISet/**//*?*/ GetResultNames(IVariable/*!*/ srcname) { + //Contract.Requires(srcname != null); + ArraySet a = new ArraySet(); + a.Add(srcname); + return a; + } + + public IVariable/*?*/ GetSourceName(IVariable/*!*/ resname) { + //Contract.Requires(resname != null); + return resname; + } + + //TODO: uncomment when works in compiler + //public G.IEnumerable*/!>> GetSourceToResult() + public IEnumerable/*!*/ GetSourceToResult() { + Contract.Ensures(Contract.Result() != null); + return emptyDictionary1; + } + + //public G.IEnumerable> GetResultToSource() + public IEnumerable/*!*/ GetResultToSource() { + Contract.Ensures(Contract.Result() != null); + return emptyDictionary2; + } + + private IdentityCombineNameMap() { + } + } + + #region Support for MultiLattice to uniquely number every subclass of Lattice + + + private static Hashtable/**//*!*/ indexMap = new Hashtable(); + private static Hashtable/**//*!*/ reverseIndexMap = new Hashtable(); + private static int globalCount = 0; + + protected virtual object/*!*/ UniqueId { + get { + Contract.Ensures(Contract.Result() != null); + return cce.NonNull(this.GetType()); + } + } + + public int Index { + get { + object unique = this.UniqueId; + if (indexMap.ContainsKey(unique)) { + object index = indexMap[unique]; + Contract.Assert(index != null); // this does nothing for nonnull analysis + if (index != null) { + return (int)index; + } + return 0; + } else { + int myIndex = globalCount++; + indexMap[unique] = myIndex; + reverseIndexMap[myIndex] = this; + return myIndex; + } + } + } + + public static Lattice GetGlobalLattice(int i) { + return reverseIndexMap[i] as Lattice; + } + #endregion + + public static bool LogSwitch = false; + /// + /// Returns the predicate that corresponds to the given lattice element. + /// + public abstract IExpr/*!*/ ToPredicate(Element/*!*/ e); + + /// + /// Allows the lattice to specify whether it understands a particular function symbol. + /// + /// The lattice is always allowed to return "true" even when it really can't do anything + /// with such functions; however, it is advantageous to say "false" when possible to + /// avoid being called to do certain things. + /// + /// The arguments to a function are provided for context so that the lattice can say + /// true or false for the same function symbol in different situations. For example, + /// a lattice may understand the multiplication of a variable and a constant but not + /// of two variables. The implementation of a lattice should not hold on to the + /// arguments. + /// + /// The function symbol. + /// The argument context. + /// True if it may understand f, false if it does not understand f. + public abstract bool Understands(IFunctionSymbol/*!*/ f, IList/**//*!*/ args); + + /// + /// Return an expression that is equivalent to the given expression that does not + /// contain the given variable according to the lattice element and queryable. + /// + /// The lattice element. + /// A queryable for asking addtional information. + /// The expression to find an equivalent expression. + /// The variable to eliminate. + /// The set of variables that can't be used in the resulting expression. + /// + /// An equivalent expression to without + /// or null if not possible. + /// + public abstract IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, Set/**//*!*/ prohibitedVars); + + /// + /// Answers a query about whether the given predicate holds given the lattice element. + /// + /// The lattice element. + /// The predicate. + /// Yes, No, or Maybe. + public abstract Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred); + + /// + /// Answers a disequality about two variables. The same information could be obtained + /// by asking CheckPredicate, but a different implementation may be simpler and more + /// efficient. + /// + /// The lattice element. + /// The first variable. + /// The second variable. + /// Yes, No, or Maybe. + public abstract Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2); + + public abstract string/*!*/ ToString(Element/*!*/ e); // for debugging + + } + [ContractClassFor(typeof(Lattice))] + abstract class LatticeContracts : Lattice { + public LatticeContracts() + : base(null) { + } + public override IExpr ToPredicate(MathematicalLattice.Element e) { + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + public override bool Understands(IFunctionSymbol f, IList args) { + Contract.Requires(f != null); + Contract.Requires(args != null); + throw new NotImplementedException(); + } + public override IExpr EquivalentExpr(MathematicalLattice.Element e, IQueryable q, IExpr expr, IVariable var, Set prohibitedVars) { + Contract.Requires(e != null); + Contract.Requires(q != null); + Contract.Requires(expr != null); + Contract.Requires(var != null); + Contract.Requires(prohibitedVars != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + public override Answer CheckPredicate(MathematicalLattice.Element e, IExpr pred) { + Contract.Requires(e != null); + Contract.Requires(pred != null); + throw new NotImplementedException(); + } + public override Answer CheckVariableDisequality(MathematicalLattice.Element e, IVariable var1, IVariable var2) { + Contract.Requires(e != null); + Contract.Requires(var1 != null); + Contract.Requires(var2 != null); + throw new NotImplementedException(); + } + public override string ToString(Element e) { + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + public override MathematicalLattice.Element Eliminate(MathematicalLattice.Element e, IVariable variable) { + Contract.Requires(e != null); + Contract.Requires(variable != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + public override MathematicalLattice.Element Rename(MathematicalLattice.Element e, IVariable oldName, IVariable newName) { + Contract.Requires(e != null); + Contract.Requires(oldName != null); + Contract.Requires(newName != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + public override MathematicalLattice.Element Constrain(MathematicalLattice.Element e, IExpr expr) { + Contract.Requires(e != null); + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } + + /// + /// Defines the relation between names used in the respective input lattice elements to the + /// various combination operators (Join,Widen,Meet,AtMost) and the names that should be used + /// in the resulting lattice element. + /// + [ContractClass(typeof(ICombineNameMapContracts))] + public interface ICombineNameMap { + ISet/**//*?*/ GetResultNames(IVariable/*!*/ srcname); + IVariable/*?*/ GetSourceName(IVariable/*!*/ resname); + + //TODO: uncommet when works in compiler + //G.IEnumerable*/!>> GetSourceToResult(); + IEnumerable/*!*/ GetSourceToResult(); + //G.IEnumerable> GetResultToSource(); + IEnumerable/*!*/ GetResultToSource(); + } + [ContractClassFor(typeof(ICombineNameMap))] + public abstract class ICombineNameMapContracts : ICombineNameMap { + #region ICombineNameMap Members + + public Set GetResultNames(IVariable srcname) { + Contract.Requires(srcname != null); + throw new NotImplementedException(); + } + + public IVariable GetSourceName(IVariable resname) { + Contract.Requires(resname != null); + throw new NotImplementedException(); + } + + public IEnumerable GetSourceToResult() { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + + public IEnumerable GetResultToSource() { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + + #endregion + } + + /// + /// Provides statistics on the number of times an operation is performed + /// and forwards the real operations to the given lattice in the constructor. + /// + public class StatisticsLattice : Lattice { + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(lattice != null); + } + + readonly Lattice/*!*/ lattice; + int eliminateCount; + int renameCount; + int constrainCount; + int toPredicateCount; + int atMostCount; + int topCount; + int bottomCount; + int isTopCount; + int isBottomCount; + int joinCount; + int meetCount; + int widenCount; + int understandsCount; + int equivalentExprCount; + int checkPredicateCount; + int checkVariableDisequalityCount; + + public StatisticsLattice(Lattice/*!*/ lattice) + : base(lattice.valueExprFactory) { + Contract.Requires(lattice != null); + this.lattice = lattice; + // base(lattice.valueExprFactory); + } + + public override Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable) { + //Contract.Requires(variable != null); + //Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + eliminateCount++; + return lattice.Eliminate(e, variable); + } + + public override Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName) { + //Contract.Requires(newName != null); + //Contract.Requires(oldName != null); + //Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + renameCount++; + return lattice.Rename(e, oldName, newName); + } + + public override Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr) { + //Contract.Requires(expr != null); + //Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + constrainCount++; + return lattice.Constrain(e, expr); + } + + + public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) { + //Contract.Requires(args != null); + //Contract.Requires(f != null); + understandsCount++; + return lattice.Understands(f, args); + } + + + public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/**//*!*/ prohibitedVars) { + //Contract.Requires(prohibitedVars != null); + //Contract.Requires(var != null); + //Contract.Requires(expr != null); + //Contract.Requires(q != null); + //Contract.Requires(e != null); + equivalentExprCount++; + return lattice.EquivalentExpr(e, q, expr, var, prohibitedVars); + } + + + public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) { + //Contract.Requires(pred != null); + //Contract.Requires(e != null); + checkPredicateCount++; + return lattice.CheckPredicate(e, pred); + } + + + public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) { + //Contract.Requires(var2 != null); + //Contract.Requires(var1 != null); + //Contract.Requires(e != null); + checkVariableDisequalityCount++; + return lattice.CheckVariableDisequality(e, var1, var2); + } + + + + public override IExpr/*!*/ ToPredicate(Element/*!*/ e) { + //Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + toPredicateCount++; + return lattice.ToPredicate(e); + } + + public override string/*!*/ ToString(Element/*!*/ e) { + //Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + return lattice.ToString(e); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + return string.Format( + "StatisticsLattice: #Eliminate={0} #Rename={1} #Constrain={2} #ToPredicate={3} " + + "#Understands={4} #EquivalentExpr={5} #CheckPredicate={6} #CheckVariableDisequality={7} " + + "#AtMost={8} #Top={9} #Bottom={9} #IsTop={10} #IsBottom={11} " + + "#NonTrivialJoin={12} #NonTrivialMeet={13} #Widen={14}", + eliminateCount, renameCount, constrainCount, toPredicateCount, + understandsCount, equivalentExprCount, checkPredicateCount, checkVariableDisequalityCount, + atMostCount, topCount, bottomCount, isTopCount, isBottomCount, + joinCount, meetCount, widenCount); + } + + protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires(b != null); + //Contract.Requires(a != null); + atMostCount++; + return lattice.LowerThan(a, b); + } + + public override Element/*!*/ Top { + get { + Contract.Ensures(Contract.Result() != null); + topCount++; + return lattice.Top; + } + } + public override Element/*!*/ Bottom { + get { + Contract.Ensures(Contract.Result() != null); + bottomCount++; + return lattice.Bottom; + } + } + + public override bool IsTop(Element/*!*/ e) { + //Contract.Requires(e != null); + isTopCount++; + return lattice.IsTop(e); + } + + public override bool IsBottom(Element/*!*/ e) { + //Contract.Requires(e != null); + isBottomCount++; + return lattice.IsBottom(e); + } + + public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires(b != null); + //Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + joinCount++; + return lattice.NontrivialJoin(a, b); + } + + public override Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires(b != null); + //Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + meetCount++; + return lattice.NontrivialMeet(a, b); + } + + public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires(b != null); + //Contract.Requires(a != null); + Contract.Ensures(Contract.Result() != null); + widenCount++; + return lattice.Widen(a, b); + } + + public override void Validate() { + base.Validate(); + lattice.Validate(); + } + + protected override object/*!*/ UniqueId { + get { + Contract.Ensures(Contract.Result() != null); + // use the base id, not the underlying-lattice id (is that the right thing to do?) + return base.UniqueId; + } + } + } + + + public sealed class LatticeQueryable : IQueryable { + private Lattice/*!*/ lattice; + private Lattice.Element/*!*/ element; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(lattice != null); + Contract.Invariant(element != null); + } + + + public LatticeQueryable(Lattice/*!*/ lattice, Lattice.Element/*!*/ element) { + Contract.Requires(element != null); + Contract.Requires(lattice != null); + this.lattice = lattice; + this.element = element; + // base(); + } + + public Answer CheckPredicate(IExpr/*!*/ pred) { + //Contract.Requires(pred != null); + return lattice.CheckPredicate(element, pred); + } + + public Answer CheckVariableDisequality(IVariable/*!*/ var1, IVariable/*!*/ var2) { + //Contract.Requires(var2 != null); + //Contract.Requires(var1 != null); + return lattice.CheckVariableDisequality(element, var1, var2); + } + } +} -- cgit v1.2.3