diff options
Diffstat (limited to 'Source/AIFramework/VariableMap/DynamicTypeLattice.cs')
| -rw-r--r-- | Source/AIFramework/VariableMap/DynamicTypeLattice.cs | 1022 |
1 files changed, 511 insertions, 511 deletions
diff --git a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs index 78bd61a0..edda7c1e 100644 --- a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs +++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs @@ -1,511 +1,511 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework {
- using System.Collections;
- using System.Diagnostics;
- //using System.Compiler.Analysis;
- //using Microsoft.SpecSharp.Collections;
- using System.Diagnostics.Contracts;
-
- /// <summary>
- /// Represents information about the dynamic type of a variable. In particular, for a
- /// variable "v", represents either Bottom, "typeof(v)==T" for some type T, or a set
- /// of constraints "typeof(v) subtype of T_i for some number of T_i's.
- /// </summary>
- public class DynamicTypeLattice : MicroLattice {
- enum What {
- Bottom,
- Exact,
- Bounds
- }
-
- private class Elt : Element {
- // Representation:
- // - Bottom is represented by: what==What.Bottom
- // - An exact type T is represented by: what==What.Exact && ty==T
- // - A set of type constraints T0, T1, T2, ..., T{n-1} is represented by:
- // -- if n==0: what==What.Bounds && ty==null && manyBounds==null
- // -- if n==1: what==What.Bounds && ty==T0 && manyBounds==null
- // -- if n>=2: what==What.Bounds && ty==null &&
- // manyBounds!=null && manyBounds.Length==n &&
- // manyBounds[0]==T0 && manyBounds[1]==T1 && ... && manyBounds[n-1]==T{n-1}
- // The reason for keeping the one-and-only bound in "ty" in case n==1 is to try
- // to prevent the need for allocating a whole array of bounds, since 1 bound is
- // bound to be common.
- // In the representation, there are no redundant bounds in manyBounds.
- // It is assumed that the types can can occur as exact bounds form a single-inheritance
- // hierarchy. That is, if T0 and T1 are types that can occur as exact types, then
- // there is no v such that typeof(v) is a subtype of both T0 and T1, unless T0 and T1 are
- // the same type.
- public readonly What what;
- public readonly IExpr ty;
- [Rep]
- public readonly IExpr[] manyBounds;
- [ContractInvariantMethod]
- void ObjectInvariant() {
-
- Contract.Invariant(what != What.Bottom || ty == null && manyBounds == null);
- Contract.Invariant(manyBounds == null || what == What.Bounds);
- Contract.Invariant(manyBounds == null || Contract.ForAll(0, manyBounds.Length, i => manyBounds[i] != null));
- }
- public Elt(What what, IExpr ty) {
- Contract.Requires(what != What.Bottom || ty == null);
- Contract.Requires(what != What.Exact || ty != null);
- this.what = what;
- this.ty = ty;
- this.manyBounds = null;
- }
-
- public Elt(IExpr[]/*!*/ bounds) {
- Contract.Requires(bounds != null);
- Contract.Requires(Contract.ForAll(0, bounds.Length, i => bounds[i] != null));
- this.what = What.Bounds;
- if (bounds.Length == 0) {
- this.ty = null;
- this.manyBounds = null;
- } else if (bounds.Length == 1) {
- this.ty = bounds[0];
- this.manyBounds = null;
- } else {
- this.ty = null;
- this.manyBounds = bounds;
- }
- }
-
- /// <summary>
- /// Constructs an Elt with "n" bounds, namely the n non-null values of the "bounds" list.
- /// </summary>
- [NotDelayed]
- public Elt(ArrayList /*IExpr*//*!*/ bounds, int n) {
- Contract.Requires(bounds != null);
- Contract.Requires(0 <= n && n <= bounds.Count);
- this.what = What.Bounds;
- if (n > 1) {
- this.manyBounds = new IExpr[n];
- }
- int k = 0;
- foreach (IExpr bound in bounds) {
- if (bound != null) {
- Contract.Assert(k != n);
- if (n == 1) {
- Contract.Assert(this.ty == null);
- this.ty = bound;
- } else {
- Contract.Assume(manyBounds != null);
- manyBounds[k] = bound;
- }
- k++;
- }
- }
- Contract.Assert(k == n);
- }
-
- public int BoundsCount {
- get {
- Contract.Ensures(0 <= Contract.Result<int>());
- if (manyBounds != null) {
- return manyBounds.Length;
- } else if (ty != null) {
- return 1;
- } else {
- return 0;
- }
- }
- }
-
- [Pure]
- public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
- Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
- return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
- }
-
- public override Element/*!*/ Clone() {
- Contract.Ensures(Contract.Result<Element>() != null);
- if (this.manyBounds != null)
- return new Elt(this.manyBounds);
- else
- return new Elt(this.what, this.ty);
- }
- }
-
- readonly ITypeExprFactory/*!*/ factory;
- readonly IPropExprFactory/*!*/ propFactory;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(factory != null);
- Contract.Invariant(propFactory != null);
- }
-
-
- public DynamicTypeLattice(ITypeExprFactory/*!*/ factory, IPropExprFactory/*!*/ propFactory) {
- Contract.Requires(propFactory != null);
- Contract.Requires(factory != null);
- this.factory = factory;
- this.propFactory = propFactory;
- // base();
- }
-
- public override Element/*!*/ Top {
- get {
- Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(What.Bounds, null);
- }
- }
-
- public override Element/*!*/ Bottom {
- get {
- Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(What.Bottom, null);
- }
- }
-
- public override bool IsTop(Element/*!*/ element) {
- //Contract.Requires(element != null);
- Elt e = (Elt)element;
- return e.what == What.Bounds && e.ty == null && e.manyBounds == null;
- }
-
- public override bool IsBottom(Element/*!*/ element) {
- //Contract.Requires(element != null);
- Elt e = (Elt)element;
- return e.what == What.Bottom;
- }
-
- public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
- //Contract.Requires(second != null);
- //Contract.Requires(first != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
- if (a.what == What.Exact && b.what == What.Exact) {
- Contract.Assert(a.ty != null && b.ty != null);
- if (factory.IsTypeEqual(a.ty, b.ty)) {
- return a;
- } else {
- return new Elt(What.Bounds, factory.JoinTypes(a.ty, b.ty));
- }
- }
-
- // The result is going to be a Bounds, since at least one of the operands is a Bounds.
- Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount); // a preconditions is that neither operand is Top
- int n = a.BoundsCount + b.BoundsCount;
-
- // Special case: a and b each has exactly one bound
- if (n == 2) {
- Contract.Assert(a.ty != null && b.ty != null);
- IExpr join = factory.JoinTypes(a.ty, b.ty);
- Contract.Assert(join != null);
- if (join == a.ty && a.what == What.Bounds) {
- return a;
- } else if (join == b.ty && b.what == What.Bounds) {
- return b;
- } else {
- return new Elt(What.Bounds, join);
- }
- }
-
- // General case
- ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n); // final size
- ArrayList /*IExpr!*/ result = new ArrayList /*IExpr!*/ (n); // a guess at the size, but could be as big as size(a)*size(b)
- if (a.ty != null) {
- allBounds.Add(a.ty);
- } else {
- allBounds.AddRange(cce.NonNull(a.manyBounds));
- }
- int bStart = allBounds.Count;
- if (b.ty != null) {
- allBounds.Add(b.ty);
- } else {
- allBounds.AddRange(cce.NonNull(b.manyBounds));
- }
- // compute the join of each pair, putting non-redundant joins into "result"
- for (int i = 0; i < bStart; i++) {
- IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);
- for (int j = bStart; j < allBounds.Count; j++) {
- IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);
-
- IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);
- Contract.Assert(join != null);
-
- int k = 0;
- while (k < result.Count) {
- IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(result[k]);
- if (factory.IsSubType(join, r)) {
- // "join" is more restrictive than a bound already placed in "result",
- // so toss out "join" and compute the join of the next pair
- goto NEXT_PAIR;
- } else if (factory.IsSubType(r, join)) {
- // "join" is less restrictive than a bound already placed in "result",
- // so toss out that old bound
- result.RemoveAt(k);
- } else {
- k++;
- }
- }
- result.Add(join);
- NEXT_PAIR: {
- }
- }
- }
- return new Elt(result, result.Count);
- }
-
-
- public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
- //Contract.Requires(second != null);
- //Contract.Requires(first != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
-
- if (a.what == What.Exact && b.what == What.Exact) {
- Contract.Assert(a.ty != null && b.ty != null);
- if (factory.IsTypeEqual(a.ty, b.ty)) {
- return a;
- } else {
- return Bottom;
- }
-
- } else if (a.what == What.Exact || b.what == What.Exact) {
- // One is Bounds, the other Exact. Make b be the Bounds one.
- if (a.what == What.Bounds) {
- Elt tmp = a;
- a = b;
- b = tmp;
- }
- Contract.Assert(a.what == What.Exact && b.what == What.Bounds);
- // Check the exact type against all bounds. If the exact type is more restrictive
- // than all bounds, then return it. If some bound is not met by the exact type, return
- // bottom.
- Contract.Assert(a.ty != null);
- if (b.ty != null && !factory.IsSubType(a.ty, b.ty)) {
- return Bottom;
- }
- if (b.manyBounds != null) {
- foreach (IExpr/*!*/ bound in b.manyBounds) {
- Contract.Assert(bound != null);
- if (!factory.IsSubType(a.ty, bound)) {
- return Bottom;
- }
- }
- }
- return a;
- } else {
- // Both operands are Bounds.
- Contract.Assert(a.what == What.Bounds && b.what == What.Bounds);
-
- // Take all the bounds, but prune those bounds that follow from others.
- Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount); // a preconditions is that neither operand is Top
- int n = a.BoundsCount + b.BoundsCount;
- // Special case: a and b each has exactly one bound
- if (n == 2) {
- Contract.Assert(a.ty != null && b.ty != null);
- if (factory.IsSubType(a.ty, b.ty)) {
- // a is more restrictive
- return a;
- } else if (factory.IsSubType(b.ty, a.ty)) {
- // b is more restrictive
- return b;
- } else {
- IExpr[]/*!*/ bounds = new IExpr[2];
- bounds[0] = a.ty;
- bounds[1] = b.ty;
- return new Elt(bounds);
- }
- }
-
- // General case
- ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n);
- if (a.ty != null) {
- allBounds.Add(a.ty);
- } else {
- allBounds.AddRange(cce.NonNull(a.manyBounds));
- }
- int bStart = allBounds.Count;
- if (b.ty != null) {
- allBounds.Add(b.ty);
- } else {
- allBounds.AddRange(cce.NonNull(b.manyBounds));
- }
- for (int i = 0; i < bStart; i++) {
- IExpr/*!*/ aBound = cce.NonNull((IExpr)allBounds[i]);
- for (int j = bStart; j < allBounds.Count; j++) {
- IExpr bBound = (IExpr/*! Wouldn't the non-null typing in the original Spec# code had made bBound never null,
- * thus negating the need for the continue statement?*/
- )allBounds[j];
- if (bBound == null) {
- continue;
- } else if (factory.IsSubType(aBound, bBound)) {
- // a is more restrictive, so blot out the b bound
- allBounds[j] = null;
- n--;
- } else if (factory.IsSubType(bBound, aBound)) {
- // b is more restrictive, so blot out the a bound
- allBounds[i] = null;
- n--;
- goto CONTINUE_OUTER_LOOP;
- }
- }
- CONTINUE_OUTER_LOOP: {
- }
- }
- Contract.Assert(1 <= n);
- return new Elt(allBounds, n);
- }
- }
-
- public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
- //Contract.Requires(second != null);
- //Contract.Requires(first != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- return Join(first, second);
- }
-
- protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
- {
- //Contract.Requires(first != null);
- //Contract.Requires(second != null);
- Elt/*!*/ a = (Elt/*!*/)cce.NonNull(first);
- Elt/*!*/ b = (Elt/*!*/)cce.NonNull(second);
- Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
-
- if (a.what == What.Exact && b.what == What.Exact) {
- Contract.Assert(a.ty != null && b.ty != null);
- return factory.IsTypeEqual(a.ty, b.ty);
- } else if (b.what == What.Exact) {
- return false;
- } else if (a.what == What.Exact) {
- Contract.Assert(a.ty != null);
- if (b.ty != null) {
- return factory.IsSubType(a.ty, b.ty);
- } else {
- return Contract.ForAll(b.manyBounds, bound => factory.IsSubType(a.ty, bound));
- }
- } else {
- Contract.Assert(a.what == What.Bounds && b.what == What.Bounds);
- Contract.Assert(a.ty != null || a.manyBounds != null); // a precondition is that a is not Top
- Contract.Assert(b.ty != null || b.manyBounds != null); // a precondition is that b is not Top
- // Return true iff: for each constraint in b, there is a stricter constraint in a.
- if (a.ty != null && b.ty != null) {
- return factory.IsSubType(a.ty, b.ty);
- } else if (a.ty != null) {
- return Contract.ForAll(b.manyBounds, bound => factory.IsSubType(a.ty, bound));
- } else if (b.ty != null) {
- return Contract.Exists(a.manyBounds, bound => factory.IsSubType(bound, b.ty));
- } else {
- return Contract.ForAll(b.manyBounds, bBound => Contract.Exists(a.manyBounds, aBound => factory.IsSubType(aBound, bBound)));
- }
- }
- }
-
- public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
- //Contract.Requires(element != null);
- //Contract.Requires(var != null);
- Contract.Ensures(Contract.Result<IExpr>() != null);
- Elt e = (Elt)element;
- switch (e.what) {
- case What.Bottom:
- return propFactory.False;
- case What.Exact:
- return factory.IsExactlyA(var, cce.NonNull(e.ty));
- case What.Bounds:
- if (e.ty == null && e.manyBounds == null) {
- return propFactory.True;
- } else if (e.ty != null) {
- return factory.IsA(var, e.ty);
- } else {
- IExpr/*!*/ p = factory.IsA(var, (IExpr/*!*/)cce.NonNull(e.manyBounds)[0]);
- for (int i = 1; i < e.manyBounds.Length; i++) {
- p = propFactory.And(p, factory.IsA(var, (IExpr/*!*/)cce.NonNull(e.manyBounds[i])));
- }
- return p;
- }
- default: {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- throw new System.Exception();
- }
- }
-
- public override IExpr GetFoldExpr(Element/*!*/ e) {
- //Contract.Requires(e != null);
- // cannot fold into an expression that can be substituted for the variable
- return null;
- }
-
- public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
- //Contract.Requires(args != null);
- //Contract.Requires(f != null);
- bool isEq = f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- if (isEq || f.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
- Contract.Assert(args.Count == 2);
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
- IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
- // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t
- if (isEq && factory.IsTypeConstant(arg0)) {
- // swap the arguments
- IExpr/*!*/ tmp = arg0;
- arg0 = arg1;
- arg1 = tmp;
- } else if (!factory.IsTypeConstant(arg1)) {
- return false;
- }
- IFunApp typeofExpr = arg0 as IFunApp;
- if (typeofExpr != null &&
- typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) {
- Contract.Assert(typeofExpr.Arguments.Count == 1);
- if (typeofExpr.Arguments[0] is IVariable) {
- // we have a match
- return true;
- }
- }
- }
- return false;
- }
-
- public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
- //Contract.Requires(e != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- IFunApp nary = e as IFunApp;
- if (nary != null) {
-
- bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
- IList/*<IExpr!>*//*!*/ args = nary.Arguments;
- Contract.Assert(args != null);
- Contract.Assert(args.Count == 2);
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
- IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
- // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t
- if (isEq && factory.IsTypeConstant(arg0)) {
- // swap the arguments
- IExpr/*!*/ tmp = arg0;
- arg0 = arg1;
- arg1 = tmp;
- } else if (!factory.IsTypeConstant(arg1)) {
- return Top;
- }
- IFunApp typeofExpr = arg0 as IFunApp;
- if (typeofExpr != null &&
- typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) {
- Contract.Assert(typeofExpr.Arguments.Count == 1);
- if (typeofExpr.Arguments[0] is IVariable) {
- // we have a match
- return new Elt(isEq ? What.Exact : What.Bounds, arg1);
- }
- }
- }
- }
- return Top;
- }
-
- }
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework { + using System.Collections; + using System.Diagnostics; + //using System.Compiler.Analysis; + //using Microsoft.SpecSharp.Collections; + using System.Diagnostics.Contracts; + + /// <summary> + /// Represents information about the dynamic type of a variable. In particular, for a + /// variable "v", represents either Bottom, "typeof(v)==T" for some type T, or a set + /// of constraints "typeof(v) subtype of T_i for some number of T_i's. + /// </summary> + public class DynamicTypeLattice : MicroLattice { + enum What { + Bottom, + Exact, + Bounds + } + + private class Elt : Element { + // Representation: + // - Bottom is represented by: what==What.Bottom + // - An exact type T is represented by: what==What.Exact && ty==T + // - A set of type constraints T0, T1, T2, ..., T{n-1} is represented by: + // -- if n==0: what==What.Bounds && ty==null && manyBounds==null + // -- if n==1: what==What.Bounds && ty==T0 && manyBounds==null + // -- if n>=2: what==What.Bounds && ty==null && + // manyBounds!=null && manyBounds.Length==n && + // manyBounds[0]==T0 && manyBounds[1]==T1 && ... && manyBounds[n-1]==T{n-1} + // The reason for keeping the one-and-only bound in "ty" in case n==1 is to try + // to prevent the need for allocating a whole array of bounds, since 1 bound is + // bound to be common. + // In the representation, there are no redundant bounds in manyBounds. + // It is assumed that the types can can occur as exact bounds form a single-inheritance + // hierarchy. That is, if T0 and T1 are types that can occur as exact types, then + // there is no v such that typeof(v) is a subtype of both T0 and T1, unless T0 and T1 are + // the same type. + public readonly What what; + public readonly IExpr ty; + [Rep] + public readonly IExpr[] manyBounds; + [ContractInvariantMethod] + void ObjectInvariant() { + + Contract.Invariant(what != What.Bottom || ty == null && manyBounds == null); + Contract.Invariant(manyBounds == null || what == What.Bounds); + Contract.Invariant(manyBounds == null || Contract.ForAll(0, manyBounds.Length, i => manyBounds[i] != null)); + } + public Elt(What what, IExpr ty) { + Contract.Requires(what != What.Bottom || ty == null); + Contract.Requires(what != What.Exact || ty != null); + this.what = what; + this.ty = ty; + this.manyBounds = null; + } + + public Elt(IExpr[]/*!*/ bounds) { + Contract.Requires(bounds != null); + Contract.Requires(Contract.ForAll(0, bounds.Length, i => bounds[i] != null)); + this.what = What.Bounds; + if (bounds.Length == 0) { + this.ty = null; + this.manyBounds = null; + } else if (bounds.Length == 1) { + this.ty = bounds[0]; + this.manyBounds = null; + } else { + this.ty = null; + this.manyBounds = bounds; + } + } + + /// <summary> + /// Constructs an Elt with "n" bounds, namely the n non-null values of the "bounds" list. + /// </summary> + [NotDelayed] + public Elt(ArrayList /*IExpr*//*!*/ bounds, int n) { + Contract.Requires(bounds != null); + Contract.Requires(0 <= n && n <= bounds.Count); + this.what = What.Bounds; + if (n > 1) { + this.manyBounds = new IExpr[n]; + } + int k = 0; + foreach (IExpr bound in bounds) { + if (bound != null) { + Contract.Assert(k != n); + if (n == 1) { + Contract.Assert(this.ty == null); + this.ty = bound; + } else { + Contract.Assume(manyBounds != null); + manyBounds[k] = bound; + } + k++; + } + } + Contract.Assert(k == n); + } + + public int BoundsCount { + get { + Contract.Ensures(0 <= Contract.Result<int>()); + if (manyBounds != null) { + return manyBounds.Length; + } else if (ty != null) { + return 1; + } else { + return 0; + } + } + } + + [Pure] + public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() { + Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>())); + return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly(); + } + + public override Element/*!*/ Clone() { + Contract.Ensures(Contract.Result<Element>() != null); + if (this.manyBounds != null) + return new Elt(this.manyBounds); + else + return new Elt(this.what, this.ty); + } + } + + readonly ITypeExprFactory/*!*/ factory; + readonly IPropExprFactory/*!*/ propFactory; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(factory != null); + Contract.Invariant(propFactory != null); + } + + + public DynamicTypeLattice(ITypeExprFactory/*!*/ factory, IPropExprFactory/*!*/ propFactory) { + Contract.Requires(propFactory != null); + Contract.Requires(factory != null); + this.factory = factory; + this.propFactory = propFactory; + // base(); + } + + public override Element/*!*/ Top { + get { + Contract.Ensures(Contract.Result<Element>() != null); + return new Elt(What.Bounds, null); + } + } + + public override Element/*!*/ Bottom { + get { + Contract.Ensures(Contract.Result<Element>() != null); + return new Elt(What.Bottom, null); + } + } + + public override bool IsTop(Element/*!*/ element) { + //Contract.Requires(element != null); + Elt e = (Elt)element; + return e.what == What.Bounds && e.ty == null && e.manyBounds == null; + } + + public override bool IsBottom(Element/*!*/ element) { + //Contract.Requires(element != null); + Elt e = (Elt)element; + return e.what == What.Bottom; + } + + public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) { + //Contract.Requires(second != null); + //Contract.Requires(first != null); + Contract.Ensures(Contract.Result<Element>() != null); + Elt a = (Elt)first; + Elt b = (Elt)second; + Contract.Assert(a.what != What.Bottom && b.what != What.Bottom); + if (a.what == What.Exact && b.what == What.Exact) { + Contract.Assert(a.ty != null && b.ty != null); + if (factory.IsTypeEqual(a.ty, b.ty)) { + return a; + } else { + return new Elt(What.Bounds, factory.JoinTypes(a.ty, b.ty)); + } + } + + // The result is going to be a Bounds, since at least one of the operands is a Bounds. + Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount); // a preconditions is that neither operand is Top + int n = a.BoundsCount + b.BoundsCount; + + // Special case: a and b each has exactly one bound + if (n == 2) { + Contract.Assert(a.ty != null && b.ty != null); + IExpr join = factory.JoinTypes(a.ty, b.ty); + Contract.Assert(join != null); + if (join == a.ty && a.what == What.Bounds) { + return a; + } else if (join == b.ty && b.what == What.Bounds) { + return b; + } else { + return new Elt(What.Bounds, join); + } + } + + // General case + ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n); // final size + ArrayList /*IExpr!*/ result = new ArrayList /*IExpr!*/ (n); // a guess at the size, but could be as big as size(a)*size(b) + if (a.ty != null) { + allBounds.Add(a.ty); + } else { + allBounds.AddRange(cce.NonNull(a.manyBounds)); + } + int bStart = allBounds.Count; + if (b.ty != null) { + allBounds.Add(b.ty); + } else { + allBounds.AddRange(cce.NonNull(b.manyBounds)); + } + // compute the join of each pair, putting non-redundant joins into "result" + for (int i = 0; i < bStart; i++) { + IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]); + for (int j = bStart; j < allBounds.Count; j++) { + IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]); + + IExpr/*!*/ join = factory.JoinTypes(aBound, bBound); + Contract.Assert(join != null); + + int k = 0; + while (k < result.Count) { + IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(result[k]); + if (factory.IsSubType(join, r)) { + // "join" is more restrictive than a bound already placed in "result", + // so toss out "join" and compute the join of the next pair + goto NEXT_PAIR; + } else if (factory.IsSubType(r, join)) { + // "join" is less restrictive than a bound already placed in "result", + // so toss out that old bound + result.RemoveAt(k); + } else { + k++; + } + } + result.Add(join); + NEXT_PAIR: { + } + } + } + return new Elt(result, result.Count); + } + + + public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) { + //Contract.Requires(second != null); + //Contract.Requires(first != null); + Contract.Ensures(Contract.Result<Element>() != null); + Elt a = (Elt)first; + Elt b = (Elt)second; + Contract.Assert(a.what != What.Bottom && b.what != What.Bottom); + + if (a.what == What.Exact && b.what == What.Exact) { + Contract.Assert(a.ty != null && b.ty != null); + if (factory.IsTypeEqual(a.ty, b.ty)) { + return a; + } else { + return Bottom; + } + + } else if (a.what == What.Exact || b.what == What.Exact) { + // One is Bounds, the other Exact. Make b be the Bounds one. + if (a.what == What.Bounds) { + Elt tmp = a; + a = b; + b = tmp; + } + Contract.Assert(a.what == What.Exact && b.what == What.Bounds); + // Check the exact type against all bounds. If the exact type is more restrictive + // than all bounds, then return it. If some bound is not met by the exact type, return + // bottom. + Contract.Assert(a.ty != null); + if (b.ty != null && !factory.IsSubType(a.ty, b.ty)) { + return Bottom; + } + if (b.manyBounds != null) { + foreach (IExpr/*!*/ bound in b.manyBounds) { + Contract.Assert(bound != null); + if (!factory.IsSubType(a.ty, bound)) { + return Bottom; + } + } + } + return a; + } else { + // Both operands are Bounds. + Contract.Assert(a.what == What.Bounds && b.what == What.Bounds); + + // Take all the bounds, but prune those bounds that follow from others. + Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount); // a preconditions is that neither operand is Top + int n = a.BoundsCount + b.BoundsCount; + // Special case: a and b each has exactly one bound + if (n == 2) { + Contract.Assert(a.ty != null && b.ty != null); + if (factory.IsSubType(a.ty, b.ty)) { + // a is more restrictive + return a; + } else if (factory.IsSubType(b.ty, a.ty)) { + // b is more restrictive + return b; + } else { + IExpr[]/*!*/ bounds = new IExpr[2]; + bounds[0] = a.ty; + bounds[1] = b.ty; + return new Elt(bounds); + } + } + + // General case + ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n); + if (a.ty != null) { + allBounds.Add(a.ty); + } else { + allBounds.AddRange(cce.NonNull(a.manyBounds)); + } + int bStart = allBounds.Count; + if (b.ty != null) { + allBounds.Add(b.ty); + } else { + allBounds.AddRange(cce.NonNull(b.manyBounds)); + } + for (int i = 0; i < bStart; i++) { + IExpr/*!*/ aBound = cce.NonNull((IExpr)allBounds[i]); + for (int j = bStart; j < allBounds.Count; j++) { + IExpr bBound = (IExpr/*! Wouldn't the non-null typing in the original Spec# code had made bBound never null, + * thus negating the need for the continue statement?*/ + )allBounds[j]; + if (bBound == null) { + continue; + } else if (factory.IsSubType(aBound, bBound)) { + // a is more restrictive, so blot out the b bound + allBounds[j] = null; + n--; + } else if (factory.IsSubType(bBound, aBound)) { + // b is more restrictive, so blot out the a bound + allBounds[i] = null; + n--; + goto CONTINUE_OUTER_LOOP; + } + } + CONTINUE_OUTER_LOOP: { + } + } + Contract.Assert(1 <= n); + return new Elt(allBounds, n); + } + } + + public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) { + //Contract.Requires(second != null); + //Contract.Requires(first != null); + Contract.Ensures(Contract.Result<Element>() != null); + return Join(first, second); + } + + protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that + { + //Contract.Requires(first != null); + //Contract.Requires(second != null); + Elt/*!*/ a = (Elt/*!*/)cce.NonNull(first); + Elt/*!*/ b = (Elt/*!*/)cce.NonNull(second); + Contract.Assert(a.what != What.Bottom && b.what != What.Bottom); + + if (a.what == What.Exact && b.what == What.Exact) { + Contract.Assert(a.ty != null && b.ty != null); + return factory.IsTypeEqual(a.ty, b.ty); + } else if (b.what == What.Exact) { + return false; + } else if (a.what == What.Exact) { + Contract.Assert(a.ty != null); + if (b.ty != null) { + return factory.IsSubType(a.ty, b.ty); + } else { + return Contract.ForAll(b.manyBounds, bound => factory.IsSubType(a.ty, bound)); + } + } else { + Contract.Assert(a.what == What.Bounds && b.what == What.Bounds); + Contract.Assert(a.ty != null || a.manyBounds != null); // a precondition is that a is not Top + Contract.Assert(b.ty != null || b.manyBounds != null); // a precondition is that b is not Top + // Return true iff: for each constraint in b, there is a stricter constraint in a. + if (a.ty != null && b.ty != null) { + return factory.IsSubType(a.ty, b.ty); + } else if (a.ty != null) { + return Contract.ForAll(b.manyBounds, bound => factory.IsSubType(a.ty, bound)); + } else if (b.ty != null) { + return Contract.Exists(a.manyBounds, bound => factory.IsSubType(bound, b.ty)); + } else { + return Contract.ForAll(b.manyBounds, bBound => Contract.Exists(a.manyBounds, aBound => factory.IsSubType(aBound, bBound))); + } + } + } + + public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) { + //Contract.Requires(element != null); + //Contract.Requires(var != null); + Contract.Ensures(Contract.Result<IExpr>() != null); + Elt e = (Elt)element; + switch (e.what) { + case What.Bottom: + return propFactory.False; + case What.Exact: + return factory.IsExactlyA(var, cce.NonNull(e.ty)); + case What.Bounds: + if (e.ty == null && e.manyBounds == null) { + return propFactory.True; + } else if (e.ty != null) { + return factory.IsA(var, e.ty); + } else { + IExpr/*!*/ p = factory.IsA(var, (IExpr/*!*/)cce.NonNull(e.manyBounds)[0]); + for (int i = 1; i < e.manyBounds.Length; i++) { + p = propFactory.And(p, factory.IsA(var, (IExpr/*!*/)cce.NonNull(e.manyBounds[i]))); + } + return p; + } + default: { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + throw new System.Exception(); + } + } + + public override IExpr GetFoldExpr(Element/*!*/ e) { + //Contract.Requires(e != null); + // cannot fold into an expression that can be substituted for the variable + return null; + } + + public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) { + //Contract.Requires(args != null); + //Contract.Requires(f != null); + bool isEq = f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq); + if (isEq || f.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) { + Contract.Assert(args.Count == 2); + IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]); + IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]); + + // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t + if (isEq && factory.IsTypeConstant(arg0)) { + // swap the arguments + IExpr/*!*/ tmp = arg0; + arg0 = arg1; + arg1 = tmp; + } else if (!factory.IsTypeConstant(arg1)) { + return false; + } + IFunApp typeofExpr = arg0 as IFunApp; + if (typeofExpr != null && + typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) { + Contract.Assert(typeofExpr.Arguments.Count == 1); + if (typeofExpr.Arguments[0] is IVariable) { + // we have a match + return true; + } + } + } + return false; + } + + public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) { + //Contract.Requires(e != null); + Contract.Ensures(Contract.Result<Element>() != null); + IFunApp nary = e as IFunApp; + if (nary != null) { + + bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq); + if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) { + IList/*<IExpr!>*//*!*/ args = nary.Arguments; + Contract.Assert(args != null); + Contract.Assert(args.Count == 2); + IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]); + IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]); + + // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t + if (isEq && factory.IsTypeConstant(arg0)) { + // swap the arguments + IExpr/*!*/ tmp = arg0; + arg0 = arg1; + arg1 = tmp; + } else if (!factory.IsTypeConstant(arg1)) { + return Top; + } + IFunApp typeofExpr = arg0 as IFunApp; + if (typeofExpr != null && + typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) { + Contract.Assert(typeofExpr.Arguments.Count == 1); + if (typeofExpr.Arguments[0] is IVariable) { + // we have a match + return new Elt(isEq ? What.Exact : What.Bounds, arg1); + } + } + } + } + return Top; + } + + } +} |