How to stop recursion from recursing

[Sixelayo]

I was writting an overly messy request trying to find the latest assignment to a VariableAccess in cpp (I know it's impossible, just limiting my request to variable and references for now), I didn't understood something so I tried debugging over a smaller example, but then I felt like I was missing understanding of basic concepts.

The pattern that I'm trying to fix is similar to this one (I know this is a pointless request, it's juste for debugging and understanding purposes):

bindingset[i]
int rec(int i){
    result = i
    or 
    exists(int stop |
        stop = 20
        and i < stop
        and result=rec(i+1)
    )
}

from int i
where i in [1..5]
select rec(i)

I expected this request to be valid and return all integer from 1 to 19, but it fails because :
There is a recursive cycle of relations that must be inlined, which is impossible: wip5bb::rec -> wip5bb::rec
Does this mean CodeQL doesn't use lazy evaluation ? Because if there are constraint on an argument of a recursive predicate then I don't understand why is code QL looking at the recursive predicate before applying constraint to its arguments. In the request above, there's the condition that "i<20" so if i>=20 there's no reason to evaluate the predicate rec. From my perspective I can use a pen paper to run this request with no issue, so there's definitly something that I truly don't understand at all.

Or maybe the thing I don't understand is the exists predicates when there's a result inside ? I expected that if no temporary variables can satisty the condition then the result in exists is just ignored because there's no coherent behavior definition otherwise. (if exists doesn't hold then it's impossible that the inside of the exists affect the outside of the exists predicate)

(To give real context : I'm looking if a "path" from an assigned value to the variable access without encountering another assignment to that variable exists, fot that I use Node from DataFlowUtil and localFlowStep. I managed to write a somewhat working request with getAPredecessor+ / dominates / postDominates predicates but it wasn't working for some conditional branching case. There are probably many other mistakes in what I've wrote because my actual request doesn't fail and it seems like my exists predicate alway holds but I can't move forward if I don't understand basic recursion)

[aibaars]

QL is a form of datalog and uses a bottom-up evaluation strategy. You might want to have a look at https://codeql.github.com/docs/ql-language-reference/evaluation-of-ql-programs/ .

QL evaluates a predicate into a set of tuples (a sort of table). QL requires all its results to be of finite size, and to achieve this it has a rule that all variable should be "bound". For example the expression result = i does not limit result in any way and would mean that the int rec(int) predicate would evaluate to pairs like (x,x) for any integer value x. The QL compiler complains about that. You can tell the compiler to stop complaining by using the bindingset annotation, however, that annotation does not work for recursive predicates. Also in this case the compiler was right, perhaps you meant result = i and i = 0 to define the base case of the recursion. With that change the compiler no longer complains, however, it goes into an infinite recursion. Not sure why it didn't detect this, it would be great if it told that the rec predicate was still infinite. I think it is iterating through all negative numbers, which are all smaller than 20 so the stop condition doesn't do anything. Most likely you meant the recursive call to be result = rec(i - 1)

[Sixelayo]

Thank you for your answer, it helped me understand a few things, especially I didn't realized that i < stop and stop = 20 did not stricly bound i. However I'm still confused and I feel like I still miss a key point. I'm sorry if I'm asking trivial questions.

I didn't meant result = i and i = 0 (because i is already bound when I call the predicate) nor result = rec(i-1) (that should return all negative number and the recursion would never stop, I want to return all integers between the argument and 20 that's why there's an addition and not a subtraction).

The "step by step" way I expected this predicate to run is :

