diff options
2 files changed, 217 insertions, 8 deletions
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 00ae4531..8bda4b95 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 | |||
@@ -14,7 +14,9 @@ import org.eclipse.emf.ecore.EObject; | |||
14 | import org.eclipse.emf.ecore.EReference; | 14 | import org.eclipse.emf.ecore.EReference; |
15 | import org.eclipse.xtext.EcoreUtil2; | 15 | import org.eclipse.xtext.EcoreUtil2; |
16 | import org.eclipse.xtext.validation.Check; | 16 | import org.eclipse.xtext.validation.Check; |
17 | import org.jetbrains.annotations.Nullable; | ||
17 | import tools.refinery.language.model.problem.*; | 18 | import tools.refinery.language.model.problem.*; |
19 | import tools.refinery.language.utils.ProblemDesugarer; | ||
18 | import tools.refinery.language.utils.ProblemUtil; | 20 | import tools.refinery.language.utils.ProblemUtil; |
19 | 21 | ||
20 | import java.util.ArrayList; | 22 | import java.util.ArrayList; |
@@ -53,9 +55,16 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
53 | 55 | ||
54 | public static final String INVALID_TRANSITIVE_CLOSURE_ISSUE = ISSUE_PREFIX + "INVALID_TRANSITIVE_CLOSURE"; | 56 | public static final String INVALID_TRANSITIVE_CLOSURE_ISSUE = ISSUE_PREFIX + "INVALID_TRANSITIVE_CLOSURE"; |
55 | 57 | ||
58 | public static final String INVALID_VALUE_ISSUE = ISSUE_PREFIX + "INVALID_VALUE"; | ||
59 | |||
60 | public static final String UNSUPPORTED_ASSERTION_ISSUE = ISSUE_PREFIX + "UNSUPPORTED_ASSERTION"; | ||
61 | |||
56 | @Inject | 62 | @Inject |
57 | private ReferenceCounter referenceCounter; | 63 | private ReferenceCounter referenceCounter; |
58 | 64 | ||
65 | @Inject | ||
66 | private ProblemDesugarer desugarer; | ||
67 | |||
59 | @Check | 68 | @Check |
60 | public void checkSingletonVariable(VariableOrNodeExpr expr) { | 69 | public void checkSingletonVariable(VariableOrNodeExpr expr) { |
61 | var variableOrNode = expr.getVariableOrNode(); | 70 | var variableOrNode = expr.getVariableOrNode(); |
@@ -203,7 +212,7 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
203 | } | 212 | } |
204 | 213 | ||
205 | @Check | 214 | @Check |
206 | void checkContainerOpposite(ReferenceDeclaration referenceDeclaration) { | 215 | public void checkContainerOpposite(ReferenceDeclaration referenceDeclaration) { |
207 | var kind = referenceDeclaration.getKind(); | 216 | var kind = referenceDeclaration.getKind(); |
208 | var opposite = referenceDeclaration.getOpposite(); | 217 | var opposite = referenceDeclaration.getOpposite(); |
209 | if (opposite != null && opposite.eIsProxy()) { | 218 | if (opposite != null && opposite.eIsProxy()) { |
@@ -231,7 +240,7 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
231 | } | 240 | } |
232 | 241 | ||
233 | @Check | 242 | @Check |
234 | void checkSupertypes(ClassDeclaration classDeclaration) { | 243 | public void checkSupertypes(ClassDeclaration classDeclaration) { |
235 | var supertypes = classDeclaration.getSuperTypes(); | 244 | var supertypes = classDeclaration.getSuperTypes(); |
236 | int supertypeCount = supertypes.size(); | 245 | int supertypeCount = supertypes.size(); |
237 | for (int i = 0; i < supertypeCount; i++) { | 246 | for (int i = 0; i < supertypeCount; i++) { |
@@ -246,7 +255,7 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
246 | } | 255 | } |
247 | 256 | ||
248 | @Check | 257 | @Check |
249 | void checkReferenceType(ReferenceDeclaration referenceDeclaration) { | 258 | public void checkReferenceType(ReferenceDeclaration referenceDeclaration) { |
250 | if (referenceDeclaration.getKind() == ReferenceKind.REFERENCE && | 259 | if (referenceDeclaration.getKind() == ReferenceKind.REFERENCE && |
251 | !ProblemUtil.isContainerReference(referenceDeclaration)) { | 260 | !ProblemUtil.isContainerReference(referenceDeclaration)) { |
252 | checkArity(referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 1); | 261 | checkArity(referenceDeclaration, ProblemPackage.Literals.REFERENCE_DECLARATION__REFERENCE_TYPE, 1); |
@@ -264,12 +273,12 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
264 | } | 273 | } |
265 | 274 | ||
266 | @Check | 275 | @Check |
267 | void checkParameterType(Parameter parameter) { | 276 | public void checkParameterType(Parameter parameter) { |
268 | checkArity(parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 1); | 277 | checkArity(parameter, ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE, 1); |
269 | } | 278 | } |
270 | 279 | ||
271 | @Check | 280 | @Check |
272 | void checkAtom(Atom atom) { | 281 | public void checkAtom(Atom atom) { |
273 | int argumentCount = atom.getArguments().size(); | 282 | int argumentCount = atom.getArguments().size(); |
274 | checkArity(atom, ProblemPackage.Literals.ATOM__RELATION, argumentCount); | 283 | checkArity(atom, ProblemPackage.Literals.ATOM__RELATION, argumentCount); |
275 | if (atom.isTransitiveClosure() && argumentCount != 2) { | 284 | if (atom.isTransitiveClosure() && argumentCount != 2) { |
@@ -281,17 +290,21 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
281 | } | 290 | } |
282 | 291 | ||
283 | @Check | 292 | @Check |
284 | void checkAssertion(Assertion assertion) { | 293 | public void checkAssertion(Assertion assertion) { |
285 | int argumentCount = assertion.getArguments().size(); | 294 | int argumentCount = assertion.getArguments().size(); |
295 | if (!(assertion.getValue() instanceof LogicConstant)) { | ||
296 | var message = "Assertion value must be one of 'true', 'false', 'unknown', or 'error'."; | ||
297 | acceptError(message, assertion, ProblemPackage.Literals.ASSERTION__VALUE, 0, INVALID_VALUE_ISSUE); | ||
298 | } | ||
286 | checkArity(assertion, ProblemPackage.Literals.ASSERTION__RELATION, argumentCount); | 299 | checkArity(assertion, ProblemPackage.Literals.ASSERTION__RELATION, argumentCount); |
287 | } | 300 | } |
288 | 301 | ||
289 | @Check | 302 | @Check |
290 | void checkTypeScope(TypeScope typeScope) { | 303 | public void checkTypeScope(TypeScope typeScope) { |
291 | checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1); | 304 | checkArity(typeScope, ProblemPackage.Literals.TYPE_SCOPE__TARGET_TYPE, 1); |
292 | } | 305 | } |
293 | 306 | ||
294 | void checkArity(EObject eObject, EReference reference, int expectedArity) { | 307 | private void checkArity(EObject eObject, EReference reference, int expectedArity) { |
295 | var value = eObject.eGet(reference); | 308 | var value = eObject.eGet(reference); |
296 | if (!(value instanceof Relation relation) || relation.eIsProxy()) { | 309 | if (!(value instanceof Relation relation) || relation.eIsProxy()) { |
297 | // Feature does not point to a {@link Relation}, we are probably already emitting another error. | 310 | // Feature does not point to a {@link Relation}, we are probably already emitting another error. |
@@ -305,4 +318,89 @@ public class ProblemValidator extends AbstractProblemValidator { | |||
305 | .formatted(relation.getName(), expectedArity, arity); | 318 | .formatted(relation.getName(), expectedArity, arity); |
306 | acceptError(message, eObject, reference, 0, INVALID_ARITY_ISSUE); | 319 | acceptError(message, eObject, reference, 0, INVALID_ARITY_ISSUE); |
307 | } | 320 | } |
321 | |||
322 | @Check | ||
323 | public void checkMultiObjectAssertion(Assertion assertion) { | ||
324 | var builtinSymbolsOption = desugarer.getBuiltinSymbols(assertion); | ||
325 | if (builtinSymbolsOption.isEmpty()) { | ||
326 | return; | ||
327 | } | ||
328 | var builtinSymbols = builtinSymbolsOption.get(); | ||
329 | var relation = assertion.getRelation(); | ||
330 | boolean isExists = builtinSymbols.exists().equals(relation); | ||
331 | boolean isEquals = builtinSymbols.equals().equals(relation); | ||
332 | if ((!isExists && !isEquals) || !(assertion.getValue() instanceof LogicConstant logicConstant)) { | ||
333 | return; | ||
334 | } | ||
335 | var value = logicConstant.getLogicValue(); | ||
336 | if (assertion.isDefault()) { | ||
337 | acceptError("Default assertions for 'exists' and 'equals' are not supported.", assertion, | ||
338 | ProblemPackage.Literals.ASSERTION__DEFAULT, 0, UNSUPPORTED_ASSERTION_ISSUE); | ||
339 | return; | ||
340 | } | ||
341 | if (value == LogicValue.ERROR) { | ||
342 | acceptError("Error assertions for 'exists' and 'equals' are not supported.", assertion, | ||
343 | ProblemPackage.Literals.ASSERTION__DEFAULT, 0, UNSUPPORTED_ASSERTION_ISSUE); | ||
344 | return; | ||
345 | } | ||
346 | if (isExists) { | ||
347 | checkExistsAssertion(assertion, value); | ||
348 | return; | ||
349 | } | ||
350 | checkEqualsAssertion(assertion, value); | ||
351 | } | ||
352 | |||
353 | private void checkExistsAssertion(Assertion assertion, LogicValue value) { | ||
354 | if (value == LogicValue.TRUE || value == LogicValue.UNKNOWN) { | ||
355 | // {@code true} is always a valid value for {@code exists}, while {@code unknown} values may always be | ||
356 | // refined to {@code true} if necessary (e.g., for individual nodes). | ||
357 | return; | ||
358 | } | ||
359 | var arguments = assertion.getArguments(); | ||
360 | if (arguments.isEmpty()) { | ||
361 | // We already report an error on invalid arity. | ||
362 | return; | ||
363 | } | ||
364 | var node = getNodeArgumentForMultiObjectAssertion(arguments.get(0)); | ||
365 | if (node != null && !node.eIsProxy() && ProblemUtil.isIndividualNode(node)) { | ||
366 | acceptError("Individual nodes must exist.", assertion, null, 0, UNSUPPORTED_ASSERTION_ISSUE); | ||
367 | } | ||
368 | } | ||
369 | |||
370 | private void checkEqualsAssertion(Assertion assertion, LogicValue value) { | ||
371 | var arguments = assertion.getArguments(); | ||
372 | if (arguments.size() < 2) { | ||
373 | // We already report an error on invalid arity. | ||
374 | return; | ||
375 | } | ||
376 | var left = getNodeArgumentForMultiObjectAssertion(arguments.get(0)); | ||
377 | var right = getNodeArgumentForMultiObjectAssertion(arguments.get(1)); | ||
378 | if (left == null || left.eIsProxy() || right == null || right.eIsProxy()) { | ||
379 | return; | ||
380 | } | ||
381 | if (left.equals(right)) { | ||
382 | if (value == LogicValue.FALSE || value == LogicValue.ERROR) { | ||
383 | acceptError("A node cannot be necessarily unequal to itself.", assertion, null, 0, | ||
384 | UNSUPPORTED_ASSERTION_ISSUE); | ||
385 | } | ||
386 | } else { | ||
387 | if (value != LogicValue.FALSE) { | ||
388 | acceptError("Equalities between distinct nodes are not supported.", assertion, null, 0, | ||
389 | UNSUPPORTED_ASSERTION_ISSUE); | ||
390 | } | ||
391 | } | ||
392 | } | ||
393 | |||
394 | @Nullable | ||
395 | private Node getNodeArgumentForMultiObjectAssertion(AssertionArgument argument) { | ||
396 | if (argument instanceof WildcardAssertionArgument) { | ||
397 | acceptError("Wildcard arguments for 'exists' are not supported.", argument, null, 0, | ||
398 | UNSUPPORTED_ASSERTION_ISSUE); | ||
399 | return null; | ||
400 | } | ||
401 | if (argument instanceof NodeAssertionArgument nodeAssertionArgument) { | ||
402 | return nodeAssertionArgument.getNode(); | ||
403 | } | ||
404 | throw new IllegalArgumentException("Unknown assertion argument: " + argument); | ||
405 | } | ||
308 | } | 406 | } |
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 new file mode 100644 index 00000000..82dea31b --- /dev/null +++ b/subprojects/language/src/test/java/tools/refinery/language/tests/validation/AssertionValidationTest.java | |||
@@ -0,0 +1,111 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.language.tests.validation; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import org.eclipse.xtext.testing.InjectWith; | ||
10 | import org.eclipse.xtext.testing.extensions.InjectionExtension; | ||
11 | import org.junit.jupiter.api.Test; | ||
12 | import org.junit.jupiter.api.extension.ExtendWith; | ||
13 | import org.junit.jupiter.params.ParameterizedTest; | ||
14 | import org.junit.jupiter.params.provider.ValueSource; | ||
15 | import tools.refinery.language.model.tests.utils.ProblemParseHelper; | ||
16 | import tools.refinery.language.tests.ProblemInjectorProvider; | ||
17 | import tools.refinery.language.validation.ProblemValidator; | ||
18 | |||
19 | import static org.hamcrest.MatcherAssert.assertThat; | ||
20 | import static org.hamcrest.Matchers.*; | ||
21 | import static org.hamcrest.Matchers.is; | ||
22 | |||
23 | @ExtendWith(InjectionExtension.class) | ||
24 | @InjectWith(ProblemInjectorProvider.class) | ||
25 | class AssertionValidationTest { | ||
26 | @Inject | ||
27 | private ProblemParseHelper parseHelper; | ||
28 | |||
29 | @Test | ||
30 | void invalidValueTest() { | ||
31 | var problem = parseHelper.parse(""" | ||
32 | class Foo. | ||
33 | |||
34 | Foo(n): 5. | ||
35 | """); | ||
36 | var issues = problem.validate(); | ||
37 | assertThat(issues, hasItem(hasProperty("issueCode", | ||
38 | is(ProblemValidator.INVALID_VALUE_ISSUE)))); | ||
39 | } | ||
40 | |||
41 | @ParameterizedTest | ||
42 | @ValueSource(strings = { | ||
43 | "default exists(n).", | ||
44 | "!exists(A).", | ||
45 | "exists(A): error.", | ||
46 | "exists(n): error.", | ||
47 | "!exists(*).", | ||
48 | "exists(*): error.", | ||
49 | "default equals(n, n).", | ||
50 | "equals(n, m).", | ||
51 | "?equals(n, m).", | ||
52 | "equals(n, m): error.", | ||
53 | "equals(A, B).", | ||
54 | "?equals(A, B).", | ||
55 | "equals(A, B): error.", | ||
56 | "!equals(n, n).", | ||
57 | "equals(n, n): error.", | ||
58 | "!equals(A, A).", | ||
59 | "equals(A, A): error.", | ||
60 | "?equals(n, *).", | ||
61 | "?equals(*, m).", | ||
62 | "equals(*, *).", | ||
63 | "!equals(*, *).", | ||
64 | "?equals(*, *).", | ||
65 | "equals(*, *): error." | ||
66 | }) | ||
67 | void invalidMultiObjectTest(String assertion) { | ||
68 | var problem = parseHelper.parse(""" | ||
69 | enum Bar { A, B } | ||
70 | |||
71 | %s | ||
72 | """.formatted(assertion)); | ||
73 | var issues = problem.validate(); | ||
74 | assertThat(issues, hasItem(hasProperty("issueCode", | ||
75 | is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE)))); | ||
76 | } | ||
77 | |||
78 | @ParameterizedTest | ||
79 | @ValueSource(strings = { | ||
80 | "exists(A).", | ||
81 | "?exists(A).", | ||
82 | "exists(n).", | ||
83 | "?exists(n).", | ||
84 | "!exists(n).", | ||
85 | "exists(*).", | ||
86 | "?exists(*).", | ||
87 | "exists(Foo::new).", | ||
88 | "?exists(Foo::new).", | ||
89 | "!exists(Foo::new).", | ||
90 | "equals(A, A).", | ||
91 | "?equals(A, A).", | ||
92 | "!equals(A, B).", | ||
93 | "equals(n, n).", | ||
94 | "?equals(n, n).", | ||
95 | "!equals(n, m).", | ||
96 | "equals(Foo::new, Foo::new).", | ||
97 | "?equals(Foo::new, Foo::new)." | ||
98 | }) | ||
99 | void validMultiObjectTest(String assertion) { | ||
100 | var problem = parseHelper.parse(""" | ||
101 | class Foo. | ||
102 | |||
103 | enum Bar { A, B } | ||
104 | |||
105 | %s | ||
106 | """.formatted(assertion)); | ||
107 | var issues = problem.validate(); | ||
108 | assertThat(issues, not(hasItem(hasProperty("issueCode", | ||
109 | is(ProblemValidator.UNSUPPORTED_ASSERTION_ISSUE))))); | ||
110 | } | ||
111 | } | ||