Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Sep 4, 2025

Previously the exclusion bit ranges used this module:

module Interval32 = IntDomWithDefaultIkind (IntDomLifter (SOverflowUnlifter (IntervalFunctor (IntOps.Int64Ops)))) (IntIkind)

There's a lot of unnecessary complication here:

  1. We're using our ikind-aware interval domain implementation for the bit ranges, which aren't really C things. And to do it we're arbitrarily considering them as C int.
  2. This ikind-awareness lifts each interval domain element into a record which also keeps track of the ikind, which is always the same for bit ranges.
  3. We're using our C overflow-aware interval domain and forgetting the overflow_info which isn't relevant for the small bit ranges anyway.
  4. Our IntervalFunctor also has bot, but bit ranges should never have that: if the bit range is bottom, the whole def_exc/enums abstraction should become bottom.
  5. For historical reasons, the bit range interval pairs are int64 * int64, but int * int would be enough for bit ranges (they're very small numbers anyway). But also it avoids extra indirection needed by int64 in OCaml.

After this PR, the module is much simpler:

module R = IntervalArith (IntOps.NIntOps)
  1. IntervalArith isn't a full-blown Lattice, but just a small set of mathematical interval operations (without a bottom). This already existed before to share some code, but is slightly extended here.
  2. NIntOps uses int for the bounds.

TODO

@sim642 sim642 added this to the v2.7.0 Bamboozled Buffalo milestone Sep 4, 2025
@sim642 sim642 added cleanup Refactoring, clean-up pr-dependency Depends or builds on another PR, which should be merged before labels Sep 4, 2025
Base automatically changed from suppress_ovwarn to master September 22, 2025 08:05
@sim642 sim642 added type-safety Type-safety improvements and removed pr-dependency Depends or builds on another PR, which should be merged before labels Sep 22, 2025
@sim642 sim642 marked this pull request as ready for review September 22, 2025 08:55
@sim642 sim642 merged commit ae53fb0 into master Sep 24, 2025
21 of 22 checks passed
@sim642 sim642 deleted the interval32 branch September 24, 2025 07:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up type-safety Type-safety improvements

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant