Clean up implication logic and do more caching (#2530)

Summary:
Release note: none

This attempts to reduce exponential blowup in the simplifier by doing more caching while computing implications and by imposing a depth limit on the number of simplify and implies calls.

It also tries to make implies and impliesNot more symmetrical, so that things are less ad-hoc.
Pull Request resolved: https://github.com/facebook/prepack/pull/2530

Differential Revision: D9664026

Pulled By: hermanventer

fbshipit-source-id: f7a9135b06298a2b77ad05bf377982a9b37e4ad1
This commit is contained in:
Herman Venter 2018-09-06 15:23:39 -07:00 committed by Facebook Github Bot
parent f319df5d8c
commit 96174b5ebf
7 changed files with 321 additions and 210 deletions

View File

@ -60,7 +60,10 @@ function runTest(name: string, config: any) {
mkdirp.sync(`${__dirname}/../fb-www`); mkdirp.sync(`${__dirname}/../fb-www`);
fs.writeFileSync(`${__dirname}/../fb-www/input.js`, sourceCode, "utf8"); fs.writeFileSync(`${__dirname}/../fb-www/input.js`, sourceCode, "utf8");
execSync(`${__dirname}/../../third-party/node/bin/node scripts/debug-fb-www.js`, { stdio: "inherit" }); execSync(
`${__dirname}/../../third-party/node/bin/node --max_old_space_size=16384 --heap-growing-percent=50 scripts/debug-fb-www.js `,
{ stdio: "inherit" }
);
console.log("\n\n\n"); console.log("\n\n\n");
console.log("-----------------------------"); console.log("-----------------------------");

View File

@ -354,8 +354,8 @@ export type DebugServerType = {
}; };
export type PathType = { export type PathType = {
implies(condition: Value): boolean, implies(condition: Value, depth?: number): boolean,
impliesNot(condition: Value): boolean, impliesNot(condition: Value, depth?: number): boolean,
withCondition<T>(condition: Value, evaluate: () => T): T, withCondition<T>(condition: Value, evaluate: () => T): T,
withInverseCondition<T>(condition: Value, evaluate: () => T): T, withInverseCondition<T>(condition: Value, evaluate: () => T): T,
pushAndRefine(condition: Value): void, pushAndRefine(condition: Value): void,
@ -365,11 +365,11 @@ export type PathType = {
export class PathConditions { export class PathConditions {
add(c: AbstractValue): void {} add(c: AbstractValue): void {}
implies(e: AbstractValue): boolean { implies(e: Value, depth: number = 0): boolean {
return false; return false;
} }
impliesNot(e: AbstractValue): boolean { impliesNot(e: Value, depth: number = 0): boolean {
return false; return false;
} }

View File

@ -34,43 +34,114 @@ export class PathConditionsImplementation extends PathConditions {
this._assumedConditions.add(c); this._assumedConditions.add(c);
} }
implies(e: AbstractValue): boolean { implies(e: Value, depth: number = 0): boolean {
if (!e.mightNotBeTrue()) return true;
if (!e.mightNotBeFalse()) return false;
invariant(e instanceof AbstractValue);
if (this._assumedConditions.has(e)) return true; if (this._assumedConditions.has(e)) return true;
if (this._impliedConditions !== undefined && this._impliedConditions.has(e)) return true; if (this._impliedConditions !== undefined && this._impliedConditions.has(e)) return true;
if (this._impliedNegatives !== undefined && this._impliedNegatives.has(e)) return false; if (this._impliedNegatives !== undefined && this._impliedNegatives.has(e)) return false;
if (this._failedImplications !== undefined && this._failedImplications.has(e)) return false; if (this._failedImplications !== undefined && this._failedImplications.has(e)) return false;
if (this._baseConditions !== undefined && this._baseConditions.implies(e)) return true; if (this._baseConditions !== undefined && this._baseConditions.implies(e, depth + 1)) return true;
for (let assumedCondition of this._assumedConditions) { for (let assumedCondition of this._assumedConditions) {
if (assumedCondition.implies(e)) { if (assumedCondition.implies(e, depth + 1)) return this.cacheImplicationSuccess(e);
if (this._impliedConditions === undefined) this._impliedConditions = new Set();
this._impliedConditions.add(e);
return true;
}
} }
// Do this here to prevent infinite recursion
if (this._failedImplications === undefined) this._failedImplications = new Set(); if (this._failedImplications === undefined) this._failedImplications = new Set();
this._failedImplications.add(e); this._failedImplications.add(e);
// implication success entries trump failed implications entries
if (e.kind === "||") {
let [x, y] = e.args;
// this => x || true, regardless of the value of x
// this => true || y, regardless of the value of y
if (!x.mightNotBeTrue() || !y.mightNotBeTrue()) return this.cacheImplicationSuccess(e);
// this => false || y, if this => y
if (!x.mightNotBeFalse() && this.implies(y, depth + 1)) return this.cacheImplicationSuccess(e);
// this => x || false if this => x
if (!y.mightNotBeFalse() && this.implies(x, depth + 1)) return this.cacheImplicationSuccess(e);
// this => x || y if this => x
if (this.implies(x, depth + 1)) return this.cacheImplicationSuccess(e);
// this => x || y if this => y
if (this.implies(y, depth + 1)) return this.cacheImplicationSuccess(e);
}
if (e.kind === "!==" || e.kind === "!=") {
let [x, y] = e.args;
if (x instanceof AbstractValue) {
// this => x !== null && x !== undefined, if this => x
// this => x != null && x != undefined, if this => x
if ((y instanceof NullValue || y instanceof UndefinedValue) && this.implies(x, depth + 1))
return this.cacheImplicationSuccess(e);
} else {
invariant(y instanceof AbstractValue); // otherwise e would have been simplied
// this => null !== y && undefined !== y, if this => y
// this => null != y && undefined != y, if this => y
if ((x instanceof NullValue || x instanceof UndefinedValue) && this.implies(y, depth + 1))
return this.cacheImplicationSuccess(e);
}
}
return false; return false;
} }
impliesNot(e: AbstractValue): boolean { cacheImplicationSuccess(e: AbstractValue): true {
if (this._impliedConditions === undefined) this._impliedConditions = new Set();
this._impliedConditions.add(e);
return true;
}
impliesNot(e: Value, depth: number = 0): boolean {
if (!e.mightNotBeTrue()) return false;
if (!e.mightNotBeFalse()) return true;
invariant(e instanceof AbstractValue);
if (this._assumedConditions.has(e)) return false; if (this._assumedConditions.has(e)) return false;
if (this._impliedConditions !== undefined && this._impliedConditions.has(e)) return false; if (this._impliedConditions !== undefined && this._impliedConditions.has(e)) return false;
if (this._impliedNegatives !== undefined && this._impliedNegatives.has(e)) return true; if (this._impliedNegatives !== undefined && this._impliedNegatives.has(e)) return true;
if (this._failedNegativeImplications !== undefined && this._failedNegativeImplications.has(e)) return false; if (this._failedNegativeImplications !== undefined && this._failedNegativeImplications.has(e)) return false;
if (this._baseConditions !== undefined && this._baseConditions.impliesNot(e)) return true; if (this._baseConditions !== undefined && this._baseConditions.impliesNot(e, depth + 1)) return true;
for (let assumedCondition of this._assumedConditions) { for (let assumedCondition of this._assumedConditions) {
invariant(assumedCondition !== undefined); if (assumedCondition.impliesNot(e, depth + 1)) return this.cacheNegativeImplicationSuccess(e);
if (assumedCondition.impliesNot(e)) {
if (this._impliedNegatives === undefined) this._impliedNegatives = new Set();
this._impliedNegatives.add(e);
return true;
}
} }
// Do this here to prevent infinite recursion
if (this._failedNegativeImplications === undefined) this._failedNegativeImplications = new Set(); if (this._failedNegativeImplications === undefined) this._failedNegativeImplications = new Set();
this._failedNegativeImplications.add(e); this._failedNegativeImplications.add(e);
// negative implication success entries trump failed negative implications entries
if (e.kind === "&&") {
let [x, y] = e.args;
// this => !(false && y) regardless of the value of y
// this => !(x && false) regardless of the value of x
if (!x.mightNotBeFalse() || !y.mightNotBeFalse()) return this.cacheNegativeImplicationSuccess(e);
// this => !(true && y), if this => !y
if (!x.mightNotBeTrue() && this.impliesNot(y, depth + 1)) return this.cacheNegativeImplicationSuccess(e);
// this => !(x && true) if this => !x
if (!y.mightNotBeTrue() && this.impliesNot(x, depth + 1)) return this.cacheNegativeImplicationSuccess(e);
// this => !(x && y) if this => !x
if (this.impliesNot(x, depth + 1)) return this.cacheNegativeImplicationSuccess(e);
// this => !(x && y) if this => !y
if (this.impliesNot(y, depth + 1)) return this.cacheNegativeImplicationSuccess(e);
}
if (e.kind === "===" || e.kind === "==") {
let [x, y] = e.args;
if (x instanceof AbstractValue) {
// this => !(x === null) && !(x === undefined), if this => x
// this => !(x == null) && !(x == undefined), if this => x
if ((y instanceof NullValue || y instanceof UndefinedValue) && this.implies(x))
return this.cacheNegativeImplicationSuccess(e);
} else {
invariant(y instanceof AbstractValue); // otherwise e would have been simplied
// this => !(null === y) && !(undefined === y), if this => y
// this => !(null == y) && !(undefined == y), if this => y
if ((x instanceof NullValue || x instanceof UndefinedValue) && this.implies(y))
return this.cacheNegativeImplicationSuccess(e);
}
}
return false; return false;
} }
cacheNegativeImplicationSuccess(e: AbstractValue): true {
if (this._impliedNegatives === undefined) this._impliedNegatives = new Set();
this._impliedNegatives.add(e);
return true;
}
isEmpty(): boolean { isEmpty(): boolean {
return this._assumedConditions.size === 0; return this._assumedConditions.size === 0;
} }
@ -83,15 +154,16 @@ export class PathConditionsImplementation extends PathConditions {
return this._assumedConditions; return this._assumedConditions;
} }
refineBaseConditons(realm: Realm): void { refineBaseConditons(realm: Realm, totalRefinements: number = 0): void {
if (realm.abstractValueImpliesMax > 0) return; if (realm.abstractValueImpliesMax > 0) return;
let total = totalRefinements;
let refine = (condition: AbstractValue) => { let refine = (condition: AbstractValue) => {
let refinedCondition = realm.simplifyAndRefineAbstractCondition(condition); let refinedCondition = realm.simplifyAndRefineAbstractCondition(condition);
if (refinedCondition !== condition) { if (refinedCondition !== condition) {
if (!refinedCondition.mightNotBeFalse()) throw new InfeasiblePathError(); if (!refinedCondition.mightNotBeFalse()) throw new InfeasiblePathError();
if (refinedCondition instanceof AbstractValue) { if (refinedCondition instanceof AbstractValue) {
this.add(refinedCondition); this.add(refinedCondition);
// These might have different answers now that we've add another path condition // These might have different answers now that we're adding another path condition
this._failedImplications = undefined; this._failedImplications = undefined;
this._failedNegativeImplications = undefined; this._failedNegativeImplications = undefined;
} }
@ -103,30 +175,31 @@ export class PathConditionsImplementation extends PathConditions {
this._baseConditions = undefined; this._baseConditions = undefined;
for (let assumedCondition of savedBaseConditions._assumedConditions) { for (let assumedCondition of savedBaseConditions._assumedConditions) {
if (assumedCondition.kind === "||") { if (assumedCondition.kind === "||") {
if (++total > 4) break;
refine(assumedCondition); refine(assumedCondition);
} }
} }
} finally { } finally {
this._baseConditions = savedBaseConditions; this._baseConditions = savedBaseConditions;
} }
savedBaseConditions.refineBaseConditons(realm); savedBaseConditions.refineBaseConditons(realm, total);
} }
} }
} }
export class PathImplementation { export class PathImplementation {
implies(condition: Value): boolean { implies(condition: Value, depth: number = 0): boolean {
if (!condition.mightNotBeTrue()) return true; // any path implies true if (!condition.mightNotBeTrue()) return true; // any path implies true
if (!condition.mightNotBeFalse()) return false; // no path condition is false if (!condition.mightNotBeFalse()) return false; // no path condition is false
invariant(condition instanceof AbstractValue); invariant(condition instanceof AbstractValue);
return condition.$Realm.pathConditions.implies(condition); return condition.$Realm.pathConditions.implies(condition, depth);
} }
impliesNot(condition: Value): boolean { impliesNot(condition: Value, depth: number = 0): boolean {
if (!condition.mightNotBeFalse()) return true; // any path implies !false if (!condition.mightNotBeFalse()) return true; // any path implies !false
if (!condition.mightNotBeTrue()) return false; // no path condition is false, so none can imply !true if (!condition.mightNotBeTrue()) return false; // no path condition is false, so none can imply !true
invariant(condition instanceof AbstractValue); invariant(condition instanceof AbstractValue);
return condition.$Realm.pathConditions.impliesNot(condition); return condition.$Realm.pathConditions.impliesNot(condition, depth);
} }
withCondition<T>(condition: Value, evaluate: () => T): T { withCondition<T>(condition: Value, evaluate: () => T): T {

View File

@ -41,7 +41,7 @@ export default function simplifyAndRefineAbstractValue(
} }
throw new FatalError(); throw new FatalError();
}; };
let result = simplify(realm, value, isCondition); let result = simplify(realm, value, isCondition, 0);
if (result !== value) realm.statistics.simplifications++; if (result !== value) realm.statistics.simplifications++;
return result; return result;
} catch (e) { } catch (e) {
@ -63,12 +63,12 @@ export default function simplifyAndRefineAbstractValue(
} }
} }
function simplify(realm, value: Value, isCondition: boolean = false): Value { function simplify(realm, value: Value, isCondition: boolean = false, depth: number): Value {
if (value instanceof ConcreteValue) return value; if (value instanceof ConcreteValue || depth > 5) return value;
invariant(value instanceof AbstractValue); invariant(value instanceof AbstractValue);
if (isCondition || value.getType() === BooleanValue) { if (isCondition || value.getType() === BooleanValue) {
if (Path.implies(value)) return realm.intrinsics.true; if (Path.implies(value, depth + 1)) return realm.intrinsics.true;
if (Path.impliesNot(value)) return realm.intrinsics.false; if (Path.impliesNot(value, depth + 1)) return realm.intrinsics.false;
} }
let loc = value.expressionLocation; let loc = value.expressionLocation;
let op = value.kind; let op = value.kind;
@ -79,16 +79,16 @@ function simplify(realm, value: Value, isCondition: boolean = false): Value {
if (x0.kind === "!") { if (x0.kind === "!") {
invariant(x0 instanceof AbstractValue); invariant(x0 instanceof AbstractValue);
let [x00] = x0.args; let [x00] = x0.args;
let xx = simplify(realm, x00, true); let xx = simplify(realm, x00, true, depth + 1);
if (isCondition || xx.getType() === BooleanValue) return xx; if (isCondition || xx.getType() === BooleanValue) return xx;
} }
return negate(realm, x0, loc, value, isCondition); return negate(realm, x0, depth + 1, loc, value, isCondition);
} }
case "||": case "||":
case "&&": { case "&&": {
let [x0, y0] = value.args; let [x0, y0] = value.args;
let x = simplify(realm, x0, isCondition); let x = simplify(realm, x0, isCondition, depth + 1);
let y = simplify(realm, y0, isCondition); let y = simplify(realm, y0, isCondition, depth + 1);
if (x instanceof AbstractValue && x.equals(y)) return x; if (x instanceof AbstractValue && x.equals(y)) return x;
// true && y <=> y // true && y <=> y
// true || y <=> true // true || y <=> true
@ -181,29 +181,29 @@ function simplify(realm, value: Value, isCondition: boolean = false): Value {
case ">": case ">":
case ">=": case ">=":
return distributeConditional(realm, value, isCondition, args => return distributeConditional(realm, value, isCondition, args =>
AbstractValue.createFromBinaryOp(realm, op, args[0], args[1], loc, undefined, isCondition) AbstractValue.createFromBinaryOp(realm, op, args[0], args[1], loc, undefined, isCondition, true)
); );
case "==": case "==":
case "!=": case "!=":
case "===": case "===":
case "!==": case "!==":
return simplifyEquality(realm, value); return simplifyEquality(realm, value, depth + 1);
case "conditional": { case "conditional": {
let [c0, x0, y0] = value.args; let [c0, x0, y0] = value.args;
let c = simplify(realm, c0, true); let c = simplify(realm, c0, true, depth + 1);
let x, y; let x, y;
if (c0 instanceof AbstractValue && c.mightBeFalse() && c.mightBeTrue()) { if (c0 instanceof AbstractValue && c.mightBeFalse() && c.mightBeTrue()) {
try { try {
x = Path.withCondition(c0, () => simplify(realm, x0, isCondition)); x = Path.withCondition(c0, () => simplify(realm, x0, isCondition, depth + 1));
} catch (e) { } catch (e) {
if (e instanceof InfeasiblePathError) { if (e instanceof InfeasiblePathError) {
// We now know that c0 cannot be be true on this path // We now know that c0 cannot be be true on this path
return simplify(realm, y0, isCondition); return simplify(realm, y0, isCondition, depth + 1);
} }
throw e; throw e;
} }
try { try {
y = Path.withInverseCondition(c0, () => simplify(realm, y0, isCondition)); y = Path.withInverseCondition(c0, () => simplify(realm, y0, isCondition, depth + 1));
} catch (e) { } catch (e) {
if (e instanceof InfeasiblePathError) { if (e instanceof InfeasiblePathError) {
// We now know that c0 cannot be be false on this path // We now know that c0 cannot be be false on this path
@ -214,31 +214,33 @@ function simplify(realm, value: Value, isCondition: boolean = false): Value {
} }
let cIsFalse = !c.mightNotBeFalse(); let cIsFalse = !c.mightNotBeFalse();
let cIsTrue = !c.mightNotBeTrue(); let cIsTrue = !c.mightNotBeTrue();
if (x === undefined && !cIsFalse) x = simplify(realm, x0, isCondition); if (x === undefined && !cIsFalse) x = simplify(realm, x0, isCondition, depth + 1);
if (cIsTrue) { if (cIsTrue) {
invariant(x !== undefined); // cIsTrue ==> !cIsFalse invariant(x !== undefined); // cIsTrue ==> !cIsFalse
return x; return x;
} }
if (y === undefined) y = simplify(realm, y0, isCondition); if (y === undefined) y = simplify(realm, y0, isCondition, depth + 1);
if (cIsFalse) return y; if (cIsFalse) return y;
invariant(x !== undefined); // because !csIsFalse invariant(x !== undefined); // because !csIsFalse
invariant(c instanceof AbstractValue); invariant(c instanceof AbstractValue);
if (Path.implies(c)) return x; if (Path.implies(c, depth + 1)) return x;
let notc = AbstractValue.createFromUnaryOp(realm, "!", c, true, loc, isCondition, true); let notc = AbstractValue.createFromUnaryOp(realm, "!", c, true, loc, isCondition, true);
if (!notc.mightNotBeTrue()) return y; if (!notc.mightNotBeTrue()) return y;
if (!notc.mightNotBeFalse()) return x; if (!notc.mightNotBeFalse()) return x;
invariant(notc instanceof AbstractValue); invariant(notc instanceof AbstractValue);
if (Path.implies(notc)) return y; if (Path.implies(notc, depth + 1)) return y;
if (!isCondition) { if (!isCondition) {
if (Path.implies(AbstractValue.createFromBinaryOp(realm, "===", value, x))) return x; if (Path.implies(AbstractValue.createFromBinaryOp(realm, "===", value, x), depth + 1)) return x;
if (!x.mightBeNumber() && Path.implies(AbstractValue.createFromBinaryOp(realm, "!==", value, x))) return y; if (!x.mightBeNumber() && Path.implies(AbstractValue.createFromBinaryOp(realm, "!==", value, x), depth + 1))
if (!y.mightBeNumber() && Path.implies(AbstractValue.createFromBinaryOp(realm, "!==", value, y))) return x; return y;
if (Path.implies(AbstractValue.createFromBinaryOp(realm, "===", value, y))) return y; if (!y.mightBeNumber() && Path.implies(AbstractValue.createFromBinaryOp(realm, "!==", value, y), depth + 1))
return x;
if (Path.implies(AbstractValue.createFromBinaryOp(realm, "===", value, y), depth + 1)) return y;
} }
// c ? x : x <=> x // c ? x : x <=> x
if (x.equals(y)) return x; if (x.equals(y)) return x;
// x ? x : y <=> x || y // x ? x : y <=> x || y
let cs = isCondition ? c : simplify(realm, c0); let cs = isCondition ? c : simplify(realm, c0, false, depth + 1);
if (cs.equals(x)) return AbstractValue.createFromLogicalOp(realm, "||", x, y, loc, isCondition, true); if (cs.equals(x)) return AbstractValue.createFromLogicalOp(realm, "||", x, y, loc, isCondition, true);
// y ? x : y <=> y && x // y ? x : y <=> y && x
if (cs.equals(y)) return AbstractValue.createFromLogicalOp(realm, "&&", y, x, loc, isCondition, true); if (cs.equals(y)) return AbstractValue.createFromLogicalOp(realm, "&&", y, x, loc, isCondition, true);
@ -271,8 +273,9 @@ function simplify(realm, value: Value, isCondition: boolean = false): Value {
invariant(abstractValue instanceof AbstractValue); invariant(abstractValue instanceof AbstractValue);
let remainingConcreteValues = []; let remainingConcreteValues = [];
for (let concreteValue of concreteValues) { for (let concreteValue of concreteValues) {
if (Path.implies(AbstractValue.createFromBinaryOp(realm, "!==", value, concreteValue))) continue; if (Path.implies(AbstractValue.createFromBinaryOp(realm, "!==", value, concreteValue), depth + 1)) continue;
if (Path.implies(AbstractValue.createFromBinaryOp(realm, "===", value, concreteValue))) return concreteValue; if (Path.implies(AbstractValue.createFromBinaryOp(realm, "===", value, concreteValue), depth + 1))
return concreteValue;
remainingConcreteValues.push(concreteValue); remainingConcreteValues.push(concreteValue);
} }
if (remainingConcreteValues.length === 0) return abstractValue; if (remainingConcreteValues.length === 0) return abstractValue;
@ -327,8 +330,8 @@ function simplifyNullCheck(
realm: Realm, realm: Realm,
op: "===" | "==" | "!==" | "!=", op: "===" | "==" | "!==" | "!=",
value: Value, value: Value,
loc: ?BabelNodeSourceLocation, depth: number,
depthCounter?: number = 0 loc: ?BabelNodeSourceLocation
): void | Value { ): void | Value {
if (op === "==" || op === "!=") { if (op === "==" || op === "!=") {
if (!value.mightNotBeNull() || !value.mightNotBeUndefined()) if (!value.mightNotBeNull() || !value.mightNotBeUndefined())
@ -342,13 +345,13 @@ function simplifyNullCheck(
invariant(value instanceof AbstractValue); // concrete values will either be null or not null invariant(value instanceof AbstractValue); // concrete values will either be null or not null
// try to simplify "(cond ? x : y) op null" to just "cond" or "!cond" // try to simplify "(cond ? x : y) op null" to just "cond" or "!cond"
// failing that, use "cond ? x op null : y op null" if either of the subexpressions simplify // failing that, use "cond ? x op null : y op null" if either of the subexpressions simplify
if (value.kind === "conditional" && depthCounter < 10) { if (value.kind === "conditional" && depth < 10) {
let [cond, x, y] = value.args; let [cond, x, y] = value.args;
let sx = simplifyNullCheck(realm, op, x, loc, depthCounter + 1); let sx = simplifyNullCheck(realm, op, x, depth + 1, loc);
let sy = simplifyNullCheck(realm, op, y, loc, depthCounter + 1); let sy = simplifyNullCheck(realm, op, y, depth + 1, loc);
if (sx !== undefined && sy !== undefined) { if (sx !== undefined && sy !== undefined) {
if (!sx.mightNotBeTrue() && !sy.mightNotBeFalse()) return makeBoolean(realm, cond, loc); if (!sx.mightNotBeTrue() && !sy.mightNotBeFalse()) return makeBoolean(realm, cond, loc);
if (!sx.mightNotBeFalse() && !sy.mightNotBeTrue()) return negate(realm, cond, loc); if (!sx.mightNotBeFalse() && !sy.mightNotBeTrue()) return negate(realm, cond, depth + 1, loc);
} }
if (sx !== undefined || sy !== undefined) { if (sx !== undefined || sy !== undefined) {
if (sx === undefined) if (sx === undefined)
@ -382,8 +385,8 @@ function simplifyUndefinedCheck(
realm: Realm, realm: Realm,
op: "===" | "==" | "!==" | "!=", op: "===" | "==" | "!==" | "!=",
value: Value, value: Value,
loc: ?BabelNodeSourceLocation, depth: number,
depthCounter?: number = 0 loc: ?BabelNodeSourceLocation
): void | Value { ): void | Value {
if (op === "==" || op === "!=") { if (op === "==" || op === "!=") {
if (!value.mightNotBeNull() || !value.mightNotBeUndefined()) if (!value.mightNotBeNull() || !value.mightNotBeUndefined())
@ -397,13 +400,13 @@ function simplifyUndefinedCheck(
invariant(value instanceof AbstractValue); // concrete values will either be undefined or not undefined invariant(value instanceof AbstractValue); // concrete values will either be undefined or not undefined
// try to simplify "(cond ? x : y) op undefined" to just "cond" or "!cond" // try to simplify "(cond ? x : y) op undefined" to just "cond" or "!cond"
// failing that, use "cond ? x op undefined : y op undefined" if either of the subexpressions simplify // failing that, use "cond ? x op undefined : y op undefined" if either of the subexpressions simplify
if (value.kind === "conditional" && depthCounter < 10) { if (value.kind === "conditional" && depth < 10) {
let [cond, x, y] = value.args; let [cond, x, y] = value.args;
let sx = simplifyUndefinedCheck(realm, op, x, loc, depthCounter + 1); let sx = simplifyUndefinedCheck(realm, op, x, depth + 1, loc);
let sy = simplifyUndefinedCheck(realm, op, y, loc, depthCounter + 1); let sy = simplifyUndefinedCheck(realm, op, y, depth + 1, loc);
if (sx !== undefined && sy !== undefined) { if (sx !== undefined && sy !== undefined) {
if (!sx.mightNotBeTrue() && !sy.mightNotBeFalse()) return makeBoolean(realm, cond, loc); if (!sx.mightNotBeTrue() && !sy.mightNotBeFalse()) return makeBoolean(realm, cond, loc);
if (!sx.mightNotBeFalse() && !sy.mightNotBeTrue()) return negate(realm, cond, loc); if (!sx.mightNotBeFalse() && !sy.mightNotBeTrue()) return negate(realm, cond, depth + 1, loc);
} }
if (sx !== undefined || sy !== undefined) { if (sx !== undefined || sy !== undefined) {
if (sx === undefined) if (sx === undefined)
@ -433,7 +436,7 @@ function simplifyUndefinedCheck(
} }
} }
function simplifyEquality(realm: Realm, equality: AbstractValue): Value { function simplifyEquality(realm: Realm, equality: AbstractValue, depth: number): Value {
let loc = equality.expressionLocation; let loc = equality.expressionLocation;
let op = equality.kind; let op = equality.kind;
let [x, y] = equality.args; let [x, y] = equality.args;
@ -441,19 +444,19 @@ function simplifyEquality(realm: Realm, equality: AbstractValue): Value {
if (x instanceof ConcreteValue) [x, y] = [y, x]; if (x instanceof ConcreteValue) [x, y] = [y, x];
if (op === "===" || op === "==" || op === "!==" || op === "==") { if (op === "===" || op === "==" || op === "!==" || op === "==") {
if (!x.mightNotBeNull()) { if (!x.mightNotBeNull()) {
let sy = simplifyNullCheck(realm, op, y); let sy = simplifyNullCheck(realm, op, y, depth + 1);
if (sy !== undefined) return sy; if (sy !== undefined) return sy;
} }
if (!y.mightNotBeNull()) { if (!y.mightNotBeNull()) {
let sx = simplifyNullCheck(realm, op, x); let sx = simplifyNullCheck(realm, op, x, depth + 1);
if (sx !== undefined) return sx; if (sx !== undefined) return sx;
} }
if (!x.mightNotBeUndefined()) { if (!x.mightNotBeUndefined()) {
let sy = simplifyUndefinedCheck(realm, op, y); let sy = simplifyUndefinedCheck(realm, op, y, depth + 1);
if (sy !== undefined) return sy; if (sy !== undefined) return sy;
} }
if (!y.mightNotBeUndefined()) { if (!y.mightNotBeUndefined()) {
let sx = simplifyUndefinedCheck(realm, op, x); let sx = simplifyUndefinedCheck(realm, op, x, depth + 1);
if (sx !== undefined) return sx; if (sx !== undefined) return sx;
} }
} }
@ -473,13 +476,13 @@ function simplifyEquality(realm: Realm, equality: AbstractValue): Value {
// ((cond ? xx : xy) === y) && xx === y && xy !== y <=> cond // ((cond ? xx : xy) === y) && xx === y && xy !== y <=> cond
if (xx.equals(y) && !xy.equals(y)) return cond; if (xx.equals(y) && !xy.equals(y)) return cond;
// ((!cond ? xx : xy) === y) && xx !== y && xy === y <=> !cond // ((!cond ? xx : xy) === y) && xx !== y && xy === y <=> !cond
if (!xx.equals(y) && xy.equals(y)) return negate(realm, cond, loc); if (!xx.equals(y) && xy.equals(y)) return negate(realm, cond, depth + 1, loc);
} else if (y instanceof AbstractValue && y.kind === "conditional") { } else if (y instanceof AbstractValue && y.kind === "conditional") {
let [cond, yx, yy] = y.args; let [cond, yx, yy] = y.args;
// (x === (cond ? yx : yy) === y) && x === yx && x !== yy <=> cond // (x === (cond ? yx : yy) === y) && x === yx && x !== yy <=> cond
if (yx.equals(x) && !yy.equals(x)) return cond; if (yx.equals(x) && !yy.equals(x)) return cond;
// (x === (!cond ? yx : yy) === y) && x !== yx && x === yy <=> !cond // (x === (!cond ? yx : yy) === y) && x !== yx && x === yy <=> !cond
if (!x.equals(yx) && x.equals(yy)) return negate(realm, cond, loc); if (!x.equals(yx) && x.equals(yy)) return negate(realm, cond, depth + 1, loc);
} }
} else if (op === "==") { } else if (op === "==") {
let xType = x.getType(); let xType = x.getType();
@ -511,19 +514,20 @@ function makeBoolean(realm: Realm, value: Value, loc: ?BabelNodeSourceLocation =
function negate( function negate(
realm: Realm, realm: Realm,
value: Value, value: Value,
depth: number = 0,
loc: ?BabelNodeSourceLocation = undefined, loc: ?BabelNodeSourceLocation = undefined,
unsimplifiedNegation: void | Value = undefined, unsimplifiedNegation: void | Value = undefined,
isCondition?: boolean isCondition?: boolean
): Value { ): Value {
if (value instanceof ConcreteValue) return ValuesDomain.computeUnary(realm, "!", value); if (value instanceof ConcreteValue) return ValuesDomain.computeUnary(realm, "!", value);
invariant(value instanceof AbstractValue); invariant(value instanceof AbstractValue);
value = simplify(realm, value, true); value = simplify(realm, value, true, depth + 1);
if (!value.mightNotBeTrue()) return realm.intrinsics.false; if (!value.mightNotBeTrue()) return realm.intrinsics.false;
if (!value.mightNotBeFalse()) return realm.intrinsics.true; if (!value.mightNotBeFalse()) return realm.intrinsics.true;
invariant(value instanceof AbstractValue); invariant(value instanceof AbstractValue);
if (value.kind === "!") { if (value.kind === "!") {
let [x] = value.args; let [x] = value.args;
if (isCondition || x.getType() === BooleanValue) return simplify(realm, x, true); if (isCondition || x.getType() === BooleanValue) return simplify(realm, x, true, depth + 1);
if (unsimplifiedNegation !== undefined) return unsimplifiedNegation; if (unsimplifiedNegation !== undefined) return unsimplifiedNegation;
return makeBoolean(realm, x, loc); return makeBoolean(realm, x, loc);
} }
@ -559,8 +563,8 @@ function negate(
break; break;
} }
if (invertedComparison !== undefined) { if (invertedComparison !== undefined) {
let left = simplify(realm, value.args[0]); let left = simplify(realm, value.args[0], false, depth + 1);
let right = simplify(realm, value.args[1]); let right = simplify(realm, value.args[1], false, depth + 1);
return AbstractValue.createFromBinaryOp(realm, invertedComparison, left, right, loc || value.expressionLocation); return AbstractValue.createFromBinaryOp(realm, invertedComparison, left, right, loc || value.expressionLocation);
} }
let invertedLogicalOp; let invertedLogicalOp;
@ -575,8 +579,8 @@ function negate(
break; break;
} }
if (invertedLogicalOp !== undefined) { if (invertedLogicalOp !== undefined) {
let left = negate(realm, value.args[0]); let left = negate(realm, value.args[0], depth + 1);
let right = negate(realm, value.args[1]); let right = negate(realm, value.args[1], depth + 1);
return AbstractValue.createFromLogicalOp( return AbstractValue.createFromLogicalOp(
realm, realm,
invertedLogicalOp, invertedLogicalOp,

View File

@ -215,154 +215,186 @@ export default class AbstractValue extends Value {
} }
// this => val. A false value does not imply that !(this => val). // this => val. A false value does not imply that !(this => val).
implies(val: Value): boolean { implies(val: AbstractValue, depth: number = 0): boolean {
if (depth > 5) return false;
if (this.equals(val)) return true; // x => x regardless of its value if (this.equals(val)) return true; // x => x regardless of its value
if (!this.mightNotBeFalse()) return true; // false => val if (this.kind === "||") {
if (!val.mightNotBeTrue()) return true; // x => true regardless of the value of x let [x, y] = this.args;
if (val instanceof AbstractValue) { let xi =
// Neither this (x) nor val (y) is a known value, so we need to do some reasoning based on the structure x.implies(val, depth + 1) ||
// x => x || y (x instanceof AbstractValue && this.$Realm.pathConditions.impliesNot(x, depth + 1));
if (val.kind === "||") { if (!xi) return false;
let [x, y] = val.args; let yi =
return this.implies(x) || this.implies(y); y.implies(val, depth + 1) ||
(y instanceof AbstractValue && this.$Realm.pathConditions.impliesNot(y, depth + 1));
return yi;
} else if (this.kind === "&&") {
let [x, y] = this.args;
let xi =
x.implies(val, depth + 1) ||
(x instanceof AbstractValue && this.$Realm.pathConditions.impliesNot(x, depth + 1));
if (xi) return true;
let yi =
y.implies(val, depth + 1) ||
(y instanceof AbstractValue && this.$Realm.pathConditions.impliesNot(y, depth + 1));
return yi;
} else if (this.kind === "!") {
let [nx] = this.args;
invariant(nx instanceof AbstractValue);
if (nx.kind === "!") {
// !!x => val if x => val
let [x] = nx.args;
invariant(x instanceof AbstractValue);
return x.implies(val, depth + 1);
}
} else if (this.kind === "conditional") {
let [c, x, y] = this.args;
// (c ? x : y) => val if x is true and y is false and c = val
if (!x.mightNotBeTrue() && !y.mightNotBeFalse()) {
return c.equals(val);
} }
// x => !y if y => !x
if (val.kind === "!") {
let [y] = val.args;
invariant(y instanceof AbstractValue);
return y.impliesNot(this);
}
// x => x !== null && x !== undefined
// x => x != null && x != undefined
if (val.kind === "!==" || val.kind === "!=") { if (val.kind === "!==" || val.kind === "!=") {
let [x, y] = val.args; let [vx, vy] = val.args;
if (this.implies(x)) return y instanceof NullValue || y instanceof UndefinedValue; if (!x.mightNotBeFalse()) {
if (this.implies(y)) return x instanceof NullValue || x instanceof UndefinedValue; // (c ? false : y) => vx !== undefined && vx !== null if y => vx, since val is false unless y is true
} if (vx instanceof AbstractValue && (vy instanceof NullValue || vy instanceof UndefinedValue))
if (this.kind === "!") { return y.implies(vx, depth + 1);
let [nx] = this.args; // (c ? false : y) => undefined !== vy && null !== vy if y => vy, since val is false unless y is true
invariant(nx instanceof AbstractValue); if ((vx instanceof NullValue || vx instanceof UndefinedValue) && vy instanceof AbstractValue)
if (nx.kind === "!") { return y.implies(vy, depth + 1);
// !!x => y if x => y } else if (!y.mightNotBeFalse()) {
let [x] = nx.args; // (c ? x : false) => vx !== undefined && vx !== null if x => vx, since val is false unless x is true
invariant(x instanceof AbstractValue); if (vx instanceof AbstractValue && (vy instanceof NullValue || vy instanceof UndefinedValue))
return x.implies(val); return x.implies(vx, depth + 1);
// (c ? x : false) => undefined !== vy && null !== vy if x => vy, since val is false unless x is true
if ((vx instanceof NullValue || vx instanceof UndefinedValue) && vy instanceof AbstractValue)
return x.implies(vy, depth + 1);
} }
} }
if (this.kind === "conditional") {
let [c, x, y] = this.args;
// (c ? x : y) => val if x is true and y is false and c = val
if (!x.mightNotBeTrue() && !y.mightNotBeFalse()) {
return c.equals(val);
}
// (c ? false : y) => y !== undefined && y !== null && y !== f // (c ? x : false) => c && x (if c or x were falsy, (c ? x : false) could not be true)
if (val.kind === "!==") { if (!y.mightNotBeFalse()) {
let [vx, vy] = val.args; if (c.implies(val, depth + 1)) return true;
if (!x.mightNotBeFalse()) { if (x.implies(val, depth + 1)) return true;
if (y.implies(vx)) return vy instanceof NullValue || vy instanceof UndefinedValue;
if (y.implies(vy)) return vx instanceof NullValue || vx instanceof UndefinedValue;
} else if (!y.mightNotBeFalse()) {
if (x.implies(vx)) return vy instanceof NullValue || vy instanceof UndefinedValue;
if (x.implies(vy)) return vx instanceof NullValue || vx instanceof UndefinedValue;
}
}
// (c ? x : false) => c && x (if c or x were falsy, (c ? x : false) could not be true)
if (!y.mightNotBeFalse()) {
if (c.implies(val)) return true;
if (x.implies(val)) return true;
}
} }
} else if (this.kind === "!==") {
// (0 !== x) => x since undefined, null, false, 0, NaN and "" are excluded by the !== and all other values are thruthy // (0 !== x) => x since undefined, null, false, 0, NaN and "" are excluded by the !== and all other values are thruthy
if (this.kind === "!==") { let [x, y] = this.args;
let [x, y] = this.args; if (x instanceof NumberValue && x.value === 0) return y.equals(val);
if (x instanceof NumberValue && x.value === 0) return y.equals(val); if (y instanceof NumberValue && y.value === 0) return x.equals(val);
if (y instanceof NumberValue && y.value === 0) return x.equals(val); } else if ((this.kind === "===" || this.kind === "==") && (val.kind === "===" || val.kind === "==")) {
} let [x, y] = this.args;
if (this.kind === "===" && val.kind === "==") { let [vx, vy] = val.args;
// x === undefined/null => y == undefined/null if (x instanceof NullValue || x instanceof UndefinedValue) {
let [x, y] = val.args; if (val.kind === "==") {
if ( // null/undefined === y && null/undefined === vy && y === vy => null/undefined == vy
x instanceof NullValue || if (vx instanceof NullValue || vx instanceof UndefinedValue) return y.equals(vy);
x instanceof UndefinedValue || // null/undefined === y && vx === null/undefined && y === vx => null/undefined == vx
y instanceof NullValue || if (vy instanceof NullValue || vy instanceof UndefinedValue) return y.equals(vx);
y instanceof UndefinedValue } else {
) { invariant(val.kind === "===");
let [vx, vy] = val.args; // null === y && null === vy && y === vy => null === vy
if ( // undefined === y && undefined === vy && y === vy => undefined === vy
vx instanceof NullValue || if (x.equals(vx)) return y.equals(vy);
vx instanceof UndefinedValue || // null === y && vx === null && y === vx => vx === null
vy instanceof NullValue || // undefined === y && vx === undefined && y === vx => vx === undefined
vy instanceof UndefinedValue if (x.equals(vy)) return y.equals(vx);
) {
return true;
}
} }
} }
if (this.kind === "||") { if (y instanceof NullValue || y instanceof UndefinedValue) {
let [x, y] = this.args; if (val.kind === "==") {
let xi = x.implies(val) || (x instanceof AbstractValue && this.$Realm.pathConditions.impliesNot(x)); // x === null/undefined && null/undefined === vy && x === vy => null/undefined == vy
if (!xi) return false; if (vx instanceof NullValue || vx instanceof UndefinedValue) return x.equals(vy);
let yi = y.implies(val) || (y instanceof AbstractValue && this.$Realm.pathConditions.impliesNot(y)); // x === null/undefined && vx === null/undefined && x === vx => null/undefined == vx
return yi; if (vy instanceof NullValue || vy instanceof UndefinedValue) return x.equals(vx);
} } else {
if (this.kind === "&&") { invariant(val.kind === "===");
let [x, y] = this.args; // x === null && null === vy && x === vy => null === vy
let xi = x.implies(val) || (x instanceof AbstractValue && this.$Realm.pathConditions.impliesNot(x)); // x == undefined && undefined === vy && x === vy => undefined === vy
if (xi) return true; if (y.equals(vx)) return x.equals(vy);
let yi = y.implies(val) || (y instanceof AbstractValue && this.$Realm.pathConditions.impliesNot(y)); // x === null && vx === null && x === vx => null == vy
return yi; // x === undefined && vx === undefined && x === vx => vx === undefined
if (y.equals(vy)) return x.equals(vx);
}
} }
} }
// x => !y if y => !x
if (val.kind === "!") {
let [y] = val.args;
invariant(y instanceof AbstractValue);
return y.impliesNot(this, depth + 1);
}
return false; return false;
} }
// this => !val. A false value does not imply that !(this => !val). // this => !val. A false value does not imply that !(this => !val).
impliesNot(val: Value): boolean { impliesNot(val: AbstractValue, depth: number = 0): boolean {
if (depth > 5) return false;
if (this.equals(val)) return false; // x => x regardless of its value, hence x => !val is false if (this.equals(val)) return false; // x => x regardless of its value, hence x => !val is false
if (!this.mightNotBeFalse()) return true; // false => !val if (this.kind === "||") {
if (!val.mightNotBeFalse()) return true; // x => !false regardless of the value of x let [x, y] = this.args;
if (val instanceof AbstractValue) { let xi = x.impliesNot(val, depth + 1);
// !x => !y if y => x if (!xi) return false;
if (this.kind === "!") { let yi = y.impliesNot(val, depth + 1);
let [x] = this.args; return yi;
} else if (this.kind === "&&") {
let [x, y] = this.args;
let xi = x.impliesNot(val, depth + 1);
if (xi) return true;
let yi = y.impliesNot(val, depth + 1);
return yi;
} else if (this.kind === "!") {
let [nx] = this.args;
invariant(nx instanceof AbstractValue);
if (nx.kind === "!") {
// !!x => !y if y => !x
let [x] = nx.args;
invariant(x instanceof AbstractValue); invariant(x instanceof AbstractValue);
if (x.kind === "!") { return x.impliesNot(val, depth + 1);
// !!x => !y if y => !x
invariant(x instanceof AbstractValue);
let [xx] = x.args;
invariant(xx instanceof AbstractValue);
return xx.impliesNot(val);
}
if (x.kind === "abstractConcreteUnion") return false; // can't use two valued logic for this.
return val.implies(x);
} }
if (this.kind === "conditional") { if (nx.kind === "abstractConcreteUnion") return false; // can't use two valued logic for this.
let [c, x, y] = this.args; // !x => !val if val => x since if val is false x can be any value and if val is true then x must be true
// (c ? x : y) => !val if x is false and y is true and c = val return val.implies(nx);
if (!x.mightNotBeFalse() && !y.mightNotBeTrue()) { } else if (this.kind === "conditional") {
return c.equals(val); let [c, x, y] = this.args;
// (c ? x : y) => !val if x is false and y is true and c = val
if (!x.mightNotBeFalse() && !y.mightNotBeTrue()) {
return c.equals(val);
}
if (val.kind === "===" || val.kind === "==") {
let [vx, vy] = val.args;
if (!x.mightNotBeFalse()) {
// (c ? false : y) => !(vx === undefined) && !(vx === null) if y => vx, since val is false unless y is true
if (vx instanceof AbstractValue && (vy instanceof NullValue || vy instanceof UndefinedValue))
return y.implies(vx, depth + 1);
// (c ? false : y) => !(undefined === vy) && !(null === vy) if y => vy, since val is false unless y is true
if ((vx instanceof NullValue || vx instanceof UndefinedValue) && vy instanceof AbstractValue)
return y.implies(vy, depth + 1);
} else if (!y.mightNotBeFalse()) {
// (c ? x : false) => !(vx === undefined) && !(vx === null) if x => vx, since val is false unless x is true
if (vx instanceof AbstractValue && (vy instanceof NullValue || vy instanceof UndefinedValue))
return x.implies(vx, depth + 1);
// (c ? x : false) => !(undefined === vy) && !(null !== vy) if x => vy, since val is false unless x is true
if ((vx instanceof NullValue || vx instanceof UndefinedValue) && vy instanceof AbstractValue)
return x.implies(vy, depth + 1);
} }
} }
if (this.kind === "===" && val.kind === "===") {
// x === y and y !== z => !(x === z) // (c ? x : false) => c && x (if c or x were falsy, (c ? x : false) could not be true)
let [x1, y1] = this.args; if (!y.mightNotBeFalse()) {
let [x2, y2] = val.args; if (c.impliesNot(val, depth + 1)) return true;
if (x1.equals(x2) && y1 instanceof ConcreteValue && y2 instanceof ConcreteValue && !y1.equals(y2)) return true; if (x.impliesNot(val, depth + 1)) return true;
// x === y and x !== z => !(z === y)
if (y1.equals(y2) && x1 instanceof ConcreteValue && x2 instanceof ConcreteValue && !x1.equals(x2)) {
return true;
}
} }
if (this.kind === "||") { } else if (this.kind === "===" && val.kind === "===") {
let [x, y] = this.args; // x === y and y !== z => !(x === z)
if (x.impliesNot(val) && y.impliesNot(val)) return true; let [x1, y1] = this.args;
} let [x2, y2] = val.args;
if (this.kind === "&&") { if (x1.equals(x2) && y1 instanceof ConcreteValue && y2 instanceof ConcreteValue && !y1.equals(y2)) return true;
let [x, y] = this.args; // x === y and x !== z => !(z === y)
if (x.impliesNot(val) || y.impliesNot(val)) return true; if (y1.equals(y2) && x1 instanceof ConcreteValue && x2 instanceof ConcreteValue && !x1.equals(x2)) {
return true;
} }
} }
return false; return false;

View File

@ -13,6 +13,7 @@ import type { BabelNodeSourceLocation } from "@babel/types";
import type { Realm } from "../realm.js"; import type { Realm } from "../realm.js";
import { import {
AbstractObjectValue, AbstractObjectValue,
AbstractValue,
BooleanValue, BooleanValue,
ConcreteValue, ConcreteValue,
NumberValue, NumberValue,
@ -62,17 +63,15 @@ export default class Value {
expressionLocation: ?BabelNodeSourceLocation; expressionLocation: ?BabelNodeSourceLocation;
$Realm: Realm; $Realm: Realm;
implies(val: Value): boolean { implies(val: AbstractValue, depth: number = 0): boolean {
if (this.equals(val)) return true;
if (!this.mightNotBeFalse()) return true; if (!this.mightNotBeFalse()) return true;
if (!val.mightNotBeTrue()) return true; if (this.equals(val)) return true;
return false; return false;
} }
impliesNot(val: Value): boolean { impliesNot(val: AbstractValue, depth: number = 0): boolean {
if (this.equals(val)) return false;
if (!this.mightNotBeFalse()) return true; if (!this.mightNotBeFalse()) return true;
if (!val.mightNotBeTrue()) return false; if (this.equals(val)) return false;
return false; return false;
} }

View File

@ -1,6 +1,6 @@
function fn(x) { function fn(x) {
for ( for (
var _iterator = x.items, var _iterator = x.entries(),
_isArray = Array.isArray(_iterator), _isArray = Array.isArray(_iterator),
_i = 0, _i = 0,
_iterator = _isArray ? _iterator : _iterator[Symbol.iterator](); _iterator = _isArray ? _iterator : _iterator[Symbol.iterator]();