diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 142940d53..de7f6847d 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -38,10 +38,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let is_unlock_procedure pn = Procname.equal pn ModelBuiltins.__delete_locked_attribute let add_path_to_state exp typ pathdomainstate = - match AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None) with - | Some rawpath -> PathDomain.add rawpath pathdomainstate - | None -> pathdomainstate - + IList.fold_left + (fun pathdomainstate_acc rawpath -> PathDomain.add rawpath pathdomainstate_acc) + pathdomainstate + (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None)) let exec_instr ((lockstate,(readstate,writestate)) as astate) { ProcData.pdesc; } _ = let is_unprotected lockstate = diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 5bb656af1..79923170d 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -79,35 +79,50 @@ let of_pvar pvar typ = let of_id id typ = base_of_id id typ, [] -let of_exp exp typ ~(f_resolve_id : Var.t -> raw option) = +let of_exp exp0 typ0 ~(f_resolve_id : Var.t -> raw option) = (* [typ] is the type of the last element of the access path (e.g., typeof(g) for x.f.g) *) - let rec of_exp_ exp typ accesses = + let rec of_exp_ exp typ accesses acc = match exp with | Exp.Var id -> begin match f_resolve_id (Var.of_id id) with - | Some (base, base_accesses) -> Some (base, base_accesses @ accesses) - | None -> Some (base_of_id id typ, accesses) + | Some (base, base_accesses) -> (base, base_accesses @ accesses) :: acc + | None -> (base_of_id id typ, accesses) :: acc end | Exp.Lvar pvar when Pvar.is_frontend_tmp pvar -> begin match f_resolve_id (Var.of_pvar pvar) with - | Some (base, base_accesses) -> Some (base, base_accesses @ accesses) - | None -> Some (base_of_pvar pvar typ, accesses) + | Some (base, base_accesses) -> (base, base_accesses @ accesses) :: acc + | None -> (base_of_pvar pvar typ, accesses) :: acc end | Exp.Lvar pvar -> - Some (base_of_pvar pvar typ, accesses) + (base_of_pvar pvar typ, accesses) :: acc | Exp.Lfield (root_exp, fld, root_exp_typ) -> let field_access = FieldAccess (fld, typ) in - of_exp_ root_exp root_exp_typ (field_access :: accesses) + of_exp_ root_exp root_exp_typ (field_access :: accesses) acc | Exp.Lindex (root_exp, _) -> let array_access = ArrayAccess typ in let array_typ = Typ.Tarray (typ, None) in - of_exp_ root_exp array_typ (array_access :: accesses) - | _ -> - (* trying to make access path from an invalid expression (e.g., a constant) *) - None in - of_exp_ exp typ [] + of_exp_ root_exp array_typ (array_access :: accesses) acc + | Exp.Cast (cast_typ, cast_exp) -> + of_exp_ cast_exp cast_typ [] acc + | Exp.UnOp (_, unop_exp, _) -> + of_exp_ unop_exp typ [] acc + | Exp.Exn exn_exp -> + of_exp_ exn_exp typ [] acc + | Exp.BinOp (_, exp1, exp2) -> + of_exp_ exp1 typ [] acc + |> of_exp_ exp2 typ [] + | Exp.Const _ | Closure _ | Sizeof _ -> + (* trying to make access path from an invalid expression *) + acc in + of_exp_ exp0 typ0 [] [] + +let of_lhs_exp lhs_exp typ ~(f_resolve_id : Var.t -> raw option) = + match of_exp lhs_exp typ ~f_resolve_id with + | [lhs_ap] -> Some lhs_ap + | [] -> None + | _ -> failwithf "Creating lhs access path from invalid access path %a" Exp.pp lhs_exp let append (base, old_accesses) new_accesses = base, old_accesses @ new_accesses diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index 684c4f433..1d8fd179b 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -47,8 +47,11 @@ val of_pvar : Pvar.t -> Typ.t -> raw (** create an access path from an ident *) val of_id : Ident.t -> Typ.t -> raw -(** convert [exp] to a raw access path, resolving identifiers using [f_resolve_id] *) -val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> raw option) -> raw option +(** extract the raw access paths that occur in [exp], resolving identifiers using [f_resolve_id] *) +val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> raw option) -> raw list + +(** convert [lhs_exp] to a raw access path, resolving identifiers using [f_resolve_id] *) +val of_lhs_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> raw option) -> raw option (** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces `x.f.g.h` *) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 26c387afe..fe3e020f9 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -117,7 +117,7 @@ module Make (TaintSpec : TaintSpec.S) = struct (* get the node associated with [exp] in [access_tree] *) let exp_get_node exp typ { Domain.access_tree; id_map; } proc_data loc = let f_resolve_id = resolve_id id_map in - match AccessPath.of_exp exp typ ~f_resolve_id with + match AccessPath.of_lhs_exp exp typ ~f_resolve_id with | Some access_path -> access_path_get_node (AccessPath.Exact access_path) access_tree proc_data loc | None -> @@ -134,7 +134,7 @@ module Make (TaintSpec : TaintSpec.S) = struct let analyze_id_assignment lhs_id rhs_exp rhs_typ ({ Domain.id_map; } as astate) = let f_resolve_id = resolve_id id_map in - match AccessPath.of_exp rhs_exp rhs_typ ~f_resolve_id with + match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with | Some rhs_access_path -> let id_map' = IdMapDomain.add lhs_id rhs_access_path id_map in { astate with Domain.id_map = id_map'; } @@ -151,7 +151,7 @@ module Make (TaintSpec : TaintSpec.S) = struct (* add [sink] to the trace associated with the [formal_num]th actual *) let add_sink_to_actual access_tree_acc (sink_param : TraceDomain.Sink.t Sink.parameter) = let actual_exp, actual_typ = IList.nth actuals sink_param.index in - match AccessPath.of_exp actual_exp actual_typ ~f_resolve_id with + match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with | Some actual_ap_raw -> let actual_ap = let is_array_typ = match actual_typ with @@ -208,7 +208,7 @@ module Make (TaintSpec : TaintSpec.S) = struct let actual_exp, actual_typ = try IList.nth actuals formal_num with Failure _ -> failwithf "Bad formal number %d" formal_num in - AccessPath.of_exp actual_exp actual_typ ~f_resolve_id in + AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id in let project ~formal_ap ~actual_ap = let projected_ap = AccessPath.append actual_ap (snd (AccessPath.extract formal_ap)) in if AccessPath.is_exact formal_ap @@ -269,7 +269,7 @@ module Make (TaintSpec : TaintSpec.S) = struct analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ astate | Sil.Store (lhs_exp, lhs_typ, rhs_exp, loc) -> let lhs_access_path = - match AccessPath.of_exp lhs_exp lhs_typ ~f_resolve_id with + match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id with | Some access_path -> access_path | None -> diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml index bc0d6a033..014fddb9d 100644 --- a/infer/src/unit/accessPathTests.ml +++ b/infer/src/unit/accessPathTests.ml @@ -78,7 +78,7 @@ let tests = let check_make_ap exp expected_ap ~f_resolve_id = let make_ap exp = - match AccessPath.of_exp exp dummy_typ ~f_resolve_id with + match AccessPath.of_lhs_exp exp dummy_typ ~f_resolve_id with | Some ap -> ap | None -> assert false in let actual_ap = make_ap exp in @@ -108,6 +108,14 @@ let tests = let id_exp = Exp.Var (Ident.create_normal (Ident.string_to_name "") 0) in Exp.Lfield (id_exp, g_fieldname, dummy_typ) in check_make_ap xFG_exp_with_id xFG ~f_resolve_id:f_resolve_id_to_xF; + (* make sure we can grab access paths from compound expressions *) + let binop_exp = Exp.le xF_exp xFG_exp in + match AccessPath.of_exp binop_exp dummy_typ ~f_resolve_id with + | [ap1; ap2] -> + assert_equal ~cmp:AccessPath.raw_equal ap1 xFG; + assert_equal ~cmp:AccessPath.raw_equal ap2 xF; + | _ -> + assert false; () in "of_exp">::of_exp_test_ in