diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 9b8f0784c..61f7ed3ab 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -201,6 +201,23 @@ module TransferFunctions = struct | Load {id; e= exp; typ} -> let represents_multiple_values = is_array_access_exp exp in BoUtils.Exec.load_locs ~represents_multiple_values id typ (Sem.eval_locs exp mem) mem + | Store {e1= tgt_exp; e2= Const (Const.Cstr _) as src; loc= location} + when Language.curr_language_is Java -> + let pname = Summary.get_proc_name summary in + let node_hash = CFG.Node.hash node in + let model_env = + BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + in + let tgt_locs = Sem.eval_locs tgt_exp mem in + let tgt_deref = + let allocsite = + Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None + ~represents_multiple_values:false + in + PowLoc.singleton (Loc.of_allocsite allocsite) + in + Dom.Mem.update_mem tgt_locs (Dom.Val.of_pow_loc ~traces:Dom.TraceSet.bottom tgt_deref) mem + |> Models.JavaString.constructor_from_char_ptr model_env tgt_deref src | Store {e1= exp1; e2= Const (Const.Cstr s); loc= location} -> let locs = Sem.eval_locs exp1 mem in let model_env = diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 96931c970..71e97ca01 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -564,6 +564,40 @@ module ArrObjCommon = struct let arr_locs = deref_of model_env exp ~fn mem in let mem = Dom.Mem.add_stack (Loc.of_id id) (eval_array_locs_length arr_locs mem) mem in load_size_alias id arr_locs mem + + + let at arr_exp ~fn index_exp = + let exec ({pname; location} as model_env) ~ret:(id, _) mem = + let array_v = + let locs = deref_of model_env arr_exp ~fn mem in + if PowLoc.is_bot locs then Dom.Val.unknown_from ~callee_pname:(Some pname) ~location + else Dom.Mem.find_set locs mem + in + Dom.Mem.add_stack (Loc.of_id id) array_v mem + and check ({location; integer_type_widths} as model_env) mem cond_set = + let idx = Sem.eval integer_type_widths index_exp mem in + let arr = Dom.Mem.find_set (deref_of model_env arr_exp ~fn mem) mem in + let relation = Dom.Mem.get_relation mem in + let latest_prune = Dom.Mem.get_latest_prune mem in + BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true + ~last_included:false ~latest_prune location cond_set + in + {exec; check} + + + let copy_constructor model_env deref_of_tgt ~fn src_exp mem = + let deref_of_src = deref_of model_env src_exp ~fn mem in + Dom.Mem.update_mem deref_of_tgt (Dom.Mem.find_set deref_of_src mem) mem + + + let constructor_from_char_ptr ({integer_type_widths} as model_env) tgt_deref ~fn src mem = + let elem_locs = PowLoc.append_field tgt_deref ~fn in + match src with + | Exp.Const (Const.Cstr s) -> + BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem + | _ -> + let v = Sem.eval integer_type_widths src mem in + Dom.Mem.update_mem elem_locs v mem end module StdVector = struct @@ -614,31 +648,16 @@ module StdVector = struct (Dom.Val.get_all_locs v, Dom.Val.get_traces v) in let deref_of_vec = append_fields vec_locs ~vec_typ ~elt_typ in - let deref_of_src = deref_of model_env elt_typ (src_exp, vec_typ) mem in + let fn = BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ in mem |> Dom.Mem.update_mem vec_locs (Dom.Val.of_pow_loc ~traces deref_of_vec) - |> Dom.Mem.update_mem deref_of_vec (Dom.Mem.find_set deref_of_src mem) + |> ArrObjCommon.copy_constructor model_env deref_of_vec ~fn src_exp in {exec; check= no_check} - let at elt_typ vec_arg index_exp = - let exec ({pname; location} as model_env) ~ret:(id, _) mem = - let array_v = - let locs = deref_of model_env elt_typ vec_arg mem in - if PowLoc.is_bot locs then Dom.Val.unknown_from ~callee_pname:(Some pname) ~location - else Dom.Mem.find_set locs mem - in - Dom.Mem.add_stack (Loc.of_id id) array_v mem - and check ({location; integer_type_widths} as model_env) mem cond_set = - let idx = Sem.eval integer_type_widths index_exp mem in - let arr = Dom.Mem.find_set (deref_of model_env elt_typ vec_arg mem) mem in - let relation = Dom.Mem.get_relation mem in - let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp:None ~relation ~is_plus:true - ~last_included:false ~latest_prune location cond_set - in - {exec; check} + let at elt_typ (vec_exp, vec_typ) index_exp = + ArrObjCommon.at vec_exp ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ) index_exp let set_size {location} locs new_size mem = @@ -693,8 +712,8 @@ module StdVector = struct end module StdBasicString = struct - let constructor_from_char_ptr_common char_typ (tgt_exp, tgt_typ) src ~len_opt = - let exec ({pname; node_hash; integer_type_widths} as model_env) ~ret mem = + let constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src ~len_opt = + let exec ({pname; node_hash} as model_env) ~ret mem = let mem = Option.value_map len_opt ~default:mem ~f:(fun len -> let {exec= malloc_exec} = malloc ~can_be_zero:true len in @@ -711,13 +730,8 @@ module StdBasicString = struct let mem = Dom.Mem.update_mem tgt_locs (Dom.Val.of_pow_loc ~traces:Trace.Set.bottom tgt_deref) mem in - let elem_locs = StdVector.append_fields ~vec_typ:tgt_typ ~elt_typ:char_typ tgt_deref in - match src with - | Exp.Const (Const.Cstr s) -> - BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem - | _ -> - let v = Sem.eval integer_type_widths src mem in - Dom.Mem.update_mem elem_locs v mem + let fn = BufferOverrunField.cpp_vector_elem ~vec_typ:tgt_typ ~elt_typ:char_typ in + ArrObjCommon.constructor_from_char_ptr model_env tgt_deref src ~fn mem in let check ({location; integer_type_widths} as model_env) mem cond_set = Option.value_map len_opt ~default:cond_set ~f:(fun len -> @@ -730,13 +744,13 @@ module StdBasicString = struct (* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) - let constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src len = - constructor_from_char_ptr_common char_typ (tgt_exp, tgt_typ) src ~len_opt:(Some len) + let constructor_from_char_ptr_with_len char_typ (tgt_exp, tgt_typ) src len = + constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src ~len_opt:(Some len) (* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) let constructor_from_char_ptr_without_len char_typ (tgt_exp, tgt_typ) src = - constructor_from_char_ptr_common char_typ (tgt_exp, tgt_typ) src ~len_opt:None + constructor_from_char_ptr char_typ (tgt_exp, tgt_typ) src ~len_opt:None (* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *) @@ -1007,6 +1021,8 @@ module JavaString = struct (length, elem) + let get_length model_env exp mem = get_length_and_elem model_env exp mem |> fst + let concat exp1 exp2 = let exec ({pname; node_hash} as model_env) ~ret:(id, _) mem = let length_v, elem = @@ -1047,6 +1063,30 @@ module JavaString = struct model_by_value v ret_id mem in {exec; check= no_check} + + + let charAt string_exp idx = ArrObjCommon.at ~fn string_exp idx + + let constructor_from_char_ptr model_env tgt_deref src mem = + ArrObjCommon.constructor_from_char_ptr model_env tgt_deref ~fn src mem + + + (* https://docs.oracle.com/javase/7/docs/api/java/lang/String.html#String(byte[]) *) + let constructor tgt_exp src = + let exec model_env ~ret:_ mem = + constructor_from_char_ptr model_env (Sem.eval_locs tgt_exp mem) src mem + in + {exec; check= no_check} + + + (* https://docs.oracle.com/javase/7/docs/api/java/lang/String.html#String(java.lang.String) *) + let copy_constructor vec_exp src_exp = + let exec ({integer_type_widths} as model_env) ~ret:_ mem = + let vec_locs = Sem.eval integer_type_widths vec_exp mem |> Dom.Val.get_all_locs in + let deref_of_vec = PowLoc.append_field vec_locs ~fn in + ArrObjCommon.copy_constructor model_env deref_of_vec ~fn src_exp mem + in + {exec; check= no_check} end module Preconditions = struct @@ -1112,6 +1152,14 @@ module Call = struct ; -"memmove" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy ; -"memset" <>$ capt_exp $+ any_arg $+ capt_exp $!--> memset ; -"strcat" <>$ capt_exp $+ capt_exp $+...$--> strcat + ; +PatternMatch.implements_lang "String" + &:: "charAt" <>$ capt_exp $+ capt_exp $--> JavaString.charAt + ; +PatternMatch.implements_lang "String" + &:: "" <>$ capt_exp + $+ capt_exp_of_typ (+PatternMatch.implements_lang "String") + $--> JavaString.copy_constructor + ; +PatternMatch.implements_lang "String" + &:: "" <>$ capt_exp $+ capt_exp $--> JavaString.constructor ; +PatternMatch.implements_lang "String" &:: "concat" <>$ capt_exp $+ capt_exp $+...$--> JavaString.concat ; +PatternMatch.implements_lang "String" @@ -1150,7 +1198,7 @@ module Call = struct < capt_typ `T &+...>:: "basic_string" $ capt_arg $+ capt_exp_of_prim_typ char_ptr $+ capt_exp_of_prim_typ (Typ.mk (Typ.Tint Typ.size_t)) - $--> StdBasicString.constructor_from_char_ptr + $--> StdBasicString.constructor_from_char_ptr_with_len ; -"std" &:: "basic_string" < capt_typ `T &+...>:: "empty" $ capt_arg $--> StdBasicString.empty diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 3bb37d9fb..ae66e1109 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -168,14 +168,32 @@ module Exec = struct mem - let get_max_char s = String.fold s ~init:0 ~f:(fun acc c -> max acc (Char.to_int c)) + let get_min_max_char s ~init_char = + let init_i = Char.to_int init_char in + String.fold s ~init:(init_i, init_i) ~f:(fun (min_acc, max_acc) c -> + let i = Char.to_int c in + (min min_acc i, max max_acc i) ) + let decl_string {pname; node_hash; location; integer_type_widths} ~do_alloc locs s mem = let stride = Some (Typ.width_of_ikind integer_type_widths IChar / 8) in let offset = Itv.zero in - let size = Itv.of_int (String.length s + 1) in + let size = + let s_length = + if Language.curr_language_is Java then String.length s else String.length s + 1 + in + Itv.of_int s_length + in let traces = Trace.Set.singleton location Trace.ArrayDeclaration in - let char_itv = Itv.join Itv.zero (Itv.of_int (get_max_char s)) in + let char_itv = + let itv = + if Int.equal (String.length s) 0 then Itv.bot + else + let min, max = get_min_max_char s ~init_char:s.[0] in + Itv.join (Itv.of_int min) (Itv.of_int max) + in + if Language.curr_language_is Java then itv else Itv.join Itv.zero itv + in let decl loc mem = (* It doesn't allocate if the character pointer is in stack, because they are already allocated at the entry of the function. *) diff --git a/infer/src/checkers/costModels.ml b/infer/src/checkers/costModels.ml index cccd38312..8a1fa0187 100644 --- a/infer/src/checkers/costModels.ml +++ b/infer/src/checkers/costModels.ml @@ -52,8 +52,10 @@ let modeled ~of_function {pname; location} ~ret:(_, ret_typ) _ : BasicCost.t = (** Given a string of length n and an optional starting index i (0 by default), return itv [0, n_u-i_l] *) -let string_len_range_itv exp ~from mem = - let itv = BufferOverrunModels.eval_string_len exp mem |> BufferOverrunDomain.Val.get_itv in +let string_len_range_itv model_env exp ~from mem = + let itv = + BufferOverrunModels.JavaString.get_length model_env exp mem |> BufferOverrunDomain.Val.get_itv + in Option.value_map from ~default:itv ~f:(fun (start_exp, integer_type_widths) -> let start_itv = BufferOverrunSemantics.eval integer_type_widths start_exp mem @@ -90,7 +92,7 @@ module JavaString = struct let substring exp begin_idx model_env ~ret:_ inferbo_mem = substring_aux ~begin_idx - ~end_v:(BufferOverrunModels.eval_string_len exp inferbo_mem) + ~end_v:(BufferOverrunModels.JavaString.get_length model_env exp inferbo_mem) model_env inferbo_mem @@ -101,24 +103,29 @@ module JavaString = struct (** O(|m|) where m is the given string and |.| is the length function *) - let indexOf_char exp {location} ~ret:_ inferbo_mem = - let itv = string_len_range_itv exp ~from:None inferbo_mem in + let indexOf_char exp ({location} as model_env) ~ret:_ inferbo_mem = + let itv = string_len_range_itv model_env exp ~from:None inferbo_mem in of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location (** O(|m|-|n|) where m is the given string and n is the index to start searching from *) - let indexOf_char_starting_from exp start_exp {integer_type_widths; location} ~ret:_ inferbo_mem = - let itv = string_len_range_itv exp ~from:(Some (start_exp, integer_type_widths)) inferbo_mem in + let indexOf_char_starting_from exp start_exp ({integer_type_widths; location} as model_env) + ~ret:_ inferbo_mem = + let itv = + string_len_range_itv model_env exp ~from:(Some (start_exp, integer_type_widths)) inferbo_mem + in of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location (** O(|m|.|n|) where m and n are the given strings *) - let indexOf_str exp index_exp {location} ~ret:_ inferbo_mem = + let indexOf_str exp index_exp ({location} as model_env) ~ret:_ inferbo_mem = let itv = - BufferOverrunModels.eval_string_len exp inferbo_mem |> BufferOverrunDomain.Val.get_itv + BufferOverrunModels.JavaString.get_length model_env exp inferbo_mem + |> BufferOverrunDomain.Val.get_itv in let index_itv = - BufferOverrunModels.eval_string_len index_exp inferbo_mem |> BufferOverrunDomain.Val.get_itv + BufferOverrunModels.JavaString.get_length model_env index_exp inferbo_mem + |> BufferOverrunDomain.Val.get_itv in let n = of_itv ~itv ~degree_kind:Polynomials.DegreeKind.Linear ~of_function:"String.indexOf" location diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/StringTest.java b/infer/tests/codetoanalyze/java/bufferoverrun/StringTest.java new file mode 100644 index 000000000..31d16526e --- /dev/null +++ b/infer/tests/codetoanalyze/java/bufferoverrun/StringTest.java @@ -0,0 +1,39 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +class StringTest { + void constant_Good() { + String s = "hello"; + char c = s.charAt(4); + } + + void constant_Bad() { + String s = "hello"; + char c = s.charAt(5); + } + + void constant_explicit_constructor_Good() { + String s = new String("hello"); + char c = s.charAt(4); + } + + void constant_explicit_constructor_Bad() { + String s = new String("hello"); + char c = s.charAt(5); + } + + void copy_constructor_Good() { + String s = new String("hello"); + String t = new String(s); + char c = t.charAt(4); + } + + void copy_constructor_Bad() { + String s = new String("hello"); + String t = new String(s); + char c = t.charAt(5); + } +} diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 8300352a5..6226b4b5d 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -10,3 +10,6 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_nega codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this.buf[*]`,Assignment,,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10] codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `this.yy`,,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32] codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] +codetoanalyze/java/bufferoverrun/StringTest.java, StringTest.constant_Bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 5 Size: 5] +codetoanalyze/java/bufferoverrun/StringTest.java, StringTest.constant_explicit_constructor_Bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 5 Size: 5] +codetoanalyze/java/bufferoverrun/StringTest.java, StringTest.copy_constructor_Bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 5 Size: 5]