From a689301c530cf5bd43ef86c3c2dc23a2c83a8904 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 6 Dec 2018 05:42:47 -0800 Subject: [PATCH] [inferbo] eval_locs Summary: `eval_locs` is like `eval |> get_all_locs` but avoids computing things that aren't necessary. The goal was not to be an optimization but is needed for Java where array blocks don't have offsets. Reviewed By: skcho Differential Revision: D13190939 fbshipit-source-id: 1cc0e6338 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 19 +++++------- .../src/bufferoverrun/bufferOverrunModels.ml | 14 ++++----- .../bufferoverrun/bufferOverrunSemantics.ml | 29 +++++++++++++++++-- infer/src/bufferoverrun/bufferOverrunUtils.ml | 5 ++-- .../src/bufferoverrun/bufferOverrunUtils.mli | 2 ++ .../codetoanalyze/c/bufferoverrun/global.c | 14 +++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 2 ++ 7 files changed, 61 insertions(+), 24 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 4a112d4c1..da1615134 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -219,11 +219,10 @@ module TransferFunctions = struct |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val) - let instantiate_param tenv integer_type_widths pdesc params callee_exit_mem eval_sym_trace - location mem = + let instantiate_param tenv pdesc params callee_exit_mem eval_sym_trace location mem = let formals = Dom.get_formals pdesc in - let actuals = List.map ~f:(fun (a, _) -> Sem.eval integer_type_widths a mem) params in - let f mem formal actual = + let actuals_locs = List.map ~f:(fun (a, _) -> Sem.eval_locs a mem) params in + let f mem formal actual_locs = match (snd formal).Typ.desc with | Typ.Tptr (typ, _) -> ( match typ.Typ.desc with @@ -237,7 +236,7 @@ module TransferFunctions = struct let instantiate_fld mem (fn, _, _) = let formal_fields = PowLoc.append_field formal_locs ~fn in let v = Dom.Mem.find_set formal_fields callee_exit_mem in - let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) ~fn in + let actual_fields = PowLoc.append_field actual_locs ~fn in Dom.Val.subst v eval_sym_trace location |> Fn.flip (Dom.Mem.strong_update actual_fields) mem in @@ -250,13 +249,12 @@ module TransferFunctions = struct |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc in let v = Dom.Mem.find_set formal_locs callee_exit_mem in - let actual_locs = Dom.Val.get_all_locs actual in Dom.Val.subst v eval_sym_trace location |> Fn.flip (Dom.Mem.strong_update actual_locs) mem ) | _ -> mem in - try List.fold2_exn formals actuals ~init:mem ~f with Invalid_argument _ -> mem + try List.fold2_exn formals actuals_locs ~init:mem ~f with Invalid_argument _ -> mem let forget_ret_relation ret callee_pname mem = @@ -294,8 +292,7 @@ module TransferFunctions = struct in let caller_mem = instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace caller_mem location - |> instantiate_param tenv integer_type_widths callee_pdesc params callee_exit_mem - eval_sym_trace location + |> instantiate_param tenv callee_pdesc params callee_exit_mem eval_sym_trace location |> forget_ret_relation ret callee_pname in Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem @@ -329,9 +326,9 @@ module TransferFunctions = struct (Pvar.pp Pp.text) pvar ; Dom.Mem.add_unknown id ~location mem ) | Load (id, exp, _, _) -> - BoUtils.Exec.load_val id (Sem.eval integer_type_widths exp mem) mem + BoUtils.Exec.load_locs id (Sem.eval_locs exp mem) mem | Store (exp1, _, exp2, location) -> - let locs = Sem.eval integer_type_widths exp1 mem |> Dom.Val.get_all_locs in + 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 let mem = let sym_exps = diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index d355b2bf3..fb8fbb8f2 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -268,15 +268,11 @@ let set_array_length array length_exp = module Split = struct - let std_vector integer_type_widths ~adds_at_least_one (vector_exp, vector_typ) location mem = + let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem = let increment = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in let size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in - let vector_size_locs = - Sem.eval integer_type_widths vector_exp mem - |> Dom.Val.get_all_locs - |> PowLoc.append_field ~fn:size_field - in + let vector_size_locs = Sem.eval_locs vector_exp mem |> PowLoc.append_field ~fn:size_field in let f_trace _ traces = Trace.(Set.add_elem location Through) traces in Dom.Mem.transform_mem ~f:(Dom.Val.plus_a ~f_trace increment) vector_size_locs mem end @@ -284,8 +280,8 @@ end module Boost = struct module Split = struct let std_vector vector_arg = - let exec {location; integer_type_widths} ~ret:_ mem = - Split.std_vector integer_type_widths ~adds_at_least_one:true vector_arg location mem + let exec {location} ~ret:_ mem = + Split.std_vector ~adds_at_least_one:true vector_arg location mem in {exec; check= no_check} end @@ -303,7 +299,7 @@ module Folly = struct (* default: ignore_empty is false *) true in - Split.std_vector integer_type_widths ~adds_at_least_one vector_arg location mem + Split.std_vector ~adds_at_least_one vector_arg location mem in {exec; check= no_check} end diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 1ec530dce..0db7c551a 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -266,6 +266,31 @@ and eval_binop : Typ.IntegerWidths.t -> Binop.t -> Exp.t -> Exp.t -> Mem.t -> Va Val.lor_sem v1 v2 +(** + [eval_locs exp mem] is like [eval_locs exp mem |> Val.get_all_locs] + but takes some shortcuts to avoid computing useless and/or problematic intermediate values +*) +let rec eval_locs : Exp.t -> Mem.t -> PowLoc.t = + fun exp mem -> + match exp with + | Var id -> + Mem.find_stack (Var.of_id id |> Loc.of_var) mem |> Val.get_all_locs + | Lvar pvar -> + let loc = Loc.of_pvar pvar in + if Mem.is_stack_loc loc mem then Mem.find loc mem |> Val.get_all_locs + else PowLoc.singleton loc + | BinOp ((Binop.MinusPI | Binop.PlusPI), e, _) | Cast (_, e) -> + eval_locs e mem + | BinOp _ | Closure _ | Const _ | Exn _ | Sizeof _ | UnOp _ -> + PowLoc.empty + | Lfield (e, fn, _) -> + eval_locs e mem |> PowLoc.append_field ~fn + | Lindex (((Lfield _ | Lindex _) as e), _) -> + Mem.find_set (eval_locs e mem) mem |> Val.get_all_locs + | Lindex (e, _) -> + eval_locs e mem + + (* It returns the array value of the input expression. For example, when "x" is a program variable, (eval_arr "x") returns array blocks the "x" is pointing to, on the other hand, (eval "x") returns the @@ -287,10 +312,10 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t = let v = eval_arr integer_type_widths e mem in set_array_stride integer_type_widths t v | Exp.Lfield (e, fn, _) -> - let locs = eval integer_type_widths e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in + let locs = eval_locs e mem |> PowLoc.append_field ~fn in Mem.find_set locs mem | Exp.Lindex (e, _) -> - let locs = eval integer_type_widths e mem |> Val.get_all_locs in + let locs = eval_locs e mem in Mem.find_set locs mem | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ -> Val.bot diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 9e092c572..78165ef25 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -22,8 +22,7 @@ module Exec = struct Dom.Mem.find_set size_powloc mem - let load_val id val_ mem = - let locs = val_ |> Dom.Val.get_all_locs in + let load_locs id locs mem = let v = Dom.Mem.find_set locs mem in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in if not v.represents_multiple_values then @@ -35,6 +34,8 @@ module Exec = struct else mem + let load_val id v mem = load_locs id (Dom.Val.get_all_locs v) mem + type decl_local = Typ.Procname.t -> node_hash:int diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index fcf515e70..b421302d7 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -14,6 +14,8 @@ module PO = BufferOverrunProofObligations module Exec : sig val get_alist_size : Dom.Val.t -> Dom.Mem.t -> Dom.Val.t + val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t + val load_val : Ident.t -> Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t type decl_local = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/global.c b/infer/tests/codetoanalyze/c/bufferoverrun/global.c index b0317757c..3a8b7f813 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/global.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/global.c @@ -39,3 +39,17 @@ void use_global_const_ten_Bad() { char arr[5]; arr[global_const_ten] = 0; } + +static const char global_arr[] = {1, 0, 1}; + +static void copyfilter_Good_FP(const char* s, const char* z, int b) { + int i; + int n = strlen(s); + for (i = 0; z[i]; i++) { // We need to infer that z[i] means i < strlen(z) + if (global_arr[z[i]] || // We need a weak update here + (z[i] == s[0] && (n == 1 || memcmp(z, s, n) == 0))) { + i = 0; + break; + } + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index ddc423d38..ef718c513 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -89,6 +89,8 @@ codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OV codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/global.c, copyfilter_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/c/bufferoverrun/global.c, copyfilter_Good_FP, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]