Python: Do pruning in QL.

[markshannon]

Does CFG pruning in QL. The extractor operates on a scope at a time, so cannot consider escaping variables when pruning. Moving pruning to QL fixes that problem.

[taus-semmle]

A bunch of questions and comments, but overall LGTM.

[taus-semmle]

Just checking: could we extend this to also account for incompatible bounds (like x < 4 and x > 5)?

[taus-semmle]

Ah, I see this is probably what happens on line 552. Is there any reason to split it up this way?

[markshannon]

Performance, the set of all bounds that contradict each other is rather large. So we want to check inequalities only when relevant.

[taus-semmle]

In that case, would it not be even better to include the constrained variable in TConstrainedByConstant? That way, the contradicts could check that it's in fact the same variable that's being constrained.

[markshannon]

I don't think so. Why have a " x is true" for every x when we just need one "is true"?

[markshannon]

It isn't symmetric.
x is None ⇒ x is Falsey but x is Falsey ⇏ x is None
Perhaps impliesFalse was a better name.

[taus-semmle]

I don't understand your argument. What is x? Is it this or other (or both)?
Judging by the documentation for contradicts/impliesFalse, I would certainly expect it to be symmetric. If A(x) being true implies B(x) is false, that means "A(x) and B(x)" is false. But then "B(x) and A(x)" is similarly false, and moving backwards B(x) true implies A(x) false.

[markshannon]

x is a Python variable, as in:

if x:
   if x is None:
       #unreachable
if not x:
     if x is not None:
          #reachable

I think I misread you as saying than if A ⇒ not B then not A ⇒ B, rather than if A ⇒ not B then B ⇒ not A.

All inequalities are handled below on line 552, so I don't think we want the additional disjunct here.
I'll add a pragma [inline] below to make the intention clear (the compiler inlines it already).

[taus-semmle]

I'm not sure a comment for the predicate on line 552 is sufficient. My whole point was that the above predicate, as currently written, looks incomplete ("where's the bounds checking?") and that a forward comment pointing to the place where this takes place would help.

Also, the above predicate still isn't symmetric: If this = TIsNone(true) and other is eq 0 (the second disjunct with this and other swapped, for the specific value 0), then I don't believe it'll work, as the test in contradicts for IsNone checks for other = TTruthy(true). To fix this, I think it should be sufficient to add or other instanceof ConstrainedByConstant after the TTruthy test.

[taus-semmle]

My bad, the instanceof check isn't sufficient, as it has to be eq specifically that's the operator.

[taus-semmle]

Two minor comments, but otherwise this looks nearly done.

[taus-semmle]

Why not leave out every second disjunct, and add or contradicts(b, a) at the end?

[markshannon]

That would make it recursive.

[taus-semmle]

Ah, I didn't know inlined predicates couldn't be recursive (though, thinking about it, that does make sense).

In that case, you could do something like this:

    pragma [inline]
    private predicate contradicts(Constraint a, Constraint b) {
        excludes(a, b) or excludes(b, a)
    }

    pragma [inline]
    private predicate excludes(Constraint a, Constraint b) {
        a = TIsNone(true) and b.cannotBeNone()
        or
        a.constrainsVariableToBe(true) and b.constrainsVariableToBe(false)
        or
        a.(ConstrainedByConstant).minValue() > b.(ConstrainedByConstant).maxValue()
        or
        exists(int val |
            a.(ConstrainedByConstant).eq(val) and b.(ConstrainedByConstant).ne(val)
        )
    }

But I'm not sure it's much of an improvement. I'll let you decide. If you think it's better as-is, I'll go ahead with the merge.

[markshannon]

Your version is a bit shorter, but mine more clearly lists all the cases, so I think I'd rather leave it as it is.