From 6bde9bda8849325d578b457912c077cc9d557c76 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Mon, 13 Jul 2015 07:53:10 -0200 Subject: [PATCH] [Bucketing] Improve error bucketing by using constant propagation when detecting direct null assignments. --- infer/src/backend/buckets.ml | 13 +- infer/src/backend/interproc.ml | 5 +- infer/src/backend/prop.ml | 14 +- infer/src/backend/prover.ml | 33 ++--- infer/src/backend/sil.ml | 6 + infer/src/backend/sil.mli | 3 + infer/src/backend/state.ml | 12 ++ infer/src/backend/state.mli | 8 + infer/src/backend/symExec.ml | 52 +++---- infer/src/checkers/constantPropagation.ml | 164 +++++++++++---------- infer/src/checkers/constantPropagation.mli | 7 +- infer/src/checkers/sqlChecker.ml | 40 +++-- 12 files changed, 194 insertions(+), 163 deletions(-) diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml index a8268f418..a415f10dc 100644 --- a/infer/src/backend/buckets.ml +++ b/infer/src/backend/buckets.ml @@ -61,9 +61,17 @@ let check_access access_opt de_opt = !formal_ids in let formal_param_used_in_call = ref false in let has_call_or_sets_null node = - let rec exp_is_null = function + let rec exp_is_null exp = match exp with | Sil.Const (Sil.Cint n) -> Sil.Int.iszero n | Sil.Cast (_, e) -> exp_is_null e + | Sil.Var _ + | Sil.Lvar _ -> + begin + match State.get_const_map () node exp with + | Some (Sil.Cint n) -> + Sil.Int.iszero n + | _ -> false + end | _ -> false in let filter = function | Sil.Call (_, _, etl, _, _) -> @@ -73,7 +81,8 @@ let check_access access_opt de_opt = | _ -> false in if list_exists arg_is_formal_param etl then formal_param_used_in_call := true; true - | Sil.Set (_, _, e, _) -> exp_is_null e + | Sil.Set (_, _, e, _) -> + exp_is_null e | _ -> false in list_exists filter (Cfg.Node.get_instrs node) in let local_access_found = ref false in diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 8dc99c809..e99c95fe5 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -467,11 +467,12 @@ let check_assignement_guard node = (** Perform symbolic execution for a node starting from an initial prop *) let do_symbolic_execution handle_exn cfg tenv (node : Cfg.node) (prop: Prop.normal Prop.t) (path : Paths.Path.t) = + let pdesc = Cfg.Node.get_proc_desc node in State.mark_execution_start node; + State.set_const_map (ConstantPropagation.build_const_map pdesc); (* build the const map lazily *) check_assignement_guard node; let instrs = Cfg.Node.get_instrs node in Ident.update_name_generator (instrs_get_normal_vars instrs); (* fresh normal vars must be fresh w.r.t. instructions *) - let pdesc = Cfg.Node.get_proc_desc node in let pset = SymExec.lifted_sym_exec handle_exn cfg tenv pdesc (Paths.PathSet.from_renamed_list [(prop, path)]) node instrs in @@ -698,7 +699,7 @@ let collect_postconditions tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t = let create_seed_vars sigma = let hpred_add_seed sigma = function | Sil.Hpointsto (Sil.Lvar pv, se, typ) when not (Sil.pvar_is_abducted pv) -> - Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: sigma + Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: sigma | _ -> sigma in list_fold_left hpred_add_seed [] sigma diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 595fe4a84..4c68b6847 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -2772,23 +2772,19 @@ end = struct let pi_size pi = pi_weight * list_length pi - module ExpMap = - Map.Make (struct - type t = Sil.exp - let compare = Sil.exp_compare end) (** Approximate the size of the longest chain by counting the max number of |-> with the same type and whose lhs is primed or footprint *) let sigma_chain_size sigma = - let tbl = ref ExpMap.empty in + let tbl = ref Sil.ExpMap.empty in let add t = try - let count = ExpMap.find t !tbl in - tbl := ExpMap.add t (count + 1) !tbl + let count = Sil.ExpMap.find t !tbl in + tbl := Sil.ExpMap.add t (count + 1) !tbl with | Not_found -> - tbl := ExpMap.add t 1 !tbl in + tbl := Sil.ExpMap.add t 1 !tbl in let process_hpred = function | Sil.Hpointsto (e, _, te) -> (match e with @@ -2797,7 +2793,7 @@ end = struct | Sil.Hlseg _ | Sil.Hdllseg _ -> () in list_iter process_hpred sigma; let size = ref 0 in - ExpMap.iter (fun t n -> size := max n !size) !tbl; + Sil.ExpMap.iter (fun t n -> size := max n !size) !tbl; !size (** Compute a size value for the prop, which indicates its diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index d3c17b709..97b533a6e 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -233,11 +233,6 @@ module Inequalities : sig val d_neqs : t -> unit end = struct - module ExpMap = - Map.Make (struct - type t = Sil.exp - let compare = Sil.exp_compare end) - type t = { mutable leqs: (Sil.exp * Sil.exp) list; (** le fasts [e1 <= e2] *) mutable lts: (Sil.exp * Sil.exp) list; (** lt facts [e1 < e2] *) @@ -281,14 +276,14 @@ end = struct else begin let umap_add umap e new_upper = try - let old_upper = ExpMap.find e umap in - if Sil.Int.leq old_upper new_upper then umap else ExpMap.add e new_upper umap - with Not_found -> ExpMap.add e new_upper umap in + let old_upper = Sil.ExpMap.find e umap in + if Sil.Int.leq old_upper new_upper then umap else Sil.ExpMap.add e new_upper umap + with Not_found -> Sil.ExpMap.add e new_upper umap in let lmap_add lmap e new_lower = try - let old_lower = ExpMap.find e lmap in - if Sil.Int.geq old_lower new_lower then lmap else ExpMap.add e new_lower lmap - with Not_found -> ExpMap.add e new_lower lmap in + let old_lower = Sil.ExpMap.find e lmap in + if Sil.Int.geq old_lower new_lower then lmap else Sil.ExpMap.add e new_lower lmap + with Not_found -> Sil.ExpMap.add e new_lower lmap in let rec umap_create_from_leqs umap = function | [] -> umap | (e1, Sil.Const (Sil.Cint upper1)):: leqs_rest -> @@ -306,7 +301,7 @@ end = struct | constr:: constrs_rest -> try let e1, e2, n = DiffConstr.to_triple constr (* e1 - e2 <= n *) in - let upper2 = ExpMap.find e2 umap in + let upper2 = Sil.ExpMap.find e2 umap in let new_upper1 = upper2 ++ n in let new_umap = umap_add umap e1 new_upper1 in umap_improve_by_difference_constraints new_umap constrs_rest @@ -317,22 +312,26 @@ end = struct | constr:: constrs_rest -> (* e2 - e1 > -n-1 *) try let e1, e2, n = DiffConstr.to_triple constr (* e2 - e1 > -n-1 *) in - let lower1 = ExpMap.find e1 lmap in + let lower1 = Sil.ExpMap.find e1 lmap in let new_lower2 = lower1 -- n -- Sil.Int.one in let new_lmap = lmap_add lmap e2 new_lower2 in lmap_improve_by_difference_constraints new_lmap constrs_rest with Not_found -> lmap_improve_by_difference_constraints lmap constrs_rest in let leqs_res = - let umap = umap_create_from_leqs ExpMap.empty leqs in + let umap = umap_create_from_leqs Sil.ExpMap.empty leqs in let umap' = umap_improve_by_difference_constraints umap diff_constraints2 in - let leqs' = ExpMap.fold (fun e upper acc_leqs -> (e, Sil.exp_int upper):: acc_leqs) umap' [] in + let leqs' = Sil.ExpMap.fold + (fun e upper acc_leqs -> (e, Sil.exp_int upper):: acc_leqs) + umap' [] in let leqs'' = (list_map DiffConstr.to_leq diff_constraints2) @ leqs' in leqs_sort_then_remove_redundancy leqs'' in let lts_res = - let lmap = lmap_create_from_lts ExpMap.empty lts in + let lmap = lmap_create_from_lts Sil.ExpMap.empty lts in let lmap' = lmap_improve_by_difference_constraints lmap diff_constraints2 in - let lts' = ExpMap.fold (fun e lower acc_lts -> (Sil.exp_int lower, e):: acc_lts) lmap' [] in + let lts' = Sil.ExpMap.fold + (fun e lower acc_lts -> (Sil.exp_int lower, e):: acc_lts) + lmap' [] in let lts'' = (list_map DiffConstr.to_lt diff_constraints2) @ lts' in lts_sort_then_remove_redundancy lts'' in { leqs = leqs_res; lts = lts_res; neqs = neqs } diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index 03b4b2520..e7c1f1843 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -1658,6 +1658,12 @@ module ExpSet = Set.Make let compare = exp_compare end) +module ExpMap = Map.Make(struct + type t = exp + let compare = exp_compare + end) + + let elist_to_eset es = list_fold_left (fun set e -> ExpSet.add e set) ExpSet.empty es diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index 5ea87cfc9..3c8b49a2e 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -349,6 +349,9 @@ module TypMap : Map.S with type key = typ (** Sets of expressions. *) module ExpSet : Set.S with type elt = exp +(** Maps with expression keys. *) +module ExpMap : Map.S with type key = exp + (** Hashtable with expressions as keys. *) module ExpHash : Hashtbl.S with type key = exp diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index 4f5738411..4aef27f13 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -10,6 +10,12 @@ module L = Logging module F = Format open Utils +type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option + +(** Constant map for the procedure *) +let const_map : const_map ref = + ref (fun node exp -> None) + (** Diverging states since the last reset for the node *) let diverging_states_node = ref Paths.PathSet.empty @@ -318,3 +324,9 @@ let set_node (node: Cfg.node) = let set_session (session: int) = last_session := session + +let get_const_map () = + !const_map + +let set_const_map const_map' = + const_map := const_map' diff --git a/infer/src/backend/state.mli b/infer/src/backend/state.mli index 36efdb5c4..eb9945230 100644 --- a/infer/src/backend/state.mli +++ b/infer/src/backend/state.mli @@ -11,6 +11,11 @@ open Utils (** Add diverging states *) val add_diverging_states : Paths.PathSet.t -> unit +type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option + +(** Get the constant map for the current procedure. *) +val get_const_map : unit -> const_map + (** Get the diverging states for the node *) val get_diverging_states_node : unit -> Paths.PathSet.t @@ -93,6 +98,9 @@ val reset : unit -> unit (** Reset the diverging states and goto information for the node *) val reset_diverging_states_goto_node : unit -> unit +(** Set the constant map for the current procedure. *) +val set_const_map : const_map -> unit + (** Set the node target of a Sil.Goto_node instruction *) val set_goto_node : int -> unit diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 1ded6c53f..3792476ed 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -939,7 +939,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path let sym_exe_builtin = Builtin.get_sym_exe_builtin fn in sym_exe_builtin cfg pdesc instr tenv _prop path ret_ids args fn loc | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_param, loc, call_flags) -> - (** Generic fun call with known name *) + (** Generic fun call with known name *) let (prop_r, _n_actual_params) = normalize_params pdesc _prop actual_param in let fn, n_actual_params = handle_special_cases_call tenv cfg callee_pname _n_actual_params in let resolved_pname = @@ -955,13 +955,13 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path Reporting.log_info pname exn; L.d_strln ("Undefined function " ^ Procname.to_string callee_pname - ^ ", returning undefined value."); + ^ ", returning undefined value."); (match Specs.get_summary pname with - | None -> () - | Some summary -> - Specs.CallStats.trace - summary.Specs.stats.Specs.call_stats callee_pname loc - (Specs.CallStats.CR_skip) !Config.footprint); + | None -> () + | Some summary -> + Specs.CallStats.trace + summary.Specs.stats.Specs.call_stats callee_pname loc + (Specs.CallStats.CR_skip) !Config.footprint); call_unknown_or_scan false cfg pdesc tenv prop_r path ret_ids ret_typ_opt n_actual_params resolved_pname loc in @@ -969,10 +969,10 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path match Specs.get_summary resolved_pname with | None -> skip_call () | Some summary when call_should_be_skipped resolved_pname summary -> - skip_call () + skip_call () | Some summary -> - sym_exec_call - cfg pdesc tenv prop_r path ret_ids n_actual_params summary loc + sym_exec_call + cfg pdesc tenv prop_r path ret_ids n_actual_params summary loc end | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (** Call via function pointer *) let (prop_r, n_actual_params) = normalize_params pdesc _prop actual_params in @@ -1192,7 +1192,7 @@ and call_unknown_or_scan is_scan cfg pdesc tenv pre path let do_exp p (e, t) = let do_attribute q = function | Sil.Aresource res_action as res - when res_action.Sil.ra_res = Sil.Rfile -> + when res_action.Sil.ra_res = Sil.Rfile -> Prop.remove_attribute res q | _ -> q in list_fold_left do_attribute p (Prop.get_exp_attributes p e) in @@ -1229,26 +1229,26 @@ and sym_exe_check_variadic_sentinel cfg pdesc tenv prop path actual_params fails (* sentinels start counting from the last argument to the function *) let n = nargs - sentinel - 1 in let build_argsi (acc, i) a = - if i = n then (acc, i+1) - else ((a,i)::acc, i+1) in + if i = n then (acc, i +1) + else ((a, i):: acc, i +1) in (* list_fold_left reverses the arguments *) let non_terminal_actuals_i = fst (list_fold_left build_argsi ([], 0) args) in let check_allocated result ((lexp, typ), i) = - (* simulate a Letderef for [lexp] *) + (* simulate a Letderef for [lexp] *) let tmp_id_deref = Ident.create_fresh Ident.kprimed in let letderef = Sil.Letderef (tmp_id_deref, lexp, typ, loc) in try sym_exec_generated false cfg tenv pdesc [letderef] result with e when exn_not_timeout e -> - if not fails_on_nil then - let deref_str = Localise.deref_str_nil_argument_in_variadic_method pname nargs i in - let err_desc = - Errdesc.explain_dereference ~use_buckets: true ~is_premature_nil: true - deref_str prop loc in - raise (Exceptions.Premature_nil_termination - (err_desc, try assert false with Assert_failure x -> x)) - else - raise e in + if not fails_on_nil then + let deref_str = Localise.deref_str_nil_argument_in_variadic_method pname nargs i in + let err_desc = + Errdesc.explain_dereference ~use_buckets: true ~is_premature_nil: true + deref_str prop loc in + raise (Exceptions.Premature_nil_termination + (err_desc, try assert false with Assert_failure x -> x)) + else + raise e in (* list_fold_left reverses the arguments back so that we report an *) (* error on the first premature nil argument *) list_fold_left check_allocated [(prop, path)] non_terminal_actuals_i @@ -1374,7 +1374,7 @@ and sym_exec_wrapper handle_exn cfg tenv pdesc instr ((prop: Prop.normal Prop.t) let lifted_sym_exec handle_exn cfg tenv pdesc (pset : Paths.PathSet.t) node (instrs : Sil.instr list) - : Paths.PathSet.t = +: Paths.PathSet.t = let pname = Cfg.Procdesc.get_proc_name pdesc in let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) = let pset2 = @@ -2088,8 +2088,8 @@ module ModelBuiltins = struct match Specs.get_summary (Procname.from_string fun_string) with | None -> assert false | Some callee_summary -> - sym_exec_call - cfg pdesc tenv prop path ret_ids [(routine_arg, snd arg)] callee_summary loc + sym_exec_call + cfg pdesc tenv prop path ret_ids [(routine_arg, snd arg)] callee_summary loc end | _ -> L.d_str "pthread_create: unknown function "; Sil.d_exp routine_name; L.d_strln ", skipping call."; diff --git a/infer/src/checkers/constantPropagation.ml b/infer/src/checkers/constantPropagation.ml index 11936b932..1807956ec 100644 --- a/infer/src/checkers/constantPropagation.ml +++ b/infer/src/checkers/constantPropagation.ml @@ -8,10 +8,6 @@ module L = Logging type t -module ConstantMap = Map.Make(struct - type t = string - let compare = string_compare -end) let string_widening_limit = 1000 let verbose = false @@ -24,85 +20,81 @@ let merge_values key c1_opt c2_opt = | None, Some c -> Some c | _ -> Some None +module ConstantMap = Sil.ExpMap + (** Dataflow struct *) module ConstantFlow = Dataflow.MakeDF(struct - type t = (Sil.const option) ConstantMap.t - - let pp fmt constants = - let print_kv k = function - | Some v -> Format.fprintf fmt " %s -> %a@." k (Sil.pp_const pe_text) v - | _ -> Format.fprintf fmt " %s -> None@." k in - Format.fprintf fmt "[@."; - ConstantMap.iter print_kv constants; - Format.fprintf fmt "]@." - - (* Item-wise equality where values are equal iff + type t = (Sil.const option) ConstantMap.t + + let pp fmt constants = + let pp_key fmt = Sil.pp_exp pe_text fmt in + let print_kv k = function + | Some v -> Format.fprintf fmt " %a -> %a@." pp_key k (Sil.pp_const pe_text) v + | _ -> Format.fprintf fmt " %a -> None@." pp_key k in + Format.fprintf fmt "[@."; + ConstantMap.iter print_kv constants; + Format.fprintf fmt "]@." + + (* Item - wise equality where values are equal iff - both are None - both are a constant and equal wrt. Sil.const_equal *) - let equal m n = ConstantMap.equal (opt_equal Sil.const_equal) m n - - let join = ConstantMap.merge merge_values - - let proc_throws pn = Dataflow.DontKnow - - let do_node node constants = - - let do_instr constants instr = - try - let update key value constants = - ConstantMap.merge - merge_values - constants - (ConstantMap.add key value ConstantMap.empty) in - - match instr with - | Sil.Letderef (i, Sil.Lvar p, _, _) -> (* tmp = var *) - let lvar = Ident.to_string i in - let rvar = Sil.pvar_to_string p in - update lvar (ConstantMap.find rvar constants) constants - - | Sil.Set (Sil.Lvar p, _, Sil.Const c, _) -> (* var = const *) - update (Sil.pvar_to_string p) (Some c) constants - - | Sil.Set (Sil.Lvar p, _, Sil.Var i, _) -> (* var = tmp *) - let lvar = Sil.pvar_to_string p in - let rvar = Ident.to_string i in - update lvar (ConstantMap.find rvar constants) constants - - (* Handle propagation of string with StringBuilder. Does not handle null case *) - | Sil.Call (_, Sil.Const (Sil.Cfun pn), (Sil.Var sb, _):: [], _, _) - when Procname.java_get_class pn = "java.lang.StringBuilder" - && Procname.java_get_method pn = "" -> (* StringBuilder. *) - update (Ident.to_string sb) (Some (Sil.Cstr "")) constants - - | Sil.Call (i:: [], Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: [], _, _) - when Procname.java_get_class pn = "java.lang.StringBuilder" - && Procname.java_get_method pn = "toString" -> (* StringBuilder.toString *) - let lvar = Ident.to_string i in - let rvar = Ident.to_string i1 in - update lvar (ConstantMap.find rvar constants) constants - - | Sil.Call (i:: [], Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], _, _) - when Procname.java_get_class pn = "java.lang.StringBuilder" - && Procname.java_get_method pn = "append" -> (* StringBuilder.append *) - let lvar = Ident.to_string i in - let rvar1 = Ident.to_string i1 in - let rvar2 = Ident.to_string i2 in - (match ConstantMap.find rvar1 constants, ConstantMap.find rvar2 constants with - | Some (Sil.Cstr s1), Some (Sil.Cstr s2) -> - begin - let s = s1 ^ s2 in - let u = - if String.length s < string_widening_limit then - Some (Sil.Cstr s) - else - None in - update lvar u constants - end - | _ -> constants) - - | _ -> constants - with Not_found -> constants in + let equal m n = ConstantMap.equal (opt_equal Sil.const_equal) m n + + let join = ConstantMap.merge merge_values + + let proc_throws pn = Dataflow.DontKnow + + let do_node node constants = + + let do_instr constants instr = + try + let update key value constants = + ConstantMap.merge + merge_values + constants + (ConstantMap.add key value ConstantMap.empty) in + + match instr with + | Sil.Letderef (i, Sil.Lvar p, _, _) -> (* tmp = var *) + update (Sil.Var i) (ConstantMap.find (Sil.Lvar p) constants) constants + + | Sil.Set (Sil.Lvar p, _, Sil.Const c, _) -> (* var = const *) + update (Sil.Lvar p) (Some c) constants + + | Sil.Set (Sil.Lvar p, _, Sil.Var i, _) -> (* var = tmp *) + update (Sil.Lvar p) (ConstantMap.find (Sil.Var i) constants) constants + + (* Handle propagation of string with StringBuilder. Does not handle null case *) + | Sil.Call (_, Sil.Const (Sil.Cfun pn), (Sil.Var sb, _):: [], _, _) + when Procname.java_get_class pn = "java.lang.StringBuilder" + && Procname.java_get_method pn = "" -> (* StringBuilder. *) + update (Sil.Var sb) (Some (Sil.Cstr "")) constants + + | Sil.Call (i:: [], Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: [], _, _) + when Procname.java_get_class pn = "java.lang.StringBuilder" + && Procname.java_get_method pn = "toString" -> (* StringBuilder.toString *) + update (Sil.Var i) (ConstantMap.find (Sil.Var i1) constants) constants + + | Sil.Call (i:: [], Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], _, _) + when Procname.java_get_class pn = "java.lang.StringBuilder" + && Procname.java_get_method pn = "append" -> (* StringBuilder.append *) + (match + ConstantMap.find (Sil.Var i1) constants, + ConstantMap.find (Sil.Var i2) constants with + | Some (Sil.Cstr s1), Some (Sil.Cstr s2) -> + begin + let s = s1 ^ s2 in + let u = + if String.length s < string_widening_limit then + Some (Sil.Cstr s) + else + None in + update (Sil.Var i) u constants + end + | _ -> constants) + + | _ -> constants + with Not_found -> constants in if verbose then begin @@ -119,7 +111,7 @@ module ConstantFlow = Dataflow.MakeDF(struct (Cfg.Node.get_instrs node) in if verbose then L.stdout "%a\n@." pp constants; [constants], [constants] -end) + end) let run proc_desc = let transitions = ConstantFlow.run proc_desc ConstantMap.empty in @@ -128,3 +120,15 @@ let run proc_desc = | ConstantFlow.Transition (_, post_states, _) -> ConstantFlow.join post_states ConstantMap.empty | ConstantFlow.Dead_state -> ConstantMap.empty in get_constants + +type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option + +(** Build a const map lazily. *) +let build_const_map pdesc = + let const_map = lazy (run pdesc) in + let f node exp = + try + let map = (Lazy.force const_map) node in + ConstantMap.find exp map + with Not_found -> None in + f diff --git a/infer/src/checkers/constantPropagation.mli b/infer/src/checkers/constantPropagation.mli index 52ce4dcb0..319859ab4 100644 --- a/infer/src/checkers/constantPropagation.mli +++ b/infer/src/checkers/constantPropagation.mli @@ -2,8 +2,7 @@ * Copyright (c) 2014 - Facebook. All rights reserved. *) -module ConstantMap: Map.S with type key = string +type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option -module ConstantFlow: Dataflow.DF with type state = (Sil.const option) ConstantMap.t - -val run: Cfg.Procdesc.t -> (Cfg.Node.t -> ConstantFlow.state) +(** Build a const map lazily. *) +val build_const_map : Cfg.Procdesc.t -> const_map diff --git a/infer/src/checkers/sqlChecker.ml b/infer/src/checkers/sqlChecker.ml index 9b85a3eeb..95824ba01 100644 --- a/infer/src/checkers/sqlChecker.ml +++ b/infer/src/checkers/sqlChecker.ml @@ -3,7 +3,6 @@ *) open Utils -open ConstantPropagation module L = Logging @@ -23,36 +22,31 @@ let callback_sql all_procs get_proc_desc idenv tenv proc_name proc_desc = list_map Str.regexp_case_fold _sql_start in (* Check for SQL string concatenations *) - let do_instr get_constants node = function + let do_instr const_map node = function | Sil.Call (_, Sil.Const (Sil.Cfun pn), (Sil.Var i1, _):: (Sil.Var i2, _):: [], l, _) when Procname.java_get_class pn = "java.lang.StringBuilder" && Procname.java_get_method pn = "append" -> - let rvar1 = Ident.to_string i1 in - let rvar2 = Ident.to_string i2 in + let rvar1 = Sil.Var i1 in + let rvar2 = Sil.Var i2 in begin let matches s r = Str.string_match r s 0 in - let constants = get_constants node in - if ConstantMap.mem rvar1 constants - && ConstantMap.mem rvar2 constants then - begin - match ConstantMap.find rvar1 constants, ConstantMap.find rvar2 constants with - | Some (Sil.Cstr ""), Some (Sil.Cstr s2) -> - if list_exists (matches s2) sql_start then - begin - L.stdout - "%s%s@." - "Possible SQL query using string concatenation. " - "Please consider using a prepared statement instead."; - let linereader = Printer.LineReader.create () in - L.stdout "%a@." (Checkers.PP.pp_loc_range linereader 2 2) l - end - | _ -> () - end + match const_map node rvar1, const_map node rvar2 with + | Some (Sil.Cstr ""), Some (Sil.Cstr s2) -> + if list_exists (matches s2) sql_start then + begin + L.stdout + "%s%s@." + "Possible SQL query using string concatenation. " + "Please consider using a prepared statement instead."; + let linereader = Printer.LineReader.create () in + L.stdout "%a@." (Checkers.PP.pp_loc_range linereader 2 2) l + end + | _ -> () end | _ -> () in try - let get_constants = ConstantPropagation.run proc_desc in + let const_map = ConstantPropagation.build_const_map proc_desc in if verbose then L.stdout "Analyzing %a...\n@." Procname.pp proc_name; - Cfg.Procdesc.iter_instrs (do_instr get_constants) proc_desc + Cfg.Procdesc.iter_instrs (do_instr const_map) proc_desc with _ -> ()