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.

Sign up for GitHub

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

Jump to bottom

fix(CP): Make sure domains do not overflow the default domain #1225

Merged
merged 2 commits into from
Aug 29, 2024
Merged

fix(CP): Make sure domains do not overflow the default domain #1225

merged 2 commits into from
Aug 29, 2024

Commits on Aug 29, 2024

  1. fix(CP): Make sure domains do not overflow the default domain 

    When reading domains through a non-canonical representative, we are
intersecting it with the default domain of the representative (i.e. the
range of the bit-vector type) in order to ensure that the resulting
domain is known to be within the range of the type.

This is useful for interval domains because we keep track of global
bounds, which we rely on in functions such as [bvshl], but are forgotten
by the call to [add_explanation].

We also need to perform the same intersection when modifying a domain
through a non-canonical representative, otherwise we might store a
domain that overflows the bounds of the type.

(It is unfortunate that we have to do this dance instead of storing type
information on the interval themselves, but that would be a bigger change).

This was found by fuzzing.
    @bclement-ocp
    bclement-ocp committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    87ebbbd View commit details
    Browse the repository at this point in the history

  2. Clarify doc

    @bclement-ocp
    bclement-ocp committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    fda5089 View commit details
    Browse the repository at this point in the history