From 31273f9ffa9b5d7abe0109e46cda63fd850c91a3 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 28 Apr 2021 10:02:13 +0200 Subject: [PATCH 1/8] better messages in the type checker --- .../forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala index c60c6252e7..5bc923c7ef 100644 --- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala +++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala @@ -92,7 +92,7 @@ class EtcTypeChecker(varPool: TypeVarPool, inferPolytypes: Boolean = false) exte computeRec(ctx, solver, mkConst(ex.sourceRef, knownType)) } } else { - onTypeError(ex.sourceRef, s"Undefined name $name. Introduce a type annotation.") + onTypeError(ex.sourceRef, s"Found no annotation for $name. Did you write one?") throw new UnwindException } @@ -170,7 +170,7 @@ class EtcTypeChecker(varPool: TypeVarPool, inferPolytypes: Boolean = false) exte onTypeFound(name.sourceRef, nameType) computeRec(ctx, solver, mkApp(ex.sourceRef, Seq(nameType), args: _*)) } else { - onTypeError(ex.sourceRef, s"Undefined operator name $name. Introduce a type annotation.") + onTypeError(ex.sourceRef, s"It looks like the operator $name is used before it is defined. Is it true?") throw new UnwindException } From 3fcbfb89c2ca84cb7fe6e51e43eb4830b3f55559 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 28 Apr 2021 14:56:44 +0200 Subject: [PATCH 2/8] closes #758: fixed missing edges in the dependency graph --- .../standard/DeclarationSorter.scala | 53 ++++++++++++++++--- .../standard/TestDeclarationSorter.scala | 8 +++ 2 files changed, 54 insertions(+), 7 deletions(-) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/DeclarationSorter.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/DeclarationSorter.scala index cb8a351c67..f7920a05e7 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/DeclarationSorter.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/DeclarationSorter.scala @@ -1,10 +1,12 @@ package at.forsyte.apalache.tla.lir.transformations.standard -import at.forsyte.apalache.tla.lir.transformations.TlaModuleTransformation import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaOper +import at.forsyte.apalache.tla.lir.transformations.TlaModuleTransformation import at.forsyte.apalache.tla.lir.transformations.impl.StableTopologicalSort +import com.typesafe.scalalogging.LazyLogging +import java.io.{FileWriter, PrintWriter} import scala.collection.immutable.HashMap /** @@ -19,12 +21,13 @@ import scala.collection.immutable.HashMap * * @author Igor Konnov */ -class DeclarationSorter extends TlaModuleTransformation { +class DeclarationSorter extends TlaModuleTransformation with LazyLogging { type Edges = Map[UID, Set[UID]] + type MapIdToDecl = Map[UID, TlaDecl] override def apply(input: TlaModule): TlaModule = { // save the original order of the declarations - val idToDecl: Map[UID, TlaDecl] = input.declarations.foldLeft(Map.empty[UID, TlaDecl]) { case (map, d) => + val idToDecl: MapIdToDecl = input.declarations.foldLeft(Map.empty[UID, TlaDecl]) { case (map, d) => map + (d.ID -> d) } @@ -38,6 +41,8 @@ class DeclarationSorter extends TlaModuleTransformation { sorted.map(idToDecl) case Right(witnesses) => + val filename = explainCyclicDependency(idToDecl, depsGraph, witnesses) + logger.error(s"Check the dependency graph in $filename. You can view it with graphviz.") val opers = witnesses.map(idToDecl).map(_.name).mkString(", ") throw new CyclicDependencyError("Found a cyclic dependency among operators: " + opers) } @@ -45,6 +50,35 @@ class DeclarationSorter extends TlaModuleTransformation { new TlaModule(input.name, sortedDeclarations) } + // Dump the dependency graph to a dot file. Otherwise, it is very hard to see what is going on. + private def explainCyclicDependency(idToDecl: MapIdToDecl, depsGraph: Edges, witnesses: Set[UID]): String = { + val filename = "dependencies.dot" + + def getName(uid: UID): String = { + idToDecl.get(uid).map(_.name).getOrElse("undefined") + } + + def printToDot(writer: PrintWriter): Unit = { + writer.println("digraph dependencies {") + + for (fromId <- witnesses) { + writer.println(""" n%s[label="%s"];""".format(fromId, getName(fromId))) + for (toId <- depsGraph.getOrElse(fromId, Set.empty)) { + writer.println(""" n%s -> n%s;""".format(fromId, toId)) + } + } + writer.println("}") + } + + val writer = new PrintWriter(new FileWriter(filename, false)) + try { + printToDot(writer) + filename + } finally { + writer.close() + } + } + // For every declaration ID id1, compute the list of distinct ID of the declarations that must be defined before id1 private def computeDependenciesGraph(declarations: Seq[TlaDecl]): Edges = { // create a map from declaration names to their IDs @@ -86,10 +120,14 @@ class DeclarationSorter extends TlaModuleTransformation { // A singleton with the id, if the name is registered; otherwise, empty set. nameToId.get(name).fold(Set.empty[UID])(Set(_)) - case OperEx(TlaOper.apply, NameEx(name), _*) => + case OperEx(TlaOper.apply, NameEx(name), args @ _*) => // This may be an application of a user-defined operator. - // A singleton with the id, if the name is registered; otherwise, empty set. - nameToId.get(name).fold(Set.empty[UID])(Set(_)) + // A singleton with the id, if the name is registered + // (that is, for a top-level definition); otherwise, return the empty set (that is, for a LET-IN). + val base = nameToId.get(name).map(Set(_)).getOrElse(Set.empty) + args.foldLeft(base) { (u, arg) => + u ++ usesRec(arg) + } case OperEx(_, args @ _*) => // join the uses of the arguments @@ -98,7 +136,8 @@ class DeclarationSorter extends TlaModuleTransformation { } case LetInEx(body, decls @ _*) => - // join the uses of the body and the declarations + // Join the uses of the body and the declarations. + // We do not track dependencies between the LET-IN operators, because they are scoped and ordered. decls.foldLeft(usesRec(body)) { (u, d) => u ++ usesRec(d.body) } diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestDeclarationSorter.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestDeclarationSorter.scala index 0156ef13ca..e95b1eb283 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestDeclarationSorter.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestDeclarationSorter.scala @@ -44,6 +44,14 @@ class TestDeclarationSorter extends FunSuite with BeforeAndAfterEach { assertThrows[CyclicDependencyError](DeclarationSorter.instance(input)) } + test("regression: a cycle hidden via a call") { + val foo = tla.declOp("Foo", tla.int(1)) + val bar = tla.declOp("Bar", tla.appOp(tla.name("Foo"), tla.appOp(tla.name("Baz")))) + val baz = tla.declOp("Baz", tla.appOp(tla.name("Foo"), tla.appOp(tla.name("Bar")))) + val input = new TlaModule("test", List(foo, bar, baz)) + assertThrows[CyclicDependencyError](DeclarationSorter.instance(input)) + } + test("Foo uses VARIABLE x out of order") { val foo = tla.declOp("Foo", tla.name("x")) val x = TlaVarDecl("x") From b8d4ed95ff1ffb5fdd8766fa306dfe8a8c1066e2 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 28 Apr 2021 14:57:40 +0200 Subject: [PATCH 3/8] entry in unreleased --- UNRELEASED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/UNRELEASED.md b/UNRELEASED.md index 332c65c35a..633f5d9887 100644 --- a/UNRELEASED.md +++ b/UNRELEASED.md @@ -23,6 +23,7 @@ * Parser: supporting annotations in multiline comments, see #718 * Parser: supporting TLA+ identifiers in annotations, see #768 * Parser: better parser for annotations, see #757 +* Parser: fixed a bug in the declaration sorter, see #758 * The command `config --enable-stats=true` creates `$HOME/.tlaplus` if needed, see #762 ### Changes From b49f1d42c6d588ee80624e2f200d51daeace193e Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 28 Apr 2021 15:25:22 +0200 Subject: [PATCH 4/8] closes #645: fixed a false cycle that, caused by a parameter having the same name as an operator --- .../standard/DeclarationSorter.scala | 17 +++++++++++------ .../standard/TestDeclarationSorter.scala | 14 ++++++++++++++ 2 files changed, 25 insertions(+), 6 deletions(-) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/DeclarationSorter.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/DeclarationSorter.scala index f7920a05e7..4634ffbe2c 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/DeclarationSorter.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/DeclarationSorter.scala @@ -64,7 +64,9 @@ class DeclarationSorter extends TlaModuleTransformation with LazyLogging { for (fromId <- witnesses) { writer.println(""" n%s[label="%s"];""".format(fromId, getName(fromId))) for (toId <- depsGraph.getOrElse(fromId, Set.empty)) { - writer.println(""" n%s -> n%s;""".format(fromId, toId)) + if (witnesses.contains(toId)) { + writer.println(""" n%s -> n%s;""".format(fromId, toId)) + } } } writer.println("}") @@ -90,7 +92,6 @@ class DeclarationSorter extends TlaModuleTransformation with LazyLogging { map + (defId -> (map(defId) ++ uses)) } - val findUses = findExprUses(nameToId) // create a map that contains the list of used-by IDs for every declaration, excluding the declaration itself val initMap = Map(declarations.map { d => d.ID -> Set.empty[UID] }: _*) declarations.foldLeft(initMap) { @@ -101,11 +102,13 @@ class DeclarationSorter extends TlaModuleTransformation with LazyLogging { map + (d.ID -> Set.empty[UID]) case (map, d @ TlaAssumeDecl(body)) => - val uses = (findUses(body) - d.ID) + val uses = findExprUses(nameToId)(body) - d.ID updateDependencies(map, d.ID, uses) - case (map, d @ TlaOperDecl(_, _, body)) => - val uses = (findUses(body) - d.ID) + case (map, d @ TlaOperDecl(_, params, body)) => + // the operator parameters may shadow the name of top-level operator, so we have to exclude parameter names + val nameToIdWithoutParams = nameToId -- params.map(_.name) + val uses = findExprUses(nameToIdWithoutParams)(body) - d.ID updateDependencies(map, d.ID, uses) case (map, _) => map @@ -139,7 +142,9 @@ class DeclarationSorter extends TlaModuleTransformation with LazyLogging { // Join the uses of the body and the declarations. // We do not track dependencies between the LET-IN operators, because they are scoped and ordered. decls.foldLeft(usesRec(body)) { (u, d) => - u ++ usesRec(d.body) + // the operator parameters may shadow the name of top-level operator, so we have to exclude parameter names + val nameToIdWithoutParams = nameToId -- d.formalParams.map(_.name) + u ++ findExprUses(nameToIdWithoutParams)(d.body) } case _ => diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestDeclarationSorter.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestDeclarationSorter.scala index e95b1eb283..fda2bb84f4 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestDeclarationSorter.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/transformations/standard/TestDeclarationSorter.scala @@ -45,6 +45,7 @@ class TestDeclarationSorter extends FunSuite with BeforeAndAfterEach { } test("regression: a cycle hidden via a call") { + // regression for #758 val foo = tla.declOp("Foo", tla.int(1)) val bar = tla.declOp("Bar", tla.appOp(tla.name("Foo"), tla.appOp(tla.name("Baz")))) val baz = tla.declOp("Baz", tla.appOp(tla.name("Foo"), tla.appOp(tla.name("Bar")))) @@ -52,6 +53,19 @@ class TestDeclarationSorter extends FunSuite with BeforeAndAfterEach { assertThrows[CyclicDependencyError](DeclarationSorter.instance(input)) } + test("regression: a false cycle") { + // regression for #645 + + // The following two declarations do not form a cycle, as Foo uses it's parameter 'pid', not calling the operator 'pid'. + // Foo(pid) == 1 + val foo = tla.declOp("Foo", tla.name("pid"), OperParam("pid")) + // pid == Foo(2) + val pid = tla.declOp("pid", tla.appOp(tla.name("Foo"), tla.int(2))) + val input = new TlaModule("test", List(foo, pid)) + val expected = new TlaModule("test", List(foo, pid)) + assert(expected == DeclarationSorter.instance(input)) + } + test("Foo uses VARIABLE x out of order") { val foo = tla.declOp("Foo", tla.name("x")) val x = TlaVarDecl("x") From 1e0ef3c2d09eac3c7ea808574d708fbbf1b77081 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 28 Apr 2021 15:25:56 +0200 Subject: [PATCH 5/8] entry in UNRELEASED --- UNRELEASED.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/UNRELEASED.md b/UNRELEASED.md index 633f5d9887..c11a4339f2 100644 --- a/UNRELEASED.md +++ b/UNRELEASED.md @@ -23,7 +23,7 @@ * Parser: supporting annotations in multiline comments, see #718 * Parser: supporting TLA+ identifiers in annotations, see #768 * Parser: better parser for annotations, see #757 -* Parser: fixed a bug in the declaration sorter, see #758 +* Parser: fixed two bugs in the declaration sorter, see #645 and #758 * The command `config --enable-stats=true` creates `$HOME/.tlaplus` if needed, see #762 ### Changes From 8a8d55496c7e6f1909a1f2770aa90a05e7bb39b0 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 28 Apr 2021 18:28:44 +0200 Subject: [PATCH 6/8] Update tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala Co-authored-by: Shon Feder --- .../at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala index 5bc923c7ef..a4fb21adc1 100644 --- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala +++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala @@ -170,7 +170,7 @@ class EtcTypeChecker(varPool: TypeVarPool, inferPolytypes: Boolean = false) exte onTypeFound(name.sourceRef, nameType) computeRec(ctx, solver, mkApp(ex.sourceRef, Seq(nameType), args: _*)) } else { - onTypeError(ex.sourceRef, s"It looks like the operator $name is used before it is defined. Is it true?") + onTypeError(ex.sourceRef, s"The operator $name is used before it is defined.") throw new UnwindException } From a8fea817536fd5945fcf712024f0f8cf4002482c Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 28 Apr 2021 18:31:34 +0200 Subject: [PATCH 7/8] Update tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala Co-authored-by: Shon Feder --- .../at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala index a4fb21adc1..3bf433d50f 100644 --- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala +++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala @@ -92,7 +92,7 @@ class EtcTypeChecker(varPool: TypeVarPool, inferPolytypes: Boolean = false) exte computeRec(ctx, solver, mkConst(ex.sourceRef, knownType)) } } else { - onTypeError(ex.sourceRef, s"Found no annotation for $name. Did you write one?") + onTypeError(ex.sourceRef, s"No annotation found for $name.") throw new UnwindException } From 2b7054662798a798a1b16876a670d147e4380ee5 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Wed, 28 Apr 2021 18:36:00 +0200 Subject: [PATCH 8/8] fixed the error message --- .../at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala index 3bf433d50f..5d28f5ed8a 100644 --- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala +++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/EtcTypeChecker.scala @@ -92,7 +92,7 @@ class EtcTypeChecker(varPool: TypeVarPool, inferPolytypes: Boolean = false) exte computeRec(ctx, solver, mkConst(ex.sourceRef, knownType)) } } else { - onTypeError(ex.sourceRef, s"No annotation found for $name.") + onTypeError(ex.sourceRef, s"No annotation found for $name. Make sure that you've put one in front of $name.") throw new UnwindException }