From 81f31068e249248b0e4c81fb6a57c0fc1f236d02 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 17 Oct 2018 07:01:00 -0700 Subject: [PATCH] [Uninit][9/13] Check rhs using prestate Reviewed By: da319 Differential Revision: D10250227 fbshipit-source-id: c72e08924 --- infer/src/checkers/uninit.ml | 40 +++++------- infer/tests/codetoanalyze/c/uninit/arrays.c | 63 +++++++++++++++++++ infer/tests/codetoanalyze/c/uninit/issues.exp | 6 ++ infer/tests/codetoanalyze/c/uninit/uninit.c | 9 ++- 4 files changed, 94 insertions(+), 24 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/uninit/arrays.c diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index e895fc8f9..c57df938d 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -184,6 +184,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let exec_instr (astate : Domain.astate) {ProcData.pdesc; extras= {formals; summary}; tenv} _ (instr : HilInstr.t) = + let check_access_expr ~loc rhs_access_expr = + if should_report_var pdesc tenv astate.maybe_uninit_vars rhs_access_expr then + report_intra rhs_access_expr loc summary + in + let check_hil_expr ~loc = function + | HilExp.AccessExpression access_expr -> + check_access_expr ~loc access_expr + | _ -> + () + in let update_prepost access_expr rhs = let lhs_base = AccessExpression.get_base access_expr in if @@ -198,6 +208,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in match instr with | Assign (lhs_access_expr, rhs_expr, loc) -> + (* check on lhs_typ to avoid false positive when assigning a pointer to another *) + ( match AccessExpression.get_typ lhs_access_expr tenv with + | Some lhs_typ when not (Typ.is_reference lhs_typ) -> + check_hil_expr ~loc rhs_expr + | _ -> + () ) ; let maybe_uninit_vars' = MaybeUninitVars.remove lhs_access_expr astate.maybe_uninit_vars in let maybe_uninit_vars = if AccessExpression.is_base lhs_access_expr then @@ -208,22 +224,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else maybe_uninit_vars' in let prepost = update_prepost lhs_access_expr rhs_expr in - (* check on lhs_typ to avoid false positive when assigning a pointer to another *) - let is_lhs_not_a_pointer = - match AccessExpression.get_typ lhs_access_expr tenv with - | None -> - false - | Some lhs_ap_typ -> - not (Typ.is_reference lhs_ap_typ) - in - ( match rhs_expr with - | AccessExpression rhs_access_expr -> - if - should_report_var pdesc tenv maybe_uninit_vars rhs_access_expr - && is_lhs_not_a_pointer - then report_intra rhs_access_expr loc summary - | _ -> - () ) ; {astate with maybe_uninit_vars; prepost} | Call (_, Direct callee_pname, _, _, _) when Typ.Procname.equal callee_pname BuiltinDecl.objc_cpp_throw -> @@ -299,13 +299,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct () ) ; {astate with maybe_uninit_vars} | Assume (expr, _, _, loc) -> - ( match expr with - | AccessExpression rhs_access_expr -> - if should_report_var pdesc tenv astate.maybe_uninit_vars rhs_access_expr then - report_intra rhs_access_expr loc summary - | _ -> - () ) ; - astate + check_hil_expr expr ~loc ; astate let pp_session_name node fmt = F.fprintf fmt "uninit %a" CFG.Node.pp_id (CFG.Node.id node) diff --git a/infer/tests/codetoanalyze/c/uninit/arrays.c b/infer/tests/codetoanalyze/c/uninit/arrays.c new file mode 100644 index 000000000..d4f7f70cb --- /dev/null +++ b/infer/tests/codetoanalyze/c/uninit/arrays.c @@ -0,0 +1,63 @@ +/* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +int array_good1_FP() { + int a[10]; + for (int i = 0; i < 10; i++) { + a[i] = 0; + } + return a[2]; +} + +int array_bad() { + int a[10]; + for (int i = 0; i < 5; i++) { + a[i] = 0; + } + return a[9]; +} + +int nondet(); + +int array_good2_FP() { + int* a[10]; + int i = 0; + while (i < 10) { + if (nondet()) { + a[i] = 0; + i++; + } + } + return a[2]; +} + +int array_good3_FP(int m) { + int* a[1000]; + int i = 0; + while (i < 1000 && i < m) { + if (nondet()) { + a[i] = 0; + m--; + } + } + return i > 0 ? a[i - 1] : 42; +} + +void mayinit_vpp(const void**); +void use_vp(void*); + +void* call_to_mayinit_and_return_good_FP() { + void* obj[10]; + mayinit_vpp((const void**)obj); + return obj[0]; +} + +void call_to_mayinit_and_call_use_good() { + void* obj[10]; + mayinit_vpp((const void**)obj); + use_vp(obj[0]); +} diff --git a/infer/tests/codetoanalyze/c/uninit/issues.exp b/infer/tests/codetoanalyze/c/uninit/issues.exp index 298d58b6f..b8be233ad 100644 --- a/infer/tests/codetoanalyze/c/uninit/issues.exp +++ b/infer/tests/codetoanalyze/c/uninit/issues.exp @@ -1 +1,7 @@ +codetoanalyze/c/uninit/arrays.c, array_bad, 5, UNINITIALIZED_VALUE, no_bucket, ERROR, [] +codetoanalyze/c/uninit/arrays.c, array_good1_FP, 5, UNINITIALIZED_VALUE, no_bucket, ERROR, [] +codetoanalyze/c/uninit/arrays.c, array_good2_FP, 9, UNINITIALIZED_VALUE, no_bucket, ERROR, [] +codetoanalyze/c/uninit/arrays.c, array_good3_FP, 9, UNINITIALIZED_VALUE, no_bucket, ERROR, [] +codetoanalyze/c/uninit/arrays.c, call_to_mayinit_and_return_good_FP, 3, UNINITIALIZED_VALUE, no_bucket, ERROR, [] codetoanalyze/c/uninit/uninit.c, dereference_bad, 2, UNINITIALIZED_VALUE, no_bucket, ERROR, [] +codetoanalyze/c/uninit/uninit.c, self_assign_bad, 2, UNINITIALIZED_VALUE, no_bucket, ERROR, [] diff --git a/infer/tests/codetoanalyze/c/uninit/uninit.c b/infer/tests/codetoanalyze/c/uninit/uninit.c index 839f1e997..63c09354d 100644 --- a/infer/tests/codetoanalyze/c/uninit/uninit.c +++ b/infer/tests/codetoanalyze/c/uninit/uninit.c @@ -21,7 +21,14 @@ int dereference_bad() { return *p; } -void FN_self_assign() { +void self_assign_bad() { int x; x = x; } + +void use_and_mayinit(int, int*); + +void call_to_use_and_mayinit_bad_FN() { + int x; + use_and_mayinit(x, &x); +}