fixed problems with datatypes

removed stale contracts in stratified inlining
added test to datatypes

10 files changed, 99 insertions, 683 deletions

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index eaef7e40..9efe1e28 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -251,7 +251,7 @@ namespace BytecodeTranslator {
         }

         var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, pdbReader) as IModule;

         // The decompiler does not turn calls to Assert/Assume into Code Model nodes

-        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);

+        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(m2);

         decompiledModules.Add(m2);

         host.RegisterAsLatest(m2);

         contractExtractors.Add(m2, host.GetContractExtractor(m2.UnitIdentity));

diff --git a/BCT/GetMeHere/AssertionInjector/Program.cs b/BCT/GetMeHere/AssertionInjector/Program.cs
index 07b5c46e..4cdcf137 100644
--- a/BCT/GetMeHere/AssertionInjector/Program.cs
+++ b/BCT/GetMeHere/AssertionInjector/Program.cs
@@ -38,10 +38,7 @@ namespace AssertionInjector {
         return errorValue;

       }

 

-      if (args[0].EndsWith(".bpl"))

-        return InjectAssertionInBpl(args[0], args[1], lineNumber, columnNumber);

-      else

-        return InjectAssertionInAssembly(args[0], args[1], lineNumber, columnNumber);

+      return InjectAssertionInBpl(args[0], args[1], lineNumber, columnNumber);

     }

 

     static int InjectAssertionInBpl(string bplFileName, string fileName, int lineNumber, int columnNumber) {

@@ -69,69 +66,6 @@ namespace AssertionInjector {
       }

       return returnValue;

     }

-

-    static int InjectAssertionInAssembly(string assemblyName, string fileName, int lineNumber, int columnNumber) {

-      string originalAssemblyPath;

-      string outputAssemblyPath;

-      string outputPdbFileName;

-

-      var returnValue = errorValue;

-

-      using (var host = new PeReader.DefaultHost()) {

-        IModule/*?*/ module = host.LoadUnitFrom(assemblyName) as IModule;

-        if (module == null || module == Dummy.Module || module == Dummy.Assembly) {

-          Console.WriteLine(assemblyName + " is not a PE file containing a CLR assembly, or an error occurred when loading it.");

-          return errorValue;

-        }

-        module = new MetadataDeepCopier(host).Copy(module);

-

-        var pdbFile = Path.ChangeExtension(module.Location, "pdb");

-        if (!File.Exists(pdbFile)) {

-          Console.WriteLine("Could not load the PDB file for '" + module.Name.Value + "' . Exiting.");

-          return errorValue;

-        }

-        using (var pdbStream = File.OpenRead(pdbFile)) {

-          if (pdbStream == null) {

-            Console.WriteLine("Could not load the PDB file for '" + module.Name.Value + "' . Exiting.");

-            return errorValue;

-          }

-          using (var pdbReader = new PdbReader(pdbStream, host)) {

-            var localScopeProvider = new ILGenerator.LocalScopeProvider(pdbReader);

-            var mutator = new GetMeHereAssemblyInjector(host, pdbReader, fileName, lineNumber, columnNumber);

-            module = mutator.Rewrite(module);

-            //Console.WriteLine("Emitted probe: {0}", mutator.emittedProbe);

-            if (mutator.emittedProbe) returnValue = 0;

-

-            originalAssemblyPath = module.Location;

-            var tempDir = Path.GetTempPath();

-            outputAssemblyPath = Path.Combine(tempDir, Path.GetFileName(originalAssemblyPath));

-            outputPdbFileName = Path.ChangeExtension(outputAssemblyPath, "pdb");

-

-            using (var outputStream = File.Create(outputAssemblyPath)) {

-              using (var pdbWriter = new PdbWriter(outputPdbFileName, pdbReader)) {

-                PeWriter.WritePeToStream(module, host, outputStream, pdbReader, localScopeProvider, pdbWriter);

-              }

-            }

-          }

-        }

-      }

-

-      try {

-        File.Copy(outputAssemblyPath, originalAssemblyPath, true);

-        File.Delete(outputAssemblyPath);

-        var originalPdbPath = Path.ChangeExtension(originalAssemblyPath, "pdb");

-        var outputPdbPath = Path.Combine(Path.GetDirectoryName(outputAssemblyPath), outputPdbFileName);

-        File.Copy(outputPdbPath, originalPdbPath, true);

-        File.Delete(outputPdbPath);

-      }

-      catch (Exception e) {

-        Console.WriteLine("Something went wrong with replacing input assembly/pdb");

-        Console.WriteLine(e.Message);

-        return errorValue;

-      }

-

-      return returnValue; // success

-    }

   }

 

   public class GetMeHereBplInjector : Bpl.StandardVisitor {

@@ -174,515 +108,4 @@ namespace AssertionInjector {
     }

   }

 

-  /// <summary>

-  /// A mutator that modifies method bodies at the IL level.

