Boogie: Renaming the AIFramework sources in preparation for committal of my port of the project

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;

+        }

+    }

+}