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

[quandary] Split exec_instr

Browse Source 
Reviewed By: ngorogiannis

Differential Revision: D13465603

fbshipit-source-id: 02799eec4
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 9d6a9f52ec
commit 3ad33c979e
1 changed files with 254 additions and 254 deletions
Show Stats Download Patch File Download Diff File

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

@ -445,11 +445,10 @@ module Make (TaintSpecification : TaintSpec.S) = struct
TaintDomain.trace_fold add_to_caller_tree summary caller_access_tree
let exec_instr (astate : Domain.t) (proc_data : extras ProcData.t) _ (instr : HilInstr.t) =
(* not all sinks are function calls; we might want to treat an array or field access as a
sink too. do this by pretending an access is a call to a dummy function and using the
existing machinery for adding function call sinks *)
let add_sinks_for_access_path access_expr loc astate =
let add_sinks_for_access_path (proc_data : extras ProcData.t) access_expr loc astate =
let rec add_sinks_for_access astate_acc = function
| HilExp.AccessExpression.Base _ ->
astate_acc
@ -476,8 +475,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
add_sinks_for_access astate_acc_result ae
in
add_sinks_for_access astate access_expr
in
let add_sources_for_access_path access_expr loc astate =
let add_sources_for_access_path (proc_data : extras ProcData.t) access_expr loc astate =
let var, _ = HilExp.AccessExpression.get_base access_expr in
if Var.is_global var then
let dummy_call_site = CallSite.make BuiltinDecl.__global_access loc in
@ -494,51 +494,35 @@ module Make (TaintSpecification : TaintSpec.S) = struct
Option.value ~default:TaintDomain.empty_node
(TaintDomain.get_node access_path astate)
in
TaintDomain.add_node access_path
(TraceDomain.add_source source trace, subtree)
astate )
TaintDomain.add_node access_path (TraceDomain.add_source source trace, subtree) astate
)
else astate
in
let rec add_sources_sinks_for_exp exp loc astate =
let rec add_sources_sinks_for_exp (proc_data : extras ProcData.t) exp loc astate =
match exp with
| HilExp.Cast (_, e) ->
add_sources_sinks_for_exp e loc astate
add_sources_sinks_for_exp proc_data e loc astate
| HilExp.AccessExpression access_expr ->
add_sinks_for_access_path access_expr loc astate
|> add_sources_for_access_path access_expr loc
add_sinks_for_access_path proc_data access_expr loc astate
|> add_sources_for_access_path proc_data access_expr loc
| _ ->
astate
in
let exec_write lhs_access_expr rhs_exp astate =
let exec_write (proc_data : extras ProcData.t) lhs_access_expr rhs_exp astate =
let rhs_node =
Option.value (hil_exp_get_node rhs_exp astate proc_data) ~default:TaintDomain.empty_node
in
let lhs_access_path = HilExp.AccessExpression.to_access_path lhs_access_expr in
TaintDomain.add_node (AccessPath.Abs.Exact lhs_access_path) rhs_node astate
in
match instr with
| Assign (Base (Var.ProgramVar pvar, _), HilExp.Exception _, _) when Pvar.is_return pvar ->
(* the Java frontend translates `throw Exception` as `return Exception`, which is a bit
wonky. this translation causes problems for us in computing a summary when an
exception is "returned" from a void function. skip code like this for now, fix via
t14159157 later *)
astate
| Assign (Base (Var.ProgramVar pvar, _), rhs_exp, _)
when Pvar.is_return pvar && HilExp.is_null_literal rhs_exp
&& Typ.equal_desc Tvoid (Procdesc.get_ret_type proc_data.pdesc).desc ->
(* similar to the case above; the Java frontend translates "return no exception" as
`return null` in a void function *)
astate
| Assign (lhs_access_expr, rhs_exp, loc) ->
add_sources_sinks_for_exp rhs_exp loc astate
|> add_sinks_for_access_path lhs_access_expr loc
|> exec_write lhs_access_expr rhs_exp
| Assume (assume_exp, _, _, loc) ->
add_sources_sinks_for_exp assume_exp loc astate
| Call (ret_ap, Direct called_pname, actuals, call_flags, callee_loc) ->
let analyze_call (proc_data : extras ProcData.t) ~ret_ap ~callee_pname ~actuals ~call_flags
~callee_loc astate =
let astate =
List.fold
~f:(fun acc exp -> add_sources_sinks_for_exp exp callee_loc acc)
~f:(fun acc exp -> add_sources_sinks_for_exp proc_data exp callee_loc acc)
actuals ~init:astate
in
let handle_model callee_pname access_tree model =
@ -559,9 +543,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
in
let propagate_to_access_path access_path actuals access_tree =
let initial_trace = access_path_get_trace access_path access_tree proc_data in
let trace_with_propagation =
List.fold ~f:exp_join_traces ~init:initial_trace actuals
in
let trace_with_propagation = List.fold ~f:exp_join_traces ~init:initial_trace actuals in
let sources = TraceDomain.sources trace_with_propagation in
let filtered_footprint =
TraceDomain.Sources.Footprint.fold
@ -592,11 +574,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
| _, [] ->
astate_acc
| TaintSpec.Propagate_to_return, actuals ->
propagate_to_access_path
(AccessPath.Abs.Abstracted (ret_ap, []))
actuals astate_acc
propagate_to_access_path (AccessPath.Abs.Abstracted (ret_ap, [])) actuals astate_acc
| ( TaintSpec.Propagate_to_receiver
, AccessExpression receiver_ae :: (_ :: _ as other_actuals) ) ->
, HilExp.AccessExpression receiver_ae :: (_ :: _ as other_actuals) ) ->
propagate_to_access_path
(AccessPath.Abs.Abstracted (HilExp.AccessExpression.to_access_path receiver_ae))
other_actuals astate_acc
@ -619,7 +599,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
(* treat unknown calls to C++ operator= as assignment *)
match List.map actuals ~f:HilExp.ignore_cast with
| [AccessExpression lhs_access_expr; rhs_exp] ->
exec_write lhs_access_expr rhs_exp access_tree
exec_write proc_data lhs_access_expr rhs_exp access_tree
| [AccessExpression lhs_access_expr; rhs_exp; HilExp.AccessExpression access_expr] -> (
let dummy_ret_access_expr = access_expr in
match dummy_ret_access_expr with
@ -627,17 +607,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct
when Pvar.is_frontend_tmp pvar ->
(* the frontend translates operator=(x, y) as operator=(x, y, dummy_ret) when
operator= returns a value type *)
exec_write lhs_access_expr rhs_exp access_tree
|> exec_write dummy_ret_access_expr rhs_exp
exec_write proc_data lhs_access_expr rhs_exp access_tree
|> exec_write proc_data dummy_ret_access_expr rhs_exp
| _ ->
L.internal_error "Unexpected call to operator= %a in %a" HilInstr.pp instr
Typ.Procname.pp
(Procdesc.get_proc_name proc_data.pdesc) ;
L.internal_error "Unexpected call to operator= at %a" Location.pp callee_loc ;
access_tree )
| _ ->
L.internal_error "Unexpected call to operator= %a in %a" HilInstr.pp instr
Typ.Procname.pp
(Procdesc.get_proc_name proc_data.pdesc) ;
L.internal_error "Unexpected call to operator= at %a" Location.pp callee_loc ;
access_tree )
| _ ->
let model =
@ -648,7 +624,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
in
let dummy_ret_opt =
match ret_ap with
| _, {Typ.desc= Tvoid} when not (Typ.Procname.is_java called_pname) -> (
| _, {Typ.desc= Tvoid} when not (Typ.Procname.is_java callee_pname) -> (
(* the C++ frontend handles returns of non-pointers by adding a dummy
pass-by-reference variable as the last actual, then returning the value by
assigning to it. understand this pattern by pretending it's the return value *)
@ -721,7 +697,31 @@ module Make (TaintSpecification : TaintSpec.S) = struct
in
Domain.join astate_acc astate_with_sanitizer
in
analyze_call Domain.empty called_pname
analyze_call Domain.empty callee_pname
let exec_instr (astate : Domain.t) (proc_data : extras ProcData.t) _ (instr : HilInstr.t) =
match instr with
| Assign (Base (Var.ProgramVar pvar, _), HilExp.Exception _, _) when Pvar.is_return pvar ->
(* the Java frontend translates `throw Exception` as `return Exception`, which is a bit
wonky. this translation causes problems for us in computing a summary when an
exception is "returned" from a void function. skip code like this for now, fix via
t14159157 later *)
astate
| Assign (Base (Var.ProgramVar pvar, _), rhs_exp, _)
when Pvar.is_return pvar && HilExp.is_null_literal rhs_exp
&& Typ.equal_desc Tvoid (Procdesc.get_ret_type proc_data.pdesc).desc ->
(* similar to the case above; the Java frontend translates "return no exception" as
`return null` in a void function *)
astate
| Assign (lhs_access_expr, rhs_exp, loc) ->
add_sources_sinks_for_exp proc_data rhs_exp loc astate
|> add_sinks_for_access_path proc_data lhs_access_expr loc
|> exec_write proc_data lhs_access_expr rhs_exp
| Assume (assume_exp, _, _, loc) ->
add_sources_sinks_for_exp proc_data assume_exp loc astate
| Call (ret_ap, Direct callee_pname, actuals, call_flags, callee_loc) ->
analyze_call proc_data ~ret_ap ~callee_pname ~actuals ~call_flags ~callee_loc astate
| _ ->
astate

Write Preview
Loading…
Cancel
Save