[inferbo] Translate re-declared globals to point to original ones

Summary:
Re-declarations of global variables sometimes hide constant
initializations in the original declaration, which caused FN before.
In this diff, it translates global variables to point to original
declarations, rather than following re-declarations, if possible.

Reviewed By: mbouaziz, jvillard

Differential Revision: D14596301

fbshipit-source-id: 55c3b5f95

infer/src/clang/cAst_utils.ml

@@ -75,7 +75,34 @@ let dummy_stmt_info () =
   {Clang_ast_t.si_pointer= get_fresh_pointer (); si_source_range= dummy_source_range ()}
 
 
-let get_decl decl_ptr = Int.Table.find ClangPointers.pointer_decl_table decl_ptr
+let named_decl_info_equal ndi1 ndi2 =
+  match
+    List.for_all2 ndi1.Clang_ast_t.ni_qual_name ndi2.Clang_ast_t.ni_qual_name ~f:String.equal
+  with
+  | List.Or_unequal_lengths.Ok b ->
+      b
+  | List.Or_unequal_lengths.Unequal_lengths ->
+      false
+
+
+let get_decl decl_ptr =
+  let decl = Int.Table.find ClangPointers.pointer_decl_table decl_ptr in
+  match decl with
+  | Some (VarDecl ({di_parent_pointer= Some parent_pointer}, ndi, _, _)) -> (
+    match Int.Table.find ClangPointers.pointer_decl_table parent_pointer with
+    | Some (CXXRecordDecl (_, _, _, decls, _, _, _, _)) -> (
+        let has_same_ndi = function
+          | Clang_ast_t.VarDecl (_, ndi', _, _) ->
+              named_decl_info_equal ndi ndi'
+          | _ ->
+              false
+        in
+        match List.find decls ~f:has_same_ndi with Some _ as decl' -> decl' | None -> decl )
+    | _ ->
+        decl )
+  | _ ->
+      decl
+
 
 let get_decl_opt decl_ptr_opt =
   match decl_ptr_opt with Some decl_ptr -> get_decl decl_ptr | None -> None

infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp

@@ -298,7 +298,7 @@ void use_global_2_Good() {
   a[S::x] = 0;
 }
 
-void use_global_2_Bad_FN() {
+void use_global_2_Bad() {
   int a[30];
   a[S::x] = 0;
 }

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

@@ -31,6 +31,7 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Call,Array access: Offset: 5 Size: 5]
+codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
 codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ]
 codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*ptr`,Assignment,Assignment,Array access: Offset: 2 Size: 1 by call to `conditional_buffer_access` ]