[HIL] Add `ExitScope` instruction

Summary:
It's useful for checkers to know when variables go out of scope to
perform garbage collection in their domains, especially for complex
domains with non-trivial joins. This makes the analyses more precise at
little cost.

This could have been added as a custom function call to a builtin, but I
decided against it because this instruction doesn't have the semantics
of any function call. It's better for each checker to explicitly not
deal with the custom instruction instead.

Reviewed By: jberdine

Differential Revision: D13102951

fbshipit-source-id: 33be22fab

infer/src/IR/HilInstr.ml

@@ -22,6 +22,7 @@ type t =
   | Assign of AccessExpression.t * HilExp.t * Location.t
   | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t
   | Call of AccessPath.base * call * HilExp.t list * CallFlags.t * Location.t
+  | ExitScope of Var.t list
 [@@deriving compare]
 
 let pp fmt = function
@@ -33,13 +34,11 @@ let pp fmt = function
       let pp_ret fmt = F.fprintf fmt "%a := " AccessPath.pp_base in
       let pp_actuals fmt = PrettyPrintable.pp_collection ~pp_item:HilExp.pp fmt in
       F.fprintf fmt "%a%a(%a) [%a]" pp_ret ret pp_call call pp_actuals actuals Location.pp loc
+  | ExitScope vars ->
+      F.fprintf fmt "exit scope [%a]" (Pp.seq ~sep:"; " Var.pp) vars
 
 
-type translation =
-  | Instr of t
-  | Bind of Var.t * AccessExpression.t
-  | Unbind of Var.t list
-  | Ignore
+type translation = Instr of t | Bind of Var.t * AccessExpression.t | 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
@@ -122,8 +121,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) =
       let branch = if true_branch then `Then else `Else in
       Instr (Assume (hil_exp, branch, if_kind, loc))
   | ExitScope (vars, _) ->
