Skip to content

Commit

Permalink
Add initial support for method contracts via requires and ensures
Browse files Browse the repository at this point in the history
  • Loading branch information
Daniel-Svensson committed Feb 7, 2016
1 parent 33e2491 commit 8611f3a
Show file tree
Hide file tree
Showing 13 changed files with 278 additions and 5 deletions.
3 changes: 2 additions & 1 deletion src/Compilers/CSharp/Portable/CSharpCodeAnalysis.csproj
Original file line number Diff line number Diff line change
Expand Up @@ -380,6 +380,7 @@
<Compile Include="Lowering\AsyncRewriter\AsyncRewriter.cs" />
<Compile Include="Lowering\AsyncRewriter\AsyncStateMachine.cs" />
<Compile Include="Lowering\AsyncRewriter\AwaitExpressionSpiller.cs" />
<Compile Include="Lowering\MethodContractRewriter.cs" />
<Compile Include="Lowering\DiagnosticsPass_ExpressionTrees.cs" />
<Compile Include="Lowering\DiagnosticsPass_Warnings.cs" />
<Compile Include="Lowering\Extensions.cs" />
Expand Down Expand Up @@ -901,4 +902,4 @@
<ImportGroup Label="Targets">
<Import Project="..\..\..\..\build\Targets\VSL.Imports.targets" />
</ImportGroup>
</Project>
</Project>
11 changes: 11 additions & 0 deletions src/Compilers/CSharp/Portable/Compiler/MethodCompiler.cs
Original file line number Diff line number Diff line change
Expand Up @@ -907,6 +907,17 @@ private void CompileMethod(

importChain = importChain ?? processedInitializers.FirstImportChain;

var sourceMemberMethod = methodSymbol as SourceMemberMethodSymbol;
if (sourceMemberMethod != null)
{
var syntax = sourceMemberMethod.GetSyntax();
var contract = syntax.MethodContract;
if (contract != null)
{
body = MethodContractRewriter.Rewrite(sourceMethod, contract, body, compilationState, diagsForCurrentMethod);
}
}

// Associate these debug imports with all methods generated from this one.
compilationState.CurrentImportChain = importChain;

Expand Down
42 changes: 42 additions & 0 deletions src/Compilers/CSharp/Portable/Lowering/MethodContractRewriter.cs
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using Microsoft.CodeAnalysis.CSharp.Symbols;
using Microsoft.CodeAnalysis.CSharp.Syntax;

namespace Microsoft.CodeAnalysis.CSharp
{
internal static class MethodContractRewriter
{
internal static BoundBlock Rewrite(SourceMethodSymbol sourceMethodSymbol, MethodContractSyntax contract, BoundBlock body, TypeCompilationState compilationState, DiagnosticBag diagsForCurrentMethod)
{
var binder = compilationState.Compilation.GetBinderFactory(sourceMethodSymbol.SyntaxTree)
.GetBinder(body.Syntax);
SyntheticBoundNodeFactory factory = new SyntheticBoundNodeFactory(sourceMethodSymbol, sourceMethodSymbol.SyntaxNode, compilationState, diagsForCurrentMethod);
var contractType = compilationState.Compilation.GetTypeByReflectionType(typeof(System.Diagnostics.Contracts.Contract), diagsForCurrentMethod);

var contractStatements = ArrayBuilder<BoundStatement>.GetInstance(contract.Requires.Count);
foreach (var requires in contract.Requires)
{
var condition = binder.BindExpression(requires.Condition, diagsForCurrentMethod);

var methodCall = factory.StaticCall(contractType, "Requires", condition);
var statement = factory.ExpressionStatement(methodCall);

contractStatements.Add(statement);
}
foreach (var requires in contract.Ensures)
{
var condition = binder.BindExpression(requires.Condition, diagsForCurrentMethod);
var methodCall = factory.StaticCall(contractType, "Ensures", condition);
var statement = factory.ExpressionStatement(methodCall);

contractStatements.Add(statement);
}

return body.Update(body.Locals, body.Statements.InsertRange(0, contractStatements.ToImmutableAndFree()));
}
}
}
57 changes: 57 additions & 0 deletions src/Compilers/CSharp/Portable/Parser/LanguageParser.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2966,6 +2966,10 @@ private MethodDeclarationSyntax ParseMethodDeclaration(
constraints[0] = this.AddErrorToFirstToken(constraints[0], ErrorCode.ERR_OverrideWithConstraints);
}

var contract = (this.CurrentToken.ContextualKind == SyntaxKind.RequiresKeyword
|| this.CurrentToken.ContextualKind == SyntaxKind.EnsuresKeyword) ?
ParseMethodContract() : null;

_termState = saveTerm;

BlockSyntax blockBody;
Expand All @@ -2992,6 +2996,7 @@ private MethodDeclarationSyntax ParseMethodDeclaration(
typeParameterList,
paramList,
constraints,
contract,
blockBody,
expressionBody,
semicolon);
Expand All @@ -3007,6 +3012,58 @@ private MethodDeclarationSyntax ParseMethodDeclaration(
}
}

