Could we move this conjunct into smallStep instead? i.e., require that every small step preserves the value number? I think that will reduce the size of the smallStep relation (and more importantly, the bigStep relation!) quite a bit.

That would be tricky, because while we do want the final Accesses to have the same ValueNumber, we don't want all intermediate instructions to have to have the same ValueNumber too, because then some crucial paths will be severed. Currently, bigStep is the same the .getASuccessor+() closure starting from instr, minus all paths that go through a barrier as defined by isBarrier(). I would hesitantly wager that this is as compact as it gets.

Actually, on second thought, maybe bigStep(i) can be optimized by having i = instr, always :) Because none of the i != instr tuples are ever needed.

That would be tricky, because while we do want the final Accesses to have the same ValueNumber, we don't want all intermediate instructions to have to have the same ValueNumber too, because then some crucial paths will be severed. Currently, bigStep is the same the .getASuccessor+() closure starting from instr, minus all paths that go through a barrier as defined by isBarrier(). I would hesitantly wager that this is as compact as it gets.

Ah, right. Yeah, I do see what you mean here.

Actually, on second thought, maybe bigStep(i) can be optimized by having i = instr, always :) Because none of the i != instr tuples are ever needed.

Yes, I think that's a good idea.

Speaking of optimizations: Currently, you're big step is defined something like:

predicate bigStep(Instruction from, Instruction to) { source(from) and smallStep*(from, to) and sink(to) }

The smallStep*(from, to) computation produces a lot of intermediate tuples that you don't really care about. We have a lot of experience in how to do this efficiently in QL, and I'd be happy to chat tomorrow about how to compute this properly. Let me just dump it here for you to read at your own pace:

The trick is to define a unary predicate to avoid producing a lot of unnecessary tuples:

// Holds if `i` can be reached starting at a source.
predicate reachedFromSource(Instruction i) {
  source(i)
  or
  exists(Instruction mid | reachedFromSource(mid) | step(mid, i))
}

// Holds if `i` can be reached starting at a source, and can eventually reach a sink.
predicate reachesSink(Instruction i) {
  reachedFromSource(i) and
  (
    sink(i)
    or
    exists(Instruction mid | reachesSink(mid) | step(i, mid))
  )
}

Then, you can use this predicate to define a smaller step relation:

predicate prunedSmallStep(Instruction from, Instruction to) {
  reachesSink(from) and reachesSink(to) and smallStep(from, to)
}

and finally, you can rewrite your bigStep as:

predicate bigStep(Instruction from, Instruction to) { source(from) and prunedSmallStep*(from, to) and sink(to) }

I have saved the best for last, implementing your proposed optimizations ^. Here are the before-and-after MRVA runs... Let's see how much of a difference it makes :)
Before: https://github.com/github/semmle-code/actions/runs/2927651707
After: https://github.com/github/semmle-code/actions/runs/2927920561

Hmm... Nope, I'm calling it. It's not worth it. I've had to inline some predicates to avoid the runaway you see in the "After", and still it's not a significant difference. This is my WIP, so it could be improved in the future: 7cc0d71

P.S. MRVA top 100 run on that WIP code: https://github.com/github/semmle-code/actions/runs/2929372003

The fact that the new code is not timing out on opencv suggest that's it's a worthwhile improvement to make. I've left a comment on your branch. We can also discuss them tomorrow if you want :)

Yeah, adding the pragma[inline] to the cartesian-product-prone predicate removed the timeout on opencv 😛 Maybe a bindingset[this] annotation would have done the trick too..? And you're right, I missed the first line from reachesSink, which might make all the difference...

So along with removing the this argument from these predicates (which might be tricky in some cases, since isBarrier does depend on this), I'll leave the exploration of this type of optimization for a follow-up issue, unless you think the performance improvements would be so drastic that they would be worth having in the initial release of this query (that is, if you think we can analyze opencv in significantly less than an hour on GitHub Actions [Locally, it's just a few minutes, fyi])

Yeah, adding the pragma[inline] to the cartesian-product-prone predicate removed the timeout on opencv 😛 Maybe a bindingset[this] annotation would have done the trick too..? And you're right, I missed the first line from reachesSink, which might make all the difference...

Yep, I think bindingset would do the same thing as a bindingset annotation implies inlining (as far as I know, at least). I also think the missing conjunct in reachesSink might make all the difference 😄, indeed.

I'm still not completely sure how to read the MRVA run output. I assume the 50 minutes of runtime on opencv is because we also have to compute the IR and all the other underlying things that the query makes use of. If it only takes a few minutes once the cached libraries are computed that sounds fine.

This is great attention to detail.

Thanks! I think there are even more special cases, that I'm parking for a follow-up issue for now (namely, the *_s variants of scanf introduced in C11).