support for running xunit systematic tests from cli (#481)

Coyote.sln

@@ -47,6 +47,8 @@ Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "Tests.Rewriting", "Tests\Te
 EndProject
 Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "Tests.Runtime", "Tests\Tests.Runtime\Tests.Runtime.csproj", "{47FD6EEE-7AFB-40B2-BD34-880FA8896199}"
 EndProject
+Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "Tests.Tools", "Tests\Tests.Tools\Tests.Tools.csproj", "{161C3CD4-C374-47C2-B306-99D3019D8F47}"
+EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
 		Debug|Any CPU = Debug|Any CPU
@@ -57,14 +59,14 @@ Global
 		{4B03C121-C1C9-4C08-A673-BFD5FC821983}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{4B03C121-C1C9-4C08-A673-BFD5FC821983}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{4B03C121-C1C9-4C08-A673-BFD5FC821983}.Release|Any CPU.Build.0 = Release|Any CPU
-		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
-		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Debug|Any CPU.Build.0 = Debug|Any CPU
-		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Release|Any CPU.ActiveCfg = Release|Any CPU
-		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Release|Any CPU.Build.0 = Release|Any CPU
 		{E75DB9C9-7842-4AE4-A29D-624F6B49F607}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
 		{E75DB9C9-7842-4AE4-A29D-624F6B49F607}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{E75DB9C9-7842-4AE4-A29D-624F6B49F607}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{E75DB9C9-7842-4AE4-A29D-624F6B49F607}.Release|Any CPU.Build.0 = Release|Any CPU
+		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{8548010B-B99D-44FD-95BD-F716C1D707B7}.Release|Any CPU.Build.0 = Release|Any CPU
 		{911F1779-3558-4590-836C-C75112D65FD8}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
 		{911F1779-3558-4590-836C-C75112D65FD8}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{911F1779-3558-4590-836C-C75112D65FD8}.Release|Any CPU.ActiveCfg = Release|Any CPU
@@ -113,14 +115,18 @@ Global
 		{47FD6EEE-7AFB-40B2-BD34-880FA8896199}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{47FD6EEE-7AFB-40B2-BD34-880FA8896199}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{47FD6EEE-7AFB-40B2-BD34-880FA8896199}.Release|Any CPU.Build.0 = Release|Any CPU
+		{161C3CD4-C374-47C2-B306-99D3019D8F47}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{161C3CD4-C374-47C2-B306-99D3019D8F47}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{161C3CD4-C374-47C2-B306-99D3019D8F47}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{161C3CD4-C374-47C2-B306-99D3019D8F47}.Release|Any CPU.Build.0 = Release|Any CPU
 	EndGlobalSection
 	GlobalSection(SolutionProperties) = preSolution
 		HideSolutionNode = FALSE
 	EndGlobalSection
 	GlobalSection(NestedProjects) = preSolution
 		{4B03C121-C1C9-4C08-A673-BFD5FC821983} = {83369B7E-5C21-4D49-A14C-E8A6A4892807}
-		{8548010B-B99D-44FD-95BD-F716C1D707B7} = {83369B7E-5C21-4D49-A14C-E8A6A4892807}
 		{E75DB9C9-7842-4AE4-A29D-624F6B49F607} = {83369B7E-5C21-4D49-A14C-E8A6A4892807}
+		{8548010B-B99D-44FD-95BD-F716C1D707B7} = {83369B7E-5C21-4D49-A14C-E8A6A4892807}
 		{911F1779-3558-4590-836C-C75112D65FD8} = {2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}
 		{DABC68C1-79D3-4324-A750-7CF72E0A0ACF} = {2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}
 		{61FC86A6-AF87-4007-B184-AF860A57AB9E} = {2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}
@@ -133,6 +139,7 @@ Global
 		{130CC5A8-946C-4EB3-982C-F6A57EB65326} = {2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}
 		{D962786B-EBBA-40BA-814C-96C02675E2D1} = {2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}
 		{47FD6EEE-7AFB-40B2-BD34-880FA8896199} = {2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}
+		{161C3CD4-C374-47C2-B306-99D3019D8F47} = {2012300C-6E5D-47A0-9D57-B3F0A73AA1D4}
 	EndGlobalSection
 	GlobalSection(ExtensibilityGlobals) = postSolution
 		SolutionGuid = {B9407046-CB24-4B07-8031-2749696EC7D8}

Scripts/run-tests.ps1

@@ -4,7 +4,7 @@
 param(
     [ValidateSet("net7.0", "net6.0", "netcoreapp3.1", "net462")]
     [string]$framework = "net7.0",
-    [ValidateSet("all", "runtime", "rewriting", "testing", "actors", "actors-testing", "standalone")]
+    [ValidateSet("all", "runtime", "rewriting", "testing", "actors", "actors-testing", "tools")]
     [string]$test = "all",
     [string]$filter = "",
     [string]$logger = "",
@@ -23,6 +23,7 @@ $targets = [ordered]@{
     "testing" = "Tests.BugFinding"
     "actors" = "Tests.Actors"
     "actors-testing" = "Tests.Actors.BugFinding"
+    "tools" = "Tests.Tools"
 }
 
 # Find that paths to the installed .NET runtime.

Source/Core/Properties/InternalsVisibleTo.cs

@@ -68,6 +68,12 @@
     "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
     "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
     "3bc97f9e")]
