From ba84bd3f1966092f7984c67029b23f8f771e25f8 Mon Sep 17 00:00:00 2001 From: Dmitry Savvinov Date: Tue, 3 Oct 2017 15:02:23 +0300 Subject: [PATCH] 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. --- .../description/ContractDescription.kt | 47 +++++++++++++ .../description/ContractDescriptionVisitor.kt | 49 +++++++++++++ .../kotlin/contracts/description/Effects.kt | 69 +++++++++++++++++++ .../description/LazyContractProvider.kt | 53 ++++++++++++++ .../expressions/LogicalCombinators.kt | 35 ++++++++++ .../description/expressions/Predicates.kt | 35 ++++++++++ .../description/expressions/Values.kt | 59 ++++++++++++++++ .../kotlin/config/LanguageVersionSettings.kt | 2 + 8 files changed, 349 insertions(+) create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/description/ContractDescription.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/description/ContractDescriptionVisitor.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/description/Effects.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/description/LazyContractProvider.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/LogicalCombinators.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/Predicates.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/Values.kt diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/ContractDescription.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/ContractDescription.kt new file mode 100644 index 00000000000..0a58abe132f --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/ContractDescription.kt @@ -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, val ownerFunction: FunctionDescriptor) + +interface ContractDescriptionElement { + fun accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R +} + +interface EffectDeclaration : ContractDescriptionElement { + override fun accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R = + contractDescriptionVisitor.visitEffectDeclaration(this, data) +} + +interface BooleanExpression : ContractDescriptionElement { + override fun accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R = + contractDescriptionVisitor.visitBooleanExpression(this, data) +} \ No newline at end of file diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/ContractDescriptionVisitor.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/ContractDescriptionVisitor.kt new file mode 100644 index 00000000000..0b1a0836696 --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/ContractDescriptionVisitor.kt @@ -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 { + 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) +} \ No newline at end of file diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/Effects.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/Effects.kt new file mode 100644 index 00000000000..c07b00cc04b --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/Effects.kt @@ -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 accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R = + contractDescriptionVisitor.visitConditionalEffectDeclaration(this, data) +} + + +/** + * Effect which specifies that subroutine returns some particular value + */ +class ReturnsEffectDeclaration(val value: ConstantReference) : EffectDeclaration { + override fun accept(contractDescriptionVisitor: ContractDescriptionVisitor, 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 accept(contractDescriptionVisitor: ContractDescriptionVisitor, 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 \ No newline at end of file diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/LazyContractProvider.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/LazyContractProvider.kt new file mode 100644 index 00000000000..4b733a53fa8 --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/LazyContractProvider.kt @@ -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 diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/LogicalCombinators.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/LogicalCombinators.kt new file mode 100644 index 00000000000..84da555c71d --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/LogicalCombinators.kt @@ -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 accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R = + contractDescriptionVisitor.visitLogicalOr(this, data) +} + +class LogicalAnd(val left: BooleanExpression, val right: BooleanExpression) : BooleanExpression { + override fun accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R = + contractDescriptionVisitor.visitLogicalAnd(this, data) +} + +class LogicalNot(val arg: BooleanExpression) : BooleanExpression { + override fun accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R = + contractDescriptionVisitor.visitLogicalNot(this, data) +} \ No newline at end of file diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/Predicates.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/Predicates.kt new file mode 100644 index 00000000000..988ee481b62 --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/Predicates.kt @@ -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 accept(contractDescriptionVisitor: ContractDescriptionVisitor, 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 accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R = + contractDescriptionVisitor.visitIsNullPredicate(this, data) + + fun negated(): IsNullPredicate = IsNullPredicate(arg, isNegated.not()) +} diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/Values.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/Values.kt new file mode 100644 index 00000000000..34b0315c3f3 --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/description/expressions/Values.kt @@ -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 accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R = + contractDescriptionVisitor.visitValue(this, data) +} + +open class ConstantReference(val name: String) : ContractDescriptionValue { + override fun accept(contractDescriptionVisitor: ContractDescriptionVisitor, 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 accept(contractDescriptionVisitor: ContractDescriptionVisitor, 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 accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D) = + contractDescriptionVisitor.visitVariableReference(this, data) +} + +class BooleanVariableReference(descriptor: ParameterDescriptor) : VariableReference(descriptor), BooleanExpression { + override fun accept(contractDescriptionVisitor: ContractDescriptionVisitor, data: D): R = + contractDescriptionVisitor.visitBooleanVariableReference(this, data) +} \ No newline at end of file diff --git a/compiler/util/src/org/jetbrains/kotlin/config/LanguageVersionSettings.kt b/compiler/util/src/org/jetbrains/kotlin/config/LanguageVersionSettings.kt index 998ab5708e3..3c451aebf76 100644 --- a/compiler/util/src/org/jetbrains/kotlin/config/LanguageVersionSettings.kt +++ b/compiler/util/src/org/jetbrains/kotlin/config/LanguageVersionSettings.kt @@ -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),