-
Notifications
You must be signed in to change notification settings - Fork 84
Description
Motivation
The actual state of mutually refining integer domains does not allow representing the union of non-overlapping intervals such as {[0, 3] [7, 10]}
If we had this information, we could improve our analyses by detecting unreachable parts of the code.
and hence improving our overflow detection.
Computational Challenge:
The naive approach of interval sets (i.e. an arbitrarily big set of intervals) is computationally problematic, given that theoretically the number of intervals we store in the set could grow quadratically after applying each operation. A solution to this would be to apply (a possibly parametrized) upper bound to the set cardinality. This should add more complexity to the way the operations are implemented. That is, if the naive operation returns many more intervals than the upper bound, we will have to sacrifice some information to respect the upper bound and avoid an explosion of the number of intervals in the set.
TODOs:
- Implement the S interface (while getting inspiration from the Interval domain implementation) including the domain concrete representation and the different operations (arithmetic ops, constructors, lattice ops)
- Refine the implementation towards being more efficient and keeping a good amount of information (maybe lookup for literature documenting relatable projects/experiences)
- Implement regression tests
- add new flag options in order to run the interval
- adjust the base.ml analysis accordingly to benefit from the refinement that our implementation requires.
