From d2e582698e8ff8dd4a2ab563739618a12e69856c Mon Sep 17 00:00:00 2001 From: Dmitry Savvinov Date: Tue, 3 Oct 2017 15:02:27 +0300 Subject: [PATCH] Effects: add interpreters of ContractDescription Interpreters convert declarative representation of contracts (ContractDescription) in internal representation convenient for usage inside compiler (Computations, Effects, etc.) ========== Effect System introduction: 3/18 --- .../interpretation/ConditionInterpreter.kt | 58 +++++++++++++++ .../ConstantValuesInterpreter.kt | 33 +++++++++ .../ContractInterpretationDispatcher.kt | 71 +++++++++++++++++++ .../EffectDeclarationInterpreter.kt | 30 ++++++++ .../interpretation/EffectsInterpreters.kt | 54 ++++++++++++++ 5 files changed, 246 insertions(+) create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ConditionInterpreter.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ConstantValuesInterpreter.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ContractInterpretationDispatcher.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/EffectDeclarationInterpreter.kt create mode 100644 compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/EffectsInterpreters.kt diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ConditionInterpreter.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ConditionInterpreter.kt new file mode 100644 index 00000000000..693e35098b6 --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ConditionInterpreter.kt @@ -0,0 +1,58 @@ +/* + * 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.interpretation + +import org.jetbrains.kotlin.contracts.description.* +import org.jetbrains.kotlin.contracts.description.expressions.* +import org.jetbrains.kotlin.contracts.model.ESExpression +import org.jetbrains.kotlin.contracts.model.functors.IsFunctor +import org.jetbrains.kotlin.contracts.model.structure.* + +internal class ConditionInterpreter(private val dispatcher: ContractInterpretationDispatcher) : ContractDescriptionVisitor { + override fun visitLogicalOr(logicalOr: LogicalOr, data: Unit): ESExpression? { + val left = logicalOr.left.accept(this, data) ?: return null + val right = logicalOr.right.accept(this, data) ?: return null + return ESOr(left, right) + } + + override fun visitLogicalAnd(logicalAnd: LogicalAnd, data: Unit): ESExpression? { + val left = logicalAnd.left.accept(this, data) ?: return null + val right = logicalAnd.right.accept(this, data) ?: return null + return ESAnd(left, right) + } + + override fun visitLogicalNot(logicalNot: LogicalNot, data: Unit): ESExpression? { + val arg = logicalNot.arg.accept(this, data) ?: return null + return ESNot(arg) + } + + override fun visitIsInstancePredicate(isInstancePredicate: IsInstancePredicate, data: Unit): ESExpression? { + val esVariable = dispatcher.interpretVariable(isInstancePredicate.arg) ?: return null + return ESIs(esVariable, IsFunctor(isInstancePredicate.type, isInstancePredicate.isNegated)) + } + + override fun visitIsNullPredicate(isNullPredicate: IsNullPredicate, data: Unit): ESExpression? { + val variable = dispatcher.interpretVariable(isNullPredicate.arg) ?: return null + return ESEqual(variable, ESConstant.NULL, isNullPredicate.isNegated) + } + + override fun visitBooleanConstantDescriptor(booleanConstantDescriptor: BooleanConstantReference, data: Unit): ESExpression? = + dispatcher.interpretConstant(booleanConstantDescriptor) + + override fun visitBooleanVariableReference(booleanVariableReference: BooleanVariableReference, data: Unit): ESExpression? = + dispatcher.interpretVariable(booleanVariableReference) +} \ No newline at end of file diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ConstantValuesInterpreter.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ConstantValuesInterpreter.kt new file mode 100644 index 00000000000..d9b3cad1af3 --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ConstantValuesInterpreter.kt @@ -0,0 +1,33 @@ +/* + * 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.interpretation + +import org.jetbrains.kotlin.contracts.description.expressions.BooleanConstantReference +import org.jetbrains.kotlin.contracts.description.expressions.ConstantReference +import org.jetbrains.kotlin.contracts.model.structure.ESConstant +import org.jetbrains.kotlin.contracts.model.structure.lift + +internal class ConstantValuesInterpreter { + fun interpretConstant(constantReference: ConstantReference): ESConstant? = when (constantReference) { + BooleanConstantReference.TRUE -> true.lift() + BooleanConstantReference.FALSE -> false.lift() + ConstantReference.NULL-> ESConstant.NULL + ConstantReference.NOT_NULL -> ESConstant.NOT_NULL + ConstantReference.WILDCARD -> ESConstant.WILDCARD + else -> null + } +} \ No newline at end of file diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ContractInterpretationDispatcher.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ContractInterpretationDispatcher.kt new file mode 100644 index 00000000000..128f457b247 --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/ContractInterpretationDispatcher.kt @@ -0,0 +1,71 @@ +/* + * 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.interpretation + +import org.jetbrains.kotlin.contracts.description.* +import org.jetbrains.kotlin.contracts.description.expressions.ConstantReference +import org.jetbrains.kotlin.contracts.description.expressions.VariableReference +import org.jetbrains.kotlin.contracts.model.functors.SubstitutingFunctor +import org.jetbrains.kotlin.contracts.model.structure.ESConstant +import org.jetbrains.kotlin.contracts.model.structure.ESVariable +import org.jetbrains.kotlin.contracts.model.ESEffect +import org.jetbrains.kotlin.contracts.model.ESExpression +import org.jetbrains.kotlin.contracts.model.Functor +import org.jetbrains.kotlin.descriptors.FunctionDescriptor + +/** + * This class manages conversion of [ContractDescription] to [Functor] + */ +class ContractInterpretationDispatcher { + private val constantsInterpreter = ConstantValuesInterpreter() + private val conditionInterpreter = ConditionInterpreter(this) + private val conditionalEffectInterpreter = ConditionalEffectInterpreter(this) + private val effectsInterpreters: List = listOf( + ReturnsEffectInterpreter(this), + CallsEffectInterpreter(this) + ) + fun resolveFunctor(functionDescriptor: FunctionDescriptor): Functor? { + val contractDescriptor = functionDescriptor.getUserData(ContractProviderKey)?.getContractDescription() ?: return null + return convertContractDescriptorToFunctor(contractDescriptor) + } + + private fun convertContractDescriptorToFunctor(contractDescription: ContractDescription): Functor? { + val resultingClauses = contractDescription.effects.map { effect -> + if (effect is ConditionalEffectDeclaration) { + conditionalEffectInterpreter.interpret(effect) ?: return null + } + else { + effectsInterpreters.mapNotNull { it.tryInterpret(effect) }.singleOrNull() ?: return null + } + } + + return SubstitutingFunctor(resultingClauses, contractDescription.ownerFunction) + } + + internal fun interpretEffect(effectDeclaration: EffectDeclaration): ESEffect? { + val convertedFunctors = effectsInterpreters.mapNotNull { it.tryInterpret(effectDeclaration) } + return convertedFunctors.singleOrNull() + } + + internal fun interpretConstant(constantReference: ConstantReference): ESConstant? = + constantsInterpreter.interpretConstant(constantReference) + + internal fun interpretCondition(booleanExpression: BooleanExpression): ESExpression? = + booleanExpression.accept(conditionInterpreter, Unit) + + internal fun interpretVariable(variableReference: VariableReference): ESVariable? = ESVariable(variableReference.descriptor) +} \ No newline at end of file diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/EffectDeclarationInterpreter.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/EffectDeclarationInterpreter.kt new file mode 100644 index 00000000000..d3c15205af6 --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/EffectDeclarationInterpreter.kt @@ -0,0 +1,30 @@ +/* + * 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.interpretation + +import org.jetbrains.kotlin.contracts.description.EffectDeclaration +import org.jetbrains.kotlin.contracts.model.ESEffect + +/** + * Interpreter of some effects. For most cases, each particular + * EffectDeclaration, EffectDeclarationInterpreter and ESEffect + * should be in 1-1-1 correspondence to each other and be agnostic + * about other implementations. + */ +internal interface EffectDeclarationInterpreter { + fun tryInterpret(effectDeclaration: EffectDeclaration): ESEffect? +} \ No newline at end of file diff --git a/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/EffectsInterpreters.kt b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/EffectsInterpreters.kt new file mode 100644 index 00000000000..6311c1ad340 --- /dev/null +++ b/compiler/resolution/src/org/jetbrains/kotlin/contracts/interpretation/EffectsInterpreters.kt @@ -0,0 +1,54 @@ +/* + * 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.interpretation + +import org.jetbrains.kotlin.contracts.description.CallsEffectDeclaration +import org.jetbrains.kotlin.contracts.description.ConditionalEffectDeclaration +import org.jetbrains.kotlin.contracts.description.EffectDeclaration +import org.jetbrains.kotlin.contracts.description.ReturnsEffectDeclaration +import org.jetbrains.kotlin.contracts.model.ConditionalEffect +import org.jetbrains.kotlin.contracts.model.ESEffect +import org.jetbrains.kotlin.contracts.model.SimpleEffect +import org.jetbrains.kotlin.contracts.model.structure.ESCalls +import org.jetbrains.kotlin.contracts.model.structure.ESReturns + +internal class CallsEffectInterpreter(private val dispatcher: ContractInterpretationDispatcher) : EffectDeclarationInterpreter { + override fun tryInterpret(effectDeclaration: EffectDeclaration): ESEffect? { + if (effectDeclaration !is CallsEffectDeclaration) return null + + val variable = dispatcher.interpretVariable(effectDeclaration.variableReference) ?: return null + val kind = effectDeclaration.kind + return ESCalls(variable, kind) + } +} + +internal class ConditionalEffectInterpreter(private val dispatcher: ContractInterpretationDispatcher) { + fun interpret(conditionalEffectDeclaration: ConditionalEffectDeclaration): ConditionalEffect? { + val effect = dispatcher.interpretEffect(conditionalEffectDeclaration.effect) as? SimpleEffect ?: return null + val condition = dispatcher.interpretCondition(conditionalEffectDeclaration.condition) ?: return null + + return ConditionalEffect(condition, effect) + } +} + +internal class ReturnsEffectInterpreter(private val dispatcher: ContractInterpretationDispatcher) : EffectDeclarationInterpreter { + override fun tryInterpret(effectDeclaration: EffectDeclaration): ESEffect? { + if (effectDeclaration !is ReturnsEffectDeclaration) return null + val returnedValue = dispatcher.interpretConstant(effectDeclaration.value) ?: return null + return ESReturns(returnedValue) + } +} \ No newline at end of file