Compose without tail duplication #2460

hermanventer · 2018-08-22T01:47:26Z

Release note: none

Closes #2435
Closes #1829

Join.composeWithEffects composes a forked completion with subsequent effects. When two or more forks could end normally, this could result in shallow copies of the subsequent effects. These were then joined together and applied, so it was mostly OK. The generator of the subsequent effects, however, ended up being joined with itself and thus transformed the generator tree to a DAG, which is not desirable for the serializer.

The new approach is to extract a join condition from the forked completion and using it to join the subsequent effects with a newly constructed empty effects. The condition ensures that the subsequent effects are applied only in situations where the forked completion is not abrupt.

Extracting this condition makes for complicated abstract expressions and this uncovered some existing bugs and limitations that are also addressed in this pull request. As a side effect, path conditions are now longer and the time to compile unrolled loops with conditional abrupt completions inside their bodies has gone up so much that the unroll limit had to be lowered.

Please note that the expected output React tests has changed because of re-ordering. I'm none too sure that this re-ordering is necessarily benign, so please review carefully.

trueadm · 2018-08-22T09:02:48Z

Looking into the tests more, I thought that the ordering here mattered but it doesn't seem to matter as this is the order of how the React Reconciler takes conditions – which seems to have flipper from before so I think this is actually fine. Unfortunately, the same pushing false invariant still occurs in our internal React bundle and also from #2361 (I wasn't sure if this PR was to also fix or somewhat address those issues too).

It appears that test/serializer/optimized-functions/LoopBailout18.js is causing the CI to fail because it takes longer than 10m and thus CircleCI fails the tests.

https://support.circleci.com/hc/en-us/articles/360007188574-Build-has-hit-timeout-limit

calebmer · 2018-08-22T16:07:02Z

src/evaluators/BinaryExpression.js

