From 06bced1a698956204fcae27c5decd4418e120456 Mon Sep 17 00:00:00 2001 From: Sergey Tepliakov Date: Sat, 24 Oct 2015 18:56:20 -0700 Subject: [PATCH 1/4] Fix for #235 Add type mapping to change generic type reference in async closure that is called from generic async methods. --- Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs | 273 ++++++++++++++++-- .../Rewriting/Utils/TypeNodeExtensions.cs | 5 + 2 files changed, 259 insertions(+), 19 deletions(-) diff --git a/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs b/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs index 749325e6..46ceeaaf 100644 --- a/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs +++ b/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs @@ -1,7 +1,6 @@ using System; using System.Collections.Generic; using System.Compiler; -using System.Diagnostics; using System.Diagnostics.Contracts; using System.Linq; using System.Threading.Tasks; @@ -59,6 +58,121 @@ namespace Microsoft.Contracts.Foxtrot /// internal class EmitAsyncClosure : StandardVisitor { + /// + /// Class that maps generic arguments of the enclosed class/method the generic arguments of the closure. + /// + /// + /// The problem. + /// Original implementation of the Code Contract didn't support async postconditions in generics. + /// Here is why: + /// Suppose we have following function (in class Foo: + /// FooAsync() where T: class + /// { + /// Contract.Ensures(Contract.Result() != null); + /// } + /// ]]> + /// In this case, ccrewrite will generate async closure class called Foo.AsyncContractClosure_0<T%gt; + /// with following structure: + /// AsyncContractClosure_0 where T : class + /// { + /// public Task CheckPost(Task task) + /// { + /// TaskStatus status = task.Status; + /// if (status == TaskStatus.RanToCompletion) + /// { + /// RewriterMethods.Ensures(task.Result != null, null, "Contract.Result() != null"); + /// } + /// return task; + /// } + /// } + /// ]]> + /// + /// The code looks good, but the IL could be invalid (without the trick that this class provides). + /// Postcondition of the method in our case is declared in the generic method (in FooAsync) + /// but ccrewrite moves it into non-generic method (CheckPost) of the generic class (closure). + /// + /// But on IL level there is different instructions for referencing method generic arguments and type generic arguments. + /// + /// After changing Contract.Result to task.Result and moving postcondition to CheckPost + /// method, following IL would be generated: + /// + /// ::get_Result() + /// IL_0016: box !!0 // <-- here is our problem! + /// ]]> + /// + /// + /// This means that method CheckPost would contains a reference to generic method argument of the + /// original method. + /// + /// The goal of this class is to store a mapping between enclosing generic types and closure generic types. + /// + private class GenericTypeMapper + { + class TypeNodePair + { + public TypeNodePair(TypeNode enclosingGenericType, TypeNode closureGenericType) + { + EnclosingGenericType = enclosingGenericType; + ClosureGenericType = closureGenericType; + } + + public TypeNode EnclosingGenericType { get; private set; } + public TypeNode ClosureGenericType { get; private set; } + } + + // Mapping between enclosing generic type and closure generic type. + // This is a simple list not a dictionary, because number of generic arguments is very small. + // So linear complexity will not harm performance. + private List typeParametersMapping = new List(); + + public bool IsEmpty { get { return typeParametersMapping.Count == 0; } } + + public void AddMapping(TypeNode enclosingGenericType, TypeNode closureGenericType) + { + typeParametersMapping.Add(new TypeNodePair(enclosingGenericType, closureGenericType)); + } + + /// + /// Returns associated generic type of the closure class by enclosing generic type (for instance, by + /// generic type of the enclosing generic method that uses current closure). + /// + /// + /// Function returns the same argument if the matching argument does not exists. + /// + public TypeNode GetClosureTypeParameterByEnclosingTypeParameter(TypeNode enclosingType) + { + if (enclosingType == null) + { + return null; + } + + var candidate = typeParametersMapping.FirstOrDefault(t => t.EnclosingGenericType == enclosingType); + return candidate != null ? candidate.ClosureGenericType : enclosingType; + } + + /// + /// Returns associated generic type of the closure class by enclosing generic type (for instance, by + /// generic type of the enclosing generic method that uses current closure). + /// + /// + /// Function returns the same argument if the matching argument does not exists. + /// + public TypeNode GetEnclosingTypeParamterByGenericTypeParameter(TypeNode closureType) + { + if (closureType == null) + { + return null; + } + + var candidate = typeParametersMapping.FirstOrDefault(t => t.ClosureGenericType == closureType); + return candidate != null ? candidate.EnclosingGenericType : closureType; + } + } + // This assembly should be in this class but not in the SystemTypes from System.CompilerCC. // Moving this type there will lead to test failures and assembly resolution errors. private static readonly AssemblyNode/*!*/ SystemCoreAssembly = SystemTypes.GetSystemCoreAssembly(false, true); @@ -92,6 +206,8 @@ internal class EmitAsyncClosure : StandardVisitor private Parameter checkMethodTaskParameter; private readonly TypeNode checkMethodTaskType; + private readonly GenericTypeMapper genericTypeMapper = new GenericTypeMapper(); + public EmitAsyncClosure(Method from, Rewriter rewriter) { Contract.Requires(from != null); @@ -132,21 +248,45 @@ public EmitAsyncClosure(Method from, Rewriter rewriter) this.func2Type = new Cache(() => HelperMethods.FindType(SystemTypes.SystemAssembly, StandardIds.System, Identifier.For("Func`2"))); - if (from.IsGeneric) + // Should distinguish between generic enclosing method and non-generic method in enclosing type. + // In both cases generated closure should be generic. + Func getGenericTypesFrom = method => + { + if (method.IsGeneric) + { + return from.TemplateParameters; + } + + if (method.DeclaringType.IsGeneric) + { + return method.DeclaringType.TemplateParameters; + } + + return null; + }; + + var enclosingTemplateParameters = getGenericTypesFrom(from); + + if (!enclosingTemplateParameters.IsNullOrEmpty()) { - this.closureClass.TemplateParameters = CreateTemplateParameters(closureClass, from, declaringType); + this.closureClass.TemplateParameters = CreateTemplateParameters(closureClass, enclosingTemplateParameters, declaringType); this.closureClass.IsGeneric = true; this.closureClass.EnsureMangledName(); this.forwarder = new Specializer( targetModule: this.declaringType.DeclaringModule, - pars: from.TemplateParameters, + pars: enclosingTemplateParameters, args: this.closureClass.TemplateParameters); this.forwarder.VisitTypeParameterList(this.closureClass.TemplateParameters); taskType = this.forwarder.VisitTypeReference(taskType); + + for (int i = 0; i < enclosingTemplateParameters.Count; i++) + { + this.genericTypeMapper.AddMapping(enclosingTemplateParameters[i], closureClass.TemplateParameters[i]); + } } else { @@ -180,11 +320,13 @@ public EmitAsyncClosure(Method from, Rewriter rewriter) consArgs.Add(this.closureClass.DeclaringType.ConsolidatedTemplateParameters[i]); } - var methodCount = from.TemplateParameters == null ? 0 : from.TemplateParameters.Count; - for (int i = 0; i < methodCount; i++) + if (!enclosingTemplateParameters.IsNullOrEmpty()) { - consArgs.Add(from.TemplateParameters[i]); - args.Add(from.TemplateParameters[i]); + for (int i = 0; i < enclosingTemplateParameters.Count; i++) + { + consArgs.Add(enclosingTemplateParameters[i]); + args.Add(enclosingTemplateParameters[i]); + } } this.closureClassInstance = @@ -197,8 +339,7 @@ public EmitAsyncClosure(Method from, Rewriter rewriter) this.closureLocal = new Local(this.ClosureClass); this.ClosureInitializer = new Block(new StatementList()); - // TODO: What is this? - // Add ClosureLocal instantiation? + // Generate constructor call that initializes closure instance this.ClosureInitializer.Statements.Add( new AssignmentStatement( this.closureLocal, @@ -219,8 +360,6 @@ public void AddAsyncPostconditions(List asyncPostconditions, Block retu Contract.Requires(taskBasedResult != null); Contract.Requires(asyncPostconditions.Count > 0); - Contract.Assume(taskBasedResult.Type == checkMethodTaskType); - // Async postconditions are impelemented using custom closure class // with CheckPost method that checks postconditions when the task // is finished. @@ -262,20 +401,24 @@ private InstanceInitializer Ctor { get { return (InstanceInitializer)this.closureClassInstance.GetMembersNamed(StandardIds.Ctor)[0]; } } - + [Pure] - private static TypeNodeList CreateTemplateParameters(Class closureClass, Method @from, TypeNode declaringType) + private static TypeNodeList CreateTemplateParameters(Class closureClass, TypeNodeList inputTemplateParameters, TypeNode declaringType) { + Contract.Requires(closureClass != null); + Contract.Requires(inputTemplateParameters != null); + Contract.Requires(declaringType != null); + var dup = new Duplicator(declaringType.DeclaringModule, declaringType); var templateParameters = new TypeNodeList(); var parentCount = declaringType.ConsolidatedTemplateParameters.CountOrDefault(); - for (int i = 0; i < from.TemplateParameters.Count; i++) + for (int i = 0; i < inputTemplateParameters.Count; i++) { var tp = HelperMethods.NewEqualTypeParameter( - dup, (ITypeParameter)from.TemplateParameters[i], + dup, (ITypeParameter)inputTemplateParameters[i], closureClass, parentCount + i); templateParameters.Add(tp); @@ -446,6 +589,15 @@ private void AddAsyncPost(List asyncPostconditions) Method contractEnsuresMethod = this.rewriter.RuntimeContracts.EnsuresMethod; + // For generic types need to 'fix' generic type parameters that are used in the closure method. + // See comment to the GenericTypeMapper for more details. + TypeParameterFixerVisitor fixer = null; + + if (!this.genericTypeMapper.IsEmpty) + { + fixer = new TypeParameterFixerVisitor(genericTypeMapper); + } + foreach (Ensures e in GetTaskResultBasedEnsures(asyncPostconditions)) { // TODO: Not sure that 'break' is enough! It seems that this is possible @@ -461,6 +613,11 @@ private void AddAsyncPost(List asyncPostconditions) // ExpressionList args = new ExpressionList(); + if (fixer != null) + { + fixer.Visit(e.PostCondition); + } + args.Add(e.PostCondition); args.Add(e.UserMessage ?? Literal.Null); @@ -504,7 +661,10 @@ private void AddAsyncPost(List asyncPostconditions) methodBodyBlock.Statements.Add(new Block(checkStatusStatements)); // Emit a check for __ContractsRuntime.insideContractEvaluation around Ensures - this.rewriter.EmitRecursionGuardAroundChecks(this.checkPostMethod, methodBodyBlock, ensuresChecks); + // TODO ST: there is no sense to add recursion check in async postcondition that can be checked in different thread! + methodBodyBlock.Statements.Add(new Block(ensuresChecks)); + // Emit a check for __ContractsRuntime.insideContractEvaluation around Ensures + //this.rewriter.EmitRecursionGuardAroundChecks(this.checkPostMethod, methodBodyBlock, ensuresChecks); // Now, normal postconditions are written to the method body. // We need to add endOfNormalPostcondition block as a marker. @@ -572,6 +732,71 @@ private void AddAsyncPost(List asyncPostconditions) methodBody.Add(returnBlock); } + /// + /// Helper visitor class that changes all references to type parameters to appropriate once. + /// + private class TypeParameterFixerVisitor : StandardVisitor + { + private readonly GenericTypeMapper genericParametersMapping; + + public TypeParameterFixerVisitor(GenericTypeMapper genericParametersMapping) + { + Contract.Requires(genericParametersMapping != null); + this.genericParametersMapping = genericParametersMapping; + } + + // Literal is used when contract result compares to null: Contract.Result() != null + public override Expression VisitLiteral(Literal literal) + { + var origin = literal.Value as TypeNode; + if (origin == null) + { + return base.VisitLiteral(literal); + } + + var newLiteralType = this.genericParametersMapping.GetClosureTypeParameterByEnclosingTypeParameter(origin); + if (newLiteralType != origin) + { + return new Literal(newLiteralType); + } + + return base.VisitLiteral(literal); + } + + public override TypeNode VisitTypeParameter(TypeNode typeParameter) + { + var fixedVersion = this.genericParametersMapping.GetClosureTypeParameterByEnclosingTypeParameter(typeParameter); + if (fixedVersion != typeParameter) + { + return fixedVersion; + } + + return base.VisitTypeParameter(typeParameter); + } + + public override TypeNode VisitTypeReference(TypeNode type) + { + var fixedVersion = this.genericParametersMapping.GetClosureTypeParameterByEnclosingTypeParameter(type); + if (fixedVersion != type) + { + return fixedVersion; + } + + return base.VisitTypeReference(type); + } + + public override TypeNode VisitTypeNode(TypeNode typeNode) + { + var fixedVersion = this.genericParametersMapping.GetClosureTypeParameterByEnclosingTypeParameter(typeNode); + if (fixedVersion != typeNode) + { + return fixedVersion; + } + + return base.VisitTypeNode(typeNode); + } + } + private static IEnumerable GetTaskResultBasedEnsures(List asyncPostconditions) { return asyncPostconditions.Where(post => !(post is EnsuresExceptional)); @@ -586,7 +811,7 @@ private static IEnumerable GetExceptionalEnsures(List [Pure] - private static Member GetUnwrapMethod(TypeNode checkMethodTaskType) + private Member GetUnwrapMethod(TypeNode checkMethodTaskType) { Contract.Requires(checkMethodTaskType != null); Contract.Ensures(Contract.Result() != null); @@ -614,7 +839,17 @@ private static Member GetUnwrapMethod(TypeNode checkMethodTaskType) { // We need to "instantiate" generic first. // I.e. for Task we need to have Unwrap(Task>): Task - return genericUnwrapCandidate.GetTemplateInstance(null, checkMethodTaskType.TemplateArguments[0]); + + // In this case we need to map back generic types. + // CheckPost method is a non-generic method from (potentially) generic closure class. + // In this case, if enclosing method is generic we need to map generic types back + // and use !!0 (reference to method template arg) instead of using !0 (which is reference + // to closure class template arg). + var enclosingGeneritType = + this.genericTypeMapper.GetEnclosingTypeParamterByGenericTypeParameter( + checkMethodTaskType.TemplateArguments[0]); + + return genericUnwrapCandidate.GetTemplateInstance(null, enclosingGeneritType); } return nonGenericUnwrapCandidate; diff --git a/Foxtrot/Driver/Rewriting/Utils/TypeNodeExtensions.cs b/Foxtrot/Driver/Rewriting/Utils/TypeNodeExtensions.cs index 8bac4169..0e843439 100644 --- a/Foxtrot/Driver/Rewriting/Utils/TypeNodeExtensions.cs +++ b/Foxtrot/Driver/Rewriting/Utils/TypeNodeExtensions.cs @@ -26,5 +26,10 @@ public static int CountOrDefault(this TypeNodeList list) { return list == null ? 0 : list.Count; } + + public static bool IsNullOrEmpty(this TypeNodeList list) + { + return list == null || list.Count == 0; + } } } \ No newline at end of file From 173ad8e0d847f5c8940c697a96cf85f8902fc012 Mon Sep 17 00:00:00 2001 From: Sergey Tepliakov Date: Sat, 24 Oct 2015 18:56:46 -0700 Subject: [PATCH 2/4] Additional test cases for async postconditions. Conflicts: Foxtrot/Tests/FoxtrotTests10.csproj --- .../AsyncPostconditionInGenericClass.cs | 52 + .../AsyncPostconditionInGenericClass2.cs | 52 + .../AsyncPostconditionInGenericMethod.cs | 53 + .../AsyncPostconditionInGenericMethod2.cs | 53 + .../AsyncPostconditionInGenericMethod3.cs | 54 + ...yncPostconditionInGenericMethodInStruct.cs | 52 + .../ExceptionalAsyncPostcondition.cs | 2 +- ...tionalAsyncPostconditionInGenericMethod.cs | 72 + ...ionalAsyncPostconditionInGenericMethod2.cs | 70 + .../{ => ExtractorTests}/ExtractorTest.cs | 2 +- Foxtrot/Tests/FoxtrotTests10.csproj | 4 +- Foxtrot/Tests/Options.cs | 18 + .../RewriterTests/AsyncTestsDataSource.cs | 73 + Foxtrot/Tests/RewriterTests/RewriterTest.cs | 1978 +++++++++++++++++ 14 files changed, 2531 insertions(+), 4 deletions(-) create mode 100644 Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass.cs create mode 100644 Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass2.cs create mode 100644 Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod.cs create mode 100644 Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod2.cs create mode 100644 Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod3.cs create mode 100644 Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethodInStruct.cs create mode 100644 Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostconditionInGenericMethod.cs create mode 100644 Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostconditionInGenericMethod2.cs rename Foxtrot/Tests/{ => ExtractorTests}/ExtractorTest.cs (99%) create mode 100644 Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs create mode 100644 Foxtrot/Tests/RewriterTests/RewriterTest.cs diff --git a/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass.cs b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass.cs new file mode 100644 index 00000000..781fa9ed --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass.cs @@ -0,0 +1,52 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + + class FooClass where T: class + { + public static Task Foo(T source) + { + Contract.Ensures(Contract.Result() != null); + + return Task.FromResult(source); + } + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + FooClass.Foo(new object()).Wait(); + } + else + { + FooClass.Foo(null).Wait(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Postcondition; + public string NegativeExpectedCondition = "Contract.Result() != null"; + } +} diff --git a/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass2.cs b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass2.cs new file mode 100644 index 00000000..c0d2133d --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass2.cs @@ -0,0 +1,52 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + + class FooClass where U: class + { + public static Task Foo(U source) + { + Contract.Ensures(Contract.Result() != null); + + return Task.FromResult(source); + } + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + FooClass.Foo(new object()).Wait(); + } + else + { + FooClass.Foo(null).Wait(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Postcondition; + public string NegativeExpectedCondition = "Contract.Result() != null"; + } +} diff --git a/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod.cs b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod.cs new file mode 100644 index 00000000..f417dc17 --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod.cs @@ -0,0 +1,53 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + + class FooClass + { + public static Task Foo(T source) where T : class + { + Contract.Ensures(Contract.Result() != null); + + return Task.FromResult(source); + } + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + FooClass.Foo(new object()).Wait(); + } + else + { + FooClass.Foo(null).Wait(); + // throw new ArgumentNullException(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Postcondition; + public string NegativeExpectedCondition = "Contract.Result() != null"; + } +} diff --git a/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod2.cs b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod2.cs new file mode 100644 index 00000000..15dbd72e --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod2.cs @@ -0,0 +1,53 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + + class FooClass + { + public static Task Foo(U source) where U : class + { + Contract.Ensures(Contract.Result() != null); + + return Task.FromResult(source); + } + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + FooClass.Foo(new object()).Wait(); + } + else + { + FooClass.Foo(null).Wait(); + // throw new ArgumentNullException(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Postcondition; + public string NegativeExpectedCondition = "Contract.Result() != null"; + } +} diff --git a/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod3.cs b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod3.cs new file mode 100644 index 00000000..edc3d09a --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod3.cs @@ -0,0 +1,54 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + + class FooClass + { + public Task Foo(U source) where U : class where T: U + { + Contract.Ensures(Contract.Result() != null); + Contract.Ensures((T)Contract.Result() != null); + + return Task.FromResult(source); + } + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + new FooClass().Foo("foo").Wait(); + } + else + { + new FooClass().Foo(null).Wait(); + // throw new ArgumentNullException(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Postcondition; + public string NegativeExpectedCondition = "Contract.Result() != null"; + } +} diff --git a/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethodInStruct.cs b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethodInStruct.cs new file mode 100644 index 00000000..6420f69b --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethodInStruct.cs @@ -0,0 +1,52 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + + struct FooStruct + { + public Task Foo(T source) where T : class + { + Contract.Ensures(Contract.Result() != null); + + return Task.FromResult(source); + } + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + new FooStruct().Foo(new object()).Wait(); + } + else + { + new FooStruct().Foo(null).Wait(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Postcondition; + public string NegativeExpectedCondition = "Contract.Result() != null"; + } +} diff --git a/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostcondition.cs b/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostcondition.cs index 4249f259..f8d669a1 100644 --- a/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostcondition.cs +++ b/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostcondition.cs @@ -40,7 +40,7 @@ public static async Task HandleFooAsync() { try { - // If async postcondition are implemented properly + // When async postcondition are implemented properly // they should not affect exception handling when the method throws. await new Foo().FooAsync(); } diff --git a/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostconditionInGenericMethod.cs b/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostconditionInGenericMethod.cs new file mode 100644 index 00000000..96d80598 --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostconditionInGenericMethod.cs @@ -0,0 +1,72 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + + class Foo + { + + private Task FooAsync(T t) where T: class + { + Contract.Ensures(Contract.Result() != null); + + //await Task.Delay(42); + + throw new InvalidOperationException(); + + //return t; + } + + public static async Task HandleFooAsync(string arg) + { + try + { + // When async postcondition are implemented properly + // they should not affect exception handling when the method throws. + await new Foo().FooAsync(arg); + await Task.Delay(42); + } + catch (InvalidOperationException) + { + Console.WriteLine("Exception should be handled!"); + } + } + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + Foo.HandleFooAsync("foo").Wait(); + } + else + { + throw new ArgumentNullException(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Precondition; + public string NegativeExpectedCondition = "Value cannot be null."; + } +} diff --git a/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostconditionInGenericMethod2.cs b/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostconditionInGenericMethod2.cs new file mode 100644 index 00000000..11f62ea2 --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/ExceptionalAsyncPostconditionInGenericMethod2.cs @@ -0,0 +1,70 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + + class Foo + { + private async Task FooAsync(T t) where T: class + { + Contract.Ensures(Contract.Result() != null); + + await Task.Delay(42); + + throw new InvalidOperationException(); + + //return t; + } + + public static async Task HandleFooAsync(string arg) + { + try + { + // When async postcondition are implemented properly + // they should not affect exception handling when the method throws. + await new Foo().FooAsync(arg); + } + catch (InvalidOperationException) + { + Console.WriteLine("Exception should be handled!"); + } + } + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + Foo.HandleFooAsync("foo").Wait(); + } + else + { + throw new ArgumentNullException(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Precondition; + public string NegativeExpectedCondition = "Value cannot be null."; + } +} diff --git a/Foxtrot/Tests/ExtractorTest.cs b/Foxtrot/Tests/ExtractorTests/ExtractorTest.cs similarity index 99% rename from Foxtrot/Tests/ExtractorTest.cs rename to Foxtrot/Tests/ExtractorTests/ExtractorTest.cs index 998bf8a1..ea572737 100644 --- a/Foxtrot/Tests/ExtractorTest.cs +++ b/Foxtrot/Tests/ExtractorTests/ExtractorTest.cs @@ -17,7 +17,7 @@ using Xunit; using Xunit.Abstractions; -namespace Tests +namespace Tests.ExtractorTests { /// /// Unit tests for ExtractorTests diff --git a/Foxtrot/Tests/FoxtrotTests10.csproj b/Foxtrot/Tests/FoxtrotTests10.csproj index 3cba4c56..6db424c4 100644 --- a/Foxtrot/Tests/FoxtrotTests10.csproj +++ b/Foxtrot/Tests/FoxtrotTests10.csproj @@ -93,10 +93,8 @@ - - @@ -115,6 +113,8 @@ + + diff --git a/Foxtrot/Tests/Options.cs b/Foxtrot/Tests/Options.cs index 4056652d..05561803 100644 --- a/Foxtrot/Tests/Options.cs +++ b/Foxtrot/Tests/Options.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Collections.ObjectModel; +using System.Diagnostics.Contracts; using System.IO; using System.Linq; @@ -249,6 +250,23 @@ public Options( this.RootDirectory = Path.GetFullPath(RelativeRoot); } + public Options WithSourceFile(string sourceFile) + { + Contract.Requires(!string.IsNullOrEmpty(sourceFile)); + + return new Options( + sourceFile: sourceFile, + foxtrotOptions: FoxtrotOptions, + useContractReferenceAssemblies: UseContractReferenceAssemblies, + compilerOptions: CompilerOptions, + references: References.ToArray(), + libPaths: LibPaths.ToArray(), + compilerCode: compilerCode, + useBinDir: UseBinDir, + useExe: UseExe, + mustSucceed: MustSucceed); + } + public bool ReleaseMode { get; set; } private static string LoadString(System.Data.DataRow dataRow, string name) diff --git a/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs b/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs new file mode 100644 index 00000000..e4d63be8 --- /dev/null +++ b/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs @@ -0,0 +1,73 @@ +using System.Collections.Generic; +using System.Linq; + +namespace Tests +{ + internal sealed class AsyncTestsDataSource + { + private static readonly Options OptionsTemplate = new Options( + sourceFile: @"dummy_file", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new[] { @"System.dll", @"System.Core.dll", @"System.Threading.Tasks.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + + public static string[] SourceFiles = new[] + { + @"Foxtrot\Tests\AsyncTests\AsyncWithoutAwait.cs", + @"Foxtrot\Tests\AsyncTests\AsyncInGenericClass.cs", + @"Foxtrot\Tests\AsyncTests\AsyncInGenericClass.cs", + @"Foxtrot\Tests\AsyncTests\AsyncEnsuresWithInterface.cs", + }; + + public static IEnumerable BaseTestCases + { + get + { + var sourceFiles = new[] + { + @"Foxtrot\Tests\AsyncTests\AsyncWithoutAwait.cs", + @"Foxtrot\Tests\AsyncTests\AsyncInGenericClass.cs", + @"Foxtrot\Tests\AsyncTests\AsyncInGenericClass.cs", + @"Foxtrot\Tests\AsyncTests\AsyncEnsuresWithInterface.cs", + }; + + return sourceFiles.Select(f => OptionsTemplate.WithSourceFile(f)); + } + } + + public static IEnumerable AsyncPostconditionsTestCases + { + get + { + var sourceFiles = new[] + { + @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericClass.cs", + @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericClass2.cs", + + @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericMethod.cs", + @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericMethod2.cs", + @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericMethod3.cs", + + @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericMethodInStruct.cs", + + @"Foxtrot\Tests\AsyncPostconditions\CancelledAsyncPostcondition.cs", + @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionsInInterface.cs", + @"Foxtrot\Tests\AsyncPostconditions\MixedAsyncPostcondition.cs", + @"Foxtrot\Tests\AsyncPostconditions\NormalAsyncPostcondition.cs", + + @"Foxtrot\Tests\AsyncPostconditions\ExceptionalAsyncPostcondition.cs", + @"Foxtrot\Tests\AsyncPostconditions\ExceptionalAsyncPostconditionInGenericMethod.cs", + @"Foxtrot\Tests\AsyncPostconditions\ExceptionalAsyncPostconditionInGenericMethod2.cs", + }; + + return sourceFiles.Select(f => OptionsTemplate.WithSourceFile(f)); + } + } + } +} \ No newline at end of file diff --git a/Foxtrot/Tests/RewriterTests/RewriterTest.cs b/Foxtrot/Tests/RewriterTests/RewriterTest.cs new file mode 100644 index 00000000..2a80ebf9 --- /dev/null +++ b/Foxtrot/Tests/RewriterTests/RewriterTest.cs @@ -0,0 +1,1978 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using Xunit; +using Xunit.Abstractions; + +namespace Tests +{ + /// + /// Unit tests for ccrewriter a.k.a. Foxtrot + /// + public class RewriterTest + { + const string FrameworkBinariesToRewritePath = @"Foxtrot\Tests\RewriteExistingBinaries\"; + + private readonly ITestOutputHelper _testOutputHelper; + + public RewriterTest(ITestOutputHelper testOutputHelper) + { + _testOutputHelper = testOutputHelper; + } + + #region Test Data + + public static IEnumerable AsyncTests + { + get + { + return Enumerable.Range(0, AsyncTestsDataSource.BaseTestCases.Count()).Select(i => new object[] { i }); + } + } + + public static IEnumerable AsyncPostconditions + { + get + { + return Enumerable.Range(0, AsyncTestsDataSource.AsyncPostconditionsTestCases.Count()).Select(i => new object[] { i }); + } + } + + + private static IEnumerable TestFileData + { + get + { + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\RequiresForAll.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\ComplexGeneric.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\PostAmbleDeletion.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\StaticOldValue.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\AbbrevGenLit.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\AbbrevGenClosure.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\ClosureOnlyBody.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\ClosureCtor.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\GenericInterfaceMethods.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\GenericConstraints.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\DupTest.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\ContractClassRemnants.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritClosureMatchingExistingClosure.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InvariantOnCtorThrow.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritRequirePublicSurface.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\ClosureAfterRequires.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\TestClosureDeletion.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\ClosureDeletionWithAbbrev.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async1.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async1.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async2.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async2.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async3.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async3.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async4.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async4.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async5.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async5.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async6.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async6.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async6b.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async6b.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async7.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async7.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async8.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async8.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async9.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async9.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async10.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async10.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async11.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async11.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async12.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async12.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async_EnsuresWithCapturedForAll.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Iterator1.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Iterator1.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Iterator2.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Iterator2.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Iterator3.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Iterator3.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritHiddenEnsures.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\BaseInvariantDelayed.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\GenericInstanceClosure.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritGenericTypeProtected.cs", + foxtrotOptions: @"/csr", + useContractReferenceAssemblies: false, + compilerOptions: @"/d:LOCALBASE", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritGenericProtected.cs", + foxtrotOptions: @"/csr", + useContractReferenceAssemblies: false, + compilerOptions: @"/d:LOCALBASE", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritOOBProtected.cs", + foxtrotOptions: @"/csr", + useContractReferenceAssemblies: false, + compilerOptions: @"/d:LOCALBASE", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritOOBClosure.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AssemblyWithContracts.dll" }, + libPaths: @"Foxtrot\Tests\AssemblyWithContracts\bin\Debug".Split(new[] { ';' }, StringSplitOptions.RemoveEmptyEntries), + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\IteratorWithLegacyPrecondition.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\DefaultParameter.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\DefaultExpression.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritGenericAbstractClass.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritGenericAbstractClass.cs", + foxtrotOptions: @"/csr", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritGenericClosurePre.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritGenericClosurePre.cs", + foxtrotOptions: @"/csr", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritExists.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AssemblyWithContracts.dll" }, + libPaths: @"Foxtrot\Tests\AssemblyWithContracts\bin\Debug".Split(new[] { ';' }, StringSplitOptions.RemoveEmptyEntries), + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritForall.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"AssemblyWithContracts.dll" }, + libPaths: @"Foxtrot\Tests\AssemblyWithContracts\bin\Debug".Split(new[] { ';' }, StringSplitOptions.RemoveEmptyEntries), + compilerCode: "", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritGenericExists.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"AssemblyWithContracts.dll" }, + libPaths: @"Foxtrot\Tests\AssemblyWithContracts\bin\Debug".Split(new[] { ';' }, StringSplitOptions.RemoveEmptyEntries), + compilerCode: "", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritGenericForall.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"AssemblyWithContracts.dll" }, + libPaths: @"Foxtrot\Tests\AssemblyWithContracts\bin\Debug".Split(new[] { ';' }, StringSplitOptions.RemoveEmptyEntries), + compilerCode: "", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritPost.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritPre.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritPreEx.cs", + foxtrotOptions: @"-assemblyMode=standard", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritPreLegacy.cs", + foxtrotOptions: @"-assemblyMode=standard", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritPreLegacyManual.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InterleavedValidations.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InterleavedValidationsInherit.cs", + foxtrotOptions: @"-assemblyMode=standard", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\OOBinterfacePost.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\OOBInterfacePre.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\OOBInterfacePreGeneric.cs", + foxtrotOptions: @"/callsiterequires", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new[] { @"AssemblyWithContracts.dll", @"System.Core.dll" }, + libPaths: @"Foxtrot\Tests\AssemblyWithContracts\bin\Debug".Split(new[] { ';' }, StringSplitOptions.RemoveEmptyEntries), + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\OOBPost.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\OOBPre.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritPreInterface.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritClosureWithStelem.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritClosureWithStelem.cs", + foxtrotOptions: @"/callsiterequires", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + } + } + + public static IEnumerable TestFile + { + get + { + return Enumerable.Range(0, TestFileData.Count()).Select(i => new object[] { i }); + } + } + + + private static IEnumerable RoslynCompatibilityData + { + get + { + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\ExpressionsInRequires.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll", @"System.Linq.Expressions.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\AsyncWithLegacyRequires.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\AsyncRequiresWithMultipleAwaits.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\InheritOOBClosure.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AssemblyWithContracts.dll" }, + libPaths: @"Foxtrot\Tests\AssemblyWithContracts\bin\Debug".Split(new[] { ';' }, StringSplitOptions.RemoveEmptyEntries), + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\Sources\Async12.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"/optimize", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\AbbrevGenClosure.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\CapturingContractResult.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\RequiresForAll.cs", + foxtrotOptions: @"-assemblyMode standard", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\InheritNonGenericAbstractClass.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: @"", + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\AsyncRequiresWithForAll.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: null, + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\AsyncWithoutContract.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: null, + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\InheritGenericAbstractClass.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: null, + references: new[] { @"System.Core.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\CapturingAsyncLambda.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: null, + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + } + } + + public static IEnumerable RoslynCompatibility + { + get + { + return Enumerable.Range(0, RoslynCompatibilityData.Count()).Select(i => new object[] { i }); + } + } + + + private static IEnumerable IteratorWithComplexGenericData + { + get + { + yield return new Options( + sourceFile: @"Foxtrot\Tests\RoslynCompatibility\IteratorWithTuple.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + } + } + + public static IEnumerable IteratorWithComplexGeneric + { + get + { + return Enumerable.Range(0, IteratorWithComplexGenericData.Count()).Select(i => new object[] { i }); + } + } + + + private static IEnumerable RewriteExistingData + { + get + { + yield return new Options( + sourceFile: @"mscorlib.dll", + foxtrotOptions: @"/throwonfailure=false", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.AddIn.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Core.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Design.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Xml.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"Microsoft.VisualStudio.Utilities.v11.0.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.ComponentModel.Composition.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Drawing.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.IO.Compression.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.IO.Compression.FileSystem.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Net.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Net.Http.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Net.Http.WebRequestdll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Numerics.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Reflection.Context.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Runtime.WindowsRuntime.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"System.Runtime.WindowsRuntime.UI.Xaml.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"VerifyWin8P.dll", + foxtrotOptions: @"", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + } + } + + public static IEnumerable RewriteExisting + { + get + { + return Enumerable.Range(0, RewriteExistingData.Count()).Select(i => new object[] { i }); + } + } + + + private static IEnumerable TestConfigurationData + { + get + { + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:0 /throwonfailure=false", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:1 /throwonfailure=false", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:2 /throwonfailure=false", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:3 /throwonfailure=false", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:4 /throwonfailure=false", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:0 /throwonfailure=true", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:1 /throwonfailure=true", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:2 /throwonfailure=true", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:3 /throwonfailure=true", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:4 /throwonfailure=true", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:0 /throwonfailure=true /callsiterequires", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:1 /throwonfailure=true /callsiterequires", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:2 /throwonfailure=true /callsiterequires", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:3 /throwonfailure=true /callsiterequires", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + yield return new Options( + sourceFile: @"", + foxtrotOptions: @"/level:4 /throwonfailure=true /callsiterequires", + useContractReferenceAssemblies: true, + compilerOptions: null, + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: true); + } + } + + public static IEnumerable TestConfiguration + { + get + { + return Enumerable.Range(0, TestConfigurationData.Count()).Select(i => new object[] { i }); + } + } + + + private static IEnumerable PublicSurfaceOnlyData + { + get + { + yield return new Options( + sourceFile: @"Foxtrot\Tests\PublicSurfaceOnly\IteratorWithComplexPrecondition.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: false); + yield return new Options( + sourceFile: @"Foxtrot\Tests\PublicSurfaceOnly\AsyncMethodWithComplexPrecondition.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new[] { @"AsyncCtpLibrary.dll" }, + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: false); + yield return new Options( + sourceFile: @"Foxtrot\Tests\PublicSurfaceOnly\CallPrivateRequiresShouldNotFail.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: false); + yield return new Options( + sourceFile: @"Foxtrot\Tests\PublicSurfaceOnly\CallPrivateEnsuresShouldNotFail.cs", + foxtrotOptions: @"", + useContractReferenceAssemblies: false, + compilerOptions: @"", + references: new string[0], + libPaths: new[] { @"Microsoft.Research\RegressionTest\ClousotTestHarness\bin\debug" }, + compilerCode: "CS", + useBinDir: false, + useExe: true, + mustSucceed: false); + } + } + + public static IEnumerable PublicSurfaceOnly + { + get + { + return Enumerable.Range(0, PublicSurfaceOnlyData.Count()).Select(i => new object[] { i }); + } + } + #endregion + + #region Async tests + [Theory] + [MemberData("AsyncTests")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "Roslyn"), Trait("Category", "VS14")] + public void AsyncTestsWithRoslynCompiler(int testIndex) + { + Options options = AsyncTestsDataSource.BaseTestCases.ElementAt(testIndex); + CreateRoslynOptions(options, "VS14RC3"); + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory] + [MemberData("AsyncTests")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "V4.5")] + public void AsyncTestsWithDotNet45(int testIndex) + { + Options options = AsyncTestsDataSource.BaseTestCases.ElementAt(testIndex); + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = @".NETFramework\v4.5"; + options.ContractFramework = @".NETFramework\v4.0"; + options.UseTestHarness = true; + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + #endregion + [Theory] + [MemberData("AsyncPostconditions")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "Roslyn"), Trait("Category", "VS14")] + public void TestAsyncPostconditionsWithRoslyn(int testIndex) + { + Options options = AsyncTestsDataSource.AsyncPostconditionsTestCases.ElementAt(testIndex); + CreateRoslynOptions(options, "VS14RC3"); + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + // TODO ST: it seems that the Trait("Category", "Roslyn" is invalid for this test! And VS14 as well! + [Theory] + [MemberData("AsyncPostconditions")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "Roslyn"), Trait("Category", "VS14")] + public void TestAsyncPostconditionsV45(int testIndex) + { + Options options = AsyncTestsDataSource.AsyncPostconditionsTestCases.ElementAt(testIndex); + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = @".NETFramework\v4.5"; + options.ContractFramework = @".NETFramework\v4.0"; + options.UseTestHarness = true; + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + #region Roslyn compiler unit tests + [Theory] + [MemberData("TestFile")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "Roslyn"), Trait("Category", "VS14")] + public void Roslyn_BuildRewriteRunFromSources(int testIndex) + { + Options options = TestFileData.ElementAt(testIndex); + CreateRoslynOptions(options, "VS14RC3"); + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory] + [MemberData("RoslynCompatibility")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "Roslyn"), Trait("Category", "VS14")] + public void Roslyn_CompatibilityCheck(int testIndex) + { + Options options = RoslynCompatibilityData.ElementAt(testIndex); + CreateRoslynOptions(options, "VS14RC3"); + + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory] + [MemberData("RoslynCompatibility")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "V4.5")] + public void TestTheRoslynCompatibilityCasesWithVS2013Compiler(int testIndex) + { + Options options = RoslynCompatibilityData.ElementAt(testIndex); + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = @".NETFramework\v4.5"; + options.ContractFramework = @".NETFramework\v4.0"; + options.UseTestHarness = true; + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory] + [MemberData("RoslynCompatibility")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "Roslyn"), Trait("Category", "VS14")] + public void Roslyn_CompatibilityCheckInReleaseMode(int testIndex) + { + Options options = RoslynCompatibilityData.ElementAt(testIndex); + CreateRoslynOptions(options, "VS14RC3"); + + options.CompilerOptions = "/optimize"; + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + /// + /// Unit test for #47 - "Could not resolve type reference" for some iterator methods in VS2015 and + /// #186 - ccrewrite produces an incorrect type name in IteratorStateMachineAttribute with some generic types + /// + [Theory] + [MemberData("IteratorWithComplexGeneric")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "Roslyn"), Trait("Category", "VS14")] + public void Roslyn_IteratorBlockWithComplexGeneric(int testIndex) + { + Options options = IteratorWithComplexGenericData.ElementAt(testIndex); + CreateRoslynOptions(options, "VS14RC3"); + // Bug with metadata reader could be reproduced only with a new mscorlib and new System.dll. + options.BuildFramework = @".NetFramework\v4.6"; + options.ReferencesFramework = @".NetFramework\v4.6"; + options.DeepVerify = true; + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + /// + /// Creates instance with default values suitable for testing roslyn-based compiler. + /// + /// Should be the same as a folder name in the /Imported/Roslyn folder. + private void CreateRoslynOptions(Options options, string compilerVersion) + { + // For VS14RC+ version compiler name is the same Csc.exe, and behavior from async/iterator perspective is similar + // to old compiler as well. That's why IsLegacyRoslyn should be false in this test case. + options.IsLegacyRoslyn = false; + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.CompilerPath = string.Format(@"Roslyn\{0}", compilerVersion); + options.BuildFramework = @".NetFramework\v4.5"; + options.ReferencesFramework = @".NetFramework\v4.5"; + options.ContractFramework = @".NETFramework\v4.5"; + options.UseTestHarness = true; + } + + #endregion Roslyn compiler unit tests + + [Theory] + [MemberData("RewriteExisting")] + [Trait("Category", "Runtime"), Trait("Category", "Framework"), Trait("Category", "V4.0"), Trait("Category", "CoreTest")] + public void RewriteFrameworkDlls40(int testIndex) + { + Options options = RewriteExistingData.ElementAt(testIndex); + var framework = @".NetFramework\v4.0"; + options.ContractFramework = framework; + var dllpath = FrameworkBinariesToRewritePath + framework; + options.BuildFramework = options.MakeAbsolute(dllpath); + var extrareferencedir = options.MakeAbsolute(TestDriver.ReferenceDirRoot); + options.LibPaths.Add(extrareferencedir); + options.FoxtrotOptions = options.FoxtrotOptions + " /verbose:4"; + options.UseContractReferenceAssemblies = false; + + if (File.Exists(options.MakeAbsolute(Path.Combine(dllpath, options.SourceFile)))) + { + TestDriver.RewriteBinary(_testOutputHelper, options, dllpath); + } + } + + [Theory] + [MemberData("RewriteExisting")] + [Trait("Category", "Runtime"), Trait("Category", "Framework"), Trait("Category", "V4.5"), Trait("Category", "CoreTest")] + public void RewriteFrameworkDlls45(int testIndex) + { + Options options = RewriteExistingData.ElementAt(testIndex); + var framework = @".NetFramework\v4.5"; + options.ContractFramework = framework; + var dllpath = FrameworkBinariesToRewritePath + framework; + var extrareferencedir = options.MakeAbsolute(TestDriver.ReferenceDirRoot); + options.LibPaths.Add(extrareferencedir); + options.BuildFramework = options.MakeAbsolute(dllpath); + options.FoxtrotOptions = options.FoxtrotOptions + " /verbose:4"; + options.UseContractReferenceAssemblies = false; + + if (File.Exists(options.MakeAbsolute(Path.Combine(dllpath, options.SourceFile)))) + { + TestDriver.RewriteBinary(_testOutputHelper, options, dllpath); + } + } + + [Theory] + [MemberData("TestConfiguration")] + [Trait("Category", "Runtime"), Trait("Category", "ThirdParty"), Trait("Category", "CoreTest")] + public void RewriteQuickGraph(int testIndex) + { + Options options = TestConfigurationData.ElementAt(testIndex); + //var options = new Options("QuickGraph", (string)TestContext.DataRow["FoxtrotOptions"], TestContext); + options.BuildFramework = @".NetFramework\v4.0"; + TestDriver.RewriteAndVerify(_testOutputHelper, "", @"Foxtrot\Tests\Quickgraph\QuickGraphBinaries\Quickgraph.dll", options); + } + + [Theory] + [MemberData("TestConfiguration")] + [Trait("Category", "Runtime"), Trait("Category", "ThirdParty"), Trait("Category", "CoreTest")] + public void RewriteQuickGraphData(int testIndex) + { + Options options = TestConfigurationData.ElementAt(testIndex); + //var options = new Options("QuickGraphData", (string)TestContext.DataRow["FoxtrotOptions"], TestContext); + options.BuildFramework = @".NetFramework\v4.0"; + options.FoxtrotOptions = options.FoxtrotOptions + " /verbose:4"; + options.Delete(@"Foxtrot\Tests\QuickGraph\QuickGraphBinaries\QuickGraph.Contracts.dll"); + TestDriver.RewriteAndVerify(_testOutputHelper, "", @"Foxtrot\Tests\Quickgraph\QuickGraphBinaries\Quickgraph.Data.dll", options); + } + + [Theory] + [MemberData("TestConfiguration")] + [Trait("Category", "Runtime"), Trait("Category", "ThirdParty"), Trait("Category", "CoreTest")] + public void RewriteQuickGraphDataOOB(int testIndex) + { + Options options = TestConfigurationData.ElementAt(testIndex); + //var options = new Options("QuickGraphDataOOB", (string)TestContext.DataRow["FoxtrotOptions"], TestContext); + options.BuildFramework = @".NetFramework\v4.0"; + options.LibPaths.Add(@"Foxtrot\Tests\QuickGraph\QuickGraphBinaries\Contracts"); // subdirectory containing contracts. + options.FoxtrotOptions = options.FoxtrotOptions + " /verbose:4"; + TestDriver.RewriteAndVerify(_testOutputHelper, "", @"Foxtrot\Tests\Quickgraph\QuickGraphBinaries\Quickgraph.Data.dll", options); + } + + [Theory] + [MemberData("TestFile")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "V3.5")] + public void BuildRewriteRunFromSourcesV35(int testIndex) + { + Options options = TestFileData.ElementAt(testIndex); + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = "v3.5"; + options.ContractFramework = "v3.5"; + options.UseTestHarness = true; + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory] + [MemberData("TestFile")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "V4.0")] + public void BuildRewriteRunFromSourcesV40(int testIndex) + { + Options options = TestFileData.ElementAt(testIndex); + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = @".NETFramework\v4.0"; + options.ContractFramework = @".NETFramework\v4.0"; + options.UseTestHarness = true; + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory] + [MemberData("TestFile")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "V4.5")] + public void BuildRewriteRunFromSourcesV45(int testIndex) + { + Options options = TestFileData.ElementAt(testIndex); + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = @".NETFramework\v4.5"; + options.ContractFramework = @".NETFramework\v4.0"; + options.UseTestHarness = true; + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory] + [MemberData("RoslynCompatibility")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "V4.5")] + public void BuildRewriteRunRoslynTestCasesWithV45(int testIndex) + { + Options options = RoslynCompatibilityData.ElementAt(testIndex); + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = @".NETFramework\v4.5"; + options.ContractFramework = @".NETFramework\v4.0"; + options.UseTestHarness = true; + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory(Skip = "Old Roslyn bits are not compatible with CCRewrite. Test (and old binaries) should be removed in the next iteration.")] + [MemberData("TestFile")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "Roslyn"), Trait("Category", "V4.5")] + public void BuildRewriteRunFromSourcesRoslynV45(int testIndex) + { + Options options = TestFileData.ElementAt(testIndex); + options.IsLegacyRoslyn = true; + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = @"Roslyn\v4.5"; + options.ReferencesFramework = @".NetFramework\v4.5"; + options.ContractFramework = @".NETFramework\v4.0"; + options.UseTestHarness = true; + + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory] + [MemberData("TestFile")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "V4.0"), Trait("Category", "V3.5")] + public void BuildRewriteRunFromSourcesV40AgainstV35Contracts(int testIndex) + { + Options options = TestFileData.ElementAt(testIndex); + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = @".NETFramework\v4.0"; + options.ContractFramework = @"v3.5"; + options.UseTestHarness = true; + + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + [Theory] + [MemberData("PublicSurfaceOnly")] + [Trait("Category", "Runtime"), Trait("Category", "CoreTest"), Trait("Category", "V4.5")] + public void BuildRewriteFromSources45WithPublicSurfaceOnly(int testIndex) + { + Options options = PublicSurfaceOnlyData.ElementAt(testIndex); + // For testing purposes you can remove /publicsurface and see what happen. Part of the tests should fail! + //options.FoxtrotOptions = options.FoxtrotOptions + String.Format("/throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /publicsurface /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName)); + options.BuildFramework = @".NETFramework\v4.5"; + options.ContractFramework = @".NETFramework\v4.0"; + options.UseTestHarness = true; + + TestDriver.BuildRewriteRun(_testOutputHelper, options); + } + + //private void GrabTestOptions(out string sourceFile, out string options, out string cscoptions, out List refs, out List libs) + //{ + // sourceFile = (string)TestContext.DataRow["Name"]; + // options = (string)TestContext.DataRow["Options"]; + // cscoptions = TestContext.DataRow["CSCOptions"] as string; + // string references = TestContext.DataRow["References"] as string; + // refs = new List(new[] { "System.dll" }); + // if (references != null) + // { + // refs.AddRange(references.Split(';')); + // } + // libs = new List(); + // string libPaths = TestContext.DataRow["Libpaths"] as string; + // if (libPaths != null) + // { + // libs.AddRange(libPaths.Split(';')); + // } + //} + } +} From 3bbeec07210c7aae3833232c5a55a5255f705015 Mon Sep 17 00:00:00 2001 From: Sergey Tepliakov Date: Sat, 24 Oct 2015 18:55:01 -0700 Subject: [PATCH 3/4] Fix for #275. Add additional logic for type comparison to cover generic async methods. --- .../Extraction/AsyncReturnValueQuery.cs | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/Foxtrot/Foxtrot/Extraction/AsyncReturnValueQuery.cs b/Foxtrot/Foxtrot/Extraction/AsyncReturnValueQuery.cs index 6b27e36d..c46168e7 100644 --- a/Foxtrot/Foxtrot/Extraction/AsyncReturnValueQuery.cs +++ b/Foxtrot/Foxtrot/Extraction/AsyncReturnValueQuery.cs @@ -76,8 +76,13 @@ public override void VisitMethodCall(MethodCall call) } } + // For async methods calledMethod (Contract.Result) would be called in the generated generic state machine, + // and calledMethod.ReturnType would be generic type argument and actualResultType can be generic method argument + // (if async postcondition declared in the generic method from non-generic class). + // In this case calledMethod.ReturnType would be != this.actualResultType + // and different comparison logic should be used (reflected in EquivalentGenercTypes method). if (this.actualResultType != null && contractNodes.IsResultMethod(template) && - calledMethod.ReturnType == this.actualResultType) + (calledMethod.ReturnType == this.actualResultType || EquivalentGenericTypes(calledMethod, actualResultType))) { // using Contract.Result() in a Task returning method, this is a shorthand for // Contract.Result>().Result @@ -87,5 +92,17 @@ public override void VisitMethodCall(MethodCall call) base.VisitMethodCall(call); } + + private static bool EquivalentGenericTypes(Method calledMethod, TypeNode actualResultType) + { + if (calledMethod.IsGeneric && actualResultType.IsTemplateParameter) + { + // Relatively naive implementation for equality, but still correct + // and should not lead to false positives. + return calledMethod.ReturnType.FullName == actualResultType.FullName; + } + + return false; + } } } \ No newline at end of file From 2163f151f2fca39cd4ac20f6b48b2ab941607cad Mon Sep 17 00:00:00 2001 From: Sergey Tepliakov Date: Fri, 22 Jan 2016 17:13:07 -0800 Subject: [PATCH 4/4] Address code review comments. --- Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs | 75 +++++++++++++------ .../AsyncPostconditionInGenericClass3.cs | 51 +++++++++++++ .../AsyncPostconditionInGenericMethod4.cs | 61 +++++++++++++++ .../RewriterTests/AsyncTestsDataSource.cs | 2 + 4 files changed, 168 insertions(+), 21 deletions(-) create mode 100644 Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass3.cs create mode 100644 Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod4.cs diff --git a/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs b/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs index 46ceeaaf..d5986e82 100644 --- a/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs +++ b/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs @@ -59,20 +59,20 @@ namespace Microsoft.Contracts.Foxtrot internal class EmitAsyncClosure : StandardVisitor { /// - /// Class that maps generic arguments of the enclosed class/method the generic arguments of the closure. + /// Class that maps generic arguments of the enclosed class/method to the generic arguments of the closure. /// /// /// The problem. /// Original implementation of the Code Contract didn't support async postconditions in generics. /// Here is why: - /// Suppose we have following function (in class Foo: + /// Suppose we have following function (in class Foo: /// FooAsync() where T: class /// { /// Contract.Ensures(Contract.Result() != null); /// } /// ]]> - /// In this case, ccrewrite will generate async closure class called Foo.AsyncContractClosure_0<T%gt; + /// In this case, ccrewrite will generate async closure class called Foo.AsyncContractClosure_0<T> /// with following structure: /// t.EnclosingGenericType == enclosingType); return candidate != null ? candidate.ClosureGenericType : enclosingType; } @@ -161,7 +167,7 @@ public TypeNode GetClosureTypeParameterByEnclosingTypeParameter(TypeNode enclosi /// /// Function returns the same argument if the matching argument does not exists. /// - public TypeNode GetEnclosingTypeParamterByGenericTypeParameter(TypeNode closureType) + public TypeNode GetEnclosingTypeParameterByClosureTypeParameter(TypeNode closureType) { if (closureType == null) { @@ -250,22 +256,7 @@ public EmitAsyncClosure(Method from, Rewriter rewriter) // Should distinguish between generic enclosing method and non-generic method in enclosing type. // In both cases generated closure should be generic. - Func getGenericTypesFrom = method => - { - if (method.IsGeneric) - { - return from.TemplateParameters; - } - - if (method.DeclaringType.IsGeneric) - { - return method.DeclaringType.TemplateParameters; - } - - return null; - }; - - var enclosingTemplateParameters = getGenericTypesFrom(from); + var enclosingTemplateParameters = GetGenericTypesFrom(from); if (!enclosingTemplateParameters.IsNullOrEmpty()) { @@ -402,6 +393,36 @@ private InstanceInitializer Ctor get { return (InstanceInitializer)this.closureClassInstance.GetMembersNamed(StandardIds.Ctor)[0]; } } + private static TypeNodeList GetGenericTypesFrom(Method method) + { + if (method.IsGeneric) + { + return method.TemplateParameters; + } + + if (method.DeclaringType.IsGeneric) + { + return GetFirstNonEmptyGenericListWalkingUpDeclaringTypes(method.DeclaringType); + } + + return null; + } + + private static TypeNodeList GetFirstNonEmptyGenericListWalkingUpDeclaringTypes(TypeNode node) + { + if (node == null) + { + return null; + } + + if (node.TemplateParameters != null && node.TemplateParameters.Count != 0) + { + return node.TemplateParameters; + } + + return GetFirstNonEmptyGenericListWalkingUpDeclaringTypes(node.DeclaringType); + } + [Pure] private static TypeNodeList CreateTemplateParameters(Class closureClass, TypeNodeList inputTemplateParameters, TypeNode declaringType) { @@ -745,6 +766,18 @@ public TypeParameterFixerVisitor(GenericTypeMapper genericParametersMapping) this.genericParametersMapping = genericParametersMapping; } + public override Expression VisitAddressDereference(AddressDereference addr) + { + // Replacing initobj !!0 to initobj !0 + var newType = genericParametersMapping.GetClosureTypeParameterByEnclosingTypeParameter(addr.Type); + if (newType != addr.Type) + { + return new AddressDereference(addr.Address, newType, addr.Volatile, addr.Alignment, addr.SourceContext); + } + + return base.VisitAddressDereference(addr); + } + // Literal is used when contract result compares to null: Contract.Result() != null public override Expression VisitLiteral(Literal literal) { @@ -846,7 +879,7 @@ private Member GetUnwrapMethod(TypeNode checkMethodTaskType) // and use !!0 (reference to method template arg) instead of using !0 (which is reference // to closure class template arg). var enclosingGeneritType = - this.genericTypeMapper.GetEnclosingTypeParamterByGenericTypeParameter( + this.genericTypeMapper.GetEnclosingTypeParameterByClosureTypeParameter( checkMethodTaskType.TemplateArguments[0]); return genericUnwrapCandidate.GetTemplateInstance(null, enclosingGeneritType); diff --git a/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass3.cs b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass3.cs new file mode 100644 index 00000000..5b4fadb6 --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericClass3.cs @@ -0,0 +1,51 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + +public class Outer { + public class Inner { + public static Task OuterClassTypeArgument(T obj) { + Contract.Ensures(Contract.Result() != null); + return Task.FromResult(obj); + } + } +} + + partial class TestMain + { + partial void Run() + { + if (behave) + { + Outer.Inner.OuterClassTypeArgument("foo").Wait(); + } + else + { + Outer.Inner.OuterClassTypeArgument(null).Wait(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Postcondition; + public string NegativeExpectedCondition = "Contract.Result() != null"; + } +} diff --git a/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod4.cs b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod4.cs new file mode 100644 index 00000000..00c4c2fe --- /dev/null +++ b/Foxtrot/Tests/AsyncPostconditions/AsyncPostconditionInGenericMethod4.cs @@ -0,0 +1,61 @@ +// CodeContracts +// +// Copyright (c) Microsoft Corporation +// +// All rights reserved. +// +// MIT License +// +// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +using System; +using System.Collections.Generic; +using System.Text; +using System.Diagnostics.Contracts; +using System.Threading; + +namespace Tests.Sources +{ + using System.Threading.Tasks; + + class FooClass + { + public static async Task Foo(T obj) { + // Does not throw when null is used instead of default(T) + Contract.Ensures(!object.Equals(Contract.Result(), default(T))); + await Task.Delay(42); + return obj; + } + } + + class BooClass + { + public static Task Foo(T obj) { + // Does not throw when null is used instead of default(T) + Contract.Ensures(!object.Equals(Contract.Result(), default(T))); + return Task.FromResult(obj); + } + } + + partial class TestMain + { + partial void Run() + { + if (behave) + { + FooClass.Foo("foo").Wait(); + } + else + { + FooClass.Foo(null).Wait(); + } + } + + public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Postcondition; + public string NegativeExpectedCondition = "!object.Equals(Contract.Result(), default(T))"; + } +} diff --git a/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs b/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs index e4d63be8..d5b48646 100644 --- a/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs +++ b/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs @@ -49,10 +49,12 @@ public static IEnumerable AsyncPostconditionsTestCases { @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericClass.cs", @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericClass2.cs", + @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericClass3.cs", @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericMethod.cs", @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericMethod2.cs", @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericMethod3.cs", + @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericMethod4.cs", @"Foxtrot\Tests\AsyncPostconditions\AsyncPostconditionInGenericMethodInStruct.cs",