[clang] initialize dynamically-size stack-allocated arrays

Summary:
Previously all knowledge of the dynamic length of such arrays was lost to infer:
```
void foo(int len) {
    int a[len];
}
```
The translation of this program would make no reference to `len` (except as a
param of `foo`).

Translate this "initialization" using the existing `__set_array_length` infer
builtin, as:

```
   # Declare local a[_]
   n$0 = len;
   __set_array_length(a, len);
```

update-submodule: facebook-clang-plugins

Reviewed By: mbouaziz

Differential Revision: D4969446

fbshipit-source-id: dff860f

facebook-clang-plugins

@@ -1 +1 @@
-Subproject commit 84b3c58ab12fd42779ea4f8c1214432801cf4a5f
+Subproject commit 0c9c4d0ebb43c686143edb51c6e80e551df05b99

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -35,6 +35,10 @@ struct
 
   type extras = Typ.Procname.t -> Procdesc.t option
 
+  let set_uninitialized (typ : Typ.t) loc mem = match typ.desc with
+    | Tint _ | Tfloat _ -> Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem
+    | _ -> mem
+
   (* NOTE: heuristic *)
   let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t
     = function
@@ -49,13 +53,6 @@ struct
     = fun pname ret params node mem ->
       match ret with
       | Some (id, _) ->
-        let set_uninitialized typ loc mem =
-          match typ.Typ.desc with
-          | Typ.Tint _
-          | Typ.Tfloat _ ->
-            Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem
-          | _ -> mem
-        in
           let (typ, stride, length0) = get_malloc_info (List.hd_exn params |> fst) in
           let length = Sem.eval length0 mem (CFG.loc node) |> Dom.Val.get_itv in
           let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in
@@ -102,6 +99,21 @@ struct
           mem
       | _ -> mem
 
+  let model_infer_set_array_length pname node params mem loc =
+    match params with
+    | (Exp.Lvar array_pvar, {Typ.desc=Typ.Tarray (typ, _, stride0)})
+      :: (length_exp, _) :: [] ->
+        let length = Sem.eval length_exp mem loc |> Dom.Val.get_itv in
+        let stride = Option.map ~f:IntLit.to_int stride0 in
+        let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in
+        mem
+        |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v
+        |> set_uninitialized typ (Dom.Val.get_array_locs v)
+    | _ :: _ :: [] ->
+        failwithf "Unexpected type of arguments for __set_array_length()"
+    | _ ->
+        failwithf "Unexpected number of arguments for __set_array_length()"
+
   let handle_unknown_call
     : Typ.Procname.t -> (Ident.t * Typ.t) option -> Typ.Procname.t
       -> (Exp.t * Typ.t) list -> CFG.node -> Dom.Mem.astate -> Location.t
@@ -114,13 +126,14 @@ struct
       | "strlen" -> model_natual_itv ret mem
       | "fgetc" -> model_fgetc ret mem
       | "infer_print" -> model_infer_print params mem loc
+      | "__set_array_length" -> model_infer_set_array_length pname node params mem loc
       | _ -> model_unknown_itv ret mem
 
   let rec declare_array
-    : Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> length:IntLit.t -> ?stride:int
+    : Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> length:IntLit.t option -> ?stride:int
     -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate
     = fun pname node loc typ ~length ?stride ~inst_num ~dimension mem ->
-      let size = IntLit.to_int length |> Itv.of_int in
+      let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in
       let arr =
         Sem.eval_array_alloc pname node typ Itv.zero size ?stride inst_num dimension
       in
@@ -133,7 +146,7 @@ struct
         Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension)
       in
       match typ.Typ.desc with
-      | Typ.Tarray (typ, Some length, stride) ->
+      | Typ.Tarray (typ, length, stride) ->
           declare_array pname node loc typ ~length ?stride:(Option.map ~f:IntLit.to_int stride)
             ~inst_num ~dimension:(dimension + 1) mem
       | _ -> mem
@@ -244,7 +257,7 @@ struct
       let pname = Procdesc.get_proc_name pdesc in
       let try_decl_arr (mem, inst_num) (pvar, typ) =
         match typ.Typ.desc with
-        | Typ.Tarray (typ, Some length, stride0) ->
+        | Typ.Tarray (typ, length, stride0) ->
             let loc = Loc.of_pvar pvar in
             let stride = Option.map ~f:IntLit.to_int stride0 in
             let mem =

