Type compatibility error message, when reading from .cfg (#2757)

* Manual type check * regression * test files * UL support * . * Update test/tla/Bug2750.cfg Co-authored-by: Thomas Pani <[email protected]> --------- Co-authored-by: Thomas Pani <[email protected]>
apalache-mc · Oct 17, 2023 · 16b040d · 16b040d
1 parent c877256
commit 16b040d
Show file tree

Hide file tree

Showing 8 changed files with 208 additions and 42 deletions.
diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/config/TlcConfig.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/config/TlcConfig.scala
@@ -1,9 +1,9 @@
 package at.forsyte.apalache.infra.tlc.config
 
 import at.forsyte.apalache.infra.tlc.config.ConfigModelValue.STR_PREFIX
-import at.forsyte.apalache.tla.lir.convenience.tla
-import at.forsyte.apalache.tla.lir.{BoolT1, IntT1, SetT1, StrT1, TlaEx, Typed, VarT1}
-import at.forsyte.apalache.tla.lir.TypedPredefs._
+import at.forsyte.apalache.tla.lir.{TlaType1, Typed, VarT1}
+import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
+import at.forsyte.apalache.tla.types.{tla, ModelValueHandler}
 
 import scala.util.parsing.input.NoPosition
 
@@ -46,7 +46,7 @@ sealed abstract class ConfigConstExpr {
    * @return
    *   the TLA IR expression that represents the parsed constant expression
    */
-  def toTlaEx: TlaEx
+  def toTla: TBuilderInstruction
 }
 
 object ConfigModelValue {
@@ -64,11 +64,11 @@ object ConfigModelValue {
  *   the name of a model value
  */
 case class ConfigModelValue(name: String) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = {
+  override def toTla: TBuilderInstruction = {
     // currently, we use the type Str for all model values.
     // In the future, we might want to distinguish between different uninterpreted types.
     // See https://github.com/informalsystems/apalache/issues/570
-    tla.str(STR_PREFIX + name).typed(StrT1)
+    tla.str(STR_PREFIX + name)
   }
 }
 
@@ -79,7 +79,7 @@ case class ConfigModelValue(name: String) extends ConfigConstExpr {
  *   an integer as BigInt
  */
 case class ConfigIntValue(num: BigInt) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = tla.bigInt(num).typed(IntT1)
+  override def toTla: TBuilderInstruction = tla.int(num)
 }
 
 /**
@@ -89,7 +89,7 @@ case class ConfigIntValue(num: BigInt) extends ConfigConstExpr {
  *   a boolean
  */
 case class ConfigBoolValue(b: Boolean) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = tla.bool(b).typed(BoolT1)
+  override def toTla: TBuilderInstruction = tla.bool(b)
 }
 
 /**
@@ -99,7 +99,13 @@ case class ConfigBoolValue(b: Boolean) extends ConfigConstExpr {
  *   a string
  */
 case class ConfigStrValue(str: String) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = tla.str(str).typed(StrT1)
+  override def toTla: TBuilderInstruction = {
+    ModelValueHandler.typeAndIndex(str) match {
+      case None                => tla.str(str)
+      case Some((constT, idx)) => tla.const(idx, constT)
+    }
+
+  }
 }
 
 /**
@@ -109,18 +115,18 @@ case class ConfigStrValue(str: String) extends ConfigConstExpr {
  *   the set elements, which are constant expression themselves.
  */
 case class ConfigSetValue(elems: ConfigConstExpr*) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = {
-    val setElems = elems.map(_.toTlaEx)
+  override def toTla: TBuilderInstruction = {
+    val setElems = elems.map(_.toTla)
     if (setElems.isEmpty) {
       // the element type is uknown, introduce a polymorphic type Set(a)
-      tla.enumSet().typed(SetT1(VarT1(0)))
+      tla.emptySet(VarT1(0))
     } else {
       // the element type should be unique
-      val headType = setElems.head.typeTag.asTlaType1()
+      val headType = TlaType1.fromTypeTag(setElems.head.typeTag)
       if (setElems.tail.exists(_.typeTag != Typed(headType))) {
         throw new TlcConfigParseError("Set elements have different types: " + setElems.mkString(", "), NoPosition)
       } else {
-        tla.enumSet(setElems: _*).typed(SetT1(headType))
+        tla.enumSet(setElems: _*)
       }
     }
   }

diff --git a/passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/ConfigurationPassImpl.scala b/passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/ConfigurationPassImpl.scala
@@ -19,6 +19,7 @@ import at.forsyte.apalache.infra.tlc.config.TlcConfig
 import at.forsyte.apalache.infra.tlc.config.InitNextSpec
 import at.forsyte.apalache.infra.tlc.config.TemporalSpec
 import at.forsyte.apalache.infra.tlc.config.NullSpec
+import at.forsyte.apalache.tla.typecheck.TypingInputException
 
 /**
  * The pass that collects the configuration parameters and overrides constants and definitions. This pass also
@@ -50,8 +51,33 @@ class ConfigurationPassImpl @Inject() (
       case Some((tlcConfig, tlcConfigFile)) => loadOptionsFromTlcConfig(tlaModule, tlcConfig, tlcConfigFile)
     }
 
-    val constOverrideNames = tlaModule.constDeclarations.map(_.name).map(ConstAndDefRewriter.OVERRIDE_PREFIX + _).toSet
-    val (constOverrides, otherOverrides) = overrides.partition(d => constOverrideNames.contains(d.name))
+    val constOverrideNamesAndTypes =
+      tlaModule.constDeclarations.map { decl =>
+        (ConstAndDefRewriter.OVERRIDE_PREFIX + decl.name) -> decl.typeTag
+      }.toMap
+
+    val (constOverrides, otherOverrides) = overrides.partition(d => constOverrideNamesAndTypes.contains(d.name))
+
+    // Typecheck
+    // Since config files are not typecheckable, blind override substitution can introduce type inconsistencies
+    // see #2750
+    // To circumvent this, we manually perform a type-consistency check, to verify that values overriding constants
+    // have the same type as the constant declaration
+    constOverrides.foreach { decl =>
+      val constDeclTag = constOverrideNamesAndTypes(decl.name)
+      val overrideTag = decl match {
+        case d: TlaOperDecl => d.body.typeTag
+        case _              => decl.typeTag
+      }
+
+      if (overrideTag != constDeclTag) {
+        throw new TypingInputException(
+            s"Constant ${decl.name.drop(ConstAndDefRewriter.OVERRIDE_PREFIX.length)} declared in the specification has the type tag $constDeclTag, while the value defined in the .cfg file has the type tag $overrideTag.\n" +
+              s"Please make sure the values in the .cfg file have types matching those in the specification, or use --cinit instead.",
+            decl.ID,
+        )
+      }
+    }
 
     val newDecls =
       if (constOverrides.nonEmpty) {

diff --git a/test/tla/Bug2750.cfg b/test/tla/Bug2750.cfg
@@ -0,0 +1,7 @@
+\* Add statements after this line.
+SPECIFICATION Spec
+CONSTANTS 
+    Producers = {p1,p2}
+    Consumers = {c1,c2}
+    BufCapacity = 1
+INVARIANT Inv
diff --git a/test/tla/Bug2750.tla b/test/tla/Bug2750.tla
@@ -0,0 +1,87 @@
+--------------------------- MODULE Bug2750 ---------------------------
+(***************************************************************************)
+(* Original problem and spec by Michel Charpentier                         *)
+(* http://www.cs.unh.edu/~charpov/programming-tlabuffer.html               *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences
+
+CONSTANTS 
+    \* @type: Set(PROC);
+    Producers,   (* the (nonempty) set of producers                       *)
+    \* @type: Set(PROC);
+    Consumers,   (* the (nonempty) set of consumers                       *)
+    \* @type: Int;
+    BufCapacity  (* the maximum number of messages in the bounded buffer  *)
+
+ASSUME Assumption ==
+       /\ Producers # {}                      (* at least one producer *)
+       /\ Consumers # {}                      (* at least one consumer *)
+       /\ Producers \intersect Consumers = {} (* no thread is both consumer and producer *)
+       /\ BufCapacity \in (Nat \ {0})         (* buffer capacity is at least 1 *)
+
+-----------------------------------------------------------------------------
+
+VARIABLES 
+    \* @type: Seq(PROC);
+    buffer, 
+    \* @type: Set(PROC);
+    waitP, 
+    \* @type: Set(PROC);
+    waitC
+
+(* define statement *)
+isfull(b) == Len(b) = BufCapacity
+isempty(b) == Len(b) = 0
+
+\* @type: << Seq(PROC), Set(PROC), Set(PROC) >>;
+vars == << buffer, waitP, waitC >>
+
+ProcSet == (Producers) \cup (Consumers)
+
+Init == (* Global variables *)
+        /\ buffer = << >>
+        /\ waitP = {}
+        /\ waitC = {}
+
+p(self) == /\ (self \notin waitP)
+           /\ IF isfull(buffer)
+                 THEN /\ IF self \in Producers
+                            THEN /\ waitP' = (waitP \union {self})
+                                 /\ waitC' = waitC
+                            ELSE /\ waitC' = (waitC \union {self})
+                                 /\ waitP' = waitP
+                      /\ UNCHANGED buffer
+                 ELSE /\ buffer' = Append(buffer, self)
+                      /\ IF waitC # {}
+                            THEN /\ \E t \in waitC:
+                                      waitC' = waitC \ {t}
+                            ELSE /\ TRUE
+                                 /\ waitC' = waitC
+                      /\ waitP' = waitP
+
+c(self) == /\ (self \notin waitC)
+           /\ IF isempty(buffer)
+                 THEN /\ IF self \in Producers
+                            THEN /\ waitP' = (waitP \union {self})
+                                 /\ waitC' = waitC
+                            ELSE /\ waitC' = (waitC \union {self})
+                                 /\ waitP' = waitP
+                      /\ UNCHANGED buffer
+                 ELSE /\ buffer' = Tail(buffer)
+                      /\ IF waitP # {}
+                            THEN /\ \E t \in waitP:
+                                      waitP' = waitP \ {t}
+                            ELSE /\ TRUE
+                                 /\ waitP' = waitP
+                      /\ waitC' = waitC
+
+Next == (\E self \in Producers: p(self))
+           \/ (\E self \in Consumers: c(self))
+
+Spec == Init /\ [][Next]_vars
+
+\* END TRANSLATION 
+
+Inv == ~(waitP = Producers /\ waitC = Consumers)
+
+=============================================================================
diff --git a/test/tla/Test2750.cfg b/test/tla/Test2750.cfg
@@ -0,0 +1,8 @@
+INIT
+Init
+NEXT
+Next
+INVARIANT
+Inv
+CONSTANT
+C = "1_OF_A"
diff --git a/test/tla/Test2750.tla b/test/tla/Test2750.tla
@@ -0,0 +1,19 @@
+----------------------- MODULE Test2750 -----------------------------
+VARIABLES
+    \* @type: A;
+    x
+
+CONSTANT
+    \* @type: A;
+    C
+
+
+Init ==
+    /\ x = C
+
+Next ==
+    UNCHANGED x
+
+Inv == TRUE
+
+===============================================================================
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
@@ -2316,6 +2316,22 @@ $ apalache-mc check --length=1 --cinit=CInit Bug2268.tla | sed 's/[IEW]@.*//'
 EXITCODE: OK
 ```
 
+### check Bug2750.tla
+
+```sh
+$ apalache-mc check --config=Bug2750.cfg Bug2750.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: ERROR (255)
+```
+
+### check Test2750.tla
+
+```sh
+$ apalache-mc check --config=Test2750.cfg Test2750.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: OK
+```
+
 ### check profiling
 
 Check that the profiler output is produced as explained in

diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/TlcConfigImporter.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/TlcConfigImporter.scala
@@ -1,10 +1,10 @@
 package at.forsyte.apalache.tla.pp
 
 import at.forsyte.apalache.infra.tlc.config._
-import at.forsyte.apalache.tla.lir.TypedPredefs._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.lir.convenience._
 import at.forsyte.apalache.tla.lir.transformations.TlaModuleTransformation
+import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
+import at.forsyte.apalache.tla.types.tla
 import com.typesafe.scalalogging.LazyLogging
 
 /**
@@ -17,28 +17,24 @@ import com.typesafe.scalalogging.LazyLogging
  *   Andrey Kuprianov
  */
 class TlcConfigImporter(config: TlcConfig) extends TlaModuleTransformation with LazyLogging {
-  private val boolOperT = OperT1(Seq(), BoolT1)
-
-  private def mkBoolName(name: String): TlaEx = {
-    tla.name(name).typed(BoolT1)
+  private def mkBoolName(name: String): TBuilderInstruction = {
+    tla.name(name, BoolT1)
   }
 
   override def apply(mod: TlaModule): TlaModule = {
 
     val assignments = config.constAssignments.map { case (param, value) =>
-      val valueEx = value.toTlaEx
-      val operT = OperT1(Seq(), valueEx.typeTag.asTlaType1())
-      tla.declOp(ConstAndDefRewriter.OVERRIDE_PREFIX + param, value.toTlaEx).as(operT)
+      val valueEx = value.toTla
+      tla.decl(ConstAndDefRewriter.OVERRIDE_PREFIX + param, valueEx)
     }
     val replacements = config.constReplacements.map { case (param, value) =>
       mod.declarations.find(_.name == value) match {
         case Some(d: TlaOperDecl) =>
           if (d.formalParams.isEmpty) {
-            val tt = d.typeTag.asTlaType1()
+            val tt = TlaType1.fromTypeTag(d.typeTag)
             assert(tt.isInstanceOf[OperT1])
-            val operT = tt.asInstanceOf[OperT1]
-            val application = tla.appOp(tla.name(value).typed(operT)).typed(operT.res)
-            tla.declOp(ConstAndDefRewriter.OVERRIDE_PREFIX + param, application).as(operT)
+            val application = tla.appOp(tla.name(value, tt))
+            tla.decl(ConstAndDefRewriter.OVERRIDE_PREFIX + param, application)
           } else {
             val nparams = d.formalParams.size
             throw new TLCConfigurationError(
@@ -47,42 +43,43 @@ class TlcConfigImporter(config: TlcConfig) extends TlaModuleTransformation with
 
         case Some(d) =>
           // This is a branch from the old untyped encoding. Does it make sense in the type encoding?
-          val tt = d.typeTag.asTlaType1()
-          tla.declOp(ConstAndDefRewriter.OVERRIDE_PREFIX + param, tla.name(value).typed(tt)).as(OperT1(Seq(), tt))
+          val tt = TlaType1.fromTypeTag(d.typeTag)
+          tla.decl(ConstAndDefRewriter.OVERRIDE_PREFIX + param, tla.name(value, tt))
 
         case None =>
           throw new TLCConfigurationError(s"Met a replacement $param <- $value, but $value is not found")
       }
     }
     val stateConstraints = config.stateConstraints.zipWithIndex.map { case (value, index) =>
-      tla.declOp(TlcConfigImporter.STATE_PREFIX + index, mkBoolName(value)).as(boolOperT)
+      tla.decl(TlcConfigImporter.STATE_PREFIX + index, mkBoolName(value))
     }
     val actionConstraints = config.actionConstraints.zipWithIndex.map { case (value, index) =>
-      tla.declOp(TlcConfigImporter.ACTION_PREFIX + index, mkBoolName(value)).as(boolOperT)
+      tla.decl(TlcConfigImporter.ACTION_PREFIX + index, mkBoolName(value))
     }
     val invariants = config.invariants.zipWithIndex.map { case (value, index) =>
-      tla.declOp(TlcConfigImporter.INVARIANT_PREFIX + index, mkBoolName(value)).as(boolOperT)
+      tla.decl(TlcConfigImporter.INVARIANT_PREFIX + index, mkBoolName(value))
     }
     val temporalProps = config.temporalProps.zipWithIndex.map { case (value, index) =>
-      tla.declOp(TlcConfigImporter.TEMPORAL_PREFIX + index, mkBoolName(value)).as(boolOperT)
+      tla.decl(TlcConfigImporter.TEMPORAL_PREFIX + index, mkBoolName(value))
     }
     val behaviorSpec = config.behaviorSpec match {
       case InitNextSpec(init, next) =>
         List(
-            tla.declOp(TlcConfigImporter.INIT, mkBoolName(init)).as(boolOperT),
-            tla.declOp(TlcConfigImporter.NEXT, mkBoolName(next)).as(boolOperT),
+            tla.decl(TlcConfigImporter.INIT, mkBoolName(init)),
+            tla.decl(TlcConfigImporter.NEXT, mkBoolName(next)),
         )
 
       case TemporalSpec(name) =>
-        List(tla.declOp(TlcConfigImporter.SPEC, mkBoolName(name)).as(boolOperT))
+        List(tla.decl(TlcConfigImporter.SPEC, mkBoolName(name)))
 
       case NullSpec() =>
         throw new TLCConfigurationError("Neither INIT and NEXT, nor SPECIFICATION found in the TLC configuration file")
     }
-    new TlaModule(mod.name,
-        mod.declarations
-          ++ assignments ++ replacements ++ stateConstraints ++ actionConstraints
-          ++ invariants ++ temporalProps ++ behaviorSpec)
+
+    val extendedDecls: Iterable[TlaDecl] =
+      (assignments ++ replacements ++ stateConstraints ++ actionConstraints ++ invariants ++ temporalProps ++ behaviorSpec)
+        .map(_.build)
+    TlaModule(mod.name, mod.declarations ++ extendedDecls)
   }
 }