Relax module duplication check#2972
Conversation
Allows for file copy by checking filename and module digest Fixes: #2910
to better match the actual check.
Avoids changing the definition and therefore changing the output of kore-exec
Baltoli
left a comment
Baltoli
left a comment
There was a problem hiding this comment.
I don't think the error message in the test here is particularly clear - the modules here are in fact identical, but happen to be declared in the same file. We probably want to distinguish (if possible) this case from "the exact same module, but moved on disk".
| // Tuple3 of moduleName, Source, Location | ||
| Map<String, List<Tuple3<String, Source, Location>>> groupedModules = | ||
| // Tuple3 of moduleName, Source, Location, digest | ||
| Map<String, List<Tuple4<String, Source, Location, Long>>> groupedModules = |
There was a problem hiding this comment.
this is probably not what you want. The tuple of String, Source, Location was being used to identify modules that appeared in two places with different filenames or locations. You probably just instead want to identify two modules that have the same name but different contents, in which case you really only need module name and digest in the value of the map.
| + firstMod._2() + " and " + firstMod._3(), secondMod._2(), secondMod._3()); | ||
| errors++; | ||
| kem.addKException(ex.getKException()); | ||
| // give an error message only if we have |
There was a problem hiding this comment.
if you do what I suggested above, we don't really need this check.
| genPriorityGroups(priorityList, priorityToPreviousGroup, priorityToAlias, topCellSortStr, semantics); | ||
| semantics.append("endmodule "); | ||
| convert(attributes, module.att(), semantics, null, null); | ||
| convert(attributes, module.att().remove(Att.DIGEST()), semantics, null, null); |
There was a problem hiding this comment.
instead of doing this, let's just remove the digest attribute when converting from a FlatModule back to a Module.
There was a problem hiding this comment.
That's not going to work for kprove.
We store CompileDefinition.parsedDefinition which has Module.
If we strip that attribute we won't have it when we do slurp in kprove. Which is where the failure happens.
|
Okay I am now very confused about exactly what this change is supposed to be fixing. Let's discuss in the meeting tomorrow. I don't understand why kprove would be worried about duplicate modules having a different location unless it's reparsing the definition during proof time, which it should not be doing anymore. |
- better hashing - comments
|
Guessing by the comments on this PR, all 3 of us have different opinions on what should happen when we encounter duplicate modules. My implementation is the most strict I can think of. It only allows for moving files around. Let's discuss this in the KDev meeting tomorrow. |
|
We probably should just keep all modules in the definition in lexical scope when parsing kprove and then make it an error to redeclare any of them in your spec module, including via |
|
We sometimes |
4 participants
Allows for file copy by checking: 1. filename 2. location and 3. module digest
Fixes: #2910