[HIL] Explicit dereference

Reviewed By: sblackshear

Differential Revision: D7350669

fbshipit-source-id: c316188

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) =
+let of_lhs_exp ~include_array_indexes ~add_deref lhs_exp typ ~(f_resolve_id: Var.t -> t option) =
-  match of_exp ~include_array_indexes lhs_exp typ ~f_resolve_id with
+  match lhs_exp with
-  | [lhs_ae] ->
+  | (Exp.Lfield _ | Exp.Lindex _) when not add_deref
-      Some lhs_ae
+    -> (
+      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

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

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<char*>` *)
         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 ->

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, _)

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->w++; // HIL: xparam->x1->w := xparam->x1->w + 1
-    (*xparam.x1).u++; // HIL: &xparam.x1.u := &xparam.x1.u + 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.x2).a.b.c++; // HIL:*(xparam->x2)->a.b.c:= *(xparam->x2)->a.b.c+1
   }
 
   void call1() {