Haskell backend loops on simple proof

[ehildenb]

Given K version (v5.2.21 with only updates to pyk library, should not affect this bug) and kore-exec version:

+ kompile --version
K version:    v5.2.21-17-g60eaf47005-dirty
Build date:   Wed Dec 01 21:25:44 UTC 2021
+ kore-exec --version
Kore version 0.58.0.0

we have an infinite loop (or seemingly), and it uses a lot of memory (OOMs my 96GB machine) on this specification:

requires "domains.md"

module TEST
    imports INT
    imports SET
    imports BOOL 

    configuration <k> $PGM:Foo </k>

    syntax Foo ::= run ( Set ) | done ( Set )
 // -----------------------------------------
    rule <k> run(S) => done(S) ... </k>

    syntax Int ::= f ( Int ) [function, no-evaluators]

    rule X ==Int f(X) => false [simplification]
    rule f(X) ==Int X => false [simplification]
endmodule

module TEST-SPEC
    imports TEST

    claim <k> run(SetItem(X) |Set SetItem(f(X))) => done(SetItem(X) SetItem(f(X))) ... </k>

endmodule

I've looked at equation debug logs and such, and can't seem to find that it's applying equations in an infinite loop. Rather, it seems to get stuck in evaluateCondition or something.

I've attached a bug report. kore-exec.tar.gz

[dopamane]

Reproducible. At first I thought this might be due to f5bed2d571628241f68c37e22d0bacb15094b6ee from the broken pipe error log but the behavior is the same when reverted.

Changing --log-level to debug, it seems to get stuck after applying an equation:

Partial debug output (last attempt and application)

``` kore-exec: [462230] Debug (DebugAttemptEquation): (DebugAttemptEquation) while applying equation at /home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md:559:8-559:45: equation is applicable kore-exec: [462638] Debug (DebugApplyEquation): applied equation at /home/dev/src/k/k-distribution/target/release/k/include/kframework/builtin/domains.md:559:8-559:45 with result: \and{SortSet{}}( /* term: */ /* Fn Spa */ /* InternalSet: */ Lbl'Unds'Set'Unds'{}( /* opaque child: */ /* Fn Spa */ LblSet'Coln'difference{}( /* Fn Spa */ /* InternalSet: */ /* element: */ LblSetItem{}( /* Fn Spa */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fn Spa */ Lblf'LParUndsRParUnds'TEST'Unds'Int'Unds'Int{}( /* Fl Fn D Sfa */ RuleVarX:SortInt{} ) ) ), /* Fl Fn D Spa */ /* InternalSet: */ /* element: */ LblSetItem{}( /* Fl Fn D Spa */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa */ RuleVarX:SortInt{} ) ) ), /* opaque child: */ /* Fl Fn D Spa */ /* InternalSet: */ /* element: */ LblSetItem{}( /* Fl Fn D Spa */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa */ RuleVarX:SortInt{} ) ) ), \and{SortSet{}}( /* predicate: */ /* D Sfa */ \top{SortSet{}}(), /* substitution: */ \top{SortSet{}}() )) ```

[ehildenb]

Note we get the same behavior even if I remove the ==Int lemmas present here (though those should be needed for this to work).

[ana-pantilie]

We should attempt to reproduce this again.

[denis-bogdanas]

K frontend commit: 0b58d4778 backend commit: 7eb8cdd39

[radumereuta]

@ana-pantilie please open a front-end issue with the changes required to make this work. We should need to add similar axioms to what we do for Maps here: https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java#L179

[jberthold]

Two simpler examples to reproduce the looping behaviour:

File test.k

module TEST
  imports SET

  syntax Run ::= Run ( Set ) | Done ( Set )

  configuration <k> $PGM:Run </k>

  rule <k> Run(S) => Done(S) ... </k>

endmodule

File spec.k

requires "test.k"
module SPEC
  imports TEST

  claim [loop1]: Run ( (S SetItem(X)) -Set SetItem(Y)     ) => Done (?_)
  claim [loop2]: Run ( SetItem(X)     |Set (S SetItem(Y)) ) => Done (?_)

endmodule

From running with an eventlog, it is clear that both claims do not actually enter rewriting at all, they are already looping when the prover starts up (however not when claims are filtered out): $ kprove --claims SPEC.loop1 spec.k loops $ kprove --claims SPEC.loop2 spec.k loops $ kprove --claims SPEC.doesnotexist spec.k does not loop