From 3e82890d6da4e2c96120fe8a4c121bc9a23ebfdb Mon Sep 17 00:00:00 2001 From: Jia Chen Date: Fri, 11 Aug 2017 13:01:34 -0700 Subject: [PATCH] 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 | 8 ++++++++ infer/src/backend/prover.ml | 4 ++++ infer/tests/codetoanalyze/c/errors/issues.exp | 3 --- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 04ba0f721..52b6d1f28 100644 --- a/infer/src/backend/prop.ml +++ b/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) diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 273bd6044..6f548fe82 100644 --- a/infer/src/backend/prover.ml +++ b/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, _) diff --git a/infer/tests/codetoanalyze/c/errors/issues.exp b/infer/tests/codetoanalyze/c/errors/issues.exp index 85128b0bb..10f14755b 100644 --- a/infer/tests/codetoanalyze/c/errors/issues.exp +++ b/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