infer/src/bufferoverrun/itv.ml

@@ -859,6 +859,8 @@ let ub : t -> Bound.t
 let of_int : int -> astate
   = fun n -> NonBottom (ItvPure.of_int n)
 
+let of_int_lit n = of_int (IntLit.to_int n)
+
 let is_bot : t -> bool
   = fun x -> equal x Bottom
 

infer/src/clang/cTrans.ml

@@ -1676,11 +1676,37 @@ struct
         (* something's wrong *)
         { empty_res_trans with root_nodes = trans_state.succ_nodes }
 
-  and init_expr_trans trans_state var_exp_typ var_stmt_info init_expr_opt =
+  and init_dynamic_array trans_state array_exp_typ array_stmt_info dynlength_stmt_pointer =
+    let dynlength_stmt = Clang_ast_main.PointerMap.find dynlength_stmt_pointer
+        !CFrontend_config.pointer_stmt_index in
+    let dynlength_stmt_info, _ = Clang_ast_proj.get_stmt_tuple dynlength_stmt in
+    let trans_state_pri = PriorityNode.try_claim_priority_node trans_state array_stmt_info in
+    let dynlength_trans_result = instruction trans_state_pri dynlength_stmt in
+    let dynlength_exp_typ = extract_exp_from_list dynlength_trans_result.exps
+        "WARNING: There should be one expression.\n" in
+    let sil_loc = CLocation.get_sil_location dynlength_stmt_info trans_state_pri.context in
+    let call_instr =
+      let call_exp = Exp.Const (Const.Cfun BuiltinDecl.__set_array_length) in
+      let actuals = [array_exp_typ; dynlength_exp_typ] in
+      Sil.Call (None, call_exp, actuals, sil_loc, CallFlags.default) in
+    let call_trans_result = { empty_res_trans with instrs = [call_instr] } in
+    let res_trans = PriorityNode.compute_results_to_parent trans_state_pri sil_loc
+        "Initialize dynamic array length" dynlength_stmt_info
+        [dynlength_trans_result; call_trans_result] in
+    { res_trans with exps = [] }
+
+  and init_expr_trans trans_state var_exp_typ ?qual_type var_stmt_info init_expr_opt =
     match init_expr_opt with
-    | None ->
-        (* Nothing to do if no init expression *)
-        { empty_res_trans with root_nodes = trans_state.succ_nodes }
+    | None -> (
+        match Option.map ~f:(fun qt -> qt.Clang_ast_t.qt_type_ptr) qual_type
+              |> Option.find_map ~f:CAst_utils.get_type with
+        | Some (Clang_ast_t.VariableArrayType (_, _, stmt_pointer)) ->
+            (* Set the dynamic length of the variable length array. Variable length array cannot
+               have an initialization expression. *)
+            init_dynamic_array trans_state var_exp_typ var_stmt_info stmt_pointer
+        | _ ->
+            (* Nothing to do if no init expression and not a variable length array *)
+            { empty_res_trans with root_nodes = trans_state.succ_nodes})
     | Some ie -> (*For init expr, translate how to compute it and assign to the var*)
         let var_exp, _ = var_exp_typ in
         let context = trans_state.context in
@@ -1732,7 +1758,8 @@ struct
       let typ = CType_decl.qual_type_to_sil_type context.CContext.tenv qual_type in
       CVar_decl.add_var_to_locals procdesc var_decl typ pvar;
       let trans_state' = { trans_state with succ_nodes = next_node } in
-      init_expr_trans trans_state' (Exp.Lvar pvar, typ) stmt_info vdi.Clang_ast_t.vdi_init_expr in
+      init_expr_trans trans_state' (Exp.Lvar pvar, typ) ~qual_type stmt_info
+        vdi.Clang_ast_t.vdi_init_expr in
 
     match var_decls with
     | [] -> { empty_res_trans with root_nodes = next_nodes }

infer/src/clang/cType_to_sil_type.ml

@@ -97,7 +97,7 @@ and type_desc_of_c_type translate_decl tenv c_type : Typ.desc =
   | IncompleteArrayType (_, {arti_element_type; arti_stride})
   | DependentSizedArrayType (_, {arti_element_type; arti_stride}) ->
       build_array_type translate_decl tenv arti_element_type None arti_stride
-  | VariableArrayType (_, {arti_element_type; arti_stride}) ->
+  | VariableArrayType (_, {arti_element_type; arti_stride}, _) ->
       build_array_type translate_decl tenv arti_element_type None arti_stride
   | ConstantArrayType (_, {arti_element_type; arti_stride}, n) ->
       build_array_type translate_decl tenv arti_element_type (Some n) arti_stride

infer/tests/codetoanalyze/c/bufferoverrun/array_dynlength.c

@@ -0,0 +1,14 @@
+/*
+ * Copyright (c) 2013 - 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.
+ */
+
+void init_variable_array(int len) {
+  int x = 2 * len;
+  int a[len + x + 1];
+  a[len + x + 1] = 0;
+}

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

@@ -1,3 +1,4 @@
+codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1] @ codetoanalyze/c/bufferoverrun/array_dynlength.c:13:3]
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/break_continue_return.c:29:5]
 codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ]
 codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ]

infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c

@@ -7,7 +7,12 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  */
 
-int main() {
+int init_const_array() {
   int z;
   int a[2][3] = {{z + 1, 2, 3}, {5, 6, 7}};
 }
+
+void init_variable_array(int len) {
+  int x = 2 * len;
+  int a[len + x + 1];
+}

infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot

@@ -1,14 +1,29 @@
 /* @generated */
 digraph iCFG {
-"main.fad58de7366495db4650cfefac2fcd61_1" [label="1: Start main\nFormals: \nLocals:  a:int[3*32][2*96] z:int \n   DECLARE_LOCALS(&return,&a,&z); [line 10]\n " color=yellow style=filled]
+"init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_1" [label="1: Start init_const_array\nFormals: \nLocals:  a:int[3*32][2*96] z:int \n   DECLARE_LOCALS(&return,&a,&z); [line 10]\n " color=yellow style=filled]
 	
 
-	 "main.fad58de7366495db4650cfefac2fcd61_1" -> "main.fad58de7366495db4650cfefac2fcd61_3" ;
-"main.fad58de7366495db4650cfefac2fcd61_2" [label="2: Exit main \n  " color=yellow style=filled]
+	 "init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_1" -> "init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_3" ;
+"init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_2" [label="2: Exit init_const_array \n  " color=yellow style=filled]
 	
 
-"main.fad58de7366495db4650cfefac2fcd61_3" [label="3:  DeclStmt \n   n$0=*&z:int [line 12]\n  *&a[0][0]:int=(n$0 + 1) [line 12]\n  *&a[0][1]:int=2 [line 12]\n  *&a[0][2]:int=3 [line 12]\n  *&a[1][0]:int=5 [line 12]\n  *&a[1][1]:int=6 [line 12]\n  *&a[1][2]:int=7 [line 12]\n " shape="box"]
+"init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_3" [label="3:  DeclStmt \n   n$0=*&z:int [line 12]\n  *&a[0][0]:int=(n$0 + 1) [line 12]\n  *&a[0][1]:int=2 [line 12]\n  *&a[0][2]:int=3 [line 12]\n  *&a[1][0]:int=5 [line 12]\n  *&a[1][1]:int=6 [line 12]\n  *&a[1][2]:int=7 [line 12]\n " shape="box"]
 	
 
-	 "main.fad58de7366495db4650cfefac2fcd61_3" -> "main.fad58de7366495db4650cfefac2fcd61_2" ;
+	 "init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_3" -> "init_const_array.b1cf412cdbd1beaf15a9f6a3789043b9_2" ;
+"init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_1" [label="1: Start init_variable_array\nFormals:  len:int\nLocals:  a:int[_*32] x:int \n   DECLARE_LOCALS(&return,&a,&x); [line 15]\n " color=yellow style=filled]
+	
+
+	 "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_1" -> "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_4" ;
+"init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_2" [label="2: Exit init_variable_array \n  " color=yellow style=filled]
+	
+
+"init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_3" [label="3:  Fallback node \n   n$0=*&len:int [line 17]\n  n$1=*&x:int [line 17]\n  _fun___set_array_length(&a:int[_*32],((n$0 + n$1) + 1):int) [line 17]\n " shape="box"]
+	
+
+	 "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_3" -> "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_2" ;
+"init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_4" [label="4:  DeclStmt \n   n$2=*&len:int [line 16]\n  *&x:int=(2 * n$2) [line 16]\n " shape="box"]
+	
+
+	 "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_4" -> "init_variable_array.8cdc6857adcb1fd04fb6555d8ce3e4c1_3" ;
 }