diff options
| author |  tabarbe <unknown> | 2010-08-27 21:15:08 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-27 21:15:08 +0000 |
| commit | c333ecd2f30badea143e79f5f944a8c63398b959 (patch) | |
| tree | 28b04dc9f46d6fa90b4fdf38ffb24898bdc139b0 /Source/AIFramework | |
| parent | dce6bf46952b5dd470ae841cae03706dbc30bc3b (diff) | |
Boogie: Removed some errors with code contracts (commenting out doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
Diffstat (limited to 'Source/AIFramework')
| -rw-r--r-- | Source/AIFramework/AIFramework.csproj | 2 | ||||
| -rw-r--r-- | Source/AIFramework/CommonFunctionSymbols.cs | 14 | ||||
| -rw-r--r-- | Source/AIFramework/Functional.cs | 729 | ||||
| -rw-r--r-- | Source/AIFramework/Lattice.cs | 82 | ||||
| -rw-r--r-- | Source/AIFramework/MultiLattice.cs | 90 | ||||
| -rw-r--r-- | Source/AIFramework/Mutable.cs | 220 | ||||
| -rw-r--r-- | Source/AIFramework/Polyhedra/LinearConstraintSystem.cs | 4 | ||||
| -rw-r--r-- | Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs | 72 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/ConstantAbstraction.cs | 414 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/DynamicTypeLattice.cs | 175 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/Intervals.cs | 363 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/Nullness.cs | 344 | ||||
| -rw-r--r-- | Source/AIFramework/VariableMap/VariableMapLattice.cs | 1505 |
13 files changed, 2039 insertions, 1975 deletions
diff --git a/Source/AIFramework/AIFramework.csproj b/Source/AIFramework/AIFramework.csproj index 0e5804d7..28ad25a9 100644 --- a/Source/AIFramework/AIFramework.csproj +++ b/Source/AIFramework/AIFramework.csproj @@ -12,7 +12,7 @@ <AssemblyName>AIFramework</AssemblyName>
<TargetFrameworkVersion>v3.5</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
- <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+ <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
<SignAssembly>true</SignAssembly>
<AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
</PropertyGroup>
diff --git a/Source/AIFramework/CommonFunctionSymbols.cs b/Source/AIFramework/CommonFunctionSymbols.cs index 2d98e8bc..7dbfdd03 100644 --- a/Source/AIFramework/CommonFunctionSymbols.cs +++ b/Source/AIFramework/CommonFunctionSymbols.cs @@ -297,7 +297,7 @@ void ObjectInvariant() public class Int : Value
{
private static readonly AIType/*!*/ inttype = new Int();
- public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return inttype; } }
+ public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return inttype; } }
private static readonly AIType/*!*/ unaryinttype = new FunctionType(Type, Type);
private static readonly AIType/*!*/ bininttype = new FunctionType(Type, Type, Type);
@@ -341,7 +341,7 @@ Contract.Ensures(Contract.Result<IntSymbol>() != null); public class Double : Value
{
private static readonly AIType/*!*/ doubletype = new Double();
- public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return doubletype; } }
+ public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return doubletype; } }
public static DoubleSymbol/*!*/ Const(double x) {
Contract.Ensures(Contract.Result<DoubleSymbol>() != null);
@@ -359,7 +359,7 @@ Contract.Ensures(Contract.Result<DoubleSymbol>() != null); public class Bv : Value
{
private static readonly AIType/*!*/ bvtype = new Bv();
- public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return bvtype; } }
+ public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return bvtype; } }
private static readonly AIType/*!*/ unaryinttype = new FunctionType(Type, Type);
private static readonly AIType/*!*/ bininttype = new FunctionType(Type, Type, Type);
@@ -407,7 +407,7 @@ Contract.Ensures(Contract.Result<BvSymbol>() != null); public class Ref : Value
{
private static readonly AIType/*!*/ reftype = new Ref();
- public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }
+ public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }
private static readonly FunctionSymbol/*!*/ _null = new FunctionSymbol("null", Type);
@@ -423,7 +423,7 @@ Contract.Ensures(Contract.Result<BvSymbol>() != null); public class HeapStructure : Value
{
private static readonly AIType/*!*/ reftype = new HeapStructure();
- public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }
+ public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }
@@ -437,7 +437,7 @@ Contract.Ensures(Contract.Result<BvSymbol>() != null); public class FieldName : Value
{
private static readonly AIType/*!*/ fieldnametype = new FieldName();
- public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return fieldnametype; } }
+ public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return fieldnametype; } }
private static readonly FunctionSymbol/*!*/ _allocated = new FunctionSymbol("$allocated", FieldName.Type);
public static FunctionSymbol/*!*/ Allocated { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _allocated; } }
@@ -460,7 +460,7 @@ Contract.Requires(f != null); public class Heap : Value
{
private static readonly AIType/*!*/ heaptype = new Heap();
- public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return heaptype; } }
+ public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return heaptype; } }
// the types in the following, select1, select2, are hard-coded; // these types may not always be appropriate
diff --git a/Source/AIFramework/Functional.cs b/Source/AIFramework/Functional.cs index e61adcc1..531ce94f 100644 --- a/Source/AIFramework/Functional.cs +++ b/Source/AIFramework/Functional.cs @@ -5,389 +5,426 @@ //-----------------------------------------------------------------------------
using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework.Collections
-{
- using System.Collections;
+namespace Microsoft.AbstractInterpretationFramework.Collections {
+ using System.Collections;
+
+ /// <summary>Represents a functional collection of key/value pairs.</summary>
+ /// <filterpriority>2</filterpriority>
+ [ContractClass(typeof(IFunctionalMapContracts))]
+ public interface IFunctionalMap : System.Collections.ICollection, System.Collections.IEnumerable {
+ /// <summary>Adds an element with the provided key and value to the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
+ /// <param name="value">The <see cref="T:System.Object" /> to use as the value of the element to add. </param>
+ /// <param name="key">The <see cref="T:System.Object" /> to use as the key of the element to add. </param>
+ /// <filterpriority>2</filterpriority>
+ IFunctionalMap/*!*/ Add(object/*!*/ key, object value);
+
+ /// <summary>
+ /// Set the value of the key (that is already in the map)
+ /// </summary>
+ IFunctionalMap/*!*/ Set(object/*!*/ key, object value);
+
+ /// <summary>Determines whether the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" /> contains an element with the specified key.</summary>
+ /// <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]
+ bool Contains(object/*!*/ key);
+
+ /// <summary>Returns an <see cref="T:System.Collections.IDictionaryEnumerator" /> for the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
+ /// <returns>An <see cref="T:System.Collections.IDictionaryEnumerator" /> for the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</returns>
+ /// <filterpriority>2</filterpriority>
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ new System.Collections.IDictionaryEnumerator GetEnumerator();
- /// <summary>Represents a functional collection of key/value pairs.</summary>
+ /// <summary>Gets an <see cref="T:System.Collections.ICollection" /> containing the keys of the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
+ /// <returns>An <see cref="T:System.Collections.ICollection" /> containing the keys of the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</returns>
/// <filterpriority>2</filterpriority>
- [ContractClass(typeof(IFunctionalMapContracts))]
- public interface IFunctionalMap : System.Collections.ICollection, System.Collections.IEnumerable
- {
- /// <summary>Adds an element with the provided key and value to the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
- /// <param name="value">The <see cref="T:System.Object" /> to use as the value of the element to add. </param>
- /// <param name="key">The <see cref="T:System.Object" /> to use as the key of the element to add. </param>
- /// <filterpriority>2</filterpriority>
- IFunctionalMap/*!*/ Add(object/*!*/ key, object value);
-
- /// <summary>
- /// Set the value of the key (that is already in the map)
- /// </summary>
- IFunctionalMap/*!*/ Set(object/*!*/ key, object value);
-
- /// <summary>Determines whether the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" /> contains an element with the specified key.</summary>
- /// <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]
- bool Contains(object/*!*/ key);
-
- /// <summary>Returns an <see cref="T:System.Collections.IDictionaryEnumerator" /> for the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
- /// <returns>An <see cref="T:System.Collections.IDictionaryEnumerator" /> for the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</returns>
- /// <filterpriority>2</filterpriority>
- [Pure] [GlobalAccess(false)] [Escapes(true,false)]
- new System.Collections.IDictionaryEnumerator GetEnumerator();
-
- /// <summary>Gets an <see cref="T:System.Collections.ICollection" /> containing the keys of the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
- /// <returns>An <see cref="T:System.Collections.ICollection" /> containing the keys of the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</returns>
- /// <filterpriority>2</filterpriority>
- System.Collections.ICollection Keys { get; }
-
- /// <summary>Removes the element with the specified key from the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
- /// <param name="key">The key of the element to remove. </param>
- /// <filterpriority>2</filterpriority>
- IFunctionalMap/*!*/ Remove(object/*!*/ key);
-
- /// <summary>Gets an <see cref="T:System.Collections.ICollection" /> containing the values in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
- /// <returns>An <see cref="T:System.Collections.ICollection" /> containing the values in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</returns>
- /// <filterpriority>2</filterpriority>
- System.Collections.ICollection Values { get; }
-
- object this [object/*!*/ key] { get; /*set;*/ }
+ System.Collections.ICollection Keys {
+ get;
+ }
+
+ /// <summary>Removes the element with the specified key from the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
+ /// <param name="key">The key of the element to remove. </param>
+ /// <filterpriority>2</filterpriority>
+ IFunctionalMap/*!*/ Remove(object/*!*/ key);
+
+ /// <summary>Gets an <see cref="T:System.Collections.ICollection" /> containing the values in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</summary>
+ /// <returns>An <see cref="T:System.Collections.ICollection" /> containing the values in the <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />.</returns>
+ /// <filterpriority>2</filterpriority>
+ System.Collections.ICollection Values {
+ get;
+ }
+
+ object this[object/*!*/ key] {
+ get; /*set;*/
}
+ }
[ContractClassFor(typeof(IFunctionalMap))]
- public abstract class IFunctionalMapContracts:IFunctionalMap{
+ public abstract class IFunctionalMapContracts : IFunctionalMap {
- #region IFunctionalMap Members
+ #region IFunctionalMap Members
-IFunctionalMap IFunctionalMap.Add(object key, object value)
-{
- Contract.Requires(key != null);
- Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
+ IFunctionalMap IFunctionalMap.Add(object key, object value) {
+ Contract.Requires(key != null);
+ Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
- throw new System.NotImplementedException();
-}
+ throw new System.NotImplementedException();
+ }
-IFunctionalMap IFunctionalMap.Set(object key, object value)
-{
- Contract.Requires(key != null);
- Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
+ IFunctionalMap IFunctionalMap.Set(object key, object value) {
+ Contract.Requires(key != null);
+ Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
- throw new System.NotImplementedException();
-}
+ throw new System.NotImplementedException();
+ }
-bool IFunctionalMap.Contains(object key)
-{
- Contract.Requires(key != null);
+ bool IFunctionalMap.Contains(object key) {
+ Contract.Requires(key != null);
- throw new System.NotImplementedException();
-}
+ throw new System.NotImplementedException();
+ }
-IDictionaryEnumerator IFunctionalMap.GetEnumerator()
-{
- throw new System.NotImplementedException();
-}
+ IDictionaryEnumerator IFunctionalMap.GetEnumerator() {
+ throw new System.NotImplementedException();
+ }
-ICollection IFunctionalMap.Keys
-{
- get { throw new System.NotImplementedException(); }
-}
+ ICollection IFunctionalMap.Keys {
+ get {
+ throw new System.NotImplementedException();
+ }
+ }
-IFunctionalMap IFunctionalMap.Remove(object key)
-{
- Contract.Requires(key != null);
- Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
+ IFunctionalMap IFunctionalMap.Remove(object key) {
+ Contract.Requires(key != null);
+ Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
- throw new System.NotImplementedException();
-}
+ throw new System.NotImplementedException();
+ }
-ICollection IFunctionalMap.Values
-{
- get { throw new System.NotImplementedException(); }
-}
+ ICollection IFunctionalMap.Values {
+ get {
+ throw new System.NotImplementedException();
+ }
+ }
-object IFunctionalMap.this[object key]
-{
- get {Contract.Ensures(Contract.Result<object>() != null);
- throw new System.NotImplementedException(); }
-}
+ object IFunctionalMap.this[object key] {
+ get {
+ Contract.Ensures(Contract.Result<object>() != null);
+ throw new System.NotImplementedException();
+ }
+ }
-#endregion
+ #endregion
-#region ICollection Members
+ #region ICollection Members
-void ICollection.CopyTo(System.Array array, int index)
-{
- throw new System.NotImplementedException();
-}
+ void ICollection.CopyTo(System.Array array, int index) {
+ throw new System.NotImplementedException();
+ }
-int ICollection.Count
-{
- get { throw new System.NotImplementedException(); }
-}
+ int ICollection.Count {
+ get {
+ throw new System.NotImplementedException();
+ }
+ }
-bool ICollection.IsSynchronized
-{
- get { throw new System.NotImplementedException(); }
-}
+ bool ICollection.IsSynchronized {
+ get {
+ throw new System.NotImplementedException();
+ }
+ }
-object ICollection.SyncRoot
-{
- get { throw new System.NotImplementedException(); }
-}
+ object ICollection.SyncRoot {
+ get {
+ throw new System.NotImplementedException();
+ }
+ }
-#endregion
+ #endregion
-#region IEnumerable Members
+ #region IEnumerable Members
-IEnumerator IEnumerable.GetEnumerator()
-{
- throw new System.NotImplementedException();
-}
+ IEnumerator IEnumerable.GetEnumerator() {
+ throw new System.NotImplementedException();
+ }
-#endregion
-}
+ #endregion
+ }
+ /// <summary>
+ /// An implementation of the
+ /// <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />
+ /// interface with a <see cref="T:System.Collections.Hashtable" /> as the backing store.
+ /// </summary>
+ class FunctionalHashtable : IFunctionalMap {
+ private readonly Hashtable/*!*/ h;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(h != null);
+ }
+
+
/// <summary>
- /// An implementation of the
- /// <see cref="T:Microsoft.AbstractInterpretationFramework.Collections.IFunctionalMap" />
- /// interface with a <see cref="T:System.Collections.Hashtable" /> as the backing store.
+ /// Cannot directly construct an instance of a FunctionalHashtbl.
/// </summary>
- class FunctionalHashtable : IFunctionalMap
- {
- private readonly Hashtable/*!*/ h;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(h != null);
-}
+ private FunctionalHashtable() {
+ this.h = new Hashtable();
+ // base();
+ }
+
+ /// <summary>
+ /// Cannot directly construct an instance of a FunctionalHashtbl.
+ /// </summary>
+ private FunctionalHashtable(Hashtable/*!*/ h) {
+ Contract.Requires(h != null);
+ this.h = h;
+ // base();
+ }
+
+ private static readonly IFunctionalMap/*!*/ empty = new FunctionalHashtable();
+ public static IFunctionalMap/*!*/ Empty {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
+ return empty;
+ }
+ }
+
+ public IFunctionalMap/*!*/ Add(object/*!*/ key, object value) {
+ //Contract.Requires(key != null);
+ Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
+ Hashtable r = h.Clone() as Hashtable;
+ Contract.Assume(r != null);
+ r.Add(key, value);
+ return new FunctionalHashtable(r);
+ }
+
+ public IFunctionalMap/*!*/ Set(object/*!*/ key, object value) {
+ //Contract.Requires(key != null);
+ Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
+ Hashtable r = h.Clone() as Hashtable;
+ Contract.Assume(r != null);
+ Contract.Assert(this.Contains(key)); // The entry must be defined
- /// <summary>
- /// Cannot directly construct an instance of a FunctionalHashtbl.
- /// </summary>
- private FunctionalHashtable()
- {
- this.h = new Hashtable();
- // base();
- }
-
- /// <summary>
- /// Cannot directly construct an instance of a FunctionalHashtbl.
- /// </summary>
- private FunctionalHashtable(Hashtable/*!*/ h){
-Contract.Requires(h != null);
- this.h = h;
- // base();
- }
-
- private static readonly IFunctionalMap/*!*/ empty = new FunctionalHashtable();
- public static IFunctionalMap/*!*/ Empty { get {Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
- return empty; } }
-
- public IFunctionalMap/*!*/ Add(object/*!*/ key, object value){
-Contract.Requires(key != null);
-Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
- Hashtable r = h.Clone() as Hashtable;
- Contract.Assume(r != null);
- r.Add(key, value);
- return new FunctionalHashtable(r);
- }
-
- public IFunctionalMap/*!*/ Set(object/*!*/ key, object value){
-Contract.Requires(key != null);
-Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
- Hashtable r = h.Clone() as Hashtable;
-
- Contract.Assume(r != null);
- Contract.Assert( this.Contains(key)); // The entry must be defined
-
- r[key] = value; - return new FunctionalHashtable(r);
- }
-
- [Pure]
- public bool Contains(object/*!*/ key){
-Contract.Requires(key != null);
- return h.Contains(key);
- }
-
- [Pure] [GlobalAccess(false)] [Escapes(true,false)]
- IEnumerator/*!*/ IEnumerable.GetEnumerator()
- {
- Contract.Ensures(Contract.Result<IEnumerator>() != null);
-
- 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){
-Contract.Requires(key != null);
-Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
- Hashtable r = h.Clone() as Hashtable;
- Contract.Assume(r != null);
- r.Remove(key);
- return new FunctionalHashtable(r);
- }
-
- public ICollection Values
- {
- get { return h.Values; }
- }
-
-
- public object this[object/*!*/ key]
- {
- get {Contract.Requires(key != null); return h[key]; }
- }
-
- public int Count
- {
- [Pure] get { return h.Count; }
- }
-
- public bool IsSynchronized
- {
- [Pure] get { return h.IsSynchronized; }
- }
-
- public object/*!*/ SyncRoot
- {
- [Pure]
- get {
- Contract.Ensures(Contract.Result<object>() != null);
- return h.SyncRoot;
- }
- }
-
- public void CopyTo(System.Array/*!*/ a, int index){
-Contract.Requires(a != null);
- h.CopyTo(a, index);
- }
- }
-
- public struct Pair/*<T1,T2>*/
- {
- 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;
- }
+ r[key] = value;
+ return new FunctionalHashtable(r);
}
+
+ [Pure]
+ public bool Contains(object/*!*/ key) {
+ //Contract.Requires(key != null);
+ return h.Contains(key);
+ }
+
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ IEnumerator/*!*/ IEnumerable.GetEnumerator() {
+ Contract.Ensures(Contract.Result<IEnumerator>() != null);
+
+ 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) {
+ //Contract.Requires(key != null);
+ Contract.Ensures(Contract.Result<IFunctionalMap>() != null);
+ Hashtable r = h.Clone() as Hashtable;
+ Contract.Assume(r != null);
+ r.Remove(key);
+ return new FunctionalHashtable(r);
+ }
+
+ public ICollection Values {
+ get {
+ return h.Values;
+ }
+ }
+
+
+ public object this[object/*!*/ key] {
+ get {
+ //Contract.Requires(key != null);
+ return h[key];
+ }
+ }
+
+ public int Count {
+ [Pure]
+ get {
+ return h.Count;
+ }
+ }
+
+ public bool IsSynchronized {
+ [Pure]
+ get {
+ return h.IsSynchronized;
+ }
+ }
+
+ public object/*!*/ SyncRoot {
+ [Pure]
+ get {
+ Contract.Ensures(Contract.Result<object>() != null);
+ return h.SyncRoot;
+ }
+ }
+
+ public void CopyTo(System.Array/*!*/ a, int index) {
+ //Contract.Requires(a != null);
+ h.CopyTo(a, index);
+ }
+ }
+
+ public struct Pair/*<T1,T2>*/
+ {
+ 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<T1,T2>
- {
- 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<T1,T2>)) return false;
-
- Pair<T1,T2> other = (Pair<T1,T2>)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() {
-Contract.Ensures(Contract.Result<string>() != null);
- return string.Format("({0},{1})", first, second);
- }
- }
-
- public struct Triple<T1,T2,T3>
- {
- 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<T1,T2,T3>)) return false;
-
- Triple<T1,T2,T3> other = (Triple<T1,T2,T3>)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() {
-Contract.Ensures(Contract.Result<string>() != null);
- return string.Format("({0},{1},{2})", first, second, third);
- }
+namespace Microsoft.AbstractInterpretationFramework.Collections.Generic {
+ using System.Collections.Generic;
+
+ public struct Pair<T1, T2> {
+ 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<T1, T2>))
+ return false;
+
+ Pair<T1, T2> other = (Pair<T1, T2>)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() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return string.Format("({0},{1})", first, second);
+ }
+ }
+
+ public struct Triple<T1, T2, T3> {
+ 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<T1, T2, T3>))
+ return false;
+
+ Triple<T1, T2, T3> other = (Triple<T1, T2, T3>)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() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return string.Format("({0},{1},{2})", first, second, third);
}
+ }
}
diff --git a/Source/AIFramework/Lattice.cs b/Source/AIFramework/Lattice.cs index cb5d3cc7..78f87421 100644 --- a/Source/AIFramework/Lattice.cs +++ b/Source/AIFramework/Lattice.cs @@ -338,8 +338,8 @@ namespace Microsoft.AbstractInterpretationFramework { //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
+ //Contract.Requires(b != null);
+ //Contract.Requires(a != null);
return AtMost(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map);
}
@@ -378,8 +378,8 @@ namespace Microsoft.AbstractInterpretationFramework { //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
+ //Contract.Requires(b != null);
+ //Contract.Requires(a != null);
Contract.Ensures(Contract.Result<Element>() != null);
return NontrivialJoin(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map);
}
@@ -413,8 +413,8 @@ namespace Microsoft.AbstractInterpretationFramework { //!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
+ //Contract.Requires(b != null);
+ //Contract.Requires(a != null);
Contract.Ensures(Contract.Result<Element>() != null);
return Widen(a, IdentityCombineNameMap.Map, b, IdentityCombineNameMap.Map);
}
@@ -498,14 +498,14 @@ namespace Microsoft.AbstractInterpretationFramework { public ISet/*<IVariable!>*//*?*/ GetResultNames(IVariable/*!*/ srcname) {
- Contract.Requires(srcname != null);
+ //Contract.Requires(srcname != null);
ArraySet a = new ArraySet();
a.Add(srcname);
return a;
}
public IVariable/*?*/ GetSourceName(IVariable/*!*/ resname) {
- Contract.Requires(resname != null);
+ //Contract.Requires(resname != null);
return resname;
}
@@ -765,25 +765,25 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable) {
- Contract.Requires(variable != null);
- Contract.Requires(e != null);
+ //Contract.Requires(variable != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
eliminateCount++;
return lattice.Eliminate(e, variable);
}
public override Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
- Contract.Requires(newName != null);
- Contract.Requires(oldName != null);
- Contract.Requires(e != null);
+ //Contract.Requires(newName != null);
+ //Contract.Requires(oldName != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
renameCount++;
return lattice.Rename(e, oldName, newName);
}
public override Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr) {
- Contract.Requires(expr != null);
- Contract.Requires(e != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
constrainCount++;
return lattice.Constrain(e, expr);
@@ -791,7 +791,7 @@ namespace Microsoft.AbstractInterpretationFramework { public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
- Contract.Requires(args != null);
+ //Contract.Requires(args != null);
Contract.Requires(f != null);
understandsCount++;
return lattice.Understands(f, args);
@@ -799,28 +799,28 @@ namespace Microsoft.AbstractInterpretationFramework { public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars) {
- Contract.Requires(prohibitedVars != null);
- Contract.Requires(var != null);
- Contract.Requires(expr != null);
- Contract.Requires(q != null);
- Contract.Requires(e != null);
+ //Contract.Requires(prohibitedVars != null);
+ //Contract.Requires(var != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(q != null);
+ //Contract.Requires(e != null);
equivalentExprCount++;
return lattice.EquivalentExpr(e, q, expr, var, prohibitedVars);
}
public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
- Contract.Requires(pred != null);
- Contract.Requires(e != null);
+ //Contract.Requires(pred != null);
+ //Contract.Requires(e != null);
checkPredicateCount++;
return lattice.CheckPredicate(e, pred);
}
public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
- Contract.Requires(var2 != null);
- Contract.Requires(var1 != null);
- Contract.Requires(e != null);
+ //Contract.Requires(var2 != null);
+ //Contract.Requires(var1 != null);
+ //Contract.Requires(e != null);
checkVariableDisequalityCount++;
return lattice.CheckVariableDisequality(e, var1, var2);
}
@@ -828,14 +828,14 @@ namespace Microsoft.AbstractInterpretationFramework { public override IExpr/*!*/ ToPredicate(Element/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
toPredicateCount++;
return lattice.ToPredicate(e);
}
public override string/*!*/ ToString(Element/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<string>() != null);
return lattice.ToString(e);
}
@@ -855,8 +855,8 @@ namespace Microsoft.AbstractInterpretationFramework { }
protected override bool AtMost(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
+ //Contract.Requires(b != null);
+ //Contract.Requires(a != null);
atMostCount++;
return lattice.LowerThan(a, b);
}
@@ -877,36 +877,36 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override bool IsTop(Element/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
isTopCount++;
return lattice.IsTop(e);
}
public override bool IsBottom(Element/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
isBottomCount++;
return lattice.IsBottom(e);
}
public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
+ //Contract.Requires(b != null);
+ //Contract.Requires(a != null);
Contract.Ensures(Contract.Result<Element>() != null);
joinCount++;
return lattice.NontrivialJoin(a, b);
}
public override Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
+ //Contract.Requires(b != null);
+ //Contract.Requires(a != null);
Contract.Ensures(Contract.Result<Element>() != null);
meetCount++;
return lattice.NontrivialMeet(a, b);
}
public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires(b != null);
- Contract.Requires(a != null);
+ //Contract.Requires(b != null);
+ //Contract.Requires(a != null);
Contract.Ensures(Contract.Result<Element>() != null);
widenCount++;
return lattice.Widen(a, b);
@@ -946,13 +946,13 @@ namespace Microsoft.AbstractInterpretationFramework { }
public Answer CheckPredicate(IExpr/*!*/ pred) {
- Contract.Requires(pred != null);
+ //Contract.Requires(pred != null);
return lattice.CheckPredicate(element, pred);
}
public Answer CheckVariableDisequality(IVariable/*!*/ var1, IVariable/*!*/ var2) {
- Contract.Requires(var2 != null);
- Contract.Requires(var1 != null);
+ //Contract.Requires(var2 != null);
+ //Contract.Requires(var1 != null);
return lattice.CheckVariableDisequality(element, var1, var2);
}
}
diff --git a/Source/AIFramework/MultiLattice.cs b/Source/AIFramework/MultiLattice.cs index e12e2d59..9071bd4c 100644 --- a/Source/AIFramework/MultiLattice.cs +++ b/Source/AIFramework/MultiLattice.cs @@ -69,7 +69,7 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override void Dump(string/*!*/ msg) {
- Contract.Requires(msg != null);
+ //Contract.Requires(msg != null);
System.Console.WriteLine("MultiLattice.Elt.Dump({0})", msg);
Element[] epl = this.elementPerLattice;
if (epl != null) {
@@ -207,7 +207,7 @@ namespace Microsoft.AbstractInterpretationFramework { public override bool IsBottom(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Elt e = (Elt)element;
// The program is errorneous/nonterminating if any subdomain knows it is.
//
@@ -223,7 +223,7 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override bool IsTop(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Elt e = (Elt)element;
if (e.elementPerLattice == null) {
return false;
@@ -240,8 +240,8 @@ namespace Microsoft.AbstractInterpretationFramework { }
protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Elt a = (Elt)first;
Elt b = (Elt)second;
@@ -261,10 +261,10 @@ namespace Microsoft.AbstractInterpretationFramework { }
protected override bool AtMost(Element/*!*/ first, ICombineNameMap/*!*/ firstToResult, Element/*!*/ second, ICombineNameMap/*!*/ secondToResult) {
- Contract.Requires(secondToResult != null);
- Contract.Requires(second != null);
- Contract.Requires(firstToResult != null);
- Contract.Requires(first != null);
+ //Contract.Requires(secondToResult != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(firstToResult != null);
+ //Contract.Requires(first != null);
Elt a = (Elt)first;
Elt b = (Elt)second;
@@ -336,48 +336,48 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override Element/*!*/ NontrivialJoin(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires((b != null));
- Contract.Requires((a != null));
+ //Contract.Requires((b != null));
+ //Contract.Requires((a != null));
Contract.Ensures(Contract.Result<Element>() != null);
return this.Combine(a, null, b, null, CombineOp.Join);
}
public override Element/*!*/ NontrivialJoin(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {
- Contract.Requires((bToResult != null));
- Contract.Requires((b != null));
- Contract.Requires((aToResult != null));
- Contract.Requires((a != null));
+ //Contract.Requires((bToResult != null));
+ //Contract.Requires((b != null));
+ //Contract.Requires((aToResult != null));
+ //Contract.Requires((a != null));
Contract.Ensures(Contract.Result<Element>() != null);
return this.Combine(a, aToResult, b, bToResult, CombineOp.Join);
}
public override Element/*!*/ NontrivialMeet(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires((b != null));
- Contract.Requires((a != null));
+ //Contract.Requires((b != null));
+ //Contract.Requires((a != null));
Contract.Ensures(Contract.Result<Element>() != null);
return this.Combine(a, null, b, null, CombineOp.Meet);
}
public override Element/*!*/ Widen(Element/*!*/ a, Element/*!*/ b) {
- Contract.Requires((b != null));
- Contract.Requires((a != null));
+ //Contract.Requires((b != null));
+ //Contract.Requires((a != null));
Contract.Ensures(Contract.Result<Element>() != null);
return this.Combine(a, null, b, null, CombineOp.Widen);
}
public override Element/*!*/ Widen(Element/*!*/ a, ICombineNameMap/*!*/ aToResult, Element/*!*/ b, ICombineNameMap/*!*/ bToResult) {
- Contract.Requires((bToResult != null));
- Contract.Requires((b != null));
- Contract.Requires((aToResult != null));
+ //Contract.Requires((bToResult != null));
+ //Contract.Requires((b != null));
+ //Contract.Requires((aToResult != null));
- Contract.Requires(a != null);
+ //Contract.Requires(a != null);
Contract.Ensures(Contract.Result<Element>() != null);
return this.Combine(a, aToResult, b, bToResult, CombineOp.Widen);
}
public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable) {
- Contract.Requires(variable != null);
- Contract.Requires(element != null);
+ //Contract.Requires(variable != null);
+ //Contract.Requires(element != null);
Contract.Ensures(Contract.Result<Element>() != null);
Elt e = (Elt)element;
if (IsBottom(e)) {
@@ -392,9 +392,9 @@ namespace Microsoft.AbstractInterpretationFramework { public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr) {
- Contract.Requires(expr != null);
- Contract.Requires(element != null);
- Contract.Ensures(Contract.Result<Element>() != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(element != null);
+ //Contract.Ensures(Contract.Result<Element>() != null);
Elt e = (Elt)element;
if (IsBottom(e)) {
return e;
@@ -408,9 +408,9 @@ namespace Microsoft.AbstractInterpretationFramework { public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
- Contract.Requires(newName != null);
- Contract.Requires(oldName != null);
- Contract.Requires(element != null);
+ //Contract.Requires(newName != null);
+ //Contract.Requires(oldName != null);
+ //Contract.Requires(element != null);
Contract.Ensures(Contract.Result<Element>() != null);
Elt e = (Elt)element;
if (IsBottom(e)) {
@@ -425,8 +425,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
- Contract.Requires(args != null);
- Contract.Requires(f != null);
+ //Contract.Requires(args != null);
+ //Contract.Requires(f != null);
bool result = false;
for (int i = 0; i < this.lattices.Count; i++) {
@@ -438,7 +438,7 @@ namespace Microsoft.AbstractInterpretationFramework { public override string/*!*/ ToString(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Contract.Ensures(Contract.Result<string>() != null);
Elt e = (Elt)element;
return e.ToString();
@@ -446,7 +446,7 @@ namespace Microsoft.AbstractInterpretationFramework { public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
Elt e = (Elt)element;
@@ -476,11 +476,11 @@ namespace Microsoft.AbstractInterpretationFramework { /// or null if not possible.
/// </returns>
public override IExpr/*?*/ EquivalentExpr(Element/*!*/ element, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, Set/*<IVariable!>*//*!*/ prohibitedVars) {
- Contract.Requires(prohibitedVars != null);
- Contract.Requires(var != null);
- Contract.Requires(expr != null);
- Contract.Requires(q != null);
- Contract.Requires(element != null);
+ //Contract.Requires(prohibitedVars != null);
+ //Contract.Requires(var != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(q != null);
+ //Contract.Requires(element != null);
Elt/*!*/ e = (Elt/*!*/)cce.NonNull(element);
for (int i = 0; i < e.Count; i++) {
@@ -495,8 +495,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override Answer CheckPredicate(Element/*!*/ element, IExpr/*!*/ pred) {
- Contract.Requires(pred != null);
- Contract.Requires(element != null);
+ //Contract.Requires(pred != null);
+ //Contract.Requires(element != null);
Elt/*!*/ e = (Elt/*!*/)cce.NonNull(element);
for (int i = 0; i < e.Count; i++) {
@@ -511,9 +511,9 @@ namespace Microsoft.AbstractInterpretationFramework { public override Answer CheckVariableDisequality(Element/*!*/ element, IVariable/*!*/ var1, IVariable/*!*/ var2) {
- Contract.Requires(var2 != null);
- Contract.Requires(var1 != null);
- Contract.Requires(element != null);
+ //Contract.Requires(var2 != null);
+ //Contract.Requires(var1 != null);
+ //Contract.Requires(element != null);
Elt/*!*/ e = (Elt/*!*/)cce.NonNull(element);
for (int i = 0; i < e.Count; i++) {
diff --git a/Source/AIFramework/Mutable.cs b/Source/AIFramework/Mutable.cs index f24b65c6..232909e4 100644 --- a/Source/AIFramework/Mutable.cs +++ b/Source/AIFramework/Mutable.cs @@ -4,126 +4,134 @@ //
//-----------------------------------------------------------------------------
using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework.Collections
-{
- using System.Collections; - using System.Diagnostics.Contracts;
+namespace Microsoft.AbstractInterpretationFramework.Collections {
+ using System.Collections;
+ using System.Diagnostics.Contracts;
+
+ /// <summary>
+ /// Extend sets for using as a IWorkList.
+ /// </summary>
+ 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.
+ public override int Count {
+ get {
+ return base.Count;
+ }
+ }
+
+ [Pure]
+ public bool IsEmpty() {
+ return Count == 0;
+ }
/// <summary>
- /// Extend sets for using as a IWorkList.
+ /// Pull an element out of the workset.
/// </summary>
- 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.
- public override int Count { get { return base.Count; } }
-
- [Pure] public bool IsEmpty()
- {
- return Count == 0;
- }
+ public object Pull() {
+ IEnumerator iter = GetEnumerator();
+ iter.MoveNext();
- /// <summary>
- /// Pull an element out of the workset.
- /// </summary>
- public object Pull()
- {
- IEnumerator iter = GetEnumerator();
- iter.MoveNext();
+ object result = cce.NonNull(iter.Current);
+ Remove(result);
- object result = cce.NonNull(iter.Current);
- Remove(result);
+ return 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){
-Contract.Requires(a != null);
- 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 {Contract.Ensures(Contract.Result<object>() != null);
- return this; } }
- public bool IsSynchronized { get { return false; } }
-
+ 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) {
+ //Contract.Requires(a != null);
+ 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 {
+ Contract.Ensures(Contract.Result<object>() != null);
+ return this;
+ }
+ }
+ public bool IsSynchronized {
+ get {
+ return false;
+ }
}
+
+ }
}
-namespace Microsoft.AbstractInterpretationFramework.Collections.Generic
-{
- using System.Collections.Generic;
+namespace Microsoft.AbstractInterpretationFramework.Collections.Generic {
+ using System.Collections.Generic;
- public class HashMultiset<T>
- {
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(dict != null);
- }
+ public class HashMultiset<T> {
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(dict != null);
+ }
- private readonly IDictionary<T,int>/*!*/ dict;
-
- //Contract.Invariant(Contract.ForAll(dict , entry => entry.Value >= 1));
-
- public HashMultiset()
- {
- this.dict = new Dictionary<T,int>();
- // base();
+ private readonly IDictionary<T, int>/*!*/ dict;
+
+ //Contract.Invariant(Contract.ForAll(dict , entry => entry.Value >= 1));
+
+ public HashMultiset() {
+ this.dict = new Dictionary<T, int>();
+ // base();
+ }
+
+ public HashMultiset(int size) {
+ this.dict = new Dictionary<T, int>(size);
+ // base();
+ }
+
+ public void Add(T t) {
+ cce.BeginExpose(this);
+ {
+ if (dict.ContainsKey(t)) {
+ dict[t] = dict[t] + 1;
+ } else {
+ dict.Add(t, 1);
}
-
- public HashMultiset(int size)
+ }
+ cce.EndExpose();
+ }
+
+ public void Remove(T t) {
+ if (dict.ContainsKey(t)) {
+ cce.BeginExpose(this);
{
- this.dict = new Dictionary<T,int>(size);
- // base();
- }
-
- public void Add(T t) {
- cce.BeginExpose(this);
- {
- if (dict.ContainsKey(t))
- {
- dict[t] = dict[t] + 1;
- }
- else
- {
- dict.Add(t,1);
- }
+ int count = dict[t];
+ if (count == 1) {
+ dict.Remove(t);
+ } else {
+ dict[t] = count - 1;
}
- cce.EndExpose();
- }
-
- public void Remove(T t)
- {
- if (dict.ContainsKey(t))
- { cce.BeginExpose(this); {
- int count = dict[t];
- if (count == 1) { dict.Remove(t); }
- else { dict[t] = count - 1; }
- }
- cce.EndExpose();
- }
- }
-
- public bool Contains(T t)
- {
- return dict.ContainsKey(t);
}
+ cce.EndExpose();
+ }
+ }
+
+ public bool Contains(T t) {
+ return dict.ContainsKey(t);
}
+ }
}
diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs index 8e5fdf86..c259febe 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs +++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs @@ -1002,7 +1002,7 @@ Contract.Requires(oldName != null); }
[Pure]
public object DoVisit(ExprVisitor/*!*/ visitor) {
- Contract.Requires(visitor != null);
+ //Contract.Requires(visitor != null);
return visitor.VisitVariable(this);
}
}
@@ -1592,7 +1592,7 @@ Contract.Requires(oldName != null); }
[Pure]
public object DoVisit(ExprVisitor/*!*/ visitor) {
- Contract.Requires(visitor != null);
+ //Contract.Requires(visitor != null);
return visitor.VisitVariable(this);
}
}
diff --git a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs index 60aceb7f..44abfed6 100644 --- a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs +++ b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs @@ -48,7 +48,7 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override void Dump(string/*!*/ msg) {
- Contract.Requires(msg != null);
+ //Contract.Requires(msg != null);
System.Console.WriteLine("PolyhedraLatticeElement.Dump({0}):", msg);
lcs.Dump();
}
@@ -107,13 +107,13 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override bool IsBottom(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
return e.lcs.IsBottom();
}
public override bool IsTop(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
return e.lcs.IsTop();
}
@@ -126,8 +126,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// <returns></returns>
protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
{
- Contract.Requires(first != null);
- Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ //Contract.Requires(second != null);
PolyhedraLatticeElement a = (PolyhedraLatticeElement)first;
PolyhedraLatticeElement b = (PolyhedraLatticeElement)second;
return b.lcs.IsSubset(a.lcs);
@@ -135,13 +135,13 @@ namespace Microsoft.AbstractInterpretationFramework { public override string/*!*/ ToString(Element/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<string>() != null);
return ((PolyhedraLatticeElement)e).lcs.ToString();
}
public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
return e.lcs.ConvertToExpression(factory);
@@ -150,8 +150,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override Lattice.Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Lattice.Element>() != null);
log.DbgMsg("Joining ...");
log.DbgMsgIndent();
@@ -165,8 +165,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override Lattice.Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Lattice.Element>() != null);
PolyhedraLatticeElement aa = (PolyhedraLatticeElement)first;
PolyhedraLatticeElement bb = (PolyhedraLatticeElement)second;
@@ -175,8 +175,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override Lattice.Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Lattice.Element>() != null);
log.DbgMsg("Widening ...");
log.DbgMsgIndent();
@@ -192,8 +192,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable) {
- Contract.Requires(variable != null);
- Contract.Requires(e != null);
+ //Contract.Requires(variable != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
log.DbgMsg(string.Format("Eliminating {0} ...", variable));
@@ -206,9 +206,9 @@ namespace Microsoft.AbstractInterpretationFramework { public override Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
- Contract.Requires(newName != null);
- Contract.Requires(oldName != null);
- Contract.Requires(e != null);
+ //Contract.Requires(newName != null);
+ //Contract.Requires(oldName != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
log.DbgMsg(string.Format("Renaming {0} to {1} in {2} ...", oldName, newName, this.ToString(e)));
@@ -220,8 +220,8 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
- Contract.Requires(args != null);
- Contract.Requires(f != null);
+ //Contract.Requires(args != null);
+ //Contract.Requires(f != null);
return f is IntSymbol ||
f.Equals(Int.Add) ||
f.Equals(Int.Sub) ||
@@ -237,9 +237,9 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
- Contract.Requires(var2 != null);
- Contract.Requires(var1 != null);
- Contract.Requires(e != null);
+ //Contract.Requires(var2 != null);
+ //Contract.Requires(var1 != null);
+ //Contract.Requires(e != null);
PolyhedraLatticeElement/*!*/ ple = (PolyhedraLatticeElement)cce.NonNull(e);
Contract.Assume(ple.lcs.Constraints != null);
ArrayList /*LinearConstraint!*//*!*/ clist = (ArrayList /*LinearConstraint!*/)cce.NonNull(ple.lcs.Constraints.Clone());
@@ -257,8 +257,8 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
- Contract.Requires(pred != null);
- Contract.Requires(e != null);
+ //Contract.Requires(pred != null);
+ //Contract.Requires(e != null);
PolyhedraLatticeElement/*!*/ ple = (PolyhedraLatticeElement)Constrain(e, pred);
Contract.Assert(ple != null);
if (ple.lcs.IsBottom()) {
@@ -295,7 +295,7 @@ namespace Microsoft.AbstractInterpretationFramework { [Pure]
public object DoVisit(ExprVisitor/*!*/ visitor) {
- Contract.Requires(visitor != null);
+ //Contract.Requires(visitor != null);
return visitor.VisitFunApp(this);
}
@@ -316,7 +316,7 @@ namespace Microsoft.AbstractInterpretationFramework { }
public IFunApp/*!*/ CloneWithArguments(IList/*<IExpr!>*//*!*/ args) {
- Contract.Requires(args != null);
+ //Contract.Requires(args != null);
Contract.Ensures(Contract.Result<IFunApp>() != null);
Contract.Assert(args.Count == 1);
return new PolyhedraLatticeNegation((IExpr/*!*/)cce.NonNull(args[0]));
@@ -324,19 +324,19 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars) {
- Contract.Requires(prohibitedVars != null);
- Contract.Requires(var != null);
- Contract.Requires(expr != null);
- Contract.Requires(q != null);
- Contract.Requires(e != null);
+ //Contract.Requires(prohibitedVars != null);
+ //Contract.Requires(var != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(q != null);
+ //Contract.Requires(e != null);
// BUGBUG: TODO: this method can be implemented in a more precise way
return null;
}
public override Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr) {
- Contract.Requires(expr != null);
- Contract.Requires(e != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
log.DbgMsg(string.Format("Constraining with {0} into {1} ...", expr, this.ToString(e)));
@@ -387,7 +387,7 @@ namespace Microsoft.AbstractInterpretationFramework { class LCBottom : LinearCondition {
public override void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist) {
- Contract.Requires(clist != null);
+ //Contract.Requires(clist != null);
// make an unsatisfiable constraint
LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
lc.rhs = Rational.FromInt(1);
@@ -415,7 +415,7 @@ namespace Microsoft.AbstractInterpretationFramework { this.constraint = constraint;
}
public override void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist) {
- Contract.Requires(clist != null);
+ //Contract.Requires(clist != null);
if (positive) {
clist.Add(constraint);
} else {
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.cs b/Source/AIFramework/VariableMap/ConstantAbstraction.cs index 89a64290..d8f17a3c 100644 --- a/Source/AIFramework/VariableMap/ConstantAbstraction.cs +++ b/Source/AIFramework/VariableMap/ConstantAbstraction.cs @@ -4,230 +4,248 @@ //
//-----------------------------------------------------------------------------
using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System.Collections;
- using System.Diagnostics;
- //using System.Compiler.Analysis;
- using Microsoft.Basetypes;
+namespace Microsoft.AbstractInterpretationFramework {
+ using System.Collections;
+ using System.Diagnostics;
+ //using System.Compiler.Analysis;
+ using Microsoft.Basetypes;
+
+ /// <summary>
+ /// Represents an invariant over constant variable assignments.
+ /// </summary>
+ public class ConstantLattice : MicroLattice {
+ enum Value {
+ Top,
+ Bottom,
+ Constant
+ }
- /// <summary>
- /// Represents an invariant over constant variable assignments.
- /// </summary>
- public class ConstantLattice : MicroLattice
- {
- enum Value { Top, Bottom, Constant }
+ private class Elt : Element {
+ public Value domainValue;
+ public BigNum constantValue; // valid iff domainValue == Value.Constant
- private class Elt : Element
- {
- public Value domainValue;
- public BigNum constantValue; // valid iff domainValue == Value.Constant
+ public Elt(Value v) {
+ this.domainValue = v;
+ }
- public Elt (Value v) { this.domainValue = v; }
+ public Elt(BigNum i) {
+ this.domainValue = Value.Constant;
+ this.constantValue = i;
+ }
- public Elt (BigNum i) { this.domainValue = Value.Constant; this.constantValue = i; }
+ public bool IsConstant {
+ get {
+ return this.domainValue == Value.Constant;
+ }
+ }
- public bool IsConstant { get { return this.domainValue == Value.Constant; } }
+ public BigNum Constant {
+ get {
+ return this.constantValue;
+ }
+ } // only when IsConstant
- public BigNum Constant { get { return this.constantValue; } } // only when IsConstant
+ [Pure]
+ public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+ return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
+ }
- [Pure]
- public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
-return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
- }
-
- public override Element/*!*/ Clone() {
-Contract.Ensures(Contract.Result<Element>() != null);
- if (this.IsConstant)
- return new Elt(constantValue);
- else
- return new Elt(domainValue);
- }
- }
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ if (this.IsConstant)
+ return new Elt(constantValue);
+ else
+ return new Elt(domainValue);
+ }
+ }
- readonly IIntExprFactory/*!*/ factory;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(factory != null);
- }
+ readonly IIntExprFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
- public ConstantLattice(IIntExprFactory/*!*/ factory){
-Contract.Requires(factory != null);
- this.factory = factory;
- // base();
- }
+ public ConstantLattice(IIntExprFactory/*!*/ factory) {
+ Contract.Requires(factory != null);
+ this.factory = factory;
+ // base();
+ }
- public override Element/*!*/ Top{get{
-Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.Top); }
- }
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Top);
+ }
+ }
- public override Element/*!*/ Bottom{get{
-Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.Bottom); }
- }
+ public override Element/*!*/ Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Bottom);
+ }
+ }
- public override bool IsTop (Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- return e.domainValue == Value.Top; - }
+ public override bool IsTop(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return e.domainValue == Value.Top;
+ }
- public override bool IsBottom (Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- return e.domainValue == Value.Bottom; - }
+ public override bool IsBottom(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return e.domainValue == Value.Bottom;
+ }
- public override Element/*!*/ NontrivialJoin (Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- 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/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ 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){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- 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){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- return Join(first,second);
- }
+ public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ 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;
+ }
- protected override bool AtMost (Element/*!*/ first, Element/*!*/ second) // this <= that
- {
- Contract.Requires(first!= null);
- Contract.Requires(second != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- return a.Constant.Equals(b.Constant);
- }
+ public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return Join(first, second);
+ }
- public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element){
-Contract.Requires(element != null);
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- return factory.Eq(var, cce.NonNull(GetFoldExpr(element)));
- }
+ protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
+ {
+ //Contract.Requires(first!= null);
+ //Contract.Requires(second != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ return a.Constant.Equals(b.Constant);
+ }
- public override IExpr GetFoldExpr(Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- Contract.Assert(e.domainValue == Value.Constant);
- return factory.Const(e.constantValue);
- }
+ public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ //Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ return factory.Eq(var, cce.NonNull(GetFoldExpr(element)));
+ }
- public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args){
-Contract.Requires(args != null);
-Contract.Requires(f != null);
- return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- }
+ public override IExpr GetFoldExpr(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ Contract.Assert(e.domainValue == Value.Constant);
+ return factory.Const(e.constantValue);
+ }
- public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e){
-Contract.Requires(e != null);
-Contract.Ensures(Contract.Result<Element>() != null);
-
- IFunApp nary = e as IFunApp;
- if (nary != null) {
- if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
- IList/*<IExpr!>*//*!*/ args = nary.Arguments;
- Contract.Assert(args != null);
- Contract.Assert(args.Count == 2);
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
- IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(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;
- }
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
+ //Contract.Requires(args != null);
+ //Contract.Requires(f != null);
+ return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ }
- /// <summary>
- /// Returns true if "expr" represents a constant integer expressions, in which case
- /// "z" returns as that integer. Otherwise, returns false, in which case "z" should
- /// not be used by the caller.
- ///
- /// This method throws an System.ArithmeticException in the event that folding the
- /// constant expression results in an arithmetic overflow or division by zero.
- /// </summary>
- private bool Fold(IExpr/*!*/ expr, out BigNum z){
-Contract.Requires(expr != null);
- IFunApp e = expr as IFunApp;
- if (e == null) {
- z = BigNum.ZERO;
- return false;
+ public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
+ //Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+
+ IFunApp nary = e as IFunApp;
+ if (nary != null) {
+ if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
+ IList/*<IExpr!>*//*!*/ args = nary.Arguments;
+ Contract.Assert(args != null);
+ Contract.Assert(args.Count == 2);
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+ IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(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;
+ }
- if (e.FunctionSymbol is IntSymbol) {
- z = ((IntSymbol)e.FunctionSymbol).Value;
- return true;
-
- } else if (e.FunctionSymbol.Equals(Int.Negate)) {
- IList/*<IExpr!>*//*!*/ args = e.Arguments;
- Contract.Assert(args != null);
- Contract.Assert(args.Count == 1);
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-
- if (Fold(arg0, out z)) {
- z = z.Neg;
- return true;
- }
-
- } else if (e.Arguments.Count == 2) {
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(e.Arguments[0]);
- IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(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;
- }
- }
-
+ /// <summary>
+ /// Returns true if "expr" represents a constant integer expressions, in which case
+ /// "z" returns as that integer. Otherwise, returns false, in which case "z" should
+ /// not be used by the caller.
+ ///
+ /// This method throws an System.ArithmeticException in the event that folding the
+ /// constant expression results in an arithmetic overflow or division by zero.
+ /// </summary>
+ private bool Fold(IExpr/*!*/ expr, out BigNum z) {
+ Contract.Requires(expr != null);
+ IFunApp e = expr as IFunApp;
+ if (e == null) {
+ z = BigNum.ZERO;
+ return false;
+ }
+
+ if (e.FunctionSymbol is IntSymbol) {
+ z = ((IntSymbol)e.FunctionSymbol).Value;
+ return true;
+
+ } else if (e.FunctionSymbol.Equals(Int.Negate)) {
+ IList/*<IExpr!>*//*!*/ args = e.Arguments;
+ Contract.Assert(args != null);
+ Contract.Assert(args.Count == 1);
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+
+ if (Fold(arg0, out z)) {
+ z = z.Neg;
+ return true;
+ }
+
+ } else if (e.Arguments.Count == 2) {
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(e.Arguments[0]);
+ IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(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/DynamicTypeLattice.cs b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs index 84525a15..78bd61a0 100644 --- a/Source/AIFramework/VariableMap/DynamicTypeLattice.cs +++ b/Source/AIFramework/VariableMap/DynamicTypeLattice.cs @@ -163,100 +163,101 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override bool IsTop(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Elt e = (Elt)element;
return e.what == What.Bounds && e.ty == null && e.manyBounds == null;
}
public override bool IsBottom(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Elt e = (Elt)element;
return e.what == What.Bottom;
}
- public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
- if (a.what == What.Exact && b.what == What.Exact) {
- Contract.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));
- }
- }
+ public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
+ if (a.what == What.Exact && b.what == What.Exact) {
+ Contract.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.
- Contract.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) {
- Contract.Assert(a.ty != null && b.ty != null);
- IExpr join = factory.JoinTypes(a.ty, b.ty);
- Contract.Assert(join != null);
- 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);
- }
- }
+ // The result is going to be a Bounds, since at least one of the operands is a Bounds.
+ Contract.Assert(1 <= a.BoundsCount && 1 <= b.BoundsCount); // a preconditions is that neither operand is Top
+ int n = a.BoundsCount + b.BoundsCount;
- // 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(cce.NonNull(a.manyBounds));
- }
- int bStart = allBounds.Count;
- if (b.ty != null) {
- allBounds.Add(b.ty);
+ // Special case: a and b each has exactly one bound
+ if (n == 2) {
+ Contract.Assert(a.ty != null && b.ty != null);
+ IExpr join = factory.JoinTypes(a.ty, b.ty);
+ Contract.Assert(join != null);
+ 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(cce.NonNull(a.manyBounds));
+ }
+ int bStart = allBounds.Count;
+ if (b.ty != null) {
+ allBounds.Add(b.ty);
+ } else {
+ allBounds.AddRange(cce.NonNull(b.manyBounds));
+ }
+ // compute the join of each pair, putting non-redundant joins into "result"
+ for (int i = 0; i < bStart; i++) {
+ IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);
+ for (int j = bStart; j < allBounds.Count; j++) {
+ IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);
+
+ IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);
+ Contract.Assert(join != null);
+
+ int k = 0;
+ while (k < result.Count) {
+ IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(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 {
- allBounds.AddRange(cce.NonNull(b.manyBounds));
+ k++;
}
- // compute the join of each pair, putting non-redundant joins into "result"
- for (int i = 0; i < bStart; i++) {
- IExpr/*!*/ aBound = cce.NonNull((IExpr/*!*/)allBounds[i]);
- for (int j = bStart; j < allBounds.Count; j++) {
- IExpr/*!*/ bBound = (IExpr/*!*/)cce.NonNull(allBounds[j]);
-
- IExpr/*!*/ join = factory.JoinTypes(aBound, bBound);
- Contract.Assert(join != null);
-
- int k = 0;
- while (k < result.Count) {
- IExpr/*!*/ r = (IExpr/*!*/)cce.NonNull(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);
+ }
+ result.Add(join);
+ NEXT_PAIR: {
+ }
}
+ }
+ return new Elt(result, result.Count);
+ }
public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Element>() != null);
Elt a = (Elt)first;
Elt b = (Elt)second;
@@ -359,16 +360,16 @@ Contract.Ensures(Contract.Result<Element>() != null); }
public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Element>() != null);
return Join(first, second);
}
protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
{
- Contract.Requires(first != null);
- Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ //Contract.Requires(second != null);
Elt/*!*/ a = (Elt/*!*/)cce.NonNull(first);
Elt/*!*/ b = (Elt/*!*/)cce.NonNull(second);
Contract.Assert(a.what != What.Bottom && b.what != What.Bottom);
@@ -403,8 +404,8 @@ Contract.Ensures(Contract.Result<Element>() != null); }
public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
- Contract.Requires(element != null);
- Contract.Requires(var != null);
+ //Contract.Requires(element != null);
+ //Contract.Requires(var != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
Elt e = (Elt)element;
switch (e.what) {
@@ -433,14 +434,14 @@ Contract.Ensures(Contract.Result<Element>() != null); }
public override IExpr GetFoldExpr(Element/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
// cannot fold into an expression that can be substituted for the variable
return null;
}
public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
- Contract.Requires(args != null);
- Contract.Requires(f != null);
+ //Contract.Requires(args != null);
+ //Contract.Requires(f != null);
bool isEq = f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
if (isEq || f.Equals(Microsoft.AbstractInterpretationFramework.Value.Subtype)) {
Contract.Assert(args.Count == 2);
@@ -470,7 +471,7 @@ Contract.Ensures(Contract.Result<Element>() != null); }
public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
IFunApp nary = e as IFunApp;
if (nary != null) {
diff --git a/Source/AIFramework/VariableMap/Intervals.cs b/Source/AIFramework/VariableMap/Intervals.cs index 73a1352f..0bf82cf4 100644 --- a/Source/AIFramework/VariableMap/Intervals.cs +++ b/Source/AIFramework/VariableMap/Intervals.cs @@ -55,7 +55,7 @@ namespace Microsoft.AbstractInterpretationFramework { /// The paramter is the top?
/// </summary>
public override bool IsTop(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
IntervalElement interval = (IntervalElement)element;
return interval.IsTop();
@@ -65,7 +65,7 @@ namespace Microsoft.AbstractInterpretationFramework { /// The parameter is the bottom?
/// </summary>
public override bool IsBottom(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
IntervalElement interval = (IntervalElement)element;
return interval.IsBottom();
@@ -75,8 +75,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// The classic, pointwise, join of intervals
/// </summary>
public override Element/*!*/ NontrivialJoin(Element/*!*/ left, Element/*!*/ right) {
- Contract.Requires(right != null);
- Contract.Requires(left != null);
+ //Contract.Requires(right != null);
+ //Contract.Requires(left != null);
Contract.Ensures(Contract.Result<Element>() != null);
IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
@@ -93,8 +93,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// The classic, pointwise, meet of intervals
/// </summary>
public override Element/*!*/ NontrivialMeet(Element/*!*/ left, Element/*!*/ right) {
- Contract.Requires(right != null);
- Contract.Requires(left != null);
+ //Contract.Requires(right != null);
+ //Contract.Requires(left != null);
Contract.Ensures(Contract.Result<Element>() != null);
IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
@@ -111,8 +111,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// left is the PREVIOUS value in the iterations and right is the NEW one
/// </summary>
public override Element/*!*/ Widen(Element/*!*/ left, Element/*!*/ right) {
- Contract.Requires(right != null);
- Contract.Requires(left != null);
+ //Contract.Requires(right != null);
+ //Contract.Requires(left != null);
Contract.Ensures(Contract.Result<Element>() != null);
IntervalElement/*!*/ prevInterval = (IntervalElement/*!*/)cce.NonNull(left);
IntervalElement/*!*/ nextInterval = (IntervalElement/*!*/)cce.NonNull(right);
@@ -130,8 +130,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// Return true iff the interval left is containted in right
/// </summary>
protected override bool AtMost(Element/*!*/ left, Element/*!*/ right) {
- Contract.Requires(right != null);
- Contract.Requires(left != null);
+ //Contract.Requires(right != null);
+ //Contract.Requires(left != null);
IntervalElement/*!*/ leftInterval = (IntervalElement/*!*/)cce.NonNull(left);
IntervalElement/*!*/ rightInterval = (IntervalElement/*!*/)cce.NonNull(right);
@@ -145,50 +145,48 @@ namespace Microsoft.AbstractInterpretationFramework { /// Return just null
/// </summary>
public override IExpr GetFoldExpr(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
return null;
}
/// <summary>
/// return a predicate inf "\leq x and x "\leq" sup (if inf [or sup] is not oo)
/// </summary>
- public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element){
-Contract.Requires(element != null);
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
-IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element); + public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ //Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element);
IExpr lowerBound = null;
- IExpr upperBound = null; + IExpr upperBound = null;
- if(! (interval.Inf is InfinitaryInt))
- {
+ 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))
- {
+ 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)
+ if (lowerBound != null && upperBound != null)
return this.factory.And(lowerBound, upperBound); // inf <= var && var <= sup
else
- if(lowerBound != null)
+ 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;
+ else
+ if (upperBound != null)
+ return upperBound;
+ else // If we reach this point, both lowerBound and upperBound are null, i.e. we have no bounds on var, so we return simply true...
+ return this.factory.True;
}
/// <summary>
/// For the moment consider just equalities. Other case must be considered
/// </summary>
public override bool Understands(IFunctionSymbol/*!*/ f, IList /*<IExpr*//*!*/ args) {
- Contract.Requires(args != null);
- Contract.Requires(f != null);
+ //Contract.Requires(args != null);
+ //Contract.Requires(f != null);
return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
}
@@ -197,7 +195,7 @@ IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element); /// Evaluate the predicate passed as input according the semantics of intervals
/// </summary>
public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ pred) {
- Contract.Requires(pred != null);
+ //Contract.Requires(pred != null);
Contract.Ensures(Contract.Result<Element>() != null);
return this.EvaluatePredicateWithState(pred, null);
}
@@ -206,14 +204,13 @@ IntervalElement/*!*/ interval = (IntervalElement/*!*/)cce.NonNull(element); /// Evaluate the predicate passed as input according the semantics of intervals and the given state.
/// Right now just basic arithmetic operations are supported. A future extension may consider an implementation of boolean predicates
/// </summary>
- public override Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ pred, IFunctionalMap/* Var -> Element */ state){
-Contract.Requires(pred != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- if(pred is IFunApp)
- {
- IFunApp fun = (IFunApp) pred;
- if(fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
- {
+ public override Element/*!*/ EvaluatePredicateWithState(IExpr/*!*/ pred, IFunctionalMap/* Var -> Element */ state) {
+ //Contract.Requires(pred != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ 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/*!*/)cce.NonNull(fun.Arguments[0]);
IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
if (leftArg is IVariable) {
@@ -221,78 +218,72 @@ Contract.Ensures(Contract.Result<Element>() != null); } else if (rightArg is IVariable) {
return Eval(leftArg, state);
}
- }
+ }
}
// otherwise we simply return Top
- return IntervalElement.Top; + return IntervalElement.Top;
}
/// <summary>
/// Evaluate the expression (that is assured to be an arithmetic expression, in the state passed as a parameter
/// </summary>
private IntervalElement/*!*/ Eval(IExpr/*!*/ exp, IFunctionalMap/* Var -> Element */ state) {
-Contract.Requires((exp != null));
-Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ Contract.Requires((exp != null));
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
IntervalElement/*!*/ retVal = (IntervalElement/*!*/)cce.NonNull(Top);
// Eval the expression by structural induction
- if(exp is IVariable && state != null) // A variable
+ if (exp is IVariable && state != null) // A variable
{
object lookup = state[exp];
- if(lookup is IntervalElement)
- retVal = (IntervalElement) lookup;
- else
- {
- retVal = (IntervalElement) Top;
+ 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
+ } else if (exp is IFunApp) {
+ IFunApp fun = (IFunApp)exp;
+
+ if (fun.FunctionSymbol is IntSymbol) // An integer
{
- IntSymbol intSymb = (IntSymbol) fun.FunctionSymbol;
+ IntSymbol intSymb = (IntSymbol)fun.FunctionSymbol;
BigNum val = intSymb.Value;
-
+
retVal = IntervalElement.Factory(val);
- }
- else if(fun.FunctionSymbol.Equals(Int.Negate)) // An unary minus
+ } else if (fun.FunctionSymbol.Equals(Int.Negate)) // An unary minus
{
IExpr/*!*/ arg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
IntervalElement/*!*/ argEval = Eval(arg, state);
Contract.Assert(argEval != null);
IntervalElement/*!*/ zero = IntervalElement.Factory(BigNum.ZERO);
Contract.Assert(zero != null);
-
+
retVal = zero - argEval;
- }
- else if(fun.Arguments.Count == 2)
- {
+ } else if (fun.Arguments.Count == 2) {
IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
-
+
IntervalElement/*!*/ leftVal = Eval(left, state);
Contract.Assert(leftVal != null);
IntervalElement/*!*/ rightVal = Eval(right, state);
Contract.Assert(rightVal != null);
- if(fun.FunctionSymbol.Equals(Int.Add))
+ if (fun.FunctionSymbol.Equals(Int.Add))
retVal = leftVal + rightVal;
- else if(fun.FunctionSymbol.Equals(Int.Sub))
+ else if (fun.FunctionSymbol.Equals(Int.Sub))
retVal = leftVal - rightVal;
- else if(fun.FunctionSymbol.Equals(Int.Mul))
+ else if (fun.FunctionSymbol.Equals(Int.Mul))
retVal = leftVal * rightVal;
- else if(fun.FunctionSymbol.Equals(Int.Div))
+ else if (fun.FunctionSymbol.Equals(Int.Div))
retVal = leftVal / rightVal;
- else if(fun.FunctionSymbol.Equals(Int.Mod))
- retVal = leftVal % rightVal; + else if (fun.FunctionSymbol.Equals(Int.Mod))
+ retVal = leftVal % rightVal;
}
- }
-
+ }
+
return retVal;
}
@@ -351,8 +342,8 @@ Contract.Ensures(Contract.Result<IntervalElement>() != null); // Construct an Interval
public static IntervalElement/*!*/ Factory(ExtendedInt/*!*/ inf, ExtendedInt/*!*/ sup) {
Contract.Requires((sup != null));
-Contract.Requires((inf != null));
-Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ Contract.Requires((inf != null));
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
if (inf is MinusInfinity && sup is PlusInfinity)
return Top;
if (inf > sup)
@@ -367,12 +358,12 @@ Contract.Ensures(Contract.Result<IntervalElement>() != null); }
public static IntervalElement/*!*/ Factory(BigNum inf, BigNum sup) {
-Contract.Ensures(Contract.Result<IntervalElement>() != null);
- ExtendedInt/*!*/ i = ExtendedInt.Factory(inf);
- ExtendedInt/*!*/ s = ExtendedInt.Factory(sup);
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ i = ExtendedInt.Factory(inf);
+ ExtendedInt/*!*/ s = ExtendedInt.Factory(sup);
- return Factory(i, s);
- }
+ return Factory(i, s);
+ }
static public IntervalElement/*!*/ Top {
get {
@@ -401,103 +392,103 @@ Contract.Ensures(Contract.Result<IntervalElement>() != null); #region Below are the arithmetic operations lifted to intervals
// Addition
- public static IntervalElement/*!*/ operator +(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
-Contract.Requires(b != null);
-Contract.Requires(a != null);
-Contract.Ensures(Contract.Result<IntervalElement>() != null);
- ExtendedInt/*!*/ inf = a.inf + b.inf;
- Contract.Assert(inf != null);
- ExtendedInt/*!*/ sup = a.sup + b.sup;
- Contract.Assert(sup != null);
-
- return Factory(inf, sup); - }
+ public static IntervalElement/*!*/ operator +(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ inf = a.inf + b.inf;
+ Contract.Assert(inf != null);
+ ExtendedInt/*!*/ sup = a.sup + b.sup;
+ Contract.Assert(sup != null);
+
+ return Factory(inf, sup);
+ }
// Subtraction
- public static IntervalElement/*!*/ operator -(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
-Contract.Requires(b != null);
-Contract.Requires(a != null);
- Contract.Ensures(Contract.Result<IntervalElement>() != null);
- ExtendedInt/*!*/ inf = a.inf - b.sup;
+ public static IntervalElement/*!*/ operator -(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ inf = a.inf - b.sup;
Contract.Assert(inf != null);
-
- ExtendedInt/*!*/ sup = a.sup - b.inf;
-Contract.Assert(sup != null);
-IntervalElement/*!*/ sub = Factory(inf, sup);
-Contract.Assert(sub != null); - return sub;
- }
+ ExtendedInt/*!*/ sup = a.sup - b.inf;
+ Contract.Assert(sup != null);
+ IntervalElement/*!*/ sub = Factory(inf, sup);
+ Contract.Assert(sub != null);
+
+ return sub;
+ }
// Multiplication
- public static IntervalElement/*!*/ operator *(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
-Contract.Requires(b != null);
-Contract.Requires(a != null);
-Contract.Ensures(Contract.Result<IntervalElement>() != null);
- ExtendedInt/*!*/ infinf = a.inf * b.inf;
- Contract.Assert(infinf != null);
- ExtendedInt/*!*/ infsup = a.inf * b.sup;
- Contract.Assert(infsup != null);
- ExtendedInt/*!*/ supinf = a.sup * b.inf;
- Contract.Assert(supinf != null);
- ExtendedInt/*!*/ supsup = a.sup * b.sup;
- Contract.Assert(supsup != null);
-
- ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
- Contract.Assert(inf != null);
- ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
- Contract.Assert(sup != null);
-
- return Factory(inf, sup);
- }
+ public static IntervalElement/*!*/ operator *(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ ExtendedInt/*!*/ infinf = a.inf * b.inf;
+ Contract.Assert(infinf != null);
+ ExtendedInt/*!*/ infsup = a.inf * b.sup;
+ Contract.Assert(infsup != null);
+ ExtendedInt/*!*/ supinf = a.sup * b.inf;
+ Contract.Assert(supinf != null);
+ ExtendedInt/*!*/ supsup = a.sup * b.sup;
+ Contract.Assert(supsup != null);
+
+ ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ Contract.Assert(inf != null);
+ ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ Contract.Assert(sup != null);
+
+ return Factory(inf, sup);
+ }
// Division
- public static IntervalElement/*!*/ operator /(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
-Contract.Requires(b != null);
-Contract.Requires(a != null);
-Contract.Ensures(Contract.Result<IntervalElement>() != null);
- if(b.inf.IsZero && b.sup.IsZero) // Check division by zero
- return IntervalElement.Top;
-
- ExtendedInt/*!*/ infinf = a.inf / b.inf;
- Contract.Assert(infinf != null);
- ExtendedInt/*!*/ infsup = a.inf / b.sup;
- Contract.Assert(infsup != null);
- ExtendedInt/*!*/ supinf = a.sup / b.inf;
- Contract.Assert(supinf != null);
- ExtendedInt/*!*/ supsup = a.sup / b.sup;
- Contract.Assert(supsup != null);
-
- ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
- Contract.Assert(inf != null);
- ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
- Contract.Assert(sup != null);
-
- return Factory(inf, sup);
- }
+ public static IntervalElement/*!*/ operator /(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ if (b.inf.IsZero && b.sup.IsZero) // Check division by zero
+ return IntervalElement.Top;
+
+ ExtendedInt/*!*/ infinf = a.inf / b.inf;
+ Contract.Assert(infinf != null);
+ ExtendedInt/*!*/ infsup = a.inf / b.sup;
+ Contract.Assert(infsup != null);
+ ExtendedInt/*!*/ supinf = a.sup / b.inf;
+ Contract.Assert(supinf != null);
+ ExtendedInt/*!*/ supsup = a.sup / b.sup;
+ Contract.Assert(supsup != null);
+
+ ExtendedInt/*!*/ inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ Contract.Assert(inf != null);
+ ExtendedInt/*!*/ sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+ Contract.Assert(sup != null);
+
+ return Factory(inf, sup);
+ }
// Division
- public static IntervalElement/*!*/ operator %(IntervalElement/*!*/ a, IntervalElement/*!*/ b){
-Contract.Requires(b != null);
-Contract.Requires(a != null);
-Contract.Ensures(Contract.Result<IntervalElement>() != null);
- if(b.inf.IsZero && b.sup.IsZero) // Check division by zero
- return IntervalElement.Top;
-
- ExtendedInt/*!*/ infinf = a.inf % b.inf;
- Contract.Assert(infinf != null);
- ExtendedInt/*!*/ infsup = a.inf % b.sup;
- Contract.Assert(infsup != null);
- ExtendedInt/*!*/ supinf = a.sup % b.inf;
- Contract.Assert(supinf != null);
- ExtendedInt/*!*/ supsup = a.sup % b.sup;
- Contract.Assert(supsup != null);
-
- ExtendedInt inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
- ExtendedInt sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
-
- return Factory(inf, sup);
- }
+ public static IntervalElement/*!*/ operator %(IntervalElement/*!*/ a, IntervalElement/*!*/ b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<IntervalElement>() != null);
+ if (b.inf.IsZero && b.sup.IsZero) // Check division by zero
+ return IntervalElement.Top;
+
+ ExtendedInt/*!*/ infinf = a.inf % b.inf;
+ Contract.Assert(infinf != null);
+ ExtendedInt/*!*/ infsup = a.inf % b.sup;
+ Contract.Assert(infsup != null);
+ ExtendedInt/*!*/ supinf = a.sup % b.inf;
+ Contract.Assert(supinf != null);
+ ExtendedInt/*!*/ supsup = a.sup % b.sup;
+ Contract.Assert(supsup != null);
+
+ ExtendedInt inf = ExtendedInt.Inf(infinf, infsup, supinf, supsup);
+ ExtendedInt sup = ExtendedInt.Sup(infinf, infsup, supinf, supsup);
+
+ return Factory(inf, sup);
+ }
#endregion
@@ -520,9 +511,9 @@ Contract.Ensures(Contract.Result<IntervalElement>() != null); [Pure]
public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
-return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
- }
+ Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+ return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
+ }
[Pure]
public override string/*!*/ ToString() {
@@ -736,13 +727,13 @@ return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsRead return sup;
}
- public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d){
-Contract.Requires(d != null);
-Contract.Requires(c != null);
-Contract.Requires(b != null);
-Contract.Requires(a != null);
-Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- ExtendedInt/*!*/ infab = Inf(a,b);
+ public static ExtendedInt/*!*/ Inf(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) {
+ Contract.Requires(d != null);
+ Contract.Requires(c != null);
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ ExtendedInt/*!*/ infab = Inf(a, b);
Contract.Assert(infab != null);
ExtendedInt/*!*/ infcd = Inf(c, d);
Contract.Assert(infcd != null);
@@ -760,13 +751,13 @@ Contract.Ensures(Contract.Result<ExtendedInt>() != null); return sup;
}
- public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d){
-Contract.Requires(d != null);
-Contract.Requires(c != null);
-Contract.Requires(b != null);
-Contract.Requires(a != null);
-Contract.Ensures(Contract.Result<ExtendedInt>() != null);
- ExtendedInt/*!*/ supab = Sup(a,b);
+ public static ExtendedInt/*!*/ Sup(ExtendedInt/*!*/ a, ExtendedInt/*!*/ b, ExtendedInt/*!*/ c, ExtendedInt/*!*/ d) {
+ Contract.Requires(d != null);
+ Contract.Requires(c != null);
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
+ Contract.Ensures(Contract.Result<ExtendedInt>() != null);
+ ExtendedInt/*!*/ supab = Sup(a, b);
Contract.Assert(supab != null);
ExtendedInt/*!*/ supcd = Sup(c, d);
Contract.Assert(supcd != null);
@@ -816,7 +807,7 @@ Contract.Ensures(Contract.Result<ExtendedInt>() != null); }
public override int CompareTo(ExtendedInt/*!*/ that) {
- Contract.Requires(that != null);
+ //Contract.Requires(that != null);
if (that is PlusInfinity)
return -1;
else if (that is PureInteger)
@@ -848,7 +839,7 @@ Contract.Ensures(Contract.Result<ExtendedInt>() != null); }
public override int CompareTo(ExtendedInt/*!*/ that) {
- Contract.Requires(that != null);
+ //Contract.Requires(that != null);
if (that is PlusInfinity)
return 0;
else
@@ -870,7 +861,7 @@ Contract.Ensures(Contract.Result<ExtendedInt>() != null); }
public override int CompareTo(ExtendedInt/*!*/ that) {
- Contract.Requires(that != null);
+ //Contract.Requires(that != null);
if (that is MinusInfinity)
return 0;
else
diff --git a/Source/AIFramework/VariableMap/Nullness.cs b/Source/AIFramework/VariableMap/Nullness.cs index 9eac6b29..613f55e0 100644 --- a/Source/AIFramework/VariableMap/Nullness.cs +++ b/Source/AIFramework/VariableMap/Nullness.cs @@ -4,200 +4,206 @@ //
//-----------------------------------------------------------------------------
using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System.Collections;
- using System.Diagnostics;
- //using System.Compiler.Analysis;
+namespace Microsoft.AbstractInterpretationFramework {
+ using System.Collections;
+ using System.Diagnostics;
+ //using System.Compiler.Analysis;
+
+ public class NullnessLattice : MicroLattice {
+ readonly INullnessFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
- public class NullnessLattice : MicroLattice
- {
- readonly INullnessFactory/*!*/ factory;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(factory != null);
- }
+ public NullnessLattice(INullnessFactory/*!*/ factory) {
+ Contract.Requires(factory != null);
+ this.factory = factory;
+ // base();
+ }
- public NullnessLattice(INullnessFactory/*!*/ factory){
-Contract.Requires(factory != null);
- this.factory = factory;
- // base();
- }
-
- enum Value { Bottom, NotNull, Null, MayBeNull }
+ enum Value {
+ Bottom,
+ NotNull,
+ Null,
+ MayBeNull
+ }
- private class Elt : Element
- {
- public Value value;
-
- public Elt (Value v) { this.value = v; }
-
- [Pure]
- public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
-return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
- }
-
- public override Element/*!*/ Clone() {
-Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(this.value);
- }
- }
+ private class Elt : Element {
+ public Value value;
+ public Elt(Value v) {
+ this.value = v;
+ }
- public override Element/*!*/ Top
- {
- get {Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.MayBeNull); }
- }
+ [Pure]
+ public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+ return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
+ }
- public override Element/*!*/ Bottom
- {
- get {Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.Bottom); }
- }
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(this.value);
+ }
+ }
- public static Element/*!*/ Null
- {
- get {Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.Null); }
- }
- public static Element/*!*/ NotNull
- {
- get {Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.NotNull); }
- }
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.MayBeNull);
+ }
+ }
- public override bool IsTop (Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt) element;
- return e.value == Value.MayBeNull;
- }
+ public override Element/*!*/ Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Bottom);
+ }
+ }
- public override bool IsBottom (Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt) element;
- return e.value == Value.Bottom;
- }
+ public static Element/*!*/ Null {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Null);
+ }
+ }
- public override Lattice.Element/*!*/ NontrivialJoin (Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Lattice.Element>() != null);
- Elt a = (Elt) first;
- Elt b = (Elt) second;
- return (a.value == b.value) ? a : (Elt)Top;
- }
+ public static Element/*!*/ NotNull {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.NotNull);
+ }
+ }
- public override Lattice.Element/*!*/ NontrivialMeet (Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Lattice.Element>() != null);
- Elt a = (Elt) first;
- Elt b = (Elt) second;
- return (a.value == b.value) ? a : (Elt)Bottom;
- }
-
- public override Element/*!*/ Widen (Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- return Join(first,second);
- }
+ public override bool IsTop(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return e.value == Value.MayBeNull;
+ }
- protected override bool AtMost (Element/*!*/ first, Element/*!*/ second) // this <= that
- {
-Contract.Requires(first != null);
-Contract.Requires(second != null);
- Elt a = (Elt) first;
- Elt b = (Elt) second;
- return a.value == b.value;
- }
+ public override bool IsBottom(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return e.value == Value.Bottom;
+ }
- public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element){
-Contract.Requires(element != null);
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- Elt e = (Elt)element;
+ public override Lattice.Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Lattice.Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ return (a.value == b.value) ? a : (Elt)Top;
+ }
- if (e.value == Value.NotNull)
- {
- return factory.Neq(var, factory.Null);
- }
- if (e.value == Value.Null)
- {
- return factory.Eq(var, factory.Null);
- }
- {Contract.Assert(false);throw new cce.UnreachableException();}
- throw new System.Exception();
- }
+ public override Lattice.Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Lattice.Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ return (a.value == b.value) ? a : (Elt)Bottom;
+ }
- public override IExpr GetFoldExpr(Element/*!*/ e){
-Contract.Requires(e != null);
- Elt elt = (Elt)e;
- if (elt.value == Value.Null) {
- return factory.Null;
- } else {
- // can't fold into an expression
- return null;
- }
- }
+ public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return Join(first, second);
+ }
- public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args){
-Contract.Requires(args != null);
-Contract.Requires(f != null);
- if (f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq) ||
- f.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
+ protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
+ {
+ //Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ return a.value == b.value;
+ }
- Contract.Assert(args.Count == 2);
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
- IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+ public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ //Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ Elt e = (Elt)element;
- // 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;
- }
+ if (e.value == Value.NotNull) {
+ return factory.Neq(var, factory.Null);
+ }
+ if (e.value == Value.Null) {
+ return factory.Eq(var, factory.Null);
+ }
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ throw new System.Exception();
+ }
- public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e){
-Contract.Requires(e != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- IFunApp nary = e as IFunApp;
- if (nary != null) {
- bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
- IList/*<IExpr!>*//*!*/ args = nary.Arguments;
- Contract.Assert(args != null);
- Contract.Assert(args.Count == 2);
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
- IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(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;
- }
+ public override IExpr GetFoldExpr(Element/*!*/ e) {
+ //Contract.Requires(e != null);
+ Elt elt = (Elt)e;
+ if (elt.value == Value.Null) {
+ return factory.Null;
+ } else {
+ // can't fold into an expression
+ return null;
+ }
+ }
- if (var != null) // found the pattern
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
+ //Contract.Requires(args != null);
+ //Contract.Requires(f != null);
+ if (f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq) ||
+ f.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
+
+ Contract.Assert(args.Count == 2);
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+ IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(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) {
+ //Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ IFunApp nary = e as IFunApp;
+ if (nary != null) {
+ bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
+ IList/*<IExpr!>*//*!*/ args = nary.Arguments;
+ Contract.Assert(args != null);
+ Contract.Assert(args.Count == 2);
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+ IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(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;
+ return isEq ? Null : NotNull;
+ }
}
+ }
+ return Top;
}
+ }
#if false
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs index e0b9ac04..169156b0 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.cs +++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs @@ -3,852 +3,855 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System.Diagnostics.Contracts;
- using System.Collections;
- using System.Collections.Generic;
- using System.Diagnostics;
-
- using Microsoft.AbstractInterpretationFramework;
- using Microsoft.AbstractInterpretationFramework.Collections;
-
- using Microsoft.Boogie;
- using IMutableSet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
- using ISet = Microsoft.Boogie.Set;
-
- /// <summary>
- /// Creates a lattice that works for several variables given a MicroLattice. Assumes
- /// if one variable is bottom, then all variables are bottom.
- /// </summary>
- public class VariableMapLattice : Lattice
- {
- private class Elt : Element
- {
- /// <summary>
- /// IsBottom(e) iff e.constraints == null
- /// </summary>
- /*MayBeNull*/
- private IFunctionalMap constraints; // of type IVariable -> LATTICE_ELEMENT
- public IFunctionalMap Constraints
- {
- get
- {
- return this.constraints;
- }
- }
+namespace Microsoft.AbstractInterpretationFramework {
+ using System.Diagnostics.Contracts;
+ using System.Collections;
+ using System.Collections.Generic;
+ using System.Diagnostics;
+
+ using Microsoft.AbstractInterpretationFramework;
+ using Microsoft.AbstractInterpretationFramework.Collections;
+
+ using Microsoft.Boogie;
+ using IMutableSet = Microsoft.Boogie.Set;
+ using HashSet = Microsoft.Boogie.Set;
+ using ISet = Microsoft.Boogie.Set;
+
+ /// <summary>
+ /// Creates a lattice that works for several variables given a MicroLattice. Assumes
+ /// if one variable is bottom, then all variables are bottom.
+ /// </summary>
+ public class VariableMapLattice : Lattice {
+ private class Elt : Element {
+ /// <summary>
+ /// IsBottom(e) iff e.constraints == null
+ /// </summary>
+ /*MayBeNull*/
+ private IFunctionalMap constraints; // of type IVariable -> LATTICE_ELEMENT
+ public IFunctionalMap Constraints {
+ get {
+ return this.constraints;
+ }
+ }
- private Elt(bool top) {
- if (top) {
- this.constraints = FunctionalHashtable.Empty;
- } else {
- this.constraints = null;
- }
- }
+ private Elt(bool top) {
+ if (top) {
+ this.constraints = FunctionalHashtable.Empty;
+ } else {
+ this.constraints = null;
+ }
+ }
- public override Element/*!*/ Clone() {
-Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(this.constraints);
- }
-
- [Pure]
- public override string/*!*/ ToString() {
-Contract.Ensures(Contract.Result<string>() != null);
- if (constraints == null) {
- return "<bottom>";
- }
- string s = "[";
- string sep = "";
- foreach(IVariable/*!*/ v in cce.NonNull(constraints.Keys)){
-Contract.Assert(v != null);
- Element m = (Element)constraints[v];
- s += sep + v.Name + " -> " + m;
- sep = ", ";
- }
- return s + "]";
- }
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(this.constraints);
+ }
- public static Elt/*!*/ Top = new Elt(true);
- public static Elt/*!*/ Bottom = new Elt(false);
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Top != null);
- Contract.Invariant(Bottom != null);
-}
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ if (constraints == null) {
+ return "<bottom>";
+ }
+ string s = "[";
+ string sep = "";
+ foreach (IVariable/*!*/ v in cce.NonNull(constraints.Keys)) {
+ Contract.Assert(v != null);
+ 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);
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Top != null);
+ Contract.Invariant(Bottom != null);
+ }
- public Elt(IFunctionalMap constraints)
- {
- this.constraints = constraints;
- }
- public bool IsBottom {
- get {
- return this.constraints == null;
- }
- }
+ public Elt(IFunctionalMap constraints) {
+ this.constraints = constraints;
+ }
- public int Count { get { return this.constraints == null ? 0 : this.constraints.Count; } }
+ public bool IsBottom {
+ get {
+ return this.constraints == null;
+ }
+ }
- public IEnumerable/*<IVariable>*//*!*/ Variables {
- get {
- Contract.Requires(!this.IsBottom);
- Contract.Ensures(Contract.Result<IEnumerable>() != null);
- Contract.Assume(this.constraints != null);
- return cce.NonNull(this.constraints.Keys);
- }
- }
+ public int Count {
+ get {
+ return this.constraints == null ? 0 : this.constraints.Count;
+ }
+ }
- public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
- Contract.Ensures(Contract.Result<IEnumerable>() != null);
- 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 IEnumerable/*<IVariable>*//*!*/ Variables {
+ get {
+ Contract.Requires(!this.IsBottom);
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
+ Contract.Assume(this.constraints != null);
+ return cce.NonNull(this.constraints.Keys);
+ }
+ }
- public Element this [IVariable/*!*/ key] {
- get{
- Contract.Requires(!this.IsBottom);
- Contract.Requires(key != null);
- Contract.Assume(this.constraints != null);
- return (Element)constraints[key];
- }
- }
+ public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
+ 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;
+ }
+ }
- /// <summary>
- /// Add a new entry in the functional map: var --> value.
- /// If the variable is already there, throws an exception
- /// </summary>
- public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice){
-Contract.Requires(microLattice != null);
-Contract.Requires(value != null);
-Contract.Requires(var != null);
-Contract.Requires((!this.IsBottom));
-Contract.Ensures(Contract.Result<Elt>() != null);
- Contract.Assume(this.constraints != null);
- Contract.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));
- }
+ public Element Lookup(IVariable v) {
+ if ((v == null) || (this.constraints == null)) {
+ return null;
+ }
+ return (Element)this.constraints[v];
+ }
- /// <summary>
- /// Set the value of the variable in the functional map
- /// If the variable is not already there, throws an exception
- /// </summary>
- public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice){
- Contract.Requires(microLattice != null);
- Contract.Requires(value != null);
- Contract.Requires(var != null);
- Contract.Ensures(Contract.Result<Elt>() != null);
- if(microLattice.IsBottom(value)) { return Bottom; }
- if(microLattice.IsTop(value)) { return this.Remove(var, microLattice); }
-
- Contract.Assume(this.constraints != null);
- Contract.Assert(this.constraints.Contains(var));
-
- // this.constraints[var] = value;
- IFunctionalMap newMap = this.constraints.Set(var, value);
-
- return new Elt(newMap);
- }
+ public Element this[IVariable/*!*/ key] {
+ get {
+ Contract.Requires(!this.IsBottom);
+ Contract.Requires(key != null);
+ Contract.Assume(this.constraints != null);
+ return (Element)constraints[key];
+ }
+ }
- public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice){
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<Elt>() != null);
- if (this.IsBottom) { return this; }
- Contract.Assume(this.constraints != null);
- return new Elt(this.constraints.Remove(var));
- }
+ /// <summary>
+ /// Add a new entry in the functional map: var --> value.
+ /// If the variable is already there, throws an exception
+ /// </summary>
+ public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
+ Contract.Requires(microLattice != null);
+ Contract.Requires(value != null);
+ Contract.Requires(var != null);
+ Contract.Requires((!this.IsBottom));
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ Contract.Assume(this.constraints != null);
+ Contract.Assert(!this.constraints.Contains(var));
+
+ if (microLattice.IsBottom(value)) {
+ return Bottom;
+ }
+ if (microLattice.IsTop(value)) {
+ return this.Remove(var, microLattice);
+ }
- public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice){
-Contract.Requires(microLattice != null);
-Contract.Requires(newName != null);
-Contract.Requires(oldName != null);
-Contract.Requires((!this.IsBottom));
-Contract.Ensures(Contract.Result<Elt>() != null);
- Element value = this[oldName];
- if (value == null) { return this; } // 'oldName' isn't in the map, so neither will be 'newName'
- Contract.Assume(this.constraints != null);
- IFunctionalMap newMap = this.constraints.Remove(oldName);
- newMap = newMap.Add(newName, value);
- return new Elt(newMap);
- }
+ return new Elt(this.constraints.Add(var, value));
+ }
- [Pure]
- public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
- throw new System.NotImplementedException();
- }
+ /// <summary>
+ /// Set the value of the variable in the functional map
+ /// If the variable is not already there, throws an exception
+ /// </summary>
+ public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice) {
+ Contract.Requires(microLattice != null);
+ Contract.Requires(value != null);
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ if (microLattice.IsBottom(value)) {
+ return Bottom;
+ }
+ if (microLattice.IsTop(value)) {
+ return this.Remove(var, microLattice);
+ }
- } // class
+ Contract.Assume(this.constraints != null);
+ Contract.Assert(this.constraints.Contains(var));
- private readonly MicroLattice/*!*/ microLattice;
+ // this.constraints[var] = value;
+ IFunctionalMap newMap = this.constraints.Set(var, value);
- private readonly IPropExprFactory/*!*/ propExprFactory;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(microLattice != null);
- Contract.Invariant(propExprFactory != null);
-}
+ return new Elt(newMap);
+ }
-
- private readonly /*maybe null*/IComparer variableComparer;
-
- public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer)
- : base(valueExprFactory){
-Contract.Requires(microLattice != null);
-Contract.Requires(valueExprFactory != null);
-Contract.Requires(propExprFactory != null);
- this.propExprFactory = propExprFactory;
- this.microLattice = microLattice;
- this.variableComparer = variableComparer;
- // base(valueExprFactory);
+ public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice) {
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ if (this.IsBottom) {
+ return this;
}
+ Contract.Assume(this.constraints != null);
+ return new Elt(this.constraints.Remove(var));
+ }
- protected override object/*!*/ UniqueId{
- get{
-Contract.Ensures(Contract.Result<object>() != null);
- return this.microLattice.GetType(); } }
+ public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice) {
+ Contract.Requires(microLattice != null);
+ Contract.Requires(newName != null);
+ Contract.Requires(oldName != null);
+ Contract.Requires((!this.IsBottom));
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ Element value = this[oldName];
+ if (value == null) {
+ return this;
+ } // 'oldName' isn't in the map, so neither will be 'newName'
+ Contract.Assume(this.constraints != null);
+ IFunctionalMap newMap = this.constraints.Remove(oldName);
+ newMap = newMap.Add(newName, value);
+ return new Elt(newMap);
+ }
- public override Element/*!*/ Top{
-get{Contract.Ensures(Contract.Result<Element>() != null);
- return Elt.Top; } }
+ [Pure]
+ public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
+ throw new System.NotImplementedException();
+ }
- public override Element Bottom{get{
-Contract.Ensures(Contract.Result<Element>() != null);
- return Elt.Bottom; } }
+ } // class
- public override bool IsTop(Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- return !e.IsBottom && e.Count == 0;
- }
+ private readonly MicroLattice/*!*/ microLattice;
- public override bool IsBottom(Element/*!*/ element){
-Contract.Requires(element != null);
- return ((Elt)element).IsBottom;
- }
+ private readonly IPropExprFactory/*!*/ propExprFactory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(microLattice != null);
+ Contract.Invariant(propExprFactory != null);
+ }
- protected override bool AtMost(Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
- 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){
-Contract.Assert(var != null);
- Element thisValue = cce.NonNull(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){
-Contract.Assert(var != null);
- if (a.Lookup(var) != null) { continue; } // we checked this case in the loop above
-
- Element thatValue = cce.NonNull(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) {
-Contract.Requires((newValue != null));
-Contract.Requires((var != null));
-Contract.Requires((element != null));
-Contract.Ensures(Contract.Result<Elt>() != null);
- Elt e = (Elt)element;
+ private readonly /*maybe null*/IComparer variableComparer;
+
+ public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer)
+ : base(valueExprFactory) {
+ Contract.Requires(microLattice != null);
+ Contract.Requires(valueExprFactory != null);
+ Contract.Requires(propExprFactory != null);
+ this.propExprFactory = propExprFactory;
+ this.microLattice = microLattice;
+ this.variableComparer = variableComparer;
+ // base(valueExprFactory);
+ }
+
+ protected override object/*!*/ UniqueId {
+ get {
+ Contract.Ensures(Contract.Result<object>() != null);
+ return this.microLattice.GetType();
+ }
+ }
+
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Top;
+ }
+ }
+
+ public override Element Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Bottom;
+ }
+ }
+
+ public override bool IsTop(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return !e.IsBottom && e.Count == 0;
+ }
+
+ public override bool IsBottom(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ return ((Elt)element).IsBottom;
+ }
+
+ protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ 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) {
+ Contract.Assert(var != null);
+ Element thisValue = cce.NonNull(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) {
+ Contract.Assert(var != null);
+ if (a.Lookup(var) != null) {
+ continue;
+ } // we checked this case in the loop above
+
+ Element thatValue = cce.NonNull(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) {
+ Contract.Requires((newValue != null));
+ Contract.Requires((var != null));
+ Contract.Requires((element != null));
+ Contract.Ensures(Contract.Result<Elt>() != null);
+ Elt e = (Elt)element;
- if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
+ 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;
+ /*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){
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<string>() != null);
- Elt e = (Elt)element;
+ public override string/*!*/ ToString(Element/*!*/ element) {
+ Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ Elt e = (Elt)element;
- if (IsTop(e)) { return "<top>"; }
- if (IsBottom(e)) { return "<bottom>"; }
+ if (IsTop(e)) {
+ return "<top>";
+ }
+ if (IsBottom(e)) {
+ return "<bottom>";
+ }
- int k = 0;
- System.Text.StringBuilder buffer = new System.Text.StringBuilder();
- foreach(IVariable/*!*/ key in e.SortedVariables(variableComparer)){
-Contract.Assert(key != null);
- if (k++ > 0) { buffer.Append("; "); }
- buffer.AppendFormat("{0} = {1}", key, e[key]);
- }
- return buffer.ToString();
+ int k = 0;
+ System.Text.StringBuilder buffer = new System.Text.StringBuilder();
+ foreach (IVariable/*!*/ key in e.SortedVariables(variableComparer)) {
+ Contract.Assert(key != null);
+ if (k++ > 0) {
+ buffer.Append("; ");
}
+ buffer.AppendFormat("{0} = {1}", key, e[key]);
+ }
+ return buffer.ToString();
+ }
- public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
-
- IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach(IVariable/*!*/ key in a.Variables){
-Contract.Assert(key != null);
- 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);
- Contract.Assert(join != null);
-
- // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
-
- return join;
+ public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+
+ IFunctionalMap newMap = FunctionalHashtable.Empty;
+ foreach (IVariable/*!*/ key in a.Variables) {
+ Contract.Assert(key != null);
+ 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);
+ Contract.Assert(join != null);
+
+ // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
- public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
+ return join;
+ }
- IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach(IVariable/*!*/ key in a.Variables){
-Contract.Assert(key != null);
-Element/*!*/ aValue = cce.NonNull(a[key]);
- Element bValue = b[key];
+ public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
- Element newValue =
- bValue == null ? aValue :
- this.microLattice.Meet(aValue, bValue);
+ IFunctionalMap newMap = FunctionalHashtable.Empty;
+ foreach (IVariable/*!*/ key in a.Variables) {
+ Contract.Assert(key != null);
+ Element/*!*/ aValue = cce.NonNull(a[key]);
+ Element bValue = b[key];
- newMap = newMap.Add(key, newValue);
- }
- foreach(IVariable/*!*/ key in b.Variables){
-Contract.Assert(key != null);
- 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);
+ Element newValue =
+ bValue == null ? aValue :
+ this.microLattice.Meet(aValue, bValue);
+
+ newMap = newMap.Add(key, newValue);
+ }
+ foreach (IVariable/*!*/ key in b.Variables) {
+ Contract.Assert(key != null);
+ Element aValue = a[key];
+ Element bValue = b[key];
+ Debug.Assert(bValue != null);
+
+ if (aValue == null) {
+ // It's a variable we didn't cover in the last loop.
+ newMap = newMap.Add(key, bValue);
}
+ }
+ return new Elt(newMap);
+ }
- /// <summary>
- /// Perform the pointwise widening of the elements in the map
- /// </summary>
- public override Element/*!*/ Widen (Element/*!*/ first, Element/*!*/ second) {
-Contract.Requires((second != null));
-Contract.Requires((first != null));
-Contract.Ensures(Contract.Result<Element>() != null);
- 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){
-Contract.Assert(key != null);
- 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);
+ /// <summary>
+ /// Perform the pointwise widening of the elements in the map
+ /// </summary>
+ public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+ Contract.Requires((second != null));
+ Contract.Requires((first != null));
+ Contract.Ensures(Contract.Result<Element>() != null);
+ 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) {
+ Contract.Assert(key != null);
+ 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);
Contract.Assert(widen != null);
- // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
+ // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
- return widen;
- }
+ return widen;
+ }
- internal static ISet/*<IVariable!>*//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/*<IVariable!>*//*!*/ ignoreVars){
-Contract.Requires(ignoreVars != null);
-Contract.Requires(e != null);
- Contract.Ensures(Contract.Result<ISet>() != null);
- HashSet s = new HashSet();
+ internal static ISet/*<IVariable!>*//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/*<IVariable!>*//*!*/ ignoreVars) {
+ Contract.Requires(ignoreVars != null);
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<ISet>() != null);
+ HashSet s = new HashSet();
- IFunApp f = e as IFunApp;
- IFunction lambda = e as IFunction;
+ 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){
-Contract.Assert(arg != null);
- s.AddAll(VariablesInExpression(arg, ignoreVars));
- }
- }
- else if (lambda != null)
+ if (e is IVariable) {
+ if (!ignoreVars.Contains(e))
+ s.Add(e);
+ } else if (f != null) // e is IFunApp
{
- IMutableSet x = new HashSet(1);
- x.Add(lambda.Param);
+ foreach (IExpr/*!*/ arg in f.Arguments) {
+ Contract.Assert(arg != null);
+ 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, cce.NonNull(Set.Union(ignoreVars, x))));
+ } else if (e is IUnknown) {
+ // skip (actually, it would be appropriate to return the universal set of all variables)
+ } else {
+ Debug.Assert(false, "case not handled: " + e);
+ }
+ return s;
+ }
- // Ignore the bound variable
- s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
- }
- else if (e is IUnknown)
- {
- // skip (actually, it would be appropriate to return the universal set of all variables)
- }
- else
- {
- Debug.Assert(false, "case not handled: " + e);
- }
- return s;
+
+ private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e) {
+ Contract.Ensures(Contract.Result<ArrayList>() != null);
+ 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 ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e)
- {
- Contract.Ensures(Contract.Result<ArrayList>() != null);
- ArrayList result = new ArrayList();
+ private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right) {
+ Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
+ left = null;
+ right = null;
- 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);
- }
+ // See if we have an equality
+ IFunApp nary = expr as IFunApp;
+ if (nary == null || !nary.FunctionSymbol.Equals(Value.Eq)) {
+ return false;
+ }
- return result;
- }
+ // 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;
+ }
- private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right)
- {
- Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out 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;
- }
+ left = idLeft;
+ right = idRight;
+ return true;
+ }
- /// <summary>
- /// Returns true iff the expression is in the form var == arithmeticExpr
- /// </summary>
- private static bool IsArithmeticExpr(IExpr/*!*/ expr){
-Contract.Requires(expr != null);
- // 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
+ /// <summary>
+ /// Returns true iff the expression is in the form var == arithmeticExpr
+ /// </summary>
+ private static bool IsArithmeticExpr(IExpr/*!*/ expr) {
+ Contract.Requires(expr != null);
+ // 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;
+ 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/*!*/)cce.NonNull(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/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
- 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/*!*/)cce.NonNull(fun.Arguments[0]));
- else if(fun.Arguments.Count != 2) // A function of two or more operands is not arithmetic
+ if (!(left is IVariable || right is IVariable)) // At least one of the two operands must be a variable
return false;
- else
- {
- IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
- IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(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;
- }
- }
+
+ 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;
- }
+ return false;
+ }
+ } else {
+ return false;
}
+ }
- public override IExpr/*!*/ ToPredicate(Element/*!*/ element){
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- 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)){
-Contract.Assert(variable != null);
- Element value = (Element)e[variable];
+ public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
+ Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ if (IsTop(element)) {
+ return propExprFactory.True;
+ }
+ if (IsBottom(element)) {
+ return propExprFactory.False;
+ }
- if (value == null || this.microLattice.IsTop(value)) { continue; } // Skip variables about which we know nothing.
- if (this.microLattice.IsBottom(value)) { return propExprFactory.False; }
+ Elt e = (Elt)element;
+ IExpr truth = propExprFactory.True;
+ IExpr result = truth;
- IExpr conjunct = this.microLattice.ToPredicate(variable, value);
+ foreach (IVariable/*!*/ variable in e.SortedVariables(variableComparer)) {
+ Contract.Assert(variable != null);
+ Element value = (Element)e[variable];
- result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
- }
- return result;
+ 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);
- public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable){
-Contract.Requires(variable != null);
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- return cce.NonNull((Elt)element).Remove(variable, this.microLattice);
+ result = (result == truth) ? (IExpr)conjunct : (IExpr)propExprFactory.And(result, conjunct);
+ }
+ return result;
+ }
+
+
+ public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable) {
+ //Contract.Requires(variable != null);
+ //Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return cce.NonNull((Elt)element).Remove(variable, this.microLattice);
+ }
+
+ private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
+ private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var) {
+ //Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ return var;
+ }
+
+ /// <summary>
+ /// Return a new expression in which each variable has been
+ /// replaced by an expression representing what is known about
+ /// that variable.
+ /// </summary>
+ private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/*<IVariable!>*//*!*/ notInlineable,
+ OnUnableToInline/*!*/ unableToInline) {
+ Contract.Requires(unableToInline != null);
+ Contract.Requires(notInlineable != null);
+ Contract.Requires(expr != null);
+ Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ 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
- private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
- private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var){
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- return var;
+ IFunApp fun = expr as IFunApp;
+ if (fun != null) {
+ IList newargs = new ArrayList();
+ foreach (IExpr/*!*/ arg in fun.Arguments) {
+ Contract.Assert(arg != null);
+ newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
}
+ return fun.CloneWithArguments(newargs);
+ }
- /// <summary>
- /// Return a new expression in which each variable has been
- /// replaced by an expression representing what is known about
- /// that variable.
- /// </summary>
- private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/*<IVariable!>*//*!*/ notInlineable,
- OnUnableToInline/*!*/ unableToInline){
- Contract.Requires(unableToInline != null);
-Contract.Requires(notInlineable != null);
-Contract.Requires(expr != null);
-Contract.Requires(element != null);
- Contract.Ensures(Contract.Result<IExpr>() != null);
- 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
- // else
+ IFunction lambda = expr as IFunction;
+ if (lambda != null) {
+ IMutableSet x = new HashSet(1);
+ x.Add(lambda.Param);
- IFunApp fun = expr as IFunApp;
- if (fun != null)
- {
- IList newargs = new ArrayList();
- foreach(IExpr/*!*/ arg in fun.Arguments){
-Contract.Assert(arg != null);
- newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
- }
- return fun.CloneWithArguments(newargs);
- }
+ // Don't inline the bound variable
+ return lambda.CloneWithBody(
+ InlineVariables(element, lambda.Body,
+ cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
+ );
+ }
- // else
+ // 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,
- cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
- );
- }
+ if (expr is IUnknown) {
+ return expr;
+ } else {
+ throw
+ new System.NotImplementedException("cannot inline identifies in expression " + expr);
+ }
+ }
- // else
-
- if (expr is IUnknown) {
- return expr;
- }
- else
- {
- throw
- new System.NotImplementedException("cannot inline identifies in expression " + expr);
- }
- }
+ public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr) {
+ //Contract.Requires(expr != null);
+ //Contract.Requires(element != null);
+ //Contract.Ensures(Contract.Result<Element>() != null);
+ Elt/*!*/ result = (Elt)element;
+ Contract.Assert(result != null);
+ if (IsBottom(element)) {
+ return result; // == element
+ }
- public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr){
-Contract.Requires(expr != null);
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt/*!*/ result = (Elt)element;
- Contract.Assert(result != null);
+ expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
- if(IsBottom(element))
- {
- return result; // == element
- }
+ foreach (IExpr/*!*/ conjunct in FindConjuncts(expr)) {
+ Contract.Assert(conjunct != null);
+ IVariable left, right;
- expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
-
- foreach(IExpr/*!*/ conjunct in FindConjuncts(expr)){
-Contract.Assert(conjunct != null);
- IVariable left, right;
-
- if (IsSimpleEquality(conjunct, out left, out right))
- {
- #region The conjunct is a simple equality
-
-
- Contract.Assert(left != null && right != null);
-
- Element leftValue = result[left], rightValue = result[right];
- if (leftValue == null) { leftValue = this.microLattice.Top; }
- if (rightValue == null) { rightValue = this.microLattice.Top; }
- Element newValue = this.microLattice.Meet(leftValue, rightValue);
- result = AddConstraint(result, left, newValue);
- result = AddConstraint(result, right, newValue);
-
- #endregion
- }
- else
- {
- ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);
-
- if (variablesInvolved.Count == 1)
- {
- #region We have just one variable
-
- IVariable var = null;
- foreach (IVariable/*!*/ v in variablesInvolved) {Contract.Assert(v != null); var = v; } // why is there no better way to get the elements?
- Contract.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/*!*/)cce.NonNull(fun.Arguments[0]);
- IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
- IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg;
-
- Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
- Contract.Assert(value != null);
- result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value);
- }
- #endregion
- }
- }
- }
- return result;
- }
+ if (IsSimpleEquality(conjunct, out left, out right)) {
+ #region The conjunct is a simple equality
- public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName){
-Contract.Requires(newName != null);
-Contract.Requires(oldName != null);
-Contract.Requires(element != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- if(IsBottom(element))
- {
- return element;
- }
- else
- {
- return ((Elt)element).Rename(oldName, newName, this.microLattice);
- }
+ Contract.Assert(left != null && right != null);
+
+ Element leftValue = result[left], rightValue = result[right];
+ if (leftValue == null) {
+ leftValue = this.microLattice.Top;
+ }
+ if (rightValue == null) {
+ rightValue = this.microLattice.Top;
+ }
+ Element newValue = this.microLattice.Meet(leftValue, rightValue);
+ result = AddConstraint(result, left, newValue);
+ result = AddConstraint(result, right, newValue);
+
+ #endregion
+ } else {
+ ISet/*<IVariable>*/ variablesInvolved = VariablesInExpression(conjunct, Set.Empty);
+
+ if (variablesInvolved.Count == 1) {
+ #region We have just one variable
+
+ IVariable var = null;
+ foreach (IVariable/*!*/ v in variablesInvolved) {
+ Contract.Assert(v != null);
+ var = v;
+ } // why is there no better way to get the elements?
+ Contract.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/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
+ IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg;
+
+ Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
+ Contract.Assert(value != null);
+ result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value);
+ }
+ #endregion
+ }
}
+ }
+ return result;
+ }
- public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args){
-Contract.Requires(args != null);
-Contract.Requires(f != null);
- return f.Equals(Prop.And) ||
- f.Equals(Value.Eq) ||
- microLattice.Understands(f, args);
- }
+ public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+ //Contract.Requires(newName != null);
+ //Contract.Requires(oldName != null);
+ //Contract.Requires(element != null);
+ //Contract.Ensures(Contract.Result<Element>() != null);
+ if (IsBottom(element)) {
+ return element;
+ } else {
+ return ((Elt)element).Rename(oldName, newName, this.microLattice);
+ }
+ }
- private sealed class EquivalentExprException :CheckedException { }
- private sealed class EquivalentExprInlineCallback
- {
- private readonly IVariable/*!*/ var;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(var != null);
- }
- public EquivalentExprInlineCallback(IVariable/*!*/ var){
-Contract.Requires(var != null);
- this.var = var;
- // base();
- }
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) {
+ Contract.Requires(args != null);
+ Contract.Requires(f != null);
+ return f.Equals(Prop.And) ||
+ f.Equals(Value.Eq) ||
+ microLattice.Understands(f, args);
+ }
- public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar)
- //throws EquivalentExprException;
- {Contract.Requires(othervar != null);
- Contract.Ensures(Contract.Result<IExpr>() != null);
- Contract.EnsuresOnThrow<EquivalentExprException>(true);
- if (othervar.Equals(var))
- throw new EquivalentExprException();
- else
- return othervar;
- }
- }
+ private sealed class EquivalentExprException : CheckedException {
+ }
+ private sealed class EquivalentExprInlineCallback {
+ private readonly IVariable/*!*/ var;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(var != null);
+ }
- public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars){
-Contract.Requires(prohibitedVars != null);
-Contract.Requires(var != null);
-Contract.Requires(expr != null);
-Contract.Requires(q != null);
-Contract.Requires(e != null);
- try
- {
- EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
- return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty),
- new OnUnableToInline(closure.ThrowOnUnableToInline));
- }
- catch (EquivalentExprException)
- {
- return null;
- }
- }
+ public EquivalentExprInlineCallback(IVariable/*!*/ var) {
+ Contract.Requires(var != null);
+ this.var = var;
+ // base();
+ }
+
+ public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar)
+ //throws EquivalentExprException;
+ {
+ Contract.Requires(othervar != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ Contract.EnsuresOnThrow<EquivalentExprException>(true);
+ if (othervar.Equals(var))
+ throw new EquivalentExprException();
+ else
+ return othervar;
+ }
+ }
+ public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars) {
+ //Contract.Requires(prohibitedVars != null);
+ //Contract.Requires(var != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(q != null);
+ //Contract.Requires(e != null);
+ try {
+ EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
+ return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty),
+ new OnUnableToInline(closure.ThrowOnUnableToInline));
+ } catch (EquivalentExprException) {
+ return null;
+ }
+ }
- /// <summary>
- /// Check to see if the given predicate holds in the given lattice element.
- ///
- /// TODO: We leave this unimplemented for now and just return maybe.
- /// </summary>
- /// <param name="e">The lattice element.</param>
- /// <param name="pred">The predicate.</param>
- /// <returns>Yes, No, or Maybe</returns>
- public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred){
-Contract.Requires(pred != null);
-Contract.Requires(e != null);
- return Answer.Maybe;
- }
- /// <summary>
- /// Answers a disequality about two variables. The same information could be obtained
- /// by asking CheckPredicate, but a different implementation may be simpler and more
- /// efficient.
- ///
- /// TODO: We leave this unimplemented for now and just return maybe.
- /// </summary>
- /// <param name="e">The lattice element.</param>
- /// <param name="var1">The first variable.</param>
- /// <param name="var2">The second variable.</param>
- /// <returns>Yes, No, or Maybe.</returns>
- public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2){
-Contract.Requires(var2 != null);
-Contract.Requires(var1 != null);
-Contract.Requires(e != null);
- return Answer.Maybe;
- }
+ /// <summary>
+ /// Check to see if the given predicate holds in the given lattice element.
+ ///
+ /// TODO: We leave this unimplemented for now and just return maybe.
+ /// </summary>
+ /// <param name="e">The lattice element.</param>
+ /// <param name="pred">The predicate.</param>
+ /// <returns>Yes, No, or Maybe</returns>
+ public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
+ //Contract.Requires(pred != null);
+ //Contract.Requires(e != null);
+ return Answer.Maybe;
+ }
- public override void Validate()
- {
- base.Validate();
- microLattice.Validate();
- }
+ /// <summary>
+ /// Answers a disequality about two variables. The same information could be obtained
+ /// by asking CheckPredicate, but a different implementation may be simpler and more
+ /// efficient.
+ ///
+ /// TODO: We leave this unimplemented for now and just return maybe.
+ /// </summary>
+ /// <param name="e">The lattice element.</param>
+ /// <param name="var1">The first variable.</param>
+ /// <param name="var2">The second variable.</param>
+ /// <returns>Yes, No, or Maybe.</returns>
+ public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
+ //Contract.Requires(var2 != null);
+ //Contract.Requires(var1 != null);
+ //Contract.Requires(e != null);
+ return Answer.Maybe;
+ }
+ public override void Validate() {
+ base.Validate();
+ microLattice.Validate();
}
+
+ }
}
|