Effects: Add declarations for description of contracts
Add ContractDescription structure which is used for declarative representation of function's contract. Also, add corresponding LanguageFeatures. ========== This is the first commit from a series of 18 commits which gradually introduce effect system into the compiler. All such commits will be marked with appropriate comment and index in that series. While each one of such commits separately shouldn't break compiler (i.e you can checkout any of them and expect compiler to build and pass tests successfully, e.g. for bissecting purposes), semantically they all are one big feature and not entirely independent. Please bear that in mind while working with/changing only some of them -- some strange effects can happen.
This commit is contained in:
Dmitry Savvinov
+47
@@ -0,0 +1,47 @@
|
||||
/*
|
||||
* Copyright 2010-2017 JetBrains s.r.o.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
package org.jetbrains.kotlin.contracts.description
|
||||
|
||||
import org.jetbrains.kotlin.descriptors.FunctionDescriptor
|
||||
|
||||
/**
|
||||
* This is actual model of contracts, i.e. what is expected to be parsed from
|
||||
* general protobuf format.
|
||||
*
|
||||
* Its intention is to provide declarative representation which is more stable
|
||||
* than inner representation of effect system, while enforcing type-checking which
|
||||
* isn't possible in protobuf representation.
|
||||
*
|
||||
* Any changes to this model should be done with previous versions in mind to keep
|
||||
* backward compatibility. Ideally, this model should only be extended, but not
|
||||
* changed.
|
||||
*/
|
||||
open class ContractDescription(val effects: List<EffectDeclaration>, val ownerFunction: FunctionDescriptor)
|
||||
|
||||
interface ContractDescriptionElement {
|
||||
fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R
|
||||
}
|
||||
|
||||
interface EffectDeclaration : ContractDescriptionElement {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitEffectDeclaration(this, data)
|
||||
}
|
||||
|
||||
interface BooleanExpression : ContractDescriptionElement {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitBooleanExpression(this, data)
|
||||
}
|
||||
+49
@@ -0,0 +1,49 @@
|
||||
/*
|
||||
* Copyright 2010-2017 JetBrains s.r.o.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
package org.jetbrains.kotlin.contracts.description
|
||||
|
||||
import org.jetbrains.kotlin.contracts.description.expressions.*
|
||||
|
||||
interface ContractDescriptionVisitor<out R, in D> {
|
||||
fun visitContractDescriptionElement(contractDescriptionElement: ContractDescriptionElement, data: D): R {
|
||||
throw IllegalStateException("Top of hierarchy reached, no overloads were found for element: $contractDescriptionElement")
|
||||
}
|
||||
|
||||
// Effects
|
||||
fun visitEffectDeclaration(effectDeclaration: EffectDeclaration, data: D): R = visitContractDescriptionElement(effectDeclaration, data)
|
||||
fun visitConditionalEffectDeclaration(conditionalEffect: ConditionalEffectDeclaration, data: D): R = visitEffectDeclaration(conditionalEffect, data)
|
||||
fun visitReturnsEffectDeclaration(returnsEffect: ReturnsEffectDeclaration, data: D): R = visitEffectDeclaration(returnsEffect, data)
|
||||
fun visitCallsEffectDeclaration(callsEffect: CallsEffectDeclaration, data: D): R = visitEffectDeclaration(callsEffect, data)
|
||||
|
||||
// Expressions
|
||||
fun visitBooleanExpression(booleanExpression: BooleanExpression, data: D): R = visitContractDescriptionElement(booleanExpression, data)
|
||||
|
||||
fun visitLogicalOr(logicalOr: LogicalOr, data: D): R = visitBooleanExpression(logicalOr, data)
|
||||
fun visitLogicalAnd(logicalAnd: LogicalAnd, data: D): R = visitBooleanExpression(logicalAnd, data)
|
||||
fun visitLogicalNot(logicalNot: LogicalNot, data: D): R = visitBooleanExpression(logicalNot, data)
|
||||
|
||||
fun visitIsInstancePredicate(isInstancePredicate: IsInstancePredicate, data: D): R = visitBooleanExpression(isInstancePredicate, data)
|
||||
fun visitIsNullPredicate(isNullPredicate: IsNullPredicate, data: D): R = visitBooleanExpression(isNullPredicate, data)
|
||||
|
||||
// Values
|
||||
fun visitValue(value: ContractDescriptionValue, data: D): R = visitContractDescriptionElement(value, data)
|
||||
|
||||
fun visitConstantDescriptor(constantReference: ConstantReference, data: D): R = visitValue(constantReference, data)
|
||||
fun visitBooleanConstantDescriptor(booleanConstantDescriptor: BooleanConstantReference, data: D): R = visitConstantDescriptor(booleanConstantDescriptor, data)
|
||||
fun visitVariableReference(variableReference: VariableReference, data: D): R = visitValue(variableReference, data)
|
||||
fun visitBooleanVariableReference(booleanVariableReference: BooleanVariableReference, data: D): R = visitVariableReference(booleanVariableReference, data)
|
||||
}
|
||||
@@ -0,0 +1,69 @@
|
||||
/*
|
||||
* Copyright 2010-2017 JetBrains s.r.o.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
package org.jetbrains.kotlin.contracts.description
|
||||
|
||||
import org.jetbrains.kotlin.contracts.description.expressions.ConstantReference
|
||||
import org.jetbrains.kotlin.contracts.description.expressions.VariableReference
|
||||
|
||||
/**
|
||||
* Effect with condition attached to it.
|
||||
*
|
||||
* [condition] is some expression, which result-type is Boolean, and clause should
|
||||
* be interpreted as: "if [effect] took place then [condition]-expression is
|
||||
* guaranteed to be true"
|
||||
*
|
||||
* NB. [effect] and [condition] connected with implication in math logic sense:
|
||||
* [effect] => [condition]. In particular this means that:
|
||||
* - there can be multiple ways how [effect] can be produced, but for any of them
|
||||
* [condition] holds.
|
||||
* - if [effect] wasn't observed, we *can't* reason that [condition] is false
|
||||
* - if [condition] is true, we *can't* reason that [effect] will be observed.
|
||||
*/
|
||||
class ConditionalEffectDeclaration(val effect: EffectDeclaration, val condition: BooleanExpression) : EffectDeclaration {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitConditionalEffectDeclaration(this, data)
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Effect which specifies that subroutine returns some particular value
|
||||
*/
|
||||
class ReturnsEffectDeclaration(val value: ConstantReference) : EffectDeclaration {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitReturnsEffectDeclaration(this, data)
|
||||
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Effect which specifies, that during execution of subroutine, callable [variableReference] will be invoked
|
||||
* [kind] amount of times, and will never be invoked after subroutine call is finished.
|
||||
*/
|
||||
class CallsEffectDeclaration(val variableReference: VariableReference, val kind: InvocationKind) : EffectDeclaration {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitCallsEffectDeclaration(this, data)
|
||||
}
|
||||
|
||||
enum class InvocationKind {
|
||||
AT_MOST_ONCE,
|
||||
EXACTLY_ONCE,
|
||||
AT_LEAST_ONCE,
|
||||
UNKNOWN
|
||||
}
|
||||
|
||||
fun InvocationKind.isDefinitelyVisited(): Boolean = this == InvocationKind.EXACTLY_ONCE || this == InvocationKind.AT_LEAST_ONCE
|
||||
fun InvocationKind.canBeRevisited(): Boolean = this == InvocationKind.UNKNOWN || this == InvocationKind.AT_LEAST_ONCE
|
||||
+53
@@ -0,0 +1,53 @@
|
||||
/*
|
||||
* Copyright 2010-2017 JetBrains s.r.o.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
package org.jetbrains.kotlin.contracts.description
|
||||
|
||||
import org.jetbrains.kotlin.descriptors.FunctionDescriptor
|
||||
|
||||
/**
|
||||
* Essentially, this is a composition of two fields: value of type 'ContractDescription' and
|
||||
* 'computation', which guarantees to initialize this field.
|
||||
*/
|
||||
class LazyContractProvider(private val computation: () -> Any?) {
|
||||
@Volatile
|
||||
private var isComputed: Boolean = false
|
||||
|
||||
private var contractDescription: ContractDescription? = null
|
||||
|
||||
|
||||
fun getContractDescription(): ContractDescription? {
|
||||
if (!isComputed) {
|
||||
computation.invoke() // should initialize contractDescription
|
||||
assert(isComputed) { "Computation of contract hasn't initialized contract properly" }
|
||||
}
|
||||
|
||||
return contractDescription
|
||||
}
|
||||
|
||||
fun setContractDescription(contractDescription: ContractDescription?) {
|
||||
this.contractDescription = contractDescription
|
||||
isComputed = true // publish
|
||||
}
|
||||
|
||||
companion object {
|
||||
fun createInitialized(contract: ContractDescription?): LazyContractProvider =
|
||||
LazyContractProvider({}).apply { setContractDescription(contract) }
|
||||
}
|
||||
}
|
||||
|
||||
// For storing into UserDataMap of FunctionDescriptor
|
||||
object ContractProviderKey : FunctionDescriptor.UserDataKey<LazyContractProvider?>
|
||||
+35
@@ -0,0 +1,35 @@
|
||||
/*
|
||||
* Copyright 2010-2017 JetBrains s.r.o.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
package org.jetbrains.kotlin.contracts.description.expressions
|
||||
|
||||
import org.jetbrains.kotlin.contracts.description.BooleanExpression
|
||||
import org.jetbrains.kotlin.contracts.description.ContractDescriptionVisitor
|
||||
|
||||
class LogicalOr(val left: BooleanExpression, val right: BooleanExpression) : BooleanExpression {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitLogicalOr(this, data)
|
||||
}
|
||||
|
||||
class LogicalAnd(val left: BooleanExpression, val right: BooleanExpression) : BooleanExpression {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitLogicalAnd(this, data)
|
||||
}
|
||||
|
||||
class LogicalNot(val arg: BooleanExpression) : BooleanExpression {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitLogicalNot(this, data)
|
||||
}
|
||||
+35
@@ -0,0 +1,35 @@
|
||||
/*
|
||||
* Copyright 2010-2017 JetBrains s.r.o.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
package org.jetbrains.kotlin.contracts.description.expressions
|
||||
|
||||
import org.jetbrains.kotlin.contracts.description.BooleanExpression
|
||||
import org.jetbrains.kotlin.contracts.description.ContractDescriptionVisitor
|
||||
import org.jetbrains.kotlin.types.KotlinType
|
||||
|
||||
class IsInstancePredicate(val arg: VariableReference, val type: KotlinType, val isNegated: Boolean) : BooleanExpression {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitIsInstancePredicate(this, data)
|
||||
|
||||
fun negated(): IsInstancePredicate = IsInstancePredicate(arg, type, isNegated.not())
|
||||
}
|
||||
|
||||
class IsNullPredicate(val arg: VariableReference, val isNegated: Boolean) : BooleanExpression {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitIsNullPredicate(this, data)
|
||||
|
||||
fun negated(): IsNullPredicate = IsNullPredicate(arg, isNegated.not())
|
||||
}
|
||||
+59
@@ -0,0 +1,59 @@
|
||||
/*
|
||||
* Copyright 2010-2017 JetBrains s.r.o.
|
||||
*
|
||||
* Licensed under the Apache License, Version 2.0 (the "License");
|
||||
* you may not use this file except in compliance with the License.
|
||||
* You may obtain a copy of the License at
|
||||
*
|
||||
* http://www.apache.org/licenses/LICENSE-2.0
|
||||
*
|
||||
* Unless required by applicable law or agreed to in writing, software
|
||||
* distributed under the License is distributed on an "AS IS" BASIS,
|
||||
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
* See the License for the specific language governing permissions and
|
||||
* limitations under the License.
|
||||
*/
|
||||
|
||||
package org.jetbrains.kotlin.contracts.description.expressions
|
||||
|
||||
import org.jetbrains.kotlin.contracts.description.BooleanExpression
|
||||
import org.jetbrains.kotlin.contracts.description.ContractDescriptionElement
|
||||
import org.jetbrains.kotlin.contracts.description.ContractDescriptionVisitor
|
||||
import org.jetbrains.kotlin.descriptors.ParameterDescriptor
|
||||
|
||||
|
||||
interface ContractDescriptionValue : ContractDescriptionElement {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitValue(this, data)
|
||||
}
|
||||
|
||||
open class ConstantReference(val name: String) : ContractDescriptionValue {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitConstantDescriptor(this, data)
|
||||
|
||||
companion object {
|
||||
val NULL = ConstantReference("NULL")
|
||||
val WILDCARD = ConstantReference("WILDCARD")
|
||||
val NOT_NULL = ConstantReference("NOT_NULL")
|
||||
}
|
||||
}
|
||||
|
||||
class BooleanConstantReference(name: String) : ConstantReference(name), BooleanExpression {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitBooleanConstantDescriptor(this, data)
|
||||
|
||||
companion object {
|
||||
val TRUE = BooleanConstantReference("TRUE")
|
||||
val FALSE = BooleanConstantReference("FALSE")
|
||||
}
|
||||
}
|
||||
|
||||
open class VariableReference(val descriptor: ParameterDescriptor) : ContractDescriptionValue {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D) =
|
||||
contractDescriptionVisitor.visitVariableReference(this, data)
|
||||
}
|
||||
|
||||
class BooleanVariableReference(descriptor: ParameterDescriptor) : VariableReference(descriptor), BooleanExpression {
|
||||
override fun <R, D> accept(contractDescriptionVisitor: ContractDescriptionVisitor<R, D>, data: D): R =
|
||||
contractDescriptionVisitor.visitBooleanVariableReference(this, data)
|
||||
}
|
||||
@@ -65,6 +65,8 @@ enum class LanguageFeature(
|
||||
JvmPackageName(KOTLIN_1_2),
|
||||
AssigningArraysToVarargsInNamedFormInAnnotations(KOTLIN_1_2),
|
||||
|
||||
ReturnsEffect(KOTLIN_1_3),
|
||||
CallsInPlaceEffect(KOTLIN_1_3),
|
||||
RestrictionOfValReassignmentViaBackingField(KOTLIN_1_3),
|
||||
NestedClassesInEnumEntryShouldBeInner(KOTLIN_1_3),
|
||||
ProhibitDataClassesOverridingCopy(KOTLIN_1_3),
|
||||
|
||||
Reference in New Issue
Block a user