From 8567afdf55de24b55dab78bc2614324c932c3e5f Mon Sep 17 00:00:00 2001 From: Kihong Heo Date: Mon, 12 Jun 2017 18:22:23 -0700 Subject: [PATCH] [inferbo] add instantiation for parameters (call-by-ptr/ref) Reviewed By: mbouaziz Differential Revision: D5155025 fbshipit-source-id: c0b4161 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 66 ++++++++++++++----- .../src/bufferoverrun/bufferOverrunDomain.ml | 11 ++-- .../c/bufferoverrun/function_call.c | 38 ++++++++++- .../codetoanalyze/c/bufferoverrun/issues.exp | 8 ++- .../cpp/bufferoverrun/function_call.cpp | 10 ++- .../cpp/bufferoverrun/issues.exp | 2 +- 6 files changed, 106 insertions(+), 29 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 2837f72b4..40dc275d9 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -223,10 +223,52 @@ struct List.fold ~f:add_formal ~init:(mem, inst_num, 0) (Sem.get_formals pdesc) |> fst3 - let instantiate_ret - : Tenv.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list - -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Val.astate - = fun tenv callee_pdesc callee_pname params caller_mem summary loc -> + let instantiate_ret ret callee_pname callee_exit_mem subst_map mem = + match ret with + | Some (id, _) -> + let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in + let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in + let ret_var = Loc.of_var (Var.of_id id) in + Dom.Val.subst ret_val subst_map + |> Fn.flip (Dom.Mem.add_stack ret_var) mem + | None -> mem + + let instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location mem = + let formals = Sem.get_formals pdesc in + let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem location) params in + let f mem formal actual = + match (snd formal).Typ.desc with + | Typ.Tptr (typ, _) -> + (match typ.Typ.desc with + | Typ.Tstruct typename -> + (match Tenv.lookup tenv typename with + | Some str -> + let formal_locs = Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_entry_mem + |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in + let instantiate_fld mem (fn, _, _) = + let formal_fields = PowLoc.append_field formal_locs fn in + let v = Dom.Mem.find_heap_set formal_fields callee_exit_mem in + let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) fn in + Dom.Val.subst v subst_map + |> Fn.flip (Dom.Mem.strong_update_heap actual_fields) mem + in + List.fold ~f:instantiate_fld ~init:mem str.Typ.Struct.fields + | _ -> mem) + | _ -> + let formal_locs = Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_entry_mem + |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in + let v = Dom.Mem.find_heap_set formal_locs callee_exit_mem in + let actual_locs = Dom.Val.get_all_locs actual in + Dom.Val.subst v subst_map + |> Fn.flip (Dom.Mem.strong_update_heap actual_locs) mem) + | _ -> mem + in + try List.fold2_exn formals actuals ~init:mem ~f with Invalid_argument _ -> mem + + let instantiate_mem + : Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t option -> Typ.Procname.t + -> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate + = fun tenv ret callee_pdesc callee_pname params caller_mem summary loc -> let callee_entry_mem = Dom.Summary.get_input summary in let callee_exit_mem = Dom.Summary.get_output summary in match callee_pdesc with @@ -234,11 +276,9 @@ struct let subst_map = Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc in - let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in - let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in - Dom.Val.subst ret_val subst_map - |> Dom.Val.normalize (* normalize bottom *) - | _ -> Dom.Val.Itv.top + instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem + |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map loc + | None -> caller_mem let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit = fun instr pre post -> @@ -270,13 +310,7 @@ struct (match Summary.read_summary pdesc callee_pname with | Some summary -> let callee = extras callee_pname in - let ret_val = - instantiate_ret tenv callee callee_pname params mem summary loc - in - (match ret with - | Some (id, _) -> - Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) ret_val mem - | _ -> mem) + instantiate_mem tenv ret callee callee_pname params mem summary loc | None -> handle_unknown_call pname ret callee_pname params node mem loc) | Declare_locals (locals, _) -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index a84b875fe..2c2467250 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -385,11 +385,6 @@ struct then { bot with itv = Itv.top } else { bot with itv = ArrayBlk.diff x.arrayblk y.arrayblk } - let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t - = fun x subst_map -> - { x with itv = Itv.subst x.itv subst_map; - arrayblk = ArrayBlk.subst x.arrayblk subst_map } - let get_symbols : t -> Itv.Symbol.t list = fun x -> List.append (Itv.get_symbols x.itv) (ArrayBlk.get_symbols x.arrayblk) @@ -398,6 +393,12 @@ struct = fun x -> { x with itv = Itv.normalize x.itv; arrayblk = ArrayBlk.normalize x.arrayblk } + let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t + = fun x subst_map -> + { x with itv = Itv.subst x.itv subst_map; + arrayblk = ArrayBlk.subst x.arrayblk subst_map } + |> normalize (* normalize bottom *) + let pp_summary : F.formatter -> t -> unit = fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c b/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c index 466d586da..079c5636e 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c @@ -12,6 +12,10 @@ #include +struct S { + int field; +}; + void arr_access(int* arr, char* p, int i) { int x = arr[0]; arr[x] = 1; /* BUG */ @@ -29,16 +33,46 @@ void ptr_set_to_zero(int* x) { *x = 0; } -void call_by_ptr_good_FP() { +void struct_ptr_set_to_zero(struct S* s) { s->field = 0; } + +void call_by_ptr_good() { int arr[10]; int i = 99; ptr_set_to_zero(&i); arr[i] = 123; } -void call_by_ptr_bad_FN() { +void call_by_arr_good() { + int arr[10]; + ptr_set_to_zero(&arr); + arr[arr[0]] = 123; +} + +void call_by_struct_ptr_good() { + int arr[10]; + struct S* s = (struct S*)malloc(sizeof(struct S)); + s->field = 99; + struct_ptr_set_to_zero(s); + arr[s->field] = 123; +} + +void call_by_ptr_bad() { int arr[10]; int i = 5; ptr_set_to_zero(&i); arr[i - 1] = 123; } + +void call_by_arr_bad() { + int arr[10]; + ptr_set_to_zero(&arr); + arr[arr[0] - 1] = 123; +} + +void call_by_struct_ptr_bad() { + int arr[10]; + struct S* sp = (struct S*)malloc(sizeof(struct S)); + sp->field = 5; + struct_ptr_set_to_zero(sp); + arr[sp->field - 1] = 123; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 4d3c83e04..2faf6535e 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -6,9 +6,11 @@ codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset: codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10]] codetoanalyze/c/bufferoverrun/for_loop.c, safealloc, 10, UNREACHABLE_CODE, [] -codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_good_FP, 4, BUFFER_OVERRUN, [Offset: [99, 99] Size: [10, 10]] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:18:3 by call `arr_access()` ] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call `arr_access()` ] +codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:21:3 by call `arr_access()` ] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:22:3 by call `arr_access()` ] codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, [] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/function_call.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/function_call.cpp index 9bf80bfbc..0b847be29 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/function_call.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/function_call.cpp @@ -7,18 +7,24 @@ * of patent rights can be found in the PATENTS file in the same directory. */ +struct S { + int field; +}; + void ref_set_to_zero(int& x) { x = 0; } -void call_by_ref_good_FP() { +void struct_ref_set_to_zero(struct S& s) { s.field = 0; } + +void call_by_ref_good() { int arr[10]; int i = 99; ref_set_to_zero(i); arr[i] = 123; } -void call_by_ref_bad_FN() { +void call_by_ref_bad() { int arr[10]; int i = 5; ref_set_to_zero(i); diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 7ab2111f8..81bc13655 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_good_FP, 4, BUFFER_OVERRUN, [Offset: [99, 99] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Offset: [s$6, s$7] Size: [s$6, s$7] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]