improvements in binary rewriting (#244)

.config/dotnet-tools.json

@@ -0,0 +1,12 @@
+{
+  "version": 1,
+  "isRoot": true,
+  "tools": {
+    "dotnet-ilverify": {
+      "version": "5.0.0",
+      "commands": [
+        "ilverify"
+      ]
+    }
+  }
+}

Common/build.props

@@ -33,9 +33,6 @@
   <PropertyGroup Condition="'$(CoyoteTargetType)' == 'Library'">
     <TargetFrameworks>$(TargetFrameworks);netstandard2.0;netstandard2.1</TargetFrameworks>
   </PropertyGroup>
-  <PropertyGroup Condition="'$(CoyoteTargetType)' == 'Library' and '$(OS)'=='Windows_NT'">
-    <TargetFrameworks Condition="'$(Framework462Installed)' and '$(Framework462Supported)'">$(TargetFrameworks);net462</TargetFrameworks>
-  </PropertyGroup>
   <PropertyGroup Condition="'$(CoyoteTargetType)' == 'Application' and '$(OS)'=='Windows_NT'">
     <TargetFrameworks Condition="'$(Framework462Installed)' and '$(Framework462Supported)'">$(TargetFrameworks);net462</TargetFrameworks>
     <TargetFrameworks Condition="'$(NetCore31Installed)' and '$(NetCore31Supported)'">$(TargetFrameworks);netcoreapp3.1</TargetFrameworks>

Scripts/run-tests.ps1

@@ -23,14 +23,12 @@ $targets = [ordered]@{
     "standalone" = "Tests.Standalone"
 }
 
-$ilverify = FindProgram("ilverify")
-if ($null -eq $ilverify) {
-    &dotnet tool install --global dotnet-ilverify
-    $ilverify = FindProgram("ilverify");
-}
-
 $dotnet_path = FindDotNet("dotnet");
 
+# Restore the local ilverify tool.
+&dotnet tool restore
+$ilverify = "dotnet ilverify"
+
 [System.Environment]::SetEnvironmentVariable('COYOTE_CLI_TELEMETRY_OPTOUT', '1')
 
 Write-Comment -prefix "." -text "Running the Coyote tests" -color "yellow"
@@ -62,7 +60,7 @@ foreach ($kvp in $targets.GetEnumerator()) {
             $command = $command + ' -r "' + "$dotnet_path/packs/Microsoft.NETCore.App.Ref/5.0.0/ref/net5.0/*.dll" + '"'
             $command = $command + ' -r "' + "$PSScriptRoot/../bin/net5.0/*.dll" + '"'
             $command = $command + ' -r "' + $NetCoreApp + '/*.dll"'
-            Invoke-ToolCommand -tool $ilverify -cmd $command -error_msg "Verifying assembly failed"
+            Invoke-ToolCommand -tool $ilverify -cmd $command -error_msg "found corrupted assembly rewriting"
         }
 
         Invoke-DotnetTest -dotnet $dotnet -project $($kvp.Name) -target $target -filter $filter -logger $logger -framework $f -verbosity $v

Source/Core/Actors/ActorFactory.cs

@@ -33,7 +33,7 @@ namespace Microsoft.Coyote.Actors
                     var constructorInfo = type.GetConstructor(Type.EmptyTypes);
                     if (constructorInfo is null)
                     {
-                        throw new Exception("Could not find empty constructor for type " + type.FullName);
+                        throw new InvalidOperationException("Could not find empty constructor for type " + type.FullName);
                     }
 
                     constructor = Expression.Lambda<Func<Actor>>(

Source/Core/Actors/ActorId.cs

@@ -109,7 +109,6 @@ namespace Microsoft.Coyote.Actors
         {
             if (obj is ActorId id)
             {
-                // Use same machanism for hashing.
                 if (this.IsNameUsedForHashing != id.IsNameUsedForHashing)
                 {
                     return false;

Source/Core/Actors/Coverage/ActorRuntimeLogGraphBuilder.cs

@@ -1000,7 +1000,8 @@ namespace Microsoft.Coyote.Actors.Coverage
             var ns = doc.Root.Name.Namespace;
             if (ns != DgmlNamespace)
             {
-                throw new Exception(string.Format("File '{0}' does not contain the DGML namespace", graphFilePath));
+                throw new InvalidOperationException(string.Format(
+                    "File '{0}' does not contain the DGML namespace", graphFilePath));
             }
 
             foreach (var e in doc.Root.Element(ns + "Nodes").Elements(ns + "Node"))

Source/Core/Configuration.cs

@@ -40,12 +40,6 @@ namespace Microsoft.Coyote
         [DataMember]
         internal string AssemblyToBeAnalyzed;
 
-        /// <summary>
-        /// The path to the binary rewriting configuration file or a folder containing assemblies to rewrite.
-        /// </summary>
-        [DataMember]
-        internal string RewritingOptionsPath;
-
         /// <summary>
         /// Test method to be used.
         /// </summary>
@@ -363,7 +357,6 @@ namespace Microsoft.Coyote
             this.OutputFilePath = string.Empty;
 
             this.AssemblyToBeAnalyzed = string.Empty;
-            this.RewritingOptionsPath = string.Empty;
             this.TestMethodName = string.Empty;
 
             this.SchedulingStrategy = "random";

Source/Core/Interception/Runtime/CompilerServices/AsyncTaskMethodBuilder.cs

@@ -5,6 +5,7 @@ using System;
 using System.Diagnostics;
 using System.Runtime.CompilerServices;
 using System.Runtime.InteropServices;
+using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Runtime;
 using SystemCompiler = System.Runtime.CompilerServices;
@@ -59,8 +60,24 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Creates an instance of the <see cref="AsyncTaskMethodBuilder"/> struct.
         /// </summary>
-        public static AsyncTaskMethodBuilder Create() =>
+        public static AsyncTaskMethodBuilder Create()
-            new AsyncTaskMethodBuilder(CoyoteRuntime.Current);
+        {
+            CoyoteRuntime runtime = null;
+            SynchronizationContext context = SynchronizationContext.Current;
+            if (context is ControlledSynchronizationContext controlledContext)
+            {
+                runtime = controlledContext.Runtime;
+            }
+            else if (context is null)
+            {
+                // Try get the current runtime, if it exists, and use it to set the current
+                // synchronization context to the controlled synchronization context.
+                runtime = CoyoteRuntime.Current;
+                runtime?.SetControlledSynchronizationContext();
+            }
+
+            return new AsyncTaskMethodBuilder(runtime);
+        }
 
         /// <summary>
         /// Begins running the builder with the associated state machine.
@@ -70,7 +87,8 @@ namespace Microsoft.Coyote.Interception
         public void Start<TStateMachine>(ref TStateMachine stateMachine)
             where TStateMachine : IAsyncStateMachine
         {
-            IO.Debug.WriteLine("<AsyncBuilder> Start state machine from task '{0}'.", Task.CurrentId);
+            IO.Debug.WriteLine("<AsyncBuilder> Start state machine from task '{0}' with context '{1}'.",
+                Task.CurrentId, SynchronizationContext.Current);
             this.MethodBuilder.Start(ref stateMachine);
         }
 
@@ -165,8 +183,24 @@ namespace Microsoft.Coyote.Interception
         /// Creates an instance of the <see cref="AsyncTaskMethodBuilder{TResult}"/> struct.
         /// </summary>
 #pragma warning disable CA1000 // Do not declare static members on generic types
-        public static AsyncTaskMethodBuilder<TResult> Create() =>
+        public static AsyncTaskMethodBuilder<TResult> Create()
-            new AsyncTaskMethodBuilder<TResult>(CoyoteRuntime.Current);
+        {
+            CoyoteRuntime runtime = null;
+            SynchronizationContext context = SynchronizationContext.Current;
+            if (context is ControlledSynchronizationContext controlledContext)
+            {
+                runtime = controlledContext.Runtime;
+            }
+            else if (context is null)
+            {
+                // Try get the current runtime, if it exists, and use it to set the current
+                // synchronization context to the controlled synchronization context.
+                runtime = CoyoteRuntime.Current;
+                runtime?.SetControlledSynchronizationContext();
+            }
+
+            return new AsyncTaskMethodBuilder<TResult>(runtime);
+        }
 #pragma warning restore CA1000 // Do not declare static members on generic types
 
         /// <summary>
@@ -177,7 +211,8 @@ namespace Microsoft.Coyote.Interception
         public void Start<TStateMachine>(ref TStateMachine stateMachine)
             where TStateMachine : IAsyncStateMachine
         {
-            IO.Debug.WriteLine("<AsyncBuilder> Start state machine from task '{0}'.", System.Threading.Tasks.Task.CurrentId);
+            IO.Debug.WriteLine("<AsyncBuilder> Start state machine from task '{0}' with context '{1}'.",
+                System.Threading.Tasks.Task.CurrentId, SynchronizationContext.Current);
             this.MethodBuilder.Start(ref stateMachine);
         }
 

Source/Core/Interception/Runtime/CompilerServices/ConfiguredTaskAwaitable.cs

@@ -3,10 +3,10 @@
 
 using System;
 using System.Runtime.CompilerServices;
+using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Runtime;
 using SystemCompiler = System.Runtime.CompilerServices;
-using SystemTasks = System.Threading.Tasks;
 
 namespace Microsoft.Coyote.Interception
 {
@@ -26,10 +26,9 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Initializes a new instance of the <see cref="ConfiguredTaskAwaitable"/> struct.
         /// </summary>
-        internal ConfiguredTaskAwaitable(CoyoteRuntime runtime, SystemTasks.Task awaitedTask,
+        internal ConfiguredTaskAwaitable(Task awaitedTask, bool continueOnCapturedContext)
-            bool continueOnCapturedContext)
         {
-            this.Awaiter = new ConfiguredTaskAwaiter(runtime, awaitedTask, continueOnCapturedContext);
+            this.Awaiter = new ConfiguredTaskAwaiter(awaitedTask, continueOnCapturedContext);
         }
 
         /// <summary>
@@ -44,15 +43,10 @@ namespace Microsoft.Coyote.Interception
         /// <remarks>This type is intended for compiler use rather than use directly in code.</remarks>
         public struct ConfiguredTaskAwaiter : ICriticalNotifyCompletion, INotifyCompletion
         {
-            /// <summary>
-            /// Responsible for controlling the execution of tasks during systematic testing.
-            /// </summary>
-            private readonly CoyoteRuntime Runtime;
-
             /// <summary>
             /// The task being awaited.
             /// </summary>
-            private readonly SystemTasks.Task AwaitedTask;
+            private readonly Task AwaitedTask;
 
             /// <summary>
             /// The task awaiter.
@@ -67,16 +61,14 @@ namespace Microsoft.Coyote.Interception
             /// <summary>
             /// Initializes a new instance of the <see cref="ConfiguredTaskAwaiter"/> struct.
             /// </summary>
-            internal ConfiguredTaskAwaiter(CoyoteRuntime runtime, SystemTasks.Task awaitedTask,
+            internal ConfiguredTaskAwaiter(Task awaitedTask, bool continueOnCapturedContext)
-                bool continueOnCapturedContext)
             {
-                if (runtime?.SchedulingPolicy != SchedulingPolicy.None)
+                if (SynchronizationContext.Current is ControlledSynchronizationContext)
                 {
                     // Force the continuation to run on the current context so that it can be controlled.
                     continueOnCapturedContext = true;
                 }
 
-                this.Runtime = runtime;
                 this.AwaitedTask = awaitedTask;
                 this.Awaiter = awaitedTask.ConfigureAwait(continueOnCapturedContext).GetAwaiter();
             }
@@ -86,7 +78,11 @@ namespace Microsoft.Coyote.Interception
             /// </summary>
             public void GetResult()
             {
-                this.Runtime?.OnWaitTask(this.AwaitedTask);
+                if (SynchronizationContext.Current is ControlledSynchronizationContext context)
+                {
+                    context.Runtime?.OnWaitTask(this.AwaitedTask);
+                }
+
                 this.Awaiter.GetResult();
             }
 
@@ -120,10 +116,9 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Initializes a new instance of the <see cref="ConfiguredTaskAwaitable{TResult}"/> struct.
         /// </summary>
-        internal ConfiguredTaskAwaitable(CoyoteRuntime runtime, SystemTasks.Task<TResult> awaitedTask,
+        internal ConfiguredTaskAwaitable(Task<TResult> awaitedTask, bool continueOnCapturedContext)
-            bool continueOnCapturedContext)
         {
-            this.Awaiter = new ConfiguredTaskAwaiter(runtime, awaitedTask, continueOnCapturedContext);
+            this.Awaiter = new ConfiguredTaskAwaiter(awaitedTask, continueOnCapturedContext);
         }
 
         /// <summary>
@@ -138,15 +133,10 @@ namespace Microsoft.Coyote.Interception
         /// <remarks>This type is intended for compiler use rather than use directly in code.</remarks>
         public struct ConfiguredTaskAwaiter : ICriticalNotifyCompletion, INotifyCompletion
         {
-            /// <summary>
-            /// Responsible for controlling the execution of tasks during systematic testing.
-            /// </summary>
-            private readonly CoyoteRuntime Runtime;
-
             /// <summary>
             /// The task being awaited.
             /// </summary>
-            private readonly SystemTasks.Task<TResult> AwaitedTask;
+            private readonly Task<TResult> AwaitedTask;
 
             /// <summary>
             /// The task awaiter.
@@ -161,16 +151,14 @@ namespace Microsoft.Coyote.Interception
             /// <summary>
             /// Initializes a new instance of the <see cref="ConfiguredTaskAwaiter"/> struct.
             /// </summary>
-            internal ConfiguredTaskAwaiter(CoyoteRuntime runtime, SystemTasks.Task<TResult> awaitedTask,
+            internal ConfiguredTaskAwaiter(Task<TResult> awaitedTask, bool continueOnCapturedContext)
-                bool continueOnCapturedContext)
             {
-                if (runtime?.SchedulingPolicy != SchedulingPolicy.None)
+                if (SynchronizationContext.Current is ControlledSynchronizationContext)
                 {
                     // Force the continuation to run on the current context so that it can be controlled.
                     continueOnCapturedContext = true;
                 }
 
-                this.Runtime = runtime;
                 this.AwaitedTask = awaitedTask;
                 this.Awaiter = awaitedTask.ConfigureAwait(continueOnCapturedContext).GetAwaiter();
             }
@@ -180,7 +168,11 @@ namespace Microsoft.Coyote.Interception
             /// </summary>
             public TResult GetResult()
             {
-                this.Runtime?.OnWaitTask(this.AwaitedTask);
+                if (SynchronizationContext.Current is ControlledSynchronizationContext context)
+                {
+                    context.Runtime?.OnWaitTask(this.AwaitedTask);
+                }
+
                 return this.Awaiter.GetResult();
             }
 

Source/Core/Interception/Runtime/CompilerServices/TaskAwaiter.cs

@@ -2,7 +2,9 @@
 // Licensed under the MIT License.
 
 using System;
+using System.Reflection;
 using System.Runtime.CompilerServices;
+using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Coyote.Runtime;
 using SystemCompiler = System.Runtime.CompilerServices;
@@ -20,11 +22,6 @@ namespace Microsoft.Coyote.Interception
         // WARNING: The layout must remain the same, as the struct is used to access
         // the generic TaskAwaiter<> as TaskAwaiter.
 
-        /// <summary>
-        /// Responsible for controlling the execution of tasks during systematic testing.
-        /// </summary>
-        private readonly CoyoteRuntime Runtime;
-
         /// <summary>
         /// The task being awaited.
         /// </summary>
@@ -43,9 +40,8 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Initializes a new instance of the <see cref="TaskAwaiter"/> struct.
         /// </summary>
-        internal TaskAwaiter(CoyoteRuntime runtime, SystemTasks.Task awaitedTask)
+        internal TaskAwaiter(SystemTasks.Task awaitedTask)
         {
-            this.Runtime = runtime;
             this.AwaitedTask = awaitedTask;
             this.Awaiter = awaitedTask.GetAwaiter();
         }
@@ -53,10 +49,9 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Initializes a new instance of the <see cref="TaskAwaiter"/> struct.
         /// </summary>
-        internal TaskAwaiter(CoyoteRuntime runtime, SystemCompiler.TaskAwaiter awaiter)
+        private TaskAwaiter(SystemTasks.Task awaitedTask, SystemCompiler.TaskAwaiter awaiter)
         {
-            this.Runtime = runtime;
+            this.AwaitedTask = awaitedTask;
-            this.AwaitedTask = null;
             this.Awaiter = awaiter;
         }
 
@@ -66,7 +61,11 @@ namespace Microsoft.Coyote.Interception
         [MethodImpl(MethodImplOptions.AggressiveInlining)]
         public void GetResult()
         {
-            this.Runtime?.OnWaitTask(this.AwaitedTask);
+            if (SynchronizationContext.Current is ControlledSynchronizationContext context)
+            {
+                context.Runtime?.OnWaitTask(this.AwaitedTask);
+            }
+
             this.Awaiter.GetResult();
         }
 
@@ -85,12 +84,24 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Wraps the specified task awaiter.
         /// </summary>
-        public static TaskAwaiter Wrap(SystemCompiler.TaskAwaiter awaiter) => new TaskAwaiter(null, awaiter);
+        public static TaskAwaiter Wrap(SystemCompiler.TaskAwaiter awaiter)
+        {
+            // Access the task being awaited through reflection.
+            var field = awaiter.GetType().GetField("m_task", BindingFlags.NonPublic | BindingFlags.Instance);
+            var awaitedTask = (Task)field?.GetValue(awaiter);
+            return new TaskAwaiter(awaitedTask, awaiter);
+        }
 
         /// <summary>
-        /// Wraps the specified task awaiter.
+        /// Wraps the specified generic task awaiter.
         /// </summary>
-        public static TaskAwaiter<TResult> Wrap<TResult>(SystemCompiler.TaskAwaiter<TResult> awaiter) => new TaskAwaiter<TResult>(null, awaiter);
+        public static TaskAwaiter<TResult> Wrap<TResult>(SystemCompiler.TaskAwaiter<TResult> awaiter)
+        {
+            // Access the generic task being awaited through reflection.
+            var field = awaiter.GetType().GetField("m_task", BindingFlags.NonPublic | BindingFlags.Instance);
+            var awaitedTask = (Task<TResult>)field?.GetValue(awaiter);
+            return new TaskAwaiter<TResult>(awaitedTask, awaiter);
+        }
     }
 
     /// <summary>
@@ -104,11 +115,6 @@ namespace Microsoft.Coyote.Interception
         // WARNING: The layout must remain the same, as the struct is used to access
         // the generic TaskAwaiter<> as TaskAwaiter.
 
-        /// <summary>
-        /// Responsible for controlling the execution of tasks during systematic testing.
-        /// </summary>
-        private readonly CoyoteRuntime Runtime;
-
         /// <summary>
         /// The task being awaited.
         /// </summary>
@@ -127,9 +133,8 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Initializes a new instance of the <see cref="TaskAwaiter{TResult}"/> struct.
         /// </summary>
-        internal TaskAwaiter(CoyoteRuntime runtime, SystemTasks.Task<TResult> awaitedTask)
+        internal TaskAwaiter(SystemTasks.Task<TResult> awaitedTask)
         {
-            this.Runtime = runtime;
             this.AwaitedTask = awaitedTask;
             this.Awaiter = awaitedTask.GetAwaiter();
         }
@@ -137,10 +142,9 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Initializes a new instance of the <see cref="TaskAwaiter{TResult}"/> struct.
         /// </summary>
-        internal TaskAwaiter(CoyoteRuntime runtime, SystemCompiler.TaskAwaiter<TResult> awaiter)
+        internal TaskAwaiter(SystemTasks.Task<TResult> awaitedTask, SystemCompiler.TaskAwaiter<TResult> awaiter)
         {
-            this.Runtime = runtime;
+            this.AwaitedTask = awaitedTask;
-            this.AwaitedTask = null;
             this.Awaiter = awaiter;
         }
 
@@ -150,7 +154,11 @@ namespace Microsoft.Coyote.Interception
         [MethodImpl(MethodImplOptions.AggressiveInlining)]
         public TResult GetResult()
         {
-            this.Runtime?.OnWaitTask(this.AwaitedTask);
+            if (SynchronizationContext.Current is ControlledSynchronizationContext context)
+            {
+                context.Runtime?.OnWaitTask(this.AwaitedTask);
+            }
+
             return this.Awaiter.GetResult();
         }
 

Source/Core/Interception/Threading/Tasks/ControlledTask.cs

@@ -405,13 +405,13 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Returns a <see cref="TaskAwaiter"/> for the specified <see cref="Task"/>.
         /// </summary>
-        public static TaskAwaiter GetAwaiter(Task task) => new TaskAwaiter(CoyoteRuntime.Current, task);
+        public static TaskAwaiter GetAwaiter(Task task) => new TaskAwaiter(task);
 
         /// <summary>
         /// Configures an awaiter used to await this task.
         /// </summary>
         public static ConfiguredTaskAwaitable ConfigureAwait(Task task, bool continueOnCapturedContext) =>
-            new ConfiguredTaskAwaitable(CoyoteRuntime.Current, task, continueOnCapturedContext);
+            new ConfiguredTaskAwaitable(task, continueOnCapturedContext);
     }
 
     /// <summary>
@@ -444,14 +444,13 @@ namespace Microsoft.Coyote.Interception
         /// <summary>
         /// Returns a <see cref="TaskAwaiter{TResult}"/> for the specified <see cref="Task{TResult}"/>.
         /// </summary>
-        public static TaskAwaiter<TResult> GetAwaiter(Task<TResult> task) =>
+        public static TaskAwaiter<TResult> GetAwaiter(Task<TResult> task) => new TaskAwaiter<TResult>(task);
-            new TaskAwaiter<TResult>(CoyoteRuntime.Current, task);
 
         /// <summary>
         /// Configures an awaiter used to await this task.
         /// </summary>
         public static ConfiguredTaskAwaitable<TResult> ConfigureAwait(Task<TResult> task, bool continueOnCapturedContext) =>
-            new ConfiguredTaskAwaitable<TResult>(CoyoteRuntime.Current, task, continueOnCapturedContext);
+            new ConfiguredTaskAwaitable<TResult>(task, continueOnCapturedContext);
 #pragma warning restore CA1000 // Do not declare static members on generic types
     }
 }

Source/Core/Runtime/CoyoteRuntime.cs

@@ -30,7 +30,8 @@ namespace Microsoft.Coyote.Runtime
     internal sealed class CoyoteRuntime : IDisposable
     {
         /// <summary>
-        /// Provides access to the runtime associated with each controlled thread.
+        /// Provides access to the runtime associated with each controlled thread, or null
+        /// if the current thread is not controlled.
         /// </summary>
         /// <remarks>
         /// In testing mode, each testing iteration uses a unique runtime instance. To safely
@@ -39,6 +40,17 @@ namespace Microsoft.Coyote.Runtime
         private static readonly ThreadLocal<CoyoteRuntime> ThreadLocalRuntime =
             new ThreadLocal<CoyoteRuntime>(false);
 
+        /// <summary>
+        /// Provides access to the runtime associated with each async local context, or null
+        /// if the current async local context has no associated runtime.
+        /// </summary>
+        /// <remarks>
+        /// In testing mode, each testing iteration uses a unique runtime instance. To safely
+        /// retrieve it from static methods, we store it in each controlled async local state.
+        /// </remarks>
+        private static readonly AsyncLocal<CoyoteRuntime> AsyncLocalRuntime =
+            new AsyncLocal<CoyoteRuntime>();
+
         /// <summary>
         /// Provides access to the operation executing on each controlled thread
         /// during systematic testing.
@@ -51,7 +63,7 @@ namespace Microsoft.Coyote.Runtime
         /// </summary>
         internal static CoyoteRuntime Current
         {
-            get => ThreadLocalRuntime.Value ?? RuntimeFactory.InstalledRuntime;
+            get => ThreadLocalRuntime.Value ?? AsyncLocalRuntime.Value ?? RuntimeFactory.InstalledRuntime;
         }
 
         /// <summary>
@@ -297,10 +309,11 @@ namespace Microsoft.Coyote.Runtime
                     // Update the current controlled thread with this runtime instance and executing
                     // operation, allowing future retrieval in the same controlled thread.
                     ThreadLocalRuntime.Value = this;
+                    AsyncLocalRuntime.Value = this.SchedulingPolicy is SchedulingPolicy.Fuzzing ? this : null;
                     ExecutingOperation.Value = op;
 
                     // Set the synchronization context to the controlled synchronization context.
-                    SynchronizationContext.SetSynchronizationContext(this.SyncContext);
+                    this.SetControlledSynchronizationContext();
 
                     this.StartOperation(op);
 
@@ -346,6 +359,7 @@ namespace Microsoft.Coyote.Runtime
                 {
                     // Clean the thread local state.
                     ExecutingOperation.Value = null;
+                    AsyncLocalRuntime.Value = null;
                     ThreadLocalRuntime.Value = null;
                 }
             });
@@ -401,10 +415,11 @@ namespace Microsoft.Coyote.Runtime
                     // Update the current controlled thread with this runtime instance and executing
                     // operation, allowing future retrieval in the same controlled thread.
                     ThreadLocalRuntime.Value = this;
+                    AsyncLocalRuntime.Value = this.SchedulingPolicy is SchedulingPolicy.Fuzzing ? this : null;
                     ExecutingOperation.Value = op;
 
                     // Set the synchronization context to the controlled synchronization context.
-                    SynchronizationContext.SetSynchronizationContext(this.SyncContext);
+                    this.SetControlledSynchronizationContext();
 
                     this.StartOperation(op);
 
@@ -425,6 +440,7 @@ namespace Microsoft.Coyote.Runtime
                 {
                     // Clean the thread local state.
                     ExecutingOperation.Value = null;
+                    AsyncLocalRuntime.Value = null;
                     ThreadLocalRuntime.Value = null;
                 }
             });
@@ -460,10 +476,11 @@ namespace Microsoft.Coyote.Runtime
                     // Update the current controlled thread with this runtime instance and executing
                     // operation, allowing future retrieval in the same controlled thread.
                     ThreadLocalRuntime.Value = this;
+                    AsyncLocalRuntime.Value = this.SchedulingPolicy is SchedulingPolicy.Fuzzing ? this : null;
                     ExecutingOperation.Value = op;
 
                     // Set the synchronization context to the controlled synchronization context.
-                    SynchronizationContext.SetSynchronizationContext(this.SyncContext);
+                    this.SetControlledSynchronizationContext();
 
                     this.StartOperation(op);
 
@@ -485,6 +502,7 @@ namespace Microsoft.Coyote.Runtime
                 {
                     // Clean the thread local state.
                     ExecutingOperation.Value = null;
+                    AsyncLocalRuntime.Value = null;
                     ThreadLocalRuntime.Value = null;
                 }
             });
