Fix bug in scanner cache PR when running kprove

[dwightguth]

You should not need to review the first commit as it is identical to the one previously reviewed. This PR just fixes the issue where we were still trying to serialize the scanner when parsing rules in kprove.

Note that we do not need to fix the case where we are deserializing the scanner yet, because we do not yet use the serialized scanner while parsing anything other than search patterns. In a follow-up PR, once this is suitably working, we will need to ensure that we use the cached scanner during kprovex

[SchmErik]

looks good to me

[radumereuta]

@dwightguth can you remind me how is this supposed to work?
I tested this and it still generates extra scanners even when kompiling twice.

regression-new/map-symbolic-tests-haskell$ kompile --no-exc-wrap --backend haskell  map-tests.k -d . -v
Parse command line options                                   =  0.011s
Importing: Source(/home/radu/work/k/k-distribution/tests/regression-new/map-symbolic-tests-haskell/map-tests.k)
Outer parsing [67 modules]                                   =  0.772s
  New scanner: MAP-TESTS-CONFIG-CELLS                        =  0.142s
  New scanner: STDOUT-STREAM-CONFIG-CELLS                    =  0.196s
  New scanner: STDIN-STREAM-CONFIG-CELLS                     =  0.220s
Parse configurations [3/3 declarations]                      =  0.525s
  New scanner: MAP-TESTS-RULE-CELLS                          =  0.128s
  New scanner: STRING-KORE-RULE-CELLS                        =  0.176s
  New scanner: STRING-COMMON-RULE-CELLS                      =  0.199s
  New scanner: MAP-TESTS-RULE-CELLS                          =  0.215s
  New scanner: K-IO-RULE-CELLS                               =  0.314s
  New scanner: STDOUT-STREAM-RULE-CELLS                      =  0.294s
  New scanner: STDIN-STREAM-RULE-CELLS                       =  0.322s
Parse rules [120/120 rules]                                  =  0.635s
Validate definition                                          =  0.149s
Apply compile pipeline                                       =  0.298s
Kompile to kore                                              =  0.005s
Save to disk                                                 =  0.033s
Backend                                                      =  0.342s
Cleanup                                                      =  0.001s
Total                                                        =  2.771s
regression-new/map-symbolic-tests-haskell$ kompile --no-exc-wrap --backend haskell  map-tests.k -d . -v
Parse command line options                                   =  0.011s
Importing: Source(/home/radu/work/k/k-distribution/tests/regression-new/map-symbolic-tests-haskell/map-tests.k)
Outer parsing [67 modules]                                   =  0.725s
Parse configurations [0/3 declarations]                      =  0.287s
  New scanner: MAP-TESTS-RULE-CELLS                          =  0.133s
Parse rules [0/120 rules]                                    =  0.189s
Validate definition                                          =  0.132s
Apply compile pipeline                                       =  0.346s
Kompile to kore                                              =  0.006s
Save to disk                                                 =  0.033s
Backend                                                      =  0.388s
Cleanup                                                      =  0.001s
Total                                                        =  2.118s
regression-new/map-symbolic-tests-haskell$ 

[dwightguth]

The goal of this PR isn't to stop scanners from being created when you run kompile; that's because we don't have any logic for deciding if the cached scanner is out of date, nor would it be particularly easy to do this. It is merely to allow us to reuse scanners during krun and eventually kprovex that are identical to the one generated by kompile

[radumereuta]

Ok, fine for now.
But you can check that the grammar used to generate the scanner is equal.
It's a coarse solution because you check the entire grammar instead of only the lexical part but it should work.

[dwightguth]

Sure, in theory you can, but any substantive change to the definition's syntax will ultimately invalidate the scanner, whereas you have now introduced a new check for equality that is pretty massive that has to be run on every invocation of kompile. I'm not convinced it's really going to help much during day to day development. Besides, my primary goal with this change is to reduce time spent on the hot path, which doesn't include time spent in kompile. We can separately try to improve time spent in kompile, of course, but generating the scanner isn't generally where most of that time is being spent in large definitions right now. Regardless, I'm going to merge this and we can continue to iterate improvements

[radumereuta]

We do grammar comparison when we invalidate cached rules anyway.
Why are you saying this is 'massive'?

[dwightguth]

We do grammar comparison when we invalidate cached rules if we have rules in the module in question. However, if the definition consists of many modules each with a few pieces of syntax, all imported into one module with no rules, then we won't actually need to do the cache invalidation check on the entire grammar all at once. Thus, you would still end up doing additional work.