search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
441 stars 40 forks source link

Crash with `funArrays` encoding #2810

Closed nano-o closed 9 months ago

nano-o commented 9 months ago

Description

Apalache crashes with funArrays encoding when there is a variable whose type is a function whose image is a set of integers.

Impact

Low impact, can use oopsla19 encoding instead.

Input specification

--------------- MODULE TestApalache -----------------

EXTENDS Integers

P == {"P1_OF_P"}

VARIABLE
    \* @type: P -> Set(Int);
    myVariable

Init ==
    myVariable = [p \in P |-> {0}]

Step(p) ==
    myVariable' = [q \in P |-> {0}]

Next == \E p \in P : Step(p)

TypeOkay == myVariable \in [P -> SUBSET Int]
TypeOkay_ == TypeOkay

=============================================

The command line parameters used to run the tool

--smt-encoding=funArrays --tuning-options=search.invariant.mode=after:search.invariantFilter=1->.* --init=TypeOkay_ --inv=TypeOkay --length=1

Expected behavior

Apalache verifies TypeOkay is inductive.

Log files

``` 2024-01-20T21:19:06,984 [main] INFO a.f.a.t.Tool\$ - # APALACHE version: 0.44.2 | build: v0.44.2 2024-01-20T21:19:06,996 [main] INFO a.f.a.t.t.o.CheckCmd - Tuning: search.outputTraces=false:search.invariant.mode=after:search.invariantFilter=1->.* 2024-01-20T21:19:07,099 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser 2024-01-20T21:19:07,213 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser [OK] 2024-01-20T21:19:07,213 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat 2024-01-20T21:19:07,214 [main] INFO a.f.a.t.p.t.EtcTypeCheckerPassImpl - > Running Snowcat .::. 2024-01-20T21:19:07,280 [main] INFO a.f.a.t.p.t.EtcTypeCheckerPassImpl - > Your types are purrfect! 2024-01-20T21:19:07,280 [main] INFO a.f.a.t.p.t.EtcTypeCheckerPassImpl - > All expressions are typed 2024-01-20T21:19:07,280 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat [OK] 2024-01-20T21:19:07,280 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass 2024-01-20T21:19:07,282 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the initialization predicate to TypeOkay_ 2024-01-20T21:19:07,282 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the transition predicate to Next 2024-01-20T21:19:07,282 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set an invariant to TypeOkay 2024-01-20T21:19:07,284 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass [OK] 2024-01-20T21:19:07,284 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass 2024-01-20T21:19:07,284 [main] INFO a.f.a.t.p.p.DesugarerPassImpl - > Desugaring... 2024-01-20T21:19:07,289 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass [OK] 2024-01-20T21:19:07,289 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass 2024-01-20T21:19:07,289 [main] INFO a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Next, TypeOkay, TypeOkay_, TypeOkay_Primed 2024-01-20T21:19:07,298 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass [OK] 2024-01-20T21:19:07,298 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass 2024-01-20T21:19:07,299 [main] INFO a.f.a.t.p.p.TemporalPassImpl - > Rewriting temporal operators... 2024-01-20T21:19:07,299 [main] INFO a.f.a.t.p.p.TemporalPassImpl - > No temporal property specified, nothing to encode 2024-01-20T21:19:07,299 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass [OK] 2024-01-20T21:19:07,299 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass 2024-01-20T21:19:07,299 [main] INFO a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Next, TypeOkay, TypeOkay_, TypeOkay_Primed 2024-01-20T21:19:07,300 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass [OK] 2024-01-20T21:19:07,300 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass 2024-01-20T21:19:07,301 [main] INFO a.f.a.t.p.a.PrimingPassImpl - > Introducing TypeOkay_Primed for TypeOkay_' 2024-01-20T21:19:07,397 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass [OK] 2024-01-20T21:19:07,398 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen 2024-01-20T21:19:07,398 [main] INFO a.f.a.t.b.p.VCGenPassImpl - > Producing verification conditions from the invariant TypeOkay 2024-01-20T21:19:07,400 [main] INFO a.f.a.t.b.VCGenerator - > VCGen produced 1 verification condition(s) 2024-01-20T21:19:07,401 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen [OK] 2024-01-20T21:19:07,402 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass 2024-01-20T21:19:07,402 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Before preprocessing: unique renaming 2024-01-20T21:19:07,405 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Applying standard transformations: 2024-01-20T21:19:07,405 [main] INFO a.f.a.t.p.p.PreproPassImpl - > PrimePropagation 2024-01-20T21:19:07,406 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Desugarer 2024-01-20T21:19:07,406 [main] INFO a.f.a.t.p.p.PreproPassImpl - > UniqueRenamer 2024-01-20T21:19:07,407 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Normalizer 2024-01-20T21:19:07,408 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Keramelizer 2024-01-20T21:19:07,410 [main] INFO a.f.a.t.p.p.PreproPassImpl - > After preprocessing: UniqueRenamer 2024-01-20T21:19:07,412 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass [OK] 2024-01-20T21:19:07,412 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass 2024-01-20T21:19:07,418 [main] INFO a.f.a.t.p.a.TransitionPassImpl - > Found 1 initializing transitions 2024-01-20T21:19:07,418 [main] INFO a.f.a.t.p.a.TransitionPassImpl - > Found 1 transitions 2024-01-20T21:19:07,418 [main] INFO a.f.a.t.p.a.TransitionPassImpl - > No constant initializer 2024-01-20T21:19:07,419 [main] INFO a.f.a.t.p.a.TransitionPassImpl - > Applying unique renaming 2024-01-20T21:19:07,420 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass [OK] 2024-01-20T21:19:07,420 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass 2024-01-20T21:19:07,423 [main] INFO a.f.a.t.p.p.OptPassImpl - > Applying optimizations: 2024-01-20T21:19:07,423 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier 2024-01-20T21:19:07,424 [main] INFO a.f.a.t.p.p.OptPassImpl - > ExprOptimizer 2024-01-20T21:19:07,425 [main] INFO a.f.a.t.p.p.OptPassImpl - > SetMembershipSimplifier 2024-01-20T21:19:07,426 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier 2024-01-20T21:19:07,426 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass [OK] 2024-01-20T21:19:07,426 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass 2024-01-20T21:19:07,428 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Marking skolemizable existentials and sets to be expanded... 2024-01-20T21:19:07,428 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Skolemization 2024-01-20T21:19:07,428 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Expansion 2024-01-20T21:19:07,429 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Remove unused let-in defs 2024-01-20T21:19:07,429 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Running analyzers... 2024-01-20T21:19:07,430 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Introduced expression grades 2024-01-20T21:19:07,430 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass [OK] 2024-01-20T21:19:07,431 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #13: BoundedChecker 2024-01-20T21:19:07,436 [main] DEBUG a.f.a.t.b.s.Z3SolverContext - Creating Z3 solver context 0 2024-01-20T21:19:07,601 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0 2024-01-20T21:19:07,601 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT 2024-01-20T21:19:07,622 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - Adapted exception intercepted: at.forsyte.apalache.tla.bmcmt.RewriterException: Not implemented (open an issue): CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)] in \$C\$12 ⊆ \$C\$4 at at.forsyte.apalache.tla.bmcmt.rules.SetInclusionRuleWithFunArrays.apply(SetInclusionRuleWithFunArrays.scala:44) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422) at at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick.\$anonfun\$pickFunFromFunSet\$6(CherryPick.scala:1020) at at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick.\$anonfun\$pickFunFromFunSet\$6\$adapted(CherryPick.scala:997) at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576) at scala.collection.IterableOnceOps.foreach\$(IterableOnce.scala:574) at scala.collection.AbstractIterable.foreach(Iterable.scala:933) at scala.collection.IterableOps\$WithFilter.foreach(Iterable.scala:903) at at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick.pickFunFromFunSet(CherryPick.scala:997) at at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick.pick(CherryPick.scala:62) at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.skolemExistsByPick(QuantRule.scala:293) at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.apply(QuantRule.scala:56) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422) at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.prepareTransition(TransitionExecutorImpl.scala:107) at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.prepareTransition(FilteredTransitionExecutor.scala:48) at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.prepareTransition(ConstrainedTransitionExecutor.scala:98) at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.\$anonfun\$prepareTransitionsAndCheckInvariants\$5(SeqModelChecker.scala:213) at scala.runtime.java8.JFunction1\$mcVI\$sp.apply(JFunction1\$mcVI\$sp.scala:18) at scala.collection.immutable.Range.foreach(Range.scala:190) at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:207) at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:123) at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:62) at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:127) at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:80) at at.forsyte.apalache.infra.passes.PassChainExecutor\$.exec(PassChainExecutor.scala:64) at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$3(PassChainExecutor.scala:53) at scala.util.Either.flatMap(Either.scala:352) at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$1(PassChainExecutor.scala:51) at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183) at scala.collection.LinearSeqOps.foldLeft\$(LinearSeq.scala:179) at scala.collection.immutable.List.foldLeft(List.scala:79) at at.forsyte.apalache.infra.passes.PassChainExecutor\$.runOnPasses(PassChainExecutor.scala:44) at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:34) at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:129) at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:138) at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:118) at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40) at at.forsyte.apalache.tla.Tool.main(Tool.scala) 2024-01-20T21:19:07,624 [main] ERROR a.f.a.t.Tool\$ - : rewriter error: Not implemented (open an issue): CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)] in \$C\$12 ⊆ \$C\$4 at.forsyte.apalache.infra.AdaptedException: : rewriter error: Not implemented (open an issue): CellTFrom(Set(Int)) and InfSet[CellTFrom(Int)] in \$C\$12 ⊆ \$C\$4 at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:39) at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:129) at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:138) at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:118) at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40) at at.forsyte.apalache.tla.Tool.main(Tool.scala) ```

System information

Triage checklist (for maintainers)

konnov commented 9 months ago

@rodrigo7491, perhaps, you have some ideas?

rodrigo7491 commented 9 months ago

I could reproduce the bug on my side. After some digging, it seems that due to an interaction between CherryPick and SetInclusionRuleWithFunArrays, infinite sets are not being properly handled in this case. This is an issue for both arrays and funArrays. I will make a PR to fix this soon.