diff options
| author |  tabarbe <unknown> | 2010-08-27 21:15:08 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-27 21:15:08 +0000 |
| commit | c333ecd2f30badea143e79f5f944a8c63398b959 (patch) | |
| tree | 28b04dc9f46d6fa90b4fdf38ffb24898bdc139b0 /Source/AIFramework/VariableMap | |
| parent | dce6bf46952b5dd470ae841cae03706dbc30bc3b (diff) | |
Boogie: Removed some errors with code contracts (commenting out doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
Diffstat (limited to 'Source/AIFramework/VariableMap')
| -rw-r--r-- | Source/AIFramework/VariableMap/ConstantAbstraction.cs | 414 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/DynamicTypeLattice.cs | 175 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/Intervals.cs | 363 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/Nullness.cs | 344 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/VariableMapLattice.cs | 1505 |
5 files changed, 1410 insertions, 1391 deletions
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.cs b/Source/AIFramework/VariableMap/ConstantAbstraction.cs index 89a64290..d8f17a3c 100644 --- a/Source/AIFramework/VariableMap/ConstantAbstraction.cs +++ b/Source/AIFramework/VariableMap/ConstantAbstraction.cs @@ -4,230 +4,248 @@ //
//-----------------------------------------------------------------------------
using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System.Collections;
- using System.Diagnostics;
- //using System.Compiler.Analysis;
- using Microsoft.Basetypes;
+namespace Microsoft.AbstractInterpretationFramework {
+ using System.Collections;
+ using System.Diagnostics;
+ //using System.Compiler.Analysis;
+ using Microsoft.Basetypes;
+
+ /// <summary>
+ /// Represents an invariant over constant variable assignments.
+ /// </summary>
+ public class ConstantLattice : MicroLattice {
+ enum Value {
+ Top,
+ Bottom,
+ Constant
+ }
- /// <summary>
- /// Represents an invariant over constant variable assignments.
- /// </summary>
- public class ConstantLattice : MicroLattice
- {
- enum Value { Top, Bottom, Constant }
+ private class Elt : Element {
+ public Value domainValue;
+ public BigNum constantValue; // valid iff domainValue == Value.Constant
- private class Elt : Element
- {
- public Value domainValue;
- public BigNum constantValue; // valid iff domainValue == Value.Constant
+ public Elt(Value v) {
+ this.domainValue = v;
+ }
- public Elt (Value v) { this.domainValue = v; }
+ public Elt(BigNum i) {
+ this.domainValue = Value.Constant;
+ this.constantValue = i;
+ }
- public Elt (BigNum i) { this.domainValue = Value.Constant; this.constantValue = i; }
+ public bool IsConstant {
+ get {
+ return this.domainValue == Value.Constant;
+ }
+ }
- public bool IsConstant { get { return this.domainValue == Value.Constant; } }
+ public BigNum Constant {
+ get {
+ return this.constantValue;
+ }
+ } // only when IsConstant
- public BigNum Constant { get { return this.constantValue; } } // only when IsConstant
+ [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 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.IsConstant)
- return new Elt(constantValue);
- else
- return new Elt(domainValue);
- }
- }
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ if (this.IsConstant)
+ return new Elt(constantValue);
+ else
+ return new Elt(domainValue);
+ }
+ }
- readonly IIntExprFactory/*!*/ factory;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(factory != null);
- }
+ readonly IIntExprFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
- public ConstantLattice(IIntExprFactory/*!*/ factory){
-Contract.Requires(factory != null);
- this.factory = factory;
- // base();
- }
+ public ConstantLattice(IIntExprFactory/*!*/ factory) {
+ Contract.Requires(factory != null);
+ this.factory = factory;
+ // base();
+ }
- public override Element/*!*/ Top{get{
-Contract.Ensures(Contract.Result<Element>() != null);
- 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{
-Contract.Ensures(Contract.Result<Element>() != null);
- 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){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- return e.domainValue == Value.Top; - }
+ 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){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- return e.domainValue == Value.Bottom; - }
+ 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){
-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/*!*/ 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){
-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){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- return Join(first,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;
+ }
- 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 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/*!*/ 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)));
- }
+ 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 GetFoldExpr(Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- Contract.Assert(e.domainValue == Value.Constant);
- return factory.Const(e.constantValue);
- }
+ 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 bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args){
-Contract.Requires(args != null);
-Contract.Requires(f != null);
- return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- }
+ public override IExpr GetFoldExpr(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ Contract.Assert(e.domainValue == Value.Constant);
+ return factory.Const(e.constantValue);
+ }
- 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;
- 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 {
- if (arg0 is IVariable) {
- BigNum z;
- if (Fold(arg1, out z)) {
- return new Elt(z);
- }
- } else if (arg1 is IVariable) {
- BigNum z;
- if (Fold(arg0, out z)) {
- return new Elt(z);
- }
- }
- } catch (System.ArithmeticException) {
- // fall through and return Top. (Note, an alternative design may
- // consider returning Bottom.)
- }
- }
- }
- return Top;
- }
+ 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>
- /// Returns true if "expr" represents a constant integer expressions, in which case
- /// "z" returns as that integer. Otherwise, returns false, in which case "z" should
- /// not be used by the caller.
- ///
- /// 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){
-Contract.Requires(expr != null);
- IFunApp e = expr as IFunApp;
- if (e == null) {
- z = BigNum.ZERO;
- 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) {
+ if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
+ 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 {
+ if (arg0 is IVariable) {
+ BigNum z;
+ if (Fold(arg1, out z)) {
+ return new Elt(z);
+ }
+ } else if (arg1 is IVariable) {
+ BigNum z;
+ if (Fold(arg0, out z)) {
+ return new Elt(z);
+ }
}
+ } catch (System.ArithmeticException) {
+ // fall through and return Top. (Note, an alternative design may
+ // consider returning Bottom.)
+ }
+ }
+ }
+ return Top;
+ }
- if (e.FunctionSymbol is IntSymbol) {
- z = ((IntSymbol)e.FunctionSymbol).Value;
- return true;
-
- } else if (e.FunctionSymbol.Equals(Int.Negate)) {
- 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;
- return true;
- }
-
- } else if (e.Arguments.Count == 2) {
- 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)) {
- z = z0 + z1;
- } else if (e.FunctionSymbol.Equals(Int.Sub)) {
- z = z0 - z1;
- } else if (e.FunctionSymbol.Equals(Int.Mul)) {
- z = z0 * z1;
- } else if (e.FunctionSymbol.Equals(Int.Div)) {
- z = z0 / z1;
- } else if (e.FunctionSymbol.Equals(Int.Mod)) {
- z = z0 % z1;
- } else {
- z = BigNum.ZERO;
- return false;
- }
- return true;
- }
- }
-
+ /// <summary>
+ /// Returns true if "expr" represents a constant integer expressions, in which case
+ /// "z" returns as that integer. Otherwise, returns false, in which case "z" should
+ /// not be used by the caller.
+ ///
+ /// 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) {
+ Contract.Requires(expr != null);
+ IFunApp e = expr as IFunApp;
+ if (e == null) {
+ z = BigNum.ZERO;
+ return false;
+ }
+
+ if (e.FunctionSymbol is IntSymbol) {
+ z = ((IntSymbol)e.FunctionSymbol).Value;
+ return true;
+
+ } else if (e.FunctionSymbol.Equals(Int.Negate)) {
+ 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;
+ return true;
+ }
+
+ } else if (e.Arguments.Count == 2) {
+ 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)) {
+ z = z0 + z1;
+ } else if (e.FunctionSymbol.Equals(Int.Sub)) {
+ z = z0 - z1;
+ } else if (e.FunctionSymbol.Equals(Int.Mul)) {
+ z = z0 * z1;
+ } else if (e.FunctionSymbol.Equals(Int.Div)) {
+ z = z0 / z1;
+ } else if (e.FunctionSymbol.Equals(Int.Mod)) {
+ z = z0 % z1;
+ } else {
z = BigNum.ZERO;
return false;
+ }
+ return true;
}
+ }
+
+ z = BigNum.ZERO;
+ return false;
}
+ }
}
diff --git a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs index 84525a15..78bd61a0 100644 --- a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs +++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs @@ -163,100 +163,101 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override bool IsTop(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Elt e = (Elt)element;
return e.what == What.Bounds && e.ty == null && e.manyBounds == null;
}
public override bool IsBottom(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Elt e = (Elt)element;
return e.what == What.Bottom;
}
- public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
- if (a.what == What.Exact && b.what == What.Exact) {
- Contract.Assert(a.ty != null && b.ty != null);
- if (factory.IsTypeEqual(a.ty, b.ty)) {
- return a;
- } else {
- return new Elt(What.Bounds, factory.JoinTypes(a.ty, b.ty));
- }
- }
+ public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
+ if (a.what == What.Exact && b.what == What.Exact) {
+ Contract.Assert(a.ty != null && b.ty != null);
+ if (factory.IsTypeEqual(a.ty, b.ty)) {
+ return a;
+ } else {
+ return new Elt(What.Bounds, factory.JoinTypes(a.ty, b.ty));
+ }
+ }
- // The result is going to be a Bounds, since at least one of the operands is a Bounds.
- Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount); // a preconditions is that neither operand is Top
- int n = a.BoundsCount + b.BoundsCount;
-
- // Special case: a and b each has exactly one bound
- if (n == 2) {
- Contract.Assert(a.ty != null && b.ty != null);
- IExpr join = factory.JoinTypes(a.ty, b.ty);
- Contract.Assert(join != null);
- if (join == a.ty && a.what == What.Bounds) {
- return a;
- } else if (join == b.ty && b.what == What.Bounds) {
- return b;
- } else {
- return new Elt(What.Bounds, join);
- }
- }
+ // The result is going to be a Bounds, since at least one of the operands is a Bounds.
+ Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount); // a preconditions is that neither operand is Top
+ int n = a.BoundsCount + b.BoundsCount;
- // General case
- ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n); // final size
- ArrayList /*IExpr!*/ result = new ArrayList /*IExpr!*/ (n); // a guess at the size, but could be as big as size(a)*size(b)
- if (a.ty != null) {
- allBounds.Add(a.ty);
- } else {
- allBounds.AddRange(cce.NonNull(a.manyBounds));
- }
- int bStart = allBounds.Count;
- if (b.ty != null) {
- allBounds.Add(b.ty);
+ // Special case: a and b each has exactly one bound
+ if (n == 2) {
+ Contract.Assert(a.ty != null && b.ty != null);
+ IExpr join = factory.JoinTypes(a.ty, b.ty);
+ Contract.Assert(join != null);
+ if (join == a.ty && a.what == What.Bounds) {
+ return a;
+ } else if (join == b.ty && b.what == What.Bounds) {
+ return b;
+ } else {
+ return new Elt(What.Bounds, join);
+ }
+ }
+
+ // General case
+ ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n); // final size
+ ArrayList /*IExpr!*/ result = new ArrayList /*IExpr!*/ (n); // a guess at the size, but could be as big as size(a)*size(b)
+ if (a.ty != null) {
+ allBounds.Add(a.ty);
+ } else {
+ allBounds.AddRange(cce.NonNull(a.manyBounds));
+ }
+ int bStart = allBounds.Count;
+ if (b.ty != null) {
+ allBounds.Add(b.ty);
+ } else {
+ allBounds.AddRange(cce.NonNull(b.manyBounds));
+ }
+ // compute the join of each pair, putting non-redundant joins into "result"
+ for (int i = 0; i < bStart; i++) {
+ IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);
+ for (int j = bStart; j < allBounds.Count; j++) {
+ IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);
+
+ IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);
+ Contract.Assert(join != null);
+
+ int k = 0;
+ while (k < result.Count) {
+ IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(result[k]);
+ if (factory.IsSubType(join, r)) {
+ // "join" is more restrictive than a bound already placed in "result",
+ // so toss out "join" and compute the join of the next pair
+ goto NEXT_PAIR;
+ } else if (factory.IsSubType(r, join)) {
+ // "join" is less restrictive than a bound already placed in "result",
+ // so toss out that old bound
+ result.RemoveAt(k);
} else {
- allBounds.AddRange(cce.NonNull(b.manyBounds));
+ k++;
}
- // compute the join of each pair, putting non-redundant joins into "result"
- for (int i = 0; i < bStart; i++) {
- IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);
- for (int j = bStart; j < allBounds.Count; j++) {
- IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);
-
- IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);
- Contract.Assert(join != null);
-
- int k = 0;
- while (k < result.Count) {
- IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(result[k]);
- if (factory.IsSubType(join, r)) {
- // "join" is more restrictive than a bound already placed in "result",
- // so toss out "join" and compute the join of the next pair
- goto NEXT_PAIR;
- } else if (factory.IsSubType(r, join)) {
- // "join" is less restrictive than a bound already placed in "result",
- // so toss out that old bound
- result.RemoveAt(k);
- } else {
- k++;
- }
- }
- result.Add(join);
- NEXT_PAIR: {}
- }
- }
- return new Elt(result, result.Count);
+ }
+ result.Add(join);
+ NEXT_PAIR: {
+ }
}
+ }
+ return new Elt(result, result.Count);
+ }
public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Element>() != null);
Elt a = (Elt)first;
Elt b = (Elt)second;
@@ -359,16 +360,16 @@ Contract.Ensures(Contract.Result<Element>() != null); }
public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Element>() != null);
return Join(first, second);
}
protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
{
- Contract.Requires(first != null);
- Contract.Requires(second != null);
+ //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);
@@ -403,8 +404,8 @@ Contract.Ensures(Contract.Result<Element>() != null); }
public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
- Contract.Requires(element != null);
- Contract.Requires(var != null);
+ //Contract.Requires(element != null);
+ //Contract.Requires(var != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
Elt e = (Elt)element;
switch (e.what) {
@@ -433,14 +434,14 @@ Contract.Ensures(Contract.Result<Element>() != null); }
public override IExpr GetFoldExpr(Element/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
// cannot fold into an expression that can be substituted for the variable
return null;
}
public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
- Contract.Requires(args != null);
- Contract.Requires(f != null);
+ //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);
@@ -470,7 +471,7 @@ Contract.Ensures(Contract.Result<Element>() != null); }
public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
IFunApp nary = e as IFunApp;
if (nary != null) {
diff --git a/Source/AIFramework/VariableMap/Intervals.cs b/Source/AIFramework/VariableMap/Intervals.cs index 73a1352f..0bf82cf4 100644 --- a/Source/AIFramework/VariableMap/Intervals.cs +++ b/Source/AIFramework/VariableMap/Intervals.cs @@ -55,7 +55,7 @@ namespace Microsoft.AbstractInterpretationFramework { /// The paramter is the top?
/// </summary>
public override bool IsTop(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
IntervalElement interval = (IntervalElement)element;
return interval.IsTop();
@@ -65,7 +65,7 @@ namespace Microsoft.AbstractInterpretationFramework { /// The parameter is the bottom?
/// </summary>
public override bool IsBottom(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
IntervalElement interval = (IntervalElement)element;
return interval.IsBottom();
@@ -75,8 +75,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// The classic, pointwise, join of intervals
/// </summary>
public override Element/*!*/ NontrivialJoin(Element/*!*/ left, Element/*!*/ right) {
- Contract.Requires(right != null);
- Contract.Requires(left != null);
+ //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);
@@ -93,8 +93,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// The classic, pointwise, meet of intervals
/// </summary>
public override Element/*!*/ NontrivialMeet(Element/*!*/ left, Element/*!*/ right) {
- Contract.Requires(right != null);
- Contract.Requires(left != null);
+ //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);
@@ -111,8 +111,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// left is the PREVIOUS value in the iterations and right is the NEW one
/// </summary>
public override Element/*!*/ Widen(Element/*!*/ left, Element/*!*/ right) {
- Contract.Requires(right != null);
- Contract.Requires(left != null);
+ //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);
@@ -130,8 +130,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// Return true iff the interval left is containted in right
/// </summary>
protected override bool AtMost(Element/*!*/ left, Element/*!*/ right) {
- Contract.Requires(right != null);
- Contract.Requires(left != null);
+ //Contract.Requires(right != null);
+ //Contract.Requires(left != null);
IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
@@ -145,50 +145,48 @@ namespace Microsoft.AbstractInterpretationFramework { /// Return just null
/// </summary>
public override IExpr GetFoldExpr(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //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){
-Contract.Requires(element != null);
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
-IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(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; + IExpr upperBound = null;
- if(! (interval.Inf is InfinitaryInt))
- {
+ if (!(interval.Inf is InfinitaryInt)) {
IExpr constant = this.factory.Const(interval.Inf.Value);
lowerBound = this.factory.AtMost(constant, var); // inf <= var
}
- if(! (interval.Sup is InfinitaryInt))
- {
+ if (!(interval.Sup is InfinitaryInt)) {
IExpr constant = this.factory.Const(interval.Sup.Value);
upperBound = this.factory.AtMost(var, constant); // var <= inf
}
- if(lowerBound != null && upperBound != null)
+ if (lowerBound != null && upperBound != null)
return this.factory.And(lowerBound, upperBound); // inf <= var && var <= sup
else
- if(lowerBound != null)
+ if (lowerBound != null)
return lowerBound;
- else
- if(upperBound != null)
- 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;
+ else
+ if (upperBound != null)
+ 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) {
- Contract.Requires(args != null);
- Contract.Requires(f != null);
+ //Contract.Requires(args != null);
+ //Contract.Requires(f != null);
return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
}
@@ -197,7 +195,7 @@ IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element); /// Evaluate the predicate passed as input according the semantics of intervals
/// </summary>
public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ pred) {
- Contract.Requires(pred != null);
+ //Contract.Requires(pred != null);
Contract.Ensures(Contract.Result<Element>() != null);
return this.EvaluatePredicateWithState(pred, null);
}
@@ -206,14 +204,13 @@ IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element); /// 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){
-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
- {
+ 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/*!*/)cce.NonNull(fun.Arguments[0]);
IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
if (leftArg is IVariable) {
@@ -221,78 +218,72 @@ Contract.Ensures(Contract.Result<Element>() != null); } else if (rightArg is IVariable) {
return Eval(leftArg, state);
}
- }
+ }
}
// otherwise we simply return Top
- return IntervalElement.Top; + return IntervalElement.Top;
}
/// <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) {
-Contract.Requires((exp != null));
-Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ Contract.Requires((exp != null));
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
IntervalElement/*!*/ retVal = (IntervalElement/*!*/)cce.NonNull(Top);
// Eval the expression by structural induction
- if(exp is IVariable && state != null) // A variable
+ if (exp is IVariable && state != null) // A variable
{
object lookup = state[exp];
- if(lookup is IntervalElement)
- retVal = (IntervalElement) lookup;
- else
- {
- retVal = (IntervalElement) Top;
+ if (lookup is IntervalElement)
+ retVal = (IntervalElement)lookup;
+ else {
+ retVal = (IntervalElement)Top;
}
- }
- else if(exp is IFunApp)
- {
- IFunApp fun = (IFunApp) exp; -
- if(fun.FunctionSymbol is IntSymbol) // An integer
+ } else if (exp is IFunApp) {
+ IFunApp fun = (IFunApp)exp;
+
+ if (fun.FunctionSymbol is IntSymbol) // An integer
{
- IntSymbol intSymb = (IntSymbol) fun.FunctionSymbol;
+ IntSymbol intSymb = (IntSymbol)fun.FunctionSymbol;
BigNum val = intSymb.Value;
-
+
retVal = IntervalElement.Factory(val);
- }
- else if(fun.FunctionSymbol.Equals(Int.Negate)) // An unary minus
+ } else if (fun.FunctionSymbol.Equals(Int.Negate)) // An unary minus
{
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)
- {
+ } else if (fun.Arguments.Count == 2) {
IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
-
+
IntervalElement/*!*/ leftVal = Eval(left, state);
Contract.Assert(leftVal != null);
IntervalElement/*!*/ rightVal = Eval(right, state);
Contract.Assert(rightVal != null);
- if(fun.FunctionSymbol.Equals(Int.Add))
+ if (fun.FunctionSymbol.Equals(Int.Add))
retVal = leftVal + rightVal;
- else if(fun.FunctionSymbol.Equals(Int.Sub))
+ else if (fun.FunctionSymbol.Equals(Int.Sub))
retVal = leftVal - rightVal;
- else if(fun.FunctionSymbol.Equals(Int.Mul))
+ else if (fun.FunctionSymbol.Equals(Int.Mul))
retVal = leftVal * rightVal;
- else if(fun.FunctionSymbol.Equals(Int.Div))
+ else if (fun.FunctionSymbol.Equals(Int.Div))
retVal = leftVal / rightVal;
- else if(fun.FunctionSymbol.Equals(Int.Mod))
- retVal = leftVal % rightVal; + else if (fun.FunctionSymbol.Equals(Int.Mod))
+ retVal = leftVal % rightVal;
}
- }
-
+ }
+
return retVal;
}
@@ -351,8 +342,8 @@ Contract.Ensures(Contract.Result<IntervalElement>() != null); // 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);
+ Contract.Requires((inf != null));
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
if (inf is MinusInfinity && sup is PlusInfinity)
return Top;
if (inf > sup)
@@ -367,12 +358,12 @@ Contract.Ensures(Contract.Result<IntervalElement>() != null); }
public static IntervalElement/*!*/ Factory(BigNum inf, BigNum sup) {
-Contract.Ensures(Contract.Result<IntervalElement>() != null);
- ExtendedInt/*!*/ i = ExtendedInt.Factory(inf);
- ExtendedInt/*!*/ s = ExtendedInt.Factory(sup);
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ i = ExtendedInt.Factory(inf);
+ ExtendedInt/*!*/ s = ExtendedInt.Factory(sup);
- return Factory(i, s);
- }
+ return Factory(i, s);
+ }
static public IntervalElement/*!*/ Top {
get {
@@ -401,103 +392,103 @@ Contract.Ensures(Contract.Result<IntervalElement>() != null); #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); - }
+ 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){
-Contract.Requires(b != null);
-Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<IntervalElement>() != null);
- ExtendedInt/*!*/ inf = a.inf - b.sup;
+ 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;
- }
+ 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){
-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);
- }
+ 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){
-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;
- 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);
- }
+ 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;
+ 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){
-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;
- 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);
-
- return Factory(inf, sup);
- }
+ 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;
+ 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);
+
+ return Factory(inf, sup);
+ }
#endregion
@@ -520,9 +511,9 @@ Contract.Ensures(Contract.Result<IntervalElement>() != null); [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();
- }
+ 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() {
@@ -736,13 +727,13 @@ return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsRead return sup;
}
- 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);
+ 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);
@@ -760,13 +751,13 @@ Contract.Ensures(Contract.Result<ExtendedInt>() != null); return sup;
}
- 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);
+ 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);
@@ -816,7 +807,7 @@ Contract.Ensures(Contract.Result<ExtendedInt>() != null); }
public override int CompareTo(ExtendedInt/*!*/ that) {
- Contract.Requires(that != null);
+ //Contract.Requires(that != null);
if (that is PlusInfinity)
return -1;
else if (that is PureInteger)
@@ -848,7 +839,7 @@ Contract.Ensures(Contract.Result<ExtendedInt>() != null); }
public override int CompareTo(ExtendedInt/*!*/ that) {
- Contract.Requires(that != null);
+ //Contract.Requires(that != null);
if (that is PlusInfinity)
return 0;
else
@@ -870,7 +861,7 @@ Contract.Ensures(Contract.Result<ExtendedInt>() != null); }
public override int CompareTo(ExtendedInt/*!*/ that) {
- Contract.Requires(that != null);
+ //Contract.Requires(that != null);
if (that is MinusInfinity)
return 0;
else
diff --git a/Source/AIFramework/VariableMap/Nullness.cs b/Source/AIFramework/VariableMap/Nullness.cs index 9eac6b29..613f55e0 100644 --- a/Source/AIFramework/VariableMap/Nullness.cs +++ b/Source/AIFramework/VariableMap/Nullness.cs @@ -4,200 +4,206 @@ //
//-----------------------------------------------------------------------------
using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System.Collections;
- using System.Diagnostics;
- //using System.Compiler.Analysis;
+namespace Microsoft.AbstractInterpretationFramework {
+ using System.Collections;
+ using System.Diagnostics;
+ //using System.Compiler.Analysis;
+
+ public class NullnessLattice : MicroLattice {
+ readonly INullnessFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
- public class NullnessLattice : MicroLattice
- {
- readonly INullnessFactory/*!*/ factory;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(factory != null);
- }
+ public NullnessLattice(INullnessFactory/*!*/ factory) {
+ Contract.Requires(factory != null);
+ this.factory = factory;
+ // base();
+ }
- public NullnessLattice(INullnessFactory/*!*/ factory){
-Contract.Requires(factory != null);
- this.factory = factory;
- // base();
- }
-
- enum Value { Bottom, NotNull, Null, MayBeNull }
+ enum Value {
+ Bottom,
+ NotNull,
+ Null,
+ MayBeNull
+ }
- private class Elt : Element
- {
- public Value value;
-
- public Elt (Value v) { this.value = v; }
-
- [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);
- return new Elt(this.value);
- }
- }
+ private class Elt : Element {
+ public Value value;
+ public Elt(Value v) {
+ this.value = v;
+ }
- public override Element/*!*/ Top
- {
- get {Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.MayBeNull); }
- }
+ [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/*!*/ Bottom
- {
- get {Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.Bottom); }
- }
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(this.value);
+ }
+ }
- public static Element/*!*/ Null
- {
- get {Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.Null); }
- }
- public static Element/*!*/ NotNull
- {
- get {Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.NotNull); }
- }
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.MayBeNull);
+ }
+ }
- public override bool IsTop (Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt) element;
- return e.value == Value.MayBeNull;
- }
+ public override Element/*!*/ Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Bottom);
+ }
+ }
- public override bool IsBottom (Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt) element;
- return e.value == Value.Bottom;
- }
+ public static Element/*!*/ Null {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Null);
+ }
+ }
- 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 static Element/*!*/ NotNull {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.NotNull);
+ }
+ }
- 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){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- return Join(first,second);
- }
+ public override bool IsTop(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return e.value == Value.MayBeNull;
+ }
- 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 bool IsBottom(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return e.value == Value.Bottom;
+ }
- 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;
+ 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;
+ }
- if (e.value == Value.NotNull)
- {
- return factory.Neq(var, factory.Null);
- }
- if (e.value == Value.Null)
- {
- return factory.Eq(var, factory.Null);
- }
- {Contract.Assert(false);throw new cce.UnreachableException();}
- throw new System.Exception();
- }
+ 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 IExpr GetFoldExpr(Element/*!*/ e){
-Contract.Requires(e != null);
- Elt elt = (Elt)e;
- if (elt.value == Value.Null) {
- return factory.Null;
- } else {
- // can't fold into an expression
- return null;
- }
- }
+ 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 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)) {
+ 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;
+ }
- Contract.Assert(args.Count == 2);
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
- IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+ 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;
- // 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) {
- return true;
- } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
- return true;
- }
- }
- return false;
- }
+ if (e.value == Value.NotNull) {
+ return factory.Neq(var, factory.Null);
+ }
+ if (e.value == Value.Null) {
+ return factory.Eq(var, factory.Null);
+ }
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ throw new System.Exception();
+ }
- 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;
- 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;
- if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null)
- {
- var = (IVariable)arg0;
- }
- else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null)
- {
- var = (IVariable)arg1;
- }
+ public override IExpr GetFoldExpr(Element/*!*/ e) {
+ //Contract.Requires(e != null);
+ Elt elt = (Elt)e;
+ if (elt.value == Value.Null) {
+ return factory.Null;
+ } else {
+ // can't fold into an expression
+ return null;
+ }
+ }
- if (var != null) // found the pattern
+ 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)) {
+
+ 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) {
+ return true;
+ } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
+ 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.Neq)) {
+ 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;
+ if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
+ var = (IVariable)arg0;
+ } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
+ var = (IVariable)arg1;
+ }
+
+ if (var != null) // found the pattern
{
- return isEq ? Null:NotNull;
- }
- }
- }
- return Top;
+ return isEq ? Null : NotNull;
+ }
}
+ }
+ return Top;
}
+ }
#if false
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs index e0b9ac04..169156b0 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.cs +++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs @@ -3,852 +3,855 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System.Diagnostics.Contracts;
- using System.Collections;
- using System.Collections.Generic;
- using System.Diagnostics;
-
- using Microsoft.AbstractInterpretationFramework;
- using Microsoft.AbstractInterpretationFramework.Collections;
-
- using Microsoft.Boogie;
- using IMutableSet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
- using ISet = Microsoft.Boogie.Set;
-
- /// <summary>
- /// Creates a lattice that works for several variables given a MicroLattice. Assumes
- /// if one variable is bottom, then all variables are bottom.
- /// </summary>
- public class VariableMapLattice : Lattice
- {
- private class Elt : Element
- {
- /// <summary>
- /// IsBottom(e) iff e.constraints == null
- /// </summary>
- /*MayBeNull*/
- private IFunctionalMap constraints; // of type IVariable -> LATTICE_ELEMENT
- public IFunctionalMap Constraints
- {
- get
- {
- return this.constraints;
- }
- }
+namespace Microsoft.AbstractInterpretationFramework {
+ using System.Diagnostics.Contracts;
+ using System.Collections;
+ using System.Collections.Generic;
+ using System.Diagnostics;
+
+ using Microsoft.AbstractInterpretationFramework;
+ using Microsoft.AbstractInterpretationFramework.Collections;
+
+ using Microsoft.Boogie;
+ using IMutableSet = Microsoft.Boogie.Set;
+ using HashSet = Microsoft.Boogie.Set;
+ using ISet = Microsoft.Boogie.Set;
+
+ /// <summary>
+ /// Creates a lattice that works for several variables given a MicroLattice. Assumes
+ /// if one variable is bottom, then all variables are bottom.
+ /// </summary>
+ public class VariableMapLattice : Lattice {
+ private class Elt : Element {
+ /// <summary>
+ /// IsBottom(e) iff e.constraints == null
+ /// </summary>
+ /*MayBeNull*/
+ private IFunctionalMap constraints; // of type IVariable -> LATTICE_ELEMENT
+ public IFunctionalMap Constraints {
+ get {
+ return this.constraints;
+ }
+ }
- private Elt(bool top) {
- if (top) {
- this.constraints = FunctionalHashtable.Empty;
- } else {
- this.constraints = null;
- }
- }
+ private Elt(bool top) {
+ if (top) {
+ this.constraints = FunctionalHashtable.Empty;
+ } else {
+ this.constraints = null;
+ }
+ }
- public override Element/*!*/ Clone() {
-Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(this.constraints);
- }
-
- [Pure]
- public override string/*!*/ ToString() {
-Contract.Ensures(Contract.Result<string>() != null);
- if (constraints == null) {
- return "<bottom>";
- }
- string s = "[";
- string sep = "";
- foreach(IVariable/*!*/ v in cce.NonNull(constraints.Keys)){
-Contract.Assert(v != null);
- Element m = (Element)constraints[v];
- s += sep + v.Name + " -> " + m;
- sep = ", ";
- }
- return s + "]";
- }
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(this.constraints);
+ }
- 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);
-}
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ if (constraints == null) {
+ return "<bottom>";
+ }
+ string s = "[";
+ string sep = "";
+ foreach (IVariable/*!*/ v in cce.NonNull(constraints.Keys)) {
+ Contract.Assert(v != null);
+ Element m = (Element)constraints[v];
+ s += sep + v.Name + " -> " + m;
+ sep = ", ";
+ }
+ return s + "]";
+ }
+ 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)
- {
- this.constraints = constraints;
- }
- public bool IsBottom {
- get {
- return this.constraints == null;
- }
- }
+ public Elt(IFunctionalMap constraints) {
+ this.constraints = constraints;
+ }
- public int Count { get { return this.constraints == null ? 0 : this.constraints.Count; } }
+ public bool IsBottom {
+ get {
+ return this.constraints == null;
+ }
+ }
- 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 int Count {
+ get {
+ return this.constraints == null ? 0 : this.constraints.Count;
+ }
+ }
- public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
- Contract.Ensures(Contract.Result<IEnumerable>() != null);
- if (variableComparer == null) {
- return Variables;
- } else {
- ArrayList /*IVariable*/ vars = new ArrayList /*IVariable*/ (Count);
- foreach (IVariable variable in Variables) {
- vars.Add(variable);
- }
- vars.Sort(variableComparer);
- return vars;
- }
- }
-
- public Element Lookup(IVariable v)
- {
- if ((v == null) || (this.constraints == null)) { return null; }
- return (Element)this.constraints[v];
- }
+ 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 Element this [IVariable/*!*/ key] {
- get{
- Contract.Requires(!this.IsBottom);
- Contract.Requires(key != null);
- Contract.Assume(this.constraints != null);
- return (Element)constraints[key];
- }
- }
+ public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
+ if (variableComparer == null) {
+ return Variables;
+ } else {
+ ArrayList /*IVariable*/ vars = new ArrayList /*IVariable*/ (Count);
+ foreach (IVariable variable in Variables) {
+ vars.Add(variable);
+ }
+ vars.Sort(variableComparer);
+ return vars;
+ }
+ }
- /// <summary>
- /// 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){
-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); }
-
- return new Elt(this.constraints.Add(var, value));
- }
+ public Element Lookup(IVariable v) {
+ if ((v == null) || (this.constraints == null)) {
+ return null;
+ }
+ return (Element)this.constraints[v];
+ }
- /// <summary>
- /// 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){
- 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); }
-
- Contract.Assume(this.constraints != null);
- Contract.Assert(this.constraints.Contains(var));
-
- // this.constraints[var] = value;
- IFunctionalMap newMap = this.constraints.Set(var, value);
-
- return new Elt(newMap);
- }
+ public Element this[IVariable/*!*/ key] {
+ get {
+ Contract.Requires(!this.IsBottom);
+ Contract.Requires(key != null);
+ Contract.Assume(this.constraints != null);
+ return (Element)constraints[key];
+ }
+ }
- public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice){
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<Elt>() != null);
- if (this.IsBottom) { return this; }
- Contract.Assume(this.constraints != null);
- return new Elt(this.constraints.Remove(var));
- }
+ /// <summary>
+ /// 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) {
+ 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);
+ }
- 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'
- Contract.Assume(this.constraints != null);
- IFunctionalMap newMap = this.constraints.Remove(oldName);
- newMap = newMap.Add(newName, value);
- return new Elt(newMap);
- }
+ return new Elt(this.constraints.Add(var, value));
+ }
- [Pure]
- public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
- throw new System.NotImplementedException();
- }
+ /// <summary>
+ /// 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) {
+ 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);
+ }
- } // class
+ Contract.Assume(this.constraints != null);
+ Contract.Assert(this.constraints.Contains(var));
- private readonly MicroLattice/*!*/ microLattice;
+ // this.constraints[var] = value;
+ IFunctionalMap newMap = this.constraints.Set(var, value);
- private readonly IPropExprFactory/*!*/ propExprFactory;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(microLattice != null);
- Contract.Invariant(propExprFactory != null);
-}
+ return new Elt(newMap);
+ }
-
- private readonly /*maybe null*/IComparer variableComparer;
-
- 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);
+ public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice) {
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ if (this.IsBottom) {
+ return this;
}
+ Contract.Assume(this.constraints != null);
+ return new Elt(this.constraints.Remove(var));
+ }
- protected override object/*!*/ UniqueId{
- get{
-Contract.Ensures(Contract.Result<object>() != null);
- return this.microLattice.GetType(); } }
+ 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'
+ Contract.Assume(this.constraints != null);
+ IFunctionalMap newMap = this.constraints.Remove(oldName);
+ newMap = newMap.Add(newName, value);
+ return new Elt(newMap);
+ }
- public override Element/*!*/ Top{
-get{Contract.Ensures(Contract.Result<Element>() != null);
- return Elt.Top; } }
+ [Pure]
+ public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
+ throw new System.NotImplementedException();
+ }
- public override Element Bottom{get{
-Contract.Ensures(Contract.Result<Element>() != null);
- return Elt.Bottom; } }
+ } // class
- public override bool IsTop(Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- return !e.IsBottom && e.Count == 0;
- }
+ private readonly MicroLattice/*!*/ microLattice;
- public override bool IsBottom(Element/*!*/ element){
-Contract.Requires(element != null);
- return ((Elt)element).IsBottom;
- }
+ private readonly IPropExprFactory/*!*/ propExprFactory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(microLattice != null);
+ Contract.Invariant(propExprFactory != null);
+ }
- 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){
-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
-
- if (this.microLattice.LowerThan(thisValue, thatValue)) { continue; } // constraint for "var" satisfies AtMost relation
-
- return false;
- }
- 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 = cce.NonNull(b[var]);
- if (this.microLattice.IsTop(thatValue)) { continue; } // this is a trivial constraint
-
- return false;
- }
- return true;
- }
- 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;
+ private readonly /*maybe null*/IComparer variableComparer;
+
+ 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 {
+ Contract.Ensures(Contract.Result<object>() != null);
+ return this.microLattice.GetType();
+ }
+ }
+
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Top;
+ }
+ }
+
+ public override Element Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Bottom;
+ }
+ }
+
+ 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) {
+ //Contract.Requires(element != null);
+ return ((Elt)element).IsBottom;
+ }
+
+ 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) {
+ 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
+
+ if (this.microLattice.LowerThan(thisValue, thatValue)) {
+ continue;
+ } // constraint for "var" satisfies AtMost relation
+
+ return false;
+ }
+ 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 = cce.NonNull(b[var]);
+ if (this.microLattice.IsTop(thatValue)) {
+ continue;
+ } // this is a trivial constraint
+
+ return false;
+ }
+ return true;
+ }
+
+ 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
+ if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
{
- /*MicroLattice*/Element currentValue = e[var];
-
- if (currentValue == null)
- {
- // No information currently, so we just add the new info.
- return e.Add(var, newValue, this.microLattice);
- }
- else
- {
- // Otherwise, take the meet of the new and current info.
- //return e.Add(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
- return e.Set(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
- }
- }
- return e;
+ /*MicroLattice*/
+ Element currentValue = e[var];
+
+ if (currentValue == null) {
+ // No information currently, so we just add the new info.
+ return e.Add(var, newValue, this.microLattice);
+ } else {
+ // Otherwise, take the meet of the new and current info.
+ //return e.Add(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
+ return e.Set(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
}
+ }
+ return e;
+ }
- public override string/*!*/ ToString(Element/*!*/ element){
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<string>() != null);
- Elt e = (Elt)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>"; }
- if (IsBottom(e)) { return "<bottom>"; }
+ if (IsTop(e)) {
+ return "<top>";
+ }
+ if (IsBottom(e)) {
+ return "<bottom>";
+ }
- int k = 0;
- System.Text.StringBuilder buffer = new System.Text.StringBuilder();
- 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();
+ int k = 0;
+ System.Text.StringBuilder buffer = new System.Text.StringBuilder();
+ 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){
-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){
-Contract.Assert(key != null);
- Element aValue = a[key];
- Element bValue = b[key];
-
- if (aValue != null && bValue != null)
- {
- // Keep only the variables known to both elements.
- Element newValue = this.microLattice.Join(aValue, bValue);
- newMap = newMap.Add(key, newValue);
- }
- }
- 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/*!*/ 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) {
+ Contract.Assert(key != null);
+ Element aValue = a[key];
+ Element bValue = b[key];
+
+ if (aValue != null && bValue != null) {
+ // Keep only the variables known to both elements.
+ Element newValue = this.microLattice.Join(aValue, bValue);
+ newMap = newMap.Add(key, newValue);
}
+ }
+ Elt/*!*/ join = new Elt(newMap);
+ Contract.Assert(join != null);
+
+ // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
- 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;
+ return join;
+ }
- IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach(IVariable/*!*/ key in a.Variables){
-Contract.Assert(key != null);
-Element/*!*/ aValue = cce.NonNull(a[key]);
- Element bValue = b[key];
+ 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;
- Element newValue =
- bValue == null ? aValue :
- this.microLattice.Meet(aValue, bValue);
+ IFunctionalMap newMap = FunctionalHashtable.Empty;
+ foreach (IVariable/*!*/ key in a.Variables) {
+ Contract.Assert(key != null);
+ Element/*!*/ aValue = cce.NonNull(a[key]);
+ Element bValue = b[key];
- newMap = newMap.Add(key, newValue);
- }
- foreach(IVariable/*!*/ key in b.Variables){
-Contract.Assert(key != null);
- Element aValue = a[key];
- Element bValue = b[key]; Debug.Assert(bValue != null);
-
- if (aValue == null)
- {
- // It's a variable we didn't cover in the last loop.
- newMap = newMap.Add(key, bValue);
- }
- }
- return new Elt(newMap);
+ Element newValue =
+ bValue == null ? aValue :
+ this.microLattice.Meet(aValue, bValue);
+
+ newMap = newMap.Add(key, newValue);
+ }
+ foreach (IVariable/*!*/ key in b.Variables) {
+ Contract.Assert(key != null);
+ Element aValue = a[key];
+ Element bValue = b[key];
+ Debug.Assert(bValue != null);
+
+ if (aValue == null) {
+ // It's a variable we didn't cover in the last loop.
+ newMap = newMap.Add(key, bValue);
}
+ }
+ return new Elt(newMap);
+ }
- /// <summary>
- /// Perform the pointwise widening of the elements in the map
- /// </summary>
- 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;
-
- // Note we have to add those cases as we do not have a "NonTrivialWiden" method
- if(a.IsBottom)
- return new Elt(b.Constraints);
- if(b.IsBottom)
- return new Elt(a.Constraints);
-
- IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach(IVariable/*!*/ key in a.Variables){
-Contract.Assert(key != null);
- Element aValue = a[key];
- Element bValue = b[key];
-
- if (aValue != null && bValue != null)
- {
- // Keep only the variables known to both elements.
- Element newValue = this.microLattice.Widen(aValue, bValue);
- newMap = newMap.Add(key, newValue);
- }
- }
- Element/*!*/ widen= new Elt(newMap);
+ /// <summary>
+ /// Perform the pointwise widening of the elements in the map
+ /// </summary>
+ 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;
+
+ // Note we have to add those cases as we do not have a "NonTrivialWiden" method
+ if (a.IsBottom)
+ return new Elt(b.Constraints);
+ if (b.IsBottom)
+ return new Elt(a.Constraints);
+
+ IFunctionalMap newMap = FunctionalHashtable.Empty;
+ foreach (IVariable/*!*/ key in a.Variables) {
+ Contract.Assert(key != null);
+ Element aValue = a[key];
+ Element bValue = b[key];
+
+ if (aValue != null && bValue != null) {
+ // Keep only the variables known to both elements.
+ Element newValue = this.microLattice.Widen(aValue, bValue);
+ newMap = newMap.Add(key, newValue);
+ }
+ }
+ Element/*!*/ widen = new Elt(newMap);
Contract.Assert(widen != null);
- // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
+ // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
- return widen;
- }
+ return widen;
+ }
- 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();
+ 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;
- IFunction lambda = e as IFunction;
+ IFunApp f = e as IFunApp;
+ IFunction lambda = e as IFunction;
- if (e is IVariable)
- {
- if (!ignoreVars.Contains(e))
- s.Add(e);
- }
- else if (f != null) // e is IFunApp
- {
- foreach(IExpr/*!*/ arg in f.Arguments){
-Contract.Assert(arg != null);
- s.AddAll(VariablesInExpression(arg, ignoreVars));
- }
- }
- else if (lambda != null)
+ if (e is IVariable) {
+ if (!ignoreVars.Contains(e))
+ s.Add(e);
+ } else if (f != null) // e is IFunApp
{
- IMutableSet x = new HashSet(1);
- x.Add(lambda.Param);
+ foreach (IExpr/*!*/ arg in f.Arguments) {
+ Contract.Assert(arg != null);
+ s.AddAll(VariablesInExpression(arg, ignoreVars));
+ }
+ } else if (lambda != null) {
+ IMutableSet x = new HashSet(1);
+ x.Add(lambda.Param);
+
+ // Ignore the bound variable
+ s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
+ } else if (e is IUnknown) {
+ // skip (actually, it would be appropriate to return the universal set of all variables)
+ } else {
+ Debug.Assert(false, "case not handled: " + e);
+ }
+ return s;
+ }
- // Ignore the bound variable
- s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
- }
- else if (e is IUnknown)
- {
- // skip (actually, it would be appropriate to return the universal set of all variables)
- }
- else
- {
- Debug.Assert(false, "case not handled: " + e);
- }
- return s;
+
+ private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e) {
+ Contract.Ensures(Contract.Result<ArrayList>() != null);
+ ArrayList result = new ArrayList();
+
+ IFunApp f = e as IFunApp;
+ if (f != null) {
+ if (f.FunctionSymbol.Equals(Prop.And)) {
+ foreach (IExpr arg in f.Arguments) {
+ result.AddRange(FindConjuncts(arg));
+ }
+ } else if (f.FunctionSymbol.Equals(Prop.Or)
+ || f.FunctionSymbol.Equals(Prop.Implies)) {
+ // Do nothing.
+ } else {
+ result.Add(e);
}
+ } else {
+ result.Add(e);
+ }
+ return result;
+ }
- private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e)
- {
- Contract.Ensures(Contract.Result<ArrayList>() != null);
- ArrayList result = new ArrayList();
+ private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right) {
+ Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
+ left = null;
+ right = null;
- IFunApp f = e as IFunApp;
- if (f != null)
- {
- if (f.FunctionSymbol.Equals(Prop.And))
- {
- foreach (IExpr arg in f.Arguments)
- {
- result.AddRange(FindConjuncts(arg));
- }
- }
- else if (f.FunctionSymbol.Equals(Prop.Or)
- || f.FunctionSymbol.Equals(Prop.Implies))
- {
- // Do nothing.
- }
- else
- {
- result.Add(e);
- }
- }
- else
- {
- result.Add(e);
- }
+ // See if we have an equality
+ IFunApp nary = expr as IFunApp;
+ if (nary == null || !nary.FunctionSymbol.Equals(Value.Eq)) {
+ return false;
+ }
- return result;
- }
+ // See if it is an equality of two variables
+ IVariable idLeft = nary.Arguments[0] as IVariable;
+ IVariable idRight = nary.Arguments[1] as IVariable;
+ if (idLeft == null || idRight == null) {
+ return false;
+ }
- private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right)
- {
- Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
- left = null;
- right = null;
-
- // See if we have an equality
- IFunApp nary = expr as IFunApp;
- if (nary == null || !nary.FunctionSymbol.Equals(Value.Eq)) { return false; }
-
- // See if it is an equality of two variables
- IVariable idLeft = nary.Arguments[0] as IVariable;
- IVariable idRight = nary.Arguments[1] as IVariable;
- if (idLeft == null || idRight == null) { return false; }
-
- left = idLeft;
- right = idRight;
- return true;
- }
+ left = idLeft;
+ right = idRight;
+ return true;
+ }
- /// <summary>
- /// Returns true iff the expression is in the form var == arithmeticExpr
- /// </summary>
- 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
- return true;
- else if(expr is IFunApp) // may be ==, +, -, /, % or an integer
+ /// <summary>
+ /// Returns true iff the expression is in the form var == arithmeticExpr
+ /// </summary>
+ 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
+ return true;
+ else if (expr is IFunApp) // may be ==, +, -, /, % or an integer
{
- IFunApp fun = (IFunApp) expr;
+ IFunApp fun = (IFunApp)expr;
+
+ 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/*!*/)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/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
- 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/*!*/)cce.NonNull(fun.Arguments[0]));
- else if(fun.Arguments.Count != 2) // A function of two or more operands is not arithmetic
+ if (!(left is IVariable || right is IVariable)) // At least one of the two operands must be a variable
return false;
- else
- {
- 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;
-
- if(fun.FunctionSymbol.Equals(Value.Eq)
- || fun.FunctionSymbol.Equals(Int.Add)
- || fun.FunctionSymbol.Equals(Int.Sub)
- || fun.FunctionSymbol.Equals(Int.Mul)
- || fun.FunctionSymbol.Equals(Int.Div)
- || fun.FunctionSymbol.Equals(Int.Mod))
- return IsArithmeticExpr(left) && IsArithmeticExpr(right);
- else
- return false;
- }
- }
+
+ if (fun.FunctionSymbol.Equals(Value.Eq)
+ || fun.FunctionSymbol.Equals(Int.Add)
+ || fun.FunctionSymbol.Equals(Int.Sub)
+ || fun.FunctionSymbol.Equals(Int.Mul)
+ || fun.FunctionSymbol.Equals(Int.Div)
+ || fun.FunctionSymbol.Equals(Int.Mod))
+ return IsArithmeticExpr(left) && IsArithmeticExpr(right);
else
- {
- return false;
- }
+ return false;
+ }
+ } else {
+ return false;
}
+ }
- 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; }
-
- Elt e = (Elt)element;
- IExpr truth = propExprFactory.True;
- IExpr result = truth;
-
- foreach(IVariable/*!*/ variable in e.SortedVariables(variableComparer)){
-Contract.Assert(variable != null);
- Element value = (Element)e[variable];
+ 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;
+ }
- if (value == null || this.microLattice.IsTop(value)) { continue; } // Skip variables about which we know nothing.
- if (this.microLattice.IsBottom(value)) { return propExprFactory.False; }
+ Elt e = (Elt)element;
+ IExpr truth = propExprFactory.True;
+ IExpr result = truth;
- IExpr conjunct = this.microLattice.ToPredicate(variable, value);
+ foreach (IVariable/*!*/ variable in e.SortedVariables(variableComparer)) {
+ Contract.Assert(variable != null);
+ Element value = (Element)e[variable];
- result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
- }
- return result;
+ if (value == null || this.microLattice.IsTop(value)) {
+ continue;
+ } // Skip variables about which we know nothing.
+ if (this.microLattice.IsBottom(value)) {
+ return propExprFactory.False;
}
+ IExpr conjunct = this.microLattice.ToPredicate(variable, value);
- 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);
+ result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
+ }
+ return result;
+ }
+
+
+ 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) {
+ //Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ return var;
+ }
+
+ /// <summary>
+ /// Return a new expression in which each variable has been
+ /// replaced by an expression representing what is known about
+ /// that variable.
+ /// </summary>
+ 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) {
+ /*MicroLattice*/
+ Element value = element[var];
+ if (notInlineable.Contains(var) || value == null || this.microLattice.IsTop(value)) {
+ return unableToInline(var); // We don't know anything about this variable.
+ } else {
+ // GetFoldExpr returns null when it can yield an expression that
+ // can be substituted for the variable.
+ IExpr valueExpr = this.microLattice.GetFoldExpr(value);
+ return (valueExpr == null) ? var : valueExpr;
}
+ }
+
+ // else
- private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
- private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var){
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- return var;
+ IFunApp fun = expr as IFunApp;
+ if (fun != null) {
+ IList newargs = new ArrayList();
+ foreach (IExpr/*!*/ arg in fun.Arguments) {
+ Contract.Assert(arg != null);
+ newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
}
+ return fun.CloneWithArguments(newargs);
+ }
- /// <summary>
- /// Return a new expression in which each variable has been
- /// replaced by an expression representing what is known about
- /// that variable.
- /// </summary>
- 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)
- {
- /*MicroLattice*/Element value = element[var];
- if (notInlineable.Contains(var) || value == null || this.microLattice.IsTop(value))
- {
- return unableToInline(var); // We don't know anything about this variable.
- }
- else
- {
- // GetFoldExpr returns null when it can yield an expression that
- // can be substituted for the variable.
- IExpr valueExpr = this.microLattice.GetFoldExpr(value);
- return (valueExpr == null) ? var : valueExpr;
- }
- }
+ // else
- // else
+ IFunction lambda = expr as IFunction;
+ if (lambda != null) {
+ IMutableSet x = new HashSet(1);
+ x.Add(lambda.Param);
- IFunApp fun = expr as IFunApp;
- if (fun != null)
- {
- IList newargs = new ArrayList();
- foreach(IExpr/*!*/ arg in fun.Arguments){
-Contract.Assert(arg != null);
- newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
- }
- return fun.CloneWithArguments(newargs);
- }
+ // Don't inline the bound variable
+ return lambda.CloneWithBody(
+ InlineVariables(element, lambda.Body,
+ cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
+ );
+ }
- // else
+ // else
- IFunction lambda = expr as IFunction;
- if (lambda != null)
- {
- IMutableSet x = new HashSet(1);
- x.Add(lambda.Param);
-
- // Don't inline the bound variable
- return lambda.CloneWithBody(
- InlineVariables(element, lambda.Body,
- cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
- );
- }
+ if (expr is IUnknown) {
+ return expr;
+ } else {
+ throw
+ new System.NotImplementedException("cannot inline identifies in expression " + expr);
+ }
+ }
- // else
-
- if (expr is IUnknown) {
- return expr;
- }
- else
- {
- throw
- new System.NotImplementedException("cannot inline identifies in expression " + expr);
- }
- }
+ 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
+ }
- 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);
+ expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
- if(IsBottom(element))
- {
- return result; // == element
- }
+ foreach (IExpr/*!*/ conjunct in FindConjuncts(expr)) {
+ Contract.Assert(conjunct != null);
+ IVariable left, right;
- expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
-
- foreach(IExpr/*!*/ conjunct in FindConjuncts(expr)){
-Contract.Assert(conjunct != null);
- IVariable left, right;
-
- if (IsSimpleEquality(conjunct, out left, out right))
- {
- #region The conjunct is a simple equality
-
-
- Contract.Assert(left != null && right != null);
-
- Element leftValue = result[left], rightValue = result[right];
- if (leftValue == null) { leftValue = this.microLattice.Top; }
- if (rightValue == null) { rightValue = this.microLattice.Top; }
- Element newValue = this.microLattice.Meet(leftValue, rightValue);
- result = AddConstraint(result, left, newValue);
- result = AddConstraint(result, right, newValue);
-
- #endregion
- }
- else
- {
- ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);
-
- if (variablesInvolved.Count == 1)
- {
- #region We have just one variable
-
- IVariable var = null;
- 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
- }
- else if(IsArithmeticExpr(conjunct) && this.microLattice.UnderstandsBasicArithmetics)
- {
- #region We evalaute an arithmetic expression
-
- IFunApp fun = (IFunApp) conjunct;
- if(fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
- {
- // get the variable to be assigned
- 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
- }
- }
- }
- return result;
- }
+ if (IsSimpleEquality(conjunct, out left, out right)) {
+ #region The conjunct is a simple equality
- 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;
- }
- else
- {
- return ((Elt)element).Rename(oldName, newName, this.microLattice);
- }
+ Contract.Assert(left != null && right != null);
+
+ Element leftValue = result[left], rightValue = result[right];
+ if (leftValue == null) {
+ leftValue = this.microLattice.Top;
+ }
+ if (rightValue == null) {
+ rightValue = this.microLattice.Top;
+ }
+ Element newValue = this.microLattice.Meet(leftValue, rightValue);
+ result = AddConstraint(result, left, newValue);
+ result = AddConstraint(result, right, newValue);
+
+ #endregion
+ } else {
+ ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);
+
+ if (variablesInvolved.Count == 1) {
+ #region We have just one variable
+
+ IVariable var = null;
+ 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
+ } else if (IsArithmeticExpr(conjunct) && this.microLattice.UnderstandsBasicArithmetics) {
+ #region We evalaute an arithmetic expression
+
+ IFunApp fun = (IFunApp)conjunct;
+ if (fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
+ {
+ // get the variable to be assigned
+ 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
+ }
}
+ }
+ return result;
+ }
- 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);
- }
+ 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;
+ } else {
+ return ((Elt)element).Rename(oldName, newName, this.microLattice);
+ }
+ }
- private sealed class EquivalentExprException :CheckedException { }
- private sealed class EquivalentExprInlineCallback
- {
- private readonly IVariable/*!*/ var;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(var != null);
- }
- public EquivalentExprInlineCallback(IVariable/*!*/ var){
-Contract.Requires(var != null);
- this.var = var;
- // base();
- }
+ 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);
+ }
- 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
- return othervar;
- }
- }
+ private sealed class EquivalentExprException : CheckedException {
+ }
+ private sealed class EquivalentExprInlineCallback {
+ private readonly IVariable/*!*/ var;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(var != null);
+ }
- 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, cce.NonNull(Set.Empty),
- new OnUnableToInline(closure.ThrowOnUnableToInline));
- }
- catch (EquivalentExprException)
- {
- return null;
- }
- }
+ public EquivalentExprInlineCallback(IVariable/*!*/ var) {
+ Contract.Requires(var != null);
+ this.var = var;
+ // base();
+ }
+
+ 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
+ return othervar;
+ }
+ }
+ 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, cce.NonNull(Set.Empty),
+ new OnUnableToInline(closure.ThrowOnUnableToInline));
+ } catch (EquivalentExprException) {
+ return null;
+ }
+ }
- /// <summary>
- /// Check to see if the given predicate holds in the given lattice element.
- ///
- /// TODO: We leave this unimplemented for now and just return maybe.
- /// </summary>
- /// <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){
-Contract.Requires(pred != null);
-Contract.Requires(e != null);
- return Answer.Maybe;
- }
- /// <summary>
- /// Answers a disequality about two variables. The same information could be obtained
- /// by asking CheckPredicate, but a different implementation may be simpler and more
- /// efficient.
- ///
- /// TODO: We leave this unimplemented for now and just return maybe.
- /// </summary>
- /// <param name="e">The lattice element.</param>
- /// <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){
-Contract.Requires(var2 != null);
-Contract.Requires(var1 != null);
-Contract.Requires(e != null);
- return Answer.Maybe;
- }
+ /// <summary>
+ /// Check to see if the given predicate holds in the given lattice element.
+ ///
+ /// TODO: We leave this unimplemented for now and just return maybe.
+ /// </summary>
+ /// <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) {
+ //Contract.Requires(pred != null);
+ //Contract.Requires(e != null);
+ return Answer.Maybe;
+ }
- public override void Validate()
- {
- base.Validate();
- microLattice.Validate();
- }
+ /// <summary>
+ /// Answers a disequality about two variables. The same information could be obtained
+ /// by asking CheckPredicate, but a different implementation may be simpler and more
+ /// efficient.
+ ///
+ /// TODO: We leave this unimplemented for now and just return maybe.
+ /// </summary>
+ /// <param name="e">The lattice element.</param>
+ /// <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) {
+ //Contract.Requires(var2 != null);
+ //Contract.Requires(var1 != null);
+ //Contract.Requires(e != null);
+ return Answer.Maybe;
+ }
+ public override void Validate() {
+ base.Validate();
+ microLattice.Validate();
}
+
+ }
}
|