Observe all unbound logicals inside Occurrence to check contract (MPSCR-66)

Previously only logicals directly used ar occurrence args
were observed. Now terms in occurrence args are traversed
recursively and all contained logicals are observed.

Also clear occurrence contract observers on discarding occ-s.
Introduce a generic way to clear observers in LogicalState.
This commit is contained in:
Grigorii Kirgizov 2020-07-27 15:33:29 +03:00
parent 3ef1c53a85
commit 2a0d4ef076
6 changed files with 171 additions and 31 deletions

View File

@ -27,6 +27,9 @@ interface LogicalStateObservable {
fun addForwardingObserver(logical: Logical<*>, observer: ForwardingLogicalObserver)
fun removeForwardingObserver(logical: Logical<*>, observer: ForwardingLogicalObserver)
= removeForwardingObserversWhere(logical, observer::equals)
fun removeForwardingObserversWhere(logical: Logical<*>, where: (ForwardingLogicalObserver) -> Boolean)
}

View File

@ -20,12 +20,13 @@ import jetbrains.mps.logic.reactor.core.*
import jetbrains.mps.logic.reactor.evaluation.EvaluationTrace
import jetbrains.mps.logic.reactor.program.IncrementalSpec
import jetbrains.mps.logic.reactor.evaluation.SessionToken
import jetbrains.mps.logic.reactor.logical.Logical
import jetbrains.mps.logic.reactor.logical.LogicalContext
import jetbrains.mps.logic.reactor.program.Constraint
import jetbrains.mps.logic.reactor.program.Rule
import jetbrains.mps.logic.reactor.util.Profiler
import jetbrains.mps.logic.reactor.util.profile
import kotlin.collections.ArrayList
import kotlin.collections.HashSet
/**
@ -52,6 +53,9 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di
private val activationQueue: ContinuedActivationQueue = ContinuedActivationQueue(journalIndex, RuleOrdering(ruleIndex))
private val occurrenceContractObserver: OccurrenceContractObserver? =
if (ispec.assertLevel().assertContracts()) OccurrenceContractObserver(logicalState, ispec) else null
private val invalidFeedbackKeys: MutableSet<Any> = mutableSetOf<Any>()
private data class MatchCandidate(val rule: Rule, val occChunk: MatchJournal.OccChunk)
@ -110,6 +114,7 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di
private fun invalidateChunk(chunk: MatchJournal.Chunk, invalidJustifications: Collection<Justified>): Iterable<Occurrence> {
// 'Undo' all activated in this chunk occurrences
// todo: need clearing observers in logicalState for occurrences we drop?
chunk.activatedLog().forEach {
dispatchingFront = dispatchingFront.forget(it)
}
@ -222,9 +227,7 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di
logActivation(active)
active.revive(logicalState)
if (ispec.assertLevel().assertContracts()) {
active.addContractObservers(logicalState)
}
occurrenceContractObserver?.onActivated(active)
}
assert(active.alive)
@ -338,6 +341,8 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di
occ.terminate(logicalState)
occurrenceContractObserver?.onDiscarded(occ)
}
trace.discard(occ)
@ -378,32 +383,6 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di
}
}
private fun Occurrence.addContractObservers(observable: LogicalStateObservable) {
if (this.isPrincipal) {
UnmodifiableLogicalObserver(this, observable)
}
}
internal class UnmodifiableLogicalObserver(val source: Occurrence, observable: LogicalStateObservable): ForwardingLogicalObserver {
init {
for (a in HashSet(source.arguments)) { // avoid duplicate subscriptions
if (a is Logical<*>) {
observable.addForwardingObserver(a, this)
}
}
}
override fun valueUpdated(logical: Logical<*>, controller: Controller) = doCheckContract(logical, controller)
override fun parentUpdated(logical: Logical<*>, controller: Controller) = doCheckContract(logical, controller)
private fun doCheckContract(logical: Logical<*>, controller: Controller) =
checkContract(false) {
"$logical can't be unified because it's used in principal occurrence $source"
}
}
private fun MatchJournal.MatchChunk.dependsOnAny(utags: Iterable<Any>): Boolean =
utags.contains(this.ruleUniqueTag) || utags.any { utag -> dependsOnRule(utag) }

View File

@ -105,6 +105,13 @@ class LogicalState : LogicalStateObservable, LogicalObserver
}
}
override fun removeForwardingObserversWhere(logical: Logical<*>, where: (ForwardingLogicalObserver) -> Boolean) {
currentFrame().removeForwardingObserversWhere(logical, where)
if (!currentFrame().isObserving(logical)) {
logical.removeObserver(this)
}
}
override fun valueUpdated(logical: Logical<*>) {
// forward to the top frame with added transient state (Controller)
currentFrame().valueUpdated(logical, controller!!)
@ -163,6 +170,13 @@ class LogicalStateFrame : LogicalStateObservable, ForwardingLogicalObserver
}
}
override fun removeForwardingObserversWhere(logical: Logical<*>, where: (ForwardingLogicalObserver) -> Boolean) {
observers[logical]?.apply {
removeIf(where)
if (isEmpty()) observers.remove(logical)
}
}
fun observed(): Sequence<Logical<*>> = observers.keys.asSequence()
// observers.keys().asSequence().map { it.wrapped }

View File

@ -0,0 +1,108 @@
/*
* Copyright 2014-2020 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 jetbrains.mps.logic.reactor.core.internal
import jetbrains.mps.logic.reactor.core.Controller
import jetbrains.mps.logic.reactor.core.ForwardingLogicalObserver
import jetbrains.mps.logic.reactor.core.LogicalStateObservable
import jetbrains.mps.logic.reactor.core.Occurrence
import jetbrains.mps.logic.reactor.logical.Logical
import jetbrains.mps.logic.reactor.program.IncrementalSpec
import jetbrains.mps.unification.Term
import kotlin.collections.HashSet
internal class OccurrenceContractObserver(private val observable: LogicalStateObservable, override val ispec: IncrementalSpec): IncrSpecHolder {
private val observers: HashMap<Int, UnmodifiableLogicalObserver> = hashMapOf()
fun onActivated(occ: Occurrence) {
if (occ.isPrincipal) {
observers[occ.identity] = UnmodifiableLogicalObserver(occ, observable)
}
}
fun onDiscarded(occ: Occurrence) {
// NB: works between incremental sessions only if this instance is preserved between them
// observers.remove(occ.identity)?.removeObservers(observable)
occ.removeContractObservers(observable)
observers.remove(occ.identity)
}
}
internal fun Occurrence.removeContractObservers(observable: LogicalStateObservable) {
for (observedLogical in this.usedUnboundLogicals()) {
observable.removeForwardingObserversWhere(observedLogical) { observer ->
observer is UnmodifiableLogicalObserver && observer.source.identity == this.identity
}
}
}
internal class UnmodifiableLogicalObserver(val source: Occurrence, observable: LogicalStateObservable): ForwardingLogicalObserver {
private val observed: HashSet<Logical<*>> = HashSet()
private fun observe(arg: Logical<*>, observable: LogicalStateObservable) {
if (!observed.contains(arg)) {
observable.addForwardingObserver(arg, this)
observed.add(arg)
}
}
init {
for (unboundLogical in source.usedUnboundLogicals()) {
observe(unboundLogical, observable)
}
}
fun removeObservers(observable: LogicalStateObservable) {
for (logical in observed) {
observable.removeForwardingObserver(logical, this)
}
observed.clear()
}
override fun valueUpdated(logical: Logical<*>, controller: Controller) = doCheckContract(logical, controller)
override fun parentUpdated(logical: Logical<*>, controller: Controller) = doCheckContract(logical, controller)
private fun doCheckContract(logical: Logical<*>, controller: Controller) =
checkContract(false) {
"$logical can't be unified because it's used in principal occurrence $source"
}
}
internal fun Occurrence.usedUnboundLogicals(): Set<Logical<*>> {
val unique = hashSetOf<Logical<*>>()
for (arg in arguments) {
val argLogicals = when (arg) {
is Logical<*> ->
if (!arg.isBound) listOf(arg)
else when(val value = arg.findRoot().value()) {
is Term -> value.unboundLogicals()
else -> emptyList()
}
is Term -> arg.unboundLogicals()
else -> emptyList()
}
unique.addAll(argLogicals)
}
return unique
}

View File

@ -30,7 +30,14 @@ class TermWalker(vararg visitors: TermVisitor<out Term>) {
@Throws(Exception::class)
abstract fun visit(t: T): MutableCollection<out Term>
// abstract fun visit(t: T): Collection<Term>
}
class SimpleVisitor<T : Term?>(
kind: Term.Kind,
private inline val f: (T) -> MutableCollection<out Term>
) : TermVisitor<T>(kind) {
override fun visit(t: T) = f(t)
}
private val visitorMap: MutableMap<Term.Kind, TermVisitor<out Term>> = EnumMap(Term.Kind::class.java)
@ -74,4 +81,30 @@ class TermWalker(vararg visitors: TermVisitor<out Term>) {
companion object {
private val SINGLETON = Any()
}
}
}
internal fun Term.unboundLogicals(): Collection<Logical<*>> = logicalsWhere { !it.isBound }
internal inline fun Term.logicalsWhere(crossinline where: (Logical<*>) -> Boolean): Collection<Logical<*>> {
val collected = arrayListOf<Logical<*>>()
TermWalker(
TermWalker.SimpleVisitor<Term>(Term.Kind.FUN) { t ->
t.arguments()
},
TermWalker.SimpleVisitor<Term>(Term.Kind.REF) { ref ->
if (ref.get() !== ref) {
Collections.singletonList(ref.get())
}
Collections.emptyList()
},
TermWalker.SimpleVisitor<Term>(Term.Kind.VAR) { v ->
if (v is LogicalOwner && where(v.logical())) {
collected.add(v.logical())
}
Collections.emptyList()
}
).walk(this)
return collected
}

View File

@ -230,6 +230,9 @@ class MockController : Controller {
override fun removeForwardingObserver(logical: Logical<*>, observer: ForwardingLogicalObserver) {
}
override fun removeForwardingObserversWhere(logical: Logical<*>, where: (ForwardingLogicalObserver) -> Boolean) {
}
}
override fun storeView(): StoreView {