Teach the prover and the normalizer aliasing rules between pointers and integers

Reviewed By: sblackshear

Differential Revision: D5604587

fbshipit-source-id: c8045df

infer/src/backend/prop.ml

@@ -775,6 +775,10 @@ module Normalize = struct
          -> Exp.bool (IntLit.eq n m)
         | Const Cfloat v, Const Cfloat w
          -> Exp.bool (Float.equal v w)
+        | Const Cint _, Exp.Lvar _ | Exp.Lvar _, Const Cint _
+         -> (* Comparing pointer with nonzero integer is undefined behavior in ISO C++ *)
+            (* Assume they are not equal *)
+            Exp.zero
         | e1', e2'
          -> Exp.eq e1' e2' )
       | BinOp (Ne, e1, e2) -> (
@@ -783,6 +787,10 @@ module Normalize = struct
          -> Exp.bool (IntLit.neq n m)
         | Const Cfloat v, Const Cfloat w
          -> Exp.bool (v <> w)
+        | Const Cint _, Exp.Lvar _ | Exp.Lvar _, Const Cint _
+         -> (* Comparing pointer with nonzero integer is undefined behavior in ISO C++ *)
+            (* Assume they are not equal *)
+            Exp.one
         | e1', e2'
          -> Exp.ne e1' e2' )
       | BinOp (LAnd, e1, e2)

infer/src/backend/prover.ml

@@ -704,6 +704,10 @@ let check_disequal tenv prop e1 e2 =
     | Exp.Lvar pv, Exp.Var id | Exp.Var id, Exp.Lvar pv
      -> (* Address of any non-global var must be different from the value of any footprint var *)
         not (Pvar.is_global pv) && Ident.is_footprint id
+    | Exp.Lvar _, Exp.Const Const.Cint _ | Exp.Const Const.Cint _, Exp.Lvar _
+     -> (* Comparing pointer with nonzero integer is undefined behavior in ISO C++ *)
+        (* Assume they are not equal *)
+        true
     | Exp.UnOp (op1, e1, _), Exp.UnOp (op2, e2, _)
      -> if Unop.equal op1 op2 then check_expr_disequal e1 e2 else false
     | Exp.Lfield (e1, f1, _), Exp.Lfield (e2, f2, _)

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

@@ -84,11 +84,8 @@ codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c, null_pointer
 codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c, potentially_null_pointer_passed_as_argument, 3, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/null_pointer_dereference.c, simple_null_pointer, 2, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/short.c, f_error, 2, NULL_DEREFERENCE
-codetoanalyze/c/errors/null_dereference/short.c, f_error, 2, NULL_TEST_AFTER_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/short.c, g_error, 2, NULL_DEREFERENCE
-codetoanalyze/c/errors/null_dereference/short.c, g_error, 2, NULL_TEST_AFTER_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/short.c, l_error, 2, NULL_DEREFERENCE
-codetoanalyze/c/errors/null_dereference/short.c, m, 2, NULL_TEST_AFTER_DEREFERENCE
 codetoanalyze/c/errors/null_test_after_deref/basic.c, null_test_deref_basic_bad, 2, NULL_TEST_AFTER_DEREFERENCE
 codetoanalyze/c/errors/resource_leaks/leak.c, fileNotClosed, 5, RESOURCE_LEAK
 codetoanalyze/c/errors/resource_leaks/leak.c, socketNotClosed, 5, RESOURCE_LEAK