search

OCamlPro / alt-ergo

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

fix(BV): Do not build unnormalized values in zero_extend #1226

Closed bclement-ocp closed 2 weeks ago

bclement-ocp commented 2 weeks ago

There is a stupid bug in the [zero_extend] function introduced in #1154: if the high bits of the extended value are known, it can create an unnormalized semantic value, which causes unsoundness.

Fix the [zero_extend] function, which is renamed to [zero_extend_to] since it takes as argument the extended size rather than the number of additional bits to add. Move the implementation to the [Bitv] module.

To prevent similar failures in the future, an heavy assertion is added in [solve] (where unsoundness would otherwise occur). I also tried to make the [Bitv.abstract] type private again, but that was a pain as it is used in several places in [Bitv_rel], so instead I simplified the code to avoid creating [Bitv.abstract] values from outside of the [Bitv] module where it was easy to do so.

No regression tests because I don't believe we can hit the bug with the code in next: we are only calling [zero_extend] on variables, so we can never create an unnormalized value this way.

bclement-ocp commented 2 weeks ago

Adding the soundness tag because this bug could cause soundness issues in conjunction with other patches, even though I don't think there is a soundness bug on next.