@@ -648,7 +666,7 @@ namespace Microsoft.Coyote.Runtime
 
             if (task.IsFaulted)
             {
-                // Propagate the failing exception by rethrowing it.
+                // Propagate the failing exception by re-throwing it.
                 ExceptionDispatchInfo.Capture(task.Exception).Throw();
             }
 
@@ -669,7 +687,7 @@ namespace Microsoft.Coyote.Runtime
 
             if (task.IsFaulted)
             {
-                // Propagate the failing exception by rethrowing it.
+                // Propagate the failing exception by re-throwing it.
                 ExceptionDispatchInfo.Capture(task.Exception).Throw();
             }
 
@@ -737,17 +755,19 @@ namespace Microsoft.Coyote.Runtime
 #endif
         internal void OnWaitTask(Task task)
         {
-            if (!task.IsCompleted)
+            if (this.SchedulingPolicy is SchedulingPolicy.Systematic && !task.IsCompleted)
             {
-                if (this.SchedulingPolicy is SchedulingPolicy.Systematic)
+                if (!this.TaskMap.ContainsKey(task))
                 {
-                    var callerOp = this.GetExecutingOperation<TaskOperation>();
+                    this.NotifyUncontrolledTaskDetected(task.Id);
-                    this.WaitUntilTaskCompletes(callerOp, task);
-                }
-                else if (this.SchedulingPolicy is SchedulingPolicy.Fuzzing)
-                {
-                    this.DelayOperation();
                 }
+
+                var callerOp = this.GetExecutingOperation<TaskOperation>();
+                this.WaitUntilTaskCompletes(callerOp, task);
+            }
+            else if (this.SchedulingPolicy is SchedulingPolicy.Fuzzing)
+            {
+                this.DelayOperation();
             }
         }
 
@@ -786,7 +806,7 @@ namespace Microsoft.Coyote.Runtime
                     // Checks if the current operation is controlled by the runtime.
                     if (ExecutingOperation.Value is null)
                     {
-                        this.NotifyUncontrolledConcurrencyDetected();
+                        this.NotifyUncontrolledTaskDetected(Task.CurrentId);
                     }
                 }
 
@@ -940,7 +960,7 @@ namespace Microsoft.Coyote.Runtime
                 // Checks if the current operation is controlled by the runtime.
                 if (ExecutingOperation.Value is null)
                 {
-                    this.NotifyUncontrolledConcurrencyDetected();
+                    this.NotifyUncontrolledTaskDetected(Task.CurrentId);
                 }
 
                 // Checks if the scheduling steps bound has been reached.
@@ -978,7 +998,7 @@ namespace Microsoft.Coyote.Runtime
                 // Checks if the current operation is controlled by the runtime.
                 if (ExecutingOperation.Value is null)
                 {
-                    this.NotifyUncontrolledConcurrencyDetected();
+                    this.NotifyUncontrolledTaskDetected(Task.CurrentId);
                 }
 
                 // Checks if the scheduling steps bound has been reached.
@@ -1200,7 +1220,7 @@ namespace Microsoft.Coyote.Runtime
                 var op = ExecutingOperation.Value;
                 if (op is null)
                 {
-                    this.NotifyUncontrolledConcurrencyDetected();
+                    this.NotifyUncontrolledTaskDetected(Task.CurrentId);
                 }
 
                 return op.Equals(this.ScheduledOperation) && op is TAsyncOperation expected ? expected : default;
@@ -1566,9 +1586,9 @@ namespace Microsoft.Coyote.Runtime
         }
 
         /// <summary>
-        /// Checks if the currently executing operation is controlled by the runtime.
+        /// Notify that an uncontrolled task was detected.
         /// </summary>
-        private void NotifyUncontrolledConcurrencyDetected()
+        private void NotifyUncontrolledTaskDetected(int? taskId)
         {
             if (this.SchedulingPolicy is SchedulingPolicy.Systematic)
             {
@@ -1576,7 +1596,7 @@ namespace Microsoft.Coyote.Runtime
                 // uncontrolled task to ease the user debugging experience.
                 // Report the invalid operation and then throw it to fail the uncontrolled task. This will
                 // most likely crash the program, but we try to fail as cleanly and fast as possible.
-                string taskId = Task.CurrentId.HasValue ? Task.CurrentId.Value.ToString() : "<unknown>";
+                string id = taskId.HasValue ? taskId.Value.ToString() : "<unknown>";
                 string message = $"Detected task '{taskId}' that is not intercepted and controlled during " +
                     "testing, so it can interfere with the ability to reproduce bug traces.";
                 if (this.Configuration.IsConcurrencyFuzzingFallbackEnabled)
@@ -1752,6 +1772,12 @@ namespace Microsoft.Coyote.Runtime
             }
         }
 
+        /// <summary>
+        /// Sets the synchronization context to the controlled synchronization context.
+        /// </summary>
+        internal void SetControlledSynchronizationContext() =>
+            SynchronizationContext.SetSynchronizationContext(this.SyncContext);
+
         /// <summary>
         /// Forces the scheduler to terminate.
         /// </summary>

Source/Core/Runtime/Scheduling/ControlledSynchronizationContext.cs

@@ -14,7 +14,7 @@ namespace Microsoft.Coyote.Runtime
         /// <summary>
         /// Responsible for controlling the execution of operations during systematic testing.
         /// </summary>
-        private CoyoteRuntime Runtime;
+        internal CoyoteRuntime Runtime { get; private set; }
 
         /// <summary>
         /// Initializes a new instance of the <see cref="ControlledSynchronizationContext"/> class.

Source/Core/Specifications/SpecificationEngine.cs

@@ -309,7 +309,7 @@ namespace Microsoft.Coyote.Specifications
         }
 
         /// <summary>
