Partially fix unsound join for top with empty environment in ApronDomain

[jerhard]

The join in the ApronDomain behaves incorrectly when given the "Top" element for the empty environment: In that case, it returns the other element. This is because the join checks for is_bot, which checks for equality with bot, which is defined as the top element for the empty environment.
In the given problematic example, the analysis is context-insensitive and the auto-tuner selected only a subset of the variables to be tracked by the relational analysis. There, such a Top-element in an empty environment would arise, leading to an unsound analysis.

This PR changes the Apron Domain to fix this issue.

[jerhard]

When changing the ApronDomain such that bot and top are actually bot and top values of Apron, respectively, another issue appears: To maintain the precision of the multithreaded relational analysis, it seems to be required that the startstate (now RD.top ()) behaves nicely with the join, i.e., is not the absorbing element. Previously, the join: join (bot ()) x yielded x, where bot () was the Apron top of the empty environment, and was used as the startstate.
Using RD.bot () as the startstate in the relational analysis no longer works, as this results in Deadcode to be detected basically everywhere.

Maybe it would be necessary to separate the abstraction for "uninitialized state" and "unreachable state".

[michael-schwarz]

Wit the help of @jerhard we looked at it a bit on Friday and were able to narrow it down a bit.

I have dug a bit further now, the problem seems to be the following:

• The unknown [V.mutex_inits] has a value of T (which is then incorporated everywhere which causes the problem)
• The side-effect is triggered during a sync transfer function with reason Join
  • At this point, a relation value only containing global variables from st is created
  • In the examples, the list of these variables is empty, and a top T an empty environment ([]) is side-effected

This problem does not surface for other privatizations such mutex-meet-tid-*, as they do not cause side-effects on Join as they require a path-sensitive multithreading analysis and thus never need to side-effect to mutex_inits because one branch may be multi-threaded while the other is not.

[michael-schwarz]

The remaining tests that fail now are

• 46/12 (to be investigated)
• All affeq tests: The modified analysis seems to call RD.top () which was not to be called according to the documentation, as there is not environment attached. This immediately raises an excpetion.

[michael-schwarz]

The problem for 46/12 was similar:

• A local variable x that has escaped is never added to mutex_init (as this happens as a side-effect when going multi-threaded) and the escape is later
• Therefore, when looking up the value for this x in [mutex_inits], we get a T in an empty environment ([])

The fix is to not consult mutex_init for variables not in the environment, and do a blind write in escape to avoid the state becoming bot from reading bot from [x].

[michael-schwarz]

If one adds a top () = {d = Some (Matrix.empty ()); env = Environment.make [||] [||]} to affeq, all tests pass. Not sure how much sense that makes though...

[michael-schwarz]

@jerhard It seems like I cannot request your review as you opened the PR, but it would be great if you can also have a look!

[michael-schwarz]

The gobview failure is unrelated, the relational analyses are not even used with gobview.

CC @stilscher

[sim642]

This sounds like some bottom-top confusion again: if there are no globals (i.e. the environment is empty), then don't side-effect (i.e. side-effect bottom) instead of side-effecting top.
Conditionally flipping a top to bottom seems inconsistent with all other values.

[michael-schwarz]

I still think it's conceptually the right thing to do and not just a hack.
The thing is that we abuse the presence of globals in the relation as a no-overhead way to track whether one of the threads being joined possibly was in single-threaded mode.
If none of these threads was single-threaded (g_vars = []), all initial values are guaranteed to have been published and no side -effect is needed.

Does this make sense? If yes, I can write a comment detailing this reasoning.

[sim642]

The thing is that we abuse the presence of globals in the relation as a no-overhead way to track whether one of the threads being joined possibly was in single-threaded mode.

How so? We explicitly check the MustBeSingleThreaded query right before this. Prior to this, nothing is conditional on g_vars = [].

[michael-schwarz]

This is the case of branched thread creation.

• Case 0: Both ST (single-threaded), nothing to do.
• Case 1: One thread is ST, and the other one is not. After the join, Q.MustBeSingleThreaded is false, and the globals from the single-threaded side of the join need need to be published. In this case, potentially, g_vars <> []. If g_vars = [] there are no globals, and not causing a side-effect is ok.
• Case 2: Both MT, nothing should be done. In this case g_vars = []. Earlier $$\bot$$ was side-effected, now $$\top$$ would be side-effected which we need to protect against.

[sim642]

Being multi-threaded doesn't imply g_vars = [], though.

Special-casing [] to flip the lattice is not a natural extension of the behavior on all other environments. I'm afraid we're setting ourselves up for a similar issue about top-bottom confusion that we're trying to fix here.

Suppose the global unknown has a non-bottom relation $R_{\{x\}}$ (on the environment $\{x\}$) and we're side-effecting $\top_\emptyset$ (on the empty environment). What is the join of these two relations?

1. $R_{\{x\}} \sqsubseteq R_{\{x\}}$ by reflexivity.
2. $\top_\emptyset \sqsubseteq R_{\{x\}}$ because $\emptyset \subseteq \{x\}$ and $\top_\emptyset \sqsubseteq R_{\{x\}}\vert_\emptyset = \top_\emptyset$ by the definition of heterogeneous $\sqsubseteq$ (e.g. see the unassume paper) and reflexivity.

