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

[racerd] refactor transition function

Browse Source 
Summary: The transition function was using a complicated-looking and possibly-inefficient pattern of options for everything, when simple pattern matching with guards is sufficient.

Reviewed By: skcho

Differential Revision: D21179606

fbshipit-source-id: a37f97594
master
Nikos Gorogiannis 5 years ago committed by Facebook GitHub Bot
parent 5d8b4947fe
commit ab79b2966a
3 changed files with 76 additions and 83 deletions
Show Stats Download Patch File Download Diff File

129
infer/src/concurrency/RacerD.ml
Unescape View File

@ -34,8 +34,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
None None
let add_access formals loc ~is_write_access locks threads ownership let get_first_actual actuals = List.hd actuals |> Option.bind ~f:get_access_exp
(proc_data : extras ProcData.t) access_domain exp =
let apply_to_first_actual ~f astate actuals =
get_first_actual actuals |> Option.value_map ~default:astate ~f
let add_access formals loc ~is_write_access locks threads ownership tenv access_domain exp =
let open Domain in let open Domain in
let rec add_field_accesses prefix_path acc = function let rec add_field_accesses prefix_path acc = function
| [] -> | [] ->
@ -44,7 +49,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let prefix_path' = Option.value_exn (AccessExpression.add_access prefix_path access) in let prefix_path' = Option.value_exn (AccessExpression.add_access prefix_path access) in
if if
(not (HilExp.Access.is_field_or_array_access access)) (not (HilExp.Access.is_field_or_array_access access))
|| RacerDModels.is_safe_access access prefix_path proc_data.tenv || RacerDModels.is_safe_access access prefix_path tenv
then add_field_accesses prefix_path' acc access_list then add_field_accesses prefix_path' acc access_list
else else
let is_write = List.is_empty access_list && is_write_access in let is_write = List.is_empty access_list && is_write_access in
@ -60,13 +65,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
add_field_accesses base acc accesses ) add_field_accesses base acc accesses )
let make_container_access formals ret_base callee_pname ~is_write receiver_ap callee_loc tenv let make_container_access proc_data ret_base callee_pname ~is_write receiver_ap callee_loc
(astate : Domain.t) = (astate : Domain.t) =
let open Domain in let open Domain in
let ProcData.{extras= formals; tenv} = proc_data in
if if
AttributeMapDomain.is_synchronized astate.attribute_map receiver_ap AttributeMapDomain.is_synchronized astate.attribute_map receiver_ap
|| RacerDModels.is_synchronized_container callee_pname receiver_ap tenv || RacerDModels.is_synchronized_container callee_pname receiver_ap tenv
then None then astate
else else
let ownership_pre = OwnershipDomain.get_owned receiver_ap astate.ownership in let ownership_pre = OwnershipDomain.get_owned receiver_ap astate.ownership in
let callee_access = let callee_access =
@ -77,16 +83,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
OwnershipDomain.add (AccessExpression.base ret_base) ownership_pre astate.ownership OwnershipDomain.add (AccessExpression.base ret_base) ownership_pre astate.ownership
in in
let accesses = AccessDomain.add_opt callee_access astate.accesses in let accesses = AccessDomain.add_opt callee_access astate.accesses in
Some {astate with accesses; ownership} {astate with accesses; ownership}
let add_reads formals exps loc ({accesses; locks; threads; ownership} as astate : Domain.t) let add_reads formals exps loc ({accesses; locks; threads; ownership} as astate : Domain.t) tenv =
proc_data = let accesses =
let accesses' =
List.fold exps ~init:accesses List.fold exps ~init:accesses
~f:(add_access formals loc ~is_write_access:false locks threads ownership proc_data) ~f:(add_access formals loc ~is_write_access:false locks threads ownership tenv)
in in
{astate with accesses= accesses'} {astate with accesses}
let expand_actuals formals actuals accesses pdesc = let expand_actuals formals actuals accesses pdesc =
@ -153,28 +158,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let open RacerDModels in let open RacerDModels in
let open RacerDDomain in let open RacerDDomain in
if RacerDModels.is_synchronized_container_constructor tenv callee_pname actuals then if RacerDModels.is_synchronized_container_constructor tenv callee_pname actuals then
List.hd actuals |> Option.bind ~f:get_access_exp apply_to_first_actual astate actuals ~f:(fun receiver ->
|> Option.value_map ~default:astate ~f:(fun receiver -> let attribute_map = AttributeMapDomain.add receiver Synchronized astate.attribute_map in
let attribute_map = {astate with attribute_map} )
AttributeMapDomain.add receiver Synchronized astate.attribute_map
in
{astate with attribute_map} )
else if RacerDModels.is_converter_to_synchronized_container tenv callee_pname actuals then else if RacerDModels.is_converter_to_synchronized_container tenv callee_pname actuals then
let attribute_map = let attribute_map =
AttributeMapDomain.add (AccessExpression.base ret_base) Synchronized astate.attribute_map AttributeMapDomain.add (AccessExpression.base ret_base) Synchronized astate.attribute_map
in in
{astate with attribute_map} {astate with attribute_map}
else if is_box callee_pname then else if is_box callee_pname then
match actuals with apply_to_first_actual astate actuals ~f:(fun actual_access_expr ->
| HilExp.AccessExpression actual_access_expr :: _ if AttributeMapDomain.is_functional astate.attribute_map actual_access_expr then
when AttributeMapDomain.is_functional astate.attribute_map actual_access_expr -> (* TODO: check for constants, which are functional? *)
(* TODO: check for constants, which are functional? *) let attribute_map =
let attribute_map = AttributeMapDomain.add (AccessExpression.base ret_base) Functional
AttributeMapDomain.add (AccessExpression.base ret_base) Functional astate.attribute_map astate.attribute_map
in in
{astate with attribute_map} {astate with attribute_map}
| _ -> else astate )
astate
else else
let ownership = let ownership =
OwnershipDomain.add (AccessExpression.base ret_base) OwnershipAbstractValue.owned OwnershipDomain.add (AccessExpression.base ret_base) OwnershipAbstractValue.owned
@ -183,37 +184,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate with ownership} {astate with ownership}
let treat_call_acquiring_ownership ret_base procname actuals loc let do_call_acquiring_ownership ret_base astate =
({ProcData.tenv; extras} as proc_data) astate () =
let open Domain in let open Domain in
if RacerDModels.acquires_ownership procname tenv then let ownership =
let astate = add_reads extras actuals loc astate proc_data in OwnershipDomain.add (AccessExpression.base ret_base) OwnershipAbstractValue.owned
let ownership = astate.ownership
OwnershipDomain.add (AccessExpression.base ret_base) OwnershipAbstractValue.owned in
astate.ownership {astate with ownership}
in
Some {astate with ownership}
else None
let treat_container_accesses ret_base callee_pname actuals loc {ProcData.tenv; extras} astate () = let do_container_access ~is_write ret_base callee_pname actuals loc proc_data astate =
let open RacerDModels in match get_first_actual actuals with
Option.bind (get_container_access callee_pname tenv) ~f:(fun container_access -> | Some receiver_expr ->
match List.hd actuals with make_container_access proc_data ret_base callee_pname ~is_write receiver_expr loc astate
| Some (HilExp.AccessExpression receiver_expr) -> | None ->
let is_write = L.internal_error "Call to %a is marked as a container access, but has no receiver"
match container_access with ContainerWrite -> true | ContainerRead -> false Procname.pp callee_pname ;
in astate
make_container_access extras ret_base callee_pname ~is_write receiver_expr loc tenv
astate
| _ ->
L.internal_error "Call to %a is marked as a container write, but has no receiver"
Procname.pp callee_pname ;
None )
let do_proc_call ret_base callee_pname actuals call_flags loc {ProcData.tenv; summary; extras} let do_proc_call ret_base callee_pname actuals call_flags loc {ProcData.tenv; summary; extras}
(astate : Domain.t) () = (astate : Domain.t) =
let open Domain in let open Domain in
let open RacerDModels in let open RacerDModels in
let open ConcurrencyModels in let open ConcurrencyModels in
@ -317,12 +308,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate_callee with ownership; attribute_map} {astate_callee with ownership; attribute_map}
let do_assignment lhs_access_exp rhs_exp loc ({ProcData.tenv; extras} as proc_data) let do_assignment lhs_access_exp rhs_exp loc {ProcData.tenv; extras} (astate : Domain.t) =
(astate : Domain.t) =
let open Domain in let open Domain in
let rhs_accesses = let rhs_accesses =
add_access extras loc ~is_write_access:false astate.locks astate.threads astate.ownership add_access extras loc ~is_write_access:false astate.locks astate.threads astate.ownership tenv
proc_data astate.accesses rhs_exp astate.accesses rhs_exp
in in
let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in
let is_functional = let is_functional =
@ -345,7 +335,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
rhs_accesses rhs_accesses
else else
add_access extras loc ~is_write_access:true astate.locks astate.threads astate.ownership add_access extras loc ~is_write_access:true astate.locks astate.threads astate.ownership
proc_data rhs_accesses (HilExp.AccessExpression lhs_access_exp) tenv rhs_accesses (HilExp.AccessExpression lhs_access_exp)
in in
let ownership = OwnershipDomain.propagate_assignment lhs_access_exp rhs_exp astate.ownership in let ownership = OwnershipDomain.propagate_assignment lhs_access_exp rhs_exp astate.ownership in
let attribute_map = let attribute_map =
@ -354,7 +344,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate with accesses; ownership; attribute_map} {astate with accesses; ownership; attribute_map}
let do_assume formals assume_exp loc proc_data (astate : Domain.t) = let do_assume formals assume_exp loc tenv (astate : Domain.t) =
let open Domain in let open Domain in
let apply_choice bool_value (acc : Domain.t) = function let apply_choice bool_value (acc : Domain.t) = function
| Attribute.LockHeld -> | Attribute.LockHeld ->
@ -373,7 +363,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
let accesses = let accesses =
add_access formals loc ~is_write_access:false astate.locks astate.threads astate.ownership add_access formals loc ~is_write_access:false astate.locks astate.threads astate.ownership
proc_data astate.accesses assume_exp tenv astate.accesses assume_exp
in in
let astate' = let astate' =
match HilExp.get_access_exprs assume_exp with match HilExp.get_access_exprs assume_exp with
@ -390,16 +380,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate' with accesses} {astate' with accesses}
let exec_instr (astate : Domain.t) ({ProcData.summary; extras} as proc_data) _ let exec_instr astate ({ProcData.summary; extras; tenv} as proc_data) _ instr =
(instr : HilInstr.t) = match (instr : HilInstr.t) with
match instr with
| Call (ret_base, Direct callee_pname, actuals, call_flags, loc) -> | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) ->
let astate = add_reads extras actuals loc astate proc_data in let astate = add_reads extras actuals loc astate tenv in
treat_call_acquiring_ownership ret_base callee_pname actuals loc proc_data astate () if RacerDModels.acquires_ownership callee_pname tenv then
|> IOption.if_none_evalopt do_call_acquiring_ownership ret_base astate
~f:(treat_container_accesses ret_base callee_pname actuals loc proc_data astate) else if RacerDModels.is_container_write tenv callee_pname then
|> IOption.if_none_eval do_container_access ~is_write:true ret_base callee_pname actuals loc proc_data astate
~f:(do_proc_call ret_base callee_pname actuals call_flags loc proc_data astate) else if RacerDModels.is_container_read tenv callee_pname then
do_container_access ~is_write:false ret_base callee_pname actuals loc proc_data astate
else do_proc_call ret_base callee_pname actuals call_flags loc proc_data astate
| Call (_, Indirect _, _, _, _) -> | Call (_, Indirect _, _, _, _) ->
if Procname.is_java (Summary.get_proc_name summary) then if Procname.is_java (Summary.get_proc_name summary) then
L.(die InternalError) "Unexpected indirect call instruction %a" HilInstr.pp instr L.(die InternalError) "Unexpected indirect call instruction %a" HilInstr.pp instr
@ -407,7 +398,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Assign (lhs_access_expr, rhs_exp, loc) -> | Assign (lhs_access_expr, rhs_exp, loc) ->
do_assignment lhs_access_expr rhs_exp loc proc_data astate do_assignment lhs_access_expr rhs_exp loc proc_data astate
| Assume (assume_exp, _, _, loc) -> | Assume (assume_exp, _, _, loc) ->
do_assume extras assume_exp loc proc_data astate do_assume extras assume_exp loc tenv astate
| Metadata _ -> | Metadata _ ->
astate astate

