* 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

14 files changed, 61 insertions, 49 deletions

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
         /// <summary>

         /// Returns true iff "t" denotes a type constant.

         /// </summary>

-        [Pure][Reads(ReadsAttribute.Reads.Owned)]

+        [Pure]

         bool IsTypeConstant(IExpr! t);

 

         /// <summary>

         /// Returns true iff t0 and t1 are types such that t0 and t1 are equal.

         /// </summary>

-        [Pure][Reads(ReadsAttribute.Reads.Owned)]

+        [Pure]

         bool IsTypeEqual(IExpr! t0, IExpr! t1);

 

         /// <summary>

         /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.

         /// </summary>

-        [Pure][Reads(ReadsAttribute.Reads.Owned)]

+        [Pure]

         bool IsSubType(IExpr! t0, IExpr! t1);

 

         /// <summary>

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
         /// </summary>

         /// <param name="visitor">The expression visitor.</param>

         /// <returns>The result of the visit.</returns>

-        [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
     /// </summary>

     public interface IFunApp : IExpr

     {

-        IFunctionSymbol! FunctionSymbol { [Pure][Reads(ReadsAttribute.Reads.Owned)] get; }

+        IFunctionSymbol! FunctionSymbol { get; }

         IList/*<IExpr!>*/! Arguments

         {

-            [Pure][Reads(ReadsAttribute.Reads.Owned)][Rep] get

+            [Pure][Rep] get

             ensures result.IsReadOnly;

             ;

         }

@@ -82,9 +82,9 @@ namespace Microsoft.AbstractInterpretationFramework
     /// </summary>

     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
     /// </summary>

     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/*<AIType!>*/! 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
         /// <returns>true if the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" /> contains an element with the key; otherwise, false.</returns>

         /// <param name="key">The key to locate in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />. </param>

         /// <filterpriority>2</filterpriority>

-        [Pure][Reads(ReadsAttribute.Reads.Owned)]

+        [Pure]

         bool Contains(object! key);

 

         /// <summary>Returns an <see cref="T:System.Collections.IDictionaryEnumerator" /> for the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>

@@ -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<IVariable!>! FreeVariables()

             {

                 List<IVariable!>! list = new List<IVariable!>();

@@ -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<IVariable!>! 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/*<IExpr!>*/! 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<IVariable!>! FreeVariables()

             {

                 return (!) (new System.Collections.Generic.List<IVariable!>()).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<IVariable!>! FreeVariables()

             {

                 return (!) (new System.Collections.Generic.List<IVariable!>()).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<IVariable!>! FreeVariables()

         {

           return (!) (new System.Collections.Generic.List<IVariable!>()).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<IVariable!>! FreeVariables()

             {

                 return (!) (new System.Collections.Generic.List<IVariable!>()).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 "<bottom>";

+              }

+              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<IVariable!>! FreeVariables()

             {

                 throw new System.NotImplementedException();