Skip to content

[DRAFT] Initialisers support - #1015

Draft
dc-mak wants to merge 11 commits into
rems-project:masterfrom
dc-mak:initialisers-completion
Draft

[DRAFT] Initialisers support#1015
dc-mak wants to merge 11 commits into
rems-project:masterfrom
dc-mak:initialisers-completion

Conversation

@dc-mak

@dc-mak dc-mak commented Sep 8, 2026

Copy link
Copy Markdown
Collaborator

No description provided.

dc-mak and others added 11 commits September 7, 2026 15:37
The desugaring of C11 6.7.9 initialisers now goes through the cursor
machine in desugaring_init.lem (via wip_desugar_initializer_). The
earlier, superseded implementation was still sitting in cabs_to_ail.lem
but was only reachable from a commented-out call site.

Remove it: the init_element/init_path types and their printers,
elemPathFromCtype3 and its helpers (skipTo, mk_elemsPathFromCtype,
cardinalityOfCtype, innerCtype, _UNUSED_ctypeAtPath,
_UNUSED_outerValidPath), the duplicate constructValue,
_UNUSED_is_fully_non_designated, _UNUSED_static_thread_implicit_initializer,
and the pathFromDesigs/foo_aux/bar/foo cluster, along with the
commented-out block that called them.

No behaviour change: none of these were reachable. This also removes a
dozen TODOs describing limitations of the dead implementation
("TODO: foo_aux, Init_expr ==> union" and friends) that made the state
of initialiser support look worse than it is, and leaves
desugaring_init.lem as the single source of truth.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
Before changing the §6.7.9 cursor machine in desugaring_init.lem, pin
down the parts that already behave correctly, so that later fixes cannot
silently regress them:

  0342  brace elision (array of structs, multidimensional arrays,
        partially braced arrays, a struct containing an array)
  0343  designators (§6.7.9#17 continuation, out-of-order and sparse
        array designators, unknown-size arrays sized from the largest
        index, nested designators)
  0344  anonymous struct/union members addressed by designator from the
        parent, and by brace elision

Also drop 0083-array_initializers.c from the skip list. It was marked
"REAL BUG(!) -- Desugaring of initializers", but it passes: the entry
is stale, and leaving it skipped hides regressions.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
`desugar_declaration_base' (block scope, and `for'-init declarations) went
through `desugar_init_declarator_BROKEN', a near-copy of
`desugar_init_declarator' marked "TODO: get rid of this function", with the
caller open-coding the typedef registration, the storage-class checks and
the identifier registration that the real function already does.

Fold the two together: `desugar_declaration_base' now calls
`desugar_init_declarator', exactly as the file-scope path in
`desugar_and_register_external_declaration' does, and keeps only what is
specific to block scope (register_internal_object_declaration, block
statics, and the automatic-duration bindings it returns).

Both already bottom out in `wip_desugar_initializer_', so this is
scope/storage-class plumbing, not initialiser logic; the point is that
subsequent initialiser fixes land in one place instead of two. Also
removes the "BROKEN: desugar_declaration_base" debug print.

Two incidental consequences of sharing the file-scope function:
  - _Atomic block declarations now go through `wrap_atomic' rather than
    `Ctype.mk_ctype_atomic', so `_Atomic int *p;' inside a block behaves as
    it already did at file scope instead of hitting an internal error;
  - a typedef with an initialiser, or with an _Alignas, inside a block is
    now reported instead of silently ignoring the initialiser.

CI: 192 passed, 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
STD §6.7.9#14 initialisation of a character array by a string literal is
implemented inline in `wip_desugar_initializer_', where it only fires when
the *whole* declared object is a character array. The cursor machine in
desugaring_init.lem needs the same explosion for a string literal appearing
as an inner initialiser, so move it out to a reusable function next to
`mk_zeroInit'.

`explode_string_literal loc array_ty char_strs' returns the (now complete)
array type, its element type, and one initialiser per element, so a caller
can either build a single AilEarray (as `wip_desugar_initializer_' does
here) or insert one leaf per character (the upcoming cursor caller).