26
infer/src/concurrency/RacerDModels.ml
Unescape View File

@ -20,8 +20,6 @@ module AnnotationAliases = struct
"Couldn't parse thread-safety annotation aliases; expected list of strings" "Couldn't parse thread-safety annotation aliases; expected list of strings"
end end
type container_access = ContainerRead | ContainerWrite
let make_android_support_template suffix methods = let make_android_support_template suffix methods =
let open MethodMatcher in let open MethodMatcher in
[ {default with classname= "android.support.v4.util." ^ suffix; methods} [ {default with classname= "android.support.v4.util." ^ suffix; methods}
@ -137,23 +135,27 @@ let is_cpp_container_write =
fun pname -> QualifiedCppName.Match.match_qualifiers matcher (Procname.get_qualifiers pname) fun pname -> QualifiedCppName.Match.match_qualifiers matcher (Procname.get_qualifiers pname)
let get_container_access pn tenv = let is_container_write tenv pn =
match pn with match pn with
| Procname.Java _ when is_java_container_write tenv pn [] -> | Procname.Java _ when is_java_container_write tenv pn [] ->
Some ContainerWrite true
| Procname.Java _ when is_java_container_read tenv pn [] -> | (Procname.ObjC_Cpp _ | C _) when is_cpp_container_write pn ->
Some ContainerRead true
| _ ->
false
let is_container_read tenv pn =
match pn with
| Procname.Java _ -> | Procname.Java _ ->
None is_java_container_read tenv pn []
(* The following order matters: we want to check if pname is a container write (* The following order matters: we want to check if pname is a container write
before we check if pname is a container read. This is due to a different before we check if pname is a container read. This is due to a different
treatment between std::map::operator[] and all other operator[]. *) treatment between std::map::operator[] and all other operator[]. *)
| (Procname.ObjC_Cpp _ | C _) when is_cpp_container_write pn -> | Procname.ObjC_Cpp _ | C _ ->
Some ContainerWrite (not (is_cpp_container_write pn)) && is_cpp_container_read pn
| (Procname.ObjC_Cpp _ | C _) when is_cpp_container_read pn ->
Some ContainerRead
| _ -> | _ ->
None false
(** holds of procedure names which should not be analyzed in order to avoid known sources of (** holds of procedure names which should not be analyzed in order to avoid known sources of

4
infer/src/concurrency/RacerDModels.mli
Unescape View File

@ -7,9 +7,9 @@
open! IStd open! IStd
type container_access = ContainerRead | ContainerWrite val is_container_read : Tenv.t -> Procname.t -> bool
val get_container_access : Procname.t -> Tenv.t -> container_access option val is_container_write : Tenv.t -> Procname.t -> bool
(** return Some (access) if this procedure accesses the contents of a container (e.g., Map.get) *) (** return Some (access) if this procedure accesses the contents of a container (e.g., Map.get) *)
val has_return_annot : (Annot.Item.t -> bool) -> Procname.t -> bool val has_return_annot : (Annot.Item.t -> bool) -> Procname.t -> bool

Write Preview
Loading…
Cancel
Save