controls and valueControls (cpp)

[Sixelayo]

I was trying to understand GuardedCondition

A Boolean condition in the AST that guards one or more basic blocks. This includes operands of logical operators but not switch statements.

predicate controls(BasicBlock controlled, boolean testIsTrue)
predicate valueControls(BasicBlock controlled, AbstractValue v)

The controls predicate :

Holds if this condition controls controlled, meaning that controlled is only entered if the value of this condition is testIsTrue.

The valueControls predicate :

Holds if this condition controls controlled, meaning that controlled is only entered if the value of this condition is v.

And finally AbstractValue

An abstract value. This is either a boolean value, or a switch case.

But wait ... wasn't it explicitly stated in GuardedCondition that it doesn't take switch case statement into account ? So what's the point of valueControls ?

My guess is that I have a wrong understanding of what is an AbstractValue is because I don't see their point in others predicates (such as comparesEq. Nor do I understand what does "dertermined by this guard" means in the documentation despite reading this I supposed it means "in the direct basic block after evaluation" but I also don't understand the point of k inleft == right+k (why do we need 3 variable for a comparison ?), so I'm probably mistaken elsewhere

[MathiasVP]

But wait ... wasn't it explicitly stated in GuardedCondition that it doesn't take switch case statement into account ? So what's the point of valueControls?

It looks like the QLDoc for hasn't been updated since we added support for switch statements (for what it's worth, this was done in #15941). I've opened a PR to fix the documentation here.

That should hopefully take care of the first part of your question :)

Now let's take the next part:

Nor do I understand what does "dertermined by this guard" means in the documentation despite reading this I supposed it means "in the direct basic block after evaluation" [...]

"determined by this guard" means "implied by this guard". That is, if you have a guard such as:

if(a == b + 42 && c > 0) { ... }

then both a == b + 42 and c > 0 are GuardConditions. So there can be multiple GuardConditions from a given guard in the source code, and we "determine those GuardConditions from the guard". I hope that clears up some confusion.

Finally:

but I also don't understand the point of k in left == right+k (why do we need 3 variable for a comparison ?), so I'm probably mistaken elsewhere

You don't need three variables for the comparison, but you can use it if it's useful to you. The point is that, there are many ways of writing a comparison such as a == b + 42 (for example, maybe someone wrote a - 2 == b + 40 or a - b - 42 == 0), and the GuardCondition library "normalizes" such comparisons for you so that you can reason about them as if they were all of the form a == b + k.

If you don't care about k you can simply put 0 there and you're left with equalities of the form a == b. For example:

from GuardCondition gc, Expr left, Expr right, boolean b
where gc.comparesEq(left, right, 0, true, b)
select gc, left, right, b

finds values gc, left, right, b such that left == right is true when gc evaluates to b.

[Sixelayo]

Thank you ! Now I understand everything.

So actually

from GuardCondition gc, Expr left, Expr right, boolean b
where gc.comparesEq(left, right, 0, true, b)

Is the exact same than :

and exists(BasicBlock bb |
        gc.ensuresEq(left, right, bb, true)
        and bb = gc.getThen()
    )

(well actually it's not the same thing because we'de need to convert right to an int and we don't have a getThen() predicate for GuardCondition, but aside from that, conceptually it does the exact same thing)