OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
132 stars 33 forks source link

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

Closed bclement-ocp closed 2 months ago

bclement-ocp commented 3 months ago

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.

Halbaroth commented 3 months ago

I was writing the issue :)

bclement-ocp commented 3 months ago

I thought I sent a DM saying I was looking into it since it is my code, but apparently I did not — apologies.