private MethodContractSyntax ParseMethodContract()
{
var requires = default(SyntaxListBuilder<RequiresDeclarationSyntax>);
var ensures = default(SyntaxListBuilder<EnsuresDeclarationSyntax>);

if (this.CurrentToken.ContextualKind == SyntaxKind.RequiresKeyword)
{
requires = _pool.Allocate<RequiresDeclarationSyntax>();
do
{
requires.Add(ParseRequiresDeclarationSyntax());
} while (this.CurrentToken.ContextualKind == SyntaxKind.RequiresKeyword);
}

if (this.CurrentToken.ContextualKind == SyntaxKind.EnsuresKeyword)
{
ensures = _pool.Allocate<EnsuresDeclarationSyntax>();
do
{
ensures.Add(ParseEnsuresDeclarationSyntax());
} while (this.CurrentToken.ContextualKind == SyntaxKind.EnsuresKeyword);
}

// Error on requires after ensures
if (this.CurrentToken.ContextualKind == SyntaxKind.RequiresKeyword)
{
this.AddErrorToFirstToken(this.CurrentToken, ErrorCode.ERR_UnexpectedToken, this.CurrentToken.Text);
}

return _syntaxFactory.MethodContract(requires, ensures);
}


private RequiresDeclarationSyntax ParseRequiresDeclarationSyntax()
{
Debug.Assert(this.CurrentToken.ContextualKind == SyntaxKind.RequiresKeyword);
var requires = this.EatContextualToken(SyntaxKind.RequiresKeyword);
var condition = this.ParseExpressionCore();

return _syntaxFactory.RequiresDeclaration(requires, condition);
}


private EnsuresDeclarationSyntax ParseEnsuresDeclarationSyntax()
{
Debug.Assert(this.CurrentToken.ContextualKind == SyntaxKind.EnsuresKeyword);
var ensures = this.EatContextualToken(SyntaxKind.EnsuresKeyword);
var condition = this.ParseExpressionCore();

return _syntaxFactory.EnsuresDeclaration(ensures, condition);
}

