Make sure that adding a path condition clears negative caches. (#2549)

Summary:
Release note: none

When a new path condition is added to an existing path conditions object, the negative caches must be cleared since the new condition might allow previously failed implications to now succeed. This was already done in one case, but a few others were missed. The clearing code is now centralized and all cases go through it.

While debugging the internal test case that failed because of the caching mistake, I also realized that PathConditions.implies and PathConditions.impliesNot can profitably deconstruct expressions of the form !x before doing the implication check. This also has the advantage that it eliminates a subtle endless recursion situation in a nicer way than the current code.

I've also added some comments in places that caught my eye during debugging.
Pull Request resolved: https://github.com/facebook/prepack/pull/2549

Differential Revision: D9883127

Pulled By: hermanventer

fbshipit-source-id: 06faa709dfecaa4f98b7d0ce5e1c7a9efb6b805f
This commit is contained in:
Herman Venter 2018-09-17 14:05:33 -07:00 committed by Facebook Github Bot
parent ee291d19dc
commit 8ba4fbc916
4 changed files with 26 additions and 24 deletions

View File

@ -129,18 +129,7 @@ export class JoinImplementation {
return rightCompletion;
}
composeWithEffectsWithTailDuplicaton(completion: Completion, effects: Effects): Effects {
if (completion instanceof AbruptCompletion) return construct_empty_effects(completion.value.$Realm, completion);
if (completion instanceof SimpleNormalCompletion) return effects.shallowCloneWithResult(effects.result);
invariant(completion instanceof JoinedNormalAndAbruptCompletions);
let e1 = this.composeWithEffects(completion.consequent, effects);
let e2 = this.composeWithEffects(completion.alternate, effects);
return this.joinEffects(completion.joinCondition, e1, e2);
}
composeWithEffects(completion: Completion, normalEffects: Effects): Effects {
if (completion.value.$Realm.abstractValueImpliesMax > 0)
return this.composeWithEffectsWithTailDuplicaton(completion, normalEffects);
if (completion instanceof JoinedNormalAndAbruptCompletions) {
let selectAbrupt = c => c instanceof AbruptCompletion && c.value !== c.value.$Realm.intrinsics.__bottomValue;
let composableCompletions = Completion.makeSelectedCompletionsInfeasibleInCopy(selectAbrupt, completion);

View File

@ -354,7 +354,9 @@ export type DebugServerType = {
};
export type PathType = {
// this => val. A false value does not imply that !(this => val).
implies(condition: Value, depth?: number): boolean,
// this => !val. A false value does not imply that !(this => !val).
impliesNot(condition: Value, depth?: number): boolean,
withCondition<T>(condition: Value, evaluate: () => T): T,
withInverseCondition<T>(condition: Value, evaluate: () => T): T,
@ -365,10 +367,12 @@ export type PathType = {
export class PathConditions {
add(c: AbstractValue): void {}
// this => val. A false value does not imply that !(this => val).
implies(e: Value, depth: number = 0): boolean {
return false;
}
// this => !val. A false value does not imply that !(this => !val).
impliesNot(e: Value, depth: number = 0): boolean {
return false;
}

View File

@ -38,12 +38,15 @@ export class PathConditionsImplementation extends PathConditions {
add(c: AbstractValue): void {
invariant(!this._readonly);
this._assumedConditions.add(c);
this._failedImplications = undefined;
this._failedNegativeImplications = undefined;
}
isReadOnly(): boolean {
return this._readonly;
}
// this => val. A false value does not imply that !(this => val).
implies(e: Value, depth: number = 0): boolean {
if (!e.mightNotBeTrue()) return true;
if (!e.mightNotBeFalse()) return false;
@ -57,10 +60,6 @@ export class PathConditionsImplementation extends PathConditions {
for (let assumedCondition of this._assumedConditions) {
if (assumedCondition.implies(e, depth + 1)) return this.cacheImplicationSuccess(e);
}
// Do this here to prevent infinite recursion
if (this._failedImplications === undefined) this._failedImplications = new Set();
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
@ -90,6 +89,12 @@ export class PathConditionsImplementation extends PathConditions {
return this.cacheImplicationSuccess(e);
}
}
if (e.kind === "!") {
let [x] = e.args;
if (this.impliesNot(x, depth + 1)) return this.cacheImplicationSuccess(e);
}
if (this._failedImplications === undefined) this._failedImplications = new Set();
this._failedImplications.add(e);
return false;
}
@ -99,6 +104,7 @@ export class PathConditionsImplementation extends PathConditions {
return true;
}
// this => !val. A false value does not imply that !(this => !val).
impliesNot(e: Value, depth: number = 0): boolean {
if (!e.mightNotBeTrue()) return false;
if (!e.mightNotBeFalse()) return true;
@ -112,10 +118,6 @@ export class PathConditionsImplementation extends PathConditions {
for (let assumedCondition of this._assumedConditions) {
if (assumedCondition.impliesNot(e, depth + 1)) return this.cacheNegativeImplicationSuccess(e);
}
// Do this here to prevent infinite recursion
if (this._failedNegativeImplications === undefined) this._failedNegativeImplications = new Set();
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
@ -135,16 +137,22 @@ export class PathConditionsImplementation extends PathConditions {
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))
if ((y instanceof NullValue || y instanceof UndefinedValue) && this.implies(x, depth + 1))
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))
if ((x instanceof NullValue || x instanceof UndefinedValue) && this.implies(y, depth + 1))
return this.cacheNegativeImplicationSuccess(e);
}
}
if (e.kind === "!") {
let [x] = e.args;
if (this.implies(x, depth + 1)) return this.cacheNegativeImplicationSuccess(e);
}
if (this._failedNegativeImplications === undefined) this._failedNegativeImplications = new Set();
this._failedNegativeImplications.add(e);
return false;
}
@ -178,9 +186,6 @@ export class PathConditionsImplementation extends PathConditions {
if (refinedCondition !== condition) {
if (!refinedCondition.mightNotBeFalse()) throw new InfeasiblePathError();
if (refinedCondition instanceof AbstractValue) {
// These might have different answers now that we're adding another path condition
refinementTarget._failedImplications = undefined;
refinementTarget._failedNegativeImplications = undefined;
refinementTarget._readonly = false;
refinementTarget.add(refinedCondition);
}
@ -205,6 +210,7 @@ export class PathConditionsImplementation extends PathConditions {
}
export class PathImplementation {
// this => val. A false value does not imply that !(this => val).
implies(condition: Value, depth: number = 0): boolean {
if (!condition.mightNotBeTrue()) return true; // any path implies true
if (!condition.mightNotBeFalse()) return false; // no path condition is false
@ -212,6 +218,7 @@ export class PathImplementation {
return condition.$Realm.pathConditions.implies(condition, depth);
}
// this => !val. A false value does not imply that !(this => !val).
impliesNot(condition: Value, depth: number = 0): boolean {
if (!condition.mightNotBeFalse()) return true; // any path implies !false
if (!condition.mightNotBeTrue()) return false; // no path condition is false, so none can imply !true

View File

@ -63,12 +63,14 @@ export default class Value {
expressionLocation: ?BabelNodeSourceLocation;
$Realm: Realm;
// this => val. A false value does not imply that !(this => val).
implies(val: AbstractValue, depth: number = 0): boolean {
if (!this.mightNotBeFalse()) return true;
if (this.equals(val)) return true;
return false;
}
// this => !val. A false value does not imply that !(this => !val).
impliesNot(val: AbstractValue, depth: number = 0): boolean {
if (!this.mightNotBeFalse()) return true;
if (this.equals(val)) return false;