diff options
Diffstat (limited to 'Source/AIFramework/VariableMap/ConstantAbstraction.cs')
-rw-r--r-- | Source/AIFramework/VariableMap/ConstantAbstraction.cs | 502 |
1 files changed, 251 insertions, 251 deletions
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.cs b/Source/AIFramework/VariableMap/ConstantAbstraction.cs index d8f17a3c..d73fc28b 100644 --- a/Source/AIFramework/VariableMap/ConstantAbstraction.cs +++ b/Source/AIFramework/VariableMap/ConstantAbstraction.cs @@ -1,251 +1,251 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System.Diagnostics.Contracts;
-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
- }
-
- private class Elt : Element {
- public Value domainValue;
- public BigNum constantValue; // valid iff domainValue == Value.Constant
-
- public Elt(Value v) {
- this.domainValue = v;
- }
-
- public Elt(BigNum i) {
- this.domainValue = Value.Constant;
- this.constantValue = i;
- }
-
- public bool IsConstant {
- get {
- return this.domainValue == Value.Constant;
- }
- }
-
- 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();
- }
-
- 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);
- }
-
-
- 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/*!*/ 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 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/*!*/ 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);
- }
-
- protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
- {
- //Contract.Requires(first!= null);
- //Contract.Requires(second != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- return a.Constant.Equals(b.Constant);
- }
-
- public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
- //Contract.Requires(element != null);
- //Contract.Requires(var != null);
- Contract.Ensures(Contract.Result<IExpr>() != null);
- return factory.Eq(var, cce.NonNull(GetFoldExpr(element)));
- }
-
- public override IExpr GetFoldExpr(Element/*!*/ element) {
- //Contract.Requires(element != null);
- Elt e = (Elt)element;
- Contract.Assert(e.domainValue == Value.Constant);
- return factory.Const(e.constantValue);
- }
-
- public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
- //Contract.Requires(args != null);
- //Contract.Requires(f != null);
- return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- }
-
- public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
- //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;
- }
-
- /// <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;
- }
- }
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System.Diagnostics.Contracts; +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 + } + + private class Elt : Element { + public Value domainValue; + public BigNum constantValue; // valid iff domainValue == Value.Constant + + public Elt(Value v) { + this.domainValue = v; + } + + public Elt(BigNum i) { + this.domainValue = Value.Constant; + this.constantValue = i; + } + + public bool IsConstant { + get { + return this.domainValue == Value.Constant; + } + } + + 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(); + } + + 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); + } + + + 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/*!*/ 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 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/*!*/ 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); + } + + protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that + { + //Contract.Requires(first!= null); + //Contract.Requires(second != null); + Elt a = (Elt)first; + Elt b = (Elt)second; + return a.Constant.Equals(b.Constant); + } + + public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) { + //Contract.Requires(element != null); + //Contract.Requires(var != null); + Contract.Ensures(Contract.Result<IExpr>() != null); + return factory.Eq(var, cce.NonNull(GetFoldExpr(element))); + } + + public override IExpr GetFoldExpr(Element/*!*/ element) { + //Contract.Requires(element != null); + Elt e = (Elt)element; + Contract.Assert(e.domainValue == Value.Constant); + return factory.Const(e.constantValue); + } + + public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) { + //Contract.Requires(args != null); + //Contract.Requires(f != null); + return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq); + } + + public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) { + //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; + } + + /// <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; + } + } +} |