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
5 changes: 4 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@

#CCRewrite Test folder
Foxtrot/Tests/Sources/bin/
Foxtrot/Tests/QuickGraph/QuickGraphBinaries/
Foxtrot/Tests/RewriteExistingBinaries/

# CodeContracts installer
Microsoft.Research/ManagedContract.Setup/devlab9ts/
Expand Down
76 changes: 76 additions & 0 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
# Contributor Guide

## Open Discussion

The most important part of an open source project is *open discussion*. If a developer, user, or other contributor has
a question, comment, suggestion, or concern about any part of this project, **please speak up**: create an issue, add
a comment to an existing issue or pull request or ask a question at jabber chat room at https://jabbr.net/#/rooms/CodeContracts.

This policy especially affects the emoji described below. Any user or contributor may freely use these symbols to
clarify intent during discussions. Questions and concerns from first-time contributors matter just as much as questions
and concerns from the original project developers.

## License

The code in this repository is licensed under the MIT license. A complete description of the license, as well as license
notices for 3rd-party code incorporated into this project, is available in the repository:

* [LICENSE](https://github.com/Microsoft/CodeContracts/blob/master/LICENSE.txt)

## Labels

This project uses many labels for categorizing issues and pull requests.

| Label | Meaning on Issue | Meaning on Pull Request |
| --- | --- | --- |
|contract issue| The issue concerns an incorrect or missing contract in the reference source code. | n/a |
| bug | The issue concerns a bug in the code | The issue concerns a bug in the code |
| enhancement | The issue is an improvement to the code | The pull request is an improvement to the code |
| up for grabs | The issue is not assigned to a particular person. If you want to work on it, just add a comment saying so and it's yours! | Normally not applicable (see comments if observed on a pull request) |
| question | The issue is a question | Normally not applicable (see comments if observed on a pull request) |
| code review | n/a | The pull request is under review |
| needs discussion | The issue needs further discussion before an actionable decision can be made | The pull request needs further discussion before an actionable decision can be made |
| pull request | A pull request intended to address the issue has been created, but not yet merged | n/a |
| blocked | The issue cannot be fixed until another issue, which may be external, is addressed | The pull request cannot be merged until another issue, which may be external, is addressed |
| do not merge | n/a | The pull request should not be merged at this time. This could indicate a work-in-progress, a problem in the implementation code, or cases where the pull request depends on (is blocked by) another issue or pull request which has not been addressed. |
| in progress | A developer is currently working on the issue | A developer is currently making updates to the code in the pull request |
| fixed | The issue has been resolved | The pull request describes a new issue (i.e. no separate issue exists), and the content of the pull request was merged to fix the issue |
| duplicate | Another issue or pull request contains the original report for this topic | Another pull request was submitted to correct the issue. This is generally only applied to pull requests after another pull request to correct the issue is merged. |
| wontfix | The issue will not be corrected. The current behavior could be by design, out of scope, or cannot be changed due to the breaking changes policy for the project (see comments for details). | The pull request will not be merged due to a fundamental issue (see description for this label on issues) |

## Emoji

GitHub provides several emoji which can be included in many areas of the site, especially including comments on issues
and pull requests. To reduce confusion during evaluation of a pull request, the following emoji convey special intent.

* :question: (`:question:`) Indicates a question. This emoji comes with **no strings attached**, which means it's fine
to simply answer the question in another comment without making any changes to code.

In general, pull requests with an unanswered question will not be merged until *someone* addresses it. This could be
the original creator of the issue or pull request, another contributor to the project, or even the person who asked
the question.

* :exclamation: (`:exclamation:`) Indicates a problem with the code which will need to be addressed before changes can
be merged into `master`. This *may* be accompanied by a specific suggestion for how to change the code. Any
contributor is completely welcome to open a discussion regarding alternative solutions, even if the originally
proposed change has already been made.

Every active contributor to a project is likely to use the :exclamation: emoji (or similar) due to a simple
misunderstanding or oversight in their evaluation. **This is absolutely fine.** If you notice a case like this, simply
add a comment to clarify the intent and the exclamation can be considered resolved.

Pull requests with an unresolved exclamation will not be merged until they are addressed by either a change in the
code or a detailed explanation. While it is possible for code with an exclamation to be merged, this will usually only
occur if *all* of the following conditions hold:

* The rationale is fully and clearly explained
* The code corrects an issue that is likely to affect users
* All other proposed solutions are either too time-consuming to implement or are equally (or more) problematic

* :bulb: (`:bulb:`) Indicates an idea or suggestion regarding a potential change in the code. These items will not
necessarily block the inclusion of code into the `master` branch, especially in cases where suggestions are trivial
and no other issues were found during code review.

In certain trivial cases (e.g. a simple formatting change), a core contributor on the project may make the suggested
change themselves in the process of merging a pull request. Like the :exclamation: emoji, :bulb: suggestions invite
open discussion about alternative solutions from any contributor.
32 changes: 15 additions & 17 deletions Foxtrot/Foxtrot/Extractor.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2326,6 +2326,7 @@ public Block Apply(Block block) {
return result;
}
}