-  /// It injects a call to GetMeHere.GetMeHere.Assert at the

-  /// specified source location.

-  /// The class GetMeHere is synthesized and injected into the

-  /// rewritten assembly.

-  /// </summary>

-  public class GetMeHereAssemblyInjector : MetadataRewriter {

-    PdbReader pdbReader;

-    string fileName;

-    int lineNumber;

-    int columnNumber;

-

-    public GetMeHereAssemblyInjector(IMetadataHost host, PdbReader pdbReader, string fileName, int lineNumber, int columnNumber)

-      : base(host) {

-      this.pdbReader = pdbReader;

-      this.fileName = fileName;

-      this.lineNumber = lineNumber;

-      this.columnNumber = columnNumber;

-    }

-

-    List<ILocalDefinition> currentLocals;

-    ILGenerator currentGenerator;

-    IEnumerator<ILocalScope>/*?*/ scopeEnumerator;

-    bool scopeEnumeratorIsValid;

-    Stack<ILocalScope> scopeStack = new Stack<ILocalScope>();

-    private NamespaceTypeDefinition getMeHereClass;

-    private MethodDefinition getMeHereAssert;

-    public bool emittedProbe;

-

-    public override void RewriteChildren(Module module) {

-      base.RewriteChildren(module);

-      module.AllTypes.Add(this.getMeHereClass);

-    }

-

-    public override void RewriteChildren(RootUnitNamespace rootUnitNamespace) {

-      var ns = this.CreateGetMeHere(rootUnitNamespace); // side effect: sets fields

-      rootUnitNamespace.Members.Add(ns);

-      base.RewriteChildren(rootUnitNamespace);

-    }

-

-    public override IMethodBody Rewrite(IMethodBody methodBody) {

-      try {

-        this.currentGenerator = null;

-        base.Rewrite(methodBody);

-        if (this.currentGenerator == null) {

-          //Console.WriteLine("Not rewriting '{0}'", MemberHelper.GetMethodSignature(methodBody.MethodDefinition, NameFormattingOptions.None));

-          return methodBody;

-        }

-        var newBody = new ILGeneratorMethodBody(this.currentGenerator, methodBody.LocalsAreZeroed, (ushort)(methodBody.MaxStack + 1),

-          methodBody.MethodDefinition, this.currentLocals ?? new List<ILocalDefinition>(), Enumerable<ITypeDefinition>.Empty);

-        return newBody;

-      } finally {

-        this.currentGenerator = null;

-        this.currentLocals = null;

-      }

-    }

-

-    public override void RewriteChildren(MethodBody methodBody) {

-      this.currentLocals = methodBody.LocalVariables;

-      //Console.WriteLine("{0}", MemberHelper.GetMethodSignature(methodBody.MethodDefinition));

-      try {

-        var operations = methodBody.Operations;

-        if (operations == null || operations.Count == 0) return;

-

-        IPrimarySourceLocation startLocation = null;

-        IPrimarySourceLocation endLocation = null;

-        var ys = this.pdbReader.GetClosestPrimarySourceLocationsFor(operations[0].Location);

-        foreach (var y in ys) {

-          //Console.WriteLine("{0}:{1}({2},{3})", y.Document.Name.Value, MemberHelper.GetMethodSignature(methodBody.MethodDefinition, NameFormattingOptions.None),

-          //  y.StartLine, y.StartColumn);

-          startLocation = y;

-          break;

-        }

-

-        if (startLocation == null || startLocation.StartLine == 0x00feefee || !startLocation.Document.Name.Value.Equals(this.fileName)) return;

-

-        var lastIndex = operations.Count;

-        do {

-          lastIndex--;

-          ys = this.pdbReader.GetClosestPrimarySourceLocationsFor(operations[lastIndex].Location);

-          foreach (var y in ys) {

-            //Console.WriteLine("{0}:{1}({2},{3})", y.Document.Name.Value, MemberHelper.GetMethodSignature(methodBody.MethodDefinition, NameFormattingOptions.None),

-            //  y.StartLine, y.StartColumn);

-            endLocation = y;

-            break;

-          }

-        } while (0 <= lastIndex && (endLocation == null || endLocation.StartLine == 0x00feefee));

-        if (lastIndex == -1 || !(startLocation.StartLine <= this.lineNumber && this.lineNumber <= endLocation.StartLine)) return;

-

-

-        ProcessOperations(methodBody, operations);

-      } catch (GetMeHereInjectorException) {

-        Console.WriteLine("Internal error during IL mutation for the method '{0}'.",

-          MemberHelper.GetMemberSignature(methodBody.MethodDefinition, NameFormattingOptions.SmartTypeName));

-      }

-

-    }

-

-    private void ProcessOperations(MethodBody methodBody, List<IOperation> operations) {

-

-      var count = operations.Count;

-      ILGenerator generator = new ILGenerator(this.host, methodBody.MethodDefinition);

-      if (this.pdbReader != null) {

-        foreach (var ns in this.pdbReader.GetNamespaceScopes(methodBody)) {

-          foreach (var uns in ns.UsedNamespaces)

-            generator.UseNamespace(uns.NamespaceName.Value);

-        }

-      }

-

-      this.currentGenerator = generator;

-      this.scopeEnumerator = this.pdbReader == null ? null : this.pdbReader.GetLocalScopes(methodBody).GetEnumerator();

-      this.scopeEnumeratorIsValid = this.scopeEnumerator != null && this.scopeEnumerator.MoveNext();

-

-      var methodName = MemberHelper.GetMemberSignature(methodBody.MethodDefinition, NameFormattingOptions.SmartTypeName);

-

-      #region Record all offsets that appear as part of an exception handler

-      Dictionary<uint, bool> offsetsUsedInExceptionInformation = new Dictionary<uint, bool>();

-      foreach (var exceptionInfo in methodBody.OperationExceptionInformation ?? Enumerable<IOperationExceptionInformation>.Empty) {

-        uint x = exceptionInfo.TryStartOffset;

-        if (!offsetsUsedInExceptionInformation.ContainsKey(x)) offsetsUsedInExceptionInformation.Add(x, true);

-        x = exceptionInfo.TryEndOffset;

-        if (!offsetsUsedInExceptionInformation.ContainsKey(x)) offsetsUsedInExceptionInformation.Add(x, true);

-        x = exceptionInfo.HandlerStartOffset;

-        if (!offsetsUsedInExceptionInformation.ContainsKey(x)) offsetsUsedInExceptionInformation.Add(x, true);

-        x = exceptionInfo.HandlerEndOffset;

-        if (!offsetsUsedInExceptionInformation.ContainsKey(x)) offsetsUsedInExceptionInformation.Add(x, true);

-        if (exceptionInfo.HandlerKind == HandlerKind.Filter) {

-          x = exceptionInfo.FilterDecisionStartOffset;

-          if (!offsetsUsedInExceptionInformation.ContainsKey(x)) offsetsUsedInExceptionInformation.Add(x, true);

-        }

-      }

-      #endregion Record all offsets that appear as part of an exception handler

-

-      Dictionary<uint, ILGeneratorLabel> offset2Label = new Dictionary<uint, ILGeneratorLabel>();

-      #region Pass 1: Make a label for each branch target

-      for (int i = 0; i < count; i++) {

-        IOperation op = operations[i];

-        switch (op.OperationCode) {

-          case OperationCode.Beq:

-          case OperationCode.Bge:

-          case OperationCode.Bge_Un:

-          case OperationCode.Bgt:

-          case OperationCode.Bgt_Un:

-          case OperationCode.Ble:

-          case OperationCode.Ble_Un:

-          case OperationCode.Blt:

-          case OperationCode.Blt_Un:

-          case OperationCode.Bne_Un:

-          case OperationCode.Br:

-          case OperationCode.Brfalse:

-          case OperationCode.Brtrue:

-          case OperationCode.Leave:

-          case OperationCode.Beq_S:

-          case OperationCode.Bge_S:

-          case OperationCode.Bge_Un_S:

-          case OperationCode.Bgt_S:

-          case OperationCode.Bgt_Un_S:

-          case OperationCode.Ble_S:

-          case OperationCode.Ble_Un_S:

-          case OperationCode.Blt_S:

-          case OperationCode.Blt_Un_S:

-          case OperationCode.Bne_Un_S:

-          case OperationCode.Br_S:

-          case OperationCode.Brfalse_S:

-          case OperationCode.Brtrue_S:

-          case OperationCode.Leave_S:

-            uint x = (uint)op.Value;

-            if (!offset2Label.ContainsKey(x))

-              offset2Label.Add(x, new ILGeneratorLabel());

-            break;

-          case OperationCode.Switch:

-            uint[] offsets = op.Value as uint[];

-            foreach (var offset in offsets) {

-              if (!offset2Label.ContainsKey(offset))

-                offset2Label.Add(offset, new ILGeneratorLabel());

-            }

-            break;

-          default:

-            break;

-        }

-      }

-      #endregion Pass 1: Make a label for each branch target

-

-      #region Pass 2: Emit each operation, along with labels

-      this.emittedProbe = false; // don't do it more than once

-      for (int i = 0; i < count; i++) {

-        IOperation op = operations[i];

-        ILGeneratorLabel label;

-        this.EmitDebugInformationFor(op);

-        #region Mark operation if it is a label for a branch

-        if (offset2Label.TryGetValue(op.Offset, out label)) {

-          generator.MarkLabel(label);

-        }

-        #endregion Mark operation if it is a label for a branch

-

-        #region Mark operation if it is pointed to by an exception handler

-        bool ignore;

-        uint offset = op.Offset;

-        if (offsetsUsedInExceptionInformation.TryGetValue(offset, out ignore)) {

-          foreach (var exceptionInfo in methodBody.OperationExceptionInformation) {

-            if (offset == exceptionInfo.TryStartOffset)

-              generator.BeginTryBody();

-

-            // Never need to do anthing when offset == exceptionInfo.TryEndOffset because

-            // we pick up an EndTryBody from the HandlerEndOffset below

-            //  generator.EndTryBody();

-

-            if (offset == exceptionInfo.HandlerStartOffset) {

-              switch (exceptionInfo.HandlerKind) {

-                case HandlerKind.Catch:

-                  generator.BeginCatchBlock(exceptionInfo.ExceptionType);

-                  break;

-                case HandlerKind.Fault:

-                  generator.BeginFaultBlock();

-                  break;

-                case HandlerKind.Filter:

-                  generator.BeginFilterBody();

-                  break;

-                case HandlerKind.Finally:

-                  generator.BeginFinallyBlock();

-                  break;

-              }

-            }

-            if (exceptionInfo.HandlerKind == HandlerKind.Filter && offset == exceptionInfo.FilterDecisionStartOffset) {

-              generator.BeginFilterBlock();

-            }

-            if (offset == exceptionInfo.HandlerEndOffset)

-              generator.EndTryBody();

-          }

-        }

-        #endregion Mark operation if it is pointed to by an exception handler

-

-        #region Emit operation along with any injection

-

-        if (!this.emittedProbe) {

-          IPrimarySourceLocation location = null;

-          var locations = this.pdbReader.GetPrimarySourceLocationsFor(op.Location);

-          foreach (var x in locations) {

-            if (x.StartLine != 0x00feefee && this.lineNumber <= x.StartLine) {

-              location = x;

-              break;

-            }

-          }

-          if (location != null) {

-            this.emittedProbe = true;

-            generator.Emit(OperationCode.Ldc_I4_0);

-            generator.Emit(OperationCode.Call, this.getMeHereAssert);

-          }

-        }

-

-        switch (op.OperationCode) {

-          #region Branches

-          case OperationCode.Beq:

-          case OperationCode.Bge:

-          case OperationCode.Bge_Un:

-          case OperationCode.Bgt:

-          case OperationCode.Bgt_Un:

-          case OperationCode.Ble:

-          case OperationCode.Ble_Un:

-          case OperationCode.Blt:

-          case OperationCode.Blt_Un:

-          case OperationCode.Bne_Un:

-          case OperationCode.Br:

-          case OperationCode.Brfalse:

-          case OperationCode.Brtrue:

-          case OperationCode.Leave:

-          case OperationCode.Beq_S:

-          case OperationCode.Bge_S:

-          case OperationCode.Bge_Un_S:

-          case OperationCode.Bgt_S:

-          case OperationCode.Bgt_Un_S:

-          case OperationCode.Ble_S:

-          case OperationCode.Ble_Un_S:

-          case OperationCode.Blt_S:

-          case OperationCode.Blt_Un_S:

-          case OperationCode.Bne_Un_S:

-          case OperationCode.Br_S:

-          case OperationCode.Brfalse_S:

-          case OperationCode.Brtrue_S:

-          case OperationCode.Leave_S:

-            generator.Emit(ILGenerator.LongVersionOf(op.OperationCode), offset2Label[(uint)op.Value]);

-            break;

-          case OperationCode.Switch:

-            uint[] offsets = op.Value as uint[];

-            ILGeneratorLabel[] labels = new ILGeneratorLabel[offsets.Length];

-            for (int j = 0, n = offsets.Length; j < n; j++) {

-              labels[j] = offset2Label[offsets[j]];

-            }

-            generator.Emit(OperationCode.Switch, labels);

-            break;

-          #endregion Branches

-          #region Everything else

-          //case OperationCode.Stloc:

-          //case OperationCode.Stloc_0:

-          //case OperationCode.Stloc_1:

-          //case OperationCode.Stloc_2:

-          //case OperationCode.Stloc_3:

-          //case OperationCode.Stloc_S:

-          //  EmitStoreLocal(generator, op);

-          //  break;

-          default:

-            if (op.Value == null) {

-              generator.Emit(op.OperationCode);

-              break;

-            }

-            var typeCode = System.Convert.GetTypeCode(op.Value);

-            switch (typeCode) {

-              case TypeCode.Byte:

-                generator.Emit(op.OperationCode, (byte)op.Value);

-                break;

-              case TypeCode.Double:

-                generator.Emit(op.OperationCode, (double)op.Value);

-                break;

-              case TypeCode.Int16:

-                generator.Emit(op.OperationCode, (short)op.Value);

-                break;

-              case TypeCode.Int32:

-                generator.Emit(op.OperationCode, (int)op.Value);

-                break;

-              case TypeCode.Int64:

-                generator.Emit(op.OperationCode, (long)op.Value);

-                break;

-              case TypeCode.Object:

-                IFieldReference fieldReference = op.Value as IFieldReference;

-                if (fieldReference != null) {

-                  generator.Emit(op.OperationCode, this.Rewrite(fieldReference));

-                  break;

-                }

-                ILocalDefinition localDefinition = op.Value as ILocalDefinition;

-                if (localDefinition != null) {

-                  generator.Emit(op.OperationCode, localDefinition);

-                  break;

-                }

-                IMethodReference methodReference = op.Value as IMethodReference;

-                if (methodReference != null) {

-                  generator.Emit(op.OperationCode, this.Rewrite(methodReference));

-                  break;

-                }

-                IParameterDefinition parameterDefinition = op.Value as IParameterDefinition;

-                if (parameterDefinition != null) {

-                  generator.Emit(op.OperationCode, parameterDefinition);

-                  break;

-                }

-                ISignature signature = op.Value as ISignature;

-                if (signature != null) {

-                  generator.Emit(op.OperationCode, signature);

-                  break;

-                }

-                ITypeReference typeReference = op.Value as ITypeReference;

-                if (typeReference != null) {

-                  generator.Emit(op.OperationCode, this.Rewrite(typeReference));

-                  break;

-                }

-                throw new GetMeHereInjectorException("Should never get here: no other IOperation argument types should exist");

-              case TypeCode.SByte:

-                generator.Emit(op.OperationCode, (sbyte)op.Value);

-                break;

-              case TypeCode.Single:

-                generator.Emit(op.OperationCode, (float)op.Value);

-                break;

-              case TypeCode.String:

-                generator.Emit(op.OperationCode, (string)op.Value);

-                break;

-              default:

-                // The other cases are the other enum values that TypeCode has.

-                // But no other argument types should be in the Operations. ILGenerator cannot handle anything else,

-                // so such IOperations should never exist.

-                //case TypeCode.Boolean:

-                //case TypeCode.Char:

-                //case TypeCode.DateTime:

-                //case TypeCode.DBNull:

-                //case TypeCode.Decimal:

-                //case TypeCode.Empty: // this would be the value for null, but the case when op.Value is null is handled before the switch statement

-                //case TypeCode.UInt16:

-                //case TypeCode.UInt32:

-                //case TypeCode.UInt64:

-                throw new GetMeHereInjectorException("Should never get here: no other IOperation argument types should exist");

-            }

-            break;

-          #endregion Everything else

-        }

-        #endregion Emit operation along with any injection

-

-      }

-      while (generator.InTryBody)

-        generator.EndTryBody();

-      while (this.scopeStack.Count > 0) {

-        this.currentGenerator.EndScope();

-        this.scopeStack.Pop();

-      }

-      #endregion Pass 2: Emit each operation, along with labels

-

-    }

-

-    private void EmitDebugInformationFor(IOperation operation) {

-      this.currentGenerator.MarkSequencePoint(operation.Location);

-      if (this.scopeEnumerator == null) return;

-      ILocalScope/*?*/ currentScope = null;

-      while (this.scopeStack.Count > 0) {

-        currentScope = this.scopeStack.Peek();

-        if (operation.Offset < currentScope.Offset + currentScope.Length) break;

-        this.scopeStack.Pop();

-        this.currentGenerator.EndScope();

-        currentScope = null;

-      }

-      while (this.scopeEnumeratorIsValid) {

-        currentScope = this.scopeEnumerator.Current;

-        if (currentScope.Offset <= operation.Offset && operation.Offset < currentScope.Offset + currentScope.Length) {

-          this.scopeStack.Push(currentScope);

-          this.currentGenerator.BeginScope();

-          foreach (var local in this.pdbReader.GetVariablesInScope(currentScope))

-            this.currentGenerator.AddVariableToCurrentScope(local);

-          foreach (var constant in this.pdbReader.GetConstantsInScope(currentScope))

-            this.currentGenerator.AddConstantToCurrentScope(constant);

-          this.scopeEnumeratorIsValid = this.scopeEnumerator.MoveNext();

-        } else

-          break;

-      }

-    }

-

-    private NestedUnitNamespace CreateGetMeHere(IUnitNamespace unitNamespace) {

-

-      var voidType = this.host.PlatformType.SystemVoid;

-

-      #region Create class

-

-      Microsoft.Cci.MethodReference compilerGeneratedCtor =

-        new Microsoft.Cci.MethodReference(

-          this.host,

-          this.host.PlatformType.SystemRuntimeCompilerServicesCompilerGeneratedAttribute,

-          CallingConvention.HasThis,

-          voidType,

-          this.host.NameTable.Ctor,

-          0);

-      CustomAttribute compilerGeneratedAttribute = new CustomAttribute();

-      compilerGeneratedAttribute.Constructor = compilerGeneratedCtor;

-

-      var getMeHereNamespace = new NestedUnitNamespace() {

-        ContainingUnitNamespace = unitNamespace,

-        Name = this.host.NameTable.GetNameFor("GetMeHere"),

-      };

-      this.getMeHereClass = new NamespaceTypeDefinition() {

-        // NB: The string name must be kept in sync with the code that recognizes GMH methods!!

-        Attributes = new List<ICustomAttribute>(){compilerGeneratedAttribute},

-        BaseClasses = new List<ITypeReference>(){this.host.PlatformType.SystemObject},

-        ContainingUnitNamespace = getMeHereNamespace,

-        InternFactory = this.host.InternFactory,

-        IsBeforeFieldInit = true,

-        IsClass = true,

-        IsSealed = true,

-        Layout = LayoutKind.Auto,

-        Name = this.host.NameTable.GetNameFor("GetMeHere"),

-        StringFormat = StringFormatKind.Ansi,

-      };

-      #endregion

-

-      #region Create methods

-      var body = new MethodBody() {

-        Operations = new List<IOperation>(){new Operation() { OperationCode = OperationCode.Ret, }},

-      };

-

-      this.getMeHereAssert = new MethodDefinition() {

-        Body = body,

-        CallingConvention = CallingConvention.Default, // Isn't it the default for the calling convention to be the default?

-        ContainingTypeDefinition = getMeHereClass,

-        IsStatic = true,

-        InternFactory = this.host.InternFactory,

-        Name = this.host.NameTable.GetNameFor("Assert"),

-        Type = voidType,

-        Visibility = TypeMemberVisibility.Public,

-      };

-      var paramList = new List<IParameterDefinition>();

-      paramList.Add(

-        new ParameterDefinition() {

-          ContainingSignature = getMeHereAssert,

-          Name = this.host.NameTable.GetNameFor("condition"),

-          Type = this.host.PlatformType.SystemBoolean,

-          Index = 0,

-        });

-      getMeHereAssert.Parameters = paramList;

-      body.MethodDefinition = getMeHereAssert;

-      getMeHereClass.Methods = new List<IMethodDefinition> { getMeHereAssert };

-      #endregion

-

-      return getMeHereNamespace;

-    }

-

-    /// <summary>

-    /// Exceptions thrown during extraction. Should not escape this class.

-    /// </summary>

-    private class GetMeHereInjectorException : Exception {

-      /// <summary>

-      /// Exception specific to an error occurring in the contract extractor

-      /// </summary>

-      public GetMeHereInjectorException() { }

-      /// <summary>

-      /// Exception specific to an error occurring in the contract extractor

-      /// </summary>

-      public GetMeHereInjectorException(string s) : base(s) { }

-      /// <summary>

-      /// Exception specific to an error occurring in the contract extractor

-      /// </summary>

-      public GetMeHereInjectorException(string s, Exception inner) : base(s, inner) { }

-      /// <summary>

-      /// Exception specific to an error occurring in the contract extractor

-      /// </summary>

-      public GetMeHereInjectorException(SerializationInfo info, StreamingContext context) : base(info, context) { }

-    }

-  }

