[inferbo] Use values of global constant variables in C

Reviewed By: mbouaziz

Differential Revision: D12838577

fbshipit-source-id: 8e7c45596

infer/src/IR/Pvar.ml

@@ -256,6 +256,8 @@ let is_compile_constant pvar =
   match pvar.pv_kind with Global_var {is_constexpr} -> is_constexpr | _ -> false
 
 
+let is_ice pvar = match pvar.pv_kind with Global_var {is_ice} -> is_ice | _ -> false
+
 let is_pod pvar = match pvar.pv_kind with Global_var {is_pod} -> is_pod | _ -> true
 
 let get_initializer_pname {pv_name; pv_kind} =

infer/src/IR/Pvar.mli

@@ -130,6 +130,10 @@ val is_compile_constant : t -> bool
 (** Is the variable's value a compile-time constant? Always (potentially incorrectly) returns
     [false] for non-globals. *)
 
+val is_ice : t -> bool
+(** Is the variable's type an integral constant expression? Always (potentially incorrectly) returns
+    [false] for non-globals. *)
+
 val is_pod : t -> bool
 (** Is the variable's type a "Plain Old Data" type (C++)? Always (potentially incorrectly) returns
     [true] for non-globals. *)

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -145,7 +145,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     match instr with
     | Load (id, _, _, _) when Ident.is_none id ->
         mem
-    | Load (id, Exp.Lvar pvar, _, location) when Pvar.is_compile_constant pvar -> (
+    | Load (id, Exp.Lvar pvar, _, location) when Pvar.is_compile_constant pvar || Pvar.is_ice pvar
+      -> (
       match Pvar.get_initializer_pname pvar with
       | Some callee_pname -> (
         match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with

infer/tests/codetoanalyze/c/bufferoverrun/global.c

@@ -21,3 +21,15 @@ void compare_global_const_enum_bad_FN() {
   if (global_const < 10)
     arr[10] = 1;
 }
+
+const int global_const_ten = 10;
+
+void use_global_const_ten_Good() {
+  char arr[20];
+  arr[global_const_ten] = 0;
+}
+
+void use_global_const_ten_Bad() {
+  char arr[5];
+  arr[global_const_ten] = 0;
+}

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

@@ -64,6 +64,7 @@ codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OV
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Assignment,Binop: ([1, +oo] + 1):signed32]