-      Unbind vars
-  (* ignoring for now; will translate as builtin function call if needed *)
+      Instr (ExitScope vars)
   | Abstract _ | Nullify _ ->
       (* these don't seem useful for most analyses. can translate them later if we want to *)
       Ignore

infer/src/IR/HilInstr.mli

@@ -18,6 +18,7 @@ type t =
       (** Assumed expression, true_branch boolean, source of the assume (conditional, ternary, etc.) *)
   | Call of AccessPath.base * call * HilExp.t list * CallFlags.t * Location.t
       (** Var to hold the return, call expression, formals *)
+  | ExitScope of Var.t list
 [@@deriving compare]
 
 val pp : F.formatter -> t -> unit
@@ -26,7 +27,6 @@ val pp : F.formatter -> t -> unit
 type translation =
   | Instr of t  (** HIL instruction to execute *)
   | 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 :

infer/src/absint/LowerHil.ml

@@ -19,8 +19,8 @@ let update_id_map hil_translation id_map =
   match (hil_translation : HilInstr.translation) with
   | Bind (id, access_path) ->
       IdAccessPathMapDomain.add id access_path id_map
-  | Unbind ids ->
-      List.fold ~f:(fun acc id -> IdAccessPathMapDomain.remove id acc) ~init:id_map ids
+  | Instr (ExitScope vars) ->
+      List.fold ~f:(fun acc var -> IdAccessPathMapDomain.remove var acc) ~init:id_map vars
   | Instr _ | Ignore ->
       id_map
 
@@ -80,14 +80,14 @@ struct
     let hil_translation =
       HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr
     in
-    let id_map' = update_id_map hil_translation id_map in
     let actual_state', id_map' =
       match hil_translation with
       | Instr hil_instr ->
-          exec_instr_actual extras id_map' node hil_instr actual_state
-      | Bind _ | Unbind _ | Ignore ->
-          (actual_state, id_map')
+          exec_instr_actual extras id_map node hil_instr actual_state
+      | Bind _ | Ignore ->
+          (actual_state, id_map)
     in
+    let id_map' = update_id_map hil_translation id_map' in
     if phys_equal id_map id_map' && phys_equal actual_state actual_state' then astate
     else (actual_state', id_map')
 end
@@ -111,7 +111,7 @@ struct
       match hil_translation with
       | Instr hil_instr ->
           Some (fun f -> Format.fprintf f "@[<h>%a@];@;" HilInstr.pp hil_instr)
-      | Bind _ | Unbind _ | Ignore ->
+      | Bind _ | Ignore ->
           None
     in
     Interpreter.compute_post ~pp_instr proc_data ~initial:initial' |> Option.map ~f:fst

infer/src/checkers/NullabilitySuggest.ml

@@ -111,6 +111,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           | None ->
               astate
         else astate
+    | ExitScope _ ->
+        astate
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "nullability suggest"

infer/src/checkers/Ownership.ml

@@ -371,6 +371,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             Domain.remove ret_id_typ astate' )
     | Assume (assume_exp, _, _, loc) ->
         Domain.exp_add_reads assume_exp loc summary astate
+    | ExitScope _ ->
+        astate
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "ownership"

infer/src/checkers/Pulse.ml

@@ -122,6 +122,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         PulseDomain.read_all loc (HilExp.get_access_exprs condition) astate |> check_error summary
     | Call (ret, call, actuals, flags, loc) ->
         dispatch_call ret call actuals flags loc astate |> check_error summary
+    | ExitScope vars ->
+        PulseDomain.remove_vars vars astate
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"

infer/src/checkers/PulseDomain.ml

@@ -611,6 +611,11 @@ module Operations = struct
     materialize_address astate access_expr location
     >>= fun (astate, addr) ->
     check_addr_access {access_expr; location} addr astate >>| mark_invalid cause addr
+
+
+  let remove_vars vars astate =
+    let stack = List.fold ~f:(fun var stack -> Stack.remove stack var) ~init:astate.stack vars in
+    if phys_equal stack astate.stack then astate else {astate with stack}
 end
 
 module StdVector = struct

infer/src/checkers/PulseDomain.mli

@@ -52,3 +52,5 @@ val write_var : Var.t -> AbstractAddress.t -> t -> t
 val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result
 
 val invalidate : PulseInvalidation.t -> Location.t -> AccessExpression.t -> t -> t access_result
+
+val remove_vars : Var.t list -> t -> t

infer/src/checkers/uninit.ml

@@ -298,7 +298,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         {astate with maybe_uninit_vars}
     | Assume (expr, _, _, loc) ->
         check_hil_expr expr ~loc ; astate
-
+    | ExitScope _ ->
+        astate
 
   let pp_session_name node fmt = F.fprintf fmt "uninit %a" CFG.Node.pp_id (CFG.Node.id node)
 end

infer/src/concurrency/RacerD.ml

@@ -591,6 +591,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           L.(die InternalError) "Unexpected indirect call instruction %a" HilInstr.pp instr
       | _ ->
           astate )
+    | ExitScope _ ->
+        astate
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "racerd"

infer/src/labs/ResourceLeaks.ml

@@ -85,6 +85,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Call (_, Indirect _, _, _, _) ->
         (* This should never happen in Java. Fail if it does. *)
         L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr
+    | ExitScope _ ->
+        astate
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks"

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -12,7 +12,6 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3,
 codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 24, column 3 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 102, column 3 here,accessed `s->f` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::FP_allocate_in_branch_ok, 9, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `std::unique_ptr<use_after_destructor::A,std::default_delete<use_after_destructor::A>>_~unique_ptr(a2)` at line 244, column 1 here,accessed `a1` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 64, column 3 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 142, column 3 here,accessed `s` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 150, column 3 here,accessed `alias` here]

infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp

@@ -232,7 +232,7 @@ void FP_destructor_order_empty_destructor_ok() {
   a.f = &b;
 }
 
-void FP_allocate_in_branch_ok(bool b) {
+void allocate_in_branch_ok(bool b) {
   std::unique_ptr<A> a1;
   std::unique_ptr<A> a2;
   std::unique_ptr<A>* a3 = &a1;