`Mutex-Meet-TID` without clusters more precise than approach with clusters

[michael-schwarz]

For the following small program:

#include<pthread.h>
pthread_mutex_t c;
int d, e, f;

void b(void* arg);

void main(int argc, char *argv) {
  pthread_t t;
  e = pthread_create(&t, 0, b, &f);
  pthread_mutex_lock(&c);
  d++;
  pthread_mutex_unlock(&c);
  pthread_mutex_lock(&c);
}

./goblint --conf conf/traces-rel.json --set ana.activated[+] threadJoins --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 1.c --sets exp.relation.prec-dump cluster.prec
./goblint --conf conf/traces-rel.json --set ana.activated[+] threadJoins --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid 1.c --sets exp.relation.prec-dump tid.prec
./apronPrecCompare cluster.prec tid.prec

we get

Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPrivTID(cluster12,join)) less precise than Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPrivTID(no-clusters,join)) (equal: 6, more precise: 0, less precise: 1, incomparable: 0, total: 7)

While such effects may happen due to W/N, it seems odd that it can be observed on such small programs. b having no implementation available seems crucial for this to happen, so it may be invalidation related somehow...

Detailed comparison

``` Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPrivTID(no-clusters,join)): [|d-1.>=0; -d+1.>=0; -d+e+2147483649.>=0; d+e+2147483647.>=0; e+2147483648.>=0; -d-e+2147483648.>=0; d-e+2147483646.>=0; -e+2147483647.>=0; -d+f+2147483649.>=0; d+f+2147483647.>=0; -e+f+2147483648.>=0; e+f+2147483648.>=0; f+2147483648.>=0; -d-f+2147483648.>=0; d-f+2147483646.>=0; -e-f+2147483647.>=0; e-f+2147483648.>=0; -f+2147483647.>=0|] (env: [|0> __daylight:int; 1> __timezone:int; 2> argc#996:int; 3> d:int; 4> daylight:int; 5> e:int; 6> f:int; 7> timezone:int|]) more precise than Apron Octagon(domain: Apron Octagon, privatization: PerMutexMeetPrivTID(cluster12,join)): [|d-1.>=0; -d+1.>=0; -d+e+2147483649.>=0; d+e+2147483647.>=0; e+2147483648.>=0; -d-e+2147483648.>=0; d-e+2147483646.>=0; -e+2147483647.>=0; -d+f+2147483649.>=0; d+f+2147483647.>=0; -e+f+4294967295.>=0; e+f+4294967296.>=0; f+2147483648.>=0; -d-f+2147483648.>=0; d-f+2147483646.>=0; -e-f+4294967294.>=0; e-f+4294967295.>=0; -f+2147483647.>=0|] (env: [|0> __daylight:int; 1> __timezone:int; 2> argc#996:int; 3> d:int; 4> daylight:int; 5> e:int; 6> f:int; 7> timezone:int|]) reverse diff: -e+f+2147483648.>=0, -e-f+2147483647.>=0, e+f+2147483648.>=0, e-f+2147483648.>=0 ```

[sim642]

b having no implementation available seems crucial for this to happen, so it may be invalidation related somehow...

On master we just crash:

analyzer/src/analyses/apron/relationAnalysis.apron.ml

Lines 676 to 679 in b129fab

	| exception Not_found ->
	(* Unknown functions *)
	(* TODO: do something like base? *)
	failwith "relation.threadenter: unknown function"

[michael-schwarz]

Yeah, I did the (* TODO: do something like base? *) for my evaluation.

[michael-schwarz]

The issue seems unrelated to widening, it happens with widen = join too.

[michael-schwarz]

Relying on YAML might make debugging easier. There we get

./goblint --conf conf/traces-rel.json --set ana.activated[+] threadJoins --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid 1.c --sets exp.relation.prec-dump cluster.prec --html --enable witness.yaml.enabled --set witness.yaml.path 1.yml

./goblint --conf conf/traces-rel.json --set ana.activated[+] threadJoins --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 1.c --set witness.yaml.validate 1.yml

[Warning][Witness] invariant unconfirmed: (2147483648LL + (long long )e) + (long long )f >= 0LL (1.c:14:1)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )e) + (long long )f >= 0LL (1.c:14:1)
[Warning][Witness] invariant unconfirmed: (2147483648LL + (long long )e) - (long long )f >= 0LL (1.c:14:1)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )e) - (long long )f >= 0LL (1.c:14:1)

[Info][Witness] witness validation summary:
confirmed: 32
unconfirmed: 4

The invariants provided here look slightly dubious to me as to whether they actually hold.

[michael-schwarz]

It seems to hold here as e is guaranteed to be zero, but I have a feeling it holds for the wrong reasons.

[michael-schwarz]

Especially since we say

[Info][Imprecise] Invalidating expressions: & e (1.c:11:3-11:35)

[michael-schwarz]

It appears that the case for an unknown thread was missing the following snippet which the other case has:

    (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
    Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
    sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
    EnterMultithreaded events only execute after threadenter and threadspawn. *)
    if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
      ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st);

Otherwise, the invalidation of e seems to have not been properly carried over to the global invariant.

[michael-schwarz]

Completed in #1417

[michael-schwarz]

There seems to be another instance of this, also with the same program.