context: //-----------------------------------------------------------------------------
  //
  // Copyright (c) Microsoft. All rights reserved.
  // This code is licensed under the Microsoft Public License.
  // THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF
  // ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY
  // IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR
  // PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT.
  //
  //-----------------------------------------------------------------------------
  using System;
  using System.Collections.Generic;
  using System.Text;
  using System.Diagnostics.Contracts;
  using Microsoft.Cci.Immutable;
  
  //^ using Microsoft.Contracts;
  
  namespace Microsoft.Cci {
  
    /// <summary>
    /// Helper class for computing information from the structure of ITypeDefinitionMember instances.
    /// </summary>
    public static class MemberHelper {
  
      /// <summary>
      /// Returns the number of bytes that separate the start of an instance of the items's declaring type from the start of the field itself.
      /// </summary>
      /// <param name="item">The item (field or nested type) of interests, which must not be static. </param>
      /// <param name="containingTypeDefinition">The type containing the item.</param>
      /// <returns></returns>
      public static uint ComputeFieldOffset(ITypeDefinitionMember item, ITypeDefinition containingTypeDefinition)
        //^ requires !field.IsStatic; 
      {
        Contract.Requires(item != null);
        Contract.Requires(containingTypeDefinition != null);
  
        uint result = 0;
        ushort bitFieldAlignment = 0;
        uint bitOffset = 0;
  
        IEnumerable<ITypeDefinitionMember> members = containingTypeDefinition.Members;
        if (containingTypeDefinition.Layout == LayoutKind.Sequential) {
          List<IFieldDefinition> fields = new List<IFieldDefinition>(IteratorHelper.GetFilterEnumerable<ITypeDefinitionMember, IFieldDefinition>(members));
          fields.Sort(delegate(IFieldDefinition f1, IFieldDefinition f2) { return f1.SequenceNumber - f2.SequenceNumber; });
          members = IteratorHelper.GetConversionEnumerable<IFieldDefinition, ITypeDefinitionMember>(fields);
        }
  
        foreach (ITypeDefinitionMember member in members) {
          INestedTypeDefinition fieldAsTypeDef = member as INestedTypeDefinition;
          if (fieldAsTypeDef != null && fieldAsTypeDef == item) {
            ushort typeAlignment = (ushort)(TypeHelper.TypeAlignment(fieldAsTypeDef.ResolvedType) * 8);
            return (((result + typeAlignment - 1) / typeAlignment) * typeAlignment) / 8;
          } else {
            IFieldDefinition/*?*/ f = member as IFieldDefinition;
            if (f == null || f.IsStatic) continue;
            if (f.Type.ResolvedType == item) continue; // in case we are calculating the offset of an anonymous type, skip the implicit field of that type
            ushort fieldAlignment = (ushort)(TypeHelper.TypeAlignment(f.Type.ResolvedType) * 8);
            if (f == item) {
              if (f.IsBitField && bitOffset > 0 && bitOffset + f.BitLength <= bitFieldAlignment) return (result - bitOffset) / 8;
              if (bitFieldAlignment > fieldAlignment) fieldAlignment = bitFieldAlignment;
              return (((result + fieldAlignment - 1) / fieldAlignment) * fieldAlignment) / 8;
            }
            uint fieldSize;
            if (f.IsBitField) {
              bitFieldAlignment = fieldAlignment;
              fieldSize = f.BitLength;
              if (bitOffset > 0 && bitOffset + fieldSize > fieldAlignment)
                bitOffset = 0;
              if (bitOffset == 0 || fieldSize == 0) {
                result = ((result + fieldAlignment - 1) / fieldAlignment) * fieldAlignment;
                bitOffset = 0;
              }
              bitOffset += fieldSize;
            } else {
              if (bitFieldAlignment > fieldAlignment) fieldAlignment = bitFieldAlignment;
              bitFieldAlignment = 0; bitOffset = 0;
              result = ((result + fieldAlignment - 1) / fieldAlignment) * fieldAlignment;
              fieldSize = TypeHelper.SizeOfType(f.Type.ResolvedType) * 8;
            }
            result += fieldSize;
          }
        }
  
        return 0;
      }
  
      /// <summary>
      /// Returns zero or more base class and interface methods that are explicitly overridden by the given method.
      /// </summary>
      /// <remarks>
      /// IMethodReferences are returned (as opposed to IMethodDefinitions) because the references are directly available:
      /// no resolving is needed to find them.
      /// </remarks>
      public static IEnumerable<IMethodReference> GetExplicitlyOverriddenMethods(IMethodDefinition overridingMethod) {
        Contract.Requires(overridingMethod != null);
        Contract.Ensures(Contract.Result<IEnumerable<IMethodReference>>() != null);
        Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<IMethodReference>>(), x => x != null));
  
        foreach (IMethodImplementation methodImplementation in overridingMethod.ContainingTypeDefinition.ExplicitImplementationOverrides) {
          if (overridingMethod.InternedKey == methodImplementation.ImplementingMethod.InternedKey)
            yield return methodImplementation.ImplementedMethod;
        }
      }
  
      /// <summary>
      /// Returns the number of least significant bits in the representation of field.Type that should be ignored when reading or writing the field value at MemberHelper.GetFieldOffset(field).
      /// </summary>
      /// <param name="field">The bit field whose bit offset is to returned.</param>
      public static uint GetFieldBitOffset(IFieldDefinition field)
        //^ requires field.IsBitField;
      {
        Contract.Requires(field != null);
        Contract.Requires(field.IsBitField);
  
        ITypeDefinition typeDefinition = field.ContainingTypeDefinition;
        uint result = 0;
        ushort bitFieldAlignment = 0;
        uint bitOffset = 0;
        IEnumerable<ITypeDefinitionMember> members = typeDefinition.Members;
        if (typeDefinition.Layout == LayoutKind.Sequential) {
          List<IFieldDefinition> fields = new List<IFieldDefinition>(IteratorHelper.GetFilterEnumerable<ITypeDefinitionMember, IFieldDefinition>(members));
          fields.Sort(delegate(IFieldDefinition f1, IFieldDefinition f2) { return f1.SequenceNumber - f2.SequenceNumber; });
          members = IteratorHelper.GetConversionEnumerable<IFieldDefinition, ITypeDefinitionMember>(fields);
        }
        foreach (ITypeDefinitionMember member in members) {
          IFieldDefinition/*?*/ f = member as IFieldDefinition;
          if (f == null || f.IsStatic) continue;
          ushort fieldAlignment = (ushort)(TypeHelper.TypeAlignment(f.Type.ResolvedType)*8);
          if (f == field) {
            if (f.IsBitField) {
              if (bitOffset > 0 && bitOffset+f.BitLength > bitFieldAlignment)
                bitOffset = 0;
              return bitOffset;
            }
            return 0;
          }
          uint fieldSize;
          if (f.IsBitField) {
            bitFieldAlignment = fieldAlignment;
            fieldSize = f.BitLength;
            if (bitOffset > 0 && bitOffset+fieldSize > fieldAlignment)
              bitOffset = 0;
            if (bitOffset == 0 || fieldSize == 0) {
              result = ((result+fieldAlignment-1)/fieldAlignment) * fieldAlignment;
              bitOffset = 0;
            }
            bitOffset += fieldSize;
          } else {
            if (bitFieldAlignment > fieldAlignment) fieldAlignment = bitFieldAlignment;
            bitFieldAlignment = 0; bitOffset = 0;
            result = ((result+fieldAlignment-1)/fieldAlignment) * fieldAlignment;
            fieldSize = TypeHelper.SizeOfType(f.Type.ResolvedType)*8;
          }
          result += fieldSize;
        }
        //^ assume false; //TODO: eventually prove this.
        return 0;
      }
  
      /// <summary>
      /// Get the field offset of a particular field, whose containing type may have its own policy
      /// of assigning offset. For example, a struct and a union in C may be different. 
      /// </summary>
      /// <param name="field">The field whose offset is to returned. The field must not be static.</param>
      public static uint GetFieldOffset(IFieldDefinition field)
        //^ requires !field.IsStatic; 
      {
        Contract.Requires(field != null);
        Contract.Requires(!field.IsStatic);
  
        ITypeDefinition typeDefinition = field.ContainingTypeDefinition;
        if (typeDefinition.Layout == LayoutKind.Explicit)
          return field.Offset;
        return ComputeFieldOffset(field, field.ContainingTypeDefinition); // TODO use typeDefinition
      }
  
      /// <summary>
      /// Returns true iff the two methods are identical (if they are both non-generic) or
      /// if they are equivalent modulo method generic type parameters (if they are both generic).
      /// </summary>
      public static bool MethodsAreEquivalent(IMethodDefinition m1, IMethodDefinition m2) {
        Contract.Requires(m1 != null);
        Contract.Requires(m2 != null);
  
        if (m1.IsGeneric)
          return m1.GenericParameterCount == m2.GenericParameterCount && MemberHelper.GenericMethodSignaturesAreEqual(m1, m2);
        else
          return MemberHelper.SignaturesAreEqual(m1, m2);
      }
  
      /// <summary>
      /// Returns zero or more interface methods that are implemented by the given method. Only methods from interfaces that
      /// are directly implemented by the containing type of the given method are returned. Interfaces declared on base classes
      /// are always fully implemented by the base class, albeit sometimes by an abstract method that is itself implemented by a derived class method.
      /// </summary>
      /// <remarks>
      /// IMethodDefinitions are returned (as opposed to IMethodReferences) because it isn't possible to find the interface methods
      /// without resolving the interface references to their definitions.
      /// </remarks>
      public static IEnumerable<IMethodDefinition> GetImplicitlyImplementedInterfaceMethods(IMethodDefinition implementingMethod) {
        Contract.Requires(implementingMethod != null);
        Contract.Ensures(Contract.Result<IEnumerable<IMethodDefinition>>() != null);
        Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<IMethodDefinition>>(), x => x != null));
  
        if (!implementingMethod.IsVirtual) yield break;
        if (implementingMethod.Visibility != TypeMemberVisibility.Public) yield break;
        if (implementingMethod.ContainingTypeDefinition.IsInterface) yield break;
        List<uint> explicitImplementations = null;
        foreach (IMethodImplementation methodImplementation in implementingMethod.ContainingTypeDefinition.ExplicitImplementationOverrides) {
          if (explicitImplementations == null) explicitImplementations = new List<uint>();
          explicitImplementations.Add(methodImplementation.ImplementedMethod.InternedKey);
        }
        if (explicitImplementations != null) explicitImplementations.Sort();
        foreach (ITypeReference interfaceReference in implementingMethod.ContainingTypeDefinition.Interfaces) {
          foreach (ITypeDefinitionMember interfaceMember in interfaceReference.ResolvedType.GetMembersNamed(implementingMethod.Name, false)) {
            IMethodDefinition/*?*/ interfaceMethod = interfaceMember as IMethodDefinition;
            if (interfaceMethod == null) continue;
            if (MethodsAreEquivalent(implementingMethod, interfaceMethod)) {
              if (explicitImplementations == null || explicitImplementations.BinarySearch(interfaceMethod.InternedKey) < 0)
                yield return interfaceMethod;
            }
          }
        }
      }
  
      /// <summary>
      /// Returns the method from the closest base class that is overridden by the given method.
      /// If no such method exists, Dummy.MethodDefinition is returned.
      /// </summary>
      public static IMethodDefinition GetImplicitlyOverriddenBaseClassMethod(IMethodDefinition derivedClassMethod) {
        Contract.Requires(derivedClassMethod != null);
        Contract.Ensures(Contract.Result<IMethodDefinition>() != null);
  
        if (!derivedClassMethod.IsVirtual || derivedClassMethod.IsNewSlot) return Dummy.MethodDefinition;
        foreach (ITypeReference baseClassReference in derivedClassMethod.ContainingTypeDefinition.BaseClasses) {
          IMethodDefinition overriddenMethod = GetImplicitlyOverriddenBaseClassMethod(derivedClassMethod, baseClassReference.ResolvedType);
          if (!(overriddenMethod is Dummy)) return overriddenMethod;
        }
        return Dummy.MethodDefinition;
      }
  
      private static IMethodDefinition GetImplicitlyOverriddenBaseClassMethod(IMethodDefinition derivedClassMethod, ITypeDefinition baseClass) {
        Contract.Requires(derivedClassMethod != null);
        Contract.Requires(baseClass != null);
        Contract.Ensures(Contract.Result<IMethodDefinition>() != null);
  
        foreach (ITypeDefinitionMember baseMember in baseClass.GetMembersNamed(derivedClassMethod.Name, false)) {
          IMethodDefinition/*?*/ baseMethod = baseMember as IMethodDefinition;
          if (baseMethod == null) continue;
          if (MemberHelper.SignaturesAreEqual(derivedClassMethod, baseMethod)) {
            if (!baseMethod.IsVirtual || baseMethod.IsSealed) return Dummy.MethodDefinition;
            return baseMethod;
          }
          if (derivedClassMethod.GenericParameterCount == baseMethod.GenericParameterCount && derivedClassMethod.IsGeneric) {
            if (MemberHelper.GenericMethodSignaturesAreEqual(derivedClassMethod, baseMethod)) {
              if (!baseMethod.IsVirtual || baseMethod.IsSealed) return Dummy.MethodDefinition;
              return baseMethod;
            }
          }
          if (!derivedClassMethod.IsHiddenBySignature) return Dummy.MethodDefinition;
        }
        foreach (ITypeReference baseClassReference in baseClass.BaseClasses) {
          IMethodDefinition overriddenMethod = GetImplicitlyOverriddenBaseClassMethod(derivedClassMethod, baseClassReference.ResolvedType);
          if (!(overriddenMethod is Dummy)) return overriddenMethod;
        }
        return Dummy.MethodDefinition;
      }
  
      /// <summary>
      /// Returns the method from the derived class that overrides the given method.
      /// If no such method exists, Dummy.MethodDefinition is returned.
      /// </summary>
      public static IMethodDefinition GetImplicitlyOverridingDerivedClassMethod(IMethodDefinition baseClassMethod, ITypeDefinition derivedClass) {
        Contract.Requires(baseClassMethod != null);
        Contract.Requires(derivedClass != null);
        Contract.Ensures(Contract.Result<IMethodDefinition>() != null);
  
  
gt:       if (baseClassMethod.IsSealed) return Dummy.Method; 