@@ -284,7 +285,8 @@ export function computeBinary(

    if (isPure && effects) {
      realm.applyEffects(effects);
-      return realm.returnOrThrowCompletion(effects.result);
+      if (effects.result instanceof SimpleNormalCompletion) return effects.result.value;
+      effects.result;


return effects.result;?

Actually no, that is debugging code that got left in. I'll remove.

hermanventer · 2018-08-22T18:11:36Z

@trueadm: The issue in #2361 does not reproduce for me at all. Oh wait, I assumed it was a serializer test case. I'll see what I can do using debug-fb-www.js.

trueadm · 2018-08-22T18:30:41Z

@hermanventer Sorry, this only seems to occur with abstractValueImpliesMax set to 1000, as per debug-fb-www's settings.

NTillmann

I feel like the simplifier rules are becoming quite problematic to write and rewrite. We need a more principled approach. Maybe not Z3 based, but there should be some kind of term rewriting system that we should be able to leverage, to write and verify rules and to generate code from it.
And instead of poking around narrow patterns, there should be normal forms, and efficient ways to encode the boolean structures...

NTillmann · 2018-08-22T21:17:42Z

src/methods/join.js

+  joinValuesOfSelectedCompletions(
+    selector: Completion => boolean,
+    completion: Completion,
+    keepInfeasiblePaths: boolean = false


Why would it ever be desirable to keep infeasible paths?

It is not desirable, but a hack to work around the fact that generator.emitConditionalThrow wants a value for its parameter. Fixing that to take the completion instead would be preferable. For this PR, however, that seems out of scope.

NTillmann · 2018-08-22T21:18:20Z

src/utils/generator.js

@@ -597,7 +597,7 @@ export class Generator {
    } else if (result instanceof JoinedNormalAndAbruptCompletions) {
      let selector = c =>
        c instanceof ThrowCompletion && c.value !== realm.intrinsics.__bottomValue && !(c.value instanceof EmptyValue);
-      output.emitConditionalThrow(Join.joinValuesOfSelectedCompletions(selector, result));
+      output.emitConditionalThrow(Join.joinValuesOfSelectedCompletions(selector, result, true));


It's hard to tell from the callsite what the , true argument means. Maybe make it named?

Why don't you want to keepInfeasiblePaths here?

NTillmann · 2018-08-22T21:24:40Z

src/utils/simplifier.js

+        if (y instanceof AbstractValue && y.kind === "||") {
+          // x || x || y <=> x || y
+          if (x.equals(y.args[0])) return y;
+          // y || x || y <=> x || y


This comment seems to be missing code.

I'll delete the comment.

NTillmann · 2018-08-22T21:26:37Z

src/utils/simplifier.js

+          if (x.equals(y.args[0])) return y;
+          // y || x || y <=> x || y
+          if (x instanceof AbstractValue && x.kind === "!") {
+            // !x || x || y <=> y


This (and the next) rule seems wrong, unless I am missing some special JavaScript craziness.

The comment is correct if you don't equate the meta variable x with the comment variable x. I'll update the comment to make it more difficult to equate them.

NTillmann · 2018-08-22T21:31:38Z

src/utils/simplifier.js

+          // y && (x && y) <=> x && y
+          if (x.equals(y.args[0]) || x.equals(y.args[1])) return y;
+        }
+        // x && (x && y || x && z) <=> x && (y && z)


The comment seems wrong, while the implementation may be correct.

The comment tries to communicate the pattern in the most abstract way. The code does not follow the names in the comment when things get complicated.

I think the comment should be // x && (x && y || x && z) <=> x && (y || z)

hermanventer

At this stage, rewriting the simplifier does not seem like a top priority. It certainly is out of scope for this PR.

hermanventer · 2018-08-23T02:14:47Z

src/utils/simplifier.js

+        if (y instanceof AbstractValue && y.kind === "||") {
+          // x || x || y <=> x || y
+          if (x.equals(y.args[0])) return y;
+          // y || x || y <=> x || y


I'll delete the comment.

hermanventer · 2018-08-23T02:16:19Z

src/utils/simplifier.js

+          if (x.equals(y.args[0])) return y;
+          // y || x || y <=> x || y
+          if (x instanceof AbstractValue && x.kind === "!") {
+            // !x || x || y <=> y


The comment is correct if you don't equate the meta variable x with the comment variable x. I'll update the comment to make it more difficult to equate them.

hermanventer · 2018-08-23T02:34:47Z

src/utils/simplifier.js

+          // y && (x && y) <=> x && y
+          if (x.equals(y.args[0]) || x.equals(y.args[1])) return y;
+        }
+        // x && (x && y || x && z) <=> x && (y && z)


The comment tries to communicate the pattern in the most abstract way. The code does not follow the names in the comment when things get complicated.

NTillmann · 2018-08-23T17:00:15Z

src/utils/simplifier.js

+          // y && (x && y) <=> x && y
+          if (x.equals(y.args[0]) || x.equals(y.args[1])) return y;
+        }
+        // x && (x && y || x && z) <=> x && (y && z)


I think the comment should be // x && (x && y || x && z) <=> x && (y || z)

NTillmann · 2018-08-23T17:02:49Z

src/utils/simplifier.js

+          if (x.equals(y.args[0])) return y;
+          if (x instanceof AbstractValue && x.kind === "!") {
+            // !x0 || x0 || y1 <=> y1
+            if (x.args[0].equals(y.args[0])) return y.args[1];


This still seems wrong to me. !x || x || y should be equivalent to true, not y.

Duh! I'll remove this.

facebook-github-bot

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

facebook-github-bot

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

NTillmann · 2018-08-24T01:00:55Z

src/utils/simplifier.js

+          // x || x || y <=> x || y
+          if (x.equals(y.args[0])) return y;
+          if (x instanceof AbstractValue && x.kind === "!") {
+            // !x0 || y0 || x0 <=> y0


This seems wrong to me. !x0 || ... || x0 is true, not equivalent to some random value.

Correct. Moreover, only if isCondition is true.

NTillmann · 2018-08-24T01:22:18Z

src/utils/simplifier.js

+            if (x.args[0].equals(y) || x.args[1].equals(y)) return x;
+          } else if (x.kind === "!") {
+            // !x && x <=> false
+            if (x.args[0].equals(y)) return realm.intrinsics.false;


Only if isCondition, right?

hermanventer · 2018-08-24T02:02:37Z

@trueadm Sadly, the internal React test is failing, presumably because of exceeding implies limits (a lot of those appear in the log output). Could you have a look and give a prognosis of how fixable this may be?

It might be necessary to make some changes so that simplification has a better worst case complexity. (And that may not be easy at all.)

facebook-github-bot

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

NTillmann · 2018-08-24T04:35:53Z

src/utils/simplifier.js

+          if (x.kind === "&&") {
+            // (x && y) && x <=> x && y
+            // (x && y) && y <=> x && y
+            if (x.args[0].equals(y) || x.args[1].equals(y)) return x;


Thinking about it, the first one is actually only valid if isCondition without reordering: (1 && 2) && 1 vs 1 && 2.

Good catch.

trueadm · 2018-08-24T12:50:02Z

This PR is currently failing the internal React bundle test with an invariant in _getTarget in the serializer. I'll dig into it today and see if I can see if there's anything obvious.

Summary: Release note: Speed up simplifier by using an implication cache per path branch The realm's path conditions is now a class instances and an explicit tree, along with caches for expressions that have already been checked for true/false using Path.implies on the current set of path conditions. The AbstractValueImplicationCounter is still there as flag, to be renamed later. It is no longer used as a global k-limit, but enables k-limits on the cost of constructing a new set of path conditions. When React is the target, path conditions are not re-specialized. This leads to a very nice performance win for the large React internal test. A number of tweaks to the simplifier were needed to get tests to pass. Some of these were borrowed from PR #2460. Pull Request resolved: #2494 Reviewed By: trueadm Differential Revision: D9554820 Pulled By: hermanventer fbshipit-source-id: 5fdc550499975fe11c0c954b9502cd4eeab2bafe

Summary: Release note: none This fixes two problems uncovered while debugging the failure of PR #2460 when run on a large internal test case: 1) CSE did not fix up recently introduced aliases of expressions. 2) The serializer logic visited array elements that were not visited because of recently introduced leak logic. Pull Request resolved: #2516 Differential Revision: D9599235 Pulled By: hermanventer fbshipit-source-id: a2047227b4aa2e0e2def7d8e7ebe0724a9525160

facebook-github-bot

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

trueadm

LGTM, merging as this is blocker for others.

hermanventer requested review from trueadm, NTillmann and calebmer August 22, 2018 01:47

facebook-github-bot added the CLA Signed label Aug 22, 2018

trueadm force-pushed the tailDup branch from 04ab477 to 6aea415 Compare August 22, 2018 11:29

calebmer reviewed Aug 22, 2018

View reviewed changes

hermanventer force-pushed the tailDup branch from 6aea415 to d061814 Compare August 22, 2018 18:03

NTillmann suggested changes Aug 22, 2018

View reviewed changes

hermanventer force-pushed the tailDup branch from d061814 to d91a2a2 Compare August 23, 2018 02:37

hermanventer commented Aug 23, 2018

View reviewed changes

NTillmann reviewed Aug 23, 2018

View reviewed changes

hermanventer force-pushed the tailDup branch 2 times, most recently from 9bdea56 to 40228ef Compare August 23, 2018 20:38

facebook-github-bot reviewed Aug 23, 2018

View reviewed changes

hermanventer force-pushed the tailDup branch from 40228ef to eb09c06 Compare August 23, 2018 21:06

facebook-github-bot reviewed Aug 23, 2018

View reviewed changes

NTillmann reviewed Aug 24, 2018

View reviewed changes

hermanventer force-pushed the tailDup branch 2 times, most recently from c69d7d8 to f22c424 Compare August 24, 2018 01:59

facebook-github-bot reviewed Aug 24, 2018

View reviewed changes

NTillmann reviewed Aug 24, 2018

View reviewed changes

hermanventer force-pushed the tailDup branch from f22c424 to 400160b Compare August 24, 2018 18:31

NTillmann approved these changes Aug 24, 2018

View reviewed changes

hermanventer mentioned this pull request Aug 28, 2018

Cache path implications #2494

Closed

hermanventer mentioned this pull request Aug 30, 2018

Fix CSE in back-end #2516

Closed

Simplifier tweaks

27e2075

hermanventer force-pushed the tailDup branch from 400160b to 27e2075 Compare August 31, 2018 02:17

facebook-github-bot reviewed Aug 31, 2018

View reviewed changes

trueadm approved these changes Aug 31, 2018

View reviewed changes

facebook-github-bot closed this in 3f2445d Aug 31, 2018

hermanventer deleted the tailDup branch August 31, 2018 18:31

hermanventer mentioned this pull request Aug 31, 2018

Compose without tail duplication #2523

Closed

Compose without tail duplication #2460

Compose without tail duplication #2460

Conversation

hermanventer commented Aug 22, 2018 • edited Loading

trueadm commented Aug 22, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hermanventer commented Aug 22, 2018 • edited Loading

trueadm commented Aug 22, 2018

NTillmann left a comment • 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

hermanventer left a 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

facebook-github-bot left a comment

Choose a reason for hiding this comment

facebook-github-bot left a 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 commented Aug 24, 2018 • edited Loading

facebook-github-bot left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

trueadm commented Aug 24, 2018

facebook-github-bot left a comment

Choose a reason for hiding this comment

trueadm left a comment

Choose a reason for hiding this comment

hermanventer commented Aug 22, 2018 •

edited

Loading

trueadm commented Aug 22, 2018 •

edited

Loading

hermanventer commented Aug 22, 2018 •

edited

Loading

NTillmann left a comment •

edited

Loading

hermanventer commented Aug 24, 2018 •

edited

Loading