From 6df0a29732253b64fb6018ed53866950a76e500d Mon Sep 17 00:00:00 2001 From: Chris Lovett Date: Tue, 11 Aug 2020 19:19:55 +0000 Subject: [PATCH] Merged PR 2892: Rewrite try/catch blocks to add when (!(ex is ExecutionCanceledException)) Still lots of work to be done, but so far it can report catch blocks that need to be rewritten. Related work items: #4620 --- Scripts/run-tests.ps1 | 7 + Source/Core/IO/ErrorReporter.cs | 3 +- Source/Core/IO/Logging/ConsoleLogger.cs | 24 ++ Source/Core/Properties/InternalsVisibleTo.cs | 6 + .../Interception/ExceptionHandlers.cs | 41 +++ Source/Test/Rewriting/AssemblyRewriter.cs | 40 +- .../Transforms/ExceptionFilterTransform.cs | 132 +++++++ .../Rewriting/Transforms/MonitorTransform.cs | 10 + .../Rewriting/Transforms/TaskTransform.cs | 8 +- .../Tasks/TaskExceptionFilterTests.cs | 343 ++++++++++++++++++ .../Tasks/Locks/AsyncLockTests.cs | 6 + 11 files changed, 607 insertions(+), 13 deletions(-) create mode 100644 Source/Core/SystematicTesting/Interception/ExceptionHandlers.cs create mode 100644 Source/Test/Rewriting/Transforms/ExceptionFilterTransform.cs create mode 100644 Tests/BinaryRewriting.Tests/Tasks/TaskExceptionFilterTests.cs diff --git a/Scripts/run-tests.ps1 b/Scripts/run-tests.ps1 index 9413331e..a40966a6 100644 --- a/Scripts/run-tests.ps1 +++ b/Scripts/run-tests.ps1 @@ -57,6 +57,13 @@ foreach ($kvp in $targets.GetEnumerator()) { # now run the rewritten test. $target = "$PSScriptRoot/../Tests/$($kvp.Value)/$($kvp.Value).csproj" Invoke-DotnetTest -dotnet $dotnet -project $($kvp.Name) -target $target -filter $filter -logger $logger -framework $f -verbosity $v + + # test that we can also rewrite a rewritten assembly and do no damage! + Rewrite -framework $f -target $target_file -keyFile $key_file + + # now run the rewritten test again. + $target = "$PSScriptRoot/../Tests/$($kvp.Value)/$($kvp.Value).csproj" + Invoke-DotnetTest -dotnet $dotnet -project $($kvp.Name) -target $target -filter $filter -logger $logger -framework $f -verbosity $v } } } diff --git a/Source/Core/IO/ErrorReporter.cs b/Source/Core/IO/ErrorReporter.cs index fd05fb88..ddba89ae 100644 --- a/Source/Core/IO/ErrorReporter.cs +++ b/Source/Core/IO/ErrorReporter.cs @@ -35,8 +35,7 @@ namespace Microsoft.Coyote.IO /// public void WriteErrorLine(string value) { - this.Write("Error: ", ConsoleColor.Red); - this.Write(value, ConsoleColor.Yellow); + this.Write("Error: " + value, ConsoleColor.Red); this.Logger.WriteLine(string.Empty); } diff --git a/Source/Core/IO/Logging/ConsoleLogger.cs b/Source/Core/IO/Logging/ConsoleLogger.cs index c74b05fa..8be2d246 100644 --- a/Source/Core/IO/Logging/ConsoleLogger.cs +++ b/Source/Core/IO/Logging/ConsoleLogger.cs @@ -53,5 +53,29 @@ namespace Microsoft.Coyote.IO { Console.WriteLine(value); } + + /// + /// Reports an error, followed by the current line terminator. + /// + /// The string to write. +#pragma warning disable CA1822 // Mark members as static + public void WriteErrorLine(string value) +#pragma warning restore CA1822 // Mark members as static + { + Error.Write(Console.Out, ConsoleColor.Red, value); + Console.WriteLine(); + } + + /// + /// Reports an warning, followed by the current line terminator. + /// + /// The string to write. +#pragma warning disable CA1822 // Mark members as static + public void WriteWarningLine(string value) +#pragma warning restore CA1822 // Mark members as static + { + Error.Write(Console.Out, ConsoleColor.Yellow, value); + Console.WriteLine(); + } } } diff --git a/Source/Core/Properties/InternalsVisibleTo.cs b/Source/Core/Properties/InternalsVisibleTo.cs index 32c781e1..997b90f5 100644 --- a/Source/Core/Properties/InternalsVisibleTo.cs +++ b/Source/Core/Properties/InternalsVisibleTo.cs @@ -44,6 +44,12 @@ using System.Runtime.CompilerServices; "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" + "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" + "3bc97f9e")] +[assembly: InternalsVisibleTo("Microsoft.Coyote.BinaryRewriting.Tests,PublicKey=" + + "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" + + "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" + + "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" + + "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" + + "3bc97f9e")] [assembly: InternalsVisibleTo("Microsoft.Coyote.Performance.Tests,PublicKey=" + "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" + "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" + diff --git a/Source/Core/SystematicTesting/Interception/ExceptionHandlers.cs b/Source/Core/SystematicTesting/Interception/ExceptionHandlers.cs new file mode 100644 index 00000000..ca63642e --- /dev/null +++ b/Source/Core/SystematicTesting/Interception/ExceptionHandlers.cs @@ -0,0 +1,41 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.ComponentModel; +using Microsoft.Coyote.IO; + +namespace Microsoft.Coyote.SystematicTesting.Interception +{ + /// + /// Provides a set of static methods for working with specific kinds of instances. + /// + /// This type is intended for compiler use rather than use directly in code. + [EditorBrowsable(EditorBrowsableState.Never)] + public static class ExceptionHandlers + { + /// + /// Checks if the exception object contains a ExecutionCanceledException, and if so + /// it throws it so that the exception is not silently handled by customer code. + /// The Coyote runtime needs to get this exception as a way to cancel the current + /// test iteration. + /// + /// The exception object. + public static void ThrowIfCoyoteRuntimeException(object e) + { + if (e is ExecutionCanceledException exe) + { + throw exe; + } + + if (e is Exception ex) + { + // Look inside in case this is some sort of auto-wrapped AggregateException. + if (ex.InnerException != null) + { + ThrowIfCoyoteRuntimeException(ex.InnerException); + } + } + } + } +} diff --git a/Source/Test/Rewriting/AssemblyRewriter.cs b/Source/Test/Rewriting/AssemblyRewriter.cs index e245b63e..31212d53 100644 --- a/Source/Test/Rewriting/AssemblyRewriter.cs +++ b/Source/Test/Rewriting/AssemblyRewriter.cs @@ -42,6 +42,11 @@ namespace Microsoft.Coyote.Rewriting /// private readonly List Transforms; + /// + /// The output log. + /// + private readonly ConsoleLogger Log = new ConsoleLogger(); + /// /// Initializes a new instance of the class. /// @@ -59,8 +64,9 @@ namespace Microsoft.Coyote.Rewriting this.Transforms = new List() { - new TaskTransform(), - new MonitorTransform() + new TaskTransform(this.Log), + new MonitorTransform(this.Log), + new ExceptionFilterTransform(this.Log) }; } @@ -81,13 +87,22 @@ namespace Microsoft.Coyote.Rewriting // Create the output directory and copy any necessery files. string outputDirectory = this.CreateOutputDirectoryAndCopyFiles(); + int errors = 0; // Rewrite the assembly files to the output directory. foreach (string assemblyPath in this.Configuration.AssemblyPaths) { - this.RewriteAssembly(assemblyPath, outputDirectory); + try + { + this.RewriteAssembly(assemblyPath, outputDirectory); + } + catch (Exception ex) + { + this.Log.WriteErrorLine(ex.Message); + errors++; + } } - if (this.Configuration.IsReplacingAssemblies) + if (errors == 0 && this.Configuration.IsReplacingAssemblies) { // If we are replacing the original assemblies, then delete the temporary output directory. Directory.Delete(outputDirectory, true); @@ -112,7 +127,7 @@ namespace Microsoft.Coyote.Rewriting throw new InvalidOperationException($"Rewriting the '{assemblyName}' assembly ({assembly.FullName}) is not allowed."); } - Console.WriteLine($"... Rewriting the '{assemblyName}' assembly ({assembly.FullName})"); + this.Log.WriteLine($"... Rewriting the '{assemblyName}' assembly ({assembly.FullName})"); foreach (var transform in this.Transforms) { // Traverse the assembly to apply each transformation pass. @@ -125,7 +140,7 @@ namespace Microsoft.Coyote.Rewriting // Write the binary in the output path with portable symbols enabled. string outputPath = Path.Combine(outputDirectory, assemblyName); - Console.WriteLine($"... Writing the modified '{assemblyName}' assembly to " + + this.Log.WriteLine($"... Writing the modified '{assemblyName}' assembly to " + $"{(this.Configuration.IsReplacingAssemblies ? assemblyPath : outputPath)}"); var writeParams = new WriterParameters() @@ -195,6 +210,11 @@ namespace Microsoft.Coyote.Rewriting /// private static void RewriteMethod(MethodDefinition method, AssemblyTransform transform) { + if (method.Body == null) + { + return; + } + Debug.WriteLine($"........... Method {method.FullName}"); transform.VisitMethod(method); @@ -239,7 +259,7 @@ namespace Microsoft.Coyote.Rewriting if (!this.Configuration.IsReplacingAssemblies) { - Console.WriteLine($"... Copying all files to the '{outputDirectory}' directory"); + this.Log.WriteLine($"... Copying all files to the '{outputDirectory}' directory"); // Copy all files to the output directory, while preserving directory structure. foreach (string directoryPath in Directory.GetDirectories(sourceDirectory, "*", SearchOption.AllDirectories)) @@ -283,7 +303,7 @@ namespace Microsoft.Coyote.Rewriting assemblyResolver.AddSearchDirectory(this.Configuration.AssembliesDirectory); // Add the assembly resolution error handler. - assemblyResolver.ResolveFailure += OnResolveAssemblyFailure; + assemblyResolver.ResolveFailure += this.OnResolveAssemblyFailure; return assemblyResolver; } @@ -296,9 +316,9 @@ namespace Microsoft.Coyote.Rewriting /// /// Handles an assembly resolution error. /// - private static AssemblyDefinition OnResolveAssemblyFailure(object sender, AssemblyNameReference reference) + private AssemblyDefinition OnResolveAssemblyFailure(object sender, AssemblyNameReference reference) { - Console.WriteLine("Error resolving assembly: " + reference.FullName); + this.Log.WriteErrorLine("Error resolving assembly: " + reference.FullName); return null; } } diff --git a/Source/Test/Rewriting/Transforms/ExceptionFilterTransform.cs b/Source/Test/Rewriting/Transforms/ExceptionFilterTransform.cs new file mode 100644 index 00000000..dbec738d --- /dev/null +++ b/Source/Test/Rewriting/Transforms/ExceptionFilterTransform.cs @@ -0,0 +1,132 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Coyote.IO; +using Mono.Cecil; +using Mono.Cecil.Cil; + +namespace Microsoft.Coyote.Rewriting +{ + internal class ExceptionFilterTransform : AssemblyTransform + { + /// + /// Console output writer. + /// + private readonly ConsoleLogger Log; + + /// + /// The type being transformed. + /// + private TypeDefinition TypeDef; + + /// + /// Is part of an async state machine. + /// + private bool IsStateMachine; + + /// + /// The current method being transformed. + /// + private MethodDefinition Method; + + internal ExceptionFilterTransform(ConsoleLogger log) + { + this.Log = log; + } + + /// + internal override void VisitType(TypeDefinition typeDef) + { + this.TypeDef = typeDef; + this.IsStateMachine = (from i in typeDef.Interfaces where i.InterfaceType.FullName == "System.Runtime.CompilerServices.IAsyncStateMachine" select i).Any(); + } + + /// + internal override void VisitMethod(MethodDefinition method) + { + this.Method = method; + } + + /// + internal override void VisitExceptionHandler(ExceptionHandler handler) + { + if (this.IsStateMachine) + { + // these have try catch blocks that forward the caught exception over to the AsyncTaskMethodBuilder.SetException + // and these are ok, Coyote knows about this. + return; + } + + // Trivial case, if the exception handler is just a rethrow! + var handlerInstruction = GetHandlerInstructions(handler); + if (handlerInstruction.Count == 2 && handlerInstruction[0].OpCode.Code == Code.Pop && + handlerInstruction[1].OpCode.Code == Code.Rethrow) + { + // ok then, doesn't matter what the filter is doing since it is just rethrowing anyway. + return; + } + + if (handler.FilterStart == null) + { + if (handler.CatchType == null) + { + // then this is a finally block, which is ok... + return; + } + + var name = handler.CatchType.FullName; + if (name == "System.Object" || name == "System.Exception" || name == "Microsoft.Coyote.RuntimeException") + { + this.AddThrowIfExecutionCanceledException(handler); + } + } + else + { + // Oh, it has a filter, then we don't care what it is we can insert a check for + // ExecutionCanceledException at the top of this handler. + this.AddThrowIfExecutionCanceledException(handler); + } + } + + private void AddThrowIfExecutionCanceledException(ExceptionHandler handler) + { + Debug.WriteLine($"............. [+] inserting ExecutionCanceledException check into existing handler."); + + var handlerType = this.Method.Module.ImportReference(typeof(Microsoft.Coyote.SystematicTesting.Interception.ExceptionHandlers)).Resolve(); + MethodReference handlerMethod = (from m in handlerType.Methods where m.Name == "ThrowIfCoyoteRuntimeException" select m).FirstOrDefault(); + handlerMethod = this.Method.Module.ImportReference(handlerMethod); + + var processor = this.Method.Body.GetILProcessor(); + var newStart = Instruction.Create(OpCodes.Dup); + processor.InsertBefore(handler.HandlerStart, newStart); + processor.InsertBefore(handler.HandlerStart, Instruction.Create(OpCodes.Call, handlerMethod)); + handler.HandlerStart = newStart; + if (handler.FilterStart == null) + { + handler.TryEnd = handler.HandlerStart; + } + } + + private static List GetHandlerInstructions(ExceptionHandler handler) + { + if (handler.HandlerStart == null) + { + return null; + } + + List result = new List(); + for (var i = handler.HandlerStart; i != handler.HandlerEnd; i = i.Next) + { + if (i.OpCode.Code != Code.Nop) + { + result.Add(i); + } + } + + return result; + } + } +} diff --git a/Source/Test/Rewriting/Transforms/MonitorTransform.cs b/Source/Test/Rewriting/Transforms/MonitorTransform.cs index ac08a3e1..12d43b15 100644 --- a/Source/Test/Rewriting/Transforms/MonitorTransform.cs +++ b/Source/Test/Rewriting/Transforms/MonitorTransform.cs @@ -37,6 +37,16 @@ namespace Microsoft.Coyote.Rewriting private const string MonitorClassName = "System.Threading.Monitor"; + /// + /// Console output writer. + /// + private readonly ConsoleLogger Log; + + internal MonitorTransform(ConsoleLogger log) + { + this.Log = log; + } + /// internal override void VisitModule(ModuleDefinition module) { diff --git a/Source/Test/Rewriting/Transforms/TaskTransform.cs b/Source/Test/Rewriting/Transforms/TaskTransform.cs index 0ff4040d..57385538 100644 --- a/Source/Test/Rewriting/Transforms/TaskTransform.cs +++ b/Source/Test/Rewriting/Transforms/TaskTransform.cs @@ -42,11 +42,17 @@ namespace Microsoft.Coyote.Rewriting /// private ILProcessor Processor; + /// + /// Console output writer. + /// + private readonly ConsoleLogger Log; + /// /// Initializes a new instance of the class. /// - internal TaskTransform() + internal TaskTransform(ConsoleLogger log) { + this.Log = log; this.RewrittenMethodCache = new Dictionary(); } diff --git a/Tests/BinaryRewriting.Tests/Tasks/TaskExceptionFilterTests.cs b/Tests/BinaryRewriting.Tests/Tasks/TaskExceptionFilterTests.cs new file mode 100644 index 00000000..78fe3bd5 --- /dev/null +++ b/Tests/BinaryRewriting.Tests/Tasks/TaskExceptionFilterTests.cs @@ -0,0 +1,343 @@ +// Copyright (c) Microsoft Corporation. +// Licensed under the MIT License. + +using System; +using System.Diagnostics; +using Microsoft.Coyote.Tasks; +using Xunit; +using Xunit.Abstractions; + +namespace Microsoft.Coyote.BinaryRewriting.Tests.Tasks +{ + /// + /// Tests that we can insert ExecutionCanceledException filter. + /// + public class TaskExceptionFilterTests : BaseProductionTest + { + public TaskExceptionFilterTests(ITestOutputHelper output) + : base(output) + { + } + + private static void TestFilterMethod() + { + // Test catch Exception + try + { + throw new ExecutionCanceledException(); + } + catch (Exception ex) + { + Debug.WriteLine(ex.GetType().FullName); + } + } + + [Fact(Timeout = 5000)] + public void TestAddExceptionFilter() + { + if (!this.IsSystematicTest) + { + // The non-rewritten code should catch the coyote exception. + TestFilterMethod(); + } + else + { + // The rewritten code should add a !(e is ExecutionCanceledException) filter + // which should allow this exception to escape the catch block. + this.RunWithException(TestFilterMethod); + } + } + + private static void TestFilterMethod2() + { + // Test catch RuntimeException + try + { + throw new ExecutionCanceledException(); + } + catch (RuntimeException ex) + { + Debug.WriteLine(ex.GetType().FullName); + } + } + + [Fact(Timeout = 5000)] + public void TestAddExceptionFilter2() + { + if (!this.IsSystematicTest) + { + // The non-rewritten code should catch the coyote exception.. + TestFilterMethod2(); + } + else + { + // The rewritten code should add a !(e is ExecutionCanceledException) filter + // which should allow this exception to escape the catch block. + this.RunWithException(TestFilterMethod2); + } + } + + private static void TestFilterMethod3() + { + // Test catch all + try + { + throw new ExecutionCanceledException(); + } + catch + { + Debug.WriteLine("caught"); + } + } + + [Fact(Timeout = 5000)] + public void TestAddExceptionFilter3() + { + if (!this.IsSystematicTest) + { + // The non-rewritten code should catch the coyote exception. + TestFilterMethod3(); + } + else + { + // The rewritten code should add a !(e is ExecutionCanceledException) filter + // which should allow this exception to escape the catch block. + this.RunWithException(TestFilterMethod3); + } + } + + private static void TestFilterMethod4() + { + // Test filter is unmodified if it is already correct! + try + { + throw new ExecutionCanceledException(); + } + catch (Exception ex) when (!(ex is ExecutionCanceledException)) + { + Debug.WriteLine(ex.GetType().FullName); + } + } + + [Fact(Timeout = 5000)] + public void TestAddExceptionFilter4() + { + // The non-rewritten code should allow the ExecutionCanceledException through + // and the rewritten code should be the same because the code should not be rewritten. + this.RunWithException(TestFilterMethod4); + } + + private static void TestFilterMethod5() + { + // Test more interesting filter is also unmodified if it is already correct! + try + { + throw new ExecutionCanceledException(); + } + catch (Exception ex) when (!(ex is NullReferenceException) && !(ex is ExecutionCanceledException)) + { + Debug.WriteLine(ex.GetType().FullName); + } + } + + [Fact(Timeout = 5000)] + public void TestAddExceptionFilter5() + { + // The non-rewritten code should allow the ExecutionCanceledException through + // and the rewritten code should be the same because the code should not be rewritten. + this.RunWithException(TestFilterMethod5); + } + + private static void TestFilterMethod6() + { + // Test more interesting filter is also unmodified if it is already correct! + // Test we can parse a slightly different order of expressions in the filter. + try + { + throw new ExecutionCanceledException(); + } + catch (Exception ex) when (!(ex is ExecutionCanceledException) && !(ex is NullReferenceException)) + { + Debug.WriteLine(ex.GetType().FullName); + } + } + + [Fact(Timeout = 5000)] + public void TestAddExceptionFilter6() + { + // The non-rewritten code should allow the ExecutionCanceledException through + // and the rewritten code should be the same because the code should not be rewritten. + this.RunWithException(TestFilterMethod6); + } + + private static void TestComplexFilterMethod() + { + // This test case we cannot yet handle because filter is too complex. + // This '|| debugging' expression causes the filter to catch ExecutionCanceledException + // which is bad, but this is hard to fix. + bool debugging = true; + try + { + throw new ExecutionCanceledException(); + } + catch (Exception ex) when (!(ex is ExecutionCanceledException) || debugging) + { + Debug.WriteLine(ex.GetType().FullName); + } + } + + [Fact(Timeout = 5000)] + public void TestEditComplexFilter() + { + if (!this.IsSystematicTest) + { + // The non-rewritten code should catch the coyote exception.. + this.Test(TestComplexFilterMethod); + } + else + { + // The rewritten code should add a !(e is ExecutionCanceledException) filter + // which should allow this exception to escape the catch block. + this.RunWithException(TestComplexFilterMethod); + } + } + + private static void TestComplexFilterMethod2() + { + // This test case we cannot yet handle because filter is too complex. + // This '&& debugging' expression causes the filter to catch ExecutionCanceledException + // which is bad, but this is hard to fix. + bool debugging = true; + try + { + throw new ExecutionCanceledException(); + } + catch (Exception ex) when (!(ex is NullReferenceException) && debugging) + { + Debug.WriteLine(ex.GetType().FullName); + } + } + + [Fact(Timeout = 5000)] + public void TestEditComplexFilter2() + { + if (!this.IsSystematicTest) + { + // The non-rewritten code should catch the coyote exception.. + this.Test(TestComplexFilterMethod2); + } + else + { + // The rewritten code should add a !(e is ExecutionCanceledException) filter + // which should allow this exception to escape the catch block. + this.RunWithException(TestComplexFilterMethod2); + } + } + + private static void TestComplexFilterMethod3() + { + try + { + throw new ExecutionCanceledException(); + } + catch (Exception ex) when (!(ex is NullReferenceException)) + { + Debug.WriteLine(ex.GetType().FullName); + } + } + + [Fact(Timeout = 5000)] + public void TestEditComplexFilter3() + { + if (!this.IsSystematicTest) + { + // The non-rewritten code should catch the coyote exception.. + this.Test(TestComplexFilterMethod3); + } + else + { + // The rewritten code should add a !(e is ExecutionCanceledException) filter + // which should allow this exception to escape the catch block. + this.RunWithException(TestComplexFilterMethod3); + } + } + + private static void TestComplexFilterMethod4() + { + // Test a crazy filter expression we cannot even parse... + int x = 10; + string suffix = "bad"; + try + { + Task.Run(() => + { + throw new ExecutionCanceledException(); + }).Wait(); + } + catch (Exception ex) when (ex.GetType().Name != (x > 10 ? "Foo" : "Bar" + suffix)) + { + Debug.WriteLine(ex.GetType().FullName); + } + } + + [Fact(Timeout = 5000)] + public void TestEditComplexFilter4() + { + if (!this.IsSystematicTest) + { + // The non-rewritten code should catch the coyote exception. + this.Test(TestComplexFilterMethod4); + } + else + { + // The rewritten code should add a !(e is ExecutionCanceledException) filter + // which should allow this exception to escape the catch block. + this.RunWithException(TestComplexFilterMethod4); + } + } + + private static void TestRethrowMethod() + { + // Test catch all, but it is ok because it does a rethrow, + // so this code should be unmodified. + try + { + throw new ExecutionCanceledException(); + } + catch (Exception) + { + throw; + } + } + + [Fact(Timeout = 5000)] + public void TestIgnoreRethrowCase() + { + // The non-rewritten code should rethrow the exception + // and the rewritten code should be the same because the code should not be rewritten. + this.RunWithException(TestRethrowMethod); + } + + private static void TestRethrowMethod2() + { + // Test catch all with specific filter for ExecutionCanceledException, + // but it is ok because it does a rethrow, so this code should be unmodified. + try + { + throw new ExecutionCanceledException(); + } + catch (Exception ex) when (ex is ExecutionCanceledException) + { + throw; + } + } + + [Fact(Timeout = 5000)] + public void TestIgnoreRethrowCase2() + { + // The non-rewritten code should rethrow the exception + // and the rewritten code should be the same because the code should not be rewritten. + this.RunWithException(TestRethrowMethod2); + } + } +} diff --git a/Tests/Production.Tests/Tasks/Locks/AsyncLockTests.cs b/Tests/Production.Tests/Tasks/Locks/AsyncLockTests.cs index 339ccbb7..ccdb8497 100644 --- a/Tests/Production.Tests/Tasks/Locks/AsyncLockTests.cs +++ b/Tests/Production.Tests/Tasks/Locks/AsyncLockTests.cs @@ -80,6 +80,12 @@ namespace Microsoft.Coyote.Production.Tests.Tasks [Fact(Timeout = 5000)] public void TestSynchronizeTwoParallelTasks() { + if (!this.IsSystematicTest) + { + // .NET cannot guarantee it will find this condition even with 200 iterations. + return; + } + this.TestWithError(async () => { SharedEntry entry = new SharedEntry();