diff options
| author |  tabarbe <unknown> | 2010-08-26 23:38:33 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-26 23:38:33 +0000 |
| commit | 1188039043117d026e6cdfe13d35aed03880fea7 (patch) | |
| tree | bff79efa62b4ce001422c62c525618c5f235e1b0 /Source/AIFramework/VariableMap/DynamicTypeLattice.cs | |
| parent | 47171ab9f9d31dab0d5e0a4c3c95c763452e9295 (diff) | |
Boogie: AIFramework port part 1/3: Committing new sources.
Diffstat (limited to 'Source/AIFramework/VariableMap/DynamicTypeLattice.cs')
| -rw-r--r-- | Source/AIFramework/VariableMap/DynamicTypeLattice.cs | 793 |
1 files changed, 414 insertions, 379 deletions
diff --git a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs index 8161cb3e..84525a15 100644 --- a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs +++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs @@ -3,171 +3,186 @@ // 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 Microsoft.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;
- invariant what == What.Bottom ==> ty == null && manyBounds == null;
- invariant manyBounds != null ==> what == What.Bounds;
- invariant manyBounds != null ==> forall{int i in (0:manyBounds.Length); manyBounds[i] != null};
-
- public Elt(What what, IExpr ty)
- requires what == What.Bottom ==> ty == null;
- requires what == What.Exact ==> ty != null;
- {
- this.what = what;
- this.ty = ty;
- this.manyBounds = null;
- }
-
- public Elt(IExpr[]! bounds)
- requires forall{int i in (0:bounds.Length); 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)
- 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) {
- assert k != n;
- if (n == 1) {
- assert this.ty == null;
- this.ty = bound;
- } else {
- assume manyBounds != null;
- manyBounds[k] = bound;
- }
- k++;
- }
- }
- assert k == n;
- }
-
- public int BoundsCount
- {
- get
- ensures 0 <= result;
- {
- if (manyBounds != null) {
- return manyBounds.Length;
- } else if (ty != null) {
- return 1;
- } else {
- return 0;
- }
- }
- }
+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
+ }
- [Pure]
- public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
- {
- return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
- }
-
- public override Element! Clone()
- {
- if (this.manyBounds != null)
- return new Elt(this.manyBounds);
- else
- return new Elt(this.what, this.ty);
+ 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;
+ readonly ITypeExprFactory/*!*/ factory;
+ readonly IPropExprFactory/*!*/ propFactory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ Contract.Invariant(propFactory != null);
+ }
- public DynamicTypeLattice(ITypeExprFactory! factory, IPropExprFactory! propFactory)
- {
- this.factory = factory;
- this.propFactory = propFactory;
- // base();
- }
- public override Element! Top
- {
- get { return new Elt(What.Bounds, 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! Bottom
- {
- get { return new Elt(What.Bottom, null); }
- }
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(What.Bounds, null);
+ }
+ }
- public override bool IsTop (Element! element)
- {
- Elt e = (Elt)element;
- return e.what == What.Bounds && e.ty == null && e.manyBounds == null;
- }
+ public override Element/*!*/ Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(What.Bottom, null);
+ }
+ }
- public override bool IsBottom(Element! element)
- {
- Elt e = (Elt)element;
- return e.what == What.Bottom;
- }
+ 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 Element! NontrivialJoin(Element! first, Element! second)
- {
+ 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;
- assert a.what != What.Bottom && b.what != What.Bottom;
+ Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
if (a.what == What.Exact && b.what == What.Exact) {
- assert a.ty != null && b.ty != null;
+ Contract.Assert(a.ty != null && b.ty != null);
if (factory.IsTypeEqual(a.ty, b.ty)) {
return a;
} else {
@@ -176,13 +191,14 @@ namespace Microsoft.AbstractInterpretationFramework }
// The result is going to be a Bounds, since at least one of the operands is a Bounds.
- assert 1 <= a.BoundsCount && 1 <= b.BoundsCount; // a preconditions is that neither operand is Top
+ 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) {
- assert a.ty != null && b.ty != null;
- IExpr! join = factory.JoinTypes(a.ty, b.ty);
+ 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) {
@@ -198,25 +214,26 @@ namespace Microsoft.AbstractInterpretationFramework if (a.ty != null) {
allBounds.Add(a.ty);
} else {
- allBounds.AddRange((!)a.manyBounds);
+ allBounds.AddRange(cce.NonNull(a.manyBounds));
}
int bStart = allBounds.Count;
if (b.ty != null) {
allBounds.Add(b.ty);
} else {
- allBounds.AddRange((!)b.manyBounds);
+ 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 = (IExpr!)allBounds[i];
+ IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);
for (int j = bStart; j < allBounds.Count; j++) {
- IExpr! bBound = (IExpr!)allBounds[j];
+ IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);
- IExpr! join = factory.JoinTypes(aBound, bBound);
+ IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);
+ Contract.Assert(join != null);
int k = 0;
while (k < result.Count) {
- IExpr! r = (IExpr!)result[k];
+ 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
@@ -237,239 +254,257 @@ namespace Microsoft.AbstractInterpretationFramework }
- public override Element! NontrivialMeet(Element! first, Element! second)
- {
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- assert a.what != What.Bottom && b.what != What.Bottom;
-
- if (a.what == What.Exact && b.what == What.Exact) {
- 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;
- }
- 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.
- 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) {
- if (!factory.IsSubType(a.ty, bound)) {
- return Bottom;
- }
- }
- }
- return a;
- }
-
- else {
- // Both operands are Bounds.
- assert a.what == What.Bounds && b.what == What.Bounds;
-
- // Take all the bounds, but prune those bounds that follow from others.
- 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) {
- 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((!)a.manyBounds);
- }
- int bStart = allBounds.Count;
- if (b.ty != null) {
- allBounds.Add(b.ty);
- } else {
- allBounds.AddRange((!)b.manyBounds);
- }
- for (int i = 0; i < bStart; i++) {
- IExpr! aBound = (IExpr!)allBounds[i];
- for (int j = bStart; j < allBounds.Count; j++) {
- IExpr bBound = (IExpr!)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: {}
- }
- assert 1 <= n;
- return new Elt(allBounds, n);
- }
+ 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;
}
- public override Element! Widen (Element! first, Element! second)
- {
- return Join(first,second);
+ } 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;
}
-
- protected override bool AtMost (Element! first, Element! second) // this <= that
- {
- Elt! a = (Elt!)first;
- Elt! b = (Elt!)second;
- assert a.what != What.Bottom && b.what != What.Bottom;
-
- if (a.what == What.Exact && b.what == What.Exact) {
- 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) {
- assert a.ty != null;
- if (b.ty != null) {
- return factory.IsSubType(a.ty, b.ty);
- } else {
- return forall{IExpr! bound in b.manyBounds; factory.IsSubType(a.ty, bound)};
- }
- } else {
- assert a.what == What.Bounds && b.what == What.Bounds;
- assert a.ty != null || a.manyBounds != null; // a precondition is that a is not Top
- 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 forall{IExpr! bound in b.manyBounds; factory.IsSubType(a.ty, bound)};
- } else if (b.ty != null) {
- return exists{IExpr! bound in a.manyBounds; factory.IsSubType(bound, b.ty)};
- } else {
- return forall{IExpr! bBound in b.manyBounds;
- exists{IExpr! aBound in a.manyBounds; factory.IsSubType(aBound, bBound)}};
- }
+ 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);
+ }
}
- public override IExpr! ToPredicate(IVariable! var, Element! element) {
- Elt e = (Elt)element;
- switch (e.what) {
- case What.Bottom:
- return propFactory.False;
- case What.Exact:
- return factory.IsExactlyA(var, (!)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!)((!)e.manyBounds)[0]);
- for (int i = 1; i < e.manyBounds.Length; i++) {
- p = propFactory.And(p, factory.IsA(var, (IExpr!)e.manyBounds[i]));
- }
- return p;
- }
- default:
- assert false;
- throw new System.Exception();
+ // 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);
+ }
- public override IExpr GetFoldExpr(Element! e) {
- // cannot fold into an expression that can be substituted for the variable
- return null;
+ 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 bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args) {
- bool isEq = f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- if (isEq || f.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
- assert args.Count == 2;
- IExpr! arg0 = (IExpr!)args[0];
- IExpr! arg1 = (IExpr!)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)) {
- assert typeofExpr.Arguments.Count == 1;
- if (typeofExpr.Arguments[0] is IVariable) {
- // we have a match
- return true;
- }
- }
+ 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 false;
- }
+ return p;
+ }
+ default: {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ throw new System.Exception();
+ }
+ }
- public override Element! EvaluatePredicate(IExpr! e) {
- IFunApp nary = e as IFunApp;
- if (nary != null) {
+ public override IExpr GetFoldExpr(Element/*!*/ e) {
+ Contract.Requires(e != null);
+ // cannot fold into an expression that can be substituted for the variable
+ return null;
+ }
- bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
- IList/*<IExpr!>*/! args = nary.Arguments;
- assert args.Count == 2;
- IExpr! arg0 = (IExpr!)args[0];
- IExpr! arg1 = (IExpr!)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)) {
- 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;
+ 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;
}
+
+ }
}
|