diff options
Diffstat (limited to 'Source/AIFramework/VariableMap/Intervals.cs')
-rw-r--r-- | Source/AIFramework/VariableMap/Intervals.cs | 1742 |
1 files changed, 871 insertions, 871 deletions
diff --git a/Source/AIFramework/VariableMap/Intervals.cs b/Source/AIFramework/VariableMap/Intervals.cs index 0bf82cf4..98bf9007 100644 --- a/Source/AIFramework/VariableMap/Intervals.cs +++ b/Source/AIFramework/VariableMap/Intervals.cs @@ -1,871 +1,871 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections;
-//using System.Compiler.Analysis;
-using Microsoft.AbstractInterpretationFramework.Collections;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-
-/////////////////////////////////////////////////////////////////////////////////
-// An implementation of the interval abstract domain
-/////////////////////////////////////////////////////////////////////////////////
-
-namespace Microsoft.AbstractInterpretationFramework {
- public class IntervalLattice : MicroLattice {
- readonly ILinearExprFactory/*!*/ factory;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(factory != null);
- }
-
-
- public IntervalLattice(ILinearExprFactory/*!*/ factory) {
- Contract.Requires(factory != null);
- this.factory = factory;
- // base();
- }
-
- public override bool UnderstandsBasicArithmetics {
- get {
- return true;
- }
- }
-
- public override Element/*!*/ Top {
- get {
- Contract.Ensures(Contract.Result<Element>() != null);
-
- return IntervalElement.Top;
- }
- }
-
- public override Element/*!*/ Bottom {
- get {
- Contract.Ensures(Contract.Result<Element>() != null);
-
- return IntervalElement.Bottom;
- }
- }
-
- /// <summary>
- /// The paramter is the top?
- /// </summary>
- public override bool IsTop(Element/*!*/ element) {
- //Contract.Requires(element != null);
- IntervalElement interval = (IntervalElement)element;
-
- return interval.IsTop();
- }
-
- /// <summary>
- /// The parameter is the bottom?
- /// </summary>
- public override bool IsBottom(Element/*!*/ element) {
- //Contract.Requires(element != null);
- IntervalElement interval = (IntervalElement)element;
-
- return interval.IsBottom();
- }
-
- /// <summary>
- /// The classic, pointwise, join of intervals
- /// </summary>
- public override Element/*!*/ NontrivialJoin(Element/*!*/ left, Element/*!*/ right) {
- //Contract.Requires(right != null);
- //Contract.Requires(left != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
- IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
-
- ExtendedInt inf = ExtendedInt.Inf(leftInterval.Inf, rightInterval.Inf);
- ExtendedInt sup = ExtendedInt.Sup(leftInterval.Sup, rightInterval.Sup);
-
- IntervalElement/*!*/ join = IntervalElement.Factory(inf, sup);
-
- return join;
- }
-
- /// <summary>
- /// The classic, pointwise, meet of intervals
- /// </summary>
- public override Element/*!*/ NontrivialMeet(Element/*!*/ left, Element/*!*/ right) {
- //Contract.Requires(right != null);
- //Contract.Requires(left != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
- IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
-
- ExtendedInt inf = ExtendedInt.Sup(leftInterval.Inf, rightInterval.Inf);
- ExtendedInt sup = ExtendedInt.Inf(leftInterval.Sup, rightInterval.Sup);
-
- return IntervalElement.Factory(inf, sup);
- }
-
-
- /// <summary>
- /// The very simple widening of intervals, to be improved with thresholds
- /// left is the PREVIOUS value in the iterations and right is the NEW one
- /// </summary>
- public override Element/*!*/ Widen(Element/*!*/ left, Element/*!*/ right) {
- //Contract.Requires(right != null);
- //Contract.Requires(left != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- IntervalElement/*!*/ prevInterval = (IntervalElement/*!*/)cce.NonNull(left);
- IntervalElement/*!*/ nextInterval = (IntervalElement/*!*/)cce.NonNull(right);
-
- ExtendedInt inf = nextInterval.Inf < prevInterval.Inf ? ExtendedInt.MinusInfinity : prevInterval.Inf;
- ExtendedInt sup = nextInterval.Sup > prevInterval.Sup ? ExtendedInt.PlusInfinity : prevInterval.Sup;
-
- IntervalElement widening = IntervalElement.Factory(inf, sup);
-
- return widening;
- }
-
-
- /// <summary>
- /// 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);
- IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
- IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
-
- if (leftInterval.IsBottom() || rightInterval.IsTop())
- return true;
-
- return rightInterval.Inf <= leftInterval.Inf && leftInterval.Sup <= rightInterval.Sup;
- }
-
- /// <summary>
- /// Return just null
- /// </summary>
- public override IExpr GetFoldExpr(Element/*!*/ element) {
- //Contract.Requires(element != null);
- return null;
- }
-
- /// <summary>
- /// return a predicate inf "\leq x and x "\leq" sup (if inf [or sup] is not oo)
- /// </summary>
- public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
- //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;
-
- 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)) {
- IExpr constant = this.factory.Const(interval.Sup.Value);
- upperBound = this.factory.AtMost(var, constant); // var <= inf
- }
-
- if (lowerBound != null && upperBound != null)
- return this.factory.And(lowerBound, upperBound); // inf <= var && var <= sup
- else
- 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;
- }
-
- /// <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);
- return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- }
-
-
- /// <summary>
- /// Evaluate the predicate passed as input according the semantics of intervals
- /// </summary>
- public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ pred) {
- //Contract.Requires(pred != null);
- Contract.Ensures(Contract.Result<Element>() != null);
- return this.EvaluatePredicateWithState(pred, null);
- }
-
- /// <summary>
- /// Evaluate the predicate passed as input according the semantics of intervals and the given state.
- /// Right now just basic arithmetic operations are supported. A future extension may consider an implementation of boolean predicates
- /// </summary>
- public override Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ pred, IFunctionalMap/* Var -> Element */ state) {
- //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) {
- return Eval(rightArg, state);
- } else if (rightArg is IVariable) {
- return Eval(leftArg, state);
- }
- }
- }
- // otherwise we simply return 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);
-
- IntervalElement/*!*/ retVal = (IntervalElement/*!*/)cce.NonNull(Top);
-
- // Eval the expression by structural induction
-
-
- if (exp is IVariable && state != null) // A variable
- {
- object lookup = state[exp];
- 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
- {
- IntSymbol intSymb = (IntSymbol)fun.FunctionSymbol;
- BigNum val = intSymb.Value;
-
- retVal = IntervalElement.Factory(val);
- } 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) {
- 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))
- retVal = leftVal + rightVal;
- else if (fun.FunctionSymbol.Equals(Int.Sub))
- retVal = leftVal - rightVal;
- else if (fun.FunctionSymbol.Equals(Int.Mul))
- retVal = leftVal * rightVal;
- else if (fun.FunctionSymbol.Equals(Int.Div))
- retVal = leftVal / rightVal;
- else if (fun.FunctionSymbol.Equals(Int.Mod))
- retVal = leftVal % rightVal;
- }
- }
-
- return retVal;
- }
-
- /// <summary>
- /// Inner class standing for an interval on integers, possibly unbounded
- /// </summary>
- private class IntervalElement : Element {
- protected static readonly IntervalElement/*!*/ TopInterval = new IntervalElement(new MinusInfinity(), new PlusInfinity()); // Top = [-oo , +oo]
- protected static readonly IntervalElement/*!*/ BottomInterval = new IntervalElement(new PlusInfinity(), new MinusInfinity()); // Bottom = [+oo, -oo]
-
- private readonly ExtendedInt/*!*/ inf;
- private readonly ExtendedInt/*!*/ sup;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(inf != null);
- Contract.Invariant(sup != null);
- }
-
- public ExtendedInt/*!*/ Inf {
- get {
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-
- return inf;
- }
- }
-
- public ExtendedInt/*!*/ Sup {
- get {
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-
- return sup;
- }
- }
-
- // Construct the inteval [val, val]
- protected IntervalElement(BigNum val) {
- this.inf = this.sup = ExtendedInt.Factory(val);
- // base();
- }
-
- // Construct the interval [inf, sup]
- protected IntervalElement(BigNum infInt, BigNum supInt) {
- this.inf = ExtendedInt.Factory(infInt);
- this.sup = ExtendedInt.Factory(supInt);
- // base(); // to please the compiler...
- }
-
- protected IntervalElement(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
- Contract.Requires(sup != null);
- Contract.Requires(inf != null);
- this.inf = inf;
- this.sup = sup;
- // base();
- }
-
- // Construct an Interval
- public static IntervalElement/*!*/ Factory(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
- Contract.Requires((sup != null));
- Contract.Requires((inf != null));
- Contract.Ensures(Contract.Result<IntervalElement>() != null);
- if (inf is MinusInfinity && sup is PlusInfinity)
- return Top;
- if (inf > sup)
- return Bottom;
- // otherwise...
- return new IntervalElement(inf, sup);
- }
-
- public static IntervalElement/*!*/ Factory(BigNum i) {
- Contract.Ensures(Contract.Result<IntervalElement>() != null);
- return new IntervalElement(i);
- }
-
- public static IntervalElement/*!*/ Factory(BigNum inf, BigNum sup) {
- Contract.Ensures(Contract.Result<IntervalElement>() != null);
- ExtendedInt/*!*/ i = ExtendedInt.Factory(inf);
- ExtendedInt/*!*/ s = ExtendedInt.Factory(sup);
-
- return Factory(i, s);
- }
-
- static public IntervalElement/*!*/ Top {
- get {
- Contract.Ensures(Contract.Result<IntervalElement>() != null);
-
- return TopInterval;
- }
- }
-
- static public IntervalElement/*!*/ Bottom {
- get {
- Contract.Ensures(Contract.Result<IntervalElement>() != null);
-
- return BottomInterval;
- }
- }
-
- public bool IsTop() {
- return this.inf is MinusInfinity && this.sup is PlusInfinity;
- }
-
- public bool IsBottom() {
- return this.inf > this.sup;
- }
-
- #region Below are the arithmetic operations lifted to intervals
-
- // Addition
- public static IntervalElement/*!*/ operator +(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<IntervalElement>() != null);
- ExtendedInt/*!*/ inf = a.inf + b.inf;
- Contract.Assert(inf != null);
- ExtendedInt/*!*/ sup = a.sup + b.sup;
- Contract.Assert(sup != null);
-
- return Factory(inf, sup);
- }
-
- // Subtraction
- public static IntervalElement/*!*/ operator -(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<IntervalElement>() != null);
- ExtendedInt/*!*/ inf = a.inf - b.sup;
- Contract.Assert(inf != null);
-
- ExtendedInt/*!*/ sup = a.sup - b.inf;
- Contract.Assert(sup != null);
- IntervalElement/*!*/ sub = Factory(inf, sup);
- Contract.Assert(sub != null);
-
- return sub;
- }
-
- // Multiplication
- public static IntervalElement/*!*/ operator *(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
- 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);
- }
-
- // 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);
- }
-
- #endregion
-
- #region Overriden methods
-
- public override Element/*!*/ Clone() {
- Contract.Ensures(Contract.Result<Element>() != null);
- // Real copying should not be needed because intervals are immutable?
- return this;
- /*
- int valInf = this.inf.Value;
- int valSup = this.sup.Value;
-
- ExtendedInt clonedInf = ExtendedInt.Factory(valInf);
- ExtendedInt clonedSup = ExtendedInt.Factory(valSup);
-
- return Factory(clonedInf, clonedSup);
- */
- }
-
- [Pure]
- public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
- Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
- return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
- }
-
- [Pure]
- public override string/*!*/ ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return "[" + this.inf + ", " + this.sup + "]";
- }
-
- #endregion
- }
- }
-
-
- /// The interface for an extended integer
- ///
- [ContractClass(typeof(ExtendedIntContracts))]
- abstract class ExtendedInt {
- private static readonly PlusInfinity/*!*/ cachedPlusInf = new PlusInfinity();
- private static readonly MinusInfinity/*!*/ cachedMinusInf = new MinusInfinity();
-
- static public ExtendedInt/*!*/ PlusInfinity {
- get {
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-
- return cachedPlusInf;
- }
- }
-
- static public ExtendedInt/*!*/ MinusInfinity {
- get {
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
-
- return cachedMinusInf;
- }
- }
-
- public abstract BigNum Value {
- get;
- }
-
- public abstract int Signum {
- get;
- }
-
- public bool IsZero {
- get {
- return Signum == 0;
- }
- }
-
- public bool IsPositive {
- get {
- return Signum > 0;
- }
- }
-
- public bool IsNegative {
- get {
- return Signum < 0;
- }
- }
-
-
- #region Below are the extensions of arithmetic operations on extended integers
-
- // Addition
- public static ExtendedInt/*!*/ operator +(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return b;
- } else {
- return ExtendedInt.Factory(a.Value + b.Value);
- }
- }
-
- // Subtraction
- public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return UnaryMinus(b);
- } else {
- return ExtendedInt.Factory(a.Value - b.Value);
- }
- }
-
- // Unary minus
- public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a) {
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- // BUGBUG: Some compiler error prevents the unary minus operator from being used
- return UnaryMinus(a);
- }
-
- // Unary minus
- public static ExtendedInt/*!*/ UnaryMinus(ExtendedInt/*!*/ a) {
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- if (a is PlusInfinity)
- return cachedMinusInf;
- if (a is MinusInfinity)
- return cachedPlusInf;
- else // a is a PureInteger
- return new PureInteger(-a.Value);
- }
-
- // Multiplication
- public static ExtendedInt/*!*/ operator *(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- if (a.IsZero) {
- return a;
- } else if (b.IsZero) {
- return b;
- } else if (a is InfinitaryInt) {
- if (b.IsPositive) {
- return a;
- } else {
- return UnaryMinus(a);
- }
- } else if (b is InfinitaryInt) {
- if (a.IsPositive) {
- return b;
- } else {
- return UnaryMinus(b);
- }
- } else {
- return ExtendedInt.Factory(a.Value * b.Value);
- }
- }
-
- // Division
- public static ExtendedInt/*!*/ operator /(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- if (b.IsZero) {
- return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
- }
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return b;
- } else {
- return ExtendedInt.Factory(a.Value / b.Value);
- }
- }
-
- // Modulo
- public static ExtendedInt/*!*/ operator %(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- if (b.IsZero) {
- return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf;
- }
- if (a is InfinitaryInt) {
- return a;
- } else if (b is InfinitaryInt) {
- return b;
- } else {
- return ExtendedInt.Factory(a.Value % b.Value);
- }
- }
-
- #endregion
-
- #region Inf and Sup operations
-
- public abstract int CompareTo(ExtendedInt/*!*/ that);
-
- public static bool operator <(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
- Contract.Requires(sup != null);
- Contract.Requires(inf != null);
- return inf.CompareTo(sup) < 0;
- }
-
- public static bool operator >(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
- Contract.Requires(sup != null);
- Contract.Requires(inf != null);
- return inf.CompareTo(sup) > 0;
- }
-
- public static bool operator <=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
- Contract.Requires(sup != null);
- Contract.Requires(inf != null);
- return inf.CompareTo(sup) <= 0;
- }
-
- public static bool operator >=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
- Contract.Requires(sup != null);
- Contract.Requires(inf != null);
- Contract.Requires(inf != null && sup != null);
- return inf.CompareTo(sup) >= 0;
- }
-
- public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
- Contract.Requires(sup != null);
- Contract.Requires(inf != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- if (inf < sup)
- return inf;
- else
- return sup;
- }
-
- public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) {
- Contract.Requires(d != null);
- Contract.Requires(c != null);
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- ExtendedInt/*!*/ infab = Inf(a, b);
- Contract.Assert(infab != null);
- ExtendedInt/*!*/ infcd = Inf(c, d);
- Contract.Assert(infcd != null);
-
- return Inf(infab, infcd);
- }
-
- public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
- Contract.Requires(sup != null);
- Contract.Requires(inf != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- if (inf > sup)
- return inf;
- else
- return sup;
- }
-
- public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) {
- Contract.Requires(d != null);
- Contract.Requires(c != null);
- Contract.Requires(b != null);
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- ExtendedInt/*!*/ supab = Sup(a, b);
- Contract.Assert(supab != null);
- ExtendedInt/*!*/ supcd = Sup(c, d);
- Contract.Assert(supcd != null);
-
- return Sup(supab, supcd);
- }
-
- #endregion
-
- // Return the ExtendedInt corresponding to the value
- public static ExtendedInt/*!*/ Factory(BigNum val) {
- Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- return new PureInteger(val);
- }
- }
- [ContractClassFor(typeof(ExtendedInt))]
- abstract class ExtendedIntContracts : ExtendedInt {
- public override int CompareTo(ExtendedInt that) {
- Contract.Requires(that != null);
- throw new NotImplementedException();
- }
- }
-
- // Stands for a normal (finite) integer x
- class PureInteger : ExtendedInt {
- public PureInteger(BigNum i) {
- this.val = i;
- }
-
- [Pure]
- public override string/*!*/ ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return this.Value.ToString();
- }
-
- private BigNum val;
- public override BigNum Value {
- get {
- return this.val;
- }
- }
-
- public override int Signum {
- get {
- return val.Signum;
- }
- }
-
- public override int CompareTo(ExtendedInt/*!*/ that) {
- //Contract.Requires(that != null);
- if (that is PlusInfinity)
- return -1;
- else if (that is PureInteger)
- return this.Value.CompareTo(that.Value);
- else // then that is a MinusInfinity
- return 1;
- }
- }
-
- abstract class InfinitaryInt : ExtendedInt {
- public override BigNum Value {
- get {
- throw new InvalidOperationException();
- }
- }
- }
-
- class PlusInfinity : InfinitaryInt {
- [Pure]
- public override string/*!*/ ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return "+oo";
- }
-
- public override int Signum {
- get {
- return 1;
- }
- }
-
- public override int CompareTo(ExtendedInt/*!*/ that) {
- //Contract.Requires(that != null);
- if (that is PlusInfinity)
- return 0;
- else
- return 1;
- }
- }
-
- class MinusInfinity : InfinitaryInt {
- [Pure]
- public override string/*!*/ ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return "-oo";
- }
-
- public override int Signum {
- get {
- return -1;
- }
- }
-
- public override int CompareTo(ExtendedInt/*!*/ that) {
- //Contract.Requires(that != null);
- if (that is MinusInfinity)
- return 0;
- else
- return -1;
- }
- }
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections; +//using System.Compiler.Analysis; +using Microsoft.AbstractInterpretationFramework.Collections; +using System.Diagnostics.Contracts; +using Microsoft.Basetypes; + +///////////////////////////////////////////////////////////////////////////////// +// An implementation of the interval abstract domain +///////////////////////////////////////////////////////////////////////////////// + +namespace Microsoft.AbstractInterpretationFramework { + public class IntervalLattice : MicroLattice { + readonly ILinearExprFactory/*!*/ factory; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(factory != null); + } + + + public IntervalLattice(ILinearExprFactory/*!*/ factory) { + Contract.Requires(factory != null); + this.factory = factory; + // base(); + } + + public override bool UnderstandsBasicArithmetics { + get { + return true; + } + } + + public override Element/*!*/ Top { + get { + Contract.Ensures(Contract.Result<Element>() != null); + + return IntervalElement.Top; + } + } + + public override Element/*!*/ Bottom { + get { + Contract.Ensures(Contract.Result<Element>() != null); + + return IntervalElement.Bottom; + } + } + + /// <summary> + /// The paramter is the top? + /// </summary> + public override bool IsTop(Element/*!*/ element) { + //Contract.Requires(element != null); + IntervalElement interval = (IntervalElement)element; + + return interval.IsTop(); + } + + /// <summary> + /// The parameter is the bottom? + /// </summary> + public override bool IsBottom(Element/*!*/ element) { + //Contract.Requires(element != null); + IntervalElement interval = (IntervalElement)element; + + return interval.IsBottom(); + } + + /// <summary> + /// The classic, pointwise, join of intervals + /// </summary> + public override Element/*!*/ NontrivialJoin(Element/*!*/ left, Element/*!*/ right) { + //Contract.Requires(right != null); + //Contract.Requires(left != null); + Contract.Ensures(Contract.Result<Element>() != null); + IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left); + IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right); + + ExtendedInt inf = ExtendedInt.Inf(leftInterval.Inf, rightInterval.Inf); + ExtendedInt sup = ExtendedInt.Sup(leftInterval.Sup, rightInterval.Sup); + + IntervalElement/*!*/ join = IntervalElement.Factory(inf, sup); + + return join; + } + + /// <summary> + /// The classic, pointwise, meet of intervals + /// </summary> + public override Element/*!*/ NontrivialMeet(Element/*!*/ left, Element/*!*/ right) { + //Contract.Requires(right != null); + //Contract.Requires(left != null); + Contract.Ensures(Contract.Result<Element>() != null); + IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left); + IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right); + + ExtendedInt inf = ExtendedInt.Sup(leftInterval.Inf, rightInterval.Inf); + ExtendedInt sup = ExtendedInt.Inf(leftInterval.Sup, rightInterval.Sup); + + return IntervalElement.Factory(inf, sup); + } + + + /// <summary> + /// The very simple widening of intervals, to be improved with thresholds + /// left is the PREVIOUS value in the iterations and right is the NEW one + /// </summary> + public override Element/*!*/ Widen(Element/*!*/ left, Element/*!*/ right) { + //Contract.Requires(right != null); + //Contract.Requires(left != null); + Contract.Ensures(Contract.Result<Element>() != null); + IntervalElement/*!*/ prevInterval = (IntervalElement/*!*/)cce.NonNull(left); + IntervalElement/*!*/ nextInterval = (IntervalElement/*!*/)cce.NonNull(right); + + ExtendedInt inf = nextInterval.Inf < prevInterval.Inf ? ExtendedInt.MinusInfinity : prevInterval.Inf; + ExtendedInt sup = nextInterval.Sup > prevInterval.Sup ? ExtendedInt.PlusInfinity : prevInterval.Sup; + + IntervalElement widening = IntervalElement.Factory(inf, sup); + + return widening; + } + + + /// <summary> + /// 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); + IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left); + IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right); + + if (leftInterval.IsBottom() || rightInterval.IsTop()) + return true; + + return rightInterval.Inf <= leftInterval.Inf && leftInterval.Sup <= rightInterval.Sup; + } + + /// <summary> + /// Return just null + /// </summary> + public override IExpr GetFoldExpr(Element/*!*/ element) { + //Contract.Requires(element != null); + return null; + } + + /// <summary> + /// return a predicate inf "\leq x and x "\leq" sup (if inf [or sup] is not oo) + /// </summary> + public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) { + //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; + + 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)) { + IExpr constant = this.factory.Const(interval.Sup.Value); + upperBound = this.factory.AtMost(var, constant); // var <= inf + } + + if (lowerBound != null && upperBound != null) + return this.factory.And(lowerBound, upperBound); // inf <= var && var <= sup + else + 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; + } + + /// <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); + return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq); + } + + + /// <summary> + /// Evaluate the predicate passed as input according the semantics of intervals + /// </summary> + public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ pred) { + //Contract.Requires(pred != null); + Contract.Ensures(Contract.Result<Element>() != null); + return this.EvaluatePredicateWithState(pred, null); + } + + /// <summary> + /// Evaluate the predicate passed as input according the semantics of intervals and the given state. + /// Right now just basic arithmetic operations are supported. A future extension may consider an implementation of boolean predicates + /// </summary> + public override Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ pred, IFunctionalMap/* Var -> Element */ state) { + //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) { + return Eval(rightArg, state); + } else if (rightArg is IVariable) { + return Eval(leftArg, state); + } + } + } + // otherwise we simply return 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); + + IntervalElement/*!*/ retVal = (IntervalElement/*!*/)cce.NonNull(Top); + + // Eval the expression by structural induction + + + if (exp is IVariable && state != null) // A variable + { + object lookup = state[exp]; + 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 + { + IntSymbol intSymb = (IntSymbol)fun.FunctionSymbol; + BigNum val = intSymb.Value; + + retVal = IntervalElement.Factory(val); + } 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) { + 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)) + retVal = leftVal + rightVal; + else if (fun.FunctionSymbol.Equals(Int.Sub)) + retVal = leftVal - rightVal; + else if (fun.FunctionSymbol.Equals(Int.Mul)) + retVal = leftVal * rightVal; + else if (fun.FunctionSymbol.Equals(Int.Div)) + retVal = leftVal / rightVal; + else if (fun.FunctionSymbol.Equals(Int.Mod)) + retVal = leftVal % rightVal; + } + } + + return retVal; + } + + /// <summary> + /// Inner class standing for an interval on integers, possibly unbounded + /// </summary> + private class IntervalElement : Element { + protected static readonly IntervalElement/*!*/ TopInterval = new IntervalElement(new MinusInfinity(), new PlusInfinity()); // Top = [-oo , +oo] + protected static readonly IntervalElement/*!*/ BottomInterval = new IntervalElement(new PlusInfinity(), new MinusInfinity()); // Bottom = [+oo, -oo] + + private readonly ExtendedInt/*!*/ inf; + private readonly ExtendedInt/*!*/ sup; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(inf != null); + Contract.Invariant(sup != null); + } + + public ExtendedInt/*!*/ Inf { + get { + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + + return inf; + } + } + + public ExtendedInt/*!*/ Sup { + get { + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + + return sup; + } + } + + // Construct the inteval [val, val] + protected IntervalElement(BigNum val) { + this.inf = this.sup = ExtendedInt.Factory(val); + // base(); + } + + // Construct the interval [inf, sup] + protected IntervalElement(BigNum infInt, BigNum supInt) { + this.inf = ExtendedInt.Factory(infInt); + this.sup = ExtendedInt.Factory(supInt); + // base(); // to please the compiler... + } + + protected IntervalElement(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) { + Contract.Requires(sup != null); + Contract.Requires(inf != null); + this.inf = inf; + this.sup = sup; + // base(); + } + + // Construct an Interval + public static IntervalElement/*!*/ Factory(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) { + Contract.Requires((sup != null)); + Contract.Requires((inf != null)); + Contract.Ensures(Contract.Result<IntervalElement>() != null); + if (inf is MinusInfinity && sup is PlusInfinity) + return Top; + if (inf > sup) + return Bottom; + // otherwise... + return new IntervalElement(inf, sup); + } + + public static IntervalElement/*!*/ Factory(BigNum i) { + Contract.Ensures(Contract.Result<IntervalElement>() != null); + return new IntervalElement(i); + } + + public static IntervalElement/*!*/ Factory(BigNum inf, BigNum sup) { + Contract.Ensures(Contract.Result<IntervalElement>() != null); + ExtendedInt/*!*/ i = ExtendedInt.Factory(inf); + ExtendedInt/*!*/ s = ExtendedInt.Factory(sup); + + return Factory(i, s); + } + + static public IntervalElement/*!*/ Top { + get { + Contract.Ensures(Contract.Result<IntervalElement>() != null); + + return TopInterval; + } + } + + static public IntervalElement/*!*/ Bottom { + get { + Contract.Ensures(Contract.Result<IntervalElement>() != null); + + return BottomInterval; + } + } + + public bool IsTop() { + return this.inf is MinusInfinity && this.sup is PlusInfinity; + } + + public bool IsBottom() { + return this.inf > this.sup; + } + + #region Below are the arithmetic operations lifted to intervals + + // Addition + public static IntervalElement/*!*/ operator +(IntervalElement/*!*/ a, IntervalElement/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<IntervalElement>() != null); + ExtendedInt/*!*/ inf = a.inf + b.inf; + Contract.Assert(inf != null); + ExtendedInt/*!*/ sup = a.sup + b.sup; + Contract.Assert(sup != null); + + return Factory(inf, sup); + } + + // Subtraction + public static IntervalElement/*!*/ operator -(IntervalElement/*!*/ a, IntervalElement/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<IntervalElement>() != null); + ExtendedInt/*!*/ inf = a.inf - b.sup; + Contract.Assert(inf != null); + + ExtendedInt/*!*/ sup = a.sup - b.inf; + Contract.Assert(sup != null); + IntervalElement/*!*/ sub = Factory(inf, sup); + Contract.Assert(sub != null); + + return sub; + } + + // Multiplication + public static IntervalElement/*!*/ operator *(IntervalElement/*!*/ a, IntervalElement/*!*/ b) { + 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); + } + + // 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); + } + + #endregion + + #region Overriden methods + + public override Element/*!*/ Clone() { + Contract.Ensures(Contract.Result<Element>() != null); + // Real copying should not be needed because intervals are immutable? + return this; + /* + int valInf = this.inf.Value; + int valSup = this.sup.Value; + + ExtendedInt clonedInf = ExtendedInt.Factory(valInf); + ExtendedInt clonedSup = ExtendedInt.Factory(valSup); + + return Factory(clonedInf, clonedSup); + */ + } + + [Pure] + public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() { + Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>())); + return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly(); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result<string>() != null); + return "[" + this.inf + ", " + this.sup + "]"; + } + + #endregion + } + } + + + /// The interface for an extended integer + /// + [ContractClass(typeof(ExtendedIntContracts))] + abstract class ExtendedInt { + private static readonly PlusInfinity/*!*/ cachedPlusInf = new PlusInfinity(); + private static readonly MinusInfinity/*!*/ cachedMinusInf = new MinusInfinity(); + + static public ExtendedInt/*!*/ PlusInfinity { + get { + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + + return cachedPlusInf; + } + } + + static public ExtendedInt/*!*/ MinusInfinity { + get { + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + + return cachedMinusInf; + } + } + + public abstract BigNum Value { + get; + } + + public abstract int Signum { + get; + } + + public bool IsZero { + get { + return Signum == 0; + } + } + + public bool IsPositive { + get { + return Signum > 0; + } + } + + public bool IsNegative { + get { + return Signum < 0; + } + } + + + #region Below are the extensions of arithmetic operations on extended integers + + // Addition + public static ExtendedInt/*!*/ operator +(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + if (a is InfinitaryInt) { + return a; + } else if (b is InfinitaryInt) { + return b; + } else { + return ExtendedInt.Factory(a.Value + b.Value); + } + } + + // Subtraction + public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + if (a is InfinitaryInt) { + return a; + } else if (b is InfinitaryInt) { + return UnaryMinus(b); + } else { + return ExtendedInt.Factory(a.Value - b.Value); + } + } + + // Unary minus + public static ExtendedInt/*!*/ operator -(ExtendedInt/*!*/ a) { + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + // BUGBUG: Some compiler error prevents the unary minus operator from being used + return UnaryMinus(a); + } + + // Unary minus + public static ExtendedInt/*!*/ UnaryMinus(ExtendedInt/*!*/ a) { + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + if (a is PlusInfinity) + return cachedMinusInf; + if (a is MinusInfinity) + return cachedPlusInf; + else // a is a PureInteger + return new PureInteger(-a.Value); + } + + // Multiplication + public static ExtendedInt/*!*/ operator *(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + if (a.IsZero) { + return a; + } else if (b.IsZero) { + return b; + } else if (a is InfinitaryInt) { + if (b.IsPositive) { + return a; + } else { + return UnaryMinus(a); + } + } else if (b is InfinitaryInt) { + if (a.IsPositive) { + return b; + } else { + return UnaryMinus(b); + } + } else { + return ExtendedInt.Factory(a.Value * b.Value); + } + } + + // Division + public static ExtendedInt/*!*/ operator /(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + if (b.IsZero) { + return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf; + } + if (a is InfinitaryInt) { + return a; + } else if (b is InfinitaryInt) { + return b; + } else { + return ExtendedInt.Factory(a.Value / b.Value); + } + } + + // Modulo + public static ExtendedInt/*!*/ operator %(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + if (b.IsZero) { + return a.IsPositive ? (ExtendedInt)cachedPlusInf : cachedMinusInf; + } + if (a is InfinitaryInt) { + return a; + } else if (b is InfinitaryInt) { + return b; + } else { + return ExtendedInt.Factory(a.Value % b.Value); + } + } + + #endregion + + #region Inf and Sup operations + + public abstract int CompareTo(ExtendedInt/*!*/ that); + + public static bool operator <(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) { + Contract.Requires(sup != null); + Contract.Requires(inf != null); + return inf.CompareTo(sup) < 0; + } + + public static bool operator >(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) { + Contract.Requires(sup != null); + Contract.Requires(inf != null); + return inf.CompareTo(sup) > 0; + } + + public static bool operator <=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) { + Contract.Requires(sup != null); + Contract.Requires(inf != null); + return inf.CompareTo(sup) <= 0; + } + + public static bool operator >=(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) { + Contract.Requires(sup != null); + Contract.Requires(inf != null); + Contract.Requires(inf != null && sup != null); + return inf.CompareTo(sup) >= 0; + } + + public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) { + Contract.Requires(sup != null); + Contract.Requires(inf != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + if (inf < sup) + return inf; + else + return sup; + } + + public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) { + Contract.Requires(d != null); + Contract.Requires(c != null); + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + ExtendedInt/*!*/ infab = Inf(a, b); + Contract.Assert(infab != null); + ExtendedInt/*!*/ infcd = Inf(c, d); + Contract.Assert(infcd != null); + + return Inf(infab, infcd); + } + + public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) { + Contract.Requires(sup != null); + Contract.Requires(inf != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + if (inf > sup) + return inf; + else + return sup; + } + + public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) { + Contract.Requires(d != null); + Contract.Requires(c != null); + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + ExtendedInt/*!*/ supab = Sup(a, b); + Contract.Assert(supab != null); + ExtendedInt/*!*/ supcd = Sup(c, d); + Contract.Assert(supcd != null); + + return Sup(supab, supcd); + } + + #endregion + + // Return the ExtendedInt corresponding to the value + public static ExtendedInt/*!*/ Factory(BigNum val) { + Contract.Ensures(Contract.Result<ExtendedInt>() != null); + return new PureInteger(val); + } + } + [ContractClassFor(typeof(ExtendedInt))] + abstract class ExtendedIntContracts : ExtendedInt { + public override int CompareTo(ExtendedInt that) { + Contract.Requires(that != null); + throw new NotImplementedException(); + } + } + + // Stands for a normal (finite) integer x + class PureInteger : ExtendedInt { + public PureInteger(BigNum i) { + this.val = i; + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result<string>() != null); + return this.Value.ToString(); + } + + private BigNum val; + public override BigNum Value { + get { + return this.val; + } + } + + public override int Signum { + get { + return val.Signum; + } + } + + public override int CompareTo(ExtendedInt/*!*/ that) { + //Contract.Requires(that != null); + if (that is PlusInfinity) + return -1; + else if (that is PureInteger) + return this.Value.CompareTo(that.Value); + else // then that is a MinusInfinity + return 1; + } + } + + abstract class InfinitaryInt : ExtendedInt { + public override BigNum Value { + get { + throw new InvalidOperationException(); + } + } + } + + class PlusInfinity : InfinitaryInt { + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result<string>() != null); + return "+oo"; + } + + public override int Signum { + get { + return 1; + } + } + + public override int CompareTo(ExtendedInt/*!*/ that) { + //Contract.Requires(that != null); + if (that is PlusInfinity) + return 0; + else + return 1; + } + } + + class MinusInfinity : InfinitaryInt { + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result<string>() != null); + return "-oo"; + } + + public override int Signum { + get { + return -1; + } + } + + public override int CompareTo(ExtendedInt/*!*/ that) { + //Contract.Requires(that != null); + if (that is MinusInfinity) + return 0; + else + return -1; + } + } +} |