Avoid linear AST expansion for local array initializers

[admkopec]

Fixes #602.

Change

When lowering a local array declaration, Unblock currently emits a separate assignment AST node for every element not explicitly listed in the initializer. Consequently, the AST and compiler memory usage grow with the declared array bound even when the initializer has a fixed source size, such as { 0 }.

This PR retains the existing individual assignments for explicitly initialized elements and represents the remaining implicit tail with a counted Sfor loop. The generated loop uses a unique compiler-created size_t index.

For each omitted element, the loop body performs the same type-specific initialization as the current lowering. This includes recursive initialization of nested arrays and structures, as well as typed initialization of pointers, floating-point values, and volatile subobjects.

As a result, the generated AST no longer grows with the number of omitted array elements. The change constructs only existing assignment and Sfor AST nodes and does not modify any verified compiler pass or proof.

Scope

The change applies to automatic declaration initializers handled by process_decl. Global and static initializers are unchanged.

Local compound literals retain the existing expression-based lowering because supporting statement-level loops there requires separate handling of expression sequence points.

I can also propose some regression tests into CompCert-small-tests once the lowering approach is reviewed.

Validation

Tested from CompCert 3.18 commit 66a9fd06:

• completed a full CompCert build, including proofs, extraction, ccomp, and the runtime library,
• compiled the complete existing regression suite,
• completed make test SIMU=qemu-x86_64,
• verified bounded post-Unblock output for a 100,000-element array.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.