+[assembly: InternalsVisibleTo("Microsoft.Coyote.Tests.Tools,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
 [assembly: InternalsVisibleTo("Tests.Performance,PublicKey=" +
     "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
     "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +

Source/Test/Properties/InternalsVisibleTo.cs

@@ -34,6 +34,12 @@
     "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
     "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
     "3bc97f9e")]
+[assembly: InternalsVisibleTo("Microsoft.Coyote.Tests.Tools,PublicKey=" +
+    "0024000004800000940000000602000000240000525341310004000001000100d7971281941569" +
+    "53fd8af100ac5ecaf1d96fab578562b91133663d6ccbf0b313d037a830a20d7af1ce02a6641d71" +
+    "d7bc9fd67a08d3fa122120a469158da22a652af4508571ac9b16c6a05d2b3b6d7004ac76be85c3" +
+    "ca3d55f6ae823cd287a2810243f2bd6be5f4ba7b016c80da954371e591b10c97b0938f721c7149" +
+    "3bc97f9e")]
 
 // Tools
 [assembly: InternalsVisibleTo("Coyote,PublicKey=" +

Source/Test/Rewriting/Attributes.cs

@@ -13,7 +13,7 @@ namespace Microsoft.Coyote.Rewriting
     /// If this attribute is applied to an assembly manifest, it denotes that the
     /// assembly has been rewritten.
     /// </remarks>
-    [AttributeUsage(AttributeTargets.Assembly)]
+    [AttributeUsage(AttributeTargets.Assembly, AllowMultiple = false)]
     public sealed class RewritingSignatureAttribute : Attribute
     {
         /// <summary>
@@ -39,7 +39,7 @@ public RewritingSignatureAttribute(string version, string signature)
     /// <summary>
     /// Attribute for declaring source code targets that must not be rewritten.
     /// </summary>
-    [AttributeUsage(AttributeTargets.Class | AttributeTargets.Struct)]
+    [AttributeUsage(AttributeTargets.Class | AttributeTargets.Struct, AllowMultiple = false)]
     public sealed class SkipRewritingAttribute : Attribute
     {
         /// <summary>

Source/Test/SystematicTesting/Frameworks/ITestLog.cs

@@ -0,0 +1,18 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using Microsoft.Coyote.Logging;
+
+namespace Microsoft.Coyote.SystematicTesting.Frameworks
+{
+    /// <summary>
+    /// Logs all test output to the installed <see cref="ILogger"/>.
+    /// </summary>
+    internal interface ITestLog
+    {
+        /// <summary>
+        /// Logs messages using the installed <see cref="ILogger"/>.
+        /// </summary>
+        LogWriter LogWriter { get; set; }
+    }
+}

Source/Test/SystematicTesting/Frameworks/Xunit/TestOutput.cs

@@ -0,0 +1,31 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using Microsoft.Coyote.Logging;
+using Xunit.Abstractions;
+
+namespace Microsoft.Coyote.SystematicTesting.Frameworks.XUnit
+{
+    /// <summary>
+    /// Redirects all xUnit test output to the installed <see cref="ILogger"/>.
+    /// </summary>
+    internal sealed class TestOutput : ITestOutputHelper, ITestLog
+    {
+        /// <summary>
+        /// Logs messages using the installed <see cref="ILogger"/>.
+        /// </summary>
+        public LogWriter LogWriter { get; set; }
+
+        /// <inheritdoc/>
+        public void WriteLine(string message)
+        {
+            this.LogWriter.WriteLine(message);
+        }
+
+        /// <inheritdoc/>
+        public void WriteLine(string format, params object[] args)
+        {
+            this.LogWriter.WriteLine(format, args);
+        }
+    }
+}

Tests/Tests.Common/TestOutputLogger.cs → Source/Test/SystematicTesting/Frameworks/Xunit/TestOutputLogger.cs

@@ -5,10 +5,10 @@
 using Microsoft.Coyote.Logging;
 using Xunit.Abstractions;
 
-namespace Microsoft.Coyote.Tests.Common
+namespace Microsoft.Coyote.SystematicTesting.Frameworks.XUnit
 {
     /// <summary>
-    /// Logger that writes to the test output.
+    /// Logger that writes to the xUnit test output.
     /// </summary>
     public sealed class TestOutputLogger : ILogger
     {
@@ -63,6 +63,7 @@ public void Write(string format, object arg0, object arg1, object arg2) =>
         public void Write(string format, params object[] args) =>
             this.Write(LogSeverity.Info, format, args);
 
+        /// <inheritdoc/>
         public void Write(LogSeverity severity, string value)
         {
             lock (this.Lock)

Source/Test/SystematicTesting/Reports/TraceReport.cs

@@ -63,11 +63,21 @@ internal static string GetJson(OperationScheduler scheduler, Configuration confi
             report.Settings.PortfolioMode = configuration.PortfolioMode.ToString().ToLower();
             report.Settings.IsLivenessCheckingEnabled = configuration.IsLivenessCheckingEnabled;
             report.Settings.LivenessTemperatureThreshold = configuration.LivenessTemperatureThreshold;
+            report.Settings.IsCollectionAccessRaceCheckingEnabled = configuration.IsCollectionAccessRaceCheckingEnabled;
             report.Settings.IsLockAccessRaceCheckingEnabled = configuration.IsLockAccessRaceCheckingEnabled;
-            report.Settings.IsPartiallyControlledConcurrencyAllowed = configuration.IsPartiallyControlledConcurrencyAllowed;
-            report.Settings.IsPartiallyControlledDataNondeterminismAllowed = configuration.IsPartiallyControlledDataNondeterminismAllowed;
-            report.Settings.UncontrolledConcurrencyResolutionAttempts = configuration.UncontrolledConcurrencyResolutionAttempts;
-            report.Settings.UncontrolledConcurrencyResolutionDelay = configuration.UncontrolledConcurrencyResolutionDelay;
+            report.Settings.IsAtomicOperationRaceCheckingEnabled = configuration.IsAtomicOperationRaceCheckingEnabled;
+            report.Settings.IsVolatileOperationRaceCheckingEnabled =
+                configuration.IsVolatileOperationRaceCheckingEnabled;
+            report.Settings.IsMemoryAccessRaceCheckingEnabled = configuration.IsMemoryAccessRaceCheckingEnabled;
+            report.Settings.IsControlFlowRaceCheckingEnabled = configuration.IsControlFlowRaceCheckingEnabled;
+            report.Settings.IsPartiallyControlledConcurrencyAllowed =
+                configuration.IsPartiallyControlledConcurrencyAllowed;
+            report.Settings.IsPartiallyControlledDataNondeterminismAllowed =
+                configuration.IsPartiallyControlledDataNondeterminismAllowed;
+            report.Settings.UncontrolledConcurrencyResolutionAttempts =
+                configuration.UncontrolledConcurrencyResolutionAttempts;
+            report.Settings.UncontrolledConcurrencyResolutionDelay =
+                configuration.UncontrolledConcurrencyResolutionDelay;
 
             report.ReportTrace(scheduler.Trace.Clone());
             return report.ToJson();
@@ -104,11 +114,23 @@ internal static ExecutionTrace FromJson(Configuration configuration)
                 configuration.PortfolioMode = PortfolioModeExtensions.FromString(report.Settings.PortfolioMode);
                 configuration.IsLivenessCheckingEnabled = report.Settings.IsLivenessCheckingEnabled;
                 configuration.LivenessTemperatureThreshold = report.Settings.LivenessTemperatureThreshold;
+                configuration.IsCollectionAccessRaceCheckingEnabled =
+                    report.Settings.IsCollectionAccessRaceCheckingEnabled;
                 configuration.IsLockAccessRaceCheckingEnabled = report.Settings.IsLockAccessRaceCheckingEnabled;
-                configuration.IsPartiallyControlledConcurrencyAllowed = report.Settings.IsPartiallyControlledConcurrencyAllowed;
-                configuration.IsPartiallyControlledDataNondeterminismAllowed = report.Settings.IsPartiallyControlledDataNondeterminismAllowed;
-                configuration.UncontrolledConcurrencyResolutionAttempts = report.Settings.UncontrolledConcurrencyResolutionAttempts;
-                configuration.UncontrolledConcurrencyResolutionDelay = report.Settings.UncontrolledConcurrencyResolutionDelay;
+                configuration.IsAtomicOperationRaceCheckingEnabled =
+                    report.Settings.IsAtomicOperationRaceCheckingEnabled;
+                configuration.IsVolatileOperationRaceCheckingEnabled =
+                    report.Settings.IsVolatileOperationRaceCheckingEnabled;
+                configuration.IsMemoryAccessRaceCheckingEnabled = report.Settings.IsMemoryAccessRaceCheckingEnabled;
+                configuration.IsControlFlowRaceCheckingEnabled = report.Settings.IsControlFlowRaceCheckingEnabled;
+                configuration.IsPartiallyControlledConcurrencyAllowed =
+                    report.Settings.IsPartiallyControlledConcurrencyAllowed;
+                configuration.IsPartiallyControlledDataNondeterminismAllowed =
+                    report.Settings.IsPartiallyControlledDataNondeterminismAllowed;
+                configuration.UncontrolledConcurrencyResolutionAttempts =
+                    report.Settings.UncontrolledConcurrencyResolutionAttempts;
+                configuration.UncontrolledConcurrencyResolutionDelay =
+                    report.Settings.UncontrolledConcurrencyResolutionDelay;
 
                 for (int idx = 0; idx < report.Steps.Count; idx++)
                 {
@@ -236,11 +258,36 @@ public sealed class TestSettings
             /// </summary>
             public int LivenessTemperatureThreshold { get; set; }
 
+            /// <summary>
+            /// Value specifying if checking races at collection accesses is enabled or not.
+            /// </summary>
+            public bool IsCollectionAccessRaceCheckingEnabled { get; set; }
+
             /// <summary>
             /// Value specifying if checking races during lock accesses is enabled or not.
             /// </summary>
             public bool IsLockAccessRaceCheckingEnabled { get; set; }
 
+            /// <summary>
+            /// Value specifying if checking races at atomic operations is enabled or not.
+            /// </summary>
+            public bool IsAtomicOperationRaceCheckingEnabled { get; set; }
+
+            /// <summary>
+            /// Value specifying if checking races at volatile operations is enabled or not.
+            /// </summary>
+            public bool IsVolatileOperationRaceCheckingEnabled { get; set; }
+
+            /// <summary>
+            /// Value specifying if checking races at memory-access locations is enabled or not.
+            /// </summary>
+            public bool IsMemoryAccessRaceCheckingEnabled { get; set; }
+
+            /// <summary>
+            /// Value specifying if checking races at control-flow branching locations is enabled or not.
+            /// </summary>
+            public bool IsControlFlowRaceCheckingEnabled { get; set; }
+
             /// <summary>
             /// Value specifying if partially controlled concurrency is allowed or not.
             /// </summary>

Source/Test/SystematicTesting/TestAttributes.cs

@@ -8,31 +8,31 @@ namespace Microsoft.Coyote.SystematicTesting
     /// <summary>
     /// Attribute for declaring the entry point to a Coyote test.
     /// </summary>
-    [AttributeUsage(AttributeTargets.Method)]
+    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false)]
     public sealed class TestAttribute : Attribute
     {
     }
 
     /// <summary>
     /// Attribute for declaring the initialization method to be called before testing starts.
     /// </summary>
-    [AttributeUsage(AttributeTargets.Method)]
+    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false)]
     public sealed class TestInitAttribute : Attribute
     {
     }
 
     /// <summary>
     /// Attribute for declaring a cleanup method to be called when all test iterations terminate.
     /// </summary>
-    [AttributeUsage(AttributeTargets.Method)]
+    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false)]
     public sealed class TestDisposeAttribute : Attribute
     {
     }
 
     /// <summary>
     /// Attribute for declaring a cleanup method to be called when each test iteration terminates.
     /// </summary>
-    [AttributeUsage(AttributeTargets.Method)]
+    [AttributeUsage(AttributeTargets.Method, AllowMultiple = false)]
     public sealed class TestIterationDisposeAttribute : Attribute
     {
     }