Simplify path conditions #970

hermanventer · 2017-09-14T02:41:22Z

Break up, simplify and refine path conditions. Also special case the property values obtained from joined objects to use the object's join condition, which is more likely to match the a path condition than the artificial "ob === ob1 ? ob1.prop : ob2.prop" that arises from the general case.

Finally, beef up the implementation of implies, to handle more complicated path conditions by breaking up && and || conditions.

NTillmann · 2017-09-14T22:50:14Z

src/evaluators/LogicalExpression.js

+  if (lval instanceof Value && compl2 instanceof Value) {
+    // joinEffects does the right thing for the side effects of the second expression but for the result the join
+    // produces a conditional expressions of the form (a ? b : a) for a && b and (a ? a : b) for a || b
+    // Rather than look for this pattern everywhere, we override this behavior and replace the completion with


"Rather than look for this pattern everywhere" - I would phrase that as a TODO: In some future, all such expressions should immediately simplify down to some normal form, and it should be impossible to construct values that are not in normal form.

This is from the previous pull request. Adding a TODO like that at this point does not strike me as at all as useful.

NTillmann · 2017-09-14T22:52:30Z

src/utils/paths.js

+function pushPathCondition(condition: Value) {
+  if (condition instanceof ConcreteValue) return;
+  if (!condition.mightNotBeTrue()) return;
+  invariant(condition instanceof AbstractValue);


Another invariant should be invariant(!condition.mightNotBeFalse()).

And both invariants should be checked before the if (condition instanceof ConcreteValue) return; statement.

It is sort of really obvious, but why not? I'll add it.

The invariant in line 45 is there to convince Flow that a Value that is not a ConcreteValue is actually an AbstractValue. It is inconvenient to insist that the condition may not known to be true and there is not much to be gained from checking that it is not, since it naturally arises from refinement of existing path conditions. It should, however, always be the case that a path condition cannot be known to be definitely false, since that would contract the implicit assertion that path conditions are always true in the path they guard. That invariant I can add.

I have no problem with the invariant(condition instanceof AbstractValue); invariant. My comments were about other invariants that are or should go in front.

NTillmann · 2017-09-14T22:56:14Z

src/utils/paths.js

+  if (condition.kind === "&&") {
+    let left = condition.args[0];
+    let right = condition.args[1];
+    invariant(left instanceof AbstractValue);


I don't get why that invariant is guaranteed to hold.

Anyone can create abstract values with the "&&", as we haven't locked that up. But that maybe secondary...

createFromLogicalOp seems to happy construct conditions where one operand is a concrete value.

I'll add a comment. The reason is that if the first argument is concrete, the second argument will never be evaluated and hence it is a mistake to make such an abstract value.

A mistake, yes, but this would be a very late invariant check. Should createFromLogicalOp disallow it as well?

Indeed. I'll see to it.

NTillmann · 2017-09-14T22:56:44Z

src/utils/paths.js

+}
+
+function pushInversePathCondition(condition: Value) {
+  if (condition instanceof ConcreteValue) return;


Similar comments as for pushPathCondition apply.

similar answers.

NTillmann · 2017-09-14T22:57:23Z

src/utils/paths.js

+    invariant(right instanceof AbstractValue);
+    pushPathCondition(left);
+    pushPathCondition(right);
+  } else {


Why the lack of symmetry? pushInversePathCondition deals with both cases... How about folding both together with a boolean parameter negate?

I did initially fold both together and I found that the code became so unreadable that I was not confident it was correct.

There lack of symmetry, such as it is, is because pushPathCondition gets a ready made condition that can be pushed as is, whereas pushInversePathCondition has to invert the condition before pushing it.

NTillmann · 2017-09-14T22:57:52Z

src/utils/paths.js

+    let realm = condition.$Realm;
+    let inverseCondition = AbstractValue.createFromUnaryOp(realm, "!", condition);
+    pushPathCondition(inverseCondition);
+    let simpliedInverseCondition = simplifyAbstractValue(realm, inverseCondition);


Spelling of simpliedInverseCondition

NTillmann · 2017-09-14T23:22:23Z

src/utils/paths.js

+    let inverseCondition = AbstractValue.createFromUnaryOp(realm, "!", condition);
+    pushPathCondition(inverseCondition);
+    let simpliedInverseCondition = simplifyAbstractValue(realm, inverseCondition);
+    if (simpliedInverseCondition instanceof AbstractValue && simpliedInverseCondition !== inverseCondition)


It's strange to see this one-off case. Maybe this is to solve a little issue at hand, but I don't want to see our reasoning infrastructure being randomized.

I'll remove the check for AbstractValue; that is no longer needed. The equality check is there to avoid duplication in the case where an expression failed to actually simplify.

What I meant with the one-off is that only here you also add the simplified path condition in addition to a non-simplified path condition. All the other pieces that get pushed might not be simplified. Overall, I am confused whether pushed path conditions are simplified or not. I don't see enforcement or comments, just this one special treatment.

NTillmann · 2017-09-14T23:28:45Z

src/values/AbstractObjectValue.js

+      // use this join condition for the join of the two property values
+      let [cond, ob1, ob2] = this.args;
+      invariant(cond instanceof AbstractValue);
+      invariant(ob1 instanceof ObjectValue);


Why are the args guaranteed to be of this shape? Hard to tell anything given that anyone can set the .kind property... But in general, if it's a conditional value, why can't there be more structure to the arguments?

We know this value in AbstractObjectValue, so both operands must be objects, otherwise invariants would fail in the constructor. The condition should be Abstract, because otherwise there would be no need for the join. The comment in line 134 already speaks to this.

Hm, can't find the constructor invariant. Can you point me to it?

Every operation on an abstract object value that retrieves elements from its values collection assert that all of the elements are objects, so this is a maintained invariant of the class. The constructor, however, does not check the invariant. There is no good reason why it shouldn't (and I expected that it does), so I'll add a check.

NTillmann · 2017-09-14T23:30:06Z

src/values/AbstractObjectValue.js

@@ -261,6 +279,24 @@ export default class AbstractObjectValue extends AbstractValue {
        return cv.$Get(P, Receiver);
      }
      invariant(false);
+    } else if (this.kind === "conditional") {
+      // this is the join of two concrete objects


Seems quite redundant with the $GetOwnProperty code.

It is, but it is also different in subtle ways that make it easier to read in its redundant form. I may come back to this, but at the moment I would prefer to keep things this way.

NTillmann · 2017-09-15T00:15:21Z

src/values/AbstractValue.js

+      let [left, right] = this.args;
+      let refinedLeft = left instanceof AbstractValue ? left.refineWithPathCondition() : left;
+      let refinedRight = right instanceof AbstractValue ? right.refineWithPathCondition() : right;
+      if (!refinedLeft.mightNotBeTrue()) return refinedRight;


This logic here seems more general than the place where it sits: createFromLogicalOp could do this kind of normalization to benefit anyone who attempts to build logical operations.

Interestingly, createFromConditionalOp already does some simplification.

I don't want the abstract value factory functions to be path sensitive. There is probably room for an in depth design discussion about all this, but it is a bit premature right now.

Totally agreed that the factory should not be path sensitive. I just meant the mightNotBeTrue() kind of checks that result in simplified expressions.

NTillmann · 2017-09-15T00:16:38Z

src/values/AbstractValue.js

    left: void | Value,
    right: void | Value,
    loc?: ?BabelNodeSourceLocation
  ): AbstractValue {
+    if (left instanceof BooleanValue && right instanceof BooleanValue) {


Why special casing for BooleanValue and not just using the more general .mightNotBeTrue kind of machinery?

This is more specific than it needs to be. I'll generalize it, but I can't really think of a valid use case for the more general form.

NTillmann

See comments.

facebook-github-bot · 2017-09-18T21:54:46Z

@hermanventer has imported this pull request. If you are a Facebook employee, you can view this diff on Phabricator.

facebook-github-bot · 2017-09-20T21:29:20Z

@hermanventer has imported this pull request. If you are a Facebook employee, you can view this diff on Phabricator.

Summary: Break up, simplify and refine path conditions. Also special case the property values obtained from joined objects to use the object's join condition, which is more likely to match the a path condition than the artificial "ob === ob1 ? ob1.prop : ob2.prop" that arises from the general case. Finally, beef up the implementation of implies, to handle more complicated path conditions by breaking up && and || conditions. Closes #970 Differential Revision: D5857033 Pulled By: hermanventer fbshipit-source-id: 5436d251378decf6de549a3d70e9605664d569e5

hermanventer requested review from cblappert and NTillmann September 14, 2017 02:41

facebook-github-bot added the CLA Signed label Sep 14, 2017

NTillmann reviewed Sep 14, 2017

View reviewed changes

NTillmann reviewed Sep 15, 2017

View reviewed changes

NTillmann suggested changes Sep 15, 2017

View reviewed changes

NTillmann approved these changes Sep 18, 2017

View reviewed changes

Simplify path conditions

54d2c1a

facebook-github-bot closed this in db79b83 Sep 20, 2017

hermanventer deleted the refine3 branch September 20, 2017 23:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Simplify path conditions #970

Simplify path conditions #970

hermanventer commented Sep 14, 2017

NTillmann Sep 14, 2017

hermanventer Sep 14, 2017 •

edited

Loading

NTillmann Sep 14, 2017

NTillmann Sep 14, 2017

hermanventer Sep 14, 2017

hermanventer Sep 15, 2017

NTillmann Sep 15, 2017

NTillmann Sep 14, 2017

hermanventer Sep 15, 2017

NTillmann Sep 15, 2017

hermanventer Sep 15, 2017

NTillmann Sep 14, 2017

hermanventer Sep 15, 2017

NTillmann Sep 14, 2017

hermanventer Sep 15, 2017 •

edited

Loading

NTillmann Sep 14, 2017

hermanventer Sep 15, 2017

NTillmann Sep 14, 2017

hermanventer Sep 15, 2017

NTillmann Sep 15, 2017

NTillmann Sep 14, 2017

hermanventer Sep 15, 2017

NTillmann Sep 15, 2017

hermanventer Sep 18, 2017

NTillmann Sep 14, 2017

hermanventer Sep 15, 2017

NTillmann Sep 15, 2017 •

edited

Loading

hermanventer Sep 15, 2017

NTillmann Sep 15, 2017

NTillmann Sep 15, 2017

hermanventer Sep 15, 2017

NTillmann left a comment

facebook-github-bot commented Sep 18, 2017

facebook-github-bot commented Sep 20, 2017

Simplify path conditions #970

Simplify path conditions #970

Conversation

hermanventer commented Sep 14, 2017

Choose a reason for hiding this comment

hermanventer Sep 14, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hermanventer Sep 15, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NTillmann Sep 15, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NTillmann left a comment

Choose a reason for hiding this comment

facebook-github-bot commented Sep 18, 2017

facebook-github-bot commented Sep 20, 2017

hermanventer Sep 14, 2017 •

edited

Loading

hermanventer Sep 15, 2017 •

edited

Loading

NTillmann Sep 15, 2017 •

edited

Loading