private TypeSyntax ParseReturnType()
{
var saveTerm = _termState;
Expand Down
4 changes: 0 additions & 4 deletions src/Compilers/CSharp/Portable/PublicAPI.Shipped.txt
Original file line number Diff line number Diff line change
Expand Up @@ -1240,7 +1240,6 @@ Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax.ExpressionBody.get
Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax.Identifier.get -> Microsoft.CodeAnalysis.SyntaxToken
Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax.ReturnType.get -> Microsoft.CodeAnalysis.CSharp.Syntax.TypeSyntax
Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax.TypeParameterList.get -> Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterListSyntax
Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax.Update(Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.AttributeListSyntax> attributeLists, Microsoft.CodeAnalysis.SyntaxTokenList modifiers, Microsoft.CodeAnalysis.CSharp.Syntax.TypeSyntax returnType, Microsoft.CodeAnalysis.CSharp.Syntax.ExplicitInterfaceSpecifierSyntax explicitInterfaceSpecifier, Microsoft.CodeAnalysis.SyntaxToken identifier, Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterListSyntax typeParameterList, Microsoft.CodeAnalysis.CSharp.Syntax.ParameterListSyntax parameterList, Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterConstraintClauseSyntax> constraintClauses, Microsoft.CodeAnalysis.CSharp.Syntax.BlockSyntax body, Microsoft.CodeAnalysis.CSharp.Syntax.ArrowExpressionClauseSyntax expressionBody, Microsoft.CodeAnalysis.SyntaxToken semicolonToken) -> Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax
Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax.WithAttributeLists(Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.AttributeListSyntax> attributeLists) -> Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax
Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax.WithBody(Microsoft.CodeAnalysis.CSharp.Syntax.BlockSyntax body) -> Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax
Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax.WithConstraintClauses(Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterConstraintClauseSyntax> constraintClauses) -> Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax
Expand Down Expand Up @@ -3718,9 +3717,6 @@ static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.MemberBindingExpression(Micro
static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.MemberBindingExpression(Microsoft.CodeAnalysis.SyntaxToken operatorToken, Microsoft.CodeAnalysis.CSharp.Syntax.SimpleNameSyntax name) -> Microsoft.CodeAnalysis.CSharp.Syntax.MemberBindingExpressionSyntax
static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.MethodDeclaration(Microsoft.CodeAnalysis.CSharp.Syntax.TypeSyntax returnType, Microsoft.CodeAnalysis.SyntaxToken identifier) -> Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax
static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.MethodDeclaration(Microsoft.CodeAnalysis.CSharp.Syntax.TypeSyntax returnType, string identifier) -> Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax
static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.MethodDeclaration(Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.AttributeListSyntax> attributeLists, Microsoft.CodeAnalysis.SyntaxTokenList modifiers, Microsoft.CodeAnalysis.CSharp.Syntax.TypeSyntax returnType, Microsoft.CodeAnalysis.CSharp.Syntax.ExplicitInterfaceSpecifierSyntax explicitInterfaceSpecifier, Microsoft.CodeAnalysis.SyntaxToken identifier, Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterListSyntax typeParameterList, Microsoft.CodeAnalysis.CSharp.Syntax.ParameterListSyntax parameterList, Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterConstraintClauseSyntax> constraintClauses, Microsoft.CodeAnalysis.CSharp.Syntax.BlockSyntax body, Microsoft.CodeAnalysis.CSharp.Syntax.ArrowExpressionClauseSyntax expressionBody) -> Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax
static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.MethodDeclaration(Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.AttributeListSyntax> attributeLists, Microsoft.CodeAnalysis.SyntaxTokenList modifiers, Microsoft.CodeAnalysis.CSharp.Syntax.TypeSyntax returnType, Microsoft.CodeAnalysis.CSharp.Syntax.ExplicitInterfaceSpecifierSyntax explicitInterfaceSpecifier, Microsoft.CodeAnalysis.SyntaxToken identifier, Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterListSyntax typeParameterList, Microsoft.CodeAnalysis.CSharp.Syntax.ParameterListSyntax parameterList, Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterConstraintClauseSyntax> constraintClauses, Microsoft.CodeAnalysis.CSharp.Syntax.BlockSyntax body, Microsoft.CodeAnalysis.CSharp.Syntax.ArrowExpressionClauseSyntax expressionBody, Microsoft.CodeAnalysis.SyntaxToken semicolonToken) -> Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax
static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.MethodDeclaration(Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.AttributeListSyntax> attributeLists, Microsoft.CodeAnalysis.SyntaxTokenList modifiers, Microsoft.CodeAnalysis.CSharp.Syntax.TypeSyntax returnType, Microsoft.CodeAnalysis.CSharp.Syntax.ExplicitInterfaceSpecifierSyntax explicitInterfaceSpecifier, Microsoft.CodeAnalysis.SyntaxToken identifier, Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterListSyntax typeParameterList, Microsoft.CodeAnalysis.CSharp.Syntax.ParameterListSyntax parameterList, Microsoft.CodeAnalysis.SyntaxList<Microsoft.CodeAnalysis.CSharp.Syntax.TypeParameterConstraintClauseSyntax> constraintClauses, Microsoft.CodeAnalysis.CSharp.Syntax.BlockSyntax body, Microsoft.CodeAnalysis.SyntaxToken semicolonToken) -> Microsoft.CodeAnalysis.CSharp.Syntax.MethodDeclarationSyntax
static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.MissingToken(Microsoft.CodeAnalysis.CSharp.SyntaxKind kind) -> Microsoft.CodeAnalysis.SyntaxToken
static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.MissingToken(Microsoft.CodeAnalysis.SyntaxTriviaList leading, Microsoft.CodeAnalysis.CSharp.SyntaxKind kind, Microsoft.CodeAnalysis.SyntaxTriviaList trailing) -> Microsoft.CodeAnalysis.SyntaxToken
static Microsoft.CodeAnalysis.CSharp.SyntaxFactory.NameColon(Microsoft.CodeAnalysis.CSharp.Syntax.IdentifierNameSyntax name) -> Microsoft.CodeAnalysis.CSharp.Syntax.NameColonSyntax
Expand Down
Loading

0 comments on commit 8611f3a

Please sign in to comment.