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/MultiLattice.cs | 1294 ++++++++++++++++++------------------ 1 file changed, 647 insertions(+), 647 deletions(-) (limited to 'Source/AIFramework/MultiLattice.cs') 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; - using Set = Microsoft.Boogie.GSet; - - - /// - /// The cartesian product lattice. - /// - 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() != null); - return new Elt(this); - } - - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != 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/*!*/ FreeVariables() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List/*!*/ list = new List(); - 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/**//*!*/ lattices) { - Contract.Requires(lattices != null); - Contract.Ensures(Contract.Result() != 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/**//*!*/ lattices) { - Contract.Requires(lattices != null); - Contract.Ensures(Contract.Result() != 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/**//*!*/ 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() != null); - return (Lattice/*!*/)cce.NonNull(this.lattices[i]); - } - - - public override Element/*!*/ Top { - get { - Contract.Ensures(Contract.Result() != null); - return Elt.Top(this.lattices); - } - } - - public override Element/*!*/ Bottom { - get { - Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != null); - Elt e = (Elt)element; - return e.ToString(); - } - - - public override IExpr/*!*/ ToPredicate(Element/*!*/ element) { - //Contract.Requires(element != null); - Contract.Ensures(Contract.Result() != 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; - } - - /// - /// 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. - /// - /// The lattice element. - /// A queryable for asking addtional information. - /// The expression to find an equivalent expression. - /// The variable to eliminate. - /// - /// An equivalent expression to without - /// or null if not possible. - /// - public override IExpr/*?*/ EquivalentExpr(Element/*!*/ element, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, Set/**//*!*/ 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(); - } - } - - /// - /// The enumeration over a MultiLattice is its sublattices. - /// - /// An enumerator over the sublattices. - [Pure] - [GlobalAccess(false)] - [Escapes(true, false)] - public IEnumerator/**//*!*/ GetEnumerator() { - Contract.Ensures(Contract.Result() != null); - return lattices.GetEnumerator(); - } - - /// - /// Return an enumerable over a mapping of sublattices to the their corresponding - /// lattice elements given a MultiLattice element. - /// - /// The MultiLattice element. - /// - /// An enumerable that yields an IDictionaryEnumerator over the - /// (Lattice, Lattice.Element) pairs. - /// - public IEnumerable/*!*/ Subelements(Element/*!*/ element) { - Contract.Requires(element != null); - Contract.Ensures(Contract.Result() != null); - return new SubelementsEnumerable(this, (Elt/*!*/)cce.NonNull(element)); - } - - /// - /// An enumerator over the sublattices and elements. - /// - private sealed class SubelementsEnumerable : IEnumerable { - private sealed class SubelementsEnumerator : IDictionaryEnumerator { - private readonly IEnumerator/**//*!*/ multiLatticeIter; - private readonly IEnumerator/**//*!*/ 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() != 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; + using Set = Microsoft.Boogie.GSet; + + + /// + /// The cartesian product lattice. + /// + 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() != null); + return new Elt(this); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != 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/*!*/ FreeVariables() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List/*!*/ list = new List(); + 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/**//*!*/ lattices) { + Contract.Requires(lattices != null); + Contract.Ensures(Contract.Result() != 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/**//*!*/ lattices) { + Contract.Requires(lattices != null); + Contract.Ensures(Contract.Result() != 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/**//*!*/ 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() != null); + return (Lattice/*!*/)cce.NonNull(this.lattices[i]); + } + + + public override Element/*!*/ Top { + get { + Contract.Ensures(Contract.Result() != null); + return Elt.Top(this.lattices); + } + } + + public override Element/*!*/ Bottom { + get { + Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != 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() != null); + Elt e = (Elt)element; + return e.ToString(); + } + + + public override IExpr/*!*/ ToPredicate(Element/*!*/ element) { + //Contract.Requires(element != null); + Contract.Ensures(Contract.Result() != 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; + } + + /// + /// 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. + /// + /// The lattice element. + /// A queryable for asking addtional information. + /// The expression to find an equivalent expression. + /// The variable to eliminate. + /// + /// An equivalent expression to without + /// or null if not possible. + /// + public override IExpr/*?*/ EquivalentExpr(Element/*!*/ element, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, Set/**//*!*/ 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(); + } + } + + /// + /// The enumeration over a MultiLattice is its sublattices. + /// + /// An enumerator over the sublattices. + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + public IEnumerator/**//*!*/ GetEnumerator() { + Contract.Ensures(Contract.Result() != null); + return lattices.GetEnumerator(); + } + + /// + /// Return an enumerable over a mapping of sublattices to the their corresponding + /// lattice elements given a MultiLattice element. + /// + /// The MultiLattice element. + /// + /// An enumerable that yields an IDictionaryEnumerator over the + /// (Lattice, Lattice.Element) pairs. + /// + public IEnumerable/*!*/ Subelements(Element/*!*/ element) { + Contract.Requires(element != null); + Contract.Ensures(Contract.Result() != null); + return new SubelementsEnumerable(this, (Elt/*!*/)cce.NonNull(element)); + } + + /// + /// An enumerator over the sublattices and elements. + /// + private sealed class SubelementsEnumerable : IEnumerable { + private sealed class SubelementsEnumerator : IDictionaryEnumerator { + private readonly IEnumerator/**//*!*/ multiLatticeIter; + private readonly IEnumerator/**//*!*/ 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() != null); + return new SubelementsEnumerator(multiLattice, multiElement); + } + } + + + } +} -- cgit v1.2.3