diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 3fefc484b..25d2aab72 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -372,7 +372,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct "/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp loc in mem - | Remove_temps _ | Abstract _ | Nullify _ + | Remove_temps (temps, _) + -> Dom.Mem.remove_temps temps mem + | Abstract _ | Nullify _ -> mem in print_debug_info instr mem output_mem ; output_mem @@ -621,6 +623,7 @@ let checker : Callbacks.proc_callback_args -> Specs.summary = fun {proc_desc; tenv; summary; get_proc_desc} -> let proc_name = Specs.get_proc_name summary in let proc_data = ProcData.make proc_desc tenv get_proc_desc in + if not (Procdesc.did_preanalysis proc_desc) then Preanal.do_liveness proc_desc tenv ; match compute_post proc_data with | Some post -> if Config.bo_debug >= 1 then print_summary proc_name post ; diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 6519c5a03..147e8cce4 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -447,6 +447,14 @@ module Stack = struct if Loc.is_logical_var k then () else F.fprintf fmt "%a -> %a@," Loc.pp k Val.pp_summary v in iter pp_not_logical_var mem + + let remove_temps : Ident.t list -> astate -> astate = + fun temps mem -> + let remove_temp mem temp = + let temp_loc = Loc.of_id temp in + remove temp_loc mem + in + List.fold temps ~init:mem ~f:remove_temp end module Heap = struct @@ -552,6 +560,11 @@ module AliasMap = struct fun k m -> try Some (M.find k m) with Not_found -> None + + let remove_temps : Ident.t list -> t -> t = + fun temps m -> + let remove_temp m temp = M.remove temp m in + List.fold temps ~init:m ~f:remove_temp end module AliasRet = struct @@ -620,6 +633,9 @@ module Alias = struct Option.value_map (find l a) ~default:a ~f:update_ret | _ -> a + + let remove_temps : Ident.t list -> astate -> astate = + fun temps a -> (AliasMap.remove_temps temps (fst a), snd a) end module MemReach = struct @@ -715,6 +731,10 @@ module MemReach = struct L.(debug BufferOverrun Verbose) "Weak update for %a <- %a@." PowLoc.pp ploc Val.pp v in weak_update_heap ploc v s + + let remove_temps : Ident.t list -> t -> t = + fun temps m -> + {m with stack= Stack.remove_temps temps m.stack; alias= Alias.remove_temps temps m.alias} end module Mem = struct @@ -784,6 +804,8 @@ module Mem = struct let can_strong_update : PowLoc.t -> bool = MemReach.can_strong_update let update_mem : PowLoc.t -> Val.t -> t -> t = fun ploc v -> f_lift (MemReach.update_mem ploc v) + + let remove_temps : Ident.t list -> t -> t = fun temps -> f_lift (MemReach.remove_temps temps) end module Summary = struct diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 64732ac30..a313b2a3f 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -6,6 +6,9 @@ codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 7, BUFFER_OVERRUN, [Ar codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 8, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, [] +codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, [] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN, [Call,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/remove_temps.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/remove_temps.cpp new file mode 100644 index 000000000..4a5a55611 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/remove_temps.cpp @@ -0,0 +1,39 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +#include + +struct S { + std::vector l; + S* next; + std::atomic ptr; +}; + +class C { + void foo_Bad(); + void goo(); + S head_; +}; + +void C::foo_Bad() { + while (1) { + S* t = head_.next; + int x = t->l.size(); + void* ptr = t->ptr; + int a[5]; + a[10] = 1; + } +} + +void C::goo() { + while (1) { + S* t = head_.next; + int x = t->l.size(); + void* ptr = t->ptr; + } +}