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 | |
| parent | 47171ab9f9d31dab0d5e0a4c3c95c763452e9295 (diff) | |
Boogie: AIFramework port part 1/3: Committing new sources.
Diffstat (limited to 'Source/AIFramework/VariableMap')
| -rw-r--r-- | Source/AIFramework/VariableMap/ConstantAbstraction.cs | 111 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/DynamicTypeLattice.cs | 793 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/Intervals.cs | 884 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/MicroLattice.cs | 42 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/Nullness.cs | 107 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/VariableMapLattice.cs | 370 |
6 files changed, 1294 insertions, 1013 deletions
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.cs b/Source/AIFramework/VariableMap/ConstantAbstraction.cs index 8ba3065f..89a64290 100644 --- a/Source/AIFramework/VariableMap/ConstantAbstraction.cs +++ b/Source/AIFramework/VariableMap/ConstantAbstraction.cs @@ -3,12 +3,12 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
namespace Microsoft.AbstractInterpretationFramework
{
using System.Collections;
using System.Diagnostics;
- using System.Compiler.Analysis;
+ //using System.Compiler.Analysis;
using Microsoft.Basetypes;
/// <summary>
@@ -32,13 +32,13 @@ namespace Microsoft.AbstractInterpretationFramework public BigNum Constant { get { return this.constantValue; } } // only when IsConstant
[Pure]
- public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
- {
- return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ 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()
- {
+ public override Element/*!*/ Clone() {
+Contract.Ensures(Contract.Result<Element>() != null);
if (this.IsConstant)
return new Elt(constantValue);
else
@@ -46,87 +46,109 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- readonly IIntExprFactory! factory;
+ readonly IIntExprFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
- public ConstantLattice(IIntExprFactory! factory)
- {
+
+ public ConstantLattice(IIntExprFactory/*!*/ factory){
+Contract.Requires(factory != null);
this.factory = factory;
// base();
}
- public override Element! Top
- {
- get { return new Elt(Value.Top); }
+ public override Element/*!*/ Top{get{
+Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Top); }
}
- public override Element! Bottom
- {
- get { return new Elt(Value.Bottom); }
+ public override Element/*!*/ Bottom{get{
+Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Bottom); }
}
- public override bool IsTop (Element! element)
- {
+ public override bool IsTop (Element/*!*/ element){
+Contract.Requires(element != null);
Elt e = (Elt)element;
return e.domainValue == Value.Top; }
- public override bool IsBottom (Element! element)
- {
+ public override bool IsBottom (Element/*!*/ element){
+Contract.Requires(element != null);
Elt e = (Elt)element;
return e.domainValue == Value.Bottom; }
- public override Element! NontrivialJoin (Element! first, Element! second)
- {
+ 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;
Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Top;
}
- public override Element! NontrivialMeet (Element! first, Element! second)
- {
+ 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;
Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Bottom;
}
- public override Element! Widen (Element! first, Element! second)
- {
+ 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
+ protected override bool AtMost (Element/*!*/ first, Element/*!*/ second) // this <= that
{
+ Contract.Requires(first!= null);
+ Contract.Requires(second != null);
Elt a = (Elt)first;
Elt b = (Elt)second;
return a.Constant.Equals(b.Constant);
}
- public override IExpr! ToPredicate(IVariable! var, Element! element) {
- return factory.Eq(var, (!)GetFoldExpr(element));
+ public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element){
+Contract.Requires(element != null);
+Contract.Requires(var != null);
+Contract.Ensures(Contract.Result<IExpr>() != null);
+ return factory.Eq(var, cce.NonNull(GetFoldExpr(element)));
}
- public override IExpr GetFoldExpr(Element! element) {
+ public override IExpr GetFoldExpr(Element/*!*/ element){
+Contract.Requires(element != null);
Elt e = (Elt)element;
- assert e.domainValue == Value.Constant;
+ Contract.Assert(e.domainValue == Value.Constant);
return factory.Const(e.constantValue);
}
- public override bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args) {
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args){
+Contract.Requires(args != null);
+Contract.Requires(f != null);
return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
}
- public override Element! EvaluatePredicate(IExpr! e) {
+ public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e){
+Contract.Requires(e != null);
+Contract.Ensures(Contract.Result<Element>() != null);
IFunApp nary = e as IFunApp;
if (nary != null) {
if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
- IList/*<IExpr!>*/! args = nary.Arguments;
- assert args.Count == 2;
- IExpr! arg0 = (IExpr!)args[0];
- IExpr! arg1 = (IExpr!)args[1];
+ 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 "x == const" or "const == x".
try {
@@ -158,8 +180,8 @@ namespace Microsoft.AbstractInterpretationFramework /// This method throws an System.ArithmeticException in the event that folding the
/// constant expression results in an arithmetic overflow or division by zero.
/// </summary>
- private bool Fold(IExpr! expr, out BigNum z)
- {
+ private bool Fold(IExpr/*!*/ expr, out BigNum z){
+Contract.Requires(expr != null);
IFunApp e = expr as IFunApp;
if (e == null) {
z = BigNum.ZERO;
@@ -171,9 +193,10 @@ namespace Microsoft.AbstractInterpretationFramework return true;
} else if (e.FunctionSymbol.Equals(Int.Negate)) {
- IList/*<IExpr!>*/! args = e.Arguments;
- assert args.Count == 1;
- IExpr! arg0 = (IExpr!)args[0];
+ IList/*<IExpr!>*//*!*/ args = e.Arguments;
+ Contract.Assert(args != null);
+ Contract.Assert(args.Count == 1);
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
if (Fold(arg0, out z)) {
z = z.Neg;
@@ -181,8 +204,8 @@ namespace Microsoft.AbstractInterpretationFramework }
} else if (e.Arguments.Count == 2) {
- IExpr! arg0 = (IExpr!)e.Arguments[0];
- IExpr! arg1 = (IExpr!)e.Arguments[1];
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(e.Arguments[0]);
+ IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(e.Arguments[1]);
BigNum z0, z1;
if (Fold(arg0, out z0) && Fold(arg1, out z1)) {
if (e.FunctionSymbol.Equals(Int.Add)) {
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;
}
+
+ }
}
diff --git a/Source/AIFramework/VariableMap/Intervals.cs b/Source/AIFramework/VariableMap/Intervals.cs index f507e020..73a1352f 100644 --- a/Source/AIFramework/VariableMap/Intervals.cs +++ b/Source/AIFramework/VariableMap/Intervals.cs @@ -5,47 +5,48 @@ //-----------------------------------------------------------------------------
using System;
using System.Collections;
-using System.Compiler.Analysis;
+//using System.Compiler.Analysis;
using Microsoft.AbstractInterpretationFramework.Collections;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
/////////////////////////////////////////////////////////////////////////////////
// An implementation of the interval abstract domain
/////////////////////////////////////////////////////////////////////////////////
-namespace Microsoft.AbstractInterpretationFramework
-{
- public class IntervalLattice : MicroLattice
- {
- readonly ILinearExprFactory! factory;
-
- public IntervalLattice(ILinearExprFactory! factory)
- {
+namespace Microsoft.AbstractInterpretationFramework {
+ public class IntervalLattice : MicroLattice {
+ readonly ILinearExprFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
+
+
+ public IntervalLattice(ILinearExprFactory/*!*/ factory) {
+ Contract.Requires(factory != null);
this.factory = factory;
// base();
}
- public override bool UnderstandsBasicArithmetics
- {
- get
- {
+ public override bool UnderstandsBasicArithmetics {
+ get {
return true;
}
}
- public override Element! Top
- {
- get
- {
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+
return IntervalElement.Top;
}
}
-
- public override Element! Bottom
- {
- get
- {
+
+ public override Element/*!*/ Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+
return IntervalElement.Bottom;
}
}
@@ -53,47 +54,51 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// The paramter is the top?
/// </summary>
- public override bool IsTop(Element! element)
- {
- IntervalElement interval = (IntervalElement) element;
-
- return interval.IsTop(); + public override bool IsTop(Element/*!*/ element) {
+ Contract.Requires(element != null);
+ IntervalElement interval = (IntervalElement)element;
+
+ return interval.IsTop();
}
/// <summary>
/// The parameter is the bottom?
/// </summary>
- public override bool IsBottom(Element! element)
- {
- IntervalElement interval = (IntervalElement) element;
-
- return interval.IsBottom(); + public override bool IsBottom(Element/*!*/ element) {
+ Contract.Requires(element != null);
+ IntervalElement interval = (IntervalElement)element;
+
+ return interval.IsBottom();
}
/// <summary>
/// The classic, pointwise, join of intervals
/// </summary>
- public override Element! NontrivialJoin(Element! left, Element! right)
- {
- IntervalElement! leftInterval = (IntervalElement!) left;
- IntervalElement! rightInterval = (IntervalElement) right;
-
+ public override Element/*!*/ NontrivialJoin(Element/*!*/ left, Element/*!*/ right) {
+ Contract.Requires(right != null);
+ Contract.Requires(left != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
+ IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
ExtendedInt inf = ExtendedInt.Inf(leftInterval.Inf, rightInterval.Inf);
ExtendedInt sup = ExtendedInt.Sup(leftInterval.Sup, rightInterval.Sup);
- IntervalElement! join = IntervalElement.Factory(inf, sup);
+ IntervalElement/*!*/ join = IntervalElement.Factory(inf, sup);
- return join; + return join;
}
/// <summary>
/// The classic, pointwise, meet of intervals
/// </summary>
- public override Element! NontrivialMeet(Element! left, Element! right)
- {
- IntervalElement! leftInterval = (IntervalElement!) left;
- IntervalElement! rightInterval = (IntervalElement) right;
-
+ public override Element/*!*/ NontrivialMeet(Element/*!*/ left, Element/*!*/ right) {
+ Contract.Requires(right != null);
+ Contract.Requires(left != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
+ IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
ExtendedInt inf = ExtendedInt.Sup(leftInterval.Inf, rightInterval.Inf);
ExtendedInt sup = ExtendedInt.Inf(leftInterval.Sup, rightInterval.Sup);
@@ -105,11 +110,13 @@ namespace Microsoft.AbstractInterpretationFramework /// The very simple widening of intervals, to be improved with thresholds
/// left is the PREVIOUS value in the iterations and right is the NEW one
/// </summary>
- public override Element! Widen(Element! left, Element! right)
- {
- IntervalElement! prevInterval = (IntervalElement!) left;
- IntervalElement! nextInterval = (IntervalElement!) right;
-
+ public override Element/*!*/ Widen(Element/*!*/ left, Element/*!*/ right) {
+ Contract.Requires(right != null);
+ Contract.Requires(left != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ IntervalElement/*!*/ prevInterval = (IntervalElement/*!*/)cce.NonNull(left);
+ IntervalElement/*!*/ nextInterval = (IntervalElement/*!*/)cce.NonNull(right);
+
ExtendedInt inf = nextInterval.Inf < prevInterval.Inf ? ExtendedInt.MinusInfinity : prevInterval.Inf;
ExtendedInt sup = nextInterval.Sup > prevInterval.Sup ? ExtendedInt.PlusInfinity : prevInterval.Sup;
@@ -122,12 +129,13 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Return true iff the interval left is containted in right
/// </summary>
- protected override bool AtMost(Element! left, Element! right)
- {
- IntervalElement! leftInterval = (IntervalElement!) left;
- IntervalElement! rightInterval = (IntervalElement!) right;
+ protected override bool AtMost(Element/*!*/ left, Element/*!*/ right) {
+ Contract.Requires(right != null);
+ Contract.Requires(left != null);
+ IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
+ IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
- if(leftInterval.IsBottom() || rightInterval.IsTop())
+ if (leftInterval.IsBottom() || rightInterval.IsTop())
return true;
return rightInterval.Inf <= leftInterval.Inf && leftInterval.Sup <= rightInterval.Sup;
@@ -136,17 +144,19 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Return just null
/// </summary>
- public override IExpr GetFoldExpr(Element! element)
- {
+ public override IExpr GetFoldExpr(Element/*!*/ element) {
+ Contract.Requires(element != null);
return null;
- }
+ }
/// <summary>
/// return a predicate inf "\leq x and x "\leq" sup (if inf [or sup] is not oo)
/// </summary>
- public override IExpr! ToPredicate(IVariable! var, Element! element)
- {
- IntervalElement! interval = (IntervalElement!) element; + public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element){
+Contract.Requires(element != null);
+Contract.Requires(var != null);
+Contract.Ensures(Contract.Result<IExpr>() != null);
+IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element); IExpr lowerBound = null;
IExpr upperBound = null; @@ -171,38 +181,41 @@ namespace Microsoft.AbstractInterpretationFramework return upperBound; else // If we reach this point, both lowerBound and upperBound are null, i.e. we have no bounds on var, so we return simply true...
return this.factory.True;
- }
+ }
/// <summary>
/// For the moment consider just equalities. Other case must be considered
/// </summary>
- public override bool Understands(IFunctionSymbol! f, IList /*<IExpr*/ ! args)
- {
- return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq); + public override bool Understands(IFunctionSymbol/*!*/ f, IList /*<IExpr*//*!*/ args) {
+ Contract.Requires(args != null);
+ Contract.Requires(f != null);
+ return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
}
/// <summary>
/// Evaluate the predicate passed as input according the semantics of intervals
/// </summary>
- public override Element! EvaluatePredicate(IExpr! pred)
- {
+ public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ pred) {
+ Contract.Requires(pred != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
return this.EvaluatePredicateWithState(pred, null);
}
-
+
/// <summary>
/// Evaluate the predicate passed as input according the semantics of intervals and the given state.
/// Right now just basic arithmetic operations are supported. A future extension may consider an implementation of boolean predicates
/// </summary>
- public override Element! EvaluatePredicateWithState(IExpr! pred, IFunctionalMap/* Var -> Element */ state)
- {
+ public override Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ pred, IFunctionalMap/* Var -> Element */ state){
+Contract.Requires(pred != null);
+Contract.Ensures(Contract.Result<Element>() != null);
if(pred is IFunApp)
{
IFunApp fun = (IFunApp) pred;
if(fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
{
- IExpr! leftArg = (IExpr!) fun.Arguments[0];
- IExpr! rightArg = (IExpr!) fun.Arguments[1];
+ IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
if (leftArg is IVariable) {
return Eval(rightArg, state);
} else if (rightArg is IVariable) {
@@ -217,10 +230,11 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Evaluate the expression (that is assured to be an arithmetic expression, in the state passed as a parameter
/// </summary>
- private IntervalElement! Eval(IExpr! exp, IFunctionalMap/* Var -> Element */ state)
- {
+ private IntervalElement/*!*/ Eval(IExpr/*!*/ exp, IFunctionalMap/* Var -> Element */ state) {
+Contract.Requires((exp != null));
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
- IntervalElement! retVal = (IntervalElement!) Top;
+ IntervalElement/*!*/ retVal = (IntervalElement/*!*/)cce.NonNull(Top);
// Eval the expression by structural induction
@@ -248,19 +262,23 @@ namespace Microsoft.AbstractInterpretationFramework }
else if(fun.FunctionSymbol.Equals(Int.Negate)) // An unary minus
{
- IExpr! arg = (IExpr!) fun.Arguments[0];
- IntervalElement! argEval = Eval(arg, state);
- IntervalElement! zero = IntervalElement.Factory(BigNum.ZERO);
+ IExpr/*!*/ arg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IntervalElement/*!*/ argEval = Eval(arg, state);
+ Contract.Assert(argEval != null);
+ IntervalElement/*!*/ zero = IntervalElement.Factory(BigNum.ZERO);
+ Contract.Assert(zero != null);
retVal = zero - argEval;
}
else if(fun.Arguments.Count == 2)
{
- IExpr! left = (IExpr!) fun.Arguments[0];
- IExpr! right = (IExpr!) fun.Arguments[1];
+ IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
- IntervalElement! leftVal = Eval(left, state);
- IntervalElement! rightVal = Eval(right, state);
+ IntervalElement/*!*/ leftVal = Eval(left, state);
+ Contract.Assert(leftVal != null);
+ IntervalElement/*!*/ rightVal = Eval(right, state);
+ Contract.Assert(rightVal != null);
if(fun.FunctionSymbol.Equals(Int.Add))
retVal = leftVal + rightVal;
@@ -281,165 +299,199 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Inner class standing for an interval on integers, possibly unbounded
/// </summary>
- private class IntervalElement : Element
- {
- protected static readonly IntervalElement! TopInterval = new IntervalElement(new MinusInfinity(), new PlusInfinity()); // Top = [-oo , +oo]
- protected static readonly IntervalElement! BottomInterval = new IntervalElement(new PlusInfinity(), new MinusInfinity()); // Bottom = [+oo, -oo]
+ private class IntervalElement : Element {
+ protected static readonly IntervalElement/*!*/ TopInterval = new IntervalElement(new MinusInfinity(), new PlusInfinity()); // Top = [-oo , +oo]
+ protected static readonly IntervalElement/*!*/ BottomInterval = new IntervalElement(new PlusInfinity(), new MinusInfinity()); // Bottom = [+oo, -oo]
+
+ private readonly ExtendedInt/*!*/ inf;
+ private readonly ExtendedInt/*!*/ sup;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(inf != null);
+ Contract.Invariant(sup != null);
+ }
- private readonly ExtendedInt! inf;
- private readonly ExtendedInt! sup;
-
- public ExtendedInt! Inf
- {
- get
- {
- return inf;
- }
- }
-
- public ExtendedInt! Sup
- {
- get
- {
- return sup;
- }
- }
-
- // Construct the inteval [val, val]
- protected IntervalElement(BigNum val)
- {
- this.inf = this.sup = ExtendedInt.Factory(val);
- // base();
- }
+ public ExtendedInt/*!*/ Inf {
+ get {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- // Construct the interval [inf, sup]
- protected IntervalElement(BigNum infInt, BigNum supInt)
- {
- this.inf = ExtendedInt.Factory(infInt);
- this.sup = ExtendedInt.Factory(supInt);
- // base(); // to please the compiler...
- }
-
- protected IntervalElement(ExtendedInt! inf, ExtendedInt! sup)
- {
- this.inf = inf;
- this.sup = sup;
- // base();
+ return inf;
}
+ }
- // Construct an Interval
- public static IntervalElement! Factory(ExtendedInt! inf, ExtendedInt! sup)
- {
- if(inf is MinusInfinity && sup is PlusInfinity)
- return Top;
- if(inf > sup)
- return Bottom;
- // otherwise...
- return new IntervalElement(inf, sup);
- }
+ public ExtendedInt/*!*/ Sup {
+ get {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- public static IntervalElement! Factory(BigNum i)
- {
- return new IntervalElement(i);
+ return sup;
}
+ }
- public static IntervalElement! Factory(BigNum inf, BigNum sup)
- {
- ExtendedInt! i = ExtendedInt.Factory(inf);
- ExtendedInt! s = ExtendedInt.Factory(sup);
+ // Construct the inteval [val, val]
+ protected IntervalElement(BigNum val) {
+ this.inf = this.sup = ExtendedInt.Factory(val);
+ // base();
+ }
+
+ // Construct the interval [inf, sup]
+ protected IntervalElement(BigNum infInt, BigNum supInt) {
+ this.inf = ExtendedInt.Factory(infInt);
+ this.sup = ExtendedInt.Factory(supInt);
+ // base(); // to please the compiler...
+ }
+
+ protected IntervalElement(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
+ this.inf = inf;
+ this.sup = sup;
+ // base();
+ }
+
+ // Construct an Interval
+ public static IntervalElement/*!*/ Factory(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires((sup != null));
+Contract.Requires((inf != null));
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ if (inf is MinusInfinity && sup is PlusInfinity)
+ return Top;
+ if (inf > sup)
+ return Bottom;
+ // otherwise...
+ return new IntervalElement(inf, sup);
+ }
+
+ public static IntervalElement/*!*/ Factory(BigNum i) {
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ return new IntervalElement(i);
+ }
+
+ public static IntervalElement/*!*/ Factory(BigNum inf, BigNum sup) {
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ i = ExtendedInt.Factory(inf);
+ ExtendedInt/*!*/ s = ExtendedInt.Factory(sup);
return Factory(i, s);
}
- static public IntervalElement! Top
- {
- get
- {
- return TopInterval;
- }
- }
+ static public IntervalElement/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
- static public IntervalElement! Bottom
- {
- get
- {
- return BottomInterval;
- }
+ return TopInterval;
}
+ }
- public bool IsTop()
- {
- return this.inf is MinusInfinity && this.sup is PlusInfinity;
- }
+ static public IntervalElement/*!*/ Bottom {
+ get {
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
- public bool IsBottom()
- {
- return this.inf > this.sup;
+ return BottomInterval;
}
+ }
- #region Below are the arithmetic operations lifted to intervals
+ public bool IsTop() {
+ return this.inf is MinusInfinity && this.sup is PlusInfinity;
+ }
- // Addition
- public static IntervalElement! operator+(IntervalElement! a, IntervalElement! b)
- {
- ExtendedInt! inf = a.inf + b.inf;
- ExtendedInt! sup = a.sup + b.sup;
+ public bool IsBottom() {
+ return this.inf > this.sup;
+ }
+
+ #region Below are the arithmetic operations lifted to intervals
+
+ // Addition
+ public static IntervalElement/*!*/ operator +(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ inf = a.inf + b.inf;
+ Contract.Assert(inf != null);
+ ExtendedInt/*!*/ sup = a.sup + b.sup;
+ Contract.Assert(sup != null);
return Factory(inf, sup); }
- // Subtraction
- public static IntervalElement! operator-(IntervalElement! a, IntervalElement! b)
- {
- ExtendedInt! inf = a.inf - b.sup;
- ExtendedInt! sup = a.sup - b.inf;
-
- IntervalElement! sub = Factory(inf, sup); + // Subtraction
+ public static IntervalElement/*!*/ operator -(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ inf = a.inf - b.sup;
+ Contract.Assert(inf != null);
+
+ ExtendedInt/*!*/ sup = a.sup - b.inf;
+Contract.Assert(sup != null);
+IntervalElement/*!*/ sub = Factory(inf, sup);
+Contract.Assert(sub != null); return sub;
- }
-
- // Multiplication
- public static IntervalElement! operator*(IntervalElement! a, IntervalElement! b)
- {
- ExtendedInt! infinf = a.inf * b.inf;
- ExtendedInt! infsup = a.inf * b.sup;
- ExtendedInt! supinf = a.sup * b.inf;
- ExtendedInt! supsup = a.sup * b.sup;
+ }
- ExtendedInt! inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
- ExtendedInt! sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ // Multiplication
+ public static IntervalElement/*!*/ operator *(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ infinf = a.inf * b.inf;
+ Contract.Assert(infinf != null);
+ ExtendedInt/*!*/ infsup = a.inf * b.sup;
+ Contract.Assert(infsup != null);
+ ExtendedInt/*!*/ supinf = a.sup * b.inf;
+ Contract.Assert(supinf != null);
+ ExtendedInt/*!*/ supsup = a.sup * b.sup;
+ Contract.Assert(supsup != null);
+
+ ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ Contract.Assert(inf != null);
+ ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ Contract.Assert(sup != null);
return Factory(inf, sup);
}
- // Division
- public static IntervalElement! operator/(IntervalElement! a, IntervalElement! b)
- {
+ // Division
+ public static IntervalElement/*!*/ operator /(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
if(b.inf.IsZero && b.sup.IsZero) // Check division by zero
return IntervalElement.Top;
- ExtendedInt! infinf = a.inf / b.inf;
- ExtendedInt! infsup = a.inf / b.sup;
- ExtendedInt! supinf = a.sup / b.inf;
- ExtendedInt! supsup = a.sup / b.sup;
+ ExtendedInt/*!*/ infinf = a.inf / b.inf;
+ Contract.Assert(infinf != null);
+ ExtendedInt/*!*/ infsup = a.inf / b.sup;
+ Contract.Assert(infsup != null);
+ ExtendedInt/*!*/ supinf = a.sup / b.inf;
+ Contract.Assert(supinf != null);
+ ExtendedInt/*!*/ supsup = a.sup / b.sup;
+ Contract.Assert(supsup != null);
- ExtendedInt! inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
- ExtendedInt! sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ Contract.Assert(inf != null);
+ ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ Contract.Assert(sup != null);
return Factory(inf, sup);
}
- // Division
- public static IntervalElement! operator%(IntervalElement! a, IntervalElement! b)
- {
+ // Division
+ public static IntervalElement/*!*/ operator %(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<IntervalElement>() != null);
if(b.inf.IsZero && b.sup.IsZero) // Check division by zero
return IntervalElement.Top;
- ExtendedInt! infinf = a.inf % b.inf;
- ExtendedInt! infsup = a.inf % b.sup;
- ExtendedInt! supinf = a.sup % b.inf;
- ExtendedInt! supsup = a.sup % b.sup;
+ ExtendedInt/*!*/ infinf = a.inf % b.inf;
+ Contract.Assert(infinf != null);
+ ExtendedInt/*!*/ infsup = a.inf % b.sup;
+ Contract.Assert(infsup != null);
+ ExtendedInt/*!*/ supinf = a.sup % b.inf;
+ Contract.Assert(supinf != null);
+ ExtendedInt/*!*/ supsup = a.sup % b.sup;
+ Contract.Assert(supsup != null);
ExtendedInt inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
ExtendedInt sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
@@ -447,67 +499,72 @@ namespace Microsoft.AbstractInterpretationFramework return Factory(inf, sup);
}
- #endregion
+ #endregion
- #region Overriden methods
+ #region Overriden methods
- public override Element! Clone()
- {
- // Real copying should not be needed because intervals are immutable?
- return this;
- /*
- int valInf = this.inf.Value;
- int valSup = this.sup.Value;
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ // Real copying should not be needed because intervals are immutable?
+ return this;
+ /*
+ int valInf = this.inf.Value;
+ int valSup = this.sup.Value;
- ExtendedInt clonedInf = ExtendedInt.Factory(valInf);
- ExtendedInt clonedSup = ExtendedInt.Factory(valSup);
+ ExtendedInt clonedInf = ExtendedInt.Factory(valInf);
+ ExtendedInt clonedSup = ExtendedInt.Factory(valSup);
- return Factory(clonedInf, clonedSup);
- */
- }
+ return Factory(clonedInf, clonedSup);
+ */
+ }
- [Pure]
- public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
- {
- return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ [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();
}
- [Pure]
- public override string! ToString()
- {
- return "[" + this.inf + ", " + this.sup + "]";
- }
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return "[" + this.inf + ", " + this.sup + "]";
+ }
- #endregion
+ #endregion
}
-}
+ }
+
-
/// The interface for an extended integer
- abstract class ExtendedInt
- {
- private static readonly PlusInfinity! cachedPlusInf = new PlusInfinity();
- private static readonly MinusInfinity! cachedMinusInf = new MinusInfinity();
-
- static public ExtendedInt! PlusInfinity
- {
- get
- {
+ ///
+ [ContractClass(typeof(ExtendedIntContracts))]
+ abstract class ExtendedInt {
+ private static readonly PlusInfinity/*!*/ cachedPlusInf = new PlusInfinity();
+ private static readonly MinusInfinity/*!*/ cachedMinusInf = new MinusInfinity();
+
+ static public ExtendedInt/*!*/ PlusInfinity {
+ get {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+
return cachedPlusInf;
}
}
- static public ExtendedInt! MinusInfinity
- {
- get
- {
+ static public ExtendedInt/*!*/ MinusInfinity {
+ get {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+
return cachedMinusInf;
- }
+ }
}
- public abstract BigNum Value { get; }
+ public abstract BigNum Value {
+ get;
+ }
- public abstract int Signum { get; }
+ public abstract int Signum {
+ get;
+ }
public bool IsZero {
get {
@@ -531,158 +588,188 @@ namespace Microsoft.AbstractInterpretationFramework #region Below are the extensions of arithmetic operations on extended integers
// Addition
- public static ExtendedInt! operator+(ExtendedInt! a, ExtendedInt! b)
- {
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return b;
- } else {
- return ExtendedInt.Factory(a.Value + b.Value);
- }
+ public static ExtendedInt/*!*/ operator +(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return b;
+ } else {
+ return ExtendedInt.Factory(a.Value + b.Value);
+ }
}
// Subtraction
- public static ExtendedInt! operator-(ExtendedInt! a, ExtendedInt! b)
- {
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return UnaryMinus(b);
- } else {
- return ExtendedInt.Factory(a.Value - b.Value);
- }
- }
-
+ public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return UnaryMinus(b);
+ } else {
+ return ExtendedInt.Factory(a.Value - b.Value);
+ }
+ }
+
// Unary minus
- public static ExtendedInt! operator-(ExtendedInt! a)
- {
+ public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a) {
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
// BUGBUG: Some compiler error prevents the unary minus operator from being used
return UnaryMinus(a);
}
// Unary minus
- public static ExtendedInt! UnaryMinus(ExtendedInt! a)
- {
- if(a is PlusInfinity)
+ public static ExtendedInt/*!*/ UnaryMinus(ExtendedInt/*!*/ a) {
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (a is PlusInfinity)
return cachedMinusInf;
- if(a is MinusInfinity)
+ if (a is MinusInfinity)
return cachedPlusInf;
else // a is a PureInteger
return new PureInteger(-a.Value);
}
// Multiplication
- public static ExtendedInt! operator*(ExtendedInt! a, ExtendedInt! b)
- {
- if (a.IsZero) {
+ public static ExtendedInt/*!*/ operator *(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (a.IsZero) {
+ return a;
+ } else if (b.IsZero) {
+ return b;
+ } else if (a is InfinitaryInt) {
+ if (b.IsPositive) {
return a;
- } else if (b.IsZero) {
- return b;
- } else if (a is InfinitaryInt) {
- if (b.IsPositive) {
- return a;
- } else {
- return UnaryMinus(a);
- }
- } else if (b is InfinitaryInt) {
- if (a.IsPositive) {
- return b;
- } else {
- return UnaryMinus(b);
- }
} else {
- return ExtendedInt.Factory(a.Value * b.Value);
+ return UnaryMinus(a);
}
- }
-
- // Division
- public static ExtendedInt! operator/(ExtendedInt! a, ExtendedInt! b)
- {
- if(b.IsZero)
- {
- return a.IsPositive? (ExtendedInt) cachedPlusInf : cachedMinusInf;
- }
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
+ } else if (b is InfinitaryInt) {
+ if (a.IsPositive) {
return b;
} else {
- return ExtendedInt.Factory(a.Value / b.Value);
+ return UnaryMinus(b);
}
+ } else {
+ return ExtendedInt.Factory(a.Value * b.Value);
+ }
+ }
+
+ // Division
+ public static ExtendedInt/*!*/ operator /(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (b.IsZero) {
+ return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
+ }
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return b;
+ } else {
+ return ExtendedInt.Factory(a.Value / b.Value);
+ }
}
// Modulo
- public static ExtendedInt! operator%(ExtendedInt! a, ExtendedInt! b)
- {
- if(b.IsZero)
- {
- return a.IsPositive? (ExtendedInt) cachedPlusInf : cachedMinusInf;
- }
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return b;
- } else {
- return ExtendedInt.Factory(a.Value % b.Value);
- }
+ public static ExtendedInt/*!*/ operator %(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (b.IsZero) {
+ return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
+ }
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return b;
+ } else {
+ return ExtendedInt.Factory(a.Value % b.Value);
+ }
}
#endregion
#region Inf and Sup operations
- public abstract int CompareTo(ExtendedInt! that);
+ public abstract int CompareTo(ExtendedInt/*!*/ that);
- public static bool operator<(ExtendedInt! inf, ExtendedInt! sup)
- {
+ public static bool operator <(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
return inf.CompareTo(sup) < 0;
}
- public static bool operator>(ExtendedInt! inf, ExtendedInt! sup)
- {
+ public static bool operator >(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
return inf.CompareTo(sup) > 0;
}
- public static bool operator<=(ExtendedInt! inf, ExtendedInt! sup)
- {
+ public static bool operator <=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
return inf.CompareTo(sup) <= 0;
}
- public static bool operator>=(ExtendedInt! inf, ExtendedInt! sup)
- requires inf != null && sup != null;
- {
+ public static bool operator >=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
+ Contract.Requires(inf != null && sup != null);
return inf.CompareTo(sup) >= 0;
}
- public static ExtendedInt! Inf(ExtendedInt! inf, ExtendedInt! sup)
- {
- if(inf < sup)
+ public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (inf < sup)
return inf;
else
return sup;
}
- public static ExtendedInt! Inf(ExtendedInt! a, ExtendedInt! b, ExtendedInt! c, ExtendedInt! d)
- {
- ExtendedInt! infab = Inf(a,b);
- ExtendedInt! infcd = Inf(c,d);
+ public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d){
+Contract.Requires(d != null);
+Contract.Requires(c != null);
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ ExtendedInt/*!*/ infab = Inf(a,b);
+ Contract.Assert(infab != null);
+ ExtendedInt/*!*/ infcd = Inf(c, d);
+ Contract.Assert(infcd != null);
return Inf(infab, infcd);
}
-
- public static ExtendedInt! Sup(ExtendedInt! inf, ExtendedInt! sup)
- {
- if(inf > sup)
+
+ public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
+ Contract.Requires(sup != null);
+ Contract.Requires(inf != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ if (inf > sup)
return inf;
else
return sup;
- }
+ }
- public static ExtendedInt! Sup(ExtendedInt! a, ExtendedInt! b, ExtendedInt! c, ExtendedInt! d)
- {
- ExtendedInt! supab = Sup(a,b);
- ExtendedInt! supcd = Sup(c,d);
+ public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d){
+Contract.Requires(d != null);
+Contract.Requires(c != null);
+Contract.Requires(b != null);
+Contract.Requires(a != null);
+Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ ExtendedInt/*!*/ supab = Sup(a,b);
+ Contract.Assert(supab != null);
+ ExtendedInt/*!*/ supcd = Sup(c, d);
+ Contract.Assert(supcd != null);
return Sup(supab, supcd);
}
@@ -690,101 +777,104 @@ namespace Microsoft.AbstractInterpretationFramework #endregion
// Return the ExtendedInt corresponding to the value
- public static ExtendedInt! Factory(BigNum val)
- {
+ public static ExtendedInt/*!*/ Factory(BigNum val) {
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
return new PureInteger(val);
}
- }
+ }
+ [ContractClassFor(typeof(ExtendedInt))]
+ abstract class ExtendedIntContracts : ExtendedInt {
+ public override int CompareTo(ExtendedInt that) {
+ Contract.Requires(that != null);
+ throw new NotImplementedException();
+ }
+ }
// Stands for a normal (finite) integer x
- class PureInteger : ExtendedInt
- {
- public PureInteger(BigNum i)
- {
+ class PureInteger : ExtendedInt {
+ public PureInteger(BigNum i) {
this.val = i;
}
[Pure]
- public override string! ToString()
- {
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return this.Value.ToString();
}
private BigNum val;
public override BigNum Value {
- get
- {
+ get {
return this.val;
}
}
public override int Signum {
- get {
- return val.Signum;
- }
- }
-
- public override int CompareTo(ExtendedInt! that) {
- if (that is PlusInfinity)
- return -1;
- else if (that is PureInteger)
- return this.Value.CompareTo(that.Value);
- else // then that is a MinusInfinity
- return 1;
- }
+ get {
+ return val.Signum;
+ }
+ }
+
+ public override int CompareTo(ExtendedInt/*!*/ that) {
+ Contract.Requires(that != null);
+ if (that is PlusInfinity)
+ return -1;
+ else if (that is PureInteger)
+ return this.Value.CompareTo(that.Value);
+ else // then that is a MinusInfinity
+ return 1;
+ }
}
- abstract class InfinitaryInt : ExtendedInt
- {
- public override BigNum Value
- {
+ abstract class InfinitaryInt : ExtendedInt {
+ public override BigNum Value {
get {
throw new InvalidOperationException();
}
}
}
- class PlusInfinity : InfinitaryInt
- {
+ class PlusInfinity : InfinitaryInt {
[Pure]
- public override string! ToString()
- {
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return "+oo";
}
public override int Signum {
- get {
- return 1;
- }
- }
-
- public override int CompareTo(ExtendedInt! that) {
- if (that is PlusInfinity)
- return 0;
- else
- return 1;
- }
+ get {
+ return 1;
+ }
+ }
+
+ public override int CompareTo(ExtendedInt/*!*/ that) {
+ Contract.Requires(that != null);
+ if (that is PlusInfinity)
+ return 0;
+ else
+ return 1;
+ }
}
- class MinusInfinity : InfinitaryInt
- {
+ class MinusInfinity : InfinitaryInt {
[Pure]
- public override string! ToString()
- {
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return "-oo";
}
public override int Signum {
- get {
- return -1;
- }
- }
-
- public override int CompareTo(ExtendedInt! that) {
- if (that is MinusInfinity)
- return 0;
- else
- return -1;
- }
+ get {
+ return -1;
+ }
+ }
+
+ public override int CompareTo(ExtendedInt/*!*/ that) {
+ Contract.Requires(that != null);
+ if (that is MinusInfinity)
+ return 0;
+ else
+ return -1;
+ }
}
}
diff --git a/Source/AIFramework/VariableMap/MicroLattice.cs b/Source/AIFramework/VariableMap/MicroLattice.cs index d38a37c0..ef98f8f7 100644 --- a/Source/AIFramework/VariableMap/MicroLattice.cs +++ b/Source/AIFramework/VariableMap/MicroLattice.cs @@ -5,22 +5,24 @@ //-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework
{
- using Microsoft.Contracts;
+ using System.Diagnostics.Contracts;
using System.Collections;
using System.Diagnostics;
- using System.Compiler;
+ //using System.Compiler;
using Microsoft.AbstractInterpretationFramework.Collections;
/// <summary>
/// Interface for a lattice that works on a per-variable basis.
/// </summary>
+ ///
+ [ContractClass(typeof(MicroLatticeContracts))]
public abstract class MicroLattice : MathematicalLattice
{
/// <summary>
/// Returns the predicate on the given variable for the given
/// lattice element.
/// </summary>
- public abstract IExpr! ToPredicate(IVariable! v, Element! e);
+ public abstract IExpr/*!*/ ToPredicate(IVariable/*!*/ v, Element/*!*/ e);
/* requires !e.IsBottom && !e.IsTop; */
/// <summary>
@@ -39,7 +41,7 @@ namespace Microsoft.AbstractInterpretationFramework /// <param name="f">The function symbol.</param>
/// <param name="args">The argument context.</param>
/// <returns>True if it may understand f, false if it does not understand f.</returns>
- public abstract bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args);
+ public abstract bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args);
/// <summary>
/// Set this property to true if the implemented MicroLattice can handle basic arithmetic.
@@ -56,15 +58,16 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="e">The predicate that is assumed to contain 1 variable.</param>
/// <returns>The most precise lattice element that is implied by the predicate.</returns>
- public abstract Element! EvaluatePredicate(IExpr! e);
+ public abstract Element/*!*/ EvaluatePredicate(IExpr/*!*/ e);
/// <summary>
/// Evaluate the predicate e and yield an overapproximation of the predicate under the state that is passed as a parameter
/// Note that unless the subclass implement it, the default behavior is to evaluate the predicate stateless, that implies that it
/// is evaluated in any possible context, i.e. it is an upper approximation
/// </summary>
- public virtual Element! EvaluatePredicateWithState(IExpr! e, IFunctionalMap state)
- {
+ public virtual Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ e, IFunctionalMap state){
+Contract.Requires(e != null);
+Contract.Ensures(Contract.Result<Element>() != null);
return EvaluatePredicate(e);
}
@@ -74,6 +77,29 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="e">A lattice element.</param>
/// <returns>The null value if no such expression can be given.</returns>
- public abstract IExpr GetFoldExpr(Element! e);
+ public abstract IExpr GetFoldExpr(Element/*!*/ e);
+ }
+ [ContractClassFor(typeof(MicroLattice))]
+ public abstract class MicroLatticeContracts : MicroLattice {
+ public override IExpr ToPredicate(IVariable v, MathematicalLattice.Element e) {
+ Contract.Requires(v != null);
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ throw new System.NotImplementedException();
+ }
+ public override bool Understands(IFunctionSymbol f, IList args) {
+ Contract.Requires(f != null);
+ Contract.Requires(args != null);
+ throw new System.NotImplementedException();
+ }
+ public override Element EvaluatePredicate(IExpr e) {
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ throw new System.NotImplementedException();
+ }
+ public override IExpr GetFoldExpr(MathematicalLattice.Element e) {
+ Contract.Requires(e != null);
+ throw new System.NotImplementedException();
+ }
}
}
\ No newline at end of file diff --git a/Source/AIFramework/VariableMap/Nullness.cs b/Source/AIFramework/VariableMap/Nullness.cs index bbd1da70..9eac6b29 100644 --- a/Source/AIFramework/VariableMap/Nullness.cs +++ b/Source/AIFramework/VariableMap/Nullness.cs @@ -3,18 +3,24 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
namespace Microsoft.AbstractInterpretationFramework
{
using System.Collections;
using System.Diagnostics;
- using System.Compiler.Analysis;
+ //using System.Compiler.Analysis;
public class NullnessLattice : MicroLattice
{
- readonly INullnessFactory! factory;
+ readonly INullnessFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
- public NullnessLattice(INullnessFactory! factory) {
+
+ public NullnessLattice(INullnessFactory/*!*/ factory){
+Contract.Requires(factory != null);
this.factory = factory;
// base();
}
@@ -28,77 +34,92 @@ namespace Microsoft.AbstractInterpretationFramework public Elt (Value v) { this.value = v; }
[Pure]
- public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
- {
- return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ 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()
- {
+ public override Element/*!*/ Clone() {
+Contract.Ensures(Contract.Result<Element>() != null);
return new Elt(this.value);
}
}
- public override Element! Top
+ public override Element/*!*/ Top
{
- get { return new Elt(Value.MayBeNull); }
+ get {Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.MayBeNull); }
}
- public override Element! Bottom
+ public override Element/*!*/ Bottom
{
- get { return new Elt(Value.Bottom); }
+ get {Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Bottom); }
}
- public static Element! Null
+ public static Element/*!*/ Null
{
- get { return new Elt(Value.Null); }
+ get {Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Null); }
}
- public static Element! NotNull
+ public static Element/*!*/ NotNull
{
- get { return new Elt(Value.NotNull); }
+ get {Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.NotNull); }
}
- public override bool IsTop (Element! element)
- {
+ public override bool IsTop (Element/*!*/ element){
+Contract.Requires(element != null);
Elt e = (Elt) element;
return e.value == Value.MayBeNull;
}
- public override bool IsBottom (Element! element)
- {
+ public override bool IsBottom (Element/*!*/ element){
+Contract.Requires(element != null);
Elt e = (Elt) element;
return e.value == Value.Bottom;
}
- public override Lattice.Element! NontrivialJoin (Element! first, Element! second)
- {
+ public override Lattice.Element/*!*/ NontrivialJoin (Element/*!*/ first, Element/*!*/ second){
+Contract.Requires(second != null);
+Contract.Requires(first != null);
+Contract.Ensures(Contract.Result<Lattice.Element>() != null);
Elt a = (Elt) first;
Elt b = (Elt) second;
return (a.value == b.value) ? a : (Elt)Top;
}
- public override Lattice.Element! NontrivialMeet (Element! first, Element! second)
- {
+ public override Lattice.Element/*!*/ NontrivialMeet (Element/*!*/ first, Element/*!*/ second){
+Contract.Requires(second != null);
+Contract.Requires(first != null);
+Contract.Ensures(Contract.Result<Lattice.Element>() != null);
Elt a = (Elt) first;
Elt b = (Elt) second;
return (a.value == b.value) ? a : (Elt)Bottom;
}
- public override Element! Widen (Element! first, Element! second)
- {
+ 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
+ protected override bool AtMost (Element/*!*/ first, Element/*!*/ second) // this <= that
{
+Contract.Requires(first != null);
+Contract.Requires(second != null);
Elt a = (Elt) first;
Elt b = (Elt) second;
return a.value == b.value;
}
- public override IExpr! ToPredicate(IVariable! var, Element! element) {
+ 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;
if (e.value == Value.NotNull)
@@ -109,11 +130,12 @@ namespace Microsoft.AbstractInterpretationFramework {
return factory.Eq(var, factory.Null);
}
- assert false;
+ {Contract.Assert(false);throw new cce.UnreachableException();}
throw new System.Exception();
}
- public override IExpr GetFoldExpr(Element! e) {
+ public override IExpr GetFoldExpr(Element/*!*/ e){
+Contract.Requires(e != null);
Elt elt = (Elt)e;
if (elt.value == Value.Null) {
return factory.Null;
@@ -123,13 +145,15 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- public override bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args) {
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args){
+Contract.Requires(args != null);
+Contract.Requires(f != null);
if (f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq) ||
f.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
- assert args.Count == 2;
- IExpr! arg0 = (IExpr!)args[0];
- IExpr! arg1 = (IExpr!)args[1];
+ Contract.Assert(args.Count == 2);
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+ IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
// Look for "x OP null" or "null OP x" where OP is "==" or "!=".
if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
@@ -141,15 +165,18 @@ namespace Microsoft.AbstractInterpretationFramework return false;
}
- public override Element! EvaluatePredicate(IExpr! e) {
+ 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.Neq)) {
- IList/*<IExpr!>*/! args = nary.Arguments;
- assert args.Count == 2;
- IExpr! arg0 = (IExpr!)args[0];
- IExpr! arg1 = (IExpr!)args[1];
+ 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 "x OP null" or "null OP x" where OP is "==" or "!=".
IVariable var = null;
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs index ab030b59..e0b9ac04 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.cs +++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs @@ -5,7 +5,7 @@ //-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework
{
- using Microsoft.Contracts;
+ using System.Diagnostics.Contracts;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
@@ -47,20 +47,21 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- public override Element! Clone()
- {
+ public override Element/*!*/ Clone() {
+Contract.Ensures(Contract.Result<Element>() != null);
return new Elt(this.constraints);
}
[Pure]
- public override string! ToString()
- {
+ public override string/*!*/ ToString() {
+Contract.Ensures(Contract.Result<string>() != null);
if (constraints == null) {
return "<bottom>";
}
string s = "[";
string sep = "";
- foreach (IVariable! v in (!)constraints.Keys) {
+ foreach(IVariable/*!*/ v in cce.NonNull(constraints.Keys)){
+Contract.Assert(v != null);
Element m = (Element)constraints[v];
s += sep + v.Name + " -> " + m;
sep = ", ";
@@ -68,8 +69,15 @@ namespace Microsoft.AbstractInterpretationFramework return s + "]";
}
- public static Elt! Top = new Elt(true);
- public static Elt! Bottom = new Elt(false);
+ public static Elt/*!*/ Top = new Elt(true);
+ public static Elt/*!*/ Bottom = new Elt(false);
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(Top != null);
+ Contract.Invariant(Bottom != null);
+}
+
public Elt(IFunctionalMap constraints)
{
@@ -84,16 +92,17 @@ namespace Microsoft.AbstractInterpretationFramework public int Count { get { return this.constraints == null ? 0 : this.constraints.Count; } }
- public IEnumerable/*<IVariable>*/! Variables {
- get
- requires !this.IsBottom;
- {
- assume this.constraints != null;
- return (!) this.constraints.Keys;
+ public IEnumerable/*<IVariable>*//*!*/ Variables {
+ get {
+ Contract.Requires(!this.IsBottom);
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
+ Contract.Assume(this.constraints != null);
+ return cce.NonNull(this.constraints.Keys);
}
}
- public IEnumerable/*<IVariable>*/! SortedVariables(/*maybe null*/ IComparer variableComparer) {
+ public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
if (variableComparer == null) {
return Variables;
} else {
@@ -112,11 +121,11 @@ namespace Microsoft.AbstractInterpretationFramework return (Element)this.constraints[v];
}
- public Element this [IVariable! key] {
- get
- requires !this.IsBottom;
- {
- assume this.constraints != null;
+ public Element this [IVariable/*!*/ key] {
+ get{
+ Contract.Requires(!this.IsBottom);
+ Contract.Requires(key != null);
+ Contract.Assume(this.constraints != null);
return (Element)constraints[key];
}
}
@@ -125,11 +134,14 @@ namespace Microsoft.AbstractInterpretationFramework /// Add a new entry in the functional map: var --> value.
/// If the variable is already there, throws an exception
/// </summary>
- public Elt! Add(IVariable! var, Element! value, MicroLattice! microLattice)
- requires !this.IsBottom;
- {
- assume this.constraints != null;
- assert !this.constraints.Contains(var);
+ public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice){
+Contract.Requires(microLattice != null);
+Contract.Requires(value != null);
+Contract.Requires(var != null);
+Contract.Requires((!this.IsBottom));
+Contract.Ensures(Contract.Result<Elt>() != null);
+ Contract.Assume(this.constraints != null);
+ Contract.Assert(!this.constraints.Contains(var));
if (microLattice.IsBottom(value)) { return Bottom; }
if (microLattice.IsTop(value)) { return this.Remove(var, microLattice); }
@@ -141,13 +153,16 @@ namespace Microsoft.AbstractInterpretationFramework /// Set the value of the variable in the functional map
/// If the variable is not already there, throws an exception
/// </summary>
- public Elt! Set(IVariable! var, Element! value, MicroLattice! microLattice)
- {
+ public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice){
+ Contract.Requires(microLattice != null);
+ Contract.Requires(value != null);
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<Elt>() != null);
if(microLattice.IsBottom(value)) { return Bottom; }
if(microLattice.IsTop(value)) { return this.Remove(var, microLattice); }
- assume this.constraints != null;
- assert this.constraints.Contains(var);
+ Contract.Assume(this.constraints != null);
+ Contract.Assert(this.constraints.Contains(var));
// this.constraints[var] = value;
IFunctionalMap newMap = this.constraints.Set(var, value);
@@ -155,74 +170,95 @@ namespace Microsoft.AbstractInterpretationFramework return new Elt(newMap);
}
- public Elt! Remove(IVariable! var, MicroLattice microLattice)
- {
+ public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice){
+Contract.Requires(var != null);
+Contract.Ensures(Contract.Result<Elt>() != null);
if (this.IsBottom) { return this; }
- assume this.constraints != null;
+ Contract.Assume(this.constraints != null);
return new Elt(this.constraints.Remove(var));
}
- public Elt! Rename(IVariable! oldName, IVariable! newName, MicroLattice! microLattice)
- requires !this.IsBottom;
- {
+ public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice){
+Contract.Requires(microLattice != null);
+Contract.Requires(newName != null);
+Contract.Requires(oldName != null);
+Contract.Requires((!this.IsBottom));
+Contract.Ensures(Contract.Result<Elt>() != null);
Element value = this[oldName];
if (value == null) { return this; } // 'oldName' isn't in the map, so neither will be 'newName'
- assume this.constraints != null;
+ Contract.Assume(this.constraints != null);
IFunctionalMap newMap = this.constraints.Remove(oldName);
newMap = newMap.Add(newName, value);
return new Elt(newMap);
}
[Pure]
- public override ICollection<IVariable!>! FreeVariables()
- {
+ public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
throw new System.NotImplementedException();
}
} // class
- private readonly MicroLattice! microLattice;
+ private readonly MicroLattice/*!*/ microLattice;
+
+ private readonly IPropExprFactory/*!*/ propExprFactory;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(microLattice != null);
+ Contract.Invariant(propExprFactory != null);
+}
- private readonly IPropExprFactory! propExprFactory;
private readonly /*maybe null*/IComparer variableComparer;
- public VariableMapLattice(IPropExprFactory! propExprFactory, IValueExprFactory! valueExprFactory, MicroLattice! microLattice, /*maybe null*/IComparer variableComparer)
- : base(valueExprFactory)
- {
+ public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer)
+ : base(valueExprFactory){
+Contract.Requires(microLattice != null);
+Contract.Requires(valueExprFactory != null);
+Contract.Requires(propExprFactory != null);
this.propExprFactory = propExprFactory;
this.microLattice = microLattice;
this.variableComparer = variableComparer;
// base(valueExprFactory);
}
- protected override object! UniqueId { get { return this.microLattice.GetType(); } }
+ protected override object/*!*/ UniqueId{
+ get{
+Contract.Ensures(Contract.Result<object>() != null);
+ return this.microLattice.GetType(); } }
- public override Element! Top { get { return Elt.Top; } }
+ public override Element/*!*/ Top{
+get{Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Top; } }
- public override Element! Bottom { get { return Elt.Bottom; } }
+ public override Element Bottom{get{
+Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Bottom; } }
- public override bool IsTop(Element! element)
- {
+ public override bool IsTop(Element/*!*/ element){
+Contract.Requires(element != null);
Elt e = (Elt)element;
return !e.IsBottom && e.Count == 0;
}
- public override bool IsBottom(Element! element)
- {
+ public override bool IsBottom(Element/*!*/ element){
+Contract.Requires(element != null);
return ((Elt)element).IsBottom;
}
- protected override bool AtMost(Element! first, Element! second)
- {
+ protected override bool AtMost(Element/*!*/ first, Element/*!*/ second){
+Contract.Requires(second != null);
+Contract.Requires(first != null);
Elt a = (Elt)first;
Elt b = (Elt)second;
// return true iff every constraint in "this" is no weaker than the corresponding
// constraint in "that" and there are no additional constraints in "that"
- foreach (IVariable! var in a.Variables)
- {
- Element thisValue = (!)a[var];
+ foreach(IVariable/*!*/ var in a.Variables){
+Contract.Assert(var != null);
+ Element thisValue = cce.NonNull(a[var]);
Element thatValue = b[var];
if (thatValue == null) { continue; } // it's okay for "a" to know something "b" doesn't
@@ -231,11 +267,11 @@ namespace Microsoft.AbstractInterpretationFramework return false;
}
- foreach (IVariable! var in b.Variables)
- {
+ foreach(IVariable/*!*/ var in b.Variables){
+Contract.Assert(var != null);
if (a.Lookup(var) != null) { continue; } // we checked this case in the loop above
- Element thatValue = (!)b[var];
+ Element thatValue = cce.NonNull(b[var]);
if (this.microLattice.IsTop(thatValue)) { continue; } // this is a trivial constraint
return false;
@@ -243,8 +279,11 @@ namespace Microsoft.AbstractInterpretationFramework return true;
}
- private Elt! AddConstraint(Element! element, IVariable! var, /*MicroLattice*/Element! newValue)
- {
+ private Elt/*!*/ AddConstraint(Element/*!*/ element, IVariable/*!*/ var, /*MicroLattice*/Element/*!*/ newValue) {
+Contract.Requires((newValue != null));
+Contract.Requires((var != null));
+Contract.Requires((element != null));
+Contract.Ensures(Contract.Result<Elt>() != null);
Elt e = (Elt)element;
if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
@@ -266,8 +305,9 @@ namespace Microsoft.AbstractInterpretationFramework return e;
}
- public override string! ToString(Element! element)
- {
+ public override string/*!*/ ToString(Element/*!*/ element){
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<string>() != null);
Elt e = (Elt)element;
if (IsTop(e)) { return "<top>"; }
@@ -275,22 +315,24 @@ namespace Microsoft.AbstractInterpretationFramework int k = 0;
System.Text.StringBuilder buffer = new System.Text.StringBuilder();
- foreach (IVariable! key in e.SortedVariables(variableComparer))
- {
+ foreach(IVariable/*!*/ key in e.SortedVariables(variableComparer)){
+Contract.Assert(key != null);
if (k++ > 0) { buffer.Append("; "); }
buffer.AppendFormat("{0} = {1}", key, e[key]);
}
return buffer.ToString();
}
- public override Element! NontrivialJoin(Element! first, Element! second)
- {
+ 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;
IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach (IVariable! key in a.Variables)
- {
+ foreach(IVariable/*!*/ key in a.Variables){
+Contract.Assert(key != null);
Element aValue = a[key];
Element bValue = b[key];
@@ -301,22 +343,25 @@ namespace Microsoft.AbstractInterpretationFramework newMap = newMap.Add(key, newValue);
}
}
- Elt! join = new Elt(newMap);
+ Elt/*!*/ join = new Elt(newMap);
+ Contract.Assert(join != null);
// System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
return join;
}
- public override Element! NontrivialMeet(Element! first, Element! second)
- {
+ 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;
IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach (IVariable! key in a.Variables)
- {
- Element! aValue = (!) a[key];
+ foreach(IVariable/*!*/ key in a.Variables){
+Contract.Assert(key != null);
+Element/*!*/ aValue = cce.NonNull(a[key]);
Element bValue = b[key];
Element newValue =
@@ -325,8 +370,8 @@ namespace Microsoft.AbstractInterpretationFramework newMap = newMap.Add(key, newValue);
}
- foreach (IVariable! key in b.Variables)
- {
+ foreach(IVariable/*!*/ key in b.Variables){
+Contract.Assert(key != null);
Element aValue = a[key];
Element bValue = b[key]; Debug.Assert(bValue != null);
@@ -342,8 +387,10 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Perform the pointwise widening of the elements in the map
/// </summary>
- public override Element! Widen (Element! first, Element! second)
- {
+ public override Element/*!*/ Widen (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;
@@ -354,8 +401,8 @@ namespace Microsoft.AbstractInterpretationFramework return new Elt(a.Constraints);
IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach (IVariable! key in a.Variables)
- {
+ foreach(IVariable/*!*/ key in a.Variables){
+Contract.Assert(key != null);
Element aValue = a[key];
Element bValue = b[key];
@@ -366,15 +413,17 @@ namespace Microsoft.AbstractInterpretationFramework newMap = newMap.Add(key, newValue);
}
}
- Element! widen= new Elt(newMap);
-
+ Element/*!*/ widen= new Elt(newMap);
+ Contract.Assert(widen != null);
// System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
return widen;
}
- internal static ISet/*<IVariable!>*/! VariablesInExpression(IExpr! e, ISet/*<IVariable!>*/! ignoreVars)
- {
+ internal static ISet/*<IVariable!>*//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/*<IVariable!>*//*!*/ ignoreVars){
+Contract.Requires(ignoreVars != null);
+Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<ISet>() != null);
HashSet s = new HashSet();
IFunApp f = e as IFunApp;
@@ -387,8 +436,8 @@ namespace Microsoft.AbstractInterpretationFramework }
else if (f != null) // e is IFunApp
{
- foreach (IExpr! arg in f.Arguments)
- {
+ foreach(IExpr/*!*/ arg in f.Arguments){
+Contract.Assert(arg != null);
s.AddAll(VariablesInExpression(arg, ignoreVars));
}
}
@@ -398,7 +447,7 @@ namespace Microsoft.AbstractInterpretationFramework x.Add(lambda.Param);
// Ignore the bound variable
- s.AddAll(VariablesInExpression(lambda.Body, (!) Set.Union(ignoreVars, x)));
+ s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
}
else if (e is IUnknown)
{
@@ -412,8 +461,9 @@ namespace Microsoft.AbstractInterpretationFramework }
- private static ArrayList/*<IExpr>*/! FindConjuncts(IExpr e)
+ private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e)
{
+ Contract.Ensures(Contract.Result<ArrayList>() != null);
ArrayList result = new ArrayList();
IFunApp f = e as IFunApp;
@@ -445,8 +495,8 @@ namespace Microsoft.AbstractInterpretationFramework }
private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right)
- ensures result ==> left != null && right != null;
- {
+ {
+ Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
left = null;
right = null;
@@ -467,8 +517,8 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Returns true iff the expression is in the form var == arithmeticExpr
/// </summary>
- private static bool IsArithmeticExpr(IExpr! expr)
- {
+ private static bool IsArithmeticExpr(IExpr/*!*/ expr){
+Contract.Requires(expr != null);
// System.Console.WriteLine("\t\tIsArithmetic called with {0} of type {1}", expr, expr.GetType().ToString());
if(expr is IVariable) // expr is a variable
@@ -480,13 +530,13 @@ namespace Microsoft.AbstractInterpretationFramework if(fun.FunctionSymbol is IntSymbol) // it is an integer
return true;
else if(fun.FunctionSymbol.Equals(Int.Negate)) // it is an unary minus
- return IsArithmeticExpr((IExpr!) fun.Arguments[0]);
+ return IsArithmeticExpr((IExpr/*!*/)cce.NonNull(fun.Arguments[0]));
else if(fun.Arguments.Count != 2) // A function of two or more operands is not arithmetic
return false;
else
{
- IExpr! left = (IExpr!) fun.Arguments[0];
- IExpr! right = (IExpr!) fun.Arguments[1];
+ IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
if(!(left is IVariable || right is IVariable)) // At least one of the two operands must be a variable
return false;
@@ -508,8 +558,9 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- public override IExpr! ToPredicate(Element! element)
- {
+ public override IExpr/*!*/ ToPredicate(Element/*!*/ element){
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<IExpr>() != null);
if (IsTop(element)) { return propExprFactory.True; }
if (IsBottom(element)) { return propExprFactory.False; }
@@ -517,8 +568,8 @@ namespace Microsoft.AbstractInterpretationFramework IExpr truth = propExprFactory.True;
IExpr result = truth;
- foreach (IVariable! variable in e.SortedVariables(variableComparer))
- {
+ foreach(IVariable/*!*/ variable in e.SortedVariables(variableComparer)){
+Contract.Assert(variable != null);
Element value = (Element)e[variable];
if (value == null || this.microLattice.IsTop(value)) { continue; } // Skip variables about which we know nothing.
@@ -532,14 +583,17 @@ namespace Microsoft.AbstractInterpretationFramework }
- public override Element! Eliminate(Element! element, IVariable! variable)
- {
- return ((Elt!)element).Remove(variable, this.microLattice);
+ public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable){
+Contract.Requires(variable != null);
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<Element>() != null);
+ return cce.NonNull((Elt)element).Remove(variable, this.microLattice);
}
- private delegate IExpr! OnUnableToInline(IVariable! var);
- private IExpr! IdentityVarToExpr(IVariable! var)
- {
+ private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
+ private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var){
+Contract.Requires(var != null);
+Contract.Ensures(Contract.Result<IExpr>() != null);
return var;
}
@@ -548,9 +602,13 @@ namespace Microsoft.AbstractInterpretationFramework /// replaced by an expression representing what is known about
/// that variable.
/// </summary>
- private IExpr! InlineVariables(Elt! element, IExpr! expr, ISet/*<IVariable!>*/! notInlineable,
- OnUnableToInline! unableToInline)
- {
+ private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/*<IVariable!>*//*!*/ notInlineable,
+ OnUnableToInline/*!*/ unableToInline){
+ Contract.Requires(unableToInline != null);
+Contract.Requires(notInlineable != null);
+Contract.Requires(expr != null);
+Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
IVariable var = expr as IVariable;
if (var != null)
{
@@ -574,8 +632,8 @@ namespace Microsoft.AbstractInterpretationFramework if (fun != null)
{
IList newargs = new ArrayList();
- foreach (IExpr! arg in fun.Arguments)
- {
+ foreach(IExpr/*!*/ arg in fun.Arguments){
+Contract.Assert(arg != null);
newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
}
return fun.CloneWithArguments(newargs);
@@ -592,7 +650,7 @@ namespace Microsoft.AbstractInterpretationFramework // Don't inline the bound variable
return lambda.CloneWithBody(
InlineVariables(element, lambda.Body,
- (!) Set.Union(notInlineable, x), unableToInline)
+ cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
);
}
@@ -610,19 +668,22 @@ namespace Microsoft.AbstractInterpretationFramework }
- public override Element! Constrain(Element! element, IExpr! expr)
- {
- Elt! result = (Elt)element;
+ public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr){
+Contract.Requires(expr != null);
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<Element>() != null);
+ Elt/*!*/ result = (Elt)element;
+ Contract.Assert(result != null);
if(IsBottom(element))
{
return result; // == element
}
- expr = InlineVariables(result, expr, (!)Set.Empty, new OnUnableToInline(IdentityVarToExpr));
+ expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
- foreach (IExpr! conjunct in FindConjuncts(expr))
- {
+ foreach(IExpr/*!*/ conjunct in FindConjuncts(expr)){
+Contract.Assert(conjunct != null);
IVariable left, right;
if (IsSimpleEquality(conjunct, out left, out right))
@@ -630,7 +691,7 @@ namespace Microsoft.AbstractInterpretationFramework #region The conjunct is a simple equality
- assert left != null && right != null;
+ Contract.Assert(left != null && right != null);
Element leftValue = result[left], rightValue = result[right];
if (leftValue == null) { leftValue = this.microLattice.Top; }
@@ -650,9 +711,9 @@ namespace Microsoft.AbstractInterpretationFramework #region We have just one variable
IVariable var = null;
- foreach (IVariable! v in variablesInvolved) { var = v; } // why is there no better way to get the elements?
- assert var != null;
- Element! value = this.microLattice.EvaluatePredicate(conjunct);
+ foreach (IVariable/*!*/ v in variablesInvolved) {Contract.Assert(v != null); var = v; } // why is there no better way to get the elements?
+ Contract.Assert(var != null);
+ Element/*!*/ value = this.microLattice.EvaluatePredicate(conjunct);
result = AddConstraint(result, var, value);
#endregion
@@ -665,12 +726,13 @@ namespace Microsoft.AbstractInterpretationFramework if(fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
{
// get the variable to be assigned
- IExpr! leftArg = (IExpr!) fun.Arguments[0];
- IExpr! rightArg = (IExpr!) fun.Arguments[1];
- IExpr! var = (leftArg is IVariable) ? leftArg : rightArg;
-
- Element! value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
- result = AddConstraint(result, (IVariable!) var, value);
+ IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
+ IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg;
+
+ Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
+ Contract.Assert(value != null);
+ result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value);
}
#endregion
}
@@ -680,8 +742,11 @@ namespace Microsoft.AbstractInterpretationFramework }
- public override Element! Rename(Element! element, IVariable! oldName, IVariable! newName)
- {
+ public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName){
+Contract.Requires(newName != null);
+Contract.Requires(oldName != null);
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<Element>() != null);
if(IsBottom(element))
{
return element;
@@ -693,26 +758,34 @@ namespace Microsoft.AbstractInterpretationFramework }
- public override bool Understands(IFunctionSymbol! f, IList! args)
- {
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args){
+Contract.Requires(args != null);
+Contract.Requires(f != null);
return f.Equals(Prop.And) ||
f.Equals(Value.Eq) ||
microLattice.Understands(f, args);
}
- private sealed class EquivalentExprException : CheckedException { }
+ private sealed class EquivalentExprException :CheckedException { }
private sealed class EquivalentExprInlineCallback
{
- private readonly IVariable! var;
- public EquivalentExprInlineCallback(IVariable! var)
- {
+ private readonly IVariable/*!*/ var;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(var != null);
+ }
+
+ public EquivalentExprInlineCallback(IVariable/*!*/ var){
+Contract.Requires(var != null);
this.var = var;
// base();
}
- public IExpr! ThrowOnUnableToInline(IVariable! othervar)
- throws EquivalentExprException;
- {
+ public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar)
+ //throws EquivalentExprException;
+ {Contract.Requires(othervar != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ Contract.EnsuresOnThrow<EquivalentExprException>(true);
if (othervar.Equals(var))
throw new EquivalentExprException();
else
@@ -720,12 +793,16 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- public override IExpr/*?*/ EquivalentExpr(Element! e, IQueryable! q, IExpr! expr, IVariable! var, ISet/*<IVariable!>*/! prohibitedVars)
- {
+ public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars){
+Contract.Requires(prohibitedVars != null);
+Contract.Requires(var != null);
+Contract.Requires(expr != null);
+Contract.Requires(q != null);
+Contract.Requires(e != null);
try
{
EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
- return InlineVariables((Elt)e, expr, (!)Set.Empty,
+ return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty),
new OnUnableToInline(closure.ThrowOnUnableToInline));
}
catch (EquivalentExprException)
@@ -743,8 +820,9 @@ namespace Microsoft.AbstractInterpretationFramework /// <param name="e">The lattice element.</param>
/// <param name="pred">The predicate.</param>
/// <returns>Yes, No, or Maybe</returns>
- public override Answer CheckPredicate(Element! e, IExpr! pred)
- {
+ public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred){
+Contract.Requires(pred != null);
+Contract.Requires(e != null);
return Answer.Maybe;
}
@@ -759,8 +837,10 @@ namespace Microsoft.AbstractInterpretationFramework /// <param name="var1">The first variable.</param>
/// <param name="var2">The second variable.</param>
/// <returns>Yes, No, or Maybe.</returns>
- public override Answer CheckVariableDisequality(Element! e, IVariable! var1, IVariable! var2)
- {
+ public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2){
+Contract.Requires(var2 != null);
+Contract.Requires(var1 != null);
+Contract.Requires(e != null);
return Answer.Maybe;
}
|