Pure move; no behaviour change. CI: 192 passed, 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
`to_init_path' mapped every union level of the cursor to a member-less
`Elem_union', throwing away which member the designator had selected, and
`constructValue_aux' then unconditionally rebuilt the union through its
*first* member -- announcing as much with a debug-level-0 print on every
union initialisation. So

  union U { int a; double b; } u = { .b = 1.5 };

silently desugared to `(union U){.a= 0}': wrong member, value lost.

Give `Elem_union' the selected member's identifier, and thread a second
map alongside the leaf values recording, for each union's own path, which
member was selected. `constructValue_aux' consults it and falls back to
the first member when a union was never reached (implicit/zero
initialisation). Because the map is written as the initialiser is walked,
a later designator for the same union overwrites an earlier one, which is
what C requires for

  union U u = { .a = 1, .b = 2.5 };   /* b, not a */

New test 0345 covers: designating a non-first member, re-designating in
both directions, a struct-typed member, an implicit (undesignated)
initialiser, a union in an array, and a union in a struct.

CI: 193 passed, 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
Facing an aggregate, an initialiser expression was always pushed all the
way down to a scalar leaf by `go_bottom' -- the code that would have
handled the exceptions was behind a literal

  if false (* is_compound_literal OR string literal *) then
    internal_error "TODO: explode the elements"

So a string literal initialising a member (rather than the whole declared
object) was rejected outright:

  struct S { char s[4]; int n; } x = { "abc", 7 };
  char c[3][4] = { "ab", "cd" };
    error: initializing 'char' with an expression of type 'char*'

Replace `go_bottom' with `go_bottom_or_stop', which stops the descent when
the expression initialises the aggregate it is facing:
  - STD §6.7.9#14: a string literal facing an array of character type, in
    which case the value recorded is the array produced by
    `explode_string_literal';
  - STD §6.7.9#13: a compound literal whose type is compatible with the
    current object.

Three supporting changes:
  - `constructValue_aux' now looks the path up in the map *before*
    dispatching on the type, since a path may name a whole aggregate and
    not just a scalar leaf;
  - the exploded array is built as `AilEarray false', not `true': it is an
    array value inside an aggregate, and the `true' ("came from a string
    literal") flag makes Ail's typing apply the array decay to it;
  - having stopped on an aggregate rather than a leaf, `go_next' would
    descend into it, so the cursor is advanced with
    `do_next_in_same_level' -- otherwise the *following* initialiser was
    lost (`{ "abc", 7 }' left n at 0).

New tests 0346 (string literal as a member, as a row of a 2-D array,
truncated and zero-padded, and reached by a designator) and 0347
(compound literal as a member, as an array element, and reached by a
designator; block scope, since a compound literal is not a constant
expression).

Note this does not unskip 0318-compound-interal-in_global.c: that one
needs `&(struct T){...}' to be accepted as an address constant at file
scope, which is a §6.6 question, not a §6.7.9 one.

CI: 195 passed, 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
STD §6.7.9#15 was unimplemented: the branch for it in
`wip_desugar_initializer_' was guarded by a literal `false', so

  wchar_t w[] = L"ab";

fell through to the generic aggregate path and was rejected with
"initializing 'wchar_t' with an expression with a non arithmetic type
'wchar_t*'".

Add `array_is_initialisable_by_string_literal', which pairs a literal's
encoding prefix with the element type the array must have: none or u8 ->
any character type (§6.7.9#14, as before), u -> char16_t, U -> char32_t,
L -> wchar_t (§6.7.9#15, checked up to compatibility with a qualified or
unqualified version). `explode_string_literal' needed no change: it
already casts each character to the array's element type.

The same predicate replaces the plain-char-only test in the cursor
machine's `go_bottom_or_stop', so a wide literal also works as an inner
initialiser. A literal whose prefix does not match the array is still
rejected, as it should be.

New test 0348. It spells char16_t/char32_t as uint_least16_t /
uint_least32_t because the bundled <uchar.h> is a stub -- adding those
typedefs is a libc change, not a §6.7.9 one.

CI: 196 passed, 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
An excess brace group -- one appearing after the cursor has already run
off the end of the object -- crashed the desugarer:

  int a[2][2] = {{1, 2}, {3, 4}, {5, 6}};
    internal error: Translation called on Ail program with an invalid node

`go_down_entering_block' refuses to descend from an overflowing cursor
(it returns DInit_nothing), and `liftM' turns that into an internal
error, which the caller in cabs_to_ail.lem catches and turns into an
AilEinvalid node -- which then blows up in the elaborator, far from the
cause. An excess *scalar* was fine; only a brace group was not.

Treat a brace group reached while overflowing as what it is: excess. It
is dropped and the cursor stays overflowing.

That also settles the "if we were overflowing before entering the block
we need to STILL be overflowing" TODO: the overflow flag is now captured
before entering the block and restored after leaving it, so the
`unmark_as_overflowing' (which is about the block level being popped)
cannot clear the state of the level being returned to.

Finally, guard the `do_next_in_same_level' call added in the previous
commit against an empty cursor, which means the whole object was
initialised by a single expression and there is no next position.

New test 0349: an excess brace group after a full array, after an
out-of-range designator, and after an excess scalar.

CI: 197 passed, 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
STD §6.7.9#2 makes it a constraint violation for an initialiser to provide
a value for an object outside the entity being initialised. Both sites in
the cursor machine that detect this already knew about it -- one carried

  (* TODO: let* () = Eff.warn "array designator is larger than array" in *)

and the other

  (* NOTE: if there is another initialiser in the list,
     we are un excess (we'll ignore, maybe warn) *)

-- and both silently dropped the value:

  int arr[2] = {1, 2, 3};   /* 3 gone, no diagnostic */
  int a2[5]  = {[7] = 1};   /* 1 gone, no diagnostic */

Warn at all three: an out-of-range array designator, an excess element,
and an excess brace group. We keep accepting the program, as GCC and Clang
do; a later commit adds a switch to reject it.

`Debug.warn' is silent unless the debug level is raised, which is not much
use for a diagnostic aimed at the user, so add `Cerb_debug.warn_always'
(the existing `warn ~always:true', which main.ml and pipeline.ml already
use) and expose it through `Debug.warn_always' and `E.warn_alwaysM'.

New test 0350. Warnings go to stderr, so the existing oracle of
0085-excess_array_initializer.c (which compares stdout) is unaffected.

CI: 198 passed, 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
The previous commit warns about excess and out-of-range initialisers but
keeps accepting them, matching GCC and Clang. STD §6.7.9#2 makes them
constraint violations, so offer that too:

  --switches=strict_initialisers

Adds `ExcessInitializers' and `ArrayDesignatorOutOfRange' to
Constraint.violation (with their §6.7.9#2 references and messages in
pp_errors.ml), `SW_strict_initialisers' to Switches (constructor, the
"strict_initialisers" name in read_switch, and the simple-equality arm of
pred), and exposes it to the Lem sources through Global. The three
reporting sites now go through one `report_excess', which either fails
with the violation or warns.

Split from the previous commit so the default-behaviour change and the new
user-facing knob are independently revertable.

New tests/run-strict-initialisers.sh (following run-copy-prop.sh, since
run-ci.sh has no way to pass per-test switches) checks both directions:
the programs are accepted without the switch and rejected with the
expected §6.7.9#2 message with it.

CI: 198 passed, 0 failed; run-strict-initialisers.sh: 6 passed, 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
When the desugaring of an initialiser fails, cabs_to_ail.lem catches the
internal error and emits `AilEinvalid ty (AilInvalid_desugaring_init_failed
str)' so that the rest of the translation unit can still be processed.
genTyping then typed that node as a well-formed rvalue, so nothing noticed
until elaboration, which died with

  internal error: Translation called on Ail program with an invalid node

-- no location, no mention of the initialiser, and uncatchable.

Report it in genTyping instead, where the node still has a location, and
carry the original message. This is deliberately the last of the §6.7.9
commits: it turns previously-silent failures into hard errors, so it should
only land once the cases that legitimately hit that path are fixed (the
excess brace group of the previous commit was one of them).

No new test: this commit's evidence is that the whole existing suite still
passes with the fallback made loud.

CI: 198 passed, 0 failed; run-strict-initialisers.sh: 6 passed, 0 failed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016p7CXDNqrW4ZWn8RyVdFLw
@dc-mak dc-mak changed the title [DRAFT [DRAFT] Initialisers support Sep 8, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant