natas_hw
/
mps-coderules
mirror of https://github.com/JetBrains/mps-coderules
0
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Add logical incr contract assertions as observers (implements MPSCR-66)

This commit is contained in:
Grigorii Kirgizov 2020-07-22 11:42:21 +03:00
parent 0fd3311c04
commit 0d0813d352
7 changed files with 133 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt
View File

@ -20,6 +20,7 @@ import jetbrains.mps.logic.reactor.core.*
import jetbrains.mps.logic.reactor.evaluation.EvaluationTrace
import jetbrains.mps.logic.reactor.program.IncrementalProgramSpec
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
@ -220,6 +221,8 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di
active.stored = true
logActivation(active)
active.revive(logicalState)
if (ispec.assertContracts()) active.addContractObservers(logicalState)
}
assert(active.alive)
@ -288,7 +291,6 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di
.then { controller.processBody(match, parent, it) }
.also { trace.finish(match) }
private fun continueReplacedHeads(match: RuleMatchEx, parent: MatchJournal.MatchChunk) {
if (!isFront() && match.isPrincipal) {
profiler.profile("continueReplaced") {
@ -375,6 +377,31 @@ 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) }

19
reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/IncrSpecHolder.kt
View File

@ -18,6 +18,7 @@ package jetbrains.mps.logic.reactor.core.internal
import jetbrains.mps.logic.reactor.core.Occurrence
import jetbrains.mps.logic.reactor.evaluation.RuleMatch
import jetbrains.mps.logic.reactor.program.IncrementalContractViolationException
import jetbrains.mps.logic.reactor.program.IncrementalProgramSpec
import jetbrains.mps.logic.reactor.program.Rule
@ -31,4 +32,20 @@ interface IncrSpecHolder {
val RuleMatch.isWeakPrincipal get() = ispec.isWeakPrincipal(this.rule())
val Rule.isWeakPrincipal get() = ispec.isWeakPrincipal(this)
}
}
inline fun checkContract(value: Boolean) {
checkContract(value) { "Contract assertion failed" }
}
inline fun checkContract(value: Boolean, lazyMsg: () -> String) {
if (!value) throw IncrementalContractViolationException(lazyMsg())
}
inline fun IncrSpecHolder.assertContract(lazyValue: () -> Boolean) {
assertContract(lazyValue) { "Contract assertion failed" }
}
inline fun IncrSpecHolder.assertContract(lazyValue: () -> Boolean, noinline lazyMsg: () -> String) {
if (ispec.assertContracts()) checkContract(lazyValue(), lazyMsg)
}

29
reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalContractViolationException.java Normal file
View File

