apalache icon indicating copy to clipboard operation
apalache copied to clipboard

Published 20 hours ago • verified publisher icon apalache-mc

Locally declared operators break use of `VariantGetUnsafe`

Open shonfeder opened this issue 2 years ago • 8 comments

Description

I found a case where operators defined using LOCAL seem to break variable substitution when using VariantGetUnsafe. Presumably this is due to some sort of error in the rewriting logic. Specs that should succeed during checking are instead resulting in errors like:

at.forsyte.apalache.tla.pp.TlaInputError: SubstRule: Variable o$1 is not assigned a value

Impact

Prevents definition of private operators for use in Option.tla module (see #2097).

Input specification

------------------- MODULE LocalTest -----------------------
EXTENDS Apalache, Variants

\* @type: Foo(Int) => Int;
LOCAL LocalOp(o) == VariantGetUnsafe("Foo", o)
\* @type: Foo(Int) => Int;
PublicOp(o) == VariantGetUnsafe("Foo", o)

GetLocal(o) == LocalOp(o)
GetPublic(o) == PublicOp(o)

Init == TRUE
Next == TRUE

InvLocal == LocalOp(Variant("Foo", 1)) = 1
InvPublic == PublicOp(Variant("Foo", 1)) = 1
InvSucceeds == GetPublic(Variant("Foo", 1)) = 1

InvFails == GetLocal(Variant("Foo", 1)) = 1
============================================================

The command line parameters used to run the tool

apalache-mc check --inv=InvFails test/tla/LocalTest.tla

Expected behavior

This should check successfully, just as all the other invariants do.

Log files

2022-08-28T19:48:17,597 [main] INFO  a.f.a.t.Tool$ - # APALACHE version: v0.28.0-50-g1019a7ccd | build: v0.28.0-50-g1019a7ccd
2022-08-28T19:48:17,600 [main] INFO  a.f.a.t.t.o.CheckCmd - Tuning: search.outputTraces=false
2022-08-28T19:48:17,601 [main] INFO  a.f.a.t.t.o.CheckCmd - Checker options: check --inv=InvFails test/tla/LocalTest.tla
2022-08-28T19:48:17,604 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
2022-08-28T19:48:17,951 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
2022-08-28T19:48:17,951 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
2022-08-28T19:48:17,951 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
2022-08-28T19:48:18,289 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Your types are purrfect!
2022-08-28T19:48:18,289 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > All expressions are typed
2022-08-28T19:48:18,290 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK]
2022-08-28T19:48:18,291 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass
2022-08-28T19:48:18,302 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --init is not set. Using Init
2022-08-28T19:48:18,303 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --next is not set. Using Next
2022-08-28T19:48:18,303 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
2022-08-28T19:48:18,304 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
2022-08-28T19:48:18,305 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set an invariant to InvFails
2022-08-28T19:48:18,321 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass [OK]
2022-08-28T19:48:18,322 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass
2022-08-28T19:48:18,323 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
2022-08-28T19:48:18,335 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass [OK]
2022-08-28T19:48:18,335 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass
2022-08-28T19:48:18,337 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, InvFails, Next
2022-08-28T19:48:18,456 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass [OK]
2022-08-28T19:48:18,458 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #5: TemporalPass
2022-08-28T19:48:18,465 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > Rewriting temporal operators...
2022-08-28T19:48:18,465 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > No temporal property specified, nothing to encode
2022-08-28T19:48:18,467 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #5: TemporalPass [OK]
2022-08-28T19:48:18,469 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #6: InlinePass
2022-08-28T19:48:18,470 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, InvFails, Next
2022-08-28T19:48:18,475 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #6: InlinePass [OK]
2022-08-28T19:48:18,476 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #7: PrimingPass
2022-08-28T19:48:18,487 [main] INFO  a.f.a.t.a.p.PrimingPassImpl -   > Introducing InitPrimed for Init'
2022-08-28T19:48:18,489 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #7: PrimingPass [OK]
2022-08-28T19:48:18,490 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #8: VCGen
2022-08-28T19:48:18,493 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Producing verification conditions from the invariant InvFails
2022-08-28T19:48:18,513 [main] INFO  a.f.a.t.b.VCGenerator -   > VCGen produced 1 verification condition(s)
2022-08-28T19:48:18,522 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #8: VCGen [OK]
2022-08-28T19:48:18,522 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #9: PreprocessingPass
2022-08-28T19:48:18,522 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
2022-08-28T19:48:18,530 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
2022-08-28T19:48:18,531 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
2022-08-28T19:48:18,532 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
2022-08-28T19:48:18,533 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
2022-08-28T19:48:18,534 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
2022-08-28T19:48:18,535 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
2022-08-28T19:48:18,537 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
2022-08-28T19:48:18,539 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #9: PreprocessingPass [OK]
2022-08-28T19:48:18,539 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #10: TransitionFinderPass
2022-08-28T19:48:18,549 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 1 initializing transitions
2022-08-28T19:48:18,554 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 1 transitions
2022-08-28T19:48:18,557 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > No constant initializer
2022-08-28T19:48:18,560 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Applying unique renaming
2022-08-28T19:48:18,562 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #10: TransitionFinderPass [OK]
2022-08-28T19:48:18,563 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #11: OptimizationPass
2022-08-28T19:48:18,577 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
2022-08-28T19:48:18,580 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2022-08-28T19:48:18,585 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
2022-08-28T19:48:18,587 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
2022-08-28T19:48:18,588 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2022-08-28T19:48:18,589 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #11: OptimizationPass [OK]
2022-08-28T19:48:18,590 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #12: AnalysisPass
2022-08-28T19:48:18,597 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
2022-08-28T19:48:18,599 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
2022-08-28T19:48:18,600 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
2022-08-28T19:48:18,602 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
2022-08-28T19:48:18,608 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
2022-08-28T19:48:18,614 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
2022-08-28T19:48:18,615 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #12: AnalysisPass [OK]
2022-08-28T19:48:18,615 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #13: BoundedChecker
2022-08-28T19:48:18,864 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
2022-08-28T19:48:18,864 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
2022-08-28T19:48:19,011 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0. Is it enabled?
2022-08-28T19:48:19,013 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0 is enabled
2022-08-28T19:48:19,014 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: Checking 1 state invariants
2022-08-28T19:48:19,016 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking state invariant 0
2022-08-28T19:48:19,017 [main] ERROR a.f.a.t.b.r.SubstRule - This error may show up when CONSTANTS are not initialized.
2022-08-28T19:48:19,018 [main] ERROR a.f.a.t.b.r.SubstRule - Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html
2022-08-28T19:48:19,020 [main] DEBUG a.f.a.i.Executor - Adapted exception intercepted: 
at.forsyte.apalache.tla.pp.TlaInputError: SubstRule: Variable o$1 is not assigned a value
	at at.forsyte.apalache.tla.bmcmt.rules.SubstRule.apply(SubstRule.scala:36)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:334)
	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.VariantOpsRule.translateVariantGetUnsafe(VariantOpsRule.scala:73)
	at at.forsyte.apalache.tla.bmcmt.rules.VariantOpsRule.apply(VariantOpsRule.scala:37)
	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.IntArithPacker.packArithExpr(IntArithPacker.scala:54)
	at at.forsyte.apalache.tla.bmcmt.rules.IntArithPacker.packArithExpr$(IntArithPacker.scala:29)
	at at.forsyte.apalache.tla.bmcmt.rules.EqRule.packArithExpr(EqRule.scala:16)
	at at.forsyte.apalache.tla.bmcmt.rules.EqRule.apply(EqRule.scala:33)
	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.NegRule.apply(NegRule.scala:27)
	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.assertState(TransitionExecutorImpl.scala:215)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.assertState(FilteredTransitionExecutor.scala:123)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.assertState(ConstrainedTransitionExecutor.scala:111)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2(SeqModelChecker.scala:360)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2$adapted(SeqModelChecker.scala:348)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)
	at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:926)
	at scala.collection.IterableOps$WithFilter.foreach(Iterable.scala:896)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.checkInvariants(SeqModelChecker.scala:348)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$5(SeqModelChecker.scala:251)
	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:215)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:133)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:63)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:132)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:88)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:23)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.$anonfun$run$5(PassChainExecutor.scala:47)
	at scala.util.Either.flatMap(Either.scala:352)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.$anonfun$run$3(PassChainExecutor.scala:46)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:169)
	at scala.collection.LinearSeqOps.foldLeft$(LinearSeq.scala:165)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:41)
	at at.forsyte.apalache.infra.Executor.run(Executor.scala:35)
	at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:109)
	at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:139)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:119)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:36)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
2022-08-28T19:48:19,021 [main] ERROR a.f.a.t.Tool$ - Input error (see the manual): SubstRule: Variable o$1 is not assigned a value
2022-08-28T19:48:19,022 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min  1 sec
2022-08-28T19:48:19,022 [main] INFO  a.f.a.t.Tool$ - Total time: 1.421 sec

Triage checklist (for maintainers)

  • [x] Reproduce the bug on the main development branch.
  • [x] Add the issue to the apalache GitHub project.
  • [ ] If the bug is high impact, ensure someone available is assigned to fix it.

shonfeder avatar Aug 28 '22 23:08 shonfeder

@Kukovec, could it be something about the inliner?

konnov avatar Aug 29 '22 09:08 konnov

I looked at this today, and the problem arises way before this gets to the inliner. Essentially,

LOCAL LocalOp(o) == VariantGetUnsafe("Foo", o)
...
GetLocal(o) == LocalOp(o)

turns into

GetLocal(o) ==
  LET (*
    @type: Foo(Int) => Int;
  *)
  LOCAL84_i_LocalOp(o) == VariantGetUnsafe("Foo", o)  
  IN
  LOCAL84_i_LocalOp(o)

in 00_OutSanyParser.tla. As you can see, there's shadowing of o inside the LET-definition.

