From 9cdd87b67bb8c8bff894be16d276e6767601cf37 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 10 Feb 2021 10:27:41 -0800 Subject: [PATCH] [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 | 2 +- infer/tests/codetoanalyze/c/performance/cost-issues.exp | 2 +- infer/tests/codetoanalyze/c/performance/issues.exp | 1 + infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp | 2 +- infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp | 1 + infer/tests/codetoanalyze/objc/performance/cost-issues.exp | 2 +- infer/tests/codetoanalyze/objc/performance/issues.exp | 1 + 7 files changed, 7 insertions(+), 4 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index b12c05fd9..838828c42 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/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) -> ( diff --git a/infer/tests/codetoanalyze/c/performance/cost-issues.exp b/infer/tests/codetoanalyze/c/performance/cost-issues.exp index 3e9f51e9e..669effa06 100644 --- a/infer/tests/codetoanalyze/c/performance/cost-issues.exp +++ b/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, [] diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index 259e622f7..990dd616b 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/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, [,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, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/switch_continue.c, unroll_loop, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp index e7fab752e..50a8fbce8 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp +++ b/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; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 6b5c23524..8a7207f69 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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, [,Assignment,,Array declaration,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global1_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,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, [,Assignment,,Array declaration,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,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, [,Set array size,Array access: Offset: 7 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Set array size,Assignment,Array access: Offset: 5 Size: 5] diff --git a/infer/tests/codetoanalyze/objc/performance/cost-issues.exp b/infer/tests/codetoanalyze/objc/performance/cost-issues.exp index 1b8359b17..29b958fcb 100644 --- a/infer/tests/codetoanalyze/objc/performance/cost-issues.exp +++ b/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, [] diff --git a/infer/tests/codetoanalyze/objc/performance/issues.exp b/infer/tests/codetoanalyze/objc/performance/issues.exp index 93b3487e1..4b7784783 100644 --- a/infer/tests/codetoanalyze/objc/performance/issues.exp +++ b/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,,Parameter `self->_bank_account`,Call,Parameter `self->_bank_account`,Assignment,,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, [,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, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/objc/performance/switch_continue.m, unroll_loop, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]