Merged PR 2761: fix bug in interface method rewriting

The `MonitorTransform` was not guarding properly for abstract/interface methods. Fixed and added a unit test.

Source/Test/Rewriting/Transforms/MonitorTransform.cs

@@ -47,8 +47,14 @@ namespace Microsoft.Coyote.Rewriting
         /// <inheritdoc/>
         internal override void VisitMethod(MethodDefinition method)
         {
-            this.Method = method;
-            this.Processor = method.Body.GetILProcessor();
+            this.Method = null;
+
+            // Only non-abstract method bodies can be rewritten.
+            if (!method.IsAbstract)
+            {
+                this.Method = method;
+                this.Processor = method.Body.GetILProcessor();
+            }
         }
 
         /// <inheritdoc/>

Tests/BinaryRewriting.Tests/BinaryRewriting.Tests.csproj

@@ -17,6 +17,7 @@
     <Compile Include="..\Production.Tests\Tasks\TaskDelayTests.cs" Link="Tasks\TaskDelayTests.cs" />
     <Compile Include="..\Production.Tests\Tasks\TaskExceptionTests.cs" Link="Tasks\TaskExceptionTests.cs" />
     <Compile Include="..\Production.Tests\Tasks\TaskIdTests.cs" Link="Tasks\TaskIdTests.cs" />
+    <Compile Include="..\Production.Tests\Tasks\TaskInterfaceTests.cs" Link="Tasks\TaskInterfaceTests.cs" />
     <Compile Include="..\Production.Tests\Tasks\TaskInterleavingsTests.cs" Link="Tasks\TaskInterleavingsTests.cs" />
     <Compile Include="..\Production.Tests\Tasks\TaskRunTests.cs" Link="Tasks\TaskRunTests.cs" />
     <Compile Include="..\Production.Tests\Tasks\TaskYieldTests.cs" Link="Tasks\TaskYieldTests.cs" />

Tests/Production.Tests/Tasks/TaskInterfaceTests.cs

@@ -0,0 +1,53 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+#if BINARY_REWRITE
+using System.Threading.Tasks;
+#else
+using Microsoft.Coyote.Tasks;
+#endif
+using Microsoft.Coyote.Specifications;
+using Xunit;
+using Xunit.Abstractions;
+
+#if BINARY_REWRITE
+namespace Microsoft.Coyote.BinaryRewriting.Tests.Tasks
+#else
+namespace Microsoft.Coyote.Production.Tests.Tasks
+#endif
+{
+    public class TaskInterfaceTests : BaseProductionTest
+    {
+        public TaskInterfaceTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        private interface IAsyncSender
+        {
+            Task<bool> SendEventAsync();
+        }
+
+        private class AsyncSender : IAsyncSender
+        {
+            public async Task<bool> SendEventAsync()
+            {
+                // Model sending some event.
+                await Task.Delay(1);
+                return true;
+            }
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestAsyncInterfaceMethodCall()
+        {
+            this.Test(async () =>
+            {
+                IAsyncSender sender = new AsyncSender();
+                bool result = await sender.SendEventAsync();
+                Specification.Assert(result, "Unexpected result.");
+            },
+            configuration: GetConfiguration());
+        }
+    }
+}

Tests/SystematicTesting.Tests/Tasks/TaskInterfaceTests.cs

@@ -0,0 +1,17 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.SystematicTesting.Tests.Tasks
+{
+    public class TaskInterfaceTests : Production.Tests.Tasks.TaskInterfaceTests
+    {
+        public TaskInterfaceTests(ITestOutputHelper output)
+            : base(output)
+        {
+        }
+
+        public override bool IsSystematicTest => true;
+    }
+}