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

@@ -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
         }
     }
 }

Source/Core/IO/ErrorReporter.cs

@@ -35,8 +35,7 @@ namespace Microsoft.Coyote.IO
         /// </summary>
         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);
         }
 

Source/Core/IO/Logging/ConsoleLogger.cs

@@ -53,5 +53,29 @@ namespace Microsoft.Coyote.IO
         {
             Console.WriteLine(value);
         }
+
+        /// <summary>
+        /// Reports an error, followed by the current line terminator.
+        /// </summary>
+        /// <param name="value">The string to write.</param>
+#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();
+        }
+
+        /// <summary>
+        /// Reports an warning, followed by the current line terminator.
+        /// </summary>
+        /// <param name="value">The string to write.</param>
+#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();
+        }
     }
 }

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" +

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
+{
+    /// <summary>
+    /// Provides a set of static methods for working with specific kinds of <see cref="Exception"/> instances.
+    /// </summary>
+    /// <remarks>This type is intended for compiler use rather than use directly in code.</remarks>
+    [EditorBrowsable(EditorBrowsableState.Never)]
+    public static class ExceptionHandlers
+    {
+        /// <summary>
+        /// 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.
+        /// </summary>
+        /// <param name="e">The exception object.</param>
+        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);
+                }
+            }
+        }
+    }
+}

Source/Test/Rewriting/AssemblyRewriter.cs

@@ -42,6 +42,11 @@ namespace Microsoft.Coyote.Rewriting
         /// </summary>
         private readonly List<AssemblyTransform> Transforms;
 
+        /// <summary>
+        /// The output log.
+        /// </summary>
+        private readonly ConsoleLogger Log = new ConsoleLogger();
+
         /// <summary>
         /// Initializes a new instance of the <see cref="AssemblyRewriter"/> class.
         /// </summary>
@@ -59,8 +64,9 @@ namespace Microsoft.Coyote.Rewriting
 
             this.Transforms = new List<AssemblyTransform>()
             {
-                 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
         /// </summary>
         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
         /// <summary>
         /// Handles an assembly resolution error.
         /// </summary>
-        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;
         }
     }

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
+    {
+        /// <summary>
+        /// Console output writer.
+        /// </summary>
+        private readonly ConsoleLogger Log;
+
+        /// <summary>
+        /// The type being transformed.
+        /// </summary>
+        private TypeDefinition TypeDef;
+
+        /// <summary>
+        /// Is part of an async state machine.
+        /// </summary>
+        private bool IsStateMachine;
+
+        /// <summary>
+        /// The current method being transformed.
+        /// </summary>
+        private MethodDefinition Method;
+
+        internal ExceptionFilterTransform(ConsoleLogger log)
+        {
+            this.Log = log;
+        }
+
+        /// <inheritdoc/>
+        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();
+        }
+
+        /// <inheritdoc/>
+        internal override void VisitMethod(MethodDefinition method)
+        {
+            this.Method = method;
+        }
+
+        /// <inheritdoc/>
+        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<Instruction> GetHandlerInstructions(ExceptionHandler handler)
+        {
+            if (handler.HandlerStart == null)
+            {
+                return null;
+            }
+
+            List<Instruction> result = new List<Instruction>();
+            for (var i = handler.HandlerStart; i != handler.HandlerEnd; i = i.Next)
+            {
+                if (i.OpCode.Code != Code.Nop)
+                {
+                    result.Add(i);
+                }
+            }
+
+            return result;
+        }
+    }
+}

Source/Test/Rewriting/Transforms/MonitorTransform.cs

@@ -37,6 +37,16 @@ namespace Microsoft.Coyote.Rewriting
 
         private const string MonitorClassName = "System.Threading.Monitor";
 
+        /// <summary>
+        /// Console output writer.
+        /// </summary>
+        private readonly ConsoleLogger Log;
+
+        internal MonitorTransform(ConsoleLogger log)
+        {
+            this.Log = log;
+        }
+
         /// <inheritdoc/>
         internal override void VisitModule(ModuleDefinition module)
         {

Source/Test/Rewriting/Transforms/TaskTransform.cs

@@ -42,11 +42,17 @@ namespace Microsoft.Coyote.Rewriting
         /// </summary>
         private ILProcessor Processor;
 
+        /// <summary>
+        /// Console output writer.
+        /// </summary>
+        private readonly ConsoleLogger Log;
+
         /// <summary>
         /// Initializes a new instance of the <see cref="TaskTransform"/> class.
         /// </summary>
-        internal TaskTransform()
+        internal TaskTransform(ConsoleLogger log)
         {
+            this.Log = log;
             this.RewrittenMethodCache = new Dictionary<string, MethodReference>();
         }
 

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
+{
+    /// <summary>
+    /// Tests that we can insert ExecutionCanceledException filter.
+    /// </summary>
+    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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(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<ExecutionCanceledException>(TestRethrowMethod2);
+        }
+    }
+}

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();