Skip to content
This repository was archived by the owner on Jul 15, 2023. It is now read-only.
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
242 changes: 115 additions & 127 deletions Microsoft.Research/RegressionTest/ClousotTests/AsyncTestDriver.cs
Original file line number Diff line number Diff line change
@@ -1,16 +1,5 @@
// CodeContracts
//
// Copyright (c) Microsoft Corporation
//
// All rights reserved.
//
// MIT License
//
// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
// Copyright (c) Microsoft. All rights reserved.
// Licensed under the MIT license. See LICENSE file in the project root for full license information.

using System;
using System.Collections.Generic;
Expand All @@ -20,147 +9,146 @@

namespace Tests
{
public class AsyncTestDriver
{
delegate void IsolatedAction<in T>(T obj, out Exception exceptionThrown, out string dataReceived);

public static readonly uint MaxWaitHandles_Default = Math.Max(1, Math.Min(4, (uint)(Environment.ProcessorCount - 1)));
public static readonly uint MaxWaitHandles_AllButOne = Math.Max(1, (uint)(Environment.ProcessorCount - 1));
public class AsyncTestDriver
{
private delegate void IsolatedAction<in T>(T obj, out Exception exceptionThrown, out string dataReceived);

private static readonly int SingleTestMaxWait = 200000;
public static readonly uint MaxWaitHandles_Default = Math.Max(1, Math.Min(4, (uint)(Environment.ProcessorCount - 1)));
public static readonly uint MaxWaitHandles_AllButOne = Math.Max(1, (uint)(Environment.ProcessorCount - 1));

private readonly Action<Options, Output> action;
private readonly IsolatedAction<Options> actionDelegate;
private readonly Func<Options, bool> skipTest;
private Dictionary<string, IAsyncResult> testAsyncResults;
private readonly uint maxWaitHandles;
private WaitHandle[] waitHandles;
private int nbWaitHandles;
private bool beginTestsProcessed = false;
private bool orderReversed = false;
private static readonly int SingleTestMaxWait = 200000;

public string BeginMessage;
private readonly Action<Options, Output> action;
private readonly IsolatedAction<Options> actionDelegate;
private readonly Func<Options, bool> skipTest;
private Dictionary<string, IAsyncResult> testAsyncResults;
private readonly uint maxWaitHandles;
private WaitHandle[] waitHandles;
private int nbWaitHandles;
private bool beginTestsProcessed = false;
private bool orderReversed = false;

public AsyncTestDriver(Action<Options, Output> action, Func<Options, bool> skipTest)
: this(action, skipTest, MaxWaitHandles_Default)
{ }
public string BeginMessage;

public AsyncTestDriver(Action<Options, Output> action, Func<Options, bool> skipTest, uint maxWaitHandles)
{
this.action = action;
this.actionDelegate = this.ActionAsIsolated;
this.skipTest = skipTest;
this.maxWaitHandles = maxWaitHandles;
}
public AsyncTestDriver(Action<Options, Output> action, Func<Options, bool> skipTest)
: this(action, skipTest, MaxWaitHandles_Default)
{ }

// We have no control on the order of the tests, so we make sure
// to always call Begin before End

public void BeginTest(Options options)
{
if (this.skipTest(options))
return;
public AsyncTestDriver(Action<Options, Output> action, Func<Options, bool> skipTest, uint maxWaitHandles)
{
this.action = action;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I saw that in some other PRs with formatting changes you also changed field names...

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I explicitly disabled that - I left a message in Gitter explaining why (basically there is so much code to reformat that we need to do the safe option first and then we can consider renaming things in the future).

I closed all the other formatting PRs so I can update them to also not rename fields.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good. Jut wanted to double check.

actionDelegate = this.ActionAsIsolated;
this.skipTest = skipTest;
this.maxWaitHandles = maxWaitHandles;
}

this.beginTestsProcessed = true;
// We have no control on the order of the tests, so we make sure
// to always call Begin before End

if (this.orderReversed)
this.EndTestInternal(options);
else
this.BeginTestInternal(options);
}
public void BeginTest(Options options)
{
if (skipTest(options))
return;

public void EndTest(Options options)
{
if (this.skipTest(options))
return;
beginTestsProcessed = true;

if (!this.beginTestsProcessed)
this.orderReversed = true;
if (orderReversed)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can formatter insert braces for single statements like that?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is following the .NET foundation bracing rules, which generally requires braces but makes an exception for cases where the entire block is a single statement which does not span multiple lines. This bracing rule was later implemented in StyleCopAnalyzers as well (DotNetAnalyzers/StyleCopAnalyzers#716, DotNetAnalyzers/StyleCopAnalyzers#717).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is a plenty of places in this code base like:

if (check)
{
  // several statements
}
else
   oneStatement;

This is very unreadable. I would prefer to not use braces only on a simple if statements (like old-style preconditions) but only when there is no else blocks. Is this consistent with .NET foundation bracing rules?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, if the if statement requires braces then the else statement must also use braces (and vice-versa). This will eventually be enforced by DotNetAnalyzers/StyleCopAnalyzers#716 (which provides document-, project-, and solution-wide automatic fixes), whether or not codeformatter.exe handles it in this pull request.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems I didn't communicate my thoughts correctly. I'll try once more.

My rules: use curly braces in all cases. The only exception is simple if-statements without else blocks for short one liners like argument validation.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

StyleCopAnalyzers and StyleCop do not currently have a rule to enforce this, though one could certainly be proposed. However, there are a couple additional things to keep in mind:

  1. I'm very much hoping that the Code Contracts projects can be moved from the Microsoft organization to the dotnet organization. If it does move here, it would make sense to use the formatting rules of other projects in that organization even if they deviate somewhat from our personal preferences (they differ from my own preference in the indentation of case statements).
  2. The initial formatting is being done with dotnet/codeformatter (both in support of the first item and because it is compatible with Visual Studio's default formatting settings) so strict brace inclusion rules might be best saved for a later time.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, I'm just curios how far my personal preferences from proposed once:) And yep, moving to dotnet organization makes a lot of sense. I'll talk to someone to understand how to do this.

this.EndTestInternal(options);
else
this.BeginTestInternal(options);
}

if (this.orderReversed)
this.BeginTestInternal(options);
else
this.EndTestInternal(options);
}
public void EndTest(Options options)
{
if (skipTest(options))
return;

private void BeginTestInternal(Options options)
{
try
{
if (this.testAsyncResults == null)
this.testAsyncResults = new Dictionary<string, IAsyncResult>();
if (!beginTestsProcessed)
orderReversed = true;

if (this.waitHandles == null)
this.waitHandles = new WaitHandle[this.maxWaitHandles];
if (orderReversed)
this.BeginTestInternal(options);
else
this.EndTestInternal(options);
}

var index = nbWaitHandles;
if (index == waitHandles.Length)
private void BeginTestInternal(Options options)
{
index = WaitHandle.WaitAny(waitHandles, waitHandles.Length * SingleTestMaxWait);
Assert.AreNotEqual(index, WaitHandle.WaitTimeout, "Previous tests timed out");
this.nbWaitHandles--;
try
{
if (testAsyncResults == null)
testAsyncResults = new Dictionary<string, IAsyncResult>();

if (waitHandles == null)
waitHandles = new WaitHandle[maxWaitHandles];

var index = nbWaitHandles;
if (index == waitHandles.Length)
{
index = WaitHandle.WaitAny(waitHandles, waitHandles.Length * SingleTestMaxWait);
Assert.AreNotEqual(index, WaitHandle.WaitTimeout, "Previous tests timed out");
nbWaitHandles--;
}

Exception dummyOutException;
string dummyOutString;
var asyncResult = actionDelegate.BeginInvoke(options, out dummyOutException, out dummyOutString, null, null);
testAsyncResults.Add(options.TestName, asyncResult);
waitHandles[index] = asyncResult.AsyncWaitHandle;
nbWaitHandles++;

Console.WriteLine(this.BeginMessage);
}
catch (Exception e)
{
Console.WriteLine("EXCEPTION: {0}", e.Message);
Assert.Fail("Exception caught");
}
}

Exception dummyOutException;
string dummyOutString;
var asyncResult = this.actionDelegate.BeginInvoke(options, out dummyOutException, out dummyOutString, null, null);
this.testAsyncResults.Add(options.TestName, asyncResult);
this.waitHandles[index] = asyncResult.AsyncWaitHandle;
this.nbWaitHandles++;

Console.WriteLine(this.BeginMessage);
}
catch (Exception e)
{
Console.WriteLine("EXCEPTION: {0}", e.Message);
Assert.Fail("Exception caught");
}
}

private void EndTestInternal(Options options)
{
Assert.IsNotNull(this.testAsyncResults, "Begin part of the test not selected");
private void EndTestInternal(Options options)
{
Assert.IsNotNull(testAsyncResults, "Begin part of the test not selected");

IAsyncResult asyncResult;
if (!this.testAsyncResults.TryGetValue(options.TestName, out asyncResult))
Assert.Fail("Begin part of the test not run");
IAsyncResult asyncResult;
if (!testAsyncResults.TryGetValue(options.TestName, out asyncResult))
Assert.Fail("Begin part of the test not run");

this.testAsyncResults.Remove(options.TestName);
testAsyncResults.Remove(options.TestName);

Assert.IsTrue(asyncResult.AsyncWaitHandle.WaitOne(SingleTestMaxWait), "Test timed out");
Assert.IsTrue(asyncResult.AsyncWaitHandle.WaitOne(SingleTestMaxWait), "Test timed out");

Exception exceptionThrown;
string dataReceived;
this.actionDelegate.EndInvoke(out exceptionThrown, out dataReceived, asyncResult);
Exception exceptionThrown;
string dataReceived;
actionDelegate.EndInvoke(out exceptionThrown, out dataReceived, asyncResult);

Console.WriteLine();
Console.WriteLine("This test case was performed {0}synchronously", asyncResult.CompletedSynchronously ? "" : "a");
Console.WriteLine();
Console.WriteLine();
Console.WriteLine("This test case was performed {0}synchronously", asyncResult.CompletedSynchronously ? "" : "a");
Console.WriteLine();

Console.Write(dataReceived);
if (exceptionThrown != null)
throw exceptionThrown;
}
Console.Write(dataReceived);
if (exceptionThrown != null)
throw exceptionThrown;
}



private void ActionAsIsolated(Options options, out Exception exceptionThrown, out string dataReceived)
{
using (var stringWriter = new StringWriter())
{
var output = new Output(String.Format("Isolated::{0}", options.TestName), stringWriter);
exceptionThrown = null;
try
private void ActionAsIsolated(Options options, out Exception exceptionThrown, out string dataReceived)
{
this.action(options, output);
using (var stringWriter = new StringWriter())
{
var output = new Output(String.Format("Isolated::{0}", options.TestName), stringWriter);
exceptionThrown = null;
try
{
action(options, output);
}
catch (Exception e)
{
exceptionThrown = e;
}
dataReceived = stringWriter.ToString();
}
}
catch (Exception e)
{
exceptionThrown = e;
}
dataReceived = stringWriter.ToString();
}
}

}
}
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,52 @@
<Reference Include="System.Xml.Linq" />
</ItemGroup>
<ItemGroup>
<Compile Include="v.cs" />
<None Include="Sources\ArrayForAll.cs" />
<None Include="Sources\AssumeInvariant.cs" />
<None Include="Sources\Decimal.cs" />
<None Include="Sources\DoubleZero.cs" />
<None Include="Sources\EnumerableAll.cs" />
<None Include="Sources\ForAll.cs" />
<None Include="Sources\HeapCrash.cs" />
<None Include="Sources\Herman.cs" />
<None Include="Sources\IOperations.cs" />
<None Include="Sources\Mulder.cs" />
<None Include="Sources\MultidimArrays.cs" />
<None Include="Sources\OperatorOverloading.cs" />
<None Include="Sources\TypeSpecializations.cs" />
<None Include="Sources\Z3Test1.cs" />
<None Include="Sources\z3test10.cs" />
<None Include="Sources\z3test11.cs" />
<None Include="Sources\z3test12.cs" />
<None Include="Sources\z3test13.cs" />
<None Include="Sources\z3test14.cs" />
<None Include="Sources\z3test15.cs" />
<None Include="Sources\z3test16.cs" />
<None Include="Sources\z3test17.cs" />
<None Include="Sources\z3test18.cs" />
<None Include="Sources\z3test19.cs" />
<None Include="Sources\z3Test2.cs" />
<None Include="Sources\z3test20.cs" />
<None Include="Sources\z3test21.cs" />
<None Include="Sources\z3test22.cs" />
<None Include="Sources\z3test23.cs" />
<None Include="Sources\z3test3.cs" />
<None Include="Sources\z3test4.cs" />
<None Include="Sources\z3test5.cs" />
<None Include="Sources\z3test6.cs" />
<None Include="Sources\z3test7.cs" />
<None Include="Sources\z3test8.cs" />
<None Include="Sources\z3test9.cs" />
<None Include="..\TestFrameworkOOB\Purity.cs">
<Link>Sources\Purity.cs</Link>
</None>
<None Include="..\TestFrameworkOOB\ReferenceToAllOOBC.cs">
<Link>Sources\ReferenceToAllOOBC.cs</Link>
</None>
<None Include="..\TestFrameworkOOB\UserFeedback.cs">
<Link>Sources\UserFeedback.cs</Link>
</None>
<Compile Include="Tests.cs" />
<None Include="..\Containers\TestContainers\ArrayWithNonNullAnalysis.cs">
<Link>Sources\ArrayWithNonNullAnalysis.cs</Link>
</None>
Expand All @@ -152,6 +197,7 @@
<Compile Include="Properties\AssemblyInfo.cs" />
<None Include="Sources\Abbreviators.cs" />
<None Include="Sources\ClassWithProtocolFinal.cs" />
<None Include="Sources\makefile" />
<None Include="Sources\NoUpHavocMethods.cs" />
<None Include="Sources\IfaceImplicitlyImplementedBug.cs" />
<Compile Include="TestDriver.cs" />
Expand Down
Loading