-

 }

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index fc28100e..500cb0ca 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -214,39 +214,27 @@ namespace Microsoft.Boogie {
     }

 

     void CreateDatatypeSelectorsAndTesters() {

-      HashSet<string> functions = new HashSet<string>();

-      List<Function> constructors = new List<Function>();

+      Dictionary<string, Function> constructors = new Dictionary<string, Function>();

+      List<Declaration> prunedTopLevelDeclarations = new List<Declaration>();

       foreach (Declaration decl in TopLevelDeclarations) {

         Function func = decl as Function;

-        if (func == null) continue;

-        functions.Add(func.Name);

-        if (QKeyValue.FindBoolAttribute(func.Attributes, "constructor"))

-          constructors.Add(func);

-      }

-

-      foreach (Function f in constructors) {

-        foreach (Variable v in f.InParams) {

-          Formal inVar = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

-          Formal outVar = new Formal(Token.NoToken, v.TypedIdent, false);

-          Function selector = new Function(f.tok, v.Name + "#" + f.Name, new VariableSeq(inVar), outVar);

-          selector.AddAttribute("selector");

-          for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

-            if (kv.Key == "constructor") continue;

-            selector.AddAttribute(kv.Key, kv.Params.ToArray());

-          }

-          if (!functions.Contains(selector.Name))

-            TopLevelDeclarations.Add(selector);

+        if (func == null || !QKeyValue.FindBoolAttribute(decl.Attributes, "constructor")) {

+          prunedTopLevelDeclarations.Add(decl);

+          continue;

         }

-        Formal inv = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

-        Formal outv = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false);

-        Function isConstructor = new Function(f.tok, "is#" + f.Name, new VariableSeq(inv), outv);

-        for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

-          if (kv.Key == "constructor") continue;

-          isConstructor.AddAttribute(kv.Key, kv.Params.ToArray());

+        if (constructors.ContainsKey(func.Name)) continue;

+        constructors.Add(func.Name, func);

+        prunedTopLevelDeclarations.Add(func);

+      }

+      TopLevelDeclarations = prunedTopLevelDeclarations;

+

+      foreach (Function f in constructors.Values) {

+        for (int i = 0; i < f.InParams.Length; i++) {

+          DatatypeSelector selector = new DatatypeSelector(f, i);

+          TopLevelDeclarations.Add(selector);

         }

-        isConstructor.AddAttribute("membership");

-        if (!functions.Contains(isConstructor.Name))

-          TopLevelDeclarations.Add(isConstructor);

+        DatatypeMembership membership = new DatatypeMembership(f);

+        TopLevelDeclarations.Add(membership);

       }

     }

 

@@ -1803,7 +1791,34 @@ namespace Microsoft.Boogie {
     }

   }

 

-  

+  public class DatatypeSelector : Function {

+    public Function constructor;

+    public int index;

+    public DatatypeSelector(Function constructor, int index)

+      : base(constructor.tok, 

+             constructor.InParams[index].Name + "#" + constructor.Name,

+             new VariableSeq(new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true)),

+             new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.InParams[index].TypedIdent.Type), false)) 

+    {

+      this.constructor = constructor;

+      this.index = index;

+    }

+    public override void Emit(TokenTextWriter stream, int level) { }

+  }

+

+  public class DatatypeMembership : Function {

+    public Function constructor;

+    public DatatypeMembership(Function constructor)

+      : base(constructor.tok, 

+             "is#" + constructor.Name,

+             new VariableSeq(new Formal(constructor.tok, new TypedIdent(constructor.tok, "", constructor.OutParams[0].TypedIdent.Type), true)),

+             new Formal(constructor.tok, new TypedIdent(constructor.tok, "", Type.Bool), false)) 

+    {

+      this.constructor = constructor;

+    }

+    public override void Emit(TokenTextWriter stream, int level) {

+    }

+  }

 

   public class Function : DeclWithFormals {

     public string Comment;

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index d3448b5d..dab0807f 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -206,13 +206,15 @@ namespace Microsoft.Boogie.SMTLib
           foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) {

             datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";

             foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {

+              string quotedConstructorName = Namer.GetQuotedName(f, f.Name);

               if (f.InParams.Length == 0) {

-                datatypeString += Namer.GetQuotedName(f, f.Name) + " ";

+                datatypeString += quotedConstructorName + " ";

               }

               else {

-                datatypeString += "(" + Namer.GetQuotedName(f, f.Name) + " ";

+                datatypeString += "(" + quotedConstructorName + " ";

                 foreach (Variable v in f.InParams) {

-                  datatypeString += "(" + v.Name + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";

+                  string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);

+                  datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";

                 }

                 datatypeString += ") ";

               }

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 8d4a4256..635280d1 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -660,11 +660,14 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       private string ExtractDatatype(Function func) {

-        if (QKeyValue.FindBoolAttribute(func.Attributes, "selector")) {

-          return func.Name.Remove(func.Name.IndexOf('#'));

-        }

-        else if (QKeyValue.FindBoolAttribute(func.Attributes, "membership")) {

-          return func.Name.Replace('#', '-');

+        if (func is DatatypeSelector) {

+          DatatypeSelector selector = (DatatypeSelector) func;

+          Variable v = selector.constructor.InParams[selector.index];

+          return ExprLineariser.Namer.GetQuotedName(v, v.Name + "#" + selector.constructor.Name);

+        }

+        else if (func is DatatypeMembership) {

+          DatatypeMembership membership = (DatatypeMembership)func;

+          return ExprLineariser.Namer.GetQuotedName(membership, "is-" + membership.constructor.Name);

         }

         else {

           return null;

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 0bc41c2a..4a4ecfb6 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -171,7 +171,7 @@ void ObjectInvariant()
       else if (node.Op is VCExprSelectOp) RegisterSelect(node);

       else {

         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;

-        if (op != null && !IsDatatypeConstructor(op.Func) && !KnownFunctions.Contains(op.Func)) {

+        if (op != null && !IsDatatypeFunction(op.Func) && !KnownFunctions.Contains(op.Func)) {

           Function f = op.Func;

           Contract.Assert(f != null);

           

@@ -264,12 +264,11 @@ void ObjectInvariant()
       return QKeyValue.FindBoolAttribute(ctorType.Decl.Attributes, "datatype");

     }

 

-    public static bool IsDatatypeConstructor(Function f) {

-      return QKeyValue.FindBoolAttribute(f.Attributes, "constructor");

-    }

-

-    public static bool IsDatatypeSelector(Function f) {

-      return QKeyValue.FindBoolAttribute(f.Attributes, "selector");

+    public static bool IsDatatypeFunction(Function f) {

+      return

+        QKeyValue.FindBoolAttribute(f.Attributes, "constructor") ||

+        f is DatatypeSelector ||

+        f is DatatypeMembership;

     }

 

     private void RegisterSelect(VCExprNAry node)

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 26361cdf..ed698d5f 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -25,12 +25,10 @@ namespace Microsoft.Boogie {
 

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(counterexample != null);

       Contract.Invariant(cce.NonNullElements(args));

     }

 

     public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {

-      Contract.Requires(cex != null);

       Contract.Requires(cce.NonNullElements(x));

       counterexample = cex;

       args = x;

diff --git a/Test/datatypes/Answer b/Test/datatypes/Answer
new file mode 100644
index 00000000..7b7b411a
--- /dev/null
+++ b/Test/datatypes/Answer
@@ -0,0 +1,14 @@
+

+-------------------- t1.bpl --------------------

+t1.bpl(23,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    t1.bpl(16,3): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

+-------------------- t2.bpl --------------------

+t2.bpl(23,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    t2.bpl(16,3): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

diff --git a/Test/datatypes/runtest.bat b/Test/datatypes/runtest.bat
index e796c905..fe2aa09d 100644
--- a/Test/datatypes/runtest.bat
+++ b/Test/datatypes/runtest.bat
@@ -4,7 +4,7 @@ setlocal
 set BOOGIEDIR=..\..\Binaries

 set BPLEXE=%BOOGIEDIR%\Boogie.exe

 

-for %%f in (t1.bpl) do (

+for %%f in (t1.bpl t2.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BPLEXE% %* /typeEncoding:m %%f

diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl
index f794b227..d4d2bf3f 100644
--- a/Test/datatypes/t2.bpl
+++ b/Test/datatypes/t2.bpl
@@ -1,62 +1,24 @@
+type TT;

+type {:datatype} Tree;

+function {:constructor} leaf`0() : Tree;

+function {:constructor} node`2(value:TT, children:TreeList) : Tree;

 

-type {:datatype} DotNetType;

+type {:datatype} TreeList;

+function {:constructor} cons`2(car:Tree, cdr:TreeList) : TreeList;

+function {:constructor} nil`0() : TreeList;

 

-/*\

- *  Subtype Axioms

-\*/

-function $Subtype(DotNetType, DotNetType) : bool;

-// reflexive

-axiom (forall t: DotNetType :: $Subtype(t, t));

-// anti-symmetric

-axiom (forall t0: DotNetType, t1: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t0) } $Subtype(t0, t1) && $Subtype(t1, t0) ==> t0 == t1);

-// transitive

-axiom (forall t0: DotNetType, t1: DotNetType, t2: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t2) } $Subtype(t0, t1) && $Subtype(t1, t2) ==> $Subtype(t0, t2));

-

-/*\

- *  Type Declarations

-\*/

-// class System.Object { ... }

-function {:constructor} System.Object() : DotNetType;

-

-// class B : System.Object { ... }

-function {:constructor} B() : DotNetType;

-axiom $Subtype(B(), System.Object());

-

-// class GenericType1<T> : System.Object { ... }

-function {:constructor} GenericType1(T:DotNetType) : DotNetType;

-axiom (forall t : DotNetType :: $Subtype(GenericType1(t), System.Object()));

-

-// class C : GenericType1<object>

-function {:constructor} C() : DotNetType;

-axiom $Subtype(C(), GenericType1(System.Object()));

-

-// class D<U> : GenericType1<U>

-function {:constructor} D(U:DotNetType) : DotNetType;

-axiom (forall u : DotNetType :: $Subtype(D(u), GenericType1(u)));

-

-// class GenericType2<T,U> : System.Object { ... }

-function {:constructor} GenericType2(T:DotNetType, U:DotNetType) : DotNetType;

-axiom (forall t : DotNetType, u : DotNetType :: $Subtype(GenericType2(t,u), System.Object()));

-

-

-procedure foo(t : DotNetType) 

+procedure foo() 

 {

-  assert System.Object() != GenericType1(t);

-  assert System.Object() != B();

-}

+  var a: Tree;

+  var b: TreeList;

+  var x: TT;

 

-procedure bar(t : DotNetType, u : DotNetType) 

-  requires t != u;

-{

-  assert System.Object() != GenericType1(t);

-  assert System.Object() != B();

-  assert GenericType1(t) != GenericType1(u);

-}

+  assert value#node`2(node`2(x, nil`0())) == x;

+  assert children#node`2(node`2(x, nil`0())) == nil`0();

+  

+  assert (cons`2(leaf`0(), nil`0()) != nil`0());

 

-function IntToType(x : int) : DotNetType;

-procedure baz(i : int)

-{

-  var t : DotNetType;

-  t := IntToType(i);

-  assert T#GenericType1(t) == System.Object();

+  assert is#nil`0(nil`0());

+

+  assert is#node`2(leaf`0());

 }
\ No newline at end of file