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),