[inferbo] Remove temporary logical variables

Reviewed By: jvillard

Differential Revision: D5432165

fbshipit-source-id: 8a9acba

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -372,7 +372,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                 "/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp loc
             in
             mem
-        | Remove_temps _ | Abstract _ | Nullify _
+        | Remove_temps (temps, _)
+         -> Dom.Mem.remove_temps temps mem
+        | Abstract _ | Nullify _
          -> mem
       in
       print_debug_info instr mem output_mem ; output_mem
@@ -621,6 +623,7 @@ let checker : Callbacks.proc_callback_args -> Specs.summary =
   fun {proc_desc; tenv; summary; get_proc_desc} ->
     let proc_name = Specs.get_proc_name summary in
     let proc_data = ProcData.make proc_desc tenv get_proc_desc in
+    if not (Procdesc.did_preanalysis proc_desc) then Preanal.do_liveness proc_desc tenv ;
     match compute_post proc_data with
     | Some post
      -> if Config.bo_debug >= 1 then print_summary proc_name post ;

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -447,6 +447,14 @@ module Stack = struct
         if Loc.is_logical_var k then () else F.fprintf fmt "%a -> %a@," Loc.pp k Val.pp_summary v
       in
       iter pp_not_logical_var mem
+
+  let remove_temps : Ident.t list -> astate -> astate =
+    fun temps mem ->
+      let remove_temp mem temp =
+        let temp_loc = Loc.of_id temp in
+        remove temp_loc mem
+      in
+      List.fold temps ~init:mem ~f:remove_temp
 end
 
 module Heap = struct
@@ -552,6 +560,11 @@ module AliasMap = struct
     fun k m ->
       try Some (M.find k m)
       with Not_found -> None
+
+  let remove_temps : Ident.t list -> t -> t =
+    fun temps m ->
+      let remove_temp m temp = M.remove temp m in
+      List.fold temps ~init:m ~f:remove_temp
 end
 
 module AliasRet = struct
@@ -620,6 +633,9 @@ module Alias = struct
           Option.value_map (find l a) ~default:a ~f:update_ret
       | _
        -> a
+
+  let remove_temps : Ident.t list -> astate -> astate =
+    fun temps a -> (AliasMap.remove_temps temps (fst a), snd a)
 end
 
 module MemReach = struct
@@ -715,6 +731,10 @@ module MemReach = struct
           L.(debug BufferOverrun Verbose) "Weak update for %a <- %a@." PowLoc.pp ploc Val.pp v
         in
         weak_update_heap ploc v s
+
+  let remove_temps : Ident.t list -> t -> t =
+    fun temps m ->
+      {m with stack= Stack.remove_temps temps m.stack; alias= Alias.remove_temps temps m.alias}
 end
 
 module Mem = struct
@@ -784,6 +804,8 @@ module Mem = struct
   let can_strong_update : PowLoc.t -> bool = MemReach.can_strong_update
 
   let update_mem : PowLoc.t -> Val.t -> t -> t = fun ploc v -> f_lift (MemReach.update_mem ploc v)
+
+  let remove_temps : Ident.t list -> t -> t = fun temps -> f_lift (MemReach.remove_temps temps)
 end
 
 module Summary = struct

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

@@ -6,6 +6,9 @@ codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 7, BUFFER_OVERRUN, [Ar
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 8, BUFFER_OVERRUN, [Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
+codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, []
+codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
+codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Call,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [42, 42] Size: [42, 42] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ]

infer/tests/codetoanalyze/cpp/bufferoverrun/remove_temps.cpp

@@ -0,0 +1,39 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#include <vector>
+
+struct S {
+  std::vector<int> l;
+  S* next;
+  std::atomic<void*> ptr;
+};
+
+class C {
+  void foo_Bad();
+  void goo();
+  S head_;
+};
+
+void C::foo_Bad() {
+  while (1) {
+    S* t = head_.next;
+    int x = t->l.size();
+    void* ptr = t->ptr;
+    int a[5];
+    a[10] = 1;
+  }
+}
+
+void C::goo() {
+  while (1) {
+    S* t = head_.next;
+    int x = t->l.size();
+    void* ptr = t->ptr;
+  }
+}