[inferbo] Handle when const global assigned to local variable

Summary:
Before this diff:

```
// Summary of const global
// { global -> v }

n$0 =* global
// n$0 -> {global}
x *= n$0
// x -> {global}
```

However, this is incorrect because we expect `x` have `v` instead of the abstract location of `global`.

To fix the issue, this diff lookups the initializer summary when `global` is evaluated as RHS of load statement.

After this diff:

```
// Summary of const global
// { global -> v }

n$0 =* global
// n$0 -> v
x *= n$0
// x -> v
```

Reviewed By: ezgicicek

Differential Revision: D26369645

fbshipit-source-id: 98b1ed085

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -152,7 +152,7 @@ let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
         Mem.find_stack (Var.of_id id |> Loc.of_var) mem
     | Exp.Lvar pvar ->
         let loc = Loc.of_pvar pvar in
-        if Mem.is_stack_loc loc mem then Mem.find loc mem else Val.of_loc loc
+        if Mem.is_stack_loc loc mem || Loc.is_global loc then Mem.find loc mem else Val.of_loc loc
     | Exp.UnOp (uop, e, _) ->
         eval_unop integer_type_widths uop e mem
     | Exp.BinOp (bop, e1, e2) -> (

infer/tests/codetoanalyze/c/performance/cost-issues.exp

@@ -62,7 +62,7 @@ codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 227,  OnUIThread
 codetoanalyze/c/performance/loops.c, if_in_loop, 323,  OnUIThread:false, []
 codetoanalyze/c/performance/loops.c, if_out_loop, 514,  OnUIThread:false, []
 codetoanalyze/c/performance/loops.c, larger_state_FN, 1004,  OnUIThread:false, []
-codetoanalyze/c/performance/loops.c, loop_use_global_vars, 3 + 4 ⋅ x + 2 ⋅ (1+max(0, x)),  OnUIThread:false, [{1+max(0, x)},Loop,{x},Loop]
+codetoanalyze/c/performance/loops.c, loop_use_global_vars, 2 + 4 ⋅ x + 2 ⋅ (1+max(0, x)),  OnUIThread:false, [{1+max(0, x)},Loop,{x},Loop]
 codetoanalyze/c/performance/loops.c, ptr_cmp, 4 + 5 ⋅ size + 2 ⋅ (2+max(-1, size)),  OnUIThread:false, [{2+max(-1, size)},Loop,{size},Loop]
 codetoanalyze/c/performance/purity.c, loop, 6006 + 1000 ⋅ |fun_ptr|,  OnUIThread:false, []
 codetoanalyze/c/performance/switch_continue.c, test_switch_FN, 600,  OnUIThread:false, []

infer/tests/codetoanalyze/c/performance/issues.exp

@@ -27,6 +27,7 @@ codetoanalyze/c/performance/exit.c, compute_exit_unreachable, 0, EXECUTION_TIME_
 codetoanalyze/c/performance/exit.c, exit_unreachable, 0, EXECUTION_TIME_UNREACHABLE_AT_EXIT, no_bucket, ERROR, [Unreachable node]
 codetoanalyze/c/performance/invariant.c, while_infinite_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/loops.c, if_in_loop, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/switch_continue.c, test_switch_FN, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp

@@ -11,7 +11,7 @@ void access_constant_global_Bad() {
   a[ConstantGlobal[0]] = 3;
 }
 
-void access_via_assignment_constant_global_Bad_FN() {
+void access_via_assignment_constant_global_Bad() {
   int a[5];
   const int* arr = ConstantGlobal;
   a[arr[0]] = 3;

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

@@ -52,6 +52,7 @@ codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_loop_with_init_S_Bad, 2,
 codetoanalyze/cpp/bufferoverrun/global.cpp, access_constant_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global1_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 3]
+codetoanalyze/cpp/bufferoverrun/global.cpp, access_via_assignment_constant_global_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Set array size,Assignment,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Set array size,Array access: Offset: 7 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Set array size,Assignment,Array access: Offset: 5 Size: 5]

infer/tests/codetoanalyze/objc/performance/cost-issues.exp

@@ -223,7 +223,7 @@ codetoanalyze/objc/performance/loops.m, do_while_independent_of_p, 227,  OnUIThr
 codetoanalyze/objc/performance/loops.m, if_in_loop, 323,  OnUIThread:false, []
 codetoanalyze/objc/performance/loops.m, if_out_loop, 514,  OnUIThread:false, []
 codetoanalyze/objc/performance/loops.m, larger_state_FN, 1004,  OnUIThread:false, []
-codetoanalyze/objc/performance/loops.m, loop_use_global_vars, 3 + 4 ⋅ x + 2 ⋅ (1+max(0, x)),  OnUIThread:false, [{1+max(0, x)},Loop,{x},Loop]
+codetoanalyze/objc/performance/loops.m, loop_use_global_vars, 2 + 4 ⋅ x + 2 ⋅ (1+max(0, x)),  OnUIThread:false, [{1+max(0, x)},Loop,{x},Loop]
 codetoanalyze/objc/performance/loops.m, ptr_cmp, 4 + 5 ⋅ size + 2 ⋅ (2+max(-1, size)),  OnUIThread:false, [{2+max(-1, size)},Loop,{size},Loop]
 codetoanalyze/objc/performance/mutable_copy_test.m, MyMutableObj.dealloc, 3,  OnUIThread:false, []
 codetoanalyze/objc/performance/mutable_copy_test.m, MyMutableObj.mObjects, 3,  OnUIThread:false, []

infer/tests/codetoanalyze/objc/performance/issues.exp

@@ -45,6 +45,7 @@ codetoanalyze/objc/performance/exit.m, exit_unreachable, 0, EXECUTION_TIME_UNREA
 codetoanalyze/objc/performance/field_access.m, create_common_person_constant, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `self->_bank_account`,Call,<LHS trace>,Parameter `self->_bank_account`,Call,Parameter `self->_bank_account`,Assignment,<RHS trace>,Parameter `income`,Binary operation: ([0, +oo] + 100):unsigned64 by call to `Person.add_income_constant:` ]
 codetoanalyze/objc/performance/invariant.m, while_infinite_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/loops.m, if_in_loop, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/objc/performance/loops.m, loop_use_global_vars, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/switch_continue.m, test_switch_FN, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/switch_continue.m, unroll_loop, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/objc/performance/switch_continue.m, unroll_loop, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]