From 36bda629c0083590c5e4d17f06e769f822617033 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Thu, 18 Feb 2010 01:58:27 +0000 Subject: * Added "deprecated" comment in help message about /interprocInfer switch. The functionality is currently broken. * Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it) * Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods --- Source/AIFramework/CommonFunctionSymbols.ssc | 19 +++++++++---------- Source/AIFramework/Expr.ssc | 20 ++++++++++---------- Source/AIFramework/Functional.ssc | 4 ++-- Source/AIFramework/Lattice.ssc | 2 +- Source/AIFramework/MultiLattice.ssc | 5 ++--- Source/AIFramework/Mutable.ssc | 3 +-- Source/AIFramework/Polyhedra/LinearConstraint.ssc | 4 ++-- .../AIFramework/Polyhedra/LinearConstraintSystem.ssc | 8 ++++---- .../AIFramework/Polyhedra/PolyhedraAbstraction.ssc | 10 +++++----- .../AIFramework/VariableMap/ConstantAbstraction.ssc | 2 +- .../AIFramework/VariableMap/DynamicTypeLattice.ssc | 2 +- Source/AIFramework/VariableMap/Intervals.ssc | 10 +++++----- Source/AIFramework/VariableMap/Nullness.ssc | 2 +- .../AIFramework/VariableMap/VariableMapLattice.ssc | 19 +++++++++++++++++-- 14 files changed, 61 insertions(+), 49 deletions(-) (limited to 'Source/AIFramework') diff --git a/Source/AIFramework/CommonFunctionSymbols.ssc b/Source/AIFramework/CommonFunctionSymbols.ssc index 4e38fbcb..f014e963 100644 --- a/Source/AIFramework/CommonFunctionSymbols.ssc +++ b/Source/AIFramework/CommonFunctionSymbols.ssc @@ -30,11 +30,10 @@ namespace Microsoft.AbstractInterpretationFramework // base(); } -// public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } } - public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } } + public AIType! AIType { get { return typ; } } [NoDefaultContract] - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { return display; @@ -65,7 +64,7 @@ namespace Microsoft.AbstractInterpretationFramework return isym != null && isym.Value.Equals(this.Value); } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override int GetHashCode() { return Value.GetHashCode(); @@ -97,7 +96,7 @@ namespace Microsoft.AbstractInterpretationFramework return isym != null && isym.Value == this.Value && isym.Bits == this.Bits; } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override int GetHashCode() { unchecked { @@ -126,7 +125,7 @@ namespace Microsoft.AbstractInterpretationFramework return dsym != null && dsym.Value == this.Value; } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override int GetHashCode() { return Value.GetHashCode(); @@ -155,7 +154,7 @@ namespace Microsoft.AbstractInterpretationFramework } [NoDefaultContract] - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override int GetHashCode() { return Value.GetHashCode(); @@ -898,19 +897,19 @@ namespace Microsoft.AbstractInterpretationFramework /// /// Returns true iff "t" denotes a type constant. /// - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] bool IsTypeConstant(IExpr! t); /// /// Returns true iff t0 and t1 are types such that t0 and t1 are equal. /// - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] 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)] + [Pure] bool IsSubType(IExpr! t0, IExpr! t1); /// diff --git a/Source/AIFramework/Expr.ssc b/Source/AIFramework/Expr.ssc index 94dc4dc7..42621239 100644 --- a/Source/AIFramework/Expr.ssc +++ b/Source/AIFramework/Expr.ssc @@ -35,7 +35,7 @@ namespace Microsoft.AbstractInterpretationFramework /// /// The expression visitor. /// The result of the visit. - [Pure][Reads(ReadsAttribute.Reads.Owned)] object DoVisit(ExprVisitor! visitor); + [Pure] object DoVisit(ExprVisitor! visitor); // TODO: Type checking of the expressions. } @@ -57,10 +57,10 @@ namespace Microsoft.AbstractInterpretationFramework /// public interface IFunApp : IExpr { - IFunctionSymbol! FunctionSymbol { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; } + IFunctionSymbol! FunctionSymbol { get; } IList/**/! Arguments { - [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep] get + [Pure][Rep] get ensures result.IsReadOnly; ; } @@ -82,9 +82,9 @@ namespace Microsoft.AbstractInterpretationFramework /// 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; } + IVariable! Param { get; } + AIType! ParamType { get; } + IExpr! Body { get; } IFunction! CloneWithBody(IExpr! body); } @@ -307,7 +307,7 @@ namespace Microsoft.AbstractInterpretationFramework /// public interface IFunctionSymbol { - AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep][ResultNotNewlyAllocated] + AIType! AIType { [Rep][ResultNotNewlyAllocated] get; } } @@ -354,7 +354,7 @@ namespace Microsoft.AbstractInterpretationFramework public IList/**/! Arguments { - [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep] + [Pure][Rep] get ensures result.IsReadOnly; { @@ -364,12 +364,12 @@ namespace Microsoft.AbstractInterpretationFramework public int Arity { - [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return argTypes.Count; } + get { return argTypes.Count; } } public AIType! ReturnType { - [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return retType; } + get { return retType; } } /* TODO Do we have the invariant that two functions are equal iff they're the same object. diff --git a/Source/AIFramework/Functional.ssc b/Source/AIFramework/Functional.ssc index 4c4a5791..1413230e 100644 --- a/Source/AIFramework/Functional.ssc +++ b/Source/AIFramework/Functional.ssc @@ -28,7 +28,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections /// true if the contains an element with the key; otherwise, false. /// The key to locate in the . /// 2 - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] bool Contains(object! key); /// Returns an for the . @@ -106,7 +106,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections return new FunctionalHashtable(r); } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public bool Contains(object! key) { return h.Contains(key); diff --git a/Source/AIFramework/Lattice.ssc b/Source/AIFramework/Lattice.ssc index 2b606492..2ecc49f8 100644 --- a/Source/AIFramework/Lattice.ssc +++ b/Source/AIFramework/Lattice.ssc @@ -576,7 +576,7 @@ namespace Microsoft.AbstractInterpretationFramework return lattice.ToString(e); } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { return string.Format( diff --git a/Source/AIFramework/MultiLattice.ssc b/Source/AIFramework/MultiLattice.ssc index b6b6ba5e..761f4c7e 100644 --- a/Source/AIFramework/MultiLattice.ssc +++ b/Source/AIFramework/MultiLattice.ssc @@ -48,7 +48,7 @@ namespace Microsoft.AbstractInterpretationFramework return new Elt(this); } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { // string s = "MultiLattice+Elt{"; @@ -83,7 +83,7 @@ namespace Microsoft.AbstractInterpretationFramework } } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override ICollection! FreeVariables() { List! list = new List(); @@ -522,7 +522,6 @@ namespace Microsoft.AbstractInterpretationFramework public object Current { - [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return this.Entry; diff --git a/Source/AIFramework/Mutable.ssc b/Source/AIFramework/Mutable.ssc index 894359ef..36bb3647 100644 --- a/Source/AIFramework/Mutable.ssc +++ b/Source/AIFramework/Mutable.ssc @@ -18,10 +18,9 @@ namespace Microsoft.AbstractInterpretationFramework.Collections // 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() + [Pure] public bool IsEmpty() { return Count == 0; } diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.ssc b/Source/AIFramework/Polyhedra/LinearConstraint.ssc index 9ce1552b..087c3696 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraint.ssc +++ b/Source/AIFramework/Polyhedra/LinearConstraint.ssc @@ -36,7 +36,7 @@ namespace Microsoft.AbstractInterpretationFramework Relation = rel; } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { string s = null; @@ -501,7 +501,7 @@ namespace Microsoft.AbstractInterpretationFramework terms.Add(dimension, value); } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { string s = null; diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc index b4e33a28..a99a4ee8 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc +++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc @@ -172,7 +172,7 @@ namespace Microsoft.AbstractInterpretationFramework return Constraints != null && Constraints.Count == 0; } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { if (Constraints == null) @@ -1055,12 +1055,12 @@ namespace Microsoft.AbstractInterpretationFramework id = count; count++; } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { return "lambda" + id; } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public object DoVisit(ExprVisitor! visitor) { return visitor.VisitVariable(this); @@ -1697,7 +1697,7 @@ namespace Microsoft.AbstractInterpretationFramework public TestVariable(string! name) { this.name = name; } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public object DoVisit(ExprVisitor! visitor) { return visitor.VisitVariable(this); } diff --git a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc index bcf9c64d..fdb8d86d 100644 --- a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc +++ b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc @@ -43,7 +43,7 @@ namespace Microsoft.AbstractInterpretationFramework } } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { return lcs.ToString(); @@ -54,7 +54,7 @@ namespace Microsoft.AbstractInterpretationFramework lcs.Dump(); } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override ICollection! FreeVariables() { return lcs.FreeVariables(); @@ -258,14 +258,14 @@ namespace Microsoft.AbstractInterpretationFramework // base(); } - [Pure][Reads(ReadsAttribute.Reads.Owned)] public object DoVisit(ExprVisitor! visitor) { + [Pure] public object DoVisit(ExprVisitor! visitor) { return visitor.VisitFunApp(this); } - public IFunctionSymbol! FunctionSymbol { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return Prop.Not; } } + public IFunctionSymbol! FunctionSymbol { get { return Prop.Not; } } public IList/**/! Arguments { - [Pure][Reads(ReadsAttribute.Reads.Owned)] get { + get { IExpr[] args = new IExpr[] { arg }; return ArrayList.ReadOnly(args); } diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc index 7b7fd87e..97fb57ce 100644 --- a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc +++ b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc @@ -31,7 +31,7 @@ namespace Microsoft.AbstractInterpretationFramework public BigNum Constant { get { return this.constantValue; } } // only when IsConstant - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override System.Collections.Generic.ICollection! FreeVariables() { return (!) (new System.Collections.Generic.List()).AsReadOnly(); diff --git a/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc b/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc index b9d1a7a4..8161cb3e 100644 --- a/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc +++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.ssc @@ -114,7 +114,7 @@ namespace Microsoft.AbstractInterpretationFramework } } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override System.Collections.Generic.ICollection! FreeVariables() { return (!) (new System.Collections.Generic.List()).AsReadOnly(); diff --git a/Source/AIFramework/VariableMap/Intervals.ssc b/Source/AIFramework/VariableMap/Intervals.ssc index 721b175d..7f6211ba 100644 --- a/Source/AIFramework/VariableMap/Intervals.ssc +++ b/Source/AIFramework/VariableMap/Intervals.ssc @@ -466,13 +466,13 @@ namespace Microsoft.AbstractInterpretationFramework */ } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override System.Collections.Generic.ICollection! FreeVariables() { return (!) (new System.Collections.Generic.List()).AsReadOnly(); } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { return "[" + this.inf + ", " + this.sup + "]"; @@ -704,7 +704,7 @@ namespace Microsoft.AbstractInterpretationFramework this.val = i; } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { return this.Value.ToString(); @@ -746,7 +746,7 @@ namespace Microsoft.AbstractInterpretationFramework class PlusInfinity : InfinitaryInt { - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { return "+oo"; @@ -768,7 +768,7 @@ namespace Microsoft.AbstractInterpretationFramework class MinusInfinity : InfinitaryInt { - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override string! ToString() { return "-oo"; diff --git a/Source/AIFramework/VariableMap/Nullness.ssc b/Source/AIFramework/VariableMap/Nullness.ssc index 63d637ce..bbd1da70 100644 --- a/Source/AIFramework/VariableMap/Nullness.ssc +++ b/Source/AIFramework/VariableMap/Nullness.ssc @@ -27,7 +27,7 @@ namespace Microsoft.AbstractInterpretationFramework public Elt (Value v) { this.value = v; } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override System.Collections.Generic.ICollection! FreeVariables() { return (!) (new System.Collections.Generic.List()).AsReadOnly(); diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc index aa15f1e6..34f876f5 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.ssc +++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc @@ -51,6 +51,22 @@ namespace Microsoft.AbstractInterpretationFramework { return new Elt(this.constraints); } + + [Pure] + public override string! ToString() + { + if (constraints == null) { + return ""; + } + string s = "["; + string sep = ""; + foreach (IVariable! v in (!)constraints.Keys) { + Element m = (Element)constraints[v]; + s += sep + v.Name + " -> " + m; + sep = ", "; + } + return s + "]"; + } public static Elt! Top = new Elt(true); public static Elt! Bottom = new Elt(false); @@ -61,7 +77,6 @@ namespace Microsoft.AbstractInterpretationFramework } public bool IsBottom { - [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return this.constraints == null; } @@ -158,7 +173,7 @@ namespace Microsoft.AbstractInterpretationFramework return new Elt(newMap); } - [Pure][Reads(ReadsAttribute.Reads.Owned)] + [Pure] public override ICollection! FreeVariables() { throw new System.NotImplementedException(); -- cgit v1.2.3