157379 2016-05-05 11:33:25 -0700 We shouldn't crash if DFG AI proved that something was unreachable on one run but then decided not to prove it on another run 2016-06-10 12:31:49 -0700 1 1 1 Unclassified WebKit JavaScriptCore WebKit Nightly Build All All RESOLVED FIXED P2 Normal --- 158631 1 fpizlo fpizlo commit-queue keith_miller mark.lam msaboff saam oldest_to_newest 1190399 0 fpizlo 2016-05-05 11:33:25 -0700 Any run of DFG AI is a fixpoint that loosens the proof until it can't fine any more counterexamples to the proof. It errs on the side of loosening proofs, i.e., on the side of proving fewer things. We run this fixpoint multiple times since there are multiple points in the DFG optimization pipeline when we run DFG AI. Each of those runs completes a fixpoint and produces the tightest proof it can that did not result in counterexamples being found. It's possible that on run K of DFG AI, we prove some property, but on run K+1, we don't prove that property. The code could have changed between the two runs due to other phases. Other phases may modify the code in such a way that it's less amenable to AI's analysis. Our design allows this because DFG AI is not 100% precise. It defends itself from making unsound choices or running forever by sometimes punting on proving some property. It must be able to do this, and so therefore, it might sometimes prove fewer things on a later run. Currently in trunk if the property that AI proves on run K but fails to prove on run K+1 is the reachability of a piece of code, then run K+1 will crash on an assertion at the Unreachable node. It will complain that it reached an Unreachable. But it might be reaching that Unreachable because it failed to prove that something earlier was always exiting. That's OK, see above. So, we should remove the assertion that AI doesn't see Unreachable. 1190400 1 278177 fpizlo 2016-05-05 11:35:23 -0700 Created attachment 278177 the patch 1190402 2 278177 mark.lam 2016-05-05 11:42:18 -0700 Comment on attachment 278177 the patch r=me 1190411 3 fpizlo 2016-05-05 12:20:01 -0700 Landed in http://trac.webkit.org/changeset/200468 278177 2016-05-05 11:35:23 -0700 2016-05-05 11:42:18 -0700 the patch blah.patch text/plain 3504 fpizlo SW5kZXg6IFNvdXJjZS9KYXZhU2NyaXB0Q29yZS9DaGFuZ2VMb2cKPT09PT09PT09PT09PT09PT09 PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQotLS0gU291 cmNlL0phdmFTY3JpcHRDb3JlL0NoYW5nZUxvZwkocmV2aXNpb24gMjAwNDY0KQorKysgU291cmNl L0phdmFTY3JpcHRDb3JlL0NoYW5nZUxvZwkod29ya2luZyBjb3B5KQpAQCAtMSwzICsxLDM5IEBA CisyMDE2LTA1LTA1ICBGaWxpcCBQaXpsbyAgPGZwaXpsb0BhcHBsZS5jb20+CisKKyAgICAgICAg V2Ugc2hvdWxkbid0IGNyYXNoIGlmIERGRyBBSSBwcm92ZWQgdGhhdCBzb21ldGhpbmcgd2FzIHVu cmVhY2hhYmxlIG9uIG9uZSBydW4gYnV0IHRoZW4gZGVjaWRlZCBub3QgdG8gcHJvdmUgaXQgb24g YW5vdGhlciBydW4KKyAgICAgICAgaHR0cHM6Ly9idWdzLndlYmtpdC5vcmcvc2hvd19idWcuY2dp P2lkPTE1NzM3OQorCisgICAgICAgIFJldmlld2VkIGJ5IE5PQk9EWSAoT09QUyEpLgorICAgICAg ICAKKyAgICAgICAgQW55IHJ1biBvZiBERkcgQUkgaXMgYSBmaXhwb2ludCB0aGF0IGxvb3NlbnMg dGhlIHByb29mIHVudGlsIGl0IGNhbid0IGZpbmUgYW55IG1vcmUKKyAgICAgICAgY291bnRlcmV4 YW1wbGVzIHRvIHRoZSBwcm9vZi4gIEl0IGVycnMgb24gdGhlIHNpZGUgb2YgbG9vc2VuaW5nIHBy b29mcywgaS5lLiwgb24gdGhlIHNpZGUgb2YKKyAgICAgICAgcHJvdmluZyBmZXdlciB0aGluZ3Mu CisKKyAgICAgICAgV2UgcnVuIHRoaXMgZml4cG9pbnQgbXVsdGlwbGUgdGltZXMgc2luY2UgdGhl cmUgYXJlIG11bHRpcGxlIHBvaW50cyBpbiB0aGUgREZHIG9wdGltaXphdGlvbgorICAgICAgICBw aXBlbGluZSB3aGVuIHdlIHJ1biBERkcgQUkuICBFYWNoIG9mIHRob3NlIHJ1bnMgY29tcGxldGVz IGEgZml4cG9pbnQgYW5kIHByb2R1Y2VzIHRoZQorICAgICAgICB0aWdodGVzdCBwcm9vZiBpdCBj YW4gdGhhdCBkaWQgbm90IHJlc3VsdCBpbiBjb3VudGVyZXhhbXBsZXMgYmVpbmcgZm91bmQuCisK KyAgICAgICAgSXQncyBwb3NzaWJsZSB0aGF0IG9uIHJ1biBLIG9mIERGRyBBSSwgd2UgcHJvdmUg c29tZSBwcm9wZXJ0eSwgYnV0IG9uIHJ1biBLKzEsIHdlIGRvbid0IHByb3ZlCisgICAgICAgIHRo YXQgcHJvcGVydHkuIFRoZSBjb2RlIGNvdWxkIGhhdmUgY2hhbmdlZCBiZXR3ZWVuIHRoZSB0d28g cnVucyBkdWUgdG8gb3RoZXIgcGhhc2VzLiBPdGhlcgorICAgICAgICBwaGFzZXMgbWF5IG1vZGlm eSB0aGUgY29kZSBpbiBzdWNoIGEgd2F5IHRoYXQgaXQncyBsZXNzIGFtZW5hYmxlIHRvIEFJJ3Mg YW5hbHlzaXMuIE91ciBkZXNpZ24KKyAgICAgICAgYWxsb3dzIHRoaXMgYmVjYXVzZSBERkcgQUkg aXMgbm90IDEwMCUgcHJlY2lzZS4gSXQgZGVmZW5kcyBpdHNlbGYgZnJvbSBtYWtpbmcgdW5zb3Vu ZCBjaG9pY2VzCisgICAgICAgIG9yIHJ1bm5pbmcgZm9yZXZlciBieSBzb21ldGltZXMgcHVudGlu ZyBvbiBwcm92aW5nIHNvbWUgcHJvcGVydHkuIEl0IG11c3QgYmUgYWJsZSB0byBkbyB0aGlzLAor ICAgICAgICBhbmQgc28gdGhlcmVmb3JlLCBpdCBtaWdodCBzb21ldGltZXMgcHJvdmUgZmV3ZXIg dGhpbmdzIG9uIGEgbGF0ZXIgcnVuLgorCisgICAgICAgIEN1cnJlbnRseSBpbiB0cnVuayBpZiB0 aGUgcHJvcGVydHkgdGhhdCBBSSBwcm92ZXMgb24gcnVuIEsgYnV0IGZhaWxzIHRvIHByb3ZlIG9u IHJ1biBLKzEgaXMKKyAgICAgICAgdGhlIHJlYWNoYWJpbGl0eSBvZiBhIHBpZWNlIG9mIGNvZGUs IHRoZW4gcnVuIEsrMSB3aWxsIGNyYXNoIG9uIGFuIGFzc2VydGlvbiBhdCB0aGUKKyAgICAgICAg VW5yZWFjaGFibGUgbm9kZS4gSXQgd2lsbCBjb21wbGFpbiB0aGF0IGl0IHJlYWNoZWQgYW4gVW5y ZWFjaGFibGUuIEJ1dCBpdCBtaWdodCBiZSByZWFjaGluZworICAgICAgICB0aGF0IFVucmVhY2hh YmxlIGJlY2F1c2UgaXQgZmFpbGVkIHRvIHByb3ZlIHRoYXQgc29tZXRoaW5nIGVhcmxpZXIgd2Fz IGFsd2F5cyBleGl0aW5nLiBUaGF0J3MKKyAgICAgICAgT0ssIHNlZSBhYm92ZS4KKworICAgICAg ICBTbywgd2Ugc2hvdWxkIHJlbW92ZSB0aGUgYXNzZXJ0aW9uIHRoYXQgQUkgZG9lc24ndCBzZWUg VW5yZWFjaGFibGUuCisgICAgICAgIAorICAgICAgICBObyBuZXcgdGVzdHMgYmVjYXVzZSBJIGRv bid0IGtub3cgaG93IHRvIG1ha2UgdGhpcyBoYXBwZW4uIEkgYmVsaWV2ZSB0aGF0IHRoaXMgaGFw cGVucyBpbiB0aGUKKyAgICAgICAgd2lsZCBiYXNlZCBvbiBjcmFzaCBsb2dzLgorCisgICAgICAg ICogZGZnL0RGR0Fic3RyYWN0SW50ZXJwcmV0ZXJJbmxpbmVzLmg6CisgICAgICAgIChKU0M6OkRG Rzo6QWJzdHJhY3RJbnRlcnByZXRlcjxBYnN0cmFjdFN0YXRlVHlwZT46OmV4ZWN1dGVFZmZlY3Rz KToKKwogMjAxNi0wNS0wNSAgS2VpdGggTWlsbGVyICA8a2VpdGhfbWlsbGVyQGFwcGxlLmNvbT4K IAogICAgICAgICBBZGQgc3VwcG9ydCBmb3IgZGVsZXRlIGJ5IHZhbHVlIHRvIHRoZSBERkcKSW5k ZXg6IFNvdXJjZS9KYXZhU2NyaXB0Q29yZS9kZmcvREZHQWJzdHJhY3RJbnRlcnByZXRlcklubGlu ZXMuaAo9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09 PT09PT09PT09PT09PT09Ci0tLSBTb3VyY2UvSmF2YVNjcmlwdENvcmUvZGZnL0RGR0Fic3RyYWN0 SW50ZXJwcmV0ZXJJbmxpbmVzLmgJKHJldmlzaW9uIDIwMDQ2MykKKysrIFNvdXJjZS9KYXZhU2Ny aXB0Q29yZS9kZmcvREZHQWJzdHJhY3RJbnRlcnByZXRlcklubGluZXMuaAkod29ya2luZyBjb3B5 KQpAQCAtMjg3OCw2ICsyODc4LDE0IEBAIGJvb2wgQWJzdHJhY3RJbnRlcnByZXRlcjxBYnN0cmFj dFN0YXRlVHkKICAgICAgICAgYnJlYWs7CiAKICAgICBjYXNlIFVucmVhY2hhYmxlOgorICAgICAg ICAvLyBJdCBtYXkgYmUgdGhhdCBkdXJpbmcgYSBwcmV2aW91cyBydW4gb2YgQUkgd2UgcHJvdmVk IHRoYXQgc29tZXRoaW5nIHdhcyB1bnJlYWNoYWJsZSwgYnV0CisgICAgICAgIC8vIGR1cmluZyB0 aGlzIHJ1biBvZiBBSSB3ZSBmb3JnZXQgdGhhdCBpdCdzIHVucmVhY2hhYmxlLiBBSSdzIHByb29m cyBkb24ndCBoYXZlIHRvIGdldAorICAgICAgICAvLyBtb25vdGluaWNhbGx5IHN0cm9uZ2VyIG92 ZXIgdGltZS4gU28sIHdlIGRvbid0IGFzc2VydCB0aGF0IEFJIGRvZXNuJ3QgcmVhY2ggdGhlCisg ICAgICAgIC8vIFVucmVhY2hhYmxlLiBXZSBoYXZlIG5vIGNob2ljZSBidXQgdG8gdGFrZSBvdXIg cGFzdCBwcm9vZiBhdCBmYWNlIHZhbHVlLiBPdGhlcndpc2Ugd2UnbGwKKyAgICAgICAgLy8gY3Jh c2ggd2hlbmV2ZXIgQUkgZmFpbHMgdG8gYmUgYXMgcG93ZXJmdWwgb24gcnVuIEsgYXMgaXQgd2Fz IG9uIHJ1biBLLTEuCisgICAgICAgIG1fc3RhdGUuc2V0SXNWYWxpZChmYWxzZSk7CisgICAgICAg IGJyZWFrOworICAgICAgICAKICAgICBjYXNlIExhc3ROb2RlVHlwZToKICAgICBjYXNlIEFyaXRo SU11bDoKICAgICBjYXNlIEZpYXRJbnQ1MjoK