From 5e50e9947c13cc08f158587de23de93f584b216f Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Tue, 10 Nov 2020 02:49:44 -0800 Subject: [PATCH] [racerd] move some domain operations into domain module Summary: As per title, plus minor improvements in interfaces and a couple of FIXMEs. Reviewed By: skcho Differential Revision: D24836125 fbshipit-source-id: f7a4dc196 --- infer/src/concurrency/RacerD.ml | 135 +++++-------------------- infer/src/concurrency/RacerDDomain.ml | 96 +++++++++++++++--- infer/src/concurrency/RacerDDomain.mli | 46 ++++----- 3 files changed, 125 insertions(+), 152 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 312657460..e2abf8aa9 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -20,75 +20,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type nonrec analysis_data = analysis_data - let rec get_access_exp = function - | HilExp.AccessExpression access_expr -> - Some access_expr - | HilExp.Cast (_, e) | HilExp.Exception e -> - get_access_exp e - | _ -> - None - - - let get_first_actual actuals = List.hd actuals |> Option.bind ~f:get_access_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 rec add_field_accesses prefix_path acc = function - | [] -> - acc - | access :: access_list -> - let prefix_path' = Option.value_exn (AccessExpression.add_access prefix_path access) in - if - (not (HilExp.Access.is_field_or_array_access access)) - || RacerDModels.is_safe_access access prefix_path tenv - then add_field_accesses prefix_path' acc access_list - else - let is_write = List.is_empty access_list && is_write_access in - let pre = OwnershipDomain.get_owned prefix_path ownership in - let snapshot_opt = - AccessSnapshot.make_access formals prefix_path' ~is_write loc locks threads pre - in - let access_acc' = AccessDomain.add_opt snapshot_opt acc in - add_field_accesses prefix_path' access_acc' access_list - in - List.fold (HilExp.get_access_exprs exp) ~init:access_domain ~f:(fun acc access_expr -> - let base, accesses = AccessExpression.to_accesses access_expr in - add_field_accesses base acc accesses ) - - - let make_container_access {interproc= {tenv}; formals} ret_base callee_pname ~is_write receiver_ap - callee_loc (astate : Domain.t) = - let open Domain in - if - AttributeMapDomain.is_synchronized astate.attribute_map receiver_ap - || RacerDModels.is_synchronized_container callee_pname receiver_ap tenv - then astate - else - let ownership_pre = OwnershipDomain.get_owned receiver_ap astate.ownership in - let callee_access = - AccessSnapshot.make_container_access formals receiver_ap ~is_write callee_pname callee_loc - astate.locks astate.threads ownership_pre - in - let ownership = - OwnershipDomain.add (AccessExpression.base ret_base) ownership_pre astate.ownership - in - let accesses = AccessDomain.add_opt callee_access astate.accesses in - {astate with accesses; ownership} - - - let add_reads formals exps loc ({accesses; locks; threads; ownership} as astate : Domain.t) tenv = - let accesses = - List.fold exps ~init:accesses - ~f:(add_access formals loc ~is_write_access:false locks threads ownership tenv) - in - {astate with accesses} - - let expand_actuals formals actuals accesses pdesc = + (* FIXME fix quadratic order with an array-backed substitution *) let open Domain in if AccessDomain.is_empty accesses then accesses else @@ -98,7 +31,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Some formal_index -> ( match List.nth actuals formal_index with | Some actual_exp -> ( - match get_access_exp actual_exp with + match accexp_of_hilexp actual_exp with | Some actual -> AccessExpression.append ~onto:actual exp |> Option.value ~default:exp | None -> @@ -152,7 +85,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let open RacerDModels in let open RacerDDomain in if RacerDModels.is_synchronized_container_constructor tenv callee_pname actuals then - apply_to_first_actual astate actuals ~f:(fun receiver -> + apply_to_first_actual actuals astate ~f:(fun receiver -> let 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 @@ -161,7 +94,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in {astate with attribute_map} else if is_box callee_pname then - apply_to_first_actual astate actuals ~f:(fun actual_access_expr -> + apply_to_first_actual actuals astate ~f:(fun actual_access_expr -> if AttributeMapDomain.is_functional astate.attribute_map actual_access_expr then (* TODO: check for constants, which are functional? *) let attribute_map = @@ -187,16 +120,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with ownership} - let do_container_access ~is_write ret_base callee_pname actuals loc analysis_data astate = - match get_first_actual actuals with - | Some receiver_expr -> - make_container_access analysis_data ret_base callee_pname ~is_write receiver_expr loc astate - | None -> - L.internal_error "Call to %a is marked as a container access, but has no receiver" - Procname.pp callee_pname ; - astate - - let do_proc_call ret_base callee_pname actuals call_flags loc {interproc= {tenv; analyze_dependency}; formals} (astate : Domain.t) = let open Domain in @@ -303,10 +226,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let do_assignment lhs_access_exp rhs_exp loc {interproc= {tenv}; formals} (astate : Domain.t) = let open Domain in - let rhs_accesses = - add_access formals loc ~is_write_access:false astate.locks astate.threads astate.ownership - tenv astate.accesses rhs_exp - in + let astate = add_access tenv formals loc ~is_write:false astate rhs_exp in let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in let is_functional = (not (List.is_empty rhs_access_exprs)) @@ -321,20 +241,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> true in - let accesses = + let astate = if is_functional then (* we want to forget about writes to @Functional fields altogether, otherwise we'll report spurious read/write races *) - rhs_accesses + astate else - add_access formals loc ~is_write_access:true astate.locks astate.threads astate.ownership - tenv rhs_accesses (HilExp.AccessExpression lhs_access_exp) + add_access tenv formals loc ~is_write:true astate (HilExp.AccessExpression lhs_access_exp) in let ownership = OwnershipDomain.propagate_assignment lhs_access_exp rhs_exp astate.ownership in let attribute_map = AttributeMapDomain.propagate_assignment lhs_access_exp rhs_exp astate.attribute_map in - {astate with accesses; ownership; attribute_map} + {astate with ownership; attribute_map} let do_assume formals assume_exp loc tenv (astate : Domain.t) = @@ -354,35 +273,31 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Attribute.(Functional | Nothing | Synchronized) -> acc in - let accesses = - add_access formals loc ~is_write_access:false astate.locks astate.threads astate.ownership - tenv astate.accesses assume_exp - in - let astate' = - match HilExp.get_access_exprs assume_exp with - | [access_expr] -> - HilExp.eval_boolean_exp access_expr assume_exp - |> Option.value_map ~default:astate ~f:(fun bool_value -> - (* prune (prune_exp) can only evaluate to true if the choice is [bool_value]. - add the constraint that the choice must be [bool_value] to the state *) - AttributeMapDomain.get access_expr astate.attribute_map - |> apply_choice bool_value astate ) - | _ -> - astate - in - {astate' with accesses} + let astate = add_access tenv formals loc ~is_write:false astate assume_exp in + match HilExp.get_access_exprs assume_exp with + | [access_expr] -> + HilExp.eval_boolean_exp access_expr assume_exp + |> Option.value_map ~default:astate ~f:(fun bool_value -> + (* prune (prune_exp) can only evaluate to true if the choice is [bool_value]. + add the constraint that the choice must be [bool_value] to the state *) + AttributeMapDomain.get access_expr astate.attribute_map + |> apply_choice bool_value astate ) + | _ -> + astate let exec_instr astate ({interproc= {proc_desc; tenv}; formals} as analysis_data) _ instr = match (instr : HilInstr.t) with | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) -> - let astate = add_reads formals actuals loc astate tenv in + let astate = Domain.add_reads_of_hilexps tenv formals actuals loc astate in if RacerDModels.acquires_ownership callee_pname tenv then do_call_acquiring_ownership ret_base astate else if RacerDModels.is_container_write tenv callee_pname then - do_container_access ~is_write:true ret_base callee_pname actuals loc analysis_data astate + Domain.add_container_access tenv formals ~is_write:true ret_base callee_pname actuals loc + astate else if RacerDModels.is_container_read tenv callee_pname then - do_container_access ~is_write:false ret_base callee_pname actuals loc analysis_data astate + Domain.add_container_access tenv formals ~is_write:false ret_base callee_pname actuals loc + astate else do_proc_call ret_base callee_pname actuals call_flags loc analysis_data astate | Call (_, Indirect _, _, _, _) -> if Procname.is_java (Procdesc.get_proc_name proc_desc) then diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index c97c4b5e0..9627512ea 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -8,8 +8,25 @@ open! IStd module AccessExpression = HilExp.AccessExpression module F = Format +module L = Logging module MF = MarkupFormatter +let rec accexp_of_hilexp hil_exp = + match (hil_exp : HilExp.t) with + | AccessExpression access_expr -> + Some access_expr + | Cast (_, e) | Exception e -> + accexp_of_hilexp e + | _ -> + None + + +let accexp_of_first_hilexp actuals = List.hd actuals |> Option.bind ~f:accexp_of_hilexp + +let apply_to_first_actual actuals astate ~f = + accexp_of_first_hilexp actuals |> Option.value_map ~default:astate ~f + + let pp_exp fmt exp = match !Language.curr_language with | Clang -> @@ -349,8 +366,7 @@ module OwnershipDomain = struct get_owned prefix astate ) - let rec ownership_of_expr expr ownership = - let open HilExp in + let rec ownership_of_expr (expr : HilExp.t) ownership = match expr with | AccessExpression access_expr -> get_owned access_expr ownership @@ -544,20 +560,13 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map} = let add_unannotated_call_access formals pname actuals loc (astate : t) = - match actuals with - | [] -> - astate - | receiver_hilexp :: _ -> ( - match HilExp.get_access_exprs receiver_hilexp with - | [] | _ :: _ :: _ -> - (* if no access exps involved, or if more than one (should be impossible), ignore *) - astate - | [receiver] -> - let snapshot = - AccessSnapshot.make_unannotated_call_access formals receiver pname astate.locks - astate.threads Unowned loc - in - {astate with accesses= AccessDomain.add_opt snapshot astate.accesses} ) + apply_to_first_actual actuals astate ~f:(fun receiver -> + let access_opt = + (* FIXME this should use the ownership of the receiver! *) + AccessSnapshot.make_unannotated_call_access formals receiver pname astate.locks + astate.threads Unowned loc + in + {astate with accesses= AccessDomain.add_opt access_opt astate.accesses} ) let astate_to_summary proc_desc formals {threads; locks; accesses; ownership; attribute_map} = @@ -582,3 +591,58 @@ let astate_to_summary proc_desc formals {threads; locks; accesses; ownership; at else AttributeMapDomain.top in {threads; locks; accesses; return_ownership; return_attribute; attributes} + + +let add_access tenv formals loc ~is_write (astate : t) exp = + let rec add_field_accesses prefix_path acc = function + | [] -> + acc + | access :: access_list -> + let prefix_path' = Option.value_exn (AccessExpression.add_access prefix_path access) in + if + (not (HilExp.Access.is_field_or_array_access access)) + || RacerDModels.is_safe_access access prefix_path tenv + then add_field_accesses prefix_path' acc access_list + else + let is_write = is_write && List.is_empty access_list in + let pre = OwnershipDomain.get_owned prefix_path astate.ownership in + let snapshot_opt = + AccessSnapshot.make_access formals prefix_path' ~is_write loc astate.locks + astate.threads pre + in + let access_acc' = AccessDomain.add_opt snapshot_opt acc in + add_field_accesses prefix_path' access_acc' access_list + in + let accesses = + List.fold (HilExp.get_access_exprs exp) ~init:astate.accesses ~f:(fun acc access_expr -> + let base, accesses = AccessExpression.to_accesses access_expr in + add_field_accesses base acc accesses ) + in + {astate with accesses} + + +let add_container_access tenv formals ~is_write ret_base callee_pname actuals loc (astate : t) = + match accexp_of_first_hilexp actuals with + | None -> + L.internal_error "Call to %a is marked as a container access, but has no receiver" Procname.pp + callee_pname ; + astate + | Some receiver_expr + when AttributeMapDomain.is_synchronized astate.attribute_map receiver_expr + || RacerDModels.is_synchronized_container callee_pname receiver_expr tenv -> + astate + | Some receiver_expr -> + let ownership_pre = OwnershipDomain.get_owned receiver_expr astate.ownership in + let callee_access_opt = + AccessSnapshot.make_container_access formals receiver_expr ~is_write callee_pname loc + astate.locks astate.threads ownership_pre + in + let ownership = + OwnershipDomain.add (AccessExpression.base ret_base) ownership_pre astate.ownership + in + let accesses = AccessDomain.add_opt callee_access_opt astate.accesses in + {astate with accesses; ownership} + + +let add_reads_of_hilexps tenv formals exps loc astate = + List.fold exps ~init:astate ~f:(add_access tenv formals loc ~is_write:false) diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index c01409b26..3ead2765a 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -9,6 +9,10 @@ open! IStd module AccessExpression = HilExp.AccessExpression module F = Format +val accexp_of_hilexp : HilExp.t -> HilExp.access_expression option + +val apply_to_first_actual : HilExp.t list -> 'a -> f:(HilExp.access_expression -> 'a) -> 'a + val pp_exp : F.formatter -> AccessExpression.t -> unit (** language sensitive pretty-printer *) @@ -27,7 +31,7 @@ module Access : sig val get_access_exp : t -> AccessExpression.t end -(** Overapproximation of number of time the lock has been acquired *) +(** Overapproximation of number of times the lock has been acquired *) module LockDomain : sig include AbstractDomain.WithBottom @@ -99,27 +103,6 @@ module AccessSnapshot : sig val get_loc : t -> Location.t - val make_access : - FormalMap.t - -> AccessExpression.t - -> is_write:bool - -> Location.t - -> LockDomain.t - -> ThreadsDomain.t - -> OwnershipAbstractValue.t - -> t option - - val make_container_access : - FormalMap.t - -> AccessExpression.t - -> is_write:bool - -> Procname.t - -> Location.t - -> LockDomain.t - -> ThreadsDomain.t - -> OwnershipAbstractValue.t - -> t option - val is_unprotected : t -> bool (** return true if not protected by lock, thread, or ownership *) @@ -148,8 +131,6 @@ module OwnershipDomain : sig val add : AccessExpression.t -> OwnershipAbstractValue.t -> t -> t - val get_owned : AccessExpression.t -> t -> OwnershipAbstractValue.t - val propagate_assignment : AccessExpression.t -> HilExp.t -> t -> t val propagate_return : AccessExpression.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t @@ -175,8 +156,6 @@ module AttributeMapDomain : sig val is_functional : t -> AccessExpression.t -> bool - val is_synchronized : t -> AccessExpression.t -> bool - val propagate_assignment : AccessExpression.t -> HilExp.t -> t -> t (** propagate attributes from the leaves to the root of an RHS Hil expression *) end @@ -210,3 +189,18 @@ val empty_summary : summary val pp_summary : F.formatter -> summary -> unit val astate_to_summary : Procdesc.t -> FormalMap.t -> t -> summary + +val add_access : Tenv.t -> FormalMap.t -> Location.t -> is_write:bool -> t -> HilExp.t -> t + +val add_container_access : + Tenv.t + -> FormalMap.t + -> is_write:bool + -> AccessPath.base + -> Procname.t + -> HilExp.t list + -> Location.t + -> t + -> t + +val add_reads_of_hilexps : Tenv.t -> FormalMap.t -> HilExp.t list -> Location.t -> t -> t