diff options
Diffstat (limited to 'Source/AIFramework/VariableMap/ConstantAbstraction.cs')
| -rw-r--r-- | Source/AIFramework/VariableMap/ConstantAbstraction.cs | 210 |
1 files changed, 210 insertions, 0 deletions
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.cs b/Source/AIFramework/VariableMap/ConstantAbstraction.cs new file mode 100644 index 00000000..8ba3065f --- /dev/null +++ b/Source/AIFramework/VariableMap/ConstantAbstraction.cs @@ -0,0 +1,210 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using Microsoft.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()
+ {
+ return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ }
+
+ public override Element! Clone()
+ {
+ if (this.IsConstant)
+ return new Elt(constantValue);
+ else
+ return new Elt(domainValue);
+ }
+ }
+
+ readonly IIntExprFactory! factory;
+
+ public ConstantLattice(IIntExprFactory! factory)
+ {
+ this.factory = factory;
+ // base();
+ }
+
+ public override Element! Top
+ {
+ get { return new Elt(Value.Top); }
+ }
+
+ public override Element! Bottom
+ {
+ get { return new Elt(Value.Bottom); }
+ }
+
+ public override bool IsTop (Element! element)
+ {
+ Elt e = (Elt)element;
+ return e.domainValue == Value.Top; + }
+
+ public override bool IsBottom (Element! element)
+ {
+ Elt e = (Elt)element;
+ return e.domainValue == Value.Bottom; + }
+
+ public override Element! NontrivialJoin (Element! first, Element! second)
+ {
+ 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)
+ {
+ 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)
+ {
+ return Join(first,second);
+ }
+
+ protected override bool AtMost (Element! first, Element! second) // this <= that
+ {
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ return a.Constant.Equals(b.Constant);
+ }
+
+ public override IExpr! ToPredicate(IVariable! var, Element! element) {
+ return factory.Eq(var, (!)GetFoldExpr(element));
+ }
+
+ public override IExpr GetFoldExpr(Element! element) {
+ Elt e = (Elt)element;
+ assert e.domainValue == Value.Constant;
+ return factory.Const(e.constantValue);
+ }
+
+ public override bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args) {
+ return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ }
+
+ public override Element! EvaluatePredicate(IExpr! e) {
+
+ IFunApp nary = e as IFunApp;
+ if (nary != null) {
+ if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
+ IList/*<IExpr!>*/! args = nary.Arguments;
+ assert args.Count == 2;
+ IExpr! arg0 = (IExpr!)args[0];
+ IExpr! arg1 = (IExpr!)args[1];
+
+ // 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)
+ {
+ 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;
+ assert args.Count == 1;
+ IExpr! arg0 = (IExpr!)args[0];
+
+ if (Fold(arg0, out z)) {
+ z = z.Neg;
+ return true;
+ }
+
+ } else if (e.Arguments.Count == 2) {
+ IExpr! arg0 = (IExpr!)e.Arguments[0];
+ IExpr! arg1 = (IExpr!)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;
+ }
+ }
+}
|