DataFlow: Support stateless isSink in StateConfigSigs

[MathiasVP]

Sometimes it's necessary to have a state-based configuration to define the correct isBarrier, but if data then does manage to reach a sink, any state should be accepted. Prior to this PR, the only way to prevent a cartesian product would be to do something like:

module PruningConfig implements ConfigSig {
  predicate isSource(Node source) {
    exists(MyState state | isSourceImpl(source, state))
  }

  predicate isSink(Node sink) { ... }
}

module PruningFlow = Global<PruningConfig>;

FlowState viableStateForSink(Node sink) {
  exists(PruningFlow::PathNode pSource, PruningFlow::PathNode pSink |
    PruningFlow::flowPath(pSource, pSink) and
    pSink.getNode() = sink and
    isSourceImpl(pSource.getNode(), result)
  )
}

module RealConfig implements StateConfigSig {
  class FlowState = MyState

  predicate isSource(Node source, FlowState state) { isSourceImpl(source, state) }

  predicate isSink(Node sink, FlowState state) {
    ... and state = viableStateForSink(sink) // <-- to prevent CP with all flow states.
  }

  predicate isBarrier(Node barrier, FlowState state) { ... }
}

because there was no isSink/1 on StateConfigSig. With this PR we can now do:

module RealConfig implements StateConfigSig {
  predicate isSource(Node source, FlowState state) { ... }

  predicate isSink(Node sink) { ... }

  predicate isBarrier(Node barrier, FlowState state) { ... }
}

with no PruningFlow mess.

cc @aschackmull I hope this isn't too controversial?

[aschackmull]

This is going to need some changes.

[MathiasVP]

@aschackmull I've rebased the PR now that #13863 has been merged (🎉).

[MathiasVP]

Hmmm @aschackmull I think adding the additional conjuncts to sinkNode breaks in the use of sinkNode in the partial flow case 😭. I've implemented one possible fix in 50f5c4d.

[aschackmull]

We can make another predicate to do a best-effort cartesian approximation for the reverse flow exploration case - this doesn't have to be extremely performant as it's just a debugging tool that'll often be restricted to specific sources/sinks anyway.
Add the following just below the relevantState predicate:

private predicate revSinkNode(NodeEx node, FlowState state) {
  sinkNodeWithState(node, state)
  or
  Config::isSink(node.asNode()) and
  relevantState(state) and
  not fullBarrier(node) and
  not stateBarrier(node, state)
}

and use it in the two places below.

[MathiasVP]

That makes sense. Thanks! Fixed in 981f675.

[aschackmull]

LGTM now.

[MathiasVP]

Hm, it looks like Java's DCA run isn't super happy about these changes. I'll investigate!

[aschackmull]

Hm, it looks like Java's DCA run isn't super happy about these changes. I'll investigate!

It might very well be unrelated to this PR - I think we're seeing a lot of OOM kills in DCA at the moment for other reasons.

[MathiasVP]

Hm, it looks like Java's DCA run isn't super happy about these changes. I'll investigate!

It might very well be unrelated to this PR - I think we're seeing a lot of OOM kills in DCA at the moment for other reasons.

Ah, thanks for the heads up. Stage timings also seem to blame a bunch of non-dataflow related queries so it's probably a fluke. In any case, I've started a separate run for Java, and I'll do a couple of local evaluations to make sure there's nothing wrong

[MathiasVP]

FWIW, none of the projects that reported a slowdown on DCA seems to be slowing down locally.

[MathiasVP]

Java has a bunch of OOMs, but this PR doesn't seem to contribute to any more of those OOMs. And since Java (nor any other language) isn't actually using this new feature yet this doesn't seem like it should block this PR. I've also verified that no bad joins are introduced.