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 | |
| 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).
26 files changed, 2930 insertions, 2782 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();
}
+
+ }
}
diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj index 66dd256e..b51afd4e 100644 --- a/Source/AbsInt/AbsInt.csproj +++ b/Source/AbsInt/AbsInt.csproj @@ -12,7 +12,7 @@ <AssemblyName>AbsInt</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/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj index b732f818..195291ec 100644 --- a/Source/Basetypes/Basetypes.csproj +++ b/Source/Basetypes/Basetypes.csproj @@ -12,7 +12,7 @@ <AssemblyName>Basetypes</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/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 6161cc57..635ccabd 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -12,7 +12,7 @@ <AssemblyName>Boogie</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/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj index 46edbd5e..34933dbf 100644 --- a/Source/CodeContractsExtender/CodeContractsExtender.csproj +++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj @@ -14,6 +14,7 @@ <FileAlignment>512</FileAlignment>
<SignAssembly>true</SignAssembly>
<AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+ <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -23,6 +24,35 @@ <DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly>
+ </CodeContractsCustomRewriterAssembly>
+ <CodeContractsCustomRewriterClass>
+ </CodeContractsCustomRewriterClass>
+ <CodeContractsLibPaths>
+ </CodeContractsLibPaths>
+ <CodeContractsExtraRewriteOptions>
+ </CodeContractsExtraRewriteOptions>
+ <CodeContractsExtraAnalysisOptions>
+ </CodeContractsExtraAnalysisOptions>
+ <CodeContractsBaseLineFile>
+ </CodeContractsBaseLineFile>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index fb9252be..a2dc77e5 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -12,7 +12,7 @@ <AssemblyName>Core</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/Graph/Graph.cs b/Source/Graph/Graph.cs index ae48d078..768f499e 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -9,803 +9,846 @@ using Microsoft.SpecSharp.Collections; using Microsoft.Contracts;
using System.Text; // for StringBuilder
using System.Diagnostics.Contracts;
-namespace Graphing{
-
-internal static class Util{
- private static string/*!*/ ListToString<T>(IEnumerable<T> xs){
- Contract.Ensures(Contract.Result<string>() != null);
- StringBuilder sb = new StringBuilder();
- sb.Append("[");
- bool first = true;
- foreach(T/*!*/ x in xs){Contract.Assert(x != null);
- if (!first) sb.Append(", ");
- sb.Append(x.ToString());
- first = false;
- }
- sb.Append("]");
- return sb.ToString();
- }
- public static string/*!*/ MapToString<Node>(Dictionary<Node,List<Node>> d){
- Contract.Ensures(Contract.Result<string>() != null);
- StringBuilder sb = new StringBuilder();
- sb.Append("{");
- bool first = true;
- foreach (KeyValuePair<Node,List<Node>> de in d){
- if (!first) sb.Append(", ");
- sb.Append(cce.NonNull( de.Key).ToString());
- sb.Append("~>");
- sb.Append(ListToString(de.Value));
- first = false;
- }
- sb.Append("}");
- return sb.ToString();
+namespace Graphing {
+
+ internal static class Util {
+ private static string/*!*/ ListToString<T>(IEnumerable<T> xs) {
+ Contract.Ensures(Contract.Result<string>() != null);
+ StringBuilder sb = new StringBuilder();
+ sb.Append("[");
+ bool first = true;
+ foreach (T/*!*/ x in xs) {
+ Contract.Assert(x != null);
+ if (!first)
+ sb.Append(", ");
+ sb.Append(x.ToString());
+ first = false;
+ }
+ sb.Append("]");
+ return sb.ToString();
+ }
+ public static string/*!*/ MapToString<Node>(Dictionary<Node, List<Node>> d) {
+ Contract.Ensures(Contract.Result<string>() != null);
+ StringBuilder sb = new StringBuilder();
+ sb.Append("{");
+ bool first = true;
+ foreach (KeyValuePair<Node, List<Node>> de in d) {
+ if (!first)
+ sb.Append(", ");
+ sb.Append(cce.NonNull(de.Key).ToString());
+ sb.Append("~>");
+ sb.Append(ListToString(de.Value));
+ first = false;
+ }
+ sb.Append("}");
+ return sb.ToString();
+ }
}
-}
-// own struct to represent possibly undefined values, because Mono does
-// not like arrays with element type T! or T?
-public struct Maybe<T> {
- private T Value;
- public bool IsSet; // initialised with false by the default ctor
- public T Val {
- get { Contract.Assume(IsSet); return Value; }
- set { Value = value; IsSet = true; }
- }
- public void UnSet() {
- IsSet = false;
+ // own struct to represent possibly undefined values, because Mono does
+ // not like arrays with element type T! or T?
+ public struct Maybe<T> {
+ private T Value;
+ public bool IsSet; // initialised with false by the default ctor
+ public T Val {
+ get {
+ Contract.Assume(IsSet);
+ return Value;
+ }
+ set {
+ Value = value;
+ IsSet = true;
+ }
+ }
+ public void UnSet() {
+ IsSet = false;
+ }
}
-}
-internal class DomRelation<Node>{
- // doms maps (unique) node numbers to the node numbers of the immediate dominator
- // to use it on Nodes, one needs the two way mapping between nodes and their numbers.
- private int[] doms; // 0 is unused: means undefined
- // here are the two mappings
- private Maybe<Node>[] postOrderNumberToNode;
- private Dictionary<Node,int> nodeToPostOrderNumber;
- private int sourceNum; // (number for) root of the graph
- private Node source; // root of the graph
- private Graph<Node> graph;
- private Dictionary<Node,List<Node>> immediateDominatorMap;
-
- [NotDelayed]
- internal DomRelation(Graph<Node> g, Node source){
- this.graph = g;
- // slot 0 not used: nodes are numbered from 1 to n so zero
- // can represent undefined.
- this.source = source;
- //:base();
- this.NewComputeDominators();
- }
- public Dictionary<Node,List<Node>> ImmediateDominatorMap{
- get { Contract.Assume( this.immediateDominatorMap != null); return this.immediateDominatorMap; }
- }
- public bool DominatedBy(Node dominee, Node dominator){
- Contract.Assume( this.nodeToPostOrderNumber != null);
- Contract.Assume(this.doms != null);
- int domineeNum = this.nodeToPostOrderNumber[dominee];
- int dominatorNum = this.nodeToPostOrderNumber[dominator];
- if (domineeNum == dominatorNum) return true;
- int currentNodeNum = this.doms[domineeNum];
- do {
- if (currentNodeNum == dominatorNum) return true;
- currentNodeNum = this.doms[currentNodeNum];
- } while (currentNodeNum != this.sourceNum);
- return false;
- }
- private Dictionary<Node,List<Node>> domMap = null;
- [Pure]
- public override string ToString(){
- Contract.Assume(this.doms != null);
- int[] localDoms = this.doms;
- Contract.Assume(this.postOrderNumberToNode != null);
- if (domMap == null){
- domMap = new Dictionary<Node,List<Node>>();
- for (int i = 1; i < localDoms.Length; i++){ // 0 slot is not used
- int domineeNum = i;
- int currentNodeNum = domineeNum;
- List<Node> dominators = new List<Node>();
- while (currentNodeNum != this.sourceNum){
- dominators.Add(this.postOrderNumberToNode[currentNodeNum].Val);
- currentNodeNum = this.doms[currentNodeNum];
- }
- dominators.Add(this.postOrderNumberToNode[this.sourceNum].Val);
- domMap.Add(this.postOrderNumberToNode[i].Val,dominators);
- }
- }
- StringBuilder sb = new StringBuilder();
- sb.Append("{");
- bool first = true;
- foreach (KeyValuePair<Node,List<Node>> de in domMap){
- if (!first) sb.Append(", ");
- sb.Append(cce.NonNull(de.Key).ToString());
- sb.Append("~>");
- sb.Append(ListToString(de.Value));
- first = false;
- }
- sb.Append("}");
- return sb.ToString();
- }
- private void PrintIntArray(int[] xs){
- Console.Write("[");
- for (int i = 0; i < xs.Length; i++){
- if (0 < i) Console.Write(", ");
- Console.Write(xs[i]);
+ internal class DomRelation<Node> {
+ // doms maps (unique) node numbers to the node numbers of the immediate dominator
+ // to use it on Nodes, one needs the two way mapping between nodes and their numbers.
+ private int[] doms; // 0 is unused: means undefined
+ // here are the two mappings
+ private Maybe<Node>[] postOrderNumberToNode;
+ private Dictionary<Node, int> nodeToPostOrderNumber;
+ private int sourceNum; // (number for) root of the graph
+ private Node source; // root of the graph
+ private Graph<Node> graph;
+ private Dictionary<Node, List<Node>> immediateDominatorMap;
+
+ [NotDelayed]
+ internal DomRelation(Graph<Node> g, Node source) {
+ this.graph = g;
+ // slot 0 not used: nodes are numbered from 1 to n so zero
+ // can represent undefined.
+ this.source = source;
+ //:base();
+ this.NewComputeDominators();
}
- Console.WriteLine("]");
- }
- public void PrintList<T>(IEnumerable<T> xs){
- Console.Write("[");
- int i = 0;
- foreach(T/*!*/ x in xs){
-Contract.Assert(x != null);
- if (0 < i) Console.Write(", ");
- Console.Write(x.ToString());
- i++;
- }
- Console.WriteLine("]");
- }
- public string/*!*/ ListToString<T>(IEnumerable<T> xs){
- Contract.Ensures(Contract.Result<string>() != null);
- StringBuilder sb = new StringBuilder();
- sb.Append("[");
- bool first = true;
- foreach(T/*!*/ x in xs){
-Contract.Assert(x != null);
- if (!first) sb.Append(", ");
- sb.Append(x.ToString());
- first = false;
- }
- sb.Append("]");
- return sb.ToString();
- }
-
- // Keith D. Cooper, Timothy J. Harvey, Ken Kennedy, "A Simple, Fast Dominance Algorithm ", Software Practice and Experience, 2001.
- // http://citeseer.ist.psu.edu/cooper01simple.html
- private void NewComputeDominators(){
- int n = this.graph.Nodes.Count;
- this.postOrderNumberToNode = new Maybe<Node>[n+1];
- this.nodeToPostOrderNumber = new Dictionary<Node,int>();
- Dictionary<Node,bool> visited = new Dictionary<Node,bool>(n);
- int currentNumber = 1;
- Contract.Assume(this.source != null);
- this.PostOrderVisit(this.source, visited, ref currentNumber);
- this.sourceNum = this.nodeToPostOrderNumber[source];
-// for (int i = 1; i <= n; i++){ Console.WriteLine(postOrderNumberToNode[i]); }
- this.doms = new int[n+1]; // 0 is unused: means undefined
- Node start_node = this.source;
- this.doms[this.nodeToPostOrderNumber[start_node]] = this.nodeToPostOrderNumber[start_node];
- bool changed = true;
-// PrintIntArray(doms);
- while (changed){
- changed = false;
- // for all nodes, b, in reverse postorder (except start_node)
- for (int nodeNum = n-1; 1 <= nodeNum; nodeNum--){
- Node b = this.postOrderNumberToNode[nodeNum].Val;
- IEnumerable<Node> predecessors = this.graph.Predecessors(b);
- // find a predecessor (i.e., a higher number) for which
- // the doms array has been set
- int new_idom = 0;
- int first_processed_predecessor = 0;
- #region new_idom <- number of first (processed) predecessor of b (pick one)
- foreach (Node p in predecessors){
- if (this.doms[this.nodeToPostOrderNumber[p]] != 0){
- int x = this.nodeToPostOrderNumber[p];
- new_idom = x;
- first_processed_predecessor = x;
- break;
+ public Dictionary<Node, List<Node>> ImmediateDominatorMap {
+ get {
+ Contract.Assume(this.immediateDominatorMap != null);
+ return this.immediateDominatorMap;
+ }
+ }
+ public bool DominatedBy(Node dominee, Node dominator) {
+ Contract.Assume(this.nodeToPostOrderNumber != null);
+ Contract.Assume(this.doms != null);
+ int domineeNum = this.nodeToPostOrderNumber[dominee];
+ int dominatorNum = this.nodeToPostOrderNumber[dominator];
+ if (domineeNum == dominatorNum)
+ return true;
+ int currentNodeNum = this.doms[domineeNum];
+ do {
+ if (currentNodeNum == dominatorNum)
+ return true;
+ currentNodeNum = this.doms[currentNodeNum];
+ } while (currentNodeNum != this.sourceNum);
+ return false;
+ }
+ private Dictionary<Node, List<Node>> domMap = null;
+ [Pure]
+ public override string ToString() {
+ Contract.Assume(this.doms != null);
+ int[] localDoms = this.doms;
+ Contract.Assume(this.postOrderNumberToNode != null);
+ if (domMap == null) {
+ domMap = new Dictionary<Node, List<Node>>();
+ for (int i = 1; i < localDoms.Length; i++) { // 0 slot is not used
+ int domineeNum = i;
+ int currentNodeNum = domineeNum;
+ List<Node> dominators = new List<Node>();
+ while (currentNodeNum != this.sourceNum) {
+ dominators.Add(this.postOrderNumberToNode[currentNodeNum].Val);
+ currentNodeNum = this.doms[currentNodeNum];
}
+ dominators.Add(this.postOrderNumberToNode[this.sourceNum].Val);
+ domMap.Add(this.postOrderNumberToNode[i].Val, dominators);
}
- #endregion
- #region for all other predecessors, p, of b
- foreach (Node p in predecessors){
- if (this.nodeToPostOrderNumber[p] == first_processed_predecessor){
- continue;
+ }
+ StringBuilder sb = new StringBuilder();
+ sb.Append("{");
+ bool first = true;
+ foreach (KeyValuePair<Node, List<Node>> de in domMap) {
+ if (!first)
+ sb.Append(", ");
+ sb.Append(cce.NonNull(de.Key).ToString());
+ sb.Append("~>");
+ sb.Append(ListToString(de.Value));
+ first = false;
+ }
+ sb.Append("}");
+ return sb.ToString();
+ }
+ private void PrintIntArray(int[] xs) {
+ Console.Write("[");
+ for (int i = 0; i < xs.Length; i++) {
+ if (0 < i)
+ Console.Write(", ");
+ Console.Write(xs[i]);
+ }
+ Console.WriteLine("]");
+ }
+ public void PrintList<T>(IEnumerable<T> xs) {
+ Console.Write("[");
+ int i = 0;
+ foreach (T/*!*/ x in xs) {
+ Contract.Assert(x != null);
+ if (0 < i)
+ Console.Write(", ");
+ Console.Write(x.ToString());
+ i++;
+ }
+ Console.WriteLine("]");
+ }
+ public string/*!*/ ListToString<T>(IEnumerable<T> xs) {
+ Contract.Ensures(Contract.Result<string>() != null);
+ StringBuilder sb = new StringBuilder();
+ sb.Append("[");
+ bool first = true;
+ foreach (T/*!*/ x in xs) {
+ Contract.Assert(x != null);
+ if (!first)
+ sb.Append(", ");
+ sb.Append(x.ToString());
+ first = false;
+ }
+ sb.Append("]");
+ return sb.ToString();
+ }
+
+ // Keith D. Cooper, Timothy J. Harvey, Ken Kennedy, "A Simple, Fast Dominance Algorithm ", Software Practice and Experience, 2001.
+ // http://citeseer.ist.psu.edu/cooper01simple.html
+ private void NewComputeDominators() {
+ int n = this.graph.Nodes.Count;
+ this.postOrderNumberToNode = new Maybe<Node>[n + 1];
+ this.nodeToPostOrderNumber = new Dictionary<Node, int>();
+ Dictionary<Node, bool> visited = new Dictionary<Node, bool>(n);
+ int currentNumber = 1;
+ Contract.Assume(this.source != null);
+ this.PostOrderVisit(this.source, visited, ref currentNumber);
+ this.sourceNum = this.nodeToPostOrderNumber[source];
+ // for (int i = 1; i <= n; i++){ Console.WriteLine(postOrderNumberToNode[i]); }
+ this.doms = new int[n + 1]; // 0 is unused: means undefined
+ Node start_node = this.source;
+ this.doms[this.nodeToPostOrderNumber[start_node]] = this.nodeToPostOrderNumber[start_node];
+ bool changed = true;
+ // PrintIntArray(doms);
+ while (changed) {
+ changed = false;
+ // for all nodes, b, in reverse postorder (except start_node)
+ for (int nodeNum = n - 1; 1 <= nodeNum; nodeNum--) {
+ Node b = this.postOrderNumberToNode[nodeNum].Val;
+ IEnumerable<Node> predecessors = this.graph.Predecessors(b);
+ // find a predecessor (i.e., a higher number) for which
+ // the doms array has been set
+ int new_idom = 0;
+ int first_processed_predecessor = 0;
+ #region new_idom <- number of first (processed) predecessor of b (pick one)
+ foreach (Node p in predecessors) {
+ if (this.doms[this.nodeToPostOrderNumber[p]] != 0) {
+ int x = this.nodeToPostOrderNumber[p];
+ new_idom = x;
+ first_processed_predecessor = x;
+ break;
+ }
+ }
+ #endregion
+ #region for all other predecessors, p, of b
+ foreach (Node p in predecessors) {
+ if (this.nodeToPostOrderNumber[p] == first_processed_predecessor) {
+ continue;
+ }
+ if (this.doms[this.nodeToPostOrderNumber[p]] != 0)
+ new_idom = intersect(this.nodeToPostOrderNumber[p], new_idom, this.doms);
}
- if (this.doms[this.nodeToPostOrderNumber[p]] != 0)
- new_idom = intersect(this.nodeToPostOrderNumber[p],new_idom,this.doms);
+ #endregion
+ if (this.doms[this.nodeToPostOrderNumber[b]] != new_idom) {
+ this.doms[this.nodeToPostOrderNumber[b]] = new_idom;
+ changed = true;
+ }
+ }
+ }
+ #region Populate the Immediate Dominator Map
+ int sourceNum = this.nodeToPostOrderNumber[this.source];
+ immediateDominatorMap = new Dictionary<Node, List<Node>>();
+ for (int i = 1; i <= n; i++) {
+ Node node = this.postOrderNumberToNode[i].Val;
+ Node idomNode = this.postOrderNumberToNode[this.doms[i]].Val;
+ if (i == sourceNum && this.doms[i] == sourceNum) {
+ continue;
}
- #endregion
- if (this.doms[this.nodeToPostOrderNumber[b]] != new_idom){
- this.doms[this.nodeToPostOrderNumber[b]] = new_idom;
- changed = true;
+ if (immediateDominatorMap.ContainsKey(idomNode)) {
+ immediateDominatorMap[idomNode].Add(node);
+ } else {
+ List<Node> l = new List<Node>();
+ l.Add(node);
+ immediateDominatorMap.Add(idomNode, l);
}
}
+ #endregion
}
- #region Populate the Immediate Dominator Map
- int sourceNum = this.nodeToPostOrderNumber[this.source];
- immediateDominatorMap = new Dictionary<Node,List<Node>>();
- for (int i = 1; i <= n; i++){
- Node node = this.postOrderNumberToNode[i].Val;
- Node idomNode = this.postOrderNumberToNode[this.doms[i]].Val;
- if ( i == sourceNum && this.doms[i] == sourceNum){
- continue;
+ private int intersect(int b1, int b2, int[] doms) {
+ int finger1 = b1;
+ int finger2 = b2;
+ while (finger1 != finger2) {
+ while (finger1 < finger2) {
+ finger1 = doms[finger1];
+ }
+ while (finger2 < finger1) {
+ finger2 = doms[finger2];
+ }
}
- if (immediateDominatorMap.ContainsKey(idomNode)){
- immediateDominatorMap[idomNode].Add(node);
- }else{
- List<Node> l = new List<Node>();
- l.Add(node);
- immediateDominatorMap.Add(idomNode,l);
+ return finger1;
+ }
+ private void PostOrderVisit(Node/*!*/ n, Dictionary<Node, bool> visited, ref int currentNumber) {
+ Contract.Requires(n != null);
+ if (visited.ContainsKey(n))
+ return;
+ visited[n] = true;
+ foreach (Node/*!*/ child in this.graph.Successors(n)) {
+ Contract.Assert(child != null);
+ PostOrderVisit(child, visited, ref currentNumber);
}
+ Contract.Assume(this.postOrderNumberToNode != null);
+ Contract.Assume(this.nodeToPostOrderNumber != null);
+ this.postOrderNumberToNode[currentNumber].Val = n;
+ this.nodeToPostOrderNumber[n] = currentNumber;
+ currentNumber++;
+ return;
}
- #endregion
}
- private int intersect(int b1, int b2, int[] doms){
- int finger1 = b1;
- int finger2 = b2;
- while (finger1 != finger2){
- while (finger1 < finger2){
- finger1 = doms[finger1];
+ public class Graph<Node> {
+ private Set<Pair<Node/*!*/, Node/*!*/>> es;
+ private Set<Node> ns;
+ private Node source;
+ private bool reducible;
+ private Set<Node> headers;
+ private Map<Node, Set<Node>> backEdgeNodes;
+ private Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>> naturalLoops;
+
+ private DomRelation<Node> dominatorMap = null;
+ private Dictionary<Node, Set<Node>> predCache = new Dictionary<Node, Set<Node>>();
+ private Dictionary<Node, Set<Node>> succCache = new Dictionary<Node, Set<Node>>();
+ private bool predComputed;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(es == null || Contract.ForAll(es, p => p.First != null && p.Second != null));
+ Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Second != null && p.First != null));
+ }
+
+
+ private class PreHeader {
+ Node/*!*/ myHeader;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(myHeader != null);
+ }
+
+ internal PreHeader(Node/*!*/ h) {
+ Contract.Requires(h != null);
+ myHeader = h;
}
- while (finger2 < finger1){
- finger2 = doms[finger2];
+
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return "#" + myHeader.ToString();
}
}
- return finger1;
- }
- private void PostOrderVisit(Node/*!*/ n, Dictionary<Node,bool> visited, ref int currentNumber){
- Contract.Requires(n != null);
- if (visited.ContainsKey(n)) return;
- visited[n] = true;
- foreach(Node/*!*/ child in this.graph.Successors(n)){
-Contract.Assert(child != null);
- PostOrderVisit(child, visited, ref currentNumber);
- }
- Contract.Assume(this.postOrderNumberToNode != null);
- Contract.Assume(this.nodeToPostOrderNumber != null);
- this.postOrderNumberToNode[currentNumber].Val = n;
- this.nodeToPostOrderNumber[n] = currentNumber;
- currentNumber++;
- return;
- }
-}
-public class Graph<Node> {
- private Set<Pair<Node/*!*/,Node/*!*/>> es;
- private Set<Node> ns;
- private Node source;
- private bool reducible;
- private Set<Node> headers;
- private Map<Node,Set<Node>> backEdgeNodes;
- private Map<Pair<Node/*!*/,Node/*!*/>,Set<Node>> naturalLoops;
-
- private DomRelation<Node> dominatorMap = null;
- private Dictionary<Node, Set<Node>> predCache = new Dictionary<Node, Set<Node>>();
- private Dictionary<Node, Set<Node>> succCache = new Dictionary<Node, Set<Node>>();
- private bool predComputed;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(es == null || Contract.ForAll(es,p=>p.First != null&&p.Second != null));
- Contract.Invariant(naturalLoops==null||Contract.ForAll(naturalLoops.Keys,p=>p.Second!=null&&p.First!=null));
-}
-
- private class PreHeader {
- Node/*!*/ myHeader;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(myHeader != null);
-}
+ public Graph(Set<Pair<Node/*!*/, Node/*!*/>> edges) {
+
+ Contract.Requires(cce.NonNullElements(edges) && Contract.ForAll(edges, p => p.First != null && p.Second != null));
+ es = edges;
+
+ // original A#
+ //ns = Set<Node>{ x : <x,y> in es } + Set<Node>{ y : <x,y> in es };
+
+ // closest Spec#
+ //ns = new Set<Node>{ Pair<Node,Node> p in edges; p.First } + new Set<Node>{ Pair<Node,Node> p in edges; p.Second };
- internal PreHeader(Node/*!*/ h) {Contract.Requires(h != null); myHeader = h; }
+ //
+ Set<Node> temp = new Set<Node>();
+ foreach (Pair<Node/*!*/, Node/*!*/> p in edges) {
+ Contract.Assert(p.First != null);
+ temp.Add(p.First);
+ Contract.Assert(p.Second != null);
+ temp.Add(p.Second);
+ }
+ ns = temp;
+ }
+ public Graph() {
+ es = new Set<Pair<Node/*!*/, Node/*!*/>>();
+ ns = new Set<Node>();
+ }
+ // BUGBUG: Set<T>.ToString() should return a non-null string
[Pure]
- public override string/*!*/ ToString() {Contract.Ensures(Contract.Result<string>() != null); return "#" + myHeader.ToString(); }
- }
+ public override string/*!*/ ToString() {
+ return "" + es.ToString();
+ }
- public Graph(Set<Pair<Node/*!*/,Node/*!*/>> edges)
- {
-
- Contract.Requires(cce.NonNullElements(edges)&&Contract.ForAll(edges,p=>p.First!=null&&p.Second!=null));
- es = edges;
-
- // original A#
- //ns = Set<Node>{ x : <x,y> in es } + Set<Node>{ y : <x,y> in es };
-
- // closest Spec#
- //ns = new Set<Node>{ Pair<Node,Node> p in edges; p.First } + new Set<Node>{ Pair<Node,Node> p in edges; p.Second };
-
- //
- Set<Node> temp = new Set<Node>();
- foreach (Pair<Node/*!*/,Node/*!*/> p in edges){
- Contract.Assert(p.First != null);
- temp.Add(p.First);
- Contract.Assert(p.Second != null);
- temp.Add(p.Second);
- }
- ns = temp;
- }
- public Graph()
- { es = new Set<Pair<Node/*!*/,Node/*!*/>>(); ns = new Set<Node>(); }
-
- // BUGBUG: Set<T>.ToString() should return a non-null string
- [Pure]
- public override string/*!*/ ToString() { return "" + es.ToString(); }
-
- public void AddSource(Node/*!*/ x)
- {
- Contract.Requires(x != null);
- // BUGBUG: This generates bad code in the compiler
- //ns += new Set<Node>{x};
- ns.Add(x);
- source = x;
- }
+ public void AddSource(Node/*!*/ x) {
+ Contract.Requires(x != null);
+ // BUGBUG: This generates bad code in the compiler
+ //ns += new Set<Node>{x};
+ ns.Add(x);
+ source = x;
+ }
- public void AddEdge(Node/*!*/ source, Node/*!*/ dest)
- {
- Contract.Requires(source != null);
- Contract.Requires(dest != null);
- //es += Set<Edge>{<source,dest>};
- //ns += Set<Node>{source, dest};
- es.Add(new Pair<Node/*!*/,Node/*!*/>(source,dest));
- ns.Add(source);
- ns.Add(dest);
- predComputed = false;
- }
+ public void AddEdge(Node/*!*/ source, Node/*!*/ dest) {
+ Contract.Requires(source != null);
+ Contract.Requires(dest != null);
+ //es += Set<Edge>{<source,dest>};
+ //ns += Set<Node>{source, dest};
+ es.Add(new Pair<Node/*!*/, Node/*!*/>(source, dest));
+ ns.Add(source);
+ ns.Add(dest);
+ predComputed = false;
+ }
- public Set<Node> Nodes { get { return ns; } }
- public IEnumerable<Pair<Node/*!*/,Node/*!*/>> Edges { get {Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Pair<Node,Node>>>())
- &&Contract.ForAll(Contract.Result<IEnumerable<Pair<Node,Node>>>(),n=>
- n.First!=null&&n.Second!=null));
- return es; } }
-
- public bool Edge(Node/*!*/ x, Node/*!*/ y) {
- Contract.Requires(x != null);
- Contract.Requires(y != null);
- // original A#
- // return <x,y> in es;
- return es.Contains(new Pair<Node/*!*/,Node/*!*/>(x,y));
- }
-
- private void ComputePredSuccCaches()
- {
- if (predComputed) return;
- predComputed = true;
- predCache = new Dictionary<Node, Set<Node>>();
- succCache = new Dictionary<Node, Set<Node>>();
-
- foreach (Node n in Nodes) {
- predCache[n] = new Set<Node>();
- succCache[n] = new Set<Node>();
- }
-
- foreach(Pair<Node/*!*/,Node/*!*/> p in Edges){
- Contract.Assert(p.First != null);
- Contract.Assert(p.Second != null);
- Set<Node> tmp;
-
- tmp = predCache[p.Second];
- tmp.Add(p.First);
- predCache[p.Second] = tmp;
-
- tmp = succCache[p.First];
- tmp.Add(p.Second);
- succCache[p.First] = tmp;
+ public Set<Node> Nodes {
+ get {
+ return ns;
+ }
+ }
+ public IEnumerable<Pair<Node/*!*/, Node/*!*/>> Edges {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Pair<Node, Node>>>())
+ && Contract.ForAll(Contract.Result<IEnumerable<Pair<Node, Node>>>(), n =>
+ n.First != null && n.Second != null));
+ return es;
+ }
+ }
+
+ public bool Edge(Node/*!*/ x, Node/*!*/ y) {
+ Contract.Requires(x != null);
+ Contract.Requires(y != null);
+ // original A#
+ // return <x,y> in es;
+ return es.Contains(new Pair<Node/*!*/, Node/*!*/>(x, y));
}
- }
- internal IEnumerable<Node> Predecessors(Node n)
- {
- // original A#
- //Set<Node> result = Set{ x : x in Nodes, Edge(x,n) };
+ private void ComputePredSuccCaches() {
+ if (predComputed)
+ return;
+ predComputed = true;
+ predCache = new Dictionary<Node, Set<Node>>();
+ succCache = new Dictionary<Node, Set<Node>>();
- ComputePredSuccCaches();
- return predCache[n];
- }
+ foreach (Node n in Nodes) {
+ predCache[n] = new Set<Node>();
+ succCache[n] = new Set<Node>();
+ }
- internal IEnumerable<Node> Successors(Node n)
- {
- ComputePredSuccCaches();
- return succCache[n];
- }
+ foreach (Pair<Node/*!*/, Node/*!*/> p in Edges) {
+ Contract.Assert(p.First != null);
+ Contract.Assert(p.Second != null);
+ Set<Node> tmp;
+
+ tmp = predCache[p.Second];
+ tmp.Add(p.First);
+ predCache[p.Second] = tmp;
- internal DomRelation<Node> /*Map<Node,Set<Node>>*/ DominatorMap
- {
- get {
- Contract.Assert(source != null);
- if (this.dominatorMap == null){
- this.dominatorMap = new DomRelation<Node>(this, this.source);
+ tmp = succCache[p.First];
+ tmp.Add(p.Second);
+ succCache[p.First] = tmp;
}
- return this.dominatorMap;
}
- }
- public Dictionary<Node,List<Node>> ImmediateDominatorMap
- {
- get {
- Contract.Assert(source != null);
- if (this.dominatorMap == null){
- this.dominatorMap = new DomRelation<Node>(this, this.source);
+ internal IEnumerable<Node> Predecessors(Node n) {
+ // original A#
+ //Set<Node> result = Set{ x : x in Nodes, Edge(x,n) };
+
+ ComputePredSuccCaches();
+ return predCache[n];
+ }
+
+ internal IEnumerable<Node> Successors(Node n) {
+ ComputePredSuccCaches();
+ return succCache[n];
+ }
+
+ internal DomRelation<Node> /*Map<Node,Set<Node>>*/ DominatorMap {
+ get {
+ Contract.Assert(source != null);
+ if (this.dominatorMap == null) {
+ this.dominatorMap = new DomRelation<Node>(this, this.source);
+ }
+ return this.dominatorMap;
}
- return this.dominatorMap.ImmediateDominatorMap;
}
- }
- public List<Node> ImmediatelyDominatedBy(Node/*!*/ n) {
- Contract.Requires(n != null);
- List<Node> dominees;
- this.ImmediateDominatorMap.TryGetValue(n, out dominees);
- return dominees == null ? new List<Node>() : dominees;
- }
- public IEnumerable<Node/*?*/> TopologicalSort()
- {
- bool acyclic;
- List<Node> sortedList;
- this.TarjanTopSort(out acyclic, out sortedList);
- return acyclic ? sortedList : new List<Node>();
- }
- // From Tarjan 1972
- public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes)
- {
- int n = this.Nodes.Count;
- if (n == 0) { acyclic = true; sortedNodes = new List<Node>(); return; }
- int[] incomingEdges = new int[n];
- // need an arbitrary numbering for the nodes to use as indices into
- // the arrays used within this algorithm
- Dictionary<Node,int> nodeToNumber = new Dictionary<Node,int>(n);
- Maybe<Node>[] numberToNode = new Maybe<Node>[n];
- int counter = 0;
- foreach (Node node in this.Nodes){
- numberToNode[counter].Val = node;
- nodeToNumber[node] = counter;
- counter++;
- }
- foreach (Pair<Node/*!*/,Node/*!*/> e in this.Edges){
- Contract.Assert(e.First != null);
- Contract.Assert(e.Second != null);
- Node/*!*/ target = e.Second;
- incomingEdges[nodeToNumber[target]]++;
- }
- List<Node> sorted = new List<Node> ();
- int sortedIndex = 0;
- while (sortedIndex < n){
- // find a root (i.e., its index)
- int rootIndex = -1;
- for (int i = 0; i < n; i++){
- if (incomingEdges[i] == 0){
- rootIndex = i;
- break;
+ public Dictionary<Node, List<Node>> ImmediateDominatorMap {
+ get {
+ Contract.Assert(source != null);
+ if (this.dominatorMap == null) {
+ this.dominatorMap = new DomRelation<Node>(this, this.source);
}
+ return this.dominatorMap.ImmediateDominatorMap;
}
- if (rootIndex == -1){
- acyclic = false; sortedNodes = new List<Node> (); return;
+ }
+ public List<Node> ImmediatelyDominatedBy(Node/*!*/ n) {
+ Contract.Requires(n != null);
+ List<Node> dominees;
+ this.ImmediateDominatorMap.TryGetValue(n, out dominees);
+ return dominees == null ? new List<Node>() : dominees;
+ }
+
+ public IEnumerable<Node/*?*/> TopologicalSort() {
+ bool acyclic;
+ List<Node> sortedList;
+ this.TarjanTopSort(out acyclic, out sortedList);
+ return acyclic ? sortedList : new List<Node>();
+ }
+ // From Tarjan 1972
+ public void TarjanTopSort(out bool acyclic, out List<Node> sortedNodes) {
+ int n = this.Nodes.Count;
+ if (n == 0) {
+ acyclic = true;
+ sortedNodes = new List<Node>();
+ return;
+ }
+ int[] incomingEdges = new int[n];
+ // need an arbitrary numbering for the nodes to use as indices into
+ // the arrays used within this algorithm
+ Dictionary<Node, int> nodeToNumber = new Dictionary<Node, int>(n);
+ Maybe<Node>[] numberToNode = new Maybe<Node>[n];
+ int counter = 0;
+ foreach (Node node in this.Nodes) {
+ numberToNode[counter].Val = node;
+ nodeToNumber[node] = counter;
+ counter++;
}
- // mark root so it won't be used again
- incomingEdges[rootIndex] = -1;
- Node root = numberToNode[rootIndex].Val; - sorted.Add(root);
- ++sortedIndex;
- foreach (Node s in this.Successors(root)){
- incomingEdges[nodeToNumber[s]]--;
+ foreach (Pair<Node/*!*/, Node/*!*/> e in this.Edges) {
+ Contract.Assert(e.First != null);
+ Contract.Assert(e.Second != null);
+ Node/*!*/ target = e.Second;
+ incomingEdges[nodeToNumber[target]]++;
+ }
+ List<Node> sorted = new List<Node>();
+ int sortedIndex = 0;
+ while (sortedIndex < n) {
+ // find a root (i.e., its index)
+ int rootIndex = -1;
+ for (int i = 0; i < n; i++) {
+ if (incomingEdges[i] == 0) {
+ rootIndex = i;
+ break;
+ }
+ }
+ if (rootIndex == -1) {
+ acyclic = false;
+ sortedNodes = new List<Node>();
+ return;
+ }
+ // mark root so it won't be used again
+ incomingEdges[rootIndex] = -1;
+ Node root = numberToNode[rootIndex].Val;
+ sorted.Add(root);
+ ++sortedIndex;
+ foreach (Node s in this.Successors(root)) {
+ incomingEdges[nodeToNumber[s]]--;
+ }
}
+ acyclic = true;
+ sortedNodes = sorted;
+ return;
}
- acyclic = true; sortedNodes = sorted; return;
- }
- private IEnumerable<Node> OldTopologicalSort()
- {
- Pair<bool,Seq<Node>> result = this.TopSort();
- return result.First ? result.Second : (IEnumerable<Node>)new Seq<Node>();
- }
- // From AsmL distribution example
- private Pair<bool,Seq<Node>> TopSort()
- {
- Seq<Node> S = new Seq<Node>();
- Set<Node> V = this.Nodes;
- Set<Node> X = new Set<Node>();
- foreach (Node/*!*/ n in V){Contract.Assert(n != null); X.Add(n); }
- bool change = true;
- while ( change )
+ private IEnumerable<Node> OldTopologicalSort() {
+ Pair<bool, Seq<Node>> result = this.TopSort();
+ return result.First ? result.Second : (IEnumerable<Node>)new Seq<Node>();
+ }
+ // From AsmL distribution example
+ private Pair<bool, Seq<Node>> TopSort() {
+ Seq<Node> S = new Seq<Node>();
+ Set<Node> V = this.Nodes;
+ Set<Node> X = new Set<Node>();
+ foreach (Node/*!*/ n in V) {
+ Contract.Assert(n != null);
+ X.Add(n);
+ }
+ bool change = true;
+ while (change)
// invariant: X = V - S
{
- change = false;
- if (X.Count > 0){
- foreach(Node/*!*/ n in X){
-Contract.Assert(n != null);
- // see if n has any incoming edges from any other node in X
- bool inDegreeZero = true;
- foreach(Node/*!*/ u in X){
-Contract.Assert(u != null);
- if (this.Edge(u,n)){
- inDegreeZero = false;
- break; // no point looking further
+ change = false;
+ if (X.Count > 0) {
+ foreach (Node/*!*/ n in X) {
+ Contract.Assert(n != null);
+ // see if n has any incoming edges from any other node in X
+ bool inDegreeZero = true;
+ foreach (Node/*!*/ u in X) {
+ Contract.Assert(u != null);
+ if (this.Edge(u, n)) {
+ inDegreeZero = false;
+ break; // no point looking further
+ }
+ }
+ if (inDegreeZero) {
+ S.Add(n);
+ X.Remove(n);
+ change = true;
+ break; // might as well go back and start looking through X from the beginning
}
}
- if (inDegreeZero){
- S.Add(n);
- X.Remove(n);
- change = true;
- break; // might as well go back and start looking through X from the beginning
+ // Then we made it all the way through X without finding a source node
+ if (!change) {
+ return new Pair<bool, Seq<Node>>(false, new Seq<Node>());
}
}
- // Then we made it all the way through X without finding a source node
- if (!change){
- return new Pair<bool,Seq<Node>>(false,new Seq<Node>());
- }
}
+ return new Pair<bool, Seq<Node>>(true, S);
}
- return new Pair<bool,Seq<Node>>(true,S);
- }
- public static bool Acyclic(Graph<Node> g, Node source)
- {
- bool acyclic;
- List<Node> sortedList;
- g.TarjanTopSort(out acyclic, out sortedList);
- return acyclic;
- }
+ public static bool Acyclic(Graph<Node> g, Node source) {
+ bool acyclic;
+ List<Node> sortedList;
+ g.TarjanTopSort(out acyclic, out sortedList);
+ return acyclic;
+ }
- //
- // [Dragon, pp. 670--671]
- // returns map D s.t. d in D(n) iff d dom n
- //
- static private Map<Node,Set<Node>> OldComputeDominators(Graph<Node> g, Node/*!*/ source){
- Contract.Requires(source != null);
- Contract.Assert(g.source != null);
- Set<Node> N = g.Nodes;
- Set<Node> nonSourceNodes = N - new Set<Node>(source);
- Map<Node,Set<Node>> D = new Map<Node,Set<Node>>();
- D[source] = new Set<Node>(source);
- foreach(Node/*!*/ n in nonSourceNodes){
-Contract.Assert(n != null);
- D[n] = N;
- }
- bool change = true;
- while ( change ){
- change = false;
- foreach(Node/*!*/ n in nonSourceNodes){
-Contract.Assert(n != null);
-
- // original A#
- //Set<Set<Node>> allPreds = new Set<Set<Node>>{ Node p in this.Predecessors(n) ; D[p] };
-
- Set<Set<Node>> allPreds = new Set<Set<Node>>();
- foreach(Node/*!*/ p in g.Predecessors(n)){
-Contract.Assert(p != null); allPreds.Add(D[p]);}
- Set<Node> temp = new Set<Node>(n) + Set<Node>.BigIntersect(allPreds);
- if ( temp != D[n] ){
- change = true;
- D[n] = temp;
+ //
+ // [Dragon, pp. 670--671]
+ // returns map D s.t. d in D(n) iff d dom n
+ //
+ static private Map<Node, Set<Node>> OldComputeDominators(Graph<Node> g, Node/*!*/ source) {
+ Contract.Requires(source != null);
+ Contract.Assert(g.source != null);
+ Set<Node> N = g.Nodes;
+ Set<Node> nonSourceNodes = N - new Set<Node>(source);
+ Map<Node, Set<Node>> D = new Map<Node, Set<Node>>();
+ D[source] = new Set<Node>(source);
+ foreach (Node/*!*/ n in nonSourceNodes) {
+ Contract.Assert(n != null);
+ D[n] = N;
+ }
+ bool change = true;
+ while (change) {
+ change = false;
+ foreach (Node/*!*/ n in nonSourceNodes) {
+ Contract.Assert(n != null);
+
+ // original A#
+ //Set<Set<Node>> allPreds = new Set<Set<Node>>{ Node p in this.Predecessors(n) ; D[p] };
+
+ Set<Set<Node>> allPreds = new Set<Set<Node>>();
+ foreach (Node/*!*/ p in g.Predecessors(n)) {
+ Contract.Assert(p != null);
+ allPreds.Add(D[p]);
+ }
+ Set<Node> temp = new Set<Node>(n) + Set<Node>.BigIntersect(allPreds);
+ if (temp != D[n]) {
+ change = true;
+ D[n] = temp;
+ }
}
}
+ return D;
}
- return D;
- }
- // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.]
- static Set<Node> NaturalLoop(Graph<Node> g, Pair<Node/*!*/,Node/*!*/> backEdge)
- {
- Contract.Requires(backEdge.First != null&&backEdge.Second!=null);
- Node/*!*/ n = backEdge.First;
- Node/*!*/ d = backEdge.Second;
- Seq<Node> stack = new Seq<Node>();
- Set<Node> loop = new Set<Node>(d);
- if ( !n.Equals(d) ) // then n is not in loop
+ // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.]
+ static Set<Node> NaturalLoop(Graph<Node> g, Pair<Node/*!*/, Node/*!*/> backEdge) {
+ Contract.Requires(backEdge.First != null && backEdge.Second != null);
+ Node/*!*/ n = backEdge.First;
+ Node/*!*/ d = backEdge.Second;
+ Seq<Node> stack = new Seq<Node>();
+ Set<Node> loop = new Set<Node>(d);
+ if (!n.Equals(d)) // then n is not in loop
{
- loop.Add(n);
- stack = new Seq<Node>(n) + stack; // push n onto stack
- }
- while ( stack.Count > 0) // not empty
+ loop.Add(n);
+ stack = new Seq<Node>(n) + stack; // push n onto stack
+ }
+ while (stack.Count > 0) // not empty
{
- Node m = stack.Head;
- stack = stack.Tail; // pop stack
- foreach(Node/*!*/ p in g.Predecessors(m)){
-Contract.Assert(p != null);
- if ( !(loop.Contains(p)) )
- {
- loop.Add(p);
- stack = new Seq<Node>(p) + stack; // push p onto stack
+ Node m = stack.Head;
+ stack = stack.Tail; // pop stack
+ foreach (Node/*!*/ p in g.Predecessors(m)) {
+ Contract.Assert(p != null);
+ if (!(loop.Contains(p))) {
+ loop.Add(p);
+ stack = new Seq<Node>(p) + stack; // push p onto stack
+ }
}
}
+ return loop;
}
- return loop;
- }
-
- internal struct ReducibleResult{
- internal bool reducible;
- internal Set<Node> headers;
- internal Map<Node,Set<Node>> backEdgeNodes;
- internal Map<Pair<Node/*!*/,Node/*!*/>,Set<Node>> naturalLoops;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Contract.ForAll(naturalLoops.Keys,p=>p.First!=null&&p.Second!=null));
-}
- internal ReducibleResult(bool b, Set<Node> headers, Map<Node,Set<Node>> backEdgeNodes, Map<Pair<Node/*!*/,Node/*!*/>,Set<Node>> naturalLoops){
- Contract.Requires(naturalLoops ==null || Contract.ForAll(naturalLoops.Keys,Key=> Key.First!=null &&Key.Second!=null));
- this.reducible = b;
- this.headers = headers;
- this.backEdgeNodes = backEdgeNodes;
- this.naturalLoops = naturalLoops;
+ internal struct ReducibleResult {
+ internal bool reducible;
+ internal Set<Node> headers;
+ internal Map<Node, Set<Node>> backEdgeNodes;
+ internal Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>> naturalLoops;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Contract.ForAll(naturalLoops.Keys, p => p.First != null && p.Second != null));
+ }
+
+ internal ReducibleResult(bool b, Set<Node> headers, Map<Node, Set<Node>> backEdgeNodes, Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>> naturalLoops) {
+ Contract.Requires(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, Key => Key.First != null && Key.Second != null));
+ this.reducible = b;
+ this.headers = headers;
+ this.backEdgeNodes = backEdgeNodes;
+ this.naturalLoops = naturalLoops;
+ }
+
}
- }
-
- // [Dragon, p. 606]
- static ReducibleResult ComputeReducible(Graph<Node> g, Node source) {
- // first, compute the dom relation
- DomRelation<Node> /*Map<Node,Set<Node>>*/ D = g.DominatorMap;
- return ComputeReducible(g,source,D);
- }
-
- // [Dragon, p. 606]
- static ReducibleResult ComputeReducible(Graph<Node> g,
- Node source,
- DomRelation<Node>/*!*/ DomRelation) {Contract.Requires(DomRelation != null);
-
- //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible");
- IEnumerable<Pair<Node/*!*/,Node/*!*/>> edges = g.Edges;
- Contract.Assert(Contract.ForAll(edges,n=>n.First != null&&n.Second!=null));
- Set<Pair<Node/*!*/,Node/*!*/>> backEdges = new Set<Pair<Node/*!*/,Node/*!*/>>();
- Set<Pair<Node/*!*/,Node/*!*/>> nonBackEdges = new Set<Pair<Node/*!*/,Node/*!*/>>();
- foreach (Pair<Node/*!*/,Node/*!*/> e in edges){
- Contract.Assert(e.First != null);
- Contract.Assert(e.Second != null);
- Node x = e.First;
- Node y = e.Second; // so there is an edge from x to y
- if ( DomRelation.DominatedBy(x,y) ){ // y dom x: which means y dominates x
- backEdges.Add(e);
- }else{
- nonBackEdges.Add(e);
- }
- }
- if ( !Acyclic(new Graph<Node>(nonBackEdges), source) ){
- return new ReducibleResult(false,
- new Set<Node>(),
- new Map<Node,Set<Node>>(),
- new Map<Pair<Node/*!*/,Node/*!*/>,Set<Node>>());
- }else{
- // original A#:
- //Set<Node> headers = Set{ d : <n,d> in backEdges };
- Set<Node> headers = new Set<Node>();
- foreach(Pair<Node/*!*/,Node/*!*/> e in backEdges){
+ // [Dragon, p. 606]
+ static ReducibleResult ComputeReducible(Graph<Node> g, Node source) {
+ // first, compute the dom relation
+ DomRelation<Node> /*Map<Node,Set<Node>>*/ D = g.DominatorMap;
+ return ComputeReducible(g, source, D);
+ }
+ // [Dragon, p. 606]
+ static ReducibleResult ComputeReducible(Graph<Node> g,
+ Node source,
+ DomRelation<Node>/*!*/ DomRelation) {
+ Contract.Requires(DomRelation != null);
+
+ //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible");
+ IEnumerable<Pair<Node/*!*/, Node/*!*/>> edges = g.Edges;
+ Contract.Assert(Contract.ForAll(edges, n => n.First != null && n.Second != null));
+ Set<Pair<Node/*!*/, Node/*!*/>> backEdges = new Set<Pair<Node/*!*/, Node/*!*/>>();
+ Set<Pair<Node/*!*/, Node/*!*/>> nonBackEdges = new Set<Pair<Node/*!*/, Node/*!*/>>();
+ foreach (Pair<Node/*!*/, Node/*!*/> e in edges) {
Contract.Assert(e.First != null);
Contract.Assert(e.Second != null);
- headers.Add(e.Second);}
- // original A#:
- //Map<Node,Set<Node>> backEdgeNodes = Map{ h -> bs : h in headers, bs = Set<Node>{ b : <b,x> in backEdges, x == h } };
- Map<Node,Set<Node>> backEdgeNodes = new Map<Node,Set<Node>>();
- foreach(Node/*!*/ h in headers){
-Contract.Assert(h != null);
- Set<Node> bs = new Set<Node>();
- foreach(Pair<Node,Node> backedge in backEdges){
- Contract.Assert(backedge.First != null);
- Contract.Assert(backedge.Second != null);
- if (backedge.Second.Equals(h)){
- bs.Add(backedge.First);
+ Node x = e.First;
+ Node y = e.Second; // so there is an edge from x to y
+ if (DomRelation.DominatedBy(x, y)) { // y dom x: which means y dominates x
+ backEdges.Add(e);
+ } else {
+ nonBackEdges.Add(e);
+ }
+ }
+ if (!Acyclic(new Graph<Node>(nonBackEdges), source)) {
+ return new ReducibleResult(false,
+ new Set<Node>(),
+ new Map<Node, Set<Node>>(),
+ new Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>>());
+ } else {
+ // original A#:
+ //Set<Node> headers = Set{ d : <n,d> in backEdges };
+ Set<Node> headers = new Set<Node>();
+ foreach (Pair<Node/*!*/, Node/*!*/> e in backEdges) {
+
+ Contract.Assert(e.First != null);
+ Contract.Assert(e.Second != null);
+ headers.Add(e.Second);
+ }
+ // original A#:
+ //Map<Node,Set<Node>> backEdgeNodes = Map{ h -> bs : h in headers, bs = Set<Node>{ b : <b,x> in backEdges, x == h } };
+ Map<Node, Set<Node>> backEdgeNodes = new Map<Node, Set<Node>>();
+ foreach (Node/*!*/ h in headers) {
+ Contract.Assert(h != null);
+ Set<Node> bs = new Set<Node>();
+ foreach (Pair<Node, Node> backedge in backEdges) {
+ Contract.Assert(backedge.First != null);
+ Contract.Assert(backedge.Second != null);
+ if (backedge.Second.Equals(h)) {
+ bs.Add(backedge.First);
+ }
}
+ backEdgeNodes.Add(h, bs);
}
- backEdgeNodes.Add(h,bs);
+
+ // original A#:
+ //Map<Pair<Node,Node>,Set<Node>> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges };
+ Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>> naturalLoops = new Map<Pair<Node/*!*/, Node/*!*/>, Set<Node>>();
+ foreach (Pair<Node/*!*/, Node/*!*/> e in backEdges) {
+ Contract.Assert(e.First != null && e.Second != null);
+ naturalLoops.Add(e, NaturalLoop(g, e));
+ }
+
+ //Console.WriteLine("[" + DateTime.Now +"]: end ComputeReducible");
+ return new ReducibleResult(true, headers, backEdgeNodes, naturalLoops);
}
+ }
+ public bool Reducible {
+ get {
+ return reducible;
+ }
+ }
+ public IEnumerable<Node> Headers {
+ get {
+ return headers;
+ }
+ }
+ public IEnumerable<Node> BackEdgeNodes(Node/*!*/ h) {
+ Contract.Requires(h != null);
// original A#:
- //Map<Pair<Node,Node>,Set<Node>> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges };
- Map<Pair<Node/*!*/,Node/*!*/>,Set<Node>> naturalLoops = new Map<Pair<Node/*!*/,Node/*!*/>,Set<Node>>();
- foreach (Pair<Node/*!*/,Node/*!*/> e in backEdges){
- Contract.Assert(e.First != null&&e.Second!=null);
- naturalLoops.Add(e,NaturalLoop(g,e));
+ //return h in backEdgeNodes ? backEdgeNodes[h] : null;
+ return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable<Node>)new Seq<Node>());
+ }
+ public IEnumerable<Node> NaturalLoops(Node/*!*/ header, Node/*!*/ backEdgeNode) {
+ Contract.Requires(header != null);
+ Contract.Requires(backEdgeNode != null);
+ Pair<Node/*!*/, Node/*!*/> e = new Pair<Node/*!*/, Node/*!*/>(backEdgeNode, header);
+ return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable<Node>)new Seq<Node>();
+ }
+
+ public void ComputeLoops() {
+ ReducibleResult r = ComputeReducible(this, this.source);
+ this.reducible = r.reducible;
+ this.headers = r.headers;
+ this.backEdgeNodes = r.backEdgeNodes;
+ this.naturalLoops = r.naturalLoops;
+ return;
+ }
+
+
+ } // end: class Graph
+
+ public class GraphProgram {
+ static void TestGraph<T>(T/*!*/ source, params Pair<T/*!*/, T/*!*/>[] edges) {
+ Contract.Requires(source != null);
+ Contract.Requires(Contract.ForAll(edges, pair => pair.First != null && pair.Second != null));
+ Set<Pair<T/*!*/, T/*!*/>> es = new Set<Pair<T/*!*/, T/*!*/>>();
+ foreach (Pair<T/*!*/, T/*!*/> e in edges) {
+ Contract.Assert(e.First != null && e.Second != null);
+ es.Add(e);
}
-
- //Console.WriteLine("[" + DateTime.Now +"]: end ComputeReducible");
- return new ReducibleResult(true, headers, backEdgeNodes, naturalLoops);
+ Graph<T> g = new Graph<T>(es);
+ g.AddSource(source);
+ Console.WriteLine("G = " + g);
+ g.ComputeLoops();
+ Console.WriteLine("G's Dominator Map = " + g.DominatorMap);
+ Console.WriteLine("G's Immediate Dominator Map = " + Util.MapToString(g.ImmediateDominatorMap));
+ Console.WriteLine("G is reducible: " + (g.Reducible ? "yes" : "no"));
}
- }
- public bool Reducible { get { return reducible; } }
- public IEnumerable<Node> Headers { get { return headers; } }
- public IEnumerable<Node> BackEdgeNodes(Node/*!*/ h){
- Contract.Requires(h != null);
- // original A#:
- //return h in backEdgeNodes ? backEdgeNodes[h] : null;
- return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable<Node>)new Seq<Node>());
- }
- public IEnumerable<Node> NaturalLoops(Node/*!*/ header, Node/*!*/ backEdgeNode)
- {
- Contract.Requires(header != null);
- Contract.Requires(backEdgeNode!=null);
- Pair<Node/*!*/,Node/*!*/> e = new Pair<Node/*!*/,Node/*!*/>(backEdgeNode,header);
- return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable<Node>)new Seq<Node>();
- }
+ static void Main(string[] args)
+ //requires forall{string s in args; s != null};
+ {
+ Console.WriteLine("Spec# says hello!");
+ // This generates bad IL -- need to fix a bug in the compiler
+ //Graph<int> g = new Graph<int>(new Set<Pair<int,int>>{ new Pair<int,int>(1,2), new Pair<int,int>(1,3), new Pair<int,int>(2,3) });
+
+ Console.WriteLine("");
+ TestGraph<char>('a',
+ new Pair<char, char>('a', 'b'),
+ new Pair<char, char>('a', 'c'),
+ new Pair<char, char>('b', 'c')
+ );
+
+ Console.WriteLine("");
+ TestGraph<char>('a',
+ new Pair<char, char>('a', 'b'),
+ new Pair<char, char>('a', 'c'),
+ new Pair<char, char>('b', 'd'),
+ new Pair<char, char>('c', 'e'),
+ new Pair<char, char>('c', 'f'),
+ new Pair<char, char>('d', 'e'),
+ new Pair<char, char>('e', 'd'),
+ new Pair<char, char>('e', 'f'),
+ new Pair<char, char>('f', 'e')
+ );
+
+ Console.WriteLine("");
+ TestGraph<char>('a',
+ new Pair<char, char>('a', 'b'),
+ new Pair<char, char>('a', 'c'),
+ new Pair<char, char>('b', 'c'),
+ new Pair<char, char>('c', 'b')
+ );
+
+ Console.WriteLine("");
+ TestGraph<int>(1,
+ new Pair<int, int>(1, 2),
+ new Pair<int, int>(1, 3),
+ new Pair<int, int>(2, 3)
+ );
+
+ Console.WriteLine("");
+ TestGraph<int>(1,
+ new Pair<int, int>(1, 2),
+ new Pair<int, int>(1, 3),
+ new Pair<int, int>(2, 3),
+ new Pair<int, int>(3, 2)
+ );
+
+ Console.WriteLine("");
+ TestGraph<int>(2,
+ new Pair<int, int>(2, 3),
+ new Pair<int, int>(2, 4),
+ new Pair<int, int>(3, 2)
+ );
+
+ Console.WriteLine("");
+ TestGraph<char>('a',
+ new Pair<char, char>('a', 'b'),
+ new Pair<char, char>('a', 'c'),
+ new Pair<char, char>('b', 'c'),
+ new Pair<char, char>('b', 'b')
+ );
- public void ComputeLoops()
- {
- ReducibleResult r = ComputeReducible(this,this.source);
- this.reducible = r.reducible;
- this.headers = r.headers;
- this.backEdgeNodes = r.backEdgeNodes;
- this.naturalLoops = r.naturalLoops;
- return;
- }
-
-
-} // end: class Graph
-
-public class GraphProgram
-{
- static void TestGraph<T>(T/*!*/ source, params Pair<T/*!*/,T/*!*/>[] edges){
- Contract.Requires(source != null);
- Contract.Requires(Contract.ForAll(edges,pair=>pair.First!=null&&pair.Second!=null));
- Set<Pair<T/*!*/,T/*!*/>> es = new Set<Pair<T/*!*/,T/*!*/>>();
- foreach (Pair<T/*!*/,T/*!*/> e in edges){Contract.Assert(e.First != null &&e.Second!=null); es.Add(e);}
- Graph<T> g = new Graph<T>(es);
- g.AddSource(source);
- Console.WriteLine("G = " + g);
- g.ComputeLoops();
- Console.WriteLine("G's Dominator Map = " + g.DominatorMap);
- Console.WriteLine("G's Immediate Dominator Map = " + Util.MapToString(g.ImmediateDominatorMap));
- Console.WriteLine("G is reducible: " + (g.Reducible ? "yes" : "no"));
- }
- static void Main(string[] args)
- //requires forall{string s in args; s != null};
- {
- Console.WriteLine("Spec# says hello!");
- // This generates bad IL -- need to fix a bug in the compiler
- //Graph<int> g = new Graph<int>(new Set<Pair<int,int>>{ new Pair<int,int>(1,2), new Pair<int,int>(1,3), new Pair<int,int>(2,3) });
-
- Console.WriteLine("");
- TestGraph<char>('a',
- new Pair<char,char>('a','b'),
- new Pair<char,char>('a','c'),
- new Pair<char,char>('b','c')
- );
-
- Console.WriteLine("");
- TestGraph<char>('a',
- new Pair<char,char>('a','b'),
- new Pair<char,char>('a','c'),
- new Pair<char,char>('b','d'),
- new Pair<char,char>('c','e'),
- new Pair<char,char>('c','f'),
- new Pair<char,char>('d','e'),
- new Pair<char,char>('e','d'),
- new Pair<char,char>('e','f'),
- new Pair<char,char>('f','e')
- );
-
- Console.WriteLine("");
- TestGraph<char>('a',
- new Pair<char,char>('a','b'),
- new Pair<char,char>('a','c'),
- new Pair<char,char>('b','c'),
- new Pair<char,char>('c','b')
- );
-
- Console.WriteLine("");
- TestGraph<int>(1,
- new Pair<int,int>(1,2),
- new Pair<int,int>(1,3),
- new Pair<int,int>(2,3)
- );
-
- Console.WriteLine("");
- TestGraph<int>(1,
- new Pair<int,int>(1,2),
- new Pair<int,int>(1,3),
- new Pair<int,int>(2,3),
- new Pair<int,int>(3,2)
- );
-
- Console.WriteLine("");
- TestGraph<int>(2,
- new Pair<int,int>(2,3),
- new Pair<int,int>(2,4),
- new Pair<int,int>(3,2)
- );
-
- Console.WriteLine("");
- TestGraph<char>('a',
- new Pair<char,char>('a','b'),
- new Pair<char,char>('a','c'),
- new Pair<char,char>('b','c'),
- new Pair<char,char>('b','b')
- );
-
-
+ }
}
-}
}
diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj index 1756b36f..f6b5c854 100644 --- a/Source/Graph/Graph.csproj +++ b/Source/Graph/Graph.csproj @@ -12,7 +12,7 @@ <AssemblyName>Graph</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/Provers/Isabelle/Isabelle.csproj b/Source/Provers/Isabelle/Isabelle.csproj index 2db71715..364667bb 100644 --- a/Source/Provers/Isabelle/Isabelle.csproj +++ b/Source/Provers/Isabelle/Isabelle.csproj @@ -14,7 +14,7 @@ <FileAlignment>512</FileAlignment>
<SignAssembly>true</SignAssembly>
<AssemblyOriginatorKeyFile>..\..\InterimKey.snk</AssemblyOriginatorKeyFile>
- <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+ <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj index fd83f893..d776642f 100644 --- a/Source/Provers/SMTLib/SMTLib.csproj +++ b/Source/Provers/SMTLib/SMTLib.csproj @@ -12,7 +12,7 @@ <AssemblyName>Provers.SMTLib</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/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj index 368f6723..f4c41511 100644 --- a/Source/Provers/Simplify/Simplify.csproj +++ b/Source/Provers/Simplify/Simplify.csproj @@ -12,7 +12,7 @@ <AssemblyName>Provers.Simplify</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/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj index 8755d6c2..114544f4 100644 --- a/Source/Provers/Z3/Z3.csproj +++ b/Source/Provers/Z3/Z3.csproj @@ -12,7 +12,7 @@ <AssemblyName>Provers.Z3</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/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 45533115..a33ea631 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -117,7 +117,7 @@ namespace Microsoft.Boogie.TypeErasure { public static List<KeyValuePair<T1, T2>>/*!*/ ToPairList<T1, T2>(IDictionary<T1, T2> dict) {
Contract.Requires((dict != null));
-Contract.Ensures(Contract.Result<List<KeyValuePair<T1, T2>>>() != null);
+ Contract.Ensures(Contract.Result<List<KeyValuePair<T1, T2>>>() != null);
List<KeyValuePair<T1, T2>>/*!*/ res = new List<KeyValuePair<T1, T2>>(dict);
return res;
}
@@ -539,7 +539,8 @@ Contract.Ensures(Contract.Result<List<KeyValuePair<T1, T2>>>() != null); [ContractClassFor(typeof(TypeAxiomBuilder))]
public abstract class TypeAxiomBuilderContracts : TypeAxiomBuilder {
- public TypeAxiomBuilderContracts() : base((VCExpressionGenerator)null) {
+ public TypeAxiomBuilderContracts()
+ : base((VCExpressionGenerator)null) {
}
internal override MapTypeAbstractionBuilder MapTypeAbstracter {
get {
@@ -614,9 +615,9 @@ Contract.Ensures(Contract.Result<List<KeyValuePair<T1, T2>>>() != null); protected VCExpr GenReverseCastEq(Function castToU, Function castFromU, out VCExprVar var, out List<VCTrigger/*!*/>/*!*/ triggers) {
Contract.Requires((castFromU != null));
-Contract.Requires((castToU != null));
-Contract.Requires((cce.NonNullElements(Contract.ValueAtReturn(out triggers))));
-Contract.Ensures(Contract.ValueAtReturn(out var) != null);
+ Contract.Requires((castToU != null));
+ Contract.Requires((cce.NonNullElements(Contract.ValueAtReturn(out triggers))));
+ Contract.Ensures(Contract.ValueAtReturn(out var) != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
var = Gen.Variable("x", U);
@@ -764,7 +765,8 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null); [ContractClassFor(typeof(TypeAxiomBuilderIntBoolU))]
public abstract class TypeAxiomBuilderIntBoolUContracts : TypeAxiomBuilderIntBoolU {
- public TypeAxiomBuilderIntBoolUContracts():base((TypeAxiomBuilderIntBoolU)null){
+ public TypeAxiomBuilderIntBoolUContracts()
+ : base((TypeAxiomBuilderIntBoolU)null) {
}
protected override VCExpr GenReverseCastAxiom(Function castToU, Function castFromU) {
Contract.Requires(castToU != null);
@@ -920,14 +922,14 @@ Contract.Ensures(Contract.ValueAtReturn(out var) != null); public Function Select(MapType rawType, out TypeSeq instantiations) {
Contract.Requires((rawType != null));
-Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
Contract.Ensures(Contract.Result<Function>() != null);
return AbstractAndGetRepresentation(rawType, out instantiations).Select;
}
public Function Store(MapType rawType, out TypeSeq instantiations) {
Contract.Requires((rawType != null));
-Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
Contract.Ensures(Contract.Result<Function>() != null);
return AbstractAndGetRepresentation(rawType, out instantiations).Store;
}
@@ -935,7 +937,7 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); private MapTypeClassRepresentation
AbstractAndGetRepresentation(MapType rawType, out TypeSeq instantiations) {
Contract.Requires((rawType != null));
-Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null);
instantiations = new TypeSeq();
MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations);
return GetClassRepresentation(abstraction);
@@ -978,7 +980,7 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))
return rawType;
- if (Contract.ForAll(0,rawType.FreeVariables.Length, var => !boundTypeParams.Has(rawType.FreeVariables[ var]))) {
+ if (Contract.ForAll(0, rawType.FreeVariables.Length, var => !boundTypeParams.Has(rawType.FreeVariables[var]))) {
// Bingo!
// if the type does not contain any bound variables, we can simply
// replace it with a type variable
@@ -1022,7 +1024,8 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); }
[ContractClassFor(typeof(MapTypeAbstractionBuilder))]
internal abstract class MapTypeAbstractionBuilderContracts : MapTypeAbstractionBuilder {
- public MapTypeAbstractionBuilderContracts() : base(null, null) {
+ public MapTypeAbstractionBuilderContracts()
+ : base(null, null) {
}
protected override void GenSelectStoreFunctions(MapType abstractedType, TypeCtorDecl synonymDecl, out Function select, out Function store) {
Contract.Requires(abstractedType != null);
@@ -1099,7 +1102,8 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); ////////////////////////////////////////////////////////////////////////////
- public TypeEraser(TypeAxiomBuilderIntBoolU axBuilder, VCExpressionGenerator gen):base(gen) {
+ public TypeEraser(TypeAxiomBuilderIntBoolU axBuilder, VCExpressionGenerator gen)
+ : base(gen) {
Contract.Requires(gen != null);
Contract.Requires(axBuilder != null);
AxBuilder = axBuilder;
@@ -1270,7 +1274,8 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); [ContractClassFor(typeof(TypeEraser))]
public abstract class TypeEraserContracts : TypeEraser {
- public TypeEraserContracts() : base(null, null) {
+ public TypeEraserContracts()
+ : base(null, null) {
}
protected override OpTypeEraser OpEraser {
get {
@@ -1317,8 +1322,8 @@ Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); private List<VCExpr/*!*/>/*!*/ MutateSeq(VCExprNAry node, VariableBindings bindings, int newPolarity) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
+ Contract.Requires((node != null));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
int oldPolarity = Eraser.Polarity;
Eraser.Polarity = newPolarity;
List<VCExpr/*!*/>/*!*/ newArgs = Eraser.MutateSeq(node, bindings);
@@ -1342,7 +1347,7 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>())); Contract.Requires(bindings != null);
Contract.Requires(node != null);
Contract.Requires((node.Arity > 0));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, newPolarity);
Type/*!*/ oldType = node[0].Type;
@@ -1357,26 +1362,26 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); public override VCExpr VisitNotOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Bool, bindings, -Eraser.Polarity);
}
public override VCExpr VisitEqOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArgumentsToOldType(node, bindings, 0);
}
public override VCExpr VisitNeqOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArgumentsToOldType(node, bindings, 0);
}
public override VCExpr VisitImpliesOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
// UGLY: the code for tracking polarities should be factored out
List<VCExpr/*!*/>/*!*/ newArgs = new List<VCExpr/*!*/>(2);
Eraser.Polarity = -Eraser.Polarity;
@@ -1387,22 +1392,22 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); }
public override VCExpr VisitDistinctOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArgumentsToOldType(node, bindings, 0);
}
public override VCExpr VisitLabelOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
// argument of the label operator should always be a formula
// (at least for Simplify ... should this be ensured at a later point?)
return CastArguments(node, Type.Bool, bindings, Eraser.Polarity);
}
public override VCExpr VisitIfThenElseOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, 0);
newArgs[0] = AxBuilder.Cast(newArgs[0], Type.Bool);
Type t = node.Type;
@@ -1413,7 +1418,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); newArgs[2] = AxBuilder.Cast(newArgs[2], t);
return Gen.Function(node.Op, newArgs);
}
- public override VCExpr/*!*/ VisitCustomOp (VCExprNAry/*!*/ node, VariableBindings/*!*/ bindings) {
+ public override VCExpr/*!*/ VisitCustomOp(VCExprNAry/*!*/ node, VariableBindings/*!*/ bindings) {
Contract.Requires(node != null);
Contract.Requires(bindings != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1423,68 +1428,68 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); }
public override VCExpr VisitAddOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
public override VCExpr VisitSubOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
public override VCExpr VisitMulOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
public override VCExpr VisitDivOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
public override VCExpr VisitModOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
public override VCExpr VisitLtOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
public override VCExpr VisitLeOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
public override VCExpr VisitGtOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
public override VCExpr VisitGeOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
public override VCExpr VisitSubtypeOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, AxBuilder.U, bindings, 0);
}
public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArgumentsToOldType(node, bindings, 0);
}
public override VCExpr VisitBvExtractOp(VCExprNAry node, VariableBindings bindings) {
@@ -1495,8 +1500,8 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); }
public override VCExpr VisitBvConcatOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
-Contract.Requires((node != null));
-Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
List<VCExpr/*!*/>/*!*/ newArgs = MutateSeq(node, bindings, 0);
// each argument is cast to its old type
@@ -1524,24 +1529,29 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); /// variables of "newNode".
/// </summary>
public static List<VCExprVar/*!*/>/*!*/ FindCastVariables(VCExprQuantifier oldNode, VCExprQuantifier newNode, TypeAxiomBuilderIntBoolU axBuilder) {
-Contract.Requires((axBuilder != null));
-Contract.Requires((newNode != null));
-Contract.Requires((oldNode != null));
-Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
+ Contract.Requires((axBuilder != null));
+ Contract.Requires((newNode != null));
+ Contract.Requires((oldNode != null));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
VariableCastCollector/*!*/ collector = new VariableCastCollector(axBuilder);
Contract.Assert(collector != null);
- if (Contract.Exists(newNode.Triggers, trigger=> trigger.Pos)) {
+ if (Contract.Exists(newNode.Triggers, trigger => trigger.Pos)) {
// look in the given triggers
- foreach (VCTrigger/*!*/ trigger in newNode.Triggers){Contract.Assert(trigger != null);
- if (trigger.Pos){
- foreach (VCExpr/*!*/ expr in trigger.Exprs){Contract.Assert(expr != null);
- collector.Traverse(expr, true);}}}
+ foreach (VCTrigger/*!*/ trigger in newNode.Triggers) {
+ Contract.Assert(trigger != null);
+ if (trigger.Pos) {
+ foreach (VCExpr/*!*/ expr in trigger.Exprs) {
+ Contract.Assert(expr != null);
+ collector.Traverse(expr, true);
+ }
+ }
+ }
} else {
// look in the body of the quantifier
collector.Traverse(newNode.Body, true);
}
- List<VCExprVar/*!*/>/*!*/ castVariables = new List<VCExprVar/*!*/> (collector.varsInCasts.Count);
+ List<VCExprVar/*!*/>/*!*/ castVariables = new List<VCExprVar/*!*/>(collector.varsInCasts.Count);
foreach (VCExprVar/*!*/ castVar in collector.varsInCasts) {
Contract.Assert(castVar != null);
int i = newNode.BoundVars.IndexOf(castVar);
@@ -1574,8 +1584,8 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>())); return true; // not used
}
- public override bool Visit(VCExprNAry node, bool arg){
-Contract.Requires(node != null);
+ public override bool Visit(VCExprNAry node, bool arg) {
+ Contract.Requires(node != null);
if (node.Op is VCExprBoogieFunctionOp) {
Function func = ((VCExprBoogieFunctionOp)node.Op).Func;
Contract.Assert(func != null);
@@ -1587,7 +1597,7 @@ Contract.Requires(node != null); }
} else if (node.Op is VCExprNAryOp) {
VCExpressionGenerator.SingletonOp op = VCExpressionGenerator.SingletonOpDict[node.Op];
- switch(op) {
+ switch (op) {
// the following operators cannot be used in triggers, so disregard any uses of variables as direct arguments
case VCExpressionGenerator.SingletonOp.NotOp:
case VCExpressionGenerator.SingletonOp.EqOp:
@@ -1601,7 +1611,7 @@ Contract.Requires(node != null); case VCExpressionGenerator.SingletonOp.GeOp:
foreach (VCExpr n in node) {
if (!(n is VCExprVar)) { // don't recurse on VCExprVar argument
- n.Accept<bool,bool>(this, arg);
+ n.Accept<bool, bool>(this, arg);
}
}
return true;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 23f5c804..209248ed 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -246,7 +246,7 @@ namespace VC { }
}
[ContractClassFor(typeof(ConditionGeneration))]
- public class ConditionGenerationContracts : ConditionGeneration {
+ public abstract class ConditionGenerationContracts : ConditionGeneration {
public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {
Contract.Requires(impl != null);
Contract.Requires(program != null);
@@ -254,7 +254,8 @@ namespace VC { Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
throw new NotImplementedException();
}
- public ConditionGenerationContracts(Program p) : base(p) {
+ public ConditionGenerationContracts(Program p)
+ : base(p) {
}
}
@@ -304,7 +305,7 @@ namespace VC { public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {
Contract.Requires(impl != null);
Contract.Requires(program != null);
- Contract.Requires(Contract.ForAll(Contract.ValueAtReturn(out errors),i=>i!=null));
+ Contract.Requires(Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));
Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
@@ -325,7 +326,7 @@ namespace VC { public Outcome StratifiedVerifyImplementation(Implementation impl, Program program, out List<Counterexample>/*?*/ errors) {
Contract.Requires(impl != null);
Contract.Requires(program != null);
- Contract.Requires(Contract.ForAll(Contract.ValueAtReturn(out errors),i=>i!=null));
+ Contract.Requires(Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));
Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || errors != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
Helpers.ExtraTraceInformation("Starting implementation verification");
@@ -345,7 +346,7 @@ namespace VC { public abstract Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback);
public virtual Outcome StratifiedVerifyImplementation(Implementation impl, Program program, VerifierCallback callback) {
-
+
Contract.Requires(impl != null);
Contract.Requires(program != null);
Contract.Requires(callback != null);
@@ -1085,7 +1086,7 @@ namespace VC { }
#endregion
#region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below]
- else if (c is AssignCmd) {
+ else if (c is AssignCmd) {
AssignCmd assign = ((AssignCmd)c).AsSimpleAssignCmd; // first remove map assignments
Contract.Assert(assign != null);
#region Substitute all variables in E with the current map
@@ -1155,7 +1156,7 @@ namespace VC { }
#endregion
#region havoc w |--> assume whereClauses, out := in( w |-> w' )
- else if (c is HavocCmd) {
+ else if (c is HavocCmd) {
if (this.preHavocIncarnationMap == null) // Save a copy of the incarnation map (at the top of a sequence of havoc statements)
this.preHavocIncarnationMap = (Hashtable)incarnationMap.Clone();
@@ -1186,7 +1187,7 @@ namespace VC { }
}
#endregion
- else if (c is CommentCmd) {
+ else if (c is CommentCmd) {
// comments are just for debugging and don't affect verification
} else if (c is SugaredCmd) {
SugaredCmd sug = (SugaredCmd)c;
@@ -1218,7 +1219,7 @@ namespace VC { }
}
#region There shouldn't be any other types of commands at this point
- else {
+ else {
Debug.Fail("Internal Error: Passive transformation handed a command that is not one of assert,assume,havoc,assign.");
}
#endregion
|