NormalizedAc.concreteElements, InternalMap, InternalSet: use HashMap and HashSet

[ana-pantilie]

Fixes #2508

Recent changes to the backend resulted in more frequent AC collection comparisons and this PR should fix the performance of that.

---

Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

• Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
• Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
• Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
• Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

[ana-pantilie]

I noticed that some of the property tests were actually failing because the term contained symbolic elements which were reordered. Turns out I had modified part of Kore.Builtin.AssociativeCommutative to use HashMap instead of Map, and we reuse the same functions for the symbolic parts and the concrete parts. Fixing this meant switching back to using Map throughout that module, and at the end converting the concrete Maps to HashMaps.

Other issues are related to our builtin evaluation and tests: we use Map and Set there, so we end up with two representations which differ by the ordering of the elements.

Would a good solution be to switch everything related to maps and sets to use HashMap and HashSet instead? I think that mixing the regular and hashed versions is pretty confusing and it's probably not that ideal in terms of performance, but I might be wrong or overlooking something.

Sort of related: do we still want to keep the symbolic elements and the opaque elements in lists?

[ana-pantilie]

We decided to use the hashed versions instead everywhere in the builtin code.

[ana-pantilie]

Edit: we discussed that this is not a problem in practice.

The integration test below is failing, and I think it's because before we'd only pick the path where X=b while, now, because the set isn't ordered we're going with X=c. I might be wrong, but I remember that one-path is implemented in such way that we only pick one particular path of execution, instead of executing all paths and just checking if at least one is proven (in contrast to all-path where we expect all of them to be proven).

module VERIFICATION
  imports PATH

endmodule

module ONE-PATH-B-SPEC
  imports VERIFICATION
  imports PATH

  // This should be provable as an one-path claim, but should not be provable as an 
  //all-path claim.
  claim <k> select => b </k>
       <state> SetItem(b) SetItem(c) </state>
    [one-path]

endmodule

with semantics:

module PATH
  import BOOL
  import INT
  import SET
  syntax S ::= "a" | "b" | "c" 
  syntax Cmd ::= "select"

  configuration <k> .K </k> <state> .Set </state>

  rule <k> select => X ...</k> <state>... SetItem(X:S) ...</state>
endmodule

Expected result is \\top, but with these changes it's:

<generatedTop>
  <k>
    c ~> .
  </k>
  <state>
    SetItem ( b )
    SetItem ( c )
  </state>
</generatedTop>

[MirceaS]

Can you confirm that no use of this function supplies an f that is non-injective? Because if it did, we would risk losing entries from the hash map.

[ana-pantilie]

We only ever use this function in places where we used to use Data.Map.Strict.mapKeys, which has the same behavior you described.