Kukovec avatar Mar 15 '23 15:03 Kukovec

Yeah, we could fix it by renaming o to LOCAL84_i_o, though this would require some substitution in the importer. We need a systematic approach to shadowing, as it is happening anyways.

konnov avatar Mar 16 '23 08:03 konnov

We have a systematic approach, it's called "using the scoped builder".

Kukovec avatar Mar 16 '23 10:03 Kukovec

But beyond that, as soon as any form of rewriting occurs, the only reasonable way to consistently avoid shadowing is to mangle all the names into unique, illegal-character prefixed strings.

Kukovec avatar Mar 16 '23 10:03 Kukovec

I just tried sketching out what it would take to add a simple UniqueNameGenerator to OppApplTranslator::translateLocalOperator. Since basically none of the classes in the parser pass are injection-managed, you'd need to pass it along all the way from ExprOrOpArgNodeTranslator, of which tens of instances are created across the code. And there's even more classes above that, but I just gave up at that point. I think it's worth revisiting the parser pass architecture, at some point in Q2/Q3, and at the very least document it, if not rework it.

Kukovec avatar Mar 16 '23 11:03 Kukovec

We have a systematic approach, it's called "using the scoped builder".

I don't see how this is related. Local operators are substituted in the importer.

konnov avatar Mar 16 '23 12:03 konnov

We have a systematic approach, it's called "using the scoped builder".

I don't see how this is related. Local operators are substituted in the importer.

Yes, and the importer manually constructs a LetInEx(...). If the builder was used instead, this issue would have been found immediately, with a ScopingException.

Kukovec avatar Mar 16 '23 13:03 Kukovec