[infer][backend] Teach the biabduction analysis more simplification rules

Reviewed By: sblackshear

Differential Revision: D5550469

fbshipit-source-id: 57ffed4

infer/src/backend/prover.ml

@@ -1310,6 +1310,11 @@ let exp_imply tenv calc_missing (subs: subst2) e1_in e2_in : subst2 =
     match (e1, e2) with
     | Exp.Var v1, Exp.Var v2
      -> var_imply subs v1 v2
+    | Exp.BinOp ((PlusA | PlusPI | MinusA | MinusPI), Exp.Var v1, e2), Exp.Var v2
+      when Ident.equal v1 v2
+     -> do_imply subs e2 Exp.zero
+    | Exp.BinOp ((PlusA | PlusPI), e2, Exp.Var v1), Exp.Var v2 when Ident.equal v1 v2
+     -> do_imply subs e2 Exp.zero
     | e1, Exp.Var v2
      -> let occurs_check v e =
           (* check whether [v] occurs in normalized [e] *)

infer/tests/codetoanalyze/cpp/errors/issues.exp

@@ -51,8 +51,12 @@ codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_result_method_n
 codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_result_method_ok_deref, 4, UNINITIALIZED_VALUE, [start of procedure boxed_ptr::smart_ptr_result_method_ok_deref(),start of procedure SmartPtr,return from a call to boxed_ptr::SmartPtr_SmartPtr,start of procedure X,return from a call to boxed_ptr::X_X,start of procedure get,return from a call to boxed_ptr::SmartPtr_get,start of procedure getPtr,return from a call to boxed_ptr::X_getPtr]
 codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_nonzero_deref2_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_nonzero_deref2_bad(),start of procedure cancellation_test::is_size_zero(),start of procedure begin,return from a call to cancellation_test::Test_begin,start of procedure end,return from a call to cancellation_test::Test_end,Condition is false,return from a call to cancellation_test::is_size_zero,Condition is false,Condition is true]
 codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_nonzero_deref_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_nonzero_deref_bad(),start of procedure cancellation_test::is_size_zero(),start of procedure begin,return from a call to cancellation_test::Test_begin,start of procedure end,return from a call to cancellation_test::Test_end,Condition is false,return from a call to cancellation_test::is_size_zero,Condition is false,Condition is true]
+codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_nonzero_deref_iter2_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_nonzero_deref_iter2_bad(),start of procedure cancellation_test::is_size_zero_iter(),start of procedure begin_iter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,return from a call to cancellation_test::Test_begin_iter,start of procedure end_iter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,return from a call to cancellation_test::Test_end_iter,start of procedure cancellation_test::operator==(),Condition is false,return from a call to cancellation_test::operator==,return from a call to cancellation_test::is_size_zero_iter,Condition is false,Condition is true]
+codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_nonzero_deref_iter_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_nonzero_deref_iter_bad(),start of procedure cancellation_test::is_size_zero_iter(),start of procedure begin_iter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,return from a call to cancellation_test::Test_begin_iter,start of procedure end_iter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,return from a call to cancellation_test::Test_end_iter,start of procedure cancellation_test::operator==(),Condition is false,return from a call to cancellation_test::operator==,return from a call to cancellation_test::is_size_zero_iter,Condition is false,Condition is true]
 codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_zero_deref2_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_zero_deref2_bad(),start of procedure cancellation_test::is_size_zero(),start of procedure begin,return from a call to cancellation_test::Test_begin,start of procedure end,return from a call to cancellation_test::Test_end,Condition is true,return from a call to cancellation_test::is_size_zero,Condition is true]
 codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_zero_deref_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_zero_deref_bad(),start of procedure cancellation_test::is_size_zero(),start of procedure begin,return from a call to cancellation_test::Test_begin,start of procedure end,return from a call to cancellation_test::Test_end,Condition is true,return from a call to cancellation_test::is_size_zero,Condition is true]
+codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_zero_deref_iter2_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_zero_deref_iter2_bad(),start of procedure cancellation_test::is_size_zero_iter(),start of procedure begin_iter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,return from a call to cancellation_test::Test_begin_iter,start of procedure end_iter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,return from a call to cancellation_test::Test_end_iter,start of procedure cancellation_test::operator==(),Condition is true,return from a call to cancellation_test::operator==,return from a call to cancellation_test::is_size_zero_iter,Condition is true]
+codetoanalyze/cpp/errors/npe/cancellation.cpp, cancellation_test::size_zero_deref_iter_bad, 4, NULL_DEREFERENCE, [start of procedure cancellation_test::size_zero_deref_iter_bad(),start of procedure cancellation_test::is_size_zero_iter(),start of procedure begin_iter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,return from a call to cancellation_test::Test_begin_iter,start of procedure end_iter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,start of procedure TestIter,return from a call to cancellation_test::TestIter_TestIter,return from a call to cancellation_test::Test_end_iter,start of procedure cancellation_test::operator==(),Condition is true,return from a call to cancellation_test::operator==,return from a call to cancellation_test::is_size_zero_iter,Condition is true]
 codetoanalyze/cpp/errors/npe/npe_added_to_b1.cpp, npe_added_to_b1::causes_npe, 2, NULL_DEREFERENCE, [start of procedure npe_added_to_b1::causes_npe(),start of procedure npe_added_to_b1::deref_ref()]
 codetoanalyze/cpp/errors/npe/npe_added_to_b1.cpp, npe_added_to_b1::causes_npe_person, 2, NULL_DEREFERENCE, [start of procedure npe_added_to_b1::causes_npe_person(),start of procedure Person,return from a call to npe_added_to_b1::Person_Person,start of procedure npe_added_to_b1::deref_person()]
 codetoanalyze/cpp/errors/npe/null_returned_by_method.cpp, testNullDeref, 3, NULL_DEREFERENCE, [start of procedure testNullDeref(),Condition is true,start of procedure getNull,return from a call to XFactory_getNull]

infer/tests/codetoanalyze/cpp/errors/npe/cancellation.cpp

@@ -8,16 +8,34 @@
  */
 namespace cancellation_test {
 
+struct TestIter {
+  int y;
+
+  TestIter(int y) : y(y) {}
+};
+
+bool operator==(const TestIter& lhs, const TestIter& rhs) {
+  return lhs.y == rhs.y;
+}
+
 struct Test {
   int x, sz;
 
   int begin() const { return x; }
   int end() const { return x + sz; }
   int end2() const { return x - sz; }
+
+  TestIter begin_iter() const { return x; }
+  TestIter end_iter() const { return x + sz; }
+  TestIter end_iter2() const { return x - sz; }
 };
 
 bool is_size_zero(const Test& t) { return t.begin() == t.end(); }
 bool is_size_zero2(const Test& t) { return t.begin() == t.end2(); }
+bool is_size_zero_iter(const Test& t) { return t.begin_iter() == t.end_iter(); }
+bool is_size_zero2_iter(const Test& t) {
+  return t.begin_iter() == t.end_iter2();
+}
 
 void size_zero_no_deref_ok() {
   int* p = nullptr;
@@ -33,6 +51,20 @@ void size_zero_deref_bad() {
     *p = 42;
 }
 
+void size_nonzero_no_deref_ok() {
+  int* p = nullptr;
+  Test t{1, 1};
+  if (is_size_zero(t))
+    *p = 42;
+}
+
+void size_nonzero_deref_bad() {
+  int* p = nullptr;
+  Test t{1, 1};
+  if (!is_size_zero(t))
+    *p = 42;
+}
+
 void size_nonzero_no_deref2_ok() {
   int* p = nullptr;
   Test t{1, 1};
@@ -61,17 +93,60 @@ void size_zero_deref2_bad() {
     *p = 42;
 }
 
-void size_nonzero_no_deref_ok() {
+void size_zero_no_deref_iter_ok() {
+  int* p = nullptr;
+  Test t{1, 0};
+  if (!is_size_zero_iter(t))
+    *p = 42;
+}
+
+void size_zero_deref_iter_bad() {
+  int* p = nullptr;
+  Test t{1, 0};
+  if (is_size_zero_iter(t))
+    *p = 42;
+}
+
+void size_nonzero_no_deref_iter_ok() {
   int* p = nullptr;
   Test t{1, 1};
-  if (is_size_zero(t))
+  if (is_size_zero_iter(t))
     *p = 42;
 }
 
-void size_nonzero_deref_bad() {
+void size_nonzero_deref_iter_bad() {
   int* p = nullptr;
   Test t{1, 1};
-  if (!is_size_zero(t))
+  if (!is_size_zero_iter(t))
+    *p = 42;
+}
+
+void size_nonzero_no_deref_iter2_ok() {
+  int* p = nullptr;
+  Test t{1, 1};
+  if (is_size_zero_iter(t))
+    *p = 42;
+}
+
+void size_nonzero_deref_iter2_bad() {
+  int* p = nullptr;
+  Test t{1, 1};
+  if (!is_size_zero_iter(t))
+    *p = 42;
+}
+
+void size_zero_no_deref_iter2_ok() {
+  int* p = nullptr;
+  Test t{1, 0};
+  if (!is_size_zero_iter(t))
     *p = 42;
 }
+
+void size_zero_deref_iter2_bad() {
+  int* p = nullptr;
+  Test t{1, 0};
+  if (is_size_zero_iter(t))
+    *p = 42;
+}
+
 } // namespace cancellation_test