From 0d07a240eacc6f84a1a2817aa4e7121504d3d244 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 22 Jan 2019 17:48:15 -0800 Subject: [PATCH] [inferbo] Literal string on stack location Summary: It adds semantics of assignment of literal string to stack locations, e.g., `char s[] = "hello";`. Depends on D13668414 Reviewed By: ezgicicek, mbouaziz Differential Revision: D13668505 fbshipit-source-id: 72caf35c3 --- infer/src/bufferoverrun/absLoc.ml | 2 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 3 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 20 +++++------ .../src/bufferoverrun/bufferOverrunModels.ml | 5 +-- .../bufferoverrun/bufferOverrunSemantics.ml | 13 +++++++ infer/src/bufferoverrun/bufferOverrunUtils.ml | 35 ++++++++++++------- .../src/bufferoverrun/bufferOverrunUtils.mli | 3 +- .../c/bufferoverrun/array_content.c | 2 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 2 ++ 9 files changed, 55 insertions(+), 30 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 6a5d03817..78f5e3ba9 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -182,7 +182,7 @@ module Loc = struct let of_allocsite a = Allocsite a - let of_c_strlen a = Field (of_allocsite a, BufferOverrunField.c_strlen) + let of_c_strlen loc = Field (loc, BufferOverrunField.c_strlen) let of_pvar pvar = Var (Var.of_pvar pvar) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a27c8ed12..64420f8be 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -176,7 +176,8 @@ module TransferFunctions = struct let node_hash = CFG.Node.hash node in BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths in - BoUtils.Exec.decl_string model_env locs s mem + let do_alloc = not (Sem.is_stack_exp exp1 mem) in + BoUtils.Exec.decl_string model_env ~do_alloc locs s mem | Store (exp1, typ, exp2, location) -> let locs = Sem.eval_locs exp1 mem in let v = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 609248fb2..f0888a28d 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -1183,19 +1183,19 @@ module MemReach = struct (* unsound *) - let set_first_idx_of_null : Allocsite.t -> Val.t -> t -> t = - fun allocsite idx m -> update_mem (PowLoc.singleton (Loc.of_c_strlen allocsite)) idx m + let set_first_idx_of_null : Loc.t -> Val.t -> t -> t = + fun loc idx m -> update_mem (PowLoc.singleton (Loc.of_c_strlen loc)) idx m (* unsound *) - let unset_first_idx_of_null : Allocsite.t -> Val.t -> t -> t = - fun allocsite idx m -> - let old_c_strlen = find_heap (Loc.of_c_strlen allocsite) m in + let unset_first_idx_of_null : Loc.t -> Val.t -> t -> t = + fun loc idx m -> + let old_c_strlen = find_heap (Loc.of_c_strlen loc) m in let idx_itv = Val.get_itv idx in if Boolean.is_true (Itv.lt_sem idx_itv (Val.get_itv old_c_strlen)) then m else let new_c_strlen = Val.of_itv ~traces:(Val.get_traces idx) (Itv.incr idx_itv) in - set_first_idx_of_null allocsite new_c_strlen m + set_first_idx_of_null loc new_c_strlen m end module Mem = struct @@ -1349,15 +1349,13 @@ module Mem = struct let unset_oenv = map ~f:MemReach.unset_oenv - let set_first_idx_of_null allocsite idx = map ~f:(MemReach.set_first_idx_of_null allocsite idx) - - let unset_first_idx_of_null allocsite idx = - map ~f:(MemReach.unset_first_idx_of_null allocsite idx) + let set_first_idx_of_null loc idx = map ~f:(MemReach.set_first_idx_of_null loc idx) + let unset_first_idx_of_null loc idx = map ~f:(MemReach.unset_first_idx_of_null loc idx) let get_c_strlen locs m = let get_c_strlen' loc acc = - match loc with Loc.Allocsite a -> Val.join acc (find (Loc.of_c_strlen a) m) | _ -> acc + match loc with Loc.Allocsite _ -> Val.join acc (find (Loc.of_c_strlen loc) m) | _ -> acc in PowLoc.fold get_c_strlen' locs Val.bot end diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 9f2ebc9bc..d17ca499e 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -75,7 +75,8 @@ let fgets str_exp num_exp = let num = Dom.Val.get_itv num_v in Itv.plus offset (Itv.set_lb_zero (Itv.decr num)) in - Dom.Mem.set_first_idx_of_null allocsite (Dom.Val.of_itv ~traces strlen) acc + Dom.Mem.set_first_idx_of_null (Loc.of_allocsite allocsite) (Dom.Val.of_itv ~traces strlen) + acc in mem |> Dom.Mem.update_mem (Sem.eval_locs str_exp mem) Dom.Val.Itv.zero_255 @@ -383,7 +384,7 @@ module StdBasicString = struct match src with | Exp.Const (Const.Cstr s) -> let locs = Sem.eval_locs tgt mem in - BoUtils.Exec.decl_string model_env locs s mem + BoUtils.Exec.decl_string model_env ~do_alloc:true locs s mem | _ -> let tgt_locs = Sem.eval_locs tgt mem in let v = Sem.eval integer_type_widths src mem in diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index f5628824d..21f9e6577 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -324,6 +324,19 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t = Val.bot +let rec is_stack_exp : Exp.t -> Mem.t -> bool = + fun exp mem -> + match exp with + | Var _ -> + true + | Lvar pvar -> + Mem.is_stack_loc (Loc.of_pvar pvar) mem + | Cast (_, e) -> + is_stack_exp e mem + | _ -> + false + + module ParamBindings = struct include PrettyPrintable.MakePPMap (struct include Pvar diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index ea78e25e5..865ed36f7 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -169,25 +169,33 @@ module Exec = struct let get_max_char s = String.fold s ~init:0 ~f:(fun acc c -> max acc (Char.to_int c)) - let decl_string {pname; node_hash; location; integer_type_widths} locs s mem = + 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 traces = Trace.Set.singleton location Trace.ArrayDeclaration in let char_itv = Itv.join Itv.zero (Itv.of_int (get_max_char s)) in let decl loc mem = - let allocsite = - let deref_kind = Symb.SymbolPath.Deref_ArrayIndex in - let path = Loc.get_path loc in - let deref_path = Option.map ~f:(fun path -> Symb.SymbolPath.deref ~deref_kind path) path in - Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:deref_path - ~represents_multiple_values:true + (* It doesn't allocate if the character pointer is in stack, because they are already + allocated at the entry of the function. *) + let deref_loc, mem = + if do_alloc then + let allocsite = + let deref_kind = Symb.SymbolPath.Deref_ArrayIndex in + let path = Loc.get_path loc in + let deref_path = + Option.map ~f:(fun path -> Symb.SymbolPath.deref ~deref_kind path) path + in + Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:deref_path + ~represents_multiple_values:true + in + let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in + (Loc.of_allocsite allocsite, Dom.Mem.update_mem (PowLoc.singleton loc) v mem) + else (loc, mem) in - let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in mem - |> Dom.Mem.update_mem (PowLoc.singleton loc) v - |> Dom.Mem.add_heap (Loc.of_allocsite allocsite) (Dom.Val.of_itv char_itv) - |> Dom.Mem.set_first_idx_of_null allocsite + |> Dom.Mem.add_heap deref_loc (Dom.Val.of_itv char_itv) + |> Dom.Mem.set_first_idx_of_null deref_loc (Dom.Val.of_itv ~traces (Itv.of_int (String.length s))) in PowLoc.fold decl locs mem @@ -197,9 +205,10 @@ module Exec = struct let traces = TraceSet.join (Dom.Val.get_traces tgt) (Dom.Val.get_traces src) in let src_itv = Dom.Val.get_itv src in let set_c_strlen1 allocsite arrinfo acc = + let loc = Loc.of_allocsite allocsite in let idx = Dom.Val.of_itv ~traces (ArrayBlk.ArrInfo.offsetof arrinfo) in - if Itv.( <= ) ~lhs:Itv.zero ~rhs:src_itv then Dom.Mem.set_first_idx_of_null allocsite idx acc - else Dom.Mem.unset_first_idx_of_null allocsite idx acc + if Itv.( <= ) ~lhs:Itv.zero ~rhs:src_itv then Dom.Mem.set_first_idx_of_null loc idx acc + else Dom.Mem.unset_first_idx_of_null loc idx acc in ArrayBlk.fold set_c_strlen1 (Dom.Val.get_array_blk tgt) mem end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 7fde0affa..715f706b3 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -41,7 +41,8 @@ module Exec : sig val set_dyn_length : ModelEnv.model_env -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t - val decl_string : ModelEnv.model_env -> PowLoc.t -> string -> Dom.Mem.t -> Dom.Mem.t + val decl_string : + ModelEnv.model_env -> do_alloc:bool -> PowLoc.t -> string -> Dom.Mem.t -> Dom.Mem.t val set_c_strlen : tgt:Dom.Val.t -> src:Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t end diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c index 0abecb03f..980fe874a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c @@ -135,7 +135,7 @@ void literal_string2_Good() { } } -void literal_string2_Bad_FN() { +void literal_string2_bad() { int a[1]; char s[] = "hello"; for (int i = 0; i < 5; i++) { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index f282a7304..5d6acc2d3 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -58,6 +58,8 @@ codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, BUFFER_O codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Array declaration,Binary operation: ([0, 99] - 2):unsigned64] codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: [-1, 98] Size: 100] codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Good_FP, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [,Array declaration,Binary operation: ([0, 99] - 1):unsigned64] +codetoanalyze/c/bufferoverrun/array_content.c, literal_string2_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/array_content.c, literal_string2_bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Array access: Offset: [0, 111] Size: 1] codetoanalyze/c/bufferoverrun/array_content.c, literal_string_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, literal_string_bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Array access: Offset: [0, 111] Size: 1] codetoanalyze/c/bufferoverrun/array_content.c, strlen_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: 5 Size: 5]