Questionable invariants in SV-COMP 2025 witnesses

[sim642]

While working on witness IDE integration, @karoliineh has looked at some of our witness invariants, which has revealed some questionable ones:

• Seemingly pointless reflexive equality:

  - invariant:
      type: loop_invariant
      location:
        file_name: ../../sv-benchmarks/c/libvsync/arraylock.i
        line: 5446
        column: 5
        function: arraylock_init
      value: flags == flags
      format: c_expression
  

  This is actually a result of a scoping issue: flags is both a local variable in the function and a global variable. Internally one of them is renamed to something like flags___0, but witness invariant generation translates back to original names, which both happen to be the same.
  Thus, this requires a more complicated scope check in terms of original names of variables to check for possible shadowing in the original program.

• Seemingly pointless self-relation:

  - invariant:
      type: loop_invariant
      location:
        file_name: ../../sv-benchmarks/c/pthread-divine/barrier_2t.i
        line: 771
        column: 5
        function: worker_fn
      value: (long long )i - (long long )i >= 0LL
      format: c_expression
  

  This is similar to the previous one, but here both is are local variables in the same scope.
  Thus, the check also needs to account for local multiple variables with the same name, possibly interacting with block scopes.

• Equality with string literal:

  - invariant:
      type: loop_invariant
      location:
        file_name: ../../sv-benchmarks/c/coreutils-v8.31/comm_3args_ok.c
        line: 89784
        column: 5
        function: emit_ancillary_info_350238
      value: '"Multi-call invocation" == infomap[1].node'
      format: c_expression
  

  I think our address domain stores the string literal as StrPtr, but as a C expression this perhaps isn't the proper way to check for string equality (comparing addresses of a literal).

• Possibly excessive function pointer casts: (our test also in sv-benchmarks)

  - invariant:
      type: loop_invariant
      location:
        file_name: tests/regression/28-race_reach/19-callback_racing.c
        file_hash: a1ce836bced7c094813d29229908add6bb9373b2656bef1a46560c4458852342
        line: 9
        column: 3
        function: foo
      value: callback == (int (*)())(& bar)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: tests/regression/28-race_reach/19-callback_racing.c
        file_hash: a1ce836bced7c094813d29229908add6bb9373b2656bef1a46560c4458852342
        line: 9
        column: 3
        function: foo
      value: (void *)callback == (void *)(& bar)
      format: c_expression
  

  The first invariant is from var_eq, the second from base. In both cases casts are inserted because callback has type int (*)(), but &bar has type int (*)(void). Both are declared with () arguments, but in function definition this apparently means (void).
  It would probably be good to fix our tests (with more precise function pointer types) and resubmit to sv-benchmarks.
  However, independently we could maybe avoid inserting the casts because the function types should be compatible in some sense, just not identical.

• Anonymous struct field access with CIL offset:

    - invariant:
        type: loop_invariant
        location:
          file_name: ../../sv-benchmarks/c/intel-tdx-module/tdh_phymem_page_reclaim__requirement__invalid_state_pamt_metadata_havoc_object.i
          line: 2362
          column: 5
          function: __VERIFIER_nondet_array_1D_struct_kot_entry_s
        value: tdcs_fv.virt_msrs.virt_ia32_vmx_cr4_fixed1.__annonCompField10.cet ==
          0ULL
        format: c_expression
  

[karoliineh]

The following still needs fixing:
[Warning][Witness] invariant unconfirmed: applet_opts == (char const *)"lwmcL" (../../sv-benchmarks/c/busybox-1.22.0/wc-2.i:2458:3)

It's from one of the 7/31 tasks from SoftwareSystems-Other-ReachSafety that we are able to verify, and this one (high-value) result is unconfirmed due to this one invariant.

[sim642]

I fixed it directly on master now.