/// <summary>
/// Use the same assumption as the extractor for a non-iterator method: the preambles are
/// in the first block.
Expand All @@ -2350,14 +2351,14 @@ StatementList GetContractClumpFromMoveNext(Method iteratorMethod, Method moveNex
{
linkerVersion = iteratorMethod.DeclaringType.DeclaringModule.LinkerMajorVersion;
}
var isRoslyn = linkerVersion == 48;
var initialState = moveNext.IsAsync && !isRoslyn ? -1 : 0;

var initialState = moveNext.IsAsync ? -1 : 0;
moveNext.MoveNextStartState = initialState;
originalContractPosition = null;
int statementIndex;
Contract.Assume(moveNext.Body != null);
Contract.Assume(moveNext.Body.Statements != null);
int blockIndex = ContractStartInMoveNext(this.contractNodes, moveNext, out statementIndex, iteratorMethod, isRoslyn);
int blockIndex = ContractStartInMoveNext(this.contractNodes, moveNext, out statementIndex, iteratorMethod);
Contract.Assert(statementIndex >= 0, "should follow from the postcondiiton");
if (blockIndex < 0) {
// Couldn't find state 0 in MoveNext method
Expand Down Expand Up @@ -2504,15 +2505,12 @@ enum EvalKind { None = 0, IsStateValue, IsFinalCompare, IsDisposingTest }
/// - assignment to state
/// - unconditional branch
///
/// Wrinkle: in Rosly, the initial async state is also 0, not -1.
/// The context uses the linker version to determine if this assembly was Roslyn generated.
///
/// Another wrinkle is async methods that are not really async and C# still emits a closure etc, but
/// Wrinkle is async methods that are not really async and C# still emits a closure etc, but
/// the method does not test the async state at all.
/// </summary>
[ContractVerification(true)]
[Pure]
static int ContractStartInMoveNext(ContractNodes contractNodes, Method moveNext, out int statementIndex, Method origMethod, bool isRoslyn)
static int ContractStartInMoveNext(ContractNodes contractNodes, Method moveNext, out int statementIndex, Method origMethod)
{
Contract.Requires(contractNodes != null);
Contract.Requires(moveNext != null);
Expand Down Expand Up @@ -2565,7 +2563,7 @@ static int ContractStartInMoveNext(ContractNodes contractNodes, Method moveNext,
lastBranchNonConditional = true;
goto OuterLoop;
}
var value = EvaluateExpression(branch.Condition, env, seenFinalCompare, isAsync, isRoslyn);
var value = EvaluateExpression(branch.Condition, env, seenFinalCompare, isAsync);
if (value.Two == EvalKind.IsDisposingTest)
{
if (value.One != 0)
Expand Down Expand Up @@ -2619,7 +2617,7 @@ static int ContractStartInMoveNext(ContractNodes contractNodes, Method moveNext,
statementIndex = i;
return currentBlockIndex;
}
var value = EvaluateExpression(swtch.Expression, env, seenFinalCompare, isAsync, isRoslyn);
var value = EvaluateExpression(swtch.Expression, env, seenFinalCompare, isAsync);
if (value.One < 0 || swtch.Targets == null || value.One >= swtch.Targets.Count)
{
// fall through
Expand Down Expand Up @@ -2649,7 +2647,7 @@ static int ContractStartInMoveNext(ContractNodes contractNodes, Method moveNext,
statementIndex = i;
return currentBlockIndex;
}
var value = EvaluateExpression(assign.Source, env, seenFinalCompare, isAsync, isRoslyn);
var value = EvaluateExpression(assign.Source, env, seenFinalCompare, isAsync);
if (IsThisDotState(assign.Target))
{
// end of trace
Expand Down Expand Up @@ -2702,7 +2700,7 @@ static int ContractStartInMoveNext(ContractNodes contractNodes, Method moveNext,
break;

default:
Contract.Assume(false);
Contract.Assume(false, string.Format("Unexpected node type '{0}'", stmt.NodeType));
return -1;
}
}
Expand Down Expand Up @@ -2748,15 +2746,15 @@ static bool IsDoFinallyBodies(Expression expression)
}

[ContractVerification(true)]
static private Pair<int, EvalKind> EvaluateExpression(Expression expression, Dictionary<Variable, Pair<int, EvalKind>> env, bool ignoreUnknown, bool isAsync, bool isRoslyn)
static private Pair<int, EvalKind> EvaluateExpression(Expression expression, Dictionary<Variable, Pair<int, EvalKind>> env, bool ignoreUnknown, bool isAsync)
{
Contract.Requires(env != null);

var binary = expression as BinaryExpression;
if (binary != null)
{
var op1 = EvaluateExpression(binary.Operand1, env, ignoreUnknown, isAsync, isRoslyn);
var op2 = EvaluateExpression(binary.Operand2, env, ignoreUnknown, isAsync, isRoslyn);
var op1 = EvaluateExpression(binary.Operand1, env, ignoreUnknown, isAsync);
var op2 = EvaluateExpression(binary.Operand2, env, ignoreUnknown, isAsync);
var resultKind = CombineEvalKind(ref op1, ref op2);
switch (binary.NodeType)
{
Expand Down Expand Up @@ -2791,7 +2789,7 @@ static private Pair<int, EvalKind> EvaluateExpression(Expression expression, Dic
var unary = expression as UnaryExpression;
if (unary != null)
{
var op = EvaluateExpression(unary.Operand, env, ignoreUnknown, isAsync, isRoslyn);
var op = EvaluateExpression(unary.Operand, env, ignoreUnknown, isAsync);
var resultKind = EvalKind.None;
if (op.Two == EvalKind.IsDisposingTest)
{
Expand Down Expand Up @@ -2830,7 +2828,7 @@ static private Pair<int, EvalKind> EvaluateExpression(Expression expression, Dic
return Pair.For(0, EvalKind.IsDisposingTest);
}
if (name.Contains("<>") && name.Contains("__state")) {
var initialState = isAsync && !isRoslyn ? -1 : 0;
var initialState = isAsync ? -1 : 0;
return Pair.For(initialState, EvalKind.IsStateValue);
}
}
Expand Down
9 changes: 8 additions & 1 deletion Foxtrot/Foxtrot/Utility.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2317,7 +2317,14 @@ public override void VisitConstruct(Construct cons)
} else
{
//Console.WriteLine("Not atomic closure part: {0}", m.FullName);
Debug.Assert(m.DeclaringType.Name.Name.Contains("DisplayClass") || !m.Name.Name.Contains("__"));
var declaringTypeName = m.DeclaringType.Name.Name;
var name = m.Name.Name;
string message =
string.Format(
"DeclaringName should contain 'DisplayClass' or Name should not have '__'. \r\nDeclaringTypeName: {0}, Name: {1}",
declaringTypeName, name);

Debug.Assert(declaringTypeName.Contains("DisplayClass") || !name.Contains("__"), message);
}
}
}
Expand Down
20 changes: 19 additions & 1 deletion Foxtrot/Tests/RewriterTests.cs
Original file line number Diff line number Diff line change
Expand Up @@ -199,17 +199,35 @@ public void BuildRewriteRunFromSourcesV45()
[DeploymentItem("Foxtrot\\Tests\\TestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\TestInputs.xml", "TestFile", DataAccessMethod.Sequential)]
[TestMethod]
[TestCategory("Runtime"), TestCategory("CoreTest"), TestCategory("Roslyn"), TestCategory("V4.5")]
[Ignore()] // Old Roslyn bits are not compatible with CCRewrite. Test (and old binaries) should be removed in the next iteration.
public void BuildRewriteRunFromSourcesRoslynV45()
{
var options = new Options(this.TestContext);
options.IsRoslyn = true;
options.IsLegacyRoslyn = true;
options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName));
options.BuildFramework = @"Roslyn\v4.5";
options.ReferencesFramework = @".NetFramework\v4.5";
options.ContractFramework = @".NETFramework\v4.0";
options.UseTestHarness = true;
TestDriver.BuildRewriteRun(options);
}

[DeploymentItem("Foxtrot\\Tests\\TestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\TestInputs.xml", "TestFile", DataAccessMethod.Sequential)]
[TestMethod]
[TestCategory("Runtime"), TestCategory("CoreTest"), TestCategory("Roslyn"), TestCategory("VS14")]
public void BuildRewriteRunFromSourcesRoslynVS14RC()
{
var options = new Options(this.TestContext);
// For VS14RC+ version compiler name is the same Csc.exe, and behavior from async/iterator perspective is similar
// to old compiler as well. That's why IsLegacyRoslyn should be false in this test case.
options.IsLegacyRoslyn = false;
options.FoxtrotOptions = options.FoxtrotOptions + String.Format(" /throwonfailure /rw:{0}.exe,TestInfrastructure.RewriterMethods", Path.GetFileNameWithoutExtension(options.TestName));
options.BuildFramework = @"Roslyn\VS14RC";
options.ReferencesFramework = @".NetFramework\v4.5";
options.ContractFramework = @".NETFramework\v4.0";
options.UseTestHarness = true;
TestDriver.BuildRewriteRun(options);
}


[DeploymentItem("Foxtrot\\Tests\\TestInputs.xml"), DataSource("Microsoft.VisualStudio.TestTools.DataSource.XML", "|DataDirectory|\\TestInputs.xml", "TestFile", DataAccessMethod.Sequential)]
Expand Down
1 change: 1 addition & 0 deletions Foxtrot/Tests/Sources/async6.cs
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ public static async Task<int> CountThem<T>(T[] values, T other)

var x = values.Length;
if (x == 4) throw new ArgumentException();
await Task.Delay(42);
return x;
}
}
Expand Down
17 changes: 12 additions & 5 deletions Foxtrot/Tests/TestDriver.cs
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,10 @@ internal static object Rewrite(string absoluteSourceDir, string absoluteBinary,
{
if (options.MustSucceed)
{
if (capture.ExitCode != 0)
{
Console.WriteLine("");
}
Assert.AreEqual(0, capture.ExitCode, "{0} returned an errorcode of {1}.", FoxtrotExe, capture.ExitCode);
}
return capture;
Expand Down Expand Up @@ -447,7 +451,10 @@ public string TestName
}
}

public bool IsRoslyn { get; set; }
/// <summary>
/// Should be true, if old (pre-RC) Roslyn compiler needs to be used.
/// </summary>
public bool IsLegacyRoslyn { get; set; }

public string Compiler
{
Expand All @@ -456,7 +463,7 @@ public string Compiler
switch (compilerCode)
{
case "VB":
if (IsRoslyn)
if (IsLegacyRoslyn)
{
return "rvbc.exe";
}
Expand All @@ -465,7 +472,7 @@ public string Compiler
return "vbc.exe";
}
default:
if (IsRoslyn)
if (IsLegacyRoslyn)
{
return "rcsc.exe";
}
Expand All @@ -478,14 +485,14 @@ public string Compiler
}

bool IsV40 { get { return this.BuildFramework.Contains("v4.0"); } }
bool IsV45 { get { return this.BuildFramework.Contains("v4.5"); } }
bool IsV45 { get { return this.BuildFramework.Contains("v4.5") || BuildFramework.Contains("VS14"); } }
bool IsSilverlight { get { return this.BuildFramework.Contains("Silverlight"); } }

string Moniker
{
get
{
if (!IsRoslyn) { return FrameworkMoniker; }
if (!IsLegacyRoslyn) { return FrameworkMoniker; }
if (compilerCode == "VB")
{
return FrameworkMoniker + ",ROSLYN";
Expand Down
6 changes: 3 additions & 3 deletions Foxtrot/Tests/UnitTests/RewrittenContractTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,6 @@ private static int RunProcess(string cwd, string tool, string arguments)
[AssemblyInitialize]
public static void AssembyInitialize(TestContext context)
{

//
// VERY IMPORTANT!! Do NOT do anything that caused any type from CodeUnderTest.dll to be loaded
// before the assembly is rewritten!!!
Expand All @@ -86,8 +85,9 @@ public static void AssembyInitialize(TestContext context)
var deploymentDir = Directory.GetCurrentDirectory();

var testResultPosition = deploymentDir.IndexOf(@"TestResults");

Assert.IsTrue(testResultPosition != -1, "Can't find the TestResults directory!!!");

Assert.IsTrue(testResultPosition != -1,
string.Format("Can't find the TestResults directory!!! Current deployment directory is '{0}'", deploymentDir));

var testDirRoot = deploymentDir.Substring(0, testResultPosition);

Expand Down
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
<?xml version ="1.0"?>
<configuration>
<startup useLegacyV2RuntimeActivationPolicy="true">
<requiredRuntime safemode="true" imageVersion="v4.0.30319" version="v4.0.30319"/>
</startup>
</configuration>
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Roslyn bits was taken from installed VS14RC.
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
<?xml version ="1.0"?>
<configuration>
<startup useLegacyV2RuntimeActivationPolicy="true">
<supportedRuntime version="v4.0.30319"/>
</startup>
</configuration>
Loading