Incorrect witness invariants found by Ultimate

[sim642]

Ultimate revealed some incorrect witness invariants that we output: https://struebli.informatik.uni-freiburg.de/logs/concurrency-witnesses/20240205-105808-concurrency-witnesses-d8006e4be6-M/tabledef.table.html#/table?sort=1_Violation_4,asc&filter=1(4*Violation*(value(invariant))).

• c/weaver/chl-collitem-subst.wvr.c, line 107. We state invariant b != 0 before assume_abort_if_not(b <= 0 || a >= b - 2147483648);, probably due to CIL transforming the logical expression and giving some internal branch nodes the same location. (Fix first in location synthesizing cil#166)
• Ultimate's counterexample has non-0/1 value for _Bool variable. Maybe that is valid?
  • If these are for _Bool variables, we shouldn't emit them at all. (Fix enums domain to not emit witness invariants for top booleans #1436)
  • c/weaver/chl-exp-term-subst.wvr.c, line 68. We state invariant sort_label_is_null_1 == (_Bool)0 || sort_label_is_null_1 == (_Bool)1, but Ultimate's counterexample has value 2.
  • c/weaver/test-easy8.wvr.c, line 70. Counterexample has c=3.
  • c/weaver/parallel-barrier.wvr.c, line 193. Counterexample f1_2=6, f1_8=4, f2_3=2, f2_9=8.
  • c/pthread-wmm/rfi002_power.oepc_power.opt_pso.oepc_pso.opt_rmo.oepc_rmo.opt.i, line 839. Counterexample weak$$choice0=3.
  • TODO: maybe this is only for uninitialized variables?
• c/pthread/fib_safe-5.i, line 721. We state the invariant 0 <= cur && cur <= 0 as a flow-insensitive invariant. Somehow interval sets get enabled (SV-COMP autotuner spuriously enables all integer domains #1472), they compute larger-than-type ranges and yield unsound truncated invariants (Interval sets are unsound due to larger-than-type ranges #1473).
• Mutex-meet invariants don't account for MUTEX_INITS. (bd329e1).
  • c/weaver/test-easy11.wvr.c, line 74. With mutex-meet with state 2147473648LL + (long long) X) + (long long) Y >= 0LL, 10000 <= Y and Y != 0. Counterexample X=-2147473649, Y=0.
  • c/weaver/popl20-simple-queue.wvr.c, line 81. Invariant (4294967295LL + (long long) back) + (long long) front >= 0LL. Counterexample back=-2147483648, front=-2147483648.
    • c/weaver/popl20-send-receive-alt.wvr.c
    • c/weaver/popl20-queue-add-2.wvr.c
    • c/weaver/popl20-more-queue-add-2-nl.wvr.c
  • c/goblint-regression/13-privatized_52-refine-protected-loop2-small_true.i, line 703. Invariant (!multithreaded || (A_locked || (g == 999))). Counterexample g=0.
    • c/goblint-regression/13-privatized_45-traces-per-global-and-current-lock-mine-incomparable_true.i
    • c/goblint-regression/13-privatized_33-traces-v-matters_true.i
  • c/pthread-atomic/time_var_mutex.i, line 721. Invariant (!multithreaded || (m_inode_locked || ((((0 <= busy) && (busy <= 1)) && (inode == 1)) && ((busy == 0) || (busy == 1)))))). Counterexample block=0, busy=0, inode=0.
• ...