Fix unsound query in path-sensitivity functor

[sim642]

While thinking about #148 (which has an experimental fix in the thread/path-sens branch) and comparing the mechanism with normal function call mechanism, I discovered the following unsoundness bug.

If different elements of the path-sensitive set (e.g. made path-sensitive by different mutex sets) have different points-to sets for a function pointer address, then these were previously combined with meet in PathSensitive2 when FromSpec uses the query from outside to determine possible functions:

analyzer/src/framework/constraints.ml

Lines 676 to 679 in e2a0555

	match ctx.ask (Queries.EvalFunvar e) with
	| `LvalSet ls -> Queries.LS.fold (fun ((x,_)) xs -> x::xs) ls []
	| `Bot -> []
	| _ -> Messages.bailwith ("ProcCall: Failed to evaluate function expression "^(sprint 80 (d_exp () e)))

So the intersection became empty and no functions were called at all! The right thing to do would be to join queries over all paths instead because paths are disjunct unlike multiple analyses which are conjunct.

This obviously isn't as precise as it could be because it forgets which functions may get called from which paths but there's no easy way around that right now. This is due to all the logic being on the top level at FromSpec instead of being somehow within PathSensitive2 where each path could evaluate the function variable separately and handle them only along that path. But that's another story altogether...

[michael-schwarz]

I was thinking if this causes any issues with analyses that can not answer some type of query at all and hence return Top. But since we still meet in MCP2 and only do the join in the functor(s) that add path-sensitivity, this is fine: If the result is Top along some path, then ask (which needs to be path-insensitive here) should also return Top.

Maybe add some comment on why we join here instead of meet that we do everywhere else?

So, LGTM! (Really fascinating that such bugs can be hidden for such a long time.)

[sim642]

Maybe add some comment on why we join here instead of meet that we do everywhere else?

The "everywhere else" for meet is really just MCP2 AFAIK, but I added comments to both now.

(Really fascinating that such bugs can be hidden for such a long time.)

This isn't so surprising because FromSpec doing the EvalFunvar query from outside of PathSensitive is basically the only query done at such high level (except also the witness generation ones now, but they have a specific implementation in PathSensitive). Everything else goes only through MCP2 and the activated analyses. And I guess conditional locking and their dependent function pointers aren't really used in practice, so this hasn't shown.