diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index e27530b9c..d1838d986 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -19,8 +19,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct module TaintDomain = TaintSpecification.AccessTree module IdMapDomain = IdAccessPathMapDomain - (** a map from a formal to its position and (optionally) whether we should treat it as a source *) - type formal_map = (int * TraceDomain.Source.t option) AccessPath.BaseMap.t + (** a map from a formal to its position *) + type formal_map = int AccessPath.BaseMap.t module Summary = Summary.Make(struct type summary = QuandarySummary.t @@ -78,11 +78,11 @@ module Make (TaintSpecification : TaintSpec.S) = struct | Var.ProgramVar pvar -> Pvar.is_global pvar | Var.LogicalVar _ -> false - let make_footprint_var formal_num = - Var.of_id (Ident.create_footprint Ident.name_spec formal_num) + let make_footprint_var formal_index = + Var.of_id (Ident.create_footprint Ident.name_spec formal_index) - let make_footprint_access_path formal_num access_path = - AccessPath.with_base_var (make_footprint_var formal_num) access_path + let make_footprint_access_path formal_index access_path = + AccessPath.with_base_var (make_footprint_var formal_index) access_path module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG @@ -109,14 +109,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct Some (TaintDomain.make_normal_leaf trace) in let root, _ = AccessPath.extract access_path in try - let formal_num, taint_opt = AccessPath.BaseMap.find root proc_data.extras in - begin - match taint_opt with - | None -> - make_footprint_trace (make_footprint_access_path formal_num access_path) - | Some source -> - Some (TaintDomain.make_normal_leaf (TraceDomain.of_source source)) - end + let formal_index = AccessPath.BaseMap.find root proc_data.extras in + make_footprint_trace (make_footprint_access_path formal_index access_path) with Not_found -> if is_global root then make_footprint_trace access_path @@ -197,7 +191,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct let add_sinks sinks actuals ({ Domain.access_tree; id_map; } as astate) proc_data callee_site = let f_resolve_id = resolve_id id_map in - (* add [sink] to the trace associated with the [formal_num]th actual *) + (* add [sink] to the trace associated with the [formal_index]th actual *) let add_sink_to_actual access_tree_acc (sink_param : TraceDomain.Sink.parameter) = let actual_exp, actual_typ = IList.nth actuals sink_param.index in match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with @@ -243,11 +237,11 @@ module Make (TaintSpecification : TaintSpec.S) = struct let apply_return ret_ap = match ret_opt with | Some (ret_id, _) -> AccessPath.with_base_var (Var.of_id ret_id) ret_ap | None -> failwith "Have summary for retval, but no ret id to bind it to!" in - let get_actual_ap formal_num = + let get_actual_ap formal_index = let f_resolve_id = resolve_id astate_in.id_map in try let actual_exp, actual_typ = - IList.nth actuals formal_num in + IList.nth actuals formal_index in AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with Failure _ -> None in @@ -501,7 +495,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct (fun base node acc -> let base' = try - let formal_index, _ = AccessPath.BaseMap.find base formal_map in + let formal_index = AccessPath.BaseMap.find base formal_map in make_footprint_var formal_index, snd base with Not_found -> base in @@ -515,6 +509,23 @@ module Make (TaintSpecification : TaintSpec.S) = struct let checker ({ Callbacks.tenv } as callback) = + (* bind parameters to a trace with a tainted source (if applicable) *) + let make_initial pdesc = + let pname = Procdesc.get_proc_name pdesc in + let access_tree = + IList.fold_left (fun acc (name, typ, taint_opt) -> + match taint_opt with + | Some source -> + let base_ap = AccessPath.Exact (AccessPath.of_pvar (Pvar.mk name pname) typ) in + TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc + | None -> + acc) + TaintDomain.empty + (TraceDomain.Source.get_tainted_formals pdesc tenv) in + if TaintDomain.BaseMap.is_empty access_tree + then Domain.empty + else { Domain.empty with Domain.access_tree; } in + let compute_post (proc_data : formal_map ProcData.t) = if not (Procdesc.did_preanalysis proc_data.pdesc) then @@ -522,7 +533,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct Preanal.do_liveness proc_data.pdesc proc_data.tenv; Preanal.do_dynamic_dispatch proc_data.pdesc (Cg.create None) proc_data.tenv; end; - match Analyzer.compute_post proc_data ~initial:Domain.empty with + let initial = make_initial proc_data.pdesc in + match Analyzer.compute_post proc_data ~initial with | Some { access_tree; } -> Some (make_summary proc_data.extras access_tree) | None -> @@ -532,15 +544,15 @@ module Make (TaintSpecification : TaintSpec.S) = struct let make_extras pdesc = let pname = Procdesc.get_proc_name pdesc in + let attrs = Procdesc.get_attributes pdesc in let formals_with_nums = IList.mapi - (fun index (name, typ, taint_opt) -> + (fun index (name, typ) -> let pvar = Pvar.mk name pname in - AccessPath.base_of_pvar pvar typ, index, taint_opt) - (TraceDomain.Source.get_tainted_formals pdesc tenv) in + AccessPath.base_of_pvar pvar typ, index) + attrs.ProcAttributes.formals in IList.fold_left - (fun formal_map (base, index, taint_opt) -> - AccessPath.BaseMap.add base (index, taint_opt) formal_map) + (fun formal_map (base, index) -> AccessPath.BaseMap.add base index formal_map) AccessPath.BaseMap.empty formals_with_nums in