From e63534412e88096d453db65b0bb8ad671dbc82ca Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe <bugs.eclipse.org@lemmster.de> Date: Tue, 25 Jul 2017 13:58:40 +0200 Subject: [PATCH] Disable unlikely level-checking bug in test suite. Warn users if it's likely they are affected by the bug (in which case they need to simplify the incorrectly flagged expression. [Bug][TLC] --- tlatools/src/tla2sany/semantic/LevelNode.java | 22 ++++++++ tlatools/src/tlc2/output/MP.java | 9 +++- tlatools/src/tlc2/tool/Spec.java | 12 ++++- tlatools/test-model/suite/test52.cfg | 5 +- tlatools/test-model/test52.cfg | 5 +- tlatools/test-model/testinvalidinvariant.cfg | 3 ++ tlatools/test-model/testinvalidinvariant.tla | 12 +++++ .../tlc2/tool/suite/TestInvalidInvariant.java | 52 +++++++++++++++++++ 8 files changed, 116 insertions(+), 4 deletions(-) create mode 100644 tlatools/test-model/testinvalidinvariant.cfg create mode 100644 tlatools/test-model/testinvalidinvariant.tla create mode 100644 tlatools/test/tlc2/tool/suite/TestInvalidInvariant.java diff --git a/tlatools/src/tla2sany/semantic/LevelNode.java b/tlatools/src/tla2sany/semantic/LevelNode.java index 5e6caf692..986dfbbde 100644 --- a/tlatools/src/tla2sany/semantic/LevelNode.java +++ b/tlatools/src/tla2sany/semantic/LevelNode.java @@ -607,6 +607,28 @@ public int levelChecked = 0 ; // (* any reasonable case where this will disallow a level-correct expression *) // (* that a user is likely to write. *) // (* *) +// (* The decision to simplify the bookkeeping results in the following, *) +// (* somewhat less unlikely problem. With the definitions *) +// (* *) +// (* ApplyToPrime(Op(_)) == Op(x') *) +// (* EqualsNoPrime(a) == x *) +// (* *) +// (* the expression ApplyToPrime(EqualsNoPrime)' , which equals x', is *) +// (* considered to be illegal. This is because the algorithm to compute the *) +// (* level makes the assumption that ApplyToPrime will always be applied to *) +// (* operators Op for which the level of Op(exp) depends on the level of *) +// (* exp. Hence, SANY's algorithm gives ApplyToPrime(Op) a level of at *) +// (* least 2 (primed expression) for any operator Op. A slightly more *) +// (* realistic example can be constructed by modifying ApplyToPrime a bit *) +// (* and applying it to ENABLED. *) +// (* TLC warns users about this bug if it reports an invariant to be *) +// (* level-incorrect in tlc2.tool.Spec.processConfigInvariants() with error *) +// (* code tlc2.output.EC.TLC_INVARIANT_VIOLATED_LEVEL. *) +// (* A corresponding test can be found in test52. Its invariant "Invariant" *) +// (* covers the ENABLED scenario. However, the invariant remains disabled *) +// (* for as long as this bug is open. The invariant Invariant can be *) +// (* re-enabled in test52.cfg once this bug is closed. *) +// (* *) // (* To compute the values of op.level, op.weights, and op.minMaxLevel for *) // (* an OpDefNode op corresponding to a definition, a level-checking *) // (* algorithm needs to keep track of the constraints on its formal *) diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java index c3b9c369c..f4af88037 100644 --- a/tlatools/src/tlc2/output/MP.java +++ b/tlatools/src/tlc2/output/MP.java @@ -363,7 +363,12 @@ public class MP b.append("Invariant %1% is violated."); break; case EC.TLC_INVARIANT_VIOLATED_LEVEL: - b.append("The invariant %1% is not a state predicate (one with no primes or temporal operators)."); + b.append("The invariant %1% is not a state predicate (one with no primes or temporal operators)."); + if (parameters.length > 1) { + b.append("\nNote that a bug can cause TLC to incorrectly report this error.\n" + + "If you believe your TLA+ or PlusCal specification to be correct,\n" + + "please check if this bug described in LevelNode.java starting at line 590ff affects you."); + } break; case EC.TLC_INVARIANT_EVALUATION_FAILED: @@ -1124,6 +1129,7 @@ public class MP */ public static String getError(int errorCode, String[] parameters) { + recorder.record(errorCode, parameters); return getMessage(ERROR, errorCode, parameters); } @@ -1154,6 +1160,7 @@ public class MP */ public static String getMessage(int errorCode, String[] parameters) { + recorder.record(errorCode, parameters); return getMessage(NONE, errorCode, parameters); } diff --git a/tlatools/src/tlc2/tool/Spec.java b/tlatools/src/tlc2/tool/Spec.java index 3c402b8a8..81bed024e 100644 --- a/tlatools/src/tlc2/tool/Spec.java +++ b/tlatools/src/tlc2/tool/Spec.java @@ -952,9 +952,19 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable { Assert.fail(EC.TLC_CONFIG_ID_REQUIRES_NO_ARG, new String[] { "invariant", name }); } + // MK 07/25/2017: Check if the invariant is a valid state predicate and produce + // a meaningful warning otherwise. With this enhancement, a rare bug in TLC's + // level-checking surfaced for which we don't have a fix right now. Fortunately, + // the bug is rather unlikely which is why TLC simply produces a warning for now + // if it "thinks" a user might be affected by the bug. + // see LevelNode.java line 590ff, Test52, TestInvalidInvariant, and related files + // for more context. if (def.getLevel() >= 2) { - Assert.fail(EC.TLC_INVARIANT_VIOLATED_LEVEL, new String[] { def.getName().toString() }); + if (!def.getBody().levelParams.isEmpty()) { + Assert.fail(EC.TLC_INVARIANT_VIOLATED_LEVEL, new String[] { def.getName().toString(), "includeWarning" }); + } + Assert.fail(EC.TLC_INVARIANT_VIOLATED_LEVEL, def.getName().toString()); } this.invNameVec.addElement(name); this.invVec.addElement(new Action(def.getBody(), Context.Empty)); diff --git a/tlatools/test-model/suite/test52.cfg b/tlatools/test-model/suite/test52.cfg index f0e860231..8990f16d4 100644 --- a/tlatools/test-model/suite/test52.cfg +++ b/tlatools/test-model/suite/test52.cfg @@ -1,3 +1,6 @@ SPECIFICATION Spec PROPERTY Property -INVARIANT Invariant +\* The Invariant is commented because of a known bug in TLC. +\* If this bug is ever addressed, Invariant can be re-enabled +\* and the test test52enabled be deleted. +\*INVARIANT Invariant diff --git a/tlatools/test-model/test52.cfg b/tlatools/test-model/test52.cfg index f0e860231..8990f16d4 100644 --- a/tlatools/test-model/test52.cfg +++ b/tlatools/test-model/test52.cfg @@ -1,3 +1,6 @@ SPECIFICATION Spec PROPERTY Property -INVARIANT Invariant +\* The Invariant is commented because of a known bug in TLC. +\* If this bug is ever addressed, Invariant can be re-enabled +\* and the test test52enabled be deleted. +\*INVARIANT Invariant diff --git a/tlatools/test-model/testinvalidinvariant.cfg b/tlatools/test-model/testinvalidinvariant.cfg new file mode 100644 index 000000000..f0e860231 --- /dev/null +++ b/tlatools/test-model/testinvalidinvariant.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +PROPERTY Property +INVARIANT Invariant diff --git a/tlatools/test-model/testinvalidinvariant.tla b/tlatools/test-model/testinvalidinvariant.tla new file mode 100644 index 000000000..e00c9bd91 --- /dev/null +++ b/tlatools/test-model/testinvalidinvariant.tla @@ -0,0 +1,12 @@ +------------------ MODULE testinvalidinvariant -------------------- +EXTENDS Integers + +VARIABLES x +Init == /\ x = 1 +Next == /\ x'= x + 1 +Spec == Init /\ [][Next]_<<x>> + +\* Primed variable is invalid. +Invariant == x' \in Nat + +================================================================== diff --git a/tlatools/test/tlc2/tool/suite/TestInvalidInvariant.java b/tlatools/test/tlc2/tool/suite/TestInvalidInvariant.java new file mode 100644 index 000000000..1e7f5b1d3 --- /dev/null +++ b/tlatools/test/tlc2/tool/suite/TestInvalidInvariant.java @@ -0,0 +1,52 @@ +/******************************************************************************* + * Copyright (c) 2017 Microsoft Research. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Markus Alexander Kuppe - initial API and implementation + ******************************************************************************/ +package tlc2.tool.suite; + +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertTrue; + +import org.junit.Test; + +import tlc2.output.EC; +import tlc2.tool.liveness.ModelCheckerTestCase; + +public class TestInvalidInvariant extends ModelCheckerTestCase { + + public TestInvalidInvariant() { + super("testinvalidinvariant"); + } + + @Test + public void testSpec() { + assertTrue(recorder.recorded(EC.TLC_FINISHED)); + assertTrue(recorder.recordedWithStringValue(EC.TLC_INVARIANT_VIOLATED_LEVEL, "Invariant")); + assertTrue(recorder.recordedWithSubStringValue(EC.GENERAL, + "The invariant Invariant is not a state predicate (one with no primes or temporal operators).")); + // See LevelNode.java line 590ff and tlc2.tool.Spec.processConfigInvariants(). + assertFalse(recorder.recordedWithSubStringValue(EC.GENERAL, + "Note that a bug can cause TLC to incorrectly report this error.")); + } +} -- GitLab