From a2a92561f7b612b472b5b7e49a2d5ca86802092f Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 31 Jan 2024 17:10:28 +0100 Subject: feat(language): validate module isolation --- subprojects/frontend/src/language/problem.grammar | 4 +- .../src/language/problemLanguageSupport.ts | 2 +- .../java/tools/refinery/language/Problem.xtext | 7 +- .../language/formatting2/ProblemFormatter.java | 3 +- .../tools/refinery/language/utils/ProblemUtil.java | 6 + .../language/validation/ProblemValidator.java | 46 +++++-- .../tests/validation/AssertionValidationTest.java | 1 - .../tests/validation/ModuleValidationTest.java | 145 +++++++++++++++++++++ 8 files changed, 198 insertions(+), 16 deletions(-) create mode 100644 subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java (limited to 'subprojects') diff --git a/subprojects/frontend/src/language/problem.grammar b/subprojects/frontend/src/language/problem.grammar index b08a9c36..ac451e7a 100644 --- a/subprojects/frontend/src/language/problem.grammar +++ b/subprojects/frontend/src/language/problem.grammar @@ -57,10 +57,10 @@ statement { // RuleBody { ":" sep "==>" sep "." } //} | AtomDeclaration { - ckw<"atom"> sep<",", AtomNodeName> "." + kw<"declare">? ckw<"atom"> sep<",", AtomNodeName> "." } | NodeDeclaration { - (ckw<"node"> | ckw<"multi">) sep<",", NodeName> "." + (kw<"declare"> | kw<"declare">? ckw<"multi">) sep<",", NodeName> "." } | ScopeDeclaration { kw<"scope"> sep<",", ScopeElement> "." diff --git a/subprojects/frontend/src/language/problemLanguageSupport.ts b/subprojects/frontend/src/language/problemLanguageSupport.ts index 3847fdd8..2483c2e3 100644 --- a/subprojects/frontend/src/language/problemLanguageSupport.ts +++ b/subprojects/frontend/src/language/problemLanguageSupport.ts @@ -28,7 +28,7 @@ const parserWithMetadata = parser.configure({ LineComment: t.lineComment, BlockComment: t.blockComment, 'module problem class enum pred fn scope': t.definitionKeyword, - 'node atom multi': t.definitionKeyword, + 'declare atom multi': t.definitionKeyword, 'abstract extends refers contains container opposite': t.modifier, 'default error contained containment': t.modifier, 'true false unknown error': t.keyword, diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext index c5c42ebe..4ce3fae1 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext +++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext @@ -256,10 +256,11 @@ ExactMultiplicity: exactValue=INT; NodeDeclaration: - kind=NodeKind nodes+=EnumLiteral ("," nodes+=EnumLiteral)* "."; + ("declare" | "declare"? kind=NodeKind) + nodes+=EnumLiteral ("," nodes+=EnumLiteral)* "."; enum NodeKind: - NODE="node" | ATOM="atom" | MULTI="multi"; + ATOM="atom" | MULTI="multi"; UpperBound returns ecore::EInt: INT | "*"; @@ -274,7 +275,7 @@ Identifier: NonContainmentIdentifier | "contains" | "container"; NonContainmentIdentifier: - ID | "node" | "atom" | "multi" | "contained" | + ID | "atom" | "multi" | "contained" | "sum" | "prod" | "min" | "max" | "problem" | "module"; Real returns ecore::EDouble: diff --git a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java index 0b87e8bb..d6ece1ea 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java +++ b/subprojects/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java @@ -23,7 +23,7 @@ public class ProblemFormatter extends AbstractJavaFormatter { protected void format(Problem problem, IFormattableDocument doc) { doc.prepend(problem, this::noSpace); var region = regionFor(problem); - doc.append(region.feature(ProblemPackage.Literals.PROBLEM__KIND), this::oneSpace); + doc.prepend(region.feature(ProblemPackage.Literals.NAMED_ELEMENT__NAME), this::oneSpace); doc.prepend(region.keyword("."), this::noSpace); appendNewLines(doc, region.keyword("."), this::twoNewLines); for (var statement : problem.getStatements()) { @@ -135,6 +135,7 @@ public class ProblemFormatter extends AbstractJavaFormatter { protected void format(NodeDeclaration nodeDeclaration, IFormattableDocument doc) { surroundNewLines(doc, nodeDeclaration, this::singleNewLine); var region = regionFor(nodeDeclaration); + doc.append(region.keyword("declare"), this::oneSpace); doc.append(region.feature(ProblemPackage.Literals.NODE_DECLARATION__KIND), this::oneSpace); formatList(region, ",", doc); doc.prepend(region.keyword("."), this::noSpace); diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java index ee0e141d..0f87c04b 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java +++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java @@ -8,6 +8,7 @@ package tools.refinery.language.utils; import org.eclipse.emf.common.util.URI; import org.eclipse.emf.ecore.EObject; import org.eclipse.emf.ecore.util.EcoreUtil; +import org.eclipse.xtext.EcoreUtil2; import tools.refinery.language.model.problem.*; public final class ProblemUtil { @@ -126,6 +127,11 @@ public final class ProblemUtil { }; } + public static boolean isInModule(EObject eObject) { + var problem = EcoreUtil2.getContainerOfType(eObject, Problem.class); + return problem != null && problem.getKind() == ModuleKind.MODULE; + } + private static URI getLibraryUri() { var libraryResource = ProblemUtil.class.getClassLoader() .getResource("tools/refinery/language/%s.problem".formatted(BUILTIN_LIBRARY_NAME)); diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java index a95e8b3c..4cbb02c2 100644 --- a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java +++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java @@ -86,8 +86,8 @@ public class ProblemValidator extends AbstractProblemValidator { var variableOrNode = expr.getVariableOrNode(); if (variableOrNode instanceof Node node && !ProblemUtil.isAtomNode(node)) { var name = node.getName(); - var message = ("Only individuals can be referenced in predicates. " + - "Mark '%s' as individual with the declaration 'indiv %s.'").formatted(name, name); + var message = ("Only atoms can be referenced in predicates. " + + "Mark '%s' as an atom with the declaration 'atom %s.'").formatted(name, name); error(message, expr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, INSIGNIFICANT_INDEX, NODE_CONSTANT_ISSUE); } @@ -302,6 +302,10 @@ public class ProblemValidator extends AbstractProblemValidator { @Check public void checkTypeScope(TypeScope typeScope) { checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1); + if (typeScope.isIncrement() && ProblemUtil.isInModule(typeScope)) { + acceptError("Incremental type scopes are not supported in modules", typeScope, null, 0, + INVALID_MULTIPLICITY_ISSUE); + } } private void checkArity(EObject eObject, EReference reference, int expectedArity) { @@ -351,9 +355,9 @@ public class ProblemValidator extends AbstractProblemValidator { } private void checkExistsAssertion(Assertion assertion, LogicValue value) { - if (value == LogicValue.TRUE || value == LogicValue.UNKNOWN) { - // {@code true} is always a valid value for {@code exists}, while {@code unknown} values may always be - // refined to {@code true} if necessary (e.g., for individual nodes). + if (value == LogicValue.UNKNOWN) { + // {@code unknown} values may always be refined to {@code true} of {@code false} if necessary (e.g., for + // atom nodes or removed multi-objects). return; } var arguments = assertion.getArguments(); @@ -361,9 +365,16 @@ public class ProblemValidator extends AbstractProblemValidator { // We already report an error on invalid arity. return; } - var node = getNodeArgumentForMultiObjectAssertion(arguments.get(0)); - if (node != null && !node.eIsProxy() && ProblemUtil.isAtomNode(node)) { - acceptError("Individual nodes must exist.", assertion, null, 0, UNSUPPORTED_ASSERTION_ISSUE); + var node = getNodeArgumentForMultiObjectAssertion(arguments.getFirst()); + if (node == null || node.eIsProxy()) { + return; + } + if (ProblemUtil.isAtomNode(node) && value != LogicValue.TRUE) { + acceptError("Atom nodes must exist.", assertion, null, 0, UNSUPPORTED_ASSERTION_ISSUE); + } + if (ProblemUtil.isMultiNode(node) && value != LogicValue.FALSE && ProblemUtil.isInModule(node)) { + acceptError("Multi-objects in modules cannot be required to exist.", assertion, null, 0, + UNSUPPORTED_ASSERTION_ISSUE); } } @@ -403,4 +414,23 @@ public class ProblemValidator extends AbstractProblemValidator { } throw new IllegalArgumentException("Unknown assertion argument: " + argument); } + + @Check + private void checkImplicitNodeInModule(Assertion assertion) { + if (!ProblemUtil.isInModule(assertion)) { + return; + } + for (var argument : assertion.getArguments()) { + if (argument instanceof NodeAssertionArgument nodeAssertionArgument) { + var node = nodeAssertionArgument.getNode(); + if (node != null && !node.eIsProxy() && ProblemUtil.isImplicitNode(node)) { + var name = node.getName(); + var message = ("Implicit nodes are not allowed in modules. Explicitly declare '%s' as a node " + + "with the declaration 'declare %s.'").formatted(name, name); + acceptError(message, nodeAssertionArgument, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE, + 0, UNSUPPORTED_ASSERTION_ISSUE); + } + } + } + } } diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java index 82dea31b..1fb08845 100644 --- a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java @@ -82,7 +82,6 @@ class AssertionValidationTest { "exists(n).", "?exists(n).", "!exists(n).", - "exists(*).", "?exists(*).", "exists(Foo::new).", "?exists(Foo::new).", diff --git a/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java new file mode 100644 index 00000000..00ad051b --- /dev/null +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/ModuleValidationTest.java @@ -0,0 +1,145 @@ +/* + * SPDX-FileCopyrightText: 2024 The Refinery Authors + * + * SPDX-License-Identifier: EPL-2.0 + */ +package tools.refinery.language.tests.validation; + +import com.google.inject.Inject; +import org.eclipse.xtext.testing.InjectWith; +import org.eclipse.xtext.testing.extensions.InjectionExtension; +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.extension.ExtendWith; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.Arguments; +import org.junit.jupiter.params.provider.MethodSource; +import tools.refinery.language.model.tests.utils.ProblemParseHelper; +import tools.refinery.language.tests.ProblemInjectorProvider; +import tools.refinery.language.validation.ProblemValidator; + +import java.util.stream.Stream; + +import static org.hamcrest.MatcherAssert.assertThat; +import static org.hamcrest.Matchers.*; + +@ExtendWith(InjectionExtension.class) +@InjectWith(ProblemInjectorProvider.class) +class ModuleValidationTest { + @Inject + private ProblemParseHelper parseHelper; + + @ParameterizedTest + @MethodSource + void invalidMultiObjectExistsTest(String invalidDeclaration) { + var problem = parseHelper.parse(""" + module. + + %s + """.formatted(invalidDeclaration)); + var issues = problem.validate(); + assertThat(issues, hasItem(hasProperty("issueCode", + is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE)))); + } + + static Stream invalidMultiObjectExistsTest() { + return Stream.of( + Arguments.of(""" + class Foo. + exists(Foo::new). + """), + Arguments.of(""" + multi m. + exists(m). + """)); + } + + @Test + void invalidScopeTest() { + var problem = parseHelper.parse(""" + module. + + class Foo. + scope Foo += 1. + """); + var issues = problem.validate(); + assertThat(issues, hasItem(hasProperty("issueCode", + is(ProblemValidator.INVALID_MULTIPLICITY_ISSUE)))); + } + + @Test + void invalidAssertionArgumentTest() { + var problem = parseHelper.parse(""" + module. + + class Foo. + Foo(foo1). + """); + var issues = problem.validate(); + assertThat(issues, hasItem(allOf( + hasProperty("issueCode", is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE)), + hasProperty("message", containsString("foo1"))))); + } + + @ParameterizedTest + @MethodSource + void validDeclarationTest(String validDeclaration) { + var problem = parseHelper.parse(validDeclaration); + var issues = problem.validate(); + assertThat(issues, hasSize(0)); + } + + static Stream validDeclarationTest() { + return Stream.concat( + invalidMultiObjectExistsTest(), + Stream.of( + Arguments.of(""" + class Foo. + scope Foo += 1. + """), + Arguments.of(""" + module. + + class Foo. + scope Foo = 1. + """), + Arguments.of(""" + class Foo. + Foo(foo1). + """), + Arguments.of(""" + module. + + class Foo. + multi foo1. + Foo(foo1). + """), + Arguments.of(""" + module. + + class Foo. + atom foo1. + Foo(foo1). + """), + Arguments.of(""" + module. + + class Foo. + declare foo1. + Foo(foo1). + """), + Arguments.of(""" + module. + + enum Foo { foo1 } + Foo(foo1). + """), + Arguments.of(""" + module. + + class Foo. + Foo(Foo::new). + """) + ) + ); + } +} -- cgit v1.2.3-54-g00ecf