path: root/Source/AIFramework/VariableMap/VariableMapLattice.ssc

//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework
{
    using Microsoft.Contracts;
    using System.Collections;
    using System.Collections.Generic;
    using System.Diagnostics;

    using Microsoft.AbstractInterpretationFramework;
    using Microsoft.AbstractInterpretationFramework.Collections;
    
    using Microsoft.Boogie;
    using IMutableSet = Microsoft.Boogie.Set;
    using HashSet = Microsoft.Boogie.Set;
    using ISet = Microsoft.Boogie.Set;

    /// <summary>
    ///  Creates a lattice that works for several variables given a MicroLattice.  Assumes
    ///  if one variable is bottom, then all variables are bottom.
    /// </summary>
    public class VariableMapLattice : Lattice
    {
        private class Elt : Element
        {
            /// <summary>
            /// IsBottom(e)  iff  e.constraints == null
            /// </summary>
            /*MayBeNull*/
            private IFunctionalMap constraints;  // of type IVariable -> LATTICE_ELEMENT
            public IFunctionalMap Constraints
            {
              get
              {
                return this.constraints;
              }
            }

            private Elt(bool top) {
                if (top) {
                    this.constraints = FunctionalHashtable.Empty;
                } else {
                    this.constraints = null;
                }
            }

            public override Element! Clone()
            {
                return new Elt(this.constraints);
            }
            
            [Pure]
            public override string! ToString()
            {
              if (constraints == null) {
                return "<bottom>";
              }
              string s = "[";
              string sep = "";
              foreach (IVariable! v in (!)constraints.Keys) {
                Element m = (Element)constraints[v];
                s += sep + v.Name + " -> " + m;
                sep = ", ";
              }
              return s + "]";
            }

            public static Elt! Top = new Elt(true);
            public static Elt! Bottom = new Elt(false);

            public Elt(IFunctionalMap constraints)
            {
                this.constraints = constraints;
            }

            public bool IsBottom { 
                 get { 
                   return this.constraints == null;
                 } 
            }

            public int Count { get { return this.constraints == null ? 0 : this.constraints.Count; } }

            public IEnumerable/*<IVariable>*/! Variables { 
              get 
                  requires !this.IsBottom;
                { 
                  assume this.constraints != null;
                  return (!) this.constraints.Keys;
                } 
            }

            public IEnumerable/*<IVariable>*/! SortedVariables(/*maybe null*/ IComparer variableComparer) {
                if (variableComparer == null) {
                    return Variables;
                } else {
                    ArrayList /*IVariable*/ vars = new ArrayList /*IVariable*/ (Count);
                    foreach (IVariable variable in Variables) {
                        vars.Add(variable);
                    }
                    vars.Sort(variableComparer);
                    return vars;
                }
            }
            
            public Element Lookup(IVariable v)
            {
                if ((v == null) || (this.constraints == null)) { return null; }
                return (Element)this.constraints[v];
            }

            public Element this [IVariable! key] { 
              get
                requires !this.IsBottom;
                { 
                  assume this.constraints != null;
                  return (Element)constraints[key];
                } 
            }

            /// <summary>
            /// Add a new entry in the functional map: var --> value.
            /// If the variable is already there, throws an exception
            /// </summary>
            public Elt! Add(IVariable! var, Element! value, MicroLattice! microLattice)
                requires !this.IsBottom;
            {
                assume this.constraints != null;
                assert !this.constraints.Contains(var);

                if (microLattice.IsBottom(value)) { return Bottom; }
                if (microLattice.IsTop(value)) { return this.Remove(var, microLattice); }
                
                return new Elt(this.constraints.Add(var, value));
            }

            /// <summary>
            /// Set the value of the variable in the functional map
            /// If the variable is not already there, throws an exception
            /// </summary>
            public Elt! Set(IVariable! var, Element! value, MicroLattice! microLattice)
            {                
                if(microLattice.IsBottom(value)) { return Bottom; }
                if(microLattice.IsTop(value)) { return this.Remove(var, microLattice); }
             
                assume this.constraints != null;
                assert this.constraints.Contains(var);

                // this.constraints[var] = value;
                IFunctionalMap newMap = this.constraints.Set(var, value);

                return new Elt(newMap);
            }

            public Elt! Remove(IVariable! var, MicroLattice microLattice)
            {
                if (this.IsBottom) { return this; }
                assume this.constraints != null;
                return new Elt(this.constraints.Remove(var));
            }

            public Elt! Rename(IVariable! oldName, IVariable! newName, MicroLattice! microLattice)
              requires !this.IsBottom;
            {
                Element value = this[oldName];
                if (value == null) { return this; } // 'oldName' isn't in the map, so neither will be 'newName'
                assume this.constraints != null;
                IFunctionalMap newMap = this.constraints.Remove(oldName);
                newMap = newMap.Add(newName, value);
                return new Elt(newMap);
            }

            [Pure]
            public override ICollection<IVariable!>! FreeVariables()
            {
                throw new System.NotImplementedException();
            }

        } // class

        private readonly MicroLattice! microLattice;

        private readonly IPropExprFactory! propExprFactory;
        
        private readonly /*maybe null*/IComparer variableComparer;

        public VariableMapLattice(IPropExprFactory! propExprFactory, IValueExprFactory! valueExprFactory, MicroLattice! microLattice, /*maybe null*/IComparer variableComparer)
            : base(valueExprFactory)
        {
            this.propExprFactory = propExprFactory;
            this.microLattice = microLattice;
            this.variableComparer = variableComparer;
            // base(valueExprFactory);
        }

        protected override object! UniqueId { get { return this.microLattice.GetType(); } }

        public override Element! Top { get { return Elt.Top; } }

        public override Element! Bottom { get { return Elt.Bottom; } }

        public override bool IsTop(Element! element)
        {
            Elt e = (Elt)element;
            return !e.IsBottom && e.Count == 0;
        }

        public override bool IsBottom(Element! element)
        {
            return ((Elt)element).IsBottom;
        }

        protected override bool AtMost(Element! first, Element! second)
        {
            Elt a = (Elt)first;
            Elt b = (Elt)second;

            // return true iff every constraint in "this" is no weaker than the corresponding
            // constraint in "that" and there are no additional constraints in "that"
            foreach (IVariable! var in a.Variables)
            {
                Element thisValue = (!)a[var];
                
                Element thatValue = b[var];
                if (thatValue == null) { continue; } // it's okay for "a" to know something "b" doesn't

                if (this.microLattice.LowerThan(thisValue, thatValue)) { continue; } // constraint for "var" satisfies AtMost relation
                
                return false;
            }
            foreach (IVariable! var in b.Variables)
            {
                if (a.Lookup(var) != null) { continue; } // we checked this case in the loop above
                
                Element thatValue = (!)b[var];
                if (this.microLattice.IsTop(thatValue)) { continue; } // this is a trivial constraint
                
                return false;
            }
            return true;
        }

        private Elt! AddConstraint(Element! element, IVariable! var, /*MicroLattice*/Element! newValue)
        {      
            Elt e = (Elt)element;

            if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
            {
                /*MicroLattice*/Element currentValue = e[var];

                if (currentValue == null)
                {
                    // No information currently, so we just add the new info.
                    return e.Add(var, newValue, this.microLattice);
                }
                else
                {
                    // Otherwise, take the meet of the new and current info.
                    //return e.Add(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
                    return e.Set(var, this.microLattice.Meet(currentValue, newValue), this.microLattice);
                }
            }
            return e;
        }

        public override string! ToString(Element! element)
        {
            Elt e = (Elt)element;

            if (IsTop(e)) { return "<top>"; }
            if (IsBottom(e)) { return "<bottom>"; }

            int k = 0;
            System.Text.StringBuilder buffer = new System.Text.StringBuilder();
            foreach (IVariable! key in e.SortedVariables(variableComparer))
            {
                if (k++ > 0) { buffer.Append("; "); }
                buffer.AppendFormat("{0} = {1}", key, e[key]);
            }
            return buffer.ToString();
        }

        public override Element! NontrivialJoin(Element! first, Element! second)
        {
            Elt a = (Elt)first;
            Elt b = (Elt)second;

            IFunctionalMap newMap = FunctionalHashtable.Empty;
            foreach (IVariable! key in a.Variables)
            {
                Element aValue = a[key];
                Element bValue = b[key];

                if (aValue != null && bValue != null)
                {
                    // Keep only the variables known to both elements.
                    Element newValue = this.microLattice.Join(aValue, bValue);
                    newMap = newMap.Add(key, newValue);
                }
            }
            Elt! join = new Elt(newMap);
        
            // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));

            return join;
        }

        public override Element! NontrivialMeet(Element! first, Element! second)
        {
            Elt a = (Elt)first;
            Elt b = (Elt)second;

            IFunctionalMap newMap = FunctionalHashtable.Empty;
            foreach (IVariable! key in a.Variables)
            {
                Element! aValue = (!) a[key];
                Element bValue = b[key];

                Element newValue =
                  bValue == null ? aValue :
                  this.microLattice.Meet(aValue, bValue);

                newMap = newMap.Add(key, newValue);
            }
            foreach (IVariable! key in b.Variables)
            {
                Element aValue = a[key];
                Element bValue = b[key]; Debug.Assert(bValue != null);

                if (aValue == null)
                {
                    // It's a variable we didn't cover in the last loop.
                    newMap = newMap.Add(key, bValue);
                }
            }
            return new Elt(newMap);
        }

        /// <summary>
        /// Perform the pointwise widening of the elements in the map
        /// </summary>
        public override Element! Widen (Element! first, Element! second)
        {          
            Elt a = (Elt)first;
            Elt b = (Elt)second;

            // Note we have to add those cases as we do not have a "NonTrivialWiden" method
            if(a.IsBottom)
              return new Elt(b.Constraints);
            if(b.IsBottom)
              return new Elt(a.Constraints);

            IFunctionalMap newMap = FunctionalHashtable.Empty;
            foreach (IVariable! key in a.Variables)
            {
                Element aValue = a[key];
                Element bValue = b[key];

                if (aValue != null && bValue != null)
                {
                    // Keep only the variables known to both elements.
                    Element newValue = this.microLattice.Widen(aValue, bValue);
                    newMap = newMap.Add(key, newValue);
                }
            }
            Element! widen= new Elt(newMap);
      
            // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));

            return widen;
        }

        internal static ISet/*<IVariable!>*/! VariablesInExpression(IExpr! e, ISet/*<IVariable!>*/! ignoreVars)
        {
            HashSet s = new HashSet();

            IFunApp f = e as IFunApp;
            IFunction lambda = e as IFunction;

            if (e is IVariable)
            {
                if (!ignoreVars.Contains(e))
                    s.Add(e);
            }
            else if (f != null) // e is IFunApp
            {
                foreach (IExpr! arg in f.Arguments)
                {
                    s.AddAll(VariablesInExpression(arg, ignoreVars));
                }
            }
            else if (lambda != null)
            {
                IMutableSet x = new HashSet(1);
                x.Add(lambda.Param);

                // Ignore the bound variable
                s.AddAll(VariablesInExpression(lambda.Body, (!) Set.Union(ignoreVars, x)));
            }
            else if (e is IUnknown)
            {
                // skip (actually, it would be appropriate to return the universal set of all variables)
            }
            else
            {
                Debug.Assert(false, "case not handled: " + e);
            }
            return s;
        }


        private static ArrayList/*<IExpr>*/! FindConjuncts(IExpr e)
        {
            ArrayList result = new ArrayList();

            IFunApp f = e as IFunApp;
            if (f != null)
            {
                if (f.FunctionSymbol.Equals(Prop.And))
                {
                    foreach (IExpr arg in f.Arguments)
                    {
                        result.AddRange(FindConjuncts(arg));
                    }
                }
                else if (f.FunctionSymbol.Equals(Prop.Or)
                         || f.FunctionSymbol.Equals(Prop.Implies))
                {
                    // Do nothing.
                }
                else
                {
                    result.Add(e);
                }
            }
            else
            {
                result.Add(e);
            }

            return result;
        }

        private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right)
            ensures result ==> left != null && right != null;
        {
            left = null;
            right = null;

            // See if we have an equality
            IFunApp nary = expr as IFunApp;
            if (nary == null || !nary.FunctionSymbol.Equals(Value.Eq)) { return false; }

            // See if it is an equality of two variables
            IVariable idLeft = nary.Arguments[0] as IVariable;
            IVariable idRight = nary.Arguments[1] as IVariable;
            if (idLeft == null || idRight == null) { return false; }

            left = idLeft;
            right = idRight;
            return true;
        }

      /// <summary>
      /// Returns true iff the expression is in the form var == arithmeticExpr
      /// </summary>
      private static bool IsArithmeticExpr(IExpr! expr) 
      {
        // System.Console.WriteLine("\t\tIsArithmetic called with {0} of type {1}", expr, expr.GetType().ToString());
        
        if(expr is IVariable)   // expr is a variable
          return true;
        else if(expr is IFunApp)     // may be ==, +, -, /, % or an integer
        {
          IFunApp fun = (IFunApp) expr;

          if(fun.FunctionSymbol is IntSymbol)     // it is an integer
            return true;
          else if(fun.FunctionSymbol.Equals(Int.Negate))  // it is an unary minus
            return IsArithmeticExpr((IExpr!) fun.Arguments[0]);
          else if(fun.Arguments.Count != 2)       // A function of two or more operands is not arithmetic
            return false;
          else 
          {
            IExpr! left = (IExpr!) fun.Arguments[0];
            IExpr! right = (IExpr!) fun.Arguments[1];

            if(!(left is IVariable || right is IVariable))    // At least one of the two operands must be a variable
              return false;

            if(fun.FunctionSymbol.Equals(Value.Eq)
                || fun.FunctionSymbol.Equals(Int.Add)
                || fun.FunctionSymbol.Equals(Int.Sub)
                || fun.FunctionSymbol.Equals(Int.Mul)
                || fun.FunctionSymbol.Equals(Int.Div)
                || fun.FunctionSymbol.Equals(Int.Mod))
              return IsArithmeticExpr(left) && IsArithmeticExpr(right);
            else 
              return false;
          } 
        }
          else
        { 
          return false;
        }    
      }

        public override IExpr! ToPredicate(Element! element)
        {
            if (IsTop(element)) { return propExprFactory.True; }
            if (IsBottom(element)) { return propExprFactory.False; }

            Elt e = (Elt)element;
            IExpr truth = propExprFactory.True;
            IExpr result = truth;
            
            foreach (IVariable! variable in e.SortedVariables(variableComparer))
            {
                Element value = (Element)e[variable];

                if (value == null || this.microLattice.IsTop(value)) { continue; } // Skip variables about which we know nothing.
                if (this.microLattice.IsBottom(value)) { return propExprFactory.False; }

                IExpr conjunct = this.microLattice.ToPredicate(variable, value);

                result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
            }
            return result;
        }


        public override Element! Eliminate(Element! element, IVariable! variable)
        {
            return ((Elt!)element).Remove(variable, this.microLattice);
        }

        private delegate IExpr! OnUnableToInline(IVariable! var);
        private IExpr! IdentityVarToExpr(IVariable! var)
        {
            return var;
        }

        /// <summary>
        /// Return a new expression in which each variable has been 
        /// replaced by an expression representing what is known about
        /// that variable.
        /// </summary>
        private IExpr! InlineVariables(Elt! element, IExpr! expr, ISet/*<IVariable!>*/! notInlineable,
            OnUnableToInline! unableToInline)
        {
            IVariable var = expr as IVariable;
            if (var != null)
            {
                /*MicroLattice*/Element value = element[var];
                if (notInlineable.Contains(var) || value == null || this.microLattice.IsTop(value))
                {
                    return unableToInline(var); // We don't know anything about this variable.
                }
                else
                {
                    // GetFoldExpr returns null when it can yield an expression that
                    // can be substituted for the variable.
                    IExpr valueExpr = this.microLattice.GetFoldExpr(value);
                    return (valueExpr == null) ? var : valueExpr;
                }
            }

            // else

            IFunApp fun = expr as IFunApp;
            if (fun != null)
            {
                IList newargs = new ArrayList();
                foreach (IExpr! arg in fun.Arguments)
                {
                    newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
                }
                return fun.CloneWithArguments(newargs);
            }

            // else

            IFunction lambda = expr as IFunction;
            if (lambda != null)
            {
                IMutableSet x = new HashSet(1);
                x.Add(lambda.Param);

                // Don't inline the bound variable
                return lambda.CloneWithBody(
                           InlineVariables(element, lambda.Body,
                                           (!) Set.Union(notInlineable, x), unableToInline)
                       );
            }

            // else
            
            if (expr is IUnknown) {
              return expr;
            }

            else
            {
                throw
                  new System.NotImplementedException("cannot inline identifies in expression " + expr);
            }
        }


        public override Element! Constrain(Element! element, IExpr! expr)
        {
            Elt! result = (Elt)element;

            if(IsBottom(element))
            {
              return result; // == element 
            }

            expr = InlineVariables(result, expr, (!)Set.Empty, new OnUnableToInline(IdentityVarToExpr));

            foreach (IExpr! conjunct in FindConjuncts(expr))
            {
                IVariable left, right;
               
                if (IsSimpleEquality(conjunct, out left, out right))
                {
                    #region The conjunct is a simple equality


                    assert left != null && right != null;

                    Element leftValue = result[left], rightValue = result[right];
                    if (leftValue == null) { leftValue = this.microLattice.Top; }
                    if (rightValue == null) { rightValue = this.microLattice.Top; }
                    Element newValue = this.microLattice.Meet(leftValue, rightValue);
                    result = AddConstraint(result, left, newValue);
                    result = AddConstraint(result, right, newValue);

                    #endregion
                }
                else
                {                   
                    ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);

                    if (variablesInvolved.Count == 1)
                    {
                        #region We have just one variable 
                       
                        IVariable var = null;
                        foreach (IVariable! v in variablesInvolved) { var = v; } // why is there no better way to get the elements?
                        assert var != null;
                        Element! value = this.microLattice.EvaluatePredicate(conjunct);
                        result = AddConstraint(result, var, value);
  
                        #endregion
                    }
                   else if(IsArithmeticExpr(conjunct) && this.microLattice.UnderstandsBasicArithmetics)
                    {
                      #region We evalaute an arithmetic expression

                       IFunApp fun = (IFunApp) conjunct;
                       if(fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
                       {                     
                          // get the variable to be assigned
                          IExpr! leftArg = (IExpr!) fun.Arguments[0];
                          IExpr! rightArg = (IExpr!) fun.Arguments[1];
                          IExpr! var = (leftArg is IVariable) ? leftArg : rightArg;
                      
                          Element! value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
                          result = AddConstraint(result, (IVariable!) var, value);
                       }
                      #endregion
                    }
                }
            }
            return result;
        }


        public override Element! Rename(Element! element, IVariable! oldName, IVariable! newName)
        {
            if(IsBottom(element))
            {
              return element;
            }
            else
            {
              return ((Elt)element).Rename(oldName, newName, this.microLattice);
            }
        }


        public override bool Understands(IFunctionSymbol! f, IList! args)
        {
            return f.Equals(Prop.And) ||
                   f.Equals(Value.Eq) ||
                   microLattice.Understands(f, args);
        }

        private sealed class EquivalentExprException : CheckedException { }
        private sealed class EquivalentExprInlineCallback
        {
            private readonly IVariable! var;
            public EquivalentExprInlineCallback(IVariable! var)
            {
                this.var = var;
                // base();
            }

            public IExpr! ThrowOnUnableToInline(IVariable! othervar)
              throws EquivalentExprException;
            {
                if (othervar.Equals(var))
                    throw new EquivalentExprException();
                else
                    return othervar;
            }
        }

        public override IExpr/*?*/ EquivalentExpr(Element! e, IQueryable! q, IExpr! expr, IVariable! var, ISet/*<IVariable!>*/! prohibitedVars)
        {
            try
            {
                EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
                return InlineVariables((Elt)e, expr, (!)Set.Empty,
                                       new OnUnableToInline(closure.ThrowOnUnableToInline));
            }
            catch (EquivalentExprException)
            {
                return null;
            }
        }


        /// <summary>
        /// Check to see if the given predicate holds in the given lattice element.
        /// 
        /// TODO:  We leave this unimplemented for now and just return maybe.
        /// </summary>
        /// <param name="e">The lattice element.</param>
        /// <param name="pred">The predicate.</param>
        /// <returns>Yes, No, or Maybe</returns>
        public override Answer CheckPredicate(Element! e, IExpr! pred)
        {
            return Answer.Maybe;
        }

        /// <summary>
        ///  Answers a disequality about two variables.  The same information could be obtained
        ///  by asking CheckPredicate, but a different implementation may be simpler and more
        ///  efficient.
        /// 
        ///  TODO: We leave this unimplemented for now and just return maybe.
        /// </summary>
        /// <param name="e">The lattice element.</param>
        /// <param name="var1">The first variable.</param>
        /// <param name="var2">The second variable.</param>
        /// <returns>Yes, No, or Maybe.</returns>
        public override Answer CheckVariableDisequality(Element! e, IVariable! var1, IVariable! var2)
        {
            return Answer.Maybe;
        }

        public override void Validate()
        {
            base.Validate();
            microLattice.Validate();
        }

    }
}