From 16b040d405a1f80f679a955f628b426f204ec2c6 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Tue, 17 Oct 2023 13:06:37 +0200 Subject: [PATCH] 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 --------- Co-authored-by: Thomas Pani --- .../apalache/infra/tlc/config/TlcConfig.scala | 34 +++++--- .../tla/passes/pp/ConfigurationPassImpl.scala | 30 ++++++- test/tla/Bug2750.cfg | 7 ++ test/tla/Bug2750.tla | 87 +++++++++++++++++++ test/tla/Test2750.cfg | 8 ++ test/tla/Test2750.tla | 19 ++++ test/tla/cli-integration-tests.md | 16 ++++ .../apalache/tla/pp/TlcConfigImporter.scala | 49 +++++------ 8 files changed, 208 insertions(+), 42 deletions(-) create mode 100644 test/tla/Bug2750.cfg create mode 100644 test/tla/Bug2750.tla create mode 100644 test/tla/Test2750.cfg create mode 100644 test/tla/Test2750.tla 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 index a85fbcba70..22a7599f5f 100644 --- 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 index 4c0a8b268b..42faa998a8 100644 --- 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 new file mode 100644 index 0000000000..b6d90bd316 --- /dev/null +++ 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 new file mode 100644 index 0000000000..e84a77a96c --- /dev/null +++ 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) + +============================================================================= \ No newline at end of file diff --git a/test/tla/Test2750.cfg b/test/tla/Test2750.cfg new file mode 100644 index 0000000000..95230348a7 --- /dev/null +++ b/test/tla/Test2750.cfg @@ -0,0 +1,8 @@ +INIT +Init +NEXT +Next +INVARIANT +Inv +CONSTANT +C = "1_OF_A" \ No newline at end of file diff --git a/test/tla/Test2750.tla b/test/tla/Test2750.tla new file mode 100644 index 0000000000..bf2286e273 --- /dev/null +++ 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 index 9594be21b3..f2bf1aaff1 100644 --- 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 index fcf89a8c2c..e3521c3c84 100644 --- 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) } }