From 0d0813d352786b962019dc7b0f4978043f82c571 Mon Sep 17 00:00:00 2001 From: Grigorii Kirgizov Date: Wed, 22 Jul 2020 11:42:21 +0300 Subject: [PATCH] Add logical incr contract assertions as observers (implements MPSCR-66) --- .../core/internal/ConstraintsProcessing.kt | 29 +++++++++++- .../reactor/core/internal/IncrSpecHolder.kt | 19 +++++++- ...IncrementalContractViolationException.java | 29 ++++++++++++ .../program/IncrementalProgramSpec.java | 5 +++ reactor/Test/test/MockIncrProgSpec.kt | 8 +++- reactor/Test/test/TestIncrementalProgram.kt | 45 +++++++++++++++++++ reactor/Test/test/TestStoreAwareJournal.kt | 3 +- 7 files changed, 133 insertions(+), 5 deletions(-) create mode 100644 reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalContractViolationException.java diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt index c0bf641e..5efd5bde 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt @@ -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): Boolean = utags.contains(this.ruleUniqueTag) || utags.any { utag -> dependsOnRule(utag) } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/IncrSpecHolder.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/IncrSpecHolder.kt index 48aa8708..521b5df6 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/IncrSpecHolder.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/IncrSpecHolder.kt @@ -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) -} \ No newline at end of file + +} + + +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) +} diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalContractViolationException.java b/reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalContractViolationException.java new file mode 100644 index 00000000..74698cf8 --- /dev/null +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalContractViolationException.java @@ -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); + } + +} diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalProgramSpec.java b/reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalProgramSpec.java index 928df908..4a38d5d0 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalProgramSpec.java +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/program/IncrementalProgramSpec.java @@ -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(); diff --git a/reactor/Test/test/MockIncrProgSpec.kt b/reactor/Test/test/MockIncrProgSpec.kt index 17a30d69..7d31f5c7 100644 --- a/reactor/Test/test/MockIncrProgSpec.kt +++ b/reactor/Test/test/MockIncrProgSpec.kt @@ -23,12 +23,18 @@ import jetbrains.mps.logic.reactor.program.Rule class MockIncrProgSpec( val principalRuleTags: Set, val principalCtrSyms: Set, - val weakPrincipalRuleTags: Set + val weakPrincipalRuleTags: Set, + private var checkContracts: Boolean = false ) : IncrementalProgramSpec { + constructor(principalRuleTags: Set, principalCtrSyms: Set) : 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 } \ No newline at end of file diff --git a/reactor/Test/test/TestIncrementalProgram.kt b/reactor/Test/test/TestIncrementalProgram.kt index b26af280..34f259f5 100644 --- a/reactor/Test/test/TestIncrementalProgram.kt +++ b/reactor/Test/test/TestIncrementalProgram.kt @@ -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 PredicateInvocation.eq(left: T, right: T) = invocationContext().tellEquals(left, right) + + @Test fun noChangesRelaunch() { lateinit var storeSnapshot: Iterable @@ -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("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( diff --git a/reactor/Test/test/TestStoreAwareJournal.kt b/reactor/Test/test/TestStoreAwareJournal.kt index 9f9a16d2..6fd84aae 100644 --- a/reactor/Test/test/TestStoreAwareJournal.kt +++ b/reactor/Test/test/TestStoreAwareJournal.kt @@ -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(