pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[quandary] switch to using base -> formal num map in extras

Browse Source 
Reviewed By: dkgi

Differential Revision: D3883256

fbshipit-source-id: 857e1f9
master
Sam Blackshear 8 years ago committed by Facebook Github Bot 2
parent 31e6849ec0
commit de146f4f2d
5 changed files with 48 additions and 44 deletions
Show Stats Download Patch File Download Diff File

12
infer/src/checkers/accessPath.ml
Unescape View File

@ -160,3 +160,15 @@ let pp_raw fmt (base, accesses) =
let pp fmt = function
| Exact access_path -> pp_raw fmt access_path
| Abstracted access_path -> F.fprintf fmt "%a*" pp_raw access_path
module BaseMap = PrettyPrintable.MakePPMap(struct
type t = base
let compare = base_compare
let pp_key = pp_base
end)
module AccessMap = PrettyPrintable.MakePPMap(struct
type t = access
let compare = access_compare
let pp_key = pp_access
end)

4
infer/src/checkers/accessPath.mli
Unescape View File

@ -81,3 +81,7 @@ val (<=) : lhs:t -> rhs:t -> bool
val pp_base : Format.formatter -> base -> unit
val pp : Format.formatter -> t -> unit
module BaseMap : PrettyPrintable.PPMap with type key = base
module AccessMap : PrettyPrintable.PPMap with type key = access

13
infer/src/checkers/accessTree.ml
Unescape View File

@ -15,17 +15,8 @@ module L = Logging
(** tree of (trace, access path) associations organized by structure of access paths *)
module Make (TraceDomain : AbstractDomain.S) = struct
module AccessMap = PrettyPrintable.MakePPMap(struct
type t = AccessPath.access
let compare = AccessPath.access_compare
let pp_key = AccessPath.pp_access
end)
module BaseMap = PrettyPrintable.MakePPMap(struct
type t = AccessPath.base
let compare = AccessPath.base_compare
let pp_key = AccessPath.pp_base
end)
module AccessMap = AccessPath.AccessMap
module BaseMap = AccessPath.BaseMap
type node = TraceDomain.astate * tree
and tree =

61
infer/src/quandary/TaintAnalysis.ml
Unescape View File

