Effects: support assert-like contracts

- Support functions that explicitly express relation between successfull
return and passed arguments (e.g., 'check')
- Note that we have to correct resulting data flow for arguments *after*
resoling (because we get contracts only after resolving). To do so, we
have to extend MutableDataFlowInfoForArguments interface with
'updateResultInfo' method.

==========
Introduction of EffectSystem: 11/18
This commit is contained in:
Dmitry Savvinov
2017-10-03 15:02:42 +03:00
parent 72b0d31329
commit 0dd6d1f4c7
4 changed files with 33 additions and 1 deletions
@@ -22,6 +22,7 @@ import org.jetbrains.kotlin.builtins.getValueParameterTypesFromFunctionType
import org.jetbrains.kotlin.builtins.isFunctionType import org.jetbrains.kotlin.builtins.isFunctionType
import org.jetbrains.kotlin.config.LanguageVersionSettings import org.jetbrains.kotlin.config.LanguageVersionSettings
import org.jetbrains.kotlin.descriptors.CallableDescriptor import org.jetbrains.kotlin.descriptors.CallableDescriptor
import org.jetbrains.kotlin.contracts.EffectSystem
import org.jetbrains.kotlin.psi.* import org.jetbrains.kotlin.psi.*
import org.jetbrains.kotlin.resolve.* import org.jetbrains.kotlin.resolve.*
import org.jetbrains.kotlin.resolve.BindingContext.CONSTRAINT_SYSTEM_COMPLETER import org.jetbrains.kotlin.resolve.BindingContext.CONSTRAINT_SYSTEM_COMPLETER
@@ -47,6 +48,7 @@ import org.jetbrains.kotlin.resolve.calls.results.OverloadResolutionResultsImpl
import org.jetbrains.kotlin.resolve.calls.results.ResolutionStatus import org.jetbrains.kotlin.resolve.calls.results.ResolutionStatus
import org.jetbrains.kotlin.resolve.calls.smartcasts.DataFlowInfo import org.jetbrains.kotlin.resolve.calls.smartcasts.DataFlowInfo
import org.jetbrains.kotlin.resolve.calls.tasks.TracingStrategy import org.jetbrains.kotlin.resolve.calls.tasks.TracingStrategy
import org.jetbrains.kotlin.resolve.scopes.receivers.TransientReceiver
import org.jetbrains.kotlin.types.ErrorUtils import org.jetbrains.kotlin.types.ErrorUtils
import org.jetbrains.kotlin.types.KotlinType import org.jetbrains.kotlin.types.KotlinType
import org.jetbrains.kotlin.types.TypeUtils import org.jetbrains.kotlin.types.TypeUtils
@@ -61,7 +63,8 @@ class CallCompleter(
private val callCheckers: Iterable<CallChecker>, private val callCheckers: Iterable<CallChecker>,
private val builtIns: KotlinBuiltIns, private val builtIns: KotlinBuiltIns,
private val languageVersionSettings: LanguageVersionSettings, private val languageVersionSettings: LanguageVersionSettings,
private val deprecationResolver: DeprecationResolver private val deprecationResolver: DeprecationResolver,
private val effectSystem: EffectSystem
) { ) {
fun <D : CallableDescriptor> completeCall( fun <D : CallableDescriptor> completeCall(
context: BasicCallResolutionContext, context: BasicCallResolutionContext,
@@ -131,6 +134,7 @@ class CallCompleter(
) { ) {
if (resolvedCall == null || resolvedCall.isCompleted || resolvedCall.constraintSystem == null) { if (resolvedCall == null || resolvedCall.isCompleted || resolvedCall.constraintSystem == null) {
completeArguments(context, results) completeArguments(context, results)
resolvedCall?.updateResultDataFlowInfoUsingEffects(context.trace)
resolvedCall?.markCallAsCompleted() resolvedCall?.markCallAsCompleted()
return return
} }
@@ -140,6 +144,7 @@ class CallCompleter(
completeArguments(context, results) completeArguments(context, results)
resolvedCall.updateResolutionStatusFromConstraintSystem(context, tracing) resolvedCall.updateResolutionStatusFromConstraintSystem(context, tracing)
resolvedCall.updateResultDataFlowInfoUsingEffects(context.trace)
resolvedCall.markCallAsCompleted() resolvedCall.markCallAsCompleted()
} }
@@ -393,4 +398,14 @@ class CallCompleter(
val expressionType = trace.getType(expression.receiverExpression) val expressionType = trace.getType(expression.receiverExpression)
return expressionType != null && TypeUtils.isNullableType(expressionType) return expressionType != null && TypeUtils.isNullableType(expressionType)
} }
private fun MutableResolvedCall<*>.updateResultDataFlowInfoUsingEffects(bindingTrace: BindingTrace) {
if (dataFlowInfoForArguments is MutableDataFlowInfoForArguments.WithoutArgumentsCheck) return
val moduleDescriptor = DescriptorUtils.getContainingModule(this.resultingDescriptor?.containingDeclaration ?: return)
val resultDFIfromES = effectSystem.getDataFlowInfoForFinishedCall(this, bindingTrace, moduleDescriptor)
dataFlowInfoForArguments.updateResultInfo(resultDFIfromES)
effectSystem.recordDefiniteInvocations(this, bindingTrace, moduleDescriptor)
}
} }
@@ -82,4 +82,12 @@ public class DataFlowInfoForArgumentsImpl extends MutableDataFlowInfoForArgument
if (resultInfo == null) return initialDataFlowInfo; if (resultInfo == null) return initialDataFlowInfo;
return initialDataFlowInfo.and(resultInfo); return initialDataFlowInfo.and(resultInfo);
} }
@Override
public void updateResultInfo(@NotNull DataFlowInfo dataFlowInfo) {
if (dataFlowInfo.equals(DataFlowInfo.Companion.getEMPTY())) return;
if (resultInfo == null) resultInfo = initialDataFlowInfo;
resultInfo = resultInfo.and(dataFlowInfo);
}
} }
@@ -29,6 +29,7 @@ public abstract class MutableDataFlowInfoForArguments implements DataFlowInfoFor
} }
public abstract void updateInfo(@NotNull ValueArgument valueArgument, @NotNull DataFlowInfo dataFlowInfo); public abstract void updateInfo(@NotNull ValueArgument valueArgument, @NotNull DataFlowInfo dataFlowInfo);
public abstract void updateResultInfo(@NotNull DataFlowInfo dataFlowInfo);
@NotNull @NotNull
@Override @Override
@@ -47,6 +48,11 @@ public abstract class MutableDataFlowInfoForArguments implements DataFlowInfoFor
throw new IllegalStateException(); throw new IllegalStateException();
} }
@Override
public void updateResultInfo(@NotNull DataFlowInfo dataFlowInfo) {
throw new IllegalStateException();
}
@NotNull @NotNull
@Override @Override
public DataFlowInfo getInfo(@NotNull ValueArgument valueArgument) { public DataFlowInfo getInfo(@NotNull ValueArgument valueArgument) {
@@ -206,6 +206,9 @@ public class ControlStructureTypingUtils {
dataFlowInfoForArgumentsMap.put(valueArgument, dataFlowInfo); dataFlowInfoForArgumentsMap.put(valueArgument, dataFlowInfo);
} }
@Override
public void updateResultInfo(@NotNull DataFlowInfo dataFlowInfo) { }
@NotNull @NotNull
@Override @Override
public DataFlowInfo getInfo(@NotNull ValueArgument valueArgument) { public DataFlowInfo getInfo(@NotNull ValueArgument valueArgument) {