From c09068e3bfee81a624cf158042c839ee5e432ba2 Mon Sep 17 00:00:00 2001
From: Daiva Naudziuniene <daivan@fb.com>
Date: Fri, 21 Dec 2018 06:35:28 -0800
Subject: [PATCH] [HIL] Preserve ExitScope location information in the
 translation from SIL

Summary: The title

Reviewed By: ngorogiannis

Differential Revision: D13537402

fbshipit-source-id: bee7b3662
---
 infer/src/IR/HilInstr.ml     | 10 +++++-----
 infer/src/IR/HilInstr.mli    |  2 +-
 infer/src/absint/LowerHil.ml |  4 ++--
 infer/src/checkers/Pulse.ml  |  2 +-
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml
index bf348f0e2..d27f831a0 100644
--- a/infer/src/IR/HilInstr.ml
+++ b/infer/src/IR/HilInstr.ml
@@ -22,7 +22,7 @@ type t =
   | Assign of HilExp.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
+  | ExitScope of Var.t list * Location.t
 [@@deriving compare]
 
 let pp fmt = function
@@ -35,8 +35,8 @@ 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
+  | ExitScope (vars, loc) ->
+      F.fprintf fmt "exit scope(%a) [%a]" (Pp.seq ~sep:"; " Var.pp) vars Location.pp loc
 
 
 type translation = Instr of t | Bind of Var.t * HilExp.AccessExpression.t | Ignore
@@ -121,8 +121,8 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) =
       let hil_exp = exp_of_sil exp (Typ.mk (Tint IBool)) in
       let branch = if true_branch then `Then else `Else in
       Instr (Assume (hil_exp, branch, if_kind, loc))
-  | ExitScope (vars, _) ->
-      Instr (ExitScope vars)
+  | ExitScope (vars, loc) ->
+      Instr (ExitScope (vars, loc))
   | Abstract _ | Nullify _ ->
       (* these don't seem useful for most analyses. can translate them later if we want to *)
       Ignore
diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli
index cdc86a8c5..83950555d 100644
--- a/infer/src/IR/HilInstr.mli
+++ b/infer/src/IR/HilInstr.mli
@@ -18,7 +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
+  | ExitScope of Var.t list * Location.t
 [@@deriving compare]
 
 val pp : F.formatter -> t -> unit
diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml
index 27466f63f..a924e2134 100644
--- a/infer/src/absint/LowerHil.ml
+++ b/infer/src/absint/LowerHil.ml
@@ -72,13 +72,13 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
         (None, bindings)
     | Bind (id, access_path) ->
         (None, Bindings.add id access_path bindings)
-    | Instr (ExitScope vars) ->
+    | Instr (ExitScope (vars, loc)) ->
         let bindings, vars =
           List.fold vars ~init:(bindings, []) ~f:(fun (bindings, vars) var ->
               let bindings, vars' = Bindings.exit_scope var bindings in
               (bindings, append_bindings vars vars') )
         in
-        let instr = if List.is_empty vars then None else Some (HilInstr.ExitScope vars) in
+        let instr = if List.is_empty vars then None else Some (HilInstr.ExitScope (vars, loc)) in
         (instr, bindings)
     | Instr instr ->
         (Some instr, bindings)
diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml
index 0359d6492..379f94855 100644
--- a/infer/src/checkers/Pulse.ml
+++ b/infer/src/checkers/Pulse.ml
@@ -136,7 +136,7 @@ module PulseTransferFunctions (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 summary ret call actuals flags loc astate |> check_error summary
-    | ExitScope vars ->
+    | ExitScope (vars, _) ->
         PulseDomain.remove_vars vars astate