diff --git a/Foxtrot/Foxtrot/Extraction/ExtractorVisitor.cs b/Foxtrot/Foxtrot/Extraction/ExtractorVisitor.cs
index b49ee7fa..e518a703 100644
--- a/Foxtrot/Foxtrot/Extraction/ExtractorVisitor.cs
+++ b/Foxtrot/Foxtrot/Extraction/ExtractorVisitor.cs
@@ -2256,6 +2256,18 @@ private static int ContractStartInMoveNext(ContractNodes contractNodes, Method m
goto OuterLoop;
}
+ // Roslyn-based compiler introduced new pattern for async methods with 2 await statements.
+ // Current implementation sets seenFinalCompare to true when `if (num != 0)` code was found in the MoveNext method.
+ // This usually meant that async preamble is finished and next statement could be a contract statement
+ // (or legacy contract statement, doesn't matter).
+ // But VS2015 compiler changes the behavior and right after `if (num != 0)` there another check that should be skipped.
+ // Please see additional comments at IsRoslynStateCheckForSecondFinishedAwaiter
+ if (seenFinalCompare && isAsync && IsRoslynStateCheckForSecondFinishedAwaiter(branch.Condition, env, ignoreUnknown: true))
+ {
+ // just skipping current statement!
+ continue;
+ }
+
var value = EvaluateExpression(branch.Condition, env, seenFinalCompare, isAsync);
if (value.Two == EvalKind.IsDisposingTest)
{
@@ -2263,13 +2275,13 @@ private static int ContractStartInMoveNext(ContractNodes contractNodes, Method m
{
return FindTargetBlock(blocks, branch.Target, currentBlockIndex);
}
-
+
if (i + 1 < block.Statements.Count)
{
statementIndex = i + 1;
return currentBlockIndex;
}
-
+
if (currentBlockIndex + 1 < body.Statements.Count)
{
return currentBlockIndex + 1;
@@ -2292,7 +2304,7 @@ private static int ContractStartInMoveNext(ContractNodes contractNodes, Method m
currentBlockIndex = FindTargetBlock(blocks, branch.Target, currentBlockIndex);
goto OuterLoop;
}
-
+
continue;
}
@@ -2461,6 +2473,57 @@ private static bool IsDoFinallyBodies(Expression expression)
return false;
}
+ ///
+ /// Roslyn-based compiler introduces different pattern for async method with two await statements:
+ /// Instead of using switch (as it does for 2+ awaits) it generates following code:
+ ///
+ /// if (num != 0)
+ /// {
+ /// if (num == 1) // <-- this if-statement should be processed differently!
+ /// {
+ /// taskAwaiter = this.<>u__1;
+ /// this.<>u__1 = default(TaskAwaiter);
+ /// this.<>1__state = -1;
+ /// goto IL_E8;
+ /// }
+ /// Contract.Requires(this.str != null);
+ /// taskAwaiter2 = Task.Delay(42).GetAwaiter();
+ /// if (!taskAwaiter2.IsCompleted)
+ /// {
+ /// this.<>1__state = 0;
+ /// this.<>u__1 = taskAwaiter2;
+ /// Foo.<Method2>d__0 <Method2>d__ = this;
+ /// this.<>t__builder.AwaitUnsafeOnCompleted<TaskAwaiter, Foo.<Method2>d__0>(ref taskAwaiter2, ref <Method2>d__);
+ /// return;
+ /// }
+ /// }
+ /// else
+ /// {
+ /// taskAwaiter2 = this.<>u__1;
+ /// this.<>u__1 = default(TaskAwaiter);
+ /// this.<>1__state = -1;
+ /// }
+ ///
+ /// Unfortunately, `if (num != 0)` was always used to detect that upcoming statement is a contract statement.
+ /// That's why after migration to VS2015 ccrewrite was failing trying to compile a method with two awaits.
+ ///
+ /// Current method helps to distinguish this new pattern and returns true for binary expression that checks state variable with 1.
+ ///
+ private static bool IsRoslynStateCheckForSecondFinishedAwaiter(Expression expression, Dictionary> env, bool ignoreUnknown)
+ {
+ var binary = expression as BinaryExpression;
+ if (binary != null)
+ {
+ var op1 = EvaluateExpression(binary.Operand1, env, ignoreUnknown, ignoreUnknown);
+ var op2 = EvaluateExpression(binary.Operand2, env, ignoreUnknown, ignoreUnknown);
+
+ // Checking is it "num == 1" statement that will present in Roslyn-based async method with exactly 2 await expressions.
+ return binary.NodeType == NodeType.Eq && op1.Two == EvalKind.IsStateValue && op2.One == 1;
+ }
+
+ return false;
+ }
+
[ContractVerification(true)]
private static Pair EvaluateExpression(Expression expression,
Dictionary> env, bool ignoreUnknown, bool isAsync)
diff --git a/Foxtrot/Tests/RewriterTests.cs b/Foxtrot/Tests/RewriterTests.cs
index 667a7ba2..5335732c 100644
--- a/Foxtrot/Tests/RewriterTests.cs
+++ b/Foxtrot/Tests/RewriterTests.cs
@@ -228,6 +228,19 @@ public void BuildRewriteRunFromSourcesV45()
TestDriver.BuildRewriteRun(options);
}
+ [DeploymentItem("Foxtrot\\Tests\\TestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\TestInputs.xml", "RoslynCompatibility", DataAccessMethod.Sequential)]
+ [TestMethod]
+ [TestCategory("Runtime"), TestCategory("CoreTest"), TestCategory("V4.5")]
+ public void BuildRewriteRunRoslynTestCasesWithV45()
+ {
+ var options = new Options(this.TestContext);
+ 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(options);
+ }
+
[DeploymentItem("Foxtrot\\Tests\\TestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\TestInputs.xml", "TestFile", DataAccessMethod.Sequential)]
[TestMethod]
[TestCategory("Runtime"), TestCategory("CoreTest"), TestCategory("Roslyn"), TestCategory("V4.5")]
diff --git a/Foxtrot/Tests/RoslynCompatibility/AbbrevGenClosure.cs b/Foxtrot/Tests/RoslynCompatibility/AbbrevGenClosure.cs
index 8c3183a0..41299adf 100644
--- a/Foxtrot/Tests/RoslynCompatibility/AbbrevGenClosure.cs
+++ b/Foxtrot/Tests/RoslynCompatibility/AbbrevGenClosure.cs
@@ -52,16 +52,6 @@ public static void MustReturnCollectionWithoutNullItem()
Contract.Ensures(Contract.ForAll(Contract.Result>(), item => item != null));
}
- public string[] GetSubscribers2(bool behave)
- {
- MustReturnCollectionWithoutNullItem();
-
- if (behave) {
- return new string[]{"a","B","c"};
- }
- return null;
- }
-
}
partial class TestMain
diff --git a/Foxtrot/Tests/RoslynCompatibility/AsyncRequiresWithMultipleAwaits.cs b/Foxtrot/Tests/RoslynCompatibility/AsyncRequiresWithMultipleAwaits.cs
new file mode 100644
index 00000000..41c03842
--- /dev/null
+++ b/Foxtrot/Tests/RoslynCompatibility/AsyncRequiresWithMultipleAwaits.cs
@@ -0,0 +1,68 @@
+// 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.Diagnostics.Contracts;
+using System.Text;
+using System.Threading.Tasks;
+
+namespace Tests.Sources
+{
+ public class Foo
+ {
+ public async Task Method1(string str)
+ {
+ Contract.Requires(str != null);
+ await Task.Delay(42);
+ }
+
+ public async Task Method2(string str)
+ {
+ // This code lead to failure previously!
+ Contract.Requires(str != null);
+
+ await Task.Delay(42);
+ await Task.Delay(43);
+ }
+
+ public async Task Method5(string str)
+ {
+ Contract.Requires(str != null);
+ await Task.Delay(42);
+ await Task.Delay(42);
+ await Task.Delay(42);
+ await Task.Delay(42);
+ await Task.Delay(42);
+ }
+ }
+
+ partial class TestMain
+ {
+ partial void Run()
+ {
+ if (behave)
+ {
+ new Foo().Method2("1");
+ }
+ else
+ {
+ new Foo().Method2(null);
+ }
+ }
+
+ public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Precondition;
+ public string NegativeExpectedCondition = "str != null";
+ }
+}
diff --git a/Foxtrot/Tests/RoslynCompatibility/AsyncWithLegacyRequires.cs b/Foxtrot/Tests/RoslynCompatibility/AsyncWithLegacyRequires.cs
new file mode 100644
index 00000000..a04c6553
--- /dev/null
+++ b/Foxtrot/Tests/RoslynCompatibility/AsyncWithLegacyRequires.cs
@@ -0,0 +1,74 @@
+// 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.Diagnostics.Contracts;
+using System.Text;
+using System.Threading.Tasks;
+
+namespace Tests.Sources
+{
+ public class Foo
+ {
+ public async Task Method1(string str)
+ {
+ if (str == null) throw new ArgumentNullException("str");
+ Contract.EndContractBlock();
+
+ await Task.Delay(42);
+ }
+
+ public async Task Method2(string str)
+ {
+ // This code lead to failure previously!
+ if (str == null) throw new ArgumentNullException("str");
+ Contract.EndContractBlock();
+
+ await Task.Delay(42);
+ await Task.Delay(43);
+ }
+
+ public async Task Method5(string str)
+ {
+ if (str == null) throw new ArgumentNullException("str");
+ Contract.EndContractBlock();
+
+ await Task.Delay(42);
+ await Task.Delay(42);
+ await Task.Delay(42);
+ await Task.Delay(42);
+ await Task.Delay(42);
+ }
+
+ }
+
+ partial class TestMain
+ {
+ partial void Run()
+ {
+ if (behave)
+ {
+ new Foo().Method2("1");
+ }
+ else
+ {
+ new Foo().Method2(null);
+ }
+ }
+
+ public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Precondition;
+ public string NegativeExpectedCondition = "Value cannot be null.\r\nParameter name: str";
+ }
+}
diff --git a/Foxtrot/Tests/Sources/ComplexGeneric.cs b/Foxtrot/Tests/Sources/ComplexGeneric.cs
index 54717cba..1dbaf1f2 100644
--- a/Foxtrot/Tests/Sources/ComplexGeneric.cs
+++ b/Foxtrot/Tests/Sources/ComplexGeneric.cs
@@ -24,6 +24,24 @@
namespace Tests.Sources
{
+// This bug was relevant only for .NET 4.0+
+#if NETFRAMEWORK_3_5
+
+ partial class TestMain
+ {
+ partial void Run()
+ {
+ if (!this.behave)
+ {
+ throw new System.ArgumentNullException();
+ }
+ }
+
+ public ContractFailureKind NegativeExpectedKind = ContractFailureKind.Precondition;
+ public string NegativeExpectedCondition = "Value cannot be null.";
+ }
+
+#else
// CCRewriter was unable to read this code from the IL due to an issue in CCI.
// This test just makes sure that the fix is in place.
@@ -65,4 +83,6 @@ partial void Run()
public string NegativeExpectedCondition = "Value cannot be null.";
}
+#endif
+
}
diff --git a/Foxtrot/Tests/Sources/TestHarness.cs b/Foxtrot/Tests/Sources/TestHarness.cs
index edf1b1e3..a2040d62 100644
--- a/Foxtrot/Tests/Sources/TestHarness.cs
+++ b/Foxtrot/Tests/Sources/TestHarness.cs
@@ -98,7 +98,7 @@ class Assert
public static void AreEqual(object expected, object actual)
{
if (object.Equals(expected, actual)) return;
- var result = String.Format("Expected: {0}, Actual: {1}", expected, actual);
+ var result = String.Format("Expected: '{0}', Actual: '{1}'", expected, actual);
Console.WriteLine(result);
throw new Exception(result);
}
diff --git a/Foxtrot/Tests/TestInputs.xml b/Foxtrot/Tests/TestInputs.xml
index 2eb5c6c7..9bb29291 100644
--- a/Foxtrot/Tests/TestInputs.xml
+++ b/Foxtrot/Tests/TestInputs.xml
@@ -11,6 +11,24 @@
/>
+
+
+
+
+