From d1e9fea6194eccc1d65d69bb525e655d63903624 Mon Sep 17 00:00:00 2001 From: rodrigo7491 Date: Fri, 15 Apr 2022 12:47:53 +0200 Subject: [PATCH 1/6] fix infinite sets representation as arrays --- .../tla/bmcmt/smt/Z3SolverContext.scala | 34 ++++++++++++++----- 1 file changed, 25 insertions(+), 9 deletions(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala index 9943a2bd50..2f89c01ca6 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala @@ -148,13 +148,19 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { // If arrays are used, they are initialized here. if (cellSort.isInstanceOf[ArraySort[_, _]] && !cell.isUnconstrained) { - val arrayInitializer = constantArrayCache.get(cellSort) match { - case Some(emptySet) => - z3context.mkEq(const, emptySet._1) - case None => - constantArrayCache += (cellSort -> (const, level)) - z3context.mkEq(const, getOrMkCellDefaultValue(cellSort)) - } + val arrayInitializer = + if (cell.cellType.isInstanceOf[InfSetT]) { + // Infinite sets are not cached because they are not empty + z3context.mkEq(const, getOrMkCellDefaultValue(cellSort, isInfiniteSet = true)) + } else { + constantArrayCache.get(cellSort) match { + case Some(emptySet) => + z3context.mkEq(const, emptySet._1) + case None => + constantArrayCache += (cellSort -> (const, level)) + z3context.mkEq(const, getOrMkCellDefaultValue(cellSort)) + } + } log(s"(assert $arrayInitializer)") z3solver.add(arrayInitializer) @@ -522,6 +528,9 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { case FinSetT(elemType) if encoding == arraysEncoding => z3context.mkArraySort(getOrMkCellSort(elemType), z3context.getBoolSort) + case InfSetT(elemType) if encoding == arraysEncoding => + z3context.mkArraySort(getOrMkCellSort(elemType), z3context.getBoolSort) + case PowSetT(domType) if encoding == arraysEncoding => z3context.mkArraySort(getOrMkCellSort(domType), z3context.getBoolSort) @@ -541,7 +550,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { } } - private def getOrMkCellDefaultValue(cellSort: Sort): ExprSort = { + private def getOrMkCellDefaultValue(cellSort: Sort, isInfiniteSet: Boolean = false): ExprSort = { val sig = "Cell_" + cellSort val sort = cellDefaults.get(sig) if (sort.isDefined) { @@ -552,10 +561,17 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { val newDefault: Expr[_1] forSome { type _1 <: Sort } = cellSort match { case _: BoolSort => z3context.mkFalse() + case _: IntSort => z3context.mkInt(0) - case arraySort: ArraySort[_, _] => + + case arraySort: ArraySort[_, _] if isInfiniteSet => + // Infinite sets are not cached because they are not empty + return z3context.mkConstArray(arraySort.getDomain, z3context.mkTrue()).asInstanceOf[ExprSort] + + case arraySort: ArraySort[_, _] if !isInfiniteSet => z3context.mkConstArray(arraySort.getDomain, getOrMkCellDefaultValue(arraySort.getRange)) + case _ => log(s"(declare-const $sig $cellSort)") z3context.mkConst(sig, cellSort) From 3243856b9fb3acd41f2102a0841ba0aafddb5ac1 Mon Sep 17 00:00:00 2001 From: rodrigo7491 Date: Mon, 23 May 2022 09:41:30 +0200 Subject: [PATCH 2/6] add integration test --- test/tla/InfDomFun.tla | 16 ++++++++++++++++ test/tla/cli-integration-tests.md | 10 ++++++++++ 2 files changed, 26 insertions(+) create mode 100644 test/tla/InfDomFun.tla diff --git a/test/tla/InfDomFun.tla b/test/tla/InfDomFun.tla new file mode 100644 index 0000000000..fea026b5e7 --- /dev/null +++ b/test/tla/InfDomFun.tla @@ -0,0 +1,16 @@ +----------------------------- MODULE InfDomFun --------------------------- +\* A regression test for functions with infinite domain, see: +\* https://github.com/informalsystems/apalache/issues/1798 +EXTENDS Integers + +VARIABLES + \* @type: Int -> Int; + f + +Init == f = [[i \in Int |-> 0] EXCEPT ![0] = 42] + +Next == UNCHANGED f + +Inv == f[0 ]= 42 + +========================================================================== diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index 9f86d3d2c0..5c6d96c01f 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -2237,6 +2237,16 @@ $ apalache-mc check --features=rows --length=4 MC_LamportMutexTyped.tla | sed 's EXITCODE: OK ``` +### check InfDomFun (array-encoding) + +A regression test for functions with infinite domain. + +```sh +$ apalache-mc check --inv=Inv InfDomFun.tla | sed 's/[IEW]@.*//' +... +EXITCODE: ERROR (12) +``` + ## running the typecheck command ### typecheck Empty.tla reports no error From eb5d688f509689be10f000033dbfd4f3f9e89279 Mon Sep 17 00:00:00 2001 From: rodrigo7491 Date: Mon, 23 May 2022 10:22:23 +0200 Subject: [PATCH 3/6] update release notes --- UNRELEASED.md | 1 + 1 file changed, 1 insertion(+) diff --git a/UNRELEASED.md b/UNRELEASED.md index faa559879f..a3612e33bd 100644 --- a/UNRELEASED.md +++ b/UNRELEASED.md @@ -24,3 +24,4 @@ * Fix potential non-determinism when picking from `[S -> T]`, see #1753 * Fix the bug in uninterpreted types, see #1792 + * Fix usage of infinite sets in the arrays encoding, see #1802 From 139e4a699561defdba008c0d04508df661438855 Mon Sep 17 00:00:00 2001 From: rodrigo7491 Date: Tue, 21 Jun 2022 13:37:16 +0200 Subject: [PATCH 4/6] fix merge conflict --- .../tla/bmcmt/smt/Z3SolverContext.scala | 51 +++++++++---------- 1 file changed, 25 insertions(+), 26 deletions(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala index 07c72c15c4..e4bc59144b 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala @@ -570,32 +570,6 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { } private def getOrMkCellDefaultValue(cellSort: Sort, isInfiniteSet: Boolean = false): ExprSort = { - private def mkCellElemSort(cellType: CellT): Sort = { - cellType match { - case CellTFrom(BoolT1) => - z3context.getBoolSort - - case CellTFrom(IntT1) => - z3context.getIntSort - - case CellTFrom(SetT1(elemType)) if encoding == arraysEncoding => - mkCellElemSort(CellTFrom(elemType)) - - case PowSetT(domType) if encoding == arraysEncoding => - mkCellElemSort(CellTFrom(domType)) - - case FinFunSetT(argType, cdmType) if encoding == arraysEncoding => - mkCellElemSort(CellTFrom(FunT1(argType.toTlaType1, cdmType.toTlaType1))) - - case CellTFrom(FunT1(argType, resType)) if encoding == arraysEncoding => - z3context.mkArraySort(mkCellElemSort(CellTFrom(argType)), mkCellElemSort(CellTFrom(resType))) - - case _ => - z3context.mkUninterpretedSort("Cell_" + cellType.signature) - } - } - - private def getOrMkCellDefaultValue(cellSort: Sort): ExprSort = { val sig = "Cell_" + cellSort val sort = cellDefaults.get(sig) if (sort.isDefined) { @@ -627,6 +601,31 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext { } } + private def mkCellElemSort(cellType: CellT): Sort = { + cellType match { + case CellTFrom(BoolT1) => + z3context.getBoolSort + + case CellTFrom(IntT1) => + z3context.getIntSort + + case CellTFrom(SetT1(elemType)) if encoding == arraysEncoding => + mkCellElemSort(CellTFrom(elemType)) + + case PowSetT(domType) if encoding == arraysEncoding => + mkCellElemSort(CellTFrom(domType)) + + case FinFunSetT(argType, cdmType) if encoding == arraysEncoding => + mkCellElemSort(CellTFrom(FunT1(argType.toTlaType1, cdmType.toTlaType1))) + + case CellTFrom(FunT1(argType, resType)) if encoding == arraysEncoding => + z3context.mkArraySort(mkCellElemSort(CellTFrom(argType)), mkCellElemSort(CellTFrom(resType))) + + case _ => + z3context.mkUninterpretedSort("Cell_" + cellType.signature) + } + } + private def toExpr(ex: TlaEx): (ExprSort, Long) = { simplifier.simplifyShallow(ex) match { case NameEx(name) => From f0d42de03c1a7459d96748c621589b3618696fad Mon Sep 17 00:00:00 2001 From: rodrigo7491 Date: Tue, 21 Jun 2022 13:37:41 +0200 Subject: [PATCH 5/6] fix whitespace --- test/tla/InfDomFun.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/tla/InfDomFun.tla b/test/tla/InfDomFun.tla index fea026b5e7..385fb464fd 100644 --- a/test/tla/InfDomFun.tla +++ b/test/tla/InfDomFun.tla @@ -11,6 +11,6 @@ Init == f = [[i \in Int |-> 0] EXCEPT ![0] = 42] Next == UNCHANGED f -Inv == f[0 ]= 42 +Inv == f[0] = 42 ========================================================================== From 08eaaa526bc525abfacaf22d0b9a5829f55f3dc1 Mon Sep 17 00:00:00 2001 From: rodrigo7491 Date: Wed, 22 Jun 2022 09:34:12 +0200 Subject: [PATCH 6/6] update release notes --- .unreleased/bug-fixes/1802.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/1802.md diff --git a/.unreleased/bug-fixes/1802.md b/.unreleased/bug-fixes/1802.md new file mode 100644 index 0000000000..5d2126142a --- /dev/null +++ b/.unreleased/bug-fixes/1802.md @@ -0,0 +1 @@ +Fix crash with infinite sets in the arrays encoding, see #1802 \ No newline at end of file