-
Notifications
You must be signed in to change notification settings - Fork 1.8k
Python: Do pruning in QL. #1292
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
4a68a1e
to
88baa3a
Compare
88baa3a
to
f843ad4
Compare
f843ad4
to
bbf7ff9
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A bunch of questions and comments, but overall LGTM.
this.getOp() = eq() and other = TIsNone(true) | ||
or | ||
this.getOp() = ne() and other.(ConstrainedByConstant).getOp() = eq() | ||
and this.intValue() = other.(ConstrainedByConstant).intValue() |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just checking: could we extend this to also account for incompatible bounds (like x < 4
and x > 5
)?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, I see this is probably what happens on line 552. Is there any reason to split it up this way?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Performance, the set of all bounds that contradict each other is rather large. So we want to check inequalities only when relevant.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think so. Why have a " x
is true" for every x
when we just need one "is true"?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It isn't symmetric.
x is None
⇒ x is Falsey
but x is Falsey
⇏ x is None
Perhaps impliesFalse
was a better name.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My bad, the instanceof
check isn't sufficient, as it has to be eq
specifically that's the operator.
… imply that 'x is None' is false.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Two minor comments, but otherwise this looks nearly done.
a.(ConstrainedByConstant).eq(val) and b.(ConstrainedByConstant).ne(val) | ||
or | ||
a.(ConstrainedByConstant).ne(val) and b.(ConstrainedByConstant).eq(val) | ||
) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not leave out every second disjunct, and add or contradicts(b, a)
at the end?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That would make it recursive.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, I didn't know inline
d 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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
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.