@ -76,26 +76,27 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
module CFG = CFG
module Domain = Domain
type formal_list = AccessPath.base list
type extras = formal_list
(** map from formals to their position *)
type formal_map = int AccessPath.BaseMap.t
type extras = formal_map
let is_formal base proc_data =
IList.exists (AccessPath.base_equal base) proc_data.ProcData.extras
let is_formal base formal_map =
AccessPath.BaseMap.mem base formal_map
let is_rooted_in_formal ap proc_data =
let is_rooted_in_formal ap formal_map =
let root, _ = AccessPath.extract ap in
is_formal root proc_data
is_formal root formal_map
let resolve_id id_map id =
try Some (IdMapDomain.find id id_map)
with Not_found -> None
(* get the node associated with [access_path] in [access_tree] *)
let access_path_get_node access_path access_tree proc_data loc =
let access_path_get_node access_path access_tree (proc_data : formal_map ProcData.t) loc =
match TaintDomain.get_node access_path access_tree with
| Some _ as node_opt ->
node_opt
| None when is_rooted_in_formal access_path proc_data ->
| None when is_rooted_in_formal access_path proc_data.extras ->
let call_site = CallSite.make (Cfg.Procdesc.get_proc_name proc_data.ProcData.pdesc) loc in
let trace =
TraceDomain.of_source (TraceDomain.Source.make_footprint access_path call_site) in
@ -239,9 +240,8 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
let access_tree = IList.fold_left apply_one astate_in.access_tree summary in
{ astate_in with access_tree; }
let exec_instr
({ Domain.id_map; } as astate) (proc_data : AccessPath.base list ProcData.t) _ instr =
let f_resolve_id = resolve_id id_map in
let exec_instr (astate : Domain.astate) (proc_data : formal_map ProcData.t) _ instr =
let f_resolve_id = resolve_id astate.id_map in
match instr with
| Sil.Load (lhs_id, rhs_exp, rhs_typ, _) ->
analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate
@ -351,7 +351,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
(** grab footprint traces in [access_tree] and make them into inputs for the summary. for each
trace Footprint(T_out, a.b.c) associated with access path x.z.y, we will produce a summary of
the form (x.z.y, T_in) => (T_in + T_out, a.b.c) *)
let make_summary formals access_tree pdesc =
let make_summary formal_map access_tree pdesc =
let add_summary_for_output summary_acc output trace =
let make_in_out_summary summary_input summary_output trace =
let _ = match summary_input with
@ -361,22 +361,14 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
summary_input summary_output (TraceDomain.to_summary_trace trace) in
let extract_input source acc =
let get_formal_number base formal_bases =
IList.find_mapi_opt
(fun index formal_base ->
if AccessPath.base_equal base formal_base
then Some index
else None)
formal_bases in
match TraceDomain.Source.get_footprint_access_path source with
| Some footprint_ap ->
let input =
let footprint_ap_base = fst (AccessPath.extract footprint_ap) in
match get_formal_number footprint_ap_base formals with
| Some index ->
match AccessPath.BaseMap.find footprint_ap_base formal_map with
| index ->
QuandarySummary.make_formal_input index footprint_ap
| None ->
| exception Not_found ->
failwithf
"Couldn't find formal number for %a@." AccessPath.pp_base footprint_ap_base in
let summary = make_in_out_summary input output trace in
@ -402,7 +394,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
| exception Not_found ->
summary_acc in
let add_formal_summaries summary_acc formal_index formal =
let add_formal_summaries formal formal_index summary_acc =
let f_make_output = QuandarySummary.make_formal_output formal_index in
add_summaries_for_base ~f_make_output formal summary_acc in
@ -414,22 +406,27 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
add_summaries_for_base
~f_make_output:QuandarySummary.make_return_output return_var_base summary_acc in
(* add summaries for each formal and for the return value *)
IList.fold_lefti add_formal_summaries [] formals
(* add summaries for each formal and the return value *)
AccessPath.BaseMap.fold add_formal_summaries formal_map []
|> add_return_summaries
let dummy_cg = Cg.create ()
let checker { Callbacks.get_proc_desc; proc_name; proc_desc; tenv; } =
let analyze_ondemand pdesc =
let make_formal_access_paths pdesc : AccessPath.base list=
let make_formal_access_paths pdesc =
let pname = Cfg.Procdesc.get_proc_name pdesc in
let attrs = Cfg.Procdesc.get_attributes pdesc in
IList.map
(fun (name, typ) ->
let pvar = Pvar.mk name pname in
AccessPath.base_of_pvar pvar typ)
attrs.ProcAttributes.formals in
let formals_with_nums =
IList.mapi
(fun index (name, typ) ->
let pvar = Pvar.mk name pname in
AccessPath.base_of_pvar pvar typ, index)
attrs.ProcAttributes.formals in
IList.fold_left
(fun formal_map (base, index) -> AccessPath.BaseMap.add base index formal_map)
AccessPath.BaseMap.empty
formals_with_nums in
let formals = make_formal_access_paths pdesc in
let proc_data = ProcData.make pdesc tenv formals in
match Analyzer.compute_post proc_data with

2
infer/src/unit/TaintTests.ml
Unescape View File

@ -275,5 +275,5 @@ let tests =
invariant "{ ret_id$0 => (SOURCE -> SINK) }";
];
] |> TestInterpreter.create_tests ~pp_opt:pp_sparse [] in
] |> TestInterpreter.create_tests ~pp_opt:pp_sparse AccessPath.BaseMap.empty in
"taint_test_suite">:::test_list

Write Preview
Loading…
Cancel
Save