From 2531c75ceaa0291698432ae521ab4966741d1cc0 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 17 Dec 2018 03:11:17 -0800 Subject: [PATCH] [inferbo] Add literal string assignment Reviewed By: mbouaziz Differential Revision: D13335547 fbshipit-source-id: a1c6f6ced --- .../src/bufferoverrun/bufferOverrunChecker.ml | 5 ++++ infer/src/bufferoverrun/bufferOverrunUtils.ml | 24 +++++++++++++++++++ .../src/bufferoverrun/bufferOverrunUtils.mli | 10 ++++++++ .../codetoanalyze/c/bufferoverrun/arith.c | 5 ++++ .../c/bufferoverrun/array_content.c | 20 ++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 11 ++++++--- 6 files changed, 72 insertions(+), 3 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 147d9c930..51611b046 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -188,6 +188,11 @@ module TransferFunctions = struct Dom.Mem.add_unknown id ~location mem ) | Load (id, exp, _, _) -> BoUtils.Exec.load_locs id (Sem.eval_locs exp mem) mem + | Store (exp1, _, Const (Const.Cstr s), location) -> + let pname = Procdesc.get_proc_name pdesc in + let node_hash = CFG.Node.hash node in + let locs = Sem.eval_locs exp1 mem in + BoUtils.Exec.decl_string pname ~node_hash integer_type_widths location locs s mem | Store (exp1, _, exp2, location) -> let locs = Sem.eval_locs exp1 mem in let v = Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 5f1b47ff5..3a874c052 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -188,6 +188,30 @@ module Exec = struct mem ) | _ -> mem + + + 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 integer_type_widths location 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 + 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) + in + PowLoc.fold decl locs mem end module Check = struct diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 569fe110c..696bfc768 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -69,6 +69,16 @@ module Exec : sig -> Dom.Mem.t val set_dyn_length : Location.t -> Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t + + val decl_string : + Typ.Procname.t + -> node_hash:int + -> Typ.IntegerWidths.t + -> Location.t + -> PowLoc.t + -> string + -> Dom.Mem.t + -> Dom.Mem.t end module Check : sig diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index b903e4209..2d3f66864 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -518,6 +518,11 @@ void call_scan_hex_Good_FP() { scan_hex_Good(cp); } +void call_scan_hex2_Good_FP() { + char* cp = "0aA"; + scan_hex_Good(cp); +} + int check_addition_overflow_Good(unsigned int x, unsigned int y) { if (((unsigned int)-1) - x < y) { return 1; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c index e8ece35c7..4970e22b2 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c @@ -103,3 +103,23 @@ void weak_update_malloc2_Bad_FN() { x[0] = 0; a[x[1]] = 0; } + +void literal_string_Good() { + int a[1]; + char* s = "hello"; + for (int i = 0; i < 5; i++) { + if (s[i] > 'o') { + a[s[i]] = 0; + } + } +} + +void literal_string_bad() { + int a[1]; + char* s = "hello"; + for (int i = 0; i < 5; i++) { + if (s[i] > 'n') { + a[s[i]] = 0; + } + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index d8485fb8a..bd91a1ae7 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -3,9 +3,12 @@ codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2, codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Call,Assignment,Assignment,Assignment,,Array declaration,Array access: Offset: [0, 8] Size: 5] codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2] -codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,,Parameter `*cp`,Assignment,Binary operation: ([58, +oo] - 97):unsigned64 by call to `scan_hex_Good` ] -codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,,Parameter `*cp`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ] -codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,,Parameter `*cp`,Assignment,Binary operation: ([-oo, +oo] - 48):unsigned64 by call to `scan_hex_Good` ] +codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex2_Good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,,Parameter `*cp`,Array access: Offset: [0, +oo] Size: 4 by call to `scan_hex_Good` ] +codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex2_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,,Parameter `*cp`,Assignment,Binary operation: ([58, 97] - 87):unsigned64 by call to `scan_hex_Good` ] +codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex2_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,,Parameter `*cp`,Assignment,Binary operation: ([58, 97] - 97):unsigned64 by call to `scan_hex_Good` ] +codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex2_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,,Parameter `*cp`,Assignment,Binary operation: ([0, 97] - 48):unsigned64 by call to `scan_hex_Good` ] +codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,,Parameter `*cp`,Array access: Offset: [0, +oo] Size: 2 by call to `scan_hex_Good` ] +codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `*cp`,Assignment,Binary operation: (0 - 48):unsigned64 by call to `scan_hex_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,,Call,Assignment,Assignment,,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ] codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ] codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Parameter `n`,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 1] @@ -46,6 +49,8 @@ codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, C codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +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, strong_update_malloc_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, 15] Size: 10]