-        /// Checks if a liveness monitor exceeded its threshold, and if yes, it reports an error.
+        /// Checks if a liveness monitor exceeded its threshold and, if yes, it reports an error.
         /// </summary>
         internal void CheckLivenessThresholdExceeded()
         {

Source/Test/Rewriting/AssemblyInfo.cs

@@ -0,0 +1,411 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using System.Reflection;
+using Microsoft.Coyote.Interception;
+using Microsoft.Coyote.IO;
+using Mono.Cecil;
+using Mono.Cecil.Cil;
+
+namespace Microsoft.Coyote.Rewriting
+{
+    /// <summary>
+    /// Contains information for an assembly that is being rewritten.
+    /// </summary>
+    internal sealed class AssemblyInfo : IDisposable
+    {
+        /// <summary>
+        /// The full name of the assembly.
+        /// </summary>
+        internal readonly string FullName;
+
+        /// <summary>
+        /// The name of the assembly.
+        /// </summary>
+        internal readonly string Name;
+
+        /// <summary>
+        /// The path to the assembly file.
+        /// </summary>
+        internal readonly string FilePath;
+
+        /// <summary>
+        /// The assembly definition.
+        /// </summary>
+        internal readonly AssemblyDefinition Definition;
+
+        /// <summary>
+        /// The assembly direct dependencies.
+        /// </summary>
+        private readonly HashSet<AssemblyInfo> Dependencies;
+
+        /// <summary>
+        /// The resolver of this assembly.
+        /// </summary>
+        private readonly IAssemblyResolver Resolver;
+
+        /// <summary>
+        /// The rewriting options.
+        /// </summary>
+        private readonly RewritingOptions Options;
+
+        /// <summary>
+        /// True if the assembly has been rewritten, else false.
+        /// </summary>
+        internal bool IsRewritten { get; private set; }
+
+        /// <summary>
+        /// True if the assembly has been disposed, else false.
+        /// </summary>
+        private bool IsDisposed;
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="AssemblyInfo"/> class.
+        /// </summary>
+        private AssemblyInfo(string name, string path, RewritingOptions options, AssemblyResolveEventHandler handler)
+        {
+            this.Name = name;
+            this.FilePath = path;
+            this.Dependencies = new HashSet<AssemblyInfo>();
+            this.Options = options;
+            this.IsRewritten = false;
+            this.IsDisposed = false;
+
+            // TODO: can we reuse it, or do we need a new one for each assembly?
+            var assemblyResolver = new DefaultAssemblyResolver();
+
+            // Add known search directories for resolving assemblies.
+            assemblyResolver.AddSearchDirectory(Path.GetDirectoryName(typeof(ControlledTask).Assembly.Location));
+            assemblyResolver.AddSearchDirectory(this.Options.AssembliesDirectory);
+            if (this.Options.DependencySearchPaths != null)
+            {
+                foreach (var dependencySearchPath in this.Options.DependencySearchPaths)
+                {
+                    assemblyResolver.AddSearchDirectory(dependencySearchPath);
+                }
+            }
+
+            // Add the assembly resolution error handler.
+            assemblyResolver.ResolveFailure += handler;
+
+            this.Resolver = assemblyResolver;
+            var readerParameters = new ReaderParameters()
+            {
+                AssemblyResolver = assemblyResolver,
+                ReadSymbols = this.IsSymbolFileAvailable()
+            };
+
+            this.Definition = AssemblyDefinition.ReadAssembly(this.FilePath, readerParameters);
+            this.FullName = this.Definition.FullName;
+        }
+
+        /// <summary>
+        /// Loads and returns the topological sorted list of unique assemblies to rewrite.
+        /// </summary>
+        internal static IEnumerable<AssemblyInfo> LoadAssembliesToRewrite(RewritingOptions options,
+            AssemblyResolveEventHandler handler)
+        {
+            // Add all explicitly requested assemblies.
+            var assemblies = new HashSet<AssemblyInfo>();
+            foreach (string path in options.AssemblyPaths)
+            {
+                if (!assemblies.Any(assembly => assembly.FilePath == path))
+                {
+                    var name = Path.GetFileName(path);
+                    if (options.IsAssemblyIgnored(name))
+                    {
+                        throw new InvalidOperationException($"Rewriting assembly '{name}' ({path}) that is in the ignore list.");
+                    }
+
+                    assemblies.Add(new AssemblyInfo(name, path, options, handler));
+                }
+            }
+
+            // Find direct dependencies to each assembly and load them, if the corresponding option is enabled.
+            foreach (var assembly in assemblies)
+            {
+                assembly.LoadDependencies(assemblies, handler);
+            }
+
+            // Validate that all assemblies are eligible for rewriting.
+            foreach (var assembly in assemblies)
+            {
+                assembly.ValidateAssembly();
+            }
+
+            return SortAssemblies(assemblies);
+        }
+
+        /// <summary>
+        /// Rewrites the assembly definition using the specified pass.
+        /// </summary>
+        internal void Rewrite(AssemblyRewriter pass)
+        {
+            Debug.WriteLine($"..... Applying the '{pass.GetType().Name}' pass");
+            foreach (var module in this.Definition.Modules)
+            {
+                Debug.WriteLine($"....... Module: {module.Name} ({module.FileName})");
+                pass.VisitModule(module);
+                foreach (var type in module.GetTypes())
+                {
+                    Debug.WriteLine($"......... Type: {type.FullName}");
+                    pass.VisitType(type);
+                    foreach (var field in type.Fields.ToArray())
+                    {
+                        Debug.WriteLine($"........... Field: {field.FullName}");
+                        pass.VisitField(field);
+                    }
+
+                    foreach (var method in type.Methods.ToArray())
+                    {
+                        if (method.Body is null)
+                        {
+                            continue;
+                        }
+
+                        Debug.WriteLine($"........... Method {method.FullName}");
+                        pass.VisitMethod(method);
+                        if (pass.ModifiedMethodBody)
+                        {
+                            AssemblyRewriter.FixInstructionOffsets(method);
+                            pass.ModifiedMethodBody = false;
+                        }
+                    }
+                }
+            }
+        }
+
+        /// <summary>
+        /// Writes the assembly to the specified output path.
+        /// </summary>
+        internal void Write(string outputPath)
+        {
+            var writerParameters = new WriterParameters()
+            {
+                WriteSymbols = this.IsSymbolFileAvailable(),
+                SymbolWriterProvider = new PortablePdbWriterProvider()
+            };
+
+            if (!string.IsNullOrEmpty(this.Options.StrongNameKeyFile))
+            {
+                using FileStream fs = File.Open(this.Options.StrongNameKeyFile, FileMode.Open);
+                writerParameters.StrongNameKeyPair = new StrongNameKeyPair(fs);
+            }
+
+            this.Definition.Write(outputPath, writerParameters);
+        }
+
+        /// <summary>
+        /// Applies the <see cref="RewritingSignatureAttribute"/> attribute to the assembly. This attribute
+        /// indicates that the assembly has been rewritten with the current version of Coyote and contains
+        /// a signature identifying the parameters used during binary rewriting of the assembly.
+        /// </summary>
+        internal void ApplyRewritingSignatureAttribute(Version rewriterVersion)
+        {
+            var signature = new AssemblySignature(this, this.Dependencies, rewriterVersion, this.Options);
+            var signatureHash = signature.ComputeHash();
+
+            CustomAttribute attribute = this.GetCustomAttribute(typeof(RewritingSignatureAttribute));
+            var versionAttributeArgument = new CustomAttributeArgument(
+                this.Definition.MainModule.ImportReference(typeof(string)), rewriterVersion.ToString());
+            var idAttributeArgument = new CustomAttributeArgument(
+                this.Definition.MainModule.ImportReference(typeof(string)), signatureHash);
+            if (attribute is null)
+            {
+                MethodReference attributeConstructor = this.Definition.MainModule.ImportReference(
+                    typeof(RewritingSignatureAttribute).GetConstructor(new Type[] { typeof(string), typeof(string) }));
+                attribute = new CustomAttribute(attributeConstructor);
+                attribute.ConstructorArguments.Add(versionAttributeArgument);
+                attribute.ConstructorArguments.Add(idAttributeArgument);
+                this.Definition.CustomAttributes.Add(attribute);
+            }
+            else
+            {
+                attribute.ConstructorArguments[0] = versionAttributeArgument;
+                attribute.ConstructorArguments[1] = idAttributeArgument;
+            }
+
+            this.IsRewritten = true;
+        }
+
+        /// <summary>
+        /// Checks if this assembly has been rewritten and, if yes, returns its version and signature.
+        /// </summary>
+        /// <returns>True if the assembly has been rewritten with the same signature, else false.</returns>
+        private bool IsAssemblyRewritten(out string version, out string signatureHash)
+        {
+            CustomAttribute attribute = this.GetCustomAttribute(typeof(RewritingSignatureAttribute));
+            if (attribute != null)
+            {
+                version = attribute.ConstructorArguments[0].Value as string;
+                signatureHash = attribute.ConstructorArguments[1].Value as string;
+                return true;
+            }
+
+            version = string.Empty;
+            signatureHash = string.Empty;
+            return false;
+        }
+
+        /// <summary>
+        /// Checks if the specified assembly is a mixed-mode assembly.
+        /// </summary>
+        /// <returns>True if the assembly only contains IL, else false.</returns>
+        private bool IsMixedModeAssembly() =>
+            this.Definition.Modules.Any(m => (m.Attributes & ModuleAttributes.ILOnly) is 0);
+
+        /// <summary>
+        /// Checks if the symbol file for the specified assembly is available.
+        /// </summary>
+        internal bool IsSymbolFileAvailable() => File.Exists(Path.ChangeExtension(this.FilePath, "pdb"));
+
+        /// <summary>
+        /// Returns the first found custom attribute with the specified type, if such an attribute
+        /// is applied to the assembly, else null.
+        /// </summary>
+        private CustomAttribute GetCustomAttribute(Type attributeType) =>
+            this.Definition.CustomAttributes.FirstOrDefault(
+                attr => attr.AttributeType.Namespace == attributeType.Namespace &&
+                attr.AttributeType.Name == attributeType.Name);
+
+        /// <summary>
+        /// Validates that the assembly can be rewritten.
+        /// </summary>
+        private void ValidateAssembly()
+        {
+            if (this.IsAssemblyRewritten(out string version, out string signatureHash))
+            {
+                // The assembly has been already rewritten so check if the signatures match.
+                var newVersion = Assembly.GetExecutingAssembly().GetName().Version;
+                var newSignature = new AssemblySignature(this, this.Dependencies, newVersion, this.Options);
+                var newSignatureHash = newSignature.ComputeHash();
+                if (version != newVersion.ToString())
+                {
+                    throw new InvalidOperationException(
+                        $"Assembly '{this.Name}' has been rewritten with a different coyote version.");
+                }
+                else if (signatureHash != newSignatureHash)
+                {
+                    throw new InvalidOperationException(
+                        $"Assembly '{this.Name}' has been rewritten with a different rewriting configuration.");
+                }
+
+                this.IsRewritten = true;
+            }
+            else if (this.IsMixedModeAssembly())
+            {
+                // Mono.Cecil does not support writing mixed-mode assemblies.
+                throw new InvalidOperationException($"Rewriting mixed-mode assembly '{this.Name}' is not supported.");
+            }
+        }
+
+        /// <summary>
+        /// Loads all dependent assemblies in the local assembly path.
+        /// </summary>
+        private void LoadDependencies(HashSet<AssemblyInfo> assemblies, AssemblyResolveEventHandler handler)
+        {
+            // Get the directory associated with this assembly.
+            var assemblyDir = Path.GetDirectoryName(this.FilePath);
+
+            // Perform a non-recursive depth-first search to find all dependencies.
+            var stack = new Stack<AssemblyInfo>();
+            stack.Push(this);
+            while (stack.Count > 0)
+            {
+                var assembly = stack.Pop();
+                foreach (var reference in assembly.Definition.Modules.SelectMany(module => module.AssemblyReferences))
+                {
+                    var fileName = reference.Name + ".dll";
+                    var path = Path.Combine(assemblyDir, fileName);
+                    if (File.Exists(path) && !this.Options.IsAssemblyIgnored(fileName))
+                    {
+                        AssemblyInfo dependency = assemblies.FirstOrDefault(assembly => assembly.FilePath == path);
+                        if (dependency is null && this.Options.IsRewritingDependencies)
+                        {
+                            var name = Path.GetFileName(path);
+                            dependency = new AssemblyInfo(name, path, this.Options, handler);
+                            stack.Push(dependency);
+                            assemblies.Add(dependency);
+                        }
+
+                        if (dependency != null)
+                        {
+                            this.Dependencies.Add(dependency);
+                        }
+                    }
+                }
+            }
+        }
+
+        /// <summary>
+        /// Sorts the specified assemblies in topological ordering.
+        /// </summary>
+        private static IEnumerable<AssemblyInfo> SortAssemblies(HashSet<AssemblyInfo> assemblies)
+        {
+            var sortedAssemblies = new List<AssemblyInfo>();
+
+            // Assemblies that have zero or visited dependencies.
+            var nextAssemblies = new HashSet<AssemblyInfo>(
+                assemblies.Where(assembly => assembly.Dependencies.Count is 0));
+
+            // Sort the assemblies in topological ordering.
+            while (nextAssemblies.Count > 0)
+            {
+                var nextAssembly = nextAssemblies.First();
+                nextAssemblies.Remove(nextAssembly);
+                sortedAssemblies.Add(nextAssembly);
+
+                // Add all assemblies that have not been sorted yet and have all their dependencies visited
+                // to the set of next assemblies to sort.
+                foreach (var assembly in assemblies.Where(assembly => !sortedAssemblies.Contains(assembly)))
+                {
+                    if (assembly.Dependencies.IsSubsetOf(sortedAssemblies))
+                    {
+                        nextAssemblies.Add(assembly);
+                    }
+                }
+            }
+
+            if (sortedAssemblies.Count != assemblies.Count)
+            {
+                // There are cycles in the assembly dependencies. This should normally never
+                // happen because C# does not allow cycles in assembly references.
+                throw new InvalidOperationException("Detected circular assembly dependencies.");
+            }
+
+            return sortedAssemblies;
+        }
+
+        /// <summary>
+        /// Determines whether the specified object is equal to the current object.
+        /// </summary>
+        public override bool Equals(object obj) => obj is AssemblyInfo info && this.FullName == info.FullName;
+
+        /// <summary>
+        /// Returns the hash code for this instance.
+        /// </summary>
+        public override int GetHashCode() => this.FullName.GetHashCode();
+
+        /// <summary>
+        /// Returns a string that represents the current assembly.
+        /// </summary>
+        public override string ToString() => this.FullName;
+
+        /// <summary>
+        /// Disposes the resources held by this object.
+        /// </summary>
+        public void Dispose()
+        {
+            if (!this.IsDisposed)
+            {
+                this.Definition?.Dispose();
+                this.Resolver?.Dispose();
+                this.IsDisposed = true;
+            }
+        }
+    }
+}

Source/Test/Rewriting/AssemblySignature.cs

@@ -0,0 +1,111 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using System.Runtime.Serialization;
+using System.Runtime.Serialization.Json;
+using System.Security.Cryptography;
+using System.Text;
+
+namespace Microsoft.Coyote.Rewriting
+{
+    /// <summary>
+    /// Signature identifying the parameters used during binary rewriting of an assembly.
+    /// </summary>
+    [DataContract]
+    internal class AssemblySignature
+    {
+        /// <summary>
+        /// The full name of the assembly.
+        /// </summary>
+        [DataMember]
+        internal readonly string FullName;
+
+        /// <summary>
+        /// The version of the binary rewriter.
+        /// </summary>
+        [DataMember]
+        internal readonly string Version;
+
+        /// <summary>
+        /// The assembly direct dependencies.
+        /// </summary>
+        [DataMember]
+        internal readonly IList<string> Dependencies;
+
+        /// <summary>
+        /// True if rewriting for concurrent collections is enabled, else false.
+        /// </summary>
+        [DataMember]
+        internal readonly bool IsRewritingConcurrentCollections;
+
+        /// <summary>
+        /// True if rewriting for data race checking is enabled, else false.
+        /// </summary>
+        [DataMember]
+        internal readonly bool IsDataRaceCheckingEnabled;
+
+        /// <summary>
+        /// True if rewriting dependent assemblies that are found in the same location is enabled, else false.
+        /// </summary>
+        [DataMember]
+        internal readonly bool IsRewritingDependencies;
+
+        /// <summary>
+        /// True if rewriting of unit test methods is enabled, else false.
+        /// </summary>
+        [DataMember]
+        internal readonly bool IsRewritingUnitTests;
+
+        /// <summary>
+        /// True if rewriting threads as controlled tasks.
+        /// </summary>
+        [DataMember]
+        internal readonly bool IsRewritingThreads;
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="AssemblySignature"/> class.
+        /// </summary>
+        internal AssemblySignature(AssemblyInfo assembly, HashSet<AssemblyInfo> dependencies,
+            Version rewriterVersion, RewritingOptions options)
+        {
+            this.FullName = assembly.FullName;
+            this.Version = rewriterVersion.ToString();
+            this.Dependencies = new List<string>(dependencies.Select(dependency => dependency.FullName));
+            this.IsRewritingConcurrentCollections = options.IsRewritingConcurrentCollections;
+            this.IsDataRaceCheckingEnabled = options.IsDataRaceCheckingEnabled;
+            this.IsRewritingDependencies = options.IsRewritingDependencies;
+            this.IsRewritingUnitTests = options.IsRewritingUnitTests;
+            this.IsRewritingThreads = options.IsRewritingThreads;
+        }
+
+        /// <summary>
+        /// Computes the hash of the signature.
+        /// </summary>
+        internal string ComputeHash()
+        {
+            using var stream = new MemoryStream();
+            var serializer = new DataContractJsonSerializer(typeof(AssemblySignature));
+            serializer.WriteObject(stream, this);
+            var data = stream.GetBuffer();
+
+            // Compute the SHA256 hash.
+            using (SHA256 sha256Hash = SHA256.Create())
+            {
+                data = sha256Hash.ComputeHash(data);
+            }
+
+            // Format each byte of the hashed data as a hexadecimal string.
+            var sb = new StringBuilder();
+            foreach (var b in data)
+            {
+                sb.Append(b.ToString("x2"));
+            }
+
+            return sb.ToString();
+        }
+    }
+}

Source/Test/Rewriting/Attributes.cs

@@ -6,23 +6,33 @@ using System;
 namespace Microsoft.Coyote.Rewriting
 {
     /// <summary>
-    /// Attribute for checking if an assembly has been rewritten by Coyote. If this attribute
+    /// Attribute that contains a signature identifying the parameters used during
-    /// is applied to an assembly, it denotes that the assembly has been rewritten.
+    /// binary rewriting of an assembly.
     /// </summary>
+    /// <remarks>
+    /// If this attribute is applied to an assembly manifest, it denotes that the
+    /// assembly has been rewritten.
+    /// </remarks>
     [AttributeUsage(AttributeTargets.Assembly)]
-    public sealed class IsAssemblyRewrittenAttribute : Attribute
+    public sealed class RewritingSignatureAttribute : Attribute
     {
         /// <summary>
-        /// The version of Coyote used for the rewritting.
+        /// The version of Coyote used for the rewriting.
         /// </summary>
         public readonly string Version;
 
         /// <summary>
-        /// Initializes a new instance of the <see cref="IsAssemblyRewrittenAttribute"/> class.
+        /// Signature identifying parameters used during rewriting.
         /// </summary>
-        public IsAssemblyRewrittenAttribute(string version)
+        public readonly string Signature;
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="RewritingSignatureAttribute"/> class.
+        /// </summary>
+        public RewritingSignatureAttribute(string version, string signature)
         {
             this.Version = version;
+            this.Signature = signature;
         }
     }
 }

Source/Test/Rewriting/Passes/AssemblyRewriter.cs

@@ -3,6 +3,7 @@
 
 using System;
 using System.Collections.Generic;
+using System.IO;
 using System.Linq;
 using Microsoft.Coyote.IO;
 using Mono.Cecil;
@@ -31,10 +32,9 @@ namespace Microsoft.Coyote.Rewriting
         protected TypeDefinition TypeDef { get; private set; }
 
         /// <summary>
-        /// List of assembly strong names of the assemblies that we are going to rewrite
+        /// The set of assemblies that are being rewritten.
-        /// so we know what the scope of the rewrite operation is.
         /// </summary>
-        public HashSet<string> AssemblyNameScope { get; internal set; }
+        protected IEnumerable<AssemblyInfo> RewrittenAssemblies { get; private set; }
 
         /// <summary>
         /// The current method being transformed.
@@ -64,8 +64,9 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="AssemblyRewriter"/> class.
         /// </summary>
-        protected AssemblyRewriter(ILogger logger)
+        protected AssemblyRewriter(IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
         {
+            this.RewrittenAssemblies = rewrittenAssemblies;
             this.Logger = logger;
         }
 
@@ -173,7 +174,7 @@ namespace Microsoft.Coyote.Rewriting
             TypeReference declaringType = this.RewriteDeclaringTypeReference(method);
             var resolvedType = Resolve(declaringType);
 
-            if (resolvedMethod == null)
+            if (resolvedMethod is null)
             {
                 // Check if this method signature has been rewritten, find the method by same name,
                 // but with newly rewritten parameter types (note: signature does not include return type
@@ -202,11 +203,10 @@ namespace Microsoft.Coyote.Rewriting
                 return result;
             }
 
-            if (resolvedMethod == null)
+            if (resolvedMethod is null)
             {
-                // print warning
+                // TODO: do we need to return the resolved method here?
                 this.TryResolve(method, out resolvedMethod);
-                // try and continue...
                 return method;
             }
 
@@ -511,7 +511,7 @@ namespace Microsoft.Coyote.Rewriting
             return result;
         }
 
-        public static TypeReference MakeGenericType(TypeReference self, params TypeReference[] arguments)
+        protected static TypeReference MakeGenericType(TypeReference self, params TypeReference[] arguments)
         {
             if (self.GenericParameters.Count != arguments.Length)
             {
@@ -527,7 +527,7 @@ namespace Microsoft.Coyote.Rewriting
             return instance;
         }
 
-        public static MethodReference MakeGenericMethod(MethodReference self, params TypeReference[] arguments)
+        protected static MethodReference MakeGenericMethod(MethodReference self, params TypeReference[] arguments)
         {
             if (self.GenericParameters.Count != arguments.Length)
             {
@@ -543,6 +543,18 @@ namespace Microsoft.Coyote.Rewriting
             return instance;
         }
 
+        /// <summary>
+        /// Returns the parameter type that is at the specified index of the given <see cref="GenericInstanceType"/>.
+        /// </summary>
+        /// <remarks>
+        /// The index is of the form '!N' where N is the index of the parameter in the generic type.
+        /// </remarks>
+        protected static TypeReference GetGenericParameterTypeFromNamedIndex(GenericInstanceType genericType, string namedIndex)
+        {
+            int index = int.Parse(namedIndex.Split('!')[1]);
+            return genericType.GenericArguments[index].GetElementType();
+        }
+
         /// <summary>
         /// Fixes the instruction offsets of the specified method.
         /// </summary>
@@ -593,6 +605,32 @@ namespace Microsoft.Coyote.Rewriting
             return name;
         }
 
+        /// <summary>
+        /// Checks if the specified type is foreign.
+        /// </summary>
+        protected bool IsForeignType(TypeDefinition type)
+        {
+            if (type is null || this.Module == type.Module)
+            {
+                return false;
+            }
+
+            // Any type from the Coyote assemblies is not a foreign type.
+            string module = Path.GetFileName(type.Module.FileName);
+            if (module is "Microsoft.Coyote.dll" || module is "Microsoft.Coyote.Test.dll")
+            {
+                return false;
+            }
+
+            // Any type from a assembly being rewritten is not a foreign type.
+            if (this.RewrittenAssemblies.Any(assembly => assembly.FilePath == type.Module.FileName))
+            {
+                return false;
+            }
+
+            return true;
+        }
+
         /// <summary>
         /// Replaces the existing instruction with a new instruction and fixes up any
         /// branch references to the old instruction so they point to the new instruction.

Source/Test/Rewriting/Passes/ConcurrentCollectionRewriter.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System.Collections.Generic;
 using Microsoft.Coyote.Interception;
 using Microsoft.Coyote.IO;
 using Mono.Cecil;
@@ -16,8 +17,8 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="ConcurrentCollectionRewriter"/> class.
         /// </summary>
-        internal ConcurrentCollectionRewriter(ILogger logger)
+        internal ConcurrentCollectionRewriter(IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
-            : base(logger)
+            : base(rewrittenAssemblies, logger)
         {
         }
 

Source/Test/Rewriting/Passes/DataRaceCheckingRewriter.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System.Collections.Generic;
 using Microsoft.Coyote.Interception;
 using Microsoft.Coyote.IO;
 using Mono.Cecil;
@@ -13,8 +14,8 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="DataRaceCheckingRewriter"/> class.
         /// </summary>
-        internal DataRaceCheckingRewriter(ILogger logger)
+        internal DataRaceCheckingRewriter(IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
-            : base(logger)
+            : base(rewrittenAssemblies, logger)
         {
         }
 

Source/Test/Rewriting/Passes/ExceptionFilterRewriter.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System.Collections.Generic;
 using System.Linq;
 using System.Threading;
 using Microsoft.Coyote.IO;
@@ -24,8 +25,8 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="ExceptionFilterRewriter"/> class.
         /// </summary>
-        internal ExceptionFilterRewriter(ILogger logger)
+        internal ExceptionFilterRewriter(IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
-            : base(logger)
+            : base(rewrittenAssemblies, logger)
         {
         }
 

Source/Test/Rewriting/Passes/InterAssemblyInvocationRewriter.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System.Collections.Generic;
 using System.IO;
 using System.Linq;
 using Microsoft.Coyote.IO;
@@ -19,8 +20,8 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="InterAssemblyInvocationRewriter"/> class.
         /// </summary>
-        internal InterAssemblyInvocationRewriter(ILogger log)
+        internal InterAssemblyInvocationRewriter(IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
-            : base(log)
+            : base(rewrittenAssemblies, logger)
         {
         }
 
@@ -82,15 +83,25 @@ namespace Microsoft.Coyote.Rewriting
                     else if (methodReference.Name is "GetAwaiter" &&
                         IsTaskAwaiterType(methodReference.ReturnType.Resolve()))
                     {
-                        var declaringType = methodReference.DeclaringType;
+                        var returnType = methodReference.ReturnType;
                         TypeDefinition providerType = this.Module.ImportReference(typeof(ControlledTasks.TaskAwaiter)).Resolve();
                         MethodReference wrapMethod = null;
-                        if (declaringType is GenericInstanceType gt)
+                        if (returnType is GenericInstanceType rgt)
                         {
-                            MethodDefinition genericMethod = providerType.Methods.FirstOrDefault(m => m.Name == "Wrap" && m.HasGenericParameters);
+                            TypeReference argType;
-                            MethodReference wrapReference = this.Module.ImportReference(genericMethod);
+                            if (methodReference.DeclaringType is GenericInstanceType dgt)
+                            {
+                                var returnArgType = rgt.GenericArguments.FirstOrDefault().GetElementType();
+                                argType = GetGenericParameterTypeFromNamedIndex(dgt, returnArgType.FullName);
+                            }
+                            else
+                            {
+                                argType = rgt.GenericArguments.FirstOrDefault().GetElementType();
+                            }
 
-                            TypeReference argType = gt.GenericArguments.FirstOrDefault().GetElementType();
+                            MethodDefinition genericMethod = providerType.Methods.FirstOrDefault(
+                                m => m.Name == "Wrap" && m.HasGenericParameters);
+                            MethodReference wrapReference = this.Module.ImportReference(genericMethod);
                             wrapMethod = MakeGenericMethod(wrapReference, argType);
                         }
                         else
@@ -118,25 +129,6 @@ namespace Microsoft.Coyote.Rewriting
             return instruction;
         }
 
-        /// <summary>
-        /// Checks if the specified type is foreign.
-        /// </summary>
-        private bool IsForeignType(TypeDefinition type)
-        {
-            if (type is null || this.Module == type.Module)
-            {
-                return false;
-            }
-
-            string module = Path.GetFileName(type.Module.FileName);
-            if (module is "Microsoft.Coyote.dll" || module is "Microsoft.Coyote.Test.dll")
-            {
-                return false;
-            }
-
-            return true;
-        }
-
         /// <summary>
         /// Checks if the specified type is a task type.
         /// </summary>

Source/Test/Rewriting/Passes/MSTestRewriter.cs

@@ -22,8 +22,8 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="MSTestRewriter"/> class.
         /// </summary>
-        internal MSTestRewriter(Configuration configuration, ILogger logger)
+        internal MSTestRewriter(Configuration configuration, IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
-            : base(logger)
+            : base(rewrittenAssemblies, logger)
         {
             this.Configuration = configuration;
         }

Source/Test/Rewriting/Passes/MonitorRewriter.cs

@@ -2,6 +2,7 @@
 // Licensed under the MIT License.
 
 using System;
+using System.Collections.Generic;
 using Microsoft.Coyote.Interception;
 using Microsoft.Coyote.IO;
 using Mono.Cecil;
@@ -26,8 +27,8 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="MonitorRewriter"/> class.
         /// </summary>
-        internal MonitorRewriter(ILogger logger)
+        internal MonitorRewriter(IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
-            : base(logger)
+            : base(rewrittenAssemblies, logger)
         {
         }
 

Source/Test/Rewriting/Passes/TaskRewriter.cs

@@ -34,8 +34,8 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="TaskRewriter"/> class.
         /// </summary>
-        internal TaskRewriter(ILogger logger)
+        internal TaskRewriter(IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
-            : base(logger)
+            : base(rewrittenAssemblies, logger)
         {
         }
 

Source/Test/Rewriting/Passes/ThreadingRewriter.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System.Collections.Generic;
 using Microsoft.Coyote.Interception;
 using Microsoft.Coyote.IO;
 using Mono.Cecil;
@@ -18,8 +19,8 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="ThreadingRewriter"/> class.
         /// </summary>
-        internal ThreadingRewriter(ILogger logger)
+        internal ThreadingRewriter(IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
-            : base(logger)
+            : base(rewrittenAssemblies, logger)
         {
         }
 

Source/Test/Rewriting/Passes/UncontrolledInvocationRewriter.cs

@@ -1,6 +1,7 @@
 // Copyright (c) Microsoft Corporation.
 // Licensed under the MIT License.
 
+using System.Collections.Generic;
 using System.IO;
 using System.Linq;
 using Microsoft.Coyote.IO;
@@ -18,8 +19,8 @@ namespace Microsoft.Coyote.Rewriting
         /// <summary>
         /// Initializes a new instance of the <see cref="UncontrolledInvocationRewriter"/> class.
         /// </summary>
-        internal UncontrolledInvocationRewriter(ILogger log)
+        internal UncontrolledInvocationRewriter(IEnumerable<AssemblyInfo> rewrittenAssemblies, ILogger logger)
-            : base(log)
+            : base(rewrittenAssemblies, logger)
         {
         }
 

Source/Test/Rewriting/RewritingEngine.cs

@@ -4,10 +4,8 @@
 using System;
 using System.Collections.Generic;
 using System.IO;
-using System.Linq;
 using System.Reflection;
-using System.Text;
+using System.Runtime.ExceptionServices;
-using System.Text.RegularExpressions;
 using System.Threading.Tasks;
 using Microsoft.ApplicationInsights;
 using Microsoft.ApplicationInsights.Channel;
@@ -16,7 +14,6 @@ using Microsoft.ApplicationInsights.Extensibility;
 using Microsoft.Coyote.Interception;
 using Microsoft.Coyote.IO;
 using Mono.Cecil;
-using Mono.Cecil.Cil;
 
 namespace Microsoft.Coyote.Rewriting
 {
@@ -47,42 +44,15 @@ namespace Microsoft.Coyote.Rewriting
         /// </summary>
         private readonly Configuration Configuration;
 
-        /// <summary>
-        /// List of assemblies that are not allowed to be rewritten.
-        /// </summary>
-        private readonly Regex DisallowedAssemblies;
-
-        /// <summary>
-        /// Simple cache to reduce redundant warnings.
-        /// </summary>
-        private readonly HashSet<string> ResolveWarnings = new HashSet<string>();
-
-        private readonly string[] DefaultDisallowedList = new string[]
-        {
-            @"Newtonsoft\.Json\.dll",
-            @"Microsoft\.Coyote\.dll",
-            @"Microsoft\.Coyote.Test\.dll",
-            @"Microsoft\.VisualStudio\.TestPlatform.*",
-            @"Microsoft\.TestPlatform.*",
-            @"System\.Private\.CoreLib\.dll",
-            @"mscorlib\.dll"
-        };
-
         /// <summary>
         /// List of passes applied while rewriting.
         /// </summary>
         private readonly List<AssemblyRewriter> RewritingPasses;
 
         /// <summary>
-        /// Map from assembly name to full name definition of the rewritten assemblies.
+        /// Simple cache to reduce redundant warnings.
         /// </summary>
-        private readonly Dictionary<string, AssemblyNameDefinition> RewrittenAssemblies;
+        private readonly HashSet<string> ResolveWarnings;
-
-        /// <summary>
-        /// List of assembly names to be rewritten, these are strong names like:
-        /// "Microsoft.AspNetCore.Mvc.Core, Version=5.0.0.0, Culture=neutral, PublicKeyToken=adb9793829ddae60".
-        /// </summary>
-        private HashSet<string> AssemblyNameScope = new HashSet<string>();
 
         /// <summary>
         /// The installed logger.
@@ -90,117 +60,35 @@ namespace Microsoft.Coyote.Rewriting
         private readonly ILogger Logger;
 
         /// <summary>
-        /// The profiler.
+        /// The installed profiler.
         /// </summary>
         private readonly Profiler Profiler;
 
         /// <summary>
         /// Initializes a new instance of the <see cref="RewritingEngine"/> class.
         /// </summary>
-        /// <param name="configuration">The test configuration to use when rewriting unit tests.</param>
+        private RewritingEngine(RewritingOptions options, Configuration configuration, ILogger logger, Profiler profiler)
-        /// <param name="options">The <see cref="RewritingOptions"/> for this rewriter.</param>
-        private RewritingEngine(Configuration configuration, RewritingOptions options)
         {
+            this.Options = options.Sanitize();
             this.Configuration = configuration;
-            this.Options = options;
+            this.RewritingPasses = new List<AssemblyRewriter>();
-            this.Logger = options.Logger ?? new ConsoleLogger() { LogLevel = options.LogLevel };
+            this.ResolveWarnings = new HashSet<string>();
-            this.Profiler = new Profiler();
+            this.Logger = logger;
-
+            this.Profiler = profiler;
-            this.RewrittenAssemblies = new Dictionary<string, AssemblyNameDefinition>();
-            var ignoredAssemblies = options.IgnoredAssemblies ?? Array.Empty<string>();
-            StringBuilder combined = new StringBuilder();
-            foreach (var e in this.DefaultDisallowedList.Concat(ignoredAssemblies))
-            {
-                combined.Append(combined.Length is 0 ? "(" : "|");
-                combined.Append(e);
-            }
-
-            combined.Append(')');
-            try
-            {
-                this.DisallowedAssemblies = new Regex(combined.ToString());
-            }
-            catch (Exception ex)
-            {
-                throw new Exception("DisallowedAssemblies not a valid regular expression\n" + ex.Message);
-            }
-
-            this.RewritingPasses = new List<AssemblyRewriter>()
-            {
-                new TaskRewriter(this.Logger),
-                new MonitorRewriter(this.Logger),
-                new ExceptionFilterRewriter(this.Logger)
-            };
-
-            if (this.Options.IsRewritingThreads)
-            {
-                this.RewritingPasses.Add(new ThreadingRewriter(this.Logger));
-            }
-
-            if (this.Options.IsRewritingConcurrentCollections)
-            {
-                this.RewritingPasses.Add(new ConcurrentCollectionRewriter(this.Logger));
-            }
-
-            if (this.Options.IsDataRaceCheckingEnabled)
-            {
-                this.RewritingPasses.Add(new DataRaceCheckingRewriter(this.Logger));
-            }
-
-            if (this.Options.IsRewritingUnitTests)
-            {
-                // We are running this pass last, as we are rewriting the original method, and
-                // we need the other rewriting passes to happen before this pass.
-                this.RewritingPasses.Add(new MSTestRewriter(this.Configuration, this.Logger));
-            }
-
-            this.RewritingPasses.Add(new InterAssemblyInvocationRewriter(this.Logger));
-            this.RewritingPasses.Add(new UncontrolledInvocationRewriter(this.Logger));
-
-            // expand folder
-            if (this.Options.AssemblyPaths is null || this.Options.AssemblyPaths.Count is 0)
-            {
-                // Expand to include all .dll files in AssemblyPaths.
-                foreach (var file in Directory.GetFiles(this.Options.AssembliesDirectory, "*.dll"))
-                {
-                    if (this.IsDisallowed(Path.GetFileName(file)))
-                    {
-                        this.Options.AssemblyPaths.Add(file);
-                    }
-                    else
-                    {
-                        Debug.WriteLine("Skipping " + file);
-                    }
-                }
-            }
         }
 
         /// <summary>
         /// Runs the engine using the specified rewriting options.
         /// </summary>
-        public static void Run(Configuration configuration, RewritingOptions options)
+        internal static void Run(RewritingOptions options, Configuration configuration, Profiler profiler)
         {
-            if (string.IsNullOrEmpty(options.AssembliesDirectory))
+            var logger = new ConsoleLogger() { LogLevel = configuration.LogLevel };
-            {
+            var engine = new RewritingEngine(options, configuration, logger, profiler);
-                throw new Exception("Please provide RewritingOptions.AssembliesDirectory");
-            }
-
-            if (string.IsNullOrEmpty(options.OutputDirectory))
-            {
-                throw new Exception("Please provide RewritingOptions.OutputDirectory");
-            }
-
-            if (options.AssemblyPaths is null || options.AssemblyPaths.Count is 0)
-            {
-                throw new Exception("Please provide RewritingOptions.AssemblyPaths");
-            }
-
-            var engine = new RewritingEngine(configuration, options);
             engine.Run();
         }
 
         /// <summary>
-        /// Runs the engine.
+        /// Runs the rewriting engine.
         /// </summary>
         private void Run()
         {
@@ -209,202 +97,106 @@ namespace Microsoft.Coyote.Rewriting
             // Create the output directory and copy any necessary files.
             string outputDirectory = this.CreateOutputDirectoryAndCopyFiles();
 
-            // Create list of all assemblies we need to transform.
+            try
-            this.AssemblyNameScope = new HashSet<string>();
-            var list = new List<string>();
-            foreach (var pair in this.FindUniqueAssemblies())
             {
-                list.Add(pair.Item1);
+                // Get the set of assemblies to rewrite.
-                this.AssemblyNameScope.Add(pair.Item2);
+                var assemblies = AssemblyInfo.LoadAssembliesToRewrite(this.Options, this.OnResolveAssemblyFailure);
-            }
+                this.InitializeRewritingPasses(assemblies);
-
+                foreach (var assembly in assemblies)
-            int errors = 0;
-
-            foreach (var assemblyPath in list)
-            {
-                try
                 {
-                    this.RewriteAssembly(assemblyPath, outputDirectory);
+                    string outputPath = Path.Combine(outputDirectory, assembly.Name);
-                }
+                    this.RewriteAssembly(assembly, outputPath);
-                catch (Exception ex)
-                {
-                    if (!this.Options.IsReplacingAssemblies)
-                    {
-                        // Make sure to copy the original assembly to avoid any corruptions.
-                        CopyFile(assemblyPath, outputDirectory);
-                    }
-
-                    if (ex is AggregateException ae && ae.InnerException != null)
-                    {
-                        this.Logger.WriteLine(LogSeverity.Error, ae.InnerException.Message);
-                    }
-                    else
-                    {
-                        this.Logger.WriteLine(LogSeverity.Error, ex.Message);
-                    }
-
-                    if (this.Configuration.IsDebugVerbosityEnabled)
-                    {
-                        this.Logger.WriteLine(LogSeverity.Error, ex.StackTrace);
-                    }
-
-                    errors++;
                 }
             }
-
+            catch (Exception ex)
-            if (errors is 0 && this.Options.IsReplacingAssemblies)
             {
-                // If we are replacing the original assemblies, then delete the temporary output directory.
+                ExceptionDispatchInfo.Capture(ex).Throw();
-                Directory.Delete(outputDirectory, true);
             }
-
+            finally
-            this.Profiler.StopMeasuringExecutionTime();
-            Console.WriteLine($". Done rewriting in {this.Profiler.Results()} sec");
-        }
-
-        /// <summary>
-        /// Recursively find all assemblies that need to be rewritten as defined in the options.
-        /// If the options IsRewritingDependencies is true then find all dependent assemblies also.
-        /// </summary>
-        /// <returns>All discovered assemblies and their strong names.</returns>
-        private IEnumerable<Tuple<string, string>> FindUniqueAssemblies()
-        {
-            HashSet<string> unique = new HashSet<string>();
-            // Rewrite the assembly files to the output directory.
-            foreach (string assemblyPath in this.Options.AssemblyPaths)
             {
-                foreach (var pair in this.FindAllDependencies(assemblyPath, unique))
+                if (this.Options.IsReplacingAssemblies())
                 {
-                    yield return pair;
+                    // If we are replacing the original assemblies, then delete the temporary output directory.
+                    Directory.Delete(outputDirectory, true);
                 }
+
+                this.Profiler.StopMeasuringExecutionTime();
             }
         }
 
         /// <summary>
-        /// Recursively find all unique dependent assemblies in local assembly path.
+        /// Initializes the passes to run during rewriting.
         /// </summary>
-        /// <param name="assemblyPath">The assembly to analyze.</param>
+        private void InitializeRewritingPasses(IEnumerable<AssemblyInfo> assemblies)
-        /// <param name="visited">Set of assemblies already visited.</param>
-        /// <returns>The newly discovered dependent assemblies.</returns>
-        private IEnumerable<Tuple<string, string>> FindAllDependencies(string assemblyPath, HashSet<string> visited)
         {
-            using var assemblyResolver = this.GetAssemblyResolver();
+            this.RewritingPasses.Add(new TaskRewriter(assemblies, this.Logger));
-            var readParams = new ReaderParameters()
+            this.RewritingPasses.Add(new MonitorRewriter(assemblies, this.Logger));
+            this.RewritingPasses.Add(new ExceptionFilterRewriter(assemblies, this.Logger));
+
+            if (this.Options.IsRewritingThreads)
             {
-                AssemblyResolver = assemblyResolver,
+                this.RewritingPasses.Add(new ThreadingRewriter(assemblies, this.Logger));
-                ReadSymbols = IsSymbolFileAvailable(assemblyPath)
-            };
-
-            using (var assembly = AssemblyDefinition.ReadAssembly(assemblyPath, readParams))
-            {
-                if (!visited.Contains(assemblyPath))
-                {
-                    visited.Add(assemblyPath);
-                    yield return new Tuple<string, string>(assemblyPath, assembly.FullName);
-                }
-
-                if (this.Options.IsRewritingDependencies)
-                {
-                    foreach (var pair in this.FindLocalDependencies(assemblyPath, assembly))
-                    {
-                        if (!visited.Contains(pair.Item1))
-                        {
-                            visited.Add(pair.Item1);
-                            yield return pair;
-
-                            // recurrse!
-                            foreach (var child in this.FindAllDependencies(pair.Item1, visited))
-                            {
-                                yield return child;
-                            }
-                        }
-                    }
-                }
             }
+
+            if (this.Options.IsRewritingConcurrentCollections)
+            {
+                this.RewritingPasses.Add(new ConcurrentCollectionRewriter(assemblies, this.Logger));
+            }
+
+            if (this.Options.IsDataRaceCheckingEnabled)
+            {
+                this.RewritingPasses.Add(new DataRaceCheckingRewriter(assemblies, this.Logger));
+            }
+
+            if (this.Options.IsRewritingUnitTests)
+            {
+                // We are running this pass last, as we are rewriting the original method, and
+                // we need the other rewriting passes to happen before this pass.
+                this.RewritingPasses.Add(new MSTestRewriter(this.Configuration, assemblies, this.Logger));
+            }
+
+            this.RewritingPasses.Add(new InterAssemblyInvocationRewriter(assemblies, this.Logger));
+            this.RewritingPasses.Add(new UncontrolledInvocationRewriter(assemblies, this.Logger));
         }
 
         /// <summary>
-        /// Rewrites the specified assembly definition.
+        /// Rewrites the specified assembly.
         /// </summary>
-        private void RewriteAssembly(string assemblyPath, string outputDirectory)
+        private void RewriteAssembly(AssemblyInfo assembly, string outputPath)
         {
-            string assemblyName = Path.GetFileName(assemblyPath);
+            try
-            if (this.IsDisallowed(assemblyName))
             {
-                throw new InvalidOperationException($"Rewriting the '{assemblyName}' assembly ({assemblyPath}) is not allowed.");
+                this.Logger.WriteLine($"... Rewriting the '{assembly.Name}' assembly ({assembly.FullName})");
-            }
+                if (assembly.IsRewritten)
-            else if (this.RewrittenAssemblies.ContainsKey(Path.GetFileNameWithoutExtension(assemblyPath)))
-            {
-                // The assembly is already rewritten, so skip it.
-                return;
-            }
-
-            string outputPath = Path.Combine(outputDirectory, assemblyName);
-
-            using var assemblyResolver = this.GetAssemblyResolver();
-            var readParams = new ReaderParameters()
-            {
-                AssemblyResolver = assemblyResolver,
-                ReadSymbols = IsSymbolFileAvailable(assemblyPath)
-            };
-
-            using (var assembly = AssemblyDefinition.ReadAssembly(assemblyPath, readParams))
-            {
-                this.Logger.WriteLine($"... Rewriting the '{assemblyName}' assembly ({assembly.FullName})");
-
-                this.RewrittenAssemblies[assembly.Name.Name] = assembly.Name;
-
-                if (IsAssemblyRewritten(assembly))
                 {
-                    // The assembly has been already rewritten by this version of Coyote, so skip it.
+                    this.Logger.WriteLine($"..... Skipping as assembly is already rewritten with matching signature");
-                    this.Logger.WriteLine(LogSeverity.Warning, $"..... Skipping assembly with reason: already rewritten by Coyote v{GetAssemblyRewritterVersion()}");
-                    return;
-                }
-                else if (IsMixedModeAssembly(assembly))
-                {
-                    // Mono.Cecil does not support writing mixed-mode assemblies.
-                    this.Logger.WriteLine(LogSeverity.Warning, $"..... Skipping assembly with reason: rewriting a mixed-mode assembly is not supported");
                     return;
                 }
 
-                this.FixAssemblyReferences(assembly);
+                // Traverse the assembly to apply each rewriting pass.
-
-                ApplyIsAssemblyRewrittenAttribute(assembly);
                 foreach (var pass in this.RewritingPasses)
                 {
-                    // Traverse the assembly to apply each rewriting pass.
+                    assembly.Rewrite(pass);
-                    Debug.WriteLine($"..... Applying the '{pass.GetType().Name}' pass");
-                    pass.AssemblyNameScope = this.AssemblyNameScope;
-                    foreach (var module in assembly.Modules)
-                    {
-                        RewriteModule(module, pass);
-                    }
                 }
 
+                // Apply the rewriting signature to the assembly metadata.
+                assembly.ApplyRewritingSignatureAttribute(GetAssemblyRewriterVersion());
+
                 // Write the binary in the output path with portable symbols enabled.
-                this.Logger.WriteLine($"... Writing the modified '{assemblyName}' assembly to " +
+                this.Logger.WriteLine($"... Writing the modified '{assembly.Name}' assembly to " +
-                    $"{(this.Options.IsReplacingAssemblies ? assemblyPath : outputPath)}");
+                    $"{(this.Options.IsReplacingAssemblies() ? assembly.FilePath : outputPath)}");
-
+                assembly.Write(outputPath);
-                var writeParams = new WriterParameters()
+            }
-                {
+            finally
-                    WriteSymbols = readParams.ReadSymbols,
+            {
-                    SymbolWriterProvider = new PortablePdbWriterProvider()
+                assembly.Dispose();
-                };
-
-                if (!string.IsNullOrEmpty(this.Options.StrongNameKeyFile))
-                {
-                    using FileStream fs = File.Open(this.Options.StrongNameKeyFile, FileMode.Open);
-                    writeParams.StrongNameKeyPair = new StrongNameKeyPair(fs);
-                }
-
-                assembly.Write(outputPath, writeParams);
             }
 
-            if (this.Options.IsReplacingAssemblies)
+            if (this.Options.IsReplacingAssemblies())
             {
-                string targetPath = Path.Combine(this.Options.AssembliesDirectory, assemblyName);
+                string targetPath = Path.Combine(this.Options.AssembliesDirectory, assembly.Name);
-                this.CopyWithRetriesAsync(outputPath, assemblyPath).Wait();
+                this.CopyWithRetriesAsync(outputPath, assembly.FilePath).Wait();
-                if (readParams.ReadSymbols)
+                if (assembly.IsSymbolFileAvailable())
                 {
                     string pdbFile = Path.ChangeExtension(outputPath, "pdb");
                     string targetPdbFile = Path.ChangeExtension(targetPath, "pdb");
@@ -413,154 +205,30 @@ namespace Microsoft.Coyote.Rewriting
             }
         }
 
-        private async Task CopyWithRetriesAsync(string srcFile, string targetFile)
-        {
-            for (int retries = 10; retries >= 0; retries--)
-            {
-                try
-                {
-                    File.Copy(srcFile, targetFile, true);
-                }
-                catch (Exception)
-                {
-                    if (retries is 0)
-                    {
-                        throw;
-                    }
-
-                    await Task.Delay(100);
-                    this.Logger.WriteLine(LogSeverity.Warning, $"... Retrying write to {targetFile}");
-                }
-            }
-        }
-
-        private void FixAssemblyReferences(AssemblyDefinition assembly)
-        {
-            foreach (var module in assembly.Modules)
-            {
-                for (int i = 0, n = module.AssemblyReferences.Count; i < n; i++)
-                {
-                    var ar = module.AssemblyReferences[i];
-                    var name = ar.Name;
-                    if (this.RewrittenAssemblies.TryGetValue(name, out AssemblyNameDefinition rewrittenName))
-                    {
-                        // rewrite this reference to point to the newly rewritten assembly.
-                        var refName = AssemblyNameReference.Parse(rewrittenName.FullName);
-                        module.AssemblyReferences[i] = refName;
-                    }
-                }
-            }
-        }
-
         /// <summary>
-        /// Enqueue any dependent assemblies that also exist in the assemblyPath and have not
+        /// Checks if the specified assembly has been already rewritten with the current version.
-        /// already been rewritten.
         /// </summary>
-        private IEnumerable<Tuple<string, string>> FindLocalDependencies(string assemblyPath, AssemblyDefinition assembly)
+        /// <param name="assembly">The assembly to check.</param>
-        {
+        /// <returns>True if the assembly has been rewritten with the current version, else false.</returns>
-            var assemblyDir = Path.GetDirectoryName(assemblyPath);
+        public static bool IsAssemblyRewritten(Assembly assembly) =>
-            foreach (var module in assembly.Modules)
+            assembly.GetCustomAttribute(typeof(RewritingSignatureAttribute)) is RewritingSignatureAttribute attribute &&
-            {
+            attribute.Version == GetAssemblyRewriterVersion().ToString();
-                foreach (var ar in module.AssemblyReferences)
-                {
-                    var name = ar.Name + ".dll";
-                    var localName = Path.Combine(assemblyDir, name);
-                    if (!this.IsDisallowed(name) &&
-                        File.Exists(localName))
-                    {
-                        yield return new Tuple<string, string>(localName, ar.FullName);
-                    }
-                }
-            }
-        }
 
         /// <summary>
-        /// Rewrites the specified module definition using the specified pass.
+        /// Returns the version of the assembly rewriter.
         /// </summary>
-        private static void RewriteModule(ModuleDefinition module, AssemblyRewriter pass)
+        private static Version GetAssemblyRewriterVersion() => Assembly.GetExecutingAssembly().GetName().Version;
-        {
-            Debug.WriteLine($"....... Module: {module.Name} ({module.FileName})");
-            pass.VisitModule(module);
-            foreach (var type in module.GetTypes())
-            {
-                RewriteType(type, pass);
-            }
-        }
 
         /// <summary>
-        /// Rewrites the specified type definition using the specified pass.
+        /// Creates the output directory, if it does not already exists, and copies all necessary files.
-        /// </summary>
-        private static void RewriteType(TypeDefinition type, AssemblyRewriter pass)
-        {
-            Debug.WriteLine($"......... Type: {type.FullName}");
-            pass.VisitType(type);
-            foreach (var field in type.Fields.ToArray())
-            {
-                Debug.WriteLine($"........... Field: {field.FullName}");
-                pass.VisitField(field);
-            }
-
-            foreach (var method in type.Methods.ToArray())
-            {
-                RewriteMethod(method, pass);
-                if (pass.ModifiedMethodBody)
-                {
-                    AssemblyRewriter.FixInstructionOffsets(method);
-                    pass.ModifiedMethodBody = false;
-                }
-            }
-        }
-
-        /// <summary>
-        /// Rewrites the specified method definition using the specified pass.
-        /// </summary>
-        private static void RewriteMethod(MethodDefinition method, AssemblyRewriter pass)
-        {
-            if (method.Body is null)
-            {
-                return;
-            }
-
-            Debug.WriteLine($"........... Method {method.FullName}");
-            pass.VisitMethod(method);
-        }
-
-        /// <summary>
-        /// Applies the <see cref="IsAssemblyRewrittenAttribute"/> attribute to the specified assembly. This attribute
-        /// indicates that the assembly has been rewritten with the current version of Coyote.
-        /// </summary>
-        private static void ApplyIsAssemblyRewrittenAttribute(AssemblyDefinition assembly)
-        {
-            CustomAttribute attribute = GetCustomAttribute(assembly, typeof(IsAssemblyRewrittenAttribute));
-            var attributeArgument = new CustomAttributeArgument(
-                assembly.MainModule.ImportReference(typeof(string)),
-                GetAssemblyRewritterVersion().ToString());
-
-            if (attribute is null)
-            {
-                MethodReference attributeConstructor = assembly.MainModule.ImportReference(
-                    typeof(IsAssemblyRewrittenAttribute).GetConstructor(new Type[] { typeof(string) }));
-                attribute = new CustomAttribute(attributeConstructor);
-                attribute.ConstructorArguments.Add(attributeArgument);
-                assembly.CustomAttributes.Add(attribute);
-            }
-            else
-            {
-                attribute.ConstructorArguments[0] = attributeArgument;
-            }
-        }
-
-        /// <summary>
-        /// Creates the output directory, if it does not already exists, and copies all necessery files.
         /// </summary>
         /// <returns>The output directory path.</returns>
         private string CreateOutputDirectoryAndCopyFiles()
         {
             string sourceDirectory = this.Options.AssembliesDirectory;
-            string outputDirectory = Directory.CreateDirectory(this.Options.IsReplacingAssemblies ?
+            string outputDirectory = Directory.CreateDirectory(this.Options.IsReplacingAssemblies() ?
                 Path.Combine(this.Options.OutputDirectory, TempDirectory) : this.Options.OutputDirectory).FullName;
-
+            if (!this.Options.IsReplacingAssemblies())
-            if (!this.Options.IsReplacingAssemblies)
             {
                 this.Logger.WriteLine($"... Copying all files to the '{outputDirectory}' directory");
 
@@ -578,7 +246,8 @@ namespace Microsoft.Coyote.Rewriting
                     if (!directoryPath.StartsWith(outputDirectory))
                     {
                         Debug.WriteLine($"..... Copying the '{directoryPath}' directory");
-                        string path = Path.Combine(outputDirectory, directoryPath.Remove(0, sourceDirectory.Length).TrimStart('\\', '/'));
+                        string path = Path.Combine(outputDirectory, directoryPath.Remove(0, sourceDirectory.Length)
+                            .TrimStart('\\', '/'));
                         Directory.CreateDirectory(path);
                         foreach (string filePath in Directory.GetFiles(directoryPath, "*"))
                         {
@@ -589,7 +258,7 @@ namespace Microsoft.Coyote.Rewriting
                 }
             }
 
-            // Copy all the dependent assemblies
+            // Copy all the dependent assemblies.
             foreach (var type in new Type[]
                 {
                     typeof(ControlledTask),
@@ -614,91 +283,27 @@ namespace Microsoft.Coyote.Rewriting
             File.Copy(filePath, Path.Combine(destination, Path.GetFileName(filePath)), true);
 
         /// <summary>
-        /// Checks if the assembly with the specified name is not allowed.
+        /// Copies the specified file to the destination with retries.
         /// </summary>
-        private bool IsDisallowed(string assemblyName) => this.DisallowedAssemblies is null ? false :
+        private async Task CopyWithRetriesAsync(string srcFile, string targetFile)
-            this.DisallowedAssemblies.IsMatch(assemblyName);
-
-        /// <summary>
-        /// Checks if the specified assembly has been already rewritten with the current version of Coyote.
-        /// </summary>
-        /// <param name="assembly">The assembly to check.</param>
-        /// <returns>True if the assembly has been rewritten, else false.</returns>
-        public static bool IsAssemblyRewritten(Assembly assembly) =>
-            assembly.GetCustomAttribute(typeof(IsAssemblyRewrittenAttribute)) is IsAssemblyRewrittenAttribute attribute &&
-            attribute.Version == GetAssemblyRewritterVersion().ToString();
-
-        /// <summary>
-        /// Checks if the specified assembly has been already rewritten with the current version of Coyote.
-        /// </summary>
-        /// <param name="assembly">The assembly to check.</param>
-        /// <returns>True if the assembly has been rewritten, else false.</returns>
-        private static bool IsAssemblyRewritten(AssemblyDefinition assembly)
         {
-            var attribute = GetCustomAttribute(assembly, typeof(IsAssemblyRewrittenAttribute));
+            for (int retries = 10; retries >= 0; retries--)
-            return attribute != null && (string)attribute.ConstructorArguments[0].Value == GetAssemblyRewritterVersion().ToString();
-        }
-
-        /// <summary>
-        /// Checks if the specified assembly is a mixed-mode assembly.
-        /// </summary>
-        /// <param name="assembly">The assembly to check.</param>
-        /// <returns>True if the assembly only contains IL, else false.</returns>
-        private static bool IsMixedModeAssembly(AssemblyDefinition assembly)
-        {
-            foreach (var module in assembly.Modules)
             {
-                if ((module.Attributes & ModuleAttributes.ILOnly) is 0)
+                try
                 {
-                    return true;
+                    File.Copy(srcFile, targetFile, true);
+                }
+                catch (Exception)
+                {
+                    if (retries is 0)
+                    {
+                        throw;
+                    }
+
+                    await Task.Delay(100);
+                    this.Logger.WriteLine(LogSeverity.Warning, $"... Retrying write to {targetFile}");
                 }
             }
-
-            return false;
-        }
-
-        /// <summary>
-        /// Checks if the symbol file for the specified assembly is available.
-        /// </summary>
-        private static bool IsSymbolFileAvailable(string assemblyPath) =>
-            File.Exists(Path.ChangeExtension(assemblyPath, "pdb"));
-
-        /// <summary>
-        /// Returns the first found custom attribute with the specified type, if such an attribute
-        /// is applied to the specified assembly, else null.
-        /// </summary>
-        private static CustomAttribute GetCustomAttribute(AssemblyDefinition assembly, Type attributeType) =>
-            assembly.CustomAttributes.FirstOrDefault(
-                attr => attr.AttributeType.Namespace == attributeType.Namespace &&
-                attr.AttributeType.Name == attributeType.Name);
-
-        /// <summary>
-        /// Returns the version of the assembly rewritter.
-        /// </summary>
-        private static Version GetAssemblyRewritterVersion() => Assembly.GetExecutingAssembly().GetName().Version;
-
-        /// <summary>
-        /// Returns a new assembly resolver.
-        /// </summary>
-        private IAssemblyResolver GetAssemblyResolver()
-        {
-            // TODO: can we reuse it, or do we need a new one for each assembly?
-            var assemblyResolver = new DefaultAssemblyResolver();
-
-            // Add known search directories for resolving assemblies.
-            assemblyResolver.AddSearchDirectory(Path.GetDirectoryName(typeof(ControlledTask).Assembly.Location));
-            assemblyResolver.AddSearchDirectory(this.Options.AssembliesDirectory);
-            if (this.Options.DependencySearchPaths != null)
-            {
-                foreach (var path in this.Options.DependencySearchPaths)
-                {
-                    assemblyResolver.AddSearchDirectory(path);
-                }
-            }
-
-            // Add the assembly resolution error handler.
-            assemblyResolver.ResolveFailure += this.OnResolveAssemblyFailure;
-            return assemblyResolver;
         }
 
         /// <summary>

Source/Test/Rewriting/RewritingOptions.cs

@@ -7,7 +7,8 @@ using System.IO;
 using System.Linq;
 using System.Runtime.Serialization;
 using System.Runtime.Serialization.Json;
-using Microsoft.Coyote.IO;
+using System.Text;
+using System.Text.RegularExpressions;
 
 namespace Microsoft.Coyote.Rewriting
 {
@@ -17,25 +18,30 @@ namespace Microsoft.Coyote.Rewriting
     /// <remarks>
     /// See <see href="/coyote/get-started/rewriting">rewriting</see> for more information.
     /// </remarks>
-    public class RewritingOptions
+    internal class RewritingOptions
     {
         /// <summary>
         /// The directory containing the assemblies to rewrite.
         /// </summary>
-        public string AssembliesDirectory { get; set; }
+        internal string AssembliesDirectory { get; set; }
 
         /// <summary>
         /// The output directory where rewritten assemblies are placed.
         /// If this is the same as the <see cref="AssembliesDirectory"/> then
         /// the rewritten assemblies will replace the original assemblies.
         /// </summary>
-        public string OutputDirectory { get; set; }
+        internal string OutputDirectory { get; set; }
 
         /// <summary>
-        /// The file names of the assemblies to rewrite.  If this list is empty then it will
+        /// The file names of the assemblies to rewrite. If this list is empty then it will
         /// rewrite all assemblies in the <see cref="AssembliesDirectory"/>.
         /// </summary>
-        public HashSet<string> AssemblyPaths { get; set; }
+        internal HashSet<string> AssemblyPaths { get; set; }
+
+        /// <summary>
+        /// The paths to search for resolving dependencies.
+        /// </summary>
+        internal IList<string> DependencySearchPaths { get; set; }
 
         /// <summary>
         /// The regular expressions used to match against assembly names to determine which assemblies
@@ -50,42 +56,27 @@ namespace Microsoft.Coyote.Rewriting
         /// System\.Private\.CoreLib
         /// mscorlib.
         /// </remarks>
-        public IList<string> IgnoredAssemblies { get; set; }
+        private Regex IgnoredAssembliesPattern { get; set; }
-
-        /// <summary>
-        /// The paths to search for resolving dependencies.
-        /// </summary>
-        public IList<string> DependencySearchPaths { get; set; }
-
-        /// <summary>
-        /// True if the input assemblies are being replaced by the rewritten ones.
-        /// </summary>
-        internal bool IsReplacingAssemblies => this.AssembliesDirectory == this.OutputDirectory;
-
-        /// <summary>
-        /// The .NET platform version that Coyote was compiled for.
-        /// </summary>
-        private string DotnetVersion;
 
         /// <summary>
         /// Path of strong name key to use for signing rewritten assemblies.
         /// </summary>
-        public string StrongNameKeyFile { get; set; }
+        internal string StrongNameKeyFile { get; set; }
 
         /// <summary>
         /// True if rewriting for concurrent collections is enabled, else false.
         /// </summary>
-        public bool IsRewritingConcurrentCollections { get; set; } = true;
+        internal bool IsRewritingConcurrentCollections { get; set; }
 
         /// <summary>
         /// True if rewriting for data race checking is enabled, else false.
         /// </summary>
-        public bool IsDataRaceCheckingEnabled { get; set; }
+        internal bool IsDataRaceCheckingEnabled { get; set; }
 
         /// <summary>
         /// True if rewriting dependent assemblies that are found in the same location is enabled, else false.
         /// </summary>
-        public bool IsRewritingDependencies { get; set; }
+        internal bool IsRewritingDependencies { get; set; }
 
         /// <summary>
         /// True if rewriting of unit test methods is enabled, else false.
@@ -96,30 +87,17 @@ namespace Microsoft.Coyote.Rewriting
         /// change the semantics of the original test. For example, if the test is sequential it
         /// will remain sequential, limiting the concurrency coverage that Coyote can achieve.
         /// </remarks>
-        public bool IsRewritingUnitTests { get; internal set; }
+        internal bool IsRewritingUnitTests { get; set; }
 
         /// <summary>
-        /// True if rewriting Threads as controlled tasks.
+        /// True if rewriting threads as controlled tasks.
         /// </summary>
         /// <remarks>
         /// Normally Thread is not supported by Coyote, but this experimental feature wraps the
         /// thread in a Task so that Coyote knows about it which avoids uncontrolled concurrency
         /// errors in some cases.
         /// </remarks>
-        public bool IsRewritingThreads { get; internal set; }
+        internal bool IsRewritingThreads { get; set; }
-
-        /// <summary>
-        /// The logger used for rewriting.
-        /// </summary>
-        /// <remarks>
-        /// By default the logger write to Console.
-        /// </remarks>
-        public ILogger Logger { get; set; }
-
-        /// <summary>
-        /// The amount of log output to produce.
-        /// </summary>
-        public LogSeverity LogLevel { get; set; }
 
         /// <summary>
         /// The .NET platform version that Coyote was compiled for.
@@ -135,118 +113,146 @@ namespace Microsoft.Coyote.Rewriting
             }
         }
 
+        /// <summary>
+        /// The .NET platform version that Coyote was compiled for.
+        /// </summary>
+        private string DotnetVersion;
+
+        /// <summary>
+        /// Initializes a new instance of the <see cref="RewritingOptions"/> class.
+        /// </summary>
+        private RewritingOptions()
+        {
+        }
+
+        /// <summary>
+        /// Creates a new instance of the <see cref="RewritingOptions"/> class with default values.
+        /// </summary>
+        internal static RewritingOptions Create() =>
+            new RewritingOptions()
+            {
+                AssembliesDirectory = string.Empty,
+                OutputDirectory = string.Empty,
+                AssemblyPaths = new HashSet<string>(),
+                DependencySearchPaths = null,
+                IgnoredAssembliesPattern = GetDisallowedAssembliesRegex(new List<string>()),
+                StrongNameKeyFile = null,
+                IsRewritingConcurrentCollections = true,
+                IsDataRaceCheckingEnabled = false,
+                IsRewritingDependencies = false,
+                IsRewritingUnitTests = false,
+                IsRewritingThreads = false
+            };
+
         /// <summary>
         /// Parses the <see cref="RewritingOptions"/> from the specified JSON configuration file.
         /// </summary>
-        public static RewritingOptions ParseFromJSON(string configurationPath)
+        internal static RewritingOptions ParseFromJSON(string configurationPath) =>
+            ParseFromJSON(new RewritingOptions(), configurationPath);
+
+        /// <summary>
+        /// Parses the JSON configuration file and merges the options into the specified
+        /// <see cref="RewritingOptions"/> object.
+        /// </summary>
+        internal static RewritingOptions ParseFromJSON(RewritingOptions options, string configurationPath)
         {
-            // TODO: replace with the new 'System.Text.Json' when .NET 5 comes out.
-
-            var assembliesDirectory = string.Empty;
-            var outputDirectory = string.Empty;
-            var assemblyPaths = new HashSet<string>();
-            IList<string> ignoredAssemblies = null;
-            IList<string> dependencySearchPaths = null;
-            string strongNameKeyFile = null;
-            bool isRewritingConcurrentCollections = false;
-            bool isDataRaceCheckingEnabled = false;
-            bool isRewritingDependencies = false;
-            bool isRewritingUnitTests = false;
-            bool isRewritingThreads = false;
-
-            string workingDirectory = Path.GetDirectoryName(Path.GetFullPath(configurationPath)) + Path.DirectorySeparatorChar;
-
             try
             {
+                // TODO: replace with the new 'System.Text.Json'.
                 using FileStream fs = new FileStream(configurationPath, FileMode.Open, FileAccess.Read);
                 var serializer = new DataContractJsonSerializer(typeof(JsonConfiguration));
                 JsonConfiguration configuration = (JsonConfiguration)serializer.ReadObject(fs);
 
-                Uri baseUri = new Uri(workingDirectory);
+                Uri baseUri = new Uri(Path.GetDirectoryName(Path.GetFullPath(configurationPath)) + Path.DirectorySeparatorChar);
                 Uri resolvedUri = new Uri(baseUri, configuration.AssembliesPath);
-                assembliesDirectory = resolvedUri.LocalPath;
+                options.AssembliesDirectory = resolvedUri.LocalPath;
-                strongNameKeyFile = configuration.StrongNameKeyFile;
-                isRewritingConcurrentCollections = configuration.IsRewritingConcurrentCollections;
-                isDataRaceCheckingEnabled = configuration.IsDataRaceCheckingEnabled;
-                isRewritingDependencies = configuration.IsRewritingDependencies;
-                isRewritingUnitTests = configuration.IsRewritingUnitTests;
-                isRewritingThreads = configuration.IsRewritingThreads;
                 if (string.IsNullOrEmpty(configuration.OutputPath))
                 {
-                    outputDirectory = assembliesDirectory;
+                    options.OutputDirectory = options.AssembliesDirectory;
                 }
                 else
                 {
                     resolvedUri = new Uri(baseUri, configuration.OutputPath);
-                    outputDirectory = resolvedUri.LocalPath;
+                    options.OutputDirectory = resolvedUri.LocalPath;
                 }
 
+                options.AssemblyPaths = new HashSet<string>();
                 if (configuration.Assemblies != null)
                 {
                     foreach (string assembly in configuration.Assemblies)
                     {
-                        resolvedUri = new Uri(Path.Combine(assembliesDirectory, assembly));
+                        resolvedUri = new Uri(Path.Combine(options.AssembliesDirectory, assembly));
-                        assemblyPaths.Add(resolvedUri.LocalPath);
+                        options.AssemblyPaths.Add(resolvedUri.LocalPath);
                     }
                 }
 
-                ignoredAssemblies = configuration.IgnoredAssemblies;
+                options.DependencySearchPaths = configuration.DependencySearchPaths;
-                dependencySearchPaths = configuration.DependencySearchPaths;
+                options.IgnoredAssembliesPattern = GetDisallowedAssembliesRegex(
+                    configuration.IgnoredAssemblies ?? Array.Empty<string>());
+                options.StrongNameKeyFile = configuration.StrongNameKeyFile;
+                options.IsRewritingConcurrentCollections = configuration.IsRewritingConcurrentCollections;
+                options.IsDataRaceCheckingEnabled = configuration.IsDataRaceCheckingEnabled;
+                options.IsRewritingDependencies = configuration.IsRewritingDependencies;
+                options.IsRewritingUnitTests = configuration.IsRewritingUnitTests;
+                options.IsRewritingThreads = configuration.IsRewritingThreads;
             }
             catch (Exception ex)
             {
-                Debug.WriteLine(ex.Message);
+                throw new InvalidOperationException(
-                throw new InvalidOperationException($"Unexpected JSON format in the '{configurationPath}' configuration file.\n{ex.Message}");
+                    $"Unexpected JSON format in the '{configurationPath}' configuration file.\n{ex.Message}");
             }
 
-            return new RewritingOptions()
+            return options;
-            {
-                AssembliesDirectory = assembliesDirectory,
-                OutputDirectory = outputDirectory,
-                AssemblyPaths = assemblyPaths,
-                IgnoredAssemblies = ignoredAssemblies,
-                DependencySearchPaths = dependencySearchPaths,
-                StrongNameKeyFile = strongNameKeyFile,
-                IsRewritingConcurrentCollections = isRewritingConcurrentCollections,
-                IsDataRaceCheckingEnabled = isDataRaceCheckingEnabled,
-                IsRewritingDependencies = isRewritingDependencies,
-                IsRewritingUnitTests = isRewritingUnitTests,
-                IsRewritingThreads = isRewritingThreads
-            };
         }
 
         /// <summary>
-        /// Override the current options with the specified options.
+        /// Returns true if the assembly with the specified name must be ignored during rewriting, else false.
         /// </summary>
-        internal void Merge(RewritingOptions options)
+        internal bool IsAssemblyIgnored(string assemblyName) => this.IgnoredAssembliesPattern.IsMatch(assemblyName);
+
+        /// <summary>
+        /// Returns true if the input assemblies are being replaced by the rewritten ones, else false.
+        /// </summary>
+        internal bool IsReplacingAssemblies() => this.AssembliesDirectory == this.OutputDirectory;
+
+        /// <summary>
+        /// Returns a regex pattern with the disallowed assemblies.
+        /// </summary>
+        private static Regex GetDisallowedAssembliesRegex(IList<string> ignoredAssemblies)
         {
-            if (!string.IsNullOrEmpty(options.StrongNameKeyFile))
+            // List of assemblies that must be ignored by default.
+            string[] defaultIgnoreList = new string[]
             {
-                this.StrongNameKeyFile = options.StrongNameKeyFile;
+                @"Newtonsoft\.Json\.dll",
+                @"Microsoft\.Coyote\.dll",
+                @"Microsoft\.Coyote.Test\.dll",
+                @"Microsoft\.VisualStudio\.TestPlatform.*",
+                @"Microsoft\.TestPlatform.*",
+                @"System\.Private\.CoreLib\.dll",
+                @"mscorlib\.dll"
+            };
+
+            StringBuilder combined = new StringBuilder();
+            foreach (var e in defaultIgnoreList.Concat(ignoredAssemblies))
+            {
+                combined.Append(combined.Length is 0 ? "(" : "|");
+                combined.Append(e);
             }
 
-            if (options.IsDataRaceCheckingEnabled)
+            combined.Append(')');
-            {
-                this.IsDataRaceCheckingEnabled = options.IsDataRaceCheckingEnabled;
-            }
 
-            if (options.IsRewritingDependencies)
+            try
             {
-                this.IsRewritingDependencies = options.IsRewritingDependencies;
+                return new Regex(combined.ToString());
             }
-
+            catch (Exception ex)
-            if (options.IsRewritingThreads)
             {
-                this.IsRewritingThreads = options.IsRewritingThreads;
+                throw new InvalidOperationException(
-            }
+                    $"Unable to create a valid regular expression for ignored assemblies. {ex.Message}.");
-
-            if (options.IsRewritingUnitTests)
-            {
-                this.IsRewritingUnitTests = options.IsRewritingUnitTests;
             }
         }
 
-        internal void ResolveVariables()
+        private void ResolveVariables()
         {
             this.AssembliesDirectory = this.ResolvePath(this.AssembliesDirectory);
             this.OutputDirectory = this.ResolvePath(this.OutputDirectory);
@@ -264,6 +270,39 @@ namespace Microsoft.Coyote.Rewriting
 
         private string ResolvePath(string path) => path.Replace("$(Platform)", this.PlatformVersion);
 
+        /// <summary>
+        /// Sanitizes the rewriting options.
+        /// </summary>
+        internal RewritingOptions Sanitize()
+        {
+            if (string.IsNullOrEmpty(this.AssembliesDirectory))
+            {
+                throw new InvalidOperationException("Please provide RewritingOptions.AssembliesDirectory");
+            }
+            else if (string.IsNullOrEmpty(this.OutputDirectory))
+            {
+                throw new InvalidOperationException("Please provide RewritingOptions.OutputDirectory");
+            }
+            else if (this.AssemblyPaths is null || this.AssemblyPaths.Count is 0)
+            {
+                throw new InvalidOperationException("Please provide RewritingOptions.AssemblyPaths");
+            }
+
+            if (this.AssemblyPaths is null || this.AssemblyPaths.Count is 0)
+            {
+                // Expand folder to include all DLLs in the path.
+                foreach (var file in Directory.GetFiles(this.AssembliesDirectory, "*.dll"))
+                {
+                    if (!this.IsAssemblyIgnored(Path.GetFileName(file)))
+                    {
+                        this.AssemblyPaths.Add(file);
+                    }
+                }
+            }
+
+            return this;
+        }
+
         /// <summary>
         /// Implements a JSON configuration object.
         /// </summary>
@@ -287,8 +326,6 @@ namespace Microsoft.Coyote.Rewriting
         [DataContract]
         private class JsonConfiguration
         {
-            private bool? isRewritingConcurrentCollections;
-
             [DataMember(Name = "AssembliesPath", IsRequired = true)]
             public string AssembliesPath { get; set; }
 
@@ -306,8 +343,12 @@ namespace Microsoft.Coyote.Rewriting
 
             [DataMember(Name = "StrongNameKeyFile")]
             public string StrongNameKeyFile { get; set; }
+
+            [DataMember(Name = "IsDataRaceCheckingEnabled")]
             public bool IsDataRaceCheckingEnabled { get; set; }
 
+            private bool? isRewritingConcurrentCollections;
+
             [DataMember(Name = "IsRewritingConcurrentCollections")]
             public bool IsRewritingConcurrentCollections
             {

Source/Test/SystematicTesting/TestingEngine.cs

@@ -855,7 +855,7 @@ namespace Microsoft.Coyote.SystematicTesting
         }
 
         /// <summary>
-        /// Checks if the test executed by the testing engine has been rewritten.
+        /// Checks if the test executed by the testing engine has been rewritten with the current version.
         /// </summary>
         /// <returns>True if the test has been rewritten, else false.</returns>
         public bool IsTestRewritten() => RewritingEngine.IsAssemblyRewritten(this.TestMethodInfo.Assembly);

Tests/Tests.BugFinding/Invocations/UncontrolledTaskTests.cs

@@ -43,6 +43,16 @@ namespace Microsoft.Coyote.BugFinding.Tests
 
         [Fact(Timeout = 5000)]
         public void TestDetectedUncontrolledGenericAwaiter()
+        {
+            this.Test(async () =>
+            {
+                await new UncontrolledGenericTaskAwaiter();
+            },
+            configuration: this.GetConfiguration().WithTestingIterations(10));
+        }
+
+        [Fact(Timeout = 5000)]
+        public void TestDetectedUncontrolledAwaiterWithGenericArgument()
         {
             this.Test(async () =>
             {

Tests/Tests.Common/BaseTest.cs

@@ -459,7 +459,7 @@ namespace Microsoft.Coyote.Tests.Common
                         };
                     }
 
-                    // BUGBUG: but is this actually letting the test complete in the case
+                    // TODO: but is this actually letting the test complete in the case
                     // of actors which run completely asynchronously?
                     await Task.WhenAny(test(runtime), errorTask.Task);
                     if (handleFailures && errorTask.Task.IsCompleted)

Tests/Tests.Common/Tasks/UncontrolledTaskAwaiter.cs

@@ -19,6 +19,19 @@ namespace Microsoft.Coyote.Tests.Common.Tasks
 #pragma warning restore CA1822 // Mark members as static
     }
 
+    /// <summary>
+    /// Helper class for task rewriting tests.
+    /// </summary>
+    /// <remarks>
+    /// We do not rewrite this class in purpose to test scenarios with partially rewritten code.
+    /// </remarks>
+    public class UncontrolledGenericTaskAwaiter
+    {
+#pragma warning disable CA1822 // Mark members as static
+        public TaskAwaiter<int> GetAwaiter() => Task.FromResult<int>(0).GetAwaiter();
+#pragma warning restore CA1822 // Mark members as static
+    }
+
     /// <summary>
     /// Helper class for task rewriting tests.
     /// </summary>

Tests/Tests.Rewriting/Configurations/ConfigurationTests.cs

@@ -29,7 +29,7 @@ namespace Microsoft.Coyote.Rewriting.Tests.Configuration
 
             Assert.Equal(Path.Combine(configDirectory, "Input"), options.AssembliesDirectory);
             Assert.Equal(Path.Combine(configDirectory, "Input", "Output"), options.OutputDirectory);
-            Assert.False(options.IsReplacingAssemblies);
+            Assert.False(options.IsReplacingAssemblies());
 
             Assert.Single(options.AssemblyPaths);
             Assert.Equal(Path.Combine(options.AssembliesDirectory, "Test.dll"), options.AssemblyPaths.First());
@@ -51,7 +51,7 @@ namespace Microsoft.Coyote.Rewriting.Tests.Configuration
 
             Assert.Equal(configDirectory, options.AssembliesDirectory);
             Assert.Equal(configDirectory, options.OutputDirectory);
-            Assert.True(options.IsReplacingAssemblies);
+            Assert.True(options.IsReplacingAssemblies());
 
             Assert.Equal(2, options.AssemblyPaths.Count());
             Assert.Equal(Path.Combine(options.AssembliesDirectory, "Test1.dll"),

Tools/Coyote/Program.cs

@@ -2,11 +2,10 @@
 // Licensed under the MIT License.
 
 using System;
-using System.Collections.Generic;
 using System.IO;
+using System.Linq;
 using Microsoft.Coyote.IO;
 using Microsoft.Coyote.Rewriting;
-using Microsoft.Coyote.Runtime;
 using Microsoft.Coyote.SystematicTesting;
 using Microsoft.Coyote.Telemetry;
 using Microsoft.Coyote.Utilities;
@@ -33,11 +32,10 @@ namespace Microsoft.Coyote
             AppDomain.CurrentDomain.UnhandledException += OnUnhandledException;
             Console.CancelKeyPress += OnProcessCanceled;
 
-            // Parses the command line options to get the configuration and rewritingOptions.
+            // Parses the command line options to get the configuration and rewriting options.
-
             var configuration = Configuration.Create();
             configuration.TelemetryServerPath = typeof(Program).Assembly.Location;
-            var rewritingOptions = new RewritingOptions();
+            var rewritingOptions = RewritingOptions.Create();
 
             var result = CoyoteTelemetryClient.GetOrCreateMachineId().Result;
             bool firstTime = result.Item2;
@@ -190,47 +188,30 @@ namespace Microsoft.Coyote
         {
             try
             {
-                string assemblyDir = null;
+                // Make sure that the platform is assigned from the command line tool
-                var fileList = new HashSet<string>();
+                // to have the correct version.
-                if (!string.IsNullOrEmpty(configuration.AssemblyToBeAnalyzed))
+                options.PlatformVersion = configuration.PlatformVersion;
+                if (options.AssemblyPaths.Count is 1)
                 {
-                    var fullPath = Path.GetFullPath(configuration.AssemblyToBeAnalyzed);
+                    Console.WriteLine($". Rewriting {options.AssemblyPaths.First()}");
-                    Console.WriteLine($". Rewriting {fullPath}");
-                    assemblyDir = Path.GetDirectoryName(fullPath);
-                    fileList.Add(fullPath);
-                }
-                else if (Directory.Exists(configuration.RewritingOptionsPath))
-                {
-                    assemblyDir = Path.GetFullPath(configuration.RewritingOptionsPath);
-                    Console.WriteLine($". Rewriting the assemblies specified in {assemblyDir}");
-                }
-
-                RewritingOptions config = options;
-
-                if (!string.IsNullOrEmpty(assemblyDir))
-                {
-                    // Create a new RewritingOptions object from command line args only.
-                    config.AssembliesDirectory = assemblyDir;
-                    config.OutputDirectory = assemblyDir;
-                    config.AssemblyPaths = fileList;
                 }
                 else
                 {
-                    // Load options from JSON file.
+                    Console.WriteLine($". Rewriting the assemblies specified in {options.AssembliesDirectory}");
-                    config = RewritingOptions.ParseFromJSON(configuration.RewritingOptionsPath);
-                    Console.WriteLine($". Rewriting the assemblies specified in {configuration.RewritingOptionsPath}");
-                    config.PlatformVersion = configuration.PlatformVersion;
-
-                    // Allow command line options to override the JSON configuration file options.
-                    config.Merge(options);
                 }
 
-                RewritingEngine.Run(configuration, config);
+                var profiler = new Profiler();
+                RewritingEngine.Run(options, configuration, profiler);
+                Console.WriteLine($". Done rewriting in {profiler.Results()} sec");
             }
             catch (Exception ex)
             {
-                Debug.WriteLine(ex.StackTrace);
+                if (ex is AggregateException aex)
-                Error.ReportAndExit(ex.Message);
+                {
+                    ex = aex.Flatten().InnerException;
+                }
+
+                Error.ReportAndExit(configuration.IsDebugVerbosityEnabled ? ex.ToString() : ex.Message);
             }
         }
 

Tools/Coyote/Utilities/CommandLineOptions.cs

@@ -121,9 +121,9 @@ You can provide one or two unsigned integer values", typeof(uint)).IsMultiValue
         /// Parses the command line options and returns a configuration.
         /// </summary>
         /// <param name="args">The command line arguments to parse.</param>
-        /// <param name="configuration">The Configuration object populated with the parsed command line options.</param>
+        /// <param name="configuration">The configuration object populated with the parsed command line options.</param>
-        /// <param name="options">The optional rewriting options.</param>
+        /// <param name="rewritingOptions">The rewriting options.</param>
-        internal bool Parse(string[] args, Configuration configuration, RewritingOptions options)
+        internal bool Parse(string[] args, Configuration configuration, RewritingOptions rewritingOptions)
         {
             try
             {
@@ -132,7 +132,7 @@ You can provide one or two unsigned integer values", typeof(uint)).IsMultiValue
                 {
                     foreach (var arg in result)
                     {
-                        UpdateConfigurationWithParsedArgument(configuration, options, arg);
+                        UpdateConfigurationWithParsedArgument(configuration, rewritingOptions, arg);
                     }
 
                     SanitizeConfiguration(configuration);
@@ -164,7 +164,8 @@ You can provide one or two unsigned integer values", typeof(uint)).IsMultiValue
         /// <summary>
         /// Updates the configuration with the specified parsed argument.
         /// </summary>
-        private static void UpdateConfigurationWithParsedArgument(Configuration configuration, RewritingOptions options, CommandLineArgument option)
+        private static void UpdateConfigurationWithParsedArgument(Configuration configuration,
+            RewritingOptions rewritingOptions, CommandLineArgument option)
         {
             switch (option.LongName)
             {
@@ -187,13 +188,13 @@ You can provide one or two unsigned integer values", typeof(uint)).IsMultiValue
                             configuration.IsVerbose = false;
                             break;
                         case "detailed":
-                            configuration.LogLevel = options.LogLevel = LogSeverity.Informational;
+                            configuration.LogLevel = LogSeverity.Informational;
                             break;
                         case "normal":
-                            configuration.LogLevel = options.LogLevel = LogSeverity.Warning;
+                            configuration.LogLevel = LogSeverity.Warning;
                             break;
                         case "minimal":
-                            configuration.LogLevel = options.LogLevel = LogSeverity.Error;
+                            configuration.LogLevel = LogSeverity.Error;
                             break;
                         default:
                             Error.ReportAndExit($"Please give a valid value for 'verbosity' must be one of 'errors', 'warnings', or 'info', but found {verbosity}.");
@@ -214,20 +215,28 @@ You can provide one or two unsigned integer values", typeof(uint)).IsMultiValue
                         string filename = (string)option.Value;
                         if (Directory.Exists(filename))
                         {
-                            // then we want to rewrite a whole folder full of dll's.
+                            // Then we want to rewrite a whole folder full of assemblies.
-                            configuration.RewritingOptionsPath = filename;
+                            var assembliesDir = Path.GetFullPath(filename);
+                            rewritingOptions.AssembliesDirectory = assembliesDir;
+                            rewritingOptions.OutputDirectory = assembliesDir;
                         }
                         else
                         {
                             string extension = Path.GetExtension(filename);
                             if (string.Compare(extension, ".json", StringComparison.OrdinalIgnoreCase) is 0)
                             {
-                                configuration.RewritingOptionsPath = filename;
+                                // Parse the rewriting options from the JSON file.
+                                RewritingOptions.ParseFromJSON(rewritingOptions, filename);
                             }
                             else if (string.Compare(extension, ".dll", StringComparison.OrdinalIgnoreCase) is 0 ||
                                 string.Compare(extension, ".exe", StringComparison.OrdinalIgnoreCase) is 0)
                             {
                                 configuration.AssemblyToBeAnalyzed = filename;
+                                var fullPath = Path.GetFullPath(filename);
+                                var assembliesDir = Path.GetDirectoryName(fullPath);
+                                rewritingOptions.AssembliesDirectory = assembliesDir;
+                                rewritingOptions.OutputDirectory = assembliesDir;
+                                rewritingOptions.AssemblyPaths.Add(fullPath);
                             }
                             else
                             {
@@ -393,19 +402,19 @@ You can provide one or two unsigned integer values", typeof(uint)).IsMultiValue
                     configuration.AdditionalCodeCoverageAssemblies[(string)option.Value] = true;
                     break;
                 case "strong-name-key-file":
-                    options.StrongNameKeyFile = (string)option.Value;
+                    rewritingOptions.StrongNameKeyFile = (string)option.Value;
                     break;
                 case "assert-data-races":
-                    options.IsDataRaceCheckingEnabled = true;
+                    rewritingOptions.IsDataRaceCheckingEnabled = true;
                     break;
                 case "rewrite-dependencies":
-                    options.IsRewritingDependencies = true;
+                    rewritingOptions.IsRewritingDependencies = true;
                     break;
                 case "rewrite-unit-tests":
-                    options.IsRewritingUnitTests = true;
+                    rewritingOptions.IsRewritingUnitTests = true;
                     break;
                 case "rewrite-threads":
-                    options.IsRewritingThreads = true;
+                    rewritingOptions.IsRewritingThreads = true;
                     break;
                 case "timeout-delay":
                     configuration.TimeoutDelay = (uint)option.Value;
@@ -463,7 +472,7 @@ You can provide one or two unsigned integer values", typeof(uint)).IsMultiValue
         }
 
         /// <summary>
-        /// Checks the configuration for errors.
+        /// Sanitizes the configuration.
         /// </summary>
         private static void SanitizeConfiguration(Configuration configuration)
         {

docs/ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute.md

@@ -0,0 +1,27 @@
+# CoyoteVersionAttribute class
+
+Attribute that defines the version of Coyote used for rewriting an assembly.
+
+```csharp
+[AttributeUsage(AttributeTargets.Assembly)]
+public sealed class CoyoteVersionAttribute : Attribute
+```
+
+## Public Members
+
+| name | description |
+| --- | --- |
+| [CoyoteVersionAttribute](CoyoteVersionAttribute/CoyoteVersionAttribute.md)(…) | Initializes a new instance of the [`CoyoteVersionAttribute`](CoyoteVersionAttribute.md) class. |
+| readonly [Identifier](CoyoteVersionAttribute/Identifier.md) | Unique identifier applied to all dependent rewritten assemblies. |
+| readonly [Version](CoyoteVersionAttribute/Version.md) | The version of Coyote used for the rewriting. |
+
+## Remarks
+
+If this attribute is applied to an assembly manifest, it denotes that the assembly has been rewritten.
+
+## See Also
+
+* namespace [Microsoft.Coyote.Rewriting](../Microsoft.Coyote.RewritingNamespace.md)
+* assembly [Microsoft.Coyote.Test](../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/CoyoteVersionAttribute.md

@@ -0,0 +1,15 @@
+# CoyoteVersionAttribute constructor
+
+Initializes a new instance of the [`CoyoteVersionAttribute`](../CoyoteVersionAttribute.md) class.
+
+```csharp
+public CoyoteVersionAttribute(string version, string identifier)
+```
+
+## See Also
+
+* class [CoyoteVersionAttribute](../CoyoteVersionAttribute.md)
+* namespace [Microsoft.Coyote.Rewriting](../CoyoteVersionAttribute.md)
+* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/Identifier.md

@@ -0,0 +1,15 @@
+# CoyoteVersionAttribute.Identifier field
+
+Unique identifier applied to all dependent rewritten assemblies.
+
+```csharp
+public readonly string Identifier;
+```
+
+## See Also
+
+* class [CoyoteVersionAttribute](../CoyoteVersionAttribute.md)
+* namespace [Microsoft.Coyote.Rewriting](../CoyoteVersionAttribute.md)
+* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/Version.md

@@ -0,0 +1,15 @@
+# CoyoteVersionAttribute.Version field
+
+The version of Coyote used for the rewriting.
+
+```csharp
+public readonly string Version;
+```
+
+## See Also
+
+* class [CoyoteVersionAttribute](../CoyoteVersionAttribute.md)
+* namespace [Microsoft.Coyote.Rewriting](../CoyoteVersionAttribute.md)
+* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
+
+<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute.md

@@ -1,22 +0,0 @@
-# IsAssemblyRewrittenAttribute class
-
-Attribute for checking if an assembly has been rewritten by Coyote. If this attribute is applied to an assembly, it denotes that the assembly has been rewritten.
-
-```csharp
-[AttributeUsage(AttributeTargets.Assembly)]
-public sealed class IsAssemblyRewrittenAttribute : Attribute
-```
-
-## Public Members
-
-| name | description |
-| --- | --- |
-| [IsAssemblyRewrittenAttribute](IsAssemblyRewrittenAttribute/IsAssemblyRewrittenAttribute.md)(…) | Initializes a new instance of the [`IsAssemblyRewrittenAttribute`](IsAssemblyRewrittenAttribute.md) class. |
-| readonly [Version](IsAssemblyRewrittenAttribute/Version.md) | The version of Coyote used for the rewritting. |
-
-## See Also
-
-* namespace [Microsoft.Coyote.Rewriting](../Microsoft.Coyote.RewritingNamespace.md)
-* assembly [Microsoft.Coyote.Test](../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute/IsAssemblyRewrittenAttribute.md

@@ -1,15 +0,0 @@
-# IsAssemblyRewrittenAttribute constructor
-
-Initializes a new instance of the [`IsAssemblyRewrittenAttribute`](../IsAssemblyRewrittenAttribute.md) class.
-
-```csharp
-public IsAssemblyRewrittenAttribute(string version)
-```
-
-## See Also
-
-* class [IsAssemblyRewrittenAttribute](../IsAssemblyRewrittenAttribute.md)
-* namespace [Microsoft.Coyote.Rewriting](../IsAssemblyRewrittenAttribute.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute/Version.md

@@ -1,15 +0,0 @@
-# IsAssemblyRewrittenAttribute.Version field
-
-The version of Coyote used for the rewritting.
-
-```csharp
-public readonly string Version;
-```
-
-## See Also
-
-* class [IsAssemblyRewrittenAttribute](../IsAssemblyRewrittenAttribute.md)
-* namespace [Microsoft.Coyote.Rewriting](../IsAssemblyRewrittenAttribute.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingEngine.md

@@ -10,8 +10,7 @@ public class RewritingEngine
 
 | name | description |
 | --- | --- |
-| static [IsAssemblyRewritten](RewritingEngine/IsAssemblyRewritten.md)(…) | Checks if the specified assembly has been already rewritten with the current version of Coyote. |
+| static [IsAssemblyRewritten](RewritingEngine/IsAssemblyRewritten.md)(…) | Checks if the specified assembly has been already rewritten with the current version. |
-| static [Run](RewritingEngine/Run.md)(…) | Runs the engine using the specified rewriting options. |
 
 ## Remarks
 

docs/ref/Microsoft.Coyote.Rewriting/RewritingEngine/IsAssemblyRewritten.md

@@ -1,6 +1,6 @@
 # RewritingEngine.IsAssemblyRewritten method
 
-Checks if the specified assembly has been already rewritten with the current version of Coyote.
+Checks if the specified assembly has been already rewritten with the current version.
 
 ```csharp
 public static bool IsAssemblyRewritten(Assembly assembly)
@@ -12,7 +12,7 @@ public static bool IsAssemblyRewritten(Assembly assembly)
 
 ## Return Value
 
-True if the assembly has been rewritten, else false.
+True if the assembly has been rewritten with the current version, else false.
 
 ## See Also
 

docs/ref/Microsoft.Coyote.Rewriting/RewritingEngine/Run.md

@@ -1,16 +0,0 @@
-# RewritingEngine.Run method
-
-Runs the engine using the specified rewriting options.
-
-```csharp
-public static void Run(Configuration configuration, RewritingOptions options)
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* class [RewritingEngine](../RewritingEngine.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingEngine.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions.md

@@ -1,38 +0,0 @@
-# RewritingOptions class
-
-Options for rewriting binaries.
-
-```csharp
-public class RewritingOptions
-```
-
-## Public Members
-
-| name | description |
-| --- | --- |
-| [RewritingOptions](RewritingOptions/RewritingOptions.md)() | The default constructor. |
-| static [ParseFromJSON](RewritingOptions/ParseFromJSON.md)(…) | Parses the [`RewritingOptions`](RewritingOptions.md) from the specified JSON configuration file. |
-| [AssembliesDirectory](RewritingOptions/AssembliesDirectory.md) { get; set; } | The directory containing the assemblies to rewrite. |
-| [AssemblyPaths](RewritingOptions/AssemblyPaths.md) { get; set; } | The file names of the assemblies to rewrite. If this list is empty then it will rewrite all assemblies in the [`AssembliesDirectory`](RewritingOptions/AssembliesDirectory.md). |
-| [DependencySearchPaths](RewritingOptions/DependencySearchPaths.md) { get; set; } | The paths to search for resolving dependencies. |
-| [IgnoredAssemblies](RewritingOptions/IgnoredAssemblies.md) { get; set; } | The regular expressions used to match against assembly names to determine which assemblies to ignore when rewriting dependencies or a whole directory. |
-| [IsDataRaceCheckingEnabled](RewritingOptions/IsDataRaceCheckingEnabled.md) { get; set; } | True if rewriting for data race checking is enabled, else false. |
-| [IsRewritingConcurrentCollections](RewritingOptions/IsRewritingConcurrentCollections.md) { get; set; } | True if rewriting for concurrent collections is enabled, else false. |
-| [IsRewritingDependencies](RewritingOptions/IsRewritingDependencies.md) { get; set; } | True if rewriting dependent assemblies that are found in the same location is enabled, else false. |
-| [IsRewritingThreads](RewritingOptions/IsRewritingThreads.md) { get; } | True if rewriting Threads as controlled tasks. |
-| [IsRewritingUnitTests](RewritingOptions/IsRewritingUnitTests.md) { get; } | True if rewriting of unit test methods is enabled, else false. |
-| [Logger](RewritingOptions/Logger.md) { get; set; } | The logger used for rewriting. |
-| [LogLevel](RewritingOptions/LogLevel.md) { get; set; } | The amount of log output to produce. |
-| [OutputDirectory](RewritingOptions/OutputDirectory.md) { get; set; } | The output directory where rewritten assemblies are placed. If this is the same as the [`AssembliesDirectory`](RewritingOptions/AssembliesDirectory.md) then the rewritten assemblies will replace the original assemblies. |
-| [StrongNameKeyFile](RewritingOptions/StrongNameKeyFile.md) { get; set; } | Path of strong name key to use for signing rewritten assemblies. |
-
-## Remarks
-
-See [rewriting](/coyote/get-started/rewriting) for more information.
-
-## See Also
-
-* namespace [Microsoft.Coyote.Rewriting](../Microsoft.Coyote.RewritingNamespace.md)
-* assembly [Microsoft.Coyote.Test](../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssembliesDirectory.md

@@ -1,15 +0,0 @@
-# RewritingOptions.AssembliesDirectory property
-
-The directory containing the assemblies to rewrite.
-
-```csharp
-public string AssembliesDirectory { get; set; }
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssemblyPaths.md

@@ -1,15 +0,0 @@
-# RewritingOptions.AssemblyPaths property
-
-The file names of the assemblies to rewrite. If this list is empty then it will rewrite all assemblies in the [`AssembliesDirectory`](AssembliesDirectory.md).
-
-```csharp
-public HashSet<string> AssemblyPaths { get; set; }
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/DependencySearchPaths.md

@@ -1,15 +0,0 @@
-# RewritingOptions.DependencySearchPaths property
-
-The paths to search for resolving dependencies.
-
-```csharp
-public IList<string> DependencySearchPaths { get; set; }
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IgnoredAssemblies.md

@@ -1,19 +0,0 @@
-# RewritingOptions.IgnoredAssemblies property
-
-The regular expressions used to match against assembly names to determine which assemblies to ignore when rewriting dependencies or a whole directory.
-
-```csharp
-public IList<string> IgnoredAssemblies { get; set; }
-```
-
-## Remarks
-
-The list automatically includes the following expressions: Microsoft\.Coyote.* Microsoft\.TestPlatform.* Microsoft\.VisualStudio\.TestPlatform.* Newtonsoft\.Json.* System\.Private\.CoreLib mscorlib.
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsDataRaceCheckingEnabled.md

@@ -1,15 +0,0 @@
-# RewritingOptions.IsDataRaceCheckingEnabled property
-
-True if rewriting for data race checking is enabled, else false.
-
-```csharp
-public bool IsDataRaceCheckingEnabled { get; set; }
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingConcurrentCollections.md

@@ -1,15 +0,0 @@
-# RewritingOptions.IsRewritingConcurrentCollections property
-
-True if rewriting for concurrent collections is enabled, else false.
-
-```csharp
-public bool IsRewritingConcurrentCollections { get; set; }
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingDependencies.md

@@ -1,15 +0,0 @@
-# RewritingOptions.IsRewritingDependencies property
-
-True if rewriting dependent assemblies that are found in the same location is enabled, else false.
-
-```csharp
-public bool IsRewritingDependencies { get; set; }
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingThreads.md

@@ -1,19 +0,0 @@
-# RewritingOptions.IsRewritingThreads property
-
-True if rewriting Threads as controlled tasks.
-
-```csharp
-public bool IsRewritingThreads { get; }
-```
-
-## Remarks
-
-Normally Thread is not supported by Coyote, but this experimental feature wraps the thread in a Task so that Coyote knows about it which avoids uncontrolled concurrency errors in some cases.
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingUnitTests.md

@@ -1,19 +0,0 @@
-# RewritingOptions.IsRewritingUnitTests property
-
-True if rewriting of unit test methods is enabled, else false.
-
-```csharp
-public bool IsRewritingUnitTests { get; }
-```
-
-## Remarks
-
-If unit test rewriting is enabled, Coyote will instrument the binary to run unit test methods in the scope of the Coyote testing engine. Note that this rewriting does not change the semantics of the original test. For example, if the test is sequential it will remain sequential, limiting the concurrency coverage that Coyote can achieve.
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/LogLevel.md

@@ -1,15 +0,0 @@
-# RewritingOptions.LogLevel property
-
-The amount of log output to produce.
-
-```csharp
-public LogSeverity LogLevel { get; set; }
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/Logger.md

@@ -1,19 +0,0 @@
-# RewritingOptions.Logger property
-
-The logger used for rewriting.
-
-```csharp
-public ILogger Logger { get; set; }
-```
-
-## Remarks
-
-By default the logger write to Console.
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/OutputDirectory.md

@@ -1,15 +0,0 @@
-# RewritingOptions.OutputDirectory property
-
-The output directory where rewritten assemblies are placed. If this is the same as the [`AssembliesDirectory`](AssembliesDirectory.md) then the rewritten assemblies will replace the original assemblies.
-
-```csharp
-public string OutputDirectory { get; set; }
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/ParseFromJSON.md

@@ -1,15 +0,0 @@
-# RewritingOptions.ParseFromJSON method
-
-Parses the [`RewritingOptions`](../RewritingOptions.md) from the specified JSON configuration file.
-
-```csharp
-public static RewritingOptions ParseFromJSON(string configurationPath)
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/RewritingOptions.md

@@ -1,15 +0,0 @@
-# RewritingOptions constructor
-
-The default constructor.
-
-```csharp
-public RewritingOptions()
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.Rewriting/RewritingOptions/StrongNameKeyFile.md

@@ -1,15 +0,0 @@
-# RewritingOptions.StrongNameKeyFile property
-
-Path of strong name key to use for signing rewritten assemblies.
-
-```csharp
-public string StrongNameKeyFile { get; set; }
-```
-
-## See Also
-
-* class [RewritingOptions](../RewritingOptions.md)
-* namespace [Microsoft.Coyote.Rewriting](../RewritingOptions.md)
-* assembly [Microsoft.Coyote.Test](../../Microsoft.Coyote.Test.md)
-
-<!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.RewritingNamespace.md

@@ -2,8 +2,7 @@
 
 | public type | description |
 | --- | --- |
-| class [IsAssemblyRewrittenAttribute](Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute.md) | Attribute for checking if an assembly has been rewritten by Coyote. If this attribute is applied to an assembly, it denotes that the assembly has been rewritten. |
+| class [CoyoteVersionAttribute](Microsoft.Coyote.Rewriting/CoyoteVersionAttribute.md) | Attribute that defines the version of Coyote used for rewriting an assembly. |
 | class [RewritingEngine](Microsoft.Coyote.Rewriting/RewritingEngine.md) | Engine that can rewrite a set of assemblies for systematic testing. |
-| class [RewritingOptions](Microsoft.Coyote.Rewriting/RewritingOptions.md) | Options for rewriting binaries. |
 
 <!-- DO NOT EDIT: generated by xmldocmd for Microsoft.Coyote.Test.dll -->

docs/ref/Microsoft.Coyote.SystematicTesting/TestingEngine.md

@@ -16,7 +16,7 @@ public sealed class TestingEngine
 | [ReproducibleTrace](TestingEngine/ReproducibleTrace.md) { get; } | The reproducable trace, if any. |
 | [TestReport](TestingEngine/TestReport.md) { get; set; } | Data structure containing information gathered during testing. |
 | [GetReport](TestingEngine/GetReport.md)() | Returns a report with the testing results. |
-| [IsTestRewritten](TestingEngine/IsTestRewritten.md)() | Checks if the test executed by the testing engine has been rewritten. |
+| [IsTestRewritten](TestingEngine/IsTestRewritten.md)() | Checks if the test executed by the testing engine has been rewritten with the current version. |
 | [RegisterPerIterationCallBack](TestingEngine/RegisterPerIterationCallBack.md)(…) | Registers a callback to invoke at the end of each iteration. The callback takes as a parameter an integer representing the current iteration. |
 | [Run](TestingEngine/Run.md)() | Runs the testing engine. |
 | [Stop](TestingEngine/Stop.md)() | Stops the testing engine. |

docs/ref/Microsoft.Coyote.SystematicTesting/TestingEngine/IsTestRewritten.md

@@ -1,6 +1,6 @@
 # TestingEngine.IsTestRewritten method
 
-Checks if the test executed by the testing engine has been rewritten.
+Checks if the test executed by the testing engine has been rewritten with the current version.
 
 ```csharp
 public bool IsTestRewritten()

docs/ref/Microsoft.Coyote.Test.md

@@ -4,9 +4,8 @@
 
 | public type | description |
 | --- | --- |
-| class [IsAssemblyRewrittenAttribute](Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute.md) | Attribute for checking if an assembly has been rewritten by Coyote. If this attribute is applied to an assembly, it denotes that the assembly has been rewritten. |
+| class [CoyoteVersionAttribute](Microsoft.Coyote.Rewriting/CoyoteVersionAttribute.md) | Attribute that defines the version of Coyote used for rewriting an assembly. |
 | class [RewritingEngine](Microsoft.Coyote.Rewriting/RewritingEngine.md) | Engine that can rewrite a set of assemblies for systematic testing. |
-| class [RewritingOptions](Microsoft.Coyote.Rewriting/RewritingOptions.md) | Options for rewriting binaries. |
 
 ## Microsoft.Coyote.SystematicTesting namespace
 

docs/ref/toc.yml

@@ -973,53 +973,20 @@ toc:
     - name: Microsoft.Coyote.Rewriting
       link: ref/Microsoft.Coyote.RewritingNamespace
       subfolderitems:
-      - name: IsAssemblyRewrittenAttribute
+      - name: CoyoteVersionAttribute
-        link: ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute
+        link: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute
         subfolderitems:
-        - name: IsAssemblyRewrittenAttribute
+        - name: CoyoteVersionAttribute
-          link: ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute/IsAssemblyRewrittenAttribute
+          link: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/CoyoteVersionAttribute
         - name: Version
-          link: ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute/Version
+          link: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/Version
+        - name: Identifier
+          link: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/Identifier
       - name: RewritingEngine
         link: ref/Microsoft.Coyote.Rewriting/RewritingEngine
         subfolderitems:
-        - name: Run
-          link: ref/Microsoft.Coyote.Rewriting/RewritingEngine/Run
         - name: IsAssemblyRewritten
           link: ref/Microsoft.Coyote.Rewriting/RewritingEngine/IsAssemblyRewritten
-      - name: RewritingOptions
-        link: ref/Microsoft.Coyote.Rewriting/RewritingOptions
-        subfolderitems:
-        - name: ParseFromJSON
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/ParseFromJSON
-        - name: RewritingOptions
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/RewritingOptions
-        - name: AssembliesDirectory
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssembliesDirectory
-        - name: OutputDirectory
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/OutputDirectory
-        - name: AssemblyPaths
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssemblyPaths
-        - name: IgnoredAssemblies
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IgnoredAssemblies
-        - name: DependencySearchPaths
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/DependencySearchPaths
-        - name: StrongNameKeyFile
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/StrongNameKeyFile
-        - name: IsRewritingConcurrentCollections
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingConcurrentCollections
-        - name: IsDataRaceCheckingEnabled
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsDataRaceCheckingEnabled
-        - name: IsRewritingDependencies
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingDependencies
-        - name: IsRewritingUnitTests
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingUnitTests
-        - name: IsRewritingThreads
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingThreads
-        - name: Logger
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/Logger
-        - name: LogLevel
-          link: ref/Microsoft.Coyote.Rewriting/RewritingOptions/LogLevel
     - name: Microsoft.Coyote.SystematicTesting
       link: ref/Microsoft.Coyote.SystematicTestingNamespace
       subfolderitems:

mkdocs-local.yml

@@ -620,35 +620,18 @@ nav:
       - Monitor.State.HotAttribute:
         - Overview: ref/Microsoft.Coyote.Specifications/Monitor.State.HotAttribute.md
         - HotAttribute: ref/Microsoft.Coyote.Specifications/Monitor.State.HotAttribute/HotAttribute.md
-  - Microsoft.Coyote.Test:
+- Microsoft.Coyote.Test:
     - Overview: ref/Microsoft.Coyote.Test.md
     - Microsoft.Coyote.Rewriting:
       - Namespace Overview: ref/Microsoft.Coyote.RewritingNamespace.md
-      - IsAssemblyRewrittenAttribute:
+      - CoyoteVersionAttribute:
-        - Overview: ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute.md
+        - Overview: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute.md
-        - IsAssemblyRewrittenAttribute: ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute/IsAssemblyRewrittenAttribute.md
+        - CoyoteVersionAttribute: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/CoyoteVersionAttribute.md
-        - Version: ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute/Version.md
+        - Version: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/Version.md
+        - Identifier: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/Identifier.md
       - RewritingEngine:
         - Overview: ref/Microsoft.Coyote.Rewriting/RewritingEngine.md
-        - Run: ref/Microsoft.Coyote.Rewriting/RewritingEngine/Run.md
         - IsAssemblyRewritten: ref/Microsoft.Coyote.Rewriting/RewritingEngine/IsAssemblyRewritten.md
-      - RewritingOptions:
-        - Overview: ref/Microsoft.Coyote.Rewriting/RewritingOptions.md
-        - ParseFromJSON: ref/Microsoft.Coyote.Rewriting/RewritingOptions/ParseFromJSON.md
-        - RewritingOptions: ref/Microsoft.Coyote.Rewriting/RewritingOptions/RewritingOptions.md
-        - AssembliesDirectory: ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssembliesDirectory.md
-        - OutputDirectory: ref/Microsoft.Coyote.Rewriting/RewritingOptions/OutputDirectory.md
-        - AssemblyPaths: ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssemblyPaths.md
-        - IgnoredAssemblies: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IgnoredAssemblies.md
-        - DependencySearchPaths: ref/Microsoft.Coyote.Rewriting/RewritingOptions/DependencySearchPaths.md
-        - StrongNameKeyFile: ref/Microsoft.Coyote.Rewriting/RewritingOptions/StrongNameKeyFile.md
-        - IsRewritingConcurrentCollections: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingConcurrentCollections.md
-        - IsDataRaceCheckingEnabled: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsDataRaceCheckingEnabled.md
-        - IsRewritingDependencies: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingDependencies.md
-        - IsRewritingUnitTests: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingUnitTests.md
-        - IsRewritingThreads: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingThreads.md
-        - Logger: ref/Microsoft.Coyote.Rewriting/RewritingOptions/Logger.md
-        - LogLevel: ref/Microsoft.Coyote.Rewriting/RewritingOptions/LogLevel.md
     - Microsoft.Coyote.SystematicTesting:
       - Namespace Overview: ref/Microsoft.Coyote.SystematicTestingNamespace.md
       - TestReport:

mkdocs.yml

@@ -624,31 +624,14 @@ nav:
     - Overview: ref/Microsoft.Coyote.Test.md
     - Microsoft.Coyote.Rewriting:
       - Namespace Overview: ref/Microsoft.Coyote.RewritingNamespace.md
-      - IsAssemblyRewrittenAttribute:
+      - CoyoteVersionAttribute:
-        - Overview: ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute.md
+        - Overview: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute.md
-        - IsAssemblyRewrittenAttribute: ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute/IsAssemblyRewrittenAttribute.md
+        - CoyoteVersionAttribute: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/CoyoteVersionAttribute.md
-        - Version: ref/Microsoft.Coyote.Rewriting/IsAssemblyRewrittenAttribute/Version.md
+        - Version: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/Version.md
+        - Identifier: ref/Microsoft.Coyote.Rewriting/CoyoteVersionAttribute/Identifier.md
       - RewritingEngine:
         - Overview: ref/Microsoft.Coyote.Rewriting/RewritingEngine.md
-        - Run: ref/Microsoft.Coyote.Rewriting/RewritingEngine/Run.md
         - IsAssemblyRewritten: ref/Microsoft.Coyote.Rewriting/RewritingEngine/IsAssemblyRewritten.md
-      - RewritingOptions:
-        - Overview: ref/Microsoft.Coyote.Rewriting/RewritingOptions.md
-        - ParseFromJSON: ref/Microsoft.Coyote.Rewriting/RewritingOptions/ParseFromJSON.md
-        - RewritingOptions: ref/Microsoft.Coyote.Rewriting/RewritingOptions/RewritingOptions.md
-        - AssembliesDirectory: ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssembliesDirectory.md
-        - OutputDirectory: ref/Microsoft.Coyote.Rewriting/RewritingOptions/OutputDirectory.md
-        - AssemblyPaths: ref/Microsoft.Coyote.Rewriting/RewritingOptions/AssemblyPaths.md
-        - IgnoredAssemblies: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IgnoredAssemblies.md
-        - DependencySearchPaths: ref/Microsoft.Coyote.Rewriting/RewritingOptions/DependencySearchPaths.md
-        - StrongNameKeyFile: ref/Microsoft.Coyote.Rewriting/RewritingOptions/StrongNameKeyFile.md
-        - IsRewritingConcurrentCollections: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingConcurrentCollections.md
-        - IsDataRaceCheckingEnabled: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsDataRaceCheckingEnabled.md
-        - IsRewritingDependencies: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingDependencies.md
-        - IsRewritingUnitTests: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingUnitTests.md
-        - IsRewritingThreads: ref/Microsoft.Coyote.Rewriting/RewritingOptions/IsRewritingThreads.md
-        - Logger: ref/Microsoft.Coyote.Rewriting/RewritingOptions/Logger.md
-        - LogLevel: ref/Microsoft.Coyote.Rewriting/RewritingOptions/LogLevel.md
     - Microsoft.Coyote.SystematicTesting:
       - Namespace Overview: ref/Microsoft.Coyote.SystematicTestingNamespace.md
       - TestReport: