diff options
Diffstat (limited to 'Source/AIFramework/VariableMap/VariableMapLattice.ssc')
| -rw-r--r-- | Source/AIFramework/VariableMap/VariableMapLattice.ssc | 749 |
1 files changed, 749 insertions, 0 deletions
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc new file mode 100644 index 00000000..aa15f1e6 --- /dev/null +++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc @@ -0,0 +1,749 @@ +//-----------------------------------------------------------------------------
+//
+// 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);
+ }
+
+ public static Elt! Top = new Elt(true);
+ public static Elt! Bottom = new Elt(false);
+
+ public Elt(IFunctionalMap constraints)
+ {
+ this.constraints = constraints;
+ }
+
+ public bool IsBottom {
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ 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][Reads(ReadsAttribute.Reads.Owned)]
+ 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
+ {
+ 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
+ {
+ 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();
+ }
+
+ }
+}
|