Relational: Use same invalidation strategy as base

[michael-schwarz]

Closes #1535

[michael-schwarz]

I don't get what goes wrong in the CI here, it works locally.
The reason seems to be non-unique test names.

[sim642]

Why is this moved out? Base only does it for non-unknown thread functions.

[michael-schwarz]

The logic of why it is needed is the same here as it is for the case where a known thread is created: One should not go into multi-threaded mode without notifying the privatization that this switch happened to ensure everything that should be published is published.

Maybe base has some reason this can be avoided, but I'm not really sure why that should be the case. We may want to make an issue to investigate this.

[michael-schwarz]

Also see the last few comments in #1551

[michael-schwarz]

#1551 (comment)

[sim642]

The one test in this PR doesn't cover this, does it?

I tried the very simple thing of creating a thread from unknown function pointer and that seems to work with base. That's because threadflag analysis emits the EnterMultiThreaded event which is handled by base (and relational).
The comment for this hack is about the globals values that get used when analyzing the created thread. For an unknown function pointer, there's no thread body to analyze anyway, so it's not clear to me when it would make a difference.

[michael-schwarz]

The test covers it in some sense. We mean to invalidate e and output

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

But this invalidation does not take and we still claim to be able to prove things about e.

[michael-schwarz]

Edit: That case is listed in the linked issue.

[sim642]

Do you mean this?

#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);
}

Where or what are we claiming to prove about e? There aren't any assertions. Can you add it as a test?

I traced sol and sol2 on it and what this changes is that we no longer have -e+2147483647.>=0, e+2147483648.>=0 and all derived octagon constraints from that. But these are just type bounds, so they shouldn't be unsound to begin with.

The point of this PR is to unify logic between base and relation analyses, but this move introduces a new difference. If the old place is really wrong, then we should also fix it in base.
I want to avoid another issue like #1535 down the line where the inconsistency comes up and there's no understanding of why they're different.

[michael-schwarz]

Sure, I guess I should have linked to this comment: #1551 (comment)

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.

These invariants exploit that e is supposedly 0, even thoughe and f have been invalidated.