[hil] add Unbind operation for removing a temporary binding

Reviewed By: jberdine

Differential Revision: D4968741

fbshipit-source-id: 08111fa

infer/src/IR/HilInstr.ml

@@ -39,7 +39,8 @@ let pp fmt = function
 
 type translation =
   | Instr of t
-  | Update of Var.t * AccessPath.Raw.t
+  | Bind of Var.t * AccessPath.Raw.t
+  | Unbind of Var.t list
   | Ignore
 
 (* convert an SIL instruction into an HIL instruction. the [f_resolve_id] function should map an SSA
@@ -51,7 +52,7 @@ let of_sil ~f_resolve_id (instr : Sil.instr) =
     let rhs_hil_exp = HilExp.of_sil ~f_resolve_id rhs_exp rhs_typ in
     match HilExp.get_access_paths rhs_hil_exp with
     | [rhs_access_path] ->
-        Update (lhs_id, rhs_access_path)
+        Bind (lhs_id, rhs_access_path)
     | _ ->
         Instr (Write (((lhs_id, rhs_typ), []), rhs_hil_exp, loc)) in
   match instr with
@@ -83,7 +84,10 @@ let of_sil ~f_resolve_id (instr : Sil.instr) =
       let hil_exp = HilExp.of_sil ~f_resolve_id exp (Typ.mk (Tint IBool)) in
       let branch = if true_branch then `Then else `Else in
       Instr (Assume (hil_exp, branch, if_kind, loc))
-  | Nullify _ | Remove_temps _
+  | Nullify (pvar, _) ->
+      Unbind [Var.of_pvar pvar]
+  | Remove_temps (ids, _) ->
+      Unbind (List.map ~f:Var.of_id ids)
   (* ignoring for now; will translate as builtin function call if needed *)
   | Abstract _ | Declare_locals _ ->
       (* these don't seem useful for most analyses. can translate them later if we want to *)

infer/src/IR/HilInstr.mli

@@ -30,12 +30,12 @@ type t =
 
 val pp : F.formatter -> t -> unit
 
-(** The result of translating an SIL instruction can either be a new HIL instruction or an update to
-    the identifier map (in the case that the SIL instructions writes to a temporary) *)
+(** Result of translating an SIL instruction *)
 type translation =
-  | Instr of t
-  | Update of Var.t * AccessPath.Raw.t
-  | Ignore
+  | Instr of t (** HIL instruction to execute *)
+  | Bind of Var.t * AccessPath.Raw.t (** add binding to identifier map *)
+  | Unbind of Var.t list (** remove binding from identifier map *)
+  | Ignore (** no-op *)
 
 (** Convert an SIL instruction to an HIL instruction *)
 val of_sil : f_resolve_id:(Var.t -> AccessPath.Raw.t option) -> Sil.instr -> translation

infer/src/checkers/ThreadSafety.ml

@@ -439,9 +439,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       try Some (IdAccessPathMapDomain.find id astate.id_map)
       with Not_found -> None in
     match HilInstr.of_sil ~f_resolve_id instr with
-    | Update (id, access_path) ->
+    | Bind (id, access_path) ->
         let id_map = IdAccessPathMapDomain.add id access_path astate.id_map in
         { astate with id_map; }
+    | Unbind ids ->
+        let id_map =
+          List.fold
+            ~f:(fun acc id -> IdAccessPathMapDomain.remove id acc) ~init:astate.id_map ids in
+        { astate with id_map; }
     | Instr hil_instr ->
         exec_hil_instr_ hil_instr
     | Ignore ->