Commits on Aug 30, 2024

1. fix(BV): Do not build unnormalized values in zero_extend …

   There is a stupid bug in the [zero_extend] function introduced in OCamlPro#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 committed Aug 30, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 3cb8cd5
   • Browse repository at this point

   Copy the full SHA

   3cb8cd5 View commit details

   Browse the repository at this point in the history