Witness invariants for arrays and principled handling of unknown indices

[sim642]

Closes #1044.

Turns out all_array_index_exp was a misnomer and that has bit us in the past:

analyzer/src/cdomains/arrayDomain.ml

Lines 428 to 433 in 997f9ae

	if i = Some MyCFG.all_array_index_exp then
	(assert !Goblintutil.global_initialization; (* just joining with xm here assumes that all values will be set, which is guaranteed during inits *)
	(* the join is needed here! see e.g 30/04 *)
	let o = match x with Partitioned (_, (_, xm, _)) -> xm | Joint v -> v in
	let r = Val.join o a in
	Joint r)

That is because exp.fast_global_inits converts

int g[10] = {1, 2, 3};

into

g[all_array_index_exp] = 1;
g[all_array_index_exp] = 2;
g[all_array_index_exp] = 3;

But it doesn't actually mean assigning to all indices, but rather assigning to some indices. Thus the weak update with join.

For the Goblint-specific array invariants, we actually want all indices and thus a strong update. Soundness of unassume is still ensured by a final join of the environments, but when unassuming g[all_index] >= 0 && g[all_index] <= 3 we don't want the two subinvariants to be joined, rather acting as refinements which allow complete overwriting.

Thus this introduces any_index_exp, which is used for exp.fast_global_inits and all kinds of unknown_exp or "unknown" indices, to make everything consistent. And all_index_exp, which is used for array invariants.