Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix type safety issues in sorted collections #15

Merged
merged 11 commits into from
Jun 23, 2024
Merged

Conversation

ericeil
Copy link
Collaborator

@ericeil ericeil commented May 16, 2024

The treap-based collections are split into hashed and sorted variants. The hashed collections are the most versatile; they'll work for any key type. The sorted collections are specific to Comparable types, taking advantage of the ordering to avoid having to deal with hash collisions.

We don't expose the notion of sorted vs hashed in the public API. Instead, we automatically create the correct collection type based on the element type. This mostly works, but has some issues currently. Take the following for example:

treapSetOf(1, null)

This is allowed statically (treapSetOf has no restrictions on the element type), but currently throws a NullPointerException at runtime. The reason is that the first element is Comparable, and so we create a SortedTreapSet, which is effecively a TreapSet<Comparable<T>> Then, when we add the null, we fail the runtime check that the element is a Comparable<T>, because it is null.

Similarly, if we start with a Comparable, and then add a non-Comparable, we also crash:

data class Foo(a: Int)
treapSetOf<Any>(1, Foo(2)) 

Where we went wrong is in making SortedTreapSet a TreapSet<Comparable<T>>. Conceptually, SortedTreapSet should be a set of arbitrary values - that just happens to only contain values that are Comparable.

We fix this by removing the constraint from SortedTreapSet (and SortedTreapMap), and adding some runtime checks to switch to the hashed collections if a non-Comparable key is added.

We also allow null as a sorted key, which prevents the (quite expensive) downgrade to the hashed collections just to get nullability.

@ericeil ericeil requested a review from jtoman May 16, 2024 22:13
@ericeil ericeil merged commit 01ac23a into Certora:main Jun 23, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant