diff --git a/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs b/Foxtrot/Driver/Rewriting/EmitAsyncClosure.cs index 02c11e9f..71effdbe 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,127 @@ namespace Microsoft.Contracts.Foxtrot /// internal class EmitAsyncClosure : StandardVisitor { + /// + /// 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: + /// FooAsync() where T: class + /// { + /// Contract.Ensures(Contract.Result() != null); + /// } + /// ]]> + /// In this case, ccrewrite will generate async closure class called Foo.AsyncContractClosure_0<T> + /// 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 gen = enclosingType; + if (gen.ConsolidatedTemplateParameters != null && gen.ConsolidatedTemplateParameters.Count != 0) + { + gen = gen.ConsolidatedTemplateParameters[0]; + } + + 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 GetEnclosingTypeParameterByClosureTypeParameter(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 +212,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 +254,30 @@ 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. + 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 +311,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 +330,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 +351,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 +392,54 @@ 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, 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); @@ -448,6 +612,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 @@ -463,6 +636,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); @@ -506,7 +684,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. @@ -574,6 +755,83 @@ 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; + } + + 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) + { + 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)); @@ -588,7 +846,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); @@ -616,7 +874,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.GetEnclosingTypeParameterByClosureTypeParameter( + 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 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 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/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/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/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/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 110f0c79..f1e34765 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 302aaf8d..559a19b8 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; @@ -282,6 +283,23 @@ public Options( { } + 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; } public bool Optimize { get; set; } diff --git a/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs b/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs new file mode 100644 index 00000000..d5b48646 --- /dev/null +++ b/Foxtrot/Tests/RewriterTests/AsyncTestsDataSource.cs @@ -0,0 +1,75 @@ +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\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", + + @"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(';')); + // } + //} + } +}