• bidingset[i] ensure that results will be finite when the predicate rec is called when i is bound to a value (which is true as I call rec when i is [1,2,3,4,5]. For that reason I don't understand why I need to consider negatives values or anythings else, because i is already bound so there's no meaning to look at every integer
• When I call the predicate rec for i in [1..5] (there may be some useless computation ocurring 5 times but that's not the point)
  • for i=1, result=i adds 1 to the return list, and because i<stop holds : result=rec(i+1) evaluates rec(2) (which is already in the returned value list because i is also equal to 2
  • for i=2, result=i adds 2 to the return list, and because i<stop holds : result=rec(i+1) evaluates rec(3) (which is already in the returned value list because i is also equal to 3
  • for i=3, result=i adds 3 to the return list, and because i<stop holds : result=rec(i+1) evaluates rec(4) (which is already in the returned value list because i is also equal to 4
  • for i=4, result=i adds 4 to the return list, and because i<stop holds : result=rec(i+1) evaluates rec(5) (which is already in the returned value list because i is also equal to 5
  • for i=5, result=i adds 5 to the return list, and because i<stop holds : result=rec(i+1) evaluates rec(6)
  • rec(6) adds 6 to the return list (because of the result=i) and because i<stop holds : evaluates rec(7)
  • rec(7) adds 7 to the return list (because of the result=i) and because i<stop holds : evaluates rec(8)
  • rec(8) adds 8 to the return list (because of the result=i) and because i<stop holds : evaluates rec(9)
  • ...
  • rec(18) adds 18 to the return list (because of the result=i) and because i<stop holds : evaluates rec(19)
  • rec(19) adds 19 to the return list (because of the result=i) and because i<stop holds : evaluates rec(20)
  • rec(20) adds 20to the return list (because of the result=i) and does not evaluate rec(21) because stop = 20 and i <stop doesn't holds, thus the recursion should stop (because result = rec(i+1) is in the same exists block than i<20
• So the result of this request should be from what I understand :
  • i = 1, result : [1..20]
  • i = 2, result : [2..20]
  • i = 3, result : [3..20]
  • i = 4, result : [4..20]
  • i = 5, result : [5..20]
• And after merging duplicates, this request should only returns integers from 1 to 20.

EDIT : To illustrate, from my understanding (which is wrong), the way I expect this query to run would be almost identical to this python code (cache and optimization aside, also I've set upper bound to 10 and not 20 to make it readable) :

def getNumber(i, acc):
    print(i, end=" ")
    acc.append(i)
    if i < 10:
        return getNumber(i+1,acc)
    else:
        return acc

i = [1,2,3,4,5]

running_query = [getNumber(x,[]) for x in i]
print(f"\nhow the query was performed : {running_query}s")

flattened_query = [item for sublist in running_query for item in sublist]
result_set = set(flattened_query)
print(f"the final result of the request : {result_set}")

From what I understood the compiler tells me a big no because he thinks result=rec(i+1) isn't bound ... But that's wrong because bindingset[i] ensure that result is bound if i is bound which is true, and i+1 is also bound.

Also I've tried mixing your suggestion and I must say that I'm even more confused :
Compilers sees no problem but from the time the request is taking it looks like an infinite recursion in this request : (I expected it to return [1..20])

int rec(int i){
    (result = i and i=0)
    or 
    exists(int stop |
        stop = 3
        and i < stop
        and result=rec(i+1)
    )
}

from int i
select rec(i)

Compiler sees no problem and request returns only 0 (with i-1 instead of i+1) (iI expected an infinite recursion)

int rec(int i){
    (result = i and i=0)
    or 
    exists(int stop |
        stop = 3
        and i < stop
        and result=rec(i-1)
    )
}

from int i
select rec(i)

[aibaars]

The evaluation of a predicate in QL does not yield a single return value, instead it returns a set of all possible combinations of parameters and result values for which the predicate "holds".

The evaluation of a recursive predicate in QL is done bottom-up and is quite different from evaluating a recursive function in a more common programming language. The evaluation strategy is roughly as follows: initially the set of answers is empty, evaluate the body of the predicate to find new possible answers, add those to the set and repeat until no new answers are found.

For example

int rec(int i){
    (result = i and i=0)
    or 
    exists(int stop |
        stop = 3
        and i < stop
        and result=rec(i-1)
    )
}

Initially {}
First iteration: result = i and i=0 gives us a new result (0 = rec(0)) which is added, now we have{0 = rec(0)} . The exists clause produces no results because {} does not contain anything that would match result = rec(i-1)

Second iteration: result = i and i=0 doesn't give us any new results, but the exists clause does. 0 = rec(0) matches result = rec(i-1) , if result = 0 and i = 1, so we add that and now have {0 = rec(0), 0 = rec(1)}

Third iteration is quite similar it finds one new result {0 = rec(0), 0 = rec(1), 0 = rec(2) }

The fourth iteration does not find any new result due to the limit i < 3, and we're done.

[aibaars]

Going back to your original question, I think you had expected CodeQL to interpret the bindingset annotation combined with the i = [0 .. 5] restriction as follows:

int rec(int i) {
  i = [1 .. 5] and
  (
    result = i
    or
    exists(int stop |
      stop = 20 and
      i < stop and
      result = rec(i + 1)
    )
  )
}

I guess this would make sense, but that is unfortunately not how things work in QL. I think the semantics of bindingset is a bit less subtle and likely just means "dear compiler please don't complain and just in-line this predicate and check that things are properly bound after inlining." . Unfortunately, the compiler cannot inline a recursive predicate, which causes it to complain There is a recursive cycle of relations that must be inlined, which is impossible

[Sixelayo]

Thank you so much for your answer ! I definitly had a lot of wrong assumptions about code ql and it helped me sort things a lot.

Now I also understand why is the other request with a +1 infinitely loops, and why it needed to be a subtraction, that's quite counter intuitive from recursion in procedural languages. That's because the result set looks like this :

• iteration 0 : {}
• iteration 1 : {(0=result(0))}
• iteration 2 : {(0=result(0),(0=result(-1))}
• iteration 3 : {(0=result(0),(0=result(-1),(0=result(-2))}

And recursion won't ever stops. The reason the compiler doesn't detect this as infinite recursion is because he can't guess the stop condition won't ever be met because i is decreasing, even if it's obvious to a human eye. I guess we haven't reached the point where we have meta static analyser designed for codeql request

Now I'm left with 2 questions :

• is there any reason why this is not the way bindingset[] works ? (That is to say : "every time a predicate with bidingset is called, adds relevant bindings at the start of the predicate".I guess because it's not possible to recompile at runtime a different predicate every single time a bindingset predicate is called but I may be wrong.
• Shouldn't it be possible to just tell the compiler to just "run the request anyways" ? The part I don't understand is must be inlined, because looking at the other 2 examples, it cannot inline the predicate nor predict if it will ends in infinite result set but nonetheless the request runs, so why is it mandatory ?