[preanalysis] do not nullify vars captured by ref

Summary:
Nullifying these leads to observable side-effects, like in the added
test.

Reviewed By: da319

Differential Revision: D23759756

fbshipit-source-id: 559a6486b

infer/src/backend/preanal.ml

@@ -229,23 +229,24 @@ module Liveness = struct
   module NullifyAnalysis = AbstractInterpreter.MakeRPO (NullifyTransferFunctions)
 
   let add_nullify_instrs summary tenv liveness_inv_map =
+    let proc_desc = Summary.get_proc_desc summary in
     let address_taken_vars =
       if Procname.is_java (Summary.get_proc_name summary) then AddressTaken.Domain.empty
         (* can't take the address of a variable in Java *)
       else
         let initial = AddressTaken.Domain.empty in
-        match AddressTaken.Analyzer.compute_post () ~initial (Summary.get_proc_desc summary) with
+        match AddressTaken.Analyzer.compute_post () ~initial proc_desc with
         | Some post ->
             post
         | None ->
             AddressTaken.Domain.empty
     in
-    let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc (Summary.get_proc_desc summary) in
+    let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in
     let nullify_proc_data = {ProcData.summary; tenv; extras= liveness_inv_map} in
     let initial = (VarDomain.empty, VarDomain.empty) in
     let nullify_inv_map = NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data ~initial in
     (* only nullify pvars that are local; don't nullify those that can escape *)
-    let is_local pvar = not (Pvar.is_return pvar || Pvar.is_global pvar) in
+    let is_local pvar = not (Liveness.is_always_in_scope proc_desc pvar) in
     let prepend_node_nullify_instructions loc pvars instrs =
       List.fold pvars ~init:instrs ~f:(fun instrs pvar ->
           if is_local pvar then Sil.Metadata (Nullify (pvar, loc)) :: instrs else instrs )
@@ -295,9 +296,10 @@ module Liveness = struct
 
 
   let process summary tenv =
-    let liveness_proc_cfg = BackwardCfg.from_pdesc (Summary.get_proc_desc summary) in
+    let proc_desc = Summary.get_proc_desc summary in
+    let liveness_proc_cfg = BackwardCfg.from_pdesc proc_desc in
     let initial = Liveness.Domain.empty in
-    let liveness_inv_map = LivenessAnalysis.exec_cfg liveness_proc_cfg () ~initial in
+    let liveness_inv_map = LivenessAnalysis.exec_cfg liveness_proc_cfg proc_desc ~initial in
     add_nullify_instrs summary tenv liveness_inv_map
 end
 

infer/src/checkers/liveness.ml

@@ -15,7 +15,9 @@ module VarSet = AbstractDomain.FiniteSet (Var)
 module Domain = VarSet
 
 (** only kill pvars that are local; don't kill those that can escape *)
-let is_always_in_scope pvar = Pvar.is_return pvar || Pvar.is_global pvar
+let is_always_in_scope proc_desc pvar =
+  Pvar.is_return pvar || Pvar.is_global pvar || Procdesc.is_captured_pvar proc_desc pvar
+
 
 let json_error ~option_name ~expected ~actual =
   L.die UserError "When parsing option %s: expected %s but got '%s'" option_name expected
@@ -92,7 +94,7 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = Domain
 
-  type analysis_data = unit
+  type analysis_data = Procdesc.t
 
   (** add all of the vars read in [exp] to the live set *)
   let exp_add_live exp astate =
@@ -122,7 +124,7 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct
         add_live_actuals_ actuals live_acc
 
 
-  let exec_instr astate () _ = function
+  let exec_instr astate proc_desc _ = function
     | Sil.Load {id= lhs_id} when Ident.is_none lhs_id ->
         (* dummy deref inserted by frontend--don't count as a read *)
         astate
@@ -130,7 +132,7 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct
         Domain.remove (Var.of_id lhs_id) astate |> exp_add_live rhs_exp
     | Sil.Store {e1= Lvar lhs_pvar; e2= rhs_exp} ->
         let astate' =
-          if is_always_in_scope lhs_pvar then astate (* never kill globals *)
+          if is_always_in_scope proc_desc lhs_pvar then astate (* never kill globals *)
           else Domain.remove (Var.of_pvar lhs_pvar) astate
         in
         exp_add_live rhs_exp astate'
@@ -147,7 +149,7 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct
         let actuals_to_read, astate =
           if cf_assign_last_arg then
             match IList.split_last_rev actuals with
-            | Some ((Exp.Lvar pvar, _), actuals') when not (is_always_in_scope pvar) ->
+            | Some ((Exp.Lvar pvar, _), actuals') when not (is_always_in_scope proc_desc pvar) ->
                 (actuals', Domain.remove (Var.of_pvar pvar) astate)
             | _ ->
                 (actuals, astate)
@@ -213,7 +215,7 @@ let get_captured_by_ref_invariant_map proc_desc =
 let checker {IntraproceduralAnalysis.proc_desc; err_log} =
   let captured_by_ref_invariant_map = get_captured_by_ref_invariant_map proc_desc in
   let cfg = CFG.from_pdesc proc_desc in
-  let invariant_map = CheckerAnalyzer.exec_cfg cfg () ~initial:Domain.empty in
+  let invariant_map = CheckerAnalyzer.exec_cfg cfg proc_desc ~initial:Domain.empty in
   (* we don't want to report in harmless cases like int i = 0; if (...) { i = ... } else { i = ... }
      that create an intentional dead store as an attempt to imitate default value semantics.
      use dead stores to a "sentinel" value as a heuristic for ignoring this case *)

infer/src/checkers/liveness.mli

@@ -14,6 +14,8 @@ module PreAnalysisTransferFunctions (CFG : ProcCfg.S) :
   TransferFunctions.SIL
     with module CFG = CFG
      and module Domain = Domain
-     and type analysis_data = unit
+     and type analysis_data = Procdesc.t
 
 val checker : IntraproceduralAnalysis.t -> unit
+
+val is_always_in_scope : Procdesc.t -> Pvar.t -> bool

infer/src/unit/livenessTests.ml

@@ -99,6 +99,8 @@ let tests =
         ; While (unknown_cond, [id_assign_var "b" "d"])
         ; invariant "{ b }"
         ; id_assign_var "a" "b" ] ) ]
-    |> TestInterpreter.create_tests (fun _summary -> ()) ~initial:Liveness.Domain.empty
+    |> TestInterpreter.create_tests
+         (fun summary -> Summary.get_proc_desc summary)
+         ~initial:Liveness.Domain.empty
   in
   "liveness_test_suite" >::: test_list

infer/tests/codetoanalyze/cpp/biabduction/npe/lambdas.cpp

@@ -0,0 +1,13 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int capture_by_ref_ok(int s) {
+  auto f = [&]() { return s; };
+  int x = f();
+  int y = f();
+  return x + y;
+}