Skip to content

Add MAP import to all modules containing configs#1965

Merged
rv-jenkins merged 4 commits intomasterfrom
mapImport
May 13, 2021
Merged

Add MAP import to all modules containing configs#1965
rv-jenkins merged 4 commits intomasterfrom
mapImport

Conversation

@radumereuta
Copy link
Copy Markdown
Contributor

@radumereuta radumereuta commented May 12, 2021

This simple test fails on master.
The MAP module should be added to every module where a configuration is present.

@radumereuta radumereuta marked this pull request as draft May 12, 2021 18:02
@radumereuta radumereuta requested a review from dwightguth May 12, 2021 18:34
@radumereuta radumereuta marked this pull request as ready for review May 12, 2021 18:35
Only by name so we keep efficiency. This fixes some module duplication issues when importing new modules.
The first one does the same thing.
@radumereuta radumereuta requested a review from ehildenb May 12, 2021 20:19
Copy link
Copy Markdown
Contributor

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you explain to me why this change is needed in order to fix Algorand on your PR when it works fine on master already? If you can't explain why it's needed, I really can't justify this.

@ehildenb
Copy link
Copy Markdown
Member

@dwightguth this seems like a bugfix to me (or at least, the intent is one, based on my conversations with @radumereuta on Slack).

He discovered (while doing other work), that if the mainModule does not import MAP but contains a configuration (either locally or in one of its imports), then import MAP will be added to the mainModule.

This works if your configuration declaration is in the mainModule, but if it's in a module that is imported by it which does not already import MAP, then MAP will be missing from the module with the configuration declaration in it, where it is needed.

Comment thread kore/src/main/scala/org/kframework/definition/outer.scala Outdated
The default behavior preserves import structure
@radumereuta
Copy link
Copy Markdown
Contributor Author

@dwightguth ignore Algorand for now. I encounter errors like this sometimes, and I prefer to fix that if it's isolated instead of trying to work around it to push another PR. (in this case the scanner changes)
Instead, look at the test I added. On master that fails with a parse error in the configuration because it can't parse token Map.

@ehildenb I've removed the equals method completely. Now the default behavior checks for:
Module(name, localSentences, imports, att)
Previously it would check only for name and the cumulated sentences which would ignore completely the import structure. For a single pass it may be fine, but when you apply multiple transformers and change connections between modules can lead to inconsistent states.
I found about this because k-exercises/tutorial/1_k/3_lambda++/lesson_1/exercises/from-call-CC-to-callcc failed. So we already have a test. Not sure how to test it even further, because what I did was to remove an optimization. I also tested regression-new and Algorand and the times are exactly the same.

This is related partially to #1838. It mitigates it a bit, but not completely. I have a bit more confidence that at least it no longer duplicates modules semantically.

@radumereuta radumereuta requested a review from dwightguth May 13, 2021 12:10
Copy link
Copy Markdown
Contributor

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems an acceptable change if I view it as purely unrelated to the scanner changes, and if it can resolve some of the issues with duplicated modules later in the pipeline, so much the better. We should have a discussion about what exactly we want the behavior of K to be here, though, before we merge this. We automatically imported MAP into the main module prior because the definition doesn't work without it. Forcing the other modules to explicitly import MAP if they use map productions makes the import system more consistent, but the configuration declaration semantics inconsistent. Whereas, allowing the other modules to automatically import MAP makes the semantics of configuration declarations more consistent, but the semantics of imports less consistent. I don't have a strong opinion on which is better, but it seems there are pros and cons to both, so we should probably discuss this as a design change rather than treating it purely like a bugfix.


override lazy val hashCode: Int = name.hashCode

override def equals(that: Any) = that match {
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we're going to be using the default equals for case classes, let's use the default hashCode as well.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought about that. But I think this is faster and still safe.
It's only used to quickly determine if two modules are different. And in our case, that happens most of the time since a Definition has unique Module names.

@radumereuta
Copy link
Copy Markdown
Contributor Author

Master behavior:
This parses fine:

module CONFIG1
configuration <k> .K </k>
endmodule

module CONFIG2
imports CONFIG1
configuration <x> <k/> <y> .Map </y> </x>
endmodule

module TEST
imports CONFIG2
endmodule

This gives an error message: Parse error: unexpected token 'Map'.

module CONFIG
configuration <x> <k> .K </k> <y> .Map </y> </x>
endmodule

module TEST
imports CONFIG
endmodule

So I view this branch as actually a bug fix. It makes the behavior more consistent.
Now both of the examples parse w/o errors.

@radumereuta radumereuta requested a review from dwightguth May 13, 2021 15:57
@dwightguth
Copy link
Copy Markdown
Contributor

I mean, it makes it so that an anomaly is more consistently anomalous, if that's what you mean. That's not the same thing as just being unqualifiedly more consistent. As I said, I want to see us discuss this as a group, even if it's brief because everyone has consensus.

@radumereuta
Copy link
Copy Markdown
Contributor Author

radumereuta commented May 13, 2021

Timings:
make build -j 1
EVM master: 1m07.004s, this branch 1m07.344s
make build -j 10
Algorand master: 2m16s, 2m19s. This branch 2m42s, 2m25s, 2m26s.
These numbers are consistent with what I usually get and in the same range.

I tested EVM with and w/o hashCode:
hashCode deleted: 3m47s, 1m28s, 1m40s
with hashCode again: 1m06s
It seems it's more consistent with precomputed hashCode.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants