Seemingly infinite loop in equation simplification

[ehildenb]

This bug report is generated by running a simplified Maker MCD Spec (https://github.com/makerdao/mkr-mcd-spec) through the kore-repl, and killing it after it hangs for a while.

kore-exec.tar.gz

If you run the kore-repl, take 6 steps, it works just fine. But then you do stepf one more time, and it seems to hang. I turned on DebugAttemptEquation, and dumped the results to a file. From what I can tell, it's just repeatedly trying the same three equations on the same input, forever.

Here are the rules which seem to loop forever:

    syntax Bool ::= wish(Address, Address, Map) [function, functional] 
 // ------------------------------------------------------------------ 
    rule wish(ADDRFROM, MSGSENDER,        _) => true                                   requires ADDRFROM ==K MSGSENDER 
    rule wish(ADDRFROM, MSGSENDER, CANADDRS) => MSGSENDER in {CANADDRS[ADDRFROM]}:>Set requires ADDRFROM in_keys(CANADDRS) 
    rule wish(       _,         _,        _) => false                                  [owise] 

The log contains many repeats of lines like this:

kore-repl: [139189290] Debug (DebugAttemptEquation):
    (InfoReachability) while checking the implication:
    applying equation at /home/dev/src/mkr-mcd-spec-pr/vat.md:237:10-237:123 to term:
        /* Fl Fn D Spa */
        Lblwish'LParUndsCommUndsCommUndsRParUnds'VAT'Unds'Bool'Unds'Address'Unds'Address'Unds'Map{}(
            /* Fl Fn D Sfa */ ConfigVarADDRFROM:SortAddress{},
            /* Fl Fn D Sfa Cl */ LblADMIN'Unds'KMCD-DRIVER'Unds'Address{}(),
            /* Fl Fn D Sfa */ ConfigVarVAT'Unds'CANS:SortMap{}
        )

This represents the middle rule of the three listed, but all three show up in the log over and over again. Note that I only turned on logging after taking the first 6 steps.

[ttuegel]

That being the only log entry is extremely suspicious. DebugAttemptEquation should log the individual steps of attempting the equation: matching, instantiation, checking requirements. If we really don't see any of that, then we must never get far enough to even match the equation.

[ana-pantilie]

Whatever the issue is, it doesn't seem related to simplifyPredicates: if I disable it, the loop is still there. I'll continue looking to see if it's in the term simplifier.

[ehildenb]

Well, I only turned on DebugAttemptEquation. I can turn on more log entries and post results if you like?

[ana-pantilie]

@ttuegel I've identified the loop: simplifyPredicate doesn't return, so, indeed, it's the term simplifier.