Frontend: local mutex handles are unsupported

[leventeBajczi]

IllegalStateException: Local mutex handles are not supported: <var>

155 failures over 61 distinct tasks in the full SV-COMP run of Theta 8.0.0 (--portfolio COMPLEX27, 900s, 15GB, 2 cores).

Example log line:

Frontend failed! (hu.bme.mit.theta.xcfa.passes.CLibraryFunctionsPass.checkMutexDecl(CLibraryFunctionsPass.kt:286), java.lang.IllegalStateException: Local mutex handles are not supported: my_callback::data)

All 61 tasks

c/goblint-regression/03-practical_15-exit_problems.c
c/goblint-regression/04-mutex_03-munge_rc.c
c/goblint-regression/04-mutex_04-munge_nr.c
c/goblint-regression/04-mutex_09-ptrmunge_rc.c
c/goblint-regression/04-mutex_10-ptrmunge_nr.c
c/goblint-regression/04-mutex_23-sound_unlock.c
c/goblint-regression/04-mutex_24-sound_lock.c
c/goblint-regression/05-lval_ls_01-idx_rc.c
c/goblint-regression/05-lval_ls_02-idx_nr.c
c/goblint-regression/05-lval_ls_03-fld_rc.c
c/goblint-regression/05-lval_ls_09-idxsense_rc.c
c/goblint-regression/05-lval_ls_11-fldsense_rc.c
c/goblint-regression/05-lval_ls_12-fldsense_nr.c
c/goblint-regression/05-lval_ls_13-idxunknown_lock.c
c/goblint-regression/05-lval_ls_16-idxunknown_unlock.c
c/goblint-regression/06-symbeq_02-funloop_norace.c
c/goblint-regression/06-symbeq_03-funloop_simple.c
c/goblint-regression/06-symbeq_04-funloop_hard1.c
c/goblint-regression/06-symbeq_05-funloop_hard2.c
c/goblint-regression/06-symbeq_06-tricky_address1.c
c/goblint-regression/06-symbeq_07-tricky_address2.c
c/goblint-regression/06-symbeq_08-tricky_address3.c
c/goblint-regression/06-symbeq_09-tricky_address4.c
c/goblint-regression/06-symbeq_10-equ_rc.c
c/goblint-regression/06-symbeq_11-equ_nr.c
c/goblint-regression/06-symbeq_13-equ_proc_nr.c
c/goblint-regression/06-symbeq_14-list_entry_rc.i
c/goblint-regression/06-symbeq_15-list_entry_nr.i
c/goblint-regression/06-symbeq_23-idxsense_nr.c
c/goblint-regression/09-regions_16-arrayloop_rc.i
c/goblint-regression/09-regions_17-arrayloop_nr.i
c/goblint-regression/13-privatized_68-pfscan_protected_loop_minimal_interval_true.c
c/goblint-regression/28-race_reach_03-munge_racing.i
c/goblint-regression/28-race_reach_04-munge_racefree.i
c/goblint-regression/28-race_reach_09-ptrmunge_racing.i
c/goblint-regression/28-race_reach_10-ptrmunge_racefree.i
c/goblint-regression/28-race_reach_70-funloop_racefree.i
c/goblint-regression/28-race_reach_71-funloop_racing.i
c/goblint-regression/28-race_reach_72-funloop_hard_racing.i
c/goblint-regression/28-race_reach_73-funloop_hard_racefree.i
c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
c/goblint-regression/28-race_reach_75-tricky_address2_racefree.i
c/goblint-regression/28-race_reach_76-tricky_address3_racefree.i
c/goblint-regression/28-race_reach_77-tricky_address4_racing.i
c/goblint-regression/28-race_reach_78-equ_racing.i
c/goblint-regression/28-race_reach_79-equ_racefree.i
c/ldv-races/race-2_1-container_of.i
c/ldv-races/race-2_3-container_of.i
c/ldv-races/race-2_3b-container_of.i
c/ldv-races/race-2_4-container_of.i
c/ldv-races/race-2_4b-container_of.i
c/ldv-races/race-2_5-container_of.i
c/ldv-races/race-2_5b-container_of.i
c/ldv-races/race-3_1-container_of-global.i
c/pthread-complex/bounded_buffer.i
c/pthread-divine/barrier_2t.i
c/pthread-divine/barrier_3t.i
c/pthread-divine/one_time_barrier_2t.i
c/pthread-divine/one_time_barrier_3t.i
c/pthread-divine/one_time_barrier_twice_2t.i
c/pthread-divine/one_time_barrier_twice_3t.i

[leventeBajczi]

Notes from an automated triage (runs and code reading on master, before #579 was merged — re-check which of these still fail):

• Group 1, 16 tasks (05-lval_ls_*, 06-symbeq_10/11/13/23, 09-regions_16/17, 28-race_reach_78/79): getParam maps &m[k]/&s.f (k ≠ 0) to a fresh m_k that is never added to the globals, so checkMutexDecl rejects it as local — a plain bug (see also Frontend: pthread handle base is not a reference variable #561), since PthreadArrayHandleUnrollPass unrolls mutex-array loops precisely to use this path. Registering the handle as a global (avoiding clashes with a user global m_1) should fix ~9 of them outright.
• Group 2, 45 tasks, reach the mutex through a pointer: constant addresses at each call site (resolvable by inlining + constant propagation before lowering), a nondet choice among a few globals (points-to case split), or stack/heap objects via thread arguments or container_of (need address-valued identity). This group is effectively the symptom list for Non-declaration-based mutex tracking #538.

---

Generated by Claude Code