Support arrays with standard invariants

[viktormalik]

When --std-invariants is set, invariants are computed for the loop head (i.e. contain the pre-loop value in addition to the loop-back values). This is not convenient for arrays since they are typically uninitialized and only get initialized inside a loop. Including the pre-loop array value would add the nondet value to the invariant, making the entire invariant (especially the one for the initializer loop) nondet.

This change prohibits usage of standard invariants for the array domain. Most of the changes are done in the template generator which:

• does not generate aux_expr for array var specs,
• always passes post_renaming_map (instead of aux_renaming_map) to the array domain and its inner domains.

This is especially necessary for SV-COMP where we use --k-induction which sets --std-invariants, too.

[viktormalik]

@peterschrammel I'm not very familiar with the purpose and working of standard invariants, do you think that it will be fine mixing standard and non-standard invariants?

cc @FrNecas who may also know something about this.

[peterschrammel]

purpose and working of standard invariants

The purpose is to output invariants that include the state on first entering the loop head, which is commonly considered as the definition of an invariant at the loop head (but is not required in our SSA encoding to perform induction proofs).

do you think that it will be fine mixing standard and non-standard invariants?

I don't see any problem with that.

Btw, I've pushed the graphml fix onto 2ls-prerequisites-cbmc-5.61.0.

[FrNecas]

Thanks for adding the graphml fix. It would be nice to also update the submodule (perhaps in this PR?)

Btw @peterschrammel do you happen to know if there is a way to make fscanf "result" nondet with CBMC? There is a new no-overflows subcategory with calls like:

    data = 0LL;
    fscanf (stdin, "%" "l" "d", &data);
    {
        int64_t result = data + 1;
...

which can overflow. CBMC makes only the return value of fscanf nondet from what I've noticed, hence we consider data to still be 0. It should be possible to somehow patch this in 2LS, I was just wondering if you see a way to make it work with CBMC.