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;
+    }
+  }
+}