From 6bacdf4a4dc33b8f13e3ed07f78e872e98e386ca Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 28 Feb 2018 21:59:48 -0800 Subject: [PATCH] [inferbo] Return newly allocated locations in callees Summary: At function calls, it copies a subset of heap memory that is newly allocated by callees and is reachable from the return value. Reviewed By: mbouaziz Differential Revision: D7081425 fbshipit-source-id: 1ce777a --- infer/src/bufferoverrun/absLoc.ml | 3 ++ .../src/bufferoverrun/bufferOverrunChecker.ml | 24 ++++++++--- .../src/bufferoverrun/bufferOverrunDomain.ml | 42 +++++++++++++++++++ .../codetoanalyze/cpp/bufferoverrun/class.cpp | 14 ++++++- .../cpp/bufferoverrun/issues.exp | 4 +- 5 files changed, 80 insertions(+), 7 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index b13626f8b..fc306d3dc 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -64,6 +64,9 @@ module Loc = struct Mangled.equal (Pvar.get_name x) Ident.name_return | _ -> false + + + let is_field_of ~loc ~field_loc = match field_loc with Field (l, _) -> equal loc l | _ -> false end module PowLoc = struct diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index dafa5bbf0..fc218cff9 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -63,9 +63,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in Dom.Mem.add_heap loc v mem | Typ.Tptr (typ, _) -> - BoUtils.Exec.decl_sym_arr - ~decl_sym_val:(decl_sym_val ~may_last_field) - pname tenv node location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem + BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname tenv node + location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tarray {elt; length} -> let size = match length with @@ -119,7 +118,20 @@ module TransferFunctions (CFG : ProcCfg.S) = struct List.fold ~f:add_formal ~init:(mem, inst_num) formals |> fst - let instantiate_ret ret callee_pname callee_exit_mem subst_map mem ret_alias location = + let instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem subst_map mem ret_alias + location = + let copy_reachable_new_locs_from locs mem = + let copy loc acc = + let v = + Dom.Mem.find_heap loc callee_exit_mem |> (fun v -> Dom.Val.subst v subst_map location) + |> Dom.Val.add_trace_elem (Trace.Return location) + in + Dom.Mem.add_heap loc v acc + in + let new_locs = Dom.Mem.get_new_heap_locs ~prev:callee_entry_mem ~next:callee_exit_mem in + let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in + PowLoc.fold copy (PowLoc.inter new_locs reachable_locs) mem + in match ret with | Some (id, _) -> let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in @@ -129,6 +141,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let mem = Option.value_map ret_alias ~default:mem ~f:add_ret_alias in Dom.Val.subst ret_val subst_map location |> Dom.Val.add_trace_elem (Trace.Return location) |> Fn.flip (Dom.Mem.add_stack ret_var) mem + |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val) | None -> mem @@ -184,7 +197,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let subst_map, ret_alias = Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias in - instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem ret_alias location + instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem subst_map caller_mem + ret_alias location |> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location | None -> caller_mem diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 3e5925b37..ebd99bb45 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -734,6 +734,28 @@ module MemReach = struct else {m with latest_prune= LatestPrune.Top} | _, _, _ -> {m with latest_prune= LatestPrune.Top} + + + let get_new_heap_locs : prev:t -> next:t -> PowLoc.t = + fun ~prev ~next -> + let add_loc loc _val acc = if Heap.mem loc prev.heap then acc else PowLoc.add loc acc in + Heap.fold add_loc next.heap PowLoc.empty + + + let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t = + let add_reachable1 ~root loc v acc = + if Loc.equal root loc then PowLoc.union acc (Val.get_all_locs v) + else if Loc.is_field_of ~loc:root ~field_loc:loc then PowLoc.add loc acc + else acc + in + let rec add_from_locs heap locs acc = PowLoc.fold (add_from_loc heap) locs acc + and add_from_loc heap loc acc = + if PowLoc.mem loc acc then acc + else + let reachable_locs = Heap.fold (add_reachable1 ~root:loc) heap PowLoc.empty in + add_from_locs heap reachable_locs (PowLoc.add loc acc) + in + fun locs m -> add_from_locs m.heap locs PowLoc.empty end module Mem = struct @@ -749,6 +771,15 @@ module Mem = struct fun default f m -> match m with Bottom -> default | NonBottom m' -> f m' + let f_lift_default2 : 'a -> (MemReach.t -> MemReach.t -> 'a) -> t -> t -> 'a = + fun default f m1 m2 -> + match (m1, m2) with + | Bottom, _ | _, Bottom -> + default + | NonBottom m1', NonBottom m2' -> + f m1' m2' + + let f_lift : (MemReach.t -> MemReach.t) -> t -> t = fun f -> f_lift_default Bottom (fun m' -> NonBottom (f m')) @@ -816,6 +847,17 @@ module Mem = struct let get_return : t -> Val.t = f_lift_default Val.bot MemReach.get_return + let get_new_heap_locs : prev:t -> next:t -> PowLoc.t = + fun ~prev ~next -> + f_lift_default2 PowLoc.empty + (fun m1 m2 -> MemReach.get_new_heap_locs ~prev:m1 ~next:m2) + prev next + + + let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t = + fun locs -> f_lift_default PowLoc.empty (MemReach.get_reachable_locs_from locs) + + let update_mem : PowLoc.t -> Val.t -> t -> t = fun ploc v -> f_lift (MemReach.update_mem ploc v) let transform_mem : f:(Val.t -> Val.t) -> PowLoc.t -> t -> t = diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp index 59f571b15..795287640 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp @@ -157,7 +157,7 @@ void flexible_array5_Good() { t->set_child(Tree::NewLeaf(), 2); } -void flexible_array5_Bad_FN() { +void flexible_array5_Bad() { Tree* t = Tree::NewNode(3); t->set_child(Tree::NewLeaf(), 5); } @@ -173,3 +173,15 @@ void flexible_array_param_Bad() { my_class4* x = (my_class4*)malloc(sizeof(my_class4) + 2 * sizeof(int)); flexible_array_param_access(x); } + +char* my_malloc() { return (char*)malloc(sizeof(my_class4) + 4 * sizeof(int)); } + +void return_class_Good() { + my_class4* x = (my_class4*)my_malloc(); + x->b[3] = 0; +} + +void return_class_Bad() { + my_class4* x = (my_class4*)my_malloc(); + x->b[5] = 0; +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index d68ec9d5d..3e92a57de 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -3,10 +3,12 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_O codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [5, 5] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Return,Call,ArrayAccess: Offset: [5, 5] Size: [3, 3] @ codetoanalyze/cpp/bufferoverrun/class.cpp:139:51 by call `Tree_set_child()` ] codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, [Call,ArrayAccess: Offset: [3, 3] Size: [3, 3] @ codetoanalyze/cpp/bufferoverrun/class.cpp:165:50 by call `flexible_array_param_access()` ] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, [Call,Assignment,Call,Assignment,Return,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, [Call,Call,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, [Offset: [10, 10] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, [Return,ArrayAccess: Offset: [5, 5] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_L5, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, +oo]] @@ -25,7 +27,7 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERR codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [6, 6] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [4, 4] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, [Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, [Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [u$4, u$5] Size: [u$4, u$5]]