Merge pull request #1802 from informalsystems/ro/infinite-sets-bug

Encode infinite sets in the arrays encoding
apalache-mc · Jun 22, 2022 · 4eca4b0 · 4eca4b0
2 parents 57268af + 46b902c
commit 4eca4b0
Show file tree

Hide file tree

Showing 4 changed files with 75 additions and 32 deletions.
diff --git a/.unreleased/bug-fixes/1802.md b/.unreleased/bug-fixes/1802.md
@@ -0,0 +1 @@
+Fix crash with infinite sets in the arrays encoding, see #1802
diff --git a/test/tla/InfDomFun.tla 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
@@ -2404,6 +2404,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

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
@@ -155,13 +155,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)
@@ -537,6 +543,9 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
           case CellTFrom(SetT1(elemType)) if encoding == arraysEncoding =>
             z3context.mkArraySort(getOrMkCellSort(CellTFrom(elemType)), z3context.getBoolSort)
 
+          case InfSetT(elemType) if encoding == arraysEncoding =>
+            z3context.mkArraySort(getOrMkCellSort(elemType), z3context.getBoolSort)
+
           case PowSetT(domType) if encoding == arraysEncoding =>
             z3context.mkArraySort(getOrMkCellSort(CellTFrom(domType)), z3context.getBoolSort)
 
@@ -560,6 +569,38 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
     }
   }
 
+  private def getOrMkCellDefaultValue(cellSort: Sort, isInfiniteSet: Boolean = false): ExprSort = {
+    val sig = "Cell_" + cellSort
+    val sort = cellDefaults.get(sig)
+    if (sort.isDefined) {
+      sort.get._1
+    } else {
+      // Explicitly annotate existential type of `newDefault`. Fixes "inferred existential type ..., which cannot be
+      // expressed by wildcards, should be enabled by making the implicit value scala.language.existentials visible."
+      val newDefault: Expr[_1] forSome { type _1 <: Sort } = cellSort match {
+        case _: BoolSort =>
+          z3context.mkFalse()
+
+        case _: IntSort =>
+          z3context.mkInt(0)
+
+        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)
+      }
+
+      cellDefaults += (sig -> (newDefault.asInstanceOf[ExprSort], level))
+      newDefault.asInstanceOf[ExprSort]
+    }
+  }
+
   private def mkCellElemSort(cellType: CellT): Sort = {
     cellType match {
       case CellTFrom(BoolT1) =>
@@ -585,31 +626,6 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
     }
   }
 
-  private def getOrMkCellDefaultValue(cellSort: Sort): ExprSort = {
-    val sig = "Cell_" + cellSort
-    val sort = cellDefaults.get(sig)
-    if (sort.isDefined) {
-      sort.get._1
-    } else {
-      // Explicitly annotate existential type of `newDefault`. Fixes "inferred existential type ..., which cannot be
-      // expressed by wildcards, should be enabled by making the implicit value scala.language.existentials visible."
-      val newDefault: Expr[_1] forSome { type _1 <: Sort } = cellSort match {
-        case _: BoolSort =>
-          z3context.mkFalse()
-        case _: IntSort =>
-          z3context.mkInt(0)
-        case arraySort: ArraySort[_, _] =>
-          z3context.mkConstArray(arraySort.getDomain, getOrMkCellDefaultValue(arraySort.getRange))
-        case _ =>
-          log(s"(declare-const $sig $cellSort)")
-          z3context.mkConst(sig, cellSort)
-      }
-
-      cellDefaults += (sig -> (newDefault.asInstanceOf[ExprSort], level))
-      newDefault.asInstanceOf[ExprSort]
-    }
-  }
-
   private def toExpr(ex: TlaEx): (ExprSort, Long) = {
     simplifier.simplifyShallow(ex) match {
       case NameEx(name) =>