Recognize more cases of zero-initialized arrays. Refine hoisting phas…

…e to be nested-arrays aware.

lib/CStarToC11.ml

@@ -213,14 +213,23 @@ let bytes_in = function
  * had static storage duration, i.e. with zero.). For prettyness, leave at least
  * one zero, unless the array was empty to start with (admissible with globals). *)
 let trim_trailing_zeros l =
-  let rec trim_trailing_zeros = function
-    | CStar.Constant (_, "0") :: tl -> trim_trailing_zeros tl
-    | [] -> [ CStar.Constant (K.UInt32, "0") ]
+  let rec all_zeros = function
+    | InitExpr (C11.Constant (_, "0")) -> true
+    | InitExpr (C11.Cast (_, Constant (_, "0"))) -> true
+    | Initializer inits -> List.for_all all_zeros inits
+    | _ -> false
+  in
+
+  let rec trim_trailing_zeros: C11.init list -> C11.init list = function
+    | hd :: tl when all_zeros hd -> trim_trailing_zeros tl
+    | [] -> [ InitExpr (C11.Constant (K.UInt32, "0")) ]
     | l -> List.rev l
   in
+
   match l with
-  | [] -> []
-  | _ -> trim_trailing_zeros (List.rev l)
+  | Initializer [] -> Initializer []
+  | Initializer l -> Initializer (trim_trailing_zeros (List.rev l))
+  | l -> l
 
 (* Turns the ML declaration inside-out to match the C reading of a type.
  *   See: en.cppreference.com/w/c/language/declarations.
@@ -627,17 +636,21 @@ and mk_stmt m (stmt: stmt): C.stmt list =
         uses createL, but we don't have (yet) codegen for this:\n" ^
         CStar.show_stmt s)
 
-  | Decl (binder, BufCreateL (Stack, inits)) ->
+  | Decl (binder, (BufCreateL (Stack, inits) as init_expr)) ->
       (* Per the C standard, static initializers guarantee for missing fields
        * that they're initialized as if they had static storage duration, i.e.
        * with zero. *)
       let t = ensure_array binder.typ (Constant (K.uint32_of_int (List.length inits))) in
       let alignment = mk_alignment m (assert_array t) in
-      let inits = trim_trailing_zeros inits in
       let qs, spec, decl = mk_spec_and_declarator m binder.name t in
-      [ Decl (qs, spec, None, None, { maybe_unused = false }, [ decl, alignment, Some (Initializer (List.map (fun e ->
-        InitExpr (mk_expr m e)
-      ) inits))])]
+      let rec to_initializer = function
+        | BufCreateL (Stack, inits) ->
+            Initializer (List.map to_initializer inits)
+        | e ->
+            InitExpr (mk_expr m e)
+      in
+      let init_expr = trim_trailing_zeros (to_initializer init_expr) in
+      [ Decl (qs, spec, None, None, { maybe_unused = false }, [ decl, alignment, Some init_expr])]
 
   | Decl (binder, e) ->
       let qs, spec, decl = mk_spec_and_declarator m binder.name binder.typ in
@@ -1119,10 +1132,10 @@ let mk_function_or_global_body m (d: decl): C.declaration_or_function list =
         | Any ->
             wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, static, extra, [ decl, alignment, None ])))
         | BufCreateL (_, es) ->
-            let es = trim_trailing_zeros es in
             let es = List.map (struct_as_initializer m) es in
+            let es = trim_trailing_zeros (Initializer es) in
             wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, static, extra, [
-              decl, alignment, Some (Initializer es) ])))
+              decl, alignment, Some es ])))
         (* Global static arrays of arithmetic type are initialized implicitly to 0 *)
         | BufCreate (_, Constant (_, "0"), _)
         | BufCreate (_, CStar.Bool false, _)

lib/Simplify.ml

@@ -898,6 +898,21 @@ let rec flag_short_circuit loc t e0 es =
       let lhs = lhs0 @ List.flatten lhss in
       lhs, with_type t (EApp (e0, es))
 
+(* When allocating an array, whether the initial elements of the array need to
+   be hoisted depend on the type; if it's an array of pointers, yes, we host. If
+   it's an array of arrays, we leave initializer lists in order to fill storage.
+   *)
+and maybe_hoist_initializer loc t e =
+  match e.node with
+  | EBufCreate _ when Helpers.is_array t ->
+      failwith "expected EBufCreateL here"
+  | EBufCreateL (l, es) when Helpers.is_array t ->
+      let lhs, es = List.split (List.map (maybe_hoist_initializer loc (Helpers.assert_tarray t)) es) in
+      let lhs = List.flatten lhs in
+      lhs, with_type t (EBufCreateL (l, es))
+  | _ ->
+      hoist_expr loc Unspecified e
+
 and hoist_stmt loc e =
   let mk = with_type e.typ in
   match e.node with
@@ -1136,7 +1151,7 @@ and hoist_expr loc pos e =
   | EBufCreate (l, e1, e2) ->
       let t = e.typ in
       let lhs1, e1 = hoist_expr loc Unspecified e1 in
-      let lhs2, e2 = hoist_expr loc Unspecified e2 in
+      let lhs2, e2 = maybe_hoist_initializer loc (Helpers.assert_tbuf_or_tarray t) e2 in
       if pos = UnderStmtLet then
         lhs1 @ lhs2, mk (EBufCreate (l, e1, e2))
       else
@@ -1145,7 +1160,7 @@ and hoist_expr loc pos e =
 
   | EBufCreateL (l, es) ->
       let t = e.typ in
-      let lhs, es = List.split (List.map (hoist_expr loc Unspecified) es) in
+      let lhs, es = List.split (List.map (maybe_hoist_initializer loc (Helpers.assert_tbuf_or_tarray t)) es) in
       let lhs = List.flatten lhs in
       if pos = UnderStmtLet then
         lhs, mk (EBufCreateL (l, es))