private static bool IsSpecPublic(Field f)
        {
            // F: 
            Contract.Requires(f != null);

            return f.Attributes.HasAttribute(ContractNodes.SpecPublicAttributeName);
        }

        /// <summary>
        /// Find shadow field in given type corresponding to field.
        /// </summary>
        public static Field FindShadow(this TypeNode parent, Field field)
        {
            if (field == null || field.Name == null)
            {
                return null;
            }

            MemberList members = parent.GetMembersNamed(field.Name);

            for (int i = 0, n = members == null ? 0 : members.Count; i < n; i++)
            {
                Field f = members[i] as Field;
                if (f != null) return f;
            }

            return null;
        }

    private Field GetReturnValueClosureField(TypeNode declaringType, TypeNode resultType, FieldFlags flags, int uniqueKey)
    {
      Contract.Requires(declaringType != null);
      
      Contract.Assume(declaringType.Template == null);
      Identifier name = Identifier.For("_result" + uniqueKey.ToString()); // unique name for this field

      Field f = declaringType.GetField(name);
      if (f != null) return f;

      f = new Field(declaringType,
        null,
        flags,
        name,
        resultType,
        null);

      declaringType.Members.Add(f);
      // remember we added it so we can make it part of initializations
      if (f.IsStatic)
      {
        topLevelStaticResultField = f;
      }
      else
      {
        topLevelClosureResultField = f;
      }
      return f;
    }

 public static List<int> FieldElementsPeerPositions(Field f)
 {
     List<int> res = new List<int>();
     if (f == null) return res;
     AttributeList al = f.GetAllAttributes(SystemTypes.ElementsPeerAttribute);
     if (al == null) return res;
     foreach (AttributeNode attr in al)
     {
         ExpressionList exprs = attr.Expressions;
         int value = -10;
         if (exprs == null || exprs.Count == 0) 
             value = -1; // default value for attribute w/o param
         else
         {
             Expression arg = exprs[0];
             Literal lit = arg as Literal;
             if (lit != null && lit.Value is int)
                 value = (int)lit.Value;
         }
         if (value == -1)  // all positions are ElementsPeer
         {
             return ElementsPositions(f.Type);
         }
         else // a specific type argument is ElementsPeer
         {
             res.Add(value);
         }
     }
     return res;
 }

        public override void VisitField(Field field)
        {
            base.VisitField(field);

            var type = HelperMethods.Unspecialize(field.Type);

            if (type == contractClass)
            {
                if (field.Type.TemplateArguments != null)
                {
                    var inst = this.OriginalType.GetTemplateInstance(field.Type, field.Type.TemplateArguments);
                    field.Type = inst;
                }
                else
                {
                    field.Type = this.OriginalType;
                }
            }
        }

        private static string GetFieldQualifiers(Field field)
        {
            string qualifiers = string.Empty;

            if (field.IsStatic)
                qualifiers += "static ";

            return qualifiers;
        }

        public override void VisitField(Field field)
        {
            if (field == null) return;

            this.CheckField(field);
        }

 private void PrepareGuardedClass(TypeNode typeNode) {
   SpecSharpCompilerOptions options = this.currentOptions as SpecSharpCompilerOptions;
   if (!(options != null && (options.DisableGuardedClassesChecks || options.Compatibility))) {
     if (typeNode is Class && typeNode.Contract != null && (typeNode.Contract.InvariantCount > 0 || typeNode.Contract.ModelfieldContractCount > 0) ||
       typeNode is Class && this.currentPreprocessorDefinedSymbols != null && this.currentPreprocessorDefinedSymbols.ContainsKey("GuardAllClasses")) {
       if (typeNode.Interfaces == null) {
         typeNode.Interfaces = new InterfaceList();
       }
       if (typeNode.Template == null) { //we have to be careful when we are passed a typeNode of a specialized generic type as it shares the contract of the 'real' generic typeNode
         #region Add the field "frame" to the class.
         Field frameField = new Field(typeNode, null, FieldFlags.Public, Identifier.For("SpecSharp::frameGuard"), SystemTypes.Guard, null);
         frameField.CciKind = CciMemberKind.Auxiliary;
         typeNode.Contract.FrameField = frameField;
         typeNode.Members.Add(frameField);
         This thisParameter = new This(typeNode);
         Method frameGetter = new Method(typeNode, NoDefaultExpose(), Identifier.For("get_SpecSharp::FrameGuard"), null, OptionalModifier.For(SystemTypes.NonNullType, SystemTypes.Guard),
           new Block(new StatementList(new Return(new BinaryExpression(new MemberBinding(thisParameter, frameField), new Literal(SystemTypes.NonNullType, SystemTypes.Type), System.Compiler.NodeType.ExplicitCoercion, OptionalModifier.For(SystemTypes.NonNullType, SystemTypes.Guard))))));
         // Pretend this method is [Delayed] so that we can call it from a delayed constructor.
         frameGetter.Attributes.Add(new AttributeNode(new Literal(ExtendedRuntimeTypes.DelayedAttribute, SystemTypes.Type), null, AttributeTargets.Method));
         frameGetter.CciKind = CciMemberKind.FrameGuardGetter;
         frameGetter.Attributes.Add(new AttributeNode(new Literal(SystemTypes.PureAttribute, SystemTypes.Type), null, AttributeTargets.Method));
         frameGetter.Flags = MethodFlags.Public | MethodFlags.HideBySig | MethodFlags.SpecialName;
         frameGetter.CallingConvention = CallingConventionFlags.HasThis;
         frameGetter.ThisParameter = thisParameter;
         typeNode.Contract.FramePropertyGetter = frameGetter;
         typeNode.Members.Add(frameGetter);
         Property frameProperty = new Property(typeNode, null, PropertyFlags.None, Identifier.For("SpecSharp::FrameGuard"), frameGetter, null);
         typeNode.Members.Add(frameProperty);
         typeNode.Contract.FrameProperty = frameProperty;
         #endregion
         typeNode.Contract.InitFrameSetsMethod = new Method(typeNode, NoDefaultExpose(), Identifier.For("SpecSharp::InitGuardSets"), null, SystemTypes.Void, null);
         typeNode.Contract.InitFrameSetsMethod.CciKind = CciMemberKind.Auxiliary;
         typeNode.Contract.InitFrameSetsMethod.Flags = MethodFlags.Public | MethodFlags.HideBySig | MethodFlags.SpecialName;
       }
     }
   }
 }

 internal static void TryAddDebuggerBrowsableNeverAttribute(Field field)
 {
     Contract.Requires(field != null);
     TryAddDebuggerBrowsableNeverAttribute(field, System.AttributeTargets.Field);
 }

        private static bool FieldAssociatedWithParameter(Field field, Method originalMethod, out Parameter p)
        {
            string fname = field.Name.Name;

            if (fname.EndsWith("__this"))
            {
                // check that it is not a nested one
                if (fname.Length > 8 && !fname.Substring(2, fname.Length - 8).Contains("__"))
                {
                    p = originalMethod.ThisParameter;
                    return true;
                }
            }

            foreach (Parameter par in originalMethod.Parameters)
            {
                string pname = par.Name.Name;
                if (fname == pname)
                {
                    p = par;
                    return true;
                }
            }

            p = null;
            return false;
        }

        public static bool IsClosureField(TypeNode container, Field field)
        {
            Contract.Requires(container != null);
            Contract.Requires(field != null);

            var type = Unspecialize(field.DeclaringType);

            if (IsClosureType(container, type)) return true;
            
            // can be a direct member of a type inside container for caching delegates
            
            if (!field.IsPrivate) return false;
            
            if (!(field.Type.IsDelegateType())) return false;
            
            if (!IsInsideOf(field, container)) return false;
            
            if (!IsCompilerGenerated(field)) return false;
            
            return true;
        }

 bool IsAccessibleFrom(Field field, Method from)
 {
 }

        public override Expression VisitLocal(Local local)
        {
            if (HelperMethods.IsClosureType(this.declaringType, local.Type))
            {
                MemberBinding mb;
                if (!closureLocals.TryGetValue(local, out mb))
                {
                    // Forwarder would be null, if enclosing method with async closure is not generic
                    var localType = forwarder != null ? forwarder.VisitTypeReference(local.Type) : local.Type;

                    var closureField = new Field(this.closureClass, null, FieldFlags.Public, local.Name, localType, null);
                    this.closureClass.Members.Add(closureField);
                    mb = new MemberBinding(this.checkMethod.ThisParameter, closureField);
                    closureLocals.Add(local, mb);

                    // initialize the closure field
                    var instantiatedField = GetMemberInstanceReference(closureField, this.closureClassInstance);
                    this.ClosureInitializer.Statements.Add(new AssignmentStatement(new MemberBinding(this.ClosureLocal, instantiatedField), local));

                }
                return mb;
            }
            return local;
        }

    private static Expression CreateProperResultAccess(ReturnValue returnValue, Expression closureObject, Field resultField)
    {
      Contract.Requires(returnValue != null);
      Contract.Requires(resultField != null);

      var fieldAccess = new MemberBinding(closureObject, resultField);

      if (resultField.Type != returnValue.Type)
      {
        // must cast to generic type expected in this context (box instance unbox.any Generic)
        return new BinaryExpression(new BinaryExpression(fieldAccess, new Literal(resultField.Type), NodeType.Box), new Literal(returnValue.Type), NodeType.UnboxAny);
      }
      else
      {
        return fieldAccess;
      }
    }

    private Method FindAndInstantiateBaseClassInvariantMethod(Class asClass, out Field baseReentrancyFlag)
    {
      baseReentrancyFlag = null;
      if (asClass == null || asClass.BaseClass == null) return null;
      if (!this.Emit(RuntimeContractEmitFlags.InheritContracts)) return null; // don't call base class invariant if we don't inherit

      var baseClass = asClass.BaseClass;

      if (!this.InheritInvariantsAcrossAssemblies && (baseClass.DeclaringModule != asClass.DeclaringModule))
        return null;

      var result = baseClass.GetMethod(Identifier.For("$InvariantMethod$"), null);

      if (result != null && !HelperMethods.IsVisibleFrom(result, asClass)) return null;

      if (result == null && baseClass.Template != null)
      {
        // instantiation of generated method has not happened.
        var generic = baseClass.Template.GetMethod(Identifier.For("$InvariantMethod$"), null);
        if (generic != null)
        {
          if (!HelperMethods.IsVisibleFrom(generic, asClass)) return null;
          // generate proper reference.
          result = GetMethodInstanceReference(generic, baseClass);
        }
      }
      // extract base reentrancy flag
      if (result != null) {
        var instantiatedParent = result.DeclaringType;
        baseReentrancyFlag = instantiatedParent.GetField(Identifier.For("$evaluatingInvariant$"));

        if (baseReentrancyFlag == null && baseClass.Template != null)
        {
          // instantiation of generated baseReentrancy flag has not happened.
          var generic = baseClass.Template.GetField(Identifier.For("$evaluatingInvariant$"));
          if (generic != null)
          {
            if (HelperMethods.IsVisibleFrom(generic, asClass))
            {
              baseReentrancyFlag = GetFieldInstanceReference(generic, baseClass);
            }
          }
        }
      }

      return result;
    }

    public override void VisitTypeNode(TypeNode typeNode) {
      if (typeNode == null) return;

      if (HelperMethods.IsContractTypeForSomeOtherType(typeNode, this.rewriterNodes) != null) {
        return;
      }
      Method savedInvariantMethod = this.InvariantMethod;
      Field savedReentrancyFlag = this.ReentrancyFlag;
      this.InvariantMethod = null;
      this.ReentrancyFlag = null;
      var savedState = this.currentState;
      this.currentState = new CurrentState(typeNode);
      var savedEmitFlags = this.AdaptRuntimeOptionsBasedOnAttributes(typeNode.Attributes);

      try
      {
        if (this.Emit(RuntimeContractEmitFlags.Invariants) && rewriterNodes.InvariantMethod != null)
        {
          InvariantList userWrittenInvariants = typeNode.Contract == null ? null : typeNode.Contract.Invariants;
          Class asClass = typeNode as Class;
          Field baseReentrancyFlag;
          Method baseInvariantMethod = FindAndInstantiateBaseClassInvariantMethod(asClass, out baseReentrancyFlag);


          if ((userWrittenInvariants != null && 0 < userWrittenInvariants.Count) || baseInvariantMethod != null)
          {
            Field reEntrancyFlag = null;
            var isStructWithExplicitLayout = IsStructWithExplicitLayout(typeNode as Struct);
            if (isStructWithExplicitLayout)
            {
              this.HandleError(new Warning(1044, String.Format("Struct '{0}' has explicit layout and an invariant. Invariant recursion guards will not be emitted and evaluation of invariants may occur too eagerly.", typeNode.FullName), new SourceContext()));
            }
            else
            {
              #region Find or create re-entrancy flag to the class
              if (baseReentrancyFlag != null)
              {
                // grab base reEntrancyFlag
                reEntrancyFlag = baseReentrancyFlag;
              }
              else
              {
                FieldFlags reentrancyFlagProtection;
                if (typeNode.IsSealed)
                {
                  reentrancyFlagProtection = FieldFlags.Private | FieldFlags.CompilerControlled;
                }
                else if (this.InheritInvariantsAcrossAssemblies)
                {
                  reentrancyFlagProtection = FieldFlags.Family | FieldFlags.CompilerControlled;
                }
                else
                {
                  reentrancyFlagProtection = FieldFlags.FamANDAssem | FieldFlags.CompilerControlled;
                }
                reEntrancyFlag = new Field(typeNode, null, reentrancyFlagProtection, Identifier.For("$evaluatingInvariant$"), SystemTypes.Boolean, null);
                RewriteHelper.TryAddCompilerGeneratedAttribute(reEntrancyFlag);
                RewriteHelper.TryAddDebuggerBrowsableNeverAttribute(reEntrancyFlag);
                typeNode.Members.Add(reEntrancyFlag);
              }
              #endregion Add re-entrancy flag to the class
            }
            Block newBody = new Block(new StatementList(3));
            // newBody ::=
            //   if (this.$evaluatingInvariant$){
            //     return (true); // don't really return true since this is a void method, but it means the invariant is assumed to hold
            //   this.$evaluatingInvariant$ := true;
            //   try{
            //     <evaluate invariants and call base invariant method>
            //   } finally {
            //     this.$evaluatingInvariant$ := false;
            //   }
            Method invariantMethod =
              new Method(
                typeNode,
                new AttributeList(),
                Identifier.For("$InvariantMethod$"),
                null,
                SystemTypes.Void,
                newBody);
            RewriteHelper.TryAddCompilerGeneratedAttribute(invariantMethod);
            invariantMethod.CallingConvention = CallingConventionFlags.HasThis;
            if (this.InheritInvariantsAcrossAssemblies)
              invariantMethod.Flags = MethodFlags.Family | MethodFlags.Virtual;
            else
              invariantMethod.Flags = MethodFlags.FamANDAssem | MethodFlags.Virtual;
            invariantMethod.Attributes.Add(new AttributeNode(new MemberBinding(null, this.runtimeContracts.ContractNodes.InvariantMethodAttribute.GetConstructor()), null));

            #region call base class invariant
            if (baseInvariantMethod != null)
            {
              newBody.Statements.Add(
                new ExpressionStatement(
                new MethodCall(
                new MemberBinding(invariantMethod.ThisParameter, baseInvariantMethod), null, NodeType.Call, SystemTypes.Void)));
            }
            #endregion
            #region Add re-entrancy test to the method
            Block invariantExit = new Block();
            if (reEntrancyFlag != null)
//.........这里部分代码省略.........

    private Class MakeContractException() {
      Class contractExceptionType;

      #region If we're rewriting an assembly for v4 or above and it *isn't* Silverlight (so serialization support is needed), then use new embedded dll as the type
      if (4 <= TargetPlatform.MajorVersion) {
        var iSafeSerializationData = SystemTypes.SystemAssembly.GetType(Identifier.For("System.Runtime.Serialization"), Identifier.For("ISafeSerializationData")) as Interface;
        if (iSafeSerializationData != null) {
          // Just much easier to write the C# and have the compiler generate everything than to try and create it all manually
          System.Reflection.Assembly embeddedAssembly;
          Stream embeddedAssemblyStream;
          embeddedAssembly = System.Reflection.Assembly.GetExecutingAssembly();
          embeddedAssemblyStream = embeddedAssembly.GetManifestResourceStream("Microsoft.Contracts.Foxtrot.InternalException.dll");
          byte[] data = new byte[0];
          using (var br = new BinaryReader(embeddedAssemblyStream)) {
            var len = embeddedAssemblyStream.Length;
            if (len < Int32.MaxValue)
              data = br.ReadBytes((int)len);
            AssemblyNode assemblyNode = AssemblyNode.GetAssembly(data, TargetPlatform.StaticAssemblyCache, true, false, true);
            contractExceptionType = assemblyNode.GetType(Identifier.For(""), Identifier.For("ContractException")) as Class;
          }
          if (contractExceptionType == null)
            throw new RewriteException("Tried to create the ContractException type from the embedded dll, but failed");
          var d = new Duplicator(this.targetAssembly, this.RuntimeContractType);
          d.FindTypesToBeDuplicated(new TypeNodeList(contractExceptionType));

          var ct = d.Visit(contractExceptionType);
          contractExceptionType = (Class)ct;
          contractExceptionType.Flags |= TypeFlags.NestedPrivate;
          this.RuntimeContractType.Members.Add(contractExceptionType);
          return contractExceptionType;
        }
      }
      #endregion

      contractExceptionType = new Class(this.targetAssembly, this.RuntimeContractType, new AttributeList(), TypeFlags.Class | TypeFlags.NestedPrivate | TypeFlags.Serializable, null, Identifier.For("ContractException"), SystemTypes.Exception, null, null);

      RewriteHelper.TryAddCompilerGeneratedAttribute(contractExceptionType);

      var kindField = new Field(contractExceptionType, null, FieldFlags.Private, Identifier.For("_Kind"), contractNodes.ContractFailureKind, null);
      var userField = new Field(contractExceptionType, null, FieldFlags.Private, Identifier.For("_UserMessage"), SystemTypes.String, null);
      var condField = new Field(contractExceptionType, null, FieldFlags.Private, Identifier.For("_Condition"), SystemTypes.String, null);
      contractExceptionType.Members.Add(kindField);
      contractExceptionType.Members.Add(userField);
      contractExceptionType.Members.Add(condField);

      #region Constructor for setting the fields
      var parameters = new ParameterList();
      var kindParam = new Parameter(Identifier.For("kind"), this.contractNodes.ContractFailureKind);
      var failureParam = new Parameter(Identifier.For("failure"), SystemTypes.String);
      var usermsgParam = new Parameter(Identifier.For("usermsg"), SystemTypes.String);
      var conditionParam = new Parameter(Identifier.For("condition"), SystemTypes.String);
      var innerParam = new Parameter(Identifier.For("inner"), SystemTypes.Exception);
      parameters.Add(kindParam);
      parameters.Add(failureParam);
      parameters.Add(usermsgParam);
      parameters.Add(conditionParam);
      parameters.Add(innerParam);
      var body = new Block(new StatementList());
      var ctor = new InstanceInitializer(contractExceptionType, null, parameters, body);
      ctor.Flags |= MethodFlags.Public | MethodFlags.HideBySig;
      ctor.CallingConvention = CallingConventionFlags.HasThis;
      body.Statements.Add(new ExpressionStatement(new MethodCall(new MemberBinding(ctor.ThisParameter, contractExceptionType.BaseClass.GetConstructor(SystemTypes.String, SystemTypes.Exception)), new ExpressionList(failureParam, innerParam))));
      body.Statements.Add(new AssignmentStatement(new MemberBinding(ctor.ThisParameter, kindField), kindParam));
      body.Statements.Add(new AssignmentStatement(new MemberBinding(ctor.ThisParameter, userField), usermsgParam));
      body.Statements.Add(new AssignmentStatement(new MemberBinding(ctor.ThisParameter, condField), conditionParam));
      body.Statements.Add(new Return());
      contractExceptionType.Members.Add(ctor);
      #endregion

      if (SystemTypes.SerializationInfo != null && SystemTypes.SerializationInfo.BaseClass != null) {
        // Silverlight (e.g.) is a platform that doesn't support serialization. So check to make sure the type really exists.
        // 
        var baseCtor = SystemTypes.Exception.GetConstructor(SystemTypes.SerializationInfo, SystemTypes.StreamingContext);

        if (baseCtor != null) {
          #region Deserialization Constructor
          parameters = new ParameterList();
          var info = new Parameter(Identifier.For("info"), SystemTypes.SerializationInfo);
          var context = new Parameter(Identifier.For("context"), SystemTypes.StreamingContext);
          parameters.Add(info);
          parameters.Add(context);
          body = new Block(new StatementList());
          ctor = new InstanceInitializer(contractExceptionType, null, parameters, body);
          ctor.Flags |= MethodFlags.Private | MethodFlags.HideBySig;
          ctor.CallingConvention = CallingConventionFlags.HasThis;
          // : base(info, context) 
          body.Statements.Add(new ExpressionStatement(new MethodCall(new MemberBinding(ctor.ThisParameter, baseCtor), new ExpressionList(info, context))));
          // _Kind = (ContractFailureKind)info.GetInt32("Kind");
          var getInt32 = SystemTypes.SerializationInfo.GetMethod(Identifier.For("GetInt32"), SystemTypes.String);
          body.Statements.Add(new AssignmentStatement(
              new MemberBinding(new This(), kindField),
              new MethodCall(new MemberBinding(info, getInt32), new ExpressionList(new Literal("Kind", SystemTypes.String)))
              ));
          // _UserMessage = info.GetString("UserMessage");
          var getString = SystemTypes.SerializationInfo.GetMethod(Identifier.For("GetString"), SystemTypes.String);
          body.Statements.Add(new AssignmentStatement(
              new MemberBinding(new This(), userField),
              new MethodCall(new MemberBinding(info, getString), new ExpressionList(new Literal("UserMessage", SystemTypes.String)))
              ));
          // _Condition = info.GetString("Condition");
//.........这里部分代码省略.........

 public static bool FieldIsAdditive(Field field) {
   if (field == null) return false;
   AttributeNode attr = field.GetAttribute(SystemTypes.AdditiveAttribute);
   if (attr == null) return false;
   ExpressionList exprs = attr.Expressions;
   if (exprs == null || exprs.Count != 1) return true;
   Literal lit = exprs[0] as Literal;
   if (lit != null && (lit.Value is bool)) return (bool)lit.Value;
   else return false;
 }

        public override Field VisitField(Field field)
        {
            if (field == null) return null;

            if (!this.IncludeModels && HelperMethods.HasAttribute(field.Attributes, ContractNodes.ModelAttributeName))
                return null;

            return base.VisitField(field);
        }

    private static Field GetInstanceField(TypeNode originalReturnType, Field possiblyGenericField, TypeNode instanceDeclaringType)
    {
      Contract.Requires(instanceDeclaringType != null);

      if (instanceDeclaringType.Template == null) return possiblyGenericField;
      var declaringTemplate = instanceDeclaringType;
      while (declaringTemplate.Template != null) { declaringTemplate = declaringTemplate.Template; }
      Contract.Assume(declaringTemplate == possiblyGenericField.DeclaringType);

      return Rewriter.GetFieldInstanceReference(possiblyGenericField, instanceDeclaringType);
#if false
      Field f = instanceDeclaringType.GetField(possiblyGenericField.Name);
      if (f != null)
      {
        // already instantiated
        return f;
      }
      // pseudo instance
      Field instance = new Field(instanceDeclaringType, possiblyGenericField.Attributes, possiblyGenericField.Flags, possiblyGenericField.Name, originalReturnType, null);
      instanceDeclaringType.Members.Add(instance);
      return instance;
#endif
    }