diff options
Diffstat (limited to 'Source/AIFramework/MultiLattice.cs')
| -rw-r--r-- | Source/AIFramework/MultiLattice.cs | 1294 |
1 files changed, 647 insertions, 647 deletions
diff --git a/Source/AIFramework/MultiLattice.cs b/Source/AIFramework/MultiLattice.cs index ba9aa752..4c9de5f0 100644 --- a/Source/AIFramework/MultiLattice.cs +++ b/Source/AIFramework/MultiLattice.cs @@ -1,647 +1,647 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework {
- using System.Diagnostics.Contracts;
- using System.Collections;
- using System.Collections.Generic;
- using System.Diagnostics;
- using Microsoft.AbstractInterpretationFramework.Collections;
-
- using Microsoft.Boogie;
-
- using ISet = Microsoft.Boogie.GSet<object>;
- using Set = Microsoft.Boogie.GSet<object>;
-
-
- /// <summary>
- /// The cartesian product lattice.
- /// </summary>
- public class MultiLattice : Lattice, IEnumerable {
- internal class Elt : Element {
- public /*MaybeNull*/Element[] elementPerLattice;
-
- public Elt(int domainCount, bool isBottom) {
- this.elementPerLattice = (domainCount == 0 && isBottom) ? null : new Element[domainCount];
- }
-
- private Elt(Elt/*!*/ other) {
- Contract.Requires(other != null);
- Element[] otherEPL = other.elementPerLattice;
- if (otherEPL != null) {
- Element[] newEPL = new Element[otherEPL.Length];
- for (int i = 0; i < newEPL.Length; i++) {
- newEPL[i] = (Element)(cce.NonNull(otherEPL[i])).Clone();
- }
- this.elementPerLattice = newEPL;
- }
- }
-
- public override Element/*!*/ Clone() {
- Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(this);
- }
-
- [Pure]
- public override string/*!*/ ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- // string s = "MultiLattice+Elt{";
- // string sep = "";
- // Element[] epl = this.elementPerLattice;
- // if (epl != null)
- // {
- // foreach (Element! e in epl)
- // {
- // s += sep + e.ToString();
- // sep = ", ";
- // }
- // }
- // return s + "}";
- if (elementPerLattice == null)
- return "";
- System.Text.StringBuilder buffer = new System.Text.StringBuilder();
- for (int i = 0; i < this.Count; i++) {
- if (i > 0)
- buffer.Append("; ");
- buffer.AppendFormat("{0}", elementPerLattice[i]);
- }
- return buffer.ToString();
- }
-
- public override void Dump(string/*!*/ msg) {
- //Contract.Requires(msg != null);
- System.Console.WriteLine("MultiLattice.Elt.Dump({0})", msg);
- Element[] epl = this.elementPerLattice;
- if (epl != null) {
- foreach (Element/*!*/ e in epl) {
- Contract.Assert(e != null);
- e.Dump(msg);
- }
- }
- }
-
- [Pure]
- public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
- Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
- List<IVariable/*!*/>/*!*/ list = new List<IVariable/*!*/>();
- for (int i = 0; i < this.Count; i++) {
- list.AddRange(cce.NonNull(this[i]).FreeVariables());
- }
- return cce.NonNull(list.AsReadOnly());
- }
-
- public static Elt/*!*/ Top(ArrayList/*<Lattice>*//*!*/ lattices) {
- Contract.Requires(lattices != null);
- Contract.Ensures(Contract.Result<Elt>() != null);
- Elt multiValue = new Elt(lattices.Count, false);
- for (int i = 0; i < lattices.Count; i++) {
- Lattice d = (Lattice/*!*/)cce.NonNull(lattices[i]);
- multiValue[d.Index] = d.Top;
- }
- Debug.Assert(multiValue.IsValid);
- return multiValue;
- }
-
-
- public static Elt/*!*/ Bottom(ArrayList/*<Lattice>*//*!*/ lattices) {
- Contract.Requires(lattices != null);
- Contract.Ensures(Contract.Result<Elt>() != null);
- Elt multiValue = new Elt(lattices.Count, true);
- for (int i = 0; i < lattices.Count; i++) {
- Lattice d = (Lattice/*!*/)cce.NonNull(lattices[i]);
- multiValue[d.Index] = d.Bottom;
- }
- Debug.Assert(multiValue.IsValid);
- return multiValue;
- }
-
- public bool IsValid {
- get {
- if (this.elementPerLattice == null) {
- return true; /*bottom*/
- }
-
- Element[] epl = this.elementPerLattice;
- for (int i = 0; i < epl.Length; i++) {
- if (epl[i] == null) {
- return false;
- }
- }
- return true;
- }
- }
-
- public int Count {
- get {
- return this.elementPerLattice == null ? 0 : this.elementPerLattice.Length;
- }
- }
-
- public bool Contains(int i) {
- return 0 <= i && i < this.Count;
- }
-
- public Element this[int i] // just syntactic sugar
- {
- get {
- Element[] epl = this.elementPerLattice;
- return epl == null ? null : epl[i];
- }
- set {
- Element[] epl = this.elementPerLattice;
- if (epl == null)
- return;
- epl[i] = value;
- }
- }
-
- } // class
-
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(lattices != null);
- Contract.Invariant(propExprFactory != null);
- }
-
- ArrayList/*<Lattice>*//*!*/ lattices = new ArrayList();
-
- private readonly IPropExprFactory/*!*/ propExprFactory;
-
-
- public MultiLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory)
- : base(valueExprFactory) {
- Contract.Requires(valueExprFactory != null);
- Contract.Requires(propExprFactory != null);
- this.propExprFactory = propExprFactory;
- // base(valueExprFactory);
- }
-
-
-
- public void AddLattice(Lattice lattice) {
- this.lattices.Add(lattice);
- }
-
- private Lattice/*!*/ SubLattice(int i) {
- Contract.Ensures(Contract.Result<Lattice>() != null);
- return (Lattice/*!*/)cce.NonNull(this.lattices[i]);
- }
-
-
- public override Element/*!*/ Top {
- get {
- Contract.Ensures(Contract.Result<Element>() != null);
- return Elt.Top(this.lattices);
- }
- }
-
- public override Element/*!*/ Bottom {
- get {
- Contract.Ensures(Contract.Result<Element>() != null);
- return Elt.Bottom(this.lattices);
- }
- }
-
-
-
-
- public override bool IsBottom(Element/*!*/ element) {
- //Contract.Requires(element != null);
- Elt e = (Elt)element;
- // The program is errorneous/nonterminating if any subdomain knows it is.
- //
- if (e.elementPerLattice == null) {
- return true;
- }
- for (int i = 0; i < e.Count; i++) {
- if (SubLattice(i).IsBottom(cce.NonNull(e[i]))) {
- return true;
- }
- }
- return false;
- }
-
- public override bool IsTop(Element/*!*/ element) {
- //Contract.Requires(element != null);
- Elt e = (Elt)element;
- if (e.elementPerLattice == null) {
- return false;
- }
- // The multidomain knows nothing about the program only if no subdomain
- // knows anything about it.
- //
- for (int i = 0; i < e.Count; i++) {
- if (!SubLattice(i).IsTop(cce.NonNull(e[i]))) {
- return false;
- }
- }
- return true;
- }
-
- protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) {
- //Contract.Requires(second != null);
- //Contract.Requires(first != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
-
- for (int i = 0; i < a.Count; i++) {
- Element thisElement = cce.NonNull(a[i]);
- Element thatElement = cce.NonNull(b[i]);
- if (thisElement.GetType() != thatElement.GetType()) {
- throw new System.InvalidOperationException(
- "AtMost called on MultiDomain objects with different lattices"
- );
- }
- if (!SubLattice(i).LowerThan(thisElement, thatElement)) {
- return false;
- }
- }
- return true;
- }
-
- protected override bool AtMost(Element/*!*/ first, ICombineNameMap/*!*/ firstToResult, Element/*!*/ second, ICombineNameMap/*!*/ secondToResult) {
- //Contract.Requires(secondToResult != null);
- //Contract.Requires(second != null);
- //Contract.Requires(firstToResult != null);
- //Contract.Requires(first != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
-
- for (int i = 0; i < a.Count; i++) {
- Element thisElement = cce.NonNull(a[i]);
- Element thatElement = cce.NonNull(b[i]);
- if (thisElement.GetType() != thatElement.GetType()) {
- throw new System.InvalidOperationException(
- "AtMost called on MultiDomain objects with different lattices"
- );
- }
- if (!SubLattice(i).LowerThan(thisElement, firstToResult, thatElement, secondToResult)) {
- return false;
- }
- }
- return true;
- }
-
-
- private enum CombineOp {
- Meet,
- Join,
- Widen
- }
-
- private Element/*!*/ Combine(Element/*!*/ first, ICombineNameMap/*?*/ firstToResult, Element/*!*/ second, ICombineNameMap/*?*/ secondToResult, CombineOp c) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
-
- int unionCount = System.Math.Max(a.Count, b.Count);
- Elt combined = new Elt(unionCount, IsBottom(a) && IsBottom(b));
- for (int i = 0; i < unionCount; i++) {
- bool thisExists = a.Contains(i);
- bool thatExists = b.Contains(i);
-
- if (thisExists && thatExists) {
- Lattice.Element suba = a[i];
- Lattice.Element subb = b[i];
- Contract.Assert(suba != null && subb != null);
-
- switch (c) {
- case CombineOp.Meet:
- combined[i] = SubLattice(i).Meet(suba, subb);
- break;
- case CombineOp.Join:
- if (firstToResult != null && secondToResult != null)
- combined[i] = SubLattice(i).Join(suba, firstToResult, subb, secondToResult);
- else
- combined[i] = SubLattice(i).Join(suba, subb);
- break;
- case CombineOp.Widen:
- if (firstToResult != null && secondToResult != null)
- combined[i] = SubLattice(i).Widen(suba, firstToResult, subb, secondToResult);
- else
- combined[i] = SubLattice(i).Widen(suba, subb);
- break;
- }
- } else if (thisExists) {
- combined[i] = a[i];
- } else {
- combined[i] = b[i];
- }
- }
- Debug.Assert(combined.IsValid);
- return combined;
- }
-
- public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) {
- //Contract.Requires((b != null));
- //Contract.Requires((a != null));
- Contract.Ensures(Contract.Result<Element>() != null);
- return this.Combine(a, null, b, null, CombineOp.Join);
- }
-
- public override 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<Element>() != null);
- return this.Combine(a, aToResult, b, bToResult, CombineOp.Join);
- }
-
- public override Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) {
- //Contract.Requires((b != null));
- //Contract.Requires((a != null));
- Contract.Ensures(Contract.Result<Element>() != null);
- return this.Combine(a, null, b, null, CombineOp.Meet);
- }
-
- public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) {
- //Contract.Requires((b != null));
- //Contract.Requires((a != null));
- Contract.Ensures(Contract.Result<Element>() != null);
- return this.Combine(a, null, b, null, CombineOp.Widen);
- }
-
- public override 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<Element>() != null);
- return this.Combine(a, aToResult, b, bToResult, CombineOp.Widen);
- }
-
- public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable) {
- //Contract.Requires(variable != null);
- //Contract.Requires(element != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- Elt e = (Elt)element;
- if (IsBottom(e)) {
- return e;
- }
- Elt newValue = new Elt(e.Count, false);
- for (int i = 0; i < this.lattices.Count; i++) {
- newValue[i] = SubLattice(i).Eliminate(cce.NonNull(e[i]), variable);
- }
- return newValue;
- }
-
-
- public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr) {
- //Contract.Requires(expr != null);
- //Contract.Requires(element != null);
- //Contract.Ensures(Contract.Result<Element>() != null);
- Elt e = (Elt)element;
- if (IsBottom(e)) {
- return e;
- }
- Elt newValue = new Elt(e.Count, false);
- for (int i = 0; i < this.lattices.Count; i++) {
- newValue[i] = SubLattice(i).Constrain(cce.NonNull(e[i]), expr);
- }
- return newValue;
- }
-
-
- public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
- //Contract.Requires(newName != null);
- //Contract.Requires(oldName != null);
- //Contract.Requires(element != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- Elt e = (Elt)element;
- if (IsBottom(e)) {
- return e;
- }
- Elt newValue = new Elt(e.Count, false);
- for (int i = 0; i < this.lattices.Count; i++) {
- newValue[i] = SubLattice(i).Rename(cce.NonNull(e[i]), oldName, newName);
- }
- return newValue;
- }
-
-
- public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
- //Contract.Requires(args != null);
- //Contract.Requires(f != null);
- bool result = false;
-
- for (int i = 0; i < this.lattices.Count; i++) {
- result = (result || SubLattice(i).Understands(f, args));
- }
-
- return result;
- }
-
-
- public override string/*!*/ ToString(Element/*!*/ element) {
- //Contract.Requires(element != null);
- Contract.Ensures(Contract.Result<string>() != null);
- Elt e = (Elt)element;
- return e.ToString();
- }
-
-
- public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
- //Contract.Requires(element != null);
- Contract.Ensures(Contract.Result<IExpr>() != null);
- Elt e = (Elt)element;
-
- IExpr result = propExprFactory.True;
- for (int i = 0; i < e.Count; i++) {
- IExpr conjunct = SubLattice(i).ToPredicate(cce.NonNull(e[i]));
- Contract.Assert(conjunct != null);
-
- result = Prop.SimplifiedAnd(propExprFactory, conjunct, result);
- }
- return result;
- }
-
- /// <summary>
- /// Return an expression that is equivalent to the given expression that does not
- /// contain the given variable according to the lattice element and queryable.
- ///
- /// Simply asks each sublattice to try to generate an equivalent expression. We
- /// do not try to combine information to infer new equivalences here.
- /// </summary>
- /// <param name="e">The lattice element.</param>
- /// <param name="q">A queryable for asking addtional information.</param>
- /// <param name="expr">The expression to find an equivalent expression.</param>
- /// <param name="var">The variable to eliminate.</param>
- /// <returns>
- /// An equivalent expression to <paramref name="expr"/> without <paramref name="var"/>
- /// or null if not possible.
- /// </returns>
- public override IExpr/*?*/ EquivalentExpr(Element/*!*/ element, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, Set/*<IVariable!>*//*!*/ prohibitedVars) {
- //Contract.Requires(prohibitedVars != null);
- //Contract.Requires(var != null);
- //Contract.Requires(expr != null);
- //Contract.Requires(q != null);
- //Contract.Requires(element != null);
- Elt/*!*/ e = (Elt/*!*/)cce.NonNull(element);
-
- for (int i = 0; i < e.Count; i++) {
- IExpr equivexpr = SubLattice(i).EquivalentExpr(cce.NonNull(e[i]), q, expr, var, prohibitedVars);
-
- if (equivexpr != null)
- return equivexpr;
- }
-
- return null;
- }
-
-
- public override Answer CheckPredicate(Element/*!*/ element, IExpr/*!*/ pred) {
- //Contract.Requires(pred != null);
- //Contract.Requires(element != null);
- Elt/*!*/ e = (Elt/*!*/)cce.NonNull(element);
-
- for (int i = 0; i < e.Count; i++) {
- Answer ans = SubLattice(i).CheckPredicate(cce.NonNull(e[i]), pred);
-
- if (ans == Answer.Yes || ans == Answer.No)
- return ans;
- }
-
- return Answer.Maybe;
- }
-
-
- public override Answer CheckVariableDisequality(Element/*!*/ element, IVariable/*!*/ var1, IVariable/*!*/ var2) {
- //Contract.Requires(var2 != null);
- //Contract.Requires(var1 != null);
- //Contract.Requires(element != null);
- Elt/*!*/ e = (Elt/*!*/)cce.NonNull(element);
-
- for (int i = 0; i < e.Count; i++) {
- Answer ans = SubLattice(i).CheckVariableDisequality(cce.NonNull(e[i]), var1, var2);
-
- if (ans == Answer.Yes || ans == Answer.No)
- return ans;
- }
-
- return Answer.Maybe;
- }
-
-
-
- public override void Validate() {
- base.Validate();
- foreach (Lattice/*!*/ l in lattices) {
- Contract.Assert(l != null);
- l.Validate();
- }
- }
-
- /// <summary>
- /// The enumeration over a MultiLattice is its sublattices.
- /// </summary>
- /// <returns>An enumerator over the sublattices.</returns>
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- public IEnumerator/*<Lattice!>*//*!*/ GetEnumerator() {
- Contract.Ensures(Contract.Result<IEnumerator>() != null);
- return lattices.GetEnumerator();
- }
-
- /// <summary>
- /// Return an enumerable over a mapping of sublattices to the their corresponding
- /// lattice elements given a MultiLattice element.
- /// </summary>
- /// <param name="element">The MultiLattice element.</param>
- /// <returns>
- /// An enumerable that yields an IDictionaryEnumerator over the
- /// (Lattice, Lattice.Element) pairs.
- /// </returns>
- public IEnumerable/*!*/ Subelements(Element/*!*/ element) {
- Contract.Requires(element != null);
- Contract.Ensures(Contract.Result<IEnumerable>() != null);
- return new SubelementsEnumerable(this, (Elt/*!*/)cce.NonNull(element));
- }
-
- /// <summary>
- /// An enumerator over the sublattices and elements.
- /// </summary>
- private sealed class SubelementsEnumerable : IEnumerable {
- private sealed class SubelementsEnumerator : IDictionaryEnumerator {
- private readonly IEnumerator/*<Lattice!>*//*!*/ multiLatticeIter;
- private readonly IEnumerator/*<Lattice.Element!>*//*!*/ multiElementIter;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(multiElementIter != null);
- Contract.Invariant(multiLatticeIter != null);
- }
-
-
- public SubelementsEnumerator(MultiLattice/*!*/ multiLattice, Elt/*!*/ multiElement) {
- Contract.Requires(multiElement != null);
- Contract.Requires(multiLattice != null);
- Contract.Requires(multiElement.elementPerLattice != null);
- this.multiLatticeIter = multiLattice.lattices.GetEnumerator();
- this.multiElementIter = multiElement.elementPerLattice.GetEnumerator();
- // base();
- }
-
- public DictionaryEntry Entry {
- get {
- return new DictionaryEntry(cce.NonNull(multiLatticeIter.Current), multiElementIter.Current);
- }
- }
-
- public object Key {
- get {
- return multiLatticeIter.Current;
- }
- }
-
- public object Value {
- get {
- return multiElementIter.Current;
- }
- }
-
- public object Current {
- get {
- return this.Entry;
- }
- }
-
- public bool MoveNext() {
- return multiLatticeIter.MoveNext() && multiElementIter.MoveNext();
- }
-
- public void Reset() {
- multiLatticeIter.Reset();
- multiElementIter.Reset();
- }
- }
-
- private MultiLattice/*!*/ multiLattice;
- private Elt/*!*/ multiElement;
-
- public SubelementsEnumerable(MultiLattice/*!*/ multiLattice, Elt/*!*/ multiElement) {
- Contract.Requires(multiElement != null);
- Contract.Requires(multiLattice != null);
- this.multiLattice = multiLattice;
- this.multiElement = multiElement;
- // base();
- }
-
- [Pure]
- [GlobalAccess(false)]
- [Escapes(true, false)]
- public IEnumerator/*!*/ GetEnumerator() {
- Contract.Ensures(Contract.Result<IEnumerator>() != null);
- return new SubelementsEnumerator(multiLattice, multiElement);
- }
- }
-
-
- }
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework { + using System.Diagnostics.Contracts; + using System.Collections; + using System.Collections.Generic; + using System.Diagnostics; + using Microsoft.AbstractInterpretationFramework.Collections; + + using Microsoft.Boogie; + + using ISet = Microsoft.Boogie.GSet<object>; + using Set = Microsoft.Boogie.GSet<object>; + + + /// <summary> + /// The cartesian product lattice. + /// </summary> + public class MultiLattice : Lattice, IEnumerable { + internal class Elt : Element { + public /*MaybeNull*/Element[] elementPerLattice; + + public Elt(int domainCount, bool isBottom) { + this.elementPerLattice = (domainCount == 0 && isBottom) ? null : new Element[domainCount]; + } + + private Elt(Elt/*!*/ other) { + Contract.Requires(other != null); + Element[] otherEPL = other.elementPerLattice; + if (otherEPL != null) { + Element[] newEPL = new Element[otherEPL.Length]; + for (int i = 0; i < newEPL.Length; i++) { + newEPL[i] = (Element)(cce.NonNull(otherEPL[i])).Clone(); + } + this.elementPerLattice = newEPL; + } + } + + public override Element/*!*/ Clone() { + Contract.Ensures(Contract.Result<Element>() != null); + return new Elt(this); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result<string>() != null); + // string s = "MultiLattice+Elt{"; + // string sep = ""; + // Element[] epl = this.elementPerLattice; + // if (epl != null) + // { + // foreach (Element! e in epl) + // { + // s += sep + e.ToString(); + // sep = ", "; + // } + // } + // return s + "}"; + if (elementPerLattice == null) + return ""; + System.Text.StringBuilder buffer = new System.Text.StringBuilder(); + for (int i = 0; i < this.Count; i++) { + if (i > 0) + buffer.Append("; "); + buffer.AppendFormat("{0}", elementPerLattice[i]); + } + return buffer.ToString(); + } + + public override void Dump(string/*!*/ msg) { + //Contract.Requires(msg != null); + System.Console.WriteLine("MultiLattice.Elt.Dump({0})", msg); + Element[] epl = this.elementPerLattice; + if (epl != null) { + foreach (Element/*!*/ e in epl) { + Contract.Assert(e != null); + e.Dump(msg); + } + } + } + + [Pure] + public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() { + Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>())); + List<IVariable/*!*/>/*!*/ list = new List<IVariable/*!*/>(); + for (int i = 0; i < this.Count; i++) { + list.AddRange(cce.NonNull(this[i]).FreeVariables()); + } + return cce.NonNull(list.AsReadOnly()); + } + + public static Elt/*!*/ Top(ArrayList/*<Lattice>*//*!*/ lattices) { + Contract.Requires(lattices != null); + Contract.Ensures(Contract.Result<Elt>() != null); + Elt multiValue = new Elt(lattices.Count, false); + for (int i = 0; i < lattices.Count; i++) { + Lattice d = (Lattice/*!*/)cce.NonNull(lattices[i]); + multiValue[d.Index] = d.Top; + } + Debug.Assert(multiValue.IsValid); + return multiValue; + } + + + public static Elt/*!*/ Bottom(ArrayList/*<Lattice>*//*!*/ lattices) { + Contract.Requires(lattices != null); + Contract.Ensures(Contract.Result<Elt>() != null); + Elt multiValue = new Elt(lattices.Count, true); + for (int i = 0; i < lattices.Count; i++) { + Lattice d = (Lattice/*!*/)cce.NonNull(lattices[i]); + multiValue[d.Index] = d.Bottom; + } + Debug.Assert(multiValue.IsValid); + return multiValue; + } + + public bool IsValid { + get { + if (this.elementPerLattice == null) { + return true; /*bottom*/ + } + + Element[] epl = this.elementPerLattice; + for (int i = 0; i < epl.Length; i++) { + if (epl[i] == null) { + return false; + } + } + return true; + } + } + + public int Count { + get { + return this.elementPerLattice == null ? 0 : this.elementPerLattice.Length; + } + } + + public bool Contains(int i) { + return 0 <= i && i < this.Count; + } + + public Element this[int i] // just syntactic sugar + { + get { + Element[] epl = this.elementPerLattice; + return epl == null ? null : epl[i]; + } + set { + Element[] epl = this.elementPerLattice; + if (epl == null) + return; + epl[i] = value; + } + } + + } // class + + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(lattices != null); + Contract.Invariant(propExprFactory != null); + } + + ArrayList/*<Lattice>*//*!*/ lattices = new ArrayList(); + + private readonly IPropExprFactory/*!*/ propExprFactory; + + + public MultiLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory) + : base(valueExprFactory) { + Contract.Requires(valueExprFactory != null); + Contract.Requires(propExprFactory != null); + this.propExprFactory = propExprFactory; + // base(valueExprFactory); + } + + + + public void AddLattice(Lattice lattice) { + this.lattices.Add(lattice); + } + + private Lattice/*!*/ SubLattice(int i) { + Contract.Ensures(Contract.Result<Lattice>() != null); + return (Lattice/*!*/)cce.NonNull(this.lattices[i]); + } + + + public override Element/*!*/ Top { + get { + Contract.Ensures(Contract.Result<Element>() != null); + return Elt.Top(this.lattices); + } + } + + public override Element/*!*/ Bottom { + get { + Contract.Ensures(Contract.Result<Element>() != null); + return Elt.Bottom(this.lattices); + } + } + + + + + public override bool IsBottom(Element/*!*/ element) { + //Contract.Requires(element != null); + Elt e = (Elt)element; + // The program is errorneous/nonterminating if any subdomain knows it is. + // + if (e.elementPerLattice == null) { + return true; + } + for (int i = 0; i < e.Count; i++) { + if (SubLattice(i).IsBottom(cce.NonNull(e[i]))) { + return true; + } + } + return false; + } + + public override bool IsTop(Element/*!*/ element) { + //Contract.Requires(element != null); + Elt e = (Elt)element; + if (e.elementPerLattice == null) { + return false; + } + // The multidomain knows nothing about the program only if no subdomain + // knows anything about it. + // + for (int i = 0; i < e.Count; i++) { + if (!SubLattice(i).IsTop(cce.NonNull(e[i]))) { + return false; + } + } + return true; + } + + protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) { + //Contract.Requires(second != null); + //Contract.Requires(first != null); + Elt a = (Elt)first; + Elt b = (Elt)second; + + for (int i = 0; i < a.Count; i++) { + Element thisElement = cce.NonNull(a[i]); + Element thatElement = cce.NonNull(b[i]); + if (thisElement.GetType() != thatElement.GetType()) { + throw new System.InvalidOperationException( + "AtMost called on MultiDomain objects with different lattices" + ); + } + if (!SubLattice(i).LowerThan(thisElement, thatElement)) { + return false; + } + } + return true; + } + + protected override bool AtMost(Element/*!*/ first, ICombineNameMap/*!*/ firstToResult, Element/*!*/ second, ICombineNameMap/*!*/ secondToResult) { + //Contract.Requires(secondToResult != null); + //Contract.Requires(second != null); + //Contract.Requires(firstToResult != null); + //Contract.Requires(first != null); + Elt a = (Elt)first; + Elt b = (Elt)second; + + for (int i = 0; i < a.Count; i++) { + Element thisElement = cce.NonNull(a[i]); + Element thatElement = cce.NonNull(b[i]); + if (thisElement.GetType() != thatElement.GetType()) { + throw new System.InvalidOperationException( + "AtMost called on MultiDomain objects with different lattices" + ); + } + if (!SubLattice(i).LowerThan(thisElement, firstToResult, thatElement, secondToResult)) { + return false; + } + } + return true; + } + + + private enum CombineOp { + Meet, + Join, + Widen + } + + private Element/*!*/ Combine(Element/*!*/ first, ICombineNameMap/*?*/ firstToResult, Element/*!*/ second, ICombineNameMap/*?*/ secondToResult, CombineOp c) { + Contract.Requires(second != null); + Contract.Requires(first != null); + Contract.Ensures(Contract.Result<Element>() != null); + Elt a = (Elt)first; + Elt b = (Elt)second; + + int unionCount = System.Math.Max(a.Count, b.Count); + Elt combined = new Elt(unionCount, IsBottom(a) && IsBottom(b)); + for (int i = 0; i < unionCount; i++) { + bool thisExists = a.Contains(i); + bool thatExists = b.Contains(i); + + if (thisExists && thatExists) { + Lattice.Element suba = a[i]; + Lattice.Element subb = b[i]; + Contract.Assert(suba != null && subb != null); + + switch (c) { + case CombineOp.Meet: + combined[i] = SubLattice(i).Meet(suba, subb); + break; + case CombineOp.Join: + if (firstToResult != null && secondToResult != null) + combined[i] = SubLattice(i).Join(suba, firstToResult, subb, secondToResult); + else + combined[i] = SubLattice(i).Join(suba, subb); + break; + case CombineOp.Widen: + if (firstToResult != null && secondToResult != null) + combined[i] = SubLattice(i).Widen(suba, firstToResult, subb, secondToResult); + else + combined[i] = SubLattice(i).Widen(suba, subb); + break; + } + } else if (thisExists) { + combined[i] = a[i]; + } else { + combined[i] = b[i]; + } + } + Debug.Assert(combined.IsValid); + return combined; + } + + public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires((b != null)); + //Contract.Requires((a != null)); + Contract.Ensures(Contract.Result<Element>() != null); + return this.Combine(a, null, b, null, CombineOp.Join); + } + + public override 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<Element>() != null); + return this.Combine(a, aToResult, b, bToResult, CombineOp.Join); + } + + public override Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires((b != null)); + //Contract.Requires((a != null)); + Contract.Ensures(Contract.Result<Element>() != null); + return this.Combine(a, null, b, null, CombineOp.Meet); + } + + public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) { + //Contract.Requires((b != null)); + //Contract.Requires((a != null)); + Contract.Ensures(Contract.Result<Element>() != null); + return this.Combine(a, null, b, null, CombineOp.Widen); + } + + public override 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<Element>() != null); + return this.Combine(a, aToResult, b, bToResult, CombineOp.Widen); + } + + public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable) { + //Contract.Requires(variable != null); + //Contract.Requires(element != null); + Contract.Ensures(Contract.Result<Element>() != null); + Elt e = (Elt)element; + if (IsBottom(e)) { + return e; + } + Elt newValue = new Elt(e.Count, false); + for (int i = 0; i < this.lattices.Count; i++) { + newValue[i] = SubLattice(i).Eliminate(cce.NonNull(e[i]), variable); + } + return newValue; + } + + + public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr) { + //Contract.Requires(expr != null); + //Contract.Requires(element != null); + //Contract.Ensures(Contract.Result<Element>() != null); + Elt e = (Elt)element; + if (IsBottom(e)) { + return e; + } + Elt newValue = new Elt(e.Count, false); + for (int i = 0; i < this.lattices.Count; i++) { + newValue[i] = SubLattice(i).Constrain(cce.NonNull(e[i]), expr); + } + return newValue; + } + + + public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) { + //Contract.Requires(newName != null); + //Contract.Requires(oldName != null); + //Contract.Requires(element != null); + Contract.Ensures(Contract.Result<Element>() != null); + Elt e = (Elt)element; + if (IsBottom(e)) { + return e; + } + Elt newValue = new Elt(e.Count, false); + for (int i = 0; i < this.lattices.Count; i++) { + newValue[i] = SubLattice(i).Rename(cce.NonNull(e[i]), oldName, newName); + } + return newValue; + } + + + public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) { + //Contract.Requires(args != null); + //Contract.Requires(f != null); + bool result = false; + + for (int i = 0; i < this.lattices.Count; i++) { + result = (result || SubLattice(i).Understands(f, args)); + } + + return result; + } + + + public override string/*!*/ ToString(Element/*!*/ element) { + //Contract.Requires(element != null); + Contract.Ensures(Contract.Result<string>() != null); + Elt e = (Elt)element; + return e.ToString(); + } + + + public override IExpr/*!*/ ToPredicate(Element/*!*/ element) { + //Contract.Requires(element != null); + Contract.Ensures(Contract.Result<IExpr>() != null); + Elt e = (Elt)element; + + IExpr result = propExprFactory.True; + for (int i = 0; i < e.Count; i++) { + IExpr conjunct = SubLattice(i).ToPredicate(cce.NonNull(e[i])); + Contract.Assert(conjunct != null); + + result = Prop.SimplifiedAnd(propExprFactory, conjunct, result); + } + return result; + } + + /// <summary> + /// Return an expression that is equivalent to the given expression that does not + /// contain the given variable according to the lattice element and queryable. + /// + /// Simply asks each sublattice to try to generate an equivalent expression. We + /// do not try to combine information to infer new equivalences here. + /// </summary> + /// <param name="e">The lattice element.</param> + /// <param name="q">A queryable for asking addtional information.</param> + /// <param name="expr">The expression to find an equivalent expression.</param> + /// <param name="var">The variable to eliminate.</param> + /// <returns> + /// An equivalent expression to <paramref name="expr"/> without <paramref name="var"/> + /// or null if not possible. + /// </returns> + public override IExpr/*?*/ EquivalentExpr(Element/*!*/ element, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, Set/*<IVariable!>*//*!*/ prohibitedVars) { + //Contract.Requires(prohibitedVars != null); + //Contract.Requires(var != null); + //Contract.Requires(expr != null); + //Contract.Requires(q != null); + //Contract.Requires(element != null); + Elt/*!*/ e = (Elt/*!*/)cce.NonNull(element); + + for (int i = 0; i < e.Count; i++) { + IExpr equivexpr = SubLattice(i).EquivalentExpr(cce.NonNull(e[i]), q, expr, var, prohibitedVars); + + if (equivexpr != null) + return equivexpr; + } + + return null; + } + + + public override Answer CheckPredicate(Element/*!*/ element, IExpr/*!*/ pred) { + //Contract.Requires(pred != null); + //Contract.Requires(element != null); + Elt/*!*/ e = (Elt/*!*/)cce.NonNull(element); + + for (int i = 0; i < e.Count; i++) { + Answer ans = SubLattice(i).CheckPredicate(cce.NonNull(e[i]), pred); + + if (ans == Answer.Yes || ans == Answer.No) + return ans; + } + + return Answer.Maybe; + } + + + public override Answer CheckVariableDisequality(Element/*!*/ element, IVariable/*!*/ var1, IVariable/*!*/ var2) { + //Contract.Requires(var2 != null); + //Contract.Requires(var1 != null); + //Contract.Requires(element != null); + Elt/*!*/ e = (Elt/*!*/)cce.NonNull(element); + + for (int i = 0; i < e.Count; i++) { + Answer ans = SubLattice(i).CheckVariableDisequality(cce.NonNull(e[i]), var1, var2); + + if (ans == Answer.Yes || ans == Answer.No) + return ans; + } + + return Answer.Maybe; + } + + + + public override void Validate() { + base.Validate(); + foreach (Lattice/*!*/ l in lattices) { + Contract.Assert(l != null); + l.Validate(); + } + } + + /// <summary> + /// The enumeration over a MultiLattice is its sublattices. + /// </summary> + /// <returns>An enumerator over the sublattices.</returns> + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + public IEnumerator/*<Lattice!>*//*!*/ GetEnumerator() { + Contract.Ensures(Contract.Result<IEnumerator>() != null); + return lattices.GetEnumerator(); + } + + /// <summary> + /// Return an enumerable over a mapping of sublattices to the their corresponding + /// lattice elements given a MultiLattice element. + /// </summary> + /// <param name="element">The MultiLattice element.</param> + /// <returns> + /// An enumerable that yields an IDictionaryEnumerator over the + /// (Lattice, Lattice.Element) pairs. + /// </returns> + public IEnumerable/*!*/ Subelements(Element/*!*/ element) { + Contract.Requires(element != null); + Contract.Ensures(Contract.Result<IEnumerable>() != null); + return new SubelementsEnumerable(this, (Elt/*!*/)cce.NonNull(element)); + } + + /// <summary> + /// An enumerator over the sublattices and elements. + /// </summary> + private sealed class SubelementsEnumerable : IEnumerable { + private sealed class SubelementsEnumerator : IDictionaryEnumerator { + private readonly IEnumerator/*<Lattice!>*//*!*/ multiLatticeIter; + private readonly IEnumerator/*<Lattice.Element!>*//*!*/ multiElementIter; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(multiElementIter != null); + Contract.Invariant(multiLatticeIter != null); + } + + + public SubelementsEnumerator(MultiLattice/*!*/ multiLattice, Elt/*!*/ multiElement) { + Contract.Requires(multiElement != null); + Contract.Requires(multiLattice != null); + Contract.Requires(multiElement.elementPerLattice != null); + this.multiLatticeIter = multiLattice.lattices.GetEnumerator(); + this.multiElementIter = multiElement.elementPerLattice.GetEnumerator(); + // base(); + } + + public DictionaryEntry Entry { + get { + return new DictionaryEntry(cce.NonNull(multiLatticeIter.Current), multiElementIter.Current); + } + } + + public object Key { + get { + return multiLatticeIter.Current; + } + } + + public object Value { + get { + return multiElementIter.Current; + } + } + + public object Current { + get { + return this.Entry; + } + } + + public bool MoveNext() { + return multiLatticeIter.MoveNext() && multiElementIter.MoveNext(); + } + + public void Reset() { + multiLatticeIter.Reset(); + multiElementIter.Reset(); + } + } + + private MultiLattice/*!*/ multiLattice; + private Elt/*!*/ multiElement; + + public SubelementsEnumerable(MultiLattice/*!*/ multiLattice, Elt/*!*/ multiElement) { + Contract.Requires(multiElement != null); + Contract.Requires(multiLattice != null); + this.multiLattice = multiLattice; + this.multiElement = multiElement; + // base(); + } + + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + public IEnumerator/*!*/ GetEnumerator() { + Contract.Ensures(Contract.Result<IEnumerator>() != null); + return new SubelementsEnumerator(multiLattice, multiElement); + } + } + + + } +} |