diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index cc464fc8b..95f34d055 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -30,6 +30,9 @@ module Access = struct F.pp_print_string fmt "&" | Dereference -> F.pp_print_string fmt "*" + + + let is_field_or_array_access = function ArrayAccess _ | FieldAccess _ -> true | _ -> false end (** Module where unsafe construction of [access_expression] is allowed. In the rest of the code, and @@ -322,6 +325,52 @@ module AccessExpression = struct init | Sizeof (_, exp_opt) -> fold_vars_exp_opt exp_opt ~init ~f + + + let truncate = function + | Base _ -> + None + | FieldOffset (prefix, fieldname) -> + Some (prefix, Access.FieldAccess fieldname) + | ArrayOffset (prefix, typ, index) -> + Some (prefix, Access.ArrayAccess (typ, index)) + | AddressOf prefix -> + Some (prefix, Access.TakeAddress) + | Dereference prefix -> + Some (prefix, Access.Dereference) + + + let to_accesses exp = + let rec to_accesses_aux acc = function + | Base _ as base -> + (base, acc) + | FieldOffset (prefix, fieldname) -> + to_accesses_aux (Access.FieldAccess fieldname :: acc) prefix + | ArrayOffset (prefix, typ, index) -> + to_accesses_aux (Access.ArrayAccess (typ, index) :: acc) prefix + | AddressOf prefix -> + to_accesses_aux (Access.TakeAddress :: acc) prefix + | Dereference prefix -> + to_accesses_aux (Access.Dereference :: acc) prefix + in + to_accesses_aux [] exp + + + let add_access exp = function + | Access.FieldAccess fieldname -> + Some (field_offset exp fieldname) + | Access.ArrayAccess (typ, index) -> + Some (array_offset exp typ index) + | Access.TakeAddress -> + address_of exp + | Access.Dereference -> + Some (dereference exp) + + + let append ~onto y = + to_accesses y |> snd + |> List.fold ~init:(Some onto) ~f:(fun acc access -> + match acc with None -> acc | Some exp -> add_access exp access ) end let rec get_typ tenv = function diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli index 1f7eb5cae..cbe8be4f6 100644 --- a/infer/src/IR/HilExp.mli +++ b/infer/src/IR/HilExp.mli @@ -17,6 +17,8 @@ module Access : sig [@@deriving compare] val pp : (Format.formatter -> 'array_index -> unit) -> Format.formatter -> 'array_index t -> unit + + val is_field_or_array_access : 'a t -> bool end type t = @@ -60,8 +62,6 @@ module AccessExpression : sig val to_access_path : access_expression -> AccessPath.t - val to_access_paths : access_expression list -> AccessPath.t list - val get_base : access_expression -> AccessPath.base val replace_base : @@ -75,6 +75,19 @@ module AccessExpression : sig val equal : access_expression -> access_expression -> bool + val to_accesses : access_expression -> access_expression * t option Access.t list + (** return the base and a list of accesses equivalent to the input expression *) + + val add_access : access_expression -> t option Access.t -> access_expression option + + val truncate : access_expression -> (access_expression * t option Access.t) option + (** remove and return the prefix and the last access of the expression if it's a base; + otherwise return None *) + + val append : onto:access_expression -> access_expression -> access_expression option + (** [append ~onto y] replaces the base of [y] with [onto] itself; this makes sense if no + [Dereference (AddressOf _)] instances are introduced *) + type nonrec t = access_expression = private | Base of AccessPath.base | FieldOffset of access_expression * Typ.Fieldname.t diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 1460e1245..de93e4a29 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -6,6 +6,7 @@ *) open! IStd +module AccessExpression = HilExp.AccessExpression module F = Format module L = Logging module MF = MarkupFormatter @@ -23,16 +24,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = ProcData.no_extras let add_access loc ~is_write_access locks threads ownership (proc_data : extras ProcData.t) - accesses exp = + access_domain exp = let open Domain in let pdesc = Summary.get_proc_desc proc_data.summary in let rec add_field_accesses prefix_path acc = function | [] -> acc | access :: access_list -> - let prefix_path' = (fst prefix_path, snd prefix_path @ [access]) in - if RacerDModels.is_safe_access access prefix_path proc_data.tenv then - add_field_accesses prefix_path' acc 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 proc_data.tenv + then add_field_accesses prefix_path' acc access_list else let is_write = List.is_empty access_list && is_write_access in let access = TraceElem.make_field_access prefix_path' ~is_write loc in @@ -41,9 +44,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct 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:accesses ~f:(fun acc access_expr -> - let base, accesses = HilExp.AccessExpression.to_access_path access_expr in - add_field_accesses (base, []) acc accesses ) + 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 ret_base callee_pname ~is_write receiver_ap callee_loc tenv @@ -66,7 +69,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> OwnershipAbstractValue.unowned in - let ownership = OwnershipDomain.add (ret_base, []) ownership_value astate.ownership in + let ownership = + OwnershipDomain.add (AccessExpression.base ret_base) ownership_value astate.ownership + in let accesses = AccessDomain.add_opt callee_access astate.accesses in Some {astate with accesses; ownership} @@ -83,32 +88,32 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let open Domain in if AccessDomain.is_empty accesses then accesses else - let rec get_access_path = function + let rec get_access_exp = function | HilExp.AccessExpression access_expr -> - Some (HilExp.AccessExpression.to_access_path access_expr) + Some access_expr | HilExp.Cast (_, e) | HilExp.Exception e -> - get_access_path e + get_access_exp e | _ -> None in let formal_map = FormalMap.make pdesc in - let expand_path ((base, accesses) as path) = - match FormalMap.get_formal_index base formal_map with + let expand_exp exp = + match FormalMap.get_formal_index (AccessExpression.get_base exp) formal_map with | Some formal_index -> ( match List.nth actuals formal_index with | Some actual_exp -> ( - match get_access_path actual_exp with + match get_access_exp actual_exp with | Some actual -> - AccessPath.append actual accesses + AccessExpression.append ~onto:actual exp |> Option.value ~default:exp | None -> - path ) + exp ) | None -> - path ) + exp ) | None -> - path + exp in let add snapshot acc = - let access' = TraceElem.map ~f:expand_path snapshot.AccessSnapshot.access in + let access' = TraceElem.map ~f:expand_exp snapshot.AccessSnapshot.access in let snapshot_opt' = AccessSnapshot.make_from_snapshot access' snapshot in AccessDomain.add_opt snapshot_opt' acc in @@ -125,16 +130,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* the actual is a constant, so it's owned in the caller. *) Conjunction actual_indexes | HilExp.AccessExpression access_expr -> ( - let actual_access_path = HilExp.AccessExpression.to_access_path access_expr in - match OwnershipDomain.get_owned actual_access_path caller_astate.ownership with - | OwnedIf formal_indexes -> - (* access path conditionally owned if [formal_indexes] are owned *) - Conjunction (IntSet.union formal_indexes actual_indexes) - | Unowned -> - (* access path not rooted in a formal and not conditionally owned *) - False ) + match OwnershipDomain.get_owned access_expr caller_astate.ownership with + | OwnedIf formal_indexes -> + (* conditionally owned if [formal_indexes] are owned *) + Conjunction (IntSet.union formal_indexes actual_indexes) + | Unowned -> + (* not rooted in a formal and not conditionally owned *) + False ) | _ -> - (* couldn't find access path, don't know if it's owned. assume not *) + (* couldn't find access expr, don't know if it's owned. assume not *) False in let update_ownership_precondition actual_index (acc : AccessSnapshot.OwnershipPrecondition.t) = @@ -174,7 +178,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses - let call_without_summary callee_pname ret_access_path call_flags actuals astate = + let call_without_summary callee_pname ret_base call_flags actuals astate = let open RacerDModels in let open RacerDDomain in let should_assume_returns_ownership (call_flags : CallFlags.t) actuals = @@ -186,7 +190,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (Procdesc.get_attributes callee_pdesc).ProcAttributes.is_abstract && match Procdesc.get_formals callee_pdesc with - | [(_, typ)] when Typ.equal typ (ret_access_path |> fst |> snd) -> + | [(_, typ)] when Typ.equal typ (snd ret_base) -> true | _ -> false ) @@ -194,11 +198,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct if is_box callee_pname then match actuals with | HilExp.AccessExpression actual_access_expr :: _ -> - let actual_ap = HilExp.AccessExpression.to_access_path actual_access_expr in - if AttributeMapDomain.has_attribute actual_ap Functional astate.attribute_map then + if AttributeMapDomain.has_attribute actual_access_expr Functional astate.attribute_map + then (* TODO: check for constants, which are functional? *) let attribute_map = - AttributeMapDomain.add_attribute ret_access_path Functional astate.attribute_map + AttributeMapDomain.add_attribute (AccessExpression.base ret_base) Functional + astate.attribute_map in {astate with attribute_map} else astate @@ -207,14 +212,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else if should_assume_returns_ownership call_flags actuals then (* assume non-interface methods with no summary and no parameters return ownership *) let ownership = - OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned astate.ownership + OwnershipDomain.add (AccessExpression.base ret_base) OwnershipAbstractValue.owned + astate.ownership in {astate with ownership} else if is_abstract_getthis_like callee_pname then (* assume abstract, single-parameter methods whose return type is equal to that of the first formal return conditional ownership -- an example is getThis in Litho *) let ownership = - OwnershipDomain.add ret_access_path + OwnershipDomain.add (AccessExpression.base ret_base) (OwnershipAbstractValue.make_owned_if 0) astate.ownership in @@ -228,7 +234,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct if RacerDModels.acquires_ownership procname tenv then let astate = add_reads actuals loc astate proc_data in let ownership = - OwnershipDomain.add (ret_base, []) OwnershipAbstractValue.owned astate.ownership + OwnershipDomain.add (AccessExpression.base ret_base) OwnershipAbstractValue.owned + astate.ownership in Some {astate with ownership} else None @@ -240,11 +247,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Option.bind (get_container_access callee_pname tenv) ~f:(fun container_access -> match List.hd actuals with | Some (HilExp.AccessExpression receiver_expr) -> - let receiver_ap = HilExp.AccessExpression.to_access_path receiver_expr in let is_write = match container_access with ContainerWrite -> true | ContainerRead -> false in - make_container_access ret_base callee_pname ~is_write receiver_ap loc tenv + make_container_access ret_base callee_pname ~is_write receiver_expr loc tenv (Summary.get_proc_desc summary) astate | _ -> L.internal_error "Call to %a is marked as a container write, but has no receiver" @@ -258,7 +264,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let open RacerDModels in let open ConcurrencyModels in let pdesc = Summary.get_proc_desc summary in - let ret_access_path = (ret_base, []) in + let ret_access_exp = AccessExpression.base ret_base in let astate = if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then Domain.add_unannotated_call_access callee_pname loc pdesc astate @@ -272,7 +278,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with threads= ThreadsDomain.AnyThreadButSelf} | MainThreadIfTrue -> let attribute_map = - AttributeMapDomain.add_attribute ret_access_path (Choice Choice.OnMainThread) + AttributeMapDomain.add_attribute ret_access_exp (Choice Choice.OnMainThread) astate.attribute_map in {astate with attribute_map} @@ -304,7 +310,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ; threads= update_for_lock_use astate.threads } | LockedIfTrue _ | GuardLockedIfTrue _ -> let attribute_map = - AttributeMapDomain.add_attribute ret_access_path (Choice Choice.LockHeld) + AttributeMapDomain.add_attribute ret_access_exp (Choice Choice.LockHeld) astate.attribute_map in {astate with attribute_map; threads= update_for_lock_use astate.threads} @@ -329,11 +335,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_callee_accesses astate accesses locks threads actuals callee_pname pdesc loc in let ownership = - OwnershipDomain.propagate_return ret_access_path return_ownership actuals + OwnershipDomain.propagate_return ret_access_exp return_ownership actuals astate.ownership in let attribute_map = - AttributeMapDomain.add ret_access_path return_attributes astate.attribute_map + AttributeMapDomain.add ret_access_exp return_attributes astate.attribute_map in let threads = ThreadsDomain.integrate_summary ~caller_astate:astate.threads @@ -341,11 +347,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in {locks; threads; accesses; ownership; attribute_map} | None -> - call_without_summary callee_pname ret_access_path call_flags actuals astate ) + call_without_summary callee_pname ret_base call_flags actuals astate ) in let add_if_annotated predicate attribute attribute_map = if PatternMatch.override_exists predicate tenv callee_pname then - AttributeMapDomain.add_attribute ret_access_path attribute attribute_map + AttributeMapDomain.add_attribute ret_access_exp attribute attribute_map else attribute_map in let attribute_map = add_if_annotated is_functional Functional astate_callee.attribute_map in @@ -354,29 +360,25 @@ module TransferFunctions (CFG : ProcCfg.S) = struct PatternMatch.override_exists (has_return_annot Annotations.ia_is_returns_ownership) tenv callee_pname - then OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned astate_callee.ownership + then OwnershipDomain.add ret_access_exp OwnershipAbstractValue.owned astate_callee.ownership else astate_callee.ownership in {astate_callee with ownership; attribute_map} - let do_assignment lhs_access_expr rhs_exp loc ({ProcData.tenv} as proc_data) (astate : Domain.t) - = + let do_assignment lhs_access_exp rhs_exp loc ({ProcData.tenv} as proc_data) (astate : Domain.t) = let open Domain in - let lhs_access_path = HilExp.AccessExpression.to_access_path lhs_access_expr in let rhs_accesses = add_access loc ~is_write_access:false astate.locks astate.threads astate.ownership proc_data astate.accesses rhs_exp in - let rhs_access_paths = - HilExp.AccessExpression.to_access_paths (HilExp.get_access_exprs rhs_exp) - in + let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in let is_functional = - (not (List.is_empty rhs_access_paths)) - && List.for_all rhs_access_paths ~f:(fun access_path -> - AttributeMapDomain.has_attribute access_path Functional astate.attribute_map ) + (not (List.is_empty rhs_access_exprs)) + && List.for_all rhs_access_exprs ~f:(fun access_exp -> + AttributeMapDomain.has_attribute access_exp Functional astate.attribute_map ) && - match AccessPath.get_typ lhs_access_path tenv with + match AccessExpression.get_typ lhs_access_exp tenv with | Some {Typ.desc= Typ.Tint ILong | Tfloat FDouble} -> (* writes to longs and doubles are not guaranteed to be atomic in Java (http://docs.oracle.com/javase/specs/jls/se7/html/jls-17.html#jls-17.7), so there @@ -392,13 +394,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct rhs_accesses else add_access loc ~is_write_access:true astate.locks astate.threads astate.ownership proc_data - rhs_accesses (HilExp.AccessExpression lhs_access_expr) - in - let ownership = - OwnershipDomain.propagate_assignment lhs_access_path rhs_exp astate.ownership + rhs_accesses (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_path rhs_exp astate.attribute_map + AttributeMapDomain.propagate_assignment lhs_access_exp rhs_exp astate.attribute_map in {astate with accesses; ownership; attribute_map} @@ -416,8 +416,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct evaluating it *) and eval_bexp var = function | HilExp.AccessExpression access_expr -> - if AccessPath.equal (HilExp.AccessExpression.to_access_path access_expr) var then Some true - else None + if AccessExpression.equal access_expr var then Some true else None | HilExp.Constant c -> Some (not (Const.iszero_int_float c)) | HilExp.UnaryOperator (Unop.LNot, e, _) -> @@ -458,10 +457,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let astate' = match HilExp.get_access_exprs assume_exp with | [access_expr] -> - let access_path = HilExp.AccessExpression.to_access_path access_expr in - eval_bexp access_path assume_exp + eval_bexp access_expr assume_exp |> Option.fold ~init:astate ~f:(fun init bool_value -> - let choices = AttributeMapDomain.get_choices access_path astate.attribute_map in + let choices = AttributeMapDomain.get_choices access_expr astate.attribute_map in (* 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 *) List.fold ~f:(add_choice bool_value) ~init choices ) @@ -525,7 +523,7 @@ let analyze_procedure {Callbacks.exe_env; summary} = let add_owned_local acc (var_data : ProcAttributes.var_data) = let pvar = Pvar.mk var_data.name proc_name in let base = AccessPath.base_of_pvar pvar var_data.typ in - OwnershipDomain.add (base, []) OwnershipAbstractValue.owned acc + OwnershipDomain.add (AccessExpression.base base) OwnershipAbstractValue.owned acc in (* Add ownership to local variables. In cpp, stack-allocated local variables cannot be raced on as every thread has its own stack. @@ -543,13 +541,13 @@ let analyze_procedure {Callbacks.exe_env; summary} = OwnershipAbstractValue.owned else OwnershipAbstractValue.make_owned_if formal_index in - OwnershipDomain.add (formal, []) ownership_value acc + OwnershipDomain.add (AccessExpression.base formal) ownership_value acc in if is_initializer tenv proc_name then let add_owned_formal acc formal_index = match FormalMap.get_formal_base formal_index formal_map with | Some base -> - OwnershipDomain.add (base, []) OwnershipAbstractValue.owned acc + OwnershipDomain.add (AccessExpression.base base) OwnershipAbstractValue.owned acc | None -> acc in @@ -579,12 +577,13 @@ let analyze_procedure {Callbacks.exe_env; summary} = in match Analyzer.compute_post proc_data ~initial with | Some {threads; locks; accesses; ownership; attribute_map} -> - let return_var_ap = - AccessPath.of_pvar (Pvar.get_ret_pvar proc_name) (Procdesc.get_ret_type proc_desc) + let return_var_exp = + AccessExpression.base + (Var.of_pvar (Pvar.get_ret_pvar proc_name), Procdesc.get_ret_type proc_desc) in - let return_ownership = OwnershipDomain.get_owned return_var_ap ownership in + let return_ownership = OwnershipDomain.get_owned return_var_exp ownership in let return_attributes = - try AttributeMapDomain.find return_var_ap attribute_map + try AttributeMapDomain.find return_var_exp attribute_map with Caml.Not_found -> AttributeSetDomain.empty in let post = {threads; locks; accesses; return_ownership; return_attributes} in @@ -675,27 +674,27 @@ let get_reporting_explanation report_kind tenv pname thread = else get_reporting_explanation_cpp -let pp_container_access fmt (access_path, access_pname) = +let pp_container_access fmt (access_exp, access_pname) = F.fprintf fmt "container %a via call to %s" (MF.wrap_monospaced AccessPath.pp) - access_path + (AccessExpression.to_access_path access_exp) (MF.monospaced_to_string (Typ.Procname.get_method access_pname)) let pp_access fmt (t : RacerDDomain.TraceElem.t) = match t.elem with - | Read {path} | Write {path} -> - (MF.wrap_monospaced AccessPath.pp) fmt path - | ContainerRead {path; pname} | ContainerWrite {path; pname} -> - pp_container_access fmt (path, pname) + | Read {exp} | Write {exp} -> + (MF.wrap_monospaced AccessPath.pp) fmt (AccessExpression.to_access_path exp) + | ContainerRead {exp; pname} | ContainerWrite {exp; pname} -> + pp_container_access fmt (exp, pname) | InterfaceCall _ as access -> RacerDDomain.Access.pp fmt access -let make_trace ~report_kind original_path = +let make_trace ~report_kind original_exp = let open RacerDDomain in let loc_trace_of_path path = TraceElem.make_loc_trace path in - let original_trace = loc_trace_of_path original_path in + let original_trace = loc_trace_of_path original_exp in let get_end_loc trace = Option.map (List.last trace) ~f:(function {Errlog.lt_loc} -> lt_loc) in let original_end = get_end_loc original_trace in let make_with_conflicts conflict_sink original_trace ~label1 ~label2 = @@ -820,17 +819,18 @@ let empty_reported = {reported_sites; reported_reads; reported_writes; reported_unannotated_calls} -(* decide if we should throw away a path before doing safety analysis +(* decide if we should throw away an access before doing safety analysis for now, just check for whether the access is within a switch-map that is auto-generated by Java. *) -let should_filter_access path_opt = +let should_filter_access exp_opt = let check_access = function - | AccessPath.ArrayAccess _ -> - false - | AccessPath.FieldAccess fld -> + | HilExp.Access.FieldAccess fld -> String.is_substring ~substring:"$SwitchMap" (Typ.Fieldname.to_string fld) + | _ -> + false in - Option.exists path_opt ~f:(fun (_, path) -> List.exists path ~f:check_access) + Option.exists exp_opt ~f:(fun exp -> + AccessExpression.to_accesses exp |> snd |> List.exists ~f:check_access ) (** @@ -868,10 +868,10 @@ end = struct let of_access (access : RacerDDomain.Access.t) = match access with - | Read {path} | Write {path} -> - Location path - | ContainerRead {path} | ContainerWrite {path} -> - Container path + | Read {exp} | Write {exp} -> + Location (AccessExpression.to_access_path exp) + | ContainerRead {exp} | ContainerWrite {exp} -> + Container (AccessExpression.to_access_path exp) | InterfaceCall pn -> Call pn end @@ -884,7 +884,7 @@ end = struct let add (rep : reported_access) map = let access = rep.snapshot.access.elem in - if RacerDDomain.Access.get_access_path access |> should_filter_access then map + if RacerDDomain.Access.get_access_exp access |> should_filter_access then map else let k = Key.of_access access in M.update k (function None -> Some [rep] | Some reps -> Some (rep :: reps)) map @@ -944,8 +944,13 @@ let should_report_guardedby_violation classname_str ({snapshot; tenv; procdesc} && Procdesc.get_proc_name procdesc |> Typ.Procname.is_java && (* restrict check to access paths of length one *) - match RacerDDomain.Access.get_access_path snapshot.access.elem with - | Some ((_, base_type), [AccessPath.FieldAccess field_name]) -> ( + match + RacerDDomain.Access.get_access_exp snapshot.access.elem + |> Option.map ~f:AccessExpression.to_accesses + |> Option.map ~f:(fun (base, accesses) -> + (base, List.filter accesses ~f:HilExp.Access.is_field_or_array_access) ) + with + | Some (AccessExpression.Base (_, base_type), [HilExp.Access.FieldAccess field_name]) -> ( match base_type.desc with | Tstruct base_name | Tptr ({desc= Tstruct base_name}, _) -> (* is the base class a subclass of the one containing the GuardedBy annotation? *) diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 0fa99ce23..6fadd9e82 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -6,11 +6,12 @@ *) open! IStd +module AccessExpression = HilExp.AccessExpression module F = Format module MF = MarkupFormatter (** Master function for deciding whether RacerD should completely ignore a variable as the root - of an access path. Currently fires on *static locals* and any variable which does not + of an access expression. Currently fires on *static locals* and any variable which does not appear in source code (eg, temporary variables and frontend introduced variables). This is because currently reports on these variables would not be easily actionable. @@ -22,17 +23,17 @@ let should_skip_var v = module Access = struct type t = - | Read of {path: AccessPath.t} - | Write of {path: AccessPath.t} - | ContainerRead of {path: AccessPath.t; pname: Typ.Procname.t} - | ContainerWrite of {path: AccessPath.t; pname: Typ.Procname.t} + | Read of {exp: AccessExpression.t} + | Write of {exp: AccessExpression.t} + | ContainerRead of {exp: AccessExpression.t; pname: Typ.Procname.t} + | ContainerWrite of {exp: AccessExpression.t; pname: Typ.Procname.t} | InterfaceCall of Typ.Procname.t [@@deriving compare] - let make_field_access path ~is_write = if is_write then Write {path} else Read {path} + let make_field_access exp ~is_write = if is_write then Write {exp} else Read {exp} - let make_container_access path pname ~is_write = - if is_write then ContainerWrite {path; pname} else ContainerRead {path; pname} + let make_container_access exp pname ~is_write = + if is_write then ContainerWrite {exp; pname} else ContainerRead {exp; pname} let is_write = function @@ -49,56 +50,56 @@ module Access = struct true - let get_access_path = function - | Read {path} | Write {path} | ContainerWrite {path} | ContainerRead {path} -> - Some path + let get_access_exp = function + | Read {exp} | Write {exp} | ContainerWrite {exp} | ContainerRead {exp} -> + Some exp | InterfaceCall _ -> None let map ~f access = match access with - | Read {path} -> - let path' = f path in - if phys_equal path path' then access else Read {path= path'} - | Write {path} -> - let path' = f path in - if phys_equal path path' then access else Write {path= path'} - | ContainerWrite ({path} as record) -> - let path' = f path in - if phys_equal path path' then access else ContainerWrite {record with path= path'} - | ContainerRead ({path} as record) -> - let path' = f path in - if phys_equal path path' then access else ContainerRead {record with path= path'} + | Read {exp} -> + let exp' = f exp in + if phys_equal exp exp' then access else Read {exp= exp'} + | Write {exp} -> + let exp' = f exp in + if phys_equal exp exp' then access else Write {exp= exp'} + | ContainerWrite ({exp} as record) -> + let exp' = f exp in + if phys_equal exp exp' then access else ContainerWrite {record with exp= exp'} + | ContainerRead ({exp} as record) -> + let exp' = f exp in + if phys_equal exp exp' then access else ContainerRead {record with exp= exp'} | InterfaceCall _ as intfcall -> intfcall let pp fmt = function - | Read {path} -> - F.fprintf fmt "Read of %a" AccessPath.pp path - | Write {path} -> - F.fprintf fmt "Write to %a" AccessPath.pp path - | ContainerRead {path; pname} -> - F.fprintf fmt "Read of container %a via %a" AccessPath.pp path Typ.Procname.pp pname - | ContainerWrite {path; pname} -> - F.fprintf fmt "Write to container %a via %a" AccessPath.pp path Typ.Procname.pp pname + | Read {exp} -> + F.fprintf fmt "Read of %a" AccessExpression.pp exp + | Write {exp} -> + F.fprintf fmt "Write to %a" AccessExpression.pp exp + | ContainerRead {exp; pname} -> + F.fprintf fmt "Read of container %a via %a" AccessExpression.pp exp Typ.Procname.pp pname + | ContainerWrite {exp; pname} -> + F.fprintf fmt "Write to container %a via %a" AccessExpression.pp exp Typ.Procname.pp pname | InterfaceCall pname -> F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp pname let pp_human fmt = function - | Read {path} | Write {path} -> - F.fprintf fmt "access to `%a`" AccessPath.pp path - | ContainerRead {path; pname} -> + | Read {exp} | Write {exp} -> + F.fprintf fmt "access to `%a`" AccessPath.pp (AccessExpression.to_access_path exp) + | ContainerRead {exp; pname} -> F.fprintf fmt "Read of container %a via call to %s" (MF.wrap_monospaced AccessPath.pp) - path + (AccessExpression.to_access_path exp) (MF.monospaced_to_string (Typ.Procname.get_method pname)) - | ContainerWrite {path; pname} -> + | ContainerWrite {exp; pname} -> F.fprintf fmt "Write to container %a via call to %s" (MF.wrap_monospaced AccessPath.pp) - path + (AccessExpression.to_access_path exp) (MF.monospaced_to_string (Typ.Procname.get_method pname)) | InterfaceCall pname -> F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp pname @@ -119,12 +120,12 @@ module TraceElem = struct let map ~f trace_elem = map ~f:(Access.map ~f) trace_elem - let make_container_access access_path pname ~is_write loc = - make (Access.make_container_access access_path pname ~is_write) loc + let make_container_access access_exp pname ~is_write loc = + make (Access.make_container_access access_exp pname ~is_write) loc - let make_field_access access_path ~is_write loc = - make (Access.make_field_access access_path ~is_write) loc + let make_field_access access_exp ~is_write loc = + make (Access.make_field_access access_exp ~is_write) loc let make_unannotated_call_access pname loc = make (Access.InterfaceCall pname) loc @@ -290,7 +291,8 @@ module AccessDomain = struct let add ({AccessSnapshot.access= {elem}} as s) astate = let skip = - Access.get_access_path elem |> Option.exists ~f:(fun ((v, _), _) -> should_skip_var v) + Access.get_access_exp elem + |> Option.exists ~f:(fun exp -> AccessExpression.get_base exp |> fst |> should_skip_var) in if skip then astate else add s astate @@ -344,32 +346,32 @@ module OwnershipAbstractValue = struct end module OwnershipDomain = struct - include AbstractDomain.Map (AccessPath) (OwnershipAbstractValue) + include AbstractDomain.Map (AccessExpression) (OwnershipAbstractValue) (* return the first non-Unowned ownership value found when checking progressively shorter - prefixes of [access_path] *) - let rec get_owned access_path astate = - let keep_looking access_path astate = - match AccessPath.truncate access_path with - | access_path', Some _ -> - get_owned access_path' astate - | _ -> + prefixes of [access_exp] *) + let rec get_owned access_exp astate = + let keep_looking (access_exp : AccessExpression.t) astate = + match AccessExpression.truncate access_exp with + | Some (prefix_exp, _) -> + get_owned prefix_exp astate + | None -> OwnershipAbstractValue.Unowned in - match find access_path astate with + match find access_exp astate with | OwnershipAbstractValue.OwnedIf _ as v -> v | OwnershipAbstractValue.Unowned -> - keep_looking access_path astate + keep_looking access_exp astate | exception Caml.Not_found -> - keep_looking access_path astate + keep_looking access_exp astate let rec ownership_of_expr expr ownership = let open HilExp in match expr with | AccessExpression access_expr -> - get_owned (AccessExpression.to_access_path access_expr) ownership + get_owned access_expr ownership | Constant _ -> OwnershipAbstractValue.owned | Exception e (* treat exceptions as transparent wrt ownership *) | Cast (_, e) -> @@ -378,16 +380,16 @@ module OwnershipDomain = struct OwnershipAbstractValue.unowned - let propagate_assignment ((lhs_root, _) as lhs_access_path) rhs_exp ownership = - if Var.is_global (fst lhs_root) then - (* do not assign ownership to access paths rooted at globals *) + let propagate_assignment lhs_access_exp rhs_exp ownership = + if AccessExpression.get_base lhs_access_exp |> fst |> Var.is_global then + (* do not assign ownership to access expressions rooted at globals *) ownership else let rhs_ownership_value = ownership_of_expr rhs_exp ownership in - add lhs_access_path rhs_ownership_value ownership + add lhs_access_exp rhs_ownership_value ownership - let propagate_return ret_access_path return_ownership actuals ownership = + let propagate_return ret_access_exp return_ownership actuals ownership = let get_ownership formal_index init = List.nth actuals formal_index (* simply skip formal if we cannot find its actual, as opposed to assuming non-ownership *) @@ -401,16 +403,16 @@ module OwnershipDomain = struct | OwnershipAbstractValue.OwnedIf formal_indexes -> IntSet.fold get_ownership formal_indexes OwnershipAbstractValue.owned in - add ret_access_path ret_ownership_wrt_actuals ownership + add ret_access_exp ret_ownership_wrt_actuals ownership - let get_precondition path t = - match get_owned path t with + let get_precondition exp t = + match get_owned exp t with | OwnedIf formal_indexes -> - (* access path conditionally owned if [formal_indexes] are owned *) + (* access expression conditionally owned if [formal_indexes] are owned *) AccessSnapshot.OwnershipPrecondition.Conjunction formal_indexes | Unowned -> - (* access path not rooted in a formal and not conditionally owned *) + (* access expression not rooted in a formal and not conditionally owned *) AccessSnapshot.OwnershipPrecondition.False end @@ -437,27 +439,27 @@ end module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute) module AttributeMapDomain = struct - include AbstractDomain.InvertedMap (AccessPath) (AttributeSetDomain) + include AbstractDomain.InvertedMap (AccessExpression) (AttributeSetDomain) - let add access_path attribute_set t = - if AttributeSetDomain.is_empty attribute_set then t else add access_path attribute_set t + let add access_expression attribute_set t = + if AttributeSetDomain.is_empty attribute_set then t else add access_expression attribute_set t - let has_attribute access_path attribute t = - try find access_path t |> AttributeSetDomain.mem attribute with Caml.Not_found -> false + let has_attribute access_expression attribute t = + try find access_expression t |> AttributeSetDomain.mem attribute with Caml.Not_found -> false - let get_choices access_path t = + let get_choices access_expression t = try - let attributes = find access_path t in + let attributes = find access_expression t in AttributeSetDomain.fold (fun cc acc -> match cc with Attribute.Choice c -> c :: acc | _ -> acc) attributes [] with Caml.Not_found -> [] - let add_attribute access_path attribute t = - update access_path + let add_attribute access_expression attribute t = + update access_expression (function | Some attrs -> Some (AttributeSetDomain.add attribute attrs) @@ -466,12 +468,10 @@ module AttributeMapDomain = struct t - let rec attributes_of_expr attribute_map e = - let open HilExp in + let rec attributes_of_expr attribute_map (e : HilExp.t) = match e with - | HilExp.AccessExpression access_expr -> ( - try find (AccessExpression.to_access_path access_expr) attribute_map - with Caml.Not_found -> AttributeSetDomain.empty ) + | AccessExpression access_expr -> ( + try find access_expr attribute_map with Caml.Not_found -> AttributeSetDomain.empty ) | Constant _ -> AttributeSetDomain.singleton Attribute.Functional | Exception expr (* treat exceptions as transparent wrt attributes *) | Cast (_, expr) -> @@ -486,9 +486,9 @@ module AttributeMapDomain = struct AttributeSetDomain.empty - let propagate_assignment lhs_access_path rhs_exp attribute_map = + let propagate_assignment lhs_access_expression rhs_exp attribute_map = let rhs_attributes = attributes_of_expr attribute_map rhs_exp in - add lhs_access_path rhs_attributes attribute_map + add lhs_access_expression rhs_attributes attribute_map end type t = diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 5e71b17fa..bcb5e5d66 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -6,14 +6,16 @@ *) open! IStd +module AccessExpression = HilExp.AccessExpression module F = Format module Access : sig type t = - | Read of {path: AccessPath.t} (** Field or array read *) - | Write of {path: AccessPath.t} (** Field or array write *) - | ContainerRead of {path: AccessPath.t; pname: Typ.Procname.t} (** Read of container object *) - | ContainerWrite of {path: AccessPath.t; pname: Typ.Procname.t} + | Read of {exp: AccessExpression.t} (** Field or array read *) + | Write of {exp: AccessExpression.t} (** Field or array write *) + | ContainerRead of {exp: AccessExpression.t; pname: Typ.Procname.t} + (** Read of container object *) + | ContainerWrite of {exp: AccessExpression.t; pname: Typ.Procname.t} (** Write to container object *) | InterfaceCall of Typ.Procname.t (** Call to method of interface not annotated with @ThreadSafe *) @@ -21,7 +23,7 @@ module Access : sig include ExplicitTrace.Element with type t := t - val get_access_path : t -> AccessPath.t option + val get_access_exp : t -> AccessExpression.t option end module TraceElem : sig @@ -32,11 +34,12 @@ module TraceElem : sig val is_container_write : t -> bool - val map : f:(AccessPath.t -> AccessPath.t) -> t -> t + val map : f:(AccessExpression.t -> AccessExpression.t) -> t -> t - val make_container_access : AccessPath.t -> Typ.Procname.t -> is_write:bool -> Location.t -> t + val make_container_access : + AccessExpression.t -> Typ.Procname.t -> is_write:bool -> Location.t -> t - val make_field_access : AccessPath.t -> is_write:bool -> Location.t -> t + val make_field_access : AccessExpression.t -> is_write:bool -> Location.t -> t end (** Overapproximation of number of locks that are currently held *) @@ -143,15 +146,15 @@ module OwnershipDomain : sig val empty : t - val add : AccessPath.t -> OwnershipAbstractValue.t -> t -> t + val add : AccessExpression.t -> OwnershipAbstractValue.t -> t -> t - val get_owned : AccessPath.t -> t -> OwnershipAbstractValue.t + val get_owned : AccessExpression.t -> t -> OwnershipAbstractValue.t - val propagate_assignment : AccessPath.t -> HilExp.t -> t -> t + val propagate_assignment : AccessExpression.t -> HilExp.t -> t -> t - val propagate_return : AccessPath.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t + val propagate_return : AccessExpression.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t - val get_precondition : AccessPath.t -> t -> AccessSnapshot.OwnershipPrecondition.t + val get_precondition : AccessExpression.t -> t -> AccessSnapshot.OwnershipPrecondition.t end (** attribute attached to a boolean variable specifying what it means when the boolean is true *) @@ -180,18 +183,18 @@ end module AttributeMapDomain : sig type t - val find : AccessPath.t -> t -> AttributeSetDomain.t + val find : AccessExpression.t -> t -> AttributeSetDomain.t - val add : AccessPath.t -> AttributeSetDomain.t -> t -> t + val add : AccessExpression.t -> AttributeSetDomain.t -> t -> t - val has_attribute : AccessPath.t -> Attribute.t -> t -> bool + val has_attribute : AccessExpression.t -> Attribute.t -> t -> bool - val get_choices : AccessPath.t -> t -> Choice.t list + val get_choices : AccessExpression.t -> t -> Choice.t list (** get the choice attributes associated with the given access path *) - val add_attribute : AccessPath.t -> Attribute.t -> t -> t + val add_attribute : AccessExpression.t -> Attribute.t -> t -> t - val propagate_assignment : AccessPath.t -> HilExp.t -> t -> t + val propagate_assignment : AccessExpression.t -> HilExp.t -> t -> t (** propagate attributes from the leaves to the root of an RHS Hil expression *) end diff --git a/infer/src/concurrency/RacerDModels.ml b/infer/src/concurrency/RacerDModels.ml index 4a72cfb4e..693aecec8 100644 --- a/infer/src/concurrency/RacerDModels.ml +++ b/infer/src/concurrency/RacerDModels.ml @@ -353,9 +353,9 @@ let is_marked_thread_safe pdesc tenv = is_thread_safe_class pname tenv || is_thread_safe_method pname tenv -let is_safe_access access prefix_path tenv = - match (access, AccessPath.get_typ prefix_path tenv) with - | ( AccessPath.FieldAccess fieldname +let is_safe_access (access : 'a HilExp.Access.t) prefix_exp tenv = + match (access, HilExp.AccessExpression.get_typ prefix_exp tenv) with + | ( HilExp.Access.FieldAccess fieldname , Some ({Typ.desc= Tstruct typename} | {desc= Tptr ({desc= Tstruct typename}, _)}) ) -> ( match Tenv.lookup tenv typename with | Some struct_typ -> @@ -386,11 +386,10 @@ let should_flag_interface_call tenv exps call_flags pname = let receiver_is_not_safe exps tenv = List.hd exps |> Option.bind ~f:(fun exp -> HilExp.get_access_exprs exp |> List.hd) - |> Option.map ~f:HilExp.AccessExpression.to_access_path - |> Option.map ~f:AccessPath.truncate + |> Option.map ~f:HilExp.AccessExpression.truncate |> Option.exists ~f:(function - | receiver_prefix, Some receiver_field -> - not (is_safe_access receiver_field receiver_prefix tenv) + | Some (receiver_prefix, receiver_access) -> + not (is_safe_access receiver_access receiver_prefix tenv) | _ -> true ) in @@ -404,7 +403,7 @@ let should_flag_interface_call tenv exps call_flags pname = call_flags.CallFlags.cf_interface && (not (is_java_library java_pname)) && (not (is_builder_function java_pname)) - (* can't ask anyone to annotate interfaces in library code, and Builder's should always be + (* can't ask anyone to annotate interfaces in library code, and Builders should always be thread-safe (would be unreasonable to ask everyone to annotate them) *) && (not (PatternMatch.check_class_attributes thread_safe_or_thread_confined tenv pname)) && (not (has_return_annot thread_safe_or_thread_confined pname)) @@ -414,7 +413,7 @@ let should_flag_interface_call tenv exps call_flags pname = false -let is_synchronized_container callee_pname ((_, (base_typ : Typ.t)), accesses) tenv = +let is_synchronized_container callee_pname (access_exp : HilExp.AccessExpression.t) tenv = let is_threadsafe_collection pn tenv = match pn with | Typ.Procname.Java java_pname -> @@ -443,13 +442,18 @@ let is_synchronized_container callee_pname ((_, (base_typ : Typ.t)), accesses) t | None -> false in - match List.rev accesses with - | AccessPath.FieldAccess base_field :: AccessPath.FieldAccess container_field :: _ + let open HilExp in + match + AccessExpression.to_accesses access_exp + |> snd + |> List.rev_filter ~f:Access.is_field_or_array_access + with + | Access.FieldAccess base_field :: Access.FieldAccess container_field :: _ when Typ.Procname.is_java callee_pname -> let base_typename = Typ.Name.Java.from_string (Typ.Fieldname.Java.get_class base_field) in is_annotated_synchronized base_typename container_field tenv - | [AccessPath.FieldAccess container_field] -> ( - match base_typ.desc with + | [Access.FieldAccess container_field] -> ( + match (AccessExpression.get_base access_exp |> snd).desc with | Typ.Tstruct base_typename | Tptr ({Typ.desc= Tstruct base_typename}, _) -> is_annotated_synchronized base_typename container_field tenv | _ -> diff --git a/infer/src/concurrency/RacerDModels.mli b/infer/src/concurrency/RacerDModels.mli index a69245d7d..b4cda84e8 100644 --- a/infer/src/concurrency/RacerDModels.mli +++ b/infer/src/concurrency/RacerDModels.mli @@ -44,11 +44,11 @@ val is_thread_safe_method : Typ.Procname.t -> Tenv.t -> bool val is_marked_thread_safe : Procdesc.t -> Tenv.t -> bool -val is_safe_access : AccessPath.access -> AccessPath.t -> Tenv.t -> bool +val is_safe_access : 'a HilExp.Access.t -> HilExp.AccessExpression.t -> Tenv.t -> bool (** check if an access to a field is thread-confined, or whether the field is volatile *) val should_flag_interface_call : Tenv.t -> HilExp.t list -> CallFlags.t -> Typ.Procname.t -> bool (** should an interface call be flagged as potentially non-thread safe? *) -val is_synchronized_container : Typ.Procname.t -> AccessPath.t -> Tenv.t -> bool -(** is a call on an access path to a method of a synchronized container? *) +val is_synchronized_container : Typ.Procname.t -> HilExp.AccessExpression.t -> Tenv.t -> bool +(** is a call on an access expression to a method of a synchronized container? *)