Cleanup of the array domains

[michael-schwarz]

Currently, the partitioned array domain is

  module Expp = ExpDomain
  module Base = Lattice.Prod3 (Val) (Val) (Val)
  include Lattice.ProdSimple(Expp) (Base)

with the additional understanding that the first component is never bottom and that if it is top, all three parts of the second component have the same value.

However, this is error prone. See, e.g., #482.

Therefore, this domain should be cleaned up such that illegal values can no longer be expressed in it (Probably by switching from Lattice.ProdSimple to a custom variant type).

[michael-schwarz]

While we do this, we should also cleanup init_value and top_value:

@michael-schwarz This is starting look like a leaky abstraction. Couldn't the array domains implement it in their corresponding modules? Currently the array domain selection is repeated 5 times instead of 1.

Originally posted by @sim642 in https://github.com/goblint/analyzer/pull/577#discussion_r794263673

[michael-schwarz]

While doing this, one should also look into improving the unrolled domain to profit from information coming, e.g., from defexc.