Functions are called after false statement

[matanl]

I noticed that when I run something like this with some_fuction I defined:
exists(1=2 and some_function())
some_function is called even though 1 is clearly not equal to 2 and I'd think it would stop evaluating at that moment.
Is that an expected behavior? Am I missing something?

[smowton]

Your problem is that CodeQL uses a bottom-up evaluation model: to evaluate exists(1 = 2 and some_predicate()), it will evaluate 1 = 2, then some_predicate(), then intersect the two. Similarly if you had exists(Something s | f(s) and g(s)), then generally CodeQL might find all Something s for which f(s) holds, then all those for which g(s) holds, and then intersect them. The optimiser might notice that f(s) is only used in contexts where g(s) holds and push the additional constraint ... and g(s) inside f or vice versa, but you shouldn't generally assume it will. If it's vital for the efficiency of g that it only considers those s where the other predicate already holds, then you should explicitly push the side-condition ...and f(s) inside g.

If you find you need to do that a lot, a good way to go about is defining class SomethingWithF extends Something { SomethingWithF() { f(this) } }, then when you define predicate g(SomethingWithF s) { ... } that's like giving the ...and f(s) side-condition.

In this particular case it seems likely you're trying to disable some predicate by adding ... and 1 = 2, similarly to writing if(0) { ... } around a block you want to disable? If so you simply have to comment the code you want to replace, and replace it by none() rather than 1 = 2, the standard CodeQL way to say 'nothing matches'.

[matanl]

Thanks a lot for the answer!

I actually used 1=2 as an example but g(s) is more representative of my problem. In my case f(s) is a fairly straightforward predicate while g(s) does some heavy liftining I would like it to do only if f(s) holds.

If I add and f(s) inside g wouldn't the same problem still exist? The bottom-up evaluation would evaluate every formula inside g. in this case and f(s) wouldn't prevent the heavy liftining, or is that only the case witin an exists? I could beistaken but I think I ran into this behavior even when I didn't use exists

[smowton]

exists definitely doesn't have any bearing either way. Generally speaking the problem of what constraints to apply in what order is called join ordering, and in CodeQL there are idiomatic ways to give useful hints, and pragma directives to force particular orderings.

For example, if g looked like g(Expr e) { exists(Call c | c.getMethod().hasName("test") and c.getAnArgument() = e and f(e)), then CodeQL could choose to build a set of all the calls to a method named test, take all their arguments, and only then check whether any of those arguments match f, or it could approach things in the reverse direction, taking those expressions that match f, then checking whether they are arguments to any call, and then finally whether those calls call an appropriately named method.

Using a class SomethingWithF is a pretty strong hint that the parameter has been restricted and is a good place to start computing the result. If that's not enough, the pragmas only_bind_into and only_bind_out (https://codeql.github.com/docs/ql-language-reference/annotations/#pragma-only-bind-out) are hard constraints on the possible orderings.

For more concrete advice, I suggest you should paste a sample of the 'heavy' predicate that currently takes a long time to compute.