Teach the prover more simplification rules

Reviewed By: sblackshear

Differential Revision: D5543631

fbshipit-source-id: a175925

infer/src/backend/prop.ml

@@ -1260,6 +1260,14 @@ module Normalize = struct
        -> if Exp.equal idx1 idx2 then normalize_eq (e1', e2')
           else if Exp.equal e1' e2' then normalize_eq (idx1, idx2)
           else eq
+      | BinOp ((PlusA | PlusPI | MinusA | MinusPI), e1, e2), e1' when Exp.equal e1 e1'
+       -> (e2, Exp.int IntLit.zero)
+      | BinOp ((PlusA | PlusPI), e2, e1), e1' when Exp.equal e1 e1'
+       -> (e2, Exp.int IntLit.zero)
+      | e1', BinOp ((PlusA | PlusPI | MinusA | MinusPI), e1, e2) when Exp.equal e1 e1'
+       -> (e2, Exp.int IntLit.zero)
+      | e1', BinOp ((PlusA | PlusPI), e2, e1) when Exp.equal e1 e1'
+       -> (e2, Exp.int IntLit.zero)
       | _
        -> eq
     in

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

@@ -49,6 +49,10 @@ codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_null_method_der
 codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_ok_field_deref, 4, UNINITIALIZED_VALUE, [start of procedure boxed_ptr::smart_ptr_ok_field_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]
 codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_result_method_null_deref, 4, NULL_DEREFERENCE, [start of procedure boxed_ptr::smart_ptr_result_method_null_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 getNull,return from a call to boxed_ptr::X_getNull]
 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_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/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

@@ -0,0 +1,77 @@
+/*
+ * 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.
+ */
+namespace cancellation_test {
+
+struct Test {
+  int x, sz;
+
+  int begin() const { return x; }
+  int end() const { return x + sz; }
+  int end2() 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(); }
+
+void size_zero_no_deref_ok() {
+  int* p = nullptr;
+  Test t{1, 0};
+  if (!is_size_zero(t))
+    *p = 42;
+}
+
+void size_zero_deref_bad() {
+  int* p = nullptr;
+  Test t{1, 0};
+  if (is_size_zero(t))
+    *p = 42;
+}
+
+void size_nonzero_no_deref2_ok() {
+  int* p = nullptr;
+  Test t{1, 1};
+  if (is_size_zero(t))
+    *p = 42;
+}
+
+void size_nonzero_deref2_bad() {
+  int* p = nullptr;
+  Test t{1, 1};
+  if (!is_size_zero(t))
+    *p = 42;
+}
+
+void size_zero_no_deref2_ok() {
+  int* p = nullptr;
+  Test t{1, 0};
+  if (!is_size_zero(t))
+    *p = 42;
+}
+
+void size_zero_deref2_bad() {
+  int* p = nullptr;
+  Test t{1, 0};
+  if (is_size_zero(t))
+    *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;
+}
+} // namespace cancellation_test