summaryrefslogtreecommitdiff
path: root/Source/AIFramework
diff options
context:
space:
mode:
Diffstat (limited to 'Source/AIFramework')
-rw-r--r--Source/AIFramework/CommonFunctionSymbols.ssc19
-rw-r--r--Source/AIFramework/Expr.ssc20
-rw-r--r--Source/AIFramework/Functional.ssc4
-rw-r--r--Source/AIFramework/Lattice.ssc2
-rw-r--r--Source/AIFramework/MultiLattice.ssc5
-rw-r--r--Source/AIFramework/Mutable.ssc3
-rw-r--r--Source/AIFramework/Polyhedra/LinearConstraint.ssc4
-rw-r--r--Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc8
-rw-r--r--Source/AIFramework/Polyhedra/PolyhedraAbstraction.ssc10
-rw-r--r--Source/AIFramework/VariableMap/ConstantAbstraction.ssc2
-rw-r--r--Source/AIFramework/VariableMap/DynamicTypeLattice.ssc2
-rw-r--r--Source/AIFramework/VariableMap/Intervals.ssc10
-rw-r--r--Source/AIFramework/VariableMap/Nullness.ssc2
-rw-r--r--Source/AIFramework/VariableMap/VariableMapLattice.ssc19
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();
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 01:27:43 +0000