diff --git a/infer/src/IR/AccessExpression.ml b/infer/src/IR/AccessExpression.ml index 560417855..c67aacfab 100644 --- a/infer/src/IR/AccessExpression.ml +++ b/infer/src/IR/AccessExpression.ml @@ -79,6 +79,8 @@ let rec get_typ t tenv : Typ.t option = let rec pp fmt = function | Base (pvar, _) -> Var.pp fmt pvar + | FieldOffset (Dereference ae, fld) -> + F.fprintf fmt "%a->%a" pp ae Typ.Fieldname.pp fld | FieldOffset (ae, fld) -> F.fprintf fmt "%a.%a" pp ae Typ.Fieldname.pp fld | ArrayOffset (ae, _, []) -> @@ -97,28 +99,64 @@ 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_pvar pvar typ = AddressOf (Base (base_of_pvar pvar typ)) let of_id id typ = Base (base_of_id id typ) +(* cancel out consective *&'s *) +let rec normalize t = + match t with + | Base _ -> + t + | Dereference AddressOf t1 -> + normalize t1 + | FieldOffset (t1, fieldname) -> + let t1' = normalize t1 in + if phys_equal t1 t1' then t else normalize (FieldOffset (t1', fieldname)) + | ArrayOffset (t1, typ, tlist) -> + let t1' = normalize t1 in + let tlist' = IList.map_changed ~f:normalize ~equal tlist in + if phys_equal t1 t1' && phys_equal tlist tlist' then t + else normalize (ArrayOffset (t1', typ, tlist')) + | Dereference t1 -> + let t1' = normalize t1 in + if phys_equal t1 t1' then t else normalize (Dereference t1') + | AddressOf t1 -> + let t1' = normalize t1 in + if phys_equal t1 t1' then t else normalize (AddressOf t1') + + (* Adapted from AccessPath.of_exp. *) -let of_exp ~include_array_indexes exp0 typ0 ~(f_resolve_id: Var.t -> t option) = +let of_exp ~include_array_indexes ~add_deref 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 + let access_expr' = if add_deref then Dereference access_expr else access_expr in + add_accesses access_expr' :: acc | None -> - add_accesses (of_id id typ) :: acc ) + let access_expr = of_id id typ in + let access_expr' = if add_deref then Dereference access_expr else access_expr in + add_accesses access_expr' :: 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 + (* do not need to add deref here as it was added implicitly in the binding *) + (* but need to remove it if add_deref is false *) + let access_expr' = + if not add_deref then match access_expr with Dereference ae -> ae | _ -> assert false + else access_expr + in + add_accesses access_expr' :: acc | None -> - add_accesses (of_pvar pvar typ) :: acc ) + let access_expr = of_pvar pvar typ in + let access_expr' = if add_deref then Dereference access_expr else access_expr in + add_accesses access_expr' :: acc ) | Exp.Lvar pvar -> - add_accesses (of_pvar pvar typ) :: acc + let access_expr = of_pvar pvar typ in + let access_expr' = if add_deref then Dereference access_expr else access_expr in + add_accesses access_expr' :: 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 @@ -142,12 +180,15 @@ let of_exp ~include_array_indexes exp0 typ0 ~(f_resolve_id: Var.t -> t option) = | Exp.Const _ | Closure _ | Sizeof _ -> acc in - of_exp_ exp0 typ0 Fn.id [] + IList.map_changed ~f:normalize ~equal (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 +let of_lhs_exp ~include_array_indexes ~add_deref lhs_exp typ ~(f_resolve_id: Var.t -> t option) = + match lhs_exp with + | (Exp.Lfield _ | Exp.Lindex _) when not add_deref + -> ( + let res = of_exp ~include_array_indexes ~add_deref:true lhs_exp typ ~f_resolve_id in + match res with [lhs_ae] -> Some (AddressOf lhs_ae) | _ -> None ) | _ -> - None + let res = of_exp ~include_array_indexes ~add_deref lhs_exp typ ~f_resolve_id in + match res with [lhs_ae] -> Some lhs_ae | _ -> None diff --git a/infer/src/IR/AccessExpression.mli b/infer/src/IR/AccessExpression.mli index f4a3c8553..7be8d5b35 100644 --- a/infer/src/IR/AccessExpression.mli +++ b/infer/src/IR/AccessExpression.mli @@ -37,5 +37,8 @@ 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 + include_array_indexes:bool -> add_deref: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] *) + +val normalize : t -> t diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index e4234d260..39004e416 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -120,9 +120,12 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ = let ae = match f_resolve_id (Var.of_id id) with | Some access_expr -> - if add_deref then AccessExpression.Dereference access_expr else access_expr + if add_deref then AccessExpression.normalize (Dereference access_expr) + else access_expr | None -> - AccessExpression.of_id id typ + let access_expr = AccessExpression.of_id id typ in + if add_deref then AccessExpression.normalize (Dereference access_expr) + else access_expr in AccessExpression ae | UnOp (op, e, typ_opt) -> @@ -156,7 +159,9 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ = in Closure (closure.name, environment) | Lfield (root_exp, fld, root_exp_typ) -> ( - match AccessExpression.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with + match + AccessExpression.of_lhs_exp ~include_array_indexes ~add_deref exp typ ~f_resolve_id + with | Some access_expr -> AccessExpression access_expr | None -> @@ -173,7 +178,9 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref 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 AccessExpression.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with + match + AccessExpression.of_lhs_exp ~include_array_indexes ~add_deref exp typ ~f_resolve_id + with | Some access_expr -> AccessExpression access_expr | None -> @@ -183,7 +190,9 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ = ( Var (Ident.create_normal (Ident.string_to_name (Exp.to_string root_exp)) 0) , index_exp )) typ ) | Lvar _ -> - match AccessExpression.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with + match + AccessExpression.of_lhs_exp ~include_array_indexes ~add_deref exp typ ~f_resolve_id + with | Some access_expr -> AccessExpression access_expr | None -> diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index 0c9b10d42..4f6c973f7 100644 --- a/infer/src/IR/HilInstr.ml +++ b/infer/src/IR/HilInstr.ml @@ -63,6 +63,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) = | Load (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 -> + (* do not need to add deref here as it is added implicitly in of_pvar by forgetting the & *) analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ loc | Call ( Some (ret_id, _) diff --git a/infer/tests/codetoanalyze/cpp/racerd/dereferencing.cpp b/infer/tests/codetoanalyze/cpp/racerd/dereferencing.cpp index 504c48f1c..f94d53087 100644 --- a/infer/tests/codetoanalyze/cpp/racerd/dereferencing.cpp +++ b/infer/tests/codetoanalyze/cpp/racerd/dereferencing.cpp @@ -31,18 +31,18 @@ class Basic { public: Basic() {} - void pointer_deref_race(int* v1) { (*v1)++; } // HIL: *(&v1) := *(&v1) + 1 + void pointer_deref_race(int* v1) { (*v1)++; } // HIL: *(v1) := *(v1) + 1 - void pointer_arith_ok(int* v2) { v2++; } // HIL: &v2 := &v2 + 1 + void pointer_arith_ok(int* v2) { v2++; } // HIL: v2 := v2 + 1 - void value_ok(int v3) { v3++; } // HIL: &v3 := &v3 + 1 + void value_ok(int v3) { v3++; } // HIL: v3 := v3 + 1 - void field_race(int& f) { f++; } // HIL: *(&f) := *(&f) + 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 + 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() {