@ -0,0 +1,29 @@
/*
* 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.program;
public class IncrementalContractViolationException extends IllegalStateException {
public IncrementalContractViolationException(String message) {
super(message);
}
public IncrementalContractViolationException(String message, Throwable ex) {
super(message, ex);
}
}

5
reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalProgramSpec.java
View File

@ -22,6 +22,8 @@ public interface IncrementalProgramSpec {
boolean isPrincipal(Rule rule);
boolean isWeakPrincipal(Rule rule);
boolean assertContracts();
class NonIncrSpec implements IncrementalProgramSpec {
@Override
public boolean isPrincipal(Constraint ctr) { return false; }
@ -29,6 +31,9 @@ public interface IncrementalProgramSpec {
public boolean isPrincipal(Rule rule) { return false; }
@Override
public boolean isWeakPrincipal(Rule rule) { return false; }
@Override
public boolean assertContracts() { return false; }
}
NonIncrSpec DefaultSpec = new NonIncrSpec();

8
reactor/Test/test/MockIncrProgSpec.kt
View File

@ -23,12 +23,18 @@ import jetbrains.mps.logic.reactor.program.Rule
class MockIncrProgSpec(
val principalRuleTags: Set<Any>,
val principalCtrSyms: Set<ConstraintSymbol>,
val weakPrincipalRuleTags: Set<Any>
val weakPrincipalRuleTags: Set<Any>,
private var checkContracts: Boolean = false
) : IncrementalProgramSpec {
constructor(principalRuleTags: Set<Any>, principalCtrSyms: Set<ConstraintSymbol>) :
this(principalRuleTags, principalCtrSyms, emptySet())
fun withContractChecks() = this.also { checkContracts = true }
override fun isPrincipal(ctr: Constraint): Boolean = principalCtrSyms.contains(ctr.symbol())
override fun isPrincipal(rule: Rule): Boolean = principalRuleTags.contains(rule.uniqueTag())
override fun isWeakPrincipal(rule: Rule): Boolean = weakPrincipalRuleTags.contains(rule.uniqueTag())
override fun assertContracts(): Boolean = checkContracts
}

45
reactor/Test/test/TestIncrementalProgram.kt
View File

@ -6,11 +6,14 @@ import jetbrains.mps.logic.reactor.core.internal.MatchJournal
import jetbrains.mps.logic.reactor.evaluation.SessionToken
import jetbrains.mps.logic.reactor.evaluation.EvaluationResult
import jetbrains.mps.logic.reactor.evaluation.EvaluationSession
import jetbrains.mps.logic.reactor.evaluation.PredicateInvocation
import jetbrains.mps.logic.reactor.program.Constraint
import jetbrains.mps.logic.reactor.program.ConstraintSymbol
import jetbrains.mps.logic.reactor.program.IncrementalContractViolationException
import org.junit.*
import org.junit.Assert.*
import program.MockConstraint
import solver.tellEquals
/*
* Copyright 2014-2019 JetBrains s.r.o.
@ -92,6 +95,9 @@ class TestIncrementalProgram {
private fun EvaluationResult.lastChunkSymbols() = this.lastChunk().activatedLog().constraintSymbols()
private fun <T : Any> PredicateInvocation.eq(left: T, right: T) = invocationContext().tellEquals(left, right)
@Test
fun noChangesRelaunch() {
lateinit var storeSnapshot: Iterable<ConstraintSymbol>
@ -1539,6 +1545,45 @@ class TestIncrementalProgram {
}
}
@Test(expected = IncrementalContractViolationException::class)
fun violatePrincipalLogicalContract() {
val progSpec = MockIncrProgSpec(
setOf("main", "produceBound"),
setOf(sym1("foo"))
).withContractChecks()
val (X, Y) = metaLogical<Int>("X", "Y")
programWithRules(
rule("main",
headReplaced(
constraint("main")
),
body(
pconstraint("foo", X)
)),
rule("produceBound",
headKept(
pconstraint("foo", X)
),
body(
statement({ x, y -> eq(x,y) }, X, Y),
constraint("hasBound", Y)
)),
rule("bindVar",
headKept(
constraint("hasBound", Y)
),
body(
statement({ y -> y.set(42) }, Y)
))
).launch("violate contract assertion", progSpec) { result ->
result.storeView().constraintSymbols() shouldBe setOf(sym1("foo"), sym1("hasBound"))
}
}
@Test
fun expectTypeGenericNonprincipal() {
val progSpec = MockIncrProgSpec(

3
reactor/Test/test/TestStoreAwareJournal.kt
View File

@ -27,10 +27,9 @@ import org.junit.Ignore
class TestStoreAwareJournal {
private object LegacyMockIncrProgSpec : IncrementalProgramSpec {
private object LegacyMockIncrProgSpec : IncrementalProgramSpec.NonIncrSpec() {
override fun isPrincipal(ctr: Constraint): Boolean = ctr.isPrincipal
override fun isPrincipal(rule: Rule): Boolean = rule.all().any { it is Constraint && it.isPrincipal }
override fun isWeakPrincipal(rule: Rule): Boolean = false
}
private class JournalDispatcherHelper(