From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Wed, 15 Jul 2009 21:03:41 +0000 Subject: Initial set of files. --- Source/AIFramework/AIFramework.sscproj | 157 ++ Source/AIFramework/CommonFunctionSymbols.ssc | 926 ++++++++++ Source/AIFramework/Expr.ssc | 447 +++++ Source/AIFramework/Functional.ssc | 284 +++ Source/AIFramework/Lattice.ssc | 685 ++++++++ Source/AIFramework/Logger.ssc | 49 + Source/AIFramework/MultiLattice.ssc | 563 ++++++ Source/AIFramework/Mutable.ssc | 117 ++ Source/AIFramework/Polyhedra/LinearConstraint.ssc | 588 +++++++ .../Polyhedra/LinearConstraintSystem.ssc | 1856 ++++++++++++++++++++ .../AIFramework/Polyhedra/PolyhedraAbstraction.ssc | 744 ++++++++ Source/AIFramework/Polyhedra/SimplexTableau.ssc | 717 ++++++++ .../VariableMap/ConstantAbstraction.ssc | 210 +++ .../VariableMap/ConstantExpressions.ssc | 538 ++++++ .../AIFramework/VariableMap/DynamicTypeLattice.ssc | 475 +++++ Source/AIFramework/VariableMap/Intervals.ssc | 790 +++++++++ Source/AIFramework/VariableMap/MicroLattice.ssc | 79 + Source/AIFramework/VariableMap/Nullness.ssc | 227 +++ .../AIFramework/VariableMap/VariableMapLattice.ssc | 749 ++++++++ 19 files changed, 10201 insertions(+) create mode 100644 Source/AIFramework/AIFramework.sscproj create mode 100644 Source/AIFramework/CommonFunctionSymbols.ssc create mode 100644 Source/AIFramework/Expr.ssc create mode 100644 Source/AIFramework/Functional.ssc create mode 100644 Source/AIFramework/Lattice.ssc create mode 100644 Source/AIFramework/Logger.ssc create mode 100644 Source/AIFramework/MultiLattice.ssc create mode 100644 Source/AIFramework/Mutable.ssc create mode 100644 Source/AIFramework/Polyhedra/LinearConstraint.ssc create mode 100644 Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc create mode 100644 Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc create mode 100644 Source/AIFramework/Polyhedra/SimplexTableau.ssc create mode 100644 Source/AIFramework/VariableMap/ConstantAbstraction.ssc create mode 100644 Source/AIFramework/VariableMap/ConstantExpressions.ssc create mode 100644 Source/AIFramework/VariableMap/DynamicTypeLattice.ssc create mode 100644 Source/AIFramework/VariableMap/Intervals.ssc create mode 100644 Source/AIFramework/VariableMap/MicroLattice.ssc create mode 100644 Source/AIFramework/VariableMap/Nullness.ssc create mode 100644 Source/AIFramework/VariableMap/VariableMapLattice.ssc (limited to 'Source/AIFramework') diff --git a/Source/AIFramework/AIFramework.sscproj b/Source/AIFramework/AIFramework.sscproj new file mode 100644 index 00000000..dd79b9b8 --- /dev/null +++ b/Source/AIFramework/AIFramework.sscproj @@ -0,0 +1,157 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/Source/AIFramework/CommonFunctionSymbols.ssc b/Source/AIFramework/CommonFunctionSymbols.ssc new file mode 100644 index 00000000..4e38fbcb --- /dev/null +++ b/Source/AIFramework/CommonFunctionSymbols.ssc @@ -0,0 +1,926 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework +{ + using Microsoft.Contracts; + using System.Collections; + using Microsoft.SpecSharp.Collections; + using Microsoft.Basetypes; + + /// + /// A basic class for function symbols. + /// + public class FunctionSymbol : IFunctionSymbol + { + private readonly string! display; + private readonly AIType! typ; + + public FunctionSymbol(AIType! typ) + : this("FunctionSymbol", typ) + { + } + + internal FunctionSymbol(string! display, AIType! typ) + { + this.display = display; + this.typ = typ; + // base(); + } + +// public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } } + public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } } + + [NoDefaultContract] + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override string! ToString() + { + return display; + } + + } + + /// + /// A class for integer constants. + /// + public class IntSymbol : FunctionSymbol + { + public readonly BigNum Value; + + /// + /// The intention is that this constructor be called only from the Int.Const method. + /// + internal IntSymbol(BigNum x) + : base((!)x.ToString(), Int.Type) + { + this.Value = x; + } + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) + { + IntSymbol isym = other as IntSymbol; + return isym != null && isym.Value.Equals(this.Value); + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override int GetHashCode() + { + return Value.GetHashCode(); + } + } + + /// + /// A class for bitvector constants. + /// + public class BvSymbol : FunctionSymbol + { + public readonly BigNum Value; + public readonly int Bits; + + /// + /// The intention is that this constructor be called only from the Int.Const method. + /// + internal BvSymbol(BigNum x, int y) + : base(x + "bv" + y, Bv.Type) + { + this.Value = x; + this.Bits = y; + } + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) + { + BvSymbol isym = other as BvSymbol; + return isym != null && isym.Value == this.Value && isym.Bits == this.Bits; + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override int GetHashCode() + { + unchecked { + return Value.GetHashCode() ^ Bits; + } + } + } + + public class DoubleSymbol : FunctionSymbol + { + public readonly double Value; + + /// + /// The intention is that this constructor be called only from the Double.Const method. + /// + internal DoubleSymbol(double x) + : base((!)x.ToString(), Double.Type) + { + this.Value = x; + } + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) + { + DoubleSymbol dsym = other as DoubleSymbol; + return dsym != null && dsym.Value == this.Value; + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override int GetHashCode() + { + return Value.GetHashCode(); + } + } + + /// + /// Function symbol based on a string. Uses the string equality for determining equality + /// of symbol. + /// + public class NamedSymbol : FunctionSymbol + { + public string! Value { [NoDefaultContract] get { return (!) this.ToString(); } } + + public NamedSymbol(string! symbol, AIType! typ) + : base(symbol, typ) + { + } + + [NoDefaultContract] + [Pure][Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) + { + NamedSymbol nsym = other as NamedSymbol; + return nsym != null && this.Value.Equals(nsym.Value); + } + + [NoDefaultContract] + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override int GetHashCode() + { + return Value.GetHashCode(); + } + } + + // + // In the following, the classes like Value and Prop serve two + // roles. The primary role is to be the base types for AIType. + // The only objects of these classes are the representative + // objects that denote an AIType, which are given by the + // "Type" property. Subtypes in the AIType language are + // encoded by subclassing. This yields some "higher-orderness" + // for checking subtyping in the AIType language, by using + // the Spec#/C# subclassing checks. + // + // The other role is simply as a module for collecting like function + // symbols. + // + + //-------------------------- Terms ---------------------------------- + + /// + /// A class with the equality symbol and the ValueType.Type. + /// + public class Value : AIType + { + private static readonly AIType! valtype = new Value(); + public static AIType! Type { get { return valtype; } } + + private static readonly FunctionType[]! funtypeCache = new FunctionType[5]; + public static FunctionType! FunctionType(int inParameterCount) + requires 0 <= inParameterCount; + // ensures result.Arity == inParameterCount; + { + FunctionType result; + if (inParameterCount < funtypeCache.Length) { + result = funtypeCache[inParameterCount]; + if (result != null) { + return result; + } + } + AIType[] signature = new AIType[1 + inParameterCount]; + for (int i = 0; i < signature.Length; i++) { + signature[i] = valtype; + } + result = new FunctionType(signature); + if (inParameterCount < funtypeCache.Length) { + funtypeCache[inParameterCount] = result; + } + return result; + } + + [Once] private static AIType! binreltype; + private static AIType! BinrelType { + get { + if (binreltype == null) { + binreltype = new FunctionType(Type, Type, Prop.Type); + } + return binreltype; + } + } + + [Once] private static FunctionSymbol! _eq; + public static FunctionSymbol! Eq { + get { + if (_eq == null) { + _eq = new FunctionSymbol("=", BinrelType); + } + return _eq; + } + } + [Once] private static FunctionSymbol! _neq; + public static FunctionSymbol! Neq { + get { + if (_neq == null) { + _neq = new FunctionSymbol("!=", BinrelType); + } + return _neq; + } + } + [Once] private static FunctionSymbol! _subtype; + public static FunctionSymbol! Subtype { + get { + if (_subtype == null) { + _subtype = new FunctionSymbol("<:", BinrelType); + } + return _subtype; + } + } + + [Once] private static AIType! typeof_type; + private static AIType! TypeofType { + get { + if (typeof_type == null) { + typeof_type = new FunctionType(Ref.Type, Type); + } + return typeof_type; + } + } + [Once] private static FunctionSymbol! _typeof; + public static FunctionSymbol! Typeof { + get { + if (_typeof == null) { + _typeof = new FunctionSymbol("typeof", TypeofType); + } + return _typeof; + } + } + + /// + /// Value should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + protected Value() { } + + } + + public class Int : Value + { + private static readonly AIType! inttype = new Int(); + public static AIType! Type { get { return inttype; } } + + private static readonly AIType! unaryinttype = new FunctionType(Type, Type); + private static readonly AIType! bininttype = new FunctionType(Type, Type, Type); + private static readonly AIType! relationtype = new FunctionType(Type, Type, Prop.Type); + + private static readonly FunctionSymbol! _negate = new FunctionSymbol("~", unaryinttype); + private static readonly FunctionSymbol! _add = new FunctionSymbol("+", bininttype); + private static readonly FunctionSymbol! _sub = new FunctionSymbol("-", bininttype); + private static readonly FunctionSymbol! _mul = new FunctionSymbol("*", bininttype); + private static readonly FunctionSymbol! _div = new FunctionSymbol("/", bininttype); + private static readonly FunctionSymbol! _mod = new FunctionSymbol("%", bininttype); + private static readonly FunctionSymbol! _atmost = new FunctionSymbol("<=", relationtype); + private static readonly FunctionSymbol! _less = new FunctionSymbol("<", relationtype); + private static readonly FunctionSymbol! _greater = new FunctionSymbol(">", relationtype); + private static readonly FunctionSymbol! _atleast = new FunctionSymbol(">=", relationtype); + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Negate { get { return _negate; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Add { get { return _add; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Sub { get { return _sub; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mul { get { return _mul; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Div { get { return _div; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mod { get { return _mod; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtMost { get { return _atmost; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Less { get { return _less; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Greater { get { return _greater; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtLeast { get { return _atleast; } } + + public static IntSymbol! Const(BigNum x) + { + // We could cache things here, but for now we don't. + return new IntSymbol(x); + } + + /// + /// Int should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Int() { } + } + + public class Double : Value + { + private static readonly AIType! doubletype = new Double(); + public static AIType! Type { get { return doubletype; } } + + public static DoubleSymbol! Const(double x) + { + // We could cache things here, but for now we don't. + return new DoubleSymbol(x); + } + + /// + /// Double should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Double() { } + } + + public class Bv : Value + { + private static readonly AIType! bvtype = new Bv(); + public static AIType! Type { get { return bvtype; } } + + private static readonly AIType! unaryinttype = new FunctionType(Type, Type); + private static readonly AIType! bininttype = new FunctionType(Type, Type, Type); + private static readonly AIType! relationtype = new FunctionType(Type, Type, Prop.Type); + + private static readonly FunctionSymbol! _negate = new FunctionSymbol("~", unaryinttype); + private static readonly FunctionSymbol! _add = new FunctionSymbol("+", bininttype); + private static readonly FunctionSymbol! _sub = new FunctionSymbol("-", bininttype); + private static readonly FunctionSymbol! _mul = new FunctionSymbol("*", bininttype); + private static readonly FunctionSymbol! _div = new FunctionSymbol("/", bininttype); + private static readonly FunctionSymbol! _mod = new FunctionSymbol("%", bininttype); + private static readonly FunctionSymbol! _concat = new FunctionSymbol("$concat", bininttype); + private static readonly FunctionSymbol! _extract = new FunctionSymbol("$extract", unaryinttype); + private static readonly FunctionSymbol! _atmost = new FunctionSymbol("<=", relationtype); + private static readonly FunctionSymbol! _less = new FunctionSymbol("<", relationtype); + private static readonly FunctionSymbol! _greater = new FunctionSymbol(">", relationtype); + private static readonly FunctionSymbol! _atleast = new FunctionSymbol(">=", relationtype); + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Negate { get { return _negate; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Add { get { return _add; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Sub { get { return _sub; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mul { get { return _mul; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Div { get { return _div; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mod { get { return _mod; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtMost { get { return _atmost; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Less { get { return _less; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Greater { get { return _greater; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtLeast { get { return _atleast; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Extract { get { return _extract; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Concat { get { return _concat; } } + + public static BvSymbol! Const(BigNum x, int y) + { + // We could cache things here, but for now we don't. + return new BvSymbol(x, y); + } + + /// + /// Int should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Bv() { } + } + + public class Ref : Value + { + private static readonly AIType! reftype = new Ref(); + public static AIType! Type { get { return reftype; } } + + private static readonly FunctionSymbol! _null = new FunctionSymbol("null", Type); + + public static FunctionSymbol! Null { get { return _null; } } + + /// + /// Ref should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Ref() { } + } + + public class HeapStructure : Value + { + private static readonly AIType! reftype = new HeapStructure(); + public static AIType! Type { get { return reftype; } } + + + + /// + /// HeapStructure should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private HeapStructure() { } + } + + public class FieldName : Value + { + private static readonly AIType! fieldnametype = new FieldName(); + public static AIType! Type { get { return fieldnametype; } } + + private static readonly FunctionSymbol! _allocated = new FunctionSymbol("$allocated", FieldName.Type); + public static FunctionSymbol! Allocated { get { return _allocated; } } + + /// + /// Is this a boolean field that monotonically goes from false to true? + /// + public static bool IsBooleanMonotonicallyWeakening(IFunctionSymbol! f) + { + return f.Equals(Allocated); + } + + /// + /// FieldName should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private FieldName() { } + } + + public class Heap : Value + { + private static readonly AIType! heaptype = new Heap(); + public static AIType! Type { get { return heaptype; } } + + // the types in the following, select1, select2, are hard-coded; + // these types may not always be appropriate + private static readonly FunctionSymbol! _select1 = new FunctionSymbol("sel1", + // Heap x FieldName -> Prop + new FunctionType(Type, FieldName.Type, Prop.Type) + ); + public static FunctionSymbol! Select1 { get { return _select1; } } + + private static readonly FunctionSymbol! _select2 = new FunctionSymbol("sel2", + // Heap x Ref x FieldName -> Value + new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type) + ); + public static FunctionSymbol! Select2 { get { return _select2; } } + + // the types in the following, store1, store2, are hard-coded; + // these types may not always be appropriate + private static readonly FunctionSymbol! _update1 = new FunctionSymbol("upd1", + // Heap x FieldName x Value -> Heap + new FunctionType(Type, FieldName.Type, Value.Type, Type) + ); + public static FunctionSymbol! Update1 { get { return _update1; } } + + private static readonly FunctionSymbol! _update2 = new FunctionSymbol("upd2", + // Heap x Ref x FieldName x Value -> Heap + new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type, Type) + ); + public static FunctionSymbol! Update2 { get { return _update2; } } + + private static readonly FunctionSymbol! _unsupportedHeapOp = + new FunctionSymbol("UnsupportedHeapOp", + // Heap x FieldName -> Prop + new FunctionType(Type, FieldName.Type, Prop.Type) + ); + public static FunctionSymbol! UnsupportedHeapOp { get { return _unsupportedHeapOp; } } + + /// + /// Heap should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Heap() { } + } + +// public class List : Value +// { +// private static IDictionary/**/! lists = new Hashtable(); +// public static AIType! Type(AIType! typeParameter) +// { +// if (lists.Contains(typeParameter)) +// return lists[typeParameter]; +// else +// { +// AIType! result = new List(typeParameter); +// lists[typeParameter] = result; +// return result; +// } +// } +// +// private static IDictionary/**/! nils = new Hashtable(); +// public static FunctionSymbol! Nil(AIType! typeParameter) +// { +// if (nils.Contains(typeParameter)) +// return nils[typeParameter]; +// else +// { +// FunctionSymbol! result = new FunctionSymbol(Type(typeParameter)); +// nils[typeParameter] = result; +// return result; +// } +// } +// +// private static IDictionary/**/! cons = new Hashtable(); +// public static FunctionSymbol! Cons(AIType! typeParameter) +// { +// if (cons.Contains(typeParameter)) +// return cons[typeParameter]; +// else +// { +// FunctionSymbol! result = new FunctionSymbol( +// new FunctionType(typeParameter, Type(typeParameter), Type(typeParameter)) +// ); +// cons[typeParameter] = result; +// return result; +// } +// } +// +// private AIType! typeParameter; +// public AIType! TypeParameter { get { return typeParameter; } } +// +// /// +// /// List should not be instantiated from the outside. +// /// +// private List(AIType! typeParameter) +// { +// this.typeParameter = typeParameter; +// } +// } +// +// public class Pair : Value +// { +// private static IDictionary! pairs = new Hashtable(); +// public static AIType! Type(AIType! type1, AIType! type2) +// { +// Microsoft.AbstractInterpretationFramework.Collections.Pair typpair +// = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2); +// +// if (pairs.Contains(typpair)) +// return pairs[typpair]; +// else +// { +// AIType! result = new Pair(type1, type2); +// pairs[typpair] = result; +// return result; +// } +// } +// +// private static IDictionary! constructs = new Hashtable(); +// public static FunctionSymbol! Pair(AIType! type1, AIType! type2) +// { +// Microsoft.AbstractInterpretationFramework.Collections.Pair typpair +// = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2); +// +// if (constructs.Contains(typpair)) +// return constructs[typpair]; +// else +// { +// FunctionSymbol! result = new FunctionSymbol( +// new FunctionType(type1, type2, Type(type1, type2)) +// ); +// constructs[typpair] = result; +// return result; +// } +// } +// +// protected AIType! type1; +// protected AIType! type2; +// +// public AIType! Type1 { get { return type1; } } +// public AIType! Type2 { get { return type2; } } +// +// /// +// /// Pair should not be instantiated from the outside, except by subclasses. +// /// +// protected Pair(AIType! type1, AIType! type2) +// { +// this.type1 = type1; +// this.type2 = type2; +// } +// } + + //-------------------------- Propositions --------------------------- + + + /// + /// A class with global propositional symbols and the Prop.Type. + /// + public sealed class Prop : AIType + { + private static readonly AIType! proptype = new Prop(); + public static AIType! Type { get { return proptype; } } + + private static readonly AIType! unaryproptype = new FunctionType(Type, Type); + private static readonly AIType! binproptype = new FunctionType(Type, Type, Type); + private static readonly AIType! quantifiertype = + new FunctionType(new FunctionType(Value.Type, Type), Type); + + private static readonly FunctionSymbol! _false = new FunctionSymbol("false", Type); + private static readonly FunctionSymbol! _true = new FunctionSymbol("true", Type); + private static readonly FunctionSymbol! _not = new FunctionSymbol("!", unaryproptype); + private static readonly FunctionSymbol! _and = new FunctionSymbol("/\\", binproptype); + private static readonly FunctionSymbol! _or = new FunctionSymbol("\\/", binproptype); + private static readonly FunctionSymbol! _implies = new FunctionSymbol("==>", binproptype); + private static readonly FunctionSymbol! _exists = new FunctionSymbol("Exists", quantifiertype); + private static readonly FunctionSymbol! _forall = new FunctionSymbol("Forall", quantifiertype); + + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! False { get { return _false; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! True { get { return _true; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Not { get { return _not; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! And { [Pure] get { return _and; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Or { get { return _or; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Implies { get { return _implies; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Exists { get { return _exists; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Forall { get { return _forall; } } + + + /// + /// Prop should not be instantiated from the outside. + /// + private Prop() { } + + + + // + // Utility Methods + // + + public static IExpr! SimplifiedAnd(IPropExprFactory! factory, IExpr! e0, IExpr! e1) + { + IFunApp fun0 = e0 as IFunApp; + if (fun0 != null) + { + if (fun0.FunctionSymbol.Equals(Prop.True)) + { + return e1; + } + else if (fun0.FunctionSymbol.Equals(Prop.False)) + { + return e0; + } + } + + IFunApp fun1 = e1 as IFunApp; + if (fun1 != null) + { + if (fun1.FunctionSymbol.Equals(Prop.True)) + { + return e0; + } + else if (fun1.FunctionSymbol.Equals(Prop.False)) + { + return e1; + } + } + + return factory.And(e0, e1); + } + + public static IExpr! SimplifiedAnd(IPropExprFactory! factory, IEnumerable/**/! exprs) + { + IExpr! result = factory.True; + foreach (IExpr! conjunct in exprs) + { + result = SimplifiedAnd(factory, result, conjunct); + } + return result; + } + + public static IExpr! SimplifiedOr(IPropExprFactory! factory, IExpr! e0, IExpr! e1) + { + IFunApp fun0 = e0 as IFunApp; + if (fun0 != null) + { + if (fun0.FunctionSymbol.Equals(Prop.False)) + { + return e1; + } + else if (fun0.FunctionSymbol.Equals(Prop.True)) + { + return e0; + } + } + + IFunApp fun1 = e1 as IFunApp; + if (fun1 != null) + { + if (fun1.FunctionSymbol.Equals(Prop.False)) + { + return e0; + } + else if (fun1.FunctionSymbol.Equals(Prop.True)) + { + return e1; + } + } + + return factory.Or(e0, e1); + } + + public static IExpr! SimplifiedOr(IPropExprFactory! factory, IEnumerable/**/! exprs) + { + IExpr! result = factory.False; + foreach (IExpr! disj in exprs) + { + result = SimplifiedOr(factory, result, disj); + } + return result; + } + + + + /// + /// Break top-level conjuncts into a list of sub-expressions. + /// + /// The expression to examine. + /// A list of conjuncts. + internal static IList/**/! BreakConjuncts(IExpr! e) + ensures forall{ IExpr sub in result; sub is IFunApp ==> !((IFunApp) sub).FunctionSymbol.Equals(Prop.And) }; + { + return BreakJuncts(e, Prop.And); + } + + /// + /// Break top-level disjuncts into a list of sub-expressions. + /// + /// The expression to examine. + /// A list of conjuncts. + internal static IList/**/! BreakDisjuncts(IExpr! e) + ensures forall{ IExpr sub in result; sub is IFunApp ==> !((IFunApp) sub).FunctionSymbol.Equals(Prop.Or) }; + { + return BreakJuncts(e, Prop.Or); + } + + private static IList/**/! BreakJuncts(IExpr! e, IFunctionSymbol! sym) + ensures forall{ IExpr sub in result; sub is IFunApp ==> !((IFunApp) sub).FunctionSymbol.Equals(sym) }; + { + ArrayList/**/! result = new ArrayList(); + + IFunApp f = e as IFunApp; + if (f != null) + { + // If it is a sym, go down into sub-expressions. + if (f.FunctionSymbol.Equals(sym)) + { + foreach (IExpr! arg in f.Arguments) + { + result.AddRange(BreakJuncts(arg,sym)); + } + } + // Otherwise, stop. + else + { + result.Add(e); + } + } + else + { + result.Add(e); + } + + return result; + } + } + + /// + /// A callback to produce a function body given the bound variable. + /// + /// The bound variable to use. + /// The function body. + public delegate IExpr! FunctionBody(IVariable! var); + + /// + /// An interface for constructing propositional expressions. + /// + /// This interface should be implemented by the client. An implementation of + /// of this class should generally be used as a singleton object. + /// + public interface IPropExprFactory + { + IFunApp! False { get /*ensures result.FunctionSymbol.Equals(Prop.False);*/; } + IFunApp! True { get /*ensures result.FunctionSymbol.Equals(Prop.True);*/; } + + IFunApp! Not(IExpr! p) /*ensures result.FunctionSymbol.Equals(Prop.Not);*/; + + IFunApp! And(IExpr! p, IExpr! q) /*ensures result.FunctionSymbol.Equals(Prop.And);*/; + IFunApp! Or(IExpr! p, IExpr! q) /*ensures result.FunctionSymbol.Equals(Prop.Or);*/; + + IFunApp! Implies(IExpr! p, IExpr! q) /*ensures result.FunctionSymbol.Equals(Prop.Implies);*/; + } + + /// + /// Like IPropExprFactory, but also with quantifiers. + /// + public interface IQuantPropExprFactory : IPropExprFactory { + /// + /// Produce an existential given the lambda-expression. + /// + /// The lambda-expression. + /// The existential. + IFunApp! Exists(IFunction! p) /*ensures result.FunctionSymbol.Equals(Prop.Exists);*/; + IFunApp! Forall(IFunction! p) /*ensures result.FunctionSymbol.Equals(Prop.Forall);*/; + + /// + /// Produce an existential given a callback that can produce a function body given the + /// bound variable to use. The implementer of this method is responsible for generating + /// a fresh new variable to pass to the FunctionBody callback to use as the bound variable. + /// + /// The function body callback. + /// The existential. + IFunApp! Exists(AIType paramType, FunctionBody! body) /*ensures result.FunctionSymbol.Equals(Prop.Exists);*/; + IFunApp! Forall(AIType paramType, FunctionBody! body) /*ensures result.FunctionSymbol.Equals(Prop.Forall);*/; + } + + /// + /// An interface for constructing value expressions. + /// + /// This interface should be implemented by the client. An implementation of + /// of this class should generally be used as a singleton object. + /// + public interface IValueExprFactory + { + IFunApp! Eq(IExpr! e0, IExpr! e1) /*ensures result.FunctionSymbol.Equals(Value.Eq);*/; + IFunApp! Neq(IExpr! e0, IExpr! e1) /*ensures result.FunctionSymbol.Equals(Value.Neq);*/; + } + + /// + /// An interface for constructing value expressions having to with null. + /// + /// This interface should be implemented by the client. An implementation of + /// of this class should generally be used as a singleton object. + /// + public interface INullnessFactory + { + IFunApp! Eq(IExpr! e0, IExpr! e1) /*ensures result.FunctionSymbol.Equals(Value.Eq);*/; + IFunApp! Neq(IExpr! e0, IExpr! e1) /*ensures result.FunctionSymbol.Equals(Value.Neq);*/; + IFunApp! Null { get; /*ensures result.FunctionSymbol.Equals(Ref.Null);*/ } + } + + /// + /// An interface for constructing integer expressions. + /// + /// This interface should be implemented by the client. An implementation of + /// of this class should generally be used as a singleton object. + /// + public interface IIntExprFactory : IValueExprFactory + { + IFunApp! Const(BigNum i) /*ensures result.FunctionSymbol.Equals(new IntSymbol(i));*/; + } + + /// + /// An interface for constructing linear integer expressions. + /// + /// This interface should be implemented by the client. An implementation of + /// of this class should generally be used as a singleton object. + /// + public interface ILinearExprFactory : IIntExprFactory + { + IFunApp! AtMost(IExpr! e0, IExpr! e1) /*ensures result.FunctionSymbol.Equals(Value.AtMost);*/; + IFunApp! Add(IExpr! e0, IExpr! e1) /*ensures result.FunctionSymbol.Equals(Value.Add);*/; + /// + /// If "var" is null, returns an expression representing r. + /// Otherwise, returns an expression representing r*var. + /// + IExpr! Term(Microsoft.Basetypes.Rational r, IVariable var); + + IFunApp! False { get /*ensures result.FunctionSymbol.Equals(Prop.False);*/; } + IFunApp! True { get /*ensures result.FunctionSymbol.Equals(Prop.True);*/; } + IFunApp! And(IExpr! p, IExpr! q) /*ensures result.FunctionSymbol.Equals(Prop.And);*/; + } + + /// + /// An interface for constructing type expressions and performing some type operations. + /// The types are assumed to be arranged in a rooted tree. + /// + /// This interface should be implemented by the client. An implementation of + /// of this class should generally be used as a singleton object. + /// + public interface ITypeExprFactory + { + /// + /// Returns an expression denoting the top of the type hierarchy. + /// + IExpr! RootType { get; } + + /// + /// Returns true iff "t" denotes a type constant. + /// + [Pure][Reads(ReadsAttribute.Reads.Owned)] + bool IsTypeConstant(IExpr! t); + + /// + /// Returns true iff t0 and t1 are types such that t0 and t1 are equal. + /// + [Pure][Reads(ReadsAttribute.Reads.Owned)] + bool IsTypeEqual(IExpr! t0, IExpr! t1); + + /// + /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1. + /// + [Pure][Reads(ReadsAttribute.Reads.Owned)] + bool IsSubType(IExpr! t0, IExpr! t1); + + /// + /// Returns the most derived supertype of both "t0" and "t1". A precondition is + /// that "t0" and "t1" both represent types. + /// + IExpr! JoinTypes(IExpr! t0, IExpr! t1); + + IFunApp! IsExactlyA(IExpr! e, IExpr! type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Eq);*/; + IFunApp! IsA(IExpr! e, IExpr! type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Subtype);*/; + } + +} diff --git a/Source/AIFramework/Expr.ssc b/Source/AIFramework/Expr.ssc new file mode 100644 index 00000000..94dc4dc7 --- /dev/null +++ b/Source/AIFramework/Expr.ssc @@ -0,0 +1,447 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +// This file specifies the expression language used by the Abstract +// Interpretation Framework. +// +// expressions e ::= x variables +// | f(e1,...,en) uninterpreted functions +// | \x:t.e lambda expressions +// +// types t ::= b user-defined/built-in base types +// | t1 * ... * tn -> t' function type + +namespace Microsoft.AbstractInterpretationFramework +{ + using System.Collections; + using Microsoft.Contracts; + + //----------------------------- Expressions ----------------------------- + + /// + /// An interface for expressions. This expression language is specified + /// by interfaces to allow the client to be able to use their existing + /// AST nodes as AIF expressions. + /// + /// This only serves as a place for operations on expressions. Clients + /// should implement directly either IVariable or IFunApp. + /// + public interface IExpr + { + /// + /// Execute a visit over the expression. + /// + /// The expression visitor. + /// The result of the visit. + [Pure][Reads(ReadsAttribute.Reads.Owned)] object DoVisit(ExprVisitor! visitor); + + // TODO: Type checking of the expressions. + } + + /// + /// An interface for variables. + /// + /// This interface should be implemented by the client. + /// + public interface IVariable : IExpr + { + string! Name { get; } // Each client must define the name for variables + } + + /// + /// An interface for function applications. + /// + /// This interface should be implemented by the client. + /// + public interface IFunApp : IExpr + { + IFunctionSymbol! FunctionSymbol { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; } + IList/**/! Arguments + { + [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep] get + ensures result.IsReadOnly; + ; + } + + /// + /// Provides a method to create a new uninterpreted function + /// with the same function symbol but with the arguments with + /// args. + /// + /// The new arguments. + /// A copy of the function with the new arguments. + IFunApp! CloneWithArguments(IList/**/! args) + //TODO requires this.Arguments.Count == args.Count; + ; + } + + /// + /// An interface for anonymous functions (i.e., lambda expressions) + /// + public interface IFunction : IExpr + { + IVariable! Param { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; } + AIType! ParamType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; } + IExpr! Body { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; } + + IFunction! CloneWithBody(IExpr! body); + } + + /// + /// An abstract class that provides an interface for expression visitors. + /// + public abstract class ExprVisitor + { + public abstract object Default(IExpr! expr); + + public virtual object VisitVariable(IVariable! var) + { + return Default(var); + } + + public virtual object VisitFunApp(IFunApp! funapp) + { + return Default(funapp); + } + + public virtual object VisitFunction(IFunction! fun) + { + return Default(fun); + } + } + + /// + /// A utility class for dealing with expressions. + /// + public sealed class ExprUtil + { + /// + /// Yield an expression that is 'inexpr' with 'var' replaced by 'subst'. + /// + /// The expression to substitute. + /// The variable to substitute for. + /// The expression to substitute into. + public static IExpr! Substitute(IExpr! subst, IVariable! var, IExpr! inexpr) + { + IExpr result = null; + + if (inexpr is IVariable) + { + result = inexpr.Equals(var) ? subst : inexpr; + } + else if (inexpr is IFunApp) + { + IFunApp! funapp = (IFunApp!)inexpr; + IList newargs = null; + newargs = new ArrayList{ IExpr! arg in funapp.Arguments; Substitute(subst, var, arg) }; + result = funapp.CloneWithArguments(newargs); + } + else if (inexpr is IFunction) + { + IFunction! fun = (IFunction!)inexpr; + + if (fun.Param.Equals(var)) + result = fun; + else + result = fun.CloneWithBody(Substitute(subst, var, fun.Body)); + } + else + { + assert false; + } + + return result; + } + + + // + // Poor man's pattern matching. + // + // The methods below implement pattern matching for AI expressions. + // + // Example Usage: + // Match(e, Prop.Imp, + // (Matcher)delegate (IExpr e) { return Match(e, Prop.And, out x, out y); } + // out z) + // which sees if 'e' matches Prop.Imp(Prop.And(x,y),z) binding x,y,z to the subtrees. + // + public delegate bool Matcher(IExpr! expr); + + private static IFunApp/*?*/ MatchFunctionSymbol(IExpr! expr, IFunctionSymbol! f) + { + IFunApp app = expr as IFunApp; + if (app != null) + { + if (app.FunctionSymbol.Equals(f)) + return app; + else + return null; + } + else + return null; + } + + public static bool Match(IExpr! expr, IFunctionSymbol! f, params Matcher[]! subs) + { + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + int i = 0; // Note ***0*** + foreach (Matcher! s in subs) + { + if (!s((IExpr!)app.Arguments[i])) { return false; } + i++; + } + return true; + } + else { return false; } + } + + // Unary Binding + public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, params Matcher[]! subs) + { + arg0 = null; + + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + arg0 = (IExpr!)app.Arguments[0]; + + int i = 1; // Note ***1*** + foreach (Matcher! s in subs) + { + if (!s((IExpr!)app.Arguments[i])) { return false; } + i++; + } + return true; + } + else { return false; } + } + + // Binary Binding + public static bool Match(IExpr! expr, IFunctionSymbol! f, Matcher! sub0, out IExpr arg1, params Matcher[]! subs) + { + arg1 = null; + + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + if (!sub0((IExpr!)app.Arguments[0])) { return false; } + + arg1 = (IExpr!)app.Arguments[1]; + + int i = 2; // Note ***2*** + foreach (Matcher! s in subs) + { + if (!s((IExpr!)app.Arguments[i])) { return false; } + i++; + } + return true; + } + else { return false; } + } + + public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, out IExpr arg1, params Matcher[]! subs) + { + arg0 = null; + arg1 = null; + + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + arg0 = (IExpr!)app.Arguments[0]; + arg1 = (IExpr!)app.Arguments[1]; + + int i = 2; // Note ***2*** + foreach (Matcher! s in subs) + { + if (!s((IExpr!)app.Arguments[i])) { return false; } + i++; + } + return true; + } + else { return false; } + } + + // Ternary Binding + public static bool Match(IExpr! expr, IFunctionSymbol! f, out IExpr arg0, out IExpr arg1, out IExpr arg2, params Matcher[]! subs) + { + arg0 = null; + arg1 = null; + arg2 = null; + + IFunApp app = MatchFunctionSymbol(expr,f); + if (app != null) + { + arg0 = (IExpr!)app.Arguments[0]; + arg1 = (IExpr!)app.Arguments[1]; + arg2 = (IExpr!)app.Arguments[2]; + + int i = 3; // Note ***3*** + foreach (Matcher! s in subs) + { + if (!s((IExpr!)app.Arguments[i])) { return false; } + i++; + } + return true; + } + else { return false; } + } + + /// + /// Not intended to be instantiated. + /// + private ExprUtil() { } + } + + //------------------------------ Symbols -------------------------------- + + /// + /// An interface for function symbols. Constants are represented by + /// 0-ary function symbols. + /// + /// This interface should be implemented by abstract domains, but client + /// expressions need keep track of function symbols. + /// + public interface IFunctionSymbol + { + AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep][ResultNotNewlyAllocated] + get; } + } + + /// + /// The type of the arguments to ExprUtil.Match, a poor man's pattern + /// matching. + /// + public interface IMatchable + { + } + + //-------------------------------- Types -------------------------------- + + /// + /// Types. + /// + public interface AIType + { + } + + /// + /// Function type constructor. + /// + public sealed class FunctionType : AIType + { + /*[Own]*/ private readonly IList/**/! argTypes; + /*[Own]*/ private readonly AIType! retType; + + public FunctionType(params AIType[]! types) + requires types.Length >= 2; + { + AIType type = types[types.Length-1]; + assume type != null; + this.retType = type; + ArrayList argTypes = new ArrayList(); + for (int i = 0; i < types.Length-1; i++) + { + type = types[i]; + assume type != null; + argTypes.Add(types); + } + this.argTypes = ArrayList.ReadOnly(argTypes); + } + + public IList/**/! Arguments + { + [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep] + get + ensures result.IsReadOnly; + { + return argTypes; + } + } + + public int Arity + { + [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return argTypes.Count; } + } + + public AIType! ReturnType + { + [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return retType; } + } + + /* TODO Do we have the invariant that two functions are equal iff they're the same object. + public override bool Equals(object o) + { + if (o != null && o is FunctionType) + { + FunctionType other = (FunctionType) o; + + if (Arity == other.Arity + && ReturnType.Equals(other.ReturnType)) + { + for (int i = 0; i < Arity; i++) + { + if (!argTypes[i].Equals(other.argTypes[i])) + return false; + } + return true; + } + else + return false; + } + else + return false; + } + */ + } + + //------------------------------ Queries ------------------------------- + + public enum Answer { Yes, No, Maybe }; + + /// + /// An interface that specifies a queryable object that can answer + /// whether a predicate holds. + /// + public interface IQueryable + { + /// + /// Answers the query whether the given predicate holds. + /// + /// The given predicate. + /// Yes, No, or Maybe. + Answer CheckPredicate(IExpr! pred); + + /// + /// A simplified interface for disequalities. One can always + /// implement this by calling CheckPredicate, but it may be + /// more efficient with this method. + /// + Answer CheckVariableDisequality(IVariable! var1, IVariable! var2); + } + + public static class QueryUtil + { + public static Answer Negate(Answer ans) + { + switch (ans) + { + case Answer.Yes: + return Answer.No; + case Answer.No: + return Answer.Yes; + default: + return Answer.Maybe; + } + } + } + + //----------------------------- Exceptions ----------------------------- + + public class TypeError : CheckedException + { + } +} diff --git a/Source/AIFramework/Functional.ssc b/Source/AIFramework/Functional.ssc new file mode 100644 index 00000000..4c4a5791 --- /dev/null +++ b/Source/AIFramework/Functional.ssc @@ -0,0 +1,284 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using Microsoft.Contracts; + +namespace Microsoft.AbstractInterpretationFramework.Collections +{ + using System.Collections; + + /// Represents a functional collection of key/value pairs. + /// 2 + public interface IFunctionalMap : System.Collections.ICollection, System.Collections.IEnumerable + { + /// Adds an element with the provided key and value to the . + /// The to use as the value of the element to add. + /// The to use as the key of the element to add. + /// 2 + IFunctionalMap! Add(object! key, object value); + + /// + /// Set the value of the key (that is already in the map) + /// + IFunctionalMap! Set(object! key, object value); + + /// Determines whether the contains an element with the specified key. + /// true if the contains an element with the key; otherwise, false. + /// The key to locate in the . + /// 2 + [Pure][Reads(ReadsAttribute.Reads.Owned)] + bool Contains(object! key); + + /// Returns an for the . + /// An for the . + /// 2 + [Pure] [GlobalAccess(false)] [Escapes(true,false)] + new System.Collections.IDictionaryEnumerator GetEnumerator(); + + /// Gets an containing the keys of the . + /// An containing the keys of the . + /// 2 + System.Collections.ICollection Keys { get; } + + /// Removes the element with the specified key from the . + /// The key of the element to remove. + /// 2 + IFunctionalMap! Remove(object! key); + + /// Gets an containing the values in the . + /// An containing the values in the . + /// 2 + System.Collections.ICollection Values { get; } + + object this [object! key] { get; /*set;*/ } + } + + + + /// + /// An implementation of the + /// + /// interface with a as the backing store. + /// + class FunctionalHashtable : IFunctionalMap + { + private readonly Hashtable! h; + + /// + /// Cannot directly construct an instance of a FunctionalHashtbl. + /// + private FunctionalHashtable() + { + this.h = new Hashtable(); + // base(); + } + + /// + /// Cannot directly construct an instance of a FunctionalHashtbl. + /// + private FunctionalHashtable(Hashtable! h) + { + this.h = h; + // base(); + } + + private static readonly IFunctionalMap! empty = new FunctionalHashtable(); + public static IFunctionalMap! Empty { get { return empty; } } + + public IFunctionalMap! Add(object! key, object value) + { + Hashtable r = h.Clone() as Hashtable; + assume r != null; + r.Add(key, value); + return new FunctionalHashtable(r); + } + + public IFunctionalMap! Set(object! key, object value) + { + Hashtable r = h.Clone() as Hashtable; + + assume r != null; + assert this.Contains(key); // The entry must be defined + + r[key] = value; + return new FunctionalHashtable(r); + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public bool Contains(object! key) + { + return h.Contains(key); + } + + [Pure] [GlobalAccess(false)] [Escapes(true,false)] + IEnumerator! IEnumerable.GetEnumerator() + { + return h.GetEnumerator(); + } + + [Pure] [GlobalAccess(false)] [Escapes(true,false)] + IDictionaryEnumerator IFunctionalMap.GetEnumerator() + { + return h.GetEnumerator(); + } + + public ICollection Keys + { + get { return h.Keys; } + } + + public IFunctionalMap! Remove(object! key) + { + Hashtable r = h.Clone() as Hashtable; + assume r != null; + r.Remove(key); + return new FunctionalHashtable(r); + } + + public ICollection Values + { + get { return h.Values; } + } + + + public object this[object! key] + { + get { return h[key]; } + } + + public int Count + { + [Pure] get { return h.Count; } + } + + public bool IsSynchronized + { + [Pure] get { return h.IsSynchronized; } + } + + public object! SyncRoot + { + [Pure] get { return h.SyncRoot; } + } + + public void CopyTo(System.Array! a, int index) + { + h.CopyTo(a, index); + } + } + + public struct Pair/**/ + { + private object first; + private object second; + + public object First { get { return first; } } + public object Second { get { return second; } } + + public Pair(object first, object second) + { + this.first = first; + this.second = second; + } + + public override bool Equals(object obj) + { + if (obj == null) return false; + if (!(obj is Pair)) return false; + + Pair other = (Pair)obj; + return object.Equals(this.first, other.first) && object.Equals(this.second, other.second); + } + + public override int GetHashCode() + { + int h = this.first == null ? 0 : this.first.GetHashCode(); + h ^= this.second == null ? 0 : this.second.GetHashCode(); + return h; + } + } +} + + +namespace Microsoft.AbstractInterpretationFramework.Collections.Generic +{ + using System.Collections.Generic; + + public struct Pair + { + private T1 first; + private T2 second; + + public T1 First { get { return first; } } + public T2 Second { get { return second; } } + + public Pair(T1 first, T2 second) + { + this.first = first; + this.second = second; + } + + public override bool Equals(object obj) + { + if (obj == null) return false; + if (!(obj is Pair)) return false; + + Pair other = (Pair)obj; + return object.Equals(this.first, other.first) && object.Equals(this.second, other.second); + } + + public override int GetHashCode() + { + int h = this.first == null ? 0 : this.first.GetHashCode(); + h ^= this.second == null ? 0 : this.second.GetHashCode(); + return h; + } + + public override string! ToString() + { + return string.Format("({0},{1})", first, second); + } + } + + public struct Triple + { + private T1 first; + private T2 second; + private T3 third; + + public T1 First { get { return first; } } + public T2 Second { get { return second; } } + public T3 Third { get { return third; } } + + public Triple(T1 first, T2 second, T3 third) + { + this.first = first; + this.second = second; + this.third = third; + } + + public override bool Equals(object obj) + { + if (obj == null) return false; + if (!(obj is Triple)) return false; + + Triple other = (Triple)obj; + return object.Equals(this.first, other.first) && object.Equals(this.second, other.second) && object.Equals(this.third, other.third); + } + + public override int GetHashCode() + { + int h = this.first == null ? 0 : this.first.GetHashCode(); + h ^= this.second == null ? 0 : this.second.GetHashCode(); + h ^= this.third == null ? 0 : this.third.GetHashCode(); + return h; + } + + public override string! ToString() + { + return string.Format("({0},{1},{2})", first, second, third); + } + } +} diff --git a/Source/AIFramework/Lattice.ssc b/Source/AIFramework/Lattice.ssc new file mode 100644 index 00000000..2b606492 --- /dev/null +++ b/Source/AIFramework/Lattice.ssc @@ -0,0 +1,685 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework +{ + using Microsoft.Contracts; + using System.Collections; + using G = System.Collections.Generic; + using System.Diagnostics; + using Microsoft.AbstractInterpretationFramework.Collections; + using Microsoft.Boogie; + using IMutableSet = Microsoft.Boogie.Set; + using ISet = Microsoft.Boogie.Set; + using HashSet = Microsoft.Boogie.Set; + using ArraySet = Microsoft.Boogie.Set; + + + + /// + /// Specifies the operations (e.g., join) on a mathematical lattice that depend + /// only on the elements of the lattice. + /// + public abstract class MathematicalLattice + { + /// + /// An element of the lattice. This class should be derived from in any + /// implementation of MathematicalLattice. + /// + public abstract class Element : System.ICloneable { + /// + /// Print out a debug-useful representation of the internal data structure of the lattice element. + /// + public virtual void Dump(string! msg) { + System.Console.WriteLine("Dump({0}) = {1}", msg, this); + } + + public abstract Element! Clone(); + object! System.ICloneable.Clone() { return this.Clone(); } + + public abstract G.ICollection! FreeVariables() + ensures result.IsReadOnly; + } + + public abstract Element! Top { get; } + public abstract Element! Bottom { get; } + + public abstract bool IsTop(Element! e); + public abstract bool IsBottom(Element! e); + + /// + /// Returns true if a <= this. + /// + protected abstract bool AtMost(Element! a, Element! b) + /* The following cases are handled elsewhere and need not be considered in subclass. */ + // requires a.GetType() == b.GetType(); + // requires ! a.IsTop; + // requires ! a.IsBottom; + // requires ! b.IsTop; + // requires ! b.IsBottom; + ; + + protected Answer TrivialLowerThan(Element! a, Element! b) + { + if (a.GetType() != b.GetType()) + { + throw new System.InvalidOperationException( + "operands to <= must be of same Element type" + ); + } + if (IsBottom(a)) { return Answer.Yes; } + if (IsTop(b)) { return Answer.Yes; } + if (IsTop(a)) { return Answer.No; } + if (IsBottom(b)) { return Answer.No; } + + return Answer.Maybe; + } + + // Is 'a' better information than 'b'? + // + public bool LowerThan(Element! a, Element! b) + { + Answer ans = TrivialLowerThan(a,b); + return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, b); + } + + // Is 'a' worse information than 'b'? + // + public bool HigherThan(Element! a, Element! b) + { + return LowerThan(b, a); + } + + // Are 'a' and 'b' equivalent? + // + public bool Equivalent(Element! a, Element! b) + { + return LowerThan(a, b) && LowerThan(b, a); + } + + public abstract Element! NontrivialJoin(Element! a, Element! b) + /* The following cases are handled elsewhere and need not be considered in subclass. */ + // requires a.GetType() == b.GetType(); + // requires ! a.IsTop; + // requires ! a.IsBottom; + // requires ! b.IsTop; + // requires ! b.IsBottom; + ; + + protected Element/*?*/ TrivialJoin(Element! a, Element! b) + { + if (a.GetType() != b.GetType()) + { + throw new System.InvalidOperationException( + "operands to Join must be of same Lattice.Element type" + ); + } + if (IsTop(a)) { return a; } + if (IsTop(b)) { return b; } + if (IsBottom(a)) { return b; } + if (IsBottom(b)) { return a; } + + return null; + } + + public Element! Join(Element! a, Element! b) + { + Element/*?*/ r = TrivialJoin(a,b); + return r != null ? r : NontrivialJoin(a, b); + } + + public abstract Element! NontrivialMeet(Element! a, Element! b) + /* The following cases are handled elsewhere and need not be considered in subclass. */ + // requires a.GetType() == b.GetType(); + // requires ! a.IsTop; + // requires ! a.IsBottom; + // requires ! b.IsTop; + // requires ! b.IsBottom; + ; + + protected Element/*?*/ TrivialMeet(Element! a, Element! b) + { + if (a.GetType() != b.GetType()) + { + throw new System.InvalidOperationException( + "operands to Meet must be of same Lattice.Element type" + ); + } + if (IsTop(a)) { return b; } + if (IsTop(b)) { return a; } + if (IsBottom(a)) { return a; } + if (IsBottom(b)) { return b; } + + return null; + } + + public Element! Meet(Element! a, Element! b) + { + Element/*?*/ r = TrivialMeet(a,b); + return r != null ? r : NontrivialMeet(a, b); + } + + public abstract Element! Widen(Element! a, Element! b); + + public virtual void Validate() + { + Debug.Assert(IsTop(Top)); + Debug.Assert(IsBottom(Bottom)); + Debug.Assert(!IsBottom(Top)); + Debug.Assert(!IsTop(Bottom)); + + Debug.Assert(LowerThan(Top, Top)); + Debug.Assert(LowerThan(Bottom, Top)); + Debug.Assert(LowerThan(Bottom, Bottom)); + + Debug.Assert(IsTop(Join(Top, Top))); + Debug.Assert(IsBottom(Join(Bottom, Bottom))); + } + } + + + /// + /// Provides an abstract interface for the operations of a lattice specific + /// to abstract interpretation (i.e., that deals with the expression language). + /// + public abstract class Lattice : MathematicalLattice + { + internal readonly IValueExprFactory! valueExprFactory; + + public Lattice(IValueExprFactory! valueExprFactory) + { + this.valueExprFactory = valueExprFactory; + // base(); + } + + #region Primitives that commands translate into + + public abstract Element! Eliminate(Element! e, IVariable! variable); + + public abstract Element! Rename(Element! e, IVariable! oldName, IVariable! newName); + + public abstract Element! Constrain(Element! e, IExpr! expr); + + #endregion + + +// TODO keep this? +// public Element! Eliminate(Element! e, VariableSeq! variables) +// { +// Lattice.Element result = e; +// foreach (IVariable var in variables) +// { +// result = this.Eliminate(result, var); +// } +// return result; +// } + + + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // Note! + // + // Concrete classes that implement Lattice must implement one of the AtMost + // overloads. We provide here a default implementation for one given a "real" + // implementation of the other. Otherwise, there will be an infinite loop! + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + + protected override bool AtMost(Element! a, Element! b) + { + return AtMost(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map); + } + + protected virtual bool AtMost(Element! a, ICombineNameMap! aToResult, Element! b, ICombineNameMap! bToResult) + { + return AtMost(ApplyCombineNameMap(a,aToResult), ApplyCombineNameMap(b,bToResult)); + } + + public bool LowerThan(Element! a, ICombineNameMap! aToResult, Element! b, ICombineNameMap! bToResult) + { + Answer ans = TrivialLowerThan(a,b); + return ans != Answer.Maybe ? ans == Answer.Yes : AtMost(a, aToResult, b, bToResult); + } + + public bool HigherThan(Element! a, ICombineNameMap! aToResult, Element! b, ICombineNameMap! bToResult) + { + return LowerThan(b, bToResult, a, aToResult); + } + + + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // Note! + // + // Concrete classes that implement Lattice must implement one of the NontrivialJoin + // overloads. We provide here a default implementation for one given a "real" + // implementation of the other. Otherwise, there will be an infinite loop! + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + + public override Element! NontrivialJoin(Element! a, Element! b) + { + return NontrivialJoin(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map); + } + + public virtual Element! NontrivialJoin(Element! a, ICombineNameMap! aToResult, Element! b, ICombineNameMap! bToResult) + { + return NontrivialJoin(ApplyCombineNameMap(a,aToResult), ApplyCombineNameMap(b,bToResult)); + } + + public Element! Join(Element! a, ICombineNameMap! aToResult, Element! b, ICombineNameMap! bToResult) + { + Element/*?*/ r = TrivialJoin(a,b); + return r != null ? r : NontrivialJoin(a, aToResult, b, bToResult); + } + + + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // Note! + // + // Concrete classes that implement Lattice must implement one of the Widen + // overloads. We provide here a default implementation for one given a "real" + // implementation of the other. Otherwise, there will be an infinite loop! + //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + + public override Element! Widen(Element! a, Element! b) + { + return Widen(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map); + } + + public virtual Element! Widen(Element! a, ICombineNameMap! aToResult, Element! b, ICombineNameMap! bToResult) + { + return Widen(ApplyCombineNameMap(a,aToResult), ApplyCombineNameMap(b,bToResult)); + } + + + /// + /// Returns the predicate that corresponds to the given lattice element. + /// + public abstract IExpr! ToPredicate(Element! e); + + /// + /// Allows the lattice to specify whether it understands a particular function symbol. + /// + /// The lattice is always allowed to return "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. + /// + /// The function symbol. + /// The argument context. + /// True if it may understand f, false if it does not understand f. + public abstract bool Understands(IFunctionSymbol! f, IList/**/! args); + + /// + /// Return an expression that is equivalent to the given expression that does not + /// contain the given variable according to the lattice element and queryable. + /// + /// The lattice element. + /// A queryable for asking addtional information. + /// The expression to find an equivalent expression. + /// The variable to eliminate. + /// The set of variables that can't be used in the resulting expression. + /// + /// An equivalent expression to without + /// or null if not possible. + /// + public abstract IExpr/*?*/ EquivalentExpr(Element! e, IQueryable! q, IExpr! expr, IVariable! var, Set/**/! prohibitedVars); + + /// + /// Answers a query about whether the given predicate holds given the lattice element. + /// + /// The lattice element. + /// The predicate. + /// Yes, No, or Maybe. + public abstract Answer CheckPredicate(Element! e, IExpr! pred); + + /// + /// 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. + /// + /// The lattice element. + /// The first variable. + /// The second variable. + /// Yes, No, or Maybe. + public abstract Answer CheckVariableDisequality(Element! e, IVariable! var1, IVariable! var2); + + /// + /// A default implementation of the given + /// the appropriate expression factories by calling CheckPredicate. + /// + protected Answer DefaultCheckVariableDisequality( + IPropExprFactory! propExprFactory, IValueExprFactory! valExprFactory, + Element! e, IVariable! var1, IVariable! var2) + { + return this.CheckPredicate(e, propExprFactory.Not(valExprFactory.Eq(var1, var2))); + } + + private Element! ApplyCombineNameMap(Element! e, ICombineNameMap! eToResult) + { + Element! result = e; + + foreach (G.KeyValuePair*/!> entry in eToResult.GetSourceToResult()) + { + IVariable! sourceName = entry.Key; + ISet/**/!>! emptyDictionary1 = new G.Dictionary*/!>(); + private static readonly G.Dictionary! emptyDictionary2 = new G.Dictionary(); + + public ISet/**//*?*/ GetResultNames(IVariable! srcname) + { + ArraySet a = new ArraySet(); + a.Add(srcname); + return a; + } + + public IVariable/*?*/ GetSourceName(IVariable! resname) + { + return resname; + } + + //TODO: uncomment when works in compiler + //public G.IEnumerable*/!>> GetSourceToResult() + public IEnumerable! GetSourceToResult() + { + return emptyDictionary1; + } + + //public G.IEnumerable> GetResultToSource() + public IEnumerable! GetResultToSource() + { + return emptyDictionary2; + } + + private IdentityCombineNameMap() { } + } + + public abstract string! ToString(Element! e); // for debugging + + #region Support for MultiLattice to uniquely number every subclass of Lattice + + private static Hashtable/**/! indexMap = new Hashtable(); + private static Hashtable/**/! reverseIndexMap = new Hashtable(); + private static int globalCount = 0; + + protected virtual object! UniqueId { get { return (!)this.GetType(); } } + + public int Index + { + get + { + object unique = this.UniqueId; + if (indexMap.ContainsKey(unique)) + { + object index = indexMap[unique]; + assert index != null; // this does nothing for nonnull analysis + if (index != null) { return (int)index; } + return 0; + } + else + { + int myIndex = globalCount++; + indexMap[unique] = myIndex; + reverseIndexMap[myIndex] = this; + return myIndex; + } + } + } + + public static Lattice GetGlobalLattice(int i) { return reverseIndexMap[i] as Lattice; } + #endregion + + public static bool LogSwitch = false; + } + + + /// + /// Defines the relation between names used in the respective input lattice elements to the + /// various combination operators (Join,Widen,Meet,AtMost) and the names that should be used + /// in the resulting lattice element. + /// + public interface ICombineNameMap + { + ISet/**//*?*/ GetResultNames(IVariable! srcname); + IVariable/*?*/ GetSourceName(IVariable! resname); + + //TODO: uncommet when works in compiler + //G.IEnumerable*/!>> GetSourceToResult(); + IEnumerable! GetSourceToResult(); + //G.IEnumerable> GetResultToSource(); + IEnumerable! GetResultToSource(); + } + + /// + /// Provides statistics on the number of times an operation is performed + /// and forwards the real operations to the given lattice in the constructor. + /// + public class StatisticsLattice : Lattice + { + readonly Lattice! lattice; + int eliminateCount; + int renameCount; + int constrainCount; + int toPredicateCount; + int atMostCount; + int topCount; + int bottomCount; + int isTopCount; + int isBottomCount; + int joinCount; + int meetCount; + int widenCount; + int understandsCount; + int equivalentExprCount; + int checkPredicateCount; + int checkVariableDisequalityCount; + + public StatisticsLattice(Lattice! lattice) + : base(lattice.valueExprFactory) + { + this.lattice = lattice; + // base(lattice.valueExprFactory); + } + + public override Element! Eliminate(Element! e, IVariable! variable) + { + eliminateCount++; + return lattice.Eliminate(e, variable); + } + + public override Element! Rename(Element! e, IVariable! oldName, IVariable! newName) + { + renameCount++; + return lattice.Rename(e, oldName, newName); + } + + public override Element! Constrain(Element! e, IExpr! expr) + { + constrainCount++; + return lattice.Constrain(e, expr); + } + + + public override bool Understands(IFunctionSymbol! f, IList! args) + { + understandsCount++; + return lattice.Understands(f, args); + } + + + public override IExpr/*?*/ EquivalentExpr(Element! e, IQueryable! q, IExpr! expr, IVariable! var, ISet/**/! prohibitedVars) + { + equivalentExprCount++; + return lattice.EquivalentExpr(e, q, expr, var, prohibitedVars); + } + + + public override Answer CheckPredicate(Element! e, IExpr! pred) + { + checkPredicateCount++; + return lattice.CheckPredicate(e, pred); + } + + + public override Answer CheckVariableDisequality(Element! e, IVariable! var1, IVariable! var2) + { + checkVariableDisequalityCount++; + return lattice.CheckVariableDisequality(e, var1, var2); + } + + + + public override IExpr! ToPredicate(Element! e) + { + toPredicateCount++; + return lattice.ToPredicate(e); + } + + public override string! ToString(Element! e) + { + return lattice.ToString(e); + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override string! ToString() + { + return string.Format( + "StatisticsLattice: #Eliminate={0} #Rename={1} #Constrain={2} #ToPredicate={3} " + + "#Understands={4} #EquivalentExpr={5} #CheckPredicate={6} #CheckVariableDisequality={7} " + + "#AtMost={8} #Top={9} #Bottom={9} #IsTop={10} #IsBottom={11} " + + "#NonTrivialJoin={12} #NonTrivialMeet={13} #Widen={14}", + eliminateCount, renameCount, constrainCount, toPredicateCount, + understandsCount, equivalentExprCount, checkPredicateCount, checkVariableDisequalityCount, + atMostCount, topCount, bottomCount, isTopCount, isBottomCount, + joinCount, meetCount, widenCount); + } + + protected override bool AtMost(Element! a, Element! b) + { + atMostCount++; + return lattice.LowerThan(a, b); + } + + public override Element! Top + { + get + { + topCount++; + return lattice.Top; + } + } + public override Element! Bottom + { + get + { + bottomCount++; + return lattice.Bottom; + } + } + + public override bool IsTop(Element! e) + { + isTopCount++; + return lattice.IsTop(e); + } + + public override bool IsBottom(Element! e) + { + isBottomCount++; + return lattice.IsBottom(e); + } + + public override Element! NontrivialJoin(Element! a, Element! b) + { + joinCount++; + return lattice.NontrivialJoin(a, b); + } + + public override Element! NontrivialMeet(Element! a, Element! b) + { + meetCount++; + return lattice.NontrivialMeet(a, b); + } + + public override Element! Widen(Element! a, Element! b) + { + widenCount++; + return lattice.Widen(a, b); + } + + public override void Validate() + { + base.Validate(); + lattice.Validate(); + } + + protected override object! UniqueId + { + get + { + // use the base id, not the underlying-lattice id (is that the right thing to do?) + return base.UniqueId; + } + } + } + + + public sealed class LatticeQueryable : IQueryable + { + private Lattice! lattice; + private Lattice.Element! element; + + public LatticeQueryable(Lattice! lattice, Lattice.Element! element) + { + this.lattice = lattice; + this.element = element; + // base(); + } + + public Answer CheckPredicate(IExpr! pred) + { + return lattice.CheckPredicate(element, pred); + } + + public Answer CheckVariableDisequality(IVariable! var1, IVariable! var2) + { + return lattice.CheckVariableDisequality(element, var1, var2); + } + } +} diff --git a/Source/AIFramework/Logger.ssc b/Source/AIFramework/Logger.ssc new file mode 100644 index 00000000..12c3ba08 --- /dev/null +++ b/Source/AIFramework/Logger.ssc @@ -0,0 +1,49 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework +{ + using System; + using System.Diagnostics; + + public class Logger + { + private string! dbgmsgContext; + private static int contextWidth = 0; + + public bool Enabled = false; + + public Logger(string! contextMsg) + { + this.dbgmsgContext = "[" + contextMsg + "] "; + contextWidth = Math.Max(contextWidth, contextMsg.Length + 3); + // base(); + } + + private static System.Text.StringBuilder! dbgmsgIndent = new System.Text.StringBuilder(); + public void DbgMsgIndent() { dbgmsgIndent.Append(' ', 2); } + public void DbgMsgUnindent() + { if (dbgmsgIndent.Length >= 2) dbgmsgIndent.Remove(0,2); } + + [ConditionalAttribute("DEBUG")] + public void DbgMsg(string msg) + { + if (Enabled) + Debug.WriteLine(dbgmsgContext.PadRight(contextWidth) + dbgmsgIndent + msg); + } + [ConditionalAttribute("DEBUG")] + public void DbgMsgNoLine(string msg) + { + if (Enabled) + Debug.Write(dbgmsgContext.PadRight(contextWidth) + dbgmsgIndent + msg); + } + [ConditionalAttribute("DEBUG")] + public void DbgMsgPlain(string msg) + { + if (Enabled) + Debug.Write(msg); + } + } +} diff --git a/Source/AIFramework/MultiLattice.ssc b/Source/AIFramework/MultiLattice.ssc new file mode 100644 index 00000000..b6b6ba5e --- /dev/null +++ b/Source/AIFramework/MultiLattice.ssc @@ -0,0 +1,563 @@ +//----------------------------------------------------------------------------- +// +// 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.Collections; + + using Microsoft.Boogie; + using ISet = Microsoft.Boogie.Set; + + + /// + /// The cartesian product lattice. + /// + public class MultiLattice : Lattice, IEnumerable + { + internal class Elt : Element + { + public /*MaybeNull*/Element[] elementPerLattice; + + public Elt(int domainCount, bool isBottom) + { + this.elementPerLattice = (domainCount == 0 && isBottom) ? null : new Element[domainCount]; + } + + private Elt(Elt! other) + { + Element[] otherEPL = other.elementPerLattice; + if (otherEPL != null) + { + Element[] newEPL = new Element[otherEPL.Length]; + for (int i = 0; i < newEPL.Length; i++) + { + newEPL[i] = (Element) ((!)otherEPL[i]).Clone(); + } + this.elementPerLattice = newEPL; + } + } + + public override Element! Clone() + { + return new Elt(this); + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override string! ToString() + { +// string s = "MultiLattice+Elt{"; +// string sep = ""; +// Element[] epl = this.elementPerLattice; +// if (epl != null) +// { +// foreach (Element! e in epl) +// { +// s += sep + e.ToString(); +// sep = ", "; +// } +// } +// return s + "}"; + if (elementPerLattice == null) return ""; + System.Text.StringBuilder buffer = new System.Text.StringBuilder(); + for (int i = 0; i < this.Count; i++) + { + if (i > 0) buffer.Append("; "); + buffer.AppendFormat("{0}", elementPerLattice[i]); + } + return buffer.ToString(); + } + + public override void Dump(string! msg) { + System.Console.WriteLine("MultiLattice.Elt.Dump({0})", msg); + Element[] epl = this.elementPerLattice; + if (epl != null) { + foreach (Element! e in epl) { + e.Dump(msg); + } + } + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override ICollection! FreeVariables() + { + List! list = new List(); + for (int i = 0; i < this.Count; i++) + { + list.AddRange(((!)this[i]).FreeVariables()); + } + return (!)list.AsReadOnly(); + } + + public static Elt! Top(ArrayList/**/! lattices) + { + Elt multiValue = new Elt(lattices.Count, false); + for (int i = 0; i < lattices.Count; i++) + { + Lattice d = (Lattice!)lattices[i]; + multiValue[d.Index] = d.Top; + } + Debug.Assert(multiValue.IsValid); + return multiValue; + } + + + public static Elt! Bottom(ArrayList/**/! lattices) + { + Elt multiValue = new Elt(lattices.Count, true); + for (int i = 0; i < lattices.Count; i++) + { + Lattice d = (Lattice!)lattices[i]; + multiValue[d.Index] = d.Bottom; + } + Debug.Assert(multiValue.IsValid); + return multiValue; + } + + public bool IsValid + { + get + { + if (this.elementPerLattice == null) { return true; /*bottom*/ } + + Element[] epl = this.elementPerLattice; + for (int i = 0; i < epl.Length; i++) + { + if (epl[i] == null) { return false; } + } + return true; + } + } + + public int Count { get { return this.elementPerLattice == null ? 0 : this.elementPerLattice.Length; } } + + public bool Contains(int i) { return 0 <= i && i < this.Count; } + + public Element this[int i] // just syntactic sugar + { + get { Element[] epl = this.elementPerLattice; return epl == null ? null : epl[i]; } + set { Element[] epl = this.elementPerLattice; if (epl == null) return; epl[i] = value; } + } + + } // class + + + + ArrayList/**/! lattices = new ArrayList(); + + private readonly IPropExprFactory! propExprFactory; + + + public MultiLattice(IPropExprFactory! propExprFactory, IValueExprFactory! valueExprFactory) + : base(valueExprFactory) + { + this.propExprFactory = propExprFactory; + // base(valueExprFactory); + } + + + + public void AddLattice(Lattice lattice) { this.lattices.Add(lattice); } + + private Lattice! SubLattice(int i) { return (Lattice!)this.lattices[i]; } + + + public override Element! Top { get { return Elt.Top(this.lattices); } } + + public override Element! Bottom { get { return Elt.Bottom(this.lattices); } } + + + + + public override bool IsBottom(Element! element) + { + Elt e = (Elt)element; + // The program is errorneous/nonterminating if any subdomain knows it is. + // + if (e.elementPerLattice == null) { return true; } + for (int i = 0; i < e.Count; i++) { if (SubLattice(i).IsBottom((!)e[i])) { return true; } } + return false; + } + + public override bool IsTop(Element! element) + { + Elt e = (Elt)element; + if (e.elementPerLattice == null) { return false; } + // The multidomain knows nothing about the program only if no subdomain + // knows anything about it. + // + for (int i = 0; i < e.Count; i++) { if (!SubLattice(i).IsTop((!)e[i])) { return false; } } + return true; + } + + protected override bool AtMost(Element! first, Element! second) + { + Elt a = (Elt)first; + Elt b = (Elt)second; + + for (int i = 0; i < a.Count; i++) + { + Element thisElement = (!) a[i]; + Element thatElement = (!) b[i]; + if (thisElement.GetType() != thatElement.GetType()) + { + throw new System.InvalidOperationException( + "AtMost called on MultiDomain objects with different lattices" + ); + } + if (!SubLattice(i).LowerThan(thisElement, thatElement)) { return false; } + } + return true; + } + + protected override bool AtMost(Element! first, ICombineNameMap! firstToResult, Element! second, ICombineNameMap! secondToResult) + { + Elt a = (Elt)first; + Elt b = (Elt)second; + + for (int i = 0; i < a.Count; i++) + { + Element thisElement = (!) a[i]; + Element thatElement = (!) b[i]; + if (thisElement.GetType() != thatElement.GetType()) + { + throw new System.InvalidOperationException( + "AtMost called on MultiDomain objects with different lattices" + ); + } + if (!SubLattice(i).LowerThan(thisElement, firstToResult, thatElement, secondToResult)) { return false; } + } + return true; + } + + + private enum CombineOp { Meet, Join, Widen } + + private Element! Combine(Element! first, ICombineNameMap/*?*/ firstToResult, Element! second, ICombineNameMap/*?*/ secondToResult, CombineOp c) + { + Elt a = (Elt)first; + Elt b = (Elt)second; + + int unionCount = System.Math.Max(a.Count, b.Count); + Elt combined = new Elt(unionCount, IsBottom(a) && IsBottom(b)); + for (int i = 0; i < unionCount; i++) + { + bool thisExists = a.Contains(i); + bool thatExists = b.Contains(i); + + if (thisExists && thatExists) + { + Lattice.Element suba = a[i]; + Lattice.Element subb = b[i]; + assert suba != null && subb != null; + + switch (c) + { + case CombineOp.Meet: + combined[i] = SubLattice(i).Meet(suba, subb); + break; + case CombineOp.Join: + if (firstToResult != null && secondToResult != null) + combined[i] = SubLattice(i).Join(suba, firstToResult, subb, secondToResult); + else + combined[i] = SubLattice(i).Join(suba, subb); + break; + case CombineOp.Widen: + if (firstToResult != null && secondToResult != null) + combined[i] = SubLattice(i).Widen(suba, firstToResult, subb, secondToResult); + else + combined[i] = SubLattice(i).Widen(suba, subb); + break; + } + } + else if (thisExists) + { + combined[i] = a[i]; + } + else + { + combined[i] = b[i]; + } + } + Debug.Assert(combined.IsValid); + return combined; + } + + public override Element! NontrivialJoin(Element! a, Element! b) { return this.Combine(a, null, b, null, CombineOp.Join); } + + public override Element! NontrivialJoin(Element! a, ICombineNameMap! aToResult, Element! b, ICombineNameMap! bToResult) { return this.Combine(a, aToResult, b, bToResult, CombineOp.Join); } + + public override Element! NontrivialMeet(Element! a, Element! b) { return this.Combine(a, null, b, null, CombineOp.Meet); } + + public override Element! Widen(Element! a, Element! b) { return this.Combine(a, null, b, null, CombineOp.Widen); } + + public override Element! Widen(Element! a, ICombineNameMap! aToResult, Element! b, ICombineNameMap! bToResult) { return this.Combine(a, aToResult, b, bToResult, CombineOp.Widen); } + + public override Element! Eliminate(Element! element, IVariable! variable) + { + Elt e = (Elt)element; + if (IsBottom(e)) + { + return e; + } + Elt newValue = new Elt(e.Count, false); + for (int i = 0; i < this.lattices.Count; i++) + { + newValue[i] = SubLattice(i).Eliminate((!) e[i], variable); + } + return newValue; + } + + + public override Element! Constrain(Element! element, IExpr! expr) + { + Elt e = (Elt)element; + if (IsBottom(e)) + { + return e; + } + Elt newValue = new Elt(e.Count, false); + for (int i = 0; i < this.lattices.Count; i++) + { + newValue[i] = SubLattice(i).Constrain((!)e[i], expr); + } + return newValue; + } + + + public override Element! Rename(Element! element, IVariable! oldName, IVariable! newName) + { + Elt e = (Elt)element; + if (IsBottom(e)) + { + return e; + } + Elt newValue = new Elt(e.Count, false); + for (int i = 0; i < this.lattices.Count; i++) + { + newValue[i] = SubLattice(i).Rename((!)e[i], oldName, newName); + } + return newValue; + } + + + public override bool Understands(IFunctionSymbol! f, IList! args) + { + bool result = false; + + for (int i = 0; i < this.lattices.Count; i++) + { + result = (result || SubLattice(i).Understands(f, args)); + } + + return result; + } + + + public override string! ToString(Element! element) + { + Elt e = (Elt)element; + return e.ToString(); + } + + + public override IExpr! ToPredicate(Element! element) + { + Elt e = (Elt)element; + + IExpr result = propExprFactory.True; + for (int i = 0; i < e.Count; i++) + { + IExpr conjunct = SubLattice(i).ToPredicate((!)e[i]); + assert conjunct != null; + + result = Prop.SimplifiedAnd(propExprFactory, conjunct, result); + } + return result; + } + + /// + /// Return an expression that is equivalent to the given expression that does not + /// contain the given variable according to the lattice element and queryable. + /// + /// Simply asks each sublattice to try to generate an equivalent expression. We + /// do not try to combine information to infer new equivalences here. + /// + /// The lattice element. + /// A queryable for asking addtional information. + /// The expression to find an equivalent expression. + /// The variable to eliminate. + /// + /// An equivalent expression to without + /// or null if not possible. + /// + public override IExpr/*?*/ EquivalentExpr(Element! element, IQueryable! q, IExpr! expr, IVariable! var, Set/**/! prohibitedVars) + { + Elt! e = (Elt!)element; + + for (int i = 0; i < e.Count; i++) + { + IExpr equivexpr = SubLattice(i).EquivalentExpr((!)e[i], q, expr, var, prohibitedVars); + + if (equivexpr != null) + return equivexpr; + } + + return null; + } + + + public override Answer CheckPredicate(Element! element, IExpr! pred) + { + Elt! e = (Elt!)element; + + for (int i = 0; i < e.Count; i++) + { + Answer ans = SubLattice(i).CheckPredicate((!)e[i], pred); + + if (ans == Answer.Yes || ans == Answer.No) + return ans; + } + + return Answer.Maybe; + } + + + public override Answer CheckVariableDisequality(Element! element, IVariable! var1, IVariable! var2) + { + Elt! e = (Elt!)element; + + for (int i = 0; i < e.Count; i++) + { + Answer ans = SubLattice(i).CheckVariableDisequality((!)e[i], var1, var2); + + if (ans == Answer.Yes || ans == Answer.No) + return ans; + } + + return Answer.Maybe; + } + + + + public override void Validate() + { + base.Validate(); + foreach (Lattice! l in lattices) + { + l.Validate(); + } + } + + /// + /// The enumeration over a MultiLattice is its sublattices. + /// + /// An enumerator over the sublattices. + [Pure] [GlobalAccess(false)] [Escapes(true,false)] + public IEnumerator/**/! GetEnumerator() + { + return lattices.GetEnumerator(); + } + + /// + /// Return an enumerable over a mapping of sublattices to the their corresponding + /// lattice elements given a MultiLattice element. + /// + /// The MultiLattice element. + /// + /// An enumerable that yields an IDictionaryEnumerator over the + /// (Lattice, Lattice.Element) pairs. + /// + public IEnumerable! Subelements(Element! element) + { + return new SubelementsEnumerable(this, (Elt!) element); + } + + /// + /// An enumerator over the sublattices and elements. + /// + private sealed class SubelementsEnumerable : IEnumerable + { + private sealed class SubelementsEnumerator : IDictionaryEnumerator + { + private readonly IEnumerator/**/! multiLatticeIter; + private readonly IEnumerator/**/! multiElementIter; + + public SubelementsEnumerator(MultiLattice! multiLattice, Elt! multiElement) + requires multiElement.elementPerLattice != null; + { + this.multiLatticeIter = multiLattice.lattices.GetEnumerator(); + this.multiElementIter = multiElement.elementPerLattice.GetEnumerator(); + // base(); + } + + public DictionaryEntry Entry + { + get + { + return new DictionaryEntry((!)multiLatticeIter.Current, multiElementIter.Current); + } + } + + public object Key + { + get + { + return multiLatticeIter.Current; + } + } + + public object Value + { + get + { + return multiElementIter.Current; + } + } + + public object Current + { + [Pure][Reads(ReadsAttribute.Reads.Owned)] + get + { + return this.Entry; + } + } + + public bool MoveNext() + { + return multiLatticeIter.MoveNext() && multiElementIter.MoveNext(); + } + + public void Reset() + { + multiLatticeIter.Reset(); + multiElementIter.Reset(); + } + } + + private MultiLattice! multiLattice; + private Elt! multiElement; + + public SubelementsEnumerable(MultiLattice! multiLattice, Elt! multiElement) + { + this.multiLattice = multiLattice; + this.multiElement = multiElement; + // base(); + } + + [Pure] [GlobalAccess(false)] [Escapes(true,false)] + public IEnumerator! GetEnumerator() + { + return new SubelementsEnumerator(multiLattice, multiElement); + } + } + + + } +} diff --git a/Source/AIFramework/Mutable.ssc b/Source/AIFramework/Mutable.ssc new file mode 100644 index 00000000..894359ef --- /dev/null +++ b/Source/AIFramework/Mutable.ssc @@ -0,0 +1,117 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework.Collections +{ + using System.Collections; + using Microsoft.Contracts; + + /// + /// Extend sets for using as a IWorkList. + /// + public class WorkSet : Microsoft.Boogie.Set, Microsoft.Boogie.IWorkList + { + + // See Bug #148 for an explanation of why this is here. + // Without it, the contract inheritance rules will complain since it + // has nowhere to attach the out-of-band contract it gets from + // ICollection.Count that it gets from IWorkList. + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override int Count { get { return base.Count; } } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] public bool IsEmpty() + { + return Count == 0; + } + + /// + /// Pull an element out of the workset. + /// + public object Pull() + { + IEnumerator iter = GetEnumerator(); + iter.MoveNext(); + + object result = (!)iter.Current; + Remove(result); + + return result; + } + + bool Microsoft.Boogie.IWorkList.Add(object o){ + if (o == null) throw new System.ArgumentNullException(); + this.Add(o); + return true; + } + bool Microsoft.Boogie.IWorkList.AddAll(IEnumerable objs){ + if (objs == null) throw new System.ArgumentNullException(); + return this.AddAll(objs); + } + + // ICollection members + public void CopyTo (System.Array! a, int i) { + if (this.Count > a.Length - i) throw new System.ArgumentException(); + int j = i; + foreach(object o in this){ + a.SetValue(o, j++); + } + return; + } + object! ICollection.SyncRoot { [Pure] get { return this; } } + public bool IsSynchronized { get { return false; } } + + } +} + +namespace Microsoft.AbstractInterpretationFramework.Collections.Generic +{ + using System.Collections.Generic; + + public class HashMultiset + { + private readonly IDictionary! dict; + + //invariant forall{KeyValuePair entry in dict; entry.Value >= 1}; + + public HashMultiset() + { + this.dict = new Dictionary(); + // base(); + } + + public HashMultiset(int size) + { + this.dict = new Dictionary(size); + // base(); + } + + public void Add(T t) + { expose (this) { + if (dict.ContainsKey(t)) + { + dict[t] = dict[t] + 1; + } + else + { + dict.Add(t,1); + } + }} + + public void Remove(T t) + { + if (dict.ContainsKey(t)) + { expose (this) { + int count = dict[t]; + if (count == 1) { dict.Remove(t); } + else { dict[t] = count - 1; } + }} + } + + public bool Contains(T t) + { + return dict.ContainsKey(t); + } + } +} diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.ssc b/Source/AIFramework/Polyhedra/LinearConstraint.ssc new file mode 100644 index 00000000..9ce1552b --- /dev/null +++ b/Source/AIFramework/Polyhedra/LinearConstraint.ssc @@ -0,0 +1,588 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using Microsoft.Contracts; +namespace Microsoft.AbstractInterpretationFramework +{ + using System; + using System.Compiler; + using System.Collections; + using Microsoft.Basetypes; + using IMutableSet = Microsoft.Boogie.Set; + using HashSet = Microsoft.Boogie.Set; + using ISet = Microsoft.Boogie.Set; + + + /// + /// Represents a single linear constraint, coefficients are stored as Rationals. + /// + public class LinearConstraint + { + + public enum ConstraintRelation + { + EQ, // equal + LE, // less-than or equal + } + + public readonly ConstraintRelation Relation; + internal Hashtable /*IVariable->Rational*/! coefficients = new Hashtable /*IVariable->Rational*/ (); + internal Rational rhs; + + public LinearConstraint (ConstraintRelation rel) + { + Relation = rel; + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override string! ToString() + { + string s = null; + foreach (DictionaryEntry /*IVariable->Rational*/ entry in coefficients) + { + if (s == null) + { + s = ""; + } + else + { + s += " + "; + } + s += String.Format("{0}*{1}", entry.Value, entry.Key); + } + System.Diagnostics.Debug.Assert(s != null, "malformed LinearConstraint: no variables"); + s += String.Format(" {0} {1}", Relation == ConstraintRelation.EQ ? "==" : "<=", rhs); + return s; + } + + +#if DONT_KNOW_HOW_TO_TAKE_THE_TYPE_OF_AN_IVARIABLE_YET + public bool IsOverIntegers + { + get + { + foreach (DictionaryEntry /*IVariable->Rational*/ entry in coefficients) + { + IVariable var = (IVariable)entry.Key; + if ( ! var.TypedIdent.Type.IsInt) { return false; } + } + return true; + } + } +#endif + + + /// + /// Note: This method requires that all dimensions are of type Variable, something that's + /// not required elsewhere in this class. + /// + /// + public IExpr! ConvertToExpression(ILinearExprFactory! factory) + { + IExpr leftSum = null; + IExpr rightSum = null; + foreach (DictionaryEntry /*object->Rational*/ entry in coefficients) + { + IVariable var = (IVariable)entry.Key; + Rational coeff = (Rational) ((!)entry.Value); + if (coeff.IsPositive) + { + leftSum = AddTerm(factory, leftSum, coeff, var); + } + else if (coeff.IsNegative) + { + rightSum = AddTerm(factory, rightSum, -coeff, var); + } + else + { + // ignore the term is coeff==0 + } + } + + if (leftSum == null && rightSum == null) + { + // there are no variables in this constraint + if (Relation == ConstraintRelation.EQ ? rhs.IsZero : rhs.IsNonNegative) { + return factory.True; + } else { + return factory.False; + } + } + + if (leftSum == null || (rightSum != null && rhs.IsNegative)) + { + // show the constant on the left side + leftSum = AddTerm(factory, leftSum, -rhs, null); + } + else if (rightSum == null || rhs.IsPositive) + { + // show the constant on the right side + rightSum = AddTerm(factory, rightSum, rhs, null); + } + + assert leftSum != null; + assert rightSum != null; + return Relation == ConstraintRelation.EQ ? factory.Eq(leftSum, rightSum) : factory.AtMost(leftSum, rightSum); + } + + /// + /// Returns an expression that denotes sum + r*x. + /// If sum==null, drops the "sum +". + /// If x==null, drops the "*x". + /// if x!=null and r==1, drops the "r*". + /// + /// + /// + /// + /// + static IExpr! AddTerm(ILinearExprFactory! factory, /*MayBeNull*/ IExpr sum, Rational r, /*MayBeNull*/ IVariable x) + { + IExpr! product = factory.Term(r, x); + if (sum == null) { + return product; + } else { + return factory.Add(sum, product); + } + } + + public ISet /*IVariable!*/! GetDefinedDimensions() + { + HashSet /*IVariable!*/ dims = new HashSet /*IVariable!*/ (coefficients.Count); + int j = 0; + foreach (IVariable! dim in coefficients.Keys) + { + dims.Add(dim); + j++; + } + System.Diagnostics.Debug.Assert(j == coefficients.Count); + return dims; + } + + /// + /// Returns true iff all of the coefficients in the constraint are 0. In that + /// case, the constraint has the form 0 <= C for some constant C; hence, the + /// constraint is either unsatisfiable or trivially satisfiable. + /// + /// + public bool IsConstant() + { + foreach (Rational coeff in coefficients.Values) + { + if (coeff.IsNonZero) + { + return false; + } + } + return true; + } + + /// + /// For an equality constraint, returns 0 == rhs. + /// For an inequality constraint, returns 0 <= rhs. + /// + public bool IsConstantSatisfiable() + { + if (Relation == ConstraintRelation.EQ) + { + return rhs.IsZero; + } + else + { + return rhs.IsNonNegative; + } + } + + /// + /// Returns 0 if "this" and "c" are not equivalent constraints. If "this" and "c" + /// are equivalent constraints, the non-0 return value "m" satisfies "this == m*c". + /// + /// + /// + public Rational IsEquivalent(LinearConstraint! c) + { + // "m" is the scale factor. If it is 0, it hasn't been used yet. If it + // is non-0, it will remain that value throughout, and it then says that + // for every dimension "d", "this[d] == m * c[d]". + Rational m = Rational.ZERO; + + ArrayList /*IVariable*/ dd = new ArrayList /*IVariable*/ (); + foreach (IVariable! d in this.GetDefinedDimensions()) + { + if (!dd.Contains(d)) { dd.Add(d); } + } + foreach (IVariable! d in c.GetDefinedDimensions()) + { + if (!dd.Contains(d)) { dd.Add(d); } + } + + foreach (IVariable! d in dd) + { + Rational a = this[d]; + Rational b = c[d]; + + if (a.IsZero || b.IsZero) + { + if (a.IsNonZero || b.IsNonZero) + { + return Rational.ZERO; // not equivalent + } + } + else if (m.IsZero) + { + m = a / b; + } + else if (a != m * b) + { + return Rational.ZERO; // not equivalent + } + } + + // we expect there to have been some non-zero coefficient, so "m" should have been used by now + System.Diagnostics.Debug.Assert(m.IsNonZero); + + // finally, check the rhs + if (this.rhs == m * c.rhs) + { + return m; // equivalent + } + else + { + return Rational.ZERO; // not equivalent + } + } + + /// + /// Splits an equality constraint into two inequality constraints, the conjunction of + /// which equals the equality constraint. Assumes "this" is a equality constraint. + /// + /// + /// + public void GenerateInequalityConstraints(out LinearConstraint a, out LinearConstraint b) + { + System.Diagnostics.Debug.Assert(this.Relation == ConstraintRelation.EQ); + + a = new LinearConstraint(ConstraintRelation.LE); + a.coefficients = (Hashtable)this.coefficients.Clone(); + a.rhs = this.rhs; + + b = new LinearConstraint(ConstraintRelation.LE); + b.coefficients = new Hashtable /*IVariable->Rational*/ (); + foreach (DictionaryEntry entry in this.coefficients) + { + b.coefficients[entry.Key] = -(Rational) ((!)entry.Value); + } + b.rhs = -this.rhs; + } + + public void SetCoefficient(IVariable! dimension, Rational coefficient) + { + coefficients[dimension] = coefficient; + } + + /// + /// Removes dimension "dim" from the constraint. Only dimensions with coefficient 0 can + /// be removed. + /// + /// + public void RemoveDimension(IVariable! dim) + { + object val = coefficients[dim]; + if (val != null) + { +#if FIXED_SERIALIZER + assert ((Rational)val).IsZero; +#endif + coefficients.Remove(dim); + } + } + + /// + /// The getter returns 0 if the dimension is not present. + /// + public Rational this [IVariable! dimension] + { + get + { + object z = coefficients[dimension]; + if (z == null) + { + return Rational.ZERO; + } + else + { + return (Rational)z; + } + } + set { SetCoefficient(dimension, value); } + } + + public LinearConstraint Rename(IVariable! oldName, IVariable! newName) + { + object /*Rational*/ z = coefficients[oldName]; + if (z == null) + { + return this; + } + else + { + System.Diagnostics.Debug.Assert(z is Rational); + Hashtable /*IVariable->Rational*/ newCoeffs = (Hashtable! /*IVariable->Rational*/)coefficients.Clone(); + newCoeffs.Remove(oldName); + newCoeffs.Add(newName, z); + + LinearConstraint lc = new LinearConstraint(this.Relation); + lc.coefficients = newCoeffs; + lc.rhs = this.rhs; + return lc; + } + } + + public LinearConstraint Clone() + { + LinearConstraint z = new LinearConstraint(Relation); + z.coefficients = (Hashtable /*IVariable->Rational*/)this.coefficients.Clone(); + z.rhs = this.rhs; + return z; + } + + /// + /// Returns a constraint like "this", but with the given relation "r". + /// + /// + public LinearConstraint! ChangeRelation(ConstraintRelation rel) + { + if (Relation == rel) + { + return this; + } + else + { + LinearConstraint z = new LinearConstraint(rel); + z.coefficients = (Hashtable)this.coefficients.Clone(); + z.rhs = this.rhs; + return z; + } + } + + /// + /// Returns a constraint like "this", but, conceptually, with the inequality relation >=. + /// + /// + public LinearConstraint! ChangeRelationToAtLeast() + { + LinearConstraint z = new LinearConstraint(ConstraintRelation.LE); + foreach (DictionaryEntry /*IVariable->Rational*/ entry in this.coefficients) + { + z.coefficients.Add(entry.Key, -(Rational) ((!)entry.Value)); + } + z.rhs = -this.rhs; + return z; + } + + /// + /// Returns the left-hand side of the constraint evaluated at the point "v". + /// Any coordinate not present in "v" is treated as if it were 0. + /// Stated differently, this routine treats the left-hand side of the constraint + /// as a row vector and "v" as a column vector, and then returns the dot-product + /// of the two. + /// + /// + /// + public Rational EvaluateLhs(FrameElement! v) + { + Rational q = Rational.ZERO; + foreach (DictionaryEntry /*IVariable,Rational*/ term in coefficients) + { + IVariable dim = (IVariable!)term.Key; + Rational a = (Rational) ((!)term.Value); + Rational x = v[dim]; + q += a * x; + } + return q; + } + + /// + /// Determines whether or not a given vertex or ray saturates the constraint. + /// + /// + /// true if "fe" is a vertex; false if "fe" is a ray + /// + public bool IsSaturatedBy(FrameElement! fe, bool vertex) + { + Rational lhs = EvaluateLhs(fe); + Rational rhs = vertex ? this.rhs : Rational.ZERO; + return lhs == rhs; + } + + /// + /// Changes the current constraint A*X <= B into (A + m*aa)*X <= B + m*bb, + /// where "cc" is the constraint aa*X <= bb. + /// + /// + /// + /// + public void AddMultiple(Rational m, LinearConstraint! cc) + { + foreach (DictionaryEntry /*IVariable->Rational*/ entry in cc.coefficients) + { + IVariable dim = (IVariable)entry.Key; + Rational d = m * (Rational) ((!)entry.Value); + if (d.IsNonZero) + { + object prev = coefficients[dim]; + if (prev == null) + { + coefficients[dim] = d; + } + else + { + coefficients[dim] = (Rational)prev + d; + } + } + } + rhs += m * cc.rhs; + } + + /// + /// Try to reduce the magnitude of the coefficients used. + /// Has a side effect on the coefficients, but leaves the meaning of the linear constraint + /// unchanged. + /// + public void Normalize() { + // compute the gcd of the numerators and the gcd of the denominators + Rational gcd = rhs; + foreach (Rational r in coefficients.Values) { + gcd = Rational.Gcd(gcd, r); + } + // Change all coefficients, to divide their numerators with gcdNum and to + // divide their denominators with gcdDen. + Hashtable /*IVariable->Rational*/ newCoefficients = new Hashtable /*IVariable->Rational*/ (coefficients.Count); + foreach (DictionaryEntry /*IVarianble->Rational*/ e in coefficients) { + Rational r = (Rational) ((!)e.Value); + if (r.IsNonZero) { + newCoefficients.Add(e.Key, new Rational(r.Numerator / gcd.Numerator, r.Denominator / gcd.Denominator)); + } else { + newCoefficients.Add(e.Key, r); + } + } + + coefficients = newCoefficients; + rhs = rhs.IsNonZero ? (Rational)new Rational(rhs.Numerator / gcd.Numerator, rhs.Denominator / gcd.Denominator) : rhs; + } + } + + /// + /// Represents a frame element (vector of dimension/value tuples). Used only + /// internally in class LinearConstraintSystem and its communication with class + /// LinearConstraint. + /// + public class FrameElement + { + + Hashtable /*IVariable->Rational*/! terms = new Hashtable /*IVariable->Rational*/ (); + + /// + /// Constructs an empty FrameElement. To add dimensions, call AddCoordinate after construction. + /// + public FrameElement() + { + } + + /// + /// This method is to be thought of as being part of the FrameElement object's construction process. + /// Assumes "dimension" is not already in FrameElement. + /// + /// + /// + public void AddCoordinate(IVariable! dimension, Rational value) + { + terms.Add(dimension, value); + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override string! ToString() + { + string s = null; + foreach (DictionaryEntry item in terms) + { + if (s == null) + { + s = "("; + } + else + { + s += ", "; + } + s += String.Format("<{0},{1}>", item.Key, (Rational) ((!)item.Value)); + } + if (s == null) + { + s = "("; + } + return s + ")"; + } + + public IMutableSet /*IVariable!*/! GetDefinedDimensions() + { + HashSet /*IVariable!*/! dims = new HashSet /*IVariable!*/ (terms.Count); + foreach (IVariable! dim in terms.Keys) + { + dims.Add(dim); + } + System.Diagnostics.Debug.Assert(dims.Count == terms.Count); + return dims; + } + + /// + /// The getter returns the value at the given dimension, or 0 if that dimension is not defined. + /// + public Rational this [IVariable! dimension] + { + get + { + object z = terms[dimension]; + if (z == null) + { + return Rational.ZERO; + } + else + { + return (Rational)z; + } + } + set + { + terms[dimension] = value; + } + } + + public FrameElement Rename(IVariable! oldName, IVariable! newName) + { + object /*Rational*/ z = terms[oldName]; + if (z == null) + { + return this; + } + else + { + System.Diagnostics.Debug.Assert(z is Rational); + Hashtable /*IVariable->Rational*/ newTerms = (Hashtable! /*IVariable->Rational*/)terms.Clone(); + newTerms.Remove(oldName); + newTerms.Add(newName, z); + + FrameElement fe = new FrameElement(); + fe.terms = newTerms; + return fe; + } + } + + public FrameElement Clone() + { + FrameElement z = new FrameElement(); + z.terms = (Hashtable /*IVariable->Rational*/)this.terms.Clone(); + return z; + } + } +} diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc new file mode 100644 index 00000000..b4e33a28 --- /dev/null +++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc @@ -0,0 +1,1856 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework +{ + using System.Collections; + using System.Collections.Generic; + using System.Diagnostics; + using System; + using Microsoft.SpecSharp.Collections; + using Microsoft.Contracts; + using Microsoft.Basetypes; + using IMutableSet = Microsoft.Boogie.Set; + using HashSet = Microsoft.Boogie.Set; + using ISet = Microsoft.Boogie.Set; + + /// + /// Represents a system of linear constraints (constraint/frame representations). + /// + public class LinearConstraintSystem + { + // -------------------------------------------------------------------------------------------------------- + // ------------------ Data structure ---------------------------------------------------------------------- + // -------------------------------------------------------------------------------------------------------- + + public /*maybe null*/ ArrayList /*LinearConstraint!*/ Constraints; + /*maybe null*/ ArrayList /*FrameElement!*/ FrameVertices; + /*maybe null*/ ArrayList /*FrameElement!*/ FrameRays; + IMutableSet/*IVariable!*/! FrameDimensions; + /*maybe null*/ ArrayList /*FrameElement!*/ FrameLines; + // Invariant: Either all of Constraints, FrameVertices, FrameRays, and FrameLines are + // null, or all are non-null. + // Invariant: Any dimension mentioned in Constraints, FrameVertices, FrameRays, or + // FrameLines is mentioned in FrameDimensions. + // The meaning of FrameDimensions is that for any dimension x not in FrameDimensions, + // there is an implicit line along dimension x (that is, ()). + + void CheckInvariant() + { + if (Constraints == null) + { + System.Diagnostics.Debug.Assert(FrameVertices == null); + System.Diagnostics.Debug.Assert(FrameRays == null); + System.Diagnostics.Debug.Assert(FrameLines == null); + System.Diagnostics.Debug.Assert(FrameDimensions.Count == 0); + } + else + { + System.Diagnostics.Debug.Assert(FrameVertices != null); + System.Diagnostics.Debug.Assert(FrameRays != null); + System.Diagnostics.Debug.Assert(FrameLines != null); + + foreach (LinearConstraint! cc in Constraints) + { +#if FIXED_DESERIALIZER + assert Forall{IVariable! var in cc.GetDefinedDimensions(); FrameDimensions.Contains(var)}; +#endif + assert cc.coefficients.Count != 0; + } + foreach (ArrayList /*FrameElement*/! FrameComponent in new ArrayList /*FrameElement*/ [] {FrameVertices, FrameRays, FrameLines}) + { + foreach (FrameElement fe in FrameComponent) + { + if (fe == null) continue; +#if FIXED_DESERIALIZER + assert Forall{IVariable! var in fe.GetDefinedDimensions(); FrameDimensions.Contains(var)}; +#endif + } + } + } + } + + // -------------------------------------------------------------------------------------------------------- + // ------------------ Constructors ------------------------------------------------------------------------ + // -------------------------------------------------------------------------------------------------------- + + /// + /// Creates a LinearConstraintSystem representing the bottom element, that is, representing + /// an unsatisfiable system of constraints. + /// + [NotDelayed] + public LinearConstraintSystem() + { + FrameDimensions = new HashSet /*IVariable!*/ (); + base(); + CheckInvariant(); + } + + /// + /// Constructs a linear constraint system with constraints "cs". + /// The constructor captures all constraints in "cs". + /// + /// + [NotDelayed] + public LinearConstraintSystem(ArrayList /*LinearConstraint!*/! cs) +#if BUG_159_HAS_BEEN_FIXED + requires Forall{LinearConstraint! cc in cs; cc.coefficients.Count != 0}; +#endif + { + ArrayList constraints = new ArrayList /*LinearConstraint!*/ (cs.Count); + foreach (LinearConstraint! cc in cs) + { + constraints.Add(cc); + } + Constraints = constraints; + FrameDimensions = new HashSet /*IVariable!*/ (); // to please compiler; this value will be overridden in the call to GenerateFrameConstraints below + base(); + + GenerateFrameFromConstraints(); + SimplifyConstraints(); + CheckInvariant(); +#if DEBUG_PRINT + Console.WriteLine("LinearConstraintSystem: constructor produced:"); + Dump(); +#endif + } + + /// + /// Constructs a linear constraint system corresponding to given vertex. This constructor + /// is only used in the test harness--it is not needed for abstract interpretation. + /// + /// + [NotDelayed] + LinearConstraintSystem(FrameElement! v) + { + IMutableSet! frameDims = v.GetDefinedDimensions(); + ArrayList /*LinearConstraint!*/ constraints = new ArrayList /*LinearConstraint!*/ (); + foreach (IVariable! dim in frameDims) + { + LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ); + lc.SetCoefficient(dim, Rational.ONE); + lc.rhs = v[dim]; + constraints.Add(lc); + } + FrameDimensions = frameDims; + Constraints = constraints; + + ArrayList /*FrameElement*/ frameVertices = new ArrayList /*FrameElement*/ (); + frameVertices.Add(v); + FrameVertices = frameVertices; + + FrameRays = new ArrayList /*FrameElement*/ (); + FrameLines = new ArrayList /*FrameElement*/ (); + + base(); + CheckInvariant(); + } + + void ChangeIntoBottom() + { + Constraints = null; + FrameVertices = null; + FrameRays = null; + FrameLines = null; + IMutableSet ss; + FrameDimensions.Clear(); // no implicit lines + } + + // -------------------------------------------------------------------------------------------------------- + // ------------------ Public operations and their support routines ---------------------------------------- + // -------------------------------------------------------------------------------------------------------- + + public bool IsBottom() + { + return Constraints == null; + } + + public bool IsTop() + { + return Constraints != null && Constraints.Count == 0; + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override string! ToString() + { + if (Constraints == null) + { + return ""; + } + else if (Constraints.Count == 0) + { + return ""; + } + else + { + string z = null; + foreach (LinearConstraint! lc in Constraints) + { + string s = lc.ToString(); + if (z == null) + { + z = s; + } + else + { + z += " AND " + s; + } + } + assert z != null; + return z; + } + } + + + public ICollection! FreeVariables() + ensures result.IsReadOnly; + { + List list = new List(); + foreach (IVariable! v in FrameDimensions) { list.Add(v); } + return (!)list.AsReadOnly(); + } + + /// + /// Note: This method requires that all dimensions are of type Variable, something that's + /// not required elsewhere in this class. + /// + /// + public IExpr! ConvertToExpression(ILinearExprFactory! factory) + { + if (this.Constraints == null) { + return factory.False; + } + if (this.Constraints.Count == 0) { + return factory.True; + } + + IExpr result = null; + foreach (LinearConstraint! lc in Constraints) + { + IExpr conjunct = lc.ConvertToExpression(factory); + result = (result == null) ? conjunct : (IExpr)factory.And(conjunct, result); + } + assert result != null; + return result; + } + + + /* IsSubset(): determines if 'lcs' is a subset of 'this' + * -- See Cousot/Halbwachs 1978, section + */ + public bool IsSubset(LinearConstraintSystem! lcs) + { + if (lcs.IsBottom()) + { + return true; + } + else if (this.IsBottom()) + { + return false; +#if DEBUG +#else + } else if (this.IsTop()) { // optimization -- this case not needed for correctness + return true; + } else if (lcs.IsTop()) { // optimization -- this case not needed for correctness + return false; +#endif + } + else + { + // phase 0: check if frame dimensions are a superset of the constraint dimensions + ISet /*IVariable!*/! frameDims = lcs.GetDefinedDimensions(); +#if DEBUG_PRINT + Console.WriteLine("DEBUG: IsSubset:"); + Console.WriteLine(" --- this:"); + this.Dump(); + Console.WriteLine(" --- lcs:"); + lcs.Dump(); + Console.WriteLine(" ---"); +#endif + foreach (LinearConstraint! cc in (!)this.Constraints) + { +#if DEBUG_PRINT + Console.WriteLine(" cc: {0}", cc); + Console.WriteLine(" cc.GetDefinedDimensions(): {0}", cc.GetDefinedDimensions()); +#endif + if (!forall{IVariable! var in cc.GetDefinedDimensions(); frameDims.Contains(var)}) + { +#if DEBUG_PRINT + Console.WriteLine(" ---> phase 0 subset violated, return false from IsSubset"); +#endif + return false; + } + } + } + + // phase 1: check frame vertices against each constraint... + foreach (FrameElement! v in (!)lcs.FrameVertices) + { + foreach (LinearConstraint! cc in this.Constraints) + { + Rational q = cc.EvaluateLhs(v); + if (cc.Relation == LinearConstraint.ConstraintRelation.LE) + { + if (!(q <= cc.rhs)) + { +#if DEBUG_PRINT + Console.WriteLine(" ---> phase 1a subset violated, return false from IsSubset"); +#endif + return false; + } + } + else + { + if (!(q == cc.rhs)) + { +#if DEBUG_PRINT + Console.WriteLine(" ---> phase 1b subset violated, return false from IsSubset"); +#endif + return false; + } + } + } + } + + // phase 2: check frame rays against each constraint... + // To check if a ray "r" falls within a constraint "cc", we add the vector "r" to + // any point "p" on the side of the half-space or plane described by constraint, and + // then check if the resulting point satisfies the constraint. That is, we check (for + // an inequality constraint with coefficients a1,a2,...,an and right-hand side + // constant C): + // a1*(r1+p1) + a2*(r2+p2) + ... + an*(rn+pn) <= C + // Equivalently: + // a1*r1 + a2*r2 + ... + an*rn + a1*p1 + a2*p2 + ... + an*pn <= C + // To find a point "p", we can pick out a coordinate, call it 1, with a non-zero + // coefficient in the constraint, and then choose "p" as the point that has the + // value C/a1 in coordinate 1 and has 0 in all other coordinates. We then check: + // a1*r1 + a2*r2 + ... + an*rn + a1*(C/a1) + a2*0 + ... + an*0 <= C + // which simplifies to: + // a1*r1 + a2*r2 + ... + an*rn + C <= C + // which in turn simplifies to: + // a1*r1 + a2*r2 + ... + an*rn <= 0 + // If the constraint is an equality constraint, we simply replace "<=" with "==" + // above. + foreach (FrameElement! r in (!)lcs.FrameRays) + { + System.Diagnostics.Debug.Assert(r != null, "encountered a null ray..."); + foreach (LinearConstraint! cc in this.Constraints) + { + System.Diagnostics.Debug.Assert(cc != null, "encountered an null constraint..."); + Rational q = cc.EvaluateLhs(r); + if (cc.Relation == LinearConstraint.ConstraintRelation.LE) + { + if (q.IsPositive) + { +#if DEBUG_PRINT + Console.WriteLine(" ---> phase 2a subset violated, return false from IsSubset"); +#endif + return false; + } + } + else + { + if (q.IsNonZero) + { +#if DEBUG_PRINT + Console.WriteLine(" ---> phase 2b subset violated, return false from IsSubset"); +#endif + return false; + } + } + } + } + + // phase 3: check frame lines against each constraint... + // To check if a line "L" falls within a constraint "cc", we check if both the + // vector "L" and "-L", interpreted as rays, fall within the constraint. From + // the discussion above, this means we check the following two properties: + // a1*L1 + a2*L2 + ... + an*Ln <= 0 (*) + // a1*(-L1) + a2*(-L2) + ... + an*(-Ln) <= 0 + // The second of these lines can be rewritten as: + // - a1*L1 - a2*L2 - ... - an*Ln <= 0 + // which is equivalent to: + // -1 * (a1*L1 + a2*L2 + ... + an*Ln) <= 0 + // Multiplying both sides by -1 and flipping the direction of the inequality, + // we have: + // a1*L1 + a2*L2 + ... + an*Ln >= 0 (**) + // Putting (*) and (**) together, we conclude that we need to check: + // a1*L1 + a2*L2 + ... + an*Ln == 0 + // If the constraint is an equality constraint, we end up with the same equation. + foreach (FrameElement! line in (!)lcs.FrameLines) + { + System.Diagnostics.Debug.Assert(line != null, "encountered a null line..."); + foreach (LinearConstraint! cc in this.Constraints) + { + System.Diagnostics.Debug.Assert(cc != null, "encountered an null constraint..."); + Rational q = cc.EvaluateLhs(line); + if (q.IsNonZero) + { +#if DEBUG_PRINT + Console.WriteLine(" ---> phase 3 subset violated, return false from IsSubset"); +#endif + return false; + } + } + } + +#if DEBUG_PRINT + Console.WriteLine(" ---> IsSubset returns true"); +#endif + return true; + } + + public LinearConstraintSystem! Meet(LinearConstraintSystem! lcs) + requires this.Constraints != null; + requires lcs.Constraints != null; + { + ArrayList /*LinearConstraint*/ clist = new ArrayList(this.Constraints.Count + lcs.Constraints.Count); + clist.AddRange(this.Constraints); + clist.AddRange(lcs.Constraints); + return new LinearConstraintSystem(clist); + } + +#if DEBUG_PRINT + public LinearConstraintSystem Join(LinearConstraintSystem lcs) + { + Console.WriteLine("==================================================================================="); + Console.WriteLine("DEBUG: Join"); + Console.WriteLine("Join: this="); + Dump(); + Console.WriteLine("Join: lcs="); + lcs.Dump(); + LinearConstraintSystem z = JoinX(lcs); + Console.WriteLine("----------Join------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"); + Console.WriteLine("Join: result="); + z.Dump(); + Console.WriteLine("==================================================================================="); + return z; + } +#endif + + /// + /// The join is computed as described in section 4.4 in Cousot and Halbwachs. + /// + /// + /// +#if DEBUG_PRINT + public LinearConstraintSystem JoinX(LinearConstraintSystem lcs) +#else + public LinearConstraintSystem! Join(LinearConstraintSystem! lcs) +#endif + { + if (this.IsBottom()) + { + return (!) lcs.Clone(); + } + else if (lcs.IsBottom()) + { + return (!) this.Clone(); + } + else if (this.IsTop() || lcs.IsTop()) + { + return new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ()); + } + else + { + LinearConstraintSystem! z; + // Start from the "larger" of the two frames (this is just a heuristic measure intended + // to save work). + assume this.FrameVertices != null; + assume this.FrameRays != null; + assume this.FrameLines != null; + assume lcs.FrameVertices != null; + assume lcs.FrameRays != null; + assume lcs.FrameLines != null; + if (this.FrameVertices.Count + this.FrameRays.Count + this.FrameLines.Count - this.FrameDimensions.Count < + lcs.FrameVertices.Count + lcs.FrameRays.Count + lcs.FrameLines.Count - lcs.FrameDimensions.Count) + { + z = (!) lcs.Clone(); + lcs = this; + } + else + { + z = (!) this.Clone(); + } +#if DEBUG_PRINT + Console.WriteLine("DEBUG: LinearConstraintSystem.Join ---------------"); + Console.WriteLine("z:"); + z.Dump(); + Console.WriteLine("lcs:"); + lcs.Dump(); +#endif + + // Start by explicating the implicit lines of z for the dimensions dims(lcs)-dims(z). + foreach (IVariable! dim in lcs.FrameDimensions) + { + if (!z.FrameDimensions.Contains(dim)) + { + z.FrameDimensions.Add(dim); + FrameElement line = new FrameElement(); + line.AddCoordinate(dim, Rational.ONE); + // Note: AddLine is not called (because the line already exists in z--it's just that + // it was represented implicitly). Instead, just tack the explicit representation onto + // FrameLines. + assume z.FrameLines != null; + z.FrameLines.Add(line); +#if DEBUG_PRINT + Console.WriteLine("Join: After explicating line: {0}", line); + z.Dump(); +#endif + } + } + + // Now, the vertices, rays, and lines can be added. + foreach (FrameElement! v in lcs.FrameVertices) + { + z.AddVertex(v); +#if DEBUG_PRINT + Console.WriteLine("Join: After adding vertex: {0}", v); + z.Dump(); +#endif + } + foreach (FrameElement! r in lcs.FrameRays) + { + z.AddRay(r); +#if DEBUG_PRINT + Console.WriteLine("Join: After adding ray: {0}", r); + z.Dump(); +#endif + } + foreach (FrameElement! l in lcs.FrameLines) + { + z.AddLine(l); +#if DEBUG_PRINT + Console.WriteLine("Join: After adding line: {0}", l); + z.Dump(); +#endif + } + // also add to z the implicit lines of lcs + foreach (IVariable! dim in z.FrameDimensions) + { + if (!lcs.FrameDimensions.Contains(dim)) + { + // "dim" is a dimension that's explicit in "z" but implicit in "lcs" + FrameElement line = new FrameElement(); + line.AddCoordinate(dim, Rational.ONE); + z.AddLine(line); +#if DEBUG_PRINT + Console.WriteLine("Join: After adding lcs's implicit line: {0}", line); + z.Dump(); +#endif + } + } + + z.SimplifyFrame(); + z.SimplifyConstraints(); + z.CheckInvariant(); +#if DEBUG_PRINT + Console.WriteLine("Join: Returning z:"); + z.Dump(); + Console.WriteLine("----------------------------------------"); +#endif + return z; + } + } + +#if DEBUG_PRINT + public LinearConstraintSystem Widen(LinearConstraintSystem lcs) + { + Console.WriteLine("==================================================================================="); + Console.WriteLine("DEBUG: Widen"); + Console.WriteLine("Widen: this="); + Dump(); + Console.WriteLine("Widen: lcs="); + lcs.Dump(); + LinearConstraintSystem z = WidenX(lcs); + Console.WriteLine("----------Widen------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"); + Console.WriteLine("Widen: result="); + z.Dump(); + Console.WriteLine("==================================================================================="); + return z; + } +#endif + +#if DEBUG_PRINT + public LinearConstraintSystem WidenX(LinearConstraintSystem lcs) +#else + public LinearConstraintSystem! Widen(LinearConstraintSystem! lcs) +#endif + { + if (this.IsBottom()) + { + return (!) lcs.Clone(); + } + else if (lcs.IsBottom()) + { + return (!) this.Clone(); + } + else if (this.IsTop() || lcs.IsTop()) + { + return new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ()); + } + + // create new LCS, we will add only verified constraints to this... + ArrayList /*LinearConstraint*/ newConstraints = new ArrayList /*LinearConstraint*/ (); + assume this.Constraints != null; + foreach (LinearConstraint! ccX in this.Constraints) + { + LinearConstraint cc = ccX; +#if DEBUG_PRINT + Console.WriteLine("Widen checking: Starting to check constraint: {0}", cc); +#endif + if (cc.IsConstant()) + { + // (Can this ever occur in the stable state of a LinearConstraintSystem? --KRML) + // constraint is unaffected by the frame components +#if DEBUG_PRINT + Console.WriteLine("Widen checking: --Adding it!"); +#endif + newConstraints.Add(cc); + continue; + } + + // PHASE I: verify constraints against all frame vertices... + + foreach (FrameElement! vertex in (!)lcs.FrameVertices) + { + Rational lhs = cc.EvaluateLhs(vertex); + if (lhs > cc.rhs) + { + // the vertex does not satisfy the inequality <= + if (cc.Relation == LinearConstraint.ConstraintRelation.LE) + { +#if DEBUG_PRINT + Console.WriteLine("Widen checking: throwing out because of vertex: {0}", vertex); +#endif + goto CHECK_NEXT_CONSTRAINT; + } + else + { + // ... but it does satisfy the inequality >= +#if DEBUG_PRINT + Console.WriteLine("Widen checking: throwing out <= because of vertex: {0}", vertex); +#endif + cc = cc.ChangeRelationToAtLeast(); +#if DEBUG_PRINT + Console.WriteLine("Widen checking: left with constraint: {0}", cc); +#endif + } + } + else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs < cc.rhs) + { + // the vertex does not satisfy the inequality >=, and the constraint is an equality constraint +#if DEBUG_PRINT + Console.WriteLine("Widen checking: throwing out >= because of vertex: {0}", vertex); +#endif + cc = cc.ChangeRelation(LinearConstraint.ConstraintRelation.LE); +#if DEBUG_PRINT + Console.WriteLine("Widen checking: left with contraint: {0}", cc); +#endif + } + } + + // PHASE II: verify constraints against all frame rays... + + foreach (FrameElement! ray in (!)lcs.FrameRays) + { + // The following assumes the constraint to have some dimension with a non-zero coefficient + Rational lhs = cc.EvaluateLhs(ray); + if (lhs.IsPositive) + { + // the ray does not satisfy the inequality <= + if (cc.Relation == LinearConstraint.ConstraintRelation.LE) + { +#if DEBUG_PRINT + Console.WriteLine("Widen checking: throwing out because of ray: {0}", ray); +#endif + goto CHECK_NEXT_CONSTRAINT; + } + else + { + // ... but it does satisfy the inequality >= +#if DEBUG_PRINT + Console.WriteLine("Widen checking: throwing out <= because of ray: {0}", ray); +#endif + cc = cc.ChangeRelationToAtLeast(); +#if DEBUG_PRINT + Console.WriteLine("Widen checking: left with contraint: {0}", cc); +#endif + } + } + else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs.IsNegative) + { + // the ray does not satisfy the inequality >=, and the constraint is an equality constraint +#if DEBUG_PRINT + Console.WriteLine("Widen checking: throwing out >= because of ray: {0}", ray); +#endif + cc = cc.ChangeRelation(LinearConstraint.ConstraintRelation.LE); +#if DEBUG_PRINT + Console.WriteLine("Widen checking: left with constraint: {0}", cc); +#endif + } + } + + // PHASE III: verify constraints against all frame lines... + + foreach (FrameElement! line in (!)lcs.FrameLines) + { + // The following assumes the constraint to have some dimension with a non-zero coefficient + Rational lhs = cc.EvaluateLhs(line); + if (!lhs.IsZero) + { + // The line satisfies neither the inequality <= nor the equality == +#if DEBUG_PRINT + Console.WriteLine("Widen checking: throwing out because of line: {0}", line); +#endif + goto CHECK_NEXT_CONSTRAINT; + } + } + + // constraint has been verified, so add to new constraint system +#if DEBUG_PRINT + Console.WriteLine("Widen checking: --Adding it!"); +#endif + newConstraints.Add(cc); + + CHECK_NEXT_CONSTRAINT: {} +#if DEBUG_PRINT + Console.WriteLine("Widen checking: done with that constraint"); +#endif + } + + return new LinearConstraintSystem(newConstraints); + } + +#if DEBUG_PRINT + public LinearConstraintSystem Project(IVariable! dim) + { + Console.WriteLine("==================================================================================="); + Console.WriteLine("DEBUG: Project(dim={0})", dim); + Console.WriteLine("Project: this="); + Dump(); + LinearConstraintSystem z = ProjectX(dim); + Console.WriteLine("----------Project------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"); + Console.WriteLine("Project: result="); + z.Dump(); + Console.WriteLine("==================================================================================="); + return z; + } +#endif + +#if DEBUG_PRINT + public LinearConstraintSystem ProjectX(IVariable! dim) +#else + public LinearConstraintSystem! Project(IVariable! dim) +#endif + requires this.Constraints != null; + { + ArrayList /*LinearConstraint!*/! cc = Project(dim, Constraints); + return new LinearConstraintSystem(cc); + } + +#if DEBUG_PRINT + public LinearConstraintSystem Rename(IVariable! oldName, IVariable! newName) + { + Console.WriteLine("==================================================================================="); + Console.WriteLine("DEBUG: Rename(oldName={0}, newName={1})", oldName, newName); + Console.WriteLine("Rename: this="); + Dump(); + LinearConstraintSystem z = RenameX(oldName, newName); + Console.WriteLine("----------Rename------------------------------>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"); + Console.WriteLine("Rename: result="); + z.Dump(); + Console.WriteLine("==================================================================================="); + return z; + } +#endif + +#if DEBUG_PRINT + public LinearConstraintSystem RenameX(IVariable! oldName, IVariable! newName) +#else + public LinearConstraintSystem! Rename(IVariable! oldName, IVariable! newName) +#endif + { + if (this.Constraints == null) + { + System.Diagnostics.Debug.Assert(this.FrameVertices == null); + System.Diagnostics.Debug.Assert(this.FrameRays == null); + System.Diagnostics.Debug.Assert(this.FrameLines == null); + return this; + } + IMutableSet /*IVariable!*/! dims = this.FrameDimensions; + if (!dims.Contains(oldName)) + { + return this; + } + + LinearConstraintSystem z = new LinearConstraintSystem(); + z.FrameDimensions = (HashSet! /*IVariable!*/)dims.Clone(); + z.FrameDimensions.Remove(oldName); + z.FrameDimensions.Add(newName); + + z.Constraints = new ArrayList /*LinearConstraint!*/ (this.Constraints.Count); + foreach (LinearConstraint! lc in (!)this.Constraints) + { + z.Constraints.Add(lc.Rename(oldName, newName)); + } + z.FrameVertices = RenameInFE((!)this.FrameVertices, oldName, newName); + z.FrameRays = RenameInFE((!)this.FrameRays, oldName, newName); + z.FrameLines = RenameInFE((!)this.FrameLines, oldName, newName); + return z; + } + + static ArrayList /*FrameElement*/ RenameInFE(ArrayList! /*FrameElement*/ list, IVariable! oldName, IVariable! newName) + { + ArrayList/*FrameElement!*/! z = new ArrayList/*FrameElement!*/ (list.Count); + foreach (FrameElement! fe in list) + { + z.Add(fe.Rename(oldName, newName)); + } + System.Diagnostics.Debug.Assert(z.Count == list.Count); + return z; + } + + // -------------------------------------------------------------------------------------------------------- + // ------------------ support routines -------------------------------------------------------------------- + // -------------------------------------------------------------------------------------------------------- + + /// + /// Returns a set of constraints that is the given set of constraints with dimension "dim" + /// projected out. See Cousot and Halbwachs, section 3.3.1.1. + /// + /// + /// + /// + static ArrayList /*LinearConstraint!*/! Project(IVariable! dim, ArrayList /*LinearConstraint!*/! constraints) + { + // Sort the inequality constaints into ones where dimension "dim" is 0, negative, and + // positive, respectively. Put equality constraints with a non-0 "dim" into "eq". + ArrayList /*LinearConstraint!*/! final = new ArrayList /*LinearConstraint!*/ (); + ArrayList /*LinearConstraint!*/! negative = new ArrayList /*LinearConstraint!*/ (); + ArrayList /*LinearConstraint!*/! positive = new ArrayList /*LinearConstraint!*/ (); + ArrayList /*LinearConstraint!*/! eq = new ArrayList /*LinearConstraint!*/ (); + foreach (LinearConstraint! cc in constraints) + { + Rational coeff = cc[dim]; + if (coeff.IsZero) + { + LinearConstraint lc = (!) cc.Clone(); + if (!lc.IsConstant()) + { + lc.RemoveDimension(dim); + final.Add(lc); + } + } + else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ) + { + eq.Add(cc); + } + else if (coeff.IsNegative) + { + negative.Add(cc); + } + else + { + System.Diagnostics.Debug.Assert(coeff.IsPositive); + positive.Add(cc); + } + } + + if (eq.Count != 0) + { + LinearConstraint eqConstraint = (LinearConstraint!)eq[eq.Count-1]; + eq.RemoveAt(eq.Count-1); + Rational eqC = -eqConstraint[dim]; + + foreach (ArrayList /*LinearConstraint!*/! list in new ArrayList[]{eq, negative, positive}) + { + foreach (LinearConstraint! lcX in list) + { + LinearConstraint lc = (!) lcX.Clone(); + lc.AddMultiple(lc[dim]/eqC, eqConstraint); + System.Diagnostics.Debug.Assert(lc[dim].IsZero); + if (!lc.IsConstant()) + { + lc.RemoveDimension(dim); + final.Add(lc); + } + else + { + System.Diagnostics.Debug.Assert(lc.IsConstantSatisfiable()); + } + } + } + } + else + { + // Consider all pairs of constraints with (negative,positive) coefficients of "dim". + foreach (LinearConstraint! cn in negative) + { + Rational dn = -cn[dim]; + System.Diagnostics.Debug.Assert(dn.IsNonNegative); + foreach (LinearConstraint! cp in positive) + { + Rational dp = cp[dim]; + + LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.LE); + lc.AddMultiple(dn, cp); + lc.AddMultiple(dp, cn); + System.Diagnostics.Debug.Assert(lc[dim].IsZero); + if (!lc.IsConstant()) + { + lc.RemoveDimension(dim); + final.Add(lc); + } + else + { + System.Diagnostics.Debug.Assert(lc.IsConstantSatisfiable()); + } + } + } + } + + return final; + } + + /// + /// Initializes FrameVertices, FrameRays, FrameLines, and FrameDimensions, see + /// Cousot and Halbwachs, section 3.4. Any previous values of these fields are + /// ignored and overwritten. + /// + /// If the set of Constraints is unsatisfiable, then "this" is changed into Bottom. + /// + void GenerateFrameFromConstraints() + { + if (Constraints == null) + { + FrameVertices = null; + FrameRays = null; + FrameLines = null; + FrameDimensions = new HashSet /*IVariable!*/ (); + return; + } + + // Step 1 (see Cousot and Halbwachs, section 3.4.3): create a Simplex Tableau. +#if DEBUG_PRINT + Console.WriteLine("DEBUG: --- GenerateFrameFromConstraint ---"); + Console.WriteLine("Constraints:"); + foreach (LinearConstraint cc in Constraints) + { + Console.WriteLine(" {0}", cc); + } +#endif + SimplexTableau tableau = new SimplexTableau(Constraints); +#if DEBUG_PRINT + Console.WriteLine("Initial tableau:"); + tableau.Dump(); +#endif + FrameDimensions = tableau.GetDimensions(); +#if DEBUG_PRINT + Console.WriteLine("Dimensions:"); + foreach (object dim in FrameDimensions) + { + Console.Write(" {0}", dim); + } + Console.WriteLine(); +#endif + + // Step 3 and 2: Put as many initial variables as possible into basis, then check if + // we reached a feasible basis + tableau.AddInitialVarsToBasis(); +#if DEBUG_PRINT + Console.WriteLine("Tableau after Step 3:"); + tableau.Dump(); +#endif + if (!tableau.IsFeasibleBasis) + { + // The polyhedron is empty (according to Cousot and Halbwachs) + ChangeIntoBottom(); + return; + } + + FrameVertices = new ArrayList /*FrameElement*/ (); + FrameRays = new ArrayList /*FrameElement*/ (); + FrameLines = new ArrayList /*FrameElement*/ (); + if (FrameDimensions.Count == 0) + { + // top element + return; + } + + if (tableau.AllInitialVarsInBasis) + { + // All initial variables are in basis; there are no lines. +#if DEBUG_PRINT + Console.WriteLine("Tableau after Steps 2 and 3 (all initial variables in basis):"); + tableau.Dump(); +#endif + } + else + { + // There are lines +#if DEBUG_PRINT + Console.WriteLine("Tableau after Steps 2 and 3 (NOT all initial variables in basis--there are lines):"); + tableau.Dump(); +#endif + // Step 4.2: Pick out the lines, then produce the tableau for a new polyhedron without those lines. + ArrayList /*LinearConstraint*/ moreConstraints = (ArrayList! /*LinearConstraint*/) Constraints.Clone(); + tableau.ProduceLines(FrameLines, moreConstraints); + tableau = new SimplexTableau(moreConstraints); +#if DEBUG_PRINT + Console.WriteLine("Lines produced:"); + foreach (FrameElement line in FrameLines) + { + Console.WriteLine(" {0}", line); + } + Console.WriteLine("The new list of constraints is:"); + foreach (LinearConstraint c in moreConstraints) + { + Console.WriteLine(" {0}", c); + } + Console.WriteLine("Tableau after producing lines in Step 4.2:"); + tableau.Dump(); +#endif + + // Repeat step 3 for the new tableau. + // Since the new tableau contains no lines, the following call should cause all initial + // variables to be in basis (see step 4.2 in section 3.4.3 of Cousot and Halbwachs). + tableau.AddInitialVarsToBasis(); + System.Diagnostics.Debug.Assert(tableau.AllInitialVarsInBasis); + System.Diagnostics.Debug.Assert(tableau.IsFeasibleBasis); // the new tableau represents a set of feasible constraints, so this basis should be found to be feasible +#if DEBUG_PRINT + Console.WriteLine("Tableau after all initial variables have been moved into basis:"); + tableau.Dump(); +#endif + } + + // Step 4.1: One vertex has been found. Find all others, too. + tableau.TraverseVertices(FrameVertices, FrameRays); +#if DEBUG_PRINT + Console.WriteLine("Tableau after vertex traversal:"); + tableau.Dump(); +#endif + } + + class LambdaDimension : IVariable + { + readonly int id; + static int count = 0; + + /// + /// Return the name of the variable + /// + public string! Name + { + get + { + return this.ToString(); + } + } + + public LambdaDimension() + { + id = count; + count++; + } + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override string! ToString() + { + return "lambda" + id; + } + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public object DoVisit(ExprVisitor! visitor) + { + return visitor.VisitVariable(this); + } + } + + /// + /// Adds a vertex to the frame of "this" and updates Constraints accordingly, see + /// Cousot and Halbwachs, section 3.3.1.1. However, this method does not simplify + /// Constraints after the operation; that remains the caller's responsibility (which + /// gives the caller the opportunity to make multiple calls to AddVertex, AddRay, + /// and AddLine before calling SimplifyConstraints). + /// Assumes Constraints (and the frame fields) to be non-null. + /// + /// + void AddVertex(FrameElement! vertex) + requires this.FrameVertices != null; + { +#if DEBUG_PRINT + Console.WriteLine("DEBUG: AddVertex called on {0}", vertex); + Console.WriteLine(" Initial constraints:"); + foreach (LinearConstraint cc in Constraints) { + Console.WriteLine(" {0}", cc); + } +#endif + + FrameVertices.Add(vertex.Clone()); +#if FIXED_DESERIALIZER + assert Forall{IVariable! var in vertex.GetDefinedDimensions(); FrameDimensions.Contains(var)}; +#endif + + // We use a new temporary dimension. + IVariable! lambda = new LambdaDimension(); + + // We change the constraints A*X <= B into + // A*X + (A*vector - B)*lambda <= A*vector. + // That means that each row k in A (which corresponds to one LinearConstraint + // in Constraints) is changed by adding + // (A*vector - B)[k] * lambda + // to row k and changing the right-hand side of row k to + // (A*vector)[k] + // Note: + // (A*vector - B)[k] + // = { vector subtraction is pointwise } + // (A*vector)[k] - B[k] + // = { A*vector is a row vector whose every row i is the dot-product of + // row i of A with the column vector "vector" } + // A[k]*vector - B[k] + foreach (LinearConstraint! cc in (!)Constraints) + { + Rational d = cc.EvaluateLhs(vertex); + cc.SetCoefficient(lambda, d - cc.rhs); + cc.rhs = d; + } + + // We also add the constraints that lambda lies between 0 ... + LinearConstraint la = new LinearConstraint(LinearConstraint.ConstraintRelation.LE); + la.SetCoefficient(lambda, Rational.MINUS_ONE); + la.rhs = Rational.ZERO; + Constraints.Add(la); + // ... and 1. + la = new LinearConstraint(LinearConstraint.ConstraintRelation.LE); + la.SetCoefficient(lambda, Rational.ONE); + la.rhs = Rational.ONE; + Constraints.Add(la); +#if DEBUG_PRINT + Console.WriteLine(" Constraints after addition:"); + foreach (LinearConstraint cc in Constraints) { + Console.WriteLine(" {0}", cc); + } +#endif + + // Finally, project out the dummy dimension. + Constraints = Project(lambda, Constraints); + +#if DEBUG_PRINT + Console.WriteLine(" Resulting constraints:"); + foreach (LinearConstraint cc in Constraints) { + Console.WriteLine(" {0}", cc); + } +#endif + } + + /// + /// Adds a ray to the frame of "this" and updates Constraints accordingly, see + /// Cousot and Halbwachs, section 3.3.1.1. However, this method does not simplify + /// Constraints after the operation; that remains the caller's responsibility (which + /// gives the caller the opportunity to make multiple calls to AddVertex, AddRay, + /// and AddLine before calling SimplifyConstraints). + /// Assumes Constraints (and the frame fields) to be non-null. + /// + /// + void AddRay(FrameElement! ray) + requires this.FrameRays != null; + { +#if DEBUG_PRINT + Console.WriteLine("DEBUG: AddRay called on {0}", ray); + Console.WriteLine(" Initial constraints:"); + foreach (LinearConstraint cc in Constraints) { + Console.WriteLine(" {0}", cc); + } +#endif + + FrameRays.Add(ray.Clone()); +#if FIXED_DESERIALIZER + assert Forall{IVariable! var in ray.GetDefinedDimensions(); FrameDimensions.Contains(var)}; +#endif + + // We use a new temporary dimension. + IVariable! lambda = new LambdaDimension(); + + // We change the constraints A*X <= B into + // A*X - (A*ray)*lambda <= B. + // That means that each row k in A (which corresponds to one LinearConstraint + // in Constraints) is changed by subtracting + // (A*ray)[k] * lambda + // from row k. + // Note: + // (A*ray)[k] + // = { A*ray is a row vector whose every row i is the dot-product of + // row i of A with the column vector "ray" } + // A[k]*ray + foreach (LinearConstraint! cc in (!)Constraints) + { + Rational d = cc.EvaluateLhs(ray); + cc.SetCoefficient(lambda, -d); + } + + // We also add the constraints that lambda is at least 0. + LinearConstraint la = new LinearConstraint(LinearConstraint.ConstraintRelation.LE); + la.SetCoefficient(lambda, Rational.MINUS_ONE); + la.rhs = Rational.ZERO; + Constraints.Add(la); +#if DEBUG_PRINT + Console.WriteLine(" Constraints after addition:"); + foreach (LinearConstraint cc in Constraints) { + Console.WriteLine(" {0}", cc); + } +#endif + + // Finally, project out the dummy dimension. + Constraints = Project(lambda, Constraints); + +#if DEBUG_PRINT + Console.WriteLine(" Resulting constraints:"); + foreach (LinearConstraint cc in Constraints) { + Console.WriteLine(" {0}", cc); + } +#endif + } + + /// + /// Adds a line to the frame of "this" and updates Constraints accordingly, see + /// Cousot and Halbwachs, section 3.3.1.1. However, this method does not simplify + /// Constraints after the operation; that remains the caller's responsibility (which + /// gives the caller the opportunity to make multiple calls to AddVertex, AddRay, + /// and AddLine before calling SimplifyConstraints). + /// Assumes Constraints (and the frame fields) to be non-null. + /// + /// + void AddLine(FrameElement! line) + requires this.FrameLines != null; + { + // Note: The code for AddLine is identical to that of AddRay, except the AddLine + // does not introduce the constraint 0 <= lambda. (One could imagine sharing the + // code between AddRay and AddLine.) +#if DEBUG_PRINT + Console.WriteLine("DEBUG: AddLine called on {0}", line); + Console.WriteLine(" Initial constraints:"); + foreach (LinearConstraint cc in Constraints) { + Console.WriteLine(" {0}", cc); + } +#endif + + FrameLines.Add(line.Clone()); +#if FIXED_DESERIALIZER + assert Forall{IVariable! var in line.GetDefinedDimensions(); FrameDimensions.Contains(var)}; +#endif + + // We use a new temporary dimension. + IVariable! lambda = new LambdaDimension(); + + // We change the constraints A*X <= B into + // A*X - (A*line)*lambda <= B. + // That means that each row k in A (which corresponds to one LinearConstraint + // in Constraints) is changed by subtracting + // (A*line)[k] * lambda + // from row k. + // Note: + // (A*line)[k] + // = { A*line is a row vector whose every row i is the dot-product of + // row i of A with the column vector "line" } + // A[k]*line + foreach (LinearConstraint! cc in (!)Constraints) + { + Rational d = cc.EvaluateLhs(line); + cc.SetCoefficient(lambda, -d); + } + +#if DEBUG_PRINT + Console.WriteLine(" Constraints after addition:"); + foreach (LinearConstraint cc in Constraints) { + Console.WriteLine(" {0}", cc); + } +#endif + + // Finally, project out the dummy dimension. + Constraints = Project(lambda, Constraints); + +#if DEBUG_PRINT + Console.WriteLine(" Resulting constraints:"); + foreach (LinearConstraint cc in Constraints) { + Console.WriteLine(" {0}", cc); + } +#endif + } + + ISet /*IVariable!*/! GetDefinedDimensions() + { + HashSet /*IVariable!*/! dims = new HashSet /*IVariable!*/ (); + foreach (ArrayList p in new ArrayList[]{FrameVertices, FrameRays, FrameLines}) + { + if (p != null) + { + foreach (FrameElement! element in p) + { + foreach (IVariable! dim in element.GetDefinedDimensions()) + { + dims.Add(dim); + } + } + } + } + return dims; + } + + // -------------------------------------------------------------------------------------------------------- + // ------------------ Simplification routines ------------------------------------------------------------- + // -------------------------------------------------------------------------------------------------------- + + /// + /// Uses the Constraints to simplify the frame. See section 3.4.4 of Cousot and Halbwachs. + /// + void SimplifyFrame() + requires this.Constraints != null; + { + SimplificationStatus[]! status; + + SimplifyFrameElements((!)FrameVertices, true, Constraints, out status); + RemoveIrrelevantFrameElements(FrameVertices, status, null); + + SimplifyFrameElements((!)FrameRays, false, Constraints, out status); + RemoveIrrelevantFrameElements(FrameRays, status, FrameLines); + } + + enum SimplificationStatus { Irrelevant, Relevant, More }; + + /// + /// For each i, sets status[i] to: + ///
    + ///
  • Irrelevant if ff[i] is irrelevant
    • + ///
  • Relevant if ff[i] is irrelevant
    • + ///
  • More if vertices is true and ray ff[i] can be replaced by a line ff[i]
    • + ///
+ /// + /// + /// true if "ff" contains vertices; false if "ff" contains rays + /// + /// + static void SimplifyFrameElements(ArrayList! /*FrameElement*/ ff, bool vertices, + ArrayList! /*LinearConstraint*/ constraints, + out SimplificationStatus[]! status) + { + status = new SimplificationStatus[ff.Count]; + bool[,] sat = new bool[ff.Count, constraints.Count]; + for (int i = 0; i < ff.Count; i++) + { + FrameElement f = (FrameElement!)ff[i]; + int cnt = 0; + for (int c = 0; c < constraints.Count; c++) + { + LinearConstraint lc = (LinearConstraint!)constraints[c]; + bool s = lc.IsSaturatedBy(f, vertices); + if (s) + { + sat[i,c] = true; + cnt++; + } + } + if (!vertices && cnt == constraints.Count) + { + status[i] = SimplificationStatus.More; + } + else + { + status[i] = SimplificationStatus.Relevant; + } + } + + CheckPairSimplifications(sat, status); + } + + /// + /// Requires sat.GetLength(0) == status.Length. + /// + /// + /// + static void CheckPairSimplifications(bool[,]! sat, SimplificationStatus[]! status) + requires sat.GetLength(0) == status.Length; + { + int M = sat.GetLength(0); + int N = sat.GetLength(1); + + for (int i = 0; i < M-1; i++) + { + if (status[i] != SimplificationStatus.Relevant) + { + continue; + } + for (int j = i+1; j < M; j++) + { + if (status[j] != SimplificationStatus.Relevant) + { + continue; + } + // check (sat[i,*] <= sat[j,*]) and (sat[i,*] >= sat[j,*]) + int cmp = 0; // -1: (sat[i,*] <= sat[j,*]), 0: equal, 1: (sat[i,*] >= sat[j,*]) + for (int c = 0; c < N; c++) + { + if (cmp < 0) + { + if (sat[i,c] && !sat[j,c]) + { + // incomparable + goto NEXT_PAIR; + } + } + else if (0 < cmp) + { + if (!sat[i,c] && sat[j,c]) + { + // incomparable + goto NEXT_PAIR; + } + } + else if (sat[i,c] != sat[j,c]) + { + if (!sat[i,c]) + { + cmp = -1; + } + else + { + cmp = 1; + } + } + } + if (cmp <= 0) + { + // sat[i,*] <= sat[j,*] holds, so mark i as irrelevant + status[i] = SimplificationStatus.Irrelevant; + goto NEXT_OUTER; + } + else + { + // sat[i,*] >= sat[j,*] holds, so mark j as irrelevant + status[j] = SimplificationStatus.Irrelevant; + } + NEXT_PAIR: {} + } + NEXT_OUTER: {} + } + } + + static void RemoveIrrelevantFrameElements(ArrayList! /*FrameElement*/ ff, SimplificationStatus[]! status, + /*maybe null*/ ArrayList /*FrameElement*/ lines) + requires ff.Count == status.Length; + { + for (int j = ff.Count - 1; 0 <= j; j--) + { + switch (status[j]) + { + case SimplificationStatus.Relevant: + break; + case SimplificationStatus.Irrelevant: +#if DEBUG_PRINT + Console.WriteLine("Removing irrelevant {0}: {1}", lines == null ? "vertex" : "ray", ff[j]); +#endif + ff.RemoveAt(j); + break; + case SimplificationStatus.More: + System.Diagnostics.Debug.Assert(lines != null); + FrameElement f = (FrameElement)ff[j]; +#if DEBUG_PRINT + Console.WriteLine("Changing ray into line: {0}", f); +#endif + ff.RemoveAt(j); + assert lines != null; + lines.Add(f); + break; + } + } + } + + /// + /// Uses the frame to simplify Constraints. See section 3.3.1.2 of Cousot and Halbwachs. + /// + /// Note: This code does not necessarily eliminate all irrelevant equalities; Cousot and + /// Halbwachs only claim that the technique eliminates all irrelevant inequalities. + /// + void SimplifyConstraints() + { + if (Constraints == null) + { + return; + } + assume this.FrameVertices != null; + assume this.FrameRays != null; + + SimplificationStatus[] status = new SimplificationStatus[Constraints.Count]; + /*readonly*/ int feCount = FrameVertices.Count + FrameRays.Count; + + // Create a table that keeps track of which constraints are satisfied by which vertices and rays + bool[,] sat = new bool[Constraints.Count, FrameVertices.Count + FrameRays.Count]; + for (int i = 0; i < Constraints.Count; i++) + { + status[i] = SimplificationStatus.Relevant; + LinearConstraint lc = (LinearConstraint!)Constraints[i]; + int cnt = 0; // number of vertices and rays that saturate lc + for (int j = 0; j < FrameVertices.Count; j++) + { + FrameElement vertex = (FrameElement!)FrameVertices[j]; + if (lc.IsSaturatedBy(vertex, true)) + { + sat[i,j] = true; + cnt++; + } + } + if (cnt == 0) + { + // no vertex saturates the constraint, so the constraint is irrelevant + status[i] = SimplificationStatus.Irrelevant; + continue; + } + for (int j = 0; j < FrameRays.Count; j++) + { + FrameElement ray = (FrameElement!)FrameRays[j]; + if (lc.IsSaturatedBy(ray, false)) + { + sat[i, FrameVertices.Count + j] = true; + cnt++; + } + } + if (cnt == feCount) + { + status[i] = SimplificationStatus.More; + } + else + { + // Cousot and Halbwachs says that all equalities are found in the way we just tested. + // If I understand that right, then we should not get here if the constraint is an + // equality constraint. The following assertion tests my understanding. --KRML + System.Diagnostics.Debug.Assert(lc.Relation == LinearConstraint.ConstraintRelation.LE); + } + } + + CheckPairSimplifications(sat, status); + + // Finally, make the changes to the list of constraints + for (int i = Constraints.Count - 1; 0 <= i; i--) + { + switch (status[i]) + { + case SimplificationStatus.Relevant: + break; + case SimplificationStatus.Irrelevant: +#if DEBUG_PRINT + Console.WriteLine("Removing irrelevant constraint: {0}", Constraints[i]); +#endif + Constraints.RemoveAt(i); + break; + case SimplificationStatus.More: + LinearConstraint lc = (LinearConstraint!)Constraints[i]; + if (lc.Relation == LinearConstraint.ConstraintRelation.LE) + { +#if DEBUG_PRINT + Console.WriteLine("Converting the following constraint into an equality: {0}", lc); +#endif + LinearConstraint lcEq = lc.ChangeRelation(LinearConstraint.ConstraintRelation.EQ); + Constraints[i] = lcEq; + } + break; + } + } + + foreach (LinearConstraint! lc in Constraints) { + lc.Normalize(); + } + } + + // -------------------------------------------------------------------------------------------------------- + // ------------------ Cloning routines -------------------------------------------------------------------- + // -------------------------------------------------------------------------------------------------------- + + public LinearConstraintSystem! Clone() + { + LinearConstraintSystem z = new LinearConstraintSystem(); + z.FrameDimensions = (IMutableSet /*IVariable!*/!)this.FrameDimensions.Clone(); + if (this.Constraints != null) + { + z.Constraints = DeeperListCopy_LC(this.Constraints); + z.FrameVertices = DeeperListCopy_FE((!)this.FrameVertices); + z.FrameRays = DeeperListCopy_FE((!)this.FrameRays); + z.FrameLines = DeeperListCopy_FE((!)this.FrameLines); + } + else + { + System.Diagnostics.Debug.Assert(this.FrameVertices == null); + System.Diagnostics.Debug.Assert(this.FrameRays == null); + System.Diagnostics.Debug.Assert(this.FrameLines == null); + // the constructor should already have set these fields of z to null + System.Diagnostics.Debug.Assert(z.Constraints == null); + System.Diagnostics.Debug.Assert(z.FrameVertices == null); + System.Diagnostics.Debug.Assert(z.FrameRays == null); + System.Diagnostics.Debug.Assert(z.FrameLines == null); + } + return z; + } + + /// + /// Clones "list" and the elements of "list". + /// + /// + /// + ArrayList /*LinearConstraint*/ DeeperListCopy_LC(ArrayList! /*LinearConstraint*/ list) + { + ArrayList /*LinearConstraint*/ z = new ArrayList /*LinearConstraint*/ (list.Count); + foreach (LinearConstraint! lc in list) + { + z.Add(lc.Clone()); + } + System.Diagnostics.Debug.Assert(z.Count == list.Count); + return z; + } + + /// + /// Clones "list" and the elements of "list". + /// + /// + /// + ArrayList /*FrameElement*/ DeeperListCopy_FE(ArrayList! /*FrameElement*/ list) + { + ArrayList /*FrameElement*/ z = new ArrayList /*FrameElement*/ (list.Count); + foreach (FrameElement! fe in list) + { + z.Add(fe.Clone()); + } + System.Diagnostics.Debug.Assert(z.Count == list.Count); + return z; + } + + // -------------------------------------------------------------------------------------------------------- + // ------------------ Debugging and unit test routines ---------------------------------------------------- + // -------------------------------------------------------------------------------------------------------- + + public void Dump() + { + Console.WriteLine(" Constraints:"); + if (Constraints == null) + { + Console.WriteLine(" "); + } + else + { + foreach (LinearConstraint cc in Constraints) + { + Console.WriteLine(" {0}", cc); + } + } + + Console.WriteLine(" FrameDimensions: {0}", FrameDimensions); + + Console.WriteLine(" FrameVerticies:"); + if (FrameVertices == null) + { + Console.WriteLine(" "); + } + else + { + foreach (FrameElement fe in FrameVertices) + { + Console.WriteLine(" {0}", fe); + } + } + + Console.WriteLine(" FrameRays:"); + if (FrameRays == null) + { + Console.WriteLine(" "); + } + else + { + foreach (FrameElement fe in FrameRays) + { + Console.WriteLine(" {0}", fe); + } + } + + Console.WriteLine(" FrameLines:"); + if (FrameLines == null) + { + Console.WriteLine(" "); + } + else + { + foreach (FrameElement fe in FrameLines) + { + Console.WriteLine(" {0}", fe); + } + } + } + + class TestVariable : IVariable { + readonly string! name; + + public string! Name + { + get + { + return name; + } + } + + public TestVariable(string! name) { + this.name = name; + } + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public object DoVisit(ExprVisitor! visitor) { + return visitor.VisitVariable(this); + } + } + + public static void RunValidationA() + { + IVariable! dim1 = new TestVariable("X"); + IVariable! dim2 = new TestVariable("Y"); + IVariable! dim3 = new TestVariable("Z"); + + FrameElement s1 = new FrameElement(); + s1.AddCoordinate(dim1, Rational.ONE); + s1.AddCoordinate(dim2, Rational.MINUS_ONE); + s1.AddCoordinate(dim3, Rational.ZERO); + FrameElement s2 = new FrameElement(); + s2.AddCoordinate(dim1, Rational.MINUS_ONE); + s2.AddCoordinate(dim2, Rational.ONE); + s2.AddCoordinate(dim3, Rational.ZERO); + FrameElement r1 = new FrameElement(); + r1.AddCoordinate(dim1, Rational.ZERO); + r1.AddCoordinate(dim2, Rational.ZERO); + r1.AddCoordinate(dim3, Rational.ONE); + FrameElement d1 = new FrameElement(); + d1.AddCoordinate(dim1, Rational.ONE); + d1.AddCoordinate(dim2, Rational.ONE); + d1.AddCoordinate(dim3, Rational.ZERO); + + // create lcs from frame -- cf. Cousot/Halbwachs 1978, section 3.3.1.1 + LinearConstraintSystem lcs = new LinearConstraintSystem(s1); + lcs.Dump(); + + lcs.AddVertex(s2); + lcs.Dump(); + + lcs.AddRay(r1); + lcs.Dump(); + + lcs.AddLine(d1); + lcs.Dump(); + + lcs.SimplifyConstraints(); + lcs.Dump(); + +#if LATER + lcs.GenerateFrameFromConstraints(); // should give us back the original frame... +#endif + Console.WriteLine("IsSubset? {0}", lcs.IsSubset(lcs.Clone())); + lcs.Dump(); + } + + /// + /// Tests the example in section 3.4.3 of Cousot and Halbwachs. + /// + public static void RunValidationB() + { + IVariable! X = new TestVariable("X"); + IVariable! Y = new TestVariable("Y"); + IVariable! Z = new TestVariable("Z"); + ArrayList /*LinearConstraint*/ cs = new ArrayList /*LinearConstraint*/ (); + + LinearConstraint c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE); + c.SetCoefficient(X, Rational.MINUS_ONE); + c.SetCoefficient(Y, Rational.ONE); + c.SetCoefficient(Z, Rational.MINUS_ONE); + c.rhs = Rational.ZERO; + cs.Add(c); + + c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE); + c.SetCoefficient(X, Rational.MINUS_ONE); + c.rhs = Rational.MINUS_ONE; + cs.Add(c); + + c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE); + c.SetCoefficient(X, Rational.MINUS_ONE); + c.SetCoefficient(Y, Rational.MINUS_ONE); + c.SetCoefficient(Z, Rational.ONE); + c.rhs = Rational.ZERO; + cs.Add(c); + + c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE); + c.SetCoefficient(Y, Rational.MINUS_ONE); + c.SetCoefficient(Z, Rational.ONE); + c.rhs = Rational.FromInt(3); + cs.Add(c); + + LinearConstraintSystem lcs = new LinearConstraintSystem(cs); + Console.WriteLine("==================== The final linear constraint system ===================="); + lcs.Dump(); + } + + public static void RunValidationC() + { + // Run the example in section 3.4.3 of Cousot and Halbwachs backwards, that is, from + // from to constraints. + IVariable! dim1 = new TestVariable("X"); + IVariable! dim2 = new TestVariable("Y"); + IVariable! dim3 = new TestVariable("Z"); + + FrameElement s0 = new FrameElement(); + s0.AddCoordinate(dim1, Rational.ONE); + s0.AddCoordinate(dim2, Rational.FromInts(1, 2)); + s0.AddCoordinate(dim3, Rational.FromInts(-1, 2)); + + FrameElement s1 = new FrameElement(); + s1.AddCoordinate(dim1, Rational.ONE); + s1.AddCoordinate(dim2, Rational.FromInts(-1, 2)); + s1.AddCoordinate(dim3, Rational.FromInts(1, 2)); + + FrameElement s2 = new FrameElement(); + s2.AddCoordinate(dim1, Rational.FromInt(3)); + s2.AddCoordinate(dim2, Rational.FromInts(-3, 2)); + s2.AddCoordinate(dim3, Rational.FromInts(3, 2)); + + FrameElement r0 = new FrameElement(); + r0.AddCoordinate(dim1, Rational.ONE); + r0.AddCoordinate(dim2, Rational.FromInts(1, 2)); + r0.AddCoordinate(dim3, Rational.FromInts(-1, 2)); + + FrameElement r1 = new FrameElement(); + r1.AddCoordinate(dim1, Rational.ONE); + r1.AddCoordinate(dim2, Rational.ZERO); + r1.AddCoordinate(dim3, Rational.ZERO); + + FrameElement d0 = new FrameElement(); + d0.AddCoordinate(dim1, Rational.ZERO); + d0.AddCoordinate(dim2, Rational.ONE); + d0.AddCoordinate(dim3, Rational.ONE); + + LinearConstraintSystem lcs = new LinearConstraintSystem(s0); + lcs.Dump(); + + lcs.AddVertex(s1); + lcs.Dump(); + + lcs.AddVertex(s2); + lcs.Dump(); + + lcs.AddRay(r0); + lcs.Dump(); + + lcs.AddRay(r1); + lcs.Dump(); + + lcs.AddLine(d0); + lcs.Dump(); + + lcs.SimplifyConstraints(); + lcs.Dump(); + +#if LATER + lcs.GenerateFrameFromConstraints(); // should give us back the original frame... +#endif + } + } +} \ No newline at end of file diff --git a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc new file mode 100644 index 00000000..bcf9c64d --- /dev/null +++ b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc @@ -0,0 +1,744 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework +{ + using System; + using System.Collections; + using System.Collections.Generic; + using System.Diagnostics; + using Microsoft.Contracts; + using Microsoft.Basetypes; + + using ISet = Microsoft.Boogie.Set; + using HashSet = Microsoft.Boogie.Set; + + + /// + /// Represents an invariant over linear variable constraints, represented by a polyhedron. + /// + public class PolyhedraLattice : Lattice + { + private static readonly Logger! log = new Logger("Polyhedra"); + + private class PolyhedraLatticeElement : Element + { + + public LinearConstraintSystem! lcs; + + /// + /// Creates a top or bottom elements, according to parameter "top". + /// + public PolyhedraLatticeElement (bool top) + { + if (top) + { + lcs = new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ()); + } + else + { + lcs = new LinearConstraintSystem(); + } + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override string! ToString() + { + return lcs.ToString(); + } + + public override void Dump(string! msg) { + System.Console.WriteLine("PolyhedraLatticeElement.Dump({0}):", msg); + lcs.Dump(); + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override ICollection! FreeVariables() + { + return lcs.FreeVariables(); + } + + public PolyhedraLatticeElement (LinearConstraintSystem! lcs) + { + this.lcs = lcs; + } + + public override Element! Clone () + { + return new PolyhedraLatticeElement( (!) lcs.Clone()); + } + + } // class + + readonly ILinearExprFactory! factory; + readonly IPropExprFactory! propFactory; + + public PolyhedraLattice(ILinearExprFactory! linearFactory, IPropExprFactory! propFactory) + : base(linearFactory) + { + log.Enabled = Lattice.LogSwitch; + this.factory = linearFactory; + this.propFactory = propFactory; + // base(linearFactory); + } + + public override Element! Top + { + get + { + return new PolyhedraLatticeElement(true); + } + } + + public override Element! Bottom + { + get + { + return new PolyhedraLatticeElement(false); + } + } + + public override bool IsBottom (Element! element) + { + PolyhedraLatticeElement e = (PolyhedraLatticeElement)element; + return e.lcs.IsBottom(); + } + + public override bool IsTop (Element! element) + { + PolyhedraLatticeElement e = (PolyhedraLatticeElement)element; + return e.lcs.IsTop(); + } + + + /// + /// Returns true iff a is a subset of this. + /// + /// + /// + protected override bool AtMost (Element! first, Element! second) // this <= that + { + PolyhedraLatticeElement a = (PolyhedraLatticeElement) first; + PolyhedraLatticeElement b = (PolyhedraLatticeElement) second; + return b.lcs.IsSubset(a.lcs); + } + + + public override string! ToString (Element! e) + { + return ((PolyhedraLatticeElement)e).lcs.ToString(); + } + + public override IExpr! ToPredicate(Element! element) + { + PolyhedraLatticeElement e = (PolyhedraLatticeElement)element; + return e.lcs.ConvertToExpression(factory); + } + + + + public override Lattice.Element! NontrivialJoin (Element! first, Element! second) + { + log.DbgMsg("Joining ..."); log.DbgMsgIndent(); + PolyhedraLatticeElement aa = (PolyhedraLatticeElement) first; + PolyhedraLatticeElement bb = (PolyhedraLatticeElement) second; + PolyhedraLatticeElement result = new PolyhedraLatticeElement(aa.lcs.Join(bb.lcs)); + log.DbgMsg(string.Format("{0} |_| {1} --> {2}", this.ToString(first), this.ToString(second), this.ToString(result))); + log.DbgMsgUnindent(); + return result; + } + + + public override Lattice.Element! NontrivialMeet (Element! first, Element! second) + { + PolyhedraLatticeElement aa = (PolyhedraLatticeElement) first; + PolyhedraLatticeElement bb = (PolyhedraLatticeElement) second; + return new PolyhedraLatticeElement(aa.lcs.Meet(bb.lcs)); + } + + + public override Lattice.Element! Widen (Element! first, Element! second) + { + log.DbgMsg("Widening ..."); log.DbgMsgIndent(); + PolyhedraLatticeElement aa = (PolyhedraLatticeElement)first; + PolyhedraLatticeElement bb = (PolyhedraLatticeElement)second; + + LinearConstraintSystem lcs = aa.lcs.Widen(bb.lcs); + PolyhedraLatticeElement result = new PolyhedraLatticeElement(lcs); + log.DbgMsg(string.Format("{0} |_| {1} --> {2}", this.ToString(first), this.ToString(second), this.ToString(result))); + log.DbgMsgUnindent(); + return result; + } + + + public override Element! Eliminate (Element! e, IVariable! variable) + { + log.DbgMsg(string.Format("Eliminating {0} ...", variable)); + + PolyhedraLatticeElement ple = (PolyhedraLatticeElement)e; + if (ple.lcs.IsBottom()) + { + return ple; + } + return new PolyhedraLatticeElement(ple.lcs.Project(variable)); + } + + + public override Element! Rename (Element! e, IVariable! oldName, IVariable! newName) + { + log.DbgMsg(string.Format("Renaming {0} to {1} in {2} ...", oldName, newName, this.ToString(e))); + + PolyhedraLatticeElement ple = (PolyhedraLatticeElement)e; + if (ple.lcs.IsBottom()) + { + return ple; + } + return new PolyhedraLatticeElement(ple.lcs.Rename(oldName, newName)); + } + + public override bool Understands(IFunctionSymbol! f, IList/**/! args) { + return f is IntSymbol || + f.Equals(Int.Add) || + f.Equals(Int.Sub) || + f.Equals(Int.Negate) || + f.Equals(Int.Mul) || + f.Equals(Int.Eq) || + f.Equals(Int.Neq) || + f.Equals(Prop.Not) || + f.Equals(Int.AtMost) || + f.Equals(Int.Less) || + f.Equals(Int.Greater) || + f.Equals(Int.AtLeast); + } + + public override Answer CheckVariableDisequality(Element! e, IVariable! var1, IVariable! var2) { + PolyhedraLatticeElement! ple = (PolyhedraLatticeElement)e; + assume ple.lcs.Constraints != null; + ArrayList /*LinearConstraint!*/! clist = (ArrayList /*LinearConstraint!*/!)ple.lcs.Constraints.Clone(); + LinearConstraint! lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ); + lc.SetCoefficient(var1, Rational.ONE); + lc.SetCoefficient(var2, Rational.MINUS_ONE); + clist.Add(lc); + LinearConstraintSystem newLcs = new LinearConstraintSystem(clist); + if (newLcs.IsBottom()) { + return Answer.Yes; + } else { + return Answer.Maybe; + } + } + + public override Answer CheckPredicate(Element! e, IExpr! pred) { + PolyhedraLatticeElement! ple = (PolyhedraLatticeElement)Constrain(e, pred); + if (ple.lcs.IsBottom()) { + return Answer.No; + } + + // Note, "pred" may contain expressions that are not understood by the propFactory (in + // particular, this may happen because--currently, and perhaps is a design we'll want + // to change in the future--propFactory deals with BoogiePL expressions whereas "pred" + // may also refer to Equivalences.UninterpFun expressions). Thus, we cannot just + // call propFactory.Not(pred) to get the negation of "pred". + pred = new PolyhedraLatticeNegation(pred); + ple = (PolyhedraLatticeElement)Constrain(e, pred); + if (ple.lcs.IsBottom()) { + return Answer.Yes; + } else { + return Answer.Maybe; + } + } + + class PolyhedraLatticeNegation : IFunApp + { + IExpr! arg; + + public PolyhedraLatticeNegation(IExpr! arg) { + this.arg = arg; + // base(); + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] public object DoVisit(ExprVisitor! visitor) { + return visitor.VisitFunApp(this); + } + + public IFunctionSymbol! FunctionSymbol { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return Prop.Not; } } + + public IList/**/! Arguments { + [Pure][Reads(ReadsAttribute.Reads.Owned)] get { + IExpr[] args = new IExpr[] { arg }; + return ArrayList.ReadOnly(args); + } + } + + public IFunApp! CloneWithArguments(IList/**/! args) { + assert args.Count == 1; + return new PolyhedraLatticeNegation((IExpr!)args[0]); + } + } + + public override IExpr/*?*/ EquivalentExpr(Element! e, IQueryable! q, IExpr! expr, IVariable! var, ISet/**/! prohibitedVars) { + // BUGBUG: TODO: this method can be implemented in a more precise way + return null; + } + + + public override Element! Constrain (Element! e, IExpr! expr) + { + log.DbgMsg(string.Format("Constraining with {0} into {1} ...", expr, this.ToString(e))); + + PolyhedraLatticeElement ple = (PolyhedraLatticeElement)e; + if (ple.lcs.IsBottom()) + { + return ple; + } + LinearCondition le = LinearExpressionBuilder.AsCondition(expr); + if (le != null) { + // update the polyhedron according to the linear expression + assume ple.lcs.Constraints != null; + ArrayList /*LinearConstraint*/ clist = (ArrayList! /*LinearConstraint*/)ple.lcs.Constraints.Clone(); + le.AddToConstraintSystem(clist); + LinearConstraintSystem newLcs = new LinearConstraintSystem(clist); + + return new PolyhedraLatticeElement(newLcs); + } + return ple; + } + + } // class + + + /// + /// A LinearCondition follows this grammar: + /// LinearCondition ::= unsatisfiable + /// | LinearConstraint + /// | ! LinearConstraint + /// Note that negations are distributed to the leaves. + /// + abstract class LinearCondition + { + /// + /// Adds constraints to the list "clist". If "this" + /// entails some disjunctive constraints, they may not be added. + /// + /// + public abstract void AddToConstraintSystem(ArrayList! /*LinearConstraint*/ clist); + } + + class LCBottom : LinearCondition + { + public override void AddToConstraintSystem(ArrayList! /*LinearConstraint*/ clist) + { + // make an unsatisfiable constraint + LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ); + lc.rhs = Rational.FromInt(1); + clist.Add(lc); + } + } + + class LinearConditionLiteral : LinearCondition + { + public readonly bool positive; + public readonly LinearConstraint! constraint; + /// + /// Precondition: positive || constraint.Relation == LinearConstraint.ConstraintRelation.EQ + /// + /// + /// + public LinearConditionLiteral(bool positive, LinearConstraint! constraint) + requires positive || constraint.Relation == LinearConstraint.ConstraintRelation.EQ; + { + this.positive = positive; + this.constraint = constraint; + } + public override void AddToConstraintSystem(ArrayList! /*LinearConstraint*/ clist) + { + if (positive) + { + clist.Add(constraint); + } + else + { + assert constraint.Relation == LinearConstraint.ConstraintRelation.EQ; + // the constraint is disjunctive, so just ignore it + } + } + } + + class LinearExpressionBuilder + { + /// + /// Builds a linear condition from "e", if possible; returns null if not possible. + /// + /// + /// + public static /*maybe null*/ LinearCondition AsCondition(IExpr e) /* throws ArithmeticException */ + { + return GetCond(e, true); + } + + static /*maybe null*/ LinearCondition GetCond(IExpr e, bool positive) /* throws ArithmeticException */ + { + IFunApp funapp = e as IFunApp; + if (funapp == null) { + return null; + } + IFunctionSymbol! s = funapp.FunctionSymbol; + if ((positive && s.Equals(Prop.False)) || + (!positive && s.Equals(Prop.True))) { + return new LCBottom(); + } else if (s.Equals(Prop.Not)) { + assert funapp.Arguments.Count == 1; + return GetCond((IExpr!)funapp.Arguments[0], !positive); + } else if (funapp.Arguments.Count == 2) { + IExpr! arg0 = (IExpr!)funapp.Arguments[0]; + IExpr! arg1 = (IExpr!)funapp.Arguments[1]; + LinearExpr le0 = AsExpr(arg0); + if (le0 == null) { + return null; + } + LinearExpr le1 = AsExpr(arg1); + if (le1 == null) { + return null; + } + + LinearConstraint constraint = null; + bool sense = true; + if ((positive && s.Equals(Int.Less)) || (!positive && s.Equals(Int.AtLeast))) + { + constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.LE, BigNum.ONE); + } + else if ((positive && s.Equals(Int.AtMost)) || (!positive && s.Equals(Int.Greater))) + { + constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.LE, BigNum.ZERO); + } + else if ((positive && s.Equals(Int.AtLeast)) || (!positive && s.Equals(Int.Less))) + { + constraint = MakeConstraint(le1, le0, LinearConstraint.ConstraintRelation.LE, BigNum.ZERO); + } + else if ((positive && s.Equals(Int.Greater)) || (!positive && s.Equals(Int.AtMost))) + { + constraint = MakeConstraint(le1, le0, LinearConstraint.ConstraintRelation.LE, BigNum.ONE); + } + else if (s.Equals(Int.Eq)) + { + constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.EQ, BigNum.ZERO); + sense = positive; + } + else if (s.Equals(Int.Neq)) + { + constraint = MakeConstraint(le0, le1, LinearConstraint.ConstraintRelation.EQ, BigNum.ZERO); + sense = !positive; + } + if (constraint != null) { + if (constraint.coefficients.Count != 0) { + return new LinearConditionLiteral(sense, constraint); + } else if (constraint.IsConstantSatisfiable()) { + return null; + } else { + return new LCBottom(); + } + } + } + return null; + } + + public static LinearConstraint MakeConstraint(LinearExpr! le0, LinearExpr! le1, + LinearConstraint.ConstraintRelation rel, BigNum constantOffset) /* throws ArithmeticException */ + { + le1.Negate(); + le0.Add(le1); + le0.AddConstant(constantOffset); + return le0.ToConstraint(rel); + } + + /// + /// Builds a linear expression from "e", if possible; returns null if not possible. + /// + /// + /// + public static /*maybe null*/ LinearExpr AsExpr(IExpr! e) /* throws ArithmeticException */ + { + if (e is IVariable) { + // Note, without a type for the variable, we don't know if the identifier is intended to hold an integer value. + // However, it seems that no harm can be caused by here treating the identifier as if it held an + // integer value, because other parts of this method will reject the expression as a linear expression + // if non-numeric operations other than equality are applied to the identifier. + return new LinearExpr((IVariable)e); + } else if (e is IFunApp) { + IFunApp! funapp = (IFunApp)e; + IFunctionSymbol! s = funapp.FunctionSymbol; + + if (s is IntSymbol) { + return new LinearExpr(((IntSymbol)s).Value); + } else if (s.Equals(Int.Negate)) { + assert funapp.Arguments.Count == 1; + LinearExpr le = AsExpr((IExpr!)funapp.Arguments[0]); + if (le != null) { + le.Negate(); + return le; + } + } else if (s.Equals(Int.Add) || s.Equals(Int.Sub) || s.Equals(Int.Mul)) { + assert funapp.Arguments.Count == 2; + IExpr! arg0 = (IExpr!)funapp.Arguments[0]; + IExpr! arg1 = (IExpr!)funapp.Arguments[1]; + LinearExpr le0 = AsExpr(arg0); + if (le0 == null) { + return null; + } + LinearExpr le1 = AsExpr(arg1); + if (le1 == null) { + return null; + } + + if (s.Equals(Int.Add)) { + le0.Add(le1); + return le0; + } else if (s.Equals(Int.Sub)) { + le1.Negate(); + le0.Add(le1); + return le0; + } else if (s.Equals(Int.Mul)) { + BigNum x; + if (le0.AsConstant(out x)) + { + le1.Multiply(x); + return le1; + } + else if (le1.AsConstant(out x)) + { + le0.Multiply(x); + return le0; + } + } + } + } + return null; + } + } + + class LinearExpr + { + BigNum constant; + Term terms; + + class Term + { + public BigNum coeff; // non-0, if the node is used + public IVariable! var; + public Term next; + + public Term(BigNum coeff, IVariable! var) + { + this.coeff = coeff; + this.var = var; + // base(); + } + } + + public LinearExpr(BigNum x) + { + constant = x; + } + + public LinearExpr(IVariable! var) + { + constant = BigNum.ZERO; + terms = new Term(BigNum.ONE, var); + } + + public ISet /*IVariable!*/ GetDefinedDimensions() + { + HashSet /*IVariable!*/! dims = new HashSet /*IVariable!*/ (); + for (Term current = terms; current != null; current = current.next) + { + dims.Add(current.var); + } + return dims; + } + + public BigNum TermCoefficient(/*MayBeNull*/ IVariable! var) + { + BigNum z = BigNum.ZERO; + if (var == null) + { + z = this.constant; + } + else if (terms != null) + { + Term current = terms; + while (current != null) + { + if (current.var == var) + { + break; + } + current = current.next; + } + if (current != null) + { + z = current.coeff; + } + } + return z; + } + + public bool AsConstant(out BigNum x) + { + if (terms == null) + { + x = constant; + return true; + } + else + { + x = BigNum.FromInt(-70022); // to please complier + return false; + } + } + + public void Negate() /* throws ArithmeticException */ + { + checked + { + constant = -constant; + } + + for (Term t = terms; t != null; t = t.next) + { + checked + { + t.coeff = -t.coeff; + } + } + } + + /// + /// Adds "x" to "this". + /// + /// + public void AddConstant(BigNum x) /* throws ArithmeticException */ + { + checked + { + constant += x; + } + } + + /// + /// Adds "le" to "this". Afterwards, "le" should not be used, because it will have been destroyed. + /// + /// + public void Add(LinearExpr! le) /* throws ArithmeticException */ + requires le != this; + { + checked + { + constant += le.constant; + } + le.constant = BigNum.FromInt(-70029); // "le" should no longer be used; assign it a strange value so that misuse is perhaps more easily detected + + // optimization: + if (le.terms == null) + { + return; + } + else if (terms == null) + { + terms = le.terms; + le.terms = null; + return; + } + + // merge the two term lists + // Use a nested loop, which is quadratic in time complexity, but we hope the lists will be small + Term newTerms = null; + while (le.terms != null) + { + // take off next term from "le" + Term t = le.terms; + le.terms = t.next; + t.next = null; + + for (Term u = terms; u != null; u = u.next) + { + if (u.var == t.var) + { + checked + { + u.coeff += t.coeff; + } + goto NextOuter; + } + } + t.next = newTerms; + newTerms = t; + + NextOuter: ; + } + + // finally, include all non-0 terms + while (terms != null) + { + // take off next term from "this" + Term t = terms; + terms = t.next; + + if (!t.coeff.IsZero) + { + t.next = newTerms; + newTerms = t; + } + } + terms = newTerms; + } + + public void Multiply(BigNum x) /* throws ArithmeticException */ + { + if (x.IsZero) + { + constant = BigNum.ZERO; + terms = null; + } + else + { + for (Term t = terms; t != null; t = t.next) + { + checked + { + t.coeff *= x; + } + } + checked + { + constant *= x; + } + } + } + + public bool IsInvertible(IVariable! var) + { + for (Term t = terms; t != null; t = t.next) + { + if (t.var == var) + { + System.Diagnostics.Debug.Assert(!t.coeff.IsZero); + return true; + } + } + return false; + } + + public LinearConstraint ToConstraint(LinearConstraint.ConstraintRelation rel) /* throws ArithmeticException */ + { + LinearConstraint constraint = new LinearConstraint(rel); + for (Term t = terms; t != null; t = t.next) + { + constraint.SetCoefficient(t.var, t.coeff.ToRational); + } + BigNum rhs = -constant; + constraint.rhs = rhs.ToRational; + return constraint; + } + } +} diff --git a/Source/AIFramework/Polyhedra/SimplexTableau.ssc b/Source/AIFramework/Polyhedra/SimplexTableau.ssc new file mode 100644 index 00000000..b6f4095c --- /dev/null +++ b/Source/AIFramework/Polyhedra/SimplexTableau.ssc @@ -0,0 +1,717 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework +{ + using System.Collections; + using System; + using Microsoft.Contracts; + using Microsoft.Basetypes; + using IMutableSet = Microsoft.Boogie.Set; + using HashSet = Microsoft.Boogie.Set; + + + /// + /// Used by LinearConstraintSystem.GenerateFrameFromConstraints. + /// + public class SimplexTableau + { + readonly int rows; + readonly int columns; + readonly Rational[,]! m; + + readonly int numInitialVars; + readonly int numSlackVars; + readonly int rhsColumn; + + readonly ArrayList /*IVariable!*/! dims; + readonly int[]! basisColumns; + readonly int[]! inBasis; + bool constructionDone = false; + + void CheckInvariant() + { + assert(rows == m.GetLength(0)); + assert(1 <= columns && columns == m.GetLength(1)); + assert(0 <= numInitialVars); + assert(0 <= numSlackVars && numSlackVars <= rows); + assert(numInitialVars + numSlackVars + 1 == columns); + assert(rhsColumn == columns - 1); + assert(dims.Count == numInitialVars); + assert(basisColumns.Length == rows); + assert(inBasis.Length == numInitialVars + numSlackVars); + + bool[] b = new bool[numInitialVars + numSlackVars]; + int numColumnsInBasis = 0; + int numUninitializedRowInfo = 0; + for (int i = 0; i < rows; i++) + { + int c = basisColumns[i]; + if (c == rhsColumn) + { + // all coefficients in this row are 0 (but the right-hand side may be non-0) + for (int j = 0; j < rhsColumn; j++) + { + assert m[i,j].IsZero; + } + numColumnsInBasis++; + } + else if (c == -1) + { + assert(!constructionDone); + numUninitializedRowInfo++; + } + else + { + // basis column is a column + assert(0 <= c && c < numInitialVars + numSlackVars); + // basis column is unique + assert(!b[c]); + b[c] = true; + // column is marked as being in basis + assert(inBasis[c] == i); + // basis column really is a basis column + for (int j = 0; j < rows; j++) + { + if (j == i) + { + assert m[j,c].HasValue(1);// == (Rational)new Rational(1)); + } + else + { + assert m[j,c].IsZero; + } + } + } + } + // no other columns are marked as being in basis + foreach (int i in inBasis) + { + if (0 <= i) + { + assert(i < rows); + numColumnsInBasis++; + } + else + { + assert(i == -1); + } + } + assert(rows - numUninitializedRowInfo <= numColumnsInBasis && numColumnsInBasis <= rows); + assert(!constructionDone || numUninitializedRowInfo == 0); + } + + /// + /// Constructs a matrix that represents the constraints "constraints", adding slack + /// variables for the inequalities among "constraints". Puts the matrix in canonical + /// form. + /// + /// + [NotDelayed] + public SimplexTableau(ArrayList /*LinearConstraint*/! constraints) + { +#if DEBUG_PRINT + Console.WriteLine("DEBUG: SimplexTableau constructor called with:"); + foreach (LinearConstraint lc in constraints) + { + Console.WriteLine(" {0}", lc); + } +#endif + // Note: This implementation is not particularly efficient, but it'll do for now. + + ArrayList dims = this.dims = new ArrayList /*IVariable!*/ (); + int slacks = 0; + foreach (LinearConstraint! cc in constraints) + { + foreach (IVariable! dim in cc.coefficients.Keys) + { + if (!dims.Contains(dim)) + { + dims.Add(dim); + } + } + if (cc.Relation == LinearConstraint.ConstraintRelation.LE) + { + slacks++; + } + } + + int numInitialVars = this.numInitialVars = dims.Count; + int numSlackVars = this.numSlackVars = slacks; + int rows = this.rows = constraints.Count; + int columns = this.columns = numInitialVars + numSlackVars + 1; + this.m = new Rational[rows, columns]; + this.rhsColumn = columns-1; + this.basisColumns = new int[rows]; + this.inBasis = new int[columns-1]; + + base(); + + for (int i = 0; i < inBasis.Length; i++) + { + inBasis[i] = -1; + } + + // Fill in the matrix + int r = 0; + int iSlack = 0; + foreach (LinearConstraint! cc in constraints) + { + for (int i = 0; i < dims.Count; i++) + { + m[r,i] = cc[(IVariable!)dims[i]]; + } + if (cc.Relation == LinearConstraint.ConstraintRelation.LE) + { + m[r, numInitialVars + iSlack] = Rational.ONE; + basisColumns[r] = numInitialVars + iSlack; + inBasis[numInitialVars + iSlack] = r; + iSlack++; + } + else + { + basisColumns[r] = -1; // special value to communicate to Pivot that basis column i hasn't been set up yet + } + m[r,rhsColumn] = cc.rhs; + r++; + } + assert(r == constraints.Count); + assert(iSlack == numSlackVars); +#if DEBUG_PRINT + Console.WriteLine("DEBUG: Intermediate tableau state in SimplexTableau constructor:"); + Dump(); +#endif + + // Go through the rows with uninitialized basis columns. These correspond to equality constraints. + // For each one, find an initial variable (non-slack variable) whose column we can make the basis + // column of the row. + for (int i = 0; i < rows; i++) + { + if (basisColumns[i] != -1) + { + continue; + } + // Find a non-0 column in row i that we can make a basis column. Since rows corresponding + // to equality constraints don't have slack variables and since the pivot operations performed + // by iterations of this loop don't introduce any non-0 coefficients in the slack-variable + // columns of these rows, we only need to look through the columns corresponding to initial + // variables. + for (int j = 0; j < numInitialVars; j++) + { + if (m[i,j].IsNonZero) + { +#if DEBUG_PRINT + Console.WriteLine("-- About to Pivot({0},{1})", i, j); +#endif + assert(inBasis[j] == -1); + Pivot(i,j); +#if DEBUG_PRINT + Console.WriteLine("Tableau after Pivot:"); + Dump(); + #endif + goto SET_UP_NEXT_INBASIS_COLUMN; + } + } + // Check the assertion in the comment above, that is, that columns corresponding to slack variables + // are 0 in this row. + for (int j = numInitialVars; j < rhsColumn; j++) + { + assert m[i,j].IsZero; + } + // There is no column in this row that we can put into basis. + basisColumns[i] = rhsColumn; + SET_UP_NEXT_INBASIS_COLUMN: {} + } + + constructionDone = true; + CheckInvariant(); + } + + public IMutableSet! /*IVariable!*/ GetDimensions() + { + HashSet /*IVariable!*/ z = new HashSet /*IVariable!*/ (); + foreach (IVariable! dim in dims) + { + z.Add(dim); + } + return z; + } + + public Rational this [int r, int c] + { + get + { + return m[r,c]; + } + set + { + m[r,c] = value; + } + } + + /// + /// Applies the Pivot Operation on row "r" and column "c". + /// + /// This method can be called when !constructionDone, that is, at a time when not all basis + /// columns have been set up (indicated by -1 in basisColumns). This method helps set up + /// those basis columns. + /// + /// The return value is an undo record that can be used with UnPivot. + /// + /// + /// + public Rational[]! Pivot(int r, int c) + { + assert(0 <= r && r < rows); + assert(0 <= c && c < columns-1); + assert(m[r,c].IsNonZero); + assert(inBasis[c] == -1); // follows from invariant and m[r,c] != 0 + assert(basisColumns[r] != rhsColumn); // follows from invariant and m[r,c] != 0 + + Rational[] undo = new Rational[rows+1]; + for (int i = 0; i < rows; i++) + { + undo[i] = m[i,c]; + } + + // scale the pivot row + Rational q = m[r,c]; + if (q != Rational.ONE) + { + for (int j = 0; j < columns; j++) + { + m[r,j] /= q; + } + } + + // subtract a multiple of the pivot row from all other rows + for (int i = 0; i < rows; i++) + { + if (i != r) + { + q = m[i,c]; + if (q.IsNonZero) + { + for (int j = 0; j < columns; j++) + { + m[i,j] -= q * m[r,j]; + } + } + } + } + + // update basis information + int prevCol = basisColumns[r]; + undo[rows] = Rational.FromInt(prevCol); + basisColumns[r] = c; + if (prevCol != -1) + { + inBasis[prevCol] = -1; + } + inBasis[c] = r; + + return undo; + } + + /// + /// If the last operation applied to the tableau was: + /// undo = Pivot(i,j); + /// then UnPivot(i, j, undo) undoes the pivot operation. + /// Note: This operation is not supported for any call to Pivot before constructionDone + /// is set to true. + /// + /// + /// + /// + void UnPivot(int r, int c, Rational[]! undo) + { + assert(0 <= r && r < rows); + assert(0 <= c && c < columns-1); + assert(m[r,c].HasValue(1)); + assert(undo.Length == rows+1); + + // add a multiple of the pivot row to all other rows + for (int i = 0; i < rows; i++) + { + if (i != r) + { + Rational q = undo[i]; + if (q.IsNonZero) + { + for (int j = 0; j < columns; j++) + { + m[i,j] += q * m[r,j]; + } + } + } + } + + // scale the pivot row + Rational p = undo[r]; + for (int j = 0; j < columns; j++) + { + m[r,j] *= p; + } + + // update basis information + int prevCol = undo[rows].AsInteger; + assert(prevCol != -1); + basisColumns[r] = prevCol; + inBasis[c] = -1; + inBasis[prevCol] = r; + } + + /// + /// Returns true iff the current basis of the system of constraints modeled by the simplex tableau + /// is feasible. May have a side effect of performing a number of pivot operations on the tableau, + /// but any such pivot operation will be in the columns of slack variables (that is, this routine + /// does not change the set of initial-variable columns in basis). + /// + /// CAVEAT: I have no particular reason to believe that the algorithm used here will terminate. --KRML + /// + /// + public bool IsFeasibleBasis + { + get + { + // while there is a slack variable in basis whose row has a negative right-hand side + while (true) + { + bool feasibleBasis = true; + for (int c = numInitialVars; c < rhsColumn; c++) + { + int k = inBasis[c]; + if (0 <= k && k < rhsColumn && m[k,rhsColumn].IsNegative) + { + assert(m[k,c].HasValue(1)); // c is in basis + // Try to pivot on a different slack variable in this row + for (int i = numInitialVars; i < rhsColumn; i++) + { + if (m[k,i].IsNegative) + { + assert(c != i); // c is in basis, so m[k,c]==1, which is not negative + Pivot(k, i); +#if DEBUG_PRINT + Console.WriteLine("Tableau after Pivot operation on ({0},{1}) in IsFeasibleBasis:", k, i); + Dump(); +#endif + assert(inBasis[c] == -1); + assert(inBasis[i] == k); + assert(m[k,rhsColumn].IsNonNegative); + goto START_ANEW; + } + } + feasibleBasis = false; + } + } + return feasibleBasis; + START_ANEW: ; + } + return false; // make compiler shut up + } + } + + /// + /// Whether or not all initial variables (the non-slack variables) are in basis) + /// + public bool AllInitialVarsInBasis + { + get + { + for (int i = 0; i < numInitialVars; i++) + { + if (inBasis[i] == -1) + { + return false; + } + } + return true; + } + } + + /// + /// Adds as many initial variables as possible to the basis. + /// + /// + public void AddInitialVarsToBasis() + { + // while there exists an initial variable not in the basis and not satisfying + // condition 3.4.2.2 in Cousot and Halbwachs, perform a pivot operation + while (true) + { + for (int i = 0; i < numInitialVars; i++) + { + if (inBasis[i] == -1) + { + // initial variable i is not in the basis + for (int j = 0; j < rows; j++) + { + if (m[j,i].IsNonZero) + { + int k = basisColumns[j]; + if (numInitialVars <= k && k < rhsColumn) + { + // slack variable k is in basis for row j + Pivot(j, i); + assert(inBasis[k] == -1); + assert(inBasis[i] == j && basisColumns[j] == i); + goto START_ANEW; + } + } + } + } + } + // No more initial variables can be moved into basis. + return; + START_ANEW: {} + } + } + + /// + /// Adds to "lines" the lines implied by initial-variable columns not in basis + /// (see section 3.4.2 of Cousot and Halbwachs), and adds to "constraints" the + /// constraints to exclude those lines (see step 4.2 of section 3.4.3 of + /// Cousot and Halbwachs). + /// + /// + /// + public void ProduceLines(ArrayList /*FrameElement*/! lines, ArrayList /*LinearConstraint*/! constraints) + { + // for every initial variable not in basis + for (int i0 = 0; i0 < numInitialVars; i0++) + { + if (inBasis[i0] == -1) + { + FrameElement fe = new FrameElement(); + LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ); + for (int i = 0; i < numInitialVars; i++) + { + if (i == i0) + { + fe.AddCoordinate((IVariable!)dims[i], Rational.ONE); + lc.SetCoefficient((IVariable!)dims[i], Rational.ONE); + } + else if (inBasis[i] != -1) + { + // i is a basis column + assert(m[inBasis[i],i].HasValue(1)); + Rational val = -m[inBasis[i],i0]; + fe.AddCoordinate((IVariable!)dims[i], val); + lc.SetCoefficient((IVariable!)dims[i], val); + } + } + lines.Add(fe); + constraints.Add(lc); + } + } + } + + /// + /// From a feasible point where all initial variables are in the basis, traverses + /// all feasible bases containing all initial variables. For each such basis, adds + /// the vertices to "vertices" and adds to "rays" the extreme rays. See step 4.2 + /// in section 3.4.3 of Cousot and Halbwachs. + /// A more efficient algorithm is found in the paper "An algorithm for + /// determining all extreme points of a convex polytope" by N. E. Dyer and L. G. Proll, + /// Mathematical Programming, 12, 1977. + /// Assumes that the tableau is in a state where all initial variables are in the basis. + /// This method has no net effect on the tableau. + /// Note: Duplicate vertices and rays may be added. + /// + /// + /// + public void TraverseVertices(ArrayList! /*FrameElement*/ vertices, ArrayList! /*FrameElement*/ rays) + { + ArrayList /*bool[]*/ basesSeenSoFar = new ArrayList /*bool[]*/ (); + TraverseBases(basesSeenSoFar, vertices, rays); + } + + /// + /// Worker method of TraverseVertices. + /// This method has no net effect on the tableau. + /// + /// + /// + /// + void TraverseBases(ArrayList /*bool[]*/! basesSeenSoFar, ArrayList /*FrameElement*/! vertices, ArrayList /*FrameElement*/! rays) + { + CheckInvariant(); + + bool[] thisBasis = new bool[numSlackVars]; + for (int i = numInitialVars; i < rhsColumn; i++) + { + if (inBasis[i] != -1) + { + thisBasis[i-numInitialVars] = true; + } + } + foreach (bool[]! basis in basesSeenSoFar) + { + assert(basis.Length == numSlackVars); + for (int i = 0; i < numSlackVars; i++) + { + if (basis[i] != thisBasis[i]) + { + goto COMPARE_WITH_NEXT_BASIS; + } + } + // thisBasis and basis are the same--that is, basisColumns has been visited before--so + // we don't traverse anything from here + return; + COMPARE_WITH_NEXT_BASIS: {} + } + // basisColumns has not been seen before; record thisBasis and continue with the traversal here + basesSeenSoFar.Add(thisBasis); + +#if DEBUG_PRINT + Console.Write("TraverseBases, new basis: "); + foreach (bool t in thisBasis) { + Console.Write("{0}", t ? "*" : "."); + } + Console.WriteLine(); + Dump(); +#endif + // Add vertex + FrameElement v = new FrameElement(); + for (int i = 0; i < rows; i++) + { + int j = basisColumns[i]; + if (j < numInitialVars) + { + v.AddCoordinate((IVariable!)dims[j], m[i,rhsColumn]); + } + } +#if DEBUG_PRINT + Console.WriteLine(" Adding vertex: {0}", v); +#endif + vertices.Add(v); + + // Add rays. Traverse all columns corresponding to slack variables that + // are not in basis (see second bullet of section 3.4.2 of Cousot and Halbwachs). + for (int i0 = numInitialVars; i0 < rhsColumn; i0++) + { + if (inBasis[i0] != -1) + { + // skip those slack-variable columns that are in basis + continue; + } + // check if slack-variable, non-basis column i corresponds to an extreme ray + for (int row = 0; row < rows; row++) + { + if (m[row,i0].IsPositive) + { + for (int k = numInitialVars; k < rhsColumn; k++) + { + if (inBasis[k] != -1 && m[row,k].IsNonZero) + { + // does not correspond to an extreme ray + goto CHECK_NEXT_SLACK_VAR; + } + } + } + } + // corresponds to an extreme ray + FrameElement ray = new FrameElement(); + for (int i = 0; i < numInitialVars; i++) + { + int j0 = inBasis[i]; + Rational val = -m[j0,i0]; + ray.AddCoordinate((IVariable!)dims[i], val); + } +#if DEBUG_PRINT + Console.WriteLine(" Adding ray: {0}", ray); +#endif + rays.Add(ray); + CHECK_NEXT_SLACK_VAR: {} + } + + // Continue traversal + for (int i = numInitialVars; i < rhsColumn; i++) + { + int j = inBasis[i]; + if (j != -1) + { + // try moving i out of basis and some other slack-variable column into basis + for (int k = numInitialVars; k < rhsColumn; k++) + { + if (inBasis[k] == -1 && m[j,k].IsPositive) + { + Rational[] undo = Pivot(j, k); + // check if the new basis is feasible + for (int p = 0; p < rows; p++) + { + int c = basisColumns[p]; + if (numInitialVars <= c && c < rhsColumn && m[p,rhsColumn].IsNegative) + { + // not feasible + goto AFTER_TRAVERSE; + } + } + TraverseBases(basesSeenSoFar, vertices, rays); + AFTER_TRAVERSE: + UnPivot(j, k, undo); + } + } + } + } + } + + public void Dump() + { + // names + Console.Write(" "); + for (int i = 0; i < numInitialVars; i++) + { + Console.Write(" {0,4} ", dims[i]); + } + Console.WriteLine(); + // numbers + Console.Write(" "); + for (int i = 0; i < columns; i++) + { + if (i == numInitialVars || i == rhsColumn) + { + Console.Write("|"); + } + Console.Write(" {0,4}", i); + if (i < rhsColumn && inBasis[i] != -1) + { + Console.Write("* "); + assert(basisColumns[inBasis[i]] == i); + } + else + { + Console.Write(" "); + } + } + Console.WriteLine(); + // line + Console.Write(" "); + for (int i = 0; i < columns; i++) + { + if (i == numInitialVars || i == rhsColumn) + { + Console.Write("+"); + } + Console.Write("---------"); + } + Console.WriteLine(); + + for (int j = 0; j < rows; j++) + { + Console.Write("{0,4}: ", basisColumns[j]); + for (int i = 0; i < columns; i++) + { + if (i == numInitialVars || i == rhsColumn) + { + Console.Write("|"); + } + Console.Write(" {0,4:n1} ", m[j,i]); + } + Console.WriteLine(); + } + } + } +} 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; + + /// + /// Represents an invariant over constant variable assignments. + /// + 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! FreeVariables() + { + return (!) (new System.Collections.Generic.List()).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/**/! 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/**/! 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; + } + + /// + /// 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. + /// + 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/**/! 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; + + /// + /// This is an abstract domain for inferring constant expressions + /// + + public class ConstantExpressions : Lattice + { + /// + /// 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 ) + /// + private class AbstractElement: Element + { + private Dictionary variableBindings; + private Dictionary> 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(); + this.variableDependences = new Dictionary>(); + } + + /// + /// Our abstract element is top if and only if it has any constraint on variables + /// + public bool IsTop + { + get + { + return this.variableBindings.Keys.Count == 0 && this.variableDependences.Keys.Count == 0; + } + } + + /// + /// Our abstract element is bottom if and only if the maps are null + /// + public bool IsBottom + { + get + { + assert (this.variableBindings == null) <==> (this.variableDependences == null); + return this.variableBindings == null && this.variableDependences == null; + } + } + + /// + /// The pointwise join... + /// + 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 dependencies = left.variableDependences[var]; + List dup = new List(dependencies); + + result.variableDependences.Add(var, dup); + } + + foreach(IVariable! var in right.variableDependences.Keys) + { + if(result.variableDependences.ContainsKey(var)) + { + List dependencies = result.variableDependences[var]; + dependencies.AddRange(right.variableDependences[var]); + } + else + { + List dependencies = right.variableDependences[var]; + List dup = new List(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; + } + + + /// + /// Normalize the current abstract element, in that it propagetes the "dynamic" information throughtout the abstract element + /// + 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... + } + } + } + } + } + } + + /// + /// The pointwise meet... + /// + 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 depLeft = left.variableDependences[var]; + List 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! varsToRemove = new List(); + + foreach(IVariable var in result. + + + } + + /// + /// Clone the current abstract element + /// + 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 dependingVars = this.variableDependences[var]; + List clonedDependingVars = new List(dependingVars); + cloned.variableDependences.Add(var, clonedDependingVars); + } + } + + /// + /// Return the variables that have a binding + /// + public override ICollection! FreeVariables() + { + List vars = new List(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; + } + + /// + /// Perform the pointwise join of the two abstract elements + /// + 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); + } + + /// + /// Perform the pointwise meet of two abstract elements + /// + 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); + } + + + } + + /// + /// A wrapper in order to have the algebraic datatype BindExpr := IExpr | Top + /// + abstract class BindExpr + { + /// + /// True iff this expression is instance of BindExprTop + /// + public bool IsTop + { + get + { + return this is BindExprTop; + } + } + + static public BindExpr Top + { + get + { + return BindExprTop.UniqueTop; + } + } + + /// + /// True iff this expression is instance of BindExprBottom + /// + 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; + } + + } + + /// + /// A wrapper for an integer + /// + 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(); + } + } + + /// + /// The dynamic expression + /// + 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 ""; + } + } + + /// + /// The unreachable expression + /// + 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 ""; + } + } + +} // 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; + + /// + /// 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. + /// + 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; + } + } + + /// + /// Constructs an Elt with "n" bounds, namely the n non-null values of the "bounds" list. + /// + [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! FreeVariables() + { + return (!) (new System.Collections.Generic.List()).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/**/! 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/**/! 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; + } + } + + /// + /// The paramter is the top? + /// + public override bool IsTop(Element! element) + { + IntervalElement interval = (IntervalElement) element; + + return interval.IsTop(); + } + + /// + /// The parameter is the bottom? + /// + public override bool IsBottom(Element! element) + { + IntervalElement interval = (IntervalElement) element; + + return interval.IsBottom(); + } + + /// + /// The classic, pointwise, join of intervals + /// + 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; + } + + /// + /// The classic, pointwise, meet of intervals + /// + 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); + } + + + /// + /// 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 + /// + 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; + } + + + /// + /// Return true iff the interval left is containted in right + /// + 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; + } + + /// + /// Return just null + /// + public override IExpr GetFoldExpr(Element! element) + { + return null; + } + + /// + /// return a predicate inf "\leq x and x "\leq" sup (if inf [or sup] is not oo) + /// + 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; + } + + /// + /// For the moment consider just equalities. Other case must be considered + /// + public override bool Understands(IFunctionSymbol! f, IList /* + /// Evaluate the predicate passed as input according the semantics of intervals + /// + public override Element! EvaluatePredicate(IExpr! pred) + { + return this.EvaluatePredicateWithState(pred, null); + } + + /// + /// 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 + /// + 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; + } + + /// + /// Evaluate the expression (that is assured to be an arithmetic expression, in the state passed as a parameter + /// + 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; + } + + /// + /// Inner class standing for an interval on integers, possibly unbounded + /// + 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! FreeVariables() + { + return (!) (new System.Collections.Generic.List()).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; + + /// + /// Interface for a lattice that works on a per-variable basis. + /// + public abstract class MicroLattice : MathematicalLattice + { + /// + /// Returns the predicate on the given variable for the given + /// lattice element. + /// + public abstract IExpr! ToPredicate(IVariable! v, Element! e); + /* requires !e.IsBottom && !e.IsTop; */ + + /// + /// 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. + /// + /// The function symbol. + /// The argument context. + /// True if it may understand f, false if it does not understand f. + public abstract bool Understands(IFunctionSymbol! f, IList/**/! args); + + /// + /// 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 + /// + public virtual bool UnderstandsBasicArithmetics + { + get { return false; } + } + + /// + /// Evaluate the predicate e and a yield the lattice element + /// that is implied by it. + /// + /// The predicate that is assumed to contain 1 variable. + /// The most precise lattice element that is implied by the predicate. + public abstract Element! EvaluatePredicate(IExpr! e); + + /// + /// 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 + /// + public virtual Element! EvaluatePredicateWithState(IExpr! e, IFunctionalMap state) + { + return EvaluatePredicate(e); + } + + /// + /// Give an expression (often a value) that can be used to substitute for + /// the variable. + /// + /// A lattice element. + /// The null value if no such expression can be given. + 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! FreeVariables() + { + return (!) (new System.Collections.Generic.List()).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/**/! 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/**/! 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; + + /// + /// 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() + { + 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/**/! Variables { + get + requires !this.IsBottom; + { + assume this.constraints != null; + return (!) this.constraints.Keys; + } + } + + public IEnumerable/**/! 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]; + } + } + + /// + /// 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) + 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)); + } + + /// + /// 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) + { + 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! 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 ""; } + if (IsBottom(e)) { return ""; } + + 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); + } + + /// + /// Perform the pointwise widening of the elements in the map + /// + 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/**/! VariablesInExpression(IExpr! e, ISet/**/! 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/**/! 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; + } + + /// + /// Returns true iff the expression is in the form var == arithmeticExpr + /// + 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; + } + + /// + /// 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) + { + 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/**/ 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/**/! prohibitedVars) + { + try + { + EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var); + return InlineVariables((Elt)e, expr, (!)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) + { + 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) + { + return Answer.Maybe; + } + + public override void Validate() + { + base.Validate(); + microLattice.Validate(); + } + + } +} -- cgit v1.2.3