Simplify path conditions

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 https://github.com/facebook/prepack/pull/970

Differential Revision: D5857033

Pulled By: hermanventer

fbshipit-source-id: 5436d251378decf6de549a3d70e9605664d569e5

.gitignore

@@ -8,4 +8,5 @@ build/
 coverage*/
 .vscode
 facebook/test
+facebook/tutorial
 prepack.min.js

src/environment.js

@@ -108,7 +108,7 @@ export type Binding = {
 export class DeclarativeEnvironmentRecord extends EnvironmentRecord {
   constructor(realm: Realm) {
     super(realm);
-    this.bindings = Object.create(null);
+    this.bindings = (Object.create(null): any);
   }
 
   bindings: { [name: string]: Binding };

src/evaluators/CallExpression.js

@@ -31,7 +31,7 @@ import {
   SameValue,
   TestIntegrityLevel,
 } from "../methods/index.js";
-import type { BabelNode, BabelNodeCallExpression, BabelNodeExpression, BabelNodeSpreadElement } from "babel-types";
+import type { BabelNodeCallExpression, BabelNodeExpression, BabelNodeSpreadElement } from "babel-types";
 import invariant from "../invariant.js";
 import * as t from "babel-types";
 import SuperCall from "./SuperCall";
@@ -116,7 +116,7 @@ function EvaluateCall(
     let [thisArg, propName] = ref instanceof Reference ? [ref.base, ref.referencedName] : [];
     if (thisArg instanceof Value) args = [thisArg];
     if (propName !== undefined && typeof propName !== "string") args.push(propName);
-    args = args.concat(ArgumentListEvaluation(realm, strictCode, env, ((ast.arguments: any): Array<BabelNode>)));
+    args = args.concat(ArgumentListEvaluation(realm, strictCode, env, ast.arguments));
     for (let arg of args) {
       if (arg !== func && arg instanceof ObjectValue && !TestIntegrityLevel(realm, arg, "frozen")) {
         let diag = new CompilerDiagnostic(
@@ -165,7 +165,7 @@ function EvaluateCall(
     // a. If SameValue(func, %eval%) is true, then
     if (SameValue(realm, func, realm.intrinsics.eval)) {
       // i. Let argList be ? ArgumentListEvaluation(Arguments).
-      let argList = ArgumentListEvaluation(realm, strictCode, env, ((ast.arguments: any): Array<BabelNode>));
+      let argList = ArgumentListEvaluation(realm, strictCode, env, ast.arguments);
       // ii. If argList has no elements, return undefined.
       if (argList.length === 0) return realm.intrinsics.undefined;
       // iii. Let evalText be the first element of argList.
@@ -216,14 +216,5 @@ function EvaluateCall(
   let tailCall = IsInTailPosition(realm, thisCall);
 
   // 8. Return ? EvaluateDirectCall(func, thisValue, Arguments, tailCall).
-  return EvaluateDirectCall(
-    realm,
-    strictCode,
-    env,
-    ref,
-    func,
-    thisValue,
-    ((ast.arguments: any): Array<BabelNode>),
-    tailCall
-  );
+  return EvaluateDirectCall(realm, strictCode, env, ref, func, thisValue, ast.arguments, tailCall);
 }

src/evaluators/IfStatement.js

@@ -18,6 +18,7 @@ import { Reference } from "../environment.js";
 import { GetValue, joinEffects, ToBoolean, UpdateEmpty } from "../methods/index.js";
 import type { BabelNode, BabelNodeIfStatement } from "babel-types";
 import invariant from "../invariant.js";
+import { withPathCondition, withInversePathCondition } from "../utils/paths.js";
 
 export function evaluate(
   ast: BabelNodeIfStatement,
@@ -86,23 +87,13 @@ export function evaluateWithAbstractConditional(
   realm: Realm
 ): NormalCompletion | Value {
   // Evaluate consequent and alternate in sandboxes and get their effects.
-  let compl1, gen1, bindings1, properties1, createdObj1;
-  realm.pathConditions.push(condValue);
-  try {
-    [compl1, gen1, bindings1, properties1, createdObj1] = realm.evaluateNodeForEffects(consequent, strictCode, env);
-  } finally {
-    realm.pathConditions.pop();
-  }
+  let [compl1, gen1, bindings1, properties1, createdObj1] = withPathCondition(condValue, () => {
+    return realm.evaluateNodeForEffects(consequent, strictCode, env);
+  });
 
-  let compl2, gen2, bindings2, properties2, createdObj2;
-  realm.pathConditions.push(AbstractValue.createFromUnaryOp(realm, "!", condValue));
-  try {
-    [compl2, gen2, bindings2, properties2, createdObj2] = alternate
-      ? realm.evaluateNodeForEffects(alternate, strictCode, env)
-      : construct_empty_effects(realm);
-  } finally {
-    realm.pathConditions.pop();
-  }
+  let [compl2, gen2, bindings2, properties2, createdObj2] = withInversePathCondition(condValue, () => {
+    return alternate ? realm.evaluateNodeForEffects(alternate, strictCode, env) : construct_empty_effects(realm);
+  });
 
   // Join the effects, creating an abstract view of what happened, regardless
   // of the actual value of condValue.

src/evaluators/LogicalExpression.js

@@ -44,11 +44,9 @@ export default function(
   }
   invariant(lval instanceof AbstractValue);
 
-  if (!lval.mightNotBeFalse()) {
-    if (ast.operator === "&&") return env.evaluate(ast.right, strictCode);
-    else {
-      return lval;
-    }
+  if (!lval.isIntrinsic()) {
+    if (!lval.mightNotBeFalse()) return ast.operator === "||" ? env.evaluate(ast.right, strictCode) : lval;
+    if (!lval.mightNotBeTrue()) return ast.operator === "&&" ? env.evaluate(ast.right, strictCode) : lval;
   }
 
   // Create empty effects for the case where ast.right is not evaluated

src/evaluators/NewExpression.js

@@ -53,7 +53,7 @@ export default function(
   } else {
     // 6. Else,
     // a. Let argList be ArgumentListEvaluation of arguments.
-    argsList = ArgumentListEvaluation(realm, strictCode, env, args);
+    argsList = ArgumentListEvaluation(realm, strictCode, env, (args: any)); // BabelNodeNewExpression needs updating
 
     // This step not necessary since we propagate completions with exceptions.
     // b. ReturnIfAbrupt(argList).

src/evaluators/SuperCall.js

@@ -9,6 +9,7 @@
 
 /* @flow */
 
+import type { BabelNodeExpression, BabelNodeSpreadElement } from "babel-types";
 import type { Realm } from "../realm.js";
 import type { LexicalEnvironment } from "../environment.js";
 import { FunctionEnvironmentRecord } from "../environment.js";
@@ -50,7 +51,7 @@ function GetSuperConstructor(realm: Realm) {
 
 // ECMA262 12.3.5.1
 export default function SuperCall(
-  Arguments: Array<BabelNode>,
+  Arguments: Array<BabelNodeExpression | BabelNodeSpreadElement>,
   strictCode: boolean,
   env: LexicalEnvironment,
   realm: Realm

src/methods/call.js

@@ -52,7 +52,7 @@ import {
 } from "../completions.js";
 import { GetTemplateObject, GetV, GetThisValue } from "../methods/get.js";
 import invariant from "../invariant.js";
-import type { BabelNode, BabelNodeExpression, BabelNodeSpreadElement, BabelNodeTemplateLiteral } from "babel-types";
+import type { BabelNodeExpression, BabelNodeSpreadElement, BabelNodeTemplateLiteral } from "babel-types";
 import * as t from "babel-types";
 
 // ECMA262 12.3.6.1
@@ -60,13 +60,13 @@ export function ArgumentListEvaluation(
   realm: Realm,
   strictCode: boolean,
   env: LexicalEnvironment,
-  argNodes: Array<BabelNode> | BabelNodeTemplateLiteral
+  argNodes: Array<BabelNodeExpression | BabelNodeSpreadElement> | BabelNodeTemplateLiteral
 ): Array<Value> {
   if (Array.isArray(argNodes)) {
     let args = [];
-    for (let node_ of ((argNodes: any): Array<BabelNode>)) {
+    for (let node_ of argNodes) {
       if (node_.type === "SpreadElement") {
-        let node = ((node_: any): BabelNodeSpreadElement);
+        let node = (node_: BabelNodeSpreadElement);
         // 1. Let list be a new empty List.
         let list = args;
 
@@ -103,7 +103,7 @@ export function ArgumentListEvaluation(
     }
     return args;
   } else {
-    let node = ((argNodes: any): BabelNodeTemplateLiteral);
+    let node = (argNodes: BabelNodeTemplateLiteral);
     if (node.expressions.length === 0) {
       // 1. Let templateLiteral be this TemplateLiteral.
       let templateLiteral = node;
@@ -402,7 +402,7 @@ export function EvaluateDirectCall(
   ref: Value | Reference,
   func: Value,
   thisValue: Value,
-  args: Array<BabelNode> | BabelNodeTemplateLiteral,
+  args: Array<BabelNodeExpression | BabelNodeSpreadElement> | BabelNodeTemplateLiteral,
   tailPosition?: boolean
 ): Value {
   // 1. Let argList be ? ArgumentListEvaluation(arguments).
@@ -422,11 +422,15 @@ export function EvaluateDirectCallWithArgList(
   tailPosition?: boolean
 ): Value {
   if (func instanceof AbstractValue && Value.isTypeCompatibleWith(func.getType(), FunctionValue)) {
-    let fullArgs = [func].concat(argList);
-    return AbstractValue.createTemporalFromBuildFunction(realm, Value, fullArgs, nodes => {
-      let fun_args = ((nodes.slice(1): any): Array<BabelNodeExpression | BabelNodeSpreadElement>);
-      return t.callExpression(nodes[0], fun_args);
-    });
+    return AbstractValue.createTemporalFromBuildFunction(
+      realm,
+      Value,
+      [func].concat(argList),
+      (nodes: Array<BabelNodeExpression>) => {
+        let fun_args = nodes.slice(1);
+        return t.callExpression(nodes[0], ((fun_args: any): Array<BabelNodeExpression | BabelNodeSpreadElement>));
+      }
+    );
   }
   func = func.throwIfNotConcrete();
 

src/serializer/ResidualHeapSerializer.js

@@ -825,7 +825,7 @@ export class ResidualHeapSerializer {
     invariant(residualBindings);
 
     invariant(val instanceof ECMAScriptSourceFunctionValue);
-    let serializedBindings = Object.create(null);
+    let serializedBindings = {};
     let instance: FunctionInstance = {
       serializedBindings,
       functionValue: val,

src/serializer/ResidualHeapVisitor.js

@@ -183,7 +183,7 @@ export class ResidualHeapVisitor {
   visitDeclarativeEnvironmentRecordBinding(r: DeclarativeEnvironmentRecord, n: string): VisitedBinding {
     let visitedBindings = this.declarativeEnvironmentRecordsBindings.get(r);
     if (!visitedBindings) {
-      visitedBindings = Object.create(null);
+      visitedBindings = (Object.create(null): any);
       this.declarativeEnvironmentRecordsBindings.set(r, visitedBindings);
     }
     let visitedBinding: ?VisitedBinding = visitedBindings[n];
@@ -278,8 +278,8 @@ export class ResidualHeapVisitor {
 
     if (!functionInfo) {
       functionInfo = {
-        unbound: Object.create(null),
-        modified: Object.create(null),
+        unbound: (Object.create(null): any),
+        modified: (Object.create(null): any),
         usesArguments: false,
         usesThis: false,
       };
@@ -312,7 +312,7 @@ export class ResidualHeapVisitor {
       }
     }
 
-    let visitedBindings = Object.create(null);
+    let visitedBindings = (Object.create(null): any);
     this._withScope(val, () => {
       invariant(functionInfo);
       for (let innerName in functionInfo.unbound) {

src/serializer/types.js

@@ -45,7 +45,7 @@ export type SerializedBinding = {
   scope?: ScopeBinding,
 };
 
-export type VisitedBindings = { [key: string]: VisitedBinding };
+export type VisitedBindings = { [key: string]: VisitedBinding }; //todo: use a map
 export type VisitedBinding = {
   value: void | Value,
   modified: boolean,

src/utils/paths.js

@@ -0,0 +1,84 @@
+/**
+ * Copyright (c) 2017-present, Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD-style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+/* @flow */
+
+import { AbstractValue, ConcreteValue, Value } from "../values/index.js";
+import invariant from "../invariant.js";
+import simplifyAbstractValue from "../utils/simplifier.js";
+
+export function withPathCondition<T>(condition: AbstractValue, evaluate: () => T): T {
+  let realm = condition.$Realm;
+  let savedPath = realm.pathConditions;
+  realm.pathConditions = [];
+  try {
+    pushPathCondition(condition);
+    pushRefinedConditions(savedPath);
+    return evaluate();
+  } finally {
+    realm.pathConditions = savedPath;
+  }
+}
+
+export function withInversePathCondition<T>(condition: AbstractValue, evaluate: () => T): T {
+  let realm = condition.$Realm;
+  let savedPath = realm.pathConditions;
+  realm.pathConditions = [];
+  try {
+    pushInversePathCondition(condition);
+    pushRefinedConditions(savedPath);
+    return evaluate();
+  } finally {
+    realm.pathConditions = savedPath;
+  }
+}
+
+// A path condition is an abstract value that is known to be true in a particular code path
+function pushPathCondition(condition: Value) {
+  invariant(condition.mightNotBeFalse()); // it is mistake to assert that false is true
+  if (condition instanceof ConcreteValue) return;
+  if (!condition.mightNotBeTrue()) return;
+  invariant(condition instanceof AbstractValue);
+  let realm = condition.$Realm;
+  if (condition.kind === "&&") {
+    let left = condition.args[0];
+    let right = condition.args[1];
+    invariant(left instanceof AbstractValue); // it is a mistake to create an abstract value when concrete value will do
+    pushPathCondition(left);
+    pushPathCondition(right);
+  } else {
+    realm.pathConditions.push(condition);
+  }
+}
+
+// An inverse path condition is an abstract value that is known to be false in a particular code path
+function pushInversePathCondition(condition: Value) {
+  invariant(condition.mightNotBeTrue()); // it is mistake to assert that true is false
+  if (condition instanceof ConcreteValue) return;
+  invariant(condition instanceof AbstractValue);
+  if (condition.kind === "||") {
+    let left = condition.args[0];
+    let right = condition.args[1];
+    invariant(left instanceof AbstractValue); // it is a mistake to create an abstract value when concrete value will do
+    pushInversePathCondition(left);
+    pushInversePathCondition(right);
+  } else {
+    let realm = condition.$Realm;
+    let inverseCondition = AbstractValue.createFromUnaryOp(realm, "!", condition);
+    pushPathCondition(inverseCondition);
+    let simplifiedInverseCondition = simplifyAbstractValue(realm, inverseCondition);
+    if (simplifiedInverseCondition !== inverseCondition) pushPathCondition(simplifiedInverseCondition);
+  }
+}
+
+function pushRefinedConditions(unrefinedConditions: Array<AbstractValue>) {
+  for (let unrefinedCond of unrefinedConditions) {
+    pushPathCondition(unrefinedCond.refineWithPathCondition());
+  }
+}

src/values/AbstractObjectValue.js

@@ -30,6 +30,9 @@ export default class AbstractObjectValue extends AbstractValue {
     optionalArgs?: {| kind?: string, intrinsicName?: string |}
   ) {
     super(realm, types, values, hashValue, args, buildNode, optionalArgs);
+    if (!values.isTop()) {
+      for (let element of this.values.getElements()) invariant(element instanceof ObjectValue);
+    }
   }
 
   getTemplate(): ObjectValue {
@@ -130,6 +133,24 @@ export default class AbstractObjectValue extends AbstractValue {
         return cv.$GetOwnProperty(P, cv);
       }
       invariant(false);
+    } else if (this.kind === "conditional") {
+      // this is the join of two concrete objects
+      // 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);
+      invariant(ob2 instanceof ObjectValue);
+      let d1 = ob1.$GetOwnProperty(P);
+      let d2 = ob2.$GetOwnProperty(P);
+      if (d1 === undefined || d2 === undefined || !equalDescriptors(d1, d2)) {
+        AbstractValue.reportIntrospectionError(this, P);
+        throw new FatalError();
+      }
+      let desc = cloneDescriptor(d1);
+      invariant(desc !== undefined);
+      if (IsDataDescriptor(this.$Realm, desc))
+        desc.value = joinValuesAsConditional(this.$Realm, cond, d1.value, d2.value);
+      return desc;
     } else {
       let hasProp = false;
       let doesNotHaveProp = false;
@@ -261,6 +282,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
+      // 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);
+      invariant(ob2 instanceof ObjectValue);
+      let d1 = ob1.$GetOwnProperty(P);
+      let d1val =
+        d1 === undefined ? this.$Realm.intrinsics.undefined : IsDataDescriptor(this.$Realm, d1) ? d1.value : undefined;
+      let d2 = ob2.$GetOwnProperty(P);
+      let d2val =
+        d2 === undefined ? this.$Realm.intrinsics.undefined : IsDataDescriptor(this.$Realm, d2) ? d2.value : undefined;
+      if (d1val === undefined || d2val === undefined) {
+        AbstractValue.reportIntrospectionError(this, P);
+        throw new FatalError();
+      }
+      return joinValuesAsConditional(this.$Realm, cond, d1val, d2val);
     } else {
       let result;
       for (let cv of elements) {

src/values/AbstractValue.js

@@ -42,6 +42,7 @@ import {
   hashTernary,
   hashUnary,
   StrictEqualityComparison,
+  ToBoolean,
 } from "../methods/index.js";
 import { TypesDomain, ValuesDomain } from "../domains/index.js";
 import invariant from "../invariant.js";
@@ -191,8 +192,34 @@ export default class AbstractValue extends Value {
   implies(val: AbstractValue): boolean {
     // Neither this nor val is a known value, so we need to some reasoning based on the structure
     if (this.equals(val)) return true; // x => x regardless of its value
-    // todo: (x & y) => z if (x => z) || (y => z)
-    // todo: x => (y | z) if (x => y) || (x = z)
+    // (x && y) => z if (x => z) || (y => z)
+    if (this.kind === "&&") {
+      let [x, y] = this.args;
+      invariant(x instanceof AbstractValue);
+      invariant(y instanceof AbstractValue);
+      return x.implies(val) || y.implies(val);
+    }
+    // (x || y) => z if (x => z) && (y => z)
+    if (this.kind === "||") {
+      let [x, y] = this.args;
+      invariant(x instanceof AbstractValue);
+      invariant(y instanceof AbstractValue);
+      return x.implies(val) && y.implies(val);
+    }
+    // x => (y && z) if (x => y) && (x = z)
+    if (val.kind === "&&") {
+      let [y, z] = this.args;
+      invariant(y instanceof AbstractValue);
+      invariant(z instanceof AbstractValue);
+      return this.implies(y) && this.implies(z);
+    }
+    // x => (y || z) if (x => y) || (x = z)
+    if (val.kind === "||") {
+      let [y, z] = this.args;
+      invariant(y instanceof AbstractValue);
+      invariant(z instanceof AbstractValue);
+      return this.implies(y) || this.implies(z);
+    }
     return false;
   }
 
@@ -294,7 +321,15 @@ export default class AbstractValue extends Value {
   }
 
   refineWithPathCondition(): Value {
-    if (this.kind !== "conditional") return this;
+    let op = this.kind;
+    if (op === "&&" || op === "||") {
+      let [left, right] = this.args;
+      let refinedLeft = left instanceof AbstractValue ? left.refineWithPathCondition() : left;
+      let refinedRight = right instanceof AbstractValue ? right.refineWithPathCondition() : right;
+      if (left === refinedLeft && right === refinedRight) return this;
+      return AbstractValue.createFromLogicalOp(this.$Realm, op, refinedLeft, refinedRight, this.expressionLocation);
+    }
+    if (op !== "conditional") return this;
     let [condition, trueVal, falseVal] = this.args;
     invariant(condition instanceof AbstractValue);
     invariant(trueVal !== undefined);
@@ -396,15 +431,19 @@ export default class AbstractValue extends Value {
     left: Value,
     right: Value,
     loc?: ?BabelNodeSourceLocation
-  ): AbstractValue {
+  ): Value {
     let leftTypes, leftValues;
     if (left instanceof AbstractValue) {
+      if (!left.isIntrinsic()) {
+        if (!left.mightNotBeTrue()) return op === "&&" ? right : left;
+        if (!left.mightNotBeFalse()) return op === "&&" ? left : right;
+      }
       leftTypes = left.types;
       leftValues = left.values;
     } else {
-      leftTypes = new TypesDomain(left.getType());
       invariant(left instanceof ConcreteValue);
-      leftValues = new ValuesDomain(left);
+      if (ToBoolean(realm, left)) return op === "&&" ? right : left;
+      else return this.kind === "&&" ? left : right;
     }
 
     let rightTypes, rightValues;
@@ -438,9 +477,15 @@ export default class AbstractValue extends Value {
     right: void | Value,
     loc?: ?BabelNodeSourceLocation
   ): AbstractValue {
-    if (left instanceof BooleanValue && right instanceof BooleanValue) {
-      if (left.value && !right.value) return condition;
-      if (!left.value && right.value) return AbstractValue.createFromUnaryOp(realm, "!", condition, true, loc);
+    if (
+      left !== undefined &&
+      left.getType() === BooleanValue &&
+      right !== undefined &&
+      right.getType() === BooleanValue
+    ) {
+      if (!left.mightNotBeTrue() && !right.mightNotBeFalse()) return condition;
+      if (!left.mightNotBeFalse() && !right.mightNotBeTrue())
+        return AbstractValue.createFromUnaryOp(realm, "!", condition, true, loc);
     }
     let types = TypesDomain.joinValues(left, right);
     let values = ValuesDomain.joinValues(realm, left, right);

test/serializer/abstract/Refine3.js

@@ -0,0 +1,16 @@
+let x = global.__abstract ? __abstract("boolean", "false") : false;
+let f = function() { return 42; }
+let modules = [];
+if (x) {
+  modules[0] = { initialized: true, f: undefined, result: f() };
+} else {
+  modules[0] = { initialized: false, f, result: undefined};
+}
+let module = modules[0];
+if (module && module.initialized) {
+} else if (module) {
+  // (!module || !x)
+  modules[0] = { initialized: true, f: undefined, result: module.f() };
+}
+
+inspect = function() { return modules[0].result; }