diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Source/AIFramework/VariableMap | |
Initial set of files.
Diffstat (limited to 'Source/AIFramework/VariableMap')
| -rw-r--r-- | Source/AIFramework/VariableMap/ConstantAbstraction.ssc | 210 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/ConstantExpressions.ssc | 538 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/DynamicTypeLattice.ssc | 475 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/Intervals.ssc | 790 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/MicroLattice.ssc | 79 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/Nullness.ssc | 227 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/VariableMapLattice.ssc | 749 |
7 files changed, 3068 insertions, 0 deletions
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc new file mode 100644 index 00000000..7b7fd87e --- /dev/null +++ b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc @@ -0,0 +1,210 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using Microsoft.Contracts;
+namespace Microsoft.AbstractInterpretationFramework
+{
+ using System.Collections;
+ using System.Diagnostics;
+ using System.Compiler.Analysis;
+ using Microsoft.Basetypes;
+
+ /// <summary>
+ /// Represents an invariant over constant variable assignments.
+ /// </summary>
+ public class ConstantLattice : MicroLattice
+ {
+ enum Value { Top, Bottom, Constant }
+
+ private class Elt : Element
+ {
+ public Value domainValue;
+ public BigNum constantValue; // valid iff domainValue == Value.Constant
+
+ public Elt (Value v) { this.domainValue = v; }
+
+ public Elt (BigNum i) { this.domainValue = Value.Constant; this.constantValue = i; }
+
+ public bool IsConstant { get { return this.domainValue == Value.Constant; } }
+
+ public BigNum Constant { get { return this.constantValue; } } // only when IsConstant
+
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
+ {
+ return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ }
+
+ public override Element! Clone()
+ {
+ if (this.IsConstant)
+ return new Elt(constantValue);
+ else
+ return new Elt(domainValue);
+ }
+ }
+
+ readonly IIntExprFactory! factory;
+
+ public ConstantLattice(IIntExprFactory! factory)
+ {
+ this.factory = factory;
+ // base();
+ }
+
+ public override Element! Top
+ {
+ get { return new Elt(Value.Top); }
+ }
+
+ public override Element! Bottom
+ {
+ get { return new Elt(Value.Bottom); }
+ }
+
+ public override bool IsTop (Element! element)
+ {
+ Elt e = (Elt)element;
+ return e.domainValue == Value.Top;
+ }
+
+ public override bool IsBottom (Element! element)
+ {
+ Elt e = (Elt)element;
+ return e.domainValue == Value.Bottom;
+ }
+
+ public override Element! NontrivialJoin (Element! first, Element! second)
+ {
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
+ return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Top;
+ }
+
+ public override Element! NontrivialMeet (Element! first, Element! second)
+ {
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
+ return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Bottom;
+ }
+
+ public override Element! Widen (Element! first, Element! second)
+ {
+ return Join(first,second);
+ }
+
+ protected override bool AtMost (Element! first, Element! second) // this <= that
+ {
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ return a.Constant.Equals(b.Constant);
+ }
+
+ public override IExpr! ToPredicate(IVariable! var, Element! element) {
+ return factory.Eq(var, (!)GetFoldExpr(element));
+ }
+
+ public override IExpr GetFoldExpr(Element! element) {
+ Elt e = (Elt)element;
+ assert e.domainValue == Value.Constant;
+ return factory.Const(e.constantValue);
+ }
+
+ public override bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args) {
+ return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ }
+
+ public override Element! EvaluatePredicate(IExpr! e) {
+
+ IFunApp nary = e as IFunApp;
+ if (nary != null) {
+ if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
+ IList/*<IExpr!>*/! args = nary.Arguments;
+ assert args.Count == 2;
+ IExpr! arg0 = (IExpr!)args[0];
+ IExpr! arg1 = (IExpr!)args[1];
+
+ // Look for "x == const" or "const == x".
+ try {
+ if (arg0 is IVariable) {
+ BigNum z;
+ if (Fold(arg1, out z)) {
+ return new Elt(z);
+ }
+ } else if (arg1 is IVariable) {
+ BigNum z;
+ if (Fold(arg0, out z)) {
+ return new Elt(z);
+ }
+ }
+ } catch (System.ArithmeticException) {
+ // fall through and return Top. (Note, an alternative design may
+ // consider returning Bottom.)
+ }
+ }
+ }
+ return Top;
+ }
+
+ /// <summary>
+ /// Returns true if "expr" represents a constant integer expressions, in which case
+ /// "z" returns as that integer. Otherwise, returns false, in which case "z" should
+ /// not be used by the caller.
+ ///
+ /// This method throws an System.ArithmeticException in the event that folding the
+ /// constant expression results in an arithmetic overflow or division by zero.
+ /// </summary>
+ private bool Fold(IExpr! expr, out BigNum z)
+ {
+ IFunApp e = expr as IFunApp;
+ if (e == null) {
+ z = BigNum.ZERO;
+ return false;
+ }
+
+ if (e.FunctionSymbol is IntSymbol) {
+ z = ((IntSymbol)e.FunctionSymbol).Value;
+ return true;
+
+ } else if (e.FunctionSymbol.Equals(Int.Negate)) {
+ IList/*<IExpr!>*/! args = e.Arguments;
+ assert args.Count == 1;
+ IExpr! arg0 = (IExpr!)args[0];
+
+ if (Fold(arg0, out z)) {
+ z = z.Neg;
+ return true;
+ }
+
+ } else if (e.Arguments.Count == 2) {
+ IExpr! arg0 = (IExpr!)e.Arguments[0];
+ IExpr! arg1 = (IExpr!)e.Arguments[1];
+ BigNum z0, z1;
+ if (Fold(arg0, out z0) && Fold(arg1, out z1)) {
+ if (e.FunctionSymbol.Equals(Int.Add)) {
+ z = z0 + z1;
+ } else if (e.FunctionSymbol.Equals(Int.Sub)) {
+ z = z0 - z1;
+ } else if (e.FunctionSymbol.Equals(Int.Mul)) {
+ z = z0 * z1;
+ } else if (e.FunctionSymbol.Equals(Int.Div)) {
+ z = z0 / z1;
+ } else if (e.FunctionSymbol.Equals(Int.Mod)) {
+ z = z0 % z1;
+ } else {
+ z = BigNum.ZERO;
+ return false;
+ }
+ return true;
+ }
+ }
+
+ z = BigNum.ZERO;
+ return false;
+ }
+ }
+}
diff --git a/Source/AIFramework/VariableMap/ConstantExpressions.ssc b/Source/AIFramework/VariableMap/ConstantExpressions.ssc new file mode 100644 index 00000000..306c4e8f --- /dev/null +++ b/Source/AIFramework/VariableMap/ConstantExpressions.ssc @@ -0,0 +1,538 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+ /////////////////////////////////////////////////////////////////////////////////
+ // The Abstract domain for determining "constant" expressions
+ // i.e. It determines which expression are statically binded
+ /////////////////////////////////////////////////////////////////////////////////
+/*
+using System;
+
+namespace Microsoft.AbstractInterpretationFramework
+{
+ using Microsoft.Contracts;
+ using System.Collections.Generic;
+ using Microsoft.AbstractInterpretationFramework;
+
+ /// <summary>
+ /// This is an abstract domain for inferring constant expressions
+ /// </summary>
+
+ public class ConstantExpressions : Lattice
+ {
+ /// <summary>
+ /// An abstract element is made of two maps:
+ /// + A map from variables to expressions \cup top ( i.e. for each variable, the expression it is binded )
+ /// + A map from variables to set of variabes ( i.e. for each variable, the set of variables that depends on its value )
+ /// </summary>
+ private class AbstractElement: Element
+ {
+ private Dictionary<IVariable!, BindExpr> variableBindings;
+ private Dictionary<IVariable!, List<IVariable>> variableDependences;
+
+ static private AbstractElement! bottom;
+ static public Element! Bottom
+ {
+ get
+ {
+ if(bottom == null)
+ {
+ bottom = new AbstractElement();
+ bottom.variableBindings = null;
+ bottom.variableDependences = null;
+ }
+ assert bottom.variableBindings == null && bottom.variableDependences == null;
+ return bottom;
+ }
+ }
+
+ static public Element! Top
+ {
+ get
+ {
+ return new AbstractElement();
+ }
+ }
+
+ AbstractElement()
+ {
+ this.variableBindings = new Dictionary<IVariable!, BindExpr>();
+ this.variableDependences = new Dictionary<IVariable!, List<IVariable>>();
+ }
+
+ /// <summary>
+ /// Our abstract element is top if and only if it has any constraint on variables
+ /// </summary>
+ public bool IsTop
+ {
+ get
+ {
+ return this.variableBindings.Keys.Count == 0 && this.variableDependences.Keys.Count == 0;
+ }
+ }
+
+ /// <summary>
+ /// Our abstract element is bottom if and only if the maps are null
+ /// </summary>
+ public bool IsBottom
+ {
+ get
+ {
+ assert (this.variableBindings == null) <==> (this.variableDependences == null);
+ return this.variableBindings == null && this.variableDependences == null;
+ }
+ }
+
+ /// <summary>
+ /// The pointwise join...
+ /// </summary>
+ public static AbstractElement! Join(AbstractElement! left, AbstractElement! right)
+ {
+ AbstractElement! result = new AbstractElement();
+
+ // Put all the variables in the left
+ foreach(IVariable! var in left.variableBindings.Keys)
+ {
+ BindExpr leftVal = left.variableBindings[var];
+ assert leftVal != null;
+
+ BindExpr rightVal = right.variableBindings[var];
+
+ if(rightVal== null) // the expression is not there
+ {
+ result.variableBindings.Add(var, leftVal);
+ }
+ else // both abstract elements have a definition for the variable....
+ {
+ result.variableBindings.Add(var, BindExpr.Join(leftVal, rightVal));
+ }
+ }
+
+ // Put all the variables in the right
+ foreach(IVariable! var in right.variableBindings.Keys)
+ {
+ BindExpr rightVal = right.variableBindings[var];
+ assert rightVal != null;
+
+ BindExpr leftVal = left.variableBindings[var];
+
+ if(rightVal== null) // the expression is not there
+ {
+ result.variableBindings.Add(var, rightVal);
+ }
+ else // both abstract elements have a definition for the variable....
+ {
+ result.variableBindings.Add(var, BindExpr.Join(rightVal, leftVal));
+ }
+ }
+
+ // Join the dependencies...
+ foreach(IVariable! var in left.variableDependences.Keys)
+ {
+ List<IVariable> dependencies = left.variableDependences[var];
+ List<IVariable> dup = new List<IVariable>(dependencies);
+
+ result.variableDependences.Add(var, dup);
+ }
+
+ foreach(IVariable! var in right.variableDependences.Keys)
+ {
+ if(result.variableDependences.ContainsKey(var))
+ {
+ List<IVariable> dependencies = result.variableDependences[var];
+ dependencies.AddRange(right.variableDependences[var]);
+ }
+ else
+ {
+ List<IVariable> dependencies = right.variableDependences[var];
+ List<IVariable> dup = new List<IVariable>(dependencies);
+
+ result.variableDependences.Add(var, dup);
+ }
+ }
+
+ // Normalize... i.e. for the variables such thas they point to an unknown expression (top) we have to update also their values
+ result.Normalize();
+
+ return result;
+ }
+
+
+ ///<summary>
+ /// Normalize the current abstract element, in that it propagetes the "dynamic" information throughtout the abstract element
+ ///</summary>
+ public void Normalize()
+ {
+ if(this.IsBottom)
+ return;
+ if(this.IsTop)
+ return;
+ assert this.variableBindings != null;
+
+ bool atFixpoint = false;
+
+ while(!atFixpoint)
+ {
+ atFixpoint = true; // guess that we've got the fixpoint...
+
+ foreach(IVariable x in this.variableBindings.Keys)
+ {
+ if(this.variableBindings[x].IsTop) // It means that the variable is tied to a dynamic expression
+ {
+ foreach(IVariable y in this.variableDependences[x]) // The all the variables that depend on x are also dynamic...
+ {
+ assert x != y; // A variable cannot depend on itself...
+ if(!this.variableBindings[y].IsTop)
+ {
+ this.variableBindings[y] = BindExpr.Top;
+ atFixpoint = false; // the assumption that we were at the fixpoint was false, we have still to propagate some information...
+ }
+ }
+ }
+ }
+ }
+ }
+
+ /// <summary>
+ /// The pointwise meet...
+ /// </summary>
+ public static AbstractElement! Meet(AbstractElement! left, AbstractElement! right)
+ {
+ AbstractElement! result = new AbstractElement();
+
+ // Put the variables that are both in left and right
+ foreach(IVariable var in left.variableBindings.Keys)
+ {
+ if(right.variableBindings.ContainsKey(var))
+ {
+ result.variableBindings.Add(var, BindExpr.Meet(left.variableBindings[var], right.variableBindings[var]));
+ }
+ }
+
+ // Intersect the dependencies
+ foreach(IVariable var in result.variableBindings.Keys)
+ {
+ List<IVariable> depLeft = left.variableDependences[var];
+ List<IVariable> depRight = right.variableDependences[var];
+
+ // Intersect the two sets
+ result.variableDependences.Add(var, depLeft);
+ foreach(IVariable v in depRight)
+ {
+ if(!result.variableDependences.ContainsKey(v))
+ {
+ result.variableDependences.Remove(v);
+ }
+ }
+ }
+
+ // Now we remove the dependencies with variables not in variableBindings
+ List<IVariable>! varsToRemove = new List<IVariable>();
+
+ foreach(IVariable var in result.
+
+
+ }
+
+ /// <summary>
+ /// Clone the current abstract element
+ /// </summary>
+ public override Element! Clone()
+ {
+ AbstractElement cloned = new AbstractElement();
+ foreach(IVariable var in this.variableBindings.Keys)
+ {
+ cloned.variableBindings.Add(var, this.variableBindings[var]);
+ }
+
+ foreach(IVariable var in this.variableDependences.Keys)
+ {
+ List<IVariable> dependingVars = this.variableDependences[var];
+ List<IVariable> clonedDependingVars = new List<IVariable>(dependingVars);
+ cloned.variableDependences.Add(var, clonedDependingVars);
+ }
+ }
+
+ /// <summary>
+ /// Return the variables that have a binding
+ /// </summary>
+ public override ICollection<IVariable!>! FreeVariables()
+ {
+ List<IVariable!> vars = new List<IVariable!>(this.variableBindings.Keys);
+
+ return vars;
+ }
+
+ public override string! ToString()
+ {
+ string! retString = "";
+ retString += "Bindings";
+
+ foreach(IVariable var in this.variableBindings.Keys)
+ {
+ string! toAdd = var.ToString() + " -> " + this.variableBindings[var];
+ retString += toAdd + ",";
+ }
+
+ retString += "\nDependencies";
+ foreach(IVariable var in this.variableDependences.Keys)
+ {
+ string! toAdd = var.ToString() + " -> " + this.variableDependences[var];
+ retString += toAdd + ",";
+ }
+
+ return retString;
+ }
+ }
+
+ public override Element! Top
+ {
+ get
+ {
+ return AbstractElement.Top;
+ }
+ }
+
+ public override Element! Bottom
+ {
+ get
+ {
+ return AbstractElement.Bottom;
+ }
+ }
+
+ public override bool IsTop(Element! e)
+ {
+ assert e is AbstractElement;
+ AbstractElement! absElement = (AbstractElement) e;
+
+ return absElement.IsTop;
+ }
+
+ public override bool IsBottom(Element! e)
+ {
+ assert e is AbstractElement;
+ AbstractElement absElement = (AbstractElement) e;
+ return absElement.IsBottom;
+ }
+
+ /// <summary>
+ /// Perform the pointwise join of the two abstract elements
+ /// </summary>
+ public override Element! NontrivialJoin(Element! a, Element! b)
+ {
+ assert a is AbstractElement;
+ assert b is AbstractElement;
+
+ AbstractElement! left = (AbstractElement!) a;
+ AbstractElement! right = (AbstractElement!) b;
+
+ return AbstractElement.Join(left, right);
+ }
+
+ /// <summary>
+ /// Perform the pointwise meet of two abstract elements
+ /// </summary>
+ public override Element! NontrivialMeet(Element! a, Element!b)
+ {
+ assert a is AbstractElement;
+ assert b is AbstractElement;
+
+ AbstractElement! left = (AbstractElement!) a;
+ AbstractElement! right = (AbstractElement!) b;
+
+ return AbstractElement.Meet(left, right);
+ }
+
+
+ }
+
+ /// <summary>
+ /// A wrapper in order to have the algebraic datatype BindExpr := IExpr | Top
+ /// </summary>
+ abstract class BindExpr
+ {
+ /// <summary>
+ /// True iff this expression is instance of BindExprTop
+ /// </summary>
+ public bool IsTop
+ {
+ get
+ {
+ return this is BindExprTop;
+ }
+ }
+
+ static public BindExpr Top
+ {
+ get
+ {
+ return BindExprTop.UniqueTop;
+ }
+ }
+
+ /// <summary>
+ /// True iff this expression is instance of BindExprBottom
+ /// </summary>
+ public bool IsBottom
+ {
+ get
+ {
+ return this is BindExprBottom;
+ }
+ }
+
+ static public BindExpr Bottom
+ {
+ get
+ {
+ return BindExprBottom.UniqueBottom;
+ }
+ }
+
+ public static BindExpr! Join(BindExpr! left, BindExpr! right)
+ {
+ if(left.IsTop || right.IsTop)
+ {
+ return BindExpr.Top;
+ }
+ else if(left.IsBottom)
+ {
+ return right;
+ }
+ else if(right.IsBottom)
+ {
+ return left;
+ }
+ else if(left.EmbeddedExpr != right.EmbeddedExpr)
+ {
+ return BindExpr.Top;
+ }
+ else // left.EmbeddedExpr == right.EmbeddedExpr
+ {
+ return left;
+ }
+ }
+
+ public static BindExpr! Meet(BindExpr! left, BindExpr! right)
+ {
+ if(left.IsTop)
+ {
+ return right;
+ }
+ else if(right.IsTop)
+ {
+ return right;
+ }
+ else if(left.IsBottom || right.IsBottom)
+ {
+ return BindExpr.Bottom;
+ }
+ else if(left.EmbeddedExpr != right.EmbeddedExpr)
+ {
+ return BindExpr.Bottom;
+ }
+ else // left.EmbeddedExpr == right.EmbeddedExpr
+ {
+ return left;
+ }
+ }
+
+ abstract public IExpr! EmbeddedExpr
+ {
+ get;
+ }
+
+ }
+
+ /// <summary>
+ /// A wrapper for an integer
+ /// </summary>
+ class Expr : BindExpr
+ {
+ private IExpr! exp;
+
+ public Expr(IExpr! exp)
+ {
+ this.exp = exp;
+ }
+
+ override public IExpr! EmbeddedExpr
+ {
+ get
+ {
+ return this.exp;
+ }
+ }
+
+ public override string! ToString()
+ {
+ return this.exp.ToString();
+ }
+ }
+
+ /// <summary>
+ /// The dynamic expression
+ /// </summary>
+ class BindExprTop : BindExpr
+ {
+ private BindExprTop top = new BindExprTop();
+ static public BindExprTop! UniqueTop
+ {
+ get
+ {
+ return this.top;
+ }
+ }
+
+ private BindExprTop() {}
+
+ override public IExpr! EmbeddedExpr
+ {
+ get
+ {
+ assert false; // If we get there, we have an error
+ }
+ }
+
+ public override string! ToString()
+ {
+ return "<dynamic expression>";
+ }
+ }
+
+ /// <summary>
+ /// The unreachable expression
+ /// </summary>
+ class BindExprBottom : BindExpr
+ {
+ private BindExprBottom! bottom = new BindExprBottom();
+ static public BindExprBottom! UniqueBottom
+ {
+ get
+ {
+ return this.bottom;
+ }
+ }
+
+ private BindExprBottom() {}
+
+ override public IExpr! EmbeddedExpr
+ {
+ get
+ {
+ assert false;
+ }
+ }
+
+ public override string! ToString()
+ {
+ return "<unreachable expression>";
+ }
+ }
+
+} // end namespace Microsoft.AbstractInterpretationFramework
+*/
\ No newline at end of file diff --git a/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc b/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc new file mode 100644 index 00000000..b9d1a7a4 --- /dev/null +++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc @@ -0,0 +1,475 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework
+{
+ using System.Collections;
+ using System.Diagnostics;
+ using System.Compiler.Analysis;
+ using Microsoft.SpecSharp.Collections;
+ using Microsoft.Contracts;
+
+ /// <summary>
+ /// Represents information about the dynamic type of a variable. In particular, for a
+ /// variable "v", represents either Bottom, "typeof(v)==T" for some type T, or a set
+ /// of constraints "typeof(v) subtype of T_i for some number of T_i's.
+ /// </summary>
+ public class DynamicTypeLattice : MicroLattice
+ {
+ enum What { Bottom, Exact, Bounds }
+
+ private class Elt : Element {
+ // Representation:
+ // - Bottom is represented by: what==What.Bottom
+ // - An exact type T is represented by: what==What.Exact && ty==T
+ // - A set of type constraints T0, T1, T2, ..., T{n-1} is represented by:
+ // -- if n==0: what==What.Bounds && ty==null && manyBounds==null
+ // -- if n==1: what==What.Bounds && ty==T0 && manyBounds==null
+ // -- if n>=2: what==What.Bounds && ty==null &&
+ // manyBounds!=null && manyBounds.Length==n &&
+ // manyBounds[0]==T0 && manyBounds[1]==T1 && ... && manyBounds[n-1]==T{n-1}
+ // The reason for keeping the one-and-only bound in "ty" in case n==1 is to try
+ // to prevent the need for allocating a whole array of bounds, since 1 bound is
+ // bound to be common.
+ // In the representation, there are no redundant bounds in manyBounds.
+ // It is assumed that the types can can occur as exact bounds form a single-inheritance
+ // hierarchy. That is, if T0 and T1 are types that can occur as exact types, then
+ // there is no v such that typeof(v) is a subtype of both T0 and T1, unless T0 and T1 are
+ // the same type.
+ public readonly What what;
+ public readonly IExpr ty;
+ [Rep]
+ public readonly IExpr[] manyBounds;
+ invariant what == What.Bottom ==> ty == null && manyBounds == null;
+ invariant manyBounds != null ==> what == What.Bounds;
+ invariant manyBounds != null ==> forall{int i in (0:manyBounds.Length); manyBounds[i] != null};
+
+ public Elt(What what, IExpr ty)
+ requires what == What.Bottom ==> ty == null;
+ requires what == What.Exact ==> ty != null;
+ {
+ this.what = what;
+ this.ty = ty;
+ this.manyBounds = null;
+ }
+
+ public Elt(IExpr[]! bounds)
+ requires forall{int i in (0:bounds.Length); bounds[i] != null};
+ {
+ this.what = What.Bounds;
+ if (bounds.Length == 0) {
+ this.ty = null;
+ this.manyBounds = null;
+ } else if (bounds.Length == 1) {
+ this.ty = bounds[0];
+ this.manyBounds = null;
+ } else {
+ this.ty = null;
+ this.manyBounds = bounds;
+ }
+ }
+
+ /// <summary>
+ /// Constructs an Elt with "n" bounds, namely the n non-null values of the "bounds" list.
+ /// </summary>
+ [NotDelayed]
+ public Elt(ArrayList /*IExpr*/! bounds, int n)
+ requires 0 <= n && n <= bounds.Count;
+ {
+ this.what = What.Bounds;
+ if (n > 1) {
+ this.manyBounds = new IExpr[n];
+ }
+ int k = 0;
+ foreach (IExpr bound in bounds) {
+ if (bound != null) {
+ assert k != n;
+ if (n == 1) {
+ assert this.ty == null;
+ this.ty = bound;
+ } else {
+ assume manyBounds != null;
+ manyBounds[k] = bound;
+ }
+ k++;
+ }
+ }
+ assert k == n;
+ }
+
+ public int BoundsCount
+ {
+ get
+ ensures 0 <= result;
+ {
+ if (manyBounds != null) {
+ return manyBounds.Length;
+ } else if (ty != null) {
+ return 1;
+ } else {
+ return 0;
+ }
+ }
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
+ {
+ return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ }
+
+ public override Element! Clone()
+ {
+ if (this.manyBounds != null)
+ return new Elt(this.manyBounds);
+ else
+ return new Elt(this.what, this.ty);
+ }
+ }
+
+ readonly ITypeExprFactory! factory;
+ readonly IPropExprFactory! propFactory;
+
+ public DynamicTypeLattice(ITypeExprFactory! factory, IPropExprFactory! propFactory)
+ {
+ this.factory = factory;
+ this.propFactory = propFactory;
+ // base();
+ }
+
+ public override Element! Top
+ {
+ get { return new Elt(What.Bounds, null); }
+ }
+
+ public override Element! Bottom
+ {
+ get { return new Elt(What.Bottom, null); }
+ }
+
+ public override bool IsTop (Element! element)
+ {
+ Elt e = (Elt)element;
+ return e.what == What.Bounds && e.ty == null && e.manyBounds == null;
+ }
+
+ public override bool IsBottom(Element! element)
+ {
+ Elt e = (Elt)element;
+ return e.what == What.Bottom;
+ }
+
+ public override Element! NontrivialJoin(Element! first, Element! second)
+ {
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ assert a.what != What.Bottom && b.what != What.Bottom;
+ if (a.what == What.Exact && b.what == What.Exact) {
+ assert a.ty != null && b.ty != null;
+ if (factory.IsTypeEqual(a.ty, b.ty)) {
+ return a;
+ } else {
+ return new Elt(What.Bounds, factory.JoinTypes(a.ty, b.ty));
+ }
+ }
+
+ // The result is going to be a Bounds, since at least one of the operands is a Bounds.
+ assert 1 <= a.BoundsCount && 1 <= b.BoundsCount; // a preconditions is that neither operand is Top
+ int n = a.BoundsCount + b.BoundsCount;
+
+ // Special case: a and b each has exactly one bound
+ if (n == 2) {
+ assert a.ty != null && b.ty != null;
+ IExpr! join = factory.JoinTypes(a.ty, b.ty);
+ if (join == a.ty && a.what == What.Bounds) {
+ return a;
+ } else if (join == b.ty && b.what == What.Bounds) {
+ return b;
+ } else {
+ return new Elt(What.Bounds, join);
+ }
+ }
+
+ // General case
+ ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n); // final size
+ ArrayList /*IExpr!*/ result = new ArrayList /*IExpr!*/ (n); // a guess at the size, but could be as big as size(a)*size(b)
+ if (a.ty != null) {
+ allBounds.Add(a.ty);
+ } else {
+ allBounds.AddRange((!)a.manyBounds);
+ }
+ int bStart = allBounds.Count;
+ if (b.ty != null) {
+ allBounds.Add(b.ty);
+ } else {
+ allBounds.AddRange((!)b.manyBounds);
+ }
+ // compute the join of each pair, putting non-redundant joins into "result"
+ for (int i = 0; i < bStart; i++) {
+ IExpr! aBound = (IExpr!)allBounds[i];
+ for (int j = bStart; j < allBounds.Count; j++) {
+ IExpr! bBound = (IExpr!)allBounds[j];
+
+ IExpr! join = factory.JoinTypes(aBound, bBound);
+
+ int k = 0;
+ while (k < result.Count) {
+ IExpr! r = (IExpr!)result[k];
+ if (factory.IsSubType(join, r)) {
+ // "join" is more restrictive than a bound already placed in "result",
+ // so toss out "join" and compute the join of the next pair
+ goto NEXT_PAIR;
+ } else if (factory.IsSubType(r, join)) {
+ // "join" is less restrictive than a bound already placed in "result",
+ // so toss out that old bound
+ result.RemoveAt(k);
+ } else {
+ k++;
+ }
+ }
+ result.Add(join);
+ NEXT_PAIR: {}
+ }
+ }
+ return new Elt(result, result.Count);
+ }
+
+
+ public override Element! NontrivialMeet(Element! first, Element! second)
+ {
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ assert a.what != What.Bottom && b.what != What.Bottom;
+
+ if (a.what == What.Exact && b.what == What.Exact) {
+ assert a.ty != null && b.ty != null;
+ if (factory.IsTypeEqual(a.ty, b.ty)) {
+ return a;
+ } else {
+ return Bottom;
+ }
+
+ } else if (a.what == What.Exact || b.what == What.Exact) {
+ // One is Bounds, the other Exact. Make b be the Bounds one.
+ if (a.what == What.Bounds) {
+ Elt tmp = a;
+ a = b;
+ b = tmp;
+ }
+ assert a.what == What.Exact && b.what == What.Bounds;
+ // Check the exact type against all bounds. If the exact type is more restrictive
+ // than all bounds, then return it. If some bound is not met by the exact type, return
+ // bottom.
+ assert a.ty != null;
+ if (b.ty != null && !factory.IsSubType(a.ty, b.ty)) {
+ return Bottom;
+ }
+ if (b.manyBounds != null) {
+ foreach (IExpr! bound in b.manyBounds) {
+ if (!factory.IsSubType(a.ty, bound)) {
+ return Bottom;
+ }
+ }
+ }
+ return a;
+ }
+
+ else {
+ // Both operands are Bounds.
+ assert a.what == What.Bounds && b.what == What.Bounds;
+
+ // Take all the bounds, but prune those bounds that follow from others.
+ assert 1 <= a.BoundsCount && 1 <= b.BoundsCount; // a preconditions is that neither operand is Top
+ int n = a.BoundsCount + b.BoundsCount;
+ // Special case: a and b each has exactly one bound
+ if (n == 2) {
+ assert a.ty != null && b.ty != null;
+ if (factory.IsSubType(a.ty, b.ty)) {
+ // a is more restrictive
+ return a;
+ } else if (factory.IsSubType(b.ty, a.ty)) {
+ // b is more restrictive
+ return b;
+ } else {
+ IExpr[]! bounds = new IExpr[2];
+ bounds[0] = a.ty;
+ bounds[1] = b.ty;
+ return new Elt(bounds);
+ }
+ }
+
+ // General case
+ ArrayList /*IExpr*/ allBounds = new ArrayList /*IExpr*/ (n);
+ if (a.ty != null) {
+ allBounds.Add(a.ty);
+ } else {
+ allBounds.AddRange((!)a.manyBounds);
+ }
+ int bStart = allBounds.Count;
+ if (b.ty != null) {
+ allBounds.Add(b.ty);
+ } else {
+ allBounds.AddRange((!)b.manyBounds);
+ }
+ for (int i = 0; i < bStart; i++) {
+ IExpr! aBound = (IExpr!)allBounds[i];
+ for (int j = bStart; j < allBounds.Count; j++) {
+ IExpr bBound = (IExpr!)allBounds[j];
+ if (bBound == null) {
+ continue;
+ } else if (factory.IsSubType(aBound, bBound)) {
+ // a is more restrictive, so blot out the b bound
+ allBounds[j] = null;
+ n--;
+ } else if (factory.IsSubType(bBound, aBound)) {
+ // b is more restrictive, so blot out the a bound
+ allBounds[i] = null;
+ n--;
+ goto CONTINUE_OUTER_LOOP;
+ }
+ }
+ CONTINUE_OUTER_LOOP: {}
+ }
+ assert 1 <= n;
+ return new Elt(allBounds, n);
+ }
+ }
+
+ public override Element! Widen (Element! first, Element! second)
+ {
+ return Join(first,second);
+ }
+
+ protected override bool AtMost (Element! first, Element! second) // this <= that
+ {
+ Elt! a = (Elt!)first;
+ Elt! b = (Elt!)second;
+ assert a.what != What.Bottom && b.what != What.Bottom;
+
+ if (a.what == What.Exact && b.what == What.Exact) {
+ assert a.ty != null && b.ty != null;
+ return factory.IsTypeEqual(a.ty, b.ty);
+ } else if (b.what == What.Exact) {
+ return false;
+ } else if (a.what == What.Exact) {
+ assert a.ty != null;
+ if (b.ty != null) {
+ return factory.IsSubType(a.ty, b.ty);
+ } else {
+ return forall{IExpr! bound in b.manyBounds; factory.IsSubType(a.ty, bound)};
+ }
+ } else {
+ assert a.what == What.Bounds && b.what == What.Bounds;
+ assert a.ty != null || a.manyBounds != null; // a precondition is that a is not Top
+ assert b.ty != null || b.manyBounds != null; // a precondition is that b is not Top
+ // Return true iff: for each constraint in b, there is a stricter constraint in a.
+ if (a.ty != null && b.ty != null) {
+ return factory.IsSubType(a.ty, b.ty);
+ } else if (a.ty != null) {
+ return forall{IExpr! bound in b.manyBounds; factory.IsSubType(a.ty, bound)};
+ } else if (b.ty != null) {
+ return exists{IExpr! bound in a.manyBounds; factory.IsSubType(bound, b.ty)};
+ } else {
+ return forall{IExpr! bBound in b.manyBounds;
+ exists{IExpr! aBound in a.manyBounds; factory.IsSubType(aBound, bBound)}};
+ }
+ }
+ }
+
+ public override IExpr! ToPredicate(IVariable! var, Element! element) {
+ Elt e = (Elt)element;
+ switch (e.what) {
+ case What.Bottom:
+ return propFactory.False;
+ case What.Exact:
+ return factory.IsExactlyA(var, (!)e.ty);
+ case What.Bounds:
+ if (e.ty == null && e.manyBounds == null) {
+ return propFactory.True;
+ } else if (e.ty != null) {
+ return factory.IsA(var, e.ty);
+ } else {
+ IExpr! p = factory.IsA(var, (IExpr!)((!)e.manyBounds)[0]);
+ for (int i = 1; i < e.manyBounds.Length; i++) {
+ p = propFactory.And(p, factory.IsA(var, (IExpr!)e.manyBounds[i]));
+ }
+ return p;
+ }
+ default:
+ assert false;
+ throw new System.Exception();
+ }
+ }
+
+ public override IExpr GetFoldExpr(Element! e) {
+ // cannot fold into an expression that can be substituted for the variable
+ return null;
+ }
+
+ public override bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args) {
+ bool isEq = f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ if (isEq || f.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
+ assert args.Count == 2;
+ IExpr! arg0 = (IExpr!)args[0];
+ IExpr! arg1 = (IExpr!)args[1];
+
+ // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t
+ if (isEq && factory.IsTypeConstant(arg0)) {
+ // swap the arguments
+ IExpr! tmp = arg0;
+ arg0 = arg1;
+ arg1 = tmp;
+ } else if (!factory.IsTypeConstant(arg1)) {
+ return false;
+ }
+ IFunApp typeofExpr = arg0 as IFunApp;
+ if (typeofExpr != null &&
+ typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) {
+ assert typeofExpr.Arguments.Count == 1;
+ if (typeofExpr.Arguments[0] is IVariable) {
+ // we have a match
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
+ public override Element! EvaluatePredicate(IExpr! e) {
+ IFunApp nary = e as IFunApp;
+ if (nary != null) {
+
+ bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
+ IList/*<IExpr!>*/! args = nary.Arguments;
+ assert args.Count == 2;
+ IExpr! arg0 = (IExpr!)args[0];
+ IExpr! arg1 = (IExpr!)args[1];
+
+ // Look for $typeof(var) == t or t == $typeof(var) or $typeof(var) <: t
+ if (isEq && factory.IsTypeConstant(arg0)) {
+ // swap the arguments
+ IExpr! tmp = arg0;
+ arg0 = arg1;
+ arg1 = tmp;
+ } else if (!factory.IsTypeConstant(arg1)) {
+ return Top;
+ }
+ IFunApp typeofExpr = arg0 as IFunApp;
+ if (typeofExpr != null &&
+ typeofExpr.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Typeof)) {
+ assert typeofExpr.Arguments.Count == 1;
+ if (typeofExpr.Arguments[0] is IVariable) {
+ // we have a match
+ return new Elt(isEq ? What.Exact : What.Bounds, arg1);
+ }
+ }
+ }
+ }
+ return Top;
+ }
+
+ }
+}
diff --git a/Source/AIFramework/VariableMap/Intervals.ssc b/Source/AIFramework/VariableMap/Intervals.ssc new file mode 100644 index 00000000..721b175d --- /dev/null +++ b/Source/AIFramework/VariableMap/Intervals.ssc @@ -0,0 +1,790 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Compiler.Analysis;
+using Microsoft.AbstractInterpretationFramework.Collections;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+
+/////////////////////////////////////////////////////////////////////////////////
+// An implementation of the interval abstract domain
+/////////////////////////////////////////////////////////////////////////////////
+
+namespace Microsoft.AbstractInterpretationFramework
+{
+ public class IntervalLattice : MicroLattice
+ {
+ readonly ILinearExprFactory! factory;
+
+ public IntervalLattice(ILinearExprFactory! factory)
+ {
+ this.factory = factory;
+ // base();
+ }
+
+ public override bool UnderstandsBasicArithmetics
+ {
+ get
+ {
+ return true;
+ }
+ }
+
+ public override Element! Top
+ {
+ get
+ {
+ return IntervalElement.Top;
+ }
+ }
+
+ public override Element! Bottom
+ {
+ get
+ {
+ return IntervalElement.Bottom;
+ }
+ }
+
+ /// <summary>
+ /// The paramter is the top?
+ /// </summary>
+ public override bool IsTop(Element! element)
+ {
+ IntervalElement interval = (IntervalElement) element;
+
+ return interval.IsTop();
+ }
+
+ /// <summary>
+ /// The parameter is the bottom?
+ /// </summary>
+ public override bool IsBottom(Element! element)
+ {
+ IntervalElement interval = (IntervalElement) element;
+
+ return interval.IsBottom();
+ }
+
+ /// <summary>
+ /// The classic, pointwise, join of intervals
+ /// </summary>
+ public override Element! NontrivialJoin(Element! left, Element! right)
+ {
+ IntervalElement! leftInterval = (IntervalElement!) left;
+ IntervalElement! rightInterval = (IntervalElement) right;
+
+ ExtendedInt inf = ExtendedInt.Inf(leftInterval.Inf, rightInterval.Inf);
+ ExtendedInt sup = ExtendedInt.Sup(leftInterval.Sup, rightInterval.Sup);
+
+ IntervalElement! join = IntervalElement.Factory(inf, sup);
+
+ return join;
+ }
+
+ /// <summary>
+ /// The classic, pointwise, meet of intervals
+ /// </summary>
+ public override Element! NontrivialMeet(Element! left, Element! right)
+ {
+ IntervalElement! leftInterval = (IntervalElement!) left;
+ IntervalElement! rightInterval = (IntervalElement) right;
+
+ ExtendedInt inf = ExtendedInt.Sup(leftInterval.Inf, rightInterval.Inf);
+ ExtendedInt sup = ExtendedInt.Inf(leftInterval.Sup, rightInterval.Sup);
+
+ return IntervalElement.Factory(inf, sup);
+ }
+
+
+ /// <summary>
+ /// The very simple widening of intervals, to be improved with thresholds
+ /// left is the PREVIOUS value in the iterations and right is the NEW one
+ /// </summary>
+ public override Element! Widen(Element! left, Element! right)
+ {
+ IntervalElement! prevInterval = (IntervalElement!) left;
+ IntervalElement! nextInterval = (IntervalElement!) right;
+
+ ExtendedInt inf = nextInterval.Inf < prevInterval.Inf ? ExtendedInt.MinusInfinity : prevInterval.Inf;
+ ExtendedInt sup = nextInterval.Sup > prevInterval.Sup ? ExtendedInt.PlusInfinity : prevInterval.Sup;
+
+ IntervalElement widening = IntervalElement.Factory(inf, sup);
+
+ return widening;
+ }
+
+
+ /// <summary>
+ /// Return true iff the interval left is containted in right
+ /// </summary>
+ protected override bool AtMost(Element! left, Element! right)
+ {
+ IntervalElement! leftInterval = (IntervalElement!) left;
+ IntervalElement! rightInterval = (IntervalElement!) right;
+
+ if(leftInterval.IsBottom() || rightInterval.IsTop())
+ return true;
+
+ return rightInterval.Inf <= leftInterval.Inf && leftInterval.Sup <= rightInterval.Sup;
+ }
+
+ /// <summary>
+ /// Return just null
+ /// </summary>
+ public override IExpr GetFoldExpr(Element! element)
+ {
+ return null;
+ }
+
+ /// <summary>
+ /// return a predicate inf "\leq x and x "\leq" sup (if inf [or sup] is not oo)
+ /// </summary>
+ public override IExpr! ToPredicate(IVariable! var, Element! element)
+ {
+ IntervalElement! interval = (IntervalElement!) element;
+ IExpr lowerBound = null;
+ IExpr upperBound = null;
+
+ if(! (interval.Inf is InfinitaryInt))
+ {
+ IExpr constant = this.factory.Const(interval.Inf.Value);
+ lowerBound = this.factory.AtMost(constant, var); // inf <= var
+ }
+ if(! (interval.Sup is InfinitaryInt))
+ {
+ IExpr constant = this.factory.Const(interval.Sup.Value);
+ upperBound = this.factory.AtMost(var, constant); // var <= inf
+ }
+
+ if(lowerBound != null && upperBound != null)
+ return this.factory.And(lowerBound, upperBound); // inf <= var && var <= sup
+ else
+ if(lowerBound != null)
+ return lowerBound;
+ else
+ if(upperBound != null)
+ return upperBound;
+ else // If we reach this point, both lowerBound and upperBound are null, i.e. we have no bounds on var, so we return simply true...
+ return this.factory.True;
+ }
+
+ /// <summary>
+ /// For the moment consider just equalities. Other case must be considered
+ /// </summary>
+ public override bool Understands(IFunctionSymbol! f, IList /*<IExpr*/ ! args)
+ {
+ return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ }
+
+
+ /// <summary>
+ /// Evaluate the predicate passed as input according the semantics of intervals
+ /// </summary>
+ public override Element! EvaluatePredicate(IExpr! pred)
+ {
+ return this.EvaluatePredicateWithState(pred, null);
+ }
+
+ /// <summary>
+ /// Evaluate the predicate passed as input according the semantics of intervals and the given state.
+ /// Right now just basic arithmetic operations are supported. A future extension may consider an implementation of boolean predicates
+ /// </summary>
+ public override Element! EvaluatePredicateWithState(IExpr! pred, IFunctionalMap/* Var -> Element */ state)
+ {
+ if(pred is IFunApp)
+ {
+ IFunApp fun = (IFunApp) pred;
+ if(fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
+ {
+ IExpr! leftArg = (IExpr!) fun.Arguments[0];
+ IExpr! rightArg = (IExpr!) fun.Arguments[1];
+ if (leftArg is IVariable) {
+ return Eval(rightArg, state);
+ } else if (rightArg is IVariable) {
+ return Eval(leftArg, state);
+ }
+ }
+ }
+ // otherwise we simply return Top
+ return IntervalElement.Top;
+ }
+
+ /// <summary>
+ /// Evaluate the expression (that is assured to be an arithmetic expression, in the state passed as a parameter
+ /// </summary>
+ private IntervalElement! Eval(IExpr! exp, IFunctionalMap/* Var -> Element */ state)
+ {
+
+ IntervalElement! retVal = (IntervalElement!) Top;
+
+ // Eval the expression by structural induction
+
+
+ if(exp is IVariable && state != null) // A variable
+ {
+ object lookup = state[exp];
+ if(lookup is IntervalElement)
+ retVal = (IntervalElement) lookup;
+ else
+ {
+ retVal = (IntervalElement) Top;
+ }
+ }
+ else if(exp is IFunApp)
+ {
+ IFunApp fun = (IFunApp) exp;
+
+ if(fun.FunctionSymbol is IntSymbol) // An integer
+ {
+ IntSymbol intSymb = (IntSymbol) fun.FunctionSymbol;
+ BigNum val = intSymb.Value;
+
+ retVal = IntervalElement.Factory(val);
+ }
+ else if(fun.FunctionSymbol.Equals(Int.Negate)) // An unary minus
+ {
+ IExpr! arg = (IExpr!) fun.Arguments[0];
+ IntervalElement! argEval = Eval(arg, state);
+ IntervalElement! zero = IntervalElement.Factory(BigNum.ZERO);
+
+ retVal = zero - argEval;
+ }
+ else if(fun.Arguments.Count == 2)
+ {
+ IExpr! left = (IExpr!) fun.Arguments[0];
+ IExpr! right = (IExpr!) fun.Arguments[1];
+
+ IntervalElement! leftVal = Eval(left, state);
+ IntervalElement! rightVal = Eval(right, state);
+
+ if(fun.FunctionSymbol.Equals(Int.Add))
+ retVal = leftVal + rightVal;
+ else if(fun.FunctionSymbol.Equals(Int.Sub))
+ retVal = leftVal - rightVal;
+ else if(fun.FunctionSymbol.Equals(Int.Mul))
+ retVal = leftVal * rightVal;
+ else if(fun.FunctionSymbol.Equals(Int.Div))
+ retVal = leftVal / rightVal;
+ else if(fun.FunctionSymbol.Equals(Int.Mod))
+ retVal = leftVal % rightVal;
+ }
+ }
+
+ return retVal;
+ }
+
+ /// <summary>
+ /// Inner class standing for an interval on integers, possibly unbounded
+ /// </summary>
+ private class IntervalElement : Element
+ {
+ protected static readonly IntervalElement! TopInterval = new IntervalElement(new MinusInfinity(), new PlusInfinity()); // Top = [-oo , +oo]
+ protected static readonly IntervalElement! BottomInterval = new IntervalElement(new PlusInfinity(), new MinusInfinity()); // Bottom = [+oo, -oo]
+
+ private readonly ExtendedInt! inf;
+ private readonly ExtendedInt! sup;
+
+ public ExtendedInt! Inf
+ {
+ get
+ {
+ return inf;
+ }
+ }
+
+ public ExtendedInt! Sup
+ {
+ get
+ {
+ return sup;
+ }
+ }
+
+ // Construct the inteval [val, val]
+ protected IntervalElement(BigNum val)
+ {
+ this.inf = this.sup = ExtendedInt.Factory(val);
+ // base();
+ }
+
+ // Construct the interval [inf, sup]
+ protected IntervalElement(BigNum infInt, BigNum supInt)
+ {
+ this.inf = ExtendedInt.Factory(infInt);
+ this.sup = ExtendedInt.Factory(supInt);
+ // base(); // to please the compiler...
+ }
+
+ protected IntervalElement(ExtendedInt! inf, ExtendedInt! sup)
+ {
+ this.inf = inf;
+ this.sup = sup;
+ // base();
+ }
+
+ // Construct an Interval
+ public static IntervalElement! Factory(ExtendedInt! inf, ExtendedInt! sup)
+ {
+ if(inf is MinusInfinity && sup is PlusInfinity)
+ return Top;
+ if(inf > sup)
+ return Bottom;
+ // otherwise...
+ return new IntervalElement(inf, sup);
+ }
+
+ public static IntervalElement! Factory(BigNum i)
+ {
+ return new IntervalElement(i);
+ }
+
+ public static IntervalElement! Factory(BigNum inf, BigNum sup)
+ {
+ ExtendedInt! i = ExtendedInt.Factory(inf);
+ ExtendedInt! s = ExtendedInt.Factory(sup);
+
+ return Factory(i, s);
+ }
+
+ static public IntervalElement! Top
+ {
+ get
+ {
+ return TopInterval;
+ }
+ }
+
+ static public IntervalElement! Bottom
+ {
+ get
+ {
+ return BottomInterval;
+ }
+ }
+
+ public bool IsTop()
+ {
+ return this.inf is MinusInfinity && this.sup is PlusInfinity;
+ }
+
+ public bool IsBottom()
+ {
+ return this.inf > this.sup;
+ }
+
+ #region Below are the arithmetic operations lifted to intervals
+
+ // Addition
+ public static IntervalElement! operator+(IntervalElement! a, IntervalElement! b)
+ {
+ ExtendedInt! inf = a.inf + b.inf;
+ ExtendedInt! sup = a.sup + b.sup;
+
+ return Factory(inf, sup);
+ }
+
+ // Subtraction
+ public static IntervalElement! operator-(IntervalElement! a, IntervalElement! b)
+ {
+ ExtendedInt! inf = a.inf - b.sup;
+ ExtendedInt! sup = a.sup - b.inf;
+
+ IntervalElement! sub = Factory(inf, sup);
+
+ return sub;
+ }
+
+ // Multiplication
+ public static IntervalElement! operator*(IntervalElement! a, IntervalElement! b)
+ {
+ ExtendedInt! infinf = a.inf * b.inf;
+ ExtendedInt! infsup = a.inf * b.sup;
+ ExtendedInt! supinf = a.sup * b.inf;
+ ExtendedInt! supsup = a.sup * b.sup;
+
+ ExtendedInt! inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ ExtendedInt! sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+
+ return Factory(inf, sup);
+ }
+
+ // Division
+ public static IntervalElement! operator/(IntervalElement! a, IntervalElement! b)
+ {
+ if(b.inf.IsZero && b.sup.IsZero) // Check division by zero
+ return IntervalElement.Top;
+
+ ExtendedInt! infinf = a.inf / b.inf;
+ ExtendedInt! infsup = a.inf / b.sup;
+ ExtendedInt! supinf = a.sup / b.inf;
+ ExtendedInt! supsup = a.sup / b.sup;
+
+ ExtendedInt! inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ ExtendedInt! sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+
+ return Factory(inf, sup);
+ }
+
+ // Division
+ public static IntervalElement! operator%(IntervalElement! a, IntervalElement! b)
+ {
+ if(b.inf.IsZero && b.sup.IsZero) // Check division by zero
+ return IntervalElement.Top;
+
+ ExtendedInt! infinf = a.inf % b.inf;
+ ExtendedInt! infsup = a.inf % b.sup;
+ ExtendedInt! supinf = a.sup % b.inf;
+ ExtendedInt! supsup = a.sup % b.sup;
+
+ ExtendedInt inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ ExtendedInt sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+
+ return Factory(inf, sup);
+ }
+
+ #endregion
+
+ #region Overriden methods
+
+ public override Element! Clone()
+ {
+ // Real copying should not be needed because intervals are immutable?
+ return this;
+ /*
+ int valInf = this.inf.Value;
+ int valSup = this.sup.Value;
+
+ ExtendedInt clonedInf = ExtendedInt.Factory(valInf);
+ ExtendedInt clonedSup = ExtendedInt.Factory(valSup);
+
+ return Factory(clonedInf, clonedSup);
+ */
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
+ {
+ return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ public override string! ToString()
+ {
+ return "[" + this.inf + ", " + this.sup + "]";
+ }
+
+ #endregion
+ }
+}
+
+
+ /// The interface for an extended integer
+ abstract class ExtendedInt
+ {
+ private static readonly PlusInfinity! cachedPlusInf = new PlusInfinity();
+ private static readonly MinusInfinity! cachedMinusInf = new MinusInfinity();
+
+ static public ExtendedInt! PlusInfinity
+ {
+ get
+ {
+ return cachedPlusInf;
+ }
+ }
+
+ static public ExtendedInt! MinusInfinity
+ {
+ get
+ {
+ return cachedMinusInf;
+ }
+ }
+
+ public abstract BigNum Value { get; }
+
+ public abstract int Signum { get; }
+
+ public bool IsZero {
+ get {
+ return Signum == 0;
+ }
+ }
+
+ public bool IsPositive {
+ get {
+ return Signum > 0;
+ }
+ }
+
+ public bool IsNegative {
+ get {
+ return Signum < 0;
+ }
+ }
+
+
+ #region Below are the extensions of arithmetic operations on extended integers
+
+ // Addition
+ public static ExtendedInt! operator+(ExtendedInt! a, ExtendedInt! b)
+ {
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return b;
+ } else {
+ return ExtendedInt.Factory(a.Value + b.Value);
+ }
+ }
+
+ // Subtraction
+ public static ExtendedInt! operator-(ExtendedInt! a, ExtendedInt! b)
+ {
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return UnaryMinus(b);
+ } else {
+ return ExtendedInt.Factory(a.Value - b.Value);
+ }
+ }
+
+ // Unary minus
+ public static ExtendedInt! operator-(ExtendedInt! a)
+ {
+ // BUGBUG: Some compiler error prevents the unary minus operator from being used
+ return UnaryMinus(a);
+ }
+
+ // Unary minus
+ public static ExtendedInt! UnaryMinus(ExtendedInt! a)
+ {
+ if(a is PlusInfinity)
+ return cachedMinusInf;
+ if(a is MinusInfinity)
+ return cachedPlusInf;
+ else // a is a PureInteger
+ return new PureInteger(-a.Value);
+ }
+
+ // Multiplication
+ public static ExtendedInt! operator*(ExtendedInt! a, ExtendedInt! b)
+ {
+ if (a.IsZero) {
+ return a;
+ } else if (b.IsZero) {
+ return b;
+ } else if (a is InfinitaryInt) {
+ if (b.IsPositive) {
+ return a;
+ } else {
+ return UnaryMinus(a);
+ }
+ } else if (b is InfinitaryInt) {
+ if (a.IsPositive) {
+ return b;
+ } else {
+ return UnaryMinus(b);
+ }
+ } else {
+ return ExtendedInt.Factory(a.Value * b.Value);
+ }
+ }
+
+ // Division
+ public static ExtendedInt! operator/(ExtendedInt! a, ExtendedInt! b)
+ {
+ if(b.IsZero)
+ {
+ return a.IsPositive? (ExtendedInt) cachedPlusInf : cachedMinusInf;
+ }
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return b;
+ } else {
+ return ExtendedInt.Factory(a.Value / b.Value);
+ }
+ }
+
+ // Modulo
+ public static ExtendedInt! operator%(ExtendedInt! a, ExtendedInt! b)
+ {
+ if(b.IsZero)
+ {
+ return a.IsPositive? (ExtendedInt) cachedPlusInf : cachedMinusInf;
+ }
+ if (a is InfinitaryInt) {
+ return a;
+ } else if (b is InfinitaryInt) {
+ return b;
+ } else {
+ return ExtendedInt.Factory(a.Value % b.Value);
+ }
+ }
+
+ #endregion
+
+ #region Inf and Sup operations
+
+ public abstract int CompareTo(ExtendedInt! that);
+
+ public static bool operator<(ExtendedInt! inf, ExtendedInt! sup)
+ {
+ return inf.CompareTo(sup) < 0;
+ }
+
+ public static bool operator>(ExtendedInt! inf, ExtendedInt! sup)
+ {
+ return inf.CompareTo(sup) > 0;
+ }
+
+ public static bool operator<=(ExtendedInt! inf, ExtendedInt! sup)
+ {
+ return inf.CompareTo(sup) <= 0;
+ }
+
+ public static bool operator>=(ExtendedInt! inf, ExtendedInt! sup)
+ requires inf != null && sup != null;
+ {
+ return inf.CompareTo(sup) >= 0;
+ }
+
+ public static ExtendedInt! Inf(ExtendedInt! inf, ExtendedInt! sup)
+ {
+ if(inf < sup)
+ return inf;
+ else
+ return sup;
+ }
+
+ public static ExtendedInt! Inf(ExtendedInt! a, ExtendedInt! b, ExtendedInt! c, ExtendedInt! d)
+ {
+ ExtendedInt! infab = Inf(a,b);
+ ExtendedInt! infcd = Inf(c,d);
+
+ return Inf(infab, infcd);
+ }
+
+ public static ExtendedInt! Sup(ExtendedInt! inf, ExtendedInt! sup)
+ {
+ if(inf > sup)
+ return inf;
+ else
+ return sup;
+ }
+
+ public static ExtendedInt! Sup(ExtendedInt! a, ExtendedInt! b, ExtendedInt! c, ExtendedInt! d)
+ {
+ ExtendedInt! supab = Sup(a,b);
+ ExtendedInt! supcd = Sup(c,d);
+
+ return Sup(supab, supcd);
+ }
+
+ #endregion
+
+ // Return the ExtendedInt corresponding to the value
+ public static ExtendedInt! Factory(BigNum val)
+ {
+ return new PureInteger(val);
+ }
+ }
+
+ // Stands for a normal (finite) integer x
+ class PureInteger : ExtendedInt
+ {
+ public PureInteger(BigNum i)
+ {
+ this.val = i;
+ }
+
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ public override string! ToString()
+ {
+ return this.Value.ToString();
+ }
+
+ private BigNum val;
+ public override BigNum Value {
+ get
+ {
+ return this.val;
+ }
+ }
+
+ public override int Signum {
+ get {
+ return val.Signum;
+ }
+ }
+
+ public override int CompareTo(ExtendedInt! that) {
+ if (that is PlusInfinity)
+ return -1;
+ else if (that is PureInteger)
+ return this.Value.CompareTo(that.Value);
+ else // then that is a MinusInfinity
+ return 1;
+ }
+ }
+
+ abstract class InfinitaryInt : ExtendedInt
+ {
+ public override BigNum Value
+ {
+ get {
+ throw new InvalidOperationException();
+ }
+ }
+ }
+
+ class PlusInfinity : InfinitaryInt
+ {
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ public override string! ToString()
+ {
+ return "+oo";
+ }
+
+ public override int Signum {
+ get {
+ return 1;
+ }
+ }
+
+ public override int CompareTo(ExtendedInt! that) {
+ if (that is PlusInfinity)
+ return 0;
+ else
+ return 1;
+ }
+ }
+
+ class MinusInfinity : InfinitaryInt
+ {
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ public override string! ToString()
+ {
+ return "-oo";
+ }
+
+ public override int Signum {
+ get {
+ return -1;
+ }
+ }
+
+ public override int CompareTo(ExtendedInt! that) {
+ if (that is MinusInfinity)
+ return 0;
+ else
+ return -1;
+ }
+ }
+}
diff --git a/Source/AIFramework/VariableMap/MicroLattice.ssc b/Source/AIFramework/VariableMap/MicroLattice.ssc new file mode 100644 index 00000000..d38a37c0 --- /dev/null +++ b/Source/AIFramework/VariableMap/MicroLattice.ssc @@ -0,0 +1,79 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework
+{
+ using Microsoft.Contracts;
+ using System.Collections;
+ using System.Diagnostics;
+ using System.Compiler;
+ using Microsoft.AbstractInterpretationFramework.Collections;
+
+ /// <summary>
+ /// Interface for a lattice that works on a per-variable basis.
+ /// </summary>
+ public abstract class MicroLattice : MathematicalLattice
+ {
+ /// <summary>
+ /// Returns the predicate on the given variable for the given
+ /// lattice element.
+ /// </summary>
+ public abstract IExpr! ToPredicate(IVariable! v, Element! e);
+ /* requires !e.IsBottom && !e.IsTop; */
+
+ /// <summary>
+ /// Allows the lattice to specify whether it understands a particular function symbol.
+ ///
+ /// The lattice is always allowed to "true" even when it really can't do anything with
+ /// such functions; however, it is advantageous to say "false" when possible to avoid
+ /// being called to do certain things.
+ ///
+ /// The arguments to a function are provided for context so that the lattice can say
+ /// true or false for the same function symbol in different situations. For example,
+ /// a lattice may understand the multiplication of a variable and a constant but not
+ /// of two variables. The implementation of a lattice should not hold on to the
+ /// arguments.
+ /// </summary>
+ /// <param name="f">The function symbol.</param>
+ /// <param name="args">The argument context.</param>
+ /// <returns>True if it may understand f, false if it does not understand f.</returns>
+ public abstract bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args);
+
+ /// <summary>
+ /// Set this property to true if the implemented MicroLattice can handle basic arithmetic.
+ /// Stated otherwise this property is set to true if the MicroLattice provides a transfer function for a predicate in a given state
+ /// </summary>
+ public virtual bool UnderstandsBasicArithmetics
+ {
+ get { return false; }
+ }
+
+ /// <summary>
+ /// Evaluate the predicate e and a yield the lattice element
+ /// that is implied by it.
+ /// </summary>
+ /// <param name="e">The predicate that is assumed to contain 1 variable.</param>
+ /// <returns>The most precise lattice element that is implied by the predicate.</returns>
+ public abstract Element! EvaluatePredicate(IExpr! e);
+
+ /// <summary>
+ /// Evaluate the predicate e and yield an overapproximation of the predicate under the state that is passed as a parameter
+ /// Note that unless the subclass implement it, the default behavior is to evaluate the predicate stateless, that implies that it
+ /// is evaluated in any possible context, i.e. it is an upper approximation
+ /// </summary>
+ public virtual Element! EvaluatePredicateWithState(IExpr! e, IFunctionalMap state)
+ {
+ return EvaluatePredicate(e);
+ }
+
+ /// <summary>
+ /// Give an expression (often a value) that can be used to substitute for
+ /// the variable.
+ /// </summary>
+ /// <param name="e">A lattice element.</param>
+ /// <returns>The null value if no such expression can be given.</returns>
+ public abstract IExpr GetFoldExpr(Element! e);
+ }
+}
\ No newline at end of file diff --git a/Source/AIFramework/VariableMap/Nullness.ssc b/Source/AIFramework/VariableMap/Nullness.ssc new file mode 100644 index 00000000..63d637ce --- /dev/null +++ b/Source/AIFramework/VariableMap/Nullness.ssc @@ -0,0 +1,227 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using Microsoft.Contracts;
+namespace Microsoft.AbstractInterpretationFramework
+{
+ using System.Collections;
+ using System.Diagnostics;
+ using System.Compiler.Analysis;
+
+ public class NullnessLattice : MicroLattice
+ {
+ readonly INullnessFactory! factory;
+
+ public NullnessLattice(INullnessFactory! factory) {
+ this.factory = factory;
+ // base();
+ }
+
+ enum Value { Bottom, NotNull, Null, MayBeNull }
+
+ private class Elt : Element
+ {
+ public Value value;
+
+ public Elt (Value v) { this.value = v; }
+
+ [Pure][Reads(ReadsAttribute.Reads.Owned)]
+ public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
+ {
+ return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ }
+
+ public override Element! Clone()
+ {
+ return new Elt(this.value);
+ }
+ }
+
+
+ public override Element! Top
+ {
+ get { return new Elt(Value.MayBeNull); }
+ }
+
+ public override Element! Bottom
+ {
+ get { return new Elt(Value.Bottom); }
+ }
+
+ public static Element! Null
+ {
+ get { return new Elt(Value.Null); }
+ }
+
+ public static Element! NotNull
+ {
+ get { return new Elt(Value.NotNull); }
+ }
+
+ public override bool IsTop (Element! element)
+ {
+ Elt e = (Elt) element;
+ return e.value == Value.MayBeNull;
+ }
+
+ public override bool IsBottom (Element! element)
+ {
+ Elt e = (Elt) element;
+ return e.value == Value.Bottom;
+ }
+
+ public override Lattice.Element! NontrivialJoin (Element! first, Element! second)
+ {
+ Elt a = (Elt) first;
+ Elt b = (Elt) second;
+ return (a.value == b.value) ? a : (Elt)Top;
+ }
+
+ public override Lattice.Element! NontrivialMeet (Element! first, Element! second)
+ {
+ Elt a = (Elt) first;
+ Elt b = (Elt) second;
+ return (a.value == b.value) ? a : (Elt)Bottom;
+ }
+
+ public override Element! Widen (Element! first, Element! second)
+ {
+ return Join(first,second);
+ }
+
+ protected override bool AtMost (Element! first, Element! second) // this <= that
+ {
+ Elt a = (Elt) first;
+ Elt b = (Elt) second;
+ return a.value == b.value;
+ }
+
+ public override IExpr! ToPredicate(IVariable! var, Element! element) {
+ Elt e = (Elt)element;
+
+ if (e.value == Value.NotNull)
+ {
+ return factory.Neq(var, factory.Null);
+ }
+ if (e.value == Value.Null)
+ {
+ return factory.Eq(var, factory.Null);
+ }
+ assert false;
+ throw new System.Exception();
+ }
+
+ public override IExpr GetFoldExpr(Element! e) {
+ Elt elt = (Elt)e;
+ if (elt.value == Value.Null) {
+ return factory.Null;
+ } else {
+ // can't fold into an expression
+ return null;
+ }
+ }
+
+ public override bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args) {
+ if (f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq) ||
+ f.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
+
+ assert args.Count == 2;
+ IExpr! arg0 = (IExpr!)args[0];
+ IExpr! arg1 = (IExpr!)args[1];
+
+ // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
+ if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
+ return true;
+ } else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ public override Element! EvaluatePredicate(IExpr! e) {
+ IFunApp nary = e as IFunApp;
+ if (nary != null) {
+ bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
+ IList/*<IExpr!>*/! args = nary.Arguments;
+ assert args.Count == 2;
+ IExpr! arg0 = (IExpr!)args[0];
+ IExpr! arg1 = (IExpr!)args[1];
+
+ // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
+ IVariable var = null;
+ if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null)
+ {
+ var = (IVariable)arg0;
+ }
+ else if (arg1 is IVariable && arg0 is IFunApp && ((IFunApp)arg0).FunctionSymbol == Ref.Null)
+ {
+ var = (IVariable)arg1;
+ }
+
+ if (var != null) // found the pattern
+ {
+ return isEq ? Null:NotNull;
+ }
+ }
+ }
+ return Top;
+ }
+ }
+
+#if false
+
+ public class NullnessMicroLattice : MicroLattice
+ {
+ public override MicroLatticeElement Top { get { return NullnessLatticeElement.Top; } }
+ public override MicroLatticeElement Bottom { get { return NullnessLatticeElement.Bottom; } }
+
+
+ public override MicroLatticeElement EvaluateExpression (Expr e, LookupValue lookup)
+ {
+ if (e is LiteralExpr && ((LiteralExpr)e).Val == null)
+ {
+ return NullnessLatticeElement.Null;
+ }
+ return Top;
+ }
+
+
+ public override MicroLatticeElement EvaluatePredicate (Expr e, LookupValue lookup)
+ {
+ NAryExpr nary = e as NAryExpr;
+ if (nary != null &&
+ (nary.Fun.FunctionName.Equals("==") || nary.Fun.FunctionName.Equals("!=")))
+ {
+ Debug.Assert(nary.Args.Length == 2);
+
+ Expr arg0 = nary.Args[0], arg1 = nary.Args[1];
+ Variable var = null;
+
+ // Look for "x OP null" or "null OP x" where OP is "==" or "!=".
+ if (arg0 is IdentifierExpr && arg1 is LiteralExpr && ((LiteralExpr)arg1).Val == null)
+ {
+ var = ((IdentifierExpr)arg0).Decl;
+ }
+ else if (arg1 is IdentifierExpr && arg0 is LiteralExpr && ((LiteralExpr)arg0).Val == null)
+ {
+ var = ((IdentifierExpr)arg1).Decl;
+ }
+
+ if (var != null) // found the pattern
+ {
+ return nary.Fun.FunctionName.Equals("==") ?
+ NullnessLatticeElement.Null :
+ NullnessLatticeElement.NotNull;
+ }
+ }
+ return Top;
+ }
+ }
+
+#endif
+
+}
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();
+ }
+
+ }
+}
|