Remove CircInterval implementation

[jerhard]

This PR removes the CircInterval implementation as it is broken and we have another interval implementation.

[jerhard]

Note that there were some more complicated and probably clever implementations for bitwise operations on circular intervals in warren.ml. The implementation in our interval domain is much more simple (and thus less precise).

[michael-schwarz]

I think we are good to merge!

[sim642]

We might have to rethink IntDomTuple at some point, so that it doesn't hard-code the number of possible integer analyses. Something more dynamic would be convenient but also probably less type-safe by using Obj. MCP2 kind of does that, but I find that hacky as well: it stores things as assoc lists with some indices as "keys".

[vogler]

We might have to rethink IntDomTuple at some point, so that it doesn't hard-code the number of possible integer analyses. Something more dynamic would be convenient but also probably less type-safe by using Obj. MCP2 kind of does that, but I find that hacky as well: it stores things as assoc lists with some indices as "keys".

analyzer/src/cdomains/intDomain.ml

Line 2034 in 90eda01

module IntDomList : S = (* deprecated, use IntDomTuple below *)

There was this before, but also static.
I see the appeal but at the moment there are only 10 lines to touch if you want to add a new integer domain.
The question is what's better in terms of performance. My assumption was that the list approach saves some memory but is much slower.

[sim642]

The question is what's better in terms of performance. My assumption was that the list approach saves some memory but is much slower.

This likely needs some more in-depth profiling (like most of Goblint really...) because it's not obvious at all. For example, if using just DefExc in a 4-component IntDomTuple, most operations would also be doing lots of BatOption.map calls on None. Or for example, create/create2 in IntDomTuple make repeated get_bool calls each time, which involves a lot more than looking up a locally cached bool variable (some places do this with options).

My general suspicion and experience with #164 is that we have subtle but massive performance bottlenecks in all sorts of subtle places, but nobody has ever profiled Goblint properly. Which isn't surprising because OCaml profiling tooling is almost non-existent. I tried and still ended up just guessing and using Stats.time to pin the problem.

[vogler]

This likely needs some more in-depth profiling (like most of Goblint really...) because it's not obvious at all. For example, if using just DefExc in a 4-component IntDomTuple, most operations would also be doing lots of BatOption.map calls on None.

The assumption was that for n activated out of m total domains you have for a binop

• n * (1+2) (List.map2 + both args) match for IntDomList
• m match for IntDomTuple.

I think I ran some test where it was faster, but would be better to have some inline benchmarks [1] in bench for questions like this.
The main motivation was to reduce boilerplate and make adding domains easier.

Or for example, create/create2 in IntDomTuple make repeated get_bool calls each time, which involves a lot more than looking up a locally cached bool variable (some places do this with options).

create/create2 shouldn't be called often compared to map*.
But good point in general. Maybe it's a good idea to include some memoization for GobConfig.get_* instead letting consumers implement it repeatedly.
Edit: done: 5c73008

My general suspicion and experience with #164 is that we have subtle but massive performance bottlenecks in all sorts of subtle places, but nobody has ever profiled Goblint properly. Which isn't surprising because OCaml profiling tooling is almost non-existent. I tried and still ended up just guessing and using Stats.time to pin the problem.

True, perf report [2] works but it's hard to find bottlenecks, for example it does not list things like get_bool. Haven't tried if enabling frame pointers helps.
The equality stuff in bench/hashcons also looks interesting. What speaks against let (=) a b = a == b || a = b?

[1] https://github.com/Chris00/ocaml-benchmark
[2] https://ocaml.org/learn/tutorials/performance_and_profiling.html#Using-perf-on-Linux

---

Maybe pull these comments into an issue 'optimization/profiling'.