diff --git a/infer/src/IR/AccessExpression.ml b/infer/src/IR/AccessExpression.ml index 8c6a6668e..560417855 100644 --- a/infer/src/IR/AccessExpression.ml +++ b/infer/src/IR/AccessExpression.ml @@ -8,32 +8,146 @@ *) open! IStd +module F = Format type t = | Base of AccessPath.base - | Offset of t * AccessPath.access - (* field/array access *) + | FieldOffset of t * Typ.Fieldname.t + | ArrayOffset of t * Typ.t * t list | AddressOf of t - (* address of operator & *) | Dereference of t - (* dereference operator * *) [@@deriving compare] (** convert to an AccessPath.t, ignoring AddressOf and Dereference for now *) let rec to_access_path t = - match t with + let rec to_access_path_ t = + match t with + | Base base -> + (base, []) + | FieldOffset (ae, fld) -> + let base, accesses = to_access_path_ ae in + (base, AccessPath.FieldAccess fld :: accesses) + | ArrayOffset (ae, typ, index_aes) -> + let access_paths = to_access_paths index_aes in + let base, accesses = to_access_path_ ae in + (base, AccessPath.ArrayAccess (typ, access_paths) :: accesses) + | AddressOf ae -> + to_access_path_ ae + | Dereference ae -> + to_access_path_ ae + in + let base, accesses = to_access_path_ t in + (base, List.rev accesses) + + +and to_access_paths ts = List.map ~f:to_access_path ts + +let rec get_base = function | Base base -> - (base, []) - | Offset (ae, acc) -> - AccessPath.append (to_access_path ae) [acc] + base + | FieldOffset (ae, _) | ArrayOffset (ae, _, _) | AddressOf ae | Dereference ae -> + get_base ae + + +let lookup_field_type_annot tenv base_typ field_name = + let lookup = Tenv.lookup tenv in + Typ.Struct.get_field_type_and_annotation ~lookup field_name base_typ + + +let rec get_typ t tenv : Typ.t option = + match t with + | Base (_, typ) -> + Some typ + | FieldOffset (ae, fld) + -> ( + let base_typ_opt = get_typ ae tenv in + match base_typ_opt with + | Some base_typ -> + Option.map (lookup_field_type_annot tenv base_typ fld) ~f:fst + | None -> + None ) + | ArrayOffset (_, typ, _) -> + Some typ | AddressOf ae -> - to_access_path ae + let base_typ_opt = get_typ ae tenv in + Option.map base_typ_opt ~f:(fun base_typ -> Typ.mk (Tptr (base_typ, Pk_pointer))) | Dereference ae -> - to_access_path ae + let base_typ_opt = get_typ ae tenv in + match base_typ_opt with Some {Typ.desc= Tptr (typ, _)} -> Some typ | _ -> None -let of_access_path (base, accesses) = - let rec add_access accesses ae = - match accesses with [] -> ae | access :: rest -> add_access rest (Offset (ae, access)) +let rec pp fmt = function + | Base (pvar, _) -> + Var.pp fmt pvar + | FieldOffset (ae, fld) -> + F.fprintf fmt "%a.%a" pp ae Typ.Fieldname.pp fld + | ArrayOffset (ae, _, []) -> + F.fprintf fmt "%a[_]" pp ae + | ArrayOffset (ae, _, index_aes) -> + F.fprintf fmt "%a[%a]" pp ae (PrettyPrintable.pp_collection ~pp_item:pp) index_aes + | AddressOf ae -> + F.fprintf fmt "&(%a)" pp ae + | Dereference ae -> + F.fprintf fmt "*(%a)" pp ae + + +let equal = [%compare.equal : t] + +let base_of_id id typ = (Var.of_id id, typ) + +let base_of_pvar pvar typ = (Var.of_pvar pvar, typ) + +let of_pvar pvar typ = Base (base_of_pvar pvar typ) + +let of_id id typ = Base (base_of_id id typ) + +(* Adapted from AccessPath.of_exp. *) +let of_exp ~include_array_indexes exp0 typ0 ~(f_resolve_id: Var.t -> t option) = + let rec of_exp_ exp typ (add_accesses: t -> t) acc : t list = + match exp with + | Exp.Var id -> ( + match f_resolve_id (Var.of_id id) with + | Some access_expr -> + add_accesses access_expr :: acc + | None -> + add_accesses (of_id id typ) :: acc ) + | Exp.Lvar pvar when Pvar.is_ssa_frontend_tmp pvar -> ( + match f_resolve_id (Var.of_pvar pvar) with + | Some access_expr -> + add_accesses access_expr :: acc + | None -> + add_accesses (of_pvar pvar typ) :: acc ) + | Exp.Lvar pvar -> + add_accesses (of_pvar pvar typ) :: acc + | Exp.Lfield (root_exp, fld, root_exp_typ) -> + let add_field_access_expr access_expr = add_accesses (FieldOffset (access_expr, fld)) in + of_exp_ root_exp root_exp_typ add_field_access_expr acc + | Exp.Lindex (root_exp, index_exp) -> + let index_access_exprs = + if include_array_indexes then of_exp_ index_exp typ Fn.id [] else [] + in + let add_array_access_expr access_expr = + add_accesses (ArrayOffset (access_expr, typ, index_access_exprs)) + in + let array_typ = Typ.mk_array typ in + of_exp_ root_exp array_typ add_array_access_expr acc + | Exp.Cast (cast_typ, cast_exp) -> + of_exp_ cast_exp cast_typ Fn.id acc + | Exp.UnOp (_, unop_exp, _) -> + of_exp_ unop_exp typ Fn.id acc + | Exp.Exn exn_exp -> + of_exp_ exn_exp typ Fn.id acc + | Exp.BinOp (_, exp1, exp2) -> + of_exp_ exp1 typ Fn.id acc |> of_exp_ exp2 typ Fn.id + | Exp.Const _ | Closure _ | Sizeof _ -> + acc in - add_access accesses (Base base) + of_exp_ exp0 typ0 Fn.id [] + + +let of_lhs_exp ~include_array_indexes lhs_exp typ ~(f_resolve_id: Var.t -> t option) = + match of_exp ~include_array_indexes lhs_exp typ ~f_resolve_id with + | [lhs_ae] -> + Some lhs_ae + | _ -> + None diff --git a/infer/src/IR/AccessExpression.mli b/infer/src/IR/AccessExpression.mli index 70ccf33c0..f4a3c8553 100644 --- a/infer/src/IR/AccessExpression.mli +++ b/infer/src/IR/AccessExpression.mli @@ -11,14 +11,31 @@ open! IStd type t = | Base of AccessPath.base - | Offset of t * AccessPath.access - (* field/array access *) + | FieldOffset of t * Typ.Fieldname.t + (* field access *) + | ArrayOffset of t * Typ.t * t list + (* array access *) | AddressOf of t - (* & *) + (* address of operator & *) | Dereference of t - (* * *) + (* dereference operator * *) [@@deriving compare] val to_access_path : t -> AccessPath.t -val of_access_path : AccessPath.t -> t +val to_access_paths : t list -> AccessPath.t list + +val of_id : Ident.t -> Typ.t -> t +(** create an access expression from an ident *) + +val get_base : t -> AccessPath.base + +val get_typ : t -> Tenv.t -> Typ.t option + +val pp : Format.formatter -> t -> unit + +val equal : t -> t -> bool + +val of_lhs_exp : + include_array_indexes:bool -> Exp.t -> Typ.t -> f_resolve_id:(Var.t -> t option) -> t option +(** convert [lhs_exp] to an access expression, resolving identifiers using [f_resolve_id] *) diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index 39c9b0181..e4234d260 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -24,7 +24,7 @@ type t = let rec pp fmt = function | AccessExpression access_expr -> - AccessPath.pp fmt (AccessExpression.to_access_path access_expr) + AccessExpression.pp fmt access_expr | UnaryOperator (op, e, _) -> F.fprintf fmt "%s%a" (Unop.str op) pp e | BinaryOperator (op, e1, e2) -> @@ -53,7 +53,7 @@ let rec pp fmt = function let rec get_typ tenv = function | AccessExpression access_expr -> - AccessPath.get_typ (AccessExpression.to_access_path access_expr) tenv + AccessExpression.get_typ access_expr tenv | UnaryOperator (_, _, typ_opt) -> typ_opt | BinaryOperator ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) -> @@ -92,39 +92,39 @@ let rec get_typ tenv = function Some (Typ.mk (Typ.Tint Typ.IUInt)) -let get_access_paths exp0 = - let rec get_access_paths_ exp acc = +let get_access_exprs exp0 = + let rec get_access_exprs_ exp acc = match exp with | AccessExpression ae -> - AccessExpression.to_access_path ae :: acc + ae :: acc | Cast (_, e) | UnaryOperator (_, e, _) | Exception e | Sizeof (_, Some e) -> - get_access_paths_ e acc + get_access_exprs_ e acc | BinaryOperator (_, e1, e2) -> - get_access_paths_ e1 acc |> get_access_paths_ e2 + get_access_exprs_ e1 acc |> get_access_exprs_ e2 | Closure (_, captured) -> - List.fold captured ~f:(fun acc (_, e) -> get_access_paths_ e acc) ~init:acc + List.fold captured ~f:(fun acc (_, e) -> get_access_exprs_ e acc) ~init:acc | Constant _ | Sizeof _ -> acc in - get_access_paths_ exp0 [] + get_access_exprs_ exp0 [] (* convert an SIL expression into an HIL expression. the [f_resolve_id] function should map an SSA temporary variable to the access path it represents. evaluating the HIL expression should produce the same result as evaluating the SIL expression and replacing the temporary variables using [f_resolve_id] *) -let of_sil ~include_array_indexes ~f_resolve_id exp typ = +let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ = let rec of_sil_ (exp: Exp.t) typ = match exp with | Var id -> - let ap = + let ae = match f_resolve_id (Var.of_id id) with - | Some access_path -> - access_path + | Some access_expr -> + if add_deref then AccessExpression.Dereference access_expr else access_expr | None -> - AccessPath.of_id id typ + AccessExpression.of_id id typ in - AccessExpression (AccessExpression.of_access_path ap) + AccessExpression ae | UnOp (op, e, typ_opt) -> UnaryOperator (op, of_sil_ e typ, typ_opt) | BinOp (op, e0, e1) -> @@ -156,9 +156,9 @@ let of_sil ~include_array_indexes ~f_resolve_id exp typ = in Closure (closure.name, environment) | Lfield (root_exp, fld, root_exp_typ) -> ( - match AccessPath.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with - | Some access_path -> - AccessExpression (AccessExpression.of_access_path access_path) + match AccessExpression.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with + | Some access_expr -> + AccessExpression access_expr | None -> (* unsupported field expression: represent with a dummy variable *) of_sil_ @@ -173,9 +173,9 @@ let of_sil ~include_array_indexes ~f_resolve_id exp typ = literal, e.g. using `const_cast` *) of_sil_ (Exp.Lindex (Var (Ident.create_normal (Ident.string_to_name s) 0), index_exp)) typ | Lindex (root_exp, index_exp) -> ( - match AccessPath.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with - | Some access_path -> - AccessExpression (AccessExpression.of_access_path access_path) + match AccessExpression.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with + | Some access_expr -> + AccessExpression access_expr | None -> (* unsupported index expression: represent with a dummy variable *) of_sil_ @@ -183,9 +183,9 @@ let of_sil ~include_array_indexes ~f_resolve_id exp typ = ( Var (Ident.create_normal (Ident.string_to_name (Exp.to_string root_exp)) 0) , index_exp )) typ ) | Lvar _ -> - match AccessPath.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with - | Some access_path -> - AccessExpression (AccessExpression.of_access_path access_path) + match AccessExpression.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with + | Some access_expr -> + AccessExpression access_expr | None -> L.(die InternalError) "Couldn't convert var expression %a to access path" Exp.pp exp in diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli index e7150727d..d431e5851 100644 --- a/infer/src/IR/HilExp.mli +++ b/infer/src/IR/HilExp.mli @@ -30,10 +30,11 @@ val get_typ : Tenv.t -> t -> Typ.t option (** Get the type of the expression. Warning: not fully implemented *) val of_sil : - include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessPath.t option) -> Exp.t -> Typ.t -> t + include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessExpression.t option) -> add_deref:bool + -> Exp.t -> Typ.t -> t (** Convert SIL expression to HIL expression *) -val get_access_paths : t -> AccessPath.t list +val get_access_exprs : t -> AccessExpression.t list (** Get all the access paths used in the given HIL expression, including duplicates if a path is used more than once. *) diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index 1165d1235..0c9b10d42 100644 --- a/infer/src/IR/HilInstr.ml +++ b/infer/src/IR/HilInstr.ml @@ -11,13 +11,13 @@ open! IStd module F = Format module L = Logging -type call = Direct of Typ.Procname.t | Indirect of AccessPath.t [@@deriving compare] +type call = Direct of Typ.Procname.t | Indirect of AccessExpression.t [@@deriving compare] let pp_call fmt = function | Direct pname -> Typ.Procname.pp fmt pname - | Indirect access_path -> - F.fprintf fmt "*%a" AccessPath.pp access_path + | Indirect access_expr -> + F.fprintf fmt "*%a" AccessExpression.pp access_expr type t = @@ -28,9 +28,7 @@ type t = let pp fmt = function | Assign (access_expr, exp, loc) -> - F.fprintf fmt "%a := %a [%a]" AccessPath.pp - (AccessExpression.to_access_path access_expr) - HilExp.pp exp Location.pp loc + F.fprintf fmt "%a := %a [%a]" AccessExpression.pp access_expr HilExp.pp exp Location.pp loc | Assume (exp, _, _, loc) -> F.fprintf fmt "assume %a [%a]" HilExp.pp exp Location.pp loc | Call (ret_opt, call, actuals, _, loc) -> @@ -39,25 +37,31 @@ let pp fmt = function F.fprintf fmt "%a%a(%a) [%a]" pp_ret ret_opt pp_call call pp_actuals actuals Location.pp loc -type translation = Instr of t | Bind of Var.t * AccessPath.t | Unbind of Var.t list | Ignore +type translation = + | Instr of t + | Bind of Var.t * AccessExpression.t + | Unbind of Var.t list + | Ignore (* convert an SIL instruction into an HIL instruction. the [f_resolve_id] function should map an SSA temporary variable to the access path it represents. evaluating the HIL instruction should produce the same result as evaluating the SIL instruction and replacing the temporary variables using [f_resolve_id]. *) let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) = - let exp_of_sil = HilExp.of_sil ~include_array_indexes ~f_resolve_id in - let analyze_id_assignment lhs_id rhs_exp rhs_typ loc = - let rhs_hil_exp = exp_of_sil rhs_exp rhs_typ in + let exp_of_sil ?(add_deref= false) = + HilExp.of_sil ~include_array_indexes ~f_resolve_id ~add_deref + in + let analyze_id_assignment ?(add_deref= false) lhs_id rhs_exp rhs_typ loc = + let rhs_hil_exp = exp_of_sil ~add_deref rhs_exp rhs_typ in match rhs_hil_exp with | AccessExpression rhs_access_expr -> - Bind (lhs_id, AccessExpression.to_access_path rhs_access_expr) + Bind (lhs_id, rhs_access_expr) | _ -> Instr (Assign (AccessExpression.Base (lhs_id, rhs_typ), rhs_hil_exp, loc)) in match instr with | Load (lhs_id, rhs_exp, rhs_typ, loc) -> - analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ loc + analyze_id_assignment ~add_deref:true (Var.of_id lhs_id) rhs_exp rhs_typ loc | Store (Lvar lhs_pvar, lhs_typ, rhs_exp, loc) when Pvar.is_ssa_frontend_tmp lhs_pvar -> analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ loc | Call @@ -70,7 +74,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) = analyze_id_assignment (Var.of_id ret_id) target_exp cast_typ loc | Store (lhs_exp, typ, rhs_exp, loc) -> let lhs_access_expr = - match exp_of_sil lhs_exp typ with + match exp_of_sil ~add_deref:true lhs_exp typ with | AccessExpression access_expr -> access_expr | BinaryOperator (_, exp0, exp1) -> ( @@ -79,14 +83,14 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) = one pointer type represented as an access path. just use that access path and forget about the arithmetic. if you need to model this more precisely, you should be using SIL instead *) - HilExp.get_access_paths exp0 + HilExp.get_access_exprs exp0 with | ap :: _ -> - AccessExpression.of_access_path ap + ap | [] -> - match HilExp.get_access_paths exp1 with + match HilExp.get_access_exprs exp1 with | ap :: _ -> - AccessExpression.of_access_path ap + ap | [] -> L.(die InternalError) "Invalid pointer arithmetic expression %a used as LHS at %a" Exp.pp lhs_exp @@ -110,7 +114,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) = | Constant Cfun procname | Closure (procname, _) -> Direct procname | AccessExpression access_expr -> - Indirect (AccessExpression.to_access_path access_expr) + Indirect access_expr | call_exp -> L.(die InternalError) "Unexpected call expression %a" HilExp.pp call_exp in diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli index 47334f391..91f39fc23 100644 --- a/infer/src/IR/HilInstr.mli +++ b/infer/src/IR/HilInstr.mli @@ -11,7 +11,7 @@ open! IStd module F = Format (** type of a procedure call; either direct or via function pointer *) -type call = Direct of Typ.Procname.t | Indirect of AccessPath.t [@@deriving compare] +type call = Direct of Typ.Procname.t | Indirect of AccessExpression.t [@@deriving compare] type t = | Assign of AccessExpression.t * HilExp.t * Location.t @@ -27,11 +27,11 @@ val pp : F.formatter -> t -> unit (** Result of translating an SIL instruction *) type translation = | Instr of t (** HIL instruction to execute *) - | Bind of Var.t * AccessPath.t (** add binding to identifier map *) + | Bind of Var.t * AccessExpression.t (** add binding to identifier map *) | Unbind of Var.t list (** remove binding from identifier map *) | Ignore (** no-op *) val of_sil : - include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessPath.t option) -> Sil.instr + include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessExpression.t option) -> Sil.instr -> translation (** Convert an SIL instruction to an HIL instruction *) diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 4b5f50b62..1aadc5863 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -67,13 +67,10 @@ struct "dump" all of the temporaries out of the id map, then execute the unlock instruction. *) let actual_state' = IdAccessPathMapDomain.fold - (fun id access_path astate_acc -> + (fun id access_expr astate_acc -> let lhs_access_path = AccessExpression.Base (id, Typ.mk Typ.Tvoid) in let dummy_assign = - HilInstr.Assign - ( lhs_access_path - , HilExp.AccessExpression (AccessExpression.of_access_path access_path) - , loc ) + HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc) in TransferFunctions.exec_instr astate_acc extras node dummy_assign ) id_map actual_state diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index 6ac57da22..279b5027a 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/infer/src/checkers/IdAccessPathMapDomain.ml @@ -11,20 +11,20 @@ open! IStd module IdMap = Var.Map module L = Logging -type astate = AccessPath.t IdMap.t +type astate = AccessExpression.t IdMap.t include IdMap -let pp fmt astate = IdMap.pp ~pp_value:AccessPath.pp fmt astate +let pp fmt astate = IdMap.pp ~pp_value:AccessExpression.pp fmt astate let check_invariant ap1 ap2 = function | Var.ProgramVar pvar when Pvar.is_ssa_frontend_tmp pvar -> (* Sawja reuses temporary variables which sometimes breaks this invariant *) () | id -> - if not (AccessPath.equal ap1 ap2) then + if not (AccessExpression.equal ap1 ap2) then L.(die InternalError) - "Id %a maps to both %a and %a" Var.pp id AccessPath.pp ap1 AccessPath.pp ap2 + "Id %a maps to both %a and %a" Var.pp id AccessExpression.pp ap1 AccessExpression.pp ap2 let ( <= ) ~lhs ~rhs = diff --git a/infer/src/checkers/IdAccessPathMapDomain.mli b/infer/src/checkers/IdAccessPathMapDomain.mli index 4c63dce82..44587d900 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.mli +++ b/infer/src/checkers/IdAccessPathMapDomain.mli @@ -13,7 +13,7 @@ open! IStd module IdMap = Var.Map -type astate = AccessPath.t IdMap.t +type astate = AccessExpression.t IdMap.t include module type of IdMap diff --git a/infer/src/checkers/Ownership.ml b/infer/src/checkers/Ownership.ml index fb74d00ad..af42b4b23 100644 --- a/infer/src/checkers/Ownership.ml +++ b/infer/src/checkers/Ownership.ml @@ -124,8 +124,9 @@ module Domain = struct let exp_add_reads exp loc summary astate = List.fold - ~f:(fun acc access_path -> access_path_add_read access_path loc summary acc) - (HilExp.get_access_paths exp) ~init:astate + ~f:(fun acc access_expr -> + access_path_add_read (AccessExpression.to_access_path access_expr) loc summary acc ) + (HilExp.get_access_exprs exp) ~init:astate let actuals_add_reads actuals loc summary astate = @@ -144,8 +145,10 @@ module Domain = struct let borrow_exp lhs_var rhs_exp astate = let rhs_vars = - List.fold (HilExp.get_access_paths rhs_exp) - ~f:(fun acc ((var, _), _) -> VarSet.add var acc) + List.fold (HilExp.get_access_exprs rhs_exp) + ~f:(fun acc access_expr -> + let (var, _), _ = AccessExpression.to_access_path access_expr in + VarSet.add var acc ) ~init:VarSet.empty in borrow_vars lhs_var rhs_vars astate diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 6b98cd7af..03c51ee79 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -164,9 +164,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_field_access pre in List.fold - ~f:(fun acc (base, accesses) -> + ~f:(fun acc access_expr -> + let base, accesses = AccessExpression.to_access_path access_expr in if is_static_access (fst base) then acc else add_field_accesses (base, []) acc accesses ) - ~init:accesses (HilExp.get_access_paths exp) + ~init:accesses (HilExp.get_access_exprs exp) let is_synchronized_container callee_pname ((_, (base_typ: Typ.t)), accesses) tenv = @@ -584,7 +585,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_access rhs_exp loc ~is_write_access:false astate.accesses astate.locks astate.threads astate.ownership proc_data in - let rhs_access_paths = HilExp.get_access_paths rhs_exp in + let rhs_access_paths = + AccessExpression.to_access_paths (HilExp.get_access_exprs rhs_exp) + in let is_functional = not (List.is_empty rhs_access_paths) && List.for_all @@ -607,10 +610,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct report spurious read/write races *) rhs_accesses else - add_access - (AccessExpression (AccessExpression.of_access_path lhs_access_path)) - loc ~is_write_access:true rhs_accesses astate.locks astate.threads astate.ownership - proc_data + add_access (AccessExpression lhs_access_expr) loc ~is_write_access:true rhs_accesses + astate.locks astate.threads astate.ownership proc_data in let ownership = propagate_ownership lhs_access_path rhs_exp astate.ownership in let attribute_map = propagate_attributes lhs_access_path rhs_exp astate.attribute_map in @@ -674,9 +675,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate.threads astate.ownership proc_data in let astate' = - match HilExp.get_access_paths assume_exp with - | [access_path] + match HilExp.get_access_exprs assume_exp with + | [access_expr] -> ( + let access_path = AccessExpression.to_access_path access_expr in let choices = AttributeMapDomain.get_choices access_path astate.attribute_map in match eval_bexp access_path assume_exp with | Some bool_value -> diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 0dfc401db..f63f8f3be 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -466,7 +466,7 @@ module StabilityDomain = struct let add_wobbly_path_exp exp paths = - let access_paths = HilExp.get_access_paths exp in + let access_paths = AccessExpression.to_access_paths (HilExp.get_access_exprs exp) in List.fold ~f:(fun acc p -> add_path p acc) access_paths ~init:paths @@ -529,9 +529,9 @@ module StabilityDomain = struct | Some formal_index -> ( match List.nth actuals formal_index with | Some actual_exp -> ( - match HilExp.get_access_paths actual_exp with + match HilExp.get_access_exprs actual_exp with | [actual] -> - AccessPath.append actual accesses + AccessPath.append (AccessExpression.to_access_path actual) accesses | _ -> path ) | None -> diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 1cd76c4dd..23b1dddab 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -449,39 +449,46 @@ module Make (TaintSpecification : TaintSpec.S) = struct (* 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 (_, accesses) loc astate = - let add_sinks_for_access astate_acc = function - | AccessPath.FieldAccess _ | AccessPath.ArrayAccess (_, []) -> + let add_sinks_for_access_path access_expr loc astate = + let rec add_sinks_for_access astate_acc = function + | AccessExpression.Base _ -> astate_acc - | AccessPath.ArrayAccess (_, indexes) -> + | AccessExpression.FieldOffset (ae, _) + | ArrayOffset (ae, _, []) + | Dereference ae + | AddressOf ae -> + add_sinks_for_access astate_acc ae + | AccessExpression.ArrayOffset (ae, _, indexes) -> let dummy_call_site = CallSite.make BuiltinDecl.__array_access loc in let dummy_actuals = - List.map - ~f:(fun index_ap -> - HilExp.AccessExpression (AccessExpression.of_access_path index_ap) ) - indexes + List.map ~f:(fun index_ae -> HilExp.AccessExpression index_ae) indexes in let sinks = TraceDomain.Sink.get dummy_call_site dummy_actuals proc_data.ProcData.tenv in - match sinks with - | None -> - astate_acc - | Some sink -> - add_sink sink dummy_actuals astate proc_data dummy_call_site + let astate_acc_result = + match sinks with + | None -> + astate_acc + | Some sink -> + add_sink sink dummy_actuals astate proc_data dummy_call_site + in + add_sinks_for_access astate_acc_result ae in - List.fold ~f:add_sinks_for_access ~init:astate accesses + add_sinks_for_access astate access_expr in - let add_sources_for_access_path (((var, _), _) as ap) loc astate = + let add_sources_for_access_path access_expr loc astate = + let var, _ = AccessExpression.get_base access_expr in if Var.is_global var then let dummy_call_site = CallSite.make BuiltinDecl.__global_access loc in match - TraceDomain.Source.get dummy_call_site - [HilExp.AccessExpression (AccessExpression.of_access_path ap)] + TraceDomain.Source.get dummy_call_site [HilExp.AccessExpression access_expr] proc_data.tenv with | Some {TraceDomain.Source.source} -> - let access_path = AccessPath.Abs.Exact ap in + let access_path = + AccessPath.Abs.Exact (AccessExpression.to_access_path access_expr) + in let trace, subtree = Option.value ~default:TaintDomain.empty_node (TaintDomain.get_node access_path astate) @@ -495,16 +502,16 @@ module Make (TaintSpecification : TaintSpec.S) = struct let add_sources_sinks_for_exp exp loc astate = match exp with | HilExp.AccessExpression access_expr -> - let access_path = AccessExpression.to_access_path access_expr in - add_sinks_for_access_path access_path loc astate - |> add_sources_for_access_path access_path loc + add_sinks_for_access_path access_expr loc astate + |> add_sources_for_access_path access_expr loc | _ -> astate in - let exec_write lhs_access_path rhs_exp astate = + let exec_write 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 = AccessExpression.to_access_path lhs_access_expr in TaintDomain.add_node (AccessPath.Abs.Exact lhs_access_path) rhs_node astate in match instr with @@ -522,9 +529,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct `return null` in a void function *) astate | Assign (lhs_access_expr, rhs_exp, loc) -> - let lhs_access_path = AccessExpression.to_access_path lhs_access_expr in add_sources_sinks_for_exp rhs_exp loc astate - |> add_sinks_for_access_path lhs_access_path loc |> exec_write lhs_access_path rhs_exp + |> 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_opt, Direct called_pname, actuals, _, callee_loc) -> @@ -614,18 +620,16 @@ module Make (TaintSpecification : TaintSpec.S) = struct match (* treat unknown calls to C++ operator= as assignment *) actuals with | [(AccessExpression lhs_access_expr); rhs_exp] -> - exec_write (AccessExpression.to_access_path lhs_access_expr) rhs_exp access_tree + exec_write lhs_access_expr rhs_exp access_tree | [(AccessExpression lhs_access_expr); rhs_exp; (HilExp.AccessExpression access_expr)] -> ( - let dummy_ret_access_path = AccessExpression.to_access_path access_expr in - match dummy_ret_access_path with - | (Var.ProgramVar pvar, _), [] when Pvar.is_frontend_tmp pvar -> + let dummy_ret_access_expr = access_expr in + match dummy_ret_access_expr with + | AccessExpression.Base (Var.ProgramVar pvar, _) 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 - (AccessExpression.to_access_path lhs_access_expr) - rhs_exp access_tree - |> exec_write dummy_ret_access_path rhs_exp + exec_write lhs_access_expr rhs_exp access_tree + |> exec_write dummy_ret_access_expr rhs_exp | _ -> L.internal_error "Unexpected call to operator= %a in %a" HilInstr.pp instr Typ.Procname.pp callee_pname ; diff --git a/infer/tests/codetoanalyze/cpp/racerd/dereferencing.cpp b/infer/tests/codetoanalyze/cpp/racerd/dereferencing.cpp new file mode 100644 index 000000000..504c48f1c --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/racerd/dereferencing.cpp @@ -0,0 +1,71 @@ +/* + * Copyright (c) 2018 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +#include + +namespace dereferencing { + +struct B { + int c; +}; + +struct A { + B b; +}; + +struct X { + int w; + int u; + X* x1; + X** x2; + A a; +}; + +class Basic { + public: + Basic() {} + + void pointer_deref_race(int* v1) { (*v1)++; } // HIL: *(&v1) := *(&v1) + 1 + + void pointer_arith_ok(int* v2) { v2++; } // HIL: &v2 := &v2 + 1 + + void value_ok(int v3) { v3++; } // HIL: &v3 := &v3 + 1 + + void field_race(int& f) { f++; } // HIL: *(&f) := *(&f) + 1 + + void mixed_deref_race(X& xparam) { + xparam.x1->w++; // HIL: &xparam.x1.w := &xparam.x1.w + 1 + (*xparam.x1).u++; // HIL: &xparam.x1.u := &xparam.x1.u + 1 + (**xparam.x2).a.b.c++; // HIL:*(&xparam.x2).a.b.c := *(&xparam.x2).a.b.c + 1 + } + + void call1() { + pointer_deref_race(&p); // race - FalseNegative + pointer_arith_ok(&q); // no race + value_ok(h); // no race + field_race(g); // race - FalseNegative + mixed_deref_race(x); // race + } + + int test_lock() { + mutex_.lock(); + call1(); + } + + int test_unlock() { call1(); } + + private: + int g; + int h; + int p; + int q; + X x; + std::mutex mutex_; +}; +} // namespace dereferencing diff --git a/infer/tests/codetoanalyze/cpp/racerd/issues.exp b/infer/tests/codetoanalyze/cpp/racerd/issues.exp index 917e160c3..5454ec180 100644 --- a/infer/tests/codetoanalyze/cpp/racerd/issues.exp +++ b/infer/tests/codetoanalyze/cpp/racerd/issues.exp @@ -3,6 +3,12 @@ codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get4, 0, LOCK_CONSISTENCY_VIO codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get5, 0, LOCK_CONSISTENCY_VIOLATION, [,call to basics::Basic_get_private_suspiciously_read,access to `&this.suspiciously_read`,,access to `&this.suspiciously_read`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_test_double_lock_bad, 0, LOCK_CONSISTENCY_VIOLATION, [,access to `&this.single_lock_suspiciously_read`,,access to `&this.single_lock_suspiciously_read`] codetoanalyze/cpp/racerd/constructor_ownership.cpp, constructors::TSL_not_locked_race, 0, LOCK_CONSISTENCY_VIOLATION, [,call to constructors::BSS_toJson_race,call to constructors::dynamic_operator=,access to `&this.type_`,,call to constructors::BSS_toJson_race,call to constructors::dynamic_operator=,access to `&this.type_`] +codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 5, LOCK_CONSISTENCY_VIOLATION, [,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.u`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.u`] +codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 5, LOCK_CONSISTENCY_VIOLATION, [,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x2.a.b.c`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x2.a.b.c`] +codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 5, LOCK_CONSISTENCY_VIOLATION, [,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.w`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.w`] +codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 0, LOCK_CONSISTENCY_VIOLATION, [,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.w`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.w`] +codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 0, LOCK_CONSISTENCY_VIOLATION, [,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x2.a.b.c`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x2.a.b.c`] +codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 0, LOCK_CONSISTENCY_VIOLATION, [,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.u`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.u`] codetoanalyze/cpp/racerd/locals_ownership.cpp, locals::Ownership_test2_bad, 5, LOCK_CONSISTENCY_VIOLATION, [,access to `&x.f`,,access to `&x.f`] codetoanalyze/cpp/racerd/locals_ownership.cpp, locals::Ownership_test3_bad, 5, LOCK_CONSISTENCY_VIOLATION, [,access to `&x.f`,,access to `&x.f`] codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard_get2, 3, LOCK_CONSISTENCY_VIOLATION, [,access to `&this.suspiciously_written`,,access to `&this.suspiciously_written`]