From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- .../AIFramework/VariableMap/VariableMapLattice.cs | 1708 ++++++++++---------- 1 file changed, 854 insertions(+), 854 deletions(-) (limited to 'Source/AIFramework/VariableMap/VariableMapLattice.cs') diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs index 172cef01..752d3f01 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.cs +++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs @@ -1,854 +1,854 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -namespace Microsoft.AbstractInterpretationFramework { - using System.Diagnostics.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.GSet; - using ISet = Microsoft.Boogie.GSet; - using Set = Microsoft.Boogie.GSet; - using HashSet = Microsoft.Boogie.GSet; - - /// - /// Creates a lattice that works for several variables given a MicroLattice. Assumes - /// if one variable is bottom, then all variables are bottom. - /// - public class VariableMapLattice : Lattice { - private class Elt : Element { - /// - /// IsBottom(e) iff e.constraints == null - /// - /*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() { - Contract.Ensures(Contract.Result() != null); - return new Elt(this.constraints); - } - - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - if (constraints == null) { - return ""; - } - string s = "["; - string sep = ""; - foreach (IVariable/*!*/ v in cce.NonNull(constraints.Keys)) { - Contract.Assert(v != null); - Element m = (Element)constraints[v]; - s += sep + v.Name + " -> " + m; - sep = ", "; - } - return s + "]"; - } - - public static readonly Elt/*!*/ Top = new Elt(true); - public static readonly 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/**//*!*/ Variables { - get { - Contract.Requires(!this.IsBottom); - Contract.Ensures(Contract.Result() != null); - Contract.Assume(this.constraints != null); - return cce.NonNull(this.constraints.Keys); - } - } - - public IEnumerable/**//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) { - Contract.Ensures(Contract.Result() != null); - 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 { - Contract.Requires(!this.IsBottom); - Contract.Requires(key != null); - Contract.Assume(this.constraints != null); - return (Element)constraints[key]; - } - } - - /// - /// Add a new entry in the functional map: var --> value. - /// If the variable is already there, throws an exception - /// - public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) { - Contract.Requires(microLattice != null); - Contract.Requires(value != null); - Contract.Requires(var != null); - Contract.Requires((!this.IsBottom)); - Contract.Ensures(Contract.Result() != null); - Contract.Assume(this.constraints != null); - Contract.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)); - } - - /// - /// Set the value of the variable in the functional map - /// If the variable is not already there, throws an exception - /// - public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) { - Contract.Requires(microLattice != null); - Contract.Requires(value != null); - Contract.Requires(var != null); - Contract.Ensures(Contract.Result() != null); - if (microLattice.IsBottom(value)) { - return Bottom; - } - if (microLattice.IsTop(value)) { - return this.Remove(var, microLattice); - } - - Contract.Assume(this.constraints != null); - Contract.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) { - Contract.Requires(var != null); - Contract.Ensures(Contract.Result() != null); - if (this.IsBottom) { - return this; - } - Contract.Assume(this.constraints != null); - return new Elt(this.constraints.Remove(var)); - } - - public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice) { - Contract.Requires(microLattice != null); - Contract.Requires(newName != null); - Contract.Requires(oldName != null); - Contract.Requires((!this.IsBottom)); - Contract.Ensures(Contract.Result() != null); - Element value = this[oldName]; - if (value == null) { - return this; - } // 'oldName' isn't in the map, so neither will be 'newName' - Contract.Assume(this.constraints != null); - IFunctionalMap newMap = this.constraints.Remove(oldName); - newMap = newMap.Add(newName, value); - return new Elt(newMap); - } - - [Pure] - public override ICollection/*!*/ FreeVariables() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - throw new System.NotImplementedException(); - } - - } // class - - private readonly MicroLattice/*!*/ microLattice; - - private readonly IPropExprFactory/*!*/ propExprFactory; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(microLattice != null); - Contract.Invariant(propExprFactory != null); - } - - - private readonly /*maybe null*/IComparer variableComparer; - - public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer) - : base(valueExprFactory) { - Contract.Requires(microLattice != null); - Contract.Requires(valueExprFactory != null); - Contract.Requires(propExprFactory != null); - this.propExprFactory = propExprFactory; - this.microLattice = microLattice; - this.variableComparer = variableComparer; - // base(valueExprFactory); - } - - protected override object/*!*/ UniqueId { - get { - Contract.Ensures(Contract.Result() != null); - return this.microLattice.GetType(); - } - } - - public override Element/*!*/ Top { - get { - Contract.Ensures(Contract.Result() != null); - return Elt.Top; - } - } - - public override Element Bottom { - get { - Contract.Ensures(Contract.Result() != null); - return Elt.Bottom; - } - } - - public override bool IsTop(Element/*!*/ element) { - //Contract.Requires(element != null); - Elt e = (Elt)element; - return !e.IsBottom && e.Count == 0; - } - - public override bool IsBottom(Element/*!*/ element) { - //Contract.Requires(element != null); - return ((Elt)element).IsBottom; - } - - protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) { - //Contract.Requires(second != null); - //Contract.Requires(first != null); - 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) { - Contract.Assert(var != null); - Element thisValue = cce.NonNull(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) { - Contract.Assert(var != null); - if (a.Lookup(var) != null) { - continue; - } // we checked this case in the loop above - - Element thatValue = cce.NonNull(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) { - Contract.Requires((newValue != null)); - Contract.Requires((var != null)); - Contract.Requires((element != null)); - Contract.Ensures(Contract.Result() != null); - 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) { - //Contract.Requires(element != null); - Contract.Ensures(Contract.Result() != null); - Elt e = (Elt)element; - - if (IsTop(e)) { - return ""; - } - if (IsBottom(e)) { - return ""; - } - - int k = 0; - System.Text.StringBuilder buffer = new System.Text.StringBuilder(); - foreach (IVariable/*!*/ key in e.SortedVariables(variableComparer)) { - Contract.Assert(key != null); - if (k++ > 0) { - buffer.Append("; "); - } - buffer.AppendFormat("{0} = {1}", key, e[key]); - } - return buffer.ToString(); - } - - public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) { - //Contract.Requires(second != null); - //Contract.Requires(first != null); - Contract.Ensures(Contract.Result() != null); - Elt a = (Elt)first; - Elt b = (Elt)second; - - IFunctionalMap newMap = FunctionalHashtable.Empty; - foreach (IVariable/*!*/ key in a.Variables) { - Contract.Assert(key != null); - 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); - Contract.Assert(join != null); - - // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join)); - - return join; - } - - public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) { - //Contract.Requires(second != null); - //Contract.Requires(first != null); - Contract.Ensures(Contract.Result() != null); - Elt a = (Elt)first; - Elt b = (Elt)second; - - IFunctionalMap newMap = FunctionalHashtable.Empty; - foreach (IVariable/*!*/ key in a.Variables) { - Contract.Assert(key != null); - Element/*!*/ aValue = cce.NonNull(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) { - Contract.Assert(key != null); - 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); - } - - /// - /// Perform the pointwise widening of the elements in the map - /// - public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) { - //Contract.Requires((second != null)); - //Contract.Requires((first != null)); - Contract.Ensures(Contract.Result() != null); - 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) { - Contract.Assert(key != null); - 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); - Contract.Assert(widen != null); - // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen)); - - return widen; - } - - internal static ISet/**//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/**//*!*/ ignoreVars) { - Contract.Requires(ignoreVars != null); - Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - 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) { - Contract.Assert(arg != null); - 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, cce.NonNull(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/**//*!*/ FindConjuncts(IExpr e) { - Contract.Ensures(Contract.Result() != null); - 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) { - Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out 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; - } - - /// - /// Returns true iff the expression is in the form var == arithmeticExpr - /// - private static bool IsArithmeticExpr(IExpr/*!*/ expr) { - Contract.Requires(expr != null); - // 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/*!*/)cce.NonNull(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/*!*/)cce.NonNull(fun.Arguments[0]); - IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(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) { - //Contract.Requires(element != null); - Contract.Ensures(Contract.Result() != null); - 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)) { - Contract.Assert(variable != null); - 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) { - //Contract.Requires(variable != null); - //Contract.Requires(element != null); - Contract.Ensures(Contract.Result() != null); - return cce.NonNull((Elt)element).Remove(variable, this.microLattice); - } - - private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var); - private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var) { - //Contract.Requires(var != null); - Contract.Ensures(Contract.Result() != null); - return var; - } - - /// - /// Return a new expression in which each variable has been - /// replaced by an expression representing what is known about - /// that variable. - /// - private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/**//*!*/ notInlineable, - OnUnableToInline/*!*/ unableToInline) { - Contract.Requires(unableToInline != null); - Contract.Requires(notInlineable != null); - Contract.Requires(expr != null); - Contract.Requires(element != null); - Contract.Ensures(Contract.Result() != null); - 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) { - Contract.Assert(arg != null); - 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, - cce.NonNull(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) { - //Contract.Requires(expr != null); - //Contract.Requires(element != null); - //Contract.Ensures(Contract.Result() != null); - Elt/*!*/ result = (Elt)element; - Contract.Assert(result != null); - - if (IsBottom(element)) { - return result; // == element - } - - expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr)); - - foreach (IExpr/*!*/ conjunct in FindConjuncts(expr)) { - Contract.Assert(conjunct != null); - IVariable left, right; - - if (IsSimpleEquality(conjunct, out left, out right)) { - #region The conjunct is a simple equality - - - Contract.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/**/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty); - - if (variablesInvolved.Count == 1) { - #region We have just one variable - - IVariable var = null; - foreach (IVariable/*!*/ v in variablesInvolved) { - Contract.Assert(v != null); - var = v; - } // why is there no better way to get the elements? - Contract.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/*!*/)cce.NonNull(fun.Arguments[0]); - IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]); - IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg; - - Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints); - Contract.Assert(value != null); - result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value); - } - #endregion - } - } - } - return result; - } - - - public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) { - //Contract.Requires(newName != null); - //Contract.Requires(oldName != null); - //Contract.Requires(element != null); - //Contract.Ensures(Contract.Result() != null); - if (IsBottom(element)) { - return element; - } else { - return ((Elt)element).Rename(oldName, newName, this.microLattice); - } - } - - - public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) { - //Contract.Requires(args != null); - //Contract.Requires(f != null); - 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; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(var != null); - } - - public EquivalentExprInlineCallback(IVariable/*!*/ var) { - Contract.Requires(var != null); - this.var = var; - // base(); - } - - public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar) - //throws EquivalentExprException; - { - Contract.Requires(othervar != null); - Contract.Ensures(Contract.Result() != null); - Contract.EnsuresOnThrow(true); - if (othervar.Equals(var)) - throw new EquivalentExprException(); - else - return othervar; - } - } - - public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/**//*!*/ prohibitedVars) { - //Contract.Requires(prohibitedVars != null); - //Contract.Requires(var != null); - //Contract.Requires(expr != null); - //Contract.Requires(q != null); - //Contract.Requires(e != null); - try { - EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var); - return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty), - new OnUnableToInline(closure.ThrowOnUnableToInline)); - } catch (EquivalentExprException) { - return null; - } - } - - - /// - /// Check to see if the given predicate holds in the given lattice element. - /// - /// TODO: We leave this unimplemented for now and just return maybe. - /// - /// The lattice element. - /// The predicate. - /// Yes, No, or Maybe - public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) { - //Contract.Requires(pred != null); - //Contract.Requires(e != null); - return Answer.Maybe; - } - - /// - /// 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. - /// - /// The lattice element. - /// The first variable. - /// The second variable. - /// Yes, No, or Maybe. - public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) { - //Contract.Requires(var2 != null); - //Contract.Requires(var1 != null); - //Contract.Requires(e != null); - return Answer.Maybe; - } - - public override void Validate() { - base.Validate(); - microLattice.Validate(); - } - - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework { + using System.Diagnostics.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.GSet; + using ISet = Microsoft.Boogie.GSet; + using Set = Microsoft.Boogie.GSet; + using HashSet = Microsoft.Boogie.GSet; + + /// + /// Creates a lattice that works for several variables given a MicroLattice. Assumes + /// if one variable is bottom, then all variables are bottom. + /// + public class VariableMapLattice : Lattice { + private class Elt : Element { + /// + /// IsBottom(e) iff e.constraints == null + /// + /*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() { + Contract.Ensures(Contract.Result() != null); + return new Elt(this.constraints); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + if (constraints == null) { + return ""; + } + string s = "["; + string sep = ""; + foreach (IVariable/*!*/ v in cce.NonNull(constraints.Keys)) { + Contract.Assert(v != null); + Element m = (Element)constraints[v]; + s += sep + v.Name + " -> " + m; + sep = ", "; + } + return s + "]"; + } + + public static readonly Elt/*!*/ Top = new Elt(true); + public static readonly 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/**//*!*/ Variables { + get { + Contract.Requires(!this.IsBottom); + Contract.Ensures(Contract.Result() != null); + Contract.Assume(this.constraints != null); + return cce.NonNull(this.constraints.Keys); + } + } + + public IEnumerable/**//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) { + Contract.Ensures(Contract.Result() != null); + 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 { + Contract.Requires(!this.IsBottom); + Contract.Requires(key != null); + Contract.Assume(this.constraints != null); + return (Element)constraints[key]; + } + } + + /// + /// Add a new entry in the functional map: var --> value. + /// If the variable is already there, throws an exception + /// + public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) { + Contract.Requires(microLattice != null); + Contract.Requires(value != null); + Contract.Requires(var != null); + Contract.Requires((!this.IsBottom)); + Contract.Ensures(Contract.Result() != null); + Contract.Assume(this.constraints != null); + Contract.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)); + } + + /// + /// Set the value of the variable in the functional map + /// If the variable is not already there, throws an exception + /// + public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) { + Contract.Requires(microLattice != null); + Contract.Requires(value != null); + Contract.Requires(var != null); + Contract.Ensures(Contract.Result() != null); + if (microLattice.IsBottom(value)) { + return Bottom; + } + if (microLattice.IsTop(value)) { + return this.Remove(var, microLattice); + } + + Contract.Assume(this.constraints != null); + Contract.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) { + Contract.Requires(var != null); + Contract.Ensures(Contract.Result() != null); + if (this.IsBottom) { + return this; + } + Contract.Assume(this.constraints != null); + return new Elt(this.constraints.Remove(var)); + } + + public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice) { + Contract.Requires(microLattice != null); + Contract.Requires(newName != null); + Contract.Requires(oldName != null); + Contract.Requires((!this.IsBottom)); + Contract.Ensures(Contract.Result() != null); + Element value = this[oldName]; + if (value == null) { + return this; + } // 'oldName' isn't in the map, so neither will be 'newName' + Contract.Assume(this.constraints != null); + IFunctionalMap newMap = this.constraints.Remove(oldName); + newMap = newMap.Add(newName, value); + return new Elt(newMap); + } + + [Pure] + public override ICollection/*!*/ FreeVariables() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + throw new System.NotImplementedException(); + } + + } // class + + private readonly MicroLattice/*!*/ microLattice; + + private readonly IPropExprFactory/*!*/ propExprFactory; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(microLattice != null); + Contract.Invariant(propExprFactory != null); + } + + + private readonly /*maybe null*/IComparer variableComparer; + + public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer) + : base(valueExprFactory) { + Contract.Requires(microLattice != null); + Contract.Requires(valueExprFactory != null); + Contract.Requires(propExprFactory != null); + this.propExprFactory = propExprFactory; + this.microLattice = microLattice; + this.variableComparer = variableComparer; + // base(valueExprFactory); + } + + protected override object/*!*/ UniqueId { + get { + Contract.Ensures(Contract.Result() != null); + return this.microLattice.GetType(); + } + } + + public override Element/*!*/ Top { + get { + Contract.Ensures(Contract.Result() != null); + return Elt.Top; + } + } + + public override Element Bottom { + get { + Contract.Ensures(Contract.Result() != null); + return Elt.Bottom; + } + } + + public override bool IsTop(Element/*!*/ element) { + //Contract.Requires(element != null); + Elt e = (Elt)element; + return !e.IsBottom && e.Count == 0; + } + + public override bool IsBottom(Element/*!*/ element) { + //Contract.Requires(element != null); + return ((Elt)element).IsBottom; + } + + protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) { + //Contract.Requires(second != null); + //Contract.Requires(first != null); + 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) { + Contract.Assert(var != null); + Element thisValue = cce.NonNull(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) { + Contract.Assert(var != null); + if (a.Lookup(var) != null) { + continue; + } // we checked this case in the loop above + + Element thatValue = cce.NonNull(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) { + Contract.Requires((newValue != null)); + Contract.Requires((var != null)); + Contract.Requires((element != null)); + Contract.Ensures(Contract.Result() != null); + 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) { + //Contract.Requires(element != null); + Contract.Ensures(Contract.Result() != null); + Elt e = (Elt)element; + + if (IsTop(e)) { + return ""; + } + if (IsBottom(e)) { + return ""; + } + + int k = 0; + System.Text.StringBuilder buffer = new System.Text.StringBuilder(); + foreach (IVariable/*!*/ key in e.SortedVariables(variableComparer)) { + Contract.Assert(key != null); + if (k++ > 0) { + buffer.Append("; "); + } + buffer.AppendFormat("{0} = {1}", key, e[key]); + } + return buffer.ToString(); + } + + public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) { + //Contract.Requires(second != null); + //Contract.Requires(first != null); + Contract.Ensures(Contract.Result() != null); + Elt a = (Elt)first; + Elt b = (Elt)second; + + IFunctionalMap newMap = FunctionalHashtable.Empty; + foreach (IVariable/*!*/ key in a.Variables) { + Contract.Assert(key != null); + 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); + Contract.Assert(join != null); + + // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join)); + + return join; + } + + public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) { + //Contract.Requires(second != null); + //Contract.Requires(first != null); + Contract.Ensures(Contract.Result() != null); + Elt a = (Elt)first; + Elt b = (Elt)second; + + IFunctionalMap newMap = FunctionalHashtable.Empty; + foreach (IVariable/*!*/ key in a.Variables) { + Contract.Assert(key != null); + Element/*!*/ aValue = cce.NonNull(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) { + Contract.Assert(key != null); + 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); + } + + /// + /// Perform the pointwise widening of the elements in the map + /// + public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) { + //Contract.Requires((second != null)); + //Contract.Requires((first != null)); + Contract.Ensures(Contract.Result() != null); + 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) { + Contract.Assert(key != null); + 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); + Contract.Assert(widen != null); + // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen)); + + return widen; + } + + internal static ISet/**//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/**//*!*/ ignoreVars) { + Contract.Requires(ignoreVars != null); + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + 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) { + Contract.Assert(arg != null); + 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, cce.NonNull(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/**//*!*/ FindConjuncts(IExpr e) { + Contract.Ensures(Contract.Result() != null); + 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) { + Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out 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; + } + + /// + /// Returns true iff the expression is in the form var == arithmeticExpr + /// + private static bool IsArithmeticExpr(IExpr/*!*/ expr) { + Contract.Requires(expr != null); + // 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/*!*/)cce.NonNull(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/*!*/)cce.NonNull(fun.Arguments[0]); + IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(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) { + //Contract.Requires(element != null); + Contract.Ensures(Contract.Result() != null); + 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)) { + Contract.Assert(variable != null); + 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) { + //Contract.Requires(variable != null); + //Contract.Requires(element != null); + Contract.Ensures(Contract.Result() != null); + return cce.NonNull((Elt)element).Remove(variable, this.microLattice); + } + + private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var); + private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var) { + //Contract.Requires(var != null); + Contract.Ensures(Contract.Result() != null); + return var; + } + + /// + /// Return a new expression in which each variable has been + /// replaced by an expression representing what is known about + /// that variable. + /// + private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/**//*!*/ notInlineable, + OnUnableToInline/*!*/ unableToInline) { + Contract.Requires(unableToInline != null); + Contract.Requires(notInlineable != null); + Contract.Requires(expr != null); + Contract.Requires(element != null); + Contract.Ensures(Contract.Result() != null); + 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) { + Contract.Assert(arg != null); + 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, + cce.NonNull(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) { + //Contract.Requires(expr != null); + //Contract.Requires(element != null); + //Contract.Ensures(Contract.Result() != null); + Elt/*!*/ result = (Elt)element; + Contract.Assert(result != null); + + if (IsBottom(element)) { + return result; // == element + } + + expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr)); + + foreach (IExpr/*!*/ conjunct in FindConjuncts(expr)) { + Contract.Assert(conjunct != null); + IVariable left, right; + + if (IsSimpleEquality(conjunct, out left, out right)) { + #region The conjunct is a simple equality + + + Contract.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/**/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty); + + if (variablesInvolved.Count == 1) { + #region We have just one variable + + IVariable var = null; + foreach (IVariable/*!*/ v in variablesInvolved) { + Contract.Assert(v != null); + var = v; + } // why is there no better way to get the elements? + Contract.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/*!*/)cce.NonNull(fun.Arguments[0]); + IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]); + IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg; + + Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints); + Contract.Assert(value != null); + result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value); + } + #endregion + } + } + } + return result; + } + + + public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) { + //Contract.Requires(newName != null); + //Contract.Requires(oldName != null); + //Contract.Requires(element != null); + //Contract.Ensures(Contract.Result() != null); + if (IsBottom(element)) { + return element; + } else { + return ((Elt)element).Rename(oldName, newName, this.microLattice); + } + } + + + public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) { + //Contract.Requires(args != null); + //Contract.Requires(f != null); + 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; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(var != null); + } + + public EquivalentExprInlineCallback(IVariable/*!*/ var) { + Contract.Requires(var != null); + this.var = var; + // base(); + } + + public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar) + //throws EquivalentExprException; + { + Contract.Requires(othervar != null); + Contract.Ensures(Contract.Result() != null); + Contract.EnsuresOnThrow(true); + if (othervar.Equals(var)) + throw new EquivalentExprException(); + else + return othervar; + } + } + + public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/**//*!*/ prohibitedVars) { + //Contract.Requires(prohibitedVars != null); + //Contract.Requires(var != null); + //Contract.Requires(expr != null); + //Contract.Requires(q != null); + //Contract.Requires(e != null); + try { + EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var); + return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty), + new OnUnableToInline(closure.ThrowOnUnableToInline)); + } catch (EquivalentExprException) { + return null; + } + } + + + /// + /// Check to see if the given predicate holds in the given lattice element. + /// + /// TODO: We leave this unimplemented for now and just return maybe. + /// + /// The lattice element. + /// The predicate. + /// Yes, No, or Maybe + public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) { + //Contract.Requires(pred != null); + //Contract.Requires(e != null); + return Answer.Maybe; + } + + /// + /// 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. + /// + /// The lattice element. + /// The first variable. + /// The second variable. + /// Yes, No, or Maybe. + public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) { + //Contract.Requires(var2 != null); + //Contract.Requires(var1 != null); + //Contract.Requires(e != null); + return Answer.Maybe; + } + + public override void Validate() { + base.Validate(); + microLattice.Validate(); + } + + } +} -- cgit v1.2.3