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* --- .../AIFramework/VariableMap/DynamicTypeLattice.cs | 1022 ++++++++++---------- 1 file changed, 511 insertions(+), 511 deletions(-) (limited to 'Source/AIFramework/VariableMap/DynamicTypeLattice.cs') 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; - - /// - /// 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. - /// - 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; - } - } - - /// - /// Constructs an Elt with "n" bounds, namely the n non-null values of the "bounds" list. - /// - [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()); - if (manyBounds != null) { - return manyBounds.Length; - } else if (ty != null) { - return 1; - } else { - return 0; - } - } - } - - [Pure] - public override System.Collections.Generic.ICollection/*!*/ FreeVariables() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return cce.NonNull(new System.Collections.Generic.List()).AsReadOnly(); - } - - public override Element/*!*/ Clone() { - Contract.Ensures(Contract.Result() != 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() != null); - return new Elt(What.Bounds, null); - } - } - - public override Element/*!*/ Bottom { - get { - Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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/**//*!*/ 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() != 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/**//*!*/ 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; + + /// + /// 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. + /// + 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; + } + } + + /// + /// Constructs an Elt with "n" bounds, namely the n non-null values of the "bounds" list. + /// + [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()); + if (manyBounds != null) { + return manyBounds.Length; + } else if (ty != null) { + return 1; + } else { + return 0; + } + } + } + + [Pure] + public override System.Collections.Generic.ICollection/*!*/ FreeVariables() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return cce.NonNull(new System.Collections.Generic.List()).AsReadOnly(); + } + + public override Element/*!*/ Clone() { + Contract.Ensures(Contract.Result() != 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() != null); + return new Elt(What.Bounds, null); + } + } + + public override Element/*!*/ Bottom { + get { + Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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/**//*!*/ 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() != 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/**//*!*/ 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; + } + + } +} -- cgit v1.2.3