It therefore follows that $R_{\{x\}}$ itself is an upper bound of $R_{\{x\}}$ and $\top_\emptyset$. Since it's equal to one of the arguments, it's obviously also the least upper bound of the two.

So side-effecting $\top_\emptyset$ should be a no-op (and this special case is not needed) if we have the right lattice. If it isn't, then we still don't have the lattice fully right. And that is completely independent from whatever thread-modular analysis we might be doing: it's just a relational domain property.

[michael-schwarz]

Principled fix is delayed to #1380.

[sim642]

Is this not just a workaround for the actual bug? Seems like escapes should also contribute to mutex_inits.

BasePriv.PerMutexPrivBase and BasePriv.PerMutexMeetTIDPriv side-effect escapes to mutex_inits at least.

[michael-schwarz]

Yes, in the base priv this is all not problematic, as it is non-relational. Here, this all becomes fragile, and I think for now we are wise to avoid the set of variables at global unknowns not only shrinking (due to decreasing protection) but also increasing in non-obvious matters due to escapes also being tracked associated with mutex_inits which is supposed to abstract the state at program start. Maybe this is also something for #1380.

[stilscher]

The gobview failure is unrelated, the relational analyses are not even used with gobview.

CC @stilscher

This is because with goblint/gobview#41 changes were made to GobView that rely on the respective changes in Goblint (#1360). Both PRs were already merged, but this PR is based on an older version that does not include the Goblint changes yet. Merging with the master branch should be sufficient to fix it.

[michael-schwarz]

Merging with the master branch should be sufficient to fix it.

It does not.

[michael-schwarz]

@jerhard @sim642: Anyone opposed to merging this as a stop-gap to at least be sound for the problematic cases reported here and enable experiments for my thesis until we have time to do #1380?

@stilscher: With the gobview things, I have no idea how to debug but it should be completely orthogonal: Nothing is touched here that is even used in JS builds.

[sim642]

With the gobview things, I have no idea how to debug but it should be completely orthogonal: Nothing is touched here that is even used in JS builds.

I haven't looked, but it might just be crashing during some initialization. For example let is_top = equal (top ()) would evaluate top () at initialization time, even if is_top is never called, but there's no Apron JS stubs. I think we don't explicitly disable Apron in JSOO builds, it works as long no calls to Apron C/JS stubs are made.

[michael-schwarz]

For example let is_top = equal (top ())

Right on the money! Together with @stilscher we were able to fix it and it was exactly this. I didn't think that the eta expansion was needed, as it was also not done for bot () but was somehow unproblematic there.

[sim642]

I didn't think that the eta expansion was needed, as it was also not done for bot () but was somehow unproblematic there.

That's odd indeed. By that logic it should've already been failing before. So maybe there's something else going on, like one of them actually getting called from elsewhere during initialization and the other one not.

[michael-schwarz]

I think it could also be an artifact of compilation order or something the like. Given that it works now, I'd suggest to go ahead and merge it.

[sim642]

Since this isn't the principled fix but still leaves us with a domain that clearly violates basic lattice properties, I think this should go through an sv-benchmarks run. It's not exactly obvious that this cannot expose some issue elsewhere by fixing this one particular sv-benchmark with some special conf.
Independently, this branch can still be used for some other benchmarks that it's needed for.

[michael-schwarz]

I think this should go through an sv-benchmarks run.

Do you currently have capacity in Tartu? Our machines are quite loaded with SOAP benchmarks for the past few weeks.

[sim642]

Do you currently have capacity in Tartu? Our machines are quite loaded with SOAP benchmarks for the past few weeks.

I don't have immediately because I'm running SV-COMP 2024 tools on Concrat with 2h time limit, which is going to take a while...
SOAP deadline is in two days though, so it's not a big delay.

[michael-schwarz]

I started a run on server02 now.

[michael-schwarz]

The results do not differ much from the last run we did on sv-comp in November (d629d14) which is our official sv-comp release.

The new numbers are:

• +2 tasks on no-data-race
• +204 tasks on unreach-call
• +12 tasks on no-overflow
• -26 tasks on mem-safety
• +/- 0 tasks on mem-cleanup
• • 73 tasks on termination

There are four new unsoundnesses (#1385) that are however also present on master. I will also start a diff with the current master to see which of these changes are actually due to this PR, but I think it at least doesn't like this is a huge regression for now.

[sim642]

#1385 lists two of the unsound cases being from list_search, which is precisely what this PR is supposed to fix (#1302), but looks like doesn't.

[michael-schwarz]

Good catch! It looks like it fixes only the issue where both branches are dead that the regression test also addresses.

[michael-schwarz]

W.r.t current master, the only changes with this PR are for unreach_call:

unreach_call.zip where 5 tasks fluctuate between TIMEOUT 900s / StackOverflow and Unknown after 880s

Runtimes remain consistent.

I would suggest to merge this now, as it fixes known soundness bugs (the one added to the regression tests) and does not deteriorate SV-COMP results.