Effects: Add inner representation of contracts

Add model of contracts used by compiler during analysis. It should be thought of as structure which used by the compiler to implement semantics, expressed by the ContractDescription. ========== Effect System introduction: 2/18
2017-10-03 15:02:26 +03:00
parent ba84bd3f19
commit afc15e9211
23 changed files with 1401 additions and 0 deletions
@@ -0,0 +1,39 @@
+/*
+ * 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.model
+
+import org.jetbrains.kotlin.types.KotlinType
+
+/**
+ * Generic abstraction of static information about some part of program.
+ */
+interface Computation {
+    /**
+     * Return-type of corresponding part of program.
+     * If type is unknown or computation doesn't have a type (e.g. if
+     * it is some construction, like "for"-loop), then type is 'null'
+     */
+    val type: KotlinType?
+
+    /**
+     * List of all possible effects of this computation.
+     * Note that it's not guaranteed to be complete, i.e. if list
+     * doesn't mention some effect, then it should be interpreted
+     * as the absence of information about that effect.
+     */
+    val effects: List<ESEffect>
+}
@@ -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.model
+
+sealed class ESEffect {
+    /**
+     * Returns:
+     *  - true, when presence of `this`-effect necessary implies presence of `other`-effect
+     *  - false, when presence of `this`-effect necessary implies absence of `other`-effect
+     *  - null, when presence of `this`-effect doesn't implies neither presence nor absence of `other`-effect
+     */
+    abstract fun isImplies(other: ESEffect): Boolean?
+}
+
+/**
+ * Abstraction of some side-effect of a computation.
+ *
+ * SimpleEffect alone means that this effect will definitely be fired.
+ */
+abstract class SimpleEffect : ESEffect()
+
+/**
+ * Effect with condition attached to it.
+ *
+ * Has the same semantics as [org.jetbrains.kotlin.contracts.description.ConditionalEffectDeclaration]
+ */
+class ConditionalEffect(val condition: ESExpression, val simpleEffect: SimpleEffect) : ESEffect() {
+    // Conservatively, always return null, indicating absence of information
+    override fun isImplies(other: ESEffect): Boolean? = null
+}
+
+
+
@@ -0,0 +1,31 @@
+/*
+ * 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.model
+
+import org.jetbrains.kotlin.contracts.model.structure.*
+
+
+interface ESExpressionVisitor<out T> {
+    fun visitIs(isOperator: ESIs): T
+    fun visitEqual(equal: ESEqual): T
+    fun visitAnd(and: ESAnd): T
+    fun visitNot(not: ESNot): T
+    fun visitOr(or: ESOr): T
+
+    fun visitVariable(esVariable: ESVariable): T
+    fun visitConstant(esConstant: ESConstant): T
+}
@@ -0,0 +1,31 @@
+/*
+ * 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.model
+
+import org.jetbrains.kotlin.types.KotlinType
+
+interface ESExpression {
+    fun <T> accept(visitor: ESExpressionVisitor<T>): T
+}
+
+interface ESOperator : ESExpression {
+    val functor: Functor
+}
+
+abstract class ESValue(override val type: KotlinType?) : Computation, ESExpression {
+    override val effects: List<ESEffect> = listOf()
+}
@@ -0,0 +1,29 @@
+/*
+ * 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.model
+
+/**
+ * An abstraction of effect-generating nature of some computation.
+ *
+ * One can think of Functor as of adjoint to function declaration, responsible
+ * for generating effects. It's [invokeWithArguments] method roughly corresponds
+ * to call of corresponding function, but instead of taking values and returning
+ * values, it takes effects and returns effects.
+ */
+interface Functor {
+    fun invokeWithArguments(arguments: List<Computation>): List<ESEffect>
+}
@@ -0,0 +1,137 @@
+/*
+ * 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.model
+
+import org.jetbrains.kotlin.types.KotlinType
+
+/**
+ * Collection of information about context.
+ *
+ * This class is pretty close semantically to DataFlowInfo, but
+ * supports broader variety of information (like, not just information
+ * about subtypes of a variable, but also about types that are definitely
+ * not subtypes of a variable).
+ *
+ * Also, it's abstracted away from PSI
+ */
+class MutableContextInfo private constructor(
+        val firedEffects: MutableList<ESEffect>,
+        val subtypes: MutableMap<ESValue, MutableSet<KotlinType>>,
+        val notSubtypes: MutableMap<ESValue, MutableSet<KotlinType>>,
+        val equalValues: MutableMap<ESValue, MutableSet<ESValue>>,
+        val notEqualValues: MutableMap<ESValue, MutableSet<ESValue>>
+) {
+    companion object {
+        val EMPTY: MutableContextInfo
+            get() = MutableContextInfo(
+                    firedEffects = mutableListOf(),
+                    subtypes = mutableMapOf(),
+                    notSubtypes = mutableMapOf(),
+                    equalValues = mutableMapOf(),
+                    notEqualValues = mutableMapOf()
+            )
+    }
+
+    fun subtype(value: ESValue, type: KotlinType) = apply { subtypes.initAndAdd(value, type) }
+
+    fun notSubtype(value: ESValue, type: KotlinType) = apply { notSubtypes.initAndAdd(value, type) }
+
+    fun equal(left: ESValue, right: ESValue) = apply {
+        equalValues.initAndAdd(left, right)
+        equalValues.initAndAdd(right, left)
+    }
+
+    fun notEqual(left: ESValue, right: ESValue) = apply {
+        notEqualValues.initAndAdd(left, right)
+        notEqualValues.initAndAdd(right, left)
+    }
+
+    fun fire(effect: ESEffect) = apply { firedEffects += effect }
+
+    fun or(other: MutableContextInfo): MutableContextInfo = MutableContextInfo(
+            firedEffects = firedEffects.intersect(other.firedEffects).toMutableList(),
+            subtypes = subtypes.intersect(other.subtypes),
+            notSubtypes = notSubtypes.intersect(other.notSubtypes),
+            equalValues = equalValues.intersect(other.equalValues),
+            notEqualValues = notEqualValues.intersect(other.notEqualValues)
+    )
+
+    fun and(other: MutableContextInfo): MutableContextInfo = MutableContextInfo(
+            firedEffects = firedEffects.union(other.firedEffects).toMutableList(),
+            subtypes = subtypes.union(other.subtypes),
+            notSubtypes = notSubtypes.union(other.notSubtypes),
+            equalValues = equalValues.union(other.equalValues),
+            notEqualValues = notEqualValues.union(other.notEqualValues)
+    )
+
+    private fun <D> MutableMap<ESValue, MutableSet<D>>.intersect(that: MutableMap<ESValue, MutableSet<D>>): MutableMap<ESValue, MutableSet<D>> {
+        val result = mutableMapOf<ESValue, MutableSet<D>>()
+
+        val allKeys = this.keys.intersect(that.keys)
+        allKeys.forEach {
+            val newValues = this[it]!!.intersect(that[it]!!)
+            if (newValues.isNotEmpty()) result[it] = newValues.toMutableSet()
+        }
+        return result
+    }
+
+    private fun <D> Map<ESValue, MutableSet<D>>.union(that: Map<ESValue, MutableSet<D>>): MutableMap<ESValue, MutableSet<D>> {
+        val result = mutableMapOf<ESValue, MutableSet<D>>()
+        result.putAll(this)
+        that.entries.forEach { (thatKey, thatValue) ->
+            val oldValue = result[thatKey] ?: mutableSetOf()
+            oldValue.addAll(thatValue)
+            result[thatKey] = oldValue
+        }
+        return result
+    }
+
+    private fun <D> MutableMap<ESValue, MutableSet<D>>.initAndAdd(key: ESValue, value: D) {
+        this.compute(key) { _, maybeValues ->
+            val setOfValues = maybeValues ?: mutableSetOf()
+            setOfValues.add(value)
+            setOfValues
+        }
+    }
+
+    fun print(): String = buildString {
+        val info = this@MutableContextInfo
+
+        fun <D> Map<ESValue, Set<D>>.printMapEntriesWithSeparator(separator: String) {
+            this.entries.filter { it.value.isNotEmpty() }.forEach { (key, value) ->
+                append(key.toString())
+                append(" $separator ")
+                appendln(value.toString())
+            }
+        }
+
+        append("Fired effects: ")
+        append(info.firedEffects.joinToString(separator = ", " ))
+        appendln("")
+
+        subtypes.printMapEntriesWithSeparator("is")
+
+        notSubtypes.printMapEntriesWithSeparator("!is")
+
+        equalValues.printMapEntriesWithSeparator("==")
+
+        notEqualValues.printMapEntriesWithSeparator("!=")
+
+        this.toString()
+    }
+
+}
@@ -0,0 +1,60 @@
+/*
+ * 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.model.functors
+
+import org.jetbrains.kotlin.contracts.model.structure.ESReturns
+import org.jetbrains.kotlin.contracts.model.structure.ESConstant
+import org.jetbrains.kotlin.contracts.model.ConditionalEffect
+import org.jetbrains.kotlin.contracts.model.ESEffect
+import org.jetbrains.kotlin.contracts.model.Computation
+
+abstract class AbstractBinaryFunctor : AbstractReducingFunctor() {
+    override fun doInvocation(arguments: List<Computation>): List<ESEffect> {
+        assert(arguments.size == 2, { "Wrong size of arguments list for Binary functor: expected 2, got ${arguments.size}" })
+        return invokeWithArguments(arguments[0], arguments[1])
+    }
+
+    fun invokeWithArguments(left: Computation, right: Computation): List<ESEffect> {
+        if (left is ESConstant) return invokeWithConstant(right, left)
+        if (right is ESConstant) return invokeWithConstant(left, right)
+
+        val nonInterestingEffects = mutableListOf<ESEffect>()
+        val leftValueReturning = mutableListOf<ConditionalEffect>()
+        val rightValueReturning = mutableListOf<ConditionalEffect>()
+
+        left.effects.forEach {
+            if (it !is ConditionalEffect || it.simpleEffect !is ESReturns || it.simpleEffect.value == ESConstant.WILDCARD)
+                nonInterestingEffects += it
+            else
+                leftValueReturning += it
+        }
+
+        right.effects.forEach {
+            if (it !is ConditionalEffect || it.simpleEffect !is ESReturns || it.simpleEffect.value == ESConstant.WILDCARD)
+                nonInterestingEffects += it
+            else
+                rightValueReturning += it
+        }
+
+        val evaluatedByFunctor = invokeWithReturningEffects(leftValueReturning, rightValueReturning)
+
+        return nonInterestingEffects + evaluatedByFunctor
+    }
+
+    protected abstract fun invokeWithConstant(computation: Computation, constant: ESConstant): List<ESEffect>
+    protected abstract fun invokeWithReturningEffects(left: List<ConditionalEffect>, right: List<ConditionalEffect>): List<ConditionalEffect>
+}
@@ -0,0 +1,34 @@
+/*
+ * 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.model.functors
+
+import org.jetbrains.kotlin.contracts.model.ESEffect
+import org.jetbrains.kotlin.contracts.model.Functor
+import org.jetbrains.kotlin.contracts.model.Computation
+import org.jetbrains.kotlin.contracts.model.visitors.Reducer
+
+/**
+ * Abstract implementation of Functor with some routine house-holding
+ * automatically performed. *
+ */
+abstract class AbstractReducingFunctor : Functor {
+    private val reducer = Reducer()
+
+    override fun invokeWithArguments(arguments: List<Computation>): List<ESEffect> = reducer.reduceEffects(doInvocation(arguments))
+
+    abstract protected fun doInvocation(arguments: List<Computation>): List<ESEffect>
+}
@@ -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.model.functors
+
+import org.jetbrains.kotlin.contracts.model.structure.ESReturns
+import org.jetbrains.kotlin.contracts.model.structure.ESConstant
+import org.jetbrains.kotlin.contracts.model.ConditionalEffect
+import org.jetbrains.kotlin.contracts.model.ESEffect
+import org.jetbrains.kotlin.contracts.model.Computation
+
+
+/**
+ * Unary functor that has sequential semantics, i.e. it won't apply to
+ * computations that can't be guaranteed to be finished.
+ *
+ * It provides [applyToFinishingClauses] method for successors, which is guaranteed to
+ * be called only on clauses that haven't failed before reaching functor transformation.
+ */
+abstract class AbstractUnaryFunctor : AbstractReducingFunctor() {
+    override fun doInvocation(arguments: List<Computation>): List<ESEffect> {
+        assert(arguments.size == 1, { "Wrong size of arguments list for Unary operator: expected 1, got ${arguments.size}" })
+        return invokeWithArguments(arguments[0])
+    }
+
+    fun invokeWithArguments(arg: Computation): List<ESEffect> {
+        val returning = mutableListOf<ConditionalEffect>()
+        val rest = mutableListOf<ESEffect>()
+
+        arg.effects.forEach { if (it !is ConditionalEffect || it.simpleEffect !is ESReturns || it.simpleEffect.value == ESConstant.WILDCARD) rest += it else returning += it }
+
+        val evaluatedByFunctor = invokeWithReturningEffects(returning)
+
+        return rest + evaluatedByFunctor
+    }
+
+    protected abstract fun invokeWithReturningEffects(list: List<ConditionalEffect>): List<ConditionalEffect>
+}
+
+
@@ -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.model.functors
+
+import org.jetbrains.kotlin.contracts.model.structure.ESReturns
+import org.jetbrains.kotlin.contracts.model.structure.ESAnd
+import org.jetbrains.kotlin.contracts.model.structure.ESConstant
+import org.jetbrains.kotlin.contracts.model.structure.ESOr
+import org.jetbrains.kotlin.contracts.model.structure.lift
+import org.jetbrains.kotlin.contracts.model.ConditionalEffect
+import org.jetbrains.kotlin.contracts.model.ESEffect
+import org.jetbrains.kotlin.contracts.model.Computation
+
+class AndFunctor : AbstractBinaryFunctor() {
+    override fun invokeWithConstant(computation: Computation, constant: ESConstant): List<ESEffect> = when (constant) {
+        ESConstant.TRUE -> computation.effects
+        ESConstant.FALSE -> emptyList()
+
+        // This means that expression isn't typechecked properly
+        else -> computation.effects
+    }
+
+    override fun invokeWithReturningEffects(left: List<ConditionalEffect>, right: List<ConditionalEffect>): List<ConditionalEffect> {
+        /* Normally, `left` and `right` contain clauses that end with Returns(false/true), but if
+         expression wasn't properly typechecked, we could get some senseless clauses here, e.g.
+         with Returns(1) (note that they still *return* as guaranteed by AbstractSequentialBinaryFunctor).
+         We will just ignore such clauses in order to make smartcasting robust while typing */
+
+        val (leftTrue, leftFalse) = left.strictPartition(ESReturns(true.lift()), ESReturns(false.lift()))
+        val (rightTrue, rightFalse) = right.strictPartition(ESReturns(true.lift()), ESReturns(false.lift()))
+
+        val whenLeftReturnsTrue = foldConditionsWithOr(leftTrue)
+        val whenRightReturnsTrue = foldConditionsWithOr(rightTrue)
+        val whenLeftReturnsFalse = foldConditionsWithOr(leftFalse)
+        val whenRightReturnsFalse = foldConditionsWithOr(rightFalse)
+
+        // Even if one of 'Returns(true)' is missing, we still can argue that other condition
+        // *must* be true when whole functor returns true
+        val conditionWhenTrue = applyWithDefault(whenLeftReturnsTrue, whenRightReturnsTrue, { l, r -> ESAnd(l, r) })
+
+        // When whole And-functor returns false, we can only argue that one of arguments was false, and to do so we
+        // have to know *both* 'Returns(false)'-conditions
+        val conditionWhenFalse = applyIfBothNotNull(whenLeftReturnsFalse, whenRightReturnsFalse, { l, r -> ESOr(l, r) })
+
+        val result = mutableListOf<ConditionalEffect>()
+
+        if (conditionWhenTrue != null) {
+            result.add(ConditionalEffect(conditionWhenTrue, ESReturns(true.lift())))
+        }
+
+        if (conditionWhenFalse != null) {
+            result.add(ConditionalEffect(conditionWhenFalse, ESReturns(false.lift())))
+        }
+
+        return result
+    }
+}
@@ -0,0 +1,114 @@
+/*
+ * 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.model.functors
+
+import org.jetbrains.kotlin.builtins.DefaultBuiltIns
+import org.jetbrains.kotlin.builtins.KotlinBuiltIns
+import org.jetbrains.kotlin.contracts.model.structure.ESReturns
+import org.jetbrains.kotlin.contracts.model.structure.ESConstant
+import org.jetbrains.kotlin.contracts.model.structure.ESEqual
+import org.jetbrains.kotlin.contracts.model.ESValue
+import org.jetbrains.kotlin.contracts.model.structure.lift
+import org.jetbrains.kotlin.contracts.model.*
+import org.jetbrains.kotlin.contracts.model.Computation
+
+class EqualsFunctor(val isNegated: Boolean) : AbstractReducingFunctor() {
+    /*
+        Equals is a bit tricky case to produce clauses, because e.g. if we want to emit "Returns(true)"-clause,
+        then we have to guarantee that we know *all* cases when 'true' could've been returned, and join
+        them with OR properly.
+        To understand this, consider following example:
+
+            foo(x) == bar(x)
+            Effects of foo(x): "Returns(true) -> x is String"
+            Effects of bar(x): "Returns(true) -> x is Int"
+
+        Of course, we can't say that the whole expression has effect "Returns(true) -> x is String && x is Int"
+        because it could've returned in 'true' also when 'foo(x) == false' and 'bar(x) == false', and we don't
+        know anything about such cases.
+
+        We don't want to code here fair analysis for general cases, because it's too complex. Instead, we just
+        check some specific cases, which are useful enough in practice
+     */
+    override fun doInvocation(arguments: List<Computation>): List<ESEffect> {
+        assert(arguments.size == 2) { "Equals functor expected 2 arguments, got ${arguments.size}" }
+
+        // TODO: AnnotationConstructorCaller kills this with implicit receiver. Investigate, how.
+        if (arguments.size != 2) return emptyList()
+        return invokeWithArguments(arguments[0], arguments[1])
+    }
+
+    fun invokeWithArguments(left: Computation, right: Computation): List<ESEffect> {
+        // First, check if both arguments are values: then we can produce both 'true' and 'false' clauses
+        if (left is ESValue && right is ESValue) {
+            return equateValues(left, right)
+        }
+
+        // Second, check is at least one of argument is Constant: then we can produce 'true'-clause and maybe even 'false'
+        if (left is ESConstant) {
+            return equateCallAndConstant(right, left)
+        }
+        if (right is ESConstant) {
+            return equateCallAndConstant(left, right)
+        }
+
+        // Otherwise, don't even try to produce something. We can improve this in future, if we would like to
+        return emptyList()
+    }
+
+    private fun equateCallAndConstant(call: Computation, constant: ESConstant): List<ESEffect> {
+        val resultingClauses = mutableListOf<ESEffect>()
+
+        for (effect in call.effects) {
+            if (effect !is ConditionalEffect || effect.simpleEffect !is ESReturns || effect.simpleEffect.value == ESConstant.WILDCARD) {
+                resultingClauses += effect
+                continue
+            }
+
+            if (effect.simpleEffect.value == constant) {
+                val trueClause = ConditionalEffect(effect.condition, ESReturns(isNegated.not().lift()))
+                resultingClauses.add(trueClause)
+            }
+
+            if (effect.simpleEffect.value != constant && effect.simpleEffect.value is ESConstant && isSafeToProduceFalse(call, effect.simpleEffect.value, constant)) {
+                val falseClause = ConditionalEffect(effect.condition, ESReturns(isNegated.lift()))
+                resultingClauses.add(falseClause)
+            }
+        }
+
+        return resultingClauses
+    }
+
+    // It is safe to produce false if we're comparing types which are isomorphic to Boolean. For such types we can be sure, that
+    // if leftConstant != rightConstant, then this is the only way to produce 'false'.
+    private fun isSafeToProduceFalse(leftCall: Computation, leftConstant: ESConstant, rightConstant: ESConstant): Boolean = when {
+        // Comparison of Boolean
+        KotlinBuiltIns.isBoolean(rightConstant.type) && leftCall.type != null && KotlinBuiltIns.isBoolean(leftCall.type!!) -> true
+
+        // Comparison of NULL/NOT_NULL, which is essentially Boolean
+        leftConstant.isNullConstant() && rightConstant.isNullConstant() -> true
+
+        else -> false
+    }
+
+    private fun equateValues(left: ESValue, right: ESValue): List<ESEffect> {
+        return listOf(
+                ConditionalEffect(ESEqual(left, right, isNegated), ESReturns(true.lift())),
+                ConditionalEffect(ESEqual(left, right, isNegated.not()), ESReturns(false.lift()))
+        )
+    }
+}
@@ -0,0 +1,61 @@
+/*
+ * 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.model.functors
+
+import org.jetbrains.kotlin.contracts.model.structure.ESOr
+import org.jetbrains.kotlin.contracts.model.ConditionalEffect
+import org.jetbrains.kotlin.contracts.model.ESEffect
+import org.jetbrains.kotlin.contracts.model.ESExpression
+
+/**
+ * Applies [operation] to [first] and [second] if both not-null, otherwise returns null
+ */
+internal fun <F, S, R> applyIfBothNotNull(first: F?, second: S?, operation: (F, S) -> R): R? =
+        if (first == null || second == null) null else operation(first, second)
+
+/**
+ * If both [first] and [second] are null, then return null
+ * If only one of [first] and [second] is null, then return other one
+ * Otherwise, return result of [operation]
+ */
+internal fun <F : R, S : R, R> applyWithDefault(first: F?, second: S?, operation: (F, S) -> R): R? = when {
+    first == null && second == null -> null
+    first == null -> second
+    second == null -> first
+    else -> operation(first, second)
+}
+
+internal fun foldConditionsWithOr(list: List<ConditionalEffect>): ESExpression? =
+        if (list.isEmpty())
+            null
+        else
+            list.map { it.condition }.reduce { acc, condition -> ESOr(acc, condition) }
+
+/**
+ * Places all clauses that equal to `firstModel` into first list, and all clauses that equal to `secondModel` into second list
+ */
+internal fun List<ConditionalEffect>.strictPartition(firstModel: ESEffect, secondModel: ESEffect): Pair<List<ConditionalEffect>, List<ConditionalEffect>> {
+    val first = mutableListOf<ConditionalEffect>()
+    val second = mutableListOf<ConditionalEffect>()
+
+    forEach {
+        if (it.simpleEffect == firstModel) first += it
+        if (it.simpleEffect == secondModel) second += it
+    }
+
+    return first to second
+}
@@ -0,0 +1,50 @@
+/*
+ * 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.model.functors
+
+import org.jetbrains.kotlin.contracts.model.structure.ESReturns
+import org.jetbrains.kotlin.contracts.model.*
+import org.jetbrains.kotlin.contracts.model.structure.*
+import org.jetbrains.kotlin.types.KotlinType
+
+class IsFunctor(val type: KotlinType, val isNegated: Boolean) : AbstractReducingFunctor() {
+    override fun doInvocation(arguments: List<Computation>): List<ESEffect> {
+        assert(arguments.size == 1, { "Wrong size of arguments list for Unary operator: expected 1, got ${arguments.size}" })
+        return invokeWithArguments(arguments[0])
+    }
+
+    fun invokeWithArguments(arg: Computation): List<ESEffect> {
+        return if (arg is ESValue)
+            invokeWithValue(arg, null)
+        else
+            arg.effects.flatMap {
+                if (it !is ConditionalEffect || it.simpleEffect !is ESReturns || it.simpleEffect.value == ESConstant.WILDCARD)
+                    listOf(it)
+                else
+                    invokeWithValue(it.simpleEffect.value, it.condition)
+            }
+    }
+
+    private fun invokeWithValue(value: ESValue, additionalCondition: ESExpression?): List<ConditionalEffect> {
+        val trueIs = ESIs(value, this)
+        val falseIs = ESIs(value, IsFunctor(type, isNegated.not()))
+
+        val trueResult = ConditionalEffect(trueIs.and(additionalCondition), ESReturns(true.lift()))
+        val falseResult = ConditionalEffect(falseIs.and(additionalCondition), ESReturns(false.lift()))
+        return listOf(trueResult, falseResult)
+    }
+}
@@ -0,0 +1,37 @@
+/*
+ * 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.model.functors
+
+import org.jetbrains.kotlin.contracts.model.structure.ESReturns
+import org.jetbrains.kotlin.contracts.model.structure.ESConstant
+import org.jetbrains.kotlin.contracts.model.ConditionalEffect
+
+class NotFunctor : AbstractUnaryFunctor() {
+    override fun invokeWithReturningEffects(list: List<ConditionalEffect>): List<ConditionalEffect> = list.mapNotNull {
+        val outcome = it.simpleEffect
+
+        // Outcome guaranteed to be Returns by AbstractSequentialUnaryFunctor, but value
+        // can be non-boolean in case of type-errors in the whole expression, like "foo(bar) && 1"
+        val returnValue = (outcome as ESReturns).value
+
+        when (returnValue) {
+            ESConstant.TRUE -> ConditionalEffect(it.condition, ESReturns(ESConstant.FALSE))
+            ESConstant.FALSE -> ConditionalEffect(it.condition, ESReturns(ESConstant.TRUE))
+            else -> null
+        }
+    }
+}
@@ -0,0 +1,70 @@
+/*
+ * 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.model.functors
+
+import org.jetbrains.kotlin.contracts.model.structure.ESReturns
+import org.jetbrains.kotlin.contracts.model.structure.ESAnd
+import org.jetbrains.kotlin.contracts.model.structure.ESConstant
+import org.jetbrains.kotlin.contracts.model.structure.ESOr
+import org.jetbrains.kotlin.contracts.model.structure.lift
+import org.jetbrains.kotlin.contracts.model.ConditionalEffect
+import org.jetbrains.kotlin.contracts.model.ESEffect
+import org.jetbrains.kotlin.contracts.model.Computation
+
+class OrFunctor : AbstractBinaryFunctor() {
+    override fun invokeWithConstant(computation: Computation, constant: ESConstant): List<ESEffect> = when (constant) {
+        ESConstant.FALSE -> computation.effects
+        ESConstant.TRUE -> emptyList()
+
+        // This means that expression isn't typechecked properly
+        else -> computation.effects
+    }
+
+    override fun invokeWithReturningEffects(left: List<ConditionalEffect>, right: List<ConditionalEffect>): List<ConditionalEffect> {
+        /* Normally, `left` and `right` contain clauses that end with Returns(false/true), but if
+         expression wasn't properly typechecked, we could get some senseless clauses here, e.g.
+         with Returns(1) (note that they still *return* as guaranteed by AbstractSequentialBinaryFunctor).
+         We will just ignore such clauses in order to make smartcasting robust while typing */
+        val (leftTrue, leftFalse) = left.strictPartition(ESReturns(true.lift()), ESReturns(false.lift()))
+        val (rightTrue, rightFalse) = right.strictPartition(ESReturns(true.lift()), ESReturns(false.lift()))
+
+        val whenLeftReturnsTrue = foldConditionsWithOr(leftTrue)
+        val whenRightReturnsTrue = foldConditionsWithOr(rightTrue)
+        val whenLeftReturnsFalse = foldConditionsWithOr(leftFalse)
+        val whenRightReturnsFalse = foldConditionsWithOr(rightFalse)
+
+        // When whole Or-functor returns true, all we know is that one of arguments was true.
+        // So, to make a correct clause we have to know *both* 'Returns(true)'-conditions
+        val conditionWhenTrue = applyIfBothNotNull(whenLeftReturnsTrue, whenRightReturnsTrue, { l, r -> ESOr(l, r) })
+
+        // Even if one of 'Returns(false)' is missing, we still can argue that other condition
+        // *must* be false when whole OR-functor returns false
+        val conditionWhenFalse = applyWithDefault(whenLeftReturnsFalse, whenRightReturnsFalse, { l, r -> ESAnd(l, r) })
+
+        val result = mutableListOf<ConditionalEffect>()
+
+        if (conditionWhenTrue != null) {
+            result.add(ConditionalEffect(conditionWhenTrue, ESReturns(true.lift())))
+        }
+
+        if (conditionWhenFalse != null) {
+            result.add(ConditionalEffect(conditionWhenFalse, ESReturns(false.lift())))
+        }
+
+        return result
+    }
+}
@@ -0,0 +1,78 @@
+/*
+ * 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.model.functors
+
+import org.jetbrains.kotlin.contracts.model.structure.ESCalls
+import org.jetbrains.kotlin.contracts.model.structure.ESReturns
+import org.jetbrains.kotlin.contracts.model.structure.ESConstant
+import org.jetbrains.kotlin.contracts.model.ESValue
+import org.jetbrains.kotlin.contracts.model.structure.ESVariable
+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.Computation
+import org.jetbrains.kotlin.contracts.model.visitors.Substitutor
+import org.jetbrains.kotlin.descriptors.FunctionDescriptor
+import org.jetbrains.kotlin.descriptors.ValueDescriptor
+import org.jetbrains.kotlin.utils.addIfNotNull
+
+class SubstitutingFunctor(private val basicEffects: List<ESEffect>, private val ownerFunction: FunctionDescriptor) : AbstractReducingFunctor() {
+    override fun doInvocation(arguments: List<Computation>): List<ESEffect> {
+        if (basicEffects.isEmpty()) return emptyList()
+
+        val receiver = listOfNotNull(ownerFunction.dispatchReceiverParameter?.toESVariable(), ownerFunction.extensionReceiverParameter?.toESVariable())
+        val parameters = receiver + ownerFunction.valueParameters.map { it.toESVariable() }
+
+        assert(parameters.size == arguments.size) {
+            "Arguments and parameters size mismatch: arguments.size = ${arguments.size}, parameters.size = ${parameters.size}"
+        }
+
+        val substitutions = parameters.zip(arguments).toMap()
+        val substitutor = Substitutor(substitutions)
+        val substitutedClauses = mutableListOf<ESEffect>()
+
+        effectsLoop@ for (effect in basicEffects) {
+            when (effect) {
+                is ConditionalEffect -> effect.condition.accept(substitutor)?.effects?.forEach {
+                    substitutedClauses.addIfNotNull(combine(effect.simpleEffect, it))
+                }
+
+                is ESCalls -> {
+                    val subsitutionForCallable = substitutions[effect.callable] as? ESValue ?: continue@effectsLoop
+                    substitutedClauses += ESCalls(subsitutionForCallable, effect.kind)
+                }
+
+                else -> substitutedClauses += effect
+            }
+        }
+
+        return substitutedClauses
+    }
+
+    private fun combine(effect: SimpleEffect, substitutedCondition: ESEffect): ESEffect? {
+        if (substitutedCondition !is ConditionalEffect) return null
+
+        val effectFromCondition = substitutedCondition.simpleEffect
+        if (effectFromCondition !is ESReturns || effectFromCondition.value == ESConstant.WILDCARD) return substitutedCondition
+
+        if (effectFromCondition.value != ESConstant.TRUE) return null
+
+        return ConditionalEffect(substitutedCondition.condition, effect)
+    }
+
+    private fun ValueDescriptor.toESVariable(): ESVariable = ESVariable(this)
+}
@@ -0,0 +1,28 @@
+/*
+ * 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.model.structure
+
+import org.jetbrains.kotlin.contracts.model.Computation
+import org.jetbrains.kotlin.contracts.model.ESEffect
+import org.jetbrains.kotlin.types.KotlinType
+
+class CallComputation(override val type: KotlinType?, override val effects: List<ESEffect>) : Computation
+
+object UNKNOWN_COMPUTATION : Computation {
+    override val type: KotlinType? = null
+    override val effects: List<ESEffect> = emptyList()
+}
@@ -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.model.structure
+
+import org.jetbrains.kotlin.contracts.description.expressions.ConstantReference
+import org.jetbrains.kotlin.contracts.description.InvocationKind
+import org.jetbrains.kotlin.contracts.model.ESEffect
+import org.jetbrains.kotlin.contracts.model.ESValue
+import org.jetbrains.kotlin.contracts.model.SimpleEffect
+
+data class ESCalls(val callable: ESValue, val kind: InvocationKind): SimpleEffect() {
+    override fun isImplies(other: ESEffect): Boolean? {
+        if (other !is ESCalls) return null
+
+        if (callable != other.callable) return null
+
+        return kind == other.kind
+    }
+
+}
+
+data class ESReturns(val value: ESValue): SimpleEffect() {
+    override fun isImplies(other: ESEffect): Boolean? {
+        if (other !is ESReturns) return null
+
+        if (this.value !is ESConstant || other.value !is ESConstant) return this.value == other.value
+
+        // ESReturns(x) implies ESReturns(?) for any 'x'
+        if (other.value.constantReference == ConstantReference.WILDCARD) return true
+
+        return value == other.value
+    }
+}
@@ -0,0 +1,52 @@
+/*
+ * 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.model.structure
+
+import org.jetbrains.kotlin.contracts.model.ESExpression
+import org.jetbrains.kotlin.contracts.model.ESExpressionVisitor
+import org.jetbrains.kotlin.contracts.model.ESOperator
+import org.jetbrains.kotlin.contracts.model.ESValue
+import org.jetbrains.kotlin.contracts.model.functors.*
+
+class ESAnd(val left: ESExpression, val right: ESExpression): ESOperator {
+    override val functor: AndFunctor = AndFunctor()
+    override fun <T> accept(visitor: ESExpressionVisitor<T>): T = visitor.visitAnd(this)
+}
+
+class ESOr(val left: ESExpression, val right: ESExpression): ESOperator {
+    override val functor: OrFunctor = OrFunctor()
+    override fun <T> accept(visitor: ESExpressionVisitor<T>): T = visitor.visitOr(this)
+}
+
+class ESNot(val arg: ESExpression): ESOperator {
+    override val functor = NotFunctor()
+    override fun <T> accept(visitor: ESExpressionVisitor<T>): T = visitor.visitNot(this)
+
+}
+
+class ESIs(val left: ESValue, override val functor: IsFunctor): ESOperator {
+    val type = functor.type
+    override fun <T> accept(visitor: ESExpressionVisitor<T>): T = visitor.visitIs(this)
+}
+
+class ESEqual(val left: ESValue, val right: ESValue, isNegated: Boolean): ESOperator {
+    override val functor: EqualsFunctor = EqualsFunctor(isNegated)
+    override fun <T> accept(visitor: ESExpressionVisitor<T>): T = visitor.visitEqual(this)
+}
+
+fun ESExpression.and(other: ESExpression?): ESExpression = if (other == null) this else ESAnd(this, other)
+fun ESExpression.or(other: ESExpression?): ESExpression = if (other == null) this else ESOr(this, other)
@@ -0,0 +1,77 @@
+/*
+ * 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.model.structure
+
+import org.jetbrains.kotlin.builtins.DefaultBuiltIns
+import org.jetbrains.kotlin.descriptors.ValueDescriptor
+import org.jetbrains.kotlin.contracts.description.expressions.ConstantReference
+import org.jetbrains.kotlin.contracts.description.expressions.BooleanConstantReference
+import org.jetbrains.kotlin.contracts.model.ESExpressionVisitor
+import org.jetbrains.kotlin.contracts.model.ESValue
+import org.jetbrains.kotlin.types.KotlinType
+import org.jetbrains.kotlin.types.typeUtil.makeNullable
+import java.util.*
+
+open class ESVariable(val descriptor: ValueDescriptor) : ESValue(descriptor.type) {
+    override fun <T> accept(visitor: ESExpressionVisitor<T>): T = visitor.visitVariable(this)
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other?.javaClass != javaClass) return false
+
+        other as ESVariable
+
+        if (descriptor != other.descriptor) return false
+
+        return true
+    }
+
+    override fun hashCode(): Int = descriptor.hashCode()
+
+    override fun toString(): String = descriptor.toString()
+}
+
+open class ESConstant private constructor(open val constantReference: ConstantReference, override val type: KotlinType) : ESValue(type) {
+    override fun <T> accept(visitor: ESExpressionVisitor<T>): T = visitor.visitConstant(this)
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other?.javaClass != javaClass) return false
+
+        other as ESConstant
+
+        if (constantReference != other.constantReference) return false
+
+        return true
+    }
+
+    override fun hashCode(): Int = Objects.hashCode(constantReference)
+
+    override fun toString(): String = constantReference.name
+
+    companion object {
+        val TRUE = ESConstant(BooleanConstantReference.TRUE, DefaultBuiltIns.Instance.booleanType)
+        val FALSE = ESConstant(BooleanConstantReference.FALSE, DefaultBuiltIns.Instance.booleanType)
+        val NULL = ESConstant(ConstantReference.NULL, DefaultBuiltIns.Instance.nothingType.makeNullable())
+        val NOT_NULL = ESConstant(ConstantReference.NOT_NULL, DefaultBuiltIns.Instance.anyType)
+        val WILDCARD = ESConstant(ConstantReference.WILDCARD, DefaultBuiltIns.Instance.anyType.makeNullable())
+    }
+
+    fun isNullConstant(): Boolean = this == NULL || this == NOT_NULL
+}
+
+fun Boolean.lift(): ESConstant = if (this) ESConstant.TRUE else ESConstant.FALSE
@@ -0,0 +1,83 @@
+/*
+ * 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.model.visitors
+
+import org.jetbrains.kotlin.builtins.DefaultBuiltIns
+import org.jetbrains.kotlin.contracts.model.*
+import org.jetbrains.kotlin.contracts.model.structure.*
+
+class InfoCollector(private val observedEffect: ESEffect) : ESExpressionVisitor<MutableContextInfo> {
+    private var isInverted: Boolean = false
+
+    fun collectFromSchema(schema: List<ESEffect>): MutableContextInfo =
+            schema.mapNotNull { collectFromEffect(it) }.fold(MutableContextInfo.EMPTY, { resultingInfo, clauseInfo -> resultingInfo.and(clauseInfo) })
+
+    private fun collectFromEffect(effect: ESEffect): MutableContextInfo? {
+        if (effect !is ConditionalEffect) {
+            return MutableContextInfo.EMPTY.fire(effect)
+        }
+
+        // Check for information from conditional effects
+        return when (observedEffect.isImplies(effect.simpleEffect)) {
+            // observed effect implies clause's effect => clause's effect was fired => clause's condition is true
+            true -> effect.condition.accept(this)
+
+            // Observed effect *may* or *doesn't* implies clause's - no useful information
+            null, false -> null
+        }
+    }
+
+    override fun visitIs(isOperator: ESIs): MutableContextInfo = with(isOperator) {
+        if (functor.isNegated != isInverted) MutableContextInfo.EMPTY.notSubtype(left, type) else MutableContextInfo.EMPTY.subtype(left, type)
+    }
+
+    override fun visitEqual(equal: ESEqual): MutableContextInfo = with(equal) {
+        if (functor.isNegated != isInverted) MutableContextInfo.EMPTY.notEqual(left, right) else MutableContextInfo.EMPTY.equal(left, right)
+    }
+
+    override fun visitAnd(and: ESAnd): MutableContextInfo {
+        val leftInfo = and.left.accept(this)
+        val rightInfo = and.right.accept(this)
+
+        return if (isInverted) leftInfo.or(rightInfo) else leftInfo.and(rightInfo)
+    }
+
+    override fun visitNot(not: ESNot): MutableContextInfo = inverted { not.arg.accept(this) }
+
+    override fun visitOr(or: ESOr): MutableContextInfo {
+        val leftInfo = or.left.accept(this)
+        val rightInfo = or.right.accept(this)
+        return if (isInverted) leftInfo.and(rightInfo) else leftInfo.or(rightInfo)
+    }
+
+    override fun visitVariable(esVariable: ESVariable): MutableContextInfo {
+        return if (esVariable.type != DefaultBuiltIns.Instance.booleanType)
+            MutableContextInfo.EMPTY
+        else
+            MutableContextInfo.EMPTY.equal(esVariable, isInverted.not().lift())
+    }
+
+    override fun visitConstant(esConstant: ESConstant): MutableContextInfo = MutableContextInfo.EMPTY
+
+    private fun <R> inverted(block: () -> R): R {
+        isInverted = isInverted.not()
+        val result = block()
+        isInverted = isInverted.not()
+        return result
+    }
+}
+
@@ -0,0 +1,111 @@
+/*
+ * 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.model.visitors
+
+import org.jetbrains.kotlin.contracts.model.*
+import org.jetbrains.kotlin.contracts.model.structure.*
+import org.jetbrains.kotlin.types.typeUtil.isSubtypeOf
+
+/**
+ * Reduces given list of effects by evaluating constant expressions,
+ * throwing away senseless checks and infeasible clauses, etc.
+ */
+class Reducer : ESExpressionVisitor<ESExpression?> {
+    fun reduceEffects(schema: List<ESEffect>): List<ESEffect> =
+            schema.mapNotNull { reduceEffect(it) }
+
+    private fun reduceEffect(effect: ESEffect): ESEffect? {
+        when (effect) {
+            is SimpleEffect -> return effect
+            is ConditionalEffect -> {
+                // Reduce condition
+                val reducedCondition = effect.condition.accept(this) ?: return null
+
+                // Filter never executed conditions
+                if (reducedCondition is ESConstant && reducedCondition == ESConstant.FALSE) return null
+
+                // Add always firing effects
+                if (reducedCondition is ESConstant && reducedCondition == ESConstant.TRUE) return effect.simpleEffect
+
+                // Leave everything else as is
+                return effect
+            }
+        }
+    }
+
+    override fun visitIs(isOperator: ESIs): ESExpression {
+        val reducedArg = isOperator.left.accept(this) as ESValue
+
+        val result = when (reducedArg) {
+            is ESConstant -> reducedArg.type.isSubtypeOf(isOperator.functor.type)
+            is ESVariable -> if (reducedArg.type?.isSubtypeOf(isOperator.functor.type) == true) true else null
+            else -> throw IllegalStateException("Unknown ESValue: $reducedArg")
+        }
+
+        // Result is unknown, do not evaluate
+        result ?: return ESIs(reducedArg, isOperator.functor)
+
+        return result.xor(isOperator.functor.isNegated).lift()
+    }
+
+    override fun visitEqual(equal: ESEqual): ESExpression {
+        val reducedLeft = equal.left.accept(this) as ESValue
+        val reducedRight = equal.right
+
+        if (reducedLeft is ESConstant) return (reducedLeft == reducedRight).xor(equal.functor.isNegated).lift()
+
+        return ESEqual(reducedLeft, reducedRight, equal.functor.isNegated)
+    }
+
+    override fun visitAnd(and: ESAnd): ESExpression? {
+        val reducedLeft = and.left.accept(this) ?: return null
+        val reducedRight = and.right.accept(this) ?: return null
+
+        return when {
+            reducedLeft == false.lift() || reducedRight == false.lift() -> false.lift()
+            reducedLeft == true.lift() -> reducedRight
+            reducedRight == true.lift() -> reducedLeft
+            else -> ESAnd(reducedLeft, reducedRight)
+        }
+    }
+
+    override fun visitOr(or: ESOr): ESExpression? {
+        val reducedLeft = or.left.accept(this) ?: return null
+        val reducedRight = or.right.accept(this) ?: return null
+
+        return when {
+            reducedLeft == true.lift() || reducedRight == true.lift() -> true.lift()
+            reducedLeft == false.lift() -> reducedRight
+            reducedRight == false.lift() -> reducedLeft
+            else -> ESOr(reducedLeft, reducedRight)
+        }
+    }
+
+    override fun visitNot(not: ESNot): ESExpression? {
+        val reducedArg = not.arg.accept(this) ?: return null
+
+        return when (reducedArg) {
+            ESConstant.TRUE -> ESConstant.FALSE
+            ESConstant.FALSE -> ESConstant.TRUE
+            else -> reducedArg
+        }
+    }
+
+    override fun visitVariable(esVariable: ESVariable): ESVariable = esVariable
+
+    override fun visitConstant(esConstant: ESConstant): ESConstant = esConstant
+}
@@ -0,0 +1,61 @@
+/*
+ * 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.model.visitors
+
+import org.jetbrains.kotlin.builtins.DefaultBuiltIns
+import org.jetbrains.kotlin.contracts.model.*
+import org.jetbrains.kotlin.contracts.model.structure.*
+
+/**
+ * Given an [ESExpression], substitutes all variables in it using provided [substitutions] map,
+ * and then flattens resulting tree, producing an [EffectSchema], which describes effects
+ * of this [ESExpression] with effects of arguments taken into consideration.
+ */
+class Substitutor(private val substitutions: Map<ESVariable, Computation>) : ESExpressionVisitor<Computation?> {
+    override fun visitIs(isOperator: ESIs): Computation? {
+        val arg = isOperator.left.accept(this) ?: return null
+        return CallComputation(DefaultBuiltIns.Instance.booleanType, isOperator.functor.invokeWithArguments(arg))
+    }
+
+    override fun visitNot(not: ESNot): Computation? {
+        val arg = not.arg.accept(this) ?: return null
+        return CallComputation(DefaultBuiltIns.Instance.booleanType, not.functor.invokeWithArguments(arg))
+    }
+
+    override fun visitEqual(equal: ESEqual): Computation? {
+        val left = equal.left.accept(this) ?: return null
+        val right = equal.right.accept(this) ?: return null
+        return CallComputation(DefaultBuiltIns.Instance.booleanType, equal.functor.invokeWithArguments(listOf(left, right)))
+    }
+
+    override fun visitAnd(and: ESAnd): Computation? {
+        val left = and.left.accept(this) ?: return null
+        val right = and.right.accept(this) ?: return null
+        return CallComputation(DefaultBuiltIns.Instance.booleanType, and.functor.invokeWithArguments(left, right))
+    }
+
+    override fun visitOr(or: ESOr): Computation? {
+        val left = or.left.accept(this) ?: return null
+        val right = or.right.accept(this) ?: return null
+        return CallComputation(DefaultBuiltIns.Instance.booleanType, or.functor.invokeWithArguments(left, right))
+    }
+
+    override fun visitVariable(esVariable: ESVariable): Computation?
+            = substitutions[esVariable] ?: esVariable
+
+    override fun visitConstant(esConstant: ESConstant): Computation? = esConstant
+}