[hack][models] first model for hhbc_cmp_same

Summary:
The Hack equality test === compare objects by reference. We propose a first model
for the underlying hhbc_cmp_same builtin. We will need to refine this model later to take into
account primitive types that are boxed in InferHack.

Reviewed By: vsiles

Differential Revision: D46061589

fbshipit-source-id: 161d67811c9ea45cb96a714d97751ff0060d65fb

infer/lib/hack/models.sil

@@ -59,6 +59,20 @@ define $builtins.hack_is_true(b: *HackMixed) : int {
     ret n1
 }
 
+define $builtins.hack_neg(b: *HackBool) : *HackBool {
+  #entry:
+    n0: *HackBool = load &b
+    n1: int = load n0.HackBool.val
+    jmp is_true, is_false
+  #is_true:
+    prune n1
+    ret $builtins.hack_make_false()
+  #is_false:
+    prune !n1
+    ret $builtins.hack_make_true()
+
+}
+
 define $builtins.hhbc_cmp_eq(x: *HackMixed, y: *HackMixed) : *HackBool {
   //TODO: provide something more generic (right now, it works for int only)
   #entry:
@@ -85,6 +99,37 @@ define $builtins.hhbc_cmp_neq(x: *HackMixed, y: *HackMixed) : *HackBool {
     ret n5
 }
 
+define $builtins.hhbc_cmp_same(x: *HackMixed, y: *HackMixed) : *HackBool {
+  #entry:
+    n0: *HackMixed = load &x
+    n1: *HackMixed = load &y
+    jmp eq, x_eq_null, x_ne_null, ne
+  #eq:
+    prune __sil_eq(n0, n1)
+    ret $builtins.hack_make_true()
+  #x_eq_null:
+    prune __sil_eq(n0, 0)
+    prune __sil_ne(n1, 0)
+    ret $builtins.hack_make_false()
+  #x_ne_null:
+    prune __sil_ne(n0, 0)
+    prune __sil_eq(n1, 0)
+    ret $builtins.hack_make_false()
+  #ne:
+    prune __sil_ne(n0, n1)
+    prune __sil_ne(n0, 0)
+    prune __sil_ne(n1, 0)
+    ret $builtins.hack_make_random_bool()
+    // TODO: refine for primitives value (because they are boxed)
+}
+
+define $builtins.hhbc_cmp_nsame(x: *HackMixed, y: *HackMixed) : *HackBool {
+  #entry:
+    n0: *HackMixed = load &x
+    n1: *HackMixed = load &y
+    ret $builtins.hack_neg($builtins.hhbc_cmp_same(n0, n1))
+}
+
 define $builtins.hhbc_class_has_reified_generics(class: *HackMixed): *HackMixed {
   #entry:
     ret $builtins.hack_make_false()

infer/tests/codetoanalyze/hack/pulse/equality.hack

@@ -0,0 +1,62 @@
+// Copyright (c) Facebook, Inc. and its affiliates.
+//
+// This source code is licensed under the MIT license found in the
+// LICENSE file in the root directory of this source tree.
+
+namespace Equality;
+
+class A {
+
+  public function eqNullSimpleBad() {
+    $a = null;
+    $taint = \Level1\taintSource();
+    if ($a === null) {
+      \Level1\taintSink($taint);
+    }
+  }
+
+  public function eqNullSimpleGood() {
+    $a = new A();
+    $taint = \Level1\taintSource();
+    if ($a === null) {
+      \Level1\taintSink($taint);
+    }
+  }
+
+  public function neNullSimpleBad() {
+    $a = new A();
+    $taint = \Level1\taintSource();
+    if ($a !== null) {
+      \Level1\taintSink($taint);
+    }
+  }
+
+  public function doubleEqNullBad(A $a) {
+    $taint = \Level1\taintSource();
+    if ($a === null) {
+      if (null === $a) {
+        \Level1\taintSink($taint);
+      }
+    }
+  }
+
+  public function doubleEqNullGood(A $a1) {
+    $taint = \Level1\taintSource();
+    $a = new A();
+    if ($a1 === null) {
+      if ($a1 === $a) {
+        \Level1\taintSink($taint);
+      }
+    }
+  }
+
+  public function doubleEqNeNullGood(A $a) {
+    $taint = \Level1\taintSource();
+    if ($a === null) {
+      if ($a !== null) {
+        \Level1\taintSink($taint);
+      }
+    }
+  }
+
+}

infer/tests/codetoanalyze/hack/pulse/issues.exp

@@ -10,6 +10,9 @@ cross_file_taint_flow.hack, $root.inheritanceCrossFileFlowBad, 4, TAINT_ERROR, n
 dict.hack, DictTests::Main.init_and_load_bad, 6, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
 dict.hack, DictTests::Main.copy_on_write_bad, 10, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
 dict.hack, DictTests::Main.FP_copy_on_write_good, 10, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
+equality.hack, Equality::A.eqNullSimpleBad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $taint
+equality.hack, Equality::A.neNullSimpleBad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $taint
+equality.hack, Equality::A.doubleEqNullBad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $taint
 function_reference.hack, FunctionReference::Main.id_fst_bad, 7, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
 intra_file_flow.hack, IntraFileFlow.explicitSinkMethodDirectOnHackMixedSinkBad, 0, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value passed as argument `#1` to `IntraFileFlow.explicitSinkMethodDirectOnHackMixedSinkBad` with kind `Simple`,when calling `IntraFileFlow$static.explicitSinkMethodDirectOnHackMixedSinkBad` here,value passed as argument `#1` to `HackMixed$static.explicitSinkAllArgs` with kind `Simple`], source: IntraFileFlow.explicitSinkMethodDirectOnHackMixedSinkBad, sink: HackMixed$static.explicitSinkAllArgs, tainted expression: $sc
 intra_file_flow.hack, IntraFileFlow$static.explicitSinkMethodDirectOnHackMixedSinkBad, 1, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value passed as argument `#1` to `IntraFileFlow$static.explicitSinkMethodDirectOnHackMixedSinkBad` with kind `Simple`,value passed as argument `#1` to `HackMixed$static.explicitSinkAllArgs` with kind `Simple`], source: IntraFileFlow$static.explicitSinkMethodDirectOnHackMixedSinkBad, sink: HackMixed$static.explicitSinkAllArgs, tainted expression: $sc