Make threadflag/thread analysis path-sensitive

[sim642]

The thread join support from PR #137 didn't improve our results on SV-COMP's NoDataRace benchmarks as much as expected. At least some of them create and join threads conditionally. This currently renders the added thread join support useless because joins in the thread analyses lose the necessary precision. Making threadflag and maybe even thread analysis path-sensitive would help with that.

I made a quick experiment but turns out this is problematic and cannot currently easily be done. The issue is the S.context d call here:

analyzer/src/framework/constraints.ml

Lines 566 to 579 in 9fd3ccc

	and spawn lval f args =
	(* TODO: adjust ctx node/edge? *)
	let d = S.threadenter ctx lval f args in
	let c = S.context d in
	let rec fctx =
	{ ctx with
	ask = fquery
	; local = d
	}
	and fquery x = S.query fctx x
	in
	r := S.threadspawn ctx lval f args fctx :: !r;
	if not full_context then sidel (FunctionEntry f, c) d;
	ignore (getl (Function f, c))

If d is a path-sensitivity domain set that happens to contain more than one path, then S.context fails because it can just return a single context. It might be necessary to rework this mechanism to be more like our previous function call mechanism where enter returns a list, not a single element, which is then handled in FromSpec to apply S.context per-element.
(That in itself is a weird mechanism because the path-sensitivity handling isn't localized to the corresponding lifter but throughout the analysis specification hierarchy.)

I have my doubts about being able to achieve this by SV-COMP 2021.

[sim642]

As I said in #155, there's an experimental fix in thread/path-sens branch.

[sim642]

Key parts of the experiment have now been cherry-picked to traces branch since the threadenter path-sensitivity crash is also possible with mutex paths. The SV-COMP examples and configuration wasn't cherry-picked.

[sim642]

Since the implementation parts already reached master via #183, then I've also cherry-picked the rest of thread/path-sens, which is the regression tests for this. Based on these